awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.Kleene (goal)
Goal:
α : Type u_1
inst : KleeneAlgebra α
a : α
n : ℕ
⊢ a ^ (n + 1) ≤ a∗
have grw : a * a ^ n ≤ a∗
Tactic: grw [pow_succ', pow_le_kstar, mul_kstar_le_kstar]
-- Lean 4 proof step from Mathlib.Algebra.Order.Kleene (goal)
Goal:
α : Type u_1
inst : KleeneAlgebra α
a : α
n : ℕ
grw : a * a ^ n ≤ a∗
⊢ a ^ (n + 1) ≤ a∗
have grw₁ : a * a∗ ≤ a∗
Tactic: grw [pow_succ', pow_le_kstar, mul_kstar_le_kstar]
-- Lean 4 proof step from Mathlib.Algebra.Order.Kleene (goal)
Goal:
α : Type u_1
inst : KleeneAlgebra α
a : α
n : ℕ
grw : a * a ^ n ≤ a∗
grw₁ : a * a∗ ≤ a∗
⊢ a ^ (n + 1) ≤ a∗
have grw₂ : a∗ ≤ a∗
Tactic: grw [pow_succ', pow_le_kstar, mul_kstar_le_kstar]
-- Lean 4 proof step from Mathlib.Algebra.Order.Kleene (goal)
Goal:
α : Type u_1
inst : KleeneAlgebra α
a : α
⊢ 1 + a * a∗ ≤ a∗
have rw : 1 ≤ a∗ ∧ a * a∗ ≤ a∗
Tactic: rw [add_le_iff]
-- Lean 4 proof step from Mathlib.Algebra.Order.Kleene (hypothesis)
Goal:
α : Type u_1
inst : KleeneAlgebra α
a : α
⊢ 1 + a * a∗ = a∗
have h : 1 + a * a∗ ≤ a∗
Tactic: have h : 1 + a * a∗ ≤ a∗ := by
    rw [add_le_iff]
    exact ⟨one_le_kstar, mul_kstar_le_kstar⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Kleene (goal)
Goal:
α : Type u_1
inst : KleeneAlgebra α
a : α
h : 1 + a * a∗ ≤ a∗
⊢ 1 + a * a∗ = a∗
have apply : a∗ ≤ 1 + a * a∗
Tactic: apply le_antisymm h
-- Lean 4 proof step from Mathlib.Algebra.Order.Kleene (hypothesis)
Goal:
α : Type u_1
inst : KleeneAlgebra α
a : α
h : 1 + a * a∗ ≤ a∗
this : 1 + a * (1 + a * a∗) ≤ 1 + a * a∗
⊢ a∗ ≤ 1 + a * a∗
have this₁ : 1 ≤ 1 + a * a∗ ∧ a * (1 + a * a∗) ≤ 1 + a * a∗
Tactic: rw [add_le_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Order.Kleene (goal)
Goal:
α : Type u_1
inst : KleeneAlgebra α
a : α
h : 1 + a * a∗ ≤ a∗
this : 1 ≤ 1 + a * a∗ ∧ a * (1 + a * a∗) ≤ 1 + a * a∗
⊢ a∗ ≤ 1 + a * a∗
have nth_rw : a∗ * 1 ≤ 1 + a * a∗
Tactic: nth_rw 1 [← mul_one a∗]
-- Lean 4 proof step from Mathlib.Algebra.Order.Kleene (goal)
Goal:
α : Type u_1
inst : KleeneAlgebra α
a : α
h : 1 + a * a∗ ≤ a∗
⊢ a∗ ≤ 1 + a * a∗
have suffices : 1 + a * (1 + a * a∗) ≤ 1 + a * a∗
Tactic: suffices 1 + a * (1 + a * a∗) ≤ 1 + a * a∗ by
    rw [add_le_iff] at this
    nth_rw 1 [← mul_one a∗]
    exact (mul_right_mono this.1).trans (kstar_mul_le_self this.2)
-- Lean 4 proof step from Mathlib.Algebra.Order.Kleene (goal)
Goal:
α : Type u_1
inst : KleeneAlgebra α
a : α
⊢ 1 + a∗ * a ≤ a∗
have rw : 1 ≤ a∗ ∧ a∗ * a ≤ a∗
Tactic: rw [add_le_iff]
-- Lean 4 proof step from Mathlib.Algebra.Order.Kleene (hypothesis)
Goal:
α : Type u_1
inst : KleeneAlgebra α
a : α
⊢ 1 + a∗ * a = a∗
have h : 1 + a∗ * a ≤ a∗
Tactic: have h : 1 + a∗ * a ≤ a∗ := by
    rw [add_le_iff]
    exact ⟨one_le_kstar, kstar_mul_le_kstar⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Kleene (goal)
Goal:
α : Type u_1
inst : KleeneAlgebra α
a : α
h : 1 + a∗ * a ≤ a∗
⊢ 1 + a∗ * a = a∗
have apply : a∗ ≤ 1 + a∗ * a
Tactic: apply le_antisymm h
-- Lean 4 proof step from Mathlib.Algebra.Order.Kleene (hypothesis)
Goal:
α : Type u_1
inst : KleeneAlgebra α
a : α
h : 1 + a∗ * a ≤ a∗
this : 1 + (1 + a∗ * a) * a ≤ 1 + a∗ * a
⊢ a∗ ≤ 1 + a∗ * a
have this₁ : 1 ≤ 1 + a∗ * a ∧ (1 + a∗ * a) * a ≤ 1 + a∗ * a
Tactic: rw [add_le_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Order.Kleene (goal)
Goal:
α : Type u_1
inst : KleeneAlgebra α
a : α
h : 1 + a∗ * a ≤ a∗
this : 1 ≤ 1 + a∗ * a ∧ (1 + a∗ * a) * a ≤ 1 + a∗ * a
⊢ a∗ ≤ 1 + a∗ * a
have nth_rw : 1 * a∗ ≤ 1 + a∗ * a
Tactic: nth_rw 1 [← one_mul a∗]
-- Lean 4 proof step from Mathlib.Algebra.Order.Kleene (goal)
Goal:
α : Type u_1
inst : KleeneAlgebra α
a : α
h : 1 + a∗ * a ≤ a∗
⊢ a∗ ≤ 1 + a∗ * a
have suffices : 1 + (1 + a∗ * a) * a ≤ 1 + a∗ * a
Tactic: suffices 1 + (1 + a∗ * a) * a ≤ 1 + a∗ * a by
    rw [add_le_iff] at this
    nth_rw 1 [← one_mul a∗]
    exact (mul_left_mono this.1).trans (mul_kstar_le_self this.2)
-- Lean 4 proof step from Mathlib.Algebra.Order.Kleene (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst : IdemSemiring α
inst_1 : LE β
inst_2 : LT β
inst_3 : Zero β
inst_4 : One β
inst_5 : Add β
inst_6 : Mul β
inst_7 : Pow β ℕ
inst_8 : SMul ℕ β
inst_9 : NatCast β
inst_10 : Max β
inst_11 : Bot β
f : β → α
hf : Injective f
le : ∀ {x y : β}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : β}, f x < f y ↔ x < y
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : β), f (x + y) = f x + f y
mul : ∀ (x y : β), f (x * y) = f x * f y
nsmul : ∀ (n : ℕ) (x : β), f (n • x) = n • f x
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
natCast : ∀ (n : ℕ), f (↑n : β) = (↑n : α)
sup : ∀ (a b : β), f (a ⊔ b) = f a ⊔ f b
bot : f ⊥ = ⊥
a b : β
⊢ f (a + b) = f (a ⊔ b)
have rw : f (a + b) = f a ⊔ f b
Tactic: rw [sup, add, add_eq_sup]
-- Lean 4 proof step from Mathlib.Algebra.Order.Kleene (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst : IdemSemiring α
inst_1 : LE β
inst_2 : LT β
inst_3 : Zero β
inst_4 : One β
inst_5 : Add β
inst_6 : Mul β
inst_7 : Pow β ℕ
inst_8 : SMul ℕ β
inst_9 : NatCast β
inst_10 : Max β
inst_11 : Bot β
f : β → α
hf : Injective f
le : ∀ {x y : β}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : β}, f x < f y ↔ x < y
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : β), f (x + y) = f x + f y
mul : ∀ (x y : β), f (x * y) = f x * f y
nsmul : ∀ (n : ℕ) (x : β), f (n • x) = n • f x
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
natCast : ∀ (n : ℕ), f (↑n : β) = (↑n : α)
sup : ∀ (a b : β), f (a ⊔ b) = f a ⊔ f b
bot : f ⊥ = ⊥
a b : β
rw : f (a + b) = f a ⊔ f b
⊢ f (a + b) = f (a ⊔ b)
have rw₁ : f a + f b = f a ⊔ f b
Tactic: rw [sup, add, add_eq_sup]
-- Lean 4 proof step from Mathlib.Algebra.Order.Kleene (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst : IdemSemiring α
inst_1 : LE β
inst_2 : LT β
inst_3 : Zero β
inst_4 : One β
inst_5 : Add β
inst_6 : Mul β
inst_7 : Pow β ℕ
inst_8 : SMul ℕ β
inst_9 : NatCast β
inst_10 : Max β
inst_11 : Bot β
f : β → α
hf : Injective f
le : ∀ {x y : β}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : β}, f x < f y ↔ x < y
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : β), f (x + y) = f x + f y
mul : ∀ (x y : β), f (x * y) = f x * f y
nsmul : ∀ (n : ℕ) (x : β), f (n • x) = n • f x
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
natCast : ∀ (n : ℕ), f (↑n : β) = (↑n : α)
sup : ∀ (a b : β), f (a ⊔ b) = f a ⊔ f b
bot : f ⊥ = ⊥
a b : β
rw : f (a + b) = f a ⊔ f b
rw₁ : f a + f b = f a ⊔ f b
⊢ f (a + b) = f (a ⊔ b)
have rw₂ : f a ⊔ f b = f a ⊔ f b
Tactic: rw [sup, add, add_eq_sup]
-- Lean 4 proof step from Mathlib.Algebra.Order.Kleene (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst : KleeneAlgebra α
inst_1 : LE β
inst_2 : LT β
inst_3 : Zero β
inst_4 : One β
inst_5 : Add β
inst_6 : Mul β
inst_7 : Pow β ℕ
inst_8 : SMul ℕ β
inst_9 : NatCast β
inst_10 : Max β
inst_11 : Bot β
inst_12 : KStar β
f : β → α
hf : Injective f
le : ∀ {x y : β}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : β}, f x < f y ↔ x < y
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : β), f (x + y) = f x + f y
mul : ∀ (x y : β), f (x * y) = f x * f y
nsmul : ∀ (n : ℕ) (x : β), f (n • x) = n • f x
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
natCast : ∀ (n : ℕ), f (↑n : β) = (↑n : α)
sup : ∀ (a b : β), f (a ⊔ b) = f a ⊔ f b
bot : f ⊥ = ⊥
kstar : ∀ (a : β), f a∗ = (f a)∗
a : β
⊢ 1 ≤ a∗
have rw : 1 ≤ (f a)∗
Tactic: rw [← le, one, kstar]
-- Lean 4 proof step from Mathlib.Algebra.Order.Kleene (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst : KleeneAlgebra α
inst_1 : LE β
inst_2 : LT β
inst_3 : Zero β
inst_4 : One β
inst_5 : Add β
inst_6 : Mul β
inst_7 : Pow β ℕ
inst_8 : SMul ℕ β
inst_9 : NatCast β
inst_10 : Max β
inst_11 : Bot β
inst_12 : KStar β
f : β → α
hf : Injective f
le : ∀ {x y : β}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : β}, f x < f y ↔ x < y
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : β), f (x + y) = f x + f y
mul : ∀ (x y : β), f (x * y) = f x * f y
nsmul : ∀ (n : ℕ) (x : β), f (n • x) = n • f x
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
natCast : ∀ (n : ℕ), f (↑n : β) = (↑n : α)
sup : ∀ (a b : β), f (a ⊔ b) = f a ⊔ f b
bot : f ⊥ = ⊥
kstar : ∀ (a : β), f a∗ = (f a)∗
a : β
⊢ a * a∗ ≤ a∗
have rw : f a * (f a)∗ ≤ (f a)∗
Tactic: rw [← le, mul, kstar]
-- Lean 4 proof step from Mathlib.Algebra.Order.Kleene (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst : KleeneAlgebra α
inst_1 : LE β
inst_2 : LT β
inst_3 : Zero β
inst_4 : One β
inst_5 : Add β
inst_6 : Mul β
inst_7 : Pow β ℕ
inst_8 : SMul ℕ β
inst_9 : NatCast β
inst_10 : Max β
inst_11 : Bot β
inst_12 : KStar β
f : β → α
hf : Injective f
le : ∀ {x y : β}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : β}, f x < f y ↔ x < y
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : β), f (x + y) = f x + f y
mul : ∀ (x y : β), f (x * y) = f x * f y
nsmul : ∀ (n : ℕ) (x : β), f (n • x) = n • f x
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
natCast : ∀ (n : ℕ), f (↑n : β) = (↑n : α)
sup : ∀ (a b : β), f (a ⊔ b) = f a ⊔ f b
bot : f ⊥ = ⊥
kstar : ∀ (a : β), f a∗ = (f a)∗
a : β
⊢ a∗ * a ≤ a∗
have rw : (f a)∗ * f a ≤ (f a)∗
Tactic: rw [← le, mul, kstar]
-- Lean 4 proof step from Mathlib.Algebra.Order.Kleene (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst : KleeneAlgebra α
inst_1 : LE β
inst_2 : LT β
inst_3 : Zero β
inst_4 : One β
inst_5 : Add β
inst_6 : Mul β
inst_7 : Pow β ℕ
inst_8 : SMul ℕ β
inst_9 : NatCast β
inst_10 : Max β
inst_11 : Bot β
inst_12 : KStar β
f : β → α
hf : Injective f
le : ∀ {x y : β}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : β}, f x < f y ↔ x < y
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : β), f (x + y) = f x + f y
mul : ∀ (x y : β), f (x * y) = f x * f y
nsmul : ∀ (n : ℕ) (x : β), f (n • x) = n • f x
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
natCast : ∀ (n : ℕ), f (↑n : β) = (↑n : α)
sup : ∀ (a b : β), f (a ⊔ b) = f a ⊔ f b
bot : f ⊥ = ⊥
kstar : ∀ (a : β), f a∗ = (f a)∗
a b : β
h : b * a ≤ b
⊢ b * a∗ ≤ b
have rw : f b * (f a)∗ ≤ f b
Tactic: rw [← le, mul, kstar]
-- Lean 4 proof step from Mathlib.Algebra.Order.Kleene (hypothesis)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst : KleeneAlgebra α
inst_1 : LE β
inst_2 : LT β
inst_3 : Zero β
inst_4 : One β
inst_5 : Add β
inst_6 : Mul β
inst_7 : Pow β ℕ
inst_8 : SMul ℕ β
inst_9 : NatCast β
inst_10 : Max β
inst_11 : Bot β
inst_12 : KStar β
f : β → α
hf : Injective f
le : ∀ {x y : β}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : β}, f x < f y ↔ x < y
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : β), f (x + y) = f x + f y
mul : ∀ (x y : β), f (x * y) = f x * f y
nsmul : ∀ (n : ℕ) (x : β), f (n • x) = n • f x
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
natCast : ∀ (n : ℕ), f (↑n : β) = (↑n : α)
sup : ∀ (a b : β), f (a ⊔ b) = f a ⊔ f b
bot : f ⊥ = ⊥
kstar : ∀ (a : β), f a∗ = (f a)∗
a b : β
h : b * a ≤ b
⊢ f b * (f a)∗ ≤ f b
have h₁ : f b * f a ≤ f b
Tactic: rw [← le, mul] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Order.Kleene (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst : KleeneAlgebra α
inst_1 : LE β
inst_2 : LT β
inst_3 : Zero β
inst_4 : One β
inst_5 : Add β
inst_6 : Mul β
inst_7 : Pow β ℕ
inst_8 : SMul ℕ β
inst_9 : NatCast β
inst_10 : Max β
inst_11 : Bot β
inst_12 : KStar β
f : β → α
hf : Injective f
le : ∀ {x y : β}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : β}, f x < f y ↔ x < y
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : β), f (x + y) = f x + f y
mul : ∀ (x y : β), f (x * y) = f x * f y
nsmul : ∀ (n : ℕ) (x : β), f (n • x) = n • f x
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
natCast : ∀ (n : ℕ), f (↑n : β) = (↑n : α)
sup : ∀ (a b : β), f (a ⊔ b) = f a ⊔ f b
bot : f ⊥ = ⊥
kstar : ∀ (a : β), f a∗ = (f a)∗
a b : β
h : a * b ≤ b
⊢ a∗ * b ≤ b
have rw : (f a)∗ * f b ≤ f b
Tactic: rw [← le, mul, kstar]
-- Lean 4 proof step from Mathlib.Algebra.Order.Kleene (hypothesis)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst : KleeneAlgebra α
inst_1 : LE β
inst_2 : LT β
inst_3 : Zero β
inst_4 : One β
inst_5 : Add β
inst_6 : Mul β
inst_7 : Pow β ℕ
inst_8 : SMul ℕ β
inst_9 : NatCast β
inst_10 : Max β
inst_11 : Bot β
inst_12 : KStar β
f : β → α
hf : Injective f
le : ∀ {x y : β}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : β}, f x < f y ↔ x < y
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : β), f (x + y) = f x + f y
mul : ∀ (x y : β), f (x * y) = f x * f y
nsmul : ∀ (n : ℕ) (x : β), f (n • x) = n • f x
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
natCast : ∀ (n : ℕ), f (↑n : β) = (↑n : α)
sup : ∀ (a b : β), f (a ⊔ b) = f a ⊔ f b
bot : f ⊥ = ⊥
kstar : ∀ (a : β), f a∗ = (f a)∗
a b : β
h : a * b ≤ b
⊢ (f a)∗ * f b ≤ f b
have h₁ : f a * f b ≤ f b
Tactic: rw [← le, mul] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Archimedean (hypothesis)
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
K : Type u_2
inst_3 : Ring K
inst_4 : LinearOrder K
inst_5 : IsOrderedRing K
inst_6 : Archimedean K
inst_7 : Module K M
inst_8 : PosSMulMono K M
a : M
k : K
h : k ≠ 0
⊢ Eq (α := ArchimedeanClass M) (mk (k • a)) (mk a)
have this : Nontrivial K
Tactic: have : Nontrivial K := nontrivial_iff.mpr ⟨k, 0, h⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Archimedean (goal)
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
K : Type u_2
inst_3 : Ring K
inst_4 : LinearOrder K
inst_5 : IsOrderedRing K
inst_6 : Archimedean K
inst_7 : Module K M
inst_8 : PosSMulMono K M
a : M
k : K
h : k ≠ 0
this : Nontrivial K
⊢ Eq (α := ArchimedeanClass M) (mk (k • a)) (mk a)
have obtain : ∀ (m : ℕ) (hm : 1 ≤ m • |k|), Eq (α := ArchimedeanClass M) (mk (k • a)) (mk a)
Tactic: obtain ⟨m, hm⟩ := Archimedean.arch 1 (show 0 < |k| by simpa using h)
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Archimedean (goal)
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
K : Type u_2
inst_3 : Ring K
inst_4 : LinearOrder K
inst_5 : IsOrderedRing K
inst_6 : Archimedean K
inst_7 : Module K M
inst_8 : PosSMulMono K M
a : M
k : K
h : k ≠ 0
this : Nontrivial K
m : ℕ
hm : 1 ≤ m • |k|
⊢ Eq (α := ArchimedeanClass M) (mk (k • a)) (mk a)
have obtain : ∀ (n : ℕ) (hn : |k| ≤ HSMul.hSMul (β := K) n 1), Eq (α := ArchimedeanClass M) (mk (k • a)) (mk a)
Tactic: obtain ⟨n, hn⟩ := Archimedean.arch |k| (show 0 < 1 by simp)
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Archimedean (goal)
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
K : Type u_2
inst_3 : Ring K
inst_4 : LinearOrder K
inst_5 : IsOrderedRing K
inst_6 : Archimedean K
inst_7 : Module K M
inst_8 : PosSMulMono K M
a : M
k : K
h : k ≠ 0
this : Nontrivial K
m : ℕ
hm : 1 ≤ m • |k|
n : ℕ
hn : |k| ≤ HSMul.hSMul (β := K) n 1
⊢ Eq (α := ArchimedeanClass M) (mk (k • a)) (mk a)
have simp_rw : (∃ (m : ℕ), |a| ≤ m • |k| • |a|) ∧ ∃ (n : ℕ), |k| • |a| ≤ n • |a|
Tactic: simp_rw [mk_eq_mk, abs_smul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Archimedean (goal)
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
K : Type u_2
inst_3 : Ring K
inst_4 : LinearOrder K
inst_5 : IsOrderedRing K
inst_6 : Archimedean K
inst_7 : Module K M
inst_8 : PosSMulMono K M
a : M
k : K
h : k ≠ 0
this : Nontrivial K
m : ℕ
hm : 1 ≤ m • |k|
n : ℕ
hn : |k| ≤ HSMul.hSMul (β := K) n 1
⊢ (∃ (m : ℕ), |a| ≤ m • |k| • |a|) ∧ ∃ (n : ℕ), |k| • |a| ≤ n • |a|
have refine_1 : |a| ≤ m • |k| • |a|
Tactic: refine ⟨⟨m, ?_⟩, ⟨n, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Archimedean (goal)
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
K : Type u_2
inst_3 : Ring K
inst_4 : LinearOrder K
inst_5 : IsOrderedRing K
inst_6 : Archimedean K
inst_7 : Module K M
inst_8 : PosSMulMono K M
a : M
k : K
h : k ≠ 0
this : Nontrivial K
m : ℕ
hm : 1 ≤ m • |k|
n : ℕ
hn : |k| ≤ HSMul.hSMul (β := K) n 1
refine_1 : |a| ≤ m • |k| • |a|
⊢ (∃ (m : ℕ), |a| ≤ m • |k| • |a|) ∧ ∃ (n : ℕ), |k| • |a| ≤ n • |a|
have refine_2 : |k| • |a| ≤ n • |a|
Tactic: refine ⟨⟨m, ?_⟩, ⟨n, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Archimedean (goal)
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
K : Type u_2
inst_3 : Ring K
inst_4 : LinearOrder K
inst_5 : IsOrderedRing K
inst_6 : Archimedean K
inst_7 : Module K M
inst_8 : PosSMulMono K M
a : M
k : K
h : k ≠ 0
this : Nontrivial K
m : ℕ
hm : 1 ≤ m • |k|
n : ℕ
hn : |k| ≤ HSMul.hSMul (β := K) n 1
⊢ |a| ≤ m • |k| • |a|
have refine_1 : |a| ≤ (m • |k|) • |a|
Tactic: rw [← smul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Archimedean (goal)
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
K : Type u_2
inst_3 : Ring K
inst_4 : LinearOrder K
inst_5 : IsOrderedRing K
inst_6 : Archimedean K
inst_7 : Module K M
inst_8 : PosSMulMono K M
a : M
k : K
h : k ≠ 0
this : Nontrivial K
m : ℕ
hm : 1 ≤ m • |k|
n : ℕ
hn : |k| ≤ HSMul.hSMul (β := K) n 1
⊢ n • |a| = HSMul.hSMul (β := K) n 1 • |a|
have rw : n • |a| = n • HSMul.hSMul.{u_2, u_1, u_1} (α := K) 1 |a|
Tactic: rw [smul_assoc, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Archimedean (goal)
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
K : Type u_2
inst_3 : Ring K
inst_4 : LinearOrder K
inst_5 : IsOrderedRing K
inst_6 : Archimedean K
inst_7 : Module K M
inst_8 : PosSMulMono K M
a : M
k : K
h : k ≠ 0
this : Nontrivial K
m : ℕ
hm : 1 ≤ m • |k|
n : ℕ
hn : |k| ≤ HSMul.hSMul (β := K) n 1
rw : n • |a| = n • HSMul.hSMul.{u_2, u_1, u_1} (α := K) 1 |a|
⊢ n • |a| = HSMul.hSMul (β := K) n 1 • |a|
have rw₁ : n • |a| = n • |a|
Tactic: rw [smul_assoc, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Archimedean (hypothesis)
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
K : Type u_2
inst_3 : Ring K
inst_4 : LinearOrder K
inst_5 : IsOrderedRing K
inst_6 : Archimedean K
inst_7 : Module K M
inst_8 : PosSMulMono K M
a : M
k : K
h : k ≠ 0
this : Nontrivial K
m : ℕ
hm : 1 ≤ m • |k|
n : ℕ
hn : |k| ≤ HSMul.hSMul (β := K) n 1
⊢ |k| • |a| ≤ n • |a|
have this₁ : n • |a| = HSMul.hSMul (β := K) n 1 • |a|
Tactic: have : n • |a| = (n • (1 : K)) • |a| := by rw [smul_assoc, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Archimedean (goal)
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
K : Type u_2
inst_3 : Ring K
inst_4 : LinearOrder K
inst_5 : IsOrderedRing K
inst_6 : Archimedean K
inst_7 : Module K M
inst_8 : PosSMulMono K M
a : M
k : K
h : k ≠ 0
this_1 : Nontrivial K
m : ℕ
hm : 1 ≤ m • |k|
n : ℕ
hn : |k| ≤ HSMul.hSMul (β := K) n 1
this : n • |a| = HSMul.hSMul (β := K) n 1 • |a|
⊢ |k| • |a| ≤ n • |a|
have refine_2 : |k| • |a| ≤ HSMul.hSMul (β := K) n 1 • |a|
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Archimedean (goal)
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
K : Type u_2
inst_3 : Ring K
inst_4 : LinearOrder K
inst_5 : IsOrderedRing K
inst_6 : Archimedean K
inst_7 : Module K M
inst_8 : PosSMulMono K M
a : M
k : K
⊢ LE.le (α := ArchimedeanClass M) (mk a) (mk (k • a))
have inl : LE.le (α := ArchimedeanClass M) (mk a) (mk (HSMul.hSMul.{u_2, u_1, u_1} (α := K) 0 a))
Tactic: obtain rfl | h := eq_or_ne k 0
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Archimedean (goal)
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
K : Type u_2
inst_3 : Ring K
inst_4 : LinearOrder K
inst_5 : IsOrderedRing K
inst_6 : Archimedean K
inst_7 : Module K M
inst_8 : PosSMulMono K M
a : M
k : K
inl : LE.le (α := ArchimedeanClass M) (mk a) (mk (HSMul.hSMul.{u_2, u_1, u_1} (α := K) 0 a))
⊢ LE.le (α := ArchimedeanClass M) (mk a) (mk (k • a))
have inr : ∀ (h : k ≠ 0), LE.le (α := ArchimedeanClass M) (mk a) (mk (k • a))
Tactic: obtain rfl | h := eq_or_ne k 0
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Archimedean (goal)
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
K : Type u_2
inst_3 : Ring K
inst_4 : LinearOrder K
inst_5 : IsOrderedRing K
inst_6 : Archimedean K
inst_7 : Module K M
inst_8 : PosSMulMono K M
s : UpperSet (ArchimedeanClass M)
k : K
a : M
⊢ a ∈ (addSubgroup s).carrier → k • a ∈ (addSubgroup s).carrier
have inl : Membership.mem (γ := Set M)
    (AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (AddSubgroup.toAddSubmonoid (addSubgroup ⊤)))) a →
  Membership.mem (γ := Set M)
    (AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (AddSubgroup.toAddSubmonoid (addSubgroup ⊤)))) (k • a)
Tactic: obtain rfl | hs := eq_or_ne s ⊤
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Archimedean (goal)
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
K : Type u_2
inst_3 : Ring K
inst_4 : LinearOrder K
inst_5 : IsOrderedRing K
inst_6 : Archimedean K
inst_7 : Module K M
inst_8 : PosSMulMono K M
s : UpperSet (ArchimedeanClass M)
k : K
a : M
inl :
  Membership.mem (γ := Set M)
      (AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (AddSubgroup.toAddSubmonoid (addSubgroup ⊤)))) a →
    Membership.mem (γ := Set M)
      (AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (AddSubgroup.toAddSubmonoid (addSubgroup ⊤)))) (k • a)
⊢ a ∈ (addSubgroup s).carrier → k • a ∈ (addSubgroup s).carrier
have inr : ∀ (hs : s ≠ ⊤), a ∈ (addSubgroup s).carrier → k • a ∈ (addSubgroup s).carrier
Tactic: obtain rfl | hs := eq_or_ne s ⊤
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Archimedean (goal)
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
K : Type u_2
inst_3 : Ring K
inst_4 : LinearOrder K
inst_5 : IsOrderedRing K
inst_6 : Archimedean K
inst_7 : Module K M
inst_8 : PosSMulMono K M
c : ArchimedeanClass M
⊢ LE.le (α := Submodule K M) (ball K c) (closedBall K c)
have inl : LE.le.{u_1} (α := Submodule K M) (ball K ⊤) (closedBall K ⊤)
Tactic: obtain rfl | hc := eq_or_ne c ⊤
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Archimedean (goal)
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
K : Type u_2
inst_3 : Ring K
inst_4 : LinearOrder K
inst_5 : IsOrderedRing K
inst_6 : Archimedean K
inst_7 : Module K M
inst_8 : PosSMulMono K M
c : ArchimedeanClass M
inl : LE.le.{u_1} (α := Submodule K M) (ball K ⊤) (closedBall K ⊤)
⊢ LE.le (α := Submodule K M) (ball K c) (closedBall K c)
have inr : ∀ (hc : c ≠ ⊤), LE.le (α := Submodule K M) (ball K c) (closedBall K c)
Tactic: obtain rfl | hc := eq_or_ne c ⊤
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Basic (goal)
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : Invertible (α := R) 2
inst_2 : Lattice M
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : IsOrderedAddMonoid M
x y : M
⊢ x ⊓ y =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
      (x + y - |y - x|)
have rw : x ⊓ y =
  HSMul.hSMul.{u_2, u_3, u_3} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
    (HSMul.hSMul (α := ℕ) 2 (x ⊓ y))
Tactic: rw [← two_nsmul_inf_eq_add_sub_abs_sub x y, two_smul, ← two_smul R,
    smul_smul, invOf_mul_self, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Basic (goal)
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : Invertible (α := R) 2
inst_2 : Lattice M
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : IsOrderedAddMonoid M
x y : M
rw :
  x ⊓ y =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
      (HSMul.hSMul (α := ℕ) 2 (x ⊓ y))
⊢ x ⊓ y =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
      (x + y - |y - x|)
have rw₁ : x ⊓ y =
  HSMul.hSMul.{u_2, u_3, u_3} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x ⊓ y + x ⊓ y)
Tactic: rw [← two_nsmul_inf_eq_add_sub_abs_sub x y, two_smul, ← two_smul R,
    smul_smul, invOf_mul_self, one_smul]