mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Order.LeftRightNhds
nhds_basis_zero_abs_lt : ∀ (α : Type u_1) [inst : TopologicalSpace α] [inst_1 : AddCommGroup α] [inst_2 : LinearOrder α] [IsOrderedAddMonoid α]
  [OrderTopology α] [NoMaxOrder α], (nhds 0).HasBasis (fun ε => 0 < ε) fun ε => {b | |b| < ε}
-- Mathlib.Topology.Order.Compact
CompactIccSpace.mk : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : Preorder α],
  (∀ {a b : α}, IsCompact (Set.Icc a b)) → CompactIccSpace α
-- Lean.Data.Json.Stream
/-- Consumes `nBytes` bytes from the stream, interprets the bytes as a utf-8 string and the string as a valid JSON object.  -/
Lean.IO.FS.Stream.readJson : IO.FS.Stream → ℕ → IO Lean.Json
-- Mathlib.RingTheory.WittVector.Frobenius
_private.Mathlib.RingTheory.WittVector.Frobenius.0.WittVector.term𝕎 : Lean.ParserDescr
-- Mathlib.Geometry.Euclidean.Inversion.ImageHyperplane
EuclideanGeometry.preimage_inversion_perpBisector_inversion : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {c y : P} {R : ℝ},
  R ≠ 0 →
    y ≠ c →
      EuclideanGeometry.inversion c R ⁻¹' ↑(AffineSubspace.perpBisector c (EuclideanGeometry.inversion c R y)) =
        Metric.sphere y (dist y c) \ {c}
-- Mathlib.Tactic.Ring.Basic
/-- Applies `Nat.cast` to a nat polynomial to produce a polynomial in `α`.

* `↑0 = 0`
* `↑(a + b) = ↑a + ↑b`
 -/
Mathlib.Tactic.Ring.ExSum.evalNatCast : {u : Lean.Level} →
  {α : Q(Type u)} →
    (sα : Q(CommSemiring «$α»)) →
      {v : Lean.Level} →
        {β : Q(Type v)} →
          (sβ : Q(CommSemiring «$β»)) →
            {a : Q(ℕ)} →
              Mathlib.Tactic.Ring.ExSum sβ a →
                Mathlib.Tactic.AtomM (Mathlib.Tactic.Ring.Common.Result (Mathlib.Tactic.Ring.ExSum sα) q(↑«$a»))
-- Mathlib.Logic.Equiv.Defs
Equiv.symm_symm_apply : ∀ {α : Sort u} {β : Sort v} (f : α ≃ β) (b : α), f.symm.symm b = f b
-- Mathlib.CategoryTheory.FinCategory.AsType
/-- A FinCategory `α` is equivalent to a FinCategory in `Type`.  -/
CategoryTheory.FinCategory.AsType : (α : Type u_1) → [Fintype α] → Type
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.veblenWith_one : ∀ {f : Ordinal.{u} → Ordinal.{u}}, Order.IsNormal f → Ordinal.veblenWith f 1 = Ordinal.deriv f
-- Mathlib.NumberTheory.Height.Projectivization
/-- The logarithmic height of a point on a finite-dimensional projective space over `K`
with a given basis.  -/
Projectivization.logHeight : {K : Type u_1} →
  [inst : Field K] → [Height.AdmissibleAbsValues K] → {ι : Type u_2} → [Finite ι] → Projectivization K (ι → K) → ℝ
-- Mathlib.Order.Hom.WithTopBot
/-- Adjoins a `⊥` to the domain of an `InfHom`.  -/
InfHom.withBot' : {α : Type u_1} →
  {β : Type u_2} →
    [inst : SemilatticeInf α] → [inst_1 : SemilatticeInf β] → [OrderBot β] → InfHom α β → InfHom (WithBot α) β
-- Init.Data.Iterators.Basic
/-- Asserts that certain step is plausibly the successor of a given iterator. What "plausible" means
is up to the `Iterator` instance but it should be strong enough to allow termination proofs.
 -/
Std.Iter.IsPlausibleStep : {α β : Type w} → [Std.Iterator α Id β] → Std.Iter β → Std.IterStep (Std.Iter β) β → Prop
-- Mathlib.CategoryTheory.Extensive
CategoryTheory.FinitaryPreExtensive.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [hasFiniteCoproducts : CategoryTheory.Limits.HasFiniteCoproducts C]
  [hasPullbacksOfInclusions : CategoryTheory.HasPullbacksOfInclusions C],
  (∀ {X Y : C} (c : CategoryTheory.Limits.BinaryCofan X Y) (a : CategoryTheory.Limits.IsColimit c),
      CategoryTheory.IsUniversalColimit c) →
    CategoryTheory.FinitaryPreExtensive C
-- Mathlib.CategoryTheory.Enriched.Ordinary.Basic
/-- A full subcategory of an enriched ordinary category is an enriched ordinary category.  -/
CategoryTheory.instEnrichedOrdinaryCategoryFullSubcategory : (V : Type u') →
  [inst : CategoryTheory.Category.{v', u'} V] →
    [inst_1 : CategoryTheory.MonoidalCategory V] →
      {C : Type u} →
        [inst_2 : CategoryTheory.Category.{v, u} C] →
          [CategoryTheory.EnrichedOrdinaryCategory V C] →
            (P : CategoryTheory.ObjectProperty C) → CategoryTheory.EnrichedOrdinaryCategory V P.FullSubcategory
-- Lean.Data.Json.Basic
Lean.Json.instOfNat : {n : ℕ} → OfNat Lean.Json n
-- Mathlib.Algebra.Order.CompleteField
/-- **Alias** of `ConditionallyCompleteLinearOrderedField.inducedOrderRingIso_symm`. -/
LinearOrderedField.inducedOrderRingIso_symm : ∀ (β : Type u_3) (γ : Type u_4) [inst : Field β] [inst_1 : ConditionallyCompleteLinearOrder β]
  [inst_2 : IsStrictOrderedRing β] [inst_3 : Field γ] [inst_4 : ConditionallyCompleteLinearOrder γ]
  [inst_5 : IsStrictOrderedRing γ],
  (ConditionallyCompleteLinearOrderedField.inducedOrderRingIso β γ).symm =
    ConditionallyCompleteLinearOrderedField.inducedOrderRingIso γ β
-- Mathlib.AlgebraicGeometry.StructureSheaf
_private.Mathlib.AlgebraicGeometry.StructureSheaf.0.AlgebraicGeometry.«termΓ(_,_)» : Lean.ParserDescr
-- Mathlib.CategoryTheory.Category.TwoP
/-- The two points of a bipointed type, bundled together as a pair of distinct elements.  -/
TwoP.toTwoPointing : (self : TwoP) → TwoPointing self.X
-- Lean.Parser.Term
/-- A specific universe in Lean's infinite hierarchy of universes.  -/
Lean.Parser.Term.sort : Lean.Parser.Parser
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.pullbackSymmetry_inv_comp_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst_1 : CategoryTheory.Limits.HasPullback f g],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackSymmetry f g).inv
      (CategoryTheory.Limits.pullback.fst f g) =
    CategoryTheory.Limits.pullback.snd g f
-- Mathlib.CategoryTheory.Enriched.Basic
/-- Typecheck an object of `ForgetEnrichment W C` as an object of `C`.  -/
CategoryTheory.ForgetEnrichment.to : {C : Type u₁} →
  (W : Type v) →
    [inst : CategoryTheory.Category.{w, v} W] →
      [inst_1 : CategoryTheory.MonoidalCategory W] →
        [inst_2 : CategoryTheory.EnrichedCategory W C] → CategoryTheory.ForgetEnrichment W C → C
-- Init.Data.SInt.Lemmas
instAssociativeInt64HMul : Std.Associative fun x1 x2 => x1 * x2
-- Mathlib.Topology.MetricSpace.HausdorffDimension
dimH_finite : ∀ {X : Type u_2} [inst : EMetricSpace X] {s : Set X}, s.Finite → dimH s = 0
-- Std.Data.ExtTreeMap.Lemmas
_private.Std.Data.ExtTreeMap.Lemmas.0.GetElem?.match_1.eq_1 : ∀ (elem : outParam (Type u_1)) (motive : Option elem → Sort u_2) (e : elem) (h_1 : (e : elem) → motive (some e))
  (h_2 : Unit → motive none),
  (match some e with
    | some e => h_1 e
    | none => h_2 ()) =
    h_1 e
-- Mathlib.Algebra.Group.Submonoid.Pointwise
AddSubmonoid.negOrderIso.eq_1 : ∀ {G : Type u_2} [inst : AddGroup G],
  AddSubmonoid.negOrderIso = { toEquiv := Equiv.neg (AddSubmonoid G), map_rel_iff' := ⋯ }
-- Mathlib.LinearAlgebra.Vandermonde
Matrix.vandermonde_apply : ∀ {R : Type u_1} [inst : CommRing R] {n : ℕ} (v : Fin n → R) (i j : Fin n), Matrix.vandermonde v i j = v i ^ ↑j
-- Mathlib.Data.Multiset.Powerset
Multiset.powersetCard_cons : ∀ {α : Type u_1} (n : ℕ) (a : α) (s : Multiset α),
  Multiset.powersetCard (n + 1) (a ::ₘ s) =
    Multiset.powersetCard (n + 1) s + Multiset.map (Multiset.cons a) (Multiset.powersetCard n s)
-- Mathlib.RingTheory.Coprime.Basic
IsRelPrime.add_mul_right_right : ∀ {R : Type u_1} [inst : CommRing R] {x y : R}, IsRelPrime x y → ∀ (z : R), IsRelPrime x (y + z * x)
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.evalAddMonoidHom_apply : ∀ {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] (m : M) (x : QuadraticMap R M N),
  (QuadraticMap.evalAddMonoidHom m) x = x m
-- Mathlib.Data.Num.Bitwise
/-- Sign of a `SNum`.  -/
SNum.sign : SNum → Bool
-- Init.Data.SInt.Lemmas
Int32.add_right_inj : ∀ {a b : Int32} (c : Int32), c + a = c + b ↔ a = b
-- Init.Prelude
_private.Init.Prelude.0.Lean.simpMacroScopesAux : Lean.Name → Lean.Name
-- Mathlib.CategoryTheory.ObjectProperty.Equivalence
/-- The equivalence between the full subcategory `⊤` of a category `C` and `C` itself.  -/
CategoryTheory.ObjectProperty.topEquivalence : (C : Type u) → [inst : CategoryTheory.Category.{v, u} C] → ⊤.FullSubcategory ≌ C
-- Mathlib.Data.Finset.Insert
Finset.Nontrivial.nonempty : ∀ {α : Type u_1} {s : Finset α}, s.Nontrivial → s.Nonempty
-- Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
SSet.N.orderIsoOfIso_symm_apply : ∀ {X Y : SSet} (e : X ≅ Y) (y : Y.N),
  (RelIso.symm (SSet.N.orderIsoOfIso e)) y =
    SSet.N.mk ((CategoryTheory.ConcreteCategory.hom (e.inv.app (Opposite.op { len := y.dim }))) y.simplex) ⋯
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring
Subsemiring.isHomogeneous_iff_forall_subset : ∀ {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [inst : AddMonoid ι] [inst_1 : Semiring A] [inst_2 : SetLike σ A]
  [inst_3 : AddSubmonoidClass σ A] (𝒜 : ι → σ) [inst_4 : DecidableEq ι] [inst_5 : GradedRing 𝒜] (R : Subsemiring A),
  DirectSum.SetLike.IsHomogeneous 𝒜 R ↔ ∀ (i : ι), ↑R ⊆ ⇑(GradedRing.proj 𝒜 i) ⁻¹' ↑R
-- Mathlib.Data.List.Palindrome
List.Palindrome.below : {α : Type u_1} → {motive : (a : List α) → a.Palindrome → Prop} → {a : List α} → a.Palindrome → Prop
-- Mathlib.Analysis.SpecialFunctions.Log.ERealExp
EReal.exp_neg : ∀ (x : EReal), (-x).exp = x.exp⁻¹
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Matrix.inv_smul' : ∀ {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α] (A : Matrix n n α)
  (k : αˣ), IsUnit A.det → (k • A)⁻¹ = k⁻¹ • A⁻¹
-- Mathlib.GroupTheory.Finiteness
AddMonoid.fg_of_finite : ∀ {M : Type u_1} [inst : AddMonoid M] [Finite M], AddMonoid.FG M
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
mdifferentiableWithinAt_insert : ∀ {𝕜 : 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] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {x : M} {s : Set M}
  {y : M}, MDiffAt[insert y s] f x ↔ MDiffAt[s] f x
-- Mathlib.Data.Set.Sups
Set.sups_comm : ∀ {α : Type u_2} [inst : SemilatticeSup α] (s t : Set α), s ⊻ t = t ⊻ s
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.Functor.instIsEquivalenceOppositeRightOp : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor Cᵒᵖ D} [F.IsEquivalence], F.rightOp.IsEquivalence
-- Mathlib.CategoryTheory.Sites.Grothendieck
/-- Transitivity of sieves in a Grothendieck topology. Use `GrothendieckTopology.transitive`.  -/
CategoryTheory.GrothendieckTopology.transitive' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (self : CategoryTheory.GrothendieckTopology C) ⦃X : C⦄
  ⦃S : CategoryTheory.Sieve X⦄,
  S ∈ self.sieves X →
    ∀ (R : CategoryTheory.Sieve X),
      (∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → CategoryTheory.Sieve.pullback f R ∈ self.sieves Y) → R ∈ self.sieves X
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.get!_insertMany_list_of_not_mem_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] [inst : BEq α] [Std.LawfulBEqCmp cmp]
  [inst_2 : Inhabited α] {l : List α} {k : α}, k ∉ t → l.contains k = false → (t.insertMany l).get! k = default
-- Mathlib.Combinatorics.SimpleGraph.Sum
/-- The disjoint sum is commutative up to isomorphism. `Iso.sumComm` as a graph isomorphism.  -/
SimpleGraph.Iso.sumComm : {V : Type u_3} → {W : Type u_5} → {G : SimpleGraph V} → {H : SimpleGraph W} → G ⊕g H ≃g H ⊕g G
-- Mathlib.Algebra.Module.Congruence.Defs
SMulCon.mk.injEq : ∀ {S : Type u_2} {M : Type u_3} [inst : SMul S M] (toSetoid : Setoid M)
  (smul : ∀ (s : S) {x y : M}, toSetoid x y → toSetoid (s • x) (s • y)) (toSetoid_1 : Setoid M)
  (smul_1 : ∀ (s : S) {x y : M}, toSetoid_1 x y → toSetoid_1 (s • x) (s • y)),
  ({ toSetoid := toSetoid, smul := smul } = { toSetoid := toSetoid_1, smul := smul_1 }) = (toSetoid = toSetoid_1)
-- Mathlib.Algebra.Group.ForwardDiff
fwdDiff_add : ∀ {M : Type u_1} {G : Type u_2} [inst : AddCommMonoid M] [inst_1 : AddCommGroup G] (h : M) (f g : M → G),
  fwdDiff h (f + g) = fwdDiff h f + fwdDiff h g
-- Mathlib.Algebra.Homology.Additive
CategoryTheory.Functor.map_homogical_complex_additive : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {W : Type u_2} [inst_2 : CategoryTheory.Category.{v_1, u_2} W] [inst_3 : CategoryTheory.Preadditive W]
  (F : CategoryTheory.Functor V W) [inst_4 : F.Additive] (c : ComplexShape ι), (F.mapHomologicalComplex c).Additive
-- Mathlib.CategoryTheory.Sites.Sheaf
CategoryTheory.sheafToPresheafCompCoyonedaCompWhiskeringLeftSheafToPresheaf_inv_app_app_hom_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} A] (X : (CategoryTheory.Sheaf J A)ᵒᵖ) (X_1 : CategoryTheory.Sheaf J A)
  (a : (CategoryTheory.coyoneda.obj X).obj X_1),
  (CategoryTheory.ConcreteCategory.hom
        ((CategoryTheory.sheafToPresheafCompCoyonedaCompWhiskeringLeftSheafToPresheaf.inv.app X).app X_1))
      a =
    Equiv.ulift.toIso.hom.hom'
      ((CategoryTheory.CategoryStruct.comp Equiv.ulift.toIso.inv
            (((CategoryTheory.fullyFaithfulSheafToPresheaf J A).compUliftCoyonedaCompWhiskeringLeft.inv.app X).app
              X_1)).hom'
        a)
-- Init.WFComputable
_private.Init.WFComputable.0.Acc.recC.eq_def : ∀ {α : Sort u_1} {r : α → α → Prop} {motive : (a : α) → Acc r a → Sort v}
  (intro : (x : α) → (h : ∀ (y : α), r y x → Acc r y) → ((y : α) → (hr : r y x) → motive y ⋯) → motive x ⋯) {a : α}
  (t : Acc r a), Acc.recC intro t = intro a ⋯ fun x hr => Acc.recC intro ⋯
-- Init.Data.List.Attach
List.attachWith_map_val : ∀ {α : Type u_1} {β : Type u_2} {p : α → Prop} {f : α → β} {l : List α} (H : ∀ a ∈ l, p a),
  List.map (fun i => f ↑i) (l.attachWith p H) = List.map f l
-- Mathlib.Topology.Algebra.Group.Basic
/-- The (topological-space) closure of a subgroup of a topological group is
itself a subgroup.  -/
Subgroup.topologicalClosure : {G : Type w} → [inst : TopologicalSpace G] → [inst_1 : Group G] → [IsTopologicalGroup G] → Subgroup G → Subgroup G
-- Mathlib.Analysis.Fourier.ZMod
_private.Mathlib.Analysis.Fourier.ZMod.0.ZMod.auxDFT.congr_simp : ∀ {N : ℕ} [inst : NeZero N] {E : Type u_1} [inst_1 : AddCommGroup E] [inst_2 : Module ℂ E] (Φ Φ_1 : ZMod N → E),
  Φ = Φ_1 → ∀ (k k_1 : ZMod N), k = k_1 → ZMod.auxDFT✝ Φ k = ZMod.auxDFT✝ Φ_1 k_1
-- Mathlib.Order.Interval.Finset.Basic
Finset.Iio_bot : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : LocallyFiniteOrderBot α] [inst_2 : OrderBot α], Finset.Iio ⊥ = ∅
-- Mathlib.Order.Heyting.Basic
Disjoint.sup_sdiff_cancel_left : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] {a b : α}, Disjoint a b → (a ⊔ b) \ a = b
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.Measure.instIsAddHaarMeasureForallVolumeOfMeasurableAddOfSigmaFinite : ∀ {ι : Type u_1} [inst : Fintype ι] {G : ι → Type u_4} [inst_1 : (i : ι) → AddGroup (G i)]
  [inst_2 : (i : ι) → MeasureTheory.MeasureSpace (G i)] [∀ (i : ι), MeasurableAdd (G i)]
  [inst_4 : (i : ι) → TopologicalSpace (G i)] [∀ (i : ι), MeasureTheory.SigmaFinite MeasureTheory.volume]
  [∀ (i : ι), MeasureTheory.volume.IsAddHaarMeasure], MeasureTheory.volume.IsAddHaarMeasure
-- Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite
Finset.prod_Ico_mul_eq_prod_Ico_add_one : ∀ {α : Type u_1} {M : Type u_2} [inst : CommMonoid M] {a b : α} [inst_1 : LinearOrder α] [inst_2 : LocallyFiniteOrder α]
  [inst_3 : AddMonoidWithOne α] [SuccAddOrder α] [NoMaxOrder α],
  a ≤ b → ∀ (f : α → M), (∏ x ∈ Finset.Ico a b, f x) * f b = ∏ x ∈ Finset.Ico a (b + 1), f x
-- Mathlib.AlgebraicTopology.SimplicialSet.Path
SSet.Truncated.Path.mk₂_arrow : ∀ {n : ℕ} {X : SSet.Truncated (n + 1)} (p q : X.Path 1) (h : p.vertex 1 = q.vertex 0) (a : Fin (Nat.succ 1)),
  (p.mk₂ q h).arrow a = ![p.arrow 0, q.arrow 0] a
-- Init.Grind.Config
Lean.Grind.CutsatConfig.toNoopConfig : Lean.Grind.CutsatConfig → Lean.Grind.NoopConfig
-- Mathlib.Algebra.Order.Nonneg.Basic
Nonneg.inhabited : {α : Type u_1} → [inst : Preorder α] → {a : α} → Inhabited { x // a ≤ x }
-- Mathlib.Analysis.Convex.Cone.Dual
/-- The dual cone of a set `s` with respect to a perfect pairing `p` is the cone consisting of all
points `y` such that for all points `x ∈ s` we have `0 ≤ p x y`.  -/
ProperCone.dual : {R : Type u_1} →
  {M : Type u_2} →
    {N : Type u_3} →
      [inst : CommRing R] →
        [inst_1 : PartialOrder R] →
          [inst_2 : IsOrderedRing R] →
            [inst_3 : TopologicalSpace R] →
              [ClosedIciTopology R] →
                [inst_5 : AddCommGroup M] →
                  [inst_6 : Module R M] →
                    [inst_7 : TopologicalSpace M] →
                      [inst_8 : AddCommGroup N] →
                        [inst_9 : Module R N] →
                          [inst_10 : TopologicalSpace N] →
                            (p : M →ₗ[R] N →ₗ[R] R) → [p.IsContPerfPair] → Set M → ProperCone R N
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKey!_diff_of_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited α] {k : α}, k ∈ m₂ → (m₁ \ m₂).getKey! k = default
-- Mathlib.RepresentationTheory.Continuous.TopRep
TopRep.of_V : ∀ {k : Type u} {G : Type v} (X : Type w) [inst : TopologicalSpace k] [inst_1 : Ring k] [inst_2 : Monoid G]
  [inst_3 : AddCommGroup X] [inst_4 : Module k X] [inst_5 : TopologicalSpace X] [inst_6 : IsTopologicalAddGroup X]
  [inst_7 : ContinuousSMul k X] (ρ : ContRepresentation k G X), ↑(TopRep.of ρ) = X
-- Init.Data.Option.Lemmas
Option.max_guard_some : ∀ {α : Type u_1} [inst : Max α] [Std.IdempotentOp max] {x : α} {p : α → Bool}, Option.guard p x ⊔ some x = some x
-- Mathlib.RepresentationTheory.FDRep
FDRep.endRingEquiv_comp_ρ : ∀ {R : Type u} {G : Type v} [inst : CommRing R] [inst_1 : Monoid G] (V : FDRep R G),
  (↑V.V.obj.endRingEquiv).comp (CategoryTheory.InducedCategory.endEquiv.toMonoidHom.comp V.ρ) = V.ρ
-- Mathlib.Order.BourbakiWitt
ChainCompletePartialOrder.IsExtremePt.setOfPred_isExtremePt_isAdmissible : ∀ {α : Type u_1} [inst : ChainCompletePartialOrder α] {x : α} {f : α → α},
  (∀ (x : α), x ≤ f x) → ChainCompletePartialOrder.IsAdmissible x f {y | ChainCompletePartialOrder.IsExtremePt x f y}
-- Mathlib.Analysis.Normed.Group.AddTorsor
IsometryEquiv.constVSub_apply : ∀ {V : Type u_2} {P : Type u_3} [inst : SeminormedAddCommGroup V] [inst_1 : PseudoMetricSpace P]
  [inst_2 : NormedAddTorsor V P] (x x_1 : P), (IsometryEquiv.constVSub x) x_1 = x -ᵥ x_1
-- Std.Data.HashSet.Lemmas
Std.HashSet.equiv_of_beq : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashSet α} [LawfulBEq α], (m₁ == m₂) = true → m₁.Equiv m₂
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.source_inter_preimage_inv_preimage : ∀ {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) (s : Set α), e.source ∩ ↑e ⁻¹' ↑e.symm ⁻¹' s = e.source ∩ s
-- Mathlib.Data.Multiset.ZeroCons
Multiset.card_eq_two : ∀ {α : Type u_1} {s : Multiset α}, s.card = 2 ↔ ∃ x y, s = {x, y}
-- Mathlib.Data.Multiset.Bind
Multiset.attach_bind_coe : ∀ {α : Type u_1} {β : Type v} (s : Multiset α) (f : α → Multiset β), (s.attach.bind fun i => f ↑i) = s.bind f
-- Mathlib.Order.Hom.BoundedLattice
InfTopHom.subtypeVal.eq_1 : ∀ {β : Type u_3} [inst : SemilatticeInf β] [inst_1 : OrderTop β] {P : β → Prop} (Pbot : P ⊤)
  (Psup : ∀ ⦃x y : β⦄, P x → P y → P (x ⊓ y)),
  InfTopHom.subtypeVal Pbot Psup = { toInfHom := InfHom.subtypeVal Psup, map_top' := ⋯ }
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKey?_alter_self : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {k : α}
  {f : Option (β k) → Option (β k)}, (m.alter k f).getKey? k = if (f (m.get? k)).isSome = true then some k else none
-- Mathlib.LinearAlgebra.TensorProduct.Tower
LinearEquiv.baseChange_tmul : ∀ (R : Type u_1) (A : Type u_2) (M : Type u_4) (N : Type u_5) [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : AddCommMonoid M] [inst_4 : AddCommMonoid N] [inst_5 : Module R M]
  [inst_6 : Module R N] {e : M ≃ₗ[R] N} (a : A) (m : M), (LinearEquiv.baseChange R A M N e) (a ⊗ₜ[R] m) = a ⊗ₜ[R] e m
-- Mathlib.Algebra.Group.Pi.Lemmas
MulHom.coe_mul : ∀ {M : Type u_5} {N : Type u_6} {x : Mul M} {x_1 : CommSemigroup N} (f g : M →ₙ* N), ⇑f * ⇑g = fun x_2 => f x_2 * g x_2
-- Mathlib.Order.Disjoint
/-- In a `ComplementedLattice`, every element admits a complement.  -/
ComplementedLattice.exists_isCompl : ∀ {α : Type u_2} {inst : Lattice α} {inst_1 : BoundedOrder α} [self : ComplementedLattice α] (a : α), ∃ b, IsCompl a b
-- Mathlib.CategoryTheory.Limits.Types.Coproducts
CategoryTheory.Limits.Types.coproductIso_mk_comp_inv_apply : ∀ {J : Type v} (F : J → Type (max v u)) (j : J) (x : F j),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Types.coproductIso F).inv) ⟨j, x⟩ =
    (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Sigma.ι F j)) x
-- Mathlib.Algebra.Group.End
Equiv.Perm.subtypeCongrHom_injective : ∀ {α : Type u_4} (p : α → Prop) [inst : DecidablePred p], Function.Injective ⇑(Equiv.Perm.subtypeCongrHom p)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.size_right_le_size_union : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp],
  t₂.size ≤ (t₁ ∪ t₂).size
-- Qq.MetaM
/-- A `Qq`-ified version of `Lean.Meta.inferType`

Instead of writing `let α ← inferType e`, this allows writing `let ⟨u, α, e⟩ ← inferTypeQ e`,
which results in a context of
```
e✝ : Expr
u : Level
α : Q(Type u)
e : Q($α)
```
Here, the new `e` is defeq to the old one, but now has `Qq`-ascribed type information.

This is frequently useful when using the `~q` matching from `QQ/Match.lean`,
as it allows an `Expr` to be turned into something that can be matched upon.
 -/
Qq.inferTypeQ : Lean.Expr →
  Lean.MetaM
    ((u : Lean.Level) ×
      (α :
        have u := u;
        Q(Sort u)) ×
        Q(«$α»))
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.compQuasiMeasurePreserving_mk : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α}
  [inst_1 : TopologicalSpace γ] [inst_2 : MeasurableSpace β] {ν : MeasureTheory.Measure β} {f : α → β} {g : β → γ}
  (hg : MeasureTheory.AEStronglyMeasurable g ν) (hf : MeasureTheory.Measure.QuasiMeasurePreserving f μ ν),
  (MeasureTheory.AEEqFun.mk g hg).compQuasiMeasurePreserving f hf = MeasureTheory.AEEqFun.mk (g ∘ f) ⋯
-- Init.Sym.Lemmas
Lean.Sym.String.eq_eq_true : ∀ (a b : String), decide (a = b) = true → (a = b) = True
-- Init.Data.UInt.Lemmas
UInt16.toUInt32_toUInt8 : ∀ (n : UInt16), n.toUInt8.toUInt32 = n.toUInt32 % 256
-- Mathlib.Topology.VectorBundle.Riemannian
Bundle.ContinuousRiemannianMetric.mk.sizeOf_spec : ∀ {B : Type u_4} [inst : TopologicalSpace B] {F : Type u_5} [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace ℝ F]
  {E : B → Type u_6} [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_4 : (b : B) → TopologicalSpace (E b)]
  [inst_5 : (b : B) → AddCommGroup (E b)] [inst_6 : (b : B) → Module ℝ (E b)] [inst_7 : FiberBundle F E]
  [inst_8 : VectorBundle ℝ F E] [inst_9 : SizeOf B] [inst_10 : SizeOf F] [inst_11 : (a : B) → SizeOf (E a)]
  (inner : (b : B) → E b →L[ℝ] E b →L[ℝ] ℝ) (symm : ∀ (b : B) (v w : E b), ((inner b) v) w = ((inner b) w) v)
  (pos : ∀ (b : B) (v : E b), v ≠ 0 → 0 < ((inner b) v) v)
  (isVonNBounded : ∀ (b : B), Bornology.IsVonNBounded ℝ {v | ((inner b) v) v < 1})
  (continuous : Continuous fun b => ⟨b, inner b⟩),
  sizeOf { inner := inner, symm := symm, pos := pos, isVonNBounded := isVonNBounded, continuous := continuous } =
    1 + sizeOf continuous