awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Kleene
Goal:
α : Type u_1
inst : KleeneAlgebra α
a : α
h : 1 + a∗ * a ≤ a∗
this : 1 ≤ 1 + a∗ * a ∧ (1 + a∗ * a) * a ≤ 1 + a∗ * a
nth_rw : 1 * a∗ ≤ 1 + a∗ * a
⊢ a∗ ≤ 1 + a∗ * a

Tactic:
nth_rw 1 [← one_mul a∗]

Premises used: KStar.kstar, one_mul
-- Module: Mathlib.Algebra.Order.Kleene
Goal:
α : Type u_1
inst : KleeneAlgebra α
a : α
h : 1 + a∗ * a ≤ a∗
this : 1 ≤ 1 + a∗ * a ∧ (1 + a∗ * a) * a ≤ 1 + a∗ * a
⊢ 1 * a∗ ≤ 1 + a∗ * a

Tactic:
(mul_left_mono this.1).trans (mul_kstar_le_self this.2)

Premises used: mul_left_mono, And.right, And.left, mul_kstar_le_self, LE.le.trans
-- Module: Mathlib.Algebra.Order.Kleene
Goal:
α : Type u_1
inst : KleeneAlgebra α
a : α
h : 1 + a∗ * a ≤ a∗
this : 1 ≤ 1 + a∗ * a ∧ (1 + a∗ * a) * a ≤ 1 + a∗ * a
⊢ 1 * a∗ ≤ 1 + a∗ * a

Tactic:
exact (mul_left_mono this.1).trans (mul_kstar_le_self this.2)

Premises used: mul_left_mono, And.right, And.left, mul_kstar_le_self, LE.le.trans
-- Module: Mathlib.Algebra.Order.Kleene
Goal:
α : Type u_1
inst : KleeneAlgebra α
a : α
h : 1 + a∗ * a ≤ a∗
suffices : 1 + (1 + a∗ * a) * a ≤ 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)
-- Module: Mathlib.Algebra.Order.Kleene
Goal:
α : Type u_1
inst : KleeneAlgebra α
a : α
h : 1 + a∗ * a ≤ a∗
⊢ 1 + (1 + a∗ * a) * a ≤ 1 + a∗ * a

Tactic:
apply add_le_add_right (mul_left_mono h)

Premises used: add_le_add_right, mul_left_mono
-- Module: Mathlib.Algebra.Order.Kleene
Goal:
α : Type u_1
β : Type u_2
inst : KleeneAlgebra α
inst_1 : KleeneAlgebra β
a : α × β
⊢ a∗ = (a.1∗, a.2∗)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Kleene
Goal:
α : Type u_1
β : Type u_2
inst : KleeneAlgebra α
inst_1 : KleeneAlgebra β
a : α × β
⊢ a∗.1 = a.1∗

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Kleene
Goal:
α : Type u_1
β : Type u_2
inst : KleeneAlgebra α
inst_1 : KleeneAlgebra β
a : α × β
⊢ a∗.2 = a.2∗

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Kleene
Goal:
ι : Type u_3
π : ι → Type u_4
inst : (i : ι) → KleeneAlgebra (π i)
a : (i : ι) → π i
⊢ a∗ = fun (i : ι) ↦ (a i)∗

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Kleene
Goal:
ι : Type u_3
π : ι → Type u_4
inst : (i : ι) → KleeneAlgebra (π i)
a : (i : ι) → π i
i : ι
⊢ a∗ i = (a i)∗

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Kleene
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
rw₂ rw₃ : f a ⊔ f b = f a ⊔ f b
⊢ f (a + b) = f (a ⊔ b)

Tactic:
rw [sup, add, add_eq_sup]

Premises used: add_eq_sup
-- Module: Mathlib.Algebra.Order.Kleene
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 : β
rw : 1 ≤ (f a)∗
⊢ 1 ≤ a∗

Tactic:
rw [← le, one, kstar]
-- Module: Mathlib.Algebra.Order.Kleene
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 ≤ (f a)∗

Tactic:
one_le_kstar

Premises used: one_le_kstar
-- Module: Mathlib.Algebra.Order.Kleene
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 ≤ (f a)∗

Tactic:
exact one_le_kstar

Premises used: one_le_kstar
-- Module: Mathlib.Algebra.Order.Kleene
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 : β
rw : f a * (f a)∗ ≤ (f a)∗
⊢ a * a∗ ≤ a∗

Tactic:
rw [← le, mul, kstar]
-- Module: Mathlib.Algebra.Order.Kleene
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 : β
⊢ f a * (f a)∗ ≤ (f a)∗

Tactic:
mul_kstar_le_kstar

Premises used: mul_kstar_le_kstar
-- Module: Mathlib.Algebra.Order.Kleene
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 : β
⊢ f a * (f a)∗ ≤ (f a)∗

Tactic:
exact mul_kstar_le_kstar

Premises used: mul_kstar_le_kstar
-- Module: Mathlib.Algebra.Order.Kleene
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 : β
rw : (f a)∗ * f a ≤ (f a)∗
⊢ a∗ * a ≤ a∗

Tactic:
rw [← le, mul, kstar]
-- Module: Mathlib.Algebra.Order.Kleene
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 : β
⊢ (f a)∗ * f a ≤ (f a)∗

Tactic:
kstar_mul_le_kstar

Premises used: kstar_mul_le_kstar
-- Module: Mathlib.Algebra.Order.Kleene
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 : β
⊢ (f a)∗ * f a ≤ (f a)∗

Tactic:
exact kstar_mul_le_kstar

Premises used: kstar_mul_le_kstar
-- Module: Mathlib.Algebra.Order.Kleene
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
rw : f b * (f a)∗ ≤ f b
⊢ b * a∗ ≤ b

Tactic:
rw [← le, mul, kstar]
-- Module: Mathlib.Algebra.Order.Kleene
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

Tactic:
rw [← le, mul] at h
-- Module: Mathlib.Algebra.Order.Kleene
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 : f b * f a ≤ f b
⊢ f b * (f a)∗ ≤ f b

Tactic:
mul_kstar_le_self h

Premises used: mul_kstar_le_self
-- Module: Mathlib.Algebra.Order.Kleene
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 : f b * f a ≤ f b
⊢ f b * (f a)∗ ≤ f b

Tactic:
exact mul_kstar_le_self h

Premises used: mul_kstar_le_self
-- Module: Mathlib.Algebra.Order.Kleene
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
rw : (f a)∗ * f b ≤ f b
⊢ a∗ * b ≤ b

Tactic:
rw [← le, mul, kstar]
-- Module: Mathlib.Algebra.Order.Kleene
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

Tactic:
rw [← le, mul] at h
-- Module: Mathlib.Algebra.Order.Kleene
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 : f a * f b ≤ f b
⊢ (f a)∗ * f b ≤ f b

Tactic:
kstar_mul_le_self h

Premises used: kstar_mul_le_self
-- Module: Mathlib.Algebra.Order.Kleene
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 : f a * f b ≤ f b
⊢ (f a)∗ * f b ≤ f b

Tactic:
exact kstar_mul_le_self h

Premises used: kstar_mul_le_self
-- Module: Mathlib.Algebra.Order.Module.Archimedean
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
⊢ Nontrivial K

Tactic:
have : Nontrivial K := nontrivial_iff.mpr ⟨k, 0, h⟩
-- Module: Mathlib.Algebra.Order.Module.Archimedean
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
⊢ 0 < |k|

Tactic:
simpa using h
-- Module: Mathlib.Algebra.Order.Module.Archimedean
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
obtain : ∀ (m : ℕ) (hm : 1 ≤ m • |k|), Eq (α := ArchimedeanClass M) (mk (k • a)) (mk a)
⊢ Eq (α := ArchimedeanClass M) (mk (k • a)) (mk a)

Tactic:
obtain ⟨m, hm⟩ := Archimedean.arch 1 (show 0 < |k| by simpa using h)

Premises used: Archimedean.arch, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.Module.Archimedean
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|
⊢ LT.lt.{u_2} (α := K) 0 1

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Module.Archimedean
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|
obtain : ∀ (n : ℕ) (hn : |k| ≤ HSMul.hSMul (β := K) n 1), Eq (α := ArchimedeanClass M) (mk (k • a)) (mk a)
⊢ Eq (α := ArchimedeanClass M) (mk (k • a)) (mk a)

Tactic:
obtain ⟨n, hn⟩ := Archimedean.arch |k| (show 0 < 1 by simp)

Premises used: abs, Archimedean.arch
-- Module: Mathlib.Algebra.Order.Module.Archimedean
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
simp_rw : (∃ (m : ℕ), |a| ≤ m • |k| • |a|) ∧ ∃ (n : ℕ), |k| • |a| ≤ n • |a|
⊢ Eq (α := ArchimedeanClass M) (mk (k • a)) (mk a)

Tactic:
simp_rw [mk_eq_mk, abs_smul]

Premises used: abs_smul, ArchimedeanClass.mk_eq_mk
-- Module: Mathlib.Algebra.Order.Module.Archimedean
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|

Tactic:
⟨⟨m, ?_⟩, ⟨n, ?_⟩⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Algebra.Order.Module.Archimedean
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|
refine_2 : |k| • |a| ≤ n • |a|
⊢ (∃ (m : ℕ), |a| ≤ m • |k| • |a|) ∧ ∃ (n : ℕ), |k| • |a| ≤ n • |a|

Tactic:
refine ⟨⟨m, ?_⟩, ⟨n, ?_⟩⟩
-- Module: Mathlib.Algebra.Order.Module.Archimedean
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|
⊢ |a| ≤ m • |k| • |a|

Tactic:
rw [← smul_assoc]

Premises used: smul_assoc
-- Module: Mathlib.Algebra.Order.Module.Archimedean
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
⊢ 0 ≤ |a|

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Module.Archimedean
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|

Tactic:
exact le_smul_of_one_le_left (by simp) hm

Premises used: le_smul_of_one_le_left
-- Module: Mathlib.Algebra.Order.Module.Archimedean
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|
rw₁ rw₂ : n • |a| = n • |a|
⊢ n • |a| = HSMul.hSMul (β := K) n 1 • |a|

Tactic:
rw [smul_assoc, one_smul]

Premises used: smul_assoc, one_smul
-- Module: Mathlib.Algebra.Order.Module.Archimedean
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|

Tactic:
have : n • |a| = (n • (1 : K)) • |a| := by rw [smul_assoc, one_smul]