mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Vector.Lemmas
Vector.flatMap_assoc : ∀ {α : Type u_1} {n : ℕ} {β : Type u_2} {m : ℕ} {γ : Type u_3} {k : ℕ} {xs : Vector α n} {f : α → Vector β m}
  {g : β → Vector γ k}, (xs.flatMap f).flatMap g = Vector.cast ⋯ (xs.flatMap fun x => (f x).flatMap g)
-- Mathlib.Combinatorics.Enumerative.DoubleCounting
Finset.card_mul_le_card_mul' : ∀ {α : Type u_2} {β : Type u_3} (r : α → β → Prop) {s : Finset α} {t : Finset β} {m n : ℕ}
  [inst : (a : α) → (b : β) → Decidable (r a b)],
  (∀ b ∈ t, n ≤ (Finset.bipartiteBelow r s b).card) →
    (∀ a ∈ s, (Finset.bipartiteAbove r t a).card ≤ m) → t.card * n ≤ s.card * m
-- Mathlib.Topology.MetricSpace.Thickening
/-- A set is contained in its own closed thickening.  -/
Metric.self_subset_cthickening : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {δ : ℝ} (E : Set α), E ⊆ Metric.cthickening δ E
-- Mathlib.FieldTheory.RatFunc.Valuation
RatFunc.CompletionAtInfty.instCoe : (F : Type u_1) → [inst : Field F] → [inst_1 : DecidableEq (RatFunc F)] → Coe (RatFunc F) (RatFunc.CompletionAtInfty F)
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
SubMulAction.fixingSubgroupEquivFixingSubgroup_coe_apply : ∀ {M : Type u_1} {α : Type u_2} [inst : Group M] [inst_1 : MulAction M α] {s t : Set α} {g : M} (hg : g • t = s)
  (x : ↥(fixingSubgroup M t)), ↑((SubMulAction.fixingSubgroupEquivFixingSubgroup hg) x) = (MulAut.conj g) ↑x
-- Init.System.Promise
/-- Creates a new `Promise`.  -/
IO.Promise.new : {α : Type} → [Nonempty α] → BaseIO (IO.Promise α)
-- Mathlib.Algebra.Homology.SpectralObject.Differentials
CategoryTheory.Abelian.SpectralObject.toCycles_πE_d : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i₀ i₁ i₂ i₃ i₄ i₅ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃)
  (f₄ : i₃ ⟶ i₄) (f₅ : i₄ ⟶ i₅) (f₁₂ : i₀ ⟶ i₂) (h₁₂ : CategoryTheory.CategoryStruct.comp f₁ f₂ = f₁₂) (f₃₄ : i₂ ⟶ i₄)
  (h₃₄ : CategoryTheory.CategoryStruct.comp f₃ f₄ = f₃₄) (n₀ n₁ n₂ n₃ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.toCycles_πE_d._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.toCycles_πE_d._auto_3)
  (hn₃ : autoParam (n₂ + 1 = n₃) CategoryTheory.Abelian.SpectralObject.toCycles_πE_d._auto_5),
  CategoryTheory.CategoryStruct.comp (X.toCycles f₃ f₄ f₃₄ h₃₄ n₁)
      (CategoryTheory.CategoryStruct.comp (X.πE f₃ f₄ f₅ n₀ n₁ n₂ hn₁ hn₂)
        (X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃)) =
    CategoryTheory.CategoryStruct.comp (X.δ f₁₂ f₃₄ n₁ n₂ hn₂)
      (CategoryTheory.CategoryStruct.comp (X.toCycles f₁ f₂ f₁₂ h₁₂ n₂) (X.πE f₁ f₂ f₃ n₁ n₂ n₃ hn₂ hn₃))
-- Mathlib.CategoryTheory.Monoidal.FunctorCategory
CategoryTheory.Monoidal.FunctorCategory.whiskerRight_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.MonoidalCategory D] {F G : CategoryTheory.Functor C D} (α : F ⟶ G)
  (F' : CategoryTheory.Functor C D) (X : C),
  (CategoryTheory.Monoidal.FunctorCategory.whiskerRight α F').app X =
    CategoryTheory.MonoidalCategoryStruct.whiskerRight (α.app X) (F'.obj X)
-- Mathlib.Data.PNat.Prime
PNat.eq_one_of_lt_two : ∀ {n : ℕ+}, n < 2 → n = 1
-- Mathlib.Probability.Independence.Conditional
ProbabilityTheory.CondIndep.condIndepSet_of_measurableSet : ∀ {Ω : Type u_1} {m' m₁ m₂ mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω] {hm' : m' ≤ mΩ}
  {μ : MeasureTheory.Measure Ω} [inst_1 : MeasureTheory.IsFiniteMeasure μ],
  ProbabilityTheory.CondIndep m' m₁ m₂ hm' μ →
    ∀ {s t : Set Ω}, MeasurableSet s → MeasurableSet t → ProbabilityTheory.CondIndepSet m' hm' s t μ
-- Mathlib.Algebra.Group.Subgroup.Pointwise
/-- For subgroups generated by a single element, see the simpler `zpow_induction_left`.  -/
Subgroup.closure_induction_left : ∀ {G : Type u_2} [inst : Group G] {s : Set G} {p : (x : G) → x ∈ Subgroup.closure s → Prop},
  p 1 ⋯ →
    (∀ (x : G) (hx : x ∈ s) (y : G) (hy : y ∈ Subgroup.closure s), p y hy → p (x * y) ⋯) →
      (∀ (x : G) (hx : x ∈ s) (y : G) (hy : y ∈ Subgroup.closure s), p y hy → p (x⁻¹ * y) ⋯) →
        ∀ {x : G} (h : x ∈ Subgroup.closure s), p x h
-- Mathlib.Analysis.Convex.Deriv
/-- If a function `f` is continuous and `f'` is strictly antitone on `ℝ` then `f` is strictly
concave. Note that we don't require differentiability, since it is guaranteed at all but at most
one point by the strict antitonicity of `f'`.  -/
StrictAnti.strictConcaveOn_univ_of_deriv : ∀ {f : ℝ → ℝ}, Continuous f → StrictAnti (deriv f) → StrictConcaveOn ℝ Set.univ f
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
IntermediateField.adjoin_intermediateField_toSubalgebra_of_isAlgebraic_left : ∀ {F : Type u_1} [inst : Field F] (E : Type u_2) [inst_1 : Field E] [inst_2 : Algebra F E] {K : Type u_3}
  [inst_3 : Field K] [inst_4 : Algebra F K] [inst_5 : Algebra E K] [IsScalarTower F E K] (L : IntermediateField F K)
  [halg : Algebra.IsAlgebraic F E], (IntermediateField.adjoin E ↑L).toSubalgebra = Algebra.adjoin E ↑L
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Lemmas
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.ratUnits_insert : ∀ {n : ℕ} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n)
  (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n), (f.insert c).ratUnits = f.ratUnits
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.coe_type_toSubalgebra : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (S : IntermediateField K L),
  ↥S.toSubalgebra = ↥S
-- Mathlib.Condensed.Light.InternallyProjective
LightCondensed.ihomPoints_symm_comp : ∀ (R : Type u) [inst : CommRing R] (B P : LightCondMod R) (S S' : LightProfinite) (π : S ⟶ S')
  (f : CategoryTheory.MonoidalCategoryStruct.tensorObj P ((LightCondensed.free R).obj S'.toCondensed) ⟶ B),
  (LightCondensed.ihomPoints R P B S).symm
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P
          ((LightCondensed.free R).map (lightProfiniteToLightCondSet.map π)))
        f) =
    (CategoryTheory.ConcreteCategory.hom ((P ⟹ B).obj.map π.op)) ((LightCondensed.ihomPoints R P B S').symm f)
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
/-- Notation for the space of bundled smooth (infinitely differentiable)
functions with support in a compact set `K`.  -/
Distributions.«term𝓓_{_}(_,_)» : Lean.ParserDescr
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.toContinuousAddMonoidHom_id : ∀ {R₁ : Type u_1} [inst : Semiring R₁] {M₁ : Type u_4} [inst_1 : TopologicalSpace M₁] [inst_2 : AddCommMonoid M₁]
  [inst_3 : Module R₁ M₁], ↑(ContinuousLinearMap.id R₁ M₁) = ContinuousAddMonoidHom.id M₁
-- Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
/-- If G preserves terminal objects and pullbacks, it preserves all finite limits.  -/
CategoryTheory.Limits.preservesFiniteLimits_of_preservesTerminal_and_pullbacks : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasPullbacks C] (G : CategoryTheory.Functor C D)
  [CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) G]
  [CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingCospan G],
  CategoryTheory.Limits.PreservesFiniteLimits G
-- Mathlib.Algebra.Order.GroupWithZero.Basic
one_le_inv_mul₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] {a b : G₀},
  0 < a → (1 ≤ a⁻¹ * b ↔ a ≤ b)
-- Mathlib.CategoryTheory.Bicategory.Grothendieck
/-- The type of objects in the fibered category associated to a pseudofunctor from a
1-category to Cat.  -/
CategoryTheory.Pseudofunctor.Grothendieck : {𝒮 : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] →
    CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮) CategoryTheory.Cat → Type (max u₁ u₂)
-- Mathlib.Algebra.Group.InjSurj
Function.Injective.negZeroClass.eq_1 : ∀ {M₁ : Type u_1} {M₂ : Type u_2} [inst : Zero M₁] [inst_1 : Neg M₁] [inst_2 : NegZeroClass M₂] (f : M₁ → M₂)
  (hf : Function.Injective f) (one : f 0 = 0) (inv : ∀ (x : M₁), f (-x) = -f x),
  Function.Injective.negZeroClass f hf one inv = { toZero := inst, toNeg := inst_1, neg_zero := ⋯ }
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get_insert_self : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] (h : (↑m).WF) {k : α} {v : β},
  Std.DHashMap.Internal.Raw₀.Const.get (m.insert k v) k ⋯ = v
-- Mathlib.Data.List.Cycle
List.next_singleton : ∀ {α : Type u_1} [inst : DecidableEq α] (x y : α) (h : x ∈ [y]), [y].next x h = y
-- Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Finset.prod_eq_mul_prod_sdiff_singleton : ∀ {ι : Type u_1} {M : Type u_3} [inst : CommMonoid M] [inst_1 : DecidableEq ι] {s : Finset ι} (i : ι) (f : ι → M),
  (i ∉ s → f i = 1) → ∏ x ∈ s, f x = f i * ∏ x ∈ s \ {i}, f x
-- Mathlib.Probability.IdentDistrib
ProbabilityTheory.IdentDistrib.nnnorm : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  [inst_2 : MeasurableSpace γ] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} {f : α → γ} {g : β → γ}
  [inst_3 : NormedAddCommGroup γ] [OpensMeasurableSpace γ],
  ProbabilityTheory.IdentDistrib f g μ ν → ProbabilityTheory.IdentDistrib (fun x => ‖f x‖₊) (fun x => ‖g x‖₊) μ ν
-- Mathlib.Algebra.Ring.Hom.Defs
/-- Reinterpret a non-unital ring homomorphism `f : α →ₙ+* β` as a semigroup
homomorphism `α →ₙ* β`. The `simp`-normal form is `(f : α →ₙ* β)`.  -/
NonUnitalRingHom.toMulHom : {α : Type u_5} →
  {β : Type u_6} → [inst : NonUnitalNonAssocSemiring α] → [inst_1 : NonUnitalNonAssocSemiring β] → (α →ₙ+* β) → α →ₙ* β
-- Mathlib.Algebra.Group.Basic
mul_one_eq_id : ∀ {M : Type u_4} [inst : MulOneClass M], (fun x => x * 1) = id
-- Std.Data.DTreeMap.Internal.WF.Defs
/-- Well-formedness of tree maps.  -/
Std.DTreeMap.Internal.Impl.WF : {α : Type u} → [Ord α] → {β : α → Type v} → Std.DTreeMap.Internal.Impl α β → Prop
-- Mathlib.CategoryTheory.Limits.Types.ColimitType
CategoryTheory.Functor.ιColimitType_eq_iff : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J (Type w₀)) {j j' : J}
  (x : F.obj j) (y : F.obj j'),
  F.ιColimitType j x = F.ιColimitType j' y ↔ Relation.EqvGen F.ColimitTypeRel ⟨j, x⟩ ⟨j', y⟩
-- Init.Data.Rat.Lemmas
Rat.ceil_add_one : ∀ {x : ℚ}, (x + 1).ceil = x.ceil + 1
-- Init.Data.Vector.Lemmas
Vector.foldr.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} (f : α → β → β) (b : β) (xs : Vector α n),
  Vector.foldr f b xs = Array.foldr f b xs.toArray
-- Mathlib.RingTheory.RamificationInertia.Inertia
/-- **Alias** of `Ideal.inertiaDeg_tower`. -/
Ideal.inertiaDeg'_tower : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  [inst_3 : Algebra R S] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [IsScalarTower R S T] (q : Ideal S) (r : Ideal T)
  [r.LiesOver q], r.inertiaDeg R = q.inertiaDeg R * r.inertiaDeg S
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem?_inter_of_not_mem_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  k ∉ t₁ → (t₁ ∩ t₂)[k]? = none
-- Mathlib.NumberTheory.MulChar.Basic
/-- If two values of quadratic characters with target `ℤ` agree after coercion into a ring
of characteristic not `2`, then they agree in `ℤ`.  -/
MulChar.IsQuadratic.eq_of_eq_coe : ∀ {R : Type u_1} [inst : CommMonoid R] {R' : Type u_2} [inst_1 : CommRing R'] {R'' : Type u_3} [inst_2 : CommRing R'']
  {χ : MulChar R ℤ},
  χ.IsQuadratic →
    ∀ {χ' : MulChar R' ℤ},
      χ'.IsQuadratic → ∀ [Nontrivial R''], ringChar R'' ≠ 2 → ∀ {a : R} {a' : R'}, ↑(χ a) = ↑(χ' a') → χ a = χ' a'
-- Mathlib.Analysis.Analytic.Linear
LinearIsometryEquiv.analyticOn : ∀ {𝕜 : 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] (f : E ≃ₗᵢ[𝕜] F)
  (s : Set E), AnalyticOn 𝕜 (⇑f) s
-- Mathlib.Analysis.Normed.Group.Constructions
ULift.normedAddGroup.eq_1 : ∀ {E : Type u_2} [inst : NormedAddGroup E],
  ULift.normedAddGroup =
    NormedAddGroup.induced (ULift.{u_5, u_2} E) E { toFun := ULift.down, map_zero' := ⋯, map_add' := ⋯ } ⋯
-- Mathlib.CategoryTheory.Limits.Presheaf
CategoryTheory.Presheaf.restrictedULiftYonedaHomEquiv'_symm_naturality_right_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {ℰ : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} ℰ]
  (A : CategoryTheory.Functor C ℰ) (P : CategoryTheory.Functor Cᵒᵖ (Type (max w v₁ v₂))) {E E' : ℰ} (g : E ⟶ E')
  (f : P ⟶ (CategoryTheory.Presheaf.restrictedULiftYoneda A).obj E)
  {Z : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.uliftYoneda.{max w v₂, v₁, u₁} P) ℰ}
  (h :
    (CategoryTheory.Functor.const
            (CategoryTheory.CostructuredArrow CategoryTheory.uliftYoneda.{max w v₂, v₁, u₁} P)).obj
        E' ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Presheaf.restrictedULiftYonedaHomEquiv' A P E').symm
        (CategoryTheory.CategoryStruct.comp f ((CategoryTheory.Presheaf.restrictedULiftYoneda A).map g)))
      h =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.Presheaf.restrictedULiftYonedaHomEquiv' A P E).symm f)
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.Functor.const
              (CategoryTheory.CostructuredArrow CategoryTheory.uliftYoneda.{max w v₂, v₁, u₁} P)).map
          g)
        h)
-- Init.Data.Float.Model.Float32
Float32.instDecidableEqModel : DecidableEq Float32.Model
-- Init.Data.Ord.Basic
Ordering.then_eq_eq : ∀ {o₁ o₂ : Ordering}, o₁.then o₂ = Ordering.eq ↔ o₁ = Ordering.eq ∧ o₂ = Ordering.eq
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getD_ofList_of_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] {l : List (α × β)} {k k' : α},
  cmp k k' = Ordering.eq →
    ∀ {v fallback : β},
      List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l →
        (k, v) ∈ l → (Std.TreeMap.ofList l cmp).getD k' fallback = v
-- Std.Sync.RecursiveMutex
/-- Creates a new `BaseRecursiveMutex`.  -/
Std.BaseRecursiveMutex.new : BaseIO Std.BaseRecursiveMutex
-- Init.Data.SInt.Lemmas
Int64.add_comm : ∀ (a b : Int64), a + b = b + a
-- Mathlib.Data.Int.ConditionallyCompleteOrder
Int.csInf_mem : ∀ {s : Set ℤ}, s.Nonempty → BddBelow s → sInf s ∈ s
-- Mathlib.RingTheory.SimpleModule.Basic
IsSimpleModule.instIsNoetherian : ∀ (R : Type u_2) [inst : Ring R] {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsSimpleModule R M],
  IsNoetherian R M
-- Mathlib.LinearAlgebra.Matrix.Permanent
Matrix.permanent_eq_one_of_card_eq_zero : ∀ {n : Type u_1} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type u_2} [inst_2 : CommSemiring R]
  {A : Matrix n n R}, Fintype.card n = 0 → A.permanent = 1
-- Mathlib.Computability.DFA
/-- Regular languages are closed under union.  -/
Language.IsRegular.add : ∀ {T : Type u} {L1 L2 : Language T}, L1.IsRegular → L2.IsRegular → (L1 + L2).IsRegular
-- Init.Core
instDecidableFalse : Decidable False
-- Mathlib.RingTheory.Ideal.Prod
Ideal.prod_mono_left : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] {I₁ I₂ : Ideal R} {J : Ideal S},
  I₁ ≤ I₂ → I₁.prod J ≤ I₂.prod J
-- Mathlib.Topology.Separation.Basic
Topology.IsEmbedding.t1Space : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [T1Space Y] {f : X → Y},
  Topology.IsEmbedding f → T1Space X
-- Mathlib.Data.SubtypeNeLift
Function.subtypeNeLift_of_neq : ∀ {ι : Type u_1} [inst : DecidableEq ι] {M : ι → Type u_2} (i₀ : ι) (f : (j : { i // i ≠ i₀ }) → M ↑j) (x : M i₀)
  (i : ι) (h : i ≠ i₀), Function.subtypeNeLift i₀ f x i = f ⟨i, h⟩
-- Init.Data.Nat.Div.Lemmas
Nat.lt_div_iff_mul_lt : ∀ {k x y : ℕ}, 0 < k → (x < y / k ↔ x * k < y - (k - 1))
-- Lean.Meta.Basic
Lean.Meta.mkFreshLevelMVar : Lean.MetaM Lean.Level
-- Mathlib.RingTheory.NonUnitalSubring.Defs
/-- The natural non-unital ring hom from a non-unital subring of a non-unital ring `R` to `R`.  -/
NonUnitalSubringClass.subtype : {R : Type u} →
  {S : Type v} →
    [inst : NonUnitalNonAssocRing R] → [inst_1 : SetLike S R] → [hSR : NonUnitalSubringClass S R] → (s : S) → ↥s →ₙ+* R
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
/-- The zero morphism has a `MonoFactorisation` through the zero object.
 -/
CategoryTheory.Limits.monoFactorisationZero : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      [CategoryTheory.Limits.HasZeroObject C] → (X Y : C) → CategoryTheory.Limits.MonoFactorisation 0
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.degree_eq_zero_iff : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] {f : MvPolynomial σ R},
  m.degree f = 0 ↔ f = MvPolynomial.C (m.leadingCoeff f)
-- Mathlib.Topology.FiberBundle.Constructions
/-- Local trivialization for trivial bundle.  -/
Bundle.Trivial.trivialization : (B : Type u_1) →
  (F : Type u_2) →
    [inst : TopologicalSpace B] → [inst_1 : TopologicalSpace F] → Bundle.Trivialization F Bundle.TotalSpace.proj
-- Mathlib.RingTheory.Bialgebra.GroupLike
GroupLike.valMonoidHom_apply : ∀ (R : Type u_1) (A : Type u_2) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Bialgebra R A]
  (self : GroupLike R A), (GroupLike.valMonoidHom R A) self = ↑self
-- Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Asymptotics.transIsEquivalentIsTheta : {α : Type u_1} →
  {β : Type u_2} →
    {β₂ : Type u_3} →
      [inst : NormedAddCommGroup β] →
        [inst_1 : Norm β₂] →
          {l : Filter α} → Trans (Asymptotics.IsEquivalent l) (Asymptotics.IsTheta l) (Asymptotics.IsTheta l)
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.restrict_eq_self : ∀ {α : Type u_1} {mα : MeasurableSpace α} {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M]
  (v : MeasureTheory.VectorMeasure α M) {i : Set α},
  MeasurableSet i → ∀ {j : Set α}, MeasurableSet j → j ⊆ i → (v.restrict i) j = v j
-- Mathlib.FieldTheory.Perfect
/-- A perfect field.

See also `PerfectRing` for a generalisation in positive characteristic.  -/
PerfectField : (K : Type u_1) → [Field K] → Prop
-- Init.Data.UInt.Bitwise
UInt16.shiftLeft_or : ∀ {a b c : UInt16}, (a ||| b) <<< c = a <<< c ||| b <<< c
-- Mathlib.AlgebraicGeometry.ResidueField
AlgebraicGeometry.Scheme.instFieldCarrierResidueField : (X : AlgebraicGeometry.Scheme) → (x : ↥X) → Field ↑(X.residueField x)
-- Lean.Meta.Basic
Lean.Meta.PostponedEntry.lhs : Lean.Meta.PostponedEntry → Lean.Level
-- Mathlib.Topology.Algebra.FilterBasis
RingFilterBasis.mul_right' : ∀ {R : Type u} {inst : Ring R} [self : RingFilterBasis R] (x₀ : R) {U : Set R},
  U ∈ self.sets → ∃ V ∈ self.sets, V ⊆ (fun x => x * x₀) ⁻¹' U
-- Mathlib.Tactic.TacticAnalysis
/-- Run the tactic analysis passes from `configs` on the tactic sequences in `stx`,
using `trees` to get the infotrees.  -/
Mathlib.TacticAnalysis.runPasses : Array Mathlib.TacticAnalysis.Pass → Lean.PersistentArray Lean.Elab.InfoTree → Lean.Elab.Command.CommandElabM Unit
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.mapLeftEq_inv_app_left : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  (R : CategoryTheory.Functor B T) {P : CategoryTheory.MorphismProperty T} {Q : CategoryTheory.MorphismProperty A}
  {W : CategoryTheory.MorphismProperty B} [inst_3 : Q.IsMultiplicative] [inst_4 : W.IsMultiplicative]
  {L₁ L₂ : CategoryTheory.Functor A T} [inst_5 : Q.RespectsIso] [inst_6 : W.RespectsIso] (l l' : L₁ ⟶ L₂) (h : l = l')
  (hl :
    ∀ (X : CategoryTheory.MorphismProperty.Comma L₂ R P Q W),
      P (CategoryTheory.CategoryStruct.comp (l.app X.left) X.hom))
  (X : CategoryTheory.MorphismProperty.Comma L₂ R P Q W),
  ((CategoryTheory.MorphismProperty.Comma.mapLeftEq R l l' h hl).inv.app X).left =
    CategoryTheory.CategoryStruct.id X.left
-- Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
/-- **Alias** of the forward direction of `collinear_iff_finrank_le_one`.

---

A set of points, whose `vectorSpan` is finite-dimensional, is
collinear if and only if their `vectorSpan` has dimension at most
`1`.  -/
Collinear.finrank_le_one : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {s : Set P} [FiniteDimensional k ↥(vectorSpan k s)],
  Collinear k s → Module.finrank k ↥(vectorSpan k s) ≤ 1
-- Mathlib.Analysis.Distribution.DerivNotation
LineDerivAdd.lineDerivOp_left_add : ∀ {V : Type u} {E : Type v} {F : outParam (Type w)} {inst : AddCommGroup V} {inst_1 : AddCommGroup E}
  {inst_2 : AddCommGroup F} {inst_3 : LineDeriv V E F} [self : LineDerivAdd V E F] (v w : V) (x : E),
  LineDeriv.lineDerivOp (v + w) x = LineDeriv.lineDerivOp v x + LineDeriv.lineDerivOp w x
-- Init.Data.Option.Lemmas
Option.guard_def : ∀ {α : Type u_1} (p : α → Bool), Option.guard p = fun x => if p x = true then some x else none
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
/-- The multicofork associated to the multicoequalizer.  -/
CategoryTheory.Limits.Multicoequalizer.multicofork : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.Limits.MultispanShape} →
      (I : CategoryTheory.Limits.MultispanIndex J C) →
        [CategoryTheory.Limits.HasMulticoequalizer I] → CategoryTheory.Limits.Multicofork I
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.SummableFamily.coe_injective : ∀ {Γ : Type u_1} {R : Type u_3} {α : Type u_5} [inst : PartialOrder Γ] [inst_1 : AddCommMonoid R],
  Function.Injective DFunLike.coe
-- Init.Data.Array.Lemmas
Array.swapAt_def : ∀ {α : Type u_1} {xs : Array α} {i : ℕ} {v : α} (hi : i < xs.size), xs.swapAt i v hi = (xs[i], xs.set i v hi)
-- Mathlib.Order.Heyting.Regular
Heyting.Regular.boundedOrder : {α : Type u_1} → [inst : HeytingAlgebra α] → BoundedOrder (Heyting.Regular α)
-- Std.Data.String.ToNat
Break.runK.match_1.congr_eq_1 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (x : Option α) (h_1 : (a : α) → motive (some a))
  (h_2 : Unit → motive none) (a : α),
  x = some a →
    (match x with
      | some a => h_1 a
      | none => h_2 ()) ≍
      h_1 a
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.toCharNeTwoNF_r : ∀ {R : Type u_1} [inst : CommRing R] (W : WeierstrassCurve R) [inst_1 : Invertible 2], W.toCharNeTwoNF.r = 0
-- Mathlib.Algebra.Group.Action.Option
Option.smul_some : ∀ {M : Type u_1} {α : Type u_3} [inst : SMul M α] (a : M) (b : α), a • some b = some (a • b)
-- Mathlib.Data.Nat.Squarefree
Nat.squarefree_iff_minSqFac : ∀ {n : ℕ}, Squarefree n ↔ n.minSqFac = none
-- Mathlib.Data.Holor
/-- The original holor can be recovered from its slices by multiplying with unit vectors and
summing up.  -/
Holor.sum_unitVec_mul_slice : ∀ {α : Type} {d : ℕ} {ds : List ℕ} [inst : Semiring α] (x : Holor α (d :: ds)),
  ∑ i ∈ (Finset.range d).attach, (Holor.unitVec d ↑i).mul (x.slice ↑i ⋯) = x
-- Mathlib.RingTheory.Congruence.Defs
RingCon.instAddCommMonoidQuotient : {R : Type u_1} → [inst : AddCommMonoid R] → [inst_1 : Mul R] → (c : RingCon R) → AddCommMonoid c.Quotient
-- Mathlib.Algebra.Lie.SemiDirect
LieAlgebra.SemiDirectSum.projr_inl_apply : ∀ {R : Type u_1} [inst : CommRing R] {K : Type u_2} [inst_1 : LieRing K] [inst_2 : LieAlgebra R K] {L : Type u_3}
  [inst_3 : LieRing L] [inst_4 : LieAlgebra R L] (ψ : L →ₗ⁅R⁆ LieDerivation R K K) {x : K},
  (LieAlgebra.SemiDirectSum.projr ψ) ((LieAlgebra.SemiDirectSum.inl ψ) x) = 0