mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.PushoutProduct
/-- If `C` is a CCC with pushouts and an initial object, then `X □ (⊥_ C ⟶ 𝟙_ C) ≅ X`.  -/
CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.rightUnitor : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasPushouts C] →
      [inst_2 : CategoryTheory.CartesianMonoidalCategory C] →
        [CategoryTheory.MonoidalClosed C] →
          [inst_4 : CategoryTheory.Limits.HasInitial C] →
            (X : CategoryTheory.Arrow C) →
              (X □
                  CategoryTheory.Arrow.mk
                    (CategoryTheory.Limits.initial.to (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))) ≅
                X
-- Mathlib.Data.DFinsupp.BigOperators
DFinsupp.prod_mapRange_index : ∀ {ι : Type u} {γ : Type w} [inst : DecidableEq ι] {β₁ : ι → Type v₁} {β₂ : ι → Type v₂}
  [inst_1 : (i : ι) → Zero (β₁ i)] [inst_2 : (i : ι) → Zero (β₂ i)] [inst_3 : (i : ι) → (x : β₁ i) → Decidable (x ≠ 0)]
  [inst_4 : (i : ι) → (x : β₂ i) → Decidable (x ≠ 0)] [inst_5 : CommMonoid γ] {f : (i : ι) → β₁ i → β₂ i}
  {hf : ∀ (i : ι), f i 0 = 0} {g : Π₀ (i : ι), β₁ i} {h : (i : ι) → β₂ i → γ},
  (∀ (i : ι), h i 0 = 1) → (DFinsupp.mapRange f hf g).prod h = g.prod fun i b => h i (f i b)
-- Mathlib.RingTheory.MvPowerSeries.Inverse
/-- A multivariate formal power series is invertible if the constant coefficient is invertible.  -/
MvPowerSeries.invOfUnit : {σ : Type u_1} → {R : Type u_2} → [inst : Ring R] → MvPowerSeries σ R → Rˣ → MvPowerSeries σ R
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
/-- The orthogonal projection sends elements of `K` to themselves.  -/
Submodule.orthogonalProjectionOnto_mem_subspace_eq_self : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {K : Submodule 𝕜 E} [inst_3 : K.HasOrthogonalProjection] (v : ↥K), K.orthogonalProjectionOnto ↑v = v
-- Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Submodule.exists_fun_fin_finrank_span_eq : ∀ (K : Type u_2) {M : Type u_3} [inst : DivisionRing K] [inst_1 : AddCommGroup M] [inst_2 : Module K M] (s : Set M)
  [Module.Finite K ↥(Submodule.span K s)],
  ∃ f,
    (∀ (i : Fin (Module.finrank K ↥(Submodule.span K s))), f i ∈ s) ∧
      Submodule.span K (Set.range f) = Submodule.span K s ∧ LinearIndependent K f
-- Mathlib.Geometry.Euclidean.Sphere.Basic
/-- Given three collinear points, two on a sphere and one inside it, the one inside it is
strictly between the other two points.  -/
EuclideanGeometry.sbtw_of_collinear_of_dist_center_lt_radius : ∀ {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 : EuclideanGeometry.Sphere P} {p₁ p₂ p₃ : P},
  Collinear ℝ {p₁, p₂, p₃} → p₁ ∈ s → dist p₂ s.center < s.radius → p₃ ∈ s → p₁ ≠ p₃ → Sbtw ℝ p₁ p₂ p₃
-- Mathlib.MeasureTheory.Measure.ProbabilityMeasure
/-- The characterization of weak convergence of probability measures by the usual (defining)
condition that the integrals of every continuous bounded function converge to the integral of the
function against the limit measure.  -/
MeasureTheory.ProbabilityMeasure.tendsto_iff_forall_integral_tendsto : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω] [inst_2 : OpensMeasurableSpace Ω]
  {γ : Type u_2} {F : Filter γ} {μs : γ → MeasureTheory.ProbabilityMeasure Ω} {μ : MeasureTheory.ProbabilityMeasure Ω},
  Filter.Tendsto μs F (nhds μ) ↔
    ∀ (f : BoundedContinuousFunction Ω ℝ),
      Filter.Tendsto (fun i => ∫ (ω : Ω), f ω ∂↑(μs i)) F (nhds (∫ (ω : Ω), f ω ∂↑μ))
-- Mathlib.NumberTheory.Height.Basic
Height.one_le_mulHeight : ∀ {K : Type u_1} [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K] {ι : Type u_2} [Finite ι] (x : ι → K),
  1 ≤ Height.mulHeight x
-- Init.Data.Range.Polymorphic.UInt
UInt64.instUpwardEnumerable : Std.PRange.UpwardEnumerable UInt64
-- Mathlib.Algebra.Category.Ring.FilteredColimits
SemiRingCat.FilteredColimits.colimitCoconeIsColimit.descAddMonoidHom_quotMk : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J SemiRingCat}
  [inst_1 : CategoryTheory.IsFiltered J] (t : CategoryTheory.Limits.Cocone F) {j : J} (x : ↑(F.obj j)),
  (SemiRingCat.FilteredColimits.colimitCoconeIsColimit.descAddMonoidHom t)
      (Quot.mk ((F.comp (CategoryTheory.forget₂ SemiRingCat MonCat)).comp (CategoryTheory.forget MonCat)).ColimitTypeRel
        ⟨j, x⟩) =
    (CategoryTheory.ConcreteCategory.hom (t.ι.app j)) x
-- Mathlib.RingTheory.TensorProduct.MvPolynomial
MvPolynomial.algebraTensorAlgEquiv_symm_X : ∀ (R : Type u) [inst : CommSemiring R] {σ : Type u_1} (A : Type u_4) [inst_1 : CommSemiring A] [inst_2 : Algebra R A]
  (s : σ), (MvPolynomial.algebraTensorAlgEquiv R A).symm (MvPolynomial.X s) = 1 ⊗ₜ[R] MvPolynomial.X s
-- Mathlib.CategoryTheory.Limits.VanKampen
CategoryTheory.IsVanKampenColimit.isUniversal : ∀ {J : Type v'} [inst : CategoryTheory.Category.{u', v'} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cocone F},
  CategoryTheory.IsVanKampenColimit c → CategoryTheory.IsUniversalColimit c
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.NeWord.mulHead.congr_simp : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] {i j : ι} (w w_1 : Monoid.CoprodI.NeWord M i j)
  (e_w : w = w_1) (x x_1 : M i) (e_x : x = x_1) (hnotone : x * w.head ≠ 1), w.mulHead x hnotone = w_1.mulHead x_1 ⋯
-- Mathlib.ModelTheory.Algebra.Ring.Basic
FirstOrder.Ring.one_def : ∀ (α : Type u_2), 1 = FirstOrder.Language.Constants.term FirstOrder.Ring.oneFunc
-- Mathlib.Combinatorics.Matroid.Sum
_private.Mathlib.Combinatorics.Matroid.Sum.0.Equiv.sumEquivSigmaBool.match_1.eq_1 : ∀ (α β : Type u_1) (motive : ((b : Bool) × bif b then β else α) → Sort u_2) (a : bif false then β else α)
  (h_1 : (a : bif false then β else α) → motive ⟨false, a⟩) (h_2 : (b : bif true then β else α) → motive ⟨true, b⟩),
  (match ⟨false, a⟩ with
    | ⟨false, a⟩ => h_1 a
    | ⟨true, b⟩ => h_2 b) =
    h_1 a
-- Init.Data.Option.Lemmas
Option.getD_guard : ∀ {α : Type u_1} {p : α → Bool} {a b : α}, (Option.guard p a).getD b = if p a = true then a else b
-- Init.Data.SInt.Lemmas
Int64.toInt_ofIntClamp : ∀ {x : ℤ}, Int64.minValue.toInt ≤ x → x ≤ Int64.maxValue.toInt → (Int64.ofIntClamp x).toInt = x
-- Mathlib.MeasureTheory.Group.FoelnerFilter
isFoelner_maxFoelner : ∀ (G : Type u_1) {X : Type u_2} [inst : MeasurableSpace X] (μ : MeasureTheory.Measure X) [inst_1 : Group G]
  [inst_2 : MulAction G X], IsFoelner G μ (maxFoelner G μ) id
-- Mathlib.Logic.Equiv.Embedding
_private.Mathlib.Logic.Equiv.Embedding.0.Equiv.sumEmbeddingEquivProdEmbeddingDisjoint.match_1.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (motive : α ⊕ β → Sort u_3) (a : α) (h_1 : (a : α) → motive (Sum.inl a))
  (h_2 : (b : β) → motive (Sum.inr b)),
  (match Sum.inl a with
    | Sum.inl a => h_1 a
    | Sum.inr b => h_2 b) =
    h_1 a
-- Mathlib.MeasureTheory.Measure.Real
/-- **Alias** of `MeasureTheory.le_measureReal_sdiff`. -/
MeasureTheory.le_measureReal_diff : ∀ {α : Type u_1} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s₁ s₂ : Set α},
  autoParam (μ s₂ ≠ ⊤) MeasureTheory.le_measureReal_sdiff._auto_1 → μ.real s₁ - μ.real s₂ ≤ μ.real (s₁ \ s₂)
-- Mathlib.Data.Sym.Sym2
/-- For a relation homomorphism `r →r r'` where `r` is symmetric, the `fromRel` set of `r` is
equivalent to summing that set restricted to equivalence classes of `r'` using a `Subtype`,
`Quot` version  -/
Equiv.sigmaQuotFromRel : {α : Type u_1} →
  {β : Type u_2} →
    {r : α → α → Prop} →
      (sym : Std.Symm r) → {r' : β → β → Prop} → (f : r →r r') → ↑(Sym2.fromRel sym) ≃ (q : Quot r') × ↑(Sym2.fromRel ⋯)
-- Mathlib.Analysis.Complex.CanonicalDecomposition
/-- Canonical factors are meromorphic.
 -/
Complex.meromorphic_canonicalFactor : ∀ (R : ℝ) (w : ℂ), Meromorphic (Complex.canonicalFactor R w)
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks
CategoryTheory.Limits.PreservesPullback.iso_inv_snd : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst_2 : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) G]
  [inst_3 : CategoryTheory.Limits.HasPullback f g] [inst_4 : CategoryTheory.Limits.HasPullback (G.map f) (G.map g)],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PreservesPullback.iso G f g).inv
      (G.map (CategoryTheory.Limits.pullback.snd f g)) =
    CategoryTheory.Limits.pullback.snd (G.map f) (G.map g)
-- Mathlib.Analysis.Real.Sqrt
ContinuousOn.sqrt : ∀ {α : Type u_1} [inst : TopologicalSpace α] {f : α → ℝ} {s : Set α},
  ContinuousOn f s → ContinuousOn (fun x => √(f x)) s
-- Mathlib.Analysis.Normed.Group.Seminorm
AddGroupSeminorm.funLike : {E : Type u_3} → [inst : AddGroup E] → FunLike (AddGroupSeminorm E) E ℝ
-- Mathlib.Algebra.Group.Even
IsSquare.zpow : ∀ {α : Type u_2} [inst : DivisionMonoid α] {a : α} (n : ℤ), IsSquare a → IsSquare (a ^ n)
-- Mathlib.Algebra.Algebra.Pi
/-- A family of algebra homomorphisms `g i : B →ₐ[R] A i` defines an algebra homomorphism
`AlgHom.pi g : B →ₐ[R] Π i, A i` given by `AlgHom.pi g x i = g i x`.  -/
AlgHom.pi : {ι : Type u_1} →
  {R : Type u_2} →
    {A : ι → Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : (i : ι) → Semiring (A i)] →
          [inst_2 : (i : ι) → Algebra R (A i)] →
            {B : Type u_4} →
              [inst_3 : Semiring B] → [inst_4 : Algebra R B] → ((i : ι) → B →ₐ[R] A i) → B →ₐ[R] (i : ι) → A i
-- Aesop.Tree.TreeM
Aesop.TreeM.instMonad : Monad Aesop.TreeM
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.AddMonObj.instIsAddMonHomZero : ∀ {D : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} D] [inst_1 : CategoryTheory.SemiCartesianMonoidalCategory D]
  (M : D) [inst_2 : CategoryTheory.AddMonObj M], CategoryTheory.IsAddMonHom CategoryTheory.AddMonObj.zero
-- Init.Data.List.Monadic
List.flatMapM.loop.eq_1 : ∀ {m : Type u → Type v} [inst : Monad m] {α : Type w} {β : Type u} (f : α → m (List β)) (x : List (List β)),
  List.flatMapM.loop f [] x = pure x.reverse.flatten
-- Mathlib.Combinatorics.Matroid.Minor.Contract
Matroid.IsNonloop.of_contract : ∀ {α : Type u_1} {M : Matroid α} {e : α} {C : Set α}, (M.contract C).IsNonloop e → M.IsNonloop e
-- Mathlib.Analysis.Calculus.Deriv.Add
/-- Eta-expanded form of `deriv.neg'` -/
deriv.fun_neg' : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F}, (deriv fun i => -f i) = fun x => -deriv f x
-- Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
HurwitzKernelBounds.summable_f_nat : ∀ (k : ℕ) (a : ℝ) {t : ℝ}, 0 < t → Summable (HurwitzKernelBounds.f_nat k a t)
-- Mathlib.Algebra.EuclideanDomain.Defs
/-- Abbreviated notation for the well-founded relation `r` in a Euclidean domain.  -/
_private.Mathlib.Algebra.EuclideanDomain.Defs.0.EuclideanDomain.«term_≺_» : Lean.TrailingParserDescr
-- Mathlib.Combinatorics.SimpleGraph.UnitDistance.Basic
SimpleGraph.UnitDistEmbedding.copy_p_apply : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} {E : Type u_3} [inst : MetricSpace E]
  (U : G.UnitDistEmbedding E) (f : H.Copy G) (a : W), (U.copy f).p a = U.p (f.toEmbedding a)
-- Mathlib.Order.Cover
CovBy.le : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, a ⋖ b → a ≤ b
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instGroup : {α : Type u_1} → {l : Filter α} → {G : Type u_6} → [Group G] → Group (l.Germ G)
-- Lean.Compiler.IR.Basic
Lean.IR.FnBody.jmp.inj : ∀ {j : Lean.IR.JoinPointId} {ys : Array Lean.IR.Arg} {j_1 : Lean.IR.JoinPointId} {ys_1 : Array Lean.IR.Arg},
  Lean.IR.FnBody.jmp j ys = Lean.IR.FnBody.jmp j_1 ys_1 → j = j_1 ∧ ys = ys_1
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
/-- Half of **Jordan's inequality** for `cos` and negative values.  -/
Real.one_add_mul_le_cos : ∀ {x : ℝ}, -(Real.pi / 2) ≤ x → x ≤ 0 → 1 + 2 / Real.pi * x ≤ Real.cos x
-- Std.Data.DHashMap.Raw
Std.DHashMap.Raw.WF.getThenInsertIfNew? : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α] {m : Std.DHashMap.Raw α β}
  {a : α} {b : β a}, m.WF → (m.getThenInsertIfNew? a b).2.WF
-- Lean.Message
/-- Stop time in seconds; 0 if unknown to avoid `Option` allocation.  -/
Lean.TraceData.stopTime : Lean.TraceData → Float
-- Mathlib.LinearAlgebra.Transvection.Basic
LinearEquiv.transvection.of_left_eq_zero : ∀ {R : Type u_1} {V : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup V] [inst_2 : Module R V] (v : V)
  (hv : optParam (0 v = 0) ⋯), LinearEquiv.transvection hv = LinearEquiv.refl R V
-- Mathlib.Tactic.CategoryTheory.ToApp
Mathlib.Tactic.CategoryTheory.ToApp.toNatTrans_congr : ∀ {C D : CategoryTheory.Cat} {F G : C ⟶ D} {η θ : F ⟶ G}, η = θ → η.toNatTrans = θ.toNatTrans
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddResult
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.insertUnitInvariant_insertRupUnits : ∀ {n : ℕ} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (f_readyForRupAdd : f.ReadyForRupAdd)
  (units : Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)),
  let assignments := (f.insertRupUnits units).1.assignments;
  have hsize := ⋯;
  have rupUnits := (f.insertRupUnits units).1.rupUnits;
  Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.InsertUnitInvariant f.assignments ⋯ rupUnits assignments hsize
-- Mathlib.Tactic.NormNum.Result
Mathlib.Meta.NormNum.IsNNRat.to_raw_eq : ∀ {α : Type u} {n d : ℕ} [inst : DivisionSemiring α] {a : α}, Mathlib.Meta.NormNum.IsNNRat a n d → a = NNRat.rawCast n d
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.subtypeClosure.eq_1 : ∀ {α : Type u_2} (M : Matroid α), M.subtypeClosure = ClosureOperator.ofCompletePred (fun F => M.IsFlat ↑F) ⋯
-- Mathlib.Analysis.Meromorphic.NormalForm
/-- If `f` is not meromorphic on `U`, conversion to normal form maps the function
to `0`.
 -/
toMeromorphicNFOn_of_not_meromorphicOn : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {U : Set 𝕜}, ¬MeromorphicOn f U → toMeromorphicNFOn f U = 0
-- Mathlib.Algebra.AddConstMap.Basic
AddConstMapClass.map_const_add : ∀ {F : Type u_1} {G : Type u_2} {H : Type u_3} [inst : FunLike F G H] {a : G} {b : H} [inst_1 : AddCommMagma G]
  [inst_2 : Add H] [AddConstMapClass F G H a b] (f : F) (x : G), f (a + x) = f x + b
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.commMap_apply_of_isReal : ∀ (K : Type u_1) [inst : Field K] (x : (K →+* ℂ) → ℂ) {w : NumberField.InfinitePlace K} (hw : w.IsReal),
  ((NumberField.mixedEmbedding.commMap K) x).1 ⟨w, hw⟩ = (x w.embedding).re
-- Init.Data.Range.Polymorphic.RangeIterator
Std.Rxo.Iterator.instProductive : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : LT α] [inst_2 : DecidableLT α]
  [Std.PRange.LawfulUpwardEnumerable α], Std.Iterators.Productive (Std.Rxo.Iterator α) Id
-- Mathlib.CategoryTheory.Monoidal.ExternalProduct.Basic
/-- Notation for `externalProduct`.
Do `open scoped CategoryTheory.MonoidalCategory.ExternalProduct`
to bring this notation in scope.  -/
CategoryTheory.MonoidalCategory.ExternalProduct.«term_⊠_» : Lean.TrailingParserDescr
-- Mathlib.Data.QPF.Multivariate.Constructions.Comp
/-- The composition of functors is itself functorial  -/
MvQPF.Comp.map : {n m : ℕ} →
  {F : TypeVec.{u} n → Type u_1} →
    {G : Fin2 n → TypeVec.{u} m → Type u} →
      {α β : TypeVec.{u} m} →
        α.Arrow β → [MvFunctor F] → [(i : Fin2 n) → MvFunctor (G i)] → MvQPF.Comp F G α → MvQPF.Comp F G β
-- Mathlib.Data.Nat.Log
Nat.log_anti_left : ∀ {b c n : ℕ}, 1 < c → c ≤ b → Nat.log b n ≤ Nat.log c n
-- Mathlib.Order.Quotient
Quotient.instLinearOrder : {α : Type u_1} →
  {s : Setoid α} →
    [inst : LinearOrder α] →
      [H : ∀ (x : Quotient s), (Quotient.mk s ⁻¹' {x}).OrdConnected] →
        [DecidableRel fun x1 x2 => x1 ≈ x2] → LinearOrder (Quotient s)
-- Lean.Meta.Tactic.Induction
_private.Lean.Meta.Tactic.Induction.0.Lean.Meta.throwUnexpectedMajorType : {α : Type} → Lean.Name → Lean.MVarId → Lean.Expr → Lean.MetaM α
-- Mathlib.Algebra.Category.ModuleCat.Basic
ModuleCat.hasForgetToAddCommGroup : (R : Type u) → [inst : Ring R] → CategoryTheory.HasForget₂ (ModuleCat R) AddCommGrpCat
-- Mathlib.Algebra.MvPolynomial.Division
_private.Mathlib.Algebra.MvPolynomial.Division.0.MvPolynomial.«term_%ᵐᵒⁿᵒᵐⁱᵃˡ__1» : Lean.TrailingParserDescr
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.getD_inter : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k fallback : α},
  (t₁ ∩ t₂).getD k fallback = if k ∈ t₂ then t₁.getD k fallback else fallback
-- Mathlib.FieldTheory.RatFunc.IntermediateField
RatFunc.natDegree_num_le_natDegree_minpolyX : ∀ {K : Type u_1} [inst : Field K] (f : RatFunc K),
  (¬∃ c, f = RatFunc.C c) → f.num.natDegree ≤ (f.minpolyX ↥K⟮f⟯).natDegree
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
/-- Normalised Eisenstein series of even weight `k ≥ 3` are non-zero.  -/
EisensteinSeries.E_ne_zero : ∀ {k : ℕ} (hk : 3 ≤ k), Even k → ModularForm.E hk ≠ 0
-- Mathlib.CategoryTheory.Join.Basic
CategoryTheory.Join.instCategory : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        CategoryTheory.Category.{max v₁ v₂, max u₂ u₁} (CategoryTheory.Join C D)
-- Mathlib.Algebra.Module.Submodule.Lattice
AddSubgroup.coe_toIntSubmodule : ∀ {M : Type u_3} [inst : AddCommGroup M] (S : AddSubgroup M), ↑(AddSubgroup.toIntSubmodule S) = ↑S
-- Std.Data.Internal.List.Associative
Std.Internal.List.maxKey_eraseKey_le_maxKey : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] [inst_2 : BEq α] [inst_3 : Std.LawfulBEqOrd α]
  {l : List ((a : α) × β a)} (hd : Std.Internal.List.DistinctKeys l) {k : α}
  {he : (Std.Internal.List.eraseKey k l).isEmpty = false},
  (compare (Std.Internal.List.maxKey (Std.Internal.List.eraseKey k l) he) (Std.Internal.List.maxKey l ⋯)).isLE = true
-- Mathlib.AlgebraicGeometry.Gluing
AlgebraicGeometry.Scheme.Cover.isOpenMap_fromGlued : ∀ {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover), IsOpenMap ⇑(AlgebraicGeometry.Scheme.Cover.fromGlued 𝒰)
-- Mathlib.GroupTheory.RegularWreathProduct
RegularWreathProduct.instInv : {D : Type u_1} → {Q : Type u_2} → [Group D] → [Group Q] → Inv (D ≀ᵣ Q)
-- Mathlib.Topology.MetricSpace.MetricSeparated
Metric.AreSeparated.mono_right : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] {s t t' : Set X},
  Metric.AreSeparated s t' → t ⊆ t' → Metric.AreSeparated s t
-- Aesop.Util.OrderedHashSet
Aesop.OrderedHashSet.contains : {α : Type u_1} → [inst : BEq α] → [inst_1 : Hashable α] → α → Aesop.OrderedHashSet α → Bool
-- Mathlib.AlgebraicTopology.DoldKan.Equivalence
CategoryTheory.Abelian.DoldKan.equivalence_functor : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] [inst_1 : CategoryTheory.Abelian A],
  CategoryTheory.Abelian.DoldKan.equivalence.functor = CategoryTheory.Abelian.DoldKan.N
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.instSliceableImplRocSlice : {α : Type u} →
  {β : α → Type v} →
    [inst : Ord α] → Std.Roc.Sliceable (Std.DTreeMap.Internal.Impl α β) α (Std.DTreeMap.Internal.RocSlice α β)
-- Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity
/-- The number of times an irreducible factor `p` appears in `normalizedFactors x` is defined by
the number of times it divides `x`. This is a slightly more general version of
`UniqueFactorizationMonoid.count_normalizedFactors_eq` that allows `p = 0`.

See also `multiplicity_eq_count_normalizedFactors` if `n` is given by `multiplicity p x`.
 -/
UniqueFactorizationMonoid.count_normalizedFactors_eq' : ∀ {R : Type u_2} [inst : CommMonoidWithZero R] [inst_1 : UniqueFactorizationMonoid R] [inst_2 : NormalizationMonoid R]
  [inst_3 : DecidableEq R] {p x : R},
  p = 0 ∨ Irreducible p →
    normalize p = p →
      ∀ {n : ℕ}, p ^ n ∣ x → ¬p ^ (n + 1) ∣ x → Multiset.count p (UniqueFactorizationMonoid.normalizedFactors x) = n
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap.0.Std.IterM.toList_filterMapWithPostcondition_filterMapWithPostcondition.match_1.eq_2 : ∀ {γ : Type u_1} (motive : Option γ → Sort u_2) (fb : γ) (h_1 : Unit → motive none) (h_2 : (fb : γ) → motive (some fb)),
  (match some fb with
    | none => h_1 ()
    | some fb => h_2 fb) =
    h_2 fb
-- Mathlib.Topology.MetricSpace.IsometricSMul
Metric.vadd_closedBall : ∀ {G : Type v} {X : Type w} [inst : PseudoMetricSpace X] [inst_1 : AddGroup G] [inst_2 : AddAction G X]
  [IsIsometricVAdd G X] (c : G) (x : X) (r : ℝ), c +ᵥ Metric.closedBall x r = Metric.closedBall (c +ᵥ x) r
-- Mathlib.Algebra.MvPolynomial.Rename
MvPolynomial.eval₂_rename_prod_mk : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_4} {S : Type u_5} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  (f : R →+* S) (g : σ × τ → S) (i : σ) (p : MvPolynomial τ R),
  MvPolynomial.eval₂ f g ((MvPolynomial.rename (Prod.mk i)) p) = MvPolynomial.eval₂ f (fun j => g (i, j)) p
-- Mathlib.Analysis.Fourier.Notation
FourierModule.fourier_smul : ∀ {R : Type u_5} {E : Type u_6} {F : outParam (Type u_7)} [inst : Add E] [inst_1 : Add F] [inst_2 : SMul R E]
  [inst_3 : SMul R F] (self : FourierModule R E F) (r : R) (f : E),
  FourierTransform.fourier (r • f) = r • FourierTransform.fourier f
-- Mathlib.Algebra.Quandle
/-- The operation for the dihedral quandle.  It does not need to be an equivalence
because it is an involution (see `dihedralAct.inv`).  -/
Quandle.dihedralAct : (n : ℕ) → ZMod n → ZMod n → ZMod n
-- Mathlib.CategoryTheory.Limits.Opposites
CategoryTheory.Limits.isColimitCoconeOfConeRightOp_desc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} J]
  (F : CategoryTheory.Functor Jᵒᵖ C) {c : CategoryTheory.Limits.Cone F.rightOp} (hc : CategoryTheory.Limits.IsLimit c)
  (s : CategoryTheory.Limits.Cocone F),
  (CategoryTheory.Limits.isColimitCoconeOfConeRightOp F hc).desc s =
    (hc.lift (CategoryTheory.Limits.coneRightOpOfCocone s)).unop
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.forM_eq_forM_keys : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} {m' : Type w → Type w'}
  [inst_2 : Monad m'] [LawfulMonad m'], m.WF → ∀ {f : α → m' PUnit.{w + 1}}, (forM m fun a => f a.fst) = m.keys.forM f
-- Mathlib.Tactic.Translate.Core
/-- A map specifying the binder names of the translated declaration.  -/
Mathlib.Tactic.Translate.Config.rename : Mathlib.Tactic.Translate.Config → Lean.NameMap Lean.Name
-- Mathlib.CategoryTheory.GlueData
CategoryTheory.GlueData'.f_hasPullback : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v, u₁} C] (self : CategoryTheory.GlueData' C) (i j k : self.J)
  (hij : i ≠ j) (hik : i ≠ k), CategoryTheory.Limits.HasPullback (self.f i j hij) (self.f i k hik)
-- Mathlib.Control.Bitraversable.Instances
Sum.bitraverse.eq_1 : ∀ {F : Type u → Type u} [inst : Applicative F] {α : Type u_1} {α' : Type u} {β : Type u_2} {β' : Type u} (f : α → F α')
  (f' : β → F β') (x_1 : α), Sum.bitraverse f f' (Sum.inl x_1) = Sum.inl <$> f x_1
-- Init.Data.Range.Polymorphic.PRange
Std.Rcc.LawfulRcoIntersection.mk : ∀ {α : Type w} [inst : LT α] [inst_1 : LE α] [inst_2 : Std.Rcc.HasRcoIntersection α],
  (∀ {a : α} {r : Std.Rcc α} {s : Std.Rco α}, a ∈ Std.Rcc.HasRcoIntersection.intersection r s ↔ a ∈ r ∧ a ∈ s) →
    Std.Rcc.LawfulRcoIntersection α
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
/-- Eta-expanded form of `TendstoUniformlyOn.mul` -/
TendstoUniformlyOn.fun_mul : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : Group α] [IsUniformGroup α] {ι : Type u_3}
  {l : Filter ι} {f f' : ι → β → α} {g g' : β → α} {s : Set β},
  TendstoUniformlyOn f g l s →
    TendstoUniformlyOn f' g' l s → TendstoUniformlyOn (fun i i_1 => f i i_1 * f' i i_1) (fun i => g i * g' i) l s