awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Prod (goal)
Goal:
A : Type u_1
inst : AddCommMonoid A
inst_1 : PartialOrder A
inst_2 : CanonicallyOrderedAdd A
inst_3 : Sub A
inst_4 : OrderedSub A
inst_5 : AddLeftReflectLE A
inst_6 : HasAntidiagonal A
n m : A
inst_7 : DecidablePred fun (x : A) ↦ x = m
inst_8 : Decidable (m ≤ n)
⊢ {x ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n | x.2 = m} = if m ≤ n then {(n - m, m)} else ∅
have rw : map { toFun := Prod.swap, inj' := sorry : A × A ↪ A × A }
    (filter ((fun (x : A × A) ↦ x.2 = m) ∘ (⇑{ toFun := Prod.swap, inj' := sorry : A × A ↪ A × A } : (a : A × A) → A × A))
      (@antidiagonal _ AddCommMonoid.toAddMonoid _ n)) =
  if m ≤ n then {(n - m, m)} else ∅
Tactic: rw [← map_swap_antidiagonal, filter_map]
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Prod (hypothesis)
Goal:
A : Type u_1
inst : AddMonoid A
inst_1 : HasAntidiagonal A
n k l : A
h : (k, l) ∈ @antidiagonal _ inst _ n
⊢ Eq (α := (n : A) × ↥(@antidiagonal _ inst _ n))
    ((fun (x : A × A) ↦
        (Sigma.mk (β := fun (n : A) ↦ ↥(@antidiagonal _ inst _ n)) (x.1 + x.2)
            (Subtype.mk (p := fun (x_1 : A × A) ↦ x_1 ∈ @antidiagonal _ inst _ (x.1 + x.2)) x ⋯) :
          (n : A) × ↥(@antidiagonal _ inst _ n)))
      ((fun (x : (n : A) × ↥(@antidiagonal _ inst _ n)) ↦
          (↑(x.snd (β := fun (n : A) ↦ ↥(@antidiagonal _ inst _ n))) : A × A))
        (Sigma.mk (β := fun (n : A) ↦ ↥(@antidiagonal _ inst _ n)) n
          (Subtype.mk (p := fun (x : A × A) ↦ x ∈ @antidiagonal _ inst _ n) (k, l) h))))
    (Sigma.mk (β := fun (n : A) ↦ ↥(@antidiagonal _ inst _ n)) n
      (Subtype.mk (p := fun (x : A × A) ↦ x ∈ @antidiagonal _ inst _ n) (k, l) h))
have h₁ : (k, l).1 + (k, l).2 = n
Tactic: rw [mem_antidiagonal] at h
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Prod (goal)
Goal:
A_1 : Type u_1
A : Type u_2
inst : AddCommMonoid A
inst_1 : PartialOrder A
inst_2 : CanonicallyOrderedAdd A
inst_3 : LocallyFiniteOrderBot A
inst_4 : DecidableEq A
n : A
a : A × A
⊢ a ∈ {uv ∈ Iic n ×ˢ Iic n | uv.1 + uv.2 = n} ↔ a.1 + a.2 = n
have simp : a.1 + a.2 = n → a ∈ Iic n ×ˢ Iic n
Tactic: simp only [mem_filter, and_iff_right_iff_imp]
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
Goal:
G : Type u_1
M : Type u_2
inst : CommMonoid G
inst_1 : LinearOrder G
inst_2 : CommMonoid M
inst_3 : PartialOrder M
inst_4 : MulArchimedean M
f : G →* M
hf : StrictMono.{u_1, u_2} (α := G) (β := M) (⇑f : (a : G) → M)
x x_1 : G
h : 1 < x_1
⊢ ∃ (n : ℕ), x ≤ x_1 ^ n
have refine : ∀ (a : ℕ), (f : (a : G) → M) x ≤ HPow.hPow (α := M) ((f : (a : G) → M) x_1 : M) a → x ≤ x_1 ^ a
Tactic: refine (MulArchimedean.arch (f x) (by simpa using hf h)).imp ?_
-- 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 : Type u_4
inst : CommGroup G
inst_1 : PartialOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
x y : Gᵒᵈ
hy_1 : 1 < y
hy : LT.lt (α := G) ((ofDual : (a : Gᵒᵈ) → G) y : G) (1 : G)
n : ℕ
hn : ((ofDual : (a : Gᵒᵈ) → G) x)⁻¹ ≤ HPow.hPow (α := G) (((ofDual : (a : Gᵒᵈ) → G) y)⁻¹ : G) n
⊢ x ≤ y ^ n
have rwa : ∀ (hn : ((ofDual : (a : Gᵒᵈ) → G) x)⁻¹ ≤ (HPow.hPow (α := G) ((ofDual : (a : Gᵒᵈ) → G) y : G) n)⁻¹), x ≤ y ^ n
Tactic: rwa [inv_pow, inv_le_inv_iff] at hn
Cleared hypotheses: hn
-- 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 : Type u_4
inst : CommGroup G
inst_1 : PartialOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
x y : Gᵒᵈ
hy_1 : 1 < y
hy : LT.lt (α := G) ((ofDual : (a : Gᵒᵈ) → G) y : G) (1 : G)
n : ℕ
hn : ((ofDual : (a : Gᵒᵈ) → G) x)⁻¹ ≤ HPow.hPow (α := G) (((ofDual : (a : Gᵒᵈ) → G) y)⁻¹ : G) n
rwa : ∀ (hn : ((ofDual : (a : Gᵒᵈ) → G) x)⁻¹ ≤ (HPow.hPow (α := G) ((ofDual : (a : Gᵒᵈ) → G) y : G) n)⁻¹), x ≤ y ^ n
⊢ x ≤ y ^ n
have rwa₁ : ∀ (hn : HPow.hPow (α := G) ((ofDual : (a : Gᵒᵈ) → G) y : G) n ≤ (ofDual : (a : Gᵒᵈ) → G) x), x ≤ y ^ n
Tactic: rwa [inv_pow, inv_le_inv_iff] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
a : G
ha : 1 < a
g : G
s : Set ℤ := {n : ℤ | a ^ n ≤ g}
⊢ ∃! k : ℤ, a ^ k ≤ g ∧ g < a ^ (k + 1)
have obtain : ∀ (k : ℕ) (hk : g⁻¹ ≤ a ^ k), ∃! k : ℤ, a ^ k ≤ g ∧ g < a ^ (k + 1)
Tactic: obtain ⟨k, hk : g⁻¹ ≤ a ^ k⟩ := MulArchimedean.arch g⁻¹ ha
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (hypothesis)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
a : G
ha : 1 < a
g : G
s : Set ℤ := {n : ℤ | a ^ n ≤ g}
k : ℕ
hk : g⁻¹ ≤ a ^ k
⊢ ∃! k : ℤ, a ^ k ≤ g ∧ g < a ^ (k + 1)
have h_ne : s.Nonempty
Tactic: have h_ne : s.Nonempty := ⟨-k, by simpa [s] using inv_le_inv' hk⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
a : G
ha : 1 < a
g : G
s : Set ℤ := {n : ℤ | a ^ n ≤ g}
k : ℕ
hk : g⁻¹ ≤ a ^ k
h_ne : s.Nonempty
⊢ ∃! k : ℤ, a ^ k ≤ g ∧ g < a ^ (k + 1)
have obtain : ∀ (k : ℕ) (hk : g ≤ a ^ k), ∃! k : ℤ, a ^ k ≤ g ∧ g < a ^ (k + 1)
Tactic: obtain ⟨k, hk⟩ := MulArchimedean.arch g ha
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
a : G
ha : 1 < a
g : G
s : Set ℤ := {n : ℤ | a ^ n ≤ g}
k_1 : ℕ
hk_1 : g⁻¹ ≤ a ^ k_1
h_ne : s.Nonempty
k : ℕ
hk : g ≤ a ^ k
n : ℤ
hn : n ∈ s
⊢ n ≤ (↑k : ℤ)
have apply : a ^ n ≤ HPow.hPow (β := ℤ) a (↑k : ℤ)
Tactic: apply (zpow_le_zpow_iff_right ha).mp
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
a : G
ha : 1 < a
g : G
s : Set ℤ := {n : ℤ | a ^ n ≤ g}
k_1 : ℕ
hk_1 : g⁻¹ ≤ a ^ k_1
h_ne : s.Nonempty
k : ℕ
hk : g ≤ a ^ k
n : ℤ
hn : n ∈ s
⊢ a ^ n ≤ HPow.hPow (β := ℤ) a (↑k : ℤ)
have rw : ∀ (hk : g ≤ HPow.hPow (β := ℤ) a (↑k : ℤ)) (n : ℤ) (hn : n ∈ s), a ^ n ≤ HPow.hPow (β := ℤ) a (↑k : ℤ)
Tactic: rw [← zpow_natCast] at hk
Cleared hypotheses: hk, n, hn
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (hypothesis)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
a : G
ha : 1 < a
g : G
s : Set ℤ := {n : ℤ | a ^ n ≤ g}
k_1 : ℕ
hk_1 : g⁻¹ ≤ a ^ k_1
h_ne : s.Nonempty
k : ℕ
hk : g ≤ a ^ k
⊢ ∃! k : ℤ, a ^ k ≤ g ∧ g < a ^ (k + 1)
have h_bdd : ∀ n ∈ s, n ≤ (↑k : ℤ)
Tactic: have h_bdd : ∀ n ∈ s, n ≤ (k : ℤ) := by
    intro n hn
    apply (zpow_le_zpow_iff_right ha).mp
    rw [← zpow_natCast] at hk
    exact le_trans hn hk
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
a : G
ha : 1 < a
g : G
s : Set ℤ := {n : ℤ | a ^ n ≤ g}
k_1 : ℕ
hk_1 : g⁻¹ ≤ a ^ k_1
h_ne : s.Nonempty
k : ℕ
hk : g ≤ a ^ k
h_bdd : ∀ n ∈ s, n ≤ (↑k : ℤ)
⊢ ∃! k : ℤ, a ^ k ≤ g ∧ g < a ^ (k + 1)
have obtain : ∀ (m : ℤ) (hm : m ∈ s) (hm' : ∀ z ∈ s, z ≤ m), ∃! k : ℤ, a ^ k ≤ g ∧ g < a ^ (k + 1)
Tactic: obtain ⟨m, hm, hm'⟩ := Int.exists_greatest_of_bdd ⟨k, h_bdd⟩ h_ne
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
a : G
ha : 1 < a
g : G
s : Set ℤ := {n : ℤ | a ^ n ≤ g}
k_1 : ℕ
hk_1 : g⁻¹ ≤ a ^ k_1
h_ne : s.Nonempty
k : ℕ
hk : g ≤ a ^ k
h_bdd : ∀ n ∈ s, n ≤ (↑k : ℤ)
m : ℤ
hm : m ∈ s
hm' : ∀ z ∈ s, z ≤ m
⊢ g < a ^ (m + 1)
have contrapose! : ∀ (hm' : a ^ (m + 1) ≤ g), ∃ z ∈ s, m < z
Tactic: contrapose! hm'
Cleared hypotheses: hm'
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (hypothesis)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
a : G
ha : 1 < a
g : G
s : Set ℤ := {n : ℤ | a ^ n ≤ g}
k_1 : ℕ
hk_1 : g⁻¹ ≤ a ^ k_1
h_ne : s.Nonempty
k : ℕ
hk : g ≤ a ^ k
h_bdd : ∀ n ∈ s, n ≤ (↑k : ℤ)
m : ℤ
hm : m ∈ s
hm' : ∀ z ∈ s, z ≤ m
⊢ ∃! k : ℤ, a ^ k ≤ g ∧ g < a ^ (k + 1)
have hm'' : g < a ^ (m + 1)
Tactic: have hm'' : g < a ^ (m + 1) := by
    contrapose! hm'
    exact ⟨m + 1, hm', lt_add_one _⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
a : G
ha : 1 < a
g : G
s : Set ℤ := {n : ℤ | a ^ n ≤ g}
k_1 : ℕ
hk_1 : g⁻¹ ≤ a ^ k_1
h_ne : s.Nonempty
k : ℕ
hk : g ≤ a ^ k
h_bdd : ∀ n ∈ s, n ≤ (↑k : ℤ)
m : ℤ
hm : m ∈ s
hm' : ∀ z ∈ s, z ≤ m
hm'' : g < a ^ (m + 1)
⊢ ∃! k : ℤ, a ^ k ≤ g ∧ g < a ^ (k + 1)
have refine : ∀ (n : ℤ) (hn : (fun (k : ℤ) ↦ a ^ k ≤ g ∧ g < a ^ (k + 1)) n), m < n + 1
Tactic: refine ⟨m, ⟨hm, hm''⟩, fun n hn => (hm' n hn.1).antisymm <| Int.le_of_lt_add_one ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
a : G
ha : 1 < a
g : G
s : Set ℤ := {n : ℤ | a ^ n ≤ g}
k_1 : ℕ
hk_1 : g⁻¹ ≤ a ^ k_1
h_ne : s.Nonempty
k : ℕ
hk : g ≤ a ^ k
h_bdd : ∀ n ∈ s, n ≤ (↑k : ℤ)
m : ℤ
hm : m ∈ s
hm' : ∀ z ∈ s, z ≤ m
hm'' : g < a ^ (m + 1)
n : ℤ
hn : (fun (k : ℤ) ↦ a ^ k ≤ g ∧ g < a ^ (k + 1)) n
⊢ m < n + 1
have rw : a ^ m < a ^ (n + 1)
Tactic: rw [← zpow_lt_zpow_iff_right ha]
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
Goal:
R : Type u_3
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
y x : R
hy : 0 < y
this : 0 ≤ 1 + y
n : ℕ
h : x ≤ n • y
⊢ (1 + y) ^ n = (y + 1) ^ n
have rw : (y + 1) ^ n = (y + 1) ^ n
Tactic: rw [add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
Goal:
R : Type u_3
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
y : R
inst_4 : ExistsAddOfLE R
x : R
hy1 : 1 < y
⊢ ∃ (n : ℕ), x < y ^ n
have obtain : ∀ (z : R) (hz : 0 < z) (hy1 : 1 < 1 + z), ∃ (n : ℕ), x < (1 + z) ^ n
Tactic: obtain ⟨z, hz, rfl⟩ := exists_pos_add_of_lt' hy1
Cleared hypotheses: y, hy1
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
Goal:
R : Type u_3
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
inst_4 : ExistsAddOfLE R
x z : R
hz : 0 < z
hy1 : 1 < 1 + z
⊢ ∃ (n : ℕ), x < (1 + z) ^ n
have rw : ∃ (n : ℕ), x < (z + 1) ^ n
Tactic: rw [add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
Goal:
R : Type u_3
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
x : R
⊢ ∃ (fl : ℤ), ∀ (z : ℤ), z ≤ fl ↔ (↑z : R) ≤ x
have below : ∃ (n : ℤ), (↑n : R) ≤ x
Tactic: apply exists_floor'
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
Goal:
R : Type u_3
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
x : R
below : ∃ (n : ℤ), (↑n : R) ≤ x
⊢ ∃ (fl : ℤ), ∀ (z : ℤ), z ≤ fl ↔ (↑z : R) ≤ x
have above : ∃ (n : ℤ), x ≤ (↑n : R)
Tactic: apply exists_floor'
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
Goal:
R : Type u_3
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
x : R
⊢ ∃ (n : ℤ), (↑n : R) ≤ x
have below : ∀ (n : ℤ) (hn : (↑n : R) < x), ∃ (n : ℤ), (↑n : R) ≤ x
Tactic: obtain ⟨n, hn⟩ := exists_int_lt x
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
Goal:
R : Type u_3
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
x : R
⊢ ∃ (n : ℤ), x ≤ (↑n : R)
have above : ∀ (n : ℤ) (hn : x < (↑n : R)), ∃ (n : ℤ), x ≤ (↑n : R)
Tactic: obtain ⟨n, hn⟩ := exists_int_gt x
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (hypothesis)
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
inst_4 : ExistsAddOfLE R
x y : R
hx : 1 ≤ x
hy : 1 < y
⊢ ∃ (n : ℕ), y ^ n ≤ x ∧ x < y ^ (n + 1)
have h : ∃ (n : ℕ), x < y ^ n
Tactic: have h : ∃ n : ℕ, x < y ^ n := pow_unbounded_of_one_lt _ hy
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (hypothesis)
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
inst_4 : ExistsAddOfLE R
x y : R
hx : 1 ≤ x
hy : 1 < y
h : ∃ (n : ℕ), x < y ^ n
n : ℕ := Nat.find (p := fun (n : ℕ) ↦ x < y ^ n) h
hn : x < y ^ n
hn0 : n = 0
⊢ False
have hn₁ : x < 1
Tactic: rw [hn0, pow_zero] at hn
Cleared hypotheses: hn, hn0
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
Goal:
K : Type u_4
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : Archimedean K
ε : K
hε : 0 < ε
⊢ ∃ (n : ℕ), 1 / HAdd.hAdd (α := K) (↑n : K) 1 < ε
have obtain : ∀ (n : ℕ) (hn : 1 / ε < (↑n : K)), ∃ (n : ℕ), 1 / HAdd.hAdd (α := K) (↑n : K) 1 < ε
Tactic: obtain ⟨n, hn⟩ := exists_nat_gt (1 / ε)
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
Goal:
K : Type u_4
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : Archimedean K
ε : K
hε : 0 < ε
n : ℕ
hn : 1 / ε < (↑n : K)
⊢ ∃ (n : ℕ), 1 / HAdd.hAdd (α := K) (↑n : K) 1 < ε
have h : 1 / HAdd.hAdd (α := K) (↑n : K) 1 < ε
Tactic: use n
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
Goal:
K : Type u_4
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : Archimedean K
ε : K
hε : 0 < ε
n : ℕ
hn : 1 / ε < (↑n : K)
⊢ 1 / HAdd.hAdd (α := K) (↑n : K) 1 < ε
have h : 1 / ε < HAdd.hAdd (α := K) (↑n : K) 1
Tactic: rw [div_lt_iff₀, ← div_lt_iff₀' hε]
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
Goal:
K : Type u_4
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : Archimedean K
ε : K
hε : 0 < ε
n : ℕ
hn : 1 / ε < (↑n : K)
h : 1 / ε < HAdd.hAdd (α := K) (↑n : K) 1
⊢ 1 / HAdd.hAdd (α := K) (↑n : K) 1 < ε
have h₁ : 0 < HAdd.hAdd (α := K) (↑n : K) 1
Tactic: rw [div_lt_iff₀, ← div_lt_iff₀' hε]
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
Goal:
K : Type u_4
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : Archimedean K
ε : K
hε : 0 < ε
n : ℕ
hn : 1 / ε < (↑n : K)
⊢ 1 / ε < HAdd.hAdd (α := K) (↑n : K) 1
have h : (↑n : K) < HAdd.hAdd (α := K) (↑n : K) 1
Tactic: apply hn.trans
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
Goal:
K : Type u_4
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : Archimedean K
x y : K
inst_4 : ExistsAddOfLE K
hx : 0 < x
hy : 1 < y
⊢ ∃ (m : ℤ), y ^ m ≤ x
have obtain : ∀ (N : ℕ) (hN : x⁻¹ < y ^ N), ∃ (m : ℤ), y ^ m ≤ x
Tactic: obtain ⟨N, hN⟩ := pow_unbounded_of_one_lt x⁻¹ hy
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
Goal:
K : Type u_4
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : Archimedean K
x y : K
inst_4 : ExistsAddOfLE K
hx : 0 < x
hy : 1 < y
N : ℕ
hN : x⁻¹ < y ^ N
⊢ ∃ (m : ℤ), y ^ m ≤ x
have h : HPow.hPow (β := ℤ) y (-(↑N : ℤ)) ≤ x
Tactic: use -N
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
Goal:
K : Type u_4
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : Archimedean K
x y : K
inst_4 : ExistsAddOfLE K
hx : 0 < x
hy : 1 < y
N : ℕ
hN : x⁻¹ < y ^ N
⊢ HPow.hPow (β := ℤ) y (-(↑N : ℤ)) ≤ x
have h : (y ^ N)⁻¹ ≤ x
Tactic: rw [zpow_neg y ↑N, zpow_natCast]
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (hypothesis)
Goal:
K : Type u_4
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : Archimedean K
x y : K
inst_4 : ExistsAddOfLE K
hx : 0 < x
hy : 1 < y
⊢ ∃ (n : ℤ), x ∈ Ico (y ^ n) (y ^ (n + 1))
have he : ∃ (m : ℤ), y ^ m ≤ x
Tactic: have he : ∃ m : ℤ, y ^ m ≤ x := by
    obtain ⟨N, hN⟩ := pow_unbounded_of_one_lt x⁻¹ hy
    use -N
    rw [zpow_neg y ↑N, zpow_natCast]
    exact ((inv_lt_comm₀ hx (lt_trans (inv_pos.2 hx) hN)).1 hN).le
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
Goal:
K : Type u_4
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : Archimedean K
x y : K
inst_4 : ExistsAddOfLE K
hx : 0 < x
hy : 1 < y
he : ∃ (m : ℤ), y ^ m ≤ x
⊢ ∃ (b : ℤ), ∀ (m : ℤ), y ^ m ≤ x → m ≤ b
have obtain : ∀ (M : ℕ) (hM : x < y ^ M), ∃ (b : ℤ), ∀ (m : ℤ), y ^ m ≤ x → m ≤ b
Tactic: obtain ⟨M, hM⟩ := pow_unbounded_of_one_lt x hy
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
Goal:
K : Type u_4
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : Archimedean K
x y : K
inst_4 : ExistsAddOfLE K
hx : 0 < x
hy : 1 < y
he : ∃ (m : ℤ), y ^ m ≤ x
M : ℕ
hM : x < y ^ M
⊢ ∃ (b : ℤ), ∀ (m : ℤ), y ^ m ≤ x → m ≤ b
have refine : ∀ (m : ℤ) (hm : y ^ m ≤ x), m ≤ (↑M : ℤ)
Tactic: refine ⟨M, fun m hm ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
Goal:
K : Type u_4
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : Archimedean K
x y : K
inst_4 : ExistsAddOfLE K
hx : 0 < x
hy : 1 < y
he : ∃ (m : ℤ), y ^ m ≤ x
M : ℕ
hM : x < y ^ M
m : ℤ
hm : y ^ m ≤ x
⊢ m ≤ (↑M : ℤ)
have contrapose! : ∀ (hM : (↑M : ℤ) < m), y ^ M ≤ x
Tactic: contrapose! hM
Cleared hypotheses: hM
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
Goal:
K : Type u_4
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : Archimedean K
x y : K
inst_4 : ExistsAddOfLE K
hx : 0 < x
hy : 1 < y
he : ∃ (m : ℤ), y ^ m ≤ x
M : ℕ
m : ℤ
hm : y ^ m ≤ x
hM : (↑M : ℤ) < m
⊢ y ^ M ≤ x
have rw : HPow.hPow (β := ℤ) y (↑M : ℤ) ≤ x
Tactic: rw [← zpow_natCast]
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (hypothesis)
Goal:
K : Type u_4
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : Archimedean K
x y : K
inst_4 : ExistsAddOfLE K
hx : 0 < x
hy : 1 < y
he : ∃ (m : ℤ), y ^ m ≤ x
⊢ ∃ (n : ℤ), x ∈ Ico (y ^ n) (y ^ (n + 1))
have hb : ∃ (b : ℤ), ∀ (m : ℤ), y ^ m ≤ x → m ≤ b
Tactic: have hb : ∃ b : ℤ, ∀ m, y ^ m ≤ x → m ≤ b := by
    obtain ⟨M, hM⟩ := pow_unbounded_of_one_lt x hy
    refine ⟨M, fun m hm ↦ ?_⟩
    contrapose! hM
    rw [← zpow_natCast]
    exact le_trans (zpow_le_zpow_right₀ hy.le hM.le) hm
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
Goal:
K : Type u_4
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : Archimedean K
x y : K
inst_4 : ExistsAddOfLE K
hx : 0 < x
hy : 1 < y
he : ∃ (m : ℤ), y ^ m ≤ x
hb : ∃ (b : ℤ), ∀ (m : ℤ), y ^ m ≤ x → m ≤ b
⊢ ∃ (n : ℤ), x ∈ Ico (y ^ n) (y ^ (n + 1))
have obtain : ∀ (n : ℤ) (hn₁ : y ^ n ≤ x) (hn₂ : ∀ (z : ℤ), y ^ z ≤ x → z ≤ n), ∃ (n : ℤ), x ∈ Ico (y ^ n) (y ^ (n + 1))
Tactic: obtain ⟨n, hn₁, hn₂⟩ := Int.exists_greatest_of_bdd hb he
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
Goal:
K : Type u_4
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : Archimedean K
x y : K
inst_4 : ExistsAddOfLE K
hx : 0 < x
hy : 1 < y
⊢ ∃ (n : ℤ), x ∈ Ico (y ^ n) (y ^ (n + 1))
have have : ∃ (m : ℤ), y ^ m ≤ x
Tactic: classical
  have he : ∃ m : ℤ, y ^ m ≤ x := by
    obtain ⟨N, hN⟩ := pow_unbounded_of_one_lt x⁻¹ hy
    use -N
    rw [zpow_neg y ↑N, zpow_natCast]
    exact ((inv_lt_comm₀ hx (lt_trans (inv_pos.2 hx) hN)).1 hN).le
  have hb : ∃ b : ℤ, ∀ m, y ^ m ≤ x → m ≤ b := by
    obtain ⟨M, hM⟩ := pow_unbounded_of_one_lt x hy
    refine ⟨M, fun m hm ↦ ?_⟩
    contrapose! hM
    rw [← zpow_natCast]
    exact le_trans (zpow_le_zpow_right₀ hy.le hM.le) hm
  obtain ⟨n, hn₁, hn₂⟩ := Int.exists_greatest_of_bdd hb he
  exact ⟨n, hn₁, lt_of_not_ge fun hge => (Int.lt_succ _).not_ge (hn₂ _ hge)⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
Goal:
K : Type u_4
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : Archimedean K
x y : K
inst_4 : ExistsAddOfLE K
hx : 0 < x
hy : 1 < y
have : ∃ (m : ℤ), y ^ m ≤ x
⊢ ∃ (n : ℤ), x ∈ Ico (y ^ n) (y ^ (n + 1))
have have₁ : ∀ (he : ∃ (m : ℤ), y ^ m ≤ x), ∃ (n : ℤ), x ∈ Ico (y ^ n) (y ^ (n + 1))
Tactic: classical
  have he : ∃ m : ℤ, y ^ m ≤ x := by
    obtain ⟨N, hN⟩ := pow_unbounded_of_one_lt x⁻¹ hy
    use -N
    rw [zpow_neg y ↑N, zpow_natCast]
    exact ((inv_lt_comm₀ hx (lt_trans (inv_pos.2 hx) hN)).1 hN).le
  have hb : ∃ b : ℤ, ∀ m, y ^ m ≤ x → m ≤ b := by
    obtain ⟨M, hM⟩ := pow_unbounded_of_one_lt x hy
    refine ⟨M, fun m hm ↦ ?_⟩
    contrapose! hM
    rw [← zpow_natCast]
    exact le_trans (zpow_le_zpow_right₀ hy.le hM.le) hm
  obtain ⟨n, hn₁, hn₂⟩ := Int.exists_greatest_of_bdd hb he
  exact ⟨n, hn₁, lt_of_not_ge fun hge => (Int.lt_succ _).not_ge (hn₂ _ hge)⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
Goal:
K : Type u_4
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : Archimedean K
x y : K
inst_4 : ExistsAddOfLE K
hx : 0 < x
hy : 1 < y
have : ∃ (m : ℤ), y ^ m ≤ x
have₁ : ∀ (he : ∃ (m : ℤ), y ^ m ≤ x), ∃ (n : ℤ), x ∈ Ico (y ^ n) (y ^ (n + 1))
have₂ : ∃ (m : ℤ), y ^ m ≤ x
have₃ have₄ : ∀ (he : ∃ (m : ℤ), y ^ m ≤ x), ∃ (n : ℤ), x ∈ Ico (y ^ n) (y ^ (n + 1))
⊢ ∃ (n : ℤ), x ∈ Ico (y ^ n) (y ^ (n + 1))
have have₅ : ∀ (he : ∃ (m : ℤ), y ^ m ≤ x) (hb : ∃ (b : ℤ), ∀ (m : ℤ), y ^ m ≤ x → m ≤ b), ∃ (n : ℤ), x ∈ Ico (y ^ n) (y ^ (n + 1))
Tactic: classical
  have he : ∃ m : ℤ, y ^ m ≤ x := by
    obtain ⟨N, hN⟩ := pow_unbounded_of_one_lt x⁻¹ hy
    use -N
    rw [zpow_neg y ↑N, zpow_natCast]
    exact ((inv_lt_comm₀ hx (lt_trans (inv_pos.2 hx) hN)).1 hN).le
  have hb : ∃ b : ℤ, ∀ m, y ^ m ≤ x → m ≤ b := by
    obtain ⟨M, hM⟩ := pow_unbounded_of_one_lt x hy
    refine ⟨M, fun m hm ↦ ?_⟩
    contrapose! hM
    rw [← zpow_natCast]
    exact le_trans (zpow_le_zpow_right₀ hy.le hM.le) hm
  obtain ⟨n, hn₁, hn₂⟩ := Int.exists_greatest_of_bdd hb he
  exact ⟨n, hn₁, lt_of_not_ge fun hge => (Int.lt_succ _).not_ge (hn₂ _ hge)⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
Goal:
K : Type u_4
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : Archimedean K
x y : K
inst_4 : ExistsAddOfLE K
hx : 0 < x
hy : 1 < y
have : ∃ (m : ℤ), y ^ m ≤ x
have₁ : ∀ (he : ∃ (m : ℤ), y ^ m ≤ x), ∃ (n : ℤ), x ∈ Ico (y ^ n) (y ^ (n + 1))
have₂ : ∃ (m : ℤ), y ^ m ≤ x
have₃ have₄ : ∀ (he : ∃ (m : ℤ), y ^ m ≤ x), ∃ (n : ℤ), x ∈ Ico (y ^ n) (y ^ (n + 1))
have₅ :
  ∀ (he : ∃ (m : ℤ), y ^ m ≤ x) (hb : ∃ (b : ℤ), ∀ (m : ℤ), y ^ m ≤ x → m ≤ b), ∃ (n : ℤ), x ∈ Ico (y ^ n) (y ^ (n + 1))
⊢ ∃ (n : ℤ), x ∈ Ico (y ^ n) (y ^ (n + 1))
have have₆ : ∀ (he : ∃ (m : ℤ), y ^ m ≤ x) (hb : ∃ (b : ℤ), ∀ (m : ℤ), y ^ m ≤ x → m ≤ b) (n : ℤ) (hn₁ : y ^ n ≤ x)
  (hn₂ : ∀ (z : ℤ), y ^ z ≤ x → z ≤ n), ∃ (n : ℤ), x ∈ Ico (y ^ n) (y ^ (n + 1))
Tactic: classical
  have he : ∃ m : ℤ, y ^ m ≤ x := by
    obtain ⟨N, hN⟩ := pow_unbounded_of_one_lt x⁻¹ hy
    use -N
    rw [zpow_neg y ↑N, zpow_natCast]
    exact ((inv_lt_comm₀ hx (lt_trans (inv_pos.2 hx) hN)).1 hN).le
  have hb : ∃ b : ℤ, ∀ m, y ^ m ≤ x → m ≤ b := by
    obtain ⟨M, hM⟩ := pow_unbounded_of_one_lt x hy
    refine ⟨M, fun m hm ↦ ?_⟩
    contrapose! hM
    rw [← zpow_natCast]
    exact le_trans (zpow_le_zpow_right₀ hy.le hM.le) hm
  obtain ⟨n, hn₁, hn₂⟩ := Int.exists_greatest_of_bdd hb he
  exact ⟨n, hn₁, lt_of_not_ge fun hge => (Int.lt_succ _).not_ge (hn₂ _ hge)⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
Goal:
K : Type u_4
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : Archimedean K
x y : K
inst_4 : ExistsAddOfLE K
hx : 0 < x
hy : 1 < y
m : ℤ
hle : y ^ m ≤ x⁻¹
hlt : x⁻¹ < y ^ (m + 1)
hyp : 0 < y
⊢ y ^ (-(m + 1)) < x
have rwa : (y ^ (m + 1))⁻¹ < x
Tactic: rwa [zpow_neg, inv_lt_comm₀ (zpow_pos hyp _) hx]