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

State before:
α β γ : Type
g : α → Option β
x : α
⊢ comp_partial all_none g x = Option.none
Tactic:
simp [comp_partial, all_none]
State after:
α β γ : Type
g : α → Option β
x : α
⊢ (match g x with
    | Option.none => Option.none
    | Option.some y => Option.none) =
    Option.none

State before:
α β γ : Type
g : α → Option β
x : α
⊢ (match g x with
    | Option.none => Option.none
    | Option.some y => Option.none) =
    Option.none
Tactic:
split <;> rfl
State after:
no goals