mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
/-- A bilinear map is called left-separating if
the only element that is left-orthogonal to every other element is `0`; i.e.,
for every nonzero `x` in `M₁`, there exists `y` in `M₂` with `B x y ≠ 0`.  -/
LinearMap.SeparatingLeft : {R : Type u_1} →
  {R₁ : Type u_2} →
    {R₂ : Type u_3} →
      {M : Type u_5} →
        {M₁ : Type u_6} →
          {M₂ : Type u_7} →
            [inst : CommSemiring R] →
              [inst_1 : AddCommMonoid M] →
                [inst_2 : Module R M] →
                  [inst_3 : CommSemiring R₁] →
                    [inst_4 : AddCommMonoid M₁] →
                      [inst_5 : Module R₁ M₁] →
                        [inst_6 : CommSemiring R₂] →
                          [inst_7 : AddCommMonoid M₂] →
                            [inst_8 : Module R₂ M₂] →
                              {I₁ : R₁ →+* R} → {I₂ : R₂ →+* R} → (M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M) → Prop
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.instInhabited : {K : Type u} → [inst : Field K] → Inhabited (ValuationSubring K)
-- Mathlib.RingTheory.Polynomial.HilbertPoly
Polynomial.preHilbertPoly.eq_1 : ∀ (F : Type u_1) [inst : Field F] (d k : ℕ),
  Polynomial.preHilbertPoly F d k = (↑d.factorial)⁻¹ • (ascPochhammer F d).comp (Polynomial.X - Polynomial.C ↑k + 1)
-- Init.Data.SInt.Lemmas
Int16.mul_sub : ∀ {a b c : Int16}, a * (b - c) = a * b - a * c
-- Mathlib.Topology.MetricSpace.Isometry
IsometryEquiv.coe_eq_toEquiv : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] (h : α ≃ᵢ β) (a : α),
  h a = h.toEquiv a
-- Mathlib.Order.LiminfLimsup
Filter.blimsup_monotone_filter : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {f g : Filter β} {p : β → Prop} {u : β → α},
  f ≤ g → Filter.blimsup u f p ≤ Filter.blimsup u g p
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.HomologyData.ofEpiOfIsIsoOfMono_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (h : S₁.HomologyData) [inst_2 : CategoryTheory.Epi φ.τ₁]
  [inst_3 : CategoryTheory.IsIso φ.τ₂] [inst_4 : CategoryTheory.Mono φ.τ₃],
  (CategoryTheory.ShortComplex.HomologyData.ofEpiOfIsIsoOfMono φ h).right =
    CategoryTheory.ShortComplex.RightHomologyData.ofEpiOfIsIsoOfMono φ h.right
-- Mathlib.Data.Int.CharZero
Function.mulSupport_intCast : ∀ {α : Type u_1} {β : Type u_2} [inst : AddGroupWithOne β] [CharZero β] {n : ℤ},
  n ≠ 1 → Function.mulSupport ↑n = Set.univ
-- Lean.BuiltinDocAttr
Lean.declareBuiltinDocStringAndRanges : Lean.Name → Lean.AttrM Unit
-- Mathlib.Order.Interval.Set.Fin
Fin.preimage_castLE_Ioi_castLE : ∀ {m n : ℕ} (i : Fin m) (h : m ≤ n), Fin.castLE h ⁻¹' Set.Ioi (Fin.castLE h i) = Set.Ioi i
-- Mathlib.Computability.Ackermann
/-- The Ackermann function is not primitive recursive.  -/
not_primrec₂_ack : ¬Primrec₂ ack
-- Mathlib.Order.Filter.AtTopBot.Tendsto
Filter.tendsto_atTop_mono : ∀ {α : Type u_3} {β : Type u_4} [inst : Preorder β] {l : Filter α} {f g : α → β},
  (∀ (n : α), f n ≤ g n) → Filter.Tendsto f l Filter.atTop → Filter.Tendsto g l Filter.atTop
-- Mathlib.Data.PSigma.Order
PSigma.Lex.denselyOrdered_of_noMaxOrder : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : Preorder ι] [inst_1 : (i : ι) → Preorder (α i)]
  [∀ (i : ι), DenselyOrdered (α i)] [∀ (i : ι), NoMaxOrder (α i)], DenselyOrdered (Σₗ' (i : ι), α i)
-- Mathlib.Algebra.Group.Prod
Prod.one_mk_mul_one_mk : ∀ {M : Type u_3} {N : Type u_4} [inst : MulOneClass M] [inst_1 : Mul N] (b₁ b₂ : N), (1, b₁) * (1, b₂) = (1, b₁ * b₂)
-- Mathlib.GroupTheory.Congruence.Defs
/-- Sometimes, an additive group is defined as a quotient of a monoid
by an additive congruence relation.
Usually, the inverse operation is defined as `Setoid.map f _` for some `f`.
This lemma allows to avoid code duplication in the definition of the inverse operation:
instead of proving both `∀ x y, c x y → c (f x) (f y)` (to define the operation)
and `∀ x, c (f x + x) 0` (to prove the group laws), one can only prove the latter.  -/
AddCon.map_of_add_left_rel_zero : ∀ {M : Type u_1} [inst : AddMonoid M] (c : AddCon M) (f : M → M),
  (∀ (x : M), c (f x + x) 0) → ∀ {x y : M}, c x y → c (f x) (f y)
-- Mathlib.Data.List.Cycle
/-- The lift of `list.map`.  -/
Cycle.map : {α : Type u_1} → {β : Type u_2} → (α → β) → Cycle α → Cycle β
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubAddAction.vadd_mem_iff' : ∀ {R : Type u} {M : Type v} [inst : AddMonoid R] [inst_1 : AddAction R M] (p : SubAddAction R M) {G : Type u_1}
  [inst_2 : AddGroup G] [inst_3 : VAdd G R] [inst_4 : AddAction G M] [VAddAssocClass G R M] (g : G) {x : M},
  g +ᵥ x ∈ p ↔ x ∈ p
-- Mathlib.Data.Int.Fib.Basic
Int.fib_of_nonneg : ∀ {n : ℤ}, 0 ≤ n → Int.fib n = ↑(Nat.fib n.toNat)
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.le_min : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k : α} {he : t ≠ ∅},
  (cmp k (t.min he)).isLE = true ↔ ∀ k' ∈ t, (cmp k k').isLE = true
-- Std.Data.HashMap.Lemmas
Std.HashMap.isEmpty_filterMap_eq_false_iff : ∀ {α : Type u} {β : Type v} {γ : Type w} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α]
  [LawfulHashable α] {f : α → β → Option γ},
  (Std.HashMap.filterMap f m).isEmpty = false ↔ ∃ k, ∃ (h : k ∈ m), (f (m.getKey k h) m[k]).isSome = true
-- Mathlib.CategoryTheory.Topos.Sheaf
/-- A construction of a subject classifier in a category of presheaves.  -/
CategoryTheory.Presheaf.classifier : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.Subobject.Classifier (CategoryTheory.Functor Cᵒᵖ (Type (max u v)))
-- Mathlib.Analysis.Convex.Basic
Convex.starConvex : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : SMul 𝕜 E] {s : Set E} {x : E}, Convex 𝕜 s → x ∈ s → StarConvex 𝕜 x s
-- Std.Http.Data.Body.Empty
/-- Empty bodies are always closed for reading.
 -/
Std.Http.Body.Empty.isClosed : Std.Http.Body.Empty → Std.Async.Async Bool
-- Std.Internal.Do.Order.Lemmas
/-- `⊤ ⊑ (P ⇨ Q)` iff `P ⊑ Q`.  -/
Std.Internal.Do.CompleteLattice.top_le_himp_iff : ∀ {l : Type u} [inst : Lean.Order.CompleteLattice l] [∀ (a : l), Lean.Order.PreservesSup (Lean.Order.meet a)] (P Q : l),
  Lean.Order.PartialOrder.rel Lean.Order.top (Lean.Order.himp P Q) ↔ Lean.Order.PartialOrder.rel P Q
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientGroup.map_mk : ∀ {G : Type u_1} {H : Type u_2} [inst : Group G] [inst_1 : Group H] (N : Subgroup G) [nN : N.Normal] (M : Subgroup H)
  [inst_2 : M.Normal] (f : G →* H) (h : N ≤ Subgroup.comap f M) (x : G), (QuotientGroup.map N M f h) ↑x = ↑(f x)
-- Init.Data.UInt.Lemmas
UInt32.mod_one : ∀ {a : UInt32}, a % 1 = 0
-- Mathlib.Topology.Sheaves.Stalks
TopCat.Presheaf.germ_res : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C] {X : TopCat}
  (F : TopCat.Presheaf C X) {U V : TopologicalSpace.Opens ↑X} (i : U ⟶ V) (x : ↑X) (hx : x ∈ U),
  CategoryTheory.CategoryStruct.comp (F.map i.op) (F.germ U x hx) = F.germ V x ⋯
-- Mathlib.MeasureTheory.Integral.Bochner.L1
/-- The Bochner integral is equal to a sum over any set that includes `f.range` (except `0`).  -/
MeasureTheory.SimpleFunc.integral_eq_sum_of_subset : ∀ {α : Type u_1} {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} [inst_2 : DecidablePred fun x => x ≠ 0] {f : MeasureTheory.SimpleFunc α F}
  {s : Finset F}, {x ∈ f.range | x ≠ 0} ⊆ s → MeasureTheory.SimpleFunc.integral μ f = ∑ x ∈ s, μ.real (⇑f ⁻¹' {x}) • x
-- Mathlib.Analysis.Calculus.ContDiff.Operations
/-- The product of two `C^n` functions at a point is `C^n` at this point.  -/
ContDiffAt.mul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : E} {n : WithTop ℕ∞} {𝔸 : Type u_3} [inst_3 : NormedRing 𝔸]
  [inst_4 : NormedAlgebra 𝕜 𝔸] {f g : E → 𝔸},
  ContDiffAt 𝕜 n f x → ContDiffAt 𝕜 n g x → ContDiffAt 𝕜 n (fun x => f x * g x) x
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.size_union_of_not_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → (∀ a ∈ t₁, a ∉ t₂) → (t₁ ∪ t₂).size = t₁.size + t₂.size
-- Lean.LoadDynlib
_private.Lean.LoadDynlib.0.Lean.DynlibImpl : NonemptyType
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- The underlying object of an object in `Under X`.  -/
CategoryTheory.Under.right : {T : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} T] → {X : T} → CategoryTheory.Under X → T
-- Mathlib.Topology.Algebra.Algebra
ContinuousAlgHom.coe_pow : ∀ {R : Type u_1} [inst : CommSemiring R] {A : Type u_2} [inst_1 : Semiring A] [inst_2 : TopologicalSpace A]
  [inst_3 : Algebra R A] (f : A →A[R] A) (n : ℕ), ⇑(f ^ n) = (⇑f)^[n]
-- Std.Data.Internal.List.Associative
Std.Internal.List.head?_keys : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [Std.LawfulEqOrd α] [inst_3 : LE α]
  [Std.LawfulOrderOrd α] [inst_5 : Min α] [Std.LawfulOrderLeftLeaningMin α] (l : List ((a : α) × β a)),
  List.Pairwise (fun a b => compare a.fst b.fst = Ordering.lt) l →
    (Std.Internal.List.keys l).head? = Std.Internal.List.minKey? l
-- Mathlib.Algebra.Star.MonoidHom
StarMulEquiv.invFun_eq_symm : ∀ {A : Type u_2} {B : Type u_3} [inst : Mul A] [inst_1 : Mul B] [inst_2 : Star A] [inst_3 : Star B] {e : A ≃⋆* B},
  EquivLike.inv e = ⇑e.symm
-- Std.Do.SPred.Laws
Std.Do.SPred.or_intro_l : ∀ {σs : List (Type u)} {P Q : Std.Do.SPred σs}, P ⊢ₛ P ∨ Q
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.biproduct.whiskerEquiv_hom : ∀ {J : Type w} {K : Type u_1} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {f : J → C} {g : K → C} (e : J ≃ K) (w : (j : J) → g (e j) ≅ f j)
  [inst_2 : CategoryTheory.Limits.HasBiproduct f] [inst_3 : CategoryTheory.Limits.HasBiproduct g],
  (CategoryTheory.Limits.biproduct.whiskerEquiv e w).hom =
    CategoryTheory.Limits.biproduct.desc fun j =>
      CategoryTheory.CategoryStruct.comp (w j).inv (CategoryTheory.Limits.biproduct.ι g (e j))
-- Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
/-- The constant functor returning a specific terminal object is indeed terminal.  -/
CategoryTheory.Functor.isTerminalConst : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {D : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        {X : D} →
          CategoryTheory.Limits.IsTerminal X → CategoryTheory.Limits.IsTerminal ((CategoryTheory.Functor.const C).obj X)
-- Mathlib.Analysis.Convex.Side
Wbtw.wSameSide₂₃ : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : CommRing R] [inst_1 : PartialOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P]
  {s : AffineSubspace R P} {x y z : P}, Wbtw R x y z → x ∈ s → s.WSameSide y z
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.spanningCoe.eq_1 : ∀ {V : Type u} {G : SimpleGraph V} (G' : G.Subgraph), G'.spanningCoe = { Adj := G'.Adj, symm := ⋯, loopless := ⋯ }
-- Mathlib.Analysis.Normed.Group.Real
norm_norm : ∀ {E : Type u_5} [inst : SeminormedAddCommGroup E] (x : E), ‖‖x‖‖ = ‖x‖
-- Mathlib.Analysis.Seminorm
Seminorm.closedBall_smul : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : SMul 𝕜 E]
  (p : Seminorm 𝕜 E) {c : NNReal}, 0 < c → ∀ (r : ℝ) (x : E), (c • p).closedBall x r = p.closedBall x (r / ↑c)
-- Mathlib.RingTheory.Flat.Basic
/-- Let `R` be a commutative semiring, let `C` be a commutative `R`-algebra, and let `A` be an
`R`-algebra. If `C ⊗[R] B` is reduced for all finitely generated subalgebras `B` of `A`, then
`C ⊗[R] A` is also reduced.  -/
IsReduced.tensorProduct_of_flat_of_forall_fg : ∀ {R : Type u_1} {C : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : CommSemiring C] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] [inst_4 : Algebra R C] [Module.Flat R C],
  (∀ (B : Subalgebra R A), B.FG → IsReduced (TensorProduct R C ↥B)) → IsReduced (TensorProduct R C A)
-- Mathlib.Algebra.Category.ModuleCat.Sheaf
/-- The bijection `(M₂ ⟶ N) ≃ (M₁ ⟶ N)` induced by a locally bijective morphism
`f : M₁ ⟶ M₂` of presheaves of modules, when `N` is a sheaf.  -/
PresheafOfModules.homEquivOfIsLocallyBijective : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {R : CategoryTheory.Functor Cᵒᵖ RingCat} →
        {M₁ M₂ : PresheafOfModules R} →
          (f : M₁ ⟶ M₂) →
            {N : PresheafOfModules R} →
              CategoryTheory.Presheaf.IsSheaf J N.presheaf →
                [J.WEqualsLocallyBijective AddCommGrpCat] →
                  [PresheafOfModules.IsLocallySurjective J f] →
                    [PresheafOfModules.IsLocallyInjective J f] → (M₂ ⟶ N) ≃ (M₁ ⟶ N)
-- Mathlib.Order.KrullDimension
Order.krullDim_nonpos_of_subsingleton : ∀ {α : Type u_1} [inst : Preorder α] [Subsingleton α], Order.krullDim α ≤ 0
-- Mathlib.GroupTheory.Coprod.Basic
/-- Isomorphism between `M ∗ PUnit` and `M`.  -/
MulEquiv.coprodPUnit : (M : Type u_1) → [inst : Monoid M] → Monoid.Coprod M PUnit.{u_4 + 1} ≃* M
-- Mathlib.Algebra.Group.Subgroup.Lattice
AddSubgroup.mem_sup_right : ∀ {G : Type u_1} [inst : AddGroup G] {S T : AddSubgroup G} {x : G}, x ∈ T → x ∈ S ⊔ T
-- Mathlib.Geometry.Euclidean.MongePoint
/-- Any three points in an orthocentric system span the same subspace
as the whole orthocentric system.  -/
EuclideanGeometry.affineSpan_of_orthocentricSystem : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : Set P},
  EuclideanGeometry.OrthocentricSystem s →
    ∀ {p : Fin 3 → P}, Set.range p ⊆ s → Function.Injective p → affineSpan ℝ (Set.range p) = affineSpan ℝ s
-- Mathlib.Geometry.Euclidean.Angle.Sphere
/-- Converse of "angles in same segment are equal" and "opposite angles of a cyclic quadrilateral
add to π", for oriented angles mod π.  -/
EuclideanGeometry.cospherical_of_two_zsmul_oangle_eq_of_not_collinear : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p₁ p₂ p₃ p₄ : P},
  2 • EuclideanGeometry.oangle p₁ p₂ p₄ = 2 • EuclideanGeometry.oangle p₁ p₃ p₄ →
    ¬Collinear ℝ {p₁, p₂, p₄} → EuclideanGeometry.Cospherical {p₁, p₂, p₃, p₄}
-- Mathlib.Algebra.Order.BigOperators.Expect
Finset.expect_le : ∀ {ι : Type u_1} {α : Type u_2} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α]
  [inst_3 : Module ℚ≥0 α] {s : Finset ι} {f : ι → α} [PosSMulMono ℚ≥0 α] {a : α},
  s.Nonempty → (∀ x ∈ s, f x ≤ a) → (s.expect fun i => f i) ≤ a
-- Mathlib.Algebra.Order.Nonneg.Field
Nonneg.instNNRatSMul : {α : Type u_1} → [inst : Semifield α] → [inst_1 : LinearOrder α] → [IsStrictOrderedRing α] → SMul ℚ≥0 { x // 0 ≤ x }
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.comp_sub : ∀ {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M : Type u_8} {N₂ : Type u_12} {N₃ : Type u_13} [inst : Semiring R₁]
  [inst_1 : Semiring R₂] [inst_2 : Semiring R₃] [inst_3 : AddCommMonoid M] [inst_4 : AddCommGroup N₂]
  [inst_5 : AddCommGroup N₃] [inst_6 : Module R₁ M] [inst_7 : Module R₂ N₂] [inst_8 : Module R₃ N₃] {σ₁₂ : R₁ →+* R₂}
  {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [inst_9 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (f g : M →ₛₗ[σ₁₂] N₂)
  (h : N₂ →ₛₗ[σ₂₃] N₃), h ∘ₛₗ (g - f) = h ∘ₛₗ g - h ∘ₛₗ f
-- Mathlib.NumberTheory.Cyclotomic.Discriminant
IsPrimitiveRoot.subOnePowerBasis.congr_simp : ∀ {n n_1 : ℕ} (e_n : n = n_1) [inst : NeZero n] (K : Type u) {L : Type v} [inst_1 : Field K] [inst_2 : CommRing L]
  [inst_3 : IsDomain L] [inst_4 : Algebra K L] [inst_5 : IsCyclotomicExtension {n} K L] {ζ ζ_1 : L} (e_ζ : ζ = ζ_1)
  (hζ : IsPrimitiveRoot ζ n), IsPrimitiveRoot.subOnePowerBasis K hζ = IsPrimitiveRoot.subOnePowerBasis K ⋯
-- Init.Grind.Config
/-- If `funext` is `true`, `grind` creates new opportunities for applying function extensionality by case-splitting
on equalities between lambda expressions.
 -/
Lean.Grind.Config.funext : Lean.Grind.Config → Bool
-- Init.Data.Int.DivMod.Lemmas
Int.fmod_add_cancel_right : ∀ {m n k : ℤ} (i : ℤ), (m + i).fmod n = (k + i).fmod n ↔ m.fmod n = k.fmod n
-- Mathlib.RingTheory.Polynomial.Basic
exists_C_coeff_notMem : ∀ {R : Type u} [inst : Semiring R] {f : Polynomial R} {I : Ideal (Polynomial R)},
  f ∉ I → ∃ i, Polynomial.C (f.coeff i) ∉ I
-- Mathlib.Algebra.Lie.Basis.Prod
/-- Simple Lie algebras with equivalent bases are equivalent.  -/
LieAlgebra.Basis.equivOfReindex : {ι₁ : Type u_1} →
  {ι₂ : Type u_2} →
    {L₁ : Type u_3} →
      {L₂ : Type u_4} →
        [inst : Finite ι₁] →
          [inst_1 : Finite ι₂] →
            (eι : ι₁ ≃ ι₂) →
              [inst_2 : LieRing L₁] →
                [inst_3 : LieRing L₂] →
                  {K : Type u_5} →
                    [inst_4 : Field K] →
                      [CharZero K] →
                        [inst_6 : LieAlgebra K L₁] →
                          [FiniteDimensional K L₁] →
                            {H₁ : LieSubalgebra K L₁} →
                              (b₁ : LieAlgebra.Basis ι₁ H₁) →
                                [inst_8 : LieAlgebra K L₂] →
                                  [FiniteDimensional K L₂] →
                                    {H₂ : LieSubalgebra K L₂} →
                                      (b₂ : LieAlgebra.Basis ι₂ H₂) →
                                        (Matrix.reindex eι eι) b₁.A = b₂.A →
                                          [LieAlgebra.IsSimple K L₁] → [LieAlgebra.IsSimple K L₂] → L₁ ≃ₗ⁅K⁆ L₂
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddMonoidHom.nsmul_apply : ∀ {A : Type u_2} {E : Type u_6} [inst : AddMonoid A] [inst_1 : TopologicalSpace A] [inst_2 : AddCommMonoid E]
  [inst_3 : TopologicalSpace E] [inst_4 : ContinuousAdd E] (f : A →ₜ+ E) (n : ℕ) (a : A), (n • f) a = n • f a
-- Batteries.Data.List.Perm
List.Perm.idxBij_symm_leftInverse_idxBij : ∀ {α : Type u_1} [inst : BEq α] [inst_1 : LawfulBEq α] {xs ys : List α} (h : xs.Perm ys),
  Function.LeftInverse ⋯.idxBij h.idxBij
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearMap.IsInvertible.inverse_apply_eq : ∀ {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace M₂]
  [inst_2 : Semiring R] [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : AddCommMonoid M₂]
  [inst_6 : Module R M₂] {f : M →L[R] M₂} {x : M} {y : M₂}, f.IsInvertible → (f.inverse y = x ↔ y = f x)
-- Mathlib.Algebra.Algebra.StrictPositivity
IsStrictlyPositive.smul : ∀ {A : Type u_1} {𝕜 : Type u_2} [inst : Ring A] [inst_1 : PartialOrder A] [inst_2 : Semifield 𝕜]
  [inst_3 : PartialOrder 𝕜] [inst_4 : Algebra 𝕜 A] [PosSMulMono 𝕜 A] {c : 𝕜},
  0 < c → ∀ {a : A}, IsStrictlyPositive a → IsStrictlyPositive (c • a)
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.toVal_inv : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] [inst_1 : DivisionRing R]
  (v : Valuation R Γ₀) (x : R), WithVal.toVal v x⁻¹ = (WithVal.toVal v x)⁻¹
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.addY_of_Z_eq_zero_right : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} [NoZeroDivisors R] {P Q : Fin 3 → R},
  W'.Equation Q → Q 2 = 0 → W'.addY P Q = -(Q 1 ^ 2 * P 2) * P 1
-- Lean.Elab.PreDefinition.TerminationHint
/-- Takes apart a `Termination.suffix` syntax object  -/
Lean.Elab.elabTerminationHints : {m : Type → Type} →
  [Monad m] → [Lean.MonadError m] → Lean.TSyntax `Lean.Parser.Termination.suffix → m Lean.Elab.TerminationHints
-- Mathlib.CategoryTheory.Filtered.Small
_private.Mathlib.CategoryTheory.Filtered.Small.0.CategoryTheory.IsCofiltered.CofilteredClosureSmall.bundledAbstractCofilteredClosure.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.IsCofilteredOrEmpty C] {α : Type w}
  (f f_1 : α → C),
  f = f_1 →
    ∀ (a a_1 : ℕ),
      a = a_1 →
        CategoryTheory.IsCofiltered.CofilteredClosureSmall.bundledAbstractCofilteredClosure✝ f a =
          CategoryTheory.IsCofiltered.CofilteredClosureSmall.bundledAbstractCofilteredClosure✝ f_1 a_1
-- Mathlib.Algebra.Order.Group.Abs
abs_abs_sub_abs_le_abs_sub : ∀ {G : Type u_1} [inst : AddCommGroup G] [inst_1 : LinearOrder G] [IsOrderedAddMonoid G] (a b : G),
  ||a| - |b|| ≤ |a - b|
-- Init.Data.List.Basic
List.instMembership : {α : Type u} → Membership α (List α)
-- Mathlib.Topology.Order.Basic
instOrderTopologyOrderDual : ∀ {α : Type u} [ts : TopologicalSpace α] [inst : Preorder α] [t : OrderTopology α], OrderTopology αᵒᵈ
-- Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
LinearIsometryEquiv.coe_toMeasurableEquiv : ∀ {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F]
  [inst_2 : NormedAddCommGroup E] [inst_3 : InnerProductSpace ℝ E] [inst_4 : MeasurableSpace E] [inst_5 : BorelSpace E]
  [inst_6 : MeasurableSpace F] [inst_7 : BorelSpace F] (f : E ≃ₗᵢ[ℝ] F), ⇑f.toMeasurableEquiv = ⇑f
-- Mathlib.LinearAlgebra.AffineSpace.Pointwise
/-- The multiplicative action on an affine subspace corresponding to applying the action to every
element.

This is available as an instance in the `Pointwise` locale.

TODO: generalize to include `SMul (P ≃ᵃ[k] P) (AffineSubspace k P)`, which acts on `P` with a
`VAdd` version of a `DistribMulAction`.  -/
AffineSubspace.pointwiseSMul : {M : Type u_1} →
  {k : Type u_2} →
    {V : Type u_3} →
      [inst : Ring k] →
        [inst_1 : AddCommGroup V] →
          [inst_2 : Module k V] → [inst_3 : DistribSMul M V] → [SMulCommClass M k V] → SMul M (AffineSubspace k V)
-- Mathlib.Algebra.Module.LinearMap.Defs
IsLinearMap.map_sub : ∀ {R : Type u_1} {M : Type u_8} {M₂ : Type u_10} [inst : Semiring R] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup M₂] [inst_3 : Module R M] [inst_4 : Module R M₂] {f : M → M₂},
  IsLinearMap R f → ∀ (x y : M), f (x - y) = f x - f y
-- Mathlib.FieldTheory.KummerExtension
irreducible_X_pow_sub_C_of_root_adjoin_eq_top : ∀ {K : Type u} [inst : Field K] {L : Type u_1} [inst_1 : Field L] [inst_2 : Algebra K L] [FiniteDimensional K L] {a : K}
  {α : L},
  α ^ Module.finrank K L = (algebraMap K L) a →
    K⟮α⟯ = ⊤ → Irreducible (Polynomial.X ^ Module.finrank K L - Polynomial.C a)
-- Lean.Meta.Tactic.Grind.EMatchTheorem
Lean.Meta.Grind.SymbolPriorityEntry.mk.sizeOf_spec : ∀ (declName : Lean.Name) (prio : ℕ), sizeOf { declName := declName, prio := prio } = 1 + sizeOf declName + sizeOf prio
-- Mathlib.Computability.TuringMachine.ToPartrec
/-- Pop a value from the stack and place the result in local store.  -/
Turing.PartrecToTM2.pop' : Turing.PartrecToTM2.K' → Turing.PartrecToTM2.Stmt' → Turing.PartrecToTM2.Stmt'
-- Mathlib.LinearAlgebra.Isomorphisms
LinearMap.quotKerEquivOfSurjective.congr_simp : ∀ {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup M₂]
  [inst_3 : Module R M] [inst_4 : Module R M₂] (f : M →ₗ[R] M₂) (hf : Function.Surjective ⇑f),
  f.quotKerEquivOfSurjective hf = f.quotKerEquivOfSurjective hf
-- Mathlib.Algebra.SkewPolynomial.Basic
/-- For a skew polynomial `p`, `p.sum f` can be written in terms of `SkewMonoidAlgebra.sum p`.  -/
SkewPolynomial.sum_def' : ∀ {R : Type u_1} [inst : Semiring R] {S : Type u_5} [inst_1 : AddCommMonoid S] (p : SkewPolynomial R) (f : ℕ → R → S),
  p.sum f = SkewMonoidAlgebra.sum p fun n r => f (Multiplicative.toAdd n) r
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
not_linearIndependent_iffₛ : ∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M], ¬LinearIndependent R v ↔ ∃ s f g, ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i ∧ ∃ i ∈ s, f i ≠ g i
-- Mathlib.Order.Interval.Set.Pi
Set.pi_univ_Iio_subset : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → Preorder (α i)] (x : (i : ι) → α i) [Nonempty ι],
  (Set.univ.pi fun i => Set.Iio (x i)) ⊆ Set.Iio x