term style equivalent to `use`

Stream: new members

[Kevin Doran]

I am trying to write a term-style solution to @Kevin Buzzard's maths challenges. I'm a little stuck on #4, with the following progress (and tactic solution included at the bottom for comparison):

import data.real.basic

open function

theorem challenge4
 (X Y Z : Type)
 (f : X → Y)
 (g : Y → Z) :
surjective (g ∘ f) → surjective g :=
assume h₁,
assume z,
 have h₂ : ∃y : Y, g y = z, from exists.elim (h₁ z)
 (assume (x : X) (hh₁ : (g ∘ f) x = z),
   have hh₂ : g (f x) = z, from hh₁, -- I'm not sure how to create a variable, y : Y, using f x.
   --exists.intro (f x) hh₂
   sorry),
 h₂

theorem challenge4_tactic
 (X Y Z : Type)
 (f : X → Y)
 (g : Y → Z) :
surjective (g ∘ f) → surjective g :=
begin
 intro h,
 intro z,
 cases h z with a ha,
 use f a,
 assumption,
end

[Kevin Buzzard]

Oh yeah, I can never do those crazy assume have proofs either. Why not just go full lambda-calculus?

[Patrick Massot]

let y := f x in exists.intro y hh₂

[Kevin Buzzard]

You can replace the sorry with ⟨f x, hh₂⟩

[Kevin Doran]

Kevin Buzzard said:

Oh yeah, I can never do those crazy assume have proofs either. Why not just go full lambda-calculus?

The downside of starting with the fantastic "Logic and Proof" website is that my understanding is currently rooted pretty exclusively in assume proofs.

[Kevin Doran]

Patrick Massot said:

let y := f x in exists.intro y hh₂

Thanks! That's what I needed. I didn't know of let ... in.

[Kevin Buzzard]

Kevin Doran said:

The downside of starting with the fantastic "Logic and Proof" website is that my understanding is currently rooted pretty exclusively in assume proofs.

Are you the kind of person who understands those big fractions with Gamma ⊢ x : P on the top and bottom?

[Kevin Buzzard]

All I know is that you don't have to have a clue about those to use Lean.

[Kevin Doran]

I'm trying to follow that path! The assume have proofs get out of hand quickly.