Documentation

Mathlib.Tactic.Basic

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

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.

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

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

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.
Equations
• One or more equations did not get rendered due to their size.

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.
Equations
• One or more equations did not get rendered due to their size.
Equations

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

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

This tactic clears all auxiliary declarations from the context.

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

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.

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.