-- Mathlib/Topology/Homotopy/HomotopyGroup.lean
theorem homotopicFrom (i : N) {p q : Ω^ N X x} :
    (toLoop i p).Homotopic (toLoop i q) → Homotopic p q

Proof state:
case refine_1
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : Path.Homotopy (toLoop i p) (toLoop i q)
x✝ : N → ↑I
⊢ ↑p (↑(Cube.insertAt i) (x✝ i, fun j => x✝ ↑j)) = ↑p x✝

Tactic:
apply congr_arg p

Result:
case refine_1
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : Path.Homotopy (toLoop i p) (toLoop i q)
x✝ : N → ↑I
⊢ ↑(Cube.insertAt i) (x✝ i, fun j => x✝ ↑j) = x✝

Proof state:
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
⊢ Path.Homotopic (toLoop i p) (toLoop i q) → Homotopic p q

Tactic:
refine Nonempty.map fun H => ⟨⟨homotopyFrom i H, ?_, ?_⟩, ?_⟩

Result:
case refine_1
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : Path.Homotopy (toLoop i p) (toLoop i q)
⊢ ∀ (x_1 : N → ↑I), (homotopyFrom i H).toFun (0, x_1) = ↑p x_1

case refine_2
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : Path.Homotopy (toLoop i p) (toLoop i q)
⊢ ∀ (x_1 : N → ↑I), (homotopyFrom i H).toFun (1, x_1) = ↑q x_1

case refine_3
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : Path.Homotopy (toLoop i p) (toLoop i q)
⊢ ∀ (t : ↑I),
    ∀ x_1 ∈ Cube.boundary N,
      {
            toFun := fun x_2 =>
              { toContinuousMap := homotopyFrom i H, map_zero_left := ?refine_1, map_one_left := ?refine_2 }.toFun
                (t, x_2),
            continuous_toFun := ⋯ }
          x_1 =
        ↑p x_1

Proof state:
case refine_2
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : Path.Homotopy (toLoop i p) (toLoop i q)
x✝ : N → ↑I
⊢ Function.uncurry (fun x_1 y => Function.uncurry (fun x_2 y => ↑(H (x_1, x_2)) y) y)
      (Prod.map id ⇑(Cube.splitAt i) (1, x✝)) =
    ↑q x✝

Tactic:
simp only [Prod.map_apply, id_eq, funSplitAt_apply,
  Function.uncurry_apply_pair, ContinuousMap.HomotopyWith.apply_zero,
  ContinuousMap.HomotopyWith.apply_one, ne_eq, Path.coe_toContinuousMap, toLoop_apply_coe,
  ContinuousMap.curry_apply, ContinuousMap.comp_apply]

Result:
case refine_2
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : Path.Homotopy (toLoop i p) (toLoop i q)
x✝ : N → ↑I
⊢ ↑q (↑(Cube.insertAt i) (x✝ i, fun j => x✝ ↑j)) = ↑q x✝

Proof state:
case refine_3
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : Path.Homotopy (toLoop i p) (toLoop i q)
⊢ ∀ (t : ↑I),
    ∀ x_1 ∈ Cube.boundary N,
      {
            toFun := fun x_2 =>
              { toContinuousMap := homotopyFrom i H, map_zero_left := ?refine_1, map_one_left := ?refine_2 }.toFun
                (t, x_2),
            continuous_toFun := ⋯ }
          x_1 =
        ↑p x_1

Tactic:
rintro t y ⟨j, jH⟩

Result:
case refine_3.intro
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : Path.Homotopy (toLoop i p) (toLoop i q)
t : ↑I
y : N → ↑I
j : N
jH : y j = 0 ∨ y j = 1
⊢ {
        toFun := fun x_1 =>
          { toContinuousMap := homotopyFrom i H, map_zero_left := ?refine_1, map_one_left := ?refine_2 }.toFun (t, x_1),
        continuous_toFun := ⋯ }
      y =
    ↑p y

Proof state:
case refine_3.intro.inl
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
p q : ↑(Ω^ N X x)
t : ↑I
y : N → ↑I
j : N
jH : y j = 0 ∨ y j = 1
H : Path.Homotopy (toLoop j p) (toLoop j q)
⊢ (↑(H (t, y j)) fun j_1 => y ↑j_1) = ↑p y

Tactic:
rw [H.eq_fst]

Result:
case refine_3.intro.inl
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
p q : ↑(Ω^ N X x)
t : ↑I
y : N → ↑I
j : N
jH : y j = 0 ∨ y j = 1
H : Path.Homotopy (toLoop j p) (toLoop j q)
⊢ (↑((toLoop j p).toContinuousMap (y j)) fun j_1 => y ↑j_1) = ↑p y

case refine_3.intro.inl.hx
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
p q : ↑(Ω^ N X x)
t : ↑I
y : N → ↑I
j : N
jH : y j = 0 ∨ y j = 1
H : Path.Homotopy (toLoop j p) (toLoop j q)
⊢ y j ∈ {0, 1}

Proof state:
case refine_3.intro
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : Path.Homotopy (toLoop i p) (toLoop i q)
t : ↑I
y : N → ↑I
j : N
jH : y j = 0 ∨ y j = 1
⊢ {
        toFun := fun x_1 =>
          { toContinuousMap := homotopyFrom i H, map_zero_left := ?refine_1, map_one_left := ?refine_2 }.toFun (t, x_1),
        continuous_toFun := ⋯ }
      y =
    ↑p y

Tactic:
erw [homotopyFrom_apply]

Result:
case refine_3.intro
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : Path.Homotopy (toLoop i p) (toLoop i q)
t : ↑I
y : N → ↑I
j : N
jH : y j = 0 ∨ y j = 1
⊢ Function.uncurry (fun x_1 y => Function.uncurry (fun x_2 y => ↑(H (x_1, x_2)) y) y)
      (Prod.map id ⇑(Cube.splitAt i) (t, y)) =
    ↑p y

Proof state:
case refine_1
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : Path.Homotopy (toLoop i p) (toLoop i q)
⊢ ∀ (x_1 : N → ↑I), (homotopyFrom i H).toFun (0, x_1) = ↑p x_1

case refine_2
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : Path.Homotopy (toLoop i p) (toLoop i q)
⊢ ∀ (x_1 : N → ↑I), (homotopyFrom i H).toFun (1, x_1) = ↑q x_1

Tactic:
all_goals
  intro
  apply (homotopyFrom_apply _ _ _).trans
  simp only [Prod.map_apply, id_eq, funSplitAt_apply,
    Function.uncurry_apply_pair, ContinuousMap.HomotopyWith.apply_zero,
    ContinuousMap.HomotopyWith.apply_one, ne_eq, Path.coe_toContinuousMap, toLoop_apply_coe,
    ContinuousMap.curry_apply, ContinuousMap.comp_apply]
  first
  | apply congr_arg p
  | apply congr_arg q
  apply (Cube.splitAt i).left_inv

Result:
no goals

Proof state:
case refine_2
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : Path.Homotopy (toLoop i p) (toLoop i q)
⊢ ∀ (x_1 : N → ↑I), (homotopyFrom i H).toFun (1, x_1) = ↑q x_1

Tactic:
intro

Result:
case refine_2
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : Path.Homotopy (toLoop i p) (toLoop i q)
x✝ : N → ↑I
⊢ (homotopyFrom i H).toFun (1, x✝) = ↑q x✝

Proof state:
case refine_2
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : Path.Homotopy (toLoop i p) (toLoop i q)
x✝ : N → ↑I
⊢ (homotopyFrom i H).toFun (1, x✝) = ↑q x✝

Tactic:
apply (homotopyFrom_apply _ _ _).trans

Result:
case refine_2
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : Path.Homotopy (toLoop i p) (toLoop i q)
x✝ : N → ↑I
⊢ Function.uncurry (fun x_1 y => Function.uncurry (fun x_2 y => ↑(H (x_1, x_2)) y) y)
      (Prod.map id ⇑(Cube.splitAt i) (1, x✝)) =
    ↑q x✝