Theorem: Partial.ext_restrict (ReactorModel/Extensions.lean)

State before:
α : Type u_1
β : Type u_2
s : Set α
f g : α ⇀ β
h : ∀ a ∈ s, f a = g a
inst✝ : DecidablePred fun x => x ∈ s
⊢ restrict f s = restrict g s
Tactic:
unfold restrict
State after:
α : Type u_1
β : Type u_2
s : Set α
f g : α ⇀ β
h : ∀ a ∈ s, f a = g a
inst✝ : DecidablePred fun x => x ∈ s
⊢ (fun a => if a ∈ s then f a else none) = fun a => if a ∈ s then g a else none

State before:
α : Type u_1
β : Type u_2
s : Set α
f g : α ⇀ β
h : ∀ a ∈ s, f a = g a
inst✝ : DecidablePred fun x => x ∈ s
⊢ (fun a => if a ∈ s then f a else none) = fun a => if a ∈ s then g a else none
Tactic:
funext
State after:
case h
α : Type u_1
β : Type u_2
s : Set α
f g : α ⇀ β
h : ∀ a ∈ s, f a = g a
inst✝ : DecidablePred fun x => x ∈ s
x✝ : α
⊢ (if x✝ ∈ s then f x✝ else none) = if x✝ ∈ s then g x✝ else none

State before:
case h
α : Type u_1
β : Type u_2
s : Set α
f g : α ⇀ β
h : ∀ a ∈ s, f a = g a
inst✝ : DecidablePred fun x => x ∈ s
x✝ : α
⊢ (if x✝ ∈ s then f x✝ else none) = if x✝ ∈ s then g x✝ else none
Tactic:
split <;> simp_all
State after:
no goals