mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
/-- **Vertical Angles Theorem**: angles opposite each other, formed by two intersecting straight
lines, are equal.  -/
EuclideanGeometry.angle_eq_angle_of_angle_eq_pi_of_angle_eq_pi : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {p₁ p₂ p₃ p₄ p₅ : P},
  EuclideanGeometry.angle p₁ p₅ p₃ = Real.pi →
    EuclideanGeometry.angle p₂ p₅ p₄ = Real.pi → EuclideanGeometry.angle p₁ p₅ p₂ = EuclideanGeometry.angle p₃ p₅ p₄
-- Lean.Environment
Lean.Kernel.Environment.Diagnostics.recordUnfold : Lean.Kernel.Diagnostics → Lean.Name → Lean.Kernel.Diagnostics
-- Mathlib.Data.Fin.Init
Fin.xor_zero : ∀ {k : ℕ} [inst : NeZero k] (a : Fin k), a ^^^ 0 = a
-- Lean.Message
/-- Returns the error name with which `msg` is tagged, if one exists.

Note that this is distinct from `msg.kind`: the `kind` of a named-error message is not equal to its
name, and there exist message kinds that are not error-name kinds.
 -/
Lean.MessageData.errorName? : Lean.MessageData → Option Lean.Name
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Lemmas
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.insert_iff : ∀ {n : ℕ} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n)
  (c1 c2 : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n), c2 ∈ (f.insert c1).toList ↔ c2 = c1 ∨ c2 ∈ f.toList
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.measure_eq_measure_larger_of_between_null_sdiff : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s₁ s₂ s₃ : Set α},
  s₁ ⊆ s₂ → s₂ ⊆ s₃ → μ (s₃ \ s₁) = 0 → μ s₂ = μ s₃
-- Mathlib.LinearAlgebra.Prod
LinearMap.coprod_comp_prod : ∀ {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} {M₄ : Type z} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M₃] [inst_4 : AddCommMonoid M₄] [inst_5 : Module R M]
  [inst_6 : Module R M₂] [inst_7 : Module R M₃] [inst_8 : Module R M₄] (f : M₂ →ₗ[R] M₄) (g : M₃ →ₗ[R] M₄)
  (f' : M →ₗ[R] M₂) (g' : M →ₗ[R] M₃), f.coprod g ∘ₗ f'.prod g' = f ∘ₗ f' + g ∘ₗ g'
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Expr.toPoly.match_1.congr_eq_5 : ∀ (motive : Lean.Grind.CommRing.Expr → Sort u_1) (a : Lean.Grind.CommRing.Expr)
  (h_1 : (n : ℤ) → motive (Lean.Grind.CommRing.Expr.num n))
  (h_2 : (n : ℤ) → motive (Lean.Grind.CommRing.Expr.intCast n))
  (h_3 : (n : ℕ) → motive (Lean.Grind.CommRing.Expr.natCast n))
  (h_4 : (x : Lean.Grind.CommRing.Var) → motive (Lean.Grind.CommRing.Expr.var x))
  (h_5 : (x : Lean.Grind.CommRing.Expr) → motive x) (x : Lean.Grind.CommRing.Expr),
  a = x →
    (∀ (n : ℤ), x = Lean.Grind.CommRing.Expr.num n → False) →
      (∀ (n : ℤ), x = Lean.Grind.CommRing.Expr.intCast n → False) →
        (∀ (n : ℕ), x = Lean.Grind.CommRing.Expr.natCast n → False) →
          (∀ (x_4 : Lean.Grind.CommRing.Var), x = Lean.Grind.CommRing.Expr.var x_4 → False) →
            (match a with
              | Lean.Grind.CommRing.Expr.num n => h_1 n
              | Lean.Grind.CommRing.Expr.intCast n => h_2 n
              | Lean.Grind.CommRing.Expr.natCast n => h_3 n
              | Lean.Grind.CommRing.Expr.var x => h_4 x
              | x => h_5 x) ≍
              h_5 x
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.foldrM_eq_foldrM_toList : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} {δ : Type w} {m : Type w → Type w'} [inst : Monad m]
  [LawfulMonad m] {f : α → δ → m δ} {init : δ}, Std.TreeSet.Raw.foldrM f init t = List.foldrM f init t.toList
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2.Stmt.goto.inj : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} {a a_1 : σ → Λ},
  Turing.TM2.Stmt.goto a = Turing.TM2.Stmt.goto a_1 → a = a_1
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Real
AEMeasurable.coe_nnreal_real : ∀ {α : Type u_1} {mα : MeasurableSpace α} {f : α → NNReal} {μ : MeasureTheory.Measure α},
  AEMeasurable f μ → AEMeasurable (fun x => ↑(f x)) μ
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem?_eq_some_iff : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α} {v : β}, t[k]? = some v ↔ ∃ (h : k ∈ t), t[k] = v
-- Mathlib.Topology.MetricSpace.Congruence
/-- A congruence preserves extended distance. Forward direction of `congruent_iff_edist_eq`.  -/
Congruent.edist_eq : ∀ {ι : Type u_1} {P₁ : Type u_3} {P₂ : Type u_4} {v₁ : ι → P₁} {v₂ : ι → P₂} [inst : PseudoEMetricSpace P₁]
  [inst_1 : PseudoEMetricSpace P₂], Congruent v₁ v₂ → ∀ (i₁ i₂ : ι), edist (v₁ i₁) (v₁ i₂) = edist (v₂ i₁) (v₂ i₂)
-- Mathlib.RingTheory.Polynomial.Bernstein
bernsteinPolynomial.flip' : ∀ (R : Type u_1) [inst : CommRing R] (n ν : ℕ),
  ν ≤ n → bernsteinPolynomial R n ν = (bernsteinPolynomial R n (n - ν)).comp (1 - Polynomial.X)
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.cosimplicialSimplicialEquiv_inverse_obj : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor SimplexCategoryᵒᵖ Cᵒᵖ),
  (CategoryTheory.cosimplicialSimplicialEquiv C).inverse.obj F = Opposite.op F.unop
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MultispanIndex.mk.injEq : ∀ {J : CategoryTheory.Limits.MultispanShape} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (left : J.L → C)
  (right : J.R → C) (fst : (a : J.L) → left a ⟶ right (J.fst a)) (snd : (a : J.L) → left a ⟶ right (J.snd a))
  (left_1 : J.L → C) (right_1 : J.R → C) (fst_1 : (a : J.L) → left_1 a ⟶ right_1 (J.fst a))
  (snd_1 : (a : J.L) → left_1 a ⟶ right_1 (J.snd a)),
  ({ left := left, right := right, fst := fst, snd := snd } =
      { left := left_1, right := right_1, fst := fst_1, snd := snd_1 }) =
    (left = left_1 ∧ right = right_1 ∧ fst ≍ fst_1 ∧ snd ≍ snd_1)
-- Mathlib.Algebra.Order.Archimedean.Class
/-- Lift a function `{a : M // a ≠ 1} → α` that's monotone along archimedean
classes to a monotone function `FiniteArchimedeanClass M₁ →o α`.  -/
FiniteArchimedeanClass.liftOrderHom : {M : Type u_1} →
  [inst : AddCommGroup M] →
    [inst_1 : LinearOrder M] →
      [inst_2 : IsOrderedAddMonoid M] →
        {α : Type u_2} →
          [inst_3 : PartialOrder α] →
            (f : { a // a ≠ 0 } → α) →
              (∀ (a b : { a // a ≠ 0 }), FiniteArchimedeanClass.mk ↑a ⋯ ≤ FiniteArchimedeanClass.mk ↑b ⋯ → f a ≤ f b) →
                FiniteArchimedeanClass M →o α
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.coconeUnopOfConeEquiv_counitIso : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ},
  CategoryTheory.Limits.coconeUnopOfConeEquiv.counitIso =
    CategoryTheory.Iso.refl
      ({ obj := fun c => Opposite.op (CategoryTheory.Limits.coneOfCoconeUnop c),
            map := fun {X Y} f => Opposite.op { hom := f.hom.op, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }.comp
        { obj := fun c => CategoryTheory.Limits.coconeUnopOfCone (Opposite.unop c),
          map := fun {X Y} f => { hom := f.unop.hom.unop, w := ⋯ }, map_id := ⋯, map_comp := ⋯ })
-- Mathlib.Algebra.Lie.Nilpotent
LieModule.iInf_lcs_le_of_isNilpotent_quot : ∀ (R : Type u) (L : Type v) (M : Type w) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] (N : LieSubmodule R L M)
  [inst_6 : LieModule R L M], LieModule.IsNilpotent L (M ⧸ N) → ⨅ k, LieModule.lowerCentralSeries R L M k ≤ N
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.min_insert_le_self : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [inst : Std.TransCmp cmp] {k : α},
  (cmp ((t.insert k).min ⋯) k).isLE = true
-- Mathlib.Data.Holor
Holor.CPRankMax.below.succ : ∀ {α : Type} [inst : Mul α] [inst_1 : AddMonoid α]
  {motive : (a : ℕ) → {ds : List ℕ} → (a_1 : Holor α ds) → Holor.CPRankMax a a_1 → Prop} (n : ℕ) {ds : List ℕ}
  (x y : Holor α ds) (a : x.CPRankMax1) (a_1 : Holor.CPRankMax n y),
  Holor.CPRankMax.below a_1 → motive n y a_1 → Holor.CPRankMax.below ⋯
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBSet.findP?_insert : ∀ {α : Type u_1} {cmp : α → α → Ordering} [Std.TransCmp cmp] (t : RBTree.RBSet α cmp) (v : α) (cut : α → Ordering)
  [RBTree.RBNode.IsStrictCut cmp cut], (t.insert v).findP? cut = if cut v = Ordering.eq then some v else t.findP? cut
-- Mathlib.Analysis.Complex.TaylorSeries
/-- A function that is complex differentiable on the complex plane is given by evaluating
its Taylor series at any point `c`.  -/
Complex.taylorSeries_eq_of_entire : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [CompleteSpace E] ⦃f : ℂ → E⦄,
  Differentiable ℂ f → ∀ (c z : ℂ), ∑' (n : ℕ), (↑n.factorial)⁻¹ • (z - c) ^ n • iteratedDeriv n f c = f z
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get?_insertIfNew : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp] {k a : α}
  {v : β},
  Std.DTreeMap.Const.get? (t.insertIfNew k v) a =
    if cmp k a = Ordering.eq ∧ k ∉ t then some v else Std.DTreeMap.Const.get? t a
-- Init.Data.String.Lemmas.Pattern.Basic
/-- Predicate stating that the region between the start of the slice `s` and the position
`pos` matches the pattern `pat`, and that there is no longer match starting at the
beginning of the slice. This is what a correct matcher should match.

In some cases, being a match and being a longest match will coincide, see
`String.Slice.Pattern.Model.NoPrefixPatternModel`.
 -/
String.Slice.Pattern.Model.IsLongestMatch : {ρ : Type} → (pat : ρ) → [String.Slice.Pattern.Model.PatternModel pat] → {s : String.Slice} → s.Pos → Prop
-- Mathlib.CategoryTheory.Bicategory.Monad.Basic
CategoryTheory.Bicategory.Comonad.comul_assoc_flip_assoc : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a : B} (t : a ⟶ a) [inst_1 : CategoryTheory.Bicategory.Comonad t]
  {Z : a ⟶ a} (h : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp t t) t ⟶ Z),
  CategoryTheory.CategoryStruct.comp CategoryTheory.Bicategory.Comonad.comul
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerRight CategoryTheory.Bicategory.Comonad.comul t) h) =
    CategoryTheory.CategoryStruct.comp CategoryTheory.Bicategory.Comonad.comul
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerLeft t CategoryTheory.Bicategory.Comonad.comul)
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator t t t).inv h))
-- Mathlib.SetTheory.Cardinal.Cofinality.Basic
_private.Mathlib.SetTheory.Cardinal.Cofinality.Basic.0.Order.cof.eq_1 : ∀ (α : Type u) [inst : Preorder α], Order.cof α = ⨅ s, Cardinal.mk ↑↑s
-- Mathlib.CategoryTheory.Triangulated.TStructure.Basic
CategoryTheory.Triangulated.TStructure.isGE_shift_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (X : C) (n a n' : ℤ),
  autoParam (a + n' = n) CategoryTheory.Triangulated.TStructure.isGE_shift_iff._auto_1 →
    (t.IsGE ((CategoryTheory.shiftFunctor C a).obj X) n' ↔ t.IsGE X n)
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
BorelSpace.countablyGenerated : ∀ {α : Type u_6} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] [BorelSpace α] [SecondCountableTopology α],
  MeasurableSpace.CountablyGenerated α
-- Lean.Declaration
/-- Number of fields (i.e., arity - nparams)  -/
Lean.ConstructorVal.numFields : Lean.ConstructorVal → ℕ
-- Mathlib.Algebra.Group.Hom.Instances
MonoidHom.instCommGroup.eq_1 : ∀ {M : Type uM} {N : Type uN} [inst : MulOneClass M] [inst_1 : CommGroup N],
  MonoidHom.instCommGroup =
    { toMonoid := MonoidHom.instCommMonoid.toMonoid, toInv := MonoidHom.instInv, toDiv := MonoidHom.instDiv,
      toZPow := ZPow.ofPow, div_eq_mul_inv := ⋯, zpow_zero' := ⋯, zpow_succ' := ⋯, zpow_neg' := ⋯, inv_mul_cancel := ⋯,
      mul_comm := ⋯ }
-- Mathlib.Algebra.RingQuot
RingQuot.preLift_def : ∀ {R : Type u_1} [inst : Semiring R] {T : Type u_2} [inst_1 : Semiring T] {r : R → R → Prop} {f : R →+* T}
  (h : ∀ ⦃x y : R⦄, r x y → f x = f y),
  RingQuot.preLift h =
    { toFun := fun x => Quot.lift ⇑f ⋯ x.toQuot, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.NumberTheory.Modular
/-- The map `lcRow0` is proper, that is, preimages of cocompact sets are finite in
`[[* , *], [c, d]]`.  -/
ModularGroup.tendsto_lcRow0 : ∀ {cd : Fin 2 → ℤ},
  IsCoprime (cd 0) (cd 1) →
    Filter.Tendsto (fun g => (ModularGroup.lcRow0 cd) ↑((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) ↑g))
      Filter.cofinite (Filter.cocompact ℝ)
-- Init.Data.Vector.Lemmas
Vector.toArray_set! : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {i : ℕ} {x : α}, (xs.set! i x).toArray = xs.toArray.set! i x
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get?_eq_some_getD : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {a : α} {fallback : β}, a ∈ t → Std.DTreeMap.Raw.Const.get? t a = some (Std.DTreeMap.Raw.Const.getD t a fallback)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.DTreeMap.Internal.Cell.alter.match_1.eq_1 : ∀ {α : Type u_2} {β : α → Type u_1} (motive : Option ((a : α) × β a) → Sort u_3) (h_1 : none = none → motive none)
  (h_2 : (k' : α) → (v' : β k') → none = some ⟨k', v'⟩ → motive (some ⟨k', v'⟩)),
  (match h : none with
    | none => h_1 h
    | some ⟨k', v'⟩ => h_2 k' v' h) =
    h_1 ⋯
-- Mathlib.RingTheory.Ideal.Norm.AbsNorm
Ideal.isFiniteRelIndex : ∀ {S : Type u_1} [inst : CommRing S] [IsDedekindDomain S] [Module.Free ℤ S] [Module.Finite ℤ S] {I : Ideal S},
  I ≠ ⊥ → ∀ (J : Ideal S), (Submodule.toAddSubgroup I).IsFiniteRelIndex (Submodule.toAddSubgroup J)
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.Integrable.smul_measure_nnreal : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ε : Type u_8} [inst : TopologicalSpace ε]
  [inst_1 : ESeminormedAddMonoid ε] {f : α → ε},
  MeasureTheory.Integrable f μ → ∀ {c : NNReal}, MeasureTheory.Integrable f (c • μ)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
/-- A pair of morphisms `h : Y ⟶ W` and `k : Z ⟶ W` satisfying `f ≫ h = g ≫ k` induces a morphism
`pushout.desc : pushout f g ⟶ W`.  -/
CategoryTheory.Limits.pushout.desc : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {W X Y Z : C} →
      {f : X ⟶ Y} →
        {g : X ⟶ Z} →
          [inst_1 : CategoryTheory.Limits.HasPushout f g] →
            (h : Y ⟶ W) →
              (k : Z ⟶ W) →
                autoParam (CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g k)
                    CategoryTheory.Limits.pushout.desc._auto_1 →
                  (CategoryTheory.Limits.pushout f g ⟶ W)
-- Mathlib.Algebra.Order.Quantale
/-- Left- and right- residuation operators on an additive quantale are similar
to the Heyting operator on complete lattices, but for a non-commutative logic.
I.e. `x ≤ y ⇨ₗ z ↔ x + y ≤ z` or alternatively `x ⇨ₗ y = sSup { z | z + x ≤ y }`.  -/
AddQuantale.«term_⇨ₗ_» : Lean.TrailingParserDescr
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.SplitSource.ext.sizeOf_spec : ∀ (declName : Lean.Name), sizeOf (Lean.Meta.Grind.SplitSource.ext declName) = 1 + sizeOf declName
-- Mathlib.Order.Filter.Tendsto
Filter.Tendsto.neBot : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {x : Filter α} {y : Filter β},
  Filter.Tendsto f x y → ∀ [hx : x.NeBot], y.NeBot
-- Mathlib.Algebra.Homology.Embedding.TruncGE
/-- The morphism `K.truncGE' e ⟶ L.truncGE' e` induced by a morphism `K ⟶ L`.  -/
HomologicalComplex.truncGE'Map : {ι : Type u_1} →
  {ι' : Type u_2} →
    {c : ComplexShape ι} →
      {c' : ComplexShape ι'} →
        {C : Type u_3} →
          [inst : CategoryTheory.Category.{v_1, u_3} C] →
            [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
              {K L : HomologicalComplex C c'} →
                (K ⟶ L) →
                  (e : c.Embedding c') →
                    [inst_2 : e.IsTruncGE] →
                      [inst_3 : ∀ (i' : ι'), K.HasHomology i'] →
                        [inst_4 : ∀ (i' : ι'), L.HasHomology i'] → K.truncGE' e ⟶ L.truncGE' e
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get?_inter_of_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  {k : α}, k ∈ t₂ → Std.DTreeMap.Const.get? (t₁ ∩ t₂) k = Std.DTreeMap.Const.get? t₁ k
-- Mathlib.Algebra.Polynomial.AlgebraMap
/-- Algebra isomorphism between `R[X]` and `R[ℕ]`. This is just an
implementation detail, but it can be useful to transfer results from `Finsupp` to polynomials.  -/
Polynomial.toFinsuppIsoAlg : (R : Type u) → [inst : CommSemiring R] → Polynomial R ≃ₐ[R] AddMonoidAlgebra R ℕ
-- Mathlib.MeasureTheory.Integral.Bochner.L1
MeasureTheory.SimpleFunc.norm_integral_le_integral_norm : ∀ {α : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_1 : NormedSpace ℝ E] (f : MeasureTheory.SimpleFunc α E),
  MeasureTheory.Integrable (⇑f) μ →
    ‖MeasureTheory.SimpleFunc.integral μ f‖ ≤ MeasureTheory.SimpleFunc.integral μ (MeasureTheory.SimpleFunc.map norm f)
-- Mathlib.Analysis.RCLike.Basic
/-- The imaginary part in an `RCLike` field, as a continuous linear map.  -/
RCLike.imCLM : {K : Type u_1} → [inst : RCLike K] → StrongDual ℝ K
-- Mathlib.Topology.MetricSpace.BundledFun
/-- A pseudometric must respect the triangle inequality.  -/
PseudoMetric.triangle' : ∀ {X : Type u_1} {R : Type u_2} [inst : Zero R] [inst_1 : Add R] [inst_2 : LE R] (self : PseudoMetric X R) (x y z : X),
  self.toFun x z ≤ self.toFun x y + self.toFun y z
-- Mathlib.Order.Interval.Finset.Basic
Finset.Ioi_insert : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : LocallyFiniteOrderTop α] [inst_2 : DecidableEq α] (a : α),
  insert a (Finset.Ioi a) = Finset.Ici a
-- Mathlib.RingTheory.Coalgebra.TensorProduct
/-- `hopf_tensor_induction x with x₁ x₂` attempts to replace `x` by
`x₁ ⊗ₜ x₂` via linearity. This is an implementation detail that is used to set up tensor products
of coalgebras, bialgebras, and hopf algebras, and shouldn't be relied on downstream.  -/
TensorProduct.tacticHopf_tensor_induction_With__ : Lean.ParserDescr
-- Mathlib.ModelTheory.Substructures
/-- The substructure `M` of the structure `M`.  -/
FirstOrder.Language.Substructure.instTop : {L : FirstOrder.Language} → {M : Type w} → [inst : L.Structure M] → Top (L.Substructure M)
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey_insertEntry_self : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : EquivBEq α] {l : List ((a : α) × β a)} {k : α} {v : β k},
  Std.Internal.List.getKey k (Std.Internal.List.insertEntry k v l) ⋯ = k
-- Mathlib.CategoryTheory.Monoidal.Cartesian.InfSemilattice
CategoryTheory.SemilatticeInf.tensorObj : ∀ {C : Type u} [inst : SemilatticeInf C] [inst_1 : OrderTop C] {X Y : C},
  CategoryTheory.MonoidalCategoryStruct.tensorObj X Y = X ⊓ Y
-- Std.Async.Signal
/-- User-defined signal 1.
 -/
Std.Async.Signal.sigusr1 : Std.Async.Signal
-- Mathlib.Algebra.MvPolynomial.Degrees
MvPolynomial.degreeOf_C_mul_le : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] (p : MvPolynomial σ R) (i : σ) (c : R),
  MvPolynomial.degreeOf i (MvPolynomial.C c * p) ≤ MvPolynomial.degreeOf i p
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidIso.cancel_right : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  [inst_3 : Add α] [inst_4 : Add β] [inst_5 : Add γ] {g₁ g₂ : α ≃+o β} {f : β ≃+o γ},
  Function.Injective ⇑f → (g₁.trans f = g₂.trans f ↔ g₁ = g₂)
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.instPowInt : {α : Type u_1} →
  {γ : Type u_3} →
    [inst : MeasurableSpace α] →
      {μ : MeasureTheory.Measure α} →
        [inst_1 : TopologicalSpace γ] → [inst_2 : Group γ] → [IsTopologicalGroup γ] → Pow (α →ₘ[μ] γ) ℤ
-- Mathlib.Combinatorics.Configuration
/-- A projective plane is a nondegenerate configuration in which every pair of lines has
an intersection point, every pair of points has a line through them,
and which has three points in general position.  -/
Configuration.ProjectivePlane : (P : Type u_1) → (L : Type u_2) → [Membership P L] → Type (max u_1 u_2)
-- Mathlib.Algebra.Lie.Weights.Killing
/-- The collection of roots as a `Finset`.  -/
LieSubalgebra.root : {K : Type u_2} →
  {L : Type u_3} →
    [inst : LieRing L] →
      [inst_1 : Field K] →
        [inst_2 : LieAlgebra K L] →
          [FiniteDimensional K L] →
            {H : LieSubalgebra K L} → [inst_4 : H.IsCartanSubalgebra] → Finset (LieModule.Weight K (↥H) L)
-- Init.Data.UInt.Lemmas
USize.toNat_ofNat : ∀ {n : ℕ}, (OfNat.ofNat n).toNat = n % 2 ^ System.Platform.numBits
-- Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Measurable.complex_ofReal : ∀ {α : Type u_1} {m : MeasurableSpace α} {f : α → ℝ}, Measurable f → Measurable fun x => ↑(f x)
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
/-- The cokernel of a morphism, expressed as the coequalizer with the 0 morphism.  -/
CategoryTheory.Limits.cokernel : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} → (f : X ⟶ Y) → [CategoryTheory.Limits.HasCokernel f] → C
-- Mathlib.Algebra.Group.ForwardDiff
/-- Express the `n`-th forward difference of `f` at `y` in terms of the values `f (y + k)`, for
`0 ≤ k ≤ n`.
 -/
fwdDiff_iter_eq_sum_shift : ∀ {M : Type u_1} {G : Type u_2} [inst : AddCommMonoid M] [inst_1 : AddCommGroup G] (h : M) (f : M → G) (n : ℕ) (y : M),
  (fwdDiff h)^[n] f y = ∑ k ∈ Finset.range (n + 1), ((-1) ^ (n - k) * ↑(n.choose k)) • f (y + k • h)
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
SimpleGraph.IsEdgeReachable.zero : ∀ {V : Type u_1} {G : SimpleGraph V} {u v : V}, G.IsEdgeReachable 0 u v
-- Mathlib.AlgebraicTopology.SimplicialCategory.Basic
/-- A simplicial category is a category `C` that is enriched over the
category of simplicial sets in such a way that morphisms in
`C` identify to the `0`-simplices of the enriched hom.  -/
CategoryTheory.SimplicialCategory : (C : Type u) → [CategoryTheory.Category.{v, u} C] → Type (max (max u (v + 1)) v)
-- Mathlib.Geometry.Manifold.PartitionOfUnity
/-- A `SmoothPartitionOfUnity` that consists of a single function, uniformly equal to one,
defined as an example for `Inhabited` instance.  -/
SmoothPartitionOfUnity.single : {ι : Type uι} →
  {E : Type uE} →
    [inst : NormedAddCommGroup E] →
      [inst_1 : NormedSpace ℝ E] →
        {H : Type uH} →
          [inst_2 : TopologicalSpace H] →
            (I : ModelWithCorners ℝ E H) →
              {M : Type uM} →
                [inst_3 : TopologicalSpace M] →
                  [inst_4 : ChartedSpace H M] → ι → (s : Set M) → SmoothPartitionOfUnity ι I M s
-- Mathlib.Algebra.Ring.Defs
NonAssocCommRing.toNonAssocRing : {α : Type u} → [self : NonAssocCommRing α] → NonAssocRing α
-- Mathlib.Data.Int.WithZero
WithZeroMulInt.toNNReal_eq_one_iff : ∀ {e : NNReal} (m : WithZero (Multiplicative ℤ)) (he0 : e ≠ 0), e ≠ 1 → ((WithZeroMulInt.toNNReal he0) m = 1 ↔ m = 1)
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.piecewise_target : ∀ {α : Type u_1} {β : Type u_2} (e e' : PartialEquiv α β) (s : Set α) (t : Set β) [inst : (x : α) → Decidable (x ∈ s)]
  [inst_1 : (y : β) → Decidable (y ∈ t)] (H : e.IsImage s t) (H' : e'.IsImage s t),
  (e.piecewise e' s t H H').target = t.ite e.target e'.target
-- Mathlib.Topology.Algebra.Ring.Basic
RingTopology.instCompleteLattice : {R : Type u_1} → [inst : Ring R] → CompleteLattice (RingTopology R)
-- Mathlib.Control.Traversable.Instances
List.traverse.eq_def : ∀ {F : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Applicative F] (f : α → F β) (x : List α),
  List.traverse f x =
    match x with
    | [] => pure []
    | x :: xs => List.cons <$> f x <*> List.traverse f xs
-- Lean.Meta.Tactic.Simp.Arith.Int.Basic
Lean.Meta.Simp.Arith.Int.ToLinear.M : Type → Type