mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FlatMap
Std.Iterators.Types.Flatten.IsPlausibleStep.outerYield_flatMap : ∀ {α β α₂ γ : Type w} {m : Type w → Type w'} [inst : Monad m] [LawfulMonad m] [inst_2 : Std.Iterator α m β]
  [inst_3 : Std.Iterator α₂ m γ] {f : β → Std.IterM m γ} {it₁ it₁' : Std.IterM m β} {b : β},
  it₁.IsPlausibleStep (Std.IterStep.yield it₁' b) →
    (Std.IterM.flatMapAfter f it₁ none).IsPlausibleStep (Std.IterStep.skip (Std.IterM.flatMapAfter f it₁' (some (f b))))
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
/-- One can reformulate smoothness within a set at a point as continuity within this set at this
point, and smoothness in any chart containing that point.  -/
mdifferentiableWithinAt_iff_of_mem_source : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {x : M} {s : Set M}
  [IsManifold I 1 M] [IsManifold I' 1 M'] {x' : M} {y : M'},
  x' ∈ (chartAt H x).source →
    f x' ∈ (chartAt H' y).source →
      (MDiffAt[s] f x' ↔
        ContinuousWithinAt f s x' ∧
          DifferentiableWithinAt 𝕜 (↑(extChartAt I' y) ∘ f ∘ ↑(extChartAt I x).symm)
            (↑(extChartAt I x).symm ⁻¹' s ∩ Set.range ↑I) (↑(extChartAt I x) x'))
-- Mathlib.MeasureTheory.VectorMeasure.Basic
/-- A vector measure over `ℝ≥0∞` is a measure.  -/
MeasureTheory.VectorMeasure.ennrealToMeasure : {α : Type u_1} → {x : MeasurableSpace α} → MeasureTheory.VectorMeasure α ENNReal → MeasureTheory.Measure α
-- Mathlib.Data.Finsupp.Basic
Finsupp.sigma_support : ∀ {ι : Type u_4} {M : Type u_5} {αs : ι → Type u_12} [inst : Zero M] (l : (i : ι) × αs i →₀ M),
  l.support = l.splitSupport.sigma fun i => (l.split i).support
-- Mathlib.RingTheory.Polynomial.HilbertPoly
/-- The polynomial satisfying the key property of `Polynomial.hilbertPoly p d` is unique.
 -/
Polynomial.existsUnique_hilbertPoly : ∀ {F : Type u_1} [inst : Field F] [CharZero F] (p : Polynomial F) (d : ℕ),
  ∃! h, ∃ N, ∀ n > N, (PowerSeries.coeff n) (↑p * ↑(PowerSeries.invOneSubPow F d)) = Polynomial.eval (↑n) h
-- Mathlib.CategoryTheory.CodiscreteCategory
CategoryTheory.codiscreteEquiv_apply : ∀ {α : Type u} (self : CategoryTheory.Codiscrete α), CategoryTheory.codiscreteEquiv self = self.as
-- Mathlib.RingTheory.Polynomial.Tower
Polynomial.aeval_root_of_mapAlg_eq_multiset_prod_X_sub_C : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : CommRing A] [inst_2 : Algebra R A] (s : Multiset A)
  {x : A},
  x ∈ s →
    ∀ {p : Polynomial R},
      (Polynomial.mapAlg R A) p = (Multiset.map (fun x => Polynomial.X - Polynomial.C x) s).prod →
        (Polynomial.aeval x) p = 0
-- Mathlib.Analysis.Complex.Norm
Complex.norm_conj : ∀ (z : ℂ), ‖(starRingEnd ℂ) z‖ = ‖z‖
-- Init.Data.SInt.Bitwise
ISize.xor_zero : ∀ {a : ISize}, a ^^^ 0 = a
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.le_min_iff : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] {a b c : (a : α) × β a}, a ≤ b ⊓ c ↔ a ≤ b ∧ a ≤ c
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonTypeDefinitionParams.toJson : Lean.Lsp.TypeDefinitionParams → Lean.Json
-- Mathlib.GroupTheory.Nilpotent
/-- A finite group is nilpotent iff the normalizer condition holds, and iff all maximal groups are
normal and iff all Sylow groups are normal and iff the group is the direct product of its Sylow
groups.  -/
Group.isNilpotent_of_finite_tfae : ∀ {G : Type u_1} [hG : Group G] [Finite G],
  [Group.IsNilpotent G, NormalizerCondition G, ∀ (H : Subgroup G), IsCoatom H → H.Normal,
      ∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (P : Sylow p G), (↑P).Normal,
      Nonempty (((p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p) G) → ↥↑P) ≃* G)].TFAE
-- Mathlib.Data.Matrix.Block
Matrix.blockDiagonalAddMonoidHom_apply : ∀ (m : Type u_2) (n : Type u_3) (o : Type u_4) (α : Type u_12) [inst : DecidableEq o] [inst_1 : AddZeroClass α]
  (M : o → Matrix m n α), (Matrix.blockDiagonalAddMonoidHom m n o α) M = Matrix.blockDiagonal M
-- Mathlib.Tactic.Linter.DeprecatedSyntaxLinter
/-- The option `linter.style.maxHeartbeats` of the deprecated syntax linter flags usages of
`set_option <name-containing-maxHeartbeats> n in cmd` that do not add a comment explaining
the reason for the modification of the `maxHeartbeats`.

This includes `set_option maxHeartbeats n in` and `set_option synthInstance.maxHeartbeats n in`.
 -/
Mathlib.Linter.Style.linter.style.maxHeartbeats : Lean.Option Bool
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.iIndepFun.indepFun : ∀ {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {β : ι → Type u_6}
  {m : (x : ι) → MeasurableSpace (β x)} {f : (i : ι) → Ω → β i},
  ProbabilityTheory.iIndepFun f μ → ∀ {i j : ι}, i ≠ j → ProbabilityTheory.IndepFun (f i) (f j) μ
-- Mathlib.Topology.Homeomorph.Lemmas
Homeomorph.comap_cocompact : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (h : X ≃ₜ Y),
  Filter.comap (⇑h) (Filter.cocompact Y) = Filter.cocompact X
-- Mathlib.LinearAlgebra.Prod
LinearMap.isCompl_range_inl_inr : ∀ {R : Type u} {M : Type v} {M₂ : Type w} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M₂]
  [inst_3 : Module R M] [inst_4 : Module R M₂], IsCompl (LinearMap.inl R M M₂).range (LinearMap.inr R M M₂).range
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.indepFun_iff_measure_inter_preimage_eq_mul : ∀ {Ω : Type u_1} {β : Type u_6} {β' : Type u_7} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {f : Ω → β}
  {g : Ω → β'} {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'},
  ProbabilityTheory.IndepFun f g μ ↔
    ∀ (s : Set β) (t : Set β'), MeasurableSet s → MeasurableSet t → μ (f ⁻¹' s ∩ g ⁻¹' t) = μ (f ⁻¹' s) * μ (g ⁻¹' t)
-- Lean.Meta.Tactic.Simp.Simproc
Lean.Meta.Simp.SimprocDeclExtState.mk.sizeOf_spec : ∀ (builtin : Std.HashMap Lean.Name (Array Lean.Meta.SimpTheoremKey))
  (newEntries : Lean.PHashMap Lean.Name (Array Lean.Meta.SimpTheoremKey)),
  sizeOf { builtin := builtin, newEntries := newEntries } = 1 + sizeOf builtin + sizeOf newEntries
-- Mathlib.Topology.Algebra.InfiniteSum.Ring
SemiconjBy.tsum_right : ∀ {ι : Type u_1} {α : Type u_3} {L : SummationFilter ι} [inst : NonUnitalNonAssocSemiring α]
  [inst_1 : TopologicalSpace α] [IsTopologicalSemiring α] [T2Space α] [L.NeBot] {f g : ι → α} (a : α),
  Summable f L →
    Summable g L → (∀ (i : ι), SemiconjBy a (f i) (g i)) → SemiconjBy a (∑'[L] (i : ι), f i) (∑'[L] (i : ι), g i)
-- Batteries.Data.String.Lemmas
_private.Batteries.Data.String.Lemmas.0.Substring.Raw.get.match_1.splitter : (motive : Substring.Raw → String.Pos.Raw → Sort u_1) →
  (x : Substring.Raw) →
    (x_1 : String.Pos.Raw) →
      ((s : String) → (b stopPos p : String.Pos.Raw) → motive { str := s, startPos := b, stopPos := stopPos } p) →
        motive x x_1
-- Mathlib.Topology.Separation.Regular
T3Space.t25Space : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T3Space X], T25Space X
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.natDegree_X : ∀ {R : Type u} [inst : Semiring R] [Nontrivial R], Polynomial.X.natDegree = 1
-- Mathlib.CategoryTheory.Monoidal.Transport
CategoryTheory.Monoidal.instMonoidalTransportedFunctorEquivalenceTransported : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          (e : C ≌ D) → (CategoryTheory.Monoidal.equivalenceTransported e).functor.Monoidal
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.getKey!_alter : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β}
  [inst_2 : EquivBEq α] [LawfulHashable α] [inst_4 : Inhabited α] {k k' : α} {f : Option β → Option β},
  m.WF →
    (Std.DHashMap.Raw.Const.alter m k f).getKey! k' =
      if (k == k') = true then if (f (Std.DHashMap.Raw.Const.get? m k)).isSome = true then k else default
      else m.getKey! k'
-- Init.Data.List.Lemmas
List.flatten_eq_flatMap : ∀ {α : Type u_1} {L : List (List α)}, L.flatten = List.flatMap id L
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
/-- A functor `F` preserves biproducts of `f` if `F` maps every bilimit bicone over `f` to a
bilimit bicone over `F.obj ∘ f`.  -/
CategoryTheory.Limits.PreservesBiproduct : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
          [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] →
            {J : Type w₁} → (J → C) → (F : CategoryTheory.Functor C D) → [F.PreservesZeroMorphisms] → Prop
-- Mathlib.RingTheory.Valuation.ValuationSubring
/-- The canonical map on value groups induced by a coarsening of valuation rings.  -/
ValuationSubring.mapOfLE : {K : Type u} → [inst : Field K] → (R S : ValuationSubring K) → R ≤ S → R.ValueGroup →*₀ S.ValueGroup
-- Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
NNReal.agm_eq_ciInf : ∀ {x y : NNReal}, x.agm y = ⨅ n, (x.agmSequences y n).2
-- Mathlib.LinearAlgebra.CliffordAlgebra.Prod
/-- If `m₁` and `m₂` are both homogeneous,
and the quadratic spaces `Q₁` and `Q₂` map into
orthogonal subspaces of `Qₙ` (for instance, when `Qₙ = Q₁.prod Q₂`),
then the product of the embedding in `CliffordAlgebra Q` commutes up to a sign factor.  -/
CliffordAlgebra.map_mul_map_of_isOrtho_of_mem_evenOdd : ∀ {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M₁]
  [inst_2 : AddCommGroup M₂] [inst_3 : AddCommGroup N] [inst_4 : Module R M₁] [inst_5 : Module R M₂]
  [inst_6 : Module R N] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} {Qₙ : QuadraticForm R N} (f₁ : Q₁ →qᵢ Qₙ)
  (f₂ : Q₂ →qᵢ Qₙ),
  (∀ (x : M₁) (y : M₂), QuadraticMap.IsOrtho Qₙ (f₁ x) (f₂ y)) →
    ∀ (m₁ : CliffordAlgebra Q₁) (m₂ : CliffordAlgebra Q₂) {i₁ i₂ : ZMod 2},
      m₁ ∈ CliffordAlgebra.evenOdd Q₁ i₁ →
        m₂ ∈ CliffordAlgebra.evenOdd Q₂ i₂ →
          (CliffordAlgebra.map f₁) m₁ * (CliffordAlgebra.map f₂) m₂ =
            (-1) ^ (i₂ * i₁) • ((CliffordAlgebra.map f₂) m₂ * (CliffordAlgebra.map f₁) m₁)
-- Mathlib.Algebra.Order.Group.Opposite
AddOpposite.instPartialOrder.eq_1 : ∀ {α : Type u_1} [inst : PartialOrder α], AddOpposite.instPartialOrder = PartialOrder.lift AddOpposite.unop ⋯
-- Mathlib.Analysis.Calculus.FormalMultilinearSeries
constFormalMultilinearSeries.congr_simp : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] (E : Type u_2) [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : ContinuousConstSMul 𝕜 E] [inst_4 : IsTopologicalAddGroup E] {F : Type u_3}
  [inst_5 : NormedAddCommGroup F] [inst_6 : IsTopologicalAddGroup F] [inst_7 : NormedSpace 𝕜 F]
  [inst_8 : ContinuousConstSMul 𝕜 F] (c c_1 : F),
  c = c_1 → ∀ (n : ℕ), constFormalMultilinearSeries 𝕜 E c n = constFormalMultilinearSeries 𝕜 E c_1 n
-- Mathlib.MeasureTheory.Function.SimpleFuncDense
MeasureTheory.SimpleFunc.approxOn_mem : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : PseudoEMetricSpace α]
  [inst_2 : OpensMeasurableSpace α] [inst_3 : MeasurableSpace β] {f : β → α} (hf : Measurable f) {s : Set α} {y₀ : α}
  (h₀ : y₀ ∈ s) [inst_4 : TopologicalSpace.SeparableSpace ↑s] (n : ℕ) (x : β),
  (MeasureTheory.SimpleFunc.approxOn f hf s y₀ h₀ n) x ∈ s
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Int
Int.reduceFDiv : Lean.Meta.Simp.DSimproc
-- Mathlib.Topology.Order.LocalExtr
IsLocalMin.comp_continuous : ∀ {α : Type u} {β : Type v} {δ : Type x} [inst : TopologicalSpace α] [inst_1 : Preorder β] {f : α → β}
  [inst_2 : TopologicalSpace δ] {g : δ → α} {b : δ}, IsLocalMin f (g b) → ContinuousAt g b → IsLocalMin (f ∘ g) b
-- Mathlib.Algebra.PresentedMonoid.Basic
PresentedAddMonoid.inductionOn₂ : ∀ {α₁ : Type u_2} {α₂ : Type u_3} {rels₁ : FreeAddMonoid α₁ → FreeAddMonoid α₁ → Prop}
  {rels₂ : FreeAddMonoid α₂ → FreeAddMonoid α₂ → Prop} {δ : PresentedAddMonoid rels₁ → PresentedAddMonoid rels₂ → Prop}
  (q₁ : PresentedAddMonoid rels₁) (q₂ : PresentedAddMonoid rels₂),
  (∀ (a : FreeAddMonoid α₁) (b : FreeAddMonoid α₂),
      δ ((PresentedAddMonoid.mk rels₁) a) ((PresentedAddMonoid.mk rels₂) b)) →
    δ q₁ q₂
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKeyD_inter : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α],
  m₁.WF → m₂.WF → ∀ {k fallback : α}, (m₁ ∩ m₂).getKeyD k fallback = if k ∈ m₂ then m₁.getKeyD k fallback else fallback
-- Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Polynomial.le_trailingDegree_X_pow : ∀ {R : Type u} [inst : Semiring R] (n : ℕ), ↑n ≤ (Polynomial.X ^ n).trailingDegree
-- Lean.Meta.Tactic.Grind.Extension
/-- Abstracted universe level param names in the `rhs`  -/
Lean.Meta.Grind.CnstrRHS.levelNames : Lean.Meta.Grind.CnstrRHS → Array Lean.Name
-- Mathlib.Order.Defs.Unbundled
IsStrictTotalOrder.toTrichotomous : ∀ {α : Sort u_1} {lt : α → α → Prop} [self : IsStrictTotalOrder α lt], Std.Trichotomous lt
-- Lean.Parser.Basic
_private.Lean.Parser.Basic.0.Lean.Parser.mkResult : Lean.Parser.ParserState → ℕ → Lean.Parser.ParserState
-- Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesSubcomplex
SSet.Subcomplex.N.cast_eq_self : ∀ {X : SSet} {A : X.Subcomplex} (s : A.N) {d : ℕ} (hd : s.dim = d), s.cast hd = s
-- Mathlib.Tactic.FieldSimp
_private.Mathlib.Tactic.FieldSimp.0.Mathlib.Tactic.FieldSimp.qNF.toNF.match_1.eq_1 : ∀ {v : Lean.Level} {M : Q(Type v)} (motive : (ℤ × Q(«$M»)) × ℕ → Sort u_1) (a : ℤ) (x : Q(«$M»)) (snd : ℕ)
  (h_1 : (a : ℤ) → (x : Q(«$M»)) → (snd : ℕ) → motive ((a, x), snd)),
  (match ((a, x), snd) with
    | ((a, x), snd) => h_1 a x snd) =
    h_1 a x snd
-- Lean.Data.Lsp.Ipc
Lean.Lsp.Ipc.CallHierarchy.mk.sizeOf_spec : ∀ (item : Lean.Lsp.CallHierarchyItem) (fromRanges : Array Lean.Lsp.Range) (children : Array Lean.Lsp.Ipc.CallHierarchy),
  sizeOf { item := item, fromRanges := fromRanges, children := children } =
    1 + sizeOf item + sizeOf fromRanges + sizeOf children
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.disjoint_neighborSet : ∀ {V : Type u} {G H : SimpleGraph V}, (∀ (v : V), Disjoint (G.neighborSet v) (H.neighborSet v)) ↔ Disjoint G H
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.coeff_coeff_sumAlgEquiv_apply_apply_support_val : ∀ (R : Type u) (S₁ : Type v) (S₂ : Type w) [inst : CommSemiring R] (a : AddMonoidAlgebra R (S₁ ⊕ S₂ →₀ ℕ))
  (a_1 : S₁ →₀ ℕ),
  (((MvPolynomial.sumAlgEquiv R S₁ S₂) a).coeff a_1).coeff.support.val =
    Multiset.filterMap (fun x => if x.1 = a_1 then some x.2 else none)
      (Multiset.map (fun x => (Finsupp.comapDomain Sum.inl x ⋯, Finsupp.comapDomain Sum.inr x ⋯)) a.coeff.support.val)
-- Mathlib.Analysis.Asymptotics.TVS
Asymptotics.isLittleOTVS_iff_tendsto_inv_smul : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} [inst : NontriviallyNormedField 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] [ContinuousSMul 𝕜 E] {f : α → 𝕜} {g : α → E} {l : Filter α},
  (∀ᶠ (x : α) in l, f x = 0 → g x = 0) → (g =o[𝕜; l] f ↔ Filter.Tendsto (fun x => (f x)⁻¹ • g x) l (nhds 0))
-- Mathlib.RingTheory.Coalgebra.TensorProduct
Coalgebra.TensorProduct.map_toLinearMap : ∀ {R : Type u_5} {S : Type u_6} {M : Type u_7} {N : Type u_8} {P : Type u_9} {Q : Type u_10} [inst : CommSemiring R]
  [inst_1 : CommSemiring S] [inst_2 : Algebra R S] [inst_3 : AddCommMonoid M] [inst_4 : AddCommMonoid N]
  [inst_5 : AddCommMonoid P] [inst_6 : AddCommMonoid Q] [inst_7 : Module R M] [inst_8 : Module R N]
  [inst_9 : Module R P] [inst_10 : Module R Q] [inst_11 : Module S M] [inst_12 : IsScalarTower R S M]
  [inst_13 : Coalgebra S M] [inst_14 : Module S N] [inst_15 : IsScalarTower R S N] [inst_16 : Coalgebra S N]
  [inst_17 : Coalgebra R P] [inst_18 : Coalgebra R Q] (f : M →ₗc[S] N) (g : P →ₗc[R] Q),
  ↑(Coalgebra.TensorProduct.map f g) = TensorProduct.AlgebraTensorModule.map ↑f ↑g
-- Mathlib.Order.Filter.Interval
Filter.HasBasis.tendstoIxxClass : ∀ {α : Type u_1} {ι : Type u_3} {p : ι → Prop} {s : ι → Set α} {l : Filter α},
  l.HasBasis p s →
    ∀ {Ixx : α → α → Set α}, (∀ (i : ι), p i → ∀ x ∈ s i, ∀ y ∈ s i, Ixx x y ⊆ s i) → Filter.TendstoIxxClass Ixx l l
-- Mathlib.RingTheory.Valuation.Basic
Valuation.val_eq_one_iff : ∀ {K : Type u_1} [inst : DivisionRing K] {Γ₀ : Type u_4} [inst_1 : LinearOrderedCommGroupWithZero Γ₀]
  (v : Valuation K Γ₀) {x : K}, v x = 1 ↔ v x⁻¹ = 1
-- Mathlib.CategoryTheory.Pi.Monoidal
CategoryTheory.Pi.monoidalPi_ε : ∀ {I : Type w₁} {C : I → Type u₁} [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)]
  [inst_1 : (i : I) → CategoryTheory.MonoidalCategory (C i)] {D : I → Type u₂}
  [inst_2 : (i : I) → CategoryTheory.Category.{v₂, u₂} (D i)] [inst_3 : (i : I) → CategoryTheory.MonoidalCategory (D i)]
  (F : (i : I) → CategoryTheory.Functor (D i) (C i)) [inst_4 : (i : I) → (F i).Monoidal] (i : I),
  CategoryTheory.Functor.LaxMonoidal.ε (CategoryTheory.Functor.pi F) i = CategoryTheory.Functor.LaxMonoidal.ε (F i)
-- Mathlib.AlgebraicGeometry.Noetherian
AlgebraicGeometry.noetherianSpace_of_isAffine : ∀ {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsAffine X] [IsNoetherianRing ↑(X.presheaf.obj (Opposite.op ⊤))],
  TopologicalSpace.NoetherianSpace ↥X
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.coe_tendsto : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α} {f : α → β} {lb : Filter β}, (↑f).Tendsto lb ↔ Filter.Tendsto f l lb
-- Init.Data.Array.Int
Array.mul_length_le_sum_of_min?_eq_some_int : ∀ {x : ℤ} {xs : Array ℤ}, xs.min? = some x → x * ↑xs.size ≤ xs.sum
-- Mathlib.RingTheory.DividedPowers.RatAlgebra
DividedPowers.OfInvertibleFactorial.dividedPowers.congr_simp : ∀ {A : Type u_1} [inst : CommSemiring A] {I : Ideal A} [inst_1 : DecidablePred fun x => x ∈ I] {n n_1 : ℕ}
  (e_n : n = n_1) (hn_fac : IsUnit ↑(n - 1).factorial) (hnI : I ^ n = 0),
  DividedPowers.OfInvertibleFactorial.dividedPowers hn_fac hnI = DividedPowers.OfInvertibleFactorial.dividedPowers ⋯ ⋯
-- Mathlib.Data.ENat.Lattice
ENat.add_sSup : ∀ {s : Set ℕ∞} {a : ℕ∞}, s.Nonempty → a + sSup s = ⨆ b ∈ s, a + b
-- Mathlib.Algebra.Homology.BifunctorHomotopy
HomologicalComplex.mapBifunctorMapHomotopy.ιMapBifunctor_hom₁_assoc : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} {I₁ : Type u_4} {I₂ : Type u_5} {J : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} D] [inst_3 : CategoryTheory.Preadditive C₁]
  [inst_4 : CategoryTheory.Preadditive C₂] [inst_5 : CategoryTheory.Preadditive D] {c₁ : ComplexShape I₁}
  {c₂ : ComplexShape I₂} {K₁ L₁ : HomologicalComplex C₁ c₁} {f₁ f₁' : K₁ ⟶ L₁} (h₁ : Homotopy f₁ f₁')
  {K₂ L₂ : HomologicalComplex C₂ c₂} (f₂ : K₂ ⟶ L₂) (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
  [inst_6 : F.Additive] [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).Additive] (c : ComplexShape J) [inst_8 : DecidableEq J]
  [inst_9 : TotalComplexShape c₁ c₂ c] [inst_10 : K₁.HasMapBifunctor K₂ F c] [inst_11 : L₁.HasMapBifunctor L₂ F c]
  (i₁ i₁' : I₁) (i₂ : I₂) (j j' : J) (h : c₁.π c₂ c (i₁', i₂) = j),
  c₁.prev i₁' = i₁ →
    ∀ {Z : D} (h_1 : (L₁.mapBifunctor L₂ F c).X j' ⟶ Z),
      CategoryTheory.CategoryStruct.comp (K₁.ιMapBifunctor K₂ F c i₁' i₂ j h)
          (CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctorMapHomotopy.hom₁ h₁ f₂ F c j j') h_1) =
        CategoryTheory.CategoryStruct.comp
          (c₁.ε₁ c₂ c (i₁, i₂) •
            CategoryTheory.CategoryStruct.comp ((F.map (h₁.hom i₁' i₁)).app (K₂.X i₂))
              (CategoryTheory.CategoryStruct.comp ((F.obj (L₁.X i₁)).map (f₂.f i₂))
                (L₁.ιMapBifunctorOrZero L₂ F c i₁ i₂ j')))
          h_1
-- Mathlib.AlgebraicGeometry.Morphisms.Basic
AlgebraicGeometry.IsZariskiLocalAtTarget.of_isPullback : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsZariskiLocalAtTarget P]
  {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} {UX UY : AlgebraicGeometry.Scheme} {iY : UY ⟶ Y}
  [AlgebraicGeometry.IsOpenImmersion iY] {iX : UX ⟶ X} {f' : UX ⟶ UY}, CategoryTheory.IsPullback iX f' f iY → P f → P f'
-- Mathlib.Order.Bounds.Basic
top_mem_upperBounds : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : OrderTop α] (s : Set α), ⊤ ∈ upperBounds s
-- Mathlib.Data.Fintype.BigOperators
/-- Sum over a sigma type equals the repeated sum.

This is a version of `Finset.sum_sigma` specialized to the case of summation over `Finset.univ`.  -/
Fintype.sum_sigma : ∀ {ι : Type u_9} {α : ι → Type u_7} {M : Type u_8} [inst : Fintype ι] [inst_1 : (i : ι) → Fintype (α i)]
  [inst_2 : AddCommMonoid M] (f : Sigma α → M), ∑ x, f x = ∑ x, ∑ y, f ⟨x, y⟩
-- Mathlib.GroupTheory.GroupAction.Primitive
AddAction.IsQuasiPreprimitive.mk : ∀ {G : Type u_1} {X : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G X]
  [toIsPretransitive : AddAction.IsPretransitive G X],
  (∀ {N : AddSubgroup G} [N.Normal], AddAction.fixedPoints (↥N) X ≠ Set.univ → AddAction.IsPretransitive (↥N) X) →
    AddAction.IsQuasiPreprimitive G X
-- Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
MvPolynomial.coeff_weightedHomogeneousComponent : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] {σ : Type u_3} [inst_1 : AddCommMonoid M] {w : σ → M} (n : M)
  (φ : MvPolynomial σ R) [inst_2 : DecidableEq M] (d : σ →₀ ℕ),
  MvPolynomial.coeff d ((MvPolynomial.weightedHomogeneousComponent w n) φ) =
    if (Finsupp.weight w) d = n then MvPolynomial.coeff d φ else 0
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.hasNatSMul : {α : Type u_1} → {β : Type u_2} → [inst : MeasurableSpace α] → [AddMonoid β] → SMul ℕ (MeasureTheory.SimpleFunc α β)
-- Mathlib.CategoryTheory.Sites.Grothendieck
/-- Construct a complete lattice from the `Inf`, but make the trivial and discrete topologies
definitionally equal to the bottom and top respectively.
 -/
CategoryTheory.GrothendieckTopology.instCompleteLattice : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → CompleteLattice (CategoryTheory.GrothendieckTopology C)
-- Mathlib.Algebra.Group.Units.Defs
AddUnits.instAdd.eq_1 : ∀ {α : Type u} [inst : AddMonoid α],
  AddUnits.instAdd = { add := fun u₁ u₂ => { val := ↑u₁ + ↑u₂, neg := u₂.neg + u₁.neg, val_neg := ⋯, neg_val := ⋯ } }
-- Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Oplax
CategoryTheory.Oplax.OplaxTrans.OplaxFunctor.bicategory_whiskerLeft_as_app : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] (C : Type u₂) [inst_1 : CategoryTheory.Bicategory C]
  {x x_1 x_2 : CategoryTheory.OplaxFunctor B C} (η : x ⟶ x_1) (x_3 x_4 : x_1 ⟶ x_2) (Γ : x_3 ⟶ x_4) (a : B),
  (CategoryTheory.Bicategory.whiskerLeft η Γ).as.app a = CategoryTheory.Bicategory.whiskerLeft (η.app a) (Γ.as.app a)
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.Mor₂.isoHom.sizeOf_spec : ∀ (e : Lean.Expr) (isoLift : Mathlib.Tactic.BicategoryLike.IsoLift) (iso : Mathlib.Tactic.BicategoryLike.Mor₂Iso),
  sizeOf (Mathlib.Tactic.BicategoryLike.Mor₂.isoHom e isoLift iso) = 1 + sizeOf e + sizeOf isoLift + sizeOf iso
-- Lean.Parser.Basic
_private.Lean.Parser.Basic.0.Lean.Parser.tokenFnAux : Lean.Parser.ParserFn
-- Mathlib.Topology.Algebra.UniformField
completableTopField_of_complete : ∀ (L : Type u_3) [inst : Field L] [inst_1 : UniformSpace L] [IsTopologicalDivisionRing L] [T0Space L] [CompleteSpace L],
  CompletableTopField L
-- Mathlib.Topology.Order.LeftRightLim
Monotone.tendsto_rightLim : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : ConditionallyCompleteLinearOrder β]
  [inst_2 : TopologicalSpace β] [OrderTopology β] {f : α → β},
  Monotone f →
    ∀ [inst_4 : TopologicalSpace α] [OrderTopology α] (x : α),
      Filter.Tendsto f (nhdsWithin x (Set.Ioi x)) (nhds (Function.rightLim f x))