mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Normed.Affine.MazurUlam
IsometryEquiv.coe_toRealLinearIsometryEquivOfMapZero_symm : ∀ {E : Type u_1} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] (f : E ≃ᵢ F) (h0 : f 0 = 0), ⇑(f.toRealLinearIsometryEquivOfMapZero h0).symm = ⇑f.symm
-- Mathlib.Logic.Relation
Relation.SymmGen.of_rel : ∀ {α : Type u_1} {r : α → α → Prop} {a b : α}, r a b → Relation.SymmGen r a b
-- Mathlib.LinearAlgebra.SModEq.Basic
SModEq.top : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {x y : M},
  x ≡ y [SMOD ⊤]
-- Mathlib.CategoryTheory.Comma.Over.StrictInitial
CategoryTheory.MorphismProperty.underEquivOfIsTerminal_functor : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P Q : CategoryTheory.MorphismProperty C)
  [inst_1 : P.ContainsIdentities] [inst_2 : Q.IsMultiplicative] [inst_3 : Q.RespectsIso]
  [inst_4 : CategoryTheory.Limits.HasStrictTerminalObjects C] (X : C) (h : CategoryTheory.Limits.IsTerminal X),
  (CategoryTheory.MorphismProperty.underEquivOfIsTerminal.{w, v_1, u_1} P Q X h).functor =
    CategoryTheory.Functor.star (P.Under Q X)
-- Mathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy
/-- A right homotopy on morphisms in the category of arrows of a preadditive category.  -/
CategoryTheory.Arrow.RightHomotopy : {V : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    [CategoryTheory.Preadditive V] → {u v : CategoryTheory.Arrow V} → (u ⟶ v) → (u ⟶ v) → Type v_1
-- Mathlib.Topology.Compactification.OnePoint.Basic
OnePoint.instFintype : {X : Type u_1} → [Fintype X] → Fintype (OnePoint X)
-- Mathlib.Logic.Relation
Relation.ReflTransGen.trans : ∀ {α : Type u_1} {r : α → α → Prop} {a b c : α},
  Relation.ReflTransGen r a b → Relation.ReflTransGen r b c → Relation.ReflTransGen r a c
-- Mathlib.CategoryTheory.Limits.Indization.IndObject
/-- Presheaves over a small finitely cocomplete category `C : Type u` are Ind-objects if and only if
they are left-exact.  -/
CategoryTheory.Limits.isIndObject_iff_preservesFiniteLimits : ∀ {C : Type u} [inst : CategoryTheory.SmallCategory C] [CategoryTheory.Limits.HasFiniteColimits C]
  (A : CategoryTheory.Functor Cᵒᵖ (Type u)),
  CategoryTheory.Limits.IsIndObject A ↔ CategoryTheory.Limits.PreservesFiniteLimits A
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.concat_eq_append : ∀ {V : Type u} {G : SimpleGraph V} {u v w : V} (p : G.Walk u v) (h : G.Adj v w),
  p.concat h = p.append (SimpleGraph.Walk.cons h SimpleGraph.Walk.nil)
-- Mathlib.Topology.Maps.Basic
Topology.IsOpenEmbedding.isEmbedding : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  Topology.IsOpenEmbedding f → Topology.IsEmbedding f
-- Lean.Expr
/-- Return `true` if the given expression is a bound variable.  -/
Lean.Expr.isBVar : Lean.Expr → Bool
-- Mathlib.Geometry.Manifold.Diffeomorph
Diffeomorph.symm_image_eq_preimage : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_4} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {H : Type u_5}
  [inst_5 : TopologicalSpace H] {G : Type u_7} [inst_6 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 F G} {M : Type u_9} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H M] {N : Type u_11}
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n : WithTop ℕ∞} (h : Diffeomorph I J M N n) (s : Set N),
  ⇑h.symm '' s = ⇑h ⁻¹' s
-- Lean.Meta.Basic
Lean.Meta.ExprParamInfo.mk : Lean.Name → Lean.Expr → Lean.BinderInfo → Lean.Meta.ExprParamInfo
-- Mathlib.RepresentationTheory.Continuous.Basic
ContIntertwiningMap.instZero : {R : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      {W : Type u_4} →
        [inst : Monoid G] →
          [inst_1 : Ring R] →
            [inst_2 : AddCommGroup V] →
              [inst_3 : TopologicalSpace V] →
                [inst_4 : IsTopologicalAddGroup V] →
                  [inst_5 : Module R V] →
                    [inst_6 : AddCommGroup W] →
                      [inst_7 : TopologicalSpace W] →
                        [inst_8 : IsTopologicalAddGroup W] →
                          [inst_9 : Module R W] →
                            {π₁ : ContRepresentation R G V} →
                              {π₂ : ContRepresentation R G W} → Zero (ContIntertwiningMap π₁ π₂)
-- Mathlib.Algebra.Homology.Embedding.Extend
/-- Auxiliary definition for `HomologicalComplex.extendMap`.  -/
HomologicalComplex.extend.mapX : {ι : Type u_1} →
  {c : ComplexShape ι} →
    {C : Type u_3} →
      [inst : CategoryTheory.Category.{v_1, u_3} C] →
        [inst_1 : CategoryTheory.Limits.HasZeroObject C] →
          [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
            {K L : HomologicalComplex C c} →
              (K ⟶ L) → (i : Option ι) → HomologicalComplex.extend.X K i ⟶ HomologicalComplex.extend.X L i
-- Mathlib.RingTheory.Algebraic.Defs
Algebra.Transcendental.mk : ∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A],
  (∃ x, Transcendental R x) → Algebra.Transcendental R A
-- Std.Tactic.BVDecide.Normalize.Bool
Std.Tactic.BVDecide.Normalize.Bool.ite_same_then : ∀ (c t e : Bool), ((bif c then t else e) == t) = (c || t == e)
-- Mathlib.SetTheory.Ordinal.Principal
Ordinal.isPrincipal_add_iff_add_lt_ne_self : ∀ {a : Ordinal.{u}}, Ordinal.IsPrincipal (fun x1 x2 => x1 + x2) a ↔ ∀ b < a, ∀ c < a, b + c ≠ a
-- Std.Time.Notation
_private.Std.Time.Notation.0.Std.Time.convertOffsetO : Std.Time.OffsetO → Lean.MacroM (Lean.TSyntax `term)
-- Mathlib.Topology.ContinuousMap.CocompactMap
CocompactMapClass.toContinuousMapClass : ∀ {F : Type u_1} {α : outParam (Type u_2)} {β : outParam (Type u_3)} {inst : TopologicalSpace α}
  {inst_1 : TopologicalSpace β} {inst_2 : FunLike F α β} [self : CocompactMapClass F α β], ContinuousMapClass F α β
-- Mathlib.CategoryTheory.Sites.Equivalence
CategoryTheory.Equivalence.sheafCongr_functor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] (K : CategoryTheory.GrothendieckTopology D) (e : C ≌ D) (A : Type u₃)
  [inst_2 : CategoryTheory.Category.{v₃, u₃} A] [inst_3 : CategoryTheory.Functor.IsDenseSubsite K J e.inverse],
  (CategoryTheory.Equivalence.sheafCongr J K e A).functor = CategoryTheory.Equivalence.sheafCongr.functor J K e A
-- Mathlib.NumberTheory.Height.Basic
/-- The multiplicative height of a tuple of elements of `K`.
For the zero tuple we take the junk value `1`.  -/
Height.mulHeight : {K : Type u_1} → [inst : Field K] → [Height.AdmissibleAbsValues K] → {ι : Type u_2} → (ι → K) → ℝ
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Unit.RioSliceData.treeMap : {α : Type u} → [inst : Ord α] → Std.DTreeMap.Internal.Unit.RioSliceData α → Std.DTreeMap.Internal.Impl α fun x => Unit
-- Mathlib.Algebra.Order.Group.Synonym
Lex.instIsRightCancelMul : ∀ {α : Type u_1} [inst : Mul α] [IsRightCancelMul α], IsRightCancelMul (Lex α)
-- Lean.Elab.Attributes
Lean.Elab.instToFormatAttribute : Std.ToFormat Lean.Elab.Attribute
-- Mathlib.Order.SuccPred.CompleteLinearOrder
IsLUB.exists_of_nonempty_of_not_isSuccPrelimit : ∀ {ι : Sort u_1} {α : Type u_2} [inst : ConditionallyCompleteLinearOrder α] [Nonempty ι] {f : ι → α} {x : α},
  IsLUB (Set.range f) x → ¬Order.IsSuccPrelimit x → ∃ i, f i = x
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.isReduced_cons_cons : ∀ {α : Type u} {L : List (α × Bool)} {a b : α × Bool},
  FreeAddGroup.IsReduced (a :: b :: L) ↔ (a.1 = b.1 → a.2 = b.2) ∧ FreeAddGroup.IsReduced (b :: L)
-- Std.Async.Basic
Std.Async.instMonadAwaitReaderTOfMonad : {m t : Type → Type} → {n : Type} → [Monad m] → [Std.Async.MonadAwait t m] → Std.Async.MonadAwait t (ReaderT n m)
-- Mathlib.Algebra.Group.Opposite
MulOpposite.instMulOneClass : {α : Type u_1} → [MulOneClass α] → MulOneClass αᵐᵒᵖ
-- Mathlib.Algebra.Category.Ring.Constructions
CommRingCat.closure_range_union_range_eq_top_of_isPushout : ∀ {R A B X : CommRingCat} {f : R ⟶ A} {g : R ⟶ B} {a : A ⟶ X} {b : B ⟶ X},
  CategoryTheory.IsPushout f g a b →
    Subring.closure
        (Set.range ⇑(CategoryTheory.ConcreteCategory.hom a) ∪ Set.range ⇑(CategoryTheory.ConcreteCategory.hom b)) =
      ⊤
-- Mathlib.RingTheory.PowerSeries.Schroder
PowerSeries.largeSchroderSeries.eq_1 : PowerSeries.largeSchroderSeries = PowerSeries.mk Nat.largeSchroder
-- Mathlib.Algebra.Order.Ring.Unbundled.Rat
Rat.mkRat_nonneg_iff : ∀ (a : ℤ) {b : ℕ}, b ≠ 0 → (0 ≤ mkRat a b ↔ 0 ≤ a)
-- Init.Data.Bool
Bool.coe_false_iff_false : ∀ {a b : Bool}, (a = false ↔ b = false) ↔ (!a) = !b
-- Mathlib.Analysis.Complex.Basic
RCLike.hasSum_im : ∀ {α : Type u_1} (𝕜 : Type u_2) [inst : RCLike 𝕜] {L : SummationFilter α} {f : α → 𝕜} {x : 𝕜},
  HasSum f x L → HasSum (fun x => RCLike.im (f x)) (RCLike.im x) L
-- Mathlib.Topology.Category.TopCat.Limits.Pullbacks
TopCat.pullbackIsoProdSubtype.eq_1 : ∀ {X Y Z : TopCat} (f : X ⟶ Z) (g : Y ⟶ Z),
  TopCat.pullbackIsoProdSubtype f g =
    (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Limits.cospan f g)).conePointUniqueUpToIso
      (TopCat.pullbackConeIsLimit f g)
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.IsAffine.affine : ∀ {X : AlgebraicGeometry.Scheme} [self : AlgebraicGeometry.IsAffine X], CategoryTheory.IsIso X.toSpecΓ
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
CategoryTheory.Limits.Cofork.unop_op_π : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : Cᵒᵖ} {f g : X ⟶ Y}
  (c : CategoryTheory.Limits.Cofork f g), c.unop.op.π = c.π
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Localization.induction_on : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {p : Localization S → Prop} (x : Localization S),
  (∀ (y : M × ↥S), p (Localization.mk y.1 y.2)) → p x
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.HomologyData.ofIso_left_π : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (e : S₁ ≅ S₂) (h : S₁.HomologyData),
  (CategoryTheory.ShortComplex.HomologyData.ofIso e h).left.π = h.left.π
-- Mathlib.CategoryTheory.Monoidal.Action.Opposites
CategoryTheory.MonoidalCategory.MonoidalRightAction.monoidalOppositeRightAction_actionHom : ∀ (C : Type u_1) (D : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] {c c' : Cᴹᵒᵖ} {d d' : D} (f : d ⟶ d') (g : c ⟶ c'),
  CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHom f g =
    CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHom g.unmop f
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.Equalizer.lift_apply_coe : ∀ {V : Type u_1} {W : Type u_2} {V₁ : Type u_3} [inst : SeminormedAddCommGroup V] [inst_1 : SeminormedAddCommGroup W]
  [inst_2 : SeminormedAddCommGroup V₁] {f g : NormedAddGroupHom V W} (φ : NormedAddGroupHom V₁ V)
  (h : f.comp φ = g.comp φ) (v : V₁), ↑((NormedAddGroupHom.Equalizer.lift φ h) v) = φ v
-- Mathlib.CategoryTheory.EpiMono
/-- Split monomorphisms are also absolute monomorphisms.  -/
CategoryTheory.SplitMono.map : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {X Y : C} →
          {f : Y ⟶ X} →
            CategoryTheory.SplitMono f → (F : CategoryTheory.Functor C D) → CategoryTheory.SplitMono (F.map f)
-- Mathlib.Topology.Algebra.RestrictedProduct.Units
RestrictedProduct.isUnit_of_eventually_isUnit : ∀ {ι : Type u_1} {R : ι → Type u_2} [inst : (i : ι) → Monoid (R i)] {S : ι → Type u_3}
  [inst_1 : (i : ι) → SetLike (S i) (R i)] [inst_2 : ∀ (i : ι), SubmonoidClass (S i) (R i)] {B : (i : ι) → S i}
  {𝓕 : Filter ι} {x : RestrictedProduct (fun i => R i) (fun i => ↑(B i)) 𝓕},
  (∀ (i : ι), IsUnit (x i)) → (∀ᶠ (i : ι) in 𝓕, ∃ (h : x i ∈ B i), IsUnit ⟨x i, h⟩) → IsUnit x
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.instNonUnitalSemiringOfIsTopologicalSemiring : {α : Type u_2} →
  {β : Type u_3} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] →
        [inst_2 : NonUnitalSemiring β] →
          [IsTopologicalSemiring β] → NonUnitalSemiring (CompactlySupportedContinuousMap α β)
-- Mathlib.Computability.PartrecBasis
Nat.Partrec'.nil : ∀ {n : ℕ}, Nat.Partrec'.Vec fun x => List.Vector.nil
-- Batteries.Data.Nat.Basic
Nat.strongRecMeasure.eq_def : ∀ {α : Sort u_1} (f : α → ℕ) {motive : α → Sort u_2} (ind : (x : α) → ((y : α) → f y < f x → motive y) → motive x)
  (x : α), Nat.strongRecMeasure f ind x = ind x fun y x => Nat.strongRecMeasure f ind y
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.instIsIsoMapOfMono : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  (f : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasKernel f] {X' Y' : C} (f' : X' ⟶ Y')
  [inst_3 : CategoryTheory.Limits.HasKernel f'] (p : X ⟶ X') (q : Y ⟶ Y')
  (w : CategoryTheory.CategoryStruct.comp f q = CategoryTheory.CategoryStruct.comp p f') [CategoryTheory.IsIso p]
  [CategoryTheory.Mono q], CategoryTheory.IsIso (CategoryTheory.Limits.kernel.map f f' p q w)
-- Aesop.RuleTac.Forward
Aesop.RuleTac.ForwardM : Type → Type
-- Mathlib.Data.PFunctor.Multivariate.M
MvPFunctor.M.bisim_lemma : ∀ {n : ℕ} (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u} n} {a₁ : P.mp.A} {f₁ : (P.mp.B a₁).Arrow α} {a' : P.A}
  {f' : (P.B a').drop.Arrow α} {f₁' : (P.B a').last → P.M α},
  MvPFunctor.M.dest P ⟨a₁, f₁⟩ = ⟨a', TypeVec.splitFun f' f₁'⟩ →
    ∃ g₁',
      ∃ (e₁' : PFunctor.M.dest a₁ = ⟨a', g₁'⟩),
        f' = MvPFunctor.M.pathDestLeft P e₁' f₁ ∧ f₁' = fun x => ⟨g₁' x, MvPFunctor.M.pathDestRight P e₁' f₁ x⟩
-- Mathlib.Data.Fin.Tuple.Basic
Fin.le_find_iff : ∀ {n : ℕ} {p : Fin n → Prop} [inst : DecidablePred p] (h : ∃ k, p k) (i : Fin n), i ≤ Fin.find p h ↔ ∀ m < i, ¬p m
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
PowerSeries.IsWeierstrassFactorizationAt.smul : ∀ {A : Type u_1} [inst : CommRing A] {g : PowerSeries A} {f : Polynomial A} {h : PowerSeries A} {I : Ideal A},
  g.IsWeierstrassFactorizationAt f h I → ∀ {a : A}, IsUnit a → (a • g).IsWeierstrassFactorizationAt f (a • h) I
-- Std.Data.DHashMap.Internal.Model
Std.DHashMap.Internal.bucket.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Hashable α] (self : Array (Std.DHashMap.Internal.AssocList α β))
  (h : 0 < self.size) (k : α),
  Std.DHashMap.Internal.bucket self h k =
    match Std.DHashMap.Internal.mkIdx self.size h (hash k) with
    | ⟨i, h⟩ => self[i]
-- Init.Data.String.Lemmas.Pattern.Find.Pred
String.Pos.find?_bool_eq_some_iff_splits : ∀ {p : Char → Bool} {s : String} {pos : s.Pos} {t u : String},
  pos.Splits t u →
    ∀ {pos' : s.Pos},
      pos.find? p = some pos' ↔
        ∃ v c w, pos'.Splits (t ++ v) (String.singleton c ++ w) ∧ p c = true ∧ ∀ d ∈ v.toList, p d = false
-- Lean.Meta.Sym.ReplaceS
_private.Lean.Meta.Sym.ReplaceS.0.Lean.Meta.Sym.visit.match_1.eq_9 : ∀ (motive : Lean.Expr → Sort u_1) (typeName : Lean.Name) (idx : ℕ) (a : Lean.Expr)
  (h_1 : (a : Lean.Literal) → motive (Lean.Expr.lit a)) (h_2 : (mvarId : Lean.MVarId) → motive (Lean.Expr.mvar mvarId))
  (h_3 : (deBruijnIndex : ℕ) → motive (Lean.Expr.bvar deBruijnIndex))
  (h_4 : (fvarId : Lean.FVarId) → motive (Lean.Expr.fvar fvarId))
  (h_5 : (declName : Lean.Name) → (us : List Lean.Level) → motive (Lean.Expr.const declName us))
  (h_6 : (u : Lean.Level) → motive (Lean.Expr.sort u)) (h_7 : (f a : Lean.Expr) → motive (f.app a))
  (h_8 : (data : Lean.MData) → (a : Lean.Expr) → motive (Lean.Expr.mdata data a))
  (h_9 : (typeName : Lean.Name) → (idx : ℕ) → (a : Lean.Expr) → motive (Lean.Expr.proj typeName idx a))
  (h_10 :
    (binderName : Lean.Name) →
      (d b : Lean.Expr) → (binderInfo : Lean.BinderInfo) → motive (Lean.Expr.forallE binderName d b binderInfo))
  (h_11 :
    (binderName : Lean.Name) →
      (d b : Lean.Expr) → (binderInfo : Lean.BinderInfo) → motive (Lean.Expr.lam binderName d b binderInfo))
  (h_12 :
    (declName : Lean.Name) → (t v b : Lean.Expr) → (nondep : Bool) → motive (Lean.Expr.letE declName t v b nondep)),
  (match Lean.Expr.proj typeName idx a with
    | Lean.Expr.lit a => h_1 a
    | Lean.Expr.mvar mvarId => h_2 mvarId
    | Lean.Expr.bvar deBruijnIndex => h_3 deBruijnIndex
    | Lean.Expr.fvar fvarId => h_4 fvarId
    | Lean.Expr.const declName us => h_5 declName us
    | Lean.Expr.sort u => h_6 u
    | f.app a => h_7 f a
    | Lean.Expr.mdata data a => h_8 data a
    | Lean.Expr.proj typeName idx a => h_9 typeName idx a
    | Lean.Expr.forallE binderName d b binderInfo => h_10 binderName d b binderInfo
    | Lean.Expr.lam binderName d b binderInfo => h_11 binderName d b binderInfo
    | Lean.Expr.letE declName t v b nondep => h_12 declName t v b nondep) =
    h_9 typeName idx a
-- Mathlib.Analysis.Fourier.AddCircleMulti
/-- **Parseval's identity** for norms: for an `L²` function `f` on `UnitAddTorus d`, the sum of the
squared norms of the Fourier coefficients equals the `L²` norm of `f`.  -/
UnitAddTorus.hasSum_sq_mFourierCoeff : ∀ {d : Type u_1} [inst : Fintype d] (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)),
  HasSum (fun i => ‖UnitAddTorus.mFourierCoeff (↑↑f) i‖ ^ 2) (∫ (t : UnitAddTorus d), ‖↑↑f t‖ ^ 2)
-- Mathlib.NumberTheory.NumberField.Completion.FinitePlace
/-- **Alias** of `NumberField.HeightOneSpectrum.one_lt_absNorm`.

---

The norm of a maximal ideal is `> 1`  -/
NumberField.RingOfIntegers.HeightOneSpectrum.one_lt_absNorm : ∀ {R : Type u_2} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R)
  [Module.Finite ℤ R] [inst_3 : Module.Free ℤ R], 1 < Ideal.absNorm v.asIdeal
-- Mathlib.Data.Set.Monotone
StrictMonoOn.eq_1 : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] (f : α → β) (s : Set α),
  StrictMonoOn f s = ∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ s → a < b → f a < f b
-- Mathlib.Probability.Kernel.Category.SFinKer
SFinKer.braiding_inv_hom : ∀ (X Y : SFinKer), (β_ X Y).inv.hom = ProbabilityTheory.Kernel.swap Y.carrier X.carrier
-- Batteries.Classes.Order
Std.LawfulBCmp.toLawfulLECmp : ∀ {α : Type u_1} [inst : LE α] [inst_1 : LT α] [inst_2 : BEq α] {cmp : α → α → Ordering} [self : Std.LawfulBCmp cmp],
  Std.LawfulLECmp cmp
-- Mathlib.Topology.UniformSpace.Ascoli
/-- **Alias** of the forward direction of `EquicontinuousOn.isClosed_range_uniformOnFun_iff_pi`.

---

Let `X` be a topological space, `𝔖` a covering of `X` by compact subsets, and
`α` a uniform space. An equicontinuous subset of `X → α` is closed in the topology of uniform
convergence on all `K ∈ 𝔖` iff it is closed in the topology of pointwise convergence.

This is a specialization of `EquicontinuousOn.isClosed_range_pi_of_uniformOnFun'` to the case where
`𝔖` covers `X`.  -/
EquicontinuousOn.isClosed_range_pi_of_uniformOnFun : ∀ {ι : Type u_1} {X : Type u_2} {α : Type u_3} [inst : TopologicalSpace X] [inst_1 : UniformSpace α] {F : ι → X → α}
  {𝔖 : Set (Set X)},
  (∀ K ∈ 𝔖, IsCompact K) →
    ⋃₀ 𝔖 = Set.univ →
      (∀ K ∈ 𝔖, EquicontinuousOn F K) → IsClosed (Set.range (⇑(UniformOnFun.ofFun 𝔖) ∘ F)) → IsClosed (Set.range F)
-- Mathlib.Topology.Compactness.Lindelof
nonLindelof_univ : ∀ (X : Type u_2) [inst : TopologicalSpace X] [NonLindelofSpace X], ¬IsLindelof Set.univ
-- Init.Data.Int.Linear
Int.Internal.Linear.eq_def : ∀ (ctx : Int.Internal.Linear.Context) (x : Int.Internal.Linear.Var) (xPoly p : Int.Internal.Linear.Poly),
  Int.Internal.Linear.eq_def_cert x xPoly p = true →
    Int.Internal.Linear.Var.denote ctx x = Int.Internal.Linear.Poly.denote' ctx xPoly →
      Int.Internal.Linear.Poly.denote' ctx p = 0
-- Mathlib.FieldTheory.SeparableClosure
/-- **Alias** of `separableClosure.algEquivOfAlgEquiv`.

---

If `E` and `K` are isomorphic as `F`-algebras, then `separableClosure F E` and
`separableClosure F K` are also isomorphic as `F`-algebras.  -/
AlgEquiv.separableClosure : {F : Type u} →
  {E : Type v} →
    [inst : Field F] →
      [inst_1 : Field E] →
        [inst_2 : Algebra F E] →
          {K : Type w} →
            [inst_3 : Field K] →
              [inst_4 : Algebra F K] → (E ≃ₐ[F] K) → ↥(separableClosure F E) ≃ₐ[F] ↥(separableClosure F K)
-- Mathlib.MeasureTheory.Integral.Average
/-- **First moment method**. The maximum of a measurable function is greater than its mean.  -/
MeasureTheory.exists_setLAverage_le : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {f : α → ENNReal},
  μ s ≠ 0 → MeasureTheory.NullMeasurableSet s μ → ∫⁻ (a : α) in s, f a ∂μ ≠ ⊤ → ∃ x ∈ s, ⨍⁻ (a : α) in s, f a ∂μ ≤ f x
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.mk_preimage_of_injective_of_subset_range_lift : ∀ {α : Type u} {β : Type v} (f : α → β) (s : Set β),
  Function.Injective f →
    s ⊆ Set.range f → Cardinal.lift.{v, u} (Cardinal.mk ↑(f ⁻¹' s)) = Cardinal.lift.{u, v} (Cardinal.mk ↑s)
-- Mathlib.Analysis.Convex.Segment
segment_eq_image_lineMap : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : Ring 𝕜] [inst_1 : PartialOrder 𝕜] [AddRightMono 𝕜] [inst_3 : AddCommGroup E]
  [inst_4 : Module 𝕜 E] (x y : E), segment 𝕜 x y = ⇑(AffineMap.lineMap x y) '' Set.Icc 0 1
-- Mathlib.CategoryTheory.Monoidal.DayConvolution.Braided
CategoryTheory.MonoidalCategory.DayConvolution.unit_app_braiding_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.BraidedCategory C]
  [inst_4 : CategoryTheory.MonoidalCategory V] [inst_5 : CategoryTheory.BraidedCategory V]
  (F G : CategoryTheory.Functor C V) [inst_6 : CategoryTheory.MonoidalCategory.DayConvolution F G]
  [inst_7 : CategoryTheory.MonoidalCategory.DayConvolution G F] (x y : C),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategory.DayConvolution.unit F G).app (x, y))
      ((CategoryTheory.MonoidalCategory.DayConvolution.braiding F G).hom.app
        (CategoryTheory.MonoidalCategoryStruct.tensorObj x y)) =
    CategoryTheory.CategoryStruct.comp (β_ ((G, F).2.obj (y, x).2) ((G, F).1.obj (y, x).1)).hom
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategory.DayConvolution.unit G F).app (y, x))
        ((CategoryTheory.MonoidalCategory.DayConvolution.convolution G F).map (β_ (y, x).1 (y, x).2).hom))
-- Mathlib.Analysis.LocallyConvex.AbsConvex
convexHull_union_neg_eq_absConvexHull : ∀ {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {s : Set E},
  (convexHull ℝ) (s ∪ -s) = (absConvexHull ℝ) s
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
WithZero.expOrderIso_symm_apply : ∀ {G : Type u_3} [inst : Preorder G] [inst_1 : AddGroup G] (a : (WithZero (Multiplicative G))ˣ),
  (RelIso.symm WithZero.expOrderIso) a = Multiplicative.toAdd (WithZero.unzero ⋯)
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Presieve.BindStruct.mk.injEq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} {S : CategoryTheory.Presieve X}
  {R : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → S f → CategoryTheory.Presieve Y} {Z : C} {h : Z ⟶ X} (Y : C) (g : Z ⟶ Y) (f : Y ⟶ X)
  (hf : S f) (hg : R hf g) (fac : CategoryTheory.CategoryStruct.comp g f = h) (Y_1 : C) (g_1 : Z ⟶ Y_1) (f_1 : Y_1 ⟶ X)
  (hf_1 : S f_1) (hg_1 : R hf_1 g_1) (fac_1 : CategoryTheory.CategoryStruct.comp g_1 f_1 = h),
  ({ Y := Y, g := g, f := f, hf := hf, hg := hg, fac := fac } =
      { Y := Y_1, g := g_1, f := f_1, hf := hf_1, hg := hg_1, fac := fac_1 }) =
    (Y = Y_1 ∧ g ≍ g_1 ∧ f ≍ f_1)
-- Mathlib.Combinatorics.Graph.Basic
Graph.IsLoopAt.vertex_mem : ∀ {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β}, G.IsLoopAt e x → x ∈ G.vertexSet