mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.MonObj.one_mul_hom_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {M : C}
  [inst_2 : CategoryTheory.MonObj M] {Z : C} (f : Z ⟶ M) {Z_1 : C} (h : M ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonObj.one f)
      (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor Z).hom
      (CategoryTheory.CategoryStruct.comp f h)
-- Mathlib.Data.Int.Interval
Finset.Ico_succ_succ : ∀ (m n : ℕ), Finset.Ico (-(↑m + 1)) (↑n + 1) = Finset.Ico (-↑m) ↑n ∪ {-(↑m + 1), ↑n}
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.maxKeyD_erase!_eq_of_not_compare_maxKeyD_eq : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF →
    ∀ {k fallback : α},
      (Std.DTreeMap.Internal.Impl.erase! k t).isEmpty = false →
        ¬compare k (t.maxKeyD fallback) = Ordering.eq →
          (Std.DTreeMap.Internal.Impl.erase! k t).maxKeyD fallback = t.maxKeyD fallback
-- Mathlib.Algebra.Lie.Solvable
LieAlgebra.ofAbelianIsSolvable : ∀ (L : Type v) [inst : LieRing L] [IsLieAbelian L], LieAlgebra.IsSolvable L
-- Init.Data.SInt.Lemmas
UInt64.toInt64_ofNat : ∀ {n : ℕ}, (OfNat.ofNat n).toInt64 = OfNat.ofNat n
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.unop_inv_rightUnitor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X : Cᵒᵖ),
  (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv.unop =
    (CategoryTheory.MonoidalCategoryStruct.rightUnitor (Opposite.unop X)).hom
-- Std.Data.HashSet.Raw
Std.HashSet.Raw.WF.erase : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashSet.Raw α} {a : α}, m.WF → (m.erase a).WF
-- Mathlib.Order.LiminfLimsup
Filter.liminf_top_eq_ciInf : ∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLattice α] {u : β → α} [Nonempty β],
  BddBelow (Set.range u) → Filter.liminf u ⊤ = ⨅ i, u i
-- Mathlib.LinearAlgebra.BilinearForm.Properties
/-- A symmetric bilinear form is characterized by the values it takes on the diagonal.  -/
LinearMap.BilinForm.ext_of_isSymm : ∀ {M : Type u_2} [inst : AddCommMonoid M] {R : Type u_8} [inst_1 : Field R] [NeZero 2] [inst_3 : Module R M]
  {B C : LinearMap.BilinForm R M}, B.IsSymm → C.IsSymm → (∀ (x : M), (B x) x = (C x) x) → B = C
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FlatMap
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.FlatMap.0.Std.IterM.flatMapAfterM.eq_1 : ∀ {α β α₂ γ : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : MonadAttach m] [inst_2 : Std.Iterator α m β]
  [inst_3 : Std.Iterator α₂ m γ] (f : β → m (Std.IterM m γ)) (it₁ : Std.IterM m β) (it₂ : Option (Std.IterM m γ)),
  Std.IterM.flatMapAfterM f it₁ it₂ = Std.IterM.flattenAfter✝ (Std.IterM.mapM f it₁) it₂
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.valuationSubringAtPrime.congr_simp : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (K : Type u_2) [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] (v v_1 : IsDedekindDomain.HeightOneSpectrum R),
  v = v_1 →
    IsDedekindDomain.HeightOneSpectrum.valuationSubringAtPrime K v =
      IsDedekindDomain.HeightOneSpectrum.valuationSubringAtPrime K v_1
-- Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
/-- For `‖z‖ ≤ 1/2`, the complex logarithm is bounded by `(3/2) * ‖z‖`.  -/
Complex.norm_log_one_add_half_le_self : ∀ {z : ℂ}, ‖z‖ ≤ 1 / 2 → ‖Complex.log (1 + z)‖ ≤ 3 / 2 * ‖z‖
-- Mathlib.CategoryTheory.Bicategory.Kan.IsKan
/-- Kan extensions on `g` along `f` are unique up to isomorphism.  -/
CategoryTheory.Bicategory.LeftExtension.IsKan.uniqueUpToIso : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} →
      {f : a ⟶ b} → {g : a ⟶ c} → {s t : CategoryTheory.Bicategory.LeftExtension f g} → s.IsKan → t.IsKan → (s ≅ t)
-- Lean.Parser.Do
Lean.Parser.Term.doHave : Lean.Parser.Parser
-- Mathlib.SetTheory.Ordinal.CantorNormalForm
Ordinal.CNF.rec_zero : ∀ {C : Ordinal.{u_2} → Sort u_1} (b : Ordinal.{u_2}) (H0 : C 0)
  (H : (o : Ordinal.{u_2}) → o ≠ 0 → C (o % b ^ Ordinal.log b o) → C o), Ordinal.CNF.rec b H0 H 0 = H0
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Matrix.isUnit_nonsing_inv_det_iff : ∀ {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α] {A : Matrix n n α},
  IsUnit A⁻¹.det ↔ IsUnit A.det
-- Mathlib.Topology.PartialHomeomorph.Basic
PartialHomeomorph.toHomeomorphOfSourceEqUnivTargetEqUniv_apply : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : PartialHomeomorph X Y)
  (h : e.source = Set.univ) (h' : e.target = Set.univ), ⇑(e.toHomeomorphOfSourceEqUnivTargetEqUniv h h') = ↑e
-- Mathlib.RingTheory.Ideal.Quotient.Operations
DoubleQuot.quotLeftToQuotSupₐ_toRingHom : ∀ (R : Type u) {A : Type u_1} [inst : CommSemiring R] [inst_1 : CommRing A] [inst_2 : Algebra R A] (I J : Ideal A),
  ↑(DoubleQuot.quotLeftToQuotSupₐ R I J) = DoubleQuot.quotLeftToQuotSup I J
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.ofChosenFiniteProducts.id_tensorHom_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (ℬ : (X Y : C) → CategoryTheory.Limits.LimitCone (CategoryTheory.Limits.pair X Y)) (X Y : C),
  CategoryTheory.CartesianMonoidalCategory.ofChosenFiniteProducts.tensorHom ℬ (CategoryTheory.CategoryStruct.id X)
      (CategoryTheory.CategoryStruct.id Y) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.CartesianMonoidalCategory.ofChosenFiniteProducts.tensorObj ℬ X Y)
-- Std.Do.Triple.SpecLemmas
List.Cursor.at.eq_1 : ∀ {α : Type u_1} (l : List α) (n : ℕ),
  List.Cursor.at l n = { «prefix» := List.take n l, suffix := List.drop n l, property := ⋯ }
-- Mathlib.CategoryTheory.Bicategory.Monad.Basic
/-- The counit 2-morphism of the comonad.  -/
CategoryTheory.Bicategory.termε : Lean.ParserDescr
-- Mathlib.Algebra.Ring.Pi
Pi.nonAssocSemiring : {I : Type u} → {f : I → Type v} → [(i : I) → NonAssocSemiring (f i)] → NonAssocSemiring ((i : I) → f i)
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.saveAppOf : Lean.HeadIndex → Lean.Meta.Grind.GrindM Unit
-- Mathlib.AlgebraicTopology.DoldKan.Faces
/-- A morphism `φ : Y ⟶ X _⦋n+1⦌` satisfies `HigherFacesVanish q φ`
when the compositions `φ ≫ X.δ j` are `0` for `j ≥ max 1 (n+2-q)`. When `q ≤ n+1`,
it basically means that the composition `φ ≫ X.δ j` are `0` for the `q` highest
possible values of a nonzero `j`. Otherwise, when `q ≥ n+2`, all the compositions
`φ ≫ X.δ j` for nonzero `j` vanish. See also the lemma `comp_P_eq_self_iff` in
`Projections.lean` which states that `HigherFacesVanish q φ` is equivalent to
the identity `φ ≫ (P q).f (n+1) = φ`.  -/
AlgebraicTopology.DoldKan.HigherFacesVanish : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [CategoryTheory.Preadditive C] →
      {X : CategoryTheory.SimplicialObject C} →
        {Y : C} → {n : ℕ} → ℕ → (Y ⟶ X.obj (Opposite.op { len := n + 1 })) → Prop
-- Mathlib.CategoryTheory.Subobject.Lattice
CategoryTheory.Subobject.finset_inf_factors : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  {I : Type u_1} {A B : C} {s : Finset I} {P : I → CategoryTheory.Subobject B} (f : A ⟶ B),
  (s.inf P).Factors f ↔ ∀ i ∈ s, (P i).Factors f
-- Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
UniformConvergenceCLM.isScalarTower : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {E : Type u_3}
  (F : Type u_4) [inst_2 : AddCommGroup E] [inst_3 : Module 𝕜₁ E] [inst_4 : TopologicalSpace E]
  [inst_5 : AddCommGroup F] [inst_6 : Module 𝕜₂ F] {S : Type u_6} {T : Type u_7} [inst_7 : TopologicalSpace F]
  [inst_8 : Monoid S] [inst_9 : DistribMulAction S F] [inst_10 : SMulCommClass 𝕜₂ S F]
  [inst_11 : ContinuousConstSMul S F] [inst_12 : Monoid T] [inst_13 : DistribMulAction T F]
  [inst_14 : SMulCommClass 𝕜₂ T F] [inst_15 : ContinuousConstSMul T F] [inst_16 : SMul S T] [IsScalarTower S T F]
  (𝔖 : Set (Set E)), IsScalarTower S T (UniformConvergenceCLM σ F 𝔖)
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
/-- The identity 1-morphism is an equivalence.  -/
CategoryTheory.Bicategory.Equivalence.id : {B : Type u₁} → [inst : CategoryTheory.Bicategory B] → (a : B) → CategoryTheory.Bicategory.Equivalence a a
-- Mathlib.Geometry.Euclidean.SignedDist
AffineSubspace.signedInfDist_def : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (s : AffineSubspace ℝ P) [inst_4 : Nonempty ↥s]
  [inst_5 : s.direction.HasOrthogonalProjection] (p : P),
  s.signedInfDist p = (signedDist (p -ᵥ ↑((EuclideanGeometry.orthogonalProjection s) p))) ↑Classical.ofNonempty
-- Mathlib.Topology.UniformSpace.Equiv
/-- Identity map as a uniform isomorphism.  -/
UniformEquiv.refl : (α : Type u_4) → [inst : UniformSpace α] → α ≃ᵤ α
-- Mathlib.Algebra.Module.Presentation.DirectSum
Module.Presentation.finsupp_relation : ∀ {A : Type u} [inst : Ring A] {N : Type v} [inst_1 : AddCommGroup N] [inst_2 : Module A N]
  (pres : Module.Presentation A N) (ι : Type w) [inst_3 : DecidableEq ι] [inst_4 : DecidableEq N]
  (x : (i : ι) × ((fun i => ((fun x => pres) i).toRelations) i).R),
  (pres.finsupp ι).relation x = Finsupp.embDomain (Function.Embedding.sigmaMk x.fst) (pres.relation x.snd)
-- Mathlib.CategoryTheory.Sites.Point.OfIsCofiltered
CategoryTheory.GrothendieckTopology.Point.toPresheafFiberOfIsCofiltered_w_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C]
  {N : Type u'} [inst_2 : CategoryTheory.Category.{v', u'} N] (p : CategoryTheory.Functor N C)
  [inst_3 : CategoryTheory.InitiallySmall N] {J : CategoryTheory.GrothendieckTopology C}
  [inst_4 : CategoryTheory.IsCofiltered N]
  (hp :
    ∀ ⦃X : C⦄,
      ∀ R ∈ J X,
        ∀ ⦃U : N⦄ (f : p.obj U ⟶ X),
          ∃ Y g,
            ∃ (_ : R.arrows g),
              ∃ V q a, CategoryTheory.CategoryStruct.comp a g = CategoryTheory.CategoryStruct.comp (p.map q) f)
  {A : Type u''} [inst_5 : CategoryTheory.Category.{v'', u''} A]
  [inst_6 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v'', u''} A] {V U : N} (f : V ⟶ U)
  (P : CategoryTheory.Functor Cᵒᵖ A) {Z : A}
  (h : (CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered p hp).presheafFiber.obj P ⟶ Z),
  CategoryTheory.CategoryStruct.comp (P.map (p.map f).op)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.GrothendieckTopology.Point.toPresheafFiberOfIsCofiltered p hp V P) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.GrothendieckTopology.Point.toPresheafFiberOfIsCofiltered p hp U P) h
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.CooperSplit.pred : Lean.Meta.Grind.Arith.Cutsat.CooperSplit → Lean.Meta.Grind.Arith.Cutsat.CooperSplitPred
-- Lean.Elab.DefView
Lean.Elab.DefsParsedSnapshot.mk.injEq : ∀ (toSnapshot : Lean.Language.Snapshot) (defs : Array Lean.Elab.DefParsed) (toSnapshot_1 : Lean.Language.Snapshot)
  (defs_1 : Array Lean.Elab.DefParsed),
  ({ toSnapshot := toSnapshot, defs := defs } = { toSnapshot := toSnapshot_1, defs := defs_1 }) =
    (toSnapshot = toSnapshot_1 ∧ defs = defs_1)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.toListModel_filter : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] {t : Std.DTreeMap.Internal.Impl α β} {h : t.Balanced}
  {f : (a : α) → β a → Bool},
  (Std.DTreeMap.Internal.Impl.filter f t h).impl.toListModel = List.filter (fun e => f e.fst e.snd) t.toListModel
-- Mathlib.Analysis.Complex.Exponential
Real.exp_eq_one_iff : ∀ (x : ℝ), Real.exp x = 1 ↔ x = 0
-- Mathlib.CategoryTheory.Monoidal.Bimod
Bimod.mk.sizeOf_spec : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {A B : CategoryTheory.Mon C} [inst_2 : SizeOf C] (X : C)
  (actLeft : CategoryTheory.MonoidalCategoryStruct.tensorObj A.X X ⟶ X)
  (one_actLeft :
    autoParam
      (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.one X) actLeft =
        (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom)
      Bimod.one_actLeft._autoParam)
  (left_assoc :
    autoParam
      (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul X) actLeft =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A.X A.X X).hom
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A.X actLeft) actLeft))
      Bimod.left_assoc._autoParam)
  (actRight : CategoryTheory.MonoidalCategoryStruct.tensorObj X B.X ⟶ X)
  (actRight_one :
    autoParam
      (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X CategoryTheory.MonObj.one) actRight =
        (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom)
      Bimod.actRight_one._autoParam)
  (right_assoc :
    autoParam
      (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X CategoryTheory.MonObj.mul) actRight =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X B.X B.X).inv
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight actRight B.X)
            actRight))
      Bimod.right_assoc._autoParam)
  (middle_assoc :
    autoParam
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight actLeft B.X) actRight =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A.X X B.X).hom
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A.X actRight) actLeft))
      Bimod.middle_assoc._autoParam),
  sizeOf
      { X := X, actLeft := actLeft, one_actLeft := one_actLeft, left_assoc := left_assoc, actRight := actRight,
        actRight_one := actRight_one, right_assoc := right_assoc, middle_assoc := middle_assoc } =
    1 + sizeOf X + sizeOf actLeft + sizeOf one_actLeft + sizeOf left_assoc + sizeOf actRight + sizeOf actRight_one +
        sizeOf right_assoc +
      sizeOf middle_assoc
-- Mathlib.Algebra.Group.Submonoid.Defs
AddSubmonoid.mem_bot : ∀ {M : Type u_1} [inst : AddZeroClass M] {x : M}, x ∈ ⊥ ↔ x = 0
-- Mathlib.Probability.Moments.SubGaussian
ProbabilityTheory.HasCondSubgaussianMGF.fun_zero : ∀ {Ω : Type u_1} {m mΩ : MeasurableSpace Ω} {hm : m ≤ mΩ} [inst : StandardBorelSpace Ω] {μ : MeasureTheory.Measure Ω}
  [inst_1 : MeasureTheory.IsFiniteMeasure μ], ProbabilityTheory.HasCondSubgaussianMGF m hm (fun x => 0) 0 μ
-- Init.Data.List.Basic
List.or_cons : ∀ {a : Bool} {l : List Bool}, (a :: l).or = (a || l.or)
-- Mathlib.Topology.Algebra.UniformConvergence
instAddMonoidUniformOnFun : {α : Type u_1} → {β : Type u_2} → {𝔖 : Set (Set α)} → [AddMonoid β] → AddMonoid (UniformOnFun α β 𝔖)
-- Mathlib.RepresentationTheory.Intertwining
Representation.Equiv.toLinearMap_refl : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} [inst : Semiring A] [inst_1 : Monoid G] [inst_2 : AddCommMonoid V]
  [inst_3 : Module A V] {ρ : Representation A G V}, (↑(Representation.Equiv.refl ρ)).toLinearMap = LinearMap.id
-- Mathlib.Data.Nat.BinaryRec
Nat.binaryRecFromOne_zero : ∀ {motive : ℕ → Sort u} (zero : motive 0) (one : motive 1)
  (bit : (b : Bool) → (n : ℕ) → n ≠ 0 → motive n → motive (Nat.bit b n)), Nat.binaryRecFromOne zero one bit 0 = zero
-- Mathlib.NumberTheory.Padics.MahlerBasis
/-- The uniform norm of the `k`-th Mahler basis function is 1, for every `k`.
 -/
PadicInt.norm_mahler_eq : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] (k : ℕ), ‖mahler k‖ = 1
-- Mathlib.Analysis.Calculus.FDeriv.Analytic
ContinuousMultilinearMap.norm_iteratedFDeriv_le : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {ι : Type u_2} {E : ι → Type u_3} [inst_3 : (i : ι) → NormedAddCommGroup (E i)]
  [inst_4 : (i : ι) → NormedSpace 𝕜 (E i)] [inst_5 : Fintype ι] (f : ContinuousMultilinearMap 𝕜 E F) (n : ℕ)
  (x : (i : ι) → E i),
  ‖iteratedFDeriv 𝕜 n (⇑f) x‖ ≤ ↑((Fintype.card ι).descFactorial n) * ‖f‖ * ‖x‖ ^ (Fintype.card ι - n)
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.X_mul_cancel_right_iff : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {p q : MvPolynomial σ R} {i : σ},
  p * MvPolynomial.X i = q * MvPolynomial.X i ↔ p = q
-- Plausible.DeriveShrinkable
/-- Creates instance commands for the `Shrinkable` typeclass  -/
_private.Plausible.DeriveShrinkable.0.Plausible.mkShrinkableInstanceCmds : Lean.Elab.Deriving.Context → Array Lean.Name → Lean.Elab.TermElabM (Array Lean.Command)
-- Init.Grind.Config
/-- Maximum number of case-splits in a proof search branch. It does not include splits performed during normalization.  -/
Lean.Grind.Config.splits : Lean.Grind.Config → ℕ
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.toArray_map_eq_toArray_mapM : ∀ {α β γ : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : MonadAttach m] [LawfulMonad m]
  [WeaklyLawfulMonadAttach m] [inst_4 : Std.Iterator α m β] [Std.Iterators.Finite α m] {f : β → γ} {it : Std.IterM m β},
  (Std.IterM.map f it).toArray = (Std.IterM.mapM (fun b => pure (f b)) it).toArray
-- Std.Time.Internal.UnitVal
Std.Time.Internal.UnitVal.ofInt.injEq : ∀ {α : ℚ} (val val_1 : ℤ), ({ val := val } = { val := val_1 }) = (val = val_1)
-- Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
SSet.N.dim_lt_of_lt : ∀ {X : SSet} {x y : X.N}, x < y → x.dim < y.dim
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.get_eq_get_get? : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k : α} {h : k ∈ t},
  t.get k h = (t.get? k).get ⋯
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap.0.Std.IterM.DefaultConsumers.forIn'_eq_match_step.match_3.eq_3 : ∀ {α β : Type u_1} {m : Type u_1 → Type u_2} [inst : Std.Iterator α m β] {it : Std.IterM m β}
  (motive : it.Step → Sort u_3) (property : it.IsPlausibleStep Std.IterStep.done)
  (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 : (property : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, property⟩),
  (match ⟨Std.IterStep.done, property⟩ with
    | ⟨Std.IterStep.yield it' out, h⟩ => h_1 it' out h
    | ⟨Std.IterStep.skip it', h⟩ => h_2 it' h
    | ⟨Std.IterStep.done, property⟩ => h_3 property) =
    h_3 property
-- Lean.ScopedEnvExtension
/-- The following function is used to implement `end_local_scope` command.

By default, all states have `delimitsLocal` set to `true`, and the following code modifies only the top element of the stack.
If the top element’s `delimitsLocal` is `false`, the function instead traverses down the stack until it reaches the first state where `delimitsLocal` is `true`.
Intuitively, `delimitsLocal` of each `State` determines whether local entries are delimited. When set to false, it allows traversal through implicit scopes where local entries are not delimited.
 -/
Lean.stateStackModify : {α β σ : Type} →
  Lean.ScopedEnvExtension α β σ → List (Lean.ScopedEnvExtension.State σ) → β → List (Lean.ScopedEnvExtension.State σ)
-- Mathlib.Data.DFinsupp.Order
DFinsupp.instSMulPosReflectLT : ∀ {ι : Type u_1} {α : Type u_3} {β : ι → Type u_4} [inst : Semiring α] [inst_1 : PartialOrder α]
  [inst_2 : (i : ι) → AddCommMonoid (β i)] [inst_3 : (i : ι) → PartialOrder (β i)] [inst_4 : (i : ι) → Module α (β i)]
  [∀ (i : ι), SMulPosReflectLT α (β i)], SMulPosReflectLT α (Π₀ (i : ι), β i)
-- Mathlib.Order.RelSeries
RelSeries.append_apply_left : ∀ {α : Type u_1} {r : SetRel α α} (p q : RelSeries r) (connect : (p.last, q.head) ∈ r) (i : Fin (p.length + 1)),
  (p.append q connect).toFun (Fin.cast ⋯ (Fin.castAdd (q.length + 1) i)) = p.toFun i
-- Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject
CategoryTheory.SimplicialObject.Splitting.isSplitMono_fromNondegComplex : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : CategoryTheory.SimplicialObject C} (s : X.Splitting)
  [inst_1 : CategoryTheory.Preadditive C], CategoryTheory.IsSplitMono s.fromNondegComplex
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
/-- The composition of a continuous function of two variables and two ae strongly measurable
functions is ae strongly measurable.  -/
Continuous.comp_aestronglyMeasurable₂ : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace β] [inst_1 : TopologicalSpace γ]
  {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β' : Type u_5} [inst_2 : TopologicalSpace β']
  {g : β → β' → γ} {f : α → β} {f' : α → β'},
  Continuous (Function.uncurry g) →
    MeasureTheory.AEStronglyMeasurable f μ →
      MeasureTheory.AEStronglyMeasurable f' μ → MeasureTheory.AEStronglyMeasurable (fun x => g (f x) (f' x)) μ
-- Init.Data.String.Defs
ByteArray.IsValidUTF8.append : ∀ {b b' : ByteArray}, b.IsValidUTF8 → b'.IsValidUTF8 → (b ++ b').IsValidUTF8
-- Mathlib.Geometry.Polygon.Basic
Polygon.toTriangle_points : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring R] [inst_1 : AddCommGroup V] [inst_2 : Module R V]
  [inst_3 : AddTorsor V P] (p : Polygon P 3) (h : Polygon.HasNondegenerateVertices R p),
  (Polygon.toTriangle R p h).points = p.vertices
-- Std.Http.Server
/-- Create a new `Server` structure with an optional configuration.
 -/
Std.Http.Server.new : optParam Std.Http.Config { } → optParam (Option Std.Net.SocketAddress) none → IO Std.Http.Server
-- Std.Data.DTreeMap.Internal.Model
/-- Model implementation of the `getEntryD` function.
Internal implementation detail of the tree map
 -/
Std.DTreeMap.Internal.Impl.getEntryDₘ : {α : Type u} → {β : α → Type v} → [Ord α] → α → Std.DTreeMap.Internal.Impl α β → (a : α) × β a → (a : α) × β a
-- Mathlib.Geometry.Manifold.IsManifold.Basic
ModelWithCorners.locallyCompactSpace : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] [LocallyCompactSpace E]
  (I : ModelWithCorners 𝕜 E H), LocallyCompactSpace H
-- Mathlib.Topology.Semicontinuity.Basic
/-- The sum of two upper semicontinuous functions is upper semicontinuous. Formulated with
`[ContinuousAdd]`. The primed version of the lemma uses an explicit continuity assumption on
addition, for application to `EReal`.  -/
UpperSemicontinuousAt.add : ∀ {α : Type u_1} [inst : TopologicalSpace α] {x : α} {γ : Type u_5} [inst_1 : AddCommMonoid γ] [inst_2 : LinearOrder γ]
  [IsOrderedAddMonoid γ] [inst_4 : TopologicalSpace γ] [OrderTopology γ] [ContinuousAdd γ] {f g : α → γ},
  UpperSemicontinuousAt f x → UpperSemicontinuousAt g x → UpperSemicontinuousAt (fun z => f z + g z) x
-- Mathlib.Algebra.Module.Submodule.Range
LinearMap.comap_le_comap_iff : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  [inst_6 : RingHomSurjective τ₁₂] {f : M →ₛₗ[τ₁₂] M₂},
  f.range = ⊤ → ∀ {p p' : Submodule R₂ M₂}, Submodule.comap f p ≤ Submodule.comap f p' ↔ p ≤ p'
-- Mathlib.RingTheory.DedekindDomain.SelmerGroup
IsDedekindDomain.HeightOneSpectrum.valuation_of_unit_eq : ∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDedekindDomain R] {K : Type v} [inst_2 : Field K] [inst_3 : Algebra R K]
  [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) (x : Rˣ),
  v.valuationOfNeZero ((Units.map ↑(algebraMap R K)) x) = 1
-- Lean.Parser.Syntax
Lean.Parser.Syntax.paren : Lean.Parser.Parser