awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : HasZeroObject.{v_1, u_3} C
h : K.IsSupported e
i' : ι'
hi' : ¬∃ (i : ι), e.f i = i'
⊢ K.ExactAt i'

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

Premises used: HomologicalComplex.exactAt_of_isSupported
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : HasZeroObject.{v_1, u_3} C
mp : (K.truncGE e).Acyclic → K.IsSupportedOutside e
mpr : K.IsSupportedOutside e → (K.truncGE e).Acyclic
⊢ (K.truncGE e).Acyclic ↔ K.IsSupportedOutside e

Tactic:
constructor
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : HasZeroObject.{v_1, u_3} C
hK : (K.truncGE e).Acyclic
i : ι
⊢ K.ExactAt (e.f i)

Tactic:
simpa only [exactAt_iff_of_quasiIsoAt (K.πTruncGE e)] using hK (e.f i)

Premises used: exactAt_iff_of_quasiIsoAt, ComplexShape.Embedding.f, HomologicalComplex.πTruncGE
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : HasZeroObject.{v_1, u_3} C
hK : (K.truncGE e).Acyclic
⊢ K.IsSupportedOutside e

Tactic:
exact ⟨fun i ↦ by simpa only [exactAt_iff_of_quasiIsoAt (K.πTruncGE e)] using hK (e.f i)⟩
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : HasZeroObject.{v_1, u_3} C
hK : K.IsSupportedOutside e
i' : ι'
pos : ∀ (hi' : ∃ (i : ι), e.f i = i'), (K.truncGE e).ExactAt i'
neg : ∀ (hi' : ¬∃ (i : ι), e.f i = i'), (K.truncGE e).ExactAt i'
⊢ (K.truncGE e).ExactAt i'

Tactic:
by_cases hi' : ∃ i, e.f i = i'
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : HasZeroObject.{v_1, u_3} C
hK : K.IsSupportedOutside e
i' : ι'
hi' : ∃ (i : ι), e.f i = i'
pos : ∀ (i : ι), (K.truncGE e).ExactAt (e.f i)
⊢ (K.truncGE e).ExactAt i'

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

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : HasZeroObject.{v_1, u_3} C
hK : K.IsSupportedOutside e
i : ι
⊢ (K.truncGE e).ExactAt (e.f i)

Tactic:
simpa only [← exactAt_iff_of_quasiIsoAt (K.πTruncGE e)] using hK.exactAt i

Premises used: HomologicalComplex.IsSupportedOutside.exactAt, exactAt_iff_of_quasiIsoAt, HomologicalComplex.πTruncGE
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : HasZeroObject.{v_1, u_3} C
hK : K.IsSupportedOutside e
i' : ι'
hi' : ¬∃ (i : ι), e.f i = i'
⊢ ∀ (i : ι), e.f i ≠ i'

Tactic:
simpa using hi'
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : HasZeroObject.{v_1, u_3} C
hK : K.IsSupportedOutside e
i' : ι'
hi' : ¬∃ (i : ι), e.f i = i'
⊢ (K.truncGE e).ExactAt i'

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

Premises used: HomologicalComplex.exactAt_of_isSupported
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_2} C c'
φ : K ⟶ L
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
inst_5 : HasZeroObject.{v_1, u_3} C
i : ι
rw :
  QuasiIsoAt (L := L.truncGE e) (CategoryStruct.comp (Y := K.truncGE e) (K.πTruncGE e) (truncGEMap φ e)) (e.f i) ↔
    QuasiIsoAt φ (e.f i)
rw₁ : QuasiIsoAt (L := L.truncGE e) (φ ≫ L.πTruncGE e) (e.f i) ↔ QuasiIsoAt φ (e.f i)
rw₂ rw₃ : QuasiIsoAt φ (e.f i) ↔ QuasiIsoAt φ (e.f i)
⊢ QuasiIsoAt (K := K.truncGE e) (L := L.truncGE e) (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]

Premises used: quasiIsoAt_iff_comp_right, HomologicalComplex.πTruncGE_naturality, quasiIsoAt_iff_comp_left, HomologicalComplex.πTruncGE
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_2} C c'
φ : K ⟶ L
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
inst_5 : HasZeroObject.{v_1, u_3} C
⊢ ∀ (i : ι) (i' : ι'),
    e.f i = i' → (QuasiIsoAt (K := K.truncGE e) (L := L.truncGE e) (truncGEMap φ e) 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]
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_2} C c'
φ : K ⟶ L
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
inst_5 : HasZeroObject.{v_1, u_3} C
this :
  ∀ (i : ι) (i' : ι'),
    e.f i = i' → (QuasiIsoAt (K := K.truncGE e) (L := L.truncGE e) (truncGEMap φ e) i' ↔ QuasiIsoAt φ i')
rw :
  (∀ (i : ι'), QuasiIsoAt (K := K.truncGE e) (L := L.truncGE e) (truncGEMap φ e) i) ↔
    ∀ (i : ι) (i' : ι'), e.f i = i' → QuasiIsoAt φ i'
⊢ QuasiIso (K := K.truncGE e) (L := L.truncGE e) (truncGEMap φ e) ↔ ∀ (i : ι) (i' : ι'), e.f i = i' → QuasiIsoAt φ i'

Tactic:
rw [quasiIso_iff]

Premises used: quasiIso_iff
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_2} C c'
φ : K ⟶ L
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
inst_5 : HasZeroObject.{v_1, u_3} C
this :
  ∀ (i : ι) (i' : ι'),
    e.f i = i' → (QuasiIsoAt (K := K.truncGE e) (L := L.truncGE e) (truncGEMap φ e) i' ↔ QuasiIsoAt φ i')
mp :
  (∀ (i : ι'), QuasiIsoAt (K := K.truncGE e) (L := L.truncGE e) (truncGEMap φ e) i) →
    ∀ (i : ι) (i' : ι'), e.f i = i' → QuasiIsoAt φ i'
mpr :
  (∀ (i : ι) (i' : ι'), e.f i = i' → QuasiIsoAt φ i') →
    ∀ (i : ι'), QuasiIsoAt (K := K.truncGE e) (L := L.truncGE e) (truncGEMap φ e) i
⊢ (∀ (i : ι'), QuasiIsoAt (K := K.truncGE e) (L := L.truncGE e) (truncGEMap φ e) i) ↔
    ∀ (i : ι) (i' : ι'), e.f i = i' → QuasiIsoAt φ i'

Tactic:
constructor
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_2} C c'
φ : K ⟶ L
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
inst_5 : HasZeroObject.{v_1, u_3} C
this :
  ∀ (i : ι) (i' : ι'),
    e.f i = i' → (QuasiIsoAt (K := K.truncGE e) (L := L.truncGE e) (truncGEMap φ e) i' ↔ QuasiIsoAt φ i')
h : ∀ (i : ι'), QuasiIsoAt (K := K.truncGE e) (L := L.truncGE e) (truncGEMap φ e) i
i : ι
i' : ι'
hi : e.f i = i'
⊢ QuasiIsoAt φ i'

Tactic:
simpa only [← this i i' hi] using h i'
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_2} C c'
φ : K ⟶ L
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
inst_5 : HasZeroObject.{v_1, u_3} C
this :
  ∀ (i : ι) (i' : ι'),
    e.f i = i' → (QuasiIsoAt (K := K.truncGE e) (L := L.truncGE e) (truncGEMap φ e) i' ↔ QuasiIsoAt φ i')
h : ∀ (i : ι) (i' : ι'), e.f i = i' → QuasiIsoAt φ i'
i' : ι'
pos : ∀ (hi' : ∃ (i : ι), e.f i = i'), QuasiIsoAt (K := K.truncGE e) (L := L.truncGE e) (truncGEMap φ e) i'
neg : ∀ (hi' : ¬∃ (i : ι), e.f i = i'), QuasiIsoAt (K := K.truncGE e) (L := L.truncGE e) (truncGEMap φ e) i'
⊢ QuasiIsoAt (K := K.truncGE e) (L := L.truncGE e) (truncGEMap φ e) i'

Tactic:
by_cases hi' : ∃ i, e.f i = i'
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_2} C c'
φ : K ⟶ L
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
inst_5 : HasZeroObject.{v_1, u_3} C
this :
  ∀ (i : ι) (i' : ι'),
    e.f i = i' → (QuasiIsoAt (K := K.truncGE e) (L := L.truncGE e) (truncGEMap φ e) i' ↔ QuasiIsoAt φ i')
h : ∀ (i : ι) (i' : ι'), e.f i = i' → QuasiIsoAt φ i'
i' : ι'
hi' : ∃ (i : ι), e.f i = i'
pos : ∀ (i : ι) (hi : e.f i = i'), QuasiIsoAt (K := K.truncGE e) (L := L.truncGE e) (truncGEMap φ e) i'
⊢ QuasiIsoAt (K := K.truncGE e) (L := L.truncGE e) (truncGEMap φ e) i'

Tactic:
obtain ⟨i, hi⟩ := hi'
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_2} C c'
φ : K ⟶ L
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
inst_5 : HasZeroObject.{v_1, u_3} C
this :
  ∀ (i : ι) (i' : ι'),
    e.f i = i' → (QuasiIsoAt (K := K.truncGE e) (L := L.truncGE e) (truncGEMap φ e) i' ↔ QuasiIsoAt φ i')
h : ∀ (i : ι) (i' : ι'), e.f i = i' → QuasiIsoAt φ i'
i' : ι'
i : ι
hi : e.f i = i'
⊢ QuasiIsoAt (K := K.truncGE e) (L := L.truncGE e) (truncGEMap φ e) i'

Tactic:
simpa only [this i i' hi] using h i i' hi
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_2} C c'
φ : K ⟶ L
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
inst_5 : HasZeroObject.{v_1, u_3} C
this :
  ∀ (i : ι) (i' : ι'),
    e.f i = i' → (QuasiIsoAt (K := K.truncGE e) (L := L.truncGE e) (truncGEMap φ e) i' ↔ QuasiIsoAt φ i')
h : ∀ (i : ι) (i' : ι'), e.f i = i' → QuasiIsoAt φ i'
i' : ι'
hi' : ¬∃ (i : ι), e.f i = i'
neg : (L.truncGE e).ExactAt i'
neg₁ : (K.truncGE e).ExactAt i'
⊢ QuasiIsoAt (K := K.truncGE e) (L := L.truncGE e) (truncGEMap φ e) i'

Tactic:
rw [quasiIsoAt_iff_exactAt]

Premises used: quasiIsoAt_iff_exactAt
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_2} C c'
φ : K ⟶ L
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
inst_5 : HasZeroObject.{v_1, u_3} C
this :
  ∀ (i : ι) (i' : ι'),
    e.f i = i' → (QuasiIsoAt (K := K.truncGE e) (L := L.truncGE e) (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'
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_2} C c'
φ : K ⟶ L
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
inst_5 : HasZeroObject.{v_1, u_3} C
this :
  ∀ (i : ι) (i' : ι'),
    e.f i = i' → (QuasiIsoAt (K := K.truncGE e) (L := L.truncGE e) (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'

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

Premises used: HomologicalComplex.exactAt_of_isSupported
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_2} C c'
φ : K ⟶ L
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
inst_5 : HasZeroObject.{v_1, u_3} C
this :
  ∀ (i : ι) (i' : ι'),
    e.f i = i' → (QuasiIsoAt (K := K.truncGE e) (L := L.truncGE e) (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:
exact exactAt_of_isSupported _ e i' (by simpa using hi')

Premises used: HomologicalComplex.exactAt_of_isSupported
-- Module: Mathlib.Algebra.Homology.Embedding.TruncLE
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K L M : HomologicalComplex.{v_1, u_3, u_2} C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst_2 : e.IsTruncLE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
inst_5 : ∀ (i' : ι'), M.HasHomology i'
i : ι
i' : ι'
hi' : e.f i = i'
hi : ¬e.BoundaryLE i
⊢ ¬e.op.BoundaryGE i

Tactic:
simpa
-- Module: Mathlib.Algebra.Homology.Embedding.TruncLE
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K L M : HomologicalComplex.{v_1, u_3, u_2} C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst_2 : e.IsTruncLE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
inst_5 : ∀ (i' : ι'), M.HasHomology i'
i : ι
i' : ι'
hi' : e.f i = i'
hi : e.BoundaryLE i
⊢ e.op.BoundaryGE i

Tactic:
simpa
-- Module: Mathlib.Algebra.Homology.Embedding.TruncLE
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncLE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
i j : ι
hij : c.Rel i j
i' j' : ι'
hi' : e.f i = i'
hj' : e.f j = j'
hj : ¬e.BoundaryLE j
⊢ ¬e.op.BoundaryGE j

Tactic:
simpa
-- Module: Mathlib.Algebra.Homology.Embedding.TruncLE
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncLE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
i j : ι
hij : c.Rel i j
i' j' : ι'
hi' : e.f i = i'
hj' : e.f j = j'
hj : ¬e.BoundaryLE j
⊢ ((K.truncLE' e).d i j).op =
    Quiver.Hom.op (Iso.hom (K.truncLE'XIso e hi' ⋯) ≫ K.d i' j' ≫ Iso.inv (K.truncLE'XIso e hj' hj))

Tactic:
simpa using K.op.truncGE'_d_eq e.op hij hj' hi' (by simpa)

Premises used: HomologicalComplex.op, HomologicalComplex.truncGE'_d_eq, ComplexShape.Embedding.op
-- Module: Mathlib.Algebra.Homology.Embedding.TruncLE
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncLE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
i j : ι
hij : c.Rel i j
i' j' : ι'
hi' : e.f i = i'
hj' : e.f j = j'
hj : e.BoundaryLE j
⊢ e.op.BoundaryGE j

Tactic:
simpa
-- Module: Mathlib.Algebra.Homology.Embedding.TruncLE
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncLE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
i j : ι
hij : c.Rel i j
i' j' : ι'
hi' : e.f i = i'
hj' : e.f j = j'
hj : e.BoundaryLE j
⊢ ((K.truncLE' e).d i j).op =
    Quiver.Hom.op (Iso.hom (K.truncLE'XIso e hi' ⋯) ≫ K.toCycles i' j' ≫ Iso.inv (K.truncLE'XIsoCycles e hj' hj))

Tactic:
simpa [truncLE', truncLE'XIso, truncLE'XIsoCycles]
      using K.op.truncGE'_d_eq_fromOpcycles e.op hij hj' hi' (by simpa)

Premises used: HomologicalComplex.truncLE'XIso, HomologicalComplex.truncLE'XIsoCycles, HomologicalComplex.op, HomologicalComplex.truncLE', HomologicalComplex.truncGE'_d_eq_fromOpcycles, ComplexShape.Embedding.op
-- Module: Mathlib.Algebra.Homology.Embedding.TruncLE
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K L M : HomologicalComplex.{v_1, u_3, u_2} C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst_2 : e.IsTruncLE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
inst_5 : ∀ (i' : ι'), M.HasHomology i'
inst_6 : HasZeroObject.{v_1, u_3} C
i : ι
i' : ι'
hi' : e.f i = i'
hi : ¬e.BoundaryLE i
⊢ ¬e.op.BoundaryGE i

Tactic:
simpa
-- Module: Mathlib.Algebra.Homology.Embedding.TruncLE
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K L M : HomologicalComplex.{v_1, u_3, u_2} C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst_2 : e.IsTruncLE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
inst_5 : ∀ (i' : ι'), M.HasHomology i'
inst_6 : HasZeroObject.{v_1, u_3} C
i : ι
i' : ι'
hi' : e.f i = i'
hi : e.BoundaryLE i
⊢ e.op.BoundaryGE i

Tactic:
simpa
-- Module: Mathlib.Algebra.Homology.Embedding.TruncLE
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_2} C c'
φ : K ⟶ L
e : c.Embedding c'
inst_2 : e.IsTruncLE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
i : ι
hi : e.BoundaryLE i
i' : ι'
h : e.f i = i'
a :
  Eq (α := Opposite.op ((L.truncLE' e).X i) ⟶ Opposite.op ((K.truncLE' e).X i))
    (Quiver.Hom.op (Hom.f (truncLE'Map φ e) i))
    (Quiver.Hom.op (Iso.hom (K.truncLE'XIsoCycles e h hi) ≫ cyclesMap φ i' ≫ Iso.inv (L.truncLE'XIsoCycles e h hi)))
⊢ Eq (α := (K.truncLE' e).X i ⟶ (L.truncLE' e).X i) (Hom.f (truncLE'Map φ e) i)
    (Iso.hom (K.truncLE'XIsoCycles e h hi) ≫ cyclesMap φ i' ≫ Iso.inv (L.truncLE'XIsoCycles e h hi))

Tactic:
apply Quiver.Hom.op_inj

Premises used: Quiver.Hom.op_inj
-- Module: Mathlib.Algebra.Homology.Embedding.TruncLE
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_2} C c'
φ : K ⟶ L
e : c.Embedding c'
inst_2 : e.IsTruncLE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
i : ι
hi : e.BoundaryLE i
i' : ι'
h : e.f i = i'
a :
  Eq (α := Opposite.op ((L.truncLE' e).X i) ⟶ Opposite.op ((K.truncLE' e).X i))
    (Hom.f (truncGE'Map (CategoryTheory.Functor.map (opFunctor C c') φ.op) e.op) i :
      { X := truncGE'.X L.op e.op,
              d := (truncGE'.d L.op e.op : (i j : ι) → truncGE'.X L.op e.op i ⟶ truncGE'.X L.op e.op j), shape := ⋯,
              d_comp_d' := ⋯ : HomologicalComplex.{v_1, u_3, u_1} Cᵒᵖ c.symm }.X
          i ⟶
        { X := truncGE'.X K.op e.op,
              d := (truncGE'.d K.op e.op : (i j : ι) → truncGE'.X K.op e.op i ⟶ truncGE'.X K.op e.op j), shape := ⋯,
              d_comp_d' := ⋯ : HomologicalComplex.{v_1, u_3, u_1} Cᵒᵖ c.symm }.X
          i)
    (CategoryStruct.comp (Y := Opposite.op (K.cycles i'))
        (CategoryStruct.comp (Y := Opposite.op (L.cycles i'))
          (Iso.hom (L.op.truncGE'XIsoOpcycles e.op h ⋯) ≫ Iso.hom (L.opcyclesOpIso i'))
          (Quiver.Hom.op (cyclesMap φ i')))
        (Iso.inv (K.opcyclesOpIso i') ≫ Iso.inv (K.op.truncGE'XIsoOpcycles e.op h ⋯)) :
      Opposite.op ((L.truncLE' e).X i) ⟶ Opposite.op ((K.truncLE' e).X i))
⊢ Eq (α := Opposite.op ((L.truncLE' e).X i) ⟶ Opposite.op ((K.truncLE' e).X i))
    (Quiver.Hom.op (Hom.f (truncLE'Map φ e) i))
    (Quiver.Hom.op (Iso.hom (K.truncLE'XIsoCycles e h hi) ≫ cyclesMap φ i' ≫ Iso.inv (L.truncLE'XIsoCycles e h hi)))

Tactic:
dsimp [truncLE'Map, truncLE'XIsoCycles]

Premises used: HomologicalComplex.truncLE'XIsoCycles, HomologicalComplex.truncLE'Map
-- Module: Mathlib.Algebra.Homology.Embedding.TruncLE
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_2} C c'
φ : K ⟶ L
e : c.Embedding c'
inst_2 : e.IsTruncLE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
i : ι
hi : e.BoundaryLE i
i' : ι'
h : e.f i = i'
⊢ e.op.BoundaryGE i

Tactic:
simpa
-- Module: Mathlib.Algebra.Homology.Embedding.TruncLE
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_2} C c'
φ : K ⟶ L
e : c.Embedding c'
inst_2 : e.IsTruncLE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
i : ι
hi : ¬e.BoundaryLE i
i' : ι'
h : e.f i = i'
⊢ ¬e.op.BoundaryGE i

Tactic:
simpa