mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
AEMeasurable.complex_ofReal : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ},
  AEMeasurable f μ → AEMeasurable (fun x => ↑(f x)) μ
-- Mathlib.Algebra.Group.Defs
/-- Typeclass for expressing that `-0 = 0`.  -/
NegZeroClass : Type u_2 → Type u_2
-- Mathlib.Data.Set.Card
Set.encard_le_one_iff_eq : ∀ {α : Type u_1} {s : Set α}, s.encard ≤ 1 ↔ s = ∅ ∨ ∃ x, s = {x}
-- Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
/-- Relative of lengths of roots in a reduced irreducible finite crystallographic root pairing are
very constrained.  -/
RootPairing.InvariantForm.apply_eq_or : ∀ {ι : 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} [Finite ι]
  [CharZero R] [P.IsCrystallographic] [IsDomain R] [P.IsReduced] (B : P.InvariantForm) [P.IsIrreducible] (i j : ι),
  (B.form (P.root i)) (P.root i) = (B.form (P.root j)) (P.root j) ∨
    (B.form (P.root i)) (P.root i) = 2 * (B.form (P.root j)) (P.root j) ∨
      (B.form (P.root i)) (P.root i) = 3 * (B.form (P.root j)) (P.root j) ∨
        (B.form (P.root j)) (P.root j) = 2 * (B.form (P.root i)) (P.root i) ∨
          (B.form (P.root j)) (P.root j) = 3 * (B.form (P.root i)) (P.root i)
-- Lean.CoreM
Lean.DeclNameGenerator.mk.sizeOf_spec : ∀ (namePrefix : Lean.Name) (idx : ℕ) (parentIdxs : List ℕ),
  sizeOf { namePrefix := namePrefix, idx := idx, parentIdxs := parentIdxs } =
    1 + sizeOf namePrefix + sizeOf idx + sizeOf parentIdxs
-- Init.Data.Int.OfNat
Int.Nonneg.pow : ∀ (a : ℤ) (k : ℕ), a ≥ 0 → a ^ k ≥ 0
-- Std.Data.HashMap.Lemmas
Std.HashMap.isEmpty_modify : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α}
  {f : β → β}, (m.modify k f).isEmpty = m.isEmpty
-- Mathlib.Analysis.InnerProductSpace.Adjoint
Submodule.adjoint_subtypeL : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : CompleteSpace E] (U : Submodule 𝕜 E) [inst_4 : CompleteSpace ↥U],
  ContinuousLinearMap.adjoint U.subtypeL = U.orthogonalProjectionOnto
-- Mathlib.Analysis.Analytic.Basic
/-- If a function admits a power series expansion within a set in a ball, then it is exponentially
close to the partial sums of this power series on strict subdisks of the disk of convergence.  -/
HasFPowerSeriesWithinOnBall.uniform_geometric_approx : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} {r : ENNReal} {r' : NNReal},
  HasFPowerSeriesWithinOnBall f p s x r →
    ↑r' < r →
      ∃ a ∈ Set.Ioo 0 1,
        ∃ C > 0, ∀ y ∈ Metric.ball 0 ↑r', ∀ (n : ℕ), x + y ∈ insert x s → ‖f (x + y) - p.partialSum n y‖ ≤ C * a ^ n
-- Mathlib.RingTheory.Regular.RegularSequence
Submodule.quotOfListConsSMulTopEquivQuotSMulTopInner_naturality : ∀ {R : Type u_1} {M : Type u_3} {M₂ : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup M₂]
  [inst_3 : Module R M] [inst_4 : Module R M₂] (r : R) (rs : List R) (f : M →ₗ[R] M₂),
  ↑(Submodule.quotOfListConsSMulTopEquivQuotSMulTopInner M₂ r rs) ∘ₗ
      (Ideal.ofList (r :: rs) • ⊤).mapQ (Ideal.ofList (r :: rs) • ⊤) f ⋯ =
    (Ideal.ofList rs • ⊤).mapQ (Ideal.ofList rs • ⊤) ((QuotSMulTop.map r) f) ⋯ ∘ₗ
      ↑(Submodule.quotOfListConsSMulTopEquivQuotSMulTopInner M r rs)
-- Lean.Meta.Sym.Pattern
/-- Similar to `Meta.decLevel?`, but never assigns metavariables.  -/
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.decLevel? : Lean.Level → Option Lean.Level
-- Mathlib.Order.Disjoint
Disjoint.symm : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : OrderBot α] ⦃a b : α⦄, Disjoint a b → Disjoint b a
-- Mathlib.NumberTheory.FunctionField
/-- **Alias** of `RatFunc.valuedCompletionAtInfty.def`. -/
FunctionField.valuedFqtInfty.def : ∀ (F : Type u_1) [inst : Field F] [inst_1 : DecidableEq (RatFunc F)] {x : RatFunc.CompletionAtInfty F},
  Valued.v x = Valued.extensionValuation x
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey_erase : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k a : α} {h' : a ∈ m.erase k}, (m.erase k).getKey a h' = m.getKey a ⋯
-- Mathlib.Data.Matrix.Block
Matrix.blockDiagonal'_one : ∀ {o : Type u_4} {m' : o → Type u_7} {α : Type u_12} [inst : DecidableEq o] [inst_1 : Zero α]
  [inst_2 : (i : o) → DecidableEq (m' i)] [inst_3 : One α], Matrix.blockDiagonal' 1 = 1
-- Mathlib.Topology.Homeomorph.Defs
/-- **Alias** of `Homeomorph.isClosed_setOfPred_iff`. -/
Homeomorph.isClosed_setOf_iff : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {p : X → Prop} {q : Y → Prop}
  (f : X ≃ₜ Y), IsClopen {x | p x} → IsClopen {y | q y} → IsClosed {x | p x ↔ q (f x)}
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
ContinuousLinearMap.lTensor_comp_rTensor : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {H : Type u_5} [inst : RCLike 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F]
  [inst_4 : InnerProductSpace 𝕜 F] [inst_5 : NormedAddCommGroup G] [inst_6 : InnerProductSpace 𝕜 G]
  [inst_7 : NormedAddCommGroup H] [inst_8 : InnerProductSpace 𝕜 H] (f : E →L[𝕜] F) (g : G →L[𝕜] H),
  ContinuousLinearMap.lTensor H f ∘SL ContinuousLinearMap.rTensor E g = TensorProduct.mapL g f
-- Mathlib.Algebra.Order.Monoid.Unbundled.Pow
nsmul_le_nsmul_right : ∀ {M : Type u_3} [inst : AddMonoid M] [inst_1 : Preorder M] [AddLeftMono M] [AddRightMono M] {a b : M},
  a ≤ b → ∀ (i : ℕ), i • a ≤ i • b
-- Lean.Compiler.LCNF.Basic
_private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.Arg.updateFVarImp : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.Arg pu → Lean.FVarId → Lean.Compiler.LCNF.Arg pu
-- Mathlib.AlgebraicTopology.EilenbergSteenrod
/-- `Hₚ` and `H` agree on `TopCat`.  -/
TopPair.HomologyPretheory.iso : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {ι : Type u_2} →
        {c : ComplexShape ι} →
          (self : TopPair.HomologyPretheory C c) → (i : ι) → self.H i ≅ TopPair.incl.comp (self.Hₚ i)
-- Mathlib.Order.Filter.AtTopBot.Finset
Filter.tendsto_finset_powerset_atTop_atTop : ∀ {α : Type u_3}, Filter.Tendsto Finset.powerset Filter.atTop Filter.atTop
-- Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Multiset.sum_hom₂_ne_zero : ∀ {ι : Type u_2} {M : Type u_5} {N : Type u_6} {O : Type u_7} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N]
  [inst_2 : AddCommMonoid O] {s : Multiset ι},
  s ≠ 0 →
    ∀ (f : M → N → O),
      (∀ (a b : M) (c d : N), f (a + b) (c + d) = f a c + f b d) →
        ∀ (f₁ : ι → M) (f₂ : ι → N),
          (Multiset.map (fun i => f (f₁ i) (f₂ i)) s).sum = f (Multiset.map f₁ s).sum (Multiset.map f₂ s).sum
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
instClosedEmbeddingContinuousFunctionalCalculusOfCompleteSpace : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : Ring A] [inst_6 : StarRing A]
  [inst_7 : MetricSpace A] [inst_8 : Algebra R A] [IsometricContinuousFunctionalCalculus R A p] [CompleteSpace R],
  ClosedEmbeddingContinuousFunctionalCalculus R A p
-- Mathlib.Analysis.BoxIntegral.Partition.Tagged
BoxIntegral.TaggedPrepartition.instMembershipBox : {ι : Type u_1} → {I : BoxIntegral.Box ι} → Membership (BoxIntegral.Box ι) (BoxIntegral.TaggedPrepartition I)
-- Mathlib.Topology.EMetricSpace.Defs
/-- Pseudoemetric space instance on the additive opposite of a pseudoemetric space.  -/
AddOpposite.instPseudoEMetricSpace : {α : Type u_2} → [PseudoEMetricSpace α] → PseudoEMetricSpace αᵃᵒᵖ
-- Init.Grind.Ring.Field
Lean.Grind.Field.add_div : ∀ {α : Type u_1} [inst : Lean.Grind.Field α] {x y z : α}, z ≠ 0 → x + y / z = (x * z + y) / z
-- Mathlib.Analysis.Complex.Hadamard
/-- An auxiliary function to prove the general statement of Hadamard's three lines theorem.  -/
Complex.HadamardThreeLines.scale : {E : Type u_1} → (ℂ → E) → ℝ → ℝ → ℂ → E
-- Mathlib.Topology.ContinuousMap.Compact
ContinuousMap.instNontrivialTopologyOfNonemptyOfNontrivial : ∀ {α : Type u_1} [inst : TopologicalSpace α] [CompactSpace α] [Nonempty α] {E : Type u_4}
  [inst_3 : NormedAddCommGroup E] [Nontrivial E], NontrivialTopology C(α, E)
-- Mathlib.Algebra.Algebra.Unitization
Unitization.inrNonUnitalStarAlgHom_apply : ∀ (R : Type u_1) (A : Type u_2) [inst : CommSemiring R] [inst_1 : StarAddMonoid R] [inst_2 : NonUnitalSemiring A]
  [inst_3 : Star A] [inst_4 : Module R A] (a : A), (Unitization.inrNonUnitalStarAlgHom R A) a = ↑a
-- Lean.Elab.Match
Lean.Elab.Term.ElabMatchTypeAndDiscrsResult.mk.sizeOf_spec : ∀ (discrs : Array Lean.Elab.Term.Discr) (matchType : Lean.Expr) (isDep : Bool)
  (alts : Array Lean.Elab.Term.TermMatchAltView),
  sizeOf { discrs := discrs, matchType := matchType, isDep := isDep, alts := alts } =
    1 + sizeOf discrs + sizeOf matchType + sizeOf isDep + sizeOf alts
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey!_filter_key : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {f : α → Bool} {k : α},
  (Std.ExtTreeMap.filter (fun k x => f k) t).getKey! k = (Option.filter f (t.getKey? k)).get!
-- Init.Data.SInt.Basic
instComplementISize : Complement ISize
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getElem?_toList_roc_eq_none : ∀ {m n : ℤ} {i : ℕ}, (n - m).toNat ≤ i → (m<...=n).toList[i]? = none
-- Mathlib.RingTheory.LaurentSeries
/-- The ring `K⟦X⟧` is isomorphic to the subring `powerSeries_as_subring K`  -/
LaurentSeries.powerSeriesEquivSubring : (K : Type u_2) → [inst : Field K] → PowerSeries K ≃+* ↥(LaurentSeries.powerSeries_as_subring K)
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.dist_pseudoMetricSpaceToPi : ∀ (p : ENNReal) {ι : Type u_2} (α : ι → Type u_3) [inst : Fact (1 ≤ p)] [inst_1 : Fintype ι]
  [inst_2 : (i : ι) → PseudoMetricSpace (α i)] (x y : (i : ι) → α i),
  dist x y = dist (WithLp.toLp p x) (WithLp.toLp p y)
-- Init.Data.Range.Polymorphic.UpwardEnumerable
Std.PRange.Least?.mk : {α : Type u} → Option α → Std.PRange.Least? α
-- Mathlib.CategoryTheory.GradedObject.Trifunctor
/-- an auxiliary type  -/
CategoryTheory.GradedObject.BifunctorComp₂₃IndexData.I₂₃ : {I₁ : Type u_7} →
  {I₂ : Type u_8} →
    {I₃ : Type u_9} →
      {J : Type u_10} → {r : I₁ × I₂ × I₃ → J} → CategoryTheory.GradedObject.BifunctorComp₂₃IndexData r → Type u_11
-- Mathlib.AlgebraicTopology.SimplicialSet.NonsingularColimit
SSet.coconeN'_ι_app : ∀ (X : SSet) [inst : X.Nonsingular] (s : X.N), X.coconeN'.ι.app s = SSet.yonedaEquiv.symm s.simplex
-- Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Ordinal.cof_add : ∀ (a : Ordinal.{u_1}) {b : Ordinal.{u_1}}, b ≠ 0 → (a + b).cof = b.cof
-- Mathlib.Algebra.Order.Field.Power
Odd.zpow_neg_iff : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {a : α} {n : ℤ},
  Odd n → (a ^ n < 0 ↔ a < 0)
-- Mathlib.Algebra.Group.Basic
inv_comp_inv : ∀ (G : Type u_3) [inst : InvolutiveInv G], Inv.inv ∘ Inv.inv = id
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
Std.Iter.filterM.eq_1 : ∀ {α β : Type w} [inst : Std.Iterator α Id β] {m : Type w → Type w'} [inst_1 : Monad m] [inst_2 : MonadAttach m]
  (f : β → m (ULift.{w, 0} Bool)) (it : Std.Iter β), Std.Iter.filterM f it = Std.IterM.filterM f it.toIterM
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem!_of_isEmpty : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : Inhabited β]
  {a : α}, t.isEmpty = true → t[a]! = default
-- Mathlib.Algebra.Order.GroupWithZero.Basic
pow_lt_one₀ : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] [inst_1 : Preorder M₀] {a : M₀} [PosMulMono M₀],
  0 ≤ a → a < 1 → ∀ {n : ℕ}, n ≠ 0 → a ^ n < 1
-- Mathlib.RingTheory.Kaehler.Basic
KaehlerDifferential.D_apply : ∀ (R : Type u) (S : Type v) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (s : S),
  (KaehlerDifferential.D R S) s = (KaehlerDifferential.ideal R S).toCotangent ⟨1 ⊗ₜ[R] s - s ⊗ₜ[R] 1, ⋯⟩
-- Mathlib.RingTheory.MvPolynomial.Homogeneous
MvPolynomial.homogeneousComponent_mem_of_mem : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommSemiring R] {I : Ideal (MvPolynomial σ R)},
  Ideal.IsHomogeneous (MvPolynomial.homogeneousSubmodule σ R) I →
    ∀ {p : MvPolynomial σ R}, p ∈ I → ∀ (n : ℕ), (MvPolynomial.homogeneousComponent n) p ∈ I
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.b₄_of_isCharNeTwoNF : ∀ {R : Type u_1} [inst : CommRing R] (W : WeierstrassCurve R) [W.IsCharNeTwoNF], W.b₄ = 2 * W.a₄
-- Mathlib.Analysis.Normed.Group.Seminorm
GroupSeminorm.instMin.eq_1 : ∀ {E : Type u_3} [inst : CommGroup E],
  GroupSeminorm.instMin =
    { min := fun p q => { toFun := fun x => ⨅ y, p y + q (x / y), map_one' := ⋯, mul_le' := ⋯, inv' := ⋯ } }
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.add_limZero : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α]
  [inst_3 : Ring β] {abv : β → α} [inst_4 : IsAbsoluteValue abv] {f g : CauSeq β abv},
  f.LimZero → g.LimZero → (f + g).LimZero
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.descE.congr_simp : ∀ {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 j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (f₁₂ : i ⟶ k)
  (h₁₂ : CategoryTheory.CategoryStruct.comp f₁ f₂ = f₁₂) (n₀ n₁ n₂ : ℤ) {A : C}
  (x x_1 : (X.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ f₁₂) ⟶ A) (e_x : x = x_1)
  (h :
    CategoryTheory.CategoryStruct.comp ((X.H n₁).map (CategoryTheory.ComposableArrows.twoδ₂Toδ₁ f₁ f₂ f₁₂ h₁₂)) x = 0)
  (hn₁ : n₀ + 1 = n₁) (h' : CategoryTheory.CategoryStruct.comp (X.δ f₁₂ f₃ n₀ n₁ hn₁) x = 0) (hn₂ : n₁ + 1 = n₂),
  X.descE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ x h hn₁ h' hn₂ = X.descE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ x_1 ⋯ hn₁ ⋯ hn₂
-- Mathlib.Analysis.InnerProductSpace.Continuous
DenseRange.eq_of_inner_right : ∀ {E : Type u_4} {ι : Type u_6} (𝕜 : Type u_7) [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] {x y : E} {f : ι → E},
  DenseRange f → (∀ (i : ι), inner 𝕜 (f i) x = inner 𝕜 (f i) y) → x = y
-- Mathlib.Algebra.Group.Commute.Defs
Commute.pow_left : ∀ {M : Type u_2} [inst : Monoid M] {a b : M}, Commute a b → ∀ (n : ℕ), Commute (a ^ n) b
-- Init.Data.Int.Order
Int.nonpos_of_mul_nonneg_right : ∀ {a b : ℤ}, 0 ≤ a * b → a < 0 → b ≤ 0
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.contains_of_contains_erase : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {k a : α},
  (t.erase k).contains a = true → t.contains a = true
-- Lean.Elab.MutualInductive
Lean.Elab.Command.InductiveElabStep2.mk.sizeOf_spec : ∀ (ctors : List Lean.Constructor) (collectUsedFVars : StateRefT' IO.RealWorld Lean.CollectFVars.State Lean.MetaM Unit)
  (collectExtraHeaderLMVars : StateRefT' IO.RealWorld Lean.CollectLevelMVars.State Lean.MetaM Unit)
  (checkUniverses : ℕ → Lean.Level → Lean.Elab.TermElabM Unit) (finalizeTermElab : Lean.Elab.TermElabM Unit)
  (prefinalize :
    List Lean.Name →
      Array Lean.Expr → (Lean.Expr → Lean.MetaM Lean.Expr) → Lean.Elab.TermElabM Lean.Elab.Command.InductiveElabStep3),
  sizeOf
      { ctors := ctors, collectUsedFVars := collectUsedFVars, collectExtraHeaderLMVars := collectExtraHeaderLMVars,
        checkUniverses := checkUniverses, finalizeTermElab := finalizeTermElab, prefinalize := prefinalize } =
    1 + sizeOf ctors
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.linearMap_ext'_iff : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_5} [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {f g : SkewPolynomial R →ₗ[R] M}, f = g ↔ ∀ (n : ℕ), f ∘ₗ SkewPolynomial.monomial n = g ∘ₗ SkewPolynomial.monomial n
-- Mathlib.Topology.Order
TopologicalSpace.nhds_mkOfNhds_filterBasis : ∀ {α : Type u} (B : α → FilterBasis α) (a : α),
  (∀ (x : α), ∀ n ∈ B x, x ∈ n) →
    (∀ (x : α), ∀ n ∈ B x, ∃ n₁ ∈ B x, ∀ x' ∈ n₁, ∃ n₂ ∈ B x', n₂ ⊆ n) → nhds a = (B a).filter
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.smul_finset_nonempty : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : SMul α β] {s : Finset β} {a : α},
  (a • s).Nonempty ↔ s.Nonempty
-- Mathlib.RepresentationTheory.Homological.ContCohomology.Functoriality
ContinuousCohomology.π_map : ∀ {k : Type u} {G H : Type v} [inst : Ring k] [inst_1 : TopologicalSpace k] [inst_2 : Group G]
  [inst_3 : TopologicalSpace G] [inst_4 : IsTopologicalGroup G] [inst_5 : Group H] [inst_6 : TopologicalSpace H]
  [inst_7 : IsTopologicalGroup H] {X : TopRep k G} {Y : TopRep k H} (φ : H →ₜ* G) (f : TopRep.res (↑φ) X ⟶ Y) (n : ℕ),
  CategoryTheory.CategoryStruct.comp (ContinuousCohomology.π X n) (ContinuousCohomology.map φ f n) =
    CategoryTheory.CategoryStruct.comp (ContinuousCohomology.cocyclesMap φ f n) (ContinuousCohomology.π Y n)
-- Init.MetaTypes
Lean.Module.mk.sizeOf_spec : ∀ (header : Lean.Syntax) (commands : Array Lean.Syntax),
  sizeOf { header := header, commands := commands } = 1 + sizeOf header + sizeOf commands
-- Mathlib.Analysis.Analytic.ChangeOrigin
FormalMultilinearSeries.le_changeOriginSeries_radius : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  (p : FormalMultilinearSeries 𝕜 E F) (k : ℕ), p.radius ≤ (p.changeOriginSeries k).radius
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
/-- **Alias** of `SkewMonoidAlgebra.coeff_mapDomain`. -/
SkewMonoidAlgebra.toFinsupp_mapDomain : ∀ {k : Type u_1} {G : Type u_2} [inst : AddCommMonoid k] {G' : Type u_3} (f : G → G') (v : SkewMonoidAlgebra k G),
  ((SkewMonoidAlgebra.mapDomain f) v).coeff = Finsupp.mapDomain f v.coeff
-- Mathlib.Algebra.Group.Submonoid.Units
Subgroup.mem_ofUnits_of_isUnit_of_unit_mem : ∀ {M : Type u_1} [inst : Monoid M] (S : Subgroup Mˣ) {x : M} (h₁ : IsUnit x), h₁.unit ∈ S → x ∈ S.ofUnits
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.comapDomain'_zero : ∀ {ι : Type u} {β : ι → Type v} {κ : Type u_1} [inst : (i : ι) → Zero (β i)] (h : κ → ι) {h' : ι → κ}
  (hh' : Function.LeftInverse h' h), DFinsupp.comapDomain' h hh' 0 = 0
-- Mathlib.Algebra.Order.GroupWithZero.Basic
inv_le_one₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀},
  0 < a → (a⁻¹ ≤ 1 ↔ 1 ≤ a)
-- Mathlib.Analysis.Normed.Group.Constructions
pi_nnnorm_lt_iff : ∀ {ι : Type u_1} {G : ι → Type u_4} [inst : Fintype ι] [inst_1 : (i : ι) → SeminormedAddGroup (G i)] {x : (i : ι) → G i}
  {r : NNReal}, 0 < r → (‖x‖₊ < r ↔ ∀ (i : ι), ‖x i‖₊ < r)
-- Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes
CategoryTheory.GrothendieckTopology.OneHypercover.isSheafFor_sieve_of_pullback : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {J : CategoryTheory.GrothendieckTopology C} {X : C}
  (E : J.OneHypercover X) {F : CategoryTheory.Functor Cᵒᵖ (Type u_2)},
  CategoryTheory.Presieve.IsSheaf J F →
    ∀ {S : CategoryTheory.Sieve X},
      (∀ (i : E.I₀), CategoryTheory.Presieve.IsSheafFor F (CategoryTheory.Sieve.pullback (E.f i) S).arrows) →
        (∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j),
            CategoryTheory.Presieve.IsSeparatedFor F
              (CategoryTheory.Sieve.pullback (CategoryTheory.CategoryStruct.comp (E.p₁ k) (E.f i)) S).arrows) →
          CategoryTheory.Presieve.IsSheafFor F S.arrows
-- Mathlib.MeasureTheory.Measure.Haar.Basic
MeasureTheory.Measure.haar.haarContent_outerMeasure_closure_pos : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalGroup G]
  (K₀ : TopologicalSpace.PositiveCompacts G), 0 < (MeasureTheory.Measure.haar.haarContent K₀).outerMeasure (closure ↑K₀)
-- Mathlib.Algebra.Group.Subsemigroup.Defs
Subsemigroup.mk.congr_simp : ∀ {M : Type u_3} [inst : Mul M] (carrier carrier_1 : Set M) (e_carrier : carrier = carrier_1)
  (mul_mem' : ∀ {a b : M}, a ∈ carrier → b ∈ carrier → a * b ∈ carrier),
  { carrier := carrier, mul_mem' := mul_mem' } = { carrier := carrier_1, mul_mem' := ⋯ }
-- Mathlib.Probability.Independence.BoundedContinuousFunction
/-- Two random variables $X$ and $Y$ are independent if
for all real bounded continuous functions $f$ and $g$,
$$P[f(X) g(Y)] = P[f(X)] * P[g(Y)].$$  -/
indepFun_of_bcf : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {G : Type u_6} {H : Type u_7}
  [inst : TopologicalSpace G] [inst_1 : MeasurableSpace G] [BorelSpace G] [HasOuterApproxClosed G]
  [inst_4 : TopologicalSpace H] [inst_5 : MeasurableSpace H] [BorelSpace H] [HasOuterApproxClosed H] {Z : Ω → G}
  {U : Ω → H} [MeasureTheory.IsFiniteMeasure P],
  AEMeasurable Z P →
    AEMeasurable U P →
      (∀ (f : BoundedContinuousFunction G ℝ) (g : BoundedContinuousFunction H ℝ),
          ∫ (x : Ω), (⇑f ∘ Z * ⇑g ∘ U) x ∂P = (∫ (x : Ω), (⇑f ∘ Z) x ∂P) * ∫ (x : Ω), (⇑g ∘ U) x ∂P) →
        ProbabilityTheory.IndepFun Z U P
-- Mathlib.Probability.Martingale.BorelCantelli
MeasureTheory.BorelCantelli.stronglyAdapted_process : ∀ {Ω : Type u_2} {m0 : MeasurableSpace Ω} {ℱ : MeasureTheory.Filtration ℕ m0} {s : ℕ → Set Ω},
  (∀ (n : ℕ), MeasurableSet (s n)) → MeasureTheory.StronglyAdapted ℱ (MeasureTheory.BorelCantelli.process s)
-- Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart
/-- A C⋆-algebra is spanned by nonnegative contractions.  -/
CStarAlgebra.span_nonneg_inter_unitClosedBall : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] [StarOrderedRing A],
  Submodule.span ℂ ({x | 0 ≤ x} ∩ Metric.closedBall 0 1) = ⊤
-- Lean.Meta.Basic
Lean.Meta.mkDefEqCacheKey : Lean.Expr → Lean.Expr → Lean.MetaM Lean.Meta.DefEqCacheKey
-- Lean.Meta.Sym.ExprPtr
Lean.Meta.Sym.hashPtrExpr.unsafe_1 : Lean.Expr → UInt64
-- Mathlib.Data.Sum.Order
OrderIso.sumAssoc_apply_inl_inr : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : LE α] [inst_1 : LE β] [inst_2 : LE γ] (b : β),
  (OrderIso.sumAssoc α β γ) (Sum.inl (Sum.inr b)) = Sum.inr (Sum.inl b)
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.mul_pos : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] {f g : CauSeq α abs},
  f.Pos → g.Pos → (f * g).Pos
-- Mathlib.CategoryTheory.Preadditive.Schur
/-- Part of **Schur's lemma** for `𝕜`-linear categories:
the hom space between two non-isomorphic simple objects is 0-dimensional.
 -/
CategoryTheory.finrank_hom_simple_simple_eq_zero_of_not_iso : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] (𝕜 : Type u_2)
  [inst_2 : DivisionRing 𝕜] [CategoryTheory.Limits.HasKernels C] [inst_4 : CategoryTheory.Linear 𝕜 C] {X Y : C}
  [CategoryTheory.Simple X] [CategoryTheory.Simple Y], (∀ (a : X ≅ Y), False) → Module.finrank 𝕜 (X ⟶ Y) = 0
-- Lean.Elab.Tactic.Meta
/-- Apply the give tactic code to `mvarId` in `MetaM`.  -/
Lean.Elab.runTactic : Lean.MVarId →
  Lean.Syntax →
    optParam Lean.Elab.Term.Context { } →
      optParam Lean.Elab.Term.State { } → Lean.MetaM (List Lean.MVarId × Lean.Elab.Term.State)
-- Lean.Meta.Tactic.Grind.Split
/-- Given `e` of the form `a ∧ b`, check whether we are ready to case-split on `e`.
That is, `e` is `False`, but neither `a` nor `b` is `False`.
  -/
_private.Lean.Meta.Tactic.Grind.Split.0.Lean.Meta.Grind.checkConjunctStatus : Lean.Expr → Lean.Expr → Lean.Expr → Lean.Meta.Grind.GoalM Lean.Meta.Grind.SplitStatus
-- Mathlib.CategoryTheory.Monad.Algebra
/-- The identity monad morphism induces the identity functor from the category of algebras to itself.
 -/
CategoryTheory.Monad.algebraFunctorOfMonadHomId : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {T₁ : CategoryTheory.Monad C} →
      CategoryTheory.Monad.algebraFunctorOfMonadHom (CategoryTheory.CategoryStruct.id T₁) ≅
        CategoryTheory.Functor.id T₁.Algebra