awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Antidiag.Pi
Goal:
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
n_1 : μ
d_1 : ℕ
n : μ
d : ℕ
i : μ × μ
_hi : i ∈ (↑(@antidiagonal _ AddCommMonoid.toAddMonoid _ n) : Set (μ × μ))
j : μ × μ
_hj : j ∈ (↑(@antidiagonal _ AddCommMonoid.toAddMonoid _ n) : Set (μ × μ))
hij : i ≠ j
ai : (i : Fin d) → μ
hai : Membership.mem (γ := Finset ((i : Fin d) → μ)) (↑(aux d i.2) : Finset (Fin d → μ)) ai
aj : (i : Fin d) → μ
haj : Membership.mem (γ := Finset ((i : Fin d) → μ)) (↑(aux d j.2) : Finset (Fin d → μ)) aj
hij' : i.1 = j.1 ∧ ai = aj
⊢ i.1 = j.1

Tactic:
exact hij'.1

Premises used: And.left
-- Module: Mathlib.Algebra.Order.Antidiag.Pi
Goal:
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
n_1 : μ
d_1 : ℕ
n : μ
d : ℕ
i : μ × μ
_hi : i ∈ (↑(@antidiagonal _ AddCommMonoid.toAddMonoid _ n) : Set (μ × μ))
j : μ × μ
_hj : j ∈ (↑(@antidiagonal _ AddCommMonoid.toAddMonoid _ n) : Set (μ × μ))
hij : i ≠ j
ai : (i : Fin d) → μ
hai : Membership.mem (γ := Finset ((i : Fin d) → μ)) (↑(aux d i.2) : Finset (Fin d → μ)) ai
aj : (i : Fin d) → μ
haj : Membership.mem (γ := Finset ((i : Fin d) → μ)) (↑(aux d j.2) : Finset (Fin d → μ)) aj
hij' : i.1 = j.1 ∧ ai = aj
⊢ Membership.mem (γ := Finset ((i : Fin d) → μ)) (↑(aux d j.2) : Finset (Fin d → μ)) ai

Tactic:
obtain ⟨-, rfl⟩ := hij'

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Antidiag.Pi
Goal:
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
n_1 : μ
d_1 : ℕ
n : μ
d : ℕ
i : μ × μ
_hi : i ∈ (↑(@antidiagonal _ AddCommMonoid.toAddMonoid _ n) : Set (μ × μ))
j : μ × μ
_hj : j ∈ (↑(@antidiagonal _ AddCommMonoid.toAddMonoid _ n) : Set (μ × μ))
hij : i ≠ j
ai : (i : Fin d) → μ
hai : Membership.mem (γ := Finset ((i : Fin d) → μ)) (↑(aux d i.2) : Finset (Fin d → μ)) ai
haj : Membership.mem (γ := Finset ((i : Fin d) → μ)) (↑(aux d j.2) : Finset (Fin d → μ)) ai
snd : ∑ i : Fin d, ai i = j.2
snd₁ snd₂ : Eq.{u_2 + 1} (α := μ) (∑ i : Fin d, ai i) (∑ i : Fin d, ai i)
⊢ i.2 = j.2

Tactic:
rw [← (aux d i.2).prop ai |>.mp hai, ← (aux d j.2).prop ai |>.mp haj]

Premises used: Subtype.prop, Iff.mp, Prod.snd
-- Module: Mathlib.Algebra.Order.Antidiag.Pi
Goal:
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
n_1 : μ
d_1 : ℕ
n : μ
d : ℕ
f : Fin (d + 1) → μ
simp_rw :
  (∃ (a : μ) (b : μ),
      a + b = n ∧
        ∃ (a_1 : (i : Fin d) → μ), ∑ i : Fin d, a_1 i = b ∧ Fin.cons (α := fun (a : Fin (d + 1)) ↦ μ) a a_1 = f) ↔
    f 0 + ∑ i : Fin d, f i.succ = n
⊢ Membership.mem (γ := Finset (Fin (d + 1) → μ))
      ((@antidiagonal _ AddCommMonoid.toAddMonoid _ n).disjiUnion
        (fun (ab : μ × μ) ↦
          map
            { toFun := Fin.cons (α := fun (a : Fin (d + 1)) ↦ μ) ab.1, inj' := ⋯ : ((i : Fin d) → μ) ↪ Fin (d + 1) → μ }
            (↑(aux d ab.2) : Finset (Fin d → μ)))
        ⋯)
      f ↔
    ∑ i : Fin (d + 1), f i = n

Tactic:
simp_rw [mem_disjiUnion, mem_antidiagonal, mem_map, Embedding.coeFn_mk, Prod.exists,
          (aux d _).prop, Fin.sum_univ_succ]

Premises used: Finset.mem_disjiUnion, Finset.HasAntidiagonal.mem_antidiagonal, Subtype.prop, Function.Embedding.coeFn_mk, Finset.mem_map, Prod.exists, Fin.sum_univ_succ
-- Module: Mathlib.Algebra.Order.Antidiag.Pi
Goal:
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
n_1 : μ
d_1 : ℕ
n : μ
d : ℕ
f : Fin (d + 1) → μ
mp :
  (∃ (a : μ) (b : μ),
      a + b = n ∧
        ∃ (a_1 : (i : Fin d) → μ), ∑ i : Fin d, a_1 i = b ∧ Fin.cons (α := fun (a : Fin (d + 1)) ↦ μ) a a_1 = f) →
    f 0 + ∑ i : Fin d, f i.succ = n
mpr :
  f 0 + ∑ i : Fin d, f i.succ = n →
    ∃ (a : μ) (b : μ),
      a + b = n ∧
        ∃ (a_1 : (i : Fin d) → μ), ∑ i : Fin d, a_1 i = b ∧ Fin.cons (α := fun (a : Fin (d + 1)) ↦ μ) a a_1 = f
⊢ (∃ (a : μ) (b : μ),
      a + b = n ∧
        ∃ (a_1 : (i : Fin d) → μ), ∑ i : Fin d, a_1 i = b ∧ Fin.cons (α := fun (a : Fin (d + 1)) ↦ μ) a a_1 = f) ↔
    f 0 + ∑ i : Fin d, f i.succ = n

Tactic:
constructor
-- Module: Mathlib.Algebra.Order.Antidiag.Pi
Goal:
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
n : μ
d_1 d : ℕ
a : μ
g : (i : Fin d) → μ
⊢ HAdd.hAdd (α := μ) (β := μ) (Fin.cons (α := fun (a : Fin (d + 1)) ↦ μ) a g 0 : μ)
      (∑ i : Fin d, Fin.cons (α := fun (a : Fin (d + 1)) ↦ μ) a g i.succ : μ) =
    a + ∑ i : Fin d, g i

Tactic:
simp only [Fin.cons_zero, Fin.cons_succ]

Premises used: Fin.cons_succ, Fin.cons_zero
-- Module: Mathlib.Algebra.Order.Antidiag.Pi
Goal:
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
n_1 : μ
d_1 : ℕ
n : μ
d : ℕ
f : Fin (d + 1) → μ
hf : f 0 + ∑ i : Fin d, f i.succ = n
⊢ ∃ (a : μ) (b : μ),
    a + b = n ∧ ∃ (a_1 : (i : Fin d) → μ), ∑ i : Fin d, a_1 i = b ∧ Fin.cons (α := fun (a : Fin (d + 1)) ↦ μ) a a_1 = f

Tactic:
⟨_, _, hf, _, rfl, Fin.cons_self_tail f⟩

Premises used: Fin.cons_self_tail, And.intro, Exists.intro, rfl
-- Module: Mathlib.Algebra.Order.Antidiag.Pi
Goal:
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
n_1 : μ
d_1 : ℕ
n : μ
d : ℕ
f : Fin (d + 1) → μ
hf : f 0 + ∑ i : Fin d, f i.succ = n
⊢ ∃ (a : μ) (b : μ),
    a + b = n ∧ ∃ (a_1 : (i : Fin d) → μ), ∑ i : Fin d, a_1 i = b ∧ Fin.cons (α := fun (a : Fin (d + 1)) ↦ μ) a a_1 = f

Tactic:
exact ⟨_, _, hf, _, rfl, Fin.cons_self_tail f⟩
-- Module: Mathlib.Algebra.Order.Antidiag.Pi
Goal:
μ : Type u_2
inst : AddCommMonoid μ
inst_1 : HasAntidiagonal μ
inst_2 : DecidableEq μ
n : μ
d : ℕ
f : Fin d → μ
⊢ f ∈ finAntidiagonal d n ↔ ∑ i : Fin d, f i = n

Tactic:
(finAntidiagonal.aux d n).prop f

Premises used: Set.Mem, setOf, Subtype.prop, Finset.finAntidiagonal.aux
-- Module: Mathlib.Algebra.Order.Antidiag.Pi
Goal:
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
n_1 : μ
s : Finset ι
n : μ
refine_1 :
  ∀ (e : ↥s ≃ Fin #s),
    Injective (β := ι → μ) fun (f : Fin #s → μ) (i : ι) ↦
      if hi : i ∈ s then f ((e : (a : ↥s) → Fin #s) (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi)) else 0
refine_2 :
  ∀ (e₁ e₂ : ↥s ≃ Fin #s),
    Eq (α := Finset (ι → μ))
      ((fun (e : ↥s ≃ Fin #s) ↦
          (map (α := Fin #s → μ)
              {
                toFun := fun (f : Fin #s → μ) (i : ι) ↦
                  if hi : i ∈ s then f ((e : (a : ↥s) → Fin #s) (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi)) else 0,
                inj' := ⋯ }
              (finAntidiagonal (#s) n) :
            Finset (ι → μ)))
        e₁)
      ((fun (e : ↥s ≃ Fin #s) ↦
          (map (α := Fin #s → μ)
              {
                toFun := fun (f : Fin #s → μ) (i : ι) ↦
                  if hi : i ∈ s then f ((e : (a : ↥s) → Fin #s) (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi)) else 0,
                inj' := ⋯ }
              (finAntidiagonal (#s) n) :
            Finset (ι → μ)))
        e₂)
⊢ Finset (ι → μ)

Tactic:
refine (Fintype.truncEquivFinOfCardEq <| Fintype.card_coe s).lift
    (fun e ↦ (finAntidiagonal s.card n).map ⟨fun f i ↦ if hi : i ∈ s then f (e ⟨i, hi⟩) else 0, ?_⟩)
    fun e₁ e₂ ↦ ?_

Premises used: Finset.map, Finset.finAntidiagonal, Function.Embedding.mk, Finset.card, Fintype.truncEquivFinOfCardEq, Fintype.card_coe, Trunc.lift
-- Module: Mathlib.Algebra.Order.Antidiag.Pi
Goal:
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
n_1 : μ
s : Finset ι
n : μ
e : ↥s ≃ Fin #s
f g : Fin #s → μ
hfg :
  Eq (α := ι → μ)
    ((fun (f : Fin #s → μ) (i : ι) ↦
        (if hi : i ∈ s then f ((e : (a : ↥s) → Fin #s) (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi)) else 0 : μ))
      f)
    ((fun (f : Fin #s → μ) (i : ι) ↦
        (if hi : i ∈ s then f ((e : (a : ↥s) → Fin #s) (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi)) else 0 : μ))
      g)
refine_1 : ∀ (i : Fin #s), f i = g i
⊢ f = g

Tactic:
ext i
-- Module: Mathlib.Algebra.Order.Antidiag.Pi
Goal:
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
n_1 : μ
s : Finset ι
n : μ
e : ↥s ≃ Fin #s
f g : Fin #s → μ
hfg :
  Eq (α := ι → μ)
    ((fun (f : Fin #s → μ) (i : ι) ↦
        (if hi : i ∈ s then f ((e : (a : ↥s) → Fin #s) (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi)) else 0 : μ))
      f)
    ((fun (f : Fin #s → μ) (i : ι) ↦
        (if hi : i ∈ s then f ((e : (a : ↥s) → Fin #s) (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi)) else 0 : μ))
      g)
i : Fin #s
⊢ f i = g i

Tactic:
simpa using congr_fun hfg (e.symm i)

Premises used: congr_fun, Equiv.symm, Subtype.val, DFunLike.coe
-- Module: Mathlib.Algebra.Order.Antidiag.Pi
Goal:
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
n_1 : μ
s : Finset ι
n : μ
e₁ e₂ : ↥s ≃ Fin #s
refine_2 :
  ∀ (f : ι → μ),
    Membership.mem (γ := Finset (ι → μ))
        ((fun (e : ↥s ≃ Fin #s) ↦
            (map (α := Fin #s → μ)
                {
                  toFun := fun (f : Fin #s → μ) (i : ι) ↦
                    if hi : i ∈ s then f ((e : (a : ↥s) → Fin #s) (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi)) else 0,
                  inj' := ⋯ }
                (finAntidiagonal (#s) n) :
              Finset (ι → μ)))
          e₁)
        f ↔
      Membership.mem (γ := Finset (ι → μ))
        ((fun (e : ↥s ≃ Fin #s) ↦
            (map (α := Fin #s → μ)
                {
                  toFun := fun (f : Fin #s → μ) (i : ι) ↦
                    if hi : i ∈ s then f ((e : (a : ↥s) → Fin #s) (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi)) else 0,
                  inj' := ⋯ }
                (finAntidiagonal (#s) n) :
              Finset (ι → μ)))
          e₂)
        f
⊢ Eq (α := Finset (ι → μ))
    ((fun (e : ↥s ≃ Fin #s) ↦
        (map (α := Fin #s → μ)
            {
              toFun := fun (f : Fin #s → μ) (i : ι) ↦
                if hi : i ∈ s then f ((e : (a : ↥s) → Fin #s) (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi)) else 0,
              inj' := ⋯ }
            (finAntidiagonal (#s) n) :
          Finset (ι → μ)))
      e₁)
    ((fun (e : ↥s ≃ Fin #s) ↦
        (map (α := Fin #s → μ)
            {
              toFun := fun (f : Fin #s → μ) (i : ι) ↦
                if hi : i ∈ s then f ((e : (a : ↥s) → Fin #s) (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi)) else 0,
              inj' := ⋯ }
            (finAntidiagonal (#s) n) :
          Finset (ι → μ)))
      e₂)

Tactic:
ext f
-- Module: Mathlib.Algebra.Order.Antidiag.Pi
Goal:
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
n_1 : μ
s : Finset ι
n : μ
e₁ e₂ : ↥s ≃ Fin #s
f : ι → μ
refine_2 :
  (∃ (a : Fin #s → μ),
      ∑ i : Fin #s, a i = n ∧
        ({
                toFun := fun (f : Fin #s → μ) (i : ι) ↦
                  if hi : i ∈ s then f ((e₁ : (a : ↥s) → Fin #s) (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi)) else 0,
                inj' := ⋯ } :
              (a : Fin #s → μ) → ι → μ)
            a =
          f) ↔
    ∃ (a : Fin #s → μ),
      ∑ i : Fin #s, a i = n ∧
        ({
                toFun := fun (f : Fin #s → μ) (i : ι) ↦
                  if hi : i ∈ s then f ((e₂ : (a : ↥s) → Fin #s) (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi)) else 0,
                inj' := ⋯ } :
              (a : Fin #s → μ) → ι → μ)
            a =
          f
⊢ Membership.mem (γ := Finset (ι → μ))
      ((fun (e : ↥s ≃ Fin #s) ↦
          (map (α := Fin #s → μ)
              {
                toFun := fun (f : Fin #s → μ) (i : ι) ↦
                  if hi : i ∈ s then f ((e : (a : ↥s) → Fin #s) (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi)) else 0,
                inj' := ⋯ }
              (finAntidiagonal (#s) n) :
            Finset (ι → μ)))
        e₁)
      f ↔
    Membership.mem (γ := Finset (ι → μ))
      ((fun (e : ↥s ≃ Fin #s) ↦
          (map (α := Fin #s → μ)
              {
                toFun := fun (f : Fin #s → μ) (i : ι) ↦
                  if hi : i ∈ s then f ((e : (a : ↥s) → Fin #s) (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi)) else 0,
                inj' := ⋯ }
              (finAntidiagonal (#s) n) :
            Finset (ι → μ)))
        e₂)
      f

Tactic:
simp only [mem_map, mem_finAntidiagonal]

Premises used: Finset.mem_map, Finset.mem_finAntidiagonal
-- Module: Mathlib.Algebra.Order.Antidiag.Pi
Goal:
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
n_1 : μ
s : Finset ι
n : μ
e₁ e₂ : ↥s ≃ Fin #s
f : ι → μ
⊢ (∃ (a : Fin #s → μ),
      ∑ i : Fin #s, a i = n ∧
        ({
                toFun := fun (f : Fin #s → μ) (i : ι) ↦
                  if hi : i ∈ s then f ((e₁ : (a : ↥s) → Fin #s) (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi)) else 0,
                inj' := ⋯ } :
              (a : Fin #s → μ) → ι → μ)
            a =
          f) ↔
    ∃ (a : Fin #s → μ),
      ∑ i : Fin #s, a i = n ∧
        ({
                toFun := fun (f : Fin #s → μ) (i : ι) ↦
                  if hi : i ∈ s then f ((e₂ : (a : ↥s) → Fin #s) (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi)) else 0,
                inj' := ⋯ } :
              (a : Fin #s → μ) → ι → μ)
            a =
          f

Tactic:
Equiv.exists_congr ((e₁.symm.trans e₂).arrowCongr <| .refl _) fun g ↦ ?_

Premises used: Equiv.trans, Equiv.arrowCongr, Equiv.symm, Equiv.refl, Equiv.exists_congr
-- Module: Mathlib.Algebra.Order.Antidiag.Pi
Goal:
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
n_1 : μ
s : Finset ι
n : μ
e₁ e₂ : ↥s ≃ Fin #s
f : ι → μ
refine_2 :
  ∀ (g : Fin #s → μ),
    ∑ i : Fin #s, g i = n ∧
        ({
                toFun := fun (f : Fin #s → μ) (i : ι) ↦
                  if hi : i ∈ s then f ((e₁ : (a : ↥s) → Fin #s) (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi)) else 0,
                inj' := ⋯ } :
              (a : Fin #s → μ) → ι → μ)
            g =
          f ↔
      ∑ i : Fin #s, ((e₁.symm.trans e₂).arrowCongr (Equiv.refl μ) : (a : Fin #s → μ) → Fin #s → μ) g i = n ∧
        ({
                toFun := fun (f : Fin #s → μ) (i : ι) ↦
                  if hi : i ∈ s then f ((e₂ : (a : ↥s) → Fin #s) (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi)) else 0,
                inj' := ⋯ } :
              (a : Fin #s → μ) → ι → μ)
            (((e₁.symm.trans e₂).arrowCongr (Equiv.refl μ) : (a : Fin #s → μ) → Fin #s → μ) g : Fin #s → μ) =
          f
⊢ (∃ (a : Fin #s → μ),
      ∑ i : Fin #s, a i = n ∧
        ({
                toFun := fun (f : Fin #s → μ) (i : ι) ↦
                  if hi : i ∈ s then f ((e₁ : (a : ↥s) → Fin #s) (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi)) else 0,
                inj' := ⋯ } :
              (a : Fin #s → μ) → ι → μ)
            a =
          f) ↔
    ∃ (a : Fin #s → μ),
      ∑ i : Fin #s, a i = n ∧
        ({
                toFun := fun (f : Fin #s → μ) (i : ι) ↦
                  if hi : i ∈ s then f ((e₂ : (a : ↥s) → Fin #s) (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi)) else 0,
                inj' := ⋯ } :
              (a : Fin #s → μ) → ι → μ)
            a =
          f

Tactic:
refine Equiv.exists_congr ((e₁.symm.trans e₂).arrowCongr <| .refl _) fun g ↦ ?_

Premises used: Equiv.trans, Equiv.arrowCongr, Equiv.symm, Equiv.refl, Equiv.exists_congr
-- Module: Mathlib.Algebra.Order.Antidiag.Pi
Goal:
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
n_1 : μ
s : Finset ι
n : μ
e₁ e₂ : ↥s ≃ Fin #s
f : ι → μ
g : Fin #s → μ
⊢ Eq.{u_2 + 1} (α := μ) (∑ x : Fin #s, g ((e₂.symm.trans e₁ : (a : Fin #s) → Fin #s) x)) (∑ x : Fin #s, g x)

Tactic:
have := Fintype.sum_equiv (e₂.symm.trans e₁) _ g fun _ ↦ rfl
-- Module: Mathlib.Algebra.Order.Antidiag.Pi
Goal:
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
n_1 : μ
s : Finset ι
n : μ
e₁ e₂ : ↥s ≃ Fin #s
f : ι → μ
g : Fin #s → μ
this : Eq.{u_2 + 1} (α := μ) (∑ x : Fin #s, g ((e₂.symm.trans e₁ : (a : Fin #s) → Fin #s) x)) (∑ x : Fin #s, g x)
⊢ ∑ i : Fin #s, g i = n ∧
      ({
              toFun := fun (f : Fin #s → μ) (i : ι) ↦
                if hi : i ∈ s then f ((e₁ : (a : ↥s) → Fin #s) (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi)) else 0,
              inj' := ⋯ } :
            (a : Fin #s → μ) → ι → μ)
          g =
        f ↔
    ∑ i : Fin #s, ((e₁.symm.trans e₂).arrowCongr (Equiv.refl μ) : (a : Fin #s → μ) → Fin #s → μ) g i = n ∧
      ({
              toFun := fun (f : Fin #s → μ) (i : ι) ↦
                if hi : i ∈ s then f ((e₂ : (a : ↥s) → Fin #s) (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi)) else 0,
              inj' := ⋯ } :
            (a : Fin #s → μ) → ι → μ)
          (((e₁.symm.trans e₂).arrowCongr (Equiv.refl μ) : (a : Fin #s → μ) → Fin #s → μ) g : Fin #s → μ) =
        f

Tactic:
simp_all
-- Module: Mathlib.Algebra.Order.Antidiag.Pi
Goal:
ι : Type u_1
μ : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
s : Finset ι
n : μ
f : ι → μ
a :
  ∀ (e : ↥s ≃ Fin #s),
    f ∈
        Trunc.lift
          (fun (e : ↥s ≃ Fin #s) ↦
            map
              {
                toFun := fun (f : Fin #s → μ) (i : ι) ↦
                  if hi : i ∈ s then f ((e : (a : ↥s) → Fin #s) (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi)) else 0,
                inj' := ⋯ : (Fin #s → μ) ↪ ι → μ }
              (finAntidiagonal (#s) n))
          ⋯ (Trunc.mk e) ↔
      s.sum f = n ∧ ∀ (i : ι), f i ≠ 0 → i ∈ s
⊢ f ∈
      Trunc.lift
        (fun (e : ↥s ≃ Fin #s) ↦
          map
            {
              toFun := fun (f : Fin #s → μ) (i : ι) ↦
                if hi : i ∈ s then f ((e : (a : ↥s) → Fin #s) (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi)) else 0,
              inj' := ⋯ : (Fin #s → μ) ↪ ι → μ }
            (finAntidiagonal (#s) n))
        ⋯ (Fintype.truncEquivFinOfCardEq ⋯) ↔
    s.sum f = n ∧ ∀ (i : ι), f i ≠ 0 → i ∈ s

Tactic:
induction Fintype.truncEquivFinOfCardEq (Fintype.card_coe s) using Trunc.ind with | _ e

Premises used: Trunc.ind, Fintype.truncEquivFinOfCardEq, Fintype.card_coe
-- Module: Mathlib.Algebra.Order.Antidiag.Pi
Goal:
ι : Type u_1
μ : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
s : Finset ι
n : μ
f : ι → μ
e : ↥s ≃ Fin #s
a :
  (∃ (a : Fin #s → μ),
      ∑ i : Fin #s, a i = n ∧
        (fun (i : ι) ↦
            if hi : i ∈ s then a ((e : (a : ↥s) → Fin #s) (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi)) else 0) =
          f) ↔
    s.sum f = n ∧ ∀ (i : ι), f i ≠ 0 → i ∈ s
⊢ f ∈
      Trunc.lift
        (fun (e : ↥s ≃ Fin #s) ↦
          map
            {
              toFun := fun (f : Fin #s → μ) (i : ι) ↦
                if hi : i ∈ s then f ((e : (a : ↥s) → Fin #s) (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi)) else 0,
              inj' := ⋯ : (Fin #s → μ) ↪ ι → μ }
            (finAntidiagonal (#s) n))
        ⋯ (Trunc.mk e) ↔
    s.sum f = n ∧ ∀ (i : ι), f i ≠ 0 → i ∈ s

Tactic:
simp only [Trunc.lift_mk, mem_map, mem_finAntidiagonal, Embedding.coeFn_mk]

Premises used: Trunc.lift_mk, Function.Embedding.coeFn_mk, Finset.mem_map, Finset.mem_finAntidiagonal
-- Module: Mathlib.Algebra.Order.Antidiag.Pi
Goal:
ι : Type u_1
μ : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
s : Finset ι
n : μ
f : ι → μ
e : ↥s ≃ Fin #s
a :
  (∃ (a : Fin #s → μ),
      ∑ i : Fin #s, a i = n ∧
        (fun (i : ι) ↦
            if hi : i ∈ s then a ((e : (a : ↥s) → Fin #s) (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi)) else 0) =
          f) →
    s.sum f = n ∧ ∀ (i : ι), f i ≠ 0 → i ∈ s
a₁ :
  (s.sum f = n ∧ ∀ (i : ι), f i ≠ 0 → i ∈ s) →
    ∃ (a : Fin #s → μ),
      ∑ i : Fin #s, a i = n ∧
        (fun (i : ι) ↦
            if hi : i ∈ s then a ((e : (a : ↥s) → Fin #s) (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi)) else 0) =
          f
⊢ (∃ (a : Fin #s → μ),
      ∑ i : Fin #s, a i = n ∧
        (fun (i : ι) ↦
            if hi : i ∈ s then a ((e : (a : ↥s) → Fin #s) (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi)) else 0) =
          f) ↔
    s.sum f = n ∧ ∀ (i : ι), f i ≠ 0 → i ∈ s

Tactic:
constructor
-- Module: Mathlib.Algebra.Order.Antidiag.Pi
Goal:
ι : Type u_1
μ : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
s : Finset ι
e : ↥s ≃ Fin #s
f : Fin #s → μ
a :
  Eq.{u_2 + 1} (α := μ) (∑ i : ↥s, f ((e : (a : ↥s) → Fin #s) (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) (↑i : ι) ⋯)))
      (∑ i : Fin #s, f i) ∧
    ∀ (i : ι),
      Ne.{u_2 + 1} (α := μ)
          ((fun (i : ι) ↦
              (if hi : i ∈ s then f ((e : (a : ↥s) → Fin #s) (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi)) else 0 : μ))
            i)
          0 →
        i ∈ s
⊢ Eq.{u_2 + 1} (α := μ)
      (∑ i ∈ s, if hi : i ∈ s then f ((e : (a : ↥s) → Fin #s) (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi)) else 0)
      (∑ i : Fin #s, f i) ∧
    ∀ (i : ι),
      Ne.{u_2 + 1} (α := μ)
          ((fun (i : ι) ↦
              (if hi : i ∈ s then f ((e : (a : ↥s) → Fin #s) (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi)) else 0 : μ))
            i)
          0 →
        i ∈ s

Tactic:
rw [sum_dite_of_true fun _ ↦ id]

Premises used: id, Finset.sum_dite_of_true
-- Module: Mathlib.Algebra.Order.Antidiag.Pi
Goal:
ι : Type u_1
μ : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
s : Finset ι
e : ↥s ≃ Fin #s
f : Fin #s → μ
⊢ ∀ (x : ↥s),
    f ((e : (a : ↥s) → Fin #s) (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) (↑x : ι) ⋯)) = f ((e : (a : ↥s) → Fin #s) x)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Antidiag.Pi
Goal:
ι : Type u_1
μ : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
s : Finset ι
e : ↥s ≃ Fin #s
f : Fin #s → μ
⊢ ∀ (i : ι),
    Ne.{u_2 + 1} (α := μ)
        ((fun (i : ι) ↦
            (if hi : i ∈ s then f ((e : (a : ↥s) → Fin #s) (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi)) else 0 : μ))
          i)
        0 →
      i ∈ s

Tactic:
simp +contextual
-- Module: Mathlib.Algebra.Order.Antidiag.Pi
Goal:
ι : Type u_1
μ : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
s : Finset ι
e : ↥s ≃ Fin #s
f : Fin #s → μ
⊢ Eq.{u_2 + 1} (α := μ) (∑ i : ↥s, f ((e : (a : ↥s) → Fin #s) (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) (↑i : ι) ⋯)))
      (∑ i : Fin #s, f i) ∧
    ∀ (i : ι),
      Ne.{u_2 + 1} (α := μ)
          ((fun (i : ι) ↦
              (if hi : i ∈ s then f ((e : (a : ↥s) → Fin #s) (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi)) else 0 : μ))
            i)
          0 →
        i ∈ s

Tactic:
exact ⟨Fintype.sum_equiv e _ _ (by simp), by simp +contextual⟩
-- Module: Mathlib.Algebra.Order.Antidiag.Pi
Goal:
ι : Type u_1
μ : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
s : Finset ι
f : ι → μ
e : ↥s ≃ Fin #s
hf : ∀ (i : ι), f i ≠ 0 → i ∈ s
⊢ (fun (i : ι) ↦
      if hi : i ∈ s then
        comp (α := Fin #s) f
          (comp (β := ↥s) (Subtype.val (p := fun (x : ι) ↦ x ∈ s)) (⇑e.symm : (a : Fin #s) → ↥s) : Fin #s → ι)
          ((e : (a : ↥s) → Fin #s) (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi) : Fin #s)
      else 0) =
    f

Tactic:
grind