-- 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_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))
neg :
  Eq (α := (↑(Ω^ N X x) : Type (max u_2 u_1)))
    ((Equiv.symm (toEquiv (loopHomeo i)) :
          (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 i) :
              (a : (↑(Ω^ N X x) : Type (max u_2 u_1))) → Path { as := const }.as { as := const }.as)
            ((Equiv.symm (toEquiv (loopHomeo j)) :
                (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 j) :
                    (a : (↑(Ω^ N X x) : Type (max u_2 u_1))) → Path { as := const }.as { as := const }.as)
                  d)
                ((toEquiv (loopHomeo j) :
                    (a : (↑(Ω^ N X x) : Type (max u_2 u_1))) → Path { as := const }.as { as := const }.as)
                  c))))
          ((toEquiv (loopHomeo i) :
              (a : (↑(Ω^ N X x) : Type (max u_2 u_1))) → Path { as := const }.as { as := const }.as)
            ((Equiv.symm (toEquiv (loopHomeo j)) :
                (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 j) :
                    (a : (↑(Ω^ N X x) : Type (max u_2 u_1))) → Path { as := const }.as { as := const }.as)
                  b)
                ((toEquiv (loopHomeo j) :
                    (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 j)) :
          (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 j) :
              (a : (↑(Ω^ N X x) : Type (max u_2 u_1))) → Path { as := const }.as { as := const }.as)
            ((Equiv.symm (toEquiv (loopHomeo i)) :
                (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 i) :
                    (a : (↑(Ω^ N X x) : Type (max u_2 u_1))) → Path { as := const }.as { as := const }.as)
                  d)
                ((toEquiv (loopHomeo i) :
                    (a : (↑(Ω^ N X x) : Type (max u_2 u_1))) → Path { as := const }.as { as := const }.as)
                  b))))
          ((toEquiv (loopHomeo j) :
              (a : (↑(Ω^ N X x) : Type (max u_2 u_1))) → Path { as := const }.as { as := const }.as)
            ((Equiv.symm (toEquiv (loopHomeo i)) :
                (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 i) :
                    (a : (↑(Ω^ N X x) : Type (max u_2 u_1))) → Path { as := const }.as { as := const }.as)
                  c)
                ((toEquiv (loopHomeo i) :
                    (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)))
⊢ Quotient.mk'
      ((Equiv.symm (toEquiv (loopHomeo i)) :
          (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 i) :
              (a : (↑(Ω^ N X x) : Type (max u_2 u_1))) → Path { as := const }.as { as := const }.as)
            ((Equiv.symm (toEquiv (loopHomeo j)) :
                (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 j) :
                    (a : (↑(Ω^ N X x) : Type (max u_2 u_1))) → Path { as := const }.as { as := const }.as)
                  d)
                ((toEquiv (loopHomeo j) :
                    (a : (↑(Ω^ N X x) : Type (max u_2 u_1))) → Path { as := const }.as { as := const }.as)
                  c))))
          ((toEquiv (loopHomeo i) :
              (a : (↑(Ω^ N X x) : Type (max u_2 u_1))) → Path { as := const }.as { as := const }.as)
            ((Equiv.symm (toEquiv (loopHomeo j)) :
                (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 j) :
                    (a : (↑(Ω^ N X x) : Type (max u_2 u_1))) → Path { as := const }.as { as := const }.as)
                  b)
                ((toEquiv (loopHomeo j) :
                    (a : (↑(Ω^ N X x) : Type (max u_2 u_1))) → Path { as := const }.as { as := const }.as)
                  a)))))) =
    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)
          c) *
      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) 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)

Tactic:
apply congr_arg Quotient.mk'

Premises used: congr_arg, Quotient.mk'