mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.Iterators.Lemmas.Producers.Range
Std.Rcc.toArray_iter : ∀ {α : Type u_1} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerableLE α] [inst_4 : Std.Rxc.IsAlwaysFinite α]
  [inst_5 : Std.PRange.LawfulUpwardEnumerable α] {r : Std.Rcc α}, r.iter.toArray = r.toArray
-- Init.Prelude
/-- `a &&& b` computes the bitwise AND of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `&&&` in identifiers is `and`. -/
HAnd.hAnd : {α : Type u} → {β : Type v} → {γ : outParam (Type w)} → [self : HAnd α β γ] → α → β → γ
-- Init.Data.Array.Lemmas
List.toArray_range : ∀ {n : ℕ}, (List.range n).toArray = Array.range n
-- Mathlib.Combinatorics.SimpleGraph.Matching
SimpleGraph.Subgraph.IsMatching.verts_eq_biUnion_edgeSet : ∀ {V : Type u_1} {G : SimpleGraph V} {M : G.Subgraph}, M.IsMatching → M.verts = ⋃ e ∈ M.edgeSet, ↑e
-- Init.System.FilePath
/-- The character that is used to separate the entries in the `$PATH` (or `%PATH%`) environment variable.

This value is platform dependent.
 -/
System.SearchPath.separator : Char
-- Mathlib.Algebra.Star.StarAlgHom
/-- The composition of ⋆-algebra homomorphisms, as a ⋆-algebra homomorphism.  -/
StarAlgHom.comp : {R : Type u_2} →
  {A : Type u_3} →
    {B : Type u_4} →
      {C : Type u_5} →
        [inst : CommSemiring R] →
          [inst_1 : Semiring A] →
            [inst_2 : Algebra R A] →
              [inst_3 : Star A] →
                [inst_4 : Semiring B] →
                  [inst_5 : Algebra R B] →
                    [inst_6 : Star B] →
                      [inst_7 : Semiring C] →
                        [inst_8 : Algebra R C] → [inst_9 : Star C] → (B →⋆ₐ[R] C) → (A →⋆ₐ[R] B) → A →⋆ₐ[R] C
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.map₂Congr_hom_app_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {A : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} A] {B : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} B] {L : D} {R : CategoryTheory.Functor C D} {L' : B}
  {R' : CategoryTheory.Functor A B} {F : CategoryTheory.Functor C A} {G : CategoryTheory.Functor D B} (α : L' ⟶ G.obj L)
  (β : R.comp G ⟶ F.comp R') {F' : CategoryTheory.Functor C A} {G' : CategoryTheory.Functor D B} (e₁ : F ≅ F')
  (e₂ : G ≅ G') (α' : L' ⟶ G'.obj L) (β' : R.comp G' ⟶ F'.comp R')
  (hα :
    autoParam (α = CategoryTheory.CategoryStruct.comp α' (e₂.inv.app L))
      CategoryTheory.StructuredArrow.map₂Congr._auto_1)
  (hβ :
    autoParam
      (CategoryTheory.CategoryStruct.comp β (CategoryTheory.Functor.whiskerRight e₁.hom R') =
        CategoryTheory.CategoryStruct.comp (R.whiskerLeft e₂.hom) β')
      CategoryTheory.StructuredArrow.map₂Congr._auto_3)
  (X : CategoryTheory.StructuredArrow L R),
  ((CategoryTheory.StructuredArrow.map₂Congr α β e₁ e₂ α' β' hα hβ).hom.app X).right = e₁.hom.app X.right
-- Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
/-- The valuation of the discriminant of a Weierstrass curve `W`,
which is at most 1 if `W` is integral. Zero otherwise.  -/
WeierstrassCurve.valuation_Δ_aux : (R : Type u_1) →
  [inst : CommRing R] →
    [inst_1 : IsDomain R] →
      [IsDiscreteValuationRing R] →
        {K : Type u_2} →
          [inst_3 : Field K] → [inst_4 : Algebra R K] → [IsFractionRing R K] → WeierstrassCurve K → { v // v ≤ 1 }
-- Mathlib.Data.List.InsertIdx
List.subset_insertIdx : ∀ {α : Type u} (l : List α) (n : ℕ) (a : α), l ⊆ l.insertIdx n a
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.continuous_comap : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : CommSemiring S] (f : R →+* S),
  Continuous (PrimeSpectrum.comap f)
-- Aesop.Forward.RuleInfo
/-- The rule's rule pattern and the premise index that was assigned to it.  -/
Aesop.ForwardRuleInfo.rulePatternInfo? : Aesop.ForwardRuleInfo → Option (Aesop.RulePattern × Aesop.PremiseIndex)
-- Mathlib.CategoryTheory.ObjectProperty.EpiMono
CategoryTheory.ObjectProperty.instIsClosedUnderQuotientsIsZeroOfHasZeroMorphisms : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C],
  CategoryTheory.ObjectProperty.IsClosedUnderQuotients CategoryTheory.Limits.IsZero
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
/-- Every isomorphism is a regular monomorphism.  -/
CategoryTheory.RegularMono.ofIso : {C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → {X Y : C} → (e : X ≅ Y) → CategoryTheory.RegularMono e.hom
-- Mathlib.Analysis.Complex.Trigonometric
Complex.ofReal_sinh : ∀ (x : ℝ), ↑(Real.sinh x) = Complex.sinh ↑x
-- Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags
Multiplicative.preorder : {α : Type u_1} → [Preorder α] → Preorder (Multiplicative α)
-- Aesop.Script.SScript
Aesop.Script.instInhabitedSScript : Inhabited Aesop.Script.SScript
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen
ConvexOn.map_condExp_le_trim_univ : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {α : Type u_2} {f : α → E}
  {φ : E → ℝ} {m mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {mE : MeasurableSpace E} [BorelSpace E]
  (hm : m ≤ mα) [MeasureTheory.SigmaFinite (μ.trim hm)],
  ConvexOn ℝ Set.univ φ →
    LowerSemicontinuous φ →
      MeasureTheory.StronglyMeasurable φ →
        MeasureTheory.Integrable f μ → MeasureTheory.Integrable (φ ∘ f) μ → φ ∘ μ[f | m] ≤ᵐ[μ.trim hm] μ[φ ∘ f | m]
-- Std.Data.Internal.List.Associative
Std.Internal.List.maxKeyD_eraseKey_eq_of_beq_maxKeyD_eq_false : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k fallback : α},
      (Std.Internal.List.eraseKey k l).isEmpty = false →
        (k == Std.Internal.List.maxKeyD l fallback) = false →
          Std.Internal.List.maxKeyD (Std.Internal.List.eraseKey k l) fallback = Std.Internal.List.maxKeyD l fallback
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.getEntry?.eq_def : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (a : α) (x : Std.DHashMap.Internal.AssocList α β),
  Std.DHashMap.Internal.AssocList.getEntry? a x =
    match x with
    | Std.DHashMap.Internal.AssocList.nil => none
    | Std.DHashMap.Internal.AssocList.cons k v es =>
      if (k == a) = true then some ⟨k, v⟩ else Std.DHashMap.Internal.AssocList.getEntry? a es
-- Mathlib.GroupTheory.Subsemigroup.Centralizer
AddSubsemigroup.closureAddCommSemigroupOfComm.eq_1 : ∀ (M : Type u_1) [inst : AddSemigroup M] {s : Set M} (hcomm : ∀ a ∈ s, ∀ b ∈ s, a + b = b + a),
  AddSubsemigroup.closureAddCommSemigroupOfComm M hcomm = inferInstance
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Lemmas
_private.Std.Tactic.BVDecide.LRAT.Internal.Formula.Lemmas.0.Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.insertUnit.match_1.eq_1 : ∀ {n : ℕ} (motive : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) → Sort u_1)
  (l : Std.Tactic.BVDecide.LRAT.Internal.PosFin n) (b : Bool)
  (h_1 : (l : Std.Tactic.BVDecide.LRAT.Internal.PosFin n) → (b : Bool) → motive (l, b)),
  (match (l, b) with
    | (l, b) => h_1 l b) =
    h_1 l b
-- Mathlib.Data.PFunctor.Multivariate.W
MvPFunctor.WPath.brecOn.eq : ∀ {n : ℕ} {P : MvPFunctor.{u} (n + 1)} {motive : (a : P.last.W) → (a_1 : Fin2 n) → P.WPath a a_1 → Sort u_1}
  {a : P.last.W} {a_1 : Fin2 n} (t : P.WPath a a_1)
  (F_1 : (a : P.last.W) → (a_2 : Fin2 n) → (t : P.WPath a a_2) → MvPFunctor.WPath.below t → motive a a_2 t),
  MvPFunctor.WPath.brecOn t F_1 = F_1 a a_1 t (MvPFunctor.WPath.brecOn.go t F_1).2
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
SimpleGraph.Reachable.coe_subgraphMap : ∀ {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph} {G'' : G'.coe.Subgraph} (f : G'.coe →g G) {u v : ↑G''.verts},
  G''.coe.Reachable u v → (SimpleGraph.Subgraph.map f G'').coe.Reachable ⟨f ↑u, ⋯⟩ ⟨f ↑v, ⋯⟩
-- Mathlib.RingTheory.Discriminant
/-- A variation of `Algebra.discr_powerBasis_eq_prod`.  -/
Algebra.discr_powerBasis_eq_prod' : ∀ (K : Type u) {L : Type v} (E : Type z) [inst : Field K] [inst_1 : Field L] [inst_2 : Field E] [inst_3 : Algebra K L]
  [inst_4 : Algebra K E] [Module.Finite K L] [IsAlgClosed E] (pb : PowerBasis K L) [Algebra.IsSeparable K L]
  (e : Fin pb.dim ≃ (L →ₐ[K] E)),
  (algebraMap K E) (Algebra.discr K ⇑pb.basis) =
    ∏ i, ∏ j > i, -(((e j) pb.gen - (e i) pb.gen) * ((e i) pb.gen - (e j) pb.gen))
-- Std.Http.Data.Status
/-- 408 Request Timeout
 -/
Std.Http.Status.requestTimeout : Std.Http.Status
-- Mathlib.Combinatorics.Additive.VerySmallDoubling
/-- A non-empty set with no doubling is the left translate of its stabilizer.  -/
Finset.smul_stabilizer_of_no_doubling : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] {A : Finset G} {a : G},
  (A * A).card ≤ A.card → a ∈ A → a • ↑(MulAction.stabilizer G A) = ↑A
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cone.whisker_π : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C}
  (E : CategoryTheory.Functor K J) (c : CategoryTheory.Limits.Cone F),
  (CategoryTheory.Limits.Cone.whisker E c).π = E.whiskerLeft c.π
-- Mathlib.Order.WithBot
WithBot.le_coe_unbotD : ∀ {α : Type u_1} [inst : Preorder α] (x : WithBot α) (b : α), x ≤ ↑(WithBot.unbotD b x)
-- Mathlib.Order.Heyting.Regular
Heyting.Regular.coe_bot : ∀ {α : Type u_1} [inst : HeytingAlgebra α], ↑⊥ = ⊥
-- Mathlib.Algebra.GCDMonoid.Basic
gcd_dvd_gcd_mul_left : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : GCDMonoid α] (m n k : α), gcd m n ∣ gcd (k * m) n
-- Lean.Widget.UserWidget
Lean.Widget.getWidgetSource : Lean.Widget.GetWidgetSourceParams → Lean.Server.RequestM (Lean.Server.RequestTask Lean.Widget.WidgetSource)
-- Mathlib.Data.Finsupp.Order
Finsupp.support_tsub : ∀ {ι : Type u_1} {α : Type u_3} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [inst_2 : CanonicallyOrderedAdd α]
  [inst_3 : Sub α] [inst_4 : OrderedSub α] {f1 f2 : ι →₀ α}, (f1 - f2).support ⊆ f1.support
-- Mathlib.Order.Filter.Basic
Filter.instNontrivialFilter : ∀ {α : Type u} [Nonempty α], Nontrivial (Filter α)
-- Mathlib.Topology.Algebra.GroupWithZero
Filter.tendsto_mul_iff_of_ne_zero : ∀ {α : Type u_1} {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : TopologicalSpace G₀] [ContinuousInv₀ G₀]
  [ContinuousMul G₀] [T1Space G₀] {f g : α → G₀} {l : Filter α} {x y : G₀},
  Filter.Tendsto g l (nhds y) →
    y ≠ 0 → (Filter.Tendsto (fun n => f n * g n) l (nhds (x * y)) ↔ Filter.Tendsto f l (nhds x))
-- Mathlib.CategoryTheory.Bicategory.Modification.Lax
CategoryTheory.Lax.OplaxTrans.Modification.mk.injEq : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.LaxFunctor B C} {η θ : F ⟶ G} (app : (a : B) → η.app a ⟶ θ.app a)
  (naturality :
    autoParam
      (∀ {a b : B} (f : a ⟶ b),
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (app b)) (θ.naturality f) =
          CategoryTheory.CategoryStruct.comp (η.naturality f)
            (CategoryTheory.Bicategory.whiskerRight (app a) (G.map f)))
      CategoryTheory.Lax.OplaxTrans.Modification.naturality._autoParam)
  (app_1 : (a : B) → η.app a ⟶ θ.app a)
  (naturality_1 :
    autoParam
      (∀ {a b : B} (f : a ⟶ b),
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (app_1 b))
            (θ.naturality f) =
          CategoryTheory.CategoryStruct.comp (η.naturality f)
            (CategoryTheory.Bicategory.whiskerRight (app_1 a) (G.map f)))
      CategoryTheory.Lax.OplaxTrans.Modification.naturality._autoParam),
  ({ app := app, naturality := naturality } = { app := app_1, naturality := naturality_1 }) = (app = app_1)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Complex.sin_periodic : Function.Periodic Complex.sin (2 * ↑Real.pi)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get?_filter : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] {f : α → β → Bool} {k : α} (h : (↑m).WF),
  Std.DHashMap.Internal.Raw₀.Const.get? (Std.DHashMap.Internal.Raw₀.filter f m) k =
    (Std.DHashMap.Internal.Raw₀.Const.get? m k).pfilter fun x h' => f (m.getKey k ⋯) x
-- Mathlib.LinearAlgebra.Pi
/-- Linear equivalence between vectors in `M² = Fin 2 → M` and `M × M`.  -/
LinearEquiv.finTwoArrow : (R : Type u) →
  (M : Type v) → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → (Fin 2 → M) ≃ₗ[R] M × M
-- Mathlib.RingTheory.Flat.Basic
/-- `M` is flat if and only if `- ⊗ M` is an exact functor.
See `Module.Flat.iff_rTensor_exact'` to generalize the universe of
`N, N', N''` to any universe that is higher than `R` and `M`.  -/
Module.Flat.iff_rTensor_exact : ∀ {R : Type u} {M : Type v} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  Module.Flat R M ↔
    ∀ ⦃N N' N'' : Type (max u v)⦄ [inst_3 : AddCommGroup N] [inst_4 : AddCommGroup N'] [inst_5 : AddCommGroup N'']
      [inst_6 : Module R N] [inst_7 : Module R N'] [inst_8 : Module R N''] ⦃f : N →ₗ[R] N'⦄ ⦃g : N' →ₗ[R] N''⦄,
      Function.Exact ⇑f ⇑g → Function.Exact ⇑(LinearMap.rTensor M f) ⇑(LinearMap.rTensor M g)
-- Mathlib.Algebra.Lie.Weights.Cartan
LieAlgebra.coe_rootSpaceWeightSpaceProduct_tmul : ∀ (R : Type u_1) (L : Type u_2) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  (H : LieSubalgebra R L) [inst_3 : LieRing.IsNilpotent ↥H] (M : Type u_3) [inst_4 : AddCommGroup M]
  [inst_5 : Module R M] [inst_6 : LieRingModule L M] [inst_7 : LieModule R L M] (χ₁ χ₂ χ₃ : ↥H → R) (hχ : χ₁ + χ₂ = χ₃)
  (x : ↥(LieAlgebra.rootSpace H χ₁)) (m : ↥(LieModule.genWeightSpace M χ₂)),
  ↑((LieAlgebra.rootSpaceWeightSpaceProduct R L H M χ₁ χ₂ χ₃ hχ) (x ⊗ₜ[R] m)) = ⁅↑x, ↑m⁆
-- Mathlib.Algebra.Notation.Prod
Prod.mk_zero_zero : ∀ {M : Type u_3} {N : Type u_4} [inst : Zero M] [inst_1 : Zero N], (0, 0) = 0
-- Mathlib.LinearAlgebra.RootSystem.Basic
/-- Over a field of characteristic zero, to check that a finite family of roots form a
crystallographic root system, we do not need to check that the coroots are stable under reflections
since this follows from the corresponding property for the roots. Likewise, we do not need to
check that the coroots span.  -/
RootPairing.mk'' : {ι : Type u_1} →
  {M : Type u_3} →
    {N : Type u_4} →
      [inst : AddCommGroup M] →
        [inst_1 : AddCommGroup N] →
          [Finite ι] →
            {k : Type u_5} →
              [inst_3 : Field k] →
                [CharZero k] →
                  [inst_5 : Module k M] →
                    [inst_6 : Module k N] →
                      (p : M →ₗ[k] N →ₗ[k] k) →
                        [p.IsPerfPair] →
                          (root : ι ↪ M) →
                            (coroot : ι ↪ N) →
                              (∀ (i : ι), (p (root i)) (coroot i) = 2) →
                                (∀ (i : ι),
                                    Set.MapsTo (⇑(Module.preReflection (root i) (p.flip (coroot i)))) (Set.range ⇑root)
                                      (Set.range ⇑root)) →
                                  Submodule.span k (Set.range ⇑root) = ⊤ → RootPairing ι k M N
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.Key.proj.injEq : ∀ (a : Lean.Name) (a_1 a_2 : ℕ) (a_3 : Lean.Name) (a_4 a_5 : ℕ),
  (Lean.Meta.LazyDiscrTree.Key.proj a a_1 a_2 = Lean.Meta.LazyDiscrTree.Key.proj a_3 a_4 a_5) =
    (a = a_3 ∧ a_1 = a_4 ∧ a_2 = a_5)
-- Mathlib.RingTheory.PowerBasis
PowerBasis.natDegree_minpolyGen : ∀ {S : Type u_2} [inst : Ring S] {A : Type u_4} [inst_1 : CommRing A] [inst_2 : Algebra A S] [Nontrivial A]
  (pb : PowerBasis A S), pb.minpolyGen.natDegree = pb.dim
-- Mathlib.Topology.Category.TopCat.Monoidal
/-- The inclusion `X ⟶ X ⊗ I` given by `0 : I` for `X : TopCat`.  -/
TopCat.ι₀ : {X : TopCat} → X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj X TopCat.I
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Algebra.range_ofId : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A],
  (Algebra.ofId R A).range = ⊥
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomMulAct.instMulActionForall : {M : Type u_1} → {β : Type u_2} → {α : Type u_3} → [inst : Monoid M] → [MulAction M α] → MulAction Mᵈᵐᵃ (α → β)
-- Mathlib.SetTheory.Cardinal.Cofinality.Club
isStationary_sUnion_iff_of_cof_le_one : ∀ {α : Type v} [inst : LinearOrder α] {s : Set (Set α)},
  Order.cof α ≤ 1 → (IsStationary (⋃₀ s) ↔ ∃ x ∈ s, IsStationary x)
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
ContinuousLinearMap.coe_inr : ∀ {R : Type u_1} [inst : Semiring R] {M₁ : Type u_2} [inst_1 : TopologicalSpace M₁] [inst_2 : AddCommMonoid M₁]
  [inst_3 : Module R M₁] {M₂ : Type u_3} [inst_4 : TopologicalSpace M₂] [inst_5 : AddCommMonoid M₂]
  [inst_6 : Module R M₂], ↑(ContinuousLinearMap.inr R M₁ M₂) = LinearMap.inr R M₁ M₂
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
StarAlgHom.realContinuousMapOfNNReal_injective : ∀ {X : Type u_1} [inst : TopologicalSpace X] {A : Type u_2} [inst_1 : Ring A] [inst_2 : StarRing A]
  [inst_3 : Algebra ℝ A], Function.Injective StarAlgHom.realContinuousMapOfNNReal
-- Mathlib.Order.Atoms
IsSimpleOrder.instIsAtomic : ∀ {α : Type u_2} [inst : Lattice α] [inst_1 : BoundedOrder α] [IsSimpleOrder α], IsAtomic α
-- Mathlib.Algebra.Module.Submodule.Invariant
Module.End.invtSubmodule_smul : ∀ {M : Type u_2} [inst : AddCommMonoid M] {R : Type u_3} {S : Type u_4} [inst_1 : Semiring R] [inst_2 : Semiring S]
  [inst_3 : Module R M] [inst_4 : Module S M] [inst_5 : DistribSMul S R] [inst_6 : SMulCommClass R S M]
  [IsScalarTower S R M] (f : Module.End R M) (c : Sˣ), (c • f).invtSubmodule = f.invtSubmodule
-- Mathlib.Topology.Algebra.InfiniteSum.Group
Summable.update : ∀ {α : Type u_1} {β : Type u_2} {L : SummationFilter β} [inst : AddCommGroup α] [inst_1 : TopologicalSpace α]
  [IsTopologicalAddGroup α] {f : β → α} [L.LeAtTop],
  Summable f L → ∀ (b : β) [inst_4 : DecidableEq β] (a : α), Summable (Function.update f b a) L
-- Mathlib.RepresentationTheory.Basic
Representation.coeff_ofMulAction : ∀ {k : Type u_1} {G : Type u_2} [inst : Semiring k] [inst_1 : Group G] {H : Type u_4} [inst_2 : MulAction G H] (g : G)
  (f : MonoidAlgebra k H) (h : H), (((Representation.ofMulAction k G H) g) f).coeff h = f.coeff (g⁻¹ • h)
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
/-- The real logarithm is continuous as a function from positive reals.  -/
Real.continuous_log' : Continuous fun x => Real.log ↑x
-- Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic
ProbabilityTheory.IsGaussianProcess.comp_left : ∀ {T : Type u_2} {Ω : Type u_3} {E : Type u_4} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X : T → Ω → E}
  [inst : NormedAddCommGroup E] [inst_1 : MeasurableSpace E] [BorelSpace E] [inst_3 : NormedSpace ℝ E]
  [SecondCountableTopology E] {F : Type u_6} [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace ℝ F]
  [inst_7 : MeasurableSpace F] [BorelSpace F] [SecondCountableTopology F] (L : T → E →L[ℝ] F),
  ProbabilityTheory.IsGaussianProcess X P → ProbabilityTheory.IsGaussianProcess (fun t ω => (L t) (X t ω)) P
-- Mathlib.LinearAlgebra.QuadraticForm.Isometry
/-- The identity isometry from a quadratic form to itself.  -/
QuadraticMap.Isometry.id : {R : Type u_1} →
  {M : Type u_2} →
    {N : Type u_7} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : AddCommMonoid N] →
            [inst_3 : Module R M] → [inst_4 : Module R N] → (Q : QuadraticMap R M N) → Q →qᵢ Q
-- Mathlib.Analysis.Normed.Algebra.MatrixExponential
Matrix.exp_blockDiagonal' : ∀ {m : Type u_1} {n' : m → Type u_3} {𝔸 : Type u_5} [inst : Fintype m] [inst_1 : DecidableEq m]
  [inst_2 : (i : m) → Fintype (n' i)] [inst_3 : (i : m) → DecidableEq (n' i)] [inst_4 : Ring 𝔸]
  [inst_5 : TopologicalSpace 𝔸] [inst_6 : IsTopologicalRing 𝔸] [T2Space 𝔸] [Algebra ℚ 𝔸]
  (v : (i : m) → Matrix (n' i) (n' i) 𝔸),
  NormedSpace.exp (Matrix.blockDiagonal' v) = Matrix.blockDiagonal' (NormedSpace.exp v)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get!_alter_self : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] (h : t.WF) {k : α} [inst_1 : Inhabited (β k)] {f : Option (β k) → Option (β k)},
  (Std.DTreeMap.Internal.Impl.alter k f t ⋯).impl.get! k = (f (t.get? k)).get!
-- Std.Data.ExtDTreeMap.Basic
Std.ExtDTreeMap.mk'.sizeOf_spec : ∀ {α : Type u} {β : α → Type v} {cmp : autoParam (α → α → Ordering) Std.ExtDTreeMap._auto_1} [inst : SizeOf α]
  [inst_1 : (a : α) → SizeOf (β a)] (inner : Quotient (Std.DTreeMap.isSetoid α β cmp)),
  sizeOf { inner := inner } = 1 + sizeOf inner
-- Mathlib.Data.Finsupp.Basic
/-- Note the `hif` argument is needed for this to work in `rw`.  -/
Finsupp.comapDomain_zero : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : Zero M] (f : α → β)
  (hif : optParam (Set.InjOn f (f ⁻¹' ↑(Finsupp.support 0))) ⋯), Finsupp.comapDomain f 0 hif = 0
-- Init.System.IO
/-- Low-level system time, tracked in whole seconds and additional nanoseconds.
 -/
IO.FS.SystemTime : Type
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
/-- This map sends `f : C(X, ℝ)` to `Real.toNNReal ∘ f`, bundled as a continuous map `C(X, ℝ≥0)`.  -/
ContinuousMap.toNNReal : {X : Type u_1} → [inst : TopologicalSpace X] → C(X, ℝ) → C(X, NNReal)
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.stdSimplex.faceSingletonIso_zero_hom_comp_ι_eq_δ : CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.faceSingletonIso 0).hom (SSet.stdSimplex.face {0}).ι =
  SSet.stdSimplex.δ 1
-- Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
SimpleGraph.isExtremal_top_free_turanGraph : ∀ {n : ℕ} {α : Type u_2} [inst : Fintype α] [Nontrivial α],
  (SimpleGraph.turanGraph n (Fintype.card α - 1)).IsExtremal ⊤.Free
-- Mathlib.Order.Filter.AtTopBot.Tendsto
Filter.tendsto_atBot_mono' : ∀ {α : Type u_3} {β : Type u_4} [inst : Preorder β] (l : Filter α) ⦃f₁ f₂ : α → β⦄,
  f₂ ≤ᶠ[l] f₁ → Filter.Tendsto f₁ l Filter.atBot → Filter.Tendsto f₂ l Filter.atBot
-- Mathlib.Data.Fin.Tuple.Take
/-- Taking `m + 1` elements is equal to taking `m` elements and adding the `(m + 1)`th one.  -/
Fin.take_succ_eq_snoc : ∀ {n : ℕ} {α : Fin n → Sort u_1} (m : ℕ) (h : m < n) (v : (i : Fin n) → α i),
  Fin.take m.succ h v = Fin.snoc (Fin.take m ⋯ v) (v ⟨m, h⟩)
-- Mathlib.Data.Set.Operations
Set.seq_eq_image2 : ∀ {α : Type u} {β : Type v} (s : Set (α → β)) (t : Set α), s.seq t = Set.image2 (fun f a => f a) s t
-- Mathlib.CategoryTheory.Bicategory.Modification.Pseudo
/-- The naturality condition.  -/
CategoryTheory.Pseudofunctor.StrongTrans.Modification.naturality_assoc : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.Pseudofunctor B C} {η θ : F ⟶ G}
  (self : CategoryTheory.Pseudofunctor.StrongTrans.Modification η θ) {a b : B} (f : a ⟶ b) {Z : F.obj a ⟶ G.obj b}
  (h : CategoryTheory.CategoryStruct.comp (θ.app a) (G.map f) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (self.app b))
      (CategoryTheory.CategoryStruct.comp (θ.naturality f).hom h) =
    CategoryTheory.CategoryStruct.comp (η.naturality f).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (self.app a) (G.map f)) h)
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2to1.StAct.pop.injEq : ∀ {K : Type u_1} {Γ : K → Type u_2} {σ : Type u_4} {k : K} (a a_1 : σ → Option (Γ k) → σ),
  (Turing.TM2to1.StAct.pop a = Turing.TM2to1.StAct.pop a_1) = (a = a_1)
-- Mathlib.Algebra.Group.Subsemigroup.Basic
Subsemigroup.notMem_of_notMem_closure : ∀ {M : Type u_1} [inst : Mul M] {s : Set M} {P : M}, P ∉ Subsemigroup.closure s → P ∉ s