awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Homotopy.Path
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p₀ q₀ : Path x₀ x₁
p₁ q₁ : Path x₁ x₂
F : p₀.Homotopy q₀
G : p₁.Homotopy q₁
⊢ Continuous (Y := (↑I : Type) × (↑I : Type)) fun (x : (↑I : Type) × (↑I : Type)) ↦
    (x.1, Set.projIcc 0 1 extend._proof_2 (2 * (↑x.2 : ℝ)))

Tactic:
fun_prop
-- Module: Mathlib.Topology.Homotopy.Path
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p₀ q₀ : Path x₀ x₁
p₁ q₁ : Path x₁ x₂
F : p₀.Homotopy q₀
G : p₁.Homotopy q₁
⊢ Continuous (Y := (↑I : Type) × (↑I : Type)) fun (x : (↑I : Type) × (↑I : Type)) ↦
    (x.1, Set.projIcc 0 1 extend._proof_2 (2 * (↑x.2 : ℝ) - 1))

Tactic:
fun_prop
-- Module: Mathlib.Topology.Homotopy.Path
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p₀ q₀ : Path x₀ x₁
p₁ q₁ : Path x₁ x₂
F : p₀.Homotopy q₀
G : p₁.Homotopy q₁
x : (↑I : Type) × (↑I : Type)
hx : (↑x.2 : ℝ) = 1 / 2
⊢ Eq (α := X) (((F.eval x.1).extend : (a : ℝ) → X) (2 * (↑x.2 : ℝ)) : X)
    (((G.eval x.1).extend : (a : ℝ) → X) (2 * (↑x.2 : ℝ) - 1) : X)

Tactic:
norm_num [hx]
-- Module: Mathlib.Topology.Homotopy.Path
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p₀ q₀ : Path x₀ x₁
p₁ q₁ : Path x₁ x₂
F : p₀.Homotopy q₀
G : p₁.Homotopy q₁
x : (↑I : Type)
⊢ Eq (α := X)
    (if (↑(0, x).2 : ℝ) ≤ 1 / 2 then ((F.eval (0, x).1).extend : (a : ℝ) → X) (2 * (↑(0, x).2 : ℝ))
      else ((G.eval (0, x).1).extend : (a : ℝ) → X) (2 * (↑(0, x).2 : ℝ) - 1) :
      X)
    (((p₀.trans p₁).toContinuousMap : (a : (↑I : Type)) → X) x : X)

Tactic:
simp [Path.trans]

Premises used: Path.trans
-- Module: Mathlib.Topology.Homotopy.Path
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p₀ q₀ : Path x₀ x₁
p₁ q₁ : Path x₁ x₂
F : p₀.Homotopy q₀
G : p₁.Homotopy q₁
x : (↑I : Type)
⊢ Eq (α := X)
    (if (↑(1, x).2 : ℝ) ≤ 1 / 2 then ((F.eval (1, x).1).extend : (a : ℝ) → X) (2 * (↑(1, x).2 : ℝ))
      else ((G.eval (1, x).1).extend : (a : ℝ) → X) (2 * (↑(1, x).2 : ℝ) - 1) :
      X)
    (((q₀.trans q₁).toContinuousMap : (a : (↑I : Type)) → X) x : X)

Tactic:
simp [Path.trans]

Premises used: Path.trans
-- Module: Mathlib.Topology.Homotopy.Path
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p₀ q₀ : Path x₀ x₁
p₁ q₁ : Path x₁ x₂
F : p₀.Homotopy q₀
G : p₁.Homotopy q₁
x t : (↑I : Type)
ht : Membership.mem (γ := Set (↑I : Type)) {0, 1} t
inl :
  ∀ (ht : t = 0),
    Eq (α := X)
      (({
              toFun := fun (x_1 : (↑I : Type)) ↦
                if (↑(x, x_1).2 : ℝ) ≤ 1 / 2 then ((F.eval (x, x_1).1).extend : (a : ℝ) → X) (2 * (↑(x, x_1).2 : ℝ))
                else ((G.eval (x, x_1).1).extend : (a : ℝ) → X) (2 * (↑(x, x_1).2 : ℝ) - 1),
              continuous_toFun := ⋯ : C((↑I : Type), X) } :
            (a : (↑I : Type)) → X)
          t :
        X)
      (((p₀.trans p₁).toContinuousMap : (a : (↑I : Type)) → X) t : X)
inr :
  ∀ (ht : Membership.mem (γ := Set (↑I : Type)) {1} t),
    Eq (α := X)
      (({
              toFun := fun (x_1 : (↑I : Type)) ↦
                if (↑(x, x_1).2 : ℝ) ≤ 1 / 2 then ((F.eval (x, x_1).1).extend : (a : ℝ) → X) (2 * (↑(x, x_1).2 : ℝ))
                else ((G.eval (x, x_1).1).extend : (a : ℝ) → X) (2 * (↑(x, x_1).2 : ℝ) - 1),
              continuous_toFun := ⋯ : C((↑I : Type), X) } :
            (a : (↑I : Type)) → X)
          t :
        X)
      (((p₀.trans p₁).toContinuousMap : (a : (↑I : Type)) → X) t : X)
⊢ Eq (α := X)
    (({
            toFun := fun (x_1 : (↑I : Type)) ↦
              if (↑(x, x_1).2 : ℝ) ≤ 1 / 2 then ((F.eval (x, x_1).1).extend : (a : ℝ) → X) (2 * (↑(x, x_1).2 : ℝ))
              else ((G.eval (x, x_1).1).extend : (a : ℝ) → X) (2 * (↑(x, x_1).2 : ℝ) - 1),
            continuous_toFun := ⋯ : C((↑I : Type), X) } :
          (a : (↑I : Type)) → X)
        t :
      X)
    (((p₀.trans p₁).toContinuousMap : (a : (↑I : Type)) → X) t : X)

Tactic:
rcases ht with ht | ht
-- Module: Mathlib.Topology.Homotopy.Path
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p₀ q₀ : Path x₀ x₁
p₁ q₁ : Path x₁ x₂
F : p₀.Homotopy q₀
G : p₁.Homotopy q₁
x t : (↑I : Type)
ht : t = 0
⊢ Eq (α := X)
    (({
            toFun := fun (x_1 : (↑I : Type)) ↦
              if (↑(x, x_1).2 : ℝ) ≤ 1 / 2 then ((F.eval (x, x_1).1).extend : (a : ℝ) → X) (2 * (↑(x, x_1).2 : ℝ))
              else ((G.eval (x, x_1).1).extend : (a : ℝ) → X) (2 * (↑(x, x_1).2 : ℝ) - 1),
            continuous_toFun := ⋯ : C((↑I : Type), X) } :
          (a : (↑I : Type)) → X)
        t :
      X)
    (((p₀.trans p₁).toContinuousMap : (a : (↑I : Type)) → X) t : X)

Tactic:
norm_num [ht]
-- Module: Mathlib.Topology.Homotopy.Path
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p₀ q₀ : Path x₀ x₁
p₁ q₁ : Path x₁ x₂
F : p₀.Homotopy q₀
G : p₁.Homotopy q₁
x t : (↑I : Type)
ht : Membership.mem (γ := Set (↑I : Type)) {1} t
⊢ t = 1

Tactic:
rw [Set.mem_singleton_iff] at ht

Premises used: Set.mem_singleton_iff
-- Module: Mathlib.Topology.Homotopy.Path
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p₀ q₀ : Path x₀ x₁
p₁ q₁ : Path x₁ x₂
F : p₀.Homotopy q₀
G : p₁.Homotopy q₁
x t : (↑I : Type)
ht : t = 1
⊢ Eq (α := X)
    (({
            toFun := fun (x_1 : (↑I : Type)) ↦
              if (↑(x, x_1).2 : ℝ) ≤ 1 / 2 then ((F.eval (x, x_1).1).extend : (a : ℝ) → X) (2 * (↑(x, x_1).2 : ℝ))
              else ((G.eval (x, x_1).1).extend : (a : ℝ) → X) (2 * (↑(x, x_1).2 : ℝ) - 1),
            continuous_toFun := ⋯ : C((↑I : Type), X) } :
          (a : (↑I : Type)) → X)
        t :
      X)
    (((p₀.trans p₁).toContinuousMap : (a : (↑I : Type)) → X) t : X)

Tactic:
norm_num [ht]
-- Module: Mathlib.Topology.Homotopy.Path
Goal:
X : Type u
inst : TopologicalSpace X
x₀ x₁ x₂ : X
p₀ q₀ : Path x₀ x₁
p₁ q₁ : Path x₁ x₂
F : p₀.Homotopy q₀
G : p₁.Homotopy q₁
x : (↑I : Type) × (↑I : Type)
pos :
  ∀ (h : (↑x.2 : ℝ) ≤ 1 / 2),
    Eq (α := X) (((F.eval x.1).extend : (a : ℝ) → X) (2 * (↑x.2 : ℝ)) : X)
      ((F.eval x.1 : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑x.2 : ℝ)) ⋯) : X)
neg :
  ∀ (h : ¬(↑x.2 : ℝ) ≤ 1 / 2),
    Eq (α := X) (((G.eval x.1).extend : (a : ℝ) → X) (2 * (↑x.2 : ℝ) - 1) : X)
      ((G.eval x.1 : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑x.2 : ℝ) - 1) ⋯) : X)
⊢ Eq (α := X)
    (if (↑x.2 : ℝ) ≤ 1 / 2 then ((F.eval x.1).extend : (a : ℝ) → X) (2 * (↑x.2 : ℝ))
      else ((G.eval x.1).extend : (a : ℝ) → X) (2 * (↑x.2 : ℝ) - 1) :
      X)
    (if h : (↑x.2 : ℝ) ≤ 1 / 2 then
        (F.eval x.1 : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑x.2 : ℝ)) ⋯)
      else (G.eval x.1 : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑x.2 : ℝ) - 1) ⋯) :
      X)

Tactic:
split_ifs
-- Module: Mathlib.Topology.Homotopy.Path
Goal:
X : Type u
inst : TopologicalSpace X
x₀ x₁ x₂ : X
p₀ q₀ : Path x₀ x₁
p₁ q₁ : Path x₁ x₂
F : p₀.Homotopy q₀
G : p₁.Homotopy q₁
x : (↑I : Type) × (↑I : Type)
h : (↑x.2 : ℝ) ≤ 1 / 2
⊢ Eq (α := X) (((F.eval x.1).extend : (a : ℝ) → X) (2 * (↑x.2 : ℝ)) : X)
    ((F.eval x.1 : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑x.2 : ℝ)) ⋯) : X)

Tactic:
Path.extend_apply _ _

Premises used: Path.extend_apply
-- Module: Mathlib.Topology.Homotopy.Path
Goal:
X : Type u
inst : TopologicalSpace X
x₀ x₁ x₂ : X
p₀ q₀ : Path x₀ x₁
p₁ q₁ : Path x₁ x₂
F : p₀.Homotopy q₀
G : p₁.Homotopy q₁
x : (↑I : Type) × (↑I : Type)
h : (↑x.2 : ℝ) ≤ 1 / 2
⊢ Eq (α := X) (((F.eval x.1).extend : (a : ℝ) → X) (2 * (↑x.2 : ℝ)) : X)
    ((F.eval x.1 : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑x.2 : ℝ)) ⋯) : X)

Tactic:
exact Path.extend_apply _ _

Premises used: Path.extend_apply
-- Module: Mathlib.Topology.Homotopy.Path
Goal:
X : Type u
inst : TopologicalSpace X
x₀ x₁ x₂ : X
p₀ q₀ : Path x₀ x₁
p₁ q₁ : Path x₁ x₂
F : p₀.Homotopy q₀
G : p₁.Homotopy q₁
x : (↑I : Type) × (↑I : Type)
h : ¬(↑x.2 : ℝ) ≤ 1 / 2
⊢ Eq (α := X) (((G.eval x.1).extend : (a : ℝ) → X) (2 * (↑x.2 : ℝ) - 1) : X)
    ((G.eval x.1 : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑x.2 : ℝ) - 1) ⋯) : X)

Tactic:
Path.extend_apply _ _

Premises used: Path.extend_apply
-- Module: Mathlib.Topology.Homotopy.Path
Goal:
X : Type u
inst : TopologicalSpace X
x₀ x₁ x₂ : X
p₀ q₀ : Path x₀ x₁
p₁ q₁ : Path x₁ x₂
F : p₀.Homotopy q₀
G : p₁.Homotopy q₁
x : (↑I : Type) × (↑I : Type)
h : ¬(↑x.2 : ℝ) ≤ 1 / 2
⊢ Eq (α := X) (((G.eval x.1).extend : (a : ℝ) → X) (2 * (↑x.2 : ℝ) - 1) : X)
    ((G.eval x.1 : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑x.2 : ℝ) - 1) ⋯) : X)

Tactic:
exact Path.extend_apply _ _

Premises used: Path.extend_apply
-- Module: Mathlib.Topology.Homotopy.Path
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p₀ q₀ : Path x₀ x₁
p₁ q₁ : Path x₁ x₂
F : p₀.Homotopy q₀
G : p₁.Homotopy q₁
t : (↑I : Type)
⊢ 0 ≤ 1 / 2

Tactic:
norm_num
-- Module: Mathlib.Topology.Homotopy.Path
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p₀ q₀ : Path x₀ x₁
p₁ q₁ : Path x₁ x₂
F : p₀.Homotopy q₀
G : p₁.Homotopy q₁
t : (↑I : Type)
⊢ 1 / 2 ≤ 1

Tactic:
norm_num
-- Module: Mathlib.Topology.Homotopy.Path
Goal:
X : Type u
inst : TopologicalSpace X
x₀ x₁ x₂ : X
p₀ q₀ : Path x₀ x₁
p₁ q₁ : Path x₁ x₂
F : p₀.Homotopy q₀
G : p₁.Homotopy q₁
t : (↑I : Type)
⊢ (if (↑(t, Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (1 / 2) ⋯).2 : ℝ) ≤ 1 / 2 then
      ((F.eval (t, Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (1 / 2) ⋯).1).extend : (a : ℝ) → X)
        (2 * (↑(t, Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (1 / 2) ⋯).2 : ℝ))
    else
      ((G.eval (t, Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (1 / 2) ⋯).1).extend : (a : ℝ) → X)
        (2 * (↑(t, Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (1 / 2) ⋯).2 : ℝ) - 1)) =
    x₁

Tactic:
norm_num
-- Module: Mathlib.Topology.Homotopy.Path
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
f : (↑I : Type) → (↑I : Type)
hf : Continuous f
hf₀ : f 0 = 0
hf₁ : f 1 = 1
x : (↑I : Type) × (↑I : Type)
⊢ 0 ≤ (↑(σ x.1) : ℝ)

Tactic:
unit_interval
-- Module: Mathlib.Topology.Homotopy.Path
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
f : (↑I : Type) → (↑I : Type)
hf : Continuous f
hf₀ : f 0 = 0
hf₁ : f 1 = 1
x : (↑I : Type) × (↑I : Type)
⊢ 0 ≤ (↑x.1 : ℝ)

Tactic:
unit_interval
-- Module: Mathlib.Topology.Homotopy.Path
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
f : (↑I : Type) → (↑I : Type)
hf : Continuous f
hf₀ : f 0 = 0
hf₁ : f 1 = 1
x : (↑I : Type) × (↑I : Type)
⊢ (↑(σ x.1) : ℝ) + (↑x.1 : ℝ) = 1

Tactic:
simp
-- Module: Mathlib.Topology.Homotopy.Path
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
f : (↑I : Type) → (↑I : Type)
hf : Continuous f
hf₀ : f 0 = 0
hf₁ : f 1 = 1
⊢ Continuous.{0, u} (Y := X) fun (x : (↑I : Type) × (↑I : Type)) ↦
    (p : (a : (↑I : Type)) → X)
      (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) ((↑(σ x.1) : ℝ) * (↑x.2 : ℝ) + (↑x.1 : ℝ) * (↑(f x.2) : ℝ)) ⋯)

Tactic:
fun_prop
-- Module: Mathlib.Topology.Homotopy.Path
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
f : (↑I : Type) → (↑I : Type)
hf : Continuous f
hf₀ : f 0 = 0
hf₁ : f 1 = 1
x : (↑I : Type)
⊢ Eq (α := X)
    ((p : (a : (↑I : Type)) → X)
        (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I)
          ((↑(σ (0, x).1) : ℝ) * (↑(0, x).2 : ℝ) + (↑(0, x).1 : ℝ) * (↑(f (0, x).2) : ℝ)) ⋯) :
      X)
    ((p.toContinuousMap : (a : (↑I : Type)) → X) x : X)

Tactic:
norm_num
-- Module: Mathlib.Topology.Homotopy.Path
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
f : (↑I : Type) → (↑I : Type)
hf : Continuous f
hf₀ : f 0 = 0
hf₁ : f 1 = 1
x : (↑I : Type)
⊢ Eq (α := X)
    ((p : (a : (↑I : Type)) → X)
        (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I)
          ((↑(σ (1, x).1) : ℝ) * (↑(1, x).2 : ℝ) + (↑(1, x).1 : ℝ) * (↑(f (1, x).2) : ℝ)) ⋯) :
      X)
    (((p.reparam f hf hf₀ hf₁).toContinuousMap : (a : (↑I : Type)) → X) x : X)

Tactic:
norm_num
-- Module: Mathlib.Topology.Homotopy.Path
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
f : (↑I : Type) → (↑I : Type)
hf : Continuous f
hf₀ : f 0 = 0
hf₁ : f 1 = 1
t x : (↑I : Type)
hx : Membership.mem (γ := Set (↑I : Type)) {0, 1} x
inl :
  ∀ (hx : x = 0),
    Eq (α := X)
      (({
              toFun := fun (x : (↑I : Type)) ↦
                (p : (a : (↑I : Type)) → X)
                  (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I)
                    ((↑(σ (t, x).1) : ℝ) * (↑(t, x).2 : ℝ) + (↑(t, x).1 : ℝ) * (↑(f (t, x).2) : ℝ)) ⋯),
              continuous_toFun := ⋯ : C((↑I : Type), X) } :
            (a : (↑I : Type)) → X)
          x :
        X)
      ((p.toContinuousMap : (a : (↑I : Type)) → X) x : X)
inr :
  ∀ (hx : Membership.mem (γ := Set (↑I : Type)) {1} x),
    Eq (α := X)
      (({
              toFun := fun (x : (↑I : Type)) ↦
                (p : (a : (↑I : Type)) → X)
                  (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I)
                    ((↑(σ (t, x).1) : ℝ) * (↑(t, x).2 : ℝ) + (↑(t, x).1 : ℝ) * (↑(f (t, x).2) : ℝ)) ⋯),
              continuous_toFun := ⋯ : C((↑I : Type), X) } :
            (a : (↑I : Type)) → X)
          x :
        X)
      ((p.toContinuousMap : (a : (↑I : Type)) → X) x : X)
⊢ Eq (α := X)
    (({
            toFun := fun (x : (↑I : Type)) ↦
              (p : (a : (↑I : Type)) → X)
                (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I)
                  ((↑(σ (t, x).1) : ℝ) * (↑(t, x).2 : ℝ) + (↑(t, x).1 : ℝ) * (↑(f (t, x).2) : ℝ)) ⋯),
            continuous_toFun := ⋯ : C((↑I : Type), X) } :
          (a : (↑I : Type)) → X)
        x :
      X)
    ((p.toContinuousMap : (a : (↑I : Type)) → X) x : X)

Tactic:
rcases hx with hx | hx
-- Module: Mathlib.Topology.Homotopy.Path
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
f : (↑I : Type) → (↑I : Type)
hf : Continuous f
hf₀ : f 0 = 0
hf₁ : f 1 = 1
t x : (↑I : Type)
hx : x = 0
inl :
  Eq (α := X)
    (({
            toFun := fun (x : (↑I : Type)) ↦
              (p : (a : (↑I : Type)) → X)
                (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I)
                  ((↑(σ (t, x).1) : ℝ) * (↑(t, x).2 : ℝ) + (↑(t, x).1 : ℝ) * (↑(f (t, x).2) : ℝ)) ⋯),
            continuous_toFun := ⋯ : C((↑I : Type), X) } :
          (a : (↑I : Type)) → X)
        0 :
      X)
    ((p.toContinuousMap : (a : (↑I : Type)) → X) 0 : X)
⊢ Eq (α := X)
    (({
            toFun := fun (x : (↑I : Type)) ↦
              (p : (a : (↑I : Type)) → X)
                (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I)
                  ((↑(σ (t, x).1) : ℝ) * (↑(t, x).2 : ℝ) + (↑(t, x).1 : ℝ) * (↑(f (t, x).2) : ℝ)) ⋯),
            continuous_toFun := ⋯ : C((↑I : Type), X) } :
          (a : (↑I : Type)) → X)
        x :
      X)
    ((p.toContinuousMap : (a : (↑I : Type)) → X) x : X)

Tactic:
rw [hx]
-- Module: Mathlib.Topology.Homotopy.Path
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
f : (↑I : Type) → (↑I : Type)
hf : Continuous f
hf₀ : f 0 = 0
hf₁ : f 1 = 1
t x : (↑I : Type)
hx : x = 0
⊢ Eq (α := X)
    (({
            toFun := fun (x : (↑I : Type)) ↦
              (p : (a : (↑I : Type)) → X)
                (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I)
                  ((↑(σ (t, x).1) : ℝ) * (↑(t, x).2 : ℝ) + (↑(t, x).1 : ℝ) * (↑(f (t, x).2) : ℝ)) ⋯),
            continuous_toFun := ⋯ : C((↑I : Type), X) } :
          (a : (↑I : Type)) → X)
        0 :
      X)
    ((p.toContinuousMap : (a : (↑I : Type)) → X) 0 : X)

Tactic:
simp [hf₀]
-- Module: Mathlib.Topology.Homotopy.Path
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
f : (↑I : Type) → (↑I : Type)
hf : Continuous f
hf₀ : f 0 = 0
hf₁ : f 1 = 1
t x : (↑I : Type)
hx : Membership.mem (γ := Set (↑I : Type)) {1} x
⊢ x = 1

Tactic:
rw [Set.mem_singleton_iff] at hx

Premises used: Set.mem_singleton_iff
-- Module: Mathlib.Topology.Homotopy.Path
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
f : (↑I : Type) → (↑I : Type)
hf : Continuous f
hf₀ : f 0 = 0
hf₁ : f 1 = 1
t x : (↑I : Type)
hx : x = 1
inr :
  Eq (α := X)
    (({
            toFun := fun (x : (↑I : Type)) ↦
              (p : (a : (↑I : Type)) → X)
                (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I)
                  ((↑(σ (t, x).1) : ℝ) * (↑(t, x).2 : ℝ) + (↑(t, x).1 : ℝ) * (↑(f (t, x).2) : ℝ)) ⋯),
            continuous_toFun := ⋯ : C((↑I : Type), X) } :
          (a : (↑I : Type)) → X)
        1 :
      X)
    ((p.toContinuousMap : (a : (↑I : Type)) → X) 1 : X)
⊢ Eq (α := X)
    (({
            toFun := fun (x : (↑I : Type)) ↦
              (p : (a : (↑I : Type)) → X)
                (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I)
                  ((↑(σ (t, x).1) : ℝ) * (↑(t, x).2 : ℝ) + (↑(t, x).1 : ℝ) * (↑(f (t, x).2) : ℝ)) ⋯),
            continuous_toFun := ⋯ : C((↑I : Type), X) } :
          (a : (↑I : Type)) → X)
        x :
      X)
    ((p.toContinuousMap : (a : (↑I : Type)) → X) x : X)

Tactic:
rw [hx]
-- Module: Mathlib.Topology.Homotopy.Path
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
f : (↑I : Type) → (↑I : Type)
hf : Continuous f
hf₀ : f 0 = 0
hf₁ : f 1 = 1
t x : (↑I : Type)
hx : x = 1
⊢ Eq (α := X)
    (({
            toFun := fun (x : (↑I : Type)) ↦
              (p : (a : (↑I : Type)) → X)
                (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I)
                  ((↑(σ (t, x).1) : ℝ) * (↑(t, x).2 : ℝ) + (↑(t, x).1 : ℝ) * (↑(f (t, x).2) : ℝ)) ⋯),
            continuous_toFun := ⋯ : C((↑I : Type), X) } :
          (a : (↑I : Type)) → X)
        1 :
      X)
    ((p.toContinuousMap : (a : (↑I : Type)) → X) 1 : X)

Tactic:
simp [hf₁]
-- Module: Mathlib.Topology.Homotopy.Path
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p q : Path x₀ x₁
F : p.Homotopy q
⊢ ∀ (x : (↑I : Type)),
    Eq (α := X) ((F : (a : (↑I : Type) × (↑I : Type)) → X) ((0, x).1, σ (0, x).2) : X)
      ((p.symm.toContinuousMap : (a : (↑I : Type)) → X) x : X)

Tactic:
simp [Path.symm]

Premises used: Path.symm
-- Module: Mathlib.Topology.Homotopy.Path
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p q : Path x₀ x₁
F : p.Homotopy q
⊢ ∀ (x : (↑I : Type)),
    Eq (α := X) ((F : (a : (↑I : Type) × (↑I : Type)) → X) ((1, x).1, σ (1, x).2) : X)
      ((q.symm.toContinuousMap : (a : (↑I : Type)) → X) x : X)

Tactic:
simp [Path.symm]

Premises used: Path.symm
-- Module: Mathlib.Topology.Homotopy.Path
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p q : Path x₀ x₁
F : p.Homotopy q
t x : (↑I : Type)
hx : Membership.mem (γ := Set (↑I : Type)) {0, 1} x
inl :
  ∀ (hx : x = 0),
    Eq (α := X)
      (({ toFun := fun (x : (↑I : Type)) ↦ (F : (a : (↑I : Type) × (↑I : Type)) → X) ((t, x).1, σ (t, x).2),
              continuous_toFun := ⋯ : C((↑I : Type), X) } :
            (a : (↑I : Type)) → X)
          x :
        X)
      ((p.symm.toContinuousMap : (a : (↑I : Type)) → X) x : X)
inr :
  ∀ (hx : Membership.mem (γ := Set (↑I : Type)) {1} x),
    Eq (α := X)
      (({ toFun := fun (x : (↑I : Type)) ↦ (F : (a : (↑I : Type) × (↑I : Type)) → X) ((t, x).1, σ (t, x).2),
              continuous_toFun := ⋯ : C((↑I : Type), X) } :
            (a : (↑I : Type)) → X)
          x :
        X)
      ((p.symm.toContinuousMap : (a : (↑I : Type)) → X) x : X)
⊢ Eq (α := X)
    (({ toFun := fun (x : (↑I : Type)) ↦ (F : (a : (↑I : Type) × (↑I : Type)) → X) ((t, x).1, σ (t, x).2),
            continuous_toFun := ⋯ : C((↑I : Type), X) } :
          (a : (↑I : Type)) → X)
        x :
      X)
    ((p.symm.toContinuousMap : (a : (↑I : Type)) → X) x : X)

Tactic:
rcases hx with hx | hx
-- Module: Mathlib.Topology.Homotopy.Path
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p q : Path x₀ x₁
F : p.Homotopy q
t x : (↑I : Type)
hx : x = 0
inl :
  Eq (α := X)
    (({ toFun := fun (x : (↑I : Type)) ↦ (F : (a : (↑I : Type) × (↑I : Type)) → X) ((t, x).1, σ (t, x).2),
            continuous_toFun := ⋯ : C((↑I : Type), X) } :
          (a : (↑I : Type)) → X)
        0 :
      X)
    ((p.symm.toContinuousMap : (a : (↑I : Type)) → X) 0 : X)
⊢ Eq (α := X)
    (({ toFun := fun (x : (↑I : Type)) ↦ (F : (a : (↑I : Type) × (↑I : Type)) → X) ((t, x).1, σ (t, x).2),
            continuous_toFun := ⋯ : C((↑I : Type), X) } :
          (a : (↑I : Type)) → X)
        x :
      X)
    ((p.symm.toContinuousMap : (a : (↑I : Type)) → X) x : X)

Tactic:
rw [hx]
-- Module: Mathlib.Topology.Homotopy.Path
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p q : Path x₀ x₁
F : p.Homotopy q
t x : (↑I : Type)
hx : x = 0
⊢ Eq (α := X)
    (({ toFun := fun (x : (↑I : Type)) ↦ (F : (a : (↑I : Type) × (↑I : Type)) → X) ((t, x).1, σ (t, x).2),
            continuous_toFun := ⋯ : C((↑I : Type), X) } :
          (a : (↑I : Type)) → X)
        0 :
      X)
    ((p.symm.toContinuousMap : (a : (↑I : Type)) → X) 0 : X)

Tactic:
simp
-- Module: Mathlib.Topology.Homotopy.Path
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p q : Path x₀ x₁
F : p.Homotopy q
t x : (↑I : Type)
hx : Membership.mem (γ := Set (↑I : Type)) {1} x
⊢ x = 1

Tactic:
rw [Set.mem_singleton_iff] at hx

Premises used: Set.mem_singleton_iff
-- Module: Mathlib.Topology.Homotopy.Path
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p q : Path x₀ x₁
F : p.Homotopy q
t x : (↑I : Type)
hx : x = 1
inr :
  Eq (α := X)
    (({ toFun := fun (x : (↑I : Type)) ↦ (F : (a : (↑I : Type) × (↑I : Type)) → X) ((t, x).1, σ (t, x).2),
            continuous_toFun := ⋯ : C((↑I : Type), X) } :
          (a : (↑I : Type)) → X)
        1 :
      X)
    ((p.symm.toContinuousMap : (a : (↑I : Type)) → X) 1 : X)
⊢ Eq (α := X)
    (({ toFun := fun (x : (↑I : Type)) ↦ (F : (a : (↑I : Type) × (↑I : Type)) → X) ((t, x).1, σ (t, x).2),
            continuous_toFun := ⋯ : C((↑I : Type), X) } :
          (a : (↑I : Type)) → X)
        x :
      X)
    ((p.symm.toContinuousMap : (a : (↑I : Type)) → X) x : X)

Tactic:
rw [hx]
-- Module: Mathlib.Topology.Homotopy.Path
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p q : Path x₀ x₁
F : p.Homotopy q
t x : (↑I : Type)
hx : x = 1
⊢ Eq (α := X)
    (({ toFun := fun (x : (↑I : Type)) ↦ (F : (a : (↑I : Type) × (↑I : Type)) → X) ((t, x).1, σ (t, x).2),
            continuous_toFun := ⋯ : C((↑I : Type), X) } :
          (a : (↑I : Type)) → X)
        1 :
      X)
    ((p.symm.toContinuousMap : (a : (↑I : Type)) → X) 1 : X)

Tactic:
simp
-- Module: Mathlib.Topology.Homotopy.Path
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p q : Path x₀ x₁
F : p.Homotopy q
f : C(X, Y)
⊢ ∀ (x : (↑I : Type)),
    Eq (α := Y)
      (Function.comp (α := (↑I : Type) × (↑I : Type)) (β := X) (⇑f : (a : X) → Y)
          (⇑F : (a : (↑I : Type) × (↑I : Type)) → X) (0, x) :
        Y)
      (((p.map ⋯).toContinuousMap : (a : (↑I : Type)) → Y) x : Y)

Tactic:
simp
-- Module: Mathlib.Topology.Homotopy.Path
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p q : Path x₀ x₁
F : p.Homotopy q
f : C(X, Y)
⊢ ∀ (x : (↑I : Type)),
    Eq (α := Y)
      (Function.comp (α := (↑I : Type) × (↑I : Type)) (β := X) (⇑f : (a : X) → Y)
          (⇑F : (a : (↑I : Type) × (↑I : Type)) → X) (1, x) :
        Y)
      (((q.map ⋯).toContinuousMap : (a : (↑I : Type)) → Y) x : Y)

Tactic:
simp