awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
inst_1 : Semiring S
inst_2 : PartialOrder S
v w : AbsoluteValue R S
inst_3 : IsDomain S
inst_4 : Nontrivial R
h : v.IsEquiv w
x : R
⊢ Eq.{u_2 + 1} (α := S) ((v : (a : R) → S) x : S) (1 : S) ↔ Eq.{u_2 + 1} (α := S) ((w : (a : R) → S) x : S) (1 : S)

Tactic:
simpa only [map_one] using h.eq_iff_eq (x := x) (y := 1)

Premises used: AbsoluteValue.IsEquiv.eq_iff_eq, map_one
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
inst_1 : Semiring S
inst_2 : PartialOrder S
v : AbsoluteValue R S
inst_3 : IsDomain S
inst_4 : Nontrivial R
w : AbsoluteValue R S
h : v.IsEquiv w
⊢ ¬v.IsNontrivial ↔ ¬w.IsNontrivial

Tactic:
aesop (add simp [not_isNontrivial_iff, h.eq_one_iff])

Premises used: AbsoluteValue.not_isNontrivial_iff, AbsoluteValue.IsEquiv.eq_one_iff
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
Goal:
R : Type u_1
S : Type u_2
inst : Field R
inst_1 : Semifield S
inst_2 : LinearOrder S
inst_3 : DecidablePred fun (x : R) ↦ x = 0
inst_4 : NoZeroDivisors R
inst_5 : IsStrictOrderedRing S
f : AbsoluteValue R S
h : f.IsEquiv AbsoluteValue.trivial
⊢ f = AbsoluteValue.trivial

Tactic:
aesop (add simp [h.eq_one_iff, AbsoluteValue.trivial])

Premises used: AbsoluteValue.trivial, AbsoluteValue.IsEquiv.eq_one_iff
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
Goal:
R : Type u_1
S : Type u_2
inst : Field R
inst_1 : Semifield S
inst_2 : LinearOrder S
v w : AbsoluteValue R S
inst_3 : IsStrictOrderedRing S
⊢ v.IsEquiv w ↔
    ∀ (x : R),
      LT.lt.{u_2} (α := S) ((v : (a : R) → S) x : S) (1 : S) ↔ LT.lt.{u_2} (α := S) ((w : (a : R) → S) x : S) (1 : S)

Tactic:
⟨fun h _ ↦ h.lt_one_iff, fun h x y ↦ ?_⟩

Premises used: AbsoluteValue.IsEquiv.lt_one_iff, Iff.intro
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
Goal:
R : Type u_1
S : Type u_2
inst : Field R
inst_1 : Semifield S
inst_2 : LinearOrder S
v w : AbsoluteValue R S
inst_3 : IsStrictOrderedRing S
refine :
  ∀
    (h :
      ∀ (x : R),
        LT.lt.{u_2} (α := S) ((v : (a : R) → S) x : S) (1 : S) ↔ LT.lt.{u_2} (α := S) ((w : (a : R) → S) x : S) (1 : S))
    (x y : R),
    LE.le.{u_2} (α := S) ((v : (a : R) → S) x : S) ((v : (a : R) → S) y : S) ↔
      LE.le.{u_2} (α := S) ((w : (a : R) → S) x : S) ((w : (a : R) → S) y : S)
⊢ v.IsEquiv w ↔
    ∀ (x : R),
      LT.lt.{u_2} (α := S) ((v : (a : R) → S) x : S) (1 : S) ↔ LT.lt.{u_2} (α := S) ((w : (a : R) → S) x : S) (1 : S)

Tactic:
refine ⟨fun h _ ↦ h.lt_one_iff, fun h x y ↦ ?_⟩
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
Goal:
R : Type u_1
S : Type u_2
inst : Field R
inst_1 : Semifield S
inst_2 : LinearOrder S
v w : AbsoluteValue R S
inst_3 : IsStrictOrderedRing S
h :
  ∀ (x : R),
    LT.lt.{u_2} (α := S) ((v : (a : R) → S) x : S) (1 : S) ↔ LT.lt.{u_2} (α := S) ((w : (a : R) → S) x : S) (1 : S)
x y : R
inl :
  Eq.{u_2 + 1} (α := S) ((v : (a : R) → S) x : S) (0 : S) →
    (LE.le.{u_2} (α := S) ((v : (a : R) → S) x : S) ((v : (a : R) → S) y : S) ↔
      LE.le.{u_2} (α := S) ((w : (a : R) → S) x : S) ((w : (a : R) → S) y : S))
inr :
  ∀ (hy₀ : Ne.{u_2 + 1} (α := S) ((v : (a : R) → S) x : S) (0 : S)),
    LE.le.{u_2} (α := S) ((v : (a : R) → S) x : S) ((v : (a : R) → S) y : S) ↔
      LE.le.{u_2} (α := S) ((w : (a : R) → S) x : S) ((w : (a : R) → S) y : S)
⊢ LE.le.{u_2} (α := S) ((v : (a : R) → S) x : S) ((v : (a : R) → S) y : S) ↔
    LE.le.{u_2} (α := S) ((w : (a : R) → S) x : S) ((w : (a : R) → S) y : S)

Tactic:
rcases eq_or_ne (v x) 0 with (_ | hy₀)

Premises used: eq_or_ne, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
Goal:
R : Type u_1
S : Type u_2
inst : Field R
inst_1 : Semifield S
inst_2 : LinearOrder S
v w : AbsoluteValue R S
inst_3 : IsStrictOrderedRing S
h :
  ∀ (x : R),
    LT.lt.{u_2} (α := S) ((v : (a : R) → S) x : S) (1 : S) ↔ LT.lt.{u_2} (α := S) ((w : (a : R) → S) x : S) (1 : S)
x y : R
h_1 : Eq.{u_2 + 1} (α := S) ((v : (a : R) → S) x : S) (0 : S)
⊢ LE.le.{u_2} (α := S) ((v : (a : R) → S) x : S) ((v : (a : R) → S) y : S) ↔
    LE.le.{u_2} (α := S) ((w : (a : R) → S) x : S) ((w : (a : R) → S) y : S)

Tactic:
simp_all
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
Goal:
R : Type u_1
S : Type u_2
inst : Field R
inst_1 : Semifield S
inst_2 : LinearOrder S
v w : AbsoluteValue R S
inst_3 : IsStrictOrderedRing S
h :
  ∀ (x : R),
    LT.lt.{u_2} (α := S) ((v : (a : R) → S) x : S) (1 : S) ↔ LT.lt.{u_2} (α := S) ((w : (a : R) → S) x : S) (1 : S)
x y : R
hy₀ : Ne.{u_2 + 1} (α := S) ((v : (a : R) → S) x : S) (0 : S)
⊢ LT.lt.{u_2} (α := S) (0 : S) ((v : (a : R) → S) x : S)

Tactic:
simp_all
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
Goal:
R : Type u_1
S : Type u_2
inst : Field R
inst_1 : Semifield S
inst_2 : LinearOrder S
v w : AbsoluteValue R S
inst_3 : IsStrictOrderedRing S
h :
  ∀ (x : R),
    LT.lt.{u_2} (α := S) ((v : (a : R) → S) x : S) (1 : S) ↔ LT.lt.{u_2} (α := S) ((w : (a : R) → S) x : S) (1 : S)
x y : R
hy₀ : Ne.{u_2 + 1} (α := S) ((v : (a : R) → S) x : S) (0 : S)
⊢ LT.lt.{u_2} (α := S) (0 : S) ((w : (a : R) → S) x : S)

Tactic:
simp_all
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
Goal:
R : Type u_1
S : Type u_2
inst : Field R
inst_1 : Semifield S
inst_2 : LinearOrder S
v w : AbsoluteValue R S
inst_3 : IsStrictOrderedRing S
h :
  ∀ (x : R),
    LT.lt.{u_2} (α := S) ((v : (a : R) → S) x : S) (1 : S) ↔ LT.lt.{u_2} (α := S) ((w : (a : R) → S) x : S) (1 : S)
x y : R
hy₀ : Ne.{u_2 + 1} (α := S) ((v : (a : R) → S) x : S) (0 : S)
inr :
  LT.lt.{u_2} (α := S) ((v : (a : R) → S) (y * x⁻¹) : S) (1 : S) ↔
    LT.lt.{u_2} (α := S) ((w : (a : R) → S) (y * x⁻¹) : S) (1 : S)
⊢ LE.le.{u_2} (α := S) ((v : (a : R) → S) x : S) ((v : (a : R) → S) y : S) ↔
    LE.le.{u_2} (α := S) ((w : (a : R) → S) x : S) ((w : (a : R) → S) y : S)

Tactic:
rw [le_iff_le_iff_lt_iff_lt, ← one_mul (v x), ← mul_inv_lt_iff₀ (by simp_all), ← one_mul (w x),
    ← mul_inv_lt_iff₀ (by simp_all), ← map_inv₀, ← map_mul, ← map_inv₀, ← map_mul]

Premises used: mul_inv_lt_iff₀, le_iff_le_iff_lt_iff_lt, map_inv₀, map_mul, DFunLike.coe, one_mul
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
Goal:
R : Type u_1
S : Type u_2
inst : Field R
inst_1 : Semifield S
inst_2 : LinearOrder S
v w : AbsoluteValue R S
inst_3 : IsStrictOrderedRing S
h :
  ∀ (x : R),
    LT.lt.{u_2} (α := S) ((v : (a : R) → S) x : S) (1 : S) ↔ LT.lt.{u_2} (α := S) ((w : (a : R) → S) x : S) (1 : S)
x y : R
hy₀ : Ne.{u_2 + 1} (α := S) ((v : (a : R) → S) x : S) (0 : S)
⊢ LT.lt.{u_2} (α := S) ((v : (a : R) → S) (y * x⁻¹) : S) (1 : S) ↔
    LT.lt.{u_2} (α := S) ((w : (a : R) → S) (y * x⁻¹) : S) (1 : S)

Tactic:
h _
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
Goal:
R : Type u_1
S : Type u_2
inst : Field R
inst_1 : Semifield S
inst_2 : LinearOrder S
v w : AbsoluteValue R S
inst_3 : IsStrictOrderedRing S
h :
  ∀ (x : R),
    LT.lt.{u_2} (α := S) ((v : (a : R) → S) x : S) (1 : S) ↔ LT.lt.{u_2} (α := S) ((w : (a : R) → S) x : S) (1 : S)
x y : R
hy₀ : Ne.{u_2 + 1} (α := S) ((v : (a : R) → S) x : S) (0 : S)
⊢ LT.lt.{u_2} (α := S) ((v : (a : R) → S) (y * x⁻¹) : S) (1 : S) ↔
    LT.lt.{u_2} (α := S) ((w : (a : R) → S) (y * x⁻¹) : S) (1 : S)

Tactic:
exact h _
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
Goal:
R : Type u_1
S : Type u_2
inst : Field R
inst_1 : Semifield S
inst_2 : LinearOrder S
v w : AbsoluteValue R S
inst_3 : IsStrictOrderedRing S
inst_4 : Archimedean S
inst_5 : ExistsAddOfLE S
hv : v.IsNontrivial
h :
  ∀ (x : R),
    LT.lt.{u_2} (α := S) ((v : (a : R) → S) x : S) (1 : S) → LT.lt.{u_2} (α := S) ((w : (a : R) → S) x : S) (1 : S)
⊢ v.IsEquiv w

Tactic:
isEquiv_iff_lt_one_iff.2 fun a ↦ ?_

Premises used: Iff.mpr, AbsoluteValue.isEquiv_iff_lt_one_iff
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
Goal:
R : Type u_1
S : Type u_2
inst : Field R
inst_1 : Semifield S
inst_2 : LinearOrder S
v w : AbsoluteValue R S
inst_3 : IsStrictOrderedRing S
inst_4 : Archimedean S
inst_5 : ExistsAddOfLE S
hv : v.IsNontrivial
h :
  ∀ (x : R),
    LT.lt.{u_2} (α := S) ((v : (a : R) → S) x : S) (1 : S) → LT.lt.{u_2} (α := S) ((w : (a : R) → S) x : S) (1 : S)
refine :
  ∀ (a : R),
    LT.lt.{u_2} (α := S) ((v : (a : R) → S) a : S) (1 : S) ↔ LT.lt.{u_2} (α := S) ((w : (a : R) → S) a : S) (1 : S)
⊢ v.IsEquiv w

Tactic:
refine isEquiv_iff_lt_one_iff.2 fun a ↦ ?_

Premises used: Iff.mpr, AbsoluteValue.isEquiv_iff_lt_one_iff
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
Goal:
R : Type u_1
S : Type u_2
inst : Field R
inst_1 : Semifield S
inst_2 : LinearOrder S
v w : AbsoluteValue R S
inst_3 : IsStrictOrderedRing S
inst_4 : Archimedean S
inst_5 : ExistsAddOfLE S
hv : v.IsNontrivial
h :
  ∀ (x : R),
    LT.lt.{u_2} (α := S) ((v : (a : R) → S) x : S) (1 : S) → LT.lt.{u_2} (α := S) ((w : (a : R) → S) x : S) (1 : S)
a : R
inl : LT.lt.{u_2} (α := S) ((v : (a : R) → S) 0 : S) (1 : S) ↔ LT.lt.{u_2} (α := S) ((w : (a : R) → S) 0 : S) (1 : S)
inr :
  ∀ (ha₀ : a ≠ 0),
    LT.lt.{u_2} (α := S) ((v : (a : R) → S) a : S) (1 : S) ↔ LT.lt.{u_2} (α := S) ((w : (a : R) → S) a : S) (1 : S)
⊢ LT.lt.{u_2} (α := S) ((v : (a : R) → S) a : S) (1 : S) ↔ LT.lt.{u_2} (α := S) ((w : (a : R) → S) a : S) (1 : S)

Tactic:
rcases eq_or_ne a 0 with (rfl | ha₀)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
Goal:
R : Type u_1
S : Type u_2
inst : Field R
inst_1 : Semifield S
inst_2 : LinearOrder S
v w : AbsoluteValue R S
inst_3 : IsStrictOrderedRing S
inst_4 : Archimedean S
inst_5 : ExistsAddOfLE S
hv : v.IsNontrivial
h :
  ∀ (x : R),
    LT.lt.{u_2} (α := S) ((v : (a : R) → S) x : S) (1 : S) → LT.lt.{u_2} (α := S) ((w : (a : R) → S) x : S) (1 : S)
⊢ LT.lt.{u_2} (α := S) ((v : (a : R) → S) 0 : S) (1 : S) ↔ LT.lt.{u_2} (α := S) ((w : (a : R) → S) 0 : S) (1 : S)

Tactic:
simp
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
Goal:
R : Type u_1
S : Type u_2
inst : Field R
inst_1 : Semifield S
inst_2 : LinearOrder S
v w : AbsoluteValue R S
inst_3 : IsStrictOrderedRing S
inst_4 : Archimedean S
inst_5 : ExistsAddOfLE S
hv : v.IsNontrivial
h :
  ∀ (x : R),
    LT.lt.{u_2} (α := S) ((v : (a : R) → S) x : S) (1 : S) → LT.lt.{u_2} (α := S) ((w : (a : R) → S) x : S) (1 : S)
a : R
ha₀ : a ≠ 0
⊢ LT.lt.{u_2} (α := S) ((v : (a : R) → S) a : S) (1 : S) ↔ LT.lt.{u_2} (α := S) ((w : (a : R) → S) a : S) (1 : S)

Tactic:
⟨h a, fun hw ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
Goal:
R : Type u_1
S : Type u_2
inst : Field R
inst_1 : Semifield S
inst_2 : LinearOrder S
v w : AbsoluteValue R S
inst_3 : IsStrictOrderedRing S
inst_4 : Archimedean S
inst_5 : ExistsAddOfLE S
hv : v.IsNontrivial
h :
  ∀ (x : R),
    LT.lt.{u_2} (α := S) ((v : (a : R) → S) x : S) (1 : S) → LT.lt.{u_2} (α := S) ((w : (a : R) → S) x : S) (1 : S)
a : R
ha₀ : a ≠ 0
inr :
  ∀ (hw : LT.lt.{u_2} (α := S) ((w : (a : R) → S) a : S) (1 : S)),
    LT.lt.{u_2} (α := S) ((v : (a : R) → S) a : S) (1 : S)
⊢ LT.lt.{u_2} (α := S) ((v : (a : R) → S) a : S) (1 : S) ↔ LT.lt.{u_2} (α := S) ((w : (a : R) → S) a : S) (1 : S)

Tactic:
refine ⟨h a, fun hw ↦ ?_⟩
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
Goal:
R : Type u_1
S : Type u_2
inst : Field R
inst_1 : Semifield S
inst_2 : LinearOrder S
v w : AbsoluteValue R S
inst_3 : IsStrictOrderedRing S
inst_4 : Archimedean S
inst_5 : ExistsAddOfLE S
hv : v.IsNontrivial
h :
  ∀ (x : R),
    LT.lt.{u_2} (α := S) ((v : (a : R) → S) x : S) (1 : S) → LT.lt.{u_2} (α := S) ((w : (a : R) → S) x : S) (1 : S)
a : R
ha₀ : a ≠ 0
hw : LT.lt.{u_2} (α := S) ((w : (a : R) → S) a : S) (1 : S)
inr :
  ∀ (x₀ : R) (hx₀ : x₀ ≠ 0 ∧ LT.lt.{u_2} (α := S) ((v : (a : R) → S) x₀ : S) (1 : S)),
    LT.lt.{u_2} (α := S) ((v : (a : R) → S) a : S) (1 : S)
⊢ LT.lt.{u_2} (α := S) ((v : (a : R) → S) a : S) (1 : S)

Tactic:
let ⟨x₀, hx₀⟩ := hv.exists_abv_lt_one
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
Goal:
R : Type u_1
S : Type u_2
inst : Field R
inst_1 : Semifield S
inst_2 : LinearOrder S
v w : AbsoluteValue R S
inst_3 : IsStrictOrderedRing S
inst_4 : Archimedean S
inst_5 : ExistsAddOfLE S
hv_1 : v.IsNontrivial
h :
  ∀ (x : R),
    LT.lt.{u_2} (α := S) ((v : (a : R) → S) x : S) (1 : S) → LT.lt.{u_2} (α := S) ((w : (a : R) → S) x : S) (1 : S)
a : R
ha₀ : a ≠ 0
hw : LT.lt.{u_2} (α := S) ((w : (a : R) → S) a : S) (1 : S)
x₀ : R
hx₀ : x₀ ≠ 0 ∧ LT.lt.{u_2} (α := S) ((v : (a : R) → S) x₀ : S) (1 : S)
n : ℕ
hv : LE.le.{u_2} (α := S) (1 : S) ((v : (a : R) → S) a : S)
⊢ LT.lt.{u_2} (α := S) (0 : S) ((w : (a : R) → S) a : S)

Tactic:
simp_all
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
Goal:
R : Type u_1
S : Type u_2
inst : Field R
inst_1 : Semifield S
inst_2 : LinearOrder S
v w : AbsoluteValue R S
inst_3 : IsStrictOrderedRing S
inst_4 : Archimedean S
inst_5 : ExistsAddOfLE S
hv_1 : v.IsNontrivial
h :
  ∀ (x : R),
    LT.lt.{u_2} (α := S) ((v : (a : R) → S) x : S) (1 : S) → LT.lt.{u_2} (α := S) ((w : (a : R) → S) x : S) (1 : S)
a : R
ha₀ : a ≠ 0
hw : LT.lt.{u_2} (α := S) ((w : (a : R) → S) a : S) (1 : S)
x₀ : R
hx₀ : x₀ ≠ 0 ∧ LT.lt.{u_2} (α := S) ((v : (a : R) → S) x₀ : S) (1 : S)
n : ℕ
hv : LE.le.{u_2} (α := S) (1 : S) ((v : (a : R) → S) a : S)
rw : LT.lt.{u_2} (α := S) ((w : (a : R) → S) (x₀ * (a ^ n)⁻¹) : S) (1 : S)
⊢ (w : (a : R) → S) x₀ < HPow.hPow (α := S) ((w : (a : R) → S) a : S) n

Tactic:
rw [← one_mul (_ ^ _), ← mul_inv_lt_iff₀ (pow_pos (by simp_all) _),
      ← map_pow, ← map_inv₀, ← map_mul]

Premises used: pow_pos, mul_inv_lt_iff₀, map_inv₀, map_pow, map_mul, HPow.hPow, one_mul
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
Goal:
R : Type u_1
S : Type u_2
inst : Field R
inst_1 : Semifield S
inst_2 : LinearOrder S
v w : AbsoluteValue R S
inst_3 : IsStrictOrderedRing S
inst_4 : Archimedean S
inst_5 : ExistsAddOfLE S
hv_1 : v.IsNontrivial
h :
  ∀ (x : R),
    LT.lt.{u_2} (α := S) ((v : (a : R) → S) x : S) (1 : S) → LT.lt.{u_2} (α := S) ((w : (a : R) → S) x : S) (1 : S)
a : R
ha₀ : a ≠ 0
hw : LT.lt.{u_2} (α := S) ((w : (a : R) → S) a : S) (1 : S)
x₀ : R
hx₀ : x₀ ≠ 0 ∧ LT.lt.{u_2} (α := S) ((v : (a : R) → S) x₀ : S) (1 : S)
n : ℕ
hv : LE.le.{u_2} (α := S) (1 : S) ((v : (a : R) → S) a : S)
a₁ : LT.lt.{u_2} (α := S) ((v : (a : R) → S) (x₀ * (a ^ n)⁻¹) : S) (1 : S)
⊢ LT.lt.{u_2} (α := S) ((w : (a : R) → S) (x₀ * (a ^ n)⁻¹) : S) (1 : S)

Tactic:
apply h
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
Goal:
R : Type u_1
S : Type u_2
inst : Field R
inst_1 : Semifield S
inst_2 : LinearOrder S
v w : AbsoluteValue R S
inst_3 : IsStrictOrderedRing S
inst_4 : Archimedean S
inst_5 : ExistsAddOfLE S
hv_1 : v.IsNontrivial
h :
  ∀ (x : R),
    LT.lt.{u_2} (α := S) ((v : (a : R) → S) x : S) (1 : S) → LT.lt.{u_2} (α := S) ((w : (a : R) → S) x : S) (1 : S)
a : R
ha₀ : a ≠ 0
hw : LT.lt.{u_2} (α := S) ((w : (a : R) → S) a : S) (1 : S)
x₀ : R
hx₀ : x₀ ≠ 0 ∧ LT.lt.{u_2} (α := S) ((v : (a : R) → S) x₀ : S) (1 : S)
n : ℕ
hv : LE.le.{u_2} (α := S) (1 : S) ((v : (a : R) → S) a : S)
⊢ LT.lt.{u_2} (α := S) (0 : S) ((v : (a : R) → S) a : S)

Tactic:
simp [ha₀]
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
Goal:
R : Type u_1
S : Type u_2
inst : Field R
inst_1 : Semifield S
inst_2 : LinearOrder S
v w : AbsoluteValue R S
inst_3 : IsStrictOrderedRing S
inst_4 : Archimedean S
inst_5 : ExistsAddOfLE S
hv_1 : v.IsNontrivial
h :
  ∀ (x : R),
    LT.lt.{u_2} (α := S) ((v : (a : R) → S) x : S) (1 : S) → LT.lt.{u_2} (α := S) ((w : (a : R) → S) x : S) (1 : S)
a : R
ha₀ : a ≠ 0
hw : LT.lt.{u_2} (α := S) ((w : (a : R) → S) a : S) (1 : S)
x₀ : R
hx₀ : x₀ ≠ 0 ∧ LT.lt.{u_2} (α := S) ((v : (a : R) → S) x₀ : S) (1 : S)
n : ℕ
hv : LE.le.{u_2} (α := S) (1 : S) ((v : (a : R) → S) a : S)
a₁ : (v : (a : R) → S) x₀ < HPow.hPow (α := S) ((v : (a : R) → S) a : S) n
⊢ LT.lt.{u_2} (α := S) ((v : (a : R) → S) (x₀ * (a ^ n)⁻¹) : S) (1 : S)

Tactic:
rw [map_mul, map_inv₀, map_pow, mul_inv_lt_iff₀ (pow_pos (by simp [ha₀]) _), one_mul]

Premises used: pow_pos, mul_inv_lt_iff₀, map_inv₀, map_pow, map_mul, one_mul
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
Goal:
R : Type u_1
S : Type u_2
inst : Field R
inst_1 : Semifield S
inst_2 : LinearOrder S
v w : AbsoluteValue R S
inst_3 : IsStrictOrderedRing S
inst_4 : Archimedean S
inst_5 : ExistsAddOfLE S
hv_1 : v.IsNontrivial
h :
  ∀ (x : R),
    LT.lt.{u_2} (α := S) ((v : (a : R) → S) x : S) (1 : S) → LT.lt.{u_2} (α := S) ((w : (a : R) → S) x : S) (1 : S)
a : R
ha₀ : a ≠ 0
hw : LT.lt.{u_2} (α := S) ((w : (a : R) → S) a : S) (1 : S)
x₀ : R
hx₀ : x₀ ≠ 0 ∧ LT.lt.{u_2} (α := S) ((v : (a : R) → S) x₀ : S) (1 : S)
n : ℕ
hv : LE.le.{u_2} (α := S) (1 : S) ((v : (a : R) → S) a : S)
⊢ (v : (a : R) → S) x₀ < HPow.hPow (α := S) ((v : (a : R) → S) a : S) n

Tactic:
lt_of_lt_of_le hx₀.2 <| one_le_pow₀ hv

Premises used: one_le_pow₀, And.right, lt_of_lt_of_le
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
Goal:
R : Type u_1
S : Type u_2
inst : Field R
inst_1 : Semifield S
inst_2 : LinearOrder S
v w : AbsoluteValue R S
inst_3 : IsStrictOrderedRing S
inst_4 : Archimedean S
inst_5 : ExistsAddOfLE S
hv_1 : v.IsNontrivial
h :
  ∀ (x : R),
    LT.lt.{u_2} (α := S) ((v : (a : R) → S) x : S) (1 : S) → LT.lt.{u_2} (α := S) ((w : (a : R) → S) x : S) (1 : S)
a : R
ha₀ : a ≠ 0
hw : LT.lt.{u_2} (α := S) ((w : (a : R) → S) a : S) (1 : S)
x₀ : R
hx₀ : x₀ ≠ 0 ∧ LT.lt.{u_2} (α := S) ((v : (a : R) → S) x₀ : S) (1 : S)
n : ℕ
hv : LE.le.{u_2} (α := S) (1 : S) ((v : (a : R) → S) a : S)
⊢ (v : (a : R) → S) x₀ < HPow.hPow (α := S) ((v : (a : R) → S) a : S) n

Tactic:
exact lt_of_lt_of_le hx₀.2 <| one_le_pow₀ hv

Premises used: one_le_pow₀, And.right, lt_of_lt_of_le
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
Goal:
R : Type u_1
S : Type u_2
inst : Field R
inst_1 : Semifield S
inst_2 : LinearOrder S
v w : AbsoluteValue R S
inst_3 : IsStrictOrderedRing S
inst_4 : Archimedean S
inst_5 : ExistsAddOfLE S
hv : v.IsNontrivial
h :
  ∀ (x : R),
    LT.lt.{u_2} (α := S) ((v : (a : R) → S) x : S) (1 : S) → LT.lt.{u_2} (α := S) ((w : (a : R) → S) x : S) (1 : S)
a : R
ha₀ : a ≠ 0
hw : LT.lt.{u_2} (α := S) ((w : (a : R) → S) a : S) (1 : S)
x₀ : R
hx₀ : x₀ ≠ 0 ∧ LT.lt.{u_2} (α := S) ((v : (a : R) → S) x₀ : S) (1 : S)
⊢ ∀ (n : ℕ) (hv : LE.le.{u_2} (α := S) (1 : S) ((v : (a : R) → S) a : S)),
    (w : (a : R) → S) x₀ < HPow.hPow (α := S) ((w : (a : R) → S) a : S) n

Tactic:
have hpow (n : ℕ) (hv : 1 ≤ v a) : w x₀ < w a ^ n := by
    rw [← one_mul (_ ^ _), ← mul_inv_lt_iff₀ (pow_pos (by simp_all) _),
      ← map_pow, ← map_inv₀, ← map_mul]
    apply h
    rw [map_mul, map_inv₀, map_pow, mul_inv_lt_iff₀ (pow_pos (by simp [ha₀]) _), one_mul]
    exact lt_of_lt_of_le hx₀.2 <| one_le_pow₀ hv
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
Goal:
R : Type u_1
S : Type u_2
inst : Field R
inst_1 : Semifield S
inst_2 : LinearOrder S
v w : AbsoluteValue R S
inst_3 : IsStrictOrderedRing S
inst_4 : Archimedean S
inst_5 : ExistsAddOfLE S
hv : v.IsNontrivial
h :
  ∀ (x : R),
    LT.lt.{u_2} (α := S) ((v : (a : R) → S) x : S) (1 : S) → LT.lt.{u_2} (α := S) ((w : (a : R) → S) x : S) (1 : S)
a : R
ha₀ : a ≠ 0
hw : LT.lt.{u_2} (α := S) ((w : (a : R) → S) a : S) (1 : S)
x₀ : R
hx₀ : x₀ ≠ 0 ∧ LT.lt.{u_2} (α := S) ((v : (a : R) → S) x₀ : S) (1 : S)
hpow :
  ∀ (n : ℕ) (hv : LE.le.{u_2} (α := S) (1 : S) ((v : (a : R) → S) a : S)),
    (w : (a : R) → S) x₀ < HPow.hPow (α := S) ((w : (a : R) → S) a : S) n
inr :
  ∀ (n : ℕ) (hn : HPow.hPow (α := S) ((w : (a : R) → S) a : S) n < (w : (a : R) → S) x₀),
    LT.lt.{u_2} (α := S) ((v : (a : R) → S) a : S) (1 : S)
⊢ LT.lt.{u_2} (α := S) ((v : (a : R) → S) a : S) (1 : S)

Tactic:
obtain ⟨n, hn⟩ := exists_pow_lt_of_lt_one (w.pos hx₀.1) hw

Premises used: exists_pow_lt_of_lt_one, AbsoluteValue.pos, And.left
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
Goal:
R : Type u_1
S : Type u_2
inst : Field R
inst_1 : Semifield S
inst_2 : LinearOrder S
v w : AbsoluteValue R S
inst_3 : IsStrictOrderedRing S
inst_4 : Archimedean S
inst_5 : ExistsAddOfLE S
hv : v.IsNontrivial
h :
  ∀ (x : R),
    LT.lt.{u_2} (α := S) ((v : (a : R) → S) x : S) (1 : S) → LT.lt.{u_2} (α := S) ((w : (a : R) → S) x : S) (1 : S)
a : R
ha₀ : a ≠ 0
hw : LT.lt.{u_2} (α := S) ((w : (a : R) → S) a : S) (1 : S)
x₀ : R
hx₀ : x₀ ≠ 0 ∧ LT.lt.{u_2} (α := S) ((v : (a : R) → S) x₀ : S) (1 : S)
hpow :
  ∀ (n : ℕ) (hv : LE.le.{u_2} (α := S) (1 : S) ((v : (a : R) → S) a : S)),
    (w : (a : R) → S) x₀ < HPow.hPow (α := S) ((w : (a : R) → S) a : S) n
n : ℕ
hn : HPow.hPow (α := S) ((w : (a : R) → S) a : S) n < (w : (a : R) → S) x₀
⊢ LT.lt.{u_2} (α := S) ((v : (a : R) → S) a : S) (1 : S)

Tactic:
not_le.1 <| mt (hpow n) <| not_lt.2 hn.le

Premises used: not_le, Iff.mpr, mt, LT.lt.le, not_lt, Iff.mp
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
Goal:
R : Type u_1
S : Type u_2
inst : Field R
inst_1 : Semifield S
inst_2 : LinearOrder S
v w : AbsoluteValue R S
inst_3 : IsStrictOrderedRing S
inst_4 : Archimedean S
inst_5 : ExistsAddOfLE S
hv : v.IsNontrivial
h :
  ∀ (x : R),
    LT.lt.{u_2} (α := S) ((v : (a : R) → S) x : S) (1 : S) → LT.lt.{u_2} (α := S) ((w : (a : R) → S) x : S) (1 : S)
a : R
ha₀ : a ≠ 0
hw : LT.lt.{u_2} (α := S) ((w : (a : R) → S) a : S) (1 : S)
x₀ : R
hx₀ : x₀ ≠ 0 ∧ LT.lt.{u_2} (α := S) ((v : (a : R) → S) x₀ : S) (1 : S)
hpow :
  ∀ (n : ℕ) (hv : LE.le.{u_2} (α := S) (1 : S) ((v : (a : R) → S) a : S)),
    (w : (a : R) → S) x₀ < HPow.hPow (α := S) ((w : (a : R) → S) a : S) n
n : ℕ
hn : HPow.hPow (α := S) ((w : (a : R) → S) a : S) n < (w : (a : R) → S) x₀
⊢ LT.lt.{u_2} (α := S) ((v : (a : R) → S) a : S) (1 : S)

Tactic:
exact not_le.1 <| mt (hpow n) <| not_lt.2 hn.le

Premises used: not_le, Iff.mpr, mt, LT.lt.le, not_lt, Iff.mp
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
Goal:
R : Type u_1
S : Type u_2
inst : Field R
inst_1 : Semifield S
inst_2 : LinearOrder S
inst_3 : IsStrictOrderedRing S
inst_4 : Archimedean S
inst_5 : ExistsAddOfLE S
v w : AbsoluteValue R S
hv : v.IsNontrivial
h : ¬v.IsEquiv w
contrapose! :
  ∀
    (h :
      ∀ (a : R) (_ : LT.lt.{u_2} (α := S) ((v : (a : R) → S) a : S) (1 : S)),
        LT.lt.{u_2} (α := S) ((w : (a : R) → S) a : S) (1 : S)),
    v.IsEquiv w
⊢ ∃ (a : R),
    LT.lt.{u_2} (α := S) ((v : (a : R) → S) a : S) (1 : S) ∧ LE.le.{u_2} (α := S) (1 : S) ((w : (a : R) → S) a : S)

Tactic:
contrapose! h
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
Goal:
R : Type u_1
S : Type u_2
inst : Field R
inst_1 : Semifield S
inst_2 : LinearOrder S
inst_3 : IsStrictOrderedRing S
inst_4 : Archimedean S
inst_5 : ExistsAddOfLE S
v w : AbsoluteValue R S
hv : v.IsNontrivial
h :
  ∀ (a : R) (_ : LT.lt.{u_2} (α := S) ((v : (a : R) → S) a : S) (1 : S)),
    LT.lt.{u_2} (α := S) ((w : (a : R) → S) a : S) (1 : S)
⊢ v.IsEquiv w

Tactic:
isEquiv_of_lt_one_imp hv h

Premises used: AbsoluteValue.isEquiv_of_lt_one_imp
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
Goal:
R : Type u_1
S : Type u_2
inst : Field R
inst_1 : Semifield S
inst_2 : LinearOrder S
inst_3 : IsStrictOrderedRing S
inst_4 : Archimedean S
inst_5 : ExistsAddOfLE S
v w : AbsoluteValue R S
hv : v.IsNontrivial
h :
  ∀ (a : R) (_ : LT.lt.{u_2} (α := S) ((v : (a : R) → S) a : S) (1 : S)),
    LT.lt.{u_2} (α := S) ((w : (a : R) → S) a : S) (1 : S)
⊢ v.IsEquiv w

Tactic:
exact isEquiv_of_lt_one_imp hv h

Premises used: AbsoluteValue.isEquiv_of_lt_one_imp
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
Goal:
R : Type u_1
S : Type u_2
inst : Field R
inst_1 : Semifield S
inst_2 : LinearOrder S
inst_3 : IsStrictOrderedRing S
inst_4 : Archimedean S
inst_5 : ExistsAddOfLE S
v w : AbsoluteValue R S
hv : v.IsNontrivial
hw : w.IsNontrivial
h : ¬v.IsEquiv w
let :
  ∀ (a : R) (hva : LT.lt.{u_2} (α := S) ((v : (a : R) → S) a : S) (1 : S))
    (hwa : LE.le.{u_2} (α := S) (1 : S) ((w : (a : R) → S) a : S)),
    ∃ (a : R),
      LT.lt.{u_2} (α := S) (1 : S) ((v : (a : R) → S) a : S) ∧ LT.lt.{u_2} (α := S) ((w : (a : R) → S) a : S) (1 : S)
⊢ ∃ (a : R),
    LT.lt.{u_2} (α := S) (1 : S) ((v : (a : R) → S) a : S) ∧ LT.lt.{u_2} (α := S) ((w : (a : R) → S) a : S) (1 : S)

Tactic:
let ⟨a, hva, hwa⟩ := exists_lt_one_one_le_of_not_isEquiv hv h