mathlib-initiative/mathlib-tactics huggingface dataset:
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
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
S : ShortComplex C
hg : S.g = 0
inst✝ : PreservesColimit (parallelPair S.f 0) F
h : S.LeftHomologyData
this : IsIso h.i
⊢ (parallelPair h.f' 0).map WalkingParallelPairHom.right ≫ (asIso h.i).hom =
    (Iso.refl ((parallelPair h.f' 0).obj WalkingParallelPair.zero)).hom ≫
      (parallelPair S.f 0).map WalkingParallelPairHom.right

Tactic:
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
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
S : ShortComplex C
hf : S.f = 0
inst✝ : PreservesLimit (parallelPair S.g 0) F
h : S.RightHomologyData
⊢ PreservesColimit (parallelPair S.f 0) F

Tactic:
hf

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
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
S : ShortComplex C
hf : S.f = 0
inst✝ : PreservesLimit (parallelPair S.g 0) F
h : S.RightHomologyData
⊢ PreservesColimit (parallelPair 0 0) F
Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic

Goal state before:
pp: case h
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u_1
inst✝² : Category.{v_1, u_1} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝¹ : F.PreservesMonomorphisms
I : D
hI : Injective I
X Y : C
f : X ⟶ G.obj I
g : X ⟶ Y
inst✝ : Mono g
w : F.obj Y ⟶ I
h : F.map g ≫ w = F.map f ≫ adj.counit.app I
⊢ adj.unit.app X ≫ G.map (F.map f ≫ adj.counit.app I) = f

Tactic:
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
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
S : ShortComplex C
hf : S.f = 0
inst✝ : PreservesLimit (parallelPair S.g 0) F
h : S.RightHomologyData
this : IsIso h.p
⊢ (parallelPair S.g 0).map WalkingParallelPairHom.left ≫
      (Iso.refl ((parallelPair S.g 0).obj WalkingParallelPair.one)).hom =
    (asIso h.p).hom ≫ (parallelPair h.g' 0).map WalkingParallelPairHom.left

Tactic:
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
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
S : ShortComplex C
hf : S.f = 0
inst✝ : PreservesLimit (parallelPair S.g 0) F
h : S.RightHomologyData
this : IsIso h.p
⊢ (parallelPair S.g 0).map WalkingParallelPairHom.right ≫
      (Iso.refl ((parallelPair S.g 0).obj WalkingParallelPair.one)).hom =
    (asIso h.p).hom ≫ (parallelPair h.g' 0).map WalkingParallelPairHom.right

Tactic:
simp

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₁.i ≫ h₁ ≫ S₂.f) ≫ S₂.g = 0

Tactic:
simp

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₁.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
⊢ S₁.f ≫ S₁.g ≫ h₂ ≫ H₂.p = 0

Tactic:
simp

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✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
h : S.HomologyData
this✝ : Epi h.left.f'
this : Mono h.right.g'
⊢ h.left.i ≫ S.g = 0

Tactic:
simp

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 : ShortComplex C
⊢ 𝟙 S ≫ 𝟙 S = 𝟙 S

Tactic:
simp

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₂
e : S₁.HomotopyEquiv S₂
e' : S₂.HomotopyEquiv S₃
⊢ (e.hom ≫ e'.hom) ≫ e'.inv ≫ e.inv = e.hom ≫ (e'.hom ≫ e'.inv) ≫ e.inv

Tactic:
simp

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₂
e : S₁.HomotopyEquiv S₂
e' : S₂.HomotopyEquiv S₃
⊢ e.hom ≫ 𝟙 S₂ ≫ e.inv = e.hom ≫ e.inv

Tactic:
simp

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₂
e : S₁.HomotopyEquiv S₂
e' : S₂.HomotopyEquiv S₃
⊢ (e'.inv ≫ e.inv) ≫ e.hom ≫ e'.hom = e'.inv ≫ (e.inv ≫ e.hom) ≫ e'.hom

Tactic:
simp

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₂
e : S₁.HomotopyEquiv S₂
e' : S₂.HomotopyEquiv S₃
⊢ e'.inv ≫ 𝟙 S₂ ≫ e'.hom = e'.inv ≫ e'.hom

Tactic:
simp

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

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
S : ShortComplex C
hS : S.ShortExact
inst✝¹ : Injective S.X₁
inst✝ : Balanced C
this : Mono S.f
⊢ S.f ≫ Injective.factorThru (𝟙 S.X₁) S.f = 𝟙 S.X₁

Tactic:
simp

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

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
S : ShortComplex C
hS : S.ShortExact
inst✝¹ : Projective S.X₃
inst✝ : Balanced C
this : Epi S.g
⊢ Projective.factorThru (𝟙 S.X₃) S.g ≫ S.g = 𝟙 S.X₃

Tactic:
simp

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:
by
  rw [(HomologyData.ofZeros S (IsZero.eq_of_tgt h _ _) (IsZero.eq_of_src h _ _)).exact_iff]
  exact h

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), PreservesColimit (parallelPair f 0) F
X Y : C
f g : X ⟶ Y
this✝ : PreservesBinaryBiproducts F := preservesBinaryBiproducts_of_preservesBinaryCoproducts F
this : F.Additive
c : Cocone (parallelPair f g)
i : IsColimit c
c' : IsColimit (CokernelCofork.ofπ (Cofork.π c) ⋯) :=
  isColimitCokernelCoforkOfCofork (i.ofIsoColimit (Cofork.isoCoforkOfπ c))
iFc : IsColimit (CokernelCofork.ofπ (F.map (Cofork.π c)) ⋯) := isColimitCoforkMapOfIsColimit' F ⋯ c'
⊢ (parallelPair (F.map (f - g)) 0).map WalkingParallelPairHom.left ≫
      (Iso.refl ((parallelPair (F.map (f - g)) 0).obj WalkingParallelPair.one)).hom =
    (Iso.refl ((parallelPair (F.map (f - g)) 0).obj WalkingParallelPair.zero)).hom ≫
      (parallelPair (F.map f - F.map g) 0).map WalkingParallelPairHom.left

Tactic:
simp

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), PreservesColimit (parallelPair f 0) F
X Y : C
f g : X ⟶ Y
this✝ : PreservesBinaryBiproducts F := preservesBinaryBiproducts_of_preservesBinaryCoproducts F
this : F.Additive
c : Cocone (parallelPair f g)
i : IsColimit c
c' : IsColimit (CokernelCofork.ofπ (Cofork.π c) ⋯) :=
  isColimitCokernelCoforkOfCofork (i.ofIsoColimit (Cofork.isoCoforkOfπ c))
iFc : IsColimit (CokernelCofork.ofπ (F.map (Cofork.π c)) ⋯) := isColimitCoforkMapOfIsColimit' F ⋯ c'
⊢ (parallelPair (F.map (f - g)) 0).map WalkingParallelPairHom.right ≫
      (Iso.refl ((parallelPair (F.map (f - g)) 0).obj WalkingParallelPair.one)).hom =
    (Iso.refl ((parallelPair (F.map (f - g)) 0).obj WalkingParallelPair.zero)).hom ≫
      (parallelPair (F.map f - F.map g) 0).map WalkingParallelPairHom.right

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Reflective

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
i : D ⥤ C
inst✝ : Reflective i
X : C
⊢ (reflectorAdjunction i).unit.app (i.obj ((reflector i).obj X)) ≫
      i.map ((reflectorAdjunction i).counit.app ((reflector i).obj X)) =
    i.map
      ((reflector i).map ((reflectorAdjunction i).unit.app X) ≫
        (reflectorAdjunction i).counit.app ((reflector i).obj X))

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Reflective

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
i : D ⥤ C
inst✝ : Reflective i
A B B' : C
h : B ⟶ B'
hB : i.essImage B
hB' : i.essImage B'
f : i.obj ((reflector i).obj A) ⟶ B
⊢ (unitCompPartialBijective A hB').symm (f ≫ h) = (unitCompPartialBijective A hB).symm f ≫ h

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Reflective

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
j : C ⥤ D
inst✝ : Coreflective j
X : D
⊢ j.map ((coreflectorAdjunction j).unit.app ((coreflector j).obj X)) ≫
      (coreflectorAdjunction j).counit.app (j.obj ((coreflector j).obj X)) =
    j.map
      ((coreflectorAdjunction j).unit.app ((coreflector j).obj X) ≫
        (coreflector j).map ((coreflectorAdjunction j).counit.app X))

Tactic:
simp

Goal state after:
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✝² : Preadditive C
inst✝¹ : Preadditive D
S : ShortComplex C
hS : S.Exact
inst✝ : HasZeroObject C
kf : KernelFork S.g
hkf : IsLimit kf
⊢ (Iso.refl kf.pt).hom ≫ Fork.ι (KernelFork.ofι (Fork.ι kf) ⋯) = Fork.ι kf

Tactic:
simp

Goal state after:
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✝² : Preadditive C
inst✝¹ : Preadditive D
S : ShortComplex C
hS : S.Exact
inst✝ : HasZeroObject C
cc : CokernelCofork S.f
hcc : IsColimit cc
⊢ Cofork.π cc ≫ (Iso.refl cc.pt).hom = Cofork.π (CokernelCofork.ofπ (Cofork.π cc) ⋯)

Tactic:
simp

Goal state after:
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✝² : Preadditive C
inst✝¹ : Preadditive D
S : ShortComplex C
hS : S.Exact
inst✝ : HasZeroObject C
cc : CokernelCofork S.f
hcc : IsColimit cc
this : S.HasHomology
⊢ Arrow.mk ((hcc.ofIsoColimit (Cofork.ext (Iso.refl cc.pt) ⋯)).desc (CokernelCofork.ofπ S.g ⋯)) ≅
    Arrow.mk S.fromOpcycles

Tactic:
refine Arrow.isoMk (IsColimit.coconePointUniqueUpToIso hcc S.opcyclesIsCokernel)
      (Iso.refl _) ?_

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✝² : Preadditive C
inst✝¹ : Preadditive D
S : ShortComplex C
hS : S.Exact
inst✝ : HasZeroObject C
cc : CokernelCofork S.f
hcc : IsColimit cc
this : S.HasHomology
⊢ (hcc.coconePointUniqueUpToIso S.opcyclesIsCokernel).hom ≫ (Arrow.mk S.fromOpcycles).hom =
    (Arrow.mk ((hcc.ofIsoColimit (Cofork.ext (Iso.refl cc.pt) ⋯)).desc (CokernelCofork.ofπ S.g ⋯))).hom ≫
      (Iso.refl
          (Arrow.mk ((hcc.ofIsoColimit (Cofork.ext (Iso.refl cc.pt) ⋯)).desc (CokernelCofork.ofπ S.g ⋯))).right).hom
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
⊢ S.f = 0

Tactic:
hf

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
⊢ 0 = 0
Module: Mathlib.CategoryTheory.Adjunction.Restrict

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
D' : Type u₄
inst✝ : Category.{v₄, u₄} D'
iC : C ⥤ C'
iD : D ⥤ D'
L' : C' ⥤ D'
R' : D' ⥤ C'
adj : L' ⊣ R'
hiC : iC.FullyFaithful
hiD : iD.FullyFaithful
L : C ⥤ D
R : D ⥤ C
comm1 : iC ⋙ L' ≅ L ⋙ iD
comm2 : iD ⋙ R' ≅ R ⋙ iC
X : D
⊢ iD.map
      (hiD.preimage
        (comm1.inv.app (R.obj X) ≫
          (adj.homEquiv (iC.obj (R.obj X)) (iD.obj X)).symm
              (𝟙 (iC.obj (R.obj X)) ≫ iC.map (𝟙 (R.obj X)) ≫ comm2.inv.app X) ≫
            𝟙 (iD.obj X))) =
    comm1.inv.app (R.obj X) ≫ L'.map (comm2.inv.app X) ≫ adj.counit.app (iD.obj X)

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst✝ : Mono f
⊢ 𝟙 X ≫ (MonoOver.mk f).arrow = f

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Subobject X
⊢ 𝟙 (underlying.obj P) ≫ (representative.obj P).arrow = P.arrow

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Y
a✝ : MonoOver Z
g : Y ⟶ a✝.obj.left
⊢ (f ≫ g) ≫ a✝.arrow = f ≫ g ≫ a✝.arrow

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasZeroMorphisms C
X Y : C
P : Subobject Y
⊢ 0 ≫ (representative.obj P).arrow = 0

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Subobject X
h : P.Factors P.arrow
⊢ P.factorThru P.arrow h ≫ P.arrow = 𝟙 (underlying.obj P) ≫ P.arrow

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst✝ : Mono f
⊢ (mk f).factorThru f ⋯ ≫ (mk f).arrow = (underlyingIso f).inv ≫ (mk f).arrow

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
P : Subobject Y
f : X ⟶ underlying.obj P
h : P.Factors (f ≫ P.arrow)
⊢ P.factorThru (f ≫ P.arrow) h ≫ P.arrow = f ≫ P.arrow

Tactic:
simp

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

Goal state before:
pp: case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasZeroMorphisms C
X Y : C
P : Subobject Y
h : P.Factors 0
⊢ P.factorThru 0 h ≫ P.arrow = 0 ≫ P.arrow

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
P : Subobject Z
f : X ⟶ Y
g : Y ⟶ Z
h : P.Factors g
⊢ (f ≫ P.factorThru g h) ≫ P.arrow = P.factorThru (f ≫ g) ⋯ ≫ P.arrow

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasZeroMorphisms C
X Y : C
P : Subobject Y
h : P.Factors 0
⊢ P.factorThru 0 h = 0

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
Y Z : C
P Q : Subobject Y
f : Z ⟶ Y
h : P ≤ Q
w : P.Factors f
⊢ Q.factorThru f ⋯ ≫ Q.arrow = (P.factorThru f w ≫ P.ofLE Q h) ≫ Q.arrow

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
X Y : C
P : Subobject Y
f g : X ⟶ Y
wf : P.Factors f
wg : P.Factors g
⊢ (P.factorThru f wf + P.factorThru g wg) ≫ (representative.obj P).arrow = f + g

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
X Y : C
P : Subobject Y
f g : X ⟶ Y
w : P.Factors (f + g)
wf : P.Factors f
wg : P.Factors g
⊢ P.factorThru (f + g) w ≫ P.arrow = (P.factorThru f wf + P.factorThru g wg) ≫ P.arrow

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
X Y : C
P : Subobject Y
f g : X ⟶ Y
w : P.Factors (f + g)
wg : P.Factors g
⊢ (P.factorThru (f + g) w - P.factorThru g wg) ≫ (representative.obj P).arrow = f

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
X Y : C
P : Subobject Y
f g : X ⟶ Y
w : P.Factors (f + g)
wg : P.Factors g
⊢ (P.factorThru (f + g) w - P.factorThru g wg) ≫ P.arrow = P.factorThru f ⋯ ≫ P.arrow

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
X Y : C
P : Subobject Y
f g : X ⟶ Y
w : P.Factors (f + g)
wf : P.Factors f
⊢ (P.factorThru (f + g) w - P.factorThru f wf) ≫ (representative.obj P).arrow = g

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
X Y : C
P : Subobject Y
f g : X ⟶ Y
w : P.Factors (f + g)
wf : P.Factors f
⊢ (P.factorThru (f + g) w - P.factorThru f wf) ≫ P.arrow = P.factorThru g ⋯ ≫ P.arrow

Tactic:
simp

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

Goal state before:
pp: case refl
C : Type u₁
inst✝ : Category.{v₁, u₁} C
A : C
X Y : Subobject A
⊢ eqToHom ⋯ ≫ X.arrow = X.arrow

Tactic:
simp

Goal state after:
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✝² : Preadditive C
inst✝¹ : Preadditive D
S : ShortComplex C
X₁ X₂ : C
inst✝ : HasBinaryBiproduct X₁ X₂
⊢ biprod.inl ≫ biprod.snd = 0

Tactic:
simp

Goal state after:
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✝¹ : Preadditive C
inst✝ : Preadditive D
S : ShortComplex C
h : S.Splitting
⊢ (S.op.f ≫ h.s.op).unop = (𝟙 S.op.X₁).unop

Tactic:
simp

Goal state after:
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✝¹ : Preadditive C
inst✝ : Preadditive D
S : ShortComplex C
h : S.Splitting
⊢ (h.r.op ≫ S.op.g).unop = (𝟙 S.op.X₃).unop

Tactic:
simp

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

Goal state before:
pp: case e'_3
C : Type u₁
inst✝ : Category.{v₁, u₁} C
B : C
X Y : Subobject B
f : underlying.obj X ⟶ underlying.obj Y
w : f ≫ Y.arrow = X.arrow
⊢ X = mk X.arrow

Tactic:
simp

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

Goal state before:
pp: case e'_4
C : Type u₁
inst✝ : Category.{v₁, u₁} C
B : C
X Y : Subobject B
f : underlying.obj X ⟶ underlying.obj Y
w : f ≫ Y.arrow = X.arrow
⊢ Y = mk Y.arrow

Tactic:
simp

Goal state after:
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✝¹ : Preadditive C
inst✝ : Preadditive D
S✝ : ShortComplex C
S : ShortComplex Cᵒᵖ
h : S.Splitting
⊢ (S.unop.f ≫ h.s.unop).op = (𝟙 S.unop.X₁).op

Tactic:
simp

Goal state after:
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✝¹ : Preadditive C
inst✝ : Preadditive D
S✝ : ShortComplex C
S : ShortComplex Cᵒᵖ
h : S.Splitting
⊢ (h.r.unop ≫ S.unop.g).op = (𝟙 S.unop.X₃).op

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
S : Subobject X
⊢ S = mk S.arrow

Tactic:
simp

Goal state after:
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✝³ : Preadditive C
inst✝² : Preadditive D
S : ShortComplex C
inst✝¹ : Balanced C
hS : S.Exact
inst✝ : Mono S.f
this✝ : S.HasHomology
this : IsIso S.toCycles
⊢ (asIso S.toCycles).symm.hom ≫ Fork.ι (KernelFork.ofι S.f ⋯) = Fork.ι (KernelFork.ofι S.iCycles ⋯)

Tactic:
simp

Goal state after:
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✝³ : Preadditive C
inst✝² : Preadditive D
S : ShortComplex C
inst✝¹ : Balanced C
hS : S.Exact
inst✝ : Epi S.g
this✝ : S.HasHomology
this : IsIso S.fromOpcycles
⊢ Cofork.π (CokernelCofork.ofπ S.pOpcycles ⋯) ≫ (asIso S.fromOpcycles).hom = Cofork.π (CokernelCofork.ofπ S.g ⋯)

Tactic:
simp

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
inst✝¹ : Balanced C
hS : S.Exact
A : C
k : A ⟶ S.X₂
hk : k ≫ S.g = 0
inst✝ : Mono S.f
⊢ hS.lift k hk ≫ S.f = k

Tactic:
simp

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
inst✝¹ : Balanced C
hS : S.Exact
A : C
k : S.X₂ ⟶ A
hk : S.f ≫ k = 0
inst✝ : Epi S.g
⊢ S.g ≫ hS.desc k hk = k

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
B : C
X : Subobject B
⊢ X.ofLE X ⋯ ≫ X.arrow = 𝟙 (underlying.obj X) ≫ X.arrow

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
B A₁ : C
f : A₁ ⟶ B
inst✝ : Mono f
⊢ ofMkLEMk f f ⋯ ≫ f = 𝟙 A₁ ≫ f

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P Q : MonoOver X
f : P ⟶ Q
⊢ Over.Hom.left f.hom ≫ Q.obj.hom = P.obj.hom

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P Q : MonoOver X
f : P ⟶ Q
x✝ : IsIso (Over.Hom.left f.hom)
⊢ (asIso (Over.Hom.left f.hom)).hom ≫ Q.obj.hom = P.obj.hom

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
A B : C
e : A ≅ B
⊢ map (e.hom ≫ e.inv) = map (𝟙 A)

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
A B : C
e : A ≅ B
⊢ map (e.inv ≫ e.hom) = map (𝟙 B)

Tactic:
simp

Goal state after: