case h
α✝ : Sort u
β✝ : Sort v
γ✝ : Sort w
α : 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 { val := i, property := h }) else w i) =
    update (fun i => if h : p i then v (↑e.symm { val := i, property := h }) else w i) (↑(↑e j)) x i
α✝ : Sort u
β✝ : Sort v
γ✝ : Sort w
α : 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 { val := i, property := h }) else w i) =
    update (fun i => if h : p i then v (↑e.symm { val := i, property := h }) else w i) (↑(↑e j)) x
ext i
case pos
α✝ : Sort u
β✝ : Sort v
γ✝ : Sort w
α : 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 { val := i, property := h }) else w i) =
    update (fun i => if h : p i then v (↑e.symm { val := i, property := h }) else w i) (↑(↑e j)) x i

case neg
α✝ : Sort u
β✝ : Sort v
γ✝ : Sort w
α : 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 { val := i, property := h }) else w i) =
    update (fun i => if h : p i then v (↑e.symm { val := i, property := h }) else w i) (↑(↑e j)) x i
case h
α✝ : Sort u
β✝ : Sort v
γ✝ : Sort w
α : 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 { val := i, property := h }) else w i) =
    update (fun i => if h : p i then v (↑e.symm { val := i, property := h }) else w i) (↑(↑e j)) x i
by_cases h : p i
case pos
α✝ : Sort u
β✝ : Sort v
γ✝ : Sort w
α : 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 { val := i, property := h } = ↑e j then x else (v ∘ ↑e.symm) { val := i, property := h }) =
    if i = ↑(↑e j) then x else v (↑e.symm { val := i, property := h })
case pos
α✝ : Sort u
β✝ : Sort v
γ✝ : Sort w
α : 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 { val := i, property := h }) else w i) =
    update (fun i => if h : p i then v (↑e.symm { val := i, property := h }) else w i) (↑(↑e j)) x i
rw [dif_pos h, Function.update_apply_equiv_apply, Equiv.symm_symm,
  Function.update_apply, Function.update_apply, dif_pos h]
case pos
α✝ : Sort u
β✝ : Sort v
γ✝ : Sort w
α : 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 : { val := i, property := h } = ↑e j ↔ i = ↑(↑e j)
⊢ (if { val := i, property := h } = ↑e j then x else (v ∘ ↑e.symm) { val := i, property := h }) =
    if i = ↑(↑e j) then x else v (↑e.symm { val := i, property := h })
case pos
α✝ : Sort u
β✝ : Sort v
γ✝ : Sort w
α : 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 { val := i, property := h } = ↑e j then x else (v ∘ ↑e.symm) { val := i, property := h }) =
    if i = ↑(↑e j) then x else v (↑e.symm { val := i, property := h })
have h_coe : (⟨i, h⟩ : Subtype p) = e j ↔ i = e j :=
  Subtype.ext_iff.trans (by rw [Subtype.coe_mk])
no goals
case pos
α✝ : Sort u
β✝ : Sort v
γ✝ : Sort w
α : 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 : { val := i, property := h } = ↑e j ↔ i = ↑(↑e j)
⊢ (if { val := i, property := h } = ↑e j then x else (v ∘ ↑e.symm) { val := i, property := h }) =
    if i = ↑(↑e j) then x else v (↑e.symm { val := i, property := h })
simp [h_coe]
no goals
α✝ : Sort u
β✝ : Sort v
γ✝ : Sort w
α : 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
⊢ ↑{ val := i, property := h } = ↑(↑e j) ↔ i = ↑(↑e j)
rw [Subtype.coe_mk]
case neg
α✝ : Sort u
β✝ : Sort v
γ✝ : Sort w
α : 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 { val := i, property := h }) else w i) =
    update (fun i => if h : p i then v (↑e.symm { val := i, property := h }) else w i) (↑(↑e j)) x i
case neg
α✝ : Sort u
β✝ : Sort v
γ✝ : Sort w
α : 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 { val := i, property := h }) else w i) =
    update (fun i => if h : p i then v (↑e.symm { val := i, property := h }) else w i) (↑(↑e j)) x i
have : i ≠ e j := by
  contrapose! h
  have : p (e j : α) := (e j).2
  rwa [← h] at this
no goals
case neg
α✝ : Sort u
β✝ : Sort v
γ✝ : Sort w
α : 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 { val := i, property := h }) else w i) =
    update (fun i => if h : p i then v (↑e.symm { val := i, property := h }) else w i) (↑(↑e j)) x i
simp [h, this]
α✝ : Sort u
β✝ : Sort v
γ✝ : Sort w
α : 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
α✝ : Sort u
β✝ : Sort v
γ✝ : Sort w
α : 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)
contrapose! h
α✝ : Sort u
β✝ : Sort v
γ✝ : Sort w
α : 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
α✝ : Sort u
β✝ : Sort v
γ✝ : Sort w
α : 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
have : p (e j : α) := (e j).2
no goals
α✝ : Sort u
β✝ : Sort v
γ✝ : Sort w
α : 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
rwa [← h] at this