mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.distribSMul : {R : Type u} → [inst : Semiring R] → {S : Type u_1} → [DistribSMul S R] → DistribSMul S (Polynomial R)
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.exp_le_intValuation_iff_emultiplicity_le : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) {r : R}
  {n : ℕ}, WithZero.exp (-↑n) ≤ v.intValuation r ↔ emultiplicity v.asIdeal (Ideal.span {r}) ≤ ↑n
-- Mathlib.Order.SuccPred.Limit
Order.isSuccLimit_iff : ∀ {α : Type u_1} [inst : Preorder α] (a : α), Order.IsSuccLimit a ↔ ¬IsMin a ∧ Order.IsSuccPrelimit a
-- Aesop.Frontend.Extension
Aesop.Frontend.getGlobalRuleSets : Array Aesop.RuleSetName → Lean.CoreM (Array (Aesop.GlobalRuleSet × Lean.Name × Lean.Name))
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
/-- The map `X ⨿ Y ⟶ X ⨿[Z] Y` is epi.  -/
CategoryTheory.Limits.epi_coprod_to_pushout : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z)
  [inst_1 : CategoryTheory.Limits.HasPushout f g] [inst_2 : CategoryTheory.Limits.HasBinaryCoproduct Y Z],
  CategoryTheory.Epi
    (CategoryTheory.Limits.coprod.desc (CategoryTheory.Limits.pushout.inl f g) (CategoryTheory.Limits.pushout.inr f g))
-- Mathlib.Algebra.GroupWithZero.Defs
IsRightCancelMulZero.to_isCancelMulZero : ∀ {M₀ : Type u_1} [inst : CommMagma M₀] [inst_1 : Zero M₀] [IsRightCancelMulZero M₀], IsCancelMulZero M₀
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKey_congr : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] (h : (↑m).WF) {k k' : α} (h' : (k == k') = true)
  (h'' : m.contains k = true), m.getKey k h'' = m.getKey k' ⋯
-- Init.Prelude
/-- A decision procedure for equality of natural numbers, usually accessed via the `DecidableEq Nat`
instance.

This function is overridden in both the kernel and the compiler to efficiently evaluate using the
arbitrary-precision arithmetic library. The definition provided here is the logical model.

Examples:
 * `Nat.decEq 5 5 = isTrue rfl`
 * `(if 3 = 4 then "yes" else "no") = "no"`
 * `show 12 = 12 by decide`
 -/
Nat.decEq : (n m : ℕ) → Decidable (n = m)
-- Mathlib.SetTheory.Cardinal.SchroederBernstein
Equiv.equivEmpty.congr_simp : ∀ (α : Sort u) [inst : IsEmpty α], Equiv.equivEmpty α = Equiv.equivEmpty α
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.Spanning.closure_eq_of_superset : ∀ {α : Type u_2} {M : Matroid α} {S T : Set α}, M.Spanning S → S ⊆ T → M.closure T = M.E
-- Init.Data.Array.Find
Array.findSome?_replicate : ∀ {α : Type u_1} {α_1 : Type u_2} {f : α → Option α_1} {n : ℕ} {a : α},
  Array.findSome? f (Array.replicate n a) = if n = 0 then none else f a
-- Mathlib.Probability.Distributions.Gaussian.Multivariate
ProbabilityTheory.isProbabilityMeasure_stdGaussian : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  [inst_3 : MeasurableSpace E] [BorelSpace E], MeasureTheory.IsProbabilityMeasure (ProbabilityTheory.stdGaussian E)
-- Mathlib.Analysis.Complex.LocallyUniformLimit
TendstoUniformlyOn.cderiv : ∀ {E : Type u_1} {ι : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {K : Set ℂ} {δ : ℝ}
  {φ : Filter ι} {F : ι → ℂ → E} {f : ℂ → E},
  TendstoUniformlyOn F f φ (Metric.cthickening δ K) →
    0 < δ →
      (∀ᶠ (n : ι) in φ, ContinuousOn (F n) (Metric.cthickening δ K)) →
        TendstoUniformlyOn (Complex.cderiv δ ∘ F) (Complex.cderiv δ f) φ K
-- Mathlib.Algebra.Order.Interval.Set.Instances
/-- like `coe_nonneg`, but with the inequality in `Ico (0:R) 1`.  -/
Set.Ico.nonneg : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R] [inst_3 : Nontrivial R]
  {t : ↑(Set.Ico 0 1)}, 0 ≤ t
-- Mathlib.Data.Sym.Sym2
/-- **Alias** of `Sym2.mk_isDiag_iff`. -/
Sym2.isDiag_iff_proj_eq : ∀ {α : Type u_1} {x y : α}, s(x, y).IsDiag ↔ x = y
-- Mathlib.MeasureTheory.Function.Egorov
MeasureTheory.Egorov.iUnionNotConvergentSeq_subset : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace α} [inst : PseudoEMetricSpace β]
  {μ : MeasureTheory.Measure α} {s : Set α} {ε : ℝ} {f : ι → α → β} {g : α → β} [inst_1 : SemilatticeSup ι]
  [inst_2 : Nonempty ι] [inst_3 : Countable ι] (hε : 0 < ε) (hf : ∀ (n : ι), Measurable fun a => edist (f n a) (g a))
  (hsm : MeasurableSet s) (hs : μ s ≠ ⊤)
  (hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Filter.Tendsto (fun n => f n x) Filter.atTop (nhds (g x))),
  MeasureTheory.Egorov.iUnionNotConvergentSeq hε hf hsm hs hfg ⊆ s
-- Mathlib.Data.Rel
SetRel.preimage_univ_right : ∀ {α : Type u_1} {β : Type u_2} {R : SetRel α β}, R.preimage Set.univ = R.dom
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
/-- Given a `PushoutObjObj` of `f₁ : Arrow C₁` and `f₂ : Arrow C₂`, a `PushoutObjObj` of `f₁` and
`f₂' : Arrow C₂`, and an isomorphism `f₂ ≅ f₂'`, this defines an isomorphism of the induced
pushout maps.  -/
CategoryTheory.Functor.PushoutObjObj.ι_iso_of_iso_right : {C₁ : Type u₁} →
  {C₂ : Type u₂} →
    {C₃ : Type u₃} →
      [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃] →
            {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)} →
              {f₁ : CategoryTheory.Arrow C₁} →
                {f₂ f₂' : CategoryTheory.Arrow C₂} →
                  (sq₁₂ : F.PushoutObjObj f₁.hom f₂.hom) →
                    (sq₁₂' : F.PushoutObjObj f₁.hom f₂'.hom) →
                      (f₂ ≅ f₂') → (CategoryTheory.Arrow.mk sq₁₂.ι ≅ CategoryTheory.Arrow.mk sq₁₂'.ι)
-- Lean.Meta.CoeAttr
Lean.Meta.instReprCoeFnInfo.repr : Lean.Meta.CoeFnInfo → ℕ → Std.Format
-- Batteries.Data.List.Interleave
List.length_interleave : ∀ {α : Type u_1} (l₁ l₂ : List α), (l₁.interleave l₂).length = l₁.length + l₂.length
-- Mathlib.Algebra.Order.Field.Basic
/-- **Alias** of the forward direction of `mul_sub_mul_div_mul_neg_iff`. -/
div_lt_div_of_mul_sub_mul_div_neg : ∀ {α : Type u_2} [inst : Field α] [inst_1 : PartialOrder α] [IsStrictOrderedRing α] {a b c d : α},
  c ≠ 0 → d ≠ 0 → (a * d - b * c) / (c * d) < 0 → a / c < b / d
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.Measure.pi_ball : ∀ {ι : Type u_1} {α : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → MeasurableSpace (α i)]
  (μ : (i : ι) → MeasureTheory.Measure (α i)) [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)]
  [inst_3 : (i : ι) → MetricSpace (α i)] (x : (i : ι) → α i) {r : ℝ},
  0 < r → (MeasureTheory.Measure.pi μ) (Metric.ball x r) = ∏ i, (μ i) (Metric.ball (x i) r)
-- Mathlib.Data.Fin.Tuple.Take
Fin.take_apply : ∀ {n : ℕ} {α : Fin n → Sort u_1} (m : ℕ) (h : m ≤ n) (v : (i : Fin n) → α i) (i : Fin m),
  Fin.take m h v i = v (Fin.castLE h i)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.subset_sub_left : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SubtractionMonoid α] {s t : Finset α}, 0 ∈ t → s ⊆ s - t
-- Mathlib.Data.ZMod.QuotientRing
Int.quotientSpanNatEquivZMod_comp_Quotient_mk : ∀ (n : ℕ), (↑(Int.quotientSpanNatEquivZMod n)).comp (Ideal.Quotient.mk (Ideal.span {↑n})) = Int.castRingHom (ZMod n)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc
Real.sinc.eq_1 : ∀ (x : ℝ), Real.sinc x = if x = 0 then 1 else Real.sin x / x
-- Mathlib.Order.WithBot
WithBot.unbotD_lt_iff : ∀ {α : Type u_1} {a b : α} [inst : LT α] {x : WithBot α}, (x = ⊥ → a < b) → (WithBot.unbotD a x < b ↔ x < ↑b)
-- Mathlib.Logic.IsEmpty.Defs
Prod.isEmpty_right : ∀ {α : Type u_1} {β : Type u_2} [IsEmpty β], IsEmpty (α × β)
-- Mathlib.NumberTheory.NumberField.Completion.Ramification
NumberField.InfinitePlace.Completion.ringEquivComplexOfIsComplex.congr_simp : ∀ {K : Type u_1} [inst : Field K] {v : NumberField.InfinitePlace K} (hv : v.IsComplex),
  NumberField.InfinitePlace.Completion.ringEquivComplexOfIsComplex hv =
    NumberField.InfinitePlace.Completion.ringEquivComplexOfIsComplex hv
-- Mathlib.Topology.Instances.ENNReal.Lemmas
/-- If `u : ι → ℝ≥0∞` is bounded, then we have `liminf (toReal ∘ u) = toReal (liminf u)`.  -/
ENNReal.liminf_toReal_eq : ∀ {ι : Type u_4} {f : Filter ι} {u : ι → ENNReal} [f.NeBot] {b : ENNReal},
  b ≠ ⊤ → (∀ᶠ (i : ι) in f, u i ≤ b) → Filter.liminf (fun i => (u i).toReal) f = (Filter.liminf u f).toReal
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.instAdd.eq_1 : ∀ {α : Type u} {R : Type u_2} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace R] [inst_2 : Add R]
  [inst_3 : BoundedAdd R] [inst_4 : ContinuousAdd R],
  BoundedContinuousFunction.instAdd =
    { add := fun f g => { toFun := fun x => f x + g x, continuous_toFun := ⋯, map_bounded' := ⋯ } }
-- Plausible.Sampleable
/-- First samples a proxy value and interprets it. Especially useful if
the proxy and target type are the same.  -/
Plausible.SampleableExt.interpSample : (α : Type u) → [Plausible.SampleableExt α] → Plausible.Gen α
-- Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
CategoryTheory.preservesLimitNatIso.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J]
  [inst_3 : CategoryTheory.Limits.PreservesLimitsOfShape J G] [inst_4 : CategoryTheory.Limits.HasLimitsOfShape J D]
  [inst_5 : CategoryTheory.Limits.HasLimitsOfShape J C],
  CategoryTheory.preservesLimitNatIso G = CategoryTheory.preservesLimitNatIso G
-- Mathlib.Analysis.Normed.Algebra.Spectrum
/-- The *spectral radius* is the supremum of the `nnnorm` (`‖·‖₊`) of elements in the spectrum,
coerced into an element of `ℝ≥0∞`. Note that it is possible for `spectrum 𝕜 a = ∅`. In this
case, `spectralRadius a = 0`. It is also possible that `spectrum 𝕜 a` be unbounded (though
not for Banach algebras, see `spectrum.isBounded`, below).  In this case,
`spectralRadius a = ∞`.  -/
spectralRadius : (𝕜 : Type u_1) → {A : Type u_2} → [inst : NormedField 𝕜] → [inst_1 : Ring A] → [Algebra 𝕜 A] → A → ENNReal
-- Mathlib.Topology.IndicatorConstPointwise
/-- The indicator functions of `Asᵢ` tend to the indicator function of `A` pointwise if and only if
for every `x`, we eventually have the equivalence `x ∈ Asᵢ ↔ x ∈ A`.  -/
tendsto_indicator_const_iff_forall_eventually : ∀ {α : Type u_1} {A : Set α} {β : Type u_2} [inst : Zero β] [inst_1 : TopologicalSpace β] {ι : Type u_3} (L : Filter ι)
  {As : ι → Set α} [T1Space β] (b : β) [NeZero b],
  Filter.Tendsto (fun i => (As i).indicator fun x => b) L (nhds (A.indicator fun x => b)) ↔
    ∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
-- Lean.Elab.Tactic.Induction
/-- Given `inductionAlts` of the form
```
syntax inductionAlts := "with " (tactic)? withPosition( (colGe inductionAlt)*)
```
Return an array containing its alternatives.
 -/
_private.Lean.Elab.Tactic.Induction.0.Lean.Elab.Tactic.getAltsOfInductionAlts : Lean.Syntax → Array Lean.Syntax
-- Std.Time.Format.Modifier
Std.Time.Modifier.M.injEq : ∀ (presentation presentation_1 : Std.Time.Number ⊕ Std.Time.Text),
  (Std.Time.Modifier.M presentation = Std.Time.Modifier.M presentation_1) = (presentation = presentation_1)
-- Mathlib.LinearAlgebra.QuadraticForm.Basis
QuadraticMap.apply_linearCombination' : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup N] [inst_3 : Module R M] [inst_4 : Module R N] (Q : QuadraticMap R M N) {g : ι → M}
  (l : ι →₀ R),
  Q ((Finsupp.linearCombination R g) l) =
    (Finsupp.linearCombination R (QuadraticMap.polarSym2 ⇑Q ∘ Sym2.map g)) l.sym2Mul -
      (Finsupp.linearCombination R (⇑Q ∘ g)) (l * l)
-- Mathlib.RingTheory.DividedPowers.DPMorphism
DividedPowers.DPMorphism.coe_toRingHom : ∀ {A : Type u_3} {B : Type u_4} [inst : CommSemiring A] [inst_1 : CommSemiring B] {I : Ideal A} {J : Ideal B}
  (hI : DividedPowers I) (hJ : DividedPowers J) {f : hI.DPMorphism hJ}, ⇑f.toRingHom = ⇑f
-- Std.Http.Data.URI.Encoding
/-- Creates an empty encoded query string.
 -/
Std.Http.URI.EncodedQueryString.empty : {r : UInt8 → Bool} → Std.Http.URI.EncodedQueryString r
-- Init.Data.UInt.IntToBitVec
Bool.toBitVec32_toUSize : ∀ {b : Bool} (h : System.Platform.numBits = 32), b.toUSize.toBitVec32 h = BitVec.setWidth 32 (BitVec.ofBool b)
-- Mathlib.CategoryTheory.MorphismProperty.Basic
/-- The morphism property on `J ⥤ C` which is defined objectwise
from `W : MorphismProperty C`.  -/
CategoryTheory.MorphismProperty.functorCategory : {C : Type u_2} →
  [inst : CategoryTheory.Category.{v, u_2} C] →
    CategoryTheory.MorphismProperty C →
      (J : Type u_1) →
        [inst_1 : CategoryTheory.Category.{v_1, u_1} J] → CategoryTheory.MorphismProperty (CategoryTheory.Functor J C)
-- Mathlib.Data.Finmap
/-- The empty map.  -/
Finmap.instEmptyCollection : {α : Type u} → {β : α → Type v} → EmptyCollection (Finmap β)
-- Init.Data.List.MinMaxIdx
List.minIdxOn?_cons : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] [Std.IsLinearPreorder β] {f : α → β} {x : α}
  {xs : List α},
  List.minIdxOn? f (x :: xs) =
    some (if h : xs = [] then 0 else if f x ≤ f (List.minOn f xs h) then 0 else List.minIdxOn f xs h + 1)
-- Mathlib.MeasureTheory.Function.UniformIntegrable
MeasureTheory.eLpNorm_indicator_le_of_bound : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  {p : ENNReal} {f : α → β},
  p ≠ ⊤ →
    ∀ {ε : ℝ},
      0 < ε →
        ∀ {M : ℝ},
          (∀ (x : α), ‖f x‖ < M) →
            ∃ δ,
              ∃ (_ : 0 < δ),
                ∀ (s : Set α),
                  MeasurableSet s →
                    μ s ≤ ENNReal.ofReal δ → MeasureTheory.eLpNorm (s.indicator f) p μ ≤ ENNReal.ofReal ε
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
IsPrimitiveRoot.adjoinEquivRingOfIntegers.congr_simp : ∀ {n n_1 : ℕ} (e_n : n = n_1) {K : Type u} [inst : Field K] {ζ : K} [inst_1 : NeZero n] [inst_2 : CharZero K]
  [inst_3 : IsCyclotomicExtension {n} ℚ K] (hζ : IsPrimitiveRoot ζ n),
  hζ.adjoinEquivRingOfIntegers = ⋯.adjoinEquivRingOfIntegers
-- Init.Data.Range.Polymorphic.PRange
Std.Roi.instDecidableMemOfDecidableLT : {α : Type u} → {r : Std.Roi α} → {a : α} → [inst : LT α] → [DecidableLT α] → Decidable (a ∈ r)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem_insertIfNew : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : EquivBEq α]
  [inst_3 : LawfulHashable α] (h : m.WF) {k a : α} {v : β} {h₁ : a ∈ m.insertIfNew k v},
  (m.insertIfNew k v)[a] = if h₂ : (k == a) = true ∧ k ∉ m then v else m[a]
-- Mathlib.Analysis.Normed.Algebra.MatrixExponential
Matrix.IsHermitian.exp : ∀ {m : Type u_1} {𝔸 : Type u_5} [inst : Fintype m] [inst_1 : DecidableEq m] [inst_2 : Ring 𝔸]
  [inst_3 : TopologicalSpace 𝔸] [inst_4 : IsTopologicalRing 𝔸] [T2Space 𝔸] [inst_6 : StarRing 𝔸] [ContinuousStar 𝔸]
  {A : Matrix m m 𝔸}, A.IsHermitian → (NormedSpace.exp A).IsHermitian
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
NumberField.ComplexEmbedding.isConj_ne_one_iff : ∀ {K : Type u_1} [inst : Field K] {k : Type u_2} [inst_1 : Field k] [inst_2 : Algebra k K] {φ : K →+* ℂ} {σ : Gal(K/k)},
  NumberField.ComplexEmbedding.IsConj φ σ → (σ ≠ 1 ↔ ¬NumberField.ComplexEmbedding.IsReal φ)
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtensionAt.ι_isoColimit_hom_assoc : ∀ {C : Type u_1} {D : Type u_2} {H : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_4, u_4} H]
  {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} {E : L.LeftExtension F} {Y : D}
  (h : E.IsPointwiseLeftKanExtensionAt Y)
  [inst_3 : CategoryTheory.Limits.HasColimit ((CategoryTheory.CostructuredArrow.proj L Y).comp F)]
  (g : CategoryTheory.CostructuredArrow L Y) {Z : H}
  (h_1 : CategoryTheory.Limits.colimit ((CategoryTheory.CostructuredArrow.proj L Y).comp F) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.StructuredArrow.hom E).app g.left)
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.StructuredArrow.right E).map g.hom)
        (CategoryTheory.CategoryStruct.comp h.isoColimit.hom h_1)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.colimit.ι ((CategoryTheory.CostructuredArrow.proj L Y).comp F) g) h_1
-- Mathlib.CategoryTheory.Action.Basic
Action.instFunLikeHomSubtypeV : (V : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    (G : Type u_2) →
      [inst_1 : Monoid G] →
        {FV : V → V → Type u_3} →
          {CV : V → Type u_4} →
            [inst_2 : (X Y : V) → FunLike (FV X Y) (CV X) (CV Y)] →
              [inst_3 : CategoryTheory.ConcreteCategory V FV] →
                (M N : Action V G) → FunLike (Action.HomSubtype V G M N) (CV M.V) (CV N.V)
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
CFC.rpow_rpow_inv : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : Ring A] [inst_2 : StarRing A] [inst_3 : TopologicalSpace A]
  [inst_4 : StarOrderedRing A] [inst_5 : Algebra ℝ A] [inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint]
  [inst_7 : NonnegSpectrumClass ℝ A] [IsSemitopologicalRing A] [T2Space A] (a : A) (x : ℝ),
  x ≠ 0 → autoParam (IsStrictlyPositive a) CFC.rpow_rpow_inv._auto_1 → (a ^ x) ^ x⁻¹ = a
-- Mathlib.Computability.Primrec.List
Nat.Primrec'.get : ∀ {n : ℕ} (i : Fin n), Nat.Primrec' fun v => v.get i
-- Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
/-- The isomorphism
`toHoCat ⋙ HoCat.ιCofibrantObject ≅ ιCofibrantObject ⋙ CofibrantObject.toHoCat`
between functors `BifibrantObject C ⥤ CofibrantObject.HoCat C`.  -/
HomotopicalAlgebra.BifibrantObject.toHoCatCompιCofibrantObject : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : HomotopicalAlgebra.ModelCategory C] →
      HomotopicalAlgebra.BifibrantObject.toHoCat.comp HomotopicalAlgebra.BifibrantObject.HoCat.ιCofibrantObject ≅
        HomotopicalAlgebra.BifibrantObject.ιCofibrantObject.comp HomotopicalAlgebra.CofibrantObject.toHoCat
-- Mathlib.Data.Part
/-- The `none` value in `Part` has a `False` domain and an empty function.  -/
Part.none : {α : Type u_1} → Part α
-- Init.Data.Order.Lemmas
Std.lt_iff_le_and_not_ge : ∀ {α : Type u} [inst : LT α] [inst_1 : LE α] [Std.LawfulOrderLT α] {a b : α}, a < b ↔ a ≤ b ∧ ¬b ≤ a
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.ValueGroupWithZero.ind : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R] {motive : ValuativeRel.ValueGroupWithZero R → Prop},
  (∀ (x : R) (y : ↥(ValuativeRel.posSubmonoid R)), motive (ValuativeRel.ValueGroupWithZero.mk x y)) →
    ∀ (t : ValuativeRel.ValueGroupWithZero R), motive t
-- Lean.Meta.Sym.Pattern
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.UnifyM.State.ePending : Lean.Meta.Sym.UnifyM.State✝ → Array (Lean.Expr × Lean.Expr)
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.vsub_sInter_subset : ∀ {α : Type u_2} {β : Type u_3} [inst : VSub α β] (s : Set β) (T : Set (Set β)), s -ᵥ ⋂₀ T ⊆ ⋂ t ∈ T, s -ᵥ t
-- Mathlib.MeasureTheory.Group.Measure
/-- If the zero element of an additive group is not isolated, then an additive Haar measure on this
group has value zero on singletons.

This applies in particular to show that an additive Haar measure on a nontrivial
finite-dimensional real vector space has no atom.  -/
MeasureTheory.Measure.IsAddHaarMeasure.nullSingletonClass : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : AddGroup G] [inst_2 : TopologicalSpace G]
  [IsTopologicalAddGroup G] [BorelSpace G] [T1Space G] [WeaklyLocallyCompactSpace G] [(nhdsWithin 0 {0}ᶜ).NeBot]
  (μ : MeasureTheory.Measure G) [μ.IsAddHaarMeasure], MeasureTheory.NullSingletonClass μ
-- Mathlib.AlgebraicGeometry.Geometrically.Basic
AlgebraicGeometry.geometrically_eq_universally : ∀ (P : CategoryTheory.ObjectProperty AlgebraicGeometry.Scheme),
  AlgebraicGeometry.geometrically P =
    CategoryTheory.MorphismProperty.universally fun X Y x => AlgebraicGeometry.IsIntegral Y → Subsingleton ↥Y → P X
-- Mathlib.FieldTheory.PerfectClosure
PerfectClosure.frobenius_mk : ∀ (K : Type u) [inst : CommRing K] (p : ℕ) [inst_1 : Fact (Nat.Prime p)] [inst_2 : CharP K p] (x : ℕ × K),
  (frobenius (PerfectClosure K p) p) (PerfectClosure.mk K p x) = PerfectClosure.mk K p (x.1, x.2 ^ p)
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.Parser.feature__3 : Lean.ParserDescr
-- Mathlib.Algebra.Order.Archimedean.Class
MulArchimedeanClass.instInhabited.eq_1 : ∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M],
  MulArchimedeanClass.instInhabited = { default := ⊤ }
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.isoRestrict_hom_ofRestrict : ∀ {X Y : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Y) [H : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion f],
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.isoRestrict f).hom
      (Y.ofRestrict ⋯) =
    f
-- Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter
CategoryTheory.SimplicialObject.δ_δ₀Iter'_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (X : CategoryTheory.SimplicialObject C) {n : ℕ}
  (i : Fin (n + 2)) (j : ℕ) {m : ℕ} (i' : Fin (m + 2))
  (h : autoParam (n + j = m) CategoryTheory.SimplicialObject.δ_δ₀Iter'._auto_1),
  autoParam (↑i' = ↑i + j) CategoryTheory.SimplicialObject.δ_δ₀Iter'._auto_3 →
    ∀ {Z : C} (h_1 : X.obj (Opposite.op { len := n }) ⟶ Z),
      CategoryTheory.CategoryStruct.comp (X.δ i') (CategoryTheory.CategoryStruct.comp (X.δ₀Iter j ⋯) h_1) =
        CategoryTheory.CategoryStruct.comp (X.δ₀Iter j ⋯) (CategoryTheory.CategoryStruct.comp (X.δ i) h_1)
-- Mathlib.Probability.Independence.Kernel.Indep
ProbabilityTheory.Kernel.iIndep.ae_isProbabilityMeasure : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {m : ι → MeasurableSpace Ω}
  {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α},
  ProbabilityTheory.Kernel.iIndep m κ μ → ∀ᵐ (a : α) ∂μ, MeasureTheory.IsProbabilityMeasure (κ a)
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.integral_smul_measure : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b : ℝ} {f : ℝ → E}
  {μ : MeasureTheory.Measure ℝ} (c : ENNReal), ∫ (x : ℝ) in a..b, f x ∂c • μ = c.toReal • ∫ (x : ℝ) in a..b, f x ∂μ
-- Mathlib.AlgebraicGeometry.Cover.MorphismProperty
AlgebraicGeometry.Scheme.Cover.copy_X : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [inst : P.RespectsIso] {X : AlgebraicGeometry.Scheme}
  (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X) (J : Type u_1)
  (obj : J → AlgebraicGeometry.Scheme) (map : (i : J) → obj i ⟶ X) (e₁ : J ≃ 𝒰.I₀) (e₂ : (i : J) → obj i ≅ 𝒰.X (e₁ i))
  (h : ∀ (i : J), map i = CategoryTheory.CategoryStruct.comp (e₂ i).hom (𝒰.f (e₁ i))) (a : J),
  (𝒰.copy J obj map e₁ e₂ h).X a = obj a
-- Mathlib.CategoryTheory.Monoidal.CommMon_
CategoryTheory.Functor.comp_mapCommMon_one : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {D : Type u₂} [inst_3 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_4 : CategoryTheory.MonoidalCategory D] [inst_5 : CategoryTheory.BraidedCategory D] {E : Type u₃}
  [inst_6 : CategoryTheory.Category.{v₃, u₃} E] [inst_7 : CategoryTheory.MonoidalCategory E]
  [inst_8 : CategoryTheory.BraidedCategory E] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D E}
  [inst_9 : F.LaxBraided] [inst_10 : G.LaxBraided] (A : CategoryTheory.CommMon C),
  CategoryTheory.MonObj.one =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε (F.comp G))
      ((F.comp G).map CategoryTheory.MonObj.one)