mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Spectral.Prespectral
/-- If `X` has a basis of compact opens and `f : X → S` is open, every
compact open of `S` is the image of a compact open of `X`.  -/
IsOpenMap.exists_opens_image_eq_of_prespectralSpace : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [PrespectralSpace X]
  {f : X → Y},
  Continuous f →
    IsOpenMap f → ∀ {U : Set Y}, U ⊆ Set.range f → IsOpen U → IsCompact U → ∃ V, IsCompact V.carrier ∧ f '' ↑V = U
-- Init.Data.SInt.Basic
instSubInt32 : Sub Int32
-- Mathlib.Algebra.Group.WithOne.Map
WithOne.map.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (f : α → β), WithOne.map f = Option.map f
-- Mathlib.CategoryTheory.Sites.CoversTop.Basic
/-- A family of elements of a presheaf of types `F` indexed by a family of objects
`Y : I → C` consists of the data of an element in `F.obj (Opposite.op (Y i))` for all `i`.  -/
CategoryTheory.Presheaf.FamilyOfElementsOnObjects : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.Functor Cᵒᵖ (Type w) → {I : Type u_1} → (I → C) → Type (max u_1 w)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.insertMany_nil : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp}, t.insertMany [] = t
-- Mathlib.RingTheory.Perfection
powMulEquiv.congr_simp : ∀ (M : Type u_1) (p p_1 : ℕ) (e_p : p = p_1) [inst : CommMonoid M] [inst_1 : PerfectRing M p],
  powMulEquiv M p = powMulEquiv M p_1
-- Mathlib.Analysis.Calculus.VectorField
VectorField.lieBracket_add_left : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {V W V₁ : E → E} {x : E},
  DifferentiableAt 𝕜 V x →
    DifferentiableAt 𝕜 V₁ x →
      VectorField.lieBracket 𝕜 (V + V₁) W x = VectorField.lieBracket 𝕜 V W x + VectorField.lieBracket 𝕜 V₁ W x
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.fixupInline : Lean.Doc.Inline Lean.ElabInline → Lean.Doc.DocM (Lean.Doc.Inline Lean.ElabInline)
-- Mathlib.Combinatorics.SimpleGraph.Sum
SimpleGraph.Embedding.sum_sum_comp_sumAssoc : ∀ {U : Type u_1} {U' : Type u_2} {V : Type u_3} {V' : Type u_4} {W : Type u_5} {W' : Type u_6} {G : SimpleGraph V}
  {H : SimpleGraph W} {I : SimpleGraph U} {G' : SimpleGraph V'} {H' : SimpleGraph W'} {I' : SimpleGraph U'}
  (f : G ↪g G') (g : H ↪g H') (h : I ↪g I'),
  (f.sum (g.sum h)).comp SimpleGraph.Iso.sumAssoc.toEmbedding =
    SimpleGraph.Iso.sumAssoc.toEmbedding.comp ((f.sum g).sum h)
-- Mathlib.Order.MinMax
le_of_max_le_left : ∀ {α : Type u} [inst : LinearOrder α] {a b c : α}, max a b ≤ c → a ≤ c
-- Mathlib.Topology.Maps.Basic
Topology.IsCoinducing.of_comp : ∀ {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],
  Continuous f → Continuous g → Topology.IsCoinducing (g ∘ f) → Topology.IsCoinducing g
-- Mathlib.Algebra.Notation.Pi.Defs
Function.const_div : ∀ {ι : Type u_1} {G : Type u_7} [inst : Div G] (a b : G),
  Function.const ι a / Function.const ι b = Function.const ι (a / b)
-- Mathlib.AlgebraicGeometry.Birational.Composition
/-- Composition respects equivalence of partial maps in both arguments.  -/
AlgebraicGeometry.Scheme.PartialMap.comp_equiv_of_equiv : ∀ {X Y Z : AlgebraicGeometry.Scheme} [inst : PreirreducibleSpace ↥X] [inst_1 : Nonempty ↥Y] (f₁ f₂ : X.PartialMap Y)
  [inst_2 : AlgebraicGeometry.IsDominant f₁.hom] [inst_3 : AlgebraicGeometry.IsDominant f₂.hom],
  f₁.equiv f₂ → ∀ (g₁ g₂ : Y.PartialMap Z), g₁.equiv g₂ → (f₁.comp g₁).equiv (f₂.comp g₂)
-- Mathlib.LinearAlgebra.LinearPMap
/-- Extend a `LinearPMap` to `f.domain ⊔ K ∙ x`.  -/
LinearPMap.supSpanSingleton : {E : Type u_4} →
  [inst : AddCommGroup E] →
    {F : Type u_5} →
      [inst_1 : AddCommGroup F] →
        {K : Type u_7} →
          {L : Type u_8} →
            [inst_2 : DivisionRing K] →
              [inst_3 : DivisionRing L] →
                {σ : K →+* L} →
                  [inst_4 : Module K E] →
                    [inst_5 : Module L F] → (f : E →ₛₗ.[σ] F) → (x : E) → F → x ∉ f.domain → E →ₛₗ.[σ] F
-- Mathlib.RingTheory.IsTensorProduct
/-- Let the following be a commutative diagram of rings
```
  R  →  S  →  T
  ↓     ↓     ↓
  R' →  S' →  T'
```
where the left-hand square is a pushout. Then the following are equivalent:
- the big rectangle is a pushout.
- the right-hand square is a pushout.

Note that this is essentially the isomorphism `T ⊗[S] (S ⊗[R] R') ≃ₐ[T] T ⊗[R] R'`.
 -/
Algebra.IsPushout.comp_iff : ∀ (R : Type u_1) (S : Type v₃) [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S] {T : Type u_4}
  [inst_3 : CommSemiring T] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [IsScalarTower R S T] (R' : Type u_6)
  (S' : Type u_7) [inst_7 : CommSemiring R'] [inst_8 : CommSemiring S'] [inst_9 : Algebra R R'] [inst_10 : Algebra S S']
  [inst_11 : Algebra R' S'] [inst_12 : Algebra R S'] [inst_13 : IsScalarTower R R' S'] [inst_14 : IsScalarTower R S S']
  {T' : Type u_8} [inst_15 : CommSemiring T'] [inst_16 : Algebra R T'] [inst_17 : Algebra S' T']
  [inst_18 : Algebra S T'] [inst_19 : Algebra T T'] [inst_20 : Algebra R' T'] [inst_21 : IsScalarTower R T T']
  [inst_22 : IsScalarTower S T T'] [inst_23 : IsScalarTower S S' T'] [inst_24 : IsScalarTower R R' T']
  [IsScalarTower R S' T'] [IsScalarTower R' S' T'] [Algebra.IsPushout R S R' S'],
  Algebra.IsPushout R T R' T' ↔ Algebra.IsPushout S T S' T'
-- Mathlib.FieldTheory.Extension
/-- The union of a chain of lifts.  -/
IntermediateField.Lifts.union : {F : Type u_1} →
  {E : Type u_2} →
    {K : Type u_3} →
      [inst : Field F] →
        [inst_1 : Field E] →
          [inst_2 : Field K] →
            [inst_3 : Algebra F E] →
              [inst_4 : Algebra F K] →
                (c : Set (IntermediateField.Lifts F E K)) →
                  IsChain (fun x1 x2 => x1 ≤ x2) c → IntermediateField.Lifts F E K
-- Mathlib.MeasureTheory.Integral.FinMeasAdditive
MeasureTheory.SimpleFunc.setToSimpleFunc_congr_left : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  (T T' : Set α → E →L[ℝ] F),
  (∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T s = T' s) →
    ∀ (f : MeasureTheory.SimpleFunc α E),
      MeasureTheory.Integrable (⇑f) μ →
        MeasureTheory.SimpleFunc.setToSimpleFunc T f = MeasureTheory.SimpleFunc.setToSimpleFunc T' f
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.meromorphic_derivWeierstrassP : ∀ (L : PeriodPair), Meromorphic L.derivWeierstrassP
-- Mathlib.Order.RelIso.Basic
RelIso.copy_eq : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (e : r ≃r s) (f : α → β) (g : β → α) (hf : f = ⇑e)
  (hg : g = ⇑e.symm), e.copy f g hf hg = e
-- Init.Data.Range.Polymorphic.Internal.SignedBitVec
_private.Init.Data.Range.Polymorphic.Internal.SignedBitVec.0.BitVec.Signed.toInt_eq_ofNat_toNat_rotate_sub : ∀ {n : ℕ} {x : BitVec n}, n > 0 → x.toInt = ↑(BitVec.Signed.rotate✝ x).toNat - ↑(BitVec.Signed.intMinSealed✝ n).toNat
-- Mathlib.CategoryTheory.LocallyCartesianClosed.Over
CategoryTheory.ChosenPullbacksAlong.Over.tensorUnit_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.ChosenPullbacks C] {X : C},
  (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over X)).hom = CategoryTheory.CategoryStruct.id X
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
NNReal.sqrt_eq_rpow : ∀ (x : NNReal), NNReal.sqrt x = x ^ (1 / 2)
-- Mathlib.Algebra.Lie.Prod
/-- The right injection into a product is a Lie algebra map.  -/
LieHom.inr : (R : Type u_1) →
  (L₁ : Type u_2) →
    (L₂ : Type u_3) →
      [inst : CommRing R] →
        [inst_1 : LieRing L₁] →
          [inst_2 : LieAlgebra R L₁] → [inst_3 : LieRing L₂] → [inst_4 : LieAlgebra R L₂] → L₂ →ₗ⁅R⁆ L₁ × L₂
-- Aesop.Search.Expansion
Aesop.SafeRulesResult.failed : Array Aesop.PostponedSafeRule → Aesop.SafeRulesResult
-- Mathlib.Algebra.Group.Defs
npowRec.eq_def : ∀ {M : Type u_1} [inst : One M] [inst_1 : Mul M] (x : ℕ) (x_1 : M),
  npowRec x x_1 =
    match x, x_1 with
    | 0, x => 1
    | n.succ, a => npowRec n a * a
-- Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
CategoryTheory.MorphismProperty.Under.pushoutCongr_hom_app_left_fst_assoc : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] {P Q : CategoryTheory.MorphismProperty T}
  [inst_1 : Q.IsMultiplicative] {X Y : T} {f : X ⟶ Y} [inst_2 : P.HasPushoutsAlong f] {g : X ⟶ Y}
  [inst_3 : P.IsStableUnderCobaseChangeAlong f] [inst_4 : Q.IsStableUnderCobaseChange] (h : f = g) (A : P.Under Q X)
  {Z : T} (h_1 : ((CategoryTheory.MorphismProperty.Under.pushout P Q g).obj A).right ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl A.hom f)
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.MorphismProperty.Under.pushoutCongr h).hom.app A).right
        h_1) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl A.hom g) h_1
-- Mathlib.Combinatorics.SimpleGraph.AdjMatrix
/-- An isomorphism of the graph of a reindexing of an adjacency matrix to the graph of the
adjacency matrix itself  -/
Matrix.IsAdjMatrix.toGraphReindexIso : {α : Type u_1} →
  {V : Type u_2} →
    {W : Type u_3} →
      (A : Matrix V V α) →
        [inst : MulZeroOneClass α] →
          [inst_1 : Nontrivial α] → (h : A.IsAdjMatrix) → (f : V ≃ W) → ⋯.toGraph ≃g h.toGraph
-- Mathlib.Algebra.Ring.Subsemiring.Defs
Subsemiring.one_mem_toNonUnitalSubsemiring : ∀ {R : Type u} [inst : NonAssocSemiring R] (S : Subsemiring R), 1 ∈ S.toNonUnitalSubsemiring
-- Mathlib.RingTheory.Coalgebra.Basic
TensorProduct.congr.eq_1 : ∀ {R : Type u_1} {R₂ : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7}
  {N : Type u_8} {M₂ : Type u_12} {N₂ : Type u_14} [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid N]
  [inst_4 : AddCommMonoid M₂] [inst_5 : AddCommMonoid N₂] [inst_6 : Module R M] [inst_7 : Module R N]
  [inst_8 : Module R₂ M₂] [inst_9 : Module R₂ N₂] {σ₂₁ : R₂ →+* R} [inst_10 : RingHomInvPair σ₁₂ σ₂₁]
  [inst_11 : RingHomInvPair σ₂₁ σ₁₂] (f : M ≃ₛₗ[σ₁₂] M₂) (g : N ≃ₛₗ[σ₁₂] N₂),
  TensorProduct.congr f g = LinearEquiv.ofLinearMap (TensorProduct.map ↑f ↑g) (TensorProduct.map ↑f.symm ↑g.symm) ⋯ ⋯
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Algebra.mem_sup_right : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] {S T : Subalgebra R A}
  {x : A}, x ∈ T → x ∈ S ⊔ T
-- Mathlib.MeasureTheory.OuterMeasure.Operations
/-- **Alias** of `smul_apply`. -/
MeasureTheory.OuterMeasure.smul_apply : ∀ {M : Type u_1} {F : Type u_2} {α : outParam (Type u_3)} {β : outParam (Type u_4)} {inst : FunLike F α β}
  {inst_1 : SMul M β} {inst_2 : SMul M F} [self : IsSMulApply M F α β] (f : F) (r : M) (x : α), (r • f) x = r • f x
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.L1.integral_eq_integral : ∀ {α : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} [inst_2 : CompleteSpace E] (f : ↥(MeasureTheory.Lp E 1 μ)),
  MeasureTheory.L1.integral f = ∫ (a : α), ↑↑f a ∂μ
-- Mathlib.AlgebraicTopology.DoldKan.NCompGamma
AlgebraicTopology.DoldKan.identity_N₂_objectwise : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasFiniteCoproducts C]
  (P : CategoryTheory.Idempotents.Karoubi (CategoryTheory.SimplicialObject C)),
  CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.N₂Γ₂.inv.app (AlgebraicTopology.DoldKan.N₂.obj P))
      (AlgebraicTopology.DoldKan.N₂.map (AlgebraicTopology.DoldKan.Γ₂N₂.natTrans.app P)) =
    CategoryTheory.CategoryStruct.id (AlgebraicTopology.DoldKan.N₂.obj P)
-- Mathlib.Computability.TuringMachine.Computable
Turing.inhabitedEvalsToInTime : Inhabited (StateTransition.EvalsToInTime (fun x => some PUnit.unit) PUnit.unit (some PUnit.unit) 0)
-- Mathlib.RingTheory.LocalRing.Pullback
AlgHom.surjective_pullbackFst_of_surjective : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [inst : CommSemiring R] [inst_1 : Ring A]
  [inst_2 : Algebra R A] [inst_3 : Ring B] [inst_4 : Algebra R B] [inst_5 : Semiring C] [inst_6 : Algebra R C]
  (f : A →ₐ[R] C) (g : B →ₐ[R] C), Function.Surjective ⇑g → Function.Surjective ⇑(f.pullbackFst g)
-- Mathlib.CategoryTheory.Adjunction.PartialAdjoint
CategoryTheory.Functor.partialLeftAdjointHomEquiv_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor D C) {X : F.PartialLeftAdjointSource} {Y Y' : D} (f : F.partialLeftAdjointObj X ⟶ Y)
  (g : Y ⟶ Y'),
  F.partialLeftAdjointHomEquiv (CategoryTheory.CategoryStruct.comp f g) =
    CategoryTheory.CategoryStruct.comp (F.partialLeftAdjointHomEquiv f) (F.map g)
-- Mathlib.Algebra.Homology.BifunctorShift
CategoryTheory.Functor.instCommShiftCochainComplexIntObjFlipMap₂CochainComplex : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {D : 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} D] →
            [inst_3 : CategoryTheory.Preadditive C₁] →
              [inst_4 : CategoryTheory.Preadditive C₂] →
                [inst_5 : CategoryTheory.Preadditive D] →
                  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) →
                    [inst_6 : F.Additive] →
                      [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).Additive] →
                        [inst_8 : ∀ (K₁ : CochainComplex C₁ ℤ) (K₂ : CochainComplex C₂ ℤ), K₁.HasMapBifunctor K₂ F] →
                          (K₂ : CochainComplex C₂ ℤ) → (F.map₂CochainComplex.flip.obj K₂).CommShift ℤ
-- Batteries.Data.List.ArrayMap
/-- This function is provided as a more efficient runtime alternative to `(l.map f).toArray`.
(It avoids the intermediate memory allocation of creating an intermediate list first.)
For verification purposes, we immediately simplify it to that form.
 -/
List.toArrayMap : {α : Type u} → {β : Type v} → List α → (α → β) → Array β
-- Init.Data.SInt.Lemmas
Int16.toInt8_neg : ∀ (x : Int16), (-x).toInt8 = -x.toInt8
-- Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
AffineBasis.finite : ∀ {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [inst : AddCommGroup V] [inst_1 : AddTorsor V P]
  [inst_2 : DivisionRing k] [inst_3 : Module k V] [FiniteDimensional k V] (b : AffineBasis ι k P), Finite ι
-- Mathlib.CategoryTheory.Monad.Products
CategoryTheory.prodComonad_ε_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : C) [inst_1 : CategoryTheory.Limits.HasBinaryProducts C]
  (x : C), (CategoryTheory.prodComonad X).ε.app x = CategoryTheory.Limits.prod.snd
-- Init.Omega.Int
Lean.Omega.Int.ofNat_lt_of_lt : ∀ {x y : ℕ}, x < y → ↑x < ↑y
-- Mathlib.Algebra.Group.Subgroup.MulOpposite
AddSubgroup.op_inj : ∀ {G : Type u_2} [inst : AddGroup G] {S T : AddSubgroup G}, S.op = T.op ↔ S = T
-- Init.Data.Range.Polymorphic.RangeIterator
Std.Rxc.Iterator.instLawfulDeterministicIterator : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : LE α] [inst_2 : DecidableLE α],
  Std.LawfulDeterministicIterator (Std.Rxc.Iterator α) Id
-- Mathlib.LinearAlgebra.Matrix.Kronecker
/-- `Matrix.kronecker` as a bilinear map.  -/
Matrix.kroneckerTMulBilinear : (R : Type u_1) →
  (S : Type u_2) →
    {α : Type u_3} →
      {β : Type u_5} →
        {l : Type u_9} →
          {m : Type u_10} →
            {n : Type u_11} →
              {p : Type u_12} →
                [inst : CommSemiring R] →
                  [inst_1 : AddCommMonoid α] →
                    [inst_2 : AddCommMonoid β] →
                      [inst_3 : Module R α] →
                        [inst_4 : Module R β] →
                          [inst_5 : Semiring S] →
                            [inst_6 : Module S α] →
                              [inst_7 : SMulCommClass R S α] →
                                Matrix l m α →ₗ[S] Matrix n p β →ₗ[R] Matrix (l × n) (m × p) (TensorProduct R α β)
-- Lean.Language.Lean.Types
Lean.Language.Lean.CommandParsedSnapshot.mk.inj : ∀ {toSnapshot : Lean.Language.Snapshot} {stx : Lean.Syntax} {parserState : Lean.Parser.ModuleParserState}
  {elabSnap : Lean.Language.Lean.CommandElaboratingSnapshot}
  {nextCmdSnap? : Option (Lean.Language.SnapshotTask Lean.Language.Lean.CommandParsedSnapshot)}
  {toSnapshot_1 : Lean.Language.Snapshot} {stx_1 : Lean.Syntax} {parserState_1 : Lean.Parser.ModuleParserState}
  {elabSnap_1 : Lean.Language.Lean.CommandElaboratingSnapshot}
  {nextCmdSnap?_1 : Option (Lean.Language.SnapshotTask Lean.Language.Lean.CommandParsedSnapshot)},
  { toSnapshot := toSnapshot, stx := stx, parserState := parserState, elabSnap := elabSnap,
        nextCmdSnap? := nextCmdSnap? } =
      { toSnapshot := toSnapshot_1, stx := stx_1, parserState := parserState_1, elabSnap := elabSnap_1,
        nextCmdSnap? := nextCmdSnap?_1 } →
    toSnapshot = toSnapshot_1 ∧
      stx = stx_1 ∧ parserState = parserState_1 ∧ elabSnap = elabSnap_1 ∧ nextCmdSnap? = nextCmdSnap?_1
-- Init.Prelude
/-- A way to interpret a fully-polymorphic function in `m` into `n`. Such a function can be thought of
as one that may change the effects in `m`, but can't do so based on specific values that are
provided.

This is the reflexive, transitive closure of `MonadFunctor`. It automatically chains together
`MonadFunctor` instances as needed. Clients of `MonadFunctor` should typically use `MonadFunctorT`,
but new instances should be defined for `MonadFunctor`.
 -/
MonadFunctorT : (Type u → Type v) → (Type u → Type w) → Type (max (max (u + 1) v) w)
-- Mathlib.Data.Finsupp.Interval
Finsupp.rangeIcc_support : ∀ {ι : Type u_1} {α : Type u_2} [inst : Zero α] [inst_1 : PartialOrder α] [inst_2 : LocallyFiniteOrder α]
  [inst_3 : DecidableEq ι] (f g : ι →₀ α), (f.rangeIcc g).support = f.support ∪ g.support
-- Mathlib.RingTheory.Polynomial.Subring
Polynomial.monic_toSubring : ∀ {R : Type u_1} [inst : Ring R] (p : Polynomial R) (T : Subring R) (hp : ↑p.coeffs ⊆ ↑T),
  (p.toSubring T hp).Monic ↔ p.Monic
-- Init.Data.UInt.Bitwise
USize.neg_one_xor : ∀ {a : USize}, -1 ^^^ a = ~~~a
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.size_filter_key_eq_size_iff : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] {f : α → Bool},
  m.WF → ((Std.DHashMap.Raw.filter (fun k x => f k) m).size = m.size ↔ ∀ (k : α) (h : k ∈ m), f (m.getKey k h) = true)
-- Init.Data.String.Iterator
/-- An iterator over the characters (Unicode code points) in a `String`. Typically created by
`String.iter`.

This is a no-longer-supported legacy API that will be removed in a future release. You should use
`String.Pos` instead, which is similar, but safer. To iterate over a string `s`, start with
`p : s.startPos`, advance it using `p.next`, access the current character using `p.get` and
check if the position is at the end using `p = s.endPos` or `p.IsAtEnd`.

String iterators pair a string with a valid byte index. This allows efficient character-by-character
processing of strings while avoiding the need to manually ensure that byte indices are used with the
correct strings.

An iterator is *valid* if the position `i` is *valid* for the string `s`, meaning `0 ≤ i ≤ s.rawEndPos`
and `i` lies on a UTF8 byte boundary. If `i = s.rawEndPos`, the iterator is at the end of the string.

Most operations on iterators return unspecified values if the iterator is not valid. The functions
in the `String.Iterator` API rule out the creation of invalid iterators, with two exceptions:
- `Iterator.next iter` is invalid if `iter` is already at the end of the string (`iter.atEnd` is
  `true`), and
- `Iterator.forward iter n`/`Iterator.nextn iter n` is invalid if `n` is strictly greater than the
  number of remaining characters.
 -/
String.Legacy.Iterator : Type
-- Mathlib.RingTheory.MvPowerSeries.Expand
MvPowerSeries.expand_subst : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [inst : CommRing R] (p : ℕ) (hp : p ≠ 0) {f : σ → MvPowerSeries τ R},
  MvPowerSeries.HasSubst f →
    ∀ {φ : MvPowerSeries σ R},
      (MvPowerSeries.expand p hp) (MvPowerSeries.subst f φ) =
        MvPowerSeries.subst (fun i => (MvPowerSeries.expand p hp) (f i)) φ
-- Mathlib.Data.Nat.Order.Lemmas
Nat.Subtype.coe_bot : ∀ {s : Set ℕ} [inst : DecidablePred fun x => x ∈ s] [h : Nonempty ↑s], ↑⊥ = Nat.find ⋯
-- Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv
CliffordAlgebra.toEven_comp_ofEven : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (Q : QuadraticForm R M),
  (CliffordAlgebra.toEven Q).comp (CliffordAlgebra.ofEven Q) =
    AlgHom.id R ↥(CliffordAlgebra.even (CliffordAlgebra.EquivEven.Q' Q))
-- Mathlib.Analysis.Normed.Module.MStructure
IsLprojection.mul : ∀ {X : Type u_1} [inst : NormedAddCommGroup X] {M : Type u_2} [inst_1 : Ring M] [inst_2 : Module M X] [FaithfulSMul M X]
  {P Q : M}, IsLprojection X P → IsLprojection X Q → IsLprojection X (P * Q)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getD_insert_self : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α],
  m.WF → ∀ {a : α} {fallback b : β a}, (m.insert a b).getD a fallback = b
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
/-- The embedding of the value group-with-zero into the nonnegative reals.  -/
ValuativeRel.RankLeOneStruct.emb : {R : Type u_1} →
  [inst : Semiring R] →
    [inst_1 : ValuativeRel R] → ValuativeRel.RankLeOneStruct R → ValuativeRel.ValueGroupWithZero R →*₀ NNReal
-- Lean.Data.Lsp.CodeActions
Lean.Lsp.instToJsonCodeActionParams : Lean.ToJson Lean.Lsp.CodeActionParams
-- Mathlib.Algebra.BigOperators.Associated
_private.Mathlib.Algebra.BigOperators.Associated.0.«term_~ᵤ_» : Lean.TrailingParserDescr
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- The natural isomorphism between `pair X Y ⋙ F` and `pair (F.obj X) (F.obj Y)`.  -/
CategoryTheory.Limits.pairComp : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u₁} →
      [inst_1 : CategoryTheory.Category.{v₁, u₁} D] →
        (X Y : C) →
          (F : CategoryTheory.Functor C D) →
            (CategoryTheory.Limits.pair X Y).comp F ≅ CategoryTheory.Limits.pair (F.obj X) (F.obj Y)
-- Mathlib.CategoryTheory.Limits.Preserves.Presheaf
CategoryTheory.Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.flipFunctorToInterchange_inv_app_app_hom_apply : ∀ {C : Type u} [inst : CategoryTheory.SmallCategory C] (A : CategoryTheory.Functor Cᵒᵖ (Type u)) {J : Type}
  [inst_1 : CategoryTheory.SmallCategory J] (K : CategoryTheory.Functor J Cᵒᵖ)
  (X : CategoryTheory.CostructuredArrow CategoryTheory.yoneda A) (X_1 : J)
  (a :
    ((CategoryTheory.Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.functorToInterchange A
                K).flip.obj
          X).obj
      X_1),
  (CategoryTheory.ConcreteCategory.hom
        (((CategoryTheory.Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.flipFunctorToInterchange A
                    K).inv.app
              X).app
          X_1))
      a =
    a
-- Mathlib.Probability.Distributions.Gaussian.Real
ProbabilityTheory.variance_continuousLinearMap_gaussianReal : ∀ {μ : ℝ} {v : NNReal} (L : ℝ →L[ℝ] ℝ),
  ProbabilityTheory.variance (⇑L) (ProbabilityTheory.gaussianReal μ v) = ↑(L 1 ^ 2).toNNReal * ↑v
-- Mathlib.Order.Bounds.Basic
exists_lub_Iio : ∀ {γ : Type u_3} [inst : LinearOrder γ] (i : γ), ∃ j, IsLUB (Set.Iio i) j
-- Mathlib.LinearAlgebra.FreeModule.Finite.Basic
/-- If a free module is finite, then the arbitrary basis is finite.  -/
Module.Free.ChooseBasisIndex.fintype : (R : Type u) →
  (M : Type v) →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] →
          [inst_3 : Module.Free R M] → [Module.Finite R M] → Fintype (Module.Free.ChooseBasisIndex R M)
-- Init.Data.Float.Float
/-- Computes the cosine of a floating-point number in radians.

This function does not reduce in the kernel. It is implemented in compiled code by the C function
`cos`.
 -/
Float.cos : Float → Float