Extracting a term from a proof

Stream: new members

[Rado Kirov]

I have a proof h: ↑(f ⟨↑z1, ⋯⟩) = ↑(nat_equiv n), I want to do some rewritings that begin with have  := (f ⟨↑z1, ⋯⟩).property but of course I can't write ... or _ because there is nowhere to infer from. But also I don't want to spell out the subtype proof. How to extract the term into a def term = ...that I can use in my new haves and existing proofs.

[Niels Voss]

I'm not completely sure what you're asking but do you know about the generalize_proofs tactic?

[Rado Kirov]

good point, yes I think that should work. I was hoping there is something like conv mode, but at the end instead of applying a tactic I extract the term into a variable.

[Rado Kirov]

have h: ↑(f ⟨↑z1, ⋯⟩) = ↑(nat_equiv n) := by sorry
<... some magic that generates t := f ⟨↑z1, ⋯⟩ so now h is h: ↑t = ↑(nat_equiv n) ... >
have := t.prop

[Rado Kirov]

btw, generalize_proofs did unblock me, but it is quite a blunt tool as I have no control over which proofs it extracts.

[Matt Diamond]

@Rado Kirov you may find this short thread useful:

#new members > rewriting an expression without writing it again

[Matt Diamond]

(though apparently the change ?x = c trick results in an unused tactic linter error)

[Matt Diamond]

also @Kyle Miller came up with a neat trick here:

#new members > Extracting left-hand side from an equality @ 💬

[Matt Diamond]

@Kyle Miller did we ever come up with a better way of doing this?

[Kyle Miller]

I don't think so.

I guess there's this new technique available in 4.22:

import Mathlib.Data.Nat.Basic

example (a b c d e : ℕ) (h : a + b + c + d + e = 0) : False := by
  conv at h => enter [1]; change ?foo
  let (eq := foo_eq) foo := ?foo
  rw [← foo_eq] at h
  /-
  a b c d e : ℕ
  foo : ℕ := a + b + c + d + e
  h : foo = 0
  foo_eq : foo = a + b + c + d + e
  ⊢ False
  -/
  sorry