/-
Copyright (c) 2019 Floris van Doorn. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Floris van Doorn
Ported by: Yury Kudryashov, Frédéric Dupuis
-/
import Mathlib.Tactic.Cases
import Mathlib.Tactic.PermuteGoals
import Mathlib.Init.Data.Int.Order

/-!
# lift tactic

This file defines the `lift` tactic, allowing the user to lift elements from one type to another
under a specified condition.

## Tags

lift, tactic
-/

/-- A class specifying that you can lift elements from `α` to `β` assuming `cond` is true.
  Used by the tactic `lift`. -/
class CanLift: {α : Sort u_1} →
  {β : Sort u_2} →
    {coe : outParam (β → α)} →
      {cond : outParam (α → Prop)} → (∀ (x : α), cond x → ∃ y, coe y = x) → CanLift α β coe cond
CanLift (α: Sort ?u.2
α β: Sort ?u.5
β : Sort _: Type ?u.2
SortSort _: Type ?u.2
 _) (coe: outParam (β → α)
coe : outParam: Sort ?u.8 → Sort ?u.8
outParam <| β: Sort ?u.5
β → α: Sort ?u.2
α) (cond: outParam (α → Prop)
cond : outParam: Sort ?u.15 → Sort ?u.15
outParam <| α: Sort ?u.2
α → Prop: Type
Prop) where
  /-- An element of `α` that satisfies `cond` belongs to the range of `coe`. -/
  prf: ∀ {α : Sort u_1} {β : Sort u_2} {coe : outParam (β → α)} {cond : outParam (α → Prop)} [self : CanLift α β coe cond]
  (x : α), cond x → ∃ y, coe y = x
prf : ∀ x: α
x : α: Sort ?u.2
α, cond: outParam (α → Prop)
cond x: α
x → ∃ y: β
y : β: Sort ?u.5
β, coe: outParam (β → α)
coe y: β
y = x: α
x
#align can_lift CanLift: (α : Sort u_1) → (β : Sort u_2) → outParam (β → α) → outParam (α → Prop) → Type
CanLift

instance: CanLift ℤ ℕ (fun n => ↑n) fun x => 0 ≤ x
instance : CanLift: (α : Sort ?u.42) → (β : Sort ?u.41) → outParam (β → α) → outParam (α → Prop) → Type
CanLift ℤ: Type
ℤ ℕ: Type
ℕ (fun n: ℕ
n : ℕ: Type
ℕ ↦ n: ℕ
n) (0 ≤ ·): ℤ → Prop
(0 ≤ ·) :=
  ⟨fun n: ?m.141
n hn: ?m.144
hn ↦ ⟨n: ?m.141
n.natAbs: ℤ → ℕ
natAbs, Int.natAbs_of_nonneg: ∀ {a : ℤ}, 0 ≤ a → ↑(Int.natAbs a) = a
Int.natAbs_of_nonneg hn: ?m.144
hn⟩⟩

/-- Enable automatic handling of pi types in `CanLift`. -/
instance Pi.canLift: (ι : Sort u_1) →
  (α : ι → Sort u_2) →
    (β : ι → Sort u_3) →
      (coe : (i : ι) → β i → α i) →
        (P : (i : ι) → α i → Prop) →
          [inst : (i : ι) → CanLift (α i) (β i) (coe i) (P i)] →
            CanLift ((i : ι) → α i) ((i : ι) → β i) (fun f i => coe i (f i)) fun f => ∀ (i : ι), P i (f i)
Pi.canLift (ι: Sort ?u.282
ι : Sort _: Type ?u.282
SortSort _: Type ?u.282
 _) (α: ι → Sort ?u.287
α β: ι → Sort ?u.292
β : ι: Sort ?u.282
ι → Sort _: Type ?u.287
SortSort _: Type ?u.287
 _) (coe: (i : ι) → β i → α i
coe : ∀ i: ?m.296
i, β: ι → Sort ?u.292
β i: ?m.296
i → α: ι → Sort ?u.287
α i: ?m.296
i) (P: (i : ι) → α i → Prop
P : ∀ i: ?m.304
i, α: ι → Sort ?u.287
α i: ?m.304
i → Prop: Type
Prop)
    [∀ i: ?m.312
i, CanLift: (α : Sort ?u.316) → (β : Sort ?u.315) → outParam (β → α) → outParam (α → Prop) → Type
CanLift (α: ι → Sort ?u.287
α i: ?m.312
i) (β: ι → Sort ?u.292
β i: ?m.312
i) (coe: (i : ι) → β i → α i
coe i: ?m.312
i) (P: (i : ι) → α i → Prop
P i: ?m.312
i)] :
    CanLift: (α : Sort ?u.323) → (β : Sort ?u.322) → outParam (β → α) → outParam (α → Prop) → Type
CanLift (∀ i: ?m.325
i, α: ι → Sort ?u.287
α i: ?m.325
i) (∀ i: ?m.330
i, β: ι → Sort ?u.292
β i: ?m.330
i) (fun f: ?m.335
f i: ?m.339
i ↦ coe: (i : ι) → β i → α i
coe i: ?m.339
i (f: ?m.335
f i: ?m.339
i)) fun f: ?m.344
f ↦ ∀ i: ?m.348
i, P: (i : ι) → α i → Prop
P i: ?m.348
i (f: ?m.344
f i: ?m.348
i) where
  prf f: ?m.388
f hf: ?m.392
hf := ⟨fun i: ?m.409
i => Classical.choose: {α : Sort ?u.411} → {p : α → Prop} → (∃ x, p x) → α
Classical.choose (CanLift.prf: ∀ {α : Sort ?u.415} {β : Sort ?u.414} {coe : outParam (β → α)} {cond : outParam (α → Prop)}
  [self : CanLift α β coe cond] (x : α), cond x → ∃ y, coe y = x
CanLift.prf (f: ?m.388
f i: ?m.409
i) (hf: ?m.392
hf i: ?m.409
i)),
    funext: ∀ {α : Sort ?u.465} {β : α → Sort ?u.464} {f g : (x : α) → β x}, (∀ (x : α), f x = g x) → f = g
funext fun i: ?m.480
i => Classical.choose_spec: ∀ {α : Sort ?u.482} {p : α → Prop} (h : ∃ x, p x), p (Classical.choose h)
Classical.choose_spec (CanLift.prf: ∀ {α : Sort ?u.486} {β : Sort ?u.485} {coe : outParam (β → α)} {cond : outParam (α → Prop)}
  [self : CanLift α β coe cond] (x : α), cond x → ∃ y, coe y = x
CanLift.prf (f: ?m.388
f i: ?m.480
i) (hf: ?m.392
hf i: ?m.480
i))⟩
#align pi.can_lift Pi.canLift: (ι : Sort u_1) →
  (α : ι → Sort u_2) →
    (β : ι → Sort u_3) →
      (coe : (i : ι) → β i → α i) →
        (P : (i : ι) → α i → Prop) →
          [inst : (i : ι) → CanLift (α i) (β i) (coe i) (P i)] →
            CanLift ((i : ι) → α i) ((i : ι) → β i) (fun f i => coe i (f i)) fun f => ∀ (i : ι), P i (f i)
Pi.canLift

theorem Subtype.exists_pi_extension: ∀ {ι : Sort u_1} {α : ι → Sort u_2} [ne : ∀ (i : ι), Nonempty (α i)] {p : ι → Prop} (f : (i : Subtype p) → α i.val),
  ∃ g, (fun i => g i.val) = f
Subtype.exists_pi_extension {ι: Sort ?u.757
ι : Sort _: Type ?u.757
SortSort _: Type ?u.757
 _} {α: ι → Sort u_2
α : ι: Sort ?u.757
ι → Sort _: Type ?u.762
SortSort _: Type ?u.762
 _} [ne: ∀ (i : ι), Nonempty (α i)
ne : ∀ i: ?m.766
i, Nonempty: Sort ?u.769 → Prop
Nonempty (α: ι → Sort ?u.762
α i: ?m.766
i)]
    {p: ι → Prop
p : ι: Sort ?u.757
ι → Prop: Type
Prop} (f: (i : Subtype p) → α i.val
f : ∀ i: Subtype p
i : Subtype: {α : Sort ?u.778} → (α → Prop) → Sort (max1?u.778)
Subtype p: ι → Prop
p, α: ι → Sort ?u.762
α i: Subtype p
i) :
    ∃ g: (i : ι) → α i
g : ∀ i: ι
i : ι: Sort ?u.757
ι, α: ι → Sort ?u.762
α i: ι
i, (fun i: Subtype p
i : Subtype: {α : Sort ?u.916} → (α → Prop) → Sort (max1?u.916)
Subtype p: ι → Prop
p => g: (i : ι) → α i
g i: Subtype p
i) = f: (i : Subtype p) → α i.val
f := by
Goals accomplished! 🐙
  ι: Sort u_1

α: ι → Sort u_2

ne: ∀ (i : ι), Nonempty (α i)

p: ι → Prop

f: (i : Subtype p) → α i.val

∃ g, (fun i => g i.val) = fhaveI : DecidablePred: {α : Sort ?u.1025} → (α → Prop) → Sort (max1?u.1025)
DecidablePred p: ι → Prop
p := fun i: ?m.1031
i ↦ Classical.propDecidable: (a : Prop) → Decidable a
Classical.propDecidable (p: ι → Prop
p i: ?m.1031
i)ι: Sort u_1

α: ι → Sort u_2

ne: ∀ (i : ι), Nonempty (α i)

p: ι → Prop

f: (i : Subtype p) → α i.val

this: DecidablePred p

∃ g, (fun i => g i.val) = f
  ι: Sort u_1

α: ι → Sort u_2

ne: ∀ (i : ι), Nonempty (α i)

p: ι → Prop

f: (i : Subtype p) → α i.val

∃ g, (fun i => g i.val) = fexact ⟨fun i: ?m.1052
i => if hi: ?m.1065
hi : p: ι → Prop
p i: ?m.1052
i then f: (i : Subtype p) → α i.val
f ⟨i: ?m.1052
i, hi: ?m.1065
hi⟩ else Classical.choice: {α : Sort ?u.1084} → Nonempty α → α
Classical.choice (ne: ∀ (i : ι), Nonempty (α i)
ne i: ?m.1052
i),
    funext: ∀ {α : Sort ?u.1092} {β : α → Sort ?u.1091} {f g : (x : α) → β x}, (∀ (x : α), f x = g x) → f = g
funext fun i: ?m.1108
i ↦ dif_pos: ∀ {c : Prop} {h : Decidable c} (hc : c) {α : Sort ?u.1110} {t : c → α} {e : ¬c → α}, dite c t e = t hc
dif_pos i: ?m.1108
i.2: ∀ {α : Sort ?u.1113} {p : α → Prop} (self : Subtype p), p self.val
2⟩
Goals accomplished! 🐙
#align subtype.exists_pi_extension Subtype.exists_pi_extension: ∀ {ι : Sort u_1} {α : ι → Sort u_2} [ne : ∀ (i : ι), Nonempty (α i)] {p : ι → Prop} (f : (i : Subtype p) → α i.val),
  ∃ g, (fun i => g i.val) = f
Subtype.exists_pi_extension

instance PiSubtype.canLift: (ι : Sort ?u.1159) →
  (α : ι → Sort ?u.1164) →
    [inst : ∀ (i : ι), Nonempty (α i)] →
      (p : ι → Prop) → CanLift ((i : Subtype p) → α i.val) ((i : ι) → α i) (fun f i => f i.val) fun x => True
PiSubtype.canLift (ι: Sort ?u.1159
ι : Sort _: Type ?u.1159
SortSort _: Type ?u.1159
 _) (α: ι → Sort ?u.1164
α : ι: Sort ?u.1159
ι → Sort _: Type ?u.1164
SortSort _: Type ?u.1164
 _) [∀ i: ?m.1168
i, Nonempty: Sort ?u.1171 → Prop
Nonempty (α: ι → Sort ?u.1164
α i: ?m.1168
i)] (p: ι → Prop
p : ι: Sort ?u.1159
ι → Prop: Type
Prop) :
    CanLift: (α : Sort ?u.1180) → (β : Sort ?u.1179) → outParam (β → α) → outParam (α → Prop) → Type
CanLift (∀ i: Subtype p
i : Subtype: {α : Sort ?u.1182} → (α → Prop) → Sort (max1?u.1182)
Subtype p: ι → Prop
p, α: ι → Sort ?u.1164
α i: Subtype p
i) (∀ i: ?m.1310
i, α: ι → Sort ?u.1164
α i: ?m.1310
i) (fun f: ?m.1315
f i: ?m.1319
i => f: ?m.1315
f i: ?m.1319
i) fun _: ?m.1411
_ => True: Prop
True where
  prf f: ?m.1448
f _: ?m.1452
_ := Subtype.exists_pi_extension: ∀ {ι : Sort ?u.1454} {α : ι → Sort ?u.1455} [ne : ∀ (i : ι), Nonempty (α i)] {p : ι → Prop}
  (f : (i : Subtype p) → α i.val), ∃ g, (fun i => g i.val) = f
Subtype.exists_pi_extension f: ?m.1448
f
#align pi_subtype.can_lift PiSubtype.canLift: (ι : Sort u_1) →
  (α : ι → Sort u_2) →
    [inst : ∀ (i : ι), Nonempty (α i)] →
      (p : ι → Prop) → CanLift ((i : Subtype p) → α i.val) ((i : ι) → α i) (fun f i => f i.val) fun x => True
PiSubtype.canLift

-- TODO: test if we need this instance in Lean 4
instance PiSubtype.canLift': (ι : Sort u_1) →
  (α : Sort u_2) →
    [inst : Nonempty α] → (p : ι → Prop) → CanLift (Subtype p → α) (ι → α) (fun f i => f i.val) fun x => True
PiSubtype.canLift' (ι: Sort ?u.1632
ι : Sort _: Type ?u.1632
SortSort _: Type ?u.1632
 _) (α: Sort ?u.1635
α : Sort _: Type ?u.1635
SortSort _: Type ?u.1635
 _) [Nonempty: Sort ?u.1638 → Prop
Nonempty α: Sort ?u.1635
α] (p: ι → Prop
p : ι: Sort ?u.1632
ι → Prop: Type
Prop) :
    CanLift: (α : Sort ?u.1646) → (β : Sort ?u.1645) → outParam (β → α) → outParam (α → Prop) → Type
CanLift (Subtype: {α : Sort ?u.1648} → (α → Prop) → Sort (max1?u.1648)
Subtype p: ι → Prop
p → α: Sort ?u.1635
α) (ι: Sort ?u.1632
ι → α: Sort ?u.1635
α) (fun f: ?m.1659
f i: ?m.1663
i => f: ?m.1659
f i: ?m.1663
i) fun _: ?m.1786
_ => True: Prop
True :=
  PiSubtype.canLift: (ι : Sort ?u.1804) →
  (α : ι → Sort ?u.1803) →
    [inst : ∀ (i : ι), Nonempty (α i)] →
      (p : ι → Prop) → CanLift ((i : Subtype p) → α i.val) ((i : ι) → α i) (fun f i => f i.val) fun x => True
PiSubtype.canLift ι: Sort ?u.1632
ι (fun _: ?m.1806
_ => α: Sort ?u.1635
α) p: ι → Prop
p
#align pi_subtype.can_lift' PiSubtype.canLift': (ι : Sort u_1) →
  (α : Sort u_2) →
    [inst : Nonempty α] → (p : ι → Prop) → CanLift (Subtype p → α) (ι → α) (fun f i => f i.val) fun x => True
PiSubtype.canLift'

instance Subtype.canLift: {α : Sort ?u.1932} → (p : α → Prop) → CanLift α { x // p x } val p
Subtype.canLift {α: Sort ?u.1932
α : Sort _: Type ?u.1932
SortSort _: Type ?u.1932
 _} (p: α → Prop
p : α: Sort ?u.1932
α → Prop: Type
Prop) :
    CanLift: (α : Sort ?u.1940) → (β : Sort ?u.1939) → outParam (β → α) → outParam (α → Prop) → Type
CanLift α: Sort ?u.1932
α { x: ?m.1944
x // p: α → Prop
p x: ?m.1944
x } Subtype.val: {α : Sort ?u.1948} → {p : α → Prop} → Subtype p → α
Subtype.val p: α → Prop
p where prf a: ?m.1978
a ha: ?m.1981
ha :=
  ⟨⟨a: ?m.1978
a, ha: ?m.1981
ha⟩, rfl: ∀ {α : Sort ?u.2004} {a : α}, a = a
rfl⟩
#align subtype.can_lift Subtype.canLift: {α : Sort u_1} → (p : α → Prop) → CanLift α { x // p x } Subtype.val p
Subtype.canLift

namespace Mathlib.Tactic

open Lean Parser Tactic Elab Tactic Meta

/-- Lift an expression to another type.
* 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.
  + 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`).
* The argument `using hn` is optional, the tactic `lift n to ℕ` does the same, but also creates a
  new subgoal that `n ≥ 0` (where `n` is the old variable).
  This subgoal will be placed at the top of the goal list.
  + So for example the tactic `lift n to ℕ` transforms the goal
    `n : ℤ, h : P n ⊢ n = 3` to two goals
    `n : ℤ, h : P n ⊢ n ≥ 0` and `n : ℕ, h : P ↑n ⊢ ↑n = 3`.
* You can also use `lift n to ℕ using e` where `e` is any expression of type `n ≥ 0`.
* Use `lift n to ℕ with k` to specify the name of the new variable.
* Use `lift n to ℕ with k hk` to also specify the name of the equality `↑k = n`. In this case, `n`
  will remain in the context. You can use `rfl` for the name of `hk` to substitute `n` away
  (i.e. the default behavior).
* You can also use `lift e to ℕ with k hk` where `e` is any expression of type `ℤ`.
  In this case, the `hk` will always stay in the context, but it will be used to rewrite `e` in
  all hypotheses and the target.
  + So for example the tactic `lift n + 3 to ℕ using hn with k hk` transforms the goal
    `n : ℤ, hn : n + 3 ≥ 0, h : P (n + 3) ⊢ n + 3 = 2 * n` to the goal
    `n : ℤ, k : ℕ, hk : ↑k = n + 3, h : P ↑k ⊢ ↑k = 2 * n`.
* The tactic `lift n to ℕ using h` will remove `h` from the context. If you want to keep it,
  specify it again as the third argument to `with`, like this: `lift n to ℕ using h with n rfl h`.
* More generally, this can lift an expression from `α` to `β` assuming that there is an instance
  of `CanLift α β`. In this case the proof obligation is specified by `CanLift.prf`.
* Given an instance `CanLift β γ`, it can also lift `α → β` to `α → γ`; more generally, given
  `β : Π a : α, Type _`, `γ : Π a : α, Type _`, and `[Π a : α, CanLift (β a) (γ a)]`, it
  automatically generates an instance `CanLift (Π a, β a) (Π a, γ a)`.

`lift` is in some sense dual to the `zify` tactic. `lift (z : ℤ) to ℕ` will change the type of an
integer `z` (in the supertype) to `ℕ` (the subtype), given a proof that `z ≥ 0`;
propositions concerning `z` will still be over `ℤ`. `zify` changes propositions about `ℕ` (the
subtype) to propositions about `ℤ` (the supertype), without changing the type of any variable.
-/
syntax (name := lift: ParserDescr
lift) "lift " term: Category
term " to " term: Category
term (" using " term: Category
term)?
  (" with " ident: Parser
ident (colGt: optParam String "checkColGt" → Parser
colGt ident: Parser
ident)? (colGt: optParam String "checkColGt" → Parser
colGt ident: Parser
ident)?)? : tactic: Category
tactic

/-- Generate instance for the `lift` tactic. -/
def Lift.getInst: Expr → Expr → MetaM (Expr × Expr × Expr)
Lift.getInst (old_tp: Expr
old_tp new_tp: Expr
new_tp : Expr: Type
Expr) : MetaM: Type → Type
MetaM (Expr: Type
Expr × Expr: Type
Expr × Expr: Type
Expr) := do
  let coe: ?m.2303
coe ← mkFreshExprMVar: Option Expr → optParam MetavarKind MetavarKind.natural → optParam Name Name.anonymous → MetaM Expr
mkFreshExprMVar (some: {α : Type ?u.2294} → α → Option α
some $ .forallE: Name → Expr → Expr → BinderInfo → Expr
.forallE `a: Name
`a new_tp: Expr
new_tp old_tp: Expr
old_tp .default: BinderInfo
.default)
  let p: ?m.2354
p ← mkFreshExprMVar: Option Expr → optParam MetavarKind MetavarKind.natural → optParam Name Name.anonymous → MetaM Expr
mkFreshExprMVar (some: {α : Type ?u.2346} → α → Option α
some $ .forallE: Name → Expr → Expr → BinderInfo → Expr
.forallE `a: Name
`a old_tp: Expr
old_tp (.sort: Level → Expr
.sort .zero: Level
.zero) .default: BinderInfo
.default)
  let inst_type: ?m.2417
inst_type ← mkAppM: Name → Array Expr → MetaM Expr
mkAppM ``CanLift: (α : Sort u_1) → (β : Sort u_2) → outParam (β → α) → outParam (α → Prop) → Type
CanLift #[old_tp: Expr
old_tp, new_tp: Expr
new_tp, coe: ?m.2303
coe, p: ?m.2354
p]
  let inst: ?m.2466
inst ← synthInstance: Expr → optParam (Option ℕ) none → MetaM Expr
synthInstance inst_type: ?m.2417
inst_type -- TODO: catch error
  return (← instantiateMVars p, ← instantiateMVars coe, ← instantiateMVars inst): ?m.2701 × ?m.2702
(← instantiateMVars: {m : Type → Type} → [inst : Monad m] → [inst : MonadMCtx m] → Expr → m Expr
instantiateMVars(← instantiateMVars p, ← instantiateMVars coe, ← instantiateMVars inst): ?m.2701 × ?m.2702
 p: ?m.2354
p(← instantiateMVars p, ← instantiateMVars coe, ← instantiateMVars inst): ?m.2701 × ?m.2702
, ← instantiateMVars: {m : Type → Type} → [inst : Monad m] → [inst : MonadMCtx m] → Expr → m Expr
instantiateMVars(← instantiateMVars p, ← instantiateMVars coe, ← instantiateMVars inst): ?m.2701 × ?m.2702
 coe: ?m.2303
coe(← instantiateMVars p, ← instantiateMVars coe, ← instantiateMVars inst): ?m.2701 × ?m.2702
, ← instantiateMVars: {m : Type → Type} → [inst : Monad m] → [inst : MonadMCtx m] → Expr → m Expr
instantiateMVars(← instantiateMVars p, ← instantiateMVars coe, ← instantiateMVars inst): ?m.2701 × ?m.2702
 inst: ?m.2466
inst(← instantiateMVars p, ← instantiateMVars coe, ← instantiateMVars inst): ?m.2701 × ?m.2702
)

/-- Main function for the `lift` tactic. -/
def Lift.main: TSyntax `term →
  TSyntax `term → Option (TSyntax `term) → Option (TSyntax `ident) → Option (TSyntax `ident) → Bool → TacticM Unit
Lift.main (e: TSyntax `term
e t: TSyntax `term
t : TSyntax: SyntaxNodeKinds → Type
TSyntax `term: Name
`term) (hUsing: Option (TSyntax `term)
hUsing : Option: Type ?u.3800 → Type ?u.3800
Option (TSyntax: SyntaxNodeKinds → Type
TSyntax `term: Name
`term))
    (newVarName: Option (TSyntax `ident)
newVarName newEqName: Option (TSyntax `ident)
newEqName : Option: Type ?u.3803 → Type ?u.3803
Option (TSyntax: SyntaxNodeKinds → Type
TSyntax `ident: Name
`ident)) (keepUsing: Bool
keepUsing : Bool: Type
Bool) : TacticM: Type → Type
TacticM Unit: Type
Unit :=
    withMainContext: {α : Type} → TacticM α → TacticM α
withMainContext do
  -- Are we using a new variable for the lifted var?
  let isNewVar: ?m.3938
isNewVar := !newVarName: Option (TSyntax `ident)
newVarName.isNone: {α : Type ?u.3939} → Option α → Bool
isNone
  -- Name of the new hypothesis containing the equality of the lifted variable with the old one
  -- rfl if none is given
  let newEqName: ?m.3946
newEqName := (newEqName: Option (TSyntax `ident)
newEqName.map: {α : Type ?u.3948} → {β : Type ?u.3947} → (α → β) → Option α → Option β
map Syntax.getId: Syntax → Name
Syntax.getId).getD: {α : Type ?u.4082} → Option α → α → α
getD `rfl: Name
`rfl
  -- Was a new hypothesis given?
  let isNewEq: ?m.4089
isNewEq := newEqName: ?m.3946
newEqName != `rfl: Name
`rfl
  let e: ?m.4256
e ← elabTerm: Syntax → Option Expr → optParam Bool false → TacticM Expr
elabTerm e: TSyntax `term
e none: {α : Type ?u.4244} → Option α
none
  let goal: ?m.4304
goal ← getMainGoal: TacticM MVarId
getMainGoal
  if !(← inferType (← instantiateMVars (← goal.getType))): ?m.4698
(← inferType: Expr → MetaM Expr
inferType(← inferType (← instantiateMVars (← goal.getType))): ?m.4698
 (← instantiateMVars (← goal.getType)): ?m.4644
(← instantiateMVars: {m : Type → Type} → [inst : Monad m] → [inst : MonadMCtx m] → Expr → m Expr
instantiateMVars(← instantiateMVars (← goal.getType)): ?m.4644
 (← goal.getType): ?m.4527
(← goal: ?m.4304
goal(← goal.getType): ?m.4527
.getType: MVarId → MetaM Expr
getType(← goal.getType): ?m.4527
)(← instantiateMVars (← goal.getType)): ?m.4644
)(← inferType (← instantiateMVars (← goal.getType))): ?m.4698
).isProp: Expr → Bool
isProp then throwError
    "lift tactic failed. Tactic is only applicable when the target is a proposition.": TacticM (?m.4705 y✝)
throwErrorthrowError
    "lift tactic failed. Tactic is only applicable when the target is a proposition.": TacticM (?m.4705 y✝)
    "lift tactic failed. Tactic is only applicable when the target is a proposition."
  if newVarName: Option (TSyntax `ident)
newVarName == none: {α : Type ?u.5353} → Option α
none ∧ !e: ?m.4256
e.isFVar: Expr → Bool
isFVar then throwError
    "lift tactic failed. When lifting an expression, a new variable name must be given": ?m.5559 ?m.5560
throwErrorthrowError
    "lift tactic failed. When lifting an expression, a new variable name must be given": ?m.5559 ?m.5560
    "lift tactic failed. When lifting an expression, a new variable name must be given"
  let (p: Expr
p, coe: Expr
coe, inst: Expr
inst) ← Lift.getInst: Expr → Expr → MetaM (Expr × Expr × Expr)
Lift.getInst (← inferType e): ?m.5813
(← inferType: Expr → MetaM Expr
inferType(← inferType e): ?m.5813
 e: ?m.4256
e(← inferType e): ?m.5813
) (← Term.elabType t): ?m.6024
(← Term.elabType: Syntax → TermElabM Expr
Term.elabType(← Term.elabType t): ?m.6024
 t: TSyntax `term
t(← Term.elabType t): ?m.6024
)
  let prf: ?m.6130
prf ← match hUsing: Option (TSyntax `term)
hUsing with
    | some: {α : Type ?u.3931} → α → Option α
some h: TSyntax `term
h => elabTermEnsuringType: Syntax → Option Expr → optParam Bool false → TacticM Expr
elabTermEnsuringTypeelabTermEnsuringType h (p.betaRev #[e]): TacticM (?m.6134 y✝)
 h: TSyntax `term
helabTermEnsuringType h (p.betaRev #[e]): TacticM (?m.6134 y✝)
 (p: Expr
pelabTermEnsuringType h (p.betaRev #[e]): TacticM (?m.6134 y✝)
.betaRev: Expr → Array Expr → optParam Bool false → optParam Bool false → Expr
betaRevelabTermEnsuringType h (p.betaRev #[e]): TacticM (?m.6134 y✝)
 #[e: ?m.4256
eelabTermEnsuringType h (p.betaRev #[e]): TacticM (?m.6134 y✝)
])
    | none: {α : Type ?u.6384} → Option α
none => mkFreshExprMVar: Option Expr → optParam MetavarKind MetavarKind.natural → optParam Name Name.anonymous → MetaM Expr
mkFreshExprMVarmkFreshExprMVar (some (p.betaRev #[e])): TacticM (?m.6134 y✝)
 (some: {α : Type ?u.6434} → α → Option α
somemkFreshExprMVar (some (p.betaRev #[e])): TacticM (?m.6134 y✝)
 (p: Expr
pmkFreshExprMVar (some (p.betaRev #[e])): TacticM (?m.6134 y✝)
.betaRev: Expr → Array Expr → optParam Bool false → optParam Bool false → Expr
betaRevmkFreshExprMVar (some (p.betaRev #[e])): TacticM (?m.6134 y✝)
 #[e: ?m.4256
emkFreshExprMVar (some (p.betaRev #[e])): TacticM (?m.6134 y✝)
]))
  let newVarName: ?m.6550
newVarName ←  match newVarName: Option (TSyntax `ident)
newVarName with
                 | some: {α : Type ?u.3925} → α → Option α
some v: TSyntax `ident
v => pure: {f : Type ?u.6610 → Type ?u.6609} → [self : Pure f] → {α : Type ?u.6610} → α → f α
purepure v.getId: TacticM (?m.6554 y✝)
 v: TSyntax `ident
vpure v.getId: TacticM (?m.6554 y✝)
.getId: Ident → Name
getId
                 | none: {α : Type ?u.6730} → Option α
none   => e: ?m.4256
ee.fvarId!.getUserName: TacticM (?m.6554 y✝)
.fvarId!: Expr → FVarId
fvarId!e.fvarId!.getUserName: TacticM (?m.6554 y✝)
.getUserName: FVarId → MetaM Name
getUserName
  let prfEx: ?m.7611
prfEx ← mkAppOptM: Name → Array (Option Expr) → MetaM Expr
mkAppOptM ``CanLift.prf: ∀ {α : Sort u_1} {β : Sort u_2} {coe : outParam (β → α)} {cond : outParam (α → Prop)} [self : CanLift α β coe cond]
  (x : α), cond x → ∃ y, coe y = x
CanLift.prf #[none: {α : Type ?u.7103} → Option α
none, none: {α : Type ?u.7108} → Option α
none, coe: Expr
coe, p: Expr
p, inst: Expr
inst, e: ?m.4256
e, prf: ?m.6130
prf]
  let prfEx: ?m.7733
prfEx ← instantiateMVars: {m : Type → Type} → [inst : Monad m] → [inst : MonadMCtx m] → Expr → m Expr
instantiateMVars prfEx: ?m.7611
prfEx
  let prfSyn: ?m.7862
prfSyn ← prfEx: ?m.7733
prfEx.toSyntax: Expr → TermElabM Term
toSyntax
  -- if we have a new variable, but no hypothesis name was provided, we temporarily use a dummy
  -- hypothesis name
  let newEqName: ?m.7865
newEqName ← if isNewVar: ?m.3938
isNewVar && !isNewEq: ?m.4089
isNewEq then withMainContext: {α : Type} → TacticM α → TacticM α
withMainContextwithMainContext <| getUnusedUserName `tmpVar: TacticM (?m.7869 y✝)
 <| getUnusedUserName: {m : Type → Type} → [inst : Monad m] → [inst : MonadLCtx m] → Name → m Name
getUnusedUserNamewithMainContext <| getUnusedUserName `tmpVar: TacticM (?m.7869 y✝)
 `tmpVar: Name
`tmpVar
               else pure: {f : Type ?u.8140 → Type ?u.8139} → [self : Pure f] → {α : Type ?u.8140} → α → f α
purepure newEqName: TacticM (?m.7869 y✝)
 newEqName: ?m.3946
newEqName
  let newEqIdent: ?m.8248
newEqIdent := mkIdent: Name → Ident
mkIdent newEqName: ?m.7865
newEqName
  -- Run rcases on the proof of the lift condition
  replaceMainGoal: List MVarId → TacticM Unit
replaceMainGoal (← Std.Tactic.RCases.rcases #[(none, prfSyn)]
    (.tuple Syntax.missing <| [newVarName, newEqName].map (.one Syntax.missing)) goal): ?m.8552
(← Std.Tactic.RCases.rcases: Array (Option Name × Syntax) → Std.Tactic.RCases.RCasesPatt → MVarId → TermElabM (List MVarId)
Std.Tactic.RCases.rcases(← Std.Tactic.RCases.rcases #[(none, prfSyn)]
    (.tuple Syntax.missing <| [newVarName, newEqName].map (.one Syntax.missing)) goal): ?m.8552
 #[(none: {α : Type ?u.8413} → Option α
none(← Std.Tactic.RCases.rcases #[(none, prfSyn)]
    (.tuple Syntax.missing <| [newVarName, newEqName].map (.one Syntax.missing)) goal): ?m.8552
, prfSyn: ?m.7862
prfSyn(← Std.Tactic.RCases.rcases #[(none, prfSyn)]
    (.tuple Syntax.missing <| [newVarName, newEqName].map (.one Syntax.missing)) goal): ?m.8552
)]
    (.tuple: Syntax → List Std.Tactic.RCases.RCasesPatt → Std.Tactic.RCases.RCasesPatt
.tuple(← Std.Tactic.RCases.rcases #[(none, prfSyn)]
    (.tuple Syntax.missing <| [newVarName, newEqName].map (.one Syntax.missing)) goal): ?m.8552
 Syntax.missing: Syntax
Syntax.missing(← Std.Tactic.RCases.rcases #[(none, prfSyn)]
    (.tuple Syntax.missing <| [newVarName, newEqName].map (.one Syntax.missing)) goal): ?m.8552
 <| [newVarName: ?m.6550
newVarName(← Std.Tactic.RCases.rcases #[(none, prfSyn)]
    (.tuple Syntax.missing <| [newVarName, newEqName].map (.one Syntax.missing)) goal): ?m.8552
, newEqName: ?m.7865
newEqName(← Std.Tactic.RCases.rcases #[(none, prfSyn)]
    (.tuple Syntax.missing <| [newVarName, newEqName].map (.one Syntax.missing)) goal): ?m.8552
].map: {α : Type ?u.8519} → {β : Type ?u.8518} → (α → β) → List α → List β
map(← Std.Tactic.RCases.rcases #[(none, prfSyn)]
    (.tuple Syntax.missing <| [newVarName, newEqName].map (.one Syntax.missing)) goal): ?m.8552
 (.one: Syntax → Name → Std.Tactic.RCases.RCasesPatt
.one(← Std.Tactic.RCases.rcases #[(none, prfSyn)]
    (.tuple Syntax.missing <| [newVarName, newEqName].map (.one Syntax.missing)) goal): ?m.8552
 Syntax.missing: Syntax
Syntax.missing(← Std.Tactic.RCases.rcases #[(none, prfSyn)]
    (.tuple Syntax.missing <| [newVarName, newEqName].map (.one Syntax.missing)) goal): ?m.8552
)) goal: ?m.4304
goal(← Std.Tactic.RCases.rcases #[(none, prfSyn)]
    (.tuple Syntax.missing <| [newVarName, newEqName].map (.one Syntax.missing)) goal): ?m.8552
)
  -- if we use a new variable, then substitute it everywhere
  if isNewVar: ?m.3938
isNewVar then
    for decl: ?m.8815
decl in ←getLCtx: {m : Type → Type} → [self : MonadLCtx m] → m LocalContext
getLCtx do
      if decl: ?m.8815
decl.userName: LocalDecl → Name
userName != newEqName: ?m.7865
newEqName then
        let declIdent: ?m.8892
declIdent := mkIdent: Name → Ident
mkIdent decl: ?m.8815
decl.userName: LocalDecl → Name
userName
        -- The line below fails if $declIdent is there only once.
        evalTactic: Syntax → TacticM Unit
evalTactic (← `(tactic| simp only [← $newEqIdent] at $declIdent $declIdent)): ?m.10095
(← `(tactic| (← `(tactic| simp only [← $newEqIdent] at $declIdent $declIdent)): ?m.10095
simp(← `(tactic| simp only [← $newEqIdent] at $declIdent $declIdent)): ?m.10095
 (← `(tactic| simp only [← $newEqIdent] at $declIdent $declIdent)): ?m.10095
only(← `(tactic| simp only [← $newEqIdent] at $declIdent $declIdent)): ?m.10095
 [← $newEqIdent: ?m.8248
newEqIdent(← `(tactic| simp only [← $newEqIdent] at $declIdent $declIdent)): ?m.10095
] (← `(tactic| simp only [← $newEqIdent] at $declIdent $declIdent)): ?m.10095
at(← `(tactic| simp only [← $newEqIdent] at $declIdent $declIdent)): ?m.10095
 $declIdent: ?m.8892
declIdent(← `(tactic| simp only [← $newEqIdent] at $declIdent $declIdent)): ?m.10095
 $declIdent: ?m.8892
declIdent(← `(tactic| simp only [← $newEqIdent] at $declIdent $declIdent)): ?m.10095
))
    evalTactic: Syntax → TacticM Unit
evalTacticevalTactic (← `(tactic| simp only [← $newEqIdent])): TacticM (?m.8616 y✝)
 (← `(tactic| simp only [← $newEqIdent])): ?m.10753
(← `(tactic| (← `(tactic| simp only [← $newEqIdent])): ?m.10753
simp(← `(tactic| simp only [← $newEqIdent])): ?m.10753
 (← `(tactic| simp only [← $newEqIdent])): ?m.10753
only(← `(tactic| simp only [← $newEqIdent])): ?m.10753
 [← $newEqIdent: ?m.8248
newEqIdent(← `(tactic| simp only [← $newEqIdent])): ?m.10753
]))
  -- Clear the temporary hypothesis used for the new variable name if applicable
  if isNewVar: ?m.3938
isNewVar && !isNewEq: ?m.4089
isNewEq then
    evalTactic: Syntax → TacticM Unit
evalTacticevalTactic (← `(tactic| clear $newEqIdent)): TacticM (?m.11067 y✝)
 (← `(tactic| clear $newEqIdent)): ?m.11333
(← `(tactic| (← `(tactic| clear $newEqIdent)): ?m.11333
clear(← `(tactic| clear $newEqIdent)): ?m.11333
 $newEqIdent: ?m.8248
newEqIdent(← `(tactic| clear $newEqIdent)): ?m.11333
))
  -- Clear the "using" hypothesis if it's a variable in the context
  if prf: ?m.6130
prf.isFVar: Expr → Bool
isFVar && !keepUsing: Bool
keepUsing then
    let some: {α : Type ?u.11697} → α → Option α
some hUsingStx: TSyntax `term
hUsingStx := hUsing: Option (TSyntax `term)
hUsing | throwError "lift tactic failed: unreachable code was reached": ?m.12599 ?m.12600
throwErrorthrowError "lift tactic failed: unreachable code was reached": ?m.12599 ?m.12600
 "lift tactic failed: unreachable code was reached"
    evalTactic: Syntax → TacticM Unit
evalTactic (← `(tactic| clear $hUsingStx)): ?m.11965
(← `(tactic| (← `(tactic| clear $hUsingStx)): ?m.11965
clear(← `(tactic| clear $hUsingStx)): ?m.11965
 $hUsingStx: TSyntax `term
hUsingStx(← `(tactic| clear $hUsingStx)): ?m.11965
))
    evalTactic: Syntax → TacticM Unit
evalTacticevalTactic (← `(tactic| try clear $hUsingStx)): TacticM (?m.11625 y✝)
 (← `(tactic| try clear $hUsingStx)): ?m.12360
(← `(tactic| (← `(tactic| try clear $hUsingStx)): ?m.12360
try(← `(tactic| try clear $hUsingStx)): ?m.12360
 (← `(tactic| try clear $hUsingStx)): ?m.12360
clear(← `(tactic| try clear $hUsingStx)): ?m.12360
 $hUsingStx: TSyntax `term
hUsingStx(← `(tactic| try clear $hUsingStx)): ?m.12360
))
  if hUsing: Option (TSyntax `term)
hUsing.isNone: {α : Type ?u.13176} → Option α → Bool
isNone then withMainContext: {α : Type} → TacticM α → TacticM α
withMainContext <| setGoals: List MVarId → TacticM Unit
setGoals (prf: ?m.6130
prf.mvarId!: Expr → MVarId
mvarId! :: (← getGoals): ?m.13318
(← getGoals: TacticM (List MVarId)
getGoals(← getGoals): ?m.13318
))

elab_rules : tactic
  | `(tactic| lift $e: ?m.46038
e to $t: ?m.46031
t $[using $h: ?m.45742
h]?) => withMainContext: {α : Type} → TacticM α → TacticM α
withMainContext <| Lift.main: TSyntax `term →
  TSyntax `term → Option (TSyntax `term) → Option (TSyntax `ident) → Option (TSyntax `ident) → Bool → TacticM Unit
Lift.main e: ?m.46038
e t: ?m.46031
t h: ?m.45609 x✝
h none: {α : Type ?u.46064} → Option α
none none: {α : Type ?u.46066} → Option α
none False: Prop
False

elab_rules : tactic | `(tactic| lift $e: ?m.47927
e to $t: ?m.47920
t $[using $h: ?m.47584
h]?
    with $newVarName: ?m.47913
newVarName) => withMainContext: {α : Type} → TacticM α → TacticM α
withMainContext <| Lift.main: TSyntax `term →
  TSyntax `term → Option (TSyntax `term) → Option (TSyntax `ident) → Option (TSyntax `ident) → Bool → TacticM Unit
Lift.main e: ?m.47927
e t: ?m.47920
t h: ?m.47451 x✝
h newVarName: ?m.47913
newVarName none: {α : Type ?u.48012} → Option α
none False: Prop
False

elab_rules : tactic | `(tactic| lift $e: ?m.50376
e to $t: ?m.50369
t $[using $h: ?m.49883
h]?
    with $newVarName: ?m.50362
newVarName $newEqName: ?m.50355
newEqName) => withMainContext: {α : Type} → TacticM α → TacticM α
withMainContext <| Lift.main: TSyntax `term →
  TSyntax `term → Option (TSyntax `term) → Option (TSyntax `ident) → Option (TSyntax `ident) → Bool → TacticM Unit
Lift.main e: ?m.50376
e t: ?m.50369
t h: ?m.49887 x✝
h newVarName: ?m.50362
newVarName newEqName: ?m.50355
newEqName False: Prop
False

elab_rules : tactic | `(tactic| lift $e: ?m.52936
e to $t: ?m.52929
t $[using $h: ?m.52567
h]?
    with $newVarName: ?m.52922
newVarName $newEqName: ?m.52915
newEqName $newPrfName: ?m.52908
newPrfName) => withMainContext: {α : Type} → TacticM α → TacticM α
withMainContext do
  if h: ?m.52434 x✝
h.isNone: {α : Type ?u.52975} → Option α → Bool
isNone then Lift.main: TSyntax `term →
  TSyntax `term → Option (TSyntax `term) → Option (TSyntax `ident) → Option (TSyntax `ident) → Bool → TacticM Unit
Lift.main e: ?m.52936
e t: ?m.52929
t h: ?m.52434 x✝
h newVarName: ?m.52922
newVarName newEqName: ?m.52915
newEqName False: Prop
False
  else
    let some: {α : Type ?u.52972} → α → Option α
some h: TSyntax `term
h := h: ?m.52434 x✝
h | unreachable!: ?m.53579
unreachable!
    if h: TSyntax `term
h.raw: {ks : SyntaxNodeKinds} → TSyntax ks → Syntax
raw == newPrfName: ?m.52908
newPrfName then Lift.main: TSyntax `term →
  TSyntax `term → Option (TSyntax `term) → Option (TSyntax `ident) → Option (TSyntax `ident) → Bool → TacticM Unit
Lift.main e: ?m.52936
e t: ?m.52929
t h: TSyntax `term
h newVarName: ?m.52922
newVarName newEqName: ?m.52915
newEqName True: Prop
True
    else Lift.main: TSyntax `term →
  TSyntax `term → Option (TSyntax `term) → Option (TSyntax `ident) → Option (TSyntax `ident) → Bool → TacticM Unit
Lift.main e: ?m.52936
e t: ?m.52929
t h: TSyntax `term
h newVarName: ?m.52922
newVarName newEqName: ?m.52915
newEqName False: Prop
False

end Mathlib.Tactic