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 ι₂
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
⊢ L.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 ι₂
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
i₁ : ι₁
i₂ : ι₂
h : ac.Boundary i₁ i₂
⊢ e₁.BoundaryLE i₁

Tactic:
e₁.boundaryLE h (fun _ => ac.disjoint _ _)

Premises used: ComplexShape.Embedding.AreComplementary.disjoint, ComplexShape.Embedding.boundaryLE
-- 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₂
i₁ : ι₁
i₂ : ι₂
h : ac.Boundary i₁ i₂
⊢ e₂.BoundaryGE i₂

Tactic:
e₂.boundaryGE h (fun _ => ac.symm.disjoint _ _)

Premises used: ComplexShape.Embedding.AreComplementary.disjoint, ComplexShape.Embedding.AreComplementary.symm, ComplexShape.Embedding.boundaryGE
-- 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₂
i₁ i₁' : ι₁
i₂ : ι₂
h : ac.Boundary i₁ i₂
h' : ac.Boundary i₁' i₂
⊢ i₁ = i₁'

Tactic:
e₁.injective_f (c.prev_eq h h')

Premises used: ComplexShape.Embedding.injective_f, ComplexShape.prev_eq
-- 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₂
i₁ : ι₁
i₂ i₂' : ι₂
h : ac.Boundary i₁ i₂
h' : ac.Boundary i₁ i₂'
⊢ i₂ = i₂'

Tactic:
e₂.injective_f (c.next_eq h h')

Premises used: ComplexShape.Embedding.injective_f, ComplexShape.next_eq
-- 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₂
i₁ : ι₁
h : e₁.BoundaryLE i₁
⊢ c.Rel (e₁.f i₁) (c.next (e₁.f i₁))

Tactic:
obtain ⟨h₁, h₂⟩ := 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₂
i₁ : ι₁
h : e₁.BoundaryLE i₁
h₁ : c.Rel (e₁.f i₁) (c.next (e₁.f i₁))
⊢ ∀ (k : ι₁), ¬c.Rel (e₁.f i₁) (e₁.f k)

Tactic:
obtain ⟨h₁, h₂⟩ := 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₂
i₁ : ι₁
h₁ : c.Rel (e₁.f i₁) (c.next (e₁.f i₁))
h₂ : ∀ (k : ι₁), ¬c.Rel (e₁.f i₁) (e₁.f k)
i₁' : ι₁
hi₁' : e₁.f i₁' = c.next (e₁.f i₁)
⊢ c.Rel (e₁.f i₁) (e₁.f i₁')

Tactic:
simpa only [← hi₁'] using 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₂
i₁ : ι₁
h₁ : c.Rel (e₁.f i₁) (c.next (e₁.f i₁))
h₂ : ∀ (k : ι₁), ¬c.Rel (e₁.f i₁) (e₁.f k)
obtain : ∀ (i₂ : ι₂) (hi₂ : c.next (e₁.f i₁) = e₂.f i₂), ∃ (i₂ : ι₂), ac.Boundary i₁ i₂
⊢ ∃ (i₂ : ι₂), ac.Boundary i₁ i₂

Tactic:
obtain ⟨i₂, hi₂⟩ := ac.exists_i₂ (c.next (e₁.f i₁))
    (fun i₁' hi₁' => h₂ i₁' (by simpa only [← hi₁'] using h₁))

Premises used: ComplexShape.Embedding.AreComplementary.exists_i₂, ComplexShape.next, 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 ι₂
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
i₁ : ι₁
h₁ : c.Rel (e₁.f i₁) (c.next (e₁.f i₁))
h₂ : ∀ (k : ι₁), ¬c.Rel (e₁.f i₁) (e₁.f k)
i₂ : ι₂
hi₂ : c.next (e₁.f i₁) = e₂.f i₂
⊢ ac.Boundary i₁ i₂

Tactic:
simpa only [hi₂] using 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₂
i₁ : ι₁
h₁ : c.Rel (e₁.f i₁) (c.next (e₁.f i₁))
h₂ : ∀ (k : ι₁), ¬c.Rel (e₁.f i₁) (e₁.f k)
i₂ : ι₂
hi₂ : c.next (e₁.f i₁) = e₂.f i₂
⊢ ∃ (i₂ : ι₂), ac.Boundary i₁ i₂

Tactic:
exact ⟨i₂, by simpa only [hi₂] using 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₂
i₂ : ι₂
h : e₂.BoundaryGE i₂
⊢ c.Rel (c.prev (e₂.f i₂)) (e₂.f i₂)

Tactic:
obtain ⟨h₁, h₂⟩ := 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₂
i₂ : ι₂
h : e₂.BoundaryGE i₂
h₁ : c.Rel (c.prev (e₂.f i₂)) (e₂.f i₂)
⊢ ∀ (i : ι₂), ¬c.Rel (e₂.f i) (e₂.f i₂)

Tactic:
obtain ⟨h₁, h₂⟩ := 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₂
i₂ : ι₂
h₁ : c.Rel (c.prev (e₂.f i₂)) (e₂.f i₂)
h₂ : ∀ (i : ι₂), ¬c.Rel (e₂.f i) (e₂.f i₂)
i₂' : ι₂
hi₂' : e₂.f i₂' = c.prev (e₂.f i₂)
⊢ c.Rel (e₂.f i₂') (e₂.f i₂)

Tactic:
simpa only [← hi₂'] using 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₂
i₂ : ι₂
h₁ : c.Rel (c.prev (e₂.f i₂)) (e₂.f i₂)
h₂ : ∀ (i : ι₂), ¬c.Rel (e₂.f i) (e₂.f i₂)
obtain : ∀ (i₁ : ι₁) (hi₁ : c.prev (e₂.f i₂) = e₁.f i₁), ∃ (i₁ : ι₁), ac.Boundary i₁ i₂
⊢ ∃ (i₁ : ι₁), ac.Boundary i₁ i₂

Tactic:
obtain ⟨i₁, hi₁⟩ := ac.exists_i₁ (c.prev (e₂.f i₂))
    (fun i₂' hi₂' => h₂ i₂' (by simpa only [← hi₂'] using h₁))

Premises used: ComplexShape.Embedding.AreComplementary.exists_i₁, ComplexShape.prev, 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 ι₂
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
i₂ : ι₂
h₁ : c.Rel (c.prev (e₂.f i₂)) (e₂.f i₂)
h₂ : ∀ (i : ι₂), ¬c.Rel (e₂.f i) (e₂.f i₂)
i₁ : ι₁
hi₁ : c.prev (e₂.f i₂) = e₁.f i₁
⊢ ac.Boundary i₁ i₂

Tactic:
simpa only [hi₁] using 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₂
i₂ : ι₂
h₁ : c.Rel (c.prev (e₂.f i₂)) (e₂.f i₂)
h₂ : ∀ (i : ι₂), ¬c.Rel (e₂.f i) (e₂.f i₂)
i₁ : ι₁
hi₁ : c.prev (e₂.f i₂) = e₁.f i₁
⊢ ∃ (i₁ : ι₁), ac.Boundary i₁ i₂

Tactic:
exact ⟨i₁, by simpa only [hi₁] using 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₂
i₁ : ι₁
h : e₁.BoundaryLE i₁
⊢ ac.Boundary i₁ (indexOfBoundaryLE ac h)

Tactic:
(exists₁ ac h).choose_spec

Premises used: Exists.choose_spec, ComplexShape.Embedding.AreComplementary.Boundary.indexOfBoundaryLE, ComplexShape.Embedding.AreComplementary.Boundary.exists₁
-- 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₂
i₂ : ι₂
h : e₂.BoundaryGE i₂
⊢ ac.Boundary (indexOfBoundaryGE ac h) i₂

Tactic:
(exists₂ ac h).choose_spec

Premises used: Exists.choose_spec, ComplexShape.Embedding.AreComplementary.Boundary.indexOfBoundaryGE, ComplexShape.Embedding.AreComplementary.Boundary.exists₂
-- 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
x : Subtype e₁.BoundaryLE
i₁ : ι₁
h : e₁.BoundaryLE i₁
a :
  (↑((fun (x : Subtype e₂.BoundaryGE) ↦
            (match (motive := Subtype e₂.BoundaryGE → Subtype e₁.BoundaryLE) x with
              | ⟨i₂, h⟩ => Subtype.mk (p := e₁.BoundaryLE) (indexOfBoundaryGE ac h) ⋯ :
              Subtype e₁.BoundaryLE))
          ((fun (x : Subtype e₁.BoundaryLE) ↦
              (match (motive := Subtype e₁.BoundaryLE → Subtype e₂.BoundaryGE) x with
                | ⟨i₁, h⟩ => Subtype.mk (p := e₂.BoundaryGE) (indexOfBoundaryLE ac h) ⋯ :
                Subtype e₂.BoundaryGE))
            (Subtype.mk (p := e₁.BoundaryLE) i₁ h))) :
      ι₁) =
    (↑(Subtype.mk (p := e₁.BoundaryLE) i₁ h) : ι₁)
⊢ (fun (x : Subtype e₂.BoundaryGE) ↦
        (match (motive := Subtype e₂.BoundaryGE → Subtype e₁.BoundaryLE) x with
          | ⟨i₂, h⟩ => Subtype.mk (p := e₁.BoundaryLE) (indexOfBoundaryGE ac h) ⋯ :
          Subtype e₁.BoundaryLE))
      ((fun (x : Subtype e₁.BoundaryLE) ↦
          (match (motive := Subtype e₁.BoundaryLE → Subtype e₂.BoundaryGE) x with
            | ⟨i₁, h⟩ => Subtype.mk (p := e₂.BoundaryGE) (indexOfBoundaryLE ac h) ⋯ :
            Subtype e₂.BoundaryGE))
        (Subtype.mk (p := e₁.BoundaryLE) i₁ h)) =
    Subtype.mk (p := e₁.BoundaryLE) i₁ h

Tactic:
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
x : Subtype e₁.BoundaryLE
i₁ : ι₁
h : e₁.BoundaryLE i₁
⊢ ac.Boundary i₁ (indexOfBoundaryLE ac h)

Tactic:
have h' := of_boundaryLE ac 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₂
K L : HomologicalComplex.{v_1, u_4, u_1} C c
x : Subtype e₁.BoundaryLE
i₁ : ι₁
h : e₁.BoundaryLE i₁
h' : ac.Boundary i₁ (indexOfBoundaryLE ac h)
⊢ ac.Boundary (indexOfBoundaryGE ac ⋯) (indexOfBoundaryLE ac h)

Tactic:
have h'' := of_boundaryGE ac h'.snd
-- 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
x : Subtype e₁.BoundaryLE
i₁ : ι₁
h : e₁.BoundaryLE i₁
h' : ac.Boundary i₁ (indexOfBoundaryLE ac h)
h'' : ac.Boundary (indexOfBoundaryGE ac ⋯) (indexOfBoundaryLE ac h)
⊢ (↑((fun (x : Subtype e₂.BoundaryGE) ↦
            (match (motive := Subtype e₂.BoundaryGE → Subtype e₁.BoundaryLE) x with
              | ⟨i₂, h⟩ => Subtype.mk (p := e₁.BoundaryLE) (indexOfBoundaryGE ac h) ⋯ :
              Subtype e₁.BoundaryLE))
          ((fun (x : Subtype e₁.BoundaryLE) ↦
              (match (motive := Subtype e₁.BoundaryLE → Subtype e₂.BoundaryGE) x with
                | ⟨i₁, h⟩ => Subtype.mk (p := e₂.BoundaryGE) (indexOfBoundaryLE ac h) ⋯ :
                Subtype e₂.BoundaryGE))
            (Subtype.mk (p := e₁.BoundaryLE) i₁ h))) :
      ι₁) =
    (↑(Subtype.mk (p := e₁.BoundaryLE) i₁ h) : ι₁)

Tactic:
fst_inj h'' h'

Premises used: ComplexShape.Embedding.AreComplementary.Boundary.fst_inj
-- 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
x : Subtype e₁.BoundaryLE
i₁ : ι₁
h : e₁.BoundaryLE i₁
h' : ac.Boundary i₁ (indexOfBoundaryLE ac h)
h'' : ac.Boundary (indexOfBoundaryGE ac ⋯) (indexOfBoundaryLE ac h)
⊢ (↑((fun (x : Subtype e₂.BoundaryGE) ↦
            (match (motive := Subtype e₂.BoundaryGE → Subtype e₁.BoundaryLE) x with
              | ⟨i₂, h⟩ => Subtype.mk (p := e₁.BoundaryLE) (indexOfBoundaryGE ac h) ⋯ :
              Subtype e₁.BoundaryLE))
          ((fun (x : Subtype e₁.BoundaryLE) ↦
              (match (motive := Subtype e₁.BoundaryLE → Subtype e₂.BoundaryGE) x with
                | ⟨i₁, h⟩ => Subtype.mk (p := e₂.BoundaryGE) (indexOfBoundaryLE ac h) ⋯ :
                Subtype e₂.BoundaryGE))
            (Subtype.mk (p := e₁.BoundaryLE) i₁ h))) :
      ι₁) =
    (↑(Subtype.mk (p := e₁.BoundaryLE) i₁ h) : ι₁)

Tactic:
exact fst_inj h'' h'

Premises used: ComplexShape.Embedding.AreComplementary.Boundary.fst_inj
-- 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
x : Subtype e₂.BoundaryGE
i₂ : ι₂
h : e₂.BoundaryGE i₂
a :
  (↑((fun (x : Subtype e₁.BoundaryLE) ↦
            (match (motive := Subtype e₁.BoundaryLE → Subtype e₂.BoundaryGE) x with
              | ⟨i₁, h⟩ => Subtype.mk (p := e₂.BoundaryGE) (indexOfBoundaryLE ac h) ⋯ :
              Subtype e₂.BoundaryGE))
          ((fun (x : Subtype e₂.BoundaryGE) ↦
              (match (motive := Subtype e₂.BoundaryGE → Subtype e₁.BoundaryLE) x with
                | ⟨i₂, h⟩ => Subtype.mk (p := e₁.BoundaryLE) (indexOfBoundaryGE ac h) ⋯ :
                Subtype e₁.BoundaryLE))
            (Subtype.mk (p := e₂.BoundaryGE) i₂ h))) :
      ι₂) =
    (↑(Subtype.mk (p := e₂.BoundaryGE) i₂ h) : ι₂)
⊢ (fun (x : Subtype e₁.BoundaryLE) ↦
        (match (motive := Subtype e₁.BoundaryLE → Subtype e₂.BoundaryGE) x with
          | ⟨i₁, h⟩ => Subtype.mk (p := e₂.BoundaryGE) (indexOfBoundaryLE ac h) ⋯ :
          Subtype e₂.BoundaryGE))
      ((fun (x : Subtype e₂.BoundaryGE) ↦
          (match (motive := Subtype e₂.BoundaryGE → Subtype e₁.BoundaryLE) x with
            | ⟨i₂, h⟩ => Subtype.mk (p := e₁.BoundaryLE) (indexOfBoundaryGE ac h) ⋯ :
            Subtype e₁.BoundaryLE))
        (Subtype.mk (p := e₂.BoundaryGE) i₂ h)) =
    Subtype.mk (p := e₂.BoundaryGE) i₂ h

Tactic:
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
x : Subtype e₂.BoundaryGE
i₂ : ι₂
h : e₂.BoundaryGE i₂
⊢ ac.Boundary (indexOfBoundaryGE ac h) i₂

Tactic:
have h' := of_boundaryGE ac 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₂
K L : HomologicalComplex.{v_1, u_4, u_1} C c
x : Subtype e₂.BoundaryGE
i₂ : ι₂
h : e₂.BoundaryGE i₂
h' : ac.Boundary (indexOfBoundaryGE ac h) i₂
⊢ ac.Boundary (indexOfBoundaryGE ac h) (indexOfBoundaryLE ac ⋯)

Tactic:
have h'' := of_boundaryLE ac h'.fst
-- 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
x : Subtype e₂.BoundaryGE
i₂ : ι₂
h : e₂.BoundaryGE i₂
h' : ac.Boundary (indexOfBoundaryGE ac h) i₂
h'' : ac.Boundary (indexOfBoundaryGE ac h) (indexOfBoundaryLE ac ⋯)
⊢ (↑((fun (x : Subtype e₁.BoundaryLE) ↦
            (match (motive := Subtype e₁.BoundaryLE → Subtype e₂.BoundaryGE) x with
              | ⟨i₁, h⟩ => Subtype.mk (p := e₂.BoundaryGE) (indexOfBoundaryLE ac h) ⋯ :
              Subtype e₂.BoundaryGE))
          ((fun (x : Subtype e₂.BoundaryGE) ↦
              (match (motive := Subtype e₂.BoundaryGE → Subtype e₁.BoundaryLE) x with
                | ⟨i₂, h⟩ => Subtype.mk (p := e₁.BoundaryLE) (indexOfBoundaryGE ac h) ⋯ :
                Subtype e₁.BoundaryLE))
            (Subtype.mk (p := e₂.BoundaryGE) i₂ h))) :
      ι₂) =
    (↑(Subtype.mk (p := e₂.BoundaryGE) i₂ h) : ι₂)

Tactic:
snd_inj h'' h'

Premises used: ComplexShape.Embedding.AreComplementary.Boundary.snd_inj
-- 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
x : Subtype e₂.BoundaryGE
i₂ : ι₂
h : e₂.BoundaryGE i₂
h' : ac.Boundary (indexOfBoundaryGE ac h) i₂
h'' : ac.Boundary (indexOfBoundaryGE ac h) (indexOfBoundaryLE ac ⋯)
⊢ (↑((fun (x : Subtype e₁.BoundaryLE) ↦
            (match (motive := Subtype e₁.BoundaryLE → Subtype e₂.BoundaryGE) x with
              | ⟨i₁, h⟩ => Subtype.mk (p := e₂.BoundaryGE) (indexOfBoundaryLE ac h) ⋯ :
              Subtype e₂.BoundaryGE))
          ((fun (x : Subtype e₂.BoundaryGE) ↦
              (match (motive := Subtype e₂.BoundaryGE → Subtype e₁.BoundaryLE) x with
                | ⟨i₂, h⟩ => Subtype.mk (p := e₁.BoundaryLE) (indexOfBoundaryGE ac h) ⋯ :
                Subtype e₁.BoundaryLE))
            (Subtype.mk (p := e₂.BoundaryGE) i₂ h))) :
      ι₂) =
    (↑(Subtype.mk (p := e₂.BoundaryGE) i₂ h) : ι₂)

Tactic:
exact snd_inj h'' h'

Premises used: ComplexShape.Embedding.AreComplementary.Boundary.snd_inj
-- Module: Mathlib.Algebra.Homology.Embedding.AreComplementary
Goal:
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
i₁ i₂ : ℕ
⊢ ¬n₀ - (↑i₁ : ℤ) = n₁ + (↑i₂ : ℤ)

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.Embedding.AreComplementary
Goal:
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
i : ℤ
pos : ∀ (hi : i ≤ n₀), (∃ (i₁ : ℕ), (embeddingUpIntLE n₀).f i₁ = i) ∨ ∃ (i₂ : ℕ), (embeddingUpIntGE n₁).f i₂ = i
neg : ∀ (hi : ¬i ≤ n₀), (∃ (i₁ : ℕ), (embeddingUpIntLE n₀).f i₁ = i) ∨ ∃ (i₂ : ℕ), (embeddingUpIntGE n₁).f i₂ = i
⊢ (∃ (i₁ : ℕ), (embeddingUpIntLE n₀).f i₁ = i) ∨ ∃ (i₂ : ℕ), (embeddingUpIntGE n₁).f i₂ = i

Tactic:
by_cases hi : i ≤ n₀
-- Module: Mathlib.Algebra.Homology.Embedding.AreComplementary
Goal:
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
i : ℤ
hi : i ≤ n₀
pos :
  ∀ (k : ℕ) (h : i + (↑k : ℤ) + 1 = n₁) (hi : i ≤ i + (↑k : ℤ)),
    (∃ (i₁ : ℕ), (embeddingUpIntLE (i + (↑k : ℤ))).f i₁ = i) ∨ ∃ (i₂ : ℕ), (embeddingUpIntGE n₁).f i₂ = i
⊢ (∃ (i₁ : ℕ), (embeddingUpIntLE n₀).f i₁ = i) ∨ ∃ (i₂ : ℕ), (embeddingUpIntGE n₁).f i₂ = i

Tactic:
obtain ⟨k, rfl⟩ := Int.exists_add_of_le hi

Premises used: Int.exists_add_of_le, rfl
-- Module: Mathlib.Algebra.Homology.Embedding.AreComplementary
Goal:
n₁ i : ℤ
k : ℕ
h : i + (↑k : ℤ) + 1 = n₁
hi : i ≤ i + (↑k : ℤ)
⊢ i + (↑k : ℤ) - (↑k : ℤ) = i

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.Embedding.AreComplementary
Goal:
n₁ i : ℤ
k : ℕ
h : i + (↑k : ℤ) + 1 = n₁
hi : i ≤ i + (↑k : ℤ)
⊢ (∃ (i₁ : ℕ), (embeddingUpIntLE (i + (↑k : ℤ))).f i₁ = i) ∨ ∃ (i₂ : ℕ), (embeddingUpIntGE n₁).f i₂ = i

Tactic:
exact Or.inl ⟨k, by dsimp; lia⟩

Premises used: Or.inl
-- Module: Mathlib.Algebra.Homology.Embedding.AreComplementary
Goal:
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
i : ℤ
hi : ¬i ≤ n₀
⊢ n₁ ≤ i

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.Embedding.AreComplementary
Goal:
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
i : ℤ
hi : ¬i ≤ n₀
neg :
  ∀ (k : ℕ) (hi : ¬n₁ + (↑k : ℤ) ≤ n₀),
    (∃ (i₁ : ℕ), (embeddingUpIntLE n₀).f i₁ = n₁ + (↑k : ℤ)) ∨ ∃ (i₂ : ℕ), (embeddingUpIntGE n₁).f i₂ = n₁ + (↑k : ℤ)
⊢ (∃ (i₁ : ℕ), (embeddingUpIntLE n₀).f i₁ = i) ∨ ∃ (i₂ : ℕ), (embeddingUpIntGE n₁).f i₂ = i

Tactic:
obtain ⟨k, rfl⟩ := Int.exists_add_of_le (show n₁ ≤ i by lia)

Premises used: Int.exists_add_of_le, rfl
-- Module: Mathlib.Algebra.Homology.Embedding.AreComplementary
Goal:
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
k : ℕ
hi : ¬n₁ + (↑k : ℤ) ≤ n₀
⊢ (∃ (i₁ : ℕ), (embeddingUpIntLE n₀).f i₁ = n₁ + (↑k : ℤ)) ∨ ∃ (i₂ : ℕ), (embeddingUpIntGE n₁).f i₂ = n₁ + (↑k : ℤ)

Tactic:
Or.inr ⟨k, rfl⟩

Premises used: Exists.intro, Or.inr, rfl
-- Module: Mathlib.Algebra.Homology.Embedding.AreComplementary
Goal:
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
k : ℕ
hi : ¬n₁ + (↑k : ℤ) ≤ n₀
⊢ (∃ (i₁ : ℕ), (embeddingUpIntLE n₀).f i₁ = n₁ + (↑k : ℤ)) ∨ ∃ (i₂ : ℕ), (embeddingUpIntGE n₁).f i₂ = n₁ + (↑k : ℤ)

Tactic:
exact Or.inr ⟨k, rfl⟩

Premises used: Or.inr
-- 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 : Abelian.{v_1, u_4} C
K : HomologicalComplex.{v_1, u_4, u_1} C c
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
inst_2 : e₁.IsTruncLE
inst_3 : e₂.IsTruncGE
ac : e₁.AreComplementary e₂
⊢ Eq (α := (K.shortComplexTruncLE e₁).X₂ ⟶ K.truncGE e₂)
    ((K.shortComplexTruncLE e₁).g ≫ K.shortComplexTruncLEX₃ToTruncGE ac) (K.πTruncGE e₂)

Tactic:
cokernel.π_desc _ _ _

Premises used: CategoryTheory.Limits.colimit, CategoryTheory.Limits.cokernel.π_desc, HomologicalComplex.shortComplexTruncLEX₃ToTruncGE, CategoryTheory.Limits.colimit.ι
-- 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 : Abelian.{v_1, u_4} C
K : HomologicalComplex.{v_1, u_4, u_1} C c
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
inst_2 : e₁.IsTruncLE
inst_3 : e₂.IsTruncGE
ac : e₁.AreComplementary e₂
i : ι
inl :
  ∀ (i₁ : ι₁),
    QuasiIsoAt (K := (K.shortComplexTruncLE e₁).X₃) (L := K.truncGE e₂) (K.shortComplexTruncLEX₃ToTruncGE ac) (e₁.f i₁)
inr :
  ∀ (i₂ : ι₂),
    QuasiIsoAt (K := (K.shortComplexTruncLE e₁).X₃) (L := K.truncGE e₂) (K.shortComplexTruncLEX₃ToTruncGE ac) (e₂.f i₂)
⊢ QuasiIsoAt (K := (K.shortComplexTruncLE e₁).X₃) (L := K.truncGE e₂) (K.shortComplexTruncLEX₃ToTruncGE ac) 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 : Abelian.{v_1, u_4} C
K : HomologicalComplex.{v_1, u_4, u_1} C c
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
inst_2 : e₁.IsTruncLE
inst_3 : e₂.IsTruncGE
ac : e₁.AreComplementary e₂
i₁ : ι₁
⊢ (K.truncGE e₂).ExactAt (e₁.f i₁)

Tactic:
have h₁ := ((ac.isSupportedOutside₁_iff (K.truncGE e₂)).2 inferInstance).exactAt i₁