mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Complex.Circle
/-- The map `fun t => exp (t * I)` from `ℝ` to the unit circle in `ℂ`,
considered as a homomorphism of groups.  -/
Circle.expHom : ℝ →+ Additive Circle
-- Lean.ToExpr
Lean.instToExprUInt32 : Lean.ToExpr UInt32
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- The domain of a 2-morphism.  -/
Mathlib.Tactic.BicategoryLike.Mor₂.srcM : {m : Type → Type} →
  [Monad m] →
    [Mathlib.Tactic.BicategoryLike.MonadMor₁ m] →
      Mathlib.Tactic.BicategoryLike.Mor₂ → m Mathlib.Tactic.BicategoryLike.Mor₁
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
CategoryTheory.Limits.parallelFamily_map_left : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : J → (X ⟶ Y)) {j : J},
  (CategoryTheory.Limits.parallelFamily f).map (CategoryTheory.Limits.WalkingParallelFamily.Hom.line j) = f j
-- Lean.Widget.InteractiveGoal
Lean.Widget.instInhabitedInteractiveHypothesisBundle : Inhabited Lean.Widget.InteractiveHypothesisBundle
-- Batteries.Data.BinomialHeap.Basic
Batteries.BinomialHeap.Imp.FindMin.WF.mk : {α : Type u_1} →
  {le : α → α → Bool} →
    {res : Batteries.BinomialHeap.Imp.FindMin α} →
      (rank : ℕ) →
        (∀ {s : Batteries.BinomialHeap.Imp.Heap α},
            Batteries.BinomialHeap.Imp.Heap.WF le rank s → Batteries.BinomialHeap.Imp.Heap.WF le 0 (res.before s)) →
          Batteries.BinomialHeap.Imp.HeapNode.WF le res.val res.node rank →
            Batteries.BinomialHeap.Imp.Heap.WF le (rank + 1) res.next → Batteries.BinomialHeap.Imp.FindMin.WF le res
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.map : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp},
  t₁.Equiv t₂ → ∀ (f : (a : α) → β a → γ a), (Std.DTreeMap.Raw.map f t₁).Equiv (Std.DTreeMap.Raw.map f t₂)
-- Lean.Meta.Match.CaseValues
Lean.Meta.CaseValuesSubgoal : Type
-- Mathlib.Probability.Kernel.Composition.Comp
ProbabilityTheory.Kernel.comp_restrict : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} {κ : ProbabilityTheory.Kernel α β} {η : ProbabilityTheory.Kernel β γ} {s : Set γ}
  (hs : MeasurableSet s), (η.restrict hs).comp κ = (η.comp κ).restrict hs
-- Mathlib.Logic.Unique
Unique.ext : ∀ {α : Sort u} {x y : Unique α}, default = default → x = y
-- Init.Data.UInt.Lemmas
UInt32.toBitVec_sub : ∀ {a b : UInt32}, (a - b).toBitVec = a.toBitVec - b.toBitVec
-- Mathlib.Order.Interval.Finset.Fin
Fin.finsetImage_val_Icc : ∀ {n : ℕ} (a b : Fin n), Finset.image Fin.val (Finset.Icc a b) = Finset.Icc ↑a ↑b
-- Mathlib.Topology.Sheaves.Skyscraper
skyscraperSheaf_obj_obj : ∀ {X : TopCat} (p₀ : ↑X) [inst : (U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type v}
  [inst_1 : CategoryTheory.Category.{u, v} C] (A : C) [inst_2 : CategoryTheory.Limits.HasTerminal C]
  (U : (TopologicalSpace.Opens ↑X)ᵒᵖ), (skyscraperSheaf p₀ A).obj.obj U = if p₀ ∈ Opposite.unop U then A else ⊤_ C
-- Mathlib.CategoryTheory.Monoidal.Closed.FunctorToTypes
CategoryTheory.FunctorToTypes.functorHomEquiv_symm_apply_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F G H : CategoryTheory.Functor C (Type (max w v u)))
  (a : CategoryTheory.MonoidalCategoryStruct.tensorObj F G ⟶ H) (X : C),
  ((CategoryTheory.FunctorToTypes.functorHomEquiv F G H).symm a).app X =
    TypeCat.ofHom fun a_1 =>
      {
        app := fun Y f =>
          TypeCat.ofHom fun x =>
            (CategoryTheory.ConcreteCategory.hom (a.app Y)) (x, (CategoryTheory.ConcreteCategory.hom (G.map f)) a_1),
        naturality := ⋯ }
-- Mathlib.RingTheory.DiscreteValuationRing.Basic
/-- An integral domain is a DVR iff it's a PID with a unique non-zero prime ideal.  -/
IsDiscreteValuationRing.iff_pid_with_one_nonzero_prime : ∀ (R : Type u) [inst : CommRing R] [inst_1 : IsDomain R],
  IsDiscreteValuationRing R ↔ IsPrincipalIdealRing R ∧ ∃! P, P ≠ ⊥ ∧ P.IsPrime
-- Mathlib.Algebra.Star.CHSH
IsCHSHTuple.A₀_sa : ∀ {R : Type u_1} [inst : Monoid R] [inst_1 : StarMul R] {A₀ A₁ B₀ B₁ : R}, IsCHSHTuple A₀ A₁ B₀ B₁ → star A₀ = A₀
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.cycles₂.eq_1 : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  groupHomology.cycles₂ A = (ModuleCat.Hom.hom (groupHomology.d₂₁ A)).ker
-- Mathlib.Algebra.Order.Nonneg.Basic
Nonneg.addMonoid : {α : Type u_1} → [inst : AddMonoid α] → [inst_1 : Preorder α] → [AddLeftMono α] → AddMonoid { x // 0 ≤ x }
-- Mathlib.MeasureTheory.Measure.Portmanteau
MeasureTheory.lintegral_le_liminf_lintegral_of_forall_isOpen_measure_le_liminf_measure : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω] [OpensMeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω} {μs : ℕ → MeasureTheory.Measure Ω} {f : Ω → ℝ},
  Continuous f →
    0 ≤ f →
      (∀ (G : Set Ω), IsOpen G → μ G ≤ Filter.liminf (fun i => (μs i) G) Filter.atTop) →
        ∫⁻ (x : Ω), ENNReal.ofReal (f x) ∂μ ≤
          Filter.liminf (fun i => ∫⁻ (x : Ω), ENNReal.ofReal (f x) ∂μs i) Filter.atTop
-- Mathlib.Order.Filter.Ker
/-- **Alias** of `Filter.giPrincipalKer`.

---

`Filter.principal` forms a Galois coinsertion with `Filter.ker`.  -/
Filter.gi_principal_ker : {α : Type u_2} → GaloisCoinsertion Filter.principal Filter.ker
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.homologyι_comp_fromOpcycles : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasHomology],
  CategoryTheory.CategoryStruct.comp S.homologyι S.fromOpcycles = 0
-- Mathlib.Analysis.Convex.Deriv
StrictConcaveOn.slope_lt_deriv : ∀ {S : Set ℝ} {f : ℝ → ℝ} {x y : ℝ},
  StrictConcaveOn ℝ S f → x ∈ S → y ∈ S → x < y → DifferentiableAt ℝ f x → slope f x y < deriv f x
-- Mathlib.GroupTheory.Nilpotent
Subgroup.upperCentralSeries_eq_top_iff_nilpotencyClass_le : ∀ {G : Type u_1} [inst : Group G] [hG : Group.IsNilpotent G] {n : ℕ},
  Subgroup.upperCentralSeries G n = ⊤ ↔ Group.nilpotencyClass G ≤ n
-- Mathlib.Topology.Convenient.OpenClosed
Topology.IsClosedEmbedding.isGeneratedBy : ∀ {ι : Type u_1} {X : ι → Type u_2} [inst : (i : ι) → TopologicalSpace (X i)] {Y : Type u_3}
  [inst_1 : TopologicalSpace Y] [∀ (i : ι) (F : TopologicalSpace.Closeds (X i)), Topology.IsGeneratedBy X ↥F]
  [Topology.IsGeneratedBy X Y] {U : Type u_4} [inst_4 : TopologicalSpace U] {f : U → Y},
  Topology.IsClosedEmbedding f → Topology.IsGeneratedBy X U
-- Mathlib.CategoryTheory.Functor.Const
CategoryTheory.Functor.constCompWhiskeringLeftIso_hom_app_app : ∀ (J : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} C]
  {D : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} D] (F : CategoryTheory.Functor J D) (X : C) (X_1 : J),
  ((CategoryTheory.Functor.constCompWhiskeringLeftIso J F).hom.app X).app X_1 = CategoryTheory.CategoryStruct.id X
-- Mathlib.Algebra.Algebra.Spectrum.Basic
spectrum.inv₀_mem_iff : ∀ {R : Type u} {A : Type v} [inst : Semifield R] [inst_1 : Ring A] [inst_2 : Algebra R A] {r : R} {a : Aˣ},
  r⁻¹ ∈ spectrum R ↑a ↔ r ∈ spectrum R ↑a⁻¹
-- Mathlib.CategoryTheory.Subobject.Lattice
CategoryTheory.Subobject.completeSemilatticeSup : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.LocallySmall.{w, v₁, u₁} C] →
      [CategoryTheory.WellPowered.{w, v₁, u₁} C] →
        [CategoryTheory.Limits.HasCoproducts C] →
          [CategoryTheory.Limits.HasImages C] → {B : C} → CompleteSemilatticeSup (CategoryTheory.Subobject B)
-- Mathlib.CategoryTheory.Opposites
/-- The natural isomorphism between functors `G ≅ F` induced by a natural isomorphism
between the opposite functors `F.op ≅ G.op`.  -/
CategoryTheory.NatIso.removeOp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → {F G : CategoryTheory.Functor C D} → (F.op ≅ G.op) → (G ≅ F)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
/-- Repeated pointwise multiplication (not the same as pointwise repeated multiplication!) of a
`Finset`. See note [pointwise nat action].  -/
Finset.npow : {α : Type u_2} → [DecidableEq α] → [One α] → [Mul α] → Pow (Finset α) ℕ
-- Mathlib.RingTheory.AlgebraicIndependent.Basic
AlgHom.algebraicIndependent_iff : ∀ {ι : Type u} {R : Type u_2} {A : Type v} {A' : Type v'} {x : ι → A} [inst : CommRing R] [inst_1 : CommRing A]
  [inst_2 : CommRing A'] [inst_3 : Algebra R A] [inst_4 : Algebra R A'] (f : A →ₐ[R] A'),
  Function.Injective ⇑f → (AlgebraicIndependent R (⇑f ∘ x) ↔ AlgebraicIndependent R x)
-- Mathlib.Analysis.Normed.Group.Uniform
dist_self_div_right : ∀ {E : Type u_2} [inst : SeminormedCommGroup E] (a b : E), dist a (a / b) = ‖b‖
-- Mathlib.Algebra.Module.Submodule.Range
LinearMap.range_le_ker_iff : ∀ {R : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} {M : Type u_5} {M₂ : Type u_6} {M₃ : Type u_7} [inst : Semiring R]
  [inst_1 : Semiring R₂] [inst_2 : Semiring R₃] [inst_3 : AddCommMonoid M] [inst_4 : AddCommMonoid M₂]
  [inst_5 : AddCommMonoid M₃] [inst_6 : Module R M] [inst_7 : Module R₂ M₂] [inst_8 : Module R₃ M₃] {τ₁₂ : R →+* R₂}
  {τ₂₃ : R₂ →+* R₃} {τ₁₃ : R →+* R₃} [inst_9 : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃] [inst_10 : RingHomSurjective τ₁₂]
  {f : M →ₛₗ[τ₁₂] M₂} {g : M₂ →ₛₗ[τ₂₃] M₃}, f.range ≤ g.ker ↔ g ∘ₛₗ f = 0
-- Mathlib.Topology.EMetricSpace.Lipschitz
LipschitzWith.ediam_image_le : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {K : NNReal} {f : α → β},
  LipschitzWith K f → ∀ (s : Set α), Metric.ediam (f '' s) ≤ ↑K * Metric.ediam s
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
CategoryTheory.Limits.ChosenPullback₃.p₁₂_eq_lift : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S} {f₃ : X₃ ⟶ S}
  {h₁₂ : CategoryTheory.Limits.ChosenPullback f₁ f₂} {h₂₃ : CategoryTheory.Limits.ChosenPullback f₂ f₃}
  {h₁₃ : CategoryTheory.Limits.ChosenPullback f₁ f₃} (h : CategoryTheory.Limits.ChosenPullback₃ h₁₂ h₂₃ h₁₃),
  h.p₁₂ = ⋯.lift h.p₁ h.p₂ ⋯
-- Init.Data.Array.Lemmas
Array.flatten_filter_not_isEmpty : ∀ {α : Type u_1} {xss : Array (Array α)}, (Array.filter (fun xs => !xs.isEmpty) xss).flatten = xss.flatten
-- Std.Data.HashSet.Raw
/-- Checks whether an element is present in a set and inserts the element if it was not found.
If the hash set already contains an element that is equal (with regard to `==`) to the given
element, then the hash set is returned unchanged.

Equivalent to (but potentially faster than) calling `contains` followed by `insert`.
 -/
Std.HashSet.Raw.containsThenInsert : {α : Type u} → [BEq α] → [Hashable α] → Std.HashSet.Raw α → α → Bool × Std.HashSet.Raw α
-- Mathlib.Algebra.Lie.Extension
LieAlgebra.Extension.proj_surjective : ∀ {R : Type u_1} {L : Type u_3} {M : Type u_4} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : LieRing M] [inst_4 : LieAlgebra R M] (E : LieAlgebra.Extension R M L), Function.Surjective ⇑E.proj
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
MeasureTheory.JordanDecomposition.ext_iff : ∀ {α : Type u_2} {inst : MeasurableSpace α} {x y : MeasureTheory.JordanDecomposition α},
  x = y ↔ x.posPart = y.posPart ∧ x.negPart = y.negPart
-- Init.Data.BitVec.Lemmas
BitVec.toNat_twoPow_of_lt : ∀ {i w : ℕ}, i < w → (BitVec.twoPow w i).toNat = 2 ^ i
-- Init.Data.Array.Lemmas
Array.replicate_succ_ne_empty : ∀ {α : Type u_1} {n : ℕ} {a : α}, Array.replicate (n + 1) a ≠ #[]
-- Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries
QuadraticForm.tmul_tensorRId_apply : ∀ {R : Type uR} {M₁ : Type uM₁} [inst : CommRing R] [inst_1 : AddCommGroup M₁] [inst_2 : Module R M₁]
  [inst_3 : Invertible 2] (Q₁ : QuadraticForm R M₁) (x : TensorProduct R M₁ R),
  Q₁ ((TensorProduct.rid R M₁) x) = (Q₁.tmul QuadraticMap.sq) x
-- Mathlib.CategoryTheory.Pi.Monoidal
CategoryTheory.Pi.monoidalClosed_closed_adj_counit : ∀ {I : Type w₁} {C : I → Type u₁} [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)]
  [inst_1 : (i : I) → CategoryTheory.MonoidalCategory (C i)] [inst_2 : (i : I) → CategoryTheory.MonoidalClosed (C i)]
  (X : (i : I) → C i), CategoryTheory.Closed.adj.counit = CategoryTheory.Pi.closedCounit X
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.map_fract_sub_fract_eq : ∀ (f : CircleDeg1Lift) (x : ℝ), f (Int.fract x) - Int.fract x = f x - x
-- Mathlib.Tactic.Linter.CommandRanges
/-- The "commandRanges" linter logs the `getRange?` and the `getRangeWithTrailing?` for each command.
The format is `[start, end, trailing]`, where
* `start` is the start of the command,
* `end` is the end of the command, not including trailing whitespace and comments,
* `trailing` is the "syntactic end" of the command, so it contains all trailing whitespace and
  comments.

Thus, assuming that there has been no tampering with positions/synthetic syntax,
if the current command is followed by another command, then `trailing` for the previous command
coincides with `start` of the following.
 -/
Mathlib.Linter.linter.commandRanges : Lean.Option Bool
-- Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Associates.prod_le_prod_iff_le : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [UniqueFactorizationMonoid α] [Nontrivial α]
  {p q : Multiset (Associates α)}, (∀ a ∈ p, Irreducible a) → (∀ a ∈ q, Irreducible a) → (p.prod ≤ q.prod ↔ p ≤ q)
-- Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
Complex.volume_ball : ∀ (a : ℂ) (r : ℝ), MeasureTheory.volume (Metric.ball a r) = ENNReal.ofReal r ^ 2 * ↑NNReal.pi
-- Mathlib.Order.CompleteLattice.Basic
iSup_const : ∀ {α : Type u_1} {ι : Sort u_4} [inst : CompleteLattice α] {a : α} [Nonempty ι], ⨆ x, a = a
-- Lean.Parser.Extension
Lean.Parser.ParserResolution.parser.injEq : ∀ (decl : Lean.Name) (isDescr : Bool) (decl_1 : Lean.Name) (isDescr_1 : Bool),
  (Lean.Parser.ParserResolution.parser decl isDescr = Lean.Parser.ParserResolution.parser decl_1 isDescr_1) =
    (decl = decl_1 ∧ isDescr = isDescr_1)
-- Mathlib.Algebra.Group.Pi.Basic
Pi.addCommMonoid : {I : Type u} → {f : I → Type v₁} → [(i : I) → AddCommMonoid (f i)] → AddCommMonoid ((i : I) → f i)
-- Init.GrindInstances.Ring.SInt
Lean.Grind.instCommRingISize : Lean.Grind.CommRing ISize
-- Mathlib.Data.PFunctor.Univariate.Basic
PFunctor.mk : (A : Type uA) → (A → Type uB) → PFunctor.{uA, uB}
-- Mathlib.LinearAlgebra.Alternating.DomCoprod
/-- Computing the `MultilinearMap.alternatization` of the `MultilinearMap.domCoprod` is the same
as computing the `AlternatingMap.domCoprod` of the `MultilinearMap.alternatization`s.
 -/
MultilinearMap.domCoprod_alternization : ∀ {ιa : Type u_1} {ιb : Type u_2} [inst : Fintype ιa] [inst_1 : Fintype ιb] {R' : Type u_3} {Mᵢ : Type u_4}
  {N₁ : Type u_5} {N₂ : Type u_6} [inst_2 : CommSemiring R'] [inst_3 : AddCommGroup N₁] [inst_4 : Module R' N₁]
  [inst_5 : AddCommGroup N₂] [inst_6 : Module R' N₂] [inst_7 : AddCommMonoid Mᵢ] [inst_8 : Module R' Mᵢ]
  [inst_9 : DecidableEq ιa] [inst_10 : DecidableEq ιb] (a : MultilinearMap R' (fun x => Mᵢ) N₁)
  (b : MultilinearMap R' (fun x => Mᵢ) N₂),
  MultilinearMap.alternatization (a.domCoprod b) =
    (MultilinearMap.alternatization a).domCoprod (MultilinearMap.alternatization b)
-- Mathlib.Algebra.Lie.OfAssociative
LieSubmodule.mapsTo_pow_toEnd_sub_algebraMap : ∀ {R : Type u} {L : Type v} {M : Type w} [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]
  (N : LieSubmodule R L M) {φ : R} {k : ℕ} {x : L},
  Set.MapsTo ⇑(((LieModule.toEnd R L M) x - (algebraMap R (Module.End R M)) φ) ^ k) ↑N ↑N
-- Mathlib.LinearAlgebra.InvariantBasisNumber
/-- An isomorphism of `R`-modules `R^n ≃ R^m` induces an isomorphism of `R/I`-modules
`R^n/I^n ≃ R^m/I^m`.  -/
_private.Mathlib.LinearAlgebra.InvariantBasisNumber.0.inducedEquiv : {R : Type u} →
  [inst : CommRing R] →
    {ι : Type v} →
      [Fintype ι] →
        {ι' : Type w} →
          [Fintype ι'] →
            (I : Ideal R) →
              ((ι → R) ≃ₗ[R] ι' → R) → ((ι → R) ⧸ Ideal.pi fun x => I) ≃ₗ[R ⧸ I] (ι' → R) ⧸ Ideal.pi fun x => I
-- Lean.Elab.MutualDef
_private.Lean.Elab.MutualDef.0.Lean.Elab.Term.withHeaderSecVars.collectUsed : Array Lean.Expr →
  Lean.Elab.Command.Scope →
    Array Lean.Elab.DefViewElabHeader →
      Bool → Std.HashMap Lean.FVarId Lean.Name → StateRefT' IO.RealWorld Lean.CollectFVars.State Lean.MetaM Unit
-- Mathlib.Geometry.Euclidean.Projection
Affine.Simplex.orthogonalProjectionSpan_congr : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup V]
  [inst_2 : InnerProductSpace 𝕜 V] [inst_3 : MetricSpace P] [inst_4 : NormedAddTorsor V P] {m n : ℕ}
  {s₁ : Affine.Simplex 𝕜 P m} {s₂ : Affine.Simplex 𝕜 P n} {p₁ p₂ : P},
  Set.range s₁.points = Set.range s₂.points →
    p₁ = p₂ → ↑(s₁.orthogonalProjectionSpan p₁) = ↑(s₂.orthogonalProjectionSpan p₂)
-- Mathlib.Analysis.Convex.Approximation
/-- The real version of `univ_sSup_of_countable_affine_eq`.  -/
ConvexOn.real_univ_sSup_of_countable_affine_eq : ∀ {E : Type u_2} {φ : E → ℝ} [inst : TopologicalSpace E] [inst_1 : AddCommGroup E] [inst_2 : Module ℝ E]
  [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] [HereditarilyLindelofSpace E],
  LowerSemicontinuous φ →
    ConvexOn ℝ Set.univ φ → ∃ 𝓕', 𝓕'.Countable ∧ sSup 𝓕' = φ ∧ ∀ f ∈ 𝓕', f ≤ φ ∧ ∃ l c, f = ⇑l + Function.const E c
-- Mathlib.RingTheory.Ideal.Operations
Ideal.span_singleton_mul_left_inj : ∀ {R : Type u} [inst : Semiring R] {I J : Ideal R} [IsDomain R] [I.IsTwoSided] [J.IsTwoSided] {x : R},
  x ≠ 0 → (I * Ideal.span {x} = J * Ideal.span {x} ↔ I = J)
-- Mathlib.Analysis.CStarAlgebra.Exponential
Commute.expUnitary_add : ∀ {A : Type u_1} [inst : NormedRing A] [inst_1 : NormedAlgebra ℂ A] [inst_2 : StarRing A] [inst_3 : ContinuousStar A]
  [inst_4 : CompleteSpace A] [inst_5 : StarModule ℂ A] {a b : ↥(selfAdjoint A)},
  Commute ↑a ↑b → selfAdjoint.expUnitary (a + b) = selfAdjoint.expUnitary a * selfAdjoint.expUnitary b
-- Mathlib.Algebra.Group.Nat.Units
/-- Alias of `isUnit_iff_eq_one` for discoverability.  -/
Nat.isUnit_iff : ∀ {n : ℕ}, IsUnit n ↔ n = 1
-- Mathlib.RingTheory.AlgebraTower
/-- Restrict the domain of an `AlgHom`.  -/
AlgHom.domRestrict : {A : Type u_3} →
  (B : Type u_4) →
    {C : Type u_5} →
      {D : Type u_6} →
        [inst : CommSemiring A] →
          [inst_1 : CommSemiring C] →
            [inst_2 : CommSemiring D] →
              [inst_3 : Algebra A C] →
                [inst_4 : Algebra A D] →
                  [inst_5 : CommSemiring B] →
                    [inst_6 : Algebra A B] → [inst_7 : Algebra B C] → [IsScalarTower A B C] → (C →ₐ[A] D) → B →ₐ[A] D
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Adjunction.Algebra.homEquiv_naturality_str : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor C C} (adj : F ⊣ G)
  (A₁ A₂ : CategoryTheory.Endofunctor.Algebra F) (f : A₁ ⟶ A₂),
  CategoryTheory.CategoryStruct.comp ((adj.homEquiv A₁.a A₁.a) A₁.str) (G.map f.f) =
    CategoryTheory.CategoryStruct.comp f.f ((adj.homEquiv A₂.a A₂.a) A₂.str)
-- Aesop.Rule.Name
Aesop.instBEqDisplayRuleName : BEq Aesop.DisplayRuleName
-- Mathlib.LinearAlgebra.Matrix.Ideal
/-- A version of `ofMatrix_rel` for a single matrix index, rather than all indices.  -/
RingCon.ofMatrix_rel' : ∀ {R : Type u_1} {n : Type u_2} [inst : NonAssocSemiring R] [inst_1 : Fintype n] [inst_2 : DecidableEq n]
  {c : RingCon (Matrix n n R)} {x y : R} (i j : n), c.ofMatrix x y ↔ c (Matrix.single i j x) (Matrix.single i j y)
-- Mathlib.Topology.Separation.CompletelyRegular
T35Space.mk : ∀ {X : Type u} [inst : TopologicalSpace X] [toT0Space : T0Space X]
  [toCompletelyRegularSpace : CompletelyRegularSpace X], T35Space X
-- Mathlib.Geometry.Manifold.ContMDiff.NormedSpace
/-- Applying a linear map to a vector is smooth within a set. Version in vector spaces. For
versions in nontrivial vector bundles, see `ContMDiffWithinAt.clm_apply_of_inCoordinates` and
`ContMDiffWithinAt.clm_bundle_apply`.  -/
ContMDiffWithinAt.clm_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F₁ : Type u_8} [inst_6 : NormedAddCommGroup F₁]
  [inst_7 : NormedSpace 𝕜 F₁] {F₂ : Type u_9} [inst_8 : NormedAddCommGroup F₂] [inst_9 : NormedSpace 𝕜 F₂]
  {n : WithTop ℕ∞} {g : M → F₁ →L[𝕜] F₂} {f : M → F₁} {s : Set M} {x : M},
  ContMDiffWithinAt I (modelWithCornersSelf 𝕜 (F₁ →L[𝕜] F₂)) n g s x →
    ContMDiffWithinAt I (modelWithCornersSelf 𝕜 F₁) n f s x →
      ContMDiffWithinAt I (modelWithCornersSelf 𝕜 F₂) n (fun x => (g x) (f x)) s x
-- Mathlib.NumberTheory.LSeries.Deriv
_private.Mathlib.NumberTheory.LSeries.Deriv.0.LSeries.LSeriesSummable_logMul_and_hasDerivAt : ∀ {f : ℕ → ℂ} {s : ℂ},
  LSeries.abscissaOfAbsConv f < ↑s.re →
    LSeriesSummable (LSeries.logMul f) s ∧ HasDerivAt (LSeries f) (-LSeries (LSeries.logMul f) s) s
-- Mathlib.Order.Nucleus
Nucleus.inf_apply : ∀ {X : Type u_1} [inst : SemilatticeInf X] (m n : Nucleus X) (x : X), (m ⊓ n) x = m x ⊓ n x
-- Mathlib.Data.Nat.Cast.Defs
/-- When writing lemmas about `OfNat.ofNat` that assume `Nat.AtLeastTwo`, the term needs to be wrapped
in `no_index` so as not to confuse `simp`, as `no_index (OfNat.ofNat n)`.

Rather than referencing this library note, use `ofNat(n)` as a shorthand for
`no_index (OfNat.ofNat n)`.

Some discussion is [on Zulip here](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/.E2.9C.94.20Polynomial.2Ecoeff.20example/near/395438147).
 -/
LibraryNote.«no_index_around_OfNat.ofNat» : Batteries.Util.LibraryNote
-- Mathlib.CategoryTheory.Monad.EquivMon
/-- Oh, monads are just monoids in the category of endofunctors (equivalence of categories).  -/
CategoryTheory.Monad.monadMonEquiv : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.Monad C ≌ CategoryTheory.Mon (CategoryTheory.Functor C C)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.insertMany_cons : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l : List (α × β)} {p : α × β},
  Std.ExtDHashMap.Const.insertMany m (p :: l) = Std.ExtDHashMap.Const.insertMany (m.insert p.1 p.2) l
-- Mathlib.RingTheory.PrincipalIdealDomain
isRelPrime_iff_isCoprime : ∀ {R : Type u} [inst : CommRing R] {x y : R} [Submodule.IsPrincipal (Ideal.span {x, y})], IsRelPrime x y ↔ IsCoprime x y
-- Mathlib.Order.Filter.AtTopBot.Field
/-- If `f` tends to negative infinity along a nontrivial filter `l`,
then `fun x ↦ r * f x` tends to infinity if and only if `r < 0`.  -/
Filter.tendsto_const_mul_atTop_iff_neg : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {l : Filter β}
  {f : β → α} {r : α} [l.NeBot],
  Filter.Tendsto f l Filter.atBot → (Filter.Tendsto (fun x => r * f x) l Filter.atTop ↔ r < 0)
-- Mathlib.LinearAlgebra.Matrix.Rank
Matrix.rank_mul_eq_left_of_det_mem_nonZeroDivisors : ∀ {m : Type um} {n : Type un} [inst : Fintype n] {R : Type u_1} [inst_1 : CommRing R] [inst_2 : DecidableEq n]
  (A : Matrix n n R) (B : Matrix m n R), A.det ∈ nonZeroDivisors R → (B * A).rank = B.rank
-- Mathlib.Topology.Compactness.Compact
/-- The product of two compact spaces is compact.  -/
instCompactSpaceProd : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [CompactSpace X] [CompactSpace Y],
  CompactSpace (X × Y)
-- Lean.Expr
/-- Return the string literal `.lit (.strVal s)`  -/
Lean.mkStrLit : String → Lean.Expr
-- Mathlib.Order.Hom.Bounded
BotHom.id.eq_1 : ∀ (α : Type u_2) [inst : Bot α], BotHom.id α = { toFun := id, map_bot' := ⋯ }
-- Mathlib.Algebra.Order.Nonneg.Field
Nonneg.coe_nnratCast : ∀ {α : Type u_1} [inst : Semifield α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] (q : ℚ≥0), ↑↑q = ↑q
-- Mathlib.NumberTheory.FunctionField
/-- **Alias** of `RatFunc.CompletionAtInfty`. -/
FunctionField.FqtInfty : (F : Type u_1) → [inst : Field F] → [DecidableEq (RatFunc F)] → Type u_1