-- Mathlib/Algebra/Homology/Embedding/TruncGEHomology.lean
lemma quasiIso_truncGEMap_iff :
    QuasiIso (truncGEMap φ e) ↔ ∀ (i : ι) (i' : ι') (_ : e.f i = i'), QuasiIsoAt φ i'

Proof state:
case mpr
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁵ : Category.{u_4, u_3} C
inst✝⁴ : HasZeroMorphisms C
K L : HomologicalComplex C c'
φ : K ⟶ L
e : c.Embedding c'
inst✝³ : e.IsTruncGE
inst✝² : ∀ (i' : ι'), K.HasHomology i'
inst✝¹ : ∀ (i' : ι'), L.HasHomology i'
inst✝ : HasZeroObject C
this : ∀ (i : ι) (i' : ι'), e.f i = i' → (QuasiIsoAt (truncGEMap φ e) i' ↔ QuasiIsoAt φ i')
h : ∀ (i : ι) (i' : ι'), e.f i = i' → QuasiIsoAt φ i'
i' : ι'
⊢ QuasiIsoAt (truncGEMap φ e) i'

Tactic:
by_cases hi' : ∃ i, e.f i = i'

Result:
case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁵ : Category.{u_4, u_3} C
inst✝⁴ : HasZeroMorphisms C
K L : HomologicalComplex C c'
φ : K ⟶ L
e : c.Embedding c'
inst✝³ : e.IsTruncGE
inst✝² : ∀ (i' : ι'), K.HasHomology i'
inst✝¹ : ∀ (i' : ι'), L.HasHomology i'
inst✝ : HasZeroObject C
this : ∀ (i : ι) (i' : ι'), e.f i = i' → (QuasiIsoAt (truncGEMap φ e) i' ↔ QuasiIsoAt φ i')
h : ∀ (i : ι) (i' : ι'), e.f i = i' → QuasiIsoAt φ i'
i' : ι'
hi' : ∃ i, e.f i = i'
⊢ QuasiIsoAt (truncGEMap φ e) i'

case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁵ : Category.{u_4, u_3} C
inst✝⁴ : HasZeroMorphisms C
K L : HomologicalComplex C c'
φ : K ⟶ L
e : c.Embedding c'
inst✝³ : e.IsTruncGE
inst✝² : ∀ (i' : ι'), K.HasHomology i'
inst✝¹ : ∀ (i' : ι'), L.HasHomology i'
inst✝ : HasZeroObject C
this : ∀ (i : ι) (i' : ι'), e.f i = i' → (QuasiIsoAt (truncGEMap φ e) i' ↔ QuasiIsoAt φ i')
h : ∀ (i : ι) (i' : ι'), e.f i = i' → QuasiIsoAt φ i'
i' : ι'
hi' : ¬∃ i, e.f i = i'
⊢ QuasiIsoAt (truncGEMap φ e) i'

Proof state:
case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁵ : Category.{u_4, u_3} C
inst✝⁴ : HasZeroMorphisms C
K L : HomologicalComplex C c'
φ : K ⟶ L
e : c.Embedding c'
inst✝³ : e.IsTruncGE
inst✝² : ∀ (i' : ι'), K.HasHomology i'
inst✝¹ : ∀ (i' : ι'), L.HasHomology i'
inst✝ : HasZeroObject C
this : ∀ (i : ι) (i' : ι'), e.f i = i' → (QuasiIsoAt (truncGEMap φ e) i' ↔ QuasiIsoAt φ i')
h : ∀ (i : ι) (i' : ι'), e.f i = i' → QuasiIsoAt φ i'
i' : ι'
hi' : ∃ i, e.f i = i'
⊢ QuasiIsoAt (truncGEMap φ e) i'

Tactic:
obtain ⟨i, hi⟩ := hi'

Result:
case pos.intro
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁵ : Category.{u_4, u_3} C
inst✝⁴ : HasZeroMorphisms C
K L : HomologicalComplex C c'
φ : K ⟶ L
e : c.Embedding c'
inst✝³ : e.IsTruncGE
inst✝² : ∀ (i' : ι'), K.HasHomology i'
inst✝¹ : ∀ (i' : ι'), L.HasHomology i'
inst✝ : HasZeroObject C
this : ∀ (i : ι) (i' : ι'), e.f i = i' → (QuasiIsoAt (truncGEMap φ e) i' ↔ QuasiIsoAt φ i')
h : ∀ (i : ι) (i' : ι'), e.f i = i' → QuasiIsoAt φ i'
i' : ι'
i : ι
hi : e.f i = i'
⊢ QuasiIsoAt (truncGEMap φ e) i'

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁵ : Category.{u_4, u_3} C
inst✝⁴ : HasZeroMorphisms C
K L : HomologicalComplex C c'
φ : K ⟶ L
e : c.Embedding c'
inst✝³ : e.IsTruncGE
inst✝² : ∀ (i' : ι'), K.HasHomology i'
inst✝¹ : ∀ (i' : ι'), L.HasHomology i'
inst✝ : HasZeroObject C
i : ι
⊢ QuasiIsoAt (truncGEMap φ e) (e.f i) ↔ QuasiIsoAt φ (e.f i)

Tactic:
rw [← quasiIsoAt_iff_comp_left (K.πTruncGE e), πTruncGE_naturality φ e,
  quasiIsoAt_iff_comp_right]

Result:
no goals

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁵ : Category.{u_4, u_3} C
inst✝⁴ : HasZeroMorphisms C
K L : HomologicalComplex C c'
φ : K ⟶ L
e : c.Embedding c'
inst✝³ : e.IsTruncGE
inst✝² : ∀ (i' : ι'), K.HasHomology i'
inst✝¹ : ∀ (i' : ι'), L.HasHomology i'
inst✝ : HasZeroObject C
this : ∀ (i : ι) (i' : ι'), e.f i = i' → (QuasiIsoAt (truncGEMap φ e) i' ↔ QuasiIsoAt φ i')
⊢ QuasiIso (truncGEMap φ e) ↔ ∀ (i : ι) (i' : ι'), e.f i = i' → QuasiIsoAt φ i'

Tactic:
rw [quasiIso_iff]

Result:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁵ : Category.{u_4, u_3} C
inst✝⁴ : HasZeroMorphisms C
K L : HomologicalComplex C c'
φ : K ⟶ L
e : c.Embedding c'
inst✝³ : e.IsTruncGE
inst✝² : ∀ (i' : ι'), K.HasHomology i'
inst✝¹ : ∀ (i' : ι'), L.HasHomology i'
inst✝ : HasZeroObject C
this : ∀ (i : ι) (i' : ι'), e.f i = i' → (QuasiIsoAt (truncGEMap φ e) i' ↔ QuasiIsoAt φ i')
⊢ (∀ (i : ι'), QuasiIsoAt (truncGEMap φ e) i) ↔ ∀ (i : ι) (i' : ι'), e.f i = i' → QuasiIsoAt φ i'

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁵ : Category.{u_4, u_3} C
inst✝⁴ : HasZeroMorphisms C
K L : HomologicalComplex C c'
φ : K ⟶ L
e : c.Embedding c'
inst✝³ : e.IsTruncGE
inst✝² : ∀ (i' : ι'), K.HasHomology i'
inst✝¹ : ∀ (i' : ι'), L.HasHomology i'
inst✝ : HasZeroObject C
this : ∀ (i : ι) (i' : ι'), e.f i = i' → (QuasiIsoAt (truncGEMap φ e) i' ↔ QuasiIsoAt φ i')
h : ∀ (i : ι) (i' : ι'), e.f i = i' → QuasiIsoAt φ i'
i' : ι'
hi' : ¬∃ i, e.f i = i'
⊢ ∀ (i : ι), e.f i ≠ i'

Tactic:
simpa using hi'

Result:
no goals

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁵ : Category.{u_4, u_3} C
inst✝⁴ : HasZeroMorphisms C
K L : HomologicalComplex C c'
φ : K ⟶ L
e : c.Embedding c'
inst✝³ : e.IsTruncGE
inst✝² : ∀ (i' : ι'), K.HasHomology i'
inst✝¹ : ∀ (i' : ι'), L.HasHomology i'
inst✝ : HasZeroObject C
⊢ QuasiIso (truncGEMap φ e) ↔ ∀ (i : ι) (i' : ι'), e.f i = i' → QuasiIsoAt φ i'

Tactic:
have : ∀ (i : ι) (i' : ι') (_ : e.f i = i'),
    QuasiIsoAt (truncGEMap φ e) i' ↔ QuasiIsoAt φ i' := by
  rintro i _ rfl
  rw [← quasiIsoAt_iff_comp_left (K.πTruncGE e), πTruncGE_naturality φ e,
    quasiIsoAt_iff_comp_right]

Result:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁵ : Category.{u_4, u_3} C
inst✝⁴ : HasZeroMorphisms C
K L : HomologicalComplex C c'
φ : K ⟶ L
e : c.Embedding c'
inst✝³ : e.IsTruncGE
inst✝² : ∀ (i' : ι'), K.HasHomology i'
inst✝¹ : ∀ (i' : ι'), L.HasHomology i'
inst✝ : HasZeroObject C
this : ∀ (i : ι) (i' : ι'), e.f i = i' → (QuasiIsoAt (truncGEMap φ e) i' ↔ QuasiIsoAt φ i')
⊢ QuasiIso (truncGEMap φ e) ↔ ∀ (i : ι) (i' : ι'), e.f i = i' → QuasiIsoAt φ i'

Proof state:
case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁵ : Category.{u_4, u_3} C
inst✝⁴ : HasZeroMorphisms C
K L : HomologicalComplex C c'
φ : K ⟶ L
e : c.Embedding c'
inst✝³ : e.IsTruncGE
inst✝² : ∀ (i' : ι'), K.HasHomology i'
inst✝¹ : ∀ (i' : ι'), L.HasHomology i'
inst✝ : HasZeroObject C
this : ∀ (i : ι) (i' : ι'), e.f i = i' → (QuasiIsoAt (truncGEMap φ e) i' ↔ QuasiIsoAt φ i')
h : ∀ (i : ι) (i' : ι'), e.f i = i' → QuasiIsoAt φ i'
i' : ι'
hi' : ¬∃ i, e.f i = i'
⊢ (L.truncGE e).ExactAt i'

case neg.hK
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁵ : Category.{u_4, u_3} C
inst✝⁴ : HasZeroMorphisms C
K L : HomologicalComplex C c'
φ : K ⟶ L
e : c.Embedding c'
inst✝³ : e.IsTruncGE
inst✝² : ∀ (i' : ι'), K.HasHomology i'
inst✝¹ : ∀ (i' : ι'), L.HasHomology i'
inst✝ : HasZeroObject C
this : ∀ (i : ι) (i' : ι'), e.f i = i' → (QuasiIsoAt (truncGEMap φ e) i' ↔ QuasiIsoAt φ i')
h : ∀ (i : ι) (i' : ι'), e.f i = i' → QuasiIsoAt φ i'
i' : ι'
hi' : ¬∃ i, e.f i = i'
⊢ (K.truncGE e).ExactAt i'

Tactic:
all_goals exact exactAt_of_isSupported _ e i' (by simpa using hi')

Result:
no goals