mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getKeyGE?.go.eq_2 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α) (best : Option α) (size : ℕ) (k' : α) (v : β k')
  (l r : Std.DTreeMap.Internal.Impl α β),
  Std.DTreeMap.Internal.Impl.getKeyGE?.go k best (Std.DTreeMap.Internal.Impl.inner size k' v l r) =
    match compare k k' with
    | Ordering.lt => Std.DTreeMap.Internal.Impl.getKeyGE?.go k (some k') l
    | Ordering.eq => some k'
    | Ordering.gt => Std.DTreeMap.Internal.Impl.getKeyGE?.go k best r
-- Mathlib.AlgebraicGeometry.ResidueField
/-- The residue fields of `Spec R` are isomorphic to `Ideal.ResidueField`.  -/
AlgebraicGeometry.Scheme.Spec.residueFieldIso : (R : CommRingCat) →
  (x : ↥(AlgebraicGeometry.Spec R)) → (AlgebraicGeometry.Spec R).residueField x ≅ CommRingCat.of x.asIdeal.ResidueField
-- Mathlib.Data.Set.Image
Set.image_preimage_eq_inter_range : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {t : Set β}, f '' f ⁻¹' t = t ∩ Set.range f
-- Lean.Meta.WHNF
_private.Lean.Meta.WHNF.0.Lean.Meta.getRecRuleFor : Lean.RecursorVal → Lean.Expr → Option Lean.RecursorRule
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.size_union_le_size_add_size : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashSet α} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α], (m₁ ∪ m₂).size ≤ m₁.size + m₂.size
-- Mathlib.Geometry.Manifold.Instances.Icc
Homeomorph.pointReflection.congr_simp : ∀ {V : Type u_4} {P : Type u_5} [inst : AddGroup V] [inst_1 : TopologicalSpace V] [inst_2 : AddTorsor V P]
  [inst_3 : TopologicalSpace P] [inst_4 : IsTopologicalAddTorsor P] (p p_1 : P),
  p = p_1 → Homeomorph.pointReflection p = Homeomorph.pointReflection p_1
-- Mathlib.CategoryTheory.Limits.Opposites
CategoryTheory.Limits.hasFiniteWidePushouts_opposite_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C],
  CategoryTheory.Limits.HasFiniteWidePushouts Cᵒᵖ ↔ CategoryTheory.Limits.HasFiniteWidePullbacks C
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.isSome_max?_of_isSome_max?_erase : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α}, (t.erase k).max?.isSome = true → t.max?.isSome = true
-- Mathlib.FieldTheory.Extension
IntermediateField.Lifts.instOrderBot : {F : Type u_1} →
  {E : Type u_2} →
    {K : Type u_3} →
      [inst : Field F] →
        [inst_1 : Field E] →
          [inst_2 : Field K] →
            [inst_3 : Algebra F E] → [inst_4 : Algebra F K] → OrderBot (IntermediateField.Lifts F E K)
-- Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
_private.Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm.0.smoothingSeminormSeq_tendsto_aux : ∀ {R : Type u_1} [inst : CommRing R] (μ : RingSeminorm R) {L : ℝ},
  0 ≤ L →
    ∀ {ε : ℝ},
      0 < ε →
        ∀ {m1 : ℕ},
          0 < m1 →
            ∀ {x : R},
              μ x ≠ 0 →
                Filter.Tendsto (fun n => (L + ε) ^ (-(↑(n % m1) / ↑n)) * (μ x ^ (n % m1)) ^ (1 / ↑n)) Filter.atTop
                  (nhds 1)
-- Init.GrindInstances.Ring.SInt
Lean.Grind.instPowInt8SintOfNatNat : Lean.Grind.ToInt.Pow Int8 (Lean.Grind.IntInterval.sint 8)
-- Mathlib.Geometry.RingedSpace.PresheafedSpace
AlgebraicGeometry.PresheafedSpace.c_isIso_of_iso : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : AlgebraicGeometry.PresheafedSpace C} (f : X ⟶ Y)
  [CategoryTheory.IsIso f], CategoryTheory.IsIso f.c
-- Mathlib.Analysis.Convex.Deriv
/-- If a function `f` is twice differentiable on an open convex set `D ⊆ ℝ` and
`f''` is nonnegative on `D`, then `f` is convex on `D`.  -/
convexOn_of_deriv2_nonneg' : ∀ {D : Set ℝ},
  Convex ℝ D →
    ∀ {f : ℝ → ℝ},
      DifferentiableOn ℝ f D → DifferentiableOn ℝ (deriv f) D → (∀ x ∈ D, 0 ≤ deriv^[2] f x) → ConvexOn ℝ D f
-- Mathlib.Order.Antisymmetrization
/-- The antisymmetrization of a product preorder is order isomorphic
to the product of antisymmetrizations.  -/
Antisymmetrization.prodEquiv : (α : Type u_1) →
  (β : Type u_2) →
    [inst : Preorder α] →
      [inst_1 : Preorder β] →
        (Antisymmetrization (α × β) fun x1 x2 => x1 ≤ x2) ≃o
          (Antisymmetrization α fun x1 x2 => x1 ≤ x2) × Antisymmetrization β fun x1 x2 => x1 ≤ x2
-- Mathlib.Algebra.Central.Basic
Algebra.IsCentral.center_eq_bot : ∀ (K : Type u) [inst : CommSemiring K] (D : Type v) [inst_1 : Semiring D] [inst_2 : Algebra K D]
  [h : Algebra.IsCentral K D], Subalgebra.center K D = ⊥
-- Mathlib.Analysis.Convex.SpecificFunctions.Basic
/-- `Real.exp` is convex on the whole real line.  -/
convexOn_exp : ConvexOn ℝ Set.univ Real.exp
-- Mathlib.Analysis.Complex.Norm
Complex.dist_self_conj : ∀ (z : ℂ), dist z ((starRingEnd ℂ) z) = 2 * |z.im|
-- Mathlib.Order.Interval.Set.UnorderedInterval
Set.Ioc_subset_uIoc : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, Set.Ioc a b ⊆ Set.uIoc a b
-- Mathlib.CategoryTheory.Monoidal.OfHasFiniteProducts
CategoryTheory.symmetricOfHasFiniteCoproducts_braiding : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasInitial C]
  [inst_2 : CategoryTheory.Limits.HasBinaryCoproducts C] (P Q : C), β_ P Q = CategoryTheory.Limits.coprod.braiding P Q
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
/-- `spanningCoe` is equivalent to `coe` for a subgraph that `IsSpanning`.  -/
SimpleGraph.Subgraph.spanningCoeEquivCoeOfSpanning : {V : Type u} → {G : SimpleGraph V} → (G' : G.Subgraph) → G'.IsSpanning → G'.spanningCoe ≃g G'.coe
-- Mathlib.RingTheory.Unramified.Locus
Algebra.exists_unramified_of_isUnramifiedAt : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [Algebra.FiniteType R A] (p : Ideal A) [inst_4 : p.IsPrime] [Algebra.IsUnramifiedAt R p],
  ∃ f ∉ p, Algebra.Unramified R (Localization.Away f)
-- Mathlib.Topology.Constructions.SumProd
IsOpenQuotientMap.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},
  IsOpenQuotientMap f → IsOpenQuotientMap g → IsOpenQuotientMap (Prod.map f g)
-- Mathlib.Topology.Covering.Quotient
Topology.IsQuotientMap.isAddQuotientCoveringMap_of_isDiscrete_ker_addMonoidHom : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] [inst_2 : AddGroup E]
  [IsTopologicalAddGroup E] [inst_4 : AddGroup X] {f : E →+ X},
  Topology.IsQuotientMap ⇑f → IsDiscrete ↑f.ker → IsAddQuotientCoveringMap ⇑f ↥f.ker
-- Mathlib.Topology.Category.Profinite.AsLimit
/-- The functor `DiscreteQuotient X ⥤ Fintype` whose limit is isomorphic to `X`.  -/
Profinite.fintypeDiagram : (X : Profinite) → CategoryTheory.Functor (DiscreteQuotient ↑X.toTop) FintypeCat
-- Mathlib.CategoryTheory.Shift.Opposite
/-- The obvious isomorphism between `OppositeShift.functor (F ⋙ G)` and the
composition of `OppositeShift.functor F` and `OppositeShift.functor G`.
 -/
CategoryTheory.NatTrans.OppositeShift.natIsoComp : {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] →
        (A : Type u_3) →
          [inst_2 : AddMonoid A] →
            [inst_3 : CategoryTheory.HasShift C A] →
              [inst_4 : CategoryTheory.HasShift D A] →
                (F : CategoryTheory.Functor C D) →
                  {E : Type u_4} →
                    [inst_5 : CategoryTheory.Category.{v_3, u_4} E] →
                      [inst_6 : CategoryTheory.HasShift E A] →
                        (G : CategoryTheory.Functor D E) →
                          CategoryTheory.OppositeShift.functor A (F.comp G) ≅
                            (CategoryTheory.OppositeShift.functor A F).comp (CategoryTheory.OppositeShift.functor A G)
-- Mathlib.Analysis.SpecialFunctions.Bernstein
/-- The Bernstein approximations
```
∑ k : Fin (n+1), f (k/n : ℝ) * n.choose k * x^k * (1-x)^(n-k)
```
for a continuous function `f : C([0,1], ℝ)` converge uniformly to `f` as `n` tends to infinity.

This is the proof given in [Richard Beals' *Analysis, an introduction*][beals-analysis], §7D,
and reproduced on wikipedia.
 -/
bernsteinApproximation_uniform : ∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : TopologicalSpace E] [inst_2 : IsTopologicalAddGroup E]
  [inst_3 : Module ℝ E] [inst_4 : ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] (f : C(↑unitInterval, E)),
  Filter.Tendsto (fun n => bernsteinApproximation n f) Filter.atTop (nhds f)
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
CategoryTheory.CostructuredArrow.mapCompιCompGrothendieckProj_inv_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (L : CategoryTheory.Functor C D) {X Y : D} (f : X ⟶ Y) (X_1 : CategoryTheory.CostructuredArrow L X),
  (CategoryTheory.CostructuredArrow.mapCompιCompGrothendieckProj L f).inv.app X_1 =
    CategoryTheory.CategoryStruct.id X_1.left
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStruct
SSet.Edge.ofEq_edge : ∀ {X : SSet} {x₀ x₁ y₀ y₁ : X.obj (Opposite.op { len := 0 })} (e : SSet.Edge x₀ x₁) (h₀ : x₀ = y₀) (h₁ : x₁ = y₁),
  (e.ofEq h₀ h₁).edge = e.edge
-- Mathlib.Algebra.Lie.Weights.Basic
LieModule.coe_genWeightSpace_of_top : ∀ {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] (χ : L → R),
  ↑(LieModule.genWeightSpace M (χ ∘ ⇑⊤.incl)) = ↑(LieModule.genWeightSpace M χ)
-- Mathlib.Analysis.SpecialFunctions.Arsinh
ContinuousAt.arsinh : ∀ {X : Type u_1} [inst : TopologicalSpace X] {f : X → ℝ} {a : X},
  ContinuousAt f a → ContinuousAt (fun x => Real.arsinh (f x)) a
-- Lean.Data.FuzzyMatching
_private.Lean.Data.FuzzyMatching.0.Lean.FuzzyMatching.fuzzyMatchCore.set : String →
  Array Lean.FuzzyMatching.Score✝ →
    ℕ → ℕ → Lean.FuzzyMatching.Score✝ → Lean.FuzzyMatching.Score✝ → Array Lean.FuzzyMatching.Score✝
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Real.arcsin.eq_1 : Real.arcsin = Subtype.val ∘ Set.IccExtend Real.arcsin._proof_2 ⇑Real.sinOrderIso.symm
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
MonoidAlgebra.mapRingEquiv.eq_1 : ∀ {R : Type u_3} {S : Type u_4} (M : Type u_6) [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : Monoid M]
  (e : R ≃+* S),
  MonoidAlgebra.mapRingEquiv M e =
    RingEquiv.ofRingHom (MonoidAlgebra.mapRingHom M ↑e) (MonoidAlgebra.mapRingHom M ↑e.symm) ⋯ ⋯
-- Mathlib.Algebra.Module.LinearMap.Basic
DomMulAct.mk_smul_linearMap_apply : ∀ {R : Type u_1} {R' : Type u_2} {M : Type u_4} {M' : Type u_5} [inst : Semiring R] [inst_1 : Semiring R']
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M'] [inst_4 : Module R M] [inst_5 : Module R' M'] {σ₁₂ : R →+* R'}
  {S' : Type u_6} [inst_6 : Monoid S'] [inst_7 : DistribMulAction S' M] [inst_8 : SMulCommClass R S' M] (a : S')
  (f : M →ₛₗ[σ₁₂] M') (x : M), (DomMulAct.mk a • f) x = f (a • x)
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas
MeasureTheory.AEStronglyMeasurable.comp_measurePreserving : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {g : α → β} {γ : Type u_4} {x : MeasurableSpace γ}
  {x_1 : MeasurableSpace α} {f : γ → α} {μ : MeasureTheory.Measure γ} {ν : MeasureTheory.Measure α},
  MeasureTheory.AEStronglyMeasurable g ν →
    MeasureTheory.MeasurePreserving f μ ν → MeasureTheory.AEStronglyMeasurable (g ∘ f) μ
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddSubsemigroup.map_comap_eq : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] (f : M →ₙ+ N) (S : AddSubsemigroup N),
  AddSubsemigroup.map f (AddSubsemigroup.comap f S) = S ⊓ f.srange
-- Mathlib.Geometry.Euclidean.Sphere.Basic
/-- For a point on a sphere, the norm of its displacement from the center equals the radius.  -/
EuclideanGeometry.norm_vsub_center_eq_radius : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : MetricSpace P] [inst_2 : NormedAddTorsor V P]
  {s : EuclideanGeometry.Sphere P} {p : P}, p ∈ s → ‖p -ᵥ s.center‖ = s.radius
-- Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
/-- The bound on the degree of the polynomials used to describe the constructible set appearing in
Chevalley's theorem with complexity bound.  -/
ChevalleyThm.degBound : ℕ → (m : ℕ) → ℕ → Multiset (Fin m) → ℕ
-- Mathlib.Data.FunLike.Basic
DFunLike.coe_fn_eq : ∀ {F : Sort u_1} {α : Sort u_2} {β : α → Sort u_3} [i : DFunLike F α β] {f g : F}, ⇑f = ⇑g ↔ f = g
-- Mathlib.Algebra.Polynomial.Splits
Polynomial.Splits.zero : ∀ {R : Type u_1} [inst : Semiring R], Polynomial.Splits 0
-- Std.Data.DHashMap.Internal.Model
_private.Std.Data.DHashMap.Internal.Model.0.Std.DHashMap.Internal.Raw₀.getThenInsertIfNew?.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α] (a : α) (b : β a) (size : ℕ)
  (buckets : Array (Std.DHashMap.Internal.AssocList α β)) (hm : 0 < { size := size, buckets := buckets }.buckets.size),
  Std.DHashMap.Internal.Raw₀.getThenInsertIfNew? ⟨{ size := size, buckets := buckets }, hm⟩ a b =
    match Std.DHashMap.Internal.mkIdx buckets.size hm (hash a) with
    | ⟨i, h⟩ =>
      let bkt := buckets[i];
      match Std.DHashMap.Internal.AssocList.getCast? a bkt with
      | none =>
        have size' := size + 1;
        let buckets' := buckets.uset i (Std.DHashMap.Internal.AssocList.cons a b bkt) h;
        (none, Std.DHashMap.Internal.Raw₀.expandIfNecessary ⟨{ size := size', buckets := buckets' }, ⋯⟩)
      | some v => (some v, ⟨{ size := size, buckets := buckets }, hm⟩)
-- Mathlib.Order.Defs.PartialOrder
/-- **Alias** of `lt_asymm`. -/
not_lt_of_gt : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, a < b → ¬b < a
-- Mathlib.Algebra.Category.MonCat.Basic
MonCat.ofHom_id : ∀ {M : Type u} [inst : Monoid M], MonCat.ofHom (MonoidHom.id M) = CategoryTheory.CategoryStruct.id (MonCat.of M)
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
HasFTaylorSeriesUpTo.of_le : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {m n : WithTop ℕ∞} {p : E → FormalMultilinearSeries 𝕜 E F},
  HasFTaylorSeriesUpTo n f p → m ≤ n → HasFTaylorSeriesUpTo m f p
-- Lean.Elab.MutualInductive
Lean.Elab.Command.InductiveElabStep3.mk.injEq : ∀ (finalize finalize_1 : Lean.Elab.TermElabM Unit),
  ({ finalize := finalize } = { finalize := finalize_1 }) = (finalize = finalize_1)
-- Mathlib.Data.NNReal.Defs
Real.toNNReal_lt_natCast : ∀ {r : ℝ} {n : ℕ}, n ≠ 0 → (r.toNNReal < ↑n ↔ r < ↑n)
-- Batteries.Recycling.RBTree.Lemmas
_private.Batteries.Recycling.RBTree.Lemmas.0.RBTree.RBNode.foldl.match_1.eq_2 : ∀ {σ : Sort u_3} {α : Type u_1} (motive : σ → RBTree.RBNode α → Sort u_2) (b : σ) (c : RBTree.RBColor)
  (l : RBTree.RBNode α) (v : α) (r : RBTree.RBNode α) (h_1 : (b : σ) → motive b RBTree.RBNode.nil)
  (h_2 :
    (b : σ) →
      (c : RBTree.RBColor) →
        (l : RBTree.RBNode α) → (v : α) → (r : RBTree.RBNode α) → motive b (RBTree.RBNode.node c l v r)),
  (match b, RBTree.RBNode.node c l v r with
    | b, RBTree.RBNode.nil => h_1 b
    | b, RBTree.RBNode.node c l v r => h_2 b c l v r) =
    h_2 b c l v r
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.MemLp.coeFn_toLp : ∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] {f : α → E} (hf : MeasureTheory.MemLp f p μ), ↑↑(MeasureTheory.MemLp.toLp f hf) =ᵐ[μ] f
-- Mathlib.Order.Hom.Basic
OrderHom.snd_comp_prod : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  (f : α →o β) (g : α →o γ), OrderHom.snd.comp (f.prod g) = g
-- Mathlib.CategoryTheory.Sigma.Basic
/-- The inclusion functor into the disjoint union of categories.  -/
CategoryTheory.Sigma.incl : {I : Type w₁} →
  {C : I → Type u₁} →
    [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] → (i : I) → CategoryTheory.Functor (C i) ((i : I) × C i)
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
CategoryTheory.Functor.PreOneHypercoverDenseData.w_assoc : ∀ {C₀ : Type u₀} {C : Type u} [inst : CategoryTheory.Category.{v₀, u₀} C₀] [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor C₀ C} {S : C} (self : F.PreOneHypercoverDenseData S) ⦃i₁ i₂ : self.I₀⦄ (j : self.I₁ i₁ i₂)
  {Z : C} (h : S ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.map (self.p₁ j)) (CategoryTheory.CategoryStruct.comp (self.f i₁) h) =
    CategoryTheory.CategoryStruct.comp (F.map (self.p₂ j)) (CategoryTheory.CategoryStruct.comp (self.f i₂) h)
-- Mathlib.FieldTheory.RatFunc.AsPolynomial
/-- `eval` is a multiplicative homomorphism except when a denominator evaluates to `0`.

Counterexample: `eval _ 0 X * eval _ 0 (1/X) = 0 ≠ 1 = eval _ 0 1 = eval _ 0 (X * 1/X)`.

See also `RatFunc.eval₂_denom_ne_zero` to make the hypotheses simpler but less general.
 -/
RatFunc.eval_mul : ∀ {K : Type u} [inst : Field K] {L : Type u} [inst_1 : Field L] (f : K →+* L) (a : L) {x y : RatFunc K},
  Polynomial.eval₂ f a x.denom ≠ 0 →
    Polynomial.eval₂ f a y.denom ≠ 0 → RatFunc.eval f a (x * y) = RatFunc.eval f a x * RatFunc.eval f a y
-- Mathlib.Order.BoundedOrder.Lattice
sup_top_eq : ∀ {α : Type u_1} [inst : SemilatticeSup α] [inst_1 : OrderTop α] (a : α), a ⊔ ⊤ = ⊤
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basic
Tactic.ComputeAsymptotics.MultiseriesExpansion.monomial_toFun' : ∀ {basis : Tactic.ComputeAsymptotics.Basis} {n : Fin (List.length basis)},
  (Tactic.ComputeAsymptotics.MultiseriesExpansion.monomial basis ↑n).toFun = basis[n]
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.getD_diff_of_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {fallback : β},
  k ∈ m₂ → Std.ExtDHashMap.Const.getD (m₁ \ m₂) k fallback = fallback
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
MeasureTheory.ComplexMeasure.integrable_rnDeriv : ∀ {α : Type u_1} {m : MeasurableSpace α} (c : MeasureTheory.ComplexMeasure α) (μ : MeasureTheory.Measure α),
  MeasureTheory.Integrable (c.rnDeriv μ) μ
-- Mathlib.Order.Filter.AtTopBot.Disjoint
Filter.disjoint_pure_atTop : ∀ {α : Type u_3} [inst : Preorder α] [NoTopOrder α] (x : α), Disjoint (pure x) Filter.atTop
-- Init.Data.String.Lemmas.Splits
String.splits_singleton_right_iff : ∀ {s : String} {p : s.Pos} {c : Char} {t : String},
  p.Splits t (String.singleton c) ↔
    ∃ (h : s.endPos ≠ s.startPos), p = s.endPos.prev h ∧ (s.endPos.prev h).get ⋯ = c ∧ s = t ++ String.singleton c
-- Mathlib.Logic.Basic
forall_cond_comm : ∀ {α : Sort u_1} {s : α → Prop} {p : α → α → Prop},
  (∀ (a : α), s a → ∀ (b : α), s b → p a b) ↔ ∀ (a b : α), s a → s b → p a b
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.liftE_ιE_fromOpcycles : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (f₂₃ : j ⟶ l)
  (h₂₃ : CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ n₂ : ℤ) {A : C}
  (x : A ⟶ (X.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ f₂₃))
  (h :
    CategoryTheory.CategoryStruct.comp x ((X.H n₁).map (CategoryTheory.ComposableArrows.twoδ₁Toδ₀ f₂ f₃ f₂₃ h₂₃)) = 0)
  (hn₂ : n₁ + 1 = n₂) (h' : CategoryTheory.CategoryStruct.comp x (X.δ f₁ f₂₃ n₁ n₂ hn₂) = 0)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.liftE_ιE_fromOpcycles._auto_1),
  CategoryTheory.CategoryStruct.comp (X.liftE f₁ f₂ f₃ f₂₃ h₂₃ n₀ n₁ n₂ x h hn₂ h' hn₁)
      (CategoryTheory.CategoryStruct.comp (X.ιE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂) (X.fromOpcycles f₂ f₃ f₂₃ h₂₃ n₁)) =
    x
-- Mathlib.MeasureTheory.OuterMeasure.Operations
MeasureTheory.OuterMeasure.instCompleteLattice : {α : Type u_1} → CompleteLattice (MeasureTheory.OuterMeasure α)
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.leftUnitor_naturality : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : B} {f g : a ⟶ b} (η : f ⟶ g),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (CategoryTheory.CategoryStruct.id a) η)
      (CategoryTheory.Bicategory.leftUnitor g).hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor f).hom η
-- Mathlib.Tactic.Sat.FromLRAT
/-- Core of `fromLRAT`. Constructs the context and main proof definitions,
but not the reification theorem. Returns:

  * `nvars`: the number of variables specified in the CNF file
  * `ctx`: The abbreviated formula, a constant like `foo.ctx_1`
  * `ctx'`: The definitional expansion of the formula, a tree of `Fmla.and` nodes
  * `proof`: A proof of `ctx.proof []`
 -/
Mathlib.Tactic.Sat.fromLRATAux : String → String → Lean.Name → Lean.MetaM (ℕ × Lean.Expr × Lean.Expr × Lean.Expr)
-- Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
CategoryTheory.Precoverage.mem_toGrothendieck_iff_of_isStableUnderComposition : ∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] {J : CategoryTheory.Precoverage C}
  [J.IsStableUnderComposition] [J.IsStableUnderBaseChange] [J.HasPullbacks] [J.HasIsos] {X : C}
  {S : CategoryTheory.Sieve X}, S ∈ J.toGrothendieck X ↔ ∃ R ∈ J.coverings X, R ≤ S.arrows
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
AddLECancellable.of_add_left : ∀ {α : Type u_1} [inst : LE α] [inst_1 : AddCommSemigroup α] [AddLeftMono α] {a b : α},
  AddLECancellable (a + b) → AddLECancellable a
-- Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
jacobiTheta₂'_add_right : ∀ (z τ : ℂ), jacobiTheta₂' z (τ + 2) = jacobiTheta₂' z τ
-- Mathlib.Geometry.Manifold.GroupLieAlgebra
mulInvariantVectorField_add : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4}
  [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : Group G] (v w : GroupLieAlgebra I G),
  mulInvariantVectorField (v + w) = mulInvariantVectorField v + mulInvariantVectorField w
-- Lean.DocString.Syntax
/-- A named URL that can be used in links and images.
 -/
Lean.Doc.Syntax.link_ref : Lean.ParserDescr
-- Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
Subgroup.instHasDetOneMinGeneralLinearGroup_1 : ∀ {n : Type u_1} [inst : Fintype n] [inst_1 : DecidableEq n] {R : Type u_2} [inst_2 : CommRing R]
  (Γ Γ' : Subgroup (GL n R)) [Γ.HasDetOne], (Γ' ⊓ Γ).HasDetOne
-- Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
/-- If the left-most part is not `{0}`, then the part containing `0` has at least two elements:
either because it's the left-most part, and then it's not just `0` by assumption, or because it's
not the left-most part and then, by increasingness of maximal elements in parts, it contains
a positive element.  -/
OrderedFinpartition.one_lt_partSize_index_zero : ∀ {n : ℕ} (c : OrderedFinpartition (n + 1)), Set.range (c.emb 0) ≠ {0} → 1 < c.partSize (c.index 0)
-- Init.Data.Order.Ord
Std.instTransCmpCompareLex : ∀ {α : Type u_1} {cmp₁ cmp₂ : α → α → Ordering} [Std.TransCmp cmp₁] [Std.TransCmp cmp₂],
  Std.TransCmp (compareLex cmp₁ cmp₂)
-- Mathlib.Order.Monotone.Monovary
monovaryOn_const_left : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] (g : ι → β) (a : α)
  (s : Set ι), MonovaryOn (Function.const ι a) g s
-- Mathlib.Analysis.Convex.Combination
Finset.centerMass_le_sup : ∀ {R : Type u_1} {ι : Type u_5} {α : Type u_7} [inst : Field R] [inst_1 : AddCommGroup α] [inst_2 : LinearOrder α]
  [inst_3 : Module R α] [inst_4 : LinearOrder R] [IsOrderedAddMonoid α] [PosSMulMono R α] {s : Finset ι} {f : ι → α}
  {w : ι → R} (hw₀ : ∀ i ∈ s, 0 ≤ w i) (hw₁ : 0 < ∑ i ∈ s, w i), s.centerMass w f ≤ s.sup' ⋯ f
-- Init.Data.Nat.Basic
Nat.not_le_eq : ∀ (a b : ℕ), (¬a ≤ b) = (b + 1 ≤ a)
-- Mathlib.Order.Hom.BoundedLattice
/-- `Subtype.val` as a `SupBotHom`.  -/
SupBotHom.subtypeVal : {β : Type u_3} →
  [inst : SemilatticeSup β] →
    [inst_1 : OrderBot β] →
      {P : β → Prop} → (Pbot : P ⊥) → (Psup : ∀ ⦃x y : β⦄, P x → P y → P (x ⊔ y)) → SupBotHom { x // P x } β