mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
/-- Composing `fiberwiseColim F H` with the evaluation functor `(evaluation C H).obj c` is
naturally isomorphic to precomposing the Grothendieck inclusion `Grothendieck.ι` to `colim`.  -/
CategoryTheory.Limits.fiberwiseColimCompEvaluationIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {F : CategoryTheory.Functor C CategoryTheory.Cat} →
      {H : Type u₂} →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} H] →
          [inst_2 : ∀ (c : C), CategoryTheory.Limits.HasColimitsOfShape (↑(F.obj c)) H] →
            (c : C) →
              (CategoryTheory.Limits.fiberwiseColim F H).comp ((CategoryTheory.evaluation C H).obj c) ≅
                ((CategoryTheory.Functor.whiskeringLeft (↑(F.obj c)) (CategoryTheory.Grothendieck F) H).obj
                      (CategoryTheory.Grothendieck.ι F c)).comp
                  CategoryTheory.Limits.colim
-- Lean.Elab.Tactic.Simp
_private.Lean.Elab.Tactic.Simp.0.Lean.Elab.Tactic.elabSimpTheorem : Lean.Meta.ConfigWithKey →
  Lean.Meta.Origin → Lean.Syntax → Bool → Bool → Lean.Elab.TermElabM Lean.Elab.Tactic.ElabSimpArgResult
-- Mathlib.Algebra.Order.AddGroupWithTop
LinearOrderedAddCommGroupWithTop.sub_lt_sub_iff_left_of_ne_top : ∀ {α : Type u_2} [inst : LinearOrderedAddCommGroupWithTop α] {a b c : α}, a ≠ ⊤ → (b - a < c - a ↔ b < c)
-- Mathlib.FieldTheory.Galois.IsGaloisGroup
IsGaloisGroup.fixedPoints_eq_bot : ∀ (G : Type u_1) (K : Type u_3) (L : Type u_4) [inst : Group G] [inst_1 : Field K] [inst_2 : Field L]
  [inst_3 : Algebra K L] [inst_4 : MulSemiringAction G L] [inst_5 : IsGaloisGroup G K L],
  FixedPoints.intermediateField G = ⊥
-- Mathlib.Analysis.Analytic.Binomial
Complex.one_add_cpow_hasFPowerSeriesOnBall_zero : ∀ {a : ℂ}, HasFPowerSeriesOnBall (fun x => (1 + x) ^ a) (binomialSeries ℂ a) 0 1
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.coe_map : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_4} [inst_2 : FunLike F M N]
  [mc : MonoidHomClass F M N] (f : F) (S : Submonoid M), ↑(Submonoid.map f S) = ⇑f '' ↑S
-- Init.Data.Bool
Bool.eq_true_or_eq_false_self : ∀ (b : Bool), b = true ∨ b = false ↔ True
-- Mathlib.Topology.Algebra.InfiniteSum.Group
Finset.hasSum_iff_compl : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommGroup α] [inst_1 : TopologicalSpace α] [IsTopologicalAddGroup α]
  {f : β → α} {a : α} (s : Finset β), HasSum f a ↔ HasSum (fun x => f ↑x) (a - ∑ i ∈ s, f i)
-- Mathlib.Topology.Algebra.AsymptoticCone
Convex.asymptoticCone : ∀ {k : Type u_1} {V : Type u_2} [inst : Field k] [inst_1 : LinearOrder k] [IsStrictOrderedRing k]
  [inst_3 : TopologicalSpace k] [OrderTopology k] [inst_5 : AddCommGroup V] [inst_6 : Module k V]
  [inst_7 : TopologicalSpace V] [IsTopologicalAddGroup V] [ContinuousSMul k V] {s : Set V},
  Convex k s → Convex k (asymptoticCone k s)
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
NonUnitalSubsemiring.centerCongr_symm_apply_coe : ∀ {R : Type u} {S : Type v} [inst : NonUnitalNonAssocSemiring R] [inst_1 : NonUnitalNonAssocSemiring S] (e : R ≃+* S)
  (s : ↥(Subsemigroup.center S)), ↑((NonUnitalSubsemiring.centerCongr e).symm s) = e.symm ↑s
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- **Alias** of `Left.one_lt_mul`.

---

Assumes left covariance.
The lemma assuming right covariance is `Right.one_lt_mul`.  -/
one_lt_mul' : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Preorder α] [MulLeftStrictMono α] {a b : α}, 1 < a → 1 < b → 1 < a * b
-- Mathlib.Analysis.BoxIntegral.UnitPartition
BoxIntegral.unitPartition.admissibleIndex.congr_simp : ∀ {ι : Type u_1} (n n_1 : ℕ) (e_n : n = n_1) [inst : NeZero n] [inst_1 : Fintype ι] (B B_1 : BoxIntegral.Box ι),
  B = B_1 → BoxIntegral.unitPartition.admissibleIndex n B = BoxIntegral.unitPartition.admissibleIndex n_1 B_1
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute
Commute.cfcHom : ∀ {𝕜 : Type u_1} {A : Type u_2} {p : A → Prop} [inst : RCLike 𝕜] [inst_1 : Ring A] [inst_2 : StarRing A]
  [inst_3 : Algebra 𝕜 A] [inst_4 : TopologicalSpace A] [inst_5 : ContinuousFunctionalCalculus 𝕜 A p]
  [IsSemitopologicalRing A] [T2Space A] {a b : A} (ha : p a),
  Commute a b → Commute (star a) b → ∀ (f : C(↑(spectrum 𝕜 a), 𝕜)), Commute ((cfcHom ha) f) b
-- Init.Grind.Module.NatModuleNorm
_private.Init.Grind.Module.NatModuleNorm.0.Lean.Grind.Linarith.Poly.denote.match_1.eq_2 : ∀ (motive : Lean.Grind.Linarith.Poly → Sort u_1) (k : ℤ) (v : Lean.Grind.Linarith.Var) (p : Lean.Grind.Linarith.Poly)
  (h_1 : Unit → motive Lean.Grind.Linarith.Poly.nil)
  (h_2 :
    (k : ℤ) →
      (v : Lean.Grind.Linarith.Var) → (p : Lean.Grind.Linarith.Poly) → motive (Lean.Grind.Linarith.Poly.add k v p)),
  (match Lean.Grind.Linarith.Poly.add k v p with
    | Lean.Grind.Linarith.Poly.nil => h_1 ()
    | Lean.Grind.Linarith.Poly.add k v p => h_2 k v p) =
    h_2 k v p
-- Mathlib.Algebra.Category.ModuleCat.Products
/-- The concrete coproduct cone is colimiting.  -/
ModuleCat.coproductCoconeIsColimit : {R : Type u} →
  [inst : Ring R] →
    {ι : Type v} →
      (Z : ι → ModuleCat R) → [inst_1 : DecidableEq ι] → CategoryTheory.Limits.IsColimit (ModuleCat.coproductCocone Z)
-- Init.Grind.Config
Lean.Grind.ConfigInteractive.toConfig : Lean.Grind.ConfigInteractive → Lean.Grind.Config
-- Mathlib.Order.Monotone.Monovary
antivary_const_left : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] (g : ι → β) (a : α),
  Antivary (Function.const ι a) g
-- Std.Time.Time.Unit.Hour
Std.Time.Hour.instDecidableLeOrdinal : {x y : Std.Time.Hour.Ordinal} → Decidable (x ≤ y)
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.coe_top : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E], ↑⊤ = Set.univ
-- Mathlib.Analysis.Normed.Ring.Basic
Real.iSup_prod_eq_prod_iSup_of_nonneg : ∀ {α : Type u_5} [inst : Fintype α] {ι : α → Type u} [∀ (a : α), Finite (ι a)] {f : (a : α) → ι a → ℝ},
  (∀ (a : α) (i : ι a), 0 ≤ f a i) → ⨆ i, ∏ a, f a (i a) = ∏ a, ⨆ i, f a i
-- Mathlib.Algebra.Field.Subfield.Defs
Subfield.pow_mem : ∀ {K : Type u} [inst : DivisionRing K] (s : Subfield K) {x : K}, x ∈ s → ∀ (n : ℕ), x ^ n ∈ s
-- Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
cbiInf_eq_of_forall_not : ∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompletePartialOrderInf α] {p : ι → Prop} {f : (i : ι) → p i → α},
  (∀ (i : ι), ¬p i) → ⨅ i, ⨅ (h : p i), f i h = sInf ∅
-- Lean.Meta.Tactic.SolveByElim
Lean.Meta.SolveByElim.ApplyRulesConfig.mk.injEq : ∀ (toBacktrackConfig : Lean.Meta.Tactic.Backtrack.BacktrackConfig) (toApplyConfig : Lean.Meta.ApplyConfig)
  (transparency : Lean.Meta.TransparencyMode) (symm exfalso : Bool)
  (toBacktrackConfig_1 : Lean.Meta.Tactic.Backtrack.BacktrackConfig) (toApplyConfig_1 : Lean.Meta.ApplyConfig)
  (transparency_1 : Lean.Meta.TransparencyMode) (symm_1 exfalso_1 : Bool),
  ({ toBacktrackConfig := toBacktrackConfig, toApplyConfig := toApplyConfig, transparency := transparency, symm := symm,
        exfalso := exfalso } =
      { toBacktrackConfig := toBacktrackConfig_1, toApplyConfig := toApplyConfig_1, transparency := transparency_1,
        symm := symm_1, exfalso := exfalso_1 }) =
    (toBacktrackConfig = toBacktrackConfig_1 ∧
      toApplyConfig = toApplyConfig_1 ∧ transparency = transparency_1 ∧ symm = symm_1 ∧ exfalso = exfalso_1)
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.iIndepFun.indepFun_finsetSum_of_notMem₀ : ∀ {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {β : Type u_10}
  {m : MeasurableSpace β} [inst : AddCommMonoid β] [MeasurableAdd₂ β] {f : ι → Ω → β},
  ProbabilityTheory.iIndepFun f μ →
    (∀ (i : ι), AEMeasurable (f i) μ) →
      ∀ {s : Finset ι} {i : ι}, i ∉ s → ProbabilityTheory.IndepFun (∑ j ∈ s, f j) (f i) μ
-- Lean.Attributes
Lean.attributeMapRef : IO.Ref (Std.HashMap Lean.Name Lean.AttributeImpl)
-- Mathlib.CategoryTheory.Comma.Arrow
CategoryTheory.Arrow.mono_left : ∀ {T : Type u} [inst : CategoryTheory.Category.{v, u} T] {f g : CategoryTheory.Arrow T} (sq : f ⟶ g)
  [CategoryTheory.Mono sq], CategoryTheory.Mono (CategoryTheory.Arrow.Hom.left sq)
-- Mathlib.NumberTheory.ArithmeticFunction.Defs
ArithmeticFunction.zero_apply : ∀ {R : Type u_1} [inst : Zero R] {x : ℕ}, 0 x = 0
-- Batteries.Recycling.RBTree.Basic
/-- `O(n)`. Constructs the list of values of the map.  -/
RBTree.RBMap.valuesList : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → RBTree.RBMap α β cmp → List β
-- Mathlib.RepresentationTheory.Continuous.Basic
/-- Continuous linear maps between modules. We only put the type classes that are necessary for the
definition, although in applications `M` and `M₂` will be topological modules over the topological
ring `R`.  -/
ContRepresentation.Equiv.cont : ∀ {R : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Monoid G] [inst_1 : Ring R]
  [inst_2 : AddCommGroup V] [inst_3 : TopologicalSpace V] [inst_4 : IsTopologicalAddGroup V] [inst_5 : Module R V]
  [inst_6 : AddCommGroup W] [inst_7 : TopologicalSpace W] [inst_8 : IsTopologicalAddGroup W] [inst_9 : Module R W]
  {π₁ : ContRepresentation R G V} {π₂ : ContRepresentation R G W} (self : π₁.Equiv π₂),
  Continuous (↑↑self.toContinuousLinearEquiv).toFun
-- Mathlib.Algebra.Notation.Support
Pi.mulSupport_mulSingle_disjoint : ∀ {ι : Type u_1} {M : Type u_3} [inst : DecidableEq ι] [inst_1 : One M] {i j : ι} {a b : M},
  a ≠ 1 → b ≠ 1 → (Disjoint (Function.mulSupport (Pi.mulSingle i a)) (Function.mulSupport (Pi.mulSingle j b)) ↔ i ≠ j)
-- Mathlib.Data.Num.Prime
_private.Mathlib.Data.Num.Prime.0.PosNum.minFac.match_1.eq_2 : ∀ (motive : PosNum → Sort u_1) (a : PosNum) (h_1 : Unit → motive PosNum.one) (h_2 : (a : PosNum) → motive a.bit0)
  (h_3 : (n : PosNum) → motive n.bit1),
  (match a.bit0 with
    | PosNum.one => h_1 ()
    | a.bit0 => h_2 a
    | n.bit1 => h_3 n) =
    h_2 a
-- Mathlib.RingTheory.Coprime.Basic
instSymmIsCoprime : ∀ {R : Type u} [inst : CommSemiring R], Std.Symm IsCoprime
-- Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat
QuadraticModuleCat.toModuleCat : {R : Type u} → [inst : CommRing R] → QuadraticModuleCat R → ModuleCat R
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.induction_on' : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {motive : Monoid.Coprod M N → Prop}
  (m : Monoid.Coprod M N),
  motive 1 →
    (∀ (m : M) (x : Monoid.Coprod M N), motive x → motive (Monoid.Coprod.inl m * x)) →
      (∀ (n : N) (x : Monoid.Coprod M N), motive x → motive (Monoid.Coprod.inr n * x)) → motive m
-- Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
CategoryTheory.kernelCokernelCompSequence.ι_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X Y Z : C} (f : X ⟶ Y)
  (g : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.kernelCokernelCompSequence.ι f g)
      CategoryTheory.Limits.biprod.snd =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι (CategoryTheory.CategoryStruct.comp f g)) f
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- If the second of three points is strictly between the other two, the oriented angle at the
first point is zero.  -/
Sbtw.oangle₂₁₃_eq_zero : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p₁ p₂ p₃ : P}, Sbtw ℝ p₁ p₂ p₃ → EuclideanGeometry.oangle p₂ p₁ p₃ = 0
-- Mathlib.Order.RelIso.Basic
RelIso.symm_trans_apply : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop} (f : r ≃r s)
  (g : s ≃r t) (a : γ), (f.trans g).symm a = f.symm (g.symm a)
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.Comon.forget_faithful : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C],
  (CategoryTheory.Comon.forget C).Faithful
-- Mathlib.Analysis.Analytic.Constructions
/-- `(f x)⁻¹` is analytic away from `f x = 0`  -/
AnalyticOn.inv : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {𝕝 : Type u_8} [inst_3 : NormedDivisionRing 𝕝] [inst_4 : NormedAlgebra 𝕜 𝕝] {f : E → 𝕝}
  {s : Set E}, AnalyticOn 𝕜 f s → (∀ x ∈ s, f x ≠ 0) → AnalyticOn 𝕜 f⁻¹ s
-- Init.Data.String.Basic
List.asString_inj : ∀ {l₁ l₂ : List Char}, String.ofList l₁ = String.ofList l₂ ↔ l₁ = l₂
-- Mathlib.Topology.Semicontinuity.Defs
/-- **Alias** of the reverse direction of `lowerSemicontinuousOn_iff_frequently`. -/
LowerSemicontinuousOn.of_frequently : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : LinearOrder β] {f : α → β} {s : Set α},
  (∀ x ∈ s, ∀ (y : β), (∃ᶠ (x' : α) in nhdsWithin x s, f x' ≤ y) → f x ≤ y) → LowerSemicontinuousOn f s
-- Mathlib.Algebra.Homology.ComplexShape
ComplexShape.instDecidableRelRelUp : (α : Type u_1) →
  [inst : AddRightCancelSemigroup α] → [DecidableEq α] → [inst_2 : One α] → DecidableRel (ComplexShape.up α).Rel
-- Init.Grind.Ring.CommSemiringAdapter
_private.Init.Grind.Ring.CommSemiringAdapter.0.Lean.Grind.CommRing.Poly.denoteS.match_1.eq_1 : ∀ (motive : Lean.Grind.CommRing.Poly → Sort u_1) (k : ℤ) (h_1 : (k : ℤ) → motive (Lean.Grind.CommRing.Poly.num k))
  (h_2 :
    (k : ℤ) →
      (m : Lean.Grind.CommRing.Mon) → (p : Lean.Grind.CommRing.Poly) → motive (Lean.Grind.CommRing.Poly.add k m p)),
  (match Lean.Grind.CommRing.Poly.num k with
    | Lean.Grind.CommRing.Poly.num k => h_1 k
    | Lean.Grind.CommRing.Poly.add k m p => h_2 k m p) =
    h_1 k
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.instCommGroupContinuousMap.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : CommGroup β]
  [inst_3 : IsTopologicalGroup β],
  ContinuousMap.instCommGroupContinuousMap = { toGroup := ContinuousMap.instGroupOfIsTopologicalGroup, mul_comm := ⋯ }
-- Mathlib.Order.Notation
/-- The bot (`⊥`, `\bot`) element 

Conventions for notations in identifiers:

 * The recommended spelling of `⊥` in identifiers is `bot`. -/
Bot.bot : {α : Type u_1} → [self : Bot α] → α
-- Init.Data.SInt.Lemmas
ISize.sub_mul : ∀ {a b c : ISize}, (a - b) * c = a * c - b * c
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
ContinuousLinearMapWOT.postcompCLM_apply : ∀ {𝕜₁ : Type u_5} {𝕜₂ : Type u_6} {𝕜₃ : Type u_7} {E : Type u_9} {F : Type u_10} {G : Type u_11} [inst : NormedField 𝕜₁]
  [inst_1 : NormedField 𝕜₂] [inst_2 : NormedField 𝕜₃] {σ₁₂ : 𝕜₁ →+* 𝕜₂} {σ₁₃ : 𝕜₁ →+* 𝕜₃} {σ₂₃ : 𝕜₂ →+* 𝕜₃}
  [inst_3 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [inst_4 : AddCommGroup E] [inst_5 : TopologicalSpace E]
  [inst_6 : Module 𝕜₁ E] [inst_7 : AddCommGroup F] [inst_8 : TopologicalSpace F] [inst_9 : Module 𝕜₂ F]
  [inst_10 : AddCommGroup G] [inst_11 : TopologicalSpace G] [inst_12 : Module 𝕜₃ G] [inst_13 : IsTopologicalAddGroup F]
  [inst_14 : ContinuousConstSMul 𝕜₂ F] [inst_15 : IsTopologicalAddGroup G] [inst_16 : ContinuousConstSMul 𝕜₃ G]
  [inst_17 : RingHomSurjective σ₂₃] [inst_18 : RingHomIsometric σ₂₃] (g : F →SWOT[σ₂₃] G) (f : E →SWOT[σ₁₂] F),
  g.postcompCLM f = g.comp f
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.instZero : {X : Type u_1} → {Y : Type u_2} → [inst : TopologicalSpace X] → [Zero Y] → Zero (LocallyConstant X Y)
-- Mathlib.Algebra.Group.Subsemigroup.Defs
AddSubsemigroup.instSetLike : {M : Type u_1} → [inst : Add M] → SetLike (AddSubsemigroup M) M
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCast_of_mem : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {l : List ((a : α) × β a)} {x : (a : α) × β a}
  (h : x ∈ l), Std.Internal.List.DistinctKeys l → Std.Internal.List.getValueCast x.fst l ⋯ = x.snd
-- Mathlib.Data.Finset.NoncommProd
Finset.noncommProd.eq_1 : ∀ {α : Type u_3} {β : Type u_4} [inst : Monoid β] (s : Finset α) (f : α → β)
  (comm : (↑s).Pairwise (Function.onFun Commute f)), s.noncommProd f comm = (Multiset.map f s.val).noncommProd ⋯
-- Mathlib.Combinatorics.Hall.Finite
/-- Here we combine the two inductive steps into a full strong induction proof,
completing the proof the harder direction of **Hall's Marriage Theorem**.
 -/
HallMarriageTheorem.hall_hard_inductive : ∀ {ι : Type u} {α : Type v} [inst : DecidableEq α] {t : ι → Finset α} [Finite ι],
  (∀ (s : Finset ι), s.card ≤ (s.biUnion t).card) → ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.norm_const_smul : ∀ {𝕜 : Type u_1} {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [inst : (i : α) → NormedAddCommGroup (E i)]
  [inst_1 : NormedDivisionRing 𝕜] [inst_2 : (i : α) → Module 𝕜 (E i)] [inst_3 : ∀ (i : α), IsBoundedSMul 𝕜 (E i)],
  p ≠ 0 → ∀ {c : 𝕜} (f : ↥(lp E p)), ‖c • f‖ = ‖c‖ * ‖f‖
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
IntermediateField.finiteDimensional_adjoin_pair : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {x y : L},
  IsIntegral K x → IsIntegral K y → FiniteDimensional K ↥K⟮x, y⟯
-- Mathlib.Topology.ContinuousOn
continuousWithinAt_union : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {s t : Set α}
  {x : α}, ContinuousWithinAt f (s ∪ t) x ↔ ContinuousWithinAt f s x ∧ ContinuousWithinAt f t x
-- Mathlib.Algebra.Ring.Hom.Defs
RingHom.coe_addMonoidHom_injective : ∀ {α : Type u_2} {β : Type u_3} {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β}, Function.Injective fun f => ↑f
-- Mathlib.Probability.Kernel.Disintegration.StandardBorel
/-- Conditional kernel of a kernel `κ : Kernel α (β × Ω)`: a Markov kernel such that
`fst κ ⊗ₖ condKernel κ = κ` (see `MeasureTheory.Measure.compProd_fst_condKernel`).
It exists whenever `Ω` is standard Borel and either `α` is countable
or `β` is countably generated.  -/
ProbabilityTheory.Kernel.condKernel : {α : Type u_5} →
  {β : Type u_6} →
    {Ω : Type u_7} →
      {mα : MeasurableSpace α} →
        {mβ : MeasurableSpace β} →
          {mΩ : MeasurableSpace Ω} →
            [StandardBorelSpace Ω] →
              [Nonempty Ω] →
                [h : MeasurableSpace.CountableOrCountablyGenerated α β] →
                  (κ : ProbabilityTheory.Kernel α (β × Ω)) →
                    [ProbabilityTheory.IsFiniteKernel κ] → ProbabilityTheory.Kernel (α × β) Ω
-- Lean.Meta.Sym.Canon
_private.Lean.Meta.Sym.Canon.0.Lean.Meta.Sym.Canon.canon.canonLambdaLoop : Array Lean.Expr → Lean.Expr → Lean.Meta.Sym.Canon.CanonM✝ Lean.Expr
-- Init.Data.Char.Basic
/-- Converts a lowercase ASCII letter to the corresponding uppercase letter. Letters outside the ASCII
alphabet are returned unchanged.

The lowercase ASCII letters are the following: `abcdefghijklmnopqrstuvwxyz`.
 -/
Char.toUpper : Char → Char
-- Mathlib.Analysis.Calculus.BumpFunction.Basic
/-- A version of `ContDiffBump.nonneg` with `x` explicit  -/
ContDiffBump.nonneg' : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : HasContDiffBump E] {c : E}
  (f : ContDiffBump c) (x : E), 0 ≤ ↑f x
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.Stream.foldr.eq_2 : ∀ {α : Type u_1} {σ : Sort u_2} (f : α → σ → σ) (x : σ) (v : α) (r : RBTree.RBNode α) (tail : RBTree.RBNode.Stream α),
  RBTree.RBNode.Stream.foldr f (RBTree.RBNode.Stream.cons v r tail) x =
    f v (RBTree.RBNode.foldr f r (RBTree.RBNode.Stream.foldr f tail x))
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.instHashableCongrKey : {enodeMap : Lean.Meta.Grind.ENodeMap} → Hashable (Lean.Meta.Grind.CongrKey enodeMap)
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.Formula.relabel.eq_1 : ∀ {L : FirstOrder.Language} {α : Type u'} {β : Type v'} (g : α → β),
  FirstOrder.Language.Formula.relabel g = FirstOrder.Language.BoundedFormula.relabel (Sum.inl ∘ g)
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
MeasureTheory.Measure.finiteAt_nhds : ∀ {α : Type u_1} {m0 : MeasurableSpace α} [inst : TopologicalSpace α] (μ : MeasureTheory.Measure α)
  [MeasureTheory.IsLocallyFiniteMeasure μ] (x : α), μ.FiniteAtFilter (nhds x)
-- Plausible.Testable
Plausible.TestResult.gaveUp.sizeOf_spec : ∀ {p : Prop} [inst : SizeOf p] (a : ℕ), sizeOf (Plausible.TestResult.gaveUp a) = 1 + sizeOf a
-- Mathlib.Order.Filter.Lift
Filter.le_lift : ∀ {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Set α → Filter β} {h : Filter β}, h ≤ f.lift g ↔ ∀ s ∈ f, h ≤ g s
-- Mathlib.RingTheory.Regular.IsSMulRegular
isSMulRegular_on_quot_iff_lsmul_comap_le : ∀ {R : Type u_1} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (N : Submodule R M)
  (r : R), IsSMulRegular (M ⧸ N) r ↔ Submodule.comap ((LinearMap.lsmul R M) r) N ≤ N
-- Mathlib.AlgebraicGeometry.Morphisms.Immersion
AlgebraicGeometry.IsImmersion.mk : ∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} [toIsPreimmersion : AlgebraicGeometry.IsPreimmersion f],
  IsLocallyClosed (Set.range ⇑f) → AlgebraicGeometry.IsImmersion f
-- Mathlib.RingTheory.Support
/-- [Stacks Tag 00L3](https://stacks.math.columbia.edu/tag/00L3) ((2)) -/
Module.support_subset_of_injective : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] (f : M →ₗ[R] N),
  Function.Injective ⇑f → Module.support R M ⊆ Module.support R N
-- Mathlib.Analysis.Analytic.Constructions
/-- If each function in a finite family has a power series within a ball, then so does the
family as a whole. Note that the positivity assumption on the radius is only needed when
the family is empty.  -/
HasFPowerSeriesWithinOnBall.pi : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {ι : Type u_9} [inst_3 : Fintype ι] {e : E} {Fm : ι → Type u_10}
  [inst_4 : (i : ι) → NormedAddCommGroup (Fm i)] [inst_5 : (i : ι) → NormedSpace 𝕜 (Fm i)] {f : (i : ι) → E → Fm i}
  {s : Set E} {r : ENNReal} {p : (i : ι) → FormalMultilinearSeries 𝕜 E (Fm i)},
  (∀ (i : ι), HasFPowerSeriesWithinOnBall (f i) (p i) s e r) →
    0 < r → HasFPowerSeriesWithinOnBall (fun x x_1 => f x_1 x) (FormalMultilinearSeries.pi p) s e r
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
WeierstrassCurve.Jacobian.Point.fromAffine_zero : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} [inst_1 : Nontrivial R],
  WeierstrassCurve.Jacobian.Point.fromAffine 0 = 0
-- Std.Data.HashMap.Lemmas
Std.HashMap.all_eq_true_iff_forall_mem_getKey_getElem : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {p : α → β → Bool}, m.all p = true ↔ ∀ (a : α) (h : a ∈ m), p (m.getKey a h) m[a] = true
-- Mathlib.Combinatorics.Enumerative.Composition
Composition.sizeUpTo_index_le : ∀ {n : ℕ} (c : Composition n) (j : Fin n), c.sizeUpTo ↑(c.index j) ≤ ↑j
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1.Stmt.move.inj : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} {a : Turing.Dir} {a_1 : Turing.TM1.Stmt Γ Λ σ} {a_2 : Turing.Dir}
  {a_3 : Turing.TM1.Stmt Γ Λ σ}, Turing.TM1.Stmt.move a a_1 = Turing.TM1.Stmt.move a_2 a_3 → a = a_2 ∧ a_1 = a_3
-- Mathlib.Algebra.Group.Submonoid.Defs
Submonoid.subtype_apply : ∀ {M : Type u_4} [inst : MulOneClass M] {s : Submonoid M} (x : ↥s), s.subtype x = ↑x
-- Mathlib.CategoryTheory.Monoidal.Ring
CategoryTheory.RingObjCat.instFaithfulForget : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C], (CategoryTheory.RingObjCat.forget C).Faithful
-- Mathlib.Algebra.QuaternionBasis
QuaternionAlgebra.lift_apply : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] {c₁ c₂ c₃ : R}
  (q : QuaternionAlgebra.Basis A c₁ c₂ c₃), QuaternionAlgebra.lift q = q.liftHom