mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.Iterators.Lemmas.Producers.Monadic.Empty
_private.Std.Data.Iterators.Lemmas.Producers.Monadic.Empty.0.Std.IterM.toArray_eq_match_step.match_1.eq_1 : ∀ {α β : Type u_1} {m : Type u_1 → Type u_2} (motive : Std.IterStep (Std.IterM m β) β → Sort u_3) (it' : Std.IterM m β)
  (out : β) (h_1 : (it' : Std.IterM m β) → (out : β) → motive (Std.IterStep.yield it' out))
  (h_2 : (it' : Std.IterM m β) → motive (Std.IterStep.skip it')) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.yield it' out with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it' => h_2 it'
    | Std.IterStep.done => h_3 ()) =
    h_1 it' out
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get?_of_isEmpty : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  t.WF → ∀ {a : α}, t.isEmpty = true → Std.DTreeMap.Raw.Const.get? t a = none
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp.Completion
SemiNormedGrp.instAdditiveCompletion : SemiNormedGrp.completion.Additive
-- Init.Data.UInt.Lemmas
UInt8.ofNatLT_toNat : ∀ (n : UInt8), UInt8.ofNatLT n.toNat ⋯ = n
-- Aesop.Util.EqualUpToIds
Aesop.EqualUpToIds.Unsafe.levelsEqualUpToIdsCore : Lean.Level → Lean.Level → Aesop.EqualUpToIdsM Bool
-- Mathlib.CategoryTheory.Monoidal.Bimod
/-- An auxiliary morphism for the definition of the underlying morphism of the inverse component of
the associator isomorphism.  -/
Bimod.AssociatorBimod.invAux : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.Limits.HasCoequalizers C] →
        [inst_3 :
            ∀ (X : C),
              CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁}
                (CategoryTheory.MonoidalCategory.tensorLeft X)] →
          [inst_4 :
              ∀ (X : C),
                CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁}
                  (CategoryTheory.MonoidalCategory.tensorRight X)] →
            {R S T U : CategoryTheory.Mon C} →
              (P : Bimod R S) →
                (Q : Bimod S T) →
                  (L : Bimod T U) →
                    CategoryTheory.MonoidalCategoryStruct.tensorObj P.X (Q.tensorBimod L).X ⟶
                      ((P.tensorBimod Q).tensorBimod L).X
-- Std.Http.Data.Status
Std.Http.Status.movedPermanently.sizeOf_spec : sizeOf Std.Http.Status.movedPermanently = 1
-- Mathlib.Analysis.InnerProductSpace.Basic
/-- **Alias** of `norm_sub_sq`.

---

Expand the square  -/
norm_sub_pow_two : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (x y : E), ‖x - y‖ ^ 2 = ‖x‖ ^ 2 - 2 * RCLike.re (inner 𝕜 x y) + ‖y‖ ^ 2
-- Mathlib.Analysis.SpecialFunctions.Gamma.Basic
/-- The `Γ` function (of a real variable `s`).  -/
Real.Gamma : ℝ → ℝ
-- Mathlib.Topology.AlexandrovDiscrete
nhdsKer_subset_iff_isOpen : ∀ {α : Type u_3} [inst : TopologicalSpace α] [AlexandrovDiscrete α] {s : Set α}, nhdsKer s ⊆ s ↔ IsOpen s
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidIso.toAddEquiv : {α : Type u_6} →
  {β : Type u_7} →
    [inst : Preorder α] → [inst_1 : Preorder β] → [inst_2 : Add α] → [inst_3 : Add β] → (α ≃+o β) → α ≃+ β
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.MemLp.integrable_norm_pow' : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  [MeasureTheory.IsFiniteMeasure μ] {f : α → β} {p : ℕ},
  MeasureTheory.MemLp f (↑p) μ → MeasureTheory.Integrable (fun x => ‖f x‖ ^ p) μ
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.neg_product : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq α] [inst_1 : InvolutiveNeg α] [inst_2 : DecidableEq β]
  [inst_3 : InvolutiveNeg β] (s : Finset α) (t : Finset β), -s ×ˢ t = (-s) ×ˢ (-t)
-- Init.Data.UInt.Basic
/-- Subtracts one 16-bit unsigned integer from another, wrapping around on underflow. Usually accessed
via the `-` operator.

This function is overridden at runtime with an efficient implementation.
 -/
UInt16.sub : UInt16 → UInt16 → UInt16
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.Scheme.Pullback.t'_fst_fst_fst_assoc : ∀ {X Y Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst : ∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g]
  (i j k : 𝒰.I₀) {Z_1 : AlgebraicGeometry.Scheme} (h : 𝒰.X j ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.t' 𝒰 f g i j k)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g j k)
          (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g j i))
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Limits.pullback.fst
            (CategoryTheory.CategoryStruct.comp
              (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.f j) f) g) (𝒰.f j))
            (𝒰.f k))
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.f j) f) g) h))) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g i j)
        (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g i k))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.snd
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g) (𝒰.f i))
          (𝒰.f j))
        h)
-- Mathlib.Algebra.Ring.Subsemiring.Defs
AddSubmonoidWithOneClass.toAddMonoidWithOne : {S : Type u_1} →
  {R : Type u_2} →
    [inst : AddMonoidWithOne R] →
      [inst_1 : SetLike S R] → (s : S) → [AddSubmonoidWithOneClass S R] → AddMonoidWithOne ↥s
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey!_union_of_not_mem_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Inhabited α]
  [inst_1 : Std.TransCmp cmp] {k : α}, k ∉ t₁ → (t₁ ∪ t₂).getKey! k = t₂.getKey! k
-- Mathlib.CategoryTheory.Monoidal.Cartesian.GrpLimits
CategoryTheory.instPreservesLimitsOfShapeMonFunctorOppositeMonCatShrinkYonedaMon : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {J : Type w} [inst_2 : CategoryTheory.Category.{u_2, w} J] [CategoryTheory.Limits.HasLimitsOfShape J C],
  CategoryTheory.Limits.PreservesLimitsOfShape J CategoryTheory.shrinkYonedaMon.{max w v, v, u_1}
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
Pi.mabs_def : ∀ {ι : Type u_2} {α : ι → Type u_3} [inst : (i : ι) → Group (α i)] (f : (i : ι) → α i)
  [inst_1 : (i : ι) → Lattice (α i)], |f|ₘ = fun i => |f i|ₘ
-- Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
instAddCommGroupWithOneGradedTensorProduct : (R : Type u_3) →
  {ι : Type u_4} →
    {A : Type u_1} →
      {B : Type u_2} →
        [inst : CommSemiring ι] →
          [inst_1 : DecidableEq ι] →
            [inst_2 : CommRing R] →
              [inst_3 : Ring A] →
                [inst_4 : Ring B] →
                  [inst_5 : Algebra R A] →
                    [inst_6 : Algebra R B] →
                      (𝒜 : ι → Submodule R A) →
                        (ℬ : ι → Submodule R B) →
                          [inst_7 : GradedAlgebra 𝒜] →
                            [inst_8 : GradedAlgebra ℬ] → AddCommGroupWithOne (GradedTensorProduct R 𝒜 ℬ)
-- Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
UpperHalfPlane.num_neg : ∀ (g : GL (Fin 2) ℝ) (z : ℂ), UpperHalfPlane.num (-g) z = -UpperHalfPlane.num g z
-- Mathlib.LinearAlgebra.BilinearForm.Orthogonal
LinearMap.BilinForm.finrank_add_finrank_orthogonal' : ∀ {V : Type u_5} {K : Type u_6} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] [FiniteDimensional K V]
  {B : LinearMap.BilinForm K V} (W : Submodule K V),
  Module.finrank K ↥W + Module.finrank K ↥(B.orthogonal W) =
    Module.finrank K V + Module.finrank K ↥(W ⊓ LinearMap.ker B)
-- Mathlib.Algebra.Group.AddChar
AddChar.div_apply : ∀ {A : Type u_1} {M : Type u_2} [inst : AddCommGroup A] [inst_1 : CommMonoid M] (ψ χ : AddChar A M) (a : A),
  (ψ / χ) a = ψ a * χ (-a)
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
/-- A `MonoidalLeftAction C D` is the data of:
- For every object `c : C` and `d : D`, an object `c ⊙ₗ d` of `D`.
- For every morphism `f : (c : C) ⟶ c'` and every `d : D`, a morphism
  `f ⊵ₗ d : c ⊙ₗ d ⟶ c' ⊙ₗ d`.
- For every morphism `f : (d : D) ⟶ d'` and every `c : C`, a morphism
  `c ⊴ₗ f : c ⊙ₗ d ⟶ c ⊙ₗ d'`.
- For every pair of morphisms `f : (c : C) ⟶ c'` and
  `f : (d : D) ⟶ d'`, a morphism `f ⊙ₗ f' : c ⊙ₗ d ⟶ c' ⊙ₗ d'`.
- A structure isomorphism `αₗ c c' d : c ⊗ c' ⊙ₗ d ≅ c ⊙ₗ c' ⊙ₗ d`.
- A structure isomorphism `λₗ d : (𝟙_ C) ⊙ₗ d ≅ d`.

Furthermore, we require identities that turn `- ⊙ₗ -` into a bifunctor,
ensure naturality of `αₗ` and `λₗ`, and ensure compatibilities with
the associator and unitor isomorphisms in `C`.  -/
CategoryTheory.MonoidalCategory.MonoidalLeftAction : (C : Type u_1) →
  (D : Type u_2) →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [CategoryTheory.Category.{v_2, u_2} D] →
        [CategoryTheory.MonoidalCategory C] → Type (max (max (max u_1 u_2) v_1) v_2)
-- Lean.LocalContext
Lean.LocalDecl.cdecl.sizeOf_spec : ∀ (index : ℕ) (fvarId : Lean.FVarId) (userName : Lean.Name) (type : Lean.Expr) (bi : Lean.BinderInfo)
  (kind : Lean.LocalDeclKind),
  sizeOf (Lean.LocalDecl.cdecl index fvarId userName type bi kind) =
    1 + sizeOf index + sizeOf fvarId + sizeOf userName + sizeOf type + sizeOf bi + sizeOf kind
-- Mathlib.CategoryTheory.Monoidal.Closed.FunctorToTypes
CategoryTheory.FunctorToTypes.rightAdj_obj_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F G : CategoryTheory.Functor C (Type (max w v u))) {X Y : C}
  (f : X ⟶ Y),
  ((CategoryTheory.FunctorToTypes.rightAdj F).obj G).map f =
    TypeCat.ofHom fun x => { app := fun X_1 a => x.app X_1 (CategoryTheory.CategoryStruct.comp f a), naturality := ⋯ }
-- Mathlib.SetTheory.Ordinal.Principal
/-- **Alias** of `Ordinal.nfp_le_of_isPrincipal`. -/
Ordinal.nfp_le_of_principal : ∀ {a o : Ordinal.{u}} {op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}},
  a < o → Ordinal.IsPrincipal op o → Ordinal.nfp (op a) a ≤ o
-- Mathlib.Order.Preorder.Chain
IsChain.preimage_relIso : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {r' : β → β → Prop} {t : Set β},
  IsChain r' t → ∀ (φ : r ≃r r'), IsChain r (⇑φ ⁻¹' t)
-- Lean.ProjFns
Lean.instInhabitedAuxParentProjectionInfo : Inhabited Lean.AuxParentProjectionInfo
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.mk_range_inl : ∀ {α : Type u} {β : Type v}, Cardinal.mk ↑(Set.range Sum.inl) = Cardinal.lift.{v, u} (Cardinal.mk α)
-- Lean.Meta.CongrTheorems
_private.Lean.Meta.CongrTheorems.0.Lean.Meta.EqInfo.hyp.injEq : ∀ (fvarId fvarId_1 : Lean.FVarId), (Lean.Meta.EqInfo.hyp✝ fvarId = Lean.Meta.EqInfo.hyp✝ fvarId_1) = (fvarId = fvarId_1)
-- Mathlib.Order.SuccPred.Limit
Order.isPredPrelimit_of_pred_ne : ∀ {α : Type u_1} {a : α} [inst : PartialOrder α] [inst_1 : PredOrder α],
  (∀ (b : α), Order.pred b ≠ a) → Order.IsPredPrelimit a
-- Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument
CategoryTheory.SmallObject.πObj_ιIteration_app_right_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (I : CategoryTheory.MorphismProperty C) (κ : Cardinal.{w})
  [inst_1 : Fact κ.IsRegular] [inst_2 : OrderBot κ.ord.ToType] [inst_3 : I.IsCardinalForSmallObjectArgument κ] {X Y : C}
  (f : X ⟶ Y) {Z : C} (h : ((CategoryTheory.SmallObject.iteration I κ).obj (CategoryTheory.Arrow.mk f)).right ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.πObj I κ f)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Arrow.Hom.right ((CategoryTheory.SmallObject.ιIteration I κ).app (CategoryTheory.Arrow.mk f)))
        h) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.SmallObject.iteration I κ).obj (CategoryTheory.Arrow.mk f)).hom
      h
-- Init.Data.UInt.Lemmas
UInt32.le_refl : ∀ (a : UInt32), a ≤ a
-- Mathlib.CategoryTheory.Limits.Preserves.Presheaf
/-- (Implementation) A natural isomorphism we will need to construct `iso`.  -/
CategoryTheory.Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.isoAux : {C : Type u} →
  [inst : CategoryTheory.SmallCategory C] →
    [inst_1 : CategoryTheory.Limits.HasFiniteColimits C] →
      (A : CategoryTheory.Functor Cᵒᵖ (Type u)) →
        {J : Type} →
          [inst_2 : CategoryTheory.SmallCategory J] →
            [inst_3 : CategoryTheory.FinCategory J] →
              (K : CategoryTheory.Functor J Cᵒᵖ) →
                (CategoryTheory.CostructuredArrow.proj CategoryTheory.yoneda A).comp
                    (CategoryTheory.yoneda.comp
                      ((CategoryTheory.evaluation Cᵒᵖ (Type u)).obj (CategoryTheory.Limits.limit K))) ≅
                  (CategoryTheory.coyoneda.comp
                        ((CategoryTheory.Functor.whiskeringLeft
                              (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A) C (Type u)).obj
                          (CategoryTheory.CostructuredArrow.proj CategoryTheory.yoneda A))).obj
                    (CategoryTheory.Limits.limit K)
-- Mathlib.Analysis.InnerProductSpace.PiL2
/-- A shorthand for `Matrix.toLpLin 2 2`.  -/
Matrix.toEuclideanLin : {𝕜 : Type u_3} →
  [inst : RCLike 𝕜] →
    {m : Type u_7} →
      {n : Type u_8} → [Fintype n] → [DecidableEq n] → Matrix m n 𝕜 ≃ₗ[𝕜] EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 m
-- Mathlib.CategoryTheory.Limits.Bicones
/-- Given a category `J`, construct a walking `Bicone J` by adjoining two elements.  -/
CategoryTheory.Bicone : Type u₁ → Type u₁
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.BinaryBicones.functoriality_obj_inr : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {D : Type uD} [inst_2 : CategoryTheory.Category.{uD', uD} D] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  (P Q : C) (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms]
  (A : CategoryTheory.Limits.BinaryBicone P Q),
  ((CategoryTheory.Limits.BinaryBicones.functoriality P Q F).obj A).inr = F.map A.inr
-- Mathlib.RepresentationTheory.Rep.Basic
/-- The functor equipping a module with the trivial representation.  -/
Rep.trivialFunctor : (k : Type u) →
  (G : Type v) → [inst : Ring k] → [inst_1 : Monoid G] → CategoryTheory.Functor (ModuleCat k) (Rep.{w, u, v} k G)
-- Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor
CategoryTheory.Functor.LaxRightLinear.μᵣ_unitality_inv : ∀ {D : Type u_1} {D' : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} D]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D'] (F : CategoryTheory.Functor D D') {C : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C] [inst_3 : CategoryTheory.MonoidalCategory C]
  [inst_4 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D]
  [inst_5 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D'] [inst_6 : F.LaxRightLinear C] (d : D),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionUnitIso (F.obj d)).inv
      (CategoryTheory.Functor.LaxRightLinear.μᵣ F d (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) =
    F.map (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionUnitIso d).inv
-- Mathlib.Logic.Relator
Relator.LeftTotal.rel_exists : ∀ {α : Sort u₁} {β : Sort u₂} {R : α → β → Prop},
  Relator.LeftTotal R →
    Relator.LiftFun (Relator.LiftFun R fun x1 x2 => x1 → x2) (fun x1 x2 => x1 → x2) (fun p => ∃ i, p i) fun q =>
      ∃ i, q i
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.basicOpen_injOn_isIdempotentElem : ∀ {R : Type u} [inst : CommSemiring R], Set.InjOn PrimeSpectrum.basicOpen {e | IsIdempotentElem e}
-- Mathlib.Data.Multiset.Basic
Multiset.case_strongInductionOn : ∀ {α : Type u_1} {p : Multiset α → Prop} (s : Multiset α),
  p 0 → (∀ (a : α) (s : Multiset α), (∀ t ≤ s, p t) → p (a ::ₘ s)) → p s
-- Init.Data.Array.Lemmas
Array.pop_eq_of_push_eq : ∀ {α : Type u_1} {a b : α} {xs ys : Array α}, xs.push a = ys.push b → xs = ys
-- Mathlib.Topology.Gluing
/-- For each `i j : ι`, a transition map `t i j : V i j ⟶ V j i`  -/
TopCat.GlueData.MkCore.t : (self : TopCat.GlueData.MkCore) →
  (i j : self.J) →
    (TopologicalSpace.Opens.toTopCat (self.U i)).obj (self.V i j) ⟶
      (TopologicalSpace.Opens.toTopCat (self.U j)).obj (self.V j i)
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.indepFun_iff_indepSet_preimage : ∀ {Ω : Type u_1} {β : Type u_6} {β' : Type u_7} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {f : Ω → β}
  {g : Ω → β'} {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'} [MeasureTheory.IsZeroOrProbabilityMeasure μ],
  Measurable f →
    Measurable g →
      (ProbabilityTheory.IndepFun f g μ ↔
        ∀ (s : Set β) (t : Set β'),
          MeasurableSet s → MeasurableSet t → ProbabilityTheory.IndepSet (f ⁻¹' s) (g ⁻¹' t) μ)
-- Mathlib.Topology.MetricSpace.Perfect
/-- Any closed uncountable subset of a Polish space admits a continuous injection
from the Cantor space `ℕ → Bool`.  -/
IsClosed.exists_nat_bool_injection_of_not_countable : ∀ {α : Type u_1} [inst : TopologicalSpace α] [PolishSpace α] {C : Set α},
  IsClosed C → ¬C.Countable → ∃ f, Set.range f ⊆ C ∧ Continuous f ∧ Function.Injective f
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
CategoryTheory.Limits.pushout_inl_iso_of_left_factors_epi : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y : C} (h : W ⟶ X) [inst_1 : CategoryTheory.Epi h]
  (f : X ⟶ Y), CategoryTheory.IsIso (CategoryTheory.Limits.pushout.inl (CategoryTheory.CategoryStruct.comp h f) h)
-- Mathlib.Algebra.Group.Action.Pi
Pi.smulCommClass : ∀ {ι : Type u_1} {M : Type u_2} {N : Type u_3} {α : ι → Type u_4} [inst : (i : ι) → SMul M (α i)]
  [inst_1 : (i : ι) → SMul N (α i)] [∀ (i : ι), SMulCommClass M N (α i)], SMulCommClass M N ((i : ι) → α i)
-- Std.Time.Zoned.Database.TzIf
Std.Time.TimeZone.TZif.instInhabitedHeader : Inhabited Std.Time.TimeZone.TZif.Header
-- Init.Data.String.Subslice
String.Slice.endExclusive_subsliceFrom : ∀ {s : String.Slice} {newStart : s.Pos}, (s.subsliceFrom newStart).endExclusive = s.endPos
-- Mathlib.NumberTheory.MulChar.Basic
/-- Extensionality. Since `MulChar`s always take the value zero on non-units, it is sufficient
to compare the values on units.  -/
MulChar.ext : ∀ {R : Type u_1} [inst : CommMonoid R] {R' : Type u_2} [inst_1 : CommMonoidWithZero R'] {χ χ' : MulChar R R'},
  (∀ (a : Rˣ), χ ↑a = χ' ↑a) → χ = χ'
-- Lean.Parser.Term
/-- The universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`.  -/
Lean.Parser.Term.prop : Lean.Parser.Parser
-- Mathlib.Topology.Closure
interior_iInter₂_lt_nat : ∀ {X : Type u} [inst : TopologicalSpace X] {n : ℕ} (f : ℕ → Set X),
  interior (⋂ m, ⋂ (_ : m < n), f m) = ⋂ m, ⋂ (_ : m < n), interior (f m)
-- Init.Data.BitVec.Lemmas
BitVec.getMsbD_intMin : ∀ {w i : ℕ}, (BitVec.intMin w).getMsbD i = (decide (0 < w) && decide (i = 0))
-- Lean.Meta.LazyDiscrTree
_private.Lean.Meta.LazyDiscrTree.0.Lean.Meta.LazyDiscrTree.createImportedEnvironmentSeq.go.eq_def : ∀ {α : Type} (cctx : Lean.Core.Context) (env : Lean.Environment)
  (act : Lean.Name → Lean.AsyncConstantInfo → Lean.MetaM (Array (Lean.Meta.LazyDiscrTree.InitEntry α)))
  (d : Lean.Meta.LazyDiscrTree.ImportData) (cacheRef : IO.Ref Lean.Meta.LazyDiscrTree.Cache)
  (tree : Lean.Meta.LazyDiscrTree.PreDiscrTree α) (start stop : ℕ),
  Lean.Meta.LazyDiscrTree.createImportedEnvironmentSeq.go✝ cctx env act d cacheRef tree start stop =
    if start < stop then
      have mname := env.header.moduleNames[start]!;
      have mdata := env.header.moduleData[start]!;
      do
      let tree ← Lean.Meta.LazyDiscrTree.loadImportedModule cctx env act d cacheRef tree mname mdata
      Lean.Meta.LazyDiscrTree.createImportedEnvironmentSeq.go✝ cctx env act d cacheRef tree (start + 1) stop
    else Lean.Meta.LazyDiscrTree.toFlat d tree
-- Mathlib.Analysis.Normed.Operator.Bilinear
/-- Compose a bilinear map `E →SL[σ₁₃] F →SL[σ₂₃] G` with two linear maps
`E' →SL[σ₁'] E` and `F' →SL[σ₂'] F`.  -/
ContinuousLinearMap.bilinearComp : {𝕜 : Type u_1} →
  {𝕜₂ : Type u_2} →
    {𝕜₃ : Type u_3} →
      {E : Type u_4} →
        {F : Type u_6} →
          {G : Type u_8} →
            [inst : SeminormedAddCommGroup E] →
              [inst_1 : SeminormedAddCommGroup F] →
                [inst_2 : SeminormedAddCommGroup G] →
                  [inst_3 : NontriviallyNormedField 𝕜] →
                    [inst_4 : NontriviallyNormedField 𝕜₂] →
                      [inst_5 : NontriviallyNormedField 𝕜₃] →
                        [inst_6 : NormedSpace 𝕜 E] →
                          [inst_7 : NormedSpace 𝕜₂ F] →
                            [inst_8 : NormedSpace 𝕜₃ G] →
                              {σ₂₃ : 𝕜₂ →+* 𝕜₃} →
                                {σ₁₃ : 𝕜 →+* 𝕜₃} →
                                  {E' : Type u_11} →
                                    {F' : Type u_12} →
                                      [inst_9 : SeminormedAddCommGroup E'] →
                                        [inst_10 : SeminormedAddCommGroup F'] →
                                          {𝕜₁' : Type u_13} →
                                            {𝕜₂' : Type u_14} →
                                              [inst_11 : NontriviallyNormedField 𝕜₁'] →
                                                [inst_12 : NontriviallyNormedField 𝕜₂'] →
                                                  [inst_13 : NormedSpace 𝕜₁' E'] →
                                                    [inst_14 : NormedSpace 𝕜₂' F'] →
                                                      {σ₁' : 𝕜₁' →+* 𝕜} →
                                                        {σ₁₃' : 𝕜₁' →+* 𝕜₃} →
                                                          {σ₂' : 𝕜₂' →+* 𝕜₂} →
                                                            {σ₂₃' : 𝕜₂' →+* 𝕜₃} →
                                                              [RingHomCompTriple σ₁' σ₁₃ σ₁₃'] →
                                                                [RingHomCompTriple σ₂' σ₂₃ σ₂₃'] →
                                                                  [RingHomIsometric σ₂₃] →
                                                                    [RingHomIsometric σ₁₃'] →
                                                                      [RingHomIsometric σ₂₃'] →
                                                                        (E →SL[σ₁₃] F →SL[σ₂₃] G) →
                                                                          (E' →SL[σ₁'] E) →
                                                                            (F' →SL[σ₂'] F) →
                                                                              E' →SL[σ₁₃'] F' →SL[σ₂₃'] G
-- Mathlib.Data.NNRat.Defs
NNRat.ext_num_den : ∀ {p q : ℚ≥0}, p.num = q.num → p.den = q.den → p = q
-- Plausible.Testable
Plausible.Testable.andTestable : {p q : Prop} → [Plausible.Testable p] → [Plausible.Testable q] → Plausible.Testable (p ∧ q)
-- Mathlib.Tactic.NormNum.PowMod
Mathlib.Meta.NormNum.natPow_zero_natMod_one : ∀ {a : ℕ}, (a.pow 0).mod 1 = 0
-- Init.Data.Int.Linear
/-- Returns `true` if `k` divides all coefficients of the given linear polynomial.
 -/
Int.Internal.Linear.Poly.divCoeffs : ℤ → Int.Internal.Linear.Poly → Bool
-- Mathlib.Algebra.DirectSum.Module
DirectSum.ker_map : ∀ {ι : Type v} {M : ι → Type w} {N : ι → Type u_2} [inst : (i : ι) → AddCommGroup (M i)]
  [inst_1 : (i : ι) → AddCommMonoid (N i)] (f : (i : ι) → M i →+ N i),
  (DirectSum.map f).ker = AddSubgroup.comap (DirectSum.coeFnAddMonoidHom M) (AddSubgroup.pi Set.univ fun x => (f x).ker)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey!_erase : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α],
  t.WF → ∀ {k a : α}, (t.erase k).getKey! a = if cmp k a = Ordering.eq then default else t.getKey! a