-- Mathlib/Logic/Function/Basic.lean
theorem update_comm {α} [DecidableEq α] {β : α → Sort*} {a b : α} (h : a ≠ b) (v : β a) (w : β b)
    (f : ∀ a, β a) : update (update f a v) b w = update (update f b w) a v

Proof state:
case h
α : Sort u_2
inst✝ : DecidableEq α
β : α → Sort u_1
a b : α
h : a ≠ b
v : β a
w : β b
f : (a : α) → β a
c : α
⊢ (if h : c = b then ⋯ ▸ w else if h : c = a then ⋯ ▸ v else f c) =
    if h : c = a then ⋯ ▸ v else if h : c = b then ⋯ ▸ w else f c

Tactic:
by_cases h₁ : c = b <;> by_cases h₂ : c = a

Result:
case pos
α : Sort u_2
inst✝ : DecidableEq α
β : α → Sort u_1
a b : α
h : a ≠ b
v : β a
w : β b
f : (a : α) → β a
c : α
h₁ : c = b
h₂ : c = a
⊢ (if h : c = b then ⋯ ▸ w else if h : c = a then ⋯ ▸ v else f c) =
    if h : c = a then ⋯ ▸ v else if h : c = b then ⋯ ▸ w else f c

case neg
α : Sort u_2
inst✝ : DecidableEq α
β : α → Sort u_1
a b : α
h : a ≠ b
v : β a
w : β b
f : (a : α) → β a
c : α
h₁ : c = b
h₂ : ¬c = a
⊢ (if h : c = b then ⋯ ▸ w else if h : c = a then ⋯ ▸ v else f c) =
    if h : c = a then ⋯ ▸ v else if h : c = b then ⋯ ▸ w else f c

case pos
α : Sort u_2
inst✝ : DecidableEq α
β : α → Sort u_1
a b : α
h : a ≠ b
v : β a
w : β b
f : (a : α) → β a
c : α
h₁ : ¬c = b
h₂ : c = a
⊢ (if h : c = b then ⋯ ▸ w else if h : c = a then ⋯ ▸ v else f c) =
    if h : c = a then ⋯ ▸ v else if h : c = b then ⋯ ▸ w else f c

case neg
α : Sort u_2
inst✝ : DecidableEq α
β : α → Sort u_1
a b : α
h : a ≠ b
v : β a
w : β b
f : (a : α) → β a
c : α
h₁ : ¬c = b
h₂ : ¬c = a
⊢ (if h : c = b then ⋯ ▸ w else if h : c = a then ⋯ ▸ v else f c) =
    if h : c = a then ⋯ ▸ v else if h : c = b then ⋯ ▸ w else f c

Proof state:
case neg
α : Sort u_2
inst✝ : DecidableEq α
β : α → Sort u_1
a b : α
h : a ≠ b
v : β a
w : β b
f : (a : α) → β a
c : α
h₁ : ¬c = b
h₂ : ¬c = a
⊢ (if h : c = b then ⋯ ▸ w else if h : c = a then ⋯ ▸ v else f c) =
    if h : c = a then ⋯ ▸ v else if h : c = b then ⋯ ▸ w else f c

Tactic:
rw [dif_neg h₁, dif_neg h₁]

Result:
no goals

Proof state:
case neg
α : Sort u_2
inst✝ : DecidableEq α
β : α → Sort u_1
a b : α
h : a ≠ b
v : β a
w : β b
f : (a : α) → β a
c : α
h₁ : c = b
h₂ : ¬c = a
⊢ (if h : c = b then ⋯ ▸ w else if h : c = a then ⋯ ▸ v else f c) =
    if h : c = a then ⋯ ▸ v else if h : c = b then ⋯ ▸ w else f c

Tactic:
rw [dif_pos h₁, dif_pos h₁, dif_neg h₂]

Result:
no goals

Proof state:
case pos
α : Sort u_2
inst✝ : DecidableEq α
β : α → Sort u_1
a b : α
h : a ≠ b
v : β a
w : β b
f : (a : α) → β a
c : α
h₁ : ¬c = b
h₂ : c = a
⊢ (if h : c = b then ⋯ ▸ w else if h : c = a then ⋯ ▸ v else f c) =
    if h : c = a then ⋯ ▸ v else if h : c = b then ⋯ ▸ w else f c

Tactic:
rw [dif_neg h₁, dif_neg h₁]

Result:
no goals

Proof state:
case h
α : Sort u_2
inst✝ : DecidableEq α
β : α → Sort u_1
a b : α
h : a ≠ b
v : β a
w : β b
f : (a : α) → β a
c : α
⊢ update (update f a v) b w c = update (update f b w) a v c

Tactic:
simp only [update]

Result:
case h
α : Sort u_2
inst✝ : DecidableEq α
β : α → Sort u_1
a b : α
h : a ≠ b
v : β a
w : β b
f : (a : α) → β a
c : α
⊢ (if h : c = b then ⋯ ▸ w else if h : c = a then ⋯ ▸ v else f c) =
    if h : c = a then ⋯ ▸ v else if h : c = b then ⋯ ▸ w else f c

Proof state:
case pos
α : Sort u_2
inst✝ : DecidableEq α
β : α → Sort u_1
a b : α
h : a ≠ b
v : β a
w : β b
f : (a : α) → β a
c : α
h₁ : c = b
h₂ : c = a
⊢ (if h : c = b then ⋯ ▸ w else if h : c = a then ⋯ ▸ v else f c) =
    if h : c = a then ⋯ ▸ v else if h : c = b then ⋯ ▸ w else f c

Tactic:
rw [dif_pos h₁, dif_pos h₂]

Result:
case pos
α : Sort u_2
inst✝ : DecidableEq α
β : α → Sort u_1
a b : α
h : a ≠ b
v : β a
w : β b
f : (a : α) → β a
c : α
h₁ : c = b
h₂ : c = a
⊢ ⋯ ▸ w = ⋯ ▸ v

Proof state:
α : Sort u_2
inst✝ : DecidableEq α
β : α → Sort u_1
a b : α
h : a ≠ b
v : β a
w : β b
f : (a : α) → β a
⊢ update (update f a v) b w = update (update f b w) a v

Tactic:
funext c

Result:
case h
α : Sort u_2
inst✝ : DecidableEq α
β : α → Sort u_1
a b : α
h : a ≠ b
v : β a
w : β b
f : (a : α) → β a
c : α
⊢ update (update f a v) b w c = update (update f b w) a v c

Proof state:
case pos
α : Sort u_2
inst✝ : DecidableEq α
β : α → Sort u_1
a b : α
h : a ≠ b
v : β a
w : β b
f : (a : α) → β a
c : α
h₁ : c = b
h₂ : c = a
⊢ ⋯ ▸ w = ⋯ ▸ v

Tactic:
cases h (h₂.symm.trans h₁)

Result:
no goals