mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Matrix.Orthogonal
/-- `Aᵀ` has orthogonal columns iff `A` has orthogonal rows.  -/
Matrix.transpose_hasOrthogonalCols_iff_hasOrthogonalRows : ∀ {α : Type u_1} {n : Type u_2} {m : Type u_3} [inst : Mul α] [inst_1 : AddCommMonoid α] (A : Matrix m n α)
  [inst_2 : Fintype n], A.transpose.HasOrthogonalCols ↔ A.HasOrthogonalRows
-- Std.Do.SPred.Laws
Std.Do.SPred.or_curry : ∀ {σs : List (Type u)} {P Q : Std.Do.SVal.StateTuple σs → Prop},
  ((Std.Do.SVal.curry fun t => { down := P t }) ∨ Std.Do.SVal.curry fun t => { down := Q t }) ⊣⊢ₛ
    Std.Do.SVal.curry fun t => { down := P t ∨ Q t }
-- Mathlib.Combinatorics.Hypergraph.Basic
/-- A vertex is isolated if it is not incident to any edges (including loops).  -/
Hypergraph.IsIsolated : {α : Type u_1} → Hypergraph α → α → Prop
-- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
MeasureTheory.monotone_lintegral : ∀ {α : Type u_1} {x : MeasurableSpace α} (μ : MeasureTheory.Measure α), Monotone (MeasureTheory.lintegral μ)
-- Mathlib.Computability.AkraBazzi.SumTransform
AkraBazziRecurrence.isEquivalent_one_sub_smoothingFn_one : Asymptotics.IsEquivalent Filter.atTop (fun x => 1 - AkraBazziRecurrence.smoothingFn x) fun x => 1
-- Mathlib.RingTheory.Localization.Basic
/-- If an algebra is simultaneously localizations for two submonoids, then an arbitrary algebra
is a localization of one submonoid iff it is a localization of the other.  -/
IsLocalization.isLocalization_iff_of_isLocalization : ∀ {R : Type u_1} [inst : CommSemiring R] (M N : Submonoid R) (S : Type u_2) [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] {P : Type u_3} [inst_3 : CommSemiring P] [IsLocalization M S] [IsLocalization N S]
  [inst_6 : Algebra R P], IsLocalization M P ↔ IsLocalization N P
-- Mathlib.AlgebraicTopology.SimplicialObject.Split
/-- a splitting of the simplicial object  -/
CategoryTheory.SimplicialObject.Split.s : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] → (self : CategoryTheory.SimplicialObject.Split C) → self.X.Splitting
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.fderivLM_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] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : SMulCommClass ℝ 𝕜 F] {n k : ℕ∞} {K : TopologicalSpace.Compacts E} (f : ContDiffMapSupportedIn E F n K),
  ⇑((ContDiffMapSupportedIn.fderivLM 𝕜 n k) f) = if k + 1 ≤ n then fderiv ℝ ⇑f else 0
-- Std.Data.Internal.List.Associative
Std.Internal.List.maxKeyD_eq_getD_maxKey? : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l : List ((a : α) × β a)} {fallback : α},
  Std.Internal.List.maxKeyD l fallback = (Std.Internal.List.maxKey? l).getD fallback
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.mem_spanSingleton : ∀ {R : Type u_1} [inst : CommRing R] (S : Submonoid R) {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  [inst_3 : IsLocalization S P] {x y : P}, x ∈ FractionalIdeal.spanSingleton S y ↔ ∃ z, z • y = x
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.get!_eq_get!_get? : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {a : α}
  [inst_1 : Inhabited (β a)], m.get! a = (m.get? a).get!
-- Aesop.Forward.Match.Types
Aesop.Match.instBEq : BEq Aesop.Match
-- Mathlib.Probability.Distributions.Gaussian.Basic
/-- A finite measure is Gaussian iff its characteristic function has value
`exp (μ[L] * I - Var[L; μ] / 2)` for every `L : Dual ℝ E`.  -/
ProbabilityTheory.isGaussian_iff_charFunDual_eq : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E]
  {μ : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasure μ],
  ProbabilityTheory.IsGaussian μ ↔
    ∀ (L : StrongDual ℝ E),
      MeasureTheory.charFunDual μ L =
        Complex.exp ((∫ (x : E), ↑(L x) ∂μ) * Complex.I - ↑(ProbabilityTheory.variance (⇑L) μ) / 2)
-- Mathlib.Topology.Defs.Basic
/-- `f : α → X` has dense range if its range (image) is a dense subset of `X`.  -/
DenseRange : {X : Type u} → [TopologicalSpace X] → {α : Type u_1} → (α → X) → Prop
-- Batteries.Tactic.SqueezeScope
/-- `squeeze_scope a => tacs` is part of the implementation of `squeeze_scope`.
Inside `tacs`, invocations of `simp` wrapped with `squeeze_wrap a _ => ...` will contribute
to the accounting associated to scope `a`.
 -/
_private.Batteries.Tactic.SqueezeScope.0.Batteries.Tactic.squeezeScopeIn : Lean.ParserDescr
-- Mathlib.Computability.ContextFreeGrammar
ContextFreeRule.Rewrites.below.cons : ∀ {T : Type u_1} {N : Type u_2} {r : ContextFreeRule T N}
  {motive : (a a_1 : List (Symbol T N)) → r.Rewrites a a_1 → Prop} (x : Symbol T N) {s₁ s₂ : List (Symbol T N)}
  (hrs : r.Rewrites s₁ s₂), ContextFreeRule.Rewrites.below hrs → motive s₁ s₂ hrs → ContextFreeRule.Rewrites.below ⋯
-- Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Monoidal
QuadraticModuleCat.toIsometry_inv_leftUnitor : ∀ {R : Type u} [inst : CommRing R] [inst_1 : Invertible 2] {M : QuadraticModuleCat R},
  QuadraticModuleCat.Hom.toIsometry (CategoryTheory.MonoidalCategoryStruct.leftUnitor M).inv =
    M.form.tensorLId.symm.toIsometry
-- Init.Data.List.TakeDrop
List.take_left : ∀ {α : Type u_1} {l₁ l₂ : List α}, List.take l₁.length (l₁ ++ l₂) = l₁
-- Mathlib.RingTheory.Extension.Presentation.Basic
Algebra.Presentation.mem_ker_naive : ∀ {R : Type u} {ι : Type w} {σ : Type t} [inst : CommRing R] {v : ι → MvPolynomial σ R}
  (s : MvPolynomial σ R ⧸ Ideal.span (Set.range v) → MvPolynomial σ R)
  (hs : ∀ (x : MvPolynomial σ R ⧸ Ideal.span (Set.range v)), (Ideal.Quotient.mk (Ideal.span (Set.range v))) (s x) = x)
  (i : ι), v i ∈ (Algebra.Presentation.naive s hs).ker
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.uniformContinuous_toLp : ∀ (p : ENNReal) {ι : Type u_2} (β : ι → Type u_4) [inst : (i : ι) → UniformSpace (β i)],
  UniformContinuous (WithLp.toLp p)
-- Mathlib.Data.Num.Lemmas
Num.bit_to_nat : ∀ (b : Bool) (n : Num), ↑(Num.bit b n) = Nat.bit b ↑n
-- Mathlib.Algebra.Order.Module.Defs
/-- A constructor for `SMulPosMono` requiring you to prove `a₁ ≤ a₂ → a₁ • b ≤ a₂ • b` only when
`0 < b`  -/
SMulPosMono.of_pos : ∀ {α : Type u_1} {β : Type u_2} [inst : Zero α] [inst_1 : Zero β] [inst_2 : SMulWithZero α β] [inst_3 : Preorder α]
  [inst_4 : PartialOrder β], (∀ (b : β), 0 < b → ∀ (a₁ a₂ : α), a₁ ≤ a₂ → a₁ • b ≤ a₂ • b) → SMulPosMono α β
-- Mathlib.Topology.MetricSpace.Infsep
Set.einfsep_eq_iInf : ∀ {α : Type u_1} [inst : EDist α] {s : Set α}, s.einfsep = ⨅ d, Function.uncurry edist ↑d
-- Mathlib.Topology.Instances.ENNReal.Lemmas
/-- Yet another metric characterization of Cauchy sequences on integers. This one is often the
most efficient.  -/
EMetric.cauchySeq_iff_le_tendsto_0 : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoEMetricSpace α] [Nonempty β] [inst_2 : SemilatticeSup β] {s : β → α},
  CauchySeq s ↔ ∃ b, (∀ (n m N : β), N ≤ n → N ≤ m → edist (s n) (s m) ≤ b N) ∧ Filter.Tendsto b Filter.atTop (nhds 0)
-- Mathlib.Geometry.Manifold.Algebra.Monoid
ContMDiffAdd.prod : ∀ {n : WithTop ℕ∞} {𝕜 : Type u_8} [inst : NontriviallyNormedField 𝕜] {E : Type u_9} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_10} [inst_3 : TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) (G : Type u_11)
  [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : Add G] [ContMDiffAdd I n G] {E' : Type u_12}
  [inst_8 : NormedAddCommGroup E'] [inst_9 : NormedSpace 𝕜 E'] {H' : Type u_13} [inst_10 : TopologicalSpace H']
  (I' : ModelWithCorners 𝕜 E' H') (G' : Type u_14) [inst_11 : TopologicalSpace G'] [inst_12 : ChartedSpace H' G']
  [inst_13 : Add G'] [ContMDiffAdd I' n G'], ContMDiffAdd (I.prod I') n (G × G')
-- Std.Data.ExtHashMap.Lemmas
/-- Variant of `getD_map` that holds with `EquivBEq` (i.e. without `LawfulBEq`).  -/
Std.ExtHashMap.getD_map' : ∀ {α : Type u} {β : Type v} {γ : Type w} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {f : α → β → γ} {k : α} {fallback : γ},
  (Std.ExtHashMap.map f m).getD k fallback = (Option.pmap (fun v h => f (m.getKey k h) v) m[k]? ⋯).getD fallback
-- Aesop.Rule
Aesop.instInhabitedLocalNormSimpRule.default : Aesop.LocalNormSimpRule
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.AddGrp.instAddMonObj.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {H : CategoryTheory.AddGrp C}
  [inst_3 : CategoryTheory.IsCommAddMonObj H.X],
  CategoryTheory.AddGrp.instAddMonObj =
    { zero := CategoryTheory.AddGrp.homMk CategoryTheory.AddMonObj.zero.hom,
      add := CategoryTheory.AddGrp.homMk CategoryTheory.AddMonObj.add.hom, zero_add := ⋯, add_zero := ⋯,
      add_assoc := ⋯ }
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.mem_of_mem_union_of_not_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α},
  k ∈ t₁ ∪ t₂ → k ∉ t₂ → k ∈ t₁
-- Lean.Expr
Lean.Expr.updateApp! : Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr
-- Mathlib.Algebra.Category.Grp.Adjunctions
/-- The free functor `Type u ⥤ Group` sending a type `X` to the free group with generators `x : X`.
 -/
GrpCat.free : CategoryTheory.Functor (Type u) GrpCat
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.get?_max! : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] [inst_1 : Inhabited α],
  t ≠ ∅ → t.get? t.max! = some t.max!
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.isBigO_snd_prod' : ∀ {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [inst : SeminormedAddCommGroup E'] [inst_1 : SeminormedAddCommGroup F']
  {l : Filter α} {f' : α → E' × F'}, (fun x => (f' x).2) =O[l] f'
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
CFC.sqrt.eq_1 : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : NonUnitalRing A] [inst_2 : TopologicalSpace A] [inst_3 : StarRing A]
  [inst_4 : Module ℝ A] [inst_5 : SMulCommClass ℝ A A] [inst_6 : IsScalarTower ℝ A A] [inst_7 : StarOrderedRing A]
  [inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_9 : NonnegSpectrumClass ℝ A] (a : A),
  CFC.sqrt a = cfcₙ (⇑NNReal.sqrt) a
-- Lean.Server.Utils
/-- Replaces the range `r` (using LSP UTF-16 positions) in `text` (using UTF-8 positions)
with `newText`.
 -/
Lean.Server.replaceLspRange : Lean.FileMap → Lean.Lsp.Range → String → Lean.FileMap
-- Mathlib.CategoryTheory.Galois.GaloisObjects
/-- For Galois `A` and a point `a` of the fiber of `A`, the evaluation at `A` as an equivalence.  -/
CategoryTheory.PreGaloisCategory.evaluationEquivOfIsGalois : {C : Type u₁} →
  [inst : CategoryTheory.Category.{u₂, u₁} C] →
    [inst_1 : CategoryTheory.GaloisCategory C] →
      (F : CategoryTheory.Functor C FintypeCat) →
        [CategoryTheory.PreGaloisCategory.FiberFunctor F] →
          (A : C) → [CategoryTheory.PreGaloisCategory.IsGalois A] → (F.obj A).obj → CategoryTheory.Aut A ≃ (F.obj A).obj
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.cos_neg : ∀ (θ : Real.Angle), (-θ).cos = θ.cos
-- Mathlib.Algebra.Polynomial.Taylor
Polynomial.taylor_X_pow : ∀ {R : Type u_1} [inst : Semiring R] (r : R) (n : ℕ),
  (Polynomial.taylor r) (Polynomial.X ^ n) = (Polynomial.X + Polynomial.C r) ^ n
-- Mathlib.Dynamics.Newton
/-- This is really an auxiliary result, en route to
`Polynomial.existsUnique_nilpotent_sub_and_aeval_eq_zero`.  -/
Polynomial.aeval_pow_two_pow_dvd_aeval_iterate_newtonMap : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {P : Polynomial R}
  {x : S},
  IsNilpotent ((Polynomial.aeval x) P) →
    IsUnit ((Polynomial.aeval x) (Polynomial.derivative P)) →
      ∀ (n : ℕ), (Polynomial.aeval x) P ^ 2 ^ n ∣ (Polynomial.aeval (P.newtonMap^[n] x)) P
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt
_private.Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt.0.Lean.Meta.Grind.Arith.Cutsat.throwMissingDecl : Lean.Name → Lean.MetaM Unit
-- Mathlib.Algebra.Homology.SpectralObject.Differentials
CategoryTheory.Abelian.SpectralObject.cyclesMap_Ψ_assoc : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (f₁₂ : i ⟶ k)
  (h₁₂ : CategoryTheory.CategoryStruct.comp f₁ f₂ = f₁₂) (f₂₃ : j ⟶ l),
  CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃ →
    ∀ (n₀ n₁ : ℤ) (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.cyclesMap_Ψ._auto_1) {Z : C}
      (h : X.opcycles f₁ f₂ n₁ ⟶ Z),
      CategoryTheory.CategoryStruct.comp
          (X.cyclesMap f₁₂ f₃ f₂ f₃ (CategoryTheory.ComposableArrows.threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂) n₀)
          (CategoryTheory.CategoryStruct.comp (X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁) h) =
        CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.Analysis.Convex.Basic
Convex.mapsTo_lineMap : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Ring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] {s : Set E} [AddRightMono 𝕜],
  Convex 𝕜 s → ∀ {x y : E}, x ∈ s → y ∈ s → Set.MapsTo (⇑(AffineMap.lineMap x y)) (Set.Icc 0 1) s
-- Mathlib.Topology.Compactness.Compact
/-- A variant of `generalized_tube_lemma` in terms of `nhdsSetWithin`.  -/
generalized_tube_lemma' : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {s s' : Set X},
  IsCompact s →
    ∀ {t t' : Set Y},
      IsCompact t →
        ∀ {n : Set (X × Y)},
          n ∈ nhdsSetWithin (s ×ˢ t) (s' ×ˢ t') → ∃ u ∈ nhdsSetWithin s s', ∃ v ∈ nhdsSetWithin t t', u ×ˢ v ⊆ n
-- Mathlib.Order.Filter.Tendsto
Filter.Tendsto.frequently_map : ∀ {α : Type u_1} {β : Type u_2} {l₁ : Filter α} {l₂ : Filter β} {p : α → Prop} {q : β → Prop} (f : α → β),
  Filter.Tendsto f l₁ l₂ → (∀ (x : α), p x → q (f x)) → (∃ᶠ (x : α) in l₁, p x) → ∃ᶠ (y : β) in l₂, q y
-- Mathlib.Topology.Separation.LinearUpperLowerSetTopology
instCompletelyNormalSpaceOfIsUpperSet : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [Topology.IsUpperSet α], CompletelyNormalSpace α
-- Mathlib.Algebra.Group.Hom.Defs
AddMonoid.End.instAddMonoidHomClass : ∀ (M : Type u_4) [inst : AddZero M], AddMonoidHomClass (AddMonoid.End M) M M
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.Hom.mapMultiforkOfIsLimit_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} A]
  {S : C} {E : CategoryTheory.PreOneHypercover S} {F : CategoryTheory.PreOneHypercover S} (f : E.Hom F)
  (P : CategoryTheory.Functor Cᵒᵖ A) {c : CategoryTheory.Limits.Multifork (E.multicospanIndex P)}
  (hc : CategoryTheory.Limits.IsLimit c) (d : CategoryTheory.Limits.Multifork (F.multicospanIndex P)) (a : E.I₀),
  CategoryTheory.CategoryStruct.comp (f.mapMultiforkOfIsLimit P hc d) (c.ι a) =
    CategoryTheory.CategoryStruct.comp (d.ι (f.s₀ a)) (P.map (f.h₀ a).op)
-- Mathlib.RingTheory.HahnSeries.Multiplication
_private.Mathlib.RingTheory.HahnSeries.Multiplication.0.HahnSeries.mul_assoc' : ∀ {Γ : Type u_1} {R : Type u_3} [inst : AddCommMonoid Γ] [inst_1 : PartialOrder Γ] [inst_2 : IsOrderedCancelAddMonoid Γ]
  [inst_3 : NonUnitalSemiring R] (x y z : HahnSeries Γ R), x * y * z = x * (y * z)
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.commSemiring : {R : Type u} →
  {M : Type v} →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] → [inst_3 : Module Rᵐᵒᵖ M] → [IsCentralScalar R M] → CommSemiring (TrivSqZeroExt R M)
-- Init.SizeOf
Bool.false.sizeOf_spec : sizeOf false = 1
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
/-- A version of `cfc_apply` in terms of `ContinuousMap.mkD`  -/
cfc_apply_mkD : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : TopologicalSpace A] [inst_6 : Ring A]
  [inst_7 : StarRing A] [inst_8 : Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] (f : R → R) (a : A)
  (ha : autoParam (p a) _auto_106✝), cfc f a = (cfcHom ha) (ContinuousMap.mkD ((spectrum R a).domRestrict f) 0)
-- Mathlib.Combinatorics.Matroid.IndepAxioms
IndepMatroid.indep_subset : ∀ {α : Type u_2} (self : IndepMatroid α) ⦃I J : Set α⦄, self.Indep J → I ⊆ J → self.Indep I
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.ker_of_isAffine : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsAffine Y],
  AlgebraicGeometry.Scheme.Hom.ker f =
    AlgebraicGeometry.Scheme.IdealSheafData.ofIdealTop
      (RingHom.ker (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appTop f)))
-- Mathlib.MeasureTheory.Measure.Regular
/-- If the restrictions of a measure to a monotone sequence of sets covering the space are
inner regular for some property `p` and all measurable sets, then the measure itself is
inner regular.  -/
MeasureTheory.Measure.InnerRegularWRT.of_restrict : ∀ {α : Type u_1} [inst : MeasurableSpace α] {p : Set α → Prop} {μ : MeasureTheory.Measure α} {s : ℕ → Set α},
  (∀ (n : ℕ), (μ.restrict (s n)).InnerRegularWRT p MeasurableSet) →
    Set.univ ⊆ ⋃ n, s n → Monotone s → μ.InnerRegularWRT p MeasurableSet
-- Mathlib.Tactic.TermCongr
/-- Implementation of `mkCongrOf`, with caching.  -/
Mathlib.Tactic.TermCongr.mkCongrOfAux : ℕ → ℕ → Lean.Expr → Lean.Expr → Mathlib.Tactic.TermCongr.M Mathlib.Tactic.TermCongr.CongrResult
-- Mathlib.RingTheory.Ideal.GoingUp
Ideal.isMaximal_of_isIntegral_of_isMaximal_comap' : ∀ {R : Type u_1} [inst : CommRing R] {S : Type u_2} [inst_1 : CommRing S] (f : R →+* S),
  f.IsIntegral → ∀ (I : Ideal S) [I.IsPrime], (Ideal.comap f I).IsMaximal → I.IsMaximal
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVBinPred.noConfusionType : Sort v✝ → Std.Tactic.BVDecide.BVBinPred → Std.Tactic.BVDecide.BVBinPred → Sort v✝
-- Mathlib.Analysis.InnerProductSpace.l2Space
/-- *A* Hilbert sum `(E, V)` of `G` is canonically isomorphic to *the* Hilbert sum of `G`,
i.e `lp G 2`.

Note that this goes in the opposite direction from `OrthogonalFamily.linearIsometry`.  -/
IsHilbertSum.linearIsometryEquiv : {ι : Type u_1} →
  {𝕜 : Type u_2} →
    [inst : RCLike 𝕜] →
      {E : Type u_3} →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : InnerProductSpace 𝕜 E] →
            {G : ι → Type u_4} →
              [inst_3 : (i : ι) → NormedAddCommGroup (G i)] →
                [inst_4 : (i : ι) → InnerProductSpace 𝕜 (G i)] →
                  [inst_5 : CompleteSpace E] → {V : (i : ι) → G i →ₗᵢ[𝕜] E} → IsHilbertSum 𝕜 G V → E ≃ₗᵢ[𝕜] ↥(lp G 2)
-- Mathlib.Topology.Order.MonotoneConvergence
Prod.supConvergenceClass : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : TopologicalSpace α]
  [inst_3 : TopologicalSpace β] [SupConvergenceClass α] [SupConvergenceClass β], SupConvergenceClass (α × β)
-- Mathlib.Order.RelClasses
IsWellOrder.toIsWellFounded : ∀ {α : Type u} {r : α → α → Prop} [self : IsWellOrder α r], IsWellFounded α r
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Grp.forget_map : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {X Y : CategoryTheory.Grp C} (f : X ⟶ Y), (CategoryTheory.Grp.forget C).map f = f.hom.hom
-- Std.Http.Data.Headers.Name
Std.Http.Header.Name.Name.beq_eq : ∀ {x y : Std.Http.Header.Name}, (x == y) = (x.value == y.value)
-- Mathlib.Data.Finsupp.Defs
Finsupp.coe_onFinset : ∀ {α : Type u_1} {M : Type u_4} [inst : Zero M] (s : Finset α) (f : α → M) (hf : ∀ (a : α), f a ≠ 0 → a ∈ s),
  ⇑(Finsupp.onFinset s f hf) = f
-- Mathlib.Probability.Process.Predictable
_private.Mathlib.Probability.Process.Predictable.0.MeasureTheory.IsStronglyPredictable.of_measurable_add_one.match_1_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (n : ℕ) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match n.succ with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_2 n
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.ParentMap : Type
-- Mathlib.Combinatorics.Additive.DoublingConst
/-- The doubling constant `σₘ[A, B]` of two finsets `A` and `B` in a group is `|A * B| / |A|`.

The notation `σₘ[A, B]` is available in scope `Combinatorics.Additive`.  -/
Finset.mulConst : {G : Type u_1} → [Group G] → [DecidableEq G] → Finset G → Finset G → ℚ≥0
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits
AlgebraicGeometry.SheafedSpace.isColimit_exists_rep : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : CategoryTheory.Category.{w', w} J]
  [Small.{v, w} J] (F : CategoryTheory.Functor J (AlgebraicGeometry.SheafedSpace C))
  [CategoryTheory.Limits.HasLimitsOfShape Jᵒᵖ C] {c : CategoryTheory.Limits.Cocone F}
  (hc : CategoryTheory.Limits.IsColimit c) (x : ↑↑c.pt.toPresheafedSpace),
  ∃ i y, (CategoryTheory.ConcreteCategory.hom (c.ι.app i).hom.base) y = x
-- Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
LinearMap.injective_iff_surjective_of_finrank_eq_finrank : ∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {V₂ : Type v'}
  [inst_3 : AddCommGroup V₂] [inst_4 : Module K V₂] [FiniteDimensional K V] [FiniteDimensional K V₂],
  Module.finrank K V = Module.finrank K V₂ → ∀ {f : V →ₗ[K] V₂}, Function.Injective ⇑f ↔ Function.Surjective ⇑f
-- Mathlib.Analysis.InnerProductSpace.NormDet
/-- `LinearMap.normDet` vanishes iff the map is not injective.
 -/
LinearMap.normDet_eq_zero_iff_ker_ne_bot : ∀ {𝕜 : Type u_1} {U : Type u_2} {V : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup U]
  [inst_2 : InnerProductSpace 𝕜 U] [inst_3 : FiniteDimensional 𝕜 U] [inst_4 : NormedAddCommGroup V]
  [inst_5 : InnerProductSpace 𝕜 V] {f : U →ₗ[𝕜] V}, f.normDet = 0 ↔ f.ker ≠ ⊥
-- Mathlib.RingTheory.Spectrum.Prime.RingHom
PrimeSpectrum.comap_id : ∀ {R : Type u} [inst : CommSemiring R], PrimeSpectrum.comap (RingHom.id R) = fun x => x
-- Mathlib.LinearAlgebra.LinearPMap
LinearPMap.instAddSemigroup : {R : Type u_1} →
  {S : Type u_2} →
    [inst : Ring R] →
      [inst_1 : Ring S] →
        {σ : R →+* S} →
          {E : Type u_4} →
            [inst_2 : AddCommGroup E] →
              [inst_3 : Module R E] →
                {F : Type u_5} → [inst_4 : AddCommGroup F] → [inst_5 : Module S F] → AddSemigroup (E →ₛₗ.[σ] F)
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.lift_add : ∀ {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} {H : ι → Type u_4} {C : Type u_5}
  {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h}
  [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [inst_2 : (i : ι) → FunLike (H i) (G i) C]
  [inst_3 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_4 : IsDirectedOrder ι] [inst_5 : (i : ι) → Add (G i)]
  [inst_6 : Add C] [inst_7 : ∀ (i j : ι) (h : i ≤ j), AddHomClass (T h) (G i) (G j)]
  [∀ (i : ι), AddHomClass (H i) (G i) C] (g : (i : ι) → H i)
  (h : ∀ (i j : ι) (h : i ≤ j) (x : G i), (g i) x = (g j) ((f i j h) x)) (x y : DirectLimit G f),
  DirectLimit.lift f (fun x => ⇑(g x)) h (x + y) =
    DirectLimit.lift f (fun x => ⇑(g x)) h x + DirectLimit.lift f (fun x => ⇑(g x)) h y
-- Mathlib.Data.Part
Part.instAdd : {α : Type u_1} → [Add α] → Add (Part α)
-- Lean.PrettyPrinter.Parenthesizer
Lean.PrettyPrinter.Parenthesizer.ParenthesizerAliasValue : Type
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.leadingCoeff_sub_of_degree_eq : ∀ {R : Type u} [inst : Ring R] {p q : Polynomial R},
  p.degree = q.degree → p.leadingCoeff ≠ q.leadingCoeff → (p - q).leadingCoeff = p.leadingCoeff - q.leadingCoeff
-- Mathlib.Order.InitialSeg
InitialSeg.map_bot : ∀ {α : Type u_1} {β : Type u_2} [inst : PartialOrder β] [inst_1 : PartialOrder α] [inst_2 : OrderBot α]
  [inst_3 : OrderBot β] (f : α ≤i β), f ⊥ = ⊥