mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.infinite_mul_of_not_infinitesimal_infinite : ∀ {x y : ℝ*}, ¬x.Infinitesimal → y.Infinite → (x * y).Infinite
-- Init.Data.List.Basic
List.eraseDupsBy.loop : {α : Type u_1} → (α → α → Bool) → List α → List α → List α
-- Mathlib.Algebra.Polynomial.EraseLead
Polynomial.eraseLead_natDegree_lt : ∀ {R : Type u_1} [inst : Semiring R] {f : Polynomial R}, 2 ≤ f.support.card → f.eraseLead.natDegree < f.natDegree
-- Lean.Compiler.IR.Basic
Lean.IR.Alt.ctor : Lean.IR.CtorInfo → Lean.IR.FnBody → Lean.IR.Alt
-- Mathlib.Topology.FiberBundle.Constructions
Bundle.Trivial.homeomorphProd_symm_apply_proj : ∀ (B : Type u_1) (F : Type u_2) [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] (x : B × F),
  ((Bundle.Trivial.homeomorphProd B F).symm x).proj = x.1
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.multicospanShape_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreOneHypercover S) (j : E.I₁'),
  E.multicospanShape.fst j = j.fst.1
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.neighborSet.memDecidable : {V : Type u} → (G : SimpleGraph V) → (v : V) → [DecidableRel G.Adj] → DecidablePred fun x => x ∈ G.neighborSet v
-- Lean.Data.JsonRpc
Lean.JsonRpc.MessageMetaData.request.injEq : ∀ (id : Lean.JsonRpc.RequestID) (method : String) (id_1 : Lean.JsonRpc.RequestID) (method_1 : String),
  (Lean.JsonRpc.MessageMetaData.request id method = Lean.JsonRpc.MessageMetaData.request id_1 method_1) =
    (id = id_1 ∧ method = method_1)
-- Mathlib.Algebra.Order.Ring.WithTop
_private.Mathlib.Algebra.Order.Ring.WithTop.0.WithTop.instMonoidWithZero.match_1.splitter : {α : Type u_1} →
  (motive : WithTop α → ℕ → Sort u_2) →
    (a : WithTop α) →
      (n : ℕ) →
        ((a : α) → (n : ℕ) → motive (some a) n) → (Unit → motive none 0) → ((_n : ℕ) → motive none _n.succ) → motive a n
-- Lean.Parser.Syntax
Lean.Parser.Command.catBehaviorSymbol.formatter : Lean.PrettyPrinter.Formatter
-- Lean.Elab.Do.Basic
/-- Constructs `m α` from `α`.  -/
Lean.Elab.Do.mkMonadApp : Lean.Expr → Lean.Elab.Do.DoElabM Lean.Expr
-- Mathlib.Topology.VectorBundle.Riemannian
/-- Given two continuous maps into the same fibers of a continuous Riemannian bundle,
their inner product is continuous.  -/
Continuous.inner_bundle : ∀ {B : Type u_1} [inst : TopologicalSpace B] {F : Type u_2} [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace ℝ F]
  {E : B → Type u_3} [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_4 : (x : B) → NormedAddCommGroup (E x)]
  [inst_5 : (x : B) → InnerProductSpace ℝ (E x)] [inst_6 : FiberBundle F E] [inst_7 : VectorBundle ℝ F E] {M : Type u_4}
  [inst_8 : TopologicalSpace M] [h : IsContinuousRiemannianBundle F E] {b : M → B} {v w : (x : M) → E (b x)},
  (Continuous fun m => ⟨b m, v m⟩) → (Continuous fun m => ⟨b m, w m⟩) → Continuous fun b_1 => inner ℝ (v b_1) (w b_1)
-- Mathlib.Data.Matrix.Reflection
_private.Mathlib.Data.Matrix.Reflection.0.Matrix.Forall.match_1.eq_2 : ∀ {α : Type u_1} (motive : (x x_1 : ℕ) → (Matrix (Fin x) (Fin x_1) α → Prop) → Sort u_2) (n x : ℕ)
  (P : Matrix (Fin (n + 1)) (Fin x) α → Prop) (h_1 : (x : ℕ) → (P : Matrix (Fin 0) (Fin x) α → Prop) → motive 0 x P)
  (h_2 : (n x : ℕ) → (P : Matrix (Fin (n + 1)) (Fin x) α → Prop) → motive n.succ x P),
  (match n.succ, x, P with
    | 0, x, P => h_1 x P
    | n.succ, x, P => h_2 n x P) =
    h_2 n x P
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
SchwartzMap.smulLeftCLM_sub : ∀ {𝕜 : Type u_2} {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NontriviallyNormedField 𝕜]
  [inst_5 : NormedAlgebra ℝ 𝕜] [inst_6 : NormedSpace 𝕜 F] {g₁ g₂ : E → 𝕜},
  Function.HasTemperateGrowth g₁ →
    Function.HasTemperateGrowth g₂ →
      SchwartzMap.smulLeftCLM F (g₁ - g₂) = SchwartzMap.smulLeftCLM F g₁ - SchwartzMap.smulLeftCLM F g₂
-- Mathlib.Algebra.Group.Subsemigroup.Defs
AddSubsemigroup.copy_eq : ∀ {M : Type u_1} [inst : Add M] {S : AddSubsemigroup M} {s : Set M} (hs : s = ↑S), S.copy s hs = S
-- Batteries.Data.Array.Scan
List.toArray_scanr : ∀ {α : Type u_1} {β : Type u_2} {init : β} {f : α → β → β} {as : List α},
  (List.scanr f init as).toArray = Array.scanr f init as.toArray
-- Mathlib.GroupTheory.Congruence.Basic
/-- The additive congruence relation on an `AddMonoid` `M` from
an `AddSubmonoid` of `M × M` for which membership is an equivalence relation.  -/
AddCon.ofAddSubmonoid : {M : Type u_1} → [inst : AddZeroClass M] → (N : AddSubmonoid (M × M)) → (Equivalence fun x y => (x, y) ∈ N) → AddCon M
-- Mathlib.CategoryTheory.Bicategory.Functor.Prelax
/-- The prefunctor between the underlying quivers.  -/
CategoryTheory.PrelaxFunctorStruct.toPrefunctor : {B : Type u₁} →
  [inst : Quiver B] →
    [inst_1 : (a b : B) → Quiver (a ⟶ b)] →
      {C : Type u₂} →
        [inst_2 : Quiver C] → [inst_3 : (a b : C) → Quiver (a ⟶ b)] → CategoryTheory.PrelaxFunctorStruct B C → B ⥤q C
-- Std.Internal.Do.WP.Lemmas
Std.Internal.Do.WPMonad.wp_tryCatch_Except_apply_eq : ∀ {ε : Type u_1} {α : Type u_2} {post : α → Prop} {epost : EPost⟨ε → Prop⟩} (x : Except ε α) (h : ε → Except ε α),
  Std.Internal.Do.wp (MonadExceptOf.tryCatch x h) post epost =
    Std.Internal.Do.wp x post epost⟨fun e => Std.Internal.Do.wp (h e) post epost⟩
-- Mathlib.Topology.Maps.Basic
Topology.IsClosedEmbedding.of_comp : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {f : X → Y} {g : Y → Z} [inst : TopologicalSpace X]
  [inst_1 : TopologicalSpace Y] [inst_2 : TopologicalSpace Z],
  Topology.IsEmbedding g → Topology.IsClosedEmbedding (g ∘ f) → Topology.IsClosedEmbedding f
-- Mathlib.Algebra.Notation.Prod
Prod.mk_eq_zero : ∀ {M : Type u_3} {N : Type u_4} [inst : Zero M] [inst_1 : Zero N] {x : M} {y : N}, (x, y) = 0 ↔ x = 0 ∧ y = 0
-- Mathlib.RingTheory.RamificationInertia.Inertia
/-- Given a prime ideal `q` of an `R`-algebra `S`, the inertia degree of `q` over `R` is defined
to be the degree of the residue field of `q` over the residue field of its preimage `p` in `R`.

When `q` is not prime, we use a junk value of `0`.

This will eventually replace the existing definition of `Ideal.inertiaDeg'`.  -/
Ideal.inertiaDeg : {S : Type u_1} → [inst : CommRing S] → Ideal S → (R : Type u_2) → [inst_1 : CommRing R] → [Algebra R S] → ℕ
-- Mathlib.AlgebraicGeometry.Morphisms.Separated
/-- **Alias** of `AlgebraicGeometry.IsSeparated.isClosedImmersion_diagonal`.

---

A morphism is separated if the diagonal map is a closed immersion.  -/
AlgebraicGeometry.IsSeparated.diagonal_isClosedImmersion : ∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} [self : AlgebraicGeometry.IsSeparated f],
  AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Limits.pullback.diagonal f)
-- Mathlib.Analysis.Asymptotics.Lemmas
/-- **Alias** of the reverse direction of `Asymptotics.isLittleO_iff_tendsto`. -/
Asymptotics.isLittleO_of_tendsto : ∀ {α : Type u_1} {𝕜 : Type u_15} [inst : NormedDivisionRing 𝕜] {l : Filter α} {f g : α → 𝕜},
  (∀ (x : α), g x = 0 → f x = 0) → Filter.Tendsto (fun x => f x / g x) l (nhds 0) → f =o[l] g
-- Mathlib.Analysis.CStarAlgebra.Multiplier
DoubleCentralizer.neg_snd : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : NormedSpace 𝕜 A] [inst_3 : SMulCommClass 𝕜 A A] [inst_4 : IsScalarTower 𝕜 A A] (a : DoubleCentralizer 𝕜 A),
  (-a).toProd.2 = -a.toProd.2
-- Lean.Elab.Tactic.Config
_private.Lean.Elab.Tactic.Config.0.Lean.Elab.Tactic.checkConfigElab : Lean.Linter.MissingDocs.SimpleHandler
-- Mathlib.RingTheory.Spectrum.Maximal.Localization
/-- A ring homomorphism induces a homomorphism between the products of localizations at primes.  -/
PrimeSpectrum.mapPiLocalization : {R : Type u_1} →
  {S : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : CommSemiring S] → (R →+* S) → PrimeSpectrum.PiLocalization R →+* PrimeSpectrum.PiLocalization S
-- Lean.Meta.Tactic.Grind.Arith.Linear.LinearM
Lean.Meta.Grind.Arith.Linear.LinearM.Context.structId : Lean.Meta.Grind.Arith.Linear.LinearM.Context → ℕ
-- Mathlib.CategoryTheory.Monoidal.NaturalTransformation
CategoryTheory.Iso.instIsMonoidalInvFunctor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  {F₁ F₂ : CategoryTheory.Functor C D} [inst_4 : F₁.LaxMonoidal] [inst_5 : F₂.LaxMonoidal] (e : F₁ ≅ F₂)
  [CategoryTheory.NatTrans.IsMonoidal e.hom], CategoryTheory.NatTrans.IsMonoidal e.inv
-- Mathlib.AlgebraicTopology.ModelCategory.Instances
HomotopicalAlgebra.instCofibrationMapOfIsWeakFactorizationSystemCofibrationsTrivialFibrations : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C]
  [inst_2 : HomotopicalAlgebra.CategoryWithCofibrations C] [inst_3 : HomotopicalAlgebra.CategoryWithFibrations C]
  {J : Type u_1} {X Y : J → C} (f : (i : J) → X i ⟶ Y i) [inst_4 : CategoryTheory.Limits.HasCoproduct X]
  [inst_5 : CategoryTheory.Limits.HasCoproduct Y] [h : ∀ (i : J), HomotopicalAlgebra.Cofibration (f i)]
  [(HomotopicalAlgebra.cofibrations C).IsWeakFactorizationSystem (HomotopicalAlgebra.trivialFibrations C)],
  HomotopicalAlgebra.Cofibration (CategoryTheory.Limits.Sigma.map f)
-- Init.Data.String.Search
String.posOf : String → Char → String.Pos.Raw
-- Lean.Parser.Module.Syntax
Lean.Parser.Module.meta.formatter : Lean.PrettyPrinter.Formatter
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.ShiftRight
Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftRight.twoPowShift : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {w : ℕ} →
        (aig : Std.Sat.AIG α) →
          Std.Tactic.BVDecide.BVExpr.bitblast.TwoPowShiftTarget aig w → Std.Sat.AIG.RefVecEntry α w
-- Mathlib.RingTheory.LinearDisjoint
Subalgebra.linearDisjoint_iff : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] (A B : Subalgebra R S),
  A.LinearDisjoint B ↔ (Subalgebra.toSubmodule A).LinearDisjoint (Subalgebra.toSubmodule B)
-- Mathlib.CategoryTheory.Enriched.EnrichedCat
CategoryTheory.EnrichedCat.rightUnitor_inv_out_app : ∀ {V : Type v} [inst : CategoryTheory.Category.{w, v} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u}
  [inst_2 : CategoryTheory.EnrichedCategory V C] {D : Type u₁} [inst_3 : CategoryTheory.EnrichedCategory V D]
  (F : CategoryTheory.EnrichedFunctor V C D) (X : CategoryTheory.ForgetEnrichment V C),
  (CategoryTheory.EnrichedCat.rightUnitor F).inv.out.app X =
    CategoryTheory.CategoryStruct.id
      (CategoryTheory.ForgetEnrichment.of V (F.obj (CategoryTheory.ForgetEnrichment.to V X)))
-- Mathlib.Algebra.Group.Basic
inv_eq_one : ∀ {α : Type u_1} [inst : DivisionMonoid α] {a : α}, a⁻¹ = 1 ↔ a = 1
-- Mathlib.Data.Set.Card
Set.encard_tsub_one_le_encard_sdiff_singleton : ∀ {α : Type u_1} (s : Set α) (x : α), s.encard - 1 ≤ (s \ {x}).encard
-- Mathlib.CategoryTheory.Sigma.Basic
CategoryTheory.Sigma.instFullSigmaIncl : ∀ {I : Type w₁} {C : I → Type u₁} [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] (i : I),
  (CategoryTheory.Sigma.incl i).Full
-- Mathlib.Tactic.Sat.FromLRAT
Mathlib.Tactic.Sat.LRATStep.add.inj : ∀ {id : ℕ} {lits proof : Array ℤ} {id_1 : ℕ} {lits_1 proof_1 : Array ℤ},
  Mathlib.Tactic.Sat.LRATStep.add id lits proof = Mathlib.Tactic.Sat.LRATStep.add id_1 lits_1 proof_1 →
    id = id_1 ∧ lits = lits_1 ∧ proof = proof_1
-- Mathlib.CategoryTheory.Bicategory.Span.Basic
CategoryTheory.Span.wl : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {Wₗ Wᵣ : CategoryTheory.MorphismProperty C} {c c' : C}
  (self : CategoryTheory.Span Wₗ Wᵣ c c'), Wₗ self.l
-- Lean.Linter.Deprecated
Lean.MessageData.isDeprecationWarning : Lean.MessageData → Bool
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.IsAddMonHom.addMonoidHom_apply : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {M N : C} [inst_2 : CategoryTheory.AddMonObj M] [inst_3 : CategoryTheory.AddMonObj N] (f : M ⟶ N)
  [inst_4 : CategoryTheory.IsAddMonHom f] (X : C) (x : X ⟶ M),
  (CategoryTheory.IsAddMonHom.addMonoidHom f X) x = CategoryTheory.CategoryStruct.comp x f
-- Mathlib.Order.Hom.BoundedLattice
SupBotHom.instSemilatticeSup.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : Max α] [inst_1 : Bot α] [inst_2 : SemilatticeSup β] [inst_3 : OrderBot β],
  SupBotHom.instSemilatticeSup = Function.Injective.semilatticeSup DFunLike.coe ⋯ ⋯ ⋯ ⋯
-- Mathlib.Topology.VectorBundle.Basic
Bundle.Trivialization.coe_coordChangeL : ∀ {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [inst : Semiring R] [inst_1 : TopologicalSpace F]
  [inst_2 : TopologicalSpace B] [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_4 : AddCommMonoid F]
  [inst_5 : Module R F] [inst_6 : (x : B) → AddCommMonoid (E x)] [inst_7 : (x : B) → Module R (E x)]
  (e e' : Bundle.Trivialization F Bundle.TotalSpace.proj) [inst_8 : Bundle.Trivialization.IsLinear R e]
  [inst_9 : Bundle.Trivialization.IsLinear R e'] {b : B} (hb : b ∈ e.baseSet ∩ e'.baseSet),
  ⇑(Bundle.Trivialization.coordChangeL R e e' b) =
    ⇑((Bundle.Trivialization.linearEquivAt R e b ⋯).symm ≪≫ₗ Bundle.Trivialization.linearEquivAt R e' b ⋯)
-- Mathlib.Order.Filter.Map
Filter.bind_map : ∀ {γ : Type u_3} {α : Type u_6} {β : Type u_7} (m : α → β) (f : Filter α) (g : β → Filter γ),
  (Filter.map m f).bind g = f.bind (g ∘ m)
-- Mathlib.AlgebraicTopology.AlternatingFaceMapComplex
CochainComplex.of.d.congr_simp : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  {α : Type u_2} [inst_2 : AddRightCancelSemigroup α] [inst_3 : One α] {inst_4 : DecidableEq α} [inst_5 : DecidableEq α]
  (X : α → V) (d d_1 : (n : α) → X n ⟶ X (n + 1)),
  d = d_1 → ∀ (i j : α), CochainComplex.of.d X d i j = CochainComplex.of.d X d_1 i j
-- Mathlib.Order.RelIso.Basic
RelIso.relHomCongr_apply_apply : ∀ {α₁ : Type u_5} {β₁ : Type u_6} {α₂ : Type u_7} {β₂ : Type u_8} {r₁ : α₁ → α₁ → Prop} {s₁ : β₁ → β₁ → Prop}
  {r₂ : α₂ → α₂ → Prop} {s₂ : β₂ → β₂ → Prop} (e₁ : r₁ ≃r r₂) (e₂ : s₁ ≃r s₂) (f₁ : r₁ →r s₁) (x : α₂),
  ((e₁.relHomCongr e₂) f₁) x = e₂ (f₁ (e₁.symm x))
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.norm_comm : ∀ {k : Type u} [inst : Semiring k] {G : Type v} [inst_1 : Group G] [inst_2 : Fintype G] {A B : Rep.{u_1, u, v} k G}
  (f : A ⟶ B), CategoryTheory.CategoryStruct.comp f B.norm = CategoryTheory.CategoryStruct.comp A.norm f
-- Mathlib.Algebra.Category.CommAlgCat.FiniteType
/-- The category of finitely generated `R`-algebras.  -/
FGAlgCat : (R : Type u) → [CommRing R] → Type (max u (v + 1))
-- Mathlib.Topology.Constructions
Finset.continuous_restrict₂ : ∀ {ι : Type u_5} {A : ι → Type u_6} [T : (i : ι) → TopologicalSpace (A i)] {s t : Finset ι} (hst : s ⊆ t),
  Continuous (Finset.restrict₂ hst)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.forM_eq_forMUncurried : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m' : Type w → Type w'} {β : Type v} {m : Std.DHashMap α fun x => β}
  [inst : Monad m'] [LawfulMonad m'] {f : α → β → m' PUnit.{w + 1}},
  Std.DHashMap.forM f m = Std.DHashMap.Const.forMUncurried (fun a => f a.1 a.2) m
-- Mathlib.LinearAlgebra.Matrix.Bilinear
/-- A version of `LinearMap.mulLeft` for matrix multiplication.  -/
mulLeftLinearMap : {l : Type u_1} →
  {m : Type u_2} →
    (n : Type u_3) →
      (R : Type u_5) →
        {A : Type u_6} →
          [Fintype m] →
            [inst : Semiring R] →
              [inst_1 : NonUnitalNonAssocSemiring A] →
                [inst_2 : Module R A] → [SMulCommClass R A A] → Matrix l m A → Matrix m n A →ₗ[R] Matrix l n A
-- Mathlib.Order.BoundedOrder.Basic
OrderDual.toDual_top : ∀ (α : Type u) [inst : Top α], OrderDual.toDual ⊤ = ⊥
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.norm_def : ∀ {d : ℤ} (n : ℤ√d), n.norm = n.re * n.re - d * n.im * n.im
-- Std.Time.Date.Unit.Weekday
_private.Std.Time.Date.Unit.Weekday.0.Std.Time.instReprWeekday.repr.match_1.eq_4 : ∀ (motive : Std.Time.Weekday → Sort u_1) (h_1 : Unit → motive Std.Time.Weekday.monday)
  (h_2 : Unit → motive Std.Time.Weekday.tuesday) (h_3 : Unit → motive Std.Time.Weekday.wednesday)
  (h_4 : Unit → motive Std.Time.Weekday.thursday) (h_5 : Unit → motive Std.Time.Weekday.friday)
  (h_6 : Unit → motive Std.Time.Weekday.saturday) (h_7 : Unit → motive Std.Time.Weekday.sunday),
  (match Std.Time.Weekday.thursday with
    | Std.Time.Weekday.monday => h_1 ()
    | Std.Time.Weekday.tuesday => h_2 ()
    | Std.Time.Weekday.wednesday => h_3 ()
    | Std.Time.Weekday.thursday => h_4 ()
    | Std.Time.Weekday.friday => h_5 ()
    | Std.Time.Weekday.saturday => h_6 ()
    | Std.Time.Weekday.sunday => h_7 ()) =
    h_4 ()
-- Mathlib.Order.Filter.Map
Filter.NeBot.of_map : ∀ {α : Type u_1} {β : Type u_2} {f : Filter α} {m : α → β}, (Filter.map m f).NeBot → f.NeBot
-- Mathlib.Algebra.Star.StarAlgHom
NonUnitalStarAlgHom.snd_prod : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [inst : Monoid R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : DistribMulAction R A] [inst_3 : Star A] [inst_4 : NonUnitalNonAssocSemiring B]
  [inst_5 : DistribMulAction R B] [inst_6 : Star B] [inst_7 : NonUnitalNonAssocSemiring C]
  [inst_8 : DistribMulAction R C] [inst_9 : Star C] (f : A →⋆ₙₐ[R] B) (g : A →⋆ₙₐ[R] C),
  (NonUnitalStarAlgHom.snd R B C).comp (f.prod g) = g
-- Mathlib.Order.OmegaCompletePartialOrder
OmegaCompletePartialOrder.ContinuousHom.congr_arg : ∀ {α : Type u_2} {β : Type u_3} [inst : OmegaCompletePartialOrder α] [inst_1 : OmegaCompletePartialOrder β] (f : α →𝒄 β)
  {x y : α}, x = y → f x = f y
-- Mathlib.Data.Vector3
Vector3.insert_fz : ∀ {α : Type u_1} {n : ℕ} (a : α) (v : Vector3 α n), Vector3.insert a v Fin2.fz = Vector3.cons a v
-- Mathlib.LinearAlgebra.Matrix.Symmetric
/-- A version of `Matrix.ext_iff` that unfolds the `Matrix.transpose`.  -/
Matrix.IsSymm.ext_iff : ∀ {α : Type u_1} {n : Type u_3} {A : Matrix n n α}, A.IsSymm ↔ ∀ (i j : n), A j i = A i j
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.instReprArgSpec.repr.match_1.eq_4 : ∀ (motive : Lean.Doc.ArgSpec✝ → Sort u_1) (a : Lean.Name) (a_1 : Bool)
  (h_1 : (a : Lean.Name) → (a_2 : Lean.Expr) → motive (Lean.Doc.ArgSpec.positional✝ a a_2))
  (h_2 : (a : Lean.Name) → (a_2 a_3 : Lean.Expr) → motive (Lean.Doc.ArgSpec.named✝ a a_2 a_3))
  (h_3 : (a : Lean.Name) → (a_2 : Lean.Expr) → motive (Lean.Doc.ArgSpec.many✝ a a_2))
  (h_4 : (a : Lean.Name) → (a_2 : Bool) → motive (Lean.Doc.ArgSpec.flag✝ a a_2)),
  (match Lean.Doc.ArgSpec.flag✝ a a_1 with
    | Lean.Doc.ArgSpec.positional✝ a a_2 => h_1 a a_2
    | Lean.Doc.ArgSpec.named✝ a a_2 a_3 => h_2 a a_2 a_3
    | Lean.Doc.ArgSpec.many✝ a a_2 => h_3 a a_2
    | Lean.Doc.ArgSpec.flag✝ a a_2 => h_4 a a_2) =
    h_4 a a_1
-- Mathlib.Analysis.Normed.Unbundled.SpectralNorm
/-- If `f` is a nonarchimedean, power-multiplicative `K`-algebra norm on `L`, then the spectral
value of a polynomial `p : K[X]` that decomposes into linear factors in `L` is equal to the
maximum of the norms of the roots. See [S. Bosch, U. Güntzer, R. Remmert, *Non-Archimedean Analysis*
(Proposition 3.1.2/1(2))][bosch-guntzer-remmert].  -/
max_norm_root_eq_spectralValue : ∀ {K : Type u_2} [inst : NormedField K] {L : Type u_3} [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : DecidableEq L] {f : AlgebraNorm K L},
  IsPowMul ⇑f →
    IsNonarchimedean ⇑f →
      f 1 = 1 →
        ∀ (p : Polynomial K) (s : Multiset L),
          (Polynomial.mapAlg K L) p = (Multiset.map (fun a => Polynomial.X - Polynomial.C a) s).prod →
            (⨆ x, if x ∈ s then f x else 0) = spectralValue p
-- Mathlib.Combinatorics.Additive.ETransform
Finset.addETransformRight.fst_add_snd_subset : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : AddGroup α] (e : α) (x : Finset α × Finset α),
  (Finset.addETransformRight e x).1 + (Finset.addETransformRight e x).2 ⊆ x.1 + x.2
-- Mathlib.RingTheory.Coalgebra.Equiv
CoalgEquiv.coe_coe : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid A]
  [inst_2 : AddCommMonoid B] [inst_3 : Module R A] [inst_4 : Module R B] [inst_5 : CoalgebraStruct R A]
  [inst_6 : CoalgebraStruct R B] (e : A ≃ₗc[R] B), ⇑↑e = ⇑e
-- Mathlib.Analysis.LocallyConvex.AbsConvex
/-- **Alias** of `balancedHull_convexHull_subset_absConvexHull`.

---

In general, equality doesn't hold here - e.g. consider `s := {(-1, 1), (1, 1)}` in `ℝ²`.  -/
balancedHull_convexHull_subseteq_absConvexHull : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] {s : Set E}, balancedHull 𝕜 ((convexHull 𝕜) s) ⊆ (absConvexHull 𝕜) s
-- Mathlib.Data.Nat.Factorization.Root
Nat.floorRoot_pow_dvd : ∀ {a n : ℕ}, n.floorRoot a ^ n ∣ a
-- Mathlib.AlgebraicGeometry.AffineTransitionLimit
/-- (Implementation) An affine open cover refining `𝒰D₀`. See the section docstring.  -/
AlgebraicGeometry.ExistsHomHomCompEqCompAux.𝒰D : {I : Type u} →
  [inst : CategoryTheory.Category.{u, u} I] →
    {S X : AlgebraicGeometry.Scheme} →
      {D : CategoryTheory.Functor I AlgebraicGeometry.Scheme} →
        {t : D ⟶ (CategoryTheory.Functor.const I).obj S} →
          {f : X ⟶ S} →
            [inst_1 : ∀ (i : I), CompactSpace ↥(D.obj i)] →
              [inst_2 : CategoryTheory.IsCofiltered I] →
                [inst_3 : ∀ {i j : I} (f : i ⟶ j), AlgebraicGeometry.IsAffineHom (D.map f)] →
                  (A : AlgebraicGeometry.ExistsHomHomCompEqCompAux D t f) → (D.obj A.i').OpenCover
-- Lean.Expr
/-- A set of unique free variable identifiers implemented using hashtables.
Hashtables are faster than red-black trees if they are used linearly.
They are not persistent data-structures.  -/
Lean.FVarIdHashSet : Type
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.max?_eq_some_max : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {he : t.isEmpty = false},
  t.max? = some (t.max he)
-- Init.Data.Array.Lemmas
Array.eq_empty_of_map_eq_empty : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {xs : Array α}, Array.map f xs = #[] → xs = #[]
-- Init.Data.Vector.Algebra
Vector.instIntModule : {α : Type u_1} → {n : ℕ} → [Lean.Grind.IntModule α] → Lean.Grind.IntModule (Vector α n)
-- Mathlib.Algebra.FiniteSupport.Basic
Function.HasFiniteMulSupport.sup : ∀ {α : Type u_1} {M : Type u_2} [inst : One M] [inst_1 : SemilatticeSup M] {f g : α → M},
  Function.HasFiniteMulSupport f → Function.HasFiniteMulSupport g → Function.HasFiniteMulSupport fun a => f a ⊔ g a
-- Mathlib.Analysis.RCLike.ContinuousMap
ContinuousMap.realToRCLike_strictMono : ∀ (X : Type u_1) (𝕜 : Type u_2) [inst : TopologicalSpace X] [inst_1 : RCLike 𝕜],
  StrictMono (ContinuousMap.realToRCLike 𝕜)
-- Mathlib.Data.ENNReal.Basic
ENNReal.top_ne_zero : ⊤ ≠ 0
-- Mathlib.Data.Finsupp.NeLocus
Finsupp.neLocus_comm : ∀ {α : Type u_1} {N : Type u_3} [inst : DecidableEq α] [inst_1 : DecidableEq N] [inst_2 : Zero N] (f g : α →₀ N),
  f.neLocus g = g.neLocus f
-- Mathlib.NumberTheory.ZetaValues
_private.Mathlib.NumberTheory.ZetaValues.0.term𝕌 : Lean.ParserDescr
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.isoImage_ι_inv_morphismRestrict_homOfLE_assoc : ∀ {X : AlgebraicGeometry.Scheme} {U V : X.Opens} (e : U ≤ V) (W : TopologicalSpace.Opens ↥↑V)
  {Z : AlgebraicGeometry.Scheme} (h : ↑W ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (AlgebraicGeometry.Scheme.Hom.isoImage U.ι ((TopologicalSpace.Opens.map (X.homOfLE e).base).obj W)).inv
      (CategoryTheory.CategoryStruct.comp (X.homOfLE e ∣_ W) h) =
    CategoryTheory.CategoryStruct.comp (X.homOfLE ⋯)
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.isoImage V.ι W).inv h)
-- Lean.Meta.DiscrTree.Main
_private.Lean.Meta.DiscrTree.Main.0.Lean.Meta.DiscrTree.getAllValuesForKey.go : {α : Type} → Lean.Meta.DiscrTree.Trie α → Array α → Array α
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.getUnsolvedGoals : Lean.Elab.Tactic.Grind.GrindTacticM (List Lean.Meta.Grind.Goal)