mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝ : Category.{v₁, u₁} T
Y : T
x✝ : Under Y
⊢ (map (𝟙 Y)).obj x✝ = (𝟭 (Under Y)).obj x✝

Tactic:
by simp [map, Comma.mapLeft]; rfl

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝ : Category.{v₁, u₁} T
Y : T
x✝ : Under Y
⊢ (mapId Y).hom.app x✝ = eqToHom ⋯

Tactic:
by ext; simp [eqToHom_right]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback

Goal state before:
pp: case h₁
C : Type u
inst✝³ : Category.{v, u} C
W X✝ Y✝ Z✝ X Y : C
f : X ⟶ Y
Z : C
inst✝² : HasBinaryProduct Y Z
inst✝¹ : HasBinaryProduct X Z
inst✝ : HasPullback f prod.fst
⊢ (prod.lift (pullback.fst f prod.fst) (pullback.snd f prod.fst ≫ prod.snd) ≫
        pullback.lift prod.fst (prod.map f (𝟙 Z)) ⋯) ≫
      pullback.snd f prod.fst =
    𝟙 (pullback f prod.fst) ≫ pullback.snd f prod.fst

Tactic:
apply prod.hom_ext

Goal state after:
case h₁.h₁
C : Type u
inst✝³ : Category.{v, u} C
W X✝ Y✝ Z✝ X Y : C
f : X ⟶ Y
Z : C
inst✝² : HasBinaryProduct Y Z
inst✝¹ : HasBinaryProduct X Z
inst✝ : HasPullback f prod.fst
⊢ ((prod.lift (pullback.fst f prod.fst) (pullback.snd f prod.fst ≫ prod.snd) ≫
          pullback.lift prod.fst (prod.map f (𝟙 Z)) ⋯) ≫
        pullback.snd f prod.fst) ≫
      prod.fst =
    (𝟙 (pullback f prod.fst) ≫ pullback.snd f prod.fst) ≫ prod.fst

case h₂
C : Type u
inst✝³ : Category.{v, u} C
W X✝ Y✝ Z✝ X Y : C
f : X ⟶ Y
Z : C
inst✝² : HasBinaryProduct Y Z
inst✝¹ : HasBinaryProduct X Z
inst✝ : HasPullback f prod.fst
⊢ ((prod.lift (pullback.fst f prod.fst) (pullback.snd f prod.fst ≫ prod.snd) ≫
          pullback.lift prod.fst (prod.map f (𝟙 Z)) ⋯) ≫
        pullback.snd f prod.fst) ≫
      prod.snd =
    (𝟙 (pullback f prod.fst) ≫ pullback.snd f prod.fst) ≫ prod.snd
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback

Goal state before:
pp: case h₀
C : Type u
inst✝³ : Category.{v, u} C
W X✝ Y✝ Z✝ X Y : C
f : X ⟶ Y
Z : C
inst✝² : HasBinaryProduct Z Y
inst✝¹ : HasBinaryProduct Z X
inst✝ : HasPullback prod.snd f
⊢ (prod.lift (pullback.fst prod.snd f ≫ prod.fst) (pullback.snd prod.snd f) ≫
        pullback.lift (prod.map (𝟙 Z) f) prod.snd ⋯) ≫
      pullback.fst prod.snd f =
    𝟙 (pullback prod.snd f) ≫ pullback.fst prod.snd f

Tactic:
apply prod.hom_ext

Goal state after:
case h₀.h₁
C : Type u
inst✝³ : Category.{v, u} C
W X✝ Y✝ Z✝ X Y : C
f : X ⟶ Y
Z : C
inst✝² : HasBinaryProduct Z Y
inst✝¹ : HasBinaryProduct Z X
inst✝ : HasPullback prod.snd f
⊢ ((prod.lift (pullback.fst prod.snd f ≫ prod.fst) (pullback.snd prod.snd f) ≫
          pullback.lift (prod.map (𝟙 Z) f) prod.snd ⋯) ≫
        pullback.fst prod.snd f) ≫
      prod.fst =
    (𝟙 (pullback prod.snd f) ≫ pullback.fst prod.snd f) ≫ prod.fst

case h₂
C : Type u
inst✝³ : Category.{v, u} C
W X✝ Y✝ Z✝ X Y : C
f : X ⟶ Y
Z : C
inst✝² : HasBinaryProduct Z Y
inst✝¹ : HasBinaryProduct Z X
inst✝ : HasPullback prod.snd f
⊢ ((prod.lift (pullback.fst prod.snd f ≫ prod.fst) (pullback.snd prod.snd f) ≫
          pullback.lift (prod.map (𝟙 Z) f) prod.snd ⋯) ≫
        pullback.fst prod.snd f) ≫
      prod.snd =
    (𝟙 (pullback prod.snd f) ≫ pullback.fst prod.snd f) ≫ prod.snd
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : Epi f
t : PushoutCocone f f
ht : IsColimit t
⊢ IsIso t.inl

Tactic:
refine ⟨⟨PushoutCocone.IsColimit.desc ht (𝟙 _) (𝟙 _) (by simp), by simp, ?_⟩⟩
  apply PushoutCocone.IsColimit.hom_ext ht
  · simp
  · simp [inl_eq_inr_of_epi_eq]

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

Goal state before:
pp: C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
s : Fork f g
W : C
k l : W ⟶ s.pt
h : k ≫ s.ι = l ≫ s.ι
⊢ k ≫ s.π.app one = l ≫ s.π.app one

Tactic:
have : k ≫ ι s ≫ f = l ≫ ι s ≫ f := by
      simp only [← Category.assoc]; exact congrArg (· ≫ f) h
    rw [s.app_one_eq_ι_comp_left, this]

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

Goal state before:
pp: C : Type u
X✝ Y : C
inst✝ : Category.{v, u} C
f✝ g : X✝ ⟶ Y
X : C
f : X ⟶ X
hf : f ≫ f = f
c : Fork (𝟙 X) f
i : IsLimit c
⊢ c.ι ≫ i.lift (Fork.ofι f ⋯) = 𝟙 c.pt

Tactic:
let := mono_of_isLimit_fork i

Goal state after:
C : Type u
X✝ Y : C
inst✝ : Category.{v, u} C
f✝ g : X✝ ⟶ Y
X : C
f : X ⟶ X
hf : f ≫ f = f
c : Fork (𝟙 X) f
i : IsLimit c
this : Mono c.ι := mono_of_isLimit_fork i
⊢ c.ι ≫ i.lift (Fork.ofι f ⋯) = 𝟙 c.pt
Module: Mathlib.CategoryTheory.Preadditive.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
P Q R S : C
J : Type u_1
s : Finset J
f : J → (P ⟶ Q)
g : J → (Q ⟶ R)
h : R ⟶ S
⊢ (∑ j ∈ s, f j ≫ g j) ≫ h = ∑ j ∈ s, f j ≫ g j ≫ h

Tactic:
by
  simp only [← Category.assoc]
  apply sum_comp

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.CompleteLattice

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
α : Sort u_1
P : α → ObjectProperty C
⊢ ∀ (i : α), (P i).isoClosure ≤ (⨆ a, P a).isoClosure

Tactic:
intro a

Goal state after:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
α : Sort u_1
P : α → ObjectProperty C
a : α
⊢ (P a).isoClosure ≤ (⨆ a, P a).isoClosure
Module: Mathlib.CategoryTheory.ObjectProperty.CompleteLattice

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
α : Sort u_1
P : α → ObjectProperty C
X : C
inst✝ : ∀ (a : α), (P a).IsClosedUnderIsomorphisms
X✝ Y✝ : C
e : X✝ ≅ Y✝
h : ∀ (i : α), P i X✝
⊢ ∀ (i : α), P i Y✝

Tactic:
intro a

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
α : Sort u_1
P : α → ObjectProperty C
X : C
inst✝ : ∀ (a : α), (P a).IsClosedUnderIsomorphisms
X✝ Y✝ : C
e : X✝ ≅ Y✝
h : ∀ (i : α), P i X✝
a : α
⊢ P a Y✝
Module: Mathlib.CategoryTheory.Limits.Preserves.Finite

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : ReflectsLimitsOfSize.{w, w₂, v₁, v₂, u₁, u₂} F
J : Type
sJ : SmallCategory J
fJ : FinCategory J
⊢ ReflectsLimitsOfShape J F

Tactic:
have := reflectsSmallestLimits_of_reflectsLimits F
    exact reflectsLimitsOfShape_of_equiv (FinCategory.equivAsType J) F

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.BinaryProducts

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
inst✝¹ : HasBinaryCoproduct X Y
inst✝ : HasBinaryCoproduct (G.obj X) (G.obj Y)
i : IsIso (coprodComparison G X Y)
⊢ IsColimit (G.mapCocone (BinaryCofan.mk coprod.inl coprod.inr))

Tactic:
apply (isColimitMapCoconeBinaryCofanEquiv _ _ _).symm _

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
inst✝¹ : HasBinaryCoproduct X Y
inst✝ : HasBinaryCoproduct (G.obj X) (G.obj Y)
i : IsIso (coprodComparison G X Y)
⊢ IsColimit (BinaryCofan.mk (G.map coprod.inl) (G.map coprod.inr))
Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
X Y : C
f g : X ⟶ Y
inst✝¹ : HasKernel f
inst✝ : HasKernel g
h : f = g
⊢ (kernelIsoOfEq h).hom ≫ kernel.ι g = kernel.ι f

Tactic:
subst h; simp

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
X Y : C
f g : X ⟶ Y
inst✝¹ : HasKernel f
inst✝ : HasKernel g
h : f = g
⊢ (kernelIsoOfEq h).inv ≫ kernel.ι f = kernel.ι g

Tactic:
subst h; simp

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
X Y Z : C
f g : X ⟶ Y
inst✝¹ : HasKernel f
inst✝ : HasKernel g
h : f = g
e : Z ⟶ X
he : e ≫ f = 0
⊢ kernel.lift f e he ≫ (kernelIsoOfEq h).hom = kernel.lift g e ⋯

Tactic:
subst h; simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
c : CokernelCofork f
i : IsColimit c
W : C
g : W ⟶ X
hg : Epi g
h : W ⟶ Y
hh : h = g ≫ f
s : Cofork h 0
⊢ (g ≫ f) ≫ s.π = g ≫ 0 ≫ s.π

Tactic:
← hh,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
c : CokernelCofork f
i : IsColimit c
W : C
g : W ⟶ X
hg : Epi g
h : W ⟶ Y
hh : h = g ≫ f
s : Cofork h 0
⊢ h ≫ s.π = g ≫ 0 ≫ s.π
Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts

Goal state before:
pp: case pos
J : Type w
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f g : J → C
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
p : (b : J) → f b ⟶ g b
j✝¹ j✝ : J
h : j✝ = j✝¹
⊢ eqToHom ⋯ ≫ p j✝¹ = p j✝ ≫ eqToHom ⋯

Tactic:
subst h; simp

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

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : Category.{v_2, u_2} D
inst✝⁷ : Category.{v_3, u_3} E
inst✝⁶ : Preadditive C
inst✝⁵ : Preadditive D
inst✝⁴ : Preadditive E
F : C ⥤ D
inst✝³ : F.Additive
inst✝² : F.Full
inst✝¹ : F.EssSurj
G : D ⥤ E
inst✝ : (F ⋙ G).Additive
X Y : D
f g : X ⟶ Y
f' : F.objPreimage X ⟶ F.objPreimage Y
hf' : F.map f' = (F.objObjPreimageIso X).hom ≫ f ≫ (F.objObjPreimageIso Y).inv
g' : F.objPreimage X ⟶ F.objPreimage Y
hg' : F.map g' = (F.objObjPreimageIso X).hom ≫ g ≫ (F.objObjPreimageIso Y).inv
⊢ G.map (F.map f' + F.map g') = G.map (F.map (f' + g'))

Tactic:
F.map_add

Goal state after:
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : Category.{v_2, u_2} D
inst✝⁷ : Category.{v_3, u_3} E
inst✝⁶ : Preadditive C
inst✝⁵ : Preadditive D
inst✝⁴ : Preadditive E
F : C ⥤ D
inst✝³ : F.Additive
inst✝² : F.Full
inst✝¹ : F.EssSurj
G : D ⥤ E
inst✝ : (F ⋙ G).Additive
X Y : D
f g : X ⟶ Y
f' : F.objPreimage X ⟶ F.objPreimage Y
hf' : F.map f' = (F.objObjPreimageIso X).hom ≫ f ≫ (F.objObjPreimageIso Y).inv
g' : F.objPreimage X ⟶ F.objPreimage Y
hg' : F.map g' = (F.objObjPreimageIso X).hom ≫ g ≫ (F.objObjPreimageIso Y).inv
⊢ G.map (F.map f' + F.map g') = G.map (F.map f' + F.map g')
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
J : Type
inst✝¹ : Fintype J
inst✝ : HasFiniteBiproducts C
f g : J → C
h : (j : J) → f j ⟶ g j
⊢ map h = ∑ j, π f j ≫ h j ≫ ι g j

Tactic:
classical
  ext
  simp [biproduct.ι_π, biproduct.ι_π_assoc, sum_comp, comp_dite, dite_comp]

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

Goal state before:
pp: case pos
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
β γ : Type
inst✝² : Finite β
ε : β ≃ γ
f : γ → C
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct (f ∘ ⇑ε)
b b' : β
h : b' = b
⊢ ι (f ∘ ⇑ε) b' ≫ ((desc fun b ↦ ι f (ε b)) ≫ lift fun b ↦ π f (ε b)) ≫ π (f ∘ ⇑ε) b =
    ι (f ∘ ⇑ε) b' ≫ 𝟙 (⨁ f ∘ ⇑ε) ≫ π (f ∘ ⇑ε) b

Tactic:
subst h; simp

Goal state after:
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
f : J → C
i : J
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct (Subtype.restrict (fun j ↦ j ≠ i) f)
s : Fork (π f i) 0
⊢ (s.ι ≫ toSubtype f fun j ↦ j ≠ i) ≫ Fork.ι (KernelFork.ofι (fromSubtype f fun j ↦ j ≠ i) ⋯) = s.ι

Tactic:
by
      apply biproduct.hom_ext; intro j
      rw [KernelFork.ι_ofι, Category.assoc, Category.assoc,
        biproduct.toSubtype_fromSubtype_assoc, biproduct.map_π]
      rcases Classical.em (i = j) with (rfl | h)
      · rw [if_neg (Classical.not_not.2 rfl), comp_zero, comp_zero, KernelFork.condition]
      · rw [if_pos (Ne.symm h), Category.comp_id]

Goal state after:
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
K : Type
inst✝¹ : Finite K
inst✝ : HasFiniteBiproducts C
f : K → C
p : K → Prop
j : Subtype pᶜ
k : Subtype p
⊢ (if h : (p ↑k)ᶜ then biproduct.ι (Subtype.restrict pᶜ f) ⟨↑k, h⟩ else 0) ≫ biproduct.π (Subtype.restrict pᶜ f) j = 0

Tactic:
dif_neg

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
K : Type
inst✝¹ : Finite K
inst✝ : HasFiniteBiproducts C
f : K → C
p : K → Prop
j : Subtype pᶜ
k : Subtype p
⊢ 0 ≫ biproduct.π (Subtype.restrict pᶜ f) j = 0

case hnc
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
K : Type
inst✝¹ : Finite K
inst✝ : HasFiniteBiproducts C
f : K → C
p : K → Prop
j : Subtype pᶜ
k : Subtype p
⊢ ¬(p ↑k)ᶜ
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:
intro a

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_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:
intro a

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.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 ≫ i.lift (Fork.ofι (Fork.ofι (𝟙 X - f ≫ section_ f) ⋯).ι ⋯) = 0

Tactic:
let := mono_of_isLimit_fork i

Goal state after:
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
this : Mono (Fork.ι c) := mono_of_isLimit_fork i
⊢ section_ f ≫ i.lift (Fork.ofι (Fork.ofι (𝟙 X - f ≫ section_ f) ⋯).ι ⋯) = 0
Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal

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

Tactic:
| zero =>

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

Goal state before:
pp: case succ.left
k : ℕ
ih : ∀ (n : ℕ), (antidiagonalTuple k n).Nodup
n : ℕ
i : ℕ × ℕ
a✝ : i ∈ antidiagonal n
⊢ (map (fun x ↦ Fin.cons i.1 x) (antidiagonalTuple k i.2)).Nodup

Tactic:
exact (ih i.snd).map (Fin.cons_right_injective (α := fun _ => ℕ) i.fst)

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

Goal state before:
pp: case succ.right.zero
k : ℕ
ih : ∀ (n : ℕ), (antidiagonalTuple k n).Nodup
⊢ Pairwise (Function.onFun Disjoint fun ni ↦ map (fun x ↦ Fin.cons ni.1 x) (antidiagonalTuple k ni.2)) (antidiagonal 0)

Tactic:
| zero =>

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

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

Tactic:
simp_rw [antidiagonalTuple, antidiagonal, List.range_succ, List.map_append, List.map_singleton,
    Nat.sub_self, List.flatMap_append, List.flatMap_singleton, List.flatMap_map]
  conv_rhs => rw [← List.nil_append [![n]]]
  congr 1
  simp_rw [List.flatMap_eq_nil_iff, List.mem_range, List.map_eq_nil_iff]
  intro x hx
  obtain ⟨m, rfl⟩ := Nat.exists_eq_add_of_lt hx
  rw [add_assoc, add_tsub_cancel_left, antidiagonalTuple_zero_succ]

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:
| zero =>

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

Goal state before:
pp: case mpr
n : ℕ
c : Composition n
⊢ n = 0 → c.blocks = []

Tactic:
· rintro rfl
    rw [← length_eq_zero_iff, ← nonpos_iff_eq_zero]
    exact c.length_le

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

Goal state before:
pp: α : Type u_1
f g : Perm α
h : f.Disjoint g
x : α
hg : g x = x
hf : f (f x) = f x
⊢ (f * g) x = (g * f) x

Tactic:
by simp [mul_apply, f.injective hf, hg]

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

Goal state before:
pp: α : Type u_1
f : Perm α
x : α
hfx : f x = x
n : ℕ
⊢ (f ^ Int.negSucc n) x = x

Tactic:
by rw [zpow_negSucc, inv_eq_iff_eq, pow_apply_eq_self_of_apply_eq_self hfx]

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 μ
a : ι
s : Finset ι
h : a ∉ s
n : μ
⊢ (insert a s).finsuppAntidiag n =
    (antidiagonal n).biUnion fun p ↦
      map { toFun := fun f ↦ (↑f).update a p.1, inj' := ⋯ } (s.finsuppAntidiag p.2).attach

Tactic:
ext f
  rw [mem_finsuppAntidiag_insert h, mem_biUnion]
  simp_rw [mem_map, mem_attach, true_and, Subtype.exists, Embedding.coeFn_mk, exists_prop, and_comm,
    eq_comm]

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 t : Finset ι
h : s ⊆ t
n : μ
⊢ s.finsuppAntidiag n ⊆ t.finsuppAntidiag n

Tactic:
intro a

Goal state after:
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
s t : Finset ι
h : s ⊆ t
n : μ
a : ι →₀ μ
⊢ a ∈ s.finsuppAntidiag n → a ∈ t.finsuppAntidiag n
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: case mp.left
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), g x ∈ s ↔ x ∈ s
h : ∀ (x : α), (ofSubtype (g.subtypePerm hg)) x = c x
⊢ c.support ⊆ s

Tactic:
intro a

Goal state after:
case mp.left
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), g x ∈ s ↔ x ∈ s
h : ∀ (x : α), (ofSubtype (g.subtypePerm hg)) x = c x
a : α
⊢ a ∈ c.support → a ∈ s
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: case insert
α : Type u_2
β : Type u_3
inst✝¹ : DecidableEq β
inst✝ : Fintype β
f : α → Perm β
x : β
⊢ ∀ (a : α) (s : Finset α),
    a ∉ s →
      (∀ {comm : (↑s).Pairwise (Commute on f)}, (∀ a ∈ s, x ∉ (f a).support) → x ∉ (s.noncommProd f comm).support) →
        ∀ {comm : (↑(insert a s)).Pairwise (Commute on f)},
          (∀ a_3 ∈ insert a s, x ∉ (f a_3).support) → x ∉ ((insert a s).noncommProd f comm).support

Tactic:
intro a

Goal state after:
case insert
α : Type u_2
β : Type u_3
inst✝¹ : DecidableEq β
inst✝ : Fintype β
f : α → Perm β
x : β
a : α
⊢ ∀ (s : Finset α),
    a ∉ s →
      (∀ {comm : (↑s).Pairwise (Commute on f)}, (∀ a ∈ s, x ∉ (f a).support) → x ∉ (s.noncommProd f comm).support) →
        ∀ {comm : (↑(insert a s)).Pairwise (Commute on f)},
          (∀ a_3 ∈ insert a s, x ∉ (f a_3).support) → x ∉ ((insert a s).noncommProd f comm).support
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: case zero
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : ∀ x ∈ f.support ∩ g.support, f x = g x
⊢ ∀ x ∈ f.support ∩ g.support, (f ^ 0) x = (g ^ 0) x

Tactic:
| zero =>

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

Goal state before:
pp: n✝ n : ℕ
s : Finset (Fin (n - 1))
i : Fin (n - 1)
this : ↑i + 1 ≠ n
⊢ (∃ j ∈ s, i = j) ↔ i ∈ s

Tactic:
exists_eq_right'

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

Goal state before:
pp: case zero
n : ℕ
c : CompositionAsSet n
h : 0 < c.boundaries.card
⊢ (take 0 c.blocks).sum = ↑(c.boundary ⟨0, h⟩)

Tactic:
| zero =>

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l l' : List α
x✝ : α
h : x✝ ∈ {x | (zipWith Equiv.swap l l').prod x ≠ x}
⊢ x✝ ∈ ↑(l.toFinset ⊔ l'.toFinset)

Tactic:
simpa using mem_or_mem_of_zipWith_swap_prod_ne h

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

Goal state before:
pp: case zero
α : Type u_1
inst✝ : DecidableEq α
xs : List α
h : xs.Nodup
hn : 0 + 1 < xs.length
⊢ xs.formPerm xs[0] = xs[0 + 1]

Tactic:
| zero =>

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

Goal state before:
pp: case zero
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
⊢ (l.rotate 0).formPerm = l.formPerm

Tactic:
| zero =>

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

Goal state before:
pp: case zero
α : Type u_1
inst✝ : DecidableEq α
l : List α
w : l.Nodup
i : ℕ
h : i < l.length
⊢ (l.formPerm ^ 0) l[i] = l[(i + 0) % l.length]

Tactic:
| zero =>

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

Goal state before:
pp: case h.h.zero
α : Type u_1
inst✝ : DecidableEq α
x y x' y' : α
l l' : List α
hd : (x :: y :: l).Nodup
hd' : (x' :: y' :: l').Nodup
h : ∀ (x_1 : α), (x :: y :: l).formPerm x_1 = (x' :: y' :: l').formPerm x_1
hx : x' ∈ x :: y :: l
n : ℕ
hn : n < (x :: y :: l).length
hx' : (x :: y :: l).get ⟨n, hn⟩ = x'
hl : (x :: y :: l).length = (x' :: y' :: l').length
hk : 0 < ((x :: y :: l).rotate n).length
hk' : 0 < (x' :: y' :: l').length
⊢ (x :: y :: l)[(0 + n) % (x :: y :: l).length] = (x' :: y' :: l')[0]

Tactic:
| zero =>

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

Goal state before:
pp: case zero
n : ℕ
i : Fin (n + 1)
ne : i ≠ 0
lt : i < 0
⊢ swap i 0 ∈ ↑(Submonoid.closure (Set.range fun i ↦ swap i.castSucc i.succ))

Tactic:
| zero =>

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

Goal state before:
pp: case inr.inl
n : ℕ
a₁ : Fin (n + 2)
H : 0 < a₁
ha₂ : ⟨a₁, 0⟩ ∉ {⟨1, 0⟩}
ha₁ : 0 < a₁
⊢ (if (swap 0 1) a₁ ≤ (swap 0 1) 0 then -1 else 1) = 1

Tactic:
simp only [and_true, heq_iff_eq, mem_singleton, Sigma.mk.inj_iff] at ha₂

Goal state after:
case inr.inl
n : ℕ
a₁ : Fin (n + 2)
H : 0 < a₁
ha₁ : 0 < a₁
ha₂ : ¬a₁ = 1
⊢ (if (swap 0 1) a₁ ≤ (swap 0 1) 0 then -1 else 1) = 1