mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.NumberTheory.NumberField.Discriminant.Basic
NumberField.discr_eq_basisMatrix_det_sq : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] [inst_2 : DecidableEq (K →+* ℂ)],
  ↑(NumberField.discr K) = (NumberField.basisMatrix K).det ^ 2
-- Mathlib.Topology.Algebra.ConstMulAction
IsClosed.smul₀ : ∀ {G₀ : Type u_4} [inst : GroupWithZero G₀] {E : Type u_5} [inst_1 : Zero E] [inst_2 : MulActionWithZero G₀ E]
  [inst_3 : TopologicalSpace E] [T1Space E] [ContinuousConstSMul G₀ E] (c : G₀) {s : Set E},
  IsClosed s → IsClosed (c • s)
-- Mathlib.Analysis.SpecialFunctions.Complex.CircleMap
circleMap_mem_sphere' : ∀ (c : ℂ) (R θ : ℝ), circleMap c R θ ∈ Metric.sphere c |R|
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.minKey!_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α], t ≠ ∅ → t.minKey! ∈ t
-- Mathlib.Order.Interval.Set.Nat
Set.ncard_Iio_nat : ∀ (b : ℕ), (Set.Iio b).ncard = b
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- The angle ∡ABA at a point.  -/
EuclideanGeometry.oangle_self_left_right : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  (p₁ p₂ : P), EuclideanGeometry.oangle p₁ p₂ p₁ = 0
-- Mathlib.Topology.Compactness.Compact
Prod.noncompactSpace_right : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [Nonempty X] [NoncompactSpace Y],
  NoncompactSpace (X × Y)
-- Mathlib.CategoryTheory.Preadditive.EndoFunctor
/-- The category of algebras over an additive endofunctor on a preadditive category is preadditive.
 -/
CategoryTheory.Endofunctor.algebraPreadditive : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      (F : CategoryTheory.Functor C C) →
        [F.Additive] → CategoryTheory.Preadditive (CategoryTheory.Endofunctor.Algebra F)
-- Init.Data.Vector.Lemmas
Vector.sum_mk : ∀ {α : Type u_1} {n : ℕ} [inst : Add α] [inst_1 : Zero α] {xs : Array α} (h : xs.size = n),
  (Vector.mk xs h).sum = xs.sum
-- Init.Data.Float.Model.Format.Basic
/-- The number of bits in the exponent.  -/
Float.Model.Format.exponentBits : Float.Model.Format → ℕ
-- Mathlib.Data.ZMod.Basic
ZMod.ringEquivCongr_refl_apply : ∀ {a : ℕ} (x : ZMod a), (ZMod.ringEquivCongr ⋯) x = x
-- Mathlib.Analysis.Convex.Visible
isVisible_iff_lineMap : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsOrderedRing 𝕜]
  [inst_3 : AddCommGroup V] [inst_4 : Module 𝕜 V] [inst_5 : AddTorsor V P] {s : Set P} {x y : P},
  x ≠ y → (IsVisible 𝕜 s x y ↔ ∀ δ ∈ Set.Ioo 0 1, (AffineMap.lineMap x y) δ ∉ s)
-- Init.Data.String.Basic
String.Pos.ofToSlice_le : ∀ {s : String} {p q : s.toSlice.Pos}, String.Pos.ofToSlice p ≤ String.Pos.ofToSlice q ↔ p ≤ q
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.prod_top : ∀ {N : Type u_2} [inst : MulOneClass N] {M : Type u_5} [inst_1 : MulOneClass M] (s : Submonoid M),
  s.prod ⊤ = Submonoid.comap (MonoidHom.fst M N) s
-- Mathlib.LinearAlgebra.Matrix.HadamardMatrix
Matrix.isHadamard_iff_mul_conjTranspose : ∀ {n : Type u_2} {R : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing R] [inst_3 : StarRing R]
  {A : Matrix n n R},
  IsRegular ↑(Fintype.card n) →
    (A.IsHadamard ↔ (∀ (i j : n), A i j ∈ unitary R) ∧ A * A.conjTranspose = ↑(Fintype.card n) • 1)
-- Mathlib.GroupTheory.PresentedGroup
PresentedGroup.mk_surjective : ∀ {α : Type u_1} (rels : Set (FreeGroup α)), Function.Surjective ⇑(PresentedGroup.mk rels)
-- Mathlib.Topology.Convenient.Localization
/-- Given a family of topological spaces `X`, this is the family of morphisms in `TopCat`
corresponding to the continuous maps `WithGeneratedByTopology X Z → Z` for
all topological spaces `Z`.  -/
TopCat.morphismPropertyWithGeneratedByTopologyEquiv : {ι : Type t} → (X : ι → Type u) → [(i : ι) → TopologicalSpace (X i)] → CategoryTheory.MorphismProperty TopCat
-- Mathlib.Data.Set.Basic
Set.le_iff_subset : ∀ {α : Type u} {s t : Set α}, s ⊆ t ↔ s ⊆ t
-- Std.Http.Test.Helpers
/-- Like `check` but closes the client channel before running the server.
Use for tests involving truncated input or silent-close (EOF-triggered behavior).
 -/
Std.Http.Internal.Test.checkClose : String →
  String →
    Std.Http.Internal.Test.TestHandler →
      (ByteArray → IO Unit) → optParam Std.Http.Config Std.Http.Internal.Test.defaultConfig → IO Unit
-- Init.NotationExtra
unexpandGetElem! : Lean.PrettyPrinter.Unexpander
-- Mathlib.Topology.MetricSpace.Holder
HolderOnWith.edist_le_of_le : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] {C r : NNReal} {f : X → Y}
  {s : Set X},
  HolderOnWith C r f s → ∀ {x y : X}, x ∈ s → y ∈ s → ∀ {d : ENNReal}, edist x y ≤ d → edist (f x) (f y) ≤ ↑C * d ^ ↑r
-- Mathlib.CategoryTheory.Limits.ConeCategory
CategoryTheory.Limits.limit.toStructuredArrow_obj : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor J C) [inst_2 : CategoryTheory.Limits.HasLimit F] (j : J),
  (CategoryTheory.Limits.limit.toStructuredArrow F).obj j =
    CategoryTheory.StructuredArrow.mk (CategoryTheory.Limits.limit.π F j)
-- Mathlib.Topology.Category.TopCat.Opens
TopologicalSpace.Opens.map_homOfLE : ∀ {X Y : TopCat} (f : X ⟶ Y) {U V : TopologicalSpace.Opens ↑Y} (e : U ≤ V),
  (TopologicalSpace.Opens.map f).map (CategoryTheory.homOfLE e) = CategoryTheory.homOfLE ⋯
-- Mathlib.InformationTheory.Hamming
Hamming.instDecidableEqOfFintype : {ι : Type u_2} → {β : ι → Type u_3} → [Fintype ι] → [(i : ι) → DecidableEq (β i)] → DecidableEq (Hamming β)
-- Mathlib.Algebra.QuaternionBasis
QuaternionAlgebra.Basis.mk.injEq : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] {c₁ c₂ c₃ : R} (i j k : A)
  (i_mul_i : i * i = c₁ • 1 + c₂ • i) (j_mul_j : j * j = c₃ • 1) (i_mul_j : i * j = k) (j_mul_i : j * i = c₂ • j - k)
  (i_1 j_1 k_1 : A) (i_mul_i_1 : i_1 * i_1 = c₁ • 1 + c₂ • i_1) (j_mul_j_1 : j_1 * j_1 = c₃ • 1)
  (i_mul_j_1 : i_1 * j_1 = k_1) (j_mul_i_1 : j_1 * i_1 = c₂ • j_1 - k_1),
  ({ i := i, j := j, k := k, i_mul_i := i_mul_i, j_mul_j := j_mul_j, i_mul_j := i_mul_j, j_mul_i := j_mul_i } =
      { i := i_1, j := j_1, k := k_1, i_mul_i := i_mul_i_1, j_mul_j := j_mul_j_1, i_mul_j := i_mul_j_1,
        j_mul_i := j_mul_i_1 }) =
    (i = i_1 ∧ j = j_1 ∧ k = k_1)
-- Lean.CoreM
/-- Performance option used by cmdline driver.  -/
Lean.internal.cmdlineSnapshots : Lean.Option Bool
-- Mathlib.MeasureTheory.Measure.Restrict
MeasurableEmbedding.comap_restrict : ∀ {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} {m1 : MeasurableSpace β} {f : α → β},
  MeasurableEmbedding f →
    ∀ (μ : MeasureTheory.Measure β) (s : Set β),
      MeasureTheory.Measure.comap f (μ.restrict s) = (MeasureTheory.Measure.comap f μ).restrict (f ⁻¹' s)
-- Mathlib.Analysis.MeanInequalities
/-- **Hölder inequality**: the sum of (the `r`-powers of) two functions is bounded by the product
of (the `r`-powers of) their `L^p` and `L^q` norms when `p`, `q` and `r` form a `Real.HolderTriple`.
A version for `ℝ`-valued functions.  -/
Real.summable_and_Lr_rpow_le_Lp_mul_Lq_tsum_of_nonneg : ∀ {ι : Type u} {f g : ι → ℝ} {p q r : ℝ},
  p.HolderTriple q r →
    (∀ (i : ι), 0 ≤ f i) →
      (∀ (i : ι), 0 ≤ g i) →
        (Summable fun i => f i ^ p) →
          (Summable fun i => g i ^ q) →
            (Summable fun i => (f i * g i) ^ r) ∧
              ∑' (i : ι), (f i * g i) ^ r ≤ (∑' (i : ι), f i ^ p) ^ (r / p) * (∑' (i : ι), g i ^ q) ^ (r / q)
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.inv_omega : Hyperreal.omega⁻¹ = Hyperreal.epsilon
-- Mathlib.Algebra.Category.Semigrp.Basic
/-- Use the `ConcreteCategory.hom` projection for `@[simps]` lemmas.  -/
MagmaCat.Hom.Simps.hom : (X Y : MagmaCat) → X.Hom Y → ↑X →ₙ* ↑Y
-- Mathlib.Algebra.GroupWithZero.Action.Defs
/-- Multiplying `0` by a scalar gives `0`  -/
SMulZeroClass.smul_zero : ∀ {M : Type u_12} {A : Type u_13} {inst : Zero A} [self : SMulZeroClass M A] (a : M), a • 0 = 0
-- Mathlib.RingTheory.Polynomial.ContentIdeal
Polynomial.contentIdeal_monomial : ∀ {R : Type u_1} [inst : Semiring R] (n : ℕ) (r : R), ((Polynomial.monomial n) r).contentIdeal = Ideal.span {r}
-- Mathlib.CategoryTheory.Sites.Descent.Precoverage
_private.Mathlib.CategoryTheory.Sites.Descent.Precoverage.0.CategoryTheory.Pseudofunctor.DescentData.full_pullFunctor.comm : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat}
  {J : CategoryTheory.GrothendieckTopology C} [inst_1 : F.IsPrestack J] {ι : Type t} {S : C} {X : ι → C}
  {f : (i : ι) → X i ⟶ S} {ι' : Type t'} {X' : ι' → C} {f' : (j : ι') → X' j ⟶ S} {α : ι' → ι}
  {p' : (j : ι') → X' j ⟶ X (α j)} (w : ∀ (j : ι'), CategoryTheory.CategoryStruct.comp (p' j) (f (α j)) = f' j)
  (hf' : CategoryTheory.Sieve.ofArrows X' f' ∈ J S) {D₁ D₂ : F.DescentData f}
  (φ :
    (CategoryTheory.Pseudofunctor.DescentData.pullFunctor F ⋯).obj D₁ ⟶
      (CategoryTheory.Pseudofunctor.DescentData.pullFunctor F ⋯).obj D₂)
  ⦃W : C⦄ (q : W ⟶ S) ⦃i₁ i₂ : ι⦄ (f₁ : W ⟶ X i₁) (f₂ : W ⟶ X i₂)
  (hf₁ :
    autoParam (CategoryTheory.CategoryStruct.comp f₁ (f i₁) = q)
      CategoryTheory.Pseudofunctor.DescentData.full_pullFunctor.comm._auto_1✝)
  (hf₂ :
    autoParam (CategoryTheory.CategoryStruct.comp f₂ (f i₂) = q)
      CategoryTheory.Pseudofunctor.DescentData.full_pullFunctor.comm._auto_3✝),
  CategoryTheory.CategoryStruct.comp
      ((F.map f₁.op.toLoc).toFunctor.map (CategoryTheory.Pseudofunctor.DescentData.full_pullFunctor.hom✝ w hf' φ i₁))
      (D₂.hom q f₁ f₂ ⋯ ⋯) =
    CategoryTheory.CategoryStruct.comp (D₁.hom q f₁ f₂ ⋯ ⋯)
      ((F.map f₂.op.toLoc).toFunctor.map (CategoryTheory.Pseudofunctor.DescentData.full_pullFunctor.hom✝ w hf' φ i₂))
-- Batteries.Recycling.RBTree.Basic
/-- The number of nodes in the tree.  -/
RBTree.RBNode.size : {α : Type u_1} → RBTree.RBNode α → ℕ
-- Mathlib.Algebra.Star.Subalgebra
NonUnitalStarSubalgebra.toStarSubalgebra_toNonUnitalStarSubalgebra : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : StarRing A] [inst_4 : Algebra R A] [inst_5 : StarModule R A] (S : NonUnitalStarSubalgebra R A) (h1 : 1 ∈ S),
  (S.toStarSubalgebra h1).toNonUnitalStarSubalgebra = S
-- Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects
/-- The colimit cocone for the coproduct with a zero object.  -/
CategoryTheory.Limits.binaryCofanZeroLeft : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroObject C] →
      [CategoryTheory.Limits.HasZeroMorphisms C] → (X : C) → CategoryTheory.Limits.BinaryCofan 0 X
-- Init.Data.UInt.Bitwise
USize.toBitVec_and : ∀ (a b : USize), (a &&& b).toBitVec = a.toBitVec &&& b.toBitVec
-- Mathlib.CategoryTheory.Monoidal.Mon
/-- A morphism of monoid objects.  -/
CategoryTheory.Mon.Hom : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] → CategoryTheory.Mon C → CategoryTheory.Mon C → Type v₁
-- Mathlib.CategoryTheory.Monoidal.Bimon_
/-- The forgetful functor from bimonoid objects to monoid objects.  -/
CategoryTheory.Bimon.toMon : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] →
        CategoryTheory.Functor (CategoryTheory.Bimon C) (CategoryTheory.Mon C)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKeyD_inter_of_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  {k fallback : α}, k ∈ t₂ → (t₁ ∩ t₂).getKeyD k fallback = t₁.getKeyD k fallback
-- Mathlib.Data.Set.Basic
Set.coe_ofPred : ∀ {α : Type u} (p : α → Prop), ↑{x | p x} = { x // p x }
-- Std.Data.HashMap.Lemmas
Std.HashMap.mem_toArray_iff_getKey?_eq_some_and_getElem?_eq_some : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α}
  {v : β}, (k, v) ∈ m.toArray ↔ m.getKey? k = some k ∧ m[k]? = some v
-- Init.Data.List.Basic
List.replicateTR.loop.eq_def : ∀ {α : Type u} (a : α) (a_1 : ℕ) (a_2 : List α),
  List.replicateTR.loop a a_1 a_2 =
    match a_1, a_2 with
    | 0, as => as
    | n.succ, as => List.replicateTR.loop a n (a :: as)
-- Init.Data.UInt.IntToBitVec
USize.toBitVec32_shiftRight : ∀ (a b : USize) (h : System.Platform.numBits = 32), (a >>> b).toBitVec32 h = a.toBitVec32 h >>> (b.toBitVec32 h % 32)
-- Mathlib.AlgebraicTopology.SimplicialSet.Basic
SSet.δ_comp_σ_succ_apply : ∀ {S : SSet} {n : ℕ} (i : Fin (n + 1)) (x : S.obj (Opposite.op { len := n })),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ S i.succ))
      ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.σ S i)) x) =
    x
-- Mathlib.Topology.NhdsWithin
nhdsWithin_iUnion : ∀ {α : Type u_1} [inst : TopologicalSpace α] {ι : Sort u_5} [Finite ι] (s : ι → Set α) (a : α),
  nhdsWithin a (⋃ i, s i) = ⨆ i, nhdsWithin a (s i)
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoDiv_sub_eq_toIcoDiv_add' : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b c : α), toIcoDiv hp (a - c) b = toIcoDiv hp a (b + c)
-- Init.Data.BitVec.Lemmas
BitVec.msb_udiv_eq_false_of : ∀ {w : ℕ} {x y : BitVec w}, x.msb = false → (x / y).msb = false
-- Qq.MetaM
Qq.elabTermEnsuringTypeQ : {u : Lean.Level} →
  Lean.Syntax →
    (expectedType : Q(Sort u)) →
      optParam Bool true → optParam Bool true → optParam (Option String) none → Lean.Elab.TermElabM Q(«$expectedType»)
-- Mathlib.Algebra.Star.StarAlgHom
/-- The inverse of a star algebra isomorphism is a star algebra isomorphism.  -/
StarAlgEquiv.symm : {R : Type u_2} →
  {A : Type u_3} →
    {B : Type u_4} →
      [inst : Add A] →
        [inst_1 : Add B] →
          [inst_2 : Mul A] →
            [inst_3 : Mul B] →
              [inst_4 : SMul R A] →
                [inst_5 : SMul R B] → [inst_6 : Star A] → [inst_7 : Star B] → (A ≃⋆ₐ[R] B) → B ≃⋆ₐ[R] A
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
/-- The integral of the derivative of a scalar multiplication.  -/
intervalIntegral.integral_deriv_smul_eq_sub_of_hasDeriv_right : ∀ {a b : ℝ} {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAlgebra ℝ 𝕜] {E : Type u_2}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedSpace ℝ E] [CompleteSpace E]
  [IsScalarTower ℝ 𝕜 E] {u u' : ℝ → 𝕜} {v v' : ℝ → E},
  ContinuousOn u (Set.uIcc a b) →
    ContinuousOn v (Set.uIcc a b) →
      (∀ x ∈ Set.Ioo (min a b) (max a b), HasDerivWithinAt u (u' x) (Set.Ioi x) x) →
        (∀ x ∈ Set.Ioo (min a b) (max a b), HasDerivWithinAt v (v' x) (Set.Ioi x) x) →
          IntervalIntegrable u' MeasureTheory.volume a b →
            IntervalIntegrable v' MeasureTheory.volume a b →
              ∫ (x : ℝ) in a..b, u' x • v x + u x • v' x = u b • v b - u a • v a
-- Mathlib.CategoryTheory.Monad.Limits
CategoryTheory.Monad.ForgetCreatesColimits.coconePoint_A : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {J : Type u}
  [inst_1 : CategoryTheory.Category.{v, u} J] {D : CategoryTheory.Functor J T.Algebra}
  (c : CategoryTheory.Limits.Cocone (D.comp T.forget)) (t : CategoryTheory.Limits.IsColimit c)
  [inst_2 : CategoryTheory.Limits.PreservesColimit (D.comp T.forget) T.toFunctor]
  [inst_3 : CategoryTheory.Limits.PreservesColimit ((D.comp T.forget).comp T.toFunctor) T.toFunctor],
  (CategoryTheory.Monad.ForgetCreatesColimits.coconePoint c t).A = c.pt
-- Mathlib.Probability.Independence.Conditional
ProbabilityTheory.iCondIndepFun.indepFun_div_right : ∀ {Ω : Type u_1} {ι : Type u_2} {β : Type u_3} {m' mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω] {hm' : m' ≤ mΩ}
  {μ : MeasureTheory.Measure Ω} [inst_1 : MeasureTheory.IsFiniteMeasure μ] {m : MeasurableSpace β} [inst_2 : Div β]
  [MeasurableDiv₂ β] {f : ι → Ω → β},
  ProbabilityTheory.iCondIndepFun m' hm' f μ →
    (∀ (i : ι), Measurable (f i)) →
      ∀ (i j k : ι), i ≠ j → i ≠ k → ProbabilityTheory.CondIndepFun m' hm' (f i) (f j / f k) μ
-- Std.Data.DHashMap.Basic
/-- Partition a hash map into two hash map based on a predicate.  -/
Std.DHashMap.partition : {α : Type u} →
  {β : α → Type v} →
    {x : BEq α} → {x_1 : Hashable α} → ((a : α) → β a → Bool) → Std.DHashMap α β → Std.DHashMap α β × Std.DHashMap α β
-- Init.Data.UInt.Lemmas
UInt16.toUInt32_ofNat : ∀ {n : ℕ}, n < 65536 → (OfNat.ofNat n).toUInt32 = OfNat.ofNat n
-- Mathlib.Geometry.Manifold.Immersion
/-- `f : M → N` is a `C^n` immersion at `x` if there are charts `φ` and `ψ` of `M` and `N`
around `x` and `f x`, respectively such that in these charts, `f` looks like `u ↦ (u, 0)`.
This version does not assume that `f` maps `φ.source` to `ψ.source`,
but that `f` is continuous at `x`.  -/
Manifold.IsImmersionAtOfComplement.mk_of_continuousAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} {F : Type u_5}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup E'']
  [inst_4 : NormedSpace 𝕜 E''] [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace 𝕜 F] {H : Type u_7}
  [inst_7 : TopologicalSpace H] {G : Type u_9} [inst_8 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} [inst_9 : TopologicalSpace M] [inst_10 : ChartedSpace H M]
  {N : Type u_13} [inst_11 : TopologicalSpace N] [inst_12 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M},
  ContinuousAt f x →
    ∀ (equiv : (E × F) ≃L[𝕜] E'') (domChart : OpenPartialHomeomorph M H) (codChart : OpenPartialHomeomorph N G),
      x ∈ domChart.source →
        f x ∈ codChart.source →
          domChart ∈ IsManifold.maximalAtlas I n M →
            codChart ∈ IsManifold.maximalAtlas J n N →
              Set.EqOn (↑(codChart.extend J) ∘ f ∘ ↑(domChart.extend I).symm) (⇑equiv ∘ fun x => (x, 0))
                  (domChart.extend I).target →
                Manifold.IsImmersionAtOfComplement F I J n f x
-- Mathlib.GroupTheory.Coset.Basic
leftCoset_rightCoset : ∀ {α : Type u_1} [inst : Semigroup α] (s : Set α) (a b : α), MulOpposite.op b • a • s = a • MulOpposite.op b • s
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Pred
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Pred.0.Std.Tactic.BVDecide.BVPred.bitblast.match_7.eq_2 : ∀ (motive : Std.Tactic.BVDecide.BVPred → Sort u_1) (w : ℕ) (expr : Std.Tactic.BVDecide.BVExpr w) (idx : ℕ)
  (h_1 :
    (w : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr w) →
        (op : Std.Tactic.BVDecide.BVBinPred) →
          (rhs : Std.Tactic.BVDecide.BVExpr w) → motive (Std.Tactic.BVDecide.BVPred.bin lhs op rhs))
  (h_2 :
    (w : ℕ) → (expr : Std.Tactic.BVDecide.BVExpr w) → (idx : ℕ) → motive (Std.Tactic.BVDecide.BVPred.getLsbD expr idx)),
  (match Std.Tactic.BVDecide.BVPred.getLsbD expr idx with
    | Std.Tactic.BVDecide.BVPred.bin lhs op rhs => h_1 w lhs op rhs
    | Std.Tactic.BVDecide.BVPred.getLsbD expr idx => h_2 w expr idx) =
    h_2 w expr idx
-- Lean.Expr
Lean.Expr.mdata.sizeOf_spec : ∀ (data : Lean.MData) (expr : Lean.Expr), sizeOf (Lean.Expr.mdata data expr) = 1 + sizeOf data + sizeOf expr
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey_insertMany_list_of_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {l : List ((a : α) × β a)} {k k' : α},
  cmp k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬cmp a.fst b.fst = Ordering.eq) l →
      k ∈ List.map Sigma.fst l → ∀ {h' : k' ∈ t.insertMany l}, (t.insertMany l).getKey k' h' = k
-- Mathlib.ModelTheory.LanguageMap
FirstOrder.Language.card_constantsOn : ∀ {α : Type u'}, (FirstOrder.Language.constantsOn α).card = Cardinal.mk α
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.EqCnstrProof.superpose_ac.sizeOf_spec : ∀ (r₁ c r₂ : Lean.Grind.AC.Seq) (c₁ c₂ : Lean.Meta.Grind.AC.EqCnstr),
  sizeOf (Lean.Meta.Grind.AC.EqCnstrProof.superpose_ac r₁ c r₂ c₁ c₂) =
    1 + sizeOf r₁ + sizeOf c + sizeOf r₂ + sizeOf c₁ + sizeOf c₂
-- Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Torsion
/-- The torsion of a covariant derivative on the tangent bundle `TM`, as a bare function.
Prefer to use `IsCovariantDerivativeOn.torsion` (which is a 2-tensor) instead.  -/
_private.Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Torsion.0.IsCovariantDerivativeOn.torsionAux : {𝕜 : 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] →
                      (((x : M) → TangentSpace I x) → (x : M) → TangentSpace I x →L[𝕜] TangentSpace I x) →
                        ((x : M) → TangentSpace I x) → ((x : M) → TangentSpace I x) → (x : M) → TangentSpace I x
-- Mathlib.Topology.UniformSpace.Basic
interior_mem_uniformity : ∀ {α : Type ua} [inst : UniformSpace α] {s : SetRel α α}, s ∈ uniformity α → interior s ∈ uniformity α
-- Mathlib.Topology.Constructions.SumProd
/-- `X × {*}` is homeomorphic to `X`.  -/
Homeomorph.prodPUnit : (X : Type u) → [inst : TopologicalSpace X] → X × PUnit.{u_7 + 1} ≃ₜ X
-- Mathlib.Algebra.Field.Shrink
Shrink.instDivisionRing : {α : Type u_1} → [inst : Small.{v, u_1} α] → [DivisionRing α] → DivisionRing (Shrink.{v, u_1} α)
-- Mathlib.Topology.MetricSpace.Defs
/-- Characterize the equality of points as the vanishing of the nonnegative distance  -/
nndist_eq_zero : ∀ {γ : Type w} [inst : MetricSpace γ] {x y : γ}, nndist x y = 0 ↔ x = y
-- Mathlib.Analysis.Normed.Lp.WithLp
/-- This prevents `toLp p x` being printed as `{ ofLp := x }` by `delabStructureInstance`.  -/
WithLp.delabToLp : Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.Order.Interval.Finset.Basic
Finset.nonempty_Ioc : ∀ {α : Type u_2} {a b : α} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α], (Finset.Ioc a b).Nonempty ↔ a < b
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
CategoryTheory.IsPushout.app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [CategoryTheory.Limits.HasPushouts D] {F₁ F₂ F₃ F₄ : CategoryTheory.Functor C D} {f₁ : F₁ ⟶ F₂} {f₂ : F₁ ⟶ F₃}
  {f₃ : F₂ ⟶ F₄} {f₄ : F₃ ⟶ F₄},
  CategoryTheory.IsPushout f₁ f₂ f₃ f₄ → ∀ (X : C), CategoryTheory.IsPushout (f₁.app X) (f₂.app X) (f₃.app X) (f₄.app X)
-- Mathlib.Order.Interval.Finset.Nat
Nat.card_Iio : ∀ (b : ℕ), (Finset.Iio b).card = b
-- Mathlib.Topology.Homotopy.TopCat.Basic
/-- The compositions of homotopies in `TopCat`.  -/
TopCat.Homotopy.trans : {X Y : TopCat} →
  {f₀ f₁ f₂ : X ⟶ Y} → TopCat.Homotopy f₀ f₁ → TopCat.Homotopy f₁ f₂ → (TopCat.Hom.hom f₀).Homotopy (TopCat.Hom.hom f₂)
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientGroup.image_coe : ∀ {G : Type u_1} [inst : Group G] (N : Subgroup G) [nN : N.Normal], QuotientGroup.mk '' ↑N = 1
-- Mathlib.NumberTheory.LucasLehmer
LucasLehmer.norm_num_ext.sModNatAux.eq_def : ∀ (b q x : ℕ),
  LucasLehmer.norm_num_ext.sModNatAux b q x =
    match x with
    | 0 => b
    | i.succ => (LucasLehmer.norm_num_ext.sModNatAux b q i ^ 2 + (q - 2)) % q
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.contains_of_contains_filter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  {f : (a : α) → β a → Bool} {k : α}, t.WF → (Std.DTreeMap.Raw.filter f t).contains k = true → t.contains k = true
-- Mathlib.Algebra.Category.MonCat.Basic
_private.Mathlib.Algebra.Category.MonCat.Basic.0.MonCat.Hom.mk.injEq : ∀ {A B : MonCat} (hom' hom'_1 : ↑A →* ↑B), ({ hom' := hom' } = { hom' := hom'_1 }) = (hom' = hom'_1)
-- Mathlib.Data.Int.Cast.Lemmas
/-- Coercion `ℕ → ℤ` as a `RingHom`.  -/
Int.ofNatHom : ℕ →+* ℤ