mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.InnerProductSpace.Basic
/-- The inner product of a vector with a multiple of itself.  -/
real_inner_smul_self_left : ∀ {F : Type u_3} [inst : SeminormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] (x : F) (r : ℝ),
  inner ℝ (r • x) x = r * (‖x‖ * ‖x‖)
-- Mathlib.CategoryTheory.Equivalence.Symmetry
CategoryTheory.Equivalence.symmEquiv_functor : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] (D : Type u_2)
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D],
  (CategoryTheory.Equivalence.symmEquiv C D).functor = CategoryTheory.Equivalence.symmEquivFunctor C D
-- Mathlib.LinearAlgebra.TensorProduct.RightExactness
/-- Tensoring an exact pair on the left gives an exact pair  -/
lTensor_exact : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup N] [inst_3 : AddCommGroup P] [inst_4 : Module R M] [inst_5 : Module R N] [inst_6 : Module R P]
  {f : M →ₗ[R] N} {g : N →ₗ[R] P} (Q : Type u_5) [inst_7 : AddCommGroup Q] [inst_8 : Module R Q],
  Function.Exact ⇑f ⇑g → Function.Surjective ⇑g → Function.Exact ⇑(LinearMap.lTensor Q f) ⇑(LinearMap.lTensor Q g)
-- Mathlib.MeasureTheory.Order.Lattice
MeasurableSup₂.toMeasurableSup : ∀ {M : Type u_1} [inst : MeasurableSpace M] [inst_1 : Max M] [MeasurableSup₂ M], MeasurableSup M
-- Mathlib.Algebra.Category.Ring.Basic
SemiRingCat.comp_apply : ∀ {R S T : SemiRingCat} (f : R ⟶ S) (g : S ⟶ T) (r : ↑R),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) r =
    (CategoryTheory.ConcreteCategory.hom g) ((CategoryTheory.ConcreteCategory.hom f) r)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.union_add_inter_subset_union : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Add α] {s₁ s₂ t₁ t₂ : Finset α},
  s₁ ∪ s₂ + t₁ ∩ t₂ ⊆ s₁ + t₁ ∪ (s₂ + t₂)
-- Init.Data.SInt.Lemmas
Int8.ofInt_bitVecToInt : ∀ (n : BitVec 8), Int8.ofInt n.toInt = Int8.ofBitVec n
-- Mathlib.CategoryTheory.Preadditive.Basic
/-- A cokernel of `f - g` is a coequalizer of `f` and `g`.  -/
CategoryTheory.Preadditive.isColimitCoforkOfCokernelCofork : {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)} →
            CategoryTheory.Limits.IsColimit c →
              CategoryTheory.Limits.IsColimit (CategoryTheory.Preadditive.coforkOfCokernelCofork c)
-- Mathlib.CategoryTheory.Action.Concrete
/-- The group isomorphism between `Function.End X` and `CategoryTheory.End X`.  -/
TypeCat.endEquiv : (X : Type u) → Function.End X ≃* CategoryTheory.End X
-- Mathlib.Topology.MetricSpace.Pseudo.Constructions
Subtype.nndist_eq : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] {p : α → Prop} (x y : Subtype p), nndist x y = nndist ↑x ↑y
-- Mathlib.RingTheory.LocalRing.NonLocalRing
/-- The following conditions are equivalent for a commutative (semi)ring `R`:
* `R` is not local,
* the maximal spectrum of `R` is nontrivial,
* `R` has two distinct maximal ideals.
 -/
IsLocalRing.not_isLocalRing_tfae : ∀ {R : Type u_1} [inst : CommSemiring R] [Nontrivial R],
  [¬IsLocalRing R, Nontrivial (MaximalSpectrum R), ∃ m₁ m₂, m₁.IsMaximal ∧ m₂.IsMaximal ∧ m₁ ≠ m₂].TFAE
-- Lean.Parser.Extra
Lean.Parser.patternIgnore.parenthesizer : Lean.PrettyPrinter.Parenthesizer → Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Order.SetNotation
/-- Delaborator for indexed unions.  -/
Set.iUnion_delab : Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.RingTheory.LocalProperties.Submodule
Submodule.eq_of_localization_maximal : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_4) [inst_3 : (P : Ideal R) → [inst : P.IsMaximal] → CommSemiring (Rₚ P)]
  [inst_4 : (P : Ideal R) → [inst_4 : P.IsMaximal] → Algebra R (Rₚ P)]
  [inst_5 : ∀ (P : Ideal R) [inst_5 : P.IsMaximal], IsLocalization.AtPrime (Rₚ P) P]
  (Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_5) [inst_6 : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)]
  [inst_7 : (P : Ideal R) → [inst_7 : P.IsMaximal] → Module R (Mₚ P)]
  [inst_8 : (P : Ideal R) → [inst : P.IsMaximal] → Module (Rₚ P) (Mₚ P)]
  [inst_9 : ∀ (P : Ideal R) [inst_9 : P.IsMaximal], IsScalarTower R (Rₚ P) (Mₚ P)]
  (f : (P : Ideal R) → [inst_10 : P.IsMaximal] → M →ₗ[R] Mₚ P)
  [inst_10 : ∀ (P : Ideal R) [inst_10 : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)] {N₁ N₂ : Submodule R M},
  (∀ (P : Ideal R) [inst_11 : P.IsMaximal],
      Submodule.localized' (Rₚ P) P.primeCompl (f P) N₁ = Submodule.localized' (Rₚ P) P.primeCompl (f P) N₂) →
    N₁ = N₂
-- Mathlib.Data.Stream.Init
Stream'.unfolds_head_eq : ∀ {α : Type u} (s : Stream' α), Stream'.unfolds Stream'.head Stream'.tail s = s
-- Mathlib.Combinatorics.SetFamily.Intersecting
Set.Subsingleton.intersecting : ∀ {α : Type u_1} [inst : SemilatticeInf α] [inst_1 : OrderBot α] {s : Set α},
  s.Subsingleton → (s.Intersecting ↔ s ≠ {⊥})
-- Mathlib.Tactic.FunProp.Types
Mathlib.Meta.FunProp.Origin.decl.inj : ∀ {name name_1 : Lean.Name},
  Mathlib.Meta.FunProp.Origin.decl name = Mathlib.Meta.FunProp.Origin.decl name_1 → name = name_1
-- Mathlib.Algebra.Module.Equiv.Basic
AddEquiv.toIntLinearEquiv_trans : ∀ {M : Type u_5} {M₂ : Type u_7} {M₃ : Type u_8} [inst : AddCommGroup M] [inst_1 : AddCommGroup M₂]
  [inst_2 : AddCommGroup M₃] {modM : Module ℤ M} {modM₂ : Module ℤ M₂} {modM₃ : Module ℤ M₃} (e : M ≃+ M₂)
  (e₂ : M₂ ≃+ M₃), (e.trans e₂).toIntLinearEquiv = e.toIntLinearEquiv ≪≫ₗ e₂.toIntLinearEquiv
-- Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1
CategoryTheory.PresheafOfGroups.OneCocycle.one_toOneCochain : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (G : CategoryTheory.Functor Cᵒᵖ GrpCat) {I : Type w'}
  (U : I → C), CategoryTheory.PresheafOfGroups.OneCocycle.toOneCochain 1 = 1
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instMulAction'.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α} {M : Type u_5} [inst : Monoid M] [inst_1 : MulAction M β],
  Filter.Germ.instMulAction' = { toSMul := Filter.Germ.instSMul', mul_smul := ⋯, one_smul := ⋯ }
-- Mathlib.NumberTheory.FactorisationProperties
Nat.Prime.not_perfect : ∀ {p : ℕ}, Nat.Prime p → ¬p.Perfect
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Arrow.w_assoc : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] {P Q W : CategoryTheory.MorphismProperty T}
  [inst_1 : Q.IsMultiplicative] [inst_2 : W.IsMultiplicative] {A B : P.Arrow Q W} (f : A ⟶ B) {Z : T} (h : B.right ⟶ Z),
  CategoryTheory.CategoryStruct.comp f.left (CategoryTheory.CategoryStruct.comp B.hom h) =
    CategoryTheory.CategoryStruct.comp A.hom (CategoryTheory.CategoryStruct.comp f.right h)
-- Std.Tactic.BVDecide.Normalize.BitVec
Std.Tactic.BVDecide.Normalize.BitVec.not_lt_zero : ∀ {n : ℕ} (a : BitVec n), a.ult 0#n = false
-- Mathlib.Algebra.Ring.Subring.Defs
Subring.subtype_apply : ∀ {R : Type u} [inst : NonAssocRing R] {s : Subring R} (x : ↥s), s.subtype x = ↑x
-- Mathlib.MeasureTheory.Covering.VitaliFamily
/-- Given a Vitali family `v` for a measure `μ`, a family `f` is a fine subfamily on a set `s` if
every point `x` in `s` belongs to arbitrarily small sets in `v.setsAt x ∩ f x`. This is precisely
the subfamilies for which the Vitali family definition ensures that one can extract a disjoint
covering of almost all `s`.  -/
VitaliFamily.FineSubfamilyOn : {X : Type u_1} →
  [inst : PseudoMetricSpace X] →
    {m0 : MeasurableSpace X} → {μ : MeasureTheory.Measure X} → VitaliFamily μ → (X → Set (Set X)) → Set X → Prop
-- Mathlib.Order.Filter.Pointwise
Filter.vaddCommClass_filter : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : VAdd α γ] [inst_1 : VAdd β γ] [VAddCommClass α β γ],
  VAddCommClass α β (Filter γ)
-- Mathlib.CategoryTheory.GradedObject.Unitor
/-- The `BifunctorComp₂₃IndexData r` attached to a `TriangleIndexData r π`.  -/
CategoryTheory.GradedObject.TriangleIndexData.ρ₂₃ : {I₁ : Type u_1} →
  {I₂ : Type u_2} →
    {I₃ : Type u_3} →
      {J : Type u_4} →
        [inst : Zero I₂] →
          {r : I₁ × I₂ × I₃ → J} →
            {π : I₁ × I₃ → J} →
              CategoryTheory.GradedObject.TriangleIndexData r π → CategoryTheory.GradedObject.BifunctorComp₂₃IndexData r
-- Mathlib.MeasureTheory.Function.LpSeminorm.Defs
MeasureTheory.eLpNorm_nnreal_pow_eq_lintegral : ∀ {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} [inst : ENorm ε] {μ : MeasureTheory.Measure α} {f : α → ε}
  {p : NNReal}, p ≠ 0 → MeasureTheory.eLpNorm f (↑p) μ ^ ↑p = ∫⁻ (x : α), ‖f x‖ₑ ^ ↑p ∂μ
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
/-- Auxiliary type for normalizing `Ring` and `Field` inequalities.  -/
Lean.Meta.Grind.Arith.Linear.RingIneqCnstr : Type
-- Mathlib.Geometry.Convex.Cone.Pointed
PointedCone.instCanLiftConvexConeToConvexConePointed : ∀ {R : Type u_1} {E : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommMonoid E] [inst_4 : Module R E],
  CanLift (ConvexCone R E) (PointedCone R E) PointedCone.toConvexCone ConvexCone.Pointed
-- Lean.Meta.DiscrTree.Main
_private.Lean.Meta.DiscrTree.Main.0.Lean.Meta.DiscrTree.tmpStar : Lean.Expr
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousSemilinearMapClass.toSemilinearMapClass : ∀ {F : Type u_1} {R : outParam (Type u_2)} {S : outParam (Type u_3)} {inst : Semiring R} {inst_1 : Semiring S}
  {σ : outParam (R →+* S)} {M : outParam (Type u_4)} {inst_2 : TopologicalSpace M} {inst_3 : AddCommMonoid M}
  {M₂ : outParam (Type u_5)} {inst_4 : TopologicalSpace M₂} {inst_5 : AddCommMonoid M₂} {inst_6 : Module R M}
  {inst_7 : Module S M₂} {inst_8 : FunLike F M M₂} [self : ContinuousSemilinearMapClass F σ M M₂],
  SemilinearMapClass F σ M M₂
-- Mathlib.Algebra.Category.CommBialgCat
CommAlgCat.monObjOpOf : {R : Type u} →
  [inst : CommRing R] →
    {A : Type u} →
      [inst_1 : CommRing A] → [inst_2 : Bialgebra R A] → CategoryTheory.MonObj (Opposite.op (CommAlgCat.of R A))
-- Mathlib.Order.ConditionallyCompleteLattice.Finset
Finset.sup'_eq_csSup_image : ∀ {ι : Type u_1} {α : Type u_2} [inst : ConditionallyCompleteLattice α] (s : Finset ι) (H : s.Nonempty) (f : ι → α),
  s.sup' H f = sSup (f '' ↑s)
-- Mathlib.Topology.Algebra.UniformConvergence
UniformFun.toFun_neg : ∀ {α : Type u_1} {β : Type u_2} [inst : Neg β] (f : UniformFun α β), UniformFun.toFun (-f) = -UniformFun.toFun f
-- Mathlib.Data.Finmap
/-- `s₁ ∪ s₂` is the key-based union of two finite maps. It is left-biased: if
there exists an `a ∈ s₁`, `lookup a (s₁ ∪ s₂) = lookup a s₁`.  -/
Finmap.union : {α : Type u} → {β : α → Type v} → [DecidableEq α] → Finmap β → Finmap β → Finmap β
-- Lean.Data.PersistentHashMap
Lean.PersistentHashMap.Node.brecOn_2.eq : ∀ {α : Type u} {β : Type v} {motive_1 : Lean.PersistentHashMap.Node α β → Sort u_1}
  {motive_2 : Array (Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β)) → Sort u_1}
  {motive_3 : List (Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β)) → Sort u_1}
  {motive_4 : Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β) → Sort u_1}
  (t : List (Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β)))
  (F_1 : (t : Lean.PersistentHashMap.Node α β) → t.below → motive_1 t)
  (F_2 :
    (t : Array (Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β))) →
      Lean.PersistentHashMap.Node.below_1 t → motive_2 t)
  (F_3 :
    (t : List (Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β))) →
      Lean.PersistentHashMap.Node.below_2 t → motive_3 t)
  (F_4 :
    (t : Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β)) →
      Lean.PersistentHashMap.Node.below_3 t → motive_4 t),
  Lean.PersistentHashMap.Node.brecOn_2 t F_1 F_2 F_3 F_4 =
    F_3 t (Lean.PersistentHashMap.Node.brecOn_2.go t F_1 F_2 F_3 F_4).2
-- Mathlib.Algebra.Order.Group.PosPart
abs_add_eq_two_nsmul_posPart : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : AddCommGroup α] [AddLeftMono α] (a : α), |a| + a = 2 • a⁺
-- Mathlib.Topology.MetricSpace.HausdorffDimension
hausdorffMeasure_of_lt_dimH : ∀ {X : Type u_2} [inst : EMetricSpace X] [inst_1 : MeasurableSpace X] [inst_2 : BorelSpace X] {s : Set X} {d : NNReal},
  ↑d < dimH s → (MeasureTheory.Measure.hausdorffMeasure ↑d) s = ⊤
-- Init.Data.List.Lemmas
/-- Variant of `getElem?_reverse` with a hypothesis giving the linear relation between the indices.  -/
List.getElem?_reverse' : ∀ {α : Type u_1} {l : List α} {i j : ℕ}, i + j + 1 = l.length → l.reverse[i]? = l[j]?
-- Mathlib.CategoryTheory.EquivalenceRelation
CategoryTheory.ReflexiveRelation.reflexivity₁_apply : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {R X : C} {p₁ p₂ : R ⟶ X}
  (self : CategoryTheory.ReflexiveRelation p₁ p₂) {F : C → C → Type uF} {carrier : C → Type w}
  {instFunLike : (X Y : C) → FunLike (F X Y) (carrier X) (carrier Y)} [inst_1 : CategoryTheory.ConcreteCategory C F]
  (x : carrier X), (CategoryTheory.ConcreteCategory.hom p₁) ((CategoryTheory.ConcreteCategory.hom self.r) x) = x
-- Mathlib.Analysis.Convolution
/-- The convolution of two even functions is also even.  -/
MeasureTheory.convolution_neg_of_neg_eq : ∀ {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup E'] [inst_2 : NormedAddCommGroup F] {f : G → E} {g : G → E'} {x : G}
  [inst_3 : NontriviallyNormedField 𝕜] [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜 E'] [inst_6 : NormedSpace 𝕜 F]
  (L : E →L[𝕜] E' →L[𝕜] F) [inst_7 : MeasurableSpace G] {μ : MeasureTheory.Measure G} [inst_8 : NormedSpace ℝ F]
  [inst_9 : AddCommGroup G] [μ.IsAddLeftInvariant] [μ.IsNegInvariant] [MeasurableNeg G] [MeasurableAdd G],
  (∀ᵐ (x : G) ∂μ, f (-x) = f x) →
    (∀ᵐ (x : G) ∂μ, g (-x) = g x) → MeasureTheory.convolution f g L μ (-x) = MeasureTheory.convolution f g L μ x
-- Mathlib.Topology.Semicontinuity.Defs
UpperHemicontinuousWithinAt.comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace γ]
  [inst_2 : TopologicalSpace β] {f : α → Set β} {s : Set α} {g : γ → α} {c : γ} {t : Set γ},
  UpperHemicontinuousWithinAt f s (g c) →
    ContinuousWithinAt g t c → Set.MapsTo g t s → UpperHemicontinuousWithinAt (f ∘ g) t c
-- Mathlib.Algebra.FreeAlgebra
/-- The free algebra on `X` is "just" the monoid algebra on the free monoid on `X`.

This would be useful when constructing linear maps out of a free algebra,
for example.
 -/
FreeAlgebra.equivMonoidAlgebraFreeMonoid : {R : Type u_1} → {X : Type u_2} → [inst : CommSemiring R] → FreeAlgebra R X ≃ₐ[R] MonoidAlgebra R (FreeMonoid X)
-- Mathlib.Tactic.CongrExclamation
/-- Asserts the given congruence theorem as fresh hypothesis, and then applies it.
Return the `fvarId` for the new hypothesis and the new subgoals.

We apply it with transparency settings specified by `Congr!.Config.transparency`.
 -/
_private.Mathlib.Tactic.CongrExclamation.0.applyCongrThm? : Congr!.Config → Lean.MVarId → Lean.Expr → Lean.Expr → Lean.MetaM (List Lean.MVarId)
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.adicCompletion.equivCompletion_symm_apply_toCompletion : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (K : Type u_2) [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R)
  (toCompletion : (IsDedekindDomain.HeightOneSpectrum.valuation K v).Completion),
  ((IsDedekindDomain.HeightOneSpectrum.adicCompletion.equivCompletion K v).symm toCompletion).toCompletion =
    toCompletion
-- Mathlib.Topology.VectorBundle.Riemannian
Bundle.RiemannianMetric.pos : ∀ {B : Type u_4} {E : B → Type u_6} [inst : (b : B) → TopologicalSpace (E b)] [inst_1 : (b : B) → AddCommGroup (E b)]
  [inst_2 : (b : B) → Module ℝ (E b)] (self : Bundle.RiemannianMetric E) (b : B) (v : E b),
  v ≠ 0 → 0 < ((self.inner b) v) v
-- Mathlib.Algebra.Module.Torsion.Basic
AddSubgroup.torsionBy.neg : ∀ (A : Type u_3) [inst : AddCommGroup A] (n : ℤ), AddSubgroup.torsionBy A (-n) = AddSubgroup.torsionBy A n
-- Init.Data.Iterators.Consumers.Monadic.Loop
/-- Returns the first non-`none` result of applying `f` to each output of the iterator, in order.
Returns `none` if `f` returns `none` for all outputs.

`O(|it|)`. Short-circuits when `f` returns `some _`.The outputs of `it` are examined in order of
iteration.

If the iterator is not finite, this function might run forever. The variant
`it.ensureTermination.findSome?` always terminates after finitely many steps.

Examples:
 * `([7, 6, 5, 8, 1, 2, 6].iterM Id).findSome? (fun x => if x < 5 then some (10 * x) else none) = pure (some 10)`
 * `([7, 6, 5, 8, 1, 2, 6].iterM Id).findSome? (fun x => if x < 1 then some (10 * x) else none) = pure none`
 -/
Std.IterM.findSome? : {α β γ : Type w} →
  {m : Type w → Type w'} →
    [Monad m] → [inst : Std.Iterator α m β] → [Std.IteratorLoop α m m] → Std.IterM m β → (β → Option γ) → m (Option γ)
-- Mathlib.MeasureTheory.Measure.Haar.Basic
/-- additive version of `MeasureTheory.Measure.haar.haarContent`  -/
MeasureTheory.Measure.haar.addHaarContent : {G : Type u_1} →
  [inst : AddGroup G] →
    [inst_1 : TopologicalSpace G] →
      [IsTopologicalAddGroup G] → TopologicalSpace.PositiveCompacts G → MeasureTheory.Content G
-- Mathlib.CategoryTheory.Limits.Shapes.Diagonal
/-- Informally, this is a special case of `pullback_map_diagonal_isPullback` for `T = X`.  -/
CategoryTheory.Limits.pullback_lift_diagonal_isPullback : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : C} [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  {S : C} (g : Y ⟶ X) (f : X ⟶ S),
  CategoryTheory.IsPullback g (CategoryTheory.Limits.pullback.lift (CategoryTheory.CategoryStruct.id Y) g ⋯)
    (CategoryTheory.Limits.pullback.diagonal f)
    (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp g f) f f f g
      (CategoryTheory.CategoryStruct.id X) (CategoryTheory.CategoryStruct.id S) ⋯ ⋯)
-- Mathlib.FieldTheory.Normal.Basic
IntermediateField.normal_sup : ∀ (F : Type u_1) (K : Type u_2) [inst : Field F] [inst_1 : Field K] [inst_2 : Algebra F K]
  (E E' : IntermediateField F K) [Normal F ↥E] [Normal F ↥E'], Normal F ↥(E ⊔ E')
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
/-- `ContinuousAlternatingMap.pi` as a `LinearEquiv`.  -/
ContinuousAlternatingMap.piLinearEquiv : {R : Type u_1} →
  {A : Type u_2} →
    {M : Type u_3} →
      {ι : Type u_5} →
        [inst : Semiring R] →
          [inst_1 : Semiring A] →
            [inst_2 : AddCommMonoid M] →
              [inst_3 : TopologicalSpace M] →
                [inst_4 : Module A M] →
                  {ι' : Type u_6} →
                    {M' : ι' → Type u_7} →
                      [inst_5 : (i : ι') → AddCommMonoid (M' i)] →
                        [inst_6 : (i : ι') → TopologicalSpace (M' i)] →
                          [inst_7 : ∀ (i : ι'), ContinuousAdd (M' i)] →
                            [inst_8 : (i : ι') → Module R (M' i)] →
                              [inst_9 : (i : ι') → Module A (M' i)] →
                                [inst_10 : ∀ (i : ι'), SMulCommClass A R (M' i)] →
                                  [inst_11 : ∀ (i : ι'), ContinuousConstSMul R (M' i)] →
                                    ((i : ι') → M [⋀^ι]→L[A] M' i) ≃ₗ[R] M [⋀^ι]→L[A] ((i : ι') → M' i)
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.instProperSpaceSubtypeComplexMemSubmoduleIntLattice : ∀ (L : PeriodPair), ProperSpace ↥L.lattice
-- Mathlib.Geometry.Euclidean.Sphere.Basic
EuclideanGeometry.Sphere.mk.inj : ∀ {P : Type u_2} {inst : MetricSpace P} {center : P} {radius : ℝ} {center_1 : P} {radius_1 : ℝ},
  { center := center, radius := radius } = { center := center_1, radius := radius_1 } →
    center = center_1 ∧ radius = radius_1
-- Mathlib.Algebra.Order.Ring.Archimedean
ArchimedeanClass.mk_inv : ∀ {R : Type u_1} [inst : LinearOrder R] [inst_1 : Field R] [inst_2 : IsOrderedRing R] (x : R),
  ArchimedeanClass.mk x⁻¹ = -ArchimedeanClass.mk x
-- Init.Data.Int.Gcd
Int.lcm_self : ∀ {a : ℤ}, a.lcm a = a.natAbs
-- Mathlib.CategoryTheory.Triangulated.TStructure.Induced
/-- The t-structure induced on a full subcategory.  -/
CategoryTheory.ObjectProperty.tStructure : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
        [inst_3 : CategoryTheory.HasShift C ℤ] →
          [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
            [inst_5 : CategoryTheory.Pretriangulated C] →
              (P : CategoryTheory.ObjectProperty C) →
                (t : CategoryTheory.Triangulated.TStructure C) →
                  [inst_6 : P.IsTriangulated] →
                    [h : P.HasInducedTStructure t] → CategoryTheory.Triangulated.TStructure P.FullSubcategory
-- Mathlib.Data.QPF.Univariate.Basic
/-- access the underlying W-type of a fixpoint data type  -/
QPF.fixToW : {F : Type u → Type u} → [q : QPF F] → QPF.Fix F → (QPF.P F).W
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.minEntry?ₘ'.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (l : Std.DTreeMap.Internal.Impl α β),
  l.minEntry?ₘ' =
    Std.DTreeMap.Internal.Impl.explore (fun x => Ordering.lt) none
      (fun sofar step =>
        match step with
        | Std.DTreeMap.Internal.Impl.ExplorationStep.lt ky a y a_1 => some ⟨ky, y⟩
        | Std.DTreeMap.Internal.Impl.ExplorationStep.eq a a_1 r => r.head?.or sofar)
      l
-- Init.Notation
/-- The attribute `@[suggest_for ..]` on a declaration suggests likely ways in which
someone might **incorrectly** refer to a definition.

* `@[suggest_for String.endPos]` on the definition of `String.rawEndPos` suggests that `"str".endPos` might be correctable to `"str".rawEndPos`.
* `@[suggest_for Either Result]` on the definition of `Except` suggests that `Either Nat String` might be correctable to `Except Nat String`.

The namespace of the suggestions is always relative to the root namespace. In the namespace `X.Y`,
adding an annotation `@[suggest_for Z.bar]` to `def Z.foo` will suggest `X.Y.Z.foo` only as a
replacement for `Z.foo`. If your intent is to suggest `X.Y.Z.foo` as a replacement for
`X.Y.Z.bar`, you must instead use the annotation `@[suggest_for X.Y.Z.bar]`.

Suggestions can be defined for structure fields or inductive branches with the
`attribute [suggest_for Exception] Except` syntax, and these attributes do not have to be added
in the same module where the actual identifier was defined.
 -/
Lean.suggest_for : Lean.ParserDescr
-- Mathlib.CategoryTheory.Limits.Creates
CategoryTheory.reflectsLimitsOfCreatesLimits : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [CategoryTheory.CreatesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F],
  CategoryTheory.Limits.ReflectsLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F
-- Mathlib.Data.Sym.Sym2
Sym2.forall_mem_pair : ∀ {α : Type u_1} {P : α → Prop} {a b : α}, (∀ x ∈ s(a, b), P x) ↔ P a ∧ P b
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
QuotientAddGroup.measurableSpace.eq_1 : ∀ {G : Type u_6} [inst : AddGroup G] [inst_1 : MeasurableSpace G] (S : AddSubgroup G),
  QuotientAddGroup.measurableSpace S = Quotient.instMeasurableSpace
-- Std.Internal.Parsec.Basic
/-- Parses one or more chars with `p` into a string, errors if none.
 -/
Std.Internal.Parsec.many1Chars : {ι elem idx : Type} →
  [inst : DecidableEq idx] →
    [inst_1 : DecidableEq elem] →
      [Std.Internal.Parsec.Input ι elem idx] → Std.Internal.Parsec ι Char → Std.Internal.Parsec ι String