[Merged by Bors] - fix: update context in recursive calls in split_ifs

[dwrensha]

Fixes #760.

Before this change, we were failing at an fvar lookup here:

mathlib4/Mathlib/Tactic/SplitIfs.lean

Line 44 in 91897c4

let typ ← instantiateMVars (← inferType (mkFVar fvarId))

[dwrensha]

I'm kind of confused about why this existing testcase works without this change:

mathlib4/test/SplitIfs.lean

Lines 13 to 18 in 91897c4

	example (x : Nat) (p q : Prop) [Decidable p] [Decidable q] :
	x = if p then (if q then x else x) else x := by
	split_ifs
	· rfl
	· rfl
	· rfl

[dwrensha]

Ah, the difference is that the new testcase puts the nested ifs within a hypothesis. So if I update the old testcase like this:

example (x : Nat) (p : Prop) [Decidable p]
    (h : x = if (if p then False else True) then y else y)
  : x = y := by
  split_ifs at h
  -- does not fully split

Then we get the same bad behavior (before we apply this PR).

[semorrison]

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style