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

Goal state before:
pp: case refine_1
J✝¹ : Type w
C✝¹ : Type uC
inst✝¹⁰ : Category.{uC', uC} C✝¹
inst✝⁹ : HasZeroMorphisms C✝¹
D✝ : Type uD
inst✝⁸ : Category.{uD', uD} D✝
inst✝⁷ : HasZeroMorphisms D✝
F : J✝¹ → C✝¹
J✝ : Type w
K : Type u_1
C✝ : Type u
inst✝⁶ : Category.{v, u} C✝
inst✝⁵ : HasZeroMorphisms C✝
J : Type w
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
D : Type uD
inst✝² : Category.{uD', uD} D
inst✝¹ : HasZeroMorphisms D
inst✝ : HasFiniteBiproducts C
X : C
a : ⨁ Empty.elim ⟶ X
⊢ a = default

Tactic:
;

Goal state after:
case refine_1
J✝¹ : Type w
C✝¹ : Type uC
inst✝¹⁰ : Category.{uC', uC} C✝¹
inst✝⁹ : HasZeroMorphisms C✝¹
D✝ : Type uD
inst✝⁸ : Category.{uD', uD} D✝
inst✝⁷ : HasZeroMorphisms D✝
F : J✝¹ → C✝¹
J✝ : Type w
K : Type u_1
C✝ : Type u
inst✝⁶ : Category.{v, u} C✝
inst✝⁵ : HasZeroMorphisms C✝
J : Type w
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
D : Type uD
inst✝² : Category.{uD', uD} D
inst✝¹ : HasZeroMorphisms D
inst✝ : HasFiniteBiproducts C
X : C
a : ⨁ Empty.elim ⟶ X
⊢ a = default
Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts

Goal state before:
pp: case refine_1
J✝¹ : Type w
C✝¹ : Type uC
inst✝¹⁰ : Category.{uC', uC} C✝¹
inst✝⁹ : HasZeroMorphisms C✝¹
D✝ : Type uD
inst✝⁸ : Category.{uD', uD} D✝
inst✝⁷ : HasZeroMorphisms D✝
F : J✝¹ → C✝¹
J✝ : Type w
K : Type u_1
C✝ : Type u
inst✝⁶ : Category.{v, u} C✝
inst✝⁵ : HasZeroMorphisms C✝
J : Type w
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
D : Type uD
inst✝² : Category.{uD', uD} D
inst✝¹ : HasZeroMorphisms D
inst✝ : HasFiniteBiproducts C
X : C
a : ⨁ Empty.elim ⟶ X
⊢ ∀ (j : Empty), biproduct.ι Empty.elim j ≫ a = biproduct.ι Empty.elim j ≫ default

Tactic:
;

Goal state after:
case refine_1
J✝¹ : Type w
C✝¹ : Type uC
inst✝¹⁰ : Category.{uC', uC} C✝¹
inst✝⁹ : HasZeroMorphisms C✝¹
D✝ : Type uD
inst✝⁸ : Category.{uD', uD} D✝
inst✝⁷ : HasZeroMorphisms D✝
F : J✝¹ → C✝¹
J✝ : Type w
K : Type u_1
C✝ : Type u
inst✝⁶ : Category.{v, u} C✝
inst✝⁵ : HasZeroMorphisms C✝
J : Type w
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
D : Type uD
inst✝² : Category.{uD', uD} D
inst✝¹ : HasZeroMorphisms D
inst✝ : HasFiniteBiproducts C
X : C
a : ⨁ Empty.elim ⟶ X
⊢ ∀ (j : Empty), biproduct.ι Empty.elim j ≫ a = biproduct.ι Empty.elim j ≫ default
Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts

Goal state before:
pp: case refine_2
J✝¹ : Type w
C✝¹ : Type uC
inst✝¹⁰ : Category.{uC', uC} C✝¹
inst✝⁹ : HasZeroMorphisms C✝¹
D✝ : Type uD
inst✝⁸ : Category.{uD', uD} D✝
inst✝⁷ : HasZeroMorphisms D✝
F : J✝¹ → C✝¹
J✝ : Type w
K : Type u_1
C✝ : Type u
inst✝⁶ : Category.{v, u} C✝
inst✝⁵ : HasZeroMorphisms C✝
J : Type w
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
D : Type uD
inst✝² : Category.{uD', uD} D
inst✝¹ : HasZeroMorphisms D
inst✝ : HasFiniteBiproducts C
X : C
a : X ⟶ ⨁ Empty.elim
⊢ a = default

Tactic:
;

Goal state after:
case refine_2
J✝¹ : Type w
C✝¹ : Type uC
inst✝¹⁰ : Category.{uC', uC} C✝¹
inst✝⁹ : HasZeroMorphisms C✝¹
D✝ : Type uD
inst✝⁸ : Category.{uD', uD} D✝
inst✝⁷ : HasZeroMorphisms D✝
F : J✝¹ → C✝¹
J✝ : Type w
K : Type u_1
C✝ : Type u
inst✝⁶ : Category.{v, u} C✝
inst✝⁵ : HasZeroMorphisms C✝
J : Type w
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
D : Type uD
inst✝² : Category.{uD', uD} D
inst✝¹ : HasZeroMorphisms D
inst✝ : HasFiniteBiproducts C
X : C
a : X ⟶ ⨁ Empty.elim
⊢ a = default
Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts

Goal state before:
pp: case refine_2
J✝¹ : Type w
C✝¹ : Type uC
inst✝¹⁰ : Category.{uC', uC} C✝¹
inst✝⁹ : HasZeroMorphisms C✝¹
D✝ : Type uD
inst✝⁸ : Category.{uD', uD} D✝
inst✝⁷ : HasZeroMorphisms D✝
F : J✝¹ → C✝¹
J✝ : Type w
K : Type u_1
C✝ : Type u
inst✝⁶ : Category.{v, u} C✝
inst✝⁵ : HasZeroMorphisms C✝
J : Type w
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
D : Type uD
inst✝² : Category.{uD', uD} D
inst✝¹ : HasZeroMorphisms D
inst✝ : HasFiniteBiproducts C
X : C
a : X ⟶ ⨁ Empty.elim
⊢ ∀ (j : Empty), a ≫ biproduct.π Empty.elim j = default ≫ biproduct.π Empty.elim j

Tactic:
;

Goal state after:
case refine_2
J✝¹ : Type w
C✝¹ : Type uC
inst✝¹⁰ : Category.{uC', uC} C✝¹
inst✝⁹ : HasZeroMorphisms C✝¹
D✝ : Type uD
inst✝⁸ : Category.{uD', uD} D✝
inst✝⁷ : HasZeroMorphisms D✝
F : J✝¹ → C✝¹
J✝ : Type w
K : Type u_1
C✝ : Type u
inst✝⁶ : Category.{v, u} C✝
inst✝⁵ : HasZeroMorphisms C✝
J : Type w
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
D : Type uD
inst✝² : Category.{uD', uD} D
inst✝¹ : HasZeroMorphisms D
inst✝ : HasFiniteBiproducts C
X : C
a : X ⟶ ⨁ Empty.elim
⊢ ∀ (j : Empty), a ≫ biproduct.π Empty.elim j = default ≫ biproduct.π Empty.elim j
Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts

Goal state before:
pp: J✝¹ : Type w
C✝¹ : Type uC
inst✝¹⁰ : Category.{uC', uC} C✝¹
inst✝⁹ : HasZeroMorphisms C✝¹
D✝ : Type uD
inst✝⁸ : Category.{uD', uD} D✝
inst✝⁷ : HasZeroMorphisms D✝
F : J✝¹ → C✝¹
J✝ : Type w
K : Type u_1
C✝ : Type u
inst✝⁶ : Category.{v, u} C✝
inst✝⁵ : HasZeroMorphisms C✝
J : Type w
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
D : Type uD
inst✝² : Category.{uD', uD} D
inst✝¹ : HasZeroMorphisms D
inst✝ : Unique J
f : J → C
j : J
⊢ default = j

Tactic:
;

Goal state after:
J✝¹ : Type w
C✝¹ : Type uC
inst✝¹⁰ : Category.{uC', uC} C✝¹
inst✝⁹ : HasZeroMorphisms C✝¹
D✝ : Type uD
inst✝⁸ : Category.{uD', uD} D✝
inst✝⁷ : HasZeroMorphisms D✝
F : J✝¹ → C✝¹
J✝ : Type w
K : Type u_1
C✝ : Type u
inst✝⁶ : Category.{v, u} C✝
inst✝⁵ : HasZeroMorphisms C✝
J : Type w
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
D : Type uD
inst✝² : Category.{uD', uD} D
inst✝¹ : HasZeroMorphisms D
inst✝ : Unique J
f : J → C
j : J
⊢ default = j
Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts

Goal state before:
pp: J✝¹ : Type w
C✝¹ : Type uC
inst✝¹⁰ : Category.{uC', uC} C✝¹
inst✝⁹ : HasZeroMorphisms C✝¹
D✝ : Type uD
inst✝⁸ : Category.{uD', uD} D✝
inst✝⁷ : HasZeroMorphisms D✝
F : J✝¹ → C✝¹
J✝ : Type w
K : Type u_1
C✝ : Type u
inst✝⁶ : Category.{v, u} C✝
inst✝⁵ : HasZeroMorphisms C✝
J : Type w
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
D : Type uD
inst✝² : Category.{uD', uD} D
inst✝¹ : HasZeroMorphisms D
inst✝ : Unique J
f : J → C
j : J
⊢ j = default

Tactic:
;

Goal state after:
J✝¹ : Type w
C✝¹ : Type uC
inst✝¹⁰ : Category.{uC', uC} C✝¹
inst✝⁹ : HasZeroMorphisms C✝¹
D✝ : Type uD
inst✝⁸ : Category.{uD', uD} D✝
inst✝⁷ : HasZeroMorphisms D✝
F : J✝¹ → C✝¹
J✝ : Type w
K : Type u_1
C✝ : Type u
inst✝⁶ : Category.{v, u} C✝
inst✝⁵ : HasZeroMorphisms C✝
J : Type w
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
D : Type uD
inst✝² : Category.{uD', uD} D
inst✝¹ : HasZeroMorphisms D
inst✝ : Unique J
f : J → C
j : J
⊢ j = default
Module: Mathlib.Algebra.Category.ModuleCat.Basic

Goal state before:
pp: R : Type u
inst✝³ : Ring R
X₁ X₂ : Type v
S₀ : Type u₀
inst✝² : CommSemiring S₀
S : Type u
inst✝¹ : Ring S
inst✝ : Algebra S₀ S
M N : ModuleCat S
x✝² : S₀
x✝¹ : S
x✝ : ↑M
⊢ (algebraMap S₀ S) x✝² • x✝¹ • x✝ = x✝² • x✝¹ • x✝

Tactic:
;

Goal state after:
R : Type u
inst✝³ : Ring R
X₁ X₂ : Type v
S₀ : Type u₀
inst✝² : CommSemiring S₀
S : Type u
inst✝¹ : Ring S
inst✝ : Algebra S₀ S
M N : ModuleCat S
x✝² : S₀
x✝¹ : S
x✝ : ↑M
⊢ (algebraMap S₀ S) x✝² • x✝¹ • x✝ = x✝² • x✝¹ • x✝
Module: Mathlib.Algebra.Category.ModuleCat.Basic

Goal state before:
pp: R : Type u
inst✝³ : Ring R
X₁ X₂ : Type v
S₀ : Type u₀
inst✝² : CommSemiring S₀
S : Type u
inst✝¹ : Ring S
inst✝ : Algebra S₀ S
M✝ N✝ x✝¹ M N : ModuleCat S
s₀ : S₀
f : x✝¹ ⟶ M
g : M ⟶ N
x✝ : ↑x✝¹
⊢ (Hom.hom ((s₀ • f) ≫ g)) x✝ = (Hom.hom (s₀ • f ≫ g)) x✝

Tactic:
;

Goal state after:
R : Type u
inst✝³ : Ring R
X₁ X₂ : Type v
S₀ : Type u₀
inst✝² : CommSemiring S₀
S : Type u
inst✝¹ : Ring S
inst✝ : Algebra S₀ S
M✝ N✝ x✝¹ M N : ModuleCat S
s₀ : S₀
f : x✝¹ ⟶ M
g : M ⟶ N
x✝ : ↑x✝¹
⊢ (Hom.hom ((s₀ • f) ≫ g)) x✝ = (Hom.hom (s₀ • f ≫ g)) x✝
Module: Mathlib.Algebra.Category.AlgCat.Basic

Goal state before:
pp: R✝ : Type u
inst✝¹ : CommRing R✝
X₁ X₂ : Type v
R : Type u_1
inst✝ : CommRing R
A : AlgCat R
x✝ : R
⊢ (RingEquiv.refl ↑((restrictScalars (RingHom.id R)).obj A))
      ((algebraMap R ↑((restrictScalars (RingHom.id R)).obj A)) x✝) =
    (algebraMap R ↑A) x✝

Tactic:
;

Goal state after:
R✝ : Type u
inst✝¹ : CommRing R✝
X₁ X₂ : Type v
R : Type u_1
inst✝ : CommRing R
A : AlgCat R
x✝ : R
⊢ (RingEquiv.refl ↑((restrictScalars (RingHom.id R)).obj A))
      ((algebraMap R ↑((restrictScalars (RingHom.id R)).obj A)) x✝) =
    (algebraMap R ↑A) x✝
Module: Mathlib.Algebra.Category.AlgCat.Basic

Goal state before:
pp: R✝ : Type u
inst✝³ : CommRing R✝
X₁ X₂ : Type v
R : Type u_1
S : Type u_2
T : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
A : AlgCat T
x✝ : R
⊢ (RingEquiv.refl ↑((restrictScalars (g.comp f)).obj A)) ((algebraMap R ↑((restrictScalars (g.comp f)).obj A)) x✝) =
    (algebraMap R ↑((restrictScalars f).obj ((restrictScalars g).obj A))) x✝

Tactic:
;

Goal state after:
R✝ : Type u
inst✝³ : CommRing R✝
X₁ X₂ : Type v
R : Type u_1
S : Type u_2
T : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
A : AlgCat T
x✝ : R
⊢ (RingEquiv.refl ↑((restrictScalars (g.comp f)).obj A)) ((algebraMap R ↑((restrictScalars (g.comp f)).obj A)) x✝) =
    (algebraMap R ↑((restrictScalars f).obj ((restrictScalars g).obj A))) x✝
Module: Mathlib.Algebra.Category.ModuleCat.Basic

Goal state before:
pp: R : Type u
inst✝ : Ring R
X₁ X₂ : Type v
M N : ModuleCat R
A : AddCommGrpCat
φ : R →+* End A
x✝² x✝¹ : R
x✝ : ↑(mkOfSMul' φ)
⊢ (ConcreteCategory.hom (φ x✝² + φ x✝¹)) x✝ = (ConcreteCategory.hom (φ x✝²)) x✝ + (ConcreteCategory.hom (φ x✝¹)) x✝

Tactic:
;

Goal state after:
R : Type u
inst✝ : Ring R
X₁ X₂ : Type v
M N : ModuleCat R
A : AddCommGrpCat
φ : R →+* End A
x✝² x✝¹ : R
x✝ : ↑(mkOfSMul' φ)
⊢ (ConcreteCategory.hom (φ x✝² + φ x✝¹)) x✝ = (ConcreteCategory.hom (φ x✝²)) x✝ + (ConcreteCategory.hom (φ x✝¹)) x✝
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
⊢ homGroup = homGroup

Tactic:
;

Goal state after:
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
⊢ homGroup = homGroup
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
⊢ homGroup X Y = homGroup X Y

Tactic:
;

Goal state after:
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
⊢ homGroup X Y = homGroup X Y
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
⊢ HAdd.hAdd = HAdd.hAdd

Tactic:
;

Goal state after:
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
⊢ HAdd.hAdd = HAdd.hAdd
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
⊢ preadditiveHasZeroMorphisms = inst✝¹

Tactic:
;

Goal state after:
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
⊢ preadditiveHasZeroMorphisms = inst✝¹
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
⊢ preadditiveHasZeroMorphisms = inst✝¹

Tactic:
;

Goal state after:
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
⊢ preadditiveHasZeroMorphisms = inst✝¹
Module: Mathlib.Order.Fin.Tuple

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

Tactic:
;

Goal state after:
n : ℕ
α : Fin (n + 1) → Type u_2
inst✝ : (i : Fin (n + 1)) → LE (α i)
x✝¹ : α 0 × ((i : Fin n) → α (succAbove 0 i))
x✝ : Fin (n + 1)
⊢ (insertNthOrderIso α 0) x✝¹ x✝ = (consOrderIso α) x✝¹ x✝
Module: Mathlib.Order.Fin.Tuple

Goal state before:
pp: n : ℕ
α : Type u_2
inst✝ : LE α
x✝¹ : α × (Fin n → α)
x✝ : Fin (n + 1)
⊢ (insertNthOrderIso (fun x ↦ α) (last n)) x✝¹ x✝ = (snocOrderIso fun x ↦ α) x✝¹ x✝

Tactic:
;

Goal state after:
n : ℕ
α : Type u_2
inst✝ : LE α
x✝¹ : α × (Fin n → α)
x✝ : Fin (n + 1)
⊢ (insertNthOrderIso (fun x ↦ α) (last n)) x✝¹ x✝ = (snocOrderIso fun x ↦ α) x✝¹ x✝
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: case h₁
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₁₁
⊢ -f₂₁ ≫ inv f₁₁ ≫ f₁₂ + f₂₂ = f₂₂ - f₂₁ ≫ inv f₁₁ ≫ f₁₂

Tactic:
;

Goal state after:
case h₁
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₁₁
⊢ -f₂₁ ≫ inv f₁₁ ≫ f₁₂ + f₂₂ = f₂₂ - f₂₁ ≫ inv f₁₁ ≫ f₁₂
Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal

Goal state before:
pp: case succ.right.succ.refine_1
k : ℕ
ih : ∀ (n : ℕ), (antidiagonalTuple k n).Nodup
n : ℕ
n_ih :
  Pairwise (Function.onFun Disjoint fun ni ↦ map (fun x ↦ Fin.cons ni.1 x) (antidiagonalTuple k ni.2)) (antidiagonal n)
a : ℕ × ℕ
x₁ x₂ : Fin k → ℕ
h : (Prod.map Nat.succ id a).1 = (0, n + 1).1 ∧ x₂ = x₁
⊢ False

Tactic:
injection h.1

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

Goal state before:
pp: case refine_2
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
n✝ : μ
s : Finset ι
n : μ
e₁ e₂ : ↥s ≃ Fin #s
f : ι → μ
g : Fin #s → μ
⊢ ∑ i, g i = n ∧ { toFun := fun f i ↦ if hi : i ∈ s then f (e₁ ⟨i, hi⟩) else 0, inj' := ⋯ } g = f ↔
    ∑ i, ((e₁.symm.trans e₂).arrowCongr (Equiv.refl μ)) g i = n ∧
      { toFun := fun f i ↦ if hi : i ∈ s then f (e₂ ⟨i, hi⟩) else 0, inj' := ⋯ }
          (((e₁.symm.trans e₂).arrowCongr (Equiv.refl μ)) g) =
        f

Tactic:
have := Fintype.sum_equiv (e₂.symm.trans e₁) _ g fun _ ↦ rfl

Goal state after:
case refine_2
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
n✝ : μ
s : Finset ι
n : μ
e₁ e₂ : ↥s ≃ Fin #s
f : ι → μ
g : Fin #s → μ
this : ∑ x, g ((e₂.symm.trans e₁) x) = ∑ x, g x
⊢ ∑ i, g i = n ∧ { toFun := fun f i ↦ if hi : i ∈ s then f (e₁ ⟨i, hi⟩) else 0, inj' := ⋯ } g = f ↔
    ∑ i, ((e₁.symm.trans e₂).arrowCongr (Equiv.refl μ)) g i = n ∧
      { toFun := fun f i ↦ if hi : i ∈ s then f (e₂ ⟨i, hi⟩) else 0, inj' := ⋯ }
          (((e₁.symm.trans e₂).arrowCongr (Equiv.refl μ)) g) =
        f
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:
simp [finsuppAntidiag, ← DFunLike.coe_fn_eq, subset_iff]

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 μ
f : ι →₀ μ
⊢ f ∈ ∅.finsuppAntidiag 0 ↔ f ∈ {0}

Tactic:
;

Goal state after:
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
f : ι →₀ μ
⊢ f ∈ ∅.finsuppAntidiag 0 ↔ f ∈ {0}
Module: Mathlib.Algebra.Order.Antidiag.Pi

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

Tactic:
;

Goal state after:
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
a✝ : ι → μ
⊢ a✝ ∈ ∅.piAntidiag 0 ↔ a✝ ∈ {0}
Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal

Goal state before:
pp: case succ.right.succ.refine_2
k : ℕ
ih : ∀ (n : ℕ), (antidiagonalTuple k n).Nodup
n : ℕ
n_ih :
  Pairwise (Function.onFun Disjoint fun ni ↦ map (fun x ↦ Fin.cons ni.1 x) (antidiagonalTuple k ni.2)) (antidiagonal n)
a b : ℕ × ℕ
h : Function.onFun Disjoint (fun ni ↦ map (fun x ↦ Fin.cons ni.1 x) (antidiagonalTuple k ni.2)) a b
x₂ : Fin k → ℕ
hx₂ : x₂ ∈ antidiagonalTuple k (Prod.map Nat.succ id b).2
h₁₂ : b.1 = a.1
hx₁ : x₂ ∈ antidiagonalTuple k (Prod.map Nat.succ id a).2
⊢ False

Tactic:
rw [Function.onFun, h₁₂] at h

Goal state after:
case succ.right.succ.refine_2
k : ℕ
ih : ∀ (n : ℕ), (antidiagonalTuple k n).Nodup
n : ℕ
n_ih :
  Pairwise (Function.onFun Disjoint fun ni ↦ map (fun x ↦ Fin.cons ni.1 x) (antidiagonalTuple k ni.2)) (antidiagonal n)
a b : ℕ × ℕ
h :
  (map (fun x ↦ Fin.cons a.1 x) (antidiagonalTuple k a.2)).Disjoint
    (map (fun x ↦ Fin.cons a.1 x) (antidiagonalTuple k b.2))
x₂ : Fin k → ℕ
hx₂ : x₂ ∈ antidiagonalTuple k (Prod.map Nat.succ id b).2
h₁₂ : b.1 = a.1
hx₁ : x₂ ∈ antidiagonalTuple k (Prod.map Nat.succ id a).2
⊢ False
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 ι
a✝ : ι → μ
⊢ a✝ ∈ s.piAntidiag 0 ↔ a✝ ∈ {0}

Tactic:
;

Goal state after:
ι : Type u_1
μ : Type u_2
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid μ
inst✝³ : PartialOrder μ
inst✝² : CanonicallyOrderedAdd μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
s : Finset ι
a✝ : ι → μ
⊢ a✝ ∈ s.piAntidiag 0 ↔ a✝ ∈ {0}
Module: Mathlib.Algebra.Order.Antidiag.Pi

Goal state before:
pp: n k : ℕ
a✝ : Fin k → ℕ
⊢ a✝ ∈ univ.piAntidiag n ↔ a✝ ∈ Nat.antidiagonalTuple k n

Tactic:
;

Goal state after:
n k : ℕ
a✝ : Fin k → ℕ
⊢ a✝ ∈ univ.piAntidiag n ↔ a✝ ∈ Nat.antidiagonalTuple k n
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
  ext f
  refine mem_smul_finset.trans ?_
  simp only [mem_filter, mem_piAntidiag, and_assoc]
  constructor
  · rintro ⟨f, rfl, hf, rfl⟩
    simpa [← mul_sum, hn] using hf
  rintro ⟨hfsum, hfsup, hfdvd⟩
  have (i : _) : n ∣ f i := by
    by_cases hi : i ∈ s
    · exact hfdvd _ hi
    · rw [not_imp_comm.1 (hfsup _) hi]
      exact dvd_zero _
  refine ⟨fun i ↦ f i / n, ?_⟩
  simp [funext_iff, Nat.mul_div_cancel', ← Nat.sum_div, *]
  grind

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
⊢ image (⇑{ toFun := fun x ↦ n • x, inj' := ⋯ }) (s.piAntidiag m) = {f ∈ s.piAntidiag (n * m) | ∀ i ∈ s, n ∣ f i}

Tactic:
;

Goal state after:
ι : Type u_1
inst✝ : DecidableEq ι
s : Finset ι
m n : ℕ
hn : n ≠ 0
⊢ image (⇑{ toFun := fun x ↦ n • x, inj' := ⋯ }) (s.piAntidiag m) = {f ∈ s.piAntidiag (n * m) | ∀ i ∈ s, n ∣ f i}
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
h₁ : x = 𝟙 W
⊢ (biprod.inl ≫ f ≫ biprod.fst ≫ biprod.inl) ≫ inv f ≫ biprod.fst + ((0 ≫ biprod.inr) ≫ inv f) ≫ biprod.fst = 0

Tactic:
simp only [zero_comp, add_zero]

Goal state after:
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
h₁ : x = 𝟙 W
⊢ (biprod.inl ≫ f ≫ biprod.fst ≫ biprod.inl) ≫ inv f ≫ biprod.fst = 0
Module: Mathlib.Combinatorics.Enumerative.Partition.Basic

Goal state before:
pp: n : ℕ
l : Multiset ℕ
hl : (filter (fun x ↦ x = 0) l).sum + (filter (fun a ↦ ¬a = 0) l).sum = n
lz : (filter (fun x ↦ x = 0) l).sum = 0
⊢ (filter (fun x ↦ x ≠ 0) l).sum = n

Tactic:
lz,

Goal state after:
n : ℕ
l : Multiset ℕ
hl : 0 + (filter (fun a ↦ ¬a = 0) l).sum = n
lz : (filter (fun x ↦ x = 0) l).sum = 0
⊢ (filter (fun x ↦ x ≠ 0) l).sum = n
Module: Mathlib.Combinatorics.Enumerative.Partition.Basic

Goal state before:
pp: case e_f
n : ℕ
σ : Type u_1
τ : Type u_2
inst✝¹ : DecidableEq σ
inst✝ : DecidableEq τ
e : σ ≃ τ
s : Sym σ n
⊢ (fun x ↦ count (e x) (map ⇑e ↑s)) = fun a ↦ count a ↑s

Tactic:
;

Goal state after:
case e_f
n : ℕ
σ : Type u_1
τ : Type u_2
inst✝¹ : DecidableEq σ
inst✝ : DecidableEq τ
e : σ ≃ τ
s : Sym σ n
⊢ (fun x ↦ count (e x) (map ⇑e ↑s)) = fun a ↦ count a ↑s
Module: Mathlib.Combinatorics.Enumerative.Partition.Basic

Goal state before:
pp: n : ℕ
σ : Type u_1
τ : Type u_2
inst✝¹ : DecidableEq σ
inst✝ : DecidableEq τ
μ : n.Partition
e : σ ≃ τ
x : { x // ofSym x = μ }
⊢ (fun x ↦ ⟨(Sym.equivCongr e.symm) ↑x, ⋯⟩) ((fun x ↦ ⟨(Sym.equivCongr e) ↑x, ⋯⟩) x) = x

Tactic:
;

Goal state after:
n : ℕ
σ : Type u_1
τ : Type u_2
inst✝¹ : DecidableEq σ
inst✝ : DecidableEq τ
μ : n.Partition
e : σ ≃ τ
x : { x // ofSym x = μ }
⊢ (fun x ↦ ⟨(Sym.equivCongr e.symm) ↑x, ⋯⟩) ((fun x ↦ ⟨(Sym.equivCongr e) ↑x, ⋯⟩) x) = x
Module: Mathlib.Combinatorics.Enumerative.Partition.Basic

Goal state before:
pp: n : ℕ
σ : Type u_1
τ : Type u_2
inst✝¹ : DecidableEq σ
inst✝ : DecidableEq τ
μ : n.Partition
e : σ ≃ τ
x : { x // ofSym x = μ }
⊢ (fun x ↦ ⟨(Sym.equivCongr e) ↑x, ⋯⟩) ((fun x ↦ ⟨(Sym.equivCongr e.symm) ↑x, ⋯⟩) x) = x

Tactic:
;

Goal state after:
n : ℕ
σ : Type u_1
τ : Type u_2
inst✝¹ : DecidableEq σ
inst✝ : DecidableEq τ
μ : n.Partition
e : σ ≃ τ
x : { x // ofSym x = μ }
⊢ (fun x ↦ ⟨(Sym.equivCongr e) ↑x, ⋯⟩) ((fun x ↦ ⟨(Sym.equivCongr e.symm) ↑x, ⋯⟩) x) = x
Module: Mathlib.Combinatorics.Enumerative.Partition.Basic

Goal state before:
pp: σ : Type u_1
inst✝ : DecidableEq σ
s : Sym σ 1
a✝ : ℕ
⊢ count a✝ (ofSym s).parts = count a✝ (indiscrete 1).parts

Tactic:
;

Goal state after:
σ : Type u_1
inst✝ : DecidableEq σ
s : Sym σ 1
a✝ : ℕ
⊢ count a✝ (ofSym s).parts = count a✝ (indiscrete 1).parts
Module: Mathlib.GroupTheory.Perm.Basic

Goal state before:
pp: α : Type u_1
f : Perm α
s : Set α
⊢ MapsTo (⇑f) s s → ∀ (n : ℕ), MapsTo (⇑f)^[n] s s

Tactic:
;

Goal state after:
α : Type u_1
f : Perm α
s : Set α
⊢ MapsTo (⇑f) s s → ∀ (n : ℕ), MapsTo (⇑f)^[n] s s
Module: Mathlib.GroupTheory.Perm.Basic

Goal state before:
pp: α : Type u_1
f : Perm α
s : Set α
⊢ SurjOn (⇑f) s s → ∀ (n : ℕ), SurjOn (⇑f)^[n] s s

Tactic:
;

Goal state after:
α : Type u_1
f : Perm α
s : Set α
⊢ SurjOn (⇑f) s s → ∀ (n : ℕ), SurjOn (⇑f)^[n] s s
Module: Mathlib.GroupTheory.Perm.Basic

Goal state before:
pp: α : Type u_1
f : Perm α
s : Set α
⊢ BijOn (⇑f) s s → ∀ (n : ℕ), BijOn (⇑f)^[n] s s

Tactic:
;

Goal state after:
α : Type u_1
f : Perm α
s : Set α
⊢ BijOn (⇑f) s s → ∀ (n : ℕ), BijOn (⇑f)^[n] s s