[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝ : Semiring α
h : ∀ (a : α), a + a = a
src✝ : Semiring α := inst✝
a b c : α
hab : a ≤ b
hbc : b ≤ c
⊢ a ≤ c
[PROOFSTEP]
simp only
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝ : Semiring α
h : ∀ (a : α), a + a = a
src✝ : Semiring α := inst✝
a b c : α
hab : a ≤ b
hbc : b ≤ c
⊢ a + c = c
[PROOFSTEP]
rw [← hbc, ← add_assoc, hab]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝ : Semiring α
h : ∀ (a : α), a + a = a
src✝ : Semiring α := inst✝
a b : α
hab : a ≤ b
hba : b ≤ a
⊢ a = b
[PROOFSTEP]
rwa [← hba, add_comm]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝ : Semiring α
h : ∀ (a : α), a + a = a
src✝ : Semiring α := inst✝
a b : α
⊢ a ≤ a ⊔ b
[PROOFSTEP]
simp only
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝ : Semiring α
h : ∀ (a : α), a + a = a
src✝ : Semiring α := inst✝
a b : α
⊢ a + (a + b) = a + b
[PROOFSTEP]
rw [← add_assoc, h]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝ : Semiring α
h : ∀ (a : α), a + a = a
src✝ : Semiring α := inst✝
a b : α
⊢ b ≤ a ⊔ b
[PROOFSTEP]
simp only
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝ : Semiring α
h : ∀ (a : α), a + a = a
src✝ : Semiring α := inst✝
a b : α
⊢ b + (a + b) = a + b
[PROOFSTEP]
rw [add_comm, add_assoc, h]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝ : Semiring α
h : ∀ (a : α), a + a = a
src✝ : Semiring α := inst✝
a b c : α
hab : a ≤ c
hbc : b ≤ c
⊢ a ⊔ b ≤ c
[PROOFSTEP]
simp only
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝ : Semiring α
h : ∀ (a : α), a + a = a
src✝ : Semiring α := inst✝
a b c : α
hab : a ≤ c
hbc : b ≤ c
⊢ a + b + c = c
[PROOFSTEP]
rwa [add_assoc, hbc]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝ : IdemSemiring α
a✝ b c a : α
⊢ a + a = a
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝ : IdemSemiring α
a✝ b c : α
n : ℕ
x✝ : n + 2 ≠ 0
a : α
⊢ (n + 2) • a = a
[PROOFSTEP]
rw [succ_nsmul, nsmul_eq_self n.succ_ne_zero, add_idem]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝ : IdemSemiring α
a b c : α
⊢ a + b = a ↔ b ≤ a
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝ : IdemSemiring α
a b c : α
⊢ a + b = b ↔ a ≤ b
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝ : IdemSemiring α
a b c : α
⊢ a + b ≤ c ↔ a ≤ c ∧ b ≤ c
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝ : IdemSemiring α
a✝ b✝ c✝ : α
src✝ : IdemSemiring α := inst✝
a b : α
hbc : a ≤ b
c : α
⊢ c + a ≤ c + b
[PROOFSTEP]
simp_rw [add_eq_sup]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝ : IdemSemiring α
a✝ b✝ c✝ : α
src✝ : IdemSemiring α := inst✝
a b : α
hbc : a ≤ b
c : α
⊢ c ⊔ a ≤ c ⊔ b
[PROOFSTEP]
exact sup_le_sup_left hbc _
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝ : IdemSemiring α
a✝ b✝ c : α
src✝ : IdemSemiring α := inst✝
a b : α
⊢ a + (a + b) = a + b
[PROOFSTEP]
rw [← add_assoc, add_idem]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝ : IdemSemiring α
a✝ b✝ c✝ a b c : α
hbc : b ≤ c
⊢ a * c + a * b = a * c
[PROOFSTEP]
rw [← mul_add, hbc.add_eq_left]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝ : IdemSemiring α
a✝ b✝ c✝ a b c : α
hbc : b ≤ c
⊢ swap (fun x x_1 => x * x_1) a c + swap (fun x x_1 => x * x_1) a b = swap (fun x x_1 => x * x_1) a c
[PROOFSTEP]
rw [← add_mul, hbc.add_eq_left]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝ : KleeneAlgebra α
a b c : α
hb : 1 ≤ b
⊢ b * a ≤ b → a∗ ≤ b
[PROOFSTEP]
simpa using mul_kstar_le hb
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝ : KleeneAlgebra α
a b c : α
hb : 1 ≤ b
⊢ a * b ≤ b → a∗ ≤ b
[PROOFSTEP]
simpa using kstar_mul_le hb
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝ : KleeneAlgebra α
a b c : α
h : a ≤ 1
⊢ 1 * a ≤ 1
[PROOFSTEP]
rwa [one_mul]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝ : KleeneAlgebra α
a b c : α
h : a∗ = a
⊢ a * a = a
[PROOFSTEP]
rw [← h, kstar_mul_kstar]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝ : KleeneAlgebra α
a b c : α
n : ℕ
⊢ a ^ (n + 1) ≤ a∗
[PROOFSTEP]
rw [pow_succ]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝ : KleeneAlgebra α
a b c : α
n : ℕ
⊢ a * a ^ n ≤ a∗
[PROOFSTEP]
exact (mul_le_mul_left' pow_le_kstar _).trans mul_kstar_le_kstar
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝⁹ : IdemSemiring α
inst✝⁸ : Zero β
inst✝⁷ : One β
inst✝⁶ : Add β
inst✝⁵ : Mul β
inst✝⁴ : Pow β ℕ
inst✝³ : SMul ℕ β
inst✝² : NatCast β
inst✝¹ : Sup β
inst✝ : Bot β
f : β → α
hf : Injective f
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 : ∀ (x : β) (n : ℕ), f (n • x) = n • f x
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
nat_cast : ∀ (n : ℕ), f ↑n = ↑n
sup : ∀ (a b : β), f (a ⊔ b) = f a ⊔ f b
bot : f ⊥ = ⊥
src✝² : Semiring β := Injective.semiring f hf zero one add mul nsmul npow nat_cast
src✝¹ : SemilatticeSup β := Injective.semilatticeSup f hf sup
src✝ : Bot β := inst✝
a b : β
⊢ f (a + b) = f (a ⊔ b)
[PROOFSTEP]
erw [sup, add, add_eq_sup]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝¹⁰ : KleeneAlgebra α
inst✝⁹ : Zero β
inst✝⁸ : One β
inst✝⁷ : Add β
inst✝⁶ : Mul β
inst✝⁵ : Pow β ℕ
inst✝⁴ : SMul ℕ β
inst✝³ : NatCast β
inst✝² : Sup β
inst✝¹ : Bot β
inst✝ : KStar β
f : β → α
hf : Injective f
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 : ∀ (x : β) (n : ℕ), f (n • x) = n • f x
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
nat_cast : ∀ (n : ℕ), f ↑n = ↑n
sup : ∀ (a b : β), f (a ⊔ b) = f a ⊔ f b
bot : f ⊥ = ⊥
kstar : ∀ (a : β), f a∗ = (f a)∗
src✝¹ : IdemSemiring β := Injective.idemSemiring f hf zero one add mul nsmul npow nat_cast sup bot
src✝ : KStar β := inst✝
a : β
⊢ 1 ≤ f a∗
[PROOFSTEP]
erw [kstar]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝¹⁰ : KleeneAlgebra α
inst✝⁹ : Zero β
inst✝⁸ : One β
inst✝⁷ : Add β
inst✝⁶ : Mul β
inst✝⁵ : Pow β ℕ
inst✝⁴ : SMul ℕ β
inst✝³ : NatCast β
inst✝² : Sup β
inst✝¹ : Bot β
inst✝ : KStar β
f : β → α
hf : Injective f
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 : ∀ (x : β) (n : ℕ), f (n • x) = n • f x
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
nat_cast : ∀ (n : ℕ), f ↑n = ↑n
sup : ∀ (a b : β), f (a ⊔ b) = f a ⊔ f b
bot : f ⊥ = ⊥
kstar : ∀ (a : β), f a∗ = (f a)∗
src✝¹ : IdemSemiring β := Injective.idemSemiring f hf zero one add mul nsmul npow nat_cast sup bot
src✝ : KStar β := inst✝
a : β
⊢ 1 ≤ (f a)∗
[PROOFSTEP]
exact one_le_kstar
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝¹⁰ : KleeneAlgebra α
inst✝⁹ : Zero β
inst✝⁸ : One β
inst✝⁷ : Add β
inst✝⁶ : Mul β
inst✝⁵ : Pow β ℕ
inst✝⁴ : SMul ℕ β
inst✝³ : NatCast β
inst✝² : Sup β
inst✝¹ : Bot β
inst✝ : KStar β
f : β → α
hf : Injective f
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 : ∀ (x : β) (n : ℕ), f (n • x) = n • f x
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
nat_cast : ∀ (n : ℕ), f ↑n = ↑n
sup : ∀ (a b : β), f (a ⊔ b) = f a ⊔ f b
bot : f ⊥ = ⊥
kstar : ∀ (a : β), f a∗ = (f a)∗
src✝¹ : IdemSemiring β := Injective.idemSemiring f hf zero one add mul nsmul npow nat_cast sup bot
src✝ : KStar β := inst✝
a : β
⊢ a * a∗ ≤ a∗
[PROOFSTEP]
change f _ ≤ _
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝¹⁰ : KleeneAlgebra α
inst✝⁹ : Zero β
inst✝⁸ : One β
inst✝⁷ : Add β
inst✝⁶ : Mul β
inst✝⁵ : Pow β ℕ
inst✝⁴ : SMul ℕ β
inst✝³ : NatCast β
inst✝² : Sup β
inst✝¹ : Bot β
inst✝ : KStar β
f : β → α
hf : Injective f
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 : ∀ (x : β) (n : ℕ), f (n • x) = n • f x
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
nat_cast : ∀ (n : ℕ), f ↑n = ↑n
sup : ∀ (a b : β), f (a ⊔ b) = f a ⊔ f b
bot : f ⊥ = ⊥
kstar : ∀ (a : β), f a∗ = (f a)∗
src✝¹ : IdemSemiring β := Injective.idemSemiring f hf zero one add mul nsmul npow nat_cast sup bot
src✝ : KStar β := inst✝
a : β
⊢ f (a * a∗) ≤ f a∗
[PROOFSTEP]
erw [mul, kstar]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝¹⁰ : KleeneAlgebra α
inst✝⁹ : Zero β
inst✝⁸ : One β
inst✝⁷ : Add β
inst✝⁶ : Mul β
inst✝⁵ : Pow β ℕ
inst✝⁴ : SMul ℕ β
inst✝³ : NatCast β
inst✝² : Sup β
inst✝¹ : Bot β
inst✝ : KStar β
f : β → α
hf : Injective f
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 : ∀ (x : β) (n : ℕ), f (n • x) = n • f x
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
nat_cast : ∀ (n : ℕ), f ↑n = ↑n
sup : ∀ (a b : β), f (a ⊔ b) = f a ⊔ f b
bot : f ⊥ = ⊥
kstar : ∀ (a : β), f a∗ = (f a)∗
src✝¹ : IdemSemiring β := Injective.idemSemiring f hf zero one add mul nsmul npow nat_cast sup bot
src✝ : KStar β := inst✝
a : β
⊢ f a * (f a)∗ ≤ (f a)∗
[PROOFSTEP]
exact mul_kstar_le_kstar
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝¹⁰ : KleeneAlgebra α
inst✝⁹ : Zero β
inst✝⁸ : One β
inst✝⁷ : Add β
inst✝⁶ : Mul β
inst✝⁵ : Pow β ℕ
inst✝⁴ : SMul ℕ β
inst✝³ : NatCast β
inst✝² : Sup β
inst✝¹ : Bot β
inst✝ : KStar β
f : β → α
hf : Injective f
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 : ∀ (x : β) (n : ℕ), f (n • x) = n • f x
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
nat_cast : ∀ (n : ℕ), f ↑n = ↑n
sup : ∀ (a b : β), f (a ⊔ b) = f a ⊔ f b
bot : f ⊥ = ⊥
kstar : ∀ (a : β), f a∗ = (f a)∗
src✝¹ : IdemSemiring β := Injective.idemSemiring f hf zero one add mul nsmul npow nat_cast sup bot
src✝ : KStar β := inst✝
a : β
⊢ a∗ * a ≤ a∗
[PROOFSTEP]
change f _ ≤ _
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝¹⁰ : KleeneAlgebra α
inst✝⁹ : Zero β
inst✝⁸ : One β
inst✝⁷ : Add β
inst✝⁶ : Mul β
inst✝⁵ : Pow β ℕ
inst✝⁴ : SMul ℕ β
inst✝³ : NatCast β
inst✝² : Sup β
inst✝¹ : Bot β
inst✝ : KStar β
f : β → α
hf : Injective f
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 : ∀ (x : β) (n : ℕ), f (n • x) = n • f x
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
nat_cast : ∀ (n : ℕ), f ↑n = ↑n
sup : ∀ (a b : β), f (a ⊔ b) = f a ⊔ f b
bot : f ⊥ = ⊥
kstar : ∀ (a : β), f a∗ = (f a)∗
src✝¹ : IdemSemiring β := Injective.idemSemiring f hf zero one add mul nsmul npow nat_cast sup bot
src✝ : KStar β := inst✝
a : β
⊢ f (a∗ * a) ≤ f a∗
[PROOFSTEP]
erw [mul, kstar]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝¹⁰ : KleeneAlgebra α
inst✝⁹ : Zero β
inst✝⁸ : One β
inst✝⁷ : Add β
inst✝⁶ : Mul β
inst✝⁵ : Pow β ℕ
inst✝⁴ : SMul ℕ β
inst✝³ : NatCast β
inst✝² : Sup β
inst✝¹ : Bot β
inst✝ : KStar β
f : β → α
hf : Injective f
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 : ∀ (x : β) (n : ℕ), f (n • x) = n • f x
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
nat_cast : ∀ (n : ℕ), f ↑n = ↑n
sup : ∀ (a b : β), f (a ⊔ b) = f a ⊔ f b
bot : f ⊥ = ⊥
kstar : ∀ (a : β), f a∗ = (f a)∗
src✝¹ : IdemSemiring β := Injective.idemSemiring f hf zero one add mul nsmul npow nat_cast sup bot
src✝ : KStar β := inst✝
a : β
⊢ (f a)∗ * f a ≤ (f a)∗
[PROOFSTEP]
exact kstar_mul_le_kstar
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝¹⁰ : KleeneAlgebra α
inst✝⁹ : Zero β
inst✝⁸ : One β
inst✝⁷ : Add β
inst✝⁶ : Mul β
inst✝⁵ : Pow β ℕ
inst✝⁴ : SMul ℕ β
inst✝³ : NatCast β
inst✝² : Sup β
inst✝¹ : Bot β
inst✝ : KStar β
f : β → α
hf : Injective f
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 : ∀ (x : β) (n : ℕ), f (n • x) = n • f x
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
nat_cast : ∀ (n : ℕ), f ↑n = ↑n
sup : ∀ (a b : β), f (a ⊔ b) = f a ⊔ f b
bot : f ⊥ = ⊥
kstar : ∀ (a : β), f a∗ = (f a)∗
src✝¹ : IdemSemiring β := Injective.idemSemiring f hf zero one add mul nsmul npow nat_cast sup bot
src✝ : KStar β := inst✝
a b : β
h : f (b * a) ≤ f b
⊢ b * a∗ ≤ b
[PROOFSTEP]
change f _ ≤ _
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝¹⁰ : KleeneAlgebra α
inst✝⁹ : Zero β
inst✝⁸ : One β
inst✝⁷ : Add β
inst✝⁶ : Mul β
inst✝⁵ : Pow β ℕ
inst✝⁴ : SMul ℕ β
inst✝³ : NatCast β
inst✝² : Sup β
inst✝¹ : Bot β
inst✝ : KStar β
f : β → α
hf : Injective f
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 : ∀ (x : β) (n : ℕ), f (n • x) = n • f x
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
nat_cast : ∀ (n : ℕ), f ↑n = ↑n
sup : ∀ (a b : β), f (a ⊔ b) = f a ⊔ f b
bot : f ⊥ = ⊥
kstar : ∀ (a : β), f a∗ = (f a)∗
src✝¹ : IdemSemiring β := Injective.idemSemiring f hf zero one add mul nsmul npow nat_cast sup bot
src✝ : KStar β := inst✝
a b : β
h : f (b * a) ≤ f b
⊢ f (b * a∗) ≤ f b
[PROOFSTEP]
erw [mul, kstar]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝¹⁰ : KleeneAlgebra α
inst✝⁹ : Zero β
inst✝⁸ : One β
inst✝⁷ : Add β
inst✝⁶ : Mul β
inst✝⁵ : Pow β ℕ
inst✝⁴ : SMul ℕ β
inst✝³ : NatCast β
inst✝² : Sup β
inst✝¹ : Bot β
inst✝ : KStar β
f : β → α
hf : Injective f
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 : ∀ (x : β) (n : ℕ), f (n • x) = n • f x
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
nat_cast : ∀ (n : ℕ), f ↑n = ↑n
sup : ∀ (a b : β), f (a ⊔ b) = f a ⊔ f b
bot : f ⊥ = ⊥
kstar : ∀ (a : β), f a∗ = (f a)∗
src✝¹ : IdemSemiring β := Injective.idemSemiring f hf zero one add mul nsmul npow nat_cast sup bot
src✝ : KStar β := inst✝
a b : β
h : f (b * a) ≤ f b
⊢ f b * (f a)∗ ≤ f b
[PROOFSTEP]
erw [mul] at h 
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝¹⁰ : KleeneAlgebra α
inst✝⁹ : Zero β
inst✝⁸ : One β
inst✝⁷ : Add β
inst✝⁶ : Mul β
inst✝⁵ : Pow β ℕ
inst✝⁴ : SMul ℕ β
inst✝³ : NatCast β
inst✝² : Sup β
inst✝¹ : Bot β
inst✝ : KStar β
f : β → α
hf : Injective f
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 : ∀ (x : β) (n : ℕ), f (n • x) = n • f x
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
nat_cast : ∀ (n : ℕ), f ↑n = ↑n
sup : ∀ (a b : β), f (a ⊔ b) = f a ⊔ f b
bot : f ⊥ = ⊥
kstar : ∀ (a : β), f a∗ = (f a)∗
src✝¹ : IdemSemiring β := Injective.idemSemiring f hf zero one add mul nsmul npow nat_cast sup bot
src✝ : KStar β := inst✝
a b : β
h : f b * f a ≤ f b
⊢ f b * (f a)∗ ≤ f b
[PROOFSTEP]
exact mul_kstar_le_self h
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝¹⁰ : KleeneAlgebra α
inst✝⁹ : Zero β
inst✝⁸ : One β
inst✝⁷ : Add β
inst✝⁶ : Mul β
inst✝⁵ : Pow β ℕ
inst✝⁴ : SMul ℕ β
inst✝³ : NatCast β
inst✝² : Sup β
inst✝¹ : Bot β
inst✝ : KStar β
f : β → α
hf : Injective f
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 : ∀ (x : β) (n : ℕ), f (n • x) = n • f x
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
nat_cast : ∀ (n : ℕ), f ↑n = ↑n
sup : ∀ (a b : β), f (a ⊔ b) = f a ⊔ f b
bot : f ⊥ = ⊥
kstar : ∀ (a : β), f a∗ = (f a)∗
src✝¹ : IdemSemiring β := Injective.idemSemiring f hf zero one add mul nsmul npow nat_cast sup bot
src✝ : KStar β := inst✝
a b : β
h : f (a * b) ≤ f b
⊢ a∗ * b ≤ b
[PROOFSTEP]
change f _ ≤ _
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝¹⁰ : KleeneAlgebra α
inst✝⁹ : Zero β
inst✝⁸ : One β
inst✝⁷ : Add β
inst✝⁶ : Mul β
inst✝⁵ : Pow β ℕ
inst✝⁴ : SMul ℕ β
inst✝³ : NatCast β
inst✝² : Sup β
inst✝¹ : Bot β
inst✝ : KStar β
f : β → α
hf : Injective f
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 : ∀ (x : β) (n : ℕ), f (n • x) = n • f x
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
nat_cast : ∀ (n : ℕ), f ↑n = ↑n
sup : ∀ (a b : β), f (a ⊔ b) = f a ⊔ f b
bot : f ⊥ = ⊥
kstar : ∀ (a : β), f a∗ = (f a)∗
src✝¹ : IdemSemiring β := Injective.idemSemiring f hf zero one add mul nsmul npow nat_cast sup bot
src✝ : KStar β := inst✝
a b : β
h : f (a * b) ≤ f b
⊢ f (a∗ * b) ≤ f b
[PROOFSTEP]
erw [mul, kstar]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝¹⁰ : KleeneAlgebra α
inst✝⁹ : Zero β
inst✝⁸ : One β
inst✝⁷ : Add β
inst✝⁶ : Mul β
inst✝⁵ : Pow β ℕ
inst✝⁴ : SMul ℕ β
inst✝³ : NatCast β
inst✝² : Sup β
inst✝¹ : Bot β
inst✝ : KStar β
f : β → α
hf : Injective f
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 : ∀ (x : β) (n : ℕ), f (n • x) = n • f x
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
nat_cast : ∀ (n : ℕ), f ↑n = ↑n
sup : ∀ (a b : β), f (a ⊔ b) = f a ⊔ f b
bot : f ⊥ = ⊥
kstar : ∀ (a : β), f a∗ = (f a)∗
src✝¹ : IdemSemiring β := Injective.idemSemiring f hf zero one add mul nsmul npow nat_cast sup bot
src✝ : KStar β := inst✝
a b : β
h : f (a * b) ≤ f b
⊢ (f a)∗ * f b ≤ f b
[PROOFSTEP]
erw [mul] at h 
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝¹⁰ : KleeneAlgebra α
inst✝⁹ : Zero β
inst✝⁸ : One β
inst✝⁷ : Add β
inst✝⁶ : Mul β
inst✝⁵ : Pow β ℕ
inst✝⁴ : SMul ℕ β
inst✝³ : NatCast β
inst✝² : Sup β
inst✝¹ : Bot β
inst✝ : KStar β
f : β → α
hf : Injective f
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 : ∀ (x : β) (n : ℕ), f (n • x) = n • f x
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
nat_cast : ∀ (n : ℕ), f ↑n = ↑n
sup : ∀ (a b : β), f (a ⊔ b) = f a ⊔ f b
bot : f ⊥ = ⊥
kstar : ∀ (a : β), f a∗ = (f a)∗
src✝¹ : IdemSemiring β := Injective.idemSemiring f hf zero one add mul nsmul npow nat_cast sup bot
src✝ : KStar β := inst✝
a b : β
h : f a * f b ≤ f b
⊢ (f a)∗ * f b ≤ f b
[PROOFSTEP]
exact kstar_mul_le_self h
