mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Slice.Array.Lemmas
Array.mkSlice_rii_eq_mkSlice_rio : ∀ {α : Type u_1} {xs : Array α}, Std.Rii.Sliceable.mkSlice xs *...* = Std.Rio.Sliceable.mkSlice xs *...xs.size
-- Mathlib.Algebra.CharP.MixedCharZero
/-- A ring of characteristic zero is of "mixed characteristic `(0, p)`" if there exists an ideal
such that the quotient `R ⧸ I` has characteristic `p`.

**Remark:** For `p = 0`, `MixedChar R 0` is a meaningless definition (i.e. satisfied by any ring)
as `R ⧸ ⊥ ≅ R` has by definition always characteristic zero.
One could require `(I ≠ ⊥)` in the definition, but then `MixedChar R 0` would mean something
like `ℤ`-algebra of extension degree `≥ 1` and would be completely independent from
whether something is a `ℚ`-algebra or not (e.g. `ℚ[X]` would satisfy it but `ℚ` wouldn't).
 -/
MixedCharZero : (R : Type u_1) → [CommRing R] → ℕ → Prop
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Metric
/-- If a measurable space on `α` is countably generated and separates points, there is some
second countable t4 topology on `α` (i.e. a separable metrizable one) for which every
open set is measurable.  -/
exists_opensMeasurableSpace_of_countablySeparated : ∀ (α : Type u_5) [m : MeasurableSpace α] [MeasurableSpace.CountablySeparated α],
  ∃ x, SecondCountableTopology α ∧ T4Space α ∧ OpensMeasurableSpace α
-- Mathlib.RingTheory.ChainOfDivisors
mkFactorOrderIsoOfFactorDvdEquiv_symm_apply_coe : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] {N : Type u_2} [inst_1 : CommMonoidWithZero N] [inst_2 : Subsingleton Mˣ]
  [inst_3 : Subsingleton Nˣ] {m : M} {n : N} {d : { l // l ∣ m } ≃ { l // l ∣ n }}
  (hd : ∀ (l l' : { l // l ∣ m }), ↑(d l) ∣ ↑(d l') ↔ ↑l ∣ ↑l') (l : ↑(Set.Iic (Associates.mk n))),
  ↑((RelIso.symm (mkFactorOrderIsoOfFactorDvdEquiv hd)) l) =
    Associates.mk ↑(d.symm ⟨associatesEquivOfUniqueUnits ↑l, ⋯⟩)
-- Init.Data.List.MinMax
List.min?_replicate : ∀ {α : Type u_1} [inst : Min α] [Std.IdempotentOp min] {n : ℕ} {a : α},
  (List.replicate n a).min? = if n = 0 then none else some a
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
/-- A version of `WithTop.map` for `OneHom`s.  -/
OneHom.withTopMap : {M : Type u_1} → {N : Type u_2} → [inst : One M] → [inst_1 : One N] → OneHom M N → OneHom (WithTop M) (WithTop N)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokenType.regexp.sizeOf_spec : sizeOf Lean.Lsp.SemanticTokenType.regexp = 1
-- Mathlib.Analysis.Normed.Group.Basic
nndist_indicator : ∀ {α : Type u_2} {E : Type u_5} [inst : SeminormedAddGroup E] (s t : Set α) (f : α → E) (x : α),
  nndist (s.indicator f x) (t.indicator f x) = ‖(symmDiff s t).indicator f x‖₊
-- Mathlib.Tactic.Determinant.Bird.Cert
/-- Certify `e = norm` by evaluating `e` with the `ring` normalizer.  -/
Mathlib.Tactic.Determinant.certEval : {u : Lean.Level} →
  {α : Q(Type u)} →
    {rα : Q(CommRing «$α»)} → Q(«$α») → Mathlib.Tactic.Determinant.CertM rα (Mathlib.Tactic.Determinant.Cert rα)
-- Mathlib.AlgebraicTopology.SimplicialSet.Basic
/-- The ulift functor `SSet.{u} ⥤ SSet.{max u v}` on simplicial sets.  -/
SSet.uliftFunctor : CategoryTheory.Functor SSet SSet
-- Mathlib.Computability.TuringMachine.ToPartrec
_private.Mathlib.Computability.TuringMachine.ToPartrec.0.Turing.PartrecToTM2.trLList.match_1.eq_1 : ∀ (motive : List (List ℕ) → Sort u_1) (h_1 : Unit → motive [])
  (h_2 : (l : List ℕ) → (ls : List (List ℕ)) → motive (l :: ls)),
  (match [] with
    | [] => h_1 ()
    | l :: ls => h_2 l ls) =
    h_1 ()
-- Mathlib.Data.ENNReal.Real
/-- **Alias** of the reverse direction of `ENNReal.ofReal_pos`. -/
_private.Mathlib.Data.ENNReal.Real.0.ENNReal.Bound.ofReal_pos_of_pos : ∀ {p : ℝ}, 0 < p → 0 < ENNReal.ofReal p
-- Mathlib.Algebra.Lie.Weights.Basic
/-- This is the Fitting decomposition of the Lie module `M`.  -/
LieModule.isCompl_genWeightSpace_zero_posFittingComp : ∀ (R : Type u_2) (L : Type u_3) (M : Type u_4) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L] [IsNoetherian R M] [IsArtinian R M],
  IsCompl (LieModule.genWeightSpace M 0) (LieModule.posFittingComp R L M)
-- Mathlib.Analysis.Normed.Lp.ProdLp
LinearIsometry.withLpProdMap_apply : ∀ (p : ENNReal) {𝕜 : Type u_1} {α : Type u_2} {β : Type u_3} {α' : Type u_5} {β' : Type u_6} [hp : Fact (1 ≤ p)]
  [inst : Semiring 𝕜] [inst_1 : SeminormedAddCommGroup α] [inst_2 : Module 𝕜 α] [inst_3 : SeminormedAddCommGroup β]
  [inst_4 : Module 𝕜 β] [inst_5 : SeminormedAddCommGroup α'] [inst_6 : Module 𝕜 α'] [inst_7 : SeminormedAddCommGroup β']
  [inst_8 : Module 𝕜 β'] (f : α →ₗᵢ[𝕜] α') (g : β →ₗᵢ[𝕜] β') (x : WithLp p (α × β)),
  (LinearIsometry.withLpProdMap p f g) x = WithLp.toLp p (f x.fst, g x.snd)
-- Init.Data.Iterators.Combinators.Monadic.FilterMap
Std.Iterators.Types.FilterMap.ext : ∀ {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {lift : ⦃α : Type w⦄ → m α → n α}
  {f : β → Std.Iterators.PostconditionT n (Option γ)} {x y : Std.Iterators.Types.FilterMap α m n lift f},
  x.inner = y.inner → x = y
-- Mathlib.ModelTheory.LanguageMap
FirstOrder.Language.constantsOnMap_isExpansionOn : ∀ {M : Type w} {α : Type u'} {β : Type v'} {f : α → β} {fα : α → M} {fβ : β → M},
  fβ ∘ f = fα → (FirstOrder.Language.LHom.constantsOnMap f).IsExpansionOn M
-- Mathlib.CategoryTheory.Subobject.Limits
/-- The kernel of a morphism `f : X ⟶ Y` as a `Subobject X`.  -/
CategoryTheory.Limits.kernelSubobject : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
        (f : X ⟶ Y) → [CategoryTheory.Limits.HasKernel f] → CategoryTheory.Subobject X
-- Mathlib.CategoryTheory.Sites.Plus
CategoryTheory.GrothendieckTopology.plusFunctor_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (D : Type w)
  [inst_1 : CategoryTheory.Category.{w', w} D]
  [inst_2 :
    ∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)]
  [inst_3 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] (P : CategoryTheory.Functor Cᵒᵖ D),
  (J.plusFunctor D).obj P = J.plusObj P
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMulEquiv.symm_trans_apply : ∀ {M : Type u_1} {N : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace N] [inst_2 : Mul M]
  [inst_3 : Mul N] {L : Type u_3} [inst_4 : Mul L] [inst_5 : TopologicalSpace L] (e₁ : M ≃ₜ* N) (e₂ : N ≃ₜ* L) (l : L),
  (e₁.trans e₂).symm l = e₁.symm (e₂.symm l)
-- Mathlib.Algebra.Group.Hom.Defs
AddHom.coe_copy : ∀ {M : Type u_4} {N : Type u_5} {x : Add M} {x_1 : Add N} (f : M →ₙ+ N) (f' : M → N) (h : f' = ⇑f), ⇑(f.copy f' h) = f'
-- Mathlib.Algebra.GroupWithZero.Units.Basic
Ring.inverse_mul_eq_iff_eq_mul : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] (x y z : M₀), IsUnit x → (Ring.inverse x * y = z ↔ y = x * z)
-- Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
MeasureTheory.Measure.haveLebesgueDecomposition_withDensity : ∀ {α : Type u_1} {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) {f : α → ENNReal},
  Measurable f → (μ.withDensity f).HaveLebesgueDecomposition μ
-- Lean.Server.References
Lean.Server.References.MatchedDefinition.mk : {α : Type} → Lean.Name → Lean.Lsp.DocumentUri → α → Lean.Lsp.Range → Lean.Server.References.MatchedDefinition α
-- Init.Prelude
Functor.mk : {f : Type u → Type v} → ({α β : Type u} → (α → β) → f α → f β) → ({α β : Type u} → α → f β → f α) → Functor f
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubMulAction.smul' : {S : Type u'} →
  {R : Type u} →
    {M : Type v} →
      [inst : Monoid R] →
        [inst_1 : MulAction R M] →
          [inst_2 : SMul S R] → [inst_3 : SMul S M] → [IsScalarTower S R M] → (p : SubMulAction R M) → SMul S ↥p
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
cfcₙHomSuperset_id : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : Nontrivial R] [inst_2 : StarRing R]
  [inst_3 : MetricSpace R] [inst_4 : IsTopologicalSemiring R] [inst_5 : ContinuousStar R] [inst_6 : NonUnitalRing A]
  [inst_7 : StarRing A] [inst_8 : TopologicalSpace A] [inst_9 : Module R A] [inst_10 : IsScalarTower R A A]
  [inst_11 : SMulCommClass R A A] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p] {a : A} (ha : p a)
  {s : Set R} (hs : quasispectrum R a ⊆ s), (cfcₙHomSuperset ha hs) (ContinuousMapZero.id s) = a
-- Mathlib.Data.Fin.Tuple.Take
Fin.take_one : ∀ {n : ℕ} {α : Fin (n + 1) → Sort u_2} (v : (i : Fin (n + 1)) → α i), Fin.take 1 ⋯ v = fun i => v (Fin.castLE ⋯ i)
-- Mathlib.Topology.Bases
TopologicalSpace.isCountablyGenerated_nhdsWithin : ∀ {α : Type u} [t : TopologicalSpace α] (x : α) [(nhds x).IsCountablyGenerated] (s : Set α),
  (nhdsWithin x s).IsCountablyGenerated
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoDiv_add_right : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α), toIcoDiv hp a (b + p) = toIcoDiv hp a b + 1
-- Mathlib.Algebra.Category.Ring.Colimits
RingCat.Colimits.Prequotient.zero : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] → {F : CategoryTheory.Functor J RingCat} → RingCat.Colimits.Prequotient F
-- Mathlib.Algebra.FiniteSupport.Basic
Function.HasFiniteMulSupport.of_comp : ∀ {α : Type u_1} {M : Type u_2} [inst : One M] {β : Type u_3} {f : β → M} {g : α → β} [inst_1 : One β],
  Function.HasFiniteMulSupport (f ∘ g) → f 1 = 1 → Function.Injective f → Function.HasFiniteMulSupport g
-- Mathlib.Analysis.Normed.Ring.Basic
NormedRing.toNorm : {α : Type u_5} → [self : NormedRing α] → Norm α
-- Mathlib.Order.Nat
Nat.instOrderBot : OrderBot ℕ
-- Mathlib.LinearAlgebra.Projectivization.PSL.Stabilizer
/-- Equivariance of `lineStab` under conjugation by elements of `SL`.  -/
Matrix.SpecialLinearGroup.lineStab_smul : ∀ {F : Type u_1} [inst : Field F] {ι : Type u_2} [inst_1 : DecidableEq ι] [inst_2 : Fintype ι]
  (g : Matrix.SpecialLinearGroup ι F) (L : Submodule F (ι → F)),
  Matrix.SpecialLinearGroup.lineStab (g • L) = MulAut.conj g • Matrix.SpecialLinearGroup.lineStab L
-- Mathlib.Data.ZMod.Basic
ZMod.natCast_self' : ∀ (n : ℕ), ↑n + 1 = 0
-- Mathlib.Algebra.Order.Pi
Pi.single_nonpos : ∀ {ι : Type u_6} {α : ι → Type u_7} [inst : DecidableEq ι] [inst_1 : (i : ι) → Zero (α i)]
  [inst_2 : (i : ι) → Preorder (α i)] {i : ι} {a : α i}, Pi.single i a ≤ 0 ↔ a ≤ 0
-- Mathlib.CategoryTheory.Category.Basic
CategoryTheory.epi_of_epi : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z)
  [CategoryTheory.Epi (CategoryTheory.CategoryStruct.comp f g)], CategoryTheory.Epi g
-- Mathlib.Order.Filter.AtTopBot.Archimedean
tendsto_intCast_atTop_iff : ∀ {α : Type u_1} {R : Type u_2} [inst : Ring R] [inst_1 : PartialOrder R] [IsStrictOrderedRing R] [Archimedean R]
  {f : α → ℤ} {l : Filter α}, Filter.Tendsto (fun n => ↑(f n)) l Filter.atTop ↔ Filter.Tendsto f l Filter.atTop
-- Std.Time.Format
/-- The americanDate format, which follows the pattern `MM-dd-uuuu`.
 -/
Std.Time.Formats.americanDate : Std.Time.GenericFormat Std.Time.Awareness.any
-- Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
SSet.relativeCellComplexOfMono_attachCells_cofan₁ : ∀ {X Y : SSet} (i : X ⟶ Y) [inst : CategoryTheory.Mono i] (d : ℕ) (x : ¬IsMax d),
  ((SSet.relativeCellComplexOfMono i).attachCells d x).cofan₁ =
    CategoryTheory.Limits.Cofan.mk (∐ fun i => (SSet.boundary d).toSSet)
      (CategoryTheory.Limits.Sigma.ι fun i => (SSet.boundary d).toSSet)
-- Batteries.Recycling.RBTree.Basic
RBTree.RBNode.reverse.eq_2 : ∀ {α : Type u_1} (c : RBTree.RBColor) (l : RBTree.RBNode α) (v : α) (r : RBTree.RBNode α),
  (RBTree.RBNode.node c l v r).reverse = RBTree.RBNode.node c r.reverse v l.reverse
-- Mathlib.RingTheory.PrincipalIdealDomain
/-- Any chain in the set of non-principal ideals has an upper bound which is non-principal.
(Namely, the union of the chain is such an upper bound.)

If you want the existence of a maximal non-principal ideal see
`Ideal.exists_maximal_not_isPrincipal`.  -/
Ideal.nonPrincipals_zorn : ∀ {R : Type u} [inst : Semiring R],
  ¬IsPrincipalIdealRing R →
    ∀ c ⊆ Ideal.nonPrincipals R, IsChain (fun x1 x2 => x1 ≤ x2) c → ∃ I ∈ Ideal.nonPrincipals R, ∀ J ∈ c, J ≤ I
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.HasColimitsOfSize.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C],
  autoParam
      (∀ (J : Type u₁) [inst_1 : CategoryTheory.Category.{v₁, u₁} J], CategoryTheory.Limits.HasColimitsOfShape J C)
      CategoryTheory.Limits.HasColimitsOfSize.has_colimits_of_shape._autoParam →
    CategoryTheory.Limits.HasColimitsOfSize.{v₁, u₁, v, u} C
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
IsAddRightRegular.withBot : ∀ {α : Type u} [inst : Add α] {a : α}, IsAddRightRegular a → IsAddRightRegular ↑a
-- Mathlib.LinearAlgebra.Complex.Module
star_mul_self_sub_self_mul_star : ∀ {A : Type u_1} [inst : NonUnitalNonAssocRing A] [inst_1 : StarRing A] [inst_2 : Module ℂ A] [IsScalarTower ℂ A A]
  [SMulCommClass ℂ A A] [inst_5 : StarModule ℂ A] (a : A),
  star a * a - a * star a = 2 • Complex.I • (↑(realPart a) * ↑(imaginaryPart a) - ↑(imaginaryPart a) * ↑(realPart a))
-- Mathlib.RepresentationTheory.Continuous.Basic
ContRepresentation.Equiv.isIntertwining' : ∀ {R : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Monoid G] [inst_1 : Ring R]
  [inst_2 : AddCommGroup V] [inst_3 : TopologicalSpace V] [inst_4 : IsTopologicalAddGroup V] [inst_5 : Module R V]
  [inst_6 : AddCommGroup W] [inst_7 : TopologicalSpace W] [inst_8 : IsTopologicalAddGroup W] [inst_9 : Module R W]
  {π₁ : ContRepresentation R G V} {π₂ : ContRepresentation R G W} (self : π₁.Equiv π₂) (g : G),
  { toLinearMap := ↑↑self.toContinuousLinearEquiv, cont := ⋯ } ∘SL π₁ g =
    π₂ g ∘SL { toLinearMap := ↑↑self.toContinuousLinearEquiv, cont := ⋯ }
-- Mathlib.Algebra.Module.Rat
/-- There can be at most one `Module ℚ E` structure on an additive commutative group.  -/
subsingleton_rat_module : ∀ (E : Type u_3) [inst : AddCommGroup E], Subsingleton (Module ℚ E)
-- Mathlib.Analysis.Convex.Extreme
IsExtreme.mk : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : SMul 𝕜 E] {A B : Set E},
  B ⊆ A → (∀ ⦃x : E⦄, x ∈ A → ∀ ⦃y : E⦄, y ∈ A → ∀ ⦃z : E⦄, z ∈ B → z ∈ openSegment 𝕜 x y → x ∈ B) → IsExtreme 𝕜 A B
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.IsLongestMatch.ne_startPos : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [String.Slice.Pattern.Model.StrictPatternModel pat] {s : String.Slice} {pos : s.Pos},
  String.Slice.Pattern.Model.IsLongestMatch pat pos → pos ≠ s.startPos
-- Mathlib.RingTheory.Valuation.ValuationRing
ValuationRing.isFractionRing_iff : ∀ {𝒪 : Type u} {K : Type v} [inst : CommRing 𝒪] [inst_1 : Field K] [inst_2 : Algebra 𝒪 K] [inst_3 : IsDomain 𝒪]
  [ValuationRing 𝒪],
  IsFractionRing 𝒪 K ↔
    (∀ (x : K), ∃ a, x = (algebraMap 𝒪 K) a ∨ x⁻¹ = (algebraMap 𝒪 K) a) ∧ Function.Injective ⇑(algebraMap 𝒪 K)
-- Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Multiset.prod_hom₂ : ∀ {ι : Type u_2} {M : Type u_5} {N : Type u_6} {O : Type u_7} [inst : CommMonoid M] [inst_1 : CommMonoid N]
  [inst_2 : CommMonoid O] (s : Multiset ι) (f : M → N → O),
  (∀ (a b : M) (c d : N), f (a * b) (c * d) = f a c * f b d) →
    f 1 1 = 1 →
      ∀ (f₁ : ι → M) (f₂ : ι → N),
        (Multiset.map (fun i => f (f₁ i) (f₂ i)) s).prod = f (Multiset.map f₁ s).prod (Multiset.map f₂ s).prod
-- Mathlib.Algebra.Order.Archimedean.Class
FiniteMulArchimedeanClass.eq_1 : ∀ (M : Type u_1) [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M],
  FiniteMulArchimedeanClass M = { A // A ≠ ⊤ }
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.EqCnstr.mk.sizeOf_spec : ∀ (p : Lean.Grind.CommRing.Poly) (h : Lean.Meta.Grind.Arith.CommRing.EqCnstrProof) (sugar id : ℕ),
  sizeOf { p := p, h := h, sugar := sugar, id := id } = 1 + sizeOf p + sizeOf h + sizeOf sugar + sizeOf id
-- Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
_private.Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence.0.ContinuousLinearMap.toBilinForm_diagonalStrongDualProd_apply : ∀ {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {L₁ : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ}
  {L₂ : StrongDual ℝ F →L[ℝ] StrongDual ℝ F →L[ℝ] ℝ} (x y : StrongDual ℝ (E × F)),
  ((ContinuousLinearMap.diagonalStrongDualProd✝ L₁ L₂).toBilinForm x) y =
    (L₁.toBilinForm (x ∘SL ContinuousLinearMap.inl ℝ E F)) (y ∘SL ContinuousLinearMap.inl ℝ E F) +
      (L₂.toBilinForm (x ∘SL ContinuousLinearMap.inr ℝ E F)) (y ∘SL ContinuousLinearMap.inr ℝ E F)
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.range_subtype : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] (S : L.Substructure M), S.subtype.toHom.range = S
-- Mathlib.Topology.Order.ProjIcc
/-- See Note [continuity lemma statement].  -/
Continuous.IccExtend : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : LinearOrder α] {a b : α} {h : a ≤ b}
  [inst_1 : TopologicalSpace α] [OrderTopology α] [inst_3 : TopologicalSpace β] [inst_4 : TopologicalSpace γ]
  {f : γ → ↑(Set.Icc a b) → β} {g : γ → α},
  Continuous ↿f → Continuous g → Continuous fun a_1 => Set.IccExtend h (f a_1) (g a_1)
-- Mathlib.Algebra.TrivSqZeroExt.Basic
/-- Inversion of the trivial-square-zero extension, sending $r + m$ to $r^{-1} - r^{-1}mr^{-1}$.

Strictly this is only a _two_-sided inverse when the left and right actions associate.  -/
TrivSqZeroExt.instInv : {R : Type u} → {M : Type v} → [Neg M] → [Inv R] → [SMul Rᵐᵒᵖ M] → [SMul R M] → Inv (TrivSqZeroExt R M)
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
/-- When every element of a set `s` is bounded by an element of a set `t`, and conversely, then
`s` and `t` have the same supremum. This holds even when the sets may be empty or unbounded.  -/
csSup_eq_csSup_of_forall_exists_le : ∀ {α : Type u_1} [inst : ConditionallyCompleteLinearOrder α] {s t : Set α},
  (∀ x ∈ s, ∃ y ∈ t, x ≤ y) → (∀ y ∈ t, ∃ x ∈ s, y ≤ x) → sSup s = sSup t
-- Mathlib.Topology.Category.TopCat.Opens
/-- If `f : X ⟶ Y` is a map of topological spaces and `U ⊆ V` are open subsets of `X` whose
images are open, this is the morphism `f'' U ⟶ f'' Y` in `Opens Y`. Useful for applications
to presheaves when we don't want to suppose that `f` is an open map.
 -/
IsOpenMap.functorMap : {X Y : TopCat} →
  {f : X ⟶ Y} →
    {U V : TopologicalSpace.Opens ↑X} →
      (HU : IsOpen (⇑(CategoryTheory.ConcreteCategory.hom f) '' ↑U)) →
        (HV : IsOpen (⇑(CategoryTheory.ConcreteCategory.hom f) '' ↑V)) →
          U ≤ V →
            ({ carrier := ⇑(CategoryTheory.ConcreteCategory.hom f) '' ↑U, is_open' := HU } ⟶
              { carrier := ⇑(CategoryTheory.ConcreteCategory.hom f) '' ↑V, is_open' := HV })
-- Mathlib.FieldTheory.RatFunc.Valuation
RatFunc.InftyValuation.map_zero' : ∀ (F : Type u_1) [inst : Field F] [inst_1 : DecidableEq (RatFunc F)], RatFunc.inftyValuationDef F 0 = 0
-- Std.Time.Format.DateFormat
/-- Noon string (e.g., "noon").  -/
Std.Time.DayPeriodSymbols.noon : Std.Time.DayPeriodSymbols → String
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.EMatch.State.mk.injEq : ∀ (thmMap : Lean.Meta.Grind.EMatchTheoremsArray) (gmt : ℕ) (thms newThms : Lean.PArray Lean.Meta.Grind.EMatchTheorem)
  (numInstances numDelayedInstances num : ℕ) (preInstances : Lean.Meta.Grind.PreInstanceSet) (nextThmIdx : ℕ)
  (matchEqNames : Lean.PHashSet Lean.Name)
  (delayedThmInsts : Lean.PHashMap Lean.Meta.Sym.ExprPtr (List Lean.Meta.Grind.DelayedTheoremInstance))
  (thmMap_1 : Lean.Meta.Grind.EMatchTheoremsArray) (gmt_1 : ℕ)
  (thms_1 newThms_1 : Lean.PArray Lean.Meta.Grind.EMatchTheorem) (numInstances_1 numDelayedInstances_1 num_1 : ℕ)
  (preInstances_1 : Lean.Meta.Grind.PreInstanceSet) (nextThmIdx_1 : ℕ) (matchEqNames_1 : Lean.PHashSet Lean.Name)
  (delayedThmInsts_1 : Lean.PHashMap Lean.Meta.Sym.ExprPtr (List Lean.Meta.Grind.DelayedTheoremInstance)),
  ({ thmMap := thmMap, gmt := gmt, thms := thms, newThms := newThms, numInstances := numInstances,
        numDelayedInstances := numDelayedInstances, num := num, preInstances := preInstances, nextThmIdx := nextThmIdx,
        matchEqNames := matchEqNames, delayedThmInsts := delayedThmInsts } =
      { thmMap := thmMap_1, gmt := gmt_1, thms := thms_1, newThms := newThms_1, numInstances := numInstances_1,
        numDelayedInstances := numDelayedInstances_1, num := num_1, preInstances := preInstances_1,
        nextThmIdx := nextThmIdx_1, matchEqNames := matchEqNames_1, delayedThmInsts := delayedThmInsts_1 }) =
    (thmMap = thmMap_1 ∧
      gmt = gmt_1 ∧
        thms = thms_1 ∧
          newThms = newThms_1 ∧
            numInstances = numInstances_1 ∧
              numDelayedInstances = numDelayedInstances_1 ∧
                num = num_1 ∧
                  preInstances = preInstances_1 ∧
                    nextThmIdx = nextThmIdx_1 ∧ matchEqNames = matchEqNames_1 ∧ delayedThmInsts = delayedThmInsts_1)
-- Mathlib.CategoryTheory.Sites.Point.Basic
CategoryTheory.GrothendieckTopology.Point.presheafFiberCocone_ι_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point)
  {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A]
  [inst_2 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] (P : CategoryTheory.Functor Cᵒᵖ A)
  (x : Φ.fiber.Elementsᵒᵖ),
  (Φ.presheafFiberCocone P).ι.app x = Φ.toPresheafFiber (Opposite.unop x).fst (Opposite.unop x).snd P
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalSubalgebra.toNonUnitalSubsemiring_injective : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A],
  Function.Injective NonUnitalSubalgebra.toNonUnitalSubsemiring
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.isClosedEmbedding_comap_fst : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : CommSemiring S],
  Topology.IsClosedEmbedding (PrimeSpectrum.comap (RingHom.fst R S))
-- Mathlib.Tactic.Linter.DeprecatedSyntaxLinter
/-- The option `linter.style.nativeDecide` of the deprecated syntax linter flags usages of
the `native_decide` tactic, which is disallowed in mathlib.  -/
Mathlib.Linter.Style.linter.style.nativeDecide : Lean.Option Bool
-- Batteries.Data.Float.Basic
/-- The floating point value closest to the mathematical constant `π`.
 -/
Float.pi : Float
-- Mathlib.RingTheory.Ideal.Colon
Submodule.iInf_colon_iUnion : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (ι₁ : Sort u_3)
  (f : ι₁ → Submodule R M) (ι₂ : Sort u_4) (g : ι₂ → Set M), (⨅ i, f i).colon (⋃ j, g j) = ⨅ i, ⨅ j, (f i).colon (g j)
-- Std.Http.Test.Helpers
/-- Create a fresh mock connection, send `raw`, and run assertions.
 -/
Std.Http.Internal.Test.check : String →
  String →
    Std.Http.Internal.Test.TestHandler →
      (ByteArray → IO Unit) → optParam Std.Http.Config Std.Http.Internal.Test.defaultConfig → IO Unit
-- Mathlib.AlgebraicGeometry.Birational.RationalMap
AlgebraicGeometry.Scheme.PartialMap.restrict_hom : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X.PartialMap Y) (U : X.Opens) (hU : Dense ↑U) (hU' : U ≤ f.domain),
  (f.restrict U hU hU').hom = CategoryTheory.CategoryStruct.comp (X.homOfLE hU') f.hom
-- Mathlib.Tactic.DepRewrite
/-- `rw!` is like `rewrite!`, but also cleans up introduced refl-casts after every substitution.
It is available as an ordinary tactic and a `conv` tactic.
 -/
Mathlib.Tactic.DepRewrite.Conv.evalDepRwSeq : Lean.Elab.Tactic.Tactic