-- Mathlib/Logic/Equiv/Set.lean
theorem dite_comp_equiv_update {α : Type*} {β : Sort*} {γ : Sort*} {p : α → Prop}
    (e : β ≃ Subtype p)
    (v : β → γ) (w : α → γ) (j : β) (x : γ) [DecidableEq β] [DecidableEq α]
    [∀ j, Decidable (p j)] :
    (fun i : α => if h : p i then (Function.update v j x) (e.symm ⟨i, h⟩) else w i) =
      Function.update (fun i : α => if h : p i then v (e.symm ⟨i, h⟩) else w i) (e j) x

Proof state:
case neg
α : Type u_1
β : Sort u_2
γ : Sort u_3
p : α → Prop
e : β ≃ Subtype p
v : β → γ
w : α → γ
j : β
x : γ
inst✝² : DecidableEq β
inst✝¹ : DecidableEq α
inst✝ : (j : α) → Decidable (p j)
i : α
h : ¬p i
⊢ (if h : p i then update v j x (e.symm ⟨i, h⟩) else w i) =
    update (fun i => if h : p i then v (e.symm ⟨i, h⟩) else w i) (↑(e j)) x i

Tactic:
have : i ≠ e j := by
  contrapose! h
  have : p (e j : α) := (e j).2
  rwa [← h] at this

Result:
case neg
α : Type u_1
β : Sort u_2
γ : Sort u_3
p : α → Prop
e : β ≃ Subtype p
v : β → γ
w : α → γ
j : β
x : γ
inst✝² : DecidableEq β
inst✝¹ : DecidableEq α
inst✝ : (j : α) → Decidable (p j)
i : α
h : ¬p i
this : i ≠ ↑(e j)
⊢ (if h : p i then update v j x (e.symm ⟨i, h⟩) else w i) =
    update (fun i => if h : p i then v (e.symm ⟨i, h⟩) else w i) (↑(e j)) x i

Proof state:
case neg
α : Type u_1
β : Sort u_2
γ : Sort u_3
p : α → Prop
e : β ≃ Subtype p
v : β → γ
w : α → γ
j : β
x : γ
inst✝² : DecidableEq β
inst✝¹ : DecidableEq α
inst✝ : (j : α) → Decidable (p j)
i : α
h : ¬p i
this : i ≠ ↑(e j)
⊢ (if h : p i then update v j x (e.symm ⟨i, h⟩) else w i) =
    update (fun i => if h : p i then v (e.symm ⟨i, h⟩) else w i) (↑(e j)) x i

Tactic:
simp [h, this]

Result:
no goals

Proof state:
α : Type u_1
β : Sort u_2
γ : Sort u_3
p : α → Prop
e : β ≃ Subtype p
v : β → γ
w : α → γ
j : β
x : γ
inst✝² : DecidableEq β
inst✝¹ : DecidableEq α
inst✝ : (j : α) → Decidable (p j)
i : α
h : p i
⊢ ↑⟨i, h⟩ = ↑(e j) ↔ i = ↑(e j)

Tactic:
rw [Subtype.coe_mk]

Result:
no goals

Proof state:
case pos
α : Type u_1
β : Sort u_2
γ : Sort u_3
p : α → Prop
e : β ≃ Subtype p
v : β → γ
w : α → γ
j : β
x : γ
inst✝² : DecidableEq β
inst✝¹ : DecidableEq α
inst✝ : (j : α) → Decidable (p j)
i : α
h : p i
⊢ (if ⟨i, h⟩ = e j then x else (v ∘ ⇑e.symm) ⟨i, h⟩) = if i = ↑(e j) then x else v (e.symm ⟨i, h⟩)

Tactic:
have h_coe : (⟨i, h⟩ : Subtype p) = e j ↔ i = e j :=
  Subtype.ext_iff.trans (by rw [Subtype.coe_mk])

Result:
case pos
α : Type u_1
β : Sort u_2
γ : Sort u_3
p : α → Prop
e : β ≃ Subtype p
v : β → γ
w : α → γ
j : β
x : γ
inst✝² : DecidableEq β
inst✝¹ : DecidableEq α
inst✝ : (j : α) → Decidable (p j)
i : α
h : p i
h_coe : ⟨i, h⟩ = e j ↔ i = ↑(e j)
⊢ (if ⟨i, h⟩ = e j then x else (v ∘ ⇑e.symm) ⟨i, h⟩) = if i = ↑(e j) then x else v (e.symm ⟨i, h⟩)

Proof state:
case pos
α : Type u_1
β : Sort u_2
γ : Sort u_3
p : α → Prop
e : β ≃ Subtype p
v : β → γ
w : α → γ
j : β
x : γ
inst✝² : DecidableEq β
inst✝¹ : DecidableEq α
inst✝ : (j : α) → Decidable (p j)
i : α
h : p i
⊢ (if h : p i then update v j x (e.symm ⟨i, h⟩) else w i) =
    update (fun i => if h : p i then v (e.symm ⟨i, h⟩) else w i) (↑(e j)) x i

Tactic:
rw [dif_pos h, Function.update_apply_equiv_apply, Equiv.symm_symm,
  Function.update_apply, Function.update_apply, dif_pos h]

Result:
case pos
α : Type u_1
β : Sort u_2
γ : Sort u_3
p : α → Prop
e : β ≃ Subtype p
v : β → γ
w : α → γ
j : β
x : γ
inst✝² : DecidableEq β
inst✝¹ : DecidableEq α
inst✝ : (j : α) → Decidable (p j)
i : α
h : p i
⊢ (if ⟨i, h⟩ = e j then x else (v ∘ ⇑e.symm) ⟨i, h⟩) = if i = ↑(e j) then x else v (e.symm ⟨i, h⟩)

Proof state:
α : Type u_1
β : Sort u_2
γ : Sort u_3
p : α → Prop
e : β ≃ Subtype p
v : β → γ
w : α → γ
j : β
x : γ
inst✝² : DecidableEq β
inst✝¹ : DecidableEq α
inst✝ : (j : α) → Decidable (p j)
⊢ (fun i => if h : p i then update v j x (e.symm ⟨i, h⟩) else w i) =
    update (fun i => if h : p i then v (e.symm ⟨i, h⟩) else w i) (↑(e j)) x

Tactic:
ext i

Result:
case h
α : Type u_1
β : Sort u_2
γ : Sort u_3
p : α → Prop
e : β ≃ Subtype p
v : β → γ
w : α → γ
j : β
x : γ
inst✝² : DecidableEq β
inst✝¹ : DecidableEq α
inst✝ : (j : α) → Decidable (p j)
i : α
⊢ (if h : p i then update v j x (e.symm ⟨i, h⟩) else w i) =
    update (fun i => if h : p i then v (e.symm ⟨i, h⟩) else w i) (↑(e j)) x i

Proof state:
case pos
α : Type u_1
β : Sort u_2
γ : Sort u_3
p : α → Prop
e : β ≃ Subtype p
v : β → γ
w : α → γ
j : β
x : γ
inst✝² : DecidableEq β
inst✝¹ : DecidableEq α
inst✝ : (j : α) → Decidable (p j)
i : α
h : p i
h_coe : ⟨i, h⟩ = e j ↔ i = ↑(e j)
⊢ (if ⟨i, h⟩ = e j then x else (v ∘ ⇑e.symm) ⟨i, h⟩) = if i = ↑(e j) then x else v (e.symm ⟨i, h⟩)

Tactic:
simp [h_coe]

Result:
no goals

Proof state:
case h
α : Type u_1
β : Sort u_2
γ : Sort u_3
p : α → Prop
e : β ≃ Subtype p
v : β → γ
w : α → γ
j : β
x : γ
inst✝² : DecidableEq β
inst✝¹ : DecidableEq α
inst✝ : (j : α) → Decidable (p j)
i : α
⊢ (if h : p i then update v j x (e.symm ⟨i, h⟩) else w i) =
    update (fun i => if h : p i then v (e.symm ⟨i, h⟩) else w i) (↑(e j)) x i

Tactic:
by_cases h : p i

Result:
case pos
α : Type u_1
β : Sort u_2
γ : Sort u_3
p : α → Prop
e : β ≃ Subtype p
v : β → γ
w : α → γ
j : β
x : γ
inst✝² : DecidableEq β
inst✝¹ : DecidableEq α
inst✝ : (j : α) → Decidable (p j)
i : α
h : p i
⊢ (if h : p i then update v j x (e.symm ⟨i, h⟩) else w i) =
    update (fun i => if h : p i then v (e.symm ⟨i, h⟩) else w i) (↑(e j)) x i

case neg
α : Type u_1
β : Sort u_2
γ : Sort u_3
p : α → Prop
e : β ≃ Subtype p
v : β → γ
w : α → γ
j : β
x : γ
inst✝² : DecidableEq β
inst✝¹ : DecidableEq α
inst✝ : (j : α) → Decidable (p j)
i : α
h : ¬p i
⊢ (if h : p i then update v j x (e.symm ⟨i, h⟩) else w i) =
    update (fun i => if h : p i then v (e.symm ⟨i, h⟩) else w i) (↑(e j)) x i

Proof state:
α : Type u_1
β : Sort u_2
γ : Sort u_3
p : α → Prop
e : β ≃ Subtype p
v : β → γ
w : α → γ
j : β
x : γ
inst✝² : DecidableEq β
inst✝¹ : DecidableEq α
inst✝ : (j : α) → Decidable (p j)
i : α
h : i = ↑(e j)
⊢ p i

Tactic:
have : p (e j : α) := (e j).2

Result:
α : Type u_1
β : Sort u_2
γ : Sort u_3
p : α → Prop
e : β ≃ Subtype p
v : β → γ
w : α → γ
j : β
x : γ
inst✝² : DecidableEq β
inst✝¹ : DecidableEq α
inst✝ : (j : α) → Decidable (p j)
i : α
h : i = ↑(e j)
this : p ↑(e j)
⊢ p i

Proof state:
α : Type u_1
β : Sort u_2
γ : Sort u_3
p : α → Prop
e : β ≃ Subtype p
v : β → γ
w : α → γ
j : β
x : γ
inst✝² : DecidableEq β
inst✝¹ : DecidableEq α
inst✝ : (j : α) → Decidable (p j)
i : α
h : i = ↑(e j)
this : p ↑(e j)
⊢ p i

Tactic:
rwa [← h] at this

Result:
no goals

Proof state:
α : Type u_1
β : Sort u_2
γ : Sort u_3
p : α → Prop
e : β ≃ Subtype p
v : β → γ
w : α → γ
j : β
x : γ
inst✝² : DecidableEq β
inst✝¹ : DecidableEq α
inst✝ : (j : α) → Decidable (p j)
i : α
h : ¬p i
⊢ i ≠ ↑(e j)

Tactic:
contrapose! h

Result:
α : Type u_1
β : Sort u_2
γ : Sort u_3
p : α → Prop
e : β ≃ Subtype p
v : β → γ
w : α → γ
j : β
x : γ
inst✝² : DecidableEq β
inst✝¹ : DecidableEq α
inst✝ : (j : α) → Decidable (p j)
i : α
h : i = ↑(e j)
⊢ p i