fix(Tactic/Lift): don't clear a variable if it's impossible (#30850)

Closes #19160.

Author: JovanGerb

Mathlib/Data/Set/Finite/Basic.lean

@@ -697,7 +697,7 @@ theorem Finite.induction_on {motive : ∀ s : Set α, s.Finite → Prop} (s : Se
     (insert : ∀ {a s}, a ∉ s →
       ∀ hs : Set.Finite s, motive s hs → motive (insert a s) (hs.insert a)) :
     motive s hs := by
-  lift s to Finset α using id hs
+  lift s to Finset α using hs
   induction s using Finset.cons_induction_on with
   | empty => simpa
   | cons a s ha ih => simpa using @insert a s ha (Set.toFinite _) (ih _)

Mathlib/GroupTheory/Perm/Cycle/Basic.lean

@@ -803,7 +803,7 @@ theorem IsCycleOn.exists_pow_eq {s : Finset α} (hf : f.IsCycleOn s) (ha : a ∈
 
 theorem IsCycleOn.exists_pow_eq' (hs : s.Finite) (hf : f.IsCycleOn s) (ha : a ∈ s) (hb : b ∈ s) :
     ∃ n : ℕ, (f ^ n) a = b := by
-  lift s to Finset α using id hs
+  lift s to Finset α using hs
   obtain ⟨n, -, hn⟩ := hf.exists_pow_eq ha hb
   exact ⟨n, hn⟩
 

Mathlib/Order/WithBot.lean

@@ -295,10 +295,8 @@ lemma unbot_le_iff (hx : x ≠ ⊥) : unbot x hx ≤ b ↔ x ≤ b := by lift x
 lemma unbotD_le_iff (hx : x = ⊥ → a ≤ b) : x.unbotD a ≤ b ↔ x ≤ b := by cases x <;> simp [hx]
 
 @[simp] lemma unbot_le_unbot (hx hy) : unbot x hx ≤ unbot y hy ↔ x ≤ y := by
-  -- TODO: Fix `lift` so that it doesn't try to clear the hypotheses I give it when it is
-  -- impossible to do so. See https://github.com/leanprover-community/mathlib4/issues/19160
-  lift x to α using id hx
-  lift y to α using id hy
+  lift x to α using hx
+  lift y to α using hy
   simp
 
 end LE
@@ -334,15 +332,13 @@ lemma lt_coe_iff : x < b ↔ ∀ a : α, x = a → a < b := by simp [lt_def]
 `PartialOrder α`. -/
 protected lemma bot_lt_iff_ne_bot : ⊥ < x ↔ x ≠ ⊥ := by cases x <;> simp
 
-lemma lt_unbot_iff (hy : y ≠ ⊥) : a < unbot y hy ↔ a < y := by lift y to α using id hy; simp
-lemma unbot_lt_iff (hx : x ≠ ⊥) : unbot x hx < b ↔ x < b := by lift x to α using id hx; simp
+lemma lt_unbot_iff (hy : y ≠ ⊥) : a < unbot y hy ↔ a < y := by lift y to α using hy; simp
+lemma unbot_lt_iff (hx : x ≠ ⊥) : unbot x hx < b ↔ x < b := by lift x to α using hx; simp
 lemma unbotD_lt_iff (hx : x = ⊥ → a < b) : x.unbotD a < b ↔ x < b := by cases x <;> simp [hx]
 
 @[simp] lemma unbot_lt_unbot (hx hy) : unbot x hx < unbot y hy ↔ x < y := by
-  -- TODO: Fix `lift` so that it doesn't try to clear the hypotheses I give it when it is
-  -- impossible to do so. See https://github.com/leanprover-community/mathlib4/issues/19160
-  lift x to α using id hx
-  lift y to α using id hy
+  lift x to α using hx
+  lift y to α using hy
   simp
 
 end LT

Mathlib/Tactic/Lift.lean

@@ -72,7 +72,8 @@ open Lean Parser Elab Tactic Meta
 * Usage: `'lift' expr 'to' expr ('using' expr)? ('with' id (id id?)?)?`.
 * If `n : ℤ` and `hn : n ≥ 0` then the tactic `lift n to ℕ using hn` creates a new
   constant of type `ℕ`, also named `n` and replaces all occurrences of the old variable `(n : ℤ)`
-  with `↑n` (where `n` in the new variable). It will remove `n` and `hn` from the context.
+  with `↑n` (where `n` in the new variable). It will clear `n` from the context and
+  try to clear `hn` from the context.
   + So for example the tactic `lift n to ℕ using hn` transforms the goal
     `n : ℤ, hn : n ≥ 0, h : P n ⊢ n = 3` to `n : ℕ, h : P ↑n ⊢ ↑n = 3`
     (here `P` is some term of type `ℤ → Prop`).
@@ -165,7 +166,6 @@ def Lift.main (e t : TSyntax `term) (hUsing : Option (TSyntax `term))
   -- Clear the "using" hypothesis if it's a variable in the context
   if prf.isFVar && !keepUsing then
     let some hUsingStx := hUsing | throwError "lift tactic failed: unreachable code was reached"
-    evalTactic (← `(tactic| clear $hUsingStx))
     evalTactic (← `(tactic| try clear $hUsingStx))
   if hUsing.isNone then withMainContext <| setGoals (prf.mvarId! :: (← getGoals))
 

MathlibTest/lift.lean

@@ -234,3 +234,12 @@ example {x : WithTop ℕ} (hx : x ≠ ⊤) (P : WithTop ℕ → Prop) (h : P x)
   lift x to ℕ using hx with u hu
   trace_state
   exact h
+
+/-! Test that the `h` in `using h` is not cleared if the goal depends on it. -/
+
+set_option linter.unusedVariables false in
+def foo (n : Int) (hn : 0 ≤ n) : Int := n
+
+example (n : Int) (hn : 0 ≤ n) : foo n hn = n := by
+  lift n to Nat using hn
+  rfl