Theorem: Interface?.merge_idem (Runtime/Interface.lean)

State before:
σ✝ : Interface.Scheme
i : Interface? σ✝
⊢ merge i i = i
Tactic:
funext var
State after:
case h
σ✝ : Interface.Scheme
i : Interface? σ✝
var : σ✝.vars
⊢ merge i i var = i var

State before:
case h
σ✝ : Interface.Scheme
i : Interface? σ✝
var : σ✝.vars
⊢ merge i i var = i var
Tactic:
simp [merge, Option.orElse]
State after:
case h
σ✝ : Interface.Scheme
i : Interface? σ✝
var : σ✝.vars
⊢ (match i var, fun x => i var with
    | some a, x => some a
    | none, b => b ()) =
    i var

State before:
case h
σ✝ : Interface.Scheme
i : Interface? σ✝
var : σ✝.vars
⊢ (match i var, fun x => i var with
    | some a, x => some a
    | none, b => b ()) =
    i var
Tactic:
split
State after:
case h.h_1
σ✝ : Interface.Scheme
i : Interface? σ✝
var : σ✝.vars
x✝¹ : Option (Interface.Scheme.type σ✝ var)
x✝ : Unit → Option (Interface.Scheme.type σ✝ var)
a✝ : Interface.Scheme.type σ✝ var
heq✝ : i var = some a✝
⊢ some a✝ = i var

case h.h_2
σ✝ : Interface.Scheme
i : Interface? σ✝
var : σ✝.vars
x✝¹ : Option (Interface.Scheme.type σ✝ var)
x✝ : Unit → Option (Interface.Scheme.type σ✝ var)
heq✝ : i var = none
⊢ (fun x => i var) () = i var