Documentation

Mathlib.Tactic.Basic

source
ink
def Mathlib.Tactic.variables :
Lean.ParserDescr
Equations
  • One or more equations did not get rendered due to their size.
source
ink
def Mathlib.Tactic.elabVariables :
Lean.Elab.Command.CommandElab
Equations
  • One or more equations did not get rendered due to their size.
source
ink
def Mathlib.Tactic.lemma :
Lean.ParserDescr

lemma means the same as theorem. It is used to denote "less important" theorems

Equations
  • One or more equations did not get rendered due to their size.
source
ink
def Mathlib.Tactic.expandLemma :
Lean.Macro

Implementation of the lemma command, by macro expansion to theorem.

Equations
  • One or more equations did not get rendered due to their size.
source
ink
def Mathlib.Tactic.tacticBy_cases_ :
Lean.ParserDescr

by_cases p makes a case distinction on p, resulting in two subgoals h : p ⊢⊢ and h : ¬ p ⊢¬ p ⊢⊢.

Equations
  • One or more equations did not get rendered due to their size.
source
ink
def Mathlib.Tactic.tacticTransitivity__ :
Lean.ParserDescr
Equations
  • One or more equations did not get rendered due to their size.
source
ink
def Mathlib.Tactic.introv :
Lean.ParserDescr

The tactic introv allows the user to automatically introduce the variables of a theorem and explicitly name the non-dependent hypotheses. Any dependent hypotheses are assigned their default names.

Examples:

example : ∀ a b : Nat, a = b → b = a := by
  introv h,
  exact h.symm
∀ a b : Nat, a = b → b = a := by
  introv h,
  exact h.symm
→ b = a := by
  introv h,
  exact h.symm

The state after introv h is

a b : ℕ,
h : a = b
⊢ b = a
⊢ b = a

example : ∀ a b : Nat, a = b → ∀ c, b = c → a = c := by
  introv h₁ h₂,
  exact h₁.trans h₂
∀ a b : Nat, a = b → ∀ c, b = c → a = c := by
  introv h₁ h₂,
  exact h₁.trans h₂
→ ∀ c, b = c → a = c := by
  introv h₁ h₂,
  exact h₁.trans h₂
∀ c, b = c → a = c := by
  introv h₁ h₂,
  exact h₁.trans h₂
→ a = c := by
  introv h₁ h₂,
  exact h₁.trans h₂

The state after introv h₁ h₂ is

a b : ℕ,
h₁ : a = b,
c : ℕ,
h₂ : b = c
⊢ a = c
⊢ a = c
Equations
  • One or more equations did not get rendered due to their size.
source
ink
def Mathlib.Tactic.evalIntrov :
Lean.Elab.Tactic.Tactic
Equations
  • One or more equations did not get rendered due to their size.
source
ink
partial def Mathlib.Tactic.evalIntrov.introsDep :
Lean.Elab.Tactic.TacticM Unit
source
ink
def Mathlib.Tactic.evalIntrov.intro1PStep :
Lean.Elab.Tactic.TacticM Unit
Equations
source
ink
def Mathlib.Tactic.tacticAssumption' :
Lean.ParserDescr

Try calling assumption on all goals; succeeds if it closes at least one goal.

Equations
source
ink
def Mathlib.Tactic.tacticMatch_target_ :
Lean.ParserDescr
Equations
  • One or more equations did not get rendered due to their size.
source
ink
def Mathlib.Tactic.clearAuxDecl :
Lean.ParserDescr

This tactic clears all auxiliary declarations from the context.

Equations
source
ink
def Lean.MVarId.clearValue (mvarId : Lean.MVarId) (fvarId : Lean.FVarId) :
Lean.MetaM Lean.MVarId

Clears the value of the local definition fvarId. Ensures that the resulting goal state is still type correct. Throws an error if it is a local hypothesis without a value.

Equations
  • One or more equations did not get rendered due to their size.
source
ink
def Mathlib.Tactic.clearValue :
Lean.ParserDescr

clear_value n₁ n₂ ... clears the bodies of the local definitions n₁, n₂ ..., changing them into regular hypotheses. A hypothesis n : α := t is changed to n : α.

The order of n₁ n₂ ... does not matter, and values will be cleared in reverse order of where they appear in the context.

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