Documentation

Mathlib.Tactic.Basic

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

Instances For

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

    Instances For

      The syntax variable (X Y ... Z : Sort*) creates a new distinct implicit universe variable for each variable in the sequence.

      Instances For

        The syntax variable (X Y ... Z : Type*) creates a new distinct implicit universe variable > 0 for each variable in the sequence.

        Instances For

          Given two arrays of FVarIds, one from an old local context and the other from a new local context, pushes FVarAliasInfos into the info tree for corresponding pairs of FVarIds. Recall that variables linked this way should be considered to be semantically identical.

          The effect of this is, for example, the unused variable linter will see that variables from the first array are used if corresponding variables in the second array are used.

          Instances For
            def Lean.MVarId.withReverted {α : Type} (mvarId : Lean.MVarId) (fvarIds : Array Lean.FVarId) (k : Lean.MVarIdArray Lean.FVarIdLean.MetaM (α × Array (Option Lean.FVarId) × Lean.MVarId)) (clearAuxDeclsInsteadOfRevert : optParam Bool false) :

            Function to help do the revert/intro pattern, running some code inside a context where certain variables have been reverted before re-introing them. It will push FVarId alias information into info trees for you according to a simple protocol.

            • fvarIds is an array of fvarIds to revert. These are passed to Lean.MVarId.revert with preserveOrder := true, hence the function raises an error if they cannot be reverted in the provided order.
            • k is given the goal with all the variables reverted and the array of reverted FVarIds, with the requested FVarIds at the beginning. It must return a tuple of a value, an array describing which FVarIds to link, and a mutated MVarId.

            The a : Array (Option FVarId) array returned by k is interpreted in the following way. The function will intro a.size variables, and then for each non-none entry we create an FVar alias between it and the corresponding introed variable. For example, having k return fvars.map .some causes all reverted variables to be introed and linked.

            Returns the value returned by k along with the resulting goal.

            Instances For

              Replace the type of the free variable fvarId with typeNew.

              If checkDefEq = true then throws an error if typeNew is not definitionally equal to the type of fvarId. Otherwise this function assumes typeNew and the type of fvarId are definitionally equal.

              This function is the same as Lean.MVarId.changeLocalDecl but makes sure to push substitution information into the infotree.

              Instances For

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

                Instances For

                  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
                  

                  The state after introv h is

                  a b : ℕ,
                  h : a = b
                  ⊢ b = a
                  
                  example : ∀ a b : Nat, a = b → ∀ c, b = c → 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
                  
                  Instances For

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

                    Instances For

                      This tactic clears all auxiliary declarations from the context.

                      Instances For

                        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.

                        Instances For

                          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.

                          Instances For