mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.NonUnitalSubsemiring.Defs
/-- This lemma exists for `aesop`, as `aesop` simplifies `x * -y` to `-(x * y)` before applying
unsafe rules like `mul_mem`, leading to a dead end in cases where `neg_mem` does not hold.  -/
mul_neg_mem : ∀ {R : Type u_1} {S : Type u_2} [inst : Mul R] [inst_1 : HasDistribNeg R] [inst_2 : SetLike S R] [MulMemClass S R]
  {s : S} {x y : R}, x ∈ s → -y ∈ s → -(x * y) ∈ s
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Iic_union_Ici : ∀ {α : Type u_1} [inst : LinearOrder α] {a : α}, Set.Iic a ∪ Set.Ici a = Set.univ
-- Mathlib.Algebra.Group.Submonoid.Units
Subgroup.ofUnits_bot : ∀ {M : Type u_1} [inst : Monoid M], ⊥.ofUnits = ⊥
-- Mathlib.Analysis.Complex.ExponentialBounds
Real.exp_neg_one_lt_d9 : Real.exp (-1) < 0.3678794412
-- Std.Time.Date.Unit.Month
/-- Creates an `Ordinal` from a `Nat`, ensuring the value is within bounds.
 -/
Std.Time.Month.Ordinal.ofNat : (data : ℕ) → autoParam (data ≥ 1 ∧ data ≤ 12) Std.Time.Month.Ordinal.ofNat._auto_1 → Std.Time.Month.Ordinal
-- Mathlib.Order.SupClosed
subset_supClosure : ∀ {α : Type u_3} [inst : SemilatticeSup α] {s : Set α}, s ⊆ supClosure s
-- Mathlib.Algebra.GroupWithZero.Indicator
Function.support_mul' : ∀ {ι : Type u_1} {M₀ : Type u_4} [inst : MulZeroClass M₀] [NoZeroDivisors M₀] (f g : ι → M₀),
  Function.support (f * g) = Function.support f ∩ Function.support g
-- Mathlib.Topology.Homotopy.Contractible
Homeomorph.contractibleSpace_iff : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : X ≃ₜ Y),
  ContractibleSpace X ↔ ContractibleSpace Y
-- Mathlib.Data.Fin.Basic
/-- A dependent variant of `Fin.elim0`.  -/
Fin.rec0 : {α : Fin 0 → Sort u_1} → (i : Fin 0) → α i
-- Init.Data.Iterators.Producers.Monadic.List
_private.Init.Data.Iterators.Producers.Monadic.List.0.Std.Iterators.Types.ListIterator.instIterator.match_1.eq_2 : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} (motive : Std.IterStep (Std.IterM m α) α → Sort u_3) (it : Std.IterM m α)
  (h_1 : (it' : Std.IterM m α) → (out : α) → motive (Std.IterStep.yield it' out))
  (h_2 : (it : Std.IterM m α) → motive (Std.IterStep.skip it)) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.skip it with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it => h_2 it
    | Std.IterStep.done => h_3 ()) =
    h_2 it
-- Lean.Server.Requests
Lean.Server.instInhabitedRequestError.default : Lean.Server.RequestError
-- Mathlib.AlgebraicGeometry.Morphisms.Basic
AlgebraicGeometry.IsZariskiLocalAtSource.of_iSup_eq_top : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsZariskiLocalAtSource P]
  {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} {ι : Sort u_1} (U : ι → X.Opens),
  iSup U = ⊤ → (∀ (i : ι), P (CategoryTheory.CategoryStruct.comp (U i).ι f)) → P f
-- Mathlib.FieldTheory.Galois.IsGaloisGroup
/-- If `G` acts as a Galois group on `L/K` and the subgroup `H` acts as a Galois group on `L/B`,
then the fixed points of `H` equals the range of `algebraMap B L`.  -/
IsGaloisGroup.fixedPoints_eq_range_algebraMap : ∀ (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] (H : Subgroup G) [hGKL : IsGaloisGroup G K L] (B : Type u_5)
  [inst_5 : CommSemiring B] [inst_6 : Algebra B L] [IsGaloisGroup (↥H) B L],
  ↑(FixedPoints.intermediateField ↥H) = Set.range ⇑(algebraMap B L)
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.map_comap_map : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] (S : AddSubmonoid M) {F : Type u_4}
  [inst_2 : FunLike F M N] [mc : AddMonoidHomClass F M N] {f : F},
  AddSubmonoid.map f (AddSubmonoid.comap f (AddSubmonoid.map f S)) = AddSubmonoid.map f S
-- Init.Data.List.SplitOn.Lemmas
List.splitOnP_cons_eq_if_modifyHead : ∀ {α : Type u_1} {p : α → Bool} (x : α) (xs : List α),
  List.splitOnP p (x :: xs) =
    if p x = true then [] :: List.splitOnP p xs else List.modifyHead (List.cons x) (List.splitOnP p xs)
-- Mathlib.Algebra.Group.Center
/-- associative property for left multiplication  -/
IsMulCentral.left_assoc : ∀ {M : Type u_1} [inst : Mul M] {z : M}, IsMulCentral z → ∀ (b c : M), z * (b * c) = z * b * c
-- Mathlib.Order.Partition.Finpartition
Finpartition.parts_subset_extendOfLE : ∀ {α : Type u_1} [inst : GeneralizedBooleanAlgebra α] [inst_1 : DecidableEq α] {a b : α} (P : Finpartition a)
  (hab : a ≤ b), P.parts ⊆ (P.extendOfLE hab).parts
-- Mathlib.Algebra.Quaternion
/-- `QuaternionAlgebra.imI` as a `LinearMap`  -/
QuaternionAlgebra.imIₗ : {R : Type u_3} → (c₁ c₂ c₃ : R) → [inst : CommRing R] → QuaternionAlgebra R c₁ c₂ c₃ →ₗ[R] R
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.Measure.measure_inv : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : InvolutiveInv G] [MeasurableInv G] (μ : MeasureTheory.Measure G)
  [μ.IsInvInvariant] (A : Set G), μ A⁻¹ = μ A
-- Mathlib.Order.Filter.Extr
Filter.EventuallyLE.isMinFilter : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder β] {f g : α → β} {a : α} {l : Filter α},
  f ≤ᶠ[l] g → f a = g a → IsMinFilter f l a → IsMinFilter g l a
-- Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
RestrictedProduct.instT2Space : ∀ {ι : Type u_1} {R : ι → Type u_2} {A : (i : ι) → Set (R i)} {𝓕 : Filter ι} [inst : (i : ι) → TopologicalSpace (R i)]
  [∀ (i : ι), T2Space (R i)], T2Space (RestrictedProduct (fun i => R i) (fun i => A i) 𝓕)
-- Mathlib.Order.WellFounded
WellFounded.isWellOrder_iff_exists_not_lt_and_eq_or_gt : ∀ {α : Type u_1} {r : α → α → Prop},
  IsWellOrder α r ↔ ∀ (s : Set α), s.Nonempty → ∃ m ∈ s, ∀ x ∈ s, ¬r x m ∧ (m = x ∨ r m x)
-- Mathlib.Analysis.Normed.Group.Hom
/-- The equalizer of two morphisms `f g : NormedAddGroupHom V W`.  -/
NormedAddGroupHom.equalizer : {V : Type u_1} →
  {W : Type u_2} →
    [inst : SeminormedAddCommGroup V] →
      [inst_1 : SeminormedAddCommGroup W] → NormedAddGroupHom V W → NormedAddGroupHom V W → AddSubgroup V
-- Init.Data.UInt.Lemmas
UInt64.lt_iff_toBitVec_lt : ∀ {a b : UInt64}, a < b ↔ a.toBitVec < b.toBitVec
-- Lean.Meta.Basic
Lean.Meta.DefEqCacheKey : Type
-- Mathlib.SetTheory.Ordinal.Topology
Ordinal.nhds_eq_pure : ∀ {a : Ordinal.{u}}, nhds a = pure a ↔ ¬Order.IsSuccLimit a
-- Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
_private.Mathlib.MeasureTheory.Function.SimpleFuncDenseLp.0.MeasureTheory.«term_→ₛ_» : Lean.TrailingParserDescr
-- Mathlib.RingTheory.Finiteness.Cardinality
/-- The kernel of a random surjective linear map from a finite free module
to a given finite module.  -/
Module.Finite.kerRepr : (R : Type u) →
  (M : Type u_1) →
    [inst : Ring R] →
      [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → [inst_3 : Module.Finite R M] → Submodule R (Fin ⋯.choose → R)
-- Mathlib.Combinatorics.KatonaCircle
Numbering.dens_prefixed : ∀ {X : Type u_1} [inst : Fintype X] [inst_1 : DecidableEq X] (s : Finset X),
  (Numbering.prefixed s).dens = (↑((Fintype.card X).choose s.card))⁻¹
-- Mathlib.Algebra.Order.Group.Action.Synonym
Lex.instMulAction : {M : Type u_1} → {α : Type u_3} → [inst : Monoid M] → [MulAction M α] → MulAction (Lex M) α
-- Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting
CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct.map_f' : ∀ {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} {p : X ⟶ Y} {f : F.obj ⊥ ⟶ X}
  {g : c.pt ⟶ Y} {j : J} (sq' : CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct c p f g j) {j' : J}
  (α : j' ⟶ j), (sq'.map α).f' = CategoryTheory.CategoryStruct.comp (F.map α) sq'.f'
-- Mathlib.Algebra.Order.Monoid.Unbundled.Pow
pow_le_pow_right' : ∀ {M : Type u_3} [inst : Monoid M] [inst_1 : Preorder M] [MulLeftMono M] {a : M} {n m : ℕ},
  1 ≤ a → n ≤ m → a ^ n ≤ a ^ m
-- Mathlib.CategoryTheory.Sites.Precoverage.Subsheaf
/-- If `F` is a sheaf for `R` and `R ∈ K X`, then the `K`-sheafification of `𝒮` is a
sheaf for `R`.  -/
CategoryTheory.Precoverage.isSheafFor_subsheafify : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {K : CategoryTheory.Precoverage C}
  {F : CategoryTheory.Functor Cᵒᵖ (Type w)} (𝒮 : (Z : C) → Set (F.obj (Opposite.op Z))) {X : C}
  {R : CategoryTheory.Presieve X},
  R ∈ K.coverings X →
    CategoryTheory.Presieve.IsSheafFor F R → CategoryTheory.Presieve.IsSheafFor (K.subsheafify 𝒮).toFunctor R
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.equivProd_unitIso_inv_app_left : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  (L : CategoryTheory.Functor A (CategoryTheory.Discrete PUnit.{u_1 + 1}))
  (R : CategoryTheory.Functor B (CategoryTheory.Discrete PUnit.{u_1 + 1})) (X : CategoryTheory.Comma L R),
  ((CategoryTheory.Comma.equivProd L R).unitIso.inv.app X).left = CategoryTheory.CategoryStruct.id X.left
-- Mathlib.Order.Atoms
Set.Ici.isAtom_iff : ∀ {α : Type u_2} [inst : PartialOrder α] {a : α} {b : ↑(Set.Ici a)}, IsAtom b ↔ a ⋖ ↑b
-- Batteries.Recycling.RBTree.Basic
/-- Rebalancing a tree which has shrunk on the left.  -/
RBTree.RBNode.balLeft : {α : Type u_1} → RBTree.RBNode α → α → RBTree.RBNode α → RBTree.RBNode α
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenNormalSubgroup.instSemilatticeSupOpenNormalSubgroup : {G : Type u} →
  [inst : Group G] → [inst_1 : TopologicalSpace G] → [SeparatelyContinuousMul G] → SemilatticeSup (OpenNormalSubgroup G)
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
CochainComplex.HomComplex.Cochain.leftShift_rightShift : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} {n : ℤ} (γ : CochainComplex.HomComplex.Cochain K L n) (a n' : ℤ) (hn' : n' + a = n),
  (γ.rightShift a n' hn').leftShift a n hn' = (a * n + a * (a - 1) / 2).negOnePow • γ.shift a
-- Mathlib.LinearAlgebra.Matrix.Bilinear
mulRightLinearMap_apply : ∀ (l : Type u_1) {m : Type u_2} {n : Type u_3} (R : Type u_5) {A : Type u_6} [inst : Fintype m] [inst_1 : Semiring R]
  [inst_2 : NonUnitalNonAssocSemiring A] [inst_3 : Module R A] [inst_4 : IsScalarTower R A A] (Y : Matrix m n A)
  (x : Matrix l m A), (mulRightLinearMap l R Y) x = x * Y
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.toStructuredArrow_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) (d : D) (X : (CategoryTheory.CostructuredArrow F d)ᵒᵖ),
  (CategoryTheory.CostructuredArrow.toStructuredArrow F d).obj X =
    CategoryTheory.StructuredArrow.mk (Opposite.unop X).hom.op
-- Mathlib.Data.ENNReal.Basic
ENNReal.one_lt_two : 1 < 2
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
_private.Mathlib.CategoryTheory.Limits.Shapes.Reflexive.0.CategoryTheory.Limits.WalkingParallelPair.inclusionWalkingReflexivePair.match_1.splitter : (motive : CategoryTheory.Limits.WalkingParallelPair → Sort u_1) →
  (x : CategoryTheory.Limits.WalkingParallelPair) →
    (Unit → motive CategoryTheory.Limits.WalkingParallelPair.one) →
      (Unit → motive CategoryTheory.Limits.WalkingParallelPair.zero) → motive x
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LongExactSequence
/-- Exactness of `Hⁱ(G, X₁) ⟶ Hⁱ(G, X₂) ⟶ Hⁱ(G, X₃)`.  -/
groupCohomology.mapShortComplex₂_exact : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {X : CategoryTheory.ShortComplex (Rep.{u, u, u} k G)},
  X.ShortExact → ∀ (i : ℕ), (groupCohomology.mapShortComplex₂ X i).Exact
-- Mathlib.Analysis.Normed.Group.Constructions
IsGreatest.pi_norm : ∀ {ι : Type u_1} {E : Type u_2} [inst : Fintype ι] [inst_1 : SeminormedAddGroup E] [Nonempty ι] (f : ι → E),
  IsGreatest (Set.range fun x => ‖f x‖) ‖f‖
-- Init.Data.Nat.Div.Basic
_private.Init.Data.Nat.Div.Basic.0.Nat.mod.match_1.splitter : (motive : ℕ → ℕ → Sort u_1) → (x x_1 : ℕ) → ((x : ℕ) → motive 0 x) → ((n m : ℕ) → motive n.succ m) → motive x x_1
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.size_insertIfNew_le : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {v : β}, (m.insertIfNew k v).size ≤ m.size + 1
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.getEntryLT?.go.eq_def : ∀ {α : Type u} {β : Type v} [inst : Ord α] (k : α) (best : Option (α × β))
  (a : Std.DTreeMap.Internal.Impl α fun x => β),
  Std.DTreeMap.Internal.Impl.Const.getEntryLT?.go k best a =
    match a with
    | Std.DTreeMap.Internal.Impl.leaf => best
    | Std.DTreeMap.Internal.Impl.inner size ky y l r =>
      match compare k ky with
      | Ordering.gt => Std.DTreeMap.Internal.Impl.Const.getEntryLT?.go k (some (ky, y)) r
      | x => Std.DTreeMap.Internal.Impl.Const.getEntryLT?.go k best l
-- Lean.DocString.Parser
Lean.Doc.Parser.UnorderedListType.ofNat : ℕ → Lean.Doc.Parser.UnorderedListType
-- Mathlib.RingTheory.AdicCompletion.Basic
AdicCompletion.AdicCauchySequence.instSMulNat : {R : Type u_1} →
  [inst : CommRing R] →
    (I : Ideal R) →
      (M : Type u_4) →
        [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → SMul ℕ (AdicCompletion.AdicCauchySequence I M)
-- Init.Data.Array.Attach
Array.attachWith_eq_map_attach : ∀ {α : Type u_1} {xs : Array α} {P : α → Prop} {H : ∀ a ∈ xs, P a},
  xs.attachWith P H =
    Array.map
      (fun x =>
        match x with
        | ⟨x, h⟩ => ⟨x, ⋯⟩)
      xs.attach
-- Init.Data.List.Nat.Sublist
List.suffix_iff_eq_drop : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <:+ l₂ ↔ l₁ = List.drop (l₂.length - l₁.length) l₂
-- Mathlib.MeasureTheory.Measure.MeasureSpace
/-- **Continuity from above**:
the measure of the intersection of a monotone family of measurable sets
indexed by a type with countably generated `atBot` filter
is equal to the infimum of the measures.  -/
Monotone.measure_iInter : ∀ {α : Type u_1} {ι : Type u_5} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : Preorder ι]
  [IsCodirectedOrder ι] [Filter.atBot.IsCountablyGenerated] {s : ι → Set α},
  Monotone s → (∀ (i : ι), MeasureTheory.NullMeasurableSet (s i) μ) → (∃ i, μ (s i) ≠ ⊤) → μ (⋂ i, s i) = ⨅ i, μ (s i)
-- Mathlib.Data.Set.Lattice
/-- `⋃₀` and `𝒫` form a Galois connection.  -/
Set.sUnion_powerset_gc : ∀ {α : Type u_1}, GaloisConnection (fun x => ⋃₀ x) fun x => 𝒫 x
-- Init.Data.Int.Linear
_private.Init.Data.Int.Linear.0.Int.Internal.Linear.denote'_addConst_eq : ∀ (ctx : Int.Internal.Linear.Context) (p : Int.Internal.Linear.Poly) (a : ℤ),
  Int.Internal.Linear.Poly.denote' ctx (p.addConst a) = Int.Internal.Linear.Poly.denote ctx p + a
-- Mathlib.Algebra.Group.AddChar
AddChar.instDecidableEq : {A : Type u_1} → {M : Type u_3} → [inst : AddMonoid A] → [inst_1 : Monoid M] → DecidableEq (AddChar A M)
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.NonemptyCompacts.isPreconnected_Iic : ∀ {α : Type u_1} [inst : TopologicalSpace α] {K : TopologicalSpace.NonemptyCompacts α},
  IsPreconnected ↑K → IsPreconnected (Set.Iic K)
-- Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
CategoryTheory.FreeGroupoid.liftNatIso.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {G : Type u₁} [inst_1 : CategoryTheory.Groupoid G]
  (F₁ F₂ : CategoryTheory.Functor (CategoryTheory.FreeGroupoid C) G)
  (τ : (CategoryTheory.FreeGroupoid.of C).comp F₁ ≅ (CategoryTheory.FreeGroupoid.of C).comp F₂),
  CategoryTheory.FreeGroupoid.liftNatIso F₁ F₂ τ =
    CategoryTheory.Localization.liftNatIso (CategoryTheory.FreeGroupoid.of C) ⊤
      ((CategoryTheory.FreeGroupoid.of C).comp F₁) ((CategoryTheory.FreeGroupoid.of C).comp F₂) F₁ F₂ τ
-- Mathlib.CategoryTheory.Shift.SingleFunctors
CategoryTheory.SingleFunctors.Hom.ext_iff : ∀ {C : Type u_1} {D : Type u_2} {inst : CategoryTheory.Category.{v_1, u_1} C}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} D} {A : Type u_5} {inst_2 : AddMonoid A}
  {inst_3 : CategoryTheory.HasShift D A} {F G : CategoryTheory.SingleFunctors C D A} {x y : F.Hom G},
  x = y ↔ x.hom = y.hom
-- Mathlib.Topology.UniformSpace.Basic
UniformContinuous₂.bicompl : ∀ {α : Type ua} {β : Type ub} {γ : Type uc} {δ : Type ud} {δ' : Type u_2} [inst : UniformSpace α]
  [inst_1 : UniformSpace β] [inst_2 : UniformSpace γ] [inst_3 : UniformSpace δ] [inst_4 : UniformSpace δ']
  {f : α → β → γ} {ga : δ → α} {gb : δ' → β},
  UniformContinuous₂ f → UniformContinuous ga → UniformContinuous gb → UniformContinuous₂ (Function.bicompl f ga gb)
-- Lean.Elab.InfoTree.Types
/-- Header information for a node in `InfoTree`.  -/
Lean.Elab.Info : Type
-- Mathlib.Analysis.Convex.Function
StrictConvexOn.add_convexOn : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommMonoid β] [inst_4 : PartialOrder β] [IsOrderedCancelAddMonoid β] [inst_6 : SMul 𝕜 E]
  [inst_7 : DistribMulAction 𝕜 β] {s : Set E} {f g : E → β},
  StrictConvexOn 𝕜 s f → ConvexOn 𝕜 s g → StrictConvexOn 𝕜 s (f + g)
-- Mathlib.Combinatorics.Tiling.Tile
DiscreteTiling.PlacedTile.coe_smul : ∀ {G : Type u_1} {X : Type u_2} {ιₚ : Type u_3} [inst : Group G] [inst_1 : MulAction G X]
  {ps : DiscreteTiling.Protoset G X ιₚ} (g : G) (pt : DiscreteTiling.PlacedTile ps), ↑(g • pt) = g • ↑pt
-- Mathlib.CategoryTheory.Shift.Pullback
CategoryTheory.pullbackShiftIso.eq_1 : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] {A : Type u_2} {B : Type u_3} [inst_1 : AddMonoid A]
  [inst_2 : AddMonoid B] [inst_3 : CategoryTheory.HasShift C B] (φ : A →+ B) (a : A) (b : B) (h : b = φ a),
  CategoryTheory.pullbackShiftIso C φ a b h = CategoryTheory.eqToIso ⋯
-- Lean.Elab.Tactic.Omega.Frontend
Lean.Elab.Tactic.Omega.MetaProblem.mk : Lean.Elab.Tactic.Omega.Problem →
  List Lean.Expr → List Lean.Expr → Std.HashSet Lean.Expr → Lean.Elab.Tactic.Omega.MetaProblem
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackToBaseIsOpenImmersion : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : AlgebraicGeometry.PresheafedSpace C} (f : X ⟶ Z)
  [hf : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f] (g : Y ⟶ Z)
  [inst_1 : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion g],
  AlgebraicGeometry.PresheafedSpace.IsOpenImmersion
    (CategoryTheory.Limits.limit.π (CategoryTheory.Limits.cospan f g) CategoryTheory.Limits.WalkingCospan.one)
-- Mathlib.Analysis.Real.Sqrt
NNReal.sqrt_inv : ∀ (x : NNReal), NNReal.sqrt x⁻¹ = (NNReal.sqrt x)⁻¹
-- Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Ordinal.iSup_lt_of_lt_cof : ∀ {α : Type u} {f : α → Ordinal.{u}} {a : Ordinal.{u}}, Cardinal.mk α < a.cof → (∀ (i : α), f i < a) → ⨆ i, f i < a
-- Mathlib.Order.WithBot
WithBot.coe_le_iff : ∀ {α : Type u_1} {a : α} [inst : LE α] {x : WithBot α}, ↑a ≤ x ↔ ∃ b, x = ↑b ∧ a ≤ b
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.ofList_cons : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {k : α} {v : β} {tl : List (α × β)},
  Std.DHashMap.Const.ofList ((k, v) :: tl) = Std.DHashMap.Const.insertMany (∅.insert k v) tl
-- Mathlib.Order.Hom.Bounded
BoundedOrderHom.cancel_right : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  [inst_3 : BoundedOrder α] [inst_4 : BoundedOrder β] [inst_5 : BoundedOrder γ] {g₁ g₂ : BoundedOrderHom β γ}
  {f : BoundedOrderHom α β}, Function.Surjective ⇑f → (g₁.comp f = g₂.comp f ↔ g₁ = g₂)
-- Mathlib.GroupTheory.GroupAction.SubMulAction
smul_mem_fixedPoints_of_normal : ∀ {G : Type u_1} [inst : Group G] {α : Type u_2} [inst_1 : MulAction G α] {H : Subgroup G} [hH : H.Normal] (g : G)
  {a : α}, a ∈ MulAction.fixedPoints (↥H) α → g • a ∈ MulAction.fixedPoints (↥H) α
-- Mathlib.CategoryTheory.MorphismProperty.Comma
/-- The functor `P.Comma L₁ R Q W ⥤ P.Comma L₃ R Q W` induced by the composition of two natural
transformations `l : L₁ ⟶ L₂` and `l' : L₂ ⟶ L₃` is naturally isomorphic to the composition of the
two functors induced by these natural transformations.  -/
CategoryTheory.MorphismProperty.Comma.mapLeftComp : {A : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} A] →
    {B : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} B] →
        {T : Type u_3} →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} T] →
            (R : CategoryTheory.Functor B T) →
              {P : CategoryTheory.MorphismProperty T} →
                {Q : CategoryTheory.MorphismProperty A} →
                  {W : CategoryTheory.MorphismProperty B} →
                    [inst_3 : Q.IsMultiplicative] →
                      [inst_4 : W.IsMultiplicative] →
                        {L₁ L₂ L₃ : CategoryTheory.Functor A T} →
                          [Q.RespectsIso] →
                            [W.RespectsIso] →
                              (l : L₁ ⟶ L₂) →
                                (l' : L₂ ⟶ L₃) →
                                  (hl :
                                      ∀ (X : CategoryTheory.MorphismProperty.Comma L₂ R P Q W),
                                        P (CategoryTheory.CategoryStruct.comp (l.app X.left) X.hom)) →
                                    (hl' :
                                        ∀ (X : CategoryTheory.MorphismProperty.Comma L₃ R P Q W),
                                          P (CategoryTheory.CategoryStruct.comp (l'.app X.left) X.hom)) →
                                      (hll' :
                                          ∀ (X : CategoryTheory.MorphismProperty.Comma L₃ R P Q W),
                                            P
                                              (CategoryTheory.CategoryStruct.comp
                                                ((CategoryTheory.CategoryStruct.comp l l').app X.left) X.hom)) →
                                        CategoryTheory.MorphismProperty.Comma.mapLeft R
                                            (CategoryTheory.CategoryStruct.comp l l') hll' ≅
                                          (CategoryTheory.MorphismProperty.Comma.mapLeft R l' hl').comp
                                            (CategoryTheory.MorphismProperty.Comma.mapLeft R l hl)
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.Const.wf_insertManyIfNewUnit₀ : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α] {ρ : Type w} [inst_4 : ForIn Id ρ α]
  {m : Std.DHashMap.Raw α fun x => Unit} {h : 0 < m.buckets.size} {l : ρ},
  m.WF → (↑↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit ⟨m, h⟩ l)).WF
-- Mathlib.Algebra.Free
_private.Mathlib.Algebra.Free.0.FreeAddMagma.liftAux.match_1.eq_2 : ∀ {α : Type u_1} (motive : FreeAddMagma α → Sort u_2) (x y : FreeAddMagma α)
  (h_1 : (x : α) → motive (FreeAddMagma.of x)) (h_2 : (x y : FreeAddMagma α) → motive (x.add y)),
  (match x.add y with
    | FreeAddMagma.of x => h_1 x
    | x.add y => h_2 x y) =
    h_2 x y
-- Mathlib.Data.Num.Prime
/-- Primality predicate for a `Num`.  -/
Num.Prime : Num → Prop
-- Mathlib.NumberTheory.MulChar.Duality
/-- If `M` is a finite commutative monoid and `R` is a ring that has enough roots of unity,
then for each `a ≠ 1` in `M`, there exists a multiplicative character `χ : M → R` such that
`χ a ≠ 1`.  -/
MulChar.exists_apply_ne_one_of_hasEnoughRootsOfUnity : ∀ (M : Type u_1) (R : Type u_2) [inst : CommMonoid M] [inst_1 : CommRing R] [Finite M]
  [HasEnoughRootsOfUnity R (Monoid.exponent Mˣ)] [Nontrivial R] {a : M}, a ≠ 1 → ∃ χ, χ a ≠ 1
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal
PresheafOfModules.Monoidal.tensorObj_map_tmul : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat}
  {M₁ M₂ : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))} {X Y : Cᵒᵖ} (f : X ⟶ Y)
  (m₁ : ↑(M₁.obj X)) (m₂ : ↑(M₂.obj X)),
  (ModuleCat.Hom.hom ((PresheafOfModules.Monoidal.tensorObj M₁ M₂).map f)) (m₁ ⊗ₜ[↑(R.obj X)] m₂) =
    (CategoryTheory.ConcreteCategory.hom (M₁.map f)) m₁ ⊗ₜ[↑(R.obj Y)]
      (CategoryTheory.ConcreteCategory.hom (M₂.map f)) m₂
-- Mathlib.Order.Filter.Pointwise
/-- `Filter α` is an `AddCommMonoid` under pointwise operations if `α` is.  -/
Filter.addCommMonoid : {α : Type u_2} → [AddCommMonoid α] → AddCommMonoid (Filter α)