mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Elab.MutualInductive
Lean.Elab.Command.elabInductive : Lean.Elab.Modifiers → Lean.Syntax → Lean.Elab.Command.CommandElabM Unit
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
SchwartzMap.instNSMul : {E : Type u_5} →
  {F : Type u_6} →
    [inst : NormedAddCommGroup E] →
      [inst_1 : NormedSpace ℝ E] →
        [inst_2 : NormedAddCommGroup F] → [inst_3 : NormedSpace ℝ F] → SMul ℕ (SchwartzMap E F)
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.mem_prod : ∀ {N : Type u_2} [inst : AddZeroClass N] {M : Type u_5} [inst_1 : AddZeroClass M] {s : AddSubmonoid M}
  {t : AddSubmonoid N} {p : M × N}, p ∈ s.prod t ↔ p.1 ∈ s ∧ p.2 ∈ t
-- Std.Tactic.BVDecide.LRAT.Actions
Std.Tactic.BVDecide.LRAT.instReprAction.repr : {β : Type u_1} → {α : Type u_2} → [Repr β] → [Repr α] → Std.Tactic.BVDecide.LRAT.Action β α → ℕ → Std.Format
-- Lean.Elab.PreDefinition.WF.GuessLex
Lean.Elab.WF.GuessLex.SavedLocalContext.savedLocalInstances : Lean.Elab.WF.GuessLex.SavedLocalContext → Lean.LocalInstances
-- Mathlib.Geometry.Diffeology.Basic
Diffeology.isOpen_iff_preimages_plots : ∀ {X : Type u_1} [inst : DiffeologicalSpace X] {u : Set X},
  IsOpen u ↔ ∀ (n : ℕ) (p : EuclideanSpace ℝ (Fin n) → X), Diffeology.IsPlot p → IsOpen (p ⁻¹' u)
-- Mathlib.Topology.Homotopy.Basic
ContinuousMap.HomotopyRel.fst_eq_snd : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f₀ f₁ : C(X, Y)} {S : Set X}
  (F : f₀.HomotopyRel f₁ S) {x : X}, x ∈ S → f₀ x = f₁ x
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.toList_map : ∀ {α β β' : Type w} {m : Type w → Type w'} [inst : Monad m] [LawfulMonad m] [inst_2 : Std.Iterator α m β]
  [Std.Iterators.Finite α m] {f : β → β'} (it : Std.IterM m β),
  (Std.IterM.map f it).toList = (fun x => List.map f x) <$> it.toList
-- Mathlib.Analysis.Convex.Function
ConvexOn.congr : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommMonoid β] [inst_4 : PartialOrder β] [inst_5 : SMul 𝕜 E] [inst_6 : SMul 𝕜 β] {s : Set E}
  {f g : E → β}, ConvexOn 𝕜 s f → Set.EqOn f g s → ConvexOn 𝕜 s g
-- Mathlib.Analysis.Normed.Ring.Basic
/-- A ring homomorphism from a `Ring R` to a `SeminormedRing S` which induces the norm structure
`SeminormedRing.induced` makes `R` satisfy `‖(1 : R)‖ = 1` whenever `‖(1 : S)‖ = 1`.  -/
NormMulClass.induced : ∀ {F : Type u_8} (R : Type u_9) (S : Type u_10) [inst : Ring R] [inst_1 : SeminormedRing S] [NormMulClass S]
  [inst_3 : FunLike F R S] [inst_4 : RingHomClass F R S] (f : F), NormMulClass R
-- Mathlib.Analysis.Convex.SimplicialComplex.Basic
Geometry.SimplicialComplex.nonempty_of_mem_faces : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Ring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] {K : Geometry.SimplicialComplex 𝕜 E} {s : Finset E}, s ∈ K.faces → s.Nonempty
-- Mathlib.CategoryTheory.Monoidal.End
CategoryTheory.left_unitality_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {M : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} M]
  [inst_2 : CategoryTheory.MonoidalCategory M] (F : CategoryTheory.Functor M (CategoryTheory.Functor C C)) (n : M)
  (X : C) [inst_3 : F.LaxMonoidal],
  CategoryTheory.CategoryStruct.comp ((F.obj n).map ((CategoryTheory.Functor.LaxMonoidal.ε F).app X))
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.Functor.LaxMonoidal.μ F (CategoryTheory.MonoidalCategoryStruct.tensorUnit M) n).app X)
        ((F.map (CategoryTheory.MonoidalCategoryStruct.leftUnitor n).hom).app X)) =
    CategoryTheory.CategoryStruct.id
      ((F.obj n).obj ((CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Functor C C)).obj X))
-- Init.Sym.Simp.SimprocDSL
/-- Maximum number of simplification steps.  -/
Lean.Parser.Command.symSimpFieldMaxSteps : Lean.ParserDescr
-- Mathlib.Analysis.Normed.Group.Basic
norm_prod_le_of_le : ∀ {ι : Type u_3} {E : Type u_5} [inst : SeminormedCommGroup E] (s : Finset ι) {f : ι → E} {n : ι → ℝ},
  (∀ b ∈ s, ‖f b‖ ≤ n b) → ‖∏ b ∈ s, f b‖ ≤ ∑ b ∈ s, n b
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
/-- If `f` is a continuous multilinear map on `E`
and `m` is an element of `∀ i, E i` such that one of the `m i` has norm `0`,
then `f m` has norm `0`.

Note that we cannot drop the continuity assumption because `f (m : Unit → E) = f (m ())`,
where the domain has zero norm and the codomain has a nonzero norm
does not satisfy this condition.  -/
MultilinearMap.norm_map_coord_zero : ∀ {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)]
  [inst_3 : SeminormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] (f : MultilinearMap 𝕜 E G),
  Continuous ⇑f → ∀ {m : (i : ι) → E i} {i : ι}, ‖m i‖ = 0 → ‖f m‖ = 0
-- Init.Data.List.Pairwise
List.nodup_nil : ∀ {α : Type u_1}, [].Nodup
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.Lp.edist_toLp_toLp : ∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] (f g : α → E) (hf : MeasureTheory.MemLp f p μ) (hg : MeasureTheory.MemLp g p μ),
  edist (MeasureTheory.MemLp.toLp f hf) (MeasureTheory.MemLp.toLp g hg) = MeasureTheory.eLpNorm (f - g) p μ
-- Mathlib.NumberTheory.RamificationInertia.Ramification
Ideal.ramificationIdx'_le_ramificationIdx' : ∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal R) (P : Ideal S)
  {T : Type u_2} [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [IsScalarTower R S T]
  (Q : Ideal T),
  p = Ideal.comap (algebraMap R S) P → p.ramificationIdx' Q ≠ 0 → P.ramificationIdx' Q ≤ p.ramificationIdx' Q
-- Mathlib.Topology.MetricSpace.Holder
holderOnWith_singleton : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] (C r : NNReal) (f : X → Y)
  (x : X), HolderOnWith C r f {x}
-- Mathlib.GroupTheory.Coxeter.Length
CoxeterSystem.exists_isReduced : ∀ {B : Type u_1} {W : Type u_2} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (w : W),
  ∃ ω, cs.IsReduced ω ∧ w = cs.wordProd ω
-- Init.Data.Int.Linear
_private.Init.Data.Int.Linear.0.Int.Internal.Linear.Poly.denote.match_1.eq_1 : ∀ (motive : Int.Internal.Linear.Poly → Sort u_1) (k : ℤ) (h_1 : (k : ℤ) → motive (Int.Internal.Linear.Poly.num k))
  (h_2 :
    (k : ℤ) →
      (v : Int.Internal.Linear.Var) → (p : Int.Internal.Linear.Poly) → motive (Int.Internal.Linear.Poly.add k v p)),
  (match Int.Internal.Linear.Poly.num k with
    | Int.Internal.Linear.Poly.num k => h_1 k
    | Int.Internal.Linear.Poly.add k v p => h_2 k v p) =
    h_1 k
-- Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
/-- `spanningSetsIndex μ x` is the least `n : ℕ` such that `x ∈ spanningSets μ n`.  -/
MeasureTheory.spanningSetsIndex : {α : Type u_1} → {m0 : MeasurableSpace α} → (μ : MeasureTheory.Measure α) → [MeasureTheory.SigmaFinite μ] → α → ℕ
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Functor.mapMonFunctor_map_app_hom : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (D : Type u₂)
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  {X Y : CategoryTheory.LaxMonoidalFunctor C D} (α : X ⟶ Y) (A : CategoryTheory.Mon C),
  (((CategoryTheory.Functor.mapMonFunctor C D).map α).app A).hom = α.hom.app A.X
-- Mathlib.Data.Finset.Image
Finset.image_subset_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] {f : α → β} {s : Finset α} {t : Finset β},
  Finset.image f s ⊆ t ↔ ∀ x ∈ s, f x ∈ t
-- Mathlib.Topology.ContinuousMap.Units
ContinuousMap.addUnitsLift_symm_apply_apply_neg' : ∀ {X : Type u_1} {M : Type u_2} [inst : TopologicalSpace X] [inst_1 : AddMonoid M] [inst_2 : TopologicalSpace M]
  [inst_3 : ContinuousAdd M] (f : AddUnits C(X, M)) (x : X), ↑(-(ContinuousMap.addUnitsLift.symm f) x) = ↑(-f) x
-- Mathlib.RingTheory.Flat.Equalizer
LinearMap.tensorEqLocusEquiv_apply : ∀ {R : Type u_1} (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (M : Type u_3)
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : Module S M] [inst_6 : IsScalarTower R S M] {N : Type u_4}
  {P : Type u_5} [inst_7 : AddCommGroup N] [inst_8 : AddCommGroup P] [inst_9 : Module R N] [inst_10 : Module R P]
  (f g : N →ₗ[R] P) [inst_11 : Module.Flat R M] (x : TensorProduct R M ↥(f.eqLocus g)),
  (LinearMap.tensorEqLocusEquiv S M f g) x = (LinearMap.tensorEqLocus S M f g) x
-- Init.Data.Slice.List.Basic
instSliceableListNatListSlice_1 : {α : Type u} → Std.Rco.Sliceable (List α) ℕ (ListSlice α)
-- Mathlib.Data.Nat.Bits
Nat.shiftLeft'_sub : ∀ (b : Bool) (m : ℕ) {n k : ℕ}, k ≤ n → Nat.shiftLeft' b m (n - k) = Nat.shiftLeft' b m n >>> k
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Pullbacks
CategoryTheory.Limits.cospanHomMk.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F G : CategoryTheory.Functor CategoryTheory.Limits.WalkingCospan C}
  (z z_1 : F.obj CategoryTheory.Limits.WalkingCospan.one ⟶ G.obj CategoryTheory.Limits.WalkingCospan.one)
  (e_z : z = z_1)
  (l l_1 : F.obj CategoryTheory.Limits.WalkingCospan.left ⟶ G.obj CategoryTheory.Limits.WalkingCospan.left)
  (e_l : l = l_1)
  (r r_1 : F.obj CategoryTheory.Limits.WalkingCospan.right ⟶ G.obj CategoryTheory.Limits.WalkingCospan.right)
  (e_r : r = r_1)
  (hl :
    CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingCospan.Hom.inl) z =
      CategoryTheory.CategoryStruct.comp l (G.map CategoryTheory.Limits.WalkingCospan.Hom.inl))
  (hr :
    CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingCospan.Hom.inr) z =
      CategoryTheory.CategoryStruct.comp r (G.map CategoryTheory.Limits.WalkingCospan.Hom.inr)),
  CategoryTheory.Limits.cospanHomMk z l r hl hr = CategoryTheory.Limits.cospanHomMk z_1 l_1 r_1 ⋯ ⋯
-- Init.Data.Subtype.Order
Subtype.instMinEqOr : ∀ {α : Type u} [inst : Min α] [inst_1 : Std.MinEqOr α] {P : α → Prop}, Std.MinEqOr (Subtype P)
-- Mathlib.Order.BooleanGenerators
/-- A lattice generated by Boolean generators is a distributive lattice.  -/
IsCompactlyGenerated.BooleanGenerators.distribLatticeOfSSupEqTop : {α : Type u_1} →
  [inst : CompleteLattice α] →
    {S : Set α} → [IsCompactlyGenerated α] → IsCompactlyGenerated.BooleanGenerators S → sSup S = ⊤ → DistribLattice α
-- Lean.Parser.Syntax
Lean.Parser.Command.notation : Lean.Parser.Parser
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.TakeWhile
_private.Std.Data.Iterators.Lemmas.Combinators.Monadic.TakeWhile.0.Std.IterM.step_takeWhileWithPostcondition.match_3.eq_2 : ∀ {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [inst : Std.Iterator α m β] {it : Std.IterM m β}
  (motive : it.Step → Sort u_3) (it' : Std.IterM m β) (h : it.IsPlausibleStep (Std.IterStep.skip it'))
  (h_1 :
    (it' : Std.IterM m β) →
      (out : β) → (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 : (it' : Std.IterM m β) → (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (h : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩),
  (match ⟨Std.IterStep.skip it', h⟩ with
    | ⟨Std.IterStep.yield it' out, h⟩ => h_1 it' out h
    | ⟨Std.IterStep.skip it', h⟩ => h_2 it' h
    | ⟨Std.IterStep.done, h⟩ => h_3 h) =
    h_2 it' h
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives
CategoryTheory.Abelian.Ext.eq_zero_of_injective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {X I : C} {n : ℕ} [CategoryTheory.Injective I]
  (e : CategoryTheory.Abelian.Ext X I (n + 1)), e = 0
-- Std.Data.TreeMap.Basic
/-- Tries to retrieve the key-value pair with the smallest key that is greater than the given key,
panicking if no such pair exists.
 -/
Std.TreeMap.getEntryGT! : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → [Inhabited (α × β)] → Std.TreeMap α β cmp → α → α × β
-- Mathlib.Algebra.FiniteSupport.Basic
Function.HasFiniteSupport.nsmul : ∀ {α : Type u_1} {M : Type u_3} [inst : AddMonoid M] {f : α → M},
  Function.HasFiniteSupport f → ∀ (n : ℕ), Function.HasFiniteSupport (n • f)
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass
CategoryTheory.ShortComplex.ShortExact.extClass_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact),
  hS.extClass.comp (CategoryTheory.Abelian.Ext.mk₀ S.f) ⋯ = 0
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
deriv_ccosh : ∀ {f : ℂ → ℂ} {x : ℂ}, DifferentiableAt ℂ f x → deriv (fun x => Complex.cosh (f x)) x = Complex.sinh (f x) * deriv f x
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
Commute.cfcAbs_right : ∀ {A : Type u_2} [inst : NonUnitalRing A] [inst_1 : StarRing A] [inst_2 : TopologicalSpace A] [inst_3 : Module ℝ A]
  [inst_4 : SMulCommClass ℝ A A] [inst_5 : IsScalarTower ℝ A A]
  [inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_7 : PartialOrder A]
  [inst_8 : StarOrderedRing A] [inst_9 : NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] {a b : A},
  Commute a b → Commute a (star b) → Commute b (CFC.abs a)
-- Mathlib.Logic.Equiv.Fin.Basic
Equiv.embeddingFinSucc_fst : ∀ {n : ℕ} {ι : Type u_1} (e : Fin (n + 1) ↪ ι), ⇑((Equiv.embeddingFinSucc n ι) e).fst = ⇑e ∘ Fin.succ
-- Mathlib.CategoryTheory.Adjunction.Limits
/-- The functor `Cone.functoriality K G : Cone K ⥤ Cone (K ⋙ G)` is a right adjoint.  -/
CategoryTheory.Adjunction.functorialityAdjunction' : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F : CategoryTheory.Functor C D} →
          {G : CategoryTheory.Functor D C} →
            (adj : F ⊣ G) →
              {J : Type u} →
                [inst_2 : CategoryTheory.Category.{v, u} J] →
                  (K : CategoryTheory.Functor J D) →
                    adj.functorialityLeftAdjoint K ⊣ CategoryTheory.Limits.Cone.functoriality K G
-- Mathlib.Topology.Homotopy.TopCat.Path
/-- a morphism from the unit interval  -/
TopCat.Path.hom : {X : TopCat} → {x y : ↑X} → X.Path x y → (TopCat.I ⟶ X)
-- Mathlib.Analysis.Normed.Module.ContinuousInverse
/-- A continuous linear equivalence has a continuous right inverse.  -/
ContinuousLinearEquiv.hasRightInverse : ∀ {R : Type u_1} [inst : Semiring R] {E : Type u_2} {F : Type u_4} [inst_1 : TopologicalSpace E]
  [inst_2 : AddCommMonoid E] [inst_3 : Module R E] [inst_4 : TopologicalSpace F] [inst_5 : AddCommMonoid F]
  [inst_6 : Module R F] (f : E ≃L[R] F), (↑f).HasRightInverse
-- Init.Prelude
/-- The transitive closure of `MonadEval`.  -/
MonadEvalT : (Type u → Type v) → (Type u → Type w) → Type (max (max (u + 1) v) w)
-- Mathlib.Analysis.InnerProductSpace.Reproducing
RKHS.instPreInnerProductSpaceCoreH₀ : {𝕜 : Type u_1} →
  [inst : RCLike 𝕜] →
    {X : Type u_2} →
      {V : Type u_3} →
        [inst_1 : NormedAddCommGroup V] →
          [inst_2 : InnerProductSpace 𝕜 V] →
            [inst_3 : CompleteSpace V] →
              {K : Matrix X X (V →L[𝕜] V)} → [Fact K.PosSemidef] → PreInnerProductSpace.Core 𝕜 (RKHS.H₀ K)
-- Mathlib.Algebra.GroupWithZero.Action.Pi
Pi.single_smul₀ : ∀ {I : Type u} {f : I → Type v} {g : I → Type u_1} [inst : (i : I) → MonoidWithZero (f i)]
  [inst_1 : (i : I) → AddMonoid (g i)] [inst_2 : (i : I) → DistribMulAction (f i) (g i)] [inst_3 : DecidableEq I]
  (i : I) (r : f i) (x : g i), Pi.single i (r • x) = Pi.single i r • Pi.single i x
-- Lean.Elab.InfoTree.Types
Lean.Elab.InfoTree.node.injEq : ∀ (i : Lean.Elab.Info) (children : Lean.PersistentArray Lean.Elab.InfoTree) (i_1 : Lean.Elab.Info)
  (children_1 : Lean.PersistentArray Lean.Elab.InfoTree),
  (Lean.Elab.InfoTree.node i children = Lean.Elab.InfoTree.node i_1 children_1) = (i = i_1 ∧ children = children_1)
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
TensorProduct.commIsometry_trans_lidIsometry : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E],
  (TensorProduct.commIsometry 𝕜 E 𝕜).trans (TensorProduct.lidIsometry 𝕜 E) = TensorProduct.ridIsometry 𝕜 E
-- Mathlib.Order.Category.LinOrd
/-- The type of morphisms in `LinOrd R`.  -/
LinOrd.Hom : LinOrd → LinOrd → Type u
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
CategoryTheory.MonoidalClosed.curry'_injective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X Y : C}
  [inst_2 : CategoryTheory.Closed X] {f f' : X ⟶ Y},
  CategoryTheory.MonoidalClosed.curry' f = CategoryTheory.MonoidalClosed.curry' f' → f = f'
-- Init.Data.Array.Lemmas
Array.getElem_ofFn : ∀ {n : ℕ} {α : Type u_1} {f : Fin n → α} {i : ℕ} (h : i < (Array.ofFn f).size), (Array.ofFn f)[i] = f ⟨i, ⋯⟩
-- Mathlib.Data.List.Infix
List.map_reverse_inits : ∀ {α : Type u_1} (l : List α), List.map List.reverse l.inits = l.reverse.tails.reverse
-- Mathlib.SetTheory.Ordinal.Enum
Ordinal.id_le_enumOrd : ∀ {s : Set Ordinal.{u}}, ¬BddAbove s → id ≤ Ordinal.enumOrd s
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.HasColimit.isoOfNatIso_inv_desc : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {F G : CategoryTheory.Functor J C} [inst_2 : CategoryTheory.Limits.HasColimit F]
  [inst_3 : CategoryTheory.Limits.HasColimit G] (t : CategoryTheory.Limits.Cocone F) (w : F ≅ G),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.HasColimit.isoOfNatIso w).inv
      (CategoryTheory.Limits.colimit.desc F t) =
    CategoryTheory.Limits.colimit.desc G ((CategoryTheory.Limits.Cocone.precompose w.inv).obj t)
-- Lean.Environment
Lean.ConstantKind.defn.sizeOf_spec : sizeOf Lean.ConstantKind.defn = 1
-- Mathlib.Algebra.Category.Grp.Basic
AddEquiv.toAddGrpIso_hom : ∀ {X Y : AddGrpCat} (e : ↑X ≃+ ↑Y), e.toAddGrpIso.hom = AddGrpCat.ofHom e.toAddMonoidHom
-- Mathlib.Order.Max
NoBotOrder.mk : ∀ {α : Type u_3} [inst : LE α], (∀ (a : α), ∃ b, ¬a ≤ b) → NoBotOrder α
-- Mathlib.Probability.Moments.SubGaussian
/-- **Alias** of `ProbabilityTheory.HasSubgaussianMGF.add_of_hasCondSubgaussianMGF`.

---

If `X` is sub-Gaussian with parameter `cX` with respect to the restriction of `μ` to
a sub-sigma-algebra `m` and `Y` is conditionally sub-Gaussian with parameter `cY` with respect to
`m` and `μ` then `X + Y` is sub-Gaussian with parameter `cX + cY` with respect to `μ`.

`HasSubgaussianMGF X cX (μ.trim hm)` can be obtained from `HasSubgaussianMGF X cX μ` if `X` is
`m`-measurable. See `HasSubgaussianMGF.trim`.  -/
ProbabilityTheory.HasSubgaussianMGF_add_of_HasCondSubgaussianMGF : ∀ {Ω : Type u_1} {m mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} [inst : StandardBorelSpace Ω]
  [inst_1 : MeasureTheory.IsFiniteMeasure μ] {Y : Ω → ℝ} {cX cY : NNReal} (hm : m ≤ mΩ),
  ProbabilityTheory.HasSubgaussianMGF X cX (μ.trim hm) →
    ProbabilityTheory.HasCondSubgaussianMGF m hm Y cY μ → ProbabilityTheory.HasSubgaussianMGF (X + Y) (cX + cY) μ
-- Mathlib.Algebra.Group.Equiv.Opposite
AddEquiv.neg'_symm_apply : ∀ (G : Type u_3) [inst : SubtractionMonoid G], ⇑(AddEquiv.neg' G).symm = Neg.neg ∘ AddOpposite.unop
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
/-- The equivalence between `integerSet K` modulo `torsion K` and `Associates (𝓞 K)⁰`.  -/
NumberField.mixedEmbedding.fundamentalCone.integerSetQuotEquivAssociates : (K : Type u_1) →
  [inst : Field K] →
    [inst_1 : NumberField K] →
      Quotient
          (MulAction.orbitRel ↥(NumberField.Units.torsion K)
            ↑(NumberField.mixedEmbedding.fundamentalCone.integerSet K)) ≃
        Associates ↥(nonZeroDivisors (NumberField.RingOfIntegers K))
-- Mathlib.InformationTheory.KullbackLeibler.DataProcessing
InformationTheory.klDiv_map_of_ac : ∀ {𝓧 : Type u_1} {𝓨 : Type u_2} {m𝓧 : MeasurableSpace 𝓧} {m𝓨 : MeasurableSpace 𝓨} {μ ν : MeasureTheory.Measure 𝓧}
  [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] {g : 𝓧 → 𝓨},
  μ.AbsolutelyContinuous ν →
    Measurable g →
      MeasureTheory.Integrable (MeasureTheory.llr μ ν) μ →
        InformationTheory.klDiv (MeasureTheory.Measure.map g μ) (MeasureTheory.Measure.map g ν) =
          ENNReal.ofReal
            (∫ (x : 𝓧), InformationTheory.klFun (ν[fun x => (μ.rnDeriv ν x).toReal | MeasurableSpace.comap g m𝓨] x) ∂ν)
-- Mathlib.Algebra.LieRinehartAlgebra.Defs
/-- This is `LieRinehartAlgebra.Hom.map_smul_apply'` restated using the coercion to function rather
than `LieRinehartAlgebra.Hom.toLieHom`.  -/
LieRinehartAlgebra.Hom.map_smul_apply : ∀ {R : Type u_1} {A₁ : Type u_2} {L₁ : Type u_3} {A₂ : Type u_4} {L₂ : Type u_5} [inst : CommRing R]
  [inst_1 : CommRing A₁] [inst_2 : LieRing L₁] [inst_3 : Module A₁ L₁] [inst_4 : LieRingModule L₁ A₁]
  [inst_5 : CommRing A₂] [inst_6 : LieRing L₂] [inst_7 : Module A₂ L₂] [inst_8 : LieRingModule L₂ A₂]
  [inst_9 : Algebra R A₁] [inst_10 : LieAlgebra R L₁] [inst_11 : Algebra R A₂] [inst_12 : LieAlgebra R L₂]
  {σ₁₂ : A₁ →ₐ[R] A₂} (f : LieRinehartAlgebra.Hom σ₁₂ L₁ L₂) (a : A₁) (x : L₁),
  f.toLieHom (a • x) = σ₁₂ a • f.toLieHom x
-- Mathlib.Order.Preorder.Chain
Flag.mk.injEq : ∀ {α : Type u_4} [inst : LE α] (carrier : Set α) (Chain' : IsChain (fun x1 x2 => x1 ≤ x2) carrier)
  (max_chain' : ∀ ⦃s : Set α⦄, IsChain (fun x1 x2 => x1 ≤ x2) s → carrier ⊆ s → carrier = s) (carrier_1 : Set α)
  (Chain'_1 : IsChain (fun x1 x2 => x1 ≤ x2) carrier_1)
  (max_chain'_1 : ∀ ⦃s : Set α⦄, IsChain (fun x1 x2 => x1 ≤ x2) s → carrier_1 ⊆ s → carrier_1 = s),
  ({ carrier := carrier, Chain' := Chain', max_chain' := max_chain' } =
      { carrier := carrier_1, Chain' := Chain'_1, max_chain' := max_chain'_1 }) =
    (carrier = carrier_1)
-- Mathlib.GroupTheory.Coxeter.Matrix
CoxeterMatrix.ext_iff : ∀ {B : Type u_1} {x y : CoxeterMatrix B}, x = y ↔ x.M = y.M
-- Mathlib.Analysis.Normed.Module.Basic
SubmoduleClass.toNormedSpace : {S : Type u_6} →
  {𝕜 : Type u_7} →
    {R : Type u_8} →
      {E : Type u_9} →
        [inst : SMul 𝕜 R] →
          [inst_1 : NormedField 𝕜] →
            [inst_2 : Ring R] →
              [inst_3 : SeminormedAddCommGroup E] →
                [inst_4 : NormedSpace 𝕜 E] →
                  [inst_5 : Module R E] →
                    [IsScalarTower 𝕜 R E] →
                      [inst : SetLike S E] →
                        [inst_6 : AddSubgroupClass S E] → [SMulMemClass S R E] → (s : S) → NormedSpace 𝕜 ↥s
-- Std.Time.Zoned
/-- Gets the current `DateTime` using the identifier of a time zone.
 -/
Std.Time.DateTime.nowAt : String → IO Std.Time.DateTime
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
le_csSup_iff : ∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {s : Set α} {a : α},
  BddAbove s → s.Nonempty → (a ≤ sSup s ↔ ∀ b ∈ upperBounds s, a ≤ b)
-- Mathlib.RingTheory.Coprime.Basic
IsCoprime.abs_right_iff : ∀ {R : Type u} [inst : CommRing R] [inst_1 : LinearOrder R] [AddLeftMono R] (x y : R), IsCoprime x |y| ↔ IsCoprime x y
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey?_inter_of_not_mem_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α},
  k ∉ t₁ → (t₁ ∩ t₂).getKey? k = none
-- Mathlib.Analysis.AbsoluteValue.Equivalence
AbsoluteValue.IsEquiv.one_lt_iff : ∀ {R : Type u_1} [inst : Semiring R] {S : Type u_2} [inst_1 : Semiring S] [inst_2 : PartialOrder S]
  {v w : AbsoluteValue R S} [IsDomain S] [Nontrivial R], v.IsEquiv w → ∀ {x : R}, 1 < v x ↔ 1 < w x
-- Mathlib.SetTheory.Ordinal.Arithmetic
/-- **Alias** of `Ordinal.natCast_lt_omega0`. -/
Ordinal.nat_lt_omega0 : ∀ (n : ℕ), ↑n < Ordinal.omega0