mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Lie.Derivation.Basic
LieDerivation.inner_apply_apply : ∀ (R : Type u_1) (L : Type u_2) (M : Type u_3) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M] (m : M)
  (m_1 : L), ((LieDerivation.inner R L M) m) m_1 = ⁅m_1, m⁆
-- Mathlib.AlgebraicGeometry.Morphisms.LocalClosure
AlgebraicGeometry.sourceLocalClosure.le : ∀ {W P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [W.ContainsIdentities] [W.RespectsIso],
  P ≤ AlgebraicGeometry.sourceLocalClosure W P
-- Init.Data.Vector.Lemmas
Vector.back_mk : ∀ {n : ℕ} {α : Type u_1} [inst : NeZero n] {xs : Array α} (h : xs.size = n), (Vector.mk xs h).back = xs.back ⋯
-- Lean.Elab.PreDefinition.TerminationHint
Lean.Elab.TerminationHints.terminationBy?? : Lean.Elab.TerminationHints → Option Lean.Syntax
-- Mathlib.ModelTheory.Skolem
/-- The **Downward Löwenheim–Skolem theorem** :
If `s` is a set in an `L`-structure `M` and `κ` an infinite cardinal such that
`max (#s, L.card) ≤ κ` and `κ ≤ # M`, then `M` has an elementary substructure containing `s` of
cardinality `κ`.  -/
FirstOrder.Language.exists_elementarySubstructure_card_eq : ∀ (L : FirstOrder.Language) {M : Type w} [inst : L.Structure M] (s : Set M) (κ : Cardinal.{w'}),
  Cardinal.aleph0 ≤ κ →
    Cardinal.lift.{w', w} (Cardinal.mk ↑s) ≤ Cardinal.lift.{w, w'} κ →
      Cardinal.lift.{w', max u v} L.card ≤ Cardinal.lift.{max u v, w'} κ →
        Cardinal.lift.{w, w'} κ ≤ Cardinal.lift.{w', w} (Cardinal.mk M) →
          ∃ S, s ⊆ ↑S ∧ Cardinal.lift.{w', w} (Cardinal.mk ↥S) = Cardinal.lift.{w, w'} κ
-- Mathlib.RingTheory.IsAdjoinRoot
/-- Unicity of `liftHom`: a map that agrees on `h.root` agrees with `liftHom` everywhere.  -/
IsAdjoinRoot.eq_liftHom : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] {f : Polynomial R} [inst_2 : Algebra R S]
  (h : IsAdjoinRoot S f) {T : Type u_1} [inst_3 : CommRing T] {x : T} [inst_4 : Algebra R T]
  (hx' : (Polynomial.aeval x) f = 0) (g : S →ₐ[R] T), g h.root = x → g = h.liftHom x hx'
-- Mathlib.Data.Seq.Parallel
Computation.exists_of_mem_parallel : ∀ {α : Type u} {S : Stream'.WSeq (Computation α)} {a : α}, a ∈ Computation.parallel S → ∃ c ∈ S, a ∈ c
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.isLongestRevMatchAt_iff : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice} {pos₁ pos₂ : s.Pos},
  String.Slice.Pattern.Model.IsLongestRevMatchAt pat pos₁ pos₂ ↔
    ∃ (h : pos₁ ≤ pos₂), String.Slice.Pattern.Model.IsLongestRevMatch pat (pos₂.sliceTo pos₁ h)
-- Mathlib.ModelTheory.Syntax
/-- Puts an `∃` quantifier on a bounded formula.  -/
FirstOrder.Language.BoundedFormula.ex : {L : FirstOrder.Language} → {α : Type u'} → {n : ℕ} → L.BoundedFormula α (n + 1) → L.BoundedFormula α n
-- Mathlib.Analysis.Normed.Group.Defs
/-- Construct a seminormed group from a translation-invariant distance.  -/
SeminormedAddGroup.ofAddDist : {E : Type u_5} →
  [inst : Norm E] →
    [inst_1 : AddGroup E] →
      [inst_2 : PseudoMetricSpace E] →
        (∀ (x : E), ‖x‖ = dist 0 x) → (∀ (x y z : E), dist x y ≤ dist (z + x) (z + y)) → SeminormedAddGroup E
-- Mathlib.Algebra.Opposites
MulOpposite.isLeftCancelAdd_iff : ∀ {α : Type u_1} [inst : Add α], IsLeftCancelAdd αᵐᵒᵖ ↔ IsLeftCancelAdd α
-- Mathlib.Data.Nat.Find
_private.Mathlib.Data.Nat.Find.0.Nat.findGreatest.match_1.splitter : (motive : ℕ → Sort u_1) → (x : ℕ) → (Unit → motive 0) → ((n : ℕ) → motive n.succ) → motive x
-- Lean.Server.Snapshots
Lean.Server.Snapshots.Snapshot.msgLog : Lean.Server.Snapshots.Snapshot → Lean.MessageLog
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometry.coe_toContinuousAffineMap : ∀ {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [inst : NormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup V] [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P]
  [inst_4 : NormedAddTorsor V P] [inst_5 : SeminormedAddCommGroup V₂] [inst_6 : NormedSpace 𝕜 V₂]
  [inst_7 : PseudoMetricSpace P₂] [inst_8 : NormedAddTorsor V₂ P₂] (f : P →ᵃⁱ[𝕜] P₂), ⇑f.toContinuousAffineMap = ⇑f
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.sub_empty : ∀ {α : Type u_2} [inst : Sub α] {s : Set α}, s - ∅ = ∅
-- Mathlib.Probability.Kernel.Integral
ProbabilityTheory.Kernel.integral_const : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {E : Type u_3}
  [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : β → E} {a : α} {μ : MeasureTheory.Measure β},
  ∫ (x : β), f x ∂(ProbabilityTheory.Kernel.const α μ) a = ∫ (x : β), f x ∂μ
-- Std.Data.DTreeMap.Internal.Balancing
Std.DTreeMap.Internal.Impl.rotateL.eq_def : ∀ {α : Type u} {β : α → Type v} (k : α) (v : β k) (l : Std.DTreeMap.Internal.Impl α β) (rk : α) (rv : β rk)
  (rl rr : Std.DTreeMap.Internal.Impl α β),
  Std.DTreeMap.Internal.Impl.rotateL k v l rk rv rl rr =
    if rl.size < Std.DTreeMap.Internal.ratio * rr.size then Std.DTreeMap.Internal.Impl.singleL k v l rk rv rl rr
    else
      match rl with
      | Std.DTreeMap.Internal.Impl.leaf => Std.DTreeMap.Internal.Impl.singleL k v l rk rv rl rr
      | Std.DTreeMap.Internal.Impl.inner size rlk rlv rll rlr =>
        Std.DTreeMap.Internal.Impl.doubleL k v l rk rv rlk rlv rll rlr rr
-- Lean.Elab.Tactic.Simp
Lean.Elab.Tactic.tactic.simp.trace : Lean.Option Bool
-- Mathlib.GroupTheory.CoprodI
/-- One can multiply an element from the left to a non-empty reduced word if it does not cancel
with the first element in the word.  -/
Monoid.CoprodI.NeWord.mulHead : {ι : Type u_1} →
  {M : ι → Type u_2} →
    [inst : (i : ι) → Monoid (M i)] →
      {i j : ι} → (w : Monoid.CoprodI.NeWord M i j) → (x : M i) → x * w.head ≠ 1 → Monoid.CoprodI.NeWord M i j
-- Mathlib.CategoryTheory.Shift.Adjunction
CategoryTheory.Adjunction.LeftAdjointCommShift.iso'.eq_1 : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  (adj : F ⊣ G) {A : Type u_3} [inst_2 : AddGroup A] [inst_3 : CategoryTheory.HasShift C A]
  [inst_4 : CategoryTheory.HasShift D A] (a b : A) (h : a + b = 0) [inst_5 : G.CommShift A],
  CategoryTheory.Adjunction.LeftAdjointCommShift.iso' adj a b h =
    (CategoryTheory.conjugateIsoEquiv (adj.comp (CategoryTheory.shiftEquiv' D a b h).toAdjunction)
          ((CategoryTheory.shiftEquiv' C a b h).toAdjunction.comp adj)).invFun
      (CategoryTheory.Functor.commShiftIso G b)
-- Std.Time.Zoned.ZoneRules
Std.Time.TimeZone.UTLocal.noConfusionType : Sort v✝ → Std.Time.TimeZone.UTLocal → Std.Time.TimeZone.UTLocal → Sort v✝
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.mapShortComplexH2_id : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A : Rep.{u, u, u} k G},
  groupHomology.mapShortComplexH2 (MonoidHom.id G) (CategoryTheory.CategoryStruct.id A) =
    CategoryTheory.CategoryStruct.id (groupHomology.shortComplexH2 A)
-- Mathlib.Order.UpperLower.Basic
IsUpperSet.bot_mem : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α} [inst_1 : OrderBot α], IsUpperSet s → (⊥ ∈ s ↔ s = Set.univ)
-- Mathlib.Order.Filter.ENNReal
NNReal.isBoundedUnder_le_toReal : ∀ {ι : Type u_1} {f : Filter ι} {u : ι → NNReal},
  (Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f fun i => ↑(u i)) ↔ Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
NumberField.InfinitePlace.mk_embedding : ∀ {K : Type u_1} [inst : Field K] (w : NumberField.InfinitePlace K), NumberField.InfinitePlace.mk w.embedding = w
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.maxKey?_eq_back?_keysArray : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → t.maxKey? = t.keysArray.back?
-- Mathlib.Data.Set.Finite.Basic
/-- `Finset` version of `Set.SurjOn.exists_subset_injOn_image_eq`.  -/
Finset.exists_subset_injOn_image_eq_of_surjOn : ∀ {α : Type u} {β : Type v} [inst : DecidableEq β] {f : α → β} (s : Set α) (t : Finset β),
  Set.SurjOn f s ↑t → ∃ u, ↑u ⊆ s ∧ Set.InjOn f ↑u ∧ Finset.image f u = t
-- Mathlib.Data.Sym.Basic
Sym.eq_1 : ∀ (α : Type u_1) (n : ℕ), Sym α n = { s // s.card = n }
-- Init.Data.Order.Lemmas
Std.instLawfulOrderLeftLeaningMin : ∀ {α : Type u_1} [inst : LE α] [inst_1 : DecidableLE α], Std.LawfulOrderLeftLeaningMin α
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated
SSet.Truncated.Edge.mk.inj : ∀ {X : SSet.Truncated 2} {x₀ x₁ : X.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge._proof_1 })}
  {edge : X.obj (Opposite.op { obj := { len := 1 }, property := SSet.Truncated.Edge._proof_2 })}
  {src_eq :
    autoParam
      ((CategoryTheory.ConcreteCategory.hom
            (X.map (SimplexCategory.Truncated.δ₂ 1 SSet.Truncated.Edge._proof_1 SSet.Truncated.Edge._proof_3).op))
          edge =
        x₀)
      SSet.Truncated.Edge.src_eq._autoParam}
  {tgt_eq :
    autoParam
      ((CategoryTheory.ConcreteCategory.hom
            (X.map (SimplexCategory.Truncated.δ₂ 0 SSet.Truncated.Edge._proof_1 SSet.Truncated.Edge._proof_3).op))
          edge =
        x₁)
      SSet.Truncated.Edge.tgt_eq._autoParam}
  {edge_1 : X.obj (Opposite.op { obj := { len := 1 }, property := SSet.Truncated.Edge._proof_2 })}
  {src_eq_1 :
    autoParam
      ((CategoryTheory.ConcreteCategory.hom
            (X.map (SimplexCategory.Truncated.δ₂ 1 SSet.Truncated.Edge._proof_1 SSet.Truncated.Edge._proof_3).op))
          edge_1 =
        x₀)
      SSet.Truncated.Edge.src_eq._autoParam}
  {tgt_eq_1 :
    autoParam
      ((CategoryTheory.ConcreteCategory.hom
            (X.map (SimplexCategory.Truncated.δ₂ 0 SSet.Truncated.Edge._proof_1 SSet.Truncated.Edge._proof_3).op))
          edge_1 =
        x₁)
      SSet.Truncated.Edge.tgt_eq._autoParam},
  { edge := edge, src_eq := src_eq, tgt_eq := tgt_eq } = { edge := edge_1, src_eq := src_eq_1, tgt_eq := tgt_eq_1 } →
    edge = edge_1
-- Mathlib.Algebra.MonoidAlgebra.Basic
/-- **Alias** of `MonoidAlgebra.lift_mapRingHom_algebraMap`. -/
MonoidAlgebra.lift_mapRangeRingHom_algebraMap : ∀ {R : Type u_1} {S : Type u_2} {A : Type u_4} {M : Type u_7} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : Monoid M] [inst_4 : CommSemiring S] [inst_5 : Algebra S A] [inst_6 : Algebra R S]
  [IsScalarTower R S A] (f : M →* A) (x : MonoidAlgebra R M),
  ((MonoidAlgebra.lift S A M) f) ((MonoidAlgebra.mapRingHom M (algebraMap R S)) x) = ((MonoidAlgebra.lift R A M) f) x
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.H1ToTensorOfIsTrivial_H1π_single : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A : Rep.{u, u, u} k G} [inst_2 : A.IsTrivial] (g : G) (a : ↑A),
  (groupHomology.H1ToTensorOfIsTrivial A)
      ((CategoryTheory.ConcreteCategory.hom (groupHomology.H1π A))
        ((CategoryTheory.ConcreteCategory.hom (groupHomology.cycles₁IsoOfIsTrivial A).inv) fun₀ | g => a)) =
    Additive.ofMul (Abelianization.of g) ⊗ₜ[ℤ] a
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range
range_cfcₙ : ∀ (𝕜 : Type u_1) {A : Type u_2} {p : A → Prop} [inst : RCLike 𝕜] [inst_1 : NonUnitalRing A] [inst_2 : StarRing A]
  [inst_3 : Module 𝕜 A] [inst_4 : IsScalarTower 𝕜 A A] [inst_5 : SMulCommClass 𝕜 A A] [inst_6 : TopologicalSpace A]
  [inst_7 : ContinuousConstSMul 𝕜 A] [inst_8 : StarModule 𝕜 A] [inst_9 : IsTopologicalRing A]
  [inst_10 : ContinuousStar A] [inst_11 : NonUnitalClosedEmbeddingContinuousFunctionalCalculus 𝕜 A p] {a : A},
  p a → (Set.range fun x => cfcₙ x a) = ↑(NonUnitalStarAlgebra.elemental 𝕜 a)
-- Mathlib.FieldTheory.RatFunc.Defs
RatFunc.toFractionRing_inj : ∀ {K : Type u} [inst : CommRing K] {x y : RatFunc K}, x.toFractionRing = y.toFractionRing ↔ x = y
-- Mathlib.Topology.Connected.Basic
connectedComponent_eq_iff_mem : ∀ {α : Type u} [inst : TopologicalSpace α] {x y : α},
  connectedComponent x = connectedComponent y ↔ x ∈ connectedComponent y
-- Mathlib.NumberTheory.FunctionField
FunctionField.ringOfIntegers.instIsNoetherianPolynomialSubtypeMemSubalgebraOfIsSeparableRatFunc : ∀ (F : Type u_1) (K : Type u_2) [inst : Field F] [inst_1 : Field K] [inst_2 : Algebra (Polynomial F) K]
  [inst_3 : Algebra (RatFunc F) K] [IsScalarTower (Polynomial F) (RatFunc F) K] [FunctionField F K]
  [Algebra.IsSeparable (RatFunc F) K], IsNoetherian (Polynomial F) ↥(FunctionField.ringOfIntegers F K)
-- Mathlib.Combinatorics.Pigeonhole
/-- The pigeonhole principle for finitely many pigeons counted by heads: given a function `f`, a
finite sets `s` and `t`, and a number `b` such that `#s ≤ #t • b`, there exists `y ∈ t` such
that its preimage in `s` has no more than `b` elements.
See also `Finset.exists_card_fiber_lt_of_card_lt_nsmul` for a stronger statement.  -/
Finset.exists_card_fiber_le_of_card_le_nsmul : ∀ {α : Type u} {β : Type v} {M : Type w} [inst : DecidableEq β] {s : Finset α} {t : Finset β} {f : α → β} {b : M}
  [inst_1 : CommSemiring M] [inst_2 : LinearOrder M] [IsStrictOrderedRing M],
  t.Nonempty → ↑s.card ≤ t.card • b → ∃ y ∈ t, ↑{x ∈ s | f x = y}.card ≤ b
-- Mathlib.CategoryTheory.Preadditive.Basic
CategoryTheory.Preadditive.isColimitCoforkOfCokernelCofork_desc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {X Y : C} {f g : X ⟶ Y}
  {c : CategoryTheory.Limits.CokernelCofork (f - g)} (i : CategoryTheory.Limits.IsColimit c)
  (s : CategoryTheory.Limits.Cofork f g),
  (CategoryTheory.Preadditive.isColimitCoforkOfCokernelCofork i).desc s =
    i.desc (CategoryTheory.Preadditive.cokernelCoforkOfCofork s)
-- Mathlib.Algebra.Group.Subgroup.Lattice
/-- Subgroup closure of a set is monotone in its argument: if `h ⊆ k`,
then `closure h ≤ closure k`.  -/
Subgroup.closure_mono : ∀ {G : Type u_1} [inst : Group G] ⦃h k : Set G⦄, h ⊆ k → Subgroup.closure h ≤ Subgroup.closure k
-- Std.Data.DTreeMap.Internal.Queries
/-- Folds the given function over the mappings in the tree in ascending order.  -/
Std.DTreeMap.Internal.Impl.foldl : {α : Type u} → {β : α → Type v} → {δ : Type w} → (δ → (a : α) → β a → δ) → δ → Std.DTreeMap.Internal.Impl α β → δ
-- Mathlib.Topology.Constructions
IsOpenMap.subtype_coind : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {p : X → Prop} {f : Y → X},
  IsOpenMap f → ∀ (hp : ∀ (x : Y), p (f x)), IsOpenMap (Subtype.coind f hp)
-- Init.Data.Range.Basic
Std.Legacy.Range : Type
-- Mathlib.Algebra.Homology.ShortComplex.Basic
CategoryTheory.ShortComplex.map_id : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C), S.map (CategoryTheory.Functor.id C) = S
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.trans_refl : ∀ {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β), e.trans (PartialEquiv.refl β) = e
-- Lean.Meta.Tactic.Simp.Rewrite
Lean.Meta.Simp.synthesizeArgs : Lean.Meta.Origin → Array Lean.BinderInfo → Array Lean.Expr → Lean.Meta.SimpM Bool
-- Mathlib.NumberTheory.Real.Irrational
/-- If `x + y` is irrational, then at least one of `x` and `y` is irrational.  -/
Irrational.add_cases : ∀ {x y : ℝ}, Irrational (x + y) → Irrational x ∨ Irrational y
-- Lean.Server.CodeActions.Basic
/-- Index in the list of code action that the given provider generated.  -/
Lean.Server.CodeActionResolveData.providerResultIndex : Lean.Server.CodeActionResolveData → ℕ
-- Mathlib.Data.Set.Restrict
/-- **Alias** of `Set.codRestrict_domRestrict`.

---

Restricting the domain and then the codomain is the same as `MapsTo.restrict`.  -/
Set.codRestrict_restrict : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} (h : ∀ (x : ↑s), f ↑x ∈ t),
  Set.codRestrict (s.domRestrict f) t h = Set.MapsTo.restrict f s t ⋯
-- Init.Data.List.Lemmas
List.all_eq : ∀ {α : Type u_1} {p : α → Bool} {l : List α}, l.all p = decide (∀ x ∈ l, p x = true)
-- Init.Data.Fin.Lemmas
Fin.val_last : ∀ (n : ℕ), ↑(Fin.last n) = n
-- Lean.Data.Lsp.Basic
Lean.Lsp.WorkDoneProgressEnd.kind : Lean.Lsp.WorkDoneProgressEnd → String
-- Mathlib.MeasureTheory.Measure.Restrict
/-- **Alias** of the reverse direction of `MeasureTheory.Measure.ext_iff_of_biUnion_eq_univ`.

---

Two measures are equal if they have equal restrictions on a spanning collection of sets
(formulated using `biUnion`).  -/
MeasureTheory.Measure.ext_of_biUnion_eq_univ : ∀ {α : Type u_2} {ι : Type u_6} {m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} {S : Set ι} {s : ι → Set α},
  S.Countable → ⋃ i ∈ S, s i = Set.univ → (∀ i ∈ S, μ.restrict (s i) = ν.restrict (s i)) → μ = ν
-- Mathlib.Order.OrderDual
/-- Transfer `HImp` across an `Equiv`.  -/
Equiv.himp : {α : Type u_1} → {β : Type u_2} → α ≃ β → [HImp β] → HImp α
-- Mathlib.Topology.Subpath
Path.range_subpathAux : ∀ (t₀ t₁ : ↑unitInterval), Set.range (Set.Icc.convexComb t₀ t₁) = Set.uIcc t₀ t₁
-- Mathlib.Data.Seq.Computation
Computation.map_id : ∀ {α : Type u} (s : Computation α), Computation.map id s = s
-- Mathlib.Topology.Order.UpperLowerSetTopology
/-- Topology whose open sets are lower sets.

Note: In general the lower set topology does not coincide with the lower topology.  -/
Topology.lowerSet : (α : Type u_4) → [Preorder α] → TopologicalSpace α
-- Mathlib.LinearAlgebra.Alternating.Basic
AlternatingMap.domLCongr_refl : ∀ (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) (S : Type u_12) [inst_5 : Semiring S]
  [inst_6 : Module S N] [inst_7 : SMulCommClass R S N],
  AlternatingMap.domLCongr R N ι S (LinearEquiv.refl R M) = LinearEquiv.refl S (M [⋀^ι]→ₗ[R] N)
-- Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
RootPairing.GeckConstruction.cartanSubalgebra.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 : Fintype ι] [inst_7 : DecidableEq ι],
  RootPairing.GeckConstruction.cartanSubalgebra b =
    { toSubmodule := Submodule.span R (Set.range RootPairing.GeckConstruction.h), lie_mem' := ⋯ }
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.RightHomologyMapData.neg_φH : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : S₁.RightHomologyData} {h₂ : S₂.RightHomologyData}
  (γ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂), γ.neg.φH = -γ.φH
-- Lean.Data.PersistentHashMap
Lean.PersistentHashMap.forIn : {m : Type w → Type w'} →
  {σ : Type w} →
    {α : Type u_1} →
      {β : Type u_2} →
        {x : BEq α} →
          {x_1 : Hashable α} → [Monad m] → Lean.PersistentHashMap α β → σ → (α × β → σ → m (ForInStep σ)) → m σ
-- Mathlib.GroupTheory.Nilpotent
Subgroup.lowerCentralSeries_prod : ∀ {G₁ : Type u_2} {G₂ : Type u_3} [inst : Group G₁] [inst_1 : Group G₂] (S₁ : Subgroup G₁) (S₂ : Subgroup G₂) (n : ℕ),
  (S₁.prod S₂).lowerCentralSeries n = (S₁.lowerCentralSeries n).prod (S₂.lowerCentralSeries n)
-- Mathlib.Geometry.Manifold.LocalInvariantProperties
ChartedSpace.liftPropAt_iff : ∀ {H : Type u_1} {M : Type u_2} {H' : Type u_3} {M' : Type u_4} [inst : TopologicalSpace H]
  [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M] [inst_3 : TopologicalSpace H']
  [inst_4 : TopologicalSpace M'] [inst_5 : ChartedSpace H' M'] {P : (H → H') → Set H → H → Prop} {f : M → M'} {x : M},
  ChartedSpace.LiftPropAt P f x ↔
    ContinuousAt f x ∧ P (↑(chartAt H' (f x)) ∘ f ∘ ↑(chartAt H x).symm) Set.univ (↑(chartAt H x) x)
-- Mathlib.RingTheory.Localization.Module
LinearIndependent.iff_fractionRing : ∀ (R : Type u_3) (K : Type u_4) [inst : CommRing R] [inst_1 : CommRing K] [inst_2 : Algebra R K] [IsFractionRing R K]
  {V : Type u_5} [inst_4 : AddCommGroup V] [inst_5 : Module R V] [inst_6 : Module K V] [IsScalarTower R K V]
  {ι : Type u_6} {b : ι → V}, LinearIndependent R b ↔ LinearIndependent K b
-- Mathlib.Topology.MetricSpace.Bounded
/-- An unbounded set has zero diameter. If you would prefer to get the value ∞, use `ediam`.
This lemma makes it possible to avoid side conditions in some situations  -/
Metric.diam_eq_zero_of_unbounded : ∀ {α : Type u} {s : Set α} [inst : PseudoMetricSpace α], ¬Bornology.IsBounded s → Metric.diam s = 0
-- Mathlib.Algebra.Homology.ComplexShape
ComplexShape.mk.inj : ∀ {ι : Type u_1} {Rel : ι → ι → Prop} {next_eq : ∀ {i j j' : ι}, Rel i j → Rel i j' → j = j'}
  {prev_eq : ∀ {i i' j : ι}, Rel i j → Rel i' j → i = i'} {Rel_1 : ι → ι → Prop}
  {next_eq_1 : ∀ {i j j' : ι}, Rel_1 i j → Rel_1 i j' → j = j'}
  {prev_eq_1 : ∀ {i i' j : ι}, Rel_1 i j → Rel_1 i' j → i = i'},
  { Rel := Rel, next_eq := next_eq, prev_eq := prev_eq } =
      { Rel := Rel_1, next_eq := next_eq_1, prev_eq := prev_eq_1 } →
    Rel = Rel_1
-- Mathlib.Topology.MetricSpace.Pseudo.Constructions
/-- Pull back a pseudometric space structure by an inducing map. This is a version of
`PseudoMetricSpace.induced` useful in case if the domain already has a `TopologicalSpace`
structure.  -/
Topology.IsInducing.comapPseudoMetricSpace : {α : Type u_3} →
  {β : Type u_4} →
    [inst : TopologicalSpace α] → [m : PseudoMetricSpace β] → {f : α → β} → Topology.IsInducing f → PseudoMetricSpace α
-- Mathlib.Order.Nucleus
/-- The restriction of a nucleus to its range forms a Galois insertion with the forgetful map from
the range to the original frame.  -/
Nucleus.giRestrict : {X : Type u_1} → [inst : Order.Frame X] → (n : Nucleus X) → GaloisInsertion (⇑n.restrict) Subtype.val
-- Mathlib.Algebra.Order.Module.HahnEmbedding
HahnEmbedding.Partial.orderTop_eq_finiteArchimedeanClassMk : ∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : IsOrderedRing K] [inst_3 : Archimedean K]
  {M : Type u_2} [inst_4 : AddCommGroup M] [inst_5 : LinearOrder M] [inst_6 : IsOrderedAddMonoid M]
  [inst_7 : Module K M] [inst_8 : IsOrderedModule K M] {R : Type u_3} [inst_9 : AddCommGroup R]
  [inst_10 : LinearOrder R] [inst_11 : Module K R] {seed : HahnEmbedding.Seed K M R} (f : HahnEmbedding.Partial seed)
  [IsOrderedAddMonoid R] [Archimedean R] {x : ↥(↑f).domain} (hx0 : ↑x ≠ 0),
  (ofLex (↑↑f x)).orderTop = ↑(FiniteArchimedeanClass.mk (↑x) hx0)
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
CategoryTheory.Limits.Cofork.op_π_app_zero : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {f g : X ⟶ Y}
  (c : CategoryTheory.Limits.Cofork f g),
  c.op.π.app CategoryTheory.Limits.WalkingParallelPair.zero = (c.ι.app CategoryTheory.Limits.WalkingParallelPair.one).op
-- Init.Data.BitVec.Basic
/-- Count the number of leading zeros downward from the `n`-th bit to the `0`-th bit for the bitblaster.
This builds a tree of `if-then-else` lookups whose length is linear in the bitwidth,
and an efficient circuit for bitblasting `clz`.  -/
BitVec.clzAuxRec : {w : ℕ} → BitVec w → ℕ → BitVec w
-- Mathlib.Algebra.Order.Ring.Archimedean
ArchimedeanClass.instZero : {R : Type u_1} →
  [inst : LinearOrder R] → [inst_1 : CommRing R] → [inst_2 : IsStrictOrderedRing R] → Zero (ArchimedeanClass R)
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
Equiv.tsum_eq_tsum_of_support : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α}
  {g : γ → α} (e : ↑(Function.support f) ≃ ↑(Function.support g)),
  (∀ (x : ↑(Function.support f)), g ↑(e x) = f ↑x) → ∑' (x : β), f x = ∑' (y : γ), g y
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
_private.Mathlib.Geometry.Convex.ConvexSpace.Defs.0.Convexity.StdSimplex.restrict_nonneg_aux : ∀ {X : Type u_2} {K : Type u_8} [inst : Semifield K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K]
  {w : Convexity.StdSimplex K X} {p : X → Prop} [inst_3 : DecidablePred p],
  0 ≤ (Finsupp.filter p w.weights).sum fun _x k => k