mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Sites.Point.OfIsCofiltered
/-- For a point constructed using `Point.ofIsCofiltered` and a functor `p : N ⥤ C`,
the fiber of a presheaf can be computed as a colimit indexed by `N`.  -/
CategoryTheory.GrothendieckTopology.Point.isColimitPresheafFiberOfIsCofilteredCocone : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C] →
      {N : Type u'} →
        [inst_2 : CategoryTheory.Category.{v', u'} N] →
          (p : CategoryTheory.Functor N C) →
            [inst_3 : CategoryTheory.InitiallySmall N] →
              {J : CategoryTheory.GrothendieckTopology C} →
                [inst_4 : CategoryTheory.IsCofiltered N] →
                  (hp :
                      ∀ ⦃X : C⦄,
                        ∀ R ∈ J X,
                          ∀ ⦃U : N⦄ (f : p.obj U ⟶ X),
                            ∃ Y g,
                              ∃ (_ : R.arrows g),
                                ∃ V q a,
                                  CategoryTheory.CategoryStruct.comp a g =
                                    CategoryTheory.CategoryStruct.comp (p.map q) f) →
                    {A : Type u''} →
                      [inst_5 : CategoryTheory.Category.{v'', u''} A] →
                        [inst_6 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v'', u''} A] →
                          (P : CategoryTheory.Functor Cᵒᵖ A) →
                            CategoryTheory.Limits.IsColimit
                              (CategoryTheory.GrothendieckTopology.Point.presheafFiberOfIsCofilteredCocone p hp P)
-- Mathlib.Algebra.Free
FreeSemigroup.length_mul : ∀ {α : Type u} (x y : FreeSemigroup α), (x * y).length = x.length + y.length
-- Mathlib.Algebra.Group.ForwardDiff
fwdDiff_aux.shiftₗ.eq_1 : ∀ (M : Type u_1) (G : Type u_2) [inst : AddCommMonoid M] [inst_1 : AddCommGroup G] (h : M),
  fwdDiff_aux.shiftₗ M G h = fwdDiff_aux.fwdDiffₗ M G h + 1
-- Init.Data.UInt.Bitwise
UInt16.ofNat_or : ∀ (a b : ℕ), UInt16.ofNat (a ||| b) = UInt16.ofNat a ||| UInt16.ofNat b
-- Mathlib.Geometry.Manifold.GroupLieAlgebra
instLieRingGroupLieAlgebra.eq_1 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4}
  [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : Group G]
  [inst_7 : LieGroup I (minSmoothness 𝕜 3) G] [inst_8 : CompleteSpace E],
  instLieRingGroupLieAlgebra =
    { toAddCommGroup := instAddCommGroupTangentSpace I 1, toBracket := instBracketGroupLieAlgebra, add_lie := ⋯,
      lie_add := ⋯, lie_self := ⋯, leibniz_lie := ⋯ }
-- Mathlib.Probability.ProductMeasure
/-- Consider a family of probability measures. You can take their products for any finite
subfamily. This gives an additive content on the measurable cylinders.  -/
MeasureTheory.piContent : {ι : Type u_1} →
  {X : ι → Type u_2} →
    {mX : (i : ι) → MeasurableSpace (X i)} →
      (μ : (i : ι) → MeasureTheory.Measure (X i)) →
        [hμ : ∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)] →
          MeasureTheory.AddContent ENNReal (MeasureTheory.measurableCylinders X)
-- Mathlib.CategoryTheory.MorphismProperty.Descent
CategoryTheory.MorphismProperty.of_isPushout_of_codescendsAlong : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P Q : CategoryTheory.MorphismProperty C} {Z X Y A : C}
  {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ A} {inr : Y ⟶ A} [P.CodescendsAlong Q],
  CategoryTheory.IsPushout f g inl inr → Q f → P inl → P g
-- Mathlib.Order.Interval.Set.WithBotTop
WithBot.Iio_coe : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, Set.Iio ↑a = WithBot.some '' Set.Iio a ∪ {⊥}
-- Mathlib.CategoryTheory.Action.Limits
CategoryTheory.Functor.mapAction_linear : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {W : Type u_3}
  [inst_1 : CategoryTheory.Category.{v_2, u_3} W] (F : CategoryTheory.Functor V W) (G : Type u_4) [inst_2 : Monoid G]
  [inst_3 : CategoryTheory.Preadditive V] [inst_4 : CategoryTheory.Preadditive W] {R : Type u_5} [inst_5 : Semiring R]
  [inst_6 : CategoryTheory.Linear R V] [inst_7 : CategoryTheory.Linear R W] [CategoryTheory.Functor.Linear R F],
  CategoryTheory.Functor.Linear R (F.mapAction G)
-- Mathlib.Analysis.Calculus.ImplicitFunction.ProdDomain
HasStrictFDerivAt.tendsto_implicitFunctionOfProdDomain : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E₁ : Type u_2} [inst_1 : NormedAddCommGroup E₁]
  [inst_2 : NormedSpace 𝕜 E₁] [inst_3 : CompleteSpace E₁] {E₂ : Type u_3} [inst_4 : NormedAddCommGroup E₂]
  [inst_5 : NormedSpace 𝕜 E₂] [inst_6 : CompleteSpace E₂] {F : Type u_4} [inst_7 : NormedAddCommGroup F]
  [inst_8 : NormedSpace 𝕜 F] [inst_9 : CompleteSpace F] {u : E₁ × E₂} {f : E₁ × E₂ → F} {f'u : E₁ × E₂ →L[𝕜] F}
  (dfu : HasStrictFDerivAt f f'u u) (if₂u : (f'u ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂).IsInvertible),
  Filter.Tendsto (dfu.implicitFunctionOfProdDomain if₂u) (nhds u.1) (nhds u.2)
-- Mathlib.Combinatorics.Colex
Finset.Colex.toColex_univ : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : Fintype α], toColex Finset.univ = ⊤
-- Aesop.Tree.UnsafeQueue
Aesop.UnsafeQueueEntry.postponedSafeRule.injEq : ∀ (r r_1 : Aesop.PostponedSafeRule),
  (Aesop.UnsafeQueueEntry.postponedSafeRule r = Aesop.UnsafeQueueEntry.postponedSafeRule r_1) = (r = r_1)
-- Init.Data.Range.Polymorphic.PRange
/-- The upper bound of the range. `upper` is not included in the range.
   -/
Std.Roo.upper : {α : Type u} → Std.Roo α → α
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Char
Char.reduceLT : Lean.Meta.Simp.Simproc
-- Mathlib.Topology.Algebra.MulAction
ContinuousWithinAt.vadd : ∀ {M : Type u_1} {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace X]
  [inst_2 : TopologicalSpace Y] [inst_3 : VAdd M X] [ContinuousVAdd M X] {f : Y → M} {g : Y → X} {b : Y} {s : Set Y},
  ContinuousWithinAt f s b → ContinuousWithinAt g s b → ContinuousWithinAt (f +ᵥ g) s b
-- Std.Net.Addr
Std.Net.instInhabitedMACAddr : Inhabited Std.Net.MACAddr
-- Mathlib.Analysis.Normed.Group.InfiniteSum
Summable.of_nnnorm_bounded : ∀ {ι : Type u_1} {E : Type u_3} [inst : SeminormedAddCommGroup E] [CompleteSpace E] {f : ι → E} {g : ι → NNReal},
  Summable g → (∀ (i : ι), ‖f i‖₊ ≤ g i) → Summable f
-- Qq.Macro
/-- `a =QL b` says that the levels `a` and `b` are definitionally equal.  -/
Qq.«term_=QL_» : Lean.ParserDescr
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal
PresheafOfModules.rightUnitor_hom_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat}
  (M₁ : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))) (X : Cᵒᵖ),
  (CategoryTheory.MonoidalCategoryStruct.rightUnitor M₁).hom.app X =
    (CategoryTheory.MonoidalCategoryStruct.rightUnitor (M₁.obj X)).hom
-- Mathlib.Geometry.Manifold.HasGroupoid
/-- Given a charted space admitting a structure groupoid, the maximal atlas associated to this
structure groupoid is the set of all charts that are compatible with the atlas, i.e., such
that changing coordinates with an atlas member gives an element of the groupoid.  -/
StructureGroupoid.maximalAtlas : {H : Type u} →
  (M : Type u_2) →
    [inst : TopologicalSpace H] →
      [inst_1 : TopologicalSpace M] → [ChartedSpace H M] → StructureGroupoid H → Set (OpenPartialHomeomorph M H)
-- Init.Data.UInt.Lemmas
UInt64.ofBitVec_add : ∀ (a b : BitVec 64), { toBitVec := a + b } = { toBitVec := a } + { toBitVec := b }
-- Batteries.Control.LawfulMonadState
/-- The namespaced `MonadStateOf.modifyGet` is equal to the `MonadState` provided `modifyGet`.  -/
monadStateOf_modifyGet_eq_modifyGet : ∀ {σ : Type u_1} {m : Type u_1 → Type u_2} {α : Type u_1} [inst : MonadStateOf σ m] (f : σ → α × σ),
  MonadStateOf.modifyGet f = modifyGet f
-- Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
SSet.S.map_toNπ_op_apply : ∀ {X : SSet} (x : X.S), (CategoryTheory.ConcreteCategory.hom (X.map x.toNπ.op)) x.toN.simplex = x.simplex
-- Std.Data.DTreeMap.Internal.Balanced
Std.DTreeMap.Internal.Impl.BalancedAtRoot.symm : ∀ {l r : ℕ}, Std.DTreeMap.Internal.Impl.BalancedAtRoot l r → Std.DTreeMap.Internal.Impl.BalancedAtRoot r l
-- Init.Core
/-- This encodes either `pure (a : α)` or `return (a : α)`:
* `pure (a : α) s` means that the block exited normally with return value `a`
* `return (b : β) s` means that the block exited via a `return b` early-exit command

The one that is actually encoded depends on the context of use.  -/
DoResultSBC.pureReturn : {α σ : Type u} → α → σ → DoResultSBC α σ
-- Mathlib.Algebra.Group.AddChar
AddChar.toAddMonoidHomEquiv_zero : ∀ {A : Type u_1} {M : Type u_3} [inst : AddMonoid A] [inst_1 : Monoid M], AddChar.toAddMonoidHomEquiv 0 = 0
-- Mathlib.Analysis.SpecialFunctions.Pow.Complex
/-- A version of `Complex.cpow_nat_mul` with RHS that matches `Complex.cpow_mul`.

The assumptions on the arguments are needed
because the equality fails, e.g., for `x = -I`, `n = 2`, `y = 1/2`.  -/
Complex.cpow_nat_mul' : ∀ {x : ℂ} {n : ℕ}, -Real.pi < ↑n * x.arg → ↑n * x.arg ≤ Real.pi → ∀ (y : ℂ), x ^ (↑n * y) = (x ^ n) ^ y
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.insertC.eq_1 : ∀ (k : ℤ) (m : Lean.Grind.CommRing.Mon) (p : Lean.Grind.CommRing.Poly) (c : ℕ),
  Lean.Grind.CommRing.Poly.insertC k m p c =
    bif k % ↑c == 0 then p else Lean.Grind.CommRing.Poly.insertC.go m c (k % ↑c) p
-- Mathlib.Data.Set.Image
Set.range_some_inter_none : ∀ (α : Type u_5), Set.range some ∩ {none} = ∅
-- Mathlib.Data.Matrix.Basic
Matrix.algebraMap_matrix_apply : ∀ {n : Type u_3} {R : Type u_7} {α : Type u_11} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommSemiring R]
  [inst_3 : Semiring α] [inst_4 : Algebra R α] {r : R} {i j : n},
  (algebraMap R (Matrix n n α)) r i j = if i = j then (algebraMap R α) r else 0
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get?_union!_of_contains_eq_false_left : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α],
  m₁.WF → m₂.WF → ∀ {k : α}, Std.DTreeMap.Internal.Impl.contains k m₁ = false → (m₁.union! m₂).get? k = m₂.get? k
-- Mathlib.Algebra.Quandle
/-- Inverse Action of a Rack  -/
Quandles.«term_◃⁻¹_» : Lean.TrailingParserDescr
-- Mathlib.Topology.Algebra.Group.ClosedSubgroup
AddSubgroup.isOpen_of_isClosed_of_finiteIndex : ∀ {G : Type u} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [SeparatelyContinuousAdd G] (H : AddSubgroup G)
  [H.FiniteIndex], IsClosed ↑H → IsOpen ↑H
-- Mathlib.Analysis.Meromorphic.NormalForm
/-- If `f` is any function and `g` is analytic without zero at `z₀`, then `f` is meromorphic in
normal form at `z₀` iff `f * g` is meromorphic in normal form at `z₀`.  -/
meromorphicNFAt_mul_iff_left : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {g : 𝕜 → 𝕜} {x : 𝕜} {f : 𝕜 → 𝕜},
  AnalyticAt 𝕜 g x → g x ≠ 0 → (MeromorphicNFAt (f * g) x ↔ MeromorphicNFAt f x)
-- Mathlib.CategoryTheory.Limits.Shapes.Diagonal
CategoryTheory.Limits.pushout.instIsSplitEpiCodiagonal : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : C} (f : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasPushout f f],
  CategoryTheory.IsSplitEpi (CategoryTheory.Limits.pushout.codiagonal f)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.size_insertManyIfNewUnit_list_le : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeMap α Unit cmp} [Std.TransCmp cmp] {l : List α},
  (t.insertManyIfNewUnit l).size ≤ t.size + l.length
-- Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
hasSum_jacobiTheta₂_term_fderiv : ∀ (z : ℂ) {τ : ℂ}, 0 < τ.im → HasSum (fun n => jacobiTheta₂_term_fderiv n z τ) (jacobiTheta₂_fderiv z τ)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.instHashablePower.hash : Lean.Grind.CommRing.Power → UInt64
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.isNone_minKey?_eq_isEmpty : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp],
  t.minKey?.isNone = t.isEmpty
-- Mathlib.AlgebraicGeometry.Birational.RationalMap
AlgebraicGeometry.Scheme.PartialMap.mk.congr_simp : ∀ {X Y : AlgebraicGeometry.Scheme} (domain : X.Opens) (dense_domain : Dense ↑domain) (hom hom_1 : ↑domain ⟶ Y),
  hom = hom_1 →
    { domain := domain, dense_domain := dense_domain, hom := hom } =
      { domain := domain, dense_domain := dense_domain, hom := hom_1 }
-- Std.Data.Internal.List.Associative
Std.Internal.List.reverse_keys : ∀ {α : Type u} {β : α → Type v} {l : List ((a : α) × β a)},
  (Std.Internal.List.keys l).reverse = Std.Internal.List.keys l.reverse
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Cochain.single_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  (K L : CochainComplex C ℤ) (p q n : ℤ), CochainComplex.HomComplex.Cochain.single 0 n = 0
-- Mathlib.Algebra.Group.TypeTags.Basic
isAddRightRegular_ofMul : ∀ {α : Type u} [inst : Monoid α] {a : α}, IsAddRightRegular (Additive.ofMul a) ↔ IsRightRegular a
-- Mathlib.Order.Defs.Unbundled
Std.Total.trichotomous : ∀ {α : Sort u_1} (r : α → α → Prop) [Std.Total r], Std.Trichotomous r
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.cooper : Lean.Meta.Grind.Arith.Cutsat.CooperSplit → Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Pred
String.Slice.endsWith_bool_iff_get : ∀ {p : Char → Bool} {s : String.Slice},
  s.endsWith p = true ↔ ∃ (h : s.endPos ≠ s.startPos), p ((s.endPos.prev h).get ⋯) = true
-- Mathlib.Analysis.Meromorphic.NormalForm
/-- If a function is meromorphic in normal form on `U`, then its divisor is
non-negative iff it is analytic.
 -/
MeromorphicNFOn.divisor_nonneg_iff_analyticOnNhd : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {U : Set 𝕜},
  MeromorphicNFOn f U → (0 ≤ MeromorphicOn.divisor f U ↔ AnalyticOnNhd 𝕜 f U)
-- Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling
SimpleGraph.TopEdgeLabeling.labelGraph_adj : ∀ {V : Type u_1} {K : Type u_3} {C : SimpleGraph.TopEdgeLabeling V K} {k : K} (x y : V),
  (SimpleGraph.EdgeLabeling.labelGraph C k).Adj x y ↔ ∃ (H : x ≠ y), SimpleGraph.EdgeLabeling.get C x y H = k
-- Mathlib.Combinatorics.SimpleGraph.Basic
/-- We can enumerate simple graphs by enumerating all functions `V → V → Bool`
and filtering on whether they are symmetric and irreflexive.  -/
instFintypeSimpleGraphOfDecidableEq : {V : Type u} → [Fintype V] → [DecidableEq V] → Fintype (SimpleGraph V)
-- Mathlib.Probability.Kernel.Composition.Prod
ProbabilityTheory.Kernel.lintegral_prod_symm : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsSFiniteKernel κ]
  (η : ProbabilityTheory.Kernel α γ) [ProbabilityTheory.IsSFiniteKernel η] (a : α) {g : β × γ → ENNReal},
  Measurable g → ∫⁻ (c : β × γ), g c ∂(κ.prod η) a = ∫⁻ (c : γ), ∫⁻ (b : β), g (b, c) ∂κ a ∂η a
-- Mathlib.Data.Setoid.Partition
/-- Equivalence classes partition the type.  -/
Setoid.classes_eqv_classes : ∀ {α : Type u_1} {r : Setoid α} (a : α), ∃! b, b ∈ r.classes ∧ a ∈ b
-- Mathlib.Data.Nat.Cast.SetInterval
Nat.image_cast_int_Ioi : ∀ (a : ℕ), Nat.cast '' Set.Ioi a = Set.Ioi ↑a
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.List.filterMap.match_1.splitter : {β : Type u_1} →
  (motive : Option β → Sort u_2) → (x : Option β) → (Unit → motive none) → ((b : β) → motive (some b)) → motive x
-- Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells
HomotopicalAlgebra.AttachCells.reindex_m : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {α : Type t} {A B : α → C} {g : (a : α) → A a ⟶ B a}
  {X₁ X₂ : C} {f : X₁ ⟶ X₂} (c : HomotopicalAlgebra.AttachCells g f) {ι' : Type w'} (e : ι' ≃ c.ι),
  (c.reindex e).m = c.m
-- Mathlib.Tactic.NormNum.Result
Mathlib.Meta.NormNum.Result'.isBool.inj : ∀ {val : Bool} {proof : Lean.Expr} {val_1 : Bool} {proof_1 : Lean.Expr},
  Mathlib.Meta.NormNum.Result'.isBool val proof = Mathlib.Meta.NormNum.Result'.isBool val_1 proof_1 →
    val = val_1 ∧ proof = proof_1
-- Mathlib.Logic.Function.Basic
Function.instIsStrictOrderOnFun : ∀ {α : Sort u_1} {β : Sort u_2} (r : β → β → Prop) (f : α → β) [IsStrictOrder β r], IsStrictOrder α (Function.onFun r f)
-- Mathlib.Analysis.Real.Cardinality
Cardinal.cantorFunction_succ : ∀ {c : ℝ} (f : ℕ → Bool),
  0 ≤ c →
    c < 1 → Cardinal.cantorFunction c f = (bif f 0 then 1 else 0) + c * Cardinal.cantorFunction c fun n => f (n + 1)
-- Mathlib.RingTheory.IsAdjoinRoot
/-- If `α` generates `S` as an algebra, then `S` is given by adjoining a root of `minpoly R α`.  -/
IsAdjoinRoot.mkOfAdjoinEqTop : {R : Type u} →
  {S : Type v} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          [IsDomain R] →
            [IsDomain S] →
              [Module.IsTorsionFree R S] →
                [IsIntegrallyClosed R] → {α : S} → IsIntegral R α → R[α] = ⊤ → IsAdjoinRoot S (minpoly R α)
-- Mathlib.Order.Filter.AtTopBot.Tendsto
Filter.Tendsto.eventually_ne_atTop : ∀ {α : Type u_3} {β : Type u_4} [inst : Preorder β] [NoTopOrder β] {f : α → β} {l : Filter α},
  Filter.Tendsto f l Filter.atTop → ∀ (c : β), ∀ᶠ (x : α) in l, f x ≠ c
-- Lean.Message
Lean.BaseMessage.severity : {α : Type u} → Lean.BaseMessage α → Lean.MessageSeverity
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing
/-- The ancestrality relation on type (II) simplices.  -/
SSet.Subcomplex.Pairing.AncestralRel : {X : SSet} → {A : X.Subcomplex} → (P : A.Pairing) → ↑P.II → ↑P.II → Prop
-- Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory
/-- This lemma allows the computation of the connecting homomorphism
`D.δ` when `D : SnakeInput C` and `C` is a concrete category.  -/
CategoryTheory.ShortComplex.SnakeInput.δ_apply' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type v}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC]
  [inst_3 : CategoryTheory.HasForget₂ C Ab] [inst_4 : CategoryTheory.Abelian C]
  [inst_5 : (CategoryTheory.forget₂ C Ab).Additive] [(CategoryTheory.forget₂ C Ab).PreservesHomology]
  (D : CategoryTheory.ShortComplex.SnakeInput C) (x₃ : ↑((CategoryTheory.forget₂ C Ab).obj D.L₀.X₃))
  (x₂ : ↑((CategoryTheory.forget₂ C Ab).obj D.L₁.X₂)) (x₁ : ↑((CategoryTheory.forget₂ C Ab).obj D.L₂.X₁)),
  (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.forget₂ C Ab).map D.L₁.g)) x₂ =
      (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.forget₂ C Ab).map D.v₀₁.τ₃)) x₃ →
    (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.forget₂ C Ab).map D.L₂.f)) x₁ =
        (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.forget₂ C Ab).map D.v₁₂.τ₂)) x₂ →
      (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.forget₂ C Ab).map D.δ)) x₃ =
        (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.forget₂ C Ab).map D.v₂₃.τ₁)) x₁
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.foldl_eq_foldl_toList : ∀ {α : Type u} {δ : Type w} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} {f : δ → α → β → δ} {init : δ},
  Std.DTreeMap.Internal.Impl.foldl f init t =
    List.foldl (fun a b => f a b.1 b.2) init (Std.DTreeMap.Internal.Impl.Const.toList t)
-- Init.Data.Fin.Fold
Fin.foldrM_succ_last : ∀ {m : Type u_1 → Type u_2} {n : ℕ} {α : Type u_1} [inst : Monad m] [LawfulMonad m] (f : Fin (n + 1) → α → m α),
  Fin.foldrM (n + 1) f = fun x => f (Fin.last n) x >>= Fin.foldrM n fun i => f i.castSucc
-- Mathlib.Data.Bool.Basic
Bool.ofNat_zero : Bool.ofNat 0 = false
-- Mathlib.FieldTheory.SeparableClosure
/-- If `i` is an `F`-algebra isomorphism of `E` and `K`, then the image of `separableClosure F E`
under the map `i` is equal to `separableClosure F K`.  -/
separableClosure.map_eq_of_algEquiv : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {K : Type w} [inst_3 : Field K]
  [inst_4 : Algebra F K] (i : E ≃ₐ[F] K), IntermediateField.map (↑i) (separableClosure F E) = separableClosure F K
-- Mathlib.Topology.UniformSpace.Basic
instUniqueUniformSpaceOfSubsingleton : {α : Type ua} → [Subsingleton α] → Unique (UniformSpace α)
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.eLpNorm'_congr_norm_ae : ∀ {α : Type u_1} {F : Type u_5} {G : Type u_6} {m0 : MeasurableSpace α} {q : ℝ} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup F] [inst_1 : NormedAddCommGroup G] {f : α → F} {g : α → G},
  (∀ᵐ (x : α) ∂μ, ‖f x‖ = ‖g x‖) → MeasureTheory.eLpNorm' f q μ = MeasureTheory.eLpNorm' g q μ
-- Mathlib.Data.PNat.Defs
/-- We define `m / k` in the same way as for `ℕ` except that when `m = n * k` we take
`m / k = n - 1`. This ensures that `m = (m % k) + k * (m / k)` in all cases. Later we
define a function `div_exact` which gives the usual `m / k` in the case where `k` divides `m`.
 -/
PNat.div : ℕ+ → ℕ+ → ℕ
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
Convexity.StdSimplex.weights_duple : ∀ {R : Type u} [inst : PartialOrder R] [inst_1 : Semiring R] {M : Type u_9} [inst_2 : IsStrictOrderedRing R] (x y : M)
  {s t : R} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1),
  (Convexity.StdSimplex.duple x y hs ht h).weights = (fun₀ | x => s) + fun₀ | y => t
-- Mathlib.Analysis.Calculus.FDeriv.Prod
differentiableOn_fst : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  {s : Set (E × F)}, DifferentiableOn 𝕜 Prod.fst s
-- Mathlib.Tactic.FBinop
/-- Compute a minimal `SRec` for an expression tree.  -/
_private.Mathlib.Tactic.FBinop.0.FBinopElab.analyze : FBinopElab.Tree✝ → Option Lean.Expr → Lean.Elab.TermElabM FBinopElab.AnalyzeResult✝
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.foldr_eq_foldr_keys : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} {δ : Type w} {f : α → δ → δ}
  {init : δ}, Std.TreeMap.Raw.foldr (fun a x d => f a d) init t = List.foldr f init t.keys
-- Mathlib.Order.WithBot
WithBot.decidableLT.eq_1 : ∀ {α : Type u_1} [inst : LT α] [inst_1 : DecidableLT α] (x : WithBot α), x.decidableLT none = isFalse ⋯
-- Mathlib.AlgebraicGeometry.Gluing
/-- Given an open cover of `X`, and a morphism `𝒰.X x ⟶ Y` for each open subscheme in the cover,
such that these morphisms are compatible in the intersection (pullback), we may glue the morphisms
together into a morphism `X ⟶ Y`.

Note:
If `X` is exactly (defeq to) the gluing of `U i`, then using `Multicoequalizer.desc` suffices.
 -/
AlgebraicGeometry.Scheme.Cover.glueMorphisms : {X : AlgebraicGeometry.Scheme} →
  (𝒰 : X.OpenCover) →
    {Y : AlgebraicGeometry.Scheme} →
      (f : (x : 𝒰.I₀) → 𝒰.X x ⟶ Y) →
        (∀ (x y : 𝒰.I₀),
            CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (𝒰.f x) (𝒰.f y)) (f x) =
              CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (𝒰.f x) (𝒰.f y)) (f y)) →
          (X ⟶ Y)
-- Init.Data.Vector.Lemmas
Vector.exists_push : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α (n + 1)}, ∃ ys a, xs = ys.push a
-- Mathlib.RingTheory.Valuation.Integers
Valuation.Integers.isPrincipal_iff_exists_eq_setOfPred_valuation_le : ∀ {F : Type u} {Γ₀ : Type v} [inst : Field F] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] {v : Valuation F Γ₀}
  {O : Type w} [inst_2 : CommRing O] [inst_3 : Algebra O F],
  v.Integers O →
    ∀ {I : Ideal O}, Submodule.IsPrincipal I ↔ ∃ x, ↑I = {y | v ((algebraMap O F) y) ≤ v ((algebraMap O F) x)}
-- Mathlib.NumberTheory.ArithmeticFunction.Zeta
ArithmeticFunction.pmul_assoc : ∀ {R : Type u_1} [inst : SemigroupWithZero R] (f₁ f₂ f₃ : ArithmeticFunction R),
  (f₁.pmul f₂).pmul f₃ = f₁.pmul (f₂.pmul f₃)
-- Mathlib.Topology.Order.MonotoneConvergence
isLUB_of_tendsto_atBot : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : Preorder α] [OrderClosedTopology α]
  [inst_3 : Preorder β] [IsCodirectedOrder β] [Nonempty β] {f : β → α} {a : α},
  Antitone f → Filter.Tendsto f Filter.atBot (nhds a) → IsLUB (Set.range f) a