mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Category.FGModuleCat.Basic
FGModuleCat.instLinearModuleCatForget₂LinearMapIdCarrierObjIsFG : ∀ (R : Type u) [inst : CommRing R],
  CategoryTheory.Functor.Linear R (CategoryTheory.forget₂ (FGModuleCat R) (ModuleCat R))
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomMulAct.instSMulForall.eq_1 : ∀ {M : Type u_1} {β : Type u_2} {α : Type u_3} [inst : SMul M α],
  DomMulAct.instSMulForall = { smul := fun c f a => f (DomMulAct.mk.symm c • a) }
-- Mathlib.Algebra.Group.Subsemigroup.MulOpposite
/-- Pull a subsemigroup back to an opposite subsemigroup along `MulOpposite.unop`  -/
Subsemigroup.op : {M : Type u_2} → [inst : Mul M] → Subsemigroup M → Subsemigroup Mᵐᵒᵖ
-- Init.Data.Dyadic.Round
_private.Init.Data.Dyadic.Round.0.Rat.toDyadic.match_1.eq_2 : ∀ (motive : ℤ → Sort u_1) (n : ℕ) (h_1 : (n : ℕ) → motive (Int.ofNat n)) (h_2 : (n : ℕ) → motive (Int.negSucc n)),
  (match Int.negSucc n with
    | Int.ofNat n => h_1 n
    | Int.negSucc n => h_2 n) =
    h_2 n
-- Mathlib.Analysis.Calculus.SmoothSeries
/-- Consider a series of functions `∑' i, f i x`. Assume that each individual function `f i` is of
class `C^N`, and moreover there is a uniform summable upper bound on the `k`-th derivative
for each `k ≤ N`. Then the series is also `C^N`.  -/
contDiff_tsum : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜]
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedAddCommGroup F] [CompleteSpace F]
  [inst_6 : NormedSpace 𝕜 F] {f : α → E → F} {v : ℕ → α → ℝ} {N : ℕ∞},
  (∀ (i : α), ContDiff 𝕜 (↑N) (f i)) →
    (∀ (k : ℕ), ↑k ≤ N → Summable (v k)) →
      (∀ (k : ℕ) (i : α) (x : E), ↑k ≤ N → ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i) →
        ContDiff 𝕜 ↑N fun x => ∑' (i : α), f i x
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
AlgHom.mem_range : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Semiring B] [inst_4 : Algebra R B] (φ : A →ₐ[R] B) {y : B}, y ∈ φ.range ↔ ∃ x, φ x = y
-- Init.Internal.Order.Basic
Lean.Order.CompleteLattice.sup_spec : ∀ {α : Sort u} [inst : Lean.Order.CompleteLattice α] (c : α → Prop),
  Lean.Order.is_sup c (Lean.Order.CompleteLattice.sup c)
-- Mathlib.Algebra.Algebra.Tower
IsScalarTower.Algebra.ext_iff : ∀ {S : Type u} {A : Type v} [inst : CommSemiring S] [inst_1 : Semiring A] {h1 h2 : Algebra S A},
  h1 = h2 ↔
    ∀ (r : S) (x : A),
      (have I := h1;
        r • x) =
        r • x
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.degree_add_le : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] {f g : MvPolynomial σ R},
  m.toSyn (m.degree (f + g)) ≤ max (m.toSyn (m.degree f)) (m.toSyn (m.degree g))
-- Mathlib.Algebra.Category.Grp.FilteredColimits
/-- The bundled additive commutative group giving the filtered colimit of a diagram.  -/
AddCommGrpCat.FilteredColimits.colimit : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    [CategoryTheory.IsFiltered J] → CategoryTheory.Functor J AddCommGrpCat → AddCommGrpCat
-- Mathlib.CategoryTheory.Iso
CategoryTheory.hom_comp_eq_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (g : X ⟶ Y) [inst_1 : CategoryTheory.IsIso g]
  {f : Y ⟶ X}, CategoryTheory.CategoryStruct.comp g f = CategoryTheory.CategoryStruct.id X ↔ f = CategoryTheory.inv g
-- Init.Sym.Lemmas
Lean.Sym.Nat.dvd_eq_false : ∀ (a b : ℕ), decide (a ∣ b) = false → (a ∣ b) = False
-- Batteries.Data.AssocList
Batteries.instInhabitedAssocList.default : {α : Type u} → {β : Type v} → Batteries.AssocList α β
-- Mathlib.Analysis.Calculus.FDeriv.WithLp
PiLp.hasStrictFDerivAt_toLp : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : ι) → NormedAddCommGroup (E i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)] [Finite ι] (p : ENNReal)
  [Fact (1 ≤ p)] (f : (i : ι) → E i), HasStrictFDerivAt (WithLp.toLp p) (↑(PiLp.continuousLinearEquiv p 𝕜 E).symm) f
-- Mathlib.Algebra.Group.Pi.Lemmas
Function.update_div : ∀ {I : Type u} {f : I → Type v} [inst : (i : I) → Div (f i)] [inst_1 : DecidableEq I] (f₁ f₂ : (i : I) → f i) (i : I)
  (x₁ x₂ : f i), Function.update (f₁ / f₂) i (x₁ / x₂) = Function.update f₁ i x₁ / Function.update f₂ i x₂
-- Mathlib.Algebra.Star.StarRingHom
StarRingEquiv.instStarRingEquivClass : ∀ {A : Type u_1} {B : Type u_2} [inst : Add A] [inst_1 : Add B] [inst_2 : Mul A] [inst_3 : Mul B] [inst_4 : Star A]
  [inst_5 : Star B], StarRingEquivClass (A ≃⋆+* B) A B
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.instIsNontrivialOfIsNontrivialOfCompatible : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : ValuativeRel R] {Γ₀ : Type u_3} [inst_2 : LinearOrderedCommMonoidWithZero Γ₀]
  [ValuativeRel.IsNontrivial R] (v : Valuation R Γ₀) [v.Compatible], v.IsNontrivial
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.hom_eval₂ : ∀ {R : Type u} {S₁ : Type v} {S₂ : Type w} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁]
  [inst_2 : CommSemiring S₂] (p : MvPolynomial σ R) (f : R →+* S₁) (φ : S₁ →+* S₂) (g : σ → S₁),
  φ (MvPolynomial.eval₂ f g p) = MvPolynomial.eval₂ (φ.comp f) (fun i => φ (g i)) p
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.gcd_pos_iff : ∀ {d : ℤ} (a : ℤ√d), 0 < a.re.gcd a.im ↔ a ≠ 0
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rcc.pairwise_toList_ne : ∀ {α : Type u} {r : Std.Rcc α} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLE α]
  [inst_5 : Std.Rxc.IsAlwaysFinite α], List.Pairwise (fun a b => a ≠ b) r.toList
-- Mathlib.Order.Bounds.Basic
IsCoinitialFor.mono_left : ∀ {α : Type u_1} [inst : Preorder α] {s t u : Set α}, s ⊆ t → IsCoinitialFor t u → IsCoinitialFor s u
-- Mathlib.RingTheory.MvPolynomial.Homogeneous
MvPolynomial.decomposition.decompose'_eq : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommSemiring R],
  DirectSum.Decomposition.decompose' = fun φ =>
    (DirectSum.mk (fun i => ↥(MvPolynomial.homogeneousSubmodule σ R i)) (Finset.image (⇑Finsupp.degree) φ.support))
      fun m => ⟨(MvPolynomial.homogeneousComponent ↑m) φ, ⋯⟩
-- Mathlib.Tactic.Linter.UnusedInstancesInType
/-- The index of the parameter among the `forall` binders in the type (starting at 0).  -/
_private.Mathlib.Tactic.Linter.UnusedInstancesInType.0.Mathlib.Linter.UnusedInstancesInType.Parameter.idx : Mathlib.Linter.UnusedInstancesInType.Parameter✝ → ℕ
-- Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal
PositiveLinearMap.instModuleComplexPreGNS : {A : Type u_1} → [inst : NonUnitalCStarAlgebra A] → [inst_1 : PartialOrder A] → (f : A →ₚ[ℂ] ℂ) → Module ℂ f.PreGNS
-- Mathlib.Probability.Independence.CharacteristicFunction
ProbabilityTheory.IndepFun.charFunDual_map_fun_add_eq_mul : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {E : Type u_2}
  {mE : MeasurableSpace E} [inst : NormedAddCommGroup E] [BorelSpace E] [SecondCountableTopology E] {X : Ω → E}
  [inst_3 : NormedSpace ℝ E] {Y : Ω → E},
  AEMeasurable X P →
    AEMeasurable Y P →
      ProbabilityTheory.IndepFun X Y P →
        MeasureTheory.charFunDual (MeasureTheory.Measure.map (fun ω => X ω + Y ω) P) =
          MeasureTheory.charFunDual (MeasureTheory.Measure.map X P) *
            MeasureTheory.charFunDual (MeasureTheory.Measure.map Y P)
-- Lean.Meta.Match.MatcherApp.Transform
Lean.Meta.MatcherApp.TransformAltFVars.mk : Array Lean.Expr →
  Array Lean.Expr → Array Lean.Expr → Array Lean.Expr → Array Lean.Expr → Lean.Meta.MatcherApp.TransformAltFVars
-- Mathlib.Tactic.CrossRefAttribute
/-- The database identifier.  -/
Mathlib.CrossRef.Tag.tag : Mathlib.CrossRef.Tag → String
-- Mathlib.Algebra.GroupWithZero.Divisibility
IsPrimal.mul : ∀ {α : Type u_2} [inst : CommMonoidWithZero α] [IsCancelMulZero α] {m n : α}, IsPrimal m → IsPrimal n → IsPrimal (m * n)
-- Mathlib.Order.Category.DistLat
DistLat.ofHom_hom : ∀ {X Y : DistLat} (f : X ⟶ Y), DistLat.ofHom (DistLat.Hom.hom f) = f
-- Init.Data.String.Iterate
/-- Creates an iterator over all characters \(Unicode code points\) in `s`.

Examples:

* `"abc".chars.toList = ['a', 'b', 'c']`

* `"ab∀c".chars.toList = ['a', 'b', '∀', 'c']`
 -/
String.chars : (s : String) → Std.Iter Char
-- Mathlib.Algebra.Group.TypeTags.Basic
toMul_ofMul : ∀ {α : Type u} (x : α), Additive.toMul (Additive.ofMul x) = x
-- Mathlib.Algebra.Algebra.Prod
/-- `Prod.map` of two algebra homomorphisms.  -/
AlgHom.prodMap : {R : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      {C : Type u_4} →
        [inst : CommSemiring R] →
          [inst_1 : Semiring A] →
            [inst_2 : Algebra R A] →
              [inst_3 : Semiring B] →
                [inst_4 : Algebra R B] →
                  [inst_5 : Semiring C] →
                    [inst_6 : Algebra R C] →
                      {D : Type u_5} →
                        [inst_7 : Semiring D] → [inst_8 : Algebra R D] → (A →ₐ[R] B) → (C →ₐ[R] D) → A × C →ₐ[R] B × D
-- Mathlib.Order.Nucleus
Nucleus.ext : ∀ {X : Type u_1} [inst : SemilatticeInf X] {m n : Nucleus X}, (∀ (a : X), m a = n a) → m = n
-- Mathlib.CategoryTheory.Limits.Indization.IndObject
CategoryTheory.Limits.IndObjectPresentation.extend_I : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A B : CategoryTheory.Functor Cᵒᵖ (Type v)}
  (P : CategoryTheory.Limits.IndObjectPresentation A) (η : A ⟶ B) [inst_1 : CategoryTheory.IsIso η],
  (P.extend η).I = P.I
-- Mathlib.Analysis.Convex.Intrinsic
mem_intrinsicInterior : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [inst : Ring 𝕜] [inst_1 : AddCommGroup V] [inst_2 : Module 𝕜 V]
  [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P] {s : Set P} {x : P},
  x ∈ intrinsicInterior 𝕜 s ↔ ∃ y ∈ interior (Subtype.val ⁻¹' s), ↑y = x
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime
/-- The functor `fromDescentDataFunctor : F.DescentData f ⥤ F.DescentData' sq sq₃`, on objects.  -/
CategoryTheory.Pseudofunctor.DescentData'.ofDescentData : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} →
      {ι : Type t} →
        {S : C} →
          {X : ι → C} →
            {f : (i : ι) → X i ⟶ S} →
              (sq : (i j : ι) → CategoryTheory.Limits.ChosenPullback (f i) (f j)) →
                (sq₃ : (i₁ i₂ i₃ : ι) → CategoryTheory.Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)) →
                  F.DescentData f → F.DescentData' sq sq₃
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get?_eq_some_iff : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k : α} {v : β}, Std.DTreeMap.Raw.Const.get? t k = some v ↔ ∃ (h : k ∈ t), Std.DTreeMap.Raw.Const.get t k h = v
-- Init.Data.Iterators.ToIterator
/-- This typeclass provides an iterator for elements of type `γ`.  -/
Std.ToIterator : Type u → (Type w → Type w') → outParam (Type w) → outParam (Type w) → Type (max u w)
-- Mathlib.Topology.Connected.Clopen
ConnectedComponents.coe_ne_coe : ∀ {α : Type u} [inst : TopologicalSpace α] {x y : α},
  ConnectedComponents.mk x ≠ ConnectedComponents.mk y ↔ connectedComponent x ≠ connectedComponent y
-- Mathlib.Data.Set.Finite.Basic
Set.Finite.preimage_embedding : ∀ {α : Type u} {β : Type v} {s : Set β} (f : α ↪ β), s.Finite → (⇑f ⁻¹' s).Finite
-- Mathlib.MeasureTheory.OuterMeasure.AE
MeasureTheory.ae_of_all : ∀ {α : Type u_1} {F : Type u_3} [inst : FunLike F (Set α) ENNReal] [inst_1 : MeasureTheory.OuterMeasureClass F α]
  {p : α → Prop} (μ : F), (∀ (a : α), p a) → ∀ᵐ (a : α) ∂μ, p a
-- Mathlib.Data.ENNReal.Inv
ENNReal.div_ne_zero : ∀ {a b : ENNReal}, a / b ≠ 0 ↔ a ≠ 0 ∧ b ≠ ⊤
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
/-- The coercion of a subgroupoid as a groupoid  -/
CategoryTheory.Subgroupoid.coe : {C : Type u} → [inst : CategoryTheory.Groupoid C] → (S : CategoryTheory.Subgroupoid C) → CategoryTheory.Groupoid ↑S.objs
-- Mathlib.Algebra.Group.Submonoid.MulAction
Submonoid.instSMulSubtypeMem.eq_1 : ∀ {M' : Type u_1} {α : Type u_2} {S' : Type u_4} [inst : SetLike S' M'] (s : S') [inst_1 : SMul M' α],
  Submonoid.instSMulSubtypeMem s = { smul := fun m a => ↑m • a }
-- Mathlib.GroupTheory.Congruence.Basic
Con.to_submonoid_inj : ∀ {M : Type u_1} [inst : MulOneClass M] (c d : Con M), ↑c = ↑d → c = d
-- Mathlib.CategoryTheory.Category.Pairwise
CategoryTheory.Pairwise.instCategory : {ι : Type v} → CategoryTheory.Category.{v, v} (CategoryTheory.Pairwise ι)
-- Lean.Meta.Basic
Lean.Meta.map3MetaM : {m : Type → Type u_1} →
  {β : Sort u_2} →
    {γ : Sort u_3} →
      {δ : Sort u_4} →
        [MonadControlT Lean.MetaM m] →
          [Monad m] → ({α : Type} → (β → γ → δ → Lean.MetaM α) → Lean.MetaM α) → {α : Type} → (β → γ → δ → m α) → m α
-- Mathlib.Algebra.Group.Units.Opposite
AddUnits.coe_unop_opEquiv : ∀ {M : Type u_2} [inst : AddMonoid M] (u : AddUnits Mᵃᵒᵖ),
  ↑(AddOpposite.unop (AddUnits.opEquiv u)) = AddOpposite.unop ↑u
-- Mathlib.Algebra.Lie.OfAssociative
/-- We can regard a module over an associative ring `A` as a Lie ring module over `A` with Lie
bracket equal to its ring commutator.

Note that this cannot be a global instance because it would create a diamond when `M = A`,
specifically we can build two mathematically-different `bracket A A`s:
1. `@Ring.bracket A _` which says `⁅a, b⁆ = a * b - b * a`
2. `(@LieRingModule.ofAssociativeModule A _ A _ _).toBracket` which says `⁅a, b⁆ = a • b`
  (and thus `⁅a, b⁆ = a * b`)

See note [reducible non-instances]  -/
LieRingModule.ofAssociativeModule : {A : Type v} → [inst : Ring A] → {M : Type w} → [inst_1 : AddCommGroup M] → [Module A M] → LieRingModule A M
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
/-- If there is a primitive `n`th root of unity in `R` and `n` is odd, then
`X ^ n + Y ^ n = ∏ (X + μ Y)`, where `μ` varies over the `n`-th roots of unity.  -/
IsPrimitiveRoot.pow_add_pow_eq_prod_add_mul : ∀ {R : Type u_1} [inst : CommRing R] {ζ : R} {n : ℕ} (x y : R) [inst_1 : IsDomain R],
  Odd n → IsPrimitiveRoot ζ n → x ^ n + y ^ n = ∏ ζ ∈ Polynomial.nthRootsFinset n 1, (x + ζ * y)
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Functions
Lean.Meta.Grind.Arith.CommRing.getMulFn : {m : Type → Type} →
  [MonadLiftT Lean.MetaM m] →
    [Lean.MonadError m] →
      [Monad m] → [Lean.Meta.Sym.Arith.MonadCanon m] → [Lean.Meta.Grind.Arith.CommRing.MonadRing m] → m Lean.Expr
-- Mathlib.Analysis.Normed.Algebra.MatrixExponential
Matrix.exp_conjTranspose : ∀ {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 𝔸), NormedSpace.exp A.conjTranspose = (NormedSpace.exp A).conjTranspose
-- Lean.Meta.HaveTelescope
/-- Simplify and then eliminate unused `let`-declarations.  -/
Lean.Meta.ZetaUnusedMode.twoPasses : Lean.Meta.ZetaUnusedMode
-- Mathlib.Algebra.Homology.HomologicalComplex
/-- If `C.d i j` and `C.d i j'` are both allowed, then we must have `j = j'`,
and so the differentials only differ by an `eqToHom`.
 -/
HomologicalComplex.d_comp_eqToHom : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c) {i j j' : ι}
  (rij : c.Rel i j) (rij' : c.Rel i j'),
  CategoryTheory.CategoryStruct.comp (C.d i j') (CategoryTheory.eqToHom ⋯) = C.d i j
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.Iso.unop_inv_hom_id_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} D] {F G : CategoryTheory.Functor C Dᵒᵖ} (e : F ≅ G) (X : C),
  CategoryTheory.CategoryStruct.comp (e.inv.app X).unop (e.hom.app X).unop =
    CategoryTheory.CategoryStruct.id (Opposite.unop (F.obj X))
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKey_modify_self : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α]
  [Inhabited α] {k : α} {f : β k → β k} {h : k ∈ m.modify k f}, (m.modify k f).getKey k h = k
-- Mathlib.Control.Bifunctor
LawfulBifunctor.flip : ∀ {F : Type u₀ → Type u₁ → Type u₂} [inst : Bifunctor F] [LawfulBifunctor F], LawfulBifunctor (flip F)
-- Mathlib.Topology.Algebra.Order.Group
tendsto_zero_iff_abs_tendsto_zero : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : AddCommGroup G] [inst_2 : LinearOrder G] [IsOrderedAddMonoid G]
  [OrderTopology G] {α : Type u_2} {l : Filter α} (f : α → G),
  Filter.Tendsto f l (nhds 0) ↔ Filter.Tendsto (abs ∘ f) l (nhds 0)
-- Mathlib.Algebra.Group.Basic
eq_of_inv_mul_eq_one : ∀ {α : Type u_1} [inst : DivisionMonoid α] {a b : α}, a⁻¹ * b = 1 → a = b
-- Mathlib.NumberTheory.Height.NumberField
_private.Mathlib.NumberTheory.Height.NumberField.0.NumberField.infinitePlace_apply_le_of_prod_le : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] {n : ℕ},
  n ≠ 0 →
    ∀ (B : ℝ) {x : NumberField.RingOfIntegers K},
      ∏ v, (⨆ i, v (![↑x, ↑n] i)) ^ v.mult ≤ B →
        ∀ (v : NumberField.InfinitePlace K), v ↑x ≤ B / ↑n ^ (Height.totalWeight K - 1)
-- Init.Tactics
/-- Configuration for the `exact?` and `apply?` tactics.
 -/
Lean.Parser.Tactic.LibrarySearchConfig : Type
-- Mathlib.Algebra.ContinuedFractions.Basic
GenContFract.instInhabited : {α : Type u_1} → [Inhabited α] → Inhabited (GenContFract α)
-- Mathlib.Data.Fin.SuccPred
Fin.predAbove_right_last : ∀ {n : ℕ} {i : Fin (n + 1)}, i.predAbove (Fin.last (n + 1)) = Fin.last n
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.isoMk_hom_s₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E F : CategoryTheory.PreOneHypercover S}
  (s₀ : E.I₀ ≃ F.I₀) (h₀ : (i : E.I₀) → E.X i ≅ F.X (s₀ i)) (s₁ : ⦃i j : E.I₀⦄ → E.I₁ i j ≃ F.I₁ (s₀ i) (s₀ j))
  (h₁ : ⦃i j : E.I₀⦄ → (k : E.I₁ i j) → E.Y k ≅ F.Y (s₁ k))
  (w₀ :
    autoParam (∀ (i : E.I₀), CategoryTheory.CategoryStruct.comp (h₀ i).hom (F.f (s₀ i)) = E.f i)
      CategoryTheory.PreOneHypercover.isoMk._auto_1)
  (w₁₁ :
    autoParam
      (∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j),
        CategoryTheory.CategoryStruct.comp (h₁ k).hom (F.p₁ (s₁ k)) =
          CategoryTheory.CategoryStruct.comp (E.p₁ k) (h₀ i).hom)
      CategoryTheory.PreOneHypercover.isoMk._auto_3)
  (w₁₂ :
    autoParam
      (∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j),
        CategoryTheory.CategoryStruct.comp (h₁ k).hom (F.p₂ (s₁ k)) =
          CategoryTheory.CategoryStruct.comp (E.p₂ k) (h₀ j).hom)
      CategoryTheory.PreOneHypercover.isoMk._auto_5)
  (a : E.I₀), (CategoryTheory.PreOneHypercover.isoMk s₀ h₀ s₁ h₁ w₀ w₁₁ w₁₂).hom.s₀ a = s₀ a
-- Lean.Elab.PreDefinition.WF.GuessLex
/-- A cache for `evalRecCall`  -/
Lean.Elab.WF.GuessLex.RecCallCache : Type
-- Init.Data.List.SplitOn.Lemmas
List.splitOn_cons_eq_if_modifyHead : ∀ {α : Type u_1} [inst : BEq α] {a : α} (x : α) (xs : List α),
  List.splitOn a (x :: xs) =
    if (x == a) = true then [] :: List.splitOn a xs else List.modifyHead (List.cons x) (List.splitOn a xs)
-- Mathlib.Algebra.Ring.Parity
Even.one_add : ∀ {α : Type u_2} [inst : Semiring α] {a : α}, Even a → Odd (1 + a)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Stepwise.mul_cert : Lean.Grind.CommRing.Poly → ℤ → Lean.Grind.CommRing.Poly → Bool
-- Mathlib.Order.Filter.Ultrafilter.Defs
Filter.le_pure_iff' : ∀ {α : Type u} {f : Filter α} {a : α}, f ≤ pure a ↔ f = ⊥ ∨ f = pure a
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
SchwartzMap.instSub : {E : Type u_5} →
  {F : Type u_6} →
    [inst : NormedAddCommGroup E] →
      [inst_1 : NormedSpace ℝ E] → [inst_2 : NormedAddCommGroup F] → [inst_3 : NormedSpace ℝ F] → Sub (SchwartzMap E F)
-- Mathlib.Data.Finset.Filter
Finset.disjoint_filter_filter : ∀ {α : Type u_1} {s t : Finset α} {p q : α → Prop} [inst : DecidablePred p] [inst_1 : DecidablePred q],
  Disjoint s t → Disjoint (Finset.filter p s) (Finset.filter q t)
-- Mathlib.Algebra.Star.Basic
star_invOf : ∀ {R : Type u_1} [inst : Monoid R] [inst_1 : StarMul R] (r : R) [inst_2 : Invertible r] [inst_3 : Invertible (star r)],
  star ⅟r = ⅟(star r)
-- Mathlib.Data.Stream.Init
Stream'.cons_injective_left : ∀ {α : Type u} (s : Stream' α), Function.Injective fun x => Stream'.cons x s
-- Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
/-- Turán-maximality with `0 < r` transfers across graph isomorphisms.  -/
SimpleGraph.IsTuranMaximal.iso : ∀ {V : Type u_1} [inst : Fintype V] {G : SimpleGraph V} [inst_1 : DecidableRel G.Adj] {r : ℕ} {W : Type u_2}
  [inst_2 : Fintype W] {H : SimpleGraph W} [inst_3 : DecidableRel H.Adj],
  G.IsTuranMaximal r → ∀ (f : G ≃g H), 0 < r → H.IsTuranMaximal r
-- Init.System.IOError
IO.Error.resourceBusy.injEq : ∀ (osCode : UInt32) (details : String) (osCode_1 : UInt32) (details_1 : String),
  (IO.Error.resourceBusy osCode details = IO.Error.resourceBusy osCode_1 details_1) =
    (osCode = osCode_1 ∧ details = details_1)
-- Mathlib.Topology.UnitInterval
unitInterval.subtype_Iic_eq_Icc : ∀ (x : ↑unitInterval), Subtype.val ⁻¹' Set.Iic ↑x = Set.Icc 0 x
-- Mathlib.Algebra.Group.Equiv.TypeTags
AddEquiv.toMultiplicative_symm_apply_apply : ∀ {G : Type u_2} {H : Type u_3} [inst : AddZeroClass G] [inst_1 : AddZeroClass H]
  (f : Multiplicative G ≃* Multiplicative H) (a : G),
  (AddEquiv.toMultiplicative.symm f) a = (AddMonoidHom.toMultiplicative.symm f.toMonoidHom) a
-- Lean.Util.LeanOptions
Lean.instInhabitedLeanOption : Inhabited Lean.LeanOption
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
/-- The cocone obtained from `IsPushout f g inl inr` is a colimit cocone.
 -/
CategoryTheory.IsPushout.isColimit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {Z X Y P : C} →
      {f : Z ⟶ X} →
        {g : Z ⟶ Y} →
          {inl : X ⟶ P} →
            {inr : Y ⟶ P} → (h : CategoryTheory.IsPushout f g inl inr) → CategoryTheory.Limits.IsColimit h.cocone
-- Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
SSet.instBalanced : CategoryTheory.Balanced SSet
-- Mathlib.Order.Interval.Set.Defs
Set.mem_Ioi : ∀ {α : Type u_1} [inst : Preorder α] {b x : α}, x ∈ Set.Ioi b ↔ b < x
-- Mathlib.Algebra.Module.LinearMap.Defs
AddMonoidHom.coe_toNatLinearMap : ∀ {M : Type u_8} {M₂ : Type u_10} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid M₂] (f : M →+ M₂),
  ⇑f.toNatLinearMap = ⇑f
-- Mathlib.Analysis.Normed.Group.Basic
ball_eq' : ∀ {E : Type u_5} [inst : SeminormedCommGroup E] (y : E) (ε : ℝ), Metric.ball y ε = {x | ‖x / y‖ < ε}
-- Mathlib.GroupTheory.OreLocalization.Basic
OreLocalization.div_eq_one : ∀ {R : Type u_1} [inst : Monoid R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S] {s : ↥S}, ↑s /ₒ s = 1
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
LinearMap.separatingLeft_toLinearMap₂'_of_det_ne_zero' : ∀ {R : Type u_1} {n : Type u_11} [inst : CommRing R] [inst_1 : DecidableEq n] [inst_2 : Fintype n] [IsDomain R]
  {M : Matrix n n R}, M.det ≠ 0 → ((Matrix.toLinearMap₂' R) M).SeparatingLeft
-- Mathlib.MeasureTheory.VectorMeasure.Integral
MeasureTheory.transpose_eq_cbmApplyMeasure : ∀ {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G]
  [inst_5 : NormedSpace ℝ G] (μ : MeasureTheory.VectorMeasure X F) (B : E →L[ℝ] F →L[ℝ] G),
  ⇑(μ.transpose B) = MeasureTheory.cbmApplyMeasure μ B
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullback_snd_isIso_of_range_subset : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : AlgebraicGeometry.PresheafedSpace C} (f : X ⟶ Z)
  [hf : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f] (g : Y ⟶ Z),
  Set.range ⇑(CategoryTheory.ConcreteCategory.hom g.base) ⊆ Set.range ⇑(CategoryTheory.ConcreteCategory.hom f.base) →
    CategoryTheory.IsIso (CategoryTheory.Limits.pullback.snd f g)
-- Mathlib.RingTheory.Nilpotent.GeometricallyReduced
Algebra.instIsReducedTensorProductOfIsAlgebraicOfIsGeometricallyReduced : ∀ (k : Type u_3) (A : Type u_4) (K : Type u_5) [inst : Field k] [inst_1 : Ring A] [inst_2 : Algebra k A]
  [inst_3 : Field K] [inst_4 : Algebra k K] [Algebra.IsAlgebraic k K] [Algebra.IsGeometricallyReduced k A],
  IsReduced (TensorProduct k K A)