Documentation
Lean
.
Meta
.
Tactic
Search
return to top
source
Imports
Lean.Meta.Tactic.AC
Lean.Meta.Tactic.Apply
Lean.Meta.Tactic.Assert
Lean.Meta.Tactic.Assumption
Lean.Meta.Tactic.AuxLemma
Lean.Meta.Tactic.BVDecide
Lean.Meta.Tactic.Backtrack
Lean.Meta.Tactic.Cases
Lean.Meta.Tactic.Cbv
Lean.Meta.Tactic.Cleanup
Lean.Meta.Tactic.Clear
Lean.Meta.Tactic.Congr
Lean.Meta.Tactic.Constructor
Lean.Meta.Tactic.Contradiction
Lean.Meta.Tactic.Delta
Lean.Meta.Tactic.ElimInfo
Lean.Meta.Tactic.Ext
Lean.Meta.Tactic.FunInd
Lean.Meta.Tactic.Generalize
Lean.Meta.Tactic.Grind
Lean.Meta.Tactic.IndependentOf
Lean.Meta.Tactic.Induction
Lean.Meta.Tactic.Intro
Lean.Meta.Tactic.Lets
Lean.Meta.Tactic.NormCast
Lean.Meta.Tactic.Refl
Lean.Meta.Tactic.Rename
Lean.Meta.Tactic.Repeat
Lean.Meta.Tactic.Replace
Lean.Meta.Tactic.Revert
Lean.Meta.Tactic.Rewrite
Lean.Meta.Tactic.Rewrites
Lean.Meta.Tactic.Rfl
Lean.Meta.Tactic.Simp
Lean.Meta.Tactic.SolveByElim
Lean.Meta.Tactic.Split
Lean.Meta.Tactic.SplitIf
Lean.Meta.Tactic.Symm
Lean.Meta.Tactic.Try
Lean.Meta.Tactic.TryThis
Lean.Meta.Tactic.Unfold
Imported by
← Mathematical handbook