mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Idempotents
CompleteOrthogonalIdempotents.pair_iff : ∀ {R : Type u_1} [inst : Ring R] {x y : R}, CompleteOrthogonalIdempotents ![x, y] ↔ IsIdempotentElem x ∧ y = 1 - x
-- Mathlib.Data.NNRat.Lemmas
Rat.toNNRat_div' : ∀ {p q : ℚ}, 0 ≤ q → (p / q).toNNRat = p.toNNRat / q.toNNRat
-- Mathlib.RingTheory.TwoSidedIdeal.Lattice
/-- **Alias** of the forward direction of `TwoSidedIdeal.one_mem_iff`. -/
TwoSidedIdeal.eq_top : ∀ {R : Type u_2} [inst : NonAssocRing R] (I : TwoSidedIdeal R), 1 ∈ I → I = ⊤
-- Mathlib.Algebra.Algebra.Unitization
Unitization.inl_one : ∀ {R : Type u_1} (A : Type u_2) [inst : One R] [inst_1 : Zero A], Unitization.inl 1 = 1
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.getD_diff_of_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  {k : α} {fallback : β}, k ∈ t₂ → Std.DTreeMap.Const.getD (t₁ \ t₂) k fallback = fallback
-- Mathlib.LinearAlgebra.TensorProduct.Tower
TensorProduct.AlgebraTensorModule.tensorTensorTensorComm_tmul : ∀ (R : Type uR) (S : Type uS) (A : Type uA) (B : Type uB) {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ}
  [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B]
  [inst_5 : AddCommMonoid M] [inst_6 : Module R M] [inst_7 : Module A M] [inst_8 : Module B M]
  [inst_9 : IsScalarTower R A M] [inst_10 : IsScalarTower R B M] [inst_11 : SMulCommClass A B M]
  [inst_12 : AddCommMonoid N] [inst_13 : Module R N] [inst_14 : AddCommMonoid P] [inst_15 : Module A P]
  [inst_16 : AddCommMonoid Q] [inst_17 : Module R Q] [inst_18 : Module R P] [inst_19 : IsScalarTower R A P]
  [inst_20 : Algebra A B] [inst_21 : IsScalarTower A B M] [inst_22 : CommSemiring S] [inst_23 : Algebra R S]
  [inst_24 : Algebra S B] [inst_25 : Module S M] [inst_26 : Module S N] [inst_27 : IsScalarTower R S M]
  [inst_28 : SMulCommClass A S M] [inst_29 : SMulCommClass S A M] [inst_30 : IsScalarTower S B M]
  [inst_31 : IsScalarTower R S N] (m : M) (n : N) (p : P) (q : Q),
  (TensorProduct.AlgebraTensorModule.tensorTensorTensorComm R S A B M N P Q) (m ⊗ₜ[S] n ⊗ₜ[A] (p ⊗ₜ[R] q)) =
    m ⊗ₜ[A] p ⊗ₜ[S] (n ⊗ₜ[R] q)
-- Mathlib.Order.Interval.Set.Infinite
Set.Ioo.infinite : ∀ {α : Type u_1} [inst : Preorder α] [DenselyOrdered α] {a b : α}, a < b → Infinite ↑(Set.Ioo a b)
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Increment
/-- The increment partition has a prescribed (very big) size in terms of the original partition.  -/
SzemerediRegularity.card_increment : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {P : Finpartition Finset.univ} {hP : P.IsEquipartition}
  {G : SimpleGraph α} [inst_2 : DecidableRel G.Adj] {ε : ℝ},
  P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α →
    ¬P.IsUniform G ε → (SzemerediRegularity.increment hP G ε).parts.card = SzemerediRegularity.stepBound P.parts.card
-- Mathlib.Topology.Category.Profinite.Nobeling.Basic
Profinite.NobelingProof.Proj.congr_simp : ∀ {I : Type u} (J J_1 : I → Prop),
  J = J_1 →
    ∀ {inst : (i : I) → Decidable (J i)} [inst_1 : (i : I) → Decidable (J_1 i)] (a a_1 : I → Bool),
      a = a_1 →
        ∀ (a_2 a_3 : I), a_2 = a_3 → Profinite.NobelingProof.Proj J a a_2 = Profinite.NobelingProof.Proj J_1 a_1 a_3
-- Mathlib.Order.Hom.BoundedLattice
SupBotHom.cancel_right : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Max α] [inst_1 : Bot α] [inst_2 : Max β] [inst_3 : Bot β]
  [inst_4 : Max γ] [inst_5 : Bot γ] {g₁ g₂ : SupBotHom β γ} {f : SupBotHom α β},
  Function.Surjective ⇑f → (g₁.comp f = g₂.comp f ↔ g₁ = g₂)
-- Mathlib.RingTheory.RingHom.Smooth
RingHom.formallySmooth_algebraMap : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S],
  (algebraMap R S).FormallySmooth ↔ Algebra.FormallySmooth R S
-- Mathlib.CategoryTheory.PathCategory.MorphismProperty
CategoryTheory.Paths.liftNatIso_inv_app : ∀ {V : Type u₁} [inst : Quiver V] {C : Type u_2} [inst_1 : CategoryTheory.Category.{v_2, u_2} C]
  {F G : CategoryTheory.Functor (CategoryTheory.Paths V) C} (α_app : (v : V) → F.obj v ≅ G.obj v)
  (α_nat :
    ∀ {X Y : V} (f : X ⟶ Y),
      CategoryTheory.CategoryStruct.comp (F.map f.toPath) (α_app Y).hom =
        CategoryTheory.CategoryStruct.comp (α_app X).hom (G.map f.toPath))
  (X : CategoryTheory.Paths V), (CategoryTheory.Paths.liftNatIso α_app α_nat).inv.app X = (α_app X).inv
-- Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
/-- Construct the equivalence class `[f]` of a simple function `f` satisfying `MemLp`.  -/
MeasureTheory.SimpleFunc.toLp : {α : Type u_1} →
  {E : Type u_4} →
    [inst : MeasurableSpace α] →
      [inst_1 : NormedAddCommGroup E] →
        {p : ENNReal} →
          {μ : MeasureTheory.Measure α} →
            (f : MeasureTheory.SimpleFunc α E) → MeasureTheory.MemLp (⇑f) p μ → ↥(MeasureTheory.Lp.simpleFunc E p μ)
-- Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm
PiTensorProduct.mapL_id : ∀ {ι : Type u_1} [inst : Fintype ι] {𝕜 : Type u_2} {E : ι → Type u_3} [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)]
  [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)],
  (PiTensorProduct.mapL fun i => ContinuousLinearMap.id 𝕜 (E i)) =
    ContinuousLinearMap.id 𝕜 (PiTensorProduct 𝕜 fun i => E i)
-- Mathlib.CategoryTheory.MorphismProperty.LiftingProperty
CategoryTheory.MorphismProperty.rlp_isStableUnderRetracts : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (T : CategoryTheory.MorphismProperty C),
  T.rlp.IsStableUnderRetracts
-- Init.Grind.AC
Lean.Grind.AC.Expr : Type
-- Mathlib.Algebra.Category.Grp.Basic
AddGrpCat.instCoeSortType.eq_1 : AddGrpCat.instCoeSortType = { coe := AddGrpCat.carrier }
-- Mathlib.Analysis.Real.Pi.Irrational
/-- Auxiliary for the proof that `π` is irrational.
The integrand in the definition of `I` is bounded by 1 and the interval has length 2, so the
integral is bounded above by `2`.
 -/
_private.Mathlib.Analysis.Real.Pi.Irrational.0.I_le : ∀ (n : ℕ), I✝ n (Real.pi / 2) ≤ 2
-- Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Matrix.IsAdjMatrix.apply_ne_zero_iff : ∀ {α : Type u_1} {V : Type u_2} {A : Matrix V V α} [inst : MulZeroOneClass α] [Nontrivial α],
  A.IsAdjMatrix → ∀ (i j : V), ¬A i j = 0 ↔ A i j = 1
-- Mathlib.Algebra.Order.Hom.MonoidWithZero
OrderMonoidWithZeroHom.instOrderHomClass : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : MulZeroOneClass α]
  [inst_3 : MulZeroOneClass β], OrderHomClass (α →*₀o β) α β
-- Mathlib.Analysis.Normed.Lp.WithLp
WithLp.coe_congr : ∀ (p : ENNReal) {V : Type u_4} {V' : Type u_5} (f : V ≃ V'), ⇑(WithLp.congr p f) = WithLp.map p ⇑f
-- Mathlib.Logic.Function.Coequalizer
Function.Coequalizer.desc_mk : ∀ {α : Type u_1} {β : Type u_2} (f g : α → β) {γ : Type u_3} (u : β → γ) (hu : u ∘ f = u ∘ g) (x : β),
  Function.Coequalizer.desc f g u hu (Function.Coequalizer.mk f g x) = u x
-- Lean.Meta.Tactic.Grind.Types
/-- E-matching theorem instantiation diagnostics  -/
Lean.Meta.Grind.State.ematchDiags : Lean.Meta.Grind.State → Lean.PArray Lean.Meta.Grind.EMatchDiagInfo
-- Mathlib.Algebra.Group.Subgroup.Lattice
Subgroup.mem_closure : ∀ {G : Type u_1} [inst : Group G] {k : Set G} {x : G}, x ∈ Subgroup.closure k ↔ ∀ (K : Subgroup G), k ⊆ ↑K → x ∈ K
-- Lean.HeadIndex
Lean.HeadIndex.proj.sizeOf_spec : ∀ (structName : Lean.Name) (idx : ℕ), sizeOf (Lean.HeadIndex.proj structName idx) = 1 + sizeOf structName + sizeOf idx
-- Mathlib.Algebra.Module.Submodule.Lattice
Submodule.top_toAddSubmonoid : ∀ {R : Type u_1} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  ⊤.toAddSubmonoid = ⊤
-- Aesop.Index.DiscrTreeConfig
Aesop.mkDiscrTreePath : Lean.Expr → Lean.MetaM (Array Lean.Meta.DiscrTree.Key)
-- Mathlib.Algebra.Group.Defs
/-- A monoid in which multiplication is cancellative.  -/
CancelMonoid : Type u → Type u
-- Mathlib.Probability.Kernel.Representation
_private.Mathlib.Probability.Kernel.Representation.0.ProbabilityTheory.Kernel.exists_measurable_map_eq_unitInterval_aux : ∀ {X : Type u_1} {mX : MeasurableSpace X} (κ : ProbabilityTheory.Kernel X ↑unitInterval)
  [ProbabilityTheory.IsMarkovKernel κ],
  ∃ f, Measurable (Function.uncurry f) ∧ ∀ (a : X), MeasureTheory.Measure.map (f a) MeasureTheory.volume = κ a
-- Mathlib.Algebra.Order.IsBotOne
IsBotOneClass.toOrderBot.eq_1 : ∀ (α : Type u_1) [inst : LE α] [inst_1 : One α] [inst_2 : IsBotOneClass α],
  IsBotOneClass.toOrderBot α = { bot := 1, bot_le := ⋯ }
-- Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
/-- The binary cofan whose point is `coprod F G`.  -/
CategoryTheory.FunctorToTypes.binaryCoproductCocone : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (F G : CategoryTheory.Functor C (Type w)) → CategoryTheory.Limits.BinaryCofan F G
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.eLpNormEssSup.eq_1 : ∀ {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} [inst : ENorm ε] (f : α → ε) (μ : MeasureTheory.Measure α),
  MeasureTheory.eLpNormEssSup f μ = essSup (fun x => ‖f x‖ₑ) μ
-- Mathlib.Data.Vector.Basic
List.Vector.head?_toList : ∀ {α : Type u_1} {n : ℕ} (v : List.Vector α n.succ), v.toList.head? = some v.head
-- Mathlib.Algebra.Group.Submonoid.Defs
/-- An additive submonoid of an additive monoid `M` is a subset containing 0 and
closed under addition.  -/
AddSubmonoid : (M : Type u_3) → [AddZeroClass M] → Type u_3
-- Mathlib.Tactic.Ring.RingNF
/-- `ring_nf` simplifies expressions in the language of commutative (semi)rings,
which rewrites all ring expressions into a normal form, allowing variables in the exponents.

`ring_nf` works as both a tactic and a conv tactic.

See also the `ring` tactic for solving a goal which is an equation in the language
of commutative (semi)rings.

* `ring_nf!` will use a more aggressive reducibility setting to identify atoms.
* `ring_nf (config := cfg)` allows for additional configuration (see `RingNF.Config`):
  * `red`: the reducibility setting (overridden by `!`)
  * `zetaDelta`: if true, local let variables can be unfolded (overridden by `!`)
  * `recursive`: if true, `ring_nf` will also recurse into atoms
* `ring_nf at l1 l2 ...` can be used to rewrite at the given locations.

Examples:
This can be used non-terminally to normalize ring expressions in the goal such as
`⊢ P (x + x + x)` ~> `⊢ P (x * 3)`, as well as being able to prove some equations that
`ring` cannot because they involve ring reasoning inside a subterm, such as
`sin (x + y) + sin (y + x) = 2 * sin (x + y)`.
 -/
Mathlib.Tactic.RingNF.ringNF : Lean.ParserDescr
-- Mathlib.Topology.Path
Path.extend_of_one_le : ∀ {X : Type u_1} [inst : TopologicalSpace X] {a b : X} (γ : Path a b) {t : ℝ}, 1 ≤ t → γ.extend t = b
-- Mathlib.Order.Concept
intentClosure_apply : ∀ {α : Type u_2} {β : Type u_3} (r : α → β → Prop) (x : Set β), (intentClosure r) x = upperPolar r (lowerPolar r x)
-- Mathlib.Analysis.Asymptotics.Defs
/-- See also `Asymptotics.IsBigO.of_norm_eventuallyLE`, which is the same lemma
stated using `Filter.EventuallyLE` instead of `Filter.Eventually`.  -/
Filter.Eventually.isBigO : ∀ {α : Type u_1} {E : Type u_3} [inst : Norm E] {f : α → E} {g : α → ℝ} {l : Filter α},
  (∀ᶠ (x : α) in l, ‖f x‖ ≤ g x) → f =O[l] g
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Presieve.bindOfArrows_ofArrows : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {ι : Type u_1} {S : C} {X : ι → C} (f : (i : ι) → X i ⟶ S)
  {σ : ι → Type u_2} {Y : (i : ι) → σ i → C} (g : (i : ι) → (j : σ i) → Y i j ⟶ X i),
  (CategoryTheory.Presieve.bindOfArrows X f fun i => CategoryTheory.Presieve.ofArrows (Y i) (g i)) =
    CategoryTheory.Presieve.ofArrows (fun p => Y p.fst p.snd) fun p =>
      CategoryTheory.CategoryStruct.comp (g p.fst p.snd) (f p.fst)
-- Mathlib.CategoryTheory.GuitartExact.VerticalComposition
/-- A 2-square stays Guitart exact if we replace the left and right functors
by isomorphic functors. See also `whiskerVertical_iff`.  -/
CategoryTheory.TwoSquare.GuitartExact.whiskerVertical : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_4} {D₂ : Type u_5} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_4, u_4} D₁]
  [inst_3 : CategoryTheory.Category.{v_5, u_5} D₂] {T : CategoryTheory.Functor C₁ D₁} {L : CategoryTheory.Functor C₁ C₂}
  {R : CategoryTheory.Functor D₁ D₂} {B : CategoryTheory.Functor C₂ D₂} (w : CategoryTheory.TwoSquare T L R B)
  {L' : CategoryTheory.Functor C₁ C₂} {R' : CategoryTheory.Functor D₁ D₂} [w.GuitartExact] (α : L ≅ L') (β : R ≅ R'),
  (w.whiskerVertical α.hom β.inv).GuitartExact
-- Mathlib.Topology.Covering.Quotient
isQuotientCoveringMap_iff : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] (f : E → X) (G : Type u_3)
  [inst_2 : Group G] [inst_3 : MulAction G E],
  IsQuotientCoveringMap f G ↔
    Topology.IsQuotientMap f ∧
      ContinuousConstSMul G E ∧
        (∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit G e₂) ∧
          ∀ (e : E), ∃ U ∈ nhds e, ∀ (g : G), ((fun x => g • x) '' U ∩ U).Nonempty → g = 1
-- Mathlib.Algebra.Field.Subfield.Basic
Subfield.mem_top : ∀ {K : Type u} [inst : DivisionRing K] (x : K), x ∈ ⊤
-- Mathlib.Analysis.Normed.Group.Seminorm
GroupSeminorm.instInhabited : {E : Type u_3} → [inst : Group E] → Inhabited (GroupSeminorm E)
-- Mathlib.Analysis.Complex.Basic
Complex.hasSum_im : ∀ {α : Type u_1} {L : SummationFilter α} {f : α → ℂ} {x : ℂ}, HasSum f x L → HasSum (fun x => (f x).im) x.im L
-- Mathlib.LinearAlgebra.LinearIndependent.Lemmas
LinearIndepOn.notMem_span_iff_id : ∀ {K : Type u_3} {V : Type u} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {s : Set V}
  {a : V}, LinearIndepOn K id s → (a ∉ Submodule.span K s ↔ LinearIndepOn K id (insert a s) ∧ a ∉ s)
-- Mathlib.Order.Comparable
AntisymmRel.incompRel_congr_right : ∀ {α : Type u_1} {a b c : α} [inst : Preorder α],
  AntisymmRel (fun x1 x2 => x1 ≤ x2) b c → (IncompRel (fun x1 x2 => x1 ≤ x2) a b ↔ IncompRel (fun x1 x2 => x1 ≤ x2) a c)
-- Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting
/-- The projective system `j ↦ SqStruct c p f g j.unop`.  -/
CategoryTheory.HasLiftingProperty.transfiniteComposition.sqFunctor : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type w} →
      [inst_1 : LinearOrder J] →
        [inst_2 : OrderBot J] →
          {F : CategoryTheory.Functor J C} →
            (c : CategoryTheory.Limits.Cocone F) →
              {X Y : C} → (X ⟶ Y) → (F.obj ⊥ ⟶ X) → (c.pt ⟶ Y) → CategoryTheory.Functor Jᵒᵖ (Type v)
-- Mathlib.Probability.Density
MeasureTheory.map_eq_withDensity_pdf : ∀ {Ω : Type u_1} {E : Type u_2} [inst : MeasurableSpace E] {m : MeasurableSpace Ω} (X : Ω → E)
  (ℙ : MeasureTheory.Measure Ω) (μ : autoParam (MeasureTheory.Measure E) MeasureTheory.map_eq_withDensity_pdf._auto_1)
  [hX : MeasureTheory.HasPDF X ℙ μ], MeasureTheory.Measure.map X ℙ = μ.withDensity (MeasureTheory.pdf X ℙ μ)
-- Mathlib.Analysis.Convex.Function
ConvexOn.le_right_of_left_le' : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommMonoid β] [inst_4 : LinearOrder β] [IsOrderedCancelAddMonoid β] [inst_6 : SMul 𝕜 E]
  [inst_7 : Module 𝕜 β] [PosSMulStrictMono 𝕜 β] {s : Set E} {f : E → β},
  ConvexOn 𝕜 s f →
    ∀ {x y : E} {a b : 𝕜}, x ∈ s → y ∈ s → 0 ≤ a → 0 < b → a + b = 1 → f x ≤ f (a • x + b • y) → f (a • x + b • y) ≤ f y
-- Mathlib.CategoryTheory.Preadditive.Mat
CategoryTheory.Mat_.instPreadditive : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.Preadditive C] → CategoryTheory.Preadditive (CategoryTheory.Mat_ C)
-- Mathlib.Analysis.InnerProductSpace.PiL2
EuclideanSpace.toLp_single : ∀ {ι : Type u_1} {𝕜 : Type u_3} [inst : RCLike 𝕜] [inst_1 : DecidableEq ι] (i : ι) (a : 𝕜),
  WithLp.toLp 2 (Pi.single i a) = EuclideanSpace.single i a
-- Mathlib.Combinatorics.Matroid.Minor.Delete
Matroid.IsCircuit.of_delete : ∀ {α : Type u_1} {M : Matroid α} {D C : Set α}, (M.delete D).IsCircuit C → M.IsCircuit C
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.mem_carrier : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] (N : LieSubmodule R L M) {x : M}, x ∈ (↑N).carrier ↔ x ∈ ↑N
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKeyD_filter_key : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α] {f : α → Bool} {k fallback : α},
  (↑m).WF →
    (Std.DHashMap.Internal.Raw₀.filter (fun k x => f k) m).getKeyD k fallback =
      (Option.filter f (m.getKey? k)).getD fallback
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
Convexity.convexCombPair_iConvexComb_right : ∀ {R : Type u_1} {M : Type u_3} {J : Type u_7} [inst : PartialOrder R] [inst_1 : Semiring R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : Convexity.ConvexSpace R M] {s t : R} (hs : 0 ≤ s) (ht : 0 ≤ t)
  (h : s + t = 1) (m : M) (g : Convexity.StdSimplex R J) (e : J → M),
  Convexity.convexCombPair s t hs ht h m (Convexity.iConvexComb g e) =
    Convexity.sConvexComb
      (Convexity.convexCombPair s t hs ht h (Convexity.StdSimplex.single m) (Convexity.StdSimplex.map e g))
-- Mathlib.Tactic.CategoryTheory.Bicategory.Normalize
Mathlib.Tactic.Bicategory.evalWhiskerLeft_comp : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c d : B} {f : a ⟶ b} {g : b ⟶ c} {h i : c ⟶ d} {η : h ⟶ i}
  {η₁ : CategoryTheory.CategoryStruct.comp g h ⟶ CategoryTheory.CategoryStruct.comp g i}
  {η₂ :
    CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h) ⟶
      CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g i)}
  {η₃ :
    CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h) ⟶
      CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g) i}
  {η₄ :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g) h ⟶
      CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g) i},
  CategoryTheory.Bicategory.whiskerLeft g η = η₁ →
    CategoryTheory.Bicategory.whiskerLeft f η₁ = η₂ →
      CategoryTheory.CategoryStruct.comp η₂ (CategoryTheory.Bicategory.associator f g i).inv = η₃ →
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g h).hom η₃ = η₄ →
          CategoryTheory.Bicategory.whiskerLeft (CategoryTheory.CategoryStruct.comp f g) η = η₄
-- Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
MeasureTheory.Measure.pairwise_aedisjoint_of_aedisjoint_forall_ne_zero : ∀ {G : Type u_5} {α : Type u_6} [inst : AddGroup G] [inst_1 : AddAction G α] {x : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {s : Set α},
  (∀ (g : G), g ≠ 0 → MeasureTheory.AEDisjoint μ (g +ᵥ s) s) →
    (∀ (g : G), MeasureTheory.Measure.QuasiMeasurePreserving (fun x => g +ᵥ x) μ μ) →
      Pairwise (Function.onFun (MeasureTheory.AEDisjoint μ) fun g => g +ᵥ s)
-- Mathlib.RingTheory.Jacobson.Ring
isJacobsonRing_of_surjective : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [H : IsJacobsonRing R],
  (∃ f, Function.Surjective ⇑f) → IsJacobsonRing S
-- Init.Data.Sum.Lemmas
Sum.bnot_isLeft : ∀ {α : Type u_1} {β : Type u_2} (x : α ⊕ β), (!x.isLeft) = x.isRight
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
WeierstrassCurve.natDegree_Ψ₃_pos : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R), 3 ≠ 0 → 0 < W.Ψ₃.natDegree
-- Mathlib.Probability.Kernel.Composition.Comp
ProbabilityTheory.Kernel.comp_apply : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} (η : ProbabilityTheory.Kernel β γ) (κ : ProbabilityTheory.Kernel α β) (a : α),
  (η.comp κ) a = (κ a).bind ⇑η
-- Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
MeasureTheory.LevyProkhorov.ofMeasure.injEq : ∀ {α : Type u_2} (toMeasure toMeasure_1 : α),
  (MeasureTheory.LevyProkhorov.ofMeasure toMeasure = MeasureTheory.LevyProkhorov.ofMeasure toMeasure_1) =
    (toMeasure = toMeasure_1)
-- Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric
Complex.regularizedGaussHGFunSeries_symm : ∀ (a b c : ℂ), a.regularizedGaussHGFunSeries b c = b.regularizedGaussHGFunSeries a c
-- Mathlib.Topology.Homotopy.Basic
ContinuousMap.Homotopy.comp_apply : ∀ {X : Type u} {Y : Type v} {Z : Type w} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] {f₀ f₁ : C(X, Y)} {g₀ g₁ : C(Y, Z)} (G : g₀.Homotopy g₁) (F : f₀.Homotopy f₁)
  (x : ↑unitInterval × X), (G.comp F) x = G (x.1, F x)
-- Mathlib.Topology.Baire.LocallyCompactRegular
/-- A Gδ subset of a locally compact R₁ space is Baire.  -/
IsGδ.baireSpace_of_t2Space_locallyCompactSpace : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X} [R1Space X] [LocallyCompactSpace X], IsGδ s → BaireSpace ↑s
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.SimplicialObject.whiskering_obj_map_app : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (D : Type u_1) [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  (H : CategoryTheory.Functor C D) {X Y : CategoryTheory.Functor SimplexCategoryᵒᵖ C} (α : X ⟶ Y)
  (X_1 : SimplexCategoryᵒᵖ),
  (((CategoryTheory.SimplicialObject.whiskering C D).obj H).map α).app X_1 = H.map (α.app X_1)
-- Mathlib.Algebra.Vertex.HVertexOperator
/-- The composite of two heterogeneous vertex operators acting on a vector, as an iterated Hahn
series.  -/
HVertexOperator.compHahnSeries : {Γ : Type u_5} →
  {Γ' : Type u_6} →
    [inst : PartialOrder Γ] →
      [inst_1 : PartialOrder Γ'] →
        {R : Type u_7} →
          [inst_2 : CommRing R] →
            {U : Type u_8} →
              {V : Type u_9} →
                {W : Type u_10} →
                  [inst_3 : AddCommGroup U] →
                    [inst_4 : Module R U] →
                      [inst_5 : AddCommGroup V] →
                        [inst_6 : Module R V] →
                          [inst_7 : AddCommGroup W] →
                            [inst_8 : Module R W] →
                              HVertexOperator Γ R V W → HVertexOperator Γ' R U V → U → HahnSeries Γ' (HahnSeries Γ W)
-- Mathlib.Analysis.Normed.Lp.MeasurableSpace
WithLp.measurableSpace.eq_1 : ∀ (p : ENNReal) (X : Type u_1) [inst : MeasurableSpace X],
  WithLp.measurableSpace p X = MeasurableSpace.comap WithLp.ofLp inferInstance
-- Mathlib.LinearAlgebra.AffineSpace.Independent
/-- A set is affinely independent if and only if the differences from
a base point in that set are linearly independent.  -/
affineIndependent_set_iff_linearIndependent_vsub : ∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {s : Set P} {p₁ : P},
  p₁ ∈ s → ((AffineIndependent k fun p => ↑p) ↔ LinearIndependent k fun (v : ↑((fun p => p -ᵥ p₁) '' (s \ {p₁}))) => ↑v)
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
LatticeOrderedAddCommGroup.solidClosure_min : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : AddCommGroup α] {s t : Set α},
  s ⊆ t → LatticeOrderedAddCommGroup.IsSolid t → LatticeOrderedAddCommGroup.solidClosure s ⊆ t
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonHover.toJson : Lean.Lsp.Hover → Lean.Json
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Udiv
Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.BlastDivSubtractShiftOutput.r : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {old : Std.Sat.AIG α} →
        {w : ℕ} →
          (self : Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.BlastDivSubtractShiftOutput old w) → self.aig.RefVec w
-- Lean.Util.LeanOptions
Lean.LeanOptionValue.ofBool.sizeOf_spec : ∀ (b : Bool), sizeOf (Lean.LeanOptionValue.ofBool b) = 1 + sizeOf b
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.subtypeSupportEqEquiv_symm_apply_coe : ∀ {ι : Type u} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → Zero (β i)]
  [inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] (s : Finset ι) (f : (i : ↥s) → { x // x ≠ 0 }),
  ↑((DFinsupp.subtypeSupportEqEquiv s).symm f) = DFinsupp.mk s fun i => ↑(f i)