mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
EuclideanSpace.volume_closedBall_fin_three : ∀ (x : EuclideanSpace ℝ (Fin 3)) (r : ℝ),
  MeasureTheory.volume (Metric.closedBall x r) = ENNReal.ofReal r ^ 3 * ENNReal.ofReal (Real.pi * 4 / 3)
-- Mathlib.RingTheory.MvPowerSeries.LinearTopology
/-- The topology on `MvPowerSeries` is a left linear topology
when the ring of coefficients has a linear topology.  -/
MvPowerSeries.LinearTopology.instIsLinearTopologyOfMulOpposite : ∀ {σ : Type u_1} {R : Type u_2} [inst : Ring R] [inst_1 : TopologicalSpace R] [IsLinearTopology R R]
  [IsLinearTopology Rᵐᵒᵖ R], IsLinearTopology (MvPowerSeries σ R) (MvPowerSeries σ R)
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
/-- The second projection in `Cochain (mappingCocone φ) L (-1)`.  -/
CochainComplex.mappingCocone.snd : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {K L : CochainComplex C ℤ} →
        (φ : K ⟶ L) →
          [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] →
            CochainComplex.HomComplex.Cochain (CochainComplex.mappingCocone φ) L (-1)
-- Std.Sat.AIG.If
Std.Sat.AIG.if_as_bool : ∀ (d l r : Bool), (if d = true then l else r) = (d && l || !d && r)
-- Mathlib.Tactic.Linarith.Oracle.FourierMotzkin
/-- The set of original assumptions which have been used in constructing this comparison.  -/
Mathlib.Tactic.Linarith.PComp.history : Mathlib.Tactic.Linarith.PComp → Std.TreeSet ℕ compare
-- Mathlib.Data.W.Constructions
WType.NatαEquivPUnitSumPUnit_symm_apply : ∀ (b : PUnit.{u + 1} ⊕ PUnit.{u_1 + 1}),
  WType.NatαEquivPUnitSumPUnit.symm b =
    match b with
    | Sum.inl val => WType.Natα.zero
    | Sum.inr val => WType.Natα.succ
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.w₀₂_τ₃_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex.SnakeInput C) {Z : C} (h : S.L₂.X₃ ⟶ Z),
  CategoryTheory.CategoryStruct.comp S.v₀₁.τ₃ (CategoryTheory.CategoryStruct.comp S.v₁₂.τ₃ h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.Logic.Unique
Option.instUniqueOfIsEmpty : {α : Type u_2} → [IsEmpty α] → Unique (Option α)
-- Init.Data.Int.DivMod.Lemmas
Int.fmod_one : ∀ (a : ℤ), a.fmod 1 = 0
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.Rel.triangle : ∀ {B : Type u} [inst : Quiver B] {a b c : B} (f : CategoryTheory.FreeBicategory.Hom a b)
  (g : CategoryTheory.FreeBicategory.Hom b c),
  CategoryTheory.FreeBicategory.Rel
    ((CategoryTheory.FreeBicategory.Hom₂.associator f (CategoryTheory.FreeBicategory.Hom.id b) g).vcomp
      (CategoryTheory.FreeBicategory.Hom₂.whisker_left f (CategoryTheory.FreeBicategory.Hom₂.left_unitor g)))
    (CategoryTheory.FreeBicategory.Hom₂.whisker_right g (CategoryTheory.FreeBicategory.Hom₂.right_unitor f))
-- Lean.Meta.Sym.AlphaShareCommon
/-- Returns `true` if `declName` is a reducible constant that the `unfoldReducible`
preprocessing step must unfold.

Projection functions are excluded even though they are `reducible` by default:
unfolding them produces kernel projections, which the `foldProjs` preprocessing
step folds back into projection function applications.
 -/
Lean.Meta.Sym.isUnfoldReducibleCandidate : Lean.Environment → Lean.Name → Bool
-- Mathlib.Analysis.SpecialFunctions.Integrals.Basic
integral_inv_one_add_sq : ∀ {a b : ℝ}, ∫ (x : ℝ) in a..b, (1 + x ^ 2)⁻¹ = Real.arctan b - Real.arctan a
-- Init.Data.String.Basic
String.Pos.Raw.isValidForSlice_stringSlice : ∀ {s : String} {p₀ p₁ : s.Pos} {h : p₀ ≤ p₁} (pos : String.Pos.Raw),
  String.Pos.Raw.IsValidForSlice (s.slice p₀ p₁ h) pos ↔
    pos.offsetBy p₀.offset ≤ p₁.offset ∧ String.Pos.Raw.IsValid s (pos.offsetBy p₀.offset)
-- Mathlib.Algebra.Order.AddGroupWithTop
LinearOrderedAddCommGroupWithTop.top_pos : ∀ {α : Type u_2} [inst : LinearOrderedAddCommGroupWithTop α], 0 < ⊤
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Power.denote.eq_3 : ∀ {α : Type u_1} [inst : Lean.Grind.Semiring α] (ctx : Lean.Grind.CommRing.Context α) (x_1 : Lean.Grind.CommRing.Var)
  (k : ℕ),
  (k = 0 → False) →
    (k = 1 → False) →
      Lean.Grind.CommRing.Power.denote ctx { x := x_1, k := k } = Lean.Grind.CommRing.Var.denote ctx x_1 ^ k
-- Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum
/-- `2` is a square in `F` iff `#F` is not congruent to `3` or `5` mod `8`.  -/
FiniteField.isSquare_two_iff : ∀ {F : Type u_1} [inst : Field F] [inst_1 : Fintype F], IsSquare 2 ↔ Fintype.card F % 8 ≠ 3 ∧ Fintype.card F % 8 ≠ 5
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
/-- The orthogonal projection onto the trivial submodule is the zero map.  -/
Submodule.orthogonalProjectionOnto_bot : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E],
  ⊥.orthogonalProjectionOnto = 0
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.kernelSequenceOpcyclesEIso_hom_τ₂ : ∀ {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) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.kernelSequenceOpcyclesEIso._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.kernelSequenceOpcyclesEIso._auto_3),
  (X.kernelSequenceOpcyclesEIso f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).hom.τ₂ = (X.opcyclesIso f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).inv
-- Mathlib.Algebra.Free
_private.Mathlib.Algebra.Free.0.FreeAddMagma.liftAux.match_1.splitter : {α : Type u_1} →
  (motive : FreeAddMagma α → Sort u_2) →
    (x : FreeAddMagma α) →
      ((x : α) → motive (FreeAddMagma.of x)) → ((x y : FreeAddMagma α) → motive (x.add y)) → motive x
-- Init.Data.List.MinMaxIdx
/-- Returns the index of an element of the non-empty list `xs` that maximizes `f`.
If `x`, `y` are such that `f x = f y`, it returns the index of whichever comes first
in the list.

The correctness of this function assumes `β` to be linearly pre-ordered.
 -/
List.maxIdxOn : {β : Type u_1} → {α : Type u_2} → [inst : LE β] → [DecidableLE β] → (α → β) → (xs : List α) → xs ≠ [] → ℕ
-- Init.Data.Nat.Basic
Nat.instLawfulBEq : LawfulBEq ℕ
-- Mathlib.Probability.Kernel.RadonNikodym
ProbabilityTheory.Kernel.singularPart.congr_simp : ∀ {α : Type u_3} {γ : Type u_4} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ}
  [hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ] (κ κ_1 : ProbabilityTheory.Kernel α γ) (e_κ : κ = κ_1)
  (η η_1 : ProbabilityTheory.Kernel α γ) (e_η : η = η_1) [inst : ProbabilityTheory.IsSFiniteKernel κ]
  [inst_1 : ProbabilityTheory.IsSFiniteKernel η], κ.singularPart η = κ_1.singularPart η_1
-- Mathlib.Data.Nat.MaxPowDiv
Nat.divMaxPow_zero_right : ∀ (n : ℕ), n.divMaxPow 0 = n
-- Mathlib.RingTheory.FractionalIdeal.Basic
FractionalIdeal.mul_le : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  {I J K : FractionalIdeal S P}, I * J ≤ K ↔ ∀ i ∈ I, ∀ j ∈ J, i * j ∈ K
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
WeierstrassCurve.leadingCoeff_Ψ₂Sq : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R), 4 ≠ 0 → W.Ψ₂Sq.leadingCoeff = 4
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.mk : {α : Type u_3} →
  [inst : MeasurableSpace α] →
    {M : Type u_4} →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : TopologicalSpace M] →
          (measureOf' : Set α → M) →
            measureOf' ∅ = 0 →
              (∀ ⦃i : Set α⦄, ¬MeasurableSet i → measureOf' i = 0) →
                (∀ ⦃f : ℕ → Set α⦄,
                    (∀ (i : ℕ), MeasurableSet (f i)) →
                      Pairwise (Function.onFun Disjoint f) →
                        HasSum (fun i => measureOf' (f i)) (measureOf' (⋃ i, f i))) →
                  MeasureTheory.VectorMeasure α M
-- Mathlib.Combinatorics.Quiver.Path.Vertices
/-- The vertex list of `cons` — convenient `simp` form.  -/
Quiver.Path.mem_vertices_cons : ∀ {V : Type u_1} [inst : Quiver V] {a b c : V} (p : Quiver.Path a b) (e : b ⟶ c) {x : V},
  x ∈ (p.cons e).vertices ↔ x ∈ p.vertices ∨ x = c
-- Mathlib.Data.Fin.Tuple.Sort
/-- `graph f` produces the finset of pairs `(f i, i)`
equipped with the lexicographic order.
 -/
Tuple.graph : {n : ℕ} → {α : Type u_1} → [LinearOrder α] → (Fin n → α) → Finset (Lex (α × Fin n))
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CallHierarchyItem.range : Lean.Lsp.CallHierarchyItem → Lean.Lsp.Range
-- Mathlib.Order.Basic
Pi.instHNot : {ι : Type u_1} → {π : ι → Type u_4} → [(i : ι) → HNot (π i)] → HNot ((i : ι) → π i)
-- Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
HomotopicalAlgebra.CofibrantObject.instFullHoCatToHoCat : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C],
  HomotopicalAlgebra.CofibrantObject.toHoCat.Full
-- Mathlib.CategoryTheory.Sites.Grothendieck
CategoryTheory.GrothendieckTopology.right_ore_of_pullbacks : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPullbacks C],
  CategoryTheory.GrothendieckTopology.RightOreCondition C
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Op
/-- If `P` is a pairing for a subcomplex `A` of a simplicial set `X`,
this is the corresponding pairing of `A.op`.  -/
SSet.Subcomplex.Pairing.op : {X : SSet} → {A : X.Subcomplex} → A.Pairing → A.op.Pairing
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
/-- Given that the top square is a pushout, the pasted square is a pushout iff the bottom square is.
 -/
CategoryTheory.Limits.pasteVertIsPushoutEquiv : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {Y₃ Y₂ Y₁ X₃ : C} →
      {g₂ : Y₃ ⟶ Y₂} →
        {g₁ : Y₂ ⟶ Y₁} →
          {i₃ : Y₃ ⟶ X₃} →
            {t₁ : CategoryTheory.Limits.PushoutCocone g₂ i₃} →
              {i₂ : Y₂ ⟶ t₁.pt} →
                (t₂ : CategoryTheory.Limits.PushoutCocone g₁ i₂) →
                  (hi₂ : i₂ = t₁.inl) →
                    CategoryTheory.Limits.IsColimit t₁ →
                      CategoryTheory.Limits.IsColimit (t₁.pasteVert t₂ hi₂) ≃ CategoryTheory.Limits.IsColimit t₂
-- Init.Data.Float.Float
/-- Computes the hyperbolic arc cosine (inverse cosine) of a floating-point number.

This function does not reduce in the kernel. It is implemented in compiled code by the C function
`acosh`.
 -/
Float.acosh : Float → Float
-- Mathlib.Topology.Connected.Clopen
/-- The preimage of the image of a set under the quotient map to `connectedComponents α`
is the union of the connected components of the elements in it.  -/
connectedComponents_preimage_image : ∀ {α : Type u} [inst : TopologicalSpace α] (U : Set α),
  ConnectedComponents.mk ⁻¹' ConnectedComponents.mk '' U = ⋃ x ∈ U, connectedComponent x
-- Mathlib.Order.Interval.Set.Basic
Set.decidableMemIci : {α : Type u_1} → [inst : Preorder α] → {b x : α} → [Decidable (b ≤ x)] → Decidable (x ∈ Set.Ici b)
-- Mathlib.CategoryTheory.Monoidal.Mon
/-- Implementation of `AddMon.equivLaxMonoidalFunctorPUnit`.  -/
CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.addMonToLaxMonoidal : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      CategoryTheory.Functor (CategoryTheory.AddMon C)
        (CategoryTheory.LaxMonoidalFunctor (CategoryTheory.Discrete PUnit.{w + 1}) C)
-- Mathlib.Data.List.Sublists
List.length_sublists : ∀ {α : Type u} (l : List α), l.sublists.length = 2 ^ l.length
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
SubMulAction.ofStabilizer.eq_1 : ∀ (G : Type u_1) [inst : Group G] {α : Type u_2} [inst_1 : MulAction G α] (a : α),
  SubMulAction.ofStabilizer G a = { carrier := {a}ᶜ, smul_mem' := ⋯ }
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roi.pairwise_toList_upwardEnumerableLt : ∀ {α : Type u} {r : Std.Roi α} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.PRange.LawfulUpwardEnumerable α]
  [inst_2 : Std.Rxi.IsAlwaysFinite α], List.Pairwise (fun a b => Std.PRange.UpwardEnumerable.LT a b) r.toList
-- Init.Data.String.Substring
Substring.Raw.takeRightWhileAux : String → String.Pos.Raw → (Char → Bool) → String.Pos.Raw → String.Pos.Raw
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.ToCodeBlock.M : Type → Type
-- Init.Grind.Config
/-- If `splitImp` is `true`, then given an implication `p → q` or `(h : p) → q h`, `grind` splits on `p`
if the implication is true. Otherwise, it will split only if `p` is an arithmetic predicate.
 -/
Lean.Grind.Config.splitImp : Lean.Grind.Config → Bool
-- Mathlib.Analysis.Normed.Group.Constructions
Pi.norm_single : ∀ {ι : Type u_1} {G : ι → Type u_4} [inst : Fintype ι] [inst_1 : DecidableEq ι]
  [inst_2 : (i : ι) → NormedAddCommGroup (G i)] {i : ι} (y : G i), ‖Pi.single i y‖ = ‖y‖
-- Lean.Data.PrefixTree
/-- Returns the value of the longest key in `t` that is a prefix of `k`, if any.  -/
Lean.PrefixTree.findLongestPrefix? : {α : Type u_1} → {β : Type u_2} → {p : α → α → Ordering} → Lean.PrefixTree α β p → List α → Option β
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey?_eq_none_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {a : α}, t.contains a = false → t.getKey? a = none
-- Mathlib.CategoryTheory.Monoidal.Functor
/-- The inverse of a monoidal category equivalence is also a monoidal category equivalence.  -/
CategoryTheory.Equivalence.isMonoidal_symm : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D] (e : C ≌ D)
  [inst_4 : e.functor.Monoidal] [inst_5 : e.inverse.Monoidal] [e.IsMonoidal], e.symm.IsMonoidal
-- Mathlib.Logic.Equiv.Prod
/-- The product of an indexed sum of types (formally, a `Sigma`-type `Σ i, α i`) by a type `β` is
equivalent to the sum of products `Σ i, (α i × β)`.  -/
Equiv.sigmaProdDistrib : {ι : Type u_9} → (α : ι → Type u_10) → (β : Type u_11) → ((i : ι) × α i) × β ≃ (i : ι) × α i × β
-- Mathlib.LinearAlgebra.CliffordAlgebra.Basic
CliffordAlgebra.Rel.of : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} (m : M),
  CliffordAlgebra.Rel Q ((TensorAlgebra.ι R) m * (TensorAlgebra.ι R) m) ((algebraMap R (TensorAlgebra R M)) (Q m))
-- Mathlib.Data.Fin.Tuple.Reflection
FinVec.sum.eq_1 : ∀ {α : Type u_1} [inst : Add α] [inst_1 : Zero α] (x_2 : Fin 0 → α), FinVec.sum x_2 = 0
-- Std.Data.String.ToInt
String.isInt_of_isNat : ∀ {s : String}, s.isNat = true → s.isInt = true
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Differentiable.ccos : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : E → ℂ},
  Differentiable ℂ f → Differentiable ℂ fun x => Complex.cos (f x)
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.leadingCoeff_of_ne_zero : ∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : Zero R] {x : HahnSeries Γ R} (hx : x ≠ 0),
  x.leadingCoeff = x.coeff (x.orderTop.untop ⋯)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.size_insertMany_empty_list_le : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} [Std.TransOrd α] {l : List (α × β)},
  (↑(Std.DTreeMap.Internal.Impl.Const.insertMany Std.DTreeMap.Internal.Impl.empty l ⋯)).size ≤ l.length
-- Init.Data.UInt.Bitwise
USize.or_neg_one : ∀ {a : USize}, a ||| -1 = -1
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem_ofList_of_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] {l : List (α × β)} {k k' : α},
  cmp k k' = Ordering.eq →
    ∀ {v : β},
      List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l →
        (k, v) ∈ l → ∀ {h : k' ∈ Std.TreeMap.ofList l cmp}, (Std.TreeMap.ofList l cmp)[k'] = v
-- Mathlib.RingTheory.OreLocalization.Ring
OreLocalization.instCommSemiring : {R : Type u_1} →
  [inst : CommSemiring R] → {S : Submonoid R} → [inst_1 : OreLocalization.OreSet S] → CommSemiring (OreLocalization S R)
-- Mathlib.RingTheory.Bialgebra.Basic
Bialgebra.counit_natCast : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Bialgebra R A] (n : ℕ),
  CoalgebraStruct.counit ↑n = ↑n
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
/-- This should be autogenerated by `@[simps]` but we need to give `1` the correct type here.  -/
ModuleCat.RestrictionCoextensionAdj.HomEquiv.toRestriction_hom_apply : ∀ {R : Type u₁} {S : Type u₂} [inst : Ring R] [inst_1 : Ring S] (f : R →+* S) {X : ModuleCat R} {Y : ModuleCat S}
  (g : Y ⟶ (ModuleCat.coextendScalars f).obj X) (y : ↑((ModuleCat.restrictScalars f).obj Y)),
  (ModuleCat.Hom.hom (ModuleCat.RestrictionCoextensionAdj.HomEquiv.toRestriction f g)) y =
    ((ModuleCat.CoextendScalars.equiv f X) ((ModuleCat.Hom.hom g) y)) 1
-- Mathlib.Topology.Connected.TotallyDisconnected
/-- A space is totally separated if any two points can be separated by two disjoint open sets
covering the whole space.  -/
TotallySeparatedSpace : (α : Type u) → [TopologicalSpace α] → Prop
-- Std.Http.Data.URI.Basic
Std.Http.URI.Host.name.injEq : ∀ (name name_1 : Std.Http.URI.DomainName),
  (Std.Http.URI.Host.name name = Std.Http.URI.Host.name name_1) = (name = name_1)
-- Mathlib.Topology.Algebra.InfiniteSum.ENNReal
ENNReal.tsum_biUnion' : ∀ {α : Type u_1} {ι : Type u_4} {S : Set ι} {f : α → ENNReal} {t : ι → Set α},
  S.PairwiseDisjoint t → ∑' (x : ↑(⋃ i ∈ S, t i)), f ↑x = ∑' (i : ↑S) (x : ↑(t ↑i)), f ↑x
-- Lean.Meta.Tactic.Simp.Arith.Int.Basic
Lean.Meta.Simp.Arith.Int.ToLinear.addAsVar : Lean.Expr → Lean.Meta.Simp.Arith.Int.ToLinear.M Int.Internal.Linear.Expr
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.uniformizer_pos : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R] [inst_2 : ValuativeRel.IsDiscrete R]
  [ValuativeRel.IsNontrivial R], 0 < ValuativeRel.uniformizer R
-- Mathlib.Order.Grade
grade_lt_grade_iff : ∀ {𝕆 : Type u_1} {α : Type u_3} [inst : Preorder 𝕆] [inst_1 : LinearOrder α] [inst_2 : GradeOrder 𝕆 α] {a b : α},
  grade 𝕆 a < grade 𝕆 b ↔ a < b
-- Mathlib.NumberTheory.LSeries.Dirichlet
DirichletCharacter.LSeries_modOne_eq : (LSeries fun n => 1 ↑n) = LSeries 1
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.eraseKey.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (k : α), Std.Internal.List.eraseKey k [] = []
-- Mathlib.Algebra.Module.GradedModule
DirectSum.GdistribMulAction.smul_add : ∀ {ιA : Type u_1} {ιB : Type u_2} {A : ιA → Type u_3} {M : ιB → Type u_4} {inst : AddMonoid ιA} {inst_1 : VAdd ιA ιB}
  {inst_2 : GradedMonoid.GMonoid A} {inst_3 : (i : ιB) → AddMonoid (M i)} [self : DirectSum.GdistribMulAction A M]
  {i : ιA} {j : ιB} (a : A i) (b c : M j),
  GradedMonoid.GSMul.smul a (b + c) = GradedMonoid.GSMul.smul a b + GradedMonoid.GSMul.smul a c
-- Mathlib.Order.WithBot
WithBot.denselyOrdered : ∀ {α : Type u_1} [inst : LT α] [DenselyOrdered α] [NoMinOrder α], DenselyOrdered (WithBot α)
-- Init.Data.UInt.Lemmas
UInt8.toBitVec_div : ∀ {a b : UInt8}, (a / b).toBitVec = a.toBitVec / b.toBitVec
-- Mathlib.Topology.Spectral.Prespectral
/-- A space is prespectral if the lattice of compact opens forms a basis.  -/
PrespectralSpace : (X : Type u_3) → [TopologicalSpace X] → Prop
-- Mathlib.AlgebraicTopology.SimplicialObject.Split
CategoryTheory.SimplicialObject.Splitting.cofan_inj_eq_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : CategoryTheory.SimplicialObject C} (s : X.Splitting)
  {Δ : SimplexCategoryᵒᵖ} (A : CategoryTheory.SimplicialObject.Splitting.IndexSet Δ) {Z : C} (h : (s.cofan Δ).pt ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((s.cofan Δ).inj A) h =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp (s.ι (Opposite.unop A.fst).len) (X.map A.e.op)) h
-- Mathlib.Algebra.Lie.OfAssociative
LieModule.toEnd_pow_apply_map : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M] {M₂ : Type w₁}
  [inst_7 : AddCommGroup M₂] [inst_8 : Module R M₂] [inst_9 : LieRingModule L M₂] [inst_10 : LieModule R L M₂]
  (f : M →ₗ⁅R,L⁆ M₂) (k : ℕ) (x : L) (m : M),
  ((LieModule.toEnd R L M₂) x ^ k) (f m) = f (((LieModule.toEnd R L M) x ^ k) m)
-- Mathlib.GroupTheory.PGroup
IsPGroup.ker_isPGroup_of_injective : ∀ {p : ℕ} {G : Type u_1} [inst : Group G] {K : Type u_2} [inst_1 : Group K] {ϕ : K →* G},
  Function.Injective ⇑ϕ → IsPGroup p ↥ϕ.ker
-- Lean.DocString.Markdown
Lean.Doc.MarkdownM.InlineCtx.mk : Bool → Bool → Bool → Lean.Doc.MarkdownM.InlineCtx
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.EMatch.State.mk.inj : ∀ {thmMap : Lean.Meta.Grind.EMatchTheoremsArray} {gmt : ℕ} {thms newThms : Lean.PArray Lean.Meta.Grind.EMatchTheorem}
  {numInstances numDelayedInstances num : ℕ} {preInstances : Lean.Meta.Grind.PreInstanceSet} {nextThmIdx : ℕ}
  {matchEqNames : Lean.PHashSet Lean.Name}
  {delayedThmInsts : Lean.PHashMap Lean.Meta.Sym.ExprPtr (List Lean.Meta.Grind.DelayedTheoremInstance)}
  {thmMap_1 : Lean.Meta.Grind.EMatchTheoremsArray} {gmt_1 : ℕ}
  {thms_1 newThms_1 : Lean.PArray Lean.Meta.Grind.EMatchTheorem} {numInstances_1 numDelayedInstances_1 num_1 : ℕ}
  {preInstances_1 : Lean.Meta.Grind.PreInstanceSet} {nextThmIdx_1 : ℕ} {matchEqNames_1 : Lean.PHashSet Lean.Name}
  {delayedThmInsts_1 : Lean.PHashMap Lean.Meta.Sym.ExprPtr (List Lean.Meta.Grind.DelayedTheoremInstance)},
  { thmMap := thmMap, gmt := gmt, thms := thms, newThms := newThms, numInstances := numInstances,
        numDelayedInstances := numDelayedInstances, num := num, preInstances := preInstances, nextThmIdx := nextThmIdx,
        matchEqNames := matchEqNames, delayedThmInsts := delayedThmInsts } =
      { thmMap := thmMap_1, gmt := gmt_1, thms := thms_1, newThms := newThms_1, numInstances := numInstances_1,
        numDelayedInstances := numDelayedInstances_1, num := num_1, preInstances := preInstances_1,
        nextThmIdx := nextThmIdx_1, matchEqNames := matchEqNames_1, delayedThmInsts := delayedThmInsts_1 } →
    thmMap = thmMap_1 ∧
      gmt = gmt_1 ∧
        thms = thms_1 ∧
          newThms = newThms_1 ∧
            numInstances = numInstances_1 ∧
              numDelayedInstances = numDelayedInstances_1 ∧
                num = num_1 ∧
                  preInstances = preInstances_1 ∧
                    nextThmIdx = nextThmIdx_1 ∧ matchEqNames = matchEqNames_1 ∧ delayedThmInsts = delayedThmInsts_1
-- Mathlib.RingTheory.Polynomial.SeparableDegree
/-- A choice of a separable contraction.  -/
Polynomial.HasSeparableContraction.contraction : {F : Type u_1} →
  [inst : CommSemiring F] → {q : ℕ} → {f : Polynomial F} → Polynomial.HasSeparableContraction q f → Polynomial F
-- Mathlib.Order.BooleanAlgebra.Set
Set.insert_sdiff_self_of_notMem : ∀ {α : Type u_1} {s : Set α} {a : α}, a ∉ s → insert a s \ {a} = s
-- Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber
/-- An upper estimate on the remainder. This estimate works with `m ∈ ℝ` satisfying `2 ≤ m` and is
weaker than the estimate `LiouvilleNumber.remainder_lt'` above. However, this estimate is
more useful for the proof.  -/
LiouvilleNumber.remainder_lt : ∀ (n : ℕ) {m : ℝ}, 2 ≤ m → LiouvilleNumber.remainder m n < 1 / (m ^ n.factorial) ^ n
-- Init.Data.Vector.Algebra
Vector.add_smul : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} [inst : Add α] [inst_1 : Add β] [inst_2 : SMul α β],
  (∀ (c d : α) (x : β), (c + d) • x = c • x + d • x) → ∀ (c d : α) (xs : Vector β n), (c + d) • xs = c • xs + d • xs
-- Mathlib.Order.CompleteLattice.Basic
sInf_insert : ∀ {α : Type u_1} [inst : CompleteLattice α] {a : α} {s : Set α}, sInf (insert a s) = a ⊓ sInf s
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.smul_eq_C_mul : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] (f : MvPowerSeries σ R) (a : R), a • f = MvPowerSeries.C a * f
-- Aesop.Search.Expansion.Norm
Aesop.checkSimp : String → Bool → Lean.MVarId → Aesop.NormM (Option Aesop.NormRuleResult) → Aesop.NormM (Option Aesop.NormRuleResult)