mathlib-initiative/mathlib-types huggingface dataset:
-- Batteries.Data.AssocList
Batteries.AssocList.brecOn.eq : ∀ {α : Type u} {β : Type v} {motive : Batteries.AssocList α β → Sort u_1} (t : Batteries.AssocList α β)
  (F_1 : (t : Batteries.AssocList α β) → Batteries.AssocList.below t → motive t),
  Batteries.AssocList.brecOn t F_1 = F_1 t (Batteries.AssocList.brecOn.go t F_1).2
-- Mathlib.Combinatorics.Tiling.Tile
/-- The index of the tile in the protoset.  -/
DiscreteTiling.PlacedTile.index : {G : Type u_1} →
  {X : Type u_2} →
    {ιₚ : Type u_3} →
      [inst : Group G] →
        [inst_1 : MulAction G X] → {ps : DiscreteTiling.Protoset G X ιₚ} → DiscreteTiling.PlacedTile ps → ιₚ
-- Mathlib.Algebra.Group.ULift
ULift.addGroup.eq_1 : ∀ {α : Type u} [inst : AddGroup α], ULift.addGroup = Function.Injective.addGroup ⇑Equiv.ulift ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
-- Mathlib.CategoryTheory.Sites.Descent.IsPrestack
/-- Compatibility isomorphism of `Pseudofunctor.presheafHom` with "restrictions".  -/
CategoryTheory.Pseudofunctor.overMapCompPresheafHomIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat) →
      {S : C} →
        (M N : ↑(F.obj { as := Opposite.op S })) →
          {S' : C} →
            (q : S' ⟶ S) →
              (CategoryTheory.Over.map q).op.comp (F.presheafHom M N) ≅
                F.presheafHom ((F.map q.op.toLoc).toFunctor.obj M) ((F.map q.op.toLoc).toFunctor.obj N)
-- Mathlib.Data.Set.Function
Function.Semiconj.surjOn_range : ∀ {α : Type u_1} {β : Type u_2} {fa : α → α} {fb : β → β} {f : α → β},
  Function.Semiconj f fa fb → Function.Surjective fa → Set.SurjOn fb (Set.range f) (Set.range f)
-- Mathlib.CategoryTheory.Enriched.FunctorCategory
CategoryTheory.Enriched.FunctorCategory.diagram_obj_obj : ∀ (V : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} C] {J : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} J]
  [inst_4 : CategoryTheory.EnrichedOrdinaryCategory V C] (F₁ F₂ : CategoryTheory.Functor J C) (X : Jᵒᵖ) (X_1 : J),
  ((CategoryTheory.Enriched.FunctorCategory.diagram V F₁ F₂).obj X).obj X_1 = F₁.obj (Opposite.unop X) ⟶[V] F₂.obj X_1
-- Lean.Meta.Sym.SymM
_private.Lean.Meta.Sym.SymM.0.Lean.Meta.Sym.registerSymExtension.unsafe_1 : {σ : Type} → Lean.Meta.Sym.SymExtension σ → Lean.Meta.Sym.SymExtension Lean.Meta.Sym.SymExtensionState
-- Mathlib.RepresentationTheory.Coinduced
Rep.coind'_ext_iff : ∀ {k : Type u} {G : Type v} {H : Type w} [inst : CommRing k] [inst_1 : Monoid G] [inst_2 : Monoid H] {φ : G →* H}
  {A : Rep.{max u w, u, v} k G} {f g : ↑(Rep.coind' φ A)},
  f = g ↔
    ∀ (h : H),
      (Rep.Hom.hom f).toLinearMap (MonoidAlgebra.single h 1) = (Rep.Hom.hom g).toLinearMap (MonoidAlgebra.single h 1)
-- Mathlib.CategoryTheory.Subfunctor.Equalizer
CategoryTheory.Subfunctor.equalizer_le : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F₁ F₂ : CategoryTheory.Functor C (Type w)}
  {A : CategoryTheory.Subfunctor F₁} (f g : A.toFunctor ⟶ F₂), CategoryTheory.Subfunctor.equalizer f g ≤ A
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.ne_neg : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) (i : ι) [NeZero 2]
  [IsDomain R], i ≠ -i
-- Lean.Elab.InfoTree.Types
Lean.Elab.FieldInfo.mk : Lean.Name → Lean.Name → Lean.LocalContext → Lean.Expr → Lean.Syntax → Lean.Elab.FieldInfo
-- Mathlib.Data.List.Lattice
List.bagInter.induct_unfolding : ∀ {α : Type u_1} [inst : BEq α] (motive : List α → List α → List α → Prop),
  (∀ (x : List α), motive [] x []) →
    (∀ (t : List α), (t = [] → False) → motive t [] []) →
      (∀ (a : α) (l₁ l₂ : List α),
          (l₂ = [] → False) →
            List.elem a l₂ = true →
              motive l₁ (l₂.erase a) (l₁.bagInter (l₂.erase a)) → motive (a :: l₁) l₂ (a :: l₁.bagInter (l₂.erase a))) →
        (∀ (a : α) (l₁ l₂ : List α),
            (l₂ = [] → False) →
              ¬List.elem a l₂ = true → motive l₁ l₂ (l₁.bagInter l₂) → motive (a :: l₁) l₂ (l₁.bagInter l₂)) →
          ∀ (a a_1 : List α), motive a a_1 (a.bagInter a_1)
-- Mathlib.Data.Finset.Sups
Finset.infs_infs_infs_comm : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SemilatticeInf α] (s t u v : Finset α),
  s ⊼ t ⊼ (u ⊼ v) = s ⊼ u ⊼ (t ⊼ v)
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.prod_dist_eq_sup : ∀ {α : Type u_2} {β : Type u_3} [inst : Dist α] [inst_1 : Dist β] (f g : WithLp ⊤ (α × β)),
  dist f g = max (dist f.fst g.fst) (dist f.snd g.snd)
-- Mathlib.CategoryTheory.LocallyCartesianClosed.Over
CategoryTheory.toOverPullbackIsoToOver_inv_app_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {X Y : C} (f : Y ⟶ X) [inst_2 : CategoryTheory.ChosenPullbacksAlong f] (X_1 : C),
  ((CategoryTheory.toOverPullbackIsoToOver f).inv.app X_1).left =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Over.Hom.left
        ((CategoryTheory.ChosenPullbacksAlong.mapPullbackAdj f).unit.app ((CategoryTheory.toOver Y).obj X_1)))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Over.Hom.left
          ((CategoryTheory.ChosenPullbacksAlong.pullback f).map
            (CategoryTheory.Over.homMk
              (CategoryTheory.CartesianMonoidalCategory.lift
                (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj X_1 Y))
                (CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.snd X_1 Y) f))
              ⋯)))
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Over.Hom.left
            ((CategoryTheory.ChosenPullbacksAlong.pullback f).map
              (CategoryTheory.Over.homMk
                (CategoryTheory.MonoidalCategoryStruct.whiskerRight
                  ((CategoryTheory.Over.mapForget f).inv.app ((CategoryTheory.toOver Y).obj X_1)) X)
                ⋯)))
          (CategoryTheory.Over.Hom.left
            ((CategoryTheory.ChosenPullbacksAlong.pullback f).map
              (CategoryTheory.Over.homMk
                (CategoryTheory.MonoidalCategoryStruct.whiskerRight
                  (CategoryTheory.SemiCartesianMonoidalCategory.fst X_1 Y) X)
                ⋯)))))
-- Mathlib.RingTheory.Finiteness.FiniteTypeLocal
/-- Finite-type can be checked on a standard covering of the target.  -/
Algebra.FiniteType.of_span_eq_top_target : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (s : Set S),
  Ideal.span s = ⊤ → (∀ x ∈ s, Algebra.FiniteType R (Localization.Away x)) → Algebra.FiniteType R S
-- Mathlib.CategoryTheory.Conj
CategoryTheory.Iso.refl_conj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} (f : CategoryTheory.End X),
  (CategoryTheory.Iso.refl X).conj f = f
-- Mathlib.Algebra.Order.Hom.Basic
/-- the image of a sum is less or equal than the maximum of the images.  -/
NonarchimedeanHomClass.map_add_le_max : ∀ {F : Type u_7} {α : outParam (Type u_8)} {β : outParam (Type u_9)} {inst : Add α} {inst_1 : LinearOrder β}
  {inst_2 : FunLike F α β} [self : NonarchimedeanHomClass F α β] (f : F) (a b : α), f (a + b) ≤ max (f a) (f b)
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toList_rcc_add_right_eq_map : ∀ {m n : ℤ}, (m...=m + n).toList = List.map (fun x => x + m) (0...=n).toList
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
/-- The `ℝ`-basis of the mixed space of `K` formed by the vector equal to `1` at `w` and `0`
elsewhere for `IsReal w` and by the couple of vectors equal to `1` (resp. `I`) at `w` and `0`
elsewhere for `IsComplex w`.  -/
NumberField.mixedEmbedding.stdBasis : (K : Type u_1) →
  [inst : Field K] →
    [NumberField K] → Module.Basis (NumberField.mixedEmbedding.index K) ℝ (NumberField.mixedEmbedding.mixedSpace K)
-- Mathlib.Analysis.RCLike.Basic
RCLike.norm_nnqsmul : ∀ (K : Type u_1) {E : Type u_2} [inst : RCLike K] [inst_1 : NormedField E] [inst_2 : CharZero E] [NormedSpace K E]
  (q : ℚ≥0) (x : E), ‖q • x‖ = q • ‖x‖
-- Mathlib.ModelTheory.Algebra.Ring.Basic
/-- The type of Ring functions, to be used in the definition of the language of rings.
It contains the operations `(+,*,-,0,1)`  -/
FirstOrder.ringFunc : ℕ → Type
-- Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
SSet.Truncated.Edge.map_tensorHom : ∀ {X Y X' Y' : SSet.Truncated 2}
  {x x' : X.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge.tensor._proof_1 })}
  (e₁ : SSet.Truncated.Edge x x')
  {y y' : Y.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge.tensor._proof_1 })}
  (e₂ : SSet.Truncated.Edge y y') (f : X ⟶ X') (g : Y ⟶ Y'),
  (e₁.tensor e₂).map (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) = (e₁.map f).tensor (e₂.map g)
-- Std.Time.Zoned.Database.TzIf
/-- Represents version 2 of the TZif format, extending TZifV1 with an optional footer.
 -/
Std.Time.TimeZone.TZif.TZifV2 : Type
-- Init.Data.UInt.Bitwise
UInt64.or_neg_one : ∀ {a : UInt64}, a ||| -1 = -1
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.isRevMatch_cast_iff : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s t : String.Slice} (h : s.copy = t.copy)
  {pos : s.Pos}, String.Slice.Pattern.Model.IsRevMatch pat (pos.cast h) ↔ String.Slice.Pattern.Model.IsRevMatch pat pos
-- Mathlib.Analysis.Normed.Operator.Bilinear
ContinuousLinearMap.le_opNorm₂ : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {E : Type u_4} {F : Type u_6} {G : Type u_8}
  [inst : SeminormedAddCommGroup E] [inst_1 : SeminormedAddCommGroup F] [inst_2 : SeminormedAddCommGroup G]
  [inst_3 : NontriviallyNormedField 𝕜] [inst_4 : NontriviallyNormedField 𝕜₂] [inst_5 : NontriviallyNormedField 𝕜₃]
  [inst_6 : NormedSpace 𝕜 E] [inst_7 : NormedSpace 𝕜₂ F] [inst_8 : NormedSpace 𝕜₃ G] {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃}
  [inst_9 : RingHomIsometric σ₂₃] [RingHomIsometric σ₁₃] (f : E →SL[σ₁₃] F →SL[σ₂₃] G) (x : E) (y : F),
  ‖(f x) y‖ ≤ ‖f‖ * ‖x‖ * ‖y‖
-- Mathlib.ModelTheory.LanguageMap
/-- A language homomorphism is an expansion on a structure if it commutes with the interpretation of
all symbols on that structure.  -/
FirstOrder.Language.LHom.IsExpansionOn : {L : FirstOrder.Language} →
  {L' : FirstOrder.Language} → (L →ᴸ L') → (M : Type u_1) → [L.Structure M] → [L'.Structure M] → Prop
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.getD_union_of_not_mem_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {fallback : β},
  k ∉ m₁ → Std.ExtDHashMap.Const.getD (m₁.union m₂) k fallback = Std.ExtDHashMap.Const.getD m₂ k fallback
-- Mathlib.Order.UpperLower.Basic
isUpperSet_empty : ∀ {α : Type u_1} [inst : LE α], IsUpperSet ∅
-- Mathlib.Order.ConditionallyCompletePartialOrder.Defs
Directed.ciSup_le : ∀ {ι : Sort u_1} {α : Type u_2} [inst : ConditionallyCompletePartialOrderSup α] {f : ι → α} {a : α} [Nonempty ι],
  Directed (fun x1 x2 => x1 ≤ x2) f → (∀ (i : ι), f i ≤ a) → ⨆ i, f i ≤ a
-- Mathlib.Algebra.Group.Subgroup.Ker
AddMonoidHom.range_comp : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} {P : Type u_6} [inst_1 : AddGroup N] [inst_2 : AddGroup P]
  (g : N →+ P) (f : G →+ N), (g.comp f).range = AddSubgroup.map g f.range
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.Semiring.mulFn? : Lean.Meta.Grind.Arith.CommRing.Semiring → Option Lean.Expr
-- Mathlib.LinearAlgebra.BilinearMap
IsBilinearMap.smul_left : ∀ {R : Type u_1} [inst : CommSemiring R] {E : Type u_2} [inst_1 : AddCommMonoid E] [inst_2 : Module R E] {F : Type u_3}
  [inst_3 : AddCommMonoid F] [inst_4 : Module R F] {G : Type u_4} [inst_5 : AddCommMonoid G] [inst_6 : Module R G]
  {f : E → F → G}, IsBilinearMap R f → ∀ (c : R) (x : E) (y : F), f (c • x) y = c • f x y
-- Mathlib.Data.Finset.Prod
Finset.diag_eq_empty : ∀ {α : Type u_1} {s : Finset α}, s.diag = ∅ ↔ s = ∅
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
/-- The n-skeleton as an endofunctor on `SimplicialObject C`.  -/
CategoryTheory.SimplicialObject.sk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (n : ℕ) →
      [∀ (F : CategoryTheory.Functor (SimplexCategory.Truncated n)ᵒᵖ C),
            (SimplexCategory.Truncated.inclusion n).op.HasLeftKanExtension F] →
        CategoryTheory.Functor (CategoryTheory.SimplicialObject C) (CategoryTheory.SimplicialObject C)
-- Init.Data.Vector.Range
Vector.range'_append : ∀ {s m n step : ℕ}, Vector.range' s m step ++ Vector.range' (s + step * m) n step = Vector.range' s (m + n) step
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat.0.Nat.mkBEqNat : Lean.Expr → Lean.Expr → Lean.Expr
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Submodule
instAddSubmonoidClassHomogeneousSubmodule : ∀ {ιA : Type u_1} {ιM : Type u_2} {σA : Type u_3} {σM : Type u_4} {A : Type u_5} {M : Type u_6} [inst : Semiring A]
  [inst_1 : AddCommMonoid M] [inst_2 : Module A M] (𝒜 : ιA → σA) (ℳ : ιM → σM) [inst_3 : DecidableEq ιA]
  [inst_4 : AddMonoid ιA] [inst_5 : SetLike σA A] [inst_6 : AddSubmonoidClass σA A] [inst_7 : GradedRing 𝒜]
  [inst_8 : DecidableEq ιM] [inst_9 : SetLike σM M] [inst_10 : AddSubmonoidClass σM M]
  [inst_11 : DirectSum.Decomposition ℳ] [inst_12 : VAdd ιA ιM] [inst_13 : SetLike.GradedSMul 𝒜 ℳ],
  AddSubmonoidClass (HomogeneousSubmodule 𝒜 ℳ) M
-- Mathlib.RingTheory.MvPolynomial.Ideal
/-- The `n`th power of `idealOfVars` is spanned by all monic monomials of total degree `n`.  -/
MvPolynomial.pow_idealOfVars_eq_span : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] (n : ℕ),
  MvPolynomial.idealOfVars σ R ^ n = Ideal.span ((fun x => (MvPolynomial.monomial x) 1) '' ⇑Finsupp.degree ⁻¹' {n})
-- Mathlib.Analysis.Fourier.FourierTransform
VectorFourier.fourierIntegral_continuousMultilinearMap_apply : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : Type u_3} {V : Type u_5} {W : Type u_6} [inst : Fintype ι]
  [inst_1 : NontriviallyNormedField 𝕜] [inst_2 : NormedAddCommGroup V] [inst_3 : NormedSpace 𝕜 V]
  [inst_4 : MeasurableSpace V] [BorelSpace V] [inst_6 : NormedAddCommGroup W] [inst_7 : NormedSpace 𝕜 W]
  {e : AddChar 𝕜 Circle} {μ : MeasureTheory.Measure V} {L : V →L[𝕜] W →L[𝕜] 𝕜} [inst_8 : NormedAddCommGroup E]
  [inst_9 : NormedSpace ℂ E] {M : ι → Type u_7} [inst_10 : (i : ι) → NormedAddCommGroup (M i)]
  [inst_11 : (i : ι) → NormedSpace ℝ (M i)] {f : V → ContinuousMultilinearMap ℝ M E} {m : (i : ι) → M i} {w : W},
  Continuous ⇑e →
    MeasureTheory.Integrable f μ →
      (VectorFourier.fourierIntegral e μ (ContinuousLinearMap.toLinearMap₁₂ L) f w) m =
        VectorFourier.fourierIntegral e μ (ContinuousLinearMap.toLinearMap₁₂ L) (fun x => (f x) m) w
-- Mathlib.Analysis.Distribution.TemperateGrowth
MeasureTheory.Measure.HasTemperateGrowth.mk : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : MeasurableSpace E] {μ : MeasureTheory.Measure E},
  (∃ n, MeasureTheory.Integrable (fun x => (1 + ‖x‖) ^ (-↑n)) μ) → μ.HasTemperateGrowth
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenSubgroup.coe_toOpens : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] {U : OpenSubgroup G}, ↑↑U = ↑U
-- Batteries.Recycling.RBTree.WF
RBTree.RBNode.cmpLT.flip : ∀ {α : Type u_1} {cmp : α → α → Ordering} {x y : α}, RBTree.RBNode.cmpLT cmp x y → RBTree.RBNode.cmpLT (flip cmp) y x
-- Init.Data.Nat.Lemmas
Nat.le_add_one_iff : ∀ {m n : ℕ}, m ≤ n + 1 ↔ m ≤ n ∨ m = n + 1
-- Lean.Meta.Tactic.Simp.Types
/-- Number of times each congr theorem has been tried.  -/
Lean.Meta.Simp.Diagnostics.congrThmCounter : Lean.Meta.Simp.Diagnostics → Lean.PHashMap Lean.Name ℕ
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.DocumentSymbol.brecOn.eq : ∀ {motive_1 : Lean.Lsp.DocumentSymbol → Sort u} {motive_2 : Lean.Lsp.DocumentSymbolAux Lean.Lsp.DocumentSymbol → Sort u}
  {motive_3 : Option (Array Lean.Lsp.DocumentSymbol) → Sort u} {motive_4 : Array Lean.Lsp.DocumentSymbol → Sort u}
  {motive_5 : List Lean.Lsp.DocumentSymbol → Sort u} (t : Lean.Lsp.DocumentSymbol)
  (F_1 : (t : Lean.Lsp.DocumentSymbol) → t.below → motive_1 t)
  (F_2 : (t : Lean.Lsp.DocumentSymbolAux Lean.Lsp.DocumentSymbol) → Lean.Lsp.DocumentSymbol.below_1 t → motive_2 t)
  (F_3 : (t : Option (Array Lean.Lsp.DocumentSymbol)) → Lean.Lsp.DocumentSymbol.below_2 t → motive_3 t)
  (F_4 : (t : Array Lean.Lsp.DocumentSymbol) → Lean.Lsp.DocumentSymbol.below_3 t → motive_4 t)
  (F_5 : (t : List Lean.Lsp.DocumentSymbol) → Lean.Lsp.DocumentSymbol.below_4 t → motive_5 t),
  t.brecOn F_1 F_2 F_3 F_4 F_5 = F_1 t (Lean.Lsp.DocumentSymbol.brecOn.go t F_1 F_2 F_3 F_4 F_5).2
-- Mathlib.Analysis.InnerProductSpace.WeakOperatorTopology
ContinuousLinearMapWOT.le_nhds_iff_forall_inner_apply_le_nhds : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E]
  [inst_3 : Module 𝕜 E] [inst_4 : NormedAddCommGroup F] [inst_5 : InnerProductSpace 𝕜 F] [CompleteSpace F]
  {l : Filter (E →WOT[𝕜] F)} {A : E →WOT[𝕜] F},
  l ≤ nhds A ↔ ∀ (x : E) (y : F), Filter.map (fun T => inner 𝕜 y (T x)) l ≤ nhds (inner 𝕜 y (A x))
-- Mathlib.Algebra.Group.Subgroup.Lattice
AddSubgroup.disjoint_def' : ∀ {G : Type u_1} [inst : AddGroup G] {H₁ H₂ : AddSubgroup G},
  Disjoint H₁ H₂ ↔ ∀ {x y : G}, x ∈ H₁ → y ∈ H₂ → x = y → x = 0
-- Mathlib.Algebra.Star.Basic
/-- A \*-ring `R` is a non-unital, non-associative (semi)ring with an involutive `star` operation
which is additive which makes `R` with its multiplicative structure into a \*-multiplication
(i.e. `star (r * s) = star s * star r`).  -/
StarRing : (R : Type u) → [NonUnitalNonAssocSemiring R] → Type u
-- Mathlib.Order.Filter.Map
Filter.mem_map : ∀ {α : Type u_1} {β : Type u_2} {f : Filter α} {m : α → β} {t : Set β}, t ∈ Filter.map m f ↔ m ⁻¹' t ∈ f
-- Mathlib.GroupTheory.Index
MulAction.index_stabilizer : ∀ (G : Type u_1) {X : Type u_2} [inst : Group G] [inst_1 : MulAction G X] (x : X),
  (MulAction.stabilizer G x).index = (MulAction.orbit G x).ncard
-- Init.Data.Iterators.Consumers.Loop
/-- Folds a function over an iterator from the left, accumulating a value starting with `init`.
The accumulated value is combined with the each element of the list in order, using `f`.

It is equivalent to `it.toList.foldl`.

This function is deprecated. Instead of `it.allowNontermination.fold`, use `it.fold`.
 -/
Std.Iter.Partial.fold : {α β : Type w} →
  {γ : Type x} → [inst : Std.Iterator α Id β] → [Std.IteratorLoop α Id Id] → (γ → β → γ) → γ → Std.Iter.Partial β → γ
-- Mathlib.Computability.NFA
NFA.mem_stepSet : ∀ {α : Type u} {σ : Type v} {M : NFA α σ} {s : σ} {S : Set σ} {a : α}, s ∈ M.stepSet S a ↔ ∃ t ∈ S, s ∈ M.step t a
-- Mathlib.Algebra.Group.Subgroup.Lattice
AddSubgroup.instUniqueOfSubsingleton : {G : Type u_1} → [inst : AddGroup G] → [Subsingleton G] → Unique (AddSubgroup G)
-- Init.Data.Option.Lemmas
Option.pelim_some' : ∀ {α : Type u_1} {x : Option α} {a : α} {α_1 : Sort u_2} {b : α_1} {f : (a : α) → x = some a → α_1} (h : x = some a),
  x.pelim b f = f a h
-- Mathlib.Data.Finsupp.Option
Finsupp.sum_option_index : ∀ {α : Type u_1} {M : Type u_2} {N : Type u_3} [inst : AddZeroClass M] [inst_1 : AddCommMonoid N] (f : Option α →₀ M)
  (b : Option α → M → N),
  (∀ (o : Option α), b o 0 = 0) →
    (∀ (o : Option α) (m₁ m₂ : M), b o (m₁ + m₂) = b o m₁ + b o m₂) →
      f.sum b = b none (f none) + f.some.sum fun a => b (some a)
-- Mathlib.MeasureTheory.Integral.Pi
/-- A version of **Fubini's theorem** with the variables indexed by a general finite type.  -/
MeasureTheory.integral_fintype_prod_eq_prod : ∀ {𝕜 : Type u_1} {ι : Type u_2} [inst : Fintype ι] [inst_1 : RCLike 𝕜] {E : ι → Type u_3} (f : (i : ι) → E i → 𝕜)
  {mE : (i : ι) → MeasurableSpace (E i)} {μ : (i : ι) → MeasureTheory.Measure (E i)}
  [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)],
  ∫ (x : (i : ι) → E i), ∏ i, f i (x i) ∂MeasureTheory.Measure.pi μ = ∏ i, ∫ (x : E i), f i x ∂μ i
-- Mathlib.Algebra.DirectSum.Decomposition
DirectSum.decompose_sub : ∀ {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [inst : DecidableEq ι] [inst_1 : AddCommGroup M] [inst_2 : SetLike σ M]
  [inst_3 : AddSubgroupClass σ M] (ℳ : ι → σ) [inst_4 : DirectSum.Decomposition ℳ] (x y : M),
  (DirectSum.decompose ℳ) (x - y) = (DirectSum.decompose ℳ) x - (DirectSum.decompose ℳ) y
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Real.logb_nonpos : ∀ {b x : ℝ}, 1 < b → 0 ≤ x → x ≤ 1 → Real.logb b x ≤ 0
-- Mathlib.Algebra.Group.Subsemigroup.Operations
Subsemigroup.top_prod : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] (s : Subsemigroup N),
  ⊤.prod s = Subsemigroup.comap (MulHom.snd M N) s
-- Mathlib.CategoryTheory.PathCategory.Basic
_private.Mathlib.CategoryTheory.PathCategory.Basic.0.CategoryTheory.composePath.match_1.splitter : {C : Type u_2} →
  [inst : CategoryTheory.Category.{u_1, u_2} C] →
    {X : C} →
      (motive : (x : C) → Quiver.Path X x → Sort u_3) →
        (x : C) →
          (x_1 : Quiver.Path X x) →
            (Unit → motive X Quiver.Path.nil) →
              ((x b : C) → (p : Quiver.Path X b) → (e : b ⟶ x) → motive x (p.cons e)) → motive x x_1
-- Init.Data.UInt.Bitwise
UInt8.not_zero : ~~~0 = -1
-- Mathlib.Data.Complex.Basic
Complex.equivRealProd_apply : ∀ (z : ℂ), Complex.equivRealProd z = (z.re, z.im)
-- Mathlib.Order.Interval.Multiset
Multiset.nodup_Ioc : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] {a b : α}, (Multiset.Ioc a b).Nodup
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
CategoryTheory.Limits.PreservesColimit.preserves : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} D}
  {J : Type w} {inst_2 : CategoryTheory.Category.{w', w} J} {K : CategoryTheory.Functor J C}
  {F : CategoryTheory.Functor C D} [self : CategoryTheory.Limits.PreservesColimit K F]
  {c : CategoryTheory.Limits.Cocone K} (hc : CategoryTheory.Limits.IsColimit c),
  Nonempty (CategoryTheory.Limits.IsColimit (F.mapCocone c))
-- Mathlib.AlgebraicGeometry.StructureSheaf
AlgebraicGeometry.StructureSheaf.smul_const : ∀ {R M : Type u} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (f : M) (r g : R)
  (U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)) (hu : U ≤ PrimeSpectrum.basicOpen g),
  r • AlgebraicGeometry.StructureSheaf.const f g U hu = AlgebraicGeometry.StructureSheaf.const (r • f) g U hu
-- Mathlib.Order.Compare
Ordering.Compares.ne_lt : ∀ {α : Type u_1} [inst : Preorder α] {o : Ordering} {a b : α}, o.Compares a b → (o ≠ Ordering.lt ↔ b ≤ a)
-- Mathlib.GroupTheory.QuotientGroup.Basic
/-- The isomorphism between the quotient of a product by the image of the `n`th power map
and the product of the quotients by the images of the `n`th power maps on the factors.  -/
QuotientGroup.mulEquivPiModRangePowMonoidHom : {ι : Type u_1} →
  (A : ι → Type u_2) →
    [inst : (i : ι) → CommGroup (A i)] →
      (n : ℕ) → ((i : ι) → A i) ⧸ (powMonoidHom n).range ≃* ((i : ι) → A i ⧸ (powMonoidHom n).range)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getD_of_isEmpty : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t.WF → ∀ {a : α} {fallback : β}, t.isEmpty = true → Std.DTreeMap.Internal.Impl.Const.getD t a fallback = fallback
-- Batteries.Data.Fin.Coding
_private.Batteries.Data.Fin.Coding.0.Fin.encodePi.match_3.eq_1 : ∀ (n : ℕ) (f : Fin (n + 1) → ℕ) (motive : Fin (Fin.prod fun x => f x.succ) → Sort u_1) (k : ℕ)
  (hk : k < Fin.prod fun x => f x.succ) (h_1 : (k : ℕ) → (hk : k < Fin.prod fun x => f x.succ) → motive ⟨k, hk⟩),
  (match ⟨k, hk⟩ with
    | ⟨k, hk⟩ => h_1 k hk) =
    h_1 k hk