awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
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 ((w : (a : F) → ℝ) b) < log ((v : (a : F) → ℝ) a) / log ((w : (a : F) → ℝ) a)
hwa : LT.lt (α := ℝ) (1 : ℝ) ((w : (a : F) → ℝ) a : ℝ)
hwb : LT.lt (α := ℝ) (1 : ℝ) ((w : (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 : ℝ)
⊢ LT.lt (α := ℝ) (1 : ℝ) ((w : (a : F) → ℝ) b : ℝ)

Tactic:
rw [div_lt_div_iff₀ (log_pos hwb) (log_pos hwa), mul_comm (v a).log,
    ← div_lt_div_iff₀ (log_pos ha) (log_pos hwa)] at h_lt

Premises used: Real.log_pos, Real.log, mul_comm, div_lt_div_iff₀, DFunLike.coe
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
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 : ℝ)
let :
  ∀ (q : ℚ) (hq₁ : log ((v : (a : F) → ℝ) b) / log ((v : (a : F) → ℝ) a) < (↑q : ℝ))
    (hq₂ : (↑q : ℝ) < log ((w : (a : F) → ℝ) b) / log ((w : (a : F) → ℝ) a)), False
⊢ False

Tactic:
let ⟨q, ⟨hq₁, hq₂⟩⟩ := exists_rat_btwn h_lt
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
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) < (↑q : ℝ)
hq₂ : (↑q : ℝ) < log ((w : (a : F) → ℝ) b) / log ((w : (a : F) → ℝ) a)
⊢ log ((v : (a : F) → ℝ) b) / log ((v : (a : F) → ℝ) a) < HDiv.hDiv (α := ℝ) (↑q.num : ℝ) (↑q.den : ℝ)

Tactic:
rw [← Rat.num_div_den q, Rat.cast_div, Rat.cast_intCast, Rat.cast_natCast] at hq₁ hq₂

Premises used: Rat.num_div_den, Rat.cast_intCast, Rat.cast_div, Rat.cast_natCast
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
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) < (↑q : ℝ)
hq₂ : (↑q : ℝ) < log ((w : (a : F) → ℝ) b) / log ((w : (a : F) → ℝ) a)
hq₃ : log ((v : (a : F) → ℝ) b) / log ((v : (a : F) → ℝ) a) < HDiv.hDiv (α := ℝ) (↑q.num : ℝ) (↑q.den : ℝ)
⊢ HDiv.hDiv (α := ℝ) (↑q.num : ℝ) (↑q.den : ℝ) < log ((w : (a : F) → ℝ) b) / log ((w : (a : F) → ℝ) a)

Tactic:
rw [← Rat.num_div_den q, Rat.cast_div, Rat.cast_intCast, Rat.cast_natCast] at hq₁ hq₂

Premises used: Rat.num_div_den, Rat.cast_intCast, Rat.cast_div, Rat.cast_natCast
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
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)
⊢ LT.lt (α := ℝ) 0 (↑q.den : ℝ)

Tactic:
simp [q.den_pos]

Premises used: Rat.den_pos
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
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 (HPow.hPow (α := ℝ) ((v : (a : F) → ℝ) b : ℝ) q.den) < log (HPow.hPow (α := ℝ) ((v : (a : F) → ℝ) a : ℝ) q.num)
hq₂ : HDiv.hDiv (α := ℝ) (↑q.num : ℝ) (↑q.den : ℝ) < log ((w : (a : F) → ℝ) b) / log ((w : (a : F) → ℝ) a)
linarith :
  LE.le (α := ℝ) ((v : (a : F) → ℝ) b : ℝ) (0 : ℝ) →
    -1 + HSub.hSub (α := ℝ) (β := ℝ) (1 : ℝ) ((v : (a : F) → ℝ) b : ℝ) +
        HSub.hSub (α := ℝ) (β := ℝ) ((v : (a : F) → ℝ) b : ℝ) (0 : ℝ) =
      0
⊢ LT.lt (α := ℝ) (0 : ℝ) ((v : (a : F) → ℝ) b : ℝ)

Tactic:
linarith
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
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 (HPow.hPow (α := ℝ) ((v : (a : F) → ℝ) b : ℝ) q.den) < log (HPow.hPow (α := ℝ) ((v : (a : F) → ℝ) a : ℝ) q.num)
hq₂ : HDiv.hDiv (α := ℝ) (↑q.num : ℝ) (↑q.den : ℝ) < log ((w : (a : F) → ℝ) b) / log ((w : (a : F) → ℝ) a)
linarith :
  LE.le (α := ℝ) ((v : (a : F) → ℝ) a : ℝ) (0 : ℝ) →
    -1 + HSub.hSub (α := ℝ) (β := ℝ) (1 : ℝ) ((v : (a : F) → ℝ) a : ℝ) +
        HSub.hSub (α := ℝ) (β := ℝ) ((v : (a : F) → ℝ) a : ℝ) (0 : ℝ) =
      0
⊢ LT.lt (α := ℝ) (0 : ℝ) ((v : (a : F) → ℝ) a : ℝ)

Tactic:
linarith
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
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₁ : HPow.hPow (α := ℝ) ((v : (a : F) → ℝ) b : ℝ) q.den < HPow.hPow (α := ℝ) ((v : (a : F) → ℝ) a : ℝ) q.num
hq₂ : HDiv.hDiv (α := ℝ) (↑q.num : ℝ) (↑q.den : ℝ) < log ((w : (a : F) → ℝ) b) / log ((w : (a : F) → ℝ) a)
linarith :
  LE.le (α := ℝ) ((v : (a : F) → ℝ) a : ℝ) (0 : ℝ) →
    -1 + HSub.hSub (α := ℝ) (β := ℝ) (1 : ℝ) ((v : (a : F) → ℝ) a : ℝ) +
        HSub.hSub (α := ℝ) (β := ℝ) ((v : (a : F) → ℝ) a : ℝ) (0 : ℝ) =
      0
⊢ LT.lt (α := ℝ) (0 : ℝ) ((v : (a : F) → ℝ) a : ℝ)

Tactic:
linarith
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
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)
⊢ 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₁

Premises used: pow_pos, Real.log_zpow, Real.log_pos, map_pow, zpow_pos, map_div₀, div_lt_one, mul_comm, Real.log_lt_log_iff, Real.log_pow, map_zpow₀, div_lt_div_iff₀
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
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)
hq₃ : LT.lt (α := ℝ) ((v : (a : F) → ℝ) (b ^ q.den / a ^ q.num) : ℝ) (1 : ℝ)
⊢ HDiv.hDiv (α := ℝ) (↑q.num : ℝ) (↑q.den : ℝ) < log ((w : (a : F) → ℝ) b) / log ((w : (a : F) → ℝ) a)

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₁

Premises used: pow_pos, Real.log_zpow, Real.log_pos, map_pow, zpow_pos, map_div₀, div_lt_one, mul_comm, Real.log_lt_log_iff, Real.log_pow, map_zpow₀, div_lt_div_iff₀
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
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)
⊢ LT.lt (α := ℝ) 0 (↑q.den : ℝ)

Tactic:
simp [q.den_pos]

Premises used: Rat.den_pos
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
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)
linarith :
  LE.le (α := ℝ) ((w : (a : F) → ℝ) a : ℝ) (0 : ℝ) →
    -1 + HSub.hSub (α := ℝ) (β := ℝ) (1 : ℝ) ((w : (a : F) → ℝ) a : ℝ) +
        HSub.hSub (α := ℝ) (β := ℝ) ((w : (a : F) → ℝ) a : ℝ) (0 : ℝ) =
      0
⊢ LT.lt (α := ℝ) (0 : ℝ) ((w : (a : F) → ℝ) a : ℝ)

Tactic:
linarith
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
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)
linarith :
  LE.le (α := ℝ) ((w : (a : F) → ℝ) b : ℝ) (0 : ℝ) →
    -1 + HSub.hSub (α := ℝ) (β := ℝ) (1 : ℝ) ((w : (a : F) → ℝ) b : ℝ) +
        HSub.hSub (α := ℝ) (β := ℝ) ((w : (a : F) → ℝ) b : ℝ) (0 : ℝ) =
      0
⊢ LT.lt (α := ℝ) (0 : ℝ) ((w : (a : F) → ℝ) b : ℝ)

Tactic:
linarith
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
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
linarith :
  LE.le (α := ℝ) ((w : (a : F) → ℝ) a : ℝ) (0 : ℝ) →
    -1 + HSub.hSub (α := ℝ) (β := ℝ) (1 : ℝ) ((w : (a : F) → ℝ) a : ℝ) +
        HSub.hSub (α := ℝ) (β := ℝ) ((w : (a : F) → ℝ) a : ℝ) (0 : ℝ) =
      0
⊢ LT.lt (α := ℝ) (0 : ℝ) ((w : (a : F) → ℝ) a : ℝ)

Tactic:
linarith
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
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)
⊢ 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₂

Premises used: pow_pos, one_lt_div, Real.log_zpow, Real.log_pos, map_pow, Real.log, zpow_pos, map_div₀, mul_comm, Real.log_lt_log_iff, Real.log_pow, map_zpow₀, div_lt_div_iff₀, DFunLike.coe
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
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₂ : LT.lt (α := ℝ) (1 : ℝ) ((w : (a : F) → ℝ) (b ^ q.den / a ^ q.num) : ℝ)
⊢ False

Tactic:
not_lt_of_gt (h.lt_one_iff.1 hq₁) hq₂

Premises used: AbsoluteValue.IsEquiv.lt_one_iff, Iff.mp, not_lt_of_gt
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
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₂ : LT.lt (α := ℝ) (1 : ℝ) ((w : (a : F) → ℝ) (b ^ q.den / a ^ q.num) : ℝ)
⊢ False

Tactic:
exact not_lt_of_gt (h.lt_one_iff.1 hq₁) hq₂

Premises used: AbsoluteValue.IsEquiv.lt_one_iff, Iff.mp, not_lt_of_gt
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
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) → ℝ)

Tactic:
⟨fun h ↦ ?_, fun ⟨t, ht, h⟩ ↦ isEquiv_iff_lt_one_iff.2
    fun x ↦ h ▸ (rpow_lt_one_iff' (v.nonneg x) ht).symm⟩

Premises used: Iff.mpr, AbsoluteValue.isEquiv_iff_lt_one_iff, Eq.rec, AbsoluteValue.nonneg, _private.0.AbsoluteValue.isEquiv_iff_exists_rpow_eq.match_1, Iff.intro, Iff.symm, AbsoluteValue.IsEquiv, Real.rpow_lt_one_iff'
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
Goal:
F : Type u_1
inst : Field F
v w : AbsoluteValue F ℝ
refine :
  ∀ (h : v.IsEquiv w),
    ∃ (c : ℝ), 0 < c ∧ Eq (α := F → ℝ) (fun (x : F) ↦ HPow.hPow (α := ℝ) ((v : (a : F) → ℝ) x : ℝ) c) (⇑w : (a : F) → ℝ)
⊢ 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⟩
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
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) → ℝ)
neg :
  ∀ (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) → ℝ)

Tactic:
by_cases hw : w.IsNontrivial

Premises used: AbsoluteValue.IsNontrivial
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
Goal:
F : Type u_1
inst : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
hw : w.IsNontrivial
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) → ℝ)
⊢ ∃ (c : ℝ), 0 < c ∧ Eq (α := F → ℝ) (fun (x : F) ↦ HPow.hPow (α := ℝ) ((v : (a : F) → ℝ) x : ℝ) c) (⇑w : (a : F) → ℝ)

Tactic:
let ⟨a, ha₀, ha₁⟩ := hw
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
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) → ℝ)

Tactic:
⟨(w a).log / (v a).log, h.log_div_log_pos ha₀ ha₁, funext fun b ↦ ?_⟩

Premises used: HDiv.hDiv, AbsoluteValue.IsEquiv.log_div_log_pos, Real.log, funext, And.intro, Exists.intro, DFunLike.coe
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
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 : ℝ)
pos :
  ∀ (b : F),
    HPow.hPow (α := ℝ) ((v : (a : F) → ℝ) b : ℝ) (log ((w : (a : F) → ℝ) a) / log ((v : (a : F) → ℝ) a)) =
      (w : (a : F) → ℝ) b
⊢ ∃ (c : ℝ), 0 < c ∧ Eq (α := F → ℝ) (fun (x : F) ↦ HPow.hPow (α := ℝ) ((v : (a : F) → ℝ) x : ℝ) c) (⇑w : (a : F) → ℝ)

Tactic:
refine ⟨(w a).log / (v a).log, h.log_div_log_pos ha₀ ha₁, funext fun b ↦ ?_⟩
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
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
pos₁ :
  ∀ (hb₀ : b ≠ 0),
    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

Tactic:
rcases eq_or_ne b 0 with rfl | hb₀

Premises used: eq_or_ne, OfNat.ofNat, rfl