mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.ClosedUnder.inf : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {n : ℕ} {f : L.Functions n} {s t : Set M},
  FirstOrder.Language.ClosedUnder f s → FirstOrder.Language.ClosedUnder f t → FirstOrder.Language.ClosedUnder f (s ⊓ t)
-- Mathlib.SetTheory.Ordinal.Notation
ONote.instToString : ToString ONote
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.TheoremGuard.mk.injEq : ∀ (e : Lean.Expr) (check : Bool) (e_1 : Lean.Expr) (check_1 : Bool),
  ({ e := e, check := check } = { e := e_1, check := check_1 }) = (e = e_1 ∧ check = check_1)
-- Mathlib.Order.Hom.BoundedLattice
SupBotHomClass.mk : ∀ {F : Type u_6} {α : Type u_7} {β : Type u_8} [inst : Max α] [inst_1 : Max β] [inst_2 : Bot α] [inst_3 : Bot β]
  [inst_4 : FunLike F α β] [toSupHomClass : SupHomClass F α β], (∀ (f : F), f ⊥ = ⊥) → SupBotHomClass F α β
-- Mathlib.Algebra.Homology.ComplexShapeSigns
ComplexShape.associative_ε₂_eq_mul : ∀ {I₁ : Type u_1} {I₂ : Type u_2} {I₃ : Type u_3} {I₁₂ : Type u_4} {I₂₃ : Type u_5} {J : Type u_6}
  (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) (c₃ : ComplexShape I₃) (c₁₂ : ComplexShape I₁₂) (c₂₃ : ComplexShape I₂₃)
  (c : ComplexShape J) [inst : TotalComplexShape c₁ c₂ c₁₂] [inst_1 : TotalComplexShape c₁₂ c₃ c]
  [inst_2 : TotalComplexShape c₂ c₃ c₂₃] [inst_3 : TotalComplexShape c₁ c₂₃ c] [c₁.Associative c₂ c₃ c₁₂ c₂₃ c]
  (i₁ : I₁) (i₂ : I₂) (i₃ : I₃),
  c₁₂.ε₂ c₃ c (c₁.π c₂ c₁₂ (i₁, i₂), i₃) = c₁.ε₂ c₂₃ c (i₁, c₂.π c₃ c₂₃ (i₂, i₃)) * c₂.ε₂ c₃ c₂₃ (i₂, i₃)
-- Mathlib.Order.TeichmullerTukey
/-- **Teichmuller-Tukey lemma**. Every nonempty family of finite character has a maximal element.  -/
Order.IsOfFiniteCharacter.exists_maximal : ∀ {α : Type u_1} {F : Set (Set α)},
  Order.IsOfFiniteCharacter F → ∀ {x : Set α}, x ∈ F → ∃ m, x ⊆ m ∧ Maximal (fun x => x ∈ F) m
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.ExtraTheorem.fvar.injEq : ∀ (fvarId fvarId_1 : Lean.FVarId),
  (Lean.Elab.Tactic.Grind.ExtraTheorem.fvar fvarId = Lean.Elab.Tactic.Grind.ExtraTheorem.fvar fvarId_1) =
    (fvarId = fvarId_1)
-- Mathlib.MeasureTheory.Measure.Haar.Unique
/-- **Uniqueness of left-invariant measures**:
Two Haar measures coincide up to a multiplicative constant in a second countable group.  -/
MeasureTheory.Measure.isMulLeftInvariant_eq_smul : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : Group G] [inst_2 : IsTopologicalGroup G]
  [inst_3 : MeasurableSpace G] [inst_4 : BorelSpace G] [LocallyCompactSpace G] [SecondCountableTopology G]
  (μ' μ : MeasureTheory.Measure G) [inst_7 : μ.IsHaarMeasure] [inst_8 : MeasureTheory.IsFiniteMeasureOnCompacts μ']
  [inst_9 : μ'.IsMulLeftInvariant], μ' = μ'.haarScalarFactor μ • μ
-- Std.Data.Internal.List.Associative
Std.Internal.List.isSome_minEntry?_insert : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α] {k : α} {v : β k}
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l → (Std.Internal.List.minEntry? (Std.Internal.List.insertEntry k v l)).isSome = true
-- Mathlib.CategoryTheory.Limits.Shapes.End
CategoryTheory.Limits.coendFunctor_obj : ∀ (J : Type u) [inst : CategoryTheory.Category.{v, u} J] (C : Type u') [inst_1 : CategoryTheory.Category.{v', u'} C]
  [inst_2 : ∀ (F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)), CategoryTheory.Limits.HasCoend F]
  (F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)),
  (CategoryTheory.Limits.coendFunctor J C).obj F = CategoryTheory.Limits.coend F
-- Mathlib.Tactic.CategoryTheory.Monoidal.Datatypes
/-- The monad for the normalization of 2-morphisms.  -/
Mathlib.Tactic.Monoidal.MonoidalM : Type → Type
-- Mathlib.Algebra.Polynomial.FieldDivision
Polynomial.degree_div_le : ∀ {R : Type u} [inst : Field R] (p q : Polynomial R), (p / q).degree ≤ p.degree
-- Mathlib.Algebra.Group.End
Equiv.Perm.sumCongr_mul : ∀ {α : Type u_7} {β : Type u_8} (e : Equiv.Perm α) (f : Equiv.Perm β) (g : Equiv.Perm α) (h : Equiv.Perm β),
  e.sumCongr f * g.sumCongr h = (e * g).sumCongr (f * h)
-- Mathlib.Topology.Compactness.CountablyCompact
CountablyCompactSpace.isCountablyCompact_univ : ∀ {E : Type u_4} {inst : TopologicalSpace E} [self : CountablyCompactSpace E], IsCountablyCompact Set.univ
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.IsPartition.biUnion : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} {π : BoxIntegral.Prepartition I}
  {πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J},
  π.IsPartition → (∀ J ∈ π, (πi J).IsPartition) → (π.biUnion πi).IsPartition
-- Std.Time.Date.Unit.Day
Std.Time.Day.instDecidableEqOrdinal : DecidableEq Std.Time.Day.Ordinal
-- Mathlib.Tactic.Order.CollectFacts
Mathlib.Tactic.Order.AtomicFact.eq : ℕ → ℕ → Lean.Expr → Mathlib.Tactic.Order.AtomicFact
-- Mathlib.Topology.OpenPartialHomeomorph.Constructions
/-- Extend an open partial homeomorphism `e : X → Z` to `X' → Z`, using an open embedding
`ι : X → X'`. On `ι(X)`, the extension is specified by `e`; its value elsewhere is arbitrary
(and uninteresting).  -/
OpenPartialHomeomorph.lift_openEmbedding : {X : Type u_7} →
  {X' : Type u_8} →
    {Z : Type u_9} →
      [inst : TopologicalSpace X] →
        [inst_1 : TopologicalSpace X'] →
          [inst_2 : TopologicalSpace Z] →
            [Nonempty Z] →
              {f : X → X'} → OpenPartialHomeomorph X Z → Topology.IsOpenEmbedding f → OpenPartialHomeomorph X' Z
-- Mathlib.Analysis.SpecialFunctions.PolarCoord
Complex.lintegral_comp_polarCoord_symm : ∀ (f : ℂ → ENNReal),
  ∫⁻ (p : ℝ × ℝ) in polarCoord.target, ENNReal.ofReal p.1 • f (↑Complex.polarCoord.symm p) = ∫⁻ (p : ℂ), f p
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.Point.neg_zero : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Affine R}, -0 = 0
-- Mathlib.Algebra.Homology.Refinements
HomologicalComplex.comp_pOpcycles_eq_zero_iff_up_to_refinements : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {c : ComplexShape ι} (K : HomologicalComplex C c) {A : C} {i : ι} (z : A ⟶ K.X i) (j : ι),
  c.prev i = j →
    (CategoryTheory.CategoryStruct.comp z (K.pOpcycles i) = 0 ↔
      ∃ A' π,
        ∃ (_ : CategoryTheory.Epi π),
          ∃ x, CategoryTheory.CategoryStruct.comp π z = CategoryTheory.CategoryStruct.comp x (K.d j i))
-- Mathlib.LinearAlgebra.DirectSum.Finite
Module.Finite.instDFinsupp : ∀ {R : Type u_1} {ι : Type u_2} [inst : Semiring R] [Finite ι] (M : ι → Type u_3)
  [inst_2 : (i : ι) → AddCommMonoid (M i)] [inst_3 : (i : ι) → Module R (M i)] [∀ (i : ι), Module.Finite R (M i)],
  Module.Finite R (Π₀ (i : ι), M i)
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
CochainComplex.HomComplex.Cochain.leftShiftLinearEquiv_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] (R : Type u_1)
  [inst_2 : Ring R] [inst_3 : CategoryTheory.Linear R C] (K L : CochainComplex C ℤ) (n a n' : ℤ) (hn : n + a = n')
  (a_1 : CochainComplex.HomComplex.Cochain K L n),
  (CochainComplex.HomComplex.Cochain.leftShiftLinearEquiv R K L n a n' hn) a_1 = a_1.leftShift a n' hn
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsColimit.uniq_cocone_morphism : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {s t : CategoryTheory.Limits.Cocone F} (h : CategoryTheory.Limits.IsColimit t)
  {f f' : t ⟶ s}, f = f'
-- Init.Data.List.BasicAux
/-- Returns a pair of lists that together contain all the elements of `as`. The first list contains
those elements for which the monadic predicate `p` returns `true`, and the second contains those for
which `p` returns `false`. The list's elements are examined in order, from left to right.

This is a monadic version of `List.partition`.

Example:
```lean example
def posOrNeg (x : Int) : Except String Bool :=
  if x > 0 then pure true
  else if x < 0 then pure false
  else throw "Zero is not positive or negative"
```
```lean example
#eval [-1, 2, 3].partitionM posOrNeg
```
```output
Except.ok ([2, 3], [-1])
```
```lean example
#eval [0, 2, 3].partitionM posOrNeg
```
```output
Except.error "Zero is not positive or negative"
```
 -/
List.partitionM : {m : Type → Type u_1} → {α : Type} → [Monad m] → (α → m Bool) → List α → m (List α × List α)
-- Std.Internal.Do.WP.Lemmas
Std.Internal.Do.WPMonad.wp_throw_Option_apply_eq : ∀ {α : Type u_1} {post : α → Prop} {epost : Prop} (e : PUnit.{1}),
  Std.Internal.Do.wp (MonadExceptOf.throw e) post epost = epost
-- Mathlib.Algebra.Group.Hom.Instances
AddMonoidHom.compHom'.eq_1 : ∀ {M : Type uM} {N : Type uN} {P : Type uP} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] [inst_2 : AddCommMonoid P]
  (f : M →+ N), f.compHom' = (AddMonoidHom.eval.comp f).flip
-- Lean.Meta.Sym.Pattern
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.process.checkLetVar : Lean.Expr → Lean.Expr → Lean.Meta.Sym.UnifyM✝ Bool
-- Mathlib.Order.Sublattice
Sublattice.prod_eq_top : ∀ {α : Type u_2} {β : Type u_3} [inst : Lattice α] [inst_1 : Lattice β] {L : Sublattice α} [Nonempty α] [Nonempty β]
  {M : Sublattice β}, L.prod M = ⊤ ↔ L = ⊤ ∧ M = ⊤
-- Init.Data.List.Lemmas
List.length_pos_iff_exists_mem : ∀ {α : Type u_1} {l : List α}, 0 < l.length ↔ ∃ a, a ∈ l
-- Mathlib.Data.Setoid.Basic
Setoid.le_iff_rel_le : ∀ {α : Type u_1} {r₁ r₂ : Setoid α}, r₁ ≤ r₂ ↔ ⇑r₁ ≤ ⇑r₂
-- Mathlib.Analysis.Normed.Module.FiniteDimension
Module.Basis.opNorm_le : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type v} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type w} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : CompleteSpace 𝕜] {ι : Type u_1} [inst_6 : Fintype ι] (v : Module.Basis ι 𝕜 E) {u : E →L[𝕜] F} {M : ℝ},
  0 ≤ M → (∀ (i : ι), ‖u (v i)‖ ≤ M) → ‖u‖ ≤ Fintype.card ι • ‖↑v.equivFunL‖ * M
-- Mathlib.Analysis.Convex.SimplicialComplex.Basic
Geometry.SimplicialComplex.ext : ∀ {𝕜 : Type u_1} {E : Type u_2} {inst : Ring 𝕜} {inst_1 : PartialOrder 𝕜} {inst_2 : AddCommGroup E}
  {inst_3 : Module 𝕜 E} {x y : Geometry.SimplicialComplex 𝕜 E}, x.faces = y.faces → x = y
-- Mathlib.Algebra.Order.Ring.Synonym
Lex.instIsDomain : ∀ {R : Type u_1} [inst : Ring R] [IsDomain R], IsDomain (Lex R)
-- Mathlib.Topology.Algebra.Nonarchimedean.Bases
/-- Given a ring filter basis on a commutative ring `R`, define a compatibility condition
on a family of submodules of an `R`-module `M`. This compatibility condition allows to get
a topological module structure.  -/
RingFilterBasis.SubmodulesBasis : {ι : Type u_1} →
  {R : Type u_2} →
    [inst : CommRing R] →
      {M : Type u_4} →
        [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → RingFilterBasis R → (ι → Submodule R M) → Prop
-- Mathlib.Analysis.Normed.Module.TransferInstance
/-- Transfer `NormedSpace` across an `Equiv`  -/
Equiv.normedSpace : {α : Type u_1} →
  {β : Type u_2} →
    (𝕜 : Type u_3) →
      [inst : NormedField 𝕜] → [inst_1 : SeminormedAddCommGroup β] → [NormedSpace 𝕜 β] → (e : α ≃ β) → NormedSpace 𝕜 α
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
/-- The ideal `⟨X - x⟩` of `R[W]` for some `x` in `R`.  -/
WeierstrassCurve.Affine.CoordinateRing.XIdeal : {R : Type r} → [inst : CommRing R] → (W' : WeierstrassCurve.Affine R) → R → Ideal W'.CoordinateRing
-- Lean.Parser.Command
Lean.Parser.Command.exit.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PushoutProduct
SSet.instKanComplexObjIhom : ∀ {A X : SSet} [X.KanComplex], (A ⟹ X).KanComplex
-- Mathlib.Topology.Algebra.AffineSubspace
AffineSubspace.isClosed_direction_iff : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring R] [inst_1 : AddCommGroup V] [inst_2 : Module R V]
  [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P] [inst_5 : TopologicalSpace V] [IsTopologicalAddTorsor P]
  [T1Space V] (s : AffineSubspace R P), IsClosed ↑s.direction ↔ IsClosed ↑s
-- Mathlib.Topology.Category.CompHausLike.Limits
/-- The pullback cone whose cone point is the explicit pullback.
 -/
CompHausLike.pullback.cone : {P : TopCat → Prop} →
  {X Y B : CompHausLike P} →
    (f : X ⟶ B) → (g : Y ⟶ B) → [CompHausLike.HasExplicitPullback f g] → CategoryTheory.Limits.PullbackCone f g
-- Mathlib.LinearAlgebra.Determinant
/-- If `M` and `M'` are each other's inverse matrices, they are square matrices up to
equivalence of types.  -/
Matrix.indexEquivOfInv : {A : Type u_5} →
  [inst : CommRing A] →
    {m : Type u_6} →
      {n : Type u_7} →
        [inst_1 : Fintype m] →
          [inst_2 : Fintype n] →
            [Nontrivial A] →
              [inst_4 : DecidableEq m] →
                [inst_5 : DecidableEq n] → {M : Matrix m n A} → {M' : Matrix n m A} → M * M' = 1 → M' * M = 1 → m ≃ n
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
/-- The isomorphism between `ValueGroupWithZero R` and `ValueGroup₀ (valuation R)`.  -/
ValuativeRel.ValueGroupWithZero.valueGroupWithZero_equiv_valueGroup₀ : {R : Type u_2} →
  [inst : Ring R] →
    [inst_1 : ValuativeRel R] →
      ValuativeRel.ValueGroupWithZero R ≃*o (MonoidWithZeroHom.ofClass (ValuativeRel.valuation R)).ValueGroup₀
-- Mathlib.RingTheory.GradedAlgebra.RingHom
GradedRingHom.coe_id : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_6} [inst : Semiring A] [inst_1 : SetLike σ A] {𝒜 : ι → σ},
  ⇑(GradedRingHom.id 𝒜) = id
-- Std.Data.Internal.List.Associative
Std.Internal.List.self_le_maxKey?_insertEntry : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] [inst_2 : BEq α] [inst_3 : Std.LawfulBEqOrd α]
  {k : α} {v : β k} {l : List ((a : α) × β a)} (hd : Std.Internal.List.DistinctKeys l) {kmi : α},
  (Std.Internal.List.maxKey? (Std.Internal.List.insertEntry k v l)).get ⋯ = kmi → (compare k kmi).isLE = true
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.ChangeAnnotationSupport.mk.injEq : ∀ (groupsOnLabel? groupsOnLabel?_1 : Option Bool),
  ({ groupsOnLabel? := groupsOnLabel? } = { groupsOnLabel? := groupsOnLabel?_1 }) = (groupsOnLabel? = groupsOnLabel?_1)
-- Mathlib.MeasureTheory.Measure.Real
MeasureTheory.measureReal_sdiff_le_iff_le_add : ∀ {α : Type u_1} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
  MeasurableSet s →
    s ⊆ t →
      ∀ (ε : ℝ),
        autoParam (μ t ≠ ⊤) MeasureTheory.measureReal_sdiff_le_iff_le_add._auto_1 →
          (μ.real (t \ s) ≤ ε ↔ μ.real t ≤ μ.real s + ε)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getKey!_alter : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  [inst : Inhabited α] (h : t.WF) {k k' : α} {f : Option β → Option β},
  (Std.DTreeMap.Internal.Impl.Const.alter k f t ⋯).impl.getKey! k' =
    if compare k k' = Ordering.eq then
      if (f (Std.DTreeMap.Internal.Impl.Const.get? t k)).isSome = true then k else default
    else t.getKey! k'
-- Mathlib.Logic.Equiv.Defs
/-- The forward map of an equivalence.

Do NOT use directly. Use the coercion instead.  -/
Equiv.toFun : {α : Sort u_1} → {β : Sort u_2} → α ≃ β → α → β
-- Aesop.Script.Step
_private.Aesop.Script.Step.0.Aesop.Script.LazyStep.runFirstSuccessfulTacticBuilder.tryTacticBuilder : Aesop.Script.LazyStep → Aesop.Script.TacticBuilder → Lean.MetaM (Option Aesop.Script.Tactic)
-- Mathlib.Analysis.Normed.Ring.Basic
/-- A mixin class with the axiom `‖1‖ = 1`. Many `NormedRing`s and all `NormedField`s satisfy this
axiom.  -/
NormOneClass : (α : Type u_5) → [Norm α] → [One α] → Prop
-- Mathlib.Geometry.Euclidean.Projection
/-- A condition for two points to have the same orthogonal projection onto a given subspace.  -/
EuclideanGeometry.orthogonalProjection_eq_orthogonalProjection_iff_vsub_mem : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup V]
  [inst_2 : InnerProductSpace 𝕜 V] [inst_3 : MetricSpace P] [inst_4 : NormedAddTorsor V P] {s : AffineSubspace 𝕜 P}
  [inst_5 : Nonempty ↥s] [inst_6 : s.direction.HasOrthogonalProjection] {p q : P},
  (EuclideanGeometry.orthogonalProjection s) p = (EuclideanGeometry.orthogonalProjection s) q ↔ p -ᵥ q ∈ s.directionᗮ
-- Init.Data.SInt.Lemmas
Int32.ofIntTruncate_int8ToInt : ∀ (x : Int8), Int32.ofIntClamp x.toInt = x.toInt32
-- Mathlib.Topology.Algebra.OpenSubgroup
/-- Reinterpret an `OpenSubgroup` as a `Subgroup`.  -/
OpenSubgroup.toSubgroup : {G : Type u_1} → [inst : Group G] → [inst_1 : TopologicalSpace G] → OpenSubgroup G → Subgroup G
-- Mathlib.Topology.Instances.Rat
Rat.dist_eq : ∀ (x y : ℚ), dist x y = |↑x - ↑y|
-- Mathlib.Algebra.Group.UniqueProds.Basic
/-- `UniqueAdd` is preserved under embeddings that are additive.

See `UniqueAdd.addHom_image_iff` for a version with swapped bundling.  -/
UniqueAdd.addHom_map_iff : ∀ {G : Type u_1} {H : Type u_2} [inst : Add G] [inst_1 : Add H] {A B : Finset G} {a0 b0 : G} (f : G ↪ H),
  (∀ (x y : G), f (x + y) = f x + f y) →
    (UniqueAdd (Finset.map f A) (Finset.map f B) (f a0) (f b0) ↔ UniqueAdd A B a0 b0)
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.φ_iterate_apply : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : MulSemiringAction (Multiplicative ℕ) R] (n : ℕ) (a : R),
  (⇑SkewPolynomial.φ)^[n] a = Multiplicative.ofAdd n • a
-- Mathlib.Data.Bool.Set
Bool.compl_singleton : ∀ (b : Bool), {b}ᶜ = {!b}
-- Mathlib.MeasureTheory.Function.AEEqFun
/-- The `MulHom` from the group of continuous maps from `α` to `β` to the group of equivalence
classes of `μ`-almost-everywhere measurable functions.  -/
ContinuousMap.toAEEqFunMulHom : {α : Type u_1} →
  {β : Type u_2} →
    [inst : MeasurableSpace α] →
      (μ : MeasureTheory.Measure α) →
        [inst_1 : TopologicalSpace α] →
          [BorelSpace α] →
            [inst_3 : TopologicalSpace β] →
              [SecondCountableTopologyEither α β] →
                [TopologicalSpace.PseudoMetrizableSpace β] →
                  [inst_6 : Group β] → [inst_7 : IsTopologicalGroup β] → C(α, β) →* α →ₘ[μ] β
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
WeierstrassCurve.Jacobian.Point.toAffine_of_Z_ne_zero : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Jacobian F} {P : Fin 3 → F} (hP : W.Nonsingular P)
  (hPz : P 2 ≠ 0),
  WeierstrassCurve.Jacobian.Point.toAffine W P = WeierstrassCurve.Affine.Point.some (P 0 / P 2 ^ 2) (P 1 / P 2 ^ 3) ⋯
-- Mathlib.Analysis.Complex.Order
Complex.nonneg_iff : ∀ {z : ℂ}, 0 ≤ z ↔ 0 ≤ z.re ∧ 0 = z.im
-- Mathlib.Algebra.Lie.Normalizer
LieSubalgebra.lie_mem_sup_of_mem_normalizer : ∀ {R : Type u_1} {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  {H : LieSubalgebra R L} {x y z : L},
  x ∈ H.normalizer → y ∈ R ∙ x ⊔ H.toSubmodule → z ∈ R ∙ x ⊔ H.toSubmodule → ⁅y, z⁆ ∈ R ∙ x ⊔ H.toSubmodule
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
/-- A morphism of snake inputs involve four morphisms of short complexes
which make the obvious diagram commute.  -/
CategoryTheory.ShortComplex.SnakeInput.Hom : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      CategoryTheory.ShortComplex.SnakeInput C → CategoryTheory.ShortComplex.SnakeInput C → Type v_1
-- Mathlib.Tactic.Push.Attr
Mathlib.Tactic.Push.Head.lambda.sizeOf_spec : sizeOf Mathlib.Tactic.Push.Head.lambda = 1
-- Mathlib.Topology.Bases
TopologicalSpace.IsTopologicalBasis.exists_nonempty_subset : ∀ {α : Type u} [t : TopologicalSpace α] {B : Set (Set α)},
  TopologicalSpace.IsTopologicalBasis B → ∀ {u : Set α}, u.Nonempty → IsOpen u → ∃ v ∈ B, v.Nonempty ∧ v ⊆ u
-- Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
SummationFilter.support_eq_limsInf : ∀ {β : Type u_2} (L : SummationFilter β), L.support = (Filter.map SetLike.coe L.filter).limsInf
-- Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
IsBoundedLinearMap.sub : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : Semiring 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : Module 𝕜 E] [inst_3 : SeminormedAddCommGroup F] [inst_4 : Module 𝕜 F] {f g : E → F},
  IsBoundedLinearMap 𝕜 f → IsBoundedLinearMap 𝕜 g → IsBoundedLinearMap 𝕜 fun e => f e - g e
-- Mathlib.Data.Fin.Tuple.Take
/-- Version of `take_addCases_left` that specializes `addCases` to `append`.  -/
Fin.take_append_left : ∀ {n n' : ℕ} {α : Sort u_2} (m : ℕ) (h : m ≤ n) (u : Fin n → α) (v : Fin n' → α),
  Fin.take m ⋯ (Fin.append u v) = Fin.take m h u
-- Mathlib.RingTheory.HopfAlgebra.MonoidAlgebra
AddMonoidAlgebra.instHopfAlgebraStruct.eq_1 : ∀ (R : Type u_1) (A : Type u_2) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : HopfAlgebra R A] (G : Type u_3)
  [inst_3 : AddGroup G],
  AddMonoidAlgebra.instHopfAlgebraStruct R A G =
    { toBialgebra := AddMonoidAlgebra.instBialgebra R A G,
      antipode :=
        ((Finsupp.lsum R) fun g => AddMonoidAlgebra.lsingle (-g) ∘ₗ HopfAlgebraStruct.antipode R) ∘ₗ
          ↑(AddMonoidAlgebra.coeffLinearEquiv R) }
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.get!_eq_getElem! : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : Inhabited β]
  {a : α}, m.get! a = m[a]!
-- Lean.Elab.Import
Lean.Elab.printImports : String → Option String → IO Unit
-- Mathlib.NumberTheory.NumberField.Ideal.Basic
IsPrimitiveRoot.not_coprime_norm_of_mk_eq_one : ∀ {K : Type u_1} [inst : Field K] {I : Ideal (NumberField.RingOfIntegers K)} [inst_1 : NumberField K],
  Ideal.absNorm I ≠ 1 →
    ∀ {n : ℕ} {ζ : K} (hn : 2 ≤ n) (hζ : IsPrimitiveRoot ζ n),
      (Ideal.Quotient.mk I) hζ.toInteger = 1 → ¬(Ideal.absNorm I).Coprime n
-- Std.Async.Process
/-- Gets the title of the current process.
 -/
Std.IO.Process.getProcessTitle : IO String
-- Mathlib.Algebra.Group.Subgroup.MulOpposite
/-- Pull an opposite additive subgroup back to an additive subgroup along `AddOpposite.op`  -/
AddSubgroup.unop : {G : Type u_2} → [inst : AddGroup G] → AddSubgroup Gᵃᵒᵖ → AddSubgroup G
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKeyD_eq_getD_getKey? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {a fallback : α}, t.getKeyD a fallback = (t.getKey? a).getD fallback
-- Mathlib.Probability.Independence.BoundedContinuousFunction
/-- A sigma-algebra $\mathcal{A}$ and a random variable $X$ are independent
if for all set $A \in \mathcal{A}$ and for all real bounded continuous function $f$,
$$P[\mathbb{I}_A f(X)] = P(A) P[f(X)].$$  -/
indep_comap_of_bcf : ∀ {Ω : Type u_1} {m mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {G : Type u_6} [inst : TopologicalSpace G]
  [inst_1 : MeasurableSpace G] [BorelSpace G] [HasOuterApproxClosed G] {Z : Ω → G}
  [MeasureTheory.IsProbabilityMeasure P],
  m ≤ mΩ →
    AEMeasurable Z P →
      (∀ (A : Set Ω),
          MeasurableSet A →
            ∀ (f : BoundedContinuousFunction G ℝ), ∫ (ω : Ω) in A, f (Z ω) ∂P = P.real A * ∫ (ω : Ω), f (Z ω) ∂P) →
        ProbabilityTheory.Indep m (MeasurableSpace.comap Z inferInstance) P
-- Mathlib.MeasureTheory.Function.EssSup
ae_lt_of_essSup_lt : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : ConditionallyCompleteLinearOrder β] {x : β} {f : α → β},
  essSup f μ < x →
    autoParam (Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (MeasureTheory.ae μ) f) ae_lt_of_essSup_lt._auto_1 →
      ∀ᵐ (y : α) ∂μ, f y < x
-- Mathlib.Topology.Compactness.CountablyCompact
/-- A countably compact Lindelöf space is compact.  -/
LindelofSpace.compactSpace : ∀ {X : Type u_4} [inst : TopologicalSpace X] [LindelofSpace X] [h : CountablyCompactSpace X], CompactSpace X
-- Lean.Meta.Tactic.Grind.EMatchTheorem
_private.Lean.Meta.Tactic.Grind.EMatchTheorem.0.Lean.Meta.Grind.Collector.State.mk.sizeOf_spec : ∀ (patterns : Array Lean.Expr) (done : Bool),
  sizeOf { patterns := patterns, done := done } = 1 + sizeOf patterns + sizeOf done
-- Mathlib.Algebra.Category.ModuleCat.Biproducts
/-- We verify that the biproduct in `ModuleCat R` is isomorphic to
the Cartesian product of the underlying types:
 -/
ModuleCat.biprodIsoProd : {R : Type u} → [inst : Ring R] → (M N : ModuleCat R) → M ⊞ N ≅ ModuleCat.of R (↑M × ↑N)
-- Mathlib.Topology.Algebra.Module.ClosedSubmodule
ClosedSubmodule.coe_toCloseds : ∀ {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : TopologicalSpace M]
  [inst_3 : Module R M] (s : ClosedSubmodule R M), ↑↑s = ↑s