mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.ContinuousOn
ContinuousWithinAt.fst : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : TopologicalSpace γ] {f : α → β × γ} {s : Set α} {a : α},
  ContinuousWithinAt f s a → ContinuousWithinAt (fun x => (f x).1) s a
-- Mathlib.Probability.Moments.Covariance
ProbabilityTheory.covariance_zero_measure : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X Y : Ω → ℝ}, ProbabilityTheory.covariance X Y 0 = 0
-- Mathlib.RingTheory.Ideal.Quotient.Basic
Ideal.Quotient.isScalarTower_right : ∀ {R : Type u_3} [inst : Ring R] {I : Ideal R} [inst_1 : I.IsTwoSided] {α : Type u_5} [inst_2 : SMul α R]
  [inst_3 : IsScalarTower α R R], IsScalarTower α (R ⧸ I) (R ⧸ I)
-- Mathlib.Geometry.Manifold.VectorField.LieBracket
Filter.EventuallyEq.mlieBracket_vectorField : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {x : M} {V W V₁ W₁ : (x : M) → TangentSpace I x},
  V₁ =ᶠ[nhds x] V → W₁ =ᶠ[nhds x] W → VectorField.mlieBracket I V₁ W₁ =ᶠ[nhds x] VectorField.mlieBracket I V W
-- Mathlib.RingTheory.MvPowerSeries.LexOrder
MvPowerSeries.lexOrder_le_of_coeff_ne_zero : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] [inst_1 : LinearOrder σ] [inst_2 : WellFoundedGT σ]
  {φ : MvPowerSeries σ R} {d : σ →₀ ℕ}, (MvPowerSeries.coeff d) φ ≠ 0 → φ.lexOrder ≤ ↑(toLex d)
-- Mathlib.Combinatorics.SimpleGraph.Acyclic
_private.Mathlib.Combinatorics.SimpleGraph.Acyclic.0.SimpleGraph.Walk.length.match_1.splitter : {V : Type u_1} →
  {G : SimpleGraph V} →
    {u : V} →
      (motive : (v : V) → G.Walk u v → Sort u_2) →
        (v : V) →
          (x : G.Walk u v) →
            (Unit → motive u SimpleGraph.Walk.nil) →
              ((v v_1 : V) → (h : G.Adj u v_1) → (q : G.Walk v_1 v) → motive v (SimpleGraph.Walk.cons h q)) → motive v x
-- Mathlib.Geometry.Convex.Cone.Basic
ConvexCone.Flat.eq_1 : ∀ {R : Type u_2} {G : Type u_3} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup G]
  [inst_3 : SMul R G] (C : ConvexCone R G), C.Flat = ∃ x ∈ C, x ≠ 0 ∧ -x ∈ C
-- Init.Data.SInt.Lemmas
Int16.toInt32_le : ∀ {a b : Int16}, a.toInt32 ≤ b.toInt32 ↔ a ≤ b
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
LinearMap.toMatrix₂.eq_1 : ∀ {R : Type u_1} {M₁ : Type u_6} {M₂ : Type u_7} {N₂ : Type u_10} {n : Type u_11} {m : Type u_12}
  [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁] [inst_2 : Module R M₁] [inst_3 : AddCommMonoid M₂]
  [inst_4 : Module R M₂] [inst_5 : AddCommMonoid N₂] [inst_6 : Module R N₂] {σ₁ σ₂ : R →+* R} [inst_7 : Fintype n]
  [inst_8 : Fintype m] [inst_9 : DecidableEq m] [inst_10 : DecidableEq n] (b₁ : Module.Basis n R M₁)
  (b₂ : Module.Basis m R M₂),
  LinearMap.toMatrix₂ b₁ b₂ =
    (b₁.equivFun.arrowCongr (b₂.equivFun.arrowCongr (LinearEquiv.refl R N₂))).trans (LinearMap.toMatrixₛₗ₂' R)
-- Mathlib.Algebra.Polynomial.Degree.Lemmas
Polynomial.natDegree_le_iff_coeff_eq_zero : ∀ {R : Type u} {n : ℕ} [inst : Semiring R] {p : Polynomial R}, p.natDegree ≤ n ↔ ∀ (N : ℕ), n < N → p.coeff N = 0
-- Mathlib.Combinatorics.Quiver.Path.Vertices
Quiver.Path.vertices_comp : ∀ {V : Type u_1} [inst : Quiver V] {a b c : V} (p : Quiver.Path a b) (q : Quiver.Path b c),
  (p.comp q).vertices = p.vertices.dropLast ++ q.vertices
-- Mathlib.Order.Filter.Defs
Filter.sInf.eq_1 : ∀ {α : Type u_1} (s : Set (Filter α)), Filter.sInf s = sSup (lowerBounds s)
-- Mathlib.Topology.Order.Monotone
AntitoneOn.tendsto_nhdsLT : ∀ {α : Type u_3} {β : Type u_4} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α]
  [inst_3 : ConditionallyCompleteLinearOrder β] [inst_4 : TopologicalSpace β] [OrderTopology β] {f : α → β} {x : α},
  AntitoneOn f (Set.Iio x) →
    BddBelow (f '' Set.Iio x) → Filter.Tendsto f (nhdsWithin x (Set.Iio x)) (nhds (sInf (f '' Set.Iio x)))
-- Mathlib.MeasureTheory.Group.Prod
/-- The map `(x, y) ↦ (x, y - x)` is measure-preserving.  -/
MeasureTheory.measurePreserving_prod_sub : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : AddGroup G] [MeasurableAdd₂ G] (μ ν : MeasureTheory.Measure G)
  [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] [MeasurableNeg G] [ν.IsAddRightInvariant],
  MeasureTheory.MeasurePreserving (fun z => (z.1, z.2 - z.1)) (μ.prod ν) (μ.prod ν)
-- Init.Data.String.Subslice
/-- The subslice is not degenerate \(but it may be empty\).  -/
String.Slice.Subslice.startInclusive_le_endExclusive : ∀ {s : String.Slice} (self : s.Subslice), self.startInclusive ≤ self.endExclusive
-- Init.GrindInstances.Ring.UInt
/-- Variant of `UInt8.ofNat_mod_size` replacing `2 ^ 8` with `256`. -/
UInt8.ofNat_mod_size' : ∀ {x : ℕ}, UInt8.ofNat (x % 256) = UInt8.ofNat x
-- Aesop.Script.Tactic
Aesop.Script.Tactic.uTactic : Aesop.Script.Tactic → Aesop.Script.UTactic
-- Mathlib.Order.Lattice
sup_lt_iff : ∀ {α : Type u} [inst : LinearOrder α] {a b c : α}, max b c < a ↔ b < a ∧ c < a
-- Mathlib.Topology.MetricSpace.Congruence
/-- A congruence preserves distance. Forward direction of `congruent_iff_dist_eq`.  -/
Congruent.dist_eq : ∀ {ι : Type u_1} {P₁ : Type u_3} {P₂ : Type u_4} {v₁ : ι → P₁} {v₂ : ι → P₂} [inst : PseudoMetricSpace P₁]
  [inst_1 : PseudoMetricSpace P₂], Congruent v₁ v₂ → ∀ (i₁ i₂ : ι), dist (v₁ i₁) (v₁ i₂) = dist (v₂ i₁) (v₂ i₂)
-- Std.Data.DTreeMap.Internal.Cell
/-- The mapping.  -/
Std.DTreeMap.Internal.Cell.inner : {α : Type u} →
  [inst : Ord α] → {β : α → Type v} → {k : α → Ordering} → Std.DTreeMap.Internal.Cell α β k → Option ((a : α) × β a)
-- Mathlib.Algebra.Lie.Solvable
LieAlgebra.derivedSeries_of_bot_eq_bot : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (k : ℕ),
  LieAlgebra.derivedSeriesOfIdeal R L k ⊥ = ⊥
-- Mathlib.Probability.Kernel.Disintegration.Unique
/-- Auxiliary lemma for `eq_condKernel_of_measure_eq_compProd`.
Uniqueness of the disintegration kernel on ℝ.  -/
ProbabilityTheory.eq_condKernel_of_measure_eq_compProd_real : ∀ {α : Type u_1} {mα : MeasurableSpace α} {ρ : MeasureTheory.Measure (α × ℝ)} [inst : MeasureTheory.IsFiniteMeasure ρ]
  (κ : ProbabilityTheory.Kernel α ℝ) [ProbabilityTheory.IsFiniteKernel κ],
  ρ = ρ.fst.compProd κ → ∀ᵐ (x : α) ∂ρ.fst, κ x = ρ.condKernel x
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.Code.return.injEq : ∀ (ref val ref_1 val_1 : Lean.Syntax),
  (Lean.Elab.Term.Do.Code.return ref val = Lean.Elab.Term.Do.Code.return ref_1 val_1) = (ref = ref_1 ∧ val = val_1)
-- Mathlib.ModelTheory.Complexity
FirstOrder.Language.BoundedFormula.toPrenex.eq_def : ∀ {L : FirstOrder.Language} {α : Type u'} (x : ℕ) (x_1 : L.BoundedFormula α x),
  x_1.toPrenex =
    match x, x_1 with
    | x, FirstOrder.Language.BoundedFormula.falsum => ⊥
    | x, FirstOrder.Language.BoundedFormula.equal t₁ t₂ => t₁.bdEqual t₂
    | x, FirstOrder.Language.BoundedFormula.rel R ts => FirstOrder.Language.BoundedFormula.rel R ts
    | x, f₁.imp f₂ => f₁.toPrenex.toPrenexImp f₂.toPrenex
    | x, f.all => f.toPrenex.all
-- Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
RestrictedProduct.instContinuousConstSMulCoe : ∀ {ι : Type u_1} (R : ι → Type u_2) {S : ι → Type u_3} [inst : (i : ι) → SetLike (S i) (R i)] {B : (i : ι) → S i}
  {𝓕 : Filter ι} [inst_1 : (i : ι) → TopologicalSpace (R i)] {G : Type u_4} [inst_2 : (i : ι) → SMul G (R i)]
  [inst_3 : ∀ (i : ι), SMulMemClass (S i) G (R i)] [∀ (i : ι), ContinuousConstSMul G (R i)],
  ContinuousConstSMul G (RestrictedProduct (fun i => R i) (fun i => ↑(B i)) 𝓕)
-- Mathlib.Algebra.Group.Pi.Units
MulEquiv.val_inv_piUnits_apply : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] (f : ((i : ι) → M i)ˣ) (i : ι),
  ↑(MulEquiv.piUnits f i)⁻¹ = f.inv i
-- Mathlib.AlgebraicTopology.SimplicialSet.Basic
SSet.σ_comp_σ_apply : ∀ {S : SSet} {n : ℕ} {i j : Fin (n + 1)},
  i ≤ j →
    ∀ (x : S.obj (Opposite.op { len := n })),
      (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.σ S i.castSucc))
          ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.σ S j)) x) =
        (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.σ S j.succ))
          ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.σ S i)) x)
-- Mathlib.Order.Filter.SmallSets
Filter.HasBasis.frequently_smallSets : ∀ {α : Type u_4} {ι : Sort u_5} {p : ι → Prop} {l : Filter α} {s : ι → Set α} {q : Set α → Prop} {hl : l.HasBasis p s},
  (∀ ⦃s t : Set α⦄, s ⊆ t → q s → q t) → ((∃ᶠ (s : Set α) in l.smallSets, q s) ↔ ∀ (i : ι), p i → q (s i))
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat.0.Nat.NatOffset.offset.sizeOf_spec : ∀ (e o : Lean.Expr) (n : ℕ), sizeOf (Nat.NatOffset.offset✝ e o n) = 1 + sizeOf e + sizeOf o + sizeOf n
-- Mathlib.Algebra.Module.LocalizedModule.Basic
IsLocalizedModule.instLiftOfLE : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {M₁ : Type u_6}
  {M₂ : Type u_7} [inst_3 : AddCommMonoid M₁] [inst_4 : AddCommMonoid M₂] [inst_5 : Module R M₁] [inst_6 : Module R M₂]
  (S₁ S₂ : Submonoid R) (h : S₁ ≤ S₂) (f₁ : M →ₗ[R] M₁) (f₂ : M →ₗ[R] M₂) [inst_7 : IsLocalizedModule S₁ f₁]
  [inst_8 : IsLocalizedModule S₂ f₂], IsLocalizedModule S₂ (IsLocalizedModule.liftOfLE S₁ S₂ h f₁ f₂)
-- Mathlib.CategoryTheory.Limits.VanKampen
CategoryTheory.IsVanKampenColimit.mapCocone_iff : ∀ {J : Type v'} [inst : CategoryTheory.Category.{u', v'} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {D : Type u_2} [inst_2 : CategoryTheory.Category.{v_2, u_2} D] (G : CategoryTheory.Functor C D)
  {F : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cocone F} [G.IsEquivalence],
  CategoryTheory.IsVanKampenColimit (G.mapCocone c) ↔ CategoryTheory.IsVanKampenColimit c
-- Mathlib.CategoryTheory.Preadditive.FreydCategory.RightFreyd
/-- The category `RightFreyd V` has all cokernels if `V` has binary biproducts.  -/
CategoryTheory.Preadditive.RightFreyd.instHasCokernels : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] [inst_1 : CategoryTheory.Preadditive V]
  [CategoryTheory.Limits.HasBinaryBiproducts V],
  CategoryTheory.Limits.HasCokernels (CategoryTheory.Preadditive.RightFreyd V)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.maxKeyD_erase_eq_iff_not_compare_maxKeyD_eq : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h : t.WF)
  {k fallback : α},
  (Std.DTreeMap.Internal.Impl.erase k t ⋯).impl.isEmpty = false →
    ((Std.DTreeMap.Internal.Impl.erase k t ⋯).impl.maxKeyD fallback = t.maxKeyD fallback ↔
      ¬compare k (t.maxKeyD fallback) = Ordering.eq)
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
CategoryTheory.section_comp_left_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A B : C} (f g : A ⟶ B)
  [inst_1 : CategoryTheory.IsReflexivePair f g] {Z : C} (h : B ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.commonSection f g) (CategoryTheory.CategoryStruct.comp f h) = h
-- Mathlib.Algebra.Order.Archimedean.Class
MulArchimedeanClass.mk_le_mk_iff_lt : ∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M] {a b : M},
  a ≠ 1 → (MulArchimedeanClass.mk a ≤ MulArchimedeanClass.mk b ↔ ∃ n, |b|ₘ < |a|ₘ ^ n)
-- Std.Http.Data.Headers.Basic
Std.Http.Header.TransferEncoding.mk.sizeOf_spec : ∀ (codings : Array String) (isValid : Std.Http.Header.TransferEncoding.Validate codings = true),
  sizeOf { codings := codings, isValid := isValid } = 1 + sizeOf codings + sizeOf isValid
-- Lean.Meta.Constructions.NoConfusion
/-- Constructs a lambda expression that returns the argument to the `noConfusion` principle for a given
constructor. In particular, returns
```
fun params x1 x2 x3 x1' x2' x3' => (x1 = x1' → x2 = x2' → x3 = x3' → P)
```
where `x1 x2 x3` and `x1' x2' x3'` are the parameters and  fields of a constructor application of
`ctorName`, omitting equalities between propositions and using `HEq` where needed.
 -/
_private.Lean.Meta.Constructions.NoConfusion.0.Lean.mkNoConfusionCtorArg : Lean.Name → Lean.Expr → Lean.MetaM Lean.Expr
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCast?_filter_not_contains_map_fst_of_containsKey_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {l₁ l₂ : List ((a : α) × β a)} {k : α},
  Std.Internal.List.DistinctKeys l₁ →
    Std.Internal.List.containsKey k l₂ = true →
      Std.Internal.List.getValueCast? k (List.filter (fun p => !(List.map Sigma.fst l₂).contains p.fst) l₁) = none
-- Mathlib.GroupTheory.ArchimedeanDensely
instFintypeAddEquivInt : Fintype (ℤ ≃+ ℤ)
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.triangleMorphismId_hom₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  (T : CategoryTheory.Pretriangulated.Triangle C),
  (CategoryTheory.Pretriangulated.triangleMorphismId T).hom₃ = CategoryTheory.CategoryStruct.id T.obj₃
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
AlgebraicGeometry.LocallyRingedSpace.stalkSpecializes_stalkMap_assoc : ∀ {X Y : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Y) (x x' : ↑X.toTopCat) (h : x ⤳ x') {Z : CommRingCat}
  (h_1 : X.presheaf.stalk x ⟶ Z),
  CategoryTheory.CategoryStruct.comp (Y.presheaf.stalkSpecializes ⋯)
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap f x) h_1) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap f x')
      (CategoryTheory.CategoryStruct.comp (X.presheaf.stalkSpecializes h) h_1)
-- Mathlib.FieldTheory.RatFunc.Luroth
_private.Mathlib.FieldTheory.RatFunc.Luroth.0.RatFunc.Luroth.Q₀_mem_lifts : ∀ {K : Type u_1} [inst : Field K] {E : IntermediateField K (RatFunc K)},
  E ≠ ⊥ → RatFunc.Luroth.Q₀✝ E ∈ Polynomial.lifts (algebraMap (Polynomial K) (RatFunc K))
-- Mathlib.Algebra.Group.Submonoid.Defs
/-- The natural monoid hom from an `AddSubmonoid` of `AddMonoid` `M` to `M`.  -/
AddSubmonoid.subtype : {M : Type u_4} → [inst : AddZeroClass M] → (S : AddSubmonoid M) → ↥S →+ M
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.iUnion_op_smul_set : ∀ {α : Type u_2} [inst : Mul α] (s t : Set α), ⋃ a ∈ t, MulOpposite.op a • s = s * t
-- Std.Time.Format
/-- The RFC822 format, which follows the pattern `eee, dd MMM uuuu HH:mm:ss ZZZ`.
This format is used in email headers and HTTP headers.
 -/
Std.Time.Formats.rfc822 : Std.Time.GenericFormat Std.Time.Awareness.any
-- Mathlib.MeasureTheory.Function.SpecialFunctions.RCLike
AEMeasurable.im : ∀ {α : Type u_1} {𝕜 : Type u_2} [inst : RCLike 𝕜] {m : MeasurableSpace α} {f : α → 𝕜} {μ : MeasureTheory.Measure α},
  AEMeasurable f μ → AEMeasurable (fun x => RCLike.im (f x)) μ
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get_insertMany_list : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [inst : Std.TransOrd α]
  [inst_1 : BEq α] [inst_2 : Std.LawfulBEqOrd α] (h : t.WF) {l : List (α × β)} {k : α}
  (h' : Std.DTreeMap.Internal.Impl.contains k ↑(Std.DTreeMap.Internal.Impl.Const.insertMany t l ⋯) = true),
  Std.DTreeMap.Internal.Impl.Const.get (↑(Std.DTreeMap.Internal.Impl.Const.insertMany t l ⋯)) k h' =
    match w :
      List.findSomeRev?
        (fun x =>
          match x with
          | (a, b) => if compare a k = Ordering.eq then some b else none)
        l with
    | some v => v
    | none => Std.DTreeMap.Internal.Impl.Const.get t k ⋯
-- Mathlib.Analysis.Calculus.FDeriv.Mul
Differentiable.smul_const : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {𝕜' : Type u_5}
  [inst_5 : NormedRing 𝕜'] [inst_6 : NormedAlgebra 𝕜 𝕜'] [inst_7 : Module 𝕜' F] [IsBoundedSMul 𝕜' F]
  [IsScalarTower 𝕜 𝕜' F] {c : E → 𝕜'}, Differentiable 𝕜 c → ∀ (f : F), Differentiable 𝕜 fun y => c y • f
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
/-- A functor preserving larger limits also preserves smaller limits.  -/
CategoryTheory.Limits.preservesLimitsOfSize_of_univLE : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [UnivLE.{w, w'}] [UnivLE.{w₂, w₂'}]
  [CategoryTheory.Limits.PreservesLimitsOfSize.{w', w₂', v₁, v₂, u₁, u₂} F],
  CategoryTheory.Limits.PreservesLimitsOfSize.{w, w₂, v₁, v₂, u₁, u₂} F
-- Mathlib.Order.KrullDimension
Order.krullDim_eq_one_iff_of_boundedOrder : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : BoundedOrder α], Order.krullDim α = 1 ↔ IsSimpleOrder α
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
cbiSup_eq_ciSup_subtype : ∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompleteLattice α] {p : ι → Prop} {f : (i : ι) → p i → α},
  BddAbove (Set.range fun i => f ↑i ⋯) → sSup ∅ ≤ ⨆ i, f ↑i ⋯ → ⨆ i, ⨆ (h : p i), f i h = ⨆ x, f ↑x ⋯
-- Mathlib.Tactic.GCongr.Core
/-- The name of the relation. For example, `a + b ≤ a + c` has ``relName := `LE.le``.  -/
Mathlib.Tactic.GCongr.GCongrKey.relName : Mathlib.Tactic.GCongr.GCongrKey → Lean.Name
-- Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Set.powersetCard.mem_mulActionHom_compl : ∀ (G : Type u_1) [inst : Group G] (α : Type u_2) [inst_1 : MulAction G α] {n : ℕ} [inst_2 : DecidableEq α]
  [inst_3 : Fintype α] {m : ℕ} {hm : m + n = Fintype.card α} {s : ↑(Set.powersetCard α n)} {a : α},
  a ∈ (Set.powersetCard.mulActionHom_compl G α hm) s ↔ a ∉ s
-- Mathlib.LinearAlgebra.Matrix.Adjugate
Matrix.adjugate_fin_one : ∀ {α : Type w} [inst : CommRing α] (A : Matrix (Fin 1) (Fin 1) α), A.adjugate = 1
-- Mathlib.Topology.VectorBundle.Hom
/-- Consider a `C^n` map `v : M → E₁` to a vector bundle, over a basemap `b : M → B`, and
linear maps `ϕ m : E₁ (b m) → E₂ (b m)` depending smoothly on `m`.
One can apply `ϕ m` to `v m`, and the resulting map is `C^n`.  -/
Continuous.clm_bundle_apply : ∀ {𝕜 : Type u_8} {B : Type u_9} {F₁ : Type u_10} {F₂ : Type u_11} {M : Type u_13} [inst : NontriviallyNormedField 𝕜]
  {E₁ : B → Type u_14} [inst_1 : (x : B) → AddCommGroup (E₁ x)] [inst_2 : (x : B) → Module 𝕜 (E₁ x)]
  [inst_3 : NormedAddCommGroup F₁] [inst_4 : NormedSpace 𝕜 F₁] [inst_5 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)]
  [inst_6 : (x : B) → TopologicalSpace (E₁ x)] {E₂ : B → Type u_15} [inst_7 : (x : B) → AddCommGroup (E₂ x)]
  [inst_8 : (x : B) → Module 𝕜 (E₂ x)] [inst_9 : NormedAddCommGroup F₂] [inst_10 : NormedSpace 𝕜 F₂]
  [inst_11 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)] [inst_12 : (x : B) → TopologicalSpace (E₂ x)]
  [inst_13 : TopologicalSpace B] [inst_14 : TopologicalSpace M] [inst_15 : FiberBundle F₁ E₁]
  [inst_16 : VectorBundle 𝕜 F₁ E₁] [inst_17 : FiberBundle F₂ E₂] [inst_18 : VectorBundle 𝕜 F₂ E₂] {b : M → B}
  {v : (x : M) → E₁ (b x)} [inst_19 : ∀ (x : B), IsTopologicalAddGroup (E₂ x)]
  [inst_20 : ∀ (x : B), ContinuousSMul 𝕜 (E₂ x)] {ϕ : (x : M) → E₁ (b x) →L[𝕜] E₂ (b x)},
  (Continuous fun m => ⟨b m, ϕ m⟩) → (Continuous fun m => ⟨b m, v m⟩) → Continuous fun m => ⟨b m, (ϕ m) (v m)⟩
-- Lean.Parser.Term
Lean.Parser.Term.fun.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.contains_eq_isSome_get? : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α] {a : α},
  m.contains a = (m.get? a).isSome
-- Mathlib.Logic.Equiv.Fin.Basic
finSuccEquiv'_succAbove : ∀ {n : ℕ} (i : Fin (n + 1)) (j : Fin n), (finSuccEquiv' i) (i.succAbove j) = some j
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
/-- If two functions coincide on a set `s`, then their iterated differentials within this set
coincide. See also `Filter.EventuallyEq.iteratedFDerivWithin_eq` and
`Filter.EventuallyEq.iteratedFDerivWithin`.  -/
iteratedFDerivWithin_congr : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f f₁ : E → F} {x : E},
  Set.EqOn f₁ f s → x ∈ s → ∀ (n : ℕ), iteratedFDerivWithin 𝕜 n f₁ s x = iteratedFDerivWithin 𝕜 n f s x
-- Lean.Environment
Lean.instReprOLeanLevel : Repr Lean.OLeanLevel
-- Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric
Complex.regularizedHGFunCoeff.eq_1 : ∀ (a b : Multiset ℂ) (n : ℕ),
  Complex.regularizedHGFunCoeff a b n =
    (Multiset.map (fun x => Polynomial.eval x (ascPochhammer ℂ n)) a).prod /
      (↑n.factorial * (Multiset.map (fun x => Complex.Gamma (x + ↑n)) b).prod)
-- Mathlib.Algebra.QuaternionBasis
QuaternionAlgebra.Basis.lift.eq_1 : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] {c₁ c₂ c₃ : R}
  (q : QuaternionAlgebra.Basis A c₁ c₂ c₃) (x : QuaternionAlgebra R c₁ c₂ c₃),
  q.lift x = (algebraMap R A) x.re + x.imI • q.i + x.imJ • q.j + x.imK • q.k
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
/-- Up to `Scheme.Modules.overEquiv`, `SheafOfModules.overFunctor` is isomorphic to
`Scheme.Modules.restrictFunctor`.  -/
AlgebraicGeometry.Scheme.Modules.overFunctorEquiv : {X : AlgebraicGeometry.Scheme} →
  (U : X.Opens) →
    (SheafOfModules.overFunctor X.ringCatSheaf U).comp (AlgebraicGeometry.Scheme.Modules.overEquiv U).functor ≅
      AlgebraicGeometry.Scheme.Modules.restrictFunctor U.ι
-- Mathlib.CategoryTheory.MorphismProperty.LiftingProperty
CategoryTheory.MorphismProperty.rlp_isMultiplicative : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (T : CategoryTheory.MorphismProperty C), T.rlp.IsMultiplicative
-- Mathlib.Topology.Order.LocalExtr
IsLocalMax.comp_mono : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : TopologicalSpace α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  {f : α → β} {a : α}, IsLocalMax f a → ∀ {g : β → γ}, Monotone g → IsLocalMax (g ∘ f) a
-- Init.Data.List.Sort.Impl
_private.Init.Data.List.Sort.Impl.0.List.MergeSort.Internal.mergeTR.go.eq_3 : ∀ {α : Type u_1} (le : α → α → Bool) (a : List α) (x_3 : α) (xs : List α) (y : α) (ys : List α),
  List.MergeSort.Internal.mergeTR.go✝ le (x_3 :: xs) (y :: ys) a =
    if le x_3 y = true then List.MergeSort.Internal.mergeTR.go✝ le xs (y :: ys) (x_3 :: a)
    else List.MergeSort.Internal.mergeTR.go✝ le (x_3 :: xs) ys (y :: a)
-- Mathlib.Algebra.ContinuedFractions.Basic
/-- Maps a function `f` on both components of a given pair.  -/
GenContFract.Pair.map : {α : Type u_1} → {β : Type u_2} → (α → β) → GenContFract.Pair α → GenContFract.Pair β
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.contains_ofList : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] [inst : BEq α] [Std.LawfulBEqCmp cmp]
  {l : List (α × β)} {k : α}, (Std.TreeMap.ofList l cmp).contains k = (List.map Prod.fst l).contains k
-- Mathlib.Algebra.Category.CommHopfAlgCat
CommHopfAlgCat.hom_comp : ∀ {R : Type u} [inst : CommRing R] {A B C : CommHopfAlgCat R} (f : A ⟶ B) (g : B ⟶ C),
  CommHopfAlgCat.Hom.hom (CategoryTheory.CategoryStruct.comp f g) =
    (CommHopfAlgCat.Hom.hom g).comp (CommHopfAlgCat.Hom.hom f)
-- Lean.Meta.Tactic.Grind.AC.Types
/-- Cached `getLevel type`  -/
Lean.Meta.Grind.AC.Struct.u : Lean.Meta.Grind.AC.Struct → Lean.Level
-- Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
CategoryTheory.ObjectProperty.prop_prod : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C)
  [P.IsClosedUnderBinaryProducts] (X Y : C) [inst_2 : CategoryTheory.Limits.HasBinaryProduct X Y], P X → P Y → P (X ⨯ Y)
-- Mathlib.Data.List.Intervals
List.Ico.zero_bot : ∀ (n : ℕ), List.Ico 0 n = List.range n
-- Mathlib.RingTheory.Ideal.Span
Ideal.mem_span_range_self : ∀ {α : Type u} [inst : Semiring α] {β : Type u_1} {f : β → α} {x : β}, f x ∈ Ideal.span (Set.range f)