mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.ModelTheory.Quotients
FirstOrder.Language.quotientStructure : {L : FirstOrder.Language} → {M : Type u_1} → {s : Setoid M} → [ps : L.Prestructure s] → L.Structure (Quotient s)
-- Mathlib.SetTheory.Cardinal.UnivLE
Ordinal.univLE_of_injective : ∀ {f : Ordinal.{u} → Ordinal.{v}}, Function.Injective f → UnivLE.{u, v}
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.instMulLeftMono : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : PartialOrder β]
  [inst_3 : MulZeroClass β] [inst_4 : ContinuousMul β] [MulLeftMono β],
  MulLeftMono (CompactlySupportedContinuousMap α β)
-- Mathlib.Algebra.Field.Defs
/-- However `qsmul` is defined, it must be propositionally equal to multiplication by `Rat.cast`.

Do not use this lemma directly. Use `Rat.cast_def` instead.  -/
Field.qsmul_def : ∀ {K : Type u} [self : Field K] (a : ℚ) (x : K), Field.qsmul a x = ↑a * x
-- Std.Data.Internal.List.Associative
Std.Internal.List.DistinctKeys.def : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l ↔ List.Pairwise (fun a b => (a.fst == b.fst) = false) l
-- Mathlib.GroupTheory.GroupAction.FixingSubgroup
/-- Fixed points of iSup of submonoids is intersection  -/
fixedPoints_submonoid_iSup : ∀ (M : Type u_1) (α : Type u_2) [inst : Monoid M] [inst_1 : MulAction M α] {ι : Sort u_3} {P : ι → Submonoid M},
  MulAction.fixedPoints (↥(iSup P)) α = ⋂ i, MulAction.fixedPoints (↥(P i)) α
-- Std.Data.ExtTreeSet.Basic
/-- Tries to retrieve the smallest element that is greater than or equal to the
given element, returning `none` if no such element exists.
 -/
Std.ExtTreeSet.getGE? : {α : Type u} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtTreeSet α cmp → α → Option α
-- Lean.Linter.UnusedVariables
/-- The options set locally to this part of the syntax (used by `IgnoreFn`)  -/
Lean.Linter.UnusedVariables.FVarDefinition.opts : Lean.Linter.UnusedVariables.FVarDefinition → Lean.Options
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.memLp_re_im_iff : ∀ {α : Type u_1} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} {K : Type u_8} [inst : RCLike K]
  {f : α → K},
  MeasureTheory.MemLp (fun x => RCLike.re (f x)) p μ ∧ MeasureTheory.MemLp (fun x => RCLike.im (f x)) p μ ↔
    MeasureTheory.MemLp f p μ
-- Init.Data.Char.Basic
/-- Returns `true` if the character is a lowercase ASCII letter.

The lowercase ASCII letters are the following: `abcdefghijklmnopqrstuvwxyz`.
 -/
Char.isLower : Char → Bool
-- Mathlib.MeasureTheory.Measure.WithDensity
MeasureTheory.withDensity_zero : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}, μ.withDensity 0 = 0
-- Mathlib.Algebra.Free
/-- If `α` is a type, then `FreeMagma α` is the free magma generated by `α`.
This is a magma equipped with a function `FreeMagma.of : α → FreeMagma α` which has
the following universal property: if `M` is any magma, and `f : α → M` is any function,
then this function is the composite of `FreeMagma.of` and a unique multiplicative homomorphism
`FreeMagma.lift f : FreeMagma α →ₙ* M`.

A typical element of `FreeMagma α` is a formal non-associative product of
elements of `α`. For example if `x` and `y` are terms of type `α` then `x * ((y * y) * x)` is a
"typical" element of `FreeMagma α`.
One can think of `FreeMagma α` as the type of binary trees with leaves labelled by `α`.
In general, no pair of distinct elements in `FreeMagma α` will commute.
 -/
FreeMagma : Type u → Type u
-- Mathlib.Data.WSeq.Defs
/-- Get the index of the first element of `s` satisfying `p`  -/
Stream'.WSeq.findIndex : {α : Type u} → (p : α → Prop) → [DecidablePred p] → Stream'.WSeq α → Computation ℕ
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.TakeWhile
Std.IterM.step_takeWhile : ∀ {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [inst : Monad m] [LawfulMonad m] [inst_2 : Std.Iterator α m β]
  {it : Std.IterM m β} {P : β → Bool},
  (Std.IterM.takeWhile P it).step = do
    let __do_lift ← it.step
    match __do_lift.inflate with
      | ⟨Std.IterStep.yield it' out, h⟩ =>
        match hP : P out with
        | true => pure (Std.Shrink.deflate (Std.PlausibleIterStep.yield (Std.IterM.takeWhile P it') out ⋯))
        | false => pure (Std.Shrink.deflate (Std.PlausibleIterStep.done ⋯))
      | ⟨Std.IterStep.skip it', h⟩ =>
        pure (Std.Shrink.deflate (Std.PlausibleIterStep.skip (Std.IterM.takeWhile P it') ⋯))
      | ⟨Std.IterStep.done, h⟩ => pure (Std.Shrink.deflate (Std.PlausibleIterStep.done ⋯))
-- Lean.Level
Lean.Level.PP.Result.offset : Lean.Level.PP.Result → ℕ → Lean.Level.PP.Result
-- Init.Data.Vector.Lemmas
Vector.any_iff_exists : ∀ {α : Type u_1} {n : ℕ} {p : α → Bool} {xs : Vector α n}, xs.any p = true ↔ ∃ i, ∃ (x : i < n), p xs[i] = true
-- Lean.Elab.InfoTree.Types
Lean.Elab.Info.ofMacroExpansionInfo.injEq : ∀ (i i_1 : Lean.Elab.MacroExpansionInfo),
  (Lean.Elab.Info.ofMacroExpansionInfo i = Lean.Elab.Info.ofMacroExpansionInfo i_1) = (i = i_1)
-- Mathlib.Combinatorics.Enumerative.Partition.Basic
Nat.Partition.ofSym_map : ∀ {n : ℕ} {σ : Type u_1} {τ : Type u_2} [inst : DecidableEq σ] [inst_1 : DecidableEq τ] (e : σ ≃ τ) (s : Sym σ n),
  Nat.Partition.ofSym (Sym.map (⇑e) s) = Nat.Partition.ofSym s
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.zero.eq_1 : ∀ {α : Type u_2} [inst : Zero α], Set.zero = { zero := {0} }
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
/-- **Fundamental theorem of calculus-1**, strict differentiability in both endpoints.

If `f : ℝ → E` is integrable on `a..b` and `f x` has finite limits `ca` and `cb` almost surely as
`x` tends to `a` and `b`, respectively, then
`(u, v) ↦ ∫ x in u..v, f x` has derivative `(u, v) ↦ v • cb - u • ca` at `(a, b)`
in the sense of strict differentiability.  -/
intervalIntegral.integral_hasStrictFDerivAt_of_tendsto_ae : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E} {ca cb : E}
  {a b : ℝ},
  IntervalIntegrable f MeasureTheory.volume a b →
    StronglyMeasurableAtFilter f (nhds a) MeasureTheory.volume →
      StronglyMeasurableAtFilter f (nhds b) MeasureTheory.volume →
        Filter.Tendsto f (nhds a ⊓ MeasureTheory.ae MeasureTheory.volume) (nhds ca) →
          Filter.Tendsto f (nhds b ⊓ MeasureTheory.ae MeasureTheory.volume) (nhds cb) →
            HasStrictFDerivAt (fun p => ∫ (x : ℝ) in p.1..p.2, f x)
              ((ContinuousLinearMap.snd ℝ ℝ ℝ).smulRight cb - (ContinuousLinearMap.fst ℝ ℝ ℝ).smulRight ca) (a, b)
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
_private.Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk.0.SzemerediRegularity.one_sub_eps_mul_card_nonuniformWitness_le_card_star : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {P : Finpartition Finset.univ} {hP : P.IsEquipartition}
  {G : SimpleGraph α} [inst_2 : DecidableRel G.Adj] {ε : ℝ} {U : Finset α} {hU : U ∈ P.parts} {V : Finset α},
  V ∈ P.parts →
    U ≠ V →
      ¬G.IsUniform ε U V →
        100 ≤ 4 ^ P.parts.card * ε ^ 5 →
          ε ≤ 1 →
            (1 - ε / 10) * ↑(G.nonuniformWitness ε U V).card ≤ ↑((SzemerediRegularity.star hP G ε hU V).biUnion id).card
-- Mathlib.Topology.MetricSpace.BundledFun
PseudoMetric.finsetSup_apply : ∀ {X : Type u_1} {R : Type u_2} [inst : AddCommMonoid R] [inst_1 : LinearOrder R] [inst_2 : AddLeftStrictMono R]
  [inst_3 : IsOrderedAddMonoid R] {Y : Type u_3} {f : Y → PseudoMetric X R} {s : Finset Y} (hs : s.Nonempty) (x y : X),
  (s.sup f) x y = s.sup' hs fun i => (f i) x y
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey?_diff : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  (t₁ \ t₂).getKey? k = if k ∈ t₂ then none else t₁.getKey? k
-- Mathlib.NumberTheory.ClassNumber.AdmissibleAbs
AbsoluteValue.instInhabitedIsAdmissibleIntAbs : Inhabited AbsoluteValue.abs.IsAdmissible
-- Init.Data.Float.Model.Unpacked.Round
Float.Model.UnpackedFloat.ExtendedMantissa.mk.sizeOf_spec : ∀ (mantissa : ℕ) (roundBit stickyBit : Bool),
  sizeOf { mantissa := mantissa, roundBit := roundBit, stickyBit := stickyBit } =
    1 + sizeOf mantissa + sizeOf roundBit + sizeOf stickyBit
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.inverseImage_op_overObj : ∀ {T : Type u_3} [inst : CategoryTheory.Category.{v_3, u_3} T] (W : CategoryTheory.MorphismProperty T) {X : T},
  W.overObj.op.inverseImage (CategoryTheory.Under.opEquivOpOver X).functor = W.op.underObj
-- Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar
/-- If `φ : A ≃ₜ+ A` then `addEquivAddHaarChar φ` is the positive
real factor by which `φ` scales Haar measures on `A`.  -/
MeasureTheory.addEquivAddHaarChar : {G : Type u_1} →
  [inst : AddGroup G] →
    [inst_1 : TopologicalSpace G] →
      [inst_2 : MeasurableSpace G] →
        [BorelSpace G] → [IsTopologicalAddGroup G] → [LocallyCompactSpace G] → G ≃ₜ+ G → NNReal
-- Mathlib.Probability.Distributions.Gaussian.Fernique
/-- **Alias** of `ProbabilityTheory.IsGaussian.nullSingletonClass`.

---

If a Gaussian measure is not a Dirac, then it has value zero on singletons.  -/
ProbabilityTheory.IsGaussian.noAtoms : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E]
  {μ : MeasureTheory.Measure E} [ProbabilityTheory.IsGaussian μ] [CompleteSpace E] [SecondCountableTopology E],
  (∀ (x : E), μ ≠ MeasureTheory.Measure.dirac x) → MeasureTheory.NullSingletonClass μ
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapComp_hom_τl : ∀ {a b c : CategoryTheory.LocallyDiscrete AlgebraicGeometry.Schemeᵒᵖ} (x : a ⟶ b) (x_1 : b ⟶ c),
  (AlgebraicGeometry.Scheme.Modules.pseudofunctor.mapComp x x_1).hom.τl =
    CategoryTheory.NatTrans.toCatHom₂ (AlgebraicGeometry.Scheme.Modules.pullbackComp x_1.as.unop x.as.unop).inv
-- Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic
/-- The linear polynomial $$\sum_i c_i X_i$$.  -/
MvPolynomial.sumSMulX : {n : Type u_1} → {R : Type u_2} → [inst : CommRing R] → (n →₀ R) →ₗ[R] MvPolynomial n R
-- Mathlib.Analysis.Meromorphic.NormalForm
/-- A product of meromorphic functions in normal form is in normal form if at most one of the factors
vanishes.
 -/
meromorphicNFAt_prod : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {ι : Type u_3} {s : Finset ι} {f : ι → 𝕜 → 𝕜},
  (∀ i ∈ s, MeromorphicNFAt (f i) x) → {σ | σ ∈ s ∧ f σ x = 0}.Subsingleton → MeromorphicNFAt (∏ i ∈ s, f i) x
-- Init.Prelude
/-- Adds an element to the *end* of a list.

The added element is the last element of the resulting list.

Examples:
* `List.concat ["red", "yellow"] "green" = ["red", "yellow", "green"]`
* `List.concat [1, 2, 3] 4 = [1, 2, 3, 4]`
* `List.concat [] () = [()]`
 -/
List.concat : {α : Type u} → List α → α → List α
-- Init.Core
/-- `ReflBEq α` says that the `BEq` implementation is reflexive.  -/
ReflBEq : (α : Type u_1) → [BEq α] → Prop
-- Mathlib.Algebra.Polynomial.Laurent
LaurentPolynomial.«term_[T;T⁻¹]» : Lean.TrailingParserDescr
-- Mathlib.Analysis.Calculus.Deriv.Basic
fderiv_eq_smul_deriv : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {x : 𝕜} (y : 𝕜), (fderiv 𝕜 f x) y = y • deriv f x
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.Lp.edist_def : ∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] (f g : ↥(MeasureTheory.Lp E p μ)), edist f g = MeasureTheory.eLpNorm (↑↑f - ↑↑g) p μ
-- Mathlib.LinearAlgebra.PiTensorProduct.Finite
PiTensorProduct.finite : ∀ {R : Type u_1} [inst : CommRing R] {ι : Type u_2} [Finite ι] {M : ι → Type u_3}
  [inst_2 : (i : ι) → AddCommGroup (M i)] [inst_3 : (i : ι) → Module R (M i)] [∀ (i : ι), Module.Finite R (M i)],
  Module.Finite R (PiTensorProduct R fun i => M i)
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.Algebra.hom_ext : ∀ {R : Type u_1} {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6}
  {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)]
  [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι] [inst_4 : CommSemiring R]
  [inst_5 : (i : ι) → Semiring (G i)] [inst_6 : (i : ι) → Algebra R (G i)]
  [inst_7 : ∀ (i j : ι) (h : i ≤ j), AlgHomClass (T h) R (G i) (G j)] [inst_8 : Nonempty ι] (P : Type u_7)
  [inst_9 : Semiring P] [inst_10 : Algebra R P] {g₁ g₂ : DirectLimit G f →ₐ[R] P},
  (∀ (i : ι), g₁.comp (DirectLimit.Algebra.of G f i) = g₂.comp (DirectLimit.Algebra.of G f i)) → g₁ = g₂
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.getKey!_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α fun x => Unit} [EquivBEq α] [LawfulHashable α]
  [inst : Inhabited α] {l : List α} {k : α},
  k ∉ m → l.contains k = false → (Std.DHashMap.Const.insertManyIfNewUnit m l).getKey! k = default
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
mabs_le_mabs_of_one_le : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : Group α] {a b : α} [MulLeftMono α], 1 ≤ a → a ≤ b → |a|ₘ ≤ |b|ₘ
-- Mathlib.MeasureTheory.OuterMeasure.Operations
MeasureTheory.OuterMeasure.instIsZeroApplySetENNReal : ∀ {α : Type u_1}, IsZeroApply (MeasureTheory.OuterMeasure α) (Set α) ENNReal
-- Mathlib.Algebra.GroupWithZero.Associated
prime_mul_iff : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] [IsCancelMulZero M] {x y : M},
  Prime (x * y) ↔ Prime x ∧ IsUnit y ∨ IsUnit x ∧ Prime y
-- Mathlib.LinearAlgebra.Alternating.Basic
/-- The multilinear map associated to an alternating map  -/
AlternatingMap.toMultilinearMap : {R : Type u_1} →
  [inst : Semiring R] →
    {M : Type u_2} →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] →
          {N : Type u_3} →
            [inst_3 : AddCommMonoid N] →
              [inst_4 : Module R N] → {ι : Type u_7} → M [⋀^ι]→ₗ[R] N → MultilinearMap R (fun x => M) N
-- Std.Tactic.BVDecide.Bitblast.BoolExpr.Basic
Std.Tactic.BVDecide.BoolExpr.eval_ite : ∀ {α : Type} {a : α → Bool} {d l r : Std.Tactic.BVDecide.BoolExpr α},
  Std.Tactic.BVDecide.BoolExpr.eval a (d.ite l r) =
    bif Std.Tactic.BVDecide.BoolExpr.eval a d then Std.Tactic.BVDecide.BoolExpr.eval a l
    else Std.Tactic.BVDecide.BoolExpr.eval a r
-- Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
_private.Mathlib.Combinatorics.SimpleGraph.Walk.Traversal.0.SimpleGraph.Walk.getVert.match_1.eq_3 : ∀ {V : Type u_1} {G : SimpleGraph V} {u : V} (motive : (v : V) → G.Walk u v → ℕ → Sort u_2) (v v_1 : V)
  (h : G.Adj u v_1) (q : G.Walk v_1 v) (n : ℕ) (h_1 : (x : ℕ) → motive u SimpleGraph.Walk.nil x)
  (h_2 : (v v_2 : V) → (h : G.Adj u v_2) → (p : G.Walk v_2 v) → motive v (SimpleGraph.Walk.cons h p) 0)
  (h_3 : (v v_2 : V) → (h : G.Adj u v_2) → (q : G.Walk v_2 v) → (n : ℕ) → motive v (SimpleGraph.Walk.cons h q) n.succ),
  (match v, SimpleGraph.Walk.cons h q, n.succ with
    | .(u), SimpleGraph.Walk.nil, x => h_1 x
    | v, SimpleGraph.Walk.cons h p, 0 => h_2 v v_2 h p
    | v, SimpleGraph.Walk.cons h q, n.succ => h_3 v v_2 h q n) =
    h_3 v v_1 h q n
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.indep_iff_forall_closure_sdiff_ne : ∀ {α : Type u_2} {M : Matroid α} {I : Set α}, M.Indep I ↔ ∀ ⦃e : α⦄, e ∈ I → M.closure (I \ {e}) ≠ M.closure I
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafMap_comp : ∀ {C₀ : Type u₀} {C : Type u} [inst : CategoryTheory.Category.{v₀, u₀} C₀] [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor C₀ C} {J₀ : CategoryTheory.GrothendieckTopology C₀}
  {J : CategoryTheory.GrothendieckTopology C} {A : Type u'} [inst_2 : CategoryTheory.Category.{v', u'} A]
  [inst_3 : CategoryTheory.Functor.IsDenseSubsite J₀ J F] (data : (X : C) → F.OneHypercoverDenseData J₀ J X)
  [inst_4 : CategoryTheory.Limits.HasLimitsOfSize.{w, w, v', u'} A] (G₀ : CategoryTheory.Sheaf J₀ A) {X Y Z : C}
  (f : X ⟶ Y) (g : Y ⟶ Z),
  CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafMap data G₀ (CategoryTheory.CategoryStruct.comp f g) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafMap data G₀ g)
      (CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafMap data G₀ f)
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.EqCnstrProof.erase0_rhs.sizeOf_spec : ∀ (c : Lean.Meta.Grind.AC.EqCnstr), sizeOf (Lean.Meta.Grind.AC.EqCnstrProof.erase0_rhs c) = 1 + sizeOf c
-- Mathlib.Order.Defs.Unbundled
/-- Local notation for an arbitrary binary relation `r`.  -/
_private.Mathlib.Order.Defs.Unbundled.0.«term_≺_» : Lean.TrailingParserDescr
-- Mathlib.CategoryTheory.Preadditive.Biproducts
CategoryTheory.Limits.BinaryBicone.ofColimitCocone_inl : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {X Y : C}
  {t : CategoryTheory.Limits.Cocone (CategoryTheory.Limits.pair X Y)} (ht : CategoryTheory.Limits.IsColimit t),
  (CategoryTheory.Limits.BinaryBicone.ofColimitCocone ht).inl = t.ι.app { as := CategoryTheory.Limits.WalkingPair.left }
-- Mathlib.Topology.Sets.VietorisTopology
/-- Auxiliary lemma showing that singleton sets form a closed set. It takes the required topological
properties as arguments, so that it applies to both the Vietoris topology and the Hausdorff
uniformity.  -/
TopologicalSpace.isClosed_range_singleton : ∀ {α : Type u_1} [inst : TopologicalSpace α] [T2Space α] {t : TopologicalSpace (Set α)},
  IsOpen {∅} → (∀ {U : Set α}, IsOpen U → IsOpen {s | (s ∩ U).Nonempty}) → IsClosed (Set.range fun x => {x})
-- Mathlib.MeasureTheory.Measure.Regular
MeasureTheory.Measure.InnerRegularWRT.of_imp : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {p q : Set α → Prop},
  (∀ (s : Set α), q s → p s) → μ.InnerRegularWRT p q
-- Mathlib.GroupTheory.Complement
Subgroup.isComplement'_bot_top : ∀ {G : Type u_1} [inst : Group G], ⊥.IsComplement' ⊤
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.getPPAnalyzeTrustSubst : Lean.Options → Bool
-- Mathlib.Algebra.AlgebraicCard
Algebraic.countable : ∀ (R : Type u) (A : Type v) [inst : CommRing R] [IsDomain R] [inst_2 : CommRing A] [IsDomain A] [inst_4 : Algebra R A]
  [Module.IsTorsionFree R A] [Countable R], {x | IsAlgebraic R x}.Countable
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
/-- `LinearMap.lTensor` as a continuous linear map, i.e. the continuous linear map `g` extended to
the map `x ⊗ₜ[𝕜] y ↦ x ⊗ₜ[𝕜] g(y)`.  -/
ContinuousLinearMap.lTensor : {𝕜 : Type u_1} →
  {E : Type u_2} →
    {F : Type u_3} →
      (G : Type u_4) →
        [inst : RCLike 𝕜] →
          [inst_1 : NormedAddCommGroup E] →
            [inst_2 : InnerProductSpace 𝕜 E] →
              [inst_3 : NormedAddCommGroup F] →
                [inst_4 : InnerProductSpace 𝕜 F] →
                  [inst_5 : NormedAddCommGroup G] →
                    [inst_6 : InnerProductSpace 𝕜 G] → (E →L[𝕜] F) → TensorProduct 𝕜 G E →L[𝕜] TensorProduct 𝕜 G F
-- Mathlib.Order.Circular
btw_rfl_right : ∀ {α : Type u_1} [inst : CircularOrder α] {a b : α}, btw a b b
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Cpop
Std.Tactic.BVDecide.BVExpr.bitblast.blastCpopTreeTarget.len : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {aig : Std.Sat.AIG α} → {w : ℕ} → Std.Tactic.BVDecide.BVExpr.bitblast.blastCpopTreeTarget aig w → ℕ
-- Mathlib.Probability.Kernel.Posterior
/-- The main property of the posterior, as equality of the following diagrams:
```
         -- id          -- κ
μ -- κ -|        =  μ -|
         -- κ†μ         -- id
```  -/
ProbabilityTheory.parallelProd_posterior_comp_copy_comp : ∀ {Ω : Type u_1} {𝓧 : Type u_2} {mΩ : MeasurableSpace Ω} {m𝓧 : MeasurableSpace 𝓧} {κ : ProbabilityTheory.Kernel Ω 𝓧}
  {μ : MeasureTheory.Measure Ω} [inst : MeasureTheory.IsFiniteMeasure μ] [inst_1 : ProbabilityTheory.IsFiniteKernel κ]
  [inst_2 : StandardBorelSpace Ω] [inst_3 : Nonempty Ω],
  ((μ.bind ⇑κ).bind ⇑(ProbabilityTheory.Kernel.copy 𝓧)).bind
      ⇑(ProbabilityTheory.Kernel.id.parallelComp (ProbabilityTheory.posterior κ μ)) =
    (μ.bind ⇑(ProbabilityTheory.Kernel.copy Ω)).bind ⇑(κ.parallelComp ProbabilityTheory.Kernel.id)
-- Batteries.Data.AssocList
_private.Batteries.Data.AssocList.0.List.toAssocList.match_1.eq_1 : ∀ {α : Type u_2} {β : Type u_1} (motive : List (α × β) → Sort u_3) (h_1 : Unit → motive [])
  (h_2 : (a : α) → (b : β) → (es : List (α × β)) → motive ((a, b) :: es)),
  (match [] with
    | [] => h_1 ()
    | (a, b) :: es => h_2 a b es) =
    h_1 ()
-- Init.Data.Int.Bitwise.Lemmas
Int.shiftLeft_add : ∀ (a : ℤ) (b c : ℕ), a <<< (b + c) = a <<< b <<< c
-- Mathlib.Order.Filter.Extr
/-- If `f` is antitone on `Iic b` and monotone on `Ici b`, then the minimum of `f` is attained
at `b`.  -/
isMinOn_univ_of_anti_mono : ∀ {α : Type u} {β : Type u_1} [inst : LinearOrder α] [inst_1 : Preorder β] {b : α} {f : α → β},
  AntitoneOn f (Set.Iic b) → MonotoneOn f (Set.Ici b) → IsMinOn f Set.univ b
-- Mathlib.Topology.Category.TopCat.Limits.Pullbacks
/-- If the map `S ⟶ T` is mono, then there is a description of the image of `W ×ₛ X ⟶ Y ×ₜ Z`.  -/
TopCat.range_pullback_map : ∀ {W X Y Z S T : TopCat} (f₁ : W ⟶ S) (f₂ : X ⟶ S) (g₁ : Y ⟶ T) (g₂ : Z ⟶ T) (i₁ : W ⟶ Y) (i₂ : X ⟶ Z) (i₃ : S ⟶ T)
  [H₃ : CategoryTheory.Mono i₃]
  (eq₁ : CategoryTheory.CategoryStruct.comp f₁ i₃ = CategoryTheory.CategoryStruct.comp i₁ g₁)
  (eq₂ : CategoryTheory.CategoryStruct.comp f₂ i₃ = CategoryTheory.CategoryStruct.comp i₂ g₂),
  Set.range ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂)) =
    ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pullback.fst g₁ g₂)) ⁻¹'
        Set.range ⇑(CategoryTheory.ConcreteCategory.hom i₁) ∩
      ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pullback.snd g₁ g₂)) ⁻¹'
        Set.range ⇑(CategoryTheory.ConcreteCategory.hom i₂)
-- Mathlib.Computability.TuringMachine.Config
_private.Mathlib.Computability.TuringMachine.Config.0.Turing.ToPartrec.Code.eval.match_1.eq_7 : ∀ (motive : Turing.ToPartrec.Code → Sort u_1) (f : Turing.ToPartrec.Code)
  (h_1 : Unit → motive Turing.ToPartrec.Code.zero') (h_2 : Unit → motive Turing.ToPartrec.Code.succ)
  (h_3 : Unit → motive Turing.ToPartrec.Code.tail) (h_4 : (f fs : Turing.ToPartrec.Code) → motive (f.cons fs))
  (h_5 : (f g : Turing.ToPartrec.Code) → motive (f.comp g)) (h_6 : (f g : Turing.ToPartrec.Code) → motive (f.case g))
  (h_7 : (f : Turing.ToPartrec.Code) → motive f.fix),
  (match f.fix with
    | Turing.ToPartrec.Code.zero' => h_1 ()
    | Turing.ToPartrec.Code.succ => h_2 ()
    | Turing.ToPartrec.Code.tail => h_3 ()
    | f.cons fs => h_4 f fs
    | f.comp g => h_5 f g
    | f.case g => h_6 f g
    | f.fix => h_7 f) =
    h_7 f
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax
CategoryTheory.Lax.OplaxTrans.vComp_naturality_naturality : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G H : CategoryTheory.LaxFunctor B C} (η : CategoryTheory.Lax.OplaxTrans F G)
  (θ : CategoryTheory.Lax.OplaxTrans G H) {a b : B} {f g : a ⟶ b} (β : f ⟶ g),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.map₂ β) (η.vCompApp θ b))
      (η.vCompNaturality θ g) =
    CategoryTheory.CategoryStruct.comp (η.vCompNaturality θ f)
      (CategoryTheory.Bicategory.whiskerLeft (η.vCompApp θ a) (H.map₂ β))
-- Plausible.Testable
/-- Execute `cmd` and repeat every time the result is `gaveUp` (at most `n` times).  -/
Plausible.retry : {p : Prop} → Plausible.Gen (Plausible.TestResult p) → ℕ → Plausible.Gen (Plausible.TestResult p)
-- Init.Data.BitVec.Lemmas
BitVec.slt_eq_sle_and_ne : ∀ {w : ℕ} {x y : BitVec w}, x.slt y = (x.sle y && x != y)
-- Mathlib.CategoryTheory.Localization.Construction
CategoryTheory.Localization.Construction.LocQuiver.mk.injEq : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] {W : CategoryTheory.MorphismProperty C} (obj obj_1 : C),
  ({ obj := obj } = { obj := obj_1 }) = (obj = obj_1)