mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Tactic.BVDecide.LRAT.Parser
_private.Std.Tactic.BVDecide.LRAT.Parser.0.Std.Tactic.BVDecide.LRAT.lratProofToString.serializeClause : Array ℤ → String
-- Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Basic
/-- The bijection `(F₁ ⊗ F₂ ⟶ F₃) ≃ (F₂ ⟶ functorEnrichedHom C F₁ F₃)` when `F₁`, `F₂`
and `F₃` are functors `J ⥤ C`, and `C` is monoidal closed.  -/
CategoryTheory.MonoidalClosed.FunctorCategory.homEquiv : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.MonoidalClosed C] →
        {J : Type u₂} →
          [inst_3 : CategoryTheory.Category.{v₂, u₂} J] →
            [inst_4 :
                ∀ (F₁ F₂ : CategoryTheory.Functor J C),
                  CategoryTheory.Enriched.FunctorCategory.HasFunctorEnrichedHom C F₁ F₂] →
              {F₁ F₂ F₃ : CategoryTheory.Functor J C} →
                (CategoryTheory.MonoidalCategoryStruct.tensorObj F₁ F₂ ⟶ F₃) ≃
                  (F₂ ⟶ CategoryTheory.Enriched.FunctorCategory.functorEnrichedHom C F₁ F₃)
-- Mathlib.Combinatorics.SetFamily.Shadow
Finset.shadow_compls : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {𝒜 : Finset (Finset α)},
  𝒜.compls.shadow = 𝒜.upShadow.compls
-- Mathlib.GroupTheory.GroupExtension.Defs
/-- The inverse of an equivalence of group extensions is an equivalence.  -/
GroupExtension.Equiv.symm : {N : Type u_1} →
  {E : Type u_2} →
    {G : Type u_3} →
      [inst : Group N] →
        [inst_1 : Group E] →
          [inst_2 : Group G] →
            {S : GroupExtension N E G} →
              {E' : Type u_4} → [inst_3 : Group E'] → {S' : GroupExtension N E' G} → S.Equiv S' → S'.Equiv S
-- Aesop.Saturate
Aesop.SaturateM.instInhabitedContext : Inhabited Aesop.SaturateM.Context
-- Mathlib.Geometry.Manifold.ChartedSpace
/-- **Alias** of `ChartedSpace.ofDiscreteTopology`.

---

Any discrete space is a charted space over a singleton set.
We keep this as a definition (not an instance) to avoid instance search trying to search for
`DiscreteTopology` or `Unique` instances.
 -/
ChartedSpace.of_discreteTopology : {H : Type u} →
  {M : Type u_2} →
    [inst : TopologicalSpace M] →
      [inst_1 : TopologicalSpace H] → [DiscreteTopology M] → [h : Unique H] → ChartedSpace H M
-- Mathlib.Order.RelIso.Basic
RelIso.embeddingSurjectiveEquivIso_symm_apply_coe_apply : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ≃r s) (a : α),
  ↑(RelIso.embeddingSurjectiveEquivIso.symm f) a = f.toEquiv a
-- Mathlib.Analysis.Asymptotics.Defs
/-- Definition of `IsBigO` in terms of filters, with the constant in the lower bound.  -/
Asymptotics.isBigO_iff'' : ∀ {α : Type u_1} {E : Type u_3} {E''' : Type u_12} [inst : Norm E] [inst_1 : SeminormedAddGroup E'''] {f : α → E}
  {l : Filter α} {g : α → E'''}, f =O[l] g ↔ ∃ c > 0, ∀ᶠ (x : α) in l, c * ‖f x‖ ≤ ‖g x‖
-- Mathlib.LinearAlgebra.TensorProduct.Tower
TensorProduct.AlgebraTensorModule.coe_rTensor : ∀ {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {P : Type uP} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module A M]
  [inst_6 : IsScalarTower R A M] [inst_7 : AddCommMonoid N] [inst_8 : Module R N] [inst_9 : AddCommMonoid P]
  [inst_10 : Module R P] [inst_11 : Module A P] [inst_12 : IsScalarTower R A P] (f : M →ₗ[A] P),
  ⇑((TensorProduct.AlgebraTensorModule.rTensor R N) f) = ⇑(LinearMap.rTensor N (↑R f))
-- Mathlib.Data.Quot
Quotient.lift.decidablePred : {α : Sort u_1} →
  {sa : Setoid α} →
    (f : α → Prop) → (h : ∀ (a b : α), a ≈ b → f a = f b) → [DecidablePred f] → DecidablePred (Quotient.lift f h)
-- Mathlib.RingTheory.LocalRing.Basic
IsLocalRing.nonunits_add : ∀ {R : Type u_1} [inst : Semiring R] [IsLocalRing R] {a b : R}, a ∈ nonunits R → b ∈ nonunits R → a + b ∈ nonunits R
-- Mathlib.CategoryTheory.GradedObject.Bifunctor
CategoryTheory.GradedObject.mapBifunctorMapMap.eq_1 : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃]
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)) {I : Type u_4} {J : Type u_5} {K : Type u_6}
  (p : I × J → K) {X₁ X₂ : CategoryTheory.GradedObject I C₁} (f : X₁ ⟶ X₂) {Y₁ Y₂ : CategoryTheory.GradedObject J C₂}
  (g : Y₁ ⟶ Y₂) [inst_3 : (((CategoryTheory.GradedObject.mapBifunctor F I J).obj X₁).obj Y₁).HasMap p]
  [inst_4 : (((CategoryTheory.GradedObject.mapBifunctor F I J).obj X₂).obj Y₂).HasMap p],
  CategoryTheory.GradedObject.mapBifunctorMapMap F p f g =
    CategoryTheory.GradedObject.mapMap
      (CategoryTheory.CategoryStruct.comp (((CategoryTheory.GradedObject.mapBifunctor F I J).map f).app Y₁)
        (((CategoryTheory.GradedObject.mapBifunctor F I J).obj X₂).map g))
      p
-- Mathlib.GroupTheory.Sylow
Sylow.mapSurjective_surjective : ∀ {G : Type u_1} [inst : Group G] [inst_1 : Finite G] {G' : Type u_2} [inst_2 : Group G'] {f : G →* G'}
  (hf : Function.Surjective ⇑f) (p : ℕ) [inst_3 : Fact (Nat.Prime p)], Function.Surjective (Sylow.mapSurjective hf)
-- Mathlib.Topology.Algebra.Module.Multilinear.Topology
ContinuousMultilinearMap.eventually_nhds_zero_mapsTo : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {F : Type u_4} [inst : NormedField 𝕜]
  [inst_1 : (i : ι) → TopologicalSpace (E i)] [inst_2 : (i : ι) → AddCommGroup (E i)]
  [inst_3 : (i : ι) → Module 𝕜 (E i)] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F] [inst_6 : TopologicalSpace F]
  [inst_7 : IsTopologicalAddGroup F] {s : Set ((i : ι) → E i)},
  Bornology.IsVonNBounded 𝕜 s →
    ∀ {U : Set F}, U ∈ nhds 0 → ∀ᶠ (f : ContinuousMultilinearMap 𝕜 E F) in nhds 0, Set.MapsTo (⇑f) s U
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.lsub_le : ∀ {ι : Type u_3} {f : ι → Ordinal.{max u_4 u_3}} {a : Ordinal.{max u_4 u_3}}, (∀ (i : ι), f i < a) → Ordinal.lsub f ≤ a
-- Mathlib.Analysis.Convex.Join
convexJoin_empty_left : ∀ {𝕜 : Type u_2} {E : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : Module 𝕜 E] (t : Set E), convexJoin 𝕜 ∅ t = ∅
-- Mathlib.CategoryTheory.Functor.FunctorHom
/-- Composition of `homObjFunctor` with the co-Yoneda embedding, i.e. Hom(F ⊗ coyoneda(-), G).
When `F G : C ⥤ Type max v' v u`, this is the internal hom of `F` and `G`: see
`Mathlib/CategoryTheory/Closed/FunctorToTypes.lean`.  -/
CategoryTheory.Functor.functorHom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} D] →
        CategoryTheory.Functor C D → CategoryTheory.Functor C D → CategoryTheory.Functor C (Type (max v' v u))
-- Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
SSet.horn₃₁.exists_desc : ∀ {X : SSet} (f₀ f₂ f₃ : SSet.stdSimplex.obj { len := 2 } ⟶ X),
  CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 2) f₀ =
      CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 0) f₃ →
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 1) f₀ =
        CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 0) f₂ →
      CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 2) f₂ =
          CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 2) f₃ →
        ∃ φ,
          CategoryTheory.CategoryStruct.comp SSet.horn₃₁.ι₀ φ = f₀ ∧
            CategoryTheory.CategoryStruct.comp SSet.horn₃₁.ι₂ φ = f₂ ∧
              CategoryTheory.CategoryStruct.comp SSet.horn₃₁.ι₃ φ = f₃
-- Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
mem_multiples_of_prime_card : ∀ {G : Type u_2} [inst : AddGroup G] {p : ℕ} [hp : Fact (Nat.Prime p)],
  Nat.card G = p → ∀ {g g' : G}, g ≠ 0 → g' ∈ AddSubmonoid.multiples g
-- Mathlib.Analysis.Calculus.Deriv.Basic
hasStrictDerivAt_id : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] (x : 𝕜), HasStrictDerivAt id 1 x
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.Measure.Subtype.volume_def : ∀ {δ : Type u_4} {u : Set δ} [inst : MeasureTheory.MeasureSpace δ],
  MeasureTheory.volume = MeasureTheory.Measure.comap Subtype.val MeasureTheory.volume
-- Mathlib.AlgebraicGeometry.Scheme
/-- The forget functor `Scheme ⥤ LocallyRingedSpace` is fully faithful.  -/
AlgebraicGeometry.Scheme.fullyFaithfulForgetToLocallyRingedSpace : AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace.FullyFaithful
-- Mathlib.Data.Set.Lattice
Set.mem_iInter₂ : ∀ {γ : Type u_3} {ι : Sort u_5} {κ : ι → Sort u_8} {x : γ} {s : (i : ι) → κ i → Set γ},
  x ∈ ⋂ i, ⋂ j, s i j ↔ ∀ (i : ι) (j : κ i), x ∈ s i j
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.loopyOn_isLoopless_iff : ∀ {α : Type u_1} {E : Set α}, (Matroid.loopyOn E).Loopless ↔ E = ∅
-- Mathlib.AlgebraicTopology.SimplexCategory.Rev
SimplexCategory.revEquivalence_functor : SimplexCategory.revEquivalence.functor = SimplexCategory.rev
-- Aesop.Tree.Data
Aesop.NormalizationState.normal.sizeOf_spec : ∀ (postGoal : Lean.MVarId) (postState : Lean.Meta.SavedState)
  (script : Array (Aesop.DisplayRuleName × Option (Array Aesop.Script.LazyStep))),
  sizeOf (Aesop.NormalizationState.normal postGoal postState script) =
    1 + sizeOf postGoal + sizeOf postState + sizeOf script
-- Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
/-- The second vertex of a walk, or the only vertex in a nil walk.  -/
SimpleGraph.Walk.snd : {V : Type u} → {G : SimpleGraph V} → {u v : V} → G.Walk u v → V
-- Lean.Elab.Tactic.Induction
/-- Expand
```
syntax "induction " term,+ (" using " ident)?  ("generalizing " (colGt term:max)+)? (inductionAlts)? : tactic
```
if `inductionAlts` has an alternative with multiple LHSs, and likewise for
`cases`, `fun_induction`, `fun_cases`.
 -/
_private.Lean.Elab.Tactic.Induction.0.Lean.Elab.Tactic.expandInduction? : Lean.Syntax → Option Lean.Syntax
-- Mathlib.Geometry.Manifold.Instances.Sphere
stereoInvFun.congr_simp : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {v : E} (hv : ‖v‖ = 1)
  (w w_1 : ↥(ℝ ∙ v)ᗮ), w = w_1 → stereoInvFun hv w = stereoInvFun hv w_1
-- Mathlib.Analysis.InnerProductSpace.EuclideanDist
ContDiff.euclidean_dist : ∀ {F : Type u_2} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] {G : Type u_3} [inst_2 : NormedAddCommGroup G]
  [inst_3 : NormedSpace ℝ G] [inst_4 : FiniteDimensional ℝ G] {f g : F → G} {n : ℕ∞},
  ContDiff ℝ (↑n) f → ContDiff ℝ (↑n) g → (∀ (x : F), f x ≠ g x) → ContDiff ℝ ↑n fun x => Euclidean.dist (f x) (g x)
-- Lean.Meta.Tactic.Grind.EMatchTheorem
Lean.Meta.Grind.EMatchTheoremKind.toSyntax : Lean.Meta.Grind.EMatchTheoremKind → Lean.CoreM (Lean.TSyntax `Lean.Parser.Attr.grindMod)
-- Mathlib.NumberTheory.Padics.PadicVal.Basic
/-- The `p`-adic valuation of `(p * n)!` is `n` more than that of `n!`.  -/
padicValNat_factorial_mul : ∀ {p : ℕ} (n : ℕ) [hp : Fact (Nat.Prime p)], padicValNat p (p * n).factorial = padicValNat p n.factorial + n
-- Mathlib.LinearAlgebra.AffineSpace.Combination
/-- Viewing a module as an affine space modelled on itself, affine combinations are just linear
combinations.  -/
Finset.affineCombination_eq_linear_combination : ∀ {k : Type u_1} {V : Type u_2} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V] {ι : Type u_4}
  (s : Finset ι) (p : ι → V) (w : ι → k), ∑ i ∈ s, w i = 1 → (Finset.affineCombination k s p) w = ∑ i ∈ s, w i • p i
-- Mathlib.RingTheory.FractionalIdeal.Inverse
FractionalIdeal.inv_of_ne_zero : ∀ (K : Type u_3) [inst : Field K] {R₁ : Type u_4} [inst_1 : CommRing R₁] [inst_2 : IsDomain R₁] [inst_3 : Algebra R₁ K]
  [inst_4 : IsFractionRing R₁ K] {J : FractionalIdeal (nonZeroDivisors R₁) K} (h : J ≠ 0), J⁻¹ = ⟨↑1 / ↑J, ⋯⟩
-- Mathlib.MeasureTheory.Measure.Haar.OfBasis
mem_parallelepiped_iff : ∀ {ι : Type u_1} {E : Type u_3} [inst : Fintype ι] [inst_1 : AddCommGroup E] [inst_2 : Module ℝ E] (v : ι → E) (x : E),
  x ∈ parallelepiped v ↔ ∃ t ∈ Set.Icc 0 1, x = ∑ i, t i • v i
-- Lean.CoreM
Lean.DeclNameGenerator.mk : Lean.Name → ℕ → List ℕ → Lean.DeclNameGenerator
-- Std.Http.Data.Chunk
Std.Http.Chunk.instReprExtensionName : Repr Std.Http.Chunk.ExtensionName
-- Init.Data.SInt.Lemmas
Int32.add_neg_eq_sub : ∀ {a b : Int32}, a + -b = a - b
-- Mathlib.Algebra.Algebra.Tower
IsScalarTower.subsemiring : ∀ {S : Type v} {A : Type w} [inst : CommSemiring S] [inst_1 : Semiring A] [inst_2 : Algebra S A] (U : Subsemiring S),
  IsScalarTower (↥U) S A
-- Init.Data.List.TakeDrop
List.take_left' : ∀ {α : Type u_1} {l₁ l₂ : List α} {i : ℕ}, l₁.length = i → List.take i (l₁ ++ l₂) = l₁
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.singleAddMonoidHom_apply : ∀ {α : Type u_3} {E : α → Type u_4} [inst : (i : α) → NormedAddCommGroup (E i)] [inst_1 : DecidableEq α] (p : ENNReal)
  (i : α) (a : E i), (lp.singleAddMonoidHom p i) a = lp.single p i a
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
/-- The proposition that an affine point `(x, y)` lies in a Weierstrass curve `W`.

In other words, it satisfies the Weierstrass equation `W(X, Y) = 0`.  -/
WeierstrassCurve.Affine.Equation : {R : Type r} → [CommRing R] → WeierstrassCurve.Affine R → R → R → Prop
-- Mathlib.Analysis.Analytic.OfScalars
_private.Mathlib.Analysis.Analytic.OfScalars.0.FormalMultilinearSeries.tendsto_succ_norm_div_norm : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] (c : ℕ → 𝕜) {r r' : NNReal},
  r' ≠ 0 →
    Filter.Tendsto (fun n => ‖c n.succ‖ / ‖c n‖) Filter.atTop (nhds ↑r) →
      Filter.Tendsto (fun n => ‖‖c (n + 1)‖ * ↑r' ^ (n + 1)‖ / ‖‖c n‖ * ↑r' ^ n‖) Filter.atTop (nhds ↑(r' * r))
-- Std.Data.ExtDHashMap.Basic
/-- Tries to retrieve the mapping for the given key, panicking if no such mapping is present.

Uses the `LawfulBEq` instance to cast the retrieved value to the correct type.
 -/
Std.ExtDHashMap.get! : {α : Type u} →
  {β : α → Type v} →
    {x : BEq α} → {x_1 : Hashable α} → [LawfulBEq α] → Std.ExtDHashMap α β → (a : α) → [Inhabited (β a)] → β a
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
/-- A functor `F` preserves biproducts if it preserves biproducts of any shape `J` of size `w`.
The usual notion of preservation of biproducts is recovered by choosing `w` to be the universe
of the morphisms of `C`.  -/
CategoryTheory.Limits.PreservesBiproducts.preserves : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} D}
  {inst_2 : CategoryTheory.Limits.HasZeroMorphisms C} {inst_3 : CategoryTheory.Limits.HasZeroMorphisms D}
  {F : CategoryTheory.Functor C D} {inst_4 : F.PreservesZeroMorphisms}
  [self : CategoryTheory.Limits.PreservesBiproducts F] {J : Type w₁},
  CategoryTheory.Limits.PreservesBiproductsOfShape J F
-- Std.Time.Date.PlainDate
/-- Creates a new `PlainDate` from year, month, and day components.
 -/
Std.Time.PlainDate.ofYearMonthDay? : Std.Time.Year.Offset → Std.Time.Month.Ordinal → Std.Time.Day.Ordinal → Option Std.Time.PlainDate
-- Lean.Data.Lsp.Basic
Lean.Lsp.instFromJsonDocumentSelector : Lean.FromJson Lean.Lsp.DocumentSelector
-- Mathlib.GroupTheory.GroupAction.Defs
MulAction.mem_orbit_of_mem_orbit_subgroup : ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] {H : Subgroup G} {a b : α},
  a ∈ MulAction.orbit (↥H) b → a ∈ MulAction.orbit G b
-- Mathlib.NumberTheory.Chebyshev
Chebyshev.psi_mono : Monotone Chebyshev.psi
-- Mathlib.RingTheory.PiTensorProduct
/-- The map `Aᵢ ⟶ ⨂ᵢ Aᵢ` given by `a ↦ 1 ⊗ ... ⊗ a ⊗ 1 ⊗ ...`
 -/
PiTensorProduct.singleAlgHom : {ι : Type u_1} →
  {R : Type u_3} →
    {A : ι → Type u_4} →
      [inst : CommSemiring R] →
        [inst_1 : (i : ι) → Semiring (A i)] →
          [inst_2 : (i : ι) → Algebra R (A i)] → [DecidableEq ι] → (i : ι) → A i →ₐ[R] PiTensorProduct R fun i => A i
-- Mathlib.Computability.NFA
NFA.disjoint_evalFrom_reverse : ∀ {α : Type u} {σ : Type v} {M : NFA α σ} {x : List α} {S S' : Set σ},
  Disjoint S (M.reverse.evalFrom S' x) → Disjoint S' (M.evalFrom S x.reverse)
-- Mathlib.CategoryTheory.Sites.MayerVietorisSquare
CategoryTheory.GrothendieckTopology.MayerVietorisSquare.SheafCondition.map_f₂₄_op_glue : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  [inst_1 : CategoryTheory.HasWeakSheafify J (Type v)] {S : J.MayerVietorisSquare}
  {P : CategoryTheory.Functor Cᵒᵖ (Type v')} (h : S.SheafCondition P) (u : P.obj (Opposite.op S.X₂))
  (v : P.obj (Opposite.op S.X₃))
  (huv :
    (CategoryTheory.ConcreteCategory.hom (P.map S.f₁₂.op)) u =
      (CategoryTheory.ConcreteCategory.hom (P.map S.f₁₃.op)) v),
  (CategoryTheory.ConcreteCategory.hom (P.map S.f₂₄.op)) (h.glue u v huv) = u
-- Mathlib.GroupTheory.FreeGroup.Basic
/-- Transform a word representing a free group element into a word representing its
negative.  -/
FreeAddGroup.negRev : {α : Type u} → List (α × Bool) → List (α × Bool)
-- Mathlib.Computability.Partrec
Nat.Partrec.below.succ : ∀ {motive : (a : ℕ →. ℕ) → Nat.Partrec a → Prop}, Nat.Partrec.below Nat.Partrec.succ
-- Mathlib.Topology.Algebra.Nonarchimedean.Bases
/-- Condition for `B` to be a filter basis on `M`.  -/
SubmodulesBasis.inter : ∀ {ι : Type u_1} {R : Type u_2} [inst : CommRing R] {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : TopologicalSpace R] {B : ι → Submodule R M}, SubmodulesBasis B → ∀ (i j : ι), ∃ k, B k ≤ B i ⊓ B j
-- Mathlib.Algebra.BigOperators.Finprod
sum_finsum_comm : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : AddCommMonoid M] (s : Finset α) (f : α → β → M),
  (∀ a ∈ s, Function.HasFiniteSupport (f a)) → ∑ a ∈ s, ∑ᶠ (b : β), f a b = ∑ᶠ (b : β), ∑ a ∈ s, f a b
-- Mathlib.Analysis.Normed.Group.Seminorm
map_sub_le_max : ∀ {E : Type u_3} {F : Type u_4} [inst : AddGroup E] [inst_1 : FunLike F E ℝ] [NonarchAddGroupSeminormClass F E] (f : F)
  (x y : E), f (x - y) ≤ max (f x) (f y)
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCast?.congr_simp : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] (a : α) (a_1 a_2 : List ((a : α) × β a)),
  a_1 = a_2 → Std.Internal.List.getValueCast? a a_1 = Std.Internal.List.getValueCast? a a_2
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.succ_ne_zero : ∀ (o : Ordinal.{u_1}), Order.succ o ≠ 0
-- Mathlib.Algebra.Category.ModuleCat.Kernels
/-- The categorical cokernel of a morphism in `ModuleCat`
agrees with the usual module-theoretical quotient.
 -/
ModuleCat.cokernelIsoRangeQuotient : {R : Type u} →
  [inst : Ring R] →
    {G H : ModuleCat R} →
      (f : G ⟶ H) → CategoryTheory.Limits.cokernel f ≅ ModuleCat.of R (↑H ⧸ (ModuleCat.Hom.hom f).range)
-- Mathlib.Algebra.Homology.Embedding.ExtendHomotopy
Homotopy.extend.hom_eq_zero₁ : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Preadditive C] {K L : HomologicalComplex C c} (e : c.Embedding c')
  (φ : (i j : ι) → K.X i ⟶ L.X j) (i' j' : ι'), (∀ (i : ι), e.f i ≠ i') → Homotopy.extend.hom e φ i' j' = 0
-- Mathlib.Topology.Semicontinuity.Basic
/-- **Alias** of the reverse direction of `lowerSemicontinuousWithinAt_inv_iff`. -/
UpperSemicontinuousWithinAt.inv : ∀ {α : Type u_4} [inst : TopologicalSpace α] {β : Type u_5} {f : α → β} {s : Set α} {a : α} [inst_1 : PartialOrder β]
  [inst_2 : CommGroup β] [IsOrderedMonoid β], UpperSemicontinuousWithinAt f s a → LowerSemicontinuousWithinAt f⁻¹ s a
-- Mathlib.Topology.UniformSpace.Defs
lift_nhds_right : ∀ {α : Type ua} {β : Type ub} [inst : UniformSpace α] {x : α} {g : Set α → Filter β},
  Monotone g → (nhds x).lift g = (uniformity α).lift fun s => g {y | (y, x) ∈ s}
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.beth_le_beth : ∀ {o₁ o₂ : Ordinal.{u_1}}, Cardinal.beth o₁ ≤ Cardinal.beth o₂ ↔ o₁ ≤ o₂
-- Aesop.RuleTac.Basic
Aesop.instInhabitedCasesTarget.default : Aesop.CasesTarget
-- Mathlib.Data.Num.Prime
Num.Prime.eq_1 : ∀ (n : Num), n.Prime = Nat.Prime ↑n
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.comma_iso_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C) [P.RespectsIso]
  {A : Type u_1} {B : Type u_2} [inst_2 : CategoryTheory.Category.{v_1, u_1} A]
  [inst_3 : CategoryTheory.Category.{v_2, u_2} B] {L : CategoryTheory.Functor A C} {R : CategoryTheory.Functor B C}
  {f g : CategoryTheory.Comma L R} (e : f ≅ g), P f.hom ↔ P g.hom
-- Std.Http.Data.Headers.Basic
/-- Parses a header value into the typed representation.
 -/
Std.Http.Header.parse : {α : Type} → [self : Std.Http.Header α] → Std.Http.Header.Value → Option α
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.selRightfAction_actionHomRight : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (x x_1 x_2 : C) (f : x_1 ⟶ x_2),
  CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight x f =
    CategoryTheory.MonoidalCategoryStruct.whiskerLeft x f
-- Mathlib.SetTheory.Lists
Lists'.brecOn.eq : ∀ {α : Type u} {motive : (a : Bool) → Lists' α a → Sort u_1} {a : Bool} (t : Lists' α a)
  (F_1 : (a : Bool) → (t : Lists' α a) → Lists'.below t → motive a t),
  Lists'.brecOn t F_1 = F_1 a t (Lists'.brecOn.go t F_1).2
-- Mathlib.RingTheory.Spectrum.Prime.FreeLocus
Module.mem_freeLocus : ∀ {R : Type uR} {M : Type uM} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {p : PrimeSpectrum R},
  p ∈ Module.freeLocus R M ↔ Module.Free (Localization.AtPrime p.asIdeal) (LocalizedModule p.asIdeal.primeCompl M)
-- Mathlib.RingTheory.PowerBasis
PowerBasis.finrank : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] [StrongRankCondition R]
  (pb : PowerBasis R S), Module.finrank R S = pb.dim
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.instNonAssocRing : {X : Type u_1} → {Y : Type u_2} → [inst : TopologicalSpace X] → [NonAssocRing Y] → NonAssocRing (LocallyConstant X Y)
-- Mathlib.NumberTheory.Padics.Complex
PadicComplex.coe_eq : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] (x : PadicAlgCl p), ↑x = (algebraMap (PadicAlgCl p) ℂ_[p]) x
-- Mathlib.Topology.ContinuousOn
continuousWithinAt_univ : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) (x : α),
  ContinuousWithinAt f Set.univ x ↔ ContinuousAt f x
-- Init.Data.BitVec.Lemmas
BitVec.toNat_srem : ∀ {w : ℕ} {x y : BitVec w},
  (x.srem y).toNat =
    match x.msb, y.msb with
    | false, false => x.toNat % y.toNat
    | false, true => x.toNat % (-y).toNat
    | true, false => (-(-x % y)).toNat
    | true, true => (-(-x % -y)).toNat
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.preimage_mul_left_one' : ∀ {α : Type u_2} [inst : Group α] {a : α}, (fun x => a⁻¹ * x) ⁻¹' 1 = {a}
-- Std.Sync.Barrier
_private.Std.Sync.Barrier.0.Std.BarrierState : Type
-- Lean.Meta.Sym.Util
/-- Instantiates assigned metavariables, applies `shareCommon`, and eliminates holes (aka `none` cells)
in the local context.
 -/
Lean.Meta.Sym.preprocessMVar : Lean.MVarId → Lean.Meta.Sym.SymM Lean.MVarId
-- Mathlib.Algebra.Group.Units.Hom
AddUnits.map_id : ∀ (M : Type u) [inst : AddMonoid M], AddUnits.map (AddMonoidHom.id M) = AddMonoidHom.id (AddUnits M)
-- Init.Data.List.Sort.Impl
_private.Init.Data.List.Sort.Impl.0.List.MergeSort.Internal.mergeSortTR₂_run_eq_mergeSort : ∀ {α : Type u_1} {le : α → α → Bool} {n : ℕ} (l : { l // l.length = n }),
  List.MergeSort.Internal.mergeSortTR₂.run✝ le l = (↑l).mergeSort le
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.isEmpty_filter_key_eq_false_iff : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  {f : α → Bool},
  t.WF → ((Std.DTreeMap.Raw.filter (fun a x => f a) t).isEmpty = false ↔ ∃ k, ∃ (h : k ∈ t), f (t.getKey k h) = true)
-- Mathlib.Topology.Neighborhoods
map_nhds : ∀ {X : Type u} [inst : TopologicalSpace X] {α : Type u_1} {x : X} {f : X → α},
  Filter.map f (nhds x) = ⨅ s ∈ {s | x ∈ s ∧ IsOpen s}, Filter.principal (f '' s)
-- Mathlib.Algebra.Order.Monoid.Submonoid
Submonoid.mem_oneLE : ∀ {M : Type u_1} [inst : Monoid M] [inst_1 : Preorder M] [inst_2 : MulLeftMono M] {a : M}, a ∈ Submonoid.oneLE M ↔ 1 ≤ a
-- Mathlib.Algebra.Notation.Prod
Prod.smul_swap : ∀ {E : Type u_8} {α : Type u_9} {β : Type u_10} [inst : SMul E α] [inst_1 : SMul E β] (c : E) (p : α × β),
  (c • p).swap = c • p.swap