I'm trying to prove example (C A S: Prop) (h1 : C → A) (h2 : A → S) : C → S. It's this level in the Lean Intro to Logic game. So far I have
have a : A := h1 c
have s : S := h2 a
exact λc ↦ s
which doesn't work because I don't have c yet. I just don't know how the beginning should be. That is, I don't know how to get c : C to begin with. I tried have c : C → C := λc ↦ c, but that's obviously not it.
Am I going about this completely wrong, or am I on the right track?
I’m not terribly familiar with this game or what it has already covered before. However, as you point out you can’t actually use h1 until you have some c : C. I think right now the only tool you have to create such a c is λ c ↦ … (or equivalently fun c => …). But you can’t then make an intermediate lemma with have. As far as I can see, you just need to do it in one go with exact λ c ↦ …. (That is the most I’m willing to give as a hint.)
Later in the game (and certainly in real Lean), you can use the tactic intro c to make such a c:C and put it into your local context.
