awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ExtraDegeneracy (goal)
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
⊢ Eq (α :=
    (widePullback.{0, v_1, u_1} f.right (fun (x : Fin 1) ↦ f.left) fun (x : Fin 1) ↦ f.hom) ⟶
      widePullback.{0, v_1, u_1} f.right (fun (x : Fin 1) ↦ f.left) fun (x : Fin 1) ↦ f.hom)
    (CategoryStruct.comp (Y := widePullback.{0, v_1, u_1} f.right (fun (x : Fin 2) ↦ f.left) fun (x : Fin 2) ↦ f.hom)
        (ExtraDegeneracy.s f S 0 : f.cechNerve _⦋0⦌ ⟶ f.cechNerve _⦋HAdd.hAdd (α := ℕ) 0 1⦌)
        (WidePullback.lift (WidePullback.base fun (x : Fin 2) ↦ f.hom)
          (fun (i : Fin 1) ↦ WidePullback.π (fun (x : Fin 2) ↦ f.hom) (Fin.succAbove 1 i)) ⋯) :
      (widePullback.{0, v_1, u_1} f.right (fun (x : Fin 1) ↦ f.left) fun (x : Fin 1) ↦ f.hom) ⟶
        widePullback.{0, v_1, u_1} f.right (fun (x : Fin 1) ↦ f.left) fun (x : Fin 1) ↦ f.hom)
    ((WidePullback.base fun (x : Fin 1) ↦ f.hom) ≫ S.section_ ≫ WidePullback.lift f.hom (fun (x : Fin 1) ↦ 𝟙 f.left) ⋯ :
      (widePullback.{0, v_1, u_1} f.right (fun (x : Fin 1) ↦ f.left) fun (x : Fin 1) ↦ f.hom) ⟶
        widePullback.{0, v_1, u_1} f.right (fun (x : Fin 1) ↦ f.left) fun (x : Fin 1) ↦ f.hom)
have a : ∀ (j : Fin 1),
  Eq (α := (widePullback.{0, v_1, u_1} f.right (fun (x : Fin 1) ↦ f.left) fun (x : Fin 1) ↦ f.hom) ⟶ f.left)
    (CategoryStruct.comp (Y := widePullback.{0, v_1, u_1} f.right (fun (x : Fin 1) ↦ f.left) fun (x : Fin 1) ↦ f.hom)
        (CategoryStruct.comp (Y :=
          widePullback.{0, v_1, u_1} f.right (fun (x : Fin 2) ↦ f.left) fun (x : Fin 2) ↦ f.hom)
          (ExtraDegeneracy.s f S 0 : f.cechNerve _⦋0⦌ ⟶ f.cechNerve _⦋HAdd.hAdd (α := ℕ) 0 1⦌)
          (WidePullback.lift (WidePullback.base fun (x : Fin 2) ↦ f.hom)
            (fun (i : Fin 1) ↦ WidePullback.π (fun (x : Fin 2) ↦ f.hom) (Fin.succAbove 1 i)) sorry))
        (WidePullback.π (fun (x : Fin 1) ↦ f.hom) j) :
      (widePullback.{0, v_1, u_1} f.right (fun (x : Fin 1) ↦ f.left) fun (x : Fin 1) ↦ f.hom) ⟶ f.left)
    (CategoryStruct.comp (Y := widePullback.{0, v_1, u_1} f.right (fun (x : Fin 1) ↦ f.left) fun (x : Fin 1) ↦ f.hom)
        ((WidePullback.base fun (x : Fin 1) ↦ f.hom) ≫
          S.section_ ≫ WidePullback.lift f.hom (fun (x : Fin 1) ↦ 𝟙 f.left) sorry)
        (WidePullback.π (fun (x : Fin 1) ↦ f.hom) j) :
      (widePullback.{0, v_1, u_1} f.right (fun (x : Fin 1) ↦ f.left) fun (x : Fin 1) ↦ f.hom) ⟶ f.left)
Tactic: ext j
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ExtraDegeneracy (goal)
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
j : Fin 1
⊢ Eq (α := (widePullback.{0, v_1, u_1} f.right (fun (x : Fin 1) ↦ f.left) fun (x : Fin 1) ↦ f.hom) ⟶ f.left)
    (CategoryStruct.comp (Y := widePullback.{0, v_1, u_1} f.right (fun (x : Fin 1) ↦ f.left) fun (x : Fin 1) ↦ f.hom)
        (CategoryStruct.comp (Y :=
          widePullback.{0, v_1, u_1} f.right (fun (x : Fin 2) ↦ f.left) fun (x : Fin 2) ↦ f.hom)
          (ExtraDegeneracy.s f S 0 : f.cechNerve _⦋0⦌ ⟶ f.cechNerve _⦋HAdd.hAdd (α := ℕ) 0 1⦌)
          (WidePullback.lift (WidePullback.base fun (x : Fin 2) ↦ f.hom)
            (fun (i : Fin 1) ↦ WidePullback.π (fun (x : Fin 2) ↦ f.hom) (Fin.succAbove 1 i)) ⋯))
        (WidePullback.π (fun (x : Fin 1) ↦ f.hom) j) :
      (widePullback.{0, v_1, u_1} f.right (fun (x : Fin 1) ↦ f.left) fun (x : Fin 1) ↦ f.hom) ⟶ f.left)
    (CategoryStruct.comp (Y := widePullback.{0, v_1, u_1} f.right (fun (x : Fin 1) ↦ f.left) fun (x : Fin 1) ↦ f.hom)
        ((WidePullback.base fun (x : Fin 1) ↦ f.hom) ≫
          S.section_ ≫ WidePullback.lift f.hom (fun (x : Fin 1) ↦ 𝟙 f.left) ⋯)
        (WidePullback.π (fun (x : Fin 1) ↦ f.hom) j) :
      (widePullback.{0, v_1, u_1} f.right (fun (x : Fin 1) ↦ f.left) fun (x : Fin 1) ↦ f.hom) ⟶ f.left)
have a : Eq (α := (widePullback.{0, v_1, u_1} f.right (fun (x : Fin 1) ↦ f.left) fun (x : Fin 1) ↦ f.hom) ⟶ f.left)
  (CategoryStruct.comp (Y := widePullback.{0, v_1, u_1} f.right (fun (x : Fin 1) ↦ f.left) fun (x : Fin 1) ↦ f.hom)
      (CategoryStruct.comp (Y := widePullback.{0, v_1, u_1} f.right (fun (x : Fin 2) ↦ f.left) fun (x : Fin 2) ↦ f.hom)
        (ExtraDegeneracy.s f S 0 : f.cechNerve _⦋0⦌ ⟶ f.cechNerve _⦋HAdd.hAdd (α := ℕ) 0 1⦌)
        (WidePullback.lift (WidePullback.base fun (x : Fin 2) ↦ f.hom)
          (fun (i : Fin 1) ↦ WidePullback.π (fun (x : Fin 2) ↦ f.hom) (Fin.succAbove 1 i)) sorry))
      (WidePullback.π (fun (x : Fin 1) ↦ f.hom) ((fun (i : Fin (⦋0⦌.len + 1)) ↦ i) ⟨0, sorry⟩)) :
    (widePullback.{0, v_1, u_1} f.right (fun (x : Fin 1) ↦ f.left) fun (x : Fin 1) ↦ f.hom) ⟶ f.left)
  (CategoryStruct.comp (Y := widePullback.{0, v_1, u_1} f.right (fun (x : Fin 1) ↦ f.left) fun (x : Fin 1) ↦ f.hom)
      ((WidePullback.base fun (x : Fin 1) ↦ f.hom) ≫
        S.section_ ≫ WidePullback.lift f.hom (fun (x : Fin 1) ↦ 𝟙 f.left) sorry)
      (WidePullback.π (fun (x : Fin 1) ↦ f.hom) ((fun (i : Fin (⦋0⦌.len + 1)) ↦ i) ⟨0, sorry⟩)) :
    (widePullback.{0, v_1, u_1} f.right (fun (x : Fin 1) ↦ f.left) fun (x : Fin 1) ↦ f.hom) ⟶ f.left)
Tactic: fin_cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ExtraDegeneracy (goal)
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 : ℕ
⊢ Eq (α := f.augmentedCechNerve.left _⦋n⦌ ⟶ f.augmentedCechNerve.left _⦋n⦌)
    (CategoryStruct.comp (Y := f.augmentedCechNerve.left _⦋n + 1⦌)
        (ExtraDegeneracy.s f S n : f.cechNerve _⦋n⦌ ⟶ f.cechNerve _⦋n + 1⦌) (f.augmentedCechNerve.left.δ 0) :
      f.augmentedCechNerve.left _⦋n⦌ ⟶ f.augmentedCechNerve.left _⦋n⦌)
    (𝟙 (f.augmentedCechNerve.left _⦋n⦌) : f.augmentedCechNerve.left _⦋n⦌ ⟶ f.augmentedCechNerve.left _⦋n⦌)
have 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)) ↦ f.left) fun (x : Fin (n + 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 : Fin (n + 1)) ↦ WidePullback.π (fun (x : Fin (n + 1 + 1)) ↦ f.hom) i.succ) sorry) :
    (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)) ↦ f.left) fun (x : Fin (n + 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) :
    (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)) ↦ f.left) fun (x : Fin (n + 1)) ↦ f.hom)
Tactic: dsimp [SimplicialObject.δ, SimplexCategory.δ]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ExtraDegeneracy (goal)
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 + 2)
⊢ Eq (α := f.augmentedCechNerve.left _⦋n + 1⦌ ⟶ f.augmentedCechNerve.left _⦋n + 1⦌)
    (ExtraDegeneracy.s f S (n + 1) ≫ f.augmentedCechNerve.left.δ i.succ :
      f.augmentedCechNerve.left _⦋n + 1⦌ ⟶ f.augmentedCechNerve.left _⦋n + 1⦌)
    (f.augmentedCechNerve.left.δ i ≫ ExtraDegeneracy.s f S n :
      f.augmentedCechNerve.left _⦋n + 1⦌ ⟶ f.augmentedCechNerve.left _⦋n + 1⦌)
have dsimp : Eq (α :=
  (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.{0, v_1, u_1} f.right (fun (x : Fin (n + 1 + 1)) ↦ f.left) fun (x : Fin (n + 1 + 1)) ↦ f.hom)
  (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)
      (ExtraDegeneracy.s f S (n + 1) : f.cechNerve _⦋n + 1⦌ ⟶ f.cechNerve _⦋n + 1 + 1⦌)
      (WidePullback.lift (WidePullback.base fun (x : Fin (n + 1 + 1 + 1)) ↦ f.hom)
        (fun (i_1 : Fin (n + 1 + 1)) ↦ WidePullback.π (fun (x : Fin (n + 1 + 1 + 1)) ↦ f.hom) (i.succ.succAbove i_1))
        sorry) :
    (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.{0, v_1, u_1} f.right (fun (x : Fin (n + 1 + 1)) ↦ f.left) fun (x : Fin (n + 1 + 1)) ↦ f.hom)
  (CategoryStruct.comp (Y :=
      widePullback.{0, v_1, u_1} f.right (fun (x : Fin (n + 1)) ↦ f.left) fun (x : Fin (n + 1)) ↦ f.hom)
      (WidePullback.lift (WidePullback.base fun (x : Fin (n + 1 + 1)) ↦ f.hom)
          (fun (i_1 : Fin (n + 1)) ↦ WidePullback.π (fun (x : Fin (n + 1 + 1)) ↦ f.hom) (i.succAbove i_1)) sorry :
        (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.{0, v_1, u_1} f.right (fun (x : Fin (n + 1)) ↦ f.left) fun (x : Fin (n + 1)) ↦ f.hom)
      (ExtraDegeneracy.s f S n : f.cechNerve _⦋n⦌ ⟶ f.cechNerve _⦋n + 1⦌) :
    (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.{0, v_1, u_1} f.right (fun (x : Fin (n + 1 + 1)) ↦ f.left) fun (x : Fin (n + 1 + 1)) ↦ f.hom)
Tactic: dsimp [SimplicialObject.δ, SimplexCategory.δ]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ExtraDegeneracy (goal)
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 (α := 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⦌)
have 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))
        sorry) :
    (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)) sorry :
        (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)
Tactic: dsimp [SimplicialObject.σ, SimplexCategory.σ]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ExtraDegeneracy (goal)
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 (α :=
    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)))
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
x : (↑I : Type) × (↑I : Type)
⊢ (if (↑x.2 : ℝ) ≤ 1 / 2 then (↑x.1 : ℝ) * 2 * (↑x.2 : ℝ) else (↑x.1 : ℝ) * (2 - 2 * (↑x.2 : ℝ))) ∈ I
have pos : (↑x.2 : ℝ) ≤ 1 / 2 → (↑x.1 : ℝ) * 2 * (↑x.2 : ℝ) ∈ I
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
x : (↑I : Type) × (↑I : Type)
pos : (↑x.2 : ℝ) ≤ 1 / 2 → (↑x.1 : ℝ) * 2 * (↑x.2 : ℝ) ∈ I
⊢ (if (↑x.2 : ℝ) ≤ 1 / 2 then (↑x.1 : ℝ) * 2 * (↑x.2 : ℝ) else (↑x.1 : ℝ) * (2 - 2 * (↑x.2 : ℝ))) ∈ I
have neg : ¬(↑x.2 : ℝ) ≤ 1 / 2 → (↑x.1 : ℝ) * (2 - 2 * (↑x.2 : ℝ)) ∈ I
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
x : (↑I : Type) × (↑I : Type)
h : (↑x.2 : ℝ) ≤ 1 / 2
⊢ (↑x.1 : ℝ) * 2 * (↑x.2 : ℝ) ∈ I
have pos : 0 ≤ (↑x.1 : ℝ) * 2 * (↑x.2 : ℝ)
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
x : (↑I : Type) × (↑I : Type)
h : (↑x.2 : ℝ) ≤ 1 / 2
pos : 0 ≤ (↑x.1 : ℝ) * 2 * (↑x.2 : ℝ)
⊢ (↑x.1 : ℝ) * 2 * (↑x.2 : ℝ) ∈ I
have pos₁ : (↑x.1 : ℝ) * 2 * (↑x.2 : ℝ) ≤ 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
x : (↑I : Type) × (↑I : Type)
h : (↑x.2 : ℝ) ≤ 1 / 2
⊢ 0 ≤ (↑x.1 : ℝ) * 2 * (↑x.2 : ℝ)
have pos : 0 ≤ (↑x.1 : ℝ) * 2
Tactic: apply mul_nonneg
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
x : (↑I : Type) × (↑I : Type)
h : (↑x.2 : ℝ) ≤ 1 / 2
pos : 0 ≤ (↑x.1 : ℝ) * 2
⊢ 0 ≤ (↑x.1 : ℝ) * 2 * (↑x.2 : ℝ)
have pos₁ : 0 ≤ (↑x.2 : ℝ)
Tactic: apply mul_nonneg
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
x : (↑I : Type) × (↑I : Type)
h : (↑x.2 : ℝ) ≤ 1 / 2
⊢ (↑x.1 : ℝ) * 2 * (↑x.2 : ℝ) ≤ 1
have pos : (↑x.1 : ℝ) * (2 * (↑x.2 : ℝ)) ≤ 1
Tactic: rw [mul_assoc]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
x : (↑I : Type) × (↑I : Type)
h : (↑x.2 : ℝ) ≤ 1 / 2
⊢ (↑x.1 : ℝ) * (2 * (↑x.2 : ℝ)) ≤ 1
have pos : (↑x.1 : ℝ) ≤ 1
Tactic: apply mul_le_one₀
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
x : (↑I : Type) × (↑I : Type)
h : (↑x.2 : ℝ) ≤ 1 / 2
pos : (↑x.1 : ℝ) ≤ 1
⊢ (↑x.1 : ℝ) * (2 * (↑x.2 : ℝ)) ≤ 1
have pos₁ : 0 ≤ 2 * (↑x.2 : ℝ)
Tactic: apply mul_le_one₀
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
x : (↑I : Type) × (↑I : Type)
h : (↑x.2 : ℝ) ≤ 1 / 2
pos : (↑x.1 : ℝ) ≤ 1
pos₁ : 0 ≤ 2 * (↑x.2 : ℝ)
⊢ (↑x.1 : ℝ) * (2 * (↑x.2 : ℝ)) ≤ 1
have pos₂ : 2 * (↑x.2 : ℝ) ≤ 1
Tactic: apply mul_le_one₀
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
x : (↑I : Type) × (↑I : Type)
h : ¬(↑x.2 : ℝ) ≤ 1 / 2
⊢ (↑x.1 : ℝ) * (2 - 2 * (↑x.2 : ℝ)) ∈ I
have neg : 0 ≤ (↑x.1 : ℝ) * (2 - 2 * (↑x.2 : ℝ))
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
x : (↑I : Type) × (↑I : Type)
h : ¬(↑x.2 : ℝ) ≤ 1 / 2
neg : 0 ≤ (↑x.1 : ℝ) * (2 - 2 * (↑x.2 : ℝ))
⊢ (↑x.1 : ℝ) * (2 - 2 * (↑x.2 : ℝ)) ∈ I
have neg₁ : (↑x.1 : ℝ) * (2 - 2 * (↑x.2 : ℝ)) ≤ 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
x : (↑I : Type) × (↑I : Type)
h : ¬(↑x.2 : ℝ) ≤ 1 / 2
⊢ 0 ≤ (↑x.1 : ℝ) * (2 - 2 * (↑x.2 : ℝ))
have neg : 0 ≤ (↑x.1 : ℝ)
Tactic: apply mul_nonneg
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
x : (↑I : Type) × (↑I : Type)
h : ¬(↑x.2 : ℝ) ≤ 1 / 2
neg : 0 ≤ (↑x.1 : ℝ)
⊢ 0 ≤ (↑x.1 : ℝ) * (2 - 2 * (↑x.2 : ℝ))
have neg₁ : 0 ≤ 2 - 2 * (↑x.2 : ℝ)
Tactic: apply mul_nonneg
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
x : (↑I : Type) × (↑I : Type)
h : ¬(↑x.2 : ℝ) ≤ 1 / 2
⊢ (↑x.1 : ℝ) * (2 - 2 * (↑x.2 : ℝ)) ≤ 1
have neg : (↑x.1 : ℝ) ≤ 1
Tactic: apply mul_le_one₀
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
x : (↑I : Type) × (↑I : Type)
h : ¬(↑x.2 : ℝ) ≤ 1 / 2
neg : (↑x.1 : ℝ) ≤ 1
⊢ (↑x.1 : ℝ) * (2 - 2 * (↑x.2 : ℝ)) ≤ 1
have neg₁ : 0 ≤ 2 - 2 * (↑x.2 : ℝ)
Tactic: apply mul_le_one₀
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
x : (↑I : Type) × (↑I : Type)
h : ¬(↑x.2 : ℝ) ≤ 1 / 2
neg : (↑x.1 : ℝ) ≤ 1
neg₁ : 0 ≤ 2 - 2 * (↑x.2 : ℝ)
⊢ (↑x.1 : ℝ) * (2 - 2 * (↑x.2 : ℝ)) ≤ 1
have neg₂ : 2 - 2 * (↑x.2 : ℝ) ≤ 1
Tactic: apply mul_le_one₀
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
x : (↑I : Type)
⊢ Eq (α := X) ((p : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (reflTransSymmAux (1, x)) ⋯) : X)
    (((p.trans p.symm).toContinuousMap : (a : (↑I : Type)) → X) x : X)
have simp : Eq (α := X)
  ((p : (a : (↑I : Type)) → X)
      (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I)
        (if (↑x : ℝ) ≤ 1 / 2 then HMul.hMul (α := ℝ) (↑1 : ℝ) 2 * (↑x : ℝ) else (↑1 : ℝ) * (2 - 2 * (↑x : ℝ))) sorry) :
    X)
  (({
          toFun :=
            (fun (t : ℝ) ↦
                if t ≤ 1 / 2 then (p.extend : (a : ℝ) → X) (2 * t) else (p.symm.extend : (a : ℝ) → X) (2 * t - 1)) ∘
              Subtype.val (p := fun (x : ℝ) ↦ x ∈ I),
          continuous_toFun := sorry : C((↑I : Type), X) } :
        (a : (↑I : Type)) → X)
      x :
    X)
Tactic: simp only [reflTransSymmAux, Path.trans]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
x : (↑I : Type)
hx : 2⁻¹ < (↑x : ℝ)
⊢ Eq (α := X)
    ((p : (a : (↑I : Type)) → X)
        (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I)
          (if (↑x : ℝ) ≤ 1 / 2 then HMul.hMul (α := ℝ) (↑1 : ℝ) 2 * (↑x : ℝ) else (↑1 : ℝ) * (2 - 2 * (↑x : ℝ))) ⋯) :
      X)
    (({
            toFun :=
              (fun (t : ℝ) ↦
                  if t ≤ 1 / 2 then (p.extend : (a : ℝ) → X) (2 * t) else (p.symm.extend : (a : ℝ) → X) (2 * t - 1)) ∘
                Subtype.val (p := fun (x : ℝ) ↦ x ∈ I),
            continuous_toFun := ⋯ : C((↑I : Type), X) } :
          (a : (↑I : Type)) → X)
        x :
      X)
have this : Eq (α := X) ((p.extend : (a : ℝ) → X) (2 - 2 * (↑x : ℝ)) : X) ((p.extend : (a : ℝ) → X) (1 - (2 * (↑x : ℝ) - 1)) : X)
Tactic: have : p.extend (2 - 2 * ↑x) = p.extend (1 - (2 * ↑x - 1)) := by ring_nf
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
x : (↑I : Type)
⊢ Eq (α := X)
    ((p : (a : (↑I : Type)) → X)
        (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I)
          (if (↑x : ℝ) ≤ 1 / 2 then HMul.hMul (α := ℝ) (↑1 : ℝ) 2 * (↑x : ℝ) else (↑1 : ℝ) * (2 - 2 * (↑x : ℝ))) ⋯) :
      X)
    (({
            toFun :=
              (fun (t : ℝ) ↦
                  if t ≤ 1 / 2 then (p.extend : (a : ℝ) → X) (2 * t) else (p.symm.extend : (a : ℝ) → X) (2 * t - 1)) ∘
                Subtype.val (p := fun (x : ℝ) ↦ x ∈ I),
            continuous_toFun := ⋯ : C((↑I : Type), X) } :
          (a : (↑I : Type)) → X)
        x :
      X)
have x₂ : (↑x : ℝ) ≤ 2⁻¹ ∨ 2⁻¹ < (↑x : ℝ)
Tactic: cases le_or_gt (x : ℝ) 2⁻¹ with
    | inl hx => simp [hx, ← extend_apply]
    | inr hx =>
      have : p.extend (2 - 2 * ↑x) = p.extend (1 - (2 * ↑x - 1)) := by ring_nf
      simpa [hx.not_ge, ← extend_apply]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
t : (↑I : Type)
⊢ (if (↑t : ℝ) ≤ 1 / 2 then 2 * (↑t : ℝ) else 1) ∈ I
have pos : (↑t : ℝ) ≤ 1 / 2 → 2 * (↑t : ℝ) ∈ I
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
t : (↑I : Type)
pos : (↑t : ℝ) ≤ 1 / 2 → 2 * (↑t : ℝ) ∈ I
⊢ (if (↑t : ℝ) ≤ 1 / 2 then 2 * (↑t : ℝ) else 1) ∈ I
have neg : ¬(↑t : ℝ) ≤ 1 / 2 → 1 ∈ I
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
t : (↑I : Type)
h : (↑t : ℝ) ≤ 1 / 2
⊢ 2 * (↑t : ℝ) ∈ I
have pos : 0 ≤ 2 * (↑t : ℝ)
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
t : (↑I : Type)
h : (↑t : ℝ) ≤ 1 / 2
pos : 0 ≤ 2 * (↑t : ℝ)
⊢ 2 * (↑t : ℝ) ∈ I
have pos₁ : 2 * (↑t : ℝ) ≤ 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
t : (↑I : Type)
h : ¬(↑t : ℝ) ≤ 1 / 2
⊢ 1 ∈ I
have neg : LE.le (α := ℝ) 0 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
t : (↑I : Type)
h : ¬(↑t : ℝ) ≤ 1 / 2
neg : LE.le (α := ℝ) 0 1
⊢ 1 ∈ I
have neg₁ : LE.le (α := ℝ) 1 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
t : (↑I : Type)
h : (↑t : ℝ) ≤ 1 / 2
⊢ 0 ≤ 2 * (↑t : ℝ)
have linarith : 2 * (↑t : ℝ) < 0 → 2 / 2 = 1
Tactic: linarith [unitInterval.le_one t, unitInterval.nonneg t]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
t : (↑I : Type)
h : (↑t : ℝ) ≤ 1 / 2
linarith : 2 * (↑t : ℝ) < 0 → 2 / 2 = 1
⊢ 0 ≤ 2 * (↑t : ℝ)
have linarith₁ : 2 * (↑t : ℝ) < 0 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith [unitInterval.le_one t, unitInterval.nonneg t]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
t : (↑I : Type)
h : (↑t : ℝ) ≤ 1 / 2
linarith : 2 * (↑t : ℝ) < 0 → 2 / 2 = 1
linarith₁ : 2 * (↑t : ℝ) < 0 → HMul.hMul (α := ℝ) 1 2 = 2
⊢ 0 ≤ 2 * (↑t : ℝ)
have linarith₂ : 2 * (↑t : ℝ) < 0 → GT.gt (α := ℝ) 2 0
Tactic: linarith [unitInterval.le_one t, unitInterval.nonneg t]