awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
Goal:
K : Type u_4
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : Archimedean K
n : ℕ
hn : n ≠ 0
x y : K
h : x < y
hy : 0 < y
q₂ : ℚ
hx₂ : max x 0 < (↑q₂ : K)
hy₂ : (↑q₂ : K) < y
q₁ : ℚ
hx₁ : max x 0 < (↑q₁ : K)
hq₁₂ : q₁ < q₂
this : 0 < q₂
q : ℚ
hq : 0 < q
hq₁ : q₁ < q ^ n
hq₂ : q ^ n < q₂
refine_1 : (↑q₁ : K) < HPow.hPow (α := K) (↑q : K) n
⊢ ∃ (q : ℚ), 0 < q ∧ x < HPow.hPow (α := K) (↑q : K) n ∧ HPow.hPow (α := K) (↑q : K) n < y
have refine_2 : HPow.hPow (α := K) (↑q : K) n < (↑q₂ : K)
Tactic: refine ⟨q, hq, (le_max_left _ _).trans_lt <| hx₁.trans ?_, hy₂.trans' ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
Goal:
K : Type u_4
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : Archimedean K
n : ℕ
hn : n ≠ 0
x y : K
h : x < y
hy : 0 < y
q₂ : ℚ
hx₂ : max x 0 < (↑q₂ : K)
hy₂ : (↑q₂ : K) < y
q₁ : ℚ
hx₁ : max x 0 < (↑q₁ : K)
hq₁₂ : q₁ < q₂
this : 0 < q₂
q : ℚ
hq : 0 < q
hq₁ : q₁ < q ^ n
hq₂ : q ^ n < q₂
⊢ (↑q₁ : K) < HPow.hPow (α := K) (↑q : K) n
have refine_1 : ∀ (hy : 0 < y) (hx₂ : max x 0 < (↑q₂ : K)) (hx₁ : max x 0 < (↑q₁ : K)) (hq : 0 < q), q₁ < q ^ n
Tactic: assumption_mod_cast
Cleared hypotheses: hy, hx₂, hx₁, hq
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
Goal:
K : Type u_4
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : Archimedean K
n : ℕ
hn : n ≠ 0
x y : K
h : x < y
hy : 0 < y
q₂ : ℚ
hx₂ : max x 0 < (↑q₂ : K)
hy₂ : (↑q₂ : K) < y
q₁ : ℚ
hx₁ : max x 0 < (↑q₁ : K)
hq₁₂ : q₁ < q₂
this : 0 < q₂
q : ℚ
hq : 0 < q
hq₁ : q₁ < q ^ n
hq₂ : q ^ n < q₂
⊢ HPow.hPow (α := K) (↑q : K) n < (↑q₂ : K)
have refine_2 : ∀ (hy : 0 < y) (hx₂ : max x 0 < (↑q₂ : K)) (hx₁ : max x 0 < (↑q₁ : K)) (hq : 0 < q), q ^ n < q₂
Tactic: assumption_mod_cast
Cleared hypotheses: hy, hx₂, hx₁, hq
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
Goal:
G : Type u_1
M : Type u_2
R : Type u_3
K_1 : Type u_4
K : Type u_5
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
⊢ Archimedean K
have rw : ∀ (x : K), ∃ (n : ℤ), x ≤ (↑n : K)
Tactic: rw [archimedean_iff_int_le]
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
Goal:
G : Type u_1
M_1 : Type u_2
R : Type u_3
K : Type u_4
M : Type u_5
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : Archimedean M
⊢ Archimedean.{u_5} (WithBot M)
have arch : ∀ (x : WithBot M) {y : WithBot M}, 0 < y → ∃ (n : ℕ), x ≤ n • y
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
Goal:
G : Type u_1
M_1 : Type u_2
R : Type u_3
K : Type u_4
M : Type u_5
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : Archimedean M
x : WithBot M
y : M
hxy : 0 < (↑y : WithBot M)
⊢ ∃ (n : ℕ), x ≤ n • (↑y : WithBot M)
have arch : ∃ (n : ℕ), ⊥ ≤ n • (↑y : WithBot M)
Tactic: cases x with
    | bot => refine ⟨0, bot_le⟩
    | coe x => simpa [← WithBot.coe_nsmul] using (Archimedean.arch x (by simpa using hxy))
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
Goal:
G : Type u_1
M_1 : Type u_2
R : Type u_3
K : Type u_4
M : Type u_5
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : Archimedean M
x : WithBot M
y : M
hxy : 0 < (↑y : WithBot M)
arch : ∃ (n : ℕ), ⊥ ≤ n • (↑y : WithBot M)
⊢ ∃ (n : ℕ), x ≤ n • (↑y : WithBot M)
have arch₁ : ∀ (x : M), ∃ (n : ℕ), (↑x : WithBot M) ≤ n • (↑y : WithBot M)
Tactic: cases x with
    | bot => refine ⟨0, bot_le⟩
    | coe x => simpa [← WithBot.coe_nsmul] using (Archimedean.arch x (by simpa using hxy))
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
Goal:
G : Type u_1
M_1 : Type u_2
R : Type u_3
K : Type u_4
M : Type u_5
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : Archimedean M
x y : WithBot M
hxy : 0 < y
⊢ ∃ (n : ℕ), x ≤ n • y
have arch : ∀ (hxy : LT.lt.{u_5} (α := WithBot M) 0 ⊥), ∃ (n : ℕ), x ≤ HSMul.hSMul (β := WithBot M) n ⊥
Tactic: cases y with
  | bot => exact absurd hxy bot_le.not_gt
  | coe y =>
    cases x with
    | bot => refine ⟨0, bot_le⟩
    | coe x => simpa [← WithBot.coe_nsmul] using (Archimedean.arch x (by simpa using hxy))
Cleared hypotheses: y, hxy
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
Goal:
G : Type u_1
M_1 : Type u_2
R : Type u_3
K : Type u_4
M : Type u_5
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : Archimedean M
x y : WithBot M
hxy : 0 < y
arch : ∀ (hxy : LT.lt.{u_5} (α := WithBot M) 0 ⊥), ∃ (n : ℕ), x ≤ HSMul.hSMul (β := WithBot M) n ⊥
⊢ ∃ (n : ℕ), x ≤ n • y
have arch₁ : ∀ (y : M) (hxy : 0 < (↑y : WithBot M)), ∃ (n : ℕ), x ≤ n • (↑y : WithBot M)
Tactic: cases y with
  | bot => exact absurd hxy bot_le.not_gt
  | coe y =>
    cases x with
    | bot => refine ⟨0, bot_le⟩
    | coe x => simpa [← WithBot.coe_nsmul] using (Archimedean.arch x (by simpa using hxy))
Cleared hypotheses: y, hxy
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
Goal:
G : Type u_1
M_1 : Type u_2
R : Type u_3
K : Type u_4
M : Type u_5
inst : CommMonoid M
inst_1 : PartialOrder M
inst_2 : MulArchimedean M
⊢ MulArchimedean.{u_5} (WithZero M)
have arch : ∀ (x : WithZero M) {y : WithZero M}, 1 < y → ∃ (n : ℕ), x ≤ y ^ n
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
Goal:
G : Type u_1
M_1 : Type u_2
R : Type u_3
K : Type u_4
M : Type u_5
inst : CommMonoid M
inst_1 : PartialOrder M
inst_2 : MulArchimedean M
x : WithZero M
y : M
hxy : 1 < (↑y : WithZero M)
⊢ ∃ (n : ℕ), x ≤ (↑y : WithZero M) ^ n
have arch : ∃ (n : ℕ), 0 ≤ (↑y : WithZero M) ^ n
Tactic: cases x with
    | zero => refine ⟨0, zero_le⟩
    | coe x => simpa [← WithZero.coe_pow] using (MulArchimedean.arch x (by simpa using hxy))
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
Goal:
G : Type u_1
M_1 : Type u_2
R : Type u_3
K : Type u_4
M : Type u_5
inst : CommMonoid M
inst_1 : PartialOrder M
inst_2 : MulArchimedean M
x : WithZero M
y : M
hxy : 1 < (↑y : WithZero M)
arch : ∃ (n : ℕ), 0 ≤ (↑y : WithZero M) ^ n
⊢ ∃ (n : ℕ), x ≤ (↑y : WithZero M) ^ n
have arch₁ : ∀ (x : M), ∃ (n : ℕ), (↑x : WithZero M) ≤ (↑y : WithZero M) ^ n
Tactic: cases x with
    | zero => refine ⟨0, zero_le⟩
    | coe x => simpa [← WithZero.coe_pow] using (MulArchimedean.arch x (by simpa using hxy))
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
Goal:
G : Type u_1
M_1 : Type u_2
R : Type u_3
K : Type u_4
M : Type u_5
inst : CommMonoid M
inst_1 : PartialOrder M
inst_2 : MulArchimedean M
x y : WithZero M
hxy : 1 < y
⊢ ∃ (n : ℕ), x ≤ y ^ n
have arch : ∀ (hxy : LT.lt.{u_5} (α := WithZero M) 1 0), ∃ (n : ℕ), x ≤ HPow.hPow (α := WithZero M) 0 n
Tactic: cases y with
  | zero => cases hxy.pos.false
  | coe y =>
    cases x with
    | zero => refine ⟨0, zero_le⟩
    | coe x => simpa [← WithZero.coe_pow] using (MulArchimedean.arch x (by simpa using hxy))
Cleared hypotheses: y, hxy
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
Goal:
G : Type u_1
M_1 : Type u_2
R : Type u_3
K : Type u_4
M : Type u_5
inst : CommMonoid M
inst_1 : PartialOrder M
inst_2 : MulArchimedean M
x y : WithZero M
hxy : 1 < y
arch : ∀ (hxy : LT.lt.{u_5} (α := WithZero M) 1 0), ∃ (n : ℕ), x ≤ HPow.hPow (α := WithZero M) 0 n
⊢ ∃ (n : ℕ), x ≤ y ^ n
have arch₁ : ∀ (y : M) (hxy : 1 < (↑y : WithZero M)), ∃ (n : ℕ), x ≤ (↑y : WithZero M) ^ n
Tactic: cases y with
  | zero => cases hxy.pos.false
  | coe y =>
    cases x with
    | zero => refine ⟨0, zero_le⟩
    | coe x => simpa [← WithZero.coe_pow] using (MulArchimedean.arch x (by simpa using hxy))
Cleared hypotheses: y, hxy
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (goal)
Goal:
M_1 : Type u_1
inst : Group M_1
inst_1 : Lattice M_1
M : Type u_2
inst_2 : CommGroup M
inst_3 : LinearOrder M
inst_4 : IsOrderedMonoid M
a_1 b_1 : M
a b c : MulArchimedeanOrder M
m : ℕ
hm :
  |(val : (a : MulArchimedeanOrder M) → M) b|ₘ ≤ HPow.hPow (α := M) (|(val : (a : MulArchimedeanOrder M) → M) a|ₘ : M) m
⊢ b ≤ c → a ≤ c
have this : ∀ (n : ℕ)
  (hn :
    |(val : (a : MulArchimedeanOrder M) → M) c|ₘ ≤
      HPow.hPow (α := M) (|(val : (a : MulArchimedeanOrder M) → M) b|ₘ : M) n),
  a ≤ c
Tactic: ⟨n, hn⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (goal)
Goal:
M_1 : Type u_1
inst : Group M_1
inst_1 : Lattice M_1
M : Type u_2
inst_2 : CommGroup M
inst_3 : LinearOrder M
inst_4 : IsOrderedMonoid M
a_1 b_1 : M
a b c : MulArchimedeanOrder M
m : ℕ
hm :
  |(val : (a : MulArchimedeanOrder M) → M) b|ₘ ≤ HPow.hPow (α := M) (|(val : (a : MulArchimedeanOrder M) → M) a|ₘ : M) m
n : ℕ
hn :
  |(val : (a : MulArchimedeanOrder M) → M) c|ₘ ≤ HPow.hPow (α := M) (|(val : (a : MulArchimedeanOrder M) → M) b|ₘ : M) n
⊢ a ≤ c
have h : |(val : (a : MulArchimedeanOrder M) → M) c|ₘ ≤
  HPow.hPow (α := M) (|(val : (a : MulArchimedeanOrder M) → M) a|ₘ : M) (m * n)
Tactic: use m * n
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (goal)
Goal:
M_1 : Type u_1
inst : Group M_1
inst_1 : Lattice M_1
M : Type u_2
inst_2 : CommGroup M
inst_3 : LinearOrder M
inst_4 : IsOrderedMonoid M
a_1 b_1 : M
a b c : MulArchimedeanOrder M
m : ℕ
hm :
  |(val : (a : MulArchimedeanOrder M) → M) b|ₘ ≤ HPow.hPow (α := M) (|(val : (a : MulArchimedeanOrder M) → M) a|ₘ : M) m
n : ℕ
hn :
  |(val : (a : MulArchimedeanOrder M) → M) c|ₘ ≤ HPow.hPow (α := M) (|(val : (a : MulArchimedeanOrder M) → M) b|ₘ : M) n
⊢ |(val : (a : MulArchimedeanOrder M) → M) c|ₘ ≤
    HPow.hPow (α := M) (|(val : (a : MulArchimedeanOrder M) → M) a|ₘ : M) (m * n)
have h : |(val : (a : MulArchimedeanOrder M) → M) c|ₘ ≤
  HPow.hPow (α := M) (|(val : (a : MulArchimedeanOrder M) → M) a|ₘ : M) m ^ n
Tactic: rw [pow_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (goal)
Goal:
M_1 : Type u_1
inst : Group M_1
inst_1 : Lattice M_1
M : Type u_2
inst_2 : CommGroup M
inst_3 : LinearOrder M
inst_4 : IsOrderedMonoid M
a_1 b_1 : M
a b : MulArchimedeanOrder M
⊢ (∀ (n : ℕ),
      HPow.hPow (α := M) (|(val : (a : MulArchimedeanOrder M) → M) b|ₘ : M) n <
        |(val : (a : MulArchimedeanOrder M) → M) a|ₘ) ↔
    (∃ (n : ℕ),
        |(val : (a : MulArchimedeanOrder M) → M) b|ₘ ≤
          HPow.hPow (α := M) (|(val : (a : MulArchimedeanOrder M) → M) a|ₘ : M) n) ∧
      ¬∃ (n : ℕ),
          |(val : (a : MulArchimedeanOrder M) → M) a|ₘ ≤
            HPow.hPow (α := M) (|(val : (a : MulArchimedeanOrder M) → M) b|ₘ : M) n
have suffices : (∀ (n : ℕ),
    HPow.hPow (α := M) (|(val : (a : MulArchimedeanOrder M) → M) b|ₘ : M) n <
      |(val : (a : MulArchimedeanOrder M) → M) a|ₘ) →
  ∃ (n : ℕ),
    |(val : (a : MulArchimedeanOrder M) → M) b|ₘ ≤
      HPow.hPow (α := M) (|(val : (a : MulArchimedeanOrder M) → M) a|ₘ : M) n
Tactic: suffices (∀ (n : ℕ), |b.val|ₘ ^ n < |a.val|ₘ) → ∃ n, |b.val|ₘ ≤ |a.val|ₘ ^ n by
      simpa using this
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (hypothesis)
Goal:
M_1 : Type u_1
inst : Group M_1
inst_1 : Lattice M_1
M : Type u_2
inst_2 : CommGroup M
inst_3 : LinearOrder M
inst_4 : IsOrderedMonoid M
a_1 b_1 : M
a b : MulArchimedeanOrder M
h :
  ∀ (n : ℕ),
    HPow.hPow (α := M) (|(val : (a : MulArchimedeanOrder M) → M) b|ₘ : M) n <
      |(val : (a : MulArchimedeanOrder M) → M) a|ₘ
⊢ ∃ (n : ℕ),
    |(val : (a : MulArchimedeanOrder M) → M) b|ₘ ≤
      HPow.hPow (α := M) (|(val : (a : MulArchimedeanOrder M) → M) a|ₘ : M) n
have h₁ : HPow.hPow (α := M) (β := ℕ) (|(val : (a : MulArchimedeanOrder M) → M) b|ₘ : M) 1 ≤
  |(val : (a : MulArchimedeanOrder M) → M) a|ₘ
Tactic: obtain h := (h 1).le
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (goal)
Goal:
M_1 : Type u_1
inst : Group M_1
inst_1 : Lattice M_1
M : Type u_2
inst_2 : CommGroup M
inst_3 : LinearOrder M
inst_4 : IsOrderedMonoid M
a_1 b_1 : M
a b : MulArchimedeanOrder M
⊢ a ≤ b ∨ b ≤ a
have inl : ∀
  (hab :
    LE.le (α := M) (|(val : (a : MulArchimedeanOrder M) → M) a|ₘ : M)
      (|(val : (a : MulArchimedeanOrder M) → M) b|ₘ : M)),
  a ≤ b ∨ b ≤ a
Tactic: obtain hab | hab := le_total |a.val|ₘ |b.val|ₘ
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (goal)
Goal:
M_1 : Type u_1
inst : Group M_1
inst_1 : Lattice M_1
M : Type u_2
inst_2 : CommGroup M
inst_3 : LinearOrder M
inst_4 : IsOrderedMonoid M
a_1 b_1 : M
a b : MulArchimedeanOrder M
inl :
  ∀
    (hab :
      LE.le (α := M) (|(val : (a : MulArchimedeanOrder M) → M) a|ₘ : M)
        (|(val : (a : MulArchimedeanOrder M) → M) b|ₘ : M)),
    a ≤ b ∨ b ≤ a
⊢ a ≤ b ∨ b ≤ a
have inr : ∀
  (hab :
    LE.le (α := M) (|(val : (a : MulArchimedeanOrder M) → M) b|ₘ : M)
      (|(val : (a : MulArchimedeanOrder M) → M) a|ₘ : M)),
  a ≤ b ∨ b ≤ a
Tactic: obtain hab | hab := le_total |a.val|ₘ |b.val|ₘ
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (goal)
Goal:
M_1 : Type u_1
inst : Group M_1
inst_1 : Lattice M_1
M : Type u_2
inst_2 : CommGroup M
inst_3 : LinearOrder M
inst_4 : IsOrderedMonoid M
a_1 b_1 : M
N : Type u_3
inst_5 : CommGroup N
inst_6 : LinearOrder N
inst_7 : IsOrderedMonoid N
f : M →*o N
a b : MulArchimedeanOrder M
n : ℕ
hn :
  |(val : (a : MulArchimedeanOrder M) → M) b|ₘ ≤ HPow.hPow (α := M) (|(val : (a : MulArchimedeanOrder M) → M) a|ₘ : M) n
⊢ LE.le.{u_3} (α := MulArchimedeanOrder N)
    ((fun (a : MulArchimedeanOrder M) ↦
        ((of : (a : N) → MulArchimedeanOrder N)
            ((f : (a : M) → N) ((val : (a : MulArchimedeanOrder M) → M) a : M) : N) :
          MulArchimedeanOrder N))
      a)
    ((fun (a : MulArchimedeanOrder M) ↦
        ((of : (a : N) → MulArchimedeanOrder N)
            ((f : (a : M) → N) ((val : (a : MulArchimedeanOrder M) → M) a : M) : N) :
          MulArchimedeanOrder N))
      b)
have simp_rw : ∃ (n : ℕ),
  LE.le.{u_3} (α := N) ((f : (a : M) → N) (|(val : (a : MulArchimedeanOrder M) → M) b|ₘ : M) : N)
    ((f : (a : M) → N) (HPow.hPow (α := M) (|(val : (a : MulArchimedeanOrder M) → M) a|ₘ : M) n) : N)
Tactic: simp_rw [le_def, val_of, ← map_mabs, ← map_pow]
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (goal)
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a b : M
⊢ Eq (α := MulArchimedeanClass M)
      (⟦(MulArchimedeanOrder.of : (a : M) → MulArchimedeanOrder M) a⟧ :
        Quotient (α := MulArchimedeanOrder M)
          (AntisymmRel.setoid (MulArchimedeanOrder M) fun (x1 x2 : MulArchimedeanOrder M) ↦ x1 ≤ x2))
      (⟦(MulArchimedeanOrder.of : (a : M) → MulArchimedeanOrder M) b⟧ :
        Quotient (α := MulArchimedeanOrder M)
          (AntisymmRel.setoid (MulArchimedeanOrder M) fun (x1 x2 : MulArchimedeanOrder M) ↦ x1 ≤ x2)) ↔
    (∃ (m : ℕ), |b|ₘ ≤ |a|ₘ ^ m) ∧ ∃ (n : ℕ), |a|ₘ ≤ |b|ₘ ^ n
have rw : (AntisymmRel.setoid (MulArchimedeanOrder M) fun (x1 x2 : MulArchimedeanOrder M) ↦ x1 ≤ x2 :
      MulArchimedeanOrder M → MulArchimedeanOrder M → Prop)
    ((MulArchimedeanOrder.of : (a : M) → MulArchimedeanOrder M) a : MulArchimedeanOrder M)
    ((MulArchimedeanOrder.of : (a : M) → MulArchimedeanOrder M) b : MulArchimedeanOrder M) ↔
  (∃ (m : ℕ), |b|ₘ ≤ |a|ₘ ^ m) ∧ ∃ (n : ℕ), |a|ₘ ≤ |b|ₘ ^ n
Tactic: rw [Quotient.eq]
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (goal)
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
α : Type u_2
f : M → α
h : ∀ (a b : M), Eq (α := MulArchimedeanClass M) (mk a) (mk b) → f a = f b
a : M
⊢ lift f h (mk a) = f a
have unfold : Quotient.lift f sorry (mk a) = f a
Tactic: unfold lift
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (goal)
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
α : Type u_2
f : M → M → α
h :
  ∀ (a₁ b₁ a₂ b₂ : M),
    Eq (α := MulArchimedeanClass M) (mk a₁) (mk b₁) →
      Eq (α := MulArchimedeanClass M) (mk a₂) (mk b₂) → f a₁ a₂ = f b₁ b₂
a b : M
⊢ lift₂ f h (mk a) (mk b) = f a b
have unfold : Quotient.lift₂ f sorry (mk a) (mk b) = f a b
Tactic: unfold lift₂
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (goal)
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a b : M
⊢ Eq (α := MulArchimedeanClass M) (mk (a / b)) (mk (b / a))
have rw : Eq (α := MulArchimedeanClass M) (mk (a / b)⁻¹) (mk (b / a))
Tactic: rw [← mk_inv, inv_div]
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (goal)
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a b : M
rw : Eq (α := MulArchimedeanClass M) (mk (a / b)⁻¹) (mk (b / a))
⊢ Eq (α := MulArchimedeanClass M) (mk (a / b)) (mk (b / a))
have rw₁ : Eq (α := MulArchimedeanClass M) (mk (b / a)) (mk (b / a))
Tactic: rw [← mk_inv, inv_div]
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (goal)
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a b : M
ha : a ≠ 1
⊢ LE.le (α := MulArchimedeanClass M) (mk a) (mk b) ↔ ∃ (n : ℕ), |b|ₘ < |a|ₘ ^ n
have refine_1 : LE.le (α := MulArchimedeanClass M) (mk a) (mk b) →
  ∀ (n : ℕ)
    (hn :
      |(MulArchimedeanOrder.val : (a : MulArchimedeanOrder M) → M)
            ((MulArchimedeanOrder.of : (a : M) → MulArchimedeanOrder M) b : MulArchimedeanOrder M)|ₘ ≤
        HPow.hPow (α := M)
          (|(MulArchimedeanOrder.val : (a : MulArchimedeanOrder M) → M)
                ((MulArchimedeanOrder.of : (a : M) → MulArchimedeanOrder M) a : MulArchimedeanOrder M)|ₘ :
            M)
          n),
    HPow.hPow (α := M)
        (|(MulArchimedeanOrder.val : (a : MulArchimedeanOrder M) → M)
              ((MulArchimedeanOrder.of : (a : M) → MulArchimedeanOrder M) a : MulArchimedeanOrder M)|ₘ :
          M)
        n <
      |a|ₘ ^ (n + 1)
Tactic: refine ⟨fun ⟨n, hn⟩ ↦ ⟨n + 1, hn.trans_lt ?_⟩, fun ⟨n, hn⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (goal)
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a b : M
ha : a ≠ 1
refine_1 :
  LE.le (α := MulArchimedeanClass M) (mk a) (mk b) →
    ∀ (n : ℕ)
      (hn :
        |(MulArchimedeanOrder.val : (a : MulArchimedeanOrder M) → M)
              ((MulArchimedeanOrder.of : (a : M) → MulArchimedeanOrder M) b : MulArchimedeanOrder M)|ₘ ≤
          HPow.hPow (α := M)
            (|(MulArchimedeanOrder.val : (a : MulArchimedeanOrder M) → M)
                  ((MulArchimedeanOrder.of : (a : M) → MulArchimedeanOrder M) a : MulArchimedeanOrder M)|ₘ :
              M)
            n),
      HPow.hPow (α := M)
          (|(MulArchimedeanOrder.val : (a : MulArchimedeanOrder M) → M)
                ((MulArchimedeanOrder.of : (a : M) → MulArchimedeanOrder M) a : MulArchimedeanOrder M)|ₘ :
            M)
          n <
        |a|ₘ ^ (n + 1)
⊢ LE.le (α := MulArchimedeanClass M) (mk a) (mk b) ↔ ∃ (n : ℕ), |b|ₘ < |a|ₘ ^ n
have refine_2 : (∃ (n : ℕ), |b|ₘ < |a|ₘ ^ n) → ∀ (n : ℕ) (hn : |b|ₘ < |a|ₘ ^ n), LE.le (α := MulArchimedeanClass M) (mk a) (mk b)
Tactic: refine ⟨fun ⟨n, hn⟩ ↦ ⟨n + 1, hn.trans_lt ?_⟩, fun ⟨n, hn⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (goal)
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a b : M
ha : a ≠ 1
h : LE.le (α := MulArchimedeanClass M) (mk a) (mk b)
n : ℕ
hn :
  |(MulArchimedeanOrder.val : (a : MulArchimedeanOrder M) → M)
        ((MulArchimedeanOrder.of : (a : M) → MulArchimedeanOrder M) b : MulArchimedeanOrder M)|ₘ ≤
    HPow.hPow (α := M)
      (|(MulArchimedeanOrder.val : (a : MulArchimedeanOrder M) → M)
            ((MulArchimedeanOrder.of : (a : M) → MulArchimedeanOrder M) a : MulArchimedeanOrder M)|ₘ :
        M)
      n
⊢ HPow.hPow (α := M)
      (|(MulArchimedeanOrder.val : (a : MulArchimedeanOrder M) → M)
            ((MulArchimedeanOrder.of : (a : M) → MulArchimedeanOrder M) a : MulArchimedeanOrder M)|ₘ :
        M)
      n <
    |a|ₘ ^ (n + 1)
have refine_1 : HPow.hPow (α := M)
    (|(MulArchimedeanOrder.val : (a : MulArchimedeanOrder M) → M)
          ((MulArchimedeanOrder.of : (a : M) → MulArchimedeanOrder M) a : MulArchimedeanOrder M)|ₘ :
      M)
    n <
  |a|ₘ ^ n * |a|ₘ
Tactic: rw [pow_succ]
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (goal)
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a b : M
A : MulArchimedeanClass M
⊢ A ≤ mk 1
have mk : ∀ (a : M), LE.le (α := MulArchimedeanClass M) (mk a) (mk 1)
Tactic: induction A using ind with | mk a
Cleared hypotheses: A
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (goal)
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a_1 b a : M
⊢ LE.le (α := MulArchimedeanClass M) (mk a) (mk 1)
have mk : ∃ (n : ℕ), |1|ₘ ≤ |a|ₘ ^ n
Tactic: rw [mk_le_mk]
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (goal)
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a : M
⊢ Eq (α := MulArchimedeanClass M) ⊤ (mk a) ↔ a = 1
have rw : Eq (α := MulArchimedeanClass M) (mk a) ⊤ ↔ a = 1
Tactic: rw [eq_comm, mk_eq_top_iff]
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (goal)
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a : M
rw : Eq (α := MulArchimedeanClass M) (mk a) ⊤ ↔ a = 1
⊢ Eq (α := MulArchimedeanClass M) ⊤ (mk a) ↔ a = 1
have rw₁ : a = 1 ↔ a = 1
Tactic: rw [eq_comm, mk_eq_top_iff]
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (goal)
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
⊢ Eq.{u_1 + 1} (α := M) (out ⊤) 1
have rw : Eq.{u_1 + 1} (α := MulArchimedeanClass M) (mk (out ⊤)) ⊤
Tactic: rw [← mk_eq_top_iff, mk_out]
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (goal)
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
rw : Eq.{u_1 + 1} (α := MulArchimedeanClass M) (mk (out ⊤)) ⊤
⊢ Eq.{u_1 + 1} (α := M) (out ⊤) 1
have rw₁ : Eq.{u_1 + 1} (α := MulArchimedeanClass M) ⊤ ⊤
Tactic: rw [← mk_eq_top_iff, mk_out]
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (goal)
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a b : M
inst_3 : Nontrivial M
⊢ ∃ (x : MulArchimedeanClass M) (y : MulArchimedeanClass M), x ≠ y
have obtain : ∀ (x : M) (hx : x ≠ 1), ∃ (x : MulArchimedeanClass M) (y : MulArchimedeanClass M), x ≠ y
Tactic: obtain ⟨x, hx⟩ := exists_ne (1 : M)
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (goal)
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a : M
ha : Membership.mem (γ := Set M) (Set.Ici 1) a
b : M
hb : Membership.mem (γ := Set M) (Set.Ici 1) b
hab : a ≤ b
⊢ LE.le (α := MulArchimedeanClass M) (mk b) (mk a)
have contrapose! : ∀ (hab : LT.lt (α := MulArchimedeanClass M) (mk a) (mk b)), b < a
Tactic: contrapose! hab
Cleared hypotheses: hab
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (hypothesis)
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a : M
ha : Membership.mem (γ := Set M) (Set.Ici 1) a
b : M
hb : Membership.mem (γ := Set M) (Set.Ici 1) b
hab : LT.lt (α := MulArchimedeanClass M) (mk a) (mk b)
⊢ b < a
have hab₁ : ∀ (n : ℕ), |b|ₘ ^ n < |a|ₘ
Tactic: rw [mk_lt_mk] at hab
Cleared hypotheses: hab
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (hypothesis)
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a : M
ha : Membership.mem (γ := Set M) (Set.Ici 1) a
b : M
hb : Membership.mem (γ := Set M) (Set.Ici 1) b
hab : ∀ (n : ℕ), |b|ₘ ^ n < |a|ₘ
⊢ b < a
have h : HPow.hPow (β := ℕ) |b|ₘ 1 < |a|ₘ
Tactic: obtain h := hab 1
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (hypothesis)
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a : M
ha : Membership.mem (γ := Set M) (Set.Ici 1) a
b : M
hb : Membership.mem (γ := Set M) (Set.Ici 1) b
hab : ∀ (n : ℕ), |b|ₘ ^ n < |a|ₘ
h : HPow.hPow (β := ℕ) |b|ₘ 1 < |a|ₘ
⊢ b < a
have h₁ : HPow.hPow (β := ℕ) b 1 < a
Tactic: rw [mabs_eq_self.mpr ha, mabs_eq_self.mpr hb] at h
Cleared hypotheses: h