awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Pi (goal)
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) → μ
⊢ (∃ (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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Pi (goal)
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
⊢ (∃ (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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Pi (goal)
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 : μ
⊢ Finset (ι → μ)
have 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
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₂ ↦ ?_
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Pi (goal)
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
⊢ Finset (ι → μ)
have 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' := sorry }
            (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' := sorry }
            (finAntidiagonal (#s) n) :
          Finset (ι → μ)))
      e₂)
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₂ ↦ ?_
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Pi (goal)
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)
⊢ f = g
have refine_1 : ∀ (i : Fin #s), f i = g i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Pi (goal)
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
⊢ 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₂)
have 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' := sorry }
              (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' := sorry }
              (finAntidiagonal (#s) n) :
            Finset (ι → μ)))
        e₂)
      f
Tactic: ext f
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Pi (goal)
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 : ι → μ
⊢ 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
have 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' := sorry } :
            (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' := sorry } :
            (a : Fin #s → μ) → ι → μ)
          a =
        f
Tactic: simp only [mem_map, mem_finAntidiagonal]
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Pi (goal)
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
have 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' := sorry } :
            (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' := sorry } :
            (a : Fin #s → μ) → ι → μ)
          (((e₁.symm.trans e₂).arrowCongr (Equiv.refl μ) : (a : Fin #s → μ) → Fin #s → μ) g : Fin #s → μ) =
        f
Tactic: refine Equiv.exists_congr ((e₁.symm.trans e₂).arrowCongr <| .refl _) fun g ↦ ?_
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Pi (hypothesis)
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 → μ
⊢ ∑ 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
have this : 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
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Pi (goal)
Goal:
ι : Type u_1
μ : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
s : Finset ι
n : μ
f : ι → μ
⊢ 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
have 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' := sorry : (Fin #s → μ) ↪ ι → μ }
            (finAntidiagonal (#s) n))
        sorry (Trunc.mk e) ↔
    s.sum f = n ∧ ∀ (i : ι), f i ≠ 0 → i ∈ s
Tactic: induction Fintype.truncEquivFinOfCardEq (Fintype.card_coe s) using Trunc.ind with | _ e
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Pi (goal)
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
⊢ 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
have 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
Tactic: simp only [Trunc.lift_mk, mem_map, mem_finAntidiagonal, Embedding.coeFn_mk]
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Pi (goal)
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 : 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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Pi (goal)
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 : 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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Pi (goal)
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, 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
have a : Eq.{u_2 + 1} (α := μ) (∑ i : ↥s, f ((e : (a : ↥s) → Fin #s) (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) (↑i : ι) sorry)))
    (∑ 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]
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Pi (goal)
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 : 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
have a : ∑ i : Fin #s, (f ∘ comp (β := ↥s) (Subtype.val (p := fun (x : ι) ↦ x ∈ s)) (⇑e.symm : (a : Fin #s) → ↥s)) i = s.sum f
Tactic: refine ⟨f ∘ (↑) ∘ e.symm, ?_, by grind⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Pi (goal)
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
⊢ ∑ i : Fin #s, (f ∘ comp (β := ↥s) (Subtype.val (p := fun (x : ι) ↦ x ∈ s)) (⇑e.symm : (a : Fin #s) → ↥s)) i = s.sum f
have 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 : ι))
Tactic: rw [← sum_attach s]
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Pi (goal)
Goal:
ι : Type u_1
μ : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
⊢ Eq (α := Finset (ι → μ)) (piAntidiag ∅ 0) {0}
have h : ∀ (a : ι → μ), Membership.mem (γ := Finset (ι → μ)) (piAntidiag ∅ 0) a ↔ Membership.mem (γ := Finset (ι → μ)) {0} a
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Pi (goal)
Goal:
ι : Type u_1
μ : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
n : μ
⊢ Eq (α := Finset (ι → μ)) (piAntidiag ∅ n) (if n = 0 then {0} else ∅)
have pos : ∀ (hn : n = 0), Eq (α := Finset (ι → μ)) (piAntidiag ∅ n) {0}
Tactic: split_ifs with hn
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Pi (goal)
Goal:
ι : Type u_1
μ : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
n : μ
pos : ∀ (hn : n = 0), Eq (α := Finset (ι → μ)) (piAntidiag ∅ n) {0}
⊢ Eq (α := Finset (ι → μ)) (piAntidiag ∅ n) (if n = 0 then {0} else ∅)
have neg : ∀ (hn : ¬n = 0), Eq (α := Finset (ι → μ)) (piAntidiag ∅ n) ∅
Tactic: split_ifs with hn
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Pi (goal)
Goal:
μ : Type u_2
inst : AddCommMonoid μ
inst_1 : HasAntidiagonal μ
inst_2 : DecidableEq μ
n : μ
⊢ ((Equiv.boolArrowEquivProd μ).finsetCongr : (a : Finset (Bool → μ)) → Finset (μ × μ)) (piAntidiag univ n) =
    @antidiagonal _ AddCommMonoid.toAddMonoid _ n
have 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
Tactic: ext ⟨x₁, x₂⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Pi (goal)
Goal:
μ : Type u_2
inst : AddCommMonoid μ
inst_1 : HasAntidiagonal μ
inst_2 : DecidableEq μ
n x₁ x₂ : μ
⊢ Membership.mem (γ := Finset (μ × μ))
      (((Equiv.boolArrowEquivProd μ).finsetCongr : (a : Finset (Bool → μ)) → Finset (μ × μ)) (piAntidiag univ n) :
        Finset (μ × μ))
      (x₁, x₂) ↔
    (x₁, x₂) ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n
have 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
Tactic: simp_rw [Equiv.finsetCongr_apply, mem_map, Equiv.toEmbedding, Function.Embedding.coeFn_mk,
    ← Equiv.eq_symm_apply]
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Pi (goal)
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 (μ × μ))
⊢ (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)
have 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
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]
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Pi (goal)
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 : μ
⊢ (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)) ⋯
have 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)) sorry
Tactic: ext f
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Pi (goal)
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 : ι → μ
⊢ 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)) ⋯
have 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
Tactic: simp only [mem_piAntidiag, sum_cons, ne_eq, mem_cons, mem_disjiUnion, mem_antidiagonal, mem_map,
    Prod.exists]
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Pi (goal)
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 : ι → μ
⊢ (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
have 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
Tactic: constructor