Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i j : N
h : i ≠ j
a b c d : ↑(Ω^ N X x)
y✝ : N → ↑I
⊢ (copy
        (fromLoop i
          (Path.trans
            (toLoop i
              (copy (fromLoop j (Path.trans (toLoop j a) (toLoop j b)))
                (fun t ↦
                  if ↑(t j) ≤ 1 / 2 then a (Function.update t j (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(t j))))
                  else b (Function.update t j (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(t j) - 1))))
                ⋯))
            (toLoop i
              (copy (fromLoop j (Path.trans (toLoop j c) (toLoop j d)))
                (fun t ↦
                  if ↑(t j) ≤ 1 / 2 then c (Function.update t j (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(t j))))
                  else d (Function.update t j (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(t j) - 1))))
                ⋯))))
        (fun t ↦
          if ↑(t i) ≤ 1 / 2 then
            (copy (fromLoop j (Path.trans (toLoop j a) (toLoop j b)))
                (fun t ↦
                  if ↑(t j) ≤ 1 / 2 then a (Function.update t j (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(t j))))
                  else b (Function.update t j (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(t j) - 1))))
                ⋯)
              (Function.update t i (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(t i))))
          else
            (copy (fromLoop j (Path.trans (toLoop j c) (toLoop j d)))
                (fun t ↦
                  if ↑(t j) ≤ 1 / 2 then c (Function.update t j (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(t j))))
                  else d (Function.update t j (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(t j) - 1))))
                ⋯)
              (Function.update t i (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(t i) - 1))))
        ⋯)
      y✝ =
    (copy
        (fromLoop j
          (Path.trans
            (toLoop j
              (copy (fromLoop i (Path.trans (toLoop i a) (toLoop i c)))
                (fun t ↦
                  if ↑(t i) ≤ 1 / 2 then a (Function.update t i (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(t i))))
                  else c (Function.update t i (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(t i) - 1))))
                ⋯))
            (toLoop j
              (copy (fromLoop i (Path.trans (toLoop i b) (toLoop i d)))
                (fun t ↦
                  if ↑(t i) ≤ 1 / 2 then b (Function.update t i (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(t i))))
                  else d (Function.update t i (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(t i) - 1))))
                ⋯))))
        (fun t ↦
          if ↑(t j) ≤ 1 / 2 then
            (copy (fromLoop i (Path.trans (toLoop i a) (toLoop i c)))
                (fun t ↦
                  if ↑(t i) ≤ 1 / 2 then a (Function.update t i (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(t i))))
                  else c (Function.update t i (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(t i) - 1))))
                ⋯)
              (Function.update t j (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(t j))))
          else
            (copy (fromLoop i (Path.trans (toLoop i b) (toLoop i d)))
                (fun t ↦
                  if ↑(t i) ≤ 1 / 2 then b (Function.update t i (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(t i))))
                  else d (Function.update t i (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(t i) - 1))))
                ⋯)
              (Function.update t j (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(t j) - 1))))
        ⋯)
      y✝

Tactic:
coe_copy,

Goal state after:
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i j : N
h : i ≠ j
a b c d : ↑(Ω^ N X x)
y✝ : N → ↑I
⊢ (if ↑(y✝ i) ≤ 1 / 2 then
      if ↑(Function.update y✝ i (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ i))) j) ≤ 1 / 2 then
        a
          (Function.update (Function.update y✝ i (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ i)))) j
            (Set.projIcc 0 1 transAt._proof_3
              (2 * ↑(Function.update y✝ i (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ i))) j))))
      else
        b
          (Function.update (Function.update y✝ i (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ i)))) j
            (Set.projIcc 0 1 transAt._proof_3
              (2 * ↑(Function.update y✝ i (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ i))) j) - 1)))
    else
      if ↑(Function.update y✝ i (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ i) - 1)) j) ≤ 1 / 2 then
        c
          (Function.update (Function.update y✝ i (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ i) - 1))) j
            (Set.projIcc 0 1 transAt._proof_3
              (2 * ↑(Function.update y✝ i (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ i) - 1)) j))))
      else
        d
          (Function.update (Function.update y✝ i (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ i) - 1))) j
            (Set.projIcc 0 1 transAt._proof_3
              (2 * ↑(Function.update y✝ i (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ i) - 1)) j) - 1)))) =
    if ↑(y✝ j) ≤ 1 / 2 then
      if ↑(Function.update y✝ j (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ j))) i) ≤ 1 / 2 then
        a
          (Function.update (Function.update y✝ j (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ j)))) i
            (Set.projIcc 0 1 transAt._proof_3
              (2 * ↑(Function.update y✝ j (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ j))) i))))
      else
        c
          (Function.update (Function.update y✝ j (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ j)))) i
            (Set.projIcc 0 1 transAt._proof_3
              (2 * ↑(Function.update y✝ j (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ j))) i) - 1)))
    else
      if ↑(Function.update y✝ j (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ j) - 1)) i) ≤ 1 / 2 then
        b
          (Function.update (Function.update y✝ j (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ j) - 1))) i
            (Set.projIcc 0 1 transAt._proof_3
              (2 * ↑(Function.update y✝ j (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ j) - 1)) i))))
      else
        d
          (Function.update (Function.update y✝ j (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ j) - 1))) i
            (Set.projIcc 0 1 transAt._proof_3
              (2 * ↑(Function.update y✝ j (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ j) - 1)) i) - 1)))