mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.InnerProductSpace.Calculus
ContDiffAt.dist : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [InnerProductSpace 𝕜 E]
  [inst : NormedSpace ℝ E] {G : Type u_4} [inst_2 : NormedAddCommGroup G] [inst_3 : NormedSpace ℝ G] {f g : G → E}
  {x : G} {n : WithTop ℕ∞},
  ContDiffAt ℝ n f x → ContDiffAt ℝ n g x → f x ≠ g x → ContDiffAt ℝ n (fun y => dist (f y) (g y)) x
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.HasSeparator.hasDetector : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Balanced C] [CategoryTheory.HasSeparator C],
  CategoryTheory.HasDetector C
-- Mathlib.Algebra.Group.Fin.Tuple
Matrix.head_zero : ∀ {α : Type u_1} {n : ℕ} [inst : Zero α], Matrix.vecHead 0 = 0
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.trim_measurableSet_eq : ∀ {α : Type u_1} {m : MeasurableSpace α} {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M]
  {n : MeasurableSpace α} {v : MeasureTheory.VectorMeasure α M} (hle : m ≤ n) {i : Set α},
  MeasurableSet i → (v.trim hle) i = v i
-- Mathlib.CategoryTheory.Monoidal.DayConvolution.DayFunctor
CategoryTheory.MonoidalCategory.DayFunctor.Hom.mk.inj : ∀ {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 G : CategoryTheory.MonoidalCategory.DayFunctor C V} {natTrans natTrans_1 : F.functor ⟶ G.functor},
  { natTrans := natTrans } = { natTrans := natTrans_1 } → natTrans = natTrans_1
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.DiseqCnstrProof.core.injEq : ∀ (a b : Lean.Expr) (ea eb : Lean.Grind.AC.Expr) (a_1 b_1 : Lean.Expr) (ea_1 eb_1 : Lean.Grind.AC.Expr),
  (Lean.Meta.Grind.AC.DiseqCnstrProof.core a b ea eb = Lean.Meta.Grind.AC.DiseqCnstrProof.core a_1 b_1 ea_1 eb_1) =
    (a = a_1 ∧ b = b_1 ∧ ea = ea_1 ∧ eb = eb_1)
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
_private.Mathlib.Algebra.BigOperators.Group.Finset.Defs.0.BigOperators.FinsetResult.finset : Lean.Term → BigOperators.FinsetResult✝
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKey!_ofList_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} [EquivBEq α] [LawfulHashable α] [inst : Inhabited α]
  {l : List ((a : α) × β a)} {k : α},
  (List.map Sigma.fst l).contains k = false → (Std.DHashMap.ofList l).getKey! k = default
-- Lean.Meta.Basic
/-- Create a constant with the given name and new universe metavariables.
Example: ``mkConstWithFreshMVarLevels `Monad`` returns `@Monad.{?u, ?v}`
 -/
Lean.Meta.mkConstWithFreshMVarLevels : Lean.Name → Lean.MetaM Lean.Expr
-- Mathlib.Topology.UniformSpace.Cauchy
cauchy_iff_exists_le_nhds : ∀ {α : Type u} [uniformSpace : UniformSpace α] [CompleteSpace α] {l : Filter α} [l.NeBot], Cauchy l ↔ ∃ x, l ≤ nhds x
-- Mathlib.Order.Hom.Basic
OrderIso.map_top' : ∀ {α : Type u_2} {β : Type u_3} [inst : LE α] [inst_1 : PartialOrder β] (f : α ≃o β) {x : α} {y : β},
  (∀ (x' : α), x' ≤ x) → (∀ (y' : β), y' ≤ y) → f x = y
-- Mathlib.Probability.Martingale.Basic
MeasureTheory.Submartingale.add : ∀ {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [inst : Preorder ι] {m0 : MeasurableSpace Ω}
  {μ : MeasureTheory.Measure Ω} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E] {f g : ι → Ω → E}
  {ℱ : MeasureTheory.Filtration ι m0} [CompleteSpace E] [inst_4 : Preorder E] [AddLeftMono E],
  MeasureTheory.Submartingale f ℱ μ → MeasureTheory.Submartingale g ℱ μ → MeasureTheory.Submartingale (f + g) ℱ μ
-- Init.Data.Repr
/-- Turns `a` into a `Format` using its `Repr` instance, with the precedence level set to that of
function application.

Together with `Repr.addAppParen`, this can be used to correctly parenthesize function application
syntax.
 -/
reprArg : {α : Type u_1} → [Repr α] → α → Std.Format
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
lt_mul_of_lt_mul_right : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Preorder α] [MulRightMono α] {a b c d : α}, a < b * c → b ≤ d → a < d * c
-- Batteries.Tactic.Lint.Simp
/-- Runs the continuation on all the simp theorems encoded in the given type.  -/
Batteries.Tactic.Lint.withSimpTheoremInfos : {α : Type} → Lean.Expr → (Batteries.Tactic.Lint.SimpTheoremInfo → Lean.MetaM α) → Lean.MetaM (Array α)
-- Mathlib.Logic.Equiv.Defs
/-- Two empty types are equivalent.  -/
Equiv.equivOfIsEmpty : (α : Sort u_1) → (β : Sort u_2) → [IsEmpty α] → [IsEmpty β] → α ≃ β
-- Aesop.Nanos
Aesop.Nanos : Type
-- Mathlib.LinearAlgebra.CliffordAlgebra.Star
CliffordAlgebra.star_ι : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} (m : M), star ((CliffordAlgebra.ι Q) m) = -(CliffordAlgebra.ι Q) m
-- Mathlib.GroupTheory.Congruence.Defs
/-- The quotient of a monoid by a congruence relation is a monoid.  -/
Con.monoid : {M : Type u_4} → [inst : Monoid M] → (c : Con M) → Monoid c.Quotient
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.invVeblen₂_of_lt_opow : ∀ {a : Ordinal.{u}}, a < Ordinal.omega0 ^ a → a.invVeblen₂ = a
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.getD_insertMany_list_of_not_mem_of_mem : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α],
  m.WF →
    ∀ {l : List α} {k k' fallback : α},
      (k == k') = true →
        k ∉ m → List.Pairwise (fun a b => (a == b) = false) l → k ∈ l → (m.insertMany l).getD k' fallback = k
-- Mathlib.CategoryTheory.Sigma.Basic
CategoryTheory.Sigma.SigmaHom.comp_def : ∀ {I : Type w₁} {C : I → Type u₁} [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] (i : I) (X Y Z : C i)
  (f : X ⟶ Y) (g : Y ⟶ Z),
  (CategoryTheory.Sigma.SigmaHom.mk f).comp (CategoryTheory.Sigma.SigmaHom.mk g) =
    CategoryTheory.Sigma.SigmaHom.mk (CategoryTheory.CategoryStruct.comp f g)
-- Mathlib.Data.Nat.Bits
Nat.one_bits : Nat.bits 1 = [true]
-- Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
AlgebraicGeometry.Scheme.AffineZariskiSite.instPreorder : {X : AlgebraicGeometry.Scheme} → Preorder X.AffineZariskiSite
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.SplitSource.ext.inj : ∀ {declName declName_1 : Lean.Name},
  Lean.Meta.Grind.SplitSource.ext declName = Lean.Meta.Grind.SplitSource.ext declName_1 → declName = declName_1
-- Init.Data.List.Control
_private.Init.Data.List.Control.0.List.findSomeM?.eq_def : ∀ {m : Type u → Type v} [inst : Monad m] {α : Type w} {β : Type u} (f : α → m (Option β)) (x : List α),
  List.findSomeM? f x =
    match x with
    | [] => pure none
    | a :: as => do
      let __do_lift ← f a
      match __do_lift with
        | some b => pure (some b)
        | none => List.findSomeM? f as
-- Mathlib.Algebra.Module.Equiv.Basic
LinearEquiv.coe_toLinearMap_mul : ∀ {R : Type u_1} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {e₁ e₂ : M ≃ₗ[R] M}, ↑(e₁ * e₂) = ↑e₁ * ↑e₂
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.IsMonHom.monoidHom_comp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {M N O X : C} [inst_2 : CategoryTheory.MonObj M] [inst_3 : CategoryTheory.MonObj N] [inst_4 : CategoryTheory.MonObj O]
  (f : M ⟶ N) (g : N ⟶ O) [inst_5 : CategoryTheory.IsMonHom f] [inst_6 : CategoryTheory.IsMonHom g],
  CategoryTheory.IsMonHom.monoidHom (CategoryTheory.CategoryStruct.comp f g) X =
    (CategoryTheory.IsMonHom.monoidHom g X).comp (CategoryTheory.IsMonHom.monoidHom f X)
-- Mathlib.GroupTheory.QuotientGroup.ModEq
AddCommGroup.modEq_iff_eq_mod_zmultiples : ∀ {G : Type u_1} [inst : AddCommGroup G] {a b p : G}, a ≡ b [PMOD p] ↔ ↑a = ↑b
-- Mathlib.Order.Filter.AtTopBot.CountablyGenerated
OrderDual.instIsCountablyGeneratedAtTop : ∀ {α : Type u_1} [inst : Preorder α] [Filter.atBot.IsCountablyGenerated], Filter.atTop.IsCountablyGenerated
-- Mathlib.Algebra.Group.Equiv.TypeTags
AddEquiv.toMultiplicativeLeft_apply_symm_apply : ∀ {G : Type u_2} {H : Type u_3} [inst : AddZeroClass G] [inst_1 : MulOneClass H] (f : G ≃+ Additive H) (a : H),
  (AddEquiv.toMultiplicativeLeft f).symm a = (AddMonoidHom.toMultiplicativeRight f.symm.toAddMonoidHom) a
-- Mathlib.Geometry.RingedSpace.SheafedSpace
AlgebraicGeometry.SheafedSpace.coeSort : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → CoeSort (AlgebraicGeometry.SheafedSpace C) (Type u_1)
-- Mathlib.NumberTheory.Divisors
Int.ne_zero_of_mem_divisors : ∀ {x z : ℤ}, x ∈ z.divisors → z ≠ 0
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- Construct the `NormalizedHom.nil` term in `m`.  -/
Mathlib.Tactic.BicategoryLike.normalizedHom.nilM : {m : Type → Type} →
  [Monad m] →
    [Mathlib.Tactic.BicategoryLike.MonadMor₁ m] →
      Mathlib.Tactic.BicategoryLike.Obj → m Mathlib.Tactic.BicategoryLike.NormalizedHom
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.intCast_eq_denoteInt : ∀ {α : Type u_1} [inst : Lean.Grind.Field α] (b : ℤ), IntCast.intCast b = Lean.Grind.CommRing.denoteInt b
-- Mathlib.Algebra.Homology.ShortComplex.Basic
CategoryTheory.ShortComplex.Hom.id_τ₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C), (CategoryTheory.ShortComplex.Hom.id S).τ₁ = CategoryTheory.CategoryStruct.id S.X₁
-- Init.Data.UInt.Lemmas
USize.mul_sub : ∀ {a b c : USize}, a * (b - c) = a * b - a * c
-- Mathlib.Order.Basic
compl_ge : ∀ {α : Type u_2} [inst : LinearOrder α], (fun x1 x2 => x1 ≥ x2)ᶜ = fun x1 x2 => x1 < x2
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
rootsOfUnityEquivOfPrimitiveRoots_symm_apply : ∀ {R : Type u_4} [inst : CommRing R] [inst_1 : IsDomain R] {S : Type u_7} {F : Type u_8} [inst_2 : CommRing S]
  [inst_3 : IsDomain S] [inst_4 : FunLike F R S] [inst_5 : MonoidHomClass F R S] {n : ℕ} [inst_6 : NeZero n] {f : F}
  (hf : Function.Injective ⇑f) (hζ : (primitiveRoots n R).Nonempty) (η : ↥(rootsOfUnity n S)),
  f ↑↑((rootsOfUnityEquivOfPrimitiveRoots hf hζ).symm η) = ↑↑η
-- Mathlib.Order.Interval.Set.ProjIcc
/-- If `f : α → β` is a constant both on $(-∞, a]$ and on $[b, +∞)$, then the extension of this
function from $[a, b]$ to the whole line is equal to the original function.  -/
Set.IccExtend_eq_self : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] {a b : α} (h : a ≤ b) (f : α → β),
  (∀ x < a, f x = f a) → (∀ (x : α), b < x → f x = f b) → Set.IccExtend h (f ∘ Subtype.val) = f
-- Mathlib.Topology.Hom.Open
ContinuousOpenMap.comp_apply : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : TopologicalSpace γ] (f : β →CO γ) (g : α →CO β) (a : α), (f.comp g) a = f (g a)
-- Init.System.FilePath
/-- Constructs a path from a list of file names by interspersing them with the current platform's path
separator.
 -/
System.mkFilePath : List String → System.FilePath
-- Mathlib.RingTheory.PowerSeries.Inverse
PowerSeries.Unit_of_divided_by_X_pow_order_zero : ∀ {k : Type u_2} [inst : Field k], PowerSeries.Unit_of_divided_by_X_pow_order 0 = 1
-- Mathlib.Tactic.Translate.UnfoldBoundary
_private.Mathlib.Tactic.Translate.UnfoldBoundary.0.Mathlib.Tactic.UnfoldBoundary.UnfoldBoundaries.unfoldInsertions.headBetaBody : Lean.Expr → Lean.Expr
-- Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
WeierstrassCurve.VariableChange.map.eq_1 : ∀ {R : Type u} [inst : CommRing R] (C : WeierstrassCurve.VariableChange R) {A : Type v} [inst_1 : CommRing A]
  (φ : R →+* A), C.map φ = { u := (Units.map ↑φ) C.u, r := φ C.r, s := φ C.s, t := φ C.t }
-- Mathlib.Topology.MetricSpace.Thickening
/-- The closed `δ`-thickening `Metric.cthickening δ E` of a subset `E` in a pseudo emetric space
consists of those points that are at infimum distance at most `δ` from `E`.  -/
Metric.cthickening : {α : Type u} → [PseudoEMetricSpace α] → ℝ → Set α → Set α
-- Mathlib.Topology.Algebra.Support
tsupport_add_neg : ∀ {X : Type u_1} {α : Type u_2} [inst : TopologicalSpace X] [inst_1 : SubtractionMonoid α] (f g : X → α),
  (tsupport fun x => f x + -g x) ⊆ tsupport f ∪ tsupport g
-- Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
mvfderiv_comp_mfderivWithin_of_eq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M' → M} {g : M → 𝕜} {x : M'}
  {y : M} {s : Set M'},
  MDiffAt g y → MDiffAt[s] f x → UniqueMDiffAt[s] x → f x = y → d[s] (g ∘ f) x = d% g y ∘SL mfderiv[s] f x
-- Mathlib.RingTheory.Ideal.Quotient.Operations
DoubleQuot.quotQuotMkₐ_toRingHom : ∀ (R : Type u) {A : Type u_1} [inst : CommSemiring R] [inst_1 : CommRing A] [inst_2 : Algebra R A] (I J : Ideal A),
  ↑(DoubleQuot.quotQuotMkₐ R I J) = DoubleQuot.quotQuotMk I J
-- Mathlib.Data.Set.Lattice
/-- If all sets in a collection are either `∅` or `Set.univ`, then so is their union.  -/
Set.sUnion_mem_empty_univ : ∀ {α : Type u_1} {S : Set (Set α)}, S ⊆ {∅, Set.univ} → ⋃₀ S ∈ {∅, Set.univ}
-- Mathlib.Algebra.Lie.SerreConstruction
/-- The exceptional split Lie algebra of type f₄.  -/
LieAlgebra.f₄ : (R : Type u) → [CommRing R] → Type u
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- A binary bicone for a pair of objects `P Q : C` consists of the cone point `X`,
maps from `X` to both `P` and `Q`, and maps from both `P` and `Q` to `X`,
so that `inl ≫ fst = 𝟙 P`, `inl ≫ snd = 0`, `inr ≫ fst = 0`, and `inr ≫ snd = 𝟙 Q`  -/
CategoryTheory.Limits.BinaryBicone.fst : {C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {P Q : C} → (self : CategoryTheory.Limits.BinaryBicone P Q) → self.pt ⟶ P
-- Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
DirectedOn.isLUB_ciSup_set : ∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompletePartialOrderSup α] {f : β → α} {s : Set β},
  DirectedOn (fun x1 x2 => x1 ≤ x2) (f '' s) → BddAbove (f '' s) → s.Nonempty → IsLUB (f '' s) (⨆ i, f ↑i)
-- Lean.Meta.Sym.Offset
/-- Increments the constant part of the offset by `k'`.  -/
Lean.Meta.Sym.Offset.inc : Lean.Meta.Sym.Offset → ℕ → Lean.Meta.Sym.Offset
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
/-- **Alias** of `intervalIntegral.integral_deriv_smul_deriv_comp'`. -/
intervalIntegral.integral_deriv_comp_smul_deriv' : ∀ {a b : ℝ} {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f f' : ℝ → ℝ} {g g' : ℝ → E}
  [CompleteSpace E],
  ContinuousOn f (Set.uIcc a b) →
    (∀ x ∈ Set.Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Set.Ioi x) x) →
      ContinuousOn f' (Set.uIcc a b) →
        ContinuousOn g (Set.uIcc (f a) (f b)) →
          (∀ x ∈ Set.Ioo (min (f a) (f b)) (max (f a) (f b)), HasDerivWithinAt g (g' x) (Set.Ioi x) x) →
            ContinuousOn g' (f '' Set.uIcc a b) → ∫ (x : ℝ) in a..b, f' x • (g' ∘ f) x = (g ∘ f) b - (g ∘ f) a
-- Mathlib.Analysis.Distribution.TestFunction
/-- The "original topology" on `𝓓^{n}(Ω, F)`, defined as the supremum over all compacts `K ⊆ Ω` of
the topology on `𝓓^{n}_{K}(E, F)`. In other words, this topology makes `𝓓^{n}(Ω, F)` the inductive
limit of the `𝓓^{n}_{K}(E, F)`s **in the category of topological spaces**.

Note that this has no reason to be a locally convex (or even vector space) topology. For this
reason, we actually endow `𝓓^{n}(Ω, F)` with another topology, namely the finest locally convex
topology which is coarser than this original topology. See `TestFunction.topologicalSpace`.  -/
TestFunction.originalTop : {E : Type u_3} →
  [inst : NormedAddCommGroup E] →
    [inst_1 : NormedSpace ℝ E] →
      (Ω : TopologicalSpace.Opens E) →
        (F : Type u_4) →
          [inst_2 : NormedAddCommGroup F] →
            [inst_3 : NormedSpace ℝ F] → (n : ℕ∞) → TopologicalSpace (TestFunction Ω F n)
-- Mathlib.Data.PFunctor.Univariate.M
PFunctor.M.head_succ : ∀ {F : PFunctor.{uA, uB}} (n m : ℕ) (x : F.M),
  PFunctor.Approx.head' (x.approx n.succ) = PFunctor.Approx.head' (x.approx m.succ)
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.CongrKey.mk : {enodes : Lean.Meta.Grind.ENodeMap} → Lean.Expr → Lean.Meta.Grind.CongrKey enodes
-- Mathlib.Algebra.MonoidAlgebra.Module
/-- `MonoidAlgebra.single` as a `DistribMulActionHom`.  -/
MonoidAlgebra.singleDistribMulActionHom : {R : Type u_1} →
  {S : Type u_2} →
    {M : Type u_3} →
      [inst : Semiring S] → [inst_1 : Monoid R] → [inst_2 : DistribMulAction R S] → M → S →+[R] MonoidAlgebra S M
-- Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
RootPairing.PolarizationIn.congr_simp : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) (S : Type u_5)
  [inst_5 : CommRing S] [inst_6 : Algebra S R] [inst_7 : FaithfulSMul S R] [inst_8 : Module S M]
  [inst_9 : IsScalarTower S R M] [inst_10 : Module S N] [inst_11 : P.IsValuedIn S] [inst_12 : Fintype ι],
  P.PolarizationIn S = P.PolarizationIn S
-- Std.Time.DateTime.PlainDateTime
Std.Time.PlainDateTime.instHAddOffset_6 : HAdd Std.Time.PlainDateTime Std.Time.Nanosecond.Offset Std.Time.PlainDateTime
-- Mathlib.CategoryTheory.WithTerminal.Cone
/-- Given a functor `K : J ⥤ Under X` and its extension `liftFromUnder K : WithInitial J ⥤ C`,
there is an obvious equivalence between cocones of these two functors.
A cocone of `K` is an object of `Under X`, so it has the form `X ⟶ t`.
Equivalently, a cocone of `WithInitial K` is an object `t : C`,
and we can recover the structure morphism as `ι.app X : X ⟶ t`.  -/
CategoryTheory.WithInitial.coconeEquiv : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : Type w} →
      [inst_1 : CategoryTheory.Category.{w', w} J] →
        {X : C} →
          {K : CategoryTheory.Functor J (CategoryTheory.Under X)} →
            CategoryTheory.Limits.Cocone K ≌
              CategoryTheory.Limits.Cocone (CategoryTheory.WithInitial.liftFromUnder.obj K)
-- Std.Http.Server.Handler
/-- Function called when a request includes `Expect: 100-continue`. Return `true` to accept
the body or `false` to reject it with `417 Expectation Failed`. The default always accepts.
 -/
Std.Http.Server.StatelessHandler.onContinue : Std.Http.Server.StatelessHandler → Std.Http.Request.Head → Std.Async.Async Bool
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.defnNatCommRing : Lean.Expr →
  Int.Internal.Linear.Var →
    Int.Internal.Linear.Expr →
      Int.Internal.Linear.Poly →
        Lean.Meta.Grind.Arith.CommRing.RingExpr →
          Lean.Grind.CommRing.Poly → Int.Internal.Linear.Poly → Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof
-- Mathlib.Analysis.CStarAlgebra.Hom
StarAlgHom.restrictScalars.congr_simp : ∀ (R : Type u_1) {S : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : Semiring A] [inst_3 : Semiring B] [inst_4 : Algebra R S] [inst_5 : Algebra S A] [inst_6 : Algebra S B]
  [inst_7 : Algebra R A] [inst_8 : Algebra R B] [inst_9 : IsScalarTower R S A] [inst_10 : IsScalarTower R S B]
  [inst_11 : Star A] [inst_12 : Star B] (f f_1 : A →⋆ₐ[S] B),
  f = f_1 → StarAlgHom.restrictScalars R f = StarAlgHom.restrictScalars R f_1
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.equivFunOnFintype_apply : ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → Zero (β i)] [inst_1 : Fintype ι] (a : Π₀ (i : ι), β i) (a_1 : ι),
  DFinsupp.equivFunOnFintype a a_1 = a a_1
-- Lean.CoreM
/-- Name generator that creates user-accessible names.  -/
Lean.DeclNameGenerator : Type
-- Mathlib.Dynamics.Flow
Flow.mem_orbit_of_mem_forwardOrbit : ∀ {τ : Type u_1} {α : Type u_2} [inst : TopologicalSpace τ] [inst_1 : TopologicalSpace α] [inst_2 : AddMonoid τ]
  (ϕ : Flow τ α) [inst_3 : Preorder τ] [inst_4 : AddLeftMono τ] {x₁ x₂ : α}, x₁ ∈ ϕ.forwardOrbit x₂ → x₁ ∈ ϕ.orbit x₂
-- Mathlib.Data.List.Cycle
List.prev_cons_cons_eq : ∀ {α : Type u_1} [inst : DecidableEq α] (l : List α) (x z : α) (h : x ∈ x :: z :: l),
  (x :: z :: l).prev x h = (z :: l).getLast ⋯
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
SimpleGraph.Preconnected.toSubgraph : ∀ {V : Type u} {G H : SimpleGraph V} (h : H ≤ G), H.Preconnected → (SimpleGraph.toSubgraph H h).Preconnected
-- Mathlib.Data.Vector3
Vector3.recOn_cons : ∀ {α : Type u_1} {C : {n : ℕ} → Vector3 α n → Sort u_2} {H0 : C []}
  {Hs : {n : ℕ} → (a : α) → (w : Vector3 α n) → C w → C (Vector3.cons a w)} {n : ℕ} {a : α} {v : Vector3 α n},
  (Vector3.cons a v).recOn H0 Hs = Hs a v (v.recOn H0 Hs)
-- Mathlib.RingTheory.AdjoinRoot
/-- The natural isomorphism `R[α]/((I[x] ⊔ (f)) / (f)) ≅ (R[x]/I[x])/((f) ⊔ I[x] / I[x])`
for `α` a root of `f : R[X]` and `I : Ideal R`  -/
AdjoinRoot.quotMapCMapSpanMkEquivQuotMapCQuotMapMk : {R : Type u_1} →
  [inst : CommRing R] →
    (I : Ideal R) →
      (f : Polynomial R) →
        AdjoinRoot f ⧸ Ideal.map (AdjoinRoot.mk f) (Ideal.map Polynomial.C I) ≃+*
          (Polynomial R ⧸ Ideal.map Polynomial.C I) ⧸
            Ideal.map (Ideal.Quotient.mk (Ideal.map Polynomial.C I)) (Ideal.span {f})
-- Lean.Elab.PreDefinition.WF.GuessLex
_private.Lean.Elab.PreDefinition.WF.GuessLex.0.Lean.Elab.WF.GuessLex.withRecApps.processRec : {α : Type} →
  (recFnName : Lean.Name) →
    ℕ → (Lean.Expr → Array Lean.Expr → Lean.MetaM α) → Lean.Expr → Lean.Expr → Lean.Elab.WF.GuessLex.M recFnName α Unit
-- Mathlib.RingTheory.RingHom.OpenImmersion
Algebra.IsStandardOpenImmersion.iff_of_algEquiv : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S] {T : Type u_4}
  [inst_3 : CommSemiring T] [inst_4 : Algebra R T] (e : S ≃ₐ[R] T),
  Algebra.IsStandardOpenImmersion R S ↔ Algebra.IsStandardOpenImmersion R T
-- Mathlib.Topology.MetricSpace.Thickening
Metric.thickening_union : ∀ {α : Type u} [inst : PseudoEMetricSpace α] (δ : ℝ) (s t : Set α),
  Metric.thickening δ (s ∪ t) = Metric.thickening δ s ∪ Metric.thickening δ t
-- Std.Time.Date.PlainDate
Std.Time.PlainDate.mk : (year : Std.Time.Year.Offset) →
  (month : Std.Time.Month.Ordinal) → (day : Std.Time.Day.Ordinal) → year.Valid month day → Std.Time.PlainDate
-- Std.Data.DTreeMap.Internal.Queries
/-- Returns the entry (key-value pair) for the key `k`, or `fallback` if such a key does not exist.  -/
Std.DTreeMap.Internal.Impl.getEntryD : {α : Type u} → {β : α → Type v} → [Ord α] → Std.DTreeMap.Internal.Impl α β → α → (a : α) × β a → (a : α) × β a
-- Mathlib.NumberTheory.ZetaValues
bernoulliFourierCoeff.eq_1 : ∀ (k : ℕ) (n : ℤ),
  bernoulliFourierCoeff k n = fourierCoeffOn bernoulliFourierCoeff._proof_1 (fun x => ↑(bernoulliFun k x)) n
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get!_insert!_self : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α],
  t.WF → ∀ {a : α} [inst_1 : Inhabited (β a)] {b : β a}, (Std.DTreeMap.Internal.Impl.insert! a b t).get! a = b
-- Mathlib.Analysis.Calculus.FDeriv.Comp
/-- **Alias** of `fderiv_fun_comp`.

---

Eta-expanded form of `fderiv_comp` -/
fderiv_comp' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f : E → F} (x : E) {g : F → G},
  DifferentiableAt 𝕜 g (f x) →
    DifferentiableAt 𝕜 f x → fderiv 𝕜 (fun x => g (f x)) x = fderiv 𝕜 g (f x) ∘SL fderiv 𝕜 f x
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get!_erase_self : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited β], m.WF → ∀ {k : α}, Std.DHashMap.Raw.Const.get! (m.erase k) k = default
-- Mathlib.Logic.Equiv.Basic
/-- If `Unique β`, then `Unique α` is equivalent to `α ≃ β`.  -/
uniqueEquivEquivUnique : (α : Sort u) → (β : Sort v) → [Unique β] → Unique α ≃ (α ≃ β)