mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Subgroup.Basic
/-- The normal closure of `s` is a normal additive subgroup.  -/
AddSubgroup.normalClosure_normal : ∀ {G : Type u_1} [inst : AddGroup G] {s : Set G}, (AddSubgroup.normalClosure s).Normal
-- Mathlib.MeasureTheory.Covering.Differentiation
VitaliFamily.ae_tendsto_lintegral_enorm_sub_div : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  (v : VitaliFamily μ) {E : Type u_2} [inst_1 : NormedAddCommGroup E] [SecondCountableTopology α] [BorelSpace α]
  [MeasureTheory.IsLocallyFiniteMeasure μ] {f : α → E},
  MeasureTheory.LocallyIntegrable f μ →
    ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun a => (∫⁻ (y : α) in a, ‖f y - f x‖ₑ ∂μ) / μ a) (v.filterAt x) (nhds 0)
-- Std.Sync.Channel
Std.Channel.instAsyncStreamOfInhabited : {α : Type} → [Inhabited α] → Std.Async.IO.AsyncStream (Std.Channel α) α
-- Mathlib.Algebra.Category.ModuleCat.Basic
ModuleCat.hom_inv_apply : ∀ {R : Type u} [inst : Ring R] {M N : ModuleCat R} (e : M ≅ N) (x : ↑N),
  (CategoryTheory.ConcreteCategory.hom e.hom) ((CategoryTheory.ConcreteCategory.hom e.inv) x) = x
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalSubalgebra.range_val : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  (S : NonUnitalSubalgebra R A), NonUnitalAlgHom.range (NonUnitalSubalgebraClass.subtype S) = S
-- Mathlib.Algebra.Group.Defs
/-- A commutative additive semigroup is a type with an associative commutative `(+)`.  -/
AddCommSemigroup : Type u → Type u
-- Lean.Meta.IndPredBelow
/-- Map from proofs `h : ∀ x y z, ...` to pairs of `n` and a proof of
`h' : ∀ x y z, <nth motive> ... (h' x y z)` (nth motive corresponds to the order of motives in
the recursor). These are used to eliminate recursive calls.
 -/
Lean.Meta.IndPredBelow.RecursionContext.motives : Lean.Meta.IndPredBelow.RecursionContext → Lean.FVarIdMap (ℕ × Lean.Expr)
-- Mathlib.Data.Sum.Order
OrderIso.sumLexDualAntidistrib_inr : ∀ {α : Type u_1} {β : Type u_2} [inst : LE α] [inst_1 : LE β] (b : β),
  (OrderIso.sumLexDualAntidistrib α β) (OrderDual.toDual (Sum.inr b)) = Sum.inl (OrderDual.toDual b)
-- Mathlib.Data.Fin.VecNotation
Matrix.cons_val_two : ∀ {α : Type u} {m : ℕ} (x : α) (u : Fin m.succ.succ → α), Matrix.vecCons x u 2 = Matrix.vecHead (Matrix.vecTail u)
-- Mathlib.Dynamics.FixedPoints.Basic
/-- If `g` semiconjugates `fa` to `fb`, then it sends fixed points of `fa` to fixed points
of `fb`.  -/
Function.Semiconj.mapsTo_fixedPoints : ∀ {α : Type u_1} {β : Type u_2} {fa : α → α} {fb : β → β} {g : α → β},
  Function.Semiconj g fa fb → Set.MapsTo g (Function.fixedPoints fa) (Function.fixedPoints fb)
-- Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv
/-- A quadratic form is isometrically equivalent to its bases representations.  -/
QuadraticMap.isometryEquivBasisRepr : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_4} →
      {N : Type u_9} →
        [inst : CommSemiring R] →
          [inst_1 : AddCommMonoid M] →
            [inst_2 : AddCommMonoid N] →
              [inst_3 : Module R M] →
                [inst_4 : Module R N] →
                  [inst_5 : Finite ι] →
                    (Q : QuadraticMap R M N) → (v : Module.Basis ι R M) → Q.IsometryEquiv (Q.basisRepr v)
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithInitial.equivComma_counitIso_inv_app_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  (X : CategoryTheory.Comma (CategoryTheory.Functor.const C) (CategoryTheory.Functor.id (CategoryTheory.Functor C D))),
  (CategoryTheory.WithInitial.equivComma.counitIso.inv.app X).left = CategoryTheory.CategoryStruct.id X.left
-- Init.Data.SInt.Lemmas
Int32.toInt_add : ∀ (a b : Int32), (a + b).toInt = (a.toInt + b.toInt).bmod (2 ^ 32)
-- Mathlib.Analysis.SpecificLimits.Basic
/-- If `g` tends to `∞`, then eventually for all `x` we have `(f x / g x) * g x = f x`.  -/
Filter.EventuallyEq.div_mul_cancel_atTop : ∀ {α : Type u_4} {K : Type u_5} [inst : DivisionSemiring K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K]
  {f g : α → K} {l : Filter α}, Filter.Tendsto g l Filter.atTop → (fun x => f x / g x * g x) =ᶠ[l] fun x => f x
-- Mathlib.FieldTheory.Finite.Extension
FiniteField.finrank_zmod_extension : ∀ (k : Type u_1) [inst : Field k] [Finite k] (p : ℕ) [inst_2 : Fact (Nat.Prime p)] [inst_3 : CharP k p] (n : ℕ)
  [NeZero n] [inst_5 : Algebra (ZMod p) k],
  Module.finrank (ZMod p) (FiniteField.Extension k p n) = Module.finrank (ZMod p) k * n
-- Mathlib.NumberTheory.LegendreSymbol.AddCharacter
/-- The map associating to `a : R` the multiplicative shift of `ψ` by `a`
is injective when `ψ` is primitive.  -/
AddChar.to_mulShift_inj_of_isPrimitive : ∀ {R : Type u} [inst : CommRing R] {R' : Type v} [inst_1 : CommMonoid R'] {ψ : AddChar R R'},
  ψ.IsPrimitive → Function.Injective ψ.mulShift
-- Mathlib.Analysis.Meromorphic.Order
/-- **Alias** of `MeromorphicOn.isClopen_setOfPred_meromorphicOrderAt_eq_top`.

---

The set where a meromorphic function has infinite order is clopen in its domain of meromorphy.
 -/
MeromorphicOn.isClopen_setOf_meromorphicOrderAt_eq_top : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {U : Set 𝕜}, MeromorphicOn f U → IsClopen {u | meromorphicOrderAt f ↑u = ⊤}
-- Mathlib.Algebra.Order.Monoid.Unbundled.Pow
Right.nsmul_nonpos : ∀ {M : Type u_3} [inst : AddMonoid M] [inst_1 : Preorder M] [AddRightMono M] {x : M}, x ≤ 0 → ∀ {n : ℕ}, n • x ≤ 0
-- Mathlib.CategoryTheory.ConcreteCategory.Basic
CategoryTheory.ConcreteCategory.hom_ext_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type w}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC] {X Y : C}
  {f g : X ⟶ Y},
  f = g ↔ ∀ (x : CC X), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x
-- Mathlib.MeasureTheory.Function.Egorov
/-- Given a sequence of functions `f` and a function `g`, `notConvergentSeq f g n j` is the
set of elements such that `f k x` and `g x` are separated by at least `1 / (n + 1)` for some
`k ≥ j`.

This definition is useful for Egorov's theorem.  -/
MeasureTheory.Egorov.notConvergentSeq : {α : Type u_1} →
  {β : Type u_2} → {ι : Type u_3} → [PseudoEMetricSpace β] → [Preorder ι] → (ι → α → β) → (α → β) → ℕ → ι → Set α
-- Mathlib.GroupTheory.Nilpotent
/-- The ⊤-specialization of `lowerCentralSeries_pi_of_finite`.  -/
Subgroup.top_lowerCentralSeries_pi_of_finite : ∀ {η : Type u_2} {Gs : η → Type u_3} [inst : (i : η) → Group (Gs i)] [Finite η] (n : ℕ),
  ⊤.lowerCentralSeries n = Subgroup.pi Set.univ fun i => ⊤.lowerCentralSeries n
-- Mathlib.Condensed.Functors
/-- The functor from `CompHaus` to `Condensed.{u} (Type u)` given by the Yoneda sheaf.  -/
compHausToCondensed' : CategoryTheory.Functor CompHaus (Condensed (Type u))
-- Mathlib.Data.DFinsupp.BigOperators
DFinsupp.prod_finsetSum_index : ∀ {ι : Type u} {β : ι → Type v} [inst : DecidableEq ι] {γ : Type w} {α : Type x}
  [inst_1 : (i : ι) → AddCommMonoid (β i)] [inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] [inst_3 : CommMonoid γ]
  {s : Finset α} {g : α → Π₀ (i : ι), β i} {h : (i : ι) → β i → γ},
  (∀ (i : ι), h i 0 = 1) →
    (∀ (i : ι) (b₁ b₂ : β i), h i (b₁ + b₂) = h i b₁ * h i b₂) → ∏ i ∈ s, (g i).prod h = (∑ i ∈ s, g i).prod h
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteAddGrp.id_apply : ∀ (A : ProfiniteAddGrp.{u}) (a : ↑A.toProfinite.toTop),
  (ProfiniteAddGrp.Hom.hom (CategoryTheory.CategoryStruct.id A)) a = a
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr
Std.Tactic.BVDecide.BVExpr.Cache.Key.expr : (self : Std.Tactic.BVDecide.BVExpr.Cache.Key) → Std.Tactic.BVDecide.BVExpr self.w
-- Mathlib.Data.Fin.Parity
Fin.odd_iff_imp : ∀ {n : ℕ} {k : Fin n} [inst : NeZero n], Odd k ↔ Even n → Odd ↑k
-- Mathlib.Topology.ShrinkingLemma
/-- If `s` is a closed set, `v` is a partial refinement, and `i` is an index such that
`i ∉ v.carrier`, then there exists a partial refinement that is strictly greater than `v`.  -/
ShrinkingLemma.PartialRefinement.exists_gt : ∀ {ι : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {u : ι → Set X} {s : Set X} [NormalSpace X]
  (v : ShrinkingLemma.PartialRefinement u s ⊤), IsClosed s → ∀ i ∉ v.carrier, ∃ v', v < v'
-- Mathlib.Topology.Covering.Basic
/-- Let `f : E → X` be a (not necessarily continuous) map between topological spaces, and let
`V` be an open subset of `X`. Suppose that there is a family `U` of disjoint subsets of `E`
that covers `f⁻¹(V)` such that for every `i`,

1. `f` is injective on `Uᵢ`,
2. `V` is contained in the image `f(Uᵢ)`,
3. the open sets in `V` are determined by their preimages in `Uᵢ`.

Then `f` admits a `Bundle.Trivialization` over the base set `V`.  -/
IsOpen.trivializationDiscrete : {E : Type u_1} →
  {X : Type u_2} →
    [inst : TopologicalSpace E] →
      [inst_1 : TopologicalSpace X] →
        {f : E → X} →
          [Nonempty (X → E)] →
            {ι : Type u_3} →
              [Nonempty ι] →
                [inst_4 : TopologicalSpace ι] →
                  [DiscreteTopology ι] →
                    (U : ι → Set E) →
                      (V : Set X) →
                        IsOpen V →
                          (∀ (i : ι) {W : Set X}, W ⊆ V → (IsOpen W ↔ IsOpen (f ⁻¹' W ∩ U i))) →
                            (∀ (i : ι), Set.InjOn f (U i)) →
                              (∀ (i : ι), Set.SurjOn f (U i) V) →
                                Pairwise (Function.onFun Disjoint U) → f ⁻¹' V ⊆ ⋃ i, U i → Bundle.Trivialization ι f
-- Mathlib.LinearAlgebra.Dimension.Basic
/-- The same-universe version of `Algebra.lift_rank_eq_of_equiv_equiv`.  -/
Algebra.rank_eq_of_equiv_equiv : ∀ {R : Type w} {S : Type v} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] {R' : Type w'}
  [inst_3 : CommSemiring R'] {S' : Type v} [inst_4 : Semiring S'] [inst_5 : Algebra R' S'] (i : R ≃+* R')
  (j : S ≃+* S'),
  (algebraMap R' S').comp i.toRingHom = j.toRingHom.comp (algebraMap R S) → Module.rank R S = Module.rank R' S'
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
/-- In a canonically-ordered additive monoid, if `S'` is contained in
`(S.erase d) ∪ {d'}` and `f d' < f d` for some `d ∈ S`, then the sum of `f` over `S'` is
strictly less than over `S`.  -/
Finset.sum_lt_sum_of_subset_erase_union_singleton : ∀ {ι : Type u_9} {M : Type u_10} [inst : DecidableEq ι] [inst_1 : AddCommMonoid M] [inst_2 : PartialOrder M]
  [CanonicallyOrderedAdd M] [AddLeftStrictMono M] {S S' : Finset ι} {f : ι → M} {d d' : ι},
  d ∈ S → S' ⊆ S.erase d ∪ {d'} → f d' < f d → ∑ x ∈ S', f x < ∑ x ∈ S, f x
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
NumberField.ComplexEmbedding.IsConj.isUnramified_mk_iff : ∀ {k : Type u_1} [inst : Field k] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra k K] {σ : Gal(K/k)} {φ : K →+* ℂ},
  NumberField.ComplexEmbedding.IsConj φ σ →
    (NumberField.InfinitePlace.IsUnramified k (NumberField.InfinitePlace.mk φ) ↔ σ = 1)
-- Mathlib.Data.WSeq.Basic
_private.Mathlib.Data.WSeq.Basic.0.Stream'.WSeq.tail.aux.match_1.eq_1 : ∀ {α : Type u_1} (motive : Option (α × Stream'.WSeq α) → Sort u_2) (h_1 : Unit → motive none)
  (h_2 : (fst : α) → (s : Stream'.WSeq α) → motive (some (fst, s))),
  (match none with
    | none => h_1 ()
    | some (fst, s) => h_2 fst s) =
    h_1 ()
-- Lean.Meta.Tactic.Grind.Internalize
Lean.Meta.Grind.activateInjectiveTheorem : Lean.Meta.Grind.InjectiveTheorem → ℕ → Lean.Meta.Grind.GoalM Unit
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenAddSubgroup.instInhabited.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G], OpenAddSubgroup.instInhabited = { default := ⊤ }
-- Init.Util
/-- Returns `true` if `a` is an exclusive object.

An object is exclusive if it is single-threaded and its reference counter is 1. This function is
unsafe because it can distinguish between definitionally equal values.
 -/
isExclusiveUnsafe : {α : Type u} → α → Bool
-- Mathlib.Data.List.Range
List.getElem_range'_1 : ∀ {n m : ℕ} (i : ℕ) (H : i < (List.range' n m).length), (List.range' n m)[i] = n + i
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.getKey?_insertManyIfNewUnit_list_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α (fun x => Unit) cmp} [inst : Std.TransCmp cmp]
  {l : List α} {k : α}, k ∈ t → (Std.ExtDTreeMap.Const.insertManyIfNewUnit t l).getKey? k = t.getKey? k
-- Lean.Data.Lsp.Basic
Lean.Lsp.TextDocumentRegistrationOptions.mk.sizeOf_spec : ∀ (documentSelector? : Option Lean.Lsp.DocumentSelector),
  sizeOf { documentSelector? := documentSelector? } = 1 + sizeOf documentSelector?
-- Mathlib.NumberTheory.Padics.HeightOneSpectrum
Rat.IsIntegralClosure.intEquiv_apply_eq_ringOfIntegersEquiv : ∀ (x : NumberField.RingOfIntegers ℚ),
  (Rat.IsIntegralClosure.intEquiv (NumberField.RingOfIntegers ℚ)) x = Rat.ringOfIntegersEquiv x
-- Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
GaussianFourier.norm_cexp_neg_mul_sq_add_mul_I' : ∀ {b : ℂ},
  b.re ≠ 0 →
    ∀ (c T : ℝ),
      ‖Complex.exp (-b * (↑T + ↑c * Complex.I) ^ 2)‖ =
        Real.exp (-(b.re * (T - b.im * c / b.re) ^ 2 - c ^ 2 * (b.im ^ 2 / b.re + b.re)))
-- Init.Sym.Lemmas
Lean.Sym.UInt64.lt_eq_true : ∀ (a b : UInt64), decide (a < b) = true → (a < b) = True
-- Mathlib.LinearAlgebra.SpecialLinearGroup
rootsOfUnity.eq_one : ∀ {R : Type u_1} [inst : CommRing R] {n : ℕ} {r : ↥(rootsOfUnity n R)}, n = 1 → ↑r = 1
-- Mathlib.Analysis.Calculus.FDeriv.Basic
differentiableAt_id : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {x : E}, DifferentiableAt 𝕜 id x
-- Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset
Finset.smul_mem_smul_finset_iff₀ : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] [inst_1 : GroupWithZero α] [inst_2 : MulAction α β]
  {s : Finset β} {a : α} {b : β}, a ≠ 0 → (a • b ∈ a • s ↔ b ∈ s)
-- Init.Data.Nat.Lemmas
Nat.lt_sub_iff_add_lt : ∀ {a b c : ℕ}, a < c - b ↔ a + b < c
-- Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
SimplexCategory.δ₀Iter_zero : ∀ (n : ℕ), SimplexCategory.δ₀Iter 0 ⋯ = CategoryTheory.CategoryStruct.id { len := n }
-- Mathlib.GroupTheory.Exponent
/-- The exponent is zero iff for all nonzero `n`, one can find a `g` such that
`n • g ≠ 0`.  -/
AddMonoid.exponent_eq_zero_iff_forall : ∀ {G : Type u} [inst : AddMonoid G], AddMonoid.exponent G = 0 ↔ ∀ n > 0, ∃ g, n • g ≠ 0
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.modify : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp],
  t₁.WF → t₂.WF → t₁.Equiv t₂ → ∀ (k : α) (f : β k → β k), (t₁.modify k f).Equiv (t₂.modify k f)
-- Mathlib.Order.Filter.Pointwise
Filter.addLeftMono : ∀ {α : Type u_2} [inst : Add α], AddLeftMono (Filter α)
-- Mathlib.RingTheory.Jacobson.Ring
/-- A ring is a Jacobson ring if and only if for all prime ideals `P`,
the Jacobson radical of `P` is equal to `P`.  -/
isJacobsonRing_iff_prime_eq : ∀ {R : Type u_1} [inst : CommRing R], IsJacobsonRing R ↔ ∀ (P : Ideal R), P.IsPrime → P.jacobson = P
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
IsEllipticNet.smul : ∀ {R : Type u_1} [inst : CommRing R] {W : ℤ → R}, IsEllipticNet W → ∀ (x : R), IsEllipticNet (x • W)
-- Mathlib.Data.NNReal.Defs
NNReal.coe_le_one : ∀ {r : NNReal}, ↑r ≤ 1 ↔ r ≤ 1
-- Mathlib.Data.Ordmap.Invariants
Ordnode.splitMin'.eq_def : ∀ {α : Type u_1} (x : Ordnode α) (x_1 : α) (x_2 : Ordnode α),
  x.splitMin' x_1 x_2 =
    match x, x_1, x_2 with
    | Ordnode.nil, x, r => (x, r)
    | Ordnode.node size ll lx lr, x, r =>
      match ll.splitMin' lx lr with
      | (xm, l') => (xm, l'.balanceR x r)
-- Mathlib.MeasureTheory.VectorMeasure.WithDensityVec
MeasureTheory.VectorMeasure.withDensity_apply : ∀ {X : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G]
  [inst_5 : NormedSpace ℝ G] {μ : MeasureTheory.VectorMeasure X F} {f : X → E} {B : E →L[ℝ] F →L[ℝ] G} {s : Set X},
  μ.Integrable f → (μ.withDensity f B) s = ∫ᵛ (x : X) in s, f x ∂[B; μ]
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.Functor.Monoidal.μ_snd_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.Monoidal] (X Y : C) {Z : D} (h : F.obj Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ F X Y)
      (CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.SemiCartesianMonoidalCategory.snd X Y)) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.snd (F.obj X) (F.obj Y)) h
-- Mathlib.Analysis.Complex.Hadamard
/-- The vertical strip in the complex plane containing all `z ∈ ℂ` such that `z.re ∈ Icc a b`.  -/
Complex.HadamardThreeLines.verticalClosedStrip : ℝ → ℝ → Set ℂ
-- Mathlib.Topology.Spectral.Basic
SpectralSpace.mk : ∀ {X : Type u_3} [inst : TopologicalSpace X] [toT0Space : T0Space X] [toCompactSpace : CompactSpace X]
  [toQuasiSober : QuasiSober X] [toQuasiSeparatedSpace : QuasiSeparatedSpace X]
  [toPrespectralSpace : PrespectralSpace X], SpectralSpace X
-- Std.Data.HashMap.Raw
/-- Creates a hash map from an array of keys, associating the value `()` with each key.

This is mainly useful to implement `HashSet.ofArray`, so if you are considering using this,
`HashSet` or `HashSet.Raw` might be a better fit for you.  -/
Std.HashMap.Raw.unitOfArray : {α : Type u} → [BEq α] → [Hashable α] → Array α → Std.HashMap.Raw α Unit
-- Mathlib.Algebra.Category.BialgCat.Basic
BialgCat.toBialgHom_comp : ∀ {R : Type u} [inst : CommRing R] {X Y Z : BialgCat R} (f : X ⟶ Y) (g : Y ⟶ Z),
  BialgCat.Hom.toBialgHom (CategoryTheory.CategoryStruct.comp f g) =
    (BialgCat.Hom.toBialgHom g).comp (BialgCat.Hom.toBialgHom f)
-- Mathlib.SetTheory.Cardinal.Aleph
Ordinal.range_omega : Set.range ⇑Ordinal.omega = {x | Ordinal.omega0 ≤ x ∧ x.IsInitial}
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem!_filter : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [inst_2 : EquivBEq α]
  [inst_3 : LawfulHashable α] [inst_4 : Inhabited β] {f : α → β → Bool} {k : α} (h : m.WF),
  (Std.HashMap.Raw.filter f m)[k]! = (m[k]?.pfilter fun x h' => f (m.getKey k ⋯) x).get!
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.instPartialOrder : {R : Type u} →
  {A : Type v} →
    [inst : CommSemiring R] → [inst_1 : Semiring A] → [inst_2 : Algebra R A] → PartialOrder (Subalgebra R A)
-- Mathlib.Topology.Algebra.ContinuousAffineMap
/-- The constant map as a continuous affine map  -/
ContinuousAffineMap.const : (R : Type u_1) →
  {V : Type u_2} →
    {W : Type u_3} →
      (P : Type u_4) →
        {Q : Type u_5} →
          [inst : Ring R] →
            [inst_1 : AddCommGroup V] →
              [inst_2 : Module R V] →
                [inst_3 : TopologicalSpace P] →
                  [inst_4 : AddTorsor V P] →
                    [inst_5 : AddCommGroup W] →
                      [inst_6 : Module R W] → [inst_7 : TopologicalSpace Q] → [inst_8 : AddTorsor W Q] → Q → P →ᴬ[R] Q
-- Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
CategoryTheory.Pseudofunctor.mapComp'_inv_whiskerRight_mapComp'₀₂₃_inv_assoc : ∀ {B : Type u₁} {C : Type u₂} [inst : CategoryTheory.Bicategory B] [inst_1 : CategoryTheory.Bicategory.Strict B]
  [inst_2 : CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) {b₀ b₁ b₂ b₃ : B} (f₀₁ : b₀ ⟶ b₁)
  (f₁₂ : b₁ ⟶ b₂) (f₂₃ : b₂ ⟶ b₃) (f₀₂ : b₀ ⟶ b₂) (f₁₃ : b₁ ⟶ b₃) (f : b₀ ⟶ b₃)
  (h₀₂ : CategoryTheory.CategoryStruct.comp f₀₁ f₁₂ = f₀₂) (h₁₃ : CategoryTheory.CategoryStruct.comp f₁₂ f₂₃ = f₁₃)
  (hf : CategoryTheory.CategoryStruct.comp f₀₂ f₂₃ = f) {Z : F.obj b₀ ⟶ F.obj b₃} (h : F.map f ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerRight (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).inv (F.map f₂₃))
      (CategoryTheory.CategoryStruct.comp (F.mapComp' f₀₂ f₂₃ f ⋯).inv h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerLeft (F.map f₀₁) (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).inv)
        (CategoryTheory.CategoryStruct.comp (F.mapComp' f₀₁ f₁₃ f ⋯).inv h))
-- Mathlib.Topology.MetricSpace.IsometricSMul
dist_mul_right : ∀ {M : Type u} [inst : Mul M] [inst_1 : PseudoMetricSpace M] [IsIsometricSMul Mᵐᵒᵖ M] (a b c : M),
  dist (a * c) (b * c) = dist a b
-- Mathlib.Algebra.Group.Embedding
mulLeftEmbedding.congr_simp : ∀ {G : Type u_1} [inst : Mul G] [inst_1 : IsLeftCancelMul G] (g g_1 : G),
  g = g_1 → mulLeftEmbedding g = mulLeftEmbedding g_1
-- Init.Data.Fin.Fold
_private.Init.Data.Fin.Fold.0.Fin.foldrM_loop_zero : ∀ {m : Type u_1 → Type u_2} {n : ℕ} {α : Type u_1} [inst : Monad m] (f : Fin n → α → m α) (x : α),
  Fin.foldrM.loop✝ n f ⟨0, ⋯⟩ x = pure x
-- Mathlib.GroupTheory.Perm.DomMulAct
/-- The cardinality of the set of permutations preserving a function  -/
DomMulAct.stabilizer_ncard : ∀ {α : Type u_1} {ι : Type u_2} (f : α → ι) [Finite α] [inst : Fintype ι],
  {g | f ∘ ⇑g = f}.ncard = ∏ i, {a | f a = i}.ncard.factorial
-- Mathlib.MeasureTheory.PiSystem
/-- If a Dynkin system is closed under binary intersection, then it forms a `σ`-algebra.  -/
MeasurableSpace.DynkinSystem.toMeasurableSpace : {α : Type u_3} →
  (d : MeasurableSpace.DynkinSystem α) → (∀ (s₁ s₂ : Set α), d.Has s₁ → d.Has s₂ → d.Has (s₁ ∩ s₂)) → MeasurableSpace α
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.get?_modify_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k : α} {f : β k → β k}, (t.modify k f).get? k = Option.map f (t.get? k)
-- Mathlib.MeasureTheory.Measure.Restrict
/-- If `s` is a measurable set, then the outer measure of `t` with respect to the restriction of
the measure to `s` equals the outer measure of `t ∩ s`. This is an alternate version of
`Measure.restrict_apply`, requiring that `s` is measurable instead of `t`.  -/
MeasureTheory.Measure.restrict_apply' : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
  MeasurableSet s → (μ.restrict s) t = μ (t ∩ s)
-- Init.Data.Int.Gcd
Int.lcm_assoc : ∀ (a b c : ℤ), (↑(a.lcm b)).lcm c = a.lcm ↑(b.lcm c)
-- Mathlib.Computability.TuringMachine.ToPartrec
/-- The (finite!) set of machine states visited during the course of evaluation of `c` in
continuation `k`. This is actually closed under forward simulation (see `tr_supports`), and the
existence of this set means that the machine constructed in this section is in fact a proper
Turing machine, with a finite set of states.  -/
Turing.PartrecToTM2.codeSupp : Turing.ToPartrec.Code → Turing.PartrecToTM2.Cont' → Finset Turing.PartrecToTM2.Λ'
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.preimage_eq_empty_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] (f : MeasureTheory.SimpleFunc α β) (b : β),
  ⇑f ⁻¹' {b} = ∅ ↔ b ∉ f.range
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.prod.eq_1 : ZFSet.prod = ZFSet.pairSep fun x x_1 => True
-- Mathlib.MeasureTheory.Integral.Bochner.Set
/-- The parametric integral over a continuous function on a compact set is continuous,
under mild assumptions on the topologies involved.  -/
continuous_parametric_integral_of_continuous : ∀ {Y : Type u_2} {E : Type u_3} {X : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : MeasurableSpace Y] [OpensMeasurableSpace Y] {μ : MeasureTheory.Measure Y} [inst_4 : NormedAddCommGroup E]
  [inst_5 : NormedSpace ℝ E] [FirstCountableTopology X] [LocallyCompactSpace X] [SecondCountableTopologyEither Y E]
  [MeasureTheory.IsLocallyFiniteMeasure μ] {f : X → Y → E},
  Continuous (Function.uncurry f) → ∀ {s : Set Y}, IsCompact s → Continuous fun x => ∫ (y : Y) in s, f x y ∂μ