mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
MDifferentiableOn.smul : ∀ {𝕜 : 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] {s : Set M} {V : Type u_18} [inst_6 : NormedAddCommGroup V]
  [inst_7 : NormedSpace 𝕜 V] {f : M → 𝕜} {g : M → V}, MDiff[s] f → MDiff[s] g → MDiff[s] (f • g)
-- Mathlib.NumberTheory.RamificationInertia.Ramification
Ideal.IsDedekindDomain.emultiplicity_map_eq_zero_of_ne : ∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] [inst_2 : Algebra R S] [IsDedekindDomain S]
  [IsDedekindDomain R] {v : Ideal R} {w : Ideal S} {p : Ideal R},
  Irreducible v → Prime p → v ≠ p → ∀ [w.LiesOver v], emultiplicity w (Ideal.map (algebraMap R S) p) = 0
-- Mathlib.Computability.StateTransition
/-- number of steps taken  -/
StateTransition.EvalsTo.steps : {σ : Type u_1} → {f : σ → Option σ} → {a : σ} → {b : Option σ} → StateTransition.EvalsTo f a b → ℕ
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
Submodule.ker_starProjection : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (U : Submodule 𝕜 E) [inst_3 : U.HasOrthogonalProjection], (↑U.starProjection).ker = Uᗮ
-- Mathlib.CategoryTheory.Limits.Shapes.StrongEpi
CategoryTheory.StrongMono.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P Q : C} {f : P ⟶ Q},
  CategoryTheory.Mono f →
    (∀ ⦃X Y : C⦄ (z : X ⟶ Y) [CategoryTheory.Epi z], CategoryTheory.HasLiftingProperty z f) →
      CategoryTheory.StrongMono f
-- Init.Grind.Module.Envelope
_private.Init.Grind.Module.Envelope.0.Lean.Grind.IntModule.OfNatModule.helper : ∀ {α : Type u} [inst : Lean.Grind.NatModule α] (h : Equivalence (Lean.Grind.IntModule.OfNatModule.r α))
  (q₁ q₂ : Lean.Grind.IntModule.OfNatModule.Q α), q₁ = q₂ → Lean.Grind.IntModule.OfNatModule.rel✝ h q₁ q₂
-- Mathlib.Tactic.NormNum.NatLog
/-- Evaluates the `Nat.clog` function.
 -/
Mathlib.Meta.NormNum.evalNatClog : Mathlib.Meta.NormNum.NormNumExt
-- Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
/-- A subset of a collinear set is collinear.  -/
Collinear.subset : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {s₁ s₂ : Set P}, s₁ ⊆ s₂ → Collinear k s₂ → Collinear k s₁
-- Lean.Elab.BuiltinCommand
Lean.Elab.Command.failIfSucceeds : Lean.Elab.Command.CommandElabM Unit → Lean.Elab.Command.CommandElabM Unit
-- Std.Data.Iterators.Lemmas.Consumers.Monadic.Set
Std.IterM.toTreeSet_eq_fold : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : Std.Iterator α m β] [inst_2 : Std.IteratorLoop α m m]
  {it : Std.IterM m β} {cmp : β → β → Ordering}, it.toTreeSet cmp = Std.IterM.fold (fun acc a => acc.insert a) ∅ it
-- Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt
HasProd.hasProd_symmetricIco_of_hasProd_symmetricIcc : ∀ {α : Type u_1} {f : ℤ → α} [inst : CommGroup α] [inst_1 : TopologicalSpace α] [ContinuousMul α] {a : α},
  HasProd f a (SummationFilter.symmetricIcc ℤ) →
    Filter.Tendsto (fun N => (f ↑N)⁻¹) Filter.atTop (nhds 1) → HasProd f a (SummationFilter.symmetricIco ℤ)
-- Mathlib.CategoryTheory.Monoidal.CommComon_
CategoryTheory.CommComon.comon : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] → (self : CategoryTheory.CommComon C) → CategoryTheory.ComonObj self.X
-- Lean.Data.SSet
Lean.SSet.fold : {α : Type u} → [inst : BEq α] → [inst_1 : Hashable α] → {σ : Type u_1} → (σ → α → σ) → σ → Lean.SSet α → σ
-- Mathlib.NumberTheory.LSeries.Injectivity
/-- Assuming `f 0 = 0`, the `LSeries` of `f` is zero if and only if either `f = 0` or the
L-series converges nowhere.  -/
LSeries_eq_zero_iff : ∀ {f : ℕ → ℂ}, f 0 = 0 → (LSeries f = 0 ↔ f = 0 ∨ LSeries.abscissaOfAbsConv f = ⊤)
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithTerminal.instFaithfulIncl : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C], CategoryTheory.WithTerminal.incl.Faithful
-- Mathlib.LinearAlgebra.Span.Basic
Submodule.disjoint_span_singleton' : ∀ {K : Type u_3} {V : Type u_6} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  {s : Submodule K V} {x : V}, x ≠ 0 → (Disjoint s (K ∙ x) ↔ x ∉ s)
-- Mathlib.Algebra.BrauerGroup.Defs
/-- Two finite-dimensional central simple algebras `A` and `B` are Brauer equivalent
if there exist `n, m ∈ ℕ+` such that `Mₙ(A) ≃ₐ[K] Mₘ(B)`.  -/
IsBrauerEquivalent : {K : Type u} → [inst : Field K] → CSA K → CSA K → Prop
-- Init.Data.List.ToArray
Array.back?.eq_1 : ∀ {α : Type u} (xs : Array α), xs.back? = xs[xs.size - 1]?
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Algebra.surjective_algebraMap_iff : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A],
  Function.Surjective ⇑(algebraMap R A) ↔ ⊤ = ⊥
-- Mathlib.CategoryTheory.Sites.Pretopology
CategoryTheory.Pretopology.instInhabited : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasPullbacks C] → Inhabited (CategoryTheory.Pretopology C)
-- Mathlib.Tactic.Translate.ToDual
/-- An attribute that tells that certain arguments of this definition are not
involved when translating.
This helps the translation heuristic by also transforming definitions if `ℕ` or another
fixed type occurs as one of these arguments.  -/
Mathlib.Tactic.ToDual.to_dual_ignore_args : Lean.ParserDescr
-- Mathlib.Probability.Kernel.CondDistrib
MeasureTheory.AEStronglyMeasurable.comp_snd_map_prodMk : ∀ {β : Type u_2} {mβ : MeasurableSpace β} {Ω : Type u_5} {F : Type u_6} {mΩ : MeasurableSpace Ω} (X : Ω → β)
  {μ : MeasureTheory.Measure Ω} [inst : TopologicalSpace F] {f : Ω → F},
  MeasureTheory.AEStronglyMeasurable f μ →
    MeasureTheory.AEStronglyMeasurable (fun x => f x.2) (MeasureTheory.Measure.map (fun ω => (X ω, ω)) μ)
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.instInhabited.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C],
  CategoryTheory.AddMon.instInhabited = { default := CategoryTheory.AddMon.trivial C }
-- Mathlib.Algebra.Homology.Embedding.ExtendHomology
/-- The homology data of `(K.extend e).sc j'` that is deduced
from a homology data of `K.sc' i j k`.  -/
HomologicalComplex.extend.homologyData' : {ι : Type u_1} →
  {ι' : Type u_2} →
    {c : ComplexShape ι} →
      {c' : ComplexShape ι'} →
        {C : Type u_3} →
          [inst : CategoryTheory.Category.{v_1, u_3} C] →
            [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
              [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
                (K : HomologicalComplex C c) →
                  (e : c.Embedding c') →
                    {i j k : ι} →
                      {j' : ι'} →
                        e.f j = j' →
                          c.prev j = i → c.next j = k → (K.sc' i j k).HomologyData → ((K.extend e).sc j').HomologyData
-- Mathlib.Algebra.MonoidAlgebra.Division
AddMonoidAlgebra.mul_of'_divOf : ∀ {k : Type u_1} {G : Type u_2} [inst : Semiring k] [inst_1 : AddCommMonoid G] [inst_2 : IsCancelAdd G]
  (x : AddMonoidAlgebra k G) (a : G), (x * AddMonoidAlgebra.of' k G a).divOf a = x
-- Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
/-- To show a category is an `InitialMonoClass` it suffices to give an initial object such that
every morphism out of it is a monomorphism.  -/
CategoryTheory.Limits.InitialMonoClass.of_isInitial : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {I : C} (hI : CategoryTheory.Limits.IsInitial I),
  (∀ (X : C), CategoryTheory.Mono (hI.to X)) → CategoryTheory.Limits.InitialMonoClass C
-- Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
SSet.instIsDiscreteHomotopyCategoryObjTruncatedOfNatNatTruncationSimplexCategoryStdSimplexMk : CategoryTheory.IsDiscrete ((SSet.truncation 2).obj (SSet.stdSimplex.obj { len := 0 })).HomotopyCategory
-- Lean.Meta.Sym.AlphaShareCommon
Lean.Meta.Sym.AlphaKey.mk.injEq : ∀ (expr expr_1 : Lean.Expr), ({ expr := expr } = { expr := expr_1 }) = (expr = expr_1)
-- Lean.Meta.Tactic.Grind.PP
Lean.Meta.Grind.goalToMessageData : Lean.Meta.Grind.Goal → Lean.Grind.Config → Lean.MetaM Lean.MessageData
-- Mathlib.RingTheory.Bialgebra.SymmetricAlgebra
SymmetricAlgebra.instIsCocomm : ∀ (R : Type u_1) [inst : CommSemiring R] (M : Type u_2) [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  Coalgebra.IsCocomm R (SymmetricAlgebra R M)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Polynomial.Chebyshev.rootMultiplicity_T_real : ∀ {n k : ℕ},
  k < n → Polynomial.rootMultiplicity (Real.cos ((2 * ↑k + 1) * Real.pi / (2 * ↑n))) (Polynomial.Chebyshev.T ℝ ↑n) = 1
-- Mathlib.Tactic.FieldSimp
/-- Given `x` in a commutative group-with-zero, construct a new expression in the standard form
*** / *** (all denominators at the end) which is equal to `x`.  -/
Mathlib.Tactic.FieldSimp.reduceExprQ : {v : Lean.Level} →
  {M : Q(Type v)} →
    ({u : Lean.Level} → (type : Q(Sort u)) → Lean.MetaM Q(«$type»)) →
      Q(CommGroupWithZero «$M») → (x : Q(«$M»)) → Mathlib.Tactic.AtomM ((x' : Q(«$M»)) × Q(«$x» = «$x'»))
-- Mathlib.CategoryTheory.Preadditive.EilenbergMoore
CategoryTheory.Monad.algebraPreadditive_homGroup_add_f : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Preadditive C]
  (T : CategoryTheory.Monad C) [inst_2 : T.Additive] (F G : T.Algebra) (α β : F ⟶ G), (α + β).f = α.f + β.f
-- Mathlib.Topology.Homotopy.HomotopyGroup
ContinuousMap.uncurry.congr_simp : ∀ {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] [inst_3 : LocallyCompactSpace Y] (f f_1 : C(X, C(Y, Z))),
  f = f_1 → f.uncurry = f_1.uncurry
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.Parser.feature_ : Lean.ParserDescr
-- Std.Time.Date.PlainDate
Std.Time.PlainDate.mk.sizeOf_spec : ∀ (year : Std.Time.Year.Offset) (month : Std.Time.Month.Ordinal) (day : Std.Time.Day.Ordinal)
  (valid : year.Valid month day),
  sizeOf { year := year, month := month, day := day, valid := valid } =
    1 + sizeOf year + sizeOf month + sizeOf day + sizeOf valid
-- Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
WeierstrassCurve.instIsEllipticOfJ : ∀ {F : Type u_2} [inst : Field F] (j : F) [inst_1 : DecidableEq F], (WeierstrassCurve.ofJ j).IsElliptic
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.toArray_filterMapWithPostcondition : ∀ {α β γ : Type w} {m : Type w → Type w'} [inst : Monad m] [LawfulMonad m] [inst_2 : Std.Iterator α Id β]
  [Std.Iterators.Finite α Id] {f : β → Std.Iterators.PostconditionT m (Option γ)} (it : Std.IterM Id β),
  (Std.IterM.filterMapWithPostcondition f it).toArray = Array.filterMapM (fun x => (f x).run) it.toArray.run
-- Mathlib.CategoryTheory.Sites.MayerVietorisSquare
CategoryTheory.GrothendieckTopology.MayerVietorisSquare.mk.injEq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  [inst_1 : CategoryTheory.HasWeakSheafify J (Type v)] (toSquare : CategoryTheory.Square C)
  (mono_f₁₃ :
    autoParam (CategoryTheory.Mono toSquare.f₁₃)
      CategoryTheory.GrothendieckTopology.MayerVietorisSquare.mono_f₁₃._autoParam)
  (isPushout : (toSquare.map (CategoryTheory.yoneda.comp (CategoryTheory.presheafToSheaf J (Type v)))).IsPushout)
  (toSquare_1 : CategoryTheory.Square C)
  (mono_f₁₃_1 :
    autoParam (CategoryTheory.Mono toSquare_1.f₁₃)
      CategoryTheory.GrothendieckTopology.MayerVietorisSquare.mono_f₁₃._autoParam)
  (isPushout_1 : (toSquare_1.map (CategoryTheory.yoneda.comp (CategoryTheory.presheafToSheaf J (Type v)))).IsPushout),
  ({ toSquare := toSquare, mono_f₁₃ := mono_f₁₃, isPushout := isPushout } =
      { toSquare := toSquare_1, mono_f₁₃ := mono_f₁₃_1, isPushout := isPushout_1 }) =
    (toSquare = toSquare_1)
-- Mathlib.Logic.Denumerable
Denumerable.toEncodable : {α : Type u_3} → [self : Denumerable α] → Encodable α
-- Lean.Elab.Tactic.Omega.Frontend
_private.Lean.Elab.Tactic.Omega.Frontend.0.Lean.Elab.Tactic.Omega.asLinearComboImpl.handleNatCast : Lean.Expr →
  Lean.Expr →
    Lean.Expr →
      Lean.Elab.Tactic.Omega.OmegaM (Lean.Omega.LinearCombo × Lean.Elab.Tactic.Omega.OmegaM Lean.Expr × List Lean.Expr)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.getKeyD_alter_self : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp]
  [Inhabited α],
  t.WF →
    ∀ {k fallback : α} {f : Option β → Option β},
      (Std.DTreeMap.Raw.Const.alter t k f).getKeyD k fallback =
        if (f (Std.DTreeMap.Raw.Const.get? t k)).isSome = true then k else fallback
-- Mathlib.Topology.Metrizable.CompletelyMetrizable
/-- The disjoint union of two completely pseudometrizable spaces is completely pseudometrizable.  -/
TopologicalSpace.IsCompletelyPseudoMetrizableSpace.sum : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [TopologicalSpace.IsCompletelyPseudoMetrizableSpace X]
  [inst_2 : TopologicalSpace Y] [TopologicalSpace.IsCompletelyPseudoMetrizableSpace Y],
  TopologicalSpace.IsCompletelyPseudoMetrizableSpace (X ⊕ Y)
-- Mathlib.Topology.Closure
/-- Interior and frontier are disjoint.  -/
disjoint_interior_frontier : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, Disjoint (interior s) (frontier s)
-- Mathlib.Algebra.Polynomial.Basic
/-- Summing the values of a function applied to the coefficients of a polynomial  -/
Polynomial.sum : {R : Type u} → [inst : Semiring R] → {S : Type u_1} → [AddCommMonoid S] → Polynomial R → (ℕ → R → S) → S
-- Mathlib.GroupTheory.Perm.Fin
Fin.cycleType_cycleIcc_of_lt : ∀ {n : ℕ} {i j : Fin n}, i < j → (i.cycleIcc j).cycleType = {↑j - ↑i + 1}
-- Mathlib.Order.Filter.Basic
Filter.eventuallyLE_congr : ∀ {α : Type u} {β : Type v} [inst : LE β] {l : Filter α} {f f' g g' : α → β},
  f =ᶠ[l] f' → g =ᶠ[l] g' → (f ≤ᶠ[l] g ↔ f' ≤ᶠ[l] g')
-- Mathlib.Algebra.BigOperators.Group.Multiset.Defs
Multiset.nsmul_count : ∀ {M : Type u_3} [inst : AddCommMonoid M] {s : Multiset M} [inst_1 : DecidableEq M] (a : M),
  Multiset.count a s • a = (Multiset.filter (Eq a) s).sum
-- Mathlib.Analysis.Normed.Unbundled.AlgebraNorm
AlgebraNormClass.toRingNormClass : ∀ {F : Type u_1} {R : outParam (Type u_2)} {inst : SeminormedCommRing R} {S : outParam (Type u_3)} {inst_1 : Ring S}
  {inst_2 : Algebra R S} {inst_3 : FunLike F S ℝ} [self : AlgebraNormClass F R S], RingNormClass F S ℝ
-- Mathlib.Algebra.Category.Grp.Colimits
AddCommGrpCat.Colimits.Quot.desc_colimitCocone : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] [inst_1 : DecidableEq J]
  (F : CategoryTheory.Functor J AddCommGrpCat) [inst_2 : Small.{w, max u w} (AddCommGrpCat.Colimits.Quot F)],
  AddCommGrpCat.Colimits.Quot.desc F (AddCommGrpCat.Colimits.colimitCocone F) = Shrink.addEquiv.symm.toAddMonoidHom
-- Mathlib.Analysis.Normed.Group.Continuity
tendsto_zero_iff_enorm_tendsto_zero : ∀ {α : Type u_1} {E : Type u_4} [inst : SeminormedAddGroup E] {f : α → E} {a : Filter α},
  Filter.Tendsto f a (nhds 0) ↔ Filter.Tendsto (fun x => ‖f x‖ₑ) a (nhds 0)
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.Mor₂.whiskerLeft.injEq : ∀ (e : Lean.Expr) (isoLift? : Option Mathlib.Tactic.BicategoryLike.IsoLift) (f g h : Mathlib.Tactic.BicategoryLike.Mor₁)
  (η : Mathlib.Tactic.BicategoryLike.Mor₂) (e_1 : Lean.Expr) (isoLift?_1 : Option Mathlib.Tactic.BicategoryLike.IsoLift)
  (f_1 g_1 h_1 : Mathlib.Tactic.BicategoryLike.Mor₁) (η_1 : Mathlib.Tactic.BicategoryLike.Mor₂),
  (Mathlib.Tactic.BicategoryLike.Mor₂.whiskerLeft e isoLift? f g h η =
      Mathlib.Tactic.BicategoryLike.Mor₂.whiskerLeft e_1 isoLift?_1 f_1 g_1 h_1 η_1) =
    (e = e_1 ∧ isoLift? = isoLift?_1 ∧ f = f_1 ∧ g = g_1 ∧ h = h_1 ∧ η = η_1)
-- Mathlib.RingTheory.Ideal.Quotient.PowTransition
/-- The linear map from `M ⧸ I ^ m • ⊤` to `M ⧸ I ^ n • ⊤` induced by
the natural inclusion `I ^ n • ⊤ → I ^ m • ⊤`.

To future contributors: Before adding lemmas related to `Submodule.factorPow`, please
check whether it can be generalized to `Submodule.factor` and whether the
corresponding (more general) lemma for `Submodule.factor` already exists.
 -/
Submodule.factorPow : {R : Type u_1} →
  [inst : Ring R] →
    (I : Ideal R) →
      (M : Type u_2) →
        [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → {m n : ℕ} → m ≤ n → M ⧸ I ^ n • ⊤ →ₗ[R] M ⧸ I ^ m • ⊤
-- Mathlib.Data.EReal.Basic
EReal.eq_bot_iff_forall_lt : ∀ (x : EReal), x = ⊥ ↔ ∀ (y : ℝ), x < ↑y
-- Mathlib.Order.Interval.Multiset
Multiset.Ico_self : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] (a : α), Multiset.Ico a a = 0
-- Std.Http.Protocol.H1.Message
/-- Receiving and parsing incoming requests from clients.
 -/
Std.Http.Protocol.H1.Direction.receiving : Std.Http.Protocol.H1.Direction
-- Mathlib.AlgebraicGeometry.Birational.RationalMap
AlgebraicGeometry.Scheme.RationalMap.isOver_iff : ∀ {X Y S : AlgebraicGeometry.Scheme} [inst : X.Over S] [inst_1 : Y.Over S] {f : X.RationalMap Y},
  AlgebraicGeometry.Scheme.RationalMap.IsOver S f ↔
    f.compHom (Y ↘ S) = AlgebraicGeometry.Scheme.Hom.toRationalMap (X ↘ S)
-- Mathlib.Topology.MetricSpace.HausdorffDistance
IsOpen.exists_iUnion_isClosed : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {U : Set α},
  IsOpen U → ∃ F, (∀ (n : ℕ), IsClosed (F n)) ∧ (∀ (n : ℕ), F n ⊆ U) ∧ ⋃ n, F n = U ∧ Monotone F
-- Mathlib.LinearAlgebra.Matrix.Kronecker
/-- Produce a matrix with `f` applied to every pair of elements from `A` and `B`.  -/
Matrix.kroneckerMap : {α : Type u_3} →
  {β : Type u_5} →
    {γ : Type u_7} →
      {l : Type u_9} →
        {m : Type u_10} →
          {n : Type u_11} → {p : Type u_12} → (α → β → γ) → Matrix l m α → Matrix n p β → Matrix (l × n) (m × p) γ
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.IsAffineOpen.isoSpec.eq_1 : ∀ {X : AlgebraicGeometry.Scheme} {U : X.Opens} (hU : AlgebraicGeometry.IsAffineOpen U),
  hU.isoSpec = (↑U).isoSpec ≪≫ AlgebraicGeometry.Scheme.Spec.mapIso U.topIso.symm.op
-- Mathlib.CategoryTheory.Sites.Grothendieck
CategoryTheory.GrothendieckTopology.Cover.Arrow.mk.inj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {X : C} {J : CategoryTheory.GrothendieckTopology C}
  {S : J.Cover X} {Y : C} {f : Y ⟶ X} {hf : (↑S).arrows f} {Y_1 : C} {f_1 : Y_1 ⟶ X} {hf_1 : (↑S).arrows f_1},
  { Y := Y, f := f, hf := hf } = { Y := Y_1, f := f_1, hf := hf_1 } → Y = Y_1 ∧ f ≍ f_1
-- Init.Data.Option.Lemmas
Option.get!_choice : ∀ {α : Type u_1} [inst : Inhabited α], (Option.choice α).get! = (Option.choice α).get ⋯
-- Mathlib.Order.OrdContinuous
LeftOrdContinuous.iterate : ∀ {α : Type u} [inst : Preorder α] {f : α → α}, LeftOrdContinuous f → ∀ (n : ℕ), LeftOrdContinuous f^[n]
-- Mathlib.Order.SetNotation
/-- Intersection of a set of sets.  -/
Set.sInter : {α : Type u} → Set (Set α) → Set α
-- Mathlib.Analysis.BoxIntegral.Partition.Split
BoxIntegral.Prepartition.inf_split : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) (i : ι) (x : ℝ),
  π ⊓ BoxIntegral.Prepartition.split I i x = π.biUnion fun J => BoxIntegral.Prepartition.split J i x
-- Mathlib.Combinatorics.Additive.AP.Three.Defs
threeAPFree_vadd_set : ∀ {α : Type u_2} [inst : AddCommMonoid α] [IsCancelAdd α] {s : Set α} {a : α}, ThreeAPFree (a +ᵥ s) ↔ ThreeAPFree s
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.yoneda_obj_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (X : C) {X_1 Y : Cᵒᵖ} (f : X_1 ⟶ Y),
  (CategoryTheory.yoneda.obj X).map f = TypeCat.ofHom fun g => CategoryTheory.CategoryStruct.comp f.unop g
-- Mathlib.Topology.UrysohnsLemma
Urysohns.CU.open_U : ∀ {X : Type u_2} [inst : TopologicalSpace X] {P : Set X → Set X → Prop} (self : Urysohns.CU P), IsOpen self.U
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.eraseIdx.match_1.splitter : {α : Type u_1} →
  (motive : List α → ℕ → Sort u_2) →
    (x : List α) →
      (x_1 : ℕ) →
        ((x : ℕ) → motive [] x) →
          ((head : α) → (as : List α) → motive (head :: as) 0) →
            ((a : α) → (as : List α) → (n : ℕ) → motive (a :: as) n.succ) → motive x x_1
-- Mathlib.CategoryTheory.Limits.Chosen.End
CategoryTheory.Limits.chosenEndFunctor_obj : ∀ {J : Type u_3} {C : Type u_4} [inst : CategoryTheory.Category.{v_3, u_4} C]
  [inst_1 : CategoryTheory.Category.{v_4, u_3} J] [inst_2 : CategoryTheory.Limits.ChosenEndsOfShape J C]
  (F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)),
  CategoryTheory.Limits.chosenEndFunctor.obj F = CategoryTheory.Limits.chosenEnd F
-- Mathlib.NumberTheory.Real.Irrational
/-- A real number is irrational if it is not equal to any rational number.  -/
Irrational : ℝ → Prop
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
/-- The triangle inequality on vectors `x`, `y`, `z` is an equality if and only if
`angle x z = π`, or `y` is a nonnegative linear combination of `x` and `z`.  -/
InnerProductGeometry.angle_eq_angle_add_angle_iff : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y z : V},
  y ≠ 0 →
    (InnerProductGeometry.angle x z = InnerProductGeometry.angle x y + InnerProductGeometry.angle y z ↔
      InnerProductGeometry.angle x z = Real.pi ∨ y ∈ Submodule.span NNReal {x, z})
-- Mathlib.Order.WithBot
WithBot.coe_eq_top : ∀ {α : Type u_1} [inst : Top α] {a : α}, ↑a = ⊤ ↔ a = ⊤
-- Mathlib.LinearAlgebra.Complex.Module
imaginaryPart_ofReal : ∀ (r : ℝ), imaginaryPart ↑r = 0
-- Lean.Data.Lsp.Ipc
_private.Lean.Data.Lsp.Ipc.0.Lean.Lsp.Ipc.expandModuleHierarchyImportedBy.go : ℕ → Lean.Lsp.LeanImport → Std.TreeSet String compare → Lean.Lsp.Ipc.IpcM (Lean.Lsp.Ipc.ModuleHierarchy × ℕ)
-- Mathlib.Tactic.NormNum.NatLog
Mathlib.Meta.NormNum.nat_clog_zero_right : ∀ (b n : ℕ), n.ble 1 = true → Nat.clog b n = 0
-- Mathlib.Topology.Baire.Lemmas
/-- In a Baire space, every nonempty open set is non‐meagre,
that is, it cannot be written as a countable union of nowhere‐dense sets.
 -/
not_isMeagre_of_isOpen : ∀ {X : Type u_1} [inst : TopologicalSpace X] [BaireSpace X] {s : Set X}, IsOpen s → s.Nonempty → ¬IsMeagre s
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.instIsScalarTower : ∀ {m : Type u_1} {n : Type u_2} {R : Type u_3} {S : Type u_4} {A : Type u_5} [inst : SMul R S] [inst_1 : SMul R A]
  [inst_2 : SMul S A] [IsScalarTower R S A], IsScalarTower R S (CStarMatrix m n A)
-- Mathlib.Algebra.Module.LinearMap.Defs
/-- Scalar multiplication by `R` of `M` can be moved through linear maps.  -/
LinearMap.CompatibleSMul.map_smul : ∀ {M : Type u_8} {M₂ : Type u_10} {inst : AddCommMonoid M} {inst_1 : AddCommMonoid M₂} {R : Type u_14} {S : Type u_15}
  {inst_2 : Semiring S} {inst_3 : SMul R M} {inst_4 : Module S M} {inst_5 : SMul R M₂} {inst_6 : Module S M₂}
  [self : LinearMap.CompatibleSMul M M₂ R S] (fₗ : M →ₗ[S] M₂) (c : R) (x : M), fₗ (c • x) = c • fₗ x
-- Mathlib.GroupTheory.OreLocalization.Basic
OreLocalization.oreDiv_mul_oreDiv : ∀ {R : Type u_1} [inst : Monoid R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S] {r₁ r₂ : R} {s₁ s₂ : ↥S},
  r₁ /ₒ s₁ * (r₂ /ₒ s₂) = OreLocalization.oreNum r₁ s₂ * r₂ /ₒ (OreLocalization.oreDenom r₁ s₂ * s₁)
-- Mathlib.Computability.TuringMachine.PostTuringMachine
/-- The translated TM0 machine (given the TM1 machine input).  -/
Turing.TM1to0.tr : {Γ : Type u_1} →
  {Λ : Type u_2} →
    [inst : Inhabited Λ] →
      {σ : Type u_3} →
        [inst_1 : Inhabited σ] → (M : Λ → Turing.TM1.Stmt Γ Λ σ) → Turing.TM0.Machine Γ (Turing.TM1to0.Λ' M)
-- Mathlib.Tactic.NormNum.Eq
_private.Mathlib.Tactic.NormNum.Eq.0.Mathlib.Meta.NormNum.evalEq.ratArm : {v : Lean.Level} →
  {β : Q(Type v)} →
    (e : Q(«$β»)) →
      (u : Lean.Level) →
        (α :
            have u := u;
            Q(Type u)) →
          (a b : Q(«$α»)) →
            Mathlib.Meta.NormNum.Result a →
              Mathlib.Meta.NormNum.Result b → Q(DivisionRing «$α») → Lean.MetaM (Mathlib.Meta.NormNum.Result e)
-- Mathlib.Tactic.Translate.Core
/-- `TranslationInfo` stores the information of how to translate a constant.  -/
Mathlib.Tactic.Translate.TranslationInfo : Type
-- Mathlib.Tactic.FunProp.Types
Mathlib.Meta.FunProp.instBEqConfig.beq : Mathlib.Meta.FunProp.Config → Mathlib.Meta.FunProp.Config → Bool