awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Interval.Set.SuccPred
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : One α
inst_2 : Add α
inst_3 : Sub α
inst_4 : SuccAddOrder α
inst_5 : PredSubOrder α
inst_6 : Nontrivial α
a b : α
⊢ Icc (a + 1) (b - 1) = Ioo a b

Tactic:
simpa [succ_eq_add_one, pred_eq_sub_one] using Icc_succ_pred_eq_Ioo a b

Premises used: Order.succ_eq_add_one, Set.Icc_succ_pred_eq_Ioo, Order.pred_eq_sub_one
-- Module: Mathlib.Algebra.Order.Interval.Set.SuccPred
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : One α
inst_2 : Add α
inst_3 : SuccAddOrder α
b : α
hb : ¬IsMax b
⊢ Iio (b + 1) = Iic b

Tactic:
simpa [succ_eq_add_one] using Iio_succ_eq_Iic_of_not_isMax hb

Premises used: Order.succ_eq_add_one, Set.Iio_succ_eq_Iic_of_not_isMax
-- Module: Mathlib.Algebra.Order.Interval.Set.SuccPred
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : One α
inst_2 : Add α
inst_3 : SuccAddOrder α
inst_4 : NoMaxOrder α
b : α
⊢ Iio (b + 1) = Iic b

Tactic:
simpa [succ_eq_add_one] using Iio_succ_eq_Iic b

Premises used: Set.Iio_succ_eq_Iic, Order.succ_eq_add_one
-- Module: Mathlib.Algebra.Order.Interval.Set.SuccPred
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : One α
inst_2 : Sub α
inst_3 : PredSubOrder α
b : α
hb : ¬IsMin b
⊢ Iic (b - 1) = Iio b

Tactic:
simpa [pred_eq_sub_one] using Iic_pred_eq_Iio_of_not_isMin hb

Premises used: Set.Iic_pred_eq_Iio_of_not_isMin, Order.pred_eq_sub_one
-- Module: Mathlib.Algebra.Order.Interval.Set.SuccPred
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : One α
inst_2 : Sub α
inst_3 : PredSubOrder α
inst_4 : NoMinOrder α
b : α
⊢ Iic (b - 1) = Iio b

Tactic:
simpa [pred_eq_sub_one] using Iic_pred_eq_Iio b

Premises used: Order.pred_eq_sub_one, Set.Iic_pred_eq_Iio
-- Module: Mathlib.Algebra.Order.Interval.Set.SuccPred
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : One α
inst_2 : Add α
inst_3 : SuccAddOrder α
a : α
ha : ¬IsMax a
⊢ Ici (a + 1) = Ioi a

Tactic:
simpa [succ_eq_add_one] using Ici_succ_eq_Ioi_of_not_isMax ha

Premises used: Order.succ_eq_add_one, Set.Ici_succ_eq_Ioi_of_not_isMax
-- Module: Mathlib.Algebra.Order.Interval.Set.SuccPred
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : One α
inst_2 : Add α
inst_3 : SuccAddOrder α
inst_4 : NoMaxOrder α
a : α
⊢ Ici (a + 1) = Ioi a

Tactic:
simpa [succ_eq_add_one] using Ici_succ_eq_Ioi a

Premises used: Order.succ_eq_add_one, Set.Ici_succ_eq_Ioi
-- Module: Mathlib.Algebra.Order.Interval.Set.SuccPred
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : One α
inst_2 : Sub α
inst_3 : PredSubOrder α
a : α
ha : ¬IsMin a
⊢ Ioi (a - 1) = Ici a

Tactic:
simpa [pred_eq_sub_one] using Ioi_pred_eq_Ici_of_not_isMin ha

Premises used: Set.Ioi_pred_eq_Ici_of_not_isMin, Order.pred_eq_sub_one
-- Module: Mathlib.Algebra.Order.Interval.Set.SuccPred
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : One α
inst_2 : Sub α
inst_3 : PredSubOrder α
inst_4 : NoMinOrder α
a : α
⊢ Ioi (a - 1) = Ici a

Tactic:
simpa [pred_eq_sub_one] using Ioi_pred_eq_Ici a

Premises used: Set.Ioi_pred_eq_Ici, Order.pred_eq_sub_one
-- Module: Mathlib.Algebra.Order.Invertible
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a : R
inst_3 : Invertible a
⊢ 0 < a * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _

Tactic:
simp only [mul_invOf_self, zero_lt_one]

Premises used: mul_invOf_self, zero_lt_one
-- Module: Mathlib.Algebra.Order.Invertible
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a : R
inst_3 : Invertible a
⊢ @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ ≤ 0 ↔ a ≤ 0

Tactic:
simp only [← not_lt, invOf_pos]

Premises used: invOf_pos, not_lt
-- Module: Mathlib.Algebra.Order.Invertible
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a : R
inst_3 : Invertible a
⊢ @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ < 0 ↔ a < 0

Tactic:
simp only [← not_le, invOf_nonneg]

Premises used: not_le, invOf_nonneg
-- Module: Mathlib.Algebra.Order.Invertible
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a : R
inst_3 : Invertible a
h : 1 ≤ a
⊢ @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ ≤ 1

Tactic:
mul_invOf_self a ▸ le_mul_of_one_le_left (invOf_nonneg.2 <| zero_le_one.trans h) h

Premises used: Iff.mpr, le_mul_of_one_le_left, invOf_nonneg, Eq.rec, mul_invOf_self, zero_le_one, LE.le.trans
-- Module: Mathlib.Algebra.Order.Invertible
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a : R
inst_3 : Invertible a
h : 1 < a
⊢ @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ < 1

Tactic:
mul_invOf_self a ▸ lt_mul_of_one_lt_left (invOf_pos.2 <| one_pos.trans h) h

Premises used: Iff.mpr, invOf_pos, Eq.rec, mul_invOf_self, LT.lt.trans, one_pos, lt_mul_of_one_lt_left
-- Module: Mathlib.Algebra.Order.Invertible
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Nontrivial R
n : ℕ
inst_4 : Invertible (α := R) (↑n : R)
⊢ LT.lt.{u_1} (α := R) 0 (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑n : R) _)

Tactic:
invOf_pos.2 <| Nat.cast_pos.2 <| pos_of_invertible_cast (R := R) n

Premises used: Iff.mpr, Nat.cast_pos, invOf_pos, pos_of_invertible_cast
-- Module: Mathlib.Algebra.Order.IsBotOne
Goal:
α : Type u_1
inst : LE α
inst_1 : One α
inst_2 : IsBotOneClass α
⊢ IsBot.{u_1} (α := α) 1

Tactic:
IsBotOneClass.isBot_one

Premises used: IsBotOneClass.isBot_one
-- Module: Mathlib.Algebra.Order.IsBotOne
Goal:
α : Type u_1
inst : LE α
inst_1 : One α
inst_2 : IsBotOneClass α
a : α
⊢ 1 ≤ a

Tactic:
isBot_one a

Premises used: isBot_one
-- Module: Mathlib.Algebra.Order.IsBotOne
Goal:
α : Type u_1
a : α
inst : Preorder α
inst_1 : One α
inst_2 : IsBotOneClass α
⊢ ¬a < 1

Tactic:
one_le.not_gt

Premises used: LE.le.not_gt, one_le
-- Module: Mathlib.Algebra.Order.IsBotOne
Goal:
α : Type u_1
a b : α
inst : Preorder α
inst_1 : One α
inst_2 : IsBotOneClass α
h : a < b
⊢ 1 < b

Tactic:
one_le.trans_lt h

Premises used: one_le, LE.le.trans_lt
-- Module: Mathlib.Algebra.Order.IsBotOne
Goal:
α : Type u_1
a b : α
inst : Preorder α
inst_1 : One α
inst_2 : IsBotOneClass α
h : a < b
⊢ b ≠ 1

Tactic:
h.one_lt.ne'

Premises used: LT.lt.ne', LT.lt.one_lt
-- Module: Mathlib.Algebra.Order.IsBotOne
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : One α
inst_2 : IsBotOneClass α
inst_3 : OrderBot α
⊢ Eq.{u_1 + 1} (α := α) ⊥ 1

Tactic:
isBot_one.eq_bot.symm

Premises used: IsBot.eq_bot, isBot_one, Eq.symm
-- Module: Mathlib.Algebra.Order.IsBotOne
Goal:
α : Type u_1
a : α
inst : PartialOrder α
inst_1 : One α
inst_2 : IsBotOneClass α
⊢ a ≤ 1 ↔ a = 1

Tactic:
one_le.ge_iff_eq'

Premises used: LE.le.ge_iff_eq', one_le
-- Module: Mathlib.Algebra.Order.IsBotOne
Goal:
α : Type u_1
a : α
inst : PartialOrder α
inst_1 : One α
inst_2 : IsBotOneClass α
⊢ 1 < a ↔ a ≠ 1

Tactic:
one_le.lt_iff_ne.trans ne_comm

Premises used: LE.le.lt_iff_ne, Iff.trans, ne_comm, one_le
-- Module: Mathlib.Algebra.Order.IsBotOne
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : One α
inst_2 : IsBotOneClass α
a : α
⊢ a = 1 ∨ 1 < a

Tactic:
one_le.eq_or_lt'

Premises used: one_le, LE.le.eq_or_lt'
-- Module: Mathlib.Algebra.Order.IsBotOne
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : One α
inst_2 : IsBotOneClass α
s : Set α
⊢ ¬1 ∈ s ↔ ∀ (x : α), x ∈ s → 1 < x

Tactic:
let := IsBotOneClass.toOrderBot α
  bot_notMem_iff

Premises used: Set.Mem, IsBotOneClass.toOrderBot, bot_notMem_iff
-- Module: Mathlib.Algebra.Order.IsBotOne
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : One α
inst_2 : IsBotOneClass α
a : α
⊢ min 1 a = 1

Tactic:
simp
-- Module: Mathlib.Algebra.Order.IsBotOne
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : One α
inst_2 : IsBotOneClass α
a : α
⊢ min a 1 = 1

Tactic:
simp
-- Module: Mathlib.Algebra.Order.IsBotOne
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : One α
inst_2 : IsBotOneClass α
a : α
⊢ max 1 a = a

Tactic:
simp
-- Module: Mathlib.Algebra.Order.IsBotOne
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : One α
inst_2 : IsBotOneClass α
a : α
⊢ max a 1 = a

Tactic:
simp
-- Module: Mathlib.Algebra.Order.IsBotOne
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : One α
inst_2 : IsBotOneClass α
a b : α
⊢ max a b = 1 ↔ a = 1 ∧ b = 1

Tactic:
let := IsBotOneClass.toOrderBot α
  max_eq_bot

Premises used: max_eq_bot, IsBotOneClass.toOrderBot
-- Module: Mathlib.Algebra.Order.IsBotOne
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : One α
inst_2 : IsBotOneClass α
a b : α
⊢ min a b = 1 ↔ a = 1 ∨ b = 1

Tactic:
let := IsBotOneClass.toOrderBot α
  min_eq_bot

Premises used: min_eq_bot, IsBotOneClass.toOrderBot
-- Module: Mathlib.Algebra.Order.IsBotOne
Goal:
α : Type u_1
a b : α
inst : Zero α
inst_1 : Preorder α
inst_2 : IsBotZeroClass α
h : a < b
⊢ NeZero b

Tactic:
⟨h.ne_zero⟩

Premises used: NeZero.mk, LT.lt.ne_zero
-- Module: Mathlib.Algebra.Order.IsBotOne
Goal:
α : Type u_1
inst : Zero α
inst_1 : PartialOrder α
inst_2 : IsBotZeroClass α
a : α
inst_3 : NeZero a
⊢ 0 < a

Tactic:
NeZero.out.pos

Premises used: Ne.pos, NeZero.out
-- Module: Mathlib.Algebra.Order.IsBotOne
Goal:
α : Type u_1
a b : α
inst : Zero α
inst_1 : Preorder α
inst_2 : IsBotZeroClass α
inst_3 : One α
inst_4 : Fact (1 < a)
⊢ NeZero a

Tactic:
of_gt <| @Fact.out (1 < a) _

Premises used: NeZero.of_gt, Fact.out
-- Module: Mathlib.Algebra.Order.IsBotOne
Goal:
α : Type u_1
a b : α
inst : Zero α
inst_1 : PartialOrder α
inst_2 : IsBotZeroClass α
inst_3 : NeZero a
h : a ≤ b
⊢ NeZero b

Tactic:
⟨((pos a).trans_le h).ne_zero⟩

Premises used: NeZero.mk, LT.lt.trans_le, NeZero.pos, LT.lt.ne_zero
-- Module: Mathlib.Algebra.Order.Kleene
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst : Semiring α
h : ∀ (a : α), a + a = a
a b c : α
hab : a + b = b
hbc : b + c = c
rw : a + (b + c) = b + c
rw₁ : a + b + c = b + c
rw₂ rw₃ : b + c = b + c
⊢ a + c = c

Tactic:
rw [← hbc, ← add_assoc, hab]

Premises used: add_assoc
-- Module: Mathlib.Algebra.Order.Kleene
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst : Semiring α
h : ∀ (a : α), a + a = a
a b : α
hab : a + b = b
hba : b + a = a
rwa : b + a = b
rwa₁ rwa₂ rwa₃ rwa₄ : a + b = b
⊢ a = b

Tactic:
rwa [← hba, add_comm]

Premises used: add_comm
-- Module: Mathlib.Algebra.Order.Kleene
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst : Semiring α
h : ∀ (a : α), a + a = a
a b : α
rw : a + a + b = a + b
rw₁ rw₂ : a + b = a + b
⊢ a + (a + b) = a + b

Tactic:
rw [← add_assoc, h]

Premises used: add_assoc
-- Module: Mathlib.Algebra.Order.Kleene
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst : Semiring α
h : ∀ (a : α), a + a = a
a b : α
rw : a + b + b = a + b
rw₁ : a + (b + b) = a + b
rw₂ rw₃ : a + b = a + b
⊢ b + (a + b) = a + b

Tactic:
rw [add_comm, add_assoc, h]

Premises used: add_assoc, add_comm
-- Module: Mathlib.Algebra.Order.Kleene
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst : Semiring α
h : ∀ (a : α), a + a = a
a b c : α
hab : a + c = c
hbc : b + c = c
rwa : a + (b + c) = c
rwa₁ rwa₂ rwa₃ rwa₄ : a + c = c
⊢ a + b + c = c

Tactic:
rwa [add_assoc, hbc]

Premises used: add_assoc
-- Module: Mathlib.Algebra.Order.Kleene
Goal:
α : Type u_1
inst : IdemSemiring α
a b : α
⊢ a + b = a ⊔ b

Tactic:
IdemSemiring.add_eq_sup _ _

Premises used: IdemSemiring.add_eq_sup
-- Module: Mathlib.Algebra.Order.Kleene
Goal:
α : Type u_1
inst : IdemSemiring α
a : α
⊢ a + a = a

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Kleene
Goal:
α : Type u_1
inst : IdemSemiring α
n : ℕ
nezero : n ≠ 0
⊢ 1 ≤ n

Tactic:
rw [← Nat.one_le_iff_ne_zero] at nezero

Premises used: Nat.one_le_iff_ne_zero
-- Module: Mathlib.Algebra.Order.Kleene
Goal:
α : Type u_1
inst : IdemSemiring α
n : ℕ
⊢ Eq.{u_1 + 1} (α := α) (↑1 : α) 1

Tactic:
Nat.cast_one

Premises used: Nat.cast_one
-- Module: Mathlib.Algebra.Order.Kleene
Goal:
α : Type u_1
inst : IdemSemiring α
n : ℕ
⊢ Eq.{u_1 + 1} (α := α) (↑1 : α) 1

Tactic:
exact Nat.cast_one

Premises used: Nat.cast_one
-- Module: Mathlib.Algebra.Order.Kleene
Goal:
α : Type u_1
inst : IdemSemiring α
n x : ℕ
hmn : 1 ≤ x
hx : Eq.{u_1 + 1} (α := α) (↑x : α) 1
succ : HAdd.hAdd (α := α) (↑x : α) (↑1 : α) = 1
succ₁ : HAdd.hAdd (α := α) 1 (↑1 : α) = 1
succ₂ : HAdd.hAdd (α := α) 1 1 = 1
succ₃ succ₄ : Eq.{u_1 + 1} (α := α) 1 1
⊢ Eq.{u_1 + 1} (α := α) (↑(x + 1) : α) 1

Tactic:
rw [Nat.cast_add, hx, Nat.cast_one, add_idem 1]

Premises used: Nat.cast_add, add_idem, OfNat.ofNat, Nat.cast_one
-- Module: Mathlib.Algebra.Order.Kleene
Goal:
α : Type u_1
inst : IdemSemiring α
n : ℕ
nezero : 1 ≤ n
base : Eq.{u_1 + 1} (α := α) (↑1 : α) 1
succ : ∀ (x : ℕ), 1 ≤ x → ∀ (hx : Eq.{u_1 + 1} (α := α) (↑x : α) 1), Eq.{u_1 + 1} (α := α) (↑(x + 1) : α) 1
⊢ Eq.{u_1 + 1} (α := α) (↑n : α) 1

Tactic:
induction n, nezero using Nat.le_induction with
  | base => exact Nat.cast_one
  | succ x _ hx => rw [Nat.cast_add, hx, Nat.cast_one, add_idem 1]

Premises used: Nat.cast_add, add_idem, OfNat.ofNat, Nat.cast_one
-- Module: Mathlib.Algebra.Order.Kleene
Goal:
α : Type u_1
inst : IdemSemiring α
n : ℕ
inst_1 : n.AtLeastTwo
⊢ Eq.{u_1 + 1} (α := α) (OfNat.ofNat n) 1

Tactic:
natCast_eq_one <| Nat.ne_zero_of_lt Nat.AtLeastTwo.prop

Premises used: Nat.AtLeastTwo.prop, natCast_eq_one, Nat.ne_zero_of_lt
-- Module: Mathlib.Algebra.Order.Kleene
Goal:
α : Type u_1
inst : IdemSemiring α
n : ℕ
h : n + 2 ≠ 0
a : α
rw : (n + 1) • a + a = a
rw₁ : a + a = a
rw₂ rw₃ : a = a
⊢ (n + 2) • a = a

Tactic:
rw [succ_nsmul, nsmul_eq_self n.succ_ne_zero, add_idem]

Premises used: Nat.succ_ne_zero, add_idem, succ_nsmul
-- Module: Mathlib.Algebra.Order.Kleene
Goal:
α : Type u_1
inst : IdemSemiring α
a b : α
⊢ a + b = a ↔ b ≤ a

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Kleene
Goal:
α : Type u_1
inst : IdemSemiring α
a b : α
⊢ a + b = b ↔ a ≤ b

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Kleene
Goal:
α : Type u_1
inst : IdemSemiring α
a b c : α
⊢ a + b ≤ c ↔ a ≤ c ∧ b ≤ c

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Kleene
Goal:
α : Type u_1
inst : IdemSemiring α
a b c : α
ha : a ≤ c
hb : b ≤ c
⊢ a + b ≤ c

Tactic:
add_le_iff.2 ⟨ha, hb⟩

Premises used: Iff.mpr, add_le_iff, And.intro
-- Module: Mathlib.Algebra.Order.Kleene
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst : IdemSemiring α
a_1 b_1 c_1 a b : α
hbc : a ≤ b
c : α
simp_rw : a ⊔ c ≤ b ⊔ c
⊢ a + c ≤ b + c

Tactic:
simp_rw [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 : IdemSemiring α
a_1 b_1 c_1 a b : α
hbc : a ≤ b
c : α
grw grw₁ : b ⊔ c ≤ b ⊔ c
⊢ a ⊔ c ≤ b ⊔ c

Tactic:
grw [hbc]
-- Module: Mathlib.Algebra.Order.Kleene
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst : IdemSemiring α
a_1 b_1 c a b : α
rw : b + (a + a) = b + a
rw₁ rw₂ : b + a = b + a
⊢ b + a + a = b + a

Tactic:
rw [add_assoc, add_idem]

Premises used: add_assoc, add_idem
-- Module: Mathlib.Algebra.Order.Kleene
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst : IdemSemiring α
a_1 b_1 c a b : α
rw : a + a + b = a + b
rw₁ rw₂ : a + b = a + b
⊢ a + (a + b) = a + b

Tactic:
rw [← add_assoc, add_idem]

Premises used: add_assoc, add_idem
-- Module: Mathlib.Algebra.Order.Kleene
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst : IdemSemiring α
a_1 b_1 c_1 a b c : α
hbc : (fun (x1 x2 : α) ↦ x1 ≤ x2) b c
rw : a * (c + b) = (fun (x1 x2 : α) ↦ x1 * x2) a c
rw₁ rw₂ : a * c = (fun (x1 x2 : α) ↦ x1 * x2) a c
⊢ HAdd.hAdd (α := α) ((fun (x1 x2 : α) ↦ x1 * x2) a c) ((fun (x1 x2 : α) ↦ x1 * x2) a b) =
    (fun (x1 x2 : α) ↦ x1 * x2) a c

Tactic:
rw [← mul_add, hbc.add_eq_left]

Premises used: mul_add, LE.le.add_eq_left
-- Module: Mathlib.Algebra.Order.Kleene
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst : IdemSemiring α
a_1 b_1 c_1 a b c : α
hbc : (fun (x1 x2 : α) ↦ x1 ≤ x2) b c
rw : (c + b) * a = swap (φ := fun (a a_2 : α) ↦ α) (fun (x1 x2 : α) ↦ x1 * x2) a c
rw₁ rw₂ : c * a = swap (φ := fun (a a_2 : α) ↦ α) (fun (x1 x2 : α) ↦ x1 * x2) a c
⊢ HAdd.hAdd (α := α) (β := α) (swap (φ := fun (a a_2 : α) ↦ α) (fun (x1 x2 : α) ↦ x1 * x2) a c : α)
      (swap (φ := fun (a a_2 : α) ↦ α) (fun (x1 x2 : α) ↦ x1 * x2) a b : α) =
    swap (φ := fun (a a_2 : α) ↦ α) (fun (x1 x2 : α) ↦ x1 * x2) a c

Tactic:
rw [← add_mul, hbc.add_eq_left]

Premises used: add_mul, LE.le.add_eq_left
-- Module: Mathlib.Algebra.Order.Kleene
Goal:
α : Type u_1
inst : KleeneAlgebra α
a : α
⊢ 1 ≤ a∗

Tactic:
KleeneAlgebra.one_le_kstar _

Premises used: KleeneAlgebra.one_le_kstar
-- Module: Mathlib.Algebra.Order.Kleene
Goal:
α : Type u_1
inst : KleeneAlgebra α
a : α
⊢ a * a∗ ≤ a∗

Tactic:
KleeneAlgebra.mul_kstar_le_kstar _

Premises used: KleeneAlgebra.mul_kstar_le_kstar
-- Module: Mathlib.Algebra.Order.Kleene
Goal:
α : Type u_1
inst : KleeneAlgebra α
a : α
⊢ a∗ * a ≤ a∗

Tactic:
KleeneAlgebra.kstar_mul_le_kstar _

Premises used: KleeneAlgebra.kstar_mul_le_kstar
-- Module: Mathlib.Algebra.Order.Kleene
Goal:
α : Type u_1
inst : KleeneAlgebra α
a b : α
⊢ b * a ≤ b → b * a∗ ≤ b

Tactic:
KleeneAlgebra.mul_kstar_le_self _ _

Premises used: KleeneAlgebra.mul_kstar_le_self
-- Module: Mathlib.Algebra.Order.Kleene
Goal:
α : Type u_1
inst : KleeneAlgebra α
a b : α
⊢ a * b ≤ b → a∗ * b ≤ b

Tactic:
KleeneAlgebra.kstar_mul_le_self _ _

Premises used: KleeneAlgebra.kstar_mul_le_self
-- Module: Mathlib.Algebra.Order.Kleene
Goal:
α : Type u_1
inst : KleeneAlgebra α
a b c : α
hb : b ≤ c
ha : c * a ≤ c
grw : c * a∗ ≤ c
grw₁ grw₂ : c ≤ c
⊢ b * a∗ ≤ c

Tactic:
grw [hb, mul_kstar_le_self ha]

Premises used: mul_kstar_le_self
-- Module: Mathlib.Algebra.Order.Kleene
Goal:
α : Type u_1
inst : KleeneAlgebra α
a b c : α
hb : b ≤ c
ha : a * c ≤ c
grw : a∗ * c ≤ c
grw₁ grw₂ : c ≤ c
⊢ a∗ * b ≤ c

Tactic:
grw [hb, kstar_mul_le_self ha]

Premises used: kstar_mul_le_self
-- Module: Mathlib.Algebra.Order.Kleene
Goal:
α : Type u_1
inst : KleeneAlgebra α
a b : α
hb : 1 ≤ b
⊢ b * a ≤ b → a∗ ≤ b

Tactic:
simpa using mul_kstar_le hb

Premises used: mul_kstar_le
-- Module: Mathlib.Algebra.Order.Kleene
Goal:
α : Type u_1
inst : KleeneAlgebra α
a b : α
hb : 1 ≤ b
⊢ a * b ≤ b → a∗ ≤ b

Tactic:
simpa using kstar_mul_le hb

Premises used: kstar_mul_le
-- Module: Mathlib.Algebra.Order.Kleene
Goal:
α : Type u_1
inst : KleeneAlgebra α
a : α
⊢ a ≤ a∗

Tactic:
le_trans (le_mul_of_one_le_left' one_le_kstar) kstar_mul_le_kstar

Premises used: one_le_kstar, le_mul_of_one_le_left', kstar_mul_le_kstar, le_trans
-- Module: Mathlib.Algebra.Order.Kleene
Goal:
α : Type u_1
inst : KleeneAlgebra α
⊢ Monotone.{u_1, u_1} (α := α) KStar.kstar

Tactic:
fun _ _ h ↦
    kstar_le_of_mul_le_left one_le_kstar <| kstar_mul_le (h.trans le_kstar) <| mul_kstar_le_kstar

Premises used: kstar_le_of_mul_le_left, Monotone, one_le_kstar, le_kstar, LE.le.trans, kstar_mul_le, mul_kstar_le_kstar
-- Module: Mathlib.Algebra.Order.Kleene
Goal:
α : Type u_1
inst : KleeneAlgebra α
a : α
h rwa rwa₁ rwa₂ rwa₃ : a ≤ 1
⊢ 1 * a ≤ 1

Tactic:
rwa [one_mul]

Premises used: one_mul
-- Module: Mathlib.Algebra.Order.Kleene
Goal:
α : Type u_1
inst : KleeneAlgebra α
⊢ Eq.{u_1 + 1} (α := α) 0∗ 1

Tactic:
kstar_eq_one.2 zero_le

Premises used: Iff.mpr, zero_le, kstar_eq_one
-- Module: Mathlib.Algebra.Order.Kleene
Goal:
α : Type u_1
inst : KleeneAlgebra α
⊢ Eq.{u_1 + 1} (α := α) 1∗ 1

Tactic:
kstar_eq_one.2 le_rfl

Premises used: Iff.mpr, le_rfl, kstar_eq_one
-- Module: Mathlib.Algebra.Order.Kleene
Goal:
α : Type u_1
inst : KleeneAlgebra α
a : α
⊢ a∗ * a∗ = a∗

Tactic:
(mul_kstar_le le_rfl <| kstar_mul_le_kstar).antisymm <| le_mul_of_one_le_left' one_le_kstar

Premises used: le_rfl, LE.le.antisymm, one_le_kstar, le_mul_of_one_le_left', mul_kstar_le, kstar_mul_le_kstar
-- Module: Mathlib.Algebra.Order.Kleene
Goal:
α : Type u_1
inst : KleeneAlgebra α
a : α
h : a∗ = a
rw : a∗ * a∗ = a∗
rw₁ rw₂ : a∗ = a∗
⊢ a * a = a

Tactic:
rw [← h, kstar_mul_kstar]

Premises used: kstar_mul_kstar
-- Module: Mathlib.Algebra.Order.Kleene
Goal:
α : Type u_1
inst : KleeneAlgebra α
a : α
⊢ a∗∗ = a∗

Tactic:
kstar_eq_self.2 ⟨kstar_mul_kstar _, one_le_kstar⟩

Premises used: Iff.mpr, one_le_kstar, kstar_mul_kstar, And.intro, kstar_eq_self
-- Module: Mathlib.Algebra.Order.Kleene
Goal:
α : Type u_1
inst : KleeneAlgebra α
a : α
n : ℕ
grw : a * a ^ n ≤ a∗
grw₁ : a * a∗ ≤ a∗
grw₂ grw₃ : a∗ ≤ a∗
⊢ a ^ (n + 1) ≤ a∗

Tactic:
grw [pow_succ', pow_le_kstar, mul_kstar_le_kstar]

Premises used: pow_succ', mul_kstar_le_kstar
-- Module: Mathlib.Algebra.Order.Kleene
Goal:
α : Type u_1
inst : KleeneAlgebra α
a : α
rw : 1 ≤ a∗ ∧ a * a∗ ≤ a∗
⊢ 1 + a * a∗ ≤ a∗

Tactic:
rw [add_le_iff]

Premises used: add_le_iff
-- Module: Mathlib.Algebra.Order.Kleene
Goal:
α : Type u_1
inst : KleeneAlgebra α
a : α
⊢ 1 ≤ a∗ ∧ a * a∗ ≤ a∗

Tactic:
⟨one_le_kstar, mul_kstar_le_kstar⟩

Premises used: one_le_kstar, And.intro, mul_kstar_le_kstar
-- Module: Mathlib.Algebra.Order.Kleene
Goal:
α : Type u_1
inst : KleeneAlgebra α
a : α
⊢ 1 ≤ a∗ ∧ a * a∗ ≤ a∗

Tactic:
exact ⟨one_le_kstar, mul_kstar_le_kstar⟩
-- Module: Mathlib.Algebra.Order.Kleene
Goal:
α : Type u_1
inst : KleeneAlgebra α
a : α
⊢ 1 + a * a∗ ≤ a∗

Tactic:
have h : 1 + a * a∗ ≤ a∗ := by
    rw [add_le_iff]
    exact ⟨one_le_kstar, mul_kstar_le_kstar⟩
-- Module: Mathlib.Algebra.Order.Kleene
Goal:
α : Type u_1
inst : KleeneAlgebra α
a : α
h : 1 + a * a∗ ≤ a∗
apply : a∗ ≤ 1 + a * a∗
⊢ 1 + a * a∗ = a∗

Tactic:
apply le_antisymm h

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

Tactic:
rw [add_le_iff] at this

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

Tactic:
nth_rw 1 [← mul_one a∗]

Premises used: KStar.kstar, mul_one
-- Module: Mathlib.Algebra.Order.Kleene
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 ≤ 1 + a * a∗

Tactic:
(mul_right_mono this.1).trans (kstar_mul_le_self this.2)

Premises used: kstar_mul_le_self, mul_right_mono, And.right, And.left, 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∗ ∧ a * (1 + a * a∗) ≤ 1 + a * a∗
⊢ a∗ * 1 ≤ 1 + a * a∗

Tactic:
exact (mul_right_mono this.1).trans (kstar_mul_le_self this.2)

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

Tactic:
apply add_le_add_right (mul_right_mono h)

Premises used: mul_right_mono, add_le_add_right
-- Module: Mathlib.Algebra.Order.Kleene
Goal:
α : Type u_1
inst : KleeneAlgebra α
a : α
rw : 1 ≤ a∗ ∧ a∗ * a ≤ a∗
⊢ 1 + a∗ * a ≤ a∗

Tactic:
rw [add_le_iff]

Premises used: add_le_iff
-- Module: Mathlib.Algebra.Order.Kleene
Goal:
α : Type u_1
inst : KleeneAlgebra α
a : α
⊢ 1 ≤ a∗ ∧ a∗ * a ≤ a∗

Tactic:
⟨one_le_kstar, kstar_mul_le_kstar⟩

Premises used: one_le_kstar, And.intro, kstar_mul_le_kstar
-- Module: Mathlib.Algebra.Order.Kleene
Goal:
α : Type u_1
inst : KleeneAlgebra α
a : α
⊢ 1 ≤ a∗ ∧ a∗ * a ≤ a∗

Tactic:
exact ⟨one_le_kstar, kstar_mul_le_kstar⟩
-- Module: Mathlib.Algebra.Order.Kleene
Goal:
α : Type u_1
inst : KleeneAlgebra α
a : α
⊢ 1 + a∗ * a ≤ a∗

Tactic:
have h : 1 + a∗ * a ≤ a∗ := by
    rw [add_le_iff]
    exact ⟨one_le_kstar, kstar_mul_le_kstar⟩
-- Module: Mathlib.Algebra.Order.Kleene
Goal:
α : Type u_1
inst : KleeneAlgebra α
a : α
h : 1 + a∗ * a ≤ a∗
apply : a∗ ≤ 1 + a∗ * a
⊢ 1 + a∗ * a = a∗

Tactic:
apply le_antisymm h

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

Tactic:
rw [add_le_iff] at this

Premises used: add_le_iff