mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Matrix.mul_left_inj_of_invertible : ∀ {m : Type u} {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α]
  (A : Matrix n n α) [Invertible A] {x y : Matrix m n α}, x * A = y * A ↔ x = y
-- Mathlib.MeasureTheory.Function.Jacobian
/-- Change of variable formula for differentiable functions, set version: if a function `f` is
injective and differentiable on a measurable set `s`, then the measure of `f '' s` is given by the
integral of `|(f' x).det|` on `s`.
Note that the measurability of `f '' s` is given by `measurable_image_of_fderivWithin`.  -/
MeasureTheory.lintegral_abs_det_fderiv_eq_addHaar_image : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E] {s : Set E}
  {f : E → E} {f' : E → E →L[ℝ] E} [inst_3 : MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.Measure E)
  [μ.IsAddHaarMeasure],
  MeasurableSet s →
    (∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) →
      Set.InjOn f s → ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ = μ (f '' s)
-- Init.Data.Int.Linear
Int.Internal.Linear.cooper_dvd_left_split_dvd2_cert : Int.Internal.Linear.Poly → Int.Internal.Linear.Poly → ℤ → ℕ → ℤ → Int.Internal.Linear.Poly → Bool
-- Lean.Data.Json.FromToJson.Basic
Lean.instFromJsonOption : {α : Type u_1} → [Lean.FromJson α] → Lean.FromJson (Option α)
-- Mathlib.Order.Monotone.Defs
StrictMonoOn.comp_strictAntiOn : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ] {g : β → γ}
  {f : α → β} {s : Set α} {t : Set β}, StrictMonoOn g t → StrictAntiOn f s → Set.MapsTo f s t → StrictAntiOn (g ∘ f) s
-- Mathlib.RingTheory.MvPowerSeries.Inverse
MvPowerSeries.smul_inv : ∀ {σ : Type u_1} {k : Type u_3} [inst : Field k] (r : k) (φ : MvPowerSeries σ k), (r • φ)⁻¹ = r⁻¹ • φ⁻¹
-- Mathlib.Algebra.Order.Archimedean.Real.Basic
Real.sInf_def : ∀ (s : Set ℝ), sInf s = -sSup (-s)
-- Mathlib.Order.OmegaCompletePartialOrder
OmegaCompletePartialOrder.Chain.directed : ∀ {α : Type u_2} [inst : Preorder α] (c : OmegaCompletePartialOrder.Chain α), Directed (fun x1 x2 => x1 ≤ x2) ⇑c
-- Init.Data.String.Lemmas.Pattern.Find.Basic
_private.Init.Data.String.Lemmas.Pattern.Find.Basic.0.String.Slice.contains.match_1.splitter : (s : String.Slice) →
  (motive : String.Slice.Pattern.SearchStep s → Sort u_1) →
    (x : String.Slice.Pattern.SearchStep s) →
      ((startPos endPos : s.Pos) → motive (String.Slice.Pattern.SearchStep.matched startPos endPos)) →
        ((x : String.Slice.Pattern.SearchStep s) →
            (∀ (startPos endPos : s.Pos), x = String.Slice.Pattern.SearchStep.matched startPos endPos → False) →
              motive x) →
          motive x
-- Batteries.Data.DList.Lemmas
_private.Batteries.Data.DList.Lemmas.0.Batteries.DList.append.match_1.splitter : {α : Type u_1} →
  (motive : Batteries.DList α → Batteries.DList α → Sort u_2) →
    (x x_1 : Batteries.DList α) →
      ((f : List α → List α) →
          (h₁ : ∀ (l : List α), f l = f [] ++ l) →
            (g : List α → List α) →
              (h₂ : ∀ (l : List α), g l = g [] ++ l) →
                motive { apply := f, invariant := h₁ } { apply := g, invariant := h₂ }) →
        motive x x_1
-- Mathlib.Algebra.Homology.DerivedCategory.HomologySequence
DerivedCategory.HomologySequence.exact₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] (T : CategoryTheory.Pretriangulated.Triangle (DerivedCategory C))
  (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) (n₀ : ℤ),
  { X₁ := (DerivedCategory.homologyFunctor C n₀).obj T.obj₁, X₂ := (DerivedCategory.homologyFunctor C n₀).obj T.obj₂,
      X₃ := (DerivedCategory.homologyFunctor C n₀).obj T.obj₃, f := (DerivedCategory.homologyFunctor C n₀).map T.mor₁,
      g := (DerivedCategory.homologyFunctor C n₀).map T.mor₂, zero := ⋯ }.Exact
-- Mathlib.Order.Defs.PartialOrder
ge_antisymm : ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, b ≤ a → a ≤ b → a = b
-- Init.Data.SInt.Basic
Int64.ofUInt64 : UInt64 → Int64
-- Mathlib.Combinatorics.Additive.DoublingConst
Finset.card_mul_subConst : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : DecidableEq G] (A B : Finset G), ↑A.card * A.subConst B = ↑(A - B).card
-- Std.Http.Data.Headers.Name
/-- Standard Connection header name
 -/
Std.Http.Header.Name.connection : Std.Http.Header.Name
-- Std.Http.Transport
_private.Std.Http.Transport.0.Std.Http.Internal.Mock.SharedState.mk.sizeOf_spec : ∀ (clientToServer serverToClient : Std.CloseableChannel ByteArray),
  sizeOf { clientToServer := clientToServer, serverToClient := serverToClient } =
    1 + sizeOf clientToServer + sizeOf serverToClient
-- Mathlib.Algebra.Notation.Support
Function.mulSupport_update_one : ∀ {ι : Type u_1} {M : Type u_3} [inst : One M] [inst_1 : DecidableEq ι] (f : ι → M) (x : ι),
  Function.mulSupport (Function.update f x 1) = Function.mulSupport f \ {x}
-- Mathlib.Data.Set.Sups
Set.sups_singleton : ∀ {α : Type u_2} [inst : SemilatticeSup α] {s : Set α} {b : α}, s ⊻ {b} = (fun a => a ⊔ b) '' s
-- Mathlib.Algebra.QuadraticDiscriminant
/-- If a polynomial of degree 2 is always nonnegative, then its discriminant is nonpositive  -/
discrim_le_zero : ∀ {K : Type u_1} [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] {a b c : K},
  (∀ (x : K), 0 ≤ a * (x * x) + b * x + c) → discrim a b c ≤ 0
-- Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Real.Gamma_strictMonoOn_Ici : StrictMonoOn Real.Gamma (Set.Ici 2)
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
/-- Continuous multilinear maps on `𝕜^n` with values in `G` are in bijection with `G`, as such a
continuous multilinear map is completely determined by its value on the constant vector made of
ones. We register this bijection as a linear isometry in
`ContinuousMultilinearMap.piFieldEquiv`.  -/
ContinuousMultilinearMap.piFieldEquiv : (𝕜 : Type u) →
  (ι : Type v) →
    (G : Type wG) →
      [inst : NontriviallyNormedField 𝕜] →
        [inst_1 : SeminormedAddCommGroup G] →
          [inst_2 : NormedSpace 𝕜 G] → [inst_3 : Fintype ι] → G ≃ₗᵢ[𝕜] ContinuousMultilinearMap 𝕜 (fun x => 𝕜) G
-- Mathlib.Analysis.Normed.Module.WeakDual
/-- A compact subset of the weak dual of a separable normed space is metrizable.  -/
WeakDual.metrizable_of_isCompact : ∀ (𝕜 : Type u_1) (E : Type u_3) [inst : NontriviallyNormedField 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [TopologicalSpace.SeparableSpace E] (K : Set (WeakDual 𝕜 E)),
  IsCompact K → TopologicalSpace.MetrizableSpace ↑K
-- Mathlib.Data.ENat.Basic
ENat.natCast_add_one_le_iff : ∀ {m : ℕ} {n : ℕ∞}, ↑m + 1 ≤ n ↔ ↑m < n
-- Mathlib.Data.Finset.Lattice.Fold
Finset.inf.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeInf α] [inst_1 : OrderTop α] (s : Finset β) (f : β → α),
  s.inf f = Finset.fold (fun x1 x2 => x1 ⊓ x2) ⊤ f s
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey?_insertManyIfNewUnit_list_of_not_mem_of_mem : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α Unit} [EquivBEq α] [LawfulHashable α],
  m.WF →
    ∀ {l : List α} {k k' : α},
      (k == k') = true →
        k ∉ m → List.Pairwise (fun a b => (a == b) = false) l → k ∈ l → (m.insertManyIfNewUnit l).getKey? k' = some k
-- Std.Do.PostCond
Std.Do.ExceptConds.and_true : ∀ {ps : Std.Do.PostShape} {x : Std.Do.ExceptConds ps}, (x ∧ₑ Std.Do.ExceptConds.true).entails x
-- Mathlib.Analysis.RCLike.Sqrt
RCLike.sqrt_map : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {𝕜' : Type u_2} [inst_1 : RCLike 𝕜'] {a : 𝕜},
  RCLike.im RCLike.I = RCLike.im RCLike.I → RCLike.sqrt ((RCLike.map 𝕜 𝕜') a) = (RCLike.map 𝕜 𝕜') (RCLike.sqrt a)
-- Mathlib.LinearAlgebra.TensorProduct.Tower
TensorProduct.AlgebraTensorModule.curry_injective_iff : ∀ {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {P : Type uP} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module A M]
  [inst_6 : IsScalarTower R A M] [inst_7 : AddCommMonoid N] [inst_8 : Module R N] [inst_9 : AddCommMonoid P]
  [inst_10 : Module R P] [inst_11 : Module A P] [inst_12 : IsScalarTower R A P] {a₁ a₂ : TensorProduct R M N →ₗ[A] P},
  a₁ = a₂ ↔ TensorProduct.AlgebraTensorModule.curry a₁ = TensorProduct.AlgebraTensorModule.curry a₂
-- Mathlib.Analysis.SpecialFunctions.Complex.Arg
Complex.abs_arg_sub_arg_lt : ∀ (x y : ℂ), |x.arg - y.arg| < 2 * Real.pi
-- Lean.Elab.MutualInductive
Lean.Elab.Command.instInhabitedElabHeaderResult : Inhabited Lean.Elab.Command.ElabHeaderResult
-- Lean.Parser
Lean.PrettyPrinter.Formatter.mkAntiquot.formatter : String → Lean.SyntaxNodeKind → optParam Bool true → optParam Bool true → Lean.PrettyPrinter.Formatter
-- Std.Http.Data.URI.Basic
/-- Sets the user information with username and optional password.
The strings will be automatically percent-encoded.
 -/
Std.Http.URI.Builder.setUserInfo : Std.Http.URI.Builder → String → optParam (Option String) none → Std.Http.URI.Builder
-- Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
CategoryTheory.PreOneHypercover.cylinder_I₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S}
  {F : CategoryTheory.PreOneHypercover S} [inst_1 : CategoryTheory.Limits.HasPullbacks C] (f g : E.Hom F)
  (p q : (i : E.I₀) × F.I₁ (f.s₀ i) (g.s₀ i)),
  (CategoryTheory.PreOneHypercover.cylinder f g).I₁ p q = ULift.{max w w', w} (E.I₁ p.fst q.fst)
-- Mathlib.Algebra.Polynomial.FieldDivision
/-- An irreducible polynomial over a field must have positive degree.  -/
Irreducible.degree_pos : ∀ {F : Type u_1} [inst : DivisionSemiring F] {f : Polynomial F}, Irreducible f → 0 < f.degree
-- Mathlib.Topology.Order.LiminfLimsup
Antitone.liminf_nhdsGT_eq_iSup₂_of_exists_gt : ∀ {α : Type u_2} {β : Type u_3} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α]
  [DenselyOrdered α] [inst_4 : CompleteLattice β] {f : α → β},
  Antitone f → ∀ (a : α), (∃ b, a < b) → Filter.liminf f (nhdsWithin a (Set.Ioi a)) = ⨆ r, ⨆ (_ : r > a), f r
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.contains_minKeyD : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → t.isEmpty = false → ∀ {fallback : α}, t.contains (t.minKeyD fallback) = true
-- Lean.Meta.CompletionName
/-- Checks whether a given name is internal due to something other than `_private`.
Correctly deals with names like `_private.<SomeNamespace>.0.<SomeType>._sizeOf_1` in a private type
`SomeType`, which `n.isInternal && !isPrivateName n` does not.
 -/
_private.Lean.Meta.CompletionName.0.Lean.Meta.isInternalNameModuloPrivate : Lean.Name → Bool
-- Mathlib.Topology.Semicontinuity.Basic
UpperSemicontinuous.sup : ∀ {α : Type u_4} {β : Type u_5} [inst : TopologicalSpace α] [inst_1 : LinearOrder β] {f g : α → β},
  UpperSemicontinuous f → UpperSemicontinuous g → UpperSemicontinuous fun x => max (f x) (g x)
-- Lean.Meta.Match.Match
_private.Lean.Meta.Match.Match.0.Lean.Meta.Match.processLeaf.go : Lean.Meta.Match.Problem → List Lean.Meta.Match.Alt → StateRefT' IO.RealWorld Lean.Meta.Match.State Lean.MetaM Unit
-- Mathlib.Algebra.Category.Ring.Basic
CategoryTheory.Iso.semiRingCatIsoToRingEquiv_toRingHom : ∀ {R S : SemiRingCat} (e : R ≅ S), ↑e.semiRingCatIsoToRingEquiv = SemiRingCat.Hom.hom e.hom
-- Mathlib.Geometry.Euclidean.MongePoint
Affine.Simplex.mongePoint_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 : ℕ} (s : Affine.Simplex ℝ P n) (e : Fin (n + 1) ≃ Fin (m + 1)),
  (s.reindex e).mongePoint = s.mongePoint
-- Mathlib.Data.Set.Constructions
FiniteInter.mk₂ : ∀ {α : Type u_1} {S : Set (Set α)},
  (∀ ⦃s : Set α⦄, s ∈ S → ∀ ⦃t : Set α⦄, t ∈ S → s ∩ t ∈ S) → FiniteInter (insert Set.univ S)
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Restrict
Submodule.subtypeL_apply : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] (p : Submodule R M) (x : ↥p), p.subtypeL x = ↑x
-- Mathlib.Order.SymmDiff
symmDiff_eq_iff_sdiff_eq : ∀ {α : Type u_2} [inst : GeneralizedBooleanAlgebra α] {a b c : α}, a ≤ c → (symmDiff a b = c ↔ c \ a = b)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.DiseqCnstrProof.commRingNorm.inj : ∀ {c : Lean.Meta.Grind.Arith.Cutsat.DiseqCnstr} {e : Lean.Meta.Grind.Arith.CommRing.RingExpr}
  {p : Lean.Grind.CommRing.Poly} {c_1 : Lean.Meta.Grind.Arith.Cutsat.DiseqCnstr}
  {e_1 : Lean.Meta.Grind.Arith.CommRing.RingExpr} {p_1 : Lean.Grind.CommRing.Poly},
  Lean.Meta.Grind.Arith.Cutsat.DiseqCnstrProof.commRingNorm c e p =
      Lean.Meta.Grind.Arith.Cutsat.DiseqCnstrProof.commRingNorm c_1 e_1 p_1 →
    c = c_1 ∧ e = e_1 ∧ p = p_1
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.size_inter_eq_size_left : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  (h₁ : m₁.WF),
  m₂.WF →
    (∀ (a : α), Std.DTreeMap.Internal.Impl.contains a m₁ = true → Std.DTreeMap.Internal.Impl.contains a m₂ = true) →
      (m₁.inter m₂ ⋯).size = m₁.size
-- Init.Grind.Ring.Basic
Lean.Grind.IsCharP.ofNat_eq_zero_iff_of_lt : ∀ {α : Type u_1} (p : ℕ) [inst : Lean.Grind.Semiring α] [Lean.Grind.IsCharP α p] {x : ℕ},
  x < p → (OfNat.ofNat x = 0 ↔ x = 0)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get!_empty : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  [inst_2 : Inhabited β] {a : α}, Std.ExtDHashMap.Const.get! ∅ a = default
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.instEpiModuleCatH0π : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  CategoryTheory.Epi (groupHomology.H0π A)
-- Init.Prelude
/-- `Or.inr` is "right injection" into an `Or`. If `h : b` then `Or.inr h : a ∨ b`.  -/
Or.inr : ∀ {a b : Prop}, b → a ∨ b
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.cokernelBiprodInrIso_inv : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {X Y : C} [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y],
  CategoryTheory.Limits.cokernelBiprodInrIso.inv =
    (CategoryTheory.Limits.biprod.isCokernelInrCokernelFork X Y).desc
      (CategoryTheory.Limits.colimit.cocone (CategoryTheory.Limits.parallelPair CategoryTheory.Limits.biprod.inr 0))
-- Mathlib.Geometry.Manifold.SmoothApprox
Continuous.exists_contDiff_approx : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E]
  [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] {f : E → F} {ε : E → ℝ} (n : ℕ∞),
  Continuous f →
    Continuous ε →
      (∀ (x : E), 0 < ε x) →
        ∃ g, ContDiff ℝ (↑n) g ∧ (∀ (x : E), dist (g x) (f x) < ε x) ∧ Function.support g ⊆ Function.support f
-- Mathlib.Data.Nat.Choose.Basic
Nat.triangle_succ : ∀ (n : ℕ), (n + 1) * (n + 1 - 1) / 2 = n * (n - 1) / 2 + n
-- Mathlib.Analysis.SpecialFunctions.Complex.Circle
AddCircle.homeomorphCircle'_symm_apply : ∀ (x : Circle), AddCircle.homeomorphCircle'.symm x = ↑(↑x).arg
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomMulAct.instGroupOfMulOpposite : {M : Type u_1} → [Group Mᵐᵒᵖ] → Group Mᵈᵐᵃ
-- Mathlib.CategoryTheory.Iso
CategoryTheory.IsIso.inv_eq_of_hom_inv_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} [inst_1 : CategoryTheory.IsIso f]
  {g : Y ⟶ X}, CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.id X → CategoryTheory.inv f = g
-- Init.Internal.Order.Basic
Lean.Order.monotone_apply : ∀ {α : Sort u} {β : α → Sort v} {γ : Sort w} [inst : Lean.Order.PartialOrder γ]
  [inst_1 : (x : α) → Lean.Order.PartialOrder (β x)] (a : α) (f : γ → (x : α) → β x),
  Lean.Order.monotone f → Lean.Order.monotone fun x => f x a
-- Lean.Elab.PreDefinition.WF.Rel
/-- If the `termMeasures` map the packed argument `argType` to `β`, then this function passes to the
continuation a value of type `WellFoundedRelation argType` that is derived from the instance
for `WellFoundedRelation β` using `invImage`.
 -/
Lean.Elab.WF.elabWFRel : {α : Type} →
  Array Lean.Name →
    Lean.Name →
      Lean.Elab.FixedParamPerms →
        Array Lean.Expr →
          Lean.Meta.ArgsPacker →
            Lean.Expr → Lean.Elab.TerminationMeasures → (Lean.Expr → Lean.Elab.TermElabM α) → Lean.Elab.TermElabM α
-- Mathlib.Data.Finsupp.Basic
/-- The equivalence between `(α ⊕ β) →₀ γ` and `(α →₀ γ) × (β →₀ γ)`.

This is the `Finsupp` version of `Equiv.sum_arrow_equiv_prod_arrow`.  -/
Finsupp.sumFinsuppEquivProdFinsupp : {α : Type u_12} → {β : Type u_13} → {γ : Type u_14} → [inst : Zero γ] → (α ⊕ β →₀ γ) ≃ (α →₀ γ) × (β →₀ γ)
-- Mathlib.Combinatorics.Matroid.Dual
Matroid.IsBase.compl_isBase_dual : ∀ {α : Type u_1} {M : Matroid α} {B : Set α}, M.IsBase B → M✶.IsBase (M.E \ B)
-- Mathlib.Order.CompleteLattice.Basic
isGLB_iInf : ∀ {α : Type u_1} {ι : Sort u_4} [inst : CompleteLattice α] {f : ι → α}, IsGLB (Set.range f) (⨅ j, f j)
-- Mathlib.FieldTheory.Finite.Basic
FiniteField.orderOf_frobeniusAlgEquivOfAlgebraic : ∀ (K : Type u_1) [inst : Field K] [inst_1 : Fintype K] (L : Type u_3) [inst_2 : Field L] [inst_3 : Algebra K L]
  [inst_4 : Finite L], orderOf (FiniteField.frobeniusAlgEquivOfAlgebraic K L) = Module.finrank K L
-- Mathlib.Algebra.Group.Pointwise.Set.ListOfFn
Set.mem_pow : ∀ {α : Type u_1} [inst : Monoid α] {s : Set α} {a : α} {n : ℕ}, a ∈ s ^ n ↔ ∃ f, (List.ofFn fun i => ↑(f i)).prod = a
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
AlgebraicGeometry.Scheme.IdealSheafData.isLocalization_away : ∀ {X : AlgebraicGeometry.Scheme} (I : X.IdealSheafData) {U V : ↑X.affineOpens} (h : U ≤ V)
  (f : ↑(X.presheaf.obj (Opposite.op ↑V))),
  U = X.affineBasicOpen f →
    IsLocalization.Away ((Ideal.Quotient.mk (I.ideal V)) f) (↑(X.presheaf.obj (Opposite.op ↑U)) ⧸ I.ideal U)
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.CostructuredArrow.ofCommaFstEquivalenceInverse_map_left_left : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor C T)
  (G : CategoryTheory.Functor D T) (c : C) {X Y : CategoryTheory.Comma ((CategoryTheory.Over.forget c).comp F) G}
  (g : X ⟶ Y),
  ((CategoryTheory.CostructuredArrow.ofCommaFstEquivalenceInverse F G c).map g).left.left =
    CategoryTheory.Over.Hom.left g.left
-- Mathlib.FieldTheory.Perfect
/-- If `f` is a polynomial over a perfect integral domain `R` of characteristic `p`, then there is
a bijection from the set of roots of `Polynomial.expand R p f` to the set of roots of `f`.
It's given by `x ↦ x ^ p`, see `rootsExpandEquivRoots_apply`.  -/
Polynomial.rootsExpandEquivRoots : {R : Type u_1} →
  [inst : CommRing R] →
    [inst_1 : IsDomain R] →
      (p : ℕ) →
        [ExpChar R p] →
          (f : Polynomial R) →
            [inst_3 : DecidableEq R] →
              [PerfectRing R p] → ↥((Polynomial.expand R p) f).roots.toFinset ≃ ↥f.roots.toFinset
-- Lean.Data.Lsp.Extra
Lean.Lsp.WaitForILeansParams.version? : Lean.Lsp.WaitForILeansParams → Option ℕ
-- Mathlib.LinearAlgebra.Matrix.Rank
/-- The rank of a diagonal matrix is the count of non-zero elements on its main diagonal  -/
Matrix.rank_diagonal : ∀ {m : Type um} {R : Type uR} [inst : Field R] [inst_1 : Fintype m] [inst_2 : DecidableEq m] [inst_3 : DecidableEq R]
  (w : m → R), (Matrix.diagonal w).rank = Fintype.card { i // w i ≠ 0 }
-- Lean.Class
/-- If `declName` is a class, return the position of its `outParams`.  -/
Lean.getOutParamPositions? : Lean.Environment → Lean.Name → Option (Array ℕ)
-- Mathlib.RingTheory.Extension.Presentation.Submersive
Algebra.PreSubmersivePresentation.reindex_map : ∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : Algebra.PreSubmersivePresentation R S ι σ) {ι' : Type u_1} {σ' : Type u_2} (e : ι' ≃ ι) (f : σ' ≃ σ) (a : σ'),
  (P.reindex e f).map a = (⇑e.symm ∘ P.map ∘ ⇑f) a
-- Mathlib.MeasureTheory.Measure.Typeclasses.Probability
/-- Note that this is not quite as useful as it looks because the measure takes values in `ℝ≥0∞`.
Thus the subtraction appearing is the truncated subtraction of `ℝ≥0∞`, rather than the
better-behaved subtraction of `ℝ`.  -/
MeasureTheory.prob_compl_eq_one_sub : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α}
  [MeasureTheory.IsProbabilityMeasure μ], MeasurableSet s → μ sᶜ = 1 - μ s
-- Mathlib.ModelTheory.Syntax
/-- Places universal quantifiers on all in-scope bound variables of a bounded formula.  -/
FirstOrder.Language.BoundedFormula.alls : {L : FirstOrder.Language} → {α : Type u'} → {n : ℕ} → L.BoundedFormula α n → L.Formula α
-- Mathlib.Analysis.InnerProductSpace.Harmonic.Basic
/-- Differences of harmonic functions are harmonic.
 -/
InnerProductSpace.HarmonicAt.sub : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  {F : Type u_2} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] {f₁ f₂ : E → F} {x : E},
  InnerProductSpace.HarmonicAt f₁ x → InnerProductSpace.HarmonicAt f₂ x → InnerProductSpace.HarmonicAt (f₁ - f₂) x
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.InlayHintParams.mk.sizeOf_spec : ∀ (toWorkDoneProgressParams : Lean.Lsp.WorkDoneProgressParams) (textDocument : Lean.Lsp.TextDocumentIdentifier)
  (range : Lean.Lsp.Range),
  sizeOf { toWorkDoneProgressParams := toWorkDoneProgressParams, textDocument := textDocument, range := range } =
    1 + sizeOf toWorkDoneProgressParams + sizeOf textDocument + sizeOf range
-- Mathlib.Condensed.Discrete.Colimit
LightCondensed.isoFinYoneda.congr_simp : ∀ (F : CategoryTheory.Functor LightProfiniteᵒᵖ (Type u)) [inst : CategoryTheory.Limits.PreservesFiniteProducts F],
  LightCondensed.isoFinYoneda F = LightCondensed.isoFinYoneda F
-- Mathlib.SetTheory.Cardinal.Basic
/-- The function `a ^< b`, defined as the supremum of `a ^ c` for `c < b`.  -/
Cardinal.powerlt : Cardinal.{u} → Cardinal.{u} → Cardinal.{u}
-- Mathlib.RingTheory.LaurentSeries
LaurentSeries.valuation_X_pow : ∀ (K : Type u_2) [inst : Field K] (s : ℕ),
  Valued.v ((HahnSeries.ofPowerSeries ℤ K) PowerSeries.X ^ s) = WithZero.exp (-↑s)
-- Mathlib.Order.Minimal
Set.minimal_iff_forall_sdiff_singleton : ∀ {α : Type u_2} {P : Set α → Prop} {s : Set α},
  (∀ ⦃s t : Set α⦄, P t → t ⊆ s → P s) → (Minimal P s ↔ P s ∧ ∀ x ∈ s, ¬P (s \ {x}))
-- Mathlib.Analysis.Normed.Ring.InfiniteSum
summable_sum_mul_range_of_summable_norm' : ∀ {R : Type u_1} [inst : NormedRing R] {f g : ℕ → R},
  (Summable fun x => ‖f x‖) →
    Summable f → (Summable fun x => ‖g x‖) → Summable g → Summable fun n => ∑ k ∈ Finset.range (n + 1), f k * g (n - k)
-- ImportGraph.Graph.TransitiveClosure
_private.ImportGraph.Graph.TransitiveClosure.0.Lean.NameMap.transitiveClosure.process : Lean.NameMap (Array Lean.Name) → Lean.NameMap Lean.NameSet → Lean.Name → Array Lean.Name → Lean.NameMap Lean.NameSet
-- Mathlib.CategoryTheory.Sites.Subcanonical
CategoryTheory.GrothendieckTopology.preservesLimitsOfSize_yoneda : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C)
  [inst_1 : J.Subcanonical],
  CategoryTheory.Limits.PreservesLimitsOfSize.{u_1, u_2, v, max u v, u, max u (v + 1)} J.yoneda
-- Init.Data.Array.Lemmas
_private.Init.Data.Array.Lemmas.0.Array.mapM.eq_1 : ∀ {α : Type u} {β : Type v} {m : Type v → Type w} [inst : Monad m] (f : α → m β) (as : Array α),
  Array.mapM f as = Array.mapM.map✝ f as 0 (Array.emptyWithCapacity as.size)
-- Mathlib.Topology.MetricSpace.Defs
dist_toMul : ∀ {X : Type u_1} [inst : Dist X] (a b : Additive X), dist (Additive.toMul a) (Additive.toMul b) = dist a b
-- Mathlib.Data.Real.Basic
_private.Mathlib.Data.Real.Basic.0.Real.inv'_def : ∀ (x : ℝ),
  Real.inv'✝ x =
    match x with
    | { cauchy := a } => { cauchy := a⁻¹ }
-- Mathlib.Order.Interval.Finset.DenselyOrdered
denselyOrdered_set_iff_subsingleton : ∀ {X : Type u_1} [inst : LinearOrder X] [LocallyFiniteOrder X] {s : Set X}, DenselyOrdered ↑s ↔ s.Subsingleton