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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
A : C
hl : IsLimit (KernelFork.ofι (diag A) ⋯) :=
  monoIsKernelOfCokernel (colimit.cocone (parallelPair (diag A) 0)) (colimit.isColimit (parallelPair (diag A) 0))
Z : C
x : Z ⟶ A
hx : x ≫ r A = 0
hxx : (x ≫ prod.lift (𝟙 A) 0) ≫ cokernel.π (diag A) = 0
⊢ x = 0

Tactic:
obtain ⟨y, hy⟩ := KernelFork.IsLimit.lift' hl _ hxx

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
A : C
hl : IsLimit (KernelFork.ofι (diag A) ⋯) :=
  monoIsKernelOfCokernel (colimit.cocone (parallelPair (diag A) 0)) (colimit.isColimit (parallelPair (diag A) 0))
Z : C
x : Z ⟶ A
hx : x ≫ r A = 0
hxx : (x ≫ prod.lift (𝟙 A) 0) ≫ cokernel.π (diag A) = 0
y : Z ⟶ (KernelFork.ofι (diag A) ⋯).pt
hy : y ≫ Fork.ι (KernelFork.ofι (diag A) ⋯) = x ≫ prod.lift (𝟙 A) 0
⊢ x = 0
Module: Mathlib.CategoryTheory.Abelian.NonPreadditive

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a : X ⟶ Y
⊢ -a + a = 0

Tactic:
by rw [add_comm, add_neg_cancel]

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.Homology

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
h₁ : IsIso (opcyclesMap φ)
h₂ : Mono φ.τ₃
⊢ IsIso (homologyMap φ)

Tactic:
have h : (S₂.homologyι ≫ inv (opcyclesMap φ)) ≫ S₁.fromOpcycles = 0 := by
    simp only [← cancel_mono φ.τ₃, zero_comp, assoc, ← fromOpcycles_naturality,
      IsIso.inv_hom_id_assoc, homologyι_comp_fromOpcycles]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
h₁ : IsIso (opcyclesMap φ)
h₂ : Mono φ.τ₃
h : (S₂.homologyι ≫ inv (opcyclesMap φ)) ≫ S₁.fromOpcycles = 0
⊢ IsIso (homologyMap φ)
Module: Mathlib.Algebra.Homology.ShortComplex.Abelian

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Abelian C
S : ShortComplex C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : HasZeroMorphisms D
kf : KernelFork S.g
cc : CokernelCofork S.f
hkf : IsLimit kf
hcc : IsColimit cc
H : C
π : kf.pt ⟶ H
ι : H ⟶ cc.pt
fac : Fork.ι kf ≫ Cofork.π cc = π ≫ ι
inst✝¹ : Epi π
inst✝ : Mono ι
⊢ Cofork.π
        ((Cocone.precompose
              (parallelPair.ext
                  (Iso.refl
                    ((parallelPair ((hkf.ofIsoLimit (Fork.ext (Iso.refl kf.pt) ⋯)).lift (KernelFork.ofι S.f ⋯)) 0).obj
                      WalkingParallelPair.zero))
                  (S.isoCyclesOfIsLimit hkf) ⋯ ⋯).inv).obj
          (CokernelCofork.ofπ π ⋯)) ≫
      (isoHomology S hkf hcc fac).hom =
    Cofork.π (CokernelCofork.ofπ S.homologyπ ⋯)

Tactic:
by simp [Cofork.π]

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.HomologyData
⊢ S.Exact ↔ IsZero h.left.H

Tactic:
by
  have := HasHomology.mk' h
  exact LeftHomologyData.exact_iff h.left

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.Ab

Goal state before:
pp: case mp
S : ShortComplex Ab
h : (AddCommGrpCat.Hom.hom S.g).ker ≤ (AddCommGrpCat.Hom.hom S.f).range
x₁ : ↑S.X₁
⊢ (AddCommGrpCat.Hom.hom S.f) x₁ ∈ (AddCommGrpCat.Hom.hom S.g).ker

Tactic:
rw [AddMonoidHom.mem_ker, ← ConcreteCategory.comp_apply, S.zero]

Goal state after:
case mp
S : ShortComplex Ab
h : (AddCommGrpCat.Hom.hom S.g).ker ≤ (AddCommGrpCat.Hom.hom S.f).range
x₁ : ↑S.X₁
⊢ (ConcreteCategory.hom 0) x₁ = 0
Module: Mathlib.Algebra.Homology.ShortComplex.Ab

Goal state before:
pp: case mpr
S : ShortComplex Ab
⊢ (AddCommGrpCat.Hom.hom S.f).range = (AddCommGrpCat.Hom.hom S.g).ker →
    (AddCommGrpCat.Hom.hom S.g).ker ≤ (AddCommGrpCat.Hom.hom S.f).range

Tactic:
intro h
    rw [h]

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
S : ShortComplex C
inst✝¹ : S.HasHomology
inst✝ : HasKernel S.g
⊢ S.Exact ↔ Epi (kernel.lift S.g S.f ⋯)

Tactic:
exact_iff_epi_toCycles

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
S : ShortComplex C
inst✝¹ : S.HasHomology
inst✝ : HasKernel S.g
⊢ Epi S.toCycles ↔ Epi (kernel.lift S.g S.f ⋯)
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
hS : IsLimit (KernelFork.ofι S.f ⋯)
inst✝ : S.HasHomology
⊢ S.Exact

Tactic:
exact_iff_epi_toCycles

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
hS : IsLimit (KernelFork.ofι S.f ⋯)
inst✝ : S.HasHomology
⊢ Epi S.toCycles
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Preadditive C
inst✝¹ : Preadditive D
S : ShortComplex C
s : S.Splitting
F : C ⥤ D
inst✝ : F.Additive
⊢ F.map s.s ≫ (S.map F).g = 𝟙 (S.map F).X₃

Tactic:
by
    dsimp [ShortComplex.map]
    simp only [← F.map_comp, s_g, F.map_id]

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
inst✝⁴ : Balanced C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₂ : S₂.Exact
inst✝³ : Epi S₁.g
inst✝² : Epi S₂.g
inst✝¹ : Epi φ.τ₁
inst✝ : Epi φ.τ₃
⊢ Epi φ.τ₂

Tactic:
have : Mono S₁.op.f := by dsimp; infer_instance

Goal state after:
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
inst✝⁴ : Balanced C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₂ : S₂.Exact
inst✝³ : Epi S₁.g
inst✝² : Epi S₂.g
inst✝¹ : Epi φ.τ₁
inst✝ : Epi φ.τ₃
this : Mono S₁.op.f
⊢ Epi φ.τ₂
Module: Mathlib.CategoryTheory.Subobject.MonoOver

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasImages C
f g : Over X
k : f ⟶ g
⊢ imageMonoOver f.hom ⟶ imageMonoOver g.hom

Tactic:
apply (forget X).preimage _

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasImages C
f g : Over X
k : f ⟶ g
⊢ (forget X).obj (imageMonoOver f.hom) ⟶ (forget X).obj (imageMonoOver g.hom)
Module: Mathlib.CategoryTheory.Subobject.Lattice

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasImages C
inst✝ : HasBinaryCoproducts C
A : C
f g : MonoOver A
⊢ f ⟶ (sup.obj f).obj g

Tactic:
refine homMk (coprod.inl ≫ factorThruImage _) ?_
  erw [Category.assoc, image.fac, coprod.inl_desc]
  rfl

Goal state after:
Module: Mathlib.CategoryTheory.Subobject.Lattice

Goal state before:
pp: case refine_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
A : C
f g : Subobject A
s : PullbackCone f.arrow g.arrow
⊢ (f ⊓ g).Factors (s.fst ≫ f.arrow)

pp: case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
A : C
f g : Subobject A
⊢ ∀ (s : PullbackCone f.arrow g.arrow), (f ⊓ g).factorThru (s.fst ≫ f.arrow) ⋯ ≫ (f ⊓ g).ofLE f ⋯ = s.fst

pp: case refine_3
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
A : C
f g : Subobject A
s : PullbackCone f.arrow g.arrow
⊢ (f ⊓ g).factorThru (s.fst ≫ f.arrow) ⋯ ≫ (f ⊓ g).ofLE g ⋯ = s.snd

pp: case refine_4
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
A : C
f g : Subobject A
x✝² : PullbackCone f.arrow g.arrow
x✝¹ : x✝².pt ⟶ underlying.obj (f ⊓ g)
h : x✝¹ ≫ (f ⊓ g).ofLE f ⋯ = x✝².fst
x✝ : x✝¹ ≫ (f ⊓ g).ofLE g ⋯ = x✝².snd
⊢ x✝¹ = (f ⊓ g).factorThru (x✝².fst ≫ f.arrow) ⋯

Tactic:
· simpa using ⟨factors_comp_arrow s.fst, by simpa [s.condition] using factors_comp_arrow s.snd⟩

Goal state after:
case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
A : C
f g : Subobject A
⊢ ∀ (s : PullbackCone f.arrow g.arrow), (f ⊓ g).factorThru (s.fst ≫ f.arrow) ⋯ ≫ (f ⊓ g).ofLE f ⋯ = s.fst

case refine_3
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
A : C
f g : Subobject A
s : PullbackCone f.arrow g.arrow
⊢ (f ⊓ g).factorThru (s.fst ≫ f.arrow) ⋯ ≫ (f ⊓ g).ofLE g ⋯ = s.snd

case refine_4
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
A : C
f g : Subobject A
x✝² : PullbackCone f.arrow g.arrow
x✝¹ : x✝².pt ⟶ underlying.obj (f ⊓ g)
h : x✝¹ ≫ (f ⊓ g).ofLE f ⋯ = x✝².fst
x✝ : x✝¹ ≫ (f ⊓ g).ofLE g ⋯ = x✝².snd
⊢ x✝¹ = (f ⊓ g).factorThru (x✝².fst ≫ f.arrow) ⋯
Module: Mathlib.CategoryTheory.Limits.Filtered

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
h : ∀ {J : Type v} [inst : SmallCategory J] [FinCategory J] (F : J ⥤ C), ∃ X, Nonempty (limit (F.op ⋙ yoneda.obj X))
J : Type v
x✝¹ : SmallCategory J
x✝ : FinCategory J
F : J ⥤ C
⊢ Nonempty (Cocone F)

Tactic:
obtain ⟨pt, ⟨ι⟩⟩ := h F
    exact ⟨⟨pt, (limitCompYonedaIsoCocone F pt).hom ι⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise

Goal state before:
pp: C : Type u_1
D : Type u_2
H : Type u_4
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_4, u_4} H
L : C ⥤ D
F : C ⥤ H
⊢ ∀ ⦃Y₁ Y₂ : D⦄ (x : Y₁ ≅ Y₂) [L.HasPointwiseLeftKanExtensionAt F Y₁], L.HasPointwiseLeftKanExtensionAt F Y₂

Tactic:
intro Y₁

Goal state after:
C : Type u_1
D : Type u_2
H : Type u_4
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_4, u_4} H
L : C ⥤ D
F : C ⥤ H
Y₁ : D
⊢ ∀ ⦃Y₂ : D⦄ (x : Y₁ ≅ Y₂) [L.HasPointwiseLeftKanExtensionAt F Y₁], L.HasPointwiseLeftKanExtensionAt F Y₂
Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise

Goal state before:
pp: C : Type u_1
D : Type u_2
H : Type u_4
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_4, u_4} H
L : C ⥤ D
F : C ⥤ H
⊢ ∀ {Y₁ Y₂ : D} (e : Y₁ ≅ Y₂), L.HasPointwiseRightKanExtensionAt F Y₁ ↔ L.HasPointwiseRightKanExtensionAt F Y₂

Tactic:
suffices ∀ ⦃Y₁ Y₂ : D⦄ (_ : Y₁ ≅ Y₂) [HasPointwiseRightKanExtensionAt L F Y₁],
      HasPointwiseRightKanExtensionAt L F Y₂ from
    fun Y₁ Y₂ e => ⟨fun _ => this e, fun _ => this e.symm⟩

Goal state after:
C : Type u_1
D : Type u_2
H : Type u_4
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_4, u_4} H
L : C ⥤ D
F : C ⥤ H
⊢ ∀ ⦃Y₁ Y₂ : D⦄ (x : Y₁ ≅ Y₂) [L.HasPointwiseRightKanExtensionAt F Y₁], L.HasPointwiseRightKanExtensionAt F Y₂
Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise

Goal state before:
pp: C : Type u_1
D : Type u_2
H : Type u_4
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_4, u_4} H
L : C ⥤ D
F : C ⥤ H
⊢ ∀ ⦃Y₁ Y₂ : D⦄ (x : Y₁ ≅ Y₂) [L.HasPointwiseRightKanExtensionAt F Y₁], L.HasPointwiseRightKanExtensionAt F Y₂

Tactic:
intro Y₁

Goal state after:
C : Type u_1
D : Type u_2
H : Type u_4
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_4, u_4} H
L : C ⥤ D
F : C ⥤ H
Y₁ : D
⊢ ∀ ⦃Y₂ : D⦄ (x : Y₁ ≅ Y₂) [L.HasPointwiseRightKanExtensionAt F Y₁], L.HasPointwiseRightKanExtensionAt F Y₂
Module: Mathlib.CategoryTheory.Functor.KanExtension.Adjunction

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
L : C ⥤ D
H : Type u_3
inst✝¹ : Category.{v_3, u_3} H
inst✝ : ∀ (F : C ⥤ H), L.HasLeftKanExtension F
F₁ F₂ : C ⥤ H
G : D ⥤ H
f : F₁ ⟶ F₂
α : F₂ ⟶ ((whiskeringLeft C D H).obj L).obj G
X : C
⊢ f.app X ≫ α.app X =
    (L.lanUnit.app F₁).app X ≫
      (L.lan.map f).app (L.obj X) ≫ ((L.lan.obj F₂).descOfIsLeftKanExtension (L.lanUnit.app F₂) G α).app (L.obj X)

Tactic:
← assoc

Goal state after:
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
L : C ⥤ D
H : Type u_3
inst✝¹ : Category.{v_3, u_3} H
inst✝ : ∀ (F : C ⥤ H), L.HasLeftKanExtension F
F₁ F₂ : C ⥤ H
G : D ⥤ H
f : F₁ ⟶ F₂
α : F₂ ⟶ ((whiskeringLeft C D H).obj L).obj G
X : C
⊢ f.app X ≫ α.app X =
    ((L.lanUnit.app F₁).app X ≫ (L.lan.map f).app (L.obj X)) ≫
      ((L.lan.obj F₂).descOfIsLeftKanExtension (L.lanUnit.app F₂) G α).app (L.obj X)
Module: Mathlib.CategoryTheory.Functor.KanExtension.Adjunction

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
L : C ⥤ D
H : Type u_3
inst✝³ : Category.{v_3, u_3} H
inst✝² : ∀ (F : C ⥤ H), L.HasLeftKanExtension F
inst✝¹ : HasColimitsOfShape C H
inst✝ : HasColimitsOfShape D H
X✝ Y✝ : C ⥤ H
f : X✝ ⟶ Y✝
i : C
⊢ (f.app i ≫ (L.lanUnit.app Y✝).app i) ≫ colimit.ι (L.lan.obj Y✝) (L.obj i) =
    (L.lanUnit.app X✝).app i ≫ (L.lan.map f).app (L.obj i) ≫ colimit.ι (L.lan.obj Y✝) (L.obj i)

Tactic:
← assoc

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
L : C ⥤ D
H : Type u_3
inst✝³ : Category.{v_3, u_3} H
inst✝² : ∀ (F : C ⥤ H), L.HasLeftKanExtension F
inst✝¹ : HasColimitsOfShape C H
inst✝ : HasColimitsOfShape D H
X✝ Y✝ : C ⥤ H
f : X✝ ⟶ Y✝
i : C
⊢ (f.app i ≫ (L.lanUnit.app Y✝).app i) ≫ colimit.ι (L.lan.obj Y✝) (L.obj i) =
    ((L.lanUnit.app X✝).app i ≫ (L.lan.map f).app (L.obj i)) ≫ colimit.ι (L.lan.obj Y✝) (L.obj i)
Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic

Goal state before:
pp: C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} C'
inst✝² : Category.{v_3, u_3} H
inst✝¹ : Category.{v_4, u_4} D
inst✝ : Category.{v_5, u_5} D'
L : C ≌ D
F₀ : C ⥤ H
F₁ : D ⥤ H
α : F₀ ≅ L.functor ⋙ F₁
⊢ ∀ (Y : StructuredArrow F₀ ((whiskeringLeft C C H).obj (𝟭 C)))
    (m : (LeftExtension.postcomp₁ L.functor L.functor.leftUnitor.inv F₀).obj (LeftExtension.mk F₁ α.hom) ⟶ Y),
    m = StructuredArrow.homMk (α.inv ≫ Y.hom ≫ Y.right.leftUnitor.hom) ⋯

Tactic:
intro y

Goal state after:
C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} C'
inst✝² : Category.{v_3, u_3} H
inst✝¹ : Category.{v_4, u_4} D
inst✝ : Category.{v_5, u_5} D'
L : C ≌ D
F₀ : C ⥤ H
F₁ : D ⥤ H
α : F₀ ≅ L.functor ⋙ F₁
y : StructuredArrow F₀ ((whiskeringLeft C C H).obj (𝟭 C))
⊢ ∀ (m : (LeftExtension.postcomp₁ L.functor L.functor.leftUnitor.inv F₀).obj (LeftExtension.mk F₁ α.hom) ⟶ y),
    m = StructuredArrow.homMk (α.inv ≫ y.hom ≫ y.right.leftUnitor.hom) ⋯
Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic

Goal state before:
pp: C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} C'
inst✝² : Category.{v_3, u_3} H
inst✝¹ : Category.{v_4, u_4} D
inst✝ : Category.{v_5, u_5} D'
L : C ≌ D
F₀ : C ⥤ H
F₁ : D ⥤ H
α : L.functor ⋙ F₁ ≅ F₀
⊢ ∀ (X : CostructuredArrow ((whiskeringLeft C C H).obj (𝟭 C)) F₀)
    (m : X ⟶ (RightExtension.postcomp₁ L.functor L.functor.leftUnitor.hom F₀).obj (RightExtension.mk F₁ α.hom)),
    m = CostructuredArrow.homMk (X.left.leftUnitor.inv ≫ X.hom ≫ α.inv) ⋯

Tactic:
intro y

Goal state after:
C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} C'
inst✝² : Category.{v_3, u_3} H
inst✝¹ : Category.{v_4, u_4} D
inst✝ : Category.{v_5, u_5} D'
L : C ≌ D
F₀ : C ⥤ H
F₁ : D ⥤ H
α : L.functor ⋙ F₁ ≅ F₀
y : CostructuredArrow ((whiskeringLeft C C H).obj (𝟭 C)) F₀
⊢ ∀ (m : y ⟶ (RightExtension.postcomp₁ L.functor L.functor.leftUnitor.hom F₀).obj (RightExtension.mk F₁ α.hom)),
    m = CostructuredArrow.homMk (y.left.leftUnitor.inv ≫ y.hom ≫ α.inv) ⋯
Module: Mathlib.CategoryTheory.Limits.Presheaf

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝² : Category.{v₂, u₂} ℰ
A : C ⥤ ℰ
inst✝¹ : uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A
L : (Cᵒᵖ ⥤ Type (max w v₁ v₂)) ⥤ ℰ
α : A ⟶ uliftYoneda.{max w v₂, v₁, u₁} ⋙ L
inst✝ : L.IsLeftKanExtension α
P : Cᵒᵖ ⥤ Type (max w v₁ v₂)
Z : Cᵒᵖ
z : P.obj Z
h₁ :
  ((uliftYonedaAdjunction L α).homEquiv P (L.obj P)) (𝟙 (L.obj P)) =
    (uliftYonedaAdjunction L α).unit.app P ≫ (restrictedULiftYoneda A).map (𝟙 (L.obj P))
⊢ (hom (((uliftYonedaAdjunction L α).unit.app P).app Z)) z =
    { down := α.app (unop Z) ≫ L.map (uliftYonedaEquiv.symm z) }

Tactic:
simp only [Functor.comp_obj, Functor.map_id, comp_id] at h₁

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝² : Category.{v₂, u₂} ℰ
A : C ⥤ ℰ
inst✝¹ : uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A
L : (Cᵒᵖ ⥤ Type (max w v₁ v₂)) ⥤ ℰ
α : A ⟶ uliftYoneda.{max w v₂, v₁, u₁} ⋙ L
inst✝ : L.IsLeftKanExtension α
P : Cᵒᵖ ⥤ Type (max w v₁ v₂)
Z : Cᵒᵖ
z : P.obj Z
h₁ : ((uliftYonedaAdjunction L α).homEquiv P (L.obj P)) (𝟙 (L.obj P)) = (uliftYonedaAdjunction L α).unit.app P
⊢ (hom (((uliftYonedaAdjunction L α).unit.app P).app Z)) z =
    { down := α.app (unop Z) ≫ L.map (uliftYonedaEquiv.symm z) }
Module: Mathlib.CategoryTheory.Subobject.Comma

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : C ⥤ D
T : D
inst✝¹ : HasFiniteColimits C
inst✝ : PreservesFiniteColimits S
A : CostructuredArrow S T
⊢ ∀ ⦃A_1 : (CostructuredArrow S T)ᵒᵖ⦄ (f : A_1 ⟶ op A) [inst : Mono f]
    {q : S.obj (unop (Subobject.underlying.obj (projectQuotient (Subobject.mk f)))) ⟶ T}
    (hq : S.map (projectQuotient (Subobject.mk f)).arrow.unop ≫ q = A.hom),
    liftQuotient (projectQuotient (Subobject.mk f)) hq = Subobject.mk f

Tactic:
intro P f hf q hq
      fapply Subobject.mk_eq_mk_of_comm
      · refine (Iso.op (isoMk ?_ ?_) : _ ≅ op (unop P))
        · exact (Subobject.underlyingIso f.unop.left.op).unop
        · refine (cancel_epi (S.map f.unop.left)).1 ?_
          simpa [← Category.assoc, ← S.map_comp] using hq
      · exact Quiver.Hom.unop_inj (by simp)

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : ∀ (X : C), ∃ J x, P.colimitsOfShape J X
⊢ P.IsSeparating

Tactic:
by
  intro X Y f g h
  obtain ⟨J, _, ⟨p⟩⟩ := hP X
  exact p.isColimit.hom_ext (fun j ↦ h _ (p.prop_diag_obj _) _)

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.AdjointFunctorTheorems

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u₁
inst✝² : Category.{v₁, u₁} D
G : D ⥤ C
inst✝¹ : HasLimits D
inst✝ : PreservesLimitsOfSize.{v₁, v₁, v₁, v, u₁, u} G
hG : SolutionSetCondition G
A : C
⊢ HasInitial (StructuredArrow A G)

Tactic:
specialize hG A

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
D : Type u₁
inst✝² : Category.{v₁, u₁} D
G : D ⥤ C
inst✝¹ : HasLimits D
inst✝ : PreservesLimitsOfSize.{v₁, v₁, v₁, v, u₁, u} G
A : C
hG : ∃ ι B f, ∀ (X : D) (h : A ⟶ G.obj X), ∃ i g, f i ≫ G.map g = h
⊢ HasInitial (StructuredArrow A G)
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Basic

Goal state before:
pp: case refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : Abelian C
inst✝¹ : Abelian D
inst✝ : IsGrothendieckAbelian.{w, v, u} C
α : C ≌ D
hasFilteredColimits : HasFilteredColimitsOfSize.{w, w, v₂, u₂} D
x✝² : Type w
x✝¹ : Category.{w, w} x✝²
x✝ : IsFiltered x✝²
⊢ HasExactColimitsOfShape x✝² D

Tactic:
exact HasExactColimitsOfShape.of_codomain_equivalence _ α

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : C
hG : IsSeparator G
X Y : C
f g : X ⟶ Y
hfg : ∀ (h : G ⟶ X), h ≫ f = h ≫ g
H : C
hH : ObjectProperty.singleton G H
h : H ⟶ X
⊢ h ≫ f = h ≫ g

Tactic:
obtain rfl := (ObjectProperty.singleton_iff _ _).1 hH

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : C
hG : IsSeparator G
X Y : C
f g : X ⟶ Y
hfg : ∀ (h : G ⟶ X), h ≫ f = h ≫ g
hH : ObjectProperty.singleton G G
h : G ⟶ X
⊢ h ≫ f = h ≫ g
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : C
hG : IsCoseparator G
X Y : C
f g : X ⟶ Y
hfg : ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
H : C
hH : ObjectProperty.singleton G H
h : Y ⟶ H
⊢ f ≫ h = g ≫ h

Tactic:
obtain rfl := (ObjectProperty.singleton_iff _ _).1 hH

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : C
hG : IsCoseparator G
X Y : C
f g : X ⟶ Y
hfg : ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
hH : ObjectProperty.singleton G G
h : Y ⟶ G
⊢ f ≫ h = g ≫ h
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : C
hG : IsDetector G
X Y : C
f : X ⟶ Y
hf : ∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h
H : C
hH : ObjectProperty.singleton G H
h : H ⟶ Y
⊢ ∃! h', h' ≫ f = h

Tactic:
obtain rfl := (ObjectProperty.singleton_iff _ _).1 hH

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : C
hG : IsDetector G
X Y : C
f : X ⟶ Y
hf : ∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h
hH : ObjectProperty.singleton G G
h : G ⟶ Y
⊢ ∃! h', h' ≫ f = h
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : C
hG : IsCodetector G
X Y : C
f : X ⟶ Y
hf : ∀ (h : X ⟶ G), ∃! h', f ≫ h' = h
H : C
hH : ObjectProperty.singleton G H
h : X ⟶ H
⊢ ∃! h', f ≫ h' = h

Tactic:
obtain rfl := (ObjectProperty.singleton_iff _ _).1 hH

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : C
hG : IsCodetector G
X Y : C
f : X ⟶ Y
hf : ∀ (h : X ⟶ G), ∃! h', f ≫ h' = h
hH : ObjectProperty.singleton G G
h : X ⟶ G
⊢ ∃! h', f ≫ h' = h
Module: Mathlib.CategoryTheory.Limits.Presheaf

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : LocallySmall.{w, v₁, u₁} C
F : C ⥤ Type w
inst✝ : HasColimitsOfShape F.Elementsᵒᵖ (Type w)
X₁ X₂ : C
f : X₁ ⟶ X₂
⊢ ∀ (j : F.Elementsᵒᵖ),
    colimit.ι
          (((whiskeringLeft F.Elementsᵒᵖ Cᵒᵖ (Type w)).obj (CategoryOfElements.π F).op).obj
            (shrinkYoneda.{w, v₁, u₁}.obj X₁))
          j ≫
        (shrinkYoneda.{w, v₁, u₁} ⋙
                (whiskeringLeft F.Elementsᵒᵖ Cᵒᵖ (Type w)).obj (CategoryOfElements.π F).op ⋙ colim).map
            f ≫
          ((colimit.isColimit ((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X₂)).coconePointUniqueUpToIso
              (isColimitCoconeπOpCompShrinkYonedaObj F X₂)).hom =
      colimit.ι
          (((whiskeringLeft F.Elementsᵒᵖ Cᵒᵖ (Type w)).obj (CategoryOfElements.π F).op).obj
            (shrinkYoneda.{w, v₁, u₁}.obj X₁))
          j ≫
        ((colimit.isColimit ((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X₁)).coconePointUniqueUpToIso
              (isColimitCoconeπOpCompShrinkYonedaObj F X₁)).hom ≫
          F.map f

Tactic:
by
        cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Coproducts

Goal state before:
pp: case mpr.refine_3
X Y : Type u
c : BinaryCofan X Y
h₁ : Injective ⇑(ConcreteCategory.hom c.inl)
h₂ : Injective ⇑(ConcreteCategory.hom c.inr)
h₃ : IsCompl (Set.range ⇑(ConcreteCategory.hom c.inl)) (Set.range ⇑(ConcreteCategory.hom c.inr))
this :
  ∀ (x : (fun X ↦ X) (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left })),
    x ∈ Set.range ⇑(ConcreteCategory.hom c.inl) ∨ x ∈ Set.range ⇑(ConcreteCategory.hom c.inr)
T : Type u
f : X ⟶ T
g : Y ⟶ T
x : (pair X Y).obj { as := right }
⊢ ∀ (x_1 : X) (h : (ConcreteCategory.hom c.inl) x_1 = (ConcreteCategory.hom c.inr) x),
    (ConcreteCategory.hom f)
        ((Equiv.ofInjective (⇑(ConcreteCategory.hom c.inl)) h₁).symm ⟨(ConcreteCategory.hom c.inr) x, ⋯⟩) =
      (ConcreteCategory.hom g) x

Tactic:
intro y

Goal state after:
case mpr.refine_3
X Y : Type u
c : BinaryCofan X Y
h₁ : Injective ⇑(ConcreteCategory.hom c.inl)
h₂ : Injective ⇑(ConcreteCategory.hom c.inr)
h₃ : IsCompl (Set.range ⇑(ConcreteCategory.hom c.inl)) (Set.range ⇑(ConcreteCategory.hom c.inr))
this :
  ∀ (x : (fun X ↦ X) (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left })),
    x ∈ Set.range ⇑(ConcreteCategory.hom c.inl) ∨ x ∈ Set.range ⇑(ConcreteCategory.hom c.inr)
T : Type u
f : X ⟶ T
g : Y ⟶ T
x : (pair X Y).obj { as := right }
y : X
⊢ ∀ (h : (ConcreteCategory.hom c.inl) y = (ConcreteCategory.hom c.inr) x),
    (ConcreteCategory.hom f)
        ((Equiv.ofInjective (⇑(ConcreteCategory.hom c.inl)) h₁).symm ⟨(ConcreteCategory.hom c.inr) x, ⋯⟩) =
      (ConcreteCategory.hom g) x