This file defines all the tactics that are required by mathport. Most of the syntax declarations in this file (as opposed to the imported files) are not defined anywhere and effectively form the TODO list before we can port mathlib to lean 4 for real.

For tactic writers: I (Mario) have put a comment before each syntax declaration to represent the estimated difficulty of writing the tactic. The key is as follows:

• E: Easy. It's a simple macro in terms of existing things, or an elab tactic for which we have many similar examples. Example: left
• M: Medium. An elab tactic, not too hard, perhaps a 100-200 lines file. Example: have
• N: Possibly requires new mechanisms in lean 4, some investigation required
• B: Hard, because it is a big and complicated tactic
• S: Possibly easy, because we can just stub it out or replace with something else
• ?: uncategorized

def Mathlib.Tactic.include : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.omit : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.parameter : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.propagateTags : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.mapply : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.tacticDestruct_ : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.abstract : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.rsimp : Lean.ParserDescr

Equations

• Mathlib.Tactic.rsimp = Lean.ParserDescr.node `Mathlib.Tactic.rsimp 1024 (Lean.ParserDescr.nonReservedSymbol "rsimp" false)

def Mathlib.Tactic.compVal : Lean.ParserDescr

Equations

• Mathlib.Tactic.compVal = Lean.ParserDescr.node `Mathlib.Tactic.compVal 1024 (Lean.ParserDescr.nonReservedSymbol "comp_val" false)

def Mathlib.Tactic.async : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.injectionsAndClear : Lean.ParserDescr

Equations

• Mathlib.Tactic.injectionsAndClear = Lean.ParserDescr.node `Mathlib.Tactic.injectionsAndClear 1024 (Lean.ParserDescr.nonReservedSymbol "injections_and_clear" false)

def Mathlib.Tactic.tryFor : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.unfoldCoes : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.unfoldWf : Lean.ParserDescr

Equations

• Mathlib.Tactic.unfoldWf = Lean.ParserDescr.node `Mathlib.Tactic.unfoldWf 1024 (Lean.ParserDescr.nonReservedSymbol "unfold_wf" false)

def Mathlib.Tactic.unfoldAux : Lean.ParserDescr

Equations

• Mathlib.Tactic.unfoldAux = Lean.ParserDescr.node `Mathlib.Tactic.unfoldAux 1024 (Lean.ParserDescr.nonReservedSymbol "unfold_aux" false)

def Mathlib.Tactic.continue : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.refineStruct : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.matchHyp : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.guardTags : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.guardProofTerm : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.failIfSuccess? : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.field : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.haveField : Lean.ParserDescr

Equations

• Mathlib.Tactic.haveField = Lean.ParserDescr.node `Mathlib.Tactic.haveField 1024 (Lean.ParserDescr.nonReservedSymbol "have_field" false)

def Mathlib.Tactic.applyField : Lean.ParserDescr

Equations

• Mathlib.Tactic.applyField = Lean.ParserDescr.node `Mathlib.Tactic.applyField 1024 (Lean.ParserDescr.nonReservedSymbol "apply_field" false)

def Mathlib.Tactic.hGeneralize : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.hGeneralize! : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.extractGoal! : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.revertDeps : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.revertAfter : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.revertTargetDeps : Lean.ParserDescr

Equations

• Mathlib.Tactic.revertTargetDeps = Lean.ParserDescr.node `Mathlib.Tactic.revertTargetDeps 1024 (Lean.ParserDescr.nonReservedSymbol "revert_target_deps" false)

def Mathlib.Tactic.rcases? : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.rintro? : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.decide! : Lean.ParserDescr

Equations

• Mathlib.Tactic.decide! = Lean.ParserDescr.node `Mathlib.Tactic.decide! 1024 (Lean.ParserDescr.nonReservedSymbol "decide!" false)

def Mathlib.Tactic.deltaInstance : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.elide : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.unelide : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.ext1? : Lean.ParserDescr

ext1? pat* is like ext1 pat* but gives a suggestion on what pattern to use

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.ext? : Lean.ParserDescr

ext? pat* is like ext pat* but gives a suggestion on what pattern to use

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.clarify : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.safe : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.finish : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.generalizesArg : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.generalizes : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.withPattern : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.cases'' : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.fixingClause : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.generalizingClause : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.induction'' : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.obviously : Lean.ParserDescr

Equations

• Mathlib.Tactic.obviously = Lean.ParserDescr.node `Mathlib.Tactic.obviously 1024 (Lean.ParserDescr.nonReservedSymbol "obviously" false)

def Mathlib.Tactic.prettyCases : Lean.ParserDescr

Equations

• Mathlib.Tactic.prettyCases = Lean.ParserDescr.node `Mathlib.Tactic.prettyCases 1024 (Lean.ParserDescr.nonReservedSymbol "pretty_cases" false)

def Mathlib.Tactic.assocRw : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.dsimpResult : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.simpResult : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.suggest : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.truncCases : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.applyNormed : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.acMono : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.reassoc : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.reassoc! : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.deriveReassocProof : Lean.ParserDescr

Equations

• Mathlib.Tactic.deriveReassocProof = Lean.ParserDescr.node `Mathlib.Tactic.deriveReassocProof 1024 (Lean.ParserDescr.nonReservedSymbol "derive_reassoc_proof" false)

def Mathlib.Tactic.subtypeInstance : Lean.ParserDescr

Equations

• Mathlib.Tactic.subtypeInstance = Lean.ParserDescr.node `Mathlib.Tactic.subtypeInstance 1024 (Lean.ParserDescr.nonReservedSymbol "subtype_instance" false)

def Mathlib.Tactic.transport : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.unfoldCases : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.equivRw : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.equivRwType : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.nthRwLHS : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.nthRwRHS : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.piInstanceDeriveField : Lean.ParserDescr

Equations

• Mathlib.Tactic.piInstanceDeriveField = Lean.ParserDescr.node `Mathlib.Tactic.piInstanceDeriveField 1024 (Lean.ParserDescr.nonReservedSymbol "pi_instance_derive_field" false)

def Mathlib.Tactic.piInstance : Lean.ParserDescr

Equations

• Mathlib.Tactic.piInstance = Lean.ParserDescr.node `Mathlib.Tactic.piInstance 1024 (Lean.ParserDescr.nonReservedSymbol "pi_instance" false)

def Mathlib.Tactic.tidy : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.tidy? : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.deriveElementwiseProof : Lean.ParserDescr

Equations

• Mathlib.Tactic.deriveElementwiseProof = Lean.ParserDescr.node `Mathlib.Tactic.deriveElementwiseProof 1024 (Lean.ParserDescr.nonReservedSymbol "derive_elementwise_proof" false)

def Mathlib.Tactic.computeDegreeLE : Lean.ParserDescr

Equations

• Mathlib.Tactic.computeDegreeLE = Lean.ParserDescr.node `Mathlib.Tactic.computeDegreeLE 1024 (Lean.ParserDescr.nonReservedSymbol "compute_degree_le" false)

def Mathlib.Tactic.mkDecorations : Lean.ParserDescr

Equations

• Mathlib.Tactic.mkDecorations = Lean.ParserDescr.node `Mathlib.Tactic.mkDecorations 1024 (Lean.ParserDescr.nonReservedSymbol "mk_decorations" false)

def Mathlib.Tactic.isBounded_default : Lean.ParserDescr

Equations

• Mathlib.Tactic.isBounded_default = Lean.ParserDescr.node `Mathlib.Tactic.isBounded_default 1024 (Lean.ParserDescr.nonReservedSymbol "isBounded_default" false)

def Mathlib.Tactic.mvBisim : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.unitInterval : Lean.ParserDescr

Equations

• Mathlib.Tactic.unitInterval = Lean.ParserDescr.node `Mathlib.Tactic.unitInterval 1024 (Lean.ParserDescr.nonReservedSymbol "unit_interval" false)

def Mathlib.Tactic.padicIndexSimp : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.uniqueDiffWithinAt_Ici_Iic_univ : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.wittTruncateFunTac : Lean.ParserDescr

Equations

• Mathlib.Tactic.wittTruncateFunTac = Lean.ParserDescr.node `Mathlib.Tactic.wittTruncateFunTac 1024 (Lean.ParserDescr.nonReservedSymbol "witt_truncate_fun_tac" false)

def Mathlib.Tactic.intro : Lean.ParserDescr

Equations

• Mathlib.Tactic.intro = Lean.ParserDescr.node `Mathlib.Tactic.intro 1024 (Lean.ParserDescr.nonReservedSymbol "intro" false)

def Mathlib.Tactic.intro! : Lean.ParserDescr

Equations

• Mathlib.Tactic.intro! = Lean.ParserDescr.node `Mathlib.Tactic.intro! 1024 (Lean.ParserDescr.nonReservedSymbol "intro!" false)

def Mathlib.Tactic.interactive : Lean.ParserDescr

Equations

• Mathlib.Tactic.interactive = Lean.ParserDescr.node `Mathlib.Tactic.interactive 1024 (Lean.ParserDescr.nonReservedSymbol "interactive" false)

def Mathlib.Tactic.expandExists : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.protectProj : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.notationClass : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.addTacticDoc : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.listUnusedDecls : Lean.ParserDescr

Equations

• Mathlib.Tactic.listUnusedDecls = Lean.ParserDescr.node `Mathlib.Tactic.listUnusedDecls 1024 (Lean.ParserDescr.symbol "#list_unused_decls")

def Mathlib.Tactic.defReplacer : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.reassocAxiom : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.sample : Lean.ParserDescr

Equations

• Mathlib.Tactic.sample = Lean.ParserDescr.node `Mathlib.Tactic.sample 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "#sample ") (Lean.ParserDescr.cat `term 0))

def Mathlib.Tactic.printSorryIn : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.assertInstance : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.assertNoInstance : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.