mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.ModelTheory.LanguageMap
FirstOrder.Language.constantsOn_Functions : ∀ (α : Type u') (a : ℕ), (FirstOrder.Language.constantsOn α).Functions a = FirstOrder.Language.constantsOnFunc α a
-- Mathlib.Order.KrullDimension
/-- Variant of `coheight_le_iff` ranging only over those series that begin exactly on `a`.
 -/
Order.coheight_le_iff' : ∀ {α : Type u_1} [inst : Preorder α] {a : α} {n : ℕ∞},
  Order.coheight a ≤ n ↔ ∀ ⦃p : LTSeries α⦄, RelSeries.head p = a → ↑p.length ≤ n
-- Init.Data.UInt.Basic
/-- Negation of 32-bit unsigned integers, computed modulo `UInt32.size`.

`UInt32.neg a` is equivalent to `429_4967_295 - a + 1`.

This function is overridden at runtime with an efficient implementation.
 -/
UInt32.neg : UInt32 → UInt32
-- Lean.Meta.Tactic.Grind.Split
/-- Returns the next case-split to be performed. It uses a very simple heuristic.  -/
_private.Lean.Meta.Tactic.Grind.Split.0.Lean.Meta.Grind.selectNextSplit? : Lean.Meta.Grind.GoalM Lean.Meta.Grind.SplitCandidate✝
-- Mathlib.Data.FP.Basic
FP.Float.sub : [C : FP.FloatCfg] → FP.RMode → FP.Float → FP.Float → FP.Float
-- Mathlib.LinearAlgebra.CliffordAlgebra.Prod
/-- The reverse direction of `CliffordAlgebra.prodEquiv`.  -/
CliffordAlgebra.toProd : {R : Type u_1} →
  {M₁ : Type u_2} →
    {M₂ : Type u_3} →
      [inst : CommRing R] →
        [inst_1 : AddCommGroup M₁] →
          [inst_2 : AddCommGroup M₂] →
            [inst_3 : Module R M₁] →
              [inst_4 : Module R M₂] →
                (Q₁ : QuadraticForm R M₁) →
                  (Q₂ : QuadraticForm R M₂) →
                    GradedTensorProduct R (CliffordAlgebra.evenOdd Q₁) (CliffordAlgebra.evenOdd Q₂) →ₐ[R]
                      CliffordAlgebra (QuadraticMap.prod Q₁ Q₂)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem_eq_getD : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {a : α} {fallback : β} {h' : a ∈ t}, t[a] = t.getD a fallback
-- Mathlib.Algebra.Ring.Opposite
AddOpposite.instSemiring : {R : Type u_1} → [Semiring R] → Semiring Rᵃᵒᵖ
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey!_union!_of_contains_eq_false_right : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [inst : Inhabited α]
  [Std.TransOrd α],
  m₁.WF → m₂.WF → ∀ {k : α}, Std.DTreeMap.Internal.Impl.contains k m₂ = false → (m₁.union! m₂).getKey! k = m₁.getKey! k
-- Mathlib.RingTheory.Bialgebra.Hom
Bialgebra.ext_to_ring_iff : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Bialgebra R A]
  {f g : A →ₐc[R] R}, f = g ↔ True
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instDiv : {G : Type u_1} → [inst : TopologicalSpace G] → [inst_1 : Div G] → [ContinuousDiv G] → Div (SeparationQuotient G)
-- Mathlib.CategoryTheory.Monoidal.Mon
/-- Composition of morphisms of monoid objects.  -/
CategoryTheory.Mon.comp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] → {M N O : CategoryTheory.Mon C} → M.Hom N → N.Hom O → M.Hom O
-- Mathlib.Algebra.Order.Floor.Div
Pi.instFloorDiv : {ι : Type u_1} →
  {α : Type u_2} →
    {π : ι → Type u_4} →
      [inst : AddCommMonoid α] →
        [inst_1 : PartialOrder α] →
          [inst_2 : (i : ι) → AddCommMonoid (π i)] →
            [inst_3 : (i : ι) → PartialOrder (π i)] →
              [inst_4 : (i : ι) → SMulZeroClass α (π i)] → [(i : ι) → FloorDiv α (π i)] → FloorDiv α ((i : ι) → π i)
-- Mathlib.NumberTheory.LucasLehmer
LucasLehmer.X.coe_mul : ∀ {q : ℕ} (n m : ℤ), ↑(n * m) = ↑n * ↑m
-- Mathlib.NumberTheory.ModularForms.SlashInvariantForms
/-- Copy of a `SlashInvariantForm` with a new `toFun` equal to the old one.
Useful to fix definitional equalities.  -/
SlashInvariantForm.copy : {Γ : outParam (Subgroup (GL (Fin 2) ℝ))} →
  {k : outParam ℤ} → (f : SlashInvariantForm Γ k) → (f' : UpperHalfPlane → ℂ) → f' = ⇑f → SlashInvariantForm Γ k
-- Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
ENNReal.log_lt_top_iff : ∀ {x : ENNReal}, x.log < ⊤ ↔ x < ⊤
-- Mathlib.Data.PFunctor.Univariate.M
PFunctor.Approx.CofixA.intro.inj : ∀ {F : PFunctor.{uA, uB}} {n : ℕ} {a : F.A} {a_1 : F.B a → PFunctor.Approx.CofixA F n} {a_2 : F.A}
  {a_3 : F.B a_2 → PFunctor.Approx.CofixA F n},
  PFunctor.Approx.CofixA.intro a a_1 = PFunctor.Approx.CofixA.intro a_2 a_3 → a = a_2 ∧ a_1 ≍ a_3
-- Mathlib.AlgebraicTopology.MooreComplex
_private.Mathlib.AlgebraicTopology.MooreComplex.0.AlgebraicTopology.NormalizedMooreComplex.objX.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (n : ℕ) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match n.succ with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_2 n
-- Mathlib.Analysis.Asymptotics.Lemmas
Asymptotics.isLittleO_const_smul_right : ∀ {α : Type u_1} {E : Type u_3} {E' : Type u_6} {𝕜 : Type u_15} [inst : Norm E] [inst_1 : SeminormedAddCommGroup E']
  [inst_2 : NormedDivisionRing 𝕜] {f : α → E} {f' : α → E'} {l : Filter α} [inst_3 : Module 𝕜 E'] [NormSMulClass 𝕜 E']
  {c : 𝕜}, c ≠ 0 → ((f =o[l] fun x => c • f' x) ↔ f =o[l] f')
-- Mathlib.Algebra.Homology.Embedding.StupidTrunc
/-- The isomorphism `(K.stupidTrunc e).X i' ≅ K.X i'` when `i` is in the image of `e.f`.  -/
HomologicalComplex.stupidTruncXIso : {ι : Type u_1} →
  {ι' : Type u_2} →
    {c : ComplexShape ι} →
      {c' : ComplexShape ι'} →
        {C : Type u_3} →
          [inst : CategoryTheory.Category.{v_1, u_3} C] →
            [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
              [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
                (K : HomologicalComplex C c') →
                  (e : c.Embedding c') →
                    [inst_3 : e.IsRelIff] → {i : ι} → {i' : ι'} → e.f i = i' → ((K.stupidTrunc e).X i' ≅ K.X i')
-- Mathlib.Combinatorics.Tiling.Tile
DiscreteTiling.Prototile.coe_mk : ∀ {G : Type u_1} {X : Type u_2} [inst : Group G] [inst_1 : MulAction G X] (c : Set X)
  (s : Subgroup ↥(MulAction.stabilizer G c)), ↑{ carrier := c, symmetries := s } = c
-- Mathlib.Control.Basic
/-- A generalization of `List.zipWith` which combines list elements with an `Applicative`.  -/
zipWithM : {F : Type u → Type v} → [Applicative F] → {α₁ α₂ φ : Type u} → (α₁ → α₂ → F φ) → List α₁ → List α₂ → F (List φ)
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
CategoryTheory.Limits.instHasColimitOppositeDiscreteOpFunctor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C}
  [CategoryTheory.Limits.HasProduct Z], CategoryTheory.Limits.HasColimit (CategoryTheory.Discrete.functor Z).op
-- Mathlib.NumberTheory.ModularForms.NormTrace
/-- The trace of a cusp form, as a cusp form.  -/
CuspForm.trace : {𝒢 : Subgroup (GL (Fin 2) ℝ)} →
  (ℋ : Subgroup (GL (Fin 2) ℝ)) →
    {F : Type u_1} →
      F → [inst : FunLike F UpperHalfPlane ℂ] → {k : ℤ} → [𝒢.IsFiniteRelIndex ℋ] → [CuspFormClass F 𝒢 k] → CuspForm ℋ k
-- Mathlib.Topology.Category.LightProfinite.Injective
/-- A nonempty light profinite space is injective in `Profinite`.  -/
Profinite.injective_of_light : ∀ (S : LightProfinite) [Nonempty ↑S.toTop], CategoryTheory.Injective (lightToProfinite.obj S)
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.preimage_const_sub_Ici : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] (a b : α),
  (fun x => a - x) ⁻¹' Set.Ici b = Set.Iic (a - b)
-- Mathlib.NumberTheory.Chebyshev
Chebyshev.theta_ge' : ∀ {x : ℝ}, 1 ≤ x → (x - 1) * Real.log 2 - Real.log (x + 2) - 2 * √x * Real.log x ≤ Chebyshev.theta x
-- Mathlib.Topology.Algebra.InfiniteSum.Module
ContinuousLinearEquiv.tsum_eq_iff : ∀ {ι : Type u_5} {R : Type u_7} {R₂ : Type u_8} {M : Type u_9} {M₂ : Type u_10} [inst : Semiring R]
  [inst_1 : Semiring R₂] [inst_2 : AddCommMonoid M] [inst_3 : Module R M] [inst_4 : AddCommMonoid M₂]
  [inst_5 : Module R₂ M₂] [inst_6 : TopologicalSpace M] [inst_7 : TopologicalSpace M₂] {σ : R →+* R₂} {σ' : R₂ →+* R}
  [inst_8 : RingHomInvPair σ σ'] [inst_9 : RingHomInvPair σ' σ] {L : SummationFilter ι} [T2Space M] [T2Space M₂]
  {f : ι → M} (e : M ≃SL[σ] M₂) {y : M₂}, ∑'[L] (z : ι), e (f z) = y ↔ ∑'[L] (z : ι), f z = e.symm y
-- Init.Data.List.Lemmas
List.getLast_of_getLast?_eq_some : ∀ {α : Type u_1} {x : α} {l : List α} (hx : l.getLast? = some x), l.getLast ⋯ = x
-- Mathlib.Analysis.MeanInequalities
NNReal.Lr_rpow_le_Lp_mul_Lq_tsum : ∀ {ι : Type u} {f g : ι → NNReal} {p q r : ℝ},
  p.HolderTriple q r →
    (Summable fun i => f i ^ p) →
      (Summable fun i => g i ^ q) →
        ∑' (i : ι), (f i * g i) ^ r ≤ (∑' (i : ι), f i ^ p) ^ (r / p) * (∑' (i : ι), g i ^ q) ^ (r / q)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVUnOp.not.sizeOf_spec : sizeOf Std.Tactic.BVDecide.BVUnOp.not = 1
-- Std.Http.Data.URI.Encoding
Std.Http.Internal.Char.isAsciiByte.eq_1 : ∀ (c : UInt8), Std.Http.Internal.Char.isAsciiByte c = decide (c < 128)
-- Mathlib.Data.List.Dedup
List.dedup_map_of_injective : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq α] [inst_1 : DecidableEq β] {f : α → β},
  Function.Injective f → ∀ (xs : List α), (List.map f xs).dedup = List.map f xs.dedup
-- Init.Data.List.Basic
List.instHasSubset : {α : Type u} → HasSubset (List α)
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.preimage_add_left_zero' : ∀ {α : Type u_2} [inst : AddGroup α] {a : α}, (fun x => -a + x) ⁻¹' 0 = {a}
-- Mathlib.NumberTheory.Padics.PadicNorm
/-- The `p`-adic norm of `0` is `0`.  -/
padicNorm.zero : ∀ {p : ℕ}, padicNorm p 0 = 0
-- Mathlib.Algebra.Group.Submonoid.Defs
Submonoid.mem_mk : ∀ {M : Type u_1} [inst : MulOneClass M] {s : Subsemigroup M} {x : M} (h_one : 1 ∈ s.carrier),
  x ∈ { toSubsemigroup := s, one_mem' := h_one } ↔ x ∈ s
-- Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1
/-- A 1-cocycle is a 1-cochain which satisfies the cocycle condition.  -/
CategoryTheory.PresheafOfGroups.OneCocycle : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.Functor Cᵒᵖ GrpCat → {I : Type w'} → (I → C) → Type (max (max (max u v) w) w')
-- Init.Data.SInt.Basic
/-- Computes the absolute value of an 8-bit signed integer.

This function is equivalent to `if a < 0 then -a else a`, so in particular `Int8.minValue` will be
mapped to `Int8.minValue`.

This function is overridden at runtime with an efficient implementation.
 -/
Int8.abs : Int8 → Int8
-- Mathlib.Data.Part
Part.left_dom_of_append_dom : ∀ {α : Type u_1} [inst : Append α] {a b : Part α}, (a ++ b).Dom → a.Dom
-- Init.Data.Nat.Lcm
Nat.pow_lcm_pow : ∀ {k n m : ℕ}, (n ^ k).lcm (m ^ k) = n.lcm m ^ k
-- Mathlib.GroupTheory.ArchimedeanDensely
MulEquiv.withZero.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : Group α] [inst_1 : Group β],
  MulEquiv.withZero =
    {
      toFun := fun e =>
        { toFun := ⇑(WithZero.map' ↑e), invFun := ⇑(WithZero.map' ↑e.symm), left_inv := ⋯, right_inv := ⋯,
          map_mul' := ⋯ },
      invFun := fun e =>
        { toFun := fun x => WithZero.unzero ⋯, invFun := fun x => WithZero.unzero ⋯, left_inv := ⋯, right_inv := ⋯,
          map_mul' := ⋯ },
      left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.Geometry.Manifold.Riemannian.Basic
/-- **Alias** of `PseudoEMetricSpace.ofRiemannianMetric`.

---

The pseudoemetric space structure associated to a Riemannian metric on a manifold. Designed
so that the topology is defeq to the original one.

This should only be used when constructing data in specific situations. To develop the theory,
one should rather assume that there is an already existing emetric space structure, which satisfies
additionally the predicate `IsRiemannianManifold I M`.  -/
PseudoEmetricSpace.ofRiemannianMetric : {E : Type u_1} →
  [inst : NormedAddCommGroup E] →
    [inst_1 : NormedSpace ℝ E] →
      {H : Type u_2} →
        [inst_2 : TopologicalSpace H] →
          (I : ModelWithCorners ℝ E H) →
            (M : Type u_3) →
              [inst_3 : TopologicalSpace M] →
                [inst_4 : ChartedSpace H M] →
                  [inst_5 : Bundle.RiemannianBundle fun x => TangentSpace I x] →
                    [inst_6 : IsManifold I 1 M] →
                      [IsContinuousRiemannianBundle E fun x => TangentSpace I x] →
                        [RegularSpace M] → PseudoEMetricSpace M
-- Mathlib.GroupTheory.MonoidLocalization.Order
/-- An ordered cancellative monoid injects into its localization by sending `a` to `a / b`.  -/
Localization.mkOrderEmbedding : {α : Type u_1} →
  [inst : CommMonoid α] →
    [inst_1 : PartialOrder α] → [inst_2 : IsOrderedCancelMonoid α] → {s : Submonoid α} → ↥s → α ↪o Localization s
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.functorEquiv_unitIso_inv_app_app_snd : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) (X : Type u₄)
  [inst_3 : CategoryTheory.Category.{v₄, u₄} X]
  (X_1 : CategoryTheory.Functor X (CategoryTheory.Limits.CategoricalPullback F G)) (X_2 : X),
  (((CategoryTheory.Limits.CategoricalPullback.functorEquiv F G X).unitIso.inv.app X_1).app X_2).snd =
    CategoryTheory.CategoryStruct.id (X_1.obj X_2).snd
-- Mathlib.Topology.Constructions.SumProd
continuous_prodMap_iff : ∀ {X : Type u} {Y : Type v} {W : Type u_1} {Z : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] [inst_3 : TopologicalSpace W] [Nonempty Z] [Nonempty W] {f : Z → X} {g : W → Y},
  Continuous (Prod.map f g) ↔ Continuous f ∧ Continuous g
-- Mathlib.Tactic.CategoryTheory.MonoidalComp
/-- Compose two morphisms in a monoidal category,
inserting unitors and associators between as necessary.  -/
CategoryTheory.monoidalComp : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {W X Y Z : C} → [CategoryTheory.MonoidalCoherence X Y] → (W ⟶ X) → (Y ⟶ Z) → (W ⟶ Z)
-- Mathlib.CategoryTheory.Bicategory.Product
CategoryTheory.Bicategory.prod_homCategory_comp_snd : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] (C : Type u₂) [inst_1 : CategoryTheory.Bicategory C] (X Y : B × C)
  {X_1 Y_1 Z : (X.1 ⟶ Y.1) × (X.2 ⟶ Y.2)} (f : (X_1.1 ⟶ Y_1.1) × (X_1.2 ⟶ Y_1.2)) (g : (Y_1.1 ⟶ Z.1) × (Y_1.2 ⟶ Z.2)),
  (CategoryTheory.CategoryStruct.comp f g).2 = CategoryTheory.CategoryStruct.comp f.2 g.2
-- Mathlib.CategoryTheory.Limits.Fubini
/-- For each object, a cocone.  -/
CategoryTheory.Limits.DiagramOfCocones.obj : {J : Type u_1} →
  {K : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} J] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} K] →
        {C : Type u_3} →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} C] →
            {F : CategoryTheory.Functor J (CategoryTheory.Functor K C)} →
              CategoryTheory.Limits.DiagramOfCocones F → (j : J) → CategoryTheory.Limits.Cocone (F.obj j)
-- Mathlib.Tactic.Choose
/-- Parse a `choose` argument from `chooseBinder` syntax. Accepts:
- `x` - plain identifier
- `_` - anonymous
- `(x : T)` - identifier with type annotation
- `(_ : T)` - anonymous with type annotation  -/
Mathlib.Tactic.Choose.parseChooseArg : Lean.TSyntax `Mathlib.Tactic.Choose.chooseBinder → Lean.MetaM Mathlib.Tactic.Choose.ChooseArg
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
contMDiffWithinAt_univ : ∀ {𝕜 : 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] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {x : M} {n : WithTop ℕ∞},
  ContMDiffWithinAt I I' n f Set.univ x ↔ ContMDiffAt I I' n f x
-- Mathlib.LinearAlgebra.TensorProduct.Map
LinearMap.rTensor_comm : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_7} {N : Type u_8} {P : Type u_9} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : Module R P] (f : M →ₗ[R] P) (x : TensorProduct R N M),
  (LinearMap.rTensor N f) ((TensorProduct.comm R N M) x) = (TensorProduct.comm R N P) ((LinearMap.lTensor N f) x)
-- Mathlib.Order.Filter.AtTopBot.Finset
Filter.tendsto_finset_image_atTop_atTop : ∀ {β : Type u_4} {γ : Type u_5} [inst : DecidableEq β] {i : β → γ} {j : γ → β},
  Function.LeftInverse j i → Filter.Tendsto (Finset.image j) Filter.atTop Filter.atTop
-- Mathlib.CategoryTheory.Functor.CurryingThree
CategoryTheory.Functor.instFaithfulProdCurry₃ : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_4} {E : Type u_9} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_4} C₃]
  [inst_3 : CategoryTheory.Category.{v_9, u_9} E], CategoryTheory.Functor.curry₃.Faithful
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.SimplicialObject.Truncated.cosk.full : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (n : ℕ)
  [inst_1 :
    ∀ (F : CategoryTheory.Functor (SimplexCategory.Truncated n)ᵒᵖ C),
      (SimplexCategory.Truncated.inclusion n).op.HasRightKanExtension F]
  [∀ (F : CategoryTheory.Functor (SimplexCategory.Truncated n)ᵒᵖ C),
      (SimplexCategory.Truncated.inclusion n).op.HasPointwiseRightKanExtension F],
  (CategoryTheory.SimplicialObject.Truncated.cosk n).Full
-- Init.PropLemmas
or_imp : ∀ {a b c : Prop}, a ∨ b → c ↔ (a → c) ∧ (b → c)
-- Mathlib.Topology.Bornology.Hom
LocallyBoundedMap.cancel_right : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Bornology α] [inst_1 : Bornology β] [inst_2 : Bornology γ]
  {g₁ g₂ : LocallyBoundedMap β γ} {f : LocallyBoundedMap α β},
  Function.Surjective ⇑f → (g₁.comp f = g₂.comp f ↔ g₁ = g₂)
-- Mathlib.NumberTheory.Padics.PadicNumbers
Padic.valuation_ofNat : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] (n : ℕ) [inst : n.AtLeastTwo], (OfNat.ofNat n).valuation = ↑(padicValNat p n)
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.instIsTorsionFree : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} [inst : CommRing R], Module.IsTorsionFree R (QuaternionAlgebra R c₁ c₂ c₃)
-- Mathlib.RingTheory.IsGaloisGroup.Basic
IsGaloisGroup.mulEquivAlgEquiv_apply_apply : ∀ (G : Type u_1) [inst : Group G] (A : Type u_2) (B : Type u_3) [inst_1 : CommRing A] [inst_2 : CommRing B]
  [inst_3 : IsDomain B] [inst_4 : Algebra A B] [inst_5 : FaithfulSMul A B] [inst_6 : MulSemiringAction G B]
  [inst_7 : IsGaloisGroup G A B] [inst_8 : Finite G] (a : G) (a_1 : B),
  ((IsGaloisGroup.mulEquivAlgEquiv G A B) a) a_1 = a • a_1
-- Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
/-- Computes `legendreSym p a` using `fastJacobiSym`.  -/
_private.Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol.0.fastLegendreSym : (p : ℕ) → [Fact (Nat.Prime p)] → ℤ → ℤ
-- Mathlib.Probability.Kernel.IonescuTulcea.Traj
ProbabilityTheory.Kernel.condExp_traj' : ∀ {X : ℕ → Type u_1} [inst : (n : ℕ) → MeasurableSpace (X n)]
  {κ : (n : ℕ) → ProbabilityTheory.Kernel ((i : ↥(Finset.Iic n)) → X ↑i) (X (n + 1))}
  [inst_1 : ∀ (n : ℕ), ProbabilityTheory.IsMarkovKernel (κ n)] {E : Type u_2} [inst_2 : NormedAddCommGroup E]
  [inst_3 : NormedSpace ℝ E] [CompleteSpace E] {a b c : ℕ},
  a ≤ b →
    b ≤ c →
      ∀ (x₀ : (i : ↥(Finset.Iic a)) → X ↑i) (f : ((n : ℕ) → X n) → E),
        ((ProbabilityTheory.Kernel.traj κ a) x₀)[f |
            ↑MeasureTheory.Filtration.piLE b] =ᵐ[(ProbabilityTheory.Kernel.traj κ a) x₀]
          fun x =>
          ∫ (y : (i : ↥(Finset.Iic c)) → X ↑i),
            ((ProbabilityTheory.Kernel.traj κ a) x₀)[f | ↑MeasureTheory.Filtration.piLE c]
              (Function.updateFinset x (Finset.Iic c)
                y) ∂(ProbabilityTheory.Kernel.partialTraj κ b c) (Preorder.frestrictLe b x)
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getElem?_union_of_not_mem_left : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α}, k ∉ m₁ → (m₁ ∪ m₂)[k]? = m₂[k]?
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.Hom₂.left_unitor_inv : {B : Type u} →
  [inst : Quiver B] →
    {a b : CategoryTheory.FreeBicategory B} →
      (f : a ⟶ b) →
        CategoryTheory.FreeBicategory.Hom₂ f (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id a) f)
-- Lean.Parser.Syntax
Lean.Parser.Command.syntax : Lean.Parser.Parser
-- Mathlib.FieldTheory.Perfect
iterate_frobeniusEquiv_symm_pow_p_pow : ∀ (R : Type u_1) (p : ℕ) [inst : CommSemiring R] [inst_1 : ExpChar R p] [inst_2 : PerfectRing R p] (x : R) (n : ℕ),
  (⇑(frobeniusEquiv R p).symm)^[n] x ^ p ^ n = x
-- Mathlib.Algebra.Lie.Solvable
LieAlgebra.abelian_iff_derived_succ_eq_bot : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (I : LieIdeal R L)
  (k : ℕ), IsLieAbelian ↥(LieAlgebra.derivedSeriesOfIdeal R L k I) ↔ LieAlgebra.derivedSeriesOfIdeal R L (k + 1) I = ⊥
-- Mathlib.Lean.Meta.Simp
/-- Run `e` while the entries in `declNames` are erased from the `simp` set, while preserving the
rest of the `simp` configuration.

Performance note: the code in `e` will be run with a new cache (which is discarded at the end of the
function). The original cache is restored when this function returns.
 -/
Lean.Meta.Simp.withoutTheorems : {α : Type} → Array Lean.Name → Lean.Meta.SimpM α → Lean.Meta.SimpM α
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarAlgebra.adjoin_le : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : NonUnitalSemiring A]
  [inst_3 : StarRing A] [inst_4 : Module R A] [inst_5 : IsScalarTower R A A] [inst_6 : SMulCommClass R A A]
  [inst_7 : StarModule R A] {S : NonUnitalStarSubalgebra R A} {s : Set A}, s ⊆ ↑S → NonUnitalStarAlgebra.adjoin R s ≤ S
-- Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
MeasureTheory.Lp.simpleFunc.norm_toLp : ∀ {α : Type u_1} {E : Type u_4} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E] {p : ENNReal}
  {μ : MeasureTheory.Measure α} [inst_2 : Fact (1 ≤ p)] (f : MeasureTheory.SimpleFunc α E)
  (hf : MeasureTheory.MemLp (⇑f) p μ), ‖f.toLp hf‖ = (MeasureTheory.eLpNorm (⇑f) p μ).toReal
-- Mathlib.SetTheory.Ordinal.FundamentalSequence
Ordinal.IsFundamentalSeq.iSup_add_one_eq : ∀ {a o : Ordinal.{u_1}} {f : ↑(Set.Iio a) → ↑(Set.Iio o)}, Ordinal.IsFundamentalSeq f → ⨆ i, ↑(f i) + 1 = o
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw.foldRev_cons_value : ∀ {α : Type u} {β : Type v} {l : Std.DHashMap.Raw α fun x => β} {acc : List β},
  Std.DHashMap.Raw.Internal.foldRev (fun acc x v => v :: acc) acc l =
    Std.Internal.List.values (Std.DHashMap.Internal.toListModel l.buckets) ++ acc
-- Mathlib.NumberTheory.ModularForms.QExpansion
UpperHalfPlane.qExpansion_eq_zero_iff : ∀ {h : ℝ} {f : UpperHalfPlane → ℂ},
  0 < h →
    Function.Periodic (f ∘ ↑UpperHalfPlane.ofComplex) ↑h →
      MDiff f → UpperHalfPlane.IsBoundedAtImInfty f → (UpperHalfPlane.qExpansion h f = 0 ↔ f = 0)
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
BoundedContinuousFunction.nnnorm_eq_iSup_nnnorm : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : SeminormedAddCommGroup β]
  (f : BoundedContinuousFunction α β), ‖f‖₊ = ⨆ x, ‖f x‖₊
-- Mathlib.LinearAlgebra.FreeModule.PID
/-- If `M` is finite free over a PID `R`, then for any submodule `N` of the same rank,
we can find basis for `M` and `N` with the same indexing such that the inclusion map
is a square diagonal matrix; this is the basis for `M`. See:
* `Submodule.smithNormalFormBotBasis` for the basis on `N`,
* `Submodule.smithNormalFormCoeffs` for the entries of the diagonal matrix
* `Submodule.smithNormalFormBotBasis_def` for the proof that the inclusion map
  forms a square diagonal matrix.
 -/
Submodule.smithNormalFormTopBasis : {ι : Type u_1} →
  {R : Type u_2} →
    [inst : CommRing R] →
      {M : Type u_3} →
        [inst_1 : AddCommGroup M] →
          [inst_2 : Module R M] →
            [IsDomain R] →
              [IsPrincipalIdealRing R] →
                {N : Submodule R M} →
                  [Finite ι] → Module.Basis ι R M → Module.finrank R ↥N = Module.finrank R M → Module.Basis ι R M