mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.PrincipalIdealDomain
/-- A principal ideal domain has unique factorization  -/
PrincipalIdealRing.to_uniqueFactorizationMonoid : ∀ {R : Type u} [inst : CommRing R] [IsDomain R] [IsPrincipalIdealRing R], UniqueFactorizationMonoid R
-- Init.Meta.Defs
_private.Init.Meta.Defs.0.Lean.quoteArray.go : {α : Type} → [Lean.Quote α] → Array α → ℕ → Array Lean.Term → Lean.Term
-- Init.Data.SInt.Lemmas
Int64.toInt8_ofIntTruncate : ∀ {n : ℤ}, -2 ^ 63 ≤ n → n < 2 ^ 63 → (Int64.ofIntClamp n).toInt8 = Int8.ofInt n
-- Mathlib.Algebra.Group.Center
Set.decidableMemAddCentralizer : {M : Type u_1} →
  {S : Set M} →
    [inst : Add M] → [(a : M) → Decidable (∀ b ∈ S, b + a = a + b)] → DecidablePred fun x => x ∈ S.addCentralizer
-- Mathlib.CategoryTheory.Subobject.MonoOver
/-- Convenience constructor for an isomorphism in monomorphisms over `X`.  -/
CategoryTheory.MonoOver.isoMk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X : C} →
      {f g : CategoryTheory.MonoOver X} →
        (h : f.obj.left ≅ g.obj.left) →
          autoParam (CategoryTheory.CategoryStruct.comp h.hom g.arrow = f.arrow) CategoryTheory.MonoOver.isoMk._auto_1 →
            (f ≅ g)
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp.Completion
SemiNormedGrp.completion.map_zero : ∀ (V W : SemiNormedGrp), SemiNormedGrp.completion.map 0 = 0
-- Mathlib.Analysis.Analytic.Constructions
/-- Powers of analytic functions (into a normed `𝕜`-algebra) are analytic.  -/
AnalyticAt.pow : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {A : Type u_7} [inst_3 : NormedRing A] [inst_4 : NormedAlgebra 𝕜 A] {f : E → A} {z : E},
  AnalyticAt 𝕜 f z → ∀ (n : ℕ), AnalyticAt 𝕜 (f ^ n) z
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Real.tendsto_logb_atTop : ∀ {b : ℝ}, 1 < b → Filter.Tendsto (Real.logb b) Filter.atTop Filter.atTop
-- Lean.Meta.Tactic.Grind.Split
/-- Creates the anchor reference syntax for the result of `mkSplitAnchorRefInfo`.
 -/
Lean.Meta.Grind.SplitAnchorRefInfo.toSyntax : Lean.Meta.Grind.SplitAnchorRefInfo → Lean.CoreM (Lean.TSyntax `grind)
-- Mathlib.Geometry.Manifold.VectorBundle.Basic
/-- A randomly chosen coordinate change on a `VectorPrebundle` satisfying `IsContMDiff`, given by
the field `exists_coordChange`. Note that `a.contMDiffCoordChange` need not be the same as
`a.coordChange`.  -/
VectorPrebundle.contMDiffCoordChange : (n : WithTop ℕ∞) →
  {𝕜 : Type u_1} →
    {B : Type u_2} →
      {F : Type u_4} →
        {E : B → Type u_6} →
          [inst : NontriviallyNormedField 𝕜] →
            {EB : Type u_7} →
              [inst_1 : NormedAddCommGroup EB] →
                [inst_2 : NormedSpace 𝕜 EB] →
                  {HB : Type u_8} →
                    [inst_3 : TopologicalSpace HB] →
                      (IB : ModelWithCorners 𝕜 EB HB) →
                        [inst_4 : TopologicalSpace B] →
                          [inst_5 : ChartedSpace HB B] →
                            [inst_6 : (x : B) → AddCommMonoid (E x)] →
                              [inst_7 : (x : B) → Module 𝕜 (E x)] →
                                [inst_8 : NormedAddCommGroup F] →
                                  [inst_9 : NormedSpace 𝕜 F] →
                                    [inst_10 : (x : B) → TopologicalSpace (E x)] →
                                      (a : VectorPrebundle 𝕜 F E) →
                                        [ha : VectorPrebundle.IsContMDiff IB a n] →
                                          {e e' : Bundle.Pretrivialization F Bundle.TotalSpace.proj} →
                                            e ∈ a.pretrivializationAtlas → e' ∈ a.pretrivializationAtlas → B → F →L[𝕜] F
-- Mathlib.MeasureTheory.Measure.Hausdorff
MeasureTheory.instIsAddLeftInvariantHausdorffMeasureOfIsIsometricVAdd : ∀ {X : Type u_2} [inst : EMetricSpace X] [inst_1 : MeasurableSpace X] [inst_2 : BorelSpace X] {d : ℝ}
  [inst_3 : AddGroup X] [IsIsometricVAdd X X], (MeasureTheory.Measure.hausdorffMeasure d).IsAddLeftInvariant
-- Mathlib.LinearAlgebra.TensorPower.Basic
TensorPower.gsemiring : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → DirectSum.GSemiring fun i => TensorPower R i M
-- Mathlib.Algebra.Category.ModuleCat.Adjunctions
ModuleCat.FreeMonoidal.εIso_inv_freeMk : ∀ (R : Type u) [inst : CommRing R] (x : PUnit.{u + 1}),
  (CategoryTheory.ConcreteCategory.hom (ModuleCat.FreeMonoidal.εIso R).inv) (ModuleCat.freeMk x) = 1
-- Mathlib.Data.FunLike.Group
FunLike.coeAddMonoidHom.eq_1 : ∀ (F : Type u_1) (α : Type u_2) (β : Type u_3) [inst : FunLike F α β] [inst_1 : AddZero F] [inst_2 : AddZeroClass β]
  [inst_3 : IsZeroApply F α β] [inst_4 : IsAddApply F α β],
  FunLike.coeAddMonoidHom F α β = { toFun := fun f => ⇑f, map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.Data.List.SplitBy
_private.Mathlib.Data.List.SplitBy.0.List.splitBy.loop.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → α → List α → List (List α) → Sort u_2) (ag : α) (r : List α) (acc : List (List α))
  (h_1 : (a : α) → (as : List α) → (b : α) → (r : List α) → (acc : List (List α)) → motive (a :: as) b r acc)
  (h_2 : (ag : α) → (r : List α) → (acc : List (List α)) → motive [] ag r acc),
  (match [], ag, r, acc with
    | a :: as, b, r, acc => h_1 a as b r acc
    | [], ag, r, acc => h_2 ag r acc) =
    h_2 ag r acc
-- Mathlib.Algebra.Order.GroupWithZero.Basic
inv_le_one_of_one_le₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀}
  [ZeroLEOneClass G₀], 1 ≤ a → a⁻¹ ≤ 1
-- Mathlib.Topology.Order.Basic
/-- A set is a neighborhood of `a` if and only if it contains an interval `(l, u)` containing `a`.
 -/
mem_nhds_iff_exists_Ioo_subset : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [NoMaxOrder α] [NoMinOrder α]
  {a : α} {s : Set α}, s ∈ nhds a ↔ ∃ l u, a ∈ Set.Ioo l u ∧ Set.Ioo l u ⊆ s
-- Mathlib.Algebra.CharP.Frobenius
/-- The Frobenius map of an algebra as a Frobenius-semilinear map.  -/
LinearMap.frobenius : (R : Type u_1) →
  [inst : CommSemiring R] →
    (S : Type u_2) →
      [inst_1 : CommSemiring S] →
        (p : ℕ) → [inst_2 : ExpChar R p] → [ExpChar S p] → [inst_4 : Algebra R S] → S →ₛₗ[frobenius R p] S
-- Mathlib.Analysis.Normed.Lp.ProdLp
/-- The projection on the first coordinate in `WithLp`.  -/
WithLp.fst : {p : ENNReal} → {α : Type u_2} → {β : Type u_3} → WithLp p (α × β) → α
-- Mathlib.Algebra.Group.ModEq
AddCommGroup.ModEq.add_iff_left : ∀ {M : Type u_1} [inst : AddCancelCommMonoid M] {a b c d p : M},
  a ≡ b [PMOD p] → (a + c ≡ b + d [PMOD p] ↔ c ≡ d [PMOD p])
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
/-- The preimage of a compact open set under a quasi-compact morphism between schemes is
compact.  -/
AlgebraicGeometry.QuasiCompact.isCompact_preimage : ∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} [self : AlgebraicGeometry.QuasiCompact f] (U : Set ↥Y),
  IsOpen U → IsCompact U → IsCompact (⇑f ⁻¹' U)
-- Mathlib.Order.RelIso.Basic
RelHomClass.wellFounded : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} {F : Type u_5} [inst : FunLike F α β]
  [RelHomClass F r s] (f : F), WellFounded s → WellFounded r
-- Mathlib.Algebra.Order.AddGroupWithTop
LinearOrderedAddCommGroupWithTop.neg_add_cancel_of_ne_top : ∀ {α : Type u_2} [inst : LinearOrderedAddCommGroupWithTop α] {a : α}, a ≠ ⊤ → -a + a = 0
-- Mathlib.Order.ScottContinuity.Prod
/-- If  is Scott continuous on a product space if it is Scott continuous and monotone in each
variable  -/
ScottContinuousOn.fromProd : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  {f : α × β → γ} {D : Set (Set (α × β))},
  (∀ (a : α), ScottContinuousOn ((fun d => Prod.snd '' d) '' D) fun b => f (a, b)) →
    (∀ (b : β), ScottContinuousOn ((fun d => Prod.fst '' d) '' D) fun a => f (a, b)) →
      (∀ (a : α), Monotone fun b => f (a, b)) → (∀ (b : β), Monotone fun a => f (a, b)) → ScottContinuousOn D f
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.maxKey!_erase_le_maxKey! : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α] {k : α}, (t.erase k).isEmpty = false → (cmp (t.erase k).maxKey! t.maxKey!).isLE = true
-- Mathlib.Order.LiminfLimsup
Filter.limsup_sup_filter : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteDistribLattice α] {f : Filter β} {u : β → α} {g : Filter β},
  Filter.limsup u (f ⊔ g) = Filter.limsup u f ⊔ Filter.limsup u g
-- Init.Meta.Defs
Lean.Meta.Rewrite.Config.mk.injEq : ∀ (transparency : Lean.Meta.TransparencyMode) (offsetCnstrs : Bool) (occs : Lean.Meta.Occurrences)
  (newGoals : Lean.Meta.Rewrite.NewGoals) (transparency_1 : Lean.Meta.TransparencyMode) (offsetCnstrs_1 : Bool)
  (occs_1 : Lean.Meta.Occurrences) (newGoals_1 : Lean.Meta.Rewrite.NewGoals),
  ({ transparency := transparency, offsetCnstrs := offsetCnstrs, occs := occs, newGoals := newGoals } =
      { transparency := transparency_1, offsetCnstrs := offsetCnstrs_1, occs := occs_1, newGoals := newGoals_1 }) =
    (transparency = transparency_1 ∧ offsetCnstrs = offsetCnstrs_1 ∧ occs = occs_1 ∧ newGoals = newGoals_1)
-- Mathlib.SetTheory.ZFC.VonNeumann
ZFSet.vonNeumann_of_isSuccPrelimit : ∀ {o : Ordinal.{u}}, Order.IsSuccPrelimit o → ZFSet.vonNeumann o = ZFSet.iUnion fun a => ZFSet.vonNeumann ↑a
-- Lean.Elab.Tactic.Grind.Config
Lean.Elab.Tactic.elabGrindConfigInteractive : Lean.Syntax →
  optParam Lean.Grind.ConfigInteractive { } → optParam Bool true → Lean.Elab.Tactic.TacticM Lean.Grind.Config
-- Mathlib.Topology.LocallyConstant.Basic
LocallyConstant.continuous : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : LocallyConstant X Y),
  Continuous ⇑f
-- Mathlib.Analysis.InnerProductSpace.Continuous
/-- When an inner product space `E` over `𝕜` is considered as a real normed space, its inner
product satisfies `IsBoundedBilinearMap`.

In order to state these results, we need a `NormedSpace ℝ E` instance. We will later establish
such an instance by restriction-of-scalars, `InnerProductSpace.rclikeToReal 𝕜 E`, but this
instance may be not definitionally equal to some other “natural” instance. So, we assume
`[NormedSpace ℝ E]`.
 -/
isBoundedBilinearMap_inner : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : NormedSpace ℝ E] [IsScalarTower ℝ 𝕜 E], IsBoundedBilinearMap ℝ fun p => inner 𝕜 p.1 p.2
-- Mathlib.Order.Category.Lat
/-- Construct a bundled `Lat` from the underlying type and typeclass.  -/
Lat.of : (X : Type u_1) → [Lattice X] → Lat
-- Mathlib.LinearAlgebra.TensorPower.Symmetric
/-- The pure tensors (i.e. the elements of the image of `SymmetricPower.tprod`) span the symmetric
tensor power.  -/
SymmetricPower.span_tprod_eq_top : ∀ (R ι : Type u) [inst : CommSemiring R] (M : Type v) [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  Submodule.span R (Set.range ⇑(SymmetricPower.tprod R)) = ⊤
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Matrix.Nondegenerate.toLinearMap₂' : ∀ {R : Type u_1} {n : Type u_11} {m : Type u_12} [inst : CommRing R] [inst_1 : DecidableEq m] [inst_2 : Fintype m]
  [inst_3 : DecidableEq n] [inst_4 : Fintype n] {M : Matrix m n R},
  M.Nondegenerate → ((Matrix.toLinearMap₂' R) M).Nondegenerate
-- Lean.Elab.PreDefinition.Main
Lean.Elab.ensureFunIndReservedNamesAvailable : Array Lean.Elab.PreDefinition → Lean.MetaM Unit
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.contains_union_of_left : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [EquivBEq α] [LawfulHashable α],
  (↑m₁).WF → (↑m₂).WF → ∀ {k : α}, m₁.contains k = true → (m₁.union m₂).contains k = true
-- Mathlib.RepresentationTheory.Coinduced
Rep.coindIso.eq_1 : ∀ {k : Type u} {G : Type v} {H : Type w} [inst : CommRing k] [inst_1 : Monoid G] [inst_2 : Monoid H] (φ : G →* H)
  (A : Rep.{max u w, u, v} k G), Rep.coindIso φ A = Rep.mkIso (Representation.Equiv.mk (Rep.coindVEquiv φ A) ⋯)
-- Mathlib.LinearAlgebra.Ray
/-- The setoid of the `SameRay` relation for the subtype of nonzero vectors.  -/
RayVector.Setoid : (R : Type u_1) →
  [inst : CommSemiring R] →
    [inst_1 : PartialOrder R] →
      [IsStrictOrderedRing R] → (M : Type u_2) → [inst_3 : AddCommMonoid M] → [Module R M] → Setoid (RayVector R M)
-- Mathlib.Topology.Order
IndiscreteTopology.of_forall_inseparable : ∀ {α : Type u} [inst : TopologicalSpace α], (∀ (x y : α), Inseparable x y) → IndiscreteTopology α
-- Mathlib.MeasureTheory.Measure.Haar.Basic
MeasureTheory.Measure.haar.chaar_mem_clPrehaar : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalGroup G]
  (K₀ : TopologicalSpace.PositiveCompacts G) (V : TopologicalSpace.OpenNhdsOf 1),
  MeasureTheory.Measure.haar.chaar K₀ ∈ MeasureTheory.Measure.haar.clPrehaar (↑K₀) V
-- Mathlib.CategoryTheory.Elements
/-- The functor out of the category of elements which forgets the element.  -/
CategoryTheory.CategoryOfElements.π : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (F : CategoryTheory.Functor C (Type w)) → CategoryTheory.Functor F.Elements C
-- Std.Tactic.BVDecide.LRAT.Internal.Assignment
Std.Tactic.BVDecide.LRAT.Internal.Assignment.neg.sizeOf_spec : sizeOf Std.Tactic.BVDecide.LRAT.Internal.Assignment.neg = 1
-- Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective
CategoryTheory.Limits.pullback.diagonalObj.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : C} (f f_1 : X ⟶ Y) (e_f : f = f_1)
  [inst_1 : CategoryTheory.Limits.HasPullback f f],
  CategoryTheory.Limits.pullback.diagonalObj f = CategoryTheory.Limits.pullback.diagonalObj f_1
-- Mathlib.AlgebraicGeometry.Morphisms.Constructors
/-- If `P` respects isos, then `stalkwise P` is local at the source.  -/
AlgebraicGeometry.stalkwise_isZariskiLocalAtSource_of_respectsIso : ∀ {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop},
  (RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => P) →
    AlgebraicGeometry.IsZariskiLocalAtSource (AlgebraicGeometry.stalkwise fun {R S} [CommRing R] [CommRing S] => P)
-- Mathlib.ModelTheory.Satisfiability
FirstOrder.Language.Theory.models_formula_iff_onTheory_models_equivSentence : ∀ {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {φ : L.Formula α},
  T ⊨ᵇ φ ↔ (L.lhomWithConstants α).onTheory T ⊨ᵇ FirstOrder.Language.Formula.equivSentence φ
-- Mathlib.Data.Nat.Cast.Order.Field
Nat.one_sub_one_div_cast_nonneg : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [AddRightMono α] (n : ℕ),
  0 ≤ 1 - 1 / ↑n
-- Mathlib.Order.CompleteBooleanAlgebra
CompleteBooleanAlgebra.toHImp : {α : Type u_1} → [self : CompleteBooleanAlgebra α] → HImp α
-- Mathlib.LinearAlgebra.Multilinear.Basic
/-- In the specific case of multilinear maps on spaces indexed by `Fin (n+1)`, where one can build
an element of `∀ (i : Fin (n+1)), M i` using `cons`, one can express directly the multiplicativity
of a multilinear map along the first variable.  -/
MultilinearMap.snoc_smul : ∀ {R : Type uR} {n : ℕ} {M : Fin n.succ → Type v} {M₂ : Type v₂} [inst : Semiring R]
  [inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)] [inst_2 : AddCommMonoid M₂]
  [inst_3 : (i : Fin n.succ) → Module R (M i)] [inst_4 : Module R M₂] (f : MultilinearMap R M M₂)
  (m : (i : Fin n) → M i.castSucc) (c : R) (x : M (Fin.last n)), f (Fin.snoc m (c • x)) = c • f (Fin.snoc m x)
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.smulCommClass_left : ∀ {R' : Type u_1} {α : Type u_2} {β : Type u_3} [inst : NonAssocSemiring R'] [inst_1 : SMul R' β] [inst_2 : SMul α β]
  [SMulCommClass R' α β] (S : Subsemiring R'), SMulCommClass (↥S) α β
-- Init.Data.List.Lemmas
List.flatten.eq_def : ∀ {α : Type u_1} (x : List (List α)),
  x.flatten =
    match x with
    | [] => []
    | l :: L => l.append L.flatten
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
/-- The construction `simplicialInsert` describes inserting an element in a list of integer and
moving it to its "right place" according to the simplicial relations. Somewhat miraculously,
the algorithm is the same for the first or the fifth simplicial relations, making it "valid"
when we treat the list as a normal form for a morphism satisfying `P_δ`, or for a morphism
satisfying `P_σ`!

This is similar in nature to `List.orderedInsert`, but note that we increment one of the element
every time we perform an exchange, making it a different construction.  -/
SimplexCategoryGenRel.simplicialInsert : ℕ → List ℕ → List ℕ
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.units_coeff_zero_smul : ∀ {R : Type u} [inst : CommRing R] [IsDomain R] (c : (Polynomial R)ˣ) (p : Polynomial R), (↑c).coeff 0 • p = ↑c * p
-- Std.Data.DTreeMap.Internal.Cell
/-- Internal implementation detail of the tree map  -/
Std.DTreeMap.Internal.Cell.get? : {α : Type u} →
  {β : α → Type v} →
    [inst : Ord α] →
      [Std.OrientedOrd α] → [Std.LawfulEqOrd α] → {k : α} → Std.DTreeMap.Internal.Cell α β (compare k) → Option (β k)
-- Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations
/-- Lemma 3.3 (b) from [Geck](Geck2017).  -/
RootPairing.GeckConstruction.lie_h_f : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Finite ι] [inst_1 : CommRing R]
  [inst_2 : IsDomain R] [inst_3 : CharZero R] [inst_4 : AddCommGroup M] [inst_5 : Module R M] [inst_6 : AddCommGroup N]
  [inst_7 : Module R N] {P : RootPairing ι R M N} [inst_8 : P.IsCrystallographic] {b : P.Base} [inst_9 : Fintype ι]
  (i j : ↥b.support),
  ⁅RootPairing.GeckConstruction.h j, RootPairing.GeckConstruction.f i⁆ =
    -b.cartanMatrix i j • RootPairing.GeckConstruction.f i
-- Mathlib.GroupTheory.Commutator.Basic
commutator_eq_bot_iff_center_eq_top : ∀ (G : Type u_1) [inst : Group G], commutator G = ⊥ ↔ Subgroup.center G = ⊤
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.valueGroupOrderIso₀_symm_restrict : ∀ {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] {R : Type u_3} [inst_1 : Ring R] (v : Valuation R Γ₀)
  (b : R), (WithVal.valueGroupOrderIso₀ v).symm (v.restrict b) = Valued.v.restrict (WithVal.toVal v b)
-- Mathlib.CategoryTheory.LiftingProperties.Over
CategoryTheory.HasLiftingProperty.over : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {A B X Y : CategoryTheory.Over S} (i : A ⟶ B)
  (p : X ⟶ Y) [CategoryTheory.HasLiftingProperty (CategoryTheory.Over.Hom.left i) (CategoryTheory.Over.Hom.left p)],
  CategoryTheory.HasLiftingProperty i p
-- Mathlib.Algebra.Free
AddMagma.FreeAddSemigroup.hom_ext_iff : ∀ {α : Type u} [inst : Add α] {β : Type v} [inst_1 : AddSemigroup β] {f g : AddMagma.FreeAddSemigroup α →ₙ+ β},
  f = g ↔ f.comp AddMagma.FreeAddSemigroup.of = g.comp AddMagma.FreeAddSemigroup.of
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.toLinearquiv_ofIsHomeomorph : ∀ {S : Type u_1} [inst : Semiring S] {S₁ : Type u_6} {M : Type u_7} {M₁ : Type u_8} [inst_1 : Semiring S₁]
  {σ : S →+* S₁} {σ' : S₁ →+* S} [inst_2 : RingHomInvPair σ σ'] [inst_3 : RingHomInvPair σ' σ]
  [inst_4 : TopologicalSpace M] [inst_5 : AddCommMonoid M] [inst_6 : Module S M] [inst_7 : TopologicalSpace M₁]
  [inst_8 : AddCommMonoid M₁] [inst_9 : Module S₁ M₁] {f : M ≃ₛₗ[σ] M₁} (hf : IsHomeomorph ⇑f),
  ↑(ContinuousLinearEquiv.ofIsHomeomorph f hf) = f
-- Mathlib.AlgebraicGeometry.Cover.Over
/-- The pullback of a cover of `S`-schemes along a morphism of `S`-schemes. This is not
definitionally equal to `AlgebraicGeometry.Scheme.Cover.pullback₁`, as here we take
the pullback in `Over S`, whose underlying scheme is only isomorphic but not equal to the
pullback in `Scheme`.  -/
AlgebraicGeometry.Scheme.Cover.pullbackCoverOver : {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
  (S : AlgebraicGeometry.Scheme) →
    [inst : P.IsStableUnderBaseChange] →
      [inst_1 : AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving P] →
        {X W : AlgebraicGeometry.Scheme} →
          (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X) →
            (f : W ⟶ X) →
              [inst_2 : W.Over S] →
                [inst_3 : X.Over S] →
                  [AlgebraicGeometry.Scheme.Cover.Over S 𝒰] →
                    [AlgebraicGeometry.Scheme.Hom.IsOver f S] →
                      AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) W
-- Lean.Widget.UserWidget
Lean.Widget.WidgetSource : Type
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.WorkspaceClientCapabilities.mk.sizeOf_spec : ∀ (applyEdit? : Option Bool) (workspaceEdit? : Option Lean.Lsp.WorkspaceEditClientCapabilities),
  sizeOf { applyEdit? := applyEdit?, workspaceEdit? := workspaceEdit? } = 1 + sizeOf applyEdit? + sizeOf workspaceEdit?
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.piEquivalenceFunctorDiscreteCompLim_comp_functorπ : ∀ {α : Type w₂} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasProductsOfShape α C] (a : α),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.piEquivalenceFunctorDiscreteCompLim α).hom
      (CategoryTheory.Limits.Pi.functorπ a) =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.piEquivalenceFunctorDiscrete α C).functor.whiskerLeft (CategoryTheory.Limits.lim.π { as := a }))
      (CategoryTheory.piEquivalenceFunctorDiscreteCompEvaluationIso C a).hom
-- Std.Data.DTreeMap.Internal.Balancing
Std.DTreeMap.Internal.Impl.balanceR!_eq_balance! : ∀ {α : Type u} {β : α → Type v} {k : α} {v : β k} {l r : Std.DTreeMap.Internal.Impl α β},
  l.Balanced →
    r.Balanced →
      Std.DTreeMap.Internal.Impl.BalanceLErasePrecond r.size l.size →
        Std.DTreeMap.Internal.Impl.balanceR! k v l r = Std.DTreeMap.Internal.Impl.balance! k v l r
-- Mathlib.Analysis.Normed.Algebra.Unitization
Unitization.cobounded_eq_aux : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : NormedSpace 𝕜 A] [inst_3 : IsScalarTower 𝕜 A A] [inst_4 : SMulCommClass 𝕜 A A]
  [inst_5 : RegularNormedAlgebra 𝕜 A], Bornology.cobounded (Unitization 𝕜 A) = Bornology.cobounded (Unitization 𝕜 A)
-- Mathlib.Data.Set.Countable
/-- Prove `Set.Countable` from a `Countable` instance on the subtype.  -/
Set.to_countable : ∀ {α : Type u} (s : Set α) [Countable ↑s], s.Countable
-- Mathlib.Tactic.Simps.Basic
_private.Mathlib.Tactic.Simps.Basic.0.Simps.elabSimpsConfig.evalConfigItem : Lean.Elab.ConfigEval.EvalConfigItem Simps.Config
-- Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Complex.integrable_pow_mul_norm_one_add_mul_inv : ∀ (n : ℕ) {z : ℂ}, ‖z‖ < 1 → IntervalIntegrable (fun t => t ^ n * ‖(1 + ↑t * z)⁻¹‖) MeasureTheory.volume 0 1
-- Init.Data.List.Lemmas
List.eq_getElem_of_length_eq_two : ∀ {α : Type u_1} (l : List α) (hl : l.length = 2), l = [l[0], l[1]]
-- Init.Data.List.Find
/-- If `¬ p xs[j]` for all `j < i`, then `i ≤ xs.findIdx p`.  -/
List.le_findIdx_of_not : ∀ {α : Type u_1} {p : α → Bool} {xs : List α} {i : ℕ} (h : i < xs.length),
  (∀ (j : ℕ) (hji : j < i), p xs[j] = false) → i ≤ List.findIdx p xs
-- Mathlib.Probability.Independence.Kernel.Indep
ProbabilityTheory.Kernel.iIndep_comap_mem_iff : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {f : ι → Set Ω} {_mΩ : MeasurableSpace Ω}
  {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α},
  ProbabilityTheory.Kernel.iIndep (fun i => MeasurableSpace.comap (fun x => x ∈ f i) ⊤) κ μ ↔
    ProbabilityTheory.Kernel.iIndepSet f κ μ
-- Mathlib.MeasureTheory.Measure.FiniteMeasureProd
MeasureTheory.ProbabilityMeasure.prod_prod : ∀ {α : Type u_1} [inst : MeasurableSpace α] {β : Type u_2} [inst_1 : MeasurableSpace β]
  (μ : MeasureTheory.ProbabilityMeasure α) (ν : MeasureTheory.ProbabilityMeasure β) (s : Set α) (t : Set β),
  (μ.prod ν) (s ×ˢ t) = μ s * ν t
-- Mathlib.CategoryTheory.NatIso
CategoryTheory.NatIso.cancel_natIso_inv_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} (α : F ≅ G) {X : C} {Y : D} (g g' : Y ⟶ G.obj X),
  CategoryTheory.CategoryStruct.comp g (α.inv.app X) = CategoryTheory.CategoryStruct.comp g' (α.inv.app X) ↔ g = g'