mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor
CategoryTheory.Functor.LaxRightLinear.μᵣ_naturality_left_assoc : ∀ {D : Type u_1} {D' : Type u_2} {inst : CategoryTheory.Category.{v_1, u_1} D}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} D'} (F : CategoryTheory.Functor D D') {C : Type u_3}
  {inst_2 : CategoryTheory.Category.{v_3, u_3} C} {inst_3 : CategoryTheory.MonoidalCategory C}
  {inst_4 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D}
  {inst_5 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D'} [self : F.LaxRightLinear C] {d d' : D}
  (f : d ⟶ d') (c : C) {Z : D'}
  (h : F.obj (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj d' c) ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft (F.map f) c)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxRightLinear.μᵣ F d' c) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxRightLinear.μᵣ F d c)
      (CategoryTheory.CategoryStruct.comp
        (F.map (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft f c)) h)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKey?_ofList_of_mem : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} [EquivBEq α] [LawfulHashable α]
  {l : List ((a : α) × β a)} {k k' : α},
  (k == k') = true →
    List.Pairwise (fun a b => (a.fst == b.fst) = false) l →
      k ∈ List.map Sigma.fst l → (Std.DHashMap.ofList l).getKey? k' = some k
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplexOne
SSet.stdSimplex.σ_objMk₁_of_lt : ∀ {n : ℕ} (i : Fin (n + 2)) (j : Fin (n + 1)),
  j.castSucc < i →
    (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.σ (SSet.stdSimplex.obj { len := 1 }) j))
        (SSet.stdSimplex.objMk₁ i) =
      SSet.stdSimplex.objMk₁ i.succ
-- Lean.Parser.Basic
Lean.Parser.PrattParsingTables.mk.inj : ∀ {leadingTable : Lean.Parser.TokenMap (Lean.Parser.Parser × ℕ)} {leadingParsers : List (Lean.Parser.Parser × ℕ)}
  {trailingTable : Lean.Parser.TokenMap (Lean.Parser.Parser × ℕ)} {trailingParsers : List (Lean.Parser.Parser × ℕ)}
  {leadingTable_1 : Lean.Parser.TokenMap (Lean.Parser.Parser × ℕ)} {leadingParsers_1 : List (Lean.Parser.Parser × ℕ)}
  {trailingTable_1 : Lean.Parser.TokenMap (Lean.Parser.Parser × ℕ)} {trailingParsers_1 : List (Lean.Parser.Parser × ℕ)},
  { leadingTable := leadingTable, leadingParsers := leadingParsers, trailingTable := trailingTable,
        trailingParsers := trailingParsers } =
      { leadingTable := leadingTable_1, leadingParsers := leadingParsers_1, trailingTable := trailingTable_1,
        trailingParsers := trailingParsers_1 } →
    leadingTable = leadingTable_1 ∧
      leadingParsers = leadingParsers_1 ∧ trailingTable = trailingTable_1 ∧ trailingParsers = trailingParsers_1
-- Mathlib.Analysis.Meromorphic.TrailingCoefficient
/-- If `f` is meromorphic at `x`, then the trailing coefficient of `f` at `x` is the limit of the
function `(· - x) ^ (-order) • f`.
 -/
MeromorphicAt.tendsto_nhds_meromorphicTrailingCoeffAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜},
  MeromorphicAt f x →
    Filter.Tendsto ((fun x_1 => x_1 - x) ^ (-(meromorphicOrderAt f x).untop₀) • f) (nhdsWithin x {x}ᶜ)
      (nhds (meromorphicTrailingCoeffAt f x))
-- ProofWidgets.Data.Html
ProofWidgets.Html.component.injEq : ∀ (a : UInt64) (a_1 : String) (a_2 : ProofWidgets.LazyEncodable Lean.Json) (a_3 : Array ProofWidgets.Html)
  (a_4 : UInt64) (a_5 : String) (a_6 : ProofWidgets.LazyEncodable Lean.Json) (a_7 : Array ProofWidgets.Html),
  (ProofWidgets.Html.component a a_1 a_2 a_3 = ProofWidgets.Html.component a_4 a_5 a_6 a_7) =
    (a = a_4 ∧ a_1 = a_5 ∧ a_2 = a_6 ∧ a_3 = a_7)
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.SummableFamily.instNeg : {Γ : Type u_1} →
  {R : Type u_3} →
    {α : Type u_5} → [inst : PartialOrder Γ] → [inst_1 : AddCommGroup R] → Neg (HahnSeries.SummableFamily Γ R α)
-- Mathlib.NumberTheory.RamificationInertia.Unramified
/-- Let `S` be a Dedekind domain that is integral and torsion-free over a characteristic-zero
domain `R`. Then an ideal `p` of `R` is unramified in `S` if and only if `S` is unramified at every
maximal ideal `P` of `S` lying over `p`.  -/
Algebra.isUnramifiedIn_iff_forall_of_isDedekindDomain : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [IsDomain R]
  [IsDedekindDomain S] [Module.IsTorsionFree R S] [CharZero R] [Algebra.IsIntegral R S] {p : Ideal R},
  Algebra.IsUnramifiedIn S p ↔ ∀ (P : Ideal S) (x : P.IsMaximal), P.LiesOver p → Algebra.IsUnramifiedAt R P
-- Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Associates.prod_top : ∀ {α : Type u_1} [inst : CommMonoidWithZero α], ⊤.prod = 0
-- Mathlib.CategoryTheory.Sums.Associator
CategoryTheory.sum.inrCompInrCompInverseAssociator.eq_1 : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (E : Type u₃) [inst_2 : CategoryTheory.Category.{v₃, u₃} E],
  CategoryTheory.sum.inrCompInrCompInverseAssociator C D E =
    (CategoryTheory.Sum.inr_ D E).isoWhiskerLeft (CategoryTheory.sum.inrCompInverseAssociator C D E) ≪≫
      ((CategoryTheory.Sum.inr_ C D).comp (CategoryTheory.Sum.inl_ (C ⊕ D) E)).inrCompSum'
        (CategoryTheory.Sum.inr_ (C ⊕ D) E)
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.WalkingMultispan.Hom.comp_eq_comp : ∀ {J : CategoryTheory.Limits.MultispanShape} {X Y Z : CategoryTheory.Limits.WalkingMultispan J} (f : X ⟶ Y) (g : Y ⟶ Z),
  CategoryTheory.Limits.WalkingMultispan.Hom.comp f g = CategoryTheory.CategoryStruct.comp f g
-- Mathlib.Data.Num.ZNum
_private.Mathlib.Data.Num.ZNum.0.PosNum.divMod.match_3.splitter : (motive : PosNum → Sort u_1) →
  (x : PosNum) → ((n : PosNum) → motive n.bit0) → ((n : PosNum) → motive n.bit1) → (Unit → motive PosNum.one) → motive x
-- Mathlib.Algebra.Algebra.Hom
AlgHom.toLinearMap_ofLinearMap : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (f : A →ₗ[R] B) (map_one : f 1 = 1)
  (map_mul : ∀ (x y : A), f (x * y) = f x * f y), (AlgHom.ofLinearMap f map_one map_mul).toLinearMap = f
-- Std.Internal.Parsec.Basic
Std.Internal.Parsec.Input.curr' : {ι : Type} →
  {elem idx : outParam Type} →
    {inst : DecidableEq idx} →
      {inst_1 : DecidableEq elem} →
        [self : Std.Internal.Parsec.Input ι elem idx] → (it : ι) → Std.Internal.Parsec.Input.hasNext it = true → elem
-- Mathlib.Topology.Spectral.Hom
SpectralMap.instFunLike : {α : Type u_2} →
  {β : Type u_3} → [inst : TopologicalSpace α] → [inst_1 : TopologicalSpace β] → FunLike (SpectralMap α β) α β
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate
SSet.toNormalizedChainComplex_fromNormalizedChainComplex_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasCoproducts C]
  [inst_2 : CategoryTheory.Preadditive C] (X : SSet) (R : C) {Z : ChainComplex C ℕ} (h : X.chainComplex R ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.toNormalizedChainComplex R)
      (CategoryTheory.CategoryStruct.comp (X.fromNormalizedChainComplex R) h) =
    CategoryTheory.CategoryStruct.comp AlgebraicTopology.DoldKan.PInfty h
-- Mathlib.LinearAlgebra.Ray
/-- Scaling by a negative unit is negation.  -/
Module.Ray.units_smul_of_neg : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] (u : Rˣ), ↑u < 0 → ∀ (v : Module.Ray R M), u • v = -v
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.cokernelBiprodInrIso_hom : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {X Y : C} [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y],
  CategoryTheory.Limits.cokernelBiprodInrIso.hom =
    CategoryTheory.Limits.colimit.desc (CategoryTheory.Limits.parallelPair CategoryTheory.Limits.biprod.inr 0)
      (CategoryTheory.Limits.biprod.inrCokernelCofork X Y)
-- Lean.Elab.Tactic.RCases
/-- A parenthesized expression, used for hovers  -/
Lean.Elab.Tactic.RCases.RCasesPatt.paren : Lean.Syntax → Lean.Elab.Tactic.RCases.RCasesPatt → Lean.Elab.Tactic.RCases.RCasesPatt
-- Mathlib.RingTheory.Localization.Away.Basic
IsLocalization.Away.isDomain : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Type u_2) [inst_1 : CommSemiring S] [inst_2 : Algebra R S] [IsDomain R]
  {x : R}, x ≠ 0 → ∀ [IsLocalization.Away x S], IsDomain S
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.HomEquiv.assoc : ∀ {C : Type u} {X Y U V : CategoryTheory.FreeMonoidalCategory C} (f : X.Hom U) (g : U.Hom V) (h : V.Hom Y),
  CategoryTheory.FreeMonoidalCategory.HomEquiv ((f.comp g).comp h) (f.comp (g.comp h))
-- Mathlib.LinearAlgebra.Matrix.Stochastic
/-- A matrix is column stochastic if each column sums to one.  -/
Matrix.mem_colStochastic_iff_sum : ∀ {R : Type u_1} {n : Type u_2} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : Semiring R]
  [inst_3 : PartialOrder R] [inst_4 : IsOrderedRing R] {M : Matrix n n R},
  M ∈ Matrix.colStochastic R n ↔ (∀ (i j : n), 0 ≤ M i j) ∧ ∀ (j : n), ∑ i, M i j = 1
-- Mathlib.Order.SuccPred.Archimedean
strictMonoOn_of_pred_lt : ∀ {α : Type u_3} {β : Type u_4} [inst : PartialOrder α] [inst_1 : Preorder β] [inst_2 : PredOrder α]
  [IsPredArchimedean α] {s : Set α} {f : α → β},
  s.OrdConnected → (∀ (a : α), ¬IsMin a → a ∈ s → Order.pred a ∈ s → f (Order.pred a) < f a) → StrictMonoOn f s
-- Mathlib.RingTheory.Smooth.Basic
/-- For a formally smooth `R`-algebra `A` and a map `f : A →ₐ[R] B ⧸ I` with `I` square-zero,
this is an arbitrary lift `A →ₐ[R] B`.  -/
Algebra.FormallySmooth.lift : {R : Type u} →
  {A : Type v} →
    [inst : CommRing R] →
      [inst_1 : CommRing A] →
        [inst_2 : Algebra R A] →
          {B : Type u_1} →
            [inst_3 : CommRing B] →
              [inst_4 : Algebra R B] →
                [Algebra.FormallySmooth R A] → (I : Ideal B) → IsNilpotent I → (A →ₐ[R] B ⧸ I) → A →ₐ[R] B
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.exists_ball_subset_ball : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x y : α} {ε : ℝ},
  y ∈ Metric.ball x ε → ∃ ε' > 0, Metric.ball y ε' ⊆ Metric.ball x ε
-- Init.Data.Bool
Bool.bne_not_self : ∀ (x : Bool), (x != !x) = true
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
AddMonoidAlgebra.mapDomainRingHom_apply : ∀ (R : Type u_3) {M : Type u_6} {N : Type u_7} [inst : Semiring R] [inst_1 : AddMonoid M] [inst_2 : AddMonoid N]
  (f : M →+ N) (x : AddMonoidAlgebra R M), (AddMonoidAlgebra.mapDomainRingHom R f) x = AddMonoidAlgebra.mapDomain (⇑f) x
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometryEquiv.constVAdd_zero : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_10} [inst : NormedField 𝕜] [inst_1 : SeminormedAddCommGroup V]
  [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P] [inst_4 : NormedAddTorsor V P],
  AffineIsometryEquiv.constVAdd 𝕜 P 0 = AffineIsometryEquiv.refl 𝕜 P
-- Mathlib.Tactic.NormNum.Result
Mathlib.Meta.NormNum.IsNNRat.den_nz : ∀ {α : Type u_1} [inst : DivisionSemiring α] {a : α} {n d : ℕ}, Mathlib.Meta.NormNum.IsNNRat a n d → ↑d ≠ 0
-- Init.System.IO
IO.instMinTaskState : Min IO.TaskState
-- Init.Data.Option.Lemmas
Option.mem_bind_iff : ∀ {α : Type u_1} {β : Type u_2} {b : β} {o : Option α} {f : α → Option β}, b ∈ o.bind f ↔ ∃ a ∈ o, b ∈ f a
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.braiding_hom_fst_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X Y : C) {Z : C} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (β_ X Y).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.fst Y X) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.snd X Y) h
-- Mathlib.RingTheory.Smooth.StandardSmoothCotangent
Algebra.Generators.basisCotangentAway_apply : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (r : R)
  [inst_3 : IsLocalization.Away r S] (x : Unit),
  (Algebra.Generators.basisCotangentAway S r) x = Algebra.Generators.cMulXSubOneCotangent S r
-- Mathlib.Analysis.InnerProductSpace.Basic
/-- See `inner_smul_left_eq_star_smul` for the case of a general algebra action.  -/
inner_smul_left : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (x y : E) (r : 𝕜), inner 𝕜 (r • x) y = (starRingEnd 𝕜) r * inner 𝕜 x y
-- Mathlib.LinearAlgebra.Matrix.Transvection
Matrix.TransvectionStruct.toMatrix_mk : ∀ {n : Type u_1} {R : Type u₂} [inst : DecidableEq n] [inst_1 : CommRing R] (i j : n) (hij : i ≠ j) (c : R),
  { i := i, j := j, hij := hij, c := c }.toMatrix = Matrix.transvection i j c
-- Mathlib.Probability.Density
/-- If `X` is a real-valued random variable that has pdf `f`, then the expectation of `X` equals
`∫ x, x * f x ∂λ` where `λ` is the Lebesgue measure.  -/
MeasureTheory.pdf.integral_mul_eq_integral : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {ℙ : MeasureTheory.Measure Ω} {X : Ω → ℝ} [MeasureTheory.IsFiniteMeasure ℙ]
  [MeasureTheory.HasPDF X ℙ MeasureTheory.volume],
  ∫ (x : ℝ), x * (MeasureTheory.pdf X ℙ MeasureTheory.volume x).toReal = ∫ (x : Ω), X x ∂ℙ
-- Mathlib.Data.Tree.Basic
/-- **Alias** of `BinaryTree.traverse`.  -/
Tree.traverse : {m : Type u_1 → Type u_2} → [Applicative m] → {α : Type u_3} → {β : Type u_1} → (α → m β) → Tree α → m (Tree β)
-- Mathlib.RingTheory.RingHom.FiniteType
RingHom.finiteType_holdsForLocalizationAway : RingHom.HoldsForLocalizationAway @RingHom.FiniteType
-- Mathlib.Topology.Algebra.UniformConvergence
UniformOnFun.toFun_inv : ∀ {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [inst : Inv β] (f : UniformOnFun α β 𝔖),
  (UniformOnFun.toFun 𝔖) f⁻¹ = ((UniformOnFun.toFun 𝔖) f)⁻¹
-- Mathlib.Algebra.Ring.Subring.Basic
/-- Product of a list of elements in a subring is in the subring.  -/
Subring.list_prod_mem : ∀ {R : Type u_1} [inst : Ring R] (s : Subring R) {l : List R}, (∀ x ∈ l, x ∈ s) → l.prod ∈ s
-- Mathlib.Analysis.SpecialFunctions.Log.Base
_private.Mathlib.Analysis.SpecialFunctions.Log.Base.0.Real.b_ne_one' : ∀ {b : ℝ}, 1 < b → b ≠ 1
-- Mathlib.CategoryTheory.Functor.OfSequence
CategoryTheory.Functor.ofSequence_map_homOfLE_succ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)) (n : ℕ),
  (CategoryTheory.Functor.ofSequence f).map (CategoryTheory.homOfLE ⋯) = f n
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey_congr : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : EquivBEq α]
  [inst_3 : LawfulHashable α] (h : m.WF) {k₁ k₂ : α} (h' : (k₁ == k₂) = true) (h₁ : k₁ ∈ m),
  m.getKey k₁ h₁ = m.getKey k₂ ⋯
-- Mathlib.RingTheory.GradedAlgebra.AlgHom
GradedAlgHom.restrictScalars_injective : ∀ {R : Type u_1} {A : Type u_6} {B : Type u_7} {ι : Type u_10} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : DecidableEq ι] [inst_6 : AddMonoid ι]
  {𝒜 : ι → Submodule R A} {ℬ : ι → Submodule R B} [inst_7 : GradedAlgebra 𝒜] [inst_8 : GradedAlgebra ℬ] (R₀ : Type u_11)
  [inst_9 : CommSemiring R₀] [inst_10 : Algebra R₀ R] [inst_11 : Algebra R₀ A] [inst_12 : Algebra R₀ B]
  [inst_13 : IsScalarTower R₀ R A] [inst_14 : IsScalarTower R₀ R B], Function.Injective ↑R₀
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Decl.instantiateTypeLevelParams : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.Decl pu → List Lean.Level → Lean.Expr
-- Mathlib.LinearAlgebra.RootSystem.Hom
RootPairing.Equiv.toEndUnit_val : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) (g : P.Aut),
  ↑((RootPairing.Equiv.toEndUnit P) g) = ↑g
-- Mathlib.Order.BoundedOrder.Basic
Subtype.coe_eq_top_iff : ∀ {α : Type u} {p : α → Prop} [inst : PartialOrder α] [inst_1 : OrderTop α] [inst_2 : OrderTop (Subtype p)],
  p ⊤ → ∀ {x : { x // p x }}, ↑x = ⊤ ↔ x = ⊤
-- Mathlib.Topology.Algebra.Ring.Basic
RingTopology.toTopologicalSpace : {R : Type u} → [inst : Ring R] → RingTopology R → TopologicalSpace R
-- Mathlib.Geometry.Manifold.Instances.Quotient
MulAction.instChartedSpaceQuotient.eq_1 : ∀ {M : Type u_1} [inst : TopologicalSpace M] {G : Type u_2} [inst_1 : Group G] [inst_2 : MulAction G M]
  [inst_3 : ProperlyDiscontinuousSMul G M] [inst_4 : ContinuousConstSMul G M] [inst_5 : IsCancelSMul G M]
  [inst_6 : T2Space M] [inst_7 : LocallyCompactSpace M] {H : Type u_3} [inst_8 : TopologicalSpace H]
  [inst_9 : ChartedSpace H M], MulAction.instChartedSpaceQuotient = ⋯.chartedSpace ⋯
-- Mathlib.Order.Hom.Bounded
BotHom.dual_apply_apply : ∀ {α : Type u_2} {β : Type u_3} [inst : LE α] [inst_1 : OrderBot α] [inst_2 : LE β] [inst_3 : OrderBot β]
  (f : BotHom α β) (a : α), (BotHom.dual f) a = f a
-- Mathlib.RingTheory.Polynomial.Content
Polynomial.isPrimitive_iff_isUnit_of_C_dvd : ∀ {R : Type u_1} [inst : CommSemiring R] {p : Polynomial R}, p.IsPrimitive ↔ ∀ (r : R), Polynomial.C r ∣ p → IsUnit r
-- Mathlib.CategoryTheory.Generator.HomologicalComplex
HomologicalComplex.isSeparating_separatingFamily : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {ι : Type w} (c : ComplexShape ι) [c.HasNoLoop]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.Limits.HasZeroObject C] {α : Type t}
  {X : α → C},
  (CategoryTheory.ObjectProperty.ofObj X).IsSeparating →
    (CategoryTheory.ObjectProperty.ofObj (HomologicalComplex.separatingFamily c X)).IsSeparating
-- Mathlib.Algebra.Order.Floor.Extended
ENat.preimage_toENNReal_Ioc : ∀ (a b : ENNReal), ENat.toENNReal ⁻¹' Set.Ioc a b = Set.Ioc ⌊a⌋ₑ ⌊b⌋ₑ
-- Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
Complex.volume_sum_rpow_le : ∀ (ι : Type u_1) [inst : Fintype ι] [Nonempty ι] {p : ℝ},
  1 ≤ p →
    ∀ (r : ℝ),
      MeasureTheory.volume {x | (∑ i, ‖x i‖ ^ p) ^ (1 / p) ≤ r} =
        ENNReal.ofReal r ^ (2 * Fintype.card ι) *
          ENNReal.ofReal
            ((Real.pi * Real.Gamma (2 / p + 1)) ^ Fintype.card ι / Real.Gamma (2 * ↑(Fintype.card ι) / p + 1))
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.measure_support_lt_top_of_lintegral_ne_top : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : MeasureTheory.SimpleFunc α ENNReal},
  f.lintegral μ ≠ ⊤ → μ (Function.support ⇑f) < ⊤
-- Mathlib.Algebra.Lie.Basic
LieHom.map_lie : ∀ {R : Type u} {L₁ : Type v} {L₂ : Type w} [inst : CommRing R] [inst_1 : LieRing L₁] [inst_2 : LieAlgebra R L₁]
  [inst_3 : LieRing L₂] [inst_4 : LieAlgebra R L₂] (f : L₁ →ₗ⁅R⁆ L₂) (x y : L₁), f ⁅x, y⁆ = ⁅f x, f y⁆
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenAddSubgroup.instPartialOrder.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G],
  OpenAddSubgroup.instPartialOrder = PartialOrder.ofSetLike (OpenAddSubgroup G) G
-- Aesop.Script.CtorNames
Aesop.CtorNames.mk.sizeOf_spec : ∀ (ctor : Lean.Name) (args : Array Lean.Name) (hasImplicitArg : Bool),
  sizeOf { ctor := ctor, args := args, hasImplicitArg := hasImplicitArg } =
    1 + sizeOf ctor + sizeOf args + sizeOf hasImplicitArg
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Three
/-- Let `(x : 𝓞 K)`. Then we have that `λ` divides one amongst `x`, `x - 1` and `x + 1`.  -/
IsCyclotomicExtension.Rat.Three.lambda_dvd_or_dvd_sub_one_or_dvd_add_one : ∀ {K : Type u_1} [inst : Field K] {ζ : K} (hζ : IsPrimitiveRoot ζ 3) (x : NumberField.RingOfIntegers K)
  [inst_1 : NumberField K] [IsCyclotomicExtension {3} ℚ K],
  hζ.toInteger - 1 ∣ x ∨ hζ.toInteger - 1 ∣ x - 1 ∨ hζ.toInteger - 1 ∣ x + 1
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.yonedaAddMonObj_obj_coe : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (M : C) [inst_2 : CategoryTheory.AddMonObj M] (X : Cᵒᵖ),
  ↑((CategoryTheory.yonedaAddMonObj M).obj X) = (Opposite.unop X ⟶ M)
-- Mathlib.Order.Completion
/-- Use `DedekindCut.lt_iff_exists'` for a version with `<` and `≤` swapped  -/
DedekindCut.lt_iff_exists : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : DedekindCut α},
  a < b ↔ ∃ c, a < DedekindCut.principal c ∧ DedekindCut.principal c ≤ b
-- Mathlib.MeasureTheory.Function.Piecewise
MeasureTheory.SimpleFunc.mk.congr_simp : ∀ {α : Type u} [inst : MeasurableSpace α] {β : Type v} (toFun toFun_1 : α → β) (e_toFun : toFun = toFun_1)
  (measurableSet_fiber' : ∀ (x : β), MeasurableSet (toFun ⁻¹' {x})) (finite_range' : (Set.range toFun).Finite),
  { toFun := toFun, measurableSet_fiber' := measurableSet_fiber', finite_range' := finite_range' } =
    { toFun := toFun_1, measurableSet_fiber' := ⋯, finite_range' := ⋯ }
-- Mathlib.CategoryTheory.Monoidal.Comon_
/-- The forgetful functor from comonoid objects to the ambient category.  -/
CategoryTheory.Comon.forget : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] → CategoryTheory.Functor (CategoryTheory.Comon C) C
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.isHashSelf_foldl_reinsertAux : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  (l : List ((a : α) × β a)) (target : { d // 0 < d.size }),
  Std.DHashMap.Internal.IsHashSelf ↑target →
    Std.DHashMap.Internal.IsHashSelf
      ↑(List.foldl (fun acc p => Std.DHashMap.Internal.Raw₀.reinsertAux hash acc p.fst p.snd) target l)
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.instNNRatCast : {R : Type u_1} →
  {Γ₀ : Type u_2} →
    [inst : LinearOrderedCommGroupWithZero Γ₀] →
      [inst_1 : DivisionRing R] → (v : Valuation R Γ₀) → NNRatCast (WithVal v)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.size_le_size_insertManyIfNewUnit_list : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtDHashMap α fun x => Unit} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l : List α}, m.size ≤ (Std.ExtDHashMap.Const.insertManyIfNewUnit m l).size
-- Lean.Parser.Tactic.Doc
/-- Extensions to tactic documentation.

This provides a structured way to indicate that an extensible tactic has been extended (for
instance, new cases tried by `trivial`).
 -/
Lean.Parser.Tactic.Doc.tacticDocExtExt : Lean.PersistentEnvExtension (Lean.Name × Array String) (Lean.Name × String) (Lean.NameMap (Array String))
-- Init.PropLemmas
/-- If two if-then-else statements only differ by the `Decidable` instances, they are equal.  -/
ite_iff_ite : ∀ (p : Prop) {h h' : Decidable p} (x y : Prop), ((if p then x else y) ↔ if p then x else y) ↔ True
-- Std.Http.Data.URI.Encoding
/-- Decodes an encoded userinfo component back to a UTF-8 string.
 -/
Std.Http.URI.EncodedUserInfo.decode : Std.Http.URI.EncodedUserInfo → Option String
-- Lean.Environment
Lean.Kernel.Exception.thmTypeIsNotProp.injEq : ∀ (env : Lean.Kernel.Environment) (name : Lean.Name) (type : Lean.Expr) (env_1 : Lean.Kernel.Environment)
  (name_1 : Lean.Name) (type_1 : Lean.Expr),
  (Lean.Kernel.Exception.thmTypeIsNotProp env name type = Lean.Kernel.Exception.thmTypeIsNotProp env_1 name_1 type_1) =
    (env = env_1 ∧ name = name_1 ∧ type = type_1)
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.evalRingHom_apply : ∀ {ι : Type u_1} (R : ι → Type u_2) {𝓕 : Filter ι} {S : ι → Type u_3} [inst : (i : ι) → SetLike (S i) (R i)]
  {B : (i : ι) → S i} [inst_1 : (i : ι) → Ring (R i)] [inst_2 : ∀ (i : ι), SubringClass (S i) (R i)]
  (x : RestrictedProduct (fun i => R i) (fun i => ↑(B i)) 𝓕) (j : ι), (RestrictedProduct.evalRingHom R j) x = x j
-- Mathlib.SetTheory.Ordinal.Exponential
Ordinal.sub_omega0_opow_log_lt : ∀ {a : Ordinal.{u_1}}, a ≠ 0 → a - Ordinal.omega0 ^ Ordinal.log Ordinal.omega0 a < a
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.compare_getKey?_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k : α}, Option.all (fun x => decide (cmp x k = Ordering.eq)) (t.getKey? k) = true