-- Mathlib/Topology/Homotopy/HomotopyGroup.lean
theorem transAt_distrib {i j : N} (h : i ≠ j) (a b c d : Ω^ N X x) :
    transAt i (transAt j a b) (transAt j c d) = transAt j (transAt i a c) (transAt i b d)

Proof state:
case H
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 : ↑(Ω^ N X x)
y✝ : N → ↑I
⊢ (transAt i (transAt j a b) (transAt j c d)) y✝ = (transAt j (transAt i a c) (transAt i b d)) y✝

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

Result:
case H
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 : ↑(Ω^ N X x)
y✝ : N → ↑I
⊢ (if ↑(y✝ i) ≤ 1 / 2 then
      if ↑(y✝ j) ≤ 1 / 2 then
        a
          (Function.update (Function.update y✝ i (Set.projIcc 0 1 transAt.proof_2 (2 * ↑(y✝ i)))) j
            (Set.projIcc 0 1 transAt.proof_2 (2 * ↑(y✝ j))))
      else
        b
          (Function.update (Function.update y✝ i (Set.projIcc 0 1 transAt.proof_2 (2 * ↑(y✝ i)))) j
            (Set.projIcc 0 1 transAt.proof_2 (2 * ↑(y✝ j) - 1)))
    else
      if ↑(y✝ j) ≤ 1 / 2 then
        c
          (Function.update (Function.update y✝ i (Set.projIcc 0 1 transAt.proof_2 (2 * ↑(y✝ i) - 1))) j
            (Set.projIcc 0 1 transAt.proof_2 (2 * ↑(y✝ j))))
      else
        d
          (Function.update (Function.update y✝ i (Set.projIcc 0 1 transAt.proof_2 (2 * ↑(y✝ i) - 1))) j
            (Set.projIcc 0 1 transAt.proof_2 (2 * ↑(y✝ j) - 1)))) =
    if ↑(y✝ j) ≤ 1 / 2 then
      if ↑(y✝ i) ≤ 1 / 2 then
        a
          (Function.update (Function.update y✝ j (Set.projIcc 0 1 transAt.proof_2 (2 * ↑(y✝ j)))) i
            (Set.projIcc 0 1 transAt.proof_2 (2 * ↑(y✝ i))))
      else
        c
          (Function.update (Function.update y✝ j (Set.projIcc 0 1 transAt.proof_2 (2 * ↑(y✝ j)))) i
            (Set.projIcc 0 1 transAt.proof_2 (2 * ↑(y✝ i) - 1)))
    else
      if ↑(y✝ i) ≤ 1 / 2 then
        b
          (Function.update (Function.update y✝ j (Set.projIcc 0 1 transAt.proof_2 (2 * ↑(y✝ j) - 1))) i
            (Set.projIcc 0 1 transAt.proof_2 (2 * ↑(y✝ i))))
      else
        d
          (Function.update (Function.update y✝ j (Set.projIcc 0 1 transAt.proof_2 (2 * ↑(y✝ j) - 1))) i
            (Set.projIcc 0 1 transAt.proof_2 (2 * ↑(y✝ i) - 1)))

Proof state:
case neg.h.e_6.h.h.h
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 : ↑(Ω^ N X x)
y✝ : N → ↑I
h✝¹ : ¬↑(y✝ i) ≤ 1 / 2
h✝ : ¬↑(y✝ j) ≤ 1 / 2
x✝ : N
⊢ x✝ = j → ¬x✝ = i

Tactic:
rintro rfl

Result:
case neg.h.e_6.h.h.h
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
a b c d : ↑(Ω^ N X x)
y✝ : N → ↑I
h✝¹ : ¬↑(y✝ i) ≤ 1 / 2
x✝ : N
h : i ≠ x✝
h✝ : ¬↑(y✝ x✝) ≤ 1 / 2
⊢ ¬x✝ = i

Proof state:
case neg.h.e_6.h.h
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 : ↑(Ω^ N X x)
y✝ : N → ↑I
h✝¹ : ¬↑(y✝ i) ≤ 1 / 2
h✝ : ¬↑(y✝ j) ≤ 1 / 2
x✝ : N
⊢ Function.update (Function.update y✝ i (Set.projIcc 0 1 transAt.proof_2 (2 * ↑(y✝ i) - 1))) j
      (Set.projIcc 0 1 transAt.proof_2 (2 * ↑(y✝ j) - 1)) x✝ =
    Function.update (Function.update y✝ j (Set.projIcc 0 1 transAt.proof_2 (2 * ↑(y✝ j) - 1))) i
      (Set.projIcc 0 1 transAt.proof_2 (2 * ↑(y✝ i) - 1)) x✝

Tactic:
simp only [Function.update, eq_rec_constant, dite_eq_ite]

Result:
case neg.h.e_6.h.h
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 : ↑(Ω^ N X x)
y✝ : N → ↑I
h✝¹ : ¬↑(y✝ i) ≤ 1 / 2
h✝ : ¬↑(y✝ j) ≤ 1 / 2
x✝ : N
⊢ (if x✝ = j then Set.projIcc 0 1 transAt.proof_2 (2 * ↑(y✝ j) - 1)
    else if x✝ = i then Set.projIcc 0 1 transAt.proof_2 (2 * ↑(y✝ i) - 1) else y✝ x✝) =
    if x✝ = i then Set.projIcc 0 1 transAt.proof_2 (2 * ↑(y✝ i) - 1)
    else if x✝ = j then Set.projIcc 0 1 transAt.proof_2 (2 * ↑(y✝ j) - 1) else y✝ x✝

Proof state:
case neg.h.e_6.h.h
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 : ↑(Ω^ N X x)
y✝ : N → ↑I
h✝¹ : ¬↑(y✝ i) ≤ 1 / 2
h✝ : ¬↑(y✝ j) ≤ 1 / 2
x✝ : N
⊢ (if x✝ = j then Set.projIcc 0 1 transAt.proof_2 (2 * ↑(y✝ j) - 1)
    else if x✝ = i then Set.projIcc 0 1 transAt.proof_2 (2 * ↑(y✝ i) - 1) else y✝ x✝) =
    if x✝ = i then Set.projIcc 0 1 transAt.proof_2 (2 * ↑(y✝ i) - 1)
    else if x✝ = j then Set.projIcc 0 1 transAt.proof_2 (2 * ↑(y✝ j) - 1) else y✝ x✝

Tactic:
apply ite_ite_comm

Result:
case neg.h.e_6.h.h.h
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 : ↑(Ω^ N X x)
y✝ : N → ↑I
h✝¹ : ¬↑(y✝ i) ≤ 1 / 2
h✝ : ¬↑(y✝ j) ≤ 1 / 2
x✝ : N
⊢ x✝ = j → ¬x✝ = i

Proof state:
case neg.h.e_6.h
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 : ↑(Ω^ N X x)
y✝ : N → ↑I
h✝¹ : ¬↑(y✝ i) ≤ 1 / 2
h✝ : ¬↑(y✝ j) ≤ 1 / 2
⊢ Function.update (Function.update y✝ i (Set.projIcc 0 1 transAt.proof_2 (2 * ↑(y✝ i) - 1))) j
      (Set.projIcc 0 1 transAt.proof_2 (2 * ↑(y✝ j) - 1)) =
    Function.update (Function.update y✝ j (Set.projIcc 0 1 transAt.proof_2 (2 * ↑(y✝ j) - 1))) i
      (Set.projIcc 0 1 transAt.proof_2 (2 * ↑(y✝ i) - 1))

Tactic:
ext1

Result:
case neg.h.e_6.h.h
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 : ↑(Ω^ N X x)
y✝ : N → ↑I
h✝¹ : ¬↑(y✝ i) ≤ 1 / 2
h✝ : ¬↑(y✝ j) ≤ 1 / 2
x✝ : N
⊢ Function.update (Function.update y✝ i (Set.projIcc 0 1 transAt.proof_2 (2 * ↑(y✝ i) - 1))) j
      (Set.projIcc 0 1 transAt.proof_2 (2 * ↑(y✝ j) - 1)) x✝ =
    Function.update (Function.update y✝ j (Set.projIcc 0 1 transAt.proof_2 (2 * ↑(y✝ j) - 1))) i
      (Set.projIcc 0 1 transAt.proof_2 (2 * ↑(y✝ i) - 1)) x✝

Proof state:
case neg.h.e_6.h.h.h
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
a b c d : ↑(Ω^ N X x)
y✝ : N → ↑I
h✝¹ : ¬↑(y✝ i) ≤ 1 / 2
x✝ : N
h : i ≠ x✝
h✝ : ¬↑(y✝ x✝) ≤ 1 / 2
⊢ ¬x✝ = i

Tactic:
exact h.symm

Result:
no goals

Proof state:
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 : ↑(Ω^ N X x)
⊢ transAt i (transAt j a b) (transAt j c d) = transAt j (transAt i a c) (transAt i b d)

Tactic:
ext

Result:
case H
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 : ↑(Ω^ N X x)
y✝ : N → ↑I
⊢ (transAt i (transAt j a b) (transAt j c d)) y✝ = (transAt j (transAt i a c) (transAt i b d)) y✝

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 : ↑(Ω^ N X x)
y✝ : N → ↑I
h✝¹ : ¬↑(y✝ i) ≤ 1 / 2
h✝ : ¬↑(y✝ j) ≤ 1 / 2
⊢ d
      (Function.update (Function.update y✝ i (Set.projIcc 0 1 transAt.proof_2 (2 * ↑(y✝ i) - 1))) j
        (Set.projIcc 0 1 transAt.proof_2 (2 * ↑(y✝ j) - 1))) =
    d
      (Function.update (Function.update y✝ j (Set.projIcc 0 1 transAt.proof_2 (2 * ↑(y✝ j) - 1))) i
        (Set.projIcc 0 1 transAt.proof_2 (2 * ↑(y✝ i) - 1)))

Tactic:
congr 1

Result:
case neg.h.e_6.h
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 : ↑(Ω^ N X x)
y✝ : N → ↑I
h✝¹ : ¬↑(y✝ i) ≤ 1 / 2
h✝ : ¬↑(y✝ j) ≤ 1 / 2
⊢ Function.update (Function.update y✝ i (Set.projIcc 0 1 transAt.proof_2 (2 * ↑(y✝ i) - 1))) j
      (Set.projIcc 0 1 transAt.proof_2 (2 * ↑(y✝ j) - 1)) =
    Function.update (Function.update y✝ j (Set.projIcc 0 1 transAt.proof_2 (2 * ↑(y✝ j) - 1))) i
      (Set.projIcc 0 1 transAt.proof_2 (2 * ↑(y✝ i) - 1))