mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValue!_eraseKey_self : ∀ {α : Type u} {β : Type v} [inst : BEq α] [PartialEquivBEq α] [inst_2 : Inhabited β] {l : List ((_ : α) × β)} {k : α},
  Std.Internal.List.DistinctKeys l → Std.Internal.List.getValue! k (Std.Internal.List.eraseKey k l) = default
-- Std.Time.Format.Modifier
Std.Time.instReprNumber : Repr Std.Time.Number
-- Lean.Structure
/-- Data for a structure field.
These are direct fields of a structure, including "subobject" fields for the embedded parents.
The full collection of fields is the transitive closure of fields through the subobject fields.
 -/
Lean.StructureFieldInfo : Type
-- Mathlib.Topology.Category.CompHausLike.Limits
CompHausLike.HasExplicitPullbacks.mk : ∀ {P : TopCat → Prop},
  (∀ {X Y B : CompHausLike P} (f : X ⟶ B) (g : Y ⟶ B), CompHausLike.HasExplicitPullback f g) →
    CompHausLike.HasExplicitPullbacks P
-- Init.Data.SInt.Lemmas
Int64.toBitVec_toInt8 : ∀ (x : Int64), x.toInt8.toBitVec = BitVec.signExtend 8 x.toBitVec
-- Mathlib.Control.ULiftable
ULiftable.down_up : ∀ {f : Type u₀ → Type u₁} {g : Type (max u₀ v₀) → Type v₁} [inst : ULiftable f g] {α : Type u₀} (x : f α),
  ULiftable.down (ULiftable.up x) = x
-- Mathlib.Data.Ordmap.Invariants
Ordnode.node3L.eq_1 : ∀ {α : Type u_1} (l : Ordnode α) (x : α) (m : Ordnode α) (y : α) (r : Ordnode α),
  l.node3L x m y r = (l.node' x m).node' y r
-- Mathlib.Topology.Sheaves.Presheaf
TopCat.Presheaf.restrict_restrict : ∀ {X : TopCat} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type u_2}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC]
  {F : TopCat.Presheaf C X} {U V W : TopologicalSpace.Opens ↑X} (e₁ : U ≤ V) (e₂ : V ≤ W)
  (x : CategoryTheory.ToType (F.obj (Opposite.op W))),
  TopCat.Presheaf.restrictOpen (TopCat.Presheaf.restrictOpen x V e₂) U e₁ = TopCat.Presheaf.restrictOpen x U ⋯
-- Std.Data.DHashMap.Internal.Model
/-- This is the general theorem used to show that access operations are correct.  -/
Std.DHashMap.Internal.apply_bucket : ∀ {α : Type u} {β : α → Type v} {γ : Type w} [inst : BEq α] [inst_1 : Hashable α] [PartialEquivBEq α] [LawfulHashable α]
  {m : Std.DHashMap.Internal.Raw₀ α β},
  Std.DHashMap.Internal.Raw.WFImp ↑m →
    ∀ {a : α} {f : Std.DHashMap.Internal.AssocList α β → γ} {g : List ((a : α) × β a) → γ},
      (∀ {l : Std.DHashMap.Internal.AssocList α β}, f l = g l.toList) →
        (∀ {l l' : List ((a : α) × β a)}, Std.Internal.List.DistinctKeys l → l.Perm l' → g l = g l') →
          (∀ {l l' : List ((a : α) × β a)}, Std.Internal.List.containsKey a l' = false → g (l ++ l') = g l) →
            f (Std.DHashMap.Internal.bucket (↑m).buckets ⋯ a) = g (Std.DHashMap.Internal.toListModel (↑m).buckets)
-- Mathlib.AlgebraicGeometry.Stalk
AlgebraicGeometry.Scheme.Opens.fromSpecStalkOfMem_toSpecΓ : ∀ {X : AlgebraicGeometry.Scheme} (U : X.Opens) (x : ↥X) (hxU : x ∈ U),
  CategoryTheory.CategoryStruct.comp (U.fromSpecStalkOfMem x hxU) U.toSpecΓ =
    AlgebraicGeometry.Spec.map (X.presheaf.germ U x hxU)
-- Std.Sync.Mutex
/-- `mutex.atomicallyOnce condvar pred k` runs `k`, waiting on `condvar` until `pred` returns true.
Both `k` and `pred` have access to the mutex's state.

Calling `mutex.atomicallyOnce` while already holding the underlying `BaseMutex` in the same thread
is undefined behavior. If this is unavoidable in your code, consider using `RecursiveMutex`.
 -/
Std.Mutex.atomicallyOnce : {m : Type → Type} →
  {α β : Type} →
    [Monad m] →
      [MonadLiftT BaseIO m] →
        [MonadFinally m] → Std.Mutex α → Std.Condvar → Std.AtomicT α m Bool → Std.AtomicT α m β → m β
-- Init.Sym.Lemmas
Lean.Sym.UInt64.lt_eq_false : ∀ (a b : UInt64), decide (a < b) = false → (a < b) = False
-- Mathlib.Analysis.Normed.Module.Alternating.Basic
ContinuousAlternatingMap.nnnorm_toContinuousMultilinearMap : ∀ {𝕜 : Type u} {E : Type wE} {F : Type wF} {ι : Type v} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : SeminormedAddCommGroup F]
  [inst_4 : NormedSpace 𝕜 F] [inst_5 : Fintype ι] (f : E [⋀^ι]→L[𝕜] F), ‖f.toContinuousMultilinearMap‖₊ = ‖f‖₊
-- Mathlib.Data.Real.ConjExponents
NNReal.HolderConjugate.conjExponent_eq : ∀ {p q : NNReal}, p.HolderConjugate q → p.conjExponent = q
-- Mathlib.LinearAlgebra.Finsupp.LinearCombination
Span.finsupp_linearCombination_repr : ∀ (R : Type u_1) {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {w : Set M}
  (x : ↥(Submodule.span R w)), (Finsupp.linearCombination R Subtype.val) (Span.repr R w x) = ↑x
-- Batteries.Data.Fin.Coding
Fin.decodeQuotient_encodeQuotient : ∀ {n : ℕ} (s : Setoid (Fin n)) [inst : DecidableRel ⇑s] (x : Quotient s),
  Fin.decodeQuotient s (Fin.encodeQuotient s x) = x
-- Mathlib.Probability.Kernel.Defs
/-- **Alias** of `FunLike.coe_add`. -/
ProbabilityTheory.Kernel.coe_add : ∀ {F : Type u_3} {α : Type u_5} {β : Type u_6} [inst : FunLike F α β] [inst_1 : Add F] [inst_2 : Add β]
  [IsAddApply F α β] (f g : F), ⇑(f + g) = ⇑f + ⇑g
-- Mathlib.NumberTheory.LSeries.Dirichlet
/-- The abscissa of (absolute) convergence of the constant sequence `1` is `1`.  -/
LSeries.abscissaOfAbsConv_one : LSeries.abscissaOfAbsConv 1 = 1
-- Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda
/-- The canonical map `colimit (pullback c.ι ((Functor.const J).map z)) ⟶ X`,
which is an isomorphism when `J` is filtered, see `isIso_f`.  -/
CategoryTheory.IsGrothendieckAbelian.IsPresentable.surjectivity.f : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      [inst_2 : CategoryTheory.IsGrothendieckAbelian.{w, v, u} C] →
        {X : C} →
          {J : Type w} →
            [inst_3 : CategoryTheory.SmallCategory J] →
              {Y : CategoryTheory.Functor J C} →
                {c : CategoryTheory.Limits.Cocone Y} →
                  (z : X ⟶ c.pt) →
                    CategoryTheory.Limits.colimit
                        (CategoryTheory.Limits.pullback c.ι ((CategoryTheory.Functor.const J).map z)) ⟶
                      X
-- Mathlib.Algebra.CharP.Subring
ExpChar.expChar_center_iff : ∀ {R : Type u} [inst : Ring R] {p : ℕ}, ExpChar (↥(Subring.center R)) p ↔ ExpChar R p
-- Mathlib.RingTheory.IsAdjoinRoot
/-- Auxiliary lemma for `apply_eq_lift`  -/
IsAdjoinRoot.apply_eq_lift : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] {f : Polynomial R} [inst_2 : Algebra R S]
  (h : IsAdjoinRoot S f) {T : Type u_1} [inst_3 : CommRing T] {i : R →+* T} {x : T} (hx : Polynomial.eval₂ i x f = 0)
  (g : S →+* T), (∀ (a : R), g ((algebraMap R S) a) = i a) → g h.root = x → ∀ (a : S), g a = (h.lift i x hx) a
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
ENNReal.add_rpow_le_two_rpow_mul_rpow_add_rpow : ∀ {p : ℝ} (a b : ENNReal), 0 ≤ p → (a + b) ^ p ≤ 2 ^ p * (a ^ p + b ^ p)
-- Lean.Meta.Tactic.Grind.Types
/-- Trace information for a case split.  -/
Lean.Meta.Grind.CaseTrace : Type
-- Lean.Elab.Tactic.SolveByElim
/-- Allow elaboration of `Config` arguments to tactics.

Note: does not generate a `(config := ...)` option due to the fields in the `omit`
clause, which are all function-valued and have no `EvalExpr` instances.
 -/
Lean.Elab.Tactic.SolveByElim.elabConfig : Lean.Syntax →
  optParam Lean.Meta.SolveByElim.SolveByElimConfig { } →
    optParam Bool true → Lean.Elab.Tactic.TacticM Lean.Meta.SolveByElim.SolveByElimConfig
-- Mathlib.Analysis.Normed.Group.Uniform
Real.isClosedEmbedding_intCast : Topology.IsClosedEmbedding Int.cast
-- Lean.Elab.Tactic.Simp
_private.Lean.Elab.Tactic.Simp.0.Lean.Elab.Tactic.simpLocation.go : Lean.Meta.Simp.Context →
  Lean.Meta.Simp.SimprocsArray →
    Option Lean.Meta.Simp.Discharge → Array Lean.FVarId → Bool → Lean.Elab.Tactic.TacticM Lean.Meta.Simp.Stats
-- Lean.Util.ParamMinimizer
/-- Initial parameter selection  -/
_private.Lean.Util.ParamMinimizer.0.Lean.Util.ParamMinimizer.Context.initialMask : {m : Type → Type} → Lean.Util.ParamMinimizer.Context✝ m → Array Bool
-- Mathlib.CategoryTheory.FiberedCategory.HomLift
/-- Given a morphism `f : R ⟶ S`, and an isomorphism `φ : a ≅ b` lifting `f`, `isoOfIsoLift f φ` is
the isomorphism `Φ : R ≅ S` with `Φ.hom = f` induced from `φ`  -/
CategoryTheory.IsHomLift.isoOfIsoLift : {𝒮 : Type u₁} →
  {𝒳 : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₂} 𝒳] →
      [inst_1 : CategoryTheory.Category.{v₂, u₁} 𝒮] →
        (p : CategoryTheory.Functor 𝒳 𝒮) →
          {R S : 𝒮} → {a b : 𝒳} → (f : R ⟶ S) → (φ : a ≅ b) → [p.IsHomLift f φ.hom] → R ≅ S
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.EqCnstrProof.simp_prefix.inj : ∀ {lhs : Bool} {s : Lean.Grind.AC.Seq} {c₁ c₂ : Lean.Meta.Grind.AC.EqCnstr} {lhs_1 : Bool} {s_1 : Lean.Grind.AC.Seq}
  {c₁_1 c₂_1 : Lean.Meta.Grind.AC.EqCnstr},
  Lean.Meta.Grind.AC.EqCnstrProof.simp_prefix lhs s c₁ c₂ =
      Lean.Meta.Grind.AC.EqCnstrProof.simp_prefix lhs_1 s_1 c₁_1 c₂_1 →
    lhs = lhs_1 ∧ s = s_1 ∧ c₁ = c₁_1 ∧ c₂ = c₂_1
-- Init.Data.String.Defs
String.Pos.Raw.isValid_zero : ∀ {s : String}, String.Pos.Raw.IsValid s 0
-- Mathlib.Topology.Sober
IsGenericPoint.inseparable : ∀ {α : Type u_1} [inst : TopologicalSpace α] {x y : α} {S : Set α},
  IsGenericPoint x S → IsGenericPoint y S → Inseparable x y
-- Init.Data.Nat.Basic
Nat.one_lt_two : 1 < 2
-- Mathlib.Computability.NFA
/-- Set of states visited by a path.  -/
NFA.Path.supp : {α : Type u} → {σ : Type v} → {M : NFA α σ} → [DecidableEq σ] → {s t : σ} → {x : List α} → M.Path s t x → Finset σ
-- Init.Data.Order.MinMaxOn
minOn_eq_if : ∀ {β : Type u_1} {α : Sort u_2} [inst : LE β] [inst_1 : DecidableLE β] {f : α → β} {a b : α},
  minOn f a b = if f a ≤ f b then a else b
-- Init.Data.List.SplitOn.Basic
_private.Init.Data.List.SplitOn.Basic.0.List.splitOnPPrepend.eq_def : ∀ {α : Type u_1} (p : α → Bool) (x x_1 : List α),
  List.splitOnPPrepend p x x_1 =
    match x, x_1 with
    | [], acc => [acc.reverse]
    | a :: t, acc =>
      if p a = true then acc.reverse :: List.splitOnPPrepend p t [] else List.splitOnPPrepend p t (a :: acc)
-- Mathlib.SetTheory.Cardinal.ENat
Cardinal.lift_ofENat : ∀ (m : ℕ∞), Cardinal.lift.{u, v} ↑m = ↑m
-- Mathlib.Order.Filter.Map
Filter.map_comap_of_mem : ∀ {α : Type u_1} {β : Type u_2} {f : Filter β} {m : α → β}, Set.range m ∈ f → Filter.map m (Filter.comap m f) = f
-- Init.Data.List.Perm
List.not_perm_cons_nil : ∀ {α : Type u_1} {l : List α} {a : α}, ¬(a :: l).Perm []
-- Mathlib.Algebra.Category.CoalgCat.Basic
/-- The underlying `CoalgHom`  -/
CoalgCat.Hom.toCoalgHom' : {R : Type u} → [inst : CommRing R] → {V W : CoalgCat R} → V.Hom W → ↑V.toModuleCat →ₗc[R] ↑W.toModuleCat
-- Mathlib.Data.Matrix.Diagonal
Matrix.diagonal_zero' : ∀ {n : Type u_3} {α : Type v} [inst : DecidableEq n] [inst_1 : Zero α], Matrix.diagonal 0 = 0
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.LeftExtension.precomp_obj_left : ∀ {C : Type u_1} {C' : Type u_2} {H : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C'] [inst_2 : CategoryTheory.Category.{v_3, u_3} H]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D] (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H)
  (G : CategoryTheory.Functor C' C)
  (X : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit F) ((CategoryTheory.Functor.whiskeringLeft C D H).obj L)),
  ((CategoryTheory.Functor.LeftExtension.precomp L F G).obj X).left = X.left
-- Mathlib.NumberTheory.Padics.Complex
PadicComplex.coe_zero : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)], ↑0 = 0
-- Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
HomotopyCategory.mappingCone_triangleh_distinguished : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] [inst_3 : CategoryTheory.Limits.HasZeroObject C]
  {X Y : CochainComplex C ℤ} (f : X ⟶ Y),
  CochainComplex.mappingCone.triangleh f ∈ CategoryTheory.Pretriangulated.distinguishedTriangles
-- Lean.Server.FileSource
Lean.Lsp.instFileSourcePlainGoalParams : Lean.Lsp.FileSource Lean.Lsp.PlainGoalParams
-- Mathlib.RingTheory.KrullDimension.Polynomial
/-- Let `p` be a maximal ideal of `A`. If `P` is a maximal ideal of `A[X]` lying above `p`,
then `ht(P) = ht(p) + 1`.
See `Polynomial.height_eq_height_add_one` for the more general version that does not assume `p` is
maximal.
 -/
_private.Mathlib.RingTheory.KrullDimension.Polynomial.0.Polynomial.height_eq_height_add_one_of_isMaximal : ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] (p : Ideal R) [p.IsMaximal] (P : Ideal (Polynomial R))
  [P.IsMaximal] [P.LiesOver p], P.height = p.height + 1
-- Mathlib.Algebra.Group.Submonoid.MulOpposite
Submonoid.unop_top : ∀ {M : Type u_2} [inst : MulOneClass M], ⊤.unop = ⊤
-- Mathlib.Algebra.Homology.Embedding.CochainComplex
CochainComplex.isStrictlyLE_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : CochainComplex C ℤ) (n : ℤ), K.IsStrictlyLE n ↔ ∀ (i : ℤ), n < i → CategoryTheory.Limits.IsZero (K.X i)
-- Mathlib.Tactic.Translate.ToAdditive
/-- Dictionary used by `guessName` to autogenerate names.
This only transforms single name components, unlike `abbreviationDict`.

Note: `guessName` capitalizes the output according to the capitalization of the input.
In order for this to work, the input should always start with a lower case letter, and the output
should always start with an upper case letter.
 -/
Mathlib.Tactic.ToAdditive.nameDict : Std.HashMap String (List String)
-- Lean.Elab.MutualDef
/-- Eagerly convert universe metavariables occurring in theorem headers to universe parameters.  -/
_private.Lean.Elab.MutualDef.0.Lean.Elab.Term.levelMVarToParamHeaders : Array Lean.Elab.DefView → Array Lean.Elab.DefViewElabHeader → Lean.Elab.TermElabM (Array Lean.Elab.DefViewElabHeader)
-- Mathlib.Order.Lex
instUniqueLex : (α : Type u_2) → [Unique α] → Unique (Lex α)
-- Mathlib.Topology.Constructions.SumProd
Topology.IsOpenEmbedding.prodMap : ∀ {X : Type u} {Y : Type v} {W : Type u_1} {Z : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] [inst_3 : TopologicalSpace W] {f : X → Y} {g : Z → W},
  Topology.IsOpenEmbedding f → Topology.IsOpenEmbedding g → Topology.IsOpenEmbedding (Prod.map f g)
-- Mathlib.Tactic.FunProp.Core
/-- Try to remove applied argument i.e. prove `P (fun x ↦ f x y)` from `P (fun x ↦ f x)`.

For example
- `funPropDecl` is `FunPropDecl` for `Continuous`
- `e = q(Continuous fun x ↦ foo (bar x) y)`
- `fData` contains info on `fun x ↦ foo (bar x) y`

This tries to prove `Continuous fun x ↦ foo (bar x) y` from `Continuous fun x ↦ foo (bar x)`
 -/
Mathlib.Meta.FunProp.removeArgRule : Mathlib.Meta.FunProp.FunPropDecl →
  Lean.Expr →
    Mathlib.Meta.FunProp.FunctionData →
      (Lean.Expr → Mathlib.Meta.FunProp.FunPropM (Option Mathlib.Meta.FunProp.Result)) →
        Mathlib.Meta.FunProp.FunPropM (Option Mathlib.Meta.FunProp.Result)
-- Init.Data.SInt.Lemmas
Int16.toInt_toInt8 : ∀ (x : Int16), x.toInt8.toInt = x.toInt.bmod (2 ^ 8)
-- Mathlib.Order.LiminfLimsup
Filter.liminf_sup_filter : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteDistribLattice α] {f : Filter β} {u : β → α} {g : Filter β},
  Filter.liminf u (f ⊔ g) = Filter.liminf u f ⊓ Filter.liminf u g
-- Init.Data.Nat.Bitwise.Lemmas
Nat.instCommutativeHAnd : Std.Commutative fun x1 x2 => x1 &&& x2
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.inv_def : ∀ {G : Type u_1} {H : Type u_2} [inst : Group G] [inst_1 : Group H] (w : FreeMonoid (G ⊕ H)),
  (Monoid.Coprod.mk w)⁻¹ =
    Monoid.Coprod.mk (FreeMonoid.ofList (List.map (Sum.map Inv.inv Inv.inv) (FreeMonoid.toList w)).reverse)
-- Mathlib.Algebra.Module.Torsion.Free
Subsingleton.to_moduleIsTorsionFree : ∀ {R : Type u_1} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Subsingleton M],
  Module.IsTorsionFree R M
-- Mathlib.CategoryTheory.ExtremalEpi
CategoryTheory.extremalEpi_iff_strongEpi_of_hasPullbacks : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasPullbacks C],
  CategoryTheory.ExtremalEpi f ↔ CategoryTheory.StrongEpi f
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.throw_MonadExcept : ∀ {m : Type u → Type v} {Pred EPred : Type u} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] {ε : Type u_1} {α : Type u}
  {post : α → Pred} {epost : EPred} [inst_4 : MonadExceptOf ε m] (err : ε),
  ⦃ Std.Internal.Do.wp (MonadExceptOf.throw err) post epost ⦄ throw err ⦃ post; epost ⦄
-- Mathlib.Order.Lattice
/-- Pointwise minimum of two monotone functions is a monotone function.  -/
MonotoneOn.min : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : LinearOrder β] {f g : α → β} {s : Set α},
  MonotoneOn f s → MonotoneOn g s → MonotoneOn (fun x => min (f x) (g x)) s
-- Mathlib.LinearAlgebra.Matrix.Kronecker
Matrix.kronecker_diagonal : ∀ {α : Type u_3} {l : Type u_9} {m : Type u_10} {n : Type u_11} [inst : MulZeroClass α] [inst_1 : DecidableEq n]
  (A : Matrix l m α) (b : n → α),
  Matrix.kroneckerMap (fun x1 x2 => x1 * x2) A (Matrix.diagonal b) =
    Matrix.blockDiagonal fun i => MulOpposite.op (b i) • A
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.addTermInfo' : Lean.Syntax →
  Lean.Expr →
    optParam (Option Lean.Expr) none →
      optParam (Option Lean.LocalContext) none →
        optParam Lean.Name Lean.Name.anonymous → optParam Bool false → optParam Bool false → Lean.Elab.TermElabM Unit
-- Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
integral_cexp_quadratic : ∀ {b : ℂ},
  b.re < 0 →
    ∀ (c d : ℂ),
      ∫ (x : ℝ), Complex.exp (b * ↑x ^ 2 + c * ↑x + d) = (↑Real.pi / -b) ^ (1 / 2) * Complex.exp (d - c ^ 2 / (4 * b))
-- Mathlib.RepresentationTheory.Homological.Resolution
HomotopyEquiv.ofIso.eq_1 : ∀ {ι : Type u_2} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} {C D : HomologicalComplex V c} (f : C ≅ D),
  HomotopyEquiv.ofIso f =
    { hom := f.hom, inv := f.inv, homotopyHomInvId := Homotopy.ofEq ⋯, homotopyInvHomId := Homotopy.ofEq ⋯ }
-- Mathlib.NumberTheory.LSeries.ZMod
/-- Special case of `differentiableAt_completedLFunction` asserting differentiability everywhere
under suitable hypotheses.
 -/
ZMod.differentiable_completedLFunction : ∀ {N : ℕ} [inst : NeZero N] {Φ : ZMod N → ℂ}, Φ 0 = 0 → ∑ j, Φ j = 0 → Differentiable ℂ (ZMod.completedLFunction Φ)
-- Lean.Meta.Tactic.Grind.Util
/-- Clears auxiliary **and** implementation detail decls used to encode recursive declarations and
implementation details.
- `grind` eliminates auxiliary declarations to ensure they are not accidentally used by its proof automation.
- `grind` eliminates implementation detail declarations because they have a support role.
 -/
Lean.MVarId.clearImplDetails : Lean.MVarId → Lean.MetaM Lean.MVarId
-- Mathlib.Data.Real.ConjExponents
ENNReal.conjExponent.eq_1 : ∀ (p : ENNReal), p.conjExponent = 1 + (p - 1)⁻¹
-- Mathlib.Analysis.SpecialFunctions.Sigmoid
AnalyticAt.sigmoid : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {x : E},
  AnalyticAt ℝ f x → AnalyticAt ℝ (Real.sigmoid ∘ f) x
-- Mathlib.Combinatorics.Enumerative.Partition.Basic
Nat.Partition.ofSums.congr_simp : ∀ (n : ℕ) (l l_1 : Multiset ℕ) (e_l : l = l_1) (hl : l.sum = n),
  Nat.Partition.ofSums n l hl = Nat.Partition.ofSums n l_1 ⋯
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.Formula.realize_imp : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} {φ ψ : L.Formula α} {v : α → M},
  (φ.imp ψ).Realize v ↔ φ.Realize v → ψ.Realize v
-- Init.Grind.Module.Envelope
Lean.Grind.IntModule.OfNatModule.toQ_zero : ∀ {α : Type u} [inst : Lean.Grind.NatModule α], Lean.Grind.IntModule.OfNatModule.toQ 0 = 0
-- Mathlib.MeasureTheory.Measure.Prod
MeasureTheory.Measure.prod.instIsFiniteMeasure : ∀ {α : Type u_4} {β : Type u_5} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (μ : MeasureTheory.Measure α)
  (ν : MeasureTheory.Measure β) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν],
  MeasureTheory.IsFiniteMeasure (μ.prod ν)
-- Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
ContinuousLinearMap.integral_comp_comm : ∀ {X : Type u_1} {E : Type u_3} {Fₗ : Type u_5} [inst : MeasurableSpace X] {μ : MeasureTheory.Measure X} {𝕜 : Type u_6}
  [inst_1 : RCLike 𝕜] [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedAddCommGroup Fₗ]
  [inst_5 : NormedSpace 𝕜 Fₗ] [inst_6 : NormedSpace ℝ Fₗ] [CompleteSpace Fₗ] [inst_8 : NormedSpace ℝ E]
  [CompleteSpace E] (L : E →L[𝕜] Fₗ) {φ : X → E},
  MeasureTheory.Integrable φ μ → ∫ (x : X), L (φ x) ∂μ = L (∫ (x : X), φ x ∂μ)
-- Lean.Meta.Tactic.Grind.Types
/-- For each equality `b = c` in `parents`, executes `k b c` IF
- `b = c` is equal to `False`, and
 -/
Lean.Meta.Grind.forEachDiseq : Lean.Meta.Grind.ParentSet → (Lean.Expr → Lean.Expr → Lean.Meta.Grind.GoalM Unit) → Lean.Meta.Grind.GoalM Unit
-- Init.Sym.Lemmas
Lean.Sym.Int16.eq_eq_false : ∀ (a b : Int16), decide (a = b) = false → (a = b) = False
-- Mathlib.CategoryTheory.Adjunction.Triple
/-- For an adjoint triple `F ⊣ G ⊣ H` where `F` and `H` are fully faithful, the components of the
natural transformation `F ⟶ H` at `G` are precisely the components of the natural transformation
`G ⋙ F ⟶ G ⋙ H` obtained from the units and counits of the adjunctions.  -/
CategoryTheory.Adjunction.Triple.leftToRight_app_obj : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  {H : CategoryTheory.Functor C D} (t : CategoryTheory.Adjunction.Triple F G H) [inst_2 : F.Full] [inst_3 : F.Faithful]
  {X : D}, t.leftToRight.app (G.obj X) = CategoryTheory.CategoryStruct.comp (t.adj₁.counit.app X) (t.adj₂.unit.app X)
-- Mathlib.Topology.Order
TopologicalSpace.isOpen_top_iff : ∀ {α : Type u_2} (U : Set α), IsOpen U ↔ U = ∅ ∨ U = Set.univ
-- Mathlib.Analysis.Complex.Trigonometric
Real.abs_cos_le_one : ∀ (x : ℝ), |Real.cos x| ≤ 1
-- Lean.Data.PersistentArray
Lean.PersistentArray.allM : {α : Type u} → {m : Type → Type w} → [Monad m] → Lean.PersistentArray α → (α → m Bool) → m Bool
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.revMatchAt?.fun_cases_unfolding : ∀ {ρ : Type} (pat : ρ) [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice} (endPos : s.Pos)
  (motive : Option s.Pos → Prop),
  (∀ (h : ∃ startPos, String.Slice.Pattern.Model.IsLongestRevMatchAt pat startPos endPos), motive (some h.choose)) →
    ((¬∃ startPos, String.Slice.Pattern.Model.IsLongestRevMatchAt pat startPos endPos) → motive none) →
      motive (String.Slice.Pattern.Model.revMatchAt? pat endPos)
-- Mathlib.Analysis.Convex.AmpleSet
/-- A set is ample iff its image under a continuous affine equivalence is.  -/
AmpleSet.image_iff : ∀ {F : Type u_1} [inst : AddCommGroup F] [inst_1 : Module ℝ F] [inst_2 : TopologicalSpace F] {E : Type u_2}
  [inst_3 : AddCommGroup E] [inst_4 : Module ℝ E] [inst_5 : TopologicalSpace E] {s : Set E} (L : E ≃ᴬ[ℝ] F),
  AmpleSet (⇑L '' s) ↔ AmpleSet s
-- Mathlib.Analysis.Analytic.Constructions
/-- Multiplication of analytic functions (valued in a normed `𝕜`-algebra) is analytic.  -/
AnalyticOn.mul : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {A : Type u_7} [inst_3 : NormedRing A] [inst_4 : NormedAlgebra 𝕜 A] {f g : E → A}
  {s : Set E}, AnalyticOn 𝕜 f s → AnalyticOn 𝕜 g s → AnalyticOn 𝕜 (fun x => f x * g x) s
-- Mathlib.Algebra.Homology.LocalCohomology
/-- The directed system of `R`-modules of the form `R/J`, where `J` is an ideal of `R`,
determined by the functor `I`  -/
localCohomology.ringModIdeals : {R : Type u} →
  [inst : CommRing R] →
    {D : Type v} →
      [inst_1 : CategoryTheory.SmallCategory D] →
        CategoryTheory.Functor D (Ideal R) → CategoryTheory.Functor D (ModuleCat R)