-- Lean 4 proof step from Mathlib.Topology.Homotopy.HomotopyGroup (goal)
Goal:
N : Type u_1
X : Type u_2
inst : TopologicalSpace X
x : X
inst_1 : DecidableEq N
i j : N
h : i ≠ j
a b c d : (↑(Ω^ N X x) : Type (max u_1 u_2))
y : N → (↑I : Type)
⊢ Eq.{u_2 + 1} (α := X) ((transAt i (transAt j a b) (transAt j c d) : (a : N → (↑I : Type)) → X) y : X)
    ((transAt j (transAt i a c) (transAt i b d) : (a : N → (↑I : Type)) → X) y : X)
have H : Eq.{u_2 + 1} (α := X)
  (if (↑(y i) : ℝ) ≤ 1 / 2 then
      if (↑(y j) : ℝ) ≤ 1 / 2 then
        (a : (a : N → (↑I : Type)) → X)
          (Function.update (β := fun (a : N) ↦ (↑I : Type))
            (Function.update (β := fun (a : N) ↦ (↑I : Type)) y i (Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y i) : ℝ))))
            j (Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y j) : ℝ))))
      else
        (b : (a : N → (↑I : Type)) → X)
          (Function.update (β := fun (a : N) ↦ (↑I : Type))
            (Function.update (β := fun (a : N) ↦ (↑I : Type)) y i (Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y i) : ℝ))))
            j (Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y j) : ℝ) - 1)))
    else
      if (↑(y j) : ℝ) ≤ 1 / 2 then
        (c : (a : N → (↑I : Type)) → X)
          (Function.update (β := fun (a : N) ↦ (↑I : Type))
            (Function.update (β := fun (a : N) ↦ (↑I : Type)) y i
              (Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y i) : ℝ) - 1)))
            j (Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y j) : ℝ))))
      else
        (d : (a : N → (↑I : Type)) → X)
          (Function.update (β := fun (a : N) ↦ (↑I : Type))
            (Function.update (β := fun (a : N) ↦ (↑I : Type)) y i
              (Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y i) : ℝ) - 1)))
            j (Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y j) : ℝ) - 1))) :
    X)
  (if (↑(y j) : ℝ) ≤ 1 / 2 then
      if (↑(y i) : ℝ) ≤ 1 / 2 then
        (a : (a : N → (↑I : Type)) → X)
          (Function.update (β := fun (a : N) ↦ (↑I : Type))
            (Function.update (β := fun (a : N) ↦ (↑I : Type)) y j (Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y j) : ℝ))))
            i (Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y i) : ℝ))))
      else
        (c : (a : N → (↑I : Type)) → X)
          (Function.update (β := fun (a : N) ↦ (↑I : Type))
            (Function.update (β := fun (a : N) ↦ (↑I : Type)) y j (Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y j) : ℝ))))
            i (Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y i) : ℝ) - 1)))
    else
      if (↑(y i) : ℝ) ≤ 1 / 2 then
        (b : (a : N → (↑I : Type)) → X)
          (Function.update (β := fun (a : N) ↦ (↑I : Type))
            (Function.update (β := fun (a : N) ↦ (↑I : Type)) y j
              (Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y j) : ℝ) - 1)))
            i (Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y i) : ℝ))))
      else
        (d : (a : N → (↑I : Type)) → X)
          (Function.update (β := fun (a : N) ↦ (↑I : Type))
            (Function.update (β := fun (a : N) ↦ (↑I : Type)) y j
              (Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y j) : ℝ) - 1)))
            i (Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y i) : ℝ) - 1))) :
    X)
Tactic: simp_rw [transAt, coe_copy, Function.update_apply, if_neg h, if_neg h.symm]