-- Mathlib/Algebra/Homology/HomologySequence.lean
/-- If `0 ⟶ X₁ ⟶ X₂ ⟶ X₃` is an exact sequence of homological complex, then
`0 ⟶ X₁.cycles i ⟶ X₂.cycles i ⟶ X₃.cycles i` is exact. This lemma states
the exactness at `X₂.cycles i`, while the fact that `X₁.cycles i ⟶ X₂.cycles i`
is a mono is an instance. -/
lemma cycles_left_exact (S : ShortComplex (HomologicalComplex C c)) (hS : S.Exact) [Mono S.f]
    (i : ι) [S.X₁.HasHomology i] [S.X₂.HasHomology i] [S.X₃.HasHomology i] :
    (ShortComplex.mk (cyclesMap S.f i) (cyclesMap S.g i)
      (by rw [← cyclesMap_comp, S.zero, cyclesMap_zero])).Exact

Proof state:
C : Type u_1
ι : Type u_2
inst✝⁵ : Category.{u_3, u_1} C
inst✝⁴ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.Exact
inst✝³ : Mono S.f
i : ι
inst✝² : S.X₁.HasHomology i
inst✝¹ : S.X₂.HasHomology i
inst✝ : S.X₃.HasHomology i
this : Mono (S.map (eval C c i)).f
hi : IsLimit (KernelFork.ofι (S.map (eval C c i)).f ⋯)
A : C
k : A ⟶ (ShortComplex.mk (cyclesMap S.f i) (cyclesMap S.g i) ⋯).X₂
hk : k ≫ (ShortComplex.mk (cyclesMap S.f i) (cyclesMap S.g i) ⋯).g = 0
⊢ { l // l ≫ (ShortComplex.mk (cyclesMap S.f i) (cyclesMap S.g i) ⋯).f = k }

Tactic:
dsimp at k hk ⊢

Result:
C : Type u_1
ι : Type u_2
inst✝⁵ : Category.{u_3, u_1} C
inst✝⁴ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.Exact
inst✝³ : Mono S.f
i : ι
inst✝² : S.X₁.HasHomology i
inst✝¹ : S.X₂.HasHomology i
inst✝ : S.X₃.HasHomology i
this : Mono (S.map (eval C c i)).f
hi : IsLimit (KernelFork.ofι (S.map (eval C c i)).f ⋯)
A : C
k : A ⟶ S.X₂.cycles i
hk : k ≫ cyclesMap S.g i = 0
⊢ { l // l ≫ cyclesMap S.f i = k }

Proof state:
C : Type u_1
ι : Type u_2
inst✝⁵ : Category.{?u.67787, u_1} C
inst✝⁴ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.Exact
inst✝³ : Mono S.f
i : ι
inst✝² : S.X₁.HasHomology i
inst✝¹ : S.X₂.HasHomology i
inst✝ : S.X₃.HasHomology i
⊢ cyclesMap S.f i ≫ cyclesMap S.g i = 0

Tactic:
rw [← cyclesMap_comp, S.zero, cyclesMap_zero]

Result:
no goals

Proof state:
C : Type u_1
ι : Type u_2
inst✝⁵ : Category.{u_3, u_1} C
inst✝⁴ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.Exact
inst✝³ : Mono S.f
i : ι
inst✝² : S.X₁.HasHomology i
inst✝¹ : S.X₂.HasHomology i
inst✝ : S.X₃.HasHomology i
⊢ (ShortComplex.mk (cyclesMap S.f i) (cyclesMap S.g i) ⋯).Exact

Tactic:
have : Mono (ShortComplex.map S (eval C c i)).f := by dsimp; infer_instance

Result:
C : Type u_1
ι : Type u_2
inst✝⁵ : Category.{u_3, u_1} C
inst✝⁴ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.Exact
inst✝³ : Mono S.f
i : ι
inst✝² : S.X₁.HasHomology i
inst✝¹ : S.X₂.HasHomology i
inst✝ : S.X₃.HasHomology i
this : Mono (S.map (eval C c i)).f
⊢ (ShortComplex.mk (cyclesMap S.f i) (cyclesMap S.g i) ⋯).Exact

Proof state:
C : Type u_1
ι : Type u_2
inst✝⁵ : Category.{u_3, u_1} C
inst✝⁴ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.Exact
inst✝³ : Mono S.f
i : ι
inst✝² : S.X₁.HasHomology i
inst✝¹ : S.X₂.HasHomology i
inst✝ : S.X₃.HasHomology i
⊢ Mono (S.map (eval C c i)).f

Tactic:
dsimp

Result:
C : Type u_1
ι : Type u_2
inst✝⁵ : Category.{u_3, u_1} C
inst✝⁴ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.Exact
inst✝³ : Mono S.f
i : ι
inst✝² : S.X₁.HasHomology i
inst✝¹ : S.X₂.HasHomology i
inst✝ : S.X₃.HasHomology i
⊢ Mono (S.f.f i)

Proof state:
C : Type u_1
ι : Type u_2
inst✝⁵ : Category.{u_3, u_1} C
inst✝⁴ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.Exact
inst✝³ : Mono S.f
i : ι
inst✝² : S.X₁.HasHomology i
inst✝¹ : S.X₂.HasHomology i
inst✝ : S.X₃.HasHomology i
this : Mono (S.map (eval C c i)).f
hi : IsLimit (KernelFork.ofι (S.map (eval C c i)).f ⋯)
A : C
k : A ⟶ S.X₂.cycles i
hk : k ≫ cyclesMap S.g i = 0
⊢ (k ≫ S.X₂.iCycles i) ≫ (S.map (eval C c i)).g = 0

Tactic:
dsimp

Result:
C : Type u_1
ι : Type u_2
inst✝⁵ : Category.{u_3, u_1} C
inst✝⁴ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.Exact
inst✝³ : Mono S.f
i : ι
inst✝² : S.X₁.HasHomology i
inst✝¹ : S.X₂.HasHomology i
inst✝ : S.X₃.HasHomology i
this : Mono (S.map (eval C c i)).f
hi : IsLimit (KernelFork.ofι (S.map (eval C c i)).f ⋯)
A : C
k : A ⟶ S.X₂.cycles i
hk : k ≫ cyclesMap S.g i = 0
⊢ (k ≫ S.X₂.iCycles i) ≫ S.g.f i = 0

Proof state:
C : Type u_1
ι : Type u_2
inst✝⁵ : Category.{u_3, u_1} C
inst✝⁴ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.Exact
inst✝³ : Mono S.f
i : ι
inst✝² : S.X₁.HasHomology i
inst✝¹ : S.X₂.HasHomology i
inst✝ : S.X₃.HasHomology i
⊢ Mono (S.f.f i)

Tactic:
infer_instance

Result:
no goals

Proof state:
C : Type u_1
ι : Type u_2
inst✝⁵ : Category.{u_3, u_1} C
inst✝⁴ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.Exact
inst✝³ : Mono S.f
i : ι
inst✝² : S.X₁.HasHomology i
inst✝¹ : S.X₂.HasHomology i
inst✝ : S.X₃.HasHomology i
this : Mono (S.map (eval C c i)).f
hi : IsLimit (KernelFork.ofι (S.map (eval C c i)).f ⋯)
A : C
k : A ⟶ S.X₂.cycles i
hk : k ≫ cyclesMap S.g i = 0
⊢ { l // l ≫ cyclesMap S.f i = k }

Tactic:
have H := KernelFork.IsLimit.lift' hi (k ≫ S.X₂.iCycles i) (by
  dsimp
  rw [assoc, ← cyclesMap_i, reassoc_of% hk, zero_comp])

Result:
C : Type u_1
ι : Type u_2
inst✝⁵ : Category.{u_3, u_1} C
inst✝⁴ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.Exact
inst✝³ : Mono S.f
i : ι
inst✝² : S.X₁.HasHomology i
inst✝¹ : S.X₂.HasHomology i
inst✝ : S.X₃.HasHomology i
this : Mono (S.map (eval C c i)).f
hi : IsLimit (KernelFork.ofι (S.map (eval C c i)).f ⋯)
A : C
k : A ⟶ S.X₂.cycles i
hk : k ≫ cyclesMap S.g i = 0
H : { l // l ≫ Fork.ι (KernelFork.ofι (S.map (eval C c i)).f ⋯) = k ≫ S.X₂.iCycles i }
⊢ { l // l ≫ cyclesMap S.f i = k }

Proof state:
C : Type u_1
ι : Type u_2
inst✝⁵ : Category.{u_3, u_1} C
inst✝⁴ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.Exact
inst✝³ : Mono S.f
i : ι
inst✝² : S.X₁.HasHomology i
inst✝¹ : S.X₂.HasHomology i
inst✝ : S.X₃.HasHomology i
this : Mono (S.map (eval C c i)).f
hi : IsLimit (KernelFork.ofι (S.map (eval C c i)).f ⋯)
A : C
k : A ⟶ S.X₂.cycles i
hk : k ≫ cyclesMap S.g i = 0
H : { l // l ≫ S.f.f i = k ≫ S.X₂.iCycles i }
⊢ { l // l ≫ cyclesMap S.f i = k }

Tactic:
refine ⟨S.X₁.liftCycles H.1 _ rfl ?_, ?_⟩

Result:
case refine_1
C : Type u_1
ι : Type u_2
inst✝⁵ : Category.{u_3, u_1} C
inst✝⁴ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.Exact
inst✝³ : Mono S.f
i : ι
inst✝² : S.X₁.HasHomology i
inst✝¹ : S.X₂.HasHomology i
inst✝ : S.X₃.HasHomology i
this : Mono (S.map (eval C c i)).f
hi : IsLimit (KernelFork.ofι (S.map (eval C c i)).f ⋯)
A : C
k : A ⟶ S.X₂.cycles i
hk : k ≫ cyclesMap S.g i = 0
H : { l // l ≫ S.f.f i = k ≫ S.X₂.iCycles i }
⊢ ↑H ≫ S.X₁.d i (c.next i) = 0

case refine_2
C : Type u_1
ι : Type u_2
inst✝⁵ : Category.{u_3, u_1} C
inst✝⁴ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.Exact
inst✝³ : Mono S.f
i : ι
inst✝² : S.X₁.HasHomology i
inst✝¹ : S.X₂.HasHomology i
inst✝ : S.X₃.HasHomology i
this : Mono (S.map (eval C c i)).f
hi : IsLimit (KernelFork.ofι (S.map (eval C c i)).f ⋯)
A : C
k : A ⟶ S.X₂.cycles i
hk : k ≫ cyclesMap S.g i = 0
H : { l // l ≫ S.f.f i = k ≫ S.X₂.iCycles i }
⊢ S.X₁.liftCycles (↑H) (c.next i) ⋯ ?refine_1 ≫ cyclesMap S.f i = k