mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Measure.ProbabilityMeasure
/-- A probability measure can be interpreted as a finite measure.  -/
MeasureTheory.ProbabilityMeasure.toFiniteMeasure : {Ω : Type u_1} → [inst : MeasurableSpace Ω] → MeasureTheory.ProbabilityMeasure Ω → MeasureTheory.FiniteMeasure Ω
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.aroots_pow : ∀ {S : Type v} {T : Type w} [inst : CommRing T] [inst_1 : CommRing S] [inst_2 : IsDomain S] [inst_3 : Algebra T S]
  (p : Polynomial T) (n : ℕ), (p ^ n).aroots S = n • p.aroots S
-- Mathlib.Order.Interval.Finset.Box
Int.mem_box : ∀ {x : ℤ × ℤ} {n : ℕ}, x ∈ Finset.box n ↔ max x.1.natAbs x.2.natAbs = n
-- Mathlib.Analysis.Normed.Operator.Mul
ContinuousLinearMap.opNNNorm_lsmul : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] (R : Type u_3) [inst_3 : NormedDivisionRing R] [inst_4 : NormedAlgebra 𝕜 R]
  [inst_5 : Module R E] [inst_6 : NormSMulClass R E] [inst_7 : IsScalarTower 𝕜 R E] [Nontrivial E],
  ‖ContinuousLinearMap.lsmul 𝕜 R‖₊ = 1
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
SimpleGraph.extend_finset_to_connected : ∀ {V : Type u} {G : SimpleGraph V},
  G.Preconnected → ∀ {t : Finset V}, t.Nonempty → ∃ t', t ⊆ t' ∧ (SimpleGraph.induce (↑t') G).Connected
-- Mathlib.CategoryTheory.Sites.Descent.DescentData
CategoryTheory.Pseudofunctor.DescentData.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} →
      {ι : Type t} →
        {S : C} →
          {X : ι → C} →
            {f : (i : ι) → X i ⟶ S} →
              (obj : (i : ι) → ↑(F.obj { as := Opposite.op (X i) })) →
                (hom :
                    ⦃Y : C⦄ →
                      (q : Y ⟶ S) →
                        ⦃i₁ i₂ : ι⦄ →
                          (f₁ : Y ⟶ X i₁) →
                            (f₂ : Y ⟶ X i₂) →
                              autoParam (CategoryTheory.CategoryStruct.comp f₁ (f i₁) = q)
                                  CategoryTheory.Pseudofunctor.DescentData._auto_1 →
                                autoParam (CategoryTheory.CategoryStruct.comp f₂ (f i₂) = q)
                                    CategoryTheory.Pseudofunctor.DescentData._auto_3 →
                                  ((F.map f₁.op.toLoc).toFunctor.obj (obj i₁) ⟶
                                    (F.map f₂.op.toLoc).toFunctor.obj (obj i₂))) →
                  autoParam
                      (∀ ⦃Y' Y : C⦄ (g : Y' ⟶ Y) (q : Y ⟶ S) (q' : Y' ⟶ S)
                        (hq : CategoryTheory.CategoryStruct.comp g q = q') ⦃i₁ i₂ : ι⦄ (f₁ : Y ⟶ X i₁) (f₂ : Y ⟶ X i₂)
                        (hf₁ : CategoryTheory.CategoryStruct.comp f₁ (f i₁) = q)
                        (hf₂ : CategoryTheory.CategoryStruct.comp f₂ (f i₂) = q) (gf₁ : Y' ⟶ X i₁) (gf₂ : Y' ⟶ X i₂)
                        (hgf₁ : CategoryTheory.CategoryStruct.comp g f₁ = gf₁)
                        (hgf₂ : CategoryTheory.CategoryStruct.comp g f₂ = gf₂),
                        CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.pullHom (hom q f₁ f₂ ⋯ ⋯) g gf₁ gf₂ ⋯ ⋯ =
                          hom q' gf₁ gf₂ ⋯ ⋯)
                      CategoryTheory.Pseudofunctor.DescentData.pullHom_hom._autoParam →
                    autoParam
                        (∀ ⦃Y : C⦄ (q : Y ⟶ S) ⦃i : ι⦄ (g : Y ⟶ X i)
                          (x : CategoryTheory.CategoryStruct.comp g (f i) = q),
                          hom q g g ⋯ ⋯ = CategoryTheory.CategoryStruct.id ((F.map g.op.toLoc).toFunctor.obj (obj i)))
                        CategoryTheory.Pseudofunctor.DescentData.hom_self._autoParam →
                      autoParam
                          (∀ ⦃Y : C⦄ (q : Y ⟶ S) ⦃i₁ i₂ i₃ : ι⦄ (f₁ : Y ⟶ X i₁) (f₂ : Y ⟶ X i₂) (f₃ : Y ⟶ X i₃)
                            (hf₁ : CategoryTheory.CategoryStruct.comp f₁ (f i₁) = q)
                            (hf₂ : CategoryTheory.CategoryStruct.comp f₂ (f i₂) = q)
                            (hf₃ : CategoryTheory.CategoryStruct.comp f₃ (f i₃) = q),
                            CategoryTheory.CategoryStruct.comp (hom q f₁ f₂ hf₁ hf₂) (hom q f₂ f₃ hf₂ hf₃) =
                              hom q f₁ f₃ hf₁ hf₃)
                          CategoryTheory.Pseudofunctor.DescentData.hom_comp._autoParam →
                        F.DescentData f
-- Mathlib.LinearAlgebra.TensorProduct.Basis
/-- The lift of an `R`-basis of `M` to an `S`-basis of the base change `S ⊗[R] M`.  -/
Module.Basis.baseChange : {R : Type u_1} →
  {M : Type u_3} →
    {ι : Type u_5} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : Module R M] →
            (S : Type u_7) →
              [inst_3 : Semiring S] →
                [inst_4 : Algebra R S] → Module.Basis ι R M → Module.Basis ι S (TensorProduct R S M)
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
SimpleGraph.coe_recolorOfEquiv : ∀ {V : Type u} (G : SimpleGraph V) {α : Type u_2} {β : Type u_3} (f : α ≃ β),
  ⇑(G.recolorOfEquiv f) = (SimpleGraph.Embedding.completeGraph f.toEmbedding).toHom.comp
-- Mathlib.CategoryTheory.Pi.Basic
CategoryTheory.Functor.eqToHom_proj : ∀ {I : Type w₀} {C : I → Type u₁} [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {x x' : (i : I) → C i}
  (h : x = x') (i : I), CategoryTheory.eqToHom h i = CategoryTheory.eqToHom ⋯
-- Init.Data.UInt.Lemmas
UInt8.sub_self : ∀ (a : UInt8), a - a = 0
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
/-- The canonical injection of G's generators into G  -/
IsFreeAddGroup.of : {G : Type u_1} → [inst : AddGroup G] → [inst_1 : IsFreeAddGroup G] → IsFreeAddGroup.Generators G → G
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
CategoryTheory.Limits.limitFlipIsoCompLim_hom_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} J]
  {K : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} K] [inst_3 : CategoryTheory.Limits.HasLimitsOfShape J C]
  (F : CategoryTheory.Functor K (CategoryTheory.Functor J C)) (X : K),
  (CategoryTheory.Limits.limitFlipIsoCompLim F).hom.app X =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limitObjIsoLimitCompEvaluation F.flip X).hom
      (CategoryTheory.Limits.HasLimit.isoOfNatIso (CategoryTheory.flipCompEvaluation F X)).hom
-- Mathlib.Algebra.Group.Hom.Defs
/-- Makes a `OneHom` inverse from the bijective inverse of a `OneHom`  -/
OneHom.inverse : {M : Type u_4} →
  {N : Type u_5} →
    [inst : One M] → [inst_1 : One N] → (f : OneHom M N) → (g : N → M) → Function.LeftInverse g ⇑f → OneHom N M
-- Lean.Util.MonadBacktrack
Lean.commitIfNoEx : {m : Type → Type} →
  {s : Type} → {ε : Type u_1} → {α : Type} → [Monad m] → [Lean.MonadBacktrack s m] → [MonadExcept ε m] → m α → m α
-- Lean.LocalContext
/-- Invisible to type class search or tactics, and hidden in the goal display.

This kind is used for temporary variables in macros.
For example: `return (← foo) + bar` expands to
`foo >>= fun __tmp => pure (__tmp + bar)`,
where `__tmp` has the `implDetail` kind.
 -/
Lean.LocalDeclKind.implDetail : Lean.LocalDeclKind
-- Mathlib.RingTheory.Idempotents
/-- A family of complete orthogonal idempotents induces an isomorphism `R ≃+* ∏ R ⧸ ⟨1 - eᵢ⟩`  -/
CompleteOrthogonalIdempotents.bijective_pi : ∀ {R : Type u_1} [inst : CommRing R] {I : Type u_3} [inst_1 : Fintype I] {e : I → R},
  CompleteOrthogonalIdempotents e → Function.Bijective ⇑(RingHom.pi fun i => Ideal.Quotient.mk (Ideal.span {1 - e i}))
-- Mathlib.Order.Filter.Ultrafilter.Defs
Ultrafilter.coe_inj : ∀ {α : Type u} {f g : Ultrafilter α}, ↑f = ↑g ↔ f = g
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.Path.ordered_iff : ∀ {α : Type u_1} {cmp : α → α → Ordering} {p : RBTree.RBNode.Path α},
  RBTree.RBNode.Path.Ordered cmp p ↔
    List.Pairwise (RBTree.RBNode.cmpLT cmp) p.listL ∧
      List.Pairwise (RBTree.RBNode.cmpLT cmp) p.listR ∧ ∀ x ∈ p.listL, ∀ y ∈ p.listR, RBTree.RBNode.cmpLT cmp x y
-- Std.Time.Format.Modifier
/-- `Y`: ISO week-based year (e.g., 2004, 04, 0002, 2). This is the year that contains the ISO week (`w`), which can
differ from the calendar year near year boundaries: e.g., Dec 31 may belong to week 1 of the following year.
 -/
Std.Time.Modifier.Y : Std.Time.Year → Std.Time.Modifier
-- Mathlib.Topology.EMetricSpace.Defs
zero_eq_edist : ∀ {γ : Type w} [inst : EMetricSpace γ] {x y : γ}, 0 = edist x y ↔ x = y
-- Mathlib.Topology.UniformSpace.Equicontinuity
/-- If a set of functions is uniformly equicontinuous, its closure for the product topology is also
uniformly equicontinuous.  -/
Set.UniformEquicontinuous.closure : ∀ {α : Type u_6} {β : Type u_8} [uα : UniformSpace α] [uβ : UniformSpace β] {A : Set (β → α)},
  A.UniformEquicontinuous → (closure A).UniformEquicontinuous
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.eq_of_add_eq_add_left : ∀ {a b c : Cardinal.{u_1}}, a + b = a + c → a < Cardinal.aleph0 → b = c
-- Mathlib.Algebra.Category.Ring.Colimits
RingCat.Colimits.Relation.below.right_distrib : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J RingCat}
  {motive : (a a_1 : RingCat.Colimits.Prequotient F) → RingCat.Colimits.Relation F a a_1 → Prop}
  (x y z : RingCat.Colimits.Prequotient F), RingCat.Colimits.Relation.below ⋯
-- Mathlib.Data.Nat.GCD.Basic
Nat.Coprime.dvd_mul_left : ∀ {m n k : ℕ}, k.Coprime m → (k ∣ m * n ↔ k ∣ n)
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.Opens.range_ι : ∀ {X : AlgebraicGeometry.Scheme} (U : X.Opens), Set.range ⇑U.ι = ↑U
-- Mathlib.Analysis.CStarAlgebra.Basic
starₗᵢ_apply : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : CommSemiring 𝕜] [inst_1 : StarRing 𝕜] [inst_2 : SeminormedAddCommGroup E]
  [inst_3 : StarAddMonoid E] [inst_4 : NormedStarGroup E] [inst_5 : Module 𝕜 E] [inst_6 : StarModule 𝕜 E] {x : E},
  (starₗᵢ 𝕜) x = star x
-- Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
restrictRootsOfUnity.congr_simp : ∀ {R : Type u_4} {S : Type u_5} {F : Type u_6} [inst : CommMonoid R] [inst_1 : CommMonoid S] [inst_2 : FunLike F R S]
  [inst_3 : MonoidHomClass F R S] (σ σ_1 : F),
  σ = σ_1 → ∀ (n : ℕ), restrictRootsOfUnity σ n = restrictRootsOfUnity σ_1 n
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.map_zero : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4}
  [inst_2 : TopologicalSpace M₁] [inst_3 : AddCommMonoid M₁] {M₂ : Type u_6} [inst_4 : TopologicalSpace M₂]
  [inst_5 : AddCommMonoid M₂] [inst_6 : Module R₁ M₁] [inst_7 : Module R₂ M₂] (f : M₁ →SL[σ₁₂] M₂), f 0 = 0
-- Init.Data.String.Hashable
String.instHashablePos : {s : String} → Hashable s.Pos
-- Mathlib.SetTheory.Ordinal.Notation
ONote.oadd_mul : ∀ (e₁ : ONote) (n₁ : ℕ+) (a₁ e₂ : ONote) (n₂ : ℕ+) (a₂ : ONote),
  e₁.oadd n₁ a₁ * e₂.oadd n₂ a₂ = if e₂ = 0 then e₁.oadd (n₁ * n₂) a₁ else (e₁ + e₂).oadd n₂ (e₁.oadd n₁ a₁ * a₂)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.map_fst_toArray_eq_keysArray : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp},
  Array.map Prod.fst (Std.DTreeMap.Raw.Const.toArray t) = t.keysArray
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
/-- If the angle between three points is π, they are collinear.  -/
EuclideanGeometry.collinear_of_angle_eq_pi : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {p₁ p₂ p₃ : P}, EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi → Collinear ℝ {p₁, p₂, p₃}
-- Mathlib.Data.PNat.Basic
PNat.instCancelCommMonoid : CancelCommMonoid ℕ+
-- Mathlib.AlgebraicGeometry.StructureSheaf
AlgebraicGeometry.StructureSheaf.comap_id' : ∀ {R : Type u} [inst : CommRing R] (U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)),
  AlgebraicGeometry.StructureSheaf.comap (RingHom.id R) U U ⋯ =
    RingHom.id ↑((AlgebraicGeometry.Spec.structureSheaf R).obj.obj (Opposite.op U))
-- Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
RestrictedProduct.isOpen_forall_mem : ∀ {ι : Type u_1} {R : ι → Type u_2} {A : (i : ι) → Set (R i)} [inst : (i : ι) → TopologicalSpace (R i)],
  (∀ (i : ι), IsOpen (A i)) → IsOpen {f | ∀ (i : ι), ↑f i ∈ A i}
-- Mathlib.CategoryTheory.ComposableArrows.Basic
/-- Constructor for `ComposableArrows C 3`.  -/
CategoryTheory.ComposableArrows.mk₃ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {X₀ X₁ X₂ X₃ : C} → (X₀ ⟶ X₁) → (X₁ ⟶ X₂) → (X₂ ⟶ X₃) → CategoryTheory.ComposableArrows C 3
-- Mathlib.Data.Bundle
Bundle.TotalSpace.toProd_symm_apply_snd : ∀ (B : Type u_4) (F : Type u_5) (x : B × F), ((Bundle.TotalSpace.toProd B F).symm x).snd = x.2
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.StrongEpiMonoFactorisation.mk.sizeOf_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} [inst_1 : SizeOf C]
  (toMonoFactorisation : CategoryTheory.Limits.MonoFactorisation f)
  [e_strong_epi : CategoryTheory.StrongEpi toMonoFactorisation.e],
  sizeOf { toMonoFactorisation := toMonoFactorisation, e_strong_epi := e_strong_epi } =
    1 + sizeOf toMonoFactorisation + sizeOf e_strong_epi
-- Init.Core
Array.mk.injEq : ∀ {α : Type u} (toList toList_1 : List α), ({ toList := toList } = { toList := toList_1 }) = (toList = toList_1)
-- Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
/-- **Alias** of `smul_apply`. -/
UniformConvergenceCLM.smul_apply : ∀ {M : Type u_1} {F : Type u_2} {α : outParam (Type u_3)} {β : outParam (Type u_4)} {inst : FunLike F α β}
  {inst_1 : SMul M β} {inst_2 : SMul M F} [self : IsSMulApply M F α β] (f : F) (r : M) (x : α), (r • f) x = r • f x
-- Lean.Message
/-- Returns the top-level tag of the message.
If none, returns `Name.anonymous`.

This does not descend into message subtrees (e.g., `.compose`, `.ofLazy`).
The message kind is expected to describe the whole message.
 -/
Lean.MessageData.kind : Lean.MessageData → Lean.Name
-- Lean.Meta.SizeOf
Lean.Meta.SizeOfSpecNested.Context.sizeOfFns : Lean.Meta.SizeOfSpecNested.Context → Array Lean.Name
-- Mathlib.Analysis.Convex.Join
Convex.convexHull_union : ∀ {𝕜 : Type u_2} {E : Type u_3} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] {s t : Set E},
  Convex 𝕜 s → Convex 𝕜 t → s.Nonempty → t.Nonempty → (convexHull 𝕜) (s ∪ t) = convexJoin 𝕜 s t
-- Aesop.Search.Expansion.Norm
Aesop.getResetForwardState : Aesop.NormM Aesop.ForwardState
-- Mathlib.Order.Interval.Finset.Box
Finset.box_succ_disjUnion : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : PartialOrder α] [inst_2 : IsOrderedRing α] [inst_3 : LocallyFiniteOrder α]
  [inst_4 : DecidableEq α] (n : ℕ),
  (Finset.box (n + 1)).disjUnion (Finset.Icc (-↑n) ↑n) ⋯ = Finset.Icc (-↑n.succ) ↑n.succ
-- Mathlib.Tactic.IntervalCases
/-- The target expression, a numeral in the input type  -/
Mathlib.Tactic.IntervalCases.IntervalCasesSubgoal.rhs : Mathlib.Tactic.IntervalCases.IntervalCasesSubgoal → Lean.Expr
-- Mathlib.Analysis.Seminorm
Seminorm.ball_eq_emptyset : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  (p : Seminorm 𝕜 E) {x : E} {r : ℝ}, r ≤ 0 → p.ball x r = ∅
-- Mathlib.Data.NNRat.Defs
NNRat.coe_divNat : ∀ (n d : ℕ), ↑(NNRat.divNat n d) = Rat.divInt ↑n ↑d
-- Mathlib.Analysis.LConvolution
/-- Additive convolution of functions  -/
MeasureTheory.lconvolution : {G : Type u_1} →
  {mG : MeasurableSpace G} → [Add G] → [Neg G] → (G → ENNReal) → (G → ENNReal) → MeasureTheory.Measure G → G → ENNReal
-- Mathlib.GroupTheory.NoncommPiCoprod
/-- The universal property of `MonoidHom.noncommPiCoprod`

Given monoid morphisms `φᵢ : Nᵢ → M` whose images pairwise commute,
there exists a unique monoid morphism `φ : Πᵢ Nᵢ → M` that induces the `φᵢ`,
and it is given by `AddMonoidHom.noncommPiCoprod`.  -/
AddMonoidHom.noncommPiCoprodEquiv : {M : Type u_1} →
  [inst : AddMonoid M] →
    {ι : Type u_2} →
      [Fintype ι] →
        {N : ι → Type u_3} →
          [inst_2 : (i : ι) → AddMonoid (N i)] →
            [DecidableEq ι] →
              { ϕ // Pairwise fun i j => ∀ (x : N i) (y : N j), AddCommute ((ϕ i) x) ((ϕ j) y) } ≃
                (((i : ι) → N i) →+ M)
-- Mathlib.Topology.MetricSpace.Contracting
/-- Let `f` be a contracting map with constant `K`; let `g` be another map uniformly
`C`-close to `f`. If `x` and `y` are their fixed points, then `dist x y ≤ C / (1 - K)`.  -/
ContractingWith.dist_fixedPoint_fixedPoint_of_dist_le' : ∀ {α : Type u_1} [inst : MetricSpace α] {K : NNReal} {f : α → α},
  ContractingWith K f →
    ∀ (g : α → α) {x y : α},
      Function.IsFixedPt f x →
        Function.IsFixedPt g y → ∀ {C : ℝ}, (∀ (z : α), dist (f z) (g z) ≤ C) → dist x y ≤ C / (1 - ↑K)
-- Init.Grind.Ordered.Ring
OfNat.ofNat.eq_1 : ∀ (α : Type u) (x : ℕ) [self : OfNat α x], OfNat.ofNat x = self.1
-- Mathlib.NumberTheory.Padics.PadicNumbers
Padic.instCharZero : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)], CharZero ℚ_[p]
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.ExProd.mul.injEq : ∀ {u : Lean.Level} {α : Q(Type u)} {BaseType : Q(«$α») → Type} {sα : Q(CommSemiring «$α»)} {x : Q(«$α»)} {e : Q(ℕ)}
  {b : Q(«$α»)} (a : Mathlib.Tactic.Ring.Common.ExBase BaseType sα x) (a_1 : Mathlib.Tactic.Ring.Common.ExProdNat e)
  (a_2 : Mathlib.Tactic.Ring.Common.ExProd BaseType sα b) (a_3 : Mathlib.Tactic.Ring.Common.ExBase BaseType sα x)
  (a_4 : Mathlib.Tactic.Ring.Common.ExProdNat e) (a_5 : Mathlib.Tactic.Ring.Common.ExProd BaseType sα b),
  (Mathlib.Tactic.Ring.Common.ExProd.mul a a_1 a_2 = Mathlib.Tactic.Ring.Common.ExProd.mul a_3 a_4 a_5) =
    (a = a_3 ∧ a_1 = a_4 ∧ a_2 = a_5)
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.lt_rpow_inv_iff_of_neg : ∀ {x y z : ℝ}, 0 < x → 0 < y → z < 0 → (x < y ^ z⁻¹ ↔ y < x ^ z)
-- Lean.Data.Lsp.Internal
Lean.Lsp.LeanIdentifier.mk : Lean.Name → Lean.Name → Bool → Lean.Lsp.LeanIdentifier
-- Mathlib.Data.Prod.Lex
Prod.Lex.instOrientedOrdLex : ∀ {α : Type u_1} {β : Type u_2} [inst : Ord α] [inst_1 : Ord β] [Std.OrientedOrd α] [Std.OrientedOrd β],
  Std.OrientedOrd (Lex (α × β))
-- Lean.Parser.Term
Lean.Parser.Term.waitIfTypeMVar.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.MeasureTheory.Measure.NullMeasurable
MeasureTheory.NullMeasurableSet.biInter : ∀ {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : β → Set α} {s : Set β},
  s.Countable → (∀ b ∈ s, MeasureTheory.NullMeasurableSet (f b) μ) → MeasureTheory.NullMeasurableSet (⋂ b ∈ s, f b) μ
-- Mathlib.AlgebraicGeometry.Cover.Sigma
/-- Collapsing a cover to a single object cover is functorial.  -/
AlgebraicGeometry.Scheme.Cover.sigmaFunctor : {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
  {S : AlgebraicGeometry.Scheme} →
    [AlgebraicGeometry.IsZariskiLocalAtSource P] →
      [UnivLE.{v, u}] →
        CategoryTheory.Functor (AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) S)
          (AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) S)
-- Mathlib.Algebra.Order.Floor.Ring
Int.ceil_div_ceil_inv_sub_one : ∀ {k : Type u_4} [inst : Field k] [inst_1 : LinearOrder k] [IsOrderedRing k] [inst_3 : FloorRing k] {a : k},
  1 ≤ a → ⌈↑⌈(a - 1)⁻¹⌉ / a⌉ = ⌈(a - 1)⁻¹⌉
-- Mathlib.Algebra.Group.Conj
isAddConj_zero_left : ∀ {α : Type u} [inst : AddMonoid α] {a : α}, IsAddConj a 0 ↔ a = 0
-- Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated
/-- The trivial (degenerate) edge at a vertex `x` is a representative for the
identity morphism `x ⟶ x`.
 -/
SSet.Truncated.HomotopyCategory₂.homMk_id : ∀ {A : SSet.Truncated 2} [inst : A.Quasicategory₂] (x : A.HomotopyCategory₂),
  SSet.Truncated.HomotopyCategory₂.homMk (SSet.Truncated.Edge.id x.pt) = CategoryTheory.CategoryStruct.id x
-- Mathlib.Analysis.Real.Sqrt
Real.sqrt_one : √1 = 1
-- Mathlib.Analysis.Convex.StdSimplex
/-- `stdSimplex 𝕜 ι` is the convex hull of the points `Pi.single i 1` for `i : ι`.  -/
convexHull_rangle_single_eq_stdSimplex : ∀ (R : Type u_1) (ι : Type u_2) [inst : Field R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] [inst_3 : Fintype ι]
  [inst_4 : DecidableEq ι], (convexHull R) (Set.range fun i => Pi.single i 1) = stdSimplex R ι
-- Init.Data.Nat.Fold
_private.Init.Data.Nat.Fold.0.Nat.dfold.loop.congr_simp : ∀ (n : ℕ) {α : (i : ℕ) → autoParam (i ≤ n) Nat.dfold._auto_1 → Type u}
  (f f_1 : (i : ℕ) → (h : i < n) → α i ⋯ → α (i + 1) ⋯),
  f = f_1 →
    ∀ (j : ℕ) (a : j ≤ n) (a_1 a_2 : α (n - j) ⋯),
      a_1 = a_2 → Nat.dfold.loop✝ n f j a a_1 = Nat.dfold.loop✝ n f_1 j a a_2
-- Mathlib.MeasureTheory.Covering.VitaliFamily
VitaliFamily.FineSubfamilyOn.covering_disjoint : ∀ {X : Type u_1} [inst : PseudoMetricSpace X] {m0 : MeasurableSpace X} {μ : MeasureTheory.Measure X}
  {v : VitaliFamily μ} {f : X → Set (Set X)} {s : Set X} (h : v.FineSubfamilyOn f s),
  h.index.PairwiseDisjoint h.covering
-- Mathlib.Order.Filter.Ker
Filter.ker_def : ∀ {α : Type u_2} (f : Filter α), f.ker = ⋂ s ∈ f, s
-- Std.Data.TreeMap.Iterator
Std.DTreeMap.Const.toList.eq_1 : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} (t : Std.DTreeMap α (fun x => β) cmp),
  Std.DTreeMap.Const.toList t = Std.DTreeMap.Internal.Impl.Const.toList t.inner
-- Mathlib.Topology.Compactness.Lindelof
Set.Finite.isLindelof : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, s.Finite → IsLindelof s
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.AEEqFun.eLpNorm_compMeasurePreserving : ∀ {α : Type u_1} {E : Type u_4} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] {β : Type u_8} {mβ : MeasurableSpace β} {f : α → β} {ν : MeasureTheory.Measure β}
  (g : β →ₘ[ν] E) (hf : MeasureTheory.MeasurePreserving f μ ν),
  MeasureTheory.eLpNorm (↑(g.compMeasurePreserving f hf)) p μ = MeasureTheory.eLpNorm (↑g) p ν
-- Mathlib.Analysis.Analytic.Basic
HasFPowerSeriesAt.coeff_zero : ∀ {𝕜 : 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}
  {pf : FormalMultilinearSeries 𝕜 E F} {x : E}, HasFPowerSeriesAt f pf x → ∀ (v : Fin 0 → E), (pf 0) v = f x
-- Mathlib.Analysis.Calculus.Deriv.Add
hasDerivWithinAt_const_add_iff : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} {s : Set 𝕜} (c : F),
  HasDerivWithinAt (fun x => c + f x) f' s x ↔ HasDerivWithinAt f f' s x
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Real.arcsin_lt_arcsin : ∀ {x y : ℝ}, -1 ≤ x → x < y → y ≤ 1 → Real.arcsin x < Real.arcsin y
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Matrix.GeneralLinearGroup.injective_upperRightHom : ∀ {R : Type u_1} [inst : Ring R], Function.Injective ⇑Matrix.GeneralLinearGroup.upperRightHom
-- Mathlib.Geometry.Manifold.IsManifold.Basic
ModelWithCorners.mk_symm : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] (e : PartialEquiv H E)
  (a : e.source = Set.univ) (b : if h : IsRCLikeNormedField 𝕜 then Convex ℝ (Set.range ↑e) else Set.range ↑e = Set.univ)
  (c : (interior (Set.range ↑e)).Nonempty) (d : Continuous ↑e) (d' : Continuous e.invFun),
  { toPartialEquiv := e, source_eq := a, convex_range' := b, nonempty_interior' := c, continuous_toFun := d,
        continuous_invFun := d' }.symm =
    e.symm
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.eval_intCast : ∀ {R : Type u} [inst : Ring R] {n : ℤ} {x : R}, Polynomial.eval x ↑n = ↑n
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MulticospanIndex.ofParallelHoms_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.Limits.MulticospanShape) {X Y : C}
  (f g : X ⟶ Y) (x : J.R), (CategoryTheory.Limits.MulticospanIndex.ofParallelHoms J f g).right x = Y