## Stream: new members

### Topic: term style equivalent to use

#### Kevin Doran (Mar 29 2020 at 11:26):

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 (Mar 29 2020 at 11:27):

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

#### Patrick Massot (Mar 29 2020 at 11:29):

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

#### Kevin Buzzard (Mar 29 2020 at 11:29):

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

#### Kevin Doran (Mar 29 2020 at 11:33):

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 (Mar 29 2020 at 11:33):

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 (Mar 29 2020 at 11:40):

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 (Mar 29 2020 at 11:40):

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

#### Kevin Doran (Mar 30 2020 at 00:47):

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

Last updated: May 10 2021 at 17:39 UTC