mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u_1
inst✝² : Category.{v_1, u_1} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝¹ : G.Full
inst✝ : G.Faithful
I : D
hI : Injective (G.obj I)
X Y : D
f : X ⟶ I
g : X ⟶ Y
⊢ ∀ [Mono g], ∃ h, g ≫ h = f

Tactic:
by
    intro
    have : PreservesLimitsOfSize.{0, 0} G := adj.rightAdjoint_preservesLimits
    rcases hI.factors (G.map f) (G.map g) with ⟨w,h⟩
    use inv (adj.counit.app _) ≫ F.map w ≫ adj.counit.app _
    exact G.map_injective (by simpa)

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

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✝ : Balanced C
S : ShortComplex C
hS : S.ShortExact
this : Epi S.g
⊢ IsColimit (CokernelCofork.ofπ S.g ⋯)

Tactic:
exact hS.exact.gIsCokernel

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

Goal state before:
pp: S : ShortComplex Ab
⊢ (AddCommGrpCat.kernelIsLimit S.g).lift (Limits.KernelFork.ofι S.f ⋯) ≫
      AddCommGrpCat.ofHom (QuotientAddGroup.mk' S.abToCycles.range) =
    0

Tactic:
by
    ext (x : S.X₁)
    dsimp
    rw [QuotientAddGroup.eq_zero_iff, AddMonoidHom.mem_range]
    apply exists_apply_eq_apply

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

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
inst✝⁵ : HasBinaryBiproducts C
inst✝⁴ : HasFiniteCoproducts C
inst✝³ : HasCoequalizers C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroObject D
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), PreservesColimit (parallelPair f 0) F
this✝ : PreservesColimitsOfShape WalkingParallelPair F := preservesCoequalizers_of_preservesCokernels F
this : PreservesColimit (empty C) F := preservesInitialObject_of_preservesZeroMorphisms F
⊢ PreservesFiniteColimits F

Tactic:
let := preservesColimitsOfShape_pempty_of_preservesInitial F

Goal state after:
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
inst✝⁵ : HasBinaryBiproducts C
inst✝⁴ : HasFiniteCoproducts C
inst✝³ : HasCoequalizers C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroObject D
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), PreservesColimit (parallelPair f 0) F
this✝¹ : PreservesColimitsOfShape WalkingParallelPair F := preservesCoequalizers_of_preservesCokernels F
this✝ : PreservesColimit (empty C) F := preservesInitialObject_of_preservesZeroMorphisms F
this : PreservesColimitsOfShape (Discrete PEmpty.{1}) F := preservesColimitsOfShape_pempty_of_preservesInitial F
⊢ PreservesFiniteColimits 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
⊢ hS.lift (KernelFork.ofι S.iCycles ⋯) ≫ S.toCycles = 𝟙 S.cycles

Tactic:
rw [← cancel_mono S.iCycles, assoc, toCycles_i, id_comp]
          exact Fork.IsLimit.lift_ι hS

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
hS : S.Exact
⊢ IsZero S.X₂ ↔ S.f = 0 ∧ S.g = 0

Tactic:
by
  constructor
  · intro h
    exact ⟨h.eq_of_tgt _ _, h.eq_of_src _ _⟩
  · rintro ⟨hf, hg⟩
    exact hS.isZero_X₂ hf hg

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

Goal state before:
pp: case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X : C
inst✝ : HasPullbacks C
f : MonoOver X
⊢ (pullback (𝟙 X)).obj (Quotient.mk'' f) = Quotient.mk'' f

Tactic:
| _ f
   => 

Goal state after:
case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X : C
inst✝ : HasPullbacks C
f : MonoOver X
⊢ (pullback (𝟙 X)).obj (Quotient.mk'' f) = Quotient.mk'' f
Module: Mathlib.CategoryTheory.Subobject.Basic

Goal state before:
pp: case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
f : MonoOver X
⊢ (map (𝟙 X)).obj (Quotient.mk'' f) = Quotient.mk'' f

Tactic:
| _ f
   => 

Goal state after:
case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
f : MonoOver X
⊢ (map (𝟙 X)).obj (Quotient.mk'' f) = Quotient.mk'' f
Module: Mathlib.CategoryTheory.Subobject.Limits

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
X Y Z✝ : C
inst✝³ : HasZeroMorphisms C
f✝ : X ⟶ Y
inst✝² : HasKernel f✝
f : X ⟶ Y
inst✝¹ : HasKernel f
Z : C
h : Y ⟶ Z
inst✝ : Mono h
⊢ IsIso ((kernelSubobject f).ofLE (kernelSubobject (f ≫ h)) ⋯)

Tactic:
rw [ofLE_mk_le_mk_of_comm (kernelCompMono f h).inv]

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
X Y Z✝ : C
inst✝³ : HasZeroMorphisms C
f✝ : X ⟶ Y
inst✝² : HasKernel f✝
f : X ⟶ Y
inst✝¹ : HasKernel f
Z : C
h : Y ⟶ Z
inst✝ : Mono h
⊢ IsIso ((underlyingIso (kernel.ι f)).hom ≫ (kernelCompMono f h).inv ≫ (underlyingIso (kernel.ι (f ≫ h))).inv)

C : Type u
inst✝⁴ : Category.{v, u} C
X Y Z✝ : C
inst✝³ : HasZeroMorphisms C
f✝ : X ⟶ Y
inst✝² : HasKernel f✝
f : X ⟶ Y
inst✝¹ : HasKernel f
Z : C
h : Y ⟶ Z
inst✝ : Mono h
⊢ (kernelCompMono f h).inv ≫ kernel.ι (f ≫ h) = kernel.ι f
Module: Mathlib.CategoryTheory.Abelian.Exact

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
h : kernel.ι S.g ≫ cokernel.π S.f = 0
W'✝ : C
x✝² : W'✝ ⟶ S.X₂
x✝¹ : x✝² ≫ S.g = 0
x✝ : W'✝ ⟶ Abelian.image S.f
hm : x✝ ≫ Abelian.image.ι S.f = x✝²
⊢ x✝² = kernel.lift (cokernel.π S.f) x✝² ⋯ ≫ Abelian.image.ι S.f

Tactic:
kernel.lift_ι

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
h : kernel.ι S.g ≫ cokernel.π S.f = 0
W'✝ : C
x✝² : W'✝ ⟶ S.X₂
x✝¹ : x✝² ≫ S.g = 0
x✝ : W'✝ ⟶ Abelian.image S.f
hm : x✝ ≫ Abelian.image.ι S.f = x✝²
⊢ x✝² = x✝²
Module: Mathlib.CategoryTheory.Abelian.Exact

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
Z : C
tfae_2_to_1 : cokernel.π f = 0 → Epi f
x✝ : Epi f
⊢ cokernel.π f = 0

Tactic:
rw [← cancel_epi f, cokernel.condition, comp_zero]

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

Goal state before:
pp: case insert.inr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
I : Type u_1
B : C
P : I → Subobject B
a✝¹ : I
s✝ : Finset I
a✝ : a✝¹ ∉ s✝
ih : ∀ i ∈ s✝, (P i).Factors (s✝.inf P).arrow
i✝ : I
m : i✝ ∈ s✝
⊢ (P i✝).Factors (P a✝¹ ⊓ s✝.inf P).arrow

Tactic:
· rw [← factorThru_arrow _ _ (inf_arrow_factors_right _ _)]
      apply factors_of_factors_right
      exact ih _ m

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Exact

Goal state before:
pp: A : Type u₁
B : Type u₂
inst✝⁶ : Category.{v₁, u₁} A
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Abelian A
inst✝³ : Abelian B
L : A ⥤ B
inst✝² : L.PreservesZeroMorphisms
inst✝¹ : L.PreservesEpimorphisms
inst✝ : ∀ {X Y : A} (f : X ⟶ Y), PreservesLimit (parallelPair f 0) L
S : ShortComplex A
hS : S.Exact
⊢ L.map (Abelian.factorThruImage S.f ≫ kernel.ι (cokernel.π S.f)) = L.map S.f

Tactic:
kernel.lift_ι

Goal state after:
A : Type u₁
B : Type u₂
inst✝⁶ : Category.{v₁, u₁} A
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Abelian A
inst✝³ : Abelian B
L : A ⥤ B
inst✝² : L.PreservesZeroMorphisms
inst✝¹ : L.PreservesEpimorphisms
inst✝ : ∀ {X Y : A} (f : X ⟶ Y), PreservesLimit (parallelPair f 0) L
S : ShortComplex A
hS : S.Exact
⊢ L.map S.f = L.map S.f
Module: Mathlib.CategoryTheory.Subobject.Lattice

Goal state before:
pp: case w
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : LocallySmall.{w, v₁, u₁} C
inst✝¹ : WellPowered.{w, v₁, u₁} C
inst✝ : HasWidePullbacks C
A : C
s : Set (Subobject A)
f : Subobject A
k : ∀ g ∈ s, f ≤ g
⊢ (leInfCone s f k).π.app none = f.arrow

Tactic:
leInfCone_π_app_none

Goal state after:
case w
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : LocallySmall.{w, v₁, u₁} C
inst✝¹ : WellPowered.{w, v₁, u₁} C
inst✝ : HasWidePullbacks C
A : C
s : Set (Subobject A)
f : Subobject A
k : ∀ g ∈ s, f ≤ g
⊢ f.arrow = f.arrow
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
X : C
Y : Subobject X
W Z : Subobject (underlying.obj Y)
⊢ { toFun := fun Z ↦ ⟨mk (Z.arrow ≫ Y.arrow), ⋯⟩, invFun := fun Z ↦ mk ((↑Z).ofLE Y ⋯), left_inv := ⋯, right_inv := ⋯ }
        W ≤
      { toFun := fun Z ↦ ⟨mk (Z.arrow ≫ Y.arrow), ⋯⟩, invFun := fun Z ↦ mk ((↑Z).ofLE Y ⋯), left_inv := ⋯,
          right_inv := ⋯ }
        Z ↔
    W ≤ Z

Tactic:
by
    dsimp
    constructor
    · intro h
      exact le_of_comm (((underlyingIso _).inv ≫ ofLE _ _ (Subtype.mk_le_mk.mp h) ≫
        (underlyingIso _).hom)) (by cat_disch)
    · intro h
      exact Subtype.mk_le_mk.mpr (le_of_comm
        ((underlyingIso _).hom ≫ ofLE _ _ h ≫ (underlyingIso _).inv) (by simp))

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

Goal state before:
pp: case mp
C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Category.{v_3, u_3} D'
inst✝ : Category.{v_4, u_4} H
L : C ⥤ D
L' : C ⥤ D'
F : C ⥤ H
E : D ≌ D'
eL : L ⋙ E.functor ≅ L'
Y : D
Y' : D'
e : E.functor.obj Y ≅ Y'
⊢ L.HasPointwiseRightKanExtensionAt F Y → L'.HasPointwiseRightKanExtensionAt F Y'

pp: case mpr
C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Category.{v_3, u_3} D'
inst✝ : Category.{v_4, u_4} H
L : C ⥤ D
L' : C ⥤ D'
F : C ⥤ H
E : D ≌ D'
eL : L ⋙ E.functor ≅ L'
Y : D
Y' : D'
e : E.functor.obj Y ≅ Y'
⊢ L'.HasPointwiseRightKanExtensionAt F Y' → L.HasPointwiseRightKanExtensionAt F Y

Tactic:
· intro
    exact hasPointwiseRightKanExtensionAt_of_equivalence L L' F E eL Y Y' e

Goal state after:
case mpr
C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Category.{v_3, u_3} D'
inst✝ : Category.{v_4, u_4} H
L : C ⥤ D
L' : C ⥤ D'
F : C ⥤ H
E : D ≌ D'
eL : L ⋙ E.functor ≅ L'
Y : D
Y' : D'
e : E.functor.obj Y ≅ Y'
⊢ L'.HasPointwiseRightKanExtensionAt F Y' → L.HasPointwiseRightKanExtensionAt F Y
Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X Y : C
f : X ⟶ Y
g g' : yoneda.obj Y ⟶ A
h : g = g'
x : F.obj (op (CostructuredArrow.mk g'))
⊢ op (CostructuredArrow.mk g') = op (CostructuredArrow.mk g)

Tactic:
by rw [h]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X Y : C
f : X ⟶ Y
g g' : yoneda.obj Y ⟶ A
h : g = g'
x : F.obj (op (CostructuredArrow.mk g'))
⊢ op (CostructuredArrow.mk (yoneda.map f ≫ g')) = op (CostructuredArrow.mk (yoneda.map f ≫ g))

Tactic:
by rw [h]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X : C
p q : YonedaCollection F X
h : p.fst = q.fst
⊢ op (CostructuredArrow.mk q.fst) = op (CostructuredArrow.mk p.fst)

Tactic:
by rw [h]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory

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✝
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
D : Type u_2
inst✝⁴ : Category.{v_2, u_2} D
E : Type u_3
inst✝³ : Category.{v_3, u_3} E
J : Type u_4
inst✝² : Category.{v_4, u_4} J
inst✝¹ : HasLimitsOfShape J E
F : D ⥤ E
inst✝ : ReflectsLimitsOfShape J F
K : J ⥤ C ⥤ D
c : Cone K
hc : IsLimit (((whiskeringRight C D E).obj F).mapCone c)
⊢ IsLimit c

Tactic:
by
    apply evaluationJointlyReflectsLimits _ (fun k ↦ ?_)
    apply isLimitOfReflects F
    exact isLimitOfPreserves ((evaluation C E).obj k) hc

Goal state after:
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
L' : D ⥤ D'
F₀ : C ⥤ H
F₁ : D ⥤ H
F₂ : D' ⥤ H
α : F₀ ⟶ L ⋙ F₁
hα : StructuredArrow.IsUniversal (mk F₁ α)
b : L'.LeftExtension F₁
hb : StructuredArrow.IsUniversal b
y : (L ⋙ L').LeftExtension F₀
u : L'.LeftExtension F₁ :=
  mk (StructuredArrow.right y)
    (hα.desc
      (mk (L' ⋙ StructuredArrow.right y) (StructuredArrow.hom y ≫ (L.associator L' (StructuredArrow.right y)).hom)))
⊢ StructuredArrow.hom ((precomp₂ L' α).obj b) ≫ ((whiskeringLeft C D' H).obj (L ⋙ L')).map (hb.desc u) =
    StructuredArrow.hom y

Tactic:
ext x

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
L' : D ⥤ D'
F₀ : C ⥤ H
F₁ : D ⥤ H
F₂ : D' ⥤ H
α : F₀ ⟶ L ⋙ F₁
hα : StructuredArrow.IsUniversal (mk F₁ α)
b : L'.LeftExtension F₁
hb : StructuredArrow.IsUniversal b
y : (L ⋙ L').LeftExtension F₀
u : L'.LeftExtension F₁ :=
  mk (StructuredArrow.right y)
    (hα.desc
      (mk (L' ⋙ StructuredArrow.right y) (StructuredArrow.hom y ≫ (L.associator L' (StructuredArrow.right y)).hom)))
x : C
⊢ (StructuredArrow.hom ((precomp₂ L' α).obj b) ≫ ((whiskeringLeft C D' H).obj (L ⋙ L')).map (hb.desc u)).app x =
    (StructuredArrow.hom y).app x
Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic

Goal state before:
pp: C : Type u_1
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁴ : Category.{v_1, u_1} 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
L' : D ⥤ D'
F₀ : C ⥤ H
F₁ : D ⥤ H
α : F₀ ⟶ L ⋙ F₁
inst✝ : F₁.IsLeftKanExtension α
F₂ : D' ⥤ H
L'' : C ⥤ D'
e : L ⋙ L' ≅ L''
β : F₁ ⟶ L' ⋙ F₂
γ : F₀ ⟶ L'' ⋙ F₂
hγ : α ≫ L.whiskerLeft β ≫ (L.associator L' F₂).inv ≫ whiskerRight e.hom F₂ = γ
Ψ : (L ⋙ L').LeftExtension F₀ ≌ L''.LeftExtension F₀ := leftExtensionEquivalenceOfIso₁ e F₀
hα : StructuredArrow.IsUniversal (LeftExtension.mk F₁ α)
x✝ : F₂.IsLeftKanExtension β
h : StructuredArrow.IsUniversal (LeftExtension.mk F₂ β)
this : StructuredArrow.IsUniversal ((LeftExtension.precomp₂ L' α).obj (LeftExtension.mk F₂ β))
⊢ StructuredArrow.hom ((LeftExtension.precomp₂ L' α).obj (LeftExtension.mk F₂ β)) ≫
      ((whiskeringLeft C D' H).obj (L ⋙ L')).map
        (NatIso.ofComponents
            (fun x ↦
              Iso.refl ((StructuredArrow.right ((LeftExtension.precomp₂ L' α).obj (LeftExtension.mk F₂ β))).obj x))
            ⋯).hom =
    StructuredArrow.hom (Ψ.inverse.obj (LeftExtension.mk F₂ γ))

Tactic:
ext x

Goal state after:
C : Type u_1
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁴ : Category.{v_1, u_1} 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
L' : D ⥤ D'
F₀ : C ⥤ H
F₁ : D ⥤ H
α : F₀ ⟶ L ⋙ F₁
inst✝ : F₁.IsLeftKanExtension α
F₂ : D' ⥤ H
L'' : C ⥤ D'
e : L ⋙ L' ≅ L''
β : F₁ ⟶ L' ⋙ F₂
γ : F₀ ⟶ L'' ⋙ F₂
hγ : α ≫ L.whiskerLeft β ≫ (L.associator L' F₂).inv ≫ whiskerRight e.hom F₂ = γ
Ψ : (L ⋙ L').LeftExtension F₀ ≌ L''.LeftExtension F₀ := leftExtensionEquivalenceOfIso₁ e F₀
hα : StructuredArrow.IsUniversal (LeftExtension.mk F₁ α)
x✝ : F₂.IsLeftKanExtension β
h : StructuredArrow.IsUniversal (LeftExtension.mk F₂ β)
this : StructuredArrow.IsUniversal ((LeftExtension.precomp₂ L' α).obj (LeftExtension.mk F₂ β))
x : C
⊢ (StructuredArrow.hom ((LeftExtension.precomp₂ L' α).obj (LeftExtension.mk F₂ β)) ≫
          ((whiskeringLeft C D' H).obj (L ⋙ L')).map
            (NatIso.ofComponents
                (fun x ↦
                  Iso.refl ((StructuredArrow.right ((LeftExtension.precomp₂ L' α).obj (LeftExtension.mk F₂ β))).obj x))
                ⋯).hom).app
      x =
    (StructuredArrow.hom (Ψ.inverse.obj (LeftExtension.mk F₂ γ))).app x
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 ⥤ ℰ
P : Cᵒᵖ ⥤ Type (max w v₁ v₂)
E : ℰ
f :
  CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P ⋙ A ⟶
    (Functor.const (CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)).obj E
x✝¹ x✝ : Cᵒᵖ
g : x✝¹ ⟶ x✝
⊢ (P.map g ≫ ↾fun x ↦ { down := f.app (CostructuredArrow.mk (uliftYonedaEquiv.symm x)) }) =
    (↾fun x ↦ { down := f.app (CostructuredArrow.mk (uliftYonedaEquiv.symm x)) }) ≫
      ((restrictedULiftYoneda A).obj E).map g

Tactic:
ext x

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝ : Category.{v₂, u₂} ℰ
A : C ⥤ ℰ
P : Cᵒᵖ ⥤ Type (max w v₁ v₂)
E : ℰ
f :
  CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P ⋙ A ⟶
    (Functor.const (CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)).obj E
x✝¹ x✝ : Cᵒᵖ
g : x✝¹ ⟶ x✝
x : P.obj x✝¹
⊢ (hom (P.map g ≫ ↾fun x ↦ { down := f.app (CostructuredArrow.mk (uliftYonedaEquiv.symm x)) })).toFun x =
    (hom
          ((↾fun x ↦ { down := f.app (CostructuredArrow.mk (uliftYonedaEquiv.symm x)) }) ≫
            ((restrictedULiftYoneda A).obj E).map g)).toFun
      x
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:
ext x

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
x : C
⊢ (StructuredArrow.Hom.right m).app x =
    (StructuredArrow.Hom.right (StructuredArrow.homMk (α.inv ≫ y.hom ≫ y.right.leftUnitor.hom) ⋯)).app x
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₀
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) ⋯

Tactic:
ext x

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)
x : C
⊢ m.left.app x = (CostructuredArrow.homMk (y.left.leftUnitor.inv ≫ y.hom ≫ α.inv) ⋯).left.app x
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 ⥤ ℰ
P : Cᵒᵖ ⥤ Type (max w v₁)
s : Cocone (functorToRepresentables P)
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ ((coconeOfRepresentable P).pt.map f ≫ ↾fun x ↦ uliftYonedaEquiv (s.ι.app (op (P.elementsMk Y x)))) =
    (↾fun x ↦ uliftYonedaEquiv (s.ι.app (op (P.elementsMk X x)))) ≫ s.pt.map f

Tactic:
ext x

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝ : Category.{v₂, u₂} ℰ
A : C ⥤ ℰ
P : Cᵒᵖ ⥤ Type (max w v₁)
s : Cocone (functorToRepresentables P)
X Y : Cᵒᵖ
f : X ⟶ Y
x : (coconeOfRepresentable P).pt.obj X
⊢ (hom ((coconeOfRepresentable P).pt.map f ≫ ↾fun x ↦ uliftYonedaEquiv (s.ι.app (op (P.elementsMk Y x))))).toFun x =
    (hom ((↾fun x ↦ uliftYonedaEquiv (s.ι.app (op (P.elementsMk X x)))) ≫ s.pt.map f)).toFun x
Module: Mathlib.CategoryTheory.Subobject.Comma

Goal state before:
pp: case i
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : D
T : C ⥤ D
inst✝¹ : HasFiniteLimits C
inst✝ : PreservesFiniteLimits T
A P : StructuredArrow S T
f : P ⟶ A
hf : Mono f
q : S ⟶ T.obj (Subobject.underlying.obj (projectSubobject (Subobject.mk f)))
hq : q ≫ T.map (projectSubobject (Subobject.mk f)).arrow = A.hom
⊢ mk q ≅ P

Tactic:
fapply isoMk

Goal state after:
case i.g
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : D
T : C ⥤ D
inst✝¹ : HasFiniteLimits C
inst✝ : PreservesFiniteLimits T
A P : StructuredArrow S T
f : P ⟶ A
hf : Mono f
q : S ⟶ T.obj (Subobject.underlying.obj (projectSubobject (Subobject.mk f)))
hq : q ≫ T.map (projectSubobject (Subobject.mk f)).arrow = A.hom
⊢ (mk q).right ≅ P.right

case w
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : D
T : C ⥤ D
inst✝¹ : HasFiniteLimits C
inst✝ : PreservesFiniteLimits T
A P : StructuredArrow S T
f : P ⟶ A
hf : Mono f
q : S ⟶ T.obj (Subobject.underlying.obj (projectSubobject (Subobject.mk f)))
hq : q ≫ T.map (projectSubobject (Subobject.mk f)).arrow = A.hom
⊢ autoParam ((mk q).hom ≫ T.map (Iso.hom ?i.g) = P.hom) isoMk._auto_1
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: case refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : P.op.IsDetecting
X Y : C
f : X ⟶ Y
hf : ∀ (G : C), P G → ∀ (h : X ⟶ G), ∃! h', f ≫ h' = h
⊢ IsIso f

pp: case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : P.IsCodetecting
X Y : Cᵒᵖ
f : X ⟶ Y
hf : ∀ (G : Cᵒᵖ), P.op G → ∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h
⊢ IsIso f

Tactic:
· refine (isIso_op_iff _).1 (hP _ fun G hG h => ?_)
    obtain ⟨t, ht, ht'⟩ := hf (unop G) hG h.unop
    exact
      ⟨t.op, Quiver.Hom.unop_inj ht, fun y hy => Quiver.Hom.unop_inj (ht' _ (Quiver.Hom.op_inj hy))⟩

Goal state after:
case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : P.IsCodetecting
X Y : Cᵒᵖ
f : X ⟶ Y
hf : ∀ (G : Cᵒᵖ), P.op G → ∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h
⊢ IsIso f
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: case refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : P.op.IsCodetecting
X Y : C
f : X ⟶ Y
hf : ∀ (G : C), P G → ∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h
⊢ IsIso f

pp: case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : P.IsDetecting
X Y : Cᵒᵖ
f : X ⟶ Y
hf : ∀ (G : Cᵒᵖ), P.op G → ∀ (h : X ⟶ G), ∃! h', f ≫ h' = h
⊢ IsIso f

Tactic:
· refine (isIso_op_iff _).1 (hP _ fun G hG h => ?_)
    obtain ⟨t, ht, ht'⟩ := hf (unop G) hG h.unop
    exact
      ⟨t.op, Quiver.Hom.unop_inj ht, fun y hy => Quiver.Hom.unop_inj (ht' _ (Quiver.Hom.op_inj hy))⟩

Goal state after:
case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : P.IsDetecting
X Y : Cᵒᵖ
f : X ⟶ Y
hf : ∀ (G : Cᵒᵖ), P.op G → ∀ (h : X ⟶ G), ∃! h', f ≫ h' = h
⊢ IsIso f
Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
⊢ ∀ {X_1 Y_1 Z : WalkingParallelFamily J} (f_1 : X_1 ⟶ Y_1) (g : Y_1 ⟶ Z),
    (match X_1, Z, f_1 ≫ g with
      | x, .(x), Hom.id .(x) => 𝟙 (WalkingParallelFamily.casesOn x X Y)
      | .(zero), .(one), line j => f j) =
      (match X_1, Y_1, f_1 with
        | x, .(x), Hom.id .(x) => 𝟙 (WalkingParallelFamily.casesOn x X Y)
        | .(zero), .(one), line j => f j) ≫
        match Y_1, Z, g with
        | x, .(x), Hom.id .(x) => 𝟙 (WalkingParallelFamily.casesOn x X Y)
        | .(zero), .(one), line j => f j

Tactic:
rintro _ _ _ ⟨⟩ ⟨⟩ <;>
      · cat_disch

Goal state after: