Working with lambdas + "some"

Stream: new members

[Torger Olson]

I'm almost done formalizing an assignment, but I'm struggling to make progress with this last one. I'm not used to working with 'λ' or 'some'. Any suggests for this current state or where I can read up on 'λ' and 'some'?

A B C : Type,
f : A → B,
g : C → B,
s : f '' univ ⊆ g '' univ,
v : A → C := λ (a : A), (λ (_x : some _ ∈ univ ∧ g (some _) = f a), some _) _,
x : A
⊢ f x = g (v x)

[Alex J. Best]

Lambdas are how you define functions, see e.g. https://leanprover.github.io/theorem_proving_in_lean/dependent_type_theory.html#function-abstraction-and-evaluation. And I'm guessing some is docs#classical.some (see https://leanprover.github.io/theorem_proving_in_lean/axioms_and_computation.html#choice).

[Alex J. Best]

Its more easy to help if you post a self contained #mwe, so some small block of code with imports that results in this tactic state rather than just the tactic state.

[Alex J. Best]

That said you probably want to rw v to replace v with its definition and maybe simp or dsimp after to see what you're left with. And the fundamental property of docs#classical.some is docs#classical.some_spec, so you'll likely need that

[Torger Olson]

Okay thanks. I'll keep reading/trying.

In case you or someone see's an obvious fix here's my mwe:

import data.set
open set function classical

variables (A B C : Type)
variable (f : A → B)
variable (g : C → B)

example (s : f '' univ ⊆ g '' univ) : ∃ (v : A → C), f = g ∘ v :=
begin
  let v : A → C,
  intro a,
  have h1 : f a ∈ g '' univ,
  sorry,
  rw mem_image at h1,
  choose c hc using h1,
  exact c,
  use v,
end

[Alex J. Best]

Here's what I would do, note the use of tactic#generalize_proofs to replace the long and ugly proof term hidden behind the underscore with just h, that can then be fed into some_spec.

import data.set
open set function classical

variables (A B C : Type)
variable (f : A → B)
variable (g : C → B)

--set_option pp.proofs true -- this will let you see what the underscores are below, but they are long and ugly expressions

example (s : f '' univ ⊆ g '' univ) : ∃ (v : A → C), f = g ∘ v :=
begin
  let v : A → C,
  { intro a,
    have h1 : f a ∈ g '' univ,
    { apply s,
      simp, },
    --rw mem_image at h1,
    choose c hc using h1,
    exact c, },
  { use v,
    ext x,
    simp [v],
    generalize_proofs h,
    rw some_spec h, },
end