mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Language.Basic
Lean.Language.Snapshot.mk.inj : ∀ {desc : autoParam String Lean.Language.Snapshot.desc._autoParam} {diagnostics : Lean.Language.Snapshot.Diagnostics}
  {infoTree? : Option Lean.Elab.InfoTree} {traces : Lean.TraceState} {isFatal : Bool}
  {desc_1 : autoParam String Lean.Language.Snapshot.desc._autoParam}
  {diagnostics_1 : Lean.Language.Snapshot.Diagnostics} {infoTree?_1 : Option Lean.Elab.InfoTree}
  {traces_1 : Lean.TraceState} {isFatal_1 : Bool},
  { desc := desc, diagnostics := diagnostics, infoTree? := infoTree?, traces := traces, isFatal := isFatal } =
      { desc := desc_1, diagnostics := diagnostics_1, infoTree? := infoTree?_1, traces := traces_1,
        isFatal := isFatal_1 } →
    desc = desc_1 ∧ diagnostics = diagnostics_1 ∧ infoTree? = infoTree?_1 ∧ traces = traces_1 ∧ isFatal = isFatal_1
-- Mathlib.AlgebraicGeometry.Group.Affine
/-- The essential image of `R`-Hopf algebras under `Spec` is precisely affine group schemes over
`Spec R`.  -/
AlgebraicGeometry.essImage_hopfSpec : ∀ {R : CommRingCat} {G : CategoryTheory.Grp (CategoryTheory.Over (AlgebraicGeometry.Spec R))},
  (AlgebraicGeometry.hopfSpec R).essImage G ↔ AlgebraicGeometry.IsAffine G.X.left
-- Mathlib.RingTheory.TwoSidedIdeal.Basic
TwoSidedIdeal.instNontrivial : ∀ {R : Type u_1} [inst : NonUnitalNonAssocRing R] [Nontrivial R], Nontrivial (TwoSidedIdeal R)
-- Mathlib.MeasureTheory.Group.Arithmetic
/-- `SubNegMonoid.SMulInt` is measurable.  -/
SubNegMonoid.measurableSMul_int₂ : ∀ (M : Type u_6) [inst : SubNegMonoid M] [inst_1 : MeasurableSpace M] [MeasurableAdd₂ M] [MeasurableNeg M],
  MeasurableSMul₂ ℤ M
-- Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit
/-- This follows the proof from
* Borceux, Handbook of categorical algebra 1, Theorem 2.13.4
 -/
CategoryTheory.Limits.colimitLimitToLimitColimit_injective : ∀ {J : Type u₁} {K : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} J] [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  [inst_2 : Small.{v, u₂} K] (F : CategoryTheory.Functor (J × K) (Type v)) [CategoryTheory.IsFiltered K]
  [inst_4 : Finite J],
  Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.colimitLimitToLimitColimit F))
-- Mathlib.LinearAlgebra.TensorProduct.Defs
/-- `IsScalarTower R'₂ R' M` implies `IsScalarTower R'₂ R' (M ⊗[R] N)`  -/
TensorProduct.isScalarTower_left : ∀ {R : Type u_1} {R' : Type u_4} [inst : CommSemiring R] [inst_1 : Monoid R'] {M : Type u_7} {N : Type u_8}
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid N] [inst_4 : DistribMulAction R' M] [inst_5 : Module R M]
  [inst_6 : Module R N] [inst_7 : SMulCommClass R R' M] {R'₂ : Type u_22} [inst_8 : Monoid R'₂]
  [inst_9 : DistribMulAction R'₂ M] [inst_10 : SMulCommClass R R'₂ M] [inst_11 : SMul R'₂ R'] [IsScalarTower R'₂ R' M],
  IsScalarTower R'₂ R' (TensorProduct R M N)
-- Mathlib.Data.Nat.Find
Nat.findGreatest_le : ∀ {P : ℕ → Prop} [inst : DecidablePred P] (n : ℕ), Nat.findGreatest P n ≤ n
-- Mathlib.CategoryTheory.GlueData
CategoryTheory.GlueData.ι_gluedIso_inv_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v, u₁} C] {C' : Type u₂} [inst_1 : CategoryTheory.Category.{v, u₂} C']
  (D : CategoryTheory.GlueData C) (F : CategoryTheory.Functor C C')
  [inst_2 : CategoryTheory.Limits.HasMulticoequalizer D.diagram]
  [inst_3 : CategoryTheory.Limits.PreservesColimit D.diagram.multispan F]
  [inst_4 : ∀ (i j k : D.J), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan (D.f i j) (D.f i k)) F]
  (i : D.J) {Z : C'} (h : F.obj D.glued ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((D.mapGlueData F).ι i) (CategoryTheory.CategoryStruct.comp (D.gluedIso F).inv h) =
    CategoryTheory.CategoryStruct.comp (F.map (D.ι i)) h
-- Lean.KeyedDeclsAttribute
Lean.KeyedDeclsAttribute.mk.sizeOf_spec : ∀ {γ : Type} [inst : SizeOf γ] (defn : Lean.KeyedDeclsAttribute.Def γ)
  (tableRef : IO.Ref (Lean.KeyedDeclsAttribute.Table γ)) (ext : Lean.KeyedDeclsAttribute.Extension γ),
  sizeOf { defn := defn, tableRef := tableRef, ext := ext } = 1 + sizeOf defn + sizeOf tableRef + sizeOf ext
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- If the second of three points is strictly between the other two, the oriented angle at the
first point (reversed) is zero.  -/
Sbtw.oangle₃₁₂_eq_zero : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p₁ p₂ p₃ : P}, Sbtw ℝ p₁ p₂ p₃ → EuclideanGeometry.oangle p₃ p₁ p₂ = 0
-- Mathlib.Order.Filter.Tendsto
Filter.tendsto_id' : ∀ {α : Type u_1} {x y : Filter α}, Filter.Tendsto id x y ↔ x ≤ y
-- Mathlib.Analysis.Normed.Module.WeakDual
/-- The image under `↑ : WeakDual 𝕜 E → (E → 𝕜)` of a polar `WeakDual.polar 𝕜 s` of a
neighborhood `s` of the origin is a closed set.  -/
WeakDual.isClosed_image_polar_of_mem_nhds : ∀ (𝕜 : Type u_1) {E : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {s : Set E}, s ∈ nhds 0 → IsClosed (DFunLike.coe '' WeakDual.polar 𝕜 s)
-- Mathlib.Data.Set.Pairwise.Basic
Set.pairwise_bot_iff : ∀ {α : Type u_1} {s : Set α}, s.Pairwise ⊥ ↔ s.Subsingleton
-- Mathlib.Order.LiminfLimsup
/-- The `liminf` of a function `u` along a filter `f` is the supremum of the `a` such that
the inequality `u x ≥ a` eventually holds for `f`.  -/
Filter.liminf : {α : Type u_1} → {β : Type u_2} → [ConditionallyCompleteLattice α] → (β → α) → Filter β → α
-- Mathlib.Topology.Algebra.Support
tsupport_nsmul : ∀ {X : Type u_1} {α : Type u_2} [inst : TopologicalSpace X] [inst_1 : AddMonoid α] (f : X → α) (n : ℕ),
  (tsupport fun x => n • f x) ⊆ tsupport f
-- Mathlib.Algebra.GCDMonoid.Basic
gcd_greatest_associated : ∀ {α : Type u_2} [inst : CommMonoidWithZero α] [inst_1 : GCDMonoid α] {a b d : α},
  d ∣ a → d ∣ b → (∀ (e : α), e ∣ a → e ∣ b → e ∣ d) → Associated d (gcd a b)
-- Lean.Elab.InfoTree.InlayHints
Lean.Elab.InlayHintLinkLocation.mk.injEq : ∀ (module : Lean.Name) (range : Lean.Syntax.Range) (module_1 : Lean.Name) (range_1 : Lean.Syntax.Range),
  ({ module := module, range := range } = { module := module_1, range := range_1 }) =
    (module = module_1 ∧ range = range_1)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.mem_of_mem_union_of_not_mem_left : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α}, k ∈ t₁ ∪ t₂ → k ∉ t₁ → k ∈ t₂
-- Mathlib.Order.WellFoundedSet
Set.PartiallyWellOrderedOn.iff_not_exists_isMinBadSeq : ∀ {α : Type u_2} {r : α → α → Prop} (rk : α → ℕ) {s : Set α},
  s.PartiallyWellOrderedOn r ↔
    ¬∃ f, Set.PartiallyWellOrderedOn.IsBadSeq r s f ∧ ∀ (n : ℕ), Set.PartiallyWellOrderedOn.IsMinBadSeq r rk s n f
-- Mathlib.CategoryTheory.Comma.Over.Pullback
CategoryTheory.Under.costar_obj_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : C) [inst_1 : CategoryTheory.Limits.HasBinaryCoproducts C]
  (X_1 : C),
  ((CategoryTheory.Under.costar X).obj X_1).hom =
    CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl
      (CategoryTheory.Limits.coprod.desc CategoryTheory.Limits.coprod.inl (CategoryTheory.CategoryStruct.id (X ⨿ X_1)))
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
/-- `true` if solver has already reported max degree issue.  -/
Lean.Meta.Grind.Arith.CommRing.State.reportedMaxDegreeIssue : Lean.Meta.Grind.Arith.CommRing.State → Bool
-- Lean.Parser.Term
Lean.Parser.Term.anonymousCtor.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.congrRight_functor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (e : C ≌ D),
  e.congrRight.functor = (CategoryTheory.Functor.whiskeringRight E C D).obj e.functor
-- Mathlib.Order.Bounds.Basic
/-- If `t` is bounded, then so is `s ∩ t`  -/
BddBelow.inter_of_right : ∀ {α : Type u_1} [inst : Preorder α] {s t : Set α}, BddBelow t → BddBelow (s ∩ t)
-- Lean.Elab.Match
_private.Lean.Elab.Match.0.Lean.Elab.Term.elabMatchAltViews.updateFirst : Option (Lean.Elab.Term.SavedState × Lean.Exception) →
  Lean.Exception → Lean.Elab.TermElabM (Lean.Elab.Term.SavedState × Lean.Exception)
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getD_ofList_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {l : List (α × β)} {k : α} {fallback : β},
  (List.map Prod.fst l).contains k = false → (Std.ExtHashMap.ofList l).getD k fallback = fallback
-- Mathlib.Data.Rel.Separated
/-- **Alias** of `SetRel.IsSeparated.of_subsingleton`. -/
Set.Subsingleton.relIsSeparated : ∀ {X : Type u_1} {R : SetRel X X} {s : Set X}, s.Subsingleton → R.IsSeparated s
-- Mathlib.Algebra.Group.Defs
AddCommMonoid.toAddCommSemigroup : {M : Type u} → [self : AddCommMonoid M] → AddCommSemigroup M
-- Mathlib.CategoryTheory.Yoneda
/-- Two morphisms of presheaves of types `P ⟶ Q` coincide if the precompositions
with morphisms `uliftYoneda.obj X ⟶ P` agree.  -/
CategoryTheory.hom_ext_uliftYoneda : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P Q : CategoryTheory.Functor Cᵒᵖ (Type (max w v₁))}
  {f g : P ⟶ Q},
  (∀ (X : C) (p : CategoryTheory.uliftYoneda.{w, v₁, u₁}.obj X ⟶ P),
      CategoryTheory.CategoryStruct.comp p f = CategoryTheory.CategoryStruct.comp p g) →
    f = g
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
WeierstrassCurve.φ_neg : ∀ {R : Type r} [inst : CommRing R] (W : WeierstrassCurve R) (n : ℤ), W.φ (-n) = W.φ n
-- Mathlib.NumberTheory.Modular
ModularGroup.isClosed_fd : IsClosed ModularGroup.fd
-- Lean.Elab.InfoTree.Types
Lean.Elab.Info.ofFieldInfo : Lean.Elab.FieldInfo → Lean.Elab.Info
-- Mathlib.CategoryTheory.Presentable.Basic
CategoryTheory.HasCardinalFilteredColimits.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {κ : Cardinal.{w}} [inst_1 : Fact κ.IsRegular],
  autoParam
      (∀ (J : Type w) [inst_2 : CategoryTheory.SmallCategory J] [CategoryTheory.IsCardinalFiltered J κ],
        CategoryTheory.Limits.HasColimitsOfShape J C)
      CategoryTheory.HasCardinalFilteredColimits.hasColimitsOfShape._autoParam →
    CategoryTheory.HasCardinalFilteredColimits C κ
-- Init.Data.BitVec.Lemmas
BitVec.eq_of_getMsbD_eq : ∀ {w : ℕ} {x y : BitVec w}, (∀ i < w, x.getMsbD i = y.getMsbD i) → x = y
-- Mathlib.Logic.Encodable.Basic
Encodable.encode_inl : ∀ {α : Type u_1} {β : Type u_2} [inst : Encodable α] [inst_1 : Encodable β] (a : α),
  Encodable.encode (Sum.inl a) = 2 * Encodable.encode a
-- Mathlib.Topology.Inseparable
specializes_of_nhdsWithin : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X} {s : Set X}, nhdsWithin x s ≤ nhdsWithin y s → x ∈ s → x ⤳ y
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.insertManyIfNewUnit.congr_simp : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {ρ : Type u_1} [inst_1 : ForIn Id ρ α]
  (t t_1 : Std.ExtTreeMap α Unit cmp),
  t = t_1 → ∀ (l l_1 : ρ), l = l_1 → t.insertManyIfNewUnit l = t_1.insertManyIfNewUnit l_1
-- Std.Data.HashSet.Raw
/-- Checks if given key is contained and returns the key if it is, otherwise `none`.
The result in the `some` case is guaranteed to be pointer equal to the key in the map.
 -/
Std.HashSet.Raw.get? : {α : Type u} → [BEq α] → [Hashable α] → Std.HashSet.Raw α → α → Option α
-- Mathlib.CategoryTheory.Abelian.Basic
/-- the kernel fork is a limit  -/
CategoryTheory.Abelian.AbelianStruct.isLimitKernelFork : {C : Type u_1} →
  [inst : CategoryTheory.Category.{u_2, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {X Y : C} →
        {f : X ⟶ Y} → (self : CategoryTheory.Abelian.AbelianStruct f) → CategoryTheory.Limits.IsLimit self.kernelFork
-- Mathlib.Tactic.Widget.SelectPanelUtils
SelectInsertParams.mk.sizeOf_spec : ∀ (pos : Lean.Lsp.Position) (goals : Array Lean.Widget.InteractiveGoal)
  (selectedLocations : Array Lean.SubExpr.GoalsLocation) (replaceRange : Lean.Lsp.Range),
  sizeOf { pos := pos, goals := goals, selectedLocations := selectedLocations, replaceRange := replaceRange } =
    1 + sizeOf pos + sizeOf goals + sizeOf selectedLocations + sizeOf replaceRange
-- Init.Data.Order.Lemmas
Std.lt_iff_le_and_ne : ∀ {α : Type u_1} [inst : LE α] [inst_1 : LT α] [Std.LawfulOrderLT α] [Std.IsPartialOrder α] {a b : α},
  a < b ↔ a ≤ b ∧ a ≠ b
-- Mathlib.MeasureTheory.Group.Convolution
/-- The convolution of s-finite measures is s-finite.  -/
MeasureTheory.Measure.sfinite_conv_of_sfinite : ∀ {M : Type u_1} [inst : AddMonoid M] [inst_1 : MeasurableSpace M] (μ ν : MeasureTheory.Measure M)
  [MeasureTheory.SFinite μ] [MeasureTheory.SFinite ν], MeasureTheory.SFinite (μ.conv ν)
-- Mathlib.Algebra.Algebra.NonUnitalHom
NonUnitalAlgHom.inl_apply : ∀ {R : Type u} [inst : Monoid R] {A : Type v} {B : Type w} [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : DistribMulAction R A] [inst_3 : NonUnitalNonAssocSemiring B] [inst_4 : DistribMulAction R B] (x : A),
  (NonUnitalAlgHom.inl R A B) x = (x, 0)
-- Mathlib.Algebra.Order.Group.Basic
zpow_left_strictMono : ∀ (α : Type u_1) [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] {n : ℤ},
  0 < n → StrictMono fun x => x ^ n
-- Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting
CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct.w₂_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : LinearOrder J] [inst_2 : OrderBot J]
  {F : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cocone F} {X Y : C} {p : X ⟶ Y} {f : F.obj ⊥ ⟶ X}
  {g : c.pt ⟶ Y} {j : J} (self : CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct c p f g j) {Z : C}
  (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp self.f' (CategoryTheory.CategoryStruct.comp p h) =
    CategoryTheory.CategoryStruct.comp (c.ι.app j) (CategoryTheory.CategoryStruct.comp g h)
-- Mathlib.Algebra.BigOperators.Fin
Fin.sum_univ_three : ∀ {M : Type u_2} [inst : AddCommMonoid M] (f : Fin 3 → M), ∑ i, f i = f 0 + f 1 + f 2
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.maxKey!_eq_iff_getKey?_eq_self_and_forall : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α], t ≠ ∅ → ∀ {km : α}, t.maxKey! = km ↔ t.getKey? km = some km ∧ ∀ k ∈ t, (cmp k km).isLE = true
-- Mathlib.CategoryTheory.Grothendieck
CategoryTheory.Grothendieck.grothendieckTypeToCat_counitIso_inv_app_coe : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (G : CategoryTheory.Functor C (Type w)) (X : G.Elements),
  ↑((CategoryTheory.Grothendieck.grothendieckTypeToCat G).counitIso.inv.app X) = CategoryTheory.CategoryStruct.id X.fst
-- Lean.Parser.Term.Basic
Lean.Parser.Tactic.tacticSeqIndentGt.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
/-- Given `f : C_c(X, ℝ)` such that `range f ⊆ [a, b]` we obtain a partition of the support of `f`
determined by partitioning `[a, b]` into `N` pieces.  -/
RealRMK.range_cut_partition : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : MeasurableSpace X] [BorelSpace X]
  (f : CompactlySupportedContinuousMap X ℝ) (a : ℝ) {ε : ℝ},
  0 < ε →
    ∀ (N : ℕ),
      Set.range ⇑f ⊆ Set.Ioo a (a + ↑N * ε) →
        ∃ E,
          tsupport ⇑f = ⋃ j, E j ∧
            Set.univ.PairwiseDisjoint E ∧
              (∀ (n : Fin N), ∀ x ∈ E n, a + ε * ↑↑n < f x ∧ f x ≤ a + ε * (↑↑n + 1)) ∧
                ∀ (n : Fin N), MeasurableSet (E n)
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
Real.sinh_log : ∀ {x : ℝ}, 0 < x → Real.sinh (Real.log x) = (x - x⁻¹) / 2
-- Mathlib.Data.Finset.Preimage
Finset.image_preimage_of_bij : ∀ {α : Type u} {β : Type v} [inst : DecidableEq β] (f : α → β) (s : Finset β) (hf : Set.BijOn f (f ⁻¹' ↑s) ↑s),
  Finset.image f (s.preimage f ⋯) = s
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
/-- Take a convex combination with the given weight distribution of an indexed family of points.  -/
Convexity.iConvexComb : {R : Type u_1} →
  {M : Type u_3} →
    {I : Type u_6} →
      [inst : PartialOrder R] →
        [inst_1 : Semiring R] →
          [inst_2 : IsStrictOrderedRing R] → [Convexity.ConvexSpace R M] → Convexity.StdSimplex R I → (I → M) → M
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Embeddings
/-- If `K` is an `n`-th cyclotomic extension of `ℚ`, where `2 < n`, then there are no real places
of `K`.  -/
IsCyclotomicExtension.Rat.nrRealPlaces_eq_zero : ∀ {n : ℕ} [NeZero n] (K : Type u) [inst : Field K] [inst_1 : CharZero K] [inst_2 : IsCyclotomicExtension {n} ℚ K],
  2 < n → NumberField.InfinitePlace.nrRealPlaces K = 0
-- Batteries.Data.DList.Lemmas
_private.Batteries.Data.DList.Lemmas.0.Batteries.DList.cons.match_1.splitter : {α : Type u_1} →
  (motive : α → Batteries.DList α → Sort u_2) →
    (x : α) →
      (x_1 : Batteries.DList α) →
        ((a : α) →
            (f : List α → List α) → (h : ∀ (l : List α), f l = f [] ++ l) → motive a { apply := f, invariant := h }) →
          motive x x_1
-- Mathlib.Topology.ContinuousOn
ContinuousOn.eq_1 : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : X → Y) (s : Set X),
  ContinuousOn f s = ∀ x ∈ s, ContinuousWithinAt f s x
-- Mathlib.Topology.Algebra.Group.SubmonoidClosure
mapClusterPt_self_atTop_nsmul : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [CompactSpace G] [IsTopologicalAddGroup G] (x : G),
  MapClusterPt x Filter.atTop fun x_1 => x_1 • x
-- Mathlib.Topology.OpenPartialHomeomorph.Basic
OpenPartialHomeomorph.toHomeomorphOfSourceEqUnivTargetEqUniv_symm_apply : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y) (h : e.source = Set.univ) (h' : e.target = Set.univ),
  ⇑(e.toHomeomorphOfSourceEqUnivTargetEqUniv h h').symm = ↑e.symm
-- Mathlib.Data.Sum.Basic
Sum.eq_right_iff_getRight_eq : ∀ {α : Type u} {β : Type v} {x : α ⊕ β} {b : β}, x = Sum.inr b ↔ ∃ (h : x.isRight = true), x.getRight h = b
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKey?_erase : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k a : α}, (m.erase k).getKey? a = if (k == a) = true then none else m.getKey? a
-- Mathlib.MeasureTheory.Measure.Prod
MeasureTheory.Measure.ae_ae_comm : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] {p : α → β → Prop},
  MeasurableSet {x | p x.1 x.2} → ((∀ᵐ (x : α) ∂μ, ∀ᵐ (y : β) ∂ν, p x y) ↔ ∀ᵐ (y : β) ∂ν, ∀ᵐ (x : α) ∂μ, p x y)
-- Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
/-- Radon-Nikodym derivative with respect to the scalar multiple of a measure.
See also `rnDeriv_smul_right_of_ne_top'`, which requires sigma-finite `ν` and `μ`.  -/
MeasureTheory.Measure.rnDeriv_smul_right_of_ne_top : ∀ {α : Type u_1} {m : MeasurableSpace α} (ν μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure ν]
  [ν.HaveLebesgueDecomposition μ] {r : ENNReal}, r ≠ 0 → r ≠ ⊤ → ν.rnDeriv (r • μ) =ᵐ[μ] r⁻¹ • ν.rnDeriv μ
-- Mathlib.Algebra.Free
FreeMagma.of : {α : Type u} → α → FreeMagma α
-- Mathlib.Analysis.Normed.Ring.Basic
/-- An injective non-unital ring homomorphism from a `NonUnitalCommRing` to a
`NonUnitalNormedCommRing` induces a `NonUnitalNormedCommRing` structure on the domain.

See note [reducible non-instances]  -/
NonUnitalNormedCommRing.induced : {F : Type u_5} →
  (R : Type u_6) →
    (S : Type u_7) →
      [inst : FunLike F R S] →
        [inst_1 : NonUnitalCommRing R] →
          [inst_2 : NonUnitalNormedCommRing S] →
            [NonUnitalRingHomClass F R S] → (f : F) → Function.Injective ⇑f → NonUnitalNormedCommRing R
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Projective
Matrix.instGroupProjGenLinGroup : (n : Type u_1) →
  [inst : Fintype n] →
    [inst_1 : DecidableEq n] → (R : Type u_2) → [inst_2 : CommRing R] → Group (Matrix.ProjGenLinGroup n R)
-- Mathlib.Data.Fin.Tuple.Basic
Fin.snoc_comp_rev : ∀ {α : Sort u_3} {n : ℕ} (a : α) (f : Fin n → α), Fin.snoc f a ∘ Fin.rev = Fin.cons a (f ∘ Fin.rev)
-- Mathlib.AlgebraicTopology.ExtraDegeneracy
SSet.Augmented.StandardSimplex.shiftFun_succ : ∀ {n : ℕ} {X : Type u_1} [inst : Zero X] (f : Fin n → X) (i : Fin n),
  SSet.Augmented.StandardSimplex.shiftFun f i.succ = f i
-- Mathlib.CategoryTheory.CopyDiscardCategory.Basic
CategoryTheory.CopyDiscardCategory.toSymmetricCategory : {C : Type u} →
  {inst : CategoryTheory.Category.{v, u} C} →
    {inst_1 : CategoryTheory.MonoidalCategory C} →
      [self : CategoryTheory.CopyDiscardCategory C] → CategoryTheory.SymmetricCategory C
-- Mathlib.Algebra.Ring.BooleanRing
BooleanRing.mk : {α : Type u_4} → [toRing : Ring α] → (∀ (a : α), IsIdempotentElem a) → BooleanRing α
-- Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
CategoryTheory.kernelCokernelCompSequence.inl_φ_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X Y Z : C} (f : X ⟶ Y)
  (g : Y ⟶ Z) {Z_1 : C} (h : Y ⊞ Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.kernelCokernelCompSequence.φ f g) h) =
    CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl h)
-- Init.Data.UInt.Basic
/-- Bitwise right shift for 32-bit unsigned integers. Usually accessed via the `>>>` operator.

This function is overridden at runtime with an efficient implementation.
 -/
UInt32.shiftRight : UInt32 → UInt32 → UInt32
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.ResolvableCompletionItem.sortText? : Lean.Lsp.ResolvableCompletionItem → Option String
-- Mathlib.Data.Num.Bitwise
instOneSNum : One SNum
-- Mathlib.Algebra.Homology.ComplexShapeSigns
/-- the signs involved in the symmetry isomorphism of the total complex  -/
TotalComplexShapeSymmetry.σ : {I₁ : Type u_1} →
  {I₂ : Type u_2} →
    {I₁₂ : Type u_4} →
      (c₁ : ComplexShape I₁) →
        (c₂ : ComplexShape I₂) →
          (c₁₂ : ComplexShape I₁₂) →
            {inst : TotalComplexShape c₁ c₂ c₁₂} →
              {inst_1 : TotalComplexShape c₂ c₁ c₁₂} → [self : TotalComplexShapeSymmetry c₁ c₂ c₁₂] → I₁ → I₂ → ℤˣ
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof.oneNeZero.sizeOf_spec : sizeOf Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof.oneNeZero = 1
-- Mathlib.CategoryTheory.Category.ReflQuiv
/-- An isomorphism of quivers lifts to an isomorphism of reflexive quivers given a suitable
compatibility with the identities.  -/
CategoryTheory.ReflQuiv.isoOfQuivIso : {V W : Type u} →
  [inst : CategoryTheory.ReflQuiver V] →
    [inst_1 : CategoryTheory.ReflQuiver W] →
      (e : CategoryTheory.Quiv.of V ≅ CategoryTheory.Quiv.of W) →
        (∀ (X : V), e.hom.map (CategoryTheory.ReflQuiver.id X) = CategoryTheory.ReflQuiver.id (e.hom.obj X)) →
          (CategoryTheory.ReflQuiv.of V ≅ CategoryTheory.ReflQuiv.of W)
-- Mathlib.Data.Nat.Factorial.NatCast
IsUnit.natCast_factorial_of_lt : ∀ {A : Type u_1} [inst : Semiring A] {n : ℕ}, IsUnit ↑(n - 1).factorial → ∀ {m : ℕ}, m < n → IsUnit ↑m.factorial
-- Batteries.Lean.NameMapAttribute
/-- Registers a new extension with the given name and type.  -/
Lean.registerNameMapExtension : (α : Type) → autoParam Lean.Name Lean.registerNameMapExtension._auto_1 → IO (Lean.NameMapExtension α)
-- Mathlib.Analysis.Complex.ReImTopology
Complex.frontier_setOfPred_im_lt : ∀ (a : ℝ), frontier {z | z.im < a} = {z | z.im = a}
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.mem_pow : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Monoid α] {s : Finset α} {a : α} {n : ℕ},
  a ∈ s ^ n ↔ ∃ f, (List.ofFn fun i => ↑(f i)).prod = a
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.IsStableUnderCobaseChange.op : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C}
  [P.IsStableUnderCobaseChange], P.op.IsStableUnderBaseChange