mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.Basic
Lean.Meta.instReprConfig_2 : Repr Lean.Meta.Config
-- Mathlib.Probability.Moments.SubGaussian
ProbabilityTheory.Kernel.HasSubgaussianMGF.integrable_exp_mul : ∀ {Ω : Type u_1} {Ω' : Type u_2} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {X : Ω → ℝ} {c : NNReal}
  {κ : ProbabilityTheory.Kernel Ω' Ω}
  {ν : autoParam (MeasureTheory.Measure Ω') ProbabilityTheory.Kernel.HasSubgaussianMGF._auto_1},
  ProbabilityTheory.Kernel.HasSubgaussianMGF X c κ ν →
    ∀ (t : ℝ), MeasureTheory.Integrable (fun ω => Real.exp (t * X ω)) (ν.bind ⇑κ)
-- Mathlib.CategoryTheory.Limits.Presheaf
CategoryTheory.Presheaf.tautologicalCocone'_ι_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (P : CategoryTheory.Functor Cᵒᵖ (Type (max w v₁)))
  (X : CategoryTheory.CostructuredArrow CategoryTheory.uliftYoneda.{w, v₁, u₁} P),
  (CategoryTheory.Presheaf.tautologicalCocone' P).ι.app X = X.hom
-- Lean.Log
/-- If `msg` is tagged as a named error, appends the error description widget displaying the
corresponding error name and explanation link. Otherwise, returns `msg` unaltered.
 -/
_private.Lean.Log.0.Lean.MessageData.appendDescriptionWidgetIfNamed : Lean.MessageData → Lean.MessageData
-- Mathlib.Data.ENNReal.Basic
ENNReal.coe_lt_natCast : ∀ {r : NNReal} {n : ℕ}, ↑r < ↑n ↔ r < ↑n
-- Mathlib.Topology.MetricSpace.Dilation
Dilation.mk.inj : ∀ {α : Type u_1} {β : Type u_2} {inst : PseudoEMetricSpace α} {inst_1 : PseudoEMetricSpace β} {toFun : α → β}
  {edist_eq' : ∃ r, r ≠ 0 ∧ ∀ (x y : α), edist (toFun x) (toFun y) = ↑r * edist x y} {toFun_1 : α → β}
  {edist_eq'_1 : ∃ r, r ≠ 0 ∧ ∀ (x y : α), edist (toFun_1 x) (toFun_1 y) = ↑r * edist x y},
  { toFun := toFun, edist_eq' := edist_eq' } = { toFun := toFun_1, edist_eq' := edist_eq'_1 } → toFun = toFun_1
-- Init.Grind.Ordered.Module
Lean.Grind.OrderedAdd.nsmul_lt_nsmul_iff : ∀ {M : Type u} [inst : LE M] [inst_1 : Std.IsPreorder M] [inst_2 : Lean.Grind.NatModule M] [Lean.Grind.OrderedAdd M]
  [inst_4 : LT M] [Std.LawfulOrderLT M] (k : ℕ) {a b : M}, a < b → (k • a < k • b ↔ 0 < k)
-- Mathlib.Algebra.Group.Invertible.Defs
/-- `Invertible a` gives a two-sided multiplicative inverse of `a`.  -/
Invertible : {α : Type u} → [Mul α] → [One α] → α → Type u
-- Lean.Meta.Match.Basic
Lean.Meta.Match.congrEqnThmSuffixBase : String
-- Lean.Data.PersistentHashMap
Lean.PersistentHashMap.Node.collision : {α : Type u} → {β : Type v} → (ks : Array α) → (vs : Array β) → ks.size = vs.size → Lean.PersistentHashMap.Node α β
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
WeierstrassCurve.Jacobian.Point.instZeroOfNontrivial : {R : Type r} → [inst : CommRing R] → {W' : WeierstrassCurve.Jacobian R} → [Nontrivial R] → Zero W'.Point
-- Mathlib.CategoryTheory.Subobject.Lattice
CategoryTheory.Subobject.inf_eq_map_pullback' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] {A : C}
  (f₁ : CategoryTheory.MonoOver A) (f₂ : CategoryTheory.Subobject A),
  (CategoryTheory.Subobject.inf.obj (Quotient.mk'' f₁)).obj f₂ =
    (CategoryTheory.Subobject.map f₁.arrow).obj ((CategoryTheory.Subobject.pullback f₁.arrow).obj f₂)
-- Mathlib.RingTheory.PowerSeries.Order
/-- The order of a formal power series is exactly `n` if the `n`th coefficient is nonzero,
and the `i`th coefficient is `0` for all `i < n`.  -/
PowerSeries.order_eq : ∀ {R : Type u_1} [inst : Semiring R] {φ : PowerSeries R} {n : ℕ∞},
  φ.order = n ↔ (∀ (i : ℕ), ↑i = n → (PowerSeries.coeff i) φ ≠ 0) ∧ ∀ (i : ℕ), ↑i < n → (PowerSeries.coeff i) φ = 0
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- The functor `WalkingParallelPair ⥤ WalkingParallelPairᵒᵖ` sending left to left and right to
right.
 -/
CategoryTheory.Limits.walkingParallelPairOp : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.WalkingParallelPairᵒᵖ
-- Mathlib.Order.RelClasses
/-- An unbounded or cofinal set.  -/
Set.Unbounded : {α : Type u} → (α → α → Prop) → Set α → Prop
-- Mathlib.CategoryTheory.Sites.Precoverage
CategoryTheory.Precoverage.instHasIsosComap : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  {F : CategoryTheory.Functor C D} {J : CategoryTheory.Precoverage D} [J.HasIsos],
  (CategoryTheory.Precoverage.comap F J).HasIsos
-- Mathlib.Algebra.Group.Center
Set.center_pi : ∀ {ι : Type u_2} {A : ι → Type u_3} [inst : (i : ι) → Mul (A i)],
  Set.center ((i : ι) → A i) = Set.univ.pi fun i => Set.center (A i)
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Ioc_sdiff_Ioi : ∀ {α : Type u_1} [inst : LinearOrder α] {a b c : α}, Set.Ioc a b \ Set.Ioi c = Set.Ioc a (min b c)
-- Lean.Environment
_private.Lean.Environment.0.Lean.EnvExtension.modifyState.unsafe_impl_12 : {σ : Type} → Lean.EnvExtension σ → (σ → σ) → Lean.Kernel.Environment → Array Lean.EnvExtensionState
-- Mathlib.Computability.DFA
/-- DFAs are closed under intersection.  -/
DFA.inter : {α : Type u} → {σ1 σ2 : Type v} → DFA α σ1 → DFA α σ2 → DFA α (σ1 × σ2)
-- Mathlib.CategoryTheory.MorphismProperty.Factorization
/-- The functorial factorization axiom for two classes of morphisms `W₁` and `W₂` in a
category `C`. It asserts that any morphism can be factored in a functorial manner
as a morphism in `W₁` followed by a morphism in `W₂`.  -/
CategoryTheory.MorphismProperty.HasFunctorialFactorization : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    CategoryTheory.MorphismProperty C → CategoryTheory.MorphismProperty C → Prop
-- Init.Data.BitVec.Basic
BitVec.add_eq : ∀ {w : ℕ} (x y : BitVec w), x.add y = x + y
-- Mathlib.CategoryTheory.GradedObject.Braiding
CategoryTheory.GradedObject.Monoidal.braiding_naturality_left : ∀ {I : Type u_1} [inst : AddCommMonoid I] {C : Type u_2} [inst_1 : CategoryTheory.Category.{v_1, u_2} C]
  [inst_2 : CategoryTheory.MonoidalCategory C] {X Y : CategoryTheory.GradedObject I C}
  (Z : CategoryTheory.GradedObject I C) [inst_3 : CategoryTheory.BraidedCategory C] [inst_4 : Y.HasTensor Z]
  [inst_5 : Z.HasTensor Y] [inst_6 : X.HasTensor Z] [inst_7 : Z.HasTensor X] (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.whiskerRight f Z)
      (CategoryTheory.GradedObject.Monoidal.braiding Y Z).hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.braiding X Z).hom
      (CategoryTheory.GradedObject.Monoidal.whiskerLeft Z f)
-- Mathlib.Analysis.Normed.Lp.ProdLp
/-- Seminormed group instance on the product of two normed groups, using the `L^p`
norm.  -/
WithLp.instProdSeminormedAddCommGroup : (p : ENNReal) →
  (α : Type u_2) →
    (β : Type u_3) →
      [hp : Fact (1 ≤ p)] →
        [SeminormedAddCommGroup α] → [SeminormedAddCommGroup β] → SeminormedAddCommGroup (WithLp p (α × β))
-- Mathlib.Algebra.Group.Subsemigroup.Basic
Subsemigroup.closure_union : ∀ {M : Type u_1} [inst : Mul M] (s t : Set M),
  Subsemigroup.closure (s ∪ t) = Subsemigroup.closure s ⊔ Subsemigroup.closure t
-- Mathlib.AlgebraicTopology.DoldKan.Compatibility
AlgebraicTopology.DoldKan.Compatibility.equivalence₂CounitIso_eq : ∀ {A : Type u_1} {A' : Type u_2} {B : Type u_3} {B' : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} A'] [inst_2 : CategoryTheory.Category.{v_3, u_3} B]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} B'] {eA : A ≌ A'} (eB : B ≌ B') {e' : A' ≌ B'}
  {F : CategoryTheory.Functor A B'} (hF : eA.functor.comp e'.functor ≅ F),
  (AlgebraicTopology.DoldKan.Compatibility.equivalence₂ eB hF).counitIso =
    AlgebraicTopology.DoldKan.Compatibility.equivalence₂CounitIso eB hF
-- Mathlib.CategoryTheory.Sites.Coverage
/-- The Grothendieck topology associated to a coverage `K`.
It is defined *inductively* as follows:
1. If `S` is a covering presieve for `K`, then the sieve generated by `S` is a covering
  sieve for the associated Grothendieck topology.
2. The top sieves are in the associated Grothendieck topology.
3. Add all sieves required by the *local character* axiom of a Grothendieck topology.

The pullback compatibility condition for a coverage ensures that the
associated Grothendieck topology is pullback stable, and so an additional constructor
in the inductive construction is not needed.
 -/
CategoryTheory.Coverage.toGrothendieck : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] → CategoryTheory.Coverage C → CategoryTheory.GrothendieckTopology C
-- Init.Omega.Coeffs
Lean.Omega.Coeffs.combo_eq_smul_add_smul : ∀ (a : ℤ) (xs : Lean.Omega.Coeffs) (b : ℤ) (ys : Lean.Omega.Coeffs), Lean.Omega.Coeffs.combo a xs b ys = a * xs + b * ys
-- Mathlib.MeasureTheory.Measure.ProbabilityMeasure
/-- Integration of (nonnegative bounded continuous) test functions against Borel probability
measures depends continuously on the measure.  -/
MeasureTheory.ProbabilityMeasure.continuous_testAgainstNN_eval : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω] [inst_2 : OpensMeasurableSpace Ω]
  (f : BoundedContinuousFunction Ω NNReal), Continuous fun μ => μ.toFiniteMeasure.testAgainstNN f
-- Mathlib.Geometry.Manifold.PartitionOfUnity
SmoothBumpCovering.support_toSmoothPartitionOfUnity_subset : ∀ {ι : Type uι} {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH}
  [inst_2 : TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_3 : TopologicalSpace M]
  [inst_4 : ChartedSpace H M] [inst_5 : FiniteDimensional ℝ E] {s : Set M} (fs : SmoothBumpCovering ι I M s)
  [inst_6 : T2Space M] [inst_7 : IsManifold I (↑⊤) M] (i : ι),
  Function.support ⇑(fs.toSmoothPartitionOfUnity i) ⊆ Function.support ↑(fs.toFun i)
-- Std.Data.DTreeMap.Internal.Operations
Std.DTreeMap.Internal.Impl.link2!.eq_def : ∀ {α : Type u} {β : α → Type v} (l r : Std.DTreeMap.Internal.Impl α β),
  l.link2! r =
    match l with
    | Std.DTreeMap.Internal.Impl.leaf => r
    | l@h:(Std.DTreeMap.Internal.Impl.inner szl k' v' l' r') =>
      match r with
      | Std.DTreeMap.Internal.Impl.leaf => l
      | r@h:(Std.DTreeMap.Internal.Impl.inner szr k'' v'' l'' r'') =>
        if Std.DTreeMap.Internal.delta * szl < szr then Std.DTreeMap.Internal.Impl.balanceL! k'' v'' (l.link2! l'') r''
        else
          if Std.DTreeMap.Internal.delta * szr < szl then Std.DTreeMap.Internal.Impl.balanceR! k' v' l' (r'.link2! r)
          else l.glue! r
-- Mathlib.Topology.Order.IsLUB
eventually_le_const_iff_forall_gt_eventually_lt_const : ∀ {α : Type u_1} {γ : Type u_2} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α]
  [FirstCountableTopology α] {l : Filter γ} [CountableInterFilter l] {f : γ → α} {a : α},
  (∀ᶠ (x : γ) in l, f x ≤ a) ↔ ∀ (b : α), a < b → ∀ᶠ (x : γ) in l, f x < b
-- Mathlib.Algebra.EuclideanDomain.Basic
EuclideanDomain.zero_mod : ∀ {R : Type u} [inst : EuclideanDomain R] (b : R), 0 % b = 0
-- Mathlib.Tactic.Linter.DocString
_private.Mathlib.Tactic.Linter.DocString.0.Mathlib.Linter.getDeclModifiers.match_1.splitter : (motive : Lean.Syntax → Sort u_1) →
  (x : Lean.Syntax) →
    ((info : Lean.SourceInfo) →
        (kind : Lean.SyntaxNodeKind) → (args : Array Lean.Syntax) → motive (Lean.Syntax.node info kind args)) →
      ((x : Lean.Syntax) →
          (∀ (info : Lean.SourceInfo) (kind : Lean.SyntaxNodeKind) (args : Array Lean.Syntax),
              x = Lean.Syntax.node info kind args → False) →
            motive x) →
        motive x
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.size_erase_le : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  (t.erase k).size ≤ t.size
-- Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
UniformConvergenceCLM.eventually_nhds_zero_mapsTo : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {E : Type u_3}
  {F : Type u_4} [inst_2 : AddCommGroup E] [inst_3 : Module 𝕜₁ E] [inst_4 : TopologicalSpace E]
  [inst_5 : AddCommGroup F] [inst_6 : Module 𝕜₂ F] [inst_7 : TopologicalSpace F] [inst_8 : IsTopologicalAddGroup F]
  {𝔖 : Set (Set E)} {s : Set E},
  s ∈ 𝔖 → ∀ {U : Set F}, U ∈ nhds 0 → ∀ᶠ (f : UniformConvergenceCLM σ F 𝔖) in nhds 0, Set.MapsTo (⇑f) s U
-- Mathlib.Logic.Basic
dite_eq_iff' : ∀ {α : Sort u_1} {P : Prop} [inst : Decidable P] {c : α} {A : P → α} {B : ¬P → α},
  dite P A B = c ↔ (∀ (h : P), A h = c) ∧ ∀ (h : ¬P), B h = c
-- Mathlib.Algebra.Field.Periodic
Function.Antiperiodic.const_smul₀ : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {c : α} [inst : AddMonoid α] [inst_1 : Neg β]
  [inst_2 : GroupWithZero γ] [inst_3 : DistribMulAction γ α],
  Function.Antiperiodic f c → ∀ {a : γ}, a ≠ 0 → Function.Antiperiodic (fun x => f (a • x)) (a⁻¹ • c)
-- Lean.Compiler.IR.Basic
Lean.IR.LitVal.str.inj : ∀ {v v_1 : String}, Lean.IR.LitVal.str v = Lean.IR.LitVal.str v_1 → v = v_1
-- Mathlib.MeasureTheory.Measure.Hausdorff
/-- A formula for `μH[d] s`.  -/
MeasureTheory.Measure.hausdorffMeasure_apply : ∀ {X : Type u_2} [inst : EMetricSpace X] [inst_1 : MeasurableSpace X] [inst_2 : BorelSpace X] (d : ℝ) (s : Set X),
  (MeasureTheory.Measure.hausdorffMeasure d) s =
    ⨆ r,
      ⨆ (_ : 0 < r),
        ⨅ t,
          ⨅ (_ : s ⊆ ⋃ n, t n),
            ⨅ (_ : ∀ (n : ℕ), Metric.ediam (t n) ≤ r), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), Metric.ediam (t n) ^ d
-- Mathlib.CategoryTheory.Grothendieck
CategoryTheory.Grothendieck.preInv.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} D]
  (F : CategoryTheory.Functor C CategoryTheory.Cat) (G : D ≌ C),
  CategoryTheory.Grothendieck.preInv F G =
    (CategoryTheory.Grothendieck.map (CategoryTheory.Functor.whiskerRight G.counitInv F)).comp
      (CategoryTheory.Grothendieck.pre (G.functor.comp F) G.inverse)
-- Mathlib.Logic.Relation
Relation.SymmGen.instRefl : ∀ {α : Type u_1} {r : α → α → Prop} [Std.Refl r], Std.Refl (Relation.SymmGen r)
-- Mathlib.Analysis.Calculus.FDeriv.Add
HasFDerivAtFilter.sub : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f g : E → F}
  {f' g' : E →L[𝕜] F} {L : Filter (E × E)},
  HasFDerivAtFilter f f' L → HasFDerivAtFilter g g' L → HasFDerivAtFilter (f - g) (f' - g') L
-- Mathlib.MeasureTheory.Measure.Haar.OfBasis
convex_parallelepiped : ∀ {ι : Type u_1} {E : Type u_3} [inst : Fintype ι] [inst_1 : AddCommGroup E] [inst_2 : Module ℝ E] (v : ι → E),
  Convex ℝ (parallelepiped v)
-- Mathlib.RingTheory.NonUnitalSubring.Defs
/-- `NonUnitalSubringClass S R` states that `S` is a type of subsets `s ⊆ R` that
are both a multiplicative submonoid and an additive subgroup.  -/
NonUnitalSubringClass : (S : Type u_1) → (R : Type u) → [NonUnitalNonAssocRing R] → [SetLike S R] → Prop
-- Mathlib.Analysis.Complex.AbelLimit
Complex.stolzSet.eq_1 : ∀ (M : ℝ), Complex.stolzSet M = {z | ‖z‖ < 1 ∧ ‖1 - z‖ < M * (1 - ‖z‖)}
-- Mathlib.LinearAlgebra.Basis.Basic
Module.Basis.coe_mk : ∀ {ι : Type u_1} {R : Type u_3} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {v : ι → M} (hli : LinearIndependent R v) (hsp : ⊤ ≤ Submodule.span R (Set.range v)), ⇑(Module.Basis.mk hli hsp) = v
-- Mathlib.Analysis.BoxIntegral.Partition.Filter
/-- A set `s : Set (TaggedPrepartition I)` belongs to `l.toFilter I` if for any `c : ℝ≥0` there
exists a function `r : ℝⁿ → (0, ∞)` (or a constant `r` if `l.bRiemann = true`) such that
`s` contains each prepartition `π` such that `l.MemBaseSet I c r π`.  -/
BoxIntegral.IntegrationParams.toFilter : {ι : Type u_1} →
  [Fintype ι] → BoxIntegral.IntegrationParams → (I : BoxIntegral.Box ι) → Filter (BoxIntegral.TaggedPrepartition I)
-- Mathlib.Topology.Instances.TrivSqZeroExt
TrivSqZeroExt.instContinuousMulOfContinuousSMulMulOppositeOfContinuousAdd : ∀ {R : Type u_3} {M : Type u_4} [inst : TopologicalSpace R] [inst_1 : TopologicalSpace M] [inst_2 : Mul R]
  [inst_3 : Add M] [inst_4 : SMul R M] [inst_5 : SMul Rᵐᵒᵖ M] [ContinuousMul R] [ContinuousSMul R M]
  [ContinuousSMul Rᵐᵒᵖ M] [ContinuousAdd M], ContinuousMul (TrivSqZeroExt R M)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Real.arctan_nonneg : ∀ {x : ℝ}, 0 ≤ Real.arctan x ↔ 0 ≤ x
-- Mathlib.Order.DirectedInverseSystem
InverseSystem.piLTProj.eq_1 : ∀ {ι : Type u_1} [inst : Preorder ι] {X : ι → Type u_5} ⦃i j : ι⦄ (h : i ≤ j) (f : InverseSystem.piLT X j)
  (l : ↑(Set.Iio i)), InverseSystem.piLTProj h f l = f ⟨↑l, ⋯⟩
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnSeries.algebraMap_apply : ∀ {Γ : Type u_1} {R : Type u_3} [inst : AddCommMonoid Γ] [inst_1 : PartialOrder Γ] [inst_2 : IsOrderedCancelAddMonoid Γ]
  [inst_3 : CommSemiring R] {A : Type u_6} [inst_4 : Semiring A] [inst_5 : Algebra R A] {r : R},
  (algebraMap R (HahnSeries Γ A)) r = HahnSeries.C ((algebraMap R A) r)
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.IsAffineOpen.self_le_iSup_basicOpen_iff : ∀ {X : AlgebraicGeometry.Scheme} {U : X.Opens},
  AlgebraicGeometry.IsAffineOpen U →
    ∀ {s : Set ↑(X.presheaf.obj (Opposite.op U))}, U ≤ ⨆ f, X.basicOpen ↑f ↔ Ideal.span s = ⊤
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.MonoFactorisation.mk.injEq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} (I : C) (m : I ⟶ Y)
  [m_mono : CategoryTheory.Mono m] (e : X ⟶ I)
  (fac : autoParam (CategoryTheory.CategoryStruct.comp e m = f) CategoryTheory.Limits.MonoFactorisation.fac._autoParam)
  (I_1 : C) (m_1 : I_1 ⟶ Y) (m_mono_1 : CategoryTheory.Mono m_1) (e_1 : X ⟶ I_1)
  (fac_1 :
    autoParam (CategoryTheory.CategoryStruct.comp e_1 m_1 = f) CategoryTheory.Limits.MonoFactorisation.fac._autoParam),
  ({ I := I, m := m, m_mono := m_mono, e := e, fac := fac } =
      { I := I_1, m := m_1, m_mono := m_mono_1, e := e_1, fac := fac_1 }) =
    (I = I_1 ∧ m ≍ m_1 ∧ e ≍ e_1)
-- Mathlib.LinearAlgebra.CliffordAlgebra.Fold
CliffordAlgebra.foldr_mul : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup N]
  [inst_3 : Module R M] [inst_4 : Module R N] (Q : QuadraticForm R M) (f : M →ₗ[R] N →ₗ[R] N)
  (hf : ∀ (m : M) (x : N), (f m) ((f m) x) = Q m • x) (n : N) (a b : CliffordAlgebra Q),
  ((CliffordAlgebra.foldr Q f hf) n) (a * b) = ((CliffordAlgebra.foldr Q f hf) (((CliffordAlgebra.foldr Q f hf) n) b)) a
-- Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne
/-- In a standard Borel space, a zero-one measure that is not the zero measure is a Dirac
measure.  -/
MeasureTheory.IsZeroOneMeasure.exists_eq_dirac : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsZeroOneMeasure μ]
  [StandardBorelSpace α] [NeZero μ], ∃ x₀, μ = MeasureTheory.Measure.dirac x₀
-- Mathlib.Topology.Algebra.Group.Basic
/-- Conjugation acting on fixed element of the additive group is continuous when both
`add` and `neg` are continuous.  -/
IsTopologicalAddGroup.continuous_addConj' : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Neg G] [inst_2 : Add G] [ContinuousAdd G] [ContinuousNeg G]
  (h : G), Continuous fun g => g + h + -g
-- Mathlib.RingTheory.LocalIso
/-- An `R`-algebra `S` is a local isomorphism if source locally (in the geometric sense),
it is a standard open immersion.  -/
Algebra.IsLocalIso : (R : Type u_1) → (S : Type u_2) → [inst : CommSemiring R] → [inst_1 : CommSemiring S] → [Algebra R S] → Prop
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey?_eq_some_getKeyD : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → ∀ {a fallback : α}, a ∈ t → t.getKey? a = some (t.getKeyD a fallback)
-- Mathlib.Geometry.Manifold.GroupLieAlgebra
inverse_mfderiv_add_left : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4}
  [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : AddGroup G] [LieAddGroup I (minSmoothness 𝕜 3) G]
  {g h : G}, ((mfderiv% fun b => g + b) h).inverse = (mfderiv% fun b => -g + b) (g + h)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.ShrinkYoneda
CategoryTheory.shrinkYonedaMon_map_app_shrinkYonedaObjObjEquiv_symm : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C]
  [inst_2 : CategoryTheory.CartesianMonoidalCategory C] {M M' : CategoryTheory.Mon C} {Y : Cᵒᵖ}
  (f : Opposite.unop Y ⟶ M.X) (g : M ⟶ M'),
  (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.shrinkYonedaMon.{w, v, u}.map g).app Y))
      (CategoryTheory.shrinkYonedaMonObjObjEquiv.symm f) =
    CategoryTheory.shrinkYonedaMonObjObjEquiv.symm (CategoryTheory.CategoryStruct.comp f g.hom)
-- Mathlib.CategoryTheory.Extensive
CategoryTheory.HasPullbacksOfInclusions.hasPullbackInr : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasBinaryCoproducts C]
  [CategoryTheory.HasPullbacksOfInclusions C] {X Y Z : C} (f : Z ⟶ X ⨿ Y),
  CategoryTheory.Limits.HasPullback CategoryTheory.Limits.coprod.inr f
-- Mathlib.Data.Fintype.EquivFin
Infinite.instSigmaOfNonempty_1 : ∀ {α : Type u_1} {β : α → Type u_4} [Nonempty α] [∀ (a : α), Infinite (β a)], Infinite ((a : α) × β a)
-- Mathlib.RingTheory.Extension.Cotangent.Free
Algebra.Generators.disjoint_ker_toKaehler_of_linearIndependent : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {ι : Type u_3}
  {κ : Type u_5} (P : Algebra.Generators R S ι) {v : κ → ι},
  (LinearIndependent S fun k => (KaehlerDifferential.D R S) (P.val (v k))) →
    Disjoint P.toExtension.toKaehler.ker (Submodule.span S (Set.range fun x => P.cotangentSpaceBasis (v x)))
-- Mathlib.Order.Bounds.Defs
/-- A set is bounded above if there exists an upper bound.  -/
BddAbove : {α : Type u_1} → [LE α] → Set α → Prop
-- Mathlib.CategoryTheory.Sites.LocalSite
CategoryTheory.GrothendieckTopology.IsLocalSite.point.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C)
  [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C] [inst_2 : J.IsLocalSite],
  CategoryTheory.GrothendieckTopology.IsLocalSite.point J = CategoryTheory.GrothendieckTopology.IsLocalSite.point J
-- Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Real.hasDerivAt_qaryEntropy : ∀ {q : ℕ} {p : ℝ}, p ≠ 0 → p ≠ 1 → HasDerivAt (Real.qaryEntropy q) (Real.log (↑q - 1) + Real.log (1 - p) - Real.log p) p
-- Mathlib.Topology.ContinuousMap.Basic
/-- Interpret `f : α → β` as an element of `C(α, β)`, falling back to the default value
`default : C(α, β)` if `f` is not continuous.
This is mainly intended to be used for `C(α, β)`-valued integration. For example, if a family of
functions `f : ι → α → β` satisfies that `f i` is continuous for almost every `i`, you can write
the `C(α, β)`-valued integral "`∫ i, f i`" as `∫ i, ContinuousMap.mkD (f i) 0`.
 -/
ContinuousMap.mkD : {α : Type u_1} →
  {β : Type u_2} → [inst : TopologicalSpace α] → [inst_1 : TopologicalSpace β] → (α → β) → C(α, β) → C(α, β)
-- Mathlib.Data.Complex.BigOperators
Complex.ofReal_balance : ∀ {α : Type u_1} [inst : Fintype α] (f : α → ℝ) (a : α), ↑(Fintype.balance f a) = Fintype.balance (Complex.ofReal ∘ f) a
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
_private.Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop.0.Std.IterM.DefaultConsumers.forIn'.match_1.splitter : {β : Type u_3} →
  (γ : Type u_1) →
    (PlausibleForInStep : β → γ → ForInStep γ → Prop) →
      (acc : γ) →
        (out : β) →
          (motive : Subtype (PlausibleForInStep out acc) → Sort u_2) →
            (__do_lift : Subtype (PlausibleForInStep out acc)) →
              ((c : γ) → (h' : PlausibleForInStep out acc (ForInStep.yield c)) → motive ⟨ForInStep.yield c, h'⟩) →
                ((c : γ) → (h : PlausibleForInStep out acc (ForInStep.done c)) → motive ⟨ForInStep.done c, h⟩) →
                  motive __do_lift
-- Init.Data.Bool
Bool.xor_true : ∀ (x : Bool), (x ^^ true) = !x
-- Mathlib.Topology.Algebra.Constructions.DomMulAct
DomMulAct.instNormalSpace : ∀ {M : Type u_1} [inst : TopologicalSpace M] [NormalSpace M], NormalSpace Mᵈᵐᵃ
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
abs_nonneg : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : AddGroup α] [AddLeftMono α] [AddRightMono α] (a : α), 0 ≤ |a|