mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Category.Grp.EpiMono

Goal state before:
pp: case refine_2
A B : GrpCat
f : A ⟶ B
b : ↑B
hb : h b = g b
r : b ∉ ↑(Hom.hom f).range
⊢ False

Tactic:
· have eq1 : (h b) (fromCoset ⟨f.hom.range, 1, one_leftCoset _⟩) =
        fromCoset ⟨f.hom.range, 1, one_leftCoset _⟩ := by
      change ((τ).symm.trans (g b)).trans τ _ = _
      dsimp [tau]
      simp [g_apply_infinity f]
    have eq2 :
        g b (fromCoset ⟨f.hom.range, 1, one_leftCoset _⟩) = fromCoset ⟨b • ↑f.hom.range, b, rfl⟩ :=
      rfl
    exact (fromCoset_ne_of_nin_range _ r).symm (by rw [← eq1, ← eq2, DFunLike.congr_fun hb])

Goal state after:
Module: Mathlib.Algebra.Category.Grp.EpiMono

Goal state before:
pp: A B : GrpCat
f : A ⟶ B
⊢ ↑(Hom.hom f).range = {x | h x = g x}

Tactic:
by
  refine Set.ext fun b => ⟨?_, fun hb : h b = g b => by_contradiction fun r => ?_⟩
  · rintro ⟨a, rfl⟩
    change h (f a) = g (f a)
    ext ⟨⟨_, ⟨y, rfl⟩⟩⟩
    · rw [g_apply_fromCoset]
      by_cases m : y ∈ f.hom.range
      · rw [h_apply_fromCoset' _ _ _ m, fromCoset_eq_of_mem_range _ m]
        change fromCoset _ = fromCoset ⟨f a • (y • _), _⟩
        simp only [← fromCoset_eq_of_mem_range _ (Subgroup.mul_mem _ ⟨a, rfl⟩ m), smul_smul]
      · rw [h_apply_fromCoset_nin_range f (f a) ⟨_, rfl⟩ _ m]
        simp only [leftCoset_assoc]
    · rw [g_apply_infinity, h_apply_infinity f (f a) ⟨_, rfl⟩]
  · have eq1 : (h b) (fromCoset ⟨f.hom.range, 1, one_leftCoset _⟩) =
        fromCoset ⟨f.hom.range, 1, one_leftCoset _⟩ := by
      change ((τ).symm.trans (g b)).trans τ _ = _
      dsimp [tau]
      simp [g_apply_infinity f]
    have eq2 :
        g b (fromCoset ⟨f.hom.range, 1, one_leftCoset _⟩) = fromCoset ⟨b • ↑f.hom.range, b, rfl⟩ :=
      rfl
    exact (fromCoset_ne_of_nin_range _ r).symm (by rw [← eq1, ← eq2, DFunLike.congr_fun hb])

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

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
S₁ S₂ S₃ : ShortComplex C
inst✝² : S₁.HasHomology
inst✝¹ : S₂.HasHomology
inst✝ : S₃.HasHomology
φ : S₁ ⟶ S₂
φ' : S₂ ⟶ S₃
hφ : QuasiIso φ
hφφ' : QuasiIso (φ ≫ φ')
⊢ QuasiIso φ'

Tactic:
rw [quasiIso_iff] at hφ hφφ' ⊢

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
S₁ S₂ S₃ : ShortComplex C
inst✝² : S₁.HasHomology
inst✝¹ : S₂.HasHomology
inst✝ : S₃.HasHomology
φ : S₁ ⟶ S₂
φ' : S₂ ⟶ S₃
hφ : IsIso (homologyMap φ)
hφφ' : IsIso (homologyMap (φ ≫ φ'))
⊢ IsIso (homologyMap φ')
Module: Mathlib.Algebra.Homology.ShortComplex.Homology

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ S₄ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.HomologyData
h₂ : S₂.HomologyData
h : S.HomologyData
⊢ IsIso (leftRightHomologyComparison' h.left h.right)

Tactic:
rw [h.leftRightHomologyComparison'_eq]
    infer_instance

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
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
⊢ h₁.homologyIso.hom ≫ rightHomologyMap' φ h₁ h₂ = homologyMap φ ≫ h₂.homologyIso.hom

Tactic:
rw [← cancel_epi h₁.homologyIso.inv, Iso.inv_hom_id_assoc,
    ← cancel_epi (leftRightHomologyComparison' S₁.leftHomologyData h₁),
    ← leftRightHomologyComparison'_naturality φ S₁.leftHomologyData h₁ S₂.leftHomologyData h₂,
    ← cancel_epi (S₁.leftHomologyData.homologyIso.hom),
    LeftHomologyData.leftHomologyIso_hom_naturality_assoc,
    leftRightHomologyComparison'_fac, leftRightHomologyComparison'_fac, assoc,
    Iso.hom_inv_id_assoc, Iso.hom_inv_id_assoc, Iso.hom_inv_id_assoc]

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
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
φ : S₁ ⟶ S₂
⊢ S₁.homologyπ ≫ homologyMap φ ≫ S₂.homologyι = S₁.iCycles ≫ φ.τ₂ ≫ S₂.pOpcycles

Tactic:
simp only [homologyι_naturality, homology_π_ι_assoc, p_opcyclesMap]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
⊢ (leftHomologyMap' φ h₁ h₂).op = rightHomologyMap' (opMap φ) h₂.op h₁.op

Tactic:
by
  let γ : LeftHomologyMapData φ h₁ h₂ := leftHomologyMapData φ h₁ h₂
  simp only [γ.leftHomologyMap'_eq, γ.op.rightHomologyMap'_eq,
    LeftHomologyMapData.op_φH]

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

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝⁴ : S₁.HasRightHomology
inst✝³ : S₂.HasRightHomology
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
⊢ IsIso (rightHomologyMap φ)

Tactic:
dsimp only [rightHomologyMap]

Goal state after:
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝⁴ : S₁.HasRightHomology
inst✝³ : S₂.HasRightHomology
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
⊢ IsIso (rightHomologyMap' φ S₁.rightHomologyData S₂.rightHomologyData)
Module: Mathlib.Algebra.Homology.ShortComplex.PreservesHomology

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✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
S S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
ψ : RightHomologyMapData φ h₁ h₂
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : h₁.IsPreservedBy F
inst✝ : h₂.IsPreservedBy F
⊢ F.map ψ.φQ ≫ (h₂.map F).g' = (h₁.map F).g' ≫ (F.mapShortComplex.map φ).τ₃

Tactic:
simpa only [RightHomologyData.map_g', F.map_comp] using! F.congr_map ψ.commg'

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
S : ShortComplex C
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 ι
⊢ (isoHomology S hkf hcc fac).hom ≫ S.homologyι ≫ (S.isoOpcyclesOfIsColimit hcc).inv = ι

Tactic:
← isoHomology_hom_comp_ι S hkf hcc fac,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
S : ShortComplex C
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 ι
⊢ (isoHomology S hkf hcc fac).hom ≫ (isoHomology S hkf hcc fac).inv ≫ ι = ι
Module: Mathlib.Algebra.Homology.ShortComplex.PreservesHomology

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✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
S : ShortComplex C
hf : S.f = 0
inst✝ : PreservesLimit (parallelPair S.g 0) F
h : S.LeftHomologyData
⊢ PreservesLimit (parallelPair S.g 0) F

Tactic:
by infer_instance

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

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✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
S : ShortComplex C
hg : S.g = 0
inst✝ : PreservesColimit (parallelPair S.f 0) F
h : S.RightHomologyData
⊢ PreservesColimit (parallelPair S.f 0) F

Tactic:
by infer_instance

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

Goal state before:
pp: case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
h : Retract X Y
i : Injective Y
A B : C
f : A ⟶ X
e : A ⟶ B
x✝ : Mono e
g : B ⟶ Y
hg : e ≫ g = f ≫ h.i
⊢ e ≫ g ≫ h.r = f

Tactic:
simp [Category.assoc', hg]

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

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
inst✝ : HasLimits C
⊢ HasLimits (Skeleton C)

Tactic:
by infer_instance

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

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
inst✝ : HasColimits C
⊢ HasColimits (Skeleton C)

Tactic:
by infer_instance

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✝ : ∀ {X Y : C} (f : X ⟶ Y), PreservesLimit (parallelPair f 0) F
X Y : C
f g : X ⟶ Y
this✝ : PreservesBinaryBiproducts F := preservesBinaryBiproducts_of_preservesBinaryProducts F
this : F.Additive
c : Cone (parallelPair f g)
i : IsLimit c
c' : IsLimit (KernelFork.ofι (Fork.ι c) ⋯) := isLimitKernelForkOfFork (i.ofIsoLimit (Fork.isoForkOfι c))
iFc : IsLimit (KernelFork.ofι (F.map (Fork.ι c)) ⋯) := isLimitForkMapOfIsLimit' F ⋯ c'
p : parallelPair (F.map (f - g)) 0 ≅ parallelPair (F.map f - F.map g) 0 := parallelPair.eqOfHomEq ⋯ ⋯
⊢ (Iso.refl (forkOfKernelFork ((Cone.postcompose p.hom).obj (KernelFork.ofι (F.map (Fork.ι c)) ⋯))).pt).hom ≫
      (Fork.ofι (F.map (Fork.ι c)) ⋯).ι =
    (forkOfKernelFork ((Cone.postcompose p.hom).obj (KernelFork.ofι (F.map (Fork.ι c)) ⋯))).ι

Tactic:
by simp [p]

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✝ : ∀ {X Y : C} (f : X ⟶ Y), PreservesColimit (parallelPair f 0) F
X Y : C
f g : X ⟶ Y
this✝ : PreservesBinaryBiproducts F := preservesBinaryBiproducts_of_preservesBinaryCoproducts F
this : F.Additive
c : Cocone (parallelPair f g)
i : IsColimit c
c' : IsColimit (CokernelCofork.ofπ (Cofork.π c) ⋯) :=
  isColimitCokernelCoforkOfCofork (i.ofIsoColimit (Cofork.isoCoforkOfπ c))
iFc : IsColimit (CokernelCofork.ofπ (F.map (Cofork.π c)) ⋯) := isColimitCoforkMapOfIsColimit' F ⋯ c'
p : parallelPair (F.map (f - g)) 0 ≅ parallelPair (F.map f - F.map g) 0 :=
  parallelPair.ext (Iso.refl ((parallelPair (F.map (f - g)) 0).obj WalkingParallelPair.zero))
    (Iso.refl ((parallelPair (F.map (f - g)) 0).obj WalkingParallelPair.one)) ⋯ ⋯
⊢ (coforkOfCokernelCofork ((Cocone.precompose p.symm.hom).obj (CokernelCofork.ofπ (F.map (Cofork.π c)) ⋯))).π ≫
      (Iso.refl
          (coforkOfCokernelCofork
              ((Cocone.precompose p.symm.hom).obj (CokernelCofork.ofπ (F.map (Cofork.π c)) ⋯))).pt).hom =
    (Cofork.ofπ (F.map (Cofork.π c)) ⋯).π

Tactic:
by simp [p]

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

Goal state before:
pp: case mpr
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
inst✝ : S.HasHomology
h : S.RightHomologyData
⊢ Mono h.g' → S.Exact

Tactic:
· intro
    simp only [h.exact_iff, IsZero.iff_id_eq_zero, ← cancel_mono h.ι, ← cancel_mono h.g',
      id_comp, h.ι_g', zero_comp]

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
P : Subobject Z
f : X ⟶ Y
g : Y ⟶ Z
h : P.Factors g
⊢ f ≫ P.factorThru g h = P.factorThru (f ≫ g) ⋯

Tactic:
by
  apply (cancel_mono P.arrow).mp
  simp

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
e : C ≌ D
inst✝² : LocallySmall.{w, v, u₁} C
inst✝¹ : LocallySmall.{w, v₂, u₂} D
inst✝ : WellPowered.{w, v, u₁} C
X : D
⊢ EssentiallySmall.{w, v, max u₁ v} (MonoOver (e.symm.functor.obj X))

Tactic:
by infer_instance

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

Goal state before:
pp: case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
⊢ S.f = 0 ∧ S.g = 0 → IsZero S.X₂

Tactic:
rintro ⟨hf, hg⟩

Goal state after:
case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
hf : S.f = 0
hg : S.g = 0
⊢ IsZero S.X₂
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
f : X ⟶ Y
inst✝ : Mono f
g h : MonoOver X
e : (map f).obj g ⟶ (map f).obj h
⊢ Over.Hom.left e.hom ≫ h.arrow = g.arrow

Tactic:
rw [← cancel_mono f, assoc]
      apply w e

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type u₃
inst✝¹ : Category.{v₃, u₃} J
inst✝ : HasFiniteLimits (Over X)
x✝² : Type
x✝¹ : SmallCategory x✝²
x✝ : FinCategory x✝²
⊢ HasLimitsOfShape x✝² (Subobject X)

Tactic:
by infer_instance

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type u₃
inst✝¹ : Category.{v₃, u₃} J
inst✝ : HasLimitsOfSize.{w, w', v₁, max u₁ v₁} (Over X)
x✝¹ : Type w'
x✝ : Category.{w, w'} x✝¹
⊢ HasLimitsOfShape x✝¹ (Subobject X)

Tactic:
by infer_instance

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
X : C
f : MonoOver X
⊢ Quotient.mk'' f ≤ Quotient.mk'' ⊤

Tactic:
exact ⟨MonoOver.leTop f⟩

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 ∧ Epi (F.map S.g)) →
    ∀ (S : ShortComplex C), S.Exact ∧ Epi S.g → (S.map F).Exact ∧ Epi (F.map S.g)
hF : ∀ (S : ShortComplex C), S.Exact ∧ Epi S.g → (S.map F).Exact ∧ Epi (F.map S.g)
X Y : C
f : X ⟶ Y
S : ShortComplex C := { X₁ := X, X₂ := Y, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }
hS : (S.map F).Exact ∧ Epi (F.map S.g) := hF S ⟨exact_cokernel f, inferInstance⟩
⊢ IsColimit (CokernelCofork.map (Cofork.ofπ (cokernel.π f) ⋯) F)

Tactic:
have : Epi (S.map F).g := hS.2

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 ∧ Epi (F.map S.g)) →
    ∀ (S : ShortComplex C), S.Exact ∧ Epi S.g → (S.map F).Exact ∧ Epi (F.map S.g)
hF : ∀ (S : ShortComplex C), S.Exact ∧ Epi S.g → (S.map F).Exact ∧ Epi (F.map S.g)
X Y : C
f : X ⟶ Y
S : ShortComplex C := { X₁ := X, X₂ := Y, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }
hS : (S.map F).Exact ∧ Epi (F.map S.g) := hF S ⟨exact_cokernel f, inferInstance⟩
this : Epi (S.map F).g
⊢ IsColimit (CokernelCofork.map (Cofork.ofπ (cokernel.π f) ⋯) F)
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
s t : (CostructuredArrow yoneda A)ᵒᵖ
f : t ⟶ s
x : F.obj t
⊢ (ConcreteCategory.hom (F.map (eqToHom ⋯)))
      (YonedaCollection.snd ((counitForward F (unop t) x).map₂ f.unop.left ⋯).val) =
    YonedaCollection.snd (counitForward F (unop s) ((ConcreteCategory.hom (F.map f)) x)).val

Tactic:
have : (CostructuredArrow.mkPrecomp t.unop.hom f.unop.left).op =
      f ≫ eqToHom (by simp [← CostructuredArrow.eq_mk]) := by
    apply Quiver.Hom.unop_inj
    simp

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
s t : (CostructuredArrow yoneda A)ᵒᵖ
f : t ⟶ s
x : F.obj t
this : (CostructuredArrow.mkPrecomp (unop t).hom f.unop.left).op = f ≫ eqToHom ⋯
⊢ (ConcreteCategory.hom (F.map (eqToHom ⋯)))
      (YonedaCollection.snd ((counitForward F (unop t) x).map₂ f.unop.left ⋯).val) =
    YonedaCollection.snd (counitForward F (unop s) ((ConcreteCategory.hom (F.map f)) x)).val
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 : 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),
    liftSubobject (projectSubobject (Subobject.mk f)) hq = Subobject.mk f

Tactic:
q

Goal state after:
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),
    liftSubobject (projectSubobject (Subobject.mk f)) hq = Subobject.mk f
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
P : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
hf : 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:
q

Goal state after:
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
P : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
hf : 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
Module: Mathlib.CategoryTheory.Limits.Presheaf

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : (Cᵒᵖ ⥤ Type (max w v₁ v₂)) ⥤ Dᵒᵖ ⥤ Type (max w v₁ v₂)
φ : F ⋙ uliftYoneda.{max w v₁, v₂, u₂} ⟶ uliftYoneda.{max w v₂, v₁, u₁} ⋙ G
P Q : Cᵒᵖ ⥤ Type (max w v₁ v₂)
f : P ⟶ Q
X : C
p : uliftYoneda.{max w v₂, v₁, u₁}.obj X ⟶ P
⊢ uliftYonedaEquiv (p ≫ presheafHom φ P ≫ F.op.whiskerLeft (G.map f)) = uliftYonedaEquiv (p ≫ f ≫ presheafHom φ Q)

Tactic:
by
    rw [← assoc p f, uliftYonedaEquiv_ι_presheafHom, ← assoc,
      uliftYonedaEquiv_comp, uliftYonedaEquiv_ι_presheafHom,
      Functor.map_comp]
    dsimp

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝³ : Category.{v₂, u₂} ℰ
A✝ A : C ⥤ ℰ
inst✝² : uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X : C
G : (Cᵒᵖ ⥤ Type (max w v₁ v₂)) ⥤ Dᵒᵖ ⥤ Type (max w v₁ v₂)
φ : F ⋙ uliftYoneda.{max w v₁, v₂, u₂} ⟶ uliftYoneda.{max w v₂, v₁, u₁} ⋙ G
inst✝ : ∀ (P : Cᵒᵖ ⥤ Type (max w v₁ v₂)), F.op.HasLeftKanExtension P
P Q : Cᵒᵖ ⥤ Type (max w v₁ v₂)
f : P ⟶ Q
⊢ F.op.lan.map f ≫ (F.op.lan.obj Q).descOfIsLeftKanExtension (F.op.lanUnit.app Q) (G.obj Q) (presheafHom φ Q) =
    (F.op.lan.obj P).descOfIsLeftKanExtension (F.op.lanUnit.app P) (G.obj P) (presheafHom φ P) ≫ G.map f

Tactic:
apply (F.op.lan.obj P).hom_ext_of_isLeftKanExtension (F.op.lanUnit.app P)

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝³ : Category.{v₂, u₂} ℰ
A✝ A : C ⥤ ℰ
inst✝² : uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X : C
G : (Cᵒᵖ ⥤ Type (max w v₁ v₂)) ⥤ Dᵒᵖ ⥤ Type (max w v₁ v₂)
φ : F ⋙ uliftYoneda.{max w v₁, v₂, u₂} ⟶ uliftYoneda.{max w v₂, v₁, u₁} ⋙ G
inst✝ : ∀ (P : Cᵒᵖ ⥤ Type (max w v₁ v₂)), F.op.HasLeftKanExtension P
P Q : Cᵒᵖ ⥤ Type (max w v₁ v₂)
f : P ⟶ Q
⊢ F.op.lanUnit.app P ≫
      F.op.whiskerLeft
        (F.op.lan.map f ≫ (F.op.lan.obj Q).descOfIsLeftKanExtension (F.op.lanUnit.app Q) (G.obj Q) (presheafHom φ Q)) =
    F.op.lanUnit.app P ≫
      F.op.whiskerLeft
        ((F.op.lan.obj P).descOfIsLeftKanExtension (F.op.lanUnit.app P) (G.obj P) (presheafHom φ P) ≫ G.map f)
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : LocallySmall.{w, v₁, u₁} C
inst✝² : WellPowered.{w, v₁, u₁} C
inst✝¹ : HasLimitsOfSize.{w, w, v₁, u₁} C
P : ObjectProperty C
inst✝ : ObjectProperty.Small.{w, v₁, u₁} P
hP : P.IsCoseparating
this✝² : HasFiniteLimits C
this✝¹ : HasProductsOfShape (Subtype P) C
this✝ : ∀ (A : C), HasProductsOfShape (StructuredArrow A P.ι) C
this : CompleteLattice (Subobject (∏ᶜ Subtype.val)) :=
  completeLatticeOfCompleteSemilatticeInf (Subobject (∏ᶜ Subtype.val))
⊢ HasInitial C

Tactic:
suffices ∀ A : C, Unique (((⊥ : Subobject (piObj (Subtype.val : Subtype P → C))) : C) ⟶ A) by
    exact hasInitial_of_unique ((⊥ : Subobject (piObj (Subtype.val : Subtype P → C))) : C)

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : LocallySmall.{w, v₁, u₁} C
inst✝² : WellPowered.{w, v₁, u₁} C
inst✝¹ : HasLimitsOfSize.{w, w, v₁, u₁} C
P : ObjectProperty C
inst✝ : ObjectProperty.Small.{w, v₁, u₁} P
hP : P.IsCoseparating
this✝² : HasFiniteLimits C
this✝¹ : HasProductsOfShape (Subtype P) C
this✝ : ∀ (A : C), HasProductsOfShape (StructuredArrow A P.ι) C
this : CompleteLattice (Subobject (∏ᶜ Subtype.val)) :=
  completeLatticeOfCompleteSemilatticeInf (Subobject (∏ᶜ Subtype.val))
⊢ (A : C) → Unique (Subobject.underlying.obj ⊥ ⟶ A)
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : LocallySmall.{w, v₁, u₁} C
inst✝² : WellPowered.{w, v₁, u₁} C
inst✝¹ : HasLimitsOfSize.{w, w, v₁, u₁} C
P : ObjectProperty C
inst✝ : ObjectProperty.Small.{w, v₁, u₁} P
hP : P.IsCoseparating
⊢ HasInitial C

Tactic:
by
  have := hasFiniteLimits_of_hasLimitsOfSize C
  have := hasProductsOfShape_of_small C (Subtype P)
  have := fun A => hasProductsOfShape_of_small.{w} C (StructuredArrow A P.ι)
  let := completeLatticeOfCompleteSemilatticeInf (Subobject (piObj (Subtype.val : Subtype P → C)))
  suffices ∀ A : C, Unique (((⊥ : Subobject (piObj (Subtype.val : Subtype P → C))) : C) ⟶ A) by
    exact hasInitial_of_unique ((⊥ : Subobject (piObj (Subtype.val : Subtype P → C))) : C)
  have := hP.mono_productTo
  refine fun A => ⟨⟨?_⟩, fun f => ?_⟩
  · let s : ∏ᶜ (Subtype.val (p := P)) ⟶ ∏ᶜ P.productToFamily A :=
      Pi.lift (fun f ↦ Pi.π Subtype.val ⟨f.right.obj, f.right.property⟩)
    exact Subobject.ofLEMk _
      (pullback.fst _ _ : pullback s (P.productTo A) ⟶ _) bot_le ≫ pullback.snd _ _
  · suffices ∀ (g : Subobject.underlying.obj ⊥ ⟶ A), f = g by
      apply this
    intro g
    suffices IsSplitEpi (equalizer.ι f g) by exact eq_of_epi_equalizer
    exact IsSplitEpi.mk' ⟨Subobject.ofLEMk _ (equalizer.ι f g ≫ Subobject.arrow _) bot_le, by
      ext
      simp⟩

Goal state after: