awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Algebra
Goal:
α : Type u_1
β : Type u_2
inst : CommSemiring α
inst_1 : PartialOrder α
inst_2 : Semiring β
inst_3 : PartialOrder β
inst_4 : Algebra α β
inst_5 : ZeroLEOneClass β
inst_6 : Nontrivial β
inst_7 : SMulPosMono α β
inst_8 : SMulPosReflectLE α β
a₁ a₂ : α
⊢ LE.le.{u_2} (α := β) ((algebraMap α β : (a : α) → β) a₁ : β) ((algebraMap α β : (a : α) → β) a₂ : β) ↔ a₁ ≤ a₂

Tactic:
simp [Algebra.algebraMap_eq_smul_one]

Premises used: Algebra.algebraMap_eq_smul_one
-- Module: Mathlib.Algebra.Order.Algebra
Goal:
α : Type u_1
β : Type u_2
inst : CommSemiring α
inst_1 : PartialOrder α
inst_2 : Semiring β
inst_3 : PartialOrder β
inst_4 : Algebra α β
inst_5 : ZeroLEOneClass β
inst_6 : Nontrivial β
inst_7 : SMulPosStrictMono α β
⊢ StrictMono.{u_1, u_2} (α := α) (β := β) (⇑(algebraMap α β) : (a : α) → β)

Tactic:
simpa [Algebra.smul_def] using smul_one_strictMono (α := α) β

Premises used: smul_one_strictMono, Algebra.smul_def
-- Module: Mathlib.Algebra.Order.Algebra
Goal:
α : Type u_1
β : Type u_2
inst : CommSemiring α
inst_1 : PartialOrder α
inst_2 : Semiring β
inst_3 : PartialOrder β
inst_4 : Algebra α β
inst_5 : ZeroLEOneClass β
inst_6 : Nontrivial β
inst_7 : SMulPosStrictMono α β
a : α
ha : 0 < a
⊢ LT.lt.{u_2} (α := β) (0 : β) ((algebraMap α β : (a : α) → β) a : β)

Tactic:
simpa using algebraMap_strictMono β ha

Premises used: algebraMap_strictMono
-- Module: Mathlib.Algebra.Order.Algebra
Goal:
α : Type u_1
β : Type u_2
inst : CommSemiring α
inst_1 : PartialOrder α
inst_2 : Semiring β
inst_3 : PartialOrder β
inst_4 : Algebra α β
inst_5 : ZeroLEOneClass β
inst_6 : Nontrivial β
inst_7 : SMulPosStrictMono α β
inst_8 : SMulPosReflectLT α β
a₁ a₂ : α
⊢ LT.lt.{u_2} (α := β) ((algebraMap α β : (a : α) → β) a₁ : β) ((algebraMap α β : (a : α) → β) a₂ : β) ↔ a₁ < a₂

Tactic:
simp [Algebra.algebraMap_eq_smul_one]

Premises used: Algebra.algebraMap_eq_smul_one
-- Module: Mathlib.Algebra.Order.Algebra
Goal:
α : Type u_1
β : Type u_2
inst : CommSemiring α
inst_1 : PartialOrder α
inst_2 : Semiring β
inst_3 : PartialOrder β
inst_4 : Algebra α β
inst_5 : IsOrderedRing β
inst_6 : SMulPosMono α β
a : α
ha : 0 ≤ a
⊢ LE.le.{u_2} (α := β) (0 : β) ((algebraMap α β : (a : α) → β) a : β)

Tactic:
positivity
-- Module: Mathlib.Algebra.Order.Algebra
Goal:
α : Type u_1
β : Type u_2
inst : CommSemiring α
inst_1 : PartialOrder α
inst_2 : Semiring β
inst_3 : PartialOrder β
inst_4 : Algebra α β
inst_5 : IsOrderedRing β
inst_6 : SMulPosMono α β
a : α
ha : 0 < a
⊢ LE.le.{u_2} (α := β) (0 : β) ((algebraMap α β : (a : α) → β) a : β)

Tactic:
positivity
-- Module: Mathlib.Algebra.Order.Algebra
Goal:
α : Type u_1
β : Type u_2
inst : CommSemiring α
inst_1 : PartialOrder α
inst_2 : Semiring β
inst_3 : PartialOrder β
inst_4 : Algebra α β
inst_5 : IsStrictOrderedRing β
inst_6 : SMulPosStrictMono α β
a : α
ha : 0 < a
⊢ LT.lt.{u_2} (α := β) (0 : β) ((algebraMap α β : (a : α) → β) a : β)

Tactic:
positivity
-- Module: Mathlib.Algebra.Order.Antidiag.Finsupp
Goal:
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
s_1 : Finset ι
n_1 : μ
f_1 : ι →₀ μ
s : Finset ι
n : μ
f : ↥(s.piAntidiag n)
⊢ ∀ (a : ι), a ∈ {x ∈ s | (↑f : ι → μ) x ≠ 0} ↔ (↑f : ι → μ) a ≠ 0

Tactic:
simpa using (mem_piAntidiag.1 f.2).2

Premises used: Finset.mem_piAntidiag, And.right, Iff.mp, Subtype.property
-- Module: Mathlib.Algebra.Order.Antidiag.Finsupp
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 ↔ s.sum (⇑f : (a : ι) → μ) = n ∧ f.support ⊆ s

Tactic:
simp [finsuppAntidiag, ← DFunLike.coe_fn_eq, subset_iff]

Premises used: Finset.finsuppAntidiag, DFunLike.coe_fn_eq, Finset.subset_iff
-- Module: Mathlib.Algebra.Order.Antidiag.Finsupp
Goal:
ι : Type u_1
μ : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
s : Finset ι
n : μ
f : ι →₀ μ
simp : f.support ⊆ s → (s.sum (⇑f : (a : ι) → μ) = n ↔ (f.sum fun (x : ι) (x_1 : μ) ↦ x_1) = n)
⊢ Membership.mem (γ := Finset (ι →₀ μ)) (s.finsuppAntidiag n) f ↔
    (f.sum fun (x : ι) (x_1 : μ) ↦ x_1) = n ∧ f.support ⊆ s

Tactic:
simp only [mem_finsuppAntidiag, and_congr_left_iff]

Premises used: Finset.mem_finsuppAntidiag, and_congr_left_iff
-- Module: Mathlib.Algebra.Order.Antidiag.Finsupp
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
rw rw₁ : s.sum (⇑f : (a : ι) → μ) = n ↔ ∑ x ∈ s, (f : (a : ι) → μ) x = n
⊢ s.sum (⇑f : (a : ι) → μ) = n ↔ (f.sum fun (x : ι) (x_1 : μ) ↦ x_1) = n

Tactic:
rw [sum_of_support_subset (N := μ) f hf (fun _ x ↦ x) fun _ _ ↦ rfl]

Premises used: rfl, Finsupp.sum_of_support_subset
-- Module: Mathlib.Algebra.Order.Antidiag.Finsupp
Goal:
ι : Type u_1
μ : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
h :
  ∀ (f : ι →₀ μ),
    Membership.mem (γ := Finset (ι →₀ μ)) (finsuppAntidiag ∅ 0) f ↔ Membership.mem (γ := Finset (ι →₀ μ)) {0} f
⊢ Eq (α := Finset (ι →₀ μ)) (finsuppAntidiag ∅ 0) {0}

Tactic:
ext f
-- Module: Mathlib.Algebra.Order.Antidiag.Finsupp
Goal:
ι : Type u_1
μ : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
f : ι →₀ μ
⊢ Membership.mem (γ := Finset (ι →₀ μ)) (finsuppAntidiag ∅ 0) f ↔ Membership.mem (γ := Finset (ι →₀ μ)) {0} f

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Antidiag.Finsupp
Goal:
ι : Type u_1
μ : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
n : μ
hn : n ≠ 0
⊢ ∀ (x : ι →₀ μ), x ∉ finsuppAntidiag ∅ n

Tactic:
simp [hn.symm]

Premises used: Ne.symm
-- Module: Mathlib.Algebra.Order.Antidiag.Finsupp
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}
neg : ∀ (hn : ¬n = 0), Eq (α := Finset (ι →₀ μ)) (finsuppAntidiag ∅ n) ∅
⊢ Eq (α := Finset (ι →₀ μ)) (finsuppAntidiag ∅ n) (if n = 0 then {0} else ∅)

Tactic:
split_ifs with hn
-- Module: Mathlib.Algebra.Order.Antidiag.Finsupp
Goal:
ι : Type u_1
μ : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
n : μ
hn : n = 0
⊢ Eq (α := Finset (ι →₀ μ)) (finsuppAntidiag ∅ n) {0}

Tactic:
simp [*]
-- Module: Mathlib.Algebra.Order.Antidiag.Finsupp
Goal:
ι : Type u_1
μ : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
n : μ
hn : ¬n = 0
⊢ Eq (α := Finset (ι →₀ μ)) (finsuppAntidiag ∅ n) ∅

Tactic:
simp [*]
-- Module: Mathlib.Algebra.Order.Antidiag.Finsupp
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 : ι →₀ μ
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
⊢ 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

Tactic:
simp only [mem_finsuppAntidiag, mem_antidiagonal, Prod.exists, sum_insert h]

Premises used: Finset.mem_finsuppAntidiag, Finset.HasAntidiagonal.mem_antidiagonal, Finset.sum_insert, Prod.exists
-- Module: Mathlib.Algebra.Order.Antidiag.Finsupp
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
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
⊢ 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:
constructor
-- Module: Mathlib.Algebra.Order.Antidiag.Finsupp
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

Tactic:
⟨_, _, rfl, Finsupp.erase a f, ?_, ?_, ?_⟩

Premises used: Finsupp.erase, And.intro, Exists.intro, rfl
-- Module: Mathlib.Algebra.Order.Antidiag.Finsupp
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)
mp₂ : (Finsupp.erase a f).support ⊆ 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

Tactic:
refine ⟨_, _, rfl, Finsupp.erase a f, ?_, ?_, ?_⟩
-- Module: Mathlib.Algebra.Order.Antidiag.Finsupp
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)
mp₁ mp₂ : f = f
⊢ f = (Finsupp.erase a f).update a ((f : (a : ι) → μ) a)

Tactic:
rw [update_erase_eq_update, Finsupp.update_self]

Premises used: Finsupp.update_self, Finsupp.update_erase_eq_update
-- Module: Mathlib.Algebra.Order.Antidiag.Finsupp
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 : ∀ x ∈ s, Eq.{u_2 + 1} (α := μ) ((Finsupp.erase a f : (a : ι) → μ) x : μ) ((f : (a : ι) → μ) x : μ)
⊢ Eq.{u_2 + 1} (α := μ) (s.sum (⇑(Finsupp.erase a f) : (a : ι) → μ)) (∑ x ∈ s, (f : (a : ι) → μ) x)

Tactic:
apply sum_congr rfl

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Algebra.Order.Antidiag.Finsupp
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
mp mp₁ : Eq.{u_2 + 1} (α := μ) ((f : (a : ι) → μ) x : μ) ((f : (a : ι) → μ) x : μ)
⊢ Eq.{u_2 + 1} (α := μ) ((Finsupp.erase a f : (a : ι) → μ) x : μ) ((f : (a : ι) → μ) x : μ)

Tactic:
rw [Finsupp.erase_ne (ne_of_mem_of_not_mem hx h)]

Premises used: Finsupp.erase_ne, ne_of_mem_of_not_mem
-- Module: Mathlib.Algebra.Order.Antidiag.Finsupp
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.support.erase a ⊆ s
mp₁ mp₂ mp₃ mp₄ : f.support ⊆ insert a s
⊢ (Finsupp.erase a f).support ⊆ s

Tactic:
rwa [support_erase, ← subset_insert_iff]

Premises used: Finsupp.support_erase, Finset.subset_insert_iff
-- Module: Mathlib.Algebra.Order.Antidiag.Finsupp
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

Tactic:
⟨?_, (support_update_subset _ _).trans (insert_subset_insert a hgsupp)⟩

Premises used: Finset.insert_subset_insert, HasSubset.Subset.trans, Finsupp.support_update_subset, And.intro
-- Module: Mathlib.Algebra.Order.Antidiag.Finsupp
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 :
  HAdd.hAdd (α := μ) (β := μ) ((g.update a n1 : (a : ι) → μ) a : μ) (∑ x ∈ s, (g.update a n1 : (a : ι) → μ) x : μ) =
    n1 + s.sum (⇑g : (a : ι) → μ)
⊢ 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

Tactic:
refine ⟨?_, (support_update_subset _ _).trans (insert_subset_insert a hgsupp)⟩
-- Module: Mathlib.Algebra.Order.Antidiag.Finsupp
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 :
  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 : ι) → μ)
⊢ HAdd.hAdd (α := μ) (β := μ) ((g.update a n1 : (a : ι) → μ) a : μ) (∑ x ∈ s, (g.update a n1 : (a : ι) → μ) x : μ) =
    n1 + s.sum (⇑g : (a : ι) → μ)

Tactic:
simp only [coe_update]

Premises used: Finsupp.coe_update
-- Module: Mathlib.Algebra.Order.Antidiag.Finsupp
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
mpr₁ :
  Eq.{u_2 + 1} (α := μ) (∑ x ∈ s, Function.update (β := fun (a : ι) ↦ μ) (⇑g : (a : ι) → μ) a n1 x)
    (s.sum (⇑g : (a : ι) → μ))
⊢ 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:
apply congr_arg₂

Premises used: congr_arg₂
-- Module: Mathlib.Algebra.Order.Antidiag.Finsupp
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 mpr₁ : n1 = n1
⊢ Function.update (β := fun (a : ι) ↦ μ) (⇑g : (a : ι) → μ) a n1 a = n1

Tactic:
rw [Function.update_self]

Premises used: Function.update_self
-- Module: Mathlib.Algebra.Order.Antidiag.Finsupp
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 :
  ∀ x ∈ s,
    Eq.{u_2 + 1} (α := μ) (Function.update (β := fun (a : ι) ↦ μ) (⇑g : (a : ι) → μ) a n1 x : μ)
      ((g : (a : ι) → μ) x : μ)
⊢ Eq.{u_2 + 1} (α := μ) (∑ x ∈ s, Function.update (β := fun (a : ι) ↦ μ) (⇑g : (a : ι) → μ) a n1 x)
    (s.sum (⇑g : (a : ι) → μ))

Tactic:
apply sum_congr rfl

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Algebra.Order.Antidiag.Finsupp
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
mpr mpr₁ : Eq.{u_2 + 1} (α := μ) ((g : (a : ι) → μ) x : μ) ((g : (a : ι) → μ) x : μ)
⊢ Eq.{u_2 + 1} (α := μ) (Function.update (β := fun (a : ι) ↦ μ) (⇑g : (a : ι) → μ) a n1 x : μ) ((g : (a : ι) → μ) x : μ)

Tactic:
rw [update_of_ne (ne_of_mem_of_not_mem hx h) n1 ⇑g]

Premises used: ne_of_mem_of_not_mem, DFunLike.coe, Function.update_of_ne
-- Module: Mathlib.Algebra.Order.Antidiag.Finsupp
Goal:
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
s_1 : Finset ι
n_1 : μ
f_1 : ι →₀ μ
a : ι
s : Finset ι
h : a ∉ s
n : μ
p : μ × μ
x x_1 : ↥(s.finsuppAntidiag p.2)
f : ι →₀ μ
hf : Membership.mem (γ := Finset (ι →₀ μ)) (s.finsuppAntidiag p.2) f
g : ι →₀ μ
hg : Membership.mem (γ := Finset (ι →₀ μ)) (s.finsuppAntidiag p.2) g
hfg :
  Eq (α := ι →₀ μ)
    ((fun (f : ↥(s.finsuppAntidiag p.2)) ↦ (↑f : ι →₀ μ).update a p.1)
      (Subtype.mk (p := fun (x : ι →₀ μ) ↦ Membership.mem (γ := Finset (ι →₀ μ)) (s.finsuppAntidiag p.2) x) f hf))
    ((fun (f : ↥(s.finsuppAntidiag p.2)) ↦ (↑f : ι →₀ μ).update a p.1)
      (Subtype.mk (p := fun (x : ι →₀ μ) ↦ Membership.mem (γ := Finset (ι →₀ μ)) (s.finsuppAntidiag p.2) x) g hg))
⊢ s.sum (⇑f : (a : ι) → μ) = p.2 ∧ f.support ⊆ s

Tactic:
simp only [mem_finsuppAntidiag] at hf hg

Premises used: Finset.mem_finsuppAntidiag
-- Module: Mathlib.Algebra.Order.Antidiag.Finsupp
Goal:
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
s_1 : Finset ι
n_1 : μ
f_1 : ι →₀ μ
a : ι
s : Finset ι
h : a ∉ s
n : μ
p : μ × μ
x x_1 : ↥(s.finsuppAntidiag p.2)
f : ι →₀ μ
hf : Membership.mem (γ := Finset (ι →₀ μ)) (s.finsuppAntidiag p.2) f
g : ι →₀ μ
hg : Membership.mem (γ := Finset (ι →₀ μ)) (s.finsuppAntidiag p.2) g
hfg :
  Eq (α := ι →₀ μ)
    ((fun (f : ↥(s.finsuppAntidiag p.2)) ↦ (↑f : ι →₀ μ).update a p.1)
      (Subtype.mk (p := fun (x : ι →₀ μ) ↦ Membership.mem (γ := Finset (ι →₀ μ)) (s.finsuppAntidiag p.2) x) f hf))
    ((fun (f : ↥(s.finsuppAntidiag p.2)) ↦ (↑f : ι →₀ μ).update a p.1)
      (Subtype.mk (p := fun (x : ι →₀ μ) ↦ Membership.mem (γ := Finset (ι →₀ μ)) (s.finsuppAntidiag p.2) x) g hg))
hf₁ : s.sum (⇑f : (a : ι) → μ) = p.2 ∧ f.support ⊆ s
⊢ s.sum (⇑g : (a : ι) → μ) = p.2 ∧ g.support ⊆ s

Tactic:
simp only [mem_finsuppAntidiag] at hf hg

Premises used: Finset.mem_finsuppAntidiag
-- Module: Mathlib.Algebra.Order.Antidiag.Finsupp
Goal:
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
s_1 : Finset ι
n_1 : μ
f_1 : ι →₀ μ
a : ι
s : Finset ι
h : a ∉ s
n : μ
p : μ × μ
x x_1 : ↥(s.finsuppAntidiag p.2)
f : ι →₀ μ
hf_1 : Membership.mem (γ := Finset (ι →₀ μ)) (s.finsuppAntidiag p.2) f
g : ι →₀ μ
hg_1 : Membership.mem (γ := Finset (ι →₀ μ)) (s.finsuppAntidiag p.2) g
hfg :
  Eq (α := ι →₀ μ)
    ((fun (f : ↥(s.finsuppAntidiag p.2)) ↦ (↑f : ι →₀ μ).update a p.1)
      (Subtype.mk (p := fun (x : ι →₀ μ) ↦ Membership.mem (γ := Finset (ι →₀ μ)) (s.finsuppAntidiag p.2) x) f hf_1))
    ((fun (f : ↥(s.finsuppAntidiag p.2)) ↦ (↑f : ι →₀ μ).update a p.1)
      (Subtype.mk (p := fun (x : ι →₀ μ) ↦ Membership.mem (γ := Finset (ι →₀ μ)) (s.finsuppAntidiag p.2) x) g hg_1))
hf : s.sum (⇑f : (a : ι) → μ) = p.2 ∧ f.support ⊆ s
hg : s.sum (⇑g : (a : ι) → μ) = p.2 ∧ g.support ⊆ s
simp :
  ∀
    (hfg :
      ∀ (x : ι), Eq.{u_2 + 1} (α := μ) ((f.update a p.1 : (a : ι) → μ) x : μ) ((g.update a p.1 : (a : ι) → μ) x : μ))
    (x : ι), Eq.{u_2 + 1} (α := μ) ((f : (a : ι) → μ) x : μ) ((g : (a : ι) → μ) x : μ)
⊢ (↑(Subtype.mk (p := fun (x : ι →₀ μ) ↦ Membership.mem (γ := Finset (ι →₀ μ)) (s.finsuppAntidiag p.2) x) f hf_1) :
      ι →₀ μ) =
    (↑(Subtype.mk (p := fun (x : ι →₀ μ) ↦ Membership.mem (γ := Finset (ι →₀ μ)) (s.finsuppAntidiag p.2) x) g hg_1) :
      ι →₀ μ)

Tactic:
simp only [DFunLike.ext_iff] at hfg ⊢

Premises used: DFunLike.ext_iff
-- Module: Mathlib.Algebra.Order.Antidiag.Finsupp
Goal:
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
s_1 : Finset ι
n_1 : μ
f_1 : ι →₀ μ
a : ι
s : Finset ι
h : a ∉ s
n : μ
p : μ × μ
x_1 x_2 : ↥(s.finsuppAntidiag p.2)
f : ι →₀ μ
hf_1 : Membership.mem (γ := Finset (ι →₀ μ)) (s.finsuppAntidiag p.2) f
g : ι →₀ μ
hg_1 : Membership.mem (γ := Finset (ι →₀ μ)) (s.finsuppAntidiag p.2) g
hf : s.sum (⇑f : (a : ι) → μ) = p.2 ∧ f.support ⊆ s
hg : s.sum (⇑g : (a : ι) → μ) = p.2 ∧ g.support ⊆ s
hfg : ∀ (x : ι), Eq.{u_2 + 1} (α := μ) ((f.update a p.1 : (a : ι) → μ) x : μ) ((g.update a p.1 : (a : ι) → μ) x : μ)
x : ι
inl :
  ∀ (h : x ∉ s)
    (hfg :
      ∀ (x_3 : ι),
        Eq.{u_2 + 1} (α := μ) ((f.update x p.1 : (a : ι) → μ) x_3 : μ) ((g.update x p.1 : (a : ι) → μ) x_3 : μ)),
    Eq.{u_2 + 1} (α := μ) ((f : (a : ι) → μ) x : μ) ((g : (a : ι) → μ) x : μ)
inr : ∀ (hx : x ≠ a), Eq.{u_2 + 1} (α := μ) ((f : (a : ι) → μ) x : μ) ((g : (a : ι) → μ) x : μ)
⊢ Eq.{u_2 + 1} (α := μ) ((f : (a : ι) → μ) x : μ) ((g : (a : ι) → μ) x : μ)

Tactic:
obtain rfl | hx := eq_or_ne x a

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Algebra.Order.Antidiag.Finsupp
Goal:
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
s_1 : Finset ι
n_1 : μ
f_1 : ι →₀ μ
s : Finset ι
n : μ
p : μ × μ
x_1 x_2 : ↥(s.finsuppAntidiag p.2)
f : ι →₀ μ
hf_1 : Membership.mem (γ := Finset (ι →₀ μ)) (s.finsuppAntidiag p.2) f
g : ι →₀ μ
hg_1 : Membership.mem (γ := Finset (ι →₀ μ)) (s.finsuppAntidiag p.2) g
hf : s.sum (⇑f : (a : ι) → μ) = p.2 ∧ f.support ⊆ s
hg : s.sum (⇑g : (a : ι) → μ) = p.2 ∧ g.support ⊆ s
x : ι
h : x ∉ s
hfg :
  ∀ (x_3 : ι), Eq.{u_2 + 1} (α := μ) ((f.update x p.1 : (a : ι) → μ) x_3 : μ) ((g.update x p.1 : (a : ι) → μ) x_3 : μ)
⊢ x ∉ f.support

Tactic:
replace hf := mt (hf.2 ·) h
-- Module: Mathlib.Algebra.Order.Antidiag.Finsupp
Goal:
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
s_1 : Finset ι
n_1 : μ
f_1 : ι →₀ μ
s : Finset ι
n : μ
p : μ × μ
x_1 x_2 : ↥(s.finsuppAntidiag p.2)
f : ι →₀ μ
hf_1 : Membership.mem (γ := Finset (ι →₀ μ)) (s.finsuppAntidiag p.2) f
g : ι →₀ μ
hg_1 : Membership.mem (γ := Finset (ι →₀ μ)) (s.finsuppAntidiag p.2) g
hg : s.sum (⇑g : (a : ι) → μ) = p.2 ∧ g.support ⊆ s
x : ι
h : x ∉ s
hfg :
  ∀ (x_3 : ι), Eq.{u_2 + 1} (α := μ) ((f.update x p.1 : (a : ι) → μ) x_3 : μ) ((g.update x p.1 : (a : ι) → μ) x_3 : μ)
hf : x ∉ f.support
⊢ x ∉ g.support

Tactic:
replace hg := mt (hg.2 ·) h
-- Module: Mathlib.Algebra.Order.Antidiag.Finsupp
Goal:
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
s_1 : Finset ι
n_1 : μ
f_1 : ι →₀ μ
s : Finset ι
n : μ
p : μ × μ
x_1 x_2 : ↥(s.finsuppAntidiag p.2)
f : ι →₀ μ
hf_1 : Membership.mem (γ := Finset (ι →₀ μ)) (s.finsuppAntidiag p.2) f
g : ι →₀ μ
hg_1 : Membership.mem (γ := Finset (ι →₀ μ)) (s.finsuppAntidiag p.2) g
x : ι
h : x ∉ s
hfg :
  ∀ (x_3 : ι), Eq.{u_2 + 1} (α := μ) ((f.update x p.1 : (a : ι) → μ) x_3 : μ) ((g.update x p.1 : (a : ι) → μ) x_3 : μ)
hf : x ∉ f.support
hg : x ∉ g.support
inl : Eq.{u_2 + 1} (α := μ) (0 : μ) ((g : (a : ι) → μ) x : μ)
inl₁ inl₂ : Eq.{u_2 + 1} (α := μ) 0 0
⊢ Eq.{u_2 + 1} (α := μ) ((f : (a : ι) → μ) x : μ) ((g : (a : ι) → μ) x : μ)

Tactic:
rw [notMem_support_iff.mp hf, notMem_support_iff.mp hg]

Premises used: Finsupp.notMem_support_iff, Iff.mp