awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Finsupp (hypothesis)
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))
⊢ (↑(Subtype.mk (p := fun (x : ι →₀ μ) ↦ Membership.mem (γ := Finset (ι →₀ μ)) (s.finsuppAntidiag p.2) x) f hf) :
      ι →₀ μ) =
    (↑(Subtype.mk (p := fun (x : ι →₀ μ) ↦ Membership.mem (γ := Finset (ι →₀ μ)) (s.finsuppAntidiag p.2) x) g hg) :
      ι →₀ μ)
have hf₁ : s.sum (⇑f : (a : ι) → μ) = p.2 ∧ f.support ⊆ s
Tactic: simp only [mem_finsuppAntidiag] at hf hg
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Finsupp (hypothesis)
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
⊢ (↑(Subtype.mk (p := fun (x : ι →₀ μ) ↦ Membership.mem (γ := Finset (ι →₀ μ)) (s.finsuppAntidiag p.2) x) f hf) :
      ι →₀ μ) =
    (↑(Subtype.mk (p := fun (x : ι →₀ μ) ↦ Membership.mem (γ := Finset (ι →₀ μ)) (s.finsuppAntidiag p.2) x) g hg) :
      ι →₀ μ)
have hg₁ : s.sum (⇑g : (a : ι) → μ) = p.2 ∧ g.support ⊆ s
Tactic: simp only [mem_finsuppAntidiag] at hf hg
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Finsupp (goal)
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
⊢ (↑(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) :
      ι →₀ μ)
have 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 : μ)
Tactic: simp only [DFunLike.ext_iff] at hfg ⊢
Cleared hypotheses: hfg
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Finsupp (goal)
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 : ι
⊢ Eq.{u_2 + 1} (α := μ) ((f : (a : ι) → μ) x : μ) ((g : (a : ι) → μ) x : μ)
have 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 : μ)
Tactic: obtain rfl | hx := eq_or_ne x a
Cleared hypotheses: a, h, hfg
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Finsupp (goal)
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 : μ)
⊢ Eq.{u_2 + 1} (α := μ) ((f : (a : ι) → μ) x : μ) ((g : (a : ι) → μ) x : μ)
have inr : ∀ (hx : x ≠ a), Eq.{u_2 + 1} (α := μ) ((f : (a : ι) → μ) x : μ) ((g : (a : ι) → μ) x : μ)
Tactic: obtain rfl | hx := eq_or_ne x a
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Finsupp (hypothesis)
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 : μ)
⊢ Eq.{u_2 + 1} (α := μ) ((f : (a : ι) → μ) x : μ) ((g : (a : ι) → μ) x : μ)
have hf₁ : x ∉ f.support
Tactic: replace hf := mt (hf.2 ·) h
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Finsupp (hypothesis)
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
⊢ Eq.{u_2 + 1} (α := μ) ((f : (a : ι) → μ) x : μ) ((g : (a : ι) → μ) x : μ)
have hg₁ : x ∉ g.support
Tactic: replace hg := mt (hg.2 ·) h
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Finsupp (goal)
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
⊢ Eq.{u_2 + 1} (α := μ) ((f : (a : ι) → μ) x : μ) ((g : (a : ι) → μ) x : μ)
have inl : Eq.{u_2 + 1} (α := μ) (0 : μ) ((g : (a : ι) → μ) x : μ)
Tactic: rw [notMem_support_iff.mp hf, notMem_support_iff.mp hg]
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Finsupp (goal)
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 : μ)
⊢ Eq.{u_2 + 1} (α := μ) ((f : (a : ι) → μ) x : μ) ((g : (a : ι) → μ) x : μ)
have inl₁ : Eq.{u_2 + 1} (α := μ) 0 0
Tactic: rw [notMem_support_iff.mp hf, notMem_support_iff.mp hg]
-- 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 : μ
⊢ Eq (α := Finset (ι →₀ μ)) ((insert a s).finsuppAntidiag n)
    ((@antidiagonal _ AddCommMonoid.toAddMonoid _ n).biUnion fun (p : μ × μ) ↦
      map (α := ↥(s.finsuppAntidiag p.2))
        { toFun := fun (f : ↥(s.finsuppAntidiag p.2)) ↦ (↑f : ι →₀ μ).update a p.1, inj' := ⋯ }
        (attach (s.finsuppAntidiag p.2)))
have h₁ : ∀ (f : ι →₀ μ),
  Membership.mem (γ := Finset (ι →₀ μ)) ((insert a s).finsuppAntidiag n) f ↔
    Membership.mem (γ := Finset (ι →₀ μ))
      ((@antidiagonal _ AddCommMonoid.toAddMonoid _ n).biUnion fun (p : μ × μ) ↦
        map (α := ↥(s.finsuppAntidiag p.2))
          { toFun := fun (f : ↥(s.finsuppAntidiag p.2)) ↦ (↑f : ι →₀ μ).update a p.1, inj' := sorry }
          (attach (s.finsuppAntidiag p.2)))
      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 μ
a : ι
s : Finset ι
h : a ∉ s
n : μ
f : ι →₀ μ
⊢ Membership.mem (γ := Finset (ι →₀ μ)) ((insert a s).finsuppAntidiag n) f ↔
    Membership.mem (γ := Finset (ι →₀ μ))
      ((@antidiagonal _ AddCommMonoid.toAddMonoid _ n).biUnion fun (p : μ × μ) ↦
        map (α := ↥(s.finsuppAntidiag p.2))
          { toFun := fun (f : ↥(s.finsuppAntidiag p.2)) ↦ (↑f : ι →₀ μ).update a p.1, inj' := ⋯ }
          (attach (s.finsuppAntidiag p.2)))
      f
have h₁ : (∃ m ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n,
    ∃ (g : ι →₀ μ), f = g.update a m.1 ∧ Membership.mem (γ := Finset (ι →₀ μ)) (s.finsuppAntidiag m.2) g) ↔
  ∃ a_1 ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n,
    Membership.mem (γ := Finset (ι →₀ μ))
      (map (α := ↥(s.finsuppAntidiag a_1.2))
        { toFun := fun (f : ↥(s.finsuppAntidiag a_1.2)) ↦ (↑f : ι →₀ μ).update a a_1.1, inj' := sorry }
        (attach (s.finsuppAntidiag a_1.2)))
      f
Tactic: rw [mem_finsuppAntidiag_insert h, mem_biUnion]
-- 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 : ι →₀ μ
⊢ (∃ m ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n,
      ∃ (g : ι →₀ μ), f = g.update a m.1 ∧ Membership.mem (γ := Finset (ι →₀ μ)) (s.finsuppAntidiag m.2) g) ↔
    ∃ a_1 ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n,
      Membership.mem (γ := Finset (ι →₀ μ))
        (map (α := ↥(s.finsuppAntidiag a_1.2))
          { toFun := fun (f : ↥(s.finsuppAntidiag a_1.2)) ↦ (↑f : ι →₀ μ).update a a_1.1, inj' := ⋯ }
          (attach (s.finsuppAntidiag a_1.2)))
        f
have h₁ : (∃ m ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n,
    ∃ (g : ι →₀ μ), f = g.update a m.1 ∧ Membership.mem (γ := Finset (ι →₀ μ)) (s.finsuppAntidiag m.2) g) ↔
  ∃ a_1 ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n,
    ∃ (a_2 : ↥(s.finsuppAntidiag a_1.2)),
      Membership.mem (γ := Finset ↥(s.finsuppAntidiag a_1.2)) (attach (s.finsuppAntidiag a_1.2)) a_2 ∧
        ({ toFun := fun (f : ↥(s.finsuppAntidiag a_1.2)) ↦ (↑f : ι →₀ μ).update a a_1.1, inj' := sorry } :
              (a : ↥(s.finsuppAntidiag a_1.2)) → ι →₀ μ)
            a_2 =
          f
Tactic: simp_rw [mem_map, mem_attach, true_and, Subtype.exists, Embedding.coeFn_mk, exists_prop, and_comm,
    eq_comm]
-- 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 : ι →₀ μ
h₁ :
  (∃ m ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n,
      ∃ (g : ι →₀ μ), f = g.update a m.1 ∧ Membership.mem (γ := Finset (ι →₀ μ)) (s.finsuppAntidiag m.2) g) ↔
    ∃ a_1 ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n,
      ∃ (a_2 : ↥(s.finsuppAntidiag a_1.2)),
        Membership.mem (γ := Finset ↥(s.finsuppAntidiag a_1.2)) (attach (s.finsuppAntidiag a_1.2)) a_2 ∧
          ({ toFun := fun (f : ↥(s.finsuppAntidiag a_1.2)) ↦ (↑f : ι →₀ μ).update a a_1.1, inj' := ⋯ } :
                (a : ↥(s.finsuppAntidiag a_1.2)) → ι →₀ μ)
              a_2 =
            f
⊢ (∃ m ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n,
      ∃ (g : ι →₀ μ), f = g.update a m.1 ∧ Membership.mem (γ := Finset (ι →₀ μ)) (s.finsuppAntidiag m.2) g) ↔
    ∃ a_1 ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n,
      Membership.mem (γ := Finset (ι →₀ μ))
        (map (α := ↥(s.finsuppAntidiag a_1.2))
          { toFun := fun (f : ↥(s.finsuppAntidiag a_1.2)) ↦ (↑f : ι →₀ μ).update a a_1.1, inj' := ⋯ }
          (attach (s.finsuppAntidiag a_1.2)))
        f
have h₂ : (∃ m ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n,
    ∃ (g : ι →₀ μ), f = g.update a m.1 ∧ Membership.mem (γ := Finset (ι →₀ μ)) (s.finsuppAntidiag m.2) g) ↔
  ∃ a_1 ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n,
    ∃ (a_2 : ↥(s.finsuppAntidiag a_1.2)),
      True ∧
        ({ toFun := fun (f : ↥(s.finsuppAntidiag a_1.2)) ↦ (↑f : ι →₀ μ).update a a_1.1, inj' := sorry } :
              (a : ↥(s.finsuppAntidiag a_1.2)) → ι →₀ μ)
            a_2 =
          f
Tactic: simp_rw [mem_map, mem_attach, true_and, Subtype.exists, Embedding.coeFn_mk, exists_prop, and_comm,
    eq_comm]
-- 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 : ι →₀ μ
h₁ :
  (∃ m ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n,
      ∃ (g : ι →₀ μ), f = g.update a m.1 ∧ Membership.mem (γ := Finset (ι →₀ μ)) (s.finsuppAntidiag m.2) g) ↔
    ∃ a_1 ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n,
      ∃ (a_2 : ↥(s.finsuppAntidiag a_1.2)),
        Membership.mem (γ := Finset ↥(s.finsuppAntidiag a_1.2)) (attach (s.finsuppAntidiag a_1.2)) a_2 ∧
          ({ toFun := fun (f : ↥(s.finsuppAntidiag a_1.2)) ↦ (↑f : ι →₀ μ).update a a_1.1, inj' := ⋯ } :
                (a : ↥(s.finsuppAntidiag a_1.2)) → ι →₀ μ)
              a_2 =
            f
h₂ :
  (∃ m ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n,
      ∃ (g : ι →₀ μ), f = g.update a m.1 ∧ Membership.mem (γ := Finset (ι →₀ μ)) (s.finsuppAntidiag m.2) g) ↔
    ∃ a_1 ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n,
      ∃ (a_2 : ↥(s.finsuppAntidiag a_1.2)),
        True ∧
          ({ toFun := fun (f : ↥(s.finsuppAntidiag a_1.2)) ↦ (↑f : ι →₀ μ).update a a_1.1, inj' := ⋯ } :
                (a : ↥(s.finsuppAntidiag a_1.2)) → ι →₀ μ)
              a_2 =
            f
⊢ (∃ m ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n,
      ∃ (g : ι →₀ μ), f = g.update a m.1 ∧ Membership.mem (γ := Finset (ι →₀ μ)) (s.finsuppAntidiag m.2) g) ↔
    ∃ a_1 ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n,
      Membership.mem (γ := Finset (ι →₀ μ))
        (map (α := ↥(s.finsuppAntidiag a_1.2))
          { toFun := fun (f : ↥(s.finsuppAntidiag a_1.2)) ↦ (↑f : ι →₀ μ).update a a_1.1, inj' := ⋯ }
          (attach (s.finsuppAntidiag a_1.2)))
        f
have h₃ : (∃ m ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n,
    ∃ (g : ι →₀ μ), f = g.update a m.1 ∧ Membership.mem (γ := Finset (ι →₀ μ)) (s.finsuppAntidiag m.2) g) ↔
  ∃ a_1 ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n,
    ∃ (a_2 : ↥(s.finsuppAntidiag a_1.2)),
      ({ toFun := fun (f : ↥(s.finsuppAntidiag a_1.2)) ↦ (↑f : ι →₀ μ).update a a_1.1, inj' := sorry } :
            (a : ↥(s.finsuppAntidiag a_1.2)) → ι →₀ μ)
          a_2 =
        f
Tactic: simp_rw [mem_map, mem_attach, true_and, Subtype.exists, Embedding.coeFn_mk, exists_prop, and_comm,
    eq_comm]
-- 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 : ι →₀ μ
h₁ :
  (∃ m ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n,
      ∃ (g : ι →₀ μ), f = g.update a m.1 ∧ Membership.mem (γ := Finset (ι →₀ μ)) (s.finsuppAntidiag m.2) g) ↔
    ∃ a_1 ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n,
      ∃ (a_2 : ↥(s.finsuppAntidiag a_1.2)),
        Membership.mem (γ := Finset ↥(s.finsuppAntidiag a_1.2)) (attach (s.finsuppAntidiag a_1.2)) a_2 ∧
          ({ toFun := fun (f : ↥(s.finsuppAntidiag a_1.2)) ↦ (↑f : ι →₀ μ).update a a_1.1, inj' := ⋯ } :
                (a : ↥(s.finsuppAntidiag a_1.2)) → ι →₀ μ)
              a_2 =
            f
h₂ :
  (∃ m ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n,
      ∃ (g : ι →₀ μ), f = g.update a m.1 ∧ Membership.mem (γ := Finset (ι →₀ μ)) (s.finsuppAntidiag m.2) g) ↔
    ∃ a_1 ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n,
      ∃ (a_2 : ↥(s.finsuppAntidiag a_1.2)),
        True ∧
          ({ toFun := fun (f : ↥(s.finsuppAntidiag a_1.2)) ↦ (↑f : ι →₀ μ).update a a_1.1, inj' := ⋯ } :
                (a : ↥(s.finsuppAntidiag a_1.2)) → ι →₀ μ)
              a_2 =
            f
h₃ :
  (∃ m ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n,
      ∃ (g : ι →₀ μ), f = g.update a m.1 ∧ Membership.mem (γ := Finset (ι →₀ μ)) (s.finsuppAntidiag m.2) g) ↔
    ∃ a_1 ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n,
      ∃ (a_2 : ↥(s.finsuppAntidiag a_1.2)),
        ({ toFun := fun (f : ↥(s.finsuppAntidiag a_1.2)) ↦ (↑f : ι →₀ μ).update a a_1.1, inj' := ⋯ } :
              (a : ↥(s.finsuppAntidiag a_1.2)) → ι →₀ μ)
            a_2 =
          f
⊢ (∃ m ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n,
      ∃ (g : ι →₀ μ), f = g.update a m.1 ∧ Membership.mem (γ := Finset (ι →₀ μ)) (s.finsuppAntidiag m.2) g) ↔
    ∃ a_1 ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n,
      Membership.mem (γ := Finset (ι →₀ μ))
        (map (α := ↥(s.finsuppAntidiag a_1.2))
          { toFun := fun (f : ↥(s.finsuppAntidiag a_1.2)) ↦ (↑f : ι →₀ μ).update a a_1.1, inj' := ⋯ }
          (attach (s.finsuppAntidiag a_1.2)))
        f
have h₄ : (∃ m ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n,
    ∃ (g : ι →₀ μ), f = g.update a m.1 ∧ Membership.mem (γ := Finset (ι →₀ μ)) (s.finsuppAntidiag m.2) g) ↔
  ∃ a_1 ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n,
    ∃ (a_2 : ι →₀ μ) (b : Membership.mem (γ := Finset (ι →₀ μ)) (s.finsuppAntidiag a_1.2) a_2),
      ({ toFun := fun (f : ↥(s.finsuppAntidiag a_1.2)) ↦ (↑f : ι →₀ μ).update a a_1.1, inj' := sorry } :
            (a : ↥(s.finsuppAntidiag a_1.2)) → ι →₀ μ)
          (Subtype.mk (p := fun (a : ι →₀ μ) ↦ Membership.mem (γ := Finset (ι →₀ μ)) (s.finsuppAntidiag a_1.2) a) a_2
            b) =
        f
Tactic: simp_rw [mem_map, mem_attach, true_and, Subtype.exists, Embedding.coeFn_mk, exists_prop, and_comm,
    eq_comm]
-- 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 t : Finset ι
h : s ⊆ t
n : μ
a : ι →₀ μ
⊢ Membership.mem (γ := Finset (ι →₀ μ)) (s.finsuppAntidiag n) a →
    Membership.mem (γ := Finset (ι →₀ μ)) (t.finsuppAntidiag n) a
have simp_rw : (a.sum fun (x : ι) (x_1 : μ) ↦ x_1) = n ∧ a.support ⊆ s → (a.sum fun (x : ι) (x_1 : μ) ↦ x_1) = n ∧ a.support ⊆ t
Tactic: simp_rw [mem_finsuppAntidiag']
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Finsupp (goal)
Goal:
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
inst_4 : AddCommMonoid μ'
inst_5 : HasAntidiagonal μ'
inst_6 : DecidableEq μ'
e : μ ≃+ μ'
s : Finset ι
n : μ
f : ι →₀ μ'
⊢ f ∈ map (Equiv.toEmbedding (AddEquiv.toEquiv (mapRange.addEquiv e))) (s.finsuppAntidiag n) →
    Membership.mem (γ := Finset (ι →₀ μ')) (s.finsuppAntidiag ((e : (a : μ) → μ') n) : Finset (ι →₀ μ')) f
have simp : (∃ (a : ι →₀ μ),
    ((a.sum fun (x : ι) (x_1 : μ) ↦ x_1) = n ∧ a.support ⊆ s) ∧
      (Equiv.toEmbedding (AddEquiv.toEquiv (mapRange.addEquiv e)) : (a : ι →₀ μ) → ι →₀ μ') a = f) →
  Eq (α := μ') (f.sum fun (x : ι) (x_1 : μ') ↦ x_1 : μ') ((e : (a : μ) → μ') n : μ') ∧ f.support ⊆ s
Tactic: simp only [mem_map, mem_finsuppAntidiag']
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Finsupp (goal)
Goal:
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
inst_4 : AddCommMonoid μ'
inst_5 : HasAntidiagonal μ'
inst_6 : DecidableEq μ'
e : μ ≃+ μ'
s : Finset ι
n : μ
g : ι →₀ μ
hsum : (g.sum fun (x : ι) (x_1 : μ) ↦ x_1) = n
hsupp : g.support ⊆ s
⊢ Eq.{u_3 + 1} (α := μ')
      (sum ((Equiv.toEmbedding (AddEquiv.toEquiv (mapRange.addEquiv e)) : (a : ι →₀ μ) → ι →₀ μ') g)
          fun (x : ι) (x_1 : μ') ↦ x_1 :
        μ')
      ((e : (a : μ) → μ') n : μ') ∧
    Finsupp.support.{u_1, u_3} (M := μ')
        ((Equiv.toEmbedding (AddEquiv.toEquiv (mapRange.addEquiv e)) : (a : ι →₀ μ) → ι →₀ μ') g) ⊆
      s
have simp : Eq.{u_3 + 1} (α := μ') (sum (M := μ') (mapRange (⇑e : (a : μ) → μ') sorry g : ι →₀ μ') fun (x : ι) (x_1 : μ') ↦ x_1 : μ')
    ((e : (a : μ) → μ') n : μ') ∧
  Finsupp.support.{u_1, u_3} (M := μ') (mapRange (⇑e : (a : μ) → μ') sorry g : ι →₀ μ') ⊆ s
Tactic: simp only [AddEquiv.toEquiv_eq_coe, mapRange.addEquiv_toEquiv, Equiv.coe_toEmbedding,
    mapRange.equiv_apply, EquivLike.coe_coe]
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Finsupp (goal)
Goal:
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
inst_4 : AddCommMonoid μ'
inst_5 : HasAntidiagonal μ'
inst_6 : DecidableEq μ'
e : μ ≃+ μ'
s : Finset ι
n : μ
g : ι →₀ μ
hsum : (g.sum fun (x : ι) (x_1 : μ) ↦ x_1) = n
hsupp : g.support ⊆ s
⊢ Eq.{u_3 + 1} (α := μ') (sum (M := μ') (mapRange (⇑e : (a : μ) → μ') ⋯ g : ι →₀ μ') fun (x : ι) (x_1 : μ') ↦ x_1 : μ')
      ((e : (a : μ) → μ') n : μ') ∧
    Finsupp.support.{u_1, u_3} (M := μ') (mapRange (⇑e : (a : μ) → μ') ⋯ g : ι →₀ μ') ⊆ s
have left : Eq.{u_3 + 1} (α := μ') (sum (M := μ') (mapRange (⇑e : (a : μ) → μ') sorry g : ι →₀ μ') fun (x : ι) (x_1 : μ') ↦ x_1 : μ')
  ((e : (a : μ) → μ') n : μ')
Tactic: constructor