mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
/-- Taylor formal composition of two formal multilinear series. The `n`-th coefficient in the
composition is defined to be the sum of `q.compAlongOrderedFinpartition p c` over all
ordered partitions of `n`.
In other words, this term (as a multilinear function applied to `v₀, ..., vₙ₋₁`) is
`∑'_{k} ∑'_{I₀ ⊔ ... ⊔ Iₖ₋₁ = {0, ..., n-1}} qₖ (p_{i₀} (...), ..., p_{iₖ₋₁} (...))`, where
`iₘ` is the size of `Iₘ` and one puts all variables of `Iₘ` as arguments to `p_{iₘ}`, in
increasing order. The sets `I₀, ..., Iₖ₋₁` are ordered so that `max I₀ < max I₁ < ... < max Iₖ₋₁`.

This definition is chosen so that the `n`-th derivative of `g ∘ f` is the Taylor composition of
the iterated derivatives of `g` and of `f`.

Not to be confused with another notion of composition for formal multilinear series, called just
`FormalMultilinearSeries.comp`, appearing in the composition of analytic functions.
 -/
FormalMultilinearSeries.taylorComp : {𝕜 : 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] →
                      FormalMultilinearSeries 𝕜 F G → FormalMultilinearSeries 𝕜 E F → FormalMultilinearSeries 𝕜 E G
-- Mathlib.Algebra.GCDMonoid.Basic
lcm_assoc : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] (m n k : α),
  lcm (lcm m n) k = lcm m (lcm n k)
-- Mathlib.Order.Hom.Bounded
BotHom.instSemilatticeInf.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : Bot α] [inst_1 : SemilatticeInf β] [inst_2 : OrderBot β],
  BotHom.instSemilatticeInf = Function.Injective.semilatticeInf DFunLike.coe ⋯ ⋯ ⋯ ⋯
-- Lean.Util.Trace
Lean.«doElemTrace[_]__» : Lean.ParserDescr
-- Mathlib.Topology.Separation.Basic
Topology.IsEmbedding.t0Space : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [T0Space Y] {f : X → Y},
  Topology.IsEmbedding f → T0Space X
-- Mathlib.Topology.ContinuousMap.StoneWeierstrass
ContinuousMap.nonUnitalStarAlgebraAdjoin_id_subset_ker_evalStarAlgHom : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {s : Set 𝕜} (h0 : 0 ∈ s),
  ↑(NonUnitalStarAlgebra.adjoin 𝕜 {ContinuousMap.restrict s (ContinuousMap.id 𝕜)}) ⊆
    ↑(RingHom.ker (ContinuousMap.evalStarAlgHom 𝕜 𝕜 ⟨0, h0⟩))
-- Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
/-- A side of a right-angled triangle divided by the sine of the opposite angle equals the
hypotenuse.  -/
EuclideanGeometry.dist_div_sin_oangle_right_of_oangle_eq_pi_div_two : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p₁ p₂ p₃ : P},
  EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(Real.pi / 2) → dist p₁ p₂ / (EuclideanGeometry.oangle p₂ p₃ p₁).sin = dist p₁ p₃
-- Mathlib.Data.Stream.Init
Stream'.get_odd : ∀ {α : Type u} (n : ℕ) (s : Stream' α), s.odd.get n = s.get (2 * n + 1)
-- Mathlib.Algebra.Polynomial.Splits
Polynomial.Splits.aeval_eq_prod_aroots : ∀ {R : Type u_1} {S : Type u_2} [inst : Field R] [inst_1 : CommRing S] [inst_2 : IsDomain S] [inst_3 : Algebra R S]
  {f : Polynomial R},
  (Polynomial.map (algebraMap R S) f).Splits →
    ∀ (x : S),
      (Polynomial.aeval x) f = (algebraMap R S) f.leadingCoeff * (Multiset.map (fun x_1 => x - x_1) (f.aroots S)).prod
-- Mathlib.Lean.Meta.RefinedDiscrTree.Initialize
Lean.Meta.RefinedDiscrTree.instInhabitedPreDiscrTree : {a : Type} → Inhabited (Lean.Meta.RefinedDiscrTree.PreDiscrTree a)
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.Formatter.recover.formatter : Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter
-- Mathlib.CategoryTheory.Types.Basic
/-- The functor which sends a functor to types to its sections.  -/
CategoryTheory.Functor.sectionsFunctor : (J : Type u) →
  [inst : CategoryTheory.Category.{v, u} J] →
    CategoryTheory.Functor (CategoryTheory.Functor J (Type w)) (Type (max u w))
-- Mathlib.CategoryTheory.FiberedCategory.Cartesian
CategoryTheory.Functor.IsCartesian.domainUniqueUpToIso_inv_isHomLift : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  (p : CategoryTheory.Functor 𝒳 𝒮) {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [inst_2 : p.IsCartesian f φ] {a' : 𝒳}
  (φ' : a' ⟶ b) [inst_3 : p.IsCartesian f φ'],
  p.IsHomLift (CategoryTheory.CategoryStruct.id R) (CategoryTheory.Functor.IsCartesian.domainUniqueUpToIso p f φ φ').hom
-- Mathlib.CategoryTheory.Sites.InducedTopology
/-- [SGA4, III, Proposition 3.2][sga-4-tome-1]  -/
CategoryTheory.Functor.mem_inducedTopology_iff : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {K : CategoryTheory.GrothendieckTopology D}
  [inst_2 : CategoryTheory.LocallySmall.{max u₁ v₁ u₂ v₂, v₁, u₁} C] (X : C) (S : CategoryTheory.Sieve X)
  (G :
    CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ (Type (max u₁ v₁ u₂ v₂)))
      (CategoryTheory.Functor Dᵒᵖ (Type (max u₁ v₁ u₂ v₂))))
  (adj : G ⊣ (CategoryTheory.Functor.whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max u₁ v₁ u₂ v₂))).obj F.op),
  S ∈ (F.inducedTopology K) X ↔
    ∀ ⦃Y : C⦄ (f : Y ⟶ X),
      K.W (G.map (CategoryTheory.Sieve.shrinkFunctor.{max u₁ v₁ u₂ v₂, v₁, u₁} (CategoryTheory.Sieve.pullback f S)).ι)
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.CompactOpens.toCompacts_map : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β)
  (hf : Continuous f) (hf' : IsOpenMap f) (s : TopologicalSpace.CompactOpens α),
  (TopologicalSpace.CompactOpens.map f hf hf' s).toCompacts = TopologicalSpace.Compacts.map f hf s.toCompacts
-- Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
MvPolynomial.IsSymmetric.antitone_supDegree : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommSemiring R] [inst_1 : LinearOrder σ] {p : MvPolynomial σ R},
  p.IsSymmetric → Antitone ⇑(ofLex (AddMonoidAlgebra.supDegree (⇑toLex) p))
-- Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
HomotopicalAlgebra.CofibrantObject.instIsLocalizedEquivalenceHoCatWeakEquivalencesToHoCatLocalizerMorphism : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C],
  (HomotopicalAlgebra.CofibrantObject.toHoCatLocalizerMorphism C).IsLocalizedEquivalence
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get?_union : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α fun x => β}
  [EquivBEq α] [LawfulHashable α],
  (↑m₁).WF →
    (↑m₂).WF →
      ∀ {k : α},
        Std.DHashMap.Internal.Raw₀.Const.get? (m₁.union m₂) k =
          (Std.DHashMap.Internal.Raw₀.Const.get? m₂ k).or (Std.DHashMap.Internal.Raw₀.Const.get? m₁ k)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Real.arctan_inv_of_neg : ∀ {x : ℝ}, x < 0 → Real.arctan x⁻¹ = -(Real.pi / 2) - Real.arctan x
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.IsBasis.insert_isBasis_insert : ∀ {α : Type u_1} {M : Matroid α} {I X : Set α} {e : α},
  M.IsBasis I X → M.Indep (insert e I) → M.IsBasis (insert e I) (insert e X)
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.monoidalOpOp_η : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C],
  CategoryTheory.Functor.OplaxMonoidal.η (CategoryTheory.opOp C) =
    CategoryTheory.CategoryStruct.id ((CategoryTheory.opOp C).obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
-- Mathlib.Algebra.Category.ModuleCat.EpiMono
/-- If the zero morphism is an epi then the codomain is trivial.  -/
ModuleCat.uniqueOfEpiZero : {R : Type u} →
  [inst : Ring R] →
    {M : Type v} →
      [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → (X : ModuleCat R) → [h : CategoryTheory.Epi 0] → Unique M
-- Mathlib.Order.Hom.Set
OrderIso.compl_symm_apply : ∀ (α : Type u_1) [inst : BooleanAlgebra α] (a : αᵒᵈ), (RelIso.symm (OrderIso.compl α)) a = (OrderDual.ofDual a)ᶜ
-- Mathlib.MeasureTheory.Function.Jacobian
MeasureTheory.integral_target_eq_integral_abs_det_fderiv_smul : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E]
  [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] {f' : E → E →L[ℝ] E} [inst_5 : MeasurableSpace E]
  [BorelSpace E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] {f : OpenPartialHomeomorph E E},
  (∀ x ∈ f.source, HasFDerivAt (↑f) (f' x) x) →
    ∀ (g : E → F), ∫ (x : E) in f.target, g x ∂μ = ∫ (x : E) in f.source, |(f' x).det| • g (↑f x) ∂μ
-- Mathlib.MeasureTheory.SpecificCodomains.Pi
/-- **Alias** of the forward direction of `MeasureTheory.memLp_pi_iff`. -/
MeasureTheory.MemLp.eval : ∀ {X : Type u_1} {mX : MeasurableSpace X} {μ : MeasureTheory.Measure X} {p : ENNReal} {ι : Type u_2} [inst : Fintype ι]
  {E : ι → Type u_3} [inst_1 : (i : ι) → NormedAddCommGroup (E i)] {f : X → (i : ι) → E i},
  MeasureTheory.MemLp f p μ → ∀ (i : ι), MeasureTheory.MemLp (fun x => f x i) p μ
-- Mathlib.Algebra.Category.GrpWithZero
GrpWithZero.str : (self : GrpWithZero) → GroupWithZero self.carrier
-- Mathlib.Logic.Basic
forall_prop_congr : ∀ {p p' : Prop} {q q' : p → Prop}, (∀ (h : p), q h ↔ q' h) → ∀ (hp : p ↔ p'), (∀ (h : p), q h) ↔ ∀ (h : p'), q' ⋯
-- Mathlib.Topology.Algebra.Module.Equiv
/-- The natural equivalence `M × N ≃L[R] M` for any `Unique` type `N`.
This is `Equiv.prodUnique` as a continuous linear equivalence.  -/
ContinuousLinearEquiv.prodUnique : (R : Type u_8) →
  (M : Type u_9) →
    (N : Type u_10) →
      [inst : Semiring R] →
        [inst_1 : TopologicalSpace M] →
          [inst_2 : AddCommMonoid M] →
            [inst_3 : TopologicalSpace N] →
              [inst_4 : AddCommMonoid N] → [Unique N] → [inst_6 : Module R M] → [inst_7 : Module R N] → (M × N) ≃L[R] M
-- Std.Http.Internal.IndexMultiMap
Std.Internal.IndexMultiMap.instForInProdOfMonad : {α : Type u} →
  {β : Type v} →
    [inst : BEq α] →
      [inst_1 : Hashable α] → {m : Type u_1 → Type u_2} → [Monad m] → ForIn m (Std.Internal.IndexMultiMap α β) (α × β)
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.mk.congr_simp : ∀ {α : Type u_5} {β : Type u_6} [inst : TopologicalSpace α] [inst_1 : Zero β] [inst_2 : TopologicalSpace β]
  (toContinuousMap toContinuousMap_1 : C(α, β)) (e_toContinuousMap : toContinuousMap = toContinuousMap_1)
  (hasCompactSupport' : HasCompactSupport toContinuousMap.toFun),
  { toContinuousMap := toContinuousMap, hasCompactSupport' := hasCompactSupport' } =
    { toContinuousMap := toContinuousMap_1, hasCompactSupport' := ⋯ }
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.dist_lt_of_nonempty_compact : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β]
  {f g : BoundedContinuousFunction α β} {C : ℝ} [Nonempty α] [CompactSpace α],
  (∀ (x : α), dist (f x) (g x) < C) → dist f g < C
-- Init.Data.Array.Attach
Array.pmap_push : ∀ {α : Type u_1} {β : Type u_2} {P : α → Prop} (f : (a : α) → P a → β) (a : α) (xs : Array α)
  (h : ∀ b ∈ xs.push a, P b), Array.pmap f (xs.push a) h = (Array.pmap f xs ⋯).push (f a ⋯)
-- Mathlib.Algebra.Ring.WithZero
WithZero.instLeftDistribClass : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Add α] [LeftDistribClass α], LeftDistribClass (WithZero α)
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
Finsupp.sum_apply' : ∀ {ι : Type u_2} {γ : Type u_3} {A : Type u_4} {B : Type u_5} [inst : AddCommMonoid A] [inst_1 : AddCommMonoid B]
  (g : ι →₀ A) (k : ι → A → γ → B) (x : γ), g.sum k x = g.sum fun i b => k i b x
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd
SSet.prodStdSimplex.pairingCore.IsType₂.φ_succ_fst : ∀ {m : ℕ} {k : Fin (m + 1)} {n : ℕ} (x : ((SSet.horn (m + 1) k.castSucc).unionProd (SSet.boundary n)).N) {d : ℕ}
  (hd : x.dim = d),
  (SSet.prodStdSimplex.pairingCore.IsType₂.φ x hd (SSet.prodStdSimplex.pairingCore.min x hd).succ).1 = k.succ
-- Mathlib.Algebra.AffineMonoid.Basic
IsAffineAddMonoid.toIsAddTorsionFree : ∀ {M : Type u_1} {inst : AddCommMonoid M} [self : IsAffineAddMonoid M], IsAddTorsionFree M
-- Mathlib.LinearAlgebra.Complex.Module
selfAdjoint.submodule.eq_1 : ∀ (R : Type u_1) (A : Type u_2) [inst : Semiring R] [inst_1 : StarMul R] [inst_2 : TrivialStar R]
  [inst_3 : AddCommGroup A] [inst_4 : Module R A] [inst_5 : StarAddMonoid A] [inst_6 : StarModule R A],
  selfAdjoint.submodule R A = { toAddSubmonoid := (selfAdjoint A).toAddSubmonoid, smul_mem' := ⋯ }
-- Mathlib.GroupTheory.NoncommPiCoprod
MonoidHom.noncommPiCoprod_range : ∀ {G : Type u_1} [inst : Group G] {ι : Type u_2} {H : ι → Type u_3} [inst_1 : (i : ι) → Group (H i)]
  (ϕ : (i : ι) → H i →* G) [inst_2 : Fintype ι]
  {hcomm : Pairwise fun i j => ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y)},
  (MonoidHom.noncommPiCoprod ϕ hcomm).range = ⨆ i, (ϕ i).range
-- Mathlib.Algebra.Group.Units.Defs
divp_self : ∀ {α : Type u} [inst : Monoid α] (u : αˣ), ↑u /ₚ u = 1
-- Mathlib.Order.Heyting.Basic
CoheytingAlgebra.toBoundedOrder : {α : Type u_2} → [inst : CoheytingAlgebra α] → BoundedOrder α
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.mul.go.eq_def : ∀ (fuel : ℕ) (m₁ m₂ : Lean.Grind.CommRing.Mon),
  Lean.Grind.CommRing.Mon.mul.go fuel m₁ m₂ =
    match fuel with
    | 0 => m₁.concat m₂
    | fuel.succ =>
      match m₁, m₂ with
      | m₁, Lean.Grind.CommRing.Mon.unit => m₁
      | Lean.Grind.CommRing.Mon.unit, m₂ => m₂
      | Lean.Grind.CommRing.Mon.mult pw₁ m₁, Lean.Grind.CommRing.Mon.mult pw₂ m₂ =>
        bif pw₁.varLt pw₂ then
          Lean.Grind.CommRing.Mon.mult pw₁
            (Lean.Grind.CommRing.Mon.mul.go fuel m₁ (Lean.Grind.CommRing.Mon.mult pw₂ m₂))
        else
          bif pw₂.varLt pw₁ then
            Lean.Grind.CommRing.Mon.mult pw₂
              (Lean.Grind.CommRing.Mon.mul.go fuel (Lean.Grind.CommRing.Mon.mult pw₁ m₁) m₂)
          else
            Lean.Grind.CommRing.Mon.mult { x := pw₁.x, k := pw₁.k + pw₂.k } (Lean.Grind.CommRing.Mon.mul.go fuel m₁ m₂)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.size_le_size_insertMany_list : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  {l : List ((a : α) × β a)}, m.size ≤ (m.insertMany l).size
-- ProofWidgets.Component.PenroseDiagram
ProofWidgets.Penrose.instInhabitedDiagramProps : Inhabited ProofWidgets.Penrose.DiagramProps
-- ProofWidgets.Component.Panel.Basic
ProofWidgets.withPanelWidgets : Lean.Elab.Tactic.Tactic
-- Mathlib.GroupTheory.OrderOfElement
IsOfFinAddOrder.addOrderOf_pos : ∀ {G : Type u_1} [inst : AddMonoid G] {x : G}, IsOfFinAddOrder x → 0 < addOrderOf x
-- Mathlib.CategoryTheory.Limits.Types.Products
CategoryTheory.Limits.Types.Small.productIso_hom_comp_eval : ∀ {J : Type v} (F : J → Type u) [inst : Small.{u, v} J] (j : J),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Types.Small.productIso F).hom
      (TypeCat.ofHom fun f => (equivShrink ((j : J) → F j)).symm f j) =
    CategoryTheory.Limits.Pi.π F j
-- Init.Data.String.Basic
ByteArray.IsValidUTF8.isUTF8FirstByte_getElem_zero : ∀ {b : ByteArray}, b.IsValidUTF8 → ∀ (h₀ : 0 < b.size), b[0].IsUTF8FirstByte
-- Mathlib.Analysis.Convex.Body
ConvexBody.mk : {V : Type u_2} →
  [inst : TopologicalSpace V] →
    [inst_1 : AddCommMonoid V] →
      [inst_2 : SMul ℝ V] → (carrier : Set V) → Convex ℝ carrier → IsCompact carrier → carrier.Nonempty → ConvexBody V
-- Init.Data.SInt.Lemmas
ISize.ofInt_eq_ofIntLE_div : ∀ {a b : ℤ} (ha₁ : ISize.minValue.toInt ≤ a) (ha₂ : a ≤ ISize.maxValue.toInt) (hb₁ : ISize.minValue.toInt ≤ b)
  (hb₂ : b ≤ ISize.maxValue.toInt), ISize.ofInt (a.tdiv b) = ISize.ofIntLE a ha₁ ha₂ / ISize.ofIntLE b hb₁ hb₂
-- Mathlib.Analysis.Normed.Ring.WithAbs
WithAbs.equiv_symm_apply : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring S] [inst_1 : PartialOrder S] [inst_2 : Semiring R]
  (v : AbsoluteValue R S) (ofAbs : R), (WithAbs.equiv v).symm ofAbs = WithAbs.toAbs v ofAbs
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
CategoryTheory.Limits.WalkingReflexivePair.instDecidableEqHom : {a a_1 : CategoryTheory.Limits.WalkingReflexivePair} → DecidableEq (a.Hom a_1)
-- Lean.Meta.Tactic.Grind.Internalize
/-- Returns `true` if `e` is of the form `@Eq Prop a b`  -/
Lean.Meta.Grind.isMorallyIff : Lean.Expr → Bool
-- Mathlib.RingTheory.PolynomialAlgebra
PolyEquivTensor.toFunBilinear_apply_eq_smul : ∀ (R : Type u_1) (A : Type u_3) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (a : A)
  (p : Polynomial R), ((PolyEquivTensor.toFunBilinear R A) a) p = a • Polynomial.map (algebraMap R A) p
-- Mathlib.Topology.NhdsSet
lift'_nhdsSet_interior : ∀ {X : Type u_2} [inst : TopologicalSpace X] (s : Set X), (nhdsSet s).lift' interior = nhdsSet s
-- Lean.Server.InfoUtils
Lean.Elab.Info.occursInOrOnBoundary : Lean.Elab.Info → String.Pos.Raw → Bool
-- Mathlib.Order.Interval.Set.Image
Antitone.image_Icc_subset : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : Preorder α] [inst_1 : Preorder β] {a b : α},
  Antitone f → f '' Set.Icc a b ⊆ Set.Icc (f b) (f a)
-- Mathlib.RingTheory.Spectrum.Prime.RingHom
PrimeSpectrum.sigmaToPi_bijective : ∀ {ι : Type u_3} (R : ι → Type u_4) [inst : (i : ι) → CommRing (R i)] [Finite ι],
  Function.Bijective (PrimeSpectrum.sigmaToPi R)
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
dist_triangle : ∀ {α : Type u} [inst : PseudoMetricSpace α] (x y z : α), dist x z ≤ dist x y + dist y z
-- Mathlib.Algebra.Group.Center
Set.addCenter_prod : ∀ {M : Type u_1} [inst : Add M] {N : Type u_2} [inst_1 : Add N],
  Set.addCenter (M × N) = Set.addCenter M ×ˢ Set.addCenter N
-- Init.Control.Lawful.Instances
instLawfulApplicativeOption : LawfulApplicative Option
-- Mathlib.Analysis.Calculus.FDeriv.Defs
/-- A function `f` is differentiable at a point `x` if it admits a derivative there (possibly
non-unique).  -/
DifferentiableAt : (𝕜 : Type u_1) →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : AddCommGroup E] →
        [Module 𝕜 E] →
          [TopologicalSpace E] →
            {F : Type u_3} → [inst_4 : AddCommGroup F] → [Module 𝕜 F] → [TopologicalSpace F] → (E → F) → E → Prop
-- Mathlib.RingTheory.Polynomial.SmallDegreeVieta
/-- **Vieta's formula** for quadratics as an iff.  -/
Polynomial.roots_quadratic_eq_pair_iff_of_ne_zero : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] {a b c x1 x2 : R},
  a ≠ 0 →
    ((Polynomial.C a * Polynomial.X ^ 2 + Polynomial.C b * Polynomial.X + Polynomial.C c).roots = {x1, x2} ↔
      b = -a * (x1 + x2) ∧ c = a * x1 * x2)
-- Mathlib.Algebra.Polynomial.BigOperators
Polynomial.natDegree_multiset_prod_le : ∀ {R : Type u} [inst : CommSemiring R] (t : Multiset (Polynomial R)),
  t.prod.natDegree ≤ (Multiset.map Polynomial.natDegree t).sum
-- Mathlib.Topology.Neighborhoods
/-- **Alias** of `closure_sdiff`. -/
closure_diff : ∀ {X : Type u} [inst : TopologicalSpace X] {s t : Set X}, closure s \ closure t ⊆ closure (s \ t)
-- Mathlib.SetTheory.Ordinal.Arithmetic
/-- **Alias** of `Ordinal.eq_natCast_or_omega0_le`. -/
Ordinal.eq_nat_or_omega0_le : ∀ (o : Ordinal.{u_4}), (∃ n, o = ↑n) ∨ Ordinal.omega0 ≤ o
-- Mathlib.Algebra.Group.Pi.Basic
Pi.addCommSemigroup.eq_1 : ∀ {I : Type u} {f : I → Type v₁} [inst : (i : I) → AddCommSemigroup (f i)],
  Pi.addCommSemigroup = { toAddSemigroup := Pi.addSemigroup, add_comm := ⋯ }
-- Lean.Elab.Syntax
Lean.Elab.Term.ToParserDescrContext.first : Lean.Elab.Term.ToParserDescrContext → Bool
-- Lean.Expr
/-- Auxiliary annotation used to mark terms marked with the "inaccessible" annotation `.(t)` and
`_` in patterns.
 -/
Lean.mkInaccessible : Lean.Expr → Lean.Expr
-- Mathlib.Topology.Order.Hom.Esakia
PseudoEpimorphism.exists_map_eq_of_map_le' : ∀ {α : Type u_6} {β : Type u_7} [inst : Preorder α] [inst_1 : Preorder β] (self : PseudoEpimorphism α β) ⦃a : α⦄
  ⦃b : β⦄, self.toFun a ≤ b → ∃ c, a ≤ c ∧ self.toFun c = b
-- Mathlib.Algebra.Group.Hom.Instances
ZeroHom.instZSMul.eq_1 : ∀ {M : Type uM} {N : Type uN} [inst : Zero M] [inst_1 : AddGroup N],
  ZeroHom.instZSMul = { smul := fun n f => { toFun := n • ⇑f, map_zero' := ⋯ } }
-- Init.Data.SInt.Bitwise
Int16.not_and_self : ∀ {a : Int16}, ~~~a &&& a = 0
-- Mathlib.Combinatorics.Additive.FreimanHom
/-- An additive `n`-Freiman homomorphism from a set `A` to a set `B` is a map which preserves sums
of `n` elements.  -/
IsAddFreimanHom : {α : Type u_2} → {β : Type u_3} → [AddCommMonoid α] → [AddCommMonoid β] → ℕ → Set α → Set β → (α → β) → Prop
-- Mathlib.Data.Complex.Basic
Complex.re_mul_ofReal : ∀ (z : ℂ) (r : ℝ), (z * ↑r).re = z.re * r
-- Mathlib.Topology.Constructions
continuous_ofAdd : ∀ {X : Type u} [inst : TopologicalSpace X], Continuous ⇑Multiplicative.ofAdd
-- Lean.DocString.Links
/-- Returns `true` if the character is one of those allowed in RFC 3986 sections 2.2 and 2.3. other
than '(' or')'.
 -/
_private.Lean.DocString.Links.0.Lean.rewriteManualLinksCore.urlChar : Char → Bool
-- Mathlib.Tactic.NormNum.Irrational
/-- Proof of `m < (k + 1) ^ n`.  -/
Mathlib.Meta.NormNum.NotPowerCertificate.pf_right : {m n : Q(ℕ)} → (self : Mathlib.Meta.NormNum.NotPowerCertificate m n) → Q(«$m» < (unknown_1 + 1) ^ «$n»)
-- Mathlib.Analysis.RCLike.Basic
RCLike.im_eq_conj_sub : ∀ {K : Type u_1} [inst : RCLike K] (z : K), ↑(RCLike.im z) = RCLike.I * ((starRingEnd K) z - z) / 2
-- Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology
WithIdeal.instNonarchimedeanRing : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : WithIdeal R], NonarchimedeanRing R
-- Mathlib.Order.Heyting.Regular
/-- A Heyting algebra with regular excluded middle is a Boolean algebra.  -/
BooleanAlgebra.ofRegular : {α : Type u_1} → [inst : HeytingAlgebra α] → (∀ (a : α), Heyting.IsRegular (a ⊔ aᶜ)) → BooleanAlgebra α
-- Init.Data.Nat.Lemmas
Nat.div_lt_div_right : ∀ {a b c : ℕ}, a ≠ 0 → a ∣ b → a ∣ c → (b / a < c / a ↔ b < c)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getD_insertIfNew : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k a : α} {fallback v : β},
      (t.insertIfNew k v).getD a fallback = if cmp k a = Ordering.eq ∧ k ∉ t then v else t.getD a fallback
-- Lean.Meta.Basic
/-- Given `e` of the form `forall (a_1 : A_1) ... (a_n : A_n), B[a_1, ..., a_n]` and `p_1 : A_1, ... p_n : A_n`, return `B[p_1, ..., p_n]`.  -/
Lean.Meta.instantiateForall : Lean.Expr → Array Lean.Expr → Lean.MetaM Lean.Expr
-- Lean.Elab.PreDefinition.TerminationHint
Lean.Elab.TerminationBy.ref : Lean.Elab.TerminationBy → Lean.Syntax
-- Mathlib.Order.Category.Preord
Preord.of.sizeOf_spec : ∀ (carrier : Type u_1) [str : Preorder carrier],
  sizeOf { carrier := carrier, str := str } = 1 + sizeOf carrier + sizeOf str
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalAlgebra.mem_iInf : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] [inst_4 : SMulCommClass R A A] {ι : Sort u_2} {S : ι → NonUnitalSubalgebra R A}
  {x : A}, x ∈ ⨅ i, S i ↔ ∀ (i : ι), x ∈ S i
-- Mathlib.Data.Set.Semiring
SetSemiring.instSemigroup : {α : Type u_1} → [Semigroup α] → Semigroup (SetSemiring α)
-- Mathlib.Algebra.Order.Group.Synonym
toColex_vadd : ∀ {β : Type u_2} {α : Type u_1} [inst : VAdd β α] (b : β) (a : α), toColex (b +ᵥ a) = b +ᵥ toColex a
-- Mathlib.Combinatorics.SetFamily.FourFunctions
_private.Mathlib.Combinatorics.SetFamily.FourFunctions.0.erase_eq_iff : ∀ {α : Type u_1} [inst : DecidableEq α] {a : α} {s t : Finset α}, a ∉ s → (t.erase a = s ↔ t = s ∨ t = insert a s)
-- Mathlib.Analysis.BoxIntegral.UnitPartition
BoxIntegral.unitPartition.mem_box_iff' : ∀ {ι : Type u_1} {n : ℕ} [inst : NeZero n] {ν : ι → ℤ} {x : ι → ℝ},
  x ∈ BoxIntegral.unitPartition.box n ν ↔ ∀ (i : ι), ↑(ν i) < ↑n * x i ∧ ↑n * x i ≤ ↑(ν i) + 1
-- Mathlib.Order.Filter.Prod
Filter.map_prodMap_coprod_le : ∀ {α₁ : Type u} {α₂ : Type v} {β₁ : Type w} {β₂ : Type x} {f₁ : Filter α₁} {f₂ : Filter α₂} {m₁ : α₁ → β₁}
  {m₂ : α₂ → β₂}, Filter.map (Prod.map m₁ m₂) (f₁.coprod f₂) ≤ (Filter.map m₁ f₁).coprod (Filter.map m₂ f₂)