awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.Embedding.AreComplementary
Goal:
ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
X : ι → Type u_5
x₁ : (i₁ : ι₁) → X (e₁.f i₁)
x₂ : (i₂ : ι₂) → X (e₂.f i₂)
i : ι₁ ⊕ ι₂
i₁ : ι₁
h : Sum.inl i₁ = i
subst :
  Eq (α := X ((ac.equiv : (a : ι₁ ⊕ ι₂) → ι) (Sum.inl i₁))) (ac.desc' (X := X) x₁ x₂ (Sum.inl i₁))
    ((desc.aux X (e₁.f i₁) ((ac.equiv : (a : ι₁ ⊕ ι₂) → ι) (Sum.inl i₁)) ⋯ :
        (a : X (e₁.f i₁)) → X ((ac.equiv : (a : ι₁ ⊕ ι₂) → ι) (Sum.inl i₁)))
      (x₁ i₁))
⊢ ac.desc' (X := X) x₁ x₂ i =
    (desc.aux X (e₁.f i₁) ((ac.equiv : (a : ι₁ ⊕ ι₂) → ι) i) ⋯ :
        (a : X (e₁.f i₁)) → X ((ac.equiv : (a : ι₁ ⊕ ι₂) → ι) i))
      (x₁ i₁)

Tactic:
subst h
-- Module: Mathlib.Algebra.Homology.Embedding.AreComplementary
Goal:
ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
X : ι → Type u_5
x₁ : (i₁ : ι₁) → X (e₁.f i₁)
x₂ : (i₂ : ι₂) → X (e₂.f i₂)
i₁ : ι₁
⊢ Eq (α := X ((ac.equiv : (a : ι₁ ⊕ ι₂) → ι) (Sum.inl i₁))) (ac.desc' (X := X) x₁ x₂ (Sum.inl i₁))
    ((desc.aux X (e₁.f i₁) ((ac.equiv : (a : ι₁ ⊕ ι₂) → ι) (Sum.inl i₁)) ⋯ :
        (a : X (e₁.f i₁)) → X ((ac.equiv : (a : ι₁ ⊕ ι₂) → ι) (Sum.inl i₁)))
      (x₁ i₁))

Tactic:
rfl
-- Module: Mathlib.Algebra.Homology.Embedding.AreComplementary
Goal:
ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
C : Type u_4
inst : Category.{v_1, u_4} C
inst_1 : HasZeroMorphisms.{v_1, u_4} C
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
X : ι → Type u_5
x₁ : (i₁ : ι₁) → X (e₁.f i₁)
x₂ : (i₂ : ι₂) → X (e₂.f i₂)
i : ι₁ ⊕ ι₂
i₂ : ι₂
h : Sum.inr i₂ = i
subst : e₂.f i₂ = (ac.equiv : (a : ι₁ ⊕ ι₂) → ι) (Sum.inr i₂)
⊢ e₂.f i₂ = (ac.equiv : (a : ι₁ ⊕ ι₂) → ι) i

Tactic:
subst h
-- Module: Mathlib.Algebra.Homology.Embedding.AreComplementary
Goal:
ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
C : Type u_4
inst : Category.{v_1, u_4} C
inst_1 : HasZeroMorphisms.{v_1, u_4} C
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
X : ι → Type u_5
x₁ : (i₁ : ι₁) → X (e₁.f i₁)
x₂ : (i₂ : ι₂) → X (e₂.f i₂)
i₂ : ι₂
⊢ e₂.f i₂ = (ac.equiv : (a : ι₁ ⊕ ι₂) → ι) (Sum.inr i₂)

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.Embedding.AreComplementary
Goal:
ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
X : ι → Type u_5
x₁ : (i₁ : ι₁) → X (e₁.f i₁)
x₂ : (i₂ : ι₂) → X (e₂.f i₂)
i : ι₁ ⊕ ι₂
i₂ : ι₂
h : Sum.inr i₂ = i
subst :
  Eq (α := X ((ac.equiv : (a : ι₁ ⊕ ι₂) → ι) (Sum.inr i₂))) (ac.desc' (X := X) x₁ x₂ (Sum.inr i₂))
    ((desc.aux X (e₂.f i₂) ((ac.equiv : (a : ι₁ ⊕ ι₂) → ι) (Sum.inr i₂)) ⋯ :
        (a : X (e₂.f i₂)) → X ((ac.equiv : (a : ι₁ ⊕ ι₂) → ι) (Sum.inr i₂)))
      (x₂ i₂))
⊢ ac.desc' (X := X) x₁ x₂ i =
    (desc.aux X (e₂.f i₂) ((ac.equiv : (a : ι₁ ⊕ ι₂) → ι) i) ⋯ :
        (a : X (e₂.f i₂)) → X ((ac.equiv : (a : ι₁ ⊕ ι₂) → ι) i))
      (x₂ i₂)

Tactic:
subst h
-- Module: Mathlib.Algebra.Homology.Embedding.AreComplementary
Goal:
ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
X : ι → Type u_5
x₁ : (i₁ : ι₁) → X (e₁.f i₁)
x₂ : (i₂ : ι₂) → X (e₂.f i₂)
i₂ : ι₂
⊢ Eq (α := X ((ac.equiv : (a : ι₁ ⊕ ι₂) → ι) (Sum.inr i₂))) (ac.desc' (X := X) x₁ x₂ (Sum.inr i₂))
    ((desc.aux X (e₂.f i₂) ((ac.equiv : (a : ι₁ ⊕ ι₂) → ι) (Sum.inr i₂)) ⋯ :
        (a : X (e₂.f i₂)) → X ((ac.equiv : (a : ι₁ ⊕ ι₂) → ι) (Sum.inr i₂)))
      (x₂ i₂))

Tactic:
rfl
-- Module: Mathlib.Algebra.Homology.Embedding.AreComplementary
Goal:
ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
C : Type u_4
inst : Category.{v_1, u_4} C
inst_1 : HasZeroMorphisms.{v_1, u_4} C
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
X : ι → Type u_5
x₁ : (i₁ : ι₁) → X (e₁.f i₁)
x₂ : (i₂ : ι₂) → X (e₂.f i₂)
i : ι
⊢ (ac.equiv : (a : ι₁ ⊕ ι₂) → ι) ((ac.equiv.symm : (a : ι) → ι₁ ⊕ ι₂) i : ι₁ ⊕ ι₂) = i

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.Embedding.AreComplementary
Goal:
ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
X : ι → Type u_5
x₁ : (i₁ : ι₁) → X (e₁.f i₁)
x₂ : (i₂ : ι₂) → X (e₂.f i₂)
i₁ : ι₁
dsimp :
  (desc.aux X ((ac.equiv : (a : ι₁ ⊕ ι₂) → ι) ((ac.equiv.symm : (a : ι) → ι₁ ⊕ ι₂) (e₁.f i₁) : ι₁ ⊕ ι₂)) (e₁.f i₁) ⋯ :
        (a : X ((ac.equiv : (a : ι₁ ⊕ ι₂) → ι) ((ac.equiv.symm : (a : ι) → ι₁ ⊕ ι₂) (e₁.f i₁)))) → X (e₁.f i₁))
      (ac.desc' (X := X) x₁ x₂ ((ac.equiv.symm : (a : ι) → ι₁ ⊕ ι₂) (e₁.f i₁))) =
    x₁ i₁
⊢ ac.desc (X := X) x₁ x₂ (e₁.f i₁) = x₁ i₁

Tactic:
dsimp [desc]

Premises used: ComplexShape.Embedding.AreComplementary.desc
-- Module: Mathlib.Algebra.Homology.Embedding.AreComplementary
Goal:
ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
X : ι → Type u_5
x₁ : (i₁ : ι₁) → X (e₁.f i₁)
x₂ : (i₂ : ι₂) → X (e₂.f i₂)
i₁ : ι₁
⊢ Eq.{u_1 + 1} (α := ι) ((ac.equiv : (a : ι₁ ⊕ ι₂) → ι) (Sum.inl i₁) : ι)
    ((ac.equiv : (a : ι₁ ⊕ ι₂) → ι) ((ac.equiv.symm : (a : ι) → ι₁ ⊕ ι₂) (e₁.f i₁) : ι₁ ⊕ ι₂) : ι)

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.Embedding.AreComplementary
Goal:
ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
X : ι → Type u_5
x₁ : (i₁ : ι₁) → X (e₁.f i₁)
x₂ : (i₂ : ι₂) → X (e₂.f i₂)
i₁ : ι₁
rw : (desc.aux X (e₁.f i₁) (e₁.f i₁) ⋯ : (a : X (e₁.f i₁)) → X (e₁.f i₁)) (x₁ i₁) = x₁ i₁
⊢ (desc.aux X ((ac.equiv : (a : ι₁ ⊕ ι₂) → ι) ((ac.equiv.symm : (a : ι) → ι₁ ⊕ ι₂) (e₁.f i₁) : ι₁ ⊕ ι₂)) (e₁.f i₁) ⋯ :
        (a : X ((ac.equiv : (a : ι₁ ⊕ ι₂) → ι) ((ac.equiv.symm : (a : ι) → ι₁ ⊕ ι₂) (e₁.f i₁)))) → X (e₁.f i₁))
      (ac.desc' (X := X) x₁ x₂ ((ac.equiv.symm : (a : ι) → ι₁ ⊕ ι₂) (e₁.f i₁))) =
    x₁ i₁

Tactic:
rw [ac.desc'_inl _ _ _ i₁ (ac.equiv.injective (by simp)), desc.aux_trans]

Premises used: ComplexShape.Embedding.AreComplementary.desc'_inl, Equiv.injective, ComplexShape.Embedding.AreComplementary.desc.aux_trans, ComplexShape.Embedding.AreComplementary.equiv
-- Module: Mathlib.Algebra.Homology.Embedding.AreComplementary
Goal:
ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
X : ι → Type u_5
x₁ : (i₁ : ι₁) → X (e₁.f i₁)
x₂ : (i₂ : ι₂) → X (e₂.f i₂)
i₁ : ι₁
⊢ (desc.aux X (e₁.f i₁) (e₁.f i₁) ⋯ : (a : X (e₁.f i₁)) → X (e₁.f i₁)) (x₁ i₁) = x₁ i₁

Tactic:
rfl
-- Module: Mathlib.Algebra.Homology.Embedding.AreComplementary
Goal:
ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
X : ι → Type u_5
x₁ : (i₁ : ι₁) → X (e₁.f i₁)
x₂ : (i₂ : ι₂) → X (e₂.f i₂)
i₂ : ι₂
dsimp :
  (desc.aux X ((ac.equiv : (a : ι₁ ⊕ ι₂) → ι) ((ac.equiv.symm : (a : ι) → ι₁ ⊕ ι₂) (e₂.f i₂) : ι₁ ⊕ ι₂)) (e₂.f i₂) ⋯ :
        (a : X ((ac.equiv : (a : ι₁ ⊕ ι₂) → ι) ((ac.equiv.symm : (a : ι) → ι₁ ⊕ ι₂) (e₂.f i₂)))) → X (e₂.f i₂))
      (ac.desc' (X := X) x₁ x₂ ((ac.equiv.symm : (a : ι) → ι₁ ⊕ ι₂) (e₂.f i₂))) =
    x₂ i₂
⊢ ac.desc (X := X) x₁ x₂ (e₂.f i₂) = x₂ i₂

Tactic:
dsimp [desc]

Premises used: ComplexShape.Embedding.AreComplementary.desc
-- Module: Mathlib.Algebra.Homology.Embedding.AreComplementary
Goal:
ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
X : ι → Type u_5
x₁ : (i₁ : ι₁) → X (e₁.f i₁)
x₂ : (i₂ : ι₂) → X (e₂.f i₂)
i₂ : ι₂
⊢ Eq.{u_1 + 1} (α := ι) ((ac.equiv : (a : ι₁ ⊕ ι₂) → ι) (Sum.inr i₂) : ι)
    ((ac.equiv : (a : ι₁ ⊕ ι₂) → ι) ((ac.equiv.symm : (a : ι) → ι₁ ⊕ ι₂) (e₂.f i₂) : ι₁ ⊕ ι₂) : ι)

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.Embedding.AreComplementary
Goal:
ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
X : ι → Type u_5
x₁ : (i₁ : ι₁) → X (e₁.f i₁)
x₂ : (i₂ : ι₂) → X (e₂.f i₂)
i₂ : ι₂
rw : (desc.aux X (e₂.f i₂) (e₂.f i₂) ⋯ : (a : X (e₂.f i₂)) → X (e₂.f i₂)) (x₂ i₂) = x₂ i₂
⊢ (desc.aux X ((ac.equiv : (a : ι₁ ⊕ ι₂) → ι) ((ac.equiv.symm : (a : ι) → ι₁ ⊕ ι₂) (e₂.f i₂) : ι₁ ⊕ ι₂)) (e₂.f i₂) ⋯ :
        (a : X ((ac.equiv : (a : ι₁ ⊕ ι₂) → ι) ((ac.equiv.symm : (a : ι) → ι₁ ⊕ ι₂) (e₂.f i₂)))) → X (e₂.f i₂))
      (ac.desc' (X := X) x₁ x₂ ((ac.equiv.symm : (a : ι) → ι₁ ⊕ ι₂) (e₂.f i₂))) =
    x₂ i₂

Tactic:
rw [ac.desc'_inr _ _ _ i₂ (ac.equiv.injective (by simp)), desc.aux_trans]

Premises used: Equiv.injective, ComplexShape.Embedding.AreComplementary.desc.aux_trans, ComplexShape.Embedding.AreComplementary.equiv, ComplexShape.Embedding.AreComplementary.desc'_inr
-- Module: Mathlib.Algebra.Homology.Embedding.AreComplementary
Goal:
ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
X : ι → Type u_5
x₁ : (i₁ : ι₁) → X (e₁.f i₁)
x₂ : (i₂ : ι₂) → X (e₂.f i₂)
i₂ : ι₂
⊢ (desc.aux X (e₂.f i₂) (e₂.f i₂) ⋯ : (a : X (e₂.f i₂)) → X (e₂.f i₂)) (x₂ i₂) = x₂ i₂

Tactic:
rfl
-- Module: Mathlib.Algebra.Homology.Embedding.AreComplementary
Goal:
ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
C : Type u_4
inst : Category.{v_1, u_4} C
inst_1 : HasZeroMorphisms.{v_1, u_4} C
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
K : HomologicalComplex.{v_1, u_4, u_1} C c
mp : K.IsStrictlySupportedOutside e₁ → K.IsStrictlySupported e₂
mpr : K.IsStrictlySupported e₂ → K.IsStrictlySupportedOutside e₁
⊢ K.IsStrictlySupportedOutside e₁ ↔ K.IsStrictlySupported e₂

Tactic:
constructor
-- Module: Mathlib.Algebra.Homology.Embedding.AreComplementary
Goal:
ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
C : Type u_4
inst : Category.{v_1, u_4} C
inst_1 : HasZeroMorphisms.{v_1, u_4} C
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
K : HomologicalComplex.{v_1, u_4, u_1} C c
h : K.IsStrictlySupportedOutside e₁
i : ι
hi : ∀ (i_1 : ι₂), e₂.f i_1 ≠ i
obtain : ∀ (i₁ : ι₁) (hi : ∀ (i : ι₂), e₂.f i ≠ e₁.f i₁), IsZero.{v_1, u_4} (K.X (e₁.f i₁))
⊢ IsZero.{v_1, u_4} (K.X i)

Tactic:
obtain ⟨i₁, rfl⟩ := ac.exists_i₁ i hi

Premises used: ComplexShape.Embedding.AreComplementary.exists_i₁, rfl
-- Module: Mathlib.Algebra.Homology.Embedding.AreComplementary
Goal:
ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
C : Type u_4
inst : Category.{v_1, u_4} C
inst_1 : HasZeroMorphisms.{v_1, u_4} C
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
K : HomologicalComplex.{v_1, u_4, u_1} C c
h : K.IsStrictlySupportedOutside e₁
i₁ : ι₁
hi : ∀ (i : ι₂), e₂.f i ≠ e₁.f i₁
⊢ IsZero.{v_1, u_4} (K.X (e₁.f i₁))

Tactic:
h.isZero i₁

Premises used: HomologicalComplex.IsStrictlySupportedOutside.isZero
-- Module: Mathlib.Algebra.Homology.Embedding.AreComplementary
Goal:
ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
C : Type u_4
inst : Category.{v_1, u_4} C
inst_1 : HasZeroMorphisms.{v_1, u_4} C
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
K : HomologicalComplex.{v_1, u_4, u_1} C c
h : K.IsStrictlySupportedOutside e₁
i₁ : ι₁
hi : ∀ (i : ι₂), e₂.f i ≠ e₁.f i₁
⊢ IsZero.{v_1, u_4} (K.X (e₁.f i₁))

Tactic:
exact h.isZero i₁

Premises used: HomologicalComplex.IsStrictlySupportedOutside.isZero
-- Module: Mathlib.Algebra.Homology.Embedding.AreComplementary
Goal:
ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
C : Type u_4
inst : Category.{v_1, u_4} C
inst_1 : HasZeroMorphisms.{v_1, u_4} C
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
K : HomologicalComplex.{v_1, u_4, u_1} C c
h : K.IsStrictlySupportedOutside e₁
⊢ K.IsStrictlySupported e₂

Tactic:
exact ⟨fun i hi => by
      obtain ⟨i₁, rfl⟩ := ac.exists_i₁ i hi
      exact h.isZero i₁⟩
-- Module: Mathlib.Algebra.Homology.Embedding.AreComplementary
Goal:
ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
C : Type u_4
inst : Category.{v_1, u_4} C
inst_1 : HasZeroMorphisms.{v_1, u_4} C
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
K : HomologicalComplex.{v_1, u_4, u_1} C c
h : K.IsStrictlySupported e₂
⊢ K.IsStrictlySupportedOutside e₁

Tactic:
⟨fun i₁ => K.isZero_X_of_isStrictlySupported e₂ _
      (fun i₂ => (ac.disjoint i₁ i₂).symm)⟩

Premises used: ComplexShape.Embedding.AreComplementary.disjoint, Ne.symm, HomologicalComplex.IsStrictlySupportedOutside.mk, ComplexShape.Embedding.f, HomologicalComplex.isZero_X_of_isStrictlySupported
-- Module: Mathlib.Algebra.Homology.Embedding.AreComplementary
Goal:
ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
C : Type u_4
inst : Category.{v_1, u_4} C
inst_1 : HasZeroMorphisms.{v_1, u_4} C
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
K : HomologicalComplex.{v_1, u_4, u_1} C c
h : K.IsStrictlySupported e₂
⊢ K.IsStrictlySupportedOutside e₁

Tactic:
exact ⟨fun i₁ => K.isZero_X_of_isStrictlySupported e₂ _
      (fun i₂ => (ac.disjoint i₁ i₂).symm)⟩
-- Module: Mathlib.Algebra.Homology.Embedding.AreComplementary
Goal:
ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
C : Type u_4
inst : Category.{v_1, u_4} C
inst_1 : HasZeroMorphisms.{v_1, u_4} C
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
K : HomologicalComplex.{v_1, u_4, u_1} C c
⊢ K.IsStrictlySupportedOutside e₂ ↔ K.IsStrictlySupported e₁

Tactic:
ac.symm.isStrictlySupportedOutside₁_iff K

Premises used: ComplexShape.Embedding.AreComplementary.isStrictlySupportedOutside₁_iff, ComplexShape.Embedding.AreComplementary.symm
-- Module: Mathlib.Algebra.Homology.Embedding.AreComplementary
Goal:
ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
C : Type u_4
inst : Category.{v_1, u_4} C
inst_1 : HasZeroMorphisms.{v_1, u_4} C
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
K : HomologicalComplex.{v_1, u_4, u_1} C c
mp : K.IsSupportedOutside e₁ → K.IsSupported e₂
mpr : K.IsSupported e₂ → K.IsSupportedOutside e₁
⊢ K.IsSupportedOutside e₁ ↔ K.IsSupported e₂

Tactic:
constructor
-- Module: Mathlib.Algebra.Homology.Embedding.AreComplementary
Goal:
ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
C : Type u_4
inst : Category.{v_1, u_4} C
inst_1 : HasZeroMorphisms.{v_1, u_4} C
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
K : HomologicalComplex.{v_1, u_4, u_1} C c
h : K.IsSupportedOutside e₁
i : ι
hi : ∀ (i_1 : ι₂), e₂.f i_1 ≠ i
obtain : ∀ (i₁ : ι₁) (hi : ∀ (i : ι₂), e₂.f i ≠ e₁.f i₁), K.ExactAt (e₁.f i₁)
⊢ K.ExactAt i

Tactic:
obtain ⟨i₁, rfl⟩ := ac.exists_i₁ i hi

Premises used: ComplexShape.Embedding.AreComplementary.exists_i₁, rfl
-- Module: Mathlib.Algebra.Homology.Embedding.AreComplementary
Goal:
ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
C : Type u_4
inst : Category.{v_1, u_4} C
inst_1 : HasZeroMorphisms.{v_1, u_4} C
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
K : HomologicalComplex.{v_1, u_4, u_1} C c
h : K.IsSupportedOutside e₁
i₁ : ι₁
hi : ∀ (i : ι₂), e₂.f i ≠ e₁.f i₁
⊢ K.ExactAt (e₁.f i₁)

Tactic:
h.exactAt i₁

Premises used: HomologicalComplex.IsSupportedOutside.exactAt
-- Module: Mathlib.Algebra.Homology.Embedding.AreComplementary
Goal:
ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
C : Type u_4
inst : Category.{v_1, u_4} C
inst_1 : HasZeroMorphisms.{v_1, u_4} C
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
K : HomologicalComplex.{v_1, u_4, u_1} C c
h : K.IsSupportedOutside e₁
i₁ : ι₁
hi : ∀ (i : ι₂), e₂.f i ≠ e₁.f i₁
⊢ K.ExactAt (e₁.f i₁)

Tactic:
exact h.exactAt i₁

Premises used: HomologicalComplex.IsSupportedOutside.exactAt
-- Module: Mathlib.Algebra.Homology.Embedding.AreComplementary
Goal:
ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
C : Type u_4
inst : Category.{v_1, u_4} C
inst_1 : HasZeroMorphisms.{v_1, u_4} C
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
K : HomologicalComplex.{v_1, u_4, u_1} C c
h : K.IsSupportedOutside e₁
⊢ K.IsSupported e₂

Tactic:
exact ⟨fun i hi => by
      obtain ⟨i₁, rfl⟩ := ac.exists_i₁ i hi
      exact h.exactAt i₁⟩
-- Module: Mathlib.Algebra.Homology.Embedding.AreComplementary
Goal:
ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
C : Type u_4
inst : Category.{v_1, u_4} C
inst_1 : HasZeroMorphisms.{v_1, u_4} C
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
K : HomologicalComplex.{v_1, u_4, u_1} C c
h : K.IsSupported e₂
⊢ K.IsSupportedOutside e₁

Tactic:
⟨fun i₁ => K.exactAt_of_isSupported e₂ _
      (fun i₂ => (ac.disjoint i₁ i₂).symm)⟩

Premises used: ComplexShape.Embedding.AreComplementary.disjoint, HomologicalComplex.exactAt_of_isSupported, Ne.symm, HomologicalComplex.IsSupportedOutside.mk, ComplexShape.Embedding.f
-- Module: Mathlib.Algebra.Homology.Embedding.AreComplementary
Goal:
ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
C : Type u_4
inst : Category.{v_1, u_4} C
inst_1 : HasZeroMorphisms.{v_1, u_4} C
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
K : HomologicalComplex.{v_1, u_4, u_1} C c
h : K.IsSupported e₂
⊢ K.IsSupportedOutside e₁

Tactic:
exact ⟨fun i₁ => K.exactAt_of_isSupported e₂ _
      (fun i₂ => (ac.disjoint i₁ i₂).symm)⟩
-- Module: Mathlib.Algebra.Homology.Embedding.AreComplementary
Goal:
ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
C : Type u_4
inst : Category.{v_1, u_4} C
inst_1 : HasZeroMorphisms.{v_1, u_4} C
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
K : HomologicalComplex.{v_1, u_4, u_1} C c
⊢ K.IsSupportedOutside e₂ ↔ K.IsSupported e₁

Tactic:
ac.symm.isSupportedOutside₁_iff K

Premises used: ComplexShape.Embedding.AreComplementary.isSupportedOutside₁_iff, ComplexShape.Embedding.AreComplementary.symm
-- Module: Mathlib.Algebra.Homology.Embedding.AreComplementary
Goal:
ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
C : Type u_4
inst : Category.{v_1, u_4} C
inst_1 : HasZeroMorphisms.{v_1, u_4} C
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
K L : HomologicalComplex.{v_1, u_4, u_1} C c
φ : K ⟶ L
hK : K.IsStrictlySupportedOutside e₂
hL : L.IsStrictlySupportedOutside e₁
h : ∀ (i : ι), φ.f i = HomologicalComplex.Hom.f 0 i
⊢ φ = 0

Tactic:
ext i
-- Module: Mathlib.Algebra.Homology.Embedding.AreComplementary
Goal:
ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
C : Type u_4
inst : Category.{v_1, u_4} C
inst_1 : HasZeroMorphisms.{v_1, u_4} C
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
K L : HomologicalComplex.{v_1, u_4, u_1} C c
φ : K ⟶ L
hK : K.IsStrictlySupportedOutside e₂
hL : L.IsStrictlySupportedOutside e₁
i : ι
h : ∀ (i₁ : ι₁), φ.f (e₁.f i₁) = HomologicalComplex.Hom.f 0 (e₁.f i₁)
h₁ : ∀ (i₂ : ι₂), φ.f (e₂.f i₂) = HomologicalComplex.Hom.f 0 (e₂.f i₂)
⊢ φ.f i = HomologicalComplex.Hom.f 0 i

Tactic:
obtain ⟨i₁, rfl⟩ | ⟨i₂, rfl⟩ := ac.union i

Premises used: ComplexShape.Embedding.AreComplementary.union, rfl
-- Module: Mathlib.Algebra.Homology.Embedding.AreComplementary
Goal:
ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
C : Type u_4
inst : Category.{v_1, u_4} C
inst_1 : HasZeroMorphisms.{v_1, u_4} C
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
K L : HomologicalComplex.{v_1, u_4, u_1} C c
φ : K ⟶ L
hK : K.IsStrictlySupportedOutside e₂
hL : L.IsStrictlySupportedOutside e₁
i₁ : ι₁
⊢ φ.f (e₁.f i₁) = HomologicalComplex.Hom.f 0 (e₁.f i₁)

Tactic:
apply (hL.isZero i₁).eq_of_tgt

Premises used: HomologicalComplex.IsStrictlySupportedOutside.isZero, CategoryTheory.Limits.IsZero.eq_of_tgt
-- Module: Mathlib.Algebra.Homology.Embedding.AreComplementary
Goal:
ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
C : Type u_4
inst : Category.{v_1, u_4} C
inst_1 : HasZeroMorphisms.{v_1, u_4} C
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
K L : HomologicalComplex.{v_1, u_4, u_1} C c
φ : K ⟶ L
hK : K.IsStrictlySupportedOutside e₂
hL : L.IsStrictlySupportedOutside e₁
i₂ : ι₂
⊢ φ.f (e₂.f i₂) = HomologicalComplex.Hom.f 0 (e₂.f i₂)

Tactic:
apply (hK.isZero i₂).eq_of_src

Premises used: HomologicalComplex.IsStrictlySupportedOutside.isZero, CategoryTheory.Limits.IsZero.eq_of_src
-- Module: Mathlib.Algebra.Homology.Embedding.AreComplementary
Goal:
ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
C : Type u_4
inst : Category.{v_1, u_4} C
inst_1 : HasZeroMorphisms.{v_1, u_4} C
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
K L : HomologicalComplex.{v_1, u_4, u_1} C c
inst_2 : K.IsStrictlySupported e₁
inst_3 : L.IsStrictlySupported e₂
φ : K ⟶ L
hK : K.IsStrictlySupportedOutside e₂
hL : L.IsStrictlySupportedOutside e₁
⊢ φ = 0

Tactic:
apply ac.hom_ext'

Premises used: ComplexShape.Embedding.AreComplementary.hom_ext'
-- Module: Mathlib.Algebra.Homology.Embedding.AreComplementary
Goal:
ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
C : Type u_4
inst : Category.{v_1, u_4} C
inst_1 : HasZeroMorphisms.{v_1, u_4} C
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
K L : HomologicalComplex.{v_1, u_4, u_1} C c
inst_2 : K.IsStrictlySupported e₁
inst_3 : L.IsStrictlySupported e₂
φ : K ⟶ L
hK : K.IsStrictlySupported e₁
⊢ K.IsStrictlySupportedOutside e₂

Tactic:
rw [ac.isStrictlySupportedOutside₂_iff]

Premises used: ComplexShape.Embedding.AreComplementary.isStrictlySupportedOutside₂_iff
-- Module: Mathlib.Algebra.Homology.Embedding.AreComplementary
Goal:
ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
C : Type u_4
inst : Category.{v_1, u_4} C
inst_1 : HasZeroMorphisms.{v_1, u_4} C
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
K L : HomologicalComplex.{v_1, u_4, u_1} C c
inst_2 : K.IsStrictlySupported e₁
inst_3 : L.IsStrictlySupported e₂
φ : K ⟶ L
⊢ K.IsStrictlySupported e₁

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.Embedding.AreComplementary
Goal:
ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
C : Type u_4
inst : Category.{v_1, u_4} C
inst_1 : HasZeroMorphisms.{v_1, u_4} C
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
K L : HomologicalComplex.{v_1, u_4, u_1} C c
inst_2 : K.IsStrictlySupported e₁
inst_3 : L.IsStrictlySupported e₂
φ : K ⟶ L
hL : L.IsStrictlySupported e₂
⊢ L.IsStrictlySupportedOutside e₁

Tactic:
rw [ac.isStrictlySupportedOutside₁_iff]

Premises used: ComplexShape.Embedding.AreComplementary.isStrictlySupportedOutside₁_iff