I wrote a proof to say the range of f under A intersect B subsets the range of f under A intersect the range of f under B. That makes sense, A intersect B subsets A and A intersect B subsets B, so why would a mapping change anything?
But man proofs are weird! Let’s look at this guys!
What in God’s green earth! Line by line we go:
Line 1) the claim i.e. “the range of f under A intersect B subsets the range of f under A intersect the range of f under B
Line 2) the first assumption. Implicit is the claim is the question what? The answer is “for everything!”. So we assume a trivial (nothin special object) to make the claim. Very good.
Line 3) the second assumption Y is in the range of f under A intersect B. Why assume it? Because anytime you prove a set subsets another, you just need to prove an arbitrary object does it. Not bad.
Line 4) what we need. That y is in the intersection of. the image of f under A and the image of f under B. Again, this is the general structure for any subset proof.
Line 4.5 and 5) This is where it gets juicey! Exists.elim?? What exists statement are we eliminating? I’m so confuded? Dan you lied, you have introduced an exists statement anywhere! Oh, joke’s on you. Implicit in line 4 is the fact “there exists a y s.t. it’s in the set”. Boom roasted! Anyway… on line 5 we introduce another arbitrary object a, which could be any atomic element of A or B? Why? Keep reading?
Line 6) Exists.elim don’t really “eliminate” so much as “use” and they use the exists statements by coupling them with a strong rule. The rule states that anything that matches the object in the exists follows a certain rule. Or, for all a who satisfy this thing something here goes nothing.. (coming back to it)
Line 7) Zooming out, my human brain makes sense. a exists, a in A, and f a = y, so how the hell could y not be in f ” A? The kicker here is what does it mean to be in the image of f under A? That gets into this whole convoulted thing … blah blah blah nobody cares you have to prove it with an exists.intro statement. And lean is like screw that! This is obvious! Here come my delightful curvy brackets to the rescue!
Line 8) similar
Line 9) hey! Isn’t this fun. An intersection is just like (you, guessed it) a conjunctive statement. So and.intro functions the same here. we combine the two points, get our resolution and go happily on our way, never wondering about images under functions again.
Dan-Knight 