# Zulip Chat Archive

## 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