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) 2022 Arthur Paulino. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Arthur Paulino, Edward Ayers, Mario Carneiro
-/
import Lean
import Mathlib.Data.Array.Defs

/--
Uses `checkColGt` to prevent

```lean
have h
exact Nat
```

From being interpreted as
```lean
have h
  exact Nat
```
-/
def 
Lean.Parser.Term.haveIdLhs': Parser
Lean.Parser.Term.haveIdLhs' : 
Parser: Type
Parser :=
  
optional: Parser โ†’ Parser
optional (
ppSpace: Parser
ppSpace >> 
ident: Parser
ident >> 
many: Parser โ†’ Parser
many (
ppSpace: Parser
ppSpace >>
    
checkColGt: optParam String "checkColGt" โ†’ Parser
checkColGt 
"expected to be indented": String
"expected to be indented" >>
    
letIdBinder: Parser
letIdBinder)) >> 
optType: Parser
optType

namespace Mathlib.Tactic

open Lean Elab.Tactic Meta

syntax "have" 
Parser.Term.haveIdLhs': Parser.Parser
Parser.Term.haveIdLhs' : 
tactic: Parser.Category
tactic
syntax "let " 
Parser.Term.haveIdLhs': Parser.Parser
Parser.Term.haveIdLhs' : 
tactic: Parser.Category
tactic
syntax "suffices" 
Parser.Term.haveIdLhs': Parser.Parser
Parser.Term.haveIdLhs' : 
tactic: Parser.Category
tactic

open Elab Term in
def 
haveLetCore: MVarId โ†’ Option Syntax โ†’ Array Syntax โ†’ Option Syntax โ†’ Bool โ†’ TermElabM (MVarId ร— MVarId)
haveLetCore (
goal: MVarId
goal : 
MVarId: Type
MVarId) (
name: Option Syntax
name : 
Option: Type ?u.558 โ†’ Type ?u.558
Option 
Syntax: Type
Syntax) (
bis: Array Syntax
bis : 
Array: Type ?u.561 โ†’ Type ?u.561
Array 
Syntax: Type
Syntax)
  (
t: Option Syntax
t : 
Option: Type ?u.564 โ†’ Type ?u.564
Option 
Syntax: Type
Syntax) (
keepTerm: Bool
keepTerm : 
Bool: Type
Bool) : 
TermElabM: Type โ†’ Type
TermElabM (
MVarId: Type
MVarId ร— 
MVarId: Type
MVarId) :=
  let 
declFn: ?m.583
declFn := if 
keepTerm: Bool
keepTerm then 
MVarId.define: MVarId โ†’ Name โ†’ Expr โ†’ Expr โ†’ MetaM MVarId
MVarId.define else 
MVarId.assert: MVarId โ†’ Name โ†’ Expr โ†’ Expr โ†’ MetaM MVarId
MVarId.assert
  
goal: MVarId
goal.
withContext: {n : Type โ†’ Type ?u.710} โ†’ [inst : MonadControlT MetaM n] โ†’ [inst : Monad n] โ†’ {ฮฑ : Type} โ†’ MVarId โ†’ n ฮฑ โ†’ n ฮฑ
withContext do
    let 
n: ?m.797
n := if let 
some: {ฮฑ : Type ?u.3065} โ†’ ฮฑ โ†’ Option ฮฑ
some 
n: Syntax
n := 
name: Option Syntax
name then 
n: Syntax
n.
getId: Syntax โ†’ Name
getId else 
`this: Name
`this
    let 
elabBinders: (Array Expr โ†’ TermElabM ?m.882) โ†’ TermElabM ?m.882
elabBinders 
k: ?m.801
k := if 
bis: Array Syntax
bis.
isEmpty: {ฮฑ : Type ?u.805} โ†’ Array ฮฑ โ†’ Bool
isEmpty then 
k: ?m.801
k 
#[]: Array ?m.1891
#[] else 
elabBinders: {ฮฑ : Type} โ†’ Array Syntax โ†’ (Array Expr โ†’ TermElabM ฮฑ) โ†’ TermElabM ฮฑ
elabBinders 
bis: Array Syntax
bis 
k: ?m.801
k
    let (
goal1: MVarId
goal1, 
t: Expr
t, 
p: Expr
p) โ† 
elabBinders: (Array Expr โ†’ TermElabM ?m.882) โ†’ TermElabM ?m.882
elabBinders fun 
es: ?m.948
es โ†ฆ do
      let 
t: ?m.962
t โ† match 
t: Option Syntax
t with
      | 
none: {ฮฑ : Type ?u.956} โ†’ Option ฮฑ
none => 
mkFreshTypeMVar: TermElabM (?m.966 yโœ)
mkFreshTypeMVar
      | 
some: {ฮฑ : Type ?u.1152} โ†’ ฮฑ โ†’ Option ฮฑ
some 
stx: Syntax
stx => 
withRef: {m : Type โ†’ Type} โ†’ [inst : Monad m] โ†’ [inst : MonadRef m] โ†’ {ฮฑ : Type} โ†’ Syntax โ†’ m ฮฑ โ†’ m ฮฑ
withRef
withRef stx do
          let e โ† Term.elabTerm stx none
          Term.synthesizeSyntheticMVars false
          instantiateMVars e: TermElabM (?m.966 yโœ)
 
stx: Syntax
stx
withRef stx do
          let e โ† Term.elabTerm stx none
          Term.synthesizeSyntheticMVars false
          instantiateMVars e: TermElabM (?m.966 yโœ)
 
withRef stx do
          let e โ† Term.elabTerm stx none
          Term.synthesizeSyntheticMVars false
          instantiateMVars e: TermElabM (?m.966 yโœ)
do
withRef stx do
          let e โ† Term.elabTerm stx none
          Term.synthesizeSyntheticMVars false
          instantiateMVars e: TermElabM (?m.966 yโœ)

          
withRef stx do
          let e โ† Term.elabTerm stx none
          Term.synthesizeSyntheticMVars false
          instantiateMVars e: TermElabM (?m.966 yโœ)
let
withRef stx do
          let e โ† Term.elabTerm stx none
          Term.synthesizeSyntheticMVars false
          instantiateMVars e: TermElabM (?m.966 yโœ)
 
e: ?m.1292
e
withRef stx do
          let e โ† Term.elabTerm stx none
          Term.synthesizeSyntheticMVars false
          instantiateMVars e: TermElabM (?m.966 yโœ)
 โ† 
Term.elabTerm: Syntax โ†’ Option Expr โ†’ optParam Bool true โ†’ optParam Bool true โ†’ TermElabM Expr
Term.elabTerm
withRef stx do
          let e โ† Term.elabTerm stx none
          Term.synthesizeSyntheticMVars false
          instantiateMVars e: TermElabM (?m.966 yโœ)
 
stx: Syntax
stx
withRef stx do
          let e โ† Term.elabTerm stx none
          Term.synthesizeSyntheticMVars false
          instantiateMVars e: TermElabM (?m.966 yโœ)
 
none: {ฮฑ : Type ?u.1282} โ†’ Option ฮฑ
none
withRef stx do
          let e โ† Term.elabTerm stx none
          Term.synthesizeSyntheticMVars false
          instantiateMVars e: TermElabM (?m.966 yโœ)

          
Term.synthesizeSyntheticMVars: optParam Bool true โ†’ optParam Bool false โ†’ TermElabM Unit
Term.synthesizeSyntheticMVars
withRef stx do
          let e โ† Term.elabTerm stx none
          Term.synthesizeSyntheticMVars false
          instantiateMVars e: TermElabM (?m.966 yโœ)
 
false: Bool
false
withRef stx do
          let e โ† Term.elabTerm stx none
          Term.synthesizeSyntheticMVars false
          instantiateMVars e: TermElabM (?m.966 yโœ)

          
instantiateMVars: {m : Type โ†’ Type} โ†’ [inst : Monad m] โ†’ [inst : MonadMCtx m] โ†’ Expr โ†’ m Expr
instantiateMVars
withRef stx do
          let e โ† Term.elabTerm stx none
          Term.synthesizeSyntheticMVars false
          instantiateMVars e: TermElabM (?m.966 yโœ)
 
e: ?m.1292
e
      let 
p: ?m.2213
p โ† 
mkFreshExprMVar: Option Expr โ†’ optParam MetavarKind MetavarKind.natural โ†’ optParam Name Name.anonymous โ†’ MetaM Expr
mkFreshExprMVar 
t: ?m.962
t 
MetavarKind.syntheticOpaque: MetavarKind
MetavarKind.syntheticOpaque 
n: ?m.797
n
      
pure: {f : Type ?u.2336 โ†’ Type ?u.2335} โ†’ [self : Pure f] โ†’ {ฮฑ : Type ?u.2336} โ†’ ฮฑ โ†’ f ฮฑ
pure (
p: ?m.2213
p.
mvarId!: Expr โ†’ MVarId
mvarId!, โ† 
mkForallFVars: Array Expr โ†’ Expr โ†’ optParam Bool false โ†’ optParam Bool true โ†’ optParam BinderInfo BinderInfo.implicit โ†’ MetaM Expr
mkForallFVars 
es: ?m.948
es 
t: ?m.962
t, โ† 
mkLambdaFVars: Array Expr โ†’ Expr โ†’ optParam Bool false โ†’ optParam Bool true โ†’ optParam BinderInfo BinderInfo.implicit โ†’ MetaM Expr
mkLambdaFVars 
es: ?m.948
es 
p: ?m.2213
p)
    let (
fvar: FVarId
fvar, 
goal2: MVarId
goal2) โ† 
(โ† declFn goal n t p): ?m.2588
(โ† 
declFn: ?m.583
declFn
(โ† declFn goal n t p): ?m.2588
 
goal: MVarId
goal
(โ† declFn goal n t p): ?m.2588
 
n: ?m.797
n
(โ† declFn goal n t p): ?m.2588
 
t: Expr
t
(โ† declFn goal n t p): ?m.2588
 
p: Expr
p
(โ† declFn goal n t p): ?m.2588
).
intro1P: MVarId โ†’ MetaM (FVarId ร— MVarId)
intro1P
    if let 
some: {ฮฑ : Type ?u.793} โ†’ ฮฑ โ†’ Option ฮฑ
some 
stx: Syntax
stx := 
name: Option Syntax
name then
      
goal2: MVarId
goal2
goal2.withContext do
        Term.addTermInfo' (isBinder := true) stx (mkFVar fvar): TermElabM (?m.2673 yโœ)
.
withContext: {n : Type โ†’ Type ?u.2728} โ†’ [inst : MonadControlT MetaM n] โ†’ [inst : Monad n] โ†’ {ฮฑ : Type} โ†’ MVarId โ†’ n ฮฑ โ†’ n ฮฑ
withContext
goal2.withContext do
        Term.addTermInfo' (isBinder := true) stx (mkFVar fvar): TermElabM (?m.2673 yโœ)
 
goal2.withContext do
        Term.addTermInfo' (isBinder := true) stx (mkFVar fvar): TermElabM (?m.2673 yโœ)
do
goal2.withContext do
        Term.addTermInfo' (isBinder := true) stx (mkFVar fvar): TermElabM (?m.2673 yโœ)

        
Term.addTermInfo': Syntax โ†’
  Expr โ†’
    optParam (Option Expr) none โ†’
      optParam (Option LocalContext) none โ†’ optParam Name Name.anonymous โ†’ optParam Bool false โ†’ TermElabM Unit
Term.addTermInfo'
goal2.withContext do
        Term.addTermInfo' (isBinder := true) stx (mkFVar fvar): TermElabM (?m.2673 yโœ)
 (isBinder := 
true: Bool
true
goal2.withContext do
        Term.addTermInfo' (isBinder := true) stx (mkFVar fvar): TermElabM (?m.2673 yโœ)
) 
stx: Syntax
stx
goal2.withContext do
        Term.addTermInfo' (isBinder := true) stx (mkFVar fvar): TermElabM (?m.2673 yโœ)
 (
mkFVar: FVarId โ†’ Expr
mkFVar
goal2.withContext do
        Term.addTermInfo' (isBinder := true) stx (mkFVar fvar): TermElabM (?m.2673 yโœ)
 
fvar: FVarId
fvar
goal2.withContext do
        Term.addTermInfo' (isBinder := true) stx (mkFVar fvar): TermElabM (?m.2673 yโœ)
)
    
pure: {f : Type ?u.3202 โ†’ Type ?u.3201} โ†’ [self : Pure f] โ†’ {ฮฑ : Type ?u.3202} โ†’ ฮฑ โ†’ f ฮฑ
pure (
goal1: MVarId
goal1, 
goal2: MVarId
goal2)

elab_rules : tactic
| `(tactic| have $[$
n: ?m.8302
n:ident $
bs: ?m.8305
bs*]? $[: $
t: ?m.8850
t:
term: Parser.Category
term]?) => do
  let (
goal1: MVarId
goal1, 
goal2: MVarId
goal2) โ† 
haveLetCore: MVarId โ†’ Option Syntax โ†’ Array Syntax โ†’ Option Syntax โ†’ Bool โ†’ Elab.TermElabM (MVarId ร— MVarId)
haveLetCore 
(โ† getMainGoal): ?m.9262
(โ† 
getMainGoal: TacticM MVarId
getMainGoal
(โ† getMainGoal): ?m.9262
) 
n: ?m.8309 xโœยน
n (
bs: ?m.8310 xโœยน n
bs.
getD: {ฮฑ : Type ?u.9452} โ†’ Option ฮฑ โ†’ ฮฑ โ†’ ฮฑ
getD 
#[]: Array ?m.9459
#[]) 
t: ?m.8854 xโœ
t 
false: Bool
false
  
replaceMainGoal: List MVarId โ†’ TacticM Unit
replaceMainGoal [
goal1: MVarId
goal1, 
goal2: MVarId
goal2]

elab_rules : tactic
| `(tactic| suffices $[$
n: ?m.13284
n:ident $
bs: ?m.13276
bs*]? $[: $
t: ?m.13667
t:
term: Parser.Category
term]?) => do
  let (
goal1: MVarId
goal1, 
goal2: MVarId
goal2) โ† 
haveLetCore: MVarId โ†’ Option Syntax โ†’ Array Syntax โ†’ Option Syntax โ†’ Bool โ†’ Elab.TermElabM (MVarId ร— MVarId)
haveLetCore 
(โ† getMainGoal): ?m.14079
(โ† 
getMainGoal: TacticM MVarId
getMainGoal
(โ† getMainGoal): ?m.14079
) 
n: ?m.13126 xโœยน
n (
bs: ?m.13127 xโœยน n
bs.
getD: {ฮฑ : Type ?u.14269} โ†’ Option ฮฑ โ†’ ฮฑ โ†’ ฮฑ
getD 
#[]: Array ?m.14276
#[]) 
t: ?m.13671 xโœ
t 
false: Bool
false
  
replaceMainGoal: List MVarId โ†’ TacticM Unit
replaceMainGoal [
goal2: MVarId
goal2, 
goal1: MVarId
goal1]

elab_rules : tactic
| `(tactic| let $[$
n: ?m.17749
n:ident $
bs: ?m.17752
bs*]? $[: $
t: ?m.18297
t:
term: Parser.Category
term]?) => 
withMainContext: {ฮฑ : Type} โ†’ TacticM ฮฑ โ†’ TacticM ฮฑ
withMainContext do
  let (
goal1: MVarId
goal1, 
goal2: MVarId
goal2) โ† 
haveLetCore: MVarId โ†’ Option Syntax โ†’ Array Syntax โ†’ Option Syntax โ†’ Bool โ†’ Elab.TermElabM (MVarId ร— MVarId)
haveLetCore 
(โ† getMainGoal): ?m.18714
(โ† 
getMainGoal: TacticM MVarId
getMainGoal
(โ† getMainGoal): ?m.18714
) 
n: ?m.17756 xโœยน
n (
bs: ?m.17757 xโœยน n
bs.
getD: {ฮฑ : Type ?u.18904} โ†’ Option ฮฑ โ†’ ฮฑ โ†’ ฮฑ
getD 
#[]: Array ?m.18911
#[]) 
t: ?m.18301 xโœ
t 
true: Bool
true
  
replaceMainGoal: List MVarId โ†’ TacticM Unit
replaceMainGoal [
goal1: MVarId
goal1, 
goal2: MVarId
goal2]