awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
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 ι
a b c : R
k : ι
hk hj : k ≠ i
ha :
  LT.lt.{u_2} (α := S) (1 : S)
      ((restrict (β := fun (x : ι) ↦ AbsoluteValue R S) (fun (k_1 : ι) ↦ k_1 ≠ k) v
              (Subtype.mk (p := fun (k_1 : ι) ↦ k_1 ≠ k) i ⋯) :
            (a : R) → S)
          a :
        S) ∧
    ∀ (j : { k_1 : ι // k_1 ≠ k }),
      j ≠ Subtype.mk (p := fun (k_1 : ι) ↦ k_1 ≠ k) i ⋯ →
        LT.lt.{u_2} (α := S)
          ((restrict (β := fun (x : ι) ↦ AbsoluteValue R S) (fun (k_1 : ι) ↦ k_1 ≠ k) v j : (a : R) → S) a : S) (1 : S)
hb :
  LT.lt.{u_2} (α := S) (1 : S)
      ((restrict (β := fun (x : ι) ↦ AbsoluteValue R S) (fun (k_1 : ι) ↦ k_1 = i ∨ k_1 = k) v
              (Subtype.mk (p := fun (k_1 : ι) ↦ k_1 = i ∨ k_1 = k) i ⋯) :
            (a : R) → S)
          b :
        S) ∧
    ∀ (j : { k_1 : ι // k_1 = i ∨ k_1 = k }),
      j ≠ Subtype.mk (p := fun (k_1 : ι) ↦ k_1 = i ∨ k_1 = k) i ⋯ →
        LT.lt.{u_2} (α := S)
          ((restrict (β := fun (x : ι) ↦ AbsoluteValue R S) (fun (k_1 : ι) ↦ k_1 = i ∨ k_1 = k) v j : (a : R) → S) b :
            S)
          (1 : S)
ha₁ : Ne.{u_2 + 1} (α := S) ((v k : (a : R) → S) a : S) (1 : S)
ha_gt : LT.lt.{u_2} (α := S) (1 : S) ((v k : (a : R) → S) a : S)
hc :
  LT.lt.{u_2} (α := S) (1 : S)
      ((restrict (β := fun (x : ι) ↦ AbsoluteValue R S) (fun (k_1 : ι) ↦ k_1 ≠ k) v
              (Subtype.mk (p := fun (k_1 : ι) ↦ k_1 ≠ k) i ⋯) :
            (a : R) → S)
          c :
        S) ∧
    (∀ (j : { k_1 : ι // k_1 ≠ k }),
        j ≠ Subtype.mk (p := fun (k_1 : ι) ↦ k_1 ≠ k) i ⋯ →
          LT.lt.{u_2} (α := S)
            ((restrict (β := fun (x : ι) ↦ AbsoluteValue R S) (fun (k_1 : ι) ↦ k_1 ≠ k) v j : (a : R) → S) c : S)
            (1 : S)) ∧
      LT.lt.{u_2} (α := S) ((v k : (a : R) → S) c : S) (1 : S)
⊢ LT.lt.{u_2} (α := S) ((v k : (a : R) → S) c : S) (1 : S)

Tactic:
try exact hc.2.2; exact hc.2.1 ⟨k, h⟩ (by grind)

Premises used: And.right
-- 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 (α := ℝ) ((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)
inr :
  ∀ (hwa : LT.lt (α := ℝ) (1 : ℝ) ((w : (a : F) → ℝ) a : ℝ)), 0 < log ((w : (a : F) → ℝ) a) / log ((v : (a : F) → ℝ) a)
⊢ 0 < log ((w : (a : F) → ℝ) a) / log ((v : (a : F) → ℝ) a)

Tactic:
rcases ha₁.lt_or_gt with hwa | hwa

Premises used: Ne.lt_or_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 (α := ℝ) ((w : (a : F) → ℝ) a : ℝ) (1 : ℝ)
hwa : LT.lt (α := ℝ) ((w : (a : F) → ℝ) a : ℝ) (1 : ℝ)
⊢ 0 < log ((w : (a : F) → ℝ) a) / log ((v : (a : F) → ℝ) a)

Tactic:
simpa using div_pos (neg_pos_of_neg <| log_neg (w.pos ha₀) (hwa))
      (neg_pos_of_neg <| log_neg (v.pos ha₀) (h.lt_one_iff.2 hwa))

Premises used: Iff.mpr, neg_pos_of_neg, AbsoluteValue.pos, AbsoluteValue.IsEquiv.lt_one_iff, div_pos, Real.log_neg
-- 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 (α := ℝ) ((w : (a : F) → ℝ) a : ℝ) (1 : ℝ)
hwa : LT.lt (α := ℝ) (1 : ℝ) ((w : (a : F) → ℝ) a : ℝ)
⊢ 0 < log ((w : (a : F) → ℝ) a) / log ((v : (a : F) → ℝ) a)

Tactic:
div_pos (log_pos <| hwa) (log_pos (h.one_lt_iff.2 hwa))

Premises used: Iff.mpr, Real.log_pos, AbsoluteValue.IsEquiv.one_lt_iff, div_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 (α := ℝ) ((w : (a : F) → ℝ) a : ℝ) (1 : ℝ)
hwa : LT.lt (α := ℝ) (1 : ℝ) ((w : (a : F) → ℝ) a : ℝ)
⊢ 0 < log ((w : (a : F) → ℝ) a) / log ((v : (a : F) → ℝ) a)

Tactic:
exact div_pos (log_pos <| hwa) (log_pos (h.one_lt_iff.2 hwa))

Premises used: Iff.mpr, Real.log_pos, AbsoluteValue.IsEquiv.one_lt_iff, div_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 : ℝ)
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
⊢ log ((v : (a : F) → ℝ) b) / log ((w : (a : F) → ℝ) b) = log ((v : (a : F) → ℝ) a) / log ((w : (a : F) → ℝ) a)

Tactic:
by_contra! h_ne
-- 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)
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
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
⊢ False

Tactic:
wlog! ha : 1 < v a generalizing a b

Premises used: 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)
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 : ℝ)
⊢ Ne (α := ℝ) ((v : (a : F) → ℝ) a⁻¹ : ℝ) (1 : ℝ)

Tactic:
simpa
-- 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)
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 : ℝ)
⊢ log ((v : (a : F) → ℝ) b) / log ((w : (a : F) → ℝ) b) ≠ log ((v : (a : F) → ℝ) a⁻¹) / log ((w : (a : F) → ℝ) a⁻¹)

Tactic:
simpa
-- 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)
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 : ℝ)
inr : LT.lt (α := ℝ) (1 : ℝ) ((v : (a : F) → ℝ) a⁻¹ : ℝ)
⊢ False

Tactic:
apply this (inv_ne_zero ha₀) (by simpa) hb₀ hb₁ (by simpa)

Premises used: inv_ne_zero
-- 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)
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 : ℝ)
⊢ LT.lt (α := ℝ) (1 : ℝ) ((v : (a : F) → ℝ) a⁻¹ : ℝ)

Tactic:
simpa using one_lt_inv_iff₀.2 ⟨v.pos ha₀, ha₁.lt_of_le ha⟩

Premises used: Iff.mpr, one_lt_inv_iff₀, AbsoluteValue.pos, And.intro, Ne.lt_of_le
-- 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 : ℝ)
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
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
⊢ False

Tactic:
wlog! hb : 1 < v b generalizing a b

Premises used: 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 : ℝ)
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 : ℝ)
⊢ Ne (α := ℝ) ((v : (a : F) → ℝ) b⁻¹ : ℝ) (1 : ℝ)

Tactic:
simpa
-- 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 : ℝ)
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 : ℝ)
⊢ log ((v : (a : F) → ℝ) b⁻¹) / log ((w : (a : F) → ℝ) b⁻¹) ≠ log ((v : (a : F) → ℝ) a) / log ((w : (a : F) → ℝ) a)

Tactic:
simpa
-- 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 : ℝ)
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 : ℝ)
inr : LT.lt (α := ℝ) (1 : ℝ) ((v : (a : F) → ℝ) b⁻¹ : ℝ)
⊢ False

Tactic:
apply this ha₀ ha₁ (inv_ne_zero hb₀) (by simpa) (by simpa) ha

Premises used: inv_ne_zero
-- 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 : ℝ)
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 : ℝ)
⊢ LT.lt (α := ℝ) (1 : ℝ) ((v : (a : F) → ℝ) b⁻¹ : ℝ)

Tactic:
simpa using one_lt_inv_iff₀.2 ⟨v.pos hb₀, hb₁.lt_of_le hb⟩

Premises used: Iff.mpr, one_lt_inv_iff₀, AbsoluteValue.pos, And.intro, Ne.lt_of_le
-- 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 : ℝ)
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
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
⊢ False

Tactic:
wlog! h_lt : (v b).log / (w b).log < (v a).log / (w a).log generalizing a b

Premises used: Real.log, 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 : ℝ)
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:
this hb₀ hb₁ ha₀ ha₁ h_ne.symm hb ha <| lt_of_le_of_ne h_lt h_ne.symm

Premises used: Ne.symm, lt_of_le_of_ne
-- 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 : ℝ)
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:
exact this hb₀ hb₁ ha₀ ha₁ h_ne.symm hb ha <| lt_of_le_of_ne h_lt h_ne.symm

Premises used: Ne.symm, lt_of_le_of_ne
-- 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)
⊢ LT.lt (α := ℝ) (1 : ℝ) ((w : (a : F) → ℝ) a : ℝ)

Tactic:
have hwa := h.one_lt_iff.1 ha
-- 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 : ℝ)
⊢ LT.lt (α := ℝ) (1 : ℝ) ((w : (a : F) → ℝ) b : ℝ)

Tactic:
have hwb := h.one_lt_iff.1 hb
-- 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 : ℝ)
⊢ 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

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 ((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)
⊢ LT.lt (α := ℝ) (1 : ℝ) ((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

Premises used: Real.log_pos, Real.log, mul_comm, div_lt_div_iff₀, DFunLike.coe