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

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

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