mathlib-initiative/mathlib-tactics huggingface dataset:
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
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
h₂' : S₂.LeftHomologyData := LeftHomologyData.ofEpiOfIsIsoOfMono φ h₁
this : IsIso (leftHomologyMap' φ h₁ h₂')
⊢ IsIso (leftHomologyMap' φ h₁ h₂)

Tactic:
have eq := leftHomologyMap'_comp φ (𝟙 S₂) h₁ h₂' h₂

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₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
h₂' : S₂.LeftHomologyData := LeftHomologyData.ofEpiOfIsIsoOfMono φ h₁
this : IsIso (leftHomologyMap' φ h₁ h₂')
eq : leftHomologyMap' (φ ≫ 𝟙 S₂) h₁ h₂ = leftHomologyMap' φ h₁ h₂' ≫ leftHomologyMap' (𝟙 S₂) h₂' h₂
⊢ IsIso (leftHomologyMap' φ h₁ h₂)
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 : C
k : A ⟶ S.X₂
hk : k ≫ S.g = 0
inst✝ : S.HasLeftHomology
A' : C
α : A' ⟶ A
⊢ α ≫ 0 = 0

Tactic:
comp_zero

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.LeftHomologyData
A : C
k : A ⟶ S.X₂
hk : k ≫ S.g = 0
inst✝ : S.HasLeftHomology
A' : C
α : A' ⟶ A
⊢ 0 = 0
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 : C
k : A ⟶ S.X₂
hk : k ≫ S.g = 0
inst✝ : S.HasLeftHomology
x : A ⟶ S.X₁
hx : k = x ≫ S.f
⊢ x ≫ 0 = 0

Tactic:
comp_zero

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.LeftHomologyData
A : C
k : A ⟶ S.X₂
hk : k ≫ S.g = 0
inst✝ : S.HasLeftHomology
x : A ⟶ S.X₁
hx : k = x ≫ S.f
⊢ 0 = 0
Module: Mathlib.Algebra.Homology.ShortComplex.Homology

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

Tactic:
have := S.isIso_leftHomologyπ hf

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
hf : S.f = 0
inst✝ : S.HasHomology
this : IsIso S.leftHomologyπ
⊢ IsIso S.homologyπ
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 (S₁.homologyπ ≫ homologyMap φ)

Tactic:
rw [homologyπ_naturality φ]

Goal state after:
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π)
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 : C
k : S.X₂ ⟶ A
hk : S.f ≫ k = 0
inst✝¹ : S.HasRightHomology
φ : S₁ ⟶ S
inst✝ : S₁.HasRightHomology
⊢ φ.τ₁ ≫ 0 = 0

Tactic:
comp_zero

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 : C
k : S.X₂ ⟶ A
hk : S.f ≫ k = 0
inst✝¹ : S.HasRightHomology
φ : S₁ ⟶ S
inst✝ : S₁.HasRightHomology
⊢ 0 = 0
Module: Mathlib.Algebra.Homology.ShortComplex.Abelian

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
S : ShortComplex C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroMorphisms D
Z'✝ : C
k : cokernel S.f ⟶ Z'✝
hk : (kernel.ι S.g ≫ cokernel.π S.f) ≫ k = 0
b : Abelian.coimage S.g ⟶ Z'✝
hb : S.cokernelToAbelianCoimage ≫ b = k
⊢ b = cokernel.desc (kernel.ι S.g) (cokernel.π S.f ≫ k) ⋯

Tactic:
simp only [← cancel_epi S.cokernelToAbelianCoimage, ← cancel_epi (cokernel.π S.f), hb,
        cokernel_π_comp_cokernelToAbelianCoimage_assoc, cokernel.π_desc]

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 φ₁ φ₂
ψ : S₃ ⟶ S₁
⊢ ψ.τ₂ ≫ 0 = 0

Tactic:
comp_zero

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 φ₁ φ₂
ψ : S₃ ⟶ S₁
⊢ 0 = 0
Module: Mathlib.CategoryTheory.Abelian.Opposite

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
A B : Cᵒᵖ
g : A ⟶ B
⊢ factorThruImage g ≫ (imageUnopOp g).inv = (image.ι g.unop).op

Tactic:
by
  rw [Iso.comp_inv_eq, image_ι_op_comp_imageUnopOp_hom]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X E✝ X✝ : Type u
f : X ⟶ X✝
e : E✝ ⟶ X✝
x✝ : Epi e
he : Function.Surjective ⇑(ConcreteCategory.hom e)
⊢ (↾fun x ↦ ⋯.choose) ≫ e = f

Tactic:
ext x; exact (he (f x)).choose_spec

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X : Type u₁
inst✝ : Nonempty X
X✝ Y✝ : Type u₁
g : X✝ ⟶ X
f : X✝ ⟶ Y✝
mono : Mono f
⊢ (f ≫
      ↾fun z ↦
        if h : z ∈ Set.range ⇑(ConcreteCategory.hom f) then (ConcreteCategory.hom g) (Classical.choose h) else ⋯.some) =
    g

Tactic:
by
      ext y
      classical
      change dite (f y ∈ Set.range f) (fun h => g (Classical.choose h)) _ = _
      split_ifs <;> rename_i h
      · rw [mono_iff_injective] at mono
        simp [mono (Classical.choose_spec h)]
      · exact False.elim (h ⟨y, rfl⟩)

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

Goal state before:
pp: case mp
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ≌ D
H : EnoughProjectives C
X : D
⊢ ProjectivePresentation X

Tactic:
exact F.symm.projectivePresentationOfMapProjectivePresentation _
      (Nonempty.some (H.presentation (F.inverse.obj X)))

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₁ : S₁.LeftHomologyData
H₂ : S₂.LeftHomologyData
h₀ : S₁.X₁ ⟶ S₂.X₁
h₀_f : h₀ ≫ S₂.f = 0
h₁ : S₁.X₂ ⟶ S₂.X₁
h₂ : S₁.X₃ ⟶ S₂.X₂
h₃ : S₁.X₃ ⟶ S₂.X₃
g_h₃ : S₁.g ≫ h₃ = 0
⊢ H₁.π ≫ 0 = 0

Tactic:
comp_zero

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₁ : S₁.LeftHomologyData
H₂ : S₂.LeftHomologyData
h₀ : S₁.X₁ ⟶ S₂.X₁
h₀_f : h₀ ≫ S₂.f = 0
h₁ : S₁.X₂ ⟶ S₂.X₁
h₂ : S₁.X₃ ⟶ S₂.X₂
h₃ : S₁.X₃ ⟶ S₂.X₃
g_h₃ : S₁.g ≫ h₃ = 0
⊢ 0 = 0
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₂ : ShortComplex C
φ₁ φ₂ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
h₁ : S₁.HomologyData
h₂ : S₂.HomologyData
⊢ homologyMap' φ₁ h₁ h₂ = homologyMap' φ₂ h₁ h₂

Tactic:
rw [h.eq_add_nullHomotopic, homologyMap'_add, homologyMap'_nullHomotopic, add_zero]

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
this : PreservesLimit (parallelPair (K.map WalkingParallelPairHom.left) (K.map WalkingParallelPairHom.right)) F :=
  preservesEqualizer_of_preservesKernels F (K.map WalkingParallelPairHom.left) (K.map WalkingParallelPairHom.right)
⊢ PreservesLimit K F

Tactic:
apply preservesLimit_of_iso_diagram F (diagramIsoParallelPair K).symm

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
h : IsZero S.X₂
⊢ S.Exact

Tactic:
rw [(HomologyData.ofZeros S (IsZero.eq_of_tgt h _ _) (IsZero.eq_of_src h _ _)).exact_iff]
  exact h

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

Goal state before:
pp: case mp
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.HomologyData
this : S.HasHomology
z : IsZero h.left.H
⊢ h.left.π ≫ 0 = 0

Tactic:
comp_zero

Goal state after:
case mp
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.HomologyData
this : S.HasHomology
z : IsZero h.left.H
⊢ 0 = 0
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
h : S.Exact
X Y : C
a : X ⟶ S.X₂
ha : a ≫ S.g = 0
b : S.X₂ ⟶ Y
hb : S.f ≫ b = 0
this : S.HasHomology
eq : S.iCycles ≫ S.pOpcycles = 0
⊢ S.liftCycles a ha ≫ 0 = 0

Tactic:
comp_zero

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.Exact
X Y : C
a : X ⟶ S.X₂
ha : a ≫ S.g = 0
b : S.X₂ ⟶ Y
hb : S.f ≫ b = 0
this : S.HasHomology
eq : S.iCycles ≫ S.pOpcycles = 0
⊢ 0 = 0
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
hf : S.f = 0
this✝¹ : S.HasHomology
this✝ : Epi S.toCycles
this : S.iCycles = 0
A : C
x₂ : A ⟶ S.X₂
hx₂ : x₂ ≫ S.g = 0
⊢ S.liftCycles x₂ hx₂ ≫ 0 = 0

Tactic:
comp_zero

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
hf : S.f = 0
this✝¹ : S.HasHomology
this✝ : Epi S.toCycles
this : S.iCycles = 0
A : C
x₂ : A ⟶ S.X₂
hx₂ : x₂ ≫ S.g = 0
⊢ 0 = 0
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
hS : S.Exact
a✝ : Epi S.f
⊢ 0 = S.f ≫ 0

Tactic:
comp_zero

Goal state after:
case mp
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
a✝ : Epi S.f
⊢ 0 = 0
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
hf : S.f = 0
hg : S.g = 0
this : Mono S.g
⊢ 0 = 0 ≫ 0

Tactic:
comp_zero

Goal state after:
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
this : Mono S.g
⊢ 0 = 0
Module: Mathlib.CategoryTheory.Subobject.Basic

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
p : Subobject X → Subobject X → Prop
h : ∀ ⦃A B : C⦄ (f : A ⟶ X) (g : B ⟶ X) [inst : Mono f] [inst_1 : Mono g], p (mk f) (mk g)
P Q : Subobject X
⊢ p P Q

Tactic:
induction P, Q using Quotient.inductionOn₂' with | _ a b
   =>  _ 

Goal state after:
case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
p : Subobject X → Subobject X → Prop
h : ∀ ⦃A B : C⦄ (f : A ⟶ X) (g : B ⟶ X) [inst : Mono f] [inst_1 : Mono g], p (mk f) (mk g)
a b : MonoOver X
⊢ p (Quotient.mk'' a) (Quotient.mk'' b)
Module: Mathlib.CategoryTheory.Subobject.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
B A : C
X : Subobject B
f : A ⟶ B
inst✝ : Mono f
i : A ≅ underlying.obj X
w : i.hom ≫ X.arrow = f
⊢ i.symm.hom ≫ f = X.arrow

Tactic:
Iso.symm_hom,

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
B A : C
X : Subobject B
f : A ⟶ B
inst✝ : Mono f
i : A ≅ underlying.obj X
w : i.hom ≫ X.arrow = f
⊢ i.inv ≫ f = X.arrow
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

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
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
hg₂ : S₂.g = 0
⊢ φ.τ₁ ≫ 0 = 0

Tactic:
comp_zero

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
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
hg₂ : S₂.g = 0
⊢ 0 = 0
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
⊢ (kernelSubobject f).factorThru h w ≫ 0 = 0

Tactic:
comp_zero

Goal state after:
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
⊢ 0 = 0
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✝ : HasCokernels C
X A B : C
f : A ⟶ X
g : B ⟶ X
hf : Mono f
hg : Mono g
h : Subobject.mk f ≤ Subobject.mk g
⊢ ofMkLEMk f g h ≫ 0 = 0

Tactic:
comp_zero

Goal state after:
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✝ : HasCokernels C
X A B : C
f : A ⟶ X
g : B ⟶ X
hf : Mono f
hg : Mono g
h : Subobject.mk f ≤ Subobject.mk g
⊢ 0 = 0
Module: Mathlib.CategoryTheory.Subobject.Limits

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : HasImage f
⊢ (imageSubobjectIso f).hom ≫ image.ι f = (imageSubobject f).arrow

Tactic:
by simp [imageSubobjectIso]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : HasImage f
⊢ (imageSubobjectIso f).inv ≫ (imageSubobject f).arrow = image.ι f

Tactic:
by simp [imageSubobjectIso]

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
A B : C
⊢ ⊥.Factors 0

Tactic:
exact ⟨0, by simp⟩

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
W'✝ : C
u : W'✝ ⟶ S.X₂
hu : u ≫ S.g = 0
⊢ kernel.lift S.g u hu ≫ 0 = 0

Tactic:
comp_zero

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
W'✝ : C
u : W'✝ ⟶ S.X₂
hu : u ≫ S.g = 0
⊢ 0 = 0
Module: Mathlib.CategoryTheory.Abelian.Exact

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
Z : C
tfae_2_to_1 : cokernel.π f = 0 → Epi f
x✝ : Epi f
⊢ 0 = f ≫ 0

Tactic:
comp_zero

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
Z : C
tfae_2_to_1 : cokernel.π f = 0 → Epi f
x✝ : Epi f
⊢ 0 = 0
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
B : C
P : I → Subobject B
a✝¹ : I
s✝ : Finset I
a✝ : a✝¹ ∉ s✝
ih : ∀ i ∈ s✝, (P i).Factors (s✝.inf P).arrow
i✝ : I
m : i✝ ∈ insert a✝¹ s✝
⊢ (P i✝).Factors ((insert a✝¹ s✝).inf P).arrow

Tactic:
rw [Finset.inf_insert]

Goal state after:
case insert
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
I : Type u_1
B : C
P : I → Subobject B
a✝¹ : I
s✝ : Finset I
a✝ : a✝¹ ∉ s✝
ih : ∀ i ∈ s✝, (P i).Factors (s✝.inf P).arrow
i✝ : I
m : i✝ ∈ insert a✝¹ s✝
⊢ (P i✝).Factors (P a✝¹ ⊓ s✝.inf P).arrow
Module: Mathlib.CategoryTheory.Abelian.Exact

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Abelian C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : Abelian D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : F.Faithful
S : ShortComplex C
hS : kernel.ι (F.map S.g) ≫ cokernel.π (F.map S.f) = 0
k : F.obj (Limits.kernel S.g) ⟶ Limits.kernel (F.map S.g)
hk : k ≫ kernel.ι (F.map S.g) = F.map (kernel.ι S.g)
l : cokernel (F.map S.f) ⟶ F.obj (cokernel S.f)
hl : cokernel.π (F.map S.f) ≫ l = F.map (cokernel.π S.f)
⊢ k ≫ kernel.ι (F.map S.g) ≫ cokernel.π (F.map S.f) ≫ l = 0

Tactic:
reassoc_of% hS,

Goal state after:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Abelian C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : Abelian D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : F.Faithful
S : ShortComplex C
hS : kernel.ι (F.map S.g) ≫ cokernel.π (F.map S.f) = 0
k : F.obj (Limits.kernel S.g) ⟶ Limits.kernel (F.map S.g)
hk : k ≫ kernel.ι (F.map S.g) = F.map (kernel.ι S.g)
l : cokernel (F.map S.f) ⟶ F.obj (cokernel S.f)
hl : cokernel.π (F.map S.f) ≫ l = F.map (cokernel.π S.f)
⊢ k ≫ 0 ≫ l = 0
Module: Mathlib.CategoryTheory.Abelian.Exact

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Abelian C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : Abelian D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : F.Faithful
S : ShortComplex C
hS : kernel.ι (F.map S.g) ≫ cokernel.π (F.map S.f) = 0
k : F.obj (Limits.kernel S.g) ⟶ Limits.kernel (F.map S.g)
hk : k ≫ kernel.ι (F.map S.g) = F.map (kernel.ι S.g)
l : cokernel (F.map S.f) ⟶ F.obj (cokernel S.f)
hl : cokernel.π (F.map S.f) ≫ l = F.map (cokernel.π S.f)
⊢ k ≫ 0 = 0

Tactic:
comp_zero

Goal state after:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Abelian C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : Abelian D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : F.Faithful
S : ShortComplex C
hS : kernel.ι (F.map S.g) ≫ cokernel.π (F.map S.f) = 0
k : F.obj (Limits.kernel S.g) ⟶ Limits.kernel (F.map S.g)
hk : k ≫ kernel.ι (F.map S.g) = F.map (kernel.ι S.g)
l : cokernel (F.map S.f) ⟶ F.obj (cokernel S.f)
hl : cokernel.π (F.map S.f) ≫ l = F.map (cokernel.π S.f)
⊢ 0 = 0
Module: Mathlib.CategoryTheory.Subobject.Lattice

Goal state before:
pp: case a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasPullbacks C
A : C
f₁ f₂ : Subobject A
inst✝ : HasBinaryProduct f₁ f₂
⊢ f₁ ⊓ f₂ ≤ (f₁ ⨯ f₂)

Tactic:
· apply leOfHom
    exact prod.lift (inf_le_left _ _).hom (inf_le_right _ _).hom

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A B : C
inst✝ : HasBinaryProduct A B
⊢ prod.fst.op ≫ (opProdIsoCoprod A B).hom = coprod.inl

Tactic:
by
  rw [opProdIsoCoprod, ← op_comp, prod.lift_fst, Quiver.Hom.op_unop]

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
F : C ⥤ H
inst✝ : L.HasPointwiseLeftKanExtension F
X : C
⊢ (L.leftKanExtensionUnit F).app X ≫ (L.leftKanExtensionObjIsoColimit F (L.obj X)).hom =
    colimit.ι (proj L (L.obj X) ⋙ F) (CostructuredArrow.mk (𝟙 (L.obj X)))

Tactic:
by
  simpa using leftKanExtensionUnit_leftKanExtension_map_leftKanExtensionObjIsoColimit_hom L F
    (L.obj X) (CostructuredArrow.mk (𝟙 _))

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
F' F'' : D ⥤ H
e : F' ≅ F''
L : C ⥤ D
F : C ⥤ H
α : L ⋙ F' ⟶ F
α' : L ⋙ F'' ⟶ F
comm : L.whiskerLeft e.hom ≫ α' = α
a✝ : F''.IsRightKanExtension α'
⊢ L.whiskerLeft (e.symm.hom ≫ e.hom) ≫ α' = α'

Tactic:
Iso.symm_hom,

Goal state after:
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
F' F'' : D ⥤ H
e : F' ≅ F''
L : C ⥤ D
F : C ⥤ H
α : L ⋙ F' ⟶ F
α' : L ⋙ F'' ⟶ F
comm : L.whiskerLeft e.hom ≫ α' = α
a✝ : F''.IsRightKanExtension α'
⊢ L.whiskerLeft (e.inv ≫ e.hom) ≫ α' = α'
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
F' F'' : D ⥤ H
e : F' ≅ F''
L : C ⥤ D
F : C ⥤ H
α : F ⟶ L ⋙ F'
α' : F ⟶ L ⋙ F''
comm : α ≫ L.whiskerLeft e.hom = α'
a✝ : F''.IsLeftKanExtension α'
⊢ α ≫ L.whiskerLeft (e.hom ≫ e.symm.hom) = α

Tactic:
Iso.symm_hom,

Goal state after:
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
F' F'' : D ⥤ H
e : F' ≅ F''
L : C ⥤ D
F : C ⥤ H
α : F ⟶ L ⋙ F'
α' : F ⟶ L ⋙ F''
comm : α ≫ L.whiskerLeft e.hom = α'
a✝ : F''.IsLeftKanExtension α'
⊢ α ≫ L.whiskerLeft (e.hom ≫ e.inv) = α
Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise

Goal state before:
pp: C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Category.{v_3, u_3} D'
inst✝¹ : Category.{v_4, u_4} H
L : C ⥤ D
L' : C ⥤ D'
F : C ⥤ H
inst✝ : L.HasPointwiseRightKanExtension F
Y₁ Y₂ Y₃ : D
f : Y₁ ⟶ Y₂
f' : Y₂ ⟶ Y₃
j : StructuredArrow Y₃ L
⊢ limit.lift (StructuredArrow.proj Y₃ L ⋙ F)
        { pt := limit (StructuredArrow.proj Y₁ L ⋙ F),
          π :=
            { app := fun g ↦ limit.π (StructuredArrow.proj Y₁ L ⋙ F) ((StructuredArrow.map (f ≫ f')).obj g),
              naturality := ⋯ } } ≫
      limit.π (StructuredArrow.proj Y₃ L ⋙ F) j =
    (limit.lift (StructuredArrow.proj Y₂ L ⋙ F)
          { pt := limit (StructuredArrow.proj Y₁ L ⋙ F),
            π :=
              { app := fun g ↦ limit.π (StructuredArrow.proj Y₁ L ⋙ F) ((StructuredArrow.map f).obj g),
                naturality := ⋯ } } ≫
        limit.lift (StructuredArrow.proj Y₃ L ⋙ F)
          { pt := limit (StructuredArrow.proj Y₂ L ⋙ F),
            π :=
              { app := fun g ↦ limit.π (StructuredArrow.proj Y₂ L ⋙ F) ((StructuredArrow.map f').obj g),
                naturality := ⋯ } }) ≫
      limit.π (StructuredArrow.proj Y₃ L ⋙ F) j

Tactic:
dsimp
    simp only [limit.lift_π, assoc]
    congr 1
    apply StructuredArrow.map_comp

Goal state after:
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 : StructuredArrow S T
⊢ ∀ ⦃A_1 : StructuredArrow S T⦄ (f : A_1 ⟶ A) [inst : 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:
intro P f hf q hq

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