Theorem: PartialComposition.comp_with_all_none_eq_all_none (TheoremProvingLean/inductive_types.lean)

State before:
α β γ : Type
f : β → Option γ
x✝ : α
⊢ comp_partial f all_none = all_none
Tactic:
funext
State after:
case h
α β γ : Type
f : β → Option γ
x✝¹ x✝ : α
⊢ comp_partial f all_none x✝ = all_none x✝

State before:
case h
α β γ : Type
f : β → Option γ
x✝¹ x✝ : α
⊢ comp_partial f all_none x✝ = all_none x✝
Tactic:
apply comp_with_all_none
State after:
no goals