mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Algebraic.Integral
/-- [Stacks Tag 0G1M](https://stacks.math.columbia.edu/tag/0G1M) -/
Algebra.IsAlgebraic.rank_fractionRing_mvPolynomial : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [alg : Algebra.IsAlgebraic R S] [inst_3 : IsDomain S] [inst_4 : FaithfulSMul R S] (σ : Type u),
  Module.rank (FractionRing (MvPolynomial σ R)) (FractionRing (MvPolynomial σ S)) =
    Cardinal.lift.{u, u_2} (Module.rank R S)
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.Std.DHashMap.Internal.AssocList.foldlM.eq_def : ∀ {α : Type u} {β : α → Type v} {δ : Type w} {m : Type w → Type w'} [inst : Monad m] (f : δ → (a : α) → β a → m δ)
  (x : δ) (x_1 : Std.DHashMap.Internal.AssocList α β),
  Std.DHashMap.Internal.AssocList.foldlM f x x_1 =
    match x, x_1 with
    | d, Std.DHashMap.Internal.AssocList.nil => pure d
    | d, Std.DHashMap.Internal.AssocList.cons a b es => do
      let d ← f d a b
      Std.DHashMap.Internal.AssocList.foldlM f d es
-- Mathlib.Topology.Algebra.InfiniteSum.Order
hasSum_zero_iff_of_nonneg : ∀ {ι : Type u_4} {α : Type u_5} {L : SummationFilter ι} [inst : AddCommMonoid α] [inst_1 : PartialOrder α]
  [IsOrderedAddMonoid α] [inst_3 : TopologicalSpace α] [OrderClosedTopology α] {f : ι → α} [L.LeAtTop] [L.NeBot],
  (∀ (i : ι), 0 ≤ f i) → (HasSum f 0 L ↔ f = 0)
-- Mathlib.MeasureTheory.Measure.Lebesgue.Basic
/-- A transvection preserves Lebesgue measure.  -/
Real.volume_preserving_transvectionStruct : ∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (t : Matrix.TransvectionStruct ι ℝ),
  MeasureTheory.MeasurePreserving (⇑(Matrix.toLin' t.toMatrix)) MeasureTheory.volume MeasureTheory.volume
-- Init.Data.Int.DivMod.Lemmas
Int.le_tdiv_of_mul_le : ∀ {a b c : ℤ}, 0 < c → a * c ≤ b → a ≤ b.tdiv c
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
/-- **Fundamental theorem of calculus-1**: if `f : ℝ → E` is integrable on `a..b` and `f x` has a
finite limit `c` almost surely at `a`, then `u ↦ ∫ x in u..b, f x` has derivative `-c` at `a`.  -/
intervalIntegral.integral_hasDerivAt_of_tendsto_ae_left : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E} {c : E}
  {a b : ℝ},
  IntervalIntegrable f MeasureTheory.volume a b →
    StronglyMeasurableAtFilter f (nhds a) MeasureTheory.volume →
      Filter.Tendsto f (nhds a ⊓ MeasureTheory.ae MeasureTheory.volume) (nhds c) →
        HasDerivAt (fun u => ∫ (x : ℝ) in u..b, f x) (-c) a
-- Mathlib.Topology.ContinuousMap.Star
ContinuousMap.star_apply : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : Star β]
  [inst_3 : ContinuousStar β] (f : C(α, β)) (x : α), (star f) x = star (f x)
-- Lean.Elab.ParseImportsFast
Lean.ParseImports.moduleIdent : Lean.ParseImports.Parser
-- Mathlib.Algebra.BigOperators.Finprod
finsum_nsmul : ∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] {f : α → M},
  Function.HasFiniteSupport f → ∀ (n : ℕ), n • ∑ᶠ (i : α), f i = ∑ᶠ (i : α), n • f i
-- Mathlib.RingTheory.Ideal.NatInt
Nat.one_mem_span_iff : ∀ {s : Set ℕ}, 1 ∈ Ideal.span s ↔ 1 ∈ s
-- Mathlib.Topology.ContinuousOn
/-- If a function `f a b` is such that `y ↦ f a b` is continuous for all `a`, and `a` lives in a
discrete space, then `f` is continuous, and vice versa.  -/
continuous_prod_of_discrete_left : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : TopologicalSpace γ] [DiscreteTopology α] {f : α × β → γ},
  Continuous f ↔ ∀ (a : α), Continuous fun x => f (a, x)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
_private.Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting.0.CategoryTheory.Limits.termX₁ : Lean.ParserDescr
-- Mathlib.Data.Bundle
/-- Notation for the direct sum of two bundles over the same base.  -/
Bundle.«term_×ᵇ_» : Lean.TrailingParserDescr
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Triplet.mk.inj : ∀ {n p q : ℤ} {hpq : p + n = q} {p_1 q_1 : ℤ} {hpq_1 : p_1 + n = q_1},
  { p := p, q := q, hpq := hpq } = { p := p_1, q := q_1, hpq := hpq_1 } → p = p_1 ∧ q = q_1
-- Mathlib.Order.Interval.Set.Pi
Set.disjoint_pi_univ_Ioc_update_left_right : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → Preorder (α i)] [inst_1 : DecidableEq ι] {x y : (i : ι) → α i}
  {i₀ : ι} {m : α i₀},
  Disjoint (Set.univ.pi fun i => Set.Ioc (x i) (Function.update y i₀ m i))
    (Set.univ.pi fun i => Set.Ioc (Function.update x i₀ m i) (y i))
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.coeLMₛₗ_apply : ∀ {R : Type u_1} {R₃ : Type u_3} {S₃ : Type u_5} [inst : Semiring R] [inst_1 : Semiring R₃] [inst_2 : Semiring S₃]
  {M : Type u_6} [inst_3 : TopologicalSpace M] [inst_4 : AddCommMonoid M] [inst_5 : Module R M] {M₃ : Type u_8}
  [inst_6 : TopologicalSpace M₃] [inst_7 : AddCommMonoid M₃] [inst_8 : Module R₃ M₃] [inst_9 : Module S₃ M₃]
  [inst_10 : SMulCommClass R₃ S₃ M₃] [inst_11 : ContinuousConstSMul S₃ M₃] (σ₁₃ : R →+* R₃) [inst_12 : ContinuousAdd M₃]
  (self : M →SL[σ₁₃] M₃), (ContinuousLinearMap.coeLMₛₗ σ₁₃) self = ↑self
-- Mathlib.RingTheory.AdicCompletion.Algebra
/-- `AdicCompletion I M` is naturally an `AdicCompletion I R` module.  -/
AdicCompletion.module : {R : Type u_1} →
  [inst : CommRing R] →
    (I : Ideal R) →
      {M : Type u_3} →
        [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → Module (AdicCompletion I R) (AdicCompletion I M)
-- Mathlib.LinearAlgebra.RootSystem.Base
/-- A base for a root system gives a `ℤ`-basis for the `ℤ`-span of the roots.  -/
RootPairing.Base.toWeightBasisInt : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      {N : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] →
              [inst_3 : AddCommGroup N] →
                [inst_4 : Module R N] →
                  {P : RootPairing ι R M N} → (b : P.Base) → [CharZero R] → Module.Basis ↥b.support ℤ ↥(P.rootSpan ℤ)
-- Std.Data.Iterators.Combinators.Monadic.StepSize
Std.Iterators.Types.StepSizeIterator.nextIdx : {α : Type w} → {m : Type w → Type w'} → {β : Type w} → Std.Iterators.Types.StepSizeIterator α m β → ℕ
-- Lean.Meta.Sym.Pattern
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.MkPreResultResult.failed.sizeOf_spec : sizeOf Lean.Meta.Sym.MkPreResultResult.failed✝ = 1
-- Mathlib.Algebra.Group.Subgroup.Ker
AddSubgroup.ker_inclusion : ∀ {G : Type u_1} [inst : AddGroup G] {H K : AddSubgroup G} (h : H ≤ K), (AddSubgroup.inclusion h).ker = ⊥
-- Mathlib.AlgebraicTopology.SimplicialSet.PushoutProduct
SSet.Subcomplex.unionProd.pushoutObjObj_inl : ∀ {X Y : SSet} (S : X.Subcomplex) (T : Y.Subcomplex),
  (SSet.Subcomplex.unionProd.pushoutObjObj S T).inl = SSet.Subcomplex.unionProd.ι₁ S T
-- Mathlib.Tactic.FunProp.FunctionData
Mathlib.Meta.FunProp.MaybeFunctionData.data.sizeOf_spec : ∀ (fData : Mathlib.Meta.FunProp.FunctionData),
  sizeOf (Mathlib.Meta.FunProp.MaybeFunctionData.data fData) = 1 + sizeOf fData
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.colimit.pre_map : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  {C : Type u} [inst_2 : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor J C}
  [inst_3 : CategoryTheory.Limits.HasColimitsOfShape J C] {G : CategoryTheory.Functor J C} (α : F ⟶ G)
  [inst_4 : CategoryTheory.Limits.HasColimitsOfShape K C] (E : CategoryTheory.Functor K J),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.pre F E) (CategoryTheory.Limits.colim.map α) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colim.map (E.whiskerLeft α))
      (CategoryTheory.Limits.colimit.pre G E)
-- Mathlib.Topology.Algebra.Module.Spaces.CompactConvergenceCLM
ContinuousLinearMap.precompCompactConvergenceCLM_apply : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂]
  [inst_2 : NormedField 𝕜₃] {σ : 𝕜₁ →+* 𝕜₂} {τ : 𝕜₂ →+* 𝕜₃} {ρ : 𝕜₁ →+* 𝕜₃} [inst_3 : RingHomCompTriple σ τ ρ]
  {E : Type u_4} {F : Type u_5} (G : Type u_6) [inst_4 : AddCommGroup E] [inst_5 : Module 𝕜₁ E]
  [inst_6 : AddCommGroup F] [inst_7 : Module 𝕜₂ F] [inst_8 : AddCommGroup G] [inst_9 : Module 𝕜₃ G]
  [inst_10 : TopologicalSpace E] [inst_11 : TopologicalSpace F] [inst_12 : TopologicalSpace G]
  [inst_13 : IsTopologicalAddGroup G] [inst_14 : ContinuousConstSMul 𝕜₃ G] (L : E →SL[σ] F)
  (f : UniformConvergenceCLM τ G {S | IsCompact S}), (ContinuousLinearMap.precompCompactConvergenceCLM G L) f = f ∘SL L
-- Lean.Elab.ErrorUtils
_private.Lean.Elab.ErrorUtils.0.Lean.HasOxfordStrings.mk : {α : Sort u_1} → α → α → α → α → Lean.HasOxfordStrings✝ α
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
NonUnitalStarAlgHom.codRestrict.congr_simp : ∀ {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : Module R A] [inst_3 : Star A] [inst_4 : NonUnitalNonAssocSemiring B] [inst_5 : Module R B] [inst_6 : Star B]
  [inst_7 : FunLike F A B] [inst_8 : NonUnitalAlgHomClass F R A B] [inst_9 : StarHomClass F A B] (f f_1 : F)
  (e_f : f = f_1) (S : NonUnitalStarSubalgebra R B) (hf : ∀ (x : A), f x ∈ S),
  NonUnitalStarAlgHom.codRestrict f S hf = NonUnitalStarAlgHom.codRestrict f_1 S ⋯
-- Mathlib.RingTheory.Ideal.Maps
RingHom.ker_rangeRestrict : ∀ {R : Type u} {S : Type v} [inst : Ring R] [inst_1 : Ring S] (f : R →+* S), RingHom.ker f.rangeRestrict = RingHom.ker f
-- Init.Data.Ord.Basic
Ordering.isGE_iff_ne_lt : ∀ {o : Ordering}, o.isGE = true ↔ ¬o = Ordering.lt
-- Mathlib.Algebra.Order.Ring.Canonical
CanonicallyOrderedAdd.pow_pos : ∀ {R : Type u} [inst : CommSemiring R] [inst_1 : PartialOrder R] [CanonicallyOrderedAdd R] [IsReduced R] {a : R},
  0 < a → ∀ (n : ℕ), 0 < a ^ n
-- Mathlib.GroupTheory.OreLocalization.Basic
AddOreLocalization.oreSub_eq_iff : ∀ {R : Type u_1} [inst : AddMonoid R] {S : AddSubmonoid R} [inst_1 : AddOreLocalization.AddOreSet S] {X : Type u_2}
  [inst_2 : AddAction R X] {r₁ r₂ : X} {s₁ s₂ : ↥S}, r₁ -ₒ s₁ = r₂ -ₒ s₂ ↔ ∃ u v, u +ᵥ r₂ = v +ᵥ r₁ ∧ ↑u + ↑s₂ = v + ↑s₁
-- Mathlib.RingTheory.Smooth.NoetherianDescent
_private.Mathlib.RingTheory.Smooth.NoetherianDescent.0.Algebra.Smooth.DescentAux.p : {A : Type u} →
  {B : Type u_2} →
    [inst : CommRing A] →
      [inst_1 : CommRing B] →
        [inst_2 : Algebra A B] →
          (self : Algebra.Smooth.DescentAux✝ A B) →
            Algebra.Smooth.DescentAux.rels✝ self →
              MvPolynomial (Algebra.Smooth.DescentAux.rels✝ self)
                (MvPolynomial (Algebra.Smooth.DescentAux.vars✝ self) A)
-- Mathlib.Algebra.Field.Defs
DivisionSemiring.toDiv : {K : Type u_2} → [self : DivisionSemiring K] → Div K
-- Std.Internal.Do.Order.Basic
Lean.Order.CompleteLattice.ofProp_false : ∀ (l : Type v) [inst : Lean.Order.CompleteLattice l], Lean.Order.CompleteLattice.ofProp False = Lean.Order.bot
-- Mathlib.Geometry.Euclidean.Altitude
Affine.Simplex.altitudeFoot_reindex : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {m n : ℕ} [inst_4 : NeZero m] [inst_5 : NeZero n] (s : Affine.Simplex ℝ P n)
  (e : Fin (n + 1) ≃ Fin (m + 1)), (s.reindex e).altitudeFoot = s.altitudeFoot ∘ ⇑e.symm
-- Mathlib.Order.Antisymmetrization
ofAntisymmetrization_lt_ofAntisymmetrization_iff : ∀ {α : Type u_1} [inst : Preorder α] {a b : Antisymmetrization α fun x1 x2 => x1 ≤ x2},
  ofAntisymmetrization (fun x1 x2 => x1 ≤ x2) a < ofAntisymmetrization (fun x1 x2 => x1 ≤ x2) b ↔ a < b
-- Mathlib.Logic.Equiv.Defs
Equiv.sigmaEquivProd_apply : ∀ (α : Type u_1) (β : Type u_2) (a : (_ : α) × β), (Equiv.sigmaEquivProd α β) a = (a.fst, a.snd)
-- Std.Tactic.Do.Syntax
Lean.Elab.Tactic.Do.VCGen.Config.mk.inj : ∀ {trivial leave elimLets jp : Bool} {stepLimit : Option ℕ}
  {errorOnMissingSpec debug internalize trivial_1 leave_1 elimLets_1 jp_1 : Bool} {stepLimit_1 : Option ℕ}
  {errorOnMissingSpec_1 debug_1 internalize_1 : Bool},
  { trivial := trivial, leave := leave, elimLets := elimLets, jp := jp, stepLimit := stepLimit,
        errorOnMissingSpec := errorOnMissingSpec, debug := debug, internalize := internalize } =
      { trivial := trivial_1, leave := leave_1, elimLets := elimLets_1, jp := jp_1, stepLimit := stepLimit_1,
        errorOnMissingSpec := errorOnMissingSpec_1, debug := debug_1, internalize := internalize_1 } →
    trivial = trivial_1 ∧
      leave = leave_1 ∧
        elimLets = elimLets_1 ∧
          jp = jp_1 ∧
            stepLimit = stepLimit_1 ∧
              errorOnMissingSpec = errorOnMissingSpec_1 ∧ debug = debug_1 ∧ internalize = internalize_1
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.WF.map : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} [inst : Ord α] {t : Std.DTreeMap.Internal.Impl α β}
  {f : (a : α) → β a → γ a}, t.WF → (Std.DTreeMap.Internal.Impl.map f t).WF
-- Mathlib.Algebra.Order.Sub.Unbundled.Basic
AddLECancellable.tsub_lt_iff_tsub_lt : ∀ {α : Type u_1} [inst : AddCommSemigroup α] [inst_1 : PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α]
  [inst_4 : Sub α] [OrderedSub α] {a b c : α},
  AddLECancellable b → AddLECancellable c → b ≤ a → c ≤ a → (a - b < c ↔ a - c < b)
-- Mathlib.Topology.EMetricSpace.Defs
Subtype.preimage_closedEBall : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {p : α → Prop} (a : { a // p a }) (r : ENNReal),
  Subtype.val ⁻¹' Metric.closedEBall (↑a) r = Metric.closedEBall a r
-- Mathlib.CategoryTheory.Monad.EquivMon
CategoryTheory.Monad.instMonObjFunctor : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → (M : CategoryTheory.Monad C) → CategoryTheory.MonObj M.toFunctor
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.sin_int_mul_two_pi_sub : ∀ (x : ℝ) (n : ℤ), Real.sin (↑n * (2 * Real.pi) - x) = -Real.sin x
-- Mathlib.Order.Hom.CompleteLattice
CompleteLatticeHom.mk.sizeOf_spec : ∀ {α : Type u_8} {β : Type u_9} [inst : CompleteLattice α] [inst_1 : CompleteLattice β] [inst_2 : SizeOf α]
  [inst_3 : SizeOf β] (tosInfHom : sInfHom α β)
  (map_sSup' : ∀ (s : Set α), tosInfHom.toFun (sSup s) = sSup (tosInfHom.toFun '' s)),
  sizeOf { tosInfHom := tosInfHom, map_sSup' := map_sSup' } = 1 + sizeOf tosInfHom
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
PiTensorProduct.reindex.eq_1 : ∀ {ι : Type u_1} {ι₂ : Type u_2} (R : Type u_4) [inst : CommSemiring R] (s : ι → Type u_7)
  [inst_1 : (i : ι) → AddCommMonoid (s i)] [inst_2 : (i : ι) → Module R (s i)] (e : ι ≃ ι₂),
  PiTensorProduct.reindex R s e =
    LinearEquiv.ofLinearMap
      (PiTensorProduct.lift
        ((MultilinearMap.domDomCongrLinearEquiv' R R s (PiTensorProduct R fun i => s (e.symm i)) e).symm
          (PiTensorProduct.tprod R)))
      (PiTensorProduct.lift
        ((MultilinearMap.domDomCongrLinearEquiv' R R s (PiTensorProduct R fun i => s i) e) (PiTensorProduct.tprod R)))
      ⋯ ⋯
-- Mathlib.Probability.Decision.BayesEstimator
/-- The estimation problem admits an argmin estimator with respect to the prior `π`.
That is, we can choose the argmin of the posterior expected loss in a measurable way.  -/
ProbabilityTheory.HasArgminEstimator : {Θ : Type u_1} →
  {𝓧 : Type u_2} →
    {mΘ : MeasurableSpace Θ} →
      {m𝓧 : MeasurableSpace 𝓧} →
        [StandardBorelSpace Θ] →
          [Nonempty Θ] →
            {𝓨 : Type u_4} →
              [MeasurableSpace 𝓨] →
                (Θ → 𝓨 → ENNReal) →
                  (P : ProbabilityTheory.Kernel Θ 𝓧) →
                    [ProbabilityTheory.IsFiniteKernel P] →
                      (π : MeasureTheory.Measure Θ) → [MeasureTheory.IsFiniteMeasure π] → Prop
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.isNormal_iff_lt_succ_and_bsup_eq : ∀ {f : Ordinal.{u} → Ordinal.{max u v}},
  Order.IsNormal f ↔
    (∀ (a : Ordinal.{u}), f a < f (Order.succ a)) ∧
      ∀ (o : Ordinal.{u}), Order.IsSuccLimit o → (o.bsup fun x x_1 => f x) = f o
-- Mathlib.RingTheory.Derivation.Basic
Derivation.compAlgebraMap_apply : ∀ {R : Type u_1} (A : Type u_2) {B : Type u_3} {M : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring A]
  [inst_2 : CommSemiring B] [inst_3 : AddCommMonoid M] [inst_4 : Algebra R A] [inst_5 : Algebra R B]
  [inst_6 : Module A M] [inst_7 : Module B M] [inst_8 : Module R M] [inst_9 : Algebra A B]
  [inst_10 : IsScalarTower R A B] [inst_11 : IsScalarTower A B M] (d : Derivation R B M) (x : A),
  (Derivation.compAlgebraMap A d) x = d ((algebraMap A B) x)
-- Mathlib.GroupTheory.PushoutI
/-- The empty normalized word, representing the identity element of the group.  -/
Monoid.PushoutI.NormalWord.empty : {ι : Type u_1} →
  {G : ι → Type u_2} →
    {H : Type u_3} →
      [inst : (i : ι) → Group (G i)] →
        [inst_1 : Group H] →
          {φ : (i : ι) → H →* G i} → {d : Monoid.PushoutI.NormalWord.Transversal φ} → Monoid.PushoutI.NormalWord d
-- Init.Data.ByteArray.Basic
/-- True if the iterator is past the array's last byte.  -/
ByteArray.Iterator.atEnd : ByteArray.Iterator → Bool
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.size_insert_le : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {k : α},
  (t.insert k).size ≤ t.size + 1
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.liftHom.eq_2 : ∀ {B : Type u₁} [inst : Quiver B] {C : Type u₂} [inst_1 : CategoryTheory.CategoryStruct.{v₂, u₂} C] (F : B ⥤q C)
  (x : CategoryTheory.FreeBicategory B),
  CategoryTheory.FreeBicategory.liftHom F (CategoryTheory.FreeBicategory.Hom.id x) =
    CategoryTheory.CategoryStruct.id (F.obj x)
-- Mathlib.Algebra.Ring.Opposite
RingHom.fromOpposite_apply : ∀ {R : Type u_2} {S : Type u_3} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+* S)
  (hf : ∀ (x y : R), Commute (f x) (f y)), ⇑(f.fromOpposite hf) = ⇑f ∘ MulOpposite.unop
-- Mathlib.Topology.MetricSpace.Isometry
/-- An isometry preserves the diameter in pseudometric spaces.  -/
Isometry.diam_image : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {f : α → β},
  Isometry f → ∀ (s : Set α), Metric.diam (f '' s) = Metric.diam s
-- Mathlib.CategoryTheory.ObjectProperty.Basic
CategoryTheory.ObjectProperty.not_le_iff_exists : ∀ {C : Type u} [inst : CategoryTheory.CategoryStruct.{v, u} C] {P Q : CategoryTheory.ObjectProperty C},
  ¬P ≤ Q ↔ ∃ X, P X ∧ ¬Q X
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.get?_union_of_not_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : LawfulBEq α]
  {k : α}, k ∉ m₂ → (m₁ ∪ m₂).get? k = m₁.get? k
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
/-- The projection from the wide pullback of `(f₁, f₂, f₃)` to the pullback of `f₁` and `f₃`.  -/
CategoryTheory.Limits.ChosenPullback₃.p₁₃ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X₁ X₂ X₃ S : C} →
      {f₁ : X₁ ⟶ S} →
        {f₂ : X₂ ⟶ S} →
          {f₃ : X₃ ⟶ S} →
            {h₁₂ : CategoryTheory.Limits.ChosenPullback f₁ f₂} →
              {h₂₃ : CategoryTheory.Limits.ChosenPullback f₂ f₃} →
                {h₁₃ : CategoryTheory.Limits.ChosenPullback f₁ f₃} →
                  (h : CategoryTheory.Limits.ChosenPullback₃ h₁₂ h₂₃ h₁₃) → h.pullback ⟶ h₁₃.pullback
-- Mathlib.GroupTheory.FixedPointFree
MonoidHom.FixedPointFree.commutatorMap_surjective : ∀ {F : Type u_1} {G : Type u_2} [inst : Group G] [inst_1 : FunLike F G G] [MonoidHomClass F G G] {φ : F} [Finite G],
  MonoidHom.FixedPointFree ⇑φ → Function.Surjective (MonoidHom.commutatorMap ⇑φ)
-- Mathlib.RingTheory.Localization.Algebra
RingHom.toKerIsLocalization_apply : ∀ {R : Type u_1} {S : Type u_2} {P : Type u_3} (Q : Type u_4) [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : CommSemiring P] [inst_3 : CommSemiring Q] {M : Submonoid R} {T : Submonoid P} [inst_4 : Algebra R S]
  [inst_5 : Algebra P Q] [inst_6 : IsLocalization M S] [inst_7 : IsLocalization T Q] (g : R →+* P)
  (hy : M ≤ Submonoid.comap g T) (r : ↥(RingHom.ker g)),
  ↑((RingHom.toKerIsLocalization S Q g hy) r) = (algebraMap R S) ↑r
-- Mathlib.Algebra.Divisibility.Units
isUnit_iff_dvd_one : ∀ {α : Type u_1} [inst : CommMonoid α] {x : α}, IsUnit x ↔ x ∣ 1
-- Lean.Meta.Tactic.Grind.CasesMatch
Lean.Meta.Grind.casesMatch : Lean.MVarId → Lean.Expr → Lean.MetaM (List Lean.MVarId)
-- Mathlib.LinearAlgebra.Dimension.Localization
/-- Given `IsScalarTower R S A`, if `A` is the fraction ring of `S`, then the finrank `finrank R S`
of the left part of the tower equals the finrank `finrank R A` of the whole tower.

See `IsFractionRing.finrank_right_eq` for the right version.
See `IsFractionRing.finrank_eq` for the simultaneous version.  -/
IsFractionRing.finrank_left_eq : ∀ (R : Type uR) (S : Type uS) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (A : Type u_1)
  [inst_3 : CommRing A] [inst_4 : Algebra S A] [inst_5 : Algebra R A] [IsScalarTower R S A] [IsFractionRing S A],
  Module.finrank R S = Module.finrank R A
-- Mathlib.Algebra.Group.Pointwise.Set.Finite
Set.Finite.vsub : ∀ {α : Type u_2} {β : Type u_3} [inst : VSub α β] {s t : Set β}, s.Finite → t.Finite → (s -ᵥ t).Finite
-- Mathlib.RingTheory.IsAdjoinRoot
IsAdjoinRoot.algEquiv_symm : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] {f : Polynomial R} [inst_2 : Algebra R S]
  (h : IsAdjoinRoot S f) {T : Type u_1} [inst_3 : Ring T] [inst_4 : Algebra R T] (h' : IsAdjoinRoot T f),
  (h.algEquiv h').symm = h'.algEquiv h
-- Std.Internal.Parsec.ByteArray
/-- Parse `n` bytes from the input into a `ByteSlice`, errors if not enough bytes.
 -/
Std.Internal.Parsec.ByteArray.take : ℕ → Std.Internal.Parsec.ByteArray.Parser ByteSlice
-- Mathlib.AlgebraicGeometry.ColimitsOver
AlgebraicGeometry.Scheme.Cover.ColimitGluingData.pullbackGluedIso.eq_1 : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [inst : P.IsStableUnderBaseChange]
  [inst_1 : P.IsMultiplicative] {S : AlgebraicGeometry.Scheme} {J : Type u_1}
  [inst_2 : CategoryTheory.Category.{v_1, u_1} J] {D : CategoryTheory.Functor J (P.Over ⊤ S)} {𝒰 : S.OpenCover}
  [inst_3 : CategoryTheory.Category.{v_2, u_2} 𝒰.I₀] [inst_4 : AlgebraicGeometry.Scheme.Cover.LocallyDirected 𝒰]
  (d : AlgebraicGeometry.Scheme.Cover.ColimitGluingData D 𝒰)
  [inst_5 :
    ∀ {i j : 𝒰.I₀} (hij : i ⟶ j),
      CategoryTheory.Limits.PreservesColimitsOfShape J
        (CategoryTheory.MorphismProperty.Over.pullback P ⊤ (AlgebraicGeometry.Scheme.Cover.trans 𝒰 hij))]
  [inst_6 : Quiver.IsThin 𝒰.I₀] [inst_7 : Small.{u, u_2} 𝒰.I₀] [inst_8 : AlgebraicGeometry.IsZariskiLocalAtTarget P]
  (i : 𝒰.I₀), d.pullbackGluedIso i = CategoryTheory.MorphismProperty.Over.isoMk ⋯.isoPullback.symm ⋯
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.getKeyD_modify_self : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α]
  (m : Std.DHashMap.Internal.Raw₀ α fun x => β),
  (↑m).WF →
    ∀ [Inhabited α] {k fallback : α} {f : β → β},
      (Std.DHashMap.Internal.Raw₀.Const.modify m k f).getKeyD k fallback = if m.contains k = true then k else fallback
-- Mathlib.Order.BoundedOrder.Lattice
max_ne_top : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : OrderTop α] {a b : α}, a ≠ ⊤ → b ≠ ⊤ → max a b ≠ ⊤
-- Mathlib.Order.UpperLower.Closure
LowerSet.sdiff_idem : ∀ {α : Type u_1} [inst : Preorder α] (s : LowerSet α) (t : Set α), (s.sdiff t).sdiff t = s.sdiff t
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- A subcomplex is closed.  -/
Topology.RelCWComplex.Subcomplex.closed' : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : Topology.RelCWComplex C D]
  (self : Topology.RelCWComplex.Subcomplex C), IsClosed self.carrier
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddLocalization.liftOn₂.eq_1 : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {p : Sort u} (x y : AddLocalization S)
  (f : M → ↥S → M → ↥S → p)
  (H :
    ∀ {a a' : M} {b b' : ↥S} {c c' : M} {d d' : ↥S},
      (AddLocalization.r S) (a, b) (a', b') → (AddLocalization.r S) (c, d) (c', d') → f a b c d = f a' b' c' d'),
  x.liftOn₂ y f H = x.liftOn (fun a b => y.liftOn (f a b) ⋯) ⋯