Documentation

Lean.Elab.GenInjective

Lean.Elab.GenInjective

Imports

Init
Lean.Elab.Command
Lean.Meta.Injective

Imported by

Lean.Elab

Lean.Elab.Command.elabGenInjectiveTheorems

def Lean.Elab.Command.elabGenInjectiveTheorems:

Lean.Elab.Command.CommandElab

Equations

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

General documentation

Library

Init.Control.Basic

Init.Control.EState

Init.Control.Except

Init.Control.ExceptCps

Init.Control.Id

Init.Control.Lawful

Init.Control.Option

Init.Control.Reader

Init.Control.State

Init.Control.StateCps

Init.Control.StateRef

Init.Data.Array

Init.Data.Array.Basic

Init.Data.Array.BasicAux

Init.Data.Array.BinSearch

Init.Data.Array.DecidableEq

Init.Data.Array.InsertionSort

Init.Data.Array.Mem

Init.Data.Array.QSort

Init.Data.Array.Subarray

Init.Data.ByteArray

Init.Data.ByteArray.Basic

Init.Data.Char.Basic

Init.Data.Fin.Basic

Init.Data.FloatArray

Init.Data.FloatArray.Basic

Init.Data.Format

Init.Data.Format.Basic

Init.Data.Format.Instances

Init.Data.Format.Macro

Init.Data.Format.Syntax

Init.Data.Int.Basic

Init.Data.List.Basic

Init.Data.List.BasicAux

Init.Data.List.Control

Init.Data.Nat.Basic

Init.Data.Nat.Bitwise

Init.Data.Nat.Control

Init.Data.Nat.Div

Init.Data.Nat.Gcd

Init.Data.Nat.Linear

Init.Data.Nat.Log2

Init.Data.Nat.SOM

Init.Data.Option

Init.Data.Option.Basic

Init.Data.Option.BasicAux

Init.Data.Option.Instances

Init.Data.String

Init.Data.String.Basic

Init.Data.String.Extra

Init.Data.ToString

Init.Data.ToString.Basic

Init.Data.ToString.Macro

Init.Data.Basic

Init.Data.Float

Init.Data.Hashable

Init.Data.OfScientific

Init.Data.Random

Init.Data.Range

Init.Data.Stream

Init.System.FilePath

Init.System.IOError

Init.System.Platform

Init.NotationExtra

Init.SimpLemmas

Init.SizeOfLemmas

Lean.Compiler.IR

Lean.Compiler.IR.Basic

Lean.Compiler.IR.Borrow

Lean.Compiler.IR.Boxing

Lean.Compiler.IR.Checker

Lean.Compiler.IR.CompilerM

Lean.Compiler.IR.CtorLayout

Lean.Compiler.IR.ElimDeadBranches

Lean.Compiler.IR.ElimDeadVars

Lean.Compiler.IR.EmitC

Lean.Compiler.IR.EmitUtil

Lean.Compiler.IR.ExpandResetReuse

Lean.Compiler.IR.Format

Lean.Compiler.IR.FreeVars

Lean.Compiler.IR.LiveVars

Lean.Compiler.IR.NormIds

Lean.Compiler.IR.PushProj

Lean.Compiler.IR.RC

Lean.Compiler.IR.ResetReuse

Lean.Compiler.IR.SimpCase

Lean.Compiler.IR.Sorry

Lean.Compiler.IR.UnboxResult

Lean.Compiler.BorrowedAnnotation

Lean.Compiler.CSimpAttr

Lean.Compiler.ClosedTermCache

Lean.Compiler.ConstFolding

Lean.Compiler.ExportAttr

Lean.Compiler.ExternAttr

Lean.Compiler.FFI

Lean.Compiler.ImplementedByAttr

Lean.Compiler.InitAttr

Lean.Compiler.InlineAttrs

Lean.Compiler.NameMangling

Lean.Compiler.NeverExtractAttr

Lean.Compiler.NoncomputableAttr

Lean.Compiler.Specialize

Lean.Compiler.Util

Lean.Data.Json.Basic

Lean.Data.Json.FromToJson

Lean.Data.Json.Parser

Lean.Data.Json.Printer

Lean.Data.Json.Stream

Lean.Data.Lsp.Basic

Lean.Data.Lsp.Capabilities

Lean.Data.Lsp.Client

Lean.Data.Lsp.Communication

Lean.Data.Lsp.Diagnostics

Lean.Data.Lsp.Extra

Lean.Data.Lsp.InitShutdown

Lean.Data.Lsp.Internal

Lean.Data.Lsp.Ipc

Lean.Data.Lsp.LanguageFeatures

Lean.Data.Lsp.TextSync

Lean.Data.Lsp.Utf16

Lean.Data.Lsp.Workspace

Lean.Data.Xml.Basic

Lean.Data.Xml.Parser

Lean.Data.Format

Lean.Data.FuzzyMatching

Lean.Data.JsonRpc

Lean.Data.KVMap

Lean.Data.LBool

Lean.Data.LOption

Lean.Data.NameTrie

Lean.Data.Occurrences

Lean.Data.OpenDecl

Lean.Data.Options

Lean.Data.Parsec

Lean.Data.Position

Lean.Data.PrefixTree

Lean.Elab.Deriving

Lean.Elab.Deriving.BEq

Lean.Elab.Deriving.Basic

Lean.Elab.Deriving.DecEq

Lean.Elab.Deriving.FromToJson

Lean.Elab.Deriving.Hashable

Lean.Elab.Deriving.Inhabited

Lean.Elab.Deriving.Ord

Lean.Elab.Deriving.Repr

Lean.Elab.Deriving.SizeOf

Lean.Elab.Deriving.Util

Lean.Elab.PreDefinition

Lean.Elab.PreDefinition.Structural

Lean.Elab.PreDefinition.Structural.BRecOn

Lean.Elab.PreDefinition.Structural.Basic

Lean.Elab.PreDefinition.Structural.Eqns

Lean.Elab.PreDefinition.Structural.FindRecArg

Lean.Elab.PreDefinition.Structural.IndPred

Lean.Elab.PreDefinition.Structural.Main

Lean.Elab.PreDefinition.Structural.Preprocess

Lean.Elab.PreDefinition.Structural.SmartUnfolding

Lean.Elab.PreDefinition.WF

Lean.Elab.PreDefinition.WF.Eqns

Lean.Elab.PreDefinition.WF.Fix

Lean.Elab.PreDefinition.WF.Ite

Lean.Elab.PreDefinition.WF.Main

Lean.Elab.PreDefinition.WF.PackDomain

Lean.Elab.PreDefinition.WF.PackMutual

Lean.Elab.PreDefinition.WF.Rel

Lean.Elab.PreDefinition.WF.TerminationHint

Lean.Elab.PreDefinition.Basic

Lean.Elab.PreDefinition.Eqns

Lean.Elab.PreDefinition.Main

Lean.Elab.PreDefinition.MkInhabitant

Lean.Elab.Quotation

Lean.Elab.Quotation.Precheck

Lean.Elab.Quotation.Util

Lean.Elab.Tactic

Lean.Elab.Tactic.Conv

Lean.Elab.Tactic.Conv.Basic

Lean.Elab.Tactic.Conv.Change

Lean.Elab.Tactic.Conv.Congr

Lean.Elab.Tactic.Conv.Delta

Lean.Elab.Tactic.Conv.Pattern

Lean.Elab.Tactic.Conv.Rewrite

Lean.Elab.Tactic.Conv.Simp

Lean.Elab.Tactic.Conv.Unfold

Lean.Elab.Tactic.Basic

Lean.Elab.Tactic.BuiltinTactic

Lean.Elab.Tactic.Cache

Lean.Elab.Tactic.Config

Lean.Elab.Tactic.Delta

Lean.Elab.Tactic.ElabTerm

Lean.Elab.Tactic.Generalize

Lean.Elab.Tactic.Induction

Lean.Elab.Tactic.Injection

Lean.Elab.Tactic.Location

Lean.Elab.Tactic.Match

Lean.Elab.Tactic.Meta

Lean.Elab.Tactic.Rewrite

Lean.Elab.Tactic.Simp

Lean.Elab.Tactic.Split

Lean.Elab.Tactic.Unfold

Lean.Elab.Attributes

Lean.Elab.AutoBound

Lean.Elab.AuxDef

Lean.Elab.AuxDiscr

Lean.Elab.Binders

Lean.Elab.BindersUtil

Lean.Elab.BuiltinCommand

Lean.Elab.BuiltinNotation

Lean.Elab.BuiltinTerm

Lean.Elab.Command

Lean.Elab.Config

Lean.Elab.DeclModifiers

Lean.Elab.DeclUtil

Lean.Elab.Declaration

Lean.Elab.DeclarationRange

Lean.Elab.DefView

Lean.Elab.ElabRules

Lean.Elab.Exception

Lean.Elab.Extra

Lean.Elab.Frontend

Lean.Elab.GenInjective

Lean.Elab.Import

Lean.Elab.Inductive

Lean.Elab.InfoTree

Lean.Elab.LetRec

Lean.Elab.Level

Lean.Elab.Macro

Lean.Elab.MacroArgUtil

Lean.Elab.MacroRules

Lean.Elab.Match

Lean.Elab.MatchAltView

Lean.Elab.Mixfix

Lean.Elab.MutualDef

Lean.Elab.Notation

Lean.Elab.PatternVar

Lean.Elab.Print

Lean.Elab.RecAppSyntax

Lean.Elab.SetOption

Lean.Elab.StructInst

Lean.Elab.Structure

Lean.Elab.Syntax

Lean.Elab.SyntheticMVars

Lean.Linter.Basic

Lean.Linter.Util

Lean.Meta.Match

Lean.Meta.Match.Basic

Lean.Meta.Match.CaseArraySizes

Lean.Meta.Match.CaseValues

Lean.Meta.Match.MVarRenaming

Lean.Meta.Match.Match

Lean.Meta.Match.MatchEqs

Lean.Meta.Match.MatchEqsExt

Lean.Meta.Match.MatchPatternAttr

Lean.Meta.Match.MatcherInfo

Lean.Meta.Match.Value

Lean.Meta.Tactic

Lean.Meta.Tactic.AC

Lean.Meta.Tactic.AC.Main

Lean.Meta.Tactic.LinearArith

Lean.Meta.Tactic.LinearArith.Nat

Lean.Meta.Tactic.LinearArith.Nat.Basic

Lean.Meta.Tactic.LinearArith.Nat.Simp

Lean.Meta.Tactic.LinearArith.Nat.Solver

Lean.Meta.Tactic.LinearArith.Basic

Lean.Meta.Tactic.LinearArith.Main

Lean.Meta.Tactic.LinearArith.Simp

Lean.Meta.Tactic.LinearArith.Solver

Lean.Meta.Tactic.Simp

Lean.Meta.Tactic.Simp.Main

Lean.Meta.Tactic.Simp.Rewrite

Lean.Meta.Tactic.Simp.SimpAll

Lean.Meta.Tactic.Simp.SimpCongrTheorems

Lean.Meta.Tactic.Simp.SimpTheorems

Lean.Meta.Tactic.Simp.Types

Lean.Meta.Tactic.Acyclic

Lean.Meta.Tactic.Apply

Lean.Meta.Tactic.Assert

Lean.Meta.Tactic.Assumption

Lean.Meta.Tactic.AuxLemma

Lean.Meta.Tactic.Cases

Lean.Meta.Tactic.Cleanup

Lean.Meta.Tactic.Clear

Lean.Meta.Tactic.Constructor

Lean.Meta.Tactic.Contradiction

Lean.Meta.Tactic.Delta

Lean.Meta.Tactic.ElimInfo

Lean.Meta.Tactic.FVarSubst

Lean.Meta.Tactic.Generalize

Lean.Meta.Tactic.Induction

Lean.Meta.Tactic.Injection

Lean.Meta.Tactic.Intro

Lean.Meta.Tactic.Refl

Lean.Meta.Tactic.Rename

Lean.Meta.Tactic.Replace

Lean.Meta.Tactic.Revert

Lean.Meta.Tactic.Rewrite

Lean.Meta.Tactic.Split

Lean.Meta.Tactic.SplitIf

Lean.Meta.Tactic.Subst

Lean.Meta.Tactic.Unfold

Lean.Meta.Tactic.UnifyEq

Lean.Meta.Tactic.Util

Lean.Meta.AbstractMVars

Lean.Meta.AbstractNestedProofs

Lean.Meta.AppBuilder

Lean.Meta.Basic

Lean.Meta.CasesOn

Lean.Meta.Check

Lean.Meta.Closure

Lean.Meta.CollectFVars

Lean.Meta.CollectMVars

Lean.Meta.CongrTheorems

Lean.Meta.Constructions

Lean.Meta.DecLevel

Lean.Meta.DiscrTree

Lean.Meta.DiscrTreeTypes

Lean.Meta.ExprDefEq

Lean.Meta.ExprLens

Lean.Meta.ExprTraverse

Lean.Meta.ForEachExpr

Lean.Meta.FunInfo

Lean.Meta.GeneralizeTelescope

Lean.Meta.GeneralizeVars

Lean.Meta.GetConst

Lean.Meta.GlobalInstances

Lean.Meta.IndPredBelow

Lean.Meta.Inductive

Lean.Meta.InferType

Lean.Meta.Injective

Lean.Meta.Instances

Lean.Meta.KAbstract

Lean.Meta.KExprMap

Lean.Meta.LevelDefEq

Lean.Meta.MatchUtil

Lean.Meta.Offset

Lean.Meta.PPGoal

Lean.Meta.RecursorInfo

Lean.Meta.Reduce

Lean.Meta.ReduceEval

Lean.Meta.SizeOf

Lean.Meta.Structure

Lean.Meta.SynthInstance

Lean.Meta.Transform

Lean.Meta.TransparencyMode

Lean.Meta.UnificationHint

Lean.Parser.Attr

Lean.Parser.Basic

Lean.Parser.Command

Lean.Parser.Extension

Lean.Parser.Extra

Lean.Parser.Level

Lean.Parser.Module

Lean.Parser.StrInterpolation

Lean.Parser.Syntax

Lean.Parser.Tactic

Lean.Parser.Term

Lean.ParserCompiler

Lean.ParserCompiler.Attribute

Lean.PrettyPrinter

Lean.PrettyPrinter.Delaborator

Lean.PrettyPrinter.Delaborator.Basic

Lean.PrettyPrinter.Delaborator.Builtins

Lean.PrettyPrinter.Delaborator.Options

Lean.PrettyPrinter.Delaborator.SubExpr

Lean.PrettyPrinter.Delaborator.TopDownAnalyze

Lean.PrettyPrinter.Basic

Lean.PrettyPrinter.Formatter

Lean.PrettyPrinter.Parenthesizer

Lean.Server.FileWorker

Lean.Server.FileWorker.RequestHandling

Lean.Server.FileWorker.Utils

Lean.Server.FileWorker.WidgetRequests

Lean.Server.Rpc

Lean.Server.Rpc.Basic

Lean.Server.Rpc.Deriving

Lean.Server.Rpc.RequestHandling

Lean.Server.AsyncList

Lean.Server.Completion

Lean.Server.FileSource

Lean.Server.GoTo

Lean.Server.InfoUtils

Lean.Server.References

Lean.Server.Requests

Lean.Server.Snapshots

Lean.Server.Utils

Lean.Server.Watchdog

Lean.Util.CollectFVars

Lean.Util.CollectLevelParams

Lean.Util.CollectMVars

Lean.Util.FindExpr

Lean.Util.FindLevelMVar

Lean.Util.FindMVar

Lean.Util.FoldConsts

Lean.Util.ForEachExpr

Lean.Util.HasConstCache

Lean.Util.MonadBacktrack

Lean.Util.MonadCache

Lean.Util.OccursCheck

Lean.Util.PPExt

Lean.Util.Paths

Lean.Util.Profile

Lean.Util.RecDepth

Lean.Util.Recognizers

Lean.Util.ReplaceExpr

Lean.Util.ReplaceLevel

Lean.Util.Sorry

Lean.Util.Trace

Lean.Widget.Basic

Lean.Widget.InteractiveCode

Lean.Widget.InteractiveDiagnostic

Lean.Widget.InteractiveGoal

Lean.Widget.TaggedText

Lean.Attributes

Lean.AuxRecursor

Lean.Declaration

Lean.DeclarationRange

Lean.Environment

Lean.ImportingFlag

Lean.InternalExceptionId

Lean.KeyedDeclsAttribute

Lean.LazyInitExtension

Lean.LoadDynlib

Lean.LocalContext

Lean.MetavarContext

Lean.ReducibilityAttrs

Lean.ResolveName

Lean.ScopedEnvExtension

Mathlib

Mathlib.Util

Mathlib.Util.IncludeStr

Std

Std.Data

Std.Data.AssocList

Std.Data.HashMap

Std.Data.HashSet

Std.Data.PersistentArray

Std.Data.PersistentHashMap

Std.Data.PersistentHashSet

Std.Data.RBTree

Std.ShareCommon

Unicode.General

Unicode.General.GeneralCategory

Unicode.General.Name

Unicode.Includes