awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
f : Arrow.{v_1, u_1} C
inst_1 : ∀ (n : ℕ), HasWidePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1)) ↦ f.left) fun (x : Fin (n + 1)) ↦ f.hom
S : SplitEpi f.hom
n : ℕ
i : Fin (n + 1)
dsimp :
  Eq (α :=
    (widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1)) ↦ f.left) fun (x : Fin (n + 1)) ↦ f.hom) ⟶
      widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1 + 1 + 1)) ↦ f.left) fun (x : Fin (n + 1 + 1 + 1)) ↦ f.hom)
    (CategoryStruct.comp (Y :=
        widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1 + 1)) ↦ f.left) fun (x : Fin (n + 1 + 1)) ↦ f.hom)
        (ExtraDegeneracy.s f S n : f.cechNerve _⦋n⦌ ⟶ f.cechNerve _⦋n + 1⦌)
        (WidePullback.lift (WidePullback.base fun (x : Fin (n + 1 + 1)) ↦ f.hom)
          (fun (i_1 : Fin (n + 1 + 1 + 1)) ↦ WidePullback.π (fun (x : Fin (n + 1 + 1)) ↦ f.hom) (i.succ.predAbove i_1))
          ⋯) :
      (widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1)) ↦ f.left) fun (x : Fin (n + 1)) ↦ f.hom) ⟶
        widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1 + 1 + 1)) ↦ f.left) fun (x : Fin (n + 1 + 1 + 1)) ↦
          f.hom)
    (CategoryStruct.comp (Y :=
        widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1 + 1)) ↦ f.left) fun (x : Fin (n + 1 + 1)) ↦ f.hom)
        (WidePullback.lift (WidePullback.base fun (x : Fin (n + 1)) ↦ f.hom)
            (fun (i_1 : Fin (n + 1 + 1)) ↦ WidePullback.π (fun (x : Fin (n + 1)) ↦ f.hom) (i.predAbove i_1)) ⋯ :
          (widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1)) ↦ f.left) fun (x : Fin (n + 1)) ↦ f.hom) ⟶
            widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1 + 1)) ↦ f.left) fun (x : Fin (n + 1 + 1)) ↦ f.hom)
        (ExtraDegeneracy.s f S (n + 1) : f.cechNerve _⦋n + 1⦌ ⟶ f.cechNerve _⦋n + 1 + 1⦌) :
      (widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1)) ↦ f.left) fun (x : Fin (n + 1)) ↦ f.hom) ⟶
        widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1 + 1 + 1)) ↦ f.left) fun (x : Fin (n + 1 + 1 + 1)) ↦
          f.hom)
⊢ Eq (α := f.augmentedCechNerve.left _⦋n⦌ ⟶ f.augmentedCechNerve.left _⦋n + 1 + 1⦌)
    (ExtraDegeneracy.s f S n ≫ f.augmentedCechNerve.left.σ i.succ :
      f.augmentedCechNerve.left _⦋n⦌ ⟶ f.augmentedCechNerve.left _⦋n + 1 + 1⦌)
    (f.augmentedCechNerve.left.σ i ≫ ExtraDegeneracy.s f S (n + 1) :
      f.augmentedCechNerve.left _⦋n⦌ ⟶ f.augmentedCechNerve.left _⦋n + 1 + 1⦌)

Tactic:
dsimp [SimplicialObject.σ, SimplexCategory.σ]

Premises used: SimplexCategory.σ, CategoryTheory.SimplicialObject.σ
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
f : Arrow.{v_1, u_1} C
inst_1 : ∀ (n : ℕ), HasWidePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1)) ↦ f.left) fun (x : Fin (n + 1)) ↦ f.hom
S : SplitEpi f.hom
n : ℕ
i : Fin (n + 1)
⊢ Eq (α := (widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1)) ↦ f.left) fun (x : Fin (n + 1)) ↦ f.hom) ⟶ f.left)
    (CategoryStruct.comp (Y :=
        widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1 + 1 + 1)) ↦ f.left) fun (x : Fin (n + 1 + 1 + 1)) ↦
          f.hom)
        (CategoryStruct.comp (Y :=
          widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1 + 1)) ↦ f.left) fun (x : Fin (n + 1 + 1)) ↦ f.hom)
          (ExtraDegeneracy.s f S n : f.cechNerve _⦋n⦌ ⟶ f.cechNerve _⦋n + 1⦌)
          (WidePullback.lift (WidePullback.base fun (x : Fin (n + 1 + 1)) ↦ f.hom)
            (fun (i_1 : Fin (n + 1 + 1 + 1)) ↦
              WidePullback.π (fun (x : Fin (n + 1 + 1)) ↦ f.hom) (i.succ.predAbove i_1))
            ⋯))
        (WidePullback.π (fun (x : Fin (n + 1 + 1 + 1)) ↦ f.hom) 0) :
      (widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1)) ↦ f.left) fun (x : Fin (n + 1)) ↦ f.hom) ⟶ f.left)
    (CategoryStruct.comp (Y :=
        widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1 + 1 + 1)) ↦ f.left) fun (x : Fin (n + 1 + 1 + 1)) ↦
          f.hom)
        (CategoryStruct.comp (Y :=
            widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1 + 1)) ↦ f.left) fun (x : Fin (n + 1 + 1)) ↦ f.hom)
            (WidePullback.lift (WidePullback.base fun (x : Fin (n + 1)) ↦ f.hom)
                (fun (i_1 : Fin (n + 1 + 1)) ↦ WidePullback.π (fun (x : Fin (n + 1)) ↦ f.hom) (i.predAbove i_1)) ⋯ :
              (widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1)) ↦ f.left) fun (x : Fin (n + 1)) ↦ f.hom) ⟶
                widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1 + 1)) ↦ f.left) fun (x : Fin (n + 1 + 1)) ↦
                  f.hom)
            (ExtraDegeneracy.s f S (n + 1) : f.cechNerve _⦋n + 1⦌ ⟶ f.cechNerve _⦋n + 1 + 1⦌) :
          (widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1)) ↦ f.left) fun (x : Fin (n + 1)) ↦ f.hom) ⟶
            widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1 + 1 + 1)) ↦ f.left) fun (x : Fin (n + 1 + 1 + 1)) ↦
              f.hom)
        (WidePullback.π (fun (x : Fin (n + 1 + 1 + 1)) ↦ f.hom) 0 :
          (widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1 + 1 + 1)) ↦ f.left) fun (x : Fin (n + 1 + 1 + 1)) ↦
              f.hom) ⟶
            f.left) :
      (widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1)) ↦ f.left) fun (x : Fin (n + 1)) ↦ f.hom) ⟶ f.left)

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
f : Arrow.{v_1, u_1} C
inst_1 : ∀ (n : ℕ), HasWidePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1)) ↦ f.left) fun (x : Fin (n + 1)) ↦ f.hom
S : SplitEpi f.hom
n : ℕ
i : Fin (n + 1)
i_1 : Fin (n + 2)
⊢ Eq (α := (widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1)) ↦ f.left) fun (x : Fin (n + 1)) ↦ f.hom) ⟶ f.left)
    (CategoryStruct.comp (Y :=
        widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1 + 1 + 1)) ↦ f.left) fun (x : Fin (n + 1 + 1 + 1)) ↦
          f.hom)
        (CategoryStruct.comp (Y :=
          widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1 + 1)) ↦ f.left) fun (x : Fin (n + 1 + 1)) ↦ f.hom)
          (ExtraDegeneracy.s f S n : f.cechNerve _⦋n⦌ ⟶ f.cechNerve _⦋n + 1⦌)
          (WidePullback.lift (WidePullback.base fun (x : Fin (n + 1 + 1)) ↦ f.hom)
            (fun (i_2 : Fin (n + 1 + 1 + 1)) ↦
              WidePullback.π (fun (x : Fin (n + 1 + 1)) ↦ f.hom) (i.succ.predAbove i_2))
            ⋯))
        (WidePullback.π (fun (x : Fin (n + 1 + 1 + 1)) ↦ f.hom) i_1.succ) :
      (widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1)) ↦ f.left) fun (x : Fin (n + 1)) ↦ f.hom) ⟶ f.left)
    (CategoryStruct.comp (Y :=
        widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1 + 1 + 1)) ↦ f.left) fun (x : Fin (n + 1 + 1 + 1)) ↦
          f.hom)
        (CategoryStruct.comp (Y :=
            widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1 + 1)) ↦ f.left) fun (x : Fin (n + 1 + 1)) ↦ f.hom)
            (WidePullback.lift (WidePullback.base fun (x : Fin (n + 1)) ↦ f.hom)
                (fun (i_2 : Fin (n + 1 + 1)) ↦ WidePullback.π (fun (x : Fin (n + 1)) ↦ f.hom) (i.predAbove i_2)) ⋯ :
              (widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1)) ↦ f.left) fun (x : Fin (n + 1)) ↦ f.hom) ⟶
                widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1 + 1)) ↦ f.left) fun (x : Fin (n + 1 + 1)) ↦
                  f.hom)
            (ExtraDegeneracy.s f S (n + 1) : f.cechNerve _⦋n + 1⦌ ⟶ f.cechNerve _⦋n + 1 + 1⦌) :
          (widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1)) ↦ f.left) fun (x : Fin (n + 1)) ↦ f.hom) ⟶
            widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1 + 1 + 1)) ↦ f.left) fun (x : Fin (n + 1 + 1 + 1)) ↦
              f.hom)
        (WidePullback.π (fun (x : Fin (n + 1 + 1 + 1)) ↦ f.hom) i_1.succ :
          (widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1 + 1 + 1)) ↦ f.left) fun (x : Fin (n + 1 + 1 + 1)) ↦
              f.hom) ⟶
            f.left) :
      (widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1)) ↦ f.left) fun (x : Fin (n + 1)) ↦ f.hom) ⟶ f.left)

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
f : Arrow.{v_1, u_1} C
inst_1 : ∀ (n : ℕ), HasWidePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1)) ↦ f.left) fun (x : Fin (n + 1)) ↦ f.hom
S : SplitEpi f.hom
n : ℕ
i : Fin (n + 1)
⊢ Eq (α :=
    (widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1)) ↦ f.left) fun (x : Fin (n + 1)) ↦ f.hom) ⟶ f.right)
    (CategoryStruct.comp (Y :=
        widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1 + 1 + 1)) ↦ f.left) fun (x : Fin (n + 1 + 1 + 1)) ↦
          f.hom)
        (CategoryStruct.comp (Y :=
          widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1 + 1)) ↦ f.left) fun (x : Fin (n + 1 + 1)) ↦ f.hom)
          (ExtraDegeneracy.s f S n : f.cechNerve _⦋n⦌ ⟶ f.cechNerve _⦋n + 1⦌)
          (WidePullback.lift (WidePullback.base fun (x : Fin (n + 1 + 1)) ↦ f.hom)
            (fun (i_1 : Fin (n + 1 + 1 + 1)) ↦
              WidePullback.π (fun (x : Fin (n + 1 + 1)) ↦ f.hom) (i.succ.predAbove i_1))
            ⋯))
        (WidePullback.base fun (x : Fin (n + 1 + 1 + 1)) ↦ f.hom) :
      (widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1)) ↦ f.left) fun (x : Fin (n + 1)) ↦ f.hom) ⟶ f.right)
    (CategoryStruct.comp (Y :=
        widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1 + 1 + 1)) ↦ f.left) fun (x : Fin (n + 1 + 1 + 1)) ↦
          f.hom)
        (CategoryStruct.comp (Y :=
            widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1 + 1)) ↦ f.left) fun (x : Fin (n + 1 + 1)) ↦ f.hom)
            (WidePullback.lift (WidePullback.base fun (x : Fin (n + 1)) ↦ f.hom)
                (fun (i_1 : Fin (n + 1 + 1)) ↦ WidePullback.π (fun (x : Fin (n + 1)) ↦ f.hom) (i.predAbove i_1)) ⋯ :
              (widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1)) ↦ f.left) fun (x : Fin (n + 1)) ↦ f.hom) ⟶
                widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1 + 1)) ↦ f.left) fun (x : Fin (n + 1 + 1)) ↦
                  f.hom)
            (ExtraDegeneracy.s f S (n + 1) : f.cechNerve _⦋n + 1⦌ ⟶ f.cechNerve _⦋n + 1 + 1⦌) :
          (widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1)) ↦ f.left) fun (x : Fin (n + 1)) ↦ f.hom) ⟶
            widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1 + 1 + 1)) ↦ f.left) fun (x : Fin (n + 1 + 1 + 1)) ↦
              f.hom)
        (WidePullback.base fun (x : Fin (n + 1 + 1 + 1)) ↦ f.hom :
          (widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1 + 1 + 1)) ↦ f.left) fun (x : Fin (n + 1 + 1 + 1)) ↦
              f.hom) ⟶
            f.right) :
      (widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1)) ↦ f.left) fun (x : Fin (n + 1)) ↦ f.hom) ⟶ f.right)

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
X : Augmented.{v_1, u_1} C
ed : X.ExtraDegeneracy
⊢ Functor.obj point X ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj (Functor.obj drop X)) 0

Tactic:
exact ed.s'

Premises used: CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.s'
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
X : Augmented.{v_1, u_1} C
ed : X.ExtraDegeneracy
⊢ HomologicalComplex.Hom.f
      (CategoryStruct.comp (Y := Functor.obj (ChainComplex.single₀ C) (Functor.obj point X))
        (NatTrans.app AlternatingFaceMapComplex.ε X)
        ((Equiv.symm
              (ChainComplex.fromSingle₀Equiv (AlternatingFaceMapComplex.obj (Functor.obj drop X))
                (Functor.obj point X)) :
            (a : point.obj X ⟶ (AlternatingFaceMapComplex.obj (drop.obj X)).X 0) →
              (ChainComplex.single₀ C).obj (point.obj X) ⟶ AlternatingFaceMapComplex.obj (drop.obj X))
          ed.s'))
      0 =
    HAdd.hAdd (α :=
        HomologicalComplex.X (AlternatingFaceMapComplex.obj (Functor.obj drop X)) 0 ⟶
          HomologicalComplex.X (AlternatingFaceMapComplex.obj (Functor.obj drop X)) 0)
        (β :=
        HomologicalComplex.X (AlternatingFaceMapComplex.obj (Functor.obj drop X)) 0 ⟶
          HomologicalComplex.X (AlternatingFaceMapComplex.obj (Functor.obj drop X)) 0)
        (0 :
          HomologicalComplex.X (AlternatingFaceMapComplex.obj (Functor.obj drop X)) 0 ⟶
            HomologicalComplex.X (AlternatingFaceMapComplex.obj (Functor.obj drop X)) 0)
        (CategoryStruct.comp (Y :=
            HomologicalComplex.X (AlternatingFaceMapComplex.obj (Functor.obj drop X)) (HAdd.hAdd (α := ℕ) 0 1))
            (Pi.single (M := fun (j : ℕ) ↦
              HomologicalComplex.X (AlternatingFaceMapComplex.obj (Functor.obj drop X)) 0 ⟶
                HomologicalComplex.X (AlternatingFaceMapComplex.obj (Functor.obj drop X)) j)
              (HAdd.hAdd (α := ℕ) 0 1) (-ed.s 0) (HAdd.hAdd (α := ℕ) 0 1))
            (HomologicalComplex.d (AlternatingFaceMapComplex.obj (Functor.obj drop X)) (HAdd.hAdd (α := ℕ) 0 1) 0) :
          HomologicalComplex.X (AlternatingFaceMapComplex.obj (Functor.obj drop X)) 0 ⟶
            HomologicalComplex.X (AlternatingFaceMapComplex.obj (Functor.obj drop X)) 0) +
      HomologicalComplex.Hom.f (𝟙 (AlternatingFaceMapComplex.obj (Functor.obj drop X))) 0

Tactic:
simp [dsimp% ChainComplex.fromSingle₀Equiv_symm_apply_f_zero
            (C := AlternatingFaceMapComplex.obj X.left), s_comp_δ₀, s₀_comp_δ₁]

Premises used: CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.s₀_comp_δ₁, ChainComplex.fromSingle₀Equiv_symm_apply_f_zero, CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.s_comp_δ₀
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
X : Augmented.{v_1, u_1} C
ed : X.ExtraDegeneracy
i : ℕ
⊢ HomologicalComplex.Hom.f
      (CategoryStruct.comp (Y := Functor.obj (ChainComplex.single₀ C) (Functor.obj point X))
        (NatTrans.app AlternatingFaceMapComplex.ε X)
        ((Equiv.symm
              (ChainComplex.fromSingle₀Equiv (AlternatingFaceMapComplex.obj (Functor.obj drop X))
                (Functor.obj point X)) :
            (a : point.obj X ⟶ (AlternatingFaceMapComplex.obj (drop.obj X)).X 0) →
              (ChainComplex.single₀ C).obj (point.obj X) ⟶ AlternatingFaceMapComplex.obj (drop.obj X))
          ed.s'))
      (i + 1) =
    HAdd.hAdd (α :=
        HomologicalComplex.X (AlternatingFaceMapComplex.obj (Functor.obj drop X)) (i + 1) ⟶
          HomologicalComplex.X (AlternatingFaceMapComplex.obj (Functor.obj drop X)) (i + 1))
        (β :=
        HomologicalComplex.X (AlternatingFaceMapComplex.obj (Functor.obj drop X)) (i + 1) ⟶
          HomologicalComplex.X (AlternatingFaceMapComplex.obj (Functor.obj drop X)) (i + 1))
        (HomologicalComplex.d (AlternatingFaceMapComplex.obj (Functor.obj drop X)) (i + 1) i ≫
          Pi.single (M := fun (j : ℕ) ↦
            HomologicalComplex.X (AlternatingFaceMapComplex.obj (Functor.obj drop X)) i ⟶
              HomologicalComplex.X (AlternatingFaceMapComplex.obj (Functor.obj drop X)) j)
            (i + 1) (-ed.s i) (i + 1))
        (CategoryStruct.comp (Y :=
            HomologicalComplex.X (AlternatingFaceMapComplex.obj (Functor.obj drop X)) (i + 1 + 1))
            (Pi.single (M := fun (j : ℕ) ↦
              HomologicalComplex.X (AlternatingFaceMapComplex.obj (Functor.obj drop X)) (i + 1) ⟶
                HomologicalComplex.X (AlternatingFaceMapComplex.obj (Functor.obj drop X)) j)
              (i + 1 + 1) (-ed.s (i + 1)) (i + 1 + 1))
            (HomologicalComplex.d (AlternatingFaceMapComplex.obj (Functor.obj drop X)) (i + 1 + 1) (i + 1)) :
          HomologicalComplex.X (AlternatingFaceMapComplex.obj (Functor.obj drop X)) (i + 1) ⟶
            HomologicalComplex.X (AlternatingFaceMapComplex.obj (Functor.obj drop X)) (i + 1)) +
      HomologicalComplex.Hom.f (𝟙 (AlternatingFaceMapComplex.obj (Functor.obj drop X))) (i + 1)

Tactic:
simp [Fin.sum_univ_succ (n := i + 2), s_comp_δ₀, Preadditive.sum_comp,
            Preadditive.comp_sum,
            s_comp_δ, pow_succ]

Premises used: pow_succ, CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.s_comp_δ, CategoryTheory.Preadditive.sum_comp, CategoryTheory.Preadditive.comp_sum, CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.s_comp_δ₀, Fin.sum_univ_succ
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
X : Augmented.{v_1, u_1} C
ed : X.ExtraDegeneracy
hfg :
  Eq.{v_1 + 1} (α :=
    HomologicalComplex.X.{v_1, u_1, 0}
        (Functor.obj (HomologicalComplex.single C (ComplexShape.down ℕ) 0) (Functor.obj point X)) 0 ⟶
      HomologicalComplex.X.{v_1, u_1, 0} (Functor.obj (ChainComplex.single₀ C) (Functor.obj point X)) 0)
    (HomologicalComplex.Hom.f
      ((Equiv.symm
              (ChainComplex.fromSingle₀Equiv (AlternatingFaceMapComplex.obj (Functor.obj drop X))
                (Functor.obj point X)) :
            (a : point.obj X ⟶ (AlternatingFaceMapComplex.obj (drop.obj X)).X 0) →
              (ChainComplex.single₀ C).obj (point.obj X) ⟶ AlternatingFaceMapComplex.obj (drop.obj X))
          ed.s' ≫
        NatTrans.app AlternatingFaceMapComplex.ε X)
      0)
    (HomologicalComplex.Hom.f (𝟙 (Functor.obj (ChainComplex.single₀ C) (Functor.obj point X))) 0)
⊢ Eq (α :=
    Quiver.Hom (V := HomologicalComplex.{v_1, u_1, 0} C (ComplexShape.down ℕ))
      (Functor.obj (ChainComplex.single₀ C) (Functor.obj point X))
      (Functor.obj (ChainComplex.single₀ C) (Functor.obj point X)))
    ((Equiv.symm
              (ChainComplex.fromSingle₀Equiv (AlternatingFaceMapComplex.obj (Functor.obj drop X))
                (Functor.obj point X)) :
            (a : point.obj X ⟶ (AlternatingFaceMapComplex.obj (drop.obj X)).X 0) →
              (ChainComplex.single₀ C).obj (point.obj X) ⟶ AlternatingFaceMapComplex.obj (drop.obj X))
          ed.s' ≫
        NatTrans.app AlternatingFaceMapComplex.ε X :
      Quiver.Hom (V := HomologicalComplex.{v_1, u_1, 0} C (ComplexShape.down ℕ))
        (Functor.obj (ChainComplex.single₀ C) (Functor.obj point X))
        (Functor.obj (ChainComplex.single₀ C) (Functor.obj point X)))
    (𝟙 (Functor.obj (ChainComplex.single₀ C) (Functor.obj point X)) :
      Quiver.Hom (V := HomologicalComplex.{v_1, u_1, 0} C (ComplexShape.down ℕ))
        (Functor.obj (ChainComplex.single₀ C) (Functor.obj point X))
        (Functor.obj (ChainComplex.single₀ C) (Functor.obj point X)))

Tactic:
ext
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
X : Augmented.{v_1, u_1} C
ed : X.ExtraDegeneracy
⊢ Eq.{v_1 + 1} (α :=
    HomologicalComplex.X.{v_1, u_1, 0}
        (Functor.obj (HomologicalComplex.single C (ComplexShape.down ℕ) 0) (Functor.obj point X)) 0 ⟶
      HomologicalComplex.X.{v_1, u_1, 0} (Functor.obj (ChainComplex.single₀ C) (Functor.obj point X)) 0)
    (HomologicalComplex.Hom.f
      ((Equiv.symm
              (ChainComplex.fromSingle₀Equiv (AlternatingFaceMapComplex.obj (Functor.obj drop X))
                (Functor.obj point X)) :
            (a : point.obj X ⟶ (AlternatingFaceMapComplex.obj (drop.obj X)).X 0) →
              (ChainComplex.single₀ C).obj (point.obj X) ⟶ AlternatingFaceMapComplex.obj (drop.obj X))
          ed.s' ≫
        NatTrans.app AlternatingFaceMapComplex.ε X)
      0)
    (HomologicalComplex.Hom.f (𝟙 (Functor.obj (ChainComplex.single₀ C) (Functor.obj point X))) 0)

Tactic:
simp [dsimp% ChainComplex.fromSingle₀Equiv_symm_apply_f_zero
      (C := AlternatingFaceMapComplex.obj X.left)]

Premises used: ChainComplex.fromSingle₀Equiv_symm_apply_f_zero
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
⊢ Continuous (Y := ℝ) fun (x : (↑I : Type) × (↑I : Type)) ↦ (↑x.2 : ℝ)

Tactic:
fun_prop
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
⊢ Continuous (Y := ℝ) fun (x : (↑I : Type) × (↑I : Type)) ↦ 1 / 2

Tactic:
fun_prop
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
⊢ ContinuousOn (Y := ℝ) (fun (x : (↑I : Type) × (↑I : Type)) ↦ (↑x.1 : ℝ) * 2 * (↑x.2 : ℝ))
    {x : (↑I : Type) × (↑I : Type) | (↑x.2 : ℝ) ≤ 1 / 2}

Tactic:
fun_prop
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
⊢ ContinuousOn (Y := ℝ) (fun (x : (↑I : Type) × (↑I : Type)) ↦ (↑x.1 : ℝ) * (2 - 2 * (↑x.2 : ℝ)))
    {x : (↑I : Type) × (↑I : Type) | 1 / 2 ≤ (↑x.2 : ℝ)}

Tactic:
fun_prop
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
⊢ ∀ (x : (↑I : Type) × (↑I : Type)),
    (↑x.2 : ℝ) = 1 / 2 → (↑x.1 : ℝ) * 2 * (↑x.2 : ℝ) = (↑x.1 : ℝ) * (2 - 2 * (↑x.2 : ℝ))

Tactic:
grind
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
x : (↑I : Type) × (↑I : Type)
pos : (↑x.2 : ℝ) ≤ 1 / 2 → (↑x.1 : ℝ) * 2 * (↑x.2 : ℝ) ∈ I
neg : ¬(↑x.2 : ℝ) ≤ 1 / 2 → (↑x.1 : ℝ) * (2 - 2 * (↑x.2 : ℝ)) ∈ I
⊢ (if (↑x.2 : ℝ) ≤ 1 / 2 then (↑x.1 : ℝ) * 2 * (↑x.2 : ℝ) else (↑x.1 : ℝ) * (2 - 2 * (↑x.2 : ℝ))) ∈ I

Tactic:
split_ifs
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
x : (↑I : Type) × (↑I : Type)
h : (↑x.2 : ℝ) ≤ 1 / 2
pos : 0 ≤ (↑x.1 : ℝ) * 2 * (↑x.2 : ℝ)
pos₁ : (↑x.1 : ℝ) * 2 * (↑x.2 : ℝ) ≤ 1
⊢ (↑x.1 : ℝ) * 2 * (↑x.2 : ℝ) ∈ I

Tactic:
constructor
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
x : (↑I : Type) × (↑I : Type)
h : (↑x.2 : ℝ) ≤ 1 / 2
pos : 0 ≤ (↑x.1 : ℝ) * 2
pos₁ : 0 ≤ (↑x.2 : ℝ)
⊢ 0 ≤ (↑x.1 : ℝ) * 2 * (↑x.2 : ℝ)

Tactic:
apply mul_nonneg

Premises used: mul_nonneg
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
x : (↑I : Type) × (↑I : Type)
h : (↑x.2 : ℝ) ≤ 1 / 2
⊢ 0 ≤ (↑x.1 : ℝ) * 2

Tactic:
grind
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
x : (↑I : Type) × (↑I : Type)
h : (↑x.2 : ℝ) ≤ 1 / 2
⊢ 0 ≤ (↑x.2 : ℝ)

Tactic:
grind
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
x : (↑I : Type) × (↑I : Type)
h : (↑x.2 : ℝ) ≤ 1 / 2
pos : (↑x.1 : ℝ) * (2 * (↑x.2 : ℝ)) ≤ 1
⊢ (↑x.1 : ℝ) * 2 * (↑x.2 : ℝ) ≤ 1

Tactic:
rw [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
x : (↑I : Type) × (↑I : Type)
h : (↑x.2 : ℝ) ≤ 1 / 2
pos : (↑x.1 : ℝ) ≤ 1
pos₁ : 0 ≤ 2 * (↑x.2 : ℝ)
pos₂ : 2 * (↑x.2 : ℝ) ≤ 1
⊢ (↑x.1 : ℝ) * (2 * (↑x.2 : ℝ)) ≤ 1

Tactic:
apply mul_le_one₀

Premises used: mul_le_one₀
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
x : (↑I : Type) × (↑I : Type)
h : (↑x.2 : ℝ) ≤ 1 / 2
⊢ (↑x.1 : ℝ) ≤ 1

Tactic:
grind
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
x : (↑I : Type) × (↑I : Type)
h : (↑x.2 : ℝ) ≤ 1 / 2
⊢ 0 ≤ 2 * (↑x.2 : ℝ)

Tactic:
grind
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
x : (↑I : Type) × (↑I : Type)
h : (↑x.2 : ℝ) ≤ 1 / 2
⊢ 2 * (↑x.2 : ℝ) ≤ 1

Tactic:
grind
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
x : (↑I : Type) × (↑I : Type)
h : ¬(↑x.2 : ℝ) ≤ 1 / 2
neg : 0 ≤ (↑x.1 : ℝ) * (2 - 2 * (↑x.2 : ℝ))
neg₁ : (↑x.1 : ℝ) * (2 - 2 * (↑x.2 : ℝ)) ≤ 1
⊢ (↑x.1 : ℝ) * (2 - 2 * (↑x.2 : ℝ)) ∈ I

Tactic:
constructor
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
x : (↑I : Type) × (↑I : Type)
h : ¬(↑x.2 : ℝ) ≤ 1 / 2
neg : 0 ≤ (↑x.1 : ℝ)
neg₁ : 0 ≤ 2 - 2 * (↑x.2 : ℝ)
⊢ 0 ≤ (↑x.1 : ℝ) * (2 - 2 * (↑x.2 : ℝ))

Tactic:
apply mul_nonneg

Premises used: mul_nonneg
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
x : (↑I : Type) × (↑I : Type)
h : ¬(↑x.2 : ℝ) ≤ 1 / 2
⊢ 0 ≤ (↑x.1 : ℝ)

Tactic:
grind
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
x : (↑I : Type) × (↑I : Type)
h : ¬(↑x.2 : ℝ) ≤ 1 / 2
⊢ 0 ≤ 2 - 2 * (↑x.2 : ℝ)

Tactic:
grind
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
x : (↑I : Type) × (↑I : Type)
h : ¬(↑x.2 : ℝ) ≤ 1 / 2
neg : (↑x.1 : ℝ) ≤ 1
neg₁ : 0 ≤ 2 - 2 * (↑x.2 : ℝ)
neg₂ : 2 - 2 * (↑x.2 : ℝ) ≤ 1
⊢ (↑x.1 : ℝ) * (2 - 2 * (↑x.2 : ℝ)) ≤ 1

Tactic:
apply mul_le_one₀

Premises used: mul_le_one₀
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
x : (↑I : Type) × (↑I : Type)
h : ¬(↑x.2 : ℝ) ≤ 1 / 2
⊢ (↑x.1 : ℝ) ≤ 1

Tactic:
grind