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

Goal state before:
pp: C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
A B : C
inst✝ : HasBinaryBiproduct A B
h : 𝟙 (A ⊞ B) = 0
⊢ 𝟙 A = biprod.inl ≫ 𝟙 (A ⊞ B) ≫ biprod.fst

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts

Goal state before:
pp: C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
A B : C
inst✝ : HasBinaryBiproduct A B
h : 𝟙 (A ⊞ B) = 0
⊢ 𝟙 B = biprod.inr ≫ 𝟙 (A ⊞ B) ≫ biprod.snd

Tactic:
simp

Goal state after:
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:
simp

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Basic

Goal state before:
pp: R : Type u
inst✝ : Ring R
X₁ X₂ : Type v
M N : ModuleCat R
x : ↑(AddCommGrpCat.of ↑M)
⊢ (ConcreteCategory.hom (AddCommGrpCat.ofHom { toFun := fun m ↦ 1 • m, map_zero' := ⋯, map_add' := ⋯ })) x =
    (ConcreteCategory.hom 1) x

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Basic

Goal state before:
pp: R : Type u
inst✝ : Ring R
X₁ X₂ : Type v
M N : ModuleCat R
x : ↑(AddCommGrpCat.of ↑M)
⊢ (ConcreteCategory.hom (AddCommGrpCat.ofHom { toFun := fun m ↦ 0 • m, map_zero' := ⋯, map_add' := ⋯ })) x =
    (ConcreteCategory.hom 0) x

Tactic:
simp

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
b : BinaryBicone X Y
hb : IsColimit b.inrCokernelCofork
T✝ : C
f : X ⟶ T✝
g : Y ⟶ T✝
⊢ BinaryCofan.inl b.toCocone ≫ (b.fst ≫ f + b.snd ≫ g) = f

Tactic:
simp

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
b : BinaryBicone X Y
hb : IsColimit b.inrCokernelCofork
T✝ : C
f : X ⟶ T✝
g : Y ⟶ T✝
⊢ BinaryCofan.inr b.toCocone ≫ (b.fst ≫ f + b.snd ≫ g) = g

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.AlgCat.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
A : AlgCat R
a : ↑A
⊢ (ConcreteCategory.hom (𝟙 A)) a = a

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.AlgCat.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
A B C : AlgCat R
f : A ⟶ B
g : B ⟶ C
a : ↑A
⊢ (ConcreteCategory.hom (f ≫ g)) a = (ConcreteCategory.hom g) ((ConcreteCategory.hom f) a)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.AlgCat.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
A B : AlgCat R
e : A ≅ B
x : ↑A
⊢ (ConcreteCategory.hom e.inv) ((ConcreteCategory.hom e.hom) x) = x

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.AlgCat.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
A B : AlgCat R
e : A ≅ B
x : ↑B
⊢ (ConcreteCategory.hom e.hom) ((ConcreteCategory.hom e.inv) x) = x

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.AlgCat.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
X₁ X₂ : Type v
X Y : AlgCat R
i : X ≅ Y
x : ↑X
⊢ (ConcreteCategory.hom i.inv) ((ConcreteCategory.hom i.hom) x) = x

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.AlgCat.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
X₁ X₂ : Type v
X Y : AlgCat R
i : X ≅ Y
x : ↑Y
⊢ (ConcreteCategory.hom i.hom) ((ConcreteCategory.hom i.inv) x) = x

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts

Goal state before:
pp: C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
P Q : C
⊢ (braiding P Q).hom ≫ (braiding Q P).hom = 𝟙 (P ⊞ Q)

Tactic:
simp

Goal state after:
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 y : R) (b : ↑(mkOfSMul' φ)), (x * y) • b = x • y • b

Tactic:
simp

Goal state after:
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
⊢ ∀ (b : ↑(mkOfSMul' φ)), 1 • b = b

Tactic:
simp

Goal state after:
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' φ)
⊢ (x✝² + x✝¹) • x✝ = x✝² • x✝ + x✝¹ • x✝

Tactic:
simp

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.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 : ↑(mkOfSMul' φ)), 0 • x = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.AlgCat.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
X₁ X₂ : Type v
A : AlgCat ℤ
x✝ : ℤ
⊢ (RingEquiv.refl ↑A) ((algebraMap ℤ ↑A) x✝) = (algebraMap ℤ ↑((forget₂ (AlgCat ℤ) RingCat).obj A)) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Basic

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
G : ModuleCat R
H : Type u
inst✝¹ : AddCommGroup H
inst✝ : Module R H
f : ↑G →ₗ[R] H
⊢ f ∘ₗ Hom.hom (𝟙 G) = f

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Basic

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
G : Type u
inst✝¹ : AddCommGroup G
inst✝ : Module R G
H : ModuleCat R
f : G →ₗ[R] ↑H
⊢ Hom.hom (𝟙 H) ∘ₗ f = f

Tactic:
simp

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
b : BinaryBicone X Y
hb : IsColimit b.inlCokernelCofork
T✝ : C
f : X ⟶ T✝
g : Y ⟶ T✝
⊢ BinaryCofan.inl b.toCocone ≫ (b.fst ≫ f + b.snd ≫ g) = f

Tactic:
simp

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
b : BinaryBicone X Y
hb : IsColimit b.inlCokernelCofork
T✝ : C
f : X ⟶ T✝
g : Y ⟶ T✝
⊢ BinaryCofan.inr b.toCocone ≫ (b.fst ≫ f + b.snd ≫ g) = g

Tactic:
simp

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 ≫ (𝟙 X - (𝟙 X - f ≫ section_ f)) = 0

Tactic:
simp

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) ⋯
⊢ 𝟙 X - (𝟙 X - f ≫ section_ f) = f ≫ section_ f

Tactic:
simp

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:
simp

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:
simp

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:
simp

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:
simp

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:
simp

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:
simp

Goal state after:
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:
simp

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:
simp

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:
simp

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:
simp

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

Goal state before:
pp: case h₀.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₁₁
⊢ (biprod.inl ≫
        (unipotentLower (-f₂₁ ≫ inv f₁₁)).hom ≫ ofComponents f₁₁ f₁₂ f₂₁ f₂₂ ≫ (unipotentUpper (-inv f₁₁ ≫ f₁₂)).hom) ≫
      biprod.fst =
    (biprod.inl ≫ biprod.map f₁₁ (f₂₂ - f₂₁ ≫ inv f₁₁ ≫ f₁₂)) ≫ biprod.fst

Tactic:
simp

Goal state after:
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₁₁
⊢ (biprod.inl ≫
        (unipotentLower (-f₂₁ ≫ inv f₁₁)).hom ≫ ofComponents f₁₁ f₁₂ f₂₁ f₂₂ ≫ (unipotentUpper (-inv f₁₁ ≫ f₁₂)).hom) ≫
      biprod.snd =
    (biprod.inl ≫ biprod.map f₁₁ (f₂₂ - f₂₁ ≫ inv f₁₁ ≫ f₁₂)) ≫ biprod.snd

Tactic:
simp

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

Goal state before:
pp: case h₁.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₁₁
⊢ (biprod.inr ≫
        (unipotentLower (-f₂₁ ≫ inv f₁₁)).hom ≫ ofComponents f₁₁ f₁₂ f₂₁ f₂₂ ≫ (unipotentUpper (-inv f₁₁ ≫ f₁₂)).hom) ≫
      biprod.fst =
    (biprod.inr ≫ biprod.map f₁₁ (f₂₂ - f₂₁ ≫ inv f₁₁ ≫ f₁₂)) ≫ biprod.fst

Tactic:
simp

Goal state after:
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₁₁
⊢ (biprod.inr ≫
        (unipotentLower (-f₂₁ ≫ inv f₁₁)).hom ≫ ofComponents f₁₁ f₁₂ f₂₁ f₂₂ ≫ (unipotentUpper (-inv f₁₁ ≫ f₁₂)).hom) ≫
      biprod.snd =
    (biprod.inr ≫ biprod.map f₁₁ (f₂₂ - f₂₁ ≫ inv f₁₁ ≫ f₁₂)) ≫ biprod.snd

Tactic:
simp

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 elim0.succ
k n✝ : ℕ
⊢ Fin.elim0 ∈ antidiagonalTuple 0 (n✝ + 1) ↔ ∑ i, i.elim0 = n✝ + 1

Tactic:
simp

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

Goal state before:
pp: case zero.zero
⊢ (antidiagonalTuple 0 0).Nodup

Tactic:
simp

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

Goal state before:
pp: case zero.succ
n✝ : ℕ
⊢ (antidiagonalTuple 0 (n✝ + 1)).Nodup

Tactic:
simp

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:
simp

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:
simp

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:
simp

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

Goal state before:
pp: case zero
k : ℕ
⊢ Pairwise
    (fun a₁ a₂ ↦
      ∀ a ∈ antidiagonalTuple k a₁.2,
        ∀ a_2 ∈ antidiagonalTuple k a₂.2,
          a₁.1 < a₂.1 ∨ a₁.1 = a₂.1 ∧ Pi.Lex (fun x1 x2 ↦ x1 < x2) (fun i x1 x2 ↦ x1 < x2) a a_2)
    (antidiagonal 0)

Tactic:
antidiagonal_zero

Goal state after:
case zero
k : ℕ
⊢ Pairwise
    (fun a₁ a₂ ↦
      ∀ a ∈ antidiagonalTuple k a₁.2,
        ∀ a_2 ∈ antidiagonalTuple k a₂.2,
          a₁.1 < a₂.1 ∨ a₁.1 = a₂.1 ∧ Pi.Lex (fun x1 x2 ↦ x1 < x2) (fun i x1 x2 ↦ x1 < x2) a a_2)
    [(0, 0)]
Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal

Goal state before:
pp: case succ
k n : ℕ
n_ih :
  Pairwise
    (fun a₁ a₂ ↦
      ∀ a ∈ antidiagonalTuple k a₁.2,
        ∀ a_2 ∈ antidiagonalTuple k a₂.2,
          a₁.1 < a₂.1 ∨ a₁.1 = a₂.1 ∧ Pi.Lex (fun x1 x2 ↦ x1 < x2) (fun i x1 x2 ↦ x1 < x2) a a_2)
    (antidiagonal n)
⊢ Pairwise
    (fun a₁ a₂ ↦
      ∀ a ∈ antidiagonalTuple k a₁.2,
        ∀ a_2 ∈ antidiagonalTuple k a₂.2,
          a₁.1 < a₂.1 ∨ a₁.1 = a₂.1 ∧ Pi.Lex (fun x1 x2 ↦ x1 < x2) (fun i x1 x2 ↦ x1 < x2) a a_2)
    (antidiagonal (n + 1))

Tactic:
simp

Goal state after:
case succ
k n : ℕ
n_ih :
  Pairwise
    (fun a₁ a₂ ↦
      ∀ a ∈ antidiagonalTuple k a₁.2,
        ∀ a_2 ∈ antidiagonalTuple k a₂.2,
          a₁.1 < a₂.1 ∨ a₁.1 = a₂.1 ∧ Pi.Lex (fun x1 x2 ↦ x1 < x2) (fun i x1 x2 ↦ x1 < x2) a a_2)
    (antidiagonal n)
⊢ (∀ (a b x x_1 : ℕ),
      x + x_1 = n →
        x + 1 = a →
          x_1 = b →
            ∀ a_4 ∈ antidiagonalTuple k (n + 1),
              ∀ a_6 ∈ antidiagonalTuple k b,
                0 < a ∨ 0 = a ∧ Pi.Lex (fun x1 x2 ↦ x1 < x2) (fun i x1 x2 ↦ x1 < x2) a_4 a_6) ∧
    Pairwise
      (fun a₁ a₂ ↦
        ∀ a ∈ antidiagonalTuple k a₁.2,
          ∀ a_2 ∈ antidiagonalTuple k a₂.2,
            a₁.1 < a₂.1 ∨ a₁.1 = a₂.1 ∧ Pi.Lex (fun x1 x2 ↦ x1 < x2) (fun i x1 x2 ↦ x1 < x2) a a_2)
      (map (Prod.map Nat.succ id) (antidiagonal n))
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:
simp

Goal state after:
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:
simp

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: n : ℕ
c : Composition n
⊢ c.length = 0 ↔ n = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: n : ℕ
c : Composition n
i : ℕ
h : i < c.length
⊢ c.sizeUpTo i < c.sizeUpTo i + c.blocks[i]

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Partition.Basic

Goal state before:
pp: n : ℕ
σ : Type u_1
τ : Type u_2
inst✝¹ : DecidableEq σ
inst✝ : DecidableEq τ
x✝ : Partition 0
⊢ x✝.parts = default.parts

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Partition.Basic

Goal state before:
pp: n : ℕ
σ : Type u_1
τ : Type u_2
inst✝¹ : DecidableEq σ
inst✝ : DecidableEq τ
x✝ : Partition 1
⊢ x✝.parts = default.parts

Tactic:
simp

Goal state after:
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:
simp

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Partition.Basic

Goal state before:
pp: n✝ : ℕ
σ : Type u_1
τ : Type u_2
inst✝¹ : DecidableEq σ
inst✝ : DecidableEq τ
n a : ℕ
ha1 : 1 ≤ a
ha : a ≤ n
q : (n - a).Partition
⊢ a ∈ { parts := a ::ₘ q.parts, parts_pos := ⋯, parts_sum := ⋯ }.parts

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
l : List (Perm α)
h1 : 1 ∉ l
h2 : List.Pairwise Disjoint l
⊢ l.Nodup

Tactic:
by
  grind [List.Pairwise.imp_of_mem, disjoint_refl_iff]

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

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Preadditive C
D : Type u'
inst✝⁴ : Category.{v', u'} D
inst✝³ : Preadditive D
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
J : Type u_1
inst✝¹ : Finite J
f : J → C
inst✝ : PreservesBiproduct f F
c✝ : Cone (Discrete.functor f)
hc : IsLimit c✝
val✝ : Fintype J
as✝ : J
⊢ ((Cone.postcompose (Discrete.compNatIsoDiscrete f F).inv).obj (F.mapBicone (Bicone.ofLimitCone hc)).toCone).π.app
      { as := as✝ } =
    (Iso.refl
          ((Cone.postcompose (Discrete.compNatIsoDiscrete f F).inv).obj
              (F.mapBicone (Bicone.ofLimitCone hc)).toCone).pt).hom ≫
      (F.mapCone c✝).π.app { as := as✝ }

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Preadditive C
D : Type u'
inst✝⁴ : Category.{v', u'} D
inst✝³ : Preadditive D
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
J : Type u_1
inst✝¹ : Finite J
f : J → C
inst✝ : PreservesLimit (Discrete.functor f) F
b : Bicone f
hb : b.IsBilimit
val✝ : Fintype J
as✝ : J
⊢ ((Cone.postcompose (Discrete.compNatIsoDiscrete f F).hom).obj (F.mapCone b.toCone)).π.app { as := as✝ } =
    (Iso.refl ((Cone.postcompose (Discrete.compNatIsoDiscrete f F).hom).obj (F.mapCone b.toCone)).pt).hom ≫
      (F.mapBicone b).toCone.π.app { as := as✝ }

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
f : Perm (Subtype p)
h : f.IsSwap
x : α
hx : p x
y : α
hy : p y
hxy : ⟨x, hx⟩ ≠ ⟨y, hy⟩ ∧ f = swap ⟨x, hx⟩ ⟨y, hy⟩
⊢ ofSubtype (swap ⟨x, hx⟩ ⟨y, hy⟩) = swap x y

Tactic:
ofSubtype_swap_eq

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
f : Perm (Subtype p)
h : f.IsSwap
x : α
hx : p x
y : α
hy : p y
hxy : ⟨x, hx⟩ ≠ ⟨y, hy⟩ ∧ f = swap ⟨x, hx⟩ ⟨y, hy⟩
⊢ swap ↑⟨x, hx⟩ ↑⟨y, hy⟩ = swap x y
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Preadditive C
D : Type u'
inst✝⁴ : Category.{v', u'} D
inst✝³ : Preadditive D
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
J : Type u_1
inst✝¹ : Finite J
f : J → C
inst✝ : PreservesBiproduct f F
c : Cocone (Discrete.functor f)
hc : IsColimit c
val✝ : Fintype J
as✝ : J
⊢ ((Cocone.precompose (Discrete.compNatIsoDiscrete f F).hom).obj
              (F.mapBicone (Bicone.ofColimitCocone hc)).toCocone).ι.app
        { as := as✝ } ≫
      (Iso.refl
          ((Cocone.precompose (Discrete.compNatIsoDiscrete f F).hom).obj
              (F.mapBicone (Bicone.ofColimitCocone hc)).toCocone).pt).hom =
    (F.mapCocone c).ι.app { as := as✝ }

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Preadditive C
D : Type u'
inst✝⁴ : Category.{v', u'} D
inst✝³ : Preadditive D
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
J : Type u_1
inst✝¹ : Finite J
f : J → C
inst✝ : PreservesColimit (Discrete.functor f) F
b : Bicone f
hb : b.IsBilimit
val✝ : Fintype J
as✝ : J
⊢ ((Cocone.precompose (Discrete.compNatIsoDiscrete f F).inv).obj (F.mapCocone b.toCocone)).ι.app { as := as✝ } ≫
      (Iso.refl ((Cocone.precompose (Discrete.compNatIsoDiscrete f F).inv).obj (F.mapCocone b.toCocone)).pt).hom =
    (F.mapBicone b).toCocone.ι.app { as := as✝ }

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
p : Perm α
a : α
⊢ p a ∈ {x | p x ≠ x} ↔ a ∈ {x | p x ≠ x}

Tactic:
simp

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

Goal state before:
pp: case left
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : Preadditive D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
X Y : C
inst✝ : PreservesBinaryBiproduct X Y F
c : Cone (pair X Y)
hc : IsLimit c
⊢ ((Cone.postcompose (diagramIsoPair (pair X Y ⋙ F)).inv).obj
            (F.mapBinaryBicone (BinaryBicone.ofLimitCone hc)).toCone).π.app
      { as := WalkingPair.left } =
    (id (Iso.refl (F.obj c.pt))).hom ≫ (F.mapCone c).π.app { as := WalkingPair.left }

Tactic:
simp

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

Goal state before:
pp: case right
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : Preadditive D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
X Y : C
inst✝ : PreservesBinaryBiproduct X Y F
c : Cone (pair X Y)
hc : IsLimit c
⊢ ((Cone.postcompose (diagramIsoPair (pair X Y ⋙ F)).inv).obj
            (F.mapBinaryBicone (BinaryBicone.ofLimitCone hc)).toCone).π.app
      { as := WalkingPair.right } =
    (id (Iso.refl (F.obj c.pt))).hom ≫ (F.mapCone c).π.app { as := WalkingPair.right }

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: n✝ : ℕ
c : Composition n✝
n : ℕ
⊢ (replicate n 1).sum = n

Tactic:
simp

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

Goal state before:
pp: case left
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : Preadditive D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
X Y : C
inst✝ : PreservesLimit (pair X Y) F
b : BinaryBicone X Y
hb : b.IsBilimit
⊢ ((Cone.postcompose (diagramIsoPair (pair X Y ⋙ F)).hom).obj (F.mapCone b.toCone)).π.app { as := WalkingPair.left } =
    (id (Iso.refl (F.obj b.pt))).hom ≫ (F.mapBinaryBicone b).toCone.π.app { as := WalkingPair.left }

Tactic:
simp

Goal state after: