mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.Conformal.InnerProduct
conformalFactorAt_inner_eq_mul_inner' : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F]
  [inst_2 : InnerProductSpace ℝ E] [inst_3 : InnerProductSpace ℝ F] {f : E → F} {x : E} (h : ConformalAt f x) (u v : E),
  inner ℝ ((fderiv ℝ f x) u) ((fderiv ℝ f x) v) = conformalFactorAt h * inner ℝ u v
-- Mathlib.GroupTheory.GroupAction.SubMulAction.Closure
SubAddAction.mem_closure_of_mem : ∀ {R : Type u_1} {M : Type u_2} [inst : VAdd R M] {s : Set M} {x : M}, x ∈ s → x ∈ SubAddAction.closure R s
-- Mathlib.Algebra.Module.Torsion.Basic
Submodule.supIndep_torsionBySet_ideal : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {ι : Type u_3}
  {p : ι → Ideal R} {S : Finset ι},
  ((↑S).Pairwise fun i j => p i ⊔ p j = ⊤) → S.SupIndep fun i => Submodule.torsionBySet R M ↑(p i)
-- Mathlib.Algebra.Order.Archimedean.Basic
exists_pow_btwn : ∀ {K : Type u_4} [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] [Archimedean K] {n : ℕ},
  n ≠ 0 → ∀ {x y : K}, x < y → 0 < y → ∃ q, 0 < q ∧ x < q ^ n ∧ q ^ n < y
-- Init.Data.Nat.Bitwise.Lemmas
Nat.le_shiftLeft : ∀ {a b : ℕ}, a ≤ a <<< b
-- Mathlib.LinearAlgebra.Finsupp.LSum
LinearMap.finsupp_sum_apply : ∀ {R : Type u_4} {R₂ : Type u_5} {M : Type u_6} {M₂ : Type u_7} {ι : Type u_8} [inst : Semiring R]
  [inst_1 : Semiring R₂] [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] {σ₁₂ : R →+* R₂} [inst_4 : Module R M]
  [inst_5 : Module R₂ M₂] {γ : Type u_9} [inst_6 : Zero γ] (t : ι →₀ γ) (g : ι → γ → M →ₛₗ[σ₁₂] M₂) (b : M),
  (t.sum g) b = t.sum fun i d => (g i d) b
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
ContinuousMultilinearMap.ext_ring_iff : ∀ {R : Type u} {ι : Type v} {M₂ : Type w₂} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₂] [inst_2 : Module R M₂]
  [inst_3 : TopologicalSpace M₂] [Finite ι] [inst_5 : TopologicalSpace R]
  {f g : ContinuousMultilinearMap R (fun x => R) M₂}, f = g ↔ (f fun x => 1) = g fun x => 1
-- Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
trdeg_lt_aleph0_of_finiteType : ∀ {R : Type u_1} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [IsDomain R]
  [fin : Algebra.FiniteType R S], Algebra.trdeg R S < Cardinal.aleph0
-- Mathlib.Order.UpperLower.Relative
IsRelLowerSet.iUnion₂ : ∀ {α : Type u_1} {ι : Sort u_2} {κ : ι → Sort u_3} {P : α → Prop} [inst : LE α] {f : (i : ι) → κ i → Set α},
  (∀ (i : ι) (j : κ i), IsRelLowerSet (f i j) P) → IsRelLowerSet (⋃ i, ⋃ j, f i j) P
-- Mathlib.Order.Filter.AtTopBot.Finset
/-- The pushforward of `atTop` on `Finset α` along `Finset.card` is `atTop` on `ℕ`, when `α` is
infinite.  -/
Filter.map_card_atTop : ∀ {α : Type u_3} [Infinite α], Filter.map Finset.card Filter.atTop = Filter.atTop
-- Mathlib.Data.Int.Init
Int.ofNat_add_negSucc_of_ge : ∀ {m n : ℕ}, n.succ ≤ m → Int.ofNat m + Int.negSucc n = Int.ofNat (m - n.succ)
-- Lean.Data.Lsp.Workspace
Lean.Lsp.instToJsonWorkspaceFolder.toJson : Lean.Lsp.WorkspaceFolder → Lean.Json
-- Mathlib.CategoryTheory.RepresentedBy
CategoryTheory.Functor.RepresentableBy.ofIso.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {F F' : CategoryTheory.Functor Cᵒᵖ (Type v)} {Y : C}
  (e : F.RepresentableBy Y) (e' : F ≅ F'),
  e.ofIso e' = { homEquiv := fun {X} => e.homEquiv.trans (e'.app (Opposite.op X)).toEquiv, homEquiv_comp := ⋯ }
-- Init.Data.Ord.SInt
ISize.instLawfulEqOrd : Std.LawfulEqOrd ISize
-- Mathlib.Algebra.Homology.ShortComplex.Homology
/-- When a short complex has homology, its homology can be computed using
any right homology data.  -/
CategoryTheory.ShortComplex.RightHomologyData.homologyIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S : CategoryTheory.ShortComplex C} → (h : S.RightHomologyData) → [inst_2 : S.HasHomology] → S.homology ≅ h.H
-- Mathlib.Topology.Maps.Proper.Basic
/-- The restriction of a proper map to a closed subset is proper.  -/
IsProperMap.restrict : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y} {C : Set X},
  IsProperMap f → IsClosed C → IsProperMap fun x => f ↑x
-- Mathlib.CategoryTheory.Sums.Products
CategoryTheory.Sum.functorEquiv_functor_map : ∀ (A : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} A] (A' : Type u_2)
  [inst_1 : CategoryTheory.Category.{v_2, u_2} A'] (B : Type u) [inst_2 : CategoryTheory.Category.{v, u} B]
  {X Y : CategoryTheory.Functor (A ⊕ A') B} (η : X ⟶ Y),
  (CategoryTheory.Sum.functorEquiv A A' B).functor.map η =
    CategoryTheory.Prod.mkHom ((CategoryTheory.Sum.inl_ A A').whiskerLeft η)
      ((CategoryTheory.Sum.inr_ A A').whiskerLeft η)
-- Mathlib.Combinatorics.SimpleGraph.Hasse
SimpleGraph.hasse.eq_1 : ∀ (α : Type u_1) [inst : Preorder α],
  SimpleGraph.hasse α = { Adj := fun a b => a ⋖ b ∨ b ⋖ a, symm := ⋯, loopless := ⋯ }
-- Init.Data.Fin.Lemmas
Fin.cast_addNat_left : ∀ {n n' m : ℕ} (i : Fin n') (h : n' + m = n + m), Fin.cast h (i.addNat m) = (Fin.cast ⋯ i).addNat m
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.map_ιE_assoc : ∀ {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₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃)
  {i₀' i₁' i₂' i₃' : ι} (f₁' : i₀' ⟶ i₁') (f₂' : i₁' ⟶ i₂') (f₃' : i₂' ⟶ i₃')
  (α : CategoryTheory.ComposableArrows.mk₃ f₁ f₂ f₃ ⟶ CategoryTheory.ComposableArrows.mk₃ f₁' f₂' f₃')
  (γ : CategoryTheory.ComposableArrows.mk₂ f₂ f₃ ⟶ CategoryTheory.ComposableArrows.mk₂ f₂' f₃') (n₀ n₁ n₂ : ℤ),
  autoParam (γ = CategoryTheory.ComposableArrows.homMk₂ (α.app 1) (α.app 2) (α.app 3) ⋯ ⋯)
      CategoryTheory.Abelian.SpectralObject.map_ιE._auto_1 →
    ∀ (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.map_ιE._auto_3)
      (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.map_ιE._auto_5) {Z : C}
      (h : X.opcycles f₂' f₃' n₁ ⟶ Z),
      CategoryTheory.CategoryStruct.comp (X.map f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ hn₁ hn₂)
          (CategoryTheory.CategoryStruct.comp (X.ιE f₁' f₂' f₃' n₀ n₁ n₂ hn₁ hn₂) h) =
        CategoryTheory.CategoryStruct.comp (X.ιE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂)
          (CategoryTheory.CategoryStruct.comp (X.opcyclesMap f₂ f₃ f₂' f₃' γ n₁) h)
-- Mathlib.Topology.Specialization
/-- A continuous map between topological spaces induces a monotone map between their specialization
orders.  -/
Specialization.map : {α : Type u_1} →
  {β : Type u_2} →
    [inst : TopologicalSpace α] → [inst_1 : TopologicalSpace β] → C(α, β) → Specialization α →o Specialization β
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Iso.isoCompInverse_inv_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] {F : CategoryTheory.Functor C E}
  {G : CategoryTheory.Functor C D} {H : D ≌ E} (i : G.comp H.functor ≅ F) (X : C),
  i.isoCompInverse.inv.app X =
    CategoryTheory.CategoryStruct.comp (H.inverse.map (i.inv.app X)) (H.unitIso.inv.app (G.obj X))
-- Mathlib.Data.WSeq.Relation
Stream'.WSeq.LiftRel.refl : ∀ {α : Type u} (R : α → α → Prop) [Std.Refl R], Std.Refl (Stream'.WSeq.LiftRel R)
-- Lean.Expr
/-- Given `a b : Int`, returns `a ≤ b`  -/
Lean.mkIntLE : Lean.Expr → Lean.Expr → Lean.Expr
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Finite
Set.finite_vadd_set : ∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] {a : G} {s : Set α},
  (a +ᵥ s).Finite ↔ s.Finite
-- Mathlib.Geometry.Euclidean.Circumcenter
_private.Mathlib.Geometry.Euclidean.Circumcenter.0.Affine.Simplex.instFintypePointsWithCircumcenterIndex.match_5.eq_2 : ∀ (n : ℕ) (motive : Affine.Simplex.PointsWithCircumcenterIndex n → Sort u_1)
  (h_1 : (a : Fin (n + 1)) → motive (Affine.Simplex.PointsWithCircumcenterIndex.pointIndex a))
  (h_2 : Unit → motive Affine.Simplex.PointsWithCircumcenterIndex.circumcenterIndex),
  (match Affine.Simplex.PointsWithCircumcenterIndex.circumcenterIndex with
    | Affine.Simplex.PointsWithCircumcenterIndex.pointIndex a => h_1 a
    | Affine.Simplex.PointsWithCircumcenterIndex.circumcenterIndex => h_2 ()) =
    h_2 ()
-- Mathlib.Data.Fintype.Powerset
Fintype.card_set : ∀ {α : Type u_1} [inst : Fintype α], Fintype.card (Set α) = 2 ^ Fintype.card α
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
eisSummand_of_gammaSet_eq_divIntMap : ∀ (k : ℤ) (z : UpperHalfPlane) {n : ℕ} (v : ↑(EisensteinSeries.gammaSet 1 n 0)),
  EisensteinSeries.eisSummand k (↑v) z = (↑n ^ k)⁻¹ * EisensteinSeries.eisSummand k (EisensteinSeries.divIntMap ↑n ↑v) z
-- Mathlib.RingTheory.Polynomial.Tower
Polynomial.aeval_algebraMap_eq_zero_iff : ∀ {R : Type u_1} {A : Type u_2} (B : Type u_3) [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra A B] [inst_5 : Algebra R B] [IsScalarTower R A B] [IsDomain A]
  [Module.IsTorsionFree A B] [Nontrivial B] (x : A) (p : Polynomial R),
  (Polynomial.aeval ((algebraMap A B) x)) p = 0 ↔ (Polynomial.aeval x) p = 0
-- Mathlib.CategoryTheory.Bicategory.Functor.Oplax
/-- Naturality of the oplax functoriality constraint, on the right.  -/
CategoryTheory.OplaxFunctor.mapComp_naturality_right_app_assoc : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] (self : CategoryTheory.OplaxFunctor B CategoryTheory.Cat)
  {a b c : B} (f : a ⟶ b) {g g' : b ⟶ c} (η : g ⟶ g') (X : ↑(self.obj a)) {Z : ↑(self.obj c)}
  (h : (self.map g').toFunctor.obj ((self.map f).toFunctor.obj X) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((self.map₂ (CategoryTheory.Bicategory.whiskerLeft f η)).toNatTrans.app X)
      (CategoryTheory.CategoryStruct.comp ((self.mapComp f g').toNatTrans.app X) h) =
    CategoryTheory.CategoryStruct.comp ((self.mapComp f g).toNatTrans.app X)
      (CategoryTheory.CategoryStruct.comp ((self.map₂ η).toNatTrans.app ((self.map f).toFunctor.obj X)) h)
-- Mathlib.Tactic.CategoryTheory.BicategoricalComp
CategoryTheory.BicategoricalCoherence.assoc'_iso : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (i : a ⟶ d)
  [inst_1 :
    CategoryTheory.BicategoricalCoherence i
      (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h))],
  CategoryTheory.BicategoricalCoherence.iso =
    CategoryTheory.BicategoricalCoherence.iso ≪≫ (CategoryTheory.Bicategory.associator f g h).symm
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.Measure.inv_inv : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : InvolutiveInv G] [MeasurableInv G] (μ : MeasureTheory.Measure G),
  μ.inv.inv = μ
-- Mathlib.Analysis.SpecialFunctions.ExpDeriv
derivWithin_exp : ∀ {f : ℝ → ℝ} {x : ℝ} {s : Set ℝ},
  DifferentiableWithinAt ℝ f s x →
    UniqueDiffWithinAt ℝ s x → derivWithin (fun x => Real.exp (f x)) s x = Real.exp (f x) * derivWithin f s x
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.Entry.funCC.sizeOf_spec : ∀ (declName : Lean.Name), sizeOf (Lean.Meta.Grind.Entry.funCC declName) = 1 + sizeOf declName
-- Init.Data.Vector.Find
Vector.get_find?_replicate : ∀ {α : Type} {n : ℕ} {a : α} {p : α → Bool} (h : (Vector.find? p (Vector.replicate n a)).isSome = true),
  (Vector.find? p (Vector.replicate n a)).get h = a
-- Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric
ordinaryHypergeometricSeries.eq_1 : ∀ {𝕂 : Type u_1} (𝔸 : Type u_2) [inst : Field 𝕂] [inst_1 : Ring 𝔸] [inst_2 : Algebra 𝕂 𝔸] [inst_3 : TopologicalSpace 𝔸]
  [inst_4 : IsTopologicalRing 𝔸] (a b c : 𝕂),
  ordinaryHypergeometricSeries 𝔸 a b c = FormalMultilinearSeries.ofScalars 𝔸 (ordinaryHypergeometricCoefficient a b c)
-- Mathlib.Algebra.Lie.Classical
LieAlgebra.Orthogonal.pb_inv : ∀ (l : Type u_4) (R : Type u₂) [inst : DecidableEq l] [inst_1 : CommRing R] [inst_2 : Fintype l]
  [inst_3 : Invertible 2], LieAlgebra.Orthogonal.PB l R * Matrix.fromBlocks 1 0 0 ⅟(LieAlgebra.Orthogonal.PD l R) = 1
-- Mathlib.NumberTheory.Height.Basic
Height.totalWeight.eq_1 : ∀ (K : Type u_1) [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K],
  Height.totalWeight K = Height.AdmissibleAbsValues.archAbsVal.card
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
lt_neg_iff_add_neg' : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LT α] [AddLeftStrictMono α] {a b : α}, a < -b ↔ b + a < 0
-- Mathlib.Algebra.Order.Interval.Set.SuccPred
Set.Ioi_sub_one_eq_Ici : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : One α] [inst_2 : Sub α] [PredSubOrder α] [NoMinOrder α] (a : α),
  Set.Ioi (a - 1) = Set.Ici a
-- Mathlib.Algebra.Lie.Extension
LieAlgebra.instLieRingL : {R : Type u_1} →
  {N : Type u_2} →
    {M : Type u_4} →
      [inst : CommRing R] →
        [inst_1 : LieRing N] →
          [inst_2 : LieAlgebra R N] →
            [inst_3 : LieRing M] → [inst_4 : LieAlgebra R M] → (E : LieAlgebra.Extension R M N) → LieRing E.L
-- Init.Data.AC
Lean.Data.AC.eval.eq_1 : ∀ {α : Sort u_1} (β : Sort u) [inst : Lean.Data.AC.EvalInformation α β] (ctx : α) (idx : ℕ),
  Lean.Data.AC.eval β ctx (Lean.Data.AC.Expr.var idx) = Lean.Data.AC.EvalInformation.evalVar ctx idx
-- Mathlib.Data.Countable.Defs
uncountable_iff_not_countable : ∀ (α : Sort u_1), Uncountable α ↔ ¬Countable α
-- Mathlib.Tactic.NormNum.LegendreSymbol
/-- This is the `norm_num` plug-in that evaluates Jacobi symbols on natural numbers.  -/
Tactic.NormNum.evalJacobiSymNat : Mathlib.Meta.NormNum.NormNumExt
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.chainsMap_f_1_comp_chainsIso₁_assoc : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k G}
  {B : Rep.{u, u, u} k H} (f : G →* H) (φ : A ⟶ Rep.res f B) {Z : ModuleCat k} (h : ModuleCat.of k (H →₀ ↑B) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((groupHomology.chainsMap f φ).f 1)
      (CategoryTheory.CategoryStruct.comp (groupHomology.chainsIso₁ B).hom h) =
    CategoryTheory.CategoryStruct.comp (groupHomology.chainsIso₁ A).hom
      (CategoryTheory.CategoryStruct.comp (groupHomology.chainsMap₁ f φ) h)
-- Mathlib.CategoryTheory.DifferentialObject
CategoryTheory.DifferentialObject.ext : ∀ {S : Type u_1} [inst : AddMonoidWithOne S] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.HasShift C S]
  {A B : CategoryTheory.DifferentialObject S C} {f g : A ⟶ B},
  autoParam (f.f = g.f) CategoryTheory.DifferentialObject.ext._auto_1 → f = g
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.SummableFamily.instModule : {Γ : Type u_1} →
  {Γ' : Type u_2} →
    {R : Type u_3} →
      {V : Type u_4} →
        {α : Type u_5} →
          [inst : AddCommMonoid Γ] →
            [inst_1 : PartialOrder Γ] →
              [inst_2 : IsOrderedCancelAddMonoid Γ] →
                [inst_3 : PartialOrder Γ'] →
                  [inst_4 : AddAction Γ Γ'] →
                    [IsOrderedCancelVAdd Γ Γ'] →
                      [inst_6 : Semiring R] →
                        [inst_7 : AddCommMonoid V] →
                          [Module R V] → Module (HahnSeries Γ R) (HahnSeries.SummableFamily Γ' V α)
-- Mathlib.Order.Lattice
Monotone.of_map_inf : ∀ {α : Type u} {β : Type v} [inst : SemilatticeInf α] [inst_1 : SemilatticeInf β] {f : α → β},
  (∀ (x y : α), f (x ⊓ y) = f x ⊓ f y) → Monotone f
-- Mathlib.Combinatorics.Schnirelmann
/-- If the Schnirelmann density is `0`, there is a positive natural for which
`|A ∩ {1, ..., n}| / n < ε`, for any positive `ε`.
Note this cannot be improved to `∃ᶠ n : ℕ in atTop`, as can be seen by `A = {1}ᶜ`.
 -/
exists_of_schnirelmannDensity_eq_zero : ∀ {A : Set ℕ} [inst : DecidablePred fun x => x ∈ A] {ε : ℝ},
  0 < ε → schnirelmannDensity A = 0 → ∃ n, 0 < n ∧ ↑{a ∈ Finset.Ioc 0 n | a ∈ A}.card / ↑n < ε
-- Mathlib.CategoryTheory.MorphismProperty.Limits
/-- `P.IsStableUnderBaseChangeAgainst P'` states that for any morphism `f` satisfying `P` and
any morphism `g` with the same codomain as `f` satisfying `P'`, any pullback of `f` along `g`
also satisfies `P`.  -/
CategoryTheory.MorphismProperty.IsStableUnderBaseChangeAgainst : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.MorphismProperty C → CategoryTheory.MorphismProperty C → Prop
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.innerRegularWRT_isCompact_isClosed_measure_ne_top_of_addGroup : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : TopologicalSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G}
  [inst_3 : AddGroup G] [IsTopologicalAddGroup G] [h : μ.InnerRegularCompactLTTop],
  μ.InnerRegularWRT (fun s => IsCompact s ∧ IsClosed s) fun s => MeasurableSet s ∧ μ s ≠ ⊤
-- Mathlib.Analysis.SpecialFunctions.Arcosh
Real.arcosh_bijOn : Set.BijOn Real.arcosh (Set.Ici 1) (Set.Ici 0)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKey!_erase_self : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited α], m.WF → ∀ {k : α}, (m.erase k).getKey! k = default
-- Std.Async.System
/-- Gets the system uptime in seconds.
 -/
Std.Async.System.getUpTime : IO Std.Time.Second.Offset
-- Mathlib.Analysis.Convex.Deriv
/-- If `f : ℝ → ℝ` is convex on `S` and differentiable within `S` at `y`, then the slope of any
secant line with right endpoint at `y` is bounded above by the derivative of `f` within `S` at `y`.

This is fractionally weaker than `ConvexOn.slope_le_of_hasDerivWithinAt_Iio` but simpler to apply
under a `DifferentiableOn S` hypothesis.  -/
ConvexOn.slope_le_of_hasDerivWithinAt : ∀ {S : Set ℝ} {f : ℝ → ℝ} {x y f' : ℝ},
  ConvexOn ℝ S f → x ∈ S → y ∈ S → x < y → HasDerivWithinAt f f' S y → slope f x y ≤ f'
-- Std.Tactic.BVDecide.LRAT.Internal.Clause
Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.unit : {n : ℕ} →
  Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) → Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n
-- Aesop.Builder.Basic
Aesop.PhaseSpec.safe : Aesop.SafeRuleInfo → Aesop.PhaseSpec
-- Mathlib.RingTheory.DividedPowers.DPMorphism
DividedPowers.dpow_comp_from_gens : ∀ {A : Type u_3} {B : Type u_4} [inst : CommSemiring A] [inst_1 : CommSemiring B] {I : Ideal A} {J : Ideal B}
  (hI : DividedPowers I) (hJ : DividedPowers J) {f : A →+* B} {S : Set A},
  I = Ideal.span S →
    (∀ s ∈ S, f s ∈ J) →
      (∀ {n : ℕ}, ∀ a ∈ S, f (hI.dpow n a) = hJ.dpow n (f a)) → ∀ {n : ℕ}, ∀ a ∈ I, hJ.dpow n (f a) = f (hI.dpow n a)
-- Batteries.Data.Array.Match
_private.Batteries.Data.Array.Match.0.Array.PrefixTable.step.match_1.eq_2 : ∀ {α : Type u_1} (t : Array.PrefixTable α) (motive : (k : ℕ) → k < t.size + 1 → Sort u_2) (k : ℕ)
  (hk : k + 1 < t.size + 1) (h_1 : (hk : 0 < t.size + 1) → motive 0 hk)
  (h_2 : (k : ℕ) → (hk : k + 1 < t.size + 1) → motive k.succ hk),
  (match k.succ, hk with
    | 0, hk => h_1 hk
    | k.succ, hk => h_2 k hk) =
    h_2 k hk
-- Mathlib.Algebra.FreeAlgebra
FreeAlgebra.instMul : (R : Type u_1) → (X : Type u_2) → [inst : CommSemiring R] → Mul (FreeAlgebra R X)
-- Init.System.IO
/-- Command name.  -/
IO.Process.SpawnArgs.cmd : IO.Process.SpawnArgs → String
-- Mathlib.RingTheory.Perfection
PerfectionMap.comp_equiv' : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {R : Type u₁} [inst_1 : CommSemiring R] [inst_2 : CharP R p] {P : Type u₃}
  [inst_3 : CommSemiring P] [inst_4 : CharP P p] [inst_5 : PerfectRing P p] {π : P →+* R} (m : PerfectionMap p π),
  (Perfection.coeff R p 0).comp ↑m.equiv = π
-- Mathlib.Data.Set.Basic
Set.subset_union_of_subset_right : ∀ {α : Type u} {s u : Set α}, s ⊆ u → ∀ (t : Set α), s ⊆ t ∪ u
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
mul_nonpos_iff : ∀ {R : Type u} [inst : Ring R] [inst_1 : LinearOrder R] {a b : R} [MulPosStrictMono R] [PosMulStrictMono R]
  [AddLeftReflectLE R] [AddLeftMono R], a * b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CompletionList.mk : Bool → Array Lean.Lsp.CompletionItem → Lean.Lsp.CompletionList
-- Mathlib.Data.Finset.Pi
Finset.restrict.eq_1 : ∀ {ι : Type u_2} {π : ι → Type u_3} (s : Finset ι) (f : (i : ι) → π i) (x : ↥s), s.restrict f x = f ↑x
-- Mathlib.LinearAlgebra.DirectSum.Finsupp
finsuppTensorFinsuppRid.eq_1 : ∀ (R : Type u_1) (M : Type u_3) (ι : Type u_5) (κ : Type u_6) [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M],
  finsuppTensorFinsuppRid R M ι κ =
    (finsuppTensorFinsupp R R M R ι κ).trans (Finsupp.lcongr (Equiv.refl (ι × κ)) (TensorProduct.rid R M))
-- Std.Data.DHashMap.Internal.Raw
Std.DHashMap.Internal.Raw.Const.ofArray_eq : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {a : Array (α × β)},
  Std.DHashMap.Raw.Const.ofArray a =
    ↑↑(Std.DHashMap.Internal.Raw₀.Const.insertMany Std.DHashMap.Internal.Raw₀.emptyWithCapacity a)
-- Mathlib.FieldTheory.Galois.Infinite
InfiniteGalois.normalAutEquivQuotient_apply : ∀ {k : Type u_1} {K : Type u_2} [inst : Field k] [inst_1 : Field K] [inst_2 : Algebra k K] [inst_3 : IsGalois k K]
  (H : ClosedSubgroup Gal(K/k)) [inst_4 : (↑H).Normal] (σ : Gal(K/k)),
  (InfiniteGalois.normalAutEquivQuotient H) ↑σ = (AlgEquiv.restrictNormalHom ↥(IntermediateField.fixedField ↑H)) σ
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Pred
String.Pos.skipWhile_bool_eq_self_iff_get : ∀ {p : Char → Bool} {s : String} {pos : s.Pos}, pos.skipWhile p = pos ↔ ∀ (h : pos ≠ s.endPos), p (pos.get h) = false
-- Lean.Server.GoTo
Lean.Server.locationLinksFromDecl : Lean.Name → Lean.Server.GoToM (Array Lean.Lsp.LeanLocationLink)
-- Mathlib.Data.Set.Lattice
Set.union_iInter : ∀ {β : Type u_2} {ι : Sort u_5} (s : Set β) (t : ι → Set β), s ∪ ⋂ i, t i = ⋂ i, s ∪ t i
-- Mathlib.GroupTheory.Complement
AddSubgroup.isComplement'_comm : ∀ {G : Type u_1} [inst : AddGroup G] {H K : AddSubgroup G}, H.IsComplement' K ↔ K.IsComplement' H
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.mem_of_mem_insertManyIfNewUnit_list : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α Unit cmp} [Std.TransCmp cmp] [inst : BEq α]
  [Std.LawfulBEqCmp cmp], t.WF → ∀ {l : List α} {k : α}, l.contains k = false → k ∈ t.insertManyIfNewUnit l → k ∈ t
-- Mathlib.Tactic.FieldSimp
Mathlib.Tactic.FieldSimp.DenomCondition.none : {v : Lean.Level} → {M : Q(Type v)} → {iM : Q(GroupWithZero «$M»)} → Mathlib.Tactic.FieldSimp.DenomCondition iM
-- Mathlib.Order.Hom.Bounded
BotHom.instLattice.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : Bot α] [inst_1 : Lattice β] [inst_2 : OrderBot β],
  BotHom.instLattice = Function.Injective.lattice DFunLike.coe ⋯ ⋯ ⋯ ⋯ ⋯
-- Mathlib.CategoryTheory.Sites.Sheafification
CategoryTheory.sheafifyMap_sheafifyLift_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} D] [inst_2 : CategoryTheory.HasWeakSheafify J D]
  {P Q R : CategoryTheory.Functor Cᵒᵖ D} (η : P ⟶ Q) (γ : Q ⟶ R) (hR : CategoryTheory.Presheaf.IsSheaf J R)
  {Z : CategoryTheory.Functor Cᵒᵖ D} (h : R ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.sheafifyMap J η)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.sheafifyLift J γ hR) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.sheafifyLift J (CategoryTheory.CategoryStruct.comp η γ) hR) h
-- Mathlib.LinearAlgebra.Charpoly.ToMatrix
/-- `charpoly f` is the characteristic polynomial of the matrix of `f` in any basis.  -/
LinearMap.charpoly_toMatrix : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : Module.Free R M] [inst_4 : Module.Finite R M] (f : M →ₗ[R] M) {ι : Type w} [inst_5 : DecidableEq ι]
  [inst_6 : Fintype ι] (b : Module.Basis ι R M), ((LinearMap.toMatrix b b) f).charpoly = f.charpoly
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
/-- The 0-cycles of the complex of inhomogeneous chains of `A` are isomorphic to `A`.  -/
groupHomology.cyclesIso₀ : {k G : Type u} →
  [inst : CommRing k] → [inst_1 : Group G] → (A : Rep.{u, u, u} k G) → groupHomology.cycles A 0 ≅ ModuleCat.of k ↑A
-- Init.Data.List.TakeDrop
List.length_drop : ∀ {α : Type u_1} {i : ℕ} {l : List α}, (List.drop i l).length = l.length - i