Theorem: Function.funEqOn.of_subset (Logic/Vorspiel/Vorspiel.lean)

State before:
α : Type u
β : Type v
p q : α → Prop
f g : α → β
e : funEqOn p f g
h : ∀ (a : α), q a → p a
⊢ funEqOn q f g
Tactic:
intro a ha
State after:
α : Type u
β : Type v
p q : α → Prop
f g : α → β
e : funEqOn p f g
h : ∀ (a : α), q a → p a
a : α
ha : q a
⊢ f a = g a

State before:
α : Type u
β : Type v
p q : α → Prop
f g : α → β
e : funEqOn p f g
h : ∀ (a : α), q a → p a
a : α
ha : q a
⊢ f a = g a
Tactic:
exact e a (h a ha)
State after:
no goals