awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.ShortComplex.QuasiIso
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
γ : LeftHomologyMapData φ h₁ h₂
rw : IsIso γ.φH ↔ IsIso (leftHomologyMap' φ h₁ h₂)
rw₁ rw₂ : IsIso γ.φH ↔ IsIso γ.φH
⊢ QuasiIso φ ↔ IsIso (leftHomologyMap' φ h₁ h₂)

Tactic:
rw [γ.quasiIso_iff, γ.leftHomologyMap'_eq]

Premises used: CategoryTheory.ShortComplex.LeftHomologyMapData.leftHomologyMap'_eq, CategoryTheory.ShortComplex.LeftHomologyMapData.quasiIso_iff
-- Module: Mathlib.Algebra.Homology.ShortComplex.QuasiIso
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
have : ∀ (γ : RightHomologyMapData φ h₁ h₂), QuasiIso φ ↔ IsIso (rightHomologyMap' φ h₁ h₂)
⊢ QuasiIso φ ↔ IsIso (rightHomologyMap' φ h₁ h₂)

Tactic:
have γ : RightHomologyMapData φ h₁ h₂ := default
-- Module: Mathlib.Algebra.Homology.ShortComplex.QuasiIso
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
γ : RightHomologyMapData φ h₁ h₂
rw : IsIso γ.φH ↔ IsIso (rightHomologyMap' φ h₁ h₂)
rw₁ rw₂ : IsIso γ.φH ↔ IsIso γ.φH
⊢ QuasiIso φ ↔ IsIso (rightHomologyMap' φ h₁ h₂)

Tactic:
rw [γ.quasiIso_iff, γ.rightHomologyMap'_eq]

Premises used: CategoryTheory.ShortComplex.RightHomologyMapData.rightHomologyMap'_eq, CategoryTheory.ShortComplex.RightHomologyMapData.quasiIso_iff
-- Module: Mathlib.Algebra.Homology.ShortComplex.QuasiIso
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
φ : S₁ ⟶ S₂
h₁ : S₁.HomologyData
h₂ : S₂.HomologyData
⊢ QuasiIso φ ↔ IsIso (homologyMap' φ h₁ h₂)

Tactic:
quasiIso_iff_isIso_leftHomologyMap' _ _ _

Premises used: CategoryTheory.ShortComplex.homologyMap', CategoryTheory.ShortComplex.quasiIso_iff_isIso_leftHomologyMap'
-- Module: Mathlib.Algebra.Homology.ShortComplex.QuasiIso
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
φ : S₁ ⟶ S₂
inst_4 : Epi φ.τ₁
inst_5 : IsIso φ.τ₂
inst_6 : Mono φ.τ₃
rw :
  IsIso (X := S₁.leftHomologyData.H) (Y := (LeftHomologyData.ofEpiOfIsIsoOfMono φ S₁.leftHomologyData).H)
    (LeftHomologyMapData.φH (LeftHomologyMapData.ofEpiOfIsIsoOfMono φ S₁.leftHomologyData))
⊢ QuasiIso φ

Tactic:
rw [((LeftHomologyMapData.ofEpiOfIsIsoOfMono φ) S₁.leftHomologyData).quasiIso_iff]

Premises used: CategoryTheory.ShortComplex.leftHomologyData, CategoryTheory.ShortComplex.LeftHomologyMapData.ofEpiOfIsIsoOfMono, CategoryTheory.ShortComplex.LeftHomologyMapData.quasiIso_iff
-- Module: Mathlib.Algebra.Homology.ShortComplex.QuasiIso
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
φ : S₁ ⟶ S₂
inst_4 : Epi φ.τ₁
inst_5 : IsIso φ.τ₂
inst_6 : Mono φ.τ₃
dsimp : IsIso.{v_1, u_1} (𝟙 S₁.leftHomology)
⊢ IsIso (X := S₁.leftHomologyData.H) (Y := (LeftHomologyData.ofEpiOfIsIsoOfMono φ S₁.leftHomologyData).H)
    (LeftHomologyMapData.φH (LeftHomologyMapData.ofEpiOfIsIsoOfMono φ S₁.leftHomologyData))

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.ShortComplex.QuasiIso
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
φ : S₁ ⟶ S₂
inst_4 : Epi φ.τ₁
inst_5 : IsIso φ.τ₂
inst_6 : Mono φ.τ₃
⊢ IsIso.{v_1, u_1} (𝟙 S₁.leftHomology)

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.ShortComplex.QuasiIso
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
φ : S₁ ⟶ S₂
have : ∀ (γ : HomologyMapData φ S₁.homologyData S₂.homologyData), QuasiIso (opMap φ) ↔ QuasiIso φ
⊢ QuasiIso (opMap φ) ↔ QuasiIso φ

Tactic:
have γ : HomologyMapData φ S₁.homologyData S₂.homologyData := default
-- Module: Mathlib.Algebra.Homology.ShortComplex.QuasiIso
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
φ : S₁ ⟶ S₂
γ : HomologyMapData φ S₁.homologyData S₂.homologyData
rw : IsIso γ.op.right.φH ↔ IsIso γ.left.φH
⊢ QuasiIso (opMap φ) ↔ QuasiIso φ

Tactic:
rw [γ.left.quasiIso_iff, γ.op.right.quasiIso_iff]

Premises used: CategoryTheory.ShortComplex.HomologyMapData.right, CategoryTheory.ShortComplex.HomologyMapData.op, CategoryTheory.ShortComplex.HomologyMapData.left, CategoryTheory.ShortComplex.LeftHomologyMapData.quasiIso_iff, CategoryTheory.ShortComplex.RightHomologyMapData.quasiIso_iff
-- Module: Mathlib.Algebra.Homology.ShortComplex.QuasiIso
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
φ : S₁ ⟶ S₂
γ : HomologyMapData φ S₁.homologyData S₂.homologyData
mp :
  IsIso.{v_1, u_1} (C := Cᵒᵖ) (X := Opposite.op S₂.homologyData.left.H) (Y := Opposite.op S₁.homologyData.left.H)
      γ.left.φH.op →
    IsIso γ.left.φH
mpr :
  IsIso γ.left.φH →
    IsIso.{v_1, u_1} (C := Cᵒᵖ) (X := Opposite.op S₂.homologyData.left.H) (Y := Opposite.op S₁.homologyData.left.H)
      γ.left.φH.op
⊢ IsIso.{v_1, u_1} (C := Cᵒᵖ) (X := Opposite.op S₂.homologyData.left.H) (Y := Opposite.op S₁.homologyData.left.H)
      γ.left.φH.op ↔
    IsIso γ.left.φH

Tactic:
constructor
-- Module: Mathlib.Algebra.Homology.ShortComplex.QuasiIso
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
φ : S₁ ⟶ S₂
γ : HomologyMapData φ S₁.homologyData S₂.homologyData
h :
  IsIso.{v_1, u_1} (C := Cᵒᵖ) (X := Opposite.op S₂.homologyData.left.H) (Y := Opposite.op S₁.homologyData.left.H)
    γ.left.φH.op
⊢ IsIso γ.left.φH

Tactic:
apply isIso_of_op

Premises used: CategoryTheory.isIso_of_op
-- Module: Mathlib.Algebra.Homology.ShortComplex.QuasiIso
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
φ : S₁ ⟶ S₂
γ : HomologyMapData φ S₁.homologyData S₂.homologyData
h : IsIso γ.left.φH
⊢ IsIso.{v_1, u_1} (C := Cᵒᵖ) (X := Opposite.op S₂.homologyData.left.H) (Y := Opposite.op S₁.homologyData.left.H)
    γ.left.φH.op

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.ShortComplex.QuasiIso
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
φ : S₁ ⟶ S₂
inst_4 rw : QuasiIso φ
⊢ QuasiIso (opMap φ)

Tactic:
rw [quasiIso_opMap_iff]

Premises used: CategoryTheory.ShortComplex.quasiIso_opMap_iff
-- Module: Mathlib.Algebra.Homology.ShortComplex.QuasiIso
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
φ : S₁ ⟶ S₂
inst_4 : QuasiIso φ
⊢ QuasiIso φ

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.ShortComplex.QuasiIso
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} Cᵒᵖ
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
inst_4 : S₁.unop.HasHomology
inst_5 : S₂.unop.HasHomology
φ : S₁ ⟶ S₂
inst_6 : QuasiIso φ
rw : QuasiIso (opMap (unopMap φ))
⊢ QuasiIso (unopMap φ)

Tactic:
rw [← quasiIso_opMap_iff]

Premises used: CategoryTheory.ShortComplex.quasiIso_opMap_iff
-- Module: Mathlib.Algebra.Homology.ShortComplex.QuasiIso
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} Cᵒᵖ
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
inst_4 : S₁.unop.HasHomology
inst_5 : S₂.unop.HasHomology
φ : S₁ ⟶ S₂
inst_6 change : QuasiIso φ
⊢ QuasiIso (opMap (unopMap φ))

Tactic:
change QuasiIso φ

Premises used: CategoryTheory.ShortComplex.QuasiIso
-- Module: Mathlib.Algebra.Homology.ShortComplex.QuasiIso
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} Cᵒᵖ
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
inst_4 : S₁.unop.HasHomology
inst_5 : S₂.unop.HasHomology
φ : S₁ ⟶ S₂
inst_6 : QuasiIso φ
⊢ QuasiIso φ

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.ShortComplex.QuasiIso
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ S₂ S₃ S₄ : ShortComplex.{v_1, u_1} C
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
inst_4 : S₃.HasHomology
inst_5 : S₄.HasHomology
φ : S₁ ⟶ S₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
rw : S₁.g ≫ φ.τ₃ = 0
rw₁ : Eq (α := S₁.X₂ ⟶ S₂.X₃) (0 ≫ φ.τ₃) 0
rw₂ rw₃ : Eq.{v_1 + 1} (α := S₁.X₂ ⟶ S₂.X₃) 0 0
⊢ φ.τ₂ ≫ S₂.g = 0

Tactic:
rw [φ.comm₂₃, hg₁, zero_comp]

Premises used: CategoryTheory.ShortComplex.Hom.comm₂₃, CategoryTheory.Limits.zero_comp
-- Module: Mathlib.Algebra.Homology.ShortComplex.QuasiIso
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
φ : S₁ ⟶ S₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
rw : S₁.g ≫ φ.τ₃ = 0
rw₁ : Eq (α := S₁.X₂ ⟶ S₂.X₃) (0 ≫ φ.τ₃) 0
rw₂ rw₃ : Eq.{v_1 + 1} (α := S₁.X₂ ⟶ S₂.X₃) 0 0
⊢ φ.τ₂ ≫ S₂.g = 0

Tactic:
rw [φ.comm₂₃, hg₁, zero_comp]

Premises used: CategoryTheory.ShortComplex.Hom.comm₂₃, CategoryTheory.Limits.zero_comp
-- Module: Mathlib.Algebra.Homology.ShortComplex.QuasiIso
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
φ : S₁ ⟶ S₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
H : LeftHomologyMapData φ (LeftHomologyData.ofZeros S₁ hf₁ hg₁)
  (LeftHomologyData.ofIsLimitKernelFork S₂ hf₂ (KernelFork.ofι (Z := S₂.cycles) S₂.iCycles ⋯) S₂.cyclesIsKernel) :=
  { φK := S₂.liftCycles φ.τ₂ ⋯, φH := S₂.liftCycles φ.τ₂ ⋯, commi := ⋯, commf' := ⋯, commπ := ⋯ }
⊢ QuasiIso φ ↔ IsIso (Y := S₂.cycles) (S₂.liftCycles φ.τ₂ ⋯)

Tactic:
H.quasiIso_iff

Premises used: CategoryTheory.ShortComplex.LeftHomologyData.liftK, CategoryTheory.ShortComplex.liftCycles, CategoryTheory.ShortComplex.LeftHomologyMapData.quasiIso_iff, CategoryTheory.ShortComplex.cycles
-- Module: Mathlib.Algebra.Homology.ShortComplex.QuasiIso
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
φ : S₁ ⟶ S₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
H : LeftHomologyMapData φ (LeftHomologyData.ofZeros S₁ hf₁ hg₁)
  (LeftHomologyData.ofIsLimitKernelFork S₂ hf₂ (KernelFork.ofι (Z := S₂.cycles) S₂.iCycles ⋯) S₂.cyclesIsKernel) :=
  { φK := S₂.liftCycles φ.τ₂ ⋯, φH := S₂.liftCycles φ.τ₂ ⋯, commi := ⋯, commf' := ⋯, commπ := ⋯ }
⊢ QuasiIso φ ↔ IsIso (Y := S₂.cycles) (S₂.liftCycles φ.τ₂ ⋯)

Tactic:
exact H.quasiIso_iff

Premises used: CategoryTheory.ShortComplex.LeftHomologyMapData.quasiIso_iff
-- Module: Mathlib.Algebra.Homology.ShortComplex.QuasiIso
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ S₂ S₃ S₄ : ShortComplex.{v_1, u_1} C
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
inst_4 : S₃.HasHomology
inst_5 : S₄.HasHomology
φ : S₁ ⟶ S₂
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
hg₂ : S₂.g = 0
rw : φ.τ₁ ≫ S₂.f = 0
rw₁ : Eq (α := S₁.X₁ ⟶ S₂.X₂) (φ.τ₁ ≫ 0) 0
rw₂ rw₃ : Eq.{v_1 + 1} (α := S₁.X₁ ⟶ S₂.X₂) 0 0
⊢ S₁.f ≫ φ.τ₂ = 0

Tactic:
rw [← φ.comm₁₂, hf₂, comp_zero]

Premises used: CategoryTheory.ShortComplex.Hom.comm₁₂, CategoryTheory.Limits.comp_zero
-- Module: Mathlib.Algebra.Homology.ShortComplex.QuasiIso
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
φ : S₁ ⟶ S₂
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
hg₂ : S₂.g = 0
rw : φ.τ₁ ≫ S₂.f = 0
rw₁ : Eq (α := S₁.X₁ ⟶ S₂.X₂) (φ.τ₁ ≫ 0) 0
rw₂ rw₃ : Eq.{v_1 + 1} (α := S₁.X₁ ⟶ S₂.X₂) 0 0
⊢ S₁.f ≫ φ.τ₂ = 0

Tactic:
rw [← φ.comm₁₂, hf₂, comp_zero]

Premises used: CategoryTheory.ShortComplex.Hom.comm₁₂, CategoryTheory.Limits.comp_zero
-- Module: Mathlib.Algebra.Homology.ShortComplex.QuasiIso
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
φ : S₁ ⟶ S₂
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
hg₂ : S₂.g = 0
H : RightHomologyMapData φ
  (RightHomologyData.ofIsColimitCokernelCofork S₁ hg₁ (CokernelCofork.ofπ (Z := S₁.opcycles) S₁.pOpcycles ⋯)
    S₁.opcyclesIsCokernel)
  (RightHomologyData.ofZeros S₂ hf₂ hg₂) :=
  { φQ := S₁.descOpcycles φ.τ₂ ⋯, φH := S₁.descOpcycles φ.τ₂ ⋯, commp := ⋯, commg' := ⋯, commι := ⋯ }
⊢ QuasiIso φ ↔ IsIso (X := S₁.opcycles) (S₁.descOpcycles φ.τ₂ ⋯)

Tactic:
H.quasiIso_iff

Premises used: CategoryTheory.ShortComplex.opcycles, CategoryTheory.ShortComplex.descOpcycles, CategoryTheory.ShortComplex.RightHomologyData.descQ, CategoryTheory.ShortComplex.RightHomologyMapData.quasiIso_iff
-- Module: Mathlib.Algebra.Homology.ShortComplex.QuasiIso
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
φ : S₁ ⟶ S₂
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
hg₂ : S₂.g = 0
H : RightHomologyMapData φ
  (RightHomologyData.ofIsColimitCokernelCofork S₁ hg₁ (CokernelCofork.ofπ (Z := S₁.opcycles) S₁.pOpcycles ⋯)
    S₁.opcyclesIsCokernel)
  (RightHomologyData.ofZeros S₂ hf₂ hg₂) :=
  { φQ := S₁.descOpcycles φ.τ₂ ⋯, φH := S₁.descOpcycles φ.τ₂ ⋯, commp := ⋯, commg' := ⋯, commι := ⋯ }
⊢ QuasiIso φ ↔ IsIso (X := S₁.opcycles) (S₁.descOpcycles φ.τ₂ ⋯)

Tactic:
exact H.quasiIso_iff

Premises used: CategoryTheory.ShortComplex.RightHomologyMapData.quasiIso_iff
-- Module: Mathlib.Algebra.Homology.ShortComplex.Retract
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ T₁ S₂ T₂ : ShortComplex.{v_1, u_1} C
inst_2 : S₁.HasHomology
inst_3 : T₁.HasHomology
inst_4 : S₂.HasHomology
inst_5 : T₂.HasHomology
f₁ : S₁ ⟶ T₁
f₂ : S₂ ⟶ T₂
h : RetractArrow f₁ f₂
hf₂ : QuasiIso f₂
rw :
  ∀ (hf₂ : IsIso (X := S₂.homology) (Y := T₂.homology) (homologyMap f₂)),
    IsIso (X := S₁.homology) (Y := T₁.homology) (homologyMap f₁)
⊢ QuasiIso f₁

Tactic:
rw [quasiIso_iff] at hf₂ ⊢

Premises used: CategoryTheory.ShortComplex.quasiIso_iff
-- Module: Mathlib.Algebra.Homology.ShortComplex.Retract
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ T₁ S₂ T₂ : ShortComplex.{v_1, u_1} C
inst_2 : S₁.HasHomology
inst_3 : T₁.HasHomology
inst_4 : S₂.HasHomology
inst_5 : T₂.HasHomology
f₁ : S₁ ⟶ T₁
f₂ : S₂ ⟶ T₂
h : RetractArrow f₁ f₂
hf₂ : IsIso (X := S₂.homology) (Y := T₂.homology) (homologyMap f₂)
⊢ homologyMap
        (have this := Arrow.Hom.left h.i;
        this) ≫
      (Arrow.mk (X := S₂.homology) (Y := T₂.homology) (homologyMap f₂)).hom =
    (Arrow.mk (X := S₁.homology) (Y := T₁.homology) (homologyMap f₁)).hom ≫
      homologyMap
        (have this := Arrow.Hom.right h.i;
        this)

Tactic:
simp [← homologyMap_comp]

Premises used: CategoryTheory.ShortComplex.homologyMap_comp
-- Module: Mathlib.Algebra.Homology.ShortComplex.Retract
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ T₁ S₂ T₂ : ShortComplex.{v_1, u_1} C
inst_2 : S₁.HasHomology
inst_3 : T₁.HasHomology
inst_4 : S₂.HasHomology
inst_5 : T₂.HasHomology
f₁ : S₁ ⟶ T₁
f₂ : S₂ ⟶ T₂
h : RetractArrow f₁ f₂
hf₂ : IsIso (X := S₂.homology) (Y := T₂.homology) (homologyMap f₂)
⊢ homologyMap
        (have this := Arrow.Hom.left h.r;
        this) ≫
      (Arrow.mk (X := S₁.homology) (Y := T₁.homology) (homologyMap f₁)).hom =
    (Arrow.mk (X := S₂.homology) (Y := T₂.homology) (homologyMap f₂)).hom ≫
      homologyMap
        (have this := Arrow.Hom.right h.r;
        this)

Tactic:
simp [← homologyMap_comp]

Premises used: CategoryTheory.ShortComplex.homologyMap_comp
-- Module: Mathlib.Algebra.Homology.ShortComplex.Retract
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ T₁ S₂ T₂ : ShortComplex.{v_1, u_1} C
inst_2 : S₁.HasHomology
inst_3 : T₁.HasHomology
inst_4 : S₂.HasHomology
inst_5 : T₂.HasHomology
f₁ : S₁ ⟶ T₁
f₂ : S₂ ⟶ T₂
h : RetractArrow f₁ f₂
hf₂ : IsIso (X := S₂.homology) (Y := T₂.homology) (homologyMap f₂)
h₁ :
  Arrow.Hom.left
      (CategoryStruct.comp (Y := Arrow.mk (X := S₂.homology) (Y := T₂.homology) (homologyMap f₂))
        (Arrow.homMk
          (homologyMap
            (have this := Arrow.Hom.left h.i;
            this))
          (homologyMap
            (have this := Arrow.Hom.right h.i;
            this))
          ⋯)
        (Arrow.homMk
          (homologyMap
            (have this := Arrow.Hom.left h.r;
            this))
          (homologyMap
            (have this := Arrow.Hom.right h.r;
            this))
          ⋯)) =
    Arrow.Hom.left (𝟙 (Arrow.mk (X := S₁.homology) (Y := T₁.homology) (homologyMap f₁)))
h₂ :
  Arrow.Hom.right
      (CategoryStruct.comp (Y := Arrow.mk (X := S₂.homology) (Y := T₂.homology) (homologyMap f₂))
        (Arrow.homMk
          (homologyMap
            (have this := Arrow.Hom.left h.i;
            this))
          (homologyMap
            (have this := Arrow.Hom.right h.i;
            this))
          ⋯)
        (Arrow.homMk
          (homologyMap
            (have this := Arrow.Hom.left h.r;
            this))
          (homologyMap
            (have this := Arrow.Hom.right h.r;
            this))
          ⋯)) =
    Arrow.Hom.right (𝟙 (Arrow.mk (X := S₁.homology) (Y := T₁.homology) (homologyMap f₁)))
⊢ CategoryStruct.comp (Y := Arrow.mk (X := S₂.homology) (Y := T₂.homology) (homologyMap f₂))
      (Arrow.homMk
        (homologyMap
          (have this := Arrow.Hom.left h.i;
          this))
        (homologyMap
          (have this := Arrow.Hom.right h.i;
          this))
        ⋯)
      (Arrow.homMk
        (homologyMap
          (have this := Arrow.Hom.left h.r;
          this))
        (homologyMap
          (have this := Arrow.Hom.right h.r;
          this))
        ⋯) =
    𝟙 (Arrow.mk (X := S₁.homology) (Y := T₁.homology) (homologyMap f₁))

Tactic:
ext
-- Module: Mathlib.Algebra.Homology.ShortComplex.Retract
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ T₁ S₂ T₂ : ShortComplex.{v_1, u_1} C
inst_2 : S₁.HasHomology
inst_3 : T₁.HasHomology
inst_4 : S₂.HasHomology
inst_5 : T₂.HasHomology
f₁ : S₁ ⟶ T₁
f₂ : S₂ ⟶ T₂
h : RetractArrow f₁ f₂
hf₂ : IsIso (X := S₂.homology) (Y := T₂.homology) (homologyMap f₂)
⊢ Arrow.Hom.left
      (CategoryStruct.comp (Y := Arrow.mk (X := S₂.homology) (Y := T₂.homology) (homologyMap f₂))
        (Arrow.homMk
          (homologyMap
            (have this := Arrow.Hom.left h.i;
            this))
          (homologyMap
            (have this := Arrow.Hom.right h.i;
            this))
          ⋯)
        (Arrow.homMk
          (homologyMap
            (have this := Arrow.Hom.left h.r;
            this))
          (homologyMap
            (have this := Arrow.Hom.right h.r;
            this))
          ⋯)) =
    Arrow.Hom.left (𝟙 (Arrow.mk (X := S₁.homology) (Y := T₁.homology) (homologyMap f₁)))

Tactic:
simp [← homologyMap_comp]

Premises used: CategoryTheory.ShortComplex.homologyMap_comp
-- Module: Mathlib.Algebra.Homology.ShortComplex.Retract
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ T₁ S₂ T₂ : ShortComplex.{v_1, u_1} C
inst_2 : S₁.HasHomology
inst_3 : T₁.HasHomology
inst_4 : S₂.HasHomology
inst_5 : T₂.HasHomology
f₁ : S₁ ⟶ T₁
f₂ : S₂ ⟶ T₂
h : RetractArrow f₁ f₂
hf₂ : IsIso (X := S₂.homology) (Y := T₂.homology) (homologyMap f₂)
⊢ Arrow.Hom.right
      (CategoryStruct.comp (Y := Arrow.mk (X := S₂.homology) (Y := T₂.homology) (homologyMap f₂))
        (Arrow.homMk
          (homologyMap
            (have this := Arrow.Hom.left h.i;
            this))
          (homologyMap
            (have this := Arrow.Hom.right h.i;
            this))
          ⋯)
        (Arrow.homMk
          (homologyMap
            (have this := Arrow.Hom.left h.r;
            this))
          (homologyMap
            (have this := Arrow.Hom.right h.r;
            this))
          ⋯)) =
    Arrow.Hom.right (𝟙 (Arrow.mk (X := S₁.homology) (Y := T₁.homology) (homologyMap f₁)))

Tactic:
simp [← homologyMap_comp]

Premises used: CategoryTheory.ShortComplex.homologyMap_comp
-- Module: Mathlib.Algebra.Homology.ShortComplex.Retract
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ T₁ S₂ T₂ : ShortComplex.{v_1, u_1} C
inst_2 : S₁.HasHomology
inst_3 : T₁.HasHomology
inst_4 : S₂.HasHomology
inst_5 : T₂.HasHomology
f₁ : S₁ ⟶ T₁
f₂ : S₂ ⟶ T₂
h : RetractArrow f₁ f₂
hf₂ : IsIso (X := S₂.homology) (Y := T₂.homology) (homologyMap f₂)
have :
  ∀
    (h :
      RetractArrow (X := S₁.homology) (Y := T₁.homology) (Z := S₂.homology) (W := T₂.homology) (homologyMap f₁)
        (homologyMap f₂)),
    IsIso (X := S₁.homology) (Y := T₁.homology) (homologyMap f₁)
⊢ IsIso (X := S₁.homology) (Y := T₁.homology) (homologyMap f₁)

Tactic:
have h : RetractArrow (homologyMap f₁) (homologyMap f₂) :=
    { i := Arrow.homMk (u := homologyMap (show S₁ ⟶ S₂ from h.i.left))
        (v := homologyMap (show T₁ ⟶ T₂ from h.i.right)) (by simp [← homologyMap_comp])
      r := Arrow.homMk (u := homologyMap (show S₂ ⟶ S₁ from h.r.left))
        (v := homologyMap (show T₂ ⟶ T₁ from h.r.right)) (by simp [← homologyMap_comp])
      retract := by ext <;> simp [← homologyMap_comp] }
-- Module: Mathlib.Algebra.Homology.ShortComplex.Retract
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ T₁ S₂ T₂ : ShortComplex.{v_1, u_1} C
inst_2 : S₁.HasHomology
inst_3 : T₁.HasHomology
inst_4 : S₂.HasHomology
inst_5 : T₂.HasHomology
f₁ : S₁ ⟶ T₁
f₂ : S₂ ⟶ T₂
h_1 : RetractArrow f₁ f₂
hf₂ : IsIso (X := S₂.homology) (Y := T₂.homology) (homologyMap f₂)
h :
  RetractArrow (X := S₁.homology) (Y := T₁.homology) (Z := S₂.homology) (W := T₂.homology) (homologyMap f₁)
    (homologyMap f₂)
⊢ IsIso (X := S₁.homology) (Y := T₁.homology) (homologyMap f₁)

Tactic:
(MorphismProperty.isomorphisms C).of_retract h hf₂

Premises used: CategoryTheory.MorphismProperty.of_retract
-- Module: Mathlib.Algebra.Homology.ShortComplex.Retract
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ T₁ S₂ T₂ : ShortComplex.{v_1, u_1} C
inst_2 : S₁.HasHomology
inst_3 : T₁.HasHomology
inst_4 : S₂.HasHomology
inst_5 : T₂.HasHomology
f₁ : S₁ ⟶ T₁
f₂ : S₂ ⟶ T₂
h_1 : RetractArrow f₁ f₂
hf₂ : IsIso (X := S₂.homology) (Y := T₂.homology) (homologyMap f₂)
h :
  RetractArrow (X := S₁.homology) (Y := T₁.homology) (Z := S₂.homology) (W := T₂.homology) (homologyMap f₁)
    (homologyMap f₂)
⊢ IsIso (X := S₁.homology) (Y := T₁.homology) (homologyMap f₁)

Tactic:
exact (MorphismProperty.isomorphisms C).of_retract h hf₂

Premises used: CategoryTheory.MorphismProperty.of_retract
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
h : S.RightHomologyData
A : C
⊢ Epi h.p

Tactic:
⟨fun _ _ => Cofork.IsColimit.hom_ext h.hp⟩

Premises used: CategoryTheory.Limits.Cofork.IsColimit.hom_ext, CategoryTheory.ShortComplex.RightHomologyData.hp, CategoryTheory.Epi.mk
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
h : S.RightHomologyData
A : C
⊢ Mono h.ι

Tactic:
⟨fun _ _ => Fork.IsLimit.hom_ext h.hι⟩

Premises used: CategoryTheory.ShortComplex.RightHomologyData.hι, CategoryTheory.Limits.Fork.IsLimit.hom_ext, CategoryTheory.Mono.mk