Lean4
/-- `removeNe_aux` case splits on any proof `h : a ≠ b` in the input,
turning it into `a < b ∨ a > b`.
This produces `2^n` branches when there are `n` such hypotheses in the input.
-/
partial def removeNe_aux : MVarId → List Expr → MetaM (List Branch) := fun g hs => do
let some (e, α, a, b) ←
hs.findSomeM?
(fun e : Expr => do
let some (α, a, b) := (← instantiateMVars (← inferType e)).ne?' |
return none
return some (e, α, a, b)) |
return [(g, hs)]
let [ng1, ng2] ←
g.apply (← mkAppOptM ``Or.elim #[none, none, ← g.getType, ← mkAppOptM ``lt_or_gt_of_ne #[α, none, a, b, e]]) |
failure
let do_goal : MVarId → MetaM (List Branch) := fun g => do
let (f, h) ← g.intro1
h.withContext
(do
let ls ← removeNe_aux h <| hs.removeAll [e]
return ls.map (fun b : Branch => (b.1, (.fvar f) :: b.2)))
return ((← do_goal ng1) ++ (← do_goal ng2))
