-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
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)
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)
⊢ 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)

Tactic:
simp_rw [transAt, coe_copy, Function.update_apply, if_neg h, if_neg h.symm]

Premises used: Function.update_apply, Ne.symm, GenLoop.transAt, GenLoop.coe_copy, if_neg