mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.Order.Group
/-- In a nontrivial densely linearly ordered commutative group,
the integer powers of an element can't be dense.  -/
not_denseRange_zpow : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : CommGroup G] [inst_2 : LinearOrder G] [IsOrderedMonoid G]
  [OrderTopology G] [Nontrivial G] [DenselyOrdered G] {a : G}, ¬DenseRange fun x => a ^ x
-- Mathlib.Order.CompleteLattice.PiLex
Pi.Lex.le_sInf_apply : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : LinearOrder ι] [inst_1 : (i : ι) → CompleteLinearOrder (α i)]
  [inst_2 : WellFoundedLT ι] {s : Set (Lex ((i : ι) → (fun i => α i) i))} {i : ι}
  {e : Lex ((i : ι) → (fun i => α i) i)}, (∀ f ∈ s, (∀ j < i, f j = sInf s j) → e i ≤ f i) → e i ≤ sInf s i
-- Mathlib.Algebra.Category.Semigrp.Basic
AddSemigrp.ofHom_id : ∀ {X : Type u} [inst : AddSemigroup X],
  AddSemigrp.ofHom (AddHom.id X) = CategoryTheory.CategoryStruct.id (AddSemigrp.of X)
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
/-- The limit bicone for the biproduct over an index type with exactly one term.  -/
CategoryTheory.Limits.limitBiconeOfUnique : {J : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
        [Unique J] → (f : J → C) → CategoryTheory.Limits.LimitBicone f
-- Init.ShareCommon
ShareCommonM.run : {σ : ShareCommon.StateFactory} → {α : Type u_1} → ShareCommonM σ α → α
-- Mathlib.Algebra.Category.MonCat.FilteredColimits
/-- Multiplication in the colimit is well-defined in the left argument.  -/
MonCat.FilteredColimits.colimitMulAux_eq_of_rel_left : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J MonCat)
  [inst_1 : CategoryTheory.IsFiltered J] {x x' y : (j : J) × ↑(F.obj j)},
  CategoryTheory.Limits.Types.FilteredColimit.Rel (F.comp (CategoryTheory.forget MonCat)) x x' →
    MonCat.FilteredColimits.colimitMulAux F x y = MonCat.FilteredColimits.colimitMulAux F x' y
-- Mathlib.Order.Filter.Lift
Filter.lift'_inf_principal_eq : ∀ {α : Type u_1} {β : Type u_2} {f : Filter α} {h : Set α → Set β} {s : Set β},
  f.lift' h ⊓ Filter.principal s = f.lift' fun t => h t ∩ s
-- Mathlib.Topology.ContinuousMap.ContinuousMapZero
/-- The coercion `C(X, R)₀ → C(X, R)` bundled as a non-unital star algebra homomorphism.  -/
ContinuousMapZero.toContinuousMapHom : {X : Type u_1} →
  {R : Type u_2} →
    [inst : Zero X] →
      [inst_1 : TopologicalSpace X] →
        [inst_2 : TopologicalSpace R] →
          [inst_3 : CommSemiring R] →
            [inst_4 : IsTopologicalSemiring R] →
              [inst_5 : StarRing R] → [inst_6 : ContinuousStar R] → ContinuousMapZero X R →⋆ₙₐ[R] C(X, R)
-- Mathlib.Data.Ordmap.Ordset
_private.Mathlib.Data.Ordmap.Ordset.0.Ordnode.mem.match_1.eq_1 : ∀ (motive : Ordering → Sort u_1) (h_1 : Unit → motive Ordering.lt) (h_2 : Unit → motive Ordering.eq)
  (h_3 : Unit → motive Ordering.gt),
  (match Ordering.lt with
    | Ordering.lt => h_1 ()
    | Ordering.eq => h_2 ()
    | Ordering.gt => h_3 ()) =
    h_1 ()
-- Mathlib.SetTheory.Ordinal.FixedPointApproximants
OrdinalApprox.lfpApprox_of_isSuccLimit : ∀ {α : Type u} [inst : CompleteLattice α] (f : α →o α) {x : α} {a : Ordinal.{u}},
  Order.IsSuccLimit a → OrdinalApprox.lfpApprox f x a = ⨆ b, OrdinalApprox.lfpApprox f x ↑b
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKeyD_maxKey : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp]
  {he : t.isEmpty = false} {fallback : α}, t.getKeyD (t.maxKey he) fallback = t.maxKey he
-- Mathlib.Topology.Bases
TopologicalSpace.encodableCountableBasis : (α : Type u) →
  [t : TopologicalSpace α] → [inst : SecondCountableTopology α] → Encodable ↑(TopologicalSpace.countableBasis α)
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Mathlib.Meta.NormNum.IsNat.rpow_eq_pow : ∀ {b : ℝ} {n : ℕ}, Mathlib.Meta.NormNum.IsNat b n → ∀ (a : ℝ), a ^ b = a ^ n
-- Mathlib.Tactic.CategoryTheory.MonoidalComp
CategoryTheory.MonoidalCoherence.whiskerLeft : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      (X Y Z : C) →
        [CategoryTheory.MonoidalCoherence Y Z] →
          CategoryTheory.MonoidalCoherence (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)
            (CategoryTheory.MonoidalCategoryStruct.tensorObj X Z)
-- Init.Data.Int.Linear
Int.Internal.Linear.cooper_dvd_left_split_dvd2 : ∀ (ctx : Int.Internal.Linear.Context) (p₁ p₂ p₃ : Int.Internal.Linear.Poly) (d : ℤ) (k : ℕ) (d' : ℤ)
  (p' : Int.Internal.Linear.Poly),
  Int.Internal.Linear.cooper_dvd_left_split ctx p₁ p₂ p₃ d k →
    Int.Internal.Linear.cooper_dvd_left_split_dvd2_cert p₁ p₃ d k d' p' = true →
      d' ∣ Int.Internal.Linear.Poly.denote' ctx p'
-- Mathlib.Analysis.Normed.Operator.Asymptotics
ContinuousLinearMap.isBigOWith_sub : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [inst : SeminormedAddCommGroup E]
  [inst_1 : SeminormedAddCommGroup F] [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] (f : E →SL[σ₁₂] F)
  (l : Filter E) (x : E), Asymptotics.IsBigOWith ‖f‖ l (fun x' => f (x' - x)) fun x' => x' - x
-- Mathlib.Data.ENNReal.Real
ENNReal.ofReal_lt_coe_iff : ∀ {a : ℝ} {b : NNReal}, 0 ≤ a → (ENNReal.ofReal a < ↑b ↔ a < ↑b)
-- Mathlib.RingTheory.Valuation.Basic
/-- `comap` preserves equivalence.  -/
AddValuation.IsEquiv.comap : ∀ {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [inst : LinearOrderedAddCommMonoidWithTop Γ₀]
  [inst_1 : LinearOrderedAddCommMonoidWithTop Γ'₀] [inst_2 : Ring R] {v₁ : AddValuation R Γ₀} {v₂ : AddValuation R Γ'₀}
  {S : Type u_7} [inst_3 : Ring S] (f : S →+* R),
  v₁.IsEquiv v₂ → (AddValuation.comap f v₁).IsEquiv (AddValuation.comap f v₂)
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
/-- `toFun` is the same as the result of coercing to a function.  -/
AffineMap.toFun_eq_coe : ∀ {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [inst : Ring k]
  [inst_1 : AddCommGroup V1] [inst_2 : Module k V1] [inst_3 : AddTorsor V1 P1] [inst_4 : AddCommGroup V2]
  [inst_5 : Module k V2] [inst_6 : AddTorsor V2 P2] (f : P1 →ᵃ[k] P2), f.toFun = ⇑f
-- Mathlib.Algebra.BigOperators.Group.List.Basic
List.prod_hom₂ : ∀ {ι : Type u_1} {M : Type u_4} {N : Type u_5} {P : Type u_6} [inst : Monoid M] [inst_1 : Monoid N] [inst_2 : Monoid P]
  (l : List ι) (f : M → N → P),
  (∀ (a b : M) (c d : N), f (a * b) (c * d) = f a c * f b d) →
    f 1 1 = 1 →
      ∀ (f₁ : ι → M) (f₂ : ι → N),
        (List.map (fun i => f (f₁ i) (f₂ i)) l).prod = f (List.map f₁ l).prod (List.map f₂ l).prod
-- Mathlib.Data.Set.Prod
Set.Disjoint.set_pi : ∀ {ι : Type u_1} {α : ι → Type u_2} {s : Set ι} {t₁ t₂ : (i : ι) → Set (α i)} {i : ι},
  i ∈ s → Disjoint (t₁ i) (t₂ i) → Disjoint (s.pi t₁) (s.pi t₂)
-- Init.Data.List.OfFn
/-- `ofFnM` on an empty domain is the empty list.  -/
List.ofFnM_zero : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} [inst : Monad m] [LawfulMonad m] {f : Fin 0 → m α}, List.ofFnM f = pure []
-- Mathlib.RingTheory.WittVector.IsPoly
WittVector.onePoly.eq_1 : ∀ (n : ℕ), WittVector.onePoly n = if n = 0 then 1 else 0
-- Mathlib.CategoryTheory.ConcreteCategory.EpiMono
CategoryTheory.ConcreteCategory.surjective_le_epimorphisms : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type w}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC],
  CategoryTheory.MorphismProperty.surjective C ≤ CategoryTheory.MorphismProperty.epimorphisms C
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
CategoryTheory.Bicategory.Adj.whiskerRight_τl : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : CategoryTheory.Bicategory.Adj B} {f g : a ⟶ b} (x : f ⟶ g)
  (β : b ⟶ c), (CategoryTheory.Bicategory.whiskerRight x β).τl = CategoryTheory.Bicategory.whiskerRight x.τl β.l
-- Mathlib.Algebra.Order.Antidiag.FinsuppEquiv
Finset.count_coe_finsuppAntidiagEquiv_apply : ∀ {ι : Type u_1} [inst : DecidableEq ι] {s : Finset ι} (n : ℕ) (f : ↥(s.finsuppAntidiag n)) (a : ↥s),
  Multiset.count a ↑((s.finsuppAntidiagEquiv n) f) = ↑f ↑a
-- Init.System.IO
instMonadAttachEIO : {ε : Type} → MonadAttach (EIO ε)
-- Mathlib.Algebra.MonoidAlgebra.Defs
/-- `AddMonoidAlgebra.single` as an `AddMonoidHom`.

TODO: Rename to `singleAddMonoidHom`.  -/
AddMonoidAlgebra.singleAddHom : {R : Type u_1} → {M : Type u_4} → [inst : Semiring R] → M → R →+ AddMonoidAlgebra R M
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
/-- The group homomorphism mapping a nonsingular affine point `(x, y)` of a Weierstrass curve `W` to
the class of the non-zero fractional ideal `⟨X - x, Y - y⟩` in the ideal class group of `F[W]`.  -/
WeierstrassCurve.Affine.Point.toClass : {F : Type u} →
  [inst : Field F] →
    {W : WeierstrassCurve.Affine F} → [inst_1 : DecidableEq F] → W.Point →+ Additive (ClassGroup W.CoordinateRing)
-- Mathlib.FieldTheory.Separable
Polynomial.emultiplicity_le_one_of_separable : ∀ {R : Type u} [inst : CommSemiring R] {p q : Polynomial R}, ¬IsUnit q → p.Separable → emultiplicity q p ≤ 1
-- Lean.Widget.InteractiveGoal
/-- If true, the hypothesis will be removed in the next tactic state.
Only present in tactic-mode goals.  -/
Lean.Widget.InteractiveHypothesisBundle.isRemoved? : Lean.Widget.InteractiveHypothesisBundle → Option Bool
-- Init.Data.Vector.Lemmas
Vector.mem_of_back? : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {a : α}, xs.back? = some a → a ∈ xs
-- Mathlib.Order.SupClosed
InfClosed.prod : ∀ {α : Type u_3} {β : Type u_4} [inst : SemilatticeInf α] [inst_1 : SemilatticeInf β] {s : Set α} {t : Set β},
  InfClosed s → InfClosed t → InfClosed (s ×ˢ t)
-- Mathlib.CategoryTheory.Monoidal.Bimod
Bimod.regular_actRight : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (A : CategoryTheory.Mon C), (Bimod.regular A).actRight = CategoryTheory.MonObj.mul
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKey_le_of_contains : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  (h : t.WF) {k : α} (hc : Std.DTreeMap.Internal.Impl.contains k t = true), (compare (t.minKey ⋯) k).isLE = true
-- Mathlib.MeasureTheory.Function.LpSpace.Indicator
MeasureTheory.indicatorConstLp.eq_1 : ∀ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup E]
  {s : Set α} (p : ENNReal) (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (c : E),
  MeasureTheory.indicatorConstLp p hs hμs c = MeasureTheory.MemLp.toLp (s.indicator fun x => c) ⋯
-- Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
OrderedFinpartition.range_emb_extendMiddle_ne_singleton_zero : ∀ {n : ℕ} (c : OrderedFinpartition n) (i j : Fin c.length), Set.range ((c.extendMiddle i).emb j) ≠ {0}
-- Mathlib.Topology.Algebra.StarSubalgebra
StarSubalgebra.topologicalClosure_coe : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : TopologicalSpace A]
  [inst_3 : Semiring A] [inst_4 : Algebra R A] [inst_5 : StarRing A] [inst_6 : StarModule R A]
  [inst_7 : IsSemitopologicalSemiring A] [inst_8 : ContinuousStar A] (s : StarSubalgebra R A),
  ↑s.topologicalClosure = closure ↑s
-- Mathlib.Topology.OpenPartialHomeomorph.Basic
/-- If an open partial homeomorphism has source and target equal to univ, then it induces a
homeomorphism between the whole spaces, expressed in this definition.  -/
OpenPartialHomeomorph.toHomeomorphOfSourceEqUnivTargetEqUniv : {X : Type u_1} →
  {Y : Type u_3} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] →
        (e : OpenPartialHomeomorph X Y) → e.source = Set.univ → e.target = Set.univ → X ≃ₜ Y
-- Mathlib.CategoryTheory.Filtered.Basic
CategoryTheory.isCofilteredOrEmpty_of_semilatticeInf : ∀ (α : Type u) [inst : SemilatticeInf α], CategoryTheory.IsCofilteredOrEmpty α
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.cokernel.π_desc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  (f : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasCokernel f] {W : C} (k : Y ⟶ W)
  (h : CategoryTheory.CategoryStruct.comp f k = 0),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π f) (CategoryTheory.Limits.cokernel.desc f k h) =
    k
-- Mathlib.Algebra.Order.CauSeq.Completion
CauSeq.Completion.instInhabitedCauchy : {α : Type u_1} →
  [inst : Field α] →
    [inst_1 : LinearOrder α] →
      [inst_2 : IsStrictOrderedRing α] →
        {β : Type u_2} →
          [inst_3 : Ring β] → {abv : β → α} → [inst_4 : IsAbsoluteValue abv] → Inhabited (CauSeq.Completion.Cauchy abv)
-- Mathlib.MeasureTheory.Integral.Average
MeasureTheory.setLAverage_congr : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α} {f : α → ENNReal},
  s =ᵐ[μ] t → ⨍⁻ (x : α) in s, f x ∂μ = ⨍⁻ (x : α) in t, f x ∂μ
-- Mathlib.Algebra.ContinuedFractions.Computation.Translations
Stream'.Seq.get?.eq_1 : ∀ {α : Type u}, Stream'.Seq.get? = Subtype.val
-- Mathlib.Analysis.InnerProductSpace.Rayleigh
ContinuousLinearMap.bddAbove_rayleighQuotient : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (T : E →L[𝕜] E), BddAbove (Set.range fun x => |T.rayleighQuotient x|)
-- Lean.Environment
_private.Lean.Environment.0.Lean.Environment.setMainModule.unsafe_impl_2 : Lean.Environment → NonScalar
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.preAleph_le_aleph : ∀ (o : Ordinal.{u_1}), Cardinal.preAleph o ≤ Cardinal.aleph o
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
WeierstrassCurve.Projective.X_eq_of_equiv : ∀ {R : Type r} [inst : CommRing R] {P Q : Fin 3 → R}, P ≈ Q → P 0 * Q 2 = Q 0 * P 2
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.eq_empty_iff_size_eq_zero : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α], m = ∅ ↔ m.size = 0
-- Init.Data.Sum.Basic
/-- Retrieves the contents from a sum known to be `inr`. -/
Sum.getRight : {α : Type u_1} → {β : Type u_2} → (ab : α ⊕ β) → ab.isRight = true → β
-- Mathlib.Topology.UniformSpace.Cauchy
Filter.Tendsto.cauchy_map : ∀ {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] {l : Filter β} [l.NeBot] {f : β → α} {a : α},
  Filter.Tendsto f l (nhds a) → Cauchy (Filter.map f l)
-- Mathlib.Analysis.Calculus.FDeriv.Add
/-- **Alias** of the reverse direction of `hasFDerivAt_add_const_iff`. -/
HasFDerivAt.add_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] {f : E → F}
  {f' : E →L[𝕜] F} {x : E} (c : F), HasFDerivAt f f' x → HasFDerivAt (fun x => f x + c) f' x
-- Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
alternatingGroup.coe_two_sylow_of_card_eq_four : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α],
  Nat.card α = 4 → ∀ (S : Sylow 2 ↥(alternatingGroup α)), ↑S = {1} ∪ {g | (↑g).cycleType = {2, 2}}
-- Mathlib.SetTheory.Cardinal.ToNat
Cardinal.cast_toNat_of_lt_aleph0 : ∀ {c : Cardinal.{u_1}}, c < Cardinal.aleph0 → ↑(Cardinal.toNat c) = c
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive
CategoryTheory.Localization.Preadditive.neg'_add'_self : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Preadditive C]
  {L : CategoryTheory.Functor C D} (W : CategoryTheory.MorphismProperty C) [inst_3 : L.IsLocalization W]
  [inst_4 : W.HasLeftCalculusOfFractions] {X Y : C} (f : L.obj X ⟶ L.obj Y),
  CategoryTheory.Localization.Preadditive.add' W (CategoryTheory.Localization.Preadditive.neg' W f) f = L.map 0
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.Measure.map_sub_left_eq_self : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : SubtractionMonoid G] [MeasurableAdd G] [MeasurableNeg G]
  (μ : MeasureTheory.Measure G) [μ.IsNegInvariant] [μ.IsAddLeftInvariant] (g : G),
  MeasureTheory.Measure.map (fun t => g - t) μ = μ
-- Mathlib.Order.Filter.Map
Filter.le_seq : ∀ {α : Type u_1} {β : Type u_2} {f : Filter (α → β)} {g : Filter α} {h : Filter β},
  (∀ t ∈ f, ∀ u ∈ g, t.seq u ∈ h) → h ≤ f.seq g
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey!_ofList_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] [inst_1 : BEq α] [Std.LawfulBEqCmp cmp]
  [inst_3 : Inhabited α] {l : List (α × β)} {k : α},
  (List.map Prod.fst l).contains k = false → (Std.ExtTreeMap.ofList l cmp).getKey! k = default
-- Mathlib.RingTheory.Polynomial.Dickson
_private.Mathlib.RingTheory.Polynomial.Dickson.0.Polynomial.dickson.match_1.splitter : (motive : ℕ → Sort u_1) → (x : ℕ) → (Unit → motive 0) → (Unit → motive 1) → ((n : ℕ) → motive n.succ.succ) → motive x
-- Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
/-- The function `n ↦ x log n + log n! - (log x + ... + log (x + n))`, which we will show tends to
`log (Gamma x)` as `n → ∞`.  -/
Real.BohrMollerup.logGammaSeq : ℝ → ℕ → ℝ
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.compMeasurable_mk : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α}
  [inst_1 : TopologicalSpace β] [inst_2 : TopologicalSpace γ] [inst_3 : MeasurableSpace β]
  [inst_4 : TopologicalSpace.PseudoMetrizableSpace β] [inst_5 : BorelSpace β] [inst_6 : MeasurableSpace γ]
  [inst_7 : TopologicalSpace.PseudoMetrizableSpace γ] [inst_8 : OpensMeasurableSpace γ]
  [inst_9 : SecondCountableTopology γ] (g : β → γ) (hg : Measurable g) (f : α → β)
  (hf : MeasureTheory.AEStronglyMeasurable f μ),
  MeasureTheory.AEEqFun.compMeasurable g hg (MeasureTheory.AEEqFun.mk f hf) = MeasureTheory.AEEqFun.mk (g ∘ f) ⋯
-- Std.Data.Internal.List.Associative
Std.Internal.List.containsKey_modifyKey : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] (k k' : α) (f : β k → β k)
  (l : List ((a : α) × β a)),
  Std.Internal.List.containsKey k' (Std.Internal.List.modifyKey k f l) = Std.Internal.List.containsKey k' l
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithInitial.mkCommaMorphism_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  {F G : CategoryTheory.Functor (CategoryTheory.WithInitial C) D} (η : F ⟶ G),
  (CategoryTheory.WithInitial.mkCommaMorphism η).left = η.app CategoryTheory.WithInitial.star
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKeyD_diff_of_not_mem_left : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k fallback : α}, k ∉ m₁ → (m₁ \ m₂).getKeyD k fallback = fallback
-- Mathlib.Algebra.Group.Subsemigroup.Basic
Subsemigroup.closure_univ : ∀ {M : Type u_1} [inst : Mul M], Subsemigroup.closure Set.univ = ⊤
-- Init.Data.String.Lemmas.Slice
String.Slice.beq_eq_decide : ∀ {s t : String.Slice}, (s == t) = decide (s.copy = t.copy)
-- Mathlib.Analysis.SpecialFunctions.Complex.Analytic
/-- `log` is analytic away from nonpositive reals  -/
analyticAt_clog : ∀ {z : ℂ}, z ∈ Complex.slitPlane → AnalyticAt ℂ Complex.log z
-- Lean.Elab.ConfigEval.Types
_private.Lean.Elab.ConfigEval.Types.0.Lean.Elab.ConfigEval.ReflectConfigItems : Type → Type
-- Mathlib.Data.Rat.Lemmas
Rat.sub_den_dvd : ∀ (q₁ q₂ : ℚ), (q₁ - q₂).den ∣ q₁.den * q₂.den
-- Init.Meta.Defs
/-- Creates literal syntax for a name. The caller must ensure that the provided string is a valid name
literal.

If `info` is provided, then the literal's source information is copied from it.
 -/
Lean.Syntax.mkNameLit : String → optParam Lean.SourceInfo Lean.SourceInfo.none → Lean.NameLit
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.SimplicialObject.Augmented.w_app_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : CategoryTheory.SimplicialObject.Augmented C} (f : X ⟶ Y)
  (n : SimplexCategoryᵒᵖ) {Z : C} (h : Y.right ⟶ Z),
  CategoryTheory.CategoryStruct.comp (f.left.app n) (CategoryTheory.CategoryStruct.comp (Y.hom.app n) h) =
    CategoryTheory.CategoryStruct.comp (X.hom.app n) (CategoryTheory.CategoryStruct.comp f.right h)
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.ofHom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {A B : C}
  [inst_2 : CategoryTheory.MonObj A] [inst_3 : CategoryTheory.MonObj B] (f : A ⟶ B)
  [inst_4 : CategoryTheory.IsMonHom f], (CategoryTheory.Mon.ofHom f).hom = f
-- Mathlib.CategoryTheory.Galois.Basic
CategoryTheory.PreGaloisCategory.fiberBinaryProductEquiv_symm_snd_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat)
  [inst_1 : CategoryTheory.PreGaloisCategory C] [inst_2 : CategoryTheory.PreGaloisCategory.FiberFunctor F] {X Y : C}
  (x : (F.obj X).obj) (y : (F.obj Y).obj),
  (CategoryTheory.ConcreteCategory.hom (F.map CategoryTheory.Limits.prod.snd))
      ((CategoryTheory.PreGaloisCategory.fiberBinaryProductEquiv F X Y).symm (x, y)) =
    y
-- Mathlib.Data.Set.Semiring
/-- The image of a set under a multiplicative homomorphism is a ring homomorphism
with respect to the pointwise operations on sets.  -/
SetSemiring.imageHom : {α : Type u_1} →
  {β : Type u_2} → [inst : MulOneClass α] → [inst_1 : MulOneClass β] → (α →* β) → SetSemiring α →+* SetSemiring β
-- Mathlib.Topology.Algebra.UniformConvergence
instNSMulUniformFun.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : SMul M β],
  instNSMulUniformFun = { smul := fun a a_1 => instNSMulUniformFun._aux_1 a_1 a }
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
/-- The pushout cocone obtained from the pullback cone associated to a
commutative square in the opposite category identifies to the cocone associated
to the flipped square.  -/
CategoryTheory.CommSq.coneUnop : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {W X Y Z : Cᵒᵖ} →
      {f : W ⟶ X} →
        {g : W ⟶ Y} → {h : X ⟶ Z} → {i : Y ⟶ Z} → (p : CategoryTheory.CommSq f g h i) → p.cone.unop ≅ ⋯.cocone
-- Mathlib.Probability.Independence.Conditional
ProbabilityTheory.condIndepFun_of_measurable_left : ∀ {Ω : Type u_1} {β : Type u_3} {β' : Type u_4} {m' mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω]
  {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [inst_1 : MeasureTheory.IsFiniteMeasure μ] {mβ : MeasurableSpace β}
  {mβ' : MeasurableSpace β'} {X : Ω → β} {Y : Ω → β'},
  Measurable X → Measurable Y → ProbabilityTheory.CondIndepFun m' hm' X Y μ
-- Mathlib.RingTheory.Extension.Presentation.Basic
Algebra.Presentation.span_range_relation_eq_ker_baseChange : ∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (T : Type u_1) [inst_3 : CommRing T] [inst_4 : Algebra R T] (P : Algebra.Presentation R S ι σ),
  Ideal.span (Set.range fun i => (MvPolynomial.map (algebraMap R T)) (P.relation i)) =
    RingHom.ker (MvPolynomial.aeval (Algebra.Generators.baseChange T P.toGenerators).val)
-- Mathlib.NumberTheory.LSeries.DirichletContinuation
/-- The L function of the trivial Dirichlet character mod `N` is obtained from the Riemann
zeta function by multiplying with `∏ p ∈ N.primeFactors, (1 - (p : ℂ) ^ (-s))`.  -/
DirichletCharacter.LFunctionTrivChar_eq_mul_riemannZeta : ∀ {N : ℕ} [inst : NeZero N] {s : ℂ},
  s ≠ 1 → DirichletCharacter.LFunctionTrivChar N s = (∏ p ∈ N.primeFactors, (1 - ↑p ^ (-s))) * riemannZeta s
-- Mathlib.GroupTheory.SpecificGroups.Quaternion
QuaternionGroup.a.sizeOf_spec : ∀ {n : ℕ} (a : ZMod (2 * n)), sizeOf (QuaternionGroup.a a) = 1 + sizeOf a
-- Mathlib.RingTheory.WittVector.Isocrystal
/-- Project the Frobenius automorphism from an isocrystal. Denoted by `Φ(p, k)` when V can be inferred.
 -/
Isocrystal.«termΦ(_,_)» : Lean.ParserDescr
-- Mathlib.RepresentationTheory.Continuous.TopRep
TopRep.Hom.ext : ∀ {k : Type u} {G : Type v} {inst : TopologicalSpace k} {inst_1 : Ring k} {inst_2 : Monoid G} {A : TopRep k G}
  {B : TopRep k G} {x y : A.Hom B}, x.hom' = y.hom' → x = y