awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Homotopy.HSpaces
Goal:
X : Type u
inst : TopologicalSpace X
x y : X
γ : Path x y
t : (↑I : Type)
h : ¬(↑t : ℝ) ≤ 1 / 2
⊢ (if (↑t : ℝ) ≤ 1 / 2 then 2 * (↑t : ℝ) else 1) = (↑1 : ℝ)

Tactic:
if_neg h

Premises used: if_neg
-- Module: Mathlib.Topology.Homotopy.HSpaces
Goal:
X : Type u
inst : TopologicalSpace X
x y : X
γ : Path x y
t : (↑I : Type)
h : (↑t : ℝ) ≤ 1 / 2
⊢ (if (↑t : ℝ) ≤ 1 / 2 then 2 * (↑t : ℝ) else 1) = (↑(Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑t : ℝ)) ⋯) : ℝ)

Tactic:
if_pos h

Premises used: if_pos
-- Module: Mathlib.Topology.Homotopy.HSpaces
Goal:
X : Type u
inst : TopologicalSpace X
x y : X
γ : Path x y
t : (↑I : Type)
h : ¬(↑t : ℝ) ≤ 1 / 2
⊢ (if (↑t : ℝ) ≤ 1 / 2 then 2 * (↑t : ℝ) else 1) = (↑1 : ℝ)

Tactic:
exacts [if_neg h, if_pos h]

Premises used: if_pos, if_neg
-- Module: Mathlib.Topology.Homotopy.HSpaces
Goal:
X : Type u
inst : TopologicalSpace X
x y : X
γ : Path x y
a :
  ∀ (t : (↑I : Type)),
    Eq (α := X) ((delayReflRight 1 γ : (a : (↑I : Type)) → X) t : X) ((γ : (a : (↑I : Type)) → X) t : X)
⊢ delayReflRight 1 γ = γ

Tactic:
ext t
-- Module: Mathlib.Topology.Homotopy.HSpaces
Goal:
X : Type u
inst : TopologicalSpace X
x y : X
γ : Path x y
t : (↑I : Type)
⊢ Eq (α := X) ((delayReflRight 1 γ : (a : (↑I : Type)) → X) t : X) ((γ : (a : (↑I : Type)) → X) t : X)

Tactic:
congr_arg γ (qRight_one_right t)

Premises used: congr_arg, DFunLike.coe, unitInterval.qRight_one_right
-- Module: Mathlib.Topology.Homotopy.HSpaces
Goal:
X : Type u
inst : TopologicalSpace X
x y : X
γ : Path x y
t : (↑I : Type)
⊢ Eq (α := X) ((delayReflRight 1 γ : (a : (↑I : Type)) → X) t : X) ((γ : (a : (↑I : Type)) → X) t : X)

Tactic:
exact congr_arg γ (qRight_one_right t)

Premises used: congr_arg, DFunLike.coe, unitInterval.qRight_one_right
-- Module: Mathlib.Topology.Homotopy.HSpaces
Goal:
X : Type u
inst : TopologicalSpace X
x y : X
⊢ Continuous (Y := Path x y) fun (p : (↑I : Type) × Path x y) ↦ delayReflLeft p.1 p.2

Tactic:
Path.continuous_symm.comp <|
    continuous_delayReflRight.comp <|
      continuous_fst.prodMk <| Path.continuous_symm.comp continuous_snd

Premises used: Path.symm, Path.continuous_symm, Continuous.comp, Path.continuous_delayReflRight, continuous_snd, continuous_fst, Path.delayReflLeft, Continuous.prodMk
-- Module: Mathlib.Topology.Homotopy.HSpaces
Goal:
X : Type u
inst : TopologicalSpace X
x y : X
γ : Path x y
⊢ delayReflLeft 0 γ = trans (refl x) γ

Tactic:
simp only [delayReflLeft, delayReflRight_zero, trans_symm, refl_symm, Path.symm_symm]

Premises used: Path.delayReflRight_zero, Path.symm_symm, Path.trans_symm, Path.refl_symm, Path.delayReflLeft
-- Module: Mathlib.Topology.Homotopy.HSpaces
Goal:
X : Type u
inst : TopologicalSpace X
x y : X
γ : Path x y
⊢ delayReflLeft 1 γ = γ

Tactic:
simp only [delayReflLeft, delayReflRight_one, Path.symm_symm]

Premises used: Path.symm_symm, Path.delayReflRight_one, Path.delayReflLeft
-- Module: Mathlib.Topology.Homotopy.HSpaces
Goal:
X : Type u
inst : TopologicalSpace X
x_1 y x : X
t : (↑I : Type)
⊢ Eq (α := Path x x)
    (({ toFun := fun (x_2 : Path x x) ↦ (fun (p : (↑I : Type) × Path x x) ↦ delayReflLeft p.1 p.2) (t, x_2),
            continuous_toFun := ⋯ } :
          (a : Path x x) → Path x x)
        (refl x) :
      Path x x)
    ((comp { toFun := fun (ρ : Path x x × Path x x) ↦ ρ.1.trans ρ.2, continuous_toFun := ⋯ }
            (prodMk (const (Path x x) (refl x)) (ContinuousMap.id (Path x x))) :
          (a : Path x x) → Path x x)
        (refl x) :
      Path x x)

Tactic:
refl_trans_refl.symm

Premises used: Path.symm, Path.trans, Path.refl_trans_refl, ContinuousMap.const, Path.delayReflLeft, Eq.symm, Path.refl
-- Module: Mathlib.Topology.Homotopy.HSpaces
Goal:
X : Type u
inst : TopologicalSpace X
x_1 y x : X
t : (↑I : Type)
⊢ Eq (α := Path x x)
    (({ toFun := fun (x_2 : Path x x) ↦ (fun (p : (↑I : Type) × Path x x) ↦ delayReflLeft p.1 p.2) (t, x_2),
            continuous_toFun := ⋯ } :
          (a : Path x x) → Path x x)
        (refl x) :
      Path x x)
    ((comp { toFun := fun (ρ : Path x x × Path x x) ↦ ρ.1.trans ρ.2, continuous_toFun := ⋯ }
            (prodMk (const (Path x x) (refl x)) (ContinuousMap.id (Path x x))) :
          (a : Path x x) → Path x x)
        (refl x) :
      Path x x)

Tactic:
exact refl_trans_refl.symm

Premises used: Path.refl_trans_refl, Eq.symm
-- Module: Mathlib.Topology.Homotopy.HSpaces
Goal:
X : Type u
inst : TopologicalSpace X
x_1 y x : X
t : (↑I : Type)
⊢ Eq (α := Path x x)
    (({ toFun := fun (x_2 : Path x x) ↦ (fun (p : (↑I : Type) × Path x x) ↦ delayReflRight p.1 p.2) (t, x_2),
            continuous_toFun := ⋯ } :
          (a : Path x x) → Path x x)
        (refl x) :
      Path x x)
    ((comp { toFun := fun (ρ : Path x x × Path x x) ↦ ρ.1.trans ρ.2, continuous_toFun := ⋯ }
            (prodMk (ContinuousMap.id (Path x x)) (const (Path x x) (refl x))) :
          (a : Path x x) → Path x x)
        (refl x) :
      Path x x)

Tactic:
refl_trans_refl.symm

Premises used: Path.trans, Path.delayReflRight, Path.refl_trans_refl, ContinuousMap.const, Eq.symm, Path.refl
-- Module: Mathlib.Topology.Homotopy.HSpaces
Goal:
X : Type u
inst : TopologicalSpace X
x_1 y x : X
t : (↑I : Type)
⊢ Eq (α := Path x x)
    (({ toFun := fun (x_2 : Path x x) ↦ (fun (p : (↑I : Type) × Path x x) ↦ delayReflRight p.1 p.2) (t, x_2),
            continuous_toFun := ⋯ } :
          (a : Path x x) → Path x x)
        (refl x) :
      Path x x)
    ((comp { toFun := fun (ρ : Path x x × Path x x) ↦ ρ.1.trans ρ.2, continuous_toFun := ⋯ }
            (prodMk (ContinuousMap.id (Path x x)) (const (Path x x) (refl x))) :
          (a : Path x x) → Path x x)
        (refl x) :
      Path x x)

Tactic:
exact refl_trans_refl.symm

Premises used: Path.refl_trans_refl, Eq.symm
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
Goal:
N : Type u_1
inst : DecidableEq N
i : N
t₀ : (↑I : Type)
t : { j : N // j ≠ i } → (↑I : Type)
H : (t₀ = 0 ∨ t₀ = 1) ∨ Membership.mem (γ := Set ({ j : N // j ≠ i } → (↑I : Type))) (boundary { j : N // j ≠ i }) t
inl :
  ∀ (H : t₀ = 0 ∨ t₀ = 1),
    Membership.mem (α := N → (↑I : Type)) (boundary N)
      ((insertAt i : (a : (↑I : Type) × ({ j : N // j ≠ i } → (↑I : Type))) → N → (↑I : Type)) (t₀, t) :
        N → (↑I : Type))
inr :
  ∀ (j : { j : N // j ≠ i }) (H : t j = 0 ∨ t j = 1),
    Membership.mem (α := N → (↑I : Type)) (boundary N)
      ((insertAt i : (a : (↑I : Type) × ({ j : N // j ≠ i } → (↑I : Type))) → N → (↑I : Type)) (t₀, t) :
        N → (↑I : Type))
⊢ Membership.mem (α := N → (↑I : Type)) (boundary N)
    ((insertAt i : (a : (↑I : Type) × ({ j : N // j ≠ i } → (↑I : Type))) → N → (↑I : Type)) (t₀, t) : N → (↑I : Type))

Tactic:
obtain H | ⟨j, H⟩ := H
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
Goal:
N : Type u_1
inst : DecidableEq N
i : N
t₀ : (↑I : Type)
t : { j : N // j ≠ i } → (↑I : Type)
H : t₀ = 0 ∨ t₀ = 1
h :
  Eq (α := (↑I : Type))
      ((insertAt i : (a : (↑I : Type) × ({ j : N // j ≠ i } → (↑I : Type))) → N → (↑I : Type)) (t₀, t) i) 0 ∨
    Eq (α := (↑I : Type))
      ((insertAt i : (a : (↑I : Type) × ({ j : N // j ≠ i } → (↑I : Type))) → N → (↑I : Type)) (t₀, t) i) 1
⊢ Membership.mem (α := N → (↑I : Type)) (boundary N)
    ((insertAt i : (a : (↑I : Type) × ({ j : N // j ≠ i } → (↑I : Type))) → N → (↑I : Type)) (t₀, t) : N → (↑I : Type))

Tactic:
use i
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
Goal:
N : Type u_1
inst : DecidableEq N
i : N
t₀ : (↑I : Type)
t : { j : N // j ≠ i } → (↑I : Type)
H : t₀ = 0 ∨ t₀ = 1
h :
  Eq (α := (↑I : Type)) (if h : i = i then (t₀, t).1 else (t₀, t).2 (Subtype.mk (p := fun (j : N) ↦ ¬j = i) i ⋯)) 0 ∨
    Eq (α := (↑I : Type)) (if h : i = i then (t₀, t).1 else (t₀, t).2 (Subtype.mk (p := fun (j : N) ↦ ¬j = i) i ⋯)) 1
h₁ h₂ h₃ h₄ : (t₀, t).1 = 0 ∨ (t₀, t).1 = 1
⊢ Eq (α := (↑I : Type))
      ((insertAt i : (a : (↑I : Type) × ({ j : N // j ≠ i } → (↑I : Type))) → N → (↑I : Type)) (t₀, t) i) 0 ∨
    Eq (α := (↑I : Type))
      ((insertAt i : (a : (↑I : Type) × ({ j : N // j ≠ i } → (↑I : Type))) → N → (↑I : Type)) (t₀, t) i) 1

Tactic:
rwa [funSplitAt_symm_apply, dif_pos rfl]

Premises used: Homeomorph.funSplitAt_symm_apply, dif_pos, rfl
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
Goal:
N : Type u_1
inst : DecidableEq N
i : N
t₀ : (↑I : Type)
t : { j : N // j ≠ i } → (↑I : Type)
j : { j : N // j ≠ i }
H : t j = 0 ∨ t j = 1
h :
  Eq (α := (↑I : Type))
      ((insertAt i : (a : (↑I : Type) × ({ j : N // j ≠ i } → (↑I : Type))) → N → (↑I : Type)) (t₀, t) (↑j : N)) 0 ∨
    Eq (α := (↑I : Type))
      ((insertAt i : (a : (↑I : Type) × ({ j : N // j ≠ i } → (↑I : Type))) → N → (↑I : Type)) (t₀, t) (↑j : N)) 1
⊢ Membership.mem (α := N → (↑I : Type)) (boundary N)
    ((insertAt i : (a : (↑I : Type) × ({ j : N // j ≠ i } → (↑I : Type))) → N → (↑I : Type)) (t₀, t) : N → (↑I : Type))

Tactic:
use j
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
Goal:
N : Type u_1
inst : DecidableEq N
i : N
t₀ : (↑I : Type)
t : { j : N // j ≠ i } → (↑I : Type)
j : { j : N // j ≠ i }
H : t j = 0 ∨ t j = 1
h :
  Eq (α := (↑I : Type))
      (if h : (↑j : N) = i then (t₀, t).1 else (t₀, t).2 (Subtype.mk (p := fun (j : N) ↦ ¬j = i) (↑j : N) ⋯)) 0 ∨
    Eq (α := (↑I : Type))
      (if h : (↑j : N) = i then (t₀, t).1 else (t₀, t).2 (Subtype.mk (p := fun (j : N) ↦ ¬j = i) (↑j : N) ⋯)) 1
h₁ :
  (t₀, t).2 (Subtype.mk (p := fun (j : N) ↦ ¬j = i) (↑j : N) ⋯) = 0 ∨
    (t₀, t).2 (Subtype.mk (p := fun (j : N) ↦ ¬j = i) (↑j : N) ⋯) = 1
h₂ h₃ h₄ h₅ : (t₀, t).2 j = 0 ∨ (t₀, t).2 j = 1
⊢ Eq (α := (↑I : Type))
      ((insertAt i : (a : (↑I : Type) × ({ j : N // j ≠ i } → (↑I : Type))) → N → (↑I : Type)) (t₀, t) (↑j : N)) 0 ∨
    Eq (α := (↑I : Type))
      ((insertAt i : (a : (↑I : Type) × ({ j : N // j ≠ i } → (↑I : Type))) → N → (↑I : Type)) (t₀, t) (↑j : N)) 1

Tactic:
rwa [funSplitAt_symm_apply, dif_neg j.prop, Subtype.coe_eta]

Premises used: Homeomorph.funSplitAt_symm_apply, dif_neg, Subtype.coe_eta, Subtype.prop
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
Goal:
N : Type u_1
X : Type u_2
inst : TopologicalSpace X
x : X
x_1 x_2 : (↑(Ω^ N X x) : Type (max u_1 u_2))
f : (N → (↑I : Type)) → X
continuous_toFun : Continuous[_, inst] f
property :
  Membership.mem (γ := Set (ContinuousMap.{u_1, u_2} (N → (↑I : Type)) X)) (Ω^ N X x)
    { toFun := f, continuous_toFun := continuous_toFun : ContinuousMap.{u_1, u_2} (N → (↑I : Type)) X }
g : (N → (↑I : Type)) → X
continuous_toFun_1 : Continuous[_, inst] g
property_1 :
  Membership.mem (γ := Set (ContinuousMap.{u_1, u_2} (N → (↑I : Type)) X)) (Ω^ N X x)
    { toFun := g, continuous_toFun := continuous_toFun_1 : ContinuousMap.{u_1, u_2} (N → (↑I : Type)) X }
h :
  Eq (α := (a : N → (↑I : Type)) → X)
    ((fun (f : (↑(Ω^ N X x) : Type (max u_1 u_2))) ↦
        ((⇑(↑f : C(N → (↑I : Type), X)) : (a : N → (↑I : Type)) → X) : (a : N → (↑I : Type)) → X))
      (Subtype.mk (p := fun (x_3 : ContinuousMap.{u_1, u_2} (N → (↑I : Type)) X) ↦
        Membership.mem (γ := Set (ContinuousMap.{u_1, u_2} (N → (↑I : Type)) X)) (Ω^ N X x) x_3)
        { toFun := f, continuous_toFun := continuous_toFun } property))
    ((fun (f : (↑(Ω^ N X x) : Type (max u_1 u_2))) ↦
        ((⇑(↑f : C(N → (↑I : Type), X)) : (a : N → (↑I : Type)) → X) : (a : N → (↑I : Type)) → X))
      (Subtype.mk (p := fun (x_3 : ContinuousMap.{u_1, u_2} (N → (↑I : Type)) X) ↦
        Membership.mem (γ := Set (ContinuousMap.{u_1, u_2} (N → (↑I : Type)) X)) (Ω^ N X x) x_3)
        { toFun := g, continuous_toFun := continuous_toFun_1 } property_1))
⊢ Subtype.mk (p := fun (x_3 : ContinuousMap.{u_1, u_2} (N → (↑I : Type)) X) ↦
      Membership.mem (γ := Set (ContinuousMap.{u_1, u_2} (N → (↑I : Type)) X)) (Ω^ N X x) x_3)
      { toFun := f, continuous_toFun := continuous_toFun : ContinuousMap.{u_1, u_2} (N → (↑I : Type)) X } property =
    Subtype.mk (p := fun (x_3 : ContinuousMap.{u_1, u_2} (N → (↑I : Type)) X) ↦
      Membership.mem (γ := Set (ContinuousMap.{u_1, u_2} (N → (↑I : Type)) X)) (Ω^ N X x) x_3)
      { toFun := g, continuous_toFun := continuous_toFun_1 } property_1

Tactic:
congr
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
Goal:
N : Type u_1
X : Type u_2
inst : TopologicalSpace X
x : X
f : (↑(Ω^ N X x) : Type (max u_1 u_2))
⊢ Eq (α := (a : N → (↑I : Type)) → X) (⇑(↑f : C(N → (↑I : Type), X)) : (a : N → (↑I : Type)) → X)
    (⇑f : (a : N → (↑I : Type)) → X)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
Goal:
N : Type u_1
X : Type u_2
inst : TopologicalSpace X
x : X
f g : (↑(Ω^ N X x) : Type (max u_1 u_2))
H :
  ∀ (y : N → (↑I : Type)),
    Eq.{u_2 + 1} (α := X) ((f : (a : N → (↑I : Type)) → X) y : X) ((g : (a : N → (↑I : Type)) → X) y : X)
⊢ f = g

Tactic:
DFunLike.coe_injective' (funext H)

Premises used: funext, DFunLike.coe_injective'
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
Goal:
N : Type u_1
X : Type u_2
inst : TopologicalSpace X
x : X
f : ContinuousMap.{u_1, u_2} (N → (↑I : Type)) X
H : Membership.mem (γ := Set (ContinuousMap.{u_1, u_2} (N → (↑I : Type)) X)) (Ω^ N X x) f
y : N → (↑I : Type)
⊢ Eq.{u_2 + 1} (α := X)
    ((Subtype.mk (p := fun (x_1 : ContinuousMap.{u_1, u_2} (N → (↑I : Type)) X) ↦
            Membership.mem (γ := Set (ContinuousMap.{u_1, u_2} (N → (↑I : Type)) X)) (Ω^ N X x) x_1) f H :
          (a : N → (↑I : Type)) → X)
        y :
      X)
    ((f : (a : N → (↑I : Type)) → X) y : X)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
Goal:
N : Type u_1
X : Type u_2
inst : TopologicalSpace X
x : X
⊢ ContinuousEval (↑(Ω^ N X x) : Type (max u_1 u_2)) (N → (↑I : Type)) X

Tactic:
.of_continuous_forget continuous_subtype_val

Premises used: continuous_subtype_val, ContinuousEval.of_continuous_forget
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
Goal:
N : Type u_1
X : Type u_2
inst : TopologicalSpace X
x : X
⊢ ContinuousEvalConst (↑(Ω^ N X x) : Type (max u_1 u_2)) (N → (↑I : Type)) X

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
Goal:
N : Type u_1
X : Type u_2
inst : TopologicalSpace X
x : X
f : (↑(Ω^ N X x) : Type (max u_1 u_2))
g : (N → (↑I : Type)) → X
h : g = (⇑f : (a : N → (↑I : Type)) → X)
⊢ Membership.mem (γ := Set (ContinuousMap.{u_1, u_2} (N → (↑I : Type)) X)) (Ω^ N X x) (↑f : C(N → (↑I : Type), X))

Tactic:
f.2

Premises used: Subtype.property
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
Goal:
N : Type u_1
X : Type u_2
inst : TopologicalSpace X
x : X
f : (↑(Ω^ N X x) : Type (max u_1 u_2))
g : (N → (↑I : Type)) → X
h : g = (⇑f : (a : N → (↑I : Type)) → X)
⊢ Membership.mem (γ := Set (ContinuousMap.{u_1, u_2} (N → (↑I : Type)) X)) (Ω^ N X x)
    { toFun := g, continuous_toFun := ⋯ }

Tactic:
convert! f.2

Premises used: Subtype.property
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
Goal:
N : Type u_1
X : Type u_2
inst : TopologicalSpace X
x : X
f : (↑(Ω^ N X x) : Type (max u_1 u_2))
g : (N → (↑I : Type)) → X
h : g = (⇑f : (a : N → (↑I : Type)) → X)
⊢ (⇑(copy f g h) : (a : N → (↑I : Type)) → X) = g

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
Goal:
N : Type u_1
X : Type u_2
inst : TopologicalSpace X
x : X
f : (↑(Ω^ N X x) : Type (max u_1 u_2))
g : (N → (↑I : Type)) → X
h : g = (⇑f : (a : N → (↑I : Type)) → X)
H :
  ∀ (x_1 : N → (↑I : Type)),
    Eq.{u_2 + 1} (α := X) ((copy f g h : (a : N → (↑I : Type)) → X) x_1 : X) ((f : (a : N → (↑I : Type)) → X) x_1 : X)
⊢ copy f g h = f

Tactic:
ext x
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
Goal:
N : Type u_1
X : Type u_2
inst : TopologicalSpace X
x_1 : X
f : (↑(Ω^ N X x_1) : Type (max u_1 u_2))
g : (N → (↑I : Type)) → X
h : g = (⇑f : (a : N → (↑I : Type)) → X)
x : N → (↑I : Type)
⊢ Eq.{u_2 + 1} (α := X) ((copy f g h : (a : N → (↑I : Type)) → X) x : X) ((f : (a : N → (↑I : Type)) → X) x : X)

Tactic:
congr_fun h x

Premises used: congr_fun
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
Goal:
N : Type u_1
X : Type u_2
inst : TopologicalSpace X
x_1 : X
f : (↑(Ω^ N X x_1) : Type (max u_1 u_2))
g : (N → (↑I : Type)) → X
h : g = (⇑f : (a : N → (↑I : Type)) → X)
x : N → (↑I : Type)
⊢ Eq.{u_2 + 1} (α := X) ((copy f g h : (a : N → (↑I : Type)) → X) x : X) ((f : (a : N → (↑I : Type)) → X) x : X)

Tactic:
exact congr_fun h x

Premises used: congr_fun
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
Goal:
N : Type u_1
X : Type u_2
inst : TopologicalSpace X
x : X
f : (↑(Ω^ N X x) : Type (max u_1 u_2))
⊢ ∀ y ∈ Cube.boundary N, (f : (a : N → (↑I : Type)) → X) y = x

Tactic:
f.2

Premises used: Set.Mem, setOf, GenLoop, Subtype.property
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
Goal:
N : Type u_1
X : Type u_2
inst : TopologicalSpace X
x : X
t : N → (↑I : Type)
⊢ (const : (a : N → (↑I : Type)) → X) t = x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
Goal:
N : Type u_1
X : Type u_2
inst : TopologicalSpace X
x_1 : X
M : Type u_3
x : X
e : M ≃ N
p : (↑(Ω^ M X x) : Type (max u_2 u_3))
⊢ Continuous.{u_1, u_3} (Y := M → (↑I : Type)) fun (t : N → (↑I : Type)) (m : M) ↦ t ((e : (a : M) → N) m)

Tactic:
fun_prop
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
Goal:
N : Type u_1
X : Type u_2
inst : TopologicalSpace X
x_1 : X
M : Type u_3
x : X
e : M ≃ N
p : (↑(Ω^ M X x) : Type (max u_2 u_3))
y : N → (↑I : Type)
h : y ∈ Cube.boundary N
n : N
hn : y n = 0 ∨ y n = 1
⊢ y ((e : (a : M) → N) ((e.symm : (a : N) → M) n : M)) = 0 ∨ y ((e : (a : M) → N) ((e.symm : (a : N) → M) n : M)) = 1

Tactic:
simpa using hn
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
Goal:
N : Type u_1
X : Type u_2
inst : TopologicalSpace X
x_1 : X
M : Type u_3
x : X
e : M ≃ N
p : (↑(Ω^ M X x) : Type (max u_2 u_3))
y : N → (↑I : Type)
h : y ∈ Cube.boundary N
n : N
hn : y n = 0 ∨ y n = 1
⊢ ((↑p : C(M → (↑I : Type), X)).comp
          { toFun := fun (t : N → (↑I : Type)) (m : M) ↦ t ((e : (a : M) → N) m), continuous_toFun := ⋯ :
            ContinuousMap.{u_1, u_3} (N → (↑I : Type)) (M → (↑I : Type)) } :
        (a : N → (↑I : Type)) → X)
      y =
    x

Tactic:
simpa using p.2 _ ⟨e.symm n, by simpa using hn⟩

Premises used: Exists.intro, Equiv.symm, DFunLike.coe, Subtype.property
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
Goal:
N : Type u_1
X : Type u_2
inst : TopologicalSpace X
x_1 : X
M : Type u_3
x : X
e : M ≃ N
p : (↑(Ω^ N X x) : Type (max u_1 u_2))
⊢ Continuous.{u_3, u_1} (Y := N → (↑I : Type)) fun (t : M → (↑I : Type)) (n : N) ↦ t ((e.symm : (a : N) → M) n)

Tactic:
fun_prop
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
Goal:
N : Type u_1
X : Type u_2
inst : TopologicalSpace X
x_1 : X
M : Type u_3
x : X
e : M ≃ N
p : (↑(Ω^ N X x) : Type (max u_1 u_2))
y : M → (↑I : Type)
h : y ∈ Cube.boundary M
m : M
hm : y m = 0 ∨ y m = 1
⊢ y ((e.symm : (a : N) → M) ((e : (a : M) → N) m : N)) = 0 ∨ y ((e.symm : (a : N) → M) ((e : (a : M) → N) m : N)) = 1

Tactic:
simpa using hm
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
Goal:
N : Type u_1
X : Type u_2
inst : TopologicalSpace X
x_1 : X
M : Type u_3
x : X
e : M ≃ N
p : (↑(Ω^ N X x) : Type (max u_1 u_2))
y : M → (↑I : Type)
h : y ∈ Cube.boundary M
m : M
hm : y m = 0 ∨ y m = 1
⊢ ((↑p : C(N → (↑I : Type), X)).comp
          { toFun := fun (t : M → (↑I : Type)) (n : N) ↦ t ((e.symm : (a : N) → M) n), continuous_toFun := ⋯ :
            ContinuousMap.{u_3, u_1} (M → (↑I : Type)) (N → (↑I : Type)) } :
        (a : M → (↑I : Type)) → X)
      y =
    x

Tactic:
simpa using p.2 _ ⟨e m, by simpa using hm⟩

Premises used: Exists.intro, DFunLike.coe, Subtype.property
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
Goal:
N : Type u_1
X : Type u_2
inst : TopologicalSpace X
x_1 : X
M : Type u_3
x : X
e : M ≃ N
p : (↑(Ω^ M X x) : Type (max u_2 u_3))
H :
  ∀ (t : M → (↑I : Type)),
    Eq.{u_2 + 1} (α := X)
      (((fun (p : (↑(Ω^ N X x) : Type (max u_1 u_2))) ↦
                (Subtype.mk (p := fun (x_2 : ContinuousMap.{u_3, u_2} (M → (↑I : Type)) X) ↦
                    Membership.mem (γ := Set (ContinuousMap.{u_3, u_2} (M → (↑I : Type)) X)) (Ω^ M X x) x_2)
                    ((↑p : C(N → (↑I : Type), X)).comp
                      { toFun := fun (t : M → (↑I : Type)) (n : N) ↦ t ((e.symm : (a : N) → M) n),
                        continuous_toFun := ⋯ })
                    ⋯ :
                  { x_2 : ContinuousMap.{u_3, u_2} (M → (↑I : Type)) X //
                    Membership.mem (γ := Set (ContinuousMap.{u_3, u_2} (M → (↑I : Type)) X)) (Ω^ M X x) x_2 }))
              ((fun (p : (↑(Ω^ M X x) : Type (max u_2 u_3))) ↦
                  (Subtype.mk (p := fun (x_2 : ContinuousMap.{u_1, u_2} (N → (↑I : Type)) X) ↦
                      Membership.mem (γ := Set (ContinuousMap.{u_1, u_2} (N → (↑I : Type)) X)) (Ω^ N X x) x_2)
                      ((↑p : C(M → (↑I : Type), X)).comp
                        { toFun := fun (t : N → (↑I : Type)) (m : M) ↦ t ((e : (a : M) → N) m), continuous_toFun := ⋯ })
                      ⋯ :
                    { x_2 : ContinuousMap.{u_1, u_2} (N → (↑I : Type)) X //
                      Membership.mem (γ := Set (ContinuousMap.{u_1, u_2} (N → (↑I : Type)) X)) (Ω^ N X x) x_2 }))
                p) :
            (a : M → (↑I : Type)) → X)
          t :
        X)
      ((p : (a : M → (↑I : Type)) → X) t : X)
⊢ (fun (p : (↑(Ω^ N X x) : Type (max u_1 u_2))) ↦
        (Subtype.mk (p := fun (x_2 : ContinuousMap.{u_3, u_2} (M → (↑I : Type)) X) ↦
            Membership.mem (γ := Set (ContinuousMap.{u_3, u_2} (M → (↑I : Type)) X)) (Ω^ M X x) x_2)
            ((↑p : C(N → (↑I : Type), X)).comp
              { toFun := fun (t : M → (↑I : Type)) (n : N) ↦ t ((e.symm : (a : N) → M) n), continuous_toFun := ⋯ })
            ⋯ :
          { x_2 : ContinuousMap.{u_3, u_2} (M → (↑I : Type)) X //
            Membership.mem (γ := Set (ContinuousMap.{u_3, u_2} (M → (↑I : Type)) X)) (Ω^ M X x) x_2 }))
      ((fun (p : (↑(Ω^ M X x) : Type (max u_2 u_3))) ↦
          (Subtype.mk (p := fun (x_2 : ContinuousMap.{u_1, u_2} (N → (↑I : Type)) X) ↦
              Membership.mem (γ := Set (ContinuousMap.{u_1, u_2} (N → (↑I : Type)) X)) (Ω^ N X x) x_2)
              ((↑p : C(M → (↑I : Type), X)).comp
                { toFun := fun (t : N → (↑I : Type)) (m : M) ↦ t ((e : (a : M) → N) m), continuous_toFun := ⋯ })
              ⋯ :
            { x_2 : ContinuousMap.{u_1, u_2} (N → (↑I : Type)) X //
              Membership.mem (γ := Set (ContinuousMap.{u_1, u_2} (N → (↑I : Type)) X)) (Ω^ N X x) x_2 }))
        p) =
    p

Tactic:
ext t
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
Goal:
N : Type u_1
X : Type u_2
inst : TopologicalSpace X
x_1 : X
M : Type u_3
x : X
e : M ≃ N
p : (↑(Ω^ M X x) : Type (max u_2 u_3))
t : M → (↑I : Type)
⊢ Eq.{u_2 + 1} (α := X)
    (((fun (p : (↑(Ω^ N X x) : Type (max u_1 u_2))) ↦
              (Subtype.mk (p := fun (x_2 : ContinuousMap.{u_3, u_2} (M → (↑I : Type)) X) ↦
                  Membership.mem (γ := Set (ContinuousMap.{u_3, u_2} (M → (↑I : Type)) X)) (Ω^ M X x) x_2)
                  ((↑p : C(N → (↑I : Type), X)).comp
                    { toFun := fun (t : M → (↑I : Type)) (n : N) ↦ t ((e.symm : (a : N) → M) n),
                      continuous_toFun := ⋯ })
                  ⋯ :
                { x_2 : ContinuousMap.{u_3, u_2} (M → (↑I : Type)) X //
                  Membership.mem (γ := Set (ContinuousMap.{u_3, u_2} (M → (↑I : Type)) X)) (Ω^ M X x) x_2 }))
            ((fun (p : (↑(Ω^ M X x) : Type (max u_2 u_3))) ↦
                (Subtype.mk (p := fun (x_2 : ContinuousMap.{u_1, u_2} (N → (↑I : Type)) X) ↦
                    Membership.mem (γ := Set (ContinuousMap.{u_1, u_2} (N → (↑I : Type)) X)) (Ω^ N X x) x_2)
                    ((↑p : C(M → (↑I : Type), X)).comp
                      { toFun := fun (t : N → (↑I : Type)) (m : M) ↦ t ((e : (a : M) → N) m), continuous_toFun := ⋯ })
                    ⋯ :
                  { x_2 : ContinuousMap.{u_1, u_2} (N → (↑I : Type)) X //
                    Membership.mem (γ := Set (ContinuousMap.{u_1, u_2} (N → (↑I : Type)) X)) (Ω^ N X x) x_2 }))
              p) :
          (a : M → (↑I : Type)) → X)
        t :
      X)
    ((p : (a : M → (↑I : Type)) → X) t : X)

Tactic:
simp