case h
α✝ : Sort u
β✝ : α✝ → Sort v
α' : Sort w
inst✝² : DecidableEq α✝
inst✝¹ : DecidableEq α'
f✝ g : (a : α✝) → β✝ a
a✝ : α✝
b✝ : β✝ a✝
α : Sort u_1
inst✝ : DecidableEq α
β : α → Sort u_2
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
α✝ : Sort u
β✝ : α✝ → Sort v
α' : Sort w
inst✝² : DecidableEq α✝
inst✝¹ : DecidableEq α'
f✝ g : (a : α✝) → β✝ a
a✝ : α✝
b✝ : β✝ a✝
α : Sort u_1
inst✝ : DecidableEq α
β : α → Sort u_2
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
funext c
case h
α✝ : Sort u
β✝ : α✝ → Sort v
α' : Sort w
inst✝² : DecidableEq α✝
inst✝¹ : DecidableEq α'
f✝ g : (a : α✝) → β✝ a
a✝ : α✝
b✝ : β✝ a✝
α : Sort u_1
inst✝ : DecidableEq α
β : α → Sort u_2
a b : α
h : a ≠ b
v : β a
w : β b
f : (a : α) → β a
c : α
⊢ (if h : c = b then (_ : b = c) ▸ w else if h : c = a then (_ : a = c) ▸ v else f c) =
    if h : c = a then (_ : a = c) ▸ v else if h : c = b then (_ : b = c) ▸ w else f c
case h
α✝ : Sort u
β✝ : α✝ → Sort v
α' : Sort w
inst✝² : DecidableEq α✝
inst✝¹ : DecidableEq α'
f✝ g : (a : α✝) → β✝ a
a✝ : α✝
b✝ : β✝ a✝
α : Sort u_1
inst✝ : DecidableEq α
β : α → Sort u_2
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
simp only [update]
case pos
α✝ : Sort u
β✝ : α✝ → Sort v
α' : Sort w
inst✝² : DecidableEq α✝
inst✝¹ : DecidableEq α'
f✝ g : (a : α✝) → β✝ a
a✝ : α✝
b✝ : β✝ a✝
α : Sort u_1
inst✝ : DecidableEq α
β : α → Sort u_2
a b : α
h : a ≠ b
v : β a
w : β b
f : (a : α) → β a
c : α
h₁ : c = b
h₂ : c = a
⊢ (if h : c = b then (_ : b = c) ▸ w else if h : c = a then (_ : a = c) ▸ v else f c) =
    if h : c = a then (_ : a = c) ▸ v else if h : c = b then (_ : b = c) ▸ w else f c

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

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

case neg
α✝ : Sort u
β✝ : α✝ → Sort v
α' : Sort w
inst✝² : DecidableEq α✝
inst✝¹ : DecidableEq α'
f✝ g : (a : α✝) → β✝ a
a✝ : α✝
b✝ : β✝ a✝
α : Sort u_1
inst✝ : DecidableEq α
β : α → Sort u_2
a b : α
h : a ≠ b
v : β a
w : β b
f : (a : α) → β a
c : α
h₁ : ¬c = b
h₂ : ¬c = a
⊢ (if h : c = b then (_ : b = c) ▸ w else if h : c = a then (_ : a = c) ▸ v else f c) =
    if h : c = a then (_ : a = c) ▸ v else if h : c = b then (_ : b = c) ▸ w else f c
case h
α✝ : Sort u
β✝ : α✝ → Sort v
α' : Sort w
inst✝² : DecidableEq α✝
inst✝¹ : DecidableEq α'
f✝ g : (a : α✝) → β✝ a
a✝ : α✝
b✝ : β✝ a✝
α : Sort u_1
inst✝ : DecidableEq α
β : α → Sort u_2
a b : α
h : a ≠ b
v : β a
w : β b
f : (a : α) → β a
c : α
⊢ (if h : c = b then (_ : b = c) ▸ w else if h : c = a then (_ : a = c) ▸ v else f c) =
    if h : c = a then (_ : a = c) ▸ v else if h : c = b then (_ : b = c) ▸ w else f c
by_cases h₁ : c = b <;> by_cases h₂ : c = a
case pos
α✝ : Sort u
β✝ : α✝ → Sort v
α' : Sort w
inst✝² : DecidableEq α✝
inst✝¹ : DecidableEq α'
f✝ g : (a : α✝) → β✝ a
a✝ : α✝
b✝ : β✝ a✝
α : Sort u_1
inst✝ : DecidableEq α
β : α → Sort u_2
a b : α
h : a ≠ b
v : β a
w : β b
f : (a : α) → β a
c : α
h₁ : c = b
h₂ : c = a
⊢ (_ : b = c) ▸ w = (_ : a = c) ▸ v
case pos
α✝ : Sort u
β✝ : α✝ → Sort v
α' : Sort w
inst✝² : DecidableEq α✝
inst✝¹ : DecidableEq α'
f✝ g : (a : α✝) → β✝ a
a✝ : α✝
b✝ : β✝ a✝
α : Sort u_1
inst✝ : DecidableEq α
β : α → Sort u_2
a b : α
h : a ≠ b
v : β a
w : β b
f : (a : α) → β a
c : α
h₁ : c = b
h₂ : c = a
⊢ (if h : c = b then (_ : b = c) ▸ w else if h : c = a then (_ : a = c) ▸ v else f c) =
    if h : c = a then (_ : a = c) ▸ v else if h : c = b then (_ : b = c) ▸ w else f c
rw [dif_pos h₁, dif_pos h₂]
no goals
case pos
α✝ : Sort u
β✝ : α✝ → Sort v
α' : Sort w
inst✝² : DecidableEq α✝
inst✝¹ : DecidableEq α'
f✝ g : (a : α✝) → β✝ a
a✝ : α✝
b✝ : β✝ a✝
α : Sort u_1
inst✝ : DecidableEq α
β : α → Sort u_2
a b : α
h : a ≠ b
v : β a
w : β b
f : (a : α) → β a
c : α
h₁ : c = b
h₂ : c = a
⊢ (_ : b = c) ▸ w = (_ : a = c) ▸ v
cases h (h₂.symm.trans h₁)
no goals
case neg
α✝ : Sort u
β✝ : α✝ → Sort v
α' : Sort w
inst✝² : DecidableEq α✝
inst✝¹ : DecidableEq α'
f✝ g : (a : α✝) → β✝ a
a✝ : α✝
b✝ : β✝ a✝
α : Sort u_1
inst✝ : DecidableEq α
β : α → Sort u_2
a b : α
h : a ≠ b
v : β a
w : β b
f : (a : α) → β a
c : α
h₁ : c = b
h₂ : ¬c = a
⊢ (if h : c = b then (_ : b = c) ▸ w else if h : c = a then (_ : a = c) ▸ v else f c) =
    if h : c = a then (_ : a = c) ▸ v else if h : c = b then (_ : b = c) ▸ w else f c
rw [dif_pos h₁, dif_pos h₁, dif_neg h₂]
no goals
case pos
α✝ : Sort u
β✝ : α✝ → Sort v
α' : Sort w
inst✝² : DecidableEq α✝
inst✝¹ : DecidableEq α'
f✝ g : (a : α✝) → β✝ a
a✝ : α✝
b✝ : β✝ a✝
α : Sort u_1
inst✝ : DecidableEq α
β : α → Sort u_2
a b : α
h : a ≠ b
v : β a
w : β b
f : (a : α) → β a
c : α
h₁ : ¬c = b
h₂ : c = a
⊢ (if h : c = b then (_ : b = c) ▸ w else if h : c = a then (_ : a = c) ▸ v else f c) =
    if h : c = a then (_ : a = c) ▸ v else if h : c = b then (_ : b = c) ▸ w else f c
rw [dif_neg h₁, dif_neg h₁, dif_pos h₂]
no goals
case neg
α✝ : Sort u
β✝ : α✝ → Sort v
α' : Sort w
inst✝² : DecidableEq α✝
inst✝¹ : DecidableEq α'
f✝ g : (a : α✝) → β✝ a
a✝ : α✝
b✝ : β✝ a✝
α : Sort u_1
inst✝ : DecidableEq α
β : α → Sort u_2
a b : α
h : a ≠ b
v : β a
w : β b
f : (a : α) → β a
c : α
h₁ : ¬c = b
h₂ : ¬c = a
⊢ (if h : c = b then (_ : b = c) ▸ w else if h : c = a then (_ : a = c) ▸ v else f c) =
    if h : c = a then (_ : a = c) ▸ v else if h : c = b then (_ : b = c) ▸ w else f c
rw [dif_neg h₁, dif_neg h₁, dif_neg h₂]