mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.ContinuousMap.Weierstrass
/-- An alternative statement of Weierstrass' theorem.

Every real-valued continuous function on `[a,b]` is a uniform limit of polynomials.
 -/
continuousMap_mem_polynomialFunctions_closure : ∀ (a b : ℝ) (f : C(↑(Set.Icc a b), ℝ)), f ∈ (polynomialFunctions (Set.Icc a b)).topologicalClosure
-- Mathlib.RingTheory.PrincipalIdealDomain
/-- See also `Irreducible.coprime_iff_not_dvd'`.  -/
Irreducible.dvd_iff_not_isCoprime : ∀ {R : Type u} [inst : CommRing R] [IsBezout R] {p n : R}, Irreducible p → (p ∣ n ↔ ¬IsCoprime p n)
-- Mathlib.Topology.VectorBundle.Riemannian
/-- The inner product along the fibers of the bundle.  -/
Bundle.ContinuousRiemannianMetric.inner : {B : Type u_4} →
  [inst : TopologicalSpace B] →
    {F : Type u_5} →
      [inst_1 : NormedAddCommGroup F] →
        [inst_2 : NormedSpace ℝ F] →
          {E : B → Type u_6} →
            [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)] →
              [inst_4 : (b : B) → TopologicalSpace (E b)] →
                [inst_5 : (b : B) → AddCommGroup (E b)] →
                  [inst_6 : (b : B) → Module ℝ (E b)] →
                    [inst_7 : FiberBundle F E] →
                      [inst_8 : VectorBundle ℝ F E] →
                        Bundle.ContinuousRiemannianMetric F E → (b : B) → E b →L[ℝ] E b →L[ℝ] ℝ
-- Mathlib.Algebra.Ring.BooleanRing
instBooleanRingAsBoolRing : {α : Type u_1} → [BooleanAlgebra α] → BooleanRing (AsBoolRing α)
-- Mathlib.Algebra.Group.Center
Set.decidableMemCentralizer : {M : Type u_1} →
  {S : Set M} →
    [inst : Mul M] → [(a : M) → Decidable (∀ b ∈ S, b * a = a * b)] → DecidablePred fun x => x ∈ S.centralizer
-- Mathlib.CategoryTheory.Adjunction.Lifting.Left
/-- (Implementation)
To construct the left adjoint, we use the coequalizer of `F' U ε_Y` with the composite

`F' U F U X ⟶ F' U F U R F' U X ⟶ F' U R F' U X ⟶ F' U X`

where the first morphism is `F' U F ι_UX`, the second is `F' U ε_RF'UX`, and the third is `δ_F'UX`.
We will show that this coequalizer exists and that it forms the object map for a left adjoint to
`R`.
 -/
CategoryTheory.LiftLeftAdjoint.otherMap : {A : Type u₁} →
  {B : Type u₂} →
    {C : Type u₃} →
      [inst : CategoryTheory.Category.{v₁, u₁} A] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            {U : CategoryTheory.Functor B C} →
              {F : CategoryTheory.Functor C B} →
                (R : CategoryTheory.Functor A B) →
                  (F' : CategoryTheory.Functor C A) →
                    (F ⊣ U) → (F' ⊣ R.comp U) → (X : B) → F'.obj (U.obj (F.obj (U.obj X))) ⟶ F'.obj (U.obj X)
-- Lean.Parser.Extension
Lean.Parser.ParserAttributeHook.mk.injEq : ∀ (postAdd postAdd_1 : Lean.Name → Lean.Name → Bool → Lean.AttrM Unit),
  ({ postAdd := postAdd } = { postAdd := postAdd_1 }) = (postAdd = postAdd_1)
-- Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
CongruenceSubgroup.Gamma_is_cong_sub : ∀ (N : ℕ) [NeZero N], CongruenceSubgroup.IsCongruenceSubgroup (CongruenceSubgroup.Gamma N)
-- Mathlib.Data.Nat.Digits.Defs
Nat.digits_getLast : ∀ {b : ℕ} (m : ℕ),
  1 < b → ∀ (p : b.digits m ≠ []) (q : b.digits (m / b) ≠ []), (b.digits m).getLast p = (b.digits (m / b)).getLast q
-- Init.Data.ToString.Extra
instToStringArray : {α : Type u_1} → [ToString α] → ToString (Array α)
-- Mathlib.Algebra.Order.Ring.StandardPart
ArchimedeanClass.FiniteElement.ext_iff : ∀ {K : Type u_1} [inst : LinearOrder K] [inst_1 : Field K] [inst_2 : IsOrderedRing K]
  {x y : ArchimedeanClass.FiniteElement K}, x = y ↔ ↑x = ↑y
-- Mathlib.Algebra.Group.Submonoid.Defs
AddSubmonoid.instNontrivial : ∀ {M : Type u_1} [inst : AddZeroClass M] [Nontrivial M], Nontrivial (AddSubmonoid M)
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.invRev_append : ∀ {α : Type u} {L₁ L₂ : List (α × Bool)}, FreeGroup.invRev (L₁ ++ L₂) = FreeGroup.invRev L₂ ++ FreeGroup.invRev L₁
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.coeff_update_apply : ∀ {R : Type u_1} [inst : Semiring R] (p : SkewPolynomial R) (n : ℕ) (a : R) (i : ℕ),
  (p.update n a).coeff i = if i = n then a else p.coeff i
-- Init.Core
/-- An associative operation satisfies `(a ∘ b) ∘ c = a ∘ (b ∘ c)`.  -/
Std.Associative.assoc : ∀ {α : Sort u} {op : α → α → α} [self : Std.Associative op] (a b c : α), op (op a b) c = op a (op b c)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.mem_iff : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t₁.WF → t₂.WF → t₁.Equiv t₂ → ∀ {k : α}, k ∈ t₁ ↔ k ∈ t₂
-- Mathlib.Combinatorics.SimpleGraph.Tutte
/-- From a graph on an even number of vertices with no perfect matching, we can remove an odd number
of vertices such that there are more odd components in the resulting graph than vertices we removed.

This is the sufficiency side of Tutte's theorem.  -/
SimpleGraph.exists_isTutteViolator : ∀ {V : Type u_1} {G : SimpleGraph V} [Finite V],
  (∀ (M : G.Subgraph), ¬M.IsPerfectMatching) → Even (Nat.card V) → ∃ u, G.IsTutteViolator u
-- Mathlib.CategoryTheory.Monoidal.Mod
/-- The action map is compatible with multiplication.  -/
CategoryTheory.ModObj.mul_smul_assoc : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C} {D : Type u₂}
  {inst_2 : CategoryTheory.Category.{v₂, u₂} D} {inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D}
  {M : C} {inst_4 : CategoryTheory.MonObj M} (X : D) [self : CategoryTheory.ModObj M X] {Z : D} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft CategoryTheory.MonObj.mul X)
      (CategoryTheory.CategoryStruct.comp CategoryTheory.ModObj.smul h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso M M X).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight M CategoryTheory.ModObj.smul)
        (CategoryTheory.CategoryStruct.comp CategoryTheory.ModObj.smul h))
-- Mathlib.Topology.EMetricSpace.Diam
/-- **Alias** of `Metric.ediam_zero`. -/
EMetric.diam_zero : ∀ {X : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : Zero X], Metric.ediam 0 = 0
-- Mathlib.Order.RelIso.Basic
/-- Transport a `RelEmbedding` across a pair of `RelIso`s, by pre- and post-composition.

This is `Equiv.embeddingCongr` for `RelEmbedding`.  -/
RelIso.relEmbeddingCongr : {α₁ : Type u_5} →
  {β₁ : Type u_6} →
    {α₂ : Type u_7} →
      {β₂ : Type u_8} →
        {r₁ : α₁ → α₁ → Prop} →
          {s₁ : β₁ → β₁ → Prop} →
            {r₂ : α₂ → α₂ → Prop} → {s₂ : β₂ → β₂ → Prop} → r₁ ≃r r₂ → s₁ ≃r s₂ → r₁ ↪r s₁ ≃ (r₂ ↪r s₂)
-- Lean.Declaration
Lean.ReducibilityHints.instOrd : Ord Lean.ReducibilityHints
-- Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
/-- The universal property of closed immersions:
For a closed immersion `f : X ⟶ Z`, given any morphism of schemes `g : Y ⟶ Z` whose kernel
contains the kernel of `X` in `Z`, we can lift this morphism to a unique `Y ⟶ X` that
commutes with these maps.
 -/
AlgebraicGeometry.IsClosedImmersion.lift : {X Y Z : AlgebraicGeometry.Scheme} →
  (f : X ⟶ Z) →
    (g : Y ⟶ Z) →
      [AlgebraicGeometry.IsClosedImmersion f] →
        AlgebraicGeometry.Scheme.Hom.ker f ≤ AlgebraicGeometry.Scheme.Hom.ker g → (Y ⟶ X)
-- Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
GradedTensorProduct.includeLeftRingHom_apply : ∀ {R : Type u_1} {ι : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring ι] [inst_1 : DecidableEq ι]
  [inst_2 : CommRing R] [inst_3 : Ring A] [inst_4 : Ring B] [inst_5 : Algebra R A] [inst_6 : Algebra R B]
  (𝒜 : ι → Submodule R A) (ℬ : ι → Submodule R B) [inst_7 : GradedAlgebra 𝒜] [inst_8 : GradedAlgebra ℬ]
  [inst_9 : Module ι (Additive ℤˣ)] (a : A), (GradedTensorProduct.includeLeftRingHom 𝒜 ℬ) a = a ᵍ⊗ₜ[R] 1
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Under.mk_left : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] {P : CategoryTheory.MorphismProperty T}
  (Q : CategoryTheory.MorphismProperty T) {X A : T} (f : X ⟶ A) (hf : P f),
  (CategoryTheory.MorphismProperty.Under.mk Q f hf).left = { as := PUnit.unit }
-- Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfFunctorialResolutions
CategoryTheory.LocalizerMorphism.isConnected_rightResolution_of_functorial_resolutions : ∀ {C₁ : Type u_1} {C₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂)
  {ρ : CategoryTheory.Functor C₂ C₁} (i : CategoryTheory.Functor.id C₂ ⟶ ρ.comp Φ.functor),
  (∀ (X₂ : C₂), W₂ (i.app X₂)) →
    W₁ = W₂.inverseImage Φ.functor →
      ∀ [Φ.functor.Full] [Φ.functor.Faithful] [W₂.HasTwoOutOfThreeProperty] [W₂.IsMultiplicative] (X₂ : C₂),
        CategoryTheory.IsConnected (Φ.RightResolution X₂)
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
Finsupp.sum_single_index : ∀ {α : Type u_1} {M : Type u_8} {N : Type u_10} [inst : Zero M] [inst_1 : AddCommMonoid N] {a : α} {b : M}
  {h : α → M → N}, h a 0 = 0 → (fun₀ | a => b).sum h = h a b
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.get_get? : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [inst : Std.TransCmp cmp] (h : t.WF) {a : α}
  {h' : (t.get? a).isSome = true}, (t.get? a).get h' = t.get a ⋯
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getD_insertMany_empty_list_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} [Std.TransOrd α] [inst : BEq α] [Std.LawfulBEqOrd α]
  [inst_2 : Std.LawfulEqOrd α] {l : List ((a : α) × β a)} {k : α} {fallback : β k},
  (List.map Sigma.fst l).contains k = false →
    (↑(Std.DTreeMap.Internal.Impl.empty.insertMany l ⋯)).getD k fallback = fallback
-- Aesop.Rule.Basic
Aesop.Rule.extra : {α : Type} → Aesop.Rule α → α
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.Iter.forIn_mapM : ∀ {α β β₂ γ : Type w} {n : Type w → Type w'} {o : Type w → Type w''} {Pred EPred : Type w} [inst : Std.Iterator α Id β]
  [inst_1 : Monad n] [LawfulMonad n] [inst_3 : Monad o] [inst_4 : Std.Internal.Do.Assertion Pred]
  [inst_5 : Std.Internal.Do.Assertion EPred] [inst_6 : Std.Internal.Do.WPMonad o Pred EPred] [inst_7 : MonadAttach n]
  [WeaklyLawfulMonadAttach n] [inst_9 : MonadLiftT n o] [LawfulMonadLiftT n o] [Std.Iterators.Finite α Id]
  [inst_12 : Std.IteratorLoop α Id o] [Std.LawfulIteratorLoop α Id o] {it : Std.Iter β} {f : β → n β₂} {init : γ}
  {g : β₂ → γ → o (ForInStep γ)} {P : Pred} {Q : γ → Pred} {eQ : EPred},
  ⦃ P ⦄
      forIn it init fun out acc => do
        let __do_lift ← liftM (f out)
        g __do_lift acc ⦃
      Q; eQ ⦄ →
    ⦃ P ⦄ forIn (Std.Iter.mapM f it) init g ⦃ Q; eQ ⦄
-- Lean.LibrarySuggestions.Basic
Lean.MVarId.getConstants : Lean.MVarId → Lean.MetaM Lean.NameSet
-- Mathlib.Analysis.Normed.Module.MStructure
/-- A projection on a normed space `X` is said to be an L-projection if, for all `x` in `X`,
$\|x\| = \|P x\| + \|(1 - P) x\|$.

Note that we write `P • x` instead of `P x` for reasons described in the module docstring.
 -/
IsLprojection : (X : Type u_1) → [inst : NormedAddCommGroup X] → {M : Type u_2} → [inst_1 : Ring M] → [Module M X] → M → Prop
-- Mathlib.Algebra.Group.Equiv.Defs
MulEquiv.mk : {M : Type u_9} →
  {N : Type u_10} →
    [inst : Mul M] →
      [inst_1 : Mul N] →
        (toEquiv : M ≃ N) → (∀ (x y : M), toEquiv.toFun (x * y) = toEquiv.toFun x * toEquiv.toFun y) → M ≃* N
-- Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
MeasureTheory.Measure.setIntegral_toReal_rnDeriv : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ]
  [MeasureTheory.SigmaFinite ν],
  μ.AbsolutelyContinuous ν → ∀ (s : Set α), ∫ (x : α) in s, (μ.rnDeriv ν x).toReal ∂ν = μ.real s
-- Lean.Elab.DefView
Lean.Elab.Command.isDefLike : Lean.Syntax → Bool
-- Mathlib.Algebra.Category.Grp.Ulift
/-- The universe lift functor for groups is faithful.
 -/
GrpCat.instFaithfulUliftFunctor : GrpCat.uliftFunctor.Faithful
-- Mathlib.RingTheory.Perfection
Perfection.coeffMonoidHom_zero_liftMonoidHom : ∀ (p : ℕ) {M : Type u_2} {N : Type u_3} [inst : CommMonoid M] [inst_1 : PerfectRing M p] [inst_2 : CommMonoid N]
  (e : M →* N) (x : M), (Perfection.coeffMonoidHom N p 0) (((Perfection.liftMonoidHom p M N) e) x) = e x
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.idealOfLE.congr_simp : ∀ {K : Type u} [inst : Field K] (R S S_1 : ValuationSubring K) (e_S : S = S_1) (h : R ≤ S),
  R.idealOfLE S h = R.idealOfLE S_1 ⋯
-- Mathlib.Data.Fin.Tuple.Curry
Function.OfArity.uncurry_two_eq_uncurry : ∀ {α β : Type u} (f : Function.OfArity α β 2), f.uncurry = Function.uncurry f ∘ ⇑(finTwoArrowEquiv α)
-- Lean.Data.Lsp.Basic
Lean.Lsp.instFromJsonTextDocumentIdentifier.fromJson : Lean.Json → Except String Lean.Lsp.TextDocumentIdentifier
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
/-- If `1 < k`, then `ζ ^ k.pred = -(∑ i ∈ range k.pred, ζ ^ i)`.  -/
IsPrimitiveRoot.pow_sub_one_eq : ∀ {R : Type u_4} {k : ℕ} [inst : CommRing R] [IsDomain R] {ζ : R},
  IsPrimitiveRoot ζ k → 1 < k → ζ ^ k.pred = -∑ i ∈ Finset.range k.pred, ζ ^ i
-- Mathlib.Analysis.Convex.GaugeRescale
/-- If `s` is a convex bounded set with a nonempty interior in a real normed space,
then there is a homeomorphism of the ambient space to itself
that sends the interior of `s` to the unit open ball
and the closure of `s` to the unit closed ball.  -/
exists_homeomorph_image_interior_closure_frontier_eq_unitBall : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {s : Set E},
  Convex ℝ s →
    (interior s).Nonempty →
      Bornology.IsBounded s →
        ∃ h,
          ⇑h '' interior s = Metric.ball 0 1 ∧
            ⇑h '' closure s = Metric.closedBall 0 1 ∧ ⇑h '' frontier s = Metric.sphere 0 1
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.isBigOWith_inv : ∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {c : ℝ} {f : α → E} {g : α → F}
  {l : Filter α}, 0 < c → (Asymptotics.IsBigOWith c⁻¹ l f g ↔ ∀ᶠ (x : α) in l, c * ‖f x‖ ≤ ‖g x‖)
-- Mathlib.GroupTheory.Congruence.Defs
Con.commMonoid.eq_1 : ∀ {M : Type u_4} [inst : CommMonoid M] (c : Con M), c.commMonoid = { toMonoid := c.monoid, mul_comm := ⋯ }
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.getD_diff : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  {k : α} {fallback : β},
  Std.DTreeMap.Const.getD (t₁ \ t₂) k fallback = if k ∈ t₂ then fallback else Std.DTreeMap.Const.getD t₁ k fallback
-- Mathlib.Order.Hom.Basic
OrderIso.injective : ∀ {α : Type u_2} {β : Type u_3} [inst : LE α] [inst_1 : LE β] (e : α ≃o β), Function.Injective ⇑e
-- Mathlib.CategoryTheory.Sites.LocalSite
CategoryTheory.GrothendieckTopology.IsLocalSite.toHasLimitsOfShape : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} (J : CategoryTheory.GrothendieckTopology C)
  [self : J.IsLocalSite], CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) C
-- Mathlib.Geometry.Manifold.HasGroupoid
hasGroupoid_of_le : ∀ {H : Type u} {M : Type u_2} [inst : TopologicalSpace H] [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M]
  {G₁ G₂ : StructureGroupoid H}, HasGroupoid M G₁ → G₁ ≤ G₂ → HasGroupoid M G₂
-- Init.Data.SInt.Bitwise
Int32.neg_one_shiftLeft_and_shiftLeft : ∀ {a b : Int32}, (-1) <<< b &&& a <<< b = a <<< b
-- Mathlib.Algebra.Tropical.Basic
Tropical.tropOrderIso_symm_coe_fn : ∀ {R : Type u} [inst : Preorder R], ⇑Tropical.tropOrderIso.symm = Tropical.untrop
-- Mathlib.Order.Hom.BoundedLattice
/-- An `InfTopHomClass` morphism preserves the top element.  -/
InfTopHomClass.map_top : ∀ {F : Type u_6} {α : Type u_7} {β : Type u_8} {inst : Min α} {inst_1 : Min β} {inst_2 : Top α} {inst_3 : Top β}
  {inst_4 : FunLike F α β} [self : InfTopHomClass F α β] (f : F), f ⊤ = ⊤
-- Init.Data.Array.Bootstrap
Array.toListAppend_eq : ∀ {α : Type u_1} {xs : Array α} {l : List α}, xs.toListAppend l = xs.toList ++ l
-- Mathlib.RingTheory.Teichmuller
/-- `teichmullerAux` as an adic Cauchy sequence.  -/
Perfection.teichmullerCauchy : {p : ℕ} →
  [Fact (Nat.Prime p)] →
    {R : Type u_1} →
      [inst : CommRing R] →
        {I : Ideal R} → [CharP (R ⧸ I) p] → Perfection (R ⧸ I) p → AdicCompletion.AdicCauchySequence I R
-- Mathlib.Algebra.Module.LocalizedModule.Submodule
/-- The canonical map to the kernel of the localization of `g` is localizing.
In other words, localization commutes with kernels.  -/
LinearMap.toKerLocalized_isLocalizedModule : ∀ {R : Type u_1} (S : Type u_2) {M : Type u_3} {N : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid N] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : Algebra R S] [inst_7 : Module S N] [IsScalarTower R S N] (p : Submonoid R) [IsLocalization p S]
  (f : M →ₗ[R] N) [inst_10 : IsLocalizedModule p f] {P : Type u_5} [inst_11 : AddCommMonoid P] [inst_12 : Module R P]
  {Q : Type u_6} [inst_13 : AddCommMonoid Q] [inst_14 : Module R Q] [inst_15 : Module S Q] [IsScalarTower R S Q]
  (f' : P →ₗ[R] Q) [inst_17 : IsLocalizedModule p f'] (g : M →ₗ[R] P),
  IsLocalizedModule p (LinearMap.toKerIsLocalized p f f' g)
-- Std.Data.DTreeMap.Lemmas
/-- Simpler variant of `get!_filterMap` when `LawfulEqCmp` is available.  -/
Std.DTreeMap.Const.get!_filterMap' : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {γ : Type w} {t : Std.DTreeMap α (fun x => β) cmp}
  [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [inst : Inhabited γ] {f : α → β → Option γ} {k : α},
  Std.DTreeMap.Const.get! (Std.DTreeMap.filterMap f t) k = ((Std.DTreeMap.Const.get? t k).bind (f k)).get!
-- Mathlib.Algebra.Group.UniqueProds.Basic
UniqueAdd.to_addOpposite : ∀ {G : Type u_1} [inst : Add G] {A B : Finset G} {a0 b0 : G},
  UniqueAdd A B a0 b0 →
    UniqueAdd (Finset.map { toFun := AddOpposite.op, inj' := ⋯ } B)
      (Finset.map { toFun := AddOpposite.op, inj' := ⋯ } A) (AddOpposite.op b0) (AddOpposite.op a0)
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
/-- If `E1` and `E2` are intermediate fields, and at least one them are algebraic, then the rank of
the compositum of `E1` and `E2` is less than or equal to the product of that of `E1` and `E2`.
Note that this result is also true without algebraic assumption,
but the proof becomes very complicated.  -/
IntermediateField.rank_sup_le_of_isAlgebraic : ∀ {K : Type u_3} {L : Type u_4} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  (E1 E2 : IntermediateField K L),
  Algebra.IsAlgebraic K ↥E1 ∨ Algebra.IsAlgebraic K ↥E2 →
    Module.rank K ↥(E1 ⊔ E2) ≤ Module.rank K ↥E1 * Module.rank K ↥E2
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.star_coe : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} (x : R) [inst : CommRing R], star ↑x = ↑x
-- Mathlib.RingTheory.Coalgebra.Hom
Coalgebra.subsingleton_to_ring : ∀ {R : Type u} (A : Type v) [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
  [inst_3 : Coalgebra R A], Subsingleton (A →ₗc[R] R)
-- Mathlib.AlgebraicGeometry.Noetherian
/-- A scheme is locally Noetherian if and only if it is covered by affine opens whose sections
are Noetherian rings.

See [Har77], Proposition II.3.2.  -/
AlgebraicGeometry.isLocallyNoetherian_iff_of_iSup_eq_top : ∀ {X : AlgebraicGeometry.Scheme} {ι : Sort u_1} {S : ι → ↑X.affineOpens},
  ⨆ i, ↑(S i) = ⊤ →
    (AlgebraicGeometry.IsLocallyNoetherian X ↔ ∀ (i : ι), IsNoetherianRing ↑(X.presheaf.obj (Opposite.op ↑(S i))))
-- Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
OrderedFinpartition.extendMiddle_partSize : ∀ {n : ℕ} (c : OrderedFinpartition n) (k : Fin c.length),
  (c.extendMiddle k).partSize = Function.update c.partSize k (c.partSize k + 1)
-- Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
curveIntegral_refl : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] (ω : E → E →L[𝕜] F) (a : E),
  ∫ᶜ (x : E) in Path.refl a, ω x = 0
-- Mathlib.CategoryTheory.Limits.HasLimits
/-- The limits of `F : J ⥤ C` and `G : K ⥤ C` are isomorphic,
if there is an equivalence `e : J ≌ K` making the triangle commute up to natural isomorphism.
 -/
CategoryTheory.Limits.HasLimit.isoOfEquivalence : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {K : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} K] →
        {C : Type u} →
          [inst_2 : CategoryTheory.Category.{v, u} C] →
            {F : CategoryTheory.Functor J C} →
              [inst_3 : CategoryTheory.Limits.HasLimit F] →
                {G : CategoryTheory.Functor K C} →
                  [inst_4 : CategoryTheory.Limits.HasLimit G] →
                    (e : J ≌ K) →
                      (e.functor.comp G ≅ F) → (CategoryTheory.Limits.limit F ≅ CategoryTheory.Limits.limit G)
-- Mathlib.Tactic.Variable
_private.Mathlib.Tactic.Variable.0.Mathlib.Command.Variable.elabVariables.process : Lean.Syntax →
  Bool →
    Lean.TSyntaxArray `Lean.Parser.Term.bracketedBinder →
      Option (Lean.TSyntaxArray `Lean.Parser.Term.bracketedBinder) → Lean.Elab.Command.CommandElabM Unit
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.Measure.prod.instIsMulRightInvariant : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Mul G] {μ : MeasureTheory.Measure G} [MeasurableMul G]
  [μ.IsMulRightInvariant] [MeasureTheory.SFinite μ] {H : Type u_3} [inst_5 : Mul H] {mH : MeasurableSpace H}
  {ν : MeasureTheory.Measure H} [MeasurableMul H] [ν.IsMulRightInvariant] [MeasureTheory.SFinite ν],
  (μ.prod ν).IsMulRightInvariant
-- Mathlib.RingTheory.RamificationInertia.Ramification
Ideal.ramificationIdx_def : ∀ {S : Type u_1} [inst : CommRing S] (q : Ideal S) (R : Type u_2) [inst_1 : CommRing R] [inst_2 : Algebra R S]
  [inst_3 : q.IsPrime],
  q.ramificationIdx R =
    (Module.length (Localization.AtPrime q)
        (Localization.AtPrime q ⧸ Ideal.map (algebraMap R (Localization.AtPrime q)) (Ideal.under R q))).toNat
-- Mathlib.Algebra.Ring.BooleanRing
BooleanRing.sup_inf_self : ∀ {α : Type u_1} [inst : BooleanRing α] (a b : α), a ⊔ a ⊓ b = a
-- Mathlib.Algebra.Group.Submonoid.Membership
Submonoid.mul_mem_sup : ∀ {M : Type u_1} [inst : MulOneClass M] {S T : Submonoid M} {x y : M}, x ∈ S → y ∈ T → x * y ∈ S ⊔ T
-- Mathlib.Order.Interval.Set.LinearOrder
/-- **Alias** of `Set.Ioi_sdiff_Ioc`. -/
Set.Ioi_diff_Ioc : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, Set.Ioi a \ Set.Ioc a b = Set.Ioi (max a b)
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Submonoid.LocalizationMap.mk'_spec' : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N]
  (f : S.LocalizationMap N) (x : M) (y : ↥S), f ↑y * f.mk' x y = f x
-- Mathlib.Algebra.BigOperators.Group.List.Defs
List.prod_induction_nonempty : ∀ {M : Type u_2} [inst : MulOneClass M] {l : List M} (p : M → Prop),
  (∀ (a b : M), p a → p b → p (a * b)) → l ≠ [] → (∀ x ∈ l, p x) → p l.prod
-- Mathlib.Algebra.Homology.Embedding.Basic
ComplexShape.Embedding.mk : {ι : Type u_1} →
  {ι' : Type u_2} →
    {c : ComplexShape ι} →
      {c' : ComplexShape ι'} →
        (f : ι → ι') → Function.Injective f → (∀ {i₁ i₂ : ι}, c.Rel i₁ i₂ → c'.Rel (f i₁) (f i₂)) → c.Embedding c'
-- Lean.Parser.Term
Lean.Parser.Term.attrKind.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
/-- `closure` forms a Galois insertion with the coercion to set.  -/
NonUnitalSubsemiring.gi : (R : Type u) → [inst : NonUnitalNonAssocSemiring R] → GaloisInsertion NonUnitalSubsemiring.closure SetLike.coe