awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
Goal:
f g : AbsoluteValue ℚ ℝ
h_1 : ∃ (c : ℝ), 0 < c ∧ ∀ (n : ℕ), HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) c = (g : (a : ℚ) → ℝ) (↑n : ℚ)
c : ℝ
hc : 0 < c
h : ∀ (n : ℕ), HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) c = (g : (a : ℚ) → ℝ) (↑n : ℚ)
x : ℚ
h₁ :
  HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (HDiv.hDiv (α := ℚ) (↑x.num : ℚ) (↑x.den : ℚ)) : ℝ) c =
    (g : (a : ℚ) → ℝ) (HDiv.hDiv (α := ℚ) (↑x.num : ℚ) (↑x.den : ℚ))
⊢ HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) x : ℝ) c = (g : (a : ℚ) → ℝ) x
have h₂ : HDiv.hDiv (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑x.num : ℚ) : ℝ) ((f : (a : ℚ) → ℝ) (↑x.den : ℚ) : ℝ) ^ c =
  (g : (a : ℚ) → ℝ) (HDiv.hDiv (α := ℚ) (↑x.num : ℚ) (↑x.den : ℚ))
Tactic: rw [← Rat.num_div_den x, map_div₀, map_div₀, div_rpow (by positivity) (by positivity), h x.den,
    ← apply_natAbs_eq, ← apply_natAbs_eq, h (natAbs x.num)]
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
Goal:
f g : AbsoluteValue ℚ ℝ
h_1 : ∃ (c : ℝ), 0 < c ∧ ∀ (n : ℕ), HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) c = (g : (a : ℚ) → ℝ) (↑n : ℚ)
c : ℝ
hc : 0 < c
h : ∀ (n : ℕ), HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) c = (g : (a : ℚ) → ℝ) (↑n : ℚ)
x : ℚ
h₁ :
  HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (HDiv.hDiv (α := ℚ) (↑x.num : ℚ) (↑x.den : ℚ)) : ℝ) c =
    (g : (a : ℚ) → ℝ) (HDiv.hDiv (α := ℚ) (↑x.num : ℚ) (↑x.den : ℚ))
h₂ :
  HDiv.hDiv (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑x.num : ℚ) : ℝ) ((f : (a : ℚ) → ℝ) (↑x.den : ℚ) : ℝ) ^ c =
    (g : (a : ℚ) → ℝ) (HDiv.hDiv (α := ℚ) (↑x.num : ℚ) (↑x.den : ℚ))
⊢ HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) x : ℝ) c = (g : (a : ℚ) → ℝ) x
have h₃ : HDiv.hDiv (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑x.num : ℚ) : ℝ) ((f : (a : ℚ) → ℝ) (↑x.den : ℚ) : ℝ) ^ c =
  HDiv.hDiv (α := ℝ) (β := ℝ) ((g : (a : ℚ) → ℝ) (↑x.num : ℚ) : ℝ) ((g : (a : ℚ) → ℝ) (↑x.den : ℚ) : ℝ)
Tactic: rw [← Rat.num_div_den x, map_div₀, map_div₀, div_rpow (by positivity) (by positivity), h x.den,
    ← apply_natAbs_eq, ← apply_natAbs_eq, h (natAbs x.num)]
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
Goal:
f g : AbsoluteValue ℚ ℝ
h_1 : ∃ (c : ℝ), 0 < c ∧ ∀ (n : ℕ), HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) c = (g : (a : ℚ) → ℝ) (↑n : ℚ)
c : ℝ
hc : 0 < c
h : ∀ (n : ℕ), HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) c = (g : (a : ℚ) → ℝ) (↑n : ℚ)
x : ℚ
h₁ :
  HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (HDiv.hDiv (α := ℚ) (↑x.num : ℚ) (↑x.den : ℚ)) : ℝ) c =
    (g : (a : ℚ) → ℝ) (HDiv.hDiv (α := ℚ) (↑x.num : ℚ) (↑x.den : ℚ))
h₂ :
  HDiv.hDiv (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑x.num : ℚ) : ℝ) ((f : (a : ℚ) → ℝ) (↑x.den : ℚ) : ℝ) ^ c =
    (g : (a : ℚ) → ℝ) (HDiv.hDiv (α := ℚ) (↑x.num : ℚ) (↑x.den : ℚ))
h₃ :
  HDiv.hDiv (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑x.num : ℚ) : ℝ) ((f : (a : ℚ) → ℝ) (↑x.den : ℚ) : ℝ) ^ c =
    HDiv.hDiv (α := ℝ) (β := ℝ) ((g : (a : ℚ) → ℝ) (↑x.num : ℚ) : ℝ) ((g : (a : ℚ) → ℝ) (↑x.den : ℚ) : ℝ)
⊢ HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) x : ℝ) c = (g : (a : ℚ) → ℝ) x
have h₄ : HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑x.num : ℚ) : ℝ) c / HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑x.den : ℚ) : ℝ) c =
  HDiv.hDiv (α := ℝ) (β := ℝ) ((g : (a : ℚ) → ℝ) (↑x.num : ℚ) : ℝ) ((g : (a : ℚ) → ℝ) (↑x.den : ℚ) : ℝ)
Tactic: rw [← Rat.num_div_den x, map_div₀, map_div₀, div_rpow (by positivity) (by positivity), h x.den,
    ← apply_natAbs_eq, ← apply_natAbs_eq, h (natAbs x.num)]
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
Goal:
f g : AbsoluteValue ℚ ℝ
h_1 : ∃ (c : ℝ), 0 < c ∧ ∀ (n : ℕ), HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) c = (g : (a : ℚ) → ℝ) (↑n : ℚ)
c : ℝ
hc : 0 < c
h : ∀ (n : ℕ), HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) c = (g : (a : ℚ) → ℝ) (↑n : ℚ)
x : ℚ
h₁ :
  HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (HDiv.hDiv (α := ℚ) (↑x.num : ℚ) (↑x.den : ℚ)) : ℝ) c =
    (g : (a : ℚ) → ℝ) (HDiv.hDiv (α := ℚ) (↑x.num : ℚ) (↑x.den : ℚ))
h₂ :
  HDiv.hDiv (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑x.num : ℚ) : ℝ) ((f : (a : ℚ) → ℝ) (↑x.den : ℚ) : ℝ) ^ c =
    (g : (a : ℚ) → ℝ) (HDiv.hDiv (α := ℚ) (↑x.num : ℚ) (↑x.den : ℚ))
h₃ :
  HDiv.hDiv (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑x.num : ℚ) : ℝ) ((f : (a : ℚ) → ℝ) (↑x.den : ℚ) : ℝ) ^ c =
    HDiv.hDiv (α := ℝ) (β := ℝ) ((g : (a : ℚ) → ℝ) (↑x.num : ℚ) : ℝ) ((g : (a : ℚ) → ℝ) (↑x.den : ℚ) : ℝ)
h₄ :
  HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑x.num : ℚ) : ℝ) c /
      HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑x.den : ℚ) : ℝ) c =
    HDiv.hDiv (α := ℝ) (β := ℝ) ((g : (a : ℚ) → ℝ) (↑x.num : ℚ) : ℝ) ((g : (a : ℚ) → ℝ) (↑x.den : ℚ) : ℝ)
⊢ HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) x : ℝ) c = (g : (a : ℚ) → ℝ) x
have h₅ : HDiv.hDiv (β := ℝ) (HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑x.num : ℚ) : ℝ) c) ((g : (a : ℚ) → ℝ) (↑x.den : ℚ) : ℝ) =
  HDiv.hDiv (α := ℝ) (β := ℝ) ((g : (a : ℚ) → ℝ) (↑x.num : ℚ) : ℝ) ((g : (a : ℚ) → ℝ) (↑x.den : ℚ) : ℝ)
Tactic: rw [← Rat.num_div_den x, map_div₀, map_div₀, div_rpow (by positivity) (by positivity), h x.den,
    ← apply_natAbs_eq, ← apply_natAbs_eq, h (natAbs x.num)]
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
Goal:
f g : AbsoluteValue ℚ ℝ
h_1 : ∃ (c : ℝ), 0 < c ∧ ∀ (n : ℕ), HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) c = (g : (a : ℚ) → ℝ) (↑n : ℚ)
c : ℝ
hc : 0 < c
h : ∀ (n : ℕ), HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) c = (g : (a : ℚ) → ℝ) (↑n : ℚ)
x : ℚ
h₁ :
  HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (HDiv.hDiv (α := ℚ) (↑x.num : ℚ) (↑x.den : ℚ)) : ℝ) c =
    (g : (a : ℚ) → ℝ) (HDiv.hDiv (α := ℚ) (↑x.num : ℚ) (↑x.den : ℚ))
h₂ :
  HDiv.hDiv (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑x.num : ℚ) : ℝ) ((f : (a : ℚ) → ℝ) (↑x.den : ℚ) : ℝ) ^ c =
    (g : (a : ℚ) → ℝ) (HDiv.hDiv (α := ℚ) (↑x.num : ℚ) (↑x.den : ℚ))
h₃ :
  HDiv.hDiv (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑x.num : ℚ) : ℝ) ((f : (a : ℚ) → ℝ) (↑x.den : ℚ) : ℝ) ^ c =
    HDiv.hDiv (α := ℝ) (β := ℝ) ((g : (a : ℚ) → ℝ) (↑x.num : ℚ) : ℝ) ((g : (a : ℚ) → ℝ) (↑x.den : ℚ) : ℝ)
h₄ :
  HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑x.num : ℚ) : ℝ) c /
      HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑x.den : ℚ) : ℝ) c =
    HDiv.hDiv (α := ℝ) (β := ℝ) ((g : (a : ℚ) → ℝ) (↑x.num : ℚ) : ℝ) ((g : (a : ℚ) → ℝ) (↑x.den : ℚ) : ℝ)
h₅ :
  HDiv.hDiv (β := ℝ) (HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑x.num : ℚ) : ℝ) c) ((g : (a : ℚ) → ℝ) (↑x.den : ℚ) : ℝ) =
    HDiv.hDiv (α := ℝ) (β := ℝ) ((g : (a : ℚ) → ℝ) (↑x.num : ℚ) : ℝ) ((g : (a : ℚ) → ℝ) (↑x.den : ℚ) : ℝ)
⊢ HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) x : ℝ) c = (g : (a : ℚ) → ℝ) x
have h₆ : HDiv.hDiv (β := ℝ) (HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑x.num.natAbs : ℚ) : ℝ) c)
    ((g : (a : ℚ) → ℝ) (↑x.den : ℚ) : ℝ) =
  HDiv.hDiv (α := ℝ) (β := ℝ) ((g : (a : ℚ) → ℝ) (↑x.num : ℚ) : ℝ) ((g : (a : ℚ) → ℝ) (↑x.den : ℚ) : ℝ)
Tactic: rw [← Rat.num_div_den x, map_div₀, map_div₀, div_rpow (by positivity) (by positivity), h x.den,
    ← apply_natAbs_eq, ← apply_natAbs_eq, h (natAbs x.num)]
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
Goal:
f g : AbsoluteValue ℚ ℝ
h_1 : ∃ (c : ℝ), 0 < c ∧ ∀ (n : ℕ), HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) c = (g : (a : ℚ) → ℝ) (↑n : ℚ)
c : ℝ
hc : 0 < c
h : ∀ (n : ℕ), HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) c = (g : (a : ℚ) → ℝ) (↑n : ℚ)
x : ℚ
h₁ :
  HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (HDiv.hDiv (α := ℚ) (↑x.num : ℚ) (↑x.den : ℚ)) : ℝ) c =
    (g : (a : ℚ) → ℝ) (HDiv.hDiv (α := ℚ) (↑x.num : ℚ) (↑x.den : ℚ))
h₂ :
  HDiv.hDiv (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑x.num : ℚ) : ℝ) ((f : (a : ℚ) → ℝ) (↑x.den : ℚ) : ℝ) ^ c =
    (g : (a : ℚ) → ℝ) (HDiv.hDiv (α := ℚ) (↑x.num : ℚ) (↑x.den : ℚ))
h₃ :
  HDiv.hDiv (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑x.num : ℚ) : ℝ) ((f : (a : ℚ) → ℝ) (↑x.den : ℚ) : ℝ) ^ c =
    HDiv.hDiv (α := ℝ) (β := ℝ) ((g : (a : ℚ) → ℝ) (↑x.num : ℚ) : ℝ) ((g : (a : ℚ) → ℝ) (↑x.den : ℚ) : ℝ)
h₄ :
  HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑x.num : ℚ) : ℝ) c /
      HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑x.den : ℚ) : ℝ) c =
    HDiv.hDiv (α := ℝ) (β := ℝ) ((g : (a : ℚ) → ℝ) (↑x.num : ℚ) : ℝ) ((g : (a : ℚ) → ℝ) (↑x.den : ℚ) : ℝ)
h₅ :
  HDiv.hDiv (β := ℝ) (HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑x.num : ℚ) : ℝ) c) ((g : (a : ℚ) → ℝ) (↑x.den : ℚ) : ℝ) =
    HDiv.hDiv (α := ℝ) (β := ℝ) ((g : (a : ℚ) → ℝ) (↑x.num : ℚ) : ℝ) ((g : (a : ℚ) → ℝ) (↑x.den : ℚ) : ℝ)
h₆ :
  HDiv.hDiv (β := ℝ) (HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑x.num.natAbs : ℚ) : ℝ) c)
      ((g : (a : ℚ) → ℝ) (↑x.den : ℚ) : ℝ) =
    HDiv.hDiv (α := ℝ) (β := ℝ) ((g : (a : ℚ) → ℝ) (↑x.num : ℚ) : ℝ) ((g : (a : ℚ) → ℝ) (↑x.den : ℚ) : ℝ)
⊢ HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) x : ℝ) c = (g : (a : ℚ) → ℝ) x
have h₇ : HDiv.hDiv (β := ℝ) (HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑x.num.natAbs : ℚ) : ℝ) c)
    ((g : (a : ℚ) → ℝ) (↑x.den : ℚ) : ℝ) =
  HDiv.hDiv (α := ℝ) (β := ℝ) ((g : (a : ℚ) → ℝ) (↑x.num.natAbs : ℚ) : ℝ) ((g : (a : ℚ) → ℝ) (↑x.den : ℚ) : ℝ)
Tactic: rw [← Rat.num_div_den x, map_div₀, map_div₀, div_rpow (by positivity) (by positivity), h x.den,
    ← apply_natAbs_eq, ← apply_natAbs_eq, h (natAbs x.num)]
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
Goal:
f g : AbsoluteValue ℚ ℝ
h_1 : ∃ (c : ℝ), 0 < c ∧ ∀ (n : ℕ), HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) c = (g : (a : ℚ) → ℝ) (↑n : ℚ)
c : ℝ
hc : 0 < c
h : ∀ (n : ℕ), HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) c = (g : (a : ℚ) → ℝ) (↑n : ℚ)
x : ℚ
h₁ :
  HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (HDiv.hDiv (α := ℚ) (↑x.num : ℚ) (↑x.den : ℚ)) : ℝ) c =
    (g : (a : ℚ) → ℝ) (HDiv.hDiv (α := ℚ) (↑x.num : ℚ) (↑x.den : ℚ))
h₂ :
  HDiv.hDiv (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑x.num : ℚ) : ℝ) ((f : (a : ℚ) → ℝ) (↑x.den : ℚ) : ℝ) ^ c =
    (g : (a : ℚ) → ℝ) (HDiv.hDiv (α := ℚ) (↑x.num : ℚ) (↑x.den : ℚ))
h₃ :
  HDiv.hDiv (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑x.num : ℚ) : ℝ) ((f : (a : ℚ) → ℝ) (↑x.den : ℚ) : ℝ) ^ c =
    HDiv.hDiv (α := ℝ) (β := ℝ) ((g : (a : ℚ) → ℝ) (↑x.num : ℚ) : ℝ) ((g : (a : ℚ) → ℝ) (↑x.den : ℚ) : ℝ)
h₄ :
  HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑x.num : ℚ) : ℝ) c /
      HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑x.den : ℚ) : ℝ) c =
    HDiv.hDiv (α := ℝ) (β := ℝ) ((g : (a : ℚ) → ℝ) (↑x.num : ℚ) : ℝ) ((g : (a : ℚ) → ℝ) (↑x.den : ℚ) : ℝ)
h₅ :
  HDiv.hDiv (β := ℝ) (HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑x.num : ℚ) : ℝ) c) ((g : (a : ℚ) → ℝ) (↑x.den : ℚ) : ℝ) =
    HDiv.hDiv (α := ℝ) (β := ℝ) ((g : (a : ℚ) → ℝ) (↑x.num : ℚ) : ℝ) ((g : (a : ℚ) → ℝ) (↑x.den : ℚ) : ℝ)
h₆ :
  HDiv.hDiv (β := ℝ) (HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑x.num.natAbs : ℚ) : ℝ) c)
      ((g : (a : ℚ) → ℝ) (↑x.den : ℚ) : ℝ) =
    HDiv.hDiv (α := ℝ) (β := ℝ) ((g : (a : ℚ) → ℝ) (↑x.num : ℚ) : ℝ) ((g : (a : ℚ) → ℝ) (↑x.den : ℚ) : ℝ)
h₇ :
  HDiv.hDiv (β := ℝ) (HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑x.num.natAbs : ℚ) : ℝ) c)
      ((g : (a : ℚ) → ℝ) (↑x.den : ℚ) : ℝ) =
    HDiv.hDiv (α := ℝ) (β := ℝ) ((g : (a : ℚ) → ℝ) (↑x.num.natAbs : ℚ) : ℝ) ((g : (a : ℚ) → ℝ) (↑x.den : ℚ) : ℝ)
⊢ HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) x : ℝ) c = (g : (a : ℚ) → ℝ) x
have h₈ : HDiv.hDiv (α := ℝ) (β := ℝ) ((g : (a : ℚ) → ℝ) (↑x.num.natAbs : ℚ) : ℝ) ((g : (a : ℚ) → ℝ) (↑x.den : ℚ) : ℝ) =
  HDiv.hDiv (α := ℝ) (β := ℝ) ((g : (a : ℚ) → ℝ) (↑x.num.natAbs : ℚ) : ℝ) ((g : (a : ℚ) → ℝ) (↑x.den : ℚ) : ℝ)
Tactic: rw [← Rat.num_div_den x, map_div₀, map_div₀, div_rpow (by positivity) (by positivity), h x.den,
    ← apply_natAbs_eq, ← apply_natAbs_eq, h (natAbs x.num)]
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
Goal:
f : AbsoluteValue ℚ ℝ
hf_nontriv : f.IsNontrivial
bdd : ∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
⊢ ∃ (n : ℕ), n ≠ 0 ∧ Ne (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
have contrapose! : ∀ (hf_nontriv : ∀ (n : ℕ) (_ : n ≠ 0), Eq (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)), ¬f.IsNontrivial
Tactic: contrapose! hf_nontriv
Cleared hypotheses: hf_nontriv
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
Goal:
f : AbsoluteValue ℚ ℝ
bdd : ∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
hf_nontriv : ∀ (n : ℕ) (_ : n ≠ 0), Eq (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
⊢ ¬f.IsNontrivial
have refine : ∀ (n : ℕ), Eq (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) ((AbsoluteValue.trivial : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ)
Tactic: refine (isNontrivial_iff_ne_trivial f).not_left.mpr <| eq_on_nat_iff_eq.mp fun n ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
Goal:
f : AbsoluteValue ℚ ℝ
bdd : ∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
hf_nontriv : ∀ (n : ℕ) (_ : n ≠ 0), Eq (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
n : ℕ
⊢ Eq (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) ((AbsoluteValue.trivial : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ)
have inl : Eq (α := ℝ) ((f : (a : ℚ) → ℝ) (↑0 : ℚ) : ℝ) ((AbsoluteValue.trivial : (a : ℚ) → ℝ) (↑0 : ℚ) : ℝ)
Tactic: rcases eq_or_ne n 0 with rfl | hn
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
Goal:
f : AbsoluteValue ℚ ℝ
bdd : ∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
hf_nontriv : ∀ (n : ℕ) (_ : n ≠ 0), Eq (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
n : ℕ
inl : Eq (α := ℝ) ((f : (a : ℚ) → ℝ) (↑0 : ℚ) : ℝ) ((AbsoluteValue.trivial : (a : ℚ) → ℝ) (↑0 : ℚ) : ℝ)
⊢ Eq (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) ((AbsoluteValue.trivial : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ)
have inr : ∀ (hn : n ≠ 0), Eq (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) ((AbsoluteValue.trivial : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ)
Tactic: rcases eq_or_ne n 0 with rfl | hn
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
Goal:
f : AbsoluteValue ℚ ℝ
hf_nontriv : f.IsNontrivial
bdd : ∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
⊢ ∃ (p : ℕ),
    (LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) ∧
        LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) (1 : ℝ)) ∧
      ∀ (m : ℕ),
        LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧
            LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) →
          p ≤ m
have obtain : ∀ (n : ℕ) (hn1 : n ≠ 0) (hn2 : Ne (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)),
  ∃ (p : ℕ),
    (LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) ∧
        LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) (1 : ℝ)) ∧
      ∀ (m : ℕ),
        LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧
            LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) →
          p ≤ m
Tactic: obtain ⟨n, hn1, hn2⟩ : ∃ n : ℕ, n ≠ 0 ∧ f n ≠ 1 := by
    contrapose! hf_nontriv
    refine (isNontrivial_iff_ne_trivial f).not_left.mpr <| eq_on_nat_iff_eq.mp fun n ↦ ?_
    rcases eq_or_ne n 0 with rfl | hn
    · simp
    · simp [hf_nontriv, hn]
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (hypothesis)
Goal:
f : AbsoluteValue ℚ ℝ
hf_nontriv : f.IsNontrivial
bdd : ∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
n : ℕ
hn1 : n ≠ 0
hn2 : Ne (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
P : Set ℕ :=
  {m : ℕ |
    LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ)}
⊢ ∃ (p : ℕ),
    (LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) ∧
        LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) (1 : ℝ)) ∧
      ∀ (m : ℕ),
        LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧
            LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) →
          p ≤ m
have hP : P.Nonempty
Tactic: have hP : P.Nonempty :=
    ⟨n, map_pos_of_ne_zero f (Nat.cast_ne_zero.mpr hn1), lt_of_le_of_ne (bdd n) hn2⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
Goal:
f : AbsoluteValue ℚ ℝ
p : ℕ
hp0 : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ)
hp1 : LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) (1 : ℝ)
hmin :
  ∀ (m : ℕ),
    LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) →
      p ≤ m
⊢ Irreducible p
have not_isUnit : ¬IsUnit p
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
Goal:
f : AbsoluteValue ℚ ℝ
p : ℕ
hp0 : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ)
hp1 : LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) (1 : ℝ)
hmin :
  ∀ (m : ℕ),
    LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) →
      p ≤ m
not_isUnit : ¬IsUnit p
⊢ Irreducible p
have isUnit_or_isUnit : ∀ ⦃a b : ℕ⦄, p = a * b → IsUnit a ∨ IsUnit b
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
Goal:
f : AbsoluteValue ℚ ℝ
p : ℕ
hp0 : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ)
hp1 : LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) (1 : ℝ)
hmin :
  ∀ (m : ℕ),
    LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) →
      p ≤ m
⊢ ¬IsUnit p
have not_isUnit : ¬p = 1
Tactic: rw [Nat.isUnit_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
Goal:
f : AbsoluteValue ℚ ℝ
a b : ℕ
hp0 : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑(a * b) : ℚ) : ℝ)
hp1 : LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑(a * b) : ℚ) : ℝ) (1 : ℝ)
hmin :
  ∀ (m : ℕ),
    LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) →
      a * b ≤ m
⊢ IsUnit a ∨ IsUnit b
have isUnit_or_isUnit : a = 1 ∨ b = 1
Tactic: rw [Nat.isUnit_iff, Nat.isUnit_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
Goal:
f : AbsoluteValue ℚ ℝ
a b : ℕ
hp0 : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑(a * b) : ℚ) : ℝ)
hp1 : LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑(a * b) : ℚ) : ℝ) (1 : ℝ)
hmin :
  ∀ (m : ℕ),
    LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) →
      a * b ≤ m
⊢ a = 1 ∨ b = 1
have isUnit_or_isUnit : ∀ (ha₁ : a ≠ 1) (hb₁ : b ≠ 1), False
Tactic: by_contra! ⟨ha₁, hb₁⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
Goal:
f : AbsoluteValue ℚ ℝ
a b : ℕ
hp0 : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑(a * b) : ℚ) : ℝ)
hp1 : LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑(a * b) : ℚ) : ℝ) (1 : ℝ)
hmin :
  ∀ (m : ℕ),
    LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) →
      a * b ≤ m
ha₁ : a ≠ 1
hb₁ : b ≠ 1
⊢ a ≠ 0 ∧ b ≠ 0
have refine : ∀ (h : a * b = 0), False
Tactic: refine mul_ne_zero_iff.mp fun h ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
Goal:
f : AbsoluteValue ℚ ℝ
a b : ℕ
hp0 : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑(a * b) : ℚ) : ℝ)
hp1 : LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑(a * b) : ℚ) : ℝ) (1 : ℝ)
hmin :
  ∀ (m : ℕ),
    LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) →
      a * b ≤ m
ha₁ : a ≠ 1
hb₁ : b ≠ 1
h : a * b = 0
⊢ False
have rwa : ∀ (hp0 : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑0 : ℚ) : ℝ))
  (hp1 : LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑(a * b) : ℚ) : ℝ) (1 : ℝ))
  (hmin :
    ∀ (m : ℕ),
      LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧
          LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) →
        a * b ≤ m)
  (ha₁ : a ≠ 1) (hb₁ : b ≠ 1) (h : a * b = 0), False
Tactic: rwa [h, Nat.cast_zero, map_zero, lt_self_iff_false] at hp0
Cleared hypotheses: hp0, hp1, hmin, ha₁, hb₁, h
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
Goal:
f : AbsoluteValue ℚ ℝ
a b : ℕ
hp0 : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑(a * b) : ℚ) : ℝ)
hp1 : LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑(a * b) : ℚ) : ℝ) (1 : ℝ)
hmin :
  ∀ (m : ℕ),
    LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) →
      a * b ≤ m
ha₁ : a ≠ 1
hb₁ : b ≠ 1
h : a * b = 0
rwa :
  ∀ (hp0 : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑0 : ℚ) : ℝ))
    (hp1 : LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑(a * b) : ℚ) : ℝ) (1 : ℝ))
    (hmin :
      ∀ (m : ℕ),
        LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧
            LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) →
          a * b ≤ m)
    (ha₁ : a ≠ 1) (hb₁ : b ≠ 1) (h : a * b = 0), False
⊢ False
have rwa₁ : ∀ (hp0 : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) 0 : ℝ))
  (hp1 : LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑(a * b) : ℚ) : ℝ) (1 : ℝ))
  (hmin :
    ∀ (m : ℕ),
      LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧
          LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) →
        a * b ≤ m)
  (ha₁ : a ≠ 1) (hb₁ : b ≠ 1) (h : a * b = 0), False
Tactic: rwa [h, Nat.cast_zero, map_zero, lt_self_iff_false] at hp0
Cleared hypotheses: hp0, hp1, hmin, ha₁, hb₁, h
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
Goal:
f : AbsoluteValue ℚ ℝ
a b : ℕ
hp0 : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑(a * b) : ℚ) : ℝ)
hp1 : LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑(a * b) : ℚ) : ℝ) (1 : ℝ)
hmin :
  ∀ (m : ℕ),
    LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) →
      a * b ≤ m
ha₁ : a ≠ 1
hb₁ : b ≠ 1
h : a * b = 0
rwa :
  ∀ (hp0 : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑0 : ℚ) : ℝ))
    (hp1 : LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑(a * b) : ℚ) : ℝ) (1 : ℝ))
    (hmin :
      ∀ (m : ℕ),
        LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧
            LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) →
          a * b ≤ m)
    (ha₁ : a ≠ 1) (hb₁ : b ≠ 1) (h : a * b = 0), False
rwa₁ :
  ∀ (hp0 : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) 0 : ℝ))
    (hp1 : LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑(a * b) : ℚ) : ℝ) (1 : ℝ))
    (hmin :
      ∀ (m : ℕ),
        LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧
            LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) →
          a * b ≤ m)
    (ha₁ : a ≠ 1) (hb₁ : b ≠ 1) (h : a * b = 0), False
⊢ False
have rwa₂ : ∀ (hp0 : LT.lt (α := ℝ) 0 0) (hp1 : LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑(a * b) : ℚ) : ℝ) (1 : ℝ))
  (hmin :
    ∀ (m : ℕ),
      LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧
          LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) →
        a * b ≤ m)
  (ha₁ : a ≠ 1) (hb₁ : b ≠ 1) (h : a * b = 0), False
Tactic: rwa [h, Nat.cast_zero, map_zero, lt_self_iff_false] at hp0
Cleared hypotheses: hp0, hp1, hmin, ha₁, hb₁, h
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
Goal:
f : AbsoluteValue ℚ ℝ
a b : ℕ
hp0 : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑(a * b) : ℚ) : ℝ)
hp1 : LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑(a * b) : ℚ) : ℝ) (1 : ℝ)
hmin :
  ∀ (m : ℕ),
    LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) →
      a * b ≤ m
ha₁ : a ≠ 1
hb₁ : b ≠ 1
h : a * b = 0
rwa :
  ∀ (hp0 : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑0 : ℚ) : ℝ))
    (hp1 : LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑(a * b) : ℚ) : ℝ) (1 : ℝ))
    (hmin :
      ∀ (m : ℕ),
        LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧
            LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) →
          a * b ≤ m)
    (ha₁ : a ≠ 1) (hb₁ : b ≠ 1) (h : a * b = 0), False
rwa₁ :
  ∀ (hp0 : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) 0 : ℝ))
    (hp1 : LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑(a * b) : ℚ) : ℝ) (1 : ℝ))
    (hmin :
      ∀ (m : ℕ),
        LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧
            LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) →
          a * b ≤ m)
    (ha₁ : a ≠ 1) (hb₁ : b ≠ 1) (h : a * b = 0), False
rwa₂ :
  ∀ (hp0 : LT.lt (α := ℝ) 0 0) (hp1 : LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑(a * b) : ℚ) : ℝ) (1 : ℝ))
    (hmin :
      ∀ (m : ℕ),
        LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧
            LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) →
          a * b ≤ m)
    (ha₁ : a ≠ 1) (hb₁ : b ≠ 1) (h : a * b = 0), False
⊢ False
have rwa₃ : ∀ (hp0 : False) (hp1 : LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑(a * b) : ℚ) : ℝ) (1 : ℝ))
  (hmin :
    ∀ (m : ℕ),
      LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧
          LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) →
        a * b ≤ m)
  (ha₁ : a ≠ 1) (hb₁ : b ≠ 1) (h : a * b = 0), False
Tactic: rwa [h, Nat.cast_zero, map_zero, lt_self_iff_false] at hp0
Cleared hypotheses: hp0, hp1, hmin, ha₁, hb₁, h