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
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
i : h.K ⟶ S₁.X₂ := h.i ≫ inv φ.τ₂
wi : i ≫ S₁.g = 0
W'✝ : C
x : W'✝ ⟶ S₁.X₂
hx : x ≫ S₁.g = 0
⊢ 0 ≫ φ.τ₃ = 0

Tactic:
zero_comp

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
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
i : h.K ⟶ S₁.X₂ := h.i ≫ inv φ.τ₂
wi : i ≫ S₁.g = 0
W'✝ : C
x : W'✝ ⟶ S₁.X₂
hx : x ≫ S₁.g = 0
⊢ 0 = 0
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
⊢ (homologyMap φ).op = S₂.homologyOpIso.inv ≫ homologyMap (opMap φ) ≫ S₁.homologyOpIso.hom

Tactic:
by
  dsimp only [homologyMap, homologyOpIso]
  rw [homologyMap'_op]
  dsimp only [Iso.symm, Iso.trans, Iso.op, Iso.refl, rightHomologyIso, leftHomologyIso,
    leftHomologyOpIso, leftHomologyMapIso', rightHomologyMapIso',
    LeftHomologyData.leftHomologyIso, homologyMap']
  simp only [assoc, rightHomologyMap'_op, op_comp, ← leftHomologyMap'_comp_assoc, id_comp,
    opMap_id, comp_id, HomologyData.op_left]

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
⊢ 0 ≫ S.leftHomologyIso.hom = 0

Tactic:
zero_comp

Goal state after:
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
⊢ 0 = 0
Module: Mathlib.Algebra.Homology.ShortComplex.Homology

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S S₁ S₂ S₃ S₄ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.HomologyData
h₂ : S₂.HomologyData
A : C
inst✝ : S.HasHomology
k : S.X₂ ⟶ A
x : S.X₃ ⟶ A
hx : k = S.g ≫ x
⊢ 0 ≫ x = 0

Tactic:
zero_comp

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S S₁ S₂ S₃ S₄ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.HomologyData
h₂ : S₂.HomologyData
A : C
inst✝ : S.HasHomology
k : S.X₂ ⟶ A
x : S.X₃ ⟶ A
hx : k = S.g ≫ x
⊢ 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
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
⊢ IsIso (leftHomologyMap' φ h₁ h₂)

Tactic:
let h₂' := LeftHomologyData.ofEpiOfIsIsoOfMono φ h₁
  have : IsIso (leftHomologyMap' φ h₁ h₂') := by
    rw [(LeftHomologyMapData.ofEpiOfIsIsoOfMono φ h₁).leftHomologyMap'_eq]
    dsimp
    infer_instance
  have eq := leftHomologyMap'_comp φ (𝟙 S₂) h₁ h₂' h₂
  rw [comp_id] at eq
  rw [eq]
  infer_instance

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 : C
k : A ⟶ S.X₂
hk : k ≫ S.g = 0
inst✝¹ : S.HasLeftHomology
φ : S ⟶ S₁
inst✝ : S₁.HasLeftHomology
⊢ 0 ≫ φ.τ₃ = 0

Tactic:
zero_comp

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
φ : S ⟶ S₁
inst✝ : S₁.HasLeftHomology
⊢ 0 = 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
h : S.RightHomologyData
A : C
k : S.X₂ ⟶ A
hk : S.f ≫ k = 0
inst✝ : S.HasRightHomology
A' : C
α : A ⟶ A'
⊢ 0 ≫ α = 0

Tactic:
zero_comp

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

Tactic:
zero_comp

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
x : S.X₃ ⟶ A
hx : k = S.g ≫ x
⊢ 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
γ : kernel S.g ⟶ cokernel S.f := kernel.ι S.g ≫ cokernel.π S.f
g' : cokernel S.f ⟶ S.X₃ := cokernel.desc S.f S.g ⋯
hg' : g' = cokernel.π γ ≫ cokernel.desc γ g' ⋯
⊢ 0 ≫ cokernel.desc γ g' ⋯ = 0

Tactic:
zero_comp

Goal state after:
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
γ : kernel S.g ⟶ cokernel S.f := kernel.ι S.g ≫ cokernel.π S.f
g' : cokernel S.f ⟶ S.X₃ := cokernel.desc S.f S.g ⋯
hg' : g' = cokernel.π γ ≫ cokernel.desc γ g' ⋯
⊢ 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
X Y : C
f : X ⟶ Y
A B : Cᵒᵖ
g : A ⟶ B
⊢ f ≫ (kernel.ι f.op).unop = 0

Tactic:
rw [← f.unop_op, ← unop_comp, f.unop_op]
      simp

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
A B : Cᵒᵖ
g : A ⟶ B
⊢ (cokernel.π f.op).unop ≫ f = 0

Tactic:
rw [← f.unop_op, ← unop_comp, f.unop_op]
      simp

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 : ShortComplex C
F : C ⥤ D
inst✝³ : F.PreservesZeroMorphisms
inst✝² : S.HasHomology
inst✝¹ : F.PreservesLeftHomologyOf S
inst✝ : F.PreservesRightHomologyOf S
γ : HomologyMapData (𝟙 (S.map F)) (S.map F).homologyData (S.homologyData.map F)
eq : γ.left.φH ≫ (S.homologyData.map F).iso.hom = (S.map F).homologyData.iso.hom ≫ γ.right.φH
⊢ (S.map F).homologyData.iso.hom ≫
      rightHomologyMap' (𝟙 (S.map F)) (S.map F).homologyData.right (S.homologyData.right.map F) ≫
        F.map S.homologyData.iso.inv =
    leftHomologyMap' (𝟙 (S.map F)) (S.map F).homologyData.left (S.homologyData.left.map F)

Tactic:
rw [← γ.left.leftHomologyMap'_eq, ← γ.right.rightHomologyMap'_eq] at eq

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
inst✝² : S.HasHomology
inst✝¹ : F.PreservesLeftHomologyOf S
inst✝ : F.PreservesRightHomologyOf S
γ : HomologyMapData (𝟙 (S.map F)) (S.map F).homologyData (S.homologyData.map F)
eq :
  leftHomologyMap' (𝟙 (S.map F)) (S.map F).homologyData.left (S.homologyData.map F).left ≫
      (S.homologyData.map F).iso.hom =
    (S.map F).homologyData.iso.hom ≫
      rightHomologyMap' (𝟙 (S.map F)) (S.map F).homologyData.right (S.homologyData.map F).right
⊢ (S.map F).homologyData.iso.hom ≫
      rightHomologyMap' (𝟙 (S.map F)) (S.map F).homologyData.right (S.homologyData.right.map F) ≫
        F.map S.homologyData.iso.inv =
    leftHomologyMap' (𝟙 (S.map F)) (S.map F).homologyData.left (S.homologyData.left.map F)
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✝ : G.PreservesEpimorphisms
P : C
hP : Projective P
E✝ X✝ : D
f : F.obj P ⟶ X✝
g : E✝ ⟶ X✝
x✝ : Epi g
f' : P ⟶ G.obj E✝
hf' : f' ≫ G.map g = adj.unit.app P ≫ G.map f
⊢ ∃ f', f' ≫ g = f

Tactic:
use F.map f' ≫ adj.counit.app _

Goal state after:
case h
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✝ : G.PreservesEpimorphisms
P : C
hP : Projective P
E✝ X✝ : D
f : F.obj P ⟶ X✝
g : E✝ ⟶ X✝
x✝ : Epi g
f' : P ⟶ G.obj E✝
hf' : f' ≫ G.map g = adj.unit.app P ≫ G.map f
⊢ (F.map f' ≫ adj.counit.app E✝) ≫ g = f
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₁.RightHomologyData
H₂ : S₂.RightHomologyData
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 ≫ H₂.ι = 0

Tactic:
zero_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₁ : S₁.RightHomologyData
H₂ : S₂.RightHomologyData
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.Exact

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

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

Goal state after:
Module: Mathlib.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
this : S.pOpcycles = 0
A : C
x₂ : S.X₂ ⟶ A
hx₂ : S.f ≫ x₂ = 0
⊢ 0 ≫ S.descOpcycles x₂ hx₂ = 0

Tactic:
zero_comp

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
A : C
x₂ : S.X₂ ⟶ A
hx₂ : S.f ≫ x₂ = 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✝ : Mono S.g
⊢ 0 = 0 ≫ S.g

Tactic:
zero_comp

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✝ : Mono S.g
⊢ 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
inst✝¹ : Balanced C
hS : S.Exact
h : S.LeftHomologyData
inst✝ : Mono S.f
this : Epi h.f'
⊢ IsIso h.f'

Tactic:
have := mono_of_mono_fac h.f'_i

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
S : ShortComplex C
inst✝¹ : Balanced C
hS : S.Exact
h : S.LeftHomologyData
inst✝ : Mono S.f
this✝ : Epi h.f'
this : Mono h.f'
⊢ IsIso h.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
inst✝⁴ : Balanced C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.Exact
inst✝³ : Mono S₁.f
inst✝² : Mono S₂.f
inst✝¹ : Mono φ.τ₁
inst✝ : Mono φ.τ₃
A : C
x₂ : A ⟶ S₁.X₂
hx₂ : x₂ ≫ φ.τ₂ = 0
x₁ : A ⟶ S₁.X₁
hx₁ : x₁ ≫ S₁.f = x₂
this : x₁ = 0
⊢ 0 ≫ S₁.f = 0

Tactic:
zero_comp

Goal state after:
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
inst✝⁴ : Balanced C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.Exact
inst✝³ : Mono S₁.f
inst✝² : Mono S₂.f
inst✝¹ : Mono φ.τ₁
inst✝ : Mono φ.τ₃
A : C
x₂ : A ⟶ S₁.X₂
hx₂ : x₂ ≫ φ.τ₂ = 0
x₁ : A ⟶ S₁.X₁
hx₁ : x₁ ≫ S₁.f = x₂
this : x₁ = 0
⊢ 0 = 0
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₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
⊢ 0 ≫ φ.τ₃ = 0

Tactic:
zero_comp

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

Tactic:
zero_comp

Goal state after:
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
⊢ 0 = 0
Module: Mathlib.CategoryTheory.Subobject.Limits

Goal state before:
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✝ : HasCokernels C
X A B : C
g : B ⟶ X
hg : Mono g
i : A ≅ B
hf : Mono (i.hom ≫ g)
⊢ (((colimit.isColimit (parallelPair (i.hom ≫ g) 0)).coconePointUniqueUpToIso
                (isCokernelEpiComp (colimit.isColimit (parallelPair g 0)) i.hom ⋯)).symm.op.hom ≫
        (cokernel.π g).op).unop =
    (cokernel.π (i.hom ≫ g)).op.unop

Tactic:
simp only [Iso.comp_inv_eq, Iso.op_hom, Iso.symm_hom, unop_comp, Quiver.Hom.unop_op,
            colimit.comp_coconePointUniqueUpToIso_hom, Cofork.ofπ_ι_app,
            coequalizer.cofork_π]

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ᵒᵖ
f : A ⟶ op X
g : B ⟶ op X
hf : Mono f
hg : Mono g
h : Subobject.mk f ≤ Subobject.mk g
⊢ 0 ≫ (ofMkLEMk g f h).unop = 0

Tactic:
zero_comp

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✝ : HasKernels C
X : C
A B : Cᵒᵖ
f : A ⟶ op X
g : B ⟶ op X
hf : Mono f
hg : Mono g
h : Subobject.mk f ≤ Subobject.mk g
⊢ 0 = 0
Module: Mathlib.CategoryTheory.Subobject.Lattice

Goal state before:
pp: case refine_1
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasImages C
inst✝ : HasBinaryCoproducts C
A : C
f g h : MonoOver A
k₁ : f ⟶ h
k₂ : g ⟶ h
⊢ ((sup.obj f).obj g).obj.left ⟶ h.obj.left

pp: case refine_2
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasImages C
inst✝ : HasBinaryCoproducts C
A : C
f g h : MonoOver A
k₁ : f ⟶ h
k₂ : g ⟶ h
⊢ ?refine_1 ≫ h.arrow = ((sup.obj f).obj g).arrow

Tactic:
· apply image.lift ⟨_, h.arrow, coprod.desc k₁.hom.left k₂.hom.left, _⟩
    ext
    · simp [w k₁]
    · simp [w k₂]

Goal state after:
case refine_2
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasImages C
inst✝ : HasBinaryCoproducts C
A : C
f g h : MonoOver A
k₁ : f ⟶ h
k₂ : g ⟶ h
⊢ image.lift
        { I := h.obj.left, m := h.arrow, m_mono := ⋯, e := coprod.desc (Over.Hom.left k₁.hom) (Over.Hom.left k₂.hom),
          fac := ⋯ } ≫
      h.arrow =
    ((sup.obj f).obj g).arrow
Module: Mathlib.CategoryTheory.Subobject.Limits

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
W X Y Z : C
f : W ⟶ X
inst✝² : HasImage f
g : Y ⟶ Z
inst✝¹ : HasImage g
sq : Arrow.mk f ⟶ Arrow.mk g
inst✝ : HasImageMap sq
⊢ image.map sq ≫ (imageSubobjectIso (Arrow.mk g).hom).inv = (imageSubobjectIso f).inv ≫ imageSubobjectMap sq

Tactic:
by
  ext
  simpa using image.map_ι sq

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
u : S.X₂ ⟶ Z'✝
hu : S.f ≫ u = 0
⊢ 0 ≫ cokernel.desc S.f u hu = 0

Tactic:
zero_comp

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
u : S.X₂ ⟶ Z'✝
hu : S.f ≫ u = 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 : kernel.ι f = 0 → Mono f
x✝ : Mono f
⊢ 0 = 0 ≫ f

Tactic:
zero_comp

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 : kernel.ι f = 0 → Mono f
x✝ : Mono f
⊢ 0 = 0
Module: Mathlib.CategoryTheory.Limits.Filtered

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
h : ∀ {J : Type v} [inst : SmallCategory J] [FinCategory J] (F : J ⥤ C), ∃ X, Nonempty (limit (F ⋙ coyoneda.obj (op X)))
J : Type v
x✝¹ : SmallCategory J
x✝ : FinCategory J
F : J ⥤ C
⊢ Nonempty (Cone F)

Tactic:
obtain ⟨pt, ⟨π⟩⟩ := h F

Goal state after:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
h : ∀ {J : Type v} [inst : SmallCategory J] [FinCategory J] (F : J ⥤ C), ∃ X, Nonempty (limit (F ⋙ coyoneda.obj (op X)))
J : Type v
x✝¹ : SmallCategory J
x✝ : FinCategory J
F : J ⥤ C
pt : C
π : limit (F ⋙ coyoneda.obj (op pt))
⊢ Nonempty (Cone F)
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✝ : HasWidePullbacks C
A : C
s : Set (Subobject A)
f : Subobject A
hf : f ∈ s
⊢ sInf s ≤ f

Tactic:
fapply le_of_comm
  · exact (underlyingIso _).hom ≫
      Limits.limit.π (wideCospan s)
        (some ⟨equivShrink (Subobject A) f,
          Set.mem_image_of_mem (equivShrink (Subobject A)) hf⟩) ≫
      eqToHom (congr_arg (fun X : Subobject A => (X : C)) (Equiv.symm_apply_apply _ _))
  · dsimp [sInf]
    simp only [Category.assoc, ← underlyingIso_hom_comp_eq_mk,
      Iso.cancel_iso_hom_left]
    convert! limit.w (wideCospan s) (WidePullbackShape.Hom.term _)
    simp

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

Goal state before:
pp: case refine_1.refine_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
A : Cᵒᵖ
f : A ⟶ op X
hf : Mono f
⊢ op (cokernel (kernel.ι f.unop)) ⟶ A

pp: case refine_1.refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
A : Cᵒᵖ
f : A ⟶ op X
hf : Mono f
⊢ A ⟶ op (cokernel (kernel.ι f.unop))

pp: case refine_1.refine_3
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
A : Cᵒᵖ
f : A ⟶ op X
hf : Mono f
⊢ (?refine_1.refine_1 ≫ ?refine_1.refine_2).unop = (𝟙 (op (cokernel (kernel.ι f.unop)))).unop

pp: case refine_1.refine_4
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
A : Cᵒᵖ
f : A ⟶ op X
hf : Mono f
⊢ (?refine_1.refine_2 ≫ ?refine_1.refine_1).unop = (𝟙 A).unop

pp: case refine_1.refine_5
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
A : Cᵒᵖ
f : A ⟶ op X
hf : Mono f
⊢ { hom := ?refine_1.refine_1, inv := ?refine_1.refine_2, hom_inv_id := ⋯, inv_hom_id := ⋯ }.hom ≫ f =
    (cokernel.π (kernel.ι f.unop)).op

Tactic:
· exact (Abelian.epiDesc f.unop _ (cokernel.condition (kernel.ι f.unop))).op

Goal state after:
case refine_1.refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
A : Cᵒᵖ
f : A ⟶ op X
hf : Mono f
⊢ A ⟶ op (cokernel (kernel.ι f.unop))

case refine_1.refine_3
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
A : Cᵒᵖ
f : A ⟶ op X
hf : Mono f
⊢ ((epiDesc f.unop (cokernel.π (kernel.ι f.unop)) ⋯).op ≫ ?refine_1.refine_2).unop =
    (𝟙 (op (cokernel (kernel.ι f.unop)))).unop

case refine_1.refine_4
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
A : Cᵒᵖ
f : A ⟶ op X
hf : Mono f
⊢ (?refine_1.refine_2 ≫ (epiDesc f.unop (cokernel.π (kernel.ι f.unop)) ⋯).op).unop = (𝟙 A).unop

case refine_1.refine_5
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
A : Cᵒᵖ
f : A ⟶ op X
hf : Mono f
⊢ { hom := (epiDesc f.unop (cokernel.π (kernel.ι f.unop)) ⋯).op, inv := ?refine_1.refine_2, hom_inv_id := ⋯,
          inv_hom_id := ⋯ }.hom ≫
      f =
    (cokernel.π (kernel.ι f.unop)).op
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Small

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : C ⥤ D
T : D
inst✝¹ : EssentiallySmall.{w, v₁, u₁} C
inst✝ : LocallySmall.{w, v₂, u₂} D
⊢ EssentiallySmall.{w, v₁, max u₁ v₂} (CostructuredArrow S T)

Tactic:
rw [← essentiallySmall_congr
    (CostructuredArrow.pre (equivSmallModel.{w} C).inverse S T).asEquivalence]
  exact essentiallySmall_of_small_of_locallySmall _

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

Goal state before:
pp: case refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : P.op.IsDetecting
X Y : C
f : X ⟶ Y
hf : ∀ (G : C), P G → ∀ (h : X ⟶ G), ∃! h', f ≫ h' = h
⊢ IsIso f

Tactic:
refine (isIso_op_iff _).1 (hP _ fun G hG h => ?_)
    obtain ⟨t, ht, ht'⟩ := hf (unop G) hG h.unop
    exact
      ⟨t.op, Quiver.Hom.unop_inj ht, fun y hy => Quiver.Hom.unop_inj (ht' _ (Quiver.Hom.op_inj hy))⟩

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

Goal state before:
pp: case refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : P.op.IsCodetecting
X Y : C
f : X ⟶ Y
hf : ∀ (G : C), P G → ∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h
⊢ IsIso f

Tactic:
refine (isIso_op_iff _).1 (hP _ fun G hG h => ?_)
    obtain ⟨t, ht, ht'⟩ := hf (unop G) hG h.unop
    exact
      ⟨t.op, Quiver.Hom.unop_inj ht, fun y hy => Quiver.Hom.unop_inj (ht' _ (Quiver.Hom.op_inj hy))⟩

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : ∀ (X : C), ∃ ι s, ∃ (_ : ∀ (i : ι), P (s i)), ∃ c x p, Epi p
X Y : C
f g : X ⟶ Y
h : ∀ (G : C), P G → ∀ (h : G ⟶ X), h ≫ f = h ≫ g
⊢ f = g

Tactic:
obtain ⟨ι, s, hs, c, hc, p, _⟩ := hP X

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : ∀ (X : C), ∃ ι s, ∃ (_ : ∀ (i : ι), P (s i)), ∃ c x p, Epi p
X Y : C
f g : X ⟶ Y
h : ∀ (G : C), P G → ∀ (h : G ⟶ X), h ≫ f = h ≫ g
ι : Type w
s : ι → C
hs : ∀ (i : ι), P (s i)
c : Cofan s
hc : IsColimit c
p : c.pt ⟶ X
h✝ : Epi p
⊢ f = g
Module: Mathlib.CategoryTheory.Generator.Basic

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

Tactic:
exact hasInitial_of_unique ((⊥ : Subobject (piObj (Subtype.val : Subtype P → C))) : C)

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasSeparator C
⊢ HasCoseparator Cᵒᵖ

Tactic:
simp [*]

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasCoseparator C
⊢ HasSeparator Cᵒᵖ

Tactic:
simp [*]

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasDetector C
⊢ HasCodetector Cᵒᵖ

Tactic:
simp [*]

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasCodetector C
⊢ HasDetector Cᵒᵖ

Tactic:
simp [*]

Goal state after: