Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+πŸ–±οΈto focus. On Mac, use Cmdinstead of Ctrl.
/-
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
Sort
Sort _: 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 :
β„•: Type
β„•
↦ 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
Sort
Sort _: Type ?u.282
_
) (
Ξ±: ΞΉ β†’ Sort ?u.287
Ξ±
Ξ²: ΞΉ β†’ Sort ?u.292
Ξ²
:
ΞΉ: Sort ?u.282
ΞΉ
β†’
Sort _: Type ?u.287
Sort
Sort _: 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
Sort
Sort _: Type ?u.757
_
} {
Ξ±: ΞΉ β†’ Sort u_2
Ξ±
:
ΞΉ: Sort ?u.757
ΞΉ
β†’
Sort _: Type ?u.762
Sort
Sort _: 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
:=

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) = f
ΞΉ: 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) = f

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
Sort
Sort _: Type ?u.1159
_
) (
Ξ±: ΞΉ β†’ Sort ?u.1164
Ξ±
:
ΞΉ: Sort ?u.1159
ΞΉ
β†’
Sort _: Type ?u.1164
Sort
Sort _: 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
Sort
Sort _: Type ?u.1632
_
) (
Ξ±: Sort ?u.1635
Ξ±
:
Sort _: Type ?u.1635
Sort
Sort _: 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
Sort
Sort _: 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) "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 (
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 (
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✝)
throwError
throwError "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
throwError
throwError "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
elabTermEnsuringType
elabTermEnsuringType h (p.betaRev #[e]): TacticM (?m.6134 y✝)
h: TSyntax `term
h
elabTermEnsuringType h (p.betaRev #[e]): TacticM (?m.6134 y✝)
(
p: Expr
p
elabTermEnsuringType h (p.betaRev #[e]): TacticM (?m.6134 y✝)
.
betaRev: Expr β†’ Array Expr β†’ optParam Bool false β†’ optParam Bool false β†’ Expr
betaRev
elabTermEnsuringType h (p.betaRev #[e]): TacticM (?m.6134 y✝)
#[
e: ?m.4256
e
elabTermEnsuringType h (p.betaRev #[e]): TacticM (?m.6134 y✝)
])
|
none: {Ξ± : Type ?u.6384} β†’ Option Ξ±
none
=> mkFreshExprMVar
mkFreshExprMVar (some (p.betaRev #[e])): TacticM (?m.6134 y✝)
(
some: {Ξ± : Type ?u.6434} β†’ Ξ± β†’ Option Ξ±
some
mkFreshExprMVar (some (p.betaRev #[e])): TacticM (?m.6134 y✝)
(
p: Expr
p
mkFreshExprMVar (some (p.betaRev #[e])): TacticM (?m.6134 y✝)
.
betaRev: Expr β†’ Array Expr β†’ optParam Bool false β†’ optParam Bool false β†’ Expr
betaRev
mkFreshExprMVar (some (p.betaRev #[e])): TacticM (?m.6134 y✝)
#[
e: ?m.4256
e
mkFreshExprMVar (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 Ξ±
pure
pure v.getId: TacticM (?m.6554 y✝)
v: TSyntax `ident
v
pure v.getId: TacticM (?m.6554 y✝)
.
getId: Ident β†’ Name
getId
|
none: {Ξ± : Type ?u.6730} β†’ Option Ξ±
none
=>
e: ?m.4256
e
e.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 Ξ±
withMainContext
withMainContext <| getUnusedUserName `tmpVar: TacticM (?m.7869 y✝)
<|
getUnusedUserName: {m : Type β†’ Type} β†’ [inst : Monad m] β†’ [inst : MonadLCtx m] β†’ Name β†’ m Name
getUnusedUserName
withMainContext <| 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 Ξ±
pure
pure 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
(← 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
(← 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
evalTactic
evalTactic (← `(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
evalTactic
evalTactic (← `(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
throwError
throwError "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
evalTactic
evalTactic (← `(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