awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Set.Group (hypothesis)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a b : α
m n : ℤ
hmn : m ≠ n
x : α
hx : x ∈ Ioc (a * b ^ m) (a * b ^ (m + 1)) ∩ Ioc (a * b ^ n) (a * b ^ (n + 1))
hb : 1 < b
i1 : a * b ^ m < a * b ^ (n + 1)
i2 : a * b ^ n < a * b ^ (m + 1)
⊢ m = n
have i1₁ : m ≤ n
Tactic: rw [mul_lt_mul_iff_left, zpow_lt_zpow_iff_right hb, Int.lt_add_one_iff] at i1 i2
Cleared hypotheses: i1, i2
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Set.Group (hypothesis)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a b : α
m n : ℤ
hmn : m ≠ n
x : α
hx : x ∈ Ioc (a * b ^ m) (a * b ^ (m + 1)) ∩ Ioc (a * b ^ n) (a * b ^ (n + 1))
hb : 1 < b
i1 : a * b ^ m < a * b ^ (n + 1)
i2 : a * b ^ n < a * b ^ (m + 1)
i1₁ : m ≤ n
⊢ m = n
have i2₁ : n ≤ m
Tactic: rw [mul_lt_mul_iff_left, zpow_lt_zpow_iff_right hb, Int.lt_add_one_iff] at i1 i2
Cleared hypotheses: i1, i2
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Set.Group (goal)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a b : α
⊢ Pairwise fun (x y : ℤ) ↦ Disjoint (Ico (a * b ^ x) (a * b ^ (x + 1))) (Ico (a * b ^ y) (a * b ^ (y + 1)))
have simp_rw : Pairwise fun (x y : ℤ) ↦ Ico (a * b ^ x) (a * b ^ (x + 1)) ∩ Ico (a * b ^ y) (a * b ^ (y + 1)) ⊆ ∅
Tactic: simp_rw [Set.disjoint_iff]
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Set.Group (goal)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a b : α
m n : ℤ
hmn : m ≠ n
x : α
hx : x ∈ Ico (a * b ^ m) (a * b ^ (m + 1)) ∩ Ico (a * b ^ n) (a * b ^ (n + 1))
⊢ Membership.mem (γ := Set α) ∅ x
have apply : m = n
Tactic: apply hmn
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Set.Group (hypothesis)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a b : α
m n : ℤ
hmn : m ≠ n
x : α
hx : x ∈ Ico (a * b ^ m) (a * b ^ (m + 1)) ∩ Ico (a * b ^ n) (a * b ^ (n + 1))
⊢ 1 < b
have this : a * b ^ m < a * b ^ (m + 1)
Tactic: have : a * b ^ m < a * b ^ (m + 1) := hx.1.1.trans_lt hx.1.2
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Set.Group (goal)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a b : α
m n : ℤ
hmn : m ≠ n
x : α
hx : x ∈ Ico (a * b ^ m) (a * b ^ (m + 1)) ∩ Ico (a * b ^ n) (a * b ^ (n + 1))
this : a * b ^ m < a * b ^ (m + 1)
⊢ 1 < b
have rwa : ∀ (this : b ^ m < b ^ (m + 1)), 1 < b
Tactic: rwa [mul_lt_mul_iff_left, ← mul_one (b ^ m), zpow_add_one, mul_lt_mul_iff_left] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Set.Group (goal)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a b : α
m n : ℤ
hmn : m ≠ n
x : α
hx : x ∈ Ico (a * b ^ m) (a * b ^ (m + 1)) ∩ Ico (a * b ^ n) (a * b ^ (n + 1))
this : a * b ^ m < a * b ^ (m + 1)
rwa : ∀ (this : b ^ m < b ^ (m + 1)), 1 < b
⊢ 1 < b
have rwa₁ : ∀ (this : b ^ m * 1 < b ^ (m + 1)), 1 < b
Tactic: rwa [mul_lt_mul_iff_left, ← mul_one (b ^ m), zpow_add_one, mul_lt_mul_iff_left] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Set.Group (goal)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a b : α
m n : ℤ
hmn : m ≠ n
x : α
hx : x ∈ Ico (a * b ^ m) (a * b ^ (m + 1)) ∩ Ico (a * b ^ n) (a * b ^ (n + 1))
this : a * b ^ m < a * b ^ (m + 1)
rwa : ∀ (this : b ^ m < b ^ (m + 1)), 1 < b
rwa₁ : ∀ (this : b ^ m * 1 < b ^ (m + 1)), 1 < b
⊢ 1 < b
have rwa₂ : ∀ (this : b ^ m * 1 < b ^ m * b), 1 < b
Tactic: rwa [mul_lt_mul_iff_left, ← mul_one (b ^ m), zpow_add_one, mul_lt_mul_iff_left] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Set.Group (goal)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a b : α
m n : ℤ
hmn : m ≠ n
x : α
hx : x ∈ Ico (a * b ^ m) (a * b ^ (m + 1)) ∩ Ico (a * b ^ n) (a * b ^ (n + 1))
this : a * b ^ m < a * b ^ (m + 1)
rwa : ∀ (this : b ^ m < b ^ (m + 1)), 1 < b
rwa₁ : ∀ (this : b ^ m * 1 < b ^ (m + 1)), 1 < b
rwa₂ : ∀ (this : b ^ m * 1 < b ^ m * b), 1 < b
⊢ 1 < b
have rwa₃ : ∀ (this : 1 < b), 1 < b
Tactic: rwa [mul_lt_mul_iff_left, ← mul_one (b ^ m), zpow_add_one, mul_lt_mul_iff_left] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Set.Group (hypothesis)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a b : α
m n : ℤ
hmn : m ≠ n
x : α
hx : x ∈ Ico (a * b ^ m) (a * b ^ (m + 1)) ∩ Ico (a * b ^ n) (a * b ^ (n + 1))
⊢ m = n
have hb : 1 < b
Tactic: have hb : 1 < b := by
    have : a * b ^ m < a * b ^ (m + 1) := hx.1.1.trans_lt hx.1.2
    rwa [mul_lt_mul_iff_left, ← mul_one (b ^ m), zpow_add_one, mul_lt_mul_iff_left] at this
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Set.Group (hypothesis)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a b : α
m n : ℤ
hmn : m ≠ n
x : α
hx : x ∈ Ico (a * b ^ m) (a * b ^ (m + 1)) ∩ Ico (a * b ^ n) (a * b ^ (n + 1))
hb : 1 < b
⊢ m = n
have i1 : a * b ^ m < a * b ^ (n + 1)
Tactic: have i1 := hx.1.1.trans_lt hx.2.2
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Set.Group (hypothesis)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a b : α
m n : ℤ
hmn : m ≠ n
x : α
hx : x ∈ Ico (a * b ^ m) (a * b ^ (m + 1)) ∩ Ico (a * b ^ n) (a * b ^ (n + 1))
hb : 1 < b
i1 : a * b ^ m < a * b ^ (n + 1)
⊢ m = n
have i2 : a * b ^ n < a * b ^ (m + 1)
Tactic: have i2 := hx.2.1.trans_lt hx.1.2
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Set.Group (hypothesis)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a b : α
m n : ℤ
hmn : m ≠ n
x : α
hx : x ∈ Ico (a * b ^ m) (a * b ^ (m + 1)) ∩ Ico (a * b ^ n) (a * b ^ (n + 1))
hb : 1 < b
i1 : a * b ^ m < a * b ^ (n + 1)
i2 : a * b ^ n < a * b ^ (m + 1)
⊢ m = n
have i1₁ : m ≤ n
Tactic: rw [mul_lt_mul_iff_left, zpow_lt_zpow_iff_right hb, Int.lt_add_one_iff] at i1 i2
Cleared hypotheses: i1, i2
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Set.Group (hypothesis)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a b : α
m n : ℤ
hmn : m ≠ n
x : α
hx : x ∈ Ico (a * b ^ m) (a * b ^ (m + 1)) ∩ Ico (a * b ^ n) (a * b ^ (n + 1))
hb : 1 < b
i1 : a * b ^ m < a * b ^ (n + 1)
i2 : a * b ^ n < a * b ^ (m + 1)
i1₁ : m ≤ n
⊢ m = n
have i2₁ : n ≤ m
Tactic: rw [mul_lt_mul_iff_left, zpow_lt_zpow_iff_right hb, Int.lt_add_one_iff] at i1 i2
Cleared hypotheses: i1, i2
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Set.Instances (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
x : (↑(Icc 0 1) : Type u_1)
⊢ (↑x : R) = 0 ↔ x = 0
have symm : x = 0 ↔ (↑x : R) = 0
Tactic: symm
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Set.Instances (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
x : (↑(Icc 0 1) : Type u_1)
⊢ (↑x : R) = 1 ↔ x = 1
have symm : x = 1 ↔ (↑x : R) = 1
Tactic: symm
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Set.Instances (hypothesis)
Goal:
β : Type u_2
inst : Ring β
inst_1 : PartialOrder β
inst_2 : IsOrderedRing β
t : β
ht : Membership.mem (γ := Set β) (Icc 0 1) t
⊢ Membership.mem (γ := Set β) (Icc 0 1) (1 - t)
have ht₁ : 0 ≤ t ∧ t ≤ 1
Tactic: rw [mem_Icc] at *
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Set.Instances (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : Nontrivial R
x : (↑(Ico 0 1) : Type u_1)
⊢ (↑x : R) = 0 ↔ x = 0
have symm : x = 0 ↔ (↑x : R) = 0
Tactic: symm
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Set.Instances (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
x : (↑(Ioc 0 1) : Type u_1)
⊢ (↑x : R) = 1 ↔ x = 1
have symm : x = 1 ↔ (↑x : R) = 1
Tactic: symm
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Set.Monoid (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedCancelAddMonoid M
inst_3 : ExistsAddOfLE M
a d : M
⊢ BijOn (fun (x : M) ↦ x + d) (Ici a) (Ici (a + d))
have refine : ∀ (x : M) (h : x ∈ Ici (a + d)), Membership.mem (γ := Set M) ((fun (x : M) ↦ x + d) '' Ici a) x
Tactic: refine ⟨by simp [MapsTo], by simp, fun _ h => ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Set.Monoid (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedCancelAddMonoid M
inst_3 : ExistsAddOfLE M
a d x : M
h : x ∈ Ici (a + d)
⊢ Membership.mem (γ := Set M) ((fun (x : M) ↦ x + d) '' Ici a) x
have obtain : ∀ (c : M) (h : a + d + c ∈ Ici (a + d)), Membership.mem (γ := Set M) ((fun (x : M) ↦ x + d) '' Ici a) (a + d + c)
Tactic: obtain ⟨c, rfl⟩ := exists_add_of_le (mem_Ici.mp h)
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Set.Monoid (hypothesis)
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedCancelAddMonoid M
inst_3 : ExistsAddOfLE M
a d c : M
h : a + d + c ∈ Ici (a + d)
⊢ Membership.mem (γ := Set M) ((fun (x : M) ↦ x + d) '' Ici a) (a + d + c)
have h₁ : a ≤ a + c
Tactic: rw [mem_Ici, add_right_comm, add_le_add_iff_right] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Set.Monoid (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedCancelAddMonoid M
inst_3 : ExistsAddOfLE M
a d c : M
h : a ≤ a + c
⊢ (fun (x : M) ↦ x + d) (a + c) = a + d + c
have rw : (fun (x : M) ↦ x + d) (a + c) = a + c + d
Tactic: rw [add_right_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Set.Monoid (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedCancelAddMonoid M
inst_3 : ExistsAddOfLE M
a d : M
⊢ BijOn (fun (x : M) ↦ x + d) (Ioi a) (Ioi (a + d))
have refine : ∀ (x : M) (h : x ∈ Ioi (a + d)), Membership.mem (γ := Set M) ((fun (x : M) ↦ x + d) '' Ioi a) x
Tactic: refine ⟨by simp [MapsTo], by simp, fun _ h => ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Set.Monoid (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedCancelAddMonoid M
inst_3 : ExistsAddOfLE M
a d x : M
h : x ∈ Ioi (a + d)
⊢ Membership.mem (γ := Set M) ((fun (x : M) ↦ x + d) '' Ioi a) x
have obtain : ∀ (c : M) (h : a + d + c ∈ Ioi (a + d)), Membership.mem (γ := Set M) ((fun (x : M) ↦ x + d) '' Ioi a) (a + d + c)
Tactic: obtain ⟨c, rfl⟩ := exists_add_of_le (mem_Ioi.mp h).le
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Set.Monoid (hypothesis)
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedCancelAddMonoid M
inst_3 : ExistsAddOfLE M
a d c : M
h : a + d + c ∈ Ioi (a + d)
⊢ Membership.mem (γ := Set M) ((fun (x : M) ↦ x + d) '' Ioi a) (a + d + c)
have h₁ : a < a + c
Tactic: rw [mem_Ioi, add_right_comm, add_lt_add_iff_right] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Set.Monoid (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedCancelAddMonoid M
inst_3 : ExistsAddOfLE M
a d c : M
h : a < a + c
⊢ (fun (x : M) ↦ x + d) (a + c) = a + d + c
have rw : (fun (x : M) ↦ x + d) (a + c) = a + c + d
Tactic: rw [add_right_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Set.Monoid (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedCancelAddMonoid M
inst_3 : ExistsAddOfLE M
a b d : M
⊢ BijOn (fun (x : M) ↦ x + d) (Icc a b) (Icc (a + d) (b + d))
have rw : BijOn (fun (x : M) ↦ x + d) (Ici a ∩ Iic b) (Ici (a + d) ∩ Iic (b + d))
Tactic: rw [← Ici_inter_Iic, ← Ici_inter_Iic]
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Set.Monoid (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedCancelAddMonoid M
inst_3 : ExistsAddOfLE M
a b d : M
⊢ BijOn (fun (x : M) ↦ x + d) (Ioo a b) (Ioo (a + d) (b + d))
have rw : BijOn (fun (x : M) ↦ x + d) (Ioi a ∩ Iio b) (Ioi (a + d) ∩ Iio (b + d))
Tactic: rw [← Ioi_inter_Iio, ← Ioi_inter_Iio]
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Set.Monoid (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedCancelAddMonoid M
inst_3 : ExistsAddOfLE M
a b d : M
⊢ BijOn (fun (x : M) ↦ x + d) (Ioc a b) (Ioc (a + d) (b + d))
have rw : BijOn (fun (x : M) ↦ x + d) (Ioi a ∩ Iic b) (Ioi (a + d) ∩ Iic (b + d))
Tactic: rw [← Ioi_inter_Iic, ← Ioi_inter_Iic]
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Set.Monoid (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedCancelAddMonoid M
inst_3 : ExistsAddOfLE M
a b d : M
⊢ BijOn (fun (x : M) ↦ x + d) (Ico a b) (Ico (a + d) (b + d))
have rw : BijOn (fun (x : M) ↦ x + d) (Ici a ∩ Iio b) (Ici (a + d) ∩ Iio (b + d))
Tactic: rw [← Ici_inter_Iio, ← Ici_inter_Iio]
-- Lean 4 proof step from Mathlib.Algebra.Order.Kleene (goal)
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
⊢ a + c = c
have rw : a + (b + c) = b + c
Tactic: rw [← hbc, ← add_assoc, hab]
-- Lean 4 proof step from Mathlib.Algebra.Order.Kleene (goal)
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
⊢ a + c = c
have rw₁ : a + b + c = b + c
Tactic: rw [← hbc, ← add_assoc, hab]
-- Lean 4 proof step from Mathlib.Algebra.Order.Kleene (goal)
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
⊢ a + c = c
have rw₂ : b + c = b + c
Tactic: rw [← hbc, ← add_assoc, hab]
-- Lean 4 proof step from Mathlib.Algebra.Order.Kleene (goal)
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
⊢ a = b
have rwa : b + a = b
Tactic: rwa [← hba, add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Kleene (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst : Semiring α
h : ∀ (a : α), a + a = a
a b : α
⊢ a + (a + b) = a + b
have rw : a + a + b = a + b
Tactic: rw [← add_assoc, 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 : Semiring α
h : ∀ (a : α), a + a = a
a b : α
rw : a + a + b = a + b
⊢ a + (a + b) = a + b
have rw₁ : a + b = a + b
Tactic: rw [← add_assoc, 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 : Semiring α
h : ∀ (a : α), a + a = a
a b : α
⊢ b + (a + b) = a + b
have rw : a + b + b = a + b
Tactic: rw [add_comm, add_assoc, 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 : Semiring α
h : ∀ (a : α), a + a = a
a b : α
rw : a + b + b = a + b
⊢ b + (a + b) = a + b
have rw₁ : a + (b + b) = a + b
Tactic: rw [add_comm, add_assoc, 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 : Semiring α
h : ∀ (a : α), a + a = a
a b : α
rw : a + b + b = a + b
rw₁ : a + (b + b) = a + b
⊢ b + (a + b) = a + b
have rw₂ : a + b = a + b
Tactic: rw [add_comm, add_assoc, 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 : Semiring α
h : ∀ (a : α), a + a = a
a b c : α
hab : a + c = c
hbc : b + c = c
⊢ a + b + c = c
have rwa : a + (b + c) = c
Tactic: rwa [add_assoc, hbc]
-- Lean 4 proof step from Mathlib.Algebra.Order.Kleene (hypothesis)
Goal:
α : Type u_1
inst : IdemSemiring α
n : ℕ
nezero : n ≠ 0
⊢ Eq.{u_1 + 1} (α := α) (↑n : α) 1
have nezero₁ : 1 ≤ n
Tactic: rw [← Nat.one_le_iff_ne_zero] at nezero
Cleared hypotheses: nezero
-- Lean 4 proof step from Mathlib.Algebra.Order.Kleene (goal)
Goal:
α : Type u_1
inst : IdemSemiring α
n x : ℕ
hmn : 1 ≤ x
hx : Eq.{u_1 + 1} (α := α) (↑x : α) 1
⊢ Eq.{u_1 + 1} (α := α) (↑(x + 1) : α) 1
have succ : HAdd.hAdd (α := α) (↑x : α) (↑1 : α) = 1
Tactic: rw [Nat.cast_add, hx, Nat.cast_one, add_idem 1]
-- Lean 4 proof step from Mathlib.Algebra.Order.Kleene (goal)
Goal:
α : Type u_1
inst : IdemSemiring α
n x : ℕ
hmn : 1 ≤ x
hx : Eq.{u_1 + 1} (α := α) (↑x : α) 1
succ : HAdd.hAdd (α := α) (↑x : α) (↑1 : α) = 1
⊢ Eq.{u_1 + 1} (α := α) (↑(x + 1) : α) 1
have succ₁ : HAdd.hAdd (α := α) 1 (↑1 : α) = 1
Tactic: rw [Nat.cast_add, hx, Nat.cast_one, add_idem 1]
-- Lean 4 proof step from Mathlib.Algebra.Order.Kleene (goal)
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
⊢ Eq.{u_1 + 1} (α := α) (↑(x + 1) : α) 1
have succ₂ : HAdd.hAdd (α := α) 1 1 = 1
Tactic: rw [Nat.cast_add, hx, Nat.cast_one, add_idem 1]
-- Lean 4 proof step from Mathlib.Algebra.Order.Kleene (goal)
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
⊢ Eq.{u_1 + 1} (α := α) (↑(x + 1) : α) 1
have succ₃ : Eq.{u_1 + 1} (α := α) 1 1
Tactic: rw [Nat.cast_add, hx, Nat.cast_one, add_idem 1]
-- Lean 4 proof step from Mathlib.Algebra.Order.Kleene (goal)
Goal:
α : Type u_1
inst : IdemSemiring α
n : ℕ
nezero : 1 ≤ n
⊢ Eq.{u_1 + 1} (α := α) (↑n : α) 1
have base : Eq.{u_1 + 1} (α := α) (↑1 : α) 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]
Cleared hypotheses: nezero
-- Lean 4 proof step from Mathlib.Algebra.Order.Kleene (goal)
Goal:
α : Type u_1
inst : IdemSemiring α
n : ℕ
nezero : 1 ≤ n
base : Eq.{u_1 + 1} (α := α) (↑1 : α) 1
⊢ Eq.{u_1 + 1} (α := α) (↑n : α) 1
have succ : ∀ (x : ℕ), 1 ≤ x → ∀ (hx : Eq.{u_1 + 1} (α := α) (↑x : α) 1), Eq.{u_1 + 1} (α := α) (↑(x + 1) : α) 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]
Cleared hypotheses: nezero
-- Lean 4 proof step from Mathlib.Algebra.Order.Kleene (goal)
Goal:
α : Type u_1
inst : IdemSemiring α
n : ℕ
h : n + 2 ≠ 0
a : α
⊢ (n + 2) • a = a
have rw : (n + 1) • a + a = a
Tactic: rw [succ_nsmul, nsmul_eq_self n.succ_ne_zero, add_idem]
-- Lean 4 proof step from Mathlib.Algebra.Order.Kleene (goal)
Goal:
α : Type u_1
inst : IdemSemiring α
n : ℕ
h : n + 2 ≠ 0
a : α
rw : (n + 1) • a + a = a
⊢ (n + 2) • a = a
have rw₁ : a + a = a
Tactic: rw [succ_nsmul, nsmul_eq_self n.succ_ne_zero, add_idem]
-- Lean 4 proof step from Mathlib.Algebra.Order.Kleene (goal)
Goal:
α : Type u_1
inst : IdemSemiring α
n : ℕ
h : n + 2 ≠ 0
a : α
rw : (n + 1) • a + a = a
rw₁ : a + a = a
⊢ (n + 2) • a = a
have rw₂ : a = a
Tactic: rw [succ_nsmul, nsmul_eq_self n.succ_ne_zero, add_idem]
-- 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 α
a_1 b_1 c_1 a b : α
hbc : a ≤ b
c : α
⊢ a + c ≤ b + c
have simp_rw : a ⊔ c ≤ b ⊔ c
Tactic: simp_rw [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 α
a_1 b_1 c_1 a b : α
hbc : a ≤ b
c : α
⊢ a ⊔ c ≤ b ⊔ c
have grw : b ⊔ c ≤ b ⊔ c
Tactic: grw [hbc]
-- 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 α
a_1 b_1 c a b : α
⊢ b + a + a = b + a
have rw : b + (a + a) = b + a
Tactic: rw [add_assoc, add_idem]
-- 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 α
a_1 b_1 c a b : α
rw : b + (a + a) = b + a
⊢ b + a + a = b + a
have rw₁ : b + a = b + a
Tactic: rw [add_assoc, add_idem]
-- 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 α
a_1 b_1 c a b : α
⊢ a + (a + b) = a + b
have rw : a + a + b = a + b
Tactic: rw [← add_assoc, add_idem]
-- 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 α
a_1 b_1 c a b : α
rw : a + a + b = a + b
⊢ a + (a + b) = a + b
have rw₁ : a + b = a + b
Tactic: rw [← add_assoc, add_idem]
-- 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 α
a_1 b_1 c_1 a b c : α
hbc : (fun (x1 x2 : α) ↦ x1 ≤ x2) b c
⊢ HAdd.hAdd (α := α) ((fun (x1 x2 : α) ↦ x1 * x2) a c) ((fun (x1 x2 : α) ↦ x1 * x2) a b) =
    (fun (x1 x2 : α) ↦ x1 * x2) a c
have rw : a * (c + b) = (fun (x1 x2 : α) ↦ x1 * x2) a c
Tactic: rw [← mul_add, hbc.add_eq_left]
-- 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 α
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
⊢ HAdd.hAdd (α := α) ((fun (x1 x2 : α) ↦ x1 * x2) a c) ((fun (x1 x2 : α) ↦ x1 * x2) a b) =
    (fun (x1 x2 : α) ↦ x1 * x2) a c
have rw₁ : a * c = (fun (x1 x2 : α) ↦ x1 * x2) a c
Tactic: rw [← mul_add, hbc.add_eq_left]
-- 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 α
a_1 b_1 c_1 a b c : α
hbc : (fun (x1 x2 : α) ↦ x1 ≤ x2) b 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
have rw : (c + b) * a = swap (φ := fun (a a_2 : α) ↦ α) (fun (x1 x2 : α) ↦ x1 * x2) a c
Tactic: rw [← add_mul, hbc.add_eq_left]
-- 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 α
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
⊢ 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
have rw₁ : c * a = swap (φ := fun (a a_2 : α) ↦ α) (fun (x1 x2 : α) ↦ x1 * x2) a c
Tactic: rw [← add_mul, hbc.add_eq_left]
-- Lean 4 proof step from Mathlib.Algebra.Order.Kleene (goal)
Goal:
α : Type u_1
inst : KleeneAlgebra α
a b c : α
hb : b ≤ c
ha : c * a ≤ c
⊢ b * a∗ ≤ c
have grw : c * a∗ ≤ c
Tactic: grw [hb, mul_kstar_le_self ha]
-- Lean 4 proof step from Mathlib.Algebra.Order.Kleene (goal)
Goal:
α : Type u_1
inst : KleeneAlgebra α
a b c : α
hb : b ≤ c
ha : c * a ≤ c
grw : c * a∗ ≤ c
⊢ b * a∗ ≤ c
have grw₁ : c ≤ c
Tactic: grw [hb, mul_kstar_le_self ha]
-- Lean 4 proof step from Mathlib.Algebra.Order.Kleene (goal)
Goal:
α : Type u_1
inst : KleeneAlgebra α
a b c : α
hb : b ≤ c
ha : a * c ≤ c
⊢ a∗ * b ≤ c
have grw : a∗ * c ≤ c
Tactic: grw [hb, kstar_mul_le_self ha]
-- Lean 4 proof step from Mathlib.Algebra.Order.Kleene (goal)
Goal:
α : Type u_1
inst : KleeneAlgebra α
a b c : α
hb : b ≤ c
ha : a * c ≤ c
grw : a∗ * c ≤ c
⊢ a∗ * b ≤ c
have grw₁ : c ≤ c
Tactic: grw [hb, kstar_mul_le_self ha]
-- Lean 4 proof step from Mathlib.Algebra.Order.Kleene (goal)
Goal:
α : Type u_1
inst : KleeneAlgebra α
a : α
h : a∗ = a
⊢ a * a = a
have rw : a∗ * a∗ = a∗
Tactic: rw [← h, kstar_mul_kstar]
-- Lean 4 proof step from Mathlib.Algebra.Order.Kleene (goal)
Goal:
α : Type u_1
inst : KleeneAlgebra α
a : α
h : a∗ = a
rw : a∗ * a∗ = a∗
⊢ a * a = a
have rw₁ : a∗ = a∗
Tactic: rw [← h, kstar_mul_kstar]