awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.AbsoluteValue.Equivalence (goal)
Goal:
R : Type u_1
S : Type u_2
inst : Field R
inst_1 : Field S
inst_2 : LinearOrder S
inst_3 : TopologicalSpace S
inst_4 : IsStrictOrderedRing S
inst_5 : Archimedean S
inst_6 : OrderTopology S
ι_1 : Type u_3
inst_7 : Finite ι_1
v_1 : ι_1 → AbsoluteValue R S
this : Fintype ι_1
P : (ι : Type u_3) → [Fintype ι] → Prop :=
  fun (ι : Type u_3) [Fintype ι] ↦
    ∀ (v : ι → AbsoluteValue R S),
      (∀ (i : ι), (v i).IsNontrivial) →
        (Pairwise fun (i j : ι) ↦ ¬(v i).IsEquiv (v j)) →
          ∀ (i : ι),
            ∃ (a : R),
              LT.lt.{u_2} (α := S) (1 : S) ((v i : (a : R) → S) a : S) ∧
                ∀ (j : ι), j ≠ i → LT.lt.{u_2} (α := S) ((v j : (a : R) → S) a : S) (1 : S)
ι : Type u_3
x : Fintype ι
h_1 : Nontrivial ι
ih : ∀ (β : Type u_3) [inst : Fintype β], card β < card ι → P β
v : ι → AbsoluteValue R S
h : ∀ (i : ι), (v i).IsNontrivial
hv : Pairwise fun (i j : ι) ↦ ¬(v i).IsEquiv (v j)
i : ι
hc_1 : card ι ≠ 2
hlt : 2 < card ι
j : ι
hj : j ≠ i
a : R
ha :
  LT.lt.{u_2} (α := S) (1 : S)
      ((restrict (β := fun (x : ι) ↦ AbsoluteValue R S) (fun (k : ι) ↦ k ≠ j) v
              (Subtype.mk (p := fun (k : ι) ↦ k ≠ j) i ⋯) :
            (a : R) → S)
          a :
        S) ∧
    ∀ (j_1 : { k : ι // k ≠ j }),
      j_1 ≠ Subtype.mk (p := fun (k : ι) ↦ k ≠ j) i ⋯ →
        LT.lt.{u_2} (α := S)
          ((restrict (β := fun (x : ι) ↦ AbsoluteValue R S) (fun (k : ι) ↦ k ≠ j) v j_1 : (a : R) → S) a : S) (1 : S)
b : R
hb :
  LT.lt.{u_2} (α := S) (1 : S)
      ((restrict (β := fun (x : ι) ↦ AbsoluteValue R S) (fun (k : ι) ↦ k = i ∨ k = j) v
              (Subtype.mk (p := fun (k : ι) ↦ k = i ∨ k = j) i ⋯) :
            (a : R) → S)
          b :
        S) ∧
    ∀ (j_1 : { k : ι // k = i ∨ k = j }),
      j_1 ≠ Subtype.mk (p := fun (k : ι) ↦ k = i ∨ k = j) i ⋯ →
        LT.lt.{u_2} (α := S)
          ((restrict (β := fun (x : ι) ↦ AbsoluteValue R S) (fun (k : ι) ↦ k = i ∨ k = j) v j_1 : (a : R) → S) b : S)
          (1 : S)
ha₁ : Ne.{u_2 + 1} (α := S) ((v j : (a : R) → S) a : S) (1 : S)
ha_gt : LT.lt.{u_2} (α := S) (1 : S) ((v j : (a : R) → S) a : S)
c : R
hc :
  LT.lt.{u_2} (α := S) (1 : S)
      ((restrict (β := fun (x : ι) ↦ AbsoluteValue R S) (fun (k : ι) ↦ k ≠ j) v
              (Subtype.mk (p := fun (k : ι) ↦ k ≠ j) i ⋯) :
            (a : R) → S)
          c :
        S) ∧
    (∀ (j_1 : { k : ι // k ≠ j }),
        j_1 ≠ Subtype.mk (p := fun (k : ι) ↦ k ≠ j) i ⋯ →
          LT.lt.{u_2} (α := S)
            ((restrict (β := fun (x : ι) ↦ AbsoluteValue R S) (fun (k : ι) ↦ k ≠ j) v j_1 : (a : R) → S) c : S)
            (1 : S)) ∧
      LT.lt.{u_2} (α := S) ((v j : (a : R) → S) c : S) (1 : S)
⊢ ∃ (a : R),
    LT.lt.{u_2} (α := S) (1 : S) ((v i : (a : R) → S) a : S) ∧
      ∀ (j : ι), j ≠ i → LT.lt.{u_2} (α := S) ((v j : (a : R) → S) a : S) (1 : S)
have refine_2 : ∀ (k : ι) (hk : k ≠ i), LT.lt.{u_2} (α := S) ((v k : (a : R) → S) c : S) (1 : S)
Tactic: refine ⟨c, hc.1, fun k hk ↦ ?_⟩
-- 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 (α := ℝ) ((w : (a : F) → ℝ) a : ℝ) (1 : ℝ)
⊢ 0 < log ((w : (a : F) → ℝ) a) / log ((v : (a : F) → ℝ) a)
have inl : ∀ (hwa : LT.lt (α := ℝ) ((w : (a : F) → ℝ) a : ℝ) (1 : ℝ)), 0 < log ((w : (a : F) → ℝ) a) / log ((v : (a : F) → ℝ) a)
Tactic: rcases ha₁.lt_or_gt with hwa | hwa
-- 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 (α := ℝ) ((w : (a : F) → ℝ) a : ℝ) (1 : ℝ)
inl :
  ∀ (hwa : LT.lt (α := ℝ) ((w : (a : F) → ℝ) a : ℝ) (1 : ℝ)), 0 < log ((w : (a : F) → ℝ) a) / log ((v : (a : F) → ℝ) a)
⊢ 0 < log ((w : (a : F) → ℝ) a) / log ((v : (a : F) → ℝ) a)
have inr : ∀ (hwa : LT.lt (α := ℝ) (1 : ℝ) ((w : (a : F) → ℝ) a : ℝ)), 0 < log ((w : (a : F) → ℝ) a) / log ((v : (a : F) → ℝ) a)
Tactic: rcases ha₁.lt_or_gt with hwa | hwa
-- 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 : ℝ)
⊢ log ((v : (a : F) → ℝ) b) / log ((w : (a : F) → ℝ) b) = log ((v : (a : F) → ℝ) a) / log ((w : (a : F) → ℝ) a)
have by_contra! : ∀
  (h_ne :
    log ((v : (a : F) → ℝ) b) / log ((w : (a : F) → ℝ) b) ≠ log ((v : (a : F) → ℝ) a) / log ((w : (a : F) → ℝ) a)),
  False
Tactic: by_contra! h_ne
-- 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)
⊢ False
have inr : ∀
  (this :
    ∀ {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 : ℝ)), False)
  (ha : LE.le (α := ℝ) ((v : (a : F) → ℝ) a : ℝ) (1 : ℝ)), False
Tactic: wlog! ha : 1 < v a generalizing a 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
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)
inr :
  ∀
    (this :
      ∀ {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 : ℝ)), False)
    (ha : LE.le (α := ℝ) ((v : (a : F) → ℝ) a : ℝ) (1 : ℝ)), False
⊢ False
have wlog! : ∀ {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 : ℝ)), False
Tactic: wlog! ha : 1 < v a generalizing a b
Cleared hypotheses: a, ha₀, ha₁, b, hb₀, hb₁, h_ne
-- 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)
this :
  ∀ {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 : ℝ)), False
ha : LE.le (α := ℝ) ((v : (a : F) → ℝ) a : ℝ) (1 : ℝ)
⊢ False
have inr : LT.lt (α := ℝ) (1 : ℝ) ((v : (a : F) → ℝ) a⁻¹ : ℝ)
Tactic: apply this (inv_ne_zero ha₀) (by simpa) hb₀ hb₁ (by simpa)
-- 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 : ℝ)
⊢ False
have inr : ∀
  (this :
    ∀ {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 : ℝ)),
      False)
  (hb : LE.le (α := ℝ) ((v : (a : F) → ℝ) b : ℝ) (1 : ℝ)), False
Tactic: wlog! hb : 1 < v b generalizing a 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
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 : ℝ)
inr :
  ∀
    (this :
      ∀ {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 : ℝ)),
        False)
    (hb : LE.le (α := ℝ) ((v : (a : F) → ℝ) b : ℝ) (1 : ℝ)), False
⊢ False
have wlog! : ∀ {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 : ℝ)), False
Tactic: wlog! hb : 1 < v b generalizing a b
Cleared hypotheses: a, ha₀, ha₁, b, hb₀, hb₁, h_ne, 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
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 : ℝ)
this :
  ∀ {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 : ℝ)),
    False
hb : LE.le (α := ℝ) ((v : (a : F) → ℝ) b : ℝ) (1 : ℝ)
⊢ False
have inr : LT.lt (α := ℝ) (1 : ℝ) ((v : (a : F) → ℝ) b⁻¹ : ℝ)
Tactic: apply this ha₀ ha₁ (inv_ne_zero hb₀) (by simpa) (by simpa) 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
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 : ℝ)
⊢ False
have inr : ∀
  (this :
    ∀ {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)),
      False)
  (h_lt :
    log ((v : (a : F) → ℝ) a) / log ((w : (a : F) → ℝ) a) ≤ log ((v : (a : F) → ℝ) b) / log ((w : (a : F) → ℝ) b)),
  False
Tactic: wlog! h_lt : (v b).log / (w b).log < (v a).log / (w a).log generalizing a 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
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 : ℝ)
inr :
  ∀
    (this :
      ∀ {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)),
        False)
    (h_lt :
      log ((v : (a : F) → ℝ) a) / log ((w : (a : F) → ℝ) a) ≤ log ((v : (a : F) → ℝ) b) / log ((w : (a : F) → ℝ) b)),
    False
⊢ False
have wlog! : ∀ {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)),
  False
Tactic: wlog! h_lt : (v b).log / (w b).log < (v a).log / (w a).log generalizing a b
Cleared hypotheses: a, ha₀, ha₁, b, hb₀, hb₁, h_ne, ha, hb
-- 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 ((w : (a : F) → ℝ) b) < log ((v : (a : F) → ℝ) a) / log ((w : (a : F) → ℝ) a)
⊢ False
have hwa : LT.lt (α := ℝ) (1 : ℝ) ((w : (a : F) → ℝ) a : ℝ)
Tactic: have hwa := h.one_lt_iff.1 ha
-- 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 ((w : (a : F) → ℝ) b) < log ((v : (a : F) → ℝ) a) / log ((w : (a : F) → ℝ) a)
hwa : LT.lt (α := ℝ) (1 : ℝ) ((w : (a : F) → ℝ) a : ℝ)
⊢ False
have hwb : LT.lt (α := ℝ) (1 : ℝ) ((w : (a : F) → ℝ) b : ℝ)
Tactic: have hwb := h.one_lt_iff.1 hb
-- 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 ((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 : ℝ)
⊢ False
have h_lt₁ : log ((v : (a : F) → ℝ) b) / log ((v : (a : F) → ℝ) a) < log ((w : (a : F) → ℝ) b) / log ((w : (a : F) → ℝ) a)
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
Cleared hypotheses: h_lt, hwa, hwb
-- 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 : ℝ)
⊢ False
have 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
Tactic: let ⟨q, ⟨hq₁, hq₂⟩⟩ := exists_rat_btwn h_lt
-- 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) < (↑q : ℝ)
hq₂ : (↑q : ℝ) < log ((w : (a : F) → ℝ) b) / log ((w : (a : F) → ℝ) a)
⊢ False
have hq₃ : 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₂
Cleared hypotheses: hq₁, hq₂
-- 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) < (↑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 : ℝ)
⊢ False
have hq₄ : 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₂
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₁ :
  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)
⊢ LT.lt (α := ℝ) (0 : ℝ) ((v : (a : F) → ℝ) b : ℝ)
have linarith : LE.le (α := ℝ) ((v : (a : F) → ℝ) b : ℝ) (0 : ℝ) →
  -1 + HSub.hSub (α := ℝ) (β := ℝ) (1 : ℝ) ((v : (a : F) → ℝ) b : ℝ) +
      HSub.hSub (α := ℝ) (β := ℝ) ((v : (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₁ :
  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)
⊢ LT.lt (α := ℝ) (0 : ℝ) ((v : (a : F) → ℝ) a : ℝ)
have linarith : LE.le (α := ℝ) ((v : (a : F) → ℝ) a : ℝ) (0 : ℝ) →
  -1 + HSub.hSub (α := ℝ) (β := ℝ) (1 : ℝ) ((v : (a : F) → ℝ) a : ℝ) +
      HSub.hSub (α := ℝ) (β := ℝ) ((v : (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₁ : 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)
⊢ LT.lt (α := ℝ) (0 : ℝ) ((v : (a : F) → ℝ) a : ℝ)
have linarith : LE.le (α := ℝ) ((v : (a : F) → ℝ) a : ℝ) (0 : ℝ) →
  -1 + HSub.hSub (α := ℝ) (β := ℝ) (1 : ℝ) ((v : (a : F) → ℝ) a : ℝ) +
      HSub.hSub (α := ℝ) (β := ℝ) ((v : (a : F) → ℝ) a : ℝ) (0 : ℝ) =
    0
Tactic: linarith