-- 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)
pos :
  (↑(y i) : ℝ) ≤ 1 / 2 →
    (↑(y j) : ℝ) ≤ 1 / 2 →
      Eq.{u_2 + 1} (α := X)
        ((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) : ℝ)))) :
          X)
        ((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) : ℝ)))) :
          X)
neg :
  (↑(y i) : ℝ) ≤ 1 / 2 →
    ¬(↑(y j) : ℝ) ≤ 1 / 2 →
      Eq.{u_2 + 1} (α := X)
        ((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))) :
          X)
        ((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) : ℝ)))) :
          X)
pos₁ :
  ¬(↑(y i) : ℝ) ≤ 1 / 2 →
    (↑(y j) : ℝ) ≤ 1 / 2 →
      Eq.{u_2 + 1} (α := X)
        ((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) : ℝ)))) :
          X)
        ((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))) :
          X)
⊢ 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)
have neg₁ : ¬(↑(y i) : ℝ) ≤ 1 / 2 →
  ¬(↑(y j) : ℝ) ≤ 1 / 2 →
    Eq.{u_2 + 1} (α := X)
      ((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)
      ((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: split_ifs