naming a value that is trapped inside some other hypothesis

Stream: new members

[Michael]

I have a function that returns a value based in part on something obtained from Exists.choose.

I apply that function and get a Prop variable that is represented as $b \in \mathrm{other\_function} \,\,\cdots\mathrm{.choose} \,\,\, x$

I'd like to isolate that ⋯.choose value (contained in the Prop variable) and give it a name, so that I can apply Exists.choose_spec and otherwise manipulate it. How do I do that?

[Aaron Liu]

there's generalize_proofs in mathlib batteries

[Snir Broshi]

Do you mean set foo := s.choose?
Can you create a #mwe?

[Michael]

import Mathlib.Data.Nat.Basic
import Mathlib.Order.Basic

section

theorem archimedes : (∀ n : ℕ, ∃ m, m > n) := by
  intro n
  exists n.succ
  apply LT.lt.gt
  apply Nat.lt_succ_iff.mpr
  exact Nat.le_refl n

example : 1 = 1 := by
  let plus_something := fun (n : ℕ) ↦ by
    let something := Exists.choose (archimedes n)
    exact n + something
  let x := plus_something 4
  have hx : x = plus_something 4 := by rfl
  unfold plus_something at hx
  have h1 : 3 + x > 10 := by
    rw [hx] -- 3 + (4 + ⋯.choose) > 10
    -- I need to show that "⋯.choose" > 3,
    -- which will be easier if I can name it
    --
    -- I want something like:
    -- let y := "⋯.choose"
    -- have hy : y > 4 := by apply Exists.choose_spec
    -- simp
    sorry
  rfl

end

[Eric Wieser]

I would guess you want to start with

import Mathlib.Data.Nat.Basic
import Mathlib.Order.Basic
import Mathlib.Tactic.Choose

section

theorem archimedes : (∀ n : ℕ, ∃ m, m > n) := by
  sorry -- what you already have is fine

example : 1 = 1 := by
  choose arch h_arch using archimedes
  let plus_something := fun (n : ℕ) ↦ n + arch n

[Michael]

there's not a way to assign a name to a value?

[Eric Wieser]

I'm more making the claim that you probably don't want to end up in the position where that question is relevant in the first place

[Aaron Liu]

Michael said:

import Mathlib.Data.Nat.Basic
import Mathlib.Order.Basic

section

theorem archimedes : (∀ n : ℕ, ∃ m, m > n) := by
  intro n
  exists n.succ
  apply LT.lt.gt
  apply Nat.lt_succ_iff.mpr
  exact Nat.le_refl n

example : 1 = 1 := by
  let plus_something := fun (n : ℕ) ↦ by
    let something := Exists.choose (archimedes n)
    exact n + something
  let x := plus_something 4
  have hx : x = plus_something 4 := by rfl
  unfold plus_something at hx
  have h1 : 3 + x > 10 := by
    rw [hx] -- 3 + (4 + ⋯.choose) > 10
    -- I need to show that "⋯.choose" > 3,
    -- which will be easier if I can name it
    --
    -- I want something like:
    -- let y := "⋯.choose"
    -- have hy : y > 4 := by apply Exists.choose_spec
    -- simp
    sorry
  rfl

end

here we go

import Mathlib.Data.Nat.Basic
import Mathlib.Order.Basic
import Batteries.Tactic.GeneralizeProofs

section

theorem archimedes : (∀ n : ℕ, ∃ m, m > n) := by
  intro n
  exists n.succ
  apply LT.lt.gt
  apply Nat.lt_succ_iff.mpr
  exact Nat.le_refl n

example : 1 = 1 := by
  let plus_something := fun (n : ℕ) ↦ by
    let something := Exists.choose (archimedes n)
    exact n + something
  let x := plus_something 4
  have hx : x = plus_something 4 := by rfl
  unfold plus_something at hx
  have h1 : 3 + x > 10 := by
    rw [hx] -- 3 + (4 + ⋯.choose) > 10
    -- I need to show that "⋯.choose" > 3,
    -- which will be easier if I can name it
    --
    -- I want something like:
    -- let y := "⋯.choose"
    -- have hy : y > 4 := by apply Exists.choose_spec
    -- simp
    generalize_proofs h at hx
    let y := h.choose
    have hy : y > 4 := by apply Exists.choose_spec
    simp
    sorry
  rfl

end