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

Goal state before:
pp: case refine_3.left
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
G : C ⥤ D
inst✝³ : HasBinaryCoproducts C
inst✝² : HasPushouts C
inst✝¹ : PreservesColimitsOfShape (Discrete WalkingPair) G
inst✝ : PreservesColimitsOfShape WalkingSpan G
K : WalkingParallelPair ⥤ C
c : Cocone (K ⋙ G)
⊢ (BinaryCofan.mk (G.map coprod.inl) (G.map coprod.inr)).ι.app { as := WalkingPair.left } ≫
      G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.left)) ≫
        c.ι.app WalkingParallelPair.one =
    (BinaryCofan.mk (G.map coprod.inl) (G.map coprod.inr)).ι.app { as := WalkingPair.left } ≫
      G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right)) ≫
        c.ι.app WalkingParallelPair.one

Tactic:
simp only [BinaryCofan.ι_app_left, BinaryCofan.mk_inl, ←
              G.map_comp_assoc, coprod.inl_desc]

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: K✝ : Type uK
V✝ : Type uV
inst✝¹³ : CommSemiring K✝
inst✝¹² : AddCommMonoid V✝
inst✝¹¹ : Module K✝ V✝
inst✝¹⁰ : Projective K✝ V✝
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁹ : CommSemiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : IsReflexive R M
K : Type u_4
V : Type u_5
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : IsReflexive K V
contra : ℵ₀ ≤ Module.rank K V
this : lift.{u_4, u_5} (Module.rank K V) < Module.rank K (Dual K (Dual K V))
heq : lift.{max u_5 u_4, u_5} (Module.rank K V) = lift.{u_5, max u_5 u_4} (Module.rank K (Dual K (Dual K V)))
⊢ False

Tactic:
← lift_umax,

Goal state after:
K✝ : Type uK
V✝ : Type uV
inst✝¹³ : CommSemiring K✝
inst✝¹² : AddCommMonoid V✝
inst✝¹¹ : Module K✝ V✝
inst✝¹⁰ : Projective K✝ V✝
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁹ : CommSemiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : IsReflexive R M
K : Type u_4
V : Type u_5
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : IsReflexive K V
contra : ℵ₀ ≤ Module.rank K V
this : lift.{max u_5 u_4, u_5} (Module.rank K V) < Module.rank K (Dual K (Dual K V))
heq : lift.{max u_5 u_4, u_5} (Module.rank K V) = lift.{u_5, max u_5 u_4} (Module.rank K (Dual K (Dual K V)))
⊢ False
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: K : Type u_1
V₁ : Type u_2
V₂ : Type u_3
inst✝⁴ : Field K
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
f : V₁ →ₗ[K] V₂
⊢ finrank K ↥f.dualMap.range = finrank K ↥f.range

Tactic:
by
  rw [congr_arg dualMap (show f = (range f).subtype.comp f.rangeRestrict by rfl),
    ← dualMap_comp_dualMap, range_comp,
    range_eq_top.mpr (dualMap_surjective_of_injective (range f).injective_subtype),
    Submodule.map_top, finrank_range_of_inj, Subspace.dual_finrank_eq]
  exact dualMap_injective_of_surjective (range_eq_top.mp f.range_rangeRestrict)

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
X✝ Y✝ : C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₁, u₂} D
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : F.IsEquivalence
X Y : C
f : X ⟶ Y
hf : NormalMono (F.map f)
reassoc' : ∀ {W : D} (h : NormalMono.Z (F.map f) ⟶ W), F.map f ≫ NormalMono.g ≫ h = 0 ≫ h
⊢ F.map (f ≫ F.preimage (NormalMono.g ≫ (F.objObjPreimageIso (NormalMono.Z (F.map f))).inv)) = F.map 0

Tactic:
simp [reassoc']

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✝⁴ : 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:
by rw [← Category.assoc, h₁]

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

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

Tactic:
rw [sub_sub_sub, add_def, ← neg_def, neg_neg b, neg_def]

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 : ShortComplex C
h : S.RightHomologyData
hg : S.g = 0
⊢ IsIso h.ι

Tactic:
by
  have ⟨φ, hφ⟩ := KernelFork.IsLimit.lift' h.hι' (𝟙 _)
    (by rw [← cancel_epi h.p, id_comp, p_g', comp_zero, hg])
  dsimp at hφ
  exact ⟨φ, by rw [← cancel_mono h.ι, assoc, hφ, comp_id, id_comp], 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
h : S.RightHomologyData
A Q' H' : C
eQ : Q' ≅ h.Q
eH : H' ≅ h.H
⊢ (S.f ≫ h.p) ≫ eQ.inv = 0

Tactic:
h.wp,

Goal state after:
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
⊢ 0 ≫ eQ.inv = 0
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
e : S₁ ≅ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
⊢ opcyclesMap' e.inv h₂ h₁ ≫ opcyclesMap' e.hom h₁ h₂ = 𝟙 h₂.Q

Tactic:
by rw [← opcyclesMap'_comp, e.inv_hom_id, opcyclesMap'_id]

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
S S₁ S₂ : ShortComplex C
h : S.RightHomologyData
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : h.IsPreservedBy F
this✝ : PreservesColimit (parallelPair S.f 0) F
this : PreservesLimit (parallelPair h.g' 0) F
⊢ F.map (S.f ≫ h.p) = 0

Tactic:
h.wp,

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✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
S S₁ S₂ : ShortComplex C
h : S.RightHomologyData
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : h.IsPreservedBy F
this✝ : PreservesColimit (parallelPair S.f 0) F
this : PreservesLimit (parallelPair h.g' 0) F
⊢ F.map 0 = 0
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
h : S.RightHomologyData
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : h.IsPreservedBy F
this✝ : PreservesColimit (parallelPair S.f 0) F
this : PreservesLimit (parallelPair h.g' 0) F
wp : F.map S.f ≫ F.map h.p = 0
hp : IsColimit ((CokernelCofork.ofπ h.p ⋯).map F)
g' : F.obj h.Q ⟶ F.obj S.X₃ := ⋯
⊢ Cofork.π ((CokernelCofork.ofπ h.p ⋯).map F) ≫ g' = Cofork.π ((CokernelCofork.ofπ h.p ⋯).map F) ≫ F.map h.g'

Tactic:
Cofork.IsColimit.π_desc hp

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✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
S S₁ S₂ : ShortComplex C
h : S.RightHomologyData
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : h.IsPreservedBy F
this✝ : PreservesColimit (parallelPair S.f 0) F
this : PreservesLimit (parallelPair h.g' 0) F
wp : F.map S.f ≫ F.map h.p = 0
hp : IsColimit ((CokernelCofork.ofπ h.p ⋯).map F)
g' : F.obj h.Q ⟶ F.obj S.X₃ := hp.desc (CokernelCofork.ofπ (S.map F).g ⋯)
⊢ Cofork.π (CokernelCofork.ofπ (S.map F).g ⋯) = Cofork.π ((CokernelCofork.ofπ h.p ⋯).map F) ≫ F.map h.g'
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 : ShortComplex C
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
hₗ : S.LeftHomologyData
hᵣ : S.RightHomologyData
inst✝¹ : hₗ.IsPreservedBy F
inst✝ : hᵣ.IsPreservedBy F
⊢ F.map (hₗ.i ≫ hᵣ.p) = (hₗ.map F).π ≫ leftRightHomologyComparison' (hₗ.map F) (hᵣ.map F) ≫ (hᵣ.map F).ι

Tactic:
rw [ShortComplex.π_leftRightHomologyComparison'_ι]

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✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
S : ShortComplex C
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
hₗ : S.LeftHomologyData
hᵣ : S.RightHomologyData
inst✝¹ : hₗ.IsPreservedBy F
inst✝ : hᵣ.IsPreservedBy F
⊢ F.map (hₗ.i ≫ hᵣ.p) = (hₗ.map F).i ≫ (hᵣ.map F).p
Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic

Goal state before:
pp: case pos
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : EnoughInjectives C
X : C
h : IsZero X
this : Injective X
⊢ ∃ p, IsZero X → IsZero p.J

Tactic:
exact ⟨{ J := X, f := 𝟙 X}, by tauto⟩

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
K : WalkingParallelPair ⥤ C
⊢ PreservesLimit K F

Tactic:
let := preservesEqualizer_of_preservesKernels F (K.map WalkingParallelPairHom.left)
        (K.map WalkingParallelPairHom.right)
    apply preservesLimit_of_iso_diagram F (diagramIsoParallelPair K).symm

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

Goal state before:
pp: case mpr
S : ShortComplex Ab
⊢ (∀ (x₂ : ↑S.X₂), (ConcreteCategory.hom S.g) x₂ = 0 → ∃ x₁, (ConcreteCategory.hom S.f) x₁ = x₂) →
    Function.Surjective ⇑S.abToCycles

Tactic:
rintro h ⟨x₂, hx₂⟩
    obtain ⟨x₁, rfl⟩ := h x₂ hx₂
    exact ⟨x₁, rfl⟩

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

Goal state before:
pp: S : ShortComplex Ab
⊢ (∀ (x₂ : ↑S.X₂), (ConcreteCategory.hom S.g) x₂ = 0 → ∃ x₁, (ConcreteCategory.hom S.f) x₁ = x₂) ↔
    Function.Exact ⇑(ConcreteCategory.hom S.f) ⇑(ConcreteCategory.hom S.g)

Tactic:
apply forall_congr'

Goal state after:
S : ShortComplex Ab
⊢ ∀ (a : ↑S.X₂),
    ((ConcreteCategory.hom S.g) a = 0 → ∃ x₁, (ConcreteCategory.hom S.f) x₁ = a) ↔
      ((ConcreteCategory.hom S.g) a = 0 ↔ a ∈ Set.range ⇑(ConcreteCategory.hom S.f))
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
⊢ PreservesColimit (parallelPair f g) F

Tactic:
let := preservesBinaryBiproducts_of_preservesBinaryCoproducts F
  have := additive_of_preservesBinaryBiproducts F
  constructor
  intro c i
  let c' := isColimitCokernelCoforkOfCofork (i.ofIsoColimit (Cofork.isoCoforkOfπ c))
  dsimp only [cokernelCoforkOfCofork_ofπ] at c'
  let iFc := isColimitCoforkMapOfIsColimit' F _ c'
  constructor
  apply
    IsColimit.ofIsoColimit _ ((Cocone.functoriality _ F).mapIso (Cofork.isoCoforkOfπ c).symm)
  apply (isColimitMapCoconeCoforkEquiv F (Cofork.condition c)).invFun
  let p : parallelPair (F.map (f - g)) 0 ≅ parallelPair (F.map f - F.map g) 0 :=
    parallelPair.ext (Iso.refl _) (Iso.refl _) (by simp) (by simp)
  exact
    IsColimit.ofIsoColimit
      (isColimitCoforkOfCokernelCofork ((IsColimit.precomposeHomEquiv p.symm _).symm iFc))
      (Cofork.ext (Iso.refl _) (by simp [p]))

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
hg : S.g = 0
this✝ : S.HasHomology
this : Mono S.fromOpcycles
⊢ Epi S.f

Tactic:
have : S.pOpcycles = 0 := by rw [← cancel_mono S.fromOpcycles, zero_comp, p_fromOpcycles, hg]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
hg : S.g = 0
this✝¹ : S.HasHomology
this✝ : Mono S.fromOpcycles
this : S.pOpcycles = 0
⊢ Epi S.f
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
hg : S.g = 0
⊢ Epi S.f

Tactic:
by
  have := hS.hasHomology
  have := hS.mono_fromOpcycles
  have : S.pOpcycles = 0 := by rw [← cancel_mono S.fromOpcycles, zero_comp, p_fromOpcycles, hg]
  apply Preadditive.epi_of_cancel_zero
  intro A x₂ hx₂
  rw [← S.p_descOpcycles x₂ hx₂, this, zero_comp]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : HasZeroMorphisms C
f : X ⟶ Y
inst✝ : HasKernel f
W : C
h : W ⟶ X
w : (kernelSubobject f).Factors h
⊢ h ≫ f = 0

Tactic:
by
    rw [← Subobject.factorThru_arrow _ _ w, Category.assoc, kernelSubobject_arrow_comp,
      comp_zero]

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✝⁶ : Preadditive C
inst✝⁵ : Preadditive D
F : C ⥤ D
inst✝⁴ : F.Additive
inst✝³ : F.PreservesHomology
inst✝² : HasZeroObject C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasCokernels C
this✝² : ∀ {X Y : C} (f : X ⟶ Y), PreservesColimit (parallelPair f 0) F
this✝¹ : HasBinaryBiproducts C
this✝ : HasCoequalizers C
this : HasZeroObject D
⊢ PreservesFiniteColimits F

Tactic:
exact preservesFiniteColimits_of_preservesCokernels F

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
h : kernel.ι S.g ≫ cokernel.π S.f = 0
Z'✝ : C
g'✝ : S.X₂ ⟶ Z'✝
eq'✝ : S.f ≫ g'✝ = 0
m✝ : Abelian.coimage S.g ⟶ Z'✝
⊢ Abelian.coimage.π S.g ≫ m✝ = g'✝ → m✝ = cokernel.desc (kernel.ι S.g) g'✝ ⋯

Tactic:
hm

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
Z'✝ : C
g'✝ : S.X₂ ⟶ Z'✝
eq'✝ : S.f ≫ g'✝ = 0
m✝ : Abelian.coimage S.g ⟶ Z'✝
hm : Abelian.coimage.π S.g ≫ m✝ = g'✝
⊢ m✝ = cokernel.desc (kernel.ι S.g) g'✝ ⋯
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)
tfae_2_to_3 :
  (∀ (S : ShortComplex C), S.Exact ∧ Epi S.g → (S.map F).Exact ∧ Epi (F.map S.g)) →
    ∀ ⦃X Y : C⦄ (f : X ⟶ Y), PreservesColimit (parallelPair f 0) F
x✝ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), PreservesColimit (parallelPair f 0) F
hF : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), PreservesColimit (parallelPair f 0) F := x✝
⊢ PreservesFiniteColimits F

Tactic:
exact preservesFiniteColimits_of_preservesCokernels F

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

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✝¹ : HasCoproducts C
inst✝ : HasImages C
A : C
s : Set (Subobject A)
f : Subobject A
k : ∀ g ∈ s, g ≤ f
⊢ sSup s ≤ f

Tactic:
by
  fapply le_of_comm
  · refine (underlyingIso _).hom ≫ image.lift ⟨_, f.arrow, ?_, ?_⟩
    · refine Sigma.desc ?_
      rintro ⟨g, m⟩
      refine underlying.map (homOfLE (k _ ?_))
      simpa using m
    · ext
      dsimp [smallCoproductDesc]
      simp
  · dsimp [sSup]
    rw [assoc, image.lift_fac, underlyingIso_hom_comp_eq_mk]

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

Goal state before:
pp: C : Type u_1
D : Type u_2
H : Type u_4
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Category.{v_4, u_4} H
L 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:
rw [hasPointwiseLeftKanExtensionAt_iff_of_natIso_left _ e₁.symm]
  let e : CostructuredArrow.proj L Y ⋙ F' ≅ CostructuredArrow.proj L Y ⋙ F :=
    NatIso.ofComponents fun X ↦ (e₂.app _).symm
  rw [HasPointwiseLeftKanExtensionAt, hasColimit_iff_of_iso e]
  infer_instance

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

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

Tactic:
NatTrans.comp_app,

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
Y : C
η : yoneda.obj Y ⟶ A
X : C
s : yoneda.obj X ⟶ A
p : OverArrows η s
⊢ yoneda.map p.val ≫ η = s

Tactic:
← yonedaEquiv.injective.eq_iff,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
Y : C
η : yoneda.obj Y ⟶ A
X : C
s : yoneda.obj X ⟶ A
p : OverArrows η s
⊢ yonedaEquiv (yoneda.map p.val ≫ η) = 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
G : C ⥤ H
inst✝² : L.HasPointwiseLeftKanExtension G
inst✝¹ : HasColimitsOfShape D H
inst✝ : HasColimitsOfShape C H
X : C
⊢ colimit.ι G X =
    colimit.ι (CostructuredArrow.grothendieckProj L ⋙ G)
        { base := L.obj X, fiber := CostructuredArrow.mk (𝟙 (L.obj X)) } ≫
      (L.colimitIsoColimitGrothendieck G).inv

Tactic:
exact (ι_colimitIsoColimitGrothendieck_inv L G ⟨L.obj X, .mk (𝟙 _)⟩).symm

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

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

Tactic:
NatTrans.comp_app,

Goal state after:
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
L : C ⥤ D
H : Type u_3
inst✝¹ : Category.{v_3, u_3} H
inst✝ : ∀ (F : C ⥤ H), L.HasRightKanExtension F
F : D ⥤ H
G₁ G₂ : C ⥤ H
β : ((whiskeringLeft C D H).obj L).obj F ⟶ G₁
f : G₁ ⟶ G₂
X : C
⊢ β.app X ≫ f.app X =
    (((L.ran.obj G₁).liftOfIsRightKanExtension (L.ranCounit.app G₁) F β).app (L.obj X) ≫ (L.ran.map f).app (L.obj X)) ≫
      (L.ranCounit.app G₂).app X
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✝¹ : HasColimitsOfShape J D
F : D ⥤ E
inst✝ : PreservesColimitsOfShape J F
K : J ⥤ C ⥤ D
c : Cocone K
hc : IsColimit c
⊢ IsColimit (((whiskeringRight C D E).obj F).mapCocone c)

Tactic:
apply evaluationJointlyReflectsColimits _ (fun k => ?_)

Goal state after:
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✝¹ : HasColimitsOfShape J D
F : D ⥤ E
inst✝ : PreservesColimitsOfShape J F
K : J ⥤ C ⥤ D
c : Cocone K
hc : IsColimit c
k : C
⊢ IsColimit (((evaluation C E).obj k).mapCocone (((whiskeringRight C D E).obj F).mapCocone c))
Module: Mathlib.CategoryTheory.Limits.Shapes.Countable

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
J : Type u_2
inst✝² : Countable J
inst✝¹ : Preorder J
inst✝ : IsCofiltered J
d : J
⊢ IsConnected (CostructuredArrow (sequentialFunctor J) d)

Tactic:
by
    obtain ⟨n, (g : (sequentialFunctor J).obj ⟨n⟩ ≤ d)⟩ := sequentialFunctor_initial_aux J d
    have : Nonempty (CostructuredArrow (sequentialFunctor J) d) :=
      ⟨CostructuredArrow.mk (homOfLE g)⟩
    apply isConnected_of_zigzag
    refine fun i j ↦ ⟨[j], ?_⟩
    simp only [List.isChain_cons_cons, Zag, List.isChain_singleton, and_true, ne_eq,
      not_false_eq_true, List.getLast_cons, List.getLast_singleton', reduceCtorEq]
    clear! C
    wlog! h : (unop i.left) ≤ (unop j.left)
    · exact or_comm.1 (this J d n g inferInstance j i (le_of_lt h))
    · right
      exact ⟨CostructuredArrow.homMk (homOfLE h).op rfl⟩

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

Goal state before:
pp: case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
⊢ (cokernelOrderHom X).comp (kernelOrderHom X) = OrderHom.id

Tactic:
change (cokernelOrderHom X).comp (kernelOrderHom X) = _

Goal state after:
case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
⊢ (cokernelOrderHom X).comp (kernelOrderHom X) = OrderHom.id
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
α : F ⟶ L ⋙ F'
inst✝ : F'.IsLeftKanExtension α
c : Cocone F
hc : IsColimit c
s : Cocone F'
m : (F'.coconeOfIsLeftKanExtension α c).pt ⟶ s.pt
hm : ∀ (j : D), (F'.coconeOfIsLeftKanExtension α c).ι.app j ≫ m = s.ι.app j
j : C
this : (F'.descOfIsLeftKanExtension α ((const D).obj c.pt) c.ι).app (L.obj j) ≫ m = s.ι.app (L.obj j)
⊢ α.app j ≫ s.ι.app (L.obj j) = { pt := s.1, ι := α ≫ L.whiskerLeft s.ι }.ι.app j

Tactic:
NatTrans.comp_app,

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
α : F ⟶ L ⋙ F'
inst✝ : F'.IsLeftKanExtension α
c : Cocone F
hc : IsColimit c
s : Cocone F'
m : (F'.coconeOfIsLeftKanExtension α c).pt ⟶ s.pt
hm : ∀ (j : D), (F'.coconeOfIsLeftKanExtension α c).ι.app j ≫ m = s.ι.app j
j : C
this : (F'.descOfIsLeftKanExtension α ((const D).obj c.pt) c.ι).app (L.obj j) ≫ m = s.ι.app (L.obj j)
⊢ α.app j ≫ s.ι.app (L.obj j) = α.app j ≫ (L.whiskerLeft s.ι).app j