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
- Mathlib.Tactic.evalIntrov.intro1PStep = Lean.Elab.Tactic.liftMetaTactic fun goal => do let __discr ← Lean.MVarId.intro1P goal match __discr with | (fst, goal) => pure [goal]
Try calling assumption
on all goals; succeeds if it closes at least one goal.
Equations
- Mathlib.Tactic.tacticAssumption' = Lean.ParserDescr.node `Mathlib.Tactic.tacticAssumption' 1024 (Lean.ParserDescr.nonReservedSymbol "assumption'" false)
Equations
- One or more equations did not get rendered due to their size.
This tactic clears all auxiliary declarations from the context.
Equations
- Mathlib.Tactic.clearAuxDecl = Lean.ParserDescr.node `Mathlib.Tactic.clearAuxDecl 1024 (Lean.ParserDescr.nonReservedSymbol "clear_aux_decl" false)
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.