mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.Presieve.exists_eq_preZeroHypercover : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (R : CategoryTheory.Presieve S), ∃ E, R = E.presieve₀
-- Mathlib.CategoryTheory.WithTerminal.Basic
_private.Mathlib.CategoryTheory.WithTerminal.Basic.0.CategoryTheory.WithInitial.map.match_1.eq_2 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C]
  (motive : (X Y : CategoryTheory.WithInitial C) → (X ⟶ Y) → Sort u_3) (a : C)
  (x : CategoryTheory.WithInitial.star ⟶ CategoryTheory.WithInitial.of a)
  (h_1 :
    (a a_1 : C) →
      (f : CategoryTheory.WithInitial.of a ⟶ CategoryTheory.WithInitial.of a_1) →
        motive (CategoryTheory.WithInitial.of a) (CategoryTheory.WithInitial.of a_1) f)
  (h_2 :
    (a : C) →
      (x : CategoryTheory.WithInitial.star ⟶ CategoryTheory.WithInitial.of a) →
        motive CategoryTheory.WithInitial.star (CategoryTheory.WithInitial.of a) x)
  (h_3 :
    (x : CategoryTheory.WithInitial.star ⟶ CategoryTheory.WithInitial.star) →
      motive CategoryTheory.WithInitial.star CategoryTheory.WithInitial.star x),
  (match CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.of a, x with
    | CategoryTheory.WithInitial.of a, CategoryTheory.WithInitial.of a_1, f => h_1 a a_1 f
    | CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.of a, x => h_2 a x
    | CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.star, x => h_3 x) =
    h_2 a x
-- Mathlib.Algebra.Algebra.Operations
Submodule.pow_one : ∀ {R : Type u} [inst : Semiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] (M : Submodule R A), M ^ 1 = M
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.DefinitionParams.mk.sizeOf_spec : ∀ (toTextDocumentPositionParams : Lean.Lsp.TextDocumentPositionParams),
  sizeOf { toTextDocumentPositionParams := toTextDocumentPositionParams } = 1 + sizeOf toTextDocumentPositionParams
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.parseEraLong : Std.Time.DateFormatSymbols → Std.Internal.Parsec.String.Parser Std.Time.Year.Era
-- Mathlib.Analysis.Normed.Group.Basic
nndist_zero_left : ∀ {E : Type u_5} [inst : SeminormedAddGroup E] (a : E), nndist 0 a = ‖a‖₊
-- Mathlib.Computability.DFA
DFA.pumping_lemma : ∀ {α : Type u} {σ : Type v} (M : DFA α σ) [inst : Fintype σ] {x : List α},
  x ∈ M.accepts →
    Fintype.card σ ≤ x.length →
      ∃ a b c, x = a ++ b ++ c ∧ a.length + b.length ≤ Fintype.card σ ∧ b ≠ [] ∧ {a} * KStar.kstar {b} * {c} ≤ M.accepts
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.Hom.ext_iff : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} {inst : CategoryTheory.Category.{v₁, u₁} A}
  {inst_1 : CategoryTheory.Category.{v₂, u₂} B} {inst_2 : CategoryTheory.Category.{v₃, u₃} C}
  {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {X : Type u₄}
  {inst_3 : CategoryTheory.Category.{v₄, u₄} X} {x y : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X}
  {x_1 y_1 : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.Hom X x y},
  x_1 = y_1 ↔ x_1.fst = y_1.fst ∧ x_1.snd = y_1.snd
-- Std.Http.Data.Response
Std.Http.Response.instReprHead : Repr Std.Http.Response.Head
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
/-- Inverse of a transvection: `transvection i j hij b * transvection i j hij (-b) = 1`.  -/
Matrix.SpecialLinearGroup.transvection_mul_neg : ∀ {ι : Type u_1} {F : Type u_2} [inst : DecidableEq ι] [inst_1 : Fintype ι] [inst_2 : CommRing F] {i j : ι}
  (hij : i ≠ j) (b : F),
  Matrix.SpecialLinearGroup.transvection hij b * Matrix.SpecialLinearGroup.transvection hij (-b) = 1
-- Mathlib.RepresentationTheory.Intertwining
/-- The projection of a product representation onto its second component is an intertwining map.  -/
Representation.IntertwiningMap.snd : (A : Type u_1) →
  {G : Type u_2} →
    {V : Type u_3} →
      {W : Type u_4} →
        [inst : Semiring A] →
          [inst_1 : Monoid G] →
            [inst_2 : AddCommMonoid V] →
              [inst_3 : AddCommMonoid W] →
                [inst_4 : Module A V] →
                  [inst_5 : Module A W] →
                    (ρ : Representation A G V) → (σ : Representation A G W) → (ρ.prod σ).IntertwiningMap σ
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.smul_set_iInter₂_subset : ∀ {α : Type u_2} {β : Type u_3} {ι : Sort u_5} {κ : ι → Sort u_6} [inst : SMul α β] (a : α) (t : (i : ι) → κ i → Set β),
  a • ⋂ i, ⋂ j, t i j ⊆ ⋂ i, ⋂ j, a • t i j
-- Mathlib.Order.Filter.IsBounded
Antitone.isBoundedUnder_le_comp_iff : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Nonempty β] [inst : LinearOrder β] [inst_1 : Preorder γ] [NoMaxOrder γ]
  {g : β → γ} {f : α → β} {l : Filter α},
  Antitone g →
    Filter.Tendsto g Filter.atBot Filter.atTop →
      (Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l (g ∘ f) ↔ Filter.IsBoundedUnder (fun x1 x2 => x2 ≤ x1) l f)
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.smul_set_inter_subset : ∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β] {t₁ t₂ : Set β} {a : α}, a • (t₁ ∩ t₂) ⊆ a • t₁ ∩ a • t₂
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey?_maxKey! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Inhabited α], t.WF → t.isEmpty = false → t.getKey? t.maxKey! = some t.maxKey!
-- Mathlib.Tactic.TFAE
/-- Prove an implication via depth-first traversal.  -/
Mathlib.Tactic.TFAE.proveImpl : Array (ℕ × ℕ × Lean.Expr) → Array Q(Prop) → ℕ → ℕ → (P P' : Q(Prop)) → Lean.MetaM Q(«$P» → «$P'»)
-- Init.Data.List.Basic
List.sum_cons : ∀ {α : Type u} [inst : Add α] [inst_1 : Zero α] {a : α} {l : List α}, (a :: l).sum = a + l.sum
-- Mathlib.Algebra.DualNumber
DualNumber.eps_mul_eps : ∀ {R : Type u_1} [inst : Semiring R], DualNumber.eps * DualNumber.eps = 0
-- Mathlib.Tactic.TermCongr
/-- Generate congruence for applications `lhs` and `rhs`.
Key detail: functions might be *overapplied* due to the values of their arguments.
For example, `id id 2` is overapplied.
To handle these, we need to segment the applications into their natural arities,
since `mkHCongrWithArity'` does not know how to generate congruence lemmas for the overapplied case.
 -/
Mathlib.Tactic.TermCongr.mkCongrOfApp : ℕ → ℕ → Lean.Expr → Lean.Expr → Mathlib.Tactic.TermCongr.M Mathlib.Tactic.TermCongr.CongrResult
-- Mathlib.Topology.ContinuousOn
/-- **Alias** of `continuousOn_union_iff_of_isOpen`.

---

A function is continuous on two open sets iff it is also continuous on their union.  -/
continouousOn_union_iff_of_isOpen : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {s t : Set α} {f : α → β},
  IsOpen s → IsOpen t → (ContinuousOn f (s ∪ t) ↔ ContinuousOn f s ∧ ContinuousOn f t)
-- Mathlib.Data.Option.Basic
Option.map_comm : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {f₁ : α → β} {f₂ : α → γ} {g₁ : β → δ} {g₂ : γ → δ},
  g₁ ∘ f₁ = g₂ ∘ f₂ → ∀ (a : α), Option.map g₁ (Option.map f₁ (some a)) = Option.map g₂ (Option.map f₂ (some a))
-- Mathlib.Algebra.GroupWithZero.InjSurj
/-- Push forward a `MonoidWithZero` along a surjective function.
See note [reducible non-instances].  -/
Function.Surjective.monoidWithZero : {M₀ : Type u_1} →
  {M₀' : Type u_3} →
    [inst : Zero M₀'] →
      [inst_1 : Mul M₀'] →
        [inst_2 : One M₀'] →
          [inst_3 : Pow M₀' ℕ] →
            [inst_4 : MonoidWithZero M₀] →
              (f : M₀ → M₀') →
                Function.Surjective f →
                  f 0 = 0 →
                    f 1 = 1 →
                      (∀ (x y : M₀), f (x * y) = f x * f y) →
                        (∀ (x : M₀) (n : ℕ), f (x ^ n) = f x ^ n) → MonoidWithZero M₀'
-- Mathlib.RingTheory.FinitePresentation
/-- A finitely presented algebra is of finite type.  -/
Algebra.FiniteType.of_finitePresentation : ∀ {R : Type w₁} {A : Type w₂} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [Algebra.FinitePresentation R A], Algebra.FiniteType R A
-- Mathlib.RingTheory.Ideal.Defs
Ideal.sub_mem : ∀ {α : Type u} [inst : Ring α] (I : Ideal α) {a b : α}, a ∈ I → b ∈ I → a - b ∈ I
-- Mathlib.Order.BooleanAlgebra.Set
Set.compl_subset_iff_union : ∀ {α : Type u_1} {s t : Set α}, sᶜ ⊆ t ↔ s ∪ t = Set.univ
-- Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic
/-- The value of the quadratic character at `-1`  -/
quadraticChar_neg_one : ∀ {F : Type u_1} [inst : Field F] [inst_1 : Fintype F] [inst_2 : DecidableEq F],
  ringChar F ≠ 2 → (quadraticChar F) (-1) = ZMod.χ₄ ↑(Fintype.card F)
-- Mathlib.Analysis.Normed.Unbundled.AlgebraNorm
/-- The seminorm of a scalar multiplication is the product of the absolute value of the scalar
and the original seminorm.  -/
AlgebraNorm.smul' : ∀ {R : Type u_1} [inst : SeminormedCommRing R] {S : Type u_2} [inst_1 : Ring S] [inst_2 : Algebra R S]
  (self : AlgebraNorm R S) (a : R) (x : S), self.toFun (a • x) = ‖a‖ * self.toFun x
-- Mathlib.Order.Category.PartOrd
PartOrd.hasForgetToPreord : CategoryTheory.HasForget₂ PartOrd Preord
-- Lean.Meta.Tactic.Grind.Arith.FieldNormNum
_private.Lean.Meta.Tactic.Grind.Arith.FieldNormNum.0.Lean.Meta.Grind.Arith.FieldNormNum.isNegInst : Lean.Expr → Lean.Meta.Grind.Arith.FieldNormNum.M✝ Bool
-- Mathlib.Condensed.Light.Sequence
_private.Mathlib.Condensed.Light.Sequence.0.InternalProjectivityProof.coverToFun_surjective : ∀ {S : Type u_1} {T : Type u_2} {X : Type u_3} (π : T → S × Option X) (σ : Option X → S → T),
  (∀ (x : Option X) (s : S), (π (σ x s)).1 = s) →
    (∀ (x : Option X) (s : S), (π (σ x s)).2 = x) →
      Function.Surjective
        (InternalProjectivityProof.coverToFun✝ (InternalProjectivityProof.fibreIncl✝ π σ)
          (InternalProjectivityProof.π_r✝ π σ))
-- Mathlib.CategoryTheory.Action.Monoidal
/-- If `V` is rigid, so is `Action V G`.  -/
Action.instRigidCategory : (V : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    [inst_1 : CategoryTheory.MonoidalCategory V] →
      (H : Type u_3) → [inst_2 : Group H] → [CategoryTheory.RigidCategory V] → CategoryTheory.RigidCategory (Action V H)
-- Mathlib.Algebra.Category.Grp.Limits
AddCommGrpCat.limitAddCommGroup : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    (F : CategoryTheory.Functor J AddCommGrpCat) →
      [inst_1 : Small.{u, max u v} ↑(F.comp (CategoryTheory.forget AddCommGrpCat)).sections] →
        AddCommGroup (CategoryTheory.Limits.Types.Small.limitCone (F.comp (CategoryTheory.forget AddCommGrpCat))).pt
-- Mathlib.CategoryTheory.Abelian.Basic
/-- Every `NonPreadditiveAbelian` category can be promoted to an abelian category.  -/
CategoryTheory.NonPreadditiveAbelian.abelian : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] → [CategoryTheory.NonPreadditiveAbelian C] → CategoryTheory.Abelian C
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.mem_union_of_left : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k : α}, k ∈ m₁ → k ∈ m₁ ∪ m₂
-- Mathlib.Topology.Gluing
TopCat.GlueData.mk.injEq : ∀ (toGlueData : CategoryTheory.GlueData TopCat)
  (f_open : ∀ (i j : toGlueData.J), Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom (toGlueData.f i j)))
  (toGlueData_1 : CategoryTheory.GlueData TopCat)
  (f_open_1 :
    ∀ (i j : toGlueData_1.J), Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom (toGlueData_1.f i j))),
  ({ toGlueData := toGlueData, f_open := f_open } = { toGlueData := toGlueData_1, f_open := f_open_1 }) =
    (toGlueData = toGlueData_1)
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Limits.Sigma.π.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {β : Type w} [inst_2 : DecidableEq β] (f : β → C) [inst_3 : CategoryTheory.Limits.HasCoproduct f] (b : β),
  CategoryTheory.Limits.Sigma.π f b =
    CategoryTheory.Limits.Sigma.desc (Function.update (fun x => 0) b (CategoryTheory.CategoryStruct.id (f b)))
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.of_toArray_perm : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp},
  t₁.toArray.Perm t₂.toArray → t₁.Equiv t₂
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.size_insertManyIfNewUnit_list : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α fun x => Unit} [EquivBEq α]
  [LawfulHashable α],
  m.WF →
    ∀ {l : List α},
      List.Pairwise (fun a b => (a == b) = false) l →
        (∀ a ∈ m, l.contains a = false) → (Std.DHashMap.Raw.Const.insertManyIfNewUnit m l).size = m.size + l.length
-- Mathlib.CategoryTheory.Limits.Shapes.End
CategoryTheory.Limits.Wedge.condition : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {C : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} C]
  {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} (c : CategoryTheory.Limits.Wedge F) {i j : J}
  (f : i ⟶ j),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multifork.ι c i) ((F.obj (Opposite.op i)).map f) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multifork.ι c j) ((F.map f.op).app j)
-- Lean.Elab.Binders
Lean.Elab.Term.elabLetIDecl : Lean.Elab.Term.TermElab
-- Init.Data.List.Find
List.findIdx_eq_getD_findIdx? : ∀ {α : Type u_1} {xs : List α} {p : α → Bool}, List.findIdx p xs = (List.findIdx? p xs).getD xs.length
-- Mathlib.Analysis.Normed.Module.Connected
/-- In a real vector space of dimension `> 1`, any sphere of nonnegative radius is connected.  -/
isConnected_sphere : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E],
  1 < Module.rank ℝ E → ∀ (x : E) {r : ℝ}, 0 ≤ r → IsConnected (Metric.sphere x r)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.isEmpty_union : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → (m₁ ∪ m₂).isEmpty = (m₁.isEmpty && m₂.isEmpty)
-- Mathlib.Topology.Closure
/-- **Alias** of `closure_sdiff_frontier`. -/
closure_diff_frontier : ∀ {X : Type u} [inst : TopologicalSpace X] (s : Set X), closure s \ frontier s = interior s
-- Mathlib.Order.Hom.BoundedLattice
/-- `Subtype.val` as an `InfTopHom`.  -/
InfTopHom.subtypeVal : {β : Type u_3} →
  [inst : SemilatticeInf β] →
    [inst_1 : OrderTop β] →
      {P : β → Prop} → (Ptop : P ⊤) → (Pinf : ∀ ⦃x y : β⦄, P x → P y → P (x ⊓ y)) → InfTopHom { x // P x } β
-- Mathlib.FieldTheory.Minpoly.Field
/-- The minimal polynomial of a nonzero element has nonzero constant coefficient.  -/
minpoly.coeff_zero_ne_zero : ∀ {A : Type u_1} {B : Type u_2} [inst : Field A] [inst_1 : Ring B] [IsDomain B] [inst_3 : Algebra A B] {x : B},
  IsIntegral A x → x ≠ 0 → (minpoly A x).coeff 0 ≠ 0
-- Mathlib.Topology.Path
Path.range_reparam : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X} (γ : Path x y) {f : ↑unitInterval → ↑unitInterval}
  (hfcont : Continuous f) (hf₀ : f 0 = 0) (hf₁ : f 1 = 1), Set.range ⇑(γ.reparam f hfcont hf₀ hf₁) = Set.range ⇑γ
-- Mathlib.Algebra.Group.Action.Defs
smul_mul' : ∀ {M : Type u_1} {N : Type u_2} [inst : Monoid M] [inst_1 : Monoid N] [inst_2 : MulDistribMulAction M N] (a : M)
  (b₁ b₂ : N), a • (b₁ * b₂) = a • b₁ * a • b₂
-- Mathlib.Algebra.RingQuot
RingQuot.mul_quot : ∀ {R : Type uR} [inst : Semiring R] (r : R → R → Prop) {a b : R},
  { toQuot := Quot.mk (RingQuot.Rel r) a } * { toQuot := Quot.mk (RingQuot.Rel r) b } =
    { toQuot := Quot.mk (RingQuot.Rel r) (a * b) }
-- Init.Data.Iterators.Basic
/-- This typeclass characterizes iterators that have deterministic return values. This typeclass does
*not* guarantee that there are no monadic side effects such as exceptions.

General monadic iterators can be nondeterministic, so that `it.IsPlausibleStep step` will be true
for no or more than one choice of `step`. This typeclass ensures that there is exactly one such
choice.

This is an experimental instance and it should not be explicitly used downstream of the standard
library.
 -/
Std.LawfulDeterministicIterator : {β : Type w} → (α : Type w) → (m : Type w → Type w') → [Std.Iterator α m β] → Prop
-- Lean.Server.FileWorker.InlayHints
Lean.Server.FileWorker.handleInlayHints : Lean.Lsp.InlayHintParams →
  Lean.Server.FileWorker.InlayHintState →
    Lean.Server.RequestM (Lean.Server.LspResponse (Array Lean.Lsp.InlayHint) × Lean.Server.FileWorker.InlayHintState)
-- Mathlib.Data.Set.Image
Set.image_subset_preimage_of_inverse : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {g : β → α}, Function.LeftInverse g f → ∀ (s : Set α), f '' s ⊆ g ⁻¹' s
-- Mathlib.Algebra.Order.Module.Defs
PosSMulReflectLE.toPosSMulReflectLT : ∀ {α : Type u_1} {β : Type u_2} [inst : Zero α] [inst_1 : Zero β] [inst_2 : SMulWithZero α β] [inst_3 : PartialOrder α]
  [inst_4 : PartialOrder β] [PosSMulReflectLE α β], PosSMulReflectLT α β
-- Mathlib.CategoryTheory.Linear.Basic
/-- Composition as a bilinear map.  -/
CategoryTheory.Linear.comp : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {S : Type w} →
        [inst_2 : CommSemiring S] →
          [inst_3 : CategoryTheory.Linear S C] → (X Y Z : C) → (X ⟶ Y) →ₗ[S] (Y ⟶ Z) →ₗ[S] X ⟶ Z
-- Mathlib.Data.Sym.Sym2
/-- Dependent recursion principle for `Sym2`. See `Quot.recOn`.  -/
Sym2.recOn : {α : Type u_1} →
  {motive : Sym2 α → Sort u_4} →
    (z : Sym2 α) →
      (f : (a b : α) → motive s(a, b)) → (∀ (a b c d : α) (h : Sym2.Rel α (a, b) (c, d)), ⋯ ▸ f a b = f c d) → motive z
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Algebra.iInf_toSubmodule : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] {ι : Sort u_1}
  (S : ι → Subalgebra R A), Subalgebra.toSubmodule (⨅ i, S i) = ⨅ i, Subalgebra.toSubmodule (S i)
-- Mathlib.Topology.Algebra.Module.Alternating.Topology
/-- The application of a multilinear map as a `ContinuousLinearMap`.  -/
ContinuousAlternatingMap.apply : (𝕜 : Type u_1) →
  (E : Type u_2) →
    (F : Type u_3) →
      {ι : Type u_4} →
        [inst : NormedField 𝕜] →
          [inst_1 : AddCommGroup E] →
            [inst_2 : Module 𝕜 E] →
              [inst_3 : TopologicalSpace E] →
                [inst_4 : AddCommGroup F] →
                  [inst_5 : Module 𝕜 F] →
                    [inst_6 : TopologicalSpace F] →
                      [inst_7 : IsTopologicalAddGroup F] →
                        [inst_8 : ContinuousConstSMul 𝕜 F] → [ContinuousSMul 𝕜 E] → (ι → E) → E [⋀^ι]→L[𝕜] F →L[𝕜] F
-- Mathlib.Data.Finset.Insert
Finset.cons_subset_cons : ∀ {α : Type u_1} {s t : Finset α} {a : α} {hs : a ∉ s} {ht : a ∉ t}, Finset.cons a s hs ⊆ Finset.cons a t ht ↔ s ⊆ t
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
IsPrimitiveRoot.integralPowerBasis_gen : ∀ {n : ℕ} {K : Type u} [inst : Field K] {ζ : K} [inst_1 : NeZero n] [inst_2 : CharZero K]
  [hcycl : IsCyclotomicExtension {n} ℚ K] (hζ : IsPrimitiveRoot ζ n), hζ.integralPowerBasis.gen = hζ.toInteger
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
_private.Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality.0.InnerProductGeometry.ortho.eq_1 : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] (x y : V),
  InnerProductGeometry.ortho✝ x y = y - (ℝ ∙ x).starProjection y
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
NumberField.mixedEmbedding.fundamentalCone.expMap_target : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  NumberField.mixedEmbedding.fundamentalCone.expMap.target = Set.univ.pi fun x => Set.Ioi 0
-- Std.Time.Notation.Spec
_private.Std.Time.Notation.Spec.0.Std.Time.convertOffsetX : Std.Time.OffsetX → Lean.MacroM (Lean.TSyntax `term)
-- Mathlib.Algebra.Regular.ULift
ULift.isAddLeftRegular_down : ∀ {R : Type v} [inst : Add R] {a : ULift.{u, v} R}, IsAddLeftRegular a.down ↔ IsAddLeftRegular a
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Ioi_union_Iic : ∀ {α : Type u_1} [inst : LinearOrder α] {a : α}, Set.Ioi a ∪ Set.Iic a = Set.univ
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.mem_iSup_of_directed : ∀ {R : Type u} [inst : NonAssocSemiring R] {ι : Sort u_1} [hι : Nonempty ι] {S : ι → Subsemiring R},
  Directed (fun x1 x2 => x1 ≤ x2) S → ∀ {x : R}, x ∈ ⨆ i, S i ↔ ∃ i, x ∈ S i
-- Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
Subgroup.unop_eq_top : ∀ {G : Type u_2} [inst : Group G] {S : Subgroup Gᵐᵒᵖ}, S.unop = ⊤ ↔ S = ⊤
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.map_monomial : ∀ {σ : Type u_1} {R : Type u_2} {S : Type u_3} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+* S) (n : σ →₀ ℕ)
  (a : R), (MvPowerSeries.map f) ((MvPowerSeries.monomial n) a) = (MvPowerSeries.monomial n) (f a)
-- Mathlib.Data.Part
Part.right_dom_of_inter_dom : ∀ {α : Type u_1} [inst : Inter α] {a b : Part α}, (a ∩ b).Dom → b.Dom
-- Init.Data.String.FindPos
/-- Obtains the smallest valid position that is strictly greater than the given byte position.
 -/
String.Slice.posGT : (s : String.Slice) → (offset : String.Pos.Raw) → offset < s.rawEndPos → s.Pos
-- Mathlib.CategoryTheory.Category.Bipointed
/-- The subtype of functions corresponding to the morphisms in `Bipointed`.  -/
Bipointed.HomSubtype : Bipointed → Bipointed → Type (max 0 u_1 u_2)
-- Mathlib.MeasureTheory.Function.Jacobian
/-- Assume that a function `f` has a derivative at every point of a set `s`. Then one may cover `s`
with countably many closed sets `t n` on which `f` is well approximated by linear maps `A n`.  -/
exists_closed_cover_approximatesLinearOn_of_hasFDerivWithinAt : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E]
  [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] [SecondCountableTopology F] (f : E → F) (s : Set E)
  (f' : E → E →L[ℝ] F),
  (∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) →
    ∀ (r : (E →L[ℝ] F) → NNReal),
      (∀ (A : E →L[ℝ] F), r A ≠ 0) →
        ∃ t A,
          (∀ (n : ℕ), IsClosed (t n)) ∧
            s ⊆ ⋃ n, t n ∧
              (∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) (r (A n))) ∧
                (s.Nonempty → ∀ (n : ℕ), ∃ y ∈ s, A n = f' y)
-- Mathlib.LinearAlgebra.ExteriorPower.Basic
exteriorPower.presentation.relations_relation : ∀ (R : Type u) [inst : CommRing R] (ι : Type u_4) [inst_1 : DecidableEq ι] (M : Type u_5) [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] (x : exteriorPower.presentation.Rels R ι M),
  (exteriorPower.presentation.relations R ι M).relation x =
    match x with
    | exteriorPower.presentation.Rels.add m i x y =>
      ((fun₀ | Function.update m i x => 1) + fun₀ | Function.update m i y => 1) -
        fun₀ | Function.update m i (x + y) => 1
    | exteriorPower.presentation.Rels.smul m i r x =>
      (fun₀ | Function.update m i (r • x) => 1) - r • fun₀ | Function.update m i x => 1
    | exteriorPower.presentation.Rels.alt m i j hm hij => fun₀ | m => 1
-- Mathlib.Topology.Algebra.ConstMulAction
Continuous.fun_const_vadd : ∀ {M : Type u_1} {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : VAdd M α] [ContinuousConstVAdd M α]
  [inst_3 : TopologicalSpace β] {g : β → α}, Continuous g → ∀ (c : M), Continuous fun i => c +ᵥ g i
-- Mathlib.LinearAlgebra.Matrix.Transvection
Matrix.TransvectionStruct.toMatrix.congr_simp : ∀ {n : Type u_1} {R : Type u₂} {inst : DecidableEq n} [inst_1 : DecidableEq n] [inst_2 : CommRing R]
  (t t_1 : Matrix.TransvectionStruct n R),
  t = t_1 → ∀ (a a_1 : n), a = a_1 → ∀ (a_2 a_3 : n), a_2 = a_3 → t.toMatrix a a_2 = t_1.toMatrix a_1 a_3
-- Mathlib.CategoryTheory.Limits.Sifted
/-- A category `C` `IsSiftedOrEmpty` if the diagonal functor `C ⥤ C × C` is final.  -/
CategoryTheory.IsSiftedOrEmpty : (C : Type u) → [CategoryTheory.Category.{v, u} C] → Prop
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.dblU_smul : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Projective F} (P : Fin 3 → F) (u : F),
  W.dblU (u • P) = u ^ 4 * W.dblU P
-- Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
/-- If `I` and `I'` are initial, they are isomorphic.  -/
CategoryTheory.Limits.IsInitial.uniqueUpToIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {I I' : C} → CategoryTheory.Limits.IsInitial I → CategoryTheory.Limits.IsInitial I' → (I ≅ I')