mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Matrix.Normed
Matrix.linfty_opNNNorm_eq_opNNNorm : ∀ {m : Type u_3} {n : Type u_4} {α : Type u_5} [inst : Fintype m] [inst_1 : Fintype n]
  [inst_2 : NontriviallyNormedField α] [NormedAlgebra ℝ α] (A : Matrix m n α),
  ‖A‖₊ = ‖{ toLinearMap := A.mulVecLin, cont := ⋯ }‖₊
-- Mathlib.Combinatorics.Graph.Basic
Graph.vertexSet_copy : ∀ {α : Type u_1} {β : Type u_2} (G : Graph α β) {vertexSet : Set α} {edgeSet : Set β} {IsLink : β → α → α → Prop}
  (hvertexSet : G.vertexSet = vertexSet) (hedgeSet : G.edgeSet = edgeSet)
  (hIsLink : ∀ (e : β) (x y : α), G.IsLink e x y ↔ IsLink e x y),
  (G.copy hvertexSet hedgeSet hIsLink).vertexSet = vertexSet
-- Mathlib.Topology.CompactOpen
/-- To show continuity of a map `α → C(β, γ)`, it suffices to show that its uncurried form
`α × β → γ` is continuous.  -/
ContinuousMap.continuous_of_continuous_uncurry : ∀ {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] (f : X → C(Y, Z)), Continuous (Function.uncurry fun x y => (f x) y) → Continuous f
-- Init.Data.List.ToArray
Array.forM.eq_1 : ∀ {α : Type u} {m : Type v → Type w} [inst : Monad m] (f : α → m PUnit.{v + 1}) (as : Array α) (start stop : ℕ),
  Array.forM f as start stop = Array.foldlM (fun x => f) PUnit.unit as start stop
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.isSeparator_detector : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasEqualizers C]
  [inst_2 : CategoryTheory.HasDetector C], CategoryTheory.IsSeparator (CategoryTheory.detector C)
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.nonUnitalNonAssocSemiring : {R : Type u_1} → {M : Type u_4} → [inst : Semiring R] → [Mul M] → NonUnitalNonAssocSemiring (MonoidAlgebra R M)
-- Mathlib.Topology.LocallyFinsupp
/-- Functions with locally finite support within `U` form an additive submonoid of functions `X → Y`.
 -/
Function.locallyFinsuppWithin.addSubmonoid : {X : Type u_1} → [TopologicalSpace X] → Set X → {Y : Type u_2} → [inst : AddMonoid Y] → AddSubmonoid (X → Y)
-- Mathlib.GroupTheory.SpecificGroups.Alternating
card_alternatingGroup : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] [Nontrivial α],
  Fintype.card ↥(alternatingGroup α) = (Fintype.card α).factorial / 2
-- Init.Data.Iterators.Consumers.Partial
Std.Iter.Partial.mk.sizeOf_spec : ∀ {α β : Type w} [inst : SizeOf α] [inst_1 : SizeOf β] (it : Std.Iter β), sizeOf { it := it } = 1 + sizeOf it
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
CategoryTheory.Oplax.OplaxTrans.Modification.whiskerLeft_naturality : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.OplaxFunctor B C} {η θ : F ⟶ G} (Γ : CategoryTheory.Oplax.OplaxTrans.Modification η θ) {b c : B}
  {a' : C} (f : a' ⟶ F.obj b) (g : b ⟶ c),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerLeft (F.map g) (Γ.app c)))
      (CategoryTheory.Bicategory.whiskerLeft f (θ.naturality g)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (η.naturality g))
      (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerRight (Γ.app b) (G.map g)))
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.Hom.w : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : D} {T : CategoryTheory.Functor C D} {X Y : CategoryTheory.StructuredArrow S T} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp X.hom (T.map (CategoryTheory.StructuredArrow.Hom.right f)) = Y.hom
-- Mathlib.Data.Quot
Quotient.liftOn₂'_mk'' : ∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {s₁ : Setoid α} {s₂ : Setoid β} (f : α → β → γ)
  (h : ∀ (a₁ : α) (a₂ : β) (b₁ : α) (b₂ : β), s₁ a₁ b₁ → s₂ a₂ b₂ → f a₁ a₂ = f b₁ b₂) (a : α) (b : β),
  (Quotient.mk'' a).liftOn₂' (Quotient.mk'' b) f h = f a b
-- Mathlib.Algebra.GroupWithZero.NonZeroDivisors
mem_nonZeroDivisorsRight_iff : ∀ (M₀ : Type u_1) [inst : MonoidWithZero M₀] {x : M₀}, x ∈ nonZeroDivisorsRight M₀ ↔ ∀ (y : M₀), y * x = 0 → y = 0
-- Mathlib.Analysis.Distribution.SchwartzSpace.Deriv
SchwartzMap.instContinuousLineDeriv : ∀ {E : Type u_5} {F : Type u_8} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace ℝ F]
  [inst_3 : NormedSpace ℝ E], ContinuousLineDeriv E (SchwartzMap E F) (SchwartzMap E F)
-- Std.Data.DHashMap.Internal.Raw
Std.DHashMap.Internal.Raw.filterMap_eq : ∀ {α : Type u} {β : α → Type v} {δ : α → Type w} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β}
  (h : m.WF) {f : (a : α) → β a → Option (δ a)},
  Std.DHashMap.Raw.filterMap f m = ↑(Std.DHashMap.Internal.Raw₀.filterMap f ⟨m, ⋯⟩)
-- Mathlib.Algebra.Group.Semiconj.Units
/-- `a` semiconjugates `x` to `a * x * a⁻¹`.  -/
Units.mk_semiconjBy : ∀ {M : Type u_1} [inst : Monoid M] (u : Mˣ) (x : M), SemiconjBy (↑u) x (↑u * x * ↑u⁻¹)
-- Mathlib.Order.Filter.Basic
Filter.EventuallyEq.vadd : ∀ {α : Type u} {β : Type v} {𝕜 : Type u_2} [inst : VAdd 𝕜 β] {l : Filter α} {f f' : α → 𝕜} {g g' : α → β},
  f =ᶠ[l] f' → g =ᶠ[l] g' → (fun x => f x +ᵥ g x) =ᶠ[l] fun x => f' x +ᵥ g' x
-- Mathlib.Tactic.Ring.Common
/-- The number 1 represented as a BaseType.  -/
Mathlib.Tactic.Ring.Common.RingCompute.one : {u : Lean.Level} →
  {α : Q(Type u)} →
    {BaseType : Q(«$α») → Type} →
      {sα : Q(CommSemiring «$α»)} →
        Mathlib.Tactic.Ring.Common.RingCompute BaseType sα → Mathlib.Tactic.Ring.Common.Result BaseType q(Nat.rawCast 1)
-- Mathlib.Data.TypeVec
TypeVec.subtypeVal_toSubtype : ∀ {n : ℕ} {α : TypeVec.{u_1} n} (p : α.Arrow (TypeVec.repeat n Prop)),
  TypeVec.comp (TypeVec.subtypeVal p) (TypeVec.toSubtype p) = fun x => Subtype.val
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Hom.range_id : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M], (FirstOrder.Language.Hom.id L M).range = ⊤
-- Mathlib.Probability.Kernel.Composition.MeasureComp
ProbabilityTheory.Kernel.comp_boolKernel : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : ProbabilityTheory.Kernel α β)
  (μ ν : MeasureTheory.Measure α),
  κ.comp (ProbabilityTheory.Kernel.boolKernel μ ν) = ProbabilityTheory.Kernel.boolKernel (μ.bind ⇑κ) (ν.bind ⇑κ)
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
/-- This structure contains the data of a family of objects `X i` which cover
the terminal object, and of a presentation of `M.over (X i)` for all `i`.  -/
SheafOfModules.QuasicoherentData : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {R : CategoryTheory.Sheaf J RingCat} →
        [∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] →
          [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] →
            SheafOfModules R → Type (max (max (max (u + 1) u₁) v₁) (w + 1))
-- Mathlib.Algebra.Torsor.Basic
/-- `Equiv.constSMul` as a homomorphism from `G` to `Equiv.perm P`  -/
Equiv.constSMulHom : {G : Type u_1} → (P : Type u_2) → [inst : Group G] → [Torsor G P] → G →* Equiv.Perm P
-- Lean.Elab.ConfigEval.DeriveEvalConfigItem
_private.Lean.Elab.ConfigEval.DeriveEvalConfigItem.0.Lean.Elab.ConfigEval.HandlerTrie.brecOn_3.go : {motive_1 : Lean.Elab.ConfigEval.HandlerTrie✝ → Sort u} →
  {motive_2 : Array (String × Lean.Elab.ConfigEval.HandlerTrie✝) → Sort u} →
    {motive_3 : List (String × Lean.Elab.ConfigEval.HandlerTrie✝) → Sort u} →
      {motive_4 : String × Lean.Elab.ConfigEval.HandlerTrie✝ → Sort u} →
        (t : String × Lean.Elab.ConfigEval.HandlerTrie✝) →
          ((t : Lean.Elab.ConfigEval.HandlerTrie✝) → Lean.Elab.ConfigEval.HandlerTrie.below✝ t → motive_1 t) →
            ((t : Array (String × Lean.Elab.ConfigEval.HandlerTrie✝)) →
                Lean.Elab.ConfigEval.HandlerTrie.below_1✝ t → motive_2 t) →
              ((t : List (String × Lean.Elab.ConfigEval.HandlerTrie✝)) →
                  Lean.Elab.ConfigEval.HandlerTrie.below_2✝ t → motive_3 t) →
                ((t : String × Lean.Elab.ConfigEval.HandlerTrie✝) →
                    Lean.Elab.ConfigEval.HandlerTrie.below_3✝ t → motive_4 t) →
                  motive_4 t ×' Lean.Elab.ConfigEval.HandlerTrie.below_3✝ t
-- Mathlib.Data.DFinsupp.Lex
DFinsupp.lex_lt_of_lt_of_preorder : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → Zero (α i)] [inst_1 : (i : ι) → Preorder (α i)] (r : ι → ι → Prop)
  [IsStrictOrder ι r] {x y : Π₀ (i : ι), α i}, x < y → ∃ i, (∀ (j : ι), r j i → x j ≤ y j ∧ y j ≤ x j) ∧ x i < y i
-- Mathlib.RingTheory.MvPolynomial.Homogeneous
MvPolynomial.isHomogeneous_X_pow : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommSemiring R] (i : σ) (n : ℕ), (MvPolynomial.X i ^ n).IsHomogeneous n
-- Mathlib.CategoryTheory.Comma.Over.Pullback
CategoryTheory.Under.postAdjunctionRight_counit_app_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Limits.HasPushouts D] {Y : D} {F : CategoryTheory.Functor C D}
  {G : CategoryTheory.Functor D C} (a : F ⊣ G) (X : CategoryTheory.Under ((CategoryTheory.Functor.id D).obj Y)),
  ((CategoryTheory.Under.postAdjunctionRight a).counit.app X).right =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pushout.desc
        (CategoryTheory.Limits.pushout.inl
          (F.map
            (CategoryTheory.CategoryStruct.comp (a.unit.app (G.1 Y))
              (G.map (CategoryTheory.CategoryStruct.comp (a.counit.app Y) X.hom))))
          (a.counit.app Y))
        (CategoryTheory.Limits.pushout.inr
          (F.map
            (CategoryTheory.CategoryStruct.comp (a.unit.app (G.1 Y))
              (G.map (CategoryTheory.CategoryStruct.comp (a.counit.app Y) X.hom))))
          (a.counit.app Y))
        ⋯)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pushout.desc
          (CategoryTheory.CategoryStruct.comp (a.counit.app X.right)
            (CategoryTheory.Limits.pushout.inl (CategoryTheory.CategoryStruct.comp (a.counit.app Y) X.hom)
              (a.counit.app Y)))
          (CategoryTheory.Limits.pushout.inr (CategoryTheory.CategoryStruct.comp (a.counit.app Y) X.hom)
            (a.counit.app Y))
          ⋯)
        (CategoryTheory.Limits.pushout.desc (CategoryTheory.CategoryStruct.id X.right) X.hom ⋯))
-- Init.SizeOf
List.cons.sizeOf_spec : ∀ {α : Type u} [inst : SizeOf α] (head : α) (tail : List α), sizeOf (head :: tail) = 1 + sizeOf head + sizeOf tail
-- Std.Http.Internal.IndexMultiMap
/-- Merges two multimaps, combining values for shared keys.
 -/
Std.Internal.IndexMultiMap.merge : {α : Type u} →
  {β : Type v} →
    [inst : BEq α] →
      [inst_1 : Hashable α] →
        [EquivBEq α] →
          [LawfulHashable α] →
            Std.Internal.IndexMultiMap α β → Std.Internal.IndexMultiMap α β → Std.Internal.IndexMultiMap α β
-- Init.Data.Array.Lemmas
Array.any_flatten : ∀ {α : Type u_1} {f : α → Bool} {xss : Array (Array α)}, xss.flatten.any f = xss.any fun x => x.any f
-- Mathlib.AlgebraicGeometry.AffineScheme
/-- Variant of `AlgebraicGeometry.localRingHom_comp_stalkIso` for `Spec.map`.  -/
AlgebraicGeometry.Scheme.localRingHom_comp_stalkIso : ∀ {R S : CommRingCat} (f : R ⟶ S) (p : PrimeSpectrum ↑S),
  CategoryTheory.CategoryStruct.comp
      (AlgebraicGeometry.Spec.stalkIso R (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p)).hom
      (CategoryTheory.CategoryStruct.comp
        (CommRingCat.ofHom
          (Localization.localRingHom (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p).asIdeal p.asIdeal
            (CommRingCat.Hom.hom f) ⋯))
        (AlgebraicGeometry.Spec.stalkIso S p).inv) =
    AlgebraicGeometry.Scheme.Hom.stalkMap (AlgebraicGeometry.Spec.map f) p
-- Mathlib.Analysis.Normed.Group.Continuity
Filter.Tendsto.nnnorm : ∀ {α : Type u_1} {E : Type u_4} [inst : SeminormedAddGroup E] {a : E} {l : Filter α} {f : α → E},
  Filter.Tendsto f l (nhds a) → Filter.Tendsto (fun x => ‖f x‖₊) l (nhds ‖a‖₊)
-- Mathlib.MeasureTheory.Measure.ProbabilityMeasure
MeasureTheory.ProbabilityMeasure.val_eq_to_measure : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] (ν : MeasureTheory.ProbabilityMeasure Ω), ↑ν = ↑ν
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.map_id_equiv : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β},
  m.WF → (Std.HashMap.Raw.map (fun x v => v) m).Equiv m
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.stdSimplex.map_objEquiv_symm : ∀ {n : SimplexCategory} {m m' : SimplexCategoryᵒᵖ} (f : Opposite.unop m ⟶ n) (g : m ⟶ m'),
  (CategoryTheory.ConcreteCategory.hom ((SSet.stdSimplex.obj n).map g)) (SSet.stdSimplex.objEquiv.symm f) =
    SSet.stdSimplex.objEquiv.symm (CategoryTheory.CategoryStruct.comp g.unop f)
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.get?_tail : ∀ {α : Type u} (s : Stream'.WSeq α) (n : ℕ), s.tail.get? n = s.get? (n + 1)
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.ciSup_mul : ∀ {ι : Type u} (f : ι → Cardinal.{v}) (c : Cardinal.{v}), (⨆ i, f i) * c = ⨆ i, f i * c
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousLinearMap.compLeftContinuous_apply : ∀ (R : Type u_3) {M : Type u_5} [inst : TopologicalSpace M] {M₂ : Type u_6} [inst_1 : TopologicalSpace M₂]
  [inst_2 : Semiring R] [inst_3 : AddCommMonoid M] [inst_4 : AddCommMonoid M₂] [inst_5 : ContinuousAdd M]
  [inst_6 : Module R M] [inst_7 : ContinuousConstSMul R M] [inst_8 : ContinuousAdd M₂] [inst_9 : Module R M₂]
  [inst_10 : ContinuousConstSMul R M₂] (α : Type u_7) [inst_11 : TopologicalSpace α] (g : M →L[R] M₂) (a : C(α, M)),
  (ContinuousLinearMap.compLeftContinuous R α g) a =
    (↑(AddMonoidHom.compLeftContinuous α (↑g).toAddMonoidHom ⋯)).toFun a
-- Mathlib.CategoryTheory.Filtered.Small
CategoryTheory.IsCofiltered.cofilteredClosure.base : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.IsCofilteredOrEmpty C] {α : Type w}
  {f : α → C} (x : α), CategoryTheory.IsCofiltered.cofilteredClosure f (f x)
-- Mathlib.Topology.Homeomorph.Defs
/-- Precomposing by a homeomorphism does not change the image of the frontier of a preimage.  -/
image_frontier_preimage_comp : ∀ {X : Type u_5} {Y : Type u_6} {Z : Type u_7} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : X → Y),
  IsHomeomorph e → ∀ (f : Y → Z) (s : Set Z), f ∘ e '' frontier (f ∘ e ⁻¹' s) = f '' frontier (f ⁻¹' s)
-- Batteries.Data.Nat.Bitwise.Lemmas
Nat.eq_of_xor_eq_zero : ∀ {x y : ℕ}, x ^^^ y = 0 → x = y
-- Mathlib.FieldTheory.LinearDisjoint
/-- Linear disjointness is symmetric.  -/
IntermediateField.linearDisjoint_comm' : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {L : Type w} [inst_3 : Field L]
  [inst_4 : Algebra F L] [inst_5 : Algebra L E] [inst_6 : IsScalarTower F L E] {L' : Type u_1} [inst_7 : Field L']
  [inst_8 : Algebra F L'] [inst_9 : Algebra L' E] [inst_10 : IsScalarTower F L' E],
  (IsScalarTower.toAlgHom F L E).fieldRange.LinearDisjoint L' ↔
    (IsScalarTower.toAlgHom F L' E).fieldRange.LinearDisjoint L
-- Mathlib.Algebra.BigOperators.Expect
Finset.mul_expect : ∀ {ι : Type u_1} {M : Type u_4} [inst : Semiring M] [inst_1 : Module ℚ≥0 M] [SMulCommClass ℚ≥0 M M] (s : Finset ι)
  (f : ι → M) (a : M), (a * s.expect fun i => f i) = s.expect fun i => a * f i
-- Mathlib.AlgebraicTopology.CechNerve
/-- the isomorphism to the product induced by the limit cone `wideCospan ι X`  -/
CategoryTheory.CechNerveTerminalFrom.wideCospan.limitIsoPi : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasTerminal C] →
      (ι : Type w) →
        [inst_2 : CategoryTheory.Limits.HasFiniteProducts C] →
          [inst_3 : Finite ι] →
            (X : C) → CategoryTheory.Limits.limit (CategoryTheory.CechNerveTerminalFrom.wideCospan ι X) ≅ ∏ᶜ fun x => X
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
/-- The seminorms on the space `𝓓^{n}_{K}(E, F)` given by the sup norm of the iterated derivatives.
In the scope `Distributions.Seminorm`, we denote them by `N[𝕜; F]_{K, n, i}`
(or `N[𝕜]_{K, n, i}`), or simply by `N[𝕜; F]_{K, i}` (or `N[𝕜; F]_{K, i}`) when `n = ∞`.  -/
Distributions.«termN[_]_{_,_,_}» : Lean.ParserDescr
-- Init.Data.Iterators.Basic
/-- Wraps the state of an iterator into an `Iter` object.  -/
Std.IterM.mk : {α : Type w} → {m : Type w → Type w'} → {β : Type w} → α → Std.IterM m β
-- Std.Internal.UV.System
Std.Internal.UV.System.instInhabitedCPUTimes : Inhabited Std.Internal.UV.System.CPUTimes
-- Mathlib.Order.OrdContinuous
RightOrdContinuous.le_iff : ∀ {α : Type u} {β : Type v} [inst : SemilatticeInf α] [inst_1 : SemilatticeInf β] {f : α → β},
  RightOrdContinuous f → Function.Injective f → ∀ {x y : α}, f y ≤ f x ↔ y ≤ x
-- Std.Time.Format.Modifier
Std.Time.Modifier.M.inj : ∀ {presentation presentation_1 : Std.Time.Number ⊕ Std.Time.Text},
  Std.Time.Modifier.M presentation = Std.Time.Modifier.M presentation_1 → presentation = presentation_1
-- Mathlib.GroupTheory.Divisible
Pi.divisibleBy.eq_1 : ∀ {ι : Type u_3} {β : Type u_4} (B : ι → Type u_5) [inst : (i : ι) → SMul β (B i)] [inst_1 : Zero β]
  [inst_2 : (i : ι) → AddMonoid (B i)] [inst_3 : (i : ι) → DivisibleBy (B i) β],
  Pi.divisibleBy B = { div := fun x n i => DivisibleBy.div (x i) n, div_zero := ⋯, div_cancel := ⋯ }
-- Mathlib.Algebra.Group.Submonoid.Basic
Submonoid.mem_closure : ∀ {M : Type u_1} [inst : MulOneClass M] {s : Set M} {x : M},
  x ∈ Submonoid.closure s ↔ ∀ (S : Submonoid M), s ⊆ ↑S → x ∈ S
-- Init.Util
panicWithPos : {α : Sort u} → [Inhabited α] → String → ℕ → ℕ → String → α
-- Mathlib.Topology.UniformSpace.UniformConvergence
/-- Uniform convergence implies pointwise convergence.  -/
TendstoUniformly.tendsto_at : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι},
  TendstoUniformly F f p → ∀ (x : α), Filter.Tendsto (fun n => F n x) p (nhds (f x))
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.card_commonNeighbors_top : ∀ {V : Type u_1} [inst : Fintype V] [inst_1 : DecidableEq V] {v w : V},
  v ≠ w → Fintype.card ↑(⊤.commonNeighbors v w) = Fintype.card V - 2
-- Lean.Parser.Do
Lean.Parser.Term.doIf.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Combinatorics.SimpleGraph.Extremal.Zarankiewicz
/-- `zarankiewicz m n s t` is greater than `x` if and only if there
exists a `completeBipartiteGraph α β`-free bipartite graph `G` with more than `x` edges.  -/
SimpleGraph.lt_zarankiewicz_iff_of_nonneg : ∀ {m n s t : ℕ} {V : Type u_1} {W : Type u_2} {α : Type u_3} {β : Type u_4} [inst : Fintype V] [inst_1 : Fintype W]
  [inst_2 : Fintype α] [inst_3 : Fintype β] {R : Type u_5} [inst_4 : Semiring R] [inst_5 : LinearOrder R]
  [FloorSemiring R],
  Fintype.card V = m →
    Fintype.card W = n →
      Fintype.card α = s →
        Fintype.card β = t →
          ∀ {x : R},
            0 ≤ x →
              (x < ↑(SimpleGraph.zarankiewicz m n s t) ↔
                ∃ G x_1, G ≤ completeBipartiteGraph V W ∧ (completeBipartiteGraph α β).Free G ∧ x < ↑G.edgeFinset.card)
-- Mathlib.Topology.Basic
isOpen_iInter_of_finite : ∀ {X : Type u} {ι : Sort v} [inst : TopologicalSpace X] [Finite ι] {s : ι → Set X},
  (∀ (i : ι), IsOpen (s i)) → IsOpen (⋂ i, s i)
-- Mathlib.Algebra.Category.HopfAlgCat.Basic
_private.Mathlib.Algebra.Category.HopfAlgCat.Basic.0.HopfAlgCat.mk : {R : Type u} →
  [inst : CommRing R] →
    (carrier : Type v) → [instRing : Ring carrier] → [instHopfAlgebra : HopfAlgebra R carrier] → HopfAlgCat R
-- Mathlib.RingTheory.PiTensorProduct
PiTensorProduct.instSemiring : {ι : Type u_1} →
  {R : Type u_3} →
    {A : ι → Type u_4} →
      [inst : CommSemiring R] →
        [inst_1 : (i : ι) → Semiring (A i)] →
          [inst_2 : (i : ι) → Algebra R (A i)] → Semiring (PiTensorProduct R fun i => A i)
-- Std.Time.DateTime.WallTime
_private.Std.Time.DateTime.WallTime.0.Std.Time.WallTime.mk : Std.Time.Duration → Std.Time.WallTime
-- Mathlib.CategoryTheory.Category.Bipointed
Bipointed.swapEquiv_inverse_obj_toProd : ∀ (X : Bipointed), (Bipointed.swapEquiv.inverse.obj X).toProd = X.toProd.swap
-- Mathlib.GroupTheory.GroupAction.Hom
AddActionHom.inverse_apply : ∀ {M : Type u_2} {X : Type u_5} [inst : VAdd M X] {Y₁ : Type u_8} [inst_1 : VAdd M Y₁] (f : X →ₑ[id] Y₁) (g : Y₁ → X)
  (h₁ : Function.LeftInverse g ⇑f) (h₂ : Function.RightInverse g ⇑f) (a : Y₁), (f.inverse g h₁ h₂) a = g a
-- Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple
/-- An auxiliary lemma en route to `RootPairing.GeckConstruction.isNilpotent_e`.  -/
_private.Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple.0.RootPairing.GeckConstruction.isNilpotent_e_aux : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : IsDomain R]
  [inst_2 : CharZero R] [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : AddCommGroup N] [inst_6 : Module R N]
  {P : RootPairing ι R M N} [inst_7 : P.IsCrystallographic] [P.IsReduced] {b : P.Base} [inst_9 : Fintype ι]
  [inst_10 : DecidableEq ι] (i : ↥b.support) {j : ι} (n : ℕ),
  j ≠ -↑i →
    (RootPairing.GeckConstruction.e i ^ n).col (Sum.inr j) = 0 ∨
      ∃ k x,
        P.root k = P.root j + n • P.root ↑i ∧
          (RootPairing.GeckConstruction.e i ^ n).col (Sum.inr j) = x • Pi.single (Sum.inr k) 1
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey!_eq_default_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {a : α}, t.contains a = false → t.getKey! a = default
-- Mathlib.MeasureTheory.Group.AEStabilizer
AddAction.coe_aestabilizer : ∀ (G : Type u_1) {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] {x : MeasurableSpace α}
  (μ : MeasureTheory.Measure α) [inst_2 : MeasureTheory.VAddInvariantMeasure G α μ] (s : Set α),
  ↑(AddAction.aestabilizer G μ s) = {g | g +ᵥ s =ᵐ[μ] s}
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.size_insertManyIfNewUnit_list : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α Unit cmp} [Std.TransCmp cmp] [inst : BEq α]
  [Std.LawfulBEqCmp cmp],
  t.WF →
    ∀ {l : List α},
      List.Pairwise (fun a b => ¬cmp a b = Ordering.eq) l →
        (∀ a ∈ t, l.contains a = false) → (t.insertManyIfNewUnit l).size = t.size + l.length
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits
PresheafOfModules.Finite.toPresheaf_preservesFiniteColimits : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (R : CategoryTheory.Functor Cᵒᵖ RingCat),
  CategoryTheory.Limits.PreservesFiniteColimits (PresheafOfModules.toPresheaf R)
-- Mathlib.Algebra.Group.Subsemigroup.Operations
Subsemigroup.comap_surjective_of_injective : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] {f : M →ₙ* N},
  Function.Injective ⇑f → Function.Surjective (Subsemigroup.comap f)
-- Mathlib.RingTheory.Polynomial.Basic
/-- The `R`-submodule of `R[X]` consisting of polynomials of degree < `n`.  -/
Polynomial.degreeLT : (R : Type u) → [inst : Semiring R] → ℕ → Submodule R (Polynomial R)
-- Mathlib.Analysis.InnerProductSpace.Defs
/-- The inner product is additive in the first coordinate.  -/
InnerProductSpace.add_left : ∀ {𝕜 : Type u_4} {E : Type u_5} {inst : RCLike 𝕜} {inst_1 : SeminormedAddCommGroup E} [self : InnerProductSpace 𝕜 E]
  (x y z : E), inner 𝕜 (x + y) z = inner 𝕜 x z + inner 𝕜 y z
-- Mathlib.Logic.Small.Basic
small_of_injective : ∀ {α : Type v} {β : Type w} [Small.{u, w} β] {f : α → β}, Function.Injective f → Small.{u, v} α
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.AddMon.Hom.hom_zero : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {M N : CategoryTheory.AddMon C}
  [inst_3 : CategoryTheory.IsCommAddMonObj N.X], CategoryTheory.AddMon.Hom.hom 0 = 0
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.Formatter.recover'.formatter : Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter
-- Mathlib.RingTheory.Localization.Away.AdjoinRoot
/-- The `R`-`AlgEquiv` between the localization of `R` away from `r` and
`R` with an inverse of `r` adjoined.  -/
Localization.awayEquivAdjoin : {R : Type u_1} →
  [inst : CommRing R] → (r : R) → Localization.Away r ≃ₐ[R] AdjoinRoot (Polynomial.C r * Polynomial.X - 1)