mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasZeroMorphisms C
inst✝⁴ : HasFiniteProducts C
inst✝³ : HasKernels C
inst✝² : IsNormalMonoCategory C
X Y Z : C
a : X ⟶ Z
b : Y ⟶ Z
inst✝¹ : Mono a
inst✝ : Mono b
P : C
f : Z ⟶ P
haf : a ≫ f = 0
i : IsLimit (KernelFork.ofι a haf)
Q : C
g : Z ⟶ Q
hbg : b ≫ g = 0
i' : IsLimit (KernelFork.ofι b hbg)
a' : kernel (prod.lift f g) ⟶ (KernelFork.ofι a haf).pt
ha' : a' ≫ Fork.ι (KernelFork.ofι a haf) = kernel.ι (prod.lift f g)
b' : kernel (prod.lift f g) ⟶ (KernelFork.ofι b hbg).pt
hb' : b' ≫ Fork.ι (KernelFork.ofι b hbg) = kernel.ι (prod.lift f g)
s : PullbackCone a b
m : s.pt ⟶ kernel (prod.lift f g)
h₁ : m ≫ a' = s.fst
x✝ : m ≫ b' = s.snd
⊢ (m ≫ a') ≫ a = s.fst ≫ a

Tactic:
h₁

Goal state after:
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasZeroMorphisms C
inst✝⁴ : HasFiniteProducts C
inst✝³ : HasKernels C
inst✝² : IsNormalMonoCategory C
X Y Z : C
a : X ⟶ Z
b : Y ⟶ Z
inst✝¹ : Mono a
inst✝ : Mono b
P : C
f : Z ⟶ P
haf : a ≫ f = 0
i : IsLimit (KernelFork.ofι a haf)
Q : C
g : Z ⟶ Q
hbg : b ≫ g = 0
i' : IsLimit (KernelFork.ofι b hbg)
a' : kernel (prod.lift f g) ⟶ (KernelFork.ofι a haf).pt
ha' : a' ≫ Fork.ι (KernelFork.ofι a haf) = kernel.ι (prod.lift f g)
b' : kernel (prod.lift f g) ⟶ (KernelFork.ofι b hbg).pt
hb' : b' ≫ Fork.ι (KernelFork.ofι b hbg) = kernel.ι (prod.lift f g)
s : PullbackCone a b
m : s.pt ⟶ kernel (prod.lift f g)
h₁ : m ≫ a' = s.fst
x✝ : m ≫ b' = s.snd
⊢ s.fst ≫ a = s.fst ≫ a
Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasZeroMorphisms C
inst✝⁴ : HasFiniteCoproducts C
inst✝³ : HasCokernels C
inst✝² : IsNormalEpiCategory C
X Y Z : C
a : X ⟶ Y
b : X ⟶ Z
inst✝¹ : Epi a
inst✝ : Epi b
P : C
f : P ⟶ X
hfa : f ≫ a = 0
i : IsColimit (CokernelCofork.ofπ a hfa)
Q : C
g : Q ⟶ X
hgb : g ≫ b = 0
i' : IsColimit (CokernelCofork.ofπ b hgb)
a' : (CokernelCofork.ofπ a hfa).pt ⟶ cokernel (coprod.desc f g)
ha' : Cofork.π (CokernelCofork.ofπ a hfa) ≫ a' = cokernel.π (coprod.desc f g)
b' : (CokernelCofork.ofπ b hgb).pt ⟶ cokernel (coprod.desc f g)
hb' : Cofork.π (CokernelCofork.ofπ b hgb) ≫ b' = cokernel.π (coprod.desc f g)
s : PushoutCocone a b
m : cokernel (coprod.desc f g) ⟶ s.pt
h₁ : a' ≫ m = s.inl
x✝ : b' ≫ m = s.inr
⊢ a ≫ a' ≫ m = a ≫ s.inl

Tactic:
h₁

Goal state after:
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasZeroMorphisms C
inst✝⁴ : HasFiniteCoproducts C
inst✝³ : HasCokernels C
inst✝² : IsNormalEpiCategory C
X Y Z : C
a : X ⟶ Y
b : X ⟶ Z
inst✝¹ : Epi a
inst✝ : Epi b
P : C
f : P ⟶ X
hfa : f ≫ a = 0
i : IsColimit (CokernelCofork.ofπ a hfa)
Q : C
g : Q ⟶ X
hgb : g ≫ b = 0
i' : IsColimit (CokernelCofork.ofπ b hgb)
a' : (CokernelCofork.ofπ a hfa).pt ⟶ cokernel (coprod.desc f g)
ha' : Cofork.π (CokernelCofork.ofπ a hfa) ≫ a' = cokernel.π (coprod.desc f g)
b' : (CokernelCofork.ofπ b hgb).pt ⟶ cokernel (coprod.desc f g)
hb' : Cofork.π (CokernelCofork.ofπ b hgb) ≫ b' = cokernel.π (coprod.desc f g)
s : PushoutCocone a b
m : cokernel (coprod.desc f g) ⟶ s.pt
h₁ : a' ≫ m = s.inl
x✝ : b' ≫ m = s.inr
⊢ a ≫ s.inl = a ≫ s.inl
Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasFiniteCoproducts C
inst✝¹ : HasCokernels C
inst✝ : IsNormalEpiCategory C
X Y : C
f g : X ⟶ Y
huv : pushout.inl (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g) = pushout.inr (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g)
⊢ f ≫ pushout.inl (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g) =
    (coprod.inr ≫ coprod.desc (𝟙 Y) f) ≫ pushout.inl (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g)

Tactic:
rw [coprod.inr_desc]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasFiniteCoproducts C
inst✝¹ : HasCokernels C
inst✝ : IsNormalEpiCategory C
X Y : C
f g : X ⟶ Y
huv : pushout.inl (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g) = pushout.inr (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g)
⊢ (coprod.inr ≫ coprod.desc (𝟙 Y) g) ≫ pushout.inr (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g) =
    g ≫ pushout.inr (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g)

Tactic:
rw [coprod.inr_desc]

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

Goal state before:
pp: case refine_2
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasKernels C
inst✝² : HasCokernels C
inst✝¹ : ∀ {X Y : C} (f : X ⟶ Y), IsIso (coimageImageComparison f)
inst✝ : HasFiniteProducts C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
m : Epi f
this✝¹ : HasImages C
this✝ : HasEqualizers C
this : HasZeroObject C
aux :
  ∀ (s : CokernelCofork (kernel.ι f)),
    Cofork.π (CokernelCofork.ofπ f ⋯) ≫
        inv (imageMonoFactorisation f).m ≫
          inv (coimageImageComparison f) ≫ colimit.desc (parallelPair (kernel.ι f) 0) s =
      Cofork.π s
A : CokernelCofork (kernel.ι f)
g : (CokernelCofork.ofπ f ⋯).pt ⟶ A.pt
hg : Cofork.π (CokernelCofork.ofπ f ⋯) ≫ g = Cofork.π A
⊢ g = inv (imageMonoFactorisation f).m ≫ inv (coimageImageComparison f) ≫ colimit.desc (parallelPair (kernel.ι f) 0) A

Tactic:
rw [CokernelCofork.π_ofπ] at hg

Goal state after:
case refine_2
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasKernels C
inst✝² : HasCokernels C
inst✝¹ : ∀ {X Y : C} (f : X ⟶ Y), IsIso (coimageImageComparison f)
inst✝ : HasFiniteProducts C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
m : Epi f
this✝¹ : HasImages C
this✝ : HasEqualizers C
this : HasZeroObject C
aux :
  ∀ (s : CokernelCofork (kernel.ι f)),
    Cofork.π (CokernelCofork.ofπ f ⋯) ≫
        inv (imageMonoFactorisation f).m ≫
          inv (coimageImageComparison f) ≫ colimit.desc (parallelPair (kernel.ι f) 0) s =
      Cofork.π s
A : CokernelCofork (kernel.ι f)
g : (CokernelCofork.ofπ f ⋯).pt ⟶ A.pt
hg : f ≫ g = Cofork.π A
⊢ g = inv (imageMonoFactorisation f).m ≫ inv (coimageImageComparison f) ≫ colimit.desc (parallelPair (kernel.ι f) 0) A
Module: Mathlib.CategoryTheory.Abelian.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPullbacks C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : Epi f
R : C
e : Y ⟶ R
h : pullback.snd f g ≫ e = 0
u : X ⊞ Y ⟶ R := biprod.desc 0 e
⊢ PullbackToBiproductIsKernel.pullbackToBiproduct f g ≫ u = 0

Tactic:
simpa [u]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPullbacks C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : Epi g
R : C
e : X ⟶ R
h : pullback.fst f g ≫ e = 0
u : X ⊞ Y ⟶ R := biprod.desc e 0
⊢ PullbackToBiproductIsKernel.pullbackToBiproduct f g ≫ u = 0

Tactic:
simpa [u]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPushouts C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : Mono f
R : C
e : R ⟶ Z
h : e ≫ pushout.inr f g = 0
u : R ⟶ Y ⊞ Z := biprod.lift 0 e
⊢ u ≫ BiproductToPushoutIsCokernel.biproductToPushout f g = 0

Tactic:
simpa [u]

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

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : Category.{v_3, u_3} E
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroMorphisms D
inst✝ : HasZeroMorphisms E
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
⊢ φ.τ₃.op ≫ S₁.op.f = S₂.op.f ≫ φ.τ₂.op

Tactic:
by
    dsimp
    simp only [← op_comp, φ.comm₂₃]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPushouts C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : Mono g
R : C
e : R ⟶ Y
h : e ≫ pushout.inl f g = 0
u : R ⟶ Y ⊞ Z := biprod.lift e 0
⊢ u ≫ BiproductToPushoutIsCokernel.biproductToPushout f g = 0

Tactic:
simpa [u]

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₂ : ShortComplex C
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
⊢ QuasiIso φ ↔ IsIso (rightHomologyMap' φ h₁ h₂)

Tactic:
by
  have γ : RightHomologyMapData φ h₁ h₂ := default
  rw [γ.quasiIso_iff, γ.rightHomologyMap'_eq]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
h : S.LeftHomologyData
A K' H' : C
eK : K' ≅ h.K
eH : H' ≅ h.H
⊢ ∀ (j : WalkingParallelPair),
    ((Cocone.precompose (parallelPair.ext (Iso.refl S.X₁) eK.symm ⋯ ⋯).inv).obj (CokernelCofork.ofπ h.π ⋯)).ι.app j ≫
        eH.symm.hom =
      (CokernelCofork.ofπ (eK.hom ≫ h.π ≫ eH.inv) ⋯).ι.app j

Tactic:
rintro (_ | _)

Goal state after:
case zero
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
h : S.LeftHomologyData
A K' H' : C
eK : K' ≅ h.K
eH : H' ≅ h.H
⊢ ((Cocone.precompose (parallelPair.ext (Iso.refl S.X₁) eK.symm ⋯ ⋯).inv).obj (CokernelCofork.ofπ h.π ⋯)).ι.app
        WalkingParallelPair.zero ≫
      eH.symm.hom =
    (CokernelCofork.ofπ (eK.hom ≫ h.π ≫ eH.inv) ⋯).ι.app WalkingParallelPair.zero

case one
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
h : S.LeftHomologyData
A K' H' : C
eK : K' ≅ h.K
eH : H' ≅ h.H
⊢ ((Cocone.precompose (parallelPair.ext (Iso.refl S.X₁) eK.symm ⋯ ⋯).inv).obj (CokernelCofork.ofπ h.π ⋯)).ι.app
        WalkingParallelPair.one ≫
      eH.symm.hom =
    (CokernelCofork.ofπ (eK.hom ≫ h.π ≫ eH.inv) ⋯).ι.app WalkingParallelPair.one
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
h : S.RightHomologyData
A Q' H' : C
eQ : Q' ≅ h.Q
eH : H' ≅ h.H
⊢ ∀ (j : WalkingParallelPair),
    ((Cone.postcompose (parallelPair.ext eQ.symm (Iso.refl S.X₃) ⋯ ⋯).hom).obj (KernelFork.ofι h.ι ⋯)).π.app j =
      eH.symm.hom ≫ (KernelFork.ofι (eH.hom ≫ h.ι ≫ eQ.inv) ⋯).π.app j

Tactic:
rintro (_ | _)

Goal state after:
case zero
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
h : S.RightHomologyData
A Q' H' : C
eQ : Q' ≅ h.Q
eH : H' ≅ h.H
⊢ ((Cone.postcompose (parallelPair.ext eQ.symm (Iso.refl S.X₃) ⋯ ⋯).hom).obj (KernelFork.ofι h.ι ⋯)).π.app
      WalkingParallelPair.zero =
    eH.symm.hom ≫ (KernelFork.ofι (eH.hom ≫ h.ι ≫ eQ.inv) ⋯).π.app WalkingParallelPair.zero

case one
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
h : S.RightHomologyData
A Q' H' : C
eQ : Q' ≅ h.Q
eH : H' ≅ h.H
⊢ ((Cone.postcompose (parallelPair.ext eQ.symm (Iso.refl S.X₃) ⋯ ⋯).hom).obj (KernelFork.ofι h.ι ⋯)).π.app
      WalkingParallelPair.one =
    eH.symm.hom ≫ (KernelFork.ofι (eH.hom ≫ h.ι ≫ eQ.inv) ⋯).π.app WalkingParallelPair.one
Module: Mathlib.Algebra.Homology.ShortComplex.Homology

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasHomology
⊢ S.toCycles ≫ S.homologyπ = 0

Tactic:
dsimp only [homologyπ]
  simp only [toCycles_comp_leftHomologyπ_assoc, zero_comp]

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₁.LeftHomologyData
h₂ : S₂.RightHomologyData
⊢ h₁.π ≫ h₁.homologyIso.inv ≫ homologyMap φ ≫ h₂.homologyIso.hom ≫ h₂.ι = h₁.i ≫ φ.τ₂ ≫ h₂.p

Tactic:
by
  dsimp only [LeftHomologyData.homologyIso, RightHomologyData.homologyIso,
    Iso.symm, Iso.trans, Iso.refl, leftHomologyIso, rightHomologyIso,
    leftHomologyMapIso', rightHomologyMapIso',
    LeftHomologyData.cyclesIso, RightHomologyData.opcyclesIso,
    LeftHomologyData.leftHomologyIso, RightHomologyData.rightHomologyIso,
    homologyMap, homologyMap']
  simp only [assoc, rightHomologyι_naturality', rightHomologyι_naturality'_assoc,
    leftHomologyπ_naturality'_assoc, HomologyData.comm_assoc, p_opcyclesMap'_assoc,
    id_τ₂, p_opcyclesMap', id_comp, cyclesMap'_i_assoc]

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

Goal state before:
pp: case refine_2
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 (cyclesMap φ)
h₂ : Epi φ.τ₁
h : S₂.toCycles ≫ inv (cyclesMap φ) ≫ S₁.homologyπ = 0
z : (CokernelCofork.ofπ S₂.homologyπ ⋯).pt ⟶ S₁.homology
hz : S₂.homologyπ ≫ z = inv (cyclesMap φ) ≫ S₁.homologyπ
⊢ z ≫ homologyMap φ = 𝟙 S₂.homology

Tactic:
← cancel_epi S₂.homologyπ,

Goal state after:
case refine_2
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 (cyclesMap φ)
h₂ : Epi φ.τ₁
h : S₂.toCycles ≫ inv (cyclesMap φ) ≫ S₁.homologyπ = 0
z : (CokernelCofork.ofπ S₂.homologyπ ⋯).pt ⟶ S₁.homology
hz : S₂.homologyπ ≫ z = inv (cyclesMap φ) ≫ S₁.homologyπ
⊢ S₂.homologyπ ≫ z ≫ homologyMap φ = S₂.homologyπ ≫ 𝟙 S₂.homology
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
inst✝ : S.HasHomology
h : S.LeftHomologyData
⊢ S.Exact ↔ IsZero h.H

Tactic:
rw [S.exact_iff_isZero_homology]
  exact Iso.isZero_iff h.homologyIso

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
inst✝ : S.HasHomology
h : S.RightHomologyData
⊢ S.Exact ↔ IsZero h.H

Tactic:
rw [S.exact_iff_isZero_homology]
  exact Iso.isZero_iff h.homologyIso

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✝² : HasZeroMorphisms C
S : ShortComplex C
inst✝¹ : S.HasHomology
inst✝ : HasZeroObject C
⊢ Nonempty (S.homology ≅ 0) → IsZero S.homology

Tactic:
rintro ⟨e⟩

Goal state after:
case mpr
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
S : ShortComplex C
inst✝¹ : S.HasHomology
inst✝ : HasZeroObject C
e : S.homology ≅ 0
⊢ IsZero S.homology
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
⊢ PreservesFiniteColimits F

Tactic:
let := preservesCoequalizers_of_preservesCokernels F
  let := preservesInitialObject_of_preservesZeroMorphisms F
  let := preservesColimitsOfShape_pempty_of_preservesInitial F
  let : PreservesFiniteCoproducts F :=
    ⟨fun _ ↦ PreservesFiniteCoproducts.of_preserves_binary_and_initial F _⟩
  exact preservesFiniteColimits_of_preservesCoequalizers_and_finiteCoproducts F

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

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 Y : C
P : Subobject Y
f : X ⟶ Y
⊢ ∀ (a b : MonoOver Y), (isIsomorphicSetoid (MonoOver Y)) a b → a.Factors f = b.Factors f

Tactic:
rintro P Q ⟨h⟩

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y : C
P✝ : Subobject Y
f : X ⟶ Y
P Q : MonoOver Y
h : P ≅ Q
⊢ P.Factors f = Q.Factors f
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
S : ShortComplex C
hS : S.Exact
J : C
f : S.X₂ ⟶ J
inst✝ : Injective J
hf : S.f ≫ f = 0
⊢ S.g ≫ hS.descToInjective f hf = f

Tactic:
by
  dsimp [descToInjective]
  simp only [← p_fromOpcycles, assoc, Injective.comp_factorThru, p_descOpcycles]

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

Goal state before:
pp: case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
this : factorThruImage S.f ≫ imageToKernel' S.f S.g ⋯ = kernel.lift S.g S.f ⋯
⊢ Epi (kernel.lift S.g S.f ⋯) → Epi (imageToKernel' S.f S.g ⋯)

Tactic:
intro
    exact epi_of_epi_fac this

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

Goal state before:
pp: case insert
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasImages C
inst✝² : HasBinaryCoproducts C
inst✝¹ : HasInitial C
inst✝ : InitialMonoClass C
I : Type u_1
A B : C
P : I → Subobject B
f : A ⟶ B
a✝¹ : I
s✝ : Finset I
a✝ : a✝¹ ∉ s✝
ih : (∃ i ∈ s✝, (P i).Factors f) → (s✝.sup P).Factors f
j : I
m : j ∈ insert a✝¹ s✝
h : (P j).Factors f
⊢ ((insert a✝¹ s✝).sup P).Factors f

Tactic:
simp only [Finset.sup_insert]

Goal state after:
case insert
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasImages C
inst✝² : HasBinaryCoproducts C
inst✝¹ : HasInitial C
inst✝ : InitialMonoClass C
I : Type u_1
A B : C
P : I → Subobject B
f : A ⟶ B
a✝¹ : I
s✝ : Finset I
a✝ : a✝¹ ∉ s✝
ih : (∃ i ∈ s✝, (P i).Factors f) → (s✝.sup P).Factors f
j : I
m : j ∈ insert a✝¹ s✝
h : (P j).Factors f
⊢ (P a✝¹ ⊔ s✝.sup P).Factors f
Module: Mathlib.CategoryTheory.Abelian.FunctorCategory

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type w
inst✝¹ : Category.{z, w} D
inst✝ : Abelian D
F G : C ⥤ D
α : F ⟶ G
X : C
⊢ ((evaluation C D).obj X).map (cokernel.π α) ≫ (PreservesCokernel.iso ((evaluation C D).obj X) α).hom =
    (Iso.refl (((evaluation C D).obj X).obj G)).hom ≫ cokernel.π (α.app X)

Tactic:
apply (cancel_mono (PreservesCokernel.iso ((evaluation C D).obj X) α).inv).1

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
D : Type w
inst✝¹ : Category.{z, w} D
inst✝ : Abelian D
F G : C ⥤ D
α : F ⟶ G
X : C
⊢ (((evaluation C D).obj X).map (cokernel.π α) ≫ (PreservesCokernel.iso ((evaluation C D).obj X) α).hom) ≫
      (PreservesCokernel.iso ((evaluation C D).obj X) α).inv =
    ((Iso.refl (((evaluation C D).obj X).obj G)).hom ≫ cokernel.π (α.app X)) ≫
      (PreservesCokernel.iso ((evaluation C D).obj X) α).inv
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 L' : C ⥤ D
F F' : C ⥤ H
Y : D
inst✝ : L.HasPointwiseLeftKanExtensionAt F Y
e₁ : L ≅ L'
e₂ : F ≅ F'
⊢ L.HasPointwiseLeftKanExtensionAt F' Y

Tactic:
let e : CostructuredArrow.proj L Y ⋙ F' ≅ CostructuredArrow.proj L Y ⋙ F :=
    NatIso.ofComponents fun X ↦ (e₂.app _).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 L' : C ⥤ D
F F' : C ⥤ H
Y : D
inst✝ : L.HasPointwiseLeftKanExtensionAt F Y
e₁ : L ≅ L'
e₂ : F ≅ F'
e : CostructuredArrow.proj L Y ⋙ F' ≅ CostructuredArrow.proj L Y ⋙ F :=
  NatIso.ofComponents (fun X ↦ (e₂.app ((CostructuredArrow.proj L Y).obj X)).symm) ⋯
⊢ 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
E : L.LeftExtension F
Y : D
h : E.IsPointwiseLeftKanExtensionAt Y
Z : H
φ : CostructuredArrow.proj L Y ⋙ F ⟶ (const (CostructuredArrow L Y)).obj Z
g : CostructuredArrow L Y
⊢ (StructuredArrow.hom E).app g.left ≫ (StructuredArrow.right E).map g.hom ≫ (IsColimit.homEquiv h).symm φ = φ.app g

Tactic:
simpa using h.ι_app_homEquiv_symm φ g

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

Goal state before:
pp: case e_a
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 E' : L.RightExtension F
Y : D
g₁ g₂ : StructuredArrow Y L
φ : g₁ ⟶ g₂
⊢ (CostructuredArrow.left E).map (L.map (StructuredArrow.Hom.right φ)) ≫ (CostructuredArrow.hom E).app g₂.right =
    (CostructuredArrow.hom E).app g₁.right ≫ F.map φ.right

Tactic:
apply E.hom.naturality

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

Goal state before:
pp: case mpr
C : Type u_1
H : Type u_3
D : Type u_4
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_3, u_3} H
inst✝ : Category.{v_4, u_4} D
L : C ⥤ D
F₁ F₂ : C ⥤ H
F₁' F₂' : D ⥤ H
α₁ : L ⋙ F₁' ⟶ F₁
α₂ : L ⋙ F₂' ⟶ F₂
e : F₁ ≅ F₂
e' : F₁' ≅ F₂'
h : L.whiskerLeft e'.hom ≫ α₂ = α₁ ≫ e.hom
eq : CostructuredArrow.IsUniversal (RightExtension.mk F₁' α₁) ≃
  CostructuredArrow.IsUniversal (RightExtension.mk F₂' α₂) := ⋯
⊢ F₂'.IsRightKanExtension α₂ → F₁'.IsRightKanExtension α₁

Tactic:
exact fun _ => ⟨⟨eq.2 (isUniversalOfIsRightKanExtension F₂' α₂)⟩⟩

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 : C ⥤ ℰ
P : Cᵒᵖ ⥤ Type (max w v₁)
s : Cocone (functorToRepresentables P)
j : P.Elementsᵒᵖ
X : Cᵒᵖ
x : ((functorToRepresentables P).obj j).obj X
φ : unop j ⟶ P.elementsMk X ((hom ((uliftYonedaEquiv.symm (unop j).snd).app X)) x) := ⟨Quiver.Hom.op x.down, ⋯⟩
this :
  (functorToRepresentables P).map φ.op ≫ s.ι.app (op (unop j)) =
    s.ι.app (op (P.elementsMk X ((hom ((uliftYonedaEquiv.symm (unop j).snd).app X)) x)))
⊢ (hom
          (((coconeOfRepresentable P).ι.app j ≫
                { app := fun X ↦ ↾fun x ↦ uliftYonedaEquiv (s.ι.app (op (P.elementsMk X x))), naturality := ⋯ }).app
            X)).toFun
      x =
    (hom ((s.ι.app j).app X)).toFun x

Tactic:
dsimp [φ] at this 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)
j : P.Elementsᵒᵖ
X : Cᵒᵖ
x : ULift.{w, v₁} (unop X ⟶ unop (unop j).fst)
φ : unop j ⟶ P.elementsMk X ((hom ((uliftYonedaEquiv.symm (unop j).snd).app X)) x) := ⟨Quiver.Hom.op x.down, ⋯⟩
this :
  uliftYoneda.{w, v₁, u₁}.map x.down ≫ s.ι.app j =
    s.ι.app (op (P.elementsMk X ((hom ((uliftYonedaEquiv.symm (unop j).snd).app X)) x)))
⊢ uliftYonedaEquiv (s.ι.app (op (P.elementsMk X ((hom ((uliftYonedaEquiv.symm (unop j).snd).app X)) x)))) =
    (hom ((s.ι.app j).app X)) x
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : ObjectProperty C
h : P.IsSeparating
D : Type u_1
inst✝ : Category.{v_1, u_1} D
α : C ≌ D
X Y : D
f g : X ⟶ Y
H : ∀ (G : D), P.strictMap α.functor G → ∀ (h : G ⟶ X), h ≫ f = h ≫ g
Z : C
hZ : P Z
h' : α.functor.obj Z ⟶ X
⊢ (α.toAdjunction.homEquiv Z X) h' ≫ α.inverse.map f = (α.toAdjunction.homEquiv Z X) h' ≫ α.inverse.map g

Tactic:
simp only [Adjunction.homEquiv_unit, Category.assoc, ← Functor.map_comp,
      H _ (P.strictMap_obj _ hZ) h']

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

Goal state before:
pp: case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : P.IsDetecting
X Y : C
f : X ⟶ Y
inst✝ : Mono f
⊢ IsIso f → ∀ (G : C), P G → Function.Surjective ⇑(ConcreteCategory.hom ((coyoneda.obj (op G)).map f))

pp: case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : P.IsDetecting
X Y : C
f : X ⟶ Y
inst✝ : Mono f
⊢ (∀ (G : C), P G → Function.Surjective ⇑(ConcreteCategory.hom ((coyoneda.obj (op G)).map f))) → IsIso f

Tactic:
· intro h
    rw [isIso_iff_yoneda_map_bijective] at h
    intro A _
    exact (h A).2

Goal state after:
case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : P.IsDetecting
X Y : C
f : X ⟶ Y
inst✝ : Mono f
⊢ (∀ (G : C), P G → Function.Surjective ⇑(ConcreteCategory.hom ((coyoneda.obj (op G)).map f))) → IsIso f