mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.FieldTheory.AbelRuffini
isIntegral_of_mem_solvableByRad : ∀ {F : Type u_1} {E : Type u_2} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {x : E},
  x ∈ solvableByRad F E → IsIntegral F x
-- Mathlib.CategoryTheory.Functor.FullyFaithful
CategoryTheory.Functor.FullyFaithful.homEquiv_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful) {X Y : C} (a : X ⟶ Y), hF.homEquiv a = F.map a
-- Mathlib.NumberTheory.NumberField.Completion.Ramification
NumberField.InfinitePlace.inertiaDeg_eq_finrank : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  (v : NumberField.InfinitePlace K) (w : NumberField.InfinitePlace L) [inst_3 : w.LiesOver v],
  v.inertiaDeg w = Module.finrank v.Completion w.Completion
-- Init.Data.String.Pattern.String
String.Slice.Pattern.ForwardSliceSearcher.getElem_buildTable_le : ∀ (pat : String.Slice) (i : ℕ) (hi : i < pat.utf8ByteSize),
  (String.Slice.Pattern.ForwardSliceSearcher.buildTable pat)[i] ≤ i
-- Mathlib.Algebra.Group.Basic
right_ne_mul : ∀ {M : Type u_4} [inst : Monoid M] [IsRightCancelMul M] {a b : M}, b ≠ a * b ↔ a ≠ 1
-- Mathlib.Algebra.Category.ModuleCat.ExteriorPower
/-- The natural isomorphism `M.exteriorPower 0 ≅ ModuleCat.of R R`.  -/
ModuleCat.exteriorPower.natIso₀ : (R : Type u) →
  [inst : CommRing R] →
    ModuleCat.exteriorPower.functor R 0 ≅ (CategoryTheory.Functor.const (ModuleCat R)).obj (ModuleCat.of R R)
-- Mathlib.Algebra.Order.Archimedean.Class
MulArchimedeanClass.mk_left_le_mk_mul : ∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M] {a b : M},
  MulArchimedeanClass.mk a ≤ MulArchimedeanClass.mk b → MulArchimedeanClass.mk a ≤ MulArchimedeanClass.mk (a * b)
-- Mathlib.GroupTheory.GroupAction.SubMulAction.Closure
SubAddAction.subset_closure : ∀ {R : Type u_1} {M : Type u_2} [inst : VAdd R M] {s : Set M}, s ⊆ ↑(SubAddAction.closure R s)
-- Mathlib.GroupTheory.Coprod.Basic
MulEquiv.coprodPUnit_apply : ∀ (M : Type u_1) [inst : Monoid M], ⇑(MulEquiv.coprodPUnit M) = ⇑Monoid.Coprod.fst
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKey!_of_isEmpty : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited α], (↑m).WF → ∀ {a : α}, (↑m).isEmpty = true → m.getKey! a = default
-- Lean.ResolveName
/-- Given a list of names produced by `resolveGlobalConst`, throws an error if the list does not contain
exactly one element.
Recall that `resolveGlobalConst` does not return empty lists.
 -/
Lean.ensureNonAmbiguous : {m : Type → Type} → [Monad m] → [Lean.MonadError m] → Lean.Syntax → List Lean.Name → m Lean.Name
-- Std.Data.TreeSet.Raw.Basic
/-- Checks if given key is contained and returns the key if it is, otherwise `fallback`.
If they key is contained the result is guaranteed to be pointer equal to the key in the set.
 -/
Std.TreeSet.Raw.getD : {α : Type u} → {cmp : α → α → Ordering} → Std.TreeSet.Raw α cmp → α → α → α
-- Mathlib.Algebra.Homology.SingleHomology
HomologicalComplex.singleObjCyclesSelfIso.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {ι : Type u_1} [inst_3 : DecidableEq ι] (c : ComplexShape ι) (j : ι)
  (A : C),
  HomologicalComplex.singleObjCyclesSelfIso c j A =
    ((HomologicalComplex.single C c j).obj A).iCyclesIso j (c.next j) ⋯ ⋯ ≪≫ HomologicalComplex.singleObjXSelf c j A
-- Mathlib.Data.Multiset.AddSub
Multiset.subset_add_right : ∀ {α : Type u_1} {s t : Multiset α}, s ⊆ t + s
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.mk_embedding_eq_arrow_of_le : ∀ {α β : Type u} [Infinite α], Cardinal.mk β ≤ Cardinal.mk α → Cardinal.mk (β ↪ α) = Cardinal.mk (β → α)
-- Mathlib.Analysis.Calculus.DifferentialForm.Basic
extDeriv_smul : ∀ {𝕜 : 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] {n : ℕ} {x : E} (c : 𝕜)
  (ω : E → E [⋀^Fin n]→L[𝕜] F), extDeriv (c • ω) x = c • extDeriv ω x
-- Mathlib.Algebra.Module.ZLattice.Basic
ZLattice.comap_toAddSubgroup : ∀ (K : Type u_1) [inst : NormedField K] {E : Type u_2} {F : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace K E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace K F] (L : Submodule ℤ E)
  (e : F →ₗ[K] E), (ZLattice.comap K L e).toAddSubgroup = AddSubgroup.comap e.toAddMonoidHom L.toAddSubgroup
-- Std.Tactic.Do.Syntax
Lean.Parser.Tactic.«mcasesPat⟨_⟩» : Lean.ParserDescr
-- Mathlib.CategoryTheory.Enriched.Limits.HasConicalLimits
CategoryTheory.Enriched.HasConicalLimitsOfShape.mk : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {V : outParam (Type u')}
  [inst_1 : CategoryTheory.Category.{v', u'} V] [inst_2 : CategoryTheory.MonoidalCategory V] {C : Type u}
  [inst_3 : CategoryTheory.Category.{v, u} C] [inst_4 : CategoryTheory.EnrichedOrdinaryCategory V C],
  autoParam (∀ (F : CategoryTheory.Functor J C), CategoryTheory.Enriched.HasConicalLimit V F)
      CategoryTheory.Enriched.HasConicalLimitsOfShape.hasConicalLimit._autoParam →
    CategoryTheory.Enriched.HasConicalLimitsOfShape J V C
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.SplitSource.mbtc.injEq : ∀ (a b : Lean.Expr) (i : ℕ) (a_1 b_1 : Lean.Expr) (i_1 : ℕ),
  (Lean.Meta.Grind.SplitSource.mbtc a b i = Lean.Meta.Grind.SplitSource.mbtc a_1 b_1 i_1) =
    (a = a_1 ∧ b = b_1 ∧ i = i_1)
-- Mathlib.NumberTheory.PellMatiyasevic
Pell.eq_pell_lem : ∀ {a : ℕ} (a1 : 1 < a) (n : ℕ) (b : ℤ√↑(Pell.d✝ a1)),
  1 ≤ b → Pell.IsPell b → b ≤ Pell.pellZd a1 n → ∃ n, b = Pell.pellZd a1 n
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey_map : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp}
  [inst : Std.TransCmp cmp] {f : α → β → γ} {k : α} {h' : k ∈ Std.TreeMap.Raw.map f t} (h : t.WF),
  (Std.TreeMap.Raw.map f t).getKey k h' = t.getKey k ⋯
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.prod_rightUnitor_inv_naturality : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} [inst_1 : CategoryTheory.Limits.HasTerminal C]
  [inst_2 : CategoryTheory.Limits.HasBinaryProducts C] (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.rightUnitor X).inv
      (CategoryTheory.Limits.prod.map f (CategoryTheory.CategoryStruct.id (⊤_ C))) =
    CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.prod.rightUnitor Y).inv
-- Mathlib.Algebra.Group.Prod
/-- Division as a monoid homomorphism.  -/
divMonoidHom : {α : Type u_6} → [inst : DivisionCommMonoid α] → α × α →* α
-- Mathlib.Topology.Homotopy.TopCat.Basic
TopCat.Homotopy.h_refl : ∀ {X Y : TopCat} {f₀ : X ⟶ Y},
  TopCat.Homotopy.h (TopCat.Homotopy.refl f₀) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.fst X TopCat.I) f₀
-- Mathlib.LinearAlgebra.TensorProduct.Associator
LinearMap.lTensor_tensor : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Type u_5) {N : Type u_6} {P : Type u_7} {Q : Type u_8}
  [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : AddCommMonoid Q]
  [inst_5 : Module R M] [inst_6 : Module R N] [inst_7 : Module R Q] [inst_8 : Module R P] (f : P →ₗ[R] Q),
  LinearMap.lTensor (TensorProduct R M N) f =
    ↑(TensorProduct.assoc R M N Q).symm ∘ₗ LinearMap.lTensor M (LinearMap.lTensor N f) ∘ₗ ↑(TensorProduct.assoc R M N P)
-- Mathlib.Data.TypeVec
_private.Mathlib.Data.TypeVec.0.TypeVec.prod.diag.match_1.eq_2 : ∀ (motive : (x : ℕ) → (x_1 : TypeVec.{u_1} x) → (x : Fin2 x) → x_1 x → Sort u_2) (n : ℕ) (x : TypeVec.{u_1} n.succ)
  (x_1 : x Fin2.fz) (h_1 : (n : ℕ) → (α : TypeVec.{u_1} n.succ) → (a : Fin2 n) → (x : α a.fs) → motive n.succ α a.fs x)
  (h_2 : (n : ℕ) → (x : TypeVec.{u_1} n.succ) → (x_2 : x Fin2.fz) → motive n.succ x Fin2.fz x_2),
  (match n.succ, x, Fin2.fz, x_1 with
    | n.succ, α, a.fs, x => h_1 n α a x
    | n.succ, x, Fin2.fz, x_2 => h_2 n x x_2) =
    h_2 n x x_1
-- Mathlib.Probability.ConditionalProbability
ProbabilityTheory.cond_apply' : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {s t : Set Ω},
  MeasurableSet t → ∀ (μ : MeasureTheory.Measure Ω), μ[t | s] = (μ s)⁻¹ * μ (s ∩ t)
-- Mathlib.LinearAlgebra.Matrix.Vec
/-- All the matrix entries, arranged into one column.  -/
Matrix.vec : {m : Type u_1} → {n : Type u_2} → {R : Type u_3} → Matrix m n R → n × m → R
-- Mathlib.MeasureTheory.VectorMeasure.Integral
MeasureTheory.VectorMeasure.integral_zero_vectorMeasure : ∀ {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] {f : X → E} {B : E →L[ℝ] F →L[ℝ] G}, ∫ᵛ (x : X), f x ∂[B; 0] = 0
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.keyAtIdxD_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {i : ℕ}
  {fallback : α}, t₁.Equiv t₂ → t₁.keyAtIdxD i fallback = t₂.keyAtIdxD i fallback
-- Mathlib.Geometry.Manifold.Bordism
/-- `M` is a `C^k` manifold.  -/
SingularManifold.isManifold : ∀ {X : Type u_1} [inst : TopologicalSpace X] {k : WithTop ℕ∞} {E : Type u_2} {H : Type u_3}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E] [inst_3 : FiniteDimensional ℝ E]
  [inst_4 : TopologicalSpace H] {I : ModelWithCorners ℝ E H} (self : SingularManifold X k I), IsManifold I k self.M
-- Mathlib.RingTheory.Ideal.HasGoingUp
Algebra.HasGoingUp.mk : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S],
  (∀ {q : Ideal R} [q.IsPrime] (P : Ideal S) [P.IsPrime], Ideal.under R P < q → ∃ Q, P ≤ Q ∧ Q.IsPrime ∧ Q.LiesOver q) →
    Algebra.HasGoingUp R S
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.contains_inter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α}, (t₁ ∩ t₂).contains k = (t₁.contains k && t₂.contains k)
-- Std.Data.TreeMap.Raw.Basic
Std.TreeMap.Raw.instUnion : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Union (Std.TreeMap.Raw α β cmp)
-- Mathlib.Geometry.Manifold.VectorBundle.Hom
mdifferentiableWithinAt_hom_bundle : ∀ {𝕜 : Type u_1} {B : Type u_2} {F₁ : Type u_3} {F₂ : Type u_4} {M : Type u_5} {E₁ : B → Type u_6} {E₂ : B → Type u_7}
  [inst : NontriviallyNormedField 𝕜] [inst_1 : (x : B) → AddCommGroup (E₁ x)] [inst_2 : (x : B) → Module 𝕜 (E₁ x)]
  [inst_3 : NormedAddCommGroup F₁] [inst_4 : NormedSpace 𝕜 F₁] [inst_5 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)]
  [inst_6 : (x : B) → TopologicalSpace (E₁ x)] [inst_7 : (x : B) → AddCommGroup (E₂ x)]
  [inst_8 : (x : B) → Module 𝕜 (E₂ x)] [inst_9 : NormedAddCommGroup F₂] [inst_10 : NormedSpace 𝕜 F₂]
  [inst_11 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)] [inst_12 : (x : B) → TopologicalSpace (E₂ x)] {EB : Type u_8}
  [inst_13 : NormedAddCommGroup EB] [inst_14 : NormedSpace 𝕜 EB] {HB : Type u_9} [inst_15 : TopologicalSpace HB]
  {IB : ModelWithCorners 𝕜 EB HB} [inst_16 : TopologicalSpace B] [inst_17 : ChartedSpace HB B] {EM : Type u_10}
  [inst_18 : NormedAddCommGroup EM] [inst_19 : NormedSpace 𝕜 EM] {HM : Type u_11} [inst_20 : TopologicalSpace HM]
  {IM : ModelWithCorners 𝕜 EM HM} [inst_21 : TopologicalSpace M] [inst_22 : ChartedSpace HM M]
  [inst_23 : FiberBundle F₁ E₁] [inst_24 : VectorBundle 𝕜 F₁ E₁] [inst_25 : FiberBundle F₂ E₂]
  [inst_26 : VectorBundle 𝕜 F₂ E₂] [inst_27 : ∀ (x : B), IsTopologicalAddGroup (E₂ x)]
  [inst_28 : ∀ (x : B), ContinuousSMul 𝕜 (E₂ x)] (f : M → Bundle.TotalSpace (F₁ →L[𝕜] F₂) fun b => E₁ b →L[𝕜] E₂ b)
  {s : Set M} {x₀ : M},
  MDiffAt[s] f x₀ ↔
    (MDiffAt[s] fun x => (f x).proj) x₀ ∧
      (MDiffAt[s] fun x =>
          ContinuousLinearMap.inCoordinates F₁ E₁ F₂ E₂ (f x₀).proj (f x).proj (f x₀).proj (f x).proj (f x).snd)
        x₀
-- Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
SSet.relativeCellComplexOfMono.Cell.ext_iff : ∀ {X Y : SSet} {i : X ⟶ Y} {d : ℕ} {x y : SSet.relativeCellComplexOfMono.Cell i d}, x = y ↔ x.simplex = y.simplex
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.bound : Lean.Expr → Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof
-- Mathlib.Tactic.FunProp.Theorems
Mathlib.Meta.FunProp.instInhabitedLambdaTheoremArgs : Inhabited Mathlib.Meta.FunProp.LambdaTheoremArgs
-- Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Filter.EventuallyEq.isEquivalent : ∀ {α : Type u_1} {β : Type u_2} [inst : NormedAddCommGroup β] {l : Filter α} {u v : α → β},
  u =ᶠ[l] v → Asymptotics.IsEquivalent l u v
-- Mathlib.Algebra.Module.Defs
Convex.combo_eq_smul_sub_add : ∀ {R : Type u_1} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {x y : M} {a b : R},
  a + b = 1 → a • x + b • y = b • (y - x) + x
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
NumberField.mixedEmbedding.convexBodyLT_neg_mem : ∀ (K : Type u_1) [inst : Field K] (f : NumberField.InfinitePlace K → NNReal),
  ∀ x ∈ NumberField.mixedEmbedding.convexBodyLT K f, -x ∈ NumberField.mixedEmbedding.convexBodyLT K f
-- Lean.Data.Lsp.Internal
/-- End character of selection range.  -/
Lean.Lsp.DeclInfo.selectionRangeEndPosCharacter : Lean.Lsp.DeclInfo → ℕ
-- Init.Data.Option.Lemmas
Option.min_eq_right : ∀ {α : Type u_1} [inst : LE α] [inst_1 : Min α],
  (∀ (x y : α), y ≤ x → x ⊓ y = y) → ∀ {a b : Option α}, b ≤ a → a ⊓ b = b
-- Mathlib.Order.UpperLower.CompleteLattice
LowerSet.lower : ∀ {α : Type u_1} [inst : LE α] (s : LowerSet α), IsLowerSet ↑s
-- Mathlib.CategoryTheory.Sites.IsSheafFor
/-- **Alias** of `CategoryTheory.Presieve.shrinkFunctorHomEquiv`.

---

(Implementation). This is a (primarily internal) equivalence between natural transformations
and compatible families.

Cf the discussion after Lemma 7.47.10 in <https://stacks.math.columbia.edu/tag/00YW>. See also
the proof of C2.1.4 of [Elephant], and the discussion in [MM92], Chapter III, Section 4.
 -/
CategoryTheory.Presieve.natTransEquivCompatibleFamily : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X : C} →
      {S : CategoryTheory.Sieve X} →
        [inst_1 : CategoryTheory.LocallySmall.{w, v₁, u₁} C] →
          {F : CategoryTheory.Functor Cᵒᵖ (Type w)} →
            ((CategoryTheory.Sieve.shrinkFunctor.{w, v₁, u₁} S).toFunctor ⟶ F) ≃ { x // x.Compatible }
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.mul_vle_mul_iff_right : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R] {x y z : R}, 0 <ᵥ x → (x * y ≤ᵥ x * z ↔ y ≤ᵥ z)
-- Mathlib.AlgebraicGeometry.Group.Affine
Bialgebra.comulBialgHom.congr_simp : ∀ (R : Type u_1) (A : Type u_2) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Bialgebra R A]
  [inst_3 : Coalgebra.IsCocomm R A], Bialgebra.comulBialgHom R A = Bialgebra.comulBialgHom R A
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
AddMonoidAlgebra.instBialgebra.eq_1 : ∀ (R : Type u_1) (A : Type u_3) (M : Type u_8) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Bialgebra R A]
  [inst_3 : AddMonoid M],
  AddMonoidAlgebra.instBialgebra R A M =
    { toAlgebra := AddMonoidAlgebra.algebra, toCoalgebra := AddMonoidAlgebra.instCoalgebra R A M, counit_one := ⋯,
      mul_compr₂_counit := ⋯, comul_one := ⋯, mul_compr₂_comul := ⋯ }
-- Lean.DocString.Parser
/-- Parses a list item according to the current nesting context.  -/
Lean.Doc.Parser.listItem : Lean.Doc.Parser.BlockCtxt → Lean.Parser.ParserFn
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.integral_eq_zero_iff_of_nonneg_ae : ∀ {f : ℝ → ℝ} {a b : ℝ} {μ : MeasureTheory.Measure ℝ},
  0 ≤ᵐ[μ.restrict (Set.Ioc a b ∪ Set.Ioc b a)] f →
    IntervalIntegrable f μ a b → (∫ (x : ℝ) in a..b, f x ∂μ = 0 ↔ f =ᵐ[μ.restrict (Set.Ioc a b ∪ Set.Ioc b a)] 0)
-- Mathlib.Algebra.Polynomial.Div
Polynomial.degree_divByMonic_le : ∀ {R : Type u} [inst : Ring R] (p q : Polynomial R), (p /ₘ q).degree ≤ p.degree
-- Mathlib.RingTheory.LocalProperties.Submodule
/-- A submodule is trivial if its localization at every maximal ideal is trivial.  -/
Submodule.eq_bot_of_localization₀_maximal : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_5) [inst_3 : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)]
  [inst_4 : (P : Ideal R) → [inst_4 : P.IsMaximal] → Module R (Mₚ P)]
  (f : (P : Ideal R) → [inst_5 : P.IsMaximal] → M →ₗ[R] Mₚ P)
  [inst_5 : ∀ (P : Ideal R) [inst_5 : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)] (N : Submodule R M),
  (∀ (P : Ideal R) [inst_6 : P.IsMaximal], Submodule.localized₀ P.primeCompl (f P) N = ⊥) → N = ⊥
-- Lean.Compiler.IR.Basic
Lean.IR.instInhabitedAlt : Inhabited Lean.IR.Alt
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.refl_symm : ∀ {R₁ : Type u_1} [inst : Semiring R₁] {M₁ : Type u_4} [inst_1 : TopologicalSpace M₁] [inst_2 : AddCommMonoid M₁]
  [inst_3 : Module R₁ M₁], (ContinuousLinearEquiv.refl R₁ M₁).symm = ContinuousLinearEquiv.refl R₁ M₁
-- Mathlib.LinearAlgebra.Semisimple
/-- A linear endomorphism is finitely semisimple if it is semisimple on every finitely-generated
invariant submodule.

See also `Module.End.isFinitelySemisimple_iff`.  -/
Module.End.isFinitelySemisimple_iff' : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {f : Module.End R M},
  f.IsFinitelySemisimple ↔
    ∀ (p : Submodule R M) (hp : p ∈ f.invtSubmodule),
      Module.Finite R ↥p → Module.End.IsSemisimple (LinearMap.restrict f hp)
-- Lean.Meta.Tactic.Simp.Types
/-- Similar to `Simproc`, but resulting expression should be definitionally equal to the input one.
 -/
Lean.Meta.Simp.DSimproc : Type
-- Lean.Elab.App
/-- User-provided named arguments that still have to be processed.  -/
Lean.Elab.Term.ElabElim.State.namedArgs : Lean.Elab.Term.ElabElim.State → List Lean.Elab.Term.NamedArg
-- Mathlib.Analysis.Normed.Group.Basic
eq_one_or_nnnorm_pos : ∀ {E : Type u_5} [inst : NormedGroup E] (a : E), a = 1 ∨ 0 < ‖a‖₊
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.forM_eq_forM : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} {m : Type w → Type w'}
  [inst : Monad m] [LawfulMonad m] {f : α → β → m PUnit.{w + 1}}, Std.TreeMap.Raw.forM f t = forM t fun a => f a.1 a.2
-- Mathlib.Algebra.Group.Subgroup.Defs
Subgroup.subtype_apply : ∀ {G : Type u_1} [inst : Group G] {s : Subgroup G} (x : ↥s), s.subtype x = ↑x
-- Mathlib.Algebra.Category.Ring.Colimits
CommRingCat.Colimits.Prequotient.add : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    {F : CategoryTheory.Functor J CommRingCat} →
      CommRingCat.Colimits.Prequotient F → CommRingCat.Colimits.Prequotient F → CommRingCat.Colimits.Prequotient F
-- Init.Prelude
instHSMul : {α : Type u_1} → {β : Type u_2} → [SMul α β] → HSMul α β β
-- Mathlib.Analysis.Complex.MeanValue
/-- **Alias** of `DiffContOnCl.circleAverage_smul_div`.

---

The **Generalized Mean Value Property** of complex differentiable functions: If `f : ℂ → E` is
complex differentiable at all points of a closed disc of radius `R` and center `c`, then for every
point `w` in the disk, the circle average `circleAverage (fun z ↦ ((z - c) * (z - w)⁻¹) • f z) c R`
equals `f w`.
 -/
circleAverage_sub_sub_inv_smul_of_differentiable_on : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [CompleteSpace E] {f : ℂ → E} {R : ℝ}
  {c w : ℂ},
  DiffContOnCl ℂ f (Metric.ball c |R|) →
    w ∈ Metric.ball c |R| → Real.circleAverage (fun z => ((z - c) / (z - w)) • f z) c R = f w
-- Mathlib.Data.ENat.Basic
ENat.mul_le_mul_left_iff : ∀ {a x y : ℕ∞}, a ≠ 0 → a ≠ ⊤ → (a * x ≤ a * y ↔ x ≤ y)
-- Lean.Data.Name
Lean.Name.quickCmpAux : Lean.Name → Lean.Name → Ordering
-- Mathlib.Topology.Category.TopCat.Opens
/-- The functor from open sets in `X` to `TopCat`,
realising each open set as a topological space itself.
 -/
TopologicalSpace.Opens.toTopCat : (X : TopCat) → CategoryTheory.Functor (TopologicalSpace.Opens ↑X) TopCat
-- Std.Sat.CNF.RelabelFin
Std.Sat.CNF.of_maxLiteral_eq_some : ∀ {maxLit : ℕ} (f : Std.Sat.CNF ℕ), f.maxLiteral = some maxLit → ∀ (lit : ℕ), Std.Sat.CNF.VarMem lit f → lit ≤ maxLit
-- Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
mvfderivWithin_mul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {s : Set M} {f g : M → 𝕜} {x : M},
  MDiffAt[s] f x → MDiffAt[s] g x → UniqueMDiffAt[s] x → d[s] (f * g) x = f x • d[s] g x + g x • d[s] f x
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
AEMeasurable.isLUB : ∀ {α : Type u_1} {δ : Type u_4} [inst : TopologicalSpace α] {mα : MeasurableSpace α} [BorelSpace α]
  {mδ : MeasurableSpace δ} [inst_2 : LinearOrder α] [OrderTopology α] [SecondCountableTopology α] {ι : Sort u_5}
  {μ : MeasureTheory.Measure δ} [Countable ι] {f : ι → δ → α} {g : δ → α},
  (∀ (i : ι), AEMeasurable (f i) μ) → (∀ᵐ (b : δ) ∂μ, IsLUB {a | ∃ i, f i b = a} (g b)) → AEMeasurable g μ
-- Mathlib.Algebra.Homology.SpectralObject.Basic
CategoryTheory.Abelian.SpectralObject.sc₁_g : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{u_3, u_1} C]
  [inst_1 : CategoryTheory.Category.{u_4, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k)
  (h : CategoryTheory.CategoryStruct.comp f g = fg) (n₀ n₁ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.sc₁._auto_1),
  (X.sc₁ f g fg h n₀ n₁ hn₁).g = (X.H n₁).map (CategoryTheory.ComposableArrows.twoδ₂Toδ₁ f g fg h)
-- Mathlib.Algebra.Ring.Hom.Defs
RingHom.mul_def : ∀ {α : Type u_2} {x : NonAssocSemiring α} (f g : α →+* α), f * g = f.comp g
-- Mathlib.MeasureTheory.VectorMeasure.SetIntegral
/-- If `f` is integrable, then `∫ᵛ x in s, f x ∂[B; μ]` is absolutely continuous in `s`:
it tends to zero as `μ.variation s` tends to zero.  -/
MeasureTheory.VectorMeasure.Integrable.tendsto_setIntegral_nhds_zero : ∀ {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedAddCommGroup G] {μ : MeasureTheory.VectorMeasure X F} {f : X → E}
  [inst_3 : NormedSpace ℝ E] [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G}
  {ι : Type u_7},
  μ.Integrable f →
    ∀ {l : Filter ι} {s : ι → Set X},
      Filter.Tendsto (⇑μ.variation ∘ s) l (nhds 0) → Filter.Tendsto (fun i => ∫ᵛ (x : X) in s i, f x ∂[B; μ]) l (nhds 0)
-- Mathlib.Analysis.Complex.CoveringMap
Complex.isAddQuotientCoveringMap_exp : IsAddQuotientCoveringMap (fun z => ⟨Complex.exp z, ⋯⟩) ↥(AddSubgroup.zmultiples (2 * ↑Real.pi * Complex.I))
-- Std.Http.Data.URI.Basic
/-- Gets the first value of a query parameter by key name, decoded as a string.
Returns the default value if the key is not found or if the value cannot be decoded.
 -/
Std.Http.URI.Query.getD : Std.Http.URI.Query → String → String → String
-- Mathlib.Analysis.Calculus.Deriv.Add
deriv.neg' : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F}, deriv (-f) = fun x => -deriv f x
-- Mathlib.Algebra.Order.Ring.WithTop
WithBot.coe_pow : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : MonoidWithZero α] [inst_2 : NoZeroDivisors α] [inst_3 : Nontrivial α]
  (a : α) (n : ℕ), ↑(a ^ n) = ↑a ^ n
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Real
measurable_ereal_toReal : Measurable EReal.toReal
-- Mathlib.Tactic.DefEqAbuse
/-- Collect instance names from successful `apply @Instance to Goal` trace nodes.
Once https://github.com/leanprover/lean4/pull/12699 is available, the `headerStr.contains "apply"`
check can be replaced with ``td.cls == `Meta.synthInstance.apply``.  -/
_private.Mathlib.Tactic.DefEqAbuse.0.Mathlib.Tactic.DefEqAbuse.findSynthSuccessApps : Lean.MessageData → BaseIO (Std.HashSet String)