awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.AbsoluteValue.Equivalence (hypothesis)
Goal:
F : Type u_1
inst : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
a : F
ha₀ : a ≠ 0
ha₁ : Ne (α := ℝ) ((v : (a : F) → ℝ) a : ℝ) (1 : ℝ)
b : F
hb₀ : b ≠ 0
hb₁ : Ne (α := ℝ) ((v : (a : F) → ℝ) b : ℝ) (1 : ℝ)
h_ne : log ((v : (a : F) → ℝ) b) / log ((w : (a : F) → ℝ) b) ≠ log ((v : (a : F) → ℝ) a) / log ((w : (a : F) → ℝ) a)
ha : LT.lt (α := ℝ) (1 : ℝ) ((v : (a : F) → ℝ) a : ℝ)
hb : LT.lt (α := ℝ) (1 : ℝ) ((v : (a : F) → ℝ) b : ℝ)
h_lt : log ((v : (a : F) → ℝ) b) / log ((v : (a : F) → ℝ) a) < log ((w : (a : F) → ℝ) b) / log ((w : (a : F) → ℝ) a)
hwa : LT.lt (α := ℝ) (1 : ℝ) ((w : (a : F) → ℝ) a : ℝ)
hwb : LT.lt (α := ℝ) (1 : ℝ) ((w : (a : F) → ℝ) b : ℝ)
q : ℚ
hq₁ : log ((v : (a : F) → ℝ) b) / log ((v : (a : F) → ℝ) a) < HDiv.hDiv (α := ℝ) (↑q.num : ℝ) (↑q.den : ℝ)
hq₂ : HDiv.hDiv (α := ℝ) (↑q.num : ℝ) (↑q.den : ℝ) < log ((w : (a : F) → ℝ) b) / log ((w : (a : F) → ℝ) a)
⊢ False
have hq₃ : LT.lt (α := ℝ) ((v : (a : F) → ℝ) (b ^ q.den / a ^ q.num) : ℝ) (1 : ℝ)
Tactic: rw [div_lt_div_iff₀ (log_pos ha) (by simp [q.den_pos]), mul_comm, ← log_pow, ← log_zpow,
    log_lt_log_iff (pow_pos (by linarith) _) (zpow_pos (by linarith) _),
    ← div_lt_one (zpow_pos (by linarith) _), ← map_pow, ← map_zpow₀, ← map_div₀] at hq₁
Cleared hypotheses: hq₁, hq₂
-- Lean 4 proof step from Mathlib.Analysis.AbsoluteValue.Equivalence (goal)
Goal:
F : Type u_1
inst : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
a : F
ha₀ : a ≠ 0
ha₁ : Ne (α := ℝ) ((v : (a : F) → ℝ) a : ℝ) (1 : ℝ)
b : F
hb₀ : b ≠ 0
hb₁ : Ne (α := ℝ) ((v : (a : F) → ℝ) b : ℝ) (1 : ℝ)
h_ne : log ((v : (a : F) → ℝ) b) / log ((w : (a : F) → ℝ) b) ≠ log ((v : (a : F) → ℝ) a) / log ((w : (a : F) → ℝ) a)
ha : LT.lt (α := ℝ) (1 : ℝ) ((v : (a : F) → ℝ) a : ℝ)
hb : LT.lt (α := ℝ) (1 : ℝ) ((v : (a : F) → ℝ) b : ℝ)
h_lt : log ((v : (a : F) → ℝ) b) / log ((v : (a : F) → ℝ) a) < log ((w : (a : F) → ℝ) b) / log ((w : (a : F) → ℝ) a)
hwa : LT.lt (α := ℝ) (1 : ℝ) ((w : (a : F) → ℝ) a : ℝ)
hwb : LT.lt (α := ℝ) (1 : ℝ) ((w : (a : F) → ℝ) b : ℝ)
q : ℚ
hq₁ : LT.lt (α := ℝ) ((v : (a : F) → ℝ) (b ^ q.den / a ^ q.num) : ℝ) (1 : ℝ)
hq₂ :
  log (HPow.hPow (α := ℝ) ((w : (a : F) → ℝ) a : ℝ) q.num) < log (HPow.hPow (α := ℝ) ((w : (a : F) → ℝ) b : ℝ) q.den)
⊢ LT.lt (α := ℝ) (0 : ℝ) ((w : (a : F) → ℝ) a : ℝ)
have linarith : LE.le (α := ℝ) ((w : (a : F) → ℝ) a : ℝ) (0 : ℝ) →
  -1 + HSub.hSub (α := ℝ) (β := ℝ) (1 : ℝ) ((w : (a : F) → ℝ) a : ℝ) +
      HSub.hSub (α := ℝ) (β := ℝ) ((w : (a : F) → ℝ) a : ℝ) (0 : ℝ) =
    0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.AbsoluteValue.Equivalence (goal)
Goal:
F : Type u_1
inst : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
a : F
ha₀ : a ≠ 0
ha₁ : Ne (α := ℝ) ((v : (a : F) → ℝ) a : ℝ) (1 : ℝ)
b : F
hb₀ : b ≠ 0
hb₁ : Ne (α := ℝ) ((v : (a : F) → ℝ) b : ℝ) (1 : ℝ)
h_ne : log ((v : (a : F) → ℝ) b) / log ((w : (a : F) → ℝ) b) ≠ log ((v : (a : F) → ℝ) a) / log ((w : (a : F) → ℝ) a)
ha : LT.lt (α := ℝ) (1 : ℝ) ((v : (a : F) → ℝ) a : ℝ)
hb : LT.lt (α := ℝ) (1 : ℝ) ((v : (a : F) → ℝ) b : ℝ)
h_lt : log ((v : (a : F) → ℝ) b) / log ((v : (a : F) → ℝ) a) < log ((w : (a : F) → ℝ) b) / log ((w : (a : F) → ℝ) a)
hwa : LT.lt (α := ℝ) (1 : ℝ) ((w : (a : F) → ℝ) a : ℝ)
hwb : LT.lt (α := ℝ) (1 : ℝ) ((w : (a : F) → ℝ) b : ℝ)
q : ℚ
hq₁ : LT.lt (α := ℝ) ((v : (a : F) → ℝ) (b ^ q.den / a ^ q.num) : ℝ) (1 : ℝ)
hq₂ :
  log (HPow.hPow (α := ℝ) ((w : (a : F) → ℝ) a : ℝ) q.num) < log (HPow.hPow (α := ℝ) ((w : (a : F) → ℝ) b : ℝ) q.den)
⊢ LT.lt (α := ℝ) (0 : ℝ) ((w : (a : F) → ℝ) b : ℝ)
have linarith : LE.le (α := ℝ) ((w : (a : F) → ℝ) b : ℝ) (0 : ℝ) →
  -1 + HSub.hSub (α := ℝ) (β := ℝ) (1 : ℝ) ((w : (a : F) → ℝ) b : ℝ) +
      HSub.hSub (α := ℝ) (β := ℝ) ((w : (a : F) → ℝ) b : ℝ) (0 : ℝ) =
    0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.AbsoluteValue.Equivalence (goal)
Goal:
F : Type u_1
inst : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
a : F
ha₀ : a ≠ 0
ha₁ : Ne (α := ℝ) ((v : (a : F) → ℝ) a : ℝ) (1 : ℝ)
b : F
hb₀ : b ≠ 0
hb₁ : Ne (α := ℝ) ((v : (a : F) → ℝ) b : ℝ) (1 : ℝ)
h_ne : log ((v : (a : F) → ℝ) b) / log ((w : (a : F) → ℝ) b) ≠ log ((v : (a : F) → ℝ) a) / log ((w : (a : F) → ℝ) a)
ha : LT.lt (α := ℝ) (1 : ℝ) ((v : (a : F) → ℝ) a : ℝ)
hb : LT.lt (α := ℝ) (1 : ℝ) ((v : (a : F) → ℝ) b : ℝ)
h_lt : log ((v : (a : F) → ℝ) b) / log ((v : (a : F) → ℝ) a) < log ((w : (a : F) → ℝ) b) / log ((w : (a : F) → ℝ) a)
hwa : LT.lt (α := ℝ) (1 : ℝ) ((w : (a : F) → ℝ) a : ℝ)
hwb : LT.lt (α := ℝ) (1 : ℝ) ((w : (a : F) → ℝ) b : ℝ)
q : ℚ
hq₁ : LT.lt (α := ℝ) ((v : (a : F) → ℝ) (b ^ q.den / a ^ q.num) : ℝ) (1 : ℝ)
hq₂ : HPow.hPow (α := ℝ) ((w : (a : F) → ℝ) a : ℝ) q.num < HPow.hPow (α := ℝ) ((w : (a : F) → ℝ) b : ℝ) q.den
⊢ LT.lt (α := ℝ) (0 : ℝ) ((w : (a : F) → ℝ) a : ℝ)
have linarith : LE.le (α := ℝ) ((w : (a : F) → ℝ) a : ℝ) (0 : ℝ) →
  -1 + HSub.hSub (α := ℝ) (β := ℝ) (1 : ℝ) ((w : (a : F) → ℝ) a : ℝ) +
      HSub.hSub (α := ℝ) (β := ℝ) ((w : (a : F) → ℝ) a : ℝ) (0 : ℝ) =
    0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.AbsoluteValue.Equivalence (hypothesis)
Goal:
F : Type u_1
inst : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
a : F
ha₀ : a ≠ 0
ha₁ : Ne (α := ℝ) ((v : (a : F) → ℝ) a : ℝ) (1 : ℝ)
b : F
hb₀ : b ≠ 0
hb₁ : Ne (α := ℝ) ((v : (a : F) → ℝ) b : ℝ) (1 : ℝ)
h_ne : log ((v : (a : F) → ℝ) b) / log ((w : (a : F) → ℝ) b) ≠ log ((v : (a : F) → ℝ) a) / log ((w : (a : F) → ℝ) a)
ha : LT.lt (α := ℝ) (1 : ℝ) ((v : (a : F) → ℝ) a : ℝ)
hb : LT.lt (α := ℝ) (1 : ℝ) ((v : (a : F) → ℝ) b : ℝ)
h_lt : log ((v : (a : F) → ℝ) b) / log ((v : (a : F) → ℝ) a) < log ((w : (a : F) → ℝ) b) / log ((w : (a : F) → ℝ) a)
hwa : LT.lt (α := ℝ) (1 : ℝ) ((w : (a : F) → ℝ) a : ℝ)
hwb : LT.lt (α := ℝ) (1 : ℝ) ((w : (a : F) → ℝ) b : ℝ)
q : ℚ
hq₁ : LT.lt (α := ℝ) ((v : (a : F) → ℝ) (b ^ q.den / a ^ q.num) : ℝ) (1 : ℝ)
hq₂ : HDiv.hDiv (α := ℝ) (↑q.num : ℝ) (↑q.den : ℝ) < log ((w : (a : F) → ℝ) b) / log ((w : (a : F) → ℝ) a)
⊢ False
have hq₃ : LT.lt (α := ℝ) (1 : ℝ) ((w : (a : F) → ℝ) (b ^ q.den / a ^ q.num) : ℝ)
Tactic: rw [div_lt_div_iff₀ (by simp [q.den_pos]) (log_pos hwa), mul_comm (w _).log,
    ← log_pow, ← log_zpow, log_lt_log_iff (zpow_pos (by linarith) _) (pow_pos (by linarith) _),
    ← one_lt_div (zpow_pos (by linarith) _), ← map_pow, ← map_zpow₀, ← map_div₀] at hq₂
Cleared hypotheses: hq₂
-- Lean 4 proof step from Mathlib.Analysis.AbsoluteValue.Equivalence (goal)
Goal:
F : Type u_1
inst : Field F
v w : AbsoluteValue F ℝ
⊢ v.IsEquiv w ↔
    ∃ (c : ℝ), 0 < c ∧ Eq (α := F → ℝ) (fun (x : F) ↦ HPow.hPow (α := ℝ) ((v : (a : F) → ℝ) x : ℝ) c) (⇑w : (a : F) → ℝ)
have refine : ∀ (h : v.IsEquiv w),
  ∃ (c : ℝ), 0 < c ∧ Eq (α := F → ℝ) (fun (x : F) ↦ HPow.hPow (α := ℝ) ((v : (a : F) → ℝ) x : ℝ) c) (⇑w : (a : F) → ℝ)
Tactic: refine ⟨fun h ↦ ?_, fun ⟨t, ht, h⟩ ↦ isEquiv_iff_lt_one_iff.2
    fun x ↦ h ▸ (rpow_lt_one_iff' (v.nonneg x) ht).symm⟩
-- Lean 4 proof step from Mathlib.Analysis.AbsoluteValue.Equivalence (goal)
Goal:
F : Type u_1
inst : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
⊢ ∃ (c : ℝ), 0 < c ∧ Eq (α := F → ℝ) (fun (x : F) ↦ HPow.hPow (α := ℝ) ((v : (a : F) → ℝ) x : ℝ) c) (⇑w : (a : F) → ℝ)
have pos : ∀ (hw : w.IsNontrivial),
  ∃ (c : ℝ), 0 < c ∧ Eq (α := F → ℝ) (fun (x : F) ↦ HPow.hPow (α := ℝ) ((v : (a : F) → ℝ) x : ℝ) c) (⇑w : (a : F) → ℝ)
Tactic: by_cases hw : w.IsNontrivial
-- Lean 4 proof step from Mathlib.Analysis.AbsoluteValue.Equivalence (goal)
Goal:
F : Type u_1
inst : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
pos :
  ∀ (hw : w.IsNontrivial),
    ∃ (c : ℝ), 0 < c ∧ Eq (α := F → ℝ) (fun (x : F) ↦ HPow.hPow (α := ℝ) ((v : (a : F) → ℝ) x : ℝ) c) (⇑w : (a : F) → ℝ)
⊢ ∃ (c : ℝ), 0 < c ∧ Eq (α := F → ℝ) (fun (x : F) ↦ HPow.hPow (α := ℝ) ((v : (a : F) → ℝ) x : ℝ) c) (⇑w : (a : F) → ℝ)
have neg : ∀ (hw : ¬w.IsNontrivial),
  ∃ (c : ℝ), 0 < c ∧ Eq (α := F → ℝ) (fun (x : F) ↦ HPow.hPow (α := ℝ) ((v : (a : F) → ℝ) x : ℝ) c) (⇑w : (a : F) → ℝ)
Tactic: by_cases hw : w.IsNontrivial
-- Lean 4 proof step from Mathlib.Analysis.AbsoluteValue.Equivalence (goal)
Goal:
F : Type u_1
inst : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
hw : w.IsNontrivial
⊢ ∃ (c : ℝ), 0 < c ∧ Eq (α := F → ℝ) (fun (x : F) ↦ HPow.hPow (α := ℝ) ((v : (a : F) → ℝ) x : ℝ) c) (⇑w : (a : F) → ℝ)
have pos : ∀ (a : F) (ha₀ : a ≠ 0) (ha₁ : Ne (α := ℝ) ((w : (a : F) → ℝ) a : ℝ) (1 : ℝ)),
  ∃ (c : ℝ), 0 < c ∧ Eq (α := F → ℝ) (fun (x : F) ↦ HPow.hPow (α := ℝ) ((v : (a : F) → ℝ) x : ℝ) c) (⇑w : (a : F) → ℝ)
Tactic: let ⟨a, ha₀, ha₁⟩ := hw
-- Lean 4 proof step from Mathlib.Analysis.AbsoluteValue.Equivalence (goal)
Goal:
F : Type u_1
inst : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
hw : w.IsNontrivial
a : F
ha₀ : a ≠ 0
ha₁ : Ne (α := ℝ) ((w : (a : F) → ℝ) a : ℝ) (1 : ℝ)
⊢ ∃ (c : ℝ), 0 < c ∧ Eq (α := F → ℝ) (fun (x : F) ↦ HPow.hPow (α := ℝ) ((v : (a : F) → ℝ) x : ℝ) c) (⇑w : (a : F) → ℝ)
have pos : ∀ (b : F),
  HPow.hPow (α := ℝ) ((v : (a : F) → ℝ) b : ℝ) (log ((w : (a : F) → ℝ) a) / log ((v : (a : F) → ℝ) a)) =
    (w : (a : F) → ℝ) b
Tactic: refine ⟨(w a).log / (v a).log, h.log_div_log_pos ha₀ ha₁, funext fun b ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.AbsoluteValue.Equivalence (goal)
Goal:
F : Type u_1
inst : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
hw : w.IsNontrivial
a : F
ha₀ : a ≠ 0
ha₁ : Ne (α := ℝ) ((w : (a : F) → ℝ) a : ℝ) (1 : ℝ)
b : F
⊢ HPow.hPow (α := ℝ) ((v : (a : F) → ℝ) b : ℝ) (log ((w : (a : F) → ℝ) a) / log ((v : (a : F) → ℝ) a)) =
    (w : (a : F) → ℝ) b
have pos : HPow.hPow (α := ℝ) ((v : (a : F) → ℝ) 0 : ℝ) (log ((w : (a : F) → ℝ) a) / log ((v : (a : F) → ℝ) a)) =
  (w : (a : F) → ℝ) 0
Tactic: rcases eq_or_ne b 0 with rfl | hb₀
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Analysis.AbsoluteValue.Equivalence (goal)
Goal:
F : Type u_1
inst : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
hw : w.IsNontrivial
a : F
ha₀ : a ≠ 0
ha₁ : Ne (α := ℝ) ((w : (a : F) → ℝ) a : ℝ) (1 : ℝ)
b : F
pos :
  HPow.hPow (α := ℝ) ((v : (a : F) → ℝ) 0 : ℝ) (log ((w : (a : F) → ℝ) a) / log ((v : (a : F) → ℝ) a)) =
    (w : (a : F) → ℝ) 0
⊢ HPow.hPow (α := ℝ) ((v : (a : F) → ℝ) b : ℝ) (log ((w : (a : F) → ℝ) a) / log ((v : (a : F) → ℝ) a)) =
    (w : (a : F) → ℝ) b
have pos₁ : ∀ (hb₀ : b ≠ 0),
  HPow.hPow (α := ℝ) ((v : (a : F) → ℝ) b : ℝ) (log ((w : (a : F) → ℝ) a) / log ((v : (a : F) → ℝ) a)) =
    (w : (a : F) → ℝ) b
Tactic: rcases eq_or_ne b 0 with rfl | hb₀
-- Lean 4 proof step from Mathlib.Analysis.AbsoluteValue.Equivalence (goal)
Goal:
F : Type u_1
inst : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
hw : w.IsNontrivial
a : F
ha₀ : a ≠ 0
ha₁ : Ne (α := ℝ) ((w : (a : F) → ℝ) a : ℝ) (1 : ℝ)
⊢ log ((w : (a : F) → ℝ) a) / log ((v : (a : F) → ℝ) a) ≠ 0
have linarith : log ((w : (a : F) → ℝ) a) / log ((v : (a : F) → ℝ) a) = 0 →
  log ((w : (a : F) → ℝ) a) / log ((v : (a : F) → ℝ) a) - 0 +
      (HMul.hMul (α := ℝ) 1 0 - 1 * (log ((w : (a : F) → ℝ) a) / log ((v : (a : F) → ℝ) a))) =
    0
Tactic: linarith [h.log_div_log_pos ha₀ ha₁]
-- Lean 4 proof step from Mathlib.Analysis.AbsoluteValue.Equivalence (goal)
Goal:
F : Type u_1
inst : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
hw : w.IsNontrivial
a : F
ha₀ : a ≠ 0
ha₁ : Ne (α := ℝ) ((w : (a : F) → ℝ) a : ℝ) (1 : ℝ)
b : F
hb₀ : b ≠ 0
⊢ HPow.hPow (α := ℝ) ((v : (a : F) → ℝ) b : ℝ) (log ((w : (a : F) → ℝ) a) / log ((v : (a : F) → ℝ) a)) =
    (w : (a : F) → ℝ) b
have pos : ∀ (hb₁ : Eq (α := ℝ) ((w : (a : F) → ℝ) b : ℝ) (1 : ℝ)),
  HPow.hPow (α := ℝ) ((v : (a : F) → ℝ) b : ℝ) (log ((w : (a : F) → ℝ) a) / log ((v : (a : F) → ℝ) a)) =
    (w : (a : F) → ℝ) b
Tactic: rcases eq_or_ne (w b) 1 with hb₁ | hb₁
-- Lean 4 proof step from Mathlib.Analysis.AbsoluteValue.Equivalence (goal)
Goal:
F : Type u_1
inst : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
hw : w.IsNontrivial
a : F
ha₀ : a ≠ 0
ha₁ : Ne (α := ℝ) ((w : (a : F) → ℝ) a : ℝ) (1 : ℝ)
b : F
hb₀ : b ≠ 0
pos :
  ∀ (hb₁ : Eq (α := ℝ) ((w : (a : F) → ℝ) b : ℝ) (1 : ℝ)),
    HPow.hPow (α := ℝ) ((v : (a : F) → ℝ) b : ℝ) (log ((w : (a : F) → ℝ) a) / log ((v : (a : F) → ℝ) a)) =
      (w : (a : F) → ℝ) b
⊢ HPow.hPow (α := ℝ) ((v : (a : F) → ℝ) b : ℝ) (log ((w : (a : F) → ℝ) a) / log ((v : (a : F) → ℝ) a)) =
    (w : (a : F) → ℝ) b
have pos₁ : ∀ (hb₁ : Ne (α := ℝ) ((w : (a : F) → ℝ) b : ℝ) (1 : ℝ)),
  HPow.hPow (α := ℝ) ((v : (a : F) → ℝ) b : ℝ) (log ((w : (a : F) → ℝ) a) / log ((v : (a : F) → ℝ) a)) =
    (w : (a : F) → ℝ) b
Tactic: rcases eq_or_ne (w b) 1 with hb₁ | hb₁
-- Lean 4 proof step from Mathlib.Analysis.AbsoluteValue.Equivalence (goal)
Goal:
F : Type u_1
inst : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
hw : w.IsNontrivial
a : F
ha₀ : a ≠ 0
ha₁ : Ne (α := ℝ) ((w : (a : F) → ℝ) a : ℝ) (1 : ℝ)
b : F
hb₀ : b ≠ 0
hb₁ : Ne (α := ℝ) ((w : (a : F) → ℝ) b : ℝ) (1 : ℝ)
⊢ HPow.hPow (α := ℝ) ((v : (a : F) → ℝ) b : ℝ) (log ((w : (a : F) → ℝ) a) / log ((v : (a : F) → ℝ) a)) =
    (w : (a : F) → ℝ) b
have pos : HPow.hPow (α := ℝ) ((v : (a : F) → ℝ) b : ℝ) (log ((w : (a : F) → ℝ) b) / log ((v : (a : F) → ℝ) b)) =
  (w : (a : F) → ℝ) b
Tactic: rw [← h.symm.log_div_log_eq_log_div_log ha₀ ha₁ hb₀ hb₁, div_eq_inv_mul, rpow_mul (v.nonneg _),
      rpow_inv_log (v.pos hb₀) (h.eq_one_iff.not.2 hb₁), exp_one_rpow, exp_log (w.pos hb₀)]
-- Lean 4 proof step from Mathlib.Analysis.AbsoluteValue.Equivalence (goal)
Goal:
F : Type u_1
inst : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
hw : w.IsNontrivial
a : F
ha₀ : a ≠ 0
ha₁ : Ne (α := ℝ) ((w : (a : F) → ℝ) a : ℝ) (1 : ℝ)
b : F
hb₀ : b ≠ 0
hb₁ : Ne (α := ℝ) ((w : (a : F) → ℝ) b : ℝ) (1 : ℝ)
pos :
  HPow.hPow (α := ℝ) ((v : (a : F) → ℝ) b : ℝ) (log ((w : (a : F) → ℝ) b) / log ((v : (a : F) → ℝ) b)) =
    (w : (a : F) → ℝ) b
⊢ HPow.hPow (α := ℝ) ((v : (a : F) → ℝ) b : ℝ) (log ((w : (a : F) → ℝ) a) / log ((v : (a : F) → ℝ) a)) =
    (w : (a : F) → ℝ) b
have pos₁ : HPow.hPow (α := ℝ) ((v : (a : F) → ℝ) b : ℝ) ((log ((v : (a : F) → ℝ) b))⁻¹ * log ((w : (a : F) → ℝ) b)) =
  (w : (a : F) → ℝ) b
Tactic: rw [← h.symm.log_div_log_eq_log_div_log ha₀ ha₁ hb₀ hb₁, div_eq_inv_mul, rpow_mul (v.nonneg _),
      rpow_inv_log (v.pos hb₀) (h.eq_one_iff.not.2 hb₁), exp_one_rpow, exp_log (w.pos hb₀)]
-- Lean 4 proof step from Mathlib.Analysis.AbsoluteValue.Equivalence (goal)
Goal:
F : Type u_1
inst : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
hw : w.IsNontrivial
a : F
ha₀ : a ≠ 0
ha₁ : Ne (α := ℝ) ((w : (a : F) → ℝ) a : ℝ) (1 : ℝ)
b : F
hb₀ : b ≠ 0
hb₁ : Ne (α := ℝ) ((w : (a : F) → ℝ) b : ℝ) (1 : ℝ)
pos :
  HPow.hPow (α := ℝ) ((v : (a : F) → ℝ) b : ℝ) (log ((w : (a : F) → ℝ) b) / log ((v : (a : F) → ℝ) b)) =
    (w : (a : F) → ℝ) b
pos₁ :
  HPow.hPow (α := ℝ) ((v : (a : F) → ℝ) b : ℝ) ((log ((v : (a : F) → ℝ) b))⁻¹ * log ((w : (a : F) → ℝ) b)) =
    (w : (a : F) → ℝ) b
⊢ HPow.hPow (α := ℝ) ((v : (a : F) → ℝ) b : ℝ) (log ((w : (a : F) → ℝ) a) / log ((v : (a : F) → ℝ) a)) =
    (w : (a : F) → ℝ) b
have pos₂ : HPow.hPow (α := ℝ) ((v : (a : F) → ℝ) b : ℝ) (log ((v : (a : F) → ℝ) b))⁻¹ ^ log ((w : (a : F) → ℝ) b) =
  (w : (a : F) → ℝ) b
Tactic: rw [← h.symm.log_div_log_eq_log_div_log ha₀ ha₁ hb₀ hb₁, div_eq_inv_mul, rpow_mul (v.nonneg _),
      rpow_inv_log (v.pos hb₀) (h.eq_one_iff.not.2 hb₁), exp_one_rpow, exp_log (w.pos hb₀)]
-- Lean 4 proof step from Mathlib.Analysis.AbsoluteValue.Equivalence (goal)
Goal:
F : Type u_1
inst : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
hw : w.IsNontrivial
a : F
ha₀ : a ≠ 0
ha₁ : Ne (α := ℝ) ((w : (a : F) → ℝ) a : ℝ) (1 : ℝ)
b : F
hb₀ : b ≠ 0
hb₁ : Ne (α := ℝ) ((w : (a : F) → ℝ) b : ℝ) (1 : ℝ)
pos :
  HPow.hPow (α := ℝ) ((v : (a : F) → ℝ) b : ℝ) (log ((w : (a : F) → ℝ) b) / log ((v : (a : F) → ℝ) b)) =
    (w : (a : F) → ℝ) b
pos₁ :
  HPow.hPow (α := ℝ) ((v : (a : F) → ℝ) b : ℝ) ((log ((v : (a : F) → ℝ) b))⁻¹ * log ((w : (a : F) → ℝ) b)) =
    (w : (a : F) → ℝ) b
pos₂ :
  HPow.hPow (α := ℝ) ((v : (a : F) → ℝ) b : ℝ) (log ((v : (a : F) → ℝ) b))⁻¹ ^ log ((w : (a : F) → ℝ) b) =
    (w : (a : F) → ℝ) b
⊢ HPow.hPow (α := ℝ) ((v : (a : F) → ℝ) b : ℝ) (log ((w : (a : F) → ℝ) a) / log ((v : (a : F) → ℝ) a)) =
    (w : (a : F) → ℝ) b
have pos₃ : rexp 1 ^ log ((w : (a : F) → ℝ) b) = (w : (a : F) → ℝ) b
Tactic: rw [← h.symm.log_div_log_eq_log_div_log ha₀ ha₁ hb₀ hb₁, div_eq_inv_mul, rpow_mul (v.nonneg _),
      rpow_inv_log (v.pos hb₀) (h.eq_one_iff.not.2 hb₁), exp_one_rpow, exp_log (w.pos hb₀)]
-- Lean 4 proof step from Mathlib.Analysis.AbsoluteValue.Equivalence (goal)
Goal:
F : Type u_1
inst : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
hw : w.IsNontrivial
a : F
ha₀ : a ≠ 0
ha₁ : Ne (α := ℝ) ((w : (a : F) → ℝ) a : ℝ) (1 : ℝ)
b : F
hb₀ : b ≠ 0
hb₁ : Ne (α := ℝ) ((w : (a : F) → ℝ) b : ℝ) (1 : ℝ)
pos :
  HPow.hPow (α := ℝ) ((v : (a : F) → ℝ) b : ℝ) (log ((w : (a : F) → ℝ) b) / log ((v : (a : F) → ℝ) b)) =
    (w : (a : F) → ℝ) b
pos₁ :
  HPow.hPow (α := ℝ) ((v : (a : F) → ℝ) b : ℝ) ((log ((v : (a : F) → ℝ) b))⁻¹ * log ((w : (a : F) → ℝ) b)) =
    (w : (a : F) → ℝ) b
pos₂ :
  HPow.hPow (α := ℝ) ((v : (a : F) → ℝ) b : ℝ) (log ((v : (a : F) → ℝ) b))⁻¹ ^ log ((w : (a : F) → ℝ) b) =
    (w : (a : F) → ℝ) b
pos₃ : rexp 1 ^ log ((w : (a : F) → ℝ) b) = (w : (a : F) → ℝ) b
⊢ HPow.hPow (α := ℝ) ((v : (a : F) → ℝ) b : ℝ) (log ((w : (a : F) → ℝ) a) / log ((v : (a : F) → ℝ) a)) =
    (w : (a : F) → ℝ) b
have pos₄ : rexp (log ((w : (a : F) → ℝ) b)) = (w : (a : F) → ℝ) b
Tactic: rw [← h.symm.log_div_log_eq_log_div_log ha₀ ha₁ hb₀ hb₁, div_eq_inv_mul, rpow_mul (v.nonneg _),
      rpow_inv_log (v.pos hb₀) (h.eq_one_iff.not.2 hb₁), exp_one_rpow, exp_log (w.pos hb₀)]
-- Lean 4 proof step from Mathlib.Analysis.AbsoluteValue.Equivalence (goal)
Goal:
F : Type u_1
inst : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
hw : w.IsNontrivial
a : F
ha₀ : a ≠ 0
ha₁ : Ne (α := ℝ) ((w : (a : F) → ℝ) a : ℝ) (1 : ℝ)
b : F
hb₀ : b ≠ 0
hb₁ : Ne (α := ℝ) ((w : (a : F) → ℝ) b : ℝ) (1 : ℝ)
pos :
  HPow.hPow (α := ℝ) ((v : (a : F) → ℝ) b : ℝ) (log ((w : (a : F) → ℝ) b) / log ((v : (a : F) → ℝ) b)) =
    (w : (a : F) → ℝ) b
pos₁ :
  HPow.hPow (α := ℝ) ((v : (a : F) → ℝ) b : ℝ) ((log ((v : (a : F) → ℝ) b))⁻¹ * log ((w : (a : F) → ℝ) b)) =
    (w : (a : F) → ℝ) b
pos₂ :
  HPow.hPow (α := ℝ) ((v : (a : F) → ℝ) b : ℝ) (log ((v : (a : F) → ℝ) b))⁻¹ ^ log ((w : (a : F) → ℝ) b) =
    (w : (a : F) → ℝ) b
pos₃ : rexp 1 ^ log ((w : (a : F) → ℝ) b) = (w : (a : F) → ℝ) b
pos₄ : rexp (log ((w : (a : F) → ℝ) b)) = (w : (a : F) → ℝ) b
⊢ HPow.hPow (α := ℝ) ((v : (a : F) → ℝ) b : ℝ) (log ((w : (a : F) → ℝ) a) / log ((v : (a : F) → ℝ) a)) =
    (w : (a : F) → ℝ) b
have pos₅ : Eq (α := ℝ) ((w : (a : F) → ℝ) b : ℝ) ((w : (a : F) → ℝ) b : ℝ)
Tactic: rw [← h.symm.log_div_log_eq_log_div_log ha₀ ha₁ hb₀ hb₁, div_eq_inv_mul, rpow_mul (v.nonneg _),
      rpow_inv_log (v.pos hb₀) (h.eq_one_iff.not.2 hb₁), exp_one_rpow, exp_log (w.pos hb₀)]
-- Lean 4 proof step from Mathlib.Analysis.AbsoluteValue.Equivalence (goal)
Goal:
F : Type u_1
inst : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
hw : ¬w.IsNontrivial
x : F
⊢ HPow.hPow (α := ℝ) (β := ℝ) ((v : (a : F) → ℝ) x : ℝ) 1 = (w : (a : F) → ℝ) x
have inl : HPow.hPow (α := ℝ) (β := ℝ) ((v : (a : F) → ℝ) 0 : ℝ) 1 = (w : (a : F) → ℝ) 0
Tactic: rcases eq_or_ne x 0 with rfl | h₀
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Analysis.AbsoluteValue.Equivalence (goal)
Goal:
F : Type u_1
inst : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
hw : ¬w.IsNontrivial
x : F
inl : HPow.hPow (α := ℝ) (β := ℝ) ((v : (a : F) → ℝ) 0 : ℝ) 1 = (w : (a : F) → ℝ) 0
⊢ HPow.hPow (α := ℝ) (β := ℝ) ((v : (a : F) → ℝ) x : ℝ) 1 = (w : (a : F) → ℝ) x
have inr : ∀ (h₀ : x ≠ 0), HPow.hPow (α := ℝ) (β := ℝ) ((v : (a : F) → ℝ) x : ℝ) 1 = (w : (a : F) → ℝ) x
Tactic: rcases eq_or_ne x 0 with rfl | h₀
-- Lean 4 proof step from Mathlib.Analysis.AbsoluteValue.Equivalence (goal)
Goal:
F : Type u_1
inst : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
U : Set (WithAbs v)
hU : Membership.mem (γ := Filter (WithAbs v)) (𝓝 0) U
⊢ Membership.mem (γ := Filter (WithAbs w)) (𝓝 0)
    ((⇑(WithAbs.congr v w (RingEquiv.refl F)) : (a : WithAbs v) → WithAbs w) '' U)
have rw : ∀ (hU : ∃ ε > 0, Metric.ball 0 ε ⊆ U),
  ∃ ε > 0,
    Subset (α := Set (WithAbs w)) (Metric.ball 0 ε)
      ((⇑(WithAbs.congr v w (RingEquiv.refl F)) : (a : WithAbs v) → WithAbs w) '' U)
Tactic: rw [Metric.mem_nhds_iff] at hU ⊢
Cleared hypotheses: hU
-- Lean 4 proof step from Mathlib.Analysis.AbsoluteValue.Equivalence (goal)
Goal:
F : Type u_1
inst : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
U : Set (WithAbs v)
hU : ∃ ε > 0, Metric.ball 0 ε ⊆ U
⊢ ∃ ε > 0,
    Subset (α := Set (WithAbs w)) (Metric.ball 0 ε)
      ((⇑(WithAbs.congr v w (RingEquiv.refl F)) : (a : WithAbs v) → WithAbs w) '' U)
have obtain : ∀ (ε : ℝ) (hε : ε > 0) (hU : Metric.ball 0 ε ⊆ U),
  ∃ ε > 0,
    Subset (α := Set (WithAbs w)) (Metric.ball 0 ε)
      ((⇑(WithAbs.congr v w (RingEquiv.refl F)) : (a : WithAbs v) → WithAbs w) '' U)
Tactic: obtain ⟨ε, hε, hU⟩ := hU
Cleared hypotheses: hU
-- Lean 4 proof step from Mathlib.Analysis.AbsoluteValue.Equivalence (goal)
Goal:
F : Type u_1
inst : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
U : Set (WithAbs v)
ε : ℝ
hε : ε > 0
hU : Metric.ball 0 ε ⊆ U
⊢ ∃ ε > 0,
    Subset (α := Set (WithAbs w)) (Metric.ball 0 ε)
      ((⇑(WithAbs.congr v w (RingEquiv.refl F)) : (a : WithAbs v) → WithAbs w) '' U)
have obtain : ∀ (c : ℝ) (hc : 0 < c)
  (hvw : Eq (α := F → ℝ) (fun (x : F) ↦ HPow.hPow (α := ℝ) ((v : (a : F) → ℝ) x : ℝ) c) (⇑w : (a : F) → ℝ)),
  ∃ ε > 0,
    Subset (α := Set (WithAbs w)) (Metric.ball 0 ε)
      ((⇑(WithAbs.congr v w (RingEquiv.refl F)) : (a : WithAbs v) → WithAbs w) '' U)
Tactic: obtain ⟨c, hc, hvw⟩ := isEquiv_iff_exists_rpow_eq.1 h
-- Lean 4 proof step from Mathlib.Analysis.AbsoluteValue.Equivalence (goal)
Goal:
F : Type u_1
inst : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
U : Set (WithAbs v)
ε : ℝ
hε : ε > 0
hU : Metric.ball 0 ε ⊆ U
c : ℝ
hc : 0 < c
hvw : Eq (α := F → ℝ) (fun (x : F) ↦ HPow.hPow (α := ℝ) ((v : (a : F) → ℝ) x : ℝ) c) (⇑w : (a : F) → ℝ)
⊢ ∃ ε > 0,
    Subset (α := Set (WithAbs w)) (Metric.ball 0 ε)
      ((⇑(WithAbs.congr v w (RingEquiv.refl F)) : (a : WithAbs v) → WithAbs w) '' U)
have refine : ∀ (x : WithAbs w) (hx : Membership.mem (γ := Set (WithAbs w)) (Metric.ball 0 (ε ^ c)) x),
  Membership.mem (γ := Set (WithAbs w)) ((⇑(WithAbs.congr v w (RingEquiv.refl F)) : (a : WithAbs v) → WithAbs w) '' U) x
Tactic: refine ⟨ε ^ c, rpow_pos_of_pos hε _, fun x hx ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.AbsoluteValue.Equivalence (goal)
Goal:
F : Type u_1
inst : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
U : Set (WithAbs v)
ε : ℝ
hε : ε > 0
hU : Metric.ball 0 ε ⊆ U
c : ℝ
hc : 0 < c
hvw : Eq (α := F → ℝ) (fun (x : F) ↦ HPow.hPow (α := ℝ) ((v : (a : F) → ℝ) x : ℝ) c) (⇑w : (a : F) → ℝ)
x : WithAbs w
hx : Membership.mem (γ := Set (WithAbs w)) (Metric.ball 0 (ε ^ c)) x
⊢ Membership.mem (γ := Set (WithAbs w)) ((⇑(WithAbs.congr v w (RingEquiv.refl F)) : (a : WithAbs v) → WithAbs w) '' U) x
have rw : Membership.mem (α := WithAbs w) (γ := Set (WithAbs w))
  ((⇑(WithAbs.congr v w (RingEquiv.refl F)) : (a : WithAbs v) → WithAbs w) '' U)
  ((WithAbs.congr v w (RingEquiv.refl F) : (a : WithAbs v) → WithAbs w)
      (((WithAbs.congr v w (RingEquiv.refl F)).symm : (a : WithAbs w) → WithAbs v) x) :
    WithAbs w)
Tactic: rw [← RingEquiv.apply_symm_apply (WithAbs.congr v w (.refl F)) x]
-- Lean 4 proof step from Mathlib.Analysis.AbsoluteValue.Equivalence (goal)
Goal:
F : Type u_1
inst : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
U : Set (WithAbs v)
ε : ℝ
hε : ε > 0
hU : Metric.ball 0 ε ⊆ U
c : ℝ
hc : 0 < c
hvw : Eq (α := F → ℝ) (fun (x : F) ↦ HPow.hPow (α := ℝ) ((v : (a : F) → ℝ) x : ℝ) c) (⇑w : (a : F) → ℝ)
x : WithAbs w
hx : Membership.mem (γ := Set (WithAbs w)) (Metric.ball 0 (ε ^ c)) x
⊢ Membership.mem (α := WithAbs w) (γ := Set (WithAbs w))
    ((⇑(WithAbs.congr v w (RingEquiv.refl F)) : (a : WithAbs v) → WithAbs w) '' U)
    ((WithAbs.congr v w (RingEquiv.refl F) : (a : WithAbs v) → WithAbs w)
        (((WithAbs.congr v w (RingEquiv.refl F)).symm : (a : WithAbs w) → WithAbs v) x) :
      WithAbs w)
have refine : Membership.mem (α := WithAbs v) (γ := Set (WithAbs v)) (Metric.ball 0 ε)
  (((WithAbs.congr v w (RingEquiv.refl F)).symm : (a : WithAbs w) → WithAbs v) x : WithAbs v)
Tactic: refine Set.mem_image_of_mem _ (hU ?_)