awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
a :
  ∑ i : Fin #s, (f ∘ comp (β := ↥s) (Subtype.val (p := fun (x : ι) ↦ x ∈ s)) (⇑e.symm : (a : Fin #s) → ↥s)) i = s.sum f
⊢ ∃ (a : Fin #s → μ),
    ∑ i : Fin #s, a i = s.sum f ∧
      (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

Tactic:
refine ⟨f ∘ (↑) ∘ e.symm, ?_, by grind⟩
-- 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
a :
  Eq.{u_2 + 1} (α := μ)
    (∑ i : Fin #s, (f ∘ comp (β := ↥s) (Subtype.val (p := fun (x : ι) ↦ x ∈ s)) (⇑e.symm : (a : Fin #s) → ↥s)) i)
    (∑ x ∈ s.attach, f (↑x : ι))
⊢ ∑ i : Fin #s, (f ∘ comp (β := ↥s) (Subtype.val (p := fun (x : ι) ↦ x ∈ s)) (⇑e.symm : (a : Fin #s) → ↥s)) i = s.sum f

Tactic:
rw [← sum_attach s]

Premises used: Finset.sum_attach
-- 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
⊢ ∀ (x : Fin #s),
    (f ∘ comp (β := ↥s) (Subtype.val (p := fun (x : ι) ↦ x ∈ s)) (⇑e.symm : (a : Fin #s) → ↥s)) x =
      f (↑((e.symm : (a : Fin #s) → ↥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 ι
f : ι → μ
e : ↥s ≃ Fin #s
hf : ∀ (i : ι), f i ≠ 0 → i ∈ s
⊢ Eq.{u_2 + 1} (α := μ)
    (∑ i : Fin #s, (f ∘ comp (β := ↥s) (Subtype.val (p := fun (x : ι) ↦ x ∈ s)) (⇑e.symm : (a : Fin #s) → ↥s)) i)
    (∑ x ∈ s.attach, f (↑x : ι))

Tactic:
exact Fintype.sum_equiv e.symm _ _ (by simp)

Premises used: Equiv.symm, Fintype.sum_equiv
-- Module: Mathlib.Algebra.Order.Antidiag.Pi
Goal:
ι : Type u_1
μ : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
h : ∀ (a : ι → μ), Membership.mem (γ := Finset (ι → μ)) (piAntidiag ∅ 0) a ↔ Membership.mem (γ := Finset (ι → μ)) {0} a
⊢ Eq (α := Finset (ι → μ)) (piAntidiag ∅ 0) {0}

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

Tactic:
simp [funext_iff]

Premises used: funext_iff
-- Module: Mathlib.Algebra.Order.Antidiag.Pi
Goal:
ι : Type u_1
μ : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
n : μ
hn : n ≠ 0
⊢ ∀ (x : ι → μ), x ∉ piAntidiag ∅ n

Tactic:
simp [hn.symm]

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

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

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 μ
n : μ
hn : ¬n = 0
⊢ Eq (α := Finset (ι → μ)) (piAntidiag ∅ n) ∅

Tactic:
simp [*]
-- Module: Mathlib.Algebra.Order.Antidiag.Pi
Goal:
μ : Type u_2
inst : AddCommMonoid μ
inst_1 : HasAntidiagonal μ
inst_2 : DecidableEq μ
n : μ
h :
  ∀ (x₁ x₂ : μ),
    Membership.mem (γ := Finset (μ × μ))
        (((Equiv.boolArrowEquivProd μ).finsetCongr : (a : Finset (Bool → μ)) → Finset (μ × μ)) (piAntidiag univ n) :
          Finset (μ × μ))
        (x₁, x₂) ↔
      (x₁, x₂) ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n
⊢ ((Equiv.boolArrowEquivProd μ).finsetCongr : (a : Finset (Bool → μ)) → Finset (μ × μ)) (piAntidiag univ n) =
    @antidiagonal _ AddCommMonoid.toAddMonoid _ n

Tactic:
ext ⟨x₁, x₂⟩
-- Module: Mathlib.Algebra.Order.Antidiag.Pi
Goal:
μ : Type u_2
inst : AddCommMonoid μ
inst_1 : HasAntidiagonal μ
inst_2 : DecidableEq μ
n x₁ x₂ : μ
h :
  (∃ (a : Bool → μ),
      Membership.mem (γ := Finset (Bool → μ)) (piAntidiag univ n) a ∧
        a = ((Equiv.boolArrowEquivProd μ).symm : (a : μ × μ) → Bool → μ) (x₁, x₂)) ↔
    (x₁, x₂) ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n
⊢ Membership.mem (γ := Finset (μ × μ))
      (((Equiv.boolArrowEquivProd μ).finsetCongr : (a : Finset (Bool → μ)) → Finset (μ × μ)) (piAntidiag univ n) :
        Finset (μ × μ))
      (x₁, x₂) ↔
    (x₁, x₂) ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n

Tactic:
simp_rw [Equiv.finsetCongr_apply, mem_map, Equiv.toEmbedding, Function.Embedding.coeFn_mk,
    ← Equiv.eq_symm_apply]

Premises used: Equiv.finsetCongr_apply, Equiv.toEmbedding, Function.Embedding.coeFn_mk, Finset.mem_map, Equiv.eq_symm_apply
-- Module: Mathlib.Algebra.Order.Antidiag.Pi
Goal:
μ : Type u_2
inst : AddCommMonoid μ
inst_1 : HasAntidiagonal μ
inst_2 : DecidableEq μ
n x₁ x₂ : μ
⊢ (∃ (a : Bool → μ),
      Membership.mem (γ := Finset (Bool → μ)) (piAntidiag univ n) a ∧
        a = ((Equiv.boolArrowEquivProd μ).symm : (a : μ × μ) → Bool → μ) (x₁, x₂)) ↔
    (x₁, x₂) ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n

Tactic:
simp [add_comm]

Premises used: add_comm
-- Module: Mathlib.Algebra.Order.Antidiag.Pi
Goal:
ι : Type u_1
μ : Type u_2
inst : DecidableEq ι
inst_1 : AddCancelCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
i : ι
s : Finset ι
hi : i ∉ s
n a b : μ
hab : (a, b) ∈ (↑(@antidiagonal _ AddCommMonoid.toAddMonoid _ n) : Set (μ × μ))
c d : μ
hcd : (c, d) ∈ (↑(@antidiagonal _ AddCommMonoid.toAddMonoid _ n) : Set (μ × μ))
simp :
  ¬b = d →
    ∀ ⦃a_2 : (j : ι) → μ⦄ (x : (j : ι) → μ),
      s.sum x = b →
        (∀ (i : ι), ¬x i = 0 → i ∈ s) →
          (x + fun (j : ι) ↦ if j = i then a else 0) = a_2 →
            ∀ (x : (j : ι) → μ),
              s.sum x = d → (∀ (i : ι), ¬x i = 0 → i ∈ s) → ¬(x + fun (j : ι) ↦ if j = i then c else 0) = a_2
⊢ (a, b) ≠ (c, d) →
    onFun (β := Finset ((j : ι) → μ)) Disjoint
      (fun (p : μ × μ) ↦ map (addRightEmbedding fun (j : ι) ↦ if j = i then p.1 else 0) (s.piAntidiag p.2)) (a, b)
      (c, d)

Tactic:
simp only [ne_eq, antidiagonal_congr' hab hcd, disjoint_left, mem_map, mem_piAntidiag,
    addRightEmbedding_apply, not_exists, not_and, and_imp, forall_exists_index]

Premises used: addRightEmbedding_apply, and_imp, forall_exists_index, not_exists, Finset.mem_piAntidiag, ne_eq, Finset.disjoint_left, Finset.mem_map, Finset.antidiagonal_congr', not_and
-- Module: Mathlib.Algebra.Order.Antidiag.Pi
Goal:
ι : Type u_1
μ : Type u_2
inst : DecidableEq ι
inst_1 : AddCancelCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
i : ι
s : Finset ι
hi : i ∉ s
n a c : μ
f : (j : ι) → μ
hab : (a, s.sum f) ∈ (↑(@antidiagonal _ AddCommMonoid.toAddMonoid _ n) : Set (μ × μ))
g : (j : ι) → μ
hcd : (c, s.sum g) ∈ (↑(@antidiagonal _ AddCommMonoid.toAddMonoid _ n) : Set (μ × μ))
hfg : ¬s.sum f = s.sum g
hgf : (g + fun (j : ι) ↦ if j = i then c else 0) = f + fun (j : ι) ↦ if j = i then a else 0
⊢ s.sum f = s.sum g

Tactic:
simpa [sum_add_distrib, hi] using congr_arg (∑ j ∈ s, · j) hgf.symm

Premises used: Finset.sum_add_distrib, congr_arg, Eq.symm, Finset.sum
-- Module: Mathlib.Algebra.Order.Antidiag.Pi
Goal:
ι : Type u_1
μ : Type u_2
inst : DecidableEq ι
inst_1 : AddCancelCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
i : ι
s : Finset ι
hi : i ∉ s
n a c : μ
f : (j : ι) → μ
hab : (a, s.sum f) ∈ (↑(@antidiagonal _ AddCommMonoid.toAddMonoid _ n) : Set (μ × μ))
g : (j : ι) → μ
hcd : (c, s.sum g) ∈ (↑(@antidiagonal _ AddCommMonoid.toAddMonoid _ n) : Set (μ × μ))
hfg : ¬s.sum f = s.sum g
hgf : (g + fun (j : ι) ↦ if j = i then c else 0) = f + fun (j : ι) ↦ if j = i then a else 0
⊢ False

Tactic:
exact hfg <| by simpa [sum_add_distrib, hi] using congr_arg (∑ j ∈ s, · j) hgf.symm
-- Module: Mathlib.Algebra.Order.Antidiag.Pi
Goal:
ι : Type u_1
μ : Type u_2
inst : DecidableEq ι
inst_1 : AddCancelCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
i : ι
s : Finset ι
hi : i ∉ s
n : μ
h :
  ∀ (f : ι → μ),
    f ∈ (cons i s hi).piAntidiag n ↔
      f ∈
        (@antidiagonal _ AddCommMonoid.toAddMonoid _ n).disjiUnion
          (fun (p : μ × μ) ↦ map (addRightEmbedding fun (t : ι) ↦ if t = i then p.1 else 0) (s.piAntidiag p.2)) ⋯
⊢ (cons i s hi).piAntidiag n =
    (@antidiagonal _ AddCommMonoid.toAddMonoid _ n).disjiUnion
      (fun (p : μ × μ) ↦ map (addRightEmbedding fun (t : ι) ↦ if t = i then p.1 else 0) (s.piAntidiag p.2)) ⋯

Tactic:
ext f
-- Module: Mathlib.Algebra.Order.Antidiag.Pi
Goal:
ι : Type u_1
μ : Type u_2
inst : DecidableEq ι
inst_1 : AddCancelCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
i : ι
s : Finset ι
hi : i ∉ s
n : μ
f : ι → μ
h :
  (f i + ∑ x ∈ s, f x = n ∧ ∀ (i_1 : ι), ¬f i_1 = 0 → i_1 = i ∨ i_1 ∈ s) ↔
    ∃ (a : μ) (b : μ),
      a + b = n ∧
        ∃ (a_1 : (t : ι) → μ),
          (s.sum a_1 = b ∧ ∀ (i : ι), ¬a_1 i = 0 → i ∈ s) ∧
            (addRightEmbedding fun (t : ι) ↦ if t = i then a else 0 : (a : (t : ι) → μ) → ι → μ) a_1 = f
⊢ f ∈ (cons i s hi).piAntidiag n ↔
    f ∈
      (@antidiagonal _ AddCommMonoid.toAddMonoid _ n).disjiUnion
        (fun (p : μ × μ) ↦ map (addRightEmbedding fun (t : ι) ↦ if t = i then p.1 else 0) (s.piAntidiag p.2)) ⋯

Tactic:
simp only [mem_piAntidiag, sum_cons, ne_eq, mem_cons, mem_disjiUnion, mem_antidiagonal, mem_map,
    Prod.exists]

Premises used: Finset.sum_cons, Finset.mem_piAntidiag, Finset.mem_disjiUnion, ne_eq, Finset.HasAntidiagonal.mem_antidiagonal, Finset.mem_map, Prod.exists, Finset.mem_cons
-- Module: Mathlib.Algebra.Order.Antidiag.Pi
Goal:
ι : Type u_1
μ : Type u_2
inst : DecidableEq ι
inst_1 : AddCancelCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
i : ι
s : Finset ι
hi : i ∉ s
n : μ
f : ι → μ
h :
  (f i + ∑ x ∈ s, f x = n ∧ ∀ (i_1 : ι), ¬f i_1 = 0 → i_1 = i ∨ i_1 ∈ s) →
    ∃ (a : μ) (b : μ),
      a + b = n ∧
        ∃ (a_1 : (t : ι) → μ),
          (s.sum a_1 = b ∧ ∀ (i : ι), ¬a_1 i = 0 → i ∈ s) ∧
            (addRightEmbedding fun (t : ι) ↦ if t = i then a else 0 : (a : (t : ι) → μ) → ι → μ) a_1 = f
h₁ :
  (∃ (a : μ) (b : μ),
      a + b = n ∧
        ∃ (a_1 : (t : ι) → μ),
          (s.sum a_1 = b ∧ ∀ (i : ι), ¬a_1 i = 0 → i ∈ s) ∧
            (addRightEmbedding fun (t : ι) ↦ if t = i then a else 0 : (a : (t : ι) → μ) → ι → μ) a_1 = f) →
    f i + ∑ x ∈ s, f x = n ∧ ∀ (i_1 : ι), ¬f i_1 = 0 → i_1 = i ∨ i_1 ∈ s
⊢ (f i + ∑ x ∈ s, f x = n ∧ ∀ (i_1 : ι), ¬f i_1 = 0 → i_1 = i ∨ i_1 ∈ s) ↔
    ∃ (a : μ) (b : μ),
      a + b = n ∧
        ∃ (a_1 : (t : ι) → μ),
          (s.sum a_1 = b ∧ ∀ (i : ι), ¬a_1 i = 0 → i ∈ s) ∧
            (addRightEmbedding fun (t : ι) ↦ if t = i then a else 0 : (a : (t : ι) → μ) → ι → μ) a_1 = f

Tactic:
constructor
-- Module: Mathlib.Algebra.Order.Antidiag.Pi
Goal:
ι : Type u_1
μ : Type u_2
inst : DecidableEq ι
inst_1 : AddCancelCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
i : ι
s : Finset ι
hi : i ∉ s
n : μ
f : ι → μ
hn : f i + ∑ x ∈ s, f x = n
hf : ∀ (i_1 : ι), ¬f i_1 = 0 → i_1 = i ∨ i_1 ∈ s
⊢ (addRightEmbedding fun (t : ι) ↦ if t = i then f i else 0 : (a : (t : ι) → μ) → ι → μ)
      (update (β := fun (t : ι) ↦ μ) f i 0) =
    f

Tactic:
aesop
-- Module: Mathlib.Algebra.Order.Antidiag.Pi
Goal:
ι : Type u_1
μ : Type u_2
inst : DecidableEq ι
inst_1 : AddCancelCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
i : ι
s : Finset ι
hi : i ∉ s
n : μ
f : ι → μ
hn : f i + ∑ x ∈ s, f x = n
hf : ∀ (i_1 : ι), ¬f i_1 = 0 → i_1 = i ∨ i_1 ∈ s
h : ∀ (j : ι), ¬update (β := fun (t : ι) ↦ μ) f i 0 j = 0 → j ∈ s
⊢ ∃ (a : μ) (b : μ),
    a + b = n ∧
      ∃ (a_1 : (t : ι) → μ),
        (s.sum a_1 = b ∧ ∀ (i : ι), ¬a_1 i = 0 → i ∈ s) ∧
          (addRightEmbedding fun (t : ι) ↦ if t = i then a else 0 : (a : (t : ι) → μ) → ι → μ) a_1 = f

Tactic:
refine ⟨_, _, hn, update f i 0, ⟨sum_update_of_notMem hi _ _, fun j ↦ ?_⟩, by aesop⟩
-- Module: Mathlib.Algebra.Order.Antidiag.Pi
Goal:
ι : Type u_1
μ : Type u_2
inst : DecidableEq ι
inst_1 : AddCancelCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
i : ι
s : Finset ι
hi : i ∉ s
n : μ
f : ι → μ
hn : f i + ∑ x ∈ s, f x = n
hf : ∀ (i_1 : ι), ¬f i_1 = 0 → i_1 = i ∨ i_1 ∈ s
j : ι
⊢ ∀ (h₁ : ¬f j = 0) (h₂ : ¬j = i), j ∈ s

Tactic:
have := fun h₁ h₂ ↦ (hf j h₁).resolve_left h₂
-- Module: Mathlib.Algebra.Order.Antidiag.Pi
Goal:
ι : Type u_1
μ : Type u_2
inst : DecidableEq ι
inst_1 : AddCancelCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
i : ι
s : Finset ι
hi : i ∉ s
n : μ
f : ι → μ
hn : f i + ∑ x ∈ s, f x = n
hf : ∀ (i_1 : ι), ¬f i_1 = 0 → i_1 = i ∨ i_1 ∈ s
j : ι
this : ∀ (h₁ : ¬f j = 0) (h₂ : ¬j = i), j ∈ s
⊢ ¬update (β := fun (t : ι) ↦ μ) f i 0 j = 0 → j ∈ s

Tactic:
aesop (add simp [update])

Premises used: Function.update
-- Module: Mathlib.Algebra.Order.Antidiag.Pi
Goal:
ι : Type u_1
μ : Type u_2
inst : DecidableEq ι
inst_1 : AddCancelCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
i : ι
s : Finset ι
hi : i ∉ s
n a : μ
g : (t : ι) → μ
hg : ∀ (i : ι), ¬g i = 0 → i ∈ s
hn : a + s.sum g = n
⊢ ¬g i = 0 → i ∈ s

Tactic:
have := hg i
-- Module: Mathlib.Algebra.Order.Antidiag.Pi
Goal:
ι : Type u_1
μ : Type u_2
inst : DecidableEq ι
inst_1 : AddCancelCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
i : ι
s : Finset ι
hi : i ∉ s
n a : μ
g : (t : ι) → μ
hg : ∀ (i : ι), ¬g i = 0 → i ∈ s
hn : a + s.sum g = n
this : ¬g i = 0 → i ∈ s
⊢ HAdd.hAdd (α := μ) (β := μ)
        ((addRightEmbedding fun (t : ι) ↦ if t = i then a else 0 : (a : (t : ι) → μ) → ι → μ) g i : μ)
        (∑ x ∈ s, (addRightEmbedding fun (t : ι) ↦ if t = i then a else 0 : (a : (t : ι) → μ) → ι → μ) g x : μ) =
      n ∧
    ∀ (i_1 : ι),
      ¬Eq.{u_2 + 1} (α := μ)
            ((addRightEmbedding fun (t : ι) ↦ if t = i then a else 0 : (a : (t : ι) → μ) → ι → μ) g i_1 : μ) (0 : μ) →
        i_1 = i ∨ i_1 ∈ s

Tactic:
aesop (add simp [sum_add_distrib])

Premises used: Finset.sum_add_distrib
-- Module: Mathlib.Algebra.Order.Antidiag.Pi
Goal:
ι : Type u_1
μ : Type u_2
inst : DecidableEq ι
inst_1 : AddCancelCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
i : ι
s : Finset ι
inst_4 : DecidableEq (ι → μ)
hi : i ∉ s
n : μ
⊢ (insert i s).piAntidiag n =
    (@antidiagonal _ AddCommMonoid.toAddMonoid _ n).biUnion fun (p : μ × μ) ↦
      image (fun (f : ι → μ) (j : ι) ↦ f j + if j = i then p.1 else 0) (s.piAntidiag p.2)

Tactic:
simpa [map_eq_image, addRightEmbedding] using piAntidiag_cons hi n

Premises used: Finset.piAntidiag_cons, Finset.map_eq_image, addRightEmbedding
-- Module: Mathlib.Algebra.Order.Antidiag.Pi
Goal:
ι : Type u_1
μ : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : PartialOrder μ
inst_3 : CanonicallyOrderedAdd μ
inst_4 : HasAntidiagonal μ
inst_5 : DecidableEq μ
s : Finset ι
h : ∀ (a : ι → μ), Membership.mem (γ := Finset (ι → μ)) (s.piAntidiag 0) a ↔ Membership.mem (γ := Finset (ι → μ)) {0} a
⊢ Eq (α := Finset (ι → μ)) (s.piAntidiag 0) {0}

Tactic:
ext
-- Module: Mathlib.Algebra.Order.Antidiag.Pi
Goal:
ι : Type u_1
μ : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : PartialOrder μ
inst_3 : CanonicallyOrderedAdd μ
inst_4 : HasAntidiagonal μ
inst_5 : DecidableEq μ
s : Finset ι
a : ι → μ
⊢ Membership.mem (γ := Finset (ι → μ)) (s.piAntidiag 0) a ↔ Membership.mem (γ := Finset (ι → μ)) {0} a

Tactic:
simp [funext_iff, not_imp_comm, ← forall_and]

Premises used: not_imp_comm, funext_iff, forall_and
-- Module: Mathlib.Algebra.Order.Antidiag.Pi
Goal:
n k : ℕ
h : ∀ (a : Fin k → ℕ), Membership.mem (γ := Finset (Fin k → ℕ)) (piAntidiag univ n) a ↔ a ∈ Nat.antidiagonalTuple k n
⊢ piAntidiag univ n = Nat.antidiagonalTuple k n

Tactic:
ext
-- Module: Mathlib.Algebra.Order.Antidiag.Pi
Goal:
n k : ℕ
a : Fin k → ℕ
⊢ Membership.mem (γ := Finset (Fin k → ℕ)) (piAntidiag univ n) a ↔ a ∈ Nat.antidiagonalTuple k n

Tactic:
simp [Nat.mem_antidiagonalTuple]

Premises used: Finset.Nat.mem_antidiagonalTuple
-- Module: Mathlib.Algebra.Order.Antidiag.Pi
Goal:
ι : Type u_1
inst : DecidableEq ι
inst_1 : DecidableEq (ι → ℕ)
s : Finset ι
m n : ℕ
hn : n ≠ 0
h : ∀ (f : ι → ℕ), f ∈ SMul.smul n (s.piAntidiag m) ↔ f ∈ {f ∈ s.piAntidiag (n * m) | ∀ i ∈ s, n ∣ f i}
⊢ SMul.smul n (s.piAntidiag m) = {f ∈ s.piAntidiag (n * m) | ∀ i ∈ s, n ∣ f i}

Tactic:
ext f
-- Module: Mathlib.Algebra.Order.Antidiag.Pi
Goal:
ι : Type u_1
inst : DecidableEq ι
inst_1 : DecidableEq (ι → ℕ)
s : Finset ι
m n : ℕ
hn : n ≠ 0
f : ι → ℕ
⊢ f ∈ SMul.smul n (s.piAntidiag m) ↔ f ∈ {f ∈ s.piAntidiag (n * m) | ∀ i ∈ s, n ∣ f i}

Tactic:
mem_smul_finset.trans ?_

Premises used: Set.Mem, setOf, Finset.mem_smul_finset, Iff.trans
-- Module: Mathlib.Algebra.Order.Antidiag.Pi
Goal:
ι : Type u_1
inst : DecidableEq ι
inst_1 : DecidableEq (ι → ℕ)
s : Finset ι
m n : ℕ
hn : n ≠ 0
f : ι → ℕ
h : (∃ y ∈ s.piAntidiag m, n • y = f) ↔ f ∈ {f ∈ s.piAntidiag (n * m) | ∀ i ∈ s, n ∣ f i}
⊢ f ∈ SMul.smul n (s.piAntidiag m) ↔ f ∈ {f ∈ s.piAntidiag (n * m) | ∀ i ∈ s, n ∣ f i}

Tactic:
refine mem_smul_finset.trans ?_

Premises used: Finset.mem_smul_finset, Iff.trans
-- Module: Mathlib.Algebra.Order.Antidiag.Pi
Goal:
ι : Type u_1
inst : DecidableEq ι
inst_1 : DecidableEq (ι → ℕ)
s : Finset ι
m n : ℕ
hn : n ≠ 0
f : ι → ℕ
h :
  (∃ (y : ι → ℕ), s.sum y = m ∧ (∀ (i : ι), y i ≠ 0 → i ∈ s) ∧ n • y = f) ↔
    s.sum f = n * m ∧ (∀ (i : ι), f i ≠ 0 → i ∈ s) ∧ ∀ i ∈ s, n ∣ f i
⊢ (∃ y ∈ s.piAntidiag m, n • y = f) ↔ f ∈ {f ∈ s.piAntidiag (n * m) | ∀ i ∈ s, n ∣ f i}

Tactic:
simp only [mem_filter, mem_piAntidiag, and_assoc]

Premises used: Finset.mem_piAntidiag, and_assoc, Finset.mem_filter
-- Module: Mathlib.Algebra.Order.Antidiag.Pi
Goal:
ι : Type u_1
inst : DecidableEq ι
inst_1 : DecidableEq (ι → ℕ)
s : Finset ι
m n : ℕ
hn : n ≠ 0
f : ι → ℕ
h :
  (∃ (y : ι → ℕ), s.sum y = m ∧ (∀ (i : ι), y i ≠ 0 → i ∈ s) ∧ n • y = f) →
    s.sum f = n * m ∧ (∀ (i : ι), f i ≠ 0 → i ∈ s) ∧ ∀ i ∈ s, n ∣ f i
h₁ :
  (s.sum f = n * m ∧ (∀ (i : ι), f i ≠ 0 → i ∈ s) ∧ ∀ i ∈ s, n ∣ f i) →
    ∃ (y : ι → ℕ), s.sum y = m ∧ (∀ (i : ι), y i ≠ 0 → i ∈ s) ∧ n • y = f
⊢ (∃ (y : ι → ℕ), s.sum y = m ∧ (∀ (i : ι), y i ≠ 0 → i ∈ s) ∧ n • y = f) ↔
    s.sum f = n * m ∧ (∀ (i : ι), f i ≠ 0 → i ∈ s) ∧ ∀ i ∈ s, n ∣ f i

Tactic:
constructor
-- Module: Mathlib.Algebra.Order.Antidiag.Pi
Goal:
ι : Type u_1
inst : DecidableEq ι
inst_1 : DecidableEq (ι → ℕ)
s : Finset ι
n : ℕ
hn : n ≠ 0
f : ι → ℕ
hf : ∀ (i : ι), f i ≠ 0 → i ∈ s
⊢ s.sum (n • f) = n * s.sum f ∧ (∀ (i : ι), (n • f) i ≠ 0 → i ∈ s) ∧ ∀ i ∈ s, n ∣ (n • f) i

Tactic:
simpa [← mul_sum, hn] using hf

Premises used: Finset.mul_sum
-- Module: Mathlib.Algebra.Order.Antidiag.Pi
Goal:
ι : Type u_1
inst : DecidableEq ι
inst_1 : DecidableEq (ι → ℕ)
s : Finset ι
m n : ℕ
hn : n ≠ 0
f : ι → ℕ
hfsum : s.sum f = n * m
hfsup : ∀ (i : ι), f i ≠ 0 → i ∈ s
hfdvd : ∀ i ∈ s, n ∣ f i
i : ι
pos : ∀ (hi : i ∈ s), n ∣ f i
neg : ∀ (hi : i ∉ s), n ∣ f i
⊢ n ∣ f i

Tactic:
by_cases hi : i ∈ s
-- Module: Mathlib.Algebra.Order.Antidiag.Pi
Goal:
ι : Type u_1
inst : DecidableEq ι
inst_1 : DecidableEq (ι → ℕ)
s : Finset ι
m n : ℕ
hn : n ≠ 0
f : ι → ℕ
hfsum : s.sum f = n * m
hfsup : ∀ (i : ι), f i ≠ 0 → i ∈ s
hfdvd : ∀ i ∈ s, n ∣ f i
i : ι
hi : i ∈ s
⊢ n ∣ f i

Tactic:
hfdvd _ hi
-- Module: Mathlib.Algebra.Order.Antidiag.Pi
Goal:
ι : Type u_1
inst : DecidableEq ι
inst_1 : DecidableEq (ι → ℕ)
s : Finset ι
m n : ℕ
hn : n ≠ 0
f : ι → ℕ
hfsum : s.sum f = n * m
hfsup : ∀ (i : ι), f i ≠ 0 → i ∈ s
hfdvd : ∀ i ∈ s, n ∣ f i
i : ι
hi : i ∈ s
⊢ n ∣ f i

Tactic:
exact hfdvd _ hi
-- Module: Mathlib.Algebra.Order.Antidiag.Pi
Goal:
ι : Type u_1
inst : DecidableEq ι
inst_1 : DecidableEq (ι → ℕ)
s : Finset ι
m n : ℕ
hn : n ≠ 0
f : ι → ℕ
hfsum : s.sum f = n * m
hfsup : ∀ (i : ι), f i ≠ 0 → i ∈ s
hfdvd : ∀ i ∈ s, n ∣ f i
i : ι
hi : i ∉ s
neg : n ∣ 0
⊢ n ∣ f i

Tactic:
rw [not_imp_comm.1 (hfsup _) hi]

Premises used: not_imp_comm, Iff.mp
-- Module: Mathlib.Algebra.Order.Antidiag.Pi
Goal:
ι : Type u_1
inst : DecidableEq ι
inst_1 : DecidableEq (ι → ℕ)
s : Finset ι
m n : ℕ
hn : n ≠ 0
f : ι → ℕ
hfsum : s.sum f = n * m
hfsup : ∀ (i : ι), f i ≠ 0 → i ∈ s
hfdvd : ∀ i ∈ s, n ∣ f i
i : ι
hi : i ∉ s
⊢ n ∣ 0

Tactic:
dvd_zero _

Premises used: dvd_zero
-- Module: Mathlib.Algebra.Order.Antidiag.Pi
Goal:
ι : Type u_1
inst : DecidableEq ι
inst_1 : DecidableEq (ι → ℕ)
s : Finset ι
m n : ℕ
hn : n ≠ 0
f : ι → ℕ
hfsum : s.sum f = n * m
hfsup : ∀ (i : ι), f i ≠ 0 → i ∈ s
hfdvd : ∀ i ∈ s, n ∣ f i
i : ι
hi : i ∉ s
⊢ n ∣ 0

Tactic:
exact dvd_zero _

Premises used: dvd_zero
-- Module: Mathlib.Algebra.Order.Antidiag.Pi
Goal:
ι : Type u_1
inst : DecidableEq ι
inst_1 : DecidableEq (ι → ℕ)
s : Finset ι
m n : ℕ
hn : n ≠ 0
f : ι → ℕ
hfsum : s.sum f = n * m
hfsup : ∀ (i : ι), f i ≠ 0 → i ∈ s
hfdvd : ∀ i ∈ s, n ∣ f i
⊢ ∀ (i : ι), n ∣ f i

Tactic:
have (i : _) : n ∣ f i := by
    by_cases hi : i ∈ s
    · exact hfdvd _ hi
    · rw [not_imp_comm.1 (hfsup _) hi]
      exact dvd_zero _
-- Module: Mathlib.Algebra.Order.Antidiag.Pi
Goal:
ι : Type u_1
inst : DecidableEq ι
inst_1 : DecidableEq (ι → ℕ)
s : Finset ι
m n : ℕ
hn : n ≠ 0
f : ι → ℕ
hfsum : s.sum f = n * m
hfsup : ∀ (i : ι), f i ≠ 0 → i ∈ s
hfdvd : ∀ i ∈ s, n ∣ f i
this : ∀ (i : ι), n ∣ f i
⊢ ∃ (y : ι → ℕ), s.sum y = m ∧ (∀ (i : ι), y i ≠ 0 → i ∈ s) ∧ n • y = f

Tactic:
⟨fun i ↦ f i / n, ?_⟩

Premises used: HDiv.hDiv, Exists.intro
-- Module: Mathlib.Algebra.Order.Antidiag.Pi
Goal:
ι : Type u_1
inst : DecidableEq ι
inst_1 : DecidableEq (ι → ℕ)
s : Finset ι
m n : ℕ
hn : n ≠ 0
f : ι → ℕ
hfsum : s.sum f = n * m
hfsup : ∀ (i : ι), f i ≠ 0 → i ∈ s
hfdvd : ∀ i ∈ s, n ∣ f i
this : ∀ (i : ι), n ∣ f i
h :
  ∑ i ∈ s, f i / n = m ∧
    (∀ (i : ι), Ne (α := ℕ) ((fun (i : ι) ↦ f i / n) i) 0 → i ∈ s) ∧
      (HSMul.hSMul (β := ι → ℕ) n fun (i : ι) ↦ f i / n) = f
⊢ ∃ (y : ι → ℕ), s.sum y = m ∧ (∀ (i : ι), y i ≠ 0 → i ∈ s) ∧ n • y = f

Tactic:
refine ⟨fun i ↦ f i / n, ?_⟩
-- Module: Mathlib.Algebra.Order.Antidiag.Pi
Goal:
ι : Type u_1
inst : DecidableEq ι
inst_1 : DecidableEq (ι → ℕ)
s : Finset ι
m n : ℕ
hn : n ≠ 0
f : ι → ℕ
hfsum : s.sum f = n * m
hfsup : ∀ (i : ι), f i ≠ 0 → i ∈ s
hfdvd : ∀ i ∈ s, n ∣ f i
this : ∀ (i : ι), n ∣ f i
h : ∀ (i : ι), n ≤ f i → i ∈ s
⊢ ∑ i ∈ s, f i / n = m ∧
    (∀ (i : ι), Ne (α := ℕ) ((fun (i : ι) ↦ f i / n) i) 0 → i ∈ s) ∧
      (HSMul.hSMul (β := ι → ℕ) n fun (i : ι) ↦ f i / n) = f

Tactic:
simp [funext_iff, Nat.mul_div_cancel', ← Nat.sum_div, *]

Premises used: funext_iff, Nat.sum_div, Nat.mul_div_cancel'
-- Module: Mathlib.Algebra.Order.Antidiag.Pi
Goal:
ι : Type u_1
inst : DecidableEq ι
inst_1 : DecidableEq (ι → ℕ)
s : Finset ι
m n : ℕ
hn : n ≠ 0
f : ι → ℕ
hfsum : s.sum f = n * m
hfsup : ∀ (i : ι), f i ≠ 0 → i ∈ s
hfdvd : ∀ i ∈ s, n ∣ f i
this : ∀ (i : ι), n ∣ f i
⊢ ∀ (i : ι), n ≤ f i → i ∈ s

Tactic:
grind
-- Module: Mathlib.Algebra.Order.Antidiag.Pi
Goal:
ι : Type u_1
inst : DecidableEq ι
s : Finset ι
m n : ℕ
hn : n ≠ 0
rw :
  image (⇑{ toFun := fun (x : (x : ι) → ℕ) ↦ n • x, inj' := ⋯ } : (a : (x : ι) → ℕ) → (x : ι) → ℕ) (s.piAntidiag m) =
    {f ∈ s.piAntidiag (n * m) | ∀ i ∈ s, n ∣ f i}
⊢ map { toFun := fun (x : (x : ι) → ℕ) ↦ n • x, inj' := ⋯ } (s.piAntidiag m) =
    {f ∈ s.piAntidiag (n * m) | ∀ i ∈ s, n ∣ f i}

Tactic:
rw [map_eq_image]

Premises used: Finset.map_eq_image
-- Module: Mathlib.Algebra.Order.Antidiag.Pi
Goal:
ι : Type u_1
inst : DecidableEq ι
s : Finset ι
m n : ℕ
hn : n ≠ 0
⊢ image (⇑{ toFun := fun (x : (x : ι) → ℕ) ↦ n • x, inj' := ⋯ } : (a : (x : ι) → ℕ) → (x : ι) → ℕ) (s.piAntidiag m) =
    {f ∈ s.piAntidiag (n * m) | ∀ i ∈ s, n ∣ f i}

Tactic:
nsmul_piAntidiag _ _ hn

Premises used: Finset.nsmul_piAntidiag