mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Format.Basic
Std.Format.FlattenAllowability.allow : Bool → Std.Format.FlattenAllowability
-- Init.Data.UInt.Lemmas
USize.toBitVec_pow : ∀ (a : USize) (n : ℕ), (a ^ n).toBitVec = a.toBitVec ^ n
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.instAddCommSemigroup.eq_1 : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : AddCommSemigroup Y],
  LocallyConstant.instAddCommSemigroup = Function.Injective.addCommSemigroup DFunLike.coe ⋯ ⋯
-- Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
MeasureTheory.lpNorm_one : ∀ {α : Type u_1} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} {𝕜 : Type u_3}
  [inst : NormedField 𝕜], p ≠ 0 → μ ≠ 0 → MeasureTheory.lpNorm 1 p μ = μ.real Set.univ ^ p.toReal⁻¹
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnSeries.single_pow : ∀ {Γ : Type u_1} {R : Type u_3} [inst : AddCommMonoid Γ] [inst_1 : PartialOrder Γ] [inst_2 : IsOrderedCancelAddMonoid Γ]
  [inst_3 : Semiring R] (a : Γ) (n : ℕ) (r : R), (HahnSeries.single a) r ^ n = (HahnSeries.single (n • a)) (r ^ n)
-- Std.Data.DHashMap.Internal.AssocList.Basic
Std.DHashMap.Internal.instInhabitedAssocList.default : {α : Type u} → {β : α → Type v} → Std.DHashMap.Internal.AssocList α β
-- Init.Data.Float.Float
/-- Adds two 64-bit floating-point numbers according to IEEE 754. Typically used via the `+` operator.

This function has a logical model in terms of `Float.Model`. It is compiled to the C addition operator.
 -/
Float.add : Float → Float → Float
-- Mathlib.Combinatorics.Enumerative.Partition.Glaisher
Nat.Partition.multipliable_powerSeriesMk_card_restricted : ∀ (R : Type u_1) [inst : TopologicalSpace R] [T2Space R] [inst_2 : CommSemiring R] [IsTopologicalSemiring R]
  (p : ℕ → Prop) [inst_4 : DecidablePred p],
  Multipliable fun i => if p (i + 1) then ∑' (j : ℕ), PowerSeries.X ^ ((i + 1) * j) else 1
-- Mathlib.Order.Closure
/-- Constructor for a closure operator using the weaker idempotency axiom: `f (f x) ≤ f x`.  -/
ClosureOperator.mk' : {α : Type u_1} →
  [inst : PartialOrder α] →
    (f : α → α) → Monotone f → (∀ (x : α), x ≤ f x) → (∀ (x : α), f (f x) ≤ f x) → ClosureOperator α
-- Mathlib.RingTheory.Trace.Defs
/-- If `x` is in the base field `K`, then the trace is `[L : K] * x`.

(If `L` is not finite-dimensional over `K`, then `trace` and `finrank` return `0`.)
 -/
Algebra.trace_algebraMap : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [StrongRankCondition R]
  [Module.Free R S] (x : R), (Algebra.trace R S) ((algebraMap R S) x) = Module.finrank R S • x
-- Batteries.Data.List.Lemmas
List.foldrIdx_nil : ∀ {α : Type u_1} {α_1 : Type u_2} {f : ℕ → α → α_1 → α_1} {i : α_1} {s : ℕ}, List.foldrIdx f i [] s = i
-- Mathlib.Topology.MetricSpace.Closeds
Metric.mem_hausdorffEntourage_of_hausdorffEDist_lt : ∀ {α : Type u_1} [inst : PseudoEMetricSpace α] {s t : Set α} {δ : ENNReal},
  Metric.hausdorffEDist s t < δ → (s, t) ∈ hausdorffEntourage {p | edist p.1 p.2 < δ}
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
AddMonoidAlgebra.mapRingEquiv.eq_1 : ∀ {R : Type u_3} {S : Type u_4} (M : Type u_6) [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : AddMonoid M]
  (e : R ≃+* S),
  AddMonoidAlgebra.mapRingEquiv M e =
    RingEquiv.ofRingHom (AddMonoidAlgebra.mapRingHom M ↑e) (AddMonoidAlgebra.mapRingHom M ↑e.symm) ⋯ ⋯
-- Mathlib.Analysis.InnerProductSpace.Calculus
OpenPartialHomeomorph.contDiffOn_univBall_symm : ∀ {n : ℕ∞} {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {c : E} {r : ℝ},
  ContDiffOn ℝ (↑n) (↑(OpenPartialHomeomorph.univBall c r).symm) (Metric.ball c r)
-- Mathlib.Algebra.Free
/-- Lifts a function `α → β` to a semigroup homomorphism `FreeSemigroup α → β` given
a semigroup `β`.  -/
FreeSemigroup.lift : {α : Type u} → {β : Type v} → [inst : Semigroup β] → (α → β) ≃ (FreeSemigroup α →ₙ* β)
-- Mathlib.LinearAlgebra.Span.Basic
Submodule.disjoint_span_singleton : ∀ {K : Type u_3} {V : Type u_6} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  {s : Submodule K V} {x : V}, Disjoint s (K ∙ x) ↔ x ∈ s → x = 0
-- Mathlib.Data.Set.Operations
Set.prodMk_mem_set_prod_eq : ∀ {α : Type u} {β : Type v} {a : α} {b : β} {s : Set α} {t : Set β}, ((a, b) ∈ s ×ˢ t) = (a ∈ s ∧ b ∈ t)
-- Mathlib.RingTheory.Extension.Generators
Algebra.Generators.Hom.ext : ∀ {R : Type u} {S : Type v} {ι : Type w} {inst : CommRing R} {inst_1 : CommRing S} {inst_2 : Algebra R S}
  {P : Algebra.Generators R S ι} {R' : Type u_1} {S' : Type u_2} {ι' : Type u_3} {inst_3 : CommRing R'}
  {inst_4 : CommRing S'} {inst_5 : Algebra R' S'} {P' : Algebra.Generators R' S' ι'} {inst_6 : Algebra S S'}
  {x y : P.Hom P'}, x.val = y.val → x = y
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.Clopens.coe_compl : ∀ {α : Type u_2} [inst : TopologicalSpace α] (s : TopologicalSpace.Clopens α), ↑sᶜ = (↑s)ᶜ
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
/-- Transfer preservation of a colimit along a natural isomorphism in the functor.  -/
CategoryTheory.Limits.preservesColimit_of_natIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] (K : CategoryTheory.Functor J C)
  {F G : CategoryTheory.Functor C D} (h : F ≅ G) [CategoryTheory.Limits.PreservesColimit K F],
  CategoryTheory.Limits.PreservesColimit K G
-- Init.Data.BitVec.Lemmas
BitVec.ule.eq_1 : ∀ {n : ℕ} (x y : BitVec n), x.ule y = decide (x.toNat ≤ y.toNat)
-- Mathlib.MeasureTheory.Integral.Average
MeasureTheory.setAverage_congr : ∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {μ : MeasureTheory.Measure α} {s t : Set α} {f : α → E}, s =ᵐ[μ] t → ⨍ (x : α) in s, f x ∂μ = ⨍ (x : α) in t, f x ∂μ
-- Std.Data.Internal.List.Associative
Std.Internal.List.perm_filter_self_iff_forall_containsKey : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {f : (a : α) → β a → Bool}
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ((List.filter (fun p => f p.fst p.snd) l).Perm l ↔
      ∀ (a : α) (h : Std.Internal.List.containsKey a l = true), f a (Std.Internal.List.getValueCast a l h) = true)
-- Mathlib.Data.Finsupp.Basic
/-- Given `l`, a finitely supported function from the sigma type `Σ (i : ι), αs i` to `M` and
an index element `i : ι`, `split l i` is the `i`th component of `l`,
a finitely supported function from `as i` to `M`.

This is the `Finsupp` version of `Sigma.curry`.
 -/
Finsupp.split : {ι : Type u_4} → {M : Type u_5} → {αs : ι → Type u_12} → [inst : Zero M] → ((i : ι) × αs i →₀ M) → (i : ι) → αs i →₀ M
-- Mathlib.FieldTheory.RatFunc.Basic
/-- Let `A⟮X⟯ / A[X] / R / R₀` be a tower. If `A[X] / R / R₀` is a scalar tower
then so is `A⟮X⟯ / R / R₀`.  -/
RatFunc.instIsScalarTowerOfIsDomainOfPolynomial : ∀ (R₀ : Type u_1) (R : Type u_2) (A : Type u_3) [inst : CommSemiring R₀] [inst_1 : CommSemiring R] [inst_2 : CommRing A]
  [IsDomain A] [inst_4 : Algebra R₀ (Polynomial A)] [inst_5 : SMul R₀ R] [inst_6 : Algebra R (Polynomial A)]
  [IsScalarTower R₀ R (Polynomial A)], IsScalarTower R₀ R (RatFunc A)
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.involutiveInv.eq_1 : ∀ {α : Type u_2} [inst : InvolutiveInv α], Set.involutiveInv = { toInv := Set.inv, inv_inv := ⋯ }
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.isClique_insert_of_notMem : ∀ {α : Type u_1} {G : SimpleGraph α} {s : Set α} {a : α},
  a ∉ s → (G.IsClique (insert a s) ↔ G.IsClique s ∧ ∀ b ∈ s, G.Adj a b)
-- Mathlib.Algebra.Order.Ring.WithTop
/-- `Nontrivial α` is needed here as otherwise we have `1 * ⊤ = ⊤` but also `0 * ⊤ = 0`.  -/
WithTop.instMulZeroOneClass : {α : Type u_1} → [DecidableEq α] → [MulZeroOneClass α] → [Nontrivial α] → MulZeroOneClass (WithTop α)
-- Mathlib.Data.Finset.Sups
Finset.infs_right_comm : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SemilatticeInf α] (s t u : Finset α), s ⊼ t ⊼ u = s ⊼ u ⊼ t
-- Mathlib.Combinatorics.Quiver.Path
Quiver.Path.isChain_cons_toList_nonempty : ∀ {V : Type u} [inst : Quiver V] {a b : V} (p : Quiver.Path a b),
  List.IsChain (fun x y => Nonempty (y ⟶ x)) (b :: p.toList)
-- Mathlib.GroupTheory.GroupAction.Defs
/-- Note that `hφ = Quotient.out_eq'` is a useful choice here.  -/
MulAction.orbitRel.Quotient.orbit_eq_orbit_out : ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] (x : MulAction.orbitRel.Quotient G α)
  {φ : MulAction.orbitRel.Quotient G α → α}, Function.RightInverse φ Quotient.mk' → x.orbit = MulAction.orbit G (φ x)
-- Mathlib.Data.Sum.Interval
Sum.Lex.instLocallyFiniteOrderTop : {α : Type u_1} →
  {β : Type u_2} →
    [inst : Preorder α] →
      [inst_1 : Preorder β] →
        [LocallyFiniteOrderTop α] → [Fintype β] → [LocallyFiniteOrderTop β] → LocallyFiniteOrderTop (α ⊕ₗ β)
-- Mathlib.Geometry.Euclidean.Sphere.OrthRadius
EuclideanGeometry.Sphere.instHasOrthogonalProjectionRealDirectionOrthRadius : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (s : EuclideanGeometry.Sphere P) (p : P),
  (s.orthRadius p).direction.HasOrthogonalProjection
-- Std.Data.TreeSet.Basic
/-- Transforms the tree set into a list of elements in ascending order.  -/
Std.TreeSet.toList : {α : Type u} → {cmp : α → α → Ordering} → Std.TreeSet α cmp → List α
-- Mathlib.Data.Fintype.Inv
Function.Embedding.invOfMemRange.congr_simp : ∀ {α : Type u_1} {β : Type u_2} [inst : Fintype α] {inst_1 : DecidableEq β} [inst_2 : DecidableEq β] (f : α ↪ β)
  (b b_1 : ↑(Set.range ⇑f)), b = b_1 → f.invOfMemRange b = f.invOfMemRange b_1
-- Mathlib.Algebra.Category.Grp.FilteredColimits
GrpCat.FilteredColimits.colimit_mul_mk_eq : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] [inst_1 : CategoryTheory.IsFiltered J]
  (F : CategoryTheory.Functor J GrpCat) (x y : (j : J) × ↑(F.obj j)) (k : J) (f : x.fst ⟶ k) (g : y.fst ⟶ k),
  GrpCat.FilteredColimits.G.mk F x * GrpCat.FilteredColimits.G.mk F y =
    GrpCat.FilteredColimits.G.mk F
      ⟨k, (CategoryTheory.ConcreteCategory.hom (F.map f)) x.snd * (CategoryTheory.ConcreteCategory.hom (F.map g)) y.snd⟩
-- Mathlib.Algebra.Module.PUnit
PUnit.instSMulCommClass_1 : ∀ {R : Type u_1} {S : Type u_2} [inst : SMul R S], SMulCommClass PUnit.{u_3 + 1} R S
-- Mathlib.AlgebraicTopology.SimplicialObject.Split
CategoryTheory.SimplicialObject.Split.Hom.mk : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {S₁ S₂ : CategoryTheory.SimplicialObject.Split C} →
      (F : S₁.X ⟶ S₂.X) →
        (f : (n : ℕ) → S₁.s.N n ⟶ S₂.s.N n) →
          autoParam
              (∀ (n : ℕ),
                CategoryTheory.CategoryStruct.comp (S₁.s.ι n) (F.app (Opposite.op { len := n })) =
                  CategoryTheory.CategoryStruct.comp (f n) (S₂.s.ι n))
              CategoryTheory.SimplicialObject.Split.Hom.comm._autoParam →
            S₁.Hom S₂
-- Mathlib.Topology.Order.IntermediateValue
isPreconnected_uIoo : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLinearOrder α] [OrderTopology α]
  [DenselyOrdered α] {a b : α}, IsPreconnected (Set.uIoo a b)
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.min?_insert : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {k : α},
  (t.insert k).min? = some (t.min?.elim k fun k' => if cmp k k' = Ordering.lt then k else k')
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsLittleO.comp_fst : ∀ {α : Type u_1} {β : Type u_2} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {f : α → E} {g : α → F}
  {l : Filter α} (l' : Filter β), f =o[l] g → (f ∘ Prod.fst) =o[l ×ˢ l'] (g ∘ Prod.fst)
-- Mathlib.Analysis.SpecialFunctions.Sigmoid
Real.tendsto_sigmoid_atBot : Filter.Tendsto Real.sigmoid Filter.atBot (nhds 0)
-- Init.Data.String.Lemmas.Pattern.Find.String
String.contains_string_eq_internal : ∀ {t s : String}, s.contains t = t.toList.isInfixOf_internal s.toList
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Ideal.prime_generator_of_prime : ∀ {A : Type u_2} [inst : CommRing A] [IsDedekindDomain A] {P : Ideal A},
  Prime P → ∀ [inst_2 : Submodule.IsPrincipal P], Prime (Submodule.IsPrincipal.generator P)
-- Mathlib.CategoryTheory.Category.Basic
/-- Notation for the identity morphism in a category.  -/
CategoryTheory.«term𝟙» : Lean.ParserDescr
-- Mathlib.Topology.Inseparable
SeparationQuotient.instZero.eq_1 : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : Zero X],
  SeparationQuotient.instZero = { zero := SeparationQuotient.mk 0 }
-- Mathlib.Computability.Partrec
Computable.option_casesOn : ∀ {α : Type u_1} {β : Type u_2} {σ : Type u_4} [inst : Primcodable α] [inst_1 : Primcodable β] [inst_2 : Primcodable σ]
  {o : α → Option β} {f : α → σ} {g : α → β → σ},
  Computable o → Computable f → Computable₂ g → Computable fun a => Option.casesOn (o a) (f a) (g a)
-- Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects
/-- A zero object is a right unit for categorical product.  -/
CategoryTheory.Limits.prodZeroIso : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroObject C] →
      [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] → (X : C) → X ⨯ 0 ≅ X
-- Mathlib.GroupTheory.Sylow
Sylow.pow_dvd_card_of_pow_dvd_card : ∀ {G : Type u} [inst : Group G] [Finite G] {p n : ℕ} [hp : Fact (Nat.Prime p)] (P : Sylow p G),
  p ^ n ∣ Nat.card G → p ^ n ∣ Nat.card ↥↑P
-- Init.Data.Range.Polymorphic.RangeIterator
_private.Init.Data.Range.Polymorphic.RangeIterator.0.Std.Rxo.Iterator.instIteratorLoop.match_1.eq_1 : ∀ {α : Type u_1} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : LT α] [inst_2 : DecidableLT α]
  {n : Type u_1 → Type u_3} (γ : Type u_1) (Pl : α → γ → ForInStep γ → Prop)
  (motive :
    (it : Std.IterM Id α) → ((b : α) → it.IsPlausibleIndirectOutput b → (c : γ) → n (Subtype (Pl b c))) → Sort u_2)
  (next upperBound : α)
  (f :
    (b : α) →
      { internalState := { next := some next, upperBound := upperBound } }.IsPlausibleIndirectOutput b →
        (c : γ) → n (Subtype (Pl b c)))
  (h_1 :
    (next upperBound : α) →
      (f :
          (b : α) →
            { internalState := { next := some next, upperBound := upperBound } }.IsPlausibleIndirectOutput b →
              (c : γ) → n (Subtype (Pl b c))) →
        motive { internalState := { next := some next, upperBound := upperBound } } f)
  (h_2 :
    (upperBound : α) →
      (f :
          (b : α) →
            { internalState := { next := none, upperBound := upperBound } }.IsPlausibleIndirectOutput b →
              (c : γ) → n (Subtype (Pl b c))) →
        motive { internalState := { next := none, upperBound := upperBound } } f),
  (match { internalState := { next := some next, upperBound := upperBound } }, f with
    | { internalState := { next := some next, upperBound := upperBound } }, f => h_1 next upperBound f
    | { internalState := { next := none, upperBound := upperBound } }, f => h_2 upperBound f) =
    h_1 next upperBound f
-- Mathlib.Algebra.Order.Interval.Basic
/-- Extension for the `positivity` tactic: The length of an interval is always nonnegative.  -/
Mathlib.Meta.Positivity.evalIntervalLength : Mathlib.Meta.Positivity.PositivityExt
-- Mathlib.FieldTheory.IsPerfectClosure
PerfectRing.liftAux_self : ∀ {K : Type u_1} {L : Type u_2} [inst : CommSemiring K] [inst_1 : CommSemiring L] (i : K →+* L) (p : ℕ)
  [inst_2 : IsPRadical i p] [inst_3 : ExpChar L p] [inst_4 : PerfectRing L p], PerfectRing.liftAux i i p = id
-- Mathlib.RingTheory.Localization.AtPrime.Basic
/-- For an `R`-algebra homomorphism `f : S →ₐ[R] P` and prime ideals `J = f⁻¹(K)` lying over `I`,
the induced algebra homomorphism from the localization of `S` at `J` to the localization of `P` at
`K` over the localization of `R` at `I`.

See `localAlgHom` for a variant where the base ring `R` is not localized.  -/
Localization.localAlgHom' : {R : Type u_1} →
  [inst : CommSemiring R] →
    {S : Type u_2} →
      [inst_1 : CommSemiring S] →
        [inst_2 : Algebra R S] →
          {P : Type u_3} →
            [inst_3 : CommSemiring P] →
              (I : Ideal R) →
                [hI : I.IsPrime] →
                  [inst_4 : Algebra R P] →
                    (J : Ideal S) →
                      (K : Ideal P) →
                        [inst_5 : J.IsPrime] →
                          [inst_6 : K.IsPrime] →
                            [inst_7 : J.LiesOver I] →
                              [inst_8 : Algebra (Localization.AtPrime I) (Localization.AtPrime J)] →
                                [Localization.AtPrime.IsLiesOverAlgebra I J] →
                                  [inst_10 : K.LiesOver I] →
                                    [inst_11 : Algebra (Localization.AtPrime I) (Localization.AtPrime K)] →
                                      [Localization.AtPrime.IsLiesOverAlgebra I K] →
                                        (f : S →ₐ[R] P) →
                                          J = Ideal.comap f K →
                                            Localization.AtPrime J →ₐ[Localization.AtPrime I] Localization.AtPrime K
-- Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
/-- The `t` coefficient of an admissible linear change of variables.  -/
WeierstrassCurve.VariableChange.t : {R : Type u} → [inst : CommRing R] → WeierstrassCurve.VariableChange R → R
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
/-- The condition for a square matrix `A` to be self-adjoint with respect to the square matrix
`J`.  -/
Matrix.IsSelfAdjoint : {R : Type u_1} → {n : Type u_11} → [CommRing R] → [Fintype n] → Matrix n n R → Matrix n n R → Prop
-- Mathlib.Topology.Closure
interior_subset_iff : ∀ {X : Type u} [inst : TopologicalSpace X] {s t : Set X}, interior s ⊆ t ↔ ∀ (U : Set X), IsOpen U → U ⊆ s → U ⊆ t
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.get_get? : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {k : α} {h : (m.get? k).isSome = true}, (m.get? k).get h = m.get k ⋯
-- Mathlib.AlgebraicGeometry.StructureSheaf
_private.Mathlib.AlgebraicGeometry.StructureSheaf.0.AlgebraicGeometry.StructureSheaf.localizationtoStalkₗ_mk : ∀ {R M : Type u} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (x : ↑(AlgebraicGeometry.PrimeSpectrum.Top R)) (f : M) (s : ↥x.asIdeal.primeCompl),
  (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.StructureSheaf.localizationtoStalkₗ✝ R M x))
      (LocalizedModule.mk f s) =
    (CategoryTheory.ConcreteCategory.hom
        ((AlgebraicGeometry.structurePresheafInModuleCat R M).germ (PrimeSpectrum.basicOpen ↑s) x ⋯))
      (AlgebraicGeometry.StructureSheaf.const f (↑s) (PrimeSpectrum.basicOpen ↑s) ⋯)
-- Mathlib.Data.Sum.Order
/-- `OrderDual` is antidistributive over `⊕ₗ` up to an order isomorphism.  -/
OrderIso.sumLexDualAntidistrib : (α : Type u_10) → (β : Type u_11) → [inst : LE α] → [inst_1 : LE β] → (α ⊕ₗ β)ᵒᵈ ≃o βᵒᵈ ⊕ₗ αᵒᵈ
-- Mathlib.LinearAlgebra.Matrix.Notation
Matrix.mul_fin_three : ∀ {α : Type u} [inst : AddCommMonoid α] [inst_1 : Mul α]
  (a₁₁ a₁₂ a₁₃ a₂₁ a₂₂ a₂₃ a₃₁ a₃₂ a₃₃ b₁₁ b₁₂ b₁₃ b₂₁ b₂₂ b₂₃ b₃₁ b₃₂ b₃₃ : α),
  !![a₁₁, a₁₂, a₁₃; a₂₁, a₂₂, a₂₃; a₃₁, a₃₂, a₃₃] * !![b₁₁, b₁₂, b₁₃; b₂₁, b₂₂, b₂₃; b₃₁, b₃₂, b₃₃] =
    !![a₁₁ * b₁₁ + a₁₂ * b₂₁ + a₁₃ * b₃₁, a₁₁ * b₁₂ + a₁₂ * b₂₂ + a₁₃ * b₃₂, a₁₁ * b₁₃ + a₁₂ * b₂₃ + a₁₃ * b₃₃;
      a₂₁ * b₁₁ + a₂₂ * b₂₁ + a₂₃ * b₃₁, a₂₁ * b₁₂ + a₂₂ * b₂₂ + a₂₃ * b₃₂, a₂₁ * b₁₃ + a₂₂ * b₂₃ + a₂₃ * b₃₃;
      a₃₁ * b₁₁ + a₃₂ * b₂₁ + a₃₃ * b₃₁, a₃₁ * b₁₂ + a₃₂ * b₂₂ + a₃₃ * b₃₂, a₃₁ * b₁₃ + a₃₂ * b₂₃ + a₃₃ * b₃₃]
-- Mathlib.Order.Filter.Tendsto
Filter.Tendsto.congr : ∀ {α : Type u_1} {β : Type u_2} {f₁ f₂ : α → β} {l₁ : Filter α} {l₂ : Filter β},
  (∀ (x : α), f₁ x = f₂ x) → Filter.Tendsto f₁ l₁ l₂ → Filter.Tendsto f₂ l₁ l₂
-- Lean.Meta.Tactic.Try.Collect
/-- Equation function candidates.  -/
Lean.Meta.Try.Collector.Result.eqnCandidates : Lean.Meta.Try.Collector.Result → Lean.Meta.Try.Collector.OrdSet Lean.Name
-- Mathlib.Probability.Kernel.Composition.Prod
ProbabilityTheory.Kernel.id_prod_eq : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β},
  ProbabilityTheory.Kernel.id =
    (ProbabilityTheory.Kernel.deterministic Prod.fst ⋯).prod (ProbabilityTheory.Kernel.deterministic Prod.snd ⋯)
-- Mathlib.Algebra.Group.Pi.Basic
Pi.involutiveInv : {I : Type u} → {f : I → Type v₁} → [(i : I) → InvolutiveInv (f i)] → InvolutiveInv ((i : I) → f i)
-- Std.Data.DTreeMap.Internal.Balanced
Std.DTreeMap.Internal.Impl.Balanced.eq : ∀ {α : Type u} {β : α → Type v} {sz : ℕ} {k : α} {v : β k} {l r : Std.DTreeMap.Internal.Impl α β},
  (Std.DTreeMap.Internal.Impl.inner sz k v l r).Balanced → sz = l.size + 1 + r.size
-- Mathlib.Data.Prod.Basic
Prod.id_prod : ∀ {α : Type u_1} {β : Type u_2}, (fun p => (p.1, p.2)) = id
-- Mathlib.Algebra.Order.Monoid.Canonical.Defs
CanonicallyOrderedAdd.le_self_add : ∀ {α : Type u_1} {inst : Add α} {inst_1 : LE α} [self : CanonicallyOrderedAdd α] (a b : α), a ≤ a + b
-- Mathlib.Data.Finset.Max
Finset.min'.eq_1 : ∀ {α : Type u_2} [inst : LinearOrder α] (s : Finset α) (H : s.Nonempty), s.min' H = s.inf' H id
-- Mathlib.Analysis.Normed.Module.Alternating.Uncurry.Fin
_private.Mathlib.Analysis.Normed.Module.Alternating.Uncurry.Fin.0.ContinuousAlternatingMap.alternatizeUncurryFinCLM.aux_apply : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : ℕ}
  (f : E →L[𝕜] E [⋀^Fin n]→L[𝕜] F) (v : Fin (n + 1) → E),
  (ContinuousAlternatingMap.alternatizeUncurryFinCLM.aux✝ f) v = ∑ i, (-1) ^ ↑i • (f (v i)) (i.removeNth v)
-- Mathlib.RingTheory.NonUnitalSubring.Defs
/-- `G` is closed under negation  -/
NonUnitalSubring.neg_mem' : ∀ {R : Type u} [inst : NonUnitalNonAssocRing R] (self : NonUnitalSubring R) {x : R},
  x ∈ self.carrier → -x ∈ self.carrier
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.normalCore.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G),
  H.normalCore = { carrier := {a | ∀ (b : G), b + a + -b ∈ H}, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }
-- Mathlib.Analysis.InnerProductSpace.Adjoint
/-- 7.64(c) in [axler2024].  -/
LinearMap.range_adjoint_comp_self : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : InnerProductSpace 𝕜 E] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : FiniteDimensional 𝕜 E] [inst_6 : FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F),
  (LinearMap.adjoint A ∘ₗ A).range = (LinearMap.adjoint A).range
-- Lean.Meta.Tactic.Ext
/-- Information about an extensionality theorem, stored in the environment extension.  -/
Lean.Meta.Ext.ExtTheorem : Type
-- Lean.Data.Lsp.Extra
Lean.Lsp.LineRange.mk.injEq : ∀ (start «end» start_1 end_1 : ℕ),
  ({ start := start, «end» := «end» } = { start := start_1, «end» := end_1 }) = (start = start_1 ∧ «end» = end_1)
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
ZeroAtInftyContinuousMapClass.toContinuousMapClass : ∀ {F : Type u_2} {α : outParam (Type u_3)} {β : outParam (Type u_4)} {inst : TopologicalSpace α} {inst_1 : Zero β}
  {inst_2 : TopologicalSpace β} {inst_3 : FunLike F α β} [self : ZeroAtInftyContinuousMapClass F α β],
  ContinuousMapClass F α β
-- Mathlib.RingTheory.GradedAlgebra.AlgHom
/-- Identity map as a `GradedAlgHom`.  -/
GradedAlgHom.id : (R : Type u_1) →
  {A : Type u_6} →
    {ι : Type u_10} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Algebra R A] →
            [inst_3 : DecidableEq ι] →
              [inst_4 : AddMonoid ι] → (𝒜 : ι → Submodule R A) → [inst_5 : GradedAlgebra 𝒜] → 𝒜 →ₐᵍ[R] 𝒜