awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.AddGroupWithTop (goal)
Goal:
α : Type u_2
inst : LinearOrderedAddCommGroupWithTop α
a b : α
⊢ 0 < a - b ↔ b < a ∨ b = ⊤
have inl : 0 < a - ⊤ ↔ ⊤ < a ∨ Eq.{u_2 + 1} (α := α) ⊤ ⊤
Tactic: obtain rfl | hb := eq_or_ne b ⊤
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Algebra.Order.AddGroupWithTop (goal)
Goal:
α : Type u_2
inst : LinearOrderedAddCommGroupWithTop α
a b : α
inl : 0 < a - ⊤ ↔ ⊤ < a ∨ Eq.{u_2 + 1} (α := α) ⊤ ⊤
⊢ 0 < a - b ↔ b < a ∨ b = ⊤
have inr : ∀ (hb : b ≠ ⊤), 0 < a - b ↔ b < a ∨ b = ⊤
Tactic: obtain rfl | hb := eq_or_ne b ⊤
-- Lean 4 proof step from Mathlib.Algebra.Order.AddGroupWithTop (goal)
Goal:
α : Type u_2
inst : LinearOrderedAddCommGroupWithTop α
a : α
⊢ 0 ≤ a - a
have inl : 0 ≤ HSub.hSub (α := α) ⊤ ⊤
Tactic: obtain rfl | ha := eq_or_ne a ⊤
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Algebra.Order.AddGroupWithTop (goal)
Goal:
α : Type u_2
inst : LinearOrderedAddCommGroupWithTop α
a : α
inl : 0 ≤ HSub.hSub (α := α) ⊤ ⊤
⊢ 0 ≤ a - a
have inr : ∀ (ha : a ≠ ⊤), 0 ≤ a - a
Tactic: obtain rfl | ha := eq_or_ne a ⊤
-- Lean 4 proof step from Mathlib.Algebra.Order.AddGroupWithTop (goal)
Goal:
α : Type u_2
inst : LinearOrderedAddCommGroupWithTop α
a : α
ha : a ≠ ⊤
⊢ 0 ≤ a - a
have inr : LE.le.{u_2} (α := α) 0 0
Tactic: rw [sub_self_eq_zero_of_ne_top ha]
-- Lean 4 proof step from Mathlib.Algebra.Order.AddGroupWithTop (goal)
Goal:
α : Type u_2
inst : LinearOrderedAddCommGroupWithTop α
a b : α
ha : a ≠ ⊤
⊢ b - a = 0 ↔ b = a
have rw : b - a = a - a ↔ b = a
Tactic: rw [← sub_self_eq_zero_of_ne_top ha, sub_left_inj_of_ne_top ha]
-- Lean 4 proof step from Mathlib.Algebra.Order.AddGroupWithTop (goal)
Goal:
α : Type u_2
inst : LinearOrderedAddCommGroupWithTop α
a b : α
ha : a ≠ ⊤
rw : b - a = a - a ↔ b = a
⊢ b - a = 0 ↔ b = a
have rw₁ : b = a ↔ b = a
Tactic: rw [← sub_self_eq_zero_of_ne_top ha, sub_left_inj_of_ne_top ha]
-- Lean 4 proof step from Mathlib.Algebra.Order.AddGroupWithTop (goal)
Goal:
G : Type u_1
inst : AddCommGroup G
x : WithTop G
⊢ ⊤ - x = ⊤
have top : HSub.hSub (α := WithTop G) ⊤ ⊤ = ⊤
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Order.AddGroupWithTop (goal)
Goal:
G : Type u_1
inst : AddCommGroup G
x : WithTop G
top : HSub.hSub (α := WithTop G) ⊤ ⊤ = ⊤
⊢ ⊤ - x = ⊤
have coe : ∀ (a : G), ⊤ - (↑a : WithTop G) = ⊤
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Order.AddGroupWithTop (goal)
Goal:
G : Type u_1
inst : AddCommGroup G
x : WithTop G
⊢ x - ⊤ = ⊤
have top : HSub.hSub (α := WithTop G) ⊤ ⊤ = ⊤
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Order.AddGroupWithTop (goal)
Goal:
G : Type u_1
inst : AddCommGroup G
x : WithTop G
top : HSub.hSub (α := WithTop G) ⊤ ⊤ = ⊤
⊢ x - ⊤ = ⊤
have coe : ∀ (a : G), (↑a : WithTop G) - ⊤ = ⊤
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Order.AddGroupWithTop (goal)
Goal:
G : Type u_1
inst : AddCommGroup G
x y : WithTop G
⊢ x - y = ⊤ ↔ x = ⊤ ∨ y = ⊤
have top : ⊤ - y = ⊤ ↔ Eq.{u_1 + 1} (α := WithTop G) ⊤ ⊤ ∨ y = ⊤
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Order.AddGroupWithTop (goal)
Goal:
G : Type u_1
inst : AddCommGroup G
x y : WithTop G
top : ⊤ - y = ⊤ ↔ Eq.{u_1 + 1} (α := WithTop G) ⊤ ⊤ ∨ y = ⊤
⊢ x - y = ⊤ ↔ x = ⊤ ∨ y = ⊤
have coe : ∀ (a : G), (↑a : WithTop G) - y = ⊤ ↔ (↑a : WithTop G) = ⊤ ∨ y = ⊤
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Order.AddGroupWithTop (goal)
Goal:
G : Type u_1
inst : AddCommGroup G
y : WithTop G
⊢ ⊤ - y = ⊤ ↔ Eq.{u_1 + 1} (α := WithTop G) ⊤ ⊤ ∨ y = ⊤
have top : HSub.hSub (α := WithTop G) ⊤ ⊤ = ⊤ ↔ Eq.{u_1 + 1} (α := WithTop G) ⊤ ⊤ ∨ Eq.{u_1 + 1} (α := WithTop G) ⊤ ⊤
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.Order.AddGroupWithTop (goal)
Goal:
G : Type u_1
inst : AddCommGroup G
y : WithTop G
top : HSub.hSub (α := WithTop G) ⊤ ⊤ = ⊤ ↔ Eq.{u_1 + 1} (α := WithTop G) ⊤ ⊤ ∨ Eq.{u_1 + 1} (α := WithTop G) ⊤ ⊤
⊢ ⊤ - y = ⊤ ↔ Eq.{u_1 + 1} (α := WithTop G) ⊤ ⊤ ∨ y = ⊤
have top₁ : ∀ (a : G), ⊤ - (↑a : WithTop G) = ⊤ ↔ Eq.{u_1 + 1} (α := WithTop G) ⊤ ⊤ ∨ (↑a : WithTop G) = ⊤
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.Order.AddGroupWithTop (goal)
Goal:
G : Type u_1
inst : AddCommGroup G
y : WithTop G
a : G
⊢ (↑a : WithTop G) - y = ⊤ ↔ (↑a : WithTop G) = ⊤ ∨ y = ⊤
have coe : (↑a : WithTop G) - ⊤ = ⊤ ↔ (↑a : WithTop G) = ⊤ ∨ Eq.{u_1 + 1} (α := WithTop G) ⊤ ⊤
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.Order.AddGroupWithTop (goal)
Goal:
G : Type u_1
inst : AddCommGroup G
y : WithTop G
a : G
coe : (↑a : WithTop G) - ⊤ = ⊤ ↔ (↑a : WithTop G) = ⊤ ∨ Eq.{u_1 + 1} (α := WithTop G) ⊤ ⊤
⊢ (↑a : WithTop G) - y = ⊤ ↔ (↑a : WithTop G) = ⊤ ∨ y = ⊤
have coe₁ : ∀ (a_1 : G), (↑a : WithTop G) - (↑a_1 : WithTop G) = ⊤ ↔ (↑a : WithTop G) = ⊤ ∨ (↑a_1 : WithTop G) = ⊤
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.Order.AddGroupWithTop (goal)
Goal:
G : Type u_1
α : Type u_2
inst : AddCommGroup G
x y : WithTop G
inst_1 : LinearOrder G
inst_2 : IsOrderedAddMonoid G
a b : WithTop G
⊢ a - b = a + -b
have top : ⊤ - b = ⊤ + -b
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Algebra.Order.AddGroupWithTop (goal)
Goal:
G : Type u_1
α : Type u_2
inst : AddCommGroup G
x y : WithTop G
inst_1 : LinearOrder G
inst_2 : IsOrderedAddMonoid G
a b : WithTop G
top : ⊤ - b = ⊤ + -b
⊢ a - b = a + -b
have coe : ∀ (a : G), (↑a : WithTop G) - b = (↑a : WithTop G) + -b
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Algebra.Order.AddGroupWithTop (goal)
Goal:
G : Type u_1
α : Type u_2
inst : AddCommGroup G
x y : WithTop G
inst_1 : LinearOrder G
inst_2 : IsOrderedAddMonoid G
b : WithTop G
⊢ ⊤ - b = ⊤ + -b
have top : HSub.hSub (α := WithTop G) ⊤ ⊤ = HAdd.hAdd (α := WithTop G) ⊤ (-⊤)
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Algebra.Order.AddGroupWithTop (goal)
Goal:
G : Type u_1
α : Type u_2
inst : AddCommGroup G
x y : WithTop G
inst_1 : LinearOrder G
inst_2 : IsOrderedAddMonoid G
b : WithTop G
top : HSub.hSub (α := WithTop G) ⊤ ⊤ = HAdd.hAdd (α := WithTop G) ⊤ (-⊤)
⊢ ⊤ - b = ⊤ + -b
have top₁ : ∀ (a : G), ⊤ - (↑a : WithTop G) = ⊤ + -(↑a : WithTop G)
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Algebra.Order.AddGroupWithTop (goal)
Goal:
G : Type u_1
α : Type u_2
inst : AddCommGroup G
x y : WithTop G
inst_1 : LinearOrder G
inst_2 : IsOrderedAddMonoid G
b : WithTop G
a : G
⊢ (↑a : WithTop G) - b = (↑a : WithTop G) + -b
have coe : (↑a : WithTop G) - ⊤ = (↑a : WithTop G) + -⊤
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Algebra.Order.AddGroupWithTop (goal)
Goal:
G : Type u_1
α : Type u_2
inst : AddCommGroup G
x y : WithTop G
inst_1 : LinearOrder G
inst_2 : IsOrderedAddMonoid G
b : WithTop G
a : G
coe : (↑a : WithTop G) - ⊤ = (↑a : WithTop G) + -⊤
⊢ (↑a : WithTop G) - b = (↑a : WithTop G) + -b
have coe₁ : ∀ (a_1 : G), (↑a : WithTop G) - (↑a_1 : WithTop G) = (↑a : WithTop G) + -(↑a_1 : WithTop G)
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Algebra.Order.AddTorsor (goal)
Goal:
G : Type u_1
P : Type u_2
inst : LE G
inst_1 : Preorder P
inst_2 : SMul G P
inst_3 : IsOrderedCancelSMul G P
a b : G
c d : P
h₁ : a ≤ b
h₂ : c < d
⊢ a • c < b • d
have refine : b • c < b • d
Tactic: refine lt_of_le_of_lt (IsOrderedSMul.smul_le_smul_right a b h₁ c) ?_
-- Lean 4 proof step from Mathlib.Algebra.Order.AddTorsor (goal)
Goal:
G : Type u_1
P : Type u_2
inst : LE G
inst_1 : Preorder P
inst_2 : SMul G P
inst_3 : IsOrderedCancelSMul G P
a b : G
c d : P
h₁ : a ≤ b
h₂ : c < d
⊢ b • c < b • d
have refine : ¬b • d ≤ b • c
Tactic: refine lt_of_le_not_ge (IsOrderedSMul.smul_le_smul_left c d (le_of_lt h₂) b) ?_
-- Lean 4 proof step from Mathlib.Algebra.Order.AddTorsor (hypothesis)
Goal:
G : Type u_1
P : Type u_2
inst : LE G
inst_1 : Preorder P
inst_2 : SMul G P
inst_3 : IsOrderedCancelSMul G P
a b : G
c d : P
h₁ : a ≤ b
h₂ : c < d
hbdc : b • d ≤ b • c
⊢ False
have h : d ≤ c
Tactic: have h : d ≤ c := IsOrderedCancelSMul.le_of_smul_le_smul_left b d c hbdc
-- Lean 4 proof step from Mathlib.Algebra.Order.AddTorsor (hypothesis)
Goal:
G : Type u_1
P : Type u_2
inst : LE G
inst_1 : Preorder P
inst_2 : SMul G P
inst_3 : IsOrderedCancelSMul G P
a b : G
c d : P
h₁ : a ≤ b
h₂ : c < d
hbdc : b • d ≤ b • c
h : d ≤ c
⊢ False
have h₃ : c ≤ d ∧ ¬d ≤ c
Tactic: rw [@lt_iff_le_not_ge] at h₂
Cleared hypotheses: h₂, hbdc, h
-- Lean 4 proof step from Mathlib.Algebra.Order.AddTorsor (goal)
Goal:
G : Type u_1
P : Type u_2
inst : Preorder G
inst_1 : Preorder P
inst_2 : SMul G P
inst_3 : IsOrderedCancelSMul G P
a b : G
c d : P
h₁ : a < b
h₂ : c ≤ d
⊢ a • c < b • d
have refine : a • d < b • d
Tactic: refine lt_of_le_of_lt (IsOrderedSMul.smul_le_smul_left c d h₂ a) ?_
-- Lean 4 proof step from Mathlib.Algebra.Order.AddTorsor (goal)
Goal:
G : Type u_1
P : Type u_2
inst : Preorder G
inst_1 : Preorder P
inst_2 : SMul G P
inst_3 : IsOrderedCancelSMul G P
a b : G
c d : P
h₁ : a < b
h₂ : c ≤ d
⊢ a • d < b • d
have refine : ¬b • d ≤ a • d
Tactic: refine lt_of_le_not_ge (IsOrderedSMul.smul_le_smul_right a b (le_of_lt h₁) d) ?_
-- Lean 4 proof step from Mathlib.Algebra.Order.AddTorsor (hypothesis)
Goal:
G : Type u_1
P : Type u_2
inst : Preorder G
inst_1 : Preorder P
inst_2 : SMul G P
inst_3 : IsOrderedCancelSMul G P
a b : G
c d : P
h₁ : a < b
h₂ : c ≤ d
hbad : b • d ≤ a • d
⊢ False
have h : b ≤ a
Tactic: have h : b ≤ a := IsOrderedCancelSMul.le_of_smul_le_smul_right b a d hbad
-- Lean 4 proof step from Mathlib.Algebra.Order.AddTorsor (hypothesis)
Goal:
G : Type u_1
P : Type u_2
inst : Preorder G
inst_1 : Preorder P
inst_2 : SMul G P
inst_3 : IsOrderedCancelSMul G P
a b : G
c d : P
h₁ : a < b
h₂ : c ≤ d
hbad : b • d ≤ a • d
h : b ≤ a
⊢ False
have h₃ : a ≤ b ∧ ¬b ≤ a
Tactic: rw [@lt_iff_le_not_ge] at h₁
Cleared hypotheses: h₁, h₂, hbad, h
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Finsupp (goal)
Goal:
ι : Type u_1
μ : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
s : Finset ι
n : μ
f : ι →₀ μ
⊢ Membership.mem (γ := Finset (ι →₀ μ)) (s.finsuppAntidiag n) f ↔
    (f.sum fun (x : ι) (x_1 : μ) ↦ x_1) = n ∧ f.support ⊆ s
have simp : f.support ⊆ s → (s.sum (⇑f : (a : ι) → μ) = n ↔ (f.sum fun (x : ι) (x_1 : μ) ↦ x_1) = n)
Tactic: simp only [mem_finsuppAntidiag, and_congr_left_iff]
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Finsupp (goal)
Goal:
ι : Type u_1
μ : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
s : Finset ι
n : μ
f : ι →₀ μ
hf : f.support ⊆ s
⊢ s.sum (⇑f : (a : ι) → μ) = n ↔ (f.sum fun (x : ι) (x_1 : μ) ↦ x_1) = n
have rw : s.sum (⇑f : (a : ι) → μ) = n ↔ ∑ x ∈ s, (f : (a : ι) → μ) x = n
Tactic: rw [sum_of_support_subset (N := μ) f hf (fun _ x ↦ x) fun _ _ ↦ rfl]
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Finsupp (goal)
Goal:
ι : Type u_1
μ : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
⊢ Eq (α := Finset (ι →₀ μ)) (finsuppAntidiag ∅ 0) {0}
have h : ∀ (f : ι →₀ μ),
  Membership.mem (γ := Finset (ι →₀ μ)) (finsuppAntidiag ∅ 0) f ↔ Membership.mem (γ := Finset (ι →₀ μ)) {0} f
Tactic: ext f
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Finsupp (goal)
Goal:
ι : Type u_1
μ : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
n : μ
⊢ Eq (α := Finset (ι →₀ μ)) (finsuppAntidiag ∅ n) (if n = 0 then {0} else ∅)
have pos : ∀ (hn : n = 0), Eq (α := Finset (ι →₀ μ)) (finsuppAntidiag ∅ n) {0}
Tactic: split_ifs with hn
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Finsupp (goal)
Goal:
ι : Type u_1
μ : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
n : μ
pos : ∀ (hn : n = 0), Eq (α := Finset (ι →₀ μ)) (finsuppAntidiag ∅ n) {0}
⊢ Eq (α := Finset (ι →₀ μ)) (finsuppAntidiag ∅ n) (if n = 0 then {0} else ∅)
have neg : ∀ (hn : ¬n = 0), Eq (α := Finset (ι →₀ μ)) (finsuppAntidiag ∅ n) ∅
Tactic: split_ifs with hn
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Finsupp (goal)
Goal:
ι : Type u_1
μ : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
a : ι
s : Finset ι
h : a ∉ s
n : μ
f : ι →₀ μ
⊢ Membership.mem (γ := Finset (ι →₀ μ)) ((insert a s).finsuppAntidiag n) f ↔
    ∃ m ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n,
      ∃ (g : ι →₀ μ), f = g.update a m.1 ∧ Membership.mem (γ := Finset (ι →₀ μ)) (s.finsuppAntidiag m.2) g
have simp : HAdd.hAdd (α := μ) (β := μ) ((f : (a : ι) → μ) a : μ) (∑ x ∈ s, (f : (a : ι) → μ) x : μ) = n ∧ f.support ⊆ insert a s ↔
  ∃ (a_1 : μ) (b : μ), a_1 + b = n ∧ ∃ (g : ι →₀ μ), f = g.update a a_1 ∧ s.sum (⇑g : (a : ι) → μ) = b ∧ g.support ⊆ s
Tactic: simp only [mem_finsuppAntidiag, mem_antidiagonal, Prod.exists, sum_insert h]
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Finsupp (goal)
Goal:
ι : Type u_1
μ : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
a : ι
s : Finset ι
h : a ∉ s
n : μ
f : ι →₀ μ
⊢ HAdd.hAdd (α := μ) (β := μ) ((f : (a : ι) → μ) a : μ) (∑ x ∈ s, (f : (a : ι) → μ) x : μ) = n ∧
      f.support ⊆ insert a s ↔
    ∃ (a_1 : μ) (b : μ), a_1 + b = n ∧ ∃ (g : ι →₀ μ), f = g.update a a_1 ∧ s.sum (⇑g : (a : ι) → μ) = b ∧ g.support ⊆ s
have mp : HAdd.hAdd (α := μ) (β := μ) ((f : (a : ι) → μ) a : μ) (∑ x ∈ s, (f : (a : ι) → μ) x : μ) = n ∧ f.support ⊆ insert a s →
  ∃ (a_2 : μ) (b : μ), a_2 + b = n ∧ ∃ (g : ι →₀ μ), f = g.update a a_2 ∧ s.sum (⇑g : (a : ι) → μ) = b ∧ g.support ⊆ s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Finsupp (goal)
Goal:
ι : Type u_1
μ : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
a : ι
s : Finset ι
h : a ∉ s
n : μ
f : ι →₀ μ
mp :
  HAdd.hAdd (α := μ) (β := μ) ((f : (a : ι) → μ) a : μ) (∑ x ∈ s, (f : (a : ι) → μ) x : μ) = n ∧
      f.support ⊆ insert a s →
    ∃ (a_2 : μ) (b : μ), a_2 + b = n ∧ ∃ (g : ι →₀ μ), f = g.update a a_2 ∧ s.sum (⇑g : (a : ι) → μ) = b ∧ g.support ⊆ s
⊢ HAdd.hAdd (α := μ) (β := μ) ((f : (a : ι) → μ) a : μ) (∑ x ∈ s, (f : (a : ι) → μ) x : μ) = n ∧
      f.support ⊆ insert a s ↔
    ∃ (a_1 : μ) (b : μ), a_1 + b = n ∧ ∃ (g : ι →₀ μ), f = g.update a a_1 ∧ s.sum (⇑g : (a : ι) → μ) = b ∧ g.support ⊆ s
have mpr : (∃ (a_1 : μ) (b : μ), a_1 + b = n ∧ ∃ (g : ι →₀ μ), f = g.update a a_1 ∧ s.sum (⇑g : (a : ι) → μ) = b ∧ g.support ⊆ s) →
  HAdd.hAdd (α := μ) (β := μ) ((f : (a : ι) → μ) a : μ) (∑ x ∈ s, (f : (a : ι) → μ) x : μ) = n ∧ f.support ⊆ insert a s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Finsupp (goal)
Goal:
ι : Type u_1
μ : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
a : ι
s : Finset ι
h : a ∉ s
f : ι →₀ μ
hsupp : f.support ⊆ insert a s
⊢ ∃ (a_1 : μ) (b : μ),
    a_1 + b = HAdd.hAdd (α := μ) (β := μ) ((f : (a : ι) → μ) a : μ) (∑ x ∈ s, (f : (a : ι) → μ) x : μ) ∧
      ∃ (g : ι →₀ μ), f = g.update a a_1 ∧ s.sum (⇑g : (a : ι) → μ) = b ∧ g.support ⊆ s
have mp : f = (Finsupp.erase a f).update a ((f : (a : ι) → μ) a)
Tactic: refine ⟨_, _, rfl, Finsupp.erase a f, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Finsupp (goal)
Goal:
ι : Type u_1
μ : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
a : ι
s : Finset ι
h : a ∉ s
f : ι →₀ μ
hsupp : f.support ⊆ insert a s
mp : f = (Finsupp.erase a f).update a ((f : (a : ι) → μ) a)
⊢ ∃ (a_1 : μ) (b : μ),
    a_1 + b = HAdd.hAdd (α := μ) (β := μ) ((f : (a : ι) → μ) a : μ) (∑ x ∈ s, (f : (a : ι) → μ) x : μ) ∧
      ∃ (g : ι →₀ μ), f = g.update a a_1 ∧ s.sum (⇑g : (a : ι) → μ) = b ∧ g.support ⊆ s
have mp₁ : Eq.{u_2 + 1} (α := μ) (s.sum (⇑(Finsupp.erase a f) : (a : ι) → μ)) (∑ x ∈ s, (f : (a : ι) → μ) x)
Tactic: refine ⟨_, _, rfl, Finsupp.erase a f, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Finsupp (goal)
Goal:
ι : Type u_1
μ : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
a : ι
s : Finset ι
h : a ∉ s
f : ι →₀ μ
hsupp : f.support ⊆ insert a s
mp : f = (Finsupp.erase a f).update a ((f : (a : ι) → μ) a)
mp₁ : Eq.{u_2 + 1} (α := μ) (s.sum (⇑(Finsupp.erase a f) : (a : ι) → μ)) (∑ x ∈ s, (f : (a : ι) → μ) x)
⊢ ∃ (a_1 : μ) (b : μ),
    a_1 + b = HAdd.hAdd (α := μ) (β := μ) ((f : (a : ι) → μ) a : μ) (∑ x ∈ s, (f : (a : ι) → μ) x : μ) ∧
      ∃ (g : ι →₀ μ), f = g.update a a_1 ∧ s.sum (⇑g : (a : ι) → μ) = b ∧ g.support ⊆ s
have mp₂ : (Finsupp.erase a f).support ⊆ s
Tactic: refine ⟨_, _, rfl, Finsupp.erase a f, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Finsupp (goal)
Goal:
ι : Type u_1
μ : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
a : ι
s : Finset ι
h : a ∉ s
f : ι →₀ μ
hsupp : f.support ⊆ insert a s
⊢ f = (Finsupp.erase a f).update a ((f : (a : ι) → μ) a)
have mp : f = f.update a ((f : (a : ι) → μ) a)
Tactic: rw [update_erase_eq_update, Finsupp.update_self]
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Finsupp (goal)
Goal:
ι : Type u_1
μ : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
a : ι
s : Finset ι
h : a ∉ s
f : ι →₀ μ
hsupp : f.support ⊆ insert a s
mp : f = f.update a ((f : (a : ι) → μ) a)
⊢ f = (Finsupp.erase a f).update a ((f : (a : ι) → μ) a)
have mp₁ : f = f
Tactic: rw [update_erase_eq_update, Finsupp.update_self]
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Finsupp (goal)
Goal:
ι : Type u_1
μ : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
a : ι
s : Finset ι
h : a ∉ s
f : ι →₀ μ
hsupp : f.support ⊆ insert a s
⊢ Eq.{u_2 + 1} (α := μ) (s.sum (⇑(Finsupp.erase a f) : (a : ι) → μ)) (∑ x ∈ s, (f : (a : ι) → μ) x)
have mp : ∀ x ∈ s, Eq.{u_2 + 1} (α := μ) ((Finsupp.erase a f : (a : ι) → μ) x : μ) ((f : (a : ι) → μ) x : μ)
Tactic: apply sum_congr rfl
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Finsupp (goal)
Goal:
ι : Type u_1
μ : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
a : ι
s : Finset ι
h : a ∉ s
f : ι →₀ μ
hsupp : f.support ⊆ insert a s
x : ι
hx : x ∈ s
⊢ Eq.{u_2 + 1} (α := μ) ((Finsupp.erase a f : (a : ι) → μ) x : μ) ((f : (a : ι) → μ) x : μ)
have mp : Eq.{u_2 + 1} (α := μ) ((f : (a : ι) → μ) x : μ) ((f : (a : ι) → μ) x : μ)
Tactic: rw [Finsupp.erase_ne (ne_of_mem_of_not_mem hx h)]
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Finsupp (goal)
Goal:
ι : Type u_1
μ : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
a : ι
s : Finset ι
h : a ∉ s
f : ι →₀ μ
hsupp : f.support ⊆ insert a s
⊢ (Finsupp.erase a f).support ⊆ s
have mp : f.support.erase a ⊆ s
Tactic: rwa [support_erase, ← subset_insert_iff]
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Finsupp (goal)
Goal:
ι : Type u_1
μ : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
a : ι
s : Finset ι
h : a ∉ s
n1 : μ
g : ι →₀ μ
hgsupp : g.support ⊆ s
⊢ HAdd.hAdd (α := μ) (β := μ) ((g.update a n1 : (a : ι) → μ) a : μ) (∑ x ∈ s, (g.update a n1 : (a : ι) → μ) x : μ) =
      n1 + s.sum (⇑g : (a : ι) → μ) ∧
    (g.update a n1).support ⊆ insert a s
have mpr : HAdd.hAdd (α := μ) (β := μ) ((g.update a n1 : (a : ι) → μ) a : μ) (∑ x ∈ s, (g.update a n1 : (a : ι) → μ) x : μ) =
  n1 + s.sum (⇑g : (a : ι) → μ)
Tactic: refine ⟨?_, (support_update_subset _ _).trans (insert_subset_insert a hgsupp)⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Finsupp (goal)
Goal:
ι : Type u_1
μ : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
a : ι
s : Finset ι
h : a ∉ s
n1 : μ
g : ι →₀ μ
hgsupp : g.support ⊆ s
⊢ HAdd.hAdd (α := μ) (β := μ) ((g.update a n1 : (a : ι) → μ) a : μ) (∑ x ∈ s, (g.update a n1 : (a : ι) → μ) x : μ) =
    n1 + s.sum (⇑g : (a : ι) → μ)
have mpr : HAdd.hAdd (α := μ) (β := μ) (Function.update (β := fun (a : ι) ↦ μ) (⇑g : (a : ι) → μ) a n1 a : μ)
    (∑ x ∈ s, Function.update (β := fun (a : ι) ↦ μ) (⇑g : (a : ι) → μ) a n1 x : μ) =
  n1 + s.sum (⇑g : (a : ι) → μ)
Tactic: simp only [coe_update]
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Finsupp (goal)
Goal:
ι : Type u_1
μ : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
a : ι
s : Finset ι
h : a ∉ s
n1 : μ
g : ι →₀ μ
hgsupp : g.support ⊆ s
⊢ HAdd.hAdd (α := μ) (β := μ) (Function.update (β := fun (a : ι) ↦ μ) (⇑g : (a : ι) → μ) a n1 a : μ)
      (∑ x ∈ s, Function.update (β := fun (a : ι) ↦ μ) (⇑g : (a : ι) → μ) a n1 x : μ) =
    n1 + s.sum (⇑g : (a : ι) → μ)
have mpr : Function.update (β := fun (a : ι) ↦ μ) (⇑g : (a : ι) → μ) a n1 a = n1
Tactic: apply congr_arg₂
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Finsupp (goal)
Goal:
ι : Type u_1
μ : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
a : ι
s : Finset ι
h : a ∉ s
n1 : μ
g : ι →₀ μ
hgsupp : g.support ⊆ s
mpr : Function.update (β := fun (a : ι) ↦ μ) (⇑g : (a : ι) → μ) a n1 a = n1
⊢ HAdd.hAdd (α := μ) (β := μ) (Function.update (β := fun (a : ι) ↦ μ) (⇑g : (a : ι) → μ) a n1 a : μ)
      (∑ x ∈ s, Function.update (β := fun (a : ι) ↦ μ) (⇑g : (a : ι) → μ) a n1 x : μ) =
    n1 + s.sum (⇑g : (a : ι) → μ)
have mpr₁ : Eq.{u_2 + 1} (α := μ) (∑ x ∈ s, Function.update (β := fun (a : ι) ↦ μ) (⇑g : (a : ι) → μ) a n1 x)
  (s.sum (⇑g : (a : ι) → μ))
Tactic: apply congr_arg₂
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Finsupp (goal)
Goal:
ι : Type u_1
μ : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
a : ι
s : Finset ι
h : a ∉ s
n1 : μ
g : ι →₀ μ
hgsupp : g.support ⊆ s
⊢ Function.update (β := fun (a : ι) ↦ μ) (⇑g : (a : ι) → μ) a n1 a = n1
have mpr : n1 = n1
Tactic: rw [Function.update_self]
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Finsupp (goal)
Goal:
ι : Type u_1
μ : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
a : ι
s : Finset ι
h : a ∉ s
n1 : μ
g : ι →₀ μ
hgsupp : g.support ⊆ s
⊢ Eq.{u_2 + 1} (α := μ) (∑ x ∈ s, Function.update (β := fun (a : ι) ↦ μ) (⇑g : (a : ι) → μ) a n1 x)
    (s.sum (⇑g : (a : ι) → μ))
have mpr : ∀ x ∈ s,
  Eq.{u_2 + 1} (α := μ) (Function.update (β := fun (a : ι) ↦ μ) (⇑g : (a : ι) → μ) a n1 x : μ) ((g : (a : ι) → μ) x : μ)
Tactic: apply sum_congr rfl
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Finsupp (goal)
Goal:
ι : Type u_1
μ : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
a : ι
s : Finset ι
h : a ∉ s
n1 : μ
g : ι →₀ μ
hgsupp : g.support ⊆ s
x : ι
hx : x ∈ s
⊢ Eq.{u_2 + 1} (α := μ) (Function.update (β := fun (a : ι) ↦ μ) (⇑g : (a : ι) → μ) a n1 x : μ) ((g : (a : ι) → μ) x : μ)
have mpr : Eq.{u_2 + 1} (α := μ) ((g : (a : ι) → μ) x : μ) ((g : (a : ι) → μ) x : μ)
Tactic: rw [update_of_ne (ne_of_mem_of_not_mem hx h) n1 ⇑g]