mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Computability.ContextFreeGrammar
/-- Input nonterminal a.k.a. left-hand side.  -/
ContextFreeRule.input : {T : Type u_1} → {N : Type u_2} → ContextFreeRule T N → N
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.size_modify : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β}
  [inst_2 : EquivBEq α] [LawfulHashable α] {k : α} {f : β → β},
  m.WF → (Std.DHashMap.Raw.Const.modify m k f).size = m.size
-- Init.Data.Range.Polymorphic.RangeIterator
/-- An efficient `IteratorLoop` instance:
As long as the compiler cannot optimize away the `Option` in the internal state, we use a special
loop implementation.
 -/
Std.Rxi.Iterator.instIteratorLoop : {α : Type u} →
  [inst : Std.PRange.UpwardEnumerable α] →
    [Std.PRange.LawfulUpwardEnumerable α] →
      {n : Type u → Type w} → [Monad n] → Std.IteratorLoop (Std.Rxi.Iterator α) Id n
-- Mathlib.RingTheory.LocalProperties.Basic
Ideal.iInf_ker_le : ∀ {R : Type u_1} [inst : CommSemiring R] (I : Ideal R),
  ⨅ p, ⨅ (x : p.IsPrime), ⨅ (_ : I ≤ p), RingHom.ker (algebraMap R (Localization.AtPrime p)) ≤ I
-- Mathlib.NumberTheory.RamificationInertia.Ramification
Ideal.ramificationIdx'.eq_1 : ∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal R)
  (P : Ideal S), p.ramificationIdx' P = sSup {n | Ideal.map (algebraMap R S) p ≤ P ^ n}
-- Mathlib.Logic.Equiv.Basic
Equiv.sigmaSigmaSubtype_symm_apply : ∀ {α : Type u_9} {β : α → Type u_10} {γ : (a : α) → β a → Type u_11} (p : (a : α) × β a → Prop)
  [uniq : Unique { ab // p ab }] {a : α} {b : β a} (c : γ a b) (h : p ⟨a, b⟩),
  (Equiv.sigmaSigmaSubtype p h).symm c = ⟨⟨a, ⟨b, c⟩⟩, h⟩
-- Std.Http.Protocol.H1.Message
/-- Determines the message body size based on the `Content-Length` header and the `Transfer-Encoding` (chunked) flag.
 -/
Std.Http.Protocol.H1.Message.Head.getSize : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Message.Head dir → Bool → Option Std.Http.Body.Length
-- Lean.Data.Lsp.Basic
Lean.Lsp.TextDocumentEdit.mk.injEq : ∀ (textDocument : Lean.Lsp.VersionedTextDocumentIdentifier) (edits : Lean.Lsp.TextEditBatch)
  (textDocument_1 : Lean.Lsp.VersionedTextDocumentIdentifier) (edits_1 : Lean.Lsp.TextEditBatch),
  ({ textDocument := textDocument, edits := edits } = { textDocument := textDocument_1, edits := edits_1 }) =
    (textDocument = textDocument_1 ∧ edits = edits_1)
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
/-- See Note [custom simps projection]. We need to specify this projection explicitly in this case,
because it is a composition of multiple projections.  -/
ContinuousMultilinearMap.Simps.apply : {R : Type u} →
  {ι : Type v} →
    {M₁ : ι → Type w₁} →
      {M₂ : Type w₂} →
        [inst : Semiring R] →
          [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] →
            [inst_2 : AddCommMonoid M₂] →
              [inst_3 : (i : ι) → Module R (M₁ i)] →
                [inst_4 : Module R M₂] →
                  [inst_5 : (i : ι) → TopologicalSpace (M₁ i)] →
                    [inst_6 : TopologicalSpace M₂] → ContinuousMultilinearMap R M₁ M₂ → ((i : ι) → M₁ i) → M₂
-- Mathlib.RingTheory.AdicCompletion.Exactness
_private.Mathlib.RingTheory.AdicCompletion.Exactness.0.AdicCompletion.mapPreimage.eq_def : ∀ {R : Type u} [inst : CommRing R] {I : Ideal R} {M : Type v} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {N : Type w} [inst_3 : AddCommGroup N] [inst_4 : Module R N] {f : M →ₗ[R] N} (hf : Function.Surjective ⇑f)
  (x : AdicCompletion.AdicCauchySequence I N) (x_1 : ℕ),
  AdicCompletion.mapPreimage✝ hf x x_1 =
    match x_1 with
    | Nat.zero => ⟨⋯.choose, ⋯⟩
    | n.succ =>
      let y := ⋯.choose;
      have hy := ⋯;
      match AdicCompletion.mapPreimage✝ hf x n with
      | ⟨yₙ, hyₙ⟩ =>
        match AdicCompletion.mapPreimageDelta✝ hf x hy hyₙ with
        | ⟨⟨d, property⟩, p⟩ => ⟨yₙ - d, ⋯⟩
-- Mathlib.Topology.NhdsWithin
nhdsWithin_eq_nhdsWithin' : ∀ {α : Type u_1} [inst : TopologicalSpace α] {a : α} {s t u : Set α},
  s ∈ nhds a → t ∩ s = u ∩ s → nhdsWithin a t = nhdsWithin a u
-- Mathlib.Algebra.Order.SuccPred
Order.IsPredPrelimit.lt_sub_one : ∀ {α : Type u_1} {x y : α} [inst : PartialOrder α] [inst_1 : Sub α] [inst_2 : One α] [PredSubOrder α],
  Order.IsPredPrelimit x → x < y → x < y - 1
-- Mathlib.NumberTheory.Zsqrtd.Basic
/-- An element of `ℤ√d` has norm equal to `1` if and only if it is contained in the submonoid
of unitary elements.  -/
Zsqrtd.norm_eq_one_iff_mem_unitary : ∀ {d : ℤ} {a : ℤ√d}, a.norm = 1 ↔ a ∈ unitary (ℤ√d)
-- Init.Data.List.Sublist
List.Sublist.drop : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Sublist l₂ → ∀ (i : ℕ), (List.drop i l₁).Sublist (List.drop i l₂)
-- Std.Do.PredTrans
Std.Do.PredTrans.apply_Functor_map : ∀ {ps : Std.Do.PostShape} {α β : Type u} (f : α → β) (x : Std.Do.PredTrans ps α) (Q : Std.Do.PostCond β ps),
  (f <$> x).apply Q = x.apply (fun a => Q.1 (f a), Q.2)
-- Std.Data.ExtDHashMap.Basic
/-- Creates a hash map from a list of mappings. If the same key appears multiple times, the last
occurrence takes precedence.  -/
Std.ExtDHashMap.Const.ofList : {α : Type u} → {β : Type v} → [inst : BEq α] → [inst_1 : Hashable α] → List (α × β) → Std.ExtDHashMap α fun x => β
-- Mathlib.Order.BoundedOrder.Basic
Subtype.coe_eq_bot_iff : ∀ {α : Type u} {p : α → Prop} [inst : PartialOrder α] [inst_1 : OrderBot α] [inst_2 : OrderBot (Subtype p)],
  p ⊥ → ∀ {x : { x // p x }}, ↑x = ⊥ ↔ x = ⊥
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenNormalSubgroup.instSetLike : {G : Type u} → [inst : Group G] → [inst_1 : TopologicalSpace G] → SetLike (OpenNormalSubgroup G) G
-- Mathlib.Topology.Algebra.UniformConvergence
UniformFun.ofFun_sum : ∀ {α : Type u_1} {ι : Type u_3} {β : Type u_4} [inst : AddCommMonoid β] {f : ι → α → β} (I : Finset ι),
  UniformFun.ofFun (∑ i ∈ I, f i) = ∑ i ∈ I, UniformFun.ofFun (f i)
-- Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
Subgroup.forall_zpowers : ∀ {G : Type u_1} [inst : Group G] {x : G} {p : ↥(Subgroup.zpowers x) → Prop},
  (∀ (g : ↥(Subgroup.zpowers x)), p g) ↔ ∀ (m : ℤ), p ⟨x ^ m, ⋯⟩
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Valuation.Compatible.vle_iff_le : ∀ {R : Type u_1} {Γ : Type u_2} {inst : Ring R} {inst_1 : LinearOrderedCommMonoidWithZero Γ} {v : Valuation R Γ}
  {inst_2 : ValuativeRel R} [self : v.Compatible] (x y : R), x ≤ᵥ y ↔ v x ≤ v y
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.toLinearMap : {A : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      {W : Type u_4} →
        [inst : Semiring A] →
          [inst_1 : Monoid G] →
            [inst_2 : AddCommMonoid V] →
              [inst_3 : AddCommMonoid W] →
                [inst_4 : Module A V] →
                  [inst_5 : Module A W] →
                    {ρ : Representation A G V} → {σ : Representation A G W} → ρ.IntertwiningMap σ → V →ₗ[A] W
-- Batteries.Util.ProofWanted
/-- File-local registry recording, for each wanted declaration, how many of its trailing binders
are auto-generated (chained `❰…❱` references and ambient `instance_wanted` includes) rather than
user-written. A `❰foo❱` reference uses this to tell `foo`'s user binders (which it re-quantifies)
apart from `foo`'s own dependency binders (which it surfaces onto the enclosing declaration; see
`classifyWantedRef`). Non-persistent across imports, like `wantedInstancesExt`.  -/
_private.Batteries.Util.ProofWanted.0.wantedArityExt : Lean.SimplePersistentEnvExtension (Lean.Name × ℕ) (Lean.NameMap ℕ)
-- Mathlib.Analysis.Complex.Basic
Complex.imCLM_coe : ↑Complex.imCLM = Complex.imLm
-- Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor
/-- `F.LeftLinear C` asserts that `F` is both lax and oplax left-linear,
in a compatible way, i.e that `μₗ` is inverse to `δₗ`.  -/
CategoryTheory.Functor.LeftLinear : {D : Type u_1} →
  {D' : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} D] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D'] →
        CategoryTheory.Functor D D' →
          (C : Type u_3) →
            [inst_2 : CategoryTheory.Category.{v_3, u_3} C] →
              [inst_3 : CategoryTheory.MonoidalCategory C] →
                [CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] →
                  [CategoryTheory.MonoidalCategory.MonoidalLeftAction C D'] → Type (max (max u_1 u_3) v_2)
-- Mathlib.FieldTheory.Galois.IsGaloisGroup
IsGaloisGroup.card_fixingSubgroup_eq_finrank : ∀ (G : Type u_1) (K : Type u_3) (L : Type u_4) [inst : Group G] [inst_1 : Field K] [inst_2 : Field L]
  [inst_3 : Algebra K L] [inst_4 : MulSemiringAction G L] (F : IntermediateField K L) [Finite G] [IsGaloisGroup G K L],
  Nat.card ↥(fixingSubgroup G ↑F) = Module.finrank (↥F) L
-- Mathlib.Algebra.MonoidAlgebra.Module
AddMonoidAlgebra.instIsTorsionFree : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : Module R S]
  [Module.IsTorsionFree R S], Module.IsTorsionFree R (AddMonoidAlgebra S M)
-- Mathlib.RingTheory.Extension.ExtendScalars
Algebra.Extension.extendScalars_algebra₂ : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : Algebra.Extension R S), P.extendScalars.algebra₂ = P.algebra₂
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.rescale_rescale : ∀ {R : Type u_1} [inst : CommSemiring R] (f : PowerSeries R) (a b : R),
  (PowerSeries.rescale b) ((PowerSeries.rescale a) f) = (PowerSeries.rescale (a * b)) f
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
CategoryTheory.Functor.biprodComparison_fst : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  (F : CategoryTheory.Functor C D) (X Y : C) [inst_4 : CategoryTheory.Limits.HasBinaryBiproduct X Y]
  [inst_5 : CategoryTheory.Limits.HasBinaryBiproduct (F.obj X) (F.obj Y)],
  CategoryTheory.CategoryStruct.comp (F.biprodComparison X Y) CategoryTheory.Limits.biprod.fst =
    F.map CategoryTheory.Limits.biprod.fst
-- Mathlib.Tactic.FunProp.Decl
Mathlib.Meta.FunProp.instBEqFunPropDecl : BEq Mathlib.Meta.FunProp.FunPropDecl
-- Lean.Elab.Tactic.Basic
Lean.Elab.Tactic.orElse : {α : Type} → Lean.Elab.Tactic.TacticM α → (Unit → Lean.Elab.Tactic.TacticM α) → Lean.Elab.Tactic.TacticM α
-- Lean.Elab.MutualInductive
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.FinalizeInductiveDecl.decl : Lean.Elab.Command.FinalizeInductiveDecl✝ → Lean.Declaration
-- Mathlib.CategoryTheory.Pi.Basic
/-- The natural isomorphism between
pulling back a grading along the identity function,
and the identity functor.  -/
CategoryTheory.Pi.comapId : (I : Type w₀) →
  (C : I → Type u₁) →
    [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] →
      CategoryTheory.Pi.comap C id ≅ CategoryTheory.Functor.id ((i : I) → C i)
-- Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
AddSubgroup.instVAdd : {G : Type u_2} → [inst : AddGroup G] → (H : AddSubgroup G) → VAdd (↥H.op) G
-- Mathlib.CategoryTheory.Category.ReflQuiv
CategoryTheory.ReflQuiv.instCoeSortType : CoeSort CategoryTheory.ReflQuiv (Type u)
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.span_idealLatticeBasis : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K]
  (I : (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K)ˣ),
  Submodule.span ℤ (Set.range ⇑(NumberField.mixedEmbedding.fractionalIdealLatticeBasis K I)) =
    NumberField.mixedEmbedding.idealLattice K I
-- Mathlib.Order.RelSeries
LTSeries.comap_length : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (p : LTSeries β) (f : α → β)
  (comap : ∀ ⦃x y : α⦄, f x < f y → x < y) (surjective : Function.Surjective f),
  (p.comap f comap surjective).length = p.length
-- Mathlib.AlgebraicGeometry.AffineSpace
AlgebraicGeometry.AffineSpace.of_mvPolynomial_int_ext : ∀ {n : Type u} {R : CommRingCat} {f g : CommRingCat.of (MvPolynomial n (ULift.{u_1, 0} ℤ)) ⟶ R},
  (∀ (i : n),
      (CategoryTheory.ConcreteCategory.hom f) (MvPolynomial.X i) =
        (CategoryTheory.ConcreteCategory.hom g) (MvPolynomial.X i)) →
    f = g
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.BraidedCategory.braiding_tensor_right_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X Y Z : C),
  (β_ X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)).hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β_ X Y).hom Z)
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Y X Z).hom
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y (β_ X Z).hom)
            (CategoryTheory.MonoidalCategoryStruct.associator Y Z X).inv)))
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
/-- A version of `Finset.sum_map` and `Finset.sum_image`, but we do not assume that `f` is
injective. Rather, we assume that the image of `f` on `I` only overlaps where `g (f i) = 0`.
The conclusion is the same as in `sum_image`.  -/
Finset.sum_image_of_pairwise_eq_zero : ∀ {ι : Type u_1} {κ : Type u_2} {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : DecidableEq ι] {f : κ → ι} {g : ι → M}
  {I : Finset κ}, ((↑I).Pairwise fun i j => f i = f j → g (f i) = 0) → ∑ s ∈ Finset.image f I, g s = ∑ i ∈ I, g (f i)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.ShiftLeft
Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftLeftConst.go_denote_mem_prefix : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} {assign : α → Bool} {inv : Bool} (aig : Std.Sat.AIG α)
  (distance : ℕ) (input : aig.RefVec w) (curr : ℕ) (hcurr : curr ≤ w) (s : aig.RefVec curr) (start : ℕ)
  (hstart : start < aig.decls.size),
  ⟦assign,
      { aig := (Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftLeftConst.go aig input distance curr hcurr s).aig,
        ref := { gate := start, invert := inv, hgate := ⋯ } }⟧ =
    ⟦assign, { aig := aig, ref := { gate := start, invert := inv, hgate := hstart } }⟧
-- Init.Data.BitVec.Lemmas
/-- The number of trailing zeroes is strictly less than the bitwidth iff the bitvector is nonzero.  -/
BitVec.ctz_lt_iff_ne_zero : ∀ {w : ℕ} {x : BitVec w}, x.ctz < ↑w ↔ x ≠ 0#w
-- Mathlib.Data.Finset.Powerset
/-- For predicate `p` decidable on subsets, it is decidable whether `p` holds for any subset.  -/
Finset.decidableExistsOfDecidableSubsets' : {α : Type u_1} → {s : Finset α} → {p : Finset α → Prop} → [(t : Finset α) → Decidable (p t)] → Decidable (∃ t ⊆ s, p t)
-- Mathlib.Algebra.Homology.Square
/-- The cokernel cofork attached to a commutative square in a preadditive category.  -/
CategoryTheory.Square.cokernelCofork : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      (sq : CategoryTheory.Square C) →
        [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct sq.X₂ sq.X₃] →
          CategoryTheory.Limits.CokernelCofork (CategoryTheory.Limits.biprod.lift sq.f₁₂ (-sq.f₁₃))
-- Mathlib.GroupTheory.QuotientGroup.Basic
/-- If the quotient by an additive subgroup gives a singleton then the additive
subgroup is the whole additive group.  -/
QuotientAddGroup.addSubgroup_eq_top_of_subsingleton : ∀ {G : Type u} [inst : AddGroup G] (H : AddSubgroup G), Subsingleton (G ⧸ H) → H = ⊤
-- Lean.Util.FoldConsts
/-- Return all names appearing in the type or value of a `ConstantInfo`.  -/
Lean.ConstantInfo.getUsedConstantsAsSet : Lean.ConstantInfo → Lean.NameSet
-- Mathlib.CategoryTheory.NatIso
CategoryTheory.Iso.app_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} (α : F ≅ G) (X : C), (α.app X).hom = α.hom.app X
-- Mathlib.Order.Sublocale
/-- The range of a nucleus is a sublocale.  -/
Nucleus.toSublocale : {X : Type u_1} → [inst : Order.Frame X] → Nucleus X → Sublocale X
-- Mathlib.Algebra.BigOperators.Finprod
finsum_mem_eq_sum_of_subset : ∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] (f : α → M) {s : Set α} {t : Finset α},
  s ∩ Function.support f ⊆ ↑t → ↑t ⊆ s → ∑ᶠ (i : α) (_ : i ∈ s), f i = ∑ i ∈ t, f i
-- Mathlib.Analysis.Normed.Group.Uniform
lipschitzWith_one_norm : ∀ {E : Type u_2} [inst : SeminormedAddGroup E], LipschitzWith 1 norm
-- Mathlib.Data.Fintype.Defs
Fintype.instFastSubsingleton : ∀ (α : Type u_4), Lean.Meta.FastSubsingleton (Fintype α)
-- Mathlib.Topology.Semicontinuity.Basic
lowerSemiContinuous_inv_iff : ∀ {α : Type u_4} [inst : TopologicalSpace α] {β : Type u_5} {f : α → β} [inst_1 : PartialOrder β] [inst_2 : CommGroup β]
  [IsOrderedMonoid β], LowerSemicontinuous f⁻¹ ↔ UpperSemicontinuous f
-- Mathlib.Analysis.Calculus.FDeriv.Basic
/-- `UniqueDiffWithinAt` achieves its goal: it implies the uniqueness of the derivative.  -/
UniqueDiffWithinAt.eq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] [ContinuousAdd E] [ContinuousSMul 𝕜 E] {F : Type u_3} [inst_6 : AddCommGroup F]
  [inst_7 : Module 𝕜 F] [inst_8 : TopologicalSpace F] [ContinuousAdd F] [ContinuousSMul 𝕜 F] {f : E → F}
  {f' f₁' : E →L[𝕜] F} {x : E} {s : Set E} [T2Space F],
  UniqueDiffWithinAt 𝕜 s x → HasFDerivWithinAt f f' s x → HasFDerivWithinAt f f₁' s x → f' = f₁'
-- Mathlib.Algebra.Polynomial.Module.AEval
Module.AEval.C_smul : ∀ {R : Type u_1} {A : Type u_3} {M : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] (a : A)
  [inst_2 : Algebra R A] [inst_3 : AddCommMonoid M] [inst_4 : Module A M] [inst_5 : Module R M]
  [inst_6 : IsScalarTower R A M] (t : R) (m : Module.AEval R M a), Polynomial.C t • m = t • m
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.homMk'_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T : D} {Y' : C} {S : CategoryTheory.Functor C D} (f : CategoryTheory.CostructuredArrow S T) (g : Y' ⟶ f.left),
  (f.homMk' g).right =
    CategoryTheory.CategoryStruct.id
      (CategoryTheory.CostructuredArrow.mk (CategoryTheory.CategoryStruct.comp (S.map g) f.hom)).right
-- Init.Data.List.MinMaxOn
_private.Init.Data.List.MinMaxOn.0.List.maxOn.eq_1 : ∀ {β : Type u_1} {α : Type u_2} [i : LE β] [inst : DecidableLE β] (f : α → β) (l : List α) (h : l ≠ []),
  List.maxOn f l h = List.minOn f l h
-- Mathlib.RingTheory.FreeRing
FreeRing.induction_on : ∀ {α : Type u} {C : FreeRing α → Prop} (z : FreeRing α),
  C (-1) →
    (∀ (b : α), C (FreeRing.of b)) →
      (∀ (x y : FreeRing α), C x → C y → C (x + y)) → (∀ (x y : FreeRing α), C x → C y → C (x * y)) → C z
-- Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy
HomotopicalAlgebra.Precylinder.LeftHomotopy.mk.injEq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} {P : HomotopicalAlgebra.Precylinder X} {Y : C}
  {f g : X ⟶ Y} (h : P.I ⟶ Y)
  (h₀ :
    autoParam (CategoryTheory.CategoryStruct.comp P.i₀ h = f) HomotopicalAlgebra.Precylinder.LeftHomotopy.h₀._autoParam)
  (h₁ :
    autoParam (CategoryTheory.CategoryStruct.comp P.i₁ h = g) HomotopicalAlgebra.Precylinder.LeftHomotopy.h₁._autoParam)
  (h_1 : P.I ⟶ Y)
  (h₀_1 :
    autoParam (CategoryTheory.CategoryStruct.comp P.i₀ h_1 = f)
      HomotopicalAlgebra.Precylinder.LeftHomotopy.h₀._autoParam)
  (h₁_1 :
    autoParam (CategoryTheory.CategoryStruct.comp P.i₁ h_1 = g)
      HomotopicalAlgebra.Precylinder.LeftHomotopy.h₁._autoParam),
  ({ h := h, h₀ := h₀, h₁ := h₁ } = { h := h_1, h₀ := h₀_1, h₁ := h₁_1 }) = (h = h_1)
-- Init.Tactics
/-- * `unfold id` unfolds all occurrences of definition `id` in the target.
* `unfold id1 id2 ...` is equivalent to `unfold id1; unfold id2; ...`.
* `unfold id at h` unfolds at the hypothesis `h`.

Definitions can be either global or local definitions.

For non-recursive global definitions, this tactic is identical to `delta`.
For recursive global definitions, it uses the "unfolding lemma" `id.eq_def`,
which is generated for each recursive definition, to unfold according to the recursive definition given by the user.
Only one level of unfolding is performed, in contrast to `simp only [id]`, which unfolds definition `id` recursively.
 -/
Lean.Parser.Tactic.unfold : Lean.ParserDescr
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.UnfoldLift.get : ∀ {m : Type u → Type v} {n : Type u → Type u_1} {σ : Type u} [inst : MonadLift m n] [inst_1 : MonadStateOf σ m],
  MonadStateOf.get = monadLift MonadStateOf.get
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.get!_min! : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.isEmpty = false → t.get! t.min! = t.min!
-- Mathlib.Data.Nat.PSub
Nat.psub.eq_2 : ∀ (m n : ℕ), m.psub n.succ = m.psub n >>= Nat.ppred
-- Mathlib.GroupTheory.GroupAction.Hom
/-- If `f` and `g` are equivariant maps, then so is `x ↦ (f x, g x)`.  -/
MulActionHom.prod : {M : Type u_1} →
  {N : Type u_2} →
    {α : Type u_3} →
      {γ : Type u_5} →
        {δ : Type u_6} →
          [inst : SMul M α] →
            [inst_1 : SMul N γ] → [inst_2 : SMul N δ] → {σ : M → N} → (α →ₑ[σ] γ) → (α →ₑ[σ] δ) → α →ₑ[σ] γ × δ
-- Init.Data.List.Lemmas
List.tail_replicate : ∀ {α : Type u_1} {n : ℕ} {a : α}, (List.replicate n a).tail = List.replicate (n - 1) a
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.map_one : ∀ {α β : Type u} (f : α → β), f <$> 1 = 1
-- Init.Data.Slice.Array.Lemmas
Subarray.toList_eq_drop_take : ∀ {α : Type u_1} {xs : Subarray α}, Std.Slice.toList xs = List.drop xs.start (List.take xs.stop xs.array.toList)
-- Mathlib.Tactic.Linarith.Datatypes
/-- `process pp l` runs `pp.transform` on `l` and returns the result,
tracing the result if `trace.linarith` is on.
 -/
Mathlib.Tactic.Linarith.GlobalBranchingPreprocessor.process : Mathlib.Tactic.Linarith.GlobalBranchingPreprocessor →
  Lean.MVarId → List Lean.Expr → Lean.MetaM (List Mathlib.Tactic.Linarith.Branch)
-- Mathlib.RingTheory.Coalgebra.Basic
/-- An arbitrarily chosen representation.  -/
Coalgebra.Repr.arbitrary : (R : Type u) →
  {A : Type v} →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid A] →
        [inst_2 : Module R A] → [inst_3 : CoalgebraStruct R A] → (a : A) → Coalgebra.Repr R a (A × A)
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
/-- A "canonical" structure map `𝟙_ V ⟶ F.obj (𝟙_ C)` that defines a natural transformation
`fromPUnit (𝟙_ V) ⟶ fromPUnit (𝟙_ C) ⋙ F`.  -/
CategoryTheory.MonoidalCategory.DayConvolutionUnit.can : {C : Type u₁} →
  {inst : CategoryTheory.Category.{v₁, u₁} C} →
    {V : Type u₂} →
      {inst_1 : CategoryTheory.Category.{v₂, u₂} V} →
        {inst_2 : CategoryTheory.MonoidalCategory C} →
          {inst_3 : CategoryTheory.MonoidalCategory V} →
            {F : CategoryTheory.Functor C V} →
              [self : CategoryTheory.MonoidalCategory.DayConvolutionUnit F] →
                CategoryTheory.MonoidalCategoryStruct.tensorUnit V ⟶
                  F.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
-- Mathlib.Algebra.Homology.ExactSequence
CategoryTheory.ShortComplex.mapToComposableArrows_app_0 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂),
  (CategoryTheory.ShortComplex.mapToComposableArrows φ).app 0 = φ.τ₁
-- Init.Data.String.Lemmas.Splits
String.Slice.splits_endPos_iff : ∀ {t₁ t₂ : String} {s : String.Slice}, s.endPos.Splits t₁ t₂ ↔ t₁ = s.copy ∧ t₂ = ""
-- Mathlib.Algebra.Ring.Ext
AddCommMonoidWithOne.toAddMonoidWithOne_injective : ∀ {R : Type u}, Function.Injective (@AddCommMonoidWithOne.toAddMonoidWithOne R)