mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.NumberTheory.LSeries.AbstractFuncEq
IsStrongFEPair.symm : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {P : WeakFEPair E},
  IsStrongFEPair P → IsStrongFEPair P.symm
-- Init.Data.Float.Model.Float
/-- Determine whether `a` is less than or equal to `b` according to IEEE rules.

This is not a total ordering, and `≤` is not reflexive.
 -/
Float.Model.le : Float.Model → Float.Model → Bool
-- Mathlib.MeasureTheory.Measure.EverywherePos
MeasurableSet.everywherePosSubset : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α}
  [OpensMeasurableSpace α], MeasurableSet s → MeasurableSet (μ.everywherePosSubset s)
-- Std.Data.HashMap.Raw
Std.HashMap.Raw.instBEqOfHashable : {α : Type u} → {β : Type v} → [BEq α] → [Hashable α] → [BEq β] → BEq (Std.HashMap.Raw α β)
-- Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
/-- Given `S ≤ X` and `T ≤ Y`, this is the subcomplex of `X ⊗ Y` given by `(X ⊗ T) ⊔ (S ⊗ Y)`.  -/
SSet.Subcomplex.unionProd : {X Y : SSet} → X.Subcomplex → Y.Subcomplex → (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).Subcomplex
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.toCatCommSqOver_obj_snd_map : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) (X : Type u₄)
  [inst_3 : CategoryTheory.Category.{v₄, u₄} X]
  (J : CategoryTheory.Functor X (CategoryTheory.Limits.CategoricalPullback F G)) {X_1 Y : X} (f : X_1 ⟶ Y),
  ((CategoryTheory.Limits.CategoricalPullback.toCatCommSqOver F G X).obj J).snd.map f = (J.map f).snd
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.mem_filter : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α] {f : α → β → Bool} {k : α},
  m.WF →
    (k ∈ Std.DHashMap.Raw.filter f m ↔ ∃ (h' : k ∈ m), f (m.getKey k h') (Std.DHashMap.Raw.Const.get m k h') = true)
-- Mathlib.Analysis.InnerProductSpace.Reproducing
RKHS.coe_add : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {X : Type u_2} {V : Type u_3} [inst_1 : NormedAddCommGroup V]
  [inst_2 : InnerProductSpace 𝕜 V] {H : Type u_4} [inst_3 : NormedAddCommGroup H] [inst_4 : InnerProductSpace 𝕜 H]
  [inst_5 : RKHS 𝕜 H X V] (f g : H), ⇑(f + g) = ⇑f + ⇑g
-- Mathlib.Algebra.Homology.DerivedCategory.HomologySequence
DerivedCategory.shift_homologyFunctor : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] (n : ℤ),
  (DerivedCategory.homologyFunctor C 0).shift n = DerivedCategory.homologyFunctor C n
-- Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
/-- Repleteness exists for full and faithful functors but not fully faithful functors, which is
why we do this inefficiently.  -/
CategoryTheory.nerveFunctor.faithful : CategoryTheory.nerveFunctor.Faithful
-- Batteries.Data.MLList.Basic
/-- Gets the last element of a monadic lazy list, as an option in the monad.
This will run forever if the list is infinite.  -/
MLList.getLast? : {m : Type u_1 → Type u_1} → {α : Type u_1} → [Monad m] → MLList m α → m (Option α)
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.MatchResult.mk : {α : Type} → Array (Array (Array α)) → Lean.Meta.LazyDiscrTree.MatchResult α
-- Mathlib.Topology.Semicontinuity.Basic
/-- **Alias** of the reverse direction of `upperSemicontinuousWithinAt_neg_iff`. -/
LowerSemicontinuousWithinAt.neg : ∀ {α : Type u_4} [inst : TopologicalSpace α] {β : Type u_5} {f : α → β} {s : Set α} {a : α} [inst_1 : PartialOrder β]
  [inst_2 : AddCommGroup β] [IsOrderedAddMonoid β],
  LowerSemicontinuousWithinAt f s a → UpperSemicontinuousWithinAt (-f) s a
-- Mathlib.Analysis.Normed.Group.AddCircle
AddCircle.coe_real_preimage_closedBall_period_zero : ∀ (x ε : ℝ), QuotientAddGroup.mk ⁻¹' Metric.closedBall (↑x) ε = Metric.closedBall x ε
-- Mathlib.Algebra.Module.LinearMap.Defs
/-- Convert an `IsLinearMap` predicate to a `LinearMap`  -/
IsLinearMap.mk' : {R : Type u_1} →
  {M : Type u_8} →
    {M₂ : Type u_10} →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : AddCommMonoid M₂] →
            [inst_3 : Module R M] → [inst_4 : Module R M₂] → (f : M → M₂) → IsLinearMap R f → M →ₗ[R] M₂
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Cpop
Std.Tactic.BVDecide.BVExpr.bitblast.blastExtractAndExtendTarget.h : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {aig : Std.Sat.AIG α} {outWidth : ℕ}
  (self : Std.Tactic.BVDecide.BVExpr.bitblast.blastExtractAndExtendTarget aig outWidth), outWidth = self.w * self.w
-- Mathlib.RingTheory.DedekindDomain.Dvr
/-- Dedekind domains, in the sense of Noetherian integrally closed domains of Krull dimension ≤ 1,
are also Dedekind domains in the sense of Noetherian domains where the localization at every
nonzero prime ideal is a DVR.  -/
IsDedekindDomain.isDedekindDomainDvr : ∀ (A : Type u_1) [inst : CommRing A] [inst_1 : IsDomain A] [IsDedekindDomain A], IsDedekindDomainDvr A
-- Mathlib.Data.Finset.NAry
Finset.sup'_image₂_right : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} [inst : DecidableEq γ] {f : α → β → γ} {s : Finset α}
  {t : Finset β} [inst_1 : SemilatticeSup δ] (g : γ → δ) (h : (Finset.image₂ f s t).Nonempty),
  (Finset.image₂ f s t).sup' h g = t.sup' ⋯ fun y => s.sup' ⋯ fun x => g (f x y)
-- Mathlib.Order.Category.Semilat
SemilatInfCat.of.sizeOf_spec : ∀ (X : Type u) [isSemilatticeInf : SemilatticeInf X] [isOrderTop : OrderTop X],
  sizeOf { X := X, isSemilatticeInf := isSemilatticeInf, isOrderTop := isOrderTop } =
    1 + sizeOf X + sizeOf isSemilatticeInf + sizeOf isOrderTop
-- Mathlib.Topology.MetricSpace.HolderNorm
/-- **Alias** of the reverse direction of `eHolderNorm_lt_top`. -/
MemHolder.eHolderNorm_lt_top : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] {r : NNReal} {f : X → Y},
  MemHolder r f → eHolderNorm r f < ⊤
-- Mathlib.Data.Finset.Prod
Finset.product_eq_biUnion : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq (α × β)] (s : Finset α) (t : Finset β),
  s ×ˢ t = s.biUnion fun a => Finset.image (fun b => (a, b)) t
-- Mathlib.Data.Nat.Factorial.Basic
Nat.add_factorial_succ_le_factorial_add_succ : ∀ (i n : ℕ), i + (n + 1).factorial ≤ (i + (n + 1)).factorial
-- Mathlib.Analysis.Convex.Intrinsic
intrinsicFrontier_singleton : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [inst : Ring 𝕜] [inst_1 : AddCommGroup V] [inst_2 : Module 𝕜 V]
  [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P] (x : P), intrinsicFrontier 𝕜 {x} = ∅
-- Mathlib.Data.Finsupp.Basic
Finsupp.mapDomainEmbedding_apply : ∀ {α : Type u_12} {β : Type u_13} (f : α ↪ β) (v : α →₀ ℕ), (Finsupp.mapDomainEmbedding f) v = Finsupp.mapDomain (⇑f) v
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.comp_right_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : D} {T : CategoryTheory.Functor C D} {X Y Z : CategoryTheory.StructuredArrow S T} (f : X ⟶ Y) (g : Y ⟶ Z)
  {Z_1 : C} (h : Z.right ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.StructuredArrow.Hom.right (CategoryTheory.CategoryStruct.comp f g))
      h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.StructuredArrow.Hom.right f)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.StructuredArrow.Hom.right g) h)
-- Mathlib.Algebra.CharP.IntermediateField
IntermediateField.charZero : ∀ {F : Type u_1} {E : Type u_2} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (L : IntermediateField F E)
  [CharZero F], CharZero ↥L
-- Init.Data.String.Basic
String.Pos.Raw.isValidForSlice_sliceFrom : ∀ {s : String.Slice} {p : s.Pos} {off : String.Pos.Raw},
  String.Pos.Raw.IsValidForSlice (s.sliceFrom p) off ↔ String.Pos.Raw.IsValidForSlice s (off.offsetBy p.offset)
-- Mathlib.Tactic.NormNum.Basic
/-- The `norm_num` extension which identifies an expression `Int.cast n`, returning `n`.  -/
Mathlib.Meta.NormNum.evalIntCast : Mathlib.Meta.NormNum.NormNumExt
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.run_OptionT : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {α : Type u} {Q : Std.Do.PostCond (Option α) ps} [inst : Std.Do.WP m ps]
  (x : OptionT m α), ⦃(Std.Do.wp x).apply (fun a => Q.1 (some a), fun x => Q.1 none, Q.2)⦄ x.run ⦃Q⦄
-- Mathlib.Geometry.Manifold.Algebra.SMul
AddAction.contMDiffVAdd_compHom : ∀ {𝕜 : 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} {H' : Type u_4}
  [inst_4 : TopologicalSpace H'] {E' : Type u_5} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E']
  {I' : ModelWithCorners 𝕜 E' H'} {H'' : Type u_6} [inst_7 : TopologicalSpace H''] {E'' : Type u_7}
  [inst_8 : NormedAddCommGroup E''] [inst_9 : NormedSpace 𝕜 E''] {I'' : ModelWithCorners 𝕜 E'' H''} {G : Type u_8}
  [inst_10 : TopologicalSpace G] [inst_11 : ChartedSpace H G] {M : Type u_9} [inst_12 : TopologicalSpace M]
  [inst_13 : ChartedSpace H' M] [inst_14 : AddMonoid G] [inst_15 : AddAction G M] {n : WithTop ℕ∞}
  [ContMDiffVAdd I I' n G M] {G' : Type u_11} [inst_17 : TopologicalSpace G'] [inst_18 : ChartedSpace H'' G']
  [inst_19 : AddMonoid G'] {f : G' →+ G}, ContMDiff I'' I n ⇑f → ContMDiffVAdd I'' I' n G' M
-- Mathlib.Data.Multiset.Find
_private.Mathlib.Data.Multiset.Find.0.List.filter.match_1.eq_2 : ∀ (motive : Bool → Sort u_1) (h_1 : Unit → motive true) (h_2 : Unit → motive false),
  (match false with
    | true => h_1 ()
    | false => h_2 ()) =
    h_2 ()
-- Batteries.Data.Fin.Coding
/-- Encode `Empty` into `Fin 0`.  -/
Fin.encodeEmpty : Empty → Fin 0
-- Mathlib.NumberTheory.Harmonic.EulerMascheroni
/-- The sequence with `n`-th term `harmonic n - log n`. We use a junk value for `n = 0`, in order
to have the sequence be strictly decreasing.  -/
Real.eulerMascheroniSeq' : ℕ → ℝ
-- Mathlib.Algebra.Order.Monoid.Lex
OrderAddMonoidHom.snd_apply : ∀ (α : Type u_1) (β : Type u_2) [inst : AddMonoid α] [inst_1 : PartialOrder α] [inst_2 : AddMonoid β]
  [inst_3 : Preorder β] (self : α × β), (OrderAddMonoidHom.snd α β) self = self.2
-- Init.Grind.Ordered.Field
Lean.Grind.Field.IsOrdered.mul_le_mul_iff_of_pos_right : ∀ {R : Type u} [inst : Lean.Grind.Field R] [inst_1 : LE R] [inst_2 : LT R] [Std.LawfulOrderLT R]
  [inst_4 : Std.IsLinearOrder R] [Lean.Grind.OrderedRing R] {a b c : R}, 0 < c → (a * c ≤ b * c ↔ a ≤ b)
-- Std.Do.SPred.SVal
_private.Std.Do.SPred.SVal.0.Std.Do.SVal.curry.match_1.eq_2 : ∀ {α : Type u_1} (motive : (σs : List (Type u_1)) → (Std.Do.SVal.StateTuple σs → α) → Sort u_2) (head : Type u_1)
  (tail : List (Type u_1)) (f : Std.Do.SVal.StateTuple (head :: tail) → α)
  (h_1 : (f : Std.Do.SVal.StateTuple [] → α) → motive [] f)
  (h_2 :
    (head : Type u_1) →
      (tail : List (Type u_1)) → (f : Std.Do.SVal.StateTuple (head :: tail) → α) → motive (head :: tail) f),
  (match head :: tail, f with
    | [], f => h_1 f
    | head :: tail, f => h_2 head tail f) =
    h_2 head tail f
-- Mathlib.Algebra.Order.Module.Basic
inf_eq_half_smul_add_sub_abs_sub : ∀ (R : Type u_2) {M : Type u_3} [inst : Semiring R] [inst_1 : Invertible 2] [inst_2 : Lattice M]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [IsOrderedAddMonoid M] (x y : M), x ⊓ y = ⅟2 • (x + y - |y - x|)
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
SchwartzMap.integral_pow_mul_iteratedFDeriv_le : ∀ (𝕜 : Type u_2) {D : Type u_4} {V : Type u_9} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup D]
  [inst_2 : NormedSpace ℝ D] [inst_3 : NormedAddCommGroup V] [inst_4 : NormedSpace ℝ V] [inst_5 : NormedSpace 𝕜 V]
  [inst_6 : MeasurableSpace D] (μ : MeasureTheory.Measure D) [hμ : μ.HasTemperateGrowth] (f : SchwartzMap D V)
  (k n : ℕ),
  ∫ (x : D), ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ∂μ ≤
    (2 ^ μ.integrablePower * ∫ (x : D), (1 + ‖x‖) ^ (-↑μ.integrablePower) ∂μ) *
      ((SchwartzMap.seminorm 𝕜 0 n) f + (SchwartzMap.seminorm 𝕜 (k + μ.integrablePower) n) f)
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
Submodule.starProjection_comp_starProjection_of_le : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {U V : Submodule 𝕜 E} [inst_3 : U.HasOrthogonalProjection] [inst_4 : V.HasOrthogonalProjection],
  U ≤ V → U.starProjection ∘SL V.starProjection = U.starProjection
-- Mathlib.Order.Closure
/-- If `c` is a closure operator on `α` and `e` an order-isomorphism
between `α` and `β` then `e ∘ c ∘ e⁻¹` is a closure operator on `β`.  -/
ClosureOperator.conjBy : {α : Type u_4} →
  {β : Type u_5} → [inst : Preorder α] → [inst_1 : Preorder β] → ClosureOperator α → α ≃o β → ClosureOperator β
-- Mathlib.Data.Finset.Density
Finset.dens_mul_card : ∀ {α : Type u_2} [inst : Fintype α] (s : Finset α), s.dens * ↑(Fintype.card α) = ↑s.card
-- Mathlib.LinearAlgebra.Multilinear.Curry
MultilinearMap.currySum_apply : ∀ {R : Type uR} {ι : Type uι} {ι' : Type uι'} {M₂ : Type v₂} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₂]
  [inst_2 : Module R M₂] {N : ι ⊕ ι' → Type u_1} [inst_3 : (i : ι ⊕ ι') → AddCommMonoid (N i)]
  [inst_4 : (i : ι ⊕ ι') → Module R (N i)] (f : MultilinearMap R N M₂) (u : (i : ι) → N (Sum.inl i))
  (v : (i : ι') → N (Sum.inr i)), (f.currySum u) v = f fun t => Sum.rec u v t
-- Mathlib.CategoryTheory.Limits.MorphismProperty
CategoryTheory.CostructuredArrow.closedUnderLimitsOfShape_discrete_empty : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] (P : CategoryTheory.MorphismProperty T) {A : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} A] {L : CategoryTheory.Functor A T} [L.Faithful] [L.Full] {Y : A}
  [P.ContainsIdentities] [P.RespectsIso],
  (CategoryTheory.MorphismProperty.costructuredArrowObj L P).IsClosedUnderLimitsOfShape
    (CategoryTheory.Discrete PEmpty.{1})
-- Mathlib.RingTheory.Polynomial.Subring
/-- Given a polynomial `p` and a subring `T` that contains the coefficients of `p`,
return the corresponding polynomial whose coefficients are in `T`.  -/
Polynomial.toSubring : {R : Type u_1} → [inst : Ring R] → (p : Polynomial R) → (T : Subring R) → ↑p.coeffs ⊆ ↑T → Polynomial ↥T
-- Mathlib.ModelTheory.FinitelyGenerated
/-- A substructure of `M` is finitely generated if it is the closure of a finite subset of `M`.  -/
FirstOrder.Language.Substructure.FG : {L : FirstOrder.Language} → {M : Type u_1} → [inst : L.Structure M] → L.Substructure M → Prop
-- Mathlib.Algebra.ContinuedFractions.Computation.Basic
/-- Creates the integer and fractional part of a value `v`, i.e. `⟨⌊v⌋, v - ⌊v⌋⟩`.  -/
GenContFract.IntFractPair.of : {K : Type u_1} → [inst : DivisionRing K] → [inst_1 : LinearOrder K] → [FloorRing K] → K → GenContFract.IntFractPair K
-- Mathlib.Algebra.Algebra.Bilinear
LinearMap.pow_mulLeft : ∀ (R : Type u_1) (A : Type u_2) [inst : Semiring R] [inst_1 : Semiring A] [inst_2 : Module R A]
  [inst_3 : SMulCommClass R A A] (a : A) (n : ℕ), LinearMap.mulLeft R a ^ n = LinearMap.mulLeft R (a ^ n)
-- Mathlib.Algebra.Ring.BooleanRing
/-- Every Boolean algebra has the structure of a Boolean ring with the following data:

* `a + b` unfolds to `a ∆ b` (symmetric difference)
* `a * b` unfolds to `a ⊓ b`
* `-a` unfolds to `a`
* `0` unfolds to `⊥`
* `1` unfolds to `⊤`
 -/
BooleanAlgebra.toBooleanRing : {α : Type u_1} → [BooleanAlgebra α] → BooleanRing α
-- Mathlib.Tactic.Order.Graph.Basic
/-- An edge in a graph. In the `order` tactic, the `proof` field stores the of
`atoms[src] ≤ atoms[dst]`.  -/
Mathlib.Tactic.Order.Edge : Type
-- Mathlib.Algebra.Group.Prod
/-- Given additive monoids `A`, `B`, the natural projection homomorphism
from `A × B` to `B`  -/
AddMonoidHom.snd : (M : Type u_3) → (N : Type u_4) → [inst : AddZeroClass M] → [inst_1 : AddZeroClass N] → M × N →+ N
-- Std.Async.Signal
Std.Async.Signal.sigtrap.sizeOf_spec : sizeOf Std.Async.Signal.sigtrap = 1
-- Mathlib.MeasureTheory.Constructions.Cylinders
MeasureTheory.measurableCylinders.eq_cylinder : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → MeasurableSpace (α i)] {t : Set ((i : ι) → α i)}
  (ht : t ∈ MeasureTheory.measurableCylinders α),
  t = MeasureTheory.cylinder (MeasureTheory.measurableCylinders.finset ht) (MeasureTheory.measurableCylinders.set ht)
-- Lean.Parser.Command
Lean.Parser.Command.openSimple.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.Scheme.Hom.coe_image : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [H : AlgebraicGeometry.IsOpenImmersion f] {U : X.Opens},
  ↑((AlgebraicGeometry.Scheme.Hom.opensFunctor f).obj U) = ⇑f '' ↑U
-- Mathlib.Geometry.Manifold.Algebra.Monoid
instInhabitedContMDiffMonoidMorphism : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {n : WithTop ℕ∞} →
      {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 : Monoid G] →
                      [inst_5 : TopologicalSpace G] →
                        [inst_6 : ChartedSpace H G] →
                          {H' : Type u_5} →
                            [inst_7 : TopologicalSpace H'] →
                              {E' : Type u_6} →
                                [inst_8 : NormedAddCommGroup E'] →
                                  [inst_9 : NormedSpace 𝕜 E'] →
                                    {I' : ModelWithCorners 𝕜 E' H'} →
                                      {G' : Type u_7} →
                                        [inst_10 : Monoid G'] →
                                          [inst_11 : TopologicalSpace G'] →
                                            [inst_12 : ChartedSpace H' G'] →
                                              Inhabited (ContMDiffMonoidMorphism I I' n G G')
-- Std.Data.HashMap.Raw
/-- Returns a list of all keys present in the hash map in some order.  -/
Std.HashMap.Raw.keys : {α : Type u} → {β : Type v} → Std.HashMap.Raw α β → List α
-- Mathlib.Topology.Compactness.Compact
/-- The complement to a compact set belongs to a filter `f` if it belongs to each filter
`𝓝 x ⊓ f`, `x ∈ s`.  -/
IsCompact.compl_mem_sets : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X},
  IsCompact s → ∀ {f : Filter X}, (∀ x ∈ s, sᶜ ∈ nhds x ⊓ f) → sᶜ ∈ f
-- Mathlib.Algebra.Star.SelfAdjoint
selfAdjoint.mem_iff : ∀ {R : Type u_1} [inst : AddGroup R] [inst_1 : StarAddMonoid R] {x : R}, x ∈ selfAdjoint R ↔ star x = x
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey_filterMap : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp}
  [inst : Std.TransCmp cmp] {f : α → β → Option γ} {k : α} {h' : k ∈ Std.TreeMap.Raw.filterMap f t} (h : t.WF),
  (Std.TreeMap.Raw.filterMap f t).getKey k h' = t.getKey k ⋯
-- Mathlib.Order.SupClosed
InfClosed.biInf_mem_of_nonempty : ∀ {α : Type u_3} [inst : CompleteLattice α] {s : Set α} {ι : Type u_5} {t : Set ι} {f : ι → α},
  InfClosed s → t.Finite → t.Nonempty → (∀ i ∈ t, f i ∈ s) → ⨅ i ∈ t, f i ∈ s
-- Mathlib.Algebra.Ring.Ext
NonUnitalNonAssocRing.ext : ∀ {R : Type u} ⦃inst₁ inst₂ : NonUnitalNonAssocRing R⦄, HAdd.hAdd = HAdd.hAdd → HMul.hMul = HMul.hMul → inst₁ = inst₂
-- Mathlib.Analysis.Normed.Field.WithAbs
WithAbs.instFiniteDimensional : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring S] [inst_1 : PartialOrder S] [inst_2 : Field R] {T : Type u_3}
  [inst_3 : Field T] (v : AbsoluteValue R S) [inst_4 : Module R T] [FiniteDimensional R T],
  FiniteDimensional (WithAbs v) T
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.forIn.eq_1 : ∀ {α : Type u} {β : α → Type v} {δ : Type w} {m : Type w → Type u_1} [inst : Monad m]
  (f : (a : α) → β a → δ → m (ForInStep δ)) (init : δ) (t : Std.DTreeMap.Internal.Impl α β),
  Std.DTreeMap.Internal.Impl.forIn f init t = do
    let __do_lift ← Std.DTreeMap.Internal.Impl.forInStep f init t
    match __do_lift with
      | ForInStep.done d => pure d
      | ForInStep.yield d => pure d
-- Mathlib.Order.Partition.Basic
Partition.partOf_mem : ∀ {α : Type u_1} {x : α} {u : Set α} {P : Partition u}, x ∈ u → P.partOf x ∈ P
-- Mathlib.Topology.UrysohnsLemma
Urysohns.CU.approx_of_notMem_U : ∀ {X : Type u_1} [inst : TopologicalSpace X] {P : Set X → Set X → Prop} (c : Urysohns.CU P) (n : ℕ) {x : X},
  x ∉ c.U → Urysohns.CU.approx n c x = 1
-- Mathlib.NumberTheory.Dioph
/-- The set of places where two Diophantine functions are congruent modulo a third
is Diophantine.  -/
Dioph.«termD≡» : Lean.ParserDescr
-- Mathlib.LinearAlgebra.TensorProduct.Tower
Submodule.baseChange_span : ∀ {R : Type u_1} {M : Type u_2} (A : Type u_3) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] (s : Set M),
  Submodule.baseChange A (Submodule.span R s) = Submodule.span A (⇑((TensorProduct.mk R A M) 1) '' s)
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.Functor.CorepresentableBy.coyoneda_homEquiv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (X : Cᵒᵖ) (Y : C),
  (CategoryTheory.Functor.CorepresentableBy.coyoneda X).homEquiv = Equiv.refl (Opposite.unop X ⟶ Y)
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.degree_mul' : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] [NoZeroDivisors R]
  {f g : MvPolynomial σ R}, f * g ≠ 0 → m.degree (f * g) = m.degree f + m.degree g
-- Mathlib.Analysis.Normed.Group.Quotient
QuotientAddGroup.quotientQuotientIsometryEquivQuotient.eq_1 : ∀ {M : Type u_1} [inst : SeminormedAddCommGroup M] {S T : AddSubgroup M} (h : S ≤ T),
  QuotientAddGroup.quotientQuotientIsometryEquivQuotient h =
    { toEquiv := (QuotientAddGroup.quotientQuotientEquivQuotient S T h).toEquiv, isometry_toFun := ⋯ }
-- Mathlib.LinearAlgebra.Multilinear.Curry
MultilinearMap.currySum_uncurrySum : ∀ {R : Type uR} {ι : Type uι} {ι' : Type uι'} {M₂ : Type v₂} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₂]
  [inst_2 : Module R M₂] {N : ι ⊕ ι' → Type u_1} [inst_3 : (i : ι ⊕ ι') → AddCommMonoid (N i)]
  [inst_4 : (i : ι ⊕ ι') → Module R (N i)]
  (g : MultilinearMap R (fun i => N (Sum.inl i)) (MultilinearMap R (fun i => N (Sum.inr i)) M₂)),
  g.uncurrySum.currySum = g
-- Lean.Elab.Binders
_private.Lean.Elab.Binders.0.Lean.Elab.Term.expandFunBinders.loop : Array Lean.Syntax → Lean.Syntax → ℕ → Array Lean.Syntax → Lean.MacroM (Array Lean.Syntax × Lean.Syntax × Bool)
-- Mathlib.Topology.MetricSpace.Dilation
Dilation.lipschitz : ∀ {α : Type u_1} {β : Type u_2} {F : Type u_4} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β]
  [inst_2 : FunLike F α β] [inst_3 : DilationClass F α β] (f : F), LipschitzWith (Dilation.ratio f) ⇑f
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.ofNatIsoLeft_unit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} {H : CategoryTheory.Functor D C} (adj : F ⊣ H) (iso : F ≅ G),
  (adj.ofNatIsoLeft iso).unit =
    CategoryTheory.CategoryStruct.comp adj.unit (CategoryTheory.Functor.whiskerRight iso.hom H)
-- Mathlib.CategoryTheory.Adjunction.Quadruple
CategoryTheory.Adjunction.Quadruple.mk.inj : ∀ {C : Type u₁} {D : Type u₂} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.Category.{v₂, u₂} D}
  {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor D C} {G : CategoryTheory.Functor C D}
  {R : CategoryTheory.Functor D C} {adj₁ : L ⊣ F} {adj₂ : F ⊣ G} {adj₃ : G ⊣ R} {adj₁_1 : L ⊣ F} {adj₂_1 : F ⊣ G}
  {adj₃_1 : G ⊣ R},
  { adj₁ := adj₁, adj₂ := adj₂, adj₃ := adj₃ } = { adj₁ := adj₁_1, adj₂ := adj₂_1, adj₃ := adj₃_1 } →
    adj₁ = adj₁_1 ∧ adj₂ = adj₂_1 ∧ adj₃ = adj₃_1
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.Cfg.ret.sizeOf_spec : ∀ (a : Turing.ToPartrec.Cont) (a_1 : List ℕ), sizeOf (Turing.ToPartrec.Cfg.ret a a_1) = 1 + sizeOf a + sizeOf a_1