mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Category.ModuleCat.Kernels

Goal state before:
pp: R : Type u
inst✝ : Ring R
M N P : ModuleCat R
f✝ f : M ⟶ N
g : N ⟶ P
H : Function.Exact ⇑(Hom.hom f) ⇑(Hom.hom g)
H₂ : Function.Surjective ⇑(Hom.hom g)
⊢ ∀ (j : WalkingParallelPair),
    (cokernelCocone f).ι.app j ≫
        (((Hom.hom g).ker.quotEquivOfEq (Hom.hom f).range ⋯).toModuleIso.symm ≪≫
            ((Hom.hom g).quotKerEquivOfSurjective H₂).toModuleIso).hom =
      (CokernelCofork.ofπ g ⋯).ι.app j

Tactic:
rintro ⟨⟩ <;> ext x
    · simpa using! (Function.Exact.apply_apply_eq_zero H x).symm
    · rfl

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

Goal state before:
pp: C : Type u
𝒞 : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasLimit (pair X Y)
inst✝ : HasLimit (parallelPair (prod.fst ≫ f) (prod.snd ≫ g))
π₁ : X ⨯ Y ⟶ X := prod.fst
π₂ : X ⨯ Y ⟶ Y := prod.snd
e : equalizer (π₁ ≫ f) (π₂ ≫ g) ⟶ X ⨯ Y := equalizer.ι (π₁ ≫ f) (π₂ ≫ g)
s : PullbackCone f g
⊢ (BinaryFan.mk (s.π.app WalkingCospan.left) (s.π.app WalkingCospan.right)).π.app { as := WalkingPair.left } ≫ f =
    (BinaryFan.mk (s.π.app WalkingCospan.left) (s.π.app WalkingCospan.right)).π.app { as := WalkingPair.right } ≫ g

Tactic:
exact PullbackCone.condition _

Goal state after:
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₂
⊢ Function.Injective ⇑f.dualMap ↔ Function.Surjective ⇑f

Tactic:
refine ⟨Function.mtr fun not_surj inj ↦ ?_, dualMap_injective_of_surjective⟩

Goal state after:
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₂
not_surj : ¬Function.Surjective ⇑f
inj : Function.Injective ⇑f.dualMap
⊢ False
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 - a - (b - 0)

Tactic:
sub_sub_sub,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b : X ⟶ Y
| 0 - b - (a - 0)
Module: Mathlib.CategoryTheory.Abelian.NonPreadditive

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

Tactic:
sub_sub_sub,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a : X ⟶ Y
⊢ a - 0 - (a - a) = a
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:
sub_sub_sub,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b : X ⟶ Y
⊢ 0 - -b - (0 - a) = b + a
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 - (a - b) = 0 - a + b

Tactic:
sub_sub_sub,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b : X ⟶ Y
⊢ 0 - a - (0 - b) = 0 - a + b
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 c : X ⟶ Y
⊢ a - b - (0 - c) = a - (b - c)

Tactic:
sub_sub_sub,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b c : X ⟶ Y
⊢ a - 0 - (b - c) = a - (b - c)
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
inst✝ : S.HasRightHomology
⊢ h.rightHomologyIso.hom ≫ h.ι = S.rightHomologyι ≫ h.opcyclesIso.hom

Tactic:
simp only [← cancel_mono h.opcyclesIso.inv, ← cancel_epi h.rightHomologyIso.inv,
    assoc, Iso.inv_hom_id_assoc, Iso.hom_inv_id, comp_id, rightHomologyIso_inv_comp_rightHomologyι]

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 : ShortComplex C
A : C
inst✝ : S.HasHomology
k : A ⟶ S.X₂
x : A ⟶ S.X₁
hx : k = x ≫ S.f
⊢ S.liftCycles k ⋯ ≫ S.homologyπ = 0

Tactic:
dsimp only [homologyπ]
  rw [S.liftCycles_leftHomologyπ_eq_zero_of_boundary_assoc k x hx, 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
φ : S₁ ⟶ S₂
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
h : Epi (cyclesMap φ)
⊢ Epi (cyclesMap φ ≫ S₂.homologyπ)

Tactic:
apply epi_comp

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h₁₂ : Homotopy φ₁ φ₂
h₂₃ : Homotopy φ₂ φ₃
⊢ φ₁.τ₃ = h₁₂.h₃ + h₂₃.h₃ + (h₁₂.h₂ + h₂₃.h₂) ≫ S₂.g + φ₃.τ₃

Tactic:
rw [h₁₂.comm₃, h₂₃.comm₃, add_comp]; abel

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
hkf : IsLimit kf
⊢ hkf.lift (KernelFork.ofι S.f ⋯) = S.toCycles ≫ (S.isoCyclesOfIsLimit hkf).inv

Tactic:
have := Fork.IsLimit.mono hkf
  simp [← cancel_mono kf.ι]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
h' : Homotopy φ₃ φ₄
⊢ (φ₁ + φ₃).τ₃ = h.h₃ + h'.h₃ + (h.h₂ + h'.h₂) ≫ S₂.g + (φ₂ + φ₄).τ₃

Tactic:
rw [add_τ₃, add_τ₃, h.comm₃, h'.comm₃, add_comp]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
h' : Homotopy φ₃ φ₄
⊢ h.h₃ + h.h₂ ≫ S₂.g + φ₂.τ₃ + (h'.h₃ + h'.h₂ ≫ S₂.g + φ₄.τ₃) =
    h.h₃ + h'.h₃ + (h.h₂ ≫ S₂.g + h'.h₂ ≫ S₂.g) + (φ₂.τ₃ + φ₄.τ₃)
Module: Mathlib.CategoryTheory.Preadditive.Projective.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝¹ : F.Full
inst✝ : F.Faithful
P : C
hP : Projective (F.obj P)
E✝ X✝ : C
f : P ⟶ X✝
g : E✝ ⟶ X✝
x✝ : Epi g
⊢ ∃ f', f' ≫ g = f

Tactic:
have := Adjunction.leftAdjoint_preservesColimits.{0, 0} adj
    rcases (@hP).1 (F.map f) (F.map g) with ⟨f', hf'⟩
    use adj.unit.app _ ≫ G.map f' ≫ (inv <| adj.unit.app _)
    exact F.map_injective (by simpa)

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
⊢ (opMap φ₁).τ₁.unop = (S₂.op.f ≫ h.h₂.op + h.h₃.op + (opMap φ₂).τ₁).unop

Tactic:
dsimp; rw [h.comm₃]; abel

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁✝ S₂✝ S₃ : ShortComplex C
φ₁✝ φ₂✝ φ₃ φ₄ : S₁✝ ⟶ S₂✝
S₁ S₂ : ShortComplex Cᵒᵖ
φ₁ φ₂ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
⊢ (unopMap φ₁).τ₁.op = (S₂.unop.f ≫ h.h₂.unop + h.h₃.unop + (unopMap φ₂).τ₁).op

Tactic:
dsimp; rw [h.comm₃]; abel

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

Goal state before:
pp: case h₃
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ : ShortComplex C
φ₁ φ₂ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
⊢ φ₁.τ₃ = (φ₂ + S₁.nullHomotopic S₂ h.h₀ ⋯ h.h₁ h.h₂ h.h₃ ⋯).τ₃

Tactic:
dsimp; rw [h.comm₃]; abel

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
e : S₁ ≅ S₂
h : S₁.ShortExact
this : Epi S₁.g
⊢ Epi (S₁.g ≫ e.hom.τ₃)

Tactic:
apply epi_comp

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
X Y Z : C
π₁ : Z ⟶ X
π₂ : Z ⟶ Y
inst✝ : PreservesLimit (parallelPair π₂ 0) F
i : IsLimit (BinaryFan.mk π₁ π₂)
bc : BinaryBicone X Y := BinaryBicone.ofLimitCone i
presf : PreservesLimit (parallelPair bc.snd 0) F := inst✝
hf : IsLimit bc.sndKernelFork := BinaryBicone.isLimitSndKernelFork i
⊢ IsLimit (F.mapCone (BinaryFan.mk π₁ π₂))

Tactic:
exact (isLimitMapConeBinaryFanEquiv F π₁ π₂).invFun
    (BinaryBicone.isBilimitOfKernelInl (F.mapBinaryBicone bc)
    (isLimitMapConeForkEquiv' F bc.inl_snd (isLimitOfPreserves F hf))).isLimit

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
⊢ PreservesLimit (parallelPair f g) F

Tactic:
have := additive_of_preservesBinaryBiproducts F

Goal state after:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Preadditive C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : Preadditive D
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : HasBinaryBiproducts C
inst✝ : ∀ {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
⊢ PreservesLimit (parallelPair f g) 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
this : PreservesBinaryBiproducts F := preservesBinaryBiproducts_of_preservesBinaryCoproducts F
⊢ PreservesColimit (parallelPair f g) F

Tactic:
have := additive_of_preservesBinaryBiproducts F

Goal state after:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Preadditive C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : Preadditive D
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : HasBinaryBiproducts C
inst✝ : ∀ {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
⊢ PreservesColimit (parallelPair f g) F
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

Goal state before:
pp: case mp
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
inst✝ : HasZeroObject C
hg : S.g = 0
this✝¹ : S.HasHomology
h : IsZero S.homology
this✝ : IsIso S.iCycles
this : Epi S.toCycles
⊢ Epi (S.toCycles ≫ S.iCycles)

Tactic:
apply epi_comp

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
s s' : S.Splitting
h : s.s = s'.s
⊢ s = s'

Tactic:
have := s.mono_f

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
s s' : S.Splitting
h : s.s = s'.s
this : Mono S.f
⊢ s = s'
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

Goal state before:
pp: case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
w : φ.τ₂ ≫ S₂.g = 0
⊢ { X₁ := S₁.X₂, X₂ := S₂.X₂, X₃ := S₂.X₃, f := φ.τ₂, g := S₂.g, zero := ⋯ }.Exact ∧ Mono φ.τ₂ →
    IsIso (S₂.liftCycles φ.τ₂ ⋯)

Tactic:
rintro ⟨h₁, h₂⟩

Goal state after:
case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
w : φ.τ₂ ≫ S₂.g = 0
h₁ : { X₁ := S₁.X₂, X₂ := S₂.X₂, X₃ := S₂.X₃, f := φ.τ₂, g := S₂.g, zero := ⋯ }.Exact
h₂ : Mono φ.τ₂
⊢ IsIso (S₂.liftCycles φ.τ₂ ⋯)
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
e : X ≅ Y
A B : Subobject X
⊢ { toFun := (map e.hom).obj, invFun := (map e.inv).obj, left_inv := ⋯, right_inv := ⋯ } A ≤
      { toFun := (map e.hom).obj, invFun := (map e.inv).obj, left_inv := ⋯, right_inv := ⋯ } B ↔
    A ≤ B

Tactic:
by
    dsimp
    constructor
    · intro h
      apply_fun (map e.inv).obj at h
      · simpa only [← map_comp, e.hom_inv_id, map_id] using h
      · apply Functor.monotone
    · intro h
      apply_fun (map e.hom).obj at h
      · exact h
      · apply Functor.monotone

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

Goal state before:
pp: case refine_1
C : Type u
inst✝³ : Category.{v, u} C
X✝ Y Z : C
inst✝² : HasZeroMorphisms C
f : X✝ ⟶ Y
inst✝¹ : HasKernel f
inst✝ : HasKernels C
X : C
A B : Cᵒᵖ
g : B ⟶ op X
hg : Mono g
i : A ≅ B
hf : Mono (i.hom ≫ g)
⊢ kernel (i.hom ≫ g).unop ≅ kernel g.unop

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✝ : HasKernels C
X : C
A B : Cᵒᵖ
g : B ⟶ op X
hg : Mono g
i : A ≅ B
hf : Mono (i.hom ≫ g)
⊢ Iso.hom ?refine_1 ≫ kernel.ι g.unop = kernel.ι (i.hom ≫ g).unop

Tactic:
· exact
            IsLimit.conePointUniqueUpToIso (limit.isLimit _)
              (isKernelCompMono (limit.isLimit (parallelPair g.unop 0)) i.unop.hom rfl)

Goal state after:
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✝ : HasKernels C
X : C
A B : Cᵒᵖ
g : B ⟶ op X
hg : Mono g
i : A ≅ B
hf : Mono (i.hom ≫ g)
⊢ ((limit.isLimit (parallelPair (g.unop ≫ i.unop.hom) 0)).conePointUniqueUpToIso
          (isKernelCompMono (limit.isLimit (parallelPair g.unop 0)) i.unop.hom ⋯)).hom ≫
      kernel.ι g.unop =
    kernel.ι (i.hom ≫ g).unop
Module: Mathlib.CategoryTheory.Abelian.Exact

Goal state before:
pp: case mpr
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 ⋯
a✝ : Epi (imageToKernel' S.f S.g ⋯)
⊢ Epi (factorThruImage S.f ≫ imageToKernel' S.f S.g ⋯)

Tactic:
apply epi_comp

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
inst✝¹ : HasImage f
inst✝ : HasEqualizers C
⊢ Epi (factorThruImage f ≫ (imageSubobjectIso f).inv)

Tactic:
apply epi_comp

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
X Y Z : C
f✝ : X ⟶ Y
inst✝⁴ : HasImage f✝
inst✝³ : HasEqualizers C
X' : C
h : X' ⟶ X
inst✝² : Epi h
f : X ⟶ Y
inst✝¹ : HasImage f
inst✝ : HasImage (h ≫ f)
⊢ Epi ((imageSubobject (h ≫ f)).ofLE (imageSubobject f) ⋯)

Tactic:
by
  rw [ofLE_mk_le_mk_of_comm (image.preComp h f)]
  · infer_instance
  · simp

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

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

Tactic:
simp [ih]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
α : Type w
inst✝¹ : HasFiniteProducts C
inst✝ : HasLimitsOfShape (Finset (Discrete α))ᵒᵖ C
F : Discrete α ⥤ C
s : Cone F
m :
  s.pt ⟶
    { pt := limit (liftToFinsetObj F),
        π := Discrete.natTrans fun j ↦ limit.π (liftToFinsetObj F) (op {j}) ≫ Pi.π (fun x ↦ F.obj ↑x) ⟨j, ⋯⟩ }.pt
h :
  ∀ (j : Discrete α),
    m ≫
        { pt := limit (liftToFinsetObj F),
                π :=
                  Discrete.natTrans fun j ↦
                    limit.π (liftToFinsetObj F) (op {j}) ≫ Pi.π (fun x ↦ F.obj ↑x) ⟨j, ⋯⟩ }.π.app
          j =
      s.π.app j
⊢ m =
    limit.lift (liftToFinsetObj F)
      { pt := s.pt, π := { app := fun x ↦ Pi.lift fun x_1 ↦ s.π.app ↑x_1, naturality := ⋯ } }

Tactic:
apply limit.hom_ext
        rintro t
        dsimp [liftToFinsetObj]
        apply limit.hom_ext
        rintro ⟨⟨j, hj⟩⟩
        convert! h j using 1
        · simp [← limit.w (liftToFinsetObj F) ⟨⟨⟨Finset.singleton_subset_iff.2 hj⟩⟩⟩]
          rfl
        · simp

Goal state after:
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))) u = yonedaEquiv s

Tactic:
hε,

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.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
E E' : L.RightExtension F
h : E.IsPointwiseRightKanExtension
G : L.RightExtension F
Y₁ Y₂ : D
φ : Y₁ ⟶ Y₂
X : StructuredArrow Y₂ L
⊢ ((CostructuredArrow.left G).map φ ≫ (h Y₂).lift (G.coneAt Y₂)) ≫ (E.coneAt Y₂).π.app X =
    ((h Y₁).lift (G.coneAt Y₁) ≫ (CostructuredArrow.left E).map φ) ≫ (E.coneAt Y₂).π.app X

Tactic:
by
        rw [assoc, (h Y₂).fac (coneAt G Y₂) X]
        simpa using ((h Y₁).fac (coneAt G Y₁) ((StructuredArrow.map φ).obj X)).symm

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

Goal state before:
pp: C : Type u_1
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_3, u_3} H
inst✝² : Category.{v_4, u_4} D
inst✝¹ : Category.{v_5, u_5} D'
L : C ⥤ D
L' : D ⥤ D'
F₀ : C ⥤ H
F₁ : D ⥤ H
α : F₀ ⟶ L ⋙ F₁
inst✝ : F₁.IsLeftKanExtension α
F₂ : D' ⥤ H
L'' : C ⥤ D'
e : L ⋙ L' ≅ L''
β : F₁ ⟶ L' ⋙ F₂
γ : F₀ ⟶ L'' ⋙ F₂
hγ : α ≫ L.whiskerLeft β ≫ (L.associator L' F₂).inv ≫ whiskerRight e.hom F₂ = γ
Ψ : (L ⋙ L').LeftExtension F₀ ≌ L''.LeftExtension F₀ := leftExtensionEquivalenceOfIso₁ e F₀
hα : StructuredArrow.IsUniversal (LeftExtension.mk F₁ α)
⊢ F₂.IsLeftKanExtension β ↔ F₂.IsLeftKanExtension γ

Tactic:
refine ⟨fun ⟨⟨h⟩⟩ => ⟨⟨?_⟩⟩, fun ⟨⟨h⟩⟩ => ⟨⟨?_⟩⟩⟩

Goal state after:
case refine_1
C : Type u_1
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_3, u_3} H
inst✝² : Category.{v_4, u_4} D
inst✝¹ : Category.{v_5, u_5} D'
L : C ⥤ D
L' : D ⥤ D'
F₀ : C ⥤ H
F₁ : D ⥤ H
α : F₀ ⟶ L ⋙ F₁
inst✝ : F₁.IsLeftKanExtension α
F₂ : D' ⥤ H
L'' : C ⥤ D'
e : L ⋙ L' ≅ L''
β : F₁ ⟶ L' ⋙ F₂
γ : F₀ ⟶ L'' ⋙ F₂
hγ : α ≫ L.whiskerLeft β ≫ (L.associator L' F₂).inv ≫ whiskerRight e.hom F₂ = γ
Ψ : (L ⋙ L').LeftExtension F₀ ≌ L''.LeftExtension F₀ := leftExtensionEquivalenceOfIso₁ e F₀
hα : StructuredArrow.IsUniversal (LeftExtension.mk F₁ α)
x✝ : F₂.IsLeftKanExtension β
h : StructuredArrow.IsUniversal (LeftExtension.mk F₂ β)
⊢ StructuredArrow.IsUniversal (LeftExtension.mk F₂ γ)

case refine_2
C : Type u_1
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_3, u_3} H
inst✝² : Category.{v_4, u_4} D
inst✝¹ : Category.{v_5, u_5} D'
L : C ⥤ D
L' : D ⥤ D'
F₀ : C ⥤ H
F₁ : D ⥤ H
α : F₀ ⟶ L ⋙ F₁
inst✝ : F₁.IsLeftKanExtension α
F₂ : D' ⥤ H
L'' : C ⥤ D'
e : L ⋙ L' ≅ L''
β : F₁ ⟶ L' ⋙ F₂
γ : F₀ ⟶ L'' ⋙ F₂
hγ : α ≫ L.whiskerLeft β ≫ (L.associator L' F₂).inv ≫ whiskerRight e.hom F₂ = γ
Ψ : (L ⋙ L').LeftExtension F₀ ≌ L''.LeftExtension F₀ := leftExtensionEquivalenceOfIso₁ e F₀
hα : StructuredArrow.IsUniversal (LeftExtension.mk F₁ α)
x✝ : F₂.IsLeftKanExtension γ
h : StructuredArrow.IsUniversal (LeftExtension.mk F₂ γ)
⊢ StructuredArrow.IsUniversal (LeftExtension.mk F₂ β)
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 ⥤ ℰ
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₂)
Y : ℰ
f : L.obj P ⟶ Y
Z : Cᵒᵖ
z : P.obj Z
⊢ (hom ((((uliftYonedaAdjunction L α).homEquiv P Y) f).app Z)) z =
    { down := α.app (unop Z) ≫ L.map (uliftYonedaEquiv.symm z) ≫ f }

Tactic:
simp [uliftYonedaAdjunction, restrictedULiftYonedaHomEquiv,
    restrictedULiftYonedaHomEquiv', IsColimit.homEquiv]

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
inst✝ : Balanced C
hP : P.IsSeparating
X Y : C
f : X ⟶ Y
hf : ∀ (G : C), P G → ∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h
Z✝ : C
g h : Y ⟶ Z✝
hgh : f ≫ g = f ≫ h
G : C
hG : P G
t : G ⟶ X
⊢ (t ≫ f) ≫ g = (t ≫ f) ≫ h

Tactic:
rw [Category.assoc, hgh, Category.assoc]

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : C
h : (coyoneda.obj (op G)).ReflectsIsomorphisms
X Y : C
f : X ⟶ Y
hf : ∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h
this : IsIso ((coyoneda.obj (op G)).map f)
⊢ IsIso f

Tactic:
exact @isIso_of_reflects_iso _ _ _ _ _ _ _ (coyoneda.obj (op G)) _ h

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

Goal state before:
pp: case refine_2
G : GrpCat
inst✝ : Subsingleton ↑G
X : GrpCat
f : X ⟶ G
⊢ f = default

Tactic:
· ext
    subsingleton

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

Goal state before:
pp: case refine_2
G : CommGrpCat
inst✝ : Subsingleton ↑G
X : CommGrpCat
f : X ⟶ G
⊢ f = default

Tactic:
· ext
    subsingleton

Goal state after: