mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
HasMFDerivWithinAt.sub : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {s : Set M} {z : M} {f g : M → E'} {f' g' : TangentSpace I z →L[𝕜] E'},
  HasMFDerivAt[s] f z f' → HasMFDerivAt[s] g z g' → HasMFDerivAt[s] (f - g) z (f' - g')
-- Mathlib.SetTheory.Ordinal.Enum
_private.Mathlib.SetTheory.Ordinal.Enum.0.Ordinal.enumOrd_mem_aux : ∀ {s : Set Ordinal.{u}},
  ¬BddAbove s → ∀ (o : Ordinal.{u}), Ordinal.enumOrd s o ∈ s ∩ {b | ∀ c < o, Ordinal.enumOrd s c < b}
-- Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
MDifferentiableAt.clm_prodMap : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F₁ : Type u_14} [inst_6 : NormedAddCommGroup F₁]
  [inst_7 : NormedSpace 𝕜 F₁] {F₂ : Type u_15} [inst_8 : NormedAddCommGroup F₂] [inst_9 : NormedSpace 𝕜 F₂]
  {F₃ : Type u_16} [inst_10 : NormedAddCommGroup F₃] [inst_11 : NormedSpace 𝕜 F₃] {F₄ : Type u_17}
  [inst_12 : NormedAddCommGroup F₄] [inst_13 : NormedSpace 𝕜 F₄] {g : M → F₁ →L[𝕜] F₃} {f : M → F₂ →L[𝕜] F₄} {x : M},
  MDiffAt g x → MDiffAt f x → (MDiffAt fun x => (g x).prodMap (f x)) x
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Real.lt_arcsin_iff_sin_lt' : ∀ {x y : ℝ}, x ∈ Set.Ico (-(Real.pi / 2)) (Real.pi / 2) → (x < Real.arcsin y ↔ Real.sin x < y)
-- Mathlib.Order.Heyting.Basic
compl_sup_le_himp : ∀ {α : Type u_2} [inst : HeytingAlgebra α] {a b : α}, aᶜ ⊔ b ≤ a ⇨ b
-- Mathlib.CategoryTheory.Category.Pairwise
CategoryTheory.Pairwise.pairwiseInhabited : {ι : Type v} → [Inhabited ι] → Inhabited (CategoryTheory.Pairwise ι)
-- Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Filter.IsMeasurablyGenerated.exists_measurable_subset : ∀ {α : Type u_1} {inst : MeasurableSpace α} {f : Filter α} [self : f.IsMeasurablyGenerated] ⦃s : Set α⦄,
  s ∈ f → ∃ t ∈ f, MeasurableSet t ∧ t ⊆ s
-- Batteries.Lean.LawfulMonad
instLawfulMonadST_batteries : ∀ {σ : Type}, LawfulMonad (ST σ)
-- Mathlib.Data.Nat.Factorization.Defs
Nat.factorization_zero_right : ∀ (n : ℕ), n.factorization 0 = 0
-- Mathlib.GroupTheory.GroupExtension.Defs
/-- The projection homomorphism `E →* G`  -/
GroupExtension.rightHom : {N : Type u_1} →
  {E : Type u_2} →
    {G : Type u_3} → [inst : Group N] → [inst_1 : Group E] → [inst_2 : Group G] → GroupExtension N E G → E →* G
-- Mathlib.Algebra.DirectSum.Basic
DirectSum.toAddMonoid.unique : ∀ {ι : Type v} {β : ι → Type w} [inst : (i : ι) → AddCommMonoid (β i)] [inst_1 : DecidableEq ι] {γ : Type u₁}
  [inst_2 : AddCommMonoid γ] (ψ : (DirectSum ι fun i => β i) →+ γ) (f : DirectSum ι fun i => β i),
  ψ f = (DirectSum.toAddMonoid fun i => ψ.comp (DirectSum.of β i)) f
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
CategoryTheory.MonoidalCategory.DayConvolution.unit_uniqueUpToIso_inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalCategory V]
  {F G : CategoryTheory.Functor C V} (h h' : CategoryTheory.MonoidalCategory.DayConvolution F G),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.DayConvolution.unit F G)
      ((CategoryTheory.MonoidalCategory.tensor C).whiskerLeft (h.uniqueUpToIso h').inv) =
    CategoryTheory.MonoidalCategory.DayConvolution.unit F G
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
WeierstrassCurve.Projective.polynomialX.eq_1 : ∀ {R : Type r} [inst : CommRing R] (W' : WeierstrassCurve.Projective R),
  W'.polynomialX = (MvPolynomial.pderiv 0) W'.polynomial
-- Mathlib.MeasureTheory.Covering.Besicovitch
Besicovitch.BallPackage.mk.inj : ∀ {β : Type u_1} {α : Type u_2} {c : β → α} {r : β → ℝ} {rpos : ∀ (b : β), 0 < r b} {r_bound : ℝ}
  {r_le : ∀ (b : β), r b ≤ r_bound} {c_1 : β → α} {r_1 : β → ℝ} {rpos_1 : ∀ (b : β), 0 < r_1 b} {r_bound_1 : ℝ}
  {r_le_1 : ∀ (b : β), r_1 b ≤ r_bound_1},
  { c := c, r := r, rpos := rpos, r_bound := r_bound, r_le := r_le } =
      { c := c_1, r := r_1, rpos := rpos_1, r_bound := r_bound_1, r_le := r_le_1 } →
    c = c_1 ∧ r = r_1 ∧ r_bound = r_bound_1
-- Mathlib.Data.Seq.Computation
Computation.lmap.eq_1 : ∀ {α : Type u} {β : Type v} {γ : Type w} (f : α → β) (a : α), Computation.lmap f (Sum.inl a) = Sum.inl (f a)
-- Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic
/-- If two functions differ only on a discrete set, then their proximity functions
agree, except perhaps at radius 0.
 -/
ValueDistribution.proximity_congr_codiscreteWithin : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {f g : ℂ → E} {a : WithTop E} {r : ℝ},
  f =ᶠ[Filter.codiscreteWithin (Metric.sphere 0 |r|)] g →
    r ≠ 0 → ValueDistribution.proximity f a r = ValueDistribution.proximity g a r
-- Lean.Meta.DiscrTree.Main
_private.Lean.Meta.DiscrTree.Main.0.Lean.Meta.DiscrTree.getMatchWithExtra.mayMatchPrefix : {α : Type} → Lean.Meta.DiscrTree α → Lean.Meta.DiscrTree.Key → Lean.MetaM Bool
-- Mathlib.Probability.Independence.Integration
/-- If `f` and `g` with values in `ℝ≥0∞` are independent and almost everywhere measurable,
then `E[f * g] = E[f] * E[g]` (slightly generalizing
`lintegral_mul_eq_lintegral_mul_lintegral_of_indepFun`).  -/
ProbabilityTheory.lintegral_mul_eq_lintegral_mul_lintegral_of_indepFun' : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {f g : Ω → ENNReal},
  AEMeasurable f μ →
    AEMeasurable g μ →
      ProbabilityTheory.IndepFun f g μ → ∫⁻ (ω : Ω), (f * g) ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), g ω ∂μ
-- Mathlib.Algebra.Ring.Prod
/-- Product of two `NonUnitalNonAssocSemiring`s is a `NonUnitalNonAssocSemiring`.  -/
Prod.instNonUnitalNonAssocSemiring : {R : Type u_1} →
  {S : Type u_3} → [NonUnitalNonAssocSemiring R] → [NonUnitalNonAssocSemiring S] → NonUnitalNonAssocSemiring (R × S)
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
ZeroAtInftyContinuousMap.instMul : {α : Type u} →
  {β : Type v} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] → [inst_2 : MulZeroClass β] → [ContinuousMul β] → Mul (ZeroAtInftyContinuousMap α β)
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.aleph0_lt_iff_aleph_one_le : ∀ {c : Cardinal.{u_1}}, Cardinal.aleph0 < c ↔ Cardinal.aleph 1 ≤ c
-- Mathlib.MeasureTheory.Measure.NullMeasurable
MeasureTheory.measure_preimage_fst_singleton_eq_sum : ∀ {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [MeasurableSingletonClass α] {mβ : MeasurableSpace β}
  [MeasurableSingletonClass β] [inst : Fintype β] (μ : MeasureTheory.Measure (α × β)) (x : α),
  μ (Prod.fst ⁻¹' {x}) = ∑ y, μ {(x, y)}
-- Mathlib.NumberTheory.Height.Basic
/-- The multiplicative height of a nonempty finite sum of field elements is at most
`n ^ (totalWeight K)` times the product of the individual multiplicative
heights, where `n` is the number of terms.  -/
Height.mulHeight₁_sum_le : ∀ {K : Type u_1} [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K] {α : Type u_2} {s : Finset α},
  s.Nonempty →
    ∀ (x : α → K), Height.mulHeight₁ (∑ a ∈ s, x a) ≤ ↑s.card ^ Height.totalWeight K * ∏ a ∈ s, Height.mulHeight₁ (x a)
-- Init.Data.Int.DivMod.Lemmas
Int.neg_bmod_self : ∀ {a : ℕ}, (-↑a).bmod a = 0
-- Init.Data.BitVec.Bitblast
BitVec.saddOverflow_eq : ∀ {w : ℕ} (x y : BitVec w), x.saddOverflow y = (x.msb == y.msb && !(x + y).msb == x.msb)
-- Mathlib.Logic.Function.FromTypes
Function.fromTypes_zero_equiv_apply : ∀ (p : Fin 0 → Type u) (τ : Type u) (a : Function.FromTypes p τ), (Function.fromTypes_zero_equiv p τ) a = a
-- Init.Data.Int.Linear
Int.Internal.Linear.cmod_nonpos : ∀ (a : ℤ) {b : ℤ}, b ≠ 0 → Int.Internal.Linear.cmod a b ≤ 0
-- Mathlib.Geometry.Manifold.Algebra.Monoid
contMDiffAt_finsum : ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_3}
  [inst_1 : TopologicalSpace H] {E : Type u_4} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E]
  {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [inst_4 : AddCommMonoid G] [inst_5 : TopologicalSpace G]
  [inst_6 : ChartedSpace H G] [ContMDiffAdd I n G] {E' : Type u_6} [inst_8 : NormedAddCommGroup E']
  [inst_9 : NormedSpace 𝕜 E'] {H' : Type u_7} [inst_10 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M : Type u_8} [inst_11 : TopologicalSpace M] [inst_12 : ChartedSpace H' M] {x₀ : M} {f : ι → M → G},
  (LocallyFinite fun i => Function.support (f i)) →
    (∀ (i : ι), ContMDiffAt I' I n (f i) x₀) → ContMDiffAt I' I n (fun x => ∑ᶠ (i : ι), f i x) x₀
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.sum_prodMkLeft : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} {ι : Type u_5} [inst : Countable ι] {κ : ι → ProbabilityTheory.Kernel α β},
  (ProbabilityTheory.Kernel.sum fun i => ProbabilityTheory.Kernel.prodMkLeft γ (κ i)) =
    ProbabilityTheory.Kernel.prodMkLeft γ (ProbabilityTheory.Kernel.sum κ)
-- Lean.Syntax
Lean.Syntax.rewriteBottomUp : (Lean.Syntax → Lean.Syntax) → Lean.Syntax → Lean.Syntax
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.EqCnstrProof.subst.injEq : ∀ (x : Lean.Grind.Linarith.Var) (c₁ c₂ : Lean.Meta.Grind.Arith.Linear.EqCnstr) (x_1 : Lean.Grind.Linarith.Var)
  (c₁_1 c₂_1 : Lean.Meta.Grind.Arith.Linear.EqCnstr),
  (Lean.Meta.Grind.Arith.Linear.EqCnstrProof.subst x c₁ c₂ =
      Lean.Meta.Grind.Arith.Linear.EqCnstrProof.subst x_1 c₁_1 c₂_1) =
    (x = x_1 ∧ c₁ = c₁_1 ∧ c₂ = c₂_1)
-- Mathlib.RingTheory.MvPowerSeries.Substitution
MvPowerSeries.rescale_zero_apply : ∀ {σ : Type u_1} {R : Type u_9} [inst : CommSemiring R] (f : MvPowerSeries σ R),
  (MvPowerSeries.rescale 0) f = MvPowerSeries.C (MvPowerSeries.constantCoeff f)
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenSubgroup.isOpen' : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] (self : OpenSubgroup G), IsOpen (↑self).carrier
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.ordered_keys_toArray : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t.WF → List.Pairwise (fun a b => compare a.1 b.1 = Ordering.lt) (Std.DTreeMap.Internal.Impl.Const.toArray t).toList
-- Mathlib.Topology.Algebra.Module.Complement
Submodule.quotientEquivOfIsTopCompl_apply : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] {p q : Submodule R M} [inst_4 : IsTopologicalAddGroup M] (h : Submodule.IsTopCompl p q)
  (x : M ⧸ p), (p.quotientEquivOfIsTopCompl q h) x = (p.quotientEquivOfIsCompl q ⋯) x
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.toOplax_mapComp' : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.Pseudofunctor B C) {b₀ b₁ b₂ : B} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (fg : b₀ ⟶ b₂)
  (h : autoParam (CategoryTheory.CategoryStruct.comp f g = fg) CategoryTheory.Pseudofunctor.toOplax_mapComp'._auto_1),
  F.toOplax.mapComp' f g fg h = (F.mapComp' f g fg h).hom
-- Mathlib.Order.CountableSupClosed
CountableSupClosed.finsetSup_mem : ∀ {α : Type u_2} {s : Set α} {ι : Type u_4} {f : ι → α} {t : Finset ι} [inst : SemilatticeSup α] [inst_1 : OrderBot α],
  CountableSupClosed s → t.Nonempty → (∀ i ∈ t, f i ∈ s) → t.sup f ∈ s
-- Init.Data.Int.Lemmas
Int.add_sub_cancel : ∀ (a b : ℤ), a + b - b = a
-- Mathlib.CategoryTheory.FiberedCategory.Fiber
/-- For fixed `S : 𝒮` this is the natural isomorphism between `fiberInclusion ⋙ p` and the constant
function valued at `S`.  -/
CategoryTheory.Functor.Fiber.fiberInclusionCompIsoConst : {𝒮 : Type u₁} →
  {𝒳 : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳] →
        {p : CategoryTheory.Functor 𝒳 𝒮} →
          {S : 𝒮} →
            CategoryTheory.Functor.Fiber.fiberInclusion.comp p ≅ (CategoryTheory.Functor.const (p.Fiber S)).obj S
-- Init.Control.Lawful.MonadAttach.Instances
_private.Init.Control.Lawful.MonadAttach.Instances.0.EStateM.instMonadAttach.match_1.splitter : {ε σ α : Type u_1} →
  (motive : EStateM.Result ε σ α → Sort u_2) →
    (x : EStateM.Result ε σ α) →
      ((a : α) → (s' : σ) → x = EStateM.Result.ok a s' → motive (EStateM.Result.ok a s')) →
        ((e : ε) → (s' : σ) → x = EStateM.Result.error e s' → motive (EStateM.Result.error e s')) → motive x
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.η_def : ∀ {k : Type u} {G : Type v} [inst : CommRing k] [inst_1 : Monoid G],
  CategoryTheory.Functor.OplaxMonoidal.η (Rep.linearization k G) = Rep.ofHom (Representation.LinearizeMonoidal.η k G)
-- Lean.Parser.Types
Lean.Parser.TrailingParser : Type
-- Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
AlgebraicGeometry.IsClosedImmersion.lift.eq_1 : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [inst : AlgebraicGeometry.IsClosedImmersion f]
  (H : AlgebraicGeometry.Scheme.Hom.ker f ≤ AlgebraicGeometry.Scheme.Hom.ker g),
  AlgebraicGeometry.IsClosedImmersion.lift f g H =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.toImage g)
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.IdealSheafData.inclusion H)
        (CategoryTheory.inv (AlgebraicGeometry.Scheme.Hom.toImage f)))
-- Mathlib.RingTheory.Localization.NumDen
IsFractionRing.exists_reduced_fraction : ∀ (A : Type u_1) [inst : CommRing A] [IsDomain A] [UniqueFactorizationMonoid A] {K : Type u_2} [inst_3 : Field K]
  [inst_4 : Algebra A K] [inst_5 : IsFractionRing A K] (x : K), ∃ a b, IsRelPrime a ↑b ∧ IsLocalization.mk' K a b = x
-- Std.Data.Iterators.Lemmas.Producers.Range
Std.Roo.length_iter : ∀ {α : Type u_1} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerableLT α] [Std.Rxo.IsAlwaysFinite α]
  [inst_5 : Std.PRange.LawfulUpwardEnumerable α] [inst_6 : Std.Rxo.HasSize α] [Std.Rxo.LawfulHasSize α] {r : Std.Roo α},
  r.iter.length = r.size
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.HasDetector.hasDetector : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} [self : CategoryTheory.HasDetector C],
  ∃ G, CategoryTheory.IsDetector G
-- Mathlib.Algebra.Group.Subgroup.Lattice
AddSubgroup.topEquiv_symm_apply_coe : ∀ {G : Type u_1} [inst : AddGroup G] (x : G), ↑(AddSubgroup.topEquiv.symm x) = x
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.getEntryLE?.go.eq_def : ∀ {α : Type u} {β : Type v} [inst : Ord α] (k : α) (best : Option (α × β))
  (a : Std.DTreeMap.Internal.Impl α fun x => β),
  Std.DTreeMap.Internal.Impl.Const.getEntryLE?.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.lt => Std.DTreeMap.Internal.Impl.Const.getEntryLE?.go k best l
      | Ordering.eq => some (ky, y)
      | Ordering.gt => Std.DTreeMap.Internal.Impl.Const.getEntryLE?.go k (some (ky, y)) r
-- Mathlib.Algebra.Homology.Embedding.Boundary
ComplexShape.Embedding.prev_f_of_not_boundaryGE : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') [e.IsRelIff]
  {i j : ι}, c.prev j = i → ¬e.BoundaryGE j → c'.prev (e.f j) = e.f i
-- Mathlib.Analysis.Convex.Extreme
isExtreme_biInter : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : SMul 𝕜 E] {A : Set E} {F : Set (Set E)},
  F.Nonempty → (∀ B ∈ F, IsExtreme 𝕜 A B) → IsExtreme 𝕜 A (⋂ B ∈ F, B)
-- Init.Data.Slice.Array.Lemmas
Subarray.mkSlice_roi_eq_mkSlice_rci : ∀ {α : Type u_1} {xs : Subarray α} {lo : ℕ},
  Std.Roi.Sliceable.mkSlice xs lo<...* = Std.Rci.Sliceable.mkSlice xs (lo + 1)...*
-- Mathlib.CategoryTheory.Monoidal.Free.Coherence
CategoryTheory.FreeMonoidalCategory.normalizeIsoApp.eq_1 : ∀ (C : Type u) (x : (CategoryTheory.Discrete ∘ CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject) C) (a : C),
  CategoryTheory.FreeMonoidalCategory.normalizeIsoApp C (CategoryTheory.FreeMonoidalCategory.of a) x =
    CategoryTheory.Iso.refl
      (((CategoryTheory.FreeMonoidalCategory.tensorFunc C).obj (CategoryTheory.FreeMonoidalCategory.of a)).obj x)
-- Mathlib.Algebra.Order.Group.Synonym
ofLex_pow : ∀ {α : Type u_1} {β : Type u_2} [inst : Pow α β] (a : Lex α) (b : β), ofLex (a ^ b) = ofLex a ^ b
-- Mathlib.Probability.Kernel.Condexp
ProbabilityTheory.condDistrib_apply_ae_eq_condExpKernel_map : ∀ {Ω : Type u_1} [mΩ : MeasurableSpace Ω] [inst : StandardBorelSpace Ω] {μ : MeasureTheory.Measure Ω}
  [inst_1 : MeasureTheory.IsFiniteMeasure μ] {β : Type u_3} {γ : Type u_4} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} [inst_2 : StandardBorelSpace β] [inst_3 : Nonempty β] {X : Ω → β} {Y : Ω → γ},
  Measurable X →
    Measurable Y →
      ∀ {s : Set β},
        MeasurableSet s →
          (fun a => ((ProbabilityTheory.condDistrib X Y μ) (Y a)) s) =ᵐ[μ] fun a =>
            (((ProbabilityTheory.condExpKernel μ (MeasurableSpace.comap Y mγ)).map X) a) s
-- Mathlib.Data.Nat.Prime.Defs
/-- A copy of `not_prime_one` stated in a way that works for `aesop`.

See https://github.com/leanprover-community/aesop/issues/197 for an explanation.  -/
Nat.prime_one_false : Nat.Prime 1 → False
-- Mathlib.Topology.Semicontinuity.Defs
SemicontinuousOn.comp : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {r : α → β → Prop} {γ : Type u_4}
  [inst_1 : TopologicalSpace γ] {g : γ → α} {s : Set γ} {t : Set α},
  SemicontinuousOn r t → ContinuousOn g s → Set.MapsTo g s t → SemicontinuousOn (r ∘ g) s
-- Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
/-- If `J ≤ I.map f`, then `f` restricts to a map `I ⟶ J` between the closed subschemes.  -/
AlgebraicGeometry.Scheme.IdealSheafData.subschemeMap : {X Y : AlgebraicGeometry.Scheme} →
  (I : X.IdealSheafData) → (J : Y.IdealSheafData) → (f : X ⟶ Y) → J ≤ I.map f → (I.subscheme ⟶ J.subscheme)
-- Std.Data.TreeMap.Raw.Basic
/-- Check if any element satisfies the predicate, short-circuiting if a predicate fails.  -/
Std.TreeMap.Raw.any : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap.Raw α β cmp → (α → β → Bool) → Bool
-- Mathlib.Algebra.Group.Subsemigroup.Defs
AddSubsemigroup.mem_mk : ∀ {M : Type u_1} [inst : Add M] {s : Set M} {x : M} (h_add : ∀ {a b : M}, a ∈ s → b ∈ s → a + b ∈ s),
  x ∈ { carrier := s, add_mem' := h_add } ↔ x ∈ s
-- Mathlib.ModelTheory.Basic
/-- The homomorphism commutes with the interpretations of the function symbols  -/
FirstOrder.Language.Equiv.map_fun' : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N]
  (self : L.Equiv M N) {n : ℕ} (f : L.Functions n) (x : Fin n → M),
  self.toFun (FirstOrder.Language.Structure.funMap f x) = FirstOrder.Language.Structure.funMap f (self.toFun ∘ x)
-- Mathlib.Algebra.Group.Subgroup.Ker
/-- The additive kernel of an `AddMonoid` homomorphism is the `AddSubgroup` of elements
such that `f x = 0`  -/
AddMonoidHom.ker : {G : Type u_1} → [inst : AddGroup G] → {M : Type u_7} → [inst_1 : AddZeroClass M] → (G →+ M) → AddSubgroup G
-- Mathlib.Probability.Independence.Basic
/-- **Alias** of the forward direction of `ProbabilityTheory.indepFun_iff_measure_inter_preimage_eq_mul`. -/
ProbabilityTheory.IndepFun.measure_inter_preimage_eq_mul : ∀ {Ω : Type u_1} {β : Type u_6} {β' : Type u_7} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {f : Ω → β}
  {g : Ω → β'} {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'},
  ProbabilityTheory.IndepFun f g μ →
    ∀ (s : Set β) (t : Set β'), MeasurableSet s → MeasurableSet t → μ (f ⁻¹' s ∩ g ⁻¹' t) = μ (f ⁻¹' s) * μ (g ⁻¹' t)
-- Mathlib.Topology.LocalAtTarget
TopologicalSpace.IsOpenCover.denseRange_iff_restrictPreimage : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {f : α → β} {ι : Type u_3}
  {U : ι → TopologicalSpace.Opens β},
  TopologicalSpace.IsOpenCover U → (DenseRange f ↔ ∀ (i : ι), DenseRange ((U i).carrier.restrictPreimage f))
-- Init.Data.Slice.List.Basic
instSliceableListNatListSlice_2 : {α : Type u} → Std.Rci.Sliceable (List α) ℕ (ListSlice α)
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
SheafOfModules.isQuasicoherent_over : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : ∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat]
  [inst_2 : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat]
  [inst_3 : ∀ (X : C) (Y : CategoryTheory.Over X), CategoryTheory.HasSheafify ((J.over X).over Y) AddCommGrpCat]
  [inst_4 : ∀ (X : C) (Y : CategoryTheory.Over X), ((J.over X).over Y).WEqualsLocallyBijective AddCommGrpCat]
  [CategoryTheory.Limits.HasPullbacks C] [CategoryTheory.Limits.HasBinaryProducts C] (M : SheafOfModules R) (X : C)
  [M.IsQuasicoherent], (M.over X).IsQuasicoherent
-- Std.Do.PostCond
Std.Do.ExceptConds.fst_and : ∀ {ps : Std.Do.PostShape} {ε : Type u} {x₁ x₂ : Std.Do.ExceptConds (Std.Do.PostShape.except ε ps)},
  (x₁ ∧ₑ x₂).1 = fun e => spred(x₁.1 e ∧ x₂.1 e)
-- Init.GrindInstances.ToInt
Lean.Grind.instDivIntIi : Lean.Grind.ToInt.Div ℤ Lean.Grind.IntInterval.ii
-- Mathlib.Order.RelClasses
/-- **Alias** of `not_ssubset_of_superset`.

---

Set notation form of `not_lt_of_ge` -/
not_ssubset_of_subset : ∀ {α : Type u_1} [UsesSetNotationForOrder α] [inst : Preorder α] {a b : α}, a ⊆ b → ¬b ⊂ a
-- Mathlib.Data.PEquiv
Equiv.toPEquiv_refl : ∀ {α : Type u_1}, (Equiv.refl α).toPEquiv = PEquiv.refl α
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.integral_Icc_eq_integral_Ioo : ∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {f : X → E} {μ : MeasureTheory.Measure X} [inst_2 : PartialOrder X] {x y : X} [MeasureTheory.NullSingletonClass μ],
  ∫ (t : X) in Set.Icc x y, f t ∂μ = ∫ (t : X) in Set.Ioo x y, f t ∂μ
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.ofList_nil : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [EquivBEq α] [LawfulHashable α], Std.ExtHashSet.ofList [] = ∅
-- Init.Grind.Ring.CommSemiringAdapter
Lean.Grind.CommRing.Poly.denoteS_mulMon_nc : ∀ {α : Type u_1} [inst : Lean.Grind.Semiring α] (ctx : Lean.Grind.CommRing.Context α) (k : ℤ)
  (m : Lean.Grind.CommRing.Mon) (p : Lean.Grind.CommRing.Poly),
  k ≥ 0 →
    p.NonnegCoeffs →
      Lean.Grind.CommRing.Poly.denoteS ctx (Lean.Grind.CommRing.Poly.mulMon_nc k m p) =
        ↑k.toNat * Lean.Grind.CommRing.Mon.denote ctx m * Lean.Grind.CommRing.Poly.denoteS ctx p
-- Init.Core
Insert.mk : {α : outParam (Type u)} → {γ : Type v} → (α → γ → γ) → Insert α γ
-- Init.Data.SInt.Lemmas
Int8.toInt_neg : ∀ (n : Int8), (-n).toInt = (-n.toInt).bmod (2 ^ 8)
-- Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
RootPairing.GeckConstruction.f.eq_1 : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N}
  [inst_5 : P.IsCrystallographic] {b : P.Base} [inst_6 : Finite ι] [inst_7 : IsDomain R] [inst_8 : CharZero R]
  (i : ↥b.support),
  RootPairing.GeckConstruction.f i =
    Matrix.fromBlocks 0 (Matrix.of fun i' j => if i' = i ∧ j = ↑i then 1 else 0)
      (Matrix.of fun i' j => if i' = -↑i then ↑|b.cartanMatrix i j| else 0)
      (Matrix.of fun i' j => if P.root i' = P.root j - P.root ↑i then ↑(RootPairing.chainTopCoeff (↑i) j) + 1 else 0)
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
/-- **Alias** of `SkewMonoidAlgebra.ofCoeff_sub`. -/
SkewMonoidAlgebra.ofFinsupp_sub : ∀ {k : Type u_1} {G : Type u_2} [inst : AddGroup k] {a b : G →₀ k}, { coeff := a - b } = { coeff := a } - { coeff := b }