-- Mathlib/Algebra/Homology/Embedding/IsSupported.lean
lemma isZero_iff_isStrictlySupported_and_isStrictlySupportedOutside :
    IsZero K ↔ K.IsStrictlySupported e ∧ K.IsStrictlySupportedOutside e

Proof state:
case mp
ι : 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 : HomologicalComplex C c'
e : c.Embedding c'
hK : IsZero K
⊢ K.IsStrictlySupported e ∧ K.IsStrictlySupportedOutside e

Tactic:
constructor

Result:
case mp.left
ι : 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 : HomologicalComplex C c'
e : c.Embedding c'
hK : IsZero K
⊢ K.IsStrictlySupported e

case mp.right
ι : 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 : HomologicalComplex C c'
e : c.Embedding c'
hK : IsZero K
⊢ K.IsStrictlySupportedOutside e

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 : HomologicalComplex C c'
e : c.Embedding c'
⊢ K.IsStrictlySupported e ∧ K.IsStrictlySupportedOutside e → IsZero K

Tactic:
rintro ⟨h₁, h₂⟩

Result:
case mpr.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 : HomologicalComplex C c'
e : c.Embedding c'
h₁ : K.IsStrictlySupported e
h₂ : K.IsStrictlySupportedOutside e
⊢ IsZero K

Proof state:
case mp.right
ι : 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 : HomologicalComplex C c'
e : c.Embedding c'
hK : IsZero K
⊢ K.IsStrictlySupportedOutside e

Tactic:
constructor

Result:
case mp.right.isZero
ι : 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 : HomologicalComplex C c'
e : c.Embedding c'
hK : IsZero K
⊢ ∀ (i : ι), IsZero (K.X (e.f i))

Proof state:
case mpr.intro.h.hX
ι : 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 : HomologicalComplex C c'
e : c.Embedding c'
h₁ : K.IsStrictlySupported e
h₂ : K.IsStrictlySupportedOutside e
n : ι'
⊢ IsZero (K.X n)

Tactic:
by_cases hn : ∃ i, e.f i = n

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 : HomologicalComplex C c'
e : c.Embedding c'
h₁ : K.IsStrictlySupported e
h₂ : K.IsStrictlySupportedOutside e
n : ι'
hn : ∃ i, e.f i = n
⊢ IsZero (K.X n)

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 : HomologicalComplex C c'
e : c.Embedding c'
h₁ : K.IsStrictlySupported e
h₂ : K.IsStrictlySupportedOutside e
n : ι'
hn : ¬∃ i, e.f i = n
⊢ IsZero (K.X n)

Proof state:
case mp.right.isZero
ι : 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 : HomologicalComplex C c'
e : c.Embedding c'
hK : IsZero K
⊢ ∀ (i : ι), IsZero (K.X (e.f i))

Tactic:
intros

Result:
case mp.right.isZero
ι : 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 : HomologicalComplex C c'
e : c.Embedding c'
hK : IsZero K
i✝ : ι
⊢ IsZero (K.X (e.f i✝))

Proof state:
case mpr.intro.h
ι : 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 : HomologicalComplex C c'
e : c.Embedding c'
h₁ : K.IsStrictlySupported e
h₂ : K.IsStrictlySupportedOutside e
n : ι'
⊢ (𝟙 K).f n = Hom.f 0 n

Tactic:
apply IsZero.eq_of_src

Result:
case mpr.intro.h.hX
ι : 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 : HomologicalComplex C c'
e : c.Embedding c'
h₁ : K.IsStrictlySupported e
h₂ : K.IsStrictlySupportedOutside e
n : ι'
⊢ IsZero (K.X n)

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 : HomologicalComplex C c'
e : c.Embedding c'
h₁ : K.IsStrictlySupported e
h₂ : K.IsStrictlySupportedOutside e
n : ι'
hn : ∃ i, e.f i = n
⊢ IsZero (K.X n)

Tactic:
obtain ⟨i, rfl⟩ := hn

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 : HomologicalComplex C c'
e : c.Embedding c'
h₁ : K.IsStrictlySupported e
h₂ : K.IsStrictlySupportedOutside e
i : ι
⊢ IsZero (K.X (e.f 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 : HomologicalComplex C c'
e : c.Embedding c'
⊢ IsZero K ↔ K.IsStrictlySupported e ∧ K.IsStrictlySupportedOutside e

Tactic:
constructor

Result:
case mp
ι : 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 : HomologicalComplex C c'
e : c.Embedding c'
⊢ IsZero K → K.IsStrictlySupported e ∧ K.IsStrictlySupportedOutside e

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 : HomologicalComplex C c'
e : c.Embedding c'
⊢ K.IsStrictlySupported e ∧ K.IsStrictlySupportedOutside e → IsZero K

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 : HomologicalComplex C c'
e : c.Embedding c'
h₁ : K.IsStrictlySupported e
h₂ : K.IsStrictlySupportedOutside e
n : ι'
hn : ¬∃ i, e.f i = n
⊢ ∀ (i : ι), e.f i ≠ n

Tactic:
simpa using hn

Result:
no goals

Proof state:
case mp.left
ι : 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 : HomologicalComplex C c'
e : c.Embedding c'
hK : IsZero K
⊢ K.IsStrictlySupported e

case mp.right
ι : 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 : HomologicalComplex C c'
e : c.Embedding c'
hK : IsZero K
⊢ K.IsStrictlySupportedOutside e

Tactic:
all_goals
  constructor
  intros
  exact (eval _ _ _).map_isZero hK

Result:
no goals

Proof state:
case mp
ι : 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 : HomologicalComplex C c'
e : c.Embedding c'
⊢ IsZero K → K.IsStrictlySupported e ∧ K.IsStrictlySupportedOutside e

Tactic:
intro hK

Result:
case mp
ι : 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 : HomologicalComplex C c'
e : c.Embedding c'
hK : IsZero K
⊢ K.IsStrictlySupported e ∧ K.IsStrictlySupportedOutside e

Proof state:
case mp.right.isZero
ι : 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 : HomologicalComplex C c'
e : c.Embedding c'
hK : IsZero K
i✝ : ι
⊢ IsZero (K.X (e.f i✝))

Tactic:
exact (eval _ _ _).map_isZero hK

Result:
no goals

Proof state:
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 : HomologicalComplex C c'
e : c.Embedding c'
h₁ : K.IsStrictlySupported e
h₂ : K.IsStrictlySupportedOutside e
i : ι
⊢ IsZero (K.X (e.f i))

Tactic:
exact h₂.isZero i

Result:
no goals