mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.ModelTheory.Arithmetic.Presburger.Basic
FirstOrder.Language.presburger.realize_add : ∀ {α : Type u_1} {t₁ t₂ : FirstOrder.Language.presburger.Term α} {M : Type u_2} {v : α → M} [inst : Zero M]
  [inst_1 : One M] [inst_2 : Add M],
  FirstOrder.Language.Term.realize v (t₁ + t₂) =
    FirstOrder.Language.Term.realize v t₁ + FirstOrder.Language.Term.realize v t₂
-- Mathlib.GroupTheory.OrderOfElement
powCoprime_inv : ∀ {n : ℕ} {G : Type u_6} [inst : Group G] (h : (Nat.card G).Coprime n) {g : G},
  (powCoprime h) g⁻¹ = ((powCoprime h) g)⁻¹
-- Mathlib.Probability.Kernel.IonescuTulcea.Traj
ProbabilityTheory.Kernel.trajContent_ne_top : ∀ {X : ℕ → Type u_1} [inst : (n : ℕ) → MeasurableSpace (X n)]
  {κ : (n : ℕ) → ProbabilityTheory.Kernel ((i : ↥(Finset.Iic n)) → X ↑i) (X (n + 1))}
  [inst_1 : ∀ (n : ℕ), ProbabilityTheory.IsMarkovKernel (κ n)] {a : ℕ} {x : (i : ↥(Finset.Iic a)) → X ↑i}
  {s : Set ((n : ℕ) → X n)}, (ProbabilityTheory.Kernel.trajContent κ x) s ≠ ⊤
-- Lean.Meta.Sym.Offset
/-- Returns `true` if `e` is an offset term. -/
Lean.Meta.Sym.isOffset : Lean.Expr → Bool
-- Lean.Meta.Tactic.Simp.Rewrite
/-- Remark: the parameter tag is used for creating trace messages. It is irrelevant otherwise.
 -/
Lean.Meta.Simp.rewrite? : Lean.Expr →
  Lean.Meta.SimpTheoremTree →
    Lean.PHashSet Lean.Meta.Origin → String → Bool → Lean.Meta.SimpM (Option Lean.Meta.Simp.Result)
-- Mathlib.Data.Fintype.Sets
Finset.Subtype.fintype : {α : Type u_1} → (s : Finset α) → Fintype ↥s
-- Mathlib.Analysis.Real.Pi.Irrational
/-- If `x` is rational, it can be written as `a / b` with `a : ℤ` and `b : ℕ` satisfying `b > 0`.  -/
_private.Mathlib.Analysis.Real.Pi.Irrational.0.not_irrational_exists_rep : ∀ {x : ℝ}, ¬Irrational x → ∃ a b, 0 < b ∧ x = ↑a / ↑b
-- Mathlib.Order.BooleanAlgebra.Set
Set.insert_sdiff_insert : ∀ {α : Type u_1} {s t : Set α} {a : α}, insert a (s \ insert a t) = insert a (s \ t)
-- Init.Grind.ToInt
/-- The embedding takes subtraction to subtraction, wrapped into the range interval.  -/
Lean.Grind.ToInt.Sub.toInt_sub : ∀ {α : Type u} {inst : Sub α} {I : outParam Lean.Grind.IntInterval} {inst_1 : Lean.Grind.ToInt α I}
  [self : Lean.Grind.ToInt.Sub α I] (x y : α), ↑(x - y) = I.wrap (↑x - ↑y)
-- Mathlib.Probability.Kernel.Composition.ParallelComp
ProbabilityTheory.Kernel.id_parallelComp_id : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β},
  ProbabilityTheory.Kernel.id.parallelComp ProbabilityTheory.Kernel.id = ProbabilityTheory.Kernel.id
-- Mathlib.CategoryTheory.Limits.Opposites
CategoryTheory.Limits.hasColimitsOfSize_opposite_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C],
  CategoryTheory.Limits.HasColimitsOfSize.{v₂, u₂, v₁, u₁} Cᵒᵖ ↔
    CategoryTheory.Limits.HasLimitsOfSize.{v₂, u₂, v₁, u₁} C
-- Mathlib.RingTheory.DividedPowers.DPMorphism
DividedPowers.DPMorphism.toRingHom : {A : Type u_3} →
  {B : Type u_4} →
    [inst : CommSemiring A] →
      [inst_1 : CommSemiring B] →
        {I : Ideal A} → {J : Ideal B} → {hI : DividedPowers I} → {hJ : DividedPowers J} → hI.DPMorphism hJ → A →+* B
-- Std.Data.DHashMap.Internal.RawLemmas
_private.Std.Data.DHashMap.Internal.RawLemmas.0.Std.DHashMap.Internal.Raw₀.perm_keys_congr_left : ∀ {α : Type u} {β : α → Type v} {l l' : List ((a : α) × β a)} {l₂ : List α},
  l.Perm l' → ((Std.Internal.List.keys l).Perm l₂ ↔ (Std.Internal.List.keys l').Perm l₂)
-- Mathlib.Order.WellFoundedSet
Set.Subsingleton.wellFoundedOn : ∀ {α : Type u_2} {r : α → α → Prop} [IsStrictOrder α r] {s : Set α}, s.Subsingleton → s.WellFoundedOn r
-- Mathlib.CategoryTheory.Triangulated.Generators
CategoryTheory.ObjectProperty.instNonemptyTriangEnvelope : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (P : CategoryTheory.ObjectProperty C) [P.Nonempty], P.triangEnvelope.Nonempty
-- Mathlib.Algebra.Group.Units.Basic
AddRightCancelMonoid.add_ne_zero : ∀ {α : Type u} [inst : AddRightCancelMonoid α] [Subsingleton (AddUnits α)] {a b : α}, a + b ≠ 0 ↔ a ≠ 0 ∨ b ≠ 0
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion
ProfiniteAddGrp.ProfiniteCompletion.mono_eta_iff_residuallyFinite : ∀ (G : AddGrpCat), CategoryTheory.Mono (ProfiniteAddGrp.ProfiniteCompletion.eta G) ↔ AddGroup.ResiduallyFinite ↑G
-- Init.Data.String.Lemmas.FindPos
String.posLE_dec : ∀ {s : String} {p : String.Pos.Raw} (h : 0 < p), s.posLE p.dec = s.posLT p h
-- Mathlib.RingTheory.Extension.Cotangent.Basic
Algebra.Generators.cotangentSpaceBasis_repr_one_tmul : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {ι : Type w}
  (P : Algebra.Generators R S ι) (x : P.toExtension.Ring) (i : ι),
  (P.cotangentSpaceBasis.repr (1 ⊗ₜ[P.toExtension.Ring] (KaehlerDifferential.D R P.toExtension.Ring) x)) i =
    (MvPolynomial.aeval P.val) ((MvPolynomial.pderiv i) x)
-- Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
/-- The `PowerBasis` of `adjoin R {x}` given by `x`. See `Algebra.adjoin.powerBasis` for a version
over a field.  -/
Algebra.adjoin.powerBasis' : {R : Type u_1} →
  {S : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [IsDomain R] →
          [inst_3 : Algebra R S] →
            [IsIntegrallyClosed R] →
              [IsDomain S] → [Module.IsTorsionFree R S] → {x : S} → IsIntegral R x → PowerBasis R ↥R[x]
-- Mathlib.Data.Num.ZNum
ZNum.bit1.eq_2 : ∀ (a : PosNum), (ZNum.pos a).bit1 = ZNum.pos a.bit1
-- Mathlib.Dynamics.Ergodic.Action.OfMinimal
aeconst_of_dense_aestabilizer_smul : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [ContinuousInv G] {X : Type u_2}
  [inst_3 : TopologicalSpace X] [R1Space X] [inst_5 : MeasurableSpace X] [BorelSpace X] [inst_7 : MulAction G X]
  [ContinuousSMul G X] {μ : MeasureTheory.Measure X} [MeasureTheory.IsFiniteMeasure μ] [μ.InnerRegular]
  [inst_11 : ErgodicSMul G X μ] {s : Set X},
  MeasureTheory.NullMeasurableSet s μ →
    Dense ↑(MulAction.aestabilizer G μ s) → Filter.EventuallyConst s (MeasureTheory.ae μ)
-- Init.Data.Iterators.Combinators.Monadic.Append
Std.Iterators.Types.Append.rel_fstDone : ∀ {α₁ α₂ : Type w} {m : Type w → Type w'} {β : Type w} [inst : Monad m] [inst_1 : Std.Iterator α₁ m β]
  [inst_2 : Std.Iterator α₂ m β] [inst_3 : Std.Iterators.Finite α₁ m] [inst_4 : Std.Iterators.Finite α₂ m]
  {it₁ : Std.IterM m β} {it₂ : Std.IterM m β},
  Std.Iterators.Types.Append.Rel α₁ α₂ m β (Std.IterM.Intermediate.appendSnd α₁ it₂) (it₁.append it₂)
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
AlgEquiv.subsingleton_left : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Semiring B] [inst_4 : Algebra R B] [Subsingleton (Subalgebra R A)], Subsingleton (A ≃ₐ[R] B)
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.Homotopy.add_h₀ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂} (h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂)
  (h' : CategoryTheory.ShortComplex.Homotopy φ₃ φ₄), (h.add h').h₀ = h.h₀ + h'.h₀
-- Mathlib.CategoryTheory.CommSq
CategoryTheory.CommSq.eq_of_epi : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W X Y : C} {f : W ⟶ X} {h i : X ⟶ Y}
  [CategoryTheory.Epi f], CategoryTheory.CommSq f f h i → h = i
-- Mathlib.Logic.Equiv.Fin.Basic
isLeft_finSumNatEquiv_symm_apply : ∀ {n : ℕ} (i : ℕ), ((finSumNatEquiv n).symm i).isLeft = decide (i < n)
-- Mathlib.Data.ENNReal.Inv
ENNReal.inv_lt_iff_inv_lt : ∀ {a b : ENNReal}, a⁻¹ < b ↔ b⁻¹ < a
-- Mathlib.CategoryTheory.Limits.Presheaf
/-- This is a cocone with point `P` for the functor `functorToRepresentables P`. It is shown in
`colimitOfRepresentable P` that this cocone is a colimit: that is, we have exhibited an arbitrary
presheaf `P` as a colimit of representables.

The construction of [MM92], Chapter I, Section 5, Corollary 3.
 -/
CategoryTheory.Presheaf.coconeOfRepresentable : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (P : CategoryTheory.Functor Cᵒᵖ (Type (max w v₁))) →
      CategoryTheory.Limits.Cocone (CategoryTheory.Presheaf.functorToRepresentables P)
-- Mathlib.Data.Finset.Lattice.Fold
Finset.sup_mem : ∀ {α : Type u_2} [inst : SemilatticeSup α] [inst_1 : OrderBot α] (s : Set α),
  ⊥ ∈ s → (∀ x ∈ s, ∀ y ∈ s, x ⊔ y ∈ s) → ∀ {ι : Type u_7} (t : Finset ι) (p : ι → α), (∀ i ∈ t, p i ∈ s) → t.sup p ∈ s
-- Mathlib.CategoryTheory.FiberedCategory.BasedCategory
CategoryTheory.BasedCategory.mk.sizeOf_spec : ∀ {𝒮 : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : SizeOf 𝒮] (obj : Type u₂)
  (category : autoParam (CategoryTheory.Category.{v₂, u₂} obj) CategoryTheory.BasedCategory.category._autoParam)
  (p : CategoryTheory.Functor obj 𝒮),
  sizeOf { obj := obj, category := category, p := p } = 1 + sizeOf obj + sizeOf category + sizeOf p
-- Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries
QuadraticForm.comp_tensorLId_eq : ∀ {R : Type uR} {M₂ : Type uM₂} [inst : CommRing R] [inst_1 : AddCommGroup M₂] [inst_2 : Module R M₂]
  [inst_3 : Invertible 2] (Q₂ : QuadraticForm R M₂),
  QuadraticMap.comp Q₂ ↑(TensorProduct.lid R M₂) = QuadraticForm.tmul QuadraticMap.sq Q₂
-- Mathlib.GroupTheory.FreeGroup.Reduce
FreeAddGroup.isReduced_toWord : ∀ {α : Type u_1} [inst : DecidableEq α] {x : FreeAddGroup α}, FreeAddGroup.IsReduced x.toWord
-- Mathlib.Dynamics.SymbolicDynamics.Basic
SymbolicDynamics.FullShift.shift_zero : ∀ {A : Type u_1} {G : Type u_2} [inst : AddMonoid G] (x : G → A), SymbolicDynamics.FullShift.shift 0 x = x
-- Mathlib.Order.Hom.WithTopBot
/-- Adjoins a `⊤` to the domain of a `SupHom`.  -/
SupHom.withTop' : {α : Type u_1} →
  {β : Type u_2} →
    [inst : SemilatticeSup α] → [inst_1 : SemilatticeSup β] → [OrderTop β] → SupHom α β → SupHom (WithTop α) β
-- Mathlib.CategoryTheory.Bicategory.LocallyGroupoid
/-- The hom direction of the (strong) natural isomorphism of pseudofunctors
between `(pseudofunctorToPith F).comp (inclusion B)` and `F`.  -/
CategoryTheory.Bicategory.Pith.pseudofunctorToPithCompInclusionStrongIsoHom : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {B' : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory B'] →
        [inst_2 : CategoryTheory.Bicategory.IsLocallyGroupoid B'] →
          (F : CategoryTheory.Pseudofunctor B' B) →
            ((CategoryTheory.Bicategory.Pith.pseudofunctorToPith F).comp
                  (CategoryTheory.Bicategory.Pith.inclusion B)).StrongTrans
              F
-- Init.Data.Int.DivMod.Lemmas
Int.add_emod_eq_add_emod_left : ∀ {m n k : ℤ} (i : ℤ), m % n = k % n → (i + m) % n = (i + k) % n
-- Mathlib.GroupTheory.Generators
/-- The generating family obtained using a generating set `S : Set G`.  -/
Group.Generators.ofSet : {G : Type u_1} → [inst : Group G] → {S : Set G} → Subgroup.closure S = ⊤ → Group.Generators G ↑S
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero
/-- The augmentation map `X.homology R 0 ⟶ R`.  -/
SSet.homology₀ε : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasCoproducts C] →
      [inst_2 : CategoryTheory.Preadditive C] →
        (X : SSet) → (R : C) → [inst_3 : CategoryTheory.CategoryWithHomology C] → X.homology R 0 ⟶ R
-- Mathlib.CategoryTheory.GradedObject.Monoidal
CategoryTheory.GradedObject.Monoidal.ιTensorObj₃'_eq_assoc : ∀ {I : Type u} [inst : AddMonoid I] {C : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} C]
  [inst_2 : CategoryTheory.MonoidalCategory C] (X₁ X₂ X₃ : CategoryTheory.GradedObject I C) [inst_3 : X₁.HasTensor X₂]
  [inst_4 : (CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂).HasTensor X₃] (i₁ i₂ i₃ j : I) (h : i₁ + i₂ + i₃ = j)
  (i₁₂ : I) (h' : i₁ + i₂ = i₁₂) {Z : C}
  (h_1 :
    CategoryTheory.GradedObject.Monoidal.tensorObj (CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂) X₃ j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.ιTensorObj₃' X₁ X₂ X₃ i₁ i₂ i₃ j h) h_1 =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight
        (CategoryTheory.GradedObject.Monoidal.ιTensorObj X₁ X₂ i₁ i₂ i₁₂ h') (X₃ i₃))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.GradedObject.Monoidal.ιTensorObj (CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂) X₃ i₁₂
          i₃ j ⋯)
        h_1)
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
Measurable.prod : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ}
  {f : α → β × γ}, (Measurable fun a => (f a).1) → (Measurable fun a => (f a).2) → Measurable f
-- Mathlib.Combinatorics.SimpleGraph.Extremal.ErdosStoneSimonovits
/-- For `w ∈ ErdosStone.filter`, there exists a `r` subets of vertices of size `t < t'`
adjacent to `w`.

This is an auxiliary definition for the Erdős-Stone theorem.  -/
_private.Mathlib.Combinatorics.SimpleGraph.Extremal.ErdosStoneSimonovits.0.SimpleGraph.ErdosStone.filter.pi : {n : ℕ} →
  {G : SimpleGraph (Fin n)} →
    [inst : DecidableRel G.Adj] →
      {r t t' : ℕ} →
        (K : G.CompleteEquipartiteSubgraph r t') →
          ↥(SimpleGraph.ErdosStone.filter✝ K t) → ↥(K.parts.pi fun x => Finset.powersetCard t x)
-- Mathlib.FieldTheory.KummerPolynomial
root_X_pow_sub_C_eq_zero_iff : ∀ {K : Type u} [inst : Field K] {n : ℕ} {a : K},
  Irreducible (Polynomial.X ^ n - Polynomial.C a) → (AdjoinRoot.root (Polynomial.X ^ n - Polynomial.C a) = 0 ↔ a = 0)
-- Mathlib.Analysis.Normed.Field.Basic
NormedField.exists_one_lt_enorm : ∀ (α : Type u_2) [inst : NontriviallyNormedField α], ∃ x, 1 < ‖x‖ₑ
-- Mathlib.Topology.Category.TopCat.Opens
Topology.IsInducing.functor_obj : ∀ {X Y : TopCat} {f : X ⟶ Y} (hf : Topology.IsInducing ⇑(CategoryTheory.ConcreteCategory.hom f))
  (U : TopologicalSpace.Opens ↑X), hf.functor.obj U = hf.functorObj U
-- Init.Data.Bool
Bool.eq_not_self : ∀ (b : Bool), b = !b ↔ False
-- Mathlib.Probability.Independence.Kernel.Indep
ProbabilityTheory.Kernel.iIndepSet_congr : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω}
  {κ η : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {s : ι → Set Ω},
  ⇑κ =ᵐ[μ] ⇑η → (ProbabilityTheory.Kernel.iIndepSet s κ μ ↔ ProbabilityTheory.Kernel.iIndepSet s η μ)
-- Mathlib.CategoryTheory.NatTrans
CategoryTheory.NatTrans.instInhabited : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C D) → Inhabited (CategoryTheory.NatTrans F F)
-- Lean.PrettyPrinter.Delaborator.Builtins
Lean.PrettyPrinter.Delaborator.delabMVar : Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
HasFTaylorSeriesUpToOn.congr_series : ∀ {𝕜 : 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 q : E → FormalMultilinearSeries 𝕜 E F},
  HasFTaylorSeriesUpToOn n f p s →
    (∀ (m : ℕ), ↑m ≤ n → Set.EqOn (fun x => p x m) (fun x => q x m) s) → HasFTaylorSeriesUpToOn n f q s
-- Mathlib.CategoryTheory.Monoidal.Opposite
/-- The (identity) equivalence between `Cᴹᵒᵖ` and `C`.  -/
CategoryTheory.MonoidalOpposite.unmopEquiv : (C : Type u₁) → [inst : CategoryTheory.Category.{v₁, u₁} C] → Cᴹᵒᵖ ≌ C
-- Mathlib.CategoryTheory.Limits.Opposites
/-- The limit of `F.op` is the opposite of `colimit F`.  -/
CategoryTheory.Limits.limitOpIsoOpColimit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} J] →
        (F : CategoryTheory.Functor J C) →
          [inst_2 : CategoryTheory.Limits.HasColimit F] →
            CategoryTheory.Limits.limit F.op ≅ Opposite.op (CategoryTheory.Limits.colimit F)
-- Mathlib.Combinatorics.Matroid.Basic
/-- **Alias** of `Matroid.IsBase.sdiff_finite_comm`. -/
Matroid.IsBase.diff_finite_comm : ∀ {α : Type u_1} {M : Matroid α} {B₁ B₂ : Set α}, M.IsBase B₁ → M.IsBase B₂ → ((B₁ \ B₂).Finite ↔ (B₂ \ B₁).Finite)
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.get?_mem : ∀ {α : Type u} {s : Stream'.WSeq α} {a : α} {n : ℕ}, some a ∈ s.get? n → a ∈ s
-- Mathlib.Analysis.Convex.Function
strictConvexOn_iff_div : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommMonoid E] [inst_4 : AddCommMonoid β] [inst_5 : PartialOrder β] [inst_6 : SMul 𝕜 E]
  [inst_7 : SMul 𝕜 β] {s : Set E} {f : E → β},
  StrictConvexOn 𝕜 s f ↔
    Convex 𝕜 s ∧
      ∀ ⦃x : E⦄,
        x ∈ s →
          ∀ ⦃y : E⦄,
            y ∈ s →
              x ≠ y →
                ∀ ⦃a b : 𝕜⦄,
                  0 < a → 0 < b → f ((a / (a + b)) • x + (b / (a + b)) • y) < (a / (a + b)) • f x + (b / (a + b)) • f y
-- ProofWidgets.Component.HtmlDisplay
ProofWidgets.instRpcEncodableHtmlDisplayProps : Lean.Server.RpcEncodable ProofWidgets.HtmlDisplayProps
-- Batteries.Data.BinomialHeap.Basic
Batteries.BinomialHeap.Imp.HeapNode.rankTR.go.eq_def : ∀ {α : Type u_1} (a : Batteries.BinomialHeap.Imp.HeapNode α) (a_1 : ℕ),
  Batteries.BinomialHeap.Imp.HeapNode.rankTR.go a a_1 =
    match a, a_1 with
    | Batteries.BinomialHeap.Imp.HeapNode.nil, r => r
    | Batteries.BinomialHeap.Imp.HeapNode.node a child s, r => Batteries.BinomialHeap.Imp.HeapNode.rankTR.go s (r + 1)
-- Mathlib.MeasureTheory.Constructions.Cylinders
/-- Given a finite set `s` of indices, a cylinder is the preimage of a set `S` of `∀ i : s, α i` by
the projection from `∀ i, α i` to `∀ i : s, α i`.  -/
MeasureTheory.cylinder : {ι : Type u_1} → {α : ι → Type u_2} → (s : Finset ι) → Set ((i : ↥s) → α ↑i) → Set ((i : ι) → α i)
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
MeasureTheory.StronglyMeasurable.oneLePart : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace β] [inst_2 : Group β]
  [inst_3 : Lattice β] [ContinuousSup β],
  MeasureTheory.StronglyMeasurable f → MeasureTheory.StronglyMeasurable fun x => (f x)⁺ᵐ
-- Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
/-- `IsClosedUnderFiniteProducts` may be checked at any universe.  -/
CategoryTheory.ObjectProperty.IsClosedUnderFiniteProducts.of_isClosedUnderLimitsOfShape : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P : CategoryTheory.ObjectProperty C},
  (∀ (J : Type w) [Finite J], P.IsClosedUnderLimitsOfShape (CategoryTheory.Discrete J)) → P.IsClosedUnderFiniteProducts
-- Mathlib.RingTheory.Localization.FractionRing
FaithfulSMul.of_field_isFractionRing : ∀ (R : Type u_1) [inst : CommRing R] (S : Type u_2) [inst_1 : CommRing S] [inst_2 : Algebra R S] (K : Type u_6)
  (L : Type u_7) [inst_3 : Field K] [inst_4 : Semiring L] [Nontrivial L] [inst_6 : Algebra R K] [IsFractionRing R K]
  [inst_8 : Algebra S L] [inst_9 : Algebra K L] [inst_10 : Algebra R L] [IsScalarTower R S L] [IsScalarTower R K L],
  FaithfulSMul R S
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.BoundedFormula.toFormula.eq_4 : ∀ {L : FirstOrder.Language} {α : Type u'} (x : ℕ) (f₁ f₂ : L.BoundedFormula α x),
  (f₁.imp f₂).toFormula = FirstOrder.Language.BoundedFormula.imp f₁.toFormula f₂.toFormula
-- Mathlib.Logic.Function.Basic
Function.swap_lt : ∀ {α : Type u_4} [inst : LT α], (Function.swap fun x1 x2 => x1 < x2) = fun x1 x2 => x1 > x2
-- Mathlib.Algebra.Free
Magma.AssocQuotient.quot_mk_assoc : ∀ {α : Type u} [inst : Mul α] (x y z : α),
  Quot.mk (Magma.AssocRel α) (x * y * z) = Quot.mk (Magma.AssocRel α) (x * (y * z))
-- Mathlib.Data.TypeVec
TypeVec.diagSub.eq_2 : ∀ (n_2 : ℕ) (α_2 : TypeVec.{u} (n_2 + 1)) (x_2 : α_2 Fin2.fz), TypeVec.diagSub Fin2.fz x_2 = ⟨(x_2, x_2), ⋯⟩
-- Mathlib.MeasureTheory.Measure.Haar.Unique
/-- Two left invariant measures give the same mass to level sets of continuous compactly supported
functions, up to the scalar `addHaarScalarFactor μ' μ`.

Auxiliary lemma in the proof of the more general
`measure_isAddInvariant_eq_smul_of_isCompact_closure`, which works for any set with
compact closure.  -/
MeasureTheory.Measure.measure_preimage_isAddLeftInvariant_eq_smul_of_hasCompactSupport : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [inst_2 : IsTopologicalAddGroup G]
  [inst_3 : MeasurableSpace G] [inst_4 : BorelSpace G] (μ' μ : MeasureTheory.Measure G) [inst_5 : μ.IsAddHaarMeasure]
  [inst_6 : MeasureTheory.IsFiniteMeasureOnCompacts μ'] [inst_7 : μ'.IsAddLeftInvariant] {f : G → ℝ},
  Continuous f → HasCompactSupport f → μ' (f ⁻¹' {1}) = μ'.addHaarScalarFactor μ • μ (f ⁻¹' {1})
-- Mathlib.Algebra.Homology.ExactSequenceFour
CategoryTheory.ComposableArrows.IsComplex.epi_cokerToKer' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {n : ℕ}
  {S : CategoryTheory.ComposableArrows C (n + 3)} (hS : S.IsComplex) (k : ℕ) (hk : k ≤ n)
  (cc : CategoryTheory.Limits.CokernelCofork (S.map' k (k + 1) ⋯ ⋯))
  (kf : CategoryTheory.Limits.KernelFork (S.map' (k + 2) (k + 3) ⋯ ⋯)) (hcc : CategoryTheory.Limits.IsColimit cc)
  (hkf : CategoryTheory.Limits.IsLimit kf),
  (S.sc hS (k + 1) ⋯).Exact → CategoryTheory.Epi (hS.cokerToKer' k hk cc kf hcc hkf)
-- Mathlib.CategoryTheory.Limits.Types.Coproducts
/-- The cofan given by a sigma type.  -/
CategoryTheory.Limits.CofanTypes.sigma : {C : Type u} → (F : C → Type v) → CategoryTheory.Limits.CofanTypes F
-- Mathlib.RingTheory.Localization.Basic
IsLocalization.algEquivOfAlgEquiv_symm : ∀ {A : Type u_4} [inst : CommSemiring A] {R : Type u_5} [inst_1 : CommSemiring R] [inst_2 : Algebra A R]
  {M : Submonoid R} {S : Type u_6} [inst_3 : CommSemiring S] [inst_4 : Algebra A S] [inst_5 : Algebra R S]
  [inst_6 : IsScalarTower A R S] [inst_7 : IsLocalization M S] {P : Type u_7} [inst_8 : CommSemiring P]
  [inst_9 : Algebra A P] {T : Submonoid P} {Q : Type u_8} [inst_10 : CommSemiring Q] [inst_11 : Algebra A Q]
  [inst_12 : Algebra P Q] [inst_13 : IsScalarTower A P Q] [inst_14 : IsLocalization T Q] {h : R ≃ₐ[A] P}
  (H : Submonoid.map h M = T),
  (IsLocalization.algEquivOfAlgEquiv S Q h H).symm = IsLocalization.algEquivOfAlgEquiv Q S h.symm ⋯
-- Mathlib.RingTheory.Extension.Cotangent.Basic
Algebra.Generators.toKaehler_tmul_D : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {ι : Type w}
  {P : Algebra.Generators R S ι} (i : ι),
  P.toExtension.toKaehler (1 ⊗ₜ[P.toExtension.Ring] (KaehlerDifferential.D R P.Ring) (MvPolynomial.X i)) =
    (KaehlerDifferential.D R S) (P.val i)
-- Mathlib.LinearAlgebra.Matrix.Vec
/-- Technical lemma shared with `vec_vecMul_kronecker` and `vec_mul_eq_vecMul`.  -/
Matrix.vec_vecMul_kronecker_of_commute : ∀ {l : Type u_2} {m : Type u_1} {n : Type u_4} {p : Type u_5} {R : Type u_3} [inst : NonUnitalSemiring R]
  [inst_1 : Fintype m] [inst_2 : Fintype n] (A : Matrix m l R) (X : Matrix m n R) (B : Matrix n p R),
  (∀ (x : R) (i : m) (j : l), Commute (A i j) x) →
    Matrix.vecMul X.vec (Matrix.kroneckerMap (fun x1 x2 => x1 * x2) B A) = (A.transpose * X * B).vec
-- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
MeasureTheory.lintegral_indicator_one : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α},
  MeasurableSet s → ∫⁻ (a : α), s.indicator 1 a ∂μ = μ s
-- Mathlib.Data.NNReal.Defs
NNReal.le_inv_iff_mul_le : ∀ {r p : NNReal}, p ≠ 0 → (r ≤ p⁻¹ ↔ r * p ≤ 1)
-- Mathlib.AlgebraicGeometry.Cover.QuasiCompact
/-- The object property on the category of pre-`0`-hypercovers of a scheme given
by quasi-compact covers.  -/
AlgebraicGeometry.Scheme.quasiCompactCover : (S : AlgebraicGeometry.Scheme) → CategoryTheory.ObjectProperty (CategoryTheory.PreZeroHypercover S)