-- 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
inst_2 : Nontrivial N
h : ∃ (y : N), y ≠ Classical.arbitrary N := ⋯
a_1 : HomotopyGroup N X x
a : (↑(Ω^ N X x) : Type (max u_2 u_1))
b_1 : HomotopyGroup N X x
b : (↑(Ω^ N X x) : Type (max u_2 u_1))
c_1 : HomotopyGroup N X x
c : (↑(Ω^ N X x) : Type (max u_2 u_1))
d_1 : HomotopyGroup N X x
d : (↑(Ω^ N X x) : Type (max u_2 u_1))
⊢ Mul.mul
      (HMul.hMul (α := HomotopyGroup N X x)
        (Quot.mk
          (⇑(Homotopic.setoid N x) : (↑(Ω^ N X x) : Type (max u_2 u_1)) → (↑(Ω^ N X x) : Type (max u_2 u_1)) → Prop) a)
        (Quot.mk
          (⇑(Homotopic.setoid N x) : (↑(Ω^ N X x) : Type (max u_2 u_1)) → (↑(Ω^ N X x) : Type (max u_2 u_1)) → Prop) b))
      (HMul.hMul (α := HomotopyGroup N X x)
        (Quot.mk
          (⇑(Homotopic.setoid N x) : (↑(Ω^ N X x) : Type (max u_2 u_1)) → (↑(Ω^ N X x) : Type (max u_2 u_1)) → Prop) c)
        (Quot.mk
          (⇑(Homotopic.setoid N x) : (↑(Ω^ N X x) : Type (max u_2 u_1)) → (↑(Ω^ N X x) : Type (max u_2 u_1)) → Prop)
          d)) =
    HMul.hMul (α := HomotopyGroup N X x)
      (Mul.mul
        (Quot.mk
          (⇑(Homotopic.setoid N x) : (↑(Ω^ N X x) : Type (max u_2 u_1)) → (↑(Ω^ N X x) : Type (max u_2 u_1)) → Prop) a)
        (Quot.mk
          (⇑(Homotopic.setoid N x) : (↑(Ω^ N X x) : Type (max u_2 u_1)) → (↑(Ω^ N X x) : Type (max u_2 u_1)) → Prop) c))
      (Mul.mul
        (Quot.mk
          (⇑(Homotopic.setoid N x) : (↑(Ω^ N X x) : Type (max u_2 u_1)) → (↑(Ω^ N X x) : Type (max u_2 u_1)) → Prop) b)
        (Quot.mk
          (⇑(Homotopic.setoid N x) : (↑(Ω^ N X x) : Type (max u_2 u_1)) → (↑(Ω^ N X x) : Type (max u_2 u_1)) → Prop) d))
have mk : Eq (α := (↑(Ω^ N X x) : Type (max u_2 u_1)))
  ((Equiv.symm (toEquiv (loopHomeo (Classical.choose (p := fun (x : N) ↦ x ≠ Classical.arbitrary N) h))) :
        (a : Path { as := const }.as { as := const }.as) → (↑(Ω^ N X x) : Type (max u_2 u_1)))
      (Path.trans (y := FundamentalGroupoid.as { as := const })
        ((toEquiv (loopHomeo (Classical.choose (p := fun (x : N) ↦ x ≠ Classical.arbitrary N) h)) :
            (a : (↑(Ω^ N X x) : Type (max u_2 u_1))) → Path { as := const }.as { as := const }.as)
          ((Equiv.symm (toEquiv (loopHomeo (Classical.arbitrary N))) :
              (a : Path { as := const }.as { as := const }.as) → (↑(Ω^ N X x) : Type (max u_2 u_1)))
            (Path.trans (y := FundamentalGroupoid.as { as := const })
              ((toEquiv (loopHomeo (Classical.arbitrary N)) :
                  (a : (↑(Ω^ N X x) : Type (max u_2 u_1))) → Path { as := const }.as { as := const }.as)
                d)
              ((toEquiv (loopHomeo (Classical.arbitrary N)) :
                  (a : (↑(Ω^ N X x) : Type (max u_2 u_1))) → Path { as := const }.as { as := const }.as)
                c))))
        ((toEquiv (loopHomeo (Classical.choose (p := fun (x : N) ↦ x ≠ Classical.arbitrary N) h)) :
            (a : (↑(Ω^ N X x) : Type (max u_2 u_1))) → Path { as := const }.as { as := const }.as)
          ((Equiv.symm (toEquiv (loopHomeo (Classical.arbitrary N))) :
              (a : Path { as := const }.as { as := const }.as) → (↑(Ω^ N X x) : Type (max u_2 u_1)))
            (Path.trans (y := FundamentalGroupoid.as { as := const })
              ((toEquiv (loopHomeo (Classical.arbitrary N)) :
                  (a : (↑(Ω^ N X x) : Type (max u_2 u_1))) → Path { as := const }.as { as := const }.as)
                b)
              ((toEquiv (loopHomeo (Classical.arbitrary N)) :
                  (a : (↑(Ω^ N X x) : Type (max u_2 u_1))) → Path { as := const }.as { as := const }.as)
                a))))) :
    (↑(Ω^ N X x) : Type (max u_2 u_1)))
  ((Equiv.symm (toEquiv (loopHomeo (Classical.arbitrary N))) :
        (a : Path { as := const }.as { as := const }.as) → (↑(Ω^ N X x) : Type (max u_2 u_1)))
      (Path.trans (y := FundamentalGroupoid.as { as := const })
        ((toEquiv (loopHomeo (Classical.arbitrary N)) :
            (a : (↑(Ω^ N X x) : Type (max u_2 u_1))) → Path { as := const }.as { as := const }.as)
          ((Equiv.symm (toEquiv (loopHomeo (Classical.choose (p := fun (x : N) ↦ x ≠ Classical.arbitrary N) h))) :
              (a : Path { as := const }.as { as := const }.as) → (↑(Ω^ N X x) : Type (max u_2 u_1)))
            (Path.trans (y := FundamentalGroupoid.as { as := const })
              ((toEquiv (loopHomeo (Classical.choose (p := fun (x : N) ↦ x ≠ Classical.arbitrary N) h)) :
                  (a : (↑(Ω^ N X x) : Type (max u_2 u_1))) → Path { as := const }.as { as := const }.as)
                d)
              ((toEquiv (loopHomeo (Classical.choose (p := fun (x : N) ↦ x ≠ Classical.arbitrary N) h)) :
                  (a : (↑(Ω^ N X x) : Type (max u_2 u_1))) → Path { as := const }.as { as := const }.as)
                b))))
        ((toEquiv (loopHomeo (Classical.arbitrary N)) :
            (a : (↑(Ω^ N X x) : Type (max u_2 u_1))) → Path { as := const }.as { as := const }.as)
          ((Equiv.symm (toEquiv (loopHomeo (Classical.choose (p := fun (x : N) ↦ x ≠ Classical.arbitrary N) h))) :
              (a : Path { as := const }.as { as := const }.as) → (↑(Ω^ N X x) : Type (max u_2 u_1)))
            (Path.trans (y := FundamentalGroupoid.as { as := const })
              ((toEquiv (loopHomeo (Classical.choose (p := fun (x : N) ↦ x ≠ Classical.arbitrary N) h)) :
                  (a : (↑(Ω^ N X x) : Type (max u_2 u_1))) → Path { as := const }.as { as := const }.as)
                c)
              ((toEquiv (loopHomeo (Classical.choose (p := fun (x : N) ↦ x ≠ Classical.arbitrary N) h)) :
                  (a : (↑(Ω^ N X x) : Type (max u_2 u_1))) → Path { as := const }.as { as := const }.as)
                a))))) :
    (↑(Ω^ N X x) : Type (max u_2 u_1)))
Tactic: apply congr_arg Quotient.mk'