awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.DenselyOrdered (goal)
Goal:
M : Type u_2
inst : LinearOrder M
inst_1 : DenselyOrdered M
x : M
inst_2 : CommMonoid M
inst_3 : ExistsMulOfLE M
inst_4 : IsOrderedCancelMonoid M
hx : 1 < x
y : M
hy : 1 < y
hyx : y < x
inl : ∀ (hyx : HPow.hPow (β := ℕ) y 2 ≤ x), ∃ (y : M), 1 < y ∧ HPow.hPow (β := ℕ) y 2 ≤ x
⊢ ∃ (y : M), 1 < y ∧ HPow.hPow (β := ℕ) y 2 ≤ x
have inr : ∀ (hxy : x ≤ HPow.hPow (β := ℕ) y 2), ∃ (y : M), 1 < y ∧ HPow.hPow (β := ℕ) y 2 ≤ x
Tactic: obtain hyx | hxy := le_total (y ^ 2) x
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.DenselyOrdered (goal)
Goal:
M : Type u_2
inst : LinearOrder M
inst_1 : DenselyOrdered M
x : M
inst_2 : CommMonoid M
inst_3 : ExistsMulOfLE M
inst_4 : IsOrderedCancelMonoid M
hx : 1 < x
y : M
hy : 1 < y
hyx : y < x
hxy : x ≤ HPow.hPow (β := ℕ) y 2
⊢ ∃ (y : M), 1 < y ∧ HPow.hPow (β := ℕ) y 2 ≤ x
have inr : ∀ (z : M) (hz : 1 < z) (hx : 1 < y * z) (hyx : y < y * z) (hxy : y * z ≤ HPow.hPow (β := ℕ) y 2),
  ∃ (y_1 : M), 1 < y_1 ∧ HPow.hPow (β := ℕ) y_1 2 ≤ y * z
Tactic: obtain ⟨z, hz, rfl⟩ := exists_one_lt_mul_of_lt' hyx
Cleared hypotheses: x, hx, hyx, hxy
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.DenselyOrdered (goal)
Goal:
M : Type u_2
inst : LinearOrder M
inst_1 : DenselyOrdered M
x : M
inst_2 : CommMonoid M
inst_3 : ExistsMulOfLE M
inst_4 : IsOrderedCancelMonoid M
hx : 1 < x
n : ℕ
⊢ ∃ (y : M), 1 < y ∧ y ^ (n + 2) < x
have obtain : ∀ (y : M) (hy : 1 < y) (hyx : y ^ (n + 1) < x), ∃ (y : M), 1 < y ∧ y ^ (n + 2) < x
Tactic: obtain ⟨y, hy, hyx⟩ := exists_pow_lt_of_one_lt hx (n + 1)
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.DenselyOrdered (goal)
Goal:
M : Type u_2
inst : LinearOrder M
inst_1 : DenselyOrdered M
x : M
inst_2 : CommMonoid M
inst_3 : ExistsMulOfLE M
inst_4 : IsOrderedCancelMonoid M
hx : 1 < x
n : ℕ
y : M
hy : 1 < y
hyx : y ^ (n + 1) < x
⊢ ∃ (y : M), 1 < y ∧ y ^ (n + 2) < x
have obtain : ∀ (z : M) (hz : 1 < z) (hzy : HPow.hPow (β := ℕ) z 2 ≤ y), ∃ (y : M), 1 < y ∧ y ^ (n + 2) < x
Tactic: obtain ⟨z, hz, hzy⟩ := exists_pow_two_le_of_one_lt hy
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.DenselyOrdered (goal)
Goal:
M : Type u_2
inst : LinearOrder M
inst_1 : DenselyOrdered M
x : M
inst_2 : CommMonoid M
inst_3 : ExistsMulOfLE M
inst_4 : IsOrderedCancelMonoid M
hx : 1 < x
n : ℕ
y : M
hy : 1 < y
hyx : y ^ (n + 1) < x
z : M
hz : 1 < z
hzy : HPow.hPow (β := ℕ) z 2 ≤ y
⊢ ∃ (y : M), 1 < y ∧ y ^ (n + 2) < x
have refine : z ^ (n + 2) ≤ y ^ (n + 1)
Tactic: refine ⟨z, hz, hyx.trans_le' ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.DenselyOrdered (goal)
Goal:
M : Type u_2
inst : LinearOrder M
inst_1 : DenselyOrdered M
x : M
inst_2 : CommMonoid M
inst_3 : ExistsMulOfLE M
inst_4 : IsOrderedCancelMonoid M
hx : 1 < x
n : ℕ
y : M
hy : 1 < y
hyx : y ^ (n + 1) < x
z : M
hz : 1 < z
hzy : HPow.hPow (β := ℕ) z 2 ≤ y
⊢ z ^ (2 * (n + 1)) = HPow.hPow (β := ℕ) z 2 ^ (n + 1)
have rw : HPow.hPow (β := ℕ) z 2 ^ (n + 1) = HPow.hPow (β := ℕ) z 2 ^ (n + 1)
Tactic: rw [pow_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.DenselyOrdered (goal)
Goal:
M : Type u_2
inst : LinearOrder M
inst_1 : DenselyOrdered M
x : M
inst_2 : CommMonoid M
inst_3 : ExistsMulOfLE M
inst_4 : IsOrderedCancelMonoid M
hx : 1 < x
n : ℕ
y : M
hy : 1 < y
hyx : y ^ (n + 1) < x
z : M
hz : 1 < z
hzy : HPow.hPow (β := ℕ) z 2 ≤ y
⊢ z ^ (n + 2) ≤ y ^ (n + 1)
have calc : z ^ (2 * (n + 1)) = HPow.hPow (β := ℕ) z 2 ^ (n + 1)
Tactic: calc z ^ (n + 2)
      _ ≤ z ^ (2 * (n + 1)) := pow_right_monotone hz.le (by lia)
      _ = (z ^ 2) ^ (n + 1) := by rw [pow_mul]
      _ ≤ y ^ (n + 1) := pow_le_pow_left' hzy (n + 1)
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.DenselyOrdered (goal)
Goal:
M : Type u_2
inst : LinearOrder M
inst_1 : DenselyOrdered M
x : M
inst_2 : CommGroup M
inst_3 : IsOrderedCancelMonoid M
hx : x < 1
n : ℕ
⊢ ∃ (y : M), y < 1 ∧ x < y ^ n
have obtain : ∀ (y : M) (hy : 1 < y) (hy' : y ^ n < x⁻¹), ∃ (y : M), y < 1 ∧ x < y ^ n
Tactic: obtain ⟨y, hy, hy'⟩ := exists_pow_lt_of_one_lt (one_lt_inv_of_inv hx) n
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.DenselyOrdered (goal)
Goal:
M : Type u_2
inst : LinearOrder M
inst_1 : DenselyOrdered M
x : M
inst_2 : CommGroup M
inst_3 : IsOrderedCancelMonoid M
hx : x < 1
n : ℕ
y : M
hy : 1 < y
hy' : y ^ n < x⁻¹
⊢ ∃ (y : M), y < 1 ∧ x < y ^ n
have right : x < y⁻¹ ^ n
Tactic: use y⁻¹, inv_lt_one_of_one_lt hy
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Finset (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
n : ℕ
h : n + 1 ≠ 0
⊢ ((n + 1) • s).toFinset = s.toFinset
have pos : ∀ (h : n = 0), ((n + 1) • s).toFinset = s.toFinset
Tactic: by_cases h : n = 0
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Finset (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
n : ℕ
h : n + 1 ≠ 0
pos : ∀ (h : n = 0), ((n + 1) • s).toFinset = s.toFinset
⊢ ((n + 1) • s).toFinset = s.toFinset
have neg : ∀ (h : ¬n = 0), ((n + 1) • s).toFinset = s.toFinset
Tactic: by_cases h : n = 0
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Finset (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
n : ℕ
h_1 : n + 1 ≠ 0
h : n = 0
⊢ ((n + 1) • s).toFinset = s.toFinset
have pos : (HAdd.hAdd (α := ℕ) 0 1 • s).toFinset = s.toFinset
Tactic: rw [h, zero_add, one_nsmul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Finset (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
n : ℕ
h_1 : n + 1 ≠ 0
h : n = 0
pos : (HAdd.hAdd (α := ℕ) 0 1 • s).toFinset = s.toFinset
pos₁ : (HSMul.hSMul (α := ℕ) 1 s).toFinset = s.toFinset
⊢ ((n + 1) • s).toFinset = s.toFinset
have pos₂ : s.toFinset = s.toFinset
Tactic: rw [h, zero_add, one_nsmul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Finset (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
n : ℕ
h_1 : n + 1 ≠ 0
h : ¬n = 0
⊢ ((n + 1) • s).toFinset = s.toFinset
have neg : (n • s + HSMul.hSMul (α := ℕ) 1 s).toFinset = s.toFinset
Tactic: rw [add_nsmul, toFinset_add, one_nsmul, toFinset_nsmul s n h, Finset.union_idempotent]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Finset (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
n : ℕ
h_1 : n + 1 ≠ 0
h : ¬n = 0
neg : (n • s + HSMul.hSMul (α := ℕ) 1 s).toFinset = s.toFinset
⊢ ((n + 1) • s).toFinset = s.toFinset
have neg₁ : (n • s).toFinset ∪ (HSMul.hSMul (α := ℕ) 1 s).toFinset = s.toFinset
Tactic: rw [add_nsmul, toFinset_add, one_nsmul, toFinset_nsmul s n h, Finset.union_idempotent]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Finset (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
n : ℕ
h_1 : n + 1 ≠ 0
h : ¬n = 0
neg : (n • s + HSMul.hSMul (α := ℕ) 1 s).toFinset = s.toFinset
neg₁ : (n • s).toFinset ∪ (HSMul.hSMul (α := ℕ) 1 s).toFinset = s.toFinset
⊢ ((n + 1) • s).toFinset = s.toFinset
have neg₂ : (n • s).toFinset ∪ s.toFinset = s.toFinset
Tactic: rw [add_nsmul, toFinset_add, one_nsmul, toFinset_nsmul s n h, Finset.union_idempotent]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Finset (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
n : ℕ
h_1 : n + 1 ≠ 0
h : ¬n = 0
neg : (n • s + HSMul.hSMul (α := ℕ) 1 s).toFinset = s.toFinset
neg₁ : (n • s).toFinset ∪ (HSMul.hSMul (α := ℕ) 1 s).toFinset = s.toFinset
neg₂ : (n • s).toFinset ∪ s.toFinset = s.toFinset
⊢ ((n + 1) • s).toFinset = s.toFinset
have neg₃ : s.toFinset ∪ s.toFinset = s.toFinset
Tactic: rw [add_nsmul, toFinset_add, one_nsmul, toFinset_nsmul s n h, Finset.union_idempotent]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Finset (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
n : ℕ
h_1 : n + 1 ≠ 0
h : ¬n = 0
neg : (n • s + HSMul.hSMul (α := ℕ) 1 s).toFinset = s.toFinset
neg₁ : (n • s).toFinset ∪ (HSMul.hSMul (α := ℕ) 1 s).toFinset = s.toFinset
neg₂ : (n • s).toFinset ∪ s.toFinset = s.toFinset
neg₃ : s.toFinset ∪ s.toFinset = s.toFinset
⊢ ((n + 1) • s).toFinset = s.toFinset
have neg₄ : s.toFinset = s.toFinset
Tactic: rw [add_nsmul, toFinset_add, one_nsmul, toFinset_nsmul s n h, Finset.union_idempotent]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Finset (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
a : α
⊢ s.toFinset = {a} ↔ s.card ≠ 0 ∧ s = HSMul.hSMul (β := Multiset α) s.card {a}
have refine_1 : ∀ (H : s.toFinset = {a}) (h : s.card = 0), False
Tactic: refine ⟨fun H ↦ ⟨fun h ↦ ?_, ext' fun x ↦ ?_⟩, fun H ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Finset (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
a : α
refine_1 : ∀ (H : s.toFinset = {a}) (h : s.card = 0), False
⊢ s.toFinset = {a} ↔ s.card ≠ 0 ∧ s = HSMul.hSMul (β := Multiset α) s.card {a}
have refine_2 : ∀ (H : s.toFinset = {a}) (x : α), count x s = count x (HSMul.hSMul (β := Multiset α) s.card {a})
Tactic: refine ⟨fun H ↦ ⟨fun h ↦ ?_, ext' fun x ↦ ?_⟩, fun H ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Finset (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
a : α
refine_1 : ∀ (H : s.toFinset = {a}) (h : s.card = 0), False
refine_2 : ∀ (H : s.toFinset = {a}) (x : α), count x s = count x (HSMul.hSMul (β := Multiset α) s.card {a})
⊢ s.toFinset = {a} ↔ s.card ≠ 0 ∧ s = HSMul.hSMul (β := Multiset α) s.card {a}
have refine_3 : ∀ (H : s.card ≠ 0 ∧ s = HSMul.hSMul (β := Multiset α) s.card {a}), s.toFinset = {a}
Tactic: refine ⟨fun H ↦ ⟨fun h ↦ ?_, ext' fun x ↦ ?_⟩, fun H ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Finset (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
a : α
H : s.toFinset = {a}
h : s.card = 0
⊢ False
have H₁ : Eq (α := Finset α) ∅ {a}
Tactic: rw [card_eq_zero.1 h, toFinset_zero] at H
Cleared hypotheses: H, h
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Finset (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
a : α
H : s.toFinset = {a}
x : α
⊢ count x s = count x (HSMul.hSMul (β := Multiset α) s.card {a})
have refine_2 : count x s = s.card * if x = a then 1 else 0
Tactic: rw [count_nsmul, count_singleton]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Finset (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
a : α
H : s.toFinset = {a}
x : α
⊢ count x s = s.card * if x = a then 1 else 0
have pos : ∀ (hx : x = a), count x s = s.card * if x = a then 1 else 0
Tactic: by_cases hx : x = a
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Finset (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
a : α
H : s.toFinset = {a}
x : α
pos : ∀ (hx : x = a), count x s = s.card * if x = a then 1 else 0
⊢ count x s = s.card * if x = a then 1 else 0
have neg : ∀ (hx : ¬x = a), count x s = s.card * if x = a then 1 else 0
Tactic: by_cases hx : x = a
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Finset (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
a : α
H : s.toFinset = {a}
x : α
hx : x = a
⊢ count x s = s.card * if x = a then 1 else 0
have pos : ∀ x ∈ s, a = x
Tactic: simp_rw [hx, ite_true, mul_one, count_eq_card]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Finset (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
a : α
H : s.toFinset = {a}
x : α
hx : x = a
y : α
hy : y ∈ s
⊢ a = y
have hy₁ : y = a
Tactic: rw [← mem_toFinset, H, Finset.mem_singleton] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Finset (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
a : α
H : s.toFinset = {a}
x : α
hx : ¬x = a
h' : x ∈ s
⊢ x = a
have rwa : ∀ (h' : x ∈ s.toFinset), x = a
Tactic: rwa [← mem_toFinset, H, Finset.mem_singleton] at h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Finset (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
a : α
H : s.toFinset = {a}
x : α
hx : ¬x = a
h' : x ∈ s
rwa : ∀ (h' : x ∈ s.toFinset), x = a
⊢ x = a
have rwa₁ : ∀ (h' : Membership.mem (γ := Finset α) {a} x), x = a
Tactic: rwa [← mem_toFinset, H, Finset.mem_singleton] at h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Finset (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
a : α
H : s.toFinset = {a}
x : α
hx : ¬x = a
h' : x ∈ s
rwa : ∀ (h' : x ∈ s.toFinset), x = a
rwa₁ : ∀ (h' : Membership.mem (γ := Finset α) {a} x), x = a
⊢ x = a
have rwa₂ : ∀ (h' : x = a), x = a
Tactic: rwa [← mem_toFinset, H, Finset.mem_singleton] at h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Finset (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
a : α
H : s.toFinset = {a}
x : α
hx : ¬x = a
⊢ count x s = s.card * if x = a then 1 else 0
have hx' : x ∉ s
Tactic: have hx' : x ∉ s := fun h' ↦ hx <| by rwa [← mem_toFinset, H, Finset.mem_singleton] at h'
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Finset (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
a : α
H : s.toFinset = {a}
x : α
hx : ¬x = a
hx' : x ∉ s
⊢ count x s = s.card * if x = a then 1 else 0
have neg : 0 = s.card * if x = a then 1 else 0
Tactic: simp_rw [count_eq_zero_of_notMem hx', hx, ite_false, Nat.mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Finset (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
a : α
H : s.toFinset = {a}
x : α
hx : ¬x = a
hx' : x ∉ s
neg : 0 = s.card * if x = a then 1 else 0
⊢ count x s = s.card * if x = a then 1 else 0
have neg₁ : 0 = s.card * if False then 1 else 0
Tactic: simp_rw [count_eq_zero_of_notMem hx', hx, ite_false, Nat.mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Finset (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
a : α
H : s.toFinset = {a}
x : α
hx : ¬x = a
hx' : x ∉ s
neg : 0 = s.card * if x = a then 1 else 0
neg₁ : 0 = s.card * if False then 1 else 0
⊢ count x s = s.card * if x = a then 1 else 0
have neg₂ : 0 = s.card * 0
Tactic: simp_rw [count_eq_zero_of_notMem hx', hx, ite_false, Nat.mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Finset (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
⊢ #s.toFinset = 1 ↔ s.card ≠ 0 ∧ ∃ (a : α), s = HSMul.hSMul (β := Multiset α) s.card {a}
have simp_rw : (∃ (a : α), s.toFinset = {a}) ↔ s.card ≠ 0 ∧ ∃ (a : α), s = HSMul.hSMul (β := Multiset α) s.card {a}
Tactic: simp_rw [Finset.card_eq_one, Multiset.toFinset_eq_singleton_iff, exists_and_left]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Finset (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
simp_rw : (∃ (a : α), s.toFinset = {a}) ↔ s.card ≠ 0 ∧ ∃ (a : α), s = HSMul.hSMul (β := Multiset α) s.card {a}
⊢ #s.toFinset = 1 ↔ s.card ≠ 0 ∧ ∃ (a : α), s = HSMul.hSMul (β := Multiset α) s.card {a}
have simp_rw₁ : (∃ (a : α), s.card ≠ 0 ∧ s = HSMul.hSMul (β := Multiset α) s.card {a}) ↔
  s.card ≠ 0 ∧ ∃ (a : α), s = HSMul.hSMul (β := Multiset α) s.card {a}
Tactic: simp_rw [Finset.card_eq_one, Multiset.toFinset_eq_singleton_iff, exists_and_left]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Finset (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : LinearOrder M
inst_1 : Add M
inst_2 : AddRightMono M
s : Finset ι
a : WithBot M
f : ι → M
⊢ fold max ⊥ (fun (i : ι) ↦ (↑(f i) : WithBot M) + a) s = fold max ⊥ (WithBot.some ∘ f) s + a
have empty : fold max ⊥ (fun (i : ι) ↦ (↑(f i) : WithBot M) + a) ∅ = fold max ⊥ (WithBot.some ∘ f) ∅ + a
Tactic: induction s using Finset.induction_on
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Finset (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : LinearOrder M
inst_1 : Add M
inst_2 : AddRightMono M
s : Finset ι
a : WithBot M
f : ι → M
empty : fold max ⊥ (fun (i : ι) ↦ (↑(f i) : WithBot M) + a) ∅ = fold max ⊥ (WithBot.some ∘ f) ∅ + a
⊢ fold max ⊥ (fun (i : ι) ↦ (↑(f i) : WithBot M) + a) s = fold max ⊥ (WithBot.some ∘ f) s + a
have insert : ∀ (a_1 : ι) (s : Finset ι),
  a_1 ∉ s →
    fold max ⊥ (fun (i : ι) ↦ (↑(f i) : WithBot M) + a) s = fold max ⊥ (WithBot.some ∘ f) s + a →
      fold max ⊥ (fun (i : ι) ↦ (↑(f i) : WithBot M) + a) (insert a_1 s) =
        fold max ⊥ (WithBot.some ∘ f) (insert a_1 s) + a
Tactic: induction s using Finset.induction_on
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Finset (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : LinearOrder M
inst_1 : Add M
inst_2 : AddRightMono M
s : Finset ι
a : WithBot M
f : ι → M
⊢ fold max ⊥ (fun (i : ι) ↦ (↑(f i) : WithBot M) + a) s = fold max ⊥ (WithBot.some ∘ f) s + a
have empty : fold max ⊥ (fun (i : ι) ↦ (↑(f i) : WithBot M) + a) ∅ = fold max ⊥ (WithBot.some ∘ f) ∅ + a
Tactic: classical induction s using Finset.induction_on <;> simp [*, max_add_add_right]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Finset (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : LinearOrder M
inst_1 : Add M
inst_2 : AddRightMono M
s : Finset ι
a : WithBot M
f : ι → M
empty : fold max ⊥ (fun (i : ι) ↦ (↑(f i) : WithBot M) + a) ∅ = fold max ⊥ (WithBot.some ∘ f) ∅ + a
⊢ fold max ⊥ (fun (i : ι) ↦ (↑(f i) : WithBot M) + a) s = fold max ⊥ (WithBot.some ∘ f) s + a
have insert : ∀ (a_1 : ι) (s : Finset ι),
  a_1 ∉ s →
    fold max ⊥ (fun (i : ι) ↦ (↑(f i) : WithBot M) + a) s = fold max ⊥ (WithBot.some ∘ f) s + a →
      fold max ⊥ (fun (i : ι) ↦ (↑(f i) : WithBot M) + a) (insert a_1 s) =
        fold max ⊥ (WithBot.some ∘ f) (insert a_1 s) + a
Tactic: classical induction s using Finset.induction_on <;> simp [*, max_add_add_right]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Finset (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : AddCommMonoid M
inst_1 : LinearOrder M
inst_2 : CanonicallyOrderedAdd M
inst_3 : Sub M
inst_4 : AddLeftReflectLE M
inst_5 : OrderedSub M
s : Finset ι
f : ι → M
a : M
hs : s.Nonempty
⊢ s.sup' hs f + a = s.sup' hs fun (i : ι) ↦ f i + a
have a₁ : s.sup' hs f + a ≤ s.sup' hs fun (i : ι) ↦ f i + a
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Finset (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : AddCommMonoid M
inst_1 : LinearOrder M
inst_2 : CanonicallyOrderedAdd M
inst_3 : Sub M
inst_4 : AddLeftReflectLE M
inst_5 : OrderedSub M
s : Finset ι
f : ι → M
a : M
hs : s.Nonempty
a₁ : s.sup' hs f + a ≤ s.sup' hs fun (i : ι) ↦ f i + a
⊢ s.sup' hs f + a = s.sup' hs fun (i : ι) ↦ f i + a
have a₂ : (s.sup' hs fun (i : ι) ↦ f i + a) ≤ s.sup' hs f + a
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Finset (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : AddCommMonoid M
inst_1 : LinearOrder M
inst_2 : CanonicallyOrderedAdd M
inst_3 : Sub M
inst_4 : AddLeftReflectLE M
inst_5 : OrderedSub M
s : Finset ι
f : ι → M
a : M
hs : s.Nonempty
⊢ s.sup' hs f + a ≤ s.sup' hs fun (i : ι) ↦ f i + a
have a₁ : a ≤ s.sup' hs fun (i : ι) ↦ f i + a
Tactic: apply add_le_of_le_tsub_right_of_le
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Finset (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : AddCommMonoid M
inst_1 : LinearOrder M
inst_2 : CanonicallyOrderedAdd M
inst_3 : Sub M
inst_4 : AddLeftReflectLE M
inst_5 : OrderedSub M
s : Finset ι
f : ι → M
a : M
hs : s.Nonempty
a₁ : a ≤ s.sup' hs fun (i : ι) ↦ f i + a
⊢ s.sup' hs f + a ≤ s.sup' hs fun (i : ι) ↦ f i + a
have a₂ : s.sup' hs f ≤ (s.sup' hs fun (i : ι) ↦ f i + a) - a
Tactic: apply add_le_of_le_tsub_right_of_le
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Finset (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : AddCommMonoid M
inst_1 : LinearOrder M
inst_2 : CanonicallyOrderedAdd M
inst_3 : Sub M
inst_4 : AddLeftReflectLE M
inst_5 : OrderedSub M
s : Finset ι
f : ι → M
a : M
hs : s.Nonempty
i : ι
hi : i ∈ s
⊢ f i + a ≤ s.sup' hs f + a
have grw : f i + a ≤ f i + a
Tactic: grw [← Finset.le_sup' _ hi]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Finset (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : AddCommMonoid M
inst_1 : LinearOrder M
inst_2 : CanonicallyOrderedAdd M
inst_3 : Sub M
inst_4 : AddLeftReflectLE M
inst_5 : OrderedSub M
s : Finset ι
hs : s.Nonempty
f : ι → M
a : M
⊢ a + s.sup' hs f = s.sup' hs fun (i : ι) ↦ a + f i
have simp_rw : s.sup' hs f + a = s.sup' sorry fun (x : ι) ↦ f x + a
Tactic: simp_rw [add_comm a, Finset.sup'_add']
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Finset (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : AddCommMonoid M
inst_1 : LinearOrder M
inst_2 : CanonicallyOrderedAdd M
inst_3 : Sub M
inst_4 : AddLeftReflectLE M
inst_5 : OrderedSub M
s : Finset ι
inst_6 : OrderBot M
hs : s.Nonempty
f : ι → M
a : M
⊢ s.sup f + a = s.sup fun (i : ι) ↦ f i + a
have rw : s.sup' hs f + a = s.sup fun (i : ι) ↦ f i + a
Tactic: rw [← Finset.sup'_eq_sup hs, ← Finset.sup'_eq_sup hs, sup'_add']
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Finset (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : AddCommMonoid M
inst_1 : LinearOrder M
inst_2 : CanonicallyOrderedAdd M
inst_3 : Sub M
inst_4 : AddLeftReflectLE M
inst_5 : OrderedSub M
s : Finset ι
inst_6 : OrderBot M
hs : s.Nonempty
f : ι → M
a : M
rw : s.sup' hs f + a = s.sup fun (i : ι) ↦ f i + a
⊢ s.sup f + a = s.sup fun (i : ι) ↦ f i + a
have rw₁ : s.sup' hs f + a = s.sup' hs fun (i : ι) ↦ f i + a
Tactic: rw [← Finset.sup'_eq_sup hs, ← Finset.sup'_eq_sup hs, sup'_add']
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Finset (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : AddCommMonoid M
inst_1 : LinearOrder M
inst_2 : CanonicallyOrderedAdd M
inst_3 : Sub M
inst_4 : AddLeftReflectLE M
inst_5 : OrderedSub M
s : Finset ι
inst_6 : OrderBot M
hs : s.Nonempty
f : ι → M
a : M
rw : s.sup' hs f + a = s.sup fun (i : ι) ↦ f i + a
rw₁ : s.sup' hs f + a = s.sup' hs fun (i : ι) ↦ f i + a
⊢ s.sup f + a = s.sup fun (i : ι) ↦ f i + a
have rw₂ : Eq.{u_3 + 1} (α := M) (s.sup' hs fun (i : ι) ↦ f i + a) (s.sup' hs fun (i : ι) ↦ f i + a)
Tactic: rw [← Finset.sup'_eq_sup hs, ← Finset.sup'_eq_sup hs, sup'_add']
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Finset (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : AddCommMonoid M
inst_1 : LinearOrder M
inst_2 : CanonicallyOrderedAdd M
inst_3 : Sub M
inst_4 : AddLeftReflectLE M
inst_5 : OrderedSub M
s : Finset ι
inst_6 : OrderBot M
hs : s.Nonempty
f : ι → M
a : M
⊢ a + s.sup f = s.sup fun (i : ι) ↦ a + f i
have rw : a + s.sup' hs f = s.sup fun (i : ι) ↦ a + f i
Tactic: rw [← Finset.sup'_eq_sup hs, ← Finset.sup'_eq_sup hs, add_sup'']
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Finset (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : AddCommMonoid M
inst_1 : LinearOrder M
inst_2 : CanonicallyOrderedAdd M
inst_3 : Sub M
inst_4 : AddLeftReflectLE M
inst_5 : OrderedSub M
s : Finset ι
inst_6 : OrderBot M
hs : s.Nonempty
f : ι → M
a : M
rw : a + s.sup' hs f = s.sup fun (i : ι) ↦ a + f i
⊢ a + s.sup f = s.sup fun (i : ι) ↦ a + f i
have rw₁ : a + s.sup' hs f = s.sup' hs fun (i : ι) ↦ a + f i
Tactic: rw [← Finset.sup'_eq_sup hs, ← Finset.sup'_eq_sup hs, add_sup'']
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Finset (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : AddCommMonoid M
inst_1 : LinearOrder M
inst_2 : CanonicallyOrderedAdd M
inst_3 : Sub M
inst_4 : AddLeftReflectLE M
inst_5 : OrderedSub M
s : Finset ι
inst_6 : OrderBot M
hs : s.Nonempty
f : ι → M
a : M
rw : a + s.sup' hs f = s.sup fun (i : ι) ↦ a + f i
rw₁ : a + s.sup' hs f = s.sup' hs fun (i : ι) ↦ a + f i
⊢ a + s.sup f = s.sup fun (i : ι) ↦ a + f i
have rw₂ : Eq.{u_3 + 1} (α := M) (s.sup' hs fun (i : ι) ↦ a + f i) (s.sup' hs fun (i : ι) ↦ a + f i)
Tactic: rw [← Finset.sup'_eq_sup hs, ← Finset.sup'_eq_sup hs, add_sup'']
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Ideal (hypothesis)
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : PartialOrder M
inst_2 : WellQuasiOrderedLE M
inst_3 : CanonicallyOrderedMul M
I : SemigroupIdeal M
⊢ I.FG
have hpwo : Set.IsPWO.{u_1} (α := M) {x : M | x ∈ I}
Tactic: have hpwo := Set.isPWO_of_wellQuasiOrderedLE { x | x ∈ I }
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Ideal (goal)
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : PartialOrder M
inst_2 : WellQuasiOrderedLE M
inst_3 : CanonicallyOrderedMul M
I : SemigroupIdeal M
hpwo : Set.IsPWO.{u_1} (α := M) {x : M | x ∈ I}
⊢ I.FG
have refine : I = closure {x : M | Minimal (fun (x : M) ↦ Membership.mem (γ := Set M) {x : M | x ∈ I} x) x}
Tactic: refine ⟨_, (setOf_minimal_antichain _).finite_of_partiallyWellOrderedOn
    (hpwo.mono (setOf_minimal_subset _)), ?_⟩