Rewriting current goal to an independent theorem

Stream: general

[Jiaming Shan]

I'm writing a tool to decompose all "have" block in the proof to independent theorem, and we can prove them one by one to crack the whole proof. However, I meet some problem when I want to get the current environment, or say what theorems you can use when proving this have block.
For example, here is the example proof I will handle:

import Mathlib
import Aesop

set_option maxHeartbeats 0

open BigOperators Real Nat Topology Rat

/-- Let $x$, $y$ and $z$ all exceed $1$ and let $w$ be a positive number such that $\log_x w = 24$, $\log_y w = 40$ and $\log_{xyz} w = 12$. Find $\log_z w$. Show that it is 060.-/
theorem aime_1983_p1 (x y z w : ℕ) (ht : 1 < x ∧ 1 < y ∧ 1 < z) (hw : 0 ≤ w)
    (h0 : Real.log w / Real.log x = 24) (h1 : Real.log w / Real.log y = 40)
    (h2 : Real.log w / Real.log (x * y * z) = 12) : Real.log w / Real.log z = 60 := by
  have hx : (x : ℝ) > 1 := by
    norm_cast
    <;> linarith [ht.1, ht.2.1, ht.2.2]

  have hy : (y : ℝ) > 1 := by
    norm_cast
    <;> linarith [ht.1, ht.2.1, ht.2.2]

  have hz : (z : ℝ) > 1 := by
    norm_cast
    <;> linarith [ht.1, ht.2.1, ht.2.2]

  have hxyz : (x : ℝ) * y * z > 1 := by
    have h₁ : (x : ℝ) > 1 := hx
    have h₂ : (y : ℝ) > 1 := hy
    have h₃ : (z : ℝ) > 1 := hz
    have h₄ : (x : ℝ) * y > 1 := by
      nlinarith
    nlinarith

I tried two methods. One is just copy paste the goal hint. However, the hxyz goal is:

x y z w : ℕ
ht : 1 < x ∧ 1 < y ∧ 1 < z
hw : 0 ≤ w
h0 : Real.log ↑w / Real.log ↑x = 24
h1 : Real.log ↑w / Real.log ↑y = 40
h2 : Real.log ↑w / Real.log (↑x * ↑y * ↑z) = 12
hx : ↑x > 1
hy : ↑y > 1
hz : ↑z > 1
⊢ ↑x * ↑y * ↑z > 1

Notice that ↑ cannot be handled, because ℝ doesn't occur in this hint.

The second method is just copy all it's previous hypothesis before it in the lean proof. However, in that case, I cannot handle some assumption introduced by like by_contra h in the parent have, which will change the state in an unknown way unless you check the goal hint, and that go back to the first problem.

Is there any easy way to do this?

[Kevin Buzzard]

because ℝ doesn't occur in this hint.

Why don't you make x,y,z,w real numbers? Surely that is what is meant in the statement? Then you'd see the reals in the context.

[Jiaming Shan]

That's a good point. I think it's a minif2f dataset problem.

[David Loeffler]

Are you aware of the extract_goal tactic? This prints a theorem statement listing the current hypotheses and asserting the current goal follows from them. This is what I always use if I want to factor out a have block into an independent theorem. It sounds quite similar to what you're doing.

[Jiaming Shan]

Thanks, that's really relavant! I checked the doc and found that it's relevant with delaboration, and I can use set_option pp.coercions.types true to solve my type problem.