mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
X✝ Y✝ : C
inst✝¹ : HasBinaryBiproduct X✝ Y✝
X Y : C
f : X ⟶ Y
inst✝ : IsSplitEpi f
c : KernelFork f
i : IsLimit c
c' : KernelFork (𝟙 X - (𝟙 X - f ≫ section_ f)) := KernelFork.ofι (Fork.ι c) ⋯
⊢ 𝟙 X - (𝟙 X - f ≫ section_ f) = f ≫ section_ f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
X✝ Y✝ : C
inst✝¹ : HasBinaryBiproduct X✝ Y✝
X Y : C
f : X ⟶ Y
inst✝ : IsSplitEpi f
c : KernelFork f
i : IsLimit c
c' : KernelFork (𝟙 X - (𝟙 X - f ≫ section_ f)) := KernelFork.ofι (Fork.ι c) ⋯
i' : IsLimit c' := isKernelCompMono i (section_ f) ⋯
i'' : IsLimit (forkOfKernelFork c') := isLimitForkOfKernelFork i'
⊢ (𝟙 X - f ≫ section_ f) ≫ (𝟙 X - f ≫ section_ f) = 𝟙 X - f ≫ section_ f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
X✝ Y✝ : C
inst✝¹ : HasBinaryBiproduct X✝ Y✝
X Y : C
f : X ⟶ Y
inst✝ : IsSplitEpi f
c : KernelFork f
i : IsLimit c
⊢ (Fork.ι c ≫
      let c' := KernelFork.ofι (Fork.ι c) ⋯;
      let i' := isKernelCompMono i (section_ f) ⋯;
      let i'' := isLimitForkOfKernelFork i';
      (splitMonoOfIdempotentOfIsLimitFork C ⋯ i'').retraction) =
    𝟙 c.pt

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
X✝ Y✝ : C
inst✝¹ : HasBinaryBiproduct X✝ Y✝
X Y : C
f : X ⟶ Y
inst✝ : IsSplitEpi f
c : KernelFork f
i : IsLimit c
⊢ Fork.ι c ≫ f = 0

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
X✝ Y✝ : C
inst✝¹ : HasBinaryBiproduct X✝ Y✝
X Y : C
f : X ⟶ Y
inst✝ : IsSplitEpi f
c : KernelFork f
i : IsLimit c
⊢ (section_ f ≫
      let c' := KernelFork.ofι (Fork.ι c) ⋯;
      let i' := isKernelCompMono i (section_ f) ⋯;
      let i'' := isLimitForkOfKernelFork i';
      (splitMonoOfIdempotentOfIsLimitFork C ⋯ i'').retraction) =
    0

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
X✝ Y✝ : C
inst✝¹ : HasBinaryBiproduct X✝ Y✝
X Y : C
f : X ⟶ Y
inst✝ : IsSplitEpi f
c : KernelFork f
i : IsLimit c
⊢ section_ f ≫ f = 𝟙 Y

Tactic:
by

Goal state after:
Module: Mathlib.Order.Fin.Tuple

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
n : ℕ
q : Fin (n + 1)
x : α
f : Fin n → α
⊢ StrictMono (q.insertNth x f) ↔
    StrictMono f ∧ (∀ (i : Fin n), i.castSucc < q → f i < x) ∧ ∀ (i : Fin n), q ≤ i.castSucc → x < f i

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
X✝ Y✝ : C
inst✝¹ : HasBinaryBiproduct X✝ Y✝
X Y : C
f : X ⟶ Y
inst✝ : IsSplitEpi f
c : KernelFork f
i : IsLimit c
⊢ (Iso.refl c.pt).hom ≫ Fork.ι (binaryBiconeOfIsSplitEpiOfKernel i).sndKernelFork = Fork.ι c

Tactic:
by

Goal state after:
Module: Mathlib.Order.Fin.Tuple

Goal state before:
pp: n : ℕ
f : Fin n → Fin (n + 1)
h : f = succ
⊢ StrictMono (cons 0 f)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
X Y : C
f g : X ⟶ Y
inst✝ : HasBinaryBiproduct X X
⊢ f + g = lift (𝟙 X) (𝟙 X) ≫ desc f g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
X Y : C
f g : X ⟶ Y
inst✝ : HasBinaryBiproduct Y Y
⊢ f + g = lift f g ≫ desc (𝟙 Y) (𝟙 Y)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Fin.Tuple

Goal state before:
pp: n : ℕ
f : Fin n → Fin (n + 1)
h : StrictMono (cons 0 f)
i : Fin n
g : Fin (n + 1) → Fin (n + 1)
hg : StrictMono g
⊢ g = id

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C✝ : Type u
inst✝⁴ : Category.{v, u} C✝
inst✝³ : Preadditive C✝
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
a b : Preadditive C
X Y : C
f g : X ⟶ Y
⊢ HasBinaryBiproduct X X

Tactic:
by

Goal state after:
Module: Mathlib.Order.Fin.Tuple

Goal state before:
pp: n : ℕ
f : Fin n → Fin (n + 1)
⊢ StrictMono (cons 0 f) ↔ f = succ

Tactic:
by

Goal state after:
Module: Mathlib.Order.Fin.Tuple

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
n : ℕ
f : Fin (n + 1) → α
a : α
⊢ Monotone (vecCons a f) ↔ a ≤ f 0 ∧ Monotone f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C✝ : Type u
inst✝⁴ : Category.{v, u} C✝
inst✝³ : Preadditive C✝
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
a b : Preadditive C
X Y : C
f g : X ⟶ Y
h₁ : f + g = biprod.lift (𝟙 X) (𝟙 X) ≫ biprod.desc f g
⊢ HasBinaryBiproduct X X

Tactic:
by

Goal state after:
Module: Mathlib.Order.Fin.Tuple

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
n : ℕ
f : Fin (n + 1) → α
a : α
⊢ Monotone ![1, 2, 2, 3]

Tactic:
by

Goal state after:
Module: Mathlib.Order.Fin.Tuple

Goal state before:
pp: α✝ : Type u_1
inst✝¹ : Preorder α✝
n✝ : ℕ
f : Fin (n✝ + 1) → α✝
a : α✝
n : ℕ
α : Fin (n + 1) → Type u_2
inst✝ : (i : Fin (n + 1)) → LE (α i)
⊢ ∀ {a b : α (last n) × ((i : Fin n) → α i.castSucc)}, (snocEquiv α) a ≤ (snocEquiv α) b ↔ a ≤ b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Fin.Tuple

Goal state before:
pp: α✝ : Type u_1
inst✝¹ : Preorder α✝
n✝ : ℕ
f : Fin (n✝ + 1) → α✝
a : α✝
n : ℕ
α : Fin (n + 1) → Type u_2
inst✝ : (i : Fin (n + 1)) → LE (α i)
p : Fin (n + 1)
⊢ ∀ {a b : α p × ((i : Fin n) → α (p.succAbove i))}, (insertNthEquiv α p) a ≤ (insertNthEquiv α p) b ↔ a ≤ b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Fin.Tuple

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Type u_2
inst✝ : (i : Fin (n + 1)) → LE (α i)
⊢ insertNthOrderIso α 0 = consOrderIso α

Tactic:
by

Goal state after:
Module: Mathlib.Order.Fin.Tuple

Goal state before:
pp: n : ℕ
α : Type u_2
inst✝ : LE α
⊢ insertNthOrderIso (fun x ↦ α) (last n) = snocOrderIso fun x ↦ α

Tactic:
by

Goal state after:
Module: Mathlib.Order.Fin.Tuple

Goal state before:
pp: n : ℕ
x : { x // x ≠ last n }
⊢ (finSuccAboveOrderIso (last n)).symm x = (↑x).castLT ⋯

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C✝ : Type u
inst✝⁴ : Category.{v, u} C✝
inst✝³ : Preadditive C✝
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
a b : Preadditive C
⊢ a = b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Fin.Tuple

Goal state before:
pp: n : ℕ
p : Fin (n + 1)
h : p ≠ last n
x : { x // x ≠ p }
⊢ (finSuccAboveEquiv p).symm x = (p.castLT ⋯).predAbove ↑x

Tactic:
by

Goal state after:
Module: Mathlib.Order.Fin.Tuple

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
n✝¹ : ℕ
f : Fin (n✝¹ + 1) → α
a : α
n✝ n m : ℕ
h : n ≤ m
i : Fin n
⊢ ↑(castLE h i) < n

Tactic:
by

Goal state after:
Module: Mathlib.Order.Fin.Tuple

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
n✝¹ : ℕ
f : Fin (n✝¹ + 1) → α
a : α
n✝ n m : ℕ
h : n ≤ m
x✝ : Fin n
⊢ (fun i ↦ ⟨↑↑i, ⋯⟩) ((fun i ↦ ⟨castLE h i, ⋯⟩) x✝) = x✝

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X₁ X₂ Y₁ Y₂ : C
f₁₁ : X₁ ⟶ Y₁
f₁₂ : X₁ ⟶ Y₂
f₂₁ : X₂ ⟶ Y₁
f₂₂ : X₂ ⟶ Y₂
⊢ biprod.inl ≫ ofComponents f₁₁ f₁₂ f₂₁ f₂₂ = f₁₁ ≫ biprod.inl + f₁₂ ≫ biprod.inr

Tactic:
by

Goal state after:
Module: Mathlib.Order.Fin.Tuple

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
n✝¹ : ℕ
f : Fin (n✝¹ + 1) → α
a : α
n✝ n m : ℕ
h : n ≤ m
x✝ : { i // ↑i < n }
⊢ (fun i ↦ ⟨castLE h i, ⋯⟩) ((fun i ↦ ⟨↑↑i, ⋯⟩) x✝) = x✝

Tactic:
by

Goal state after:
Module: Mathlib.Order.Fin.Tuple

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
n✝¹ : ℕ
f : Fin (n✝¹ + 1) → α
a : α
n✝ n m : ℕ
h : n ≤ m
⊢ ∀ {a b : Fin n},
    { toFun := fun i ↦ ⟨castLE h i, ⋯⟩, invFun := fun i ↦ ⟨↑↑i, ⋯⟩, left_inv := ⋯, right_inv := ⋯ } a ≤
        { toFun := fun i ↦ ⟨castLE h i, ⋯⟩, invFun := fun i ↦ ⟨↑↑i, ⋯⟩, left_inv := ⋯, right_inv := ⋯ } b ↔
      a ≤ b

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X₁ X₂ Y₁ Y₂ : C
f₁₁ : X₁ ⟶ Y₁
f₁₂ : X₁ ⟶ Y₂
f₂₁ : X₂ ⟶ Y₁
f₂₂ : X₂ ⟶ Y₂
⊢ biprod.inr ≫ ofComponents f₁₁ f₁₂ f₂₁ f₂₂ = f₂₁ ≫ biprod.inl + f₂₂ ≫ biprod.inr

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X₁ X₂ Y₁ Y₂ : C
f₁₁ : X₁ ⟶ Y₁
f₁₂ : X₁ ⟶ Y₂
f₂₁ : X₂ ⟶ Y₁
f₂₂ : X₂ ⟶ Y₂
⊢ ofComponents f₁₁ f₁₂ f₂₁ f₂₂ ≫ biprod.fst = biprod.fst ≫ f₁₁ + biprod.snd ≫ f₂₁

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X₁ X₂ Y₁ Y₂ : C
f₁₁ : X₁ ⟶ Y₁
f₁₂ : X₁ ⟶ Y₂
f₂₁ : X₂ ⟶ Y₁
f₂₂ : X₂ ⟶ Y₂
⊢ ofComponents f₁₁ f₁₂ f₂₁ f₂₂ ≫ biprod.snd = biprod.fst ≫ f₁₂ + biprod.snd ≫ f₂₂

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X₁ X₂ Y₁ Y₂ : C
f : X₁ ⊞ X₂ ⟶ Y₁ ⊞ Y₂
⊢ ofComponents (biprod.inl ≫ f ≫ biprod.fst) (biprod.inl ≫ f ≫ biprod.snd) (biprod.inr ≫ f ≫ biprod.fst)
      (biprod.inr ≫ f ≫ biprod.snd) =
    f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C
f₁₁ : X₁ ⟶ Y₁
f₁₂ : X₁ ⟶ Y₂
f₂₁ : X₂ ⟶ Y₁
f₂₂ : X₂ ⟶ Y₂
g₁₁ : Y₁ ⟶ Z₁
g₁₂ : Y₁ ⟶ Z₂
g₂₁ : Y₂ ⟶ Z₁
g₂₂ : Y₂ ⟶ Z₂
⊢ ofComponents f₁₁ f₁₂ f₂₁ f₂₂ ≫ ofComponents g₁₁ g₁₂ g₂₁ g₂₂ =
    ofComponents (f₁₁ ≫ g₁₁ + f₁₂ ≫ g₂₁) (f₁₁ ≫ g₁₂ + f₁₂ ≫ g₂₂) (f₂₁ ≫ g₁₁ + f₂₂ ≫ g₂₁) (f₂₁ ≫ g₁₂ + f₂₂ ≫ g₂₂)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
X₁ X₂ Y₁ Y₂ : C
f₁₁ : X₁ ⟶ Y₁
f₁₂ : X₁ ⟶ Y₂
f₂₁ : X₂ ⟶ Y₁
f₂₂ : X₂ ⟶ Y₂
inst✝ : IsIso f₁₁
⊢ (unipotentLower (-f₂₁ ≫ inv f₁₁)).hom ≫ ofComponents f₁₁ f₁₂ f₂₁ f₂₂ ≫ (unipotentUpper (-inv f₁₁ ≫ f₁₂)).hom =
    biprod.map f₁₁ (f₂₂ - f₂₁ ≫ inv f₁₁ ≫ f₁₂)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
X₁ X₂ Y₁ Y₂ : C
f₁₁ : X₁ ⟶ Y₁
f₁₂ : X₁ ⟶ Y₂
f₂₁ : X₂ ⟶ Y₁
f₂₂ : X₂ ⟶ Y₂
f : X₁ ⊞ X₂ ⟶ Y₁ ⊞ Y₂
inst✝ : IsIso (biprod.inl ≫ f ≫ biprod.fst)
⊢ (L : X₁ ⊞ X₂ ≅ X₁ ⊞ X₂) ×'
    (R : Y₁ ⊞ Y₂ ≅ Y₁ ⊞ Y₂) ×' (g₂₂ : X₂ ⟶ Y₂) ×' L.hom ≫ f ≫ R.hom = biprod.map (biprod.inl ≫ f ≫ biprod.fst) g₂₂

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
inst✝² : HasBinaryBiproducts C
X₁ X₂ Y₁ Y₂ : C
f₁₁ : X₁ ⟶ Y₁
f₁₂ : X₁ ⟶ Y₂
f₂₁ : X₂ ⟶ Y₁
f₂₂ : X₂ ⟶ Y₂
inst✝¹ : IsIso f₁₁
inst✝ : IsIso (ofComponents f₁₁ f₁₂ f₂₁ f₂₂)
L : X₁ ⊞ X₂ ≅ X₁ ⊞ X₂
R : Y₁ ⊞ Y₂ ≅ Y₁ ⊞ Y₂
g : X₂ ⟶ Y₂
w : L.hom ≫ ofComponents f₁₁ f₁₂ f₂₁ f₂₂ ≫ R.hom = biprod.map f₁₁ g
⊢ IsIso (biprod.map f₁₁ g)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
inst✝² : HasBinaryBiproducts C
X₁ X₂ Y₁ Y₂ : C
f₁₁ : X₁ ⟶ Y₁
f₁₂ : X₁ ⟶ Y₂
f₂₁ : X₂ ⟶ Y₁
f₂₂ : X₂ ⟶ Y₂
inst✝¹ : IsIso f₁₁
inst✝ : IsIso (ofComponents f₁₁ f₁₂ f₂₁ f₂₂)
⊢ X₂ ≅ Y₂

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
X₁ X₂ Y₁ Y₂ : C
f₁₁ : X₁ ⟶ Y₁
f₁₂ : X₁ ⟶ Y₂
f₂₁ : X₂ ⟶ Y₁
f₂₂ : X₂ ⟶ Y₂
f : X₁ ⊞ X₂ ≅ Y₁ ⊞ Y₂
inst✝ : IsIso (biprod.inl ≫ f.hom ≫ biprod.fst)
⊢ IsIso
    (ofComponents (biprod.inl ≫ f.hom ≫ biprod.fst) (biprod.inl ≫ f.hom ≫ biprod.snd) (biprod.inr ≫ f.hom ≫ biprod.fst)
      (biprod.inr ≫ f.hom ≫ biprod.snd))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
W X Y Z : C
f : W ⊞ X ⟶ Y ⊞ Z
inst✝ : IsIso f
nz : 𝟙 W ≠ 0
a₁ : biprod.inl ≫ f ≫ biprod.fst = 0
a₂ : biprod.inl ≫ f ≫ biprod.snd = 0
x : W ⟶ W := biprod.inl ≫ f ≫ inv f ≫ biprod.fst
⊢ x = 𝟙 W

Tactic:
by

Goal state after:
Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal

Goal state before:
pp: n k : ℕ
x : Fin k → ℕ
⊢ x ∈ antidiagonalTuple k n ↔ ∑ i, x i = n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Antidiag.Pi

Goal state before:
pp: ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
n✝ : μ
d : ℕ
n : μ
h : n = 0
⊢ ∀ (f : Fin 0 → μ), f ∈ {0} ↔ ∑ i, f i = n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Antidiag.Pi

Goal state before:
pp: ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
n✝ : μ
d : ℕ
n : μ
h : ¬n = 0
⊢ ∀ (f : Fin 0 → μ), f ∈ ∅ ↔ ∑ i, f i = n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Antidiag.Pi

Goal state before:
pp: ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
n✝ : μ
d✝ : ℕ
n : μ
d : ℕ
⊢ (↑(antidiagonal n)).PairwiseDisjoint fun ab ↦ map { toFun := Fin.cons ab.1, inj' := ⋯ } ↑(aux d ab.2)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Antidiag.Pi

Goal state before:
pp: ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
n✝ : μ
d✝ : ℕ
n : μ
d : ℕ
f : Fin (d + 1) → μ
⊢ f ∈ (antidiagonal n).disjiUnion (fun ab ↦ map { toFun := Fin.cons ab.1, inj' := ⋯ } ↑(aux d ab.2)) ⋯ ↔ ∑ i, f i = n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Antidiag.Finsupp

Goal state before:
pp: ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
s✝ : Finset ι
n✝ : μ
f✝ : ι →₀ μ
s : Finset ι
n : μ
f : ↥(s.piAntidiag n)
⊢ ∀ (a : ι), a ∈ {x ∈ s | ↑f x ≠ 0} ↔ ↑f a ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Antidiag.Pi

Goal state before:
pp: ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
n✝ : μ
s : Finset ι
n : μ
⊢ Finset (ι → μ)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Antidiag.Finsupp

Goal state before:
pp: ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
s : Finset ι
n : μ
f : ι →₀ μ
⊢ f ∈ s.finsuppAntidiag n ↔ s.sum ⇑f = n ∧ f.support ⊆ s

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Antidiag.Pi

Goal state before:
pp: ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
s : Finset ι
e : ↥s ≃ Fin #s
f : Fin #s → μ
⊢ ∀ (x : ↥s), f (e ⟨↑x, ⋯⟩) = f (e x)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Antidiag.Pi

Goal state before:
pp: ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
s : Finset ι
e : ↥s ≃ Fin #s
f : Fin #s → μ
⊢ ∀ (i : ι), (fun i ↦ if hi : i ∈ s then f (e ⟨i, hi⟩) else 0) i ≠ 0 → i ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Antidiag.Finsupp

Goal state before:
pp: ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
s : Finset ι
n : μ
f : ι →₀ μ
⊢ f ∈ s.finsuppAntidiag n ↔ (f.sum fun x x_1 ↦ x_1) = n ∧ f.support ⊆ s

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Antidiag.Pi

Goal state before:
pp: ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
s : Finset ι
f : ι → μ
e : ↥s ≃ Fin #s
hf : ∀ (i : ι), f i ≠ 0 → i ∈ s
⊢ (fun i ↦ if hi : i ∈ s then (f ∘ Subtype.val ∘ ⇑e.symm) (e ⟨i, hi⟩) else 0) = f

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Antidiag.Pi

Goal state before:
pp: ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
s : Finset ι
f : ι → μ
e : ↥s ≃ Fin #s
hf : ∀ (i : ι), f i ≠ 0 → i ∈ s
⊢ ∀ (x : Fin #s), (f ∘ Subtype.val ∘ ⇑e.symm) x = f ↑(e.symm x)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Antidiag.Finsupp

Goal state before:
pp: ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
⊢ ∅.finsuppAntidiag 0 = {0}

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Antidiag.Pi

Goal state before:
pp: ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
s : Finset ι
n : μ
f : ι → μ
⊢ f ∈ s.piAntidiag n ↔ s.sum f = n ∧ ∀ (i : ι), f i ≠ 0 → i ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Antidiag.Finsupp

Goal state before:
pp: ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
n : μ
hn : n ≠ 0
⊢ ∀ (x : ι →₀ μ), x ∉ ∅.finsuppAntidiag n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Antidiag.Pi

Goal state before:
pp: ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
⊢ ∅.piAntidiag 0 = {0}

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Antidiag.Pi

Goal state before:
pp: ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
n : μ
hn : n ≠ 0
⊢ ∀ (x : ι → μ), x ∉ ∅.piAntidiag n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Antidiag.Pi

Goal state before:
pp: ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
n : μ
⊢ ∅.piAntidiag n = if n = 0 then {0} else ∅

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Antidiag.Finsupp

Goal state before:
pp: ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
n : μ
⊢ ∅.finsuppAntidiag n = if n = 0 then {0} else ∅

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Antidiag.Pi

Goal state before:
pp: μ : Type u_2
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
n : μ
⊢ (Equiv.boolArrowEquivProd μ).finsetCongr (univ.piAntidiag n) = antidiagonal n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Antidiag.Pi

Goal state before:
pp: ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCancelCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
i : ι
s : Finset ι
hi : i ∉ s
n a c : μ
f : ι → μ
hab : (a, s.sum f) ∈ ↑(antidiagonal n)
g : ι → μ
hcd : (c, s.sum g) ∈ ↑(antidiagonal n)
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:
by

Goal state after:
Module: Mathlib.Algebra.Order.Antidiag.Pi

Goal state before:
pp: ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCancelCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
i : ι
s : Finset ι
hi : i ∉ s
n : μ
⊢ (↑(antidiagonal n)).PairwiseDisjoint fun p ↦
    map (addRightEmbedding fun j ↦ if j = i then p.1 else 0) (s.piAntidiag p.2)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal

Goal state before:
pp: k n : ℕ
⊢ (antidiagonalTuple k n).Nodup

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Antidiag.Pi

Goal state before:
pp: ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCancelCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : 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) (update f i 0) = f

Tactic:
by

Goal state after:
Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal

Goal state before:
pp: k : ℕ
⊢ antidiagonalTuple (k + 1) 0 = [0]

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Antidiag.Pi

Goal state before:
pp: ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCancelCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
i : ι
s : Finset ι
hi : i ∉ s
n : μ
⊢ (cons i s hi).piAntidiag n =
    (antidiagonal n).disjiUnion (fun p ↦ map (addRightEmbedding fun t ↦ if t = i then p.1 else 0) (s.piAntidiag p.2)) ⋯

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Antidiag.Pi

Goal state before:
pp: ι : Type u_1
μ : Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : AddCancelCommMonoid μ
inst✝² : HasAntidiagonal μ
inst✝¹ : DecidableEq μ
i : ι
s : Finset ι
inst✝ : DecidableEq (ι → μ)
hi : i ∉ s
n : μ
⊢ (insert i s).piAntidiag n =
    (antidiagonal n).biUnion fun p ↦ image (fun f j ↦ f j + if j = i then p.1 else 0) (s.piAntidiag p.2)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Antidiag.Pi

Goal state before:
pp: ι : Type u_1
μ : Type u_2
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid μ
inst✝³ : PartialOrder μ
inst✝² : CanonicallyOrderedAdd μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
s : Finset ι
⊢ s.piAntidiag 0 = {0}

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Antidiag.Pi

Goal state before:
pp: n k : ℕ
⊢ univ.piAntidiag n = Nat.antidiagonalTuple k n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Antidiag.Finsupp

Goal state before:
pp: case mp.refine_1
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
a : ι
s : Finset ι
h : a ∉ s
f : ι →₀ μ
hsupp : f.support ⊆ insert a s
⊢ f = f.update a (f a)

Tactic:
Finsupp.update_self

Goal state after:
case mp.refine_1
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
a : ι
s : Finset ι
h : a ∉ s
f : ι →₀ μ
hsupp : f.support ⊆ insert a s
⊢ f = f
Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal

Goal state before:
pp: n : ℕ
⊢ antidiagonalTuple 1 n = [![n]]

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Antidiag.Pi

Goal state before:
pp: ι : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : 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:
by

Goal state after:
Module: Mathlib.Algebra.Order.Antidiag.Pi

Goal state before:
pp: ι : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq (ι → ℕ)
s : Finset ι
m n : ℕ
hn : n ≠ 0
⊢ n • s.piAntidiag m = {f ∈ s.piAntidiag (n * m) | ∀ i ∈ s, n ∣ f i}

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Antidiag.Pi

Goal state before:
pp: ι : Type u_1
inst✝ : DecidableEq ι
s : Finset ι
m n : ℕ
hn : n ≠ 0
⊢ map { toFun := fun x ↦ n • x, inj' := ⋯ } (s.piAntidiag m) = {f ∈ s.piAntidiag (n * m) | ∀ i ∈ s, n ∣ f i}

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Antidiag.Pi

Goal state before:
pp: ι : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m n : ℕ
hn : n ≠ 0
⊢ n • univ.piAntidiag m = {f ∈ univ.piAntidiag (n * m) | ∀ (i : ι), n ∣ f i}

Tactic:
by

Goal state after: