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) 2018 Johannes HΓΆlzl. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Johannes HΓΆlzl, Floris van Doorn, Mario Carneiro, Reid Barton, Johan Commelin
-/

import Mathlib.Util.Tactic
import Mathlib.Logic.Function.Basic

/-!
# `choose` tactic
Performs Skolemization, that is, given `h : βˆ€ a:Ξ±, βˆƒ b:Ξ², p a b |- G` produces
`f : Ξ± β†’ Ξ², hf: βˆ€ a, p a (f a) |- G`.

TODO: switch to `rcases` syntax: `choose ⟨i, j, h₁ -⟩ := expr`.
-/

open Lean Meta Elab Tactic

namespace Mathlib.Tactic.Choose

/-- Given `Ξ± : Sort u`, `nonemp : Nonempty Ξ±`, `p : Ξ± β†’ Prop`, a context of free variables
`ctx`, and a pair of an element `val : Ξ±` and `spec : p val`,
`mk_sometimes u Ξ± nonemp p ctx (val, spec)` produces another pair `val', spec'`
such that `val'` does not have any free variables from elements of `ctx` whose types are
propositions. This is done by applying `Function.sometimes` to abstract over all the propositional
arguments. -/
def 
mk_sometimes: Level β†’ Expr β†’ Expr β†’ Expr β†’ List Expr β†’ Expr Γ— Expr β†’ MetaM (Expr Γ— Expr)
mk_sometimes (
u: Level
u : 
Level: Type
Level) (
Ξ±: Expr
Ξ± 
nonemp: Expr
nonemp 
p: Expr
p : 
Expr: Type
Expr) :
  
List: Type ?u.11 β†’ Type ?u.11
List 
Expr: Type
Expr β†’ 
Expr: Type
Expr Γ— 
Expr: Type
Expr β†’ 
MetaM: Type β†’ Type
MetaM (
Expr: Type
Expr Γ— 
Expr: Type
Expr)
| [], (
val: Expr
val, 
spec: Expr
spec) => 
pure: {f : Type ?u.73 β†’ Type ?u.72} β†’ [self : Pure f] β†’ {Ξ± : Type ?u.73} β†’ Ξ± β†’ f Ξ±
pure (
val: Expr
val, 
spec: Expr
spec)
| (
e: Expr
e :: 
ctx: List Expr
ctx), (
val: Expr
val, 
spec: Expr
spec) => do
  let (
val: Expr
val, 
spec: Expr
spec) ← 
mk_sometimes: Level β†’ Expr β†’ Expr β†’ Expr β†’ List Expr β†’ Expr Γ— Expr β†’ MetaM (Expr Γ— Expr)
mk_sometimes 
u: Level
u 
Ξ±: Expr
Ξ± 
nonemp: Expr
nonemp 
p: Expr
p 
ctx: List Expr
ctx (
val: Expr
val, 
spec: Expr
spec)
  let 
t: ?m.339
t ← 
inferType: Expr β†’ MetaM Expr
inferType 
e: Expr
e
  let 
b: ?m.388
b ← 
isProp: Expr β†’ MetaM Bool
isProp 
t: ?m.339
t
  if 
b: ?m.388
b then do
    let 
val': ?m.536
val' ← 
mkLambdaFVars: Array Expr β†’ Expr β†’ optParam Bool false β†’ optParam Bool true β†’ optParam BinderInfo BinderInfo.implicit β†’ MetaM Expr
mkLambdaFVars #[
e: Expr
e] 
val: Expr
val
    
pure: {f : Type ?u.539 β†’ Type ?u.538} β†’ [self : Pure f] β†’ {Ξ± : Type ?u.539} β†’ Ξ± β†’ f Ξ±
pure
      (
mkApp4: Expr β†’ Expr β†’ Expr β†’ Expr β†’ Expr β†’ Expr
mkApp4 (
Expr.const: Name β†’ List Level β†’ Expr
Expr.const ``
Function.sometimes: {Ξ± : Sort u_1} β†’ {Ξ² : Sort u_2} β†’ [inst : Nonempty Ξ²] β†’ (Ξ± β†’ Ξ²) β†’ Ξ²
Function.sometimes [
Level.zero: Level
Level.zero, 
u: Level
u]) 
t: ?m.339
t 
Ξ±: Expr
Ξ± 
nonemp: Expr
nonemp 
val': ?m.536
val',
      
mkApp7: Expr β†’ Expr β†’ Expr β†’ Expr β†’ Expr β†’ Expr β†’ Expr β†’ Expr β†’ Expr
mkApp7 (
Expr.const: Name β†’ List Level β†’ Expr
Expr.const ``
Function.sometimes_spec: βˆ€ {p : Prop} {Ξ± : Sort u_1} [inst : Nonempty Ξ±] (P : Ξ± β†’ Prop) (f : p β†’ Ξ±) (a : p), P (f a) β†’ P (Function.sometimes f)
Function.sometimes_spec [
u: Level
u]) 
t: ?m.339
t 
Ξ±: Expr
Ξ± 
nonemp: Expr
nonemp 
p: Expr
p 
val': ?m.536
val' 
e: Expr
e 
spec: Expr
spec)
  else 
pure: {f : Type ?u.592 β†’ Type ?u.591} β†’ [self : Pure f] β†’ {Ξ± : Type ?u.592} β†’ Ξ± β†’ f Ξ±
pure (
val: Expr
val, 
spec: Expr
spec)

/-- Results of searching for nonempty instances,
to eliminate dependencies on propositions (`choose!`).
`success` means we found at least one instance;
`failure ts` means we didn't find instances for any `t ∈ ts`.
(`failure []` means we didn't look for instances at all.)

Rationale:
`choose!` means we are expected to succeed at least once
in eliminating dependencies on propositions.
-/
inductive 
ElimStatus: Sort ?u.2533
ElimStatus
| 
success: ElimStatus
success
| 
failure: List Expr β†’ ElimStatus
failure (
ts: List Expr
ts : 
List: Type ?u.2536 β†’ Type ?u.2536
List 
Expr: Type
Expr)

/-- Combine two statuses, keeping a success from either side
or merging the failures. -/
def 
ElimStatus.merge: ElimStatus β†’ ElimStatus β†’ ElimStatus
ElimStatus.merge : 
ElimStatus: Type
ElimStatus β†’ 
ElimStatus: Type
ElimStatus β†’ 
ElimStatus: Type
ElimStatus
| 
success: ElimStatus
success, _ => 
success: ElimStatus
success
| _, 
success: ElimStatus
success => 
success: ElimStatus
success
| 
failure: List Expr β†’ ElimStatus
failure 
ts₁: List Expr
ts₁, 
failure: List Expr β†’ ElimStatus
failure 
tsβ‚‚: List Expr
tsβ‚‚ => 
failure: List Expr β†’ ElimStatus
failure (
ts₁: List Expr
ts₁ ++ 
tsβ‚‚: List Expr
tsβ‚‚)

/-- `mkFreshNameFrom orig base` returns `mkFreshUserName base` if ``orig = `_``
and `orig` otherwise. -/
def 
mkFreshNameFrom: Name β†’ Name β†’ CoreM Name
mkFreshNameFrom (
orig: Name
orig 
base: Name
base : 
Name: Type
Name) : 
CoreM: Type β†’ Type
CoreM 
Name: Type
Name :=
  if 
orig: Name
orig = 
`_: Name
`_ then 
mkFreshUserName: Name β†’ CoreM Name
mkFreshUserName 
base: Name
base else 
pure: {f : Type ?u.3144 β†’ Type ?u.3143} β†’ [self : Pure f] β†’ {Ξ± : Type ?u.3144} β†’ Ξ± β†’ f Ξ±
pure 
orig: Name
orig

/-- Changes `(h : βˆ€xs, βˆƒa:Ξ±, p a) ⊒ g` to `(d : βˆ€xs, a) ⊒ (s : βˆ€xs, p (d xs)) β†’ g` and
`(h : βˆ€xs, p xs ∧ q xs) ⊒ g` to `(d : βˆ€xs, p xs) ⊒ (s : βˆ€xs, q xs) β†’ g`.
`choose1` returns a tuple of

- the error result (see `ElimStatus`)
- the data new free variable that was "chosen"
- the new goal (which contains the spec of the data as domain of an arrow type)

If `nondep` is true and `Ξ±` is inhabited, then it will remove the dependency of `d` on
all propositional assumptions in `xs`. For example if `ys` are propositions then
`(h : βˆ€xs ys, βˆƒa:Ξ±, p a) ⊒ g` becomes `(d : βˆ€xs, a) (s : βˆ€xs ys, p (d xs)) ⊒ g`. -/
def 
choose1: MVarId β†’ Bool β†’ Option Expr β†’ Name β†’ MetaM (ElimStatus Γ— Expr Γ— MVarId)
choose1 (
g: MVarId
g : 
MVarId: Type
MVarId) (
nondep: Bool
nondep : 
Bool: Type
Bool) (
h: Option Expr
h : 
Option: Type ?u.3406 β†’ Type ?u.3406
Option 
Expr: Type
Expr) (
data: Name
data : 
Name: Type
Name) :
  
MetaM: Type β†’ Type
MetaM (
ElimStatus: Type
ElimStatus Γ— 
Expr: Type
Expr Γ— 
MVarId: Type
MVarId) := do
  let (
g: MVarId
g, 
h: Expr
h) ← match 
h: Option Expr
h with
  | 
some: {Ξ± : Type ?u.3449} β†’ Ξ± β†’ Option Ξ±
some 
e: Expr
e => 
pure: {f : Type ?u.3522 β†’ Type ?u.3521} β†’ [self : Pure f] β†’ {Ξ± : Type ?u.3522} β†’ Ξ± β†’ f Ξ±
pure
pure (g, e): MetaM (?m.3466 y✝)
 (
g: MVarId
g
pure (g, e): MetaM (?m.3466 y✝)
, 
e: Expr
e
pure (g, e): MetaM (?m.3466 y✝)
)
  | 
none: {Ξ± : Type ?u.3617} β†’ Option Ξ±
none   => do
    let (
e: FVarId
e, 
g: MVarId
g) ← 
g: MVarId
g.
intro1P: MVarId β†’ MetaM (FVarId Γ— MVarId)
intro1P
    
pure: {f : Type ?u.3736 β†’ Type ?u.3735} β†’ [self : Pure f] β†’ {Ξ± : Type ?u.3736} β†’ Ξ± β†’ f Ξ±
pure
pure (g, .fvar e): MetaM (?m.3466 y✝)
 (
g: MVarId
g
pure (g, .fvar e): MetaM (?m.3466 y✝)
, 
.fvar: FVarId β†’ Expr
.fvar
pure (g, .fvar e): MetaM (?m.3466 y✝)
 
e: FVarId
e
pure (g, .fvar e): MetaM (?m.3466 y✝)
)
  
g: MVarId
g.
withContext: {n : Type β†’ Type ?u.3961} β†’ [inst : MonadControlT MetaM n] β†’ [inst : Monad n] β†’ {Ξ± : Type} β†’ MVarId β†’ n Ξ± β†’ n Ξ±
withContext do
    let 
h: ?m.4099
h ← 
instantiateMVars: {m : Type β†’ Type} β†’ [inst : Monad m] β†’ [inst : MonadMCtx m] β†’ Expr β†’ m Expr
instantiateMVars 
h: Expr
h
    let 
t: ?m.4148
t ← 
inferType: Expr β†’ MetaM Expr
inferType 
h: ?m.4099
h
    
forallTelescopeReducing: {n : Type β†’ Type ?u.4150} β†’
  [inst : MonadControlT MetaM n] β†’ [inst : Monad n] β†’ {Ξ± : Type} β†’ Expr β†’ (Array Expr β†’ Expr β†’ n Ξ±) β†’ n Ξ±
forallTelescopeReducing 
t: ?m.4148
t fun 
ctx: ?m.4191
ctx 
t: ?m.4194
t ↦ do
      
(← withTransparency .all (whnf t)): ?m.4349
(← 
withTransparency: {n : Type β†’ Type ?u.4237} β†’
  [inst : MonadControlT MetaM n] β†’ [inst : Monad n] β†’ {Ξ± : Type} β†’ TransparencyMode β†’ n Ξ± β†’ n Ξ±
withTransparency
(← withTransparency .all (whnf t)): ?m.4349
 
.all: TransparencyMode
.all
(← withTransparency .all (whnf t)): ?m.4349
 (
whnf: Expr β†’ MetaM Expr
whnf
(← withTransparency .all (whnf t)): ?m.4349
 
t: ?m.4194
t
(← withTransparency .all (whnf t)): ?m.4349
)).
withApp: {Ξ± : Sort ?u.4351} β†’ Expr β†’ (Expr β†’ Array Expr β†’ Ξ±) β†’ Ξ±
withApp fun
      | 
.const: Name β†’ List Level β†’ Expr
.const 
``Exists: Name
``
Exists: {Ξ± : Sort u} β†’ (Ξ± β†’ Prop) β†’ Prop
Exists [
u: Level
u], #[
Ξ±: Expr
Ξ±, 
p: Expr
p] => do
        let 
data: ?m.4656
data ← 
mkFreshNameFrom: Name β†’ Name β†’ CoreM Name
mkFreshNameFrom 
data: Name
data (
(← p.getBinderName): ?m.4501
(← 
p: Expr
p
(← p.getBinderName): ?m.4501
.
getBinderName: Expr β†’ MetaM (Option Name)
getBinderName
(← p.getBinderName): ?m.4501
).
getD: {Ξ± : Type ?u.4551} β†’ Option Ξ± β†’ Ξ± β†’ Ξ±
getD 
`h: Name
`h)
        let ((
neFail: ElimStatus
neFail : ElimStatus), (
nonemp: Option Expr
nonemp : Option Expr)) ← if 
nondep: Bool
nondep then
          let 
ne: ?m.4760
ne := (
Expr.const: Name β†’ List Level β†’ Expr
Expr.const ``
Nonempty: Sort u β†’ Prop
Nonempty [
u: Level
u]).
app: Expr β†’ Expr β†’ Expr
app 
Ξ±: Expr
Ξ±
          let 
m: ?m.4874
m ← 
mkFreshExprMVar: Option Expr β†’ optParam MetavarKind MetavarKind.natural β†’ optParam Name Name.anonymous β†’ MetaM Expr
mkFreshExprMVar 
ne: ?m.4760
ne
          let mut 
g': ?m.5629
g' := 
m: ?m.4874
m.
mvarId!: Expr β†’ MVarId
mvarId!
          for 
e: ?m.4965
e in 
ctx: ?m.4191
ctx do
            if 
(← isProof e): ?m.5020
(← 
isProof: Expr β†’ MetaM Bool
isProof
(← isProof e): ?m.5020
 
e: ?m.4965
e
(← isProof e): ?m.5020
) then continue
            let 
ty: ?m.5383
ty ← 
whnf: Expr β†’ MetaM Expr
whnf 
(← inferType e): ?m.5334
(← 
inferType: Expr β†’ MetaM Expr
inferType
(← inferType e): ?m.5334
 
e: ?m.4965
e
(← inferType e): ?m.5334
)
            let 
nety: ?m.5386
nety := (
Expr.const: Name β†’ List Level β†’ Expr
Expr.const ``
Nonempty: Sort u β†’ Prop
Nonempty [
u: Level
u]).
app: Expr β†’ Expr β†’ Expr
app 
ty: ?m.5383
ty
            let 
neval: ?m.5395
neval := 
mkApp2: Expr β†’ Expr β†’ Expr β†’ Expr
mkApp2 (
Expr.const: Name β†’ List Level β†’ Expr
Expr.const ``
Nonempty.intro: βˆ€ {Ξ± : Sort u}, Ξ± β†’ Nonempty Ξ±
Nonempty.intro [
u: Level
u]) 
ty: ?m.5383
ty 
e: ?m.4965
e
            
g': ?m.4971
g' ← 
g': MVarId
g'.
assert: MVarId β†’ Name β†’ Expr β†’ Expr β†’ MetaM MVarId
assert 
.anonymous: Name
.anonymous 
nety: ?m.5386
nety 
neval: ?m.5395
neval
          (
_: ?m.5683
_, 
g': MVarId
g') ← 
g': ?m.5629
g'.
intros: MVarId β†’ MetaM (Array FVarId Γ— MVarId)
intros
          
g': MVarId
g'
g'.withContext do
            match ← synthInstance? (← g'.getType) with
            | some e => do
              g'.assign e
              let m ← instantiateMVars m
              pure (.success, some m)
            | none => pure (.failure [ne], none): MetaM (?m.4663 y✝)
.
withContext: {n : Type β†’ Type ?u.5750} β†’ [inst : MonadControlT MetaM n] β†’ [inst : Monad n] β†’ {Ξ± : Type} β†’ MVarId β†’ n Ξ± β†’ n Ξ±
withContext
g'.withContext do
            match ← synthInstance? (← g'.getType) with
            | some e => do
              g'.assign e
              let m ← instantiateMVars m
              pure (.success, some m)
            | none => pure (.failure [ne], none): MetaM (?m.4663 y✝)
 
g'.withContext do
            match ← synthInstance? (← g'.getType) with
            | some e => do
              g'.assign e
              let m ← instantiateMVars m
              pure (.success, some m)
            | none => pure (.failure [ne], none): MetaM (?m.4663 y✝)
do
g'.withContext do
            match ← synthInstance? (← g'.getType) with
            | some e => do
              g'.assign e
              let m ← instantiateMVars m
              pure (.success, some m)
            | none => pure (.failure [ne], none): MetaM (?m.4663 y✝)

            
g'.withContext do
            match ← synthInstance? (← g'.getType) with
            | some e => do
              g'.assign e
              let m ← instantiateMVars m
              pure (.success, some m)
            | none => pure (.failure [ne], none): MetaM (?m.4663 y✝)
match
g'.withContext do
            match ← synthInstance? (← g'.getType) with
            | some e => do
              g'.assign e
              let m ← instantiateMVars m
              pure (.success, some m)
            | none => pure (.failure [ne], none): MetaM (?m.4663 y✝)
 ← 
synthInstance?: Expr β†’ optParam (Option β„•) none β†’ MetaM (Option Expr)
synthInstance?
g'.withContext do
            match ← synthInstance? (← g'.getType) with
            | some e => do
              g'.assign e
              let m ← instantiateMVars m
              pure (.success, some m)
            | none => pure (.failure [ne], none): MetaM (?m.4663 y✝)
 
(← g'.getType): ?m.5855
(← 
g': MVarId
g'
(← g'.getType): ?m.5855
.
getType: MVarId β†’ MetaM Expr
getType
(← g'.getType): ?m.5855
)
g'.withContext do
            match ← synthInstance? (← g'.getType) with
            | some e => do
              g'.assign e
              let m ← instantiateMVars m
              pure (.success, some m)
            | none => pure (.failure [ne], none): MetaM (?m.4663 y✝)
 
g'.withContext do
            match ← synthInstance? (← g'.getType) with
            | some e => do
              g'.assign e
              let m ← instantiateMVars m
              pure (.success, some m)
            | none => pure (.failure [ne], none): MetaM (?m.4663 y✝)
with
g'.withContext do
            match ← synthInstance? (← g'.getType) with
            | some e => do
              g'.assign e
              let m ← instantiateMVars m
              pure (.success, some m)
            | none => pure (.failure [ne], none): MetaM (?m.4663 y✝)

            | 
some: {Ξ± : Type ?u.5906} β†’ Ξ± β†’ Option Ξ±
some
g'.withContext do
            match ← synthInstance? (← g'.getType) with
            | some e => do
              g'.assign e
              let m ← instantiateMVars m
              pure (.success, some m)
            | none => pure (.failure [ne], none): MetaM (?m.4663 y✝)
 
e: Expr
e
g'.withContext do
            match ← synthInstance? (← g'.getType) with
            | some e => do
              g'.assign e
              let m ← instantiateMVars m
              pure (.success, some m)
            | none => pure (.failure [ne], none): MetaM (?m.4663 y✝)
 => 
g'.withContext do
            match ← synthInstance? (← g'.getType) with
            | some e => do
              g'.assign e
              let m ← instantiateMVars m
              pure (.success, some m)
            | none => pure (.failure [ne], none): MetaM (?m.4663 y✝)
do
g'.withContext do
            match ← synthInstance? (← g'.getType) with
            | some e => do
              g'.assign e
              let m ← instantiateMVars m
              pure (.success, some m)
            | none => pure (.failure [ne], none): MetaM (?m.4663 y✝)

              
g': MVarId
g'
g'.withContext do
            match ← synthInstance? (← g'.getType) with
            | some e => do
              g'.assign e
              let m ← instantiateMVars m
              pure (.success, some m)
            | none => pure (.failure [ne], none): MetaM (?m.4663 y✝)
.
assign: {m : Type β†’ Type} β†’ [inst : MonadMCtx m] β†’ MVarId β†’ Expr β†’ m Unit
assign
g'.withContext do
            match ← synthInstance? (← g'.getType) with
            | some e => do
              g'.assign e
              let m ← instantiateMVars m
              pure (.success, some m)
            | none => pure (.failure [ne], none): MetaM (?m.4663 y✝)
 
e: Expr
e
g'.withContext do
            match ← synthInstance? (← g'.getType) with
            | some e => do
              g'.assign e
              let m ← instantiateMVars m
              pure (.success, some m)
            | none => pure (.failure [ne], none): MetaM (?m.4663 y✝)

              
g'.withContext do
            match ← synthInstance? (← g'.getType) with
            | some e => do
              g'.assign e
              let m ← instantiateMVars m
              pure (.success, some m)
            | none => pure (.failure [ne], none): MetaM (?m.4663 y✝)
let
g'.withContext do
            match ← synthInstance? (← g'.getType) with
            | some e => do
              g'.assign e
              let m ← instantiateMVars m
              pure (.success, some m)
            | none => pure (.failure [ne], none): MetaM (?m.4663 y✝)
 
m: ?m.6035
m
g'.withContext do
            match ← synthInstance? (← g'.getType) with
            | some e => do
              g'.assign e
              let m ← instantiateMVars m
              pure (.success, some m)
            | none => pure (.failure [ne], none): MetaM (?m.4663 y✝)
 ← 
instantiateMVars: {m : Type β†’ Type} β†’ [inst : Monad m] β†’ [inst : MonadMCtx m] β†’ Expr β†’ m Expr
instantiateMVars
g'.withContext do
            match ← synthInstance? (← g'.getType) with
            | some e => do
              g'.assign e
              let m ← instantiateMVars m
              pure (.success, some m)
            | none => pure (.failure [ne], none): MetaM (?m.4663 y✝)
 
m: ?m.4874
m
g'.withContext do
            match ← synthInstance? (← g'.getType) with
            | some e => do
              g'.assign e
              let m ← instantiateMVars m
              pure (.success, some m)
            | none => pure (.failure [ne], none): MetaM (?m.4663 y✝)

              
pure: {f : Type ?u.6038 β†’ Type ?u.6037} β†’ [self : Pure f] β†’ {Ξ± : Type ?u.6038} β†’ Ξ± β†’ f Ξ±
pure
g'.withContext do
            match ← synthInstance? (← g'.getType) with
            | some e => do
              g'.assign e
              let m ← instantiateMVars m
              pure (.success, some m)
            | none => pure (.failure [ne], none): MetaM (?m.4663 y✝)
 (
.success: ElimStatus
.success
g'.withContext do
            match ← synthInstance? (← g'.getType) with
            | some e => do
              g'.assign e
              let m ← instantiateMVars m
              pure (.success, some m)
            | none => pure (.failure [ne], none): MetaM (?m.4663 y✝)
, 
some: {Ξ± : Type ?u.6069} β†’ Ξ± β†’ Option Ξ±
some
g'.withContext do
            match ← synthInstance? (← g'.getType) with
            | some e => do
              g'.assign e
              let m ← instantiateMVars m
              pure (.success, some m)
            | none => pure (.failure [ne], none): MetaM (?m.4663 y✝)
 
m: ?m.6035
m
g'.withContext do
            match ← synthInstance? (← g'.getType) with
            | some e => do
              g'.assign e
              let m ← instantiateMVars m
              pure (.success, some m)
            | none => pure (.failure [ne], none): MetaM (?m.4663 y✝)
)
            | 
none: {Ξ± : Type ?u.6095} β†’ Option Ξ±
none
g'.withContext do
            match ← synthInstance? (← g'.getType) with
            | some e => do
              g'.assign e
              let m ← instantiateMVars m
              pure (.success, some m)
            | none => pure (.failure [ne], none): MetaM (?m.4663 y✝)
 => 
pure: {f : Type ?u.6104 β†’ Type ?u.6103} β†’ [self : Pure f] β†’ {Ξ± : Type ?u.6104} β†’ Ξ± β†’ f Ξ±
pure
g'.withContext do
            match ← synthInstance? (← g'.getType) with
            | some e => do
              g'.assign e
              let m ← instantiateMVars m
              pure (.success, some m)
            | none => pure (.failure [ne], none): MetaM (?m.4663 y✝)
 (
.failure: List Expr β†’ ElimStatus
.failure
g'.withContext do
            match ← synthInstance? (← g'.getType) with
            | some e => do
              g'.assign e
              let m ← instantiateMVars m
              pure (.success, some m)
            | none => pure (.failure [ne], none): MetaM (?m.4663 y✝)
 [
ne: ?m.4760
ne
g'.withContext do
            match ← synthInstance? (← g'.getType) with
            | some e => do
              g'.assign e
              let m ← instantiateMVars m
              pure (.success, some m)
            | none => pure (.failure [ne], none): MetaM (?m.4663 y✝)
], 
none: {Ξ± : Type ?u.6134} β†’ Option Ξ±
none
g'.withContext do
            match ← synthInstance? (← g'.getType) with
            | some e => do
              g'.assign e
              let m ← instantiateMVars m
              pure (.success, some m)
            | none => pure (.failure [ne], none): MetaM (?m.4663 y✝)
)
        else 
pure: {f : Type ?u.6383 β†’ Type ?u.6382} β†’ [self : Pure f] β†’ {Ξ± : Type ?u.6383} β†’ Ξ± β†’ f Ξ±
pure
pure (.failure [], none): MetaM (?m.4663 y✝)
 (
.failure: List Expr β†’ ElimStatus
.failure
pure (.failure [], none): MetaM (?m.4663 y✝)
 
[]: List ?m.7148
[]
pure (.failure [], none): MetaM (?m.4663 y✝)
, 
none: {Ξ± : Type ?u.6412} β†’ Option Ξ±
none
pure (.failure [], none): MetaM (?m.4663 y✝)
)
        let 
ctx': ?m.6522
ctx' ← if 
nonemp: Option Expr
nonemp.
isSome: {Ξ± : Type ?u.6530} β†’ Option Ξ± β†’ Bool
isSome then 
ctx: ?m.4191
ctx
ctx.filterM (not <$> isProof ·): MetaM (?m.6526 y✝)
.
filterM: {m : Type β†’ Type ?u.6662} β†’
  {Ξ± : Type} β†’
    [inst : Monad m] β†’ (Ξ± β†’ m Bool) β†’ (as : Array Ξ±) β†’ optParam β„• 0 β†’ optParam β„• (Array.size as) β†’ m (Array Ξ±)
filterM
ctx.filterM (not <$> isProof ·): MetaM (?m.6526 y✝)
 (
not: Bool β†’ Bool
not
ctx.filterM (not <$> isProof ·): MetaM (?m.6526 y✝)
 <$> 
isProof: Expr β†’ MetaM Bool
isProof
ctx.filterM (not <$> isProof ·): MetaM (?m.6526 y✝)
 Β·) else 
pure: {f : Type ?u.6816 β†’ Type ?u.6815} β†’ [self : Pure f] β†’ {Ξ± : Type ?u.6816} β†’ Ξ± β†’ f Ξ±
pure
pure ctx: MetaM (?m.6526 y✝)
 
ctx: ?m.4191
ctx
        let 
dataTy: ?m.6918
dataTy ← 
mkForallFVars: Array Expr β†’ Expr β†’ optParam Bool false β†’ optParam Bool true β†’ optParam BinderInfo BinderInfo.implicit β†’ MetaM Expr
mkForallFVars 
ctx': ?m.6522
ctx' 
Ξ±: Expr
Ξ±
        let mut 
dataVal: ?m.6921
dataVal := 
mkApp3: Expr β†’ Expr β†’ Expr β†’ Expr β†’ Expr
mkApp3 (
.const: Name β†’ List Level β†’ Expr
.const ``
Classical.choose: {Ξ± : Sort u} β†’ {p : Ξ± β†’ Prop} β†’ (βˆƒ x, p x) β†’ Ξ±
Classical.choose [
u: Level
u]) 
Ξ±: Expr
Ξ± 
p: Expr
p (
mkAppN: Expr β†’ Array Expr β†’ Expr
mkAppN 
h: ?m.4099
h 
ctx: ?m.4191
ctx)
        let mut 
specVal: ?m.6929
specVal := 
mkApp3: Expr β†’ Expr β†’ Expr β†’ Expr β†’ Expr
mkApp3 (
.const: Name β†’ List Level β†’ Expr
.const ``
Classical.choose_spec: βˆ€ {Ξ± : Sort u} {p : Ξ± β†’ Prop} (h : βˆƒ x, p x), p (Classical.choose h)
Classical.choose_spec [
u: Level
u]) 
Ξ±: Expr
Ξ± 
p: Expr
p (
mkAppN: Expr β†’ Array Expr β†’ Expr
mkAppN 
h: ?m.4099
h 
ctx: ?m.4191
ctx)
        if let 
some: {Ξ± : Type ?u.6951} β†’ Ξ± β†’ Option Ξ±
some 
nonemp: Expr
nonemp := 
nonemp: Option Expr
nonemp then
          (
dataVal: ?m.6921
dataVal, 
specVal: Expr
specVal) ← 
mk_sometimes: Level β†’ Expr β†’ Expr β†’ Expr β†’ List Expr β†’ Expr Γ— Expr β†’ MetaM (Expr Γ— Expr)
mk_sometimes 
u: Level
u 
Ξ±: Expr
Ξ± 
nonemp: Expr
nonemp 
p: Expr
p 
ctx: ?m.4191
ctx.
toList: {Ξ± : Type ?u.7006} β†’ Array Ξ± β†’ List Ξ±
toList (
dataVal: ?m.6921
dataVal, 
specVal: ?m.6929
specVal)
        
dataVal: ?m.7415
dataVal ← 
mkLambdaFVars: Array Expr β†’ Expr β†’ optParam Bool false β†’ optParam Bool true β†’ optParam BinderInfo BinderInfo.implicit β†’ MetaM Expr
mkLambdaFVars 
ctx': ?m.6522
ctx' 
dataVal: Expr
dataVal
        
specVal: ?m.7467
specVal ← 
mkLambdaFVars: Array Expr β†’ Expr β†’ optParam Bool false β†’ optParam Bool true β†’ optParam BinderInfo BinderInfo.implicit β†’ MetaM Expr
mkLambdaFVars 
ctx: ?m.4191
ctx 
specVal: Expr
specVal
        let (
fvar: Expr
fvar, 
g: MVarId
g) ← 
withLocalDeclD: {n : Type β†’ Type ?u.7505} β†’
  [inst : MonadControlT MetaM n] β†’ [inst : Monad n] β†’ {Ξ± : Type} β†’ Name β†’ Expr β†’ (Expr β†’ n Ξ±) β†’ n Ξ±
withLocalDeclD 
.anonymous: Name
.anonymous 
dataTy: ?m.6918
dataTy fun 
d: ?m.7546
d ↦ do
          let 
specTy: ?m.7617
specTy ← 
mkForallFVars: Array Expr β†’ Expr β†’ optParam Bool false β†’ optParam Bool true β†’ optParam BinderInfo BinderInfo.implicit β†’ MetaM Expr
mkForallFVars 
ctx: ?m.4191
ctx (
p: Expr
p.
app: Expr β†’ Expr β†’ Expr
app (
mkAppN: Expr β†’ Array Expr β†’ Expr
mkAppN 
d: ?m.7546
d 
ctx': ?m.6522
ctx')).
headBeta: Expr β†’ Expr
headBeta
          
g: MVarId
g.
withContext: {n : Type β†’ Type ?u.7619} β†’ [inst : MonadControlT MetaM n] β†’ [inst : Monad n] β†’ {Ξ± : Type} β†’ MVarId β†’ n Ξ± β†’ n Ξ±
withContext <| 
withLocalDeclD: {n : Type β†’ Type ?u.7665} β†’
  [inst : MonadControlT MetaM n] β†’ [inst : Monad n] β†’ {Ξ± : Type} β†’ Name β†’ Expr β†’ (Expr β†’ n Ξ±) β†’ n Ξ±
withLocalDeclD 
data: ?m.4656
data 
dataTy: ?m.6918
dataTy fun 
d': ?m.7706
d' ↦ do
            let 
mvarTy: ?m.7920
mvarTy ← 
mkArrow: Expr β†’ Expr β†’ CoreM Expr
mkArrow (
specTy: ?m.7617
specTy.
replaceFVar: Expr β†’ Expr β†’ Expr β†’ Expr
replaceFVar 
d: ?m.7546
d 
d': ?m.7706
d') 
(← g.getType): ?m.7761
(← 
g: MVarId
g
(← g.getType): ?m.7761
.
getType: MVarId β†’ MetaM Expr
getType
(← g.getType): ?m.7761
)
            let 
newMVar: ?m.8019
newMVar ← 
mkFreshExprSyntheticOpaqueMVar: Expr β†’ optParam Name Name.anonymous β†’ MetaM Expr
mkFreshExprSyntheticOpaqueMVar 
mvarTy: ?m.7920
mvarTy 
(← g.getTag): ?m.7970
(← 
g: MVarId
g
(← g.getTag): ?m.7970
.
getTag: MVarId β†’ MetaM Name
getTag
(← g.getTag): ?m.7970
)
            
g: MVarId
g.
assign: {m : Type β†’ Type} β†’ [inst : MonadMCtx m] β†’ MVarId β†’ Expr β†’ m Unit
assign <| 
mkApp2: Expr β†’ Expr β†’ Expr β†’ Expr
mkApp2 
(← mkLambdaFVars #[d'] newMVar): ?m.8076
(← 
mkLambdaFVars: Array Expr β†’ Expr β†’ optParam Bool false β†’ optParam Bool true β†’ optParam BinderInfo BinderInfo.implicit β†’ MetaM Expr
mkLambdaFVars
(← mkLambdaFVars #[d'] newMVar): ?m.8076
 #[
d': ?m.7706
d'
(← mkLambdaFVars #[d'] newMVar): ?m.8076
] 
newMVar: ?m.8019
newMVar
(← mkLambdaFVars #[d'] newMVar): ?m.8076
) 
dataVal: ?m.7415
dataVal 
specVal: ?m.7467
specVal
            
pure: {f : Type ?u.8135 β†’ Type ?u.8134} β†’ [self : Pure f] β†’ {Ξ± : Type ?u.8135} β†’ Ξ± β†’ f Ξ±
pure (
d': ?m.7706
d', 
newMVar: ?m.8019
newMVar.
mvarId!: Expr β†’ MVarId
mvarId!)
        let 
g: ?m.8345
g ← match 
h: ?m.4099
h with
        | 
.fvar: FVarId β†’ Expr
.fvar 
v: FVarId
v => 
g: MVarId
g
g.clear v: MetaM (?m.8349 y✝)
.
clear: MVarId β†’ FVarId β†’ MetaM MVarId
clear
g.clear v: MetaM (?m.8349 y✝)
 
v: FVarId
v
        | _ => 
pure: {f : Type ?u.8476 β†’ Type ?u.8475} β†’ [self : Pure f] β†’ {Ξ± : Type ?u.8476} β†’ Ξ± β†’ f Ξ±
pure
pure g: MetaM (?m.8349 y✝)
 
g: MVarId
g
        return (
neFail: ElimStatus
neFail, 
fvar: Expr
fvar, 
g: ?m.8345
g)
      | 
.const: Name β†’ List Level β†’ Expr
.const 
``And: Name
``
And: Prop β†’ Prop β†’ Prop
And _, #[
p: Expr
p, 
q: Expr
q] => do
        let 
data: ?m.9308
data ← 
mkFreshNameFrom: Name β†’ Name β†’ CoreM Name
mkFreshNameFrom 
data: Name
data 
`h: Name
`h
        let 
e1: ?m.9360
e1 ← 
mkLambdaFVars: Array Expr β†’ Expr β†’ optParam Bool false β†’ optParam Bool true β†’ optParam BinderInfo BinderInfo.implicit β†’ MetaM Expr
mkLambdaFVars 
ctx: ?m.4191
ctx $ 
mkApp3: Expr β†’ Expr β†’ Expr β†’ Expr β†’ Expr
mkApp3 (
.const: Name β†’ List Level β†’ Expr
.const ``
And.left: βˆ€ {a b : Prop}, a ∧ b β†’ a
And.left  
[]: List ?m.9353
[]) 
p: Expr
p 
q: Expr
q (
mkAppN: Expr β†’ Array Expr β†’ Expr
mkAppN 
h: ?m.4099
h 
ctx: ?m.4191
ctx)
        let 
e2: ?m.9411
e2 ← 
mkLambdaFVars: Array Expr β†’ Expr β†’ optParam Bool false β†’ optParam Bool true β†’ optParam BinderInfo BinderInfo.implicit β†’ MetaM Expr
mkLambdaFVars 
ctx: ?m.4191
ctx $ 
mkApp3: Expr β†’ Expr β†’ Expr β†’ Expr β†’ Expr
mkApp3 (
.const: Name β†’ List Level β†’ Expr
.const ``
And.right: βˆ€ {a b : Prop}, a ∧ b β†’ b
And.right 
[]: List ?m.9404
[]) 
p: Expr
p 
q: Expr
q (
mkAppN: Expr β†’ Array Expr β†’ Expr
mkAppN 
h: ?m.4099
h 
ctx: ?m.4191
ctx)
        let 
t1: ?m.9460
t1 ← 
inferType: Expr β†’ MetaM Expr
inferType 
e1: ?m.9360
e1
        let 
t2: ?m.9509
t2 ← 
inferType: Expr β†’ MetaM Expr
inferType 
e2: ?m.9411
e2
        let (
fvar: FVarId
fvar, 
g: MVarId
g) ← 
(← (← g.assert .anonymous t2 e2).assert data t1 e1): ?m.9625
(← 
(← g.assert .anonymous t2 e2): ?m.9567
(← 
g: MVarId
g
(← g.assert .anonymous t2 e2): ?m.9567
.
assert: MVarId β†’ Name β†’ Expr β†’ Expr β†’ MetaM MVarId
assert
(← g.assert .anonymous t2 e2): ?m.9567
 
.anonymous: Name
.anonymous
(← g.assert .anonymous t2 e2): ?m.9567
 
t2: ?m.9509
t2
(← g.assert .anonymous t2 e2): ?m.9567
 
e2: ?m.9411
e2
(← g.assert .anonymous t2 e2): ?m.9567
)
(← (← g.assert .anonymous t2 e2).assert data t1 e1): ?m.9625
.
assert: MVarId β†’ Name β†’ Expr β†’ Expr β†’ MetaM MVarId
assert
(← (← g.assert .anonymous t2 e2).assert data t1 e1): ?m.9625
 
data: ?m.9308
data
(← (← g.assert .anonymous t2 e2).assert data t1 e1): ?m.9625
 
t1: ?m.9460
t1
(← (← g.assert .anonymous t2 e2).assert data t1 e1): ?m.9625
 
e1: ?m.9360
e1
(← (← g.assert .anonymous t2 e2).assert data t1 e1): ?m.9625
).
intro1P: MVarId β†’ MetaM (FVarId Γ— MVarId)
intro1P
        let 
g: ?m.9704
g ← match 
h: ?m.4099
h with
        | 
.fvar: FVarId β†’ Expr
.fvar 
v: FVarId
v => 
g: MVarId
g
g.clear v: MetaM (?m.9708 y✝)
.
clear: MVarId β†’ FVarId β†’ MetaM MVarId
clear
g.clear v: MetaM (?m.9708 y✝)
 
v: FVarId
v
        | _ => 
pure: {f : Type ?u.9835 β†’ Type ?u.9834} β†’ [self : Pure f] β†’ {Ξ± : Type ?u.9835} β†’ Ξ± β†’ f Ξ±
pure
pure g: MetaM (?m.9708 y✝)
 
g: MVarId
g
        return (
.success: ElimStatus
.success, 
.fvar: FVarId β†’ Expr
.fvar 
fvar: FVarId
fvar, 
g: ?m.9704
g)
      -- TODO: support Ξ£, Γ—, or even any inductive type with 1 constructor ?
      | _, _ => 
throwError "expected a term of the shape `βˆ€xs, βˆƒa, p xs a` or `βˆ€xs, p xs ∧ q xs`": ?m.10310 ?m.10311
throwError
throwError "expected a term of the shape `βˆ€xs, βˆƒa, p xs a` or `βˆ€xs, p xs ∧ q xs`": ?m.10310 ?m.10311
 "expected a term of the shape `βˆ€xs, βˆƒa, p xs a` or `βˆ€xs, p xs ∧ q xs`"

/-- A wrapper around `choose1` that parses identifiers and adds variable info to new variables. -/
def 
choose1WithInfo: MVarId β†’ Bool β†’ Option Expr β†’ TSyntax `Lean.binderIdent β†’ TermElabM (ElimStatus Γ— MVarId)
choose1WithInfo (
g: MVarId
g : 
MVarId: Type
MVarId) (
nondep: Bool
nondep : 
Bool: Type
Bool) (
h: Option Expr
h : 
Option: Type ?u.31895 β†’ Type ?u.31895
Option 
Expr: Type
Expr) (
data: TSyntax `Lean.binderIdent
data : 
TSyntax: SyntaxNodeKinds β†’ Type
TSyntax ``
binderIdent: ParserDescr
binderIdent) :
  
TermElabM: Type β†’ Type
TermElabM (
ElimStatus: Type
ElimStatus Γ— 
MVarId: Type
MVarId) := do
  let 
n: ?m.32024
n := if let `(
binderIdent: ParserDescr
binderIdent| $
n: ?m.32136
n:ident) := 
data: TSyntax `Lean.binderIdent
data then 
n: ?m.32136
n.
getId: Ident β†’ Name
getId else 
`_: Name
`_
  let (
status: ElimStatus
status, 
fvar: Expr
fvar, 
g: MVarId
g) ← 
choose1: MVarId β†’ Bool β†’ Option Expr β†’ Name β†’ MetaM (ElimStatus Γ— Expr Γ— MVarId)
choose1 
g: MVarId
g 
nondep: Bool
nondep 
h: Option Expr
h 
n: ?m.32024
n
  
g: MVarId
g.
withContext: {n : Type β†’ Type ?u.32426} β†’ [inst : MonadControlT MetaM n] β†’ [inst : Monad n] β†’ {Ξ± : Type} β†’ MVarId β†’ n Ξ± β†’ n Ξ±
withContext <| 
fvar: Expr
fvar.
addLocalVarInfoForBinderIdent: Expr β†’ TSyntax `Lean.binderIdent β†’ TermElabM Unit
addLocalVarInfoForBinderIdent 
data: TSyntax `Lean.binderIdent
data
  
pure: {f : Type ?u.32634 β†’ Type ?u.32633} β†’ [self : Pure f] β†’ {Ξ± : Type ?u.32634} β†’ Ξ± β†’ f Ξ±
pure (
status: ElimStatus
status, 
g: MVarId
g)

/-- A loop around `choose1`. The main entry point for the `choose` tactic. -/
def 
elabChoose: Bool β†’ Option Expr β†’ List (TSyntax `Lean.binderIdent) β†’ ElimStatus β†’ MVarId β†’ TermElabM MVarId
elabChoose (
nondep: Bool
nondep : 
Bool: Type
Bool) (
h: Option Expr
h : 
Option: Type ?u.33849 β†’ Type ?u.33849
Option 
Expr: Type
Expr) :
  
List: Type ?u.33853 β†’ Type ?u.33853
List (
TSyntax: SyntaxNodeKinds β†’ Type
TSyntax ``
binderIdent: ParserDescr
binderIdent) β†’ 
ElimStatus: Type
ElimStatus β†’ 
MVarId: Type
MVarId β†’ 
TermElabM: Type β†’ Type
TermElabM 
MVarId: Type
MVarId
| [], _, _ => 
throwError "expect list of variables": ?m.33981 ?m.33982
throwError
throwError "expect list of variables": ?m.33981 ?m.33982
 "expect list of variables"
| [
n: TSyntax `Lean.binderIdent
n], 
status: ElimStatus
status, 
g: MVarId
g =>
  match 
nondep: Bool
nondep, 
status: ElimStatus
status with
  | 
true: Bool
true, 
.failure: List Expr β†’ ElimStatus
.failure 
tys: List Expr
tys => do -- We expected some elimination, but it didn't happen.
    let mut 
msg: ?m.34331
msg := 
m!"choose!: failed to synthesize any nonempty instances": MessageData
m!
m!"choose!: failed to synthesize any nonempty instances": MessageData
"choose!: failed to synthesize any nonempty instances"
    for 
ty: ?m.34428
ty in 
tys: List Expr
tys do
      
msg: ?m.34434
msg := 
msg: ?m.34434
msg ++ m!"{
(← mkFreshExprMVar ty): ?m.34633
(← 
mkFreshExprMVar: Option Expr β†’ optParam MetavarKind MetavarKind.natural β†’ optParam Name Name.anonymous β†’ MetaM Expr
mkFreshExprMVar
(← mkFreshExprMVar ty): ?m.34633
 
ty: ?m.34428
ty
(← mkFreshExprMVar ty): ?m.34633
).
mvarId!: Expr β†’ MVarId
mvarId!}"
    throwError 
msg: ?m.34907
msg
  | _, _ => do
    let (
fvar: FVarId
fvar, 
g: MVarId
g) ← match 
n: TSyntax `Lean.binderIdent
n with
    | `(
binderIdent: ParserDescr
binderIdent| $
n: ?m.35121
n:ident) => 
g: MVarId
g
g.intro n.getId: TermElabM (?m.35008 y✝)
.
intro: MVarId β†’ Name β†’ MetaM (FVarId Γ— MVarId)
intro
g.intro n.getId: TermElabM (?m.35008 y✝)
 
n: ?m.35121
n
g.intro n.getId: TermElabM (?m.35008 y✝)
.
getId: Ident β†’ Name
getId
    | _ => 
g: MVarId
g
g.intro1: TermElabM (?m.35008 y✝)
.
intro1: MVarId β†’ MetaM (FVarId Γ— MVarId)
intro1
    
g: MVarId
g.
withContext: {n : Type β†’ Type ?u.35466} β†’ [inst : MonadControlT MetaM n] β†’ [inst : Monad n] β†’ {Ξ± : Type} β†’ MVarId β†’ n Ξ± β†’ n Ξ±
withContext <| (
Expr.fvar: FVarId β†’ Expr
Expr.fvar 
fvar: FVarId
fvar).
addLocalVarInfoForBinderIdent: Expr β†’ TSyntax `Lean.binderIdent β†’ TermElabM Unit
addLocalVarInfoForBinderIdent 
n: TSyntax `Lean.binderIdent
n
    return 
g: MVarId
g
| 
n: TSyntax `Lean.binderIdent
n::
ns: List (TSyntax `Lean.binderIdent)
ns, 
status: ElimStatus
status, 
g: MVarId
g => do
  let (
status': ElimStatus
status', 
g: MVarId
g) ← 
choose1WithInfo: MVarId β†’ Bool β†’ Option Expr β†’ TSyntax `Lean.binderIdent β†’ TermElabM (ElimStatus Γ— MVarId)
choose1WithInfo 
g: MVarId
g 
nondep: Bool
nondep 
h: Option Expr
h 
n: TSyntax `Lean.binderIdent
n
  
elabChoose: Bool β†’ Option Expr β†’ List (TSyntax `Lean.binderIdent) β†’ ElimStatus β†’ MVarId β†’ TermElabM MVarId
elabChoose 
nondep: Bool
nondep 
none: {Ξ± : Type ?u.36024} β†’ Option Ξ±
none 
ns: List (TSyntax `Lean.binderIdent)
ns (
status: ElimStatus
status.
merge: ElimStatus β†’ ElimStatus β†’ ElimStatus
merge 
status': ElimStatus
status') 
g: MVarId
g

/--
* `choose a b h h' using hyp` takes a hypothesis `hyp` of the form
  `βˆ€ (x : X) (y : Y), βˆƒ (a : A) (b : B), P x y a b ∧ Q x y a b`
  for some `P Q : X β†’ Y β†’ A β†’ B β†’ Prop` and outputs
  into context a function `a : X β†’ Y β†’ A`, `b : X β†’ Y β†’ B` and two assumptions:
  `h : βˆ€ (x : X) (y : Y), P x y (a x y) (b x y)` and
  `h' : βˆ€ (x : X) (y : Y), Q x y (a x y) (b x y)`. It also works with dependent versions.

* `choose! a b h h' using hyp` does the same, except that it will remove dependency of
  the functions on propositional arguments if possible. For example if `Y` is a proposition
  and `A` and `B` are nonempty in the above example then we will instead get
  `a : X β†’ A`, `b : X β†’ B`, and the assumptions
  `h : βˆ€ (x : X) (y : Y), P x y (a x) (b x)` and
  `h' : βˆ€ (x : X) (y : Y), Q x y (a x) (b x)`.

The `using hyp` part can be ommited,
which will effectively cause `choose` to start with an `intro hyp`.

Examples:

```
example (h : βˆ€ n m : β„•, βˆƒ i j, m = n + i ∨ m + j = n) : True := by
  choose i j h using h
  guard_hyp i : β„• β†’ β„• β†’ β„•
  guard_hyp j : β„• β†’ β„• β†’ β„•
  guard_hyp h : βˆ€ (n m : β„•), m = n + i n m ∨ m + j n m = n
  trivial
```

```
example (h : βˆ€ i : β„•, i < 7 β†’ βˆƒ j, i < j ∧ j < i+i) : True := by
  choose! f h h' using h
  guard_hyp f : β„• β†’ β„•
  guard_hyp h : βˆ€ (i : β„•), i < 7 β†’ i < f i
  guard_hyp h' : βˆ€ (i : β„•), i < 7 β†’ f i < i + i
  trivial
```
-/
syntax (name := 
choose: ParserDescr
choose) "choose" "!"? (
colGt: optParam String "checkColGt" β†’ Parser.Parser
colGt 
binderIdent: ParserDescr
binderIdent)+ (" using " 
term: Parser.Category
term)? : 
tactic: Parser.Category
tactic
elab_rules : tactic
| `(tactic| choose $[!%$
b: ?m.40295
b]? $[$
ids: Array (TSyntax `Lean.binderIdent)
ids]* $[using $
h: ?m.40782 x✝
h]?) => 
withMainContext: {Ξ± : Type} β†’ TacticM Ξ± β†’ TacticM Ξ±
withMainContext do
  let 
h: ?m.41274
h ← 
h: ?m.40782 x✝
h.
mapM: {m : Type ?u.41082 β†’ Type ?u.41081} β†’
  {Ξ± : Type ?u.41080} β†’ {Ξ² : Type ?u.41082} β†’ [inst : Monad m] β†’ (Ξ± β†’ m Ξ²) β†’ Option Ξ± β†’ m (Option Ξ²)
mapM (
Elab.Tactic.elabTerm: Syntax β†’ Option Expr β†’ optParam Bool false β†’ TacticM Expr
Elab.Tactic.elabTerm Β· 
none: {Ξ± : Type ?u.41126} β†’ Option Ξ±
none)
  let 
g: ?m.41517
g ← 
elabChoose: Bool β†’ Option Expr β†’ List (TSyntax `Lean.binderIdent) β†’ ElimStatus β†’ MVarId β†’ TermElabM MVarId
elabChoose 
b: ?m.40299 x✝¹
b.
isSome: {Ξ± : Type ?u.41372} β†’ Option Ξ± β†’ Bool
isSome 
h: ?m.41274
h 
ids: Array (TSyntax `Lean.binderIdent)
ids.
toList: {Ξ± : Type ?u.41392} β†’ Array Ξ± β†’ List Ξ±
toList (
.failure: List Expr β†’ ElimStatus
.failure 
[]: List ?m.41405
[]) 
(← getMainGoal): ?m.41322
(← 
getMainGoal: TacticM MVarId
getMainGoal
(← getMainGoal): ?m.41322
)
  
replaceMainGoal: List MVarId β†’ TacticM Unit
replaceMainGoal [
g: ?m.41517
g]

@[inherit_doc 
choose: ParserDescr
choose]
syntax "choose!" (
colGt: optParam String "checkColGt" β†’ Parser.Parser
colGt 
binderIdent: ParserDescr
binderIdent)+ (" using " 
term: Parser.Category
term)? : 
tactic: Parser.Category
tactic
macro_rules
  | `(tactic| choose! $[$
ids: Array (TSyntax `Lean.binderIdent)
ids]* $[using $
h: ?m.44936 x✝
h]?) => `(tactic| choose ! $[$
ids: ?m.45468
ids]* $[using $
h: ?m.44936 x✝
h]?)