awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.Double
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₀ i₁ : ι
hi₀₁ : c.Rel i₀ i₁
h : i₀ ≠ i₁
X : C
K : HomologicalComplex.{v_1, u_1, u_2} C c
g : double (𝟙 X) hi₀₁ ⟶ K
h₀ :
  Hom.f
      ((fun (φ₀ : Functor.obj (eval C c i₀ ⋙ Functor.obj coyoneda (op X)) K) ↦
          (mkHomFromDouble hi₀₁ h φ₀ (φ₀ ≫ K.d i₀ i₁) ⋯ ⋯ : double (𝟙 X) hi₀₁ ⟶ K))
        ((fun (g : double (𝟙 X) hi₀₁ ⟶ K) ↦ Iso.inv (doubleXIso₀ (𝟙 X) hi₀₁) ≫ g.f i₀) g))
      i₀ =
    g.f i₀
h₁ :
  Hom.f
      ((fun (φ₀ : Functor.obj (eval C c i₀ ⋙ Functor.obj coyoneda (op X)) K) ↦
          (mkHomFromDouble hi₀₁ h φ₀ (φ₀ ≫ K.d i₀ i₁) ⋯ ⋯ : double (𝟙 X) hi₀₁ ⟶ K))
        ((fun (g : double (𝟙 X) hi₀₁ ⟶ K) ↦ Iso.inv (doubleXIso₀ (𝟙 X) hi₀₁) ≫ g.f i₀) g))
      i₁ =
    g.f i₁
⊢ (fun (φ₀ : Functor.obj (eval C c i₀ ⋙ Functor.obj coyoneda (op X)) K) ↦
        (mkHomFromDouble hi₀₁ h φ₀ (φ₀ ≫ K.d i₀ i₁) ⋯ ⋯ : double (𝟙 X) hi₀₁ ⟶ K))
      ((fun (g : double (𝟙 X) hi₀₁ ⟶ K) ↦ Iso.inv (doubleXIso₀ (𝟙 X) hi₀₁) ≫ g.f i₀) g) =
    g

Tactic:
ext
-- Module: Mathlib.Algebra.Homology.Double
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₀ i₁ : ι
hi₀₁ : c.Rel i₀ i₁
h : i₀ ≠ i₁
X : C
K : HomologicalComplex.{v_1, u_1, u_2} C c
g : double (𝟙 X) hi₀₁ ⟶ K
⊢ Hom.f
      ((fun (φ₀ : Functor.obj (eval C c i₀ ⋙ Functor.obj coyoneda (op X)) K) ↦
          (mkHomFromDouble hi₀₁ h φ₀ (φ₀ ≫ K.d i₀ i₁) ⋯ ⋯ : double (𝟙 X) hi₀₁ ⟶ K))
        ((fun (g : double (𝟙 X) hi₀₁ ⟶ K) ↦ Iso.inv (doubleXIso₀ (𝟙 X) hi₀₁) ≫ g.f i₀) g))
      i₀ =
    g.f i₀

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.Double
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₀ i₁ : ι
hi₀₁ : c.Rel i₀ i₁
h : i₀ ≠ i₁
X : C
K : HomologicalComplex.{v_1, u_1, u_2} C c
g : double (𝟙 X) hi₀₁ ⟶ K
⊢ Hom.f
      ((fun (φ₀ : Functor.obj (eval C c i₀ ⋙ Functor.obj coyoneda (op X)) K) ↦
          (mkHomFromDouble hi₀₁ h φ₀ (φ₀ ≫ K.d i₀ i₁) ⋯ ⋯ : double (𝟙 X) hi₀₁ ⟶ K))
        ((fun (g : double (𝟙 X) hi₀₁ ⟶ K) ↦ Iso.inv (doubleXIso₀ (𝟙 X) hi₀₁) ≫ g.f i₀) g))
      i₁ =
    g.f i₁

Tactic:
simp [double_d _ _ h]

Premises used: HomologicalComplex.double_d
-- Module: Mathlib.Algebra.Homology.Double
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₀ i₁ : ι
hi₀₁ : c.Rel i₀ i₁
h : i₀ ≠ i₁
X : C
K : HomologicalComplex.{v_1, u_1, u_2} C c
x : Functor.obj (eval C c i₀ ⋙ Functor.obj coyoneda (op X)) K
⊢ (fun (g : double (𝟙 X) hi₀₁ ⟶ K) ↦ Iso.inv (doubleXIso₀ (𝟙 X) hi₀₁) ≫ g.f i₀)
      ((fun (φ₀ : Functor.obj (eval C c i₀ ⋙ Functor.obj coyoneda (op X)) K) ↦
          (mkHomFromDouble hi₀₁ h φ₀ (φ₀ ≫ K.d i₀ i₁) ⋯ ⋯ : double (𝟙 X) hi₀₁ ⟶ K))
        x) =
    x

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.Double
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₀ i₁ : ι
hi₀₁ : c.Rel i₀ i₁
h : i₀ ≠ i₁
X : C
Y Y' : HomologicalComplex.{v_1, u_1, u_2} C c
x : Y ⟶ Y'
x_1 : double (𝟙 X) hi₀₁ ⟶ Y
⊢ Eq.{v_1 + 1} (α := Functor.obj (eval C c i₀ ⋙ Functor.obj coyoneda (op X)) Y')
    (({ toFun := fun (g : double (𝟙 X) hi₀₁ ⟶ Y') ↦ Iso.inv (doubleXIso₀ (𝟙 X) hi₀₁) ≫ g.f i₀,
            invFun := fun (φ₀ : Functor.obj (eval C c i₀ ⋙ Functor.obj coyoneda (op X)) Y') ↦
              mkHomFromDouble hi₀₁ h φ₀ (φ₀ ≫ Y'.d i₀ i₁) ⋯ ⋯,
            left_inv := ⋯, right_inv := ⋯ } :
          (a : double (𝟙 X) hi₀₁ ⟶ Y') → (eval C c i₀ ⋙ coyoneda.obj (op X)).obj Y')
        (x_1 ≫ x) :
      Functor.obj (eval C c i₀ ⋙ Functor.obj coyoneda (op X)) Y')
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (CategoryTheory.Functor.map (eval C c i₀ ⋙ Functor.obj coyoneda (op X)) x) :
          (a : (fun (X : Type v_1) ↦ X) ((eval C c i₀ ⋙ coyoneda.obj (op X)).obj Y)) →
            (fun (X : Type v_1) ↦ X) ((eval C c i₀ ⋙ coyoneda.obj (op X)).obj Y'))
        (({ toFun := fun (g : double (𝟙 X) hi₀₁ ⟶ Y) ↦ Iso.inv (doubleXIso₀ (𝟙 X) hi₀₁) ≫ g.f i₀,
                invFun := fun (φ₀ : Functor.obj (eval C c i₀ ⋙ Functor.obj coyoneda (op X)) Y) ↦
                  mkHomFromDouble hi₀₁ h φ₀ (φ₀ ≫ Y.d i₀ i₁) ⋯ ⋯,
                left_inv := ⋯, right_inv := ⋯ } :
              (a : double (𝟙 X) hi₀₁ ⟶ Y) → (eval C c i₀ ⋙ coyoneda.obj (op X)).obj Y)
            x_1 :
          Functor.obj (eval C c i₀ ⋙ Functor.obj coyoneda (op X)) Y) :
      (fun (X : Type v_1) ↦ X) (Functor.obj (eval C c i₀ ⋙ Functor.obj coyoneda (op X)) Y'))

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.Double
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
i : ι
inst_3 : DecidableEq ι
hi : ∀ (j : ι), ¬c.Rel i j
X : C
K : HomologicalComplex.{v_1, u_1, u_2} C c
f : Functor.obj (eval C c i ⋙ Functor.obj coyoneda (op X)) K
⊢ (fun (g : Functor.obj (single C c i) X ⟶ K) ↦ Iso.inv (singleObjXSelf c i X) ≫ g.f i)
      ((fun (f : Functor.obj (eval C c i ⋙ Functor.obj coyoneda (op X)) K) ↦
          (mkHomFromSingle f ⋯ : Functor.obj (single C c i) X ⟶ K))
        f) =
    f

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.Double
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
i : ι
inst_3 : DecidableEq ι
hi : ∀ (j : ι), ¬c.Rel i j
X : C
⊢ ∀ {Y Y' : HomologicalComplex.{v_1, u_1, u_2} C c} (g : Y ⟶ Y') (f : Functor.obj (single C c i) X ⟶ Y),
    Eq.{v_1 + 1} (α := Functor.obj (eval C c i ⋙ Functor.obj coyoneda (op X)) Y')
      (({ toFun := fun (g : Functor.obj (single C c i) X ⟶ Y') ↦ Iso.inv (singleObjXSelf c i X) ≫ g.f i,
              invFun := fun (f : Functor.obj (eval C c i ⋙ Functor.obj coyoneda (op X)) Y') ↦ mkHomFromSingle f ⋯,
              left_inv := ⋯, right_inv := ⋯ } :
            (a : (single C c i).obj X ⟶ Y') → (eval C c i ⋙ coyoneda.obj (op X)).obj Y')
          (f ≫ g) :
        Functor.obj (eval C c i ⋙ Functor.obj coyoneda (op X)) Y')
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (CategoryTheory.Functor.map (eval C c i ⋙ Functor.obj coyoneda (op X)) g) :
            (a : (fun (X : Type v_1) ↦ X) ((eval C c i ⋙ coyoneda.obj (op X)).obj Y)) →
              (fun (X : Type v_1) ↦ X) ((eval C c i ⋙ coyoneda.obj (op X)).obj Y'))
          (({ toFun := fun (g : Functor.obj (single C c i) X ⟶ Y) ↦ Iso.inv (singleObjXSelf c i X) ≫ g.f i,
                  invFun := fun (f : Functor.obj (eval C c i ⋙ Functor.obj coyoneda (op X)) Y) ↦ mkHomFromSingle f ⋯,
                  left_inv := ⋯, right_inv := ⋯ } :
                (a : (single C c i).obj X ⟶ Y) → (eval C c i ⋙ coyoneda.obj (op X)).obj Y)
              f :
            Functor.obj (eval C c i ⋙ Functor.obj coyoneda (op X)) Y) :
        (fun (X : Type v_1) ↦ X) (Functor.obj (eval C c i ⋙ Functor.obj coyoneda (op X)) Y'))

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.Double
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
inst_3 : c.HasNoLoop
X : C
j : ι
pos :
  (h : ∃ (k : ι), c.Rel j k) →
    Functor.CorepresentableBy (C := HomologicalComplex.{v_1, u_1, u_2} C c) (eval C c j ⋙ Functor.obj coyoneda (op X))
      (double (𝟙 X) ⋯)
neg :
  (h : ¬∃ (k : ι), c.Rel j k) →
    Functor.CorepresentableBy (C := HomologicalComplex.{v_1, u_1, u_2} C c) (eval C c j ⋙ Functor.obj coyoneda (op X))
      (Functor.obj (single C c j) X)
⊢ Functor.CorepresentableBy (C := HomologicalComplex.{v_1, u_1, u_2} C c) (eval C c j ⋙ Functor.obj coyoneda (op X))
    (if hj : ∃ (k : ι), c.Rel j k then double (𝟙 X) ⋯ else Functor.obj (single C c j) X)

Tactic:
split_ifs with h
-- Module: Mathlib.Algebra.Homology.Double
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
inst_3 : c.HasNoLoop
X : C
j : ι
h : ∃ (k : ι), c.Rel j k
⊢ Functor.CorepresentableBy (C := HomologicalComplex.{v_1, u_1, u_2} C c) (eval C c j ⋙ Functor.obj coyoneda (op X))
    (double (𝟙 X) ⋯)

Tactic:
exact evalCompCoyonedaCorepresentableByDoubleId _
      (fun hj ↦ c.not_rel_of_eq hj h.choose_spec) _

Premises used: Exists.choose_spec, ComplexShape.not_rel_of_eq, HomologicalComplex.evalCompCoyonedaCorepresentableByDoubleId
-- Module: Mathlib.Algebra.Homology.Double
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
inst_3 : c.HasNoLoop
X : C
j : ι
h : ¬∃ (k : ι), c.Rel j k
neg : ∀ (j_1 : ι), ¬c.Rel j j_1
⊢ Functor.CorepresentableBy (C := HomologicalComplex.{v_1, u_1, u_2} C c) (eval C c j ⋙ Functor.obj coyoneda (op X))
    (Functor.obj (single C c j) X)

Tactic:
apply evalCompCoyonedaCorepresentableBySingle

Premises used: HomologicalComplex.evalCompCoyonedaCorepresentableBySingle
-- Module: Mathlib.Algebra.Homology.Double
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
inst_3 : c.HasNoLoop
X : C
j : ι
h : ¬∃ (k : ι), c.Rel j k
neg : (∃ (k : ι), c.Rel j k ∧ j ≠ k) → ∀ (j_1 : ι), ¬c.Rel j j_1
neg₁ : (∀ (k : ι), ¬c.Rel j k) → ∀ (j_1 : ι), ¬c.Rel j j_1
⊢ ∀ (j_1 : ι), ¬c.Rel j j_1

Tactic:
obtain _ | _ := c.exists_distinct_prev_or j

Premises used: ComplexShape.exists_distinct_prev_or
-- Module: Mathlib.Algebra.Homology.Double
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
inst_3 : c.HasNoLoop
X : C
j : ι
h : ¬∃ (k : ι), c.Rel j k
h_1 : ∃ (k : ι), c.Rel j k ∧ j ≠ k
neg neg₁ : ∀ (j_1 w : ι), c.Rel j w → j ≠ w → ¬c.Rel j j_1
neg₂ neg₃ neg₄ neg₅ neg₆ neg₇ : ∀ (j_1 w : ι), c.Rel j w → j ≠ w → c.Rel j j_1 → False
⊢ ∀ (j_1 : ι), ¬c.Rel j j_1

Tactic:
tauto
-- Module: Mathlib.Algebra.Homology.Double
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
inst_3 : c.HasNoLoop
X : C
j : ι
h : ¬∃ (k : ι), c.Rel j k
h_1 : ∀ (k : ι), ¬c.Rel j k
⊢ ∀ (j_1 : ι), ¬c.Rel j j_1

Tactic:
tauto
-- Module: Mathlib.Algebra.Homology.Double
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
inst_3 : c.HasNoLoop
X : C
j : ι
pos :
  (h : ∃ (k : ι), c.Rel j k) →
    Functor.CorepresentableBy (C := HomologicalComplex.{v_1, u_1, u_2} C c) (eval C c j ⋙ Functor.obj coyoneda (op X))
      (double (𝟙 X) ⋯)
neg neg₁ :
  (h : ¬∃ (k : ι), c.Rel j k) →
    Functor.CorepresentableBy (C := HomologicalComplex.{v_1, u_1, u_2} C c) (eval C c j ⋙ Functor.obj coyoneda (op X))
      (Functor.obj (single C c j) X)
⊢ Functor.CorepresentableBy (C := HomologicalComplex.{v_1, u_1, u_2} C c) (eval C c j ⋙ Functor.obj coyoneda (op X))
    (if hj : ∃ (k : ι), c.Rel j k then double (𝟙 X) ⋯ else Functor.obj (single C c j) X)

Tactic:
classical
  split_ifs with h
  · exact evalCompCoyonedaCorepresentableByDoubleId _
      (fun hj ↦ c.not_rel_of_eq hj h.choose_spec) _
  · apply evalCompCoyonedaCorepresentableBySingle
    obtain _ | _ := c.exists_distinct_prev_or j <;> tauto

Premises used: ComplexShape.exists_distinct_prev_or, HomologicalComplex.evalCompCoyonedaCorepresentableBySingle
-- 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 : ι
hi : ∀ (i₂ : ι₂), e₂.f i₂ ≠ i
inl : ∀ (i₁ : ι₁) (hi : ∀ (i₂ : ι₂), e₂.f i₂ ≠ e₁.f i₁), ∃ (i₁_1 : ι₁), e₁.f i₁ = e₁.f i₁_1
inr : ∀ (i₂ : ι₂) (hi : ∀ (i₂_1 : ι₂), e₂.f i₂_1 ≠ e₂.f i₂), ∃ (i₁ : ι₁), e₂.f i₂ = e₁.f i₁
⊢ ∃ (i₁ : ι₁), i = e₁.f 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 ι₂
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
i₁ : ι₁
hi : ∀ (i₂ : ι₂), e₂.f i₂ ≠ e₁.f i₁
⊢ ∃ (i₁_1 : ι₁), e₁.f i₁ = e₁.f i₁_1

Tactic:
⟨_, rfl⟩

Premises used: Exists.intro, 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₂
i₁ : ι₁
hi : ∀ (i₂ : ι₂), e₂.f i₂ ≠ e₁.f i₁
⊢ ∃ (i₁_1 : ι₁), e₁.f i₁ = e₁.f i₁_1

Tactic:
exact ⟨_, 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₂
i₂ : ι₂
hi : ∀ (i₂_1 : ι₂), e₂.f i₂_1 ≠ e₂.f i₂
inr : False
⊢ ∃ (i₁ : ι₁), e₂.f i₂ = e₁.f i₁

Tactic:
exfalso
-- 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₂ : ι₂
hi : ∀ (i₂_1 : ι₂), e₂.f i₂_1 ≠ e₂.f i₂
⊢ False

Tactic:
hi i₂ rfl

Premises used: 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₂
i₂ : ι₂
hi : ∀ (i₂_1 : ι₂), e₂.f i₂_1 ≠ e₂.f i₂
⊢ False

Tactic:
exact hi i₂ rfl

Premises used: 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₂
i : ι
hi : ∀ (i₁ : ι₁), e₁.f i₁ ≠ i
⊢ ∃ (i₂ : ι₂), i = e₂.f i₂

Tactic:
ac.symm.exists_i₁ i hi

Premises used: ComplexShape.Embedding.AreComplementary.exists_i₁, 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 ι₂
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
left : Function.Injective (fromSum e₁ e₂)
right : Function.Surjective (fromSum e₁ e₂)
⊢ Function.Bijective (fromSum e₁ 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 ι₂
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
i₁ j₁ : ι₁
h : fromSum e₁ e₂ (Sum.inl i₁) = fromSum e₁ e₂ (Sum.inl j₁)
left : ∀ (h : fromSum e₁ e₂ (Sum.inl i₁) = fromSum e₁ e₂ (Sum.inl i₁)), Eq (α := ι₁ ⊕ ι₂) (Sum.inl i₁) (Sum.inl i₁)
⊢ Eq (α := ι₁ ⊕ ι₂) (Sum.inl i₁) (Sum.inl j₁)

Tactic:
obtain rfl := e₁.injective_f h

Premises used: ComplexShape.Embedding.injective_f, 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₂
i₁ : ι₁
h : fromSum e₁ e₂ (Sum.inl i₁) = fromSum e₁ e₂ (Sum.inl i₁)
⊢ Eq (α := ι₁ ⊕ ι₂) (Sum.inl i₁) (Sum.inl 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₂
i₁ : ι₁
j₂ : ι₂
h : fromSum e₁ e₂ (Sum.inl i₁) = fromSum e₁ e₂ (Sum.inr j₂)
⊢ Sum.inl i₁ = Sum.inr j₂

Tactic:
(ac.disjoint _ _ h).elim

Premises used: False.elim, ComplexShape.Embedding.AreComplementary.disjoint
-- 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₁ : ι₁
j₂ : ι₂
h : fromSum e₁ e₂ (Sum.inl i₁) = fromSum e₁ e₂ (Sum.inr j₂)
⊢ Sum.inl i₁ = Sum.inr j₂

Tactic:
exact (ac.disjoint _ _ h).elim

Premises used: False.elim, ComplexShape.Embedding.AreComplementary.disjoint
-- 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₂ : ι₂
j₁ : ι₁
h : fromSum e₁ e₂ (Sum.inr i₂) = fromSum e₁ e₂ (Sum.inl j₁)
⊢ Sum.inr i₂ = Sum.inl j₁

Tactic:
(ac.disjoint _ _ h.symm).elim

Premises used: False.elim, ComplexShape.Embedding.AreComplementary.disjoint, Eq.symm
-- 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₂ : ι₂
j₁ : ι₁
h : fromSum e₁ e₂ (Sum.inr i₂) = fromSum e₁ e₂ (Sum.inl j₁)
⊢ Sum.inr i₂ = Sum.inl j₁

Tactic:
exact (ac.disjoint _ _ h.symm).elim

Premises used: False.elim, ComplexShape.Embedding.AreComplementary.disjoint, Eq.symm
-- 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₂ j₂ : ι₂
h : fromSum e₁ e₂ (Sum.inr i₂) = fromSum e₁ e₂ (Sum.inr j₂)
left : ∀ (h : fromSum e₁ e₂ (Sum.inr i₂) = fromSum e₁ e₂ (Sum.inr i₂)), Eq (α := ι₁ ⊕ ι₂) (Sum.inr i₂) (Sum.inr i₂)
⊢ Eq (α := ι₁ ⊕ ι₂) (Sum.inr i₂) (Sum.inr j₂)

Tactic:
obtain rfl := e₂.injective_f h

Premises used: ComplexShape.Embedding.injective_f, 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₂
i₂ : ι₂
h : fromSum e₁ e₂ (Sum.inr i₂) = fromSum e₁ e₂ (Sum.inr i₂)
⊢ Eq (α := ι₁ ⊕ ι₂) (Sum.inr i₂) (Sum.inr 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₂
n : ι
right : ∀ (i₁ : ι₁), ∃ (a : ι₁ ⊕ ι₂), fromSum e₁ e₂ a = e₁.f i₁
right₁ : ∀ (i₂ : ι₂), ∃ (a : ι₁ ⊕ ι₂), fromSum e₁ e₂ a = e₂.f i₂
⊢ ∃ (a : ι₁ ⊕ ι₂), fromSum e₁ e₂ a = n

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

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 ι₂
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
i₁ : ι₁
⊢ ∃ (a : ι₁ ⊕ ι₂), fromSum e₁ e₂ a = e₁.f i₁

Tactic:
⟨Sum.inl i₁, rfl⟩

Premises used: Sum.inl, Exists.intro, 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₂
i₁ : ι₁
⊢ ∃ (a : ι₁ ⊕ ι₂), fromSum e₁ e₂ a = e₁.f i₁

Tactic:
exact ⟨Sum.inl i₁, 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₂
i₂ : ι₂
⊢ ∃ (a : ι₁ ⊕ ι₂), fromSum e₁ e₂ a = e₂.f i₂

Tactic:
⟨Sum.inr i₂, rfl⟩

Premises used: Sum.inr, Exists.intro, 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₂
i₂ : ι₂
⊢ ∃ (a : ι₁ ⊕ ι₂), fromSum e₁ e₂ a = e₂.f i₂

Tactic:
exact ⟨Sum.inr i₂, 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₂
i₁ : ι₁
⊢ (ac.equiv : (a : ι₁ ⊕ ι₂) → ι) (Sum.inl i₁) = e₁.f i₁

Tactic:
rfl

Premises used: ComplexShape.Embedding.AreComplementary.fromSum, 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₂
i₂ : ι₂
⊢ (ac.equiv : (a : ι₁ ⊕ ι₂) → ι) (Sum.inr i₂) = e₂.f i₂

Tactic:
rfl

Premises used: ComplexShape.Embedding.AreComplementary.fromSum, 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 j : ι
hij : i = j
subst : X i ≃ X i
⊢ X i ≃ X j

Tactic:
subst hij
-- 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 : ι
⊢ X i ≃ X i

Tactic:
rfl
-- Module: Mathlib.Algebra.Homology.Embedding.AreComplementary
Goal:
ι : Type u_1
X : ι → Type u_5
i j k : ι
hij : i = j
hjk : j = k
x : X i
subst :
  Eq (α := X i) ((aux X i i ⋯ : (a : X i) → X i) ((aux X i i ⋯ : (a : X i) → X i) x : X i) : X i)
    ((aux X i i ⋯ : (a : X i) → X i) x : X i)
⊢ Eq (α := X k) ((aux X j k hjk : (a : X j) → X k) ((aux X i j hij : (a : X i) → X j) x : X j) : X k)
    ((aux X i k ⋯ : (a : X i) → X k) x : X k)

Tactic:
subst hij hjk
-- Module: Mathlib.Algebra.Homology.Embedding.AreComplementary
Goal:
ι : Type u_1
X : ι → Type u_5
i : ι
x : X i
⊢ Eq (α := X i) ((aux X i i ⋯ : (a : X i) → X i) ((aux X i i ⋯ : (a : X i) → X i) x : X i) : X i)
    ((aux X i i ⋯ : (a : X i) → X i) x : 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.inl i₁ = i
subst : e₁.f i₁ = (ac.equiv : (a : ι₁ ⊕ ι₂) → ι) (Sum.inl 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.inl i₁)

Tactic:
simp