mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Convex.EGauge
/-- The extended gauge of a point `(a, b)` with respect to the product of balanced sets `U` and `V`
is equal to the maximum of the extended gauges of `a` with respect to `U`
and `b` with respect to `V`.
 -/
egauge_prod_mk : ∀ {𝕜 : Type u_1} [inst : NormedDivisionRing 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  {F : Type u_3} [inst_3 : AddCommGroup F] [inst_4 : Module 𝕜 F] {U : Set E} {V : Set F},
  Balanced 𝕜 U → Balanced 𝕜 V → ∀ (a : E) (b : F), egauge 𝕜 (U ×ˢ V) (a, b) = max (egauge 𝕜 U a) (egauge 𝕜 V b)
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey_alter_self : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  [Inhabited α] {k : α} {f : Option β → Option β} {h : k ∈ m.alter k f}, (m.alter k f).getKey k h = k
-- Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
ContMDiffSection.coe_nsmul : ∀ {𝕜 : 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] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → TopologicalSpace (V x)] [inst_10 : FiberBundle F V] [inst_11 : (x : M) → AddCommGroup (V x)]
  [inst_12 : (x : M) → Module 𝕜 (V x)] [inst_13 : VectorBundle 𝕜 F V] (s : ContMDiffSection I F n V) (k : ℕ),
  ⇑(k • s) = k • ⇑s
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Ideal.eq_prime_pow_of_succ_lt_of_le : ∀ {A : Type u_2} [inst : CommRing A] [IsDedekindDomain A] {P I : Ideal A} [P_prime : P.IsPrime],
  P ≠ ⊥ → ∀ {i : ℕ}, P ^ (i + 1) < I → I ≤ P ^ i → I = P ^ i
-- Mathlib.Algebra.Category.Ring.Basic
CommSemiRingCat.hom_inv_apply : ∀ {R S : CommSemiRingCat} (e : R ≅ S) (s : ↑S),
  (CategoryTheory.ConcreteCategory.hom e.hom) ((CategoryTheory.ConcreteCategory.hom e.inv) s) = s
-- Mathlib.Data.PNat.Xgcd
/-- `flip` flips the placement of variables during the algorithm.  -/
PNat.XgcdType.flip : PNat.XgcdType → PNat.XgcdType
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.NumDenSameDeg.deg : {ι : Type u_1} →
  {A : Type u_2} →
    {σ : Type u_3} →
      [inst : CommRing A] →
        [inst_1 : SetLike σ A] → {𝒜 : ι → σ} → {x : Submonoid A} → HomogeneousLocalization.NumDenSameDeg 𝒜 x → ι
-- Mathlib.Algebra.Group.Submonoid.Operations
MonoidHom.domRestrict_mrange : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] (S : Submonoid M) (f : M →* N),
  MonoidHom.mrange (f.domRestrict S) = Submonoid.map f S
-- Std.Data.HashMap.Lemmas
Std.HashMap.getD_inter_of_not_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α} {fallback : β}, k ∉ m₂ → (m₁ ∩ m₂).getD k fallback = fallback
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKeyD_insert : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h : t.WF)
  {k a fallback : α} {v : β k},
  (Std.DTreeMap.Internal.Impl.insert k v t ⋯).impl.getKeyD a fallback =
    if compare k a = Ordering.eq then k else t.getKeyD a fallback
-- Std.Internal.Do.Order.Heyting
/-- Unit for `⇨`, the meet specialization of `PreservesSup.le_upperAdjoint`: `a ⊓ x ⊑ b → x ⊑ a ⇨ b`.  -/
Lean.Order.le_himp : ∀ {α : Type u} [inst : Lean.Order.CompleteLattice α] {a b x : α},
  Lean.Order.PartialOrder.rel (Lean.Order.meet a x) b → Lean.Order.PartialOrder.rel x (Lean.Order.himp a b)
-- Init.Data.Int.DivMod.Lemmas
Int.tmod_lt_of_pos : ∀ (a : ℤ) {b : ℤ}, 0 < b → a.tmod b < b
-- Init.Data.Iterators.Consumers.Monadic.Loop
Std.IteratorLoop.WithWF.mk.sizeOf_spec : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} [inst : Std.Iterator α m β] {γ : Type x}
  {PlausibleForInStep : β → γ → ForInStep γ → Prop} {hwf : Std.IteratorLoop.WellFounded α m PlausibleForInStep}
  [inst_1 : SizeOf α] [inst_2 : (a : Type w) → SizeOf (m a)] [inst_3 : SizeOf β] [inst_4 : SizeOf γ]
  [inst_5 : (a : β) → (a_1 : γ) → (a_2 : ForInStep γ) → SizeOf (PlausibleForInStep a a_1 a_2)] (it : Std.IterM m β)
  (acc : γ), sizeOf { it := it, acc := acc } = 1 + sizeOf it + sizeOf acc
-- Init.Data.List.Sort.Lemmas
_private.Init.Data.List.Sort.Lemmas.0.List.zipIdxLE.eq_1 : ∀ {α : Type u_1} (le : α → α → Bool) (a b : α × ℕ),
  List.zipIdxLE le a b = if le a.1 b.1 = true then if le b.1 a.1 = true then decide (a.2 ≤ b.2) else true else false
-- Mathlib.Data.EReal.Basic
EReal.coe_orderEmbedding : ⇑EReal.orderEmbedding = Real.toEReal
-- Lean.Meta.SizeOf
Lean.Meta.genSizeOfSpec : Lean.Option Bool
-- Std.Http.Data.URI.Basic
Std.Http.URI.Authority.mk.inj : ∀ {userInfo : Option Std.Http.URI.UserInfo} {host : Std.Http.URI.Host} {port : Std.Http.URI.Port}
  {userInfo_1 : Option Std.Http.URI.UserInfo} {host_1 : Std.Http.URI.Host} {port_1 : Std.Http.URI.Port},
  { userInfo := userInfo, host := host, port := port } = { userInfo := userInfo_1, host := host_1, port := port_1 } →
    userInfo = userInfo_1 ∧ host = host_1 ∧ port = port_1
-- Lean.Elab.InfoTree.Types
/-- Context for the name of the declaration that surrounds nodes contained within this `context` node.
For example, this makes the name of the surrounding declaration available in `InfoTree` nodes
corresponding to the terms within the declaration.
 -/
Lean.Elab.PartialContextInfo.parentDeclCtx : Lean.Name → Lean.Elab.PartialContextInfo
-- Mathlib.Topology.UniformSpace.Equicontinuity
Set.EquicontinuousOn.mono : ∀ {X : Type u_3} {α : Type u_6} [tX : TopologicalSpace X] [uα : UniformSpace α] {H H' : Set (X → α)} {S : Set X},
  H.EquicontinuousOn S → H' ⊆ H → H'.EquicontinuousOn S
-- Mathlib.Order.Interval.Finset.Basic
Finset.Ioo_eq_empty_of_le : ∀ {α : Type u_2} {a b : α} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α], b ≤ a → Finset.Ioo a b = ∅
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.coe_algebraMap : ∀ {R' : Type u'} {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  (S : Subalgebra R A) [inst_3 : CommSemiring R'] [inst_4 : SMul R' R] [inst_5 : Algebra R' A]
  [inst_6 : IsScalarTower R' R A] (r : R'), ↑((algebraMap R' ↥S) r) = (algebraMap R' A) r
-- Mathlib.Lean.Meta.CongrTheorems
Lean.Meta.FastIsEmpty.inst : ∀ {α : Sort u} [self : Lean.Meta.FastIsEmpty α], IsEmpty α
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.selfLeftAction_actionHomLeft : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C] {c c' : C}
  (f : c ⟶ c') (x : C),
  CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft f x =
    CategoryTheory.MonoidalCategoryStruct.whiskerRight f x
-- Mathlib.CategoryTheory.Limits.Constructions.Over.Products
CategoryTheory.Over.ConstructProducts.conesEquivUnitIso_inv_app_hom : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (B : C)
  (F : CategoryTheory.Functor (CategoryTheory.Discrete J) (CategoryTheory.Over B))
  (X : CategoryTheory.Limits.Cone (CategoryTheory.Over.ConstructProducts.widePullbackDiagramOfDiagramOver B F)),
  ((CategoryTheory.Over.ConstructProducts.conesEquivUnitIso B F).inv.app X).hom = CategoryTheory.CategoryStruct.id X.pt
-- Mathlib.GroupTheory.CosetCover
Submodule.exists_finiteIndex_of_cover : ∀ {R : Type u_1} {M : Type u_2} {ι : Type u_3} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {p : ι → Submodule R M} {s : Finset ι}, ⋃ i ∈ s, ↑(p i) = Set.univ → ∃ k ∈ s, (p k).toAddSubgroup.FiniteIndex
-- Mathlib.Algebra.Category.CoalgCat.Monoidal
CoalgCat.tensorUnit_isAddCommGroup : ∀ (R : Type u) [inst : CommRing R],
  (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CoalgCat R)).isAddCommGroup = inst.toAddCommGroup
-- Mathlib.Logic.Basic
ite_ite_comm : ∀ {α : Sort u_1} (P Q : Prop) [inst : Decidable P] (a b : α) {c : α} [inst_1 : Decidable Q],
  (P → ¬Q) → (if P then a else if Q then b else c) = if Q then b else if P then a else c
-- Mathlib.Analysis.Convex.Side
AffineSubspace.SOppSide.exists_sbtw : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Field R] [inst_1 : LinearOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P]
  {s : AffineSubspace R P} {x y : P}, s.SOppSide x y → ∃ p ∈ s, Sbtw R x p y
-- Mathlib.Order.Bounds.Image
AntitoneOn.mem_upperBounds_image : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {s t : Set α} {a : α},
  AntitoneOn f t → s ⊆ t → a ∈ lowerBounds s → a ∈ t → f a ∈ upperBounds (f '' s)
-- Mathlib.Data.Set.Finite.Basic
Set.Finite.coe_toFinset : ∀ {α : Type u} {s : Set α} (hs : s.Finite), ↑hs.toFinset = s
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
/-- In the case that `n = ∞` we don't need the continuity assumption in
`HasFTaylorSeriesUpToOn`.  -/
hasFTaylorSeriesUpToOn_top_iff' : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f : E → F} {N : WithTop ℕ∞} {p : E → FormalMultilinearSeries 𝕜 E F},
  ↑⊤ ≤ N →
    (HasFTaylorSeriesUpToOn N f p s ↔
      (∀ x ∈ s, (p x 0).curry0 = f x) ∧
        ∀ (m : ℕ), ∀ x ∈ s, HasFDerivWithinAt (fun y => p y m) (p x m.succ).curryLeft s x)
-- Mathlib.Algebra.Order.GroupWithZero.Basic
zpow_lt_one_iff_right_of_lt_one₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀} [ZeroLEOneClass G₀]
  {n : ℤ}, 0 < a → a < 1 → (a ^ n < 1 ↔ 0 < n)
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.adicAbv_coe_lt_one_iff : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] {K : Type u_2} [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) {b : NNReal}
  (hb : 1 < b) (r : R), (v.adicAbv hb) ((algebraMap R K) r) < 1 ↔ r ∈ v.asIdeal
-- Mathlib.Algebra.Order.GroupWithZero.Basic
posMulMono_iff_posMulStrictMono : ∀ {α : Type u_1} [inst : MonoidWithZero α] [inst_1 : PartialOrder α] [IsLeftCancelMulZero α],
  PosMulMono α ↔ PosMulStrictMono α
-- Mathlib.Analysis.Complex.Basic
/-- The only continuous ring homomorphism from `ℝ` to `ℂ` is the identity.  -/
Complex.ringHom_eq_ofReal_of_continuous : ∀ {f : ℝ →+* ℂ}, Continuous ⇑f → f = Complex.ofRealHom
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
CategoryTheory.Bicategory.Adjunction.homEquiv₁_symm_apply : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {b c d : B} {l : b ⟶ c} {r : c ⟶ b}
  (adj : CategoryTheory.Bicategory.Adjunction l r) {g : b ⟶ d} {h : c ⟶ d}
  (β : CategoryTheory.CategoryStruct.comp r g ⟶ h),
  adj.homEquiv₁.symm β =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor g).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight adj.unit g)
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator l r g).hom
          (CategoryTheory.Bicategory.whiskerLeft l β)))
-- Mathlib.Topology.UniformSpace.Defs
nhdsWithin_eq_comap_uniformity_of_mem : ∀ {α : Type ua} [inst : UniformSpace α] {x : α} {T : Set α},
  x ∈ T → ∀ (S : Set α), nhdsWithin x S = Filter.comap (Prod.mk x) (uniformity α ⊓ Filter.principal (T ×ˢ S))
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.veblen_lt_veblen_veblen_iff : ∀ {o₁ o₂ a : Ordinal.{u}},
  o₂ ≤ o₁ → (Ordinal.veblen o₂ a < Ordinal.veblen o₁ (Ordinal.veblen o₂ a) ↔ a < Ordinal.veblen o₁ a)
-- Mathlib.Algebra.Ring.Subring.Basic
/-- The centralizer of a set inside a ring as a `Subring`.  -/
Subring.centralizer : {R : Type u_1} → [inst : Ring R] → Set R → Subring R
-- Mathlib.MeasureTheory.Measure.Real
/-- **Alias** of `MeasureTheory.measureReal_sdiff`. -/
MeasureTheory.measureReal_diff : ∀ {α : Type u_1} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s₁ s₂ : Set α},
  s₂ ⊆ s₁ →
    MeasurableSet s₂ →
      autoParam (μ s₁ ≠ ⊤) MeasureTheory.measureReal_sdiff._auto_1 → μ.real (s₁ \ s₂) = μ.real s₁ - μ.real s₂
-- Mathlib.RingTheory.Spectrum.Prime.Topology
/-- `basicOpen r` is the open subset containing all prime ideals not containing `r`.  -/
PrimeSpectrum.basicOpen : {R : Type u} → [inst : CommSemiring R] → R → TopologicalSpace.Opens (PrimeSpectrum R)
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.toRingHom_refl : ∀ {R : Type u_4} [inst : NonAssocSemiring R], (RingEquiv.refl R).toRingHom = RingHom.id R
-- Mathlib.Algebra.Group.Pi.Lemmas
AddHom.coeFn_apply : ∀ (α : Type u_5) (β : Type u_6) [inst : Add α] [inst_1 : AddCommSemigroup β] (g : α →ₙ+ β) (a : α),
  (AddHom.coeFn α β) g a = g a
-- Mathlib.GroupTheory.Index
AddSubgroup.relIndex_le_of_le_left : ∀ {G : Type u_1} [inst : AddGroup G] {H K L : AddSubgroup G}, H ≤ K → H.relIndex L ≠ 0 → K.relIndex L ≤ H.relIndex L
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
Real.log.eq_1 : ∀ (x : ℝ), Real.log x = if hx : x = 0 then 0 else Real.expOrderIso.symm ⟨|x|, ⋯⟩
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.role.fakeOpen : Lean.Syntax
-- Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
/-- The main estimate in the proof of the Riesz-Markov-Kakutani: `Λ f` is bounded above by the
integral of `f` with respect to the `rieszMeasure` associated to `Λ`.  -/
_private.Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real.0.RealRMK.integral_riesz_aux : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : T2Space X] [inst_2 : MeasurableSpace X] [inst_3 : BorelSpace X]
  (Λ : CompactlySupportedContinuousMap X ℝ →ₚ[ℝ] ℝ) [inst_4 : LocallyCompactSpace X]
  (f : CompactlySupportedContinuousMap X ℝ), Λ f ≤ ∫ (x : X), f x ∂ RealRMK.rieszMeasure Λ
-- Mathlib.Data.List.Infix
List.IsPrefix.nodup : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <+: l₂ → l₂.Nodup → l₁.Nodup
-- Mathlib.GroupTheory.FiniteIndexNormalSubgroup
FiniteIndexNormalSubgroup.instCoeSubgroup.eq_1 : ∀ {G : Type u_1} [inst : Group G], FiniteIndexNormalSubgroup.instCoeSubgroup = { coe := fun H => H.toSubgroup }
-- Mathlib.Order.Concept
/-- **Alias** of `Concept.intent_min`. -/
Concept.intent_inf : ∀ {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (c d : Concept α β r),
  (c ⊓ d).intent = upperPolar r (c.extent ∩ d.extent)
-- Mathlib.Geometry.Manifold.ContMDiff.Atlas
isLocalStructomorphOn_contDiffGroupoid_iff_aux : ∀ {𝕜 : 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] {n : WithTop ℕ∞} {M' : Type u_5}
  [inst_6 : TopologicalSpace M'] [IsManifold I n M] [inst_8 : ChartedSpace H M'] [IsM' : IsManifold I n M']
  {f : OpenPartialHomeomorph M M'},
  ChartedSpace.LiftPropOn (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f) f.source →
    ContMDiffOn I I n (↑f) f.source
-- Mathlib.AlgebraicGeometry.Properties
AlgebraicGeometry.isField_of_isIntegral_of_subsingleton : ∀ (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsIntegral X] [Subsingleton ↥X],
  IsField ↑(X.presheaf.obj (Opposite.op ⊤))
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Submodule
PresheafOfModules.Submodule.homOfLE.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  {M : PresheafOfModules R} {N₁ N₂ : M.Submodule} (hle : N₁ ≤ N₂),
  PresheafOfModules.Submodule.homOfLE hle = PresheafOfModules.Submodule.homOfLE hle
-- Std.Data.DHashMap.Internal.Raw
_private.Std.Data.DHashMap.Internal.Raw.0.Std.DHashMap.Raw.alter.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] [inst_2 : Hashable α] (m : Std.DHashMap.Raw α β)
  (a : α) (f : Option (β a) → Option (β a)),
  m.alter a f = if h : 0 < m.buckets.size then ↑(Std.DHashMap.Internal.Raw₀.alter ⟨m, h⟩ a f) else ∅
-- Mathlib.MeasureTheory.Function.Holder
ContinuousLinearMap.lpPairing.eq_1 : ∀ {α : Type u_1} {𝕜 : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {m : MeasurableSpace α}
  (μ : MeasureTheory.Measure α) (p q : ENNReal) [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : NormedSpace 𝕜 G] [inst_7 : Fact (1 ≤ p)] [inst_8 : Fact (1 ≤ q)] [inst_9 : p.HolderConjugate q]
  [inst_10 : NormedSpace ℝ G] [inst_11 : SMulCommClass ℝ 𝕜 G] [inst_12 : CompleteSpace G] (B : E →L[𝕜] F →L[𝕜] G),
  ContinuousLinearMap.lpPairing μ p q B =
    ContinuousLinearMap.postcomp (↥(MeasureTheory.Lp F q μ)) (MeasureTheory.L1.integralCLM' 𝕜) ∘SL
      ContinuousLinearMap.holderL μ p q 1 B
-- Batteries.Data.Array.Scan
Array.scanl.hcongr_7 : ∀ (β β' : Type u_1),
  β = β' →
    ∀ (α α' : Type u_2),
      α = α' →
        ∀ (f : β → α → β) (f' : β' → α' → β'),
          f ≍ f' →
            ∀ (init : β) (init' : β'),
              init ≍ init' →
                ∀ (as : Array α) (as' : Array α'),
                  as ≍ as' →
                    ∀ (start start' : ℕ),
                      start = start' →
                        ∀ (stop stop' : ℕ),
                          stop = stop' → Array.scanl f init as start stop ≍ Array.scanl f' init' as' start' stop'
-- Lean.Meta.Sym.SymM
/-- Similar to `reportIssue!`, but only reports issue if `sym.debug` is set to `true`.  -/
Lean.Meta.Sym.doElemReportDbgIssue!__ : Lean.ParserDescr
-- Mathlib.Order.Atoms
covBy_iff_coatom_Iic : ∀ {α : Type u_2} [inst : PartialOrder α] {a b : α} (h : a ≤ b), a ⋖ b ↔ IsCoatom ⟨a, h⟩
-- Mathlib.Analysis.SpecificLimits.Normed
tsum_geometric_of_abs_lt_one : ∀ {r : ℝ}, |r| < 1 → ∑' (n : ℕ), r ^ n = (1 - r)⁻¹
-- Mathlib.AlgebraicGeometry.ZariskisMainTheorem
AlgebraicGeometry.instIsOpenImmersionCompSchemeιQuasiFiniteLocusToNormalization : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.LocallyOfFiniteType f]
  [inst_1 : AlgebraicGeometry.IsSeparated f] [inst_2 : AlgebraicGeometry.QuasiCompact f],
  AlgebraicGeometry.IsOpenImmersion
    (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.quasiFiniteLocus f).ι
      (AlgebraicGeometry.Scheme.Hom.toNormalization f))
-- Mathlib.CategoryTheory.Monoidal.Ring
/-- The forgetful functor from the category of commutative ring objects
to the category of ring objects.  -/
CategoryTheory.CommRingObjCat.forget₂RingObjCat : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] →
        CategoryTheory.Functor (CategoryTheory.CommRingObjCat C) (CategoryTheory.RingObjCat C)
-- Mathlib.Analysis.BoxIntegral.Partition.Tagged
BoxIntegral.Prepartition.tag_biUnionTagged : ∀ {ι : Type u_1} {I J : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I)
  {πi : (J : BoxIntegral.Box ι) → BoxIntegral.TaggedPrepartition J},
  J ∈ π → ∀ {J' : BoxIntegral.Box ι}, J' ∈ πi J → (π.biUnionTagged πi).tag J' = (πi J).tag J'
-- Mathlib.Algebra.DirectSum.Ring
DirectSum.toSemiring_coe_addMonoidHom : ∀ {ι : Type u_1} [inst : DecidableEq ι] {A : ι → Type u_2} {R : Type u_3} [inst_1 : (i : ι) → AddCommMonoid (A i)]
  [inst_2 : AddMonoid ι] [inst_3 : DirectSum.GSemiring A] [inst_4 : Semiring R] (f : (i : ι) → A i →+ R)
  (hone : (f 0) GradedMonoid.GOne.one = 1)
  (hmul : ∀ {i j : ι} (ai : A i) (aj : A j), (f (i + j)) (GradedMonoid.GMul.mul ai aj) = (f i) ai * (f j) aj),
  ↑(DirectSum.toSemiring f hone hmul) = DirectSum.toAddMonoid f
-- Mathlib.Topology.MetricSpace.Algebra
LipschitzMul.lipschitz_mul : ∀ {β : Type u_2} {inst : PseudoMetricSpace β} {inst_1 : Monoid β} [self : LipschitzMul β],
  ∃ C, LipschitzWith C fun p => p.1 * p.2
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Matrix.toLinearMap₂'_single : ∀ {R : Type u_1} {N₂ : Type u_10} {n : Type u_11} {m : Type u_12} [inst : CommSemiring R] [inst_1 : AddCommMonoid N₂]
  [inst_2 : Module R N₂] [inst_3 : Fintype n] [inst_4 : Fintype m] [inst_5 : DecidableEq n] [inst_6 : DecidableEq m]
  (M : Matrix n m N₂) (i : n) (j : m), (((Matrix.toLinearMap₂' R) M) (Pi.single i 1)) (Pi.single j 1) = M i j
-- Std.Sat.CNF.Basic
Std.Sat.CNF.instAppend : {α : Type u_1} → Append (Std.Sat.CNF α)
-- Mathlib.Tactic.Translate.Core
/-- `TranslateData` is a structure that holds all data required for a translation attribute.  -/
Mathlib.Tactic.Translate.TranslateData : Type
-- Mathlib.Algebra.Group.Hom.Defs
AddMonoidHom.instAddMonoidHomClass : ∀ {M : Type u_4} {N : Type u_5} [inst : AddZero M] [inst_1 : AddZero N], AddMonoidHomClass (M →+ N) M N
-- Mathlib.RingTheory.OrderOfVanishing.Noetherian
Ring.ordFrac_eq_inverse_comp_valuation : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsDiscreteValuationRing R] {K : Type u_2}
  [inst_3 : Field K] [inst_4 : Algebra R K] [inst_5 : IsFractionRing R K],
  Ring.ordFrac R =
    MonoidWithZero.inverse.comp
      (IsDedekindDomain.HeightOneSpectrum.valuation K (IsDiscreteValuationRing.maximalIdeal R)).toMonoidWithZeroHom
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.instInhabitedEqCnstr : Inhabited Lean.Meta.Grind.Arith.CommRing.EqCnstr
-- Mathlib.Topology.UniformSpace.Cauchy
/-- The closure of a totally bounded set is totally bounded.  -/
TotallyBounded.closure : ∀ {α : Type u} [uniformSpace : UniformSpace α] {s : Set α}, TotallyBounded s → TotallyBounded (closure s)
-- Mathlib.Analysis.Calculus.DiffContOnCl
DiffContOnCl.add : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedSpace 𝕜 F] {f g : E → F} {s : Set E},
  DiffContOnCl 𝕜 f s → DiffContOnCl 𝕜 g s → DiffContOnCl 𝕜 (f + g) s
-- Mathlib.CategoryTheory.Bicategory.Grothendieck
CategoryTheory.Pseudofunctor.CoGrothendieck.forget_map : ∀ {𝒮 : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮]
  (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat) {X Y : F.CoGrothendieck}
  (f : X ⟶ Y), (CategoryTheory.Pseudofunctor.CoGrothendieck.forget F).map f = f.base
-- Mathlib.Computability.TuringMachine.Config
/-- `head` gets the head of the input list: `head [] = [0]`, `head (n :: v) = [n]`.  -/
Turing.ToPartrec.Code.head : Turing.ToPartrec.Code
-- Mathlib.CategoryTheory.Idempotents.Karoubi
CategoryTheory.Idempotents.Karoubi.comp_p : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P Q : CategoryTheory.Idempotents.Karoubi C}
  (f : P.Hom Q), CategoryTheory.CategoryStruct.comp f.f Q.p = f.f
-- Mathlib.Data.Finset.Update
Function.updateFinset_congr : ∀ {ι : Type u_1} {π : ι → Sort u_2} {x : (i : ι) → π i} [inst : DecidableEq ι] {s t : Finset ι} {y : (i : ↥s) → π ↑i}
  {z : (i : ↥t) → π ↑i} (h : s = t), Function.updateFinset x s y = Function.updateFinset x t fun i => y ⟨↑i, ⋯⟩
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKeyD_of_isEmpty : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {a fallback : α}, m.isEmpty = true → m.getKeyD a fallback = fallback
-- Mathlib.Data.Rel
SetRel.dom_inv : ∀ {α : Type u_1} {β : Type u_2} {R : SetRel α β}, R.inv.dom = R.cod
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
/-- `CommSemiring` instance for `type`  -/
Lean.Meta.Grind.Arith.CommRing.CommRing.commSemiringInst : Lean.Meta.Grind.Arith.CommRing.CommRing → Lean.Expr
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get!_diff_of_not_mem_left : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : Inhabited β] {k : α}, k ∉ t₁ → Std.DTreeMap.Const.get! (t₁ \ t₂) k = default
-- Mathlib.CategoryTheory.Limits.Elements
CategoryTheory.Functor.Elements.hasInitial_iff_isRepresentable : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor Cᵒᵖ (Type w)),
  CategoryTheory.Limits.HasInitial F.Elements ↔ F.IsRepresentable
-- Mathlib.SetTheory.Cardinal.NatCard
Set.ecard_strictMono : ∀ {α : Type u_1} [Finite α], StrictMono (ENat.card ∘ Set.Elem)