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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X✝ Y✝ : Cᵒᵖ
f : X✝ ⟶ Y✝
⊢ (f.unop ≫ 𝟙 (unop X✝)).op = f

Tactic:
comp_id,

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X✝ Y✝ : Cᵒᵖ
f : X✝ ⟶ Y✝
⊢ f.unop.op = f
Module: Mathlib.CategoryTheory.Pi.Basic

Goal state before:
pp: I : Type w₀
J✝ : Type w₁
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
J : Type w₁
K : Type w₂
f : K → J
g : J → I
X Y : (i : I) → C i
f' : X ⟶ Y
⊢ ((comap C g ⋙ comap (C ∘ g) f).map f' ≫ fun b ↦ 𝟙 (Y (g (f b)))) =
    (fun b ↦ 𝟙 (X (g (f b)))) ≫ (comap C (g ∘ f)).map f'

Tactic:
by simp only [comap, Function.comp]; funext; simp

Goal state after:
Module: Mathlib.CategoryTheory.Discrete.Basic

Goal state before:
pp: α : Type u₁
C : Type u₂
inst✝ : Category.{v₂, u₂} C
I : Type u₁
F : I → C
X Y : Discrete I
f : X ⟶ Y
⊢ (F ∘ as) X ⟶ (F ∘ as) Y

Tactic:
dsimp
    rcases f with ⟨⟨h⟩⟩
    exact eqToHom (congrArg _ h)

Goal state after:
Module: Mathlib.CategoryTheory.Pi.Basic

Goal state before:
pp: I : Type w₀
J✝ : Type w₁
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
J : Type w₁
K : Type w₂
f : K → J
g : J → I
X Y : (i : I) → C i
f' : X ⟶ Y
⊢ ((comap C (g ∘ f)).map f' ≫ fun b ↦ 𝟙 (Y (g (f b)))) =
    (fun b ↦ 𝟙 (X (g (f b)))) ≫ (comap C g ⋙ comap (C ∘ g) f).map f'

Tactic:
by simp only [comap, Function.comp]; funext; simp

Goal state after:
Module: Mathlib.CategoryTheory.Equivalence

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
e : C ≌ D
G : D ⥤ C
iso : e.inverse ≅ G
X : C
⊢ e.functor.map (e.unitIso.hom.app X ≫ 𝟙 (e.inverse.obj (e.functor.obj X))) ≫ e.counitIso.hom.app (e.functor.obj X) =
    𝟙 (e.functor.obj X)

Tactic:
comp_id,

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
e : C ≌ D
G : D ⥤ C
iso : e.inverse ≅ G
X : C
⊢ e.functor.map (e.unitIso.hom.app X) ≫ e.counitIso.hom.app (e.functor.obj X) = 𝟙 (e.functor.obj X)
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
P : MorphismProperty C
F : C ⥤ D
Q : MorphismProperty D
inst✝ : Q.RespectsIso
⊢ P.strictMap F ≤ Q ↔ P ≤ Q.inverseImage F

Tactic:
strictMap_le_iff_le_inverseImage

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
P : MorphismProperty C
F : C ⥤ D
Q : MorphismProperty D
inst✝ : Q.RespectsIso
⊢ P ≤ Q.inverseImage F ↔ P ≤ Q.inverseImage F
Module: Mathlib.CategoryTheory.Adjunction.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
G_obj : D → C
e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y)
he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), (e X' Y) (F.map f ≫ g) = f ≫ (e X Y) g
Y Y' Y'' : D
g : Y ⟶ Y'
g' : Y' ⟶ Y''
| (e (G_obj Y) Y').symm ((e (G_obj Y) Y') ((e (G_obj Y) Y).symm (𝟙 (G_obj Y)) ≫ g) ≫ 𝟙 (G_obj Y')) ≫ g'

Tactic:
comp_id,

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
G_obj : D → C
e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y)
he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), (e X' Y) (F.map f ≫ g) = f ≫ (e X Y) g
Y Y' Y'' : D
g : Y ⟶ Y'
g' : Y' ⟶ Y''
| (e (G_obj Y) Y').symm ((e (G_obj Y) Y') ((e (G_obj Y) Y).symm (𝟙 (G_obj Y)) ≫ g)) ≫ g'
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Cᵒᵖ ⥤ Type v
Y : C
e : {X : C} → (X ⟶ Y) ≃ F.obj (op X)
he : ∀ {X X' : C} (f : X ⟶ X') (g : X' ⟶ Y), e (f ≫ g) = (ConcreteCategory.hom (F.map f.op)) (e g)
e' : {X : C} → (X ⟶ Y) ≃ F.obj (op X)
he' : ∀ {X X' : C} (f : X ⟶ X') (g : X' ⟶ Y), e' (f ≫ g) = (ConcreteCategory.hom (F.map f.op)) (e' g)
h : { homEquiv := e, homEquiv_comp := he }.homEquiv (𝟙 Y) = { homEquiv := e', homEquiv_comp := he' }.homEquiv (𝟙 Y)
this :
  ∀ {X : C} (f : X ⟶ Y),
    { homEquiv := e, homEquiv_comp := he }.homEquiv f = { homEquiv := e', homEquiv_comp := he' }.homEquiv f
x✝¹ : C
x✝ : x✝¹ ⟶ Y
⊢ e x✝ = e' x✝

Tactic:
apply this

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : C ⥤ Type v
X : C
e : {Y : C} → (X ⟶ Y) ≃ F.obj Y
he : ∀ {Y Y' : C} (g : Y ⟶ Y') (f : X ⟶ Y), e (f ≫ g) = (ConcreteCategory.hom (F.map g)) (e f)
e' : {Y : C} → (X ⟶ Y) ≃ F.obj Y
he' : ∀ {Y Y' : C} (g : Y ⟶ Y') (f : X ⟶ Y), e' (f ≫ g) = (ConcreteCategory.hom (F.map g)) (e' f)
h : { homEquiv := e, homEquiv_comp := he }.homEquiv (𝟙 X) = { homEquiv := e', homEquiv_comp := he' }.homEquiv (𝟙 X)
this :
  ∀ {Y : C} (f : X ⟶ Y),
    { homEquiv := e, homEquiv_comp := he }.homEquiv f = { homEquiv := e', homEquiv_comp := he' }.homEquiv f
x✝¹ : C
x✝ : X ⟶ x✝¹
⊢ e x✝ = e' x✝

Tactic:
apply this

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Basic

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a : B
⊢ (λ_ (𝟙 a)).inv = (ρ_ (𝟙 a)).inv

Tactic:
simp [Iso.inv_eq_inv]

Goal state after:
Module: Mathlib.CategoryTheory.EssentiallySmall

Goal state before:
pp: case mp.left
C : Type u
inst✝ : Category.{v, u} C
h : EssentiallySmall.{w, v, u} C
⊢ Small.{w, u} (Skeleton C)

pp: case mp.right
C : Type u
inst✝ : Category.{v, u} C
h : EssentiallySmall.{w, v, u} C
⊢ LocallySmall.{w, v, u} C

Tactic:
· rcases h with ⟨S, 𝒮, ⟨e⟩⟩
      refine ⟨⟨Skeleton S, ⟨?_⟩⟩⟩
      exact e.skeletonEquiv

Goal state after:
case mp.right
C : Type u
inst✝ : Category.{v, u} C
h : EssentiallySmall.{w, v, u} C
⊢ LocallySmall.{w, v, u} C
Module: Mathlib.CategoryTheory.EssentiallySmall

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Small.{w, u} C
inst✝ : LocallySmall.{w, v, u} C
⊢ Small.{w, max u v} (Arrow C)

Tactic:
let φ (f : Arrow C) : Σ (s t : C), s ⟶ t := ⟨_, _, f.hom⟩
  refine small_of_injective (f := φ) ?_
  rintro ⟨s, t, f⟩ ⟨s', t', f'⟩ h
  obtain rfl : s = s' := congr_arg Sigma.fst h
  simp only [Sigma.mk.injEq, heq_eq_eq, true_and, φ] at h
  obtain rfl : t = t' := h.1
  obtain rfl : f = f' := by simpa using h
  rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.HasLimits

Goal state before:
pp: J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F : J ⥤ C
inst✝¹ : HasLimit F
G : K ⥤ C
inst✝ : HasLimit G
e : J ≌ K
w : e.functor ⋙ G ≅ F
k : K
⊢ (isoOfEquivalence e w).hom ≫ limit.π G k =
    limit.π F (e.inverse.obj k) ≫ w.inv.app (e.inverse.obj k) ≫ G.map (e.counit.app k)

Tactic:
by
  simp only [HasLimit.isoOfEquivalence, IsLimit.conePointsIsoOfEquivalence_hom]
  simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.HasLimits

Goal state before:
pp: J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
F : J ⥤ C
inst✝¹ : HasLimit F
G : C ⥤ D
inst✝ : HasLimit (F ⋙ G)
j : J
⊢ post F G ≫ π (F ⋙ G) j = G.map (π F j)

Tactic:
simp [limit.post]

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

Goal state before:
pp: β : Type w
α : Type w₂
C : Type u
inst✝¹ : Category.{v, u} C
f : α → C
g : β → C
inst✝ : HasCoproduct f
e : β ≃ α
iso : (j : β) → g j ≅ f (e j)
⊢ HasCoproduct g

Tactic:
by
  have α : Discrete.functor g ≅ (Discrete.equivalence e).functor ⋙ Discrete.functor f :=
    Discrete.natIso (fun ⟨j⟩ => iso j)
  exact hasColimit_of_iso α

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

Goal state before:
pp: case refine_3
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝ : Category.{v, u} C
ι : Type u_1
ι' : Type u_2
X : ι → ι' → C
c : (i : ι) → Cofan fun j ↦ X i j
hc : (i : ι) → IsColimit (c i)
c' : Cofan fun i ↦ (c i).pt
hc' : IsColimit c'
t : Cofan fun p ↦ X p.1 p.2
m : (Cofan.mk c'.pt fun p ↦ (c p.1).inj p.2 ≫ c'.inj p.1).pt ⟶ t.pt
hm : ∀ (j : ι × ι'), (Cofan.mk c'.pt fun p ↦ (c p.1).inj p.2 ≫ c'.inj p.1).inj j ≫ m = t.inj j
⊢ m = desc hc' fun i ↦ desc (hc i) fun j ↦ t.inj (i, j)

Tactic:
· refine Cofan.IsColimit.hom_ext hc' _ _ fun i ↦ ?_
    exact Cofan.IsColimit.hom_ext (hc i) _ _ fun j ↦ (by simpa using hm (i, j))

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S : D
T : C ⥤ D
f : StructuredArrow S T
⊢ f.homMk' (𝟙 f.right) = eqToHom ⋯

Tactic:
simp [eqToHom_right]

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S : D
Y' Y'' : C
T : C ⥤ D
f : StructuredArrow S T
g : f.right ⟶ Y'
g' : Y' ⟶ Y''
⊢ f.homMk' (g ≫ g') = f.homMk' g ≫ (mk (f.hom ≫ T.map g)).homMk' g' ≫ eqToHom ⋯

Tactic:
simp [eqToHom_right]

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
⊢ Hom.right ((mapId Y).hom.app x✝) = Hom.right (eqToHom ⋯)

Tactic:
simp [eqToHom_right]

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
T T' T'' : D
Y Y' Y'' : C
S S' : C ⥤ D
A : Type u₃
inst✝¹ : Category.{v₃, u₃} A
B : Type u₄
inst✝ : Category.{v₄, u₄} B
U : A ⥤ B
V : B
F : C ⥤ A
G : D ⥤ B
α : F ⋙ U ⟶ S ⋙ G
β : G.obj T ⟶ V
F' : C ⥤ A
G' : D ⥤ B
e₁ : F ≅ F'
e₂ : G ≅ G'
α' : F' ⋙ U ⟶ S ⋙ G'
β' : G'.obj T ⟶ V
hα : α ≫ S.whiskerLeft e₂.hom = Functor.whiskerRight e₁.hom U ≫ α'
hβ : β = e₂.hom.app T ≫ β'
X : CostructuredArrow S T
⊢ U.map (e₁.app X.left).hom ≫ ((map₂ α' β').obj X).hom = ((map₂ α β).obj X).hom

Tactic:
subst hβ

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
T T' T'' : D
Y Y' Y'' : C
S S' : C ⥤ D
A : Type u₃
inst✝¹ : Category.{v₃, u₃} A
B : Type u₄
inst✝ : Category.{v₄, u₄} B
U : A ⥤ B
V : B
F : C ⥤ A
G : D ⥤ B
α : F ⋙ U ⟶ S ⋙ G
F' : C ⥤ A
G' : D ⥤ B
e₁ : F ≅ F'
e₂ : G ≅ G'
α' : F' ⋙ U ⟶ S ⋙ G'
β' : G'.obj T ⟶ V
hα : α ≫ S.whiskerLeft e₂.hom = Functor.whiskerRight e₁.hom U ≫ α'
X : CostructuredArrow S T
⊢ U.map (e₁.app X.left).hom ≫ ((map₂ α' β').obj X).hom = ((map₂ α (e₂.hom.app T ≫ β')).obj X).hom
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
T T' T'' : D
Y Y' Y'' : C
S S' : C ⥤ D
A : Type u₃
inst✝¹ : Category.{v₃, u₃} A
B : Type u₄
inst✝ : Category.{v₄, u₄} B
U : A ⥤ B
V : B
F : C ⥤ A
G : D ⥤ B
α : F ⋙ U ⟶ S ⋙ G
β : G.obj T ⟶ V
F' : C ⥤ A
G' : D ⥤ B
e₁ : F ≅ F'
e₂ : G ≅ G'
α' : F' ⋙ U ⟶ S ⋙ G'
β' : G'.obj T ⟶ V
hα : α ≫ S.whiskerLeft e₂.hom = Functor.whiskerRight e₁.hom U ≫ α'
hβ : β = e₂.hom.app T ≫ β'
X : CostructuredArrow S T
⊢ U.map (e₁.app X.left).hom ≫ ((map₂ α' β').obj X).hom = ((map₂ α β).obj X).hom

pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
T T' T'' : D
Y Y' Y'' : C
S S' : C ⥤ D
A : Type u₃
inst✝¹ : Category.{v₃, u₃} A
B : Type u₄
inst✝ : Category.{v₄, u₄} B
U : A ⥤ B
V : B
F : C ⥤ A
G : D ⥤ B
α : F ⋙ U ⟶ S ⋙ G
β : G.obj T ⟶ V
F' : C ⥤ A
G' : D ⥤ B
e₁ : F ≅ F'
e₂ : G ≅ G'
α' : F' ⋙ U ⟶ S ⋙ G'
β' : G'.obj T ⟶ V
hα : α ≫ S.whiskerLeft e₂.hom = Functor.whiskerRight e₁.hom U ≫ α'
hβ : β = e₂.hom.app T ≫ β'
⊢ ∀ {X Y : CostructuredArrow S T} (f : X ⟶ Y),
    (map₂ α β).map f ≫ (isoMk (e₁.app Y.left) ⋯).hom = (isoMk (e₁.app X.left) ⋯).hom ≫ (map₂ α' β').map f

Tactic:
· subst hβ
    simp [← reassoc_of% dsimp% congr($(hα).app X.left)]
  · simp

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
F : C ⥤ D
inst✝¹ : F.Full
inst✝ : F.Faithful
X : C
hX : IsZero (F.obj X)
h : F.FullyFaithful
this : (Y : C) → Unique (F.obj X ⟶ F.obj Y)
⊢ IsZero X

Tactic:
have (Y : C) := (hX.unique_from (F.obj Y)).some

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
F : C ⥤ D
inst✝¹ : F.Full
inst✝ : F.Faithful
X : C
hX : IsZero (F.obj X)
h : F.FullyFaithful
this✝ : (Y : C) → Unique (F.obj X ⟶ F.obj Y)
this : (Y : C) → Unique (F.obj Y ⟶ F.obj X)
⊢ IsZero X
Module: Mathlib.CategoryTheory.Limits.Shapes.Images

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
X Y : C
f f' : X ⟶ Y
inst✝² : HasImage f
inst✝¹ : HasImage f'
inst✝ : HasEqualizers C
h : f = f'
⊢ ι f = (eqToIso h).hom ≫ ι f'

Tactic:
apply image.ext
  subst h
  simp [asIso, image.eqToIso, image.eqToHom]

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✝
P : C
ι : P ⟶ X✝
w : ι ≫ f✝ = ι ≫ g
X Y : WalkingParallelPair
f : X ⟶ Y
⊢ ((Functor.const WalkingParallelPair).obj P).map f ≫
      WalkingParallelPair.casesOn (motive := fun t ↦
        Y = t → (((Functor.const WalkingParallelPair).obj P).obj Y ⟶ (parallelPair f✝ g).obj Y)) Y (fun h ↦ ⋯ ▸ ι)
        (fun h ↦ ⋯ ▸ ι ≫ f✝) ⋯ =
    WalkingParallelPair.casesOn (motive := fun t ↦
        X = t → (((Functor.const WalkingParallelPair).obj P).obj X ⟶ (parallelPair f✝ g).obj X)) X (fun h ↦ ⋯ ▸ ι)
        (fun h ↦ ⋯ ▸ ι ≫ f✝) ⋯ ≫
      (parallelPair f✝ g).map f

Tactic:
cases X <;> cases Y <;> cases f <;> simp [w]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
f : X ⟶ Y
c : CokernelCofork f
hc : IsColimit c
h : IsZero c.pt
R✝ : C
g : Y ⟶ R✝
hg : f ≫ g = 0
⊢ g = 0

Tactic:
obtain ⟨a, ha⟩ := CokernelCofork.IsColimit.desc' hc _ hg

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
f : X ⟶ Y
c : CokernelCofork f
hc : IsColimit c
h : IsZero c.pt
R✝ : C
g : Y ⟶ R✝
hg : f ≫ g = 0
a : c.pt ⟶ R✝
ha : Cofork.π c ≫ a = g
⊢ g = 0
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
D : Type u'
inst✝² : Category.{v, u'} D
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : F.IsEquivalence
app : (j : WalkingParallelPair) → (parallelPair f 0 ⋙ F).obj j ≅ (parallelPair (F.map f) 0).obj j :=
  fun j ↦
    match j with
    | zero => Iso.refl ((parallelPair f 0 ⋙ F).obj zero)
    | one => Iso.refl ((parallelPair f 0 ⋙ F).obj one)
⊢ ∀ {X_1 Y_1 : WalkingParallelPair} (f_1 : X_1 ⟶ Y_1),
    (parallelPair f 0 ⋙ F).map f_1 ≫ (app Y_1).hom = (app X_1).hom ≫ (parallelPair (F.map f) 0).map f_1

Tactic:
by rintro ⟨i⟩ ⟨j⟩ <;> rintro (g | g) <;> aesop

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
Z : C
l : X ⟶ Z
i : Z ≅ Y
h : l ≫ i.hom = f
s : KernelFork f
hs : IsLimit s
⊢ Fork.ι s ≫ l = 0

Tactic:
simp [← i.comp_inv_eq.2 h.symm]

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
inst✝ : HasKernel f
Z : C
l : X ⟶ Z
i : Z ≅ Y
h : l ≫ i.hom = f
⊢ ι f ≫ l = 0

Tactic:
simp [← i.comp_inv_eq.2 h.symm]

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 g : J → C
inst✝² : HasBiproduct f
inst✝¹ : HasBiproduct g
p : (j : J) → f j ⟶ g j
inst✝ : ∀ (j : J), Mono (p j)
⊢ Mono (map p)

Tactic:
by
  rw [show Sigma.map p = (biproduct.isoCoproduct _).inv ≫ biproduct.map p ≫
    (biproduct.isoCoproduct _).hom by aesop]
  infer_instance

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

Goal state before:
pp: case neg.h
J : Type w
K : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f : J → C
g : K → C
e : J ≃ K
w : (j : J) → g (e j) ≅ f j
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
k : K
j : J
h : ¬k = e j
⊢ e j ≠ k

Tactic:
exact Ne.symm h

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

Goal state before:
pp: J : Type w
K : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f : J → C
g : K → C
e : J ≃ K
w : (j : J) → g (e j) ≅ f j
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
⊢ (whiskerEquiv e w).inv = lift fun j ↦ π g (e j) ≫ (w j).hom

Tactic:
by
  simp only [whiskerEquiv_inv]
  ext j k
  by_cases h : k = e j
  · subst h
    simp only [ι_desc_assoc, ← eqToHom_iso_hom_naturality_assoc w (e.symm_apply_apply j).symm,
      Equiv.symm_apply_apply, eqToHom_comp_ι, Category.assoc, bicone_ι_π_self, Category.comp_id,
      lift_π, bicone_ι_π_self_assoc]
  · simp only [ι_desc_assoc, Category.assoc, lift_π]
    rw [biproduct.ι_π_ne, biproduct.ι_π_ne_assoc]
    · simp
    · exact h
    · rintro rfl
      simp at h

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
t : BinaryBicone X Y
ht : IsColimit t.toCocone
⊢ t.snd = BinaryCofan.IsColimit.desc ht 0 (𝟙 Y)

Tactic:
by
  apply ht.uniq (BinaryCofan.mk 0 (𝟙 Y))
  rintro ⟨⟨⟩⟩ <;> 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 : IsLimit b.fstKernelFork
T : C
f : T ⟶ X
g : T ⟶ Y
m : T ⟶ b.pt
h₁ : m ≫ BinaryFan.fst b.toCone = f
h₂ : m ≫ BinaryFan.snd b.toCone = g
h₁' : (m - (f ≫ b.inl + g ≫ b.inr)) ≫ b.fst = 0
h₂' : (m - (f ≫ b.inl + g ≫ b.inr)) ≫ b.snd = 0
q : T ⟶ Y
hq : q ≫ b.inr = m - (f ≫ b.inl + g ≫ b.inr)
⊢ ((m - (f ≫ b.inl + g ≫ b.inr)) ≫ b.snd) ≫ b.inr = 0

Tactic:
h₂',

Goal state after:
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 : IsLimit b.fstKernelFork
T : C
f : T ⟶ X
g : T ⟶ Y
m : T ⟶ b.pt
h₁ : m ≫ BinaryFan.fst b.toCone = f
h₂ : m ≫ BinaryFan.snd b.toCone = g
h₁' : (m - (f ≫ b.inl + g ≫ b.inr)) ≫ b.fst = 0
h₂' : (m - (f ≫ b.inl + g ≫ b.inr)) ≫ b.snd = 0
q : T ⟶ Y
hq : q ≫ b.inr = m - (f ≫ b.inl + g ≫ b.inr)
⊢ 0 ≫ b.inr = 0
Module: Mathlib.Order.Fin.Tuple

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Type u_1
x₀ y₀ : α 0
x y : (i : Fin n) → α i.succ
s : {i : Fin n.succ} → α i → α i → Prop
⊢ ((∀ (j : Fin n.succ), j < 0 → cons x₀ x j = cons y₀ y j) ∧ s (cons x₀ x 0) (cons y₀ y 0) ∨
      ∃ i, (∀ (j : Fin n.succ), j < i.succ → cons x₀ x j = cons y₀ y j) ∧ s (x i) (y i)) ↔
    s x₀ y₀ ∨ x₀ = y₀ ∧ ∃ i, (∀ (j : Fin n), j < i → x j = y j) ∧ s (x i) (y i)

Tactic:
Fin.cons_zero,

Goal state after:
n : ℕ
α : Fin (n + 1) → Type u_1
x₀ y₀ : α 0
x y : (i : Fin n) → α i.succ
s : {i : Fin n.succ} → α i → α i → Prop
⊢ ((∀ (j : Fin n.succ), j < 0 → cons x₀ x j = cons y₀ y j) ∧ s x₀ y₀ ∨
      ∃ i, (∀ (j : Fin n.succ), j < i.succ → cons x₀ x j = cons y₀ y j) ∧ s (x i) (y i)) ↔
    s x₀ y₀ ∨ x₀ = y₀ ∧ ∃ i, (∀ (j : Fin n), j < i → x j = y j) ∧ s (x i) (y i)
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
m : b.pt ⟶ T
h₁ : BinaryCofan.inl b.toCocone ≫ m = f
h₂ : BinaryCofan.inr b.toCocone ≫ m = g
h₁' : b.inl ≫ (m - (b.fst ≫ f + b.snd ≫ g)) = 0
h₂' : b.inr ≫ (m - (b.fst ≫ f + b.snd ≫ g)) = 0
q : Y ⟶ T
hq : b.snd ≫ q = m - (b.fst ≫ f + b.snd ≫ g)
⊢ b.snd ≫ b.inr ≫ (m - (b.fst ≫ f + b.snd ≫ g)) = 0

Tactic:
h₂',

Goal state after:
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
m : b.pt ⟶ T
h₁ : BinaryCofan.inl b.toCocone ≫ m = f
h₂ : BinaryCofan.inr b.toCocone ≫ m = g
h₁' : b.inl ≫ (m - (b.fst ≫ f + b.snd ≫ g)) = 0
h₂' : b.inr ≫ (m - (b.fst ≫ f + b.snd ≫ g)) = 0
q : Y ⟶ T
hq : b.snd ≫ q = m - (b.fst ≫ f + b.snd ≫ g)
⊢ b.snd ≫ 0 = 0
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
  refine ⟨fun h ↦ ⟨fun a b hab ↦ ?_, ⟨fun i hlt ↦ ?_, fun i hlt ↦ ?_⟩⟩, ?_⟩
  · simpa [hab] using h (a := q.succAbove a) (b := q.succAbove b)
  · have : q.succAbove i < q := by simp [succAbove_of_castSucc_lt, hlt]
    simpa using h this
  · have : q < q.succAbove i := by simp [succAbove_of_le_castSucc, hlt, ← le_castSucc_iff]
    simpa using h this
  · rintro ⟨h, hlt, hgt⟩ a b hab
    cases a using succAboveCases q <;> cases b using succAboveCases q
    · simp at hab
    · rename_i j
      have : q ≤ j.castSucc := by simpa [lt_succAbove_iff_le_castSucc] using hab
      simpa using hgt _ this
    · rename_i j
      have : j.castSucc < q := by simpa [succAbove_lt_iff_castSucc_lt] using hab
      simpa using hlt _ this
    · simpa using h <| (strictMono_succAbove _).lt_iff_lt.mp hab

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

Goal state before:
pp: case succ.right.succ
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)
⊢ Pairwise (Function.onFun Disjoint fun ni ↦ map (fun x ↦ Fin.cons ni.1 x) (antidiagonalTuple k ni.2))
    (antidiagonal (n + 1))

Tactic:
rw [List.Nat.antidiagonal_succ]
    refine List.Pairwise.cons (fun a ha x hx₁ hx₂ => ?_) (n_ih.map _ fun a b h x hx₁ hx₂ => ?_)
    · rw [List.mem_map] at hx₁ hx₂ ha
      obtain ⟨⟨a, -, rfl⟩, ⟨x₁, -, rfl⟩, ⟨x₂, -, h⟩⟩ := ha, hx₁, hx₂
      rw [Fin.cons_inj] at h
      injection h.1
    · rw [List.mem_map] at hx₁ hx₂
      obtain ⟨⟨x₁, hx₁, rfl⟩, ⟨x₂, hx₂, h₁₂⟩⟩ := hx₁, hx₂
      dsimp at h₁₂
      rw [Fin.cons_inj, Nat.succ_inj] at h₁₂
      obtain ⟨h₁₂, rfl⟩ := h₁₂
      rw [Function.onFun, h₁₂] at h
      exact h (List.mem_map_of_mem hx₁) (List.mem_map_of_mem hx₂)

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

Goal state before:
pp: n : ℕ
c : Composition n
j : ℕ
h : j < n
⊢ ∃ i, j < c.sizeUpTo (i + 1) ∧ i < c.length

Tactic:
have length_pos := length_pos_of_sum_pos (blocks c) (h.pos.trans_eq c.blocks_sum.symm)
  refine ⟨_, ?_, Nat.pred_lt length_pos.ne'⟩
  have : c.length - 1 + 1 = c.length := Nat.succ_pred_eq_of_pos length_pos
  simp [this, h]

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

Goal state before:
pp: n : ℕ
c : Composition n
j : Fin n
⊢ (c.embedding (c.index j)) (c.invEmbedding j) = j

Tactic:
Fin.ext_iff

Goal state after:
n : ℕ
c : Composition n
j : Fin n
⊢ ↑((c.embedding (c.index j)) (c.invEmbedding j)) = ↑j
Module: Mathlib.Combinatorics.Enumerative.Partition.Basic

Goal state before:
pp: n : ℕ
p : n.Partition
⊢ p.toFinsuppAntidiag ∈ (Finset.Icc 1 n).finsuppAntidiag n

Tactic:
have hp : p.parts.toFinset ⊆ Finset.Icc 1 n := by
    grind
  suffices ∑ m ∈ Finset.Icc 1 n, Multiset.count m p.parts * m = n by simpa [toFinsuppAntidiag, hp]
  convert! ← p.parts_sum
  rw [Finset.sum_multiset_count]
  apply Finset.sum_subset hp
  suffices ∀ (x : ℕ), 1 ≤ x → x ≤ n → x ∉ p.parts → x ∉ p.parts ∨ x = 0 by simpa
  grind

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

Goal state before:
pp: case mp
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length
h : j ∈ Set.range ⇑(c.embedding i)
k : Fin (c.blocksFun i)
hk : (c.embedding i) k = j
⊢ c.sizeUpTo ↑i ≤ ↑j ∧ ↑j < c.sizeUpTo (↑i).succ

Tactic:
Fin.ext_iff

Goal state after:
case mp
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length
h : j ∈ Set.range ⇑(c.embedding i)
k : Fin (c.blocksFun i)
hk : ↑((c.embedding i) k) = ↑j
⊢ c.sizeUpTo ↑i ≤ ↑j ∧ ↑j < c.sizeUpTo (↑i).succ