-- Mathlib/Topology/Homotopy/HomotopyGroup.lean
theorem auxGroup_indep (i j : N) : (auxGroup i : Group (HomotopyGroup N X x)) = auxGroup j

Proof state:
case neg.mk.mk.mk.mk
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i j : N
h : ¬i = j
a✝ : HomotopyGroup N X x
a : ↑(Ω^ N X x)
b✝ : HomotopyGroup N X x
b : ↑(Ω^ N X x)
c✝ : HomotopyGroup N X x
c : ↑(Ω^ N X x)
d✝ : HomotopyGroup N X x
d : ↑(Ω^ N X x)
⊢ Quotient.mk'
      ((loopHomeo i).symm
        (Path.trans
          ((loopHomeo i).toEquiv ((loopHomeo j).symm (Path.trans ((loopHomeo j).toEquiv d) ((loopHomeo j).toEquiv c))))
          ((loopHomeo i).toEquiv
            ((loopHomeo j).symm (Path.trans ((loopHomeo j).toEquiv b) ((loopHomeo j).toEquiv a)))))) =
    Mul.mul (Mul.mul (Quot.mk (⇑(Homotopic.setoid N x)) a) (Quot.mk (⇑(Homotopic.setoid N x)) c))
      (Mul.mul (Quot.mk (⇑(Homotopic.setoid N x)) b) (Quot.mk (⇑(Homotopic.setoid N x)) d))

Tactic:
apply congr_arg Quotient.mk'

Result:
case neg.mk.mk.mk.mk
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i j : N
h : ¬i = j
a✝ : HomotopyGroup N X x
a : ↑(Ω^ N X x)
b✝ : HomotopyGroup N X x
b : ↑(Ω^ N X x)
c✝ : HomotopyGroup N X x
c : ↑(Ω^ N X x)
d✝ : HomotopyGroup N X x
d : ↑(Ω^ N X x)
⊢ (loopHomeo i).symm
      (Path.trans
        ((loopHomeo i).toEquiv ((loopHomeo j).symm (Path.trans ((loopHomeo j).toEquiv d) ((loopHomeo j).toEquiv c))))
        ((loopHomeo i).toEquiv ((loopHomeo j).symm (Path.trans ((loopHomeo j).toEquiv b) ((loopHomeo j).toEquiv a))))) =
    (loopHomeo j).symm
      (Path.trans
        ((loopHomeo j).toEquiv ((loopHomeo i).symm (Path.trans ((loopHomeo i).toEquiv d) ((loopHomeo i).toEquiv b))))
        ((loopHomeo j).toEquiv ((loopHomeo i).symm (Path.trans ((loopHomeo i).toEquiv c) ((loopHomeo i).toEquiv a)))))

Proof state:
case neg.mk.mk.mk.mk
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i j : N
h : ¬i = j
a✝ : HomotopyGroup N X x
a : ↑(Ω^ N X x)
b✝ : HomotopyGroup N X x
b : ↑(Ω^ N X x)
c✝ : HomotopyGroup N X x
c : ↑(Ω^ N X x)
d✝ : HomotopyGroup N X x
d : ↑(Ω^ N X x)
⊢ Mul.mul (Mul.mul (Quot.mk (⇑(Homotopic.setoid N x)) a) (Quot.mk (⇑(Homotopic.setoid N x)) b))
      (Mul.mul (Quot.mk (⇑(Homotopic.setoid N x)) c) (Quot.mk (⇑(Homotopic.setoid N x)) d)) =
    Mul.mul (Mul.mul (Quot.mk (⇑(Homotopic.setoid N x)) a) (Quot.mk (⇑(Homotopic.setoid N x)) c))
      (Mul.mul (Quot.mk (⇑(Homotopic.setoid N x)) b) (Quot.mk (⇑(Homotopic.setoid N x)) d))

Tactic:
change Quotient.mk' _ = _

Result:
case neg.mk.mk.mk.mk
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i j : N
h : ¬i = j
a✝ : HomotopyGroup N X x
a : ↑(Ω^ N X x)
b✝ : HomotopyGroup N X x
b : ↑(Ω^ N X x)
c✝ : HomotopyGroup N X x
c : ↑(Ω^ N X x)
d✝ : HomotopyGroup N X x
d : ↑(Ω^ N X x)
⊢ Quotient.mk'
      ((loopHomeo i).symm
        (Path.trans
          ((loopHomeo i).toEquiv ((loopHomeo j).symm (Path.trans ((loopHomeo j).toEquiv d) ((loopHomeo j).toEquiv c))))
          ((loopHomeo i).toEquiv
            ((loopHomeo j).symm (Path.trans ((loopHomeo j).toEquiv b) ((loopHomeo j).toEquiv a)))))) =
    Mul.mul (Mul.mul (Quot.mk (⇑(Homotopic.setoid N x)) a) (Quot.mk (⇑(Homotopic.setoid N x)) c))
      (Mul.mul (Quot.mk (⇑(Homotopic.setoid N x)) b) (Quot.mk (⇑(Homotopic.setoid N x)) d))

Proof state:
case neg.mk.mk.mk.mk
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i j : N
h : ¬i = j
a✝ : HomotopyGroup N X x
a : ↑(Ω^ N X x)
b✝ : HomotopyGroup N X x
b : ↑(Ω^ N X x)
c✝ : HomotopyGroup N X x
c : ↑(Ω^ N X x)
d✝ : HomotopyGroup N X x
d : ↑(Ω^ N X x)
⊢ (loopHomeo i).symm
      (Path.trans
        ((loopHomeo i).toEquiv ((loopHomeo j).symm (Path.trans ((loopHomeo j).toEquiv d) ((loopHomeo j).toEquiv c))))
        ((loopHomeo i).toEquiv ((loopHomeo j).symm (Path.trans ((loopHomeo j).toEquiv b) ((loopHomeo j).toEquiv a))))) =
    (loopHomeo j).symm
      (Path.trans
        ((loopHomeo j).toEquiv ((loopHomeo i).symm (Path.trans ((loopHomeo i).toEquiv d) ((loopHomeo i).toEquiv b))))
        ((loopHomeo j).toEquiv ((loopHomeo i).symm (Path.trans ((loopHomeo i).toEquiv c) ((loopHomeo i).toEquiv a)))))

Tactic:
simp only [fromLoop_trans_toLoop, transAt_distrib h, coe_toEquiv, loopHomeo_apply,
  coe_symm_toEquiv, loopHomeo_symm_apply]

Result:
no goals

Proof state:
case pos
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i j : N
h : i = j
⊢ auxGroup i = auxGroup j

Tactic:
rw [h]

Result:
no goals

Proof state:
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i j : N
⊢ auxGroup i = auxGroup j

Tactic:
by_cases h : i = j

Result:
case pos
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i j : N
h : i = j
⊢ auxGroup i = auxGroup j

case neg
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i j : N
h : ¬i = j
⊢ auxGroup i = auxGroup j

Proof state:
case neg
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i j : N
h : ¬i = j
⊢ ∀ (a b c d : HomotopyGroup N X x), Mul.mul (Mul.mul a b) (Mul.mul c d) = Mul.mul (Mul.mul a c) (Mul.mul b d)

Tactic:
rintro ⟨a⟩ ⟨b⟩ ⟨c⟩ ⟨d⟩

Result:
case neg.mk.mk.mk.mk
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i j : N
h : ¬i = j
a✝ : HomotopyGroup N X x
a : ↑(Ω^ N X x)
b✝ : HomotopyGroup N X x
b : ↑(Ω^ N X x)
c✝ : HomotopyGroup N X x
c : ↑(Ω^ N X x)
d✝ : HomotopyGroup N X x
d : ↑(Ω^ N X x)
⊢ Mul.mul (Mul.mul (Quot.mk (⇑(Homotopic.setoid N x)) a) (Quot.mk (⇑(Homotopic.setoid N x)) b))
      (Mul.mul (Quot.mk (⇑(Homotopic.setoid N x)) c) (Quot.mk (⇑(Homotopic.setoid N x)) d)) =
    Mul.mul (Mul.mul (Quot.mk (⇑(Homotopic.setoid N x)) a) (Quot.mk (⇑(Homotopic.setoid N x)) c))
      (Mul.mul (Quot.mk (⇑(Homotopic.setoid N x)) b) (Quot.mk (⇑(Homotopic.setoid N x)) d))

Proof state:
case neg
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i j : N
h : ¬i = j
⊢ auxGroup i = auxGroup j

Tactic:
refine Group.ext (EckmannHilton.mul (isUnital_auxGroup i) (isUnital_auxGroup j) ?_)

Result:
case neg
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i j : N
h : ¬i = j
⊢ ∀ (a b c d : HomotopyGroup N X x), Mul.mul (Mul.mul a b) (Mul.mul c d) = Mul.mul (Mul.mul a c) (Mul.mul b d)