mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
_private.Lean.PrettyPrinter.Delaborator.TopDownAnalyze.0.Lean.PrettyPrinter.Delaborator.TopDownAnalyze.analyzeAppStagedCore.collectHigherOrders : Lean.PrettyPrinter.Delaborator.TopDownAnalyze.AnalyzeAppM Unit
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.map_ofNat : ∀ {R : Type u} {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁] (f : R →+* S₁) (n : ℕ)
  [inst_2 : n.AtLeastTwo], (MvPolynomial.map f) (OfNat.ofNat n) = OfNat.ofNat n
-- Init.Data.Fin.Bitwise
Fin.and_val : ∀ {n : ℕ} (a b : Fin n), ↑(a &&& b) = ↑a &&& ↑b
-- Mathlib.CategoryTheory.Comma.Arrow
/-- The left object of an arrow.  -/
CategoryTheory.Arrow.left : {T : Type u} → [inst : CategoryTheory.Category.{v, u} T] → CategoryTheory.Arrow T → T
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get!_map_of_getKey?_eq_some : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {γ : Type w}
  (m : Std.DHashMap.Internal.Raw₀ α fun x => β) [EquivBEq α] [LawfulHashable α] [inst_4 : Inhabited γ] {f : α → β → γ}
  {k k' : α},
  (↑m).WF →
    m.getKey? k = some k' →
      Std.DHashMap.Internal.Raw₀.Const.get! (Std.DHashMap.Internal.Raw₀.map f m) k =
        (Option.map (f k') (Std.DHashMap.Internal.Raw₀.Const.get? m k)).get!
-- Mathlib.AlgebraicGeometry.Morphisms.LocalIso
/-- A local isomorphism of schemes is a morphism that is (Zariski-)source-locally an
open immersion.  -/
AlgebraicGeometry.IsLocalIso : {X Y : AlgebraicGeometry.Scheme} → (X ⟶ Y) → Prop
-- Mathlib.GroupTheory.QuotientGroup.Finite
Finite.of_subgroup_quotient : ∀ {G : Type u_2} [inst : Group G] (H : Subgroup G) [Finite ↥H] [Finite (G ⧸ H)], Finite G
-- Mathlib.Topology.ContinuousMap.CocompactMap
/-- The cocompact filter on `α` tends to the cocompact filter on `β` under the function  -/
CocompactMap.cocompact_tendsto' : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (self : CocompactMap α β),
  Filter.Tendsto self.toFun (Filter.cocompact α) (Filter.cocompact β)
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
WeierstrassCurve.φ_one : ∀ {R : Type r} [inst : CommRing R] (W : WeierstrassCurve R), W.φ 1 = Polynomial.C Polynomial.X
-- Mathlib.Data.List.AList
AList.lookup_union_left : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {a : α} {s₁ s₂ : AList β},
  a ∈ s₁ → AList.lookup a (s₁ ∪ s₂) = AList.lookup a s₁
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
AlgebraicGeometry.Scheme.IdealSheafData.instIsEmptyCarrierCarrierCommRingCatSubschemeTop : ∀ {X : AlgebraicGeometry.Scheme}, IsEmpty ↥⊤.subscheme
-- Lean.ReducibilityAttrs
Lean.ReducibilityStatus.irreducible : Lean.ReducibilityStatus
-- Mathlib.Data.ZMod.ValMinAbs
ZMod.valMinAbs_spec : ∀ {n : ℕ} [NeZero n] (x : ZMod n) (y : ℤ), x.valMinAbs = y ↔ x = ↑y ∧ y * 2 ∈ Set.Ioc (-↑n) ↑n
-- Mathlib.Analysis.Convex.Star
starConvex_iUnion : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : SMul 𝕜 E] {x : E} {ι : Sort u_4} {s : ι → Set E},
  (∀ (i : ι), StarConvex 𝕜 x (s i)) → StarConvex 𝕜 x (⋃ i, s i)
-- Mathlib.Analysis.Polynomial.Basic
Polynomial.eventually_atTop_not_isRoot : ∀ {𝕜 : Type u_1} [inst : NormedField 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (P : Polynomial 𝕜),
  P ≠ 0 → ∀ᶠ (x : 𝕜) in Filter.atTop, ¬P.IsRoot x
-- Std.Internal.Parsec.String
/-- Parses the given char.
 -/
Std.Internal.Parsec.String.pchar : Char → Std.Internal.Parsec.String.Parser Char
-- Init.Data.List.Lemmas
List.foldl_flip_append_eq_append : ∀ {α : Type u_1} {β : Type u_2} {l : List α} {f : α → List β} {l' : List β},
  List.foldl (fun xs y => f y ++ xs) l' l = (List.map f l).reverse.flatten ++ l'
-- Mathlib.NumberTheory.ModularForms.SlashActions
SlashAction.neg_slash : ∀ {β : Type u_1} {G : Type u_2} {α : Type u_3} [inst : Monoid G] [inst_1 : AddGroup α] [inst_2 : SlashAction β G α]
  (k : β) (g : G) (a : α), SlashAction.map k g (-a) = -SlashAction.map k g a
-- Mathlib.Order.Hom.Lattice
SupHom.mk.injEq : ∀ {α : Type u_6} {β : Type u_7} [inst : Max α] [inst_1 : Max β] (toFun : α → β)
  (map_sup' : ∀ (a b : α), toFun (a ⊔ b) = toFun a ⊔ toFun b) (toFun_1 : α → β)
  (map_sup'_1 : ∀ (a b : α), toFun_1 (a ⊔ b) = toFun_1 a ⊔ toFun_1 b),
  ({ toFun := toFun, map_sup' := map_sup' } = { toFun := toFun_1, map_sup' := map_sup'_1 }) = (toFun = toFun_1)
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
/-- If the pullback map is obtained via whiskering,
then the result `sheaf_hom (whisker_left G.op α)` is equal to `α`.
 -/
CategoryTheory.Functor.IsCoverDense.sheafHom_eq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {K : CategoryTheory.GrothendieckTopology D} {A : Type u_4}
  [inst_2 : CategoryTheory.Category.{v_4, u_4} A] (G : CategoryTheory.Functor C D) [inst_3 : G.IsCoverDense K]
  [inst_4 : G.IsLocallyFull K] {ℱ : CategoryTheory.Functor Dᵒᵖ A} {ℱ' : CategoryTheory.Sheaf K A} (α : ℱ ⟶ ℱ'.obj),
  CategoryTheory.Functor.IsCoverDense.sheafHom (G.op.whiskerLeft α) = α
-- Mathlib.Data.Real.Basic
Real.mk_le_of_forall_le : ∀ {f : CauSeq ℚ abs} {x : ℝ}, (∃ i, ∀ j ≥ i, ↑(↑f j) ≤ x) → Real.mk f ≤ x
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.MatchClone.pushArgsAux : Array Lean.Meta.ParamInfo → ℕ → Lean.Expr → Array Lean.Expr → Lean.MetaM (Array Lean.Expr)
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
atTop_isMeasurablyGenerated : ∀ {α : Type u_1} [inst : TopologicalSpace α] {mα : MeasurableSpace α} [OpensMeasurableSpace α] [inst_2 : Preorder α]
  [ClosedIciTopology α], Filter.atTop.IsMeasurablyGenerated
-- Batteries.Data.List.Lemmas
List.getElem_zero_idxsOf_eq_idxOf : ∀ {α : Type u_1} {xs : List α} {x : α} [inst : BEq α] (h : 0 < (List.idxsOf x xs).length),
  (List.idxsOf x xs)[0] = List.idxOf x xs
-- Mathlib.Algebra.Field.Subfield.Basic
Subfield.smul_def : ∀ {K : Type u} [inst : DivisionRing K] {X : Type u_1} [inst_1 : SMul K X] {F : Subfield K} (g : ↥F) (m : X),
  g • m = ↑g • m
-- Mathlib.Computability.Primrec.Basic
Primrec.bind_decode_iff : ∀ {α : Type u_1} {β : Type u_2} {σ : Type u_3} [inst : Primcodable α] [inst_1 : Primcodable β] [inst_2 : Primcodable σ]
  {f : α → β → Option σ}, (Primrec₂ fun a n => (Encodable.decode n).bind (f a)) ↔ Primrec₂ f
-- Mathlib.Analysis.BoxIntegral.Box.Basic
BoxIntegral.Box.lower_ne_upper : ∀ {ι : Type u_1} (I : BoxIntegral.Box ι) (i : ι), I.lower i ≠ I.upper i
-- Mathlib.Algebra.Homology.Additive
/-- An equivalence of categories induces an equivalences between the respective categories
of homological complex.
 -/
CategoryTheory.Equivalence.mapHomologicalComplex : {ι : Type u_1} →
  {W₁ : Type u_3} →
    {W₂ : Type u_4} →
      [inst : CategoryTheory.Category.{v_2, u_3} W₁] →
        [inst_1 : CategoryTheory.Category.{v_3, u_4} W₂] →
          [inst_2 : CategoryTheory.Limits.HasZeroMorphisms W₁] →
            [inst_3 : CategoryTheory.Limits.HasZeroMorphisms W₂] →
              (e : W₁ ≌ W₂) →
                [e.functor.PreservesZeroMorphisms] →
                  (c : ComplexShape ι) → HomologicalComplex W₁ c ≌ HomologicalComplex W₂ c
-- Lean.Meta.Tactic.Grind.Core
/-- Tries to apply beta-reduction using the parent applications of the functions in `fns` with
the lambda expressions in `lams`.
 -/
Lean.Meta.Grind.propagateBeta : Array Lean.Expr → Array Lean.Expr → Lean.Meta.Grind.GoalM Unit
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.isIso_op_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y),
  CategoryTheory.IsIso f.op ↔ CategoryTheory.IsIso f
-- Mathlib.Data.FunLike.Group
/-- A `FunLike` type that satisfies `(f + g) x = f x + g x` is a left cancel additive
semigroup if `β` is a left cancel additive semigroup.  -/
FunLike.addLeftCancelSemigroup : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : FunLike F α β] →
        [inst_1 : Add F] → [inst_2 : AddLeftCancelSemigroup β] → [IsAddApply F α β] → AddLeftCancelSemigroup F
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.coeFnMonoidHom_apply : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : MulOneClass Y] (a : LocallyConstant X Y)
  (a_1 : X), LocallyConstant.coeFnMonoidHom a a_1 = a a_1
-- Mathlib.Data.DFinsupp.Defs
/-- `subtypeDomain` but as an `AddMonoidHom`.  -/
DFinsupp.subtypeDomainAddMonoidHom : {ι : Type u} →
  (β : ι → Type v) →
    [inst : (i : ι) → AddZeroClass (β i)] →
      (p : ι → Prop) → [DecidablePred p] → (Π₀ (i : ι), β i) →+ Π₀ (i : Subtype p), β ↑i
-- Init.Data.Nat.Lcm
Nat.lcm_dvd_lcm_of_dvd_left : ∀ {m k : ℕ} (n : ℕ), m ∣ k → m.lcm n ∣ k.lcm n
-- Mathlib.MeasureTheory.Measure.Content
MeasureTheory.Content.innerContent_bot : ∀ {G : Type w} [inst : TopologicalSpace G] (μ : MeasureTheory.Content G), μ.innerContent ⊥ = 0
-- Mathlib.Topology.UniformSpace.UniformEmbedding
totallyBounded_preimage : ∀ {α : Type u} {β : Type v} [inst : UniformSpace α] [inst_1 : UniformSpace β] {f : α → β} {s : Set β},
  IsUniformInducing f → TotallyBounded s → TotallyBounded (f ⁻¹' s)
-- Mathlib.Algebra.Homology.AlternatingConst
ComplexShape.up_nat_odd_add : ∀ {i j : ℕ}, (ComplexShape.up ℕ).Rel i j → Odd (i + j)
-- Mathlib.Data.Stream.Init
Stream'.mem_cons_of_mem : ∀ {α : Type u} {a : α} {s : Stream' α} (b : α), a ∈ s → a ∈ Stream'.cons b s
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
/-- The image of a pre-`0`-hypercover under a functor.  -/
CategoryTheory.PreZeroHypercover.map : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {S : C} →
      {D : Type u_1} →
        [inst_1 : CategoryTheory.Category.{v_1, u_1} D] →
          (F : CategoryTheory.Functor C D) →
            CategoryTheory.PreZeroHypercover S → CategoryTheory.PreZeroHypercover (F.obj S)
-- Mathlib.Topology.Covering.Basic
IsOpen.trivializationDiscrete_source : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X}
  [inst_2 : Nonempty (X → E)] {ι : Type u_3} [inst_3 : Nonempty ι] [inst_4 : TopologicalSpace ι]
  [inst_5 : DiscreteTopology ι] (U : ι → Set E) (V : Set X) (open_V : IsOpen V)
  (open_iff : ∀ (i : ι) {W : Set X}, W ⊆ V → (IsOpen W ↔ IsOpen (f ⁻¹' W ∩ U i))) (inj : ∀ (i : ι), Set.InjOn f (U i))
  (surj : ∀ (i : ι), Set.SurjOn f (U i) V) (disjoint : Pairwise (Function.onFun Disjoint U))
  (exhaustive : f ⁻¹' V ⊆ ⋃ i, U i),
  (IsOpen.trivializationDiscrete U V open_V open_iff inj surj disjoint exhaustive).source = f ⁻¹' V
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.Iter.fold_filterMapM : ∀ {α β γ δ : Type w} {n : Type w → Type w'} {Pred EPred : Type w} [inst : Std.Iterator α Id β]
  [Std.Iterators.Finite α Id] [inst_2 : Monad n] [inst_3 : MonadAttach n] [WeaklyLawfulMonadAttach n]
  [inst_5 : Std.Internal.Do.Assertion Pred] [inst_6 : Std.Internal.Do.Assertion EPred]
  [inst_7 : Std.Internal.Do.WPMonad n Pred EPred] [inst_8 : Std.IteratorLoop α Id n] [Std.LawfulIteratorLoop α Id n]
  {f : β → n (Option γ)} {g : δ → γ → δ} {init : δ} {it : Std.Iter β} {P : Pred} {Q : δ → Pred} {eQ : EPred},
  ⦃ P ⦄
      Std.Iter.foldM
        (fun d b => do
          let __x ← f b
          match __x with
            | some c => pure (g d c)
            | x => pure d)
        init it ⦃
      Q; eQ ⦄ →
    ⦃ P ⦄ Std.IterM.fold g init (Std.Iter.filterMapM f it) ⦃ Q; eQ ⦄
-- Mathlib.Analysis.Distribution.TemperedDistribution
/-- This coercion has to be a `CoeHead`, because `𝓢'(E, F)` can't infer the value of `p` or `μ`.  -/
MeasureTheory.Lp.instCoeToTemperedDistribution : {E : Type u_3} →
  {F : Type u_4} →
    [inst : NormedAddCommGroup E] →
      [inst_1 : NormedSpace ℝ E] →
        [inst_2 : NormedAddCommGroup F] →
          [inst_3 : NormedSpace ℂ F] →
            [CompleteSpace F] →
              [inst_5 : MeasurableSpace E] →
                [BorelSpace E] →
                  {μ : MeasureTheory.Measure E} →
                    [hμ : μ.HasTemperateGrowth] →
                      {p : ENNReal} →
                        [hp : Fact (1 ≤ p)] → CoeHead (↥(MeasureTheory.Lp F p μ)) (TemperedDistribution E F)
-- Mathlib.Topology.MetricSpace.Isometry
IsometryEquiv.symm_apply_eq : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] (h : α ≃ᵢ β) {x : α} {y : β},
  h.symm y = x ↔ y = h x
-- Mathlib.Topology.UnitInterval
/-- Form a convex linear combination of two points in a closed interval.

This should be removed once a general theory of convex spaces is available in Mathlib.
 -/
Set.Icc.convexComb : {a b : ℝ} → ↑(Set.Icc a b) → ↑(Set.Icc a b) → ↑unitInterval → ↑(Set.Icc a b)
-- Mathlib.GroupTheory.OreLocalization.Basic
AddOreLocalization.zero_sub_vadd : ∀ {R : Type u_1} [inst : AddMonoid R] {S : AddSubmonoid R} [inst_1 : AddOreLocalization.AddOreSet S] {X : Type u_2}
  [inst_2 : AddAction R X] {r : X} {s t : ↥S}, (0 -ₒ t) +ᵥ r -ₒ s = r -ₒ (s + t)
-- Mathlib.Algebra.Homology.ExactSequence
/-- A map of short complexes induces a map of composable arrows with the same data.  -/
CategoryTheory.ShortComplex.mapToComposableArrows : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} → (S₁ ⟶ S₂) → (S₁.toComposableArrows ⟶ S₂.toComposableArrows)
-- Mathlib.MeasureTheory.Group.Measure
/-- **Alias** of `MeasureTheory.Measure.IsHaarMeasure.nullSingletonClass`.

---

If the neutral element of a group is not isolated, then a Haar measure on this group has value
zero on singletons.

The additive version of this instance applies in particular to show that an additive Haar
measure on a nontrivial finite-dimensional real vector space has no atom.  -/
MeasureTheory.Measure.IsHaarMeasure.noAtoms : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Group G] [inst_2 : TopologicalSpace G] [IsTopologicalGroup G]
  [BorelSpace G] [T1Space G] [WeaklyLocallyCompactSpace G] [(nhdsWithin 1 {1}ᶜ).NeBot] (μ : MeasureTheory.Measure G)
  [μ.IsHaarMeasure], MeasureTheory.NullSingletonClass μ
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
Finsupp.single_multiset_sum : ∀ {α : Type u_1} {M : Type u_8} [inst : AddCommMonoid M] (s : Multiset M) (a : α),
  (fun₀ | a => s.sum) = (Multiset.map (Finsupp.single a) s).sum
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.NewFact.eq : Lean.Expr → Lean.Expr → Lean.Expr → Bool → Lean.Meta.Grind.NewFact
-- Lean.Parser.Command
Lean.Parser.Command.eraseAttr.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
MDifferentiable.mdifferentiableAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {x : M},
  MDiff f → MDiffAt f x
-- Mathlib.Algebra.Order.Interval.Set.Group
Set.add_mem_Ioo_iff_right : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] {a b c d : α},
  a + b ∈ Set.Ioo c d ↔ b ∈ Set.Ioo (c - a) (d - a)
-- Mathlib.Topology.Perfect
/-- Any uncountable closed set in a second countable space contains a nonempty perfect subset.  -/
exists_perfect_nonempty_of_isClosed_of_not_countable : ∀ {α : Type u_1} [inst : TopologicalSpace α] {C : Set α} [SecondCountableTopology α],
  IsClosed C → ¬C.Countable → ∃ D, Perfect D ∧ D.Nonempty ∧ D ⊆ C
-- Mathlib.CategoryTheory.Sites.Equivalence
CategoryTheory.Equivalence.hasSheafCompose : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] (K : CategoryTheory.GrothendieckTopology D) (e : C ≌ D)
  [CategoryTheory.Functor.IsDenseSubsite K J e.inverse] {A : Type u_1} [inst_3 : CategoryTheory.Category.{v_1, u_1} A]
  {B : Type u_2} [inst_4 : CategoryTheory.Category.{v_2, u_2} B] (F : CategoryTheory.Functor A B) [K.HasSheafCompose F],
  J.HasSheafCompose F
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.getKey?_modify : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} {k k' : α}
  {f : β → β},
  (Std.DTreeMap.Const.modify t k f).getKey? k' =
    if cmp k k' = Ordering.eq then if k ∈ t then some k else none else t.getKey? k'
-- Mathlib.CategoryTheory.Limits.Constructions.Over.Products
/-- The product of `Y` and `Z` in `Over X` is isomorphic to `Y ×ₓ Z`.  -/
CategoryTheory.Over.prodLeftIsoPullback : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X : C} →
      (Y Z : CategoryTheory.Over X) →
        [inst_1 : CategoryTheory.Limits.HasPullback Y.hom Z.hom] →
          [inst_2 : CategoryTheory.Limits.HasBinaryProduct Y Z] →
            (Y ⨯ Z).left ≅ CategoryTheory.Limits.pullback Y.hom Z.hom
-- Mathlib.Lean.CoreM
/-- Run a `CoreM α` in a fresh `Environment` with specified `modules : List Name` imported.
 -/
CoreM.withImportModules : {α : Type} →
  Array Lean.Name →
    Lean.CoreM α →
      optParam (Option Lean.SearchPath) none → optParam Lean.Options ∅ → optParam UInt32 0 → optParam String "" → IO α
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.toProd.eq_1 : ∀ {M : Type u_1} {N : Type u_2} [inst : AddMonoid M] [inst_1 : AddMonoid N],
  AddMonoid.Coprod.toProd = AddMonoid.Coprod.lift (AddMonoidHom.inl M N) (AddMonoidHom.inr M N)
-- Mathlib.Geometry.Euclidean.Inversion.ImageHyperplane
EuclideanGeometry.image_inversion_perpBisector : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {c y : P} {R : ℝ},
  R ≠ 0 →
    y ≠ c →
      EuclideanGeometry.inversion c R '' ↑(AffineSubspace.perpBisector c y) =
        Metric.sphere (EuclideanGeometry.inversion c R y) (R ^ 2 / dist y c) \ {c}
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.norm_integral_le_of_norm_le_const_ae : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b C : ℝ} {f : ℝ → E},
  (∀ᵐ (x : ℝ), x ∈ Set.uIoc a b → ‖f x‖ ≤ C) → ‖∫ (x : ℝ) in a..b, f x‖ ≤ C * |b - a|
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify
PresheafOfModules.toPresheaf_map_toSheafify : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R₀ : CategoryTheory.Functor Cᵒᵖ RingCat} {R : CategoryTheory.Sheaf J RingCat} (α : R₀ ⟶ R.obj)
  [inst_1 : CategoryTheory.Presheaf.IsLocallyInjective J α] [inst_2 : CategoryTheory.Presheaf.IsLocallySurjective J α]
  {M₀ : PresheafOfModules R₀} {A : CategoryTheory.Sheaf J AddCommGrpCat} (φ : M₀.presheaf ⟶ A.obj)
  [inst_3 : CategoryTheory.Presheaf.IsLocallyInjective J φ] [inst_4 : CategoryTheory.Presheaf.IsLocallySurjective J φ],
  (PresheafOfModules.toPresheaf R₀).map (PresheafOfModules.toSheafify α φ) = φ
-- Mathlib.Analysis.InnerProductSpace.TwoDim
Orientation.abs_areaForm_of_orthogonal : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : Fact (Module.finrank ℝ E = 2)]
  (o : Orientation ℝ E (Fin 2)) {x y : E}, inner ℝ x y = 0 → |(o.areaForm x) y| = ‖x‖ * ‖y‖
-- Mathlib.NumberTheory.NumberField.Units.Basic
NumberField.Units.torsion_eq_one_or_neg_one_of_odd_finrank : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K],
  Odd (Module.finrank ℚ K) → ∀ (x : ↥(NumberField.Units.torsion K)), ↑x = 1 ∨ ↑x = -1
-- Mathlib.RingTheory.Localization.Basic
instIsScalarTowerLocalizationAlgebraMapSubmonoid : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) (S : Type u_2) [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S], IsScalarTower R (Localization M) (Localization (Algebra.algebraMapSubmonoid S M))
-- Mathlib.CategoryTheory.Abelian.LeftDerived
CategoryTheory.NatTrans.leftDerivedToHomotopyCategory_comp_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  [inst_2 : CategoryTheory.Abelian C] [inst_3 : CategoryTheory.HasProjectiveResolutions C]
  [inst_4 : CategoryTheory.Abelian D] {F G H : CategoryTheory.Functor C D} (α : F ⟶ G) (β : G ⟶ H) [inst_5 : F.Additive]
  [inst_6 : G.Additive] [inst_7 : H.Additive] {Z : CategoryTheory.Functor C (HomotopyCategory D (ComplexShape.down ℕ))}
  (h : H.leftDerivedToHomotopyCategory ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.NatTrans.leftDerivedToHomotopyCategory (CategoryTheory.CategoryStruct.comp α β)) h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.NatTrans.leftDerivedToHomotopyCategory α)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.NatTrans.leftDerivedToHomotopyCategory β) h)
-- Mathlib.Computability.Primrec.Basic
Primrec.ulower_down : ∀ {α : Type u_1} [inst : Primcodable α], Primrec ULower.down
-- Mathlib.Order.Category.PartOrd
PartOrd.ofHom_apply : ∀ {X Y : Type u} [inst : PartialOrder X] [inst_1 : PartialOrder Y] (f : X →o Y) (x : X),
  (CategoryTheory.ConcreteCategory.hom (PartOrd.ofHom f)) x = f x
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.instConditionallyCompleteLinearOrderBot : ConditionallyCompleteLinearOrderBot Cardinal.{u_1}
-- Mathlib.Tactic.NormNum.Core
Mathlib.Meta.NormNum.instInhabitedNormNums : Inhabited Mathlib.Meta.NormNum.NormNums
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.biproductUniqueIso_hom : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_2 : Unique J] (f : J → C),
  (CategoryTheory.Limits.biproductUniqueIso f).hom =
    CategoryTheory.Limits.biproduct.desc (CategoryTheory.Limits.limitBiconeOfUnique f).bicone.ι
-- Std.Http.Protocol.H1
/-- Signals that the user is not sending data anymore.
 -/
Std.Http.Protocol.H1.Machine.userClosedBody : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Machine dir → Std.Http.Protocol.H1.Machine dir
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.mul_eq_map₂ : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : Mul β] (f g : MeasureTheory.SimpleFunc α β),
  f * g = MeasureTheory.SimpleFunc.map (fun p => p.1 * p.2) (f.pair g)
-- Init.Data.AC
Lean.Data.AC.norm.eq_1 : ∀ {α : Sort u_1} [info : Lean.Data.AC.ContextInformation α] (ctx : α) (e : Lean.Data.AC.Expr),
  Lean.Data.AC.norm ctx e =
    if Lean.Data.AC.ContextInformation.isIdem ctx = true then
      Lean.Data.AC.mergeIdem
        (if Lean.Data.AC.ContextInformation.isComm ctx = true then
          Lean.Data.AC.sort (Lean.Data.AC.removeNeutrals ctx e.toList)
        else Lean.Data.AC.removeNeutrals ctx e.toList)
    else
      if Lean.Data.AC.ContextInformation.isComm ctx = true then
        Lean.Data.AC.sort (Lean.Data.AC.removeNeutrals ctx e.toList)
      else Lean.Data.AC.removeNeutrals ctx e.toList
-- Mathlib.Logic.Equiv.Fin.Basic
finSumNatEquiv_symm_apply_fin : ∀ {n : ℕ} (i : Fin n), (finSumNatEquiv n).symm ↑i = Sum.inl i
-- Std.Data.HashMap.Lemmas
Std.HashMap.find?_toArray_eq_some_iff_getKey?_eq_some_and_getElem?_eq_some : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k k' : α} {v : β}, Array.find? (fun a => a.1 == k) m.toArray = some (k', v) ↔ m.getKey? k = some k' ∧ m[k]? = some v
-- Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Dynamics.coverEntropyEntourage_le_coverEntropyInfEntourage : ∀ {X : Type u_1} {T : X → X} {U : SetRel X X} {F : Set X},
  Set.MapsTo T F F →
    ∀ [U.IsSymm], Dynamics.coverEntropyEntourage T F (U.comp U) ≤ Dynamics.coverEntropyInfEntourage T F U
-- Lean.Compiler.ExternAttr
Lean.instHashableExternAttrData.hash : Lean.ExternAttrData → UInt64
-- Mathlib.Topology.ContinuousOn
continuousWithinAt_insert_self : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {s : Set α}
  {x : α}, ContinuousWithinAt f (insert x s) x ↔ ContinuousWithinAt f s x