mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.SuccPred.Limit
/-- **Alias** of `Order.isSuccPrelimit_iff_isMin`. -/
Order.isSuccPrelimit_iff : ∀ {α : Type u_1} {a : α} [inst : PartialOrder α] [inst_1 : SuccOrder α] [IsSuccArchimedean α],
  Order.IsSuccPrelimit a ↔ IsMin a
-- Mathlib.GroupTheory.GroupExtension.Defs
AddGroupExtension.mk.inj : ∀ {N : Type u_1} {E : Type u_2} {G : Type u_3} {inst : AddGroup N} {inst_1 : AddGroup E} {inst_2 : AddGroup G}
  {inl : N →+ E} {rightHom : E →+ G} {inl_injective : Function.Injective ⇑inl}
  {range_inl_eq_ker_rightHom : inl.range = rightHom.ker} {rightHom_surjective : Function.Surjective ⇑rightHom}
  {inl_1 : N →+ E} {rightHom_1 : E →+ G} {inl_injective_1 : Function.Injective ⇑inl_1}
  {range_inl_eq_ker_rightHom_1 : inl_1.range = rightHom_1.ker}
  {rightHom_surjective_1 : Function.Surjective ⇑rightHom_1},
  { inl := inl, rightHom := rightHom, inl_injective := inl_injective,
        range_inl_eq_ker_rightHom := range_inl_eq_ker_rightHom, rightHom_surjective := rightHom_surjective } =
      { inl := inl_1, rightHom := rightHom_1, inl_injective := inl_injective_1,
        range_inl_eq_ker_rightHom := range_inl_eq_ker_rightHom_1, rightHom_surjective := rightHom_surjective_1 } →
    inl = inl_1 ∧ rightHom = rightHom_1
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.le_of_dvd : ∀ {a b : Ordinal.{u_4}}, b ≠ 0 → a ∣ b → a ≤ b
-- Mathlib.Data.Part
Part.bind_of_mem : ∀ {α : Type u_1} {β : Type u_2} {o : Part α} {a : α}, a ∈ o → ∀ (f : α → Part β), o.bind f = f a
-- Init.Data.Range.Polymorphic.UInt
UInt64.instHasSize_2 : Std.Rxi.HasSize UInt64
-- Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
CategoryTheory.hoFunctor.isIso_prodComparison_of_stdSimplex : ∀ {D : SSet} (X : SSet),
  (∀ (m : ℕ),
      CategoryTheory.IsIso (CategoryTheory.Limits.prodComparison SSet.hoFunctor D (SSet.stdSimplex.obj { len := m }))) →
    CategoryTheory.IsIso (CategoryTheory.Limits.prodComparison SSet.hoFunctor D X)
-- Aesop.Tree.Data.ForwardRuleMatches
/-- Erase several complete matches.  -/
Aesop.ForwardRuleMatches.eraseMany : Array Aesop.ForwardRuleMatch → Aesop.ForwardRuleMatches → Aesop.ForwardRuleMatches
-- Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
/-- `AddChar.zmod` bundled as an `AddChar`.  -/
AddChar.zmodHom : {n : ℕ} → [NeZero n] → AddChar (ZMod n) (AddChar (ZMod n) Circle)
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
/-- The pi-type of profinite groups is a profinite group.  -/
ProfiniteGrp.pi : {α : Type u} → (α → ProfiniteGrp.{u_1}) → ProfiniteGrp.{max u u_1}
-- Mathlib.Topology.ContinuousMap.CocompactMap
/-- A homeomorphism is a cocompact map.  -/
Homeomorph.toCocompactMap : {α : Type u_1} →
  {β : Type u_2} → [inst : TopologicalSpace α] → [inst_1 : TopologicalSpace β] → α ≃ₜ β → CocompactMap α β
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
/-- A commutative group object is a group object in the category of group objects.  -/
CategoryTheory.Grp.instGrpObj : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] →
        {H : CategoryTheory.Grp C} → [CategoryTheory.IsCommMonObj H.X] → CategoryTheory.GrpObj H
-- Mathlib.FieldTheory.KrullTopology
/-- If `L/K` is a field extension, then we have `Gal(L/K) ∈ fixedByFinite K L`.  -/
top_fixedByFinite : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L], ⊤ ∈ fixedByFinite K L
-- Mathlib.GroupTheory.GroupAction.SubMulAction
/-- A subset closed under the additive action inherits that action.  -/
SetLike.vadd' : {S : Type u'} →
  {M : Type v} →
    {N : Type u_1} →
      {α : Type u_2} →
        [inst : SetLike S α] →
          [inst_1 : VAdd M N] →
            [inst_2 : VAdd M α] →
              [inst_3 : AddMonoid N] →
                [inst_4 : AddAction N α] → [VAddMemClass S N α] → [VAddAssocClass M N α] → (s : S) → VAdd M ↥s
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.evalMonoidHom.eq_1 : ∀ {ι : Type u_1} (R : ι → Type u_2) {𝓕 : Filter ι} {S : ι → Type u_3} [inst : (i : ι) → SetLike (S i) (R i)]
  {B : (i : ι) → S i} (j : ι) [inst_1 : (i : ι) → Monoid (R i)] [inst_2 : ∀ (i : ι), SubmonoidClass (S i) (R i)],
  RestrictedProduct.evalMonoidHom R j = { toFun := fun x => x j, map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.Analysis.ODE.Transform
isIntegralCurveAt_comp_add : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {γ : ℝ → E} {v : ℝ → E → E} {t₀ dt : ℝ},
  IsIntegralCurveAt (γ ∘ fun x => x + dt) (v ∘ fun x => x + dt) (t₀ - dt) ↔ IsIntegralCurveAt γ v t₀
-- Mathlib.RingTheory.Extension.Cotangent.Basic
Algebra.Extension.H1Cotangent.map_eq : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {P : Algebra.Extension R S}
  {R' : Type u'} {S' : Type v'} [inst_3 : CommRing R'] [inst_4 : CommRing S'] [inst_5 : Algebra R' S']
  {P' : Algebra.Extension R' S'} [inst_6 : Algebra R R'] [inst_7 : Algebra S S'] [inst_8 : Algebra R S']
  [inst_9 : IsScalarTower R R' S'] [IsScalarTower R S S'] (f g : P.Hom P'),
  Algebra.Extension.H1Cotangent.map f = Algebra.Extension.H1Cotangent.map g
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.Entry.ext : Lean.Name → Lean.Meta.Grind.Entry
-- Mathlib.CategoryTheory.Abelian.Projective.Resolution
CategoryTheory.ProjectiveResolution.ofComplex.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.EnoughProjectives C] (Z : C),
  CategoryTheory.ProjectiveResolution.ofComplex Z =
    ChainComplex.mk' (CategoryTheory.Projective.over Z)
      (CategoryTheory.Projective.syzygies (CategoryTheory.Projective.π Z))
      (CategoryTheory.Projective.d (CategoryTheory.Projective.π Z)) fun {X₀ X₁} f =>
      ⟨CategoryTheory.Projective.syzygies f, ⟨CategoryTheory.Projective.d f, ⋯⟩⟩
-- Mathlib.Algebra.Quaternion
Quaternion.star_smul : ∀ {S : Type u_1} {R : Type u_3} [inst : CommRing R] [inst_1 : Monoid S] [inst_2 : DistribMulAction S R] (s : S)
  (a : Quaternion R), star (s • a) = s • star a
-- Lean.Compiler.LCNF.Types
/-- Given a LCNF `type` of the form `forall (a_1 : A_1) ... (a_n : A_n), B[a_1, ..., a_n]` and `p_1 : A_1, ... p_n : A_n`,
return `B[p_1, ..., p_n]`.

Remark: similar to `Meta.instantiateForall`, buf for LCNF types.
 -/
Lean.Compiler.LCNF.instantiateForall : Lean.Expr → Array Lean.Expr → Lean.CoreM Lean.Expr
-- Mathlib.Order.Filter.Ring
Filter.EventuallyLE.mul_nonneg : ∀ {α : Type u} {β : Type v} [inst : Semiring β] [inst_1 : PartialOrder β] [IsOrderedRing β] {l : Filter α}
  {f g : α → β}, 0 ≤ᶠ[l] f → 0 ≤ᶠ[l] g → 0 ≤ᶠ[l] f * g
-- Lean.Elab.InfoTree.Types
Lean.Elab.OptionInfo.mk : Lean.Syntax → Lean.Name → Lean.Name → Lean.Elab.OptionInfo
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.limit.isoLimitCone_hom_π_assoc : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor J C} [inst_2 : CategoryTheory.Limits.HasLimit F] (t : CategoryTheory.Limits.LimitCone F)
  (j : J) {Z : C} (h : F.obj j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.isoLimitCone t).hom
      (CategoryTheory.CategoryStruct.comp (t.cone.π.app j) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π F j) h
-- Lean.Meta.Match.MatcherApp.Basic
Lean.Meta.MatcherApp.toMatcherInfo : Lean.Meta.MatcherApp → Lean.Meta.MatcherInfo
-- Mathlib.Algebra.Homology.SpectralObject.Basic
CategoryTheory.Abelian.SpectralObject.sc₂_X₂ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{u_3, u_1} C]
  [inst_1 : CategoryTheory.Category.{u_4, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k)
  (h : CategoryTheory.CategoryStruct.comp f g = fg) (n₀ : ℤ),
  (X.sc₂ f g fg h n₀).X₂ = (X.H n₀).obj (CategoryTheory.ComposableArrows.mk₁ fg)
-- Mathlib.LinearAlgebra.Dual.Defs
Module.symm_dualMap_evalEquiv : ∀ (R : Type u_3) (M : Type u_4) [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Module.IsReflexive R M], ↑(Module.evalEquiv R M).symm.dualMap = Module.Dual.eval R (Module.Dual R M)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Maps
SimpleGraph.Walk.map_copy : ∀ {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G →g G') {u v u' v' : V} (p : G.Walk u v)
  (hu : u = u') (hv : v = v'), SimpleGraph.Walk.map f (p.copy hu hv) = (SimpleGraph.Walk.map f p).copy ⋯ ⋯
-- Mathlib.Algebra.Order.Field.Basic
le_div_self : ∀ {α : Type u_2} [inst : Semifield α] [inst_1 : PartialOrder α] [PosMulReflectLT α] {a b : α},
  0 ≤ a → 0 < b → b ≤ 1 → a ≤ a / b
-- Mathlib.Geometry.Manifold.VectorBundle.Basic
Bundle.contMDiff_proj : ∀ {n : WithTop ℕ∞} {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} (E : B → Type u_6) [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace 𝕜 F] [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_4 : (x : B) → TopologicalSpace (E x)] {EB : Type u_7} [inst_5 : NormedAddCommGroup EB]
  [inst_6 : NormedSpace 𝕜 EB] {HB : Type u_8} [inst_7 : TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB}
  [inst_8 : TopologicalSpace B] [inst_9 : ChartedSpace HB B] [inst_10 : FiberBundle F E],
  ContMDiff (IB.prod (modelWithCornersSelf 𝕜 F)) IB n Bundle.TotalSpace.proj
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.setIntegral_mono : ∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : PartialOrder E] [IsOrderedAddMonoid E] [IsOrderedModule ℝ E] {μ : MeasureTheory.Measure X} {f g : X → E}
  {s : Set X} [ClosedIciTopology E],
  MeasureTheory.IntegrableOn f s μ →
    MeasureTheory.IntegrableOn g s μ → f ≤ g → ∫ (x : X) in s, f x ∂μ ≤ ∫ (x : X) in s, g x ∂μ
-- Mathlib.Geometry.Manifold.LocalDiffeomorph
/-- A `C^n` diffeomorphism is a local diffeomorphism.  -/
Diffeomorph.isLocalDiffeomorph : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {H₁ : Type u_5}
  [inst_5 : TopologicalSpace H₁] {H₂ : Type u_6} [inst_6 : TopologicalSpace H₂] {I : ModelWithCorners 𝕜 E H₁}
  {J : ModelWithCorners 𝕜 F H₂} {M : Type u_8} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H₁ M] {N : Type u_9}
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace H₂ N] {n : WithTop ℕ∞} (Φ : Diffeomorph I J M N n),
  IsLocalDiffeomorph I J n ⇑Φ
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.get?_union : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : α → Type v} {m₁ m₂ : Std.DHashMap.Raw α β}
  [inst_2 : LawfulBEq α], m₁.WF → m₂.WF → ∀ {k : α}, (m₁ ∪ m₂).get? k = (m₂.get? k).or (m₁.get? k)
-- Mathlib.Topology.Algebra.Module.Determinant
ContinuousLinearEquiv.det_coe_symm : ∀ {R : Type u_1} [inst : Field R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] (A : M ≃L[R] M), (↑A.symm).det = (↑A).det⁻¹
-- Mathlib.Algebra.Module.Presentation.Tautological
_private.Mathlib.Algebra.Module.Presentation.Tautological.0.Module.Presentation.tautologicalRelations.match_1.splitter : (A : Type u_2) →
  (M : Type u_1) →
    (motive : Module.Presentation.tautological.R A M → Sort u_3) →
      (x : Module.Presentation.tautological.R A M) →
        ((m₁ m₂ : M) → motive (Module.Presentation.tautological.R.add m₁ m₂)) →
          ((a : A) → (m : M) → motive (Module.Presentation.tautological.R.smul a m)) → motive x
-- Mathlib.Topology.Sets.Opens
TopologicalSpace.Opens.mem_interior : ∀ {α : Type u_2} [inst : TopologicalSpace α] {s : Set α} {x : α}, x ∈ TopologicalSpace.Opens.interior s ↔ x ∈ interior s
-- Mathlib.Computability.EpsilonNFA
εNFA.εClosure.brecOn : ∀ {α : Type u} {σ : Type v} {M : εNFA α σ} {S : Set σ} {motive : (a : σ) → M.εClosure S a → Prop} {a : σ}
  (t : M.εClosure S a), (∀ (a : σ) (t : M.εClosure S a), εNFA.εClosure.below t → motive a t) → motive a t
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.mem_boxes : ∀ {ι : Type u_1} {I J : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I), J ∈ π.boxes ↔ J ∈ π
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.mem_iff_pullback_eq_top : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {S : CategoryTheory.Sieve X} (f : Y ⟶ X),
  S.arrows f ↔ CategoryTheory.Sieve.pullback f S = ⊤
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
/-- Given a functor `F : C₀ ⥤ C` and an object `S : C`, this structure roughly
contains the data of a pre-`1`-hypercover of `S` consisting of objects in `C₀`.  -/
CategoryTheory.Functor.PreOneHypercoverDenseData : {C₀ : Type u₀} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v₀, u₀} C₀] →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        CategoryTheory.Functor C₀ C → C → Type (max (max (max u₀ v) v₀) (w + 1))
-- Mathlib.Algebra.BigOperators.Group.List.Lemmas
List.prod_isUnit : ∀ {M : Type u_4} [inst : Monoid M] {L : List M}, (∀ m ∈ L, IsUnit m) → IsUnit L.prod
-- Std.Time.Format
/-- Formats a `DateTime` value into a simple date time with timezone string that can be parsed by the date% notation with the timezone identifier.
 -/
Std.Time.DateTime.toLeanDateTimeWithIdentifierString : Std.Time.DateTime → String
-- Mathlib.Topology.VectorBundle.Basic
ContinuousLinearMap.inCoordinates.eq_1 : ∀ {B : Type u_2} (F : Type u_3) (E : B → Type u_4) [inst : (x : B) → AddCommMonoid (E x)]
  [inst_1 : NormedAddCommGroup F] [inst_2 : TopologicalSpace B] [inst_3 : (x : B) → TopologicalSpace (E x)]
  {𝕜₁ : Type u_5} {𝕜₂ : Type u_6} [inst_4 : NontriviallyNormedField 𝕜₁] [inst_5 : NontriviallyNormedField 𝕜₂]
  {σ : 𝕜₁ →+* 𝕜₂} {B' : Type u_7} [inst_6 : TopologicalSpace B'] [inst_7 : NormedSpace 𝕜₁ F]
  [inst_8 : (x : B) → Module 𝕜₁ (E x)] [inst_9 : TopologicalSpace (Bundle.TotalSpace F E)] (F' : Type u_8)
  [inst_10 : NormedAddCommGroup F'] [inst_11 : NormedSpace 𝕜₂ F'] (E' : B' → Type u_9)
  [inst_12 : (x : B') → AddCommMonoid (E' x)] [inst_13 : (x : B') → Module 𝕜₂ (E' x)]
  [inst_14 : TopologicalSpace (Bundle.TotalSpace F' E')] [inst_15 : FiberBundle F E] [inst_16 : VectorBundle 𝕜₁ F E]
  [inst_17 : (x : B') → TopologicalSpace (E' x)] [inst_18 : FiberBundle F' E'] [inst_19 : VectorBundle 𝕜₂ F' E']
  (x₀ x : B) (y₀ y : B') (ϕ : E x →SL[σ] E' y),
  ContinuousLinearMap.inCoordinates F E F' E' x₀ x y₀ y ϕ =
    Bundle.Trivialization.continuousLinearMapAt 𝕜₂ (trivializationAt F' E' y₀) y ∘SL
      ϕ ∘SL Bundle.Trivialization.symmL 𝕜₁ (trivializationAt F E x₀) x
-- Mathlib.MeasureTheory.VectorMeasure.Prod
MeasureTheory.VectorMeasure.hasProd_flip_iff : ∀ {X : Type u_2} {Y : Type u_3} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X}
  {mY : MeasurableSpace Y} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G] [inst_5 : NormedSpace ℝ G]
  {μ : MeasureTheory.VectorMeasure X E} {ν : MeasureTheory.VectorMeasure Y F} {B : E →L[ℝ] F →L[ℝ] G},
  ν.HasProd μ B.flip ↔ μ.HasProd ν B
-- Batteries.Lean.EStateM
EStateM.Result.map_eq_error : ∀ {ε σ α β : Type u_1} (f : α → β) {x : EStateM.Result ε σ α} {e : ε} {s : σ},
  EStateM.Result.map f x = EStateM.Result.error e s ↔ x = EStateM.Result.error e s
-- Mathlib.Data.Set.Finite.Lattice
Set.infinite_of_not_bddAbove : ∀ {α : Type u} [inst : Preorder α] [IsDirectedOrder α] [Nonempty α] {s : Set α}, ¬BddAbove s → s.Infinite
-- Mathlib.LinearAlgebra.TensorProduct.Subalgebra
/-- Given `R`-algebras `S,T`, there is a natural `R`-linear isomorphism from `S ⊗[R] T` to
`S' ⊗[R] T'` where `S',T'` are the images of `S,T` in `S ⊗[R] T` respectively.
This is promoted to an `R`-algebra isomorphism `Algebra.TensorProduct.algEquivIncludeRange`.  -/
Algebra.TensorProduct.linearEquivIncludeRange : (R : Type u_1) →
  (S : Type u_2) →
    (T : Type u_3) →
      [inst : CommSemiring R] →
        [inst_1 : Semiring S] →
          [inst_2 : Algebra R S] →
            [inst_3 : Semiring T] →
              [inst_4 : Algebra R T] →
                TensorProduct R S T ≃ₗ[R]
                  TensorProduct R ↥Algebra.TensorProduct.includeLeft.range ↥Algebra.TensorProduct.includeRight.range
-- Mathlib.Algebra.Order.Archimedean.Basic
existsUnique_mul_zpow_mem_Ico : ∀ {G : Type u_1} [inst : CommGroup G] [inst_1 : LinearOrder G] [IsOrderedMonoid G] [MulArchimedean G] {a : G},
  1 < a → ∀ (b c : G), ∃! m, b * a ^ m ∈ Set.Ico c (c * a)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.maxKey?_bind_getKey? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp],
  t.maxKey?.bind t.getKey? = t.maxKey?
-- Mathlib.LinearAlgebra.Span.TensorProduct
Submodule.tensorEquivSpan_apply_tmul : ∀ {R : Type u_1} (A : Type u_2) {M : Type u_3} [inst : CommSemiring R] [inst_1 : CommSemiring 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]
  (p : Submodule R M) [inst_7 : Algebra.IsEpi R A] [inst_8 : Module.Flat R A] (a : A) (x : ↥p),
  ↑((Submodule.tensorEquivSpan A p) (a ⊗ₜ[R] x)) = a • ↑x
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.inter_div_subset : ∀ {α : Type u_2} [inst : Div α] {s₁ s₂ t : Set α}, s₁ ∩ s₂ / t ⊆ s₁ / t ∩ (s₂ / t)
-- Mathlib.Data.Set.Card
Set.ncard_inter_le_ncard_left : ∀ {α : Type u_1} (s t : Set α), autoParam s.Finite Set.ncard_inter_le_ncard_left._auto_1 → (s ∩ t).ncard ≤ s.ncard
-- Mathlib.Data.EReal.Operations
_private.Mathlib.Data.EReal.Operations.0.EReal.recENNReal_neg_coe_ennreal : {motive : EReal → Sort u_1} →
  (coe : (x : ENNReal) → motive ↑x) →
    (neg_coe : (x : ENNReal) → 0 < x → motive (-↑x)) →
      {x : ENNReal} → (hx : 0 < x) → ProofWanted (EReal.recENNReal coe neg_coe (-↑x) = neg_coe x hx)
-- Mathlib.Data.Multiset.Count
Multiset.count_zero : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α), Multiset.count a 0 = 0
-- Mathlib.Algebra.Homology.Embedding.TruncLE
HomologicalComplex.instMonoιTruncLE : ∀ {ι : 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.HasZeroMorphisms C]
  (K : HomologicalComplex C c') (e : c.Embedding c') [inst_2 : e.IsTruncLE] [inst_3 : ∀ (i' : ι'), K.HasHomology i']
  [inst_4 : CategoryTheory.Limits.HasZeroObject C], CategoryTheory.Mono (K.ιTruncLE e)
-- Mathlib.Data.Seq.Parallel
Computation.terminates_parallel : ∀ {α : Type u} {S : Stream'.WSeq (Computation α)} {c : Computation α},
  c ∈ S → ∀ [T : c.Terminates], (Computation.parallel S).Terminates
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.Opens.topIso_hom : ∀ {X : AlgebraicGeometry.Scheme} (U : X.Opens), U.topIso.hom = X.presheaf.map (CategoryTheory.eqToHom ⋯).op
-- Init.Data.UInt.Lemmas
UInt32.add_def : ∀ (a b : UInt32), a + b = { toBitVec := a.toBitVec + b.toBitVec }
-- Init.Data.SInt.Lemmas
Int8.toInt8_toISize : ∀ (n : Int8), n.toISize.toInt8 = n
-- Mathlib.Probability.Moments.CovarianceBilin
ProbabilityTheory.covarianceBilin_zero : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : MeasurableSpace E]
  [inst_3 : BorelSpace E], ProbabilityTheory.covarianceBilin 0 = 0
-- Mathlib.Analysis.MellinTransform
hasMellin_sub : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f g : ℝ → E} {s : ℂ},
  MellinConvergent f s → MellinConvergent g s → HasMellin (fun t => f t - g t) s (mellin f s - mellin g s)
-- Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
/-- The logarithmic counting function is even.
 -/
Function.locallyFinsuppWithin.logCounting_even : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : ProperSpace E] (D : Function.locallyFinsupp E ℤ),
  Function.Even (Function.locallyFinsuppWithin.logCounting D)
-- Std.Http.Data.Headers.Name
/-- Attempts to create a `Name` from a `String`, returning `none` if the string contains invalid
characters for HTTP header names or is empty.
 -/
Std.Http.Header.Name.ofString? : String → Option Std.Http.Header.Name
-- Mathlib.LinearAlgebra.Matrix.PosDef
Matrix.PosSemidef.conjTranspose_mul_mul_same : ∀ {m : Type u_1} {n : Type u_2} {R : Type u_3} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R]
  [inst_3 : Fintype n] [Finite m] {A : Matrix n n R},
  A.PosSemidef → ∀ (B : Matrix n m R), (B.conjTranspose * A * B).PosSemidef
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
CategoryTheory.Subgroupoid.disconnect_isTotallyDisconnected : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C] (S : CategoryTheory.Subgroupoid C), S.disconnect.IsTotallyDisconnected
-- Mathlib.Topology.Compactness.CountablyCompact
isCountablyCompact_iff_isCountablyCompact_univ : ∀ {E : Type u_2} [inst : TopologicalSpace E] {A : Set E}, IsCountablyCompact A ↔ IsCountablyCompact Set.univ
-- Mathlib.Tactic.Linter.Style
/-- The `nameCheck` linter emits a warning on declarations whose name is non-standard style.
(Currently, this only includes declarations whose name includes a double underscore.)

**Why is this bad?** Double underscores in theorem names can be considered non-standard style and
probably have been introduced by accident.
**How to fix this?** Use single underscores to separate parts of a name, following standard naming
conventions.
 -/
_private.Mathlib.Tactic.Linter.Style.0.Mathlib.Linter.Style.nameCheck.doubleUnderscore : Lean.Linter
-- Mathlib.Order.Interval.Finset.Defs
Finset.mem_Ioi : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrderTop α] {a x : α}, x ∈ Finset.Ioi a ↔ a < x
-- Mathlib.Probability.ProbabilityMassFunction.Basic
PMF.support.eq_1 : ∀ {α : Type u_1} (p : PMF α), p.support = Function.support ⇑p
-- Std.Time.Date.Unit.Year
/-- `Offset` represents a year offset, defined as an `Int`.
 -/
Std.Time.Year.Offset : Type
-- Mathlib.Algebra.Group.Units.Defs
/-- Units of a `Monoid`, bundled version. Notation: `αˣ`.

An element of a `Monoid` is a unit if it has a two-sided inverse.
This version bundles the inverse element so that it can be computed.
For a predicate see `IsUnit`.  -/
«term_ˣ» : Lean.TrailingParserDescr
-- Mathlib.CategoryTheory.FiberedCategory.HasFibers
HasFibers.Fib.homMk.congr_simp : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  {p : CategoryTheory.Functor 𝒳 𝒮} [inst_2 : HasFibers p] {S : 𝒮} {a b : HasFibers.Fib p S}
  (φ φ_1 : (HasFibers.ι S).obj a ⟶ (HasFibers.ι S).obj b) (e_φ : φ = φ_1)
  [inst_3 : p.IsHomLift (CategoryTheory.CategoryStruct.id S) φ], HasFibers.Fib.homMk φ = HasFibers.Fib.homMk φ_1
-- Lean.Elab.Tactic.Induction
_private.Lean.Elab.Tactic.Induction.0.Lean.Elab.Tactic.ElimApp.State.motive : Lean.Elab.Tactic.ElimApp.State✝ → Option Lean.MVarId
-- Mathlib.Algebra.Order.AddGroupWithTop
WithTop.LinearOrderedAddCommGroup.instNeg : {G : Type u_1} → [AddCommGroup G] → Neg (WithTop G)
-- Mathlib.Data.FunLike.Group
/-- A `FunLike` type is an additive commutative group if `β` is an additive
commutative group.  -/
FunLike.addCommGroup : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : FunLike F α β] →
        [inst_1 : Add F] →
          [inst_2 : Zero F] →
            [inst_3 : SMul ℕ F] →
              [inst_4 : Neg F] →
                [inst_5 : Sub F] →
                  [inst_6 : SMul ℤ F] →
                    [inst_7 : AddCommGroup β] →
                      [IsZeroApply F α β] →
                        [IsAddApply F α β] →
                          [IsNegApply F α β] →
                            [IsSubApply F α β] → [IsSMulApply ℕ F α β] → [IsSMulApply ℤ F α β] → AddCommGroup F
-- Mathlib.Topology.Maps.Basic
Topology.IsQuotientMap.of_comp_of_isCoinducing : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {f : X → Y} {g : Y → Z} [inst : TopologicalSpace X]
  [inst_1 : TopologicalSpace Y] [inst_2 : TopologicalSpace Z],
  Topology.IsQuotientMap (g ∘ f) → Topology.IsCoinducing f → Topology.IsQuotientMap g
-- Mathlib.GroupTheory.GroupAction.FixingSubgroup
mem_fixingSubgroup_compl_iff_movedBy_subset : ∀ (M : Type u_1) {α : Type u_2} [inst : Group M] [inst_1 : MulAction M α] {s : Set α} {m : M},
  m ∈ fixingSubgroup M sᶜ ↔ (MulAction.fixedBy α m)ᶜ ⊆ s