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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasZeroMorphisms C
X Y : C
P : Subobject Y
f : X ⟶ Y
h : P.Factors f
⊢ P.factorThru f h = 0 ↔ f = 0

Tactic:
fconstructor
  · intro w
    replace w := w =≫ P.arrow
    simpa using w
  · rintro rfl
    ext
    simp

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

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

Tactic:
| _ t
   => 

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

Goal state before:
pp: case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : Mono f
inst✝ : Mono g
t : MonoOver X
⊢ (map (f ≫ g)).obj (Quotient.mk'' t) = (map g).obj ((map f).obj (Quotient.mk'' t))

Tactic:
| _ t
   => 

Goal state after:
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : Mono f
inst✝ : Mono g
t : MonoOver X
⊢ (map (f ≫ g)).obj (Quotient.mk'' t) = (map g).obj ((map f).obj (Quotient.mk'' t))
Module: Mathlib.CategoryTheory.Subobject.Limits

Goal state before:
pp: case refine_1
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝¹ : HasEqualizer f g
W : C
h : W ⟶ X
inst✝ : HasPullbacks C
⊢ (equalizerSubobject (h ≫ f) (h ≫ g)).Factors ((Subobject.pullback h).obj (equalizerSubobject f g)).arrow

pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝¹ : HasEqualizer f g
W : C
h : W ⟶ X
inst✝ : HasPullbacks C
⊢ ((Subobject.pullback h).obj (equalizerSubobject f g)).Factors (equalizerSubobject (h ≫ f) (h ≫ g)).arrow

Tactic:
· apply equalizerSubobject_factors
    have := (Subobject.isPullback h (equalizerSubobject f g)).w
    rw [← reassoc_of% (Subobject.isPullback h (equalizerSubobject f g)).w,
      ← reassoc_of% (Subobject.isPullback h (equalizerSubobject f g)).w,
      equalizerSubobject_arrow_comp]

Goal state after:
case refine_2
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝¹ : HasEqualizer f g
W : C
h : W ⟶ X
inst✝ : HasPullbacks C
⊢ ((Subobject.pullback h).obj (equalizerSubobject f g)).Factors (equalizerSubobject (h ≫ f) (h ≫ g)).arrow
Module: Mathlib.CategoryTheory.Subobject.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst✝ : Mono f
X₁ X₂ : Subobject X
h : (map f).obj X₁ = (map f).obj X₂
⊢ X₁ = X₂

Tactic:
induction X₁ using Subobject.ind
  induction X₂ using Subobject.ind
  simp only [map_mk] at h
  exact mk_eq_mk_of_comm _ _ (isoOfMkEqMk _ _ h) (by simp [← cancel_mono f])

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

Goal state before:
pp: case refine_2
C : Type u
inst✝³ : Category.{v, u} C
X✝ Y Z : C
inst✝² : HasZeroMorphisms C
f✝ : X✝ ⟶ Y
inst✝¹ : HasKernel f✝
inst✝ : HasCokernels C
X A B : C
f : A ⟶ X
g : B ⟶ X
hf : Mono f
hg : Mono g
h : Subobject.mk f ≤ Subobject.mk g
⊢ (cokernel.desc f (cokernel.π g) ⋯).op ≫ (cokernel.π f).op = (cokernel.π g).op

Tactic:
· exact Quiver.Hom.unop_inj (cokernel.π_desc _ _ _)

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
⊢ S.Exact ↔ IsIso (imageToKernel' S.f S.g ⋯)

Tactic:
by
  simp only [S.exact_iff_epi_imageToKernel', isIso_iff_mono_and_epi, iff_and_self]
  intro
  apply Limits.kernel.lift_mono

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

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✝² : Abelian C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : F.Additive
tfae_1_to_2 :
  (∀ (S : ShortComplex C), S.ShortExact → (S.map F).Exact ∧ Mono (F.map S.f)) →
    ∀ (S : ShortComplex C), S.Exact ∧ Mono S.f → (S.map F).Exact ∧ Mono (F.map S.f)
tfae_2_to_3 :
  (∀ (S : ShortComplex C), S.Exact ∧ Mono S.f → (S.map F).Exact ∧ Mono (F.map S.f)) →
    ∀ ⦃X Y : C⦄ (f : X ⟶ Y), PreservesLimit (parallelPair f 0) F
⊢ [∀ (S : ShortComplex C), S.ShortExact → (S.map F).Exact ∧ Mono (F.map S.f),
      ∀ (S : ShortComplex C), S.Exact ∧ Mono S.f → (S.map F).Exact ∧ Mono (F.map S.f),
      ∀ ⦃X Y : C⦄ (f : X ⟶ Y), PreservesLimit (parallelPair f 0) F, PreservesFiniteLimits F].TFAE

Tactic:
tfae_have 3 → 4
  | hF => by
    exact preservesFiniteLimits_of_preservesKernels F

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
inst✝² : Abelian C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : F.Additive
tfae_1_to_2 :
  (∀ (S : ShortComplex C), S.ShortExact → (S.map F).Exact ∧ Mono (F.map S.f)) →
    ∀ (S : ShortComplex C), S.Exact ∧ Mono S.f → (S.map F).Exact ∧ Mono (F.map S.f)
tfae_2_to_3 :
  (∀ (S : ShortComplex C), S.Exact ∧ Mono S.f → (S.map F).Exact ∧ Mono (F.map S.f)) →
    ∀ ⦃X Y : C⦄ (f : X ⟶ Y), PreservesLimit (parallelPair f 0) F
tfae_3_to_4 : (∀ ⦃X Y : C⦄ (f : X ⟶ Y), PreservesLimit (parallelPair f 0) F) → PreservesFiniteLimits F
⊢ [∀ (S : ShortComplex C), S.ShortExact → (S.map F).Exact ∧ Mono (F.map S.f),
      ∀ (S : ShortComplex C), S.Exact ∧ Mono S.f → (S.map F).Exact ∧ Mono (F.map S.f),
      ∀ ⦃X Y : C⦄ (f : X ⟶ Y), PreservesLimit (parallelPair f 0) F, PreservesFiniteLimits F].TFAE
Module: Mathlib.Algebra.Homology.ShortComplex.ExactFunctor

Goal state before:
pp: case refine_1
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Abelian C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : F.Additive
x✝ : ∀ (S : ShortComplex C), S.ShortExact → (S.map F).ShortExact
hF : ∀ (S : ShortComplex C), S.ShortExact → (S.map F).ShortExact := x✝
X Y : C
f : X ⟶ Y
⊢ PreservesLimit (parallelPair f 0) F

Tactic:
have h := (preservesFiniteLimits_tfae F |>.out 0 2 |>.1 fun S hS ↦
        And.intro (hF S hS).exact (hF S hS).mono_f)

Goal state after:
case refine_1
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Abelian C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : F.Additive
x✝ : ∀ (S : ShortComplex C), S.ShortExact → (S.map F).ShortExact
hF : ∀ (S : ShortComplex C), S.ShortExact → (S.map F).ShortExact := x✝
X Y : C
f : X ⟶ Y
h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), PreservesLimit (parallelPair f 0) F
⊢ PreservesLimit (parallelPair f 0) F
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.PreservesMonomorphisms
inst✝ : ∀ {X Y : A} (f : X ⟶ Y), PreservesColimit (parallelPair f 0) L
⊢ L.PreservesHomology

Tactic:
apply preservesHomology_of_map_exact
  intro S hS
  let φ : (ShortComplex.mk _ _ (Abelian.comp_coimage_π_eq_zero S.zero)).map L ⟶ S.map L :=
    { τ₁ := 𝟙 _
      τ₂ := 𝟙 _
      τ₃ := L.map (Abelian.factorThruCoimage S.g)
      comm₂₃ := by
        dsimp
        rw [Category.id_comp, ← L.map_comp, cokernel.π_desc] }
  apply (ShortComplex.exact_iff_of_epi_of_isIso_of_mono φ).1
  apply ShortComplex.exact_of_g_is_cokernel
  exact CokernelCofork.mapIsColimit _ ((S.exact_iff_exact_coimage_π).1 hS).gIsCokernel L

Goal state after:
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✝¹ : LocallySmall.{w, v₁, u₁} C
inst✝ : WellPowered.{w, v₁, u₁} C
A : C
s : Set (Subobject A)
f : Subobject A
k : ∀ g ∈ s, f ≤ g
j : ↑(⇑(equivShrink (Subobject A)) '' s)
⊢ (equivShrink (Subobject A)).symm ↑j ∈ s

Tactic:
rcases j with ⟨-, ⟨g, ⟨m, rfl⟩⟩⟩

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : LocallySmall.{w, v₁, u₁} C
inst✝ : WellPowered.{w, v₁, u₁} C
A : C
s : Set (Subobject A)
f : Subobject A
k : ∀ g ∈ s, f ≤ g
g : Subobject A
m : g ∈ s
⊢ (equivShrink (Subobject A)).symm ↑⟨(equivShrink (Subobject A)) g, ⋯⟩ ∈ s
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X : Type v₂
α : Type u_1
Z : α → C
inst✝ : HasCoproduct Z
x✝ : Discrete α
⊢ (Discrete.functor (((Discrete.opposite α).inverse ⋙ (Discrete.functor Z).op).obj ∘ Discrete.mk)).obj x✝ ≅
    (Discrete.functor fun x ↦ op (Z x)).obj x✝

Tactic:
by rfl

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X : Type v₂
α : Type u_1
Z : α → C
inst✝ : HasProduct Z
x✝ : Discrete α
⊢ (Discrete.functor (((Discrete.opposite α).inverse ⋙ (Discrete.functor Z).op).obj ∘ Discrete.mk)).obj x✝ ≅
    (Discrete.functor fun x ↦ op (Z x)).obj x✝

Tactic:
by rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.Filtered

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
α : Type w
inst✝² : HasFiniteCoproducts C
f : α → C
inst✝¹ : HasColimitsOfShape (Finset (Discrete α)) C
inst✝ : HasCoproduct f
S : Finset (Discrete α)
j : ↥S
⊢ Sigma.ι (fun x ↦ f (↑x).as) j ≫
      colimit.ι (liftToFinsetObj (Discrete.functor f)) S ≫
        ((liftToFinsetColimitCocone (Discrete.functor f)).isColimit.coconePointUniqueUpToIso
            (colimit.isColimit (Discrete.functor f))).hom =
    Sigma.ι (fun x ↦ f (↑x).as) j ≫ Sigma.desc fun s ↦ Sigma.ι f (↑s).as

Tactic:
rw [← Category.assoc]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
α : Type w
inst✝² : HasFiniteCoproducts C
f : α → C
inst✝¹ : HasColimitsOfShape (Finset (Discrete α)) C
inst✝ : HasCoproduct f
S : Finset (Discrete α)
j : ↥S
⊢ (Sigma.ι (fun x ↦ f (↑x).as) j ≫ colimit.ι (liftToFinsetObj (Discrete.functor f)) S) ≫
      ((liftToFinsetColimitCocone (Discrete.functor f)).isColimit.coconePointUniqueUpToIso
          (colimit.isColimit (Discrete.functor f))).hom =
    Sigma.ι (fun x ↦ f (↑x).as) j ≫ Sigma.desc fun s ↦ Sigma.ι f (↑s).as
Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A F G : Cᵒᵖ ⥤ Type v
η : F ⟶ A
μ : G ⟶ A
ε : F ⟶ G
hε : ε ≫ μ = η
X : C
s : yoneda.obj X ⟶ A
u : F.obj (op X)
h : MakesOverArrow η s u
⊢ (ConcreteCategory.hom (ε.app (op X) ≫ μ.app (op X))) u = yonedaEquiv s

Tactic:
← NatTrans.comp_app,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
A F G : Cᵒᵖ ⥤ Type v
η : F ⟶ A
μ : G ⟶ A
ε : F ⟶ G
hε : ε ≫ μ = η
X : C
s : yoneda.obj X ⟶ A
u : F.obj (op X)
h : MakesOverArrow η s u
⊢ (ConcreteCategory.hom ((ε ≫ μ).app (op X))) u = yonedaEquiv s
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✝³ : L.Full
inst✝² : L.Faithful
F : C ⥤ H
inst✝¹ : L.HasPointwiseLeftKanExtension F
inst✝ : ∀ (F : C ⥤ H), L.HasLeftKanExtension F
⊢ IsIso ((L.lanAdjunction H).unit.app F)

Tactic:
rw [lanAdjunction_unit]

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✝³ : L.Full
inst✝² : L.Faithful
F : C ⥤ H
inst✝¹ : L.HasPointwiseLeftKanExtension F
inst✝ : ∀ (F : C ⥤ H), L.HasLeftKanExtension F
⊢ IsIso (L.lanUnit.app F)
Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise

Goal state before:
pp: 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
inst✝ : L.HasPointwiseRightKanExtension F
X : D
j : StructuredArrow X L
⊢ (limit.cone (StructuredArrow.proj X L ⋙ F)).π.app j =
    (Iso.refl (limit.cone (StructuredArrow.proj X L ⋙ F)).pt).hom ≫
      ((RightExtension.mk (L.pointwiseRightKanExtension F) (L.pointwiseRightKanExtensionCounit F)).coneAt X).π.app j

Tactic:
dsimp
    simp only [limit.lift_π, StructuredArrow.map_mk, id_comp]
    congr
    rw [comp_id, ← StructuredArrow.eq_mk]

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)))
a : (precomp₂ L' α).obj b ⟶ y
t : C
a_w_t :
  (StructuredArrow.hom ((precomp₂ L' α).obj b) ≫
          ((whiskeringLeft C D' H).obj (L ⋙ L')).map (StructuredArrow.Hom.right a)).app
      t =
    (StructuredArrow.hom y).app t
hb_fac_app :
  (StructuredArrow.hom b ≫ ((whiskeringLeft D D' H).obj L').map (hb.desc u)).app (L.obj t) =
    (StructuredArrow.hom u).app (L.obj t)
⊢ α.app t ≫ (StructuredArrow.hom b).app (L.obj t) ≫ (StructuredArrow.Hom.right a).app (L'.obj (L.obj t)) =
    α.app t ≫ (StructuredArrow.hom b).app (L.obj t) ≫ (hb.desc u).app (L'.obj (L.obj t))

Tactic:
have hα_fac_app :=
      congr_app
        (hα.fac <| LeftExtension.mk _ <|
          y.hom ≫ (L.associator L' y.right).hom) t

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)))
a : (precomp₂ L' α).obj b ⟶ y
t : C
a_w_t :
  (StructuredArrow.hom ((precomp₂ L' α).obj b) ≫
          ((whiskeringLeft C D' H).obj (L ⋙ L')).map (StructuredArrow.Hom.right a)).app
      t =
    (StructuredArrow.hom y).app t
hb_fac_app :
  (StructuredArrow.hom b ≫ ((whiskeringLeft D D' H).obj L').map (hb.desc u)).app (L.obj t) =
    (StructuredArrow.hom u).app (L.obj t)
hα_fac_app :
  (StructuredArrow.hom (mk F₁ α) ≫
          ((whiskeringLeft C D H).obj L).map
            (hα.desc
              (mk (L' ⋙ StructuredArrow.right y)
                (StructuredArrow.hom y ≫ (L.associator L' (StructuredArrow.right y)).hom)))).app
      t =
    (StructuredArrow.hom
          (mk (L' ⋙ StructuredArrow.right y)
            (StructuredArrow.hom y ≫ (L.associator L' (StructuredArrow.right y)).hom))).app
      t
⊢ α.app t ≫ (StructuredArrow.hom b).app (L.obj t) ≫ (StructuredArrow.Hom.right a).app (L'.obj (L.obj t)) =
    α.app t ≫ (StructuredArrow.hom b).app (L.obj t) ≫ (hb.desc u).app (L'.obj (L.obj t))
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'
F' : D ⥤ H
L : C ⥤ D
F : C ⥤ H
α : L ⋙ F' ⟶ F
inst✝ : F'.IsRightKanExtension α
c : Cone F
hc : IsLimit c
s : Cone F'
m : s.pt ⟶ (F'.coneOfIsRightKanExtension α c).pt
hm : ∀ (j : D), m ≫ (F'.coneOfIsRightKanExtension α c).π.app j = s.π.app j
j : C
this : m ≫ (F'.coneOfIsRightKanExtension α c).π.app (L.obj j) = s.π.app (L.obj j)
⊢ m ≫ c.π.app j = hc.lift { pt := s.1, π := L.whiskerLeft s.π ≫ α } ≫ c.π.app j

Tactic:
nth_rw 1 [← F'.liftOfIsRightKanExtension_fac_app α ((const D).obj c.pt)]

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'
F' : D ⥤ H
L : C ⥤ D
F : C ⥤ H
α : L ⋙ F' ⟶ F
inst✝ : F'.IsRightKanExtension α
c : Cone F
hc : IsLimit c
s : Cone F'
m : s.pt ⟶ (F'.coneOfIsRightKanExtension α c).pt
hm : ∀ (j : D), m ≫ (F'.coneOfIsRightKanExtension α c).π.app j = s.π.app j
j : C
this : m ≫ (F'.coneOfIsRightKanExtension α c).π.app (L.obj j) = s.π.app (L.obj j)
⊢ m ≫ (F'.liftOfIsRightKanExtension α ((const D).obj c.pt) c.π).app (L.obj j) ≫ α.app j =
    hc.lift { pt := s.1, π := L.whiskerLeft s.π ≫ α } ≫ c.π.app j
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✝ : ℰᵒᵖ ⥤ Type (max w v₁ v₂)
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₂)
X Y : ℰ
f : L.obj P ⟶ X
g : X ⟶ Y
⊢ (restrictedULiftYonedaHomEquiv L α P Y) (f ≫ g) =
    (restrictedULiftYonedaHomEquiv L α P X) f ≫ (restrictedULiftYoneda A).map g

Tactic:
have := @IsColimit.homEquiv_symm_naturality (h :=
          Functor.isPointwiseLeftKanExtensionOfIsLeftKanExtension L α P)
        dsimp at this
        apply (restrictedULiftYonedaHomEquiv L α P Y).symm.injective
        apply (Functor.isPointwiseLeftKanExtensionOfIsLeftKanExtension L α P).hom_ext
        intro
        simp [restrictedULiftYonedaHomEquiv,
          restrictedULiftYonedaHomEquiv'_symm_naturality_right, this]

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

Goal state before:
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
G : C
hG : P G
h : unop Y ⟶ G
t : op G ⟶ X
ht : t ≫ f = h.op
ht' : ∀ (y : op G ⟶ X), (fun h' ↦ h' ≫ f = h.op) y → y = t
⊢ ∃! h', f.unop ≫ h' = h

Tactic:
refine ⟨t.unop, Quiver.Hom.op_inj ht, fun y hy => Quiver.Hom.op_inj (ht' _ ?_)⟩

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
G : C
hG : P G
h : unop Y ⟶ G
t : op G ⟶ X
ht : t ≫ f = h.op
ht' : ∀ (y : op G ⟶ X), (fun h' ↦ h' ≫ f = h.op) y → y = t
y : unop X ⟶ G
hy : (fun h' ↦ f.unop ≫ h' = h) y
⊢ (fun h' ↦ h' ≫ f = h.op) y.op
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
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
G : C
hG : P G
h : G ⟶ unop X
t : Y ⟶ op G
ht : f ≫ t = h.op
ht' : ∀ (y : Y ⟶ op G), (fun h' ↦ f ≫ h' = h.op) y → y = t
⊢ ∃! h', h' ≫ f.unop = h

Tactic:
refine ⟨t.unop, Quiver.Hom.op_inj ht, fun y hy => Quiver.Hom.op_inj (ht' _ ?_)⟩

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
G : C
hG : P G
h : G ⟶ unop X
t : Y ⟶ op G
ht : f ≫ t = h.op
ht' : ∀ (y : Y ⟶ op G), (fun h' ↦ f ≫ h' = h.op) y → y = t
y : G ⟶ unop Y
hy : (fun h' ↦ h' ≫ f.unop = h) y
⊢ (fun h' ↦ f ≫ h' = h.op) y.op
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: case mpr.refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : P.IsDetecting
X Y : C
f : X ⟶ Y
inst✝ : Mono f
hf : ∀ (G : C), P G → Function.Surjective ⇑(ConcreteCategory.hom ((coyoneda.obj (op G)).map f))
A : C
hA : P A
g : A ⟶ Y
⊢ ∀ (y₁ y₂ : A ⟶ X), y₁ ≫ f = g → y₂ ≫ f = g → y₁ = y₂

Tactic:
· intro l₁ l₂ h₁ h₂
      rw [← cancel_mono f, h₁, h₂]

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.limitsOfShape J X
⊢ P.IsCoseparating

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

Goal state after:
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
u : F.Elementsᵒᵖ
X Y : C
f : X ⟶ Y
x : (((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.flip).obj u).obj X
⊢ (ConcreteCategory.hom
          ((((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.flip).obj u).map f ≫
            (coconeπOpCompShrinkYonedaObj F Y).ι.app u)).toFun
      x =
    (ConcreteCategory.hom
          ((coconeπOpCompShrinkYonedaObj F X).ι.app u ≫ (((const F.Elementsᵒᵖ).obj F).obj u).map f)).toFun
      x

Tactic:
obtain ⟨x, rfl⟩ := shrinkYonedaObjObjEquiv.symm.surjective x

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : LocallySmall.{w, v₁, u₁} C
F : C ⥤ Type w
u : F.Elementsᵒᵖ
X Y : C
f : X ⟶ Y
x : unop ((CategoryOfElements.π F).op.obj u) ⟶ X
⊢ (ConcreteCategory.hom
          ((((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.flip).obj u).map f ≫
            (coconeπOpCompShrinkYonedaObj F Y).ι.app u)).toFun
      (shrinkYonedaObjObjEquiv.symm x) =
    (ConcreteCategory.hom
          ((coconeπOpCompShrinkYonedaObj F X).ι.app u ≫ (((const F.Elementsᵒᵖ).obj F).obj u).map f)).toFun
      (shrinkYonedaObjObjEquiv.symm x)
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
u v : F.Elementsᵒᵖ
g : u ⟶ v
X : C
x : (((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.flip).obj u).obj X
⊢ (ConcreteCategory.hom
          ((((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.flip).map g ≫
                { app := fun X ↦ (coconeπOpCompShrinkYonedaObj F X).ι.app v, naturality := ⋯ }).app
            X)).toFun
      x =
    (ConcreteCategory.hom
          (({ app := fun X ↦ (coconeπOpCompShrinkYonedaObj F X).ι.app u, naturality := ⋯ } ≫
                ((const F.Elementsᵒᵖ).obj F).map g).app
            X)).toFun
      x

Tactic:
obtain ⟨x, rfl⟩ := shrinkYonedaObjObjEquiv.symm.surjective x

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : LocallySmall.{w, v₁, u₁} C
F : C ⥤ Type w
u v : F.Elementsᵒᵖ
g : u ⟶ v
X : C
x : unop ((CategoryOfElements.π F).op.obj u) ⟶ X
⊢ (ConcreteCategory.hom
          ((((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.flip).map g ≫
                { app := fun X ↦ (coconeπOpCompShrinkYonedaObj F X).ι.app v, naturality := ⋯ }).app
            X)).toFun
      (shrinkYonedaObjObjEquiv.symm x) =
    (ConcreteCategory.hom
          (({ app := fun X ↦ (coconeπOpCompShrinkYonedaObj F X).ι.app u, naturality := ⋯ } ≫
                ((const F.Elementsᵒᵖ).obj F).map g).app
            X)).toFun
      (shrinkYonedaObjObjEquiv.symm x)
Module: Mathlib.Algebra.Ring.NegOnePow

Goal state before:
pp: n₁ n₂ : ℤ
⊢ (n₁ - n₂).negOnePow = n₁.negOnePow * n₂.negOnePow

Tactic:
simp only [sub_eq_add_neg, negOnePow_add, negOnePow_neg]

Goal state after:
Module: Mathlib.Algebra.Ring.Periodic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
c c₁ c₂ x✝ : α
inst✝ : AddGroup α
h : Periodic f c
x : α ⧸ AddSubgroup.zmultiples c
a b : α
h' : (QuotientAddGroup.leftRel (AddSubgroup.zmultiples c)) a b
⊢ f a = f b

Tactic:
rw [QuotientAddGroup.leftRel_apply] at h'

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
c c₁ c₂ x✝ : α
inst✝ : AddGroup α
h : Periodic f c
x : α ⧸ AddSubgroup.zmultiples c
a b : α
h' : -a + b ∈ AddSubgroup.zmultiples c
⊢ f a = f b