mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rcc.toList_eq_if_roc : ∀ {α : Type u} {r : Std.Rcc α} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLE α]
  [inst_5 : Std.Rxc.IsAlwaysFinite α],
  r.toList = if r.lower ≤ r.upper then r.lower :: (r.lower<...=r.upper).toList else []
-- Mathlib.Analysis.Calculus.LogDeriv
logDeriv_mul : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {f g : 𝕜 → 𝕜'} (x : 𝕜),
  f x ≠ 0 →
    g x ≠ 0 →
      DifferentiableAt 𝕜 f x → DifferentiableAt 𝕜 g x → logDeriv (fun z => f z * g z) x = logDeriv f x + logDeriv g x
-- Mathlib.Analysis.Asymptotics.TVS
Asymptotics.isLittleOTVS_iff_tendsto_div : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommGroup F]
  [inst_5 : TopologicalSpace F] [inst_6 : Module 𝕜 F] {f : α → E} {g : α → F} {l : Filter α},
  f =o[𝕜; l] g ↔ ∀ U ∈ nhds 0, ∃ V ∈ nhds 0, Filter.Tendsto (fun x => egauge 𝕜 U (f x) / egauge 𝕜 V (g x)) l (nhds 0)
-- Mathlib.Algebra.Category.ModuleCat.Topology.Basic
/-- The underlying topological space.  -/
TopModuleCat.topologicalSpace : {R : Type u} →
  [inst : Ring R] → [inst_1 : TopologicalSpace R] → (self : TopModuleCat R) → TopologicalSpace ↑self.toModuleCat
-- Lean.Server.Requests
Lean.Server.StatefulRequestHandler.fileSource : Lean.Server.StatefulRequestHandler → Lean.Json → Except Lean.Server.RequestError Lean.Lsp.DocumentUri
-- Mathlib.LinearAlgebra.PerfectPairing.Restrict
/-- The restriction of a perfect pairing to submodules is a perfect pairing.  -/
LinearMap.IsPerfPair.restrict : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] (p : M →ₗ[R] N →ₗ[R] R) [inst_5 : p.IsPerfPair] {M' : Type u_4}
  {N' : Type u_5} [inst_6 : AddCommGroup M'] [inst_7 : Module R M'] [inst_8 : AddCommGroup N'] [inst_9 : Module R N']
  (i : M' →ₗ[R] M) (j : N' →ₗ[R] N),
  Function.Injective ⇑i → Function.Injective ⇑j → p.IsPerfectCompl i.range j.range → (p.compl₁₂ i j).IsPerfPair
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
nonneg_le_nonneg_of_sq_le_sq : ∀ {R : Type u} [inst : Semiring R] [inst_1 : LinearOrder R] [PosMulStrictMono R] [MulPosMono R] {a b : R},
  0 ≤ b → a * a ≤ b * b → a ≤ b
-- Mathlib.Algebra.Category.Ring.Constructions
CommRingCat.coproductCocone_pt : ∀ (A B : CommRingCat), (A.coproductCocone B).pt = CommRingCat.of (TensorProduct ℤ ↑A ↑B)
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
abs_of_pos : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : AddGroup α] {a : α} [AddLeftMono α], 0 < a → |a| = a
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.MonoidalOpposite.unmopFunctor_ε : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C],
  CategoryTheory.Functor.LaxMonoidal.ε (CategoryTheory.unmopFunctor C) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
-- Mathlib.Algebra.Polynomial.Monic
Polynomial.Monic.add_of_right : ∀ {R : Type u} [inst : Semiring R] {p q : Polynomial R}, q.Monic → p.degree < q.degree → (p + q).Monic
-- Std.Data.DTreeMap.Basic
/-- Tries to retrieve the smallest key that is greater than or equal to the
given key, returning `none` if no such key exists.
 -/
Std.DTreeMap.getKeyGE? : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → Std.DTreeMap α β cmp → α → Option α
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.succ_ok : ∀ {q : Turing.PartrecToTM2.Λ'} {s : Option Turing.PartrecToTM2.Γ'} {n : ℕ} {c d : List Turing.PartrecToTM2.Γ'},
  StateTransition.Reaches₁ (Turing.TM2.step Turing.PartrecToTM2.tr)
    { l := some q.succ, var := s, stk := Turing.PartrecToTM2.K'.elim (Turing.PartrecToTM2.trList [n]) [] c d }
    { l := some q, var := none, stk := Turing.PartrecToTM2.K'.elim (Turing.PartrecToTM2.trList [n.succ]) [] c d }
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.MonoFactorisation.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      {f : X ⟶ Y} →
        (I : C) →
          (m : I ⟶ Y) →
            [m_mono : CategoryTheory.Mono m] →
              (e : X ⟶ I) →
                autoParam (CategoryTheory.CategoryStruct.comp e m = f)
                    CategoryTheory.Limits.MonoFactorisation.fac._autoParam →
                  CategoryTheory.Limits.MonoFactorisation f
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.hasFPowerSeriesAt_derivWeierstrassPExcept : ∀ (L : PeriodPair) (l : ℂ),
  HasFPowerSeriesAt (L.derivWeierstrassPExcept l)
    (FormalMultilinearSeries.ofScalars ℂ fun i => (↑i + 1) * (↑i + 2) * L.sumInvPow l (i + 3)) l
-- Mathlib.Order.UpperLower.Prod
LowerSet.prod_bot : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (s : LowerSet α), s ×ˢ ⊥ = ⊥
-- Init.Data.Array.Lemmas
_private.Init.Data.Array.Lemmas.0.Array.firstM.go.eq_1 : ∀ {β : Type v} {α : Type u} {m : Type v → Type w} [inst : Alternative m] (f : α → m β) (as : Array α) (i : ℕ),
  Array.firstM.go✝ f as i = if hlt : i < as.size then f as[i] <|> Array.firstM.go✝ f as (i + 1) else failure
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.U_eq_two_mul_T_add_U : ∀ (R : Type u_1) [inst : CommRing R] (n : ℤ),
  Polynomial.Chebyshev.U R (n + 2) = 2 * Polynomial.Chebyshev.T R (n + 2) + Polynomial.Chebyshev.U R n
-- Plausible.Sampleable
Plausible.Prop.sampleableExt : Plausible.SampleableExt Prop
-- Init.Prelude
/-- A success value of type `α`  -/
Except.ok : {ε : Type u} → {α : Type v} → α → Except ε α
-- Init.Core
/-- Notation type class for the intersection operation `∩`.  -/
Inter : Type u → Type u
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing
/-- A pairing is proper when each type (II) simplex
is uniquely a `1`-codimensional face of the corresponding (I)
simplex.  -/
SSet.Subcomplex.Pairing.IsProper : {X : SSet} → {A : X.Subcomplex} → A.Pairing → Prop
-- Std.Data.DTreeMap.Internal.Operations
/-- Computes the union of the given tree maps. If a key appears in both maps, the entry contained in the second argument will appear in the result.

This function always merges the smaller map into the larger map.
 -/
Std.DTreeMap.Internal.Impl.union : {α : Type u} →
  {β : α → Type v} →
    [Ord α] → (t₁ t₂ : Std.DTreeMap.Internal.Impl α β) → t₁.Balanced → t₂.Balanced → Std.DTreeMap.Internal.Impl α β
-- Std.Data.HashMap.Lemmas
Std.HashMap.not_mem_inter_of_not_mem_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α}, k ∉ m₁ → k ∉ m₁ ∩ m₂
-- Std.Data.TreeSet.Raw.Basic
/-- Creates a new empty tree set. It is also possible and recommended to
use the empty collection notations `∅` and `{}` to create an empty tree set. `simp` replaces
`empty` with `∅`.
 -/
Std.TreeSet.Raw.filter : {α : Type u} → {cmp : α → α → Ordering} → (α → Bool) → Std.TreeSet.Raw α cmp → Std.TreeSet.Raw α cmp
-- Init.Data.UInt.Lemmas
UInt8.toUInt16_ofNat : ∀ {n : ℕ}, n < 256 → (OfNat.ofNat n).toUInt16 = OfNat.ofNat n
-- Mathlib.Data.Ordmap.Invariants
_private.Mathlib.Data.Ordmap.Invariants.0.Ordnode.findMax'.match_1.splitter : {α : Type u_1} →
  (motive : α → Ordnode α → Sort u_2) →
    (x : α) →
      (x_1 : Ordnode α) →
        ((x : α) → motive x Ordnode.nil) →
          ((x : α) →
              (size : ℕ) → (l : Ordnode α) → (x_2 : α) → (r : Ordnode α) → motive x (Ordnode.node size l x_2 r)) →
            motive x x_1
-- Mathlib.GroupTheory.Coset.Defs
QuotientGroup.instHasQuotientSubgroup.eq_1 : ∀ {α : Type u_1} [inst : Group α],
  QuotientGroup.instHasQuotientSubgroup = { Quotient := fun s => Quotient (QuotientGroup.leftRel s) }
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.DropWhile
_private.Std.Data.Iterators.Lemmas.Combinators.Monadic.DropWhile.0.Std.Iterators.Types.DropWhile.instIterator.match_3.eq_2 : ∀ {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [inst : Std.Iterator α m β]
  {P : β → Std.Iterators.PostconditionT m (ULift.{u_1, 0} Bool)} (it : Std.IterM m β)
  (motive : it.internalState.inner.Step → Sort u_3) (it' : Std.IterM m β)
  (h : it.internalState.inner.IsPlausibleStep (Std.IterStep.skip it'))
  (h_1 :
    (it' : Std.IterM m β) →
      (out : β) →
        (h : it.internalState.inner.IsPlausibleStep (Std.IterStep.yield it' out)) →
          motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 :
    (it' : Std.IterM m β) →
      (h : it.internalState.inner.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (h : it.internalState.inner.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩),
  (match ⟨Std.IterStep.skip it', h⟩ with
    | ⟨Std.IterStep.yield it' out, h⟩ => h_1 it' out h
    | ⟨Std.IterStep.skip it', h⟩ => h_2 it' h
    | ⟨Std.IterStep.done, h⟩ => h_3 h) =
    h_2 it' h
-- Aesop.Percent
Aesop.Percent.hundred : Aesop.Percent
-- Mathlib.Tactic.FunProp.Types
/-- `fun_prop` config  -/
Mathlib.Meta.FunProp.Context.config : Mathlib.Meta.FunProp.Context → Mathlib.Meta.FunProp.Config
-- Mathlib.Topology.CompactOpen
ContinuousMap.homeoFnOfDiscrete_symm_apply_apply : ∀ {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [inst_2 : DiscreteTopology X]
  (f : X → Y) (a : X), (ContinuousMap.homeoFnOfDiscrete.symm f) a = f a
-- Mathlib.MeasureTheory.Measure.Haar.Extension
/-- If `φ : A →* B` and `ψ : B →* C` define a short exact sequence of topological groups, then we
can pull back a continuous compactly supported function `f` on `B` along `φ` to the continuous
compactly supported function `a ↦ f (b * φ a)` on `A`.  -/
TopologicalGroup.IsSES.pullback : {A : Type u_1} →
  {B : Type u_2} →
    {C : Type u_3} →
      {E : Type u_4} →
        [inst : Group A] →
          [inst_1 : Group B] →
            [inst_2 : Group C] →
              [inst_3 : TopologicalSpace A] →
                [inst_4 : TopologicalSpace B] →
                  [inst_5 : TopologicalSpace C] →
                    {φ : A →* B} →
                      {ψ : B →* C} →
                        TopologicalGroup.IsSES φ ψ →
                          [IsTopologicalGroup A] →
                            [IsTopologicalGroup B] →
                              [inst : NormedAddCommGroup E] →
                                CompactlySupportedContinuousMap B E → B → CompactlySupportedContinuousMap A E
-- Std.Data.HashSet.Lemmas
Std.HashSet.get_ofList_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List α} {k k' : α},
  (k == k') = true →
    List.Pairwise (fun a b => (a == b) = false) l →
      k ∈ l → ∀ {h : k' ∈ Std.HashSet.ofList l}, (Std.HashSet.ofList l).get k' h = k
-- Mathlib.LinearAlgebra.AffineSpace.Ordered
pos_of_slope_pos : ∀ {𝕜 : Type u_4} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {f : 𝕜 → 𝕜} {x₀ b : 𝕜},
  x₀ < b → 0 < slope f x₀ b → f x₀ = 0 → 0 < f b
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.le_pi_iff : ∀ {η : Type u_7} {f : η → Type u_8} [inst : (i : η) → Group (f i)] {I : Set η} {H : (i : η) → Subgroup (f i)}
  {J : Subgroup ((i : η) → f i)}, J ≤ Subgroup.pi I H ↔ ∀ i ∈ I, J ≤ Subgroup.comap (Pi.evalMonoidHom f i) (H i)
-- Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Monoidal
QuadraticModuleCat.toIsometry_tensorHom : ∀ {R : Type u} [inst : CommRing R] [inst_1 : Invertible 2] {K L M N : QuadraticModuleCat R} (f : K ⟶ L) (g : M ⟶ N),
  QuadraticModuleCat.Hom.toIsometry (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) =
    (QuadraticModuleCat.Hom.toIsometry f).tmul (QuadraticModuleCat.Hom.toIsometry g)
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
CategoryTheory.Limits.WidePullbackCone.reindex_base : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {ι : Type u_2} {X : C} {Y : ι → C} {f : (i : ι) → Y i ⟶ X}
  (s : CategoryTheory.Limits.WidePullbackCone f) {ι' : Type u_3} (e : ι' ≃ ι), (s.reindex e).base = s.base
-- Mathlib.Data.Seq.Computation
Computation.monad : Monad Computation
-- Mathlib.Data.DFinsupp.Ext
DFinsupp.addHom_ext'_iff : ∀ {ι : Type u} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → AddZeroClass (β i)] {γ : Type w}
  [inst_2 : AddZeroClass γ] {f g : (Π₀ (i : ι), β i) →+ γ},
  f = g ↔ ∀ (x : ι), f.comp (DFinsupp.singleAddHom β x) = g.comp (DFinsupp.singleAddHom β x)
-- Lean.Elab.Do.Basic
/-- The cached `PUnit` expression.  -/
Lean.Elab.Do.mkPUnit : Lean.Elab.Do.DoElabM Lean.Expr
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
isAdjointPair_toLinearMap₂' : ∀ {R : Type u_1} {n : Type u_11} {n' : Type u_13} [inst : CommRing R] [inst_1 : Fintype n] [inst_2 : Fintype n']
  (J : Matrix n n R) (J' : Matrix n' n' R) (A : Matrix n' n R) (A' : Matrix n n' R) [inst_3 : DecidableEq n]
  [inst_4 : DecidableEq n'],
  ((Matrix.toLinearMap₂' R) J).IsAdjointPair ((Matrix.toLinearMap₂' R) J') ⇑(Matrix.toLin' A) ⇑(Matrix.toLin' A') ↔
    J.IsAdjointPair J' A A'
-- Mathlib.Topology.Compactness.Compact
Set.Finite.isCompact_sUnion : ∀ {X : Type u} [inst : TopologicalSpace X] {S : Set (Set X)}, S.Finite → (∀ s ∈ S, IsCompact s) → IsCompact (⋃₀ S)
-- Mathlib.Analysis.Distribution.TemperateGrowth
/-- A function has temperate growth if and only if it is smooth and its `n`-th iterated
derivative is `O((1 + ‖x‖) ^ k)` for some `k : ℕ` (depending on `n`).

Note that the `O` here is with respect to the `⊤` filter, meaning that the bound holds everywhere.

TODO: when `E` is finite dimensional, this is equivalent to the derivatives being `O(‖x‖ ^ k)`
as `‖x‖ → ∞`.
 -/
Function.hasTemperateGrowth_iff_isBigO : ∀ {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {f : E → F},
  Function.HasTemperateGrowth f ↔ ContDiff ℝ (↑⊤) f ∧ ∀ (n : ℕ), ∃ k, iteratedFDeriv ℝ n f =O[⊤] fun x => (1 + ‖x‖) ^ k
-- Mathlib.RingTheory.RingHomProperties
RingHom.CodescendsAlong.mk : ∀ {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop}
  (Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop),
  (RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => P) →
    (∀ ⦃R S T : Type u⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
        [inst_4 : Algebra R T], Q (algebraMap R S) → P (algebraMap S (TensorProduct R S T)) → P (algebraMap R T)) →
      RingHom.CodescendsAlong (fun {R S} [CommRing R] [CommRing S] => P) fun {R S} [CommRing R] [CommRing S] => Q
-- Lean.Meta.Tactic.Grind.EMatchTheorem
/-- State for the (pattern) `CollectorM` monad  -/
_private.Lean.Meta.Tactic.Grind.EMatchTheorem.0.Lean.Meta.Grind.Collector.State : Type
-- Std.Data.HashMap.Raw
/-- Updates the values of the hash map by applying the given function to all mappings, keeping
only those mappings where the function returns `some` value.
 -/
Std.HashMap.Raw.filterMap : {α : Type u} → {β : Type v} → {γ : Type w} → (α → β → Option γ) → Std.HashMap.Raw α β → Std.HashMap.Raw α γ
-- Mathlib.Data.Finset.Lattice.Fold
Finset.sup'.congr_simp : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeSup α] (s s_1 : Finset β) (e_s : s = s_1) (H : s.Nonempty)
  (f f_1 : β → α), f = f_1 → s.sup' H f = s_1.sup' ⋯ f_1
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
/-- The morphism in the constructed localized category that is induced by a left fraction.  -/
CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom.mk : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {W : CategoryTheory.MorphismProperty C} →
      {X Y : C} → W.LeftFraction X Y → CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom W X Y
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.coe_toEquiv : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : AddCommGroup V₂] [inst_3 : Module k V₁] [inst_4 : Module k V₂]
  [inst_5 : AddTorsor V₁ P₁] [inst_6 : AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂), ⇑e.toEquiv = ⇑e
-- Mathlib.Algebra.Order.Monoid.Canonical.Defs
CanonicallyOrderedAdd.mk : ∀ {α : Type u_1} [inst : Add α] [inst_1 : LE α] [toExistsAddOfLE : ExistsAddOfLE α],
  (∀ (a b : α), a ≤ b + a) → (∀ (a b : α), a ≤ a + b) → CanonicallyOrderedAdd α
-- Mathlib.Analysis.Convex.Side
Affine.Simplex.sOppSide_affineSpan_faceOpposite_point_right_iff : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Field R] [inst_1 : LinearOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P] {n : ℕ}
  [inst_6 : NeZero n] (s : Affine.Simplex R P n) {w : Fin (n + 1) → R},
  ∑ j, w j = 1 →
    ∀ {i : Fin (n + 1)},
      (affineSpan R (Set.range (s.faceOpposite i).points)).SOppSide
          ((Finset.affineCombination R Finset.univ s.points) w) (s.points i) ↔
        w i < 0
-- Std.Do.SPred.SVal
Std.Do.SVal.uncurry.eq_def : ∀ {α : Type u} {σs : List (Type u)} (f : Std.Do.SVal σs α),
  f.uncurry =
    match (motive := (σs : List (Type u)) → Std.Do.SVal σs α → Std.Do.SVal.StateTuple σs → α) σs, f with
    | [], f => fun x => f
    | head :: tail, f => fun x =>
      match x with
      | (s, t) => (f s).uncurry t
-- Mathlib.Order.Filter.Prod
Filter.prod_principal_principal : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β},
  Filter.principal s ×ˢ Filter.principal t = Filter.principal (s ×ˢ t)
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
/-- An angle in a non-degenerate right-angled triangle is less than `π / 2`.  -/
EuclideanGeometry.angle_lt_pi_div_two_of_angle_eq_pi_div_two : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {p₁ p₂ p₃ : P},
  EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi / 2 → p₃ ≠ p₂ → EuclideanGeometry.angle p₂ p₃ p₁ < Real.pi / 2
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalSubalgebra.instIsScalarTowerSubtypeMem : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  {S : NonUnitalSubalgebra R A} [IsScalarTower R A A], IsScalarTower R ↥S ↥S
-- Mathlib.MeasureTheory.Function.L1Space.AEEqFun
MeasureTheory.L1.aestronglyMeasurable_coeFn : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  (f : ↥(MeasureTheory.Lp β 1 μ)), MeasureTheory.AEStronglyMeasurable (↑↑f) μ
-- Mathlib.Control.Functor
Functor.Comp.instInhabited : {F : Type u → Type w} → {G : Type v → Type u} → {α : Type v} → [Inhabited (F (G α))] → Inhabited (Functor.Comp F G α)
-- Mathlib.NumberTheory.ModularForms.SlashActions
_private.Mathlib.NumberTheory.ModularForms.SlashActions.0.ModularForm.add_slash : ∀ (k : ℤ) (A : GL (Fin 2) ℝ) (f g : UpperHalfPlane → ℂ),
  ModularForm.privateSlash✝ k A (f + g) = ModularForm.privateSlash✝ k A f + ModularForm.privateSlash✝ k A g
-- Init.System.IOError
IO.Error.userError.injEq : ∀ (msg msg_1 : String), (IO.Error.userError msg = IO.Error.userError msg_1) = (msg = msg_1)
-- Std.Sync.CancellationToken
Std.CancellationToken.State.mk.injEq : ∀ (reason : Option Std.CancellationReason) (consumers : Std.Queue Std.CancellationToken.Consumer)
  (reason_1 : Option Std.CancellationReason) (consumers_1 : Std.Queue Std.CancellationToken.Consumer),
  ({ reason := reason, consumers := consumers } = { reason := reason_1, consumers := consumers_1 }) =
    (reason = reason_1 ∧ consumers = consumers_1)
-- Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
/-- The unique existence of an inverse to `spine X m` for all `m ≤ n + 1`
implies the mere existence of such an inverse.  -/
SSet.Truncated.StrictSegal.isStrictSegal : ∀ {n : ℕ} {X : SSet.Truncated (n + 1)} (sx : X.StrictSegal), X.IsStrictSegal
-- Std.Http.Protocol.H1.Reader
Std.Http.Protocol.H1.Reader.instReprBodyState : Repr Std.Http.Protocol.H1.Reader.BodyState
-- Mathlib.Geometry.Convex.Star
/-- A set `s` is star-convex at a point `x` if every segment from `x` to a point in `s` is
contained in `s`.

TODO: Replace `StarConvex` with this predicate.  -/
Convexity.IsStarConvexSet : (R : Type u_1) →
  {X : Type u_2} →
    [inst : Semiring R] →
      [inst_1 : PartialOrder R] → [inst_2 : IsStrictOrderedRing R] → [Convexity.ConvexSpace R X] → X → Set X → Prop
-- Init.Data.Function
Function.LeftInverse.injective : ∀ {α : Sort u_1} {β : Sort u_2} {g : β → α} {f : α → β}, Function.LeftInverse g f → Function.Injective f
-- Init.Data.Range.Polymorphic.Nat
Std.instHasRcoIntersectionNat_6 : Std.Rio.HasRcoIntersection ℕ
-- Mathlib.CategoryTheory.Limits.Shapes.End
/-- Given `F : Jᵒᵖ ⥤ J ⥤ C`, a cowedge for `F` is a type of cocones
(specifically the type of multicoforks for `multispanIndexCoend F`):
the point of a universal cowedge is the coend of `F`.  -/
CategoryTheory.Limits.Cowedge : {J : Type u} →
  [inst : CategoryTheory.Category.{v, u} J] →
    {C : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} C] →
        CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C) → Type (max (max (max u v) u') v')
-- Mathlib.Tactic.NormNum.Core
/-- Erases a name marked `norm_num` by adding it to the state's `erased` field and
removing it from the state's list of `Entry`s.  -/
Mathlib.Meta.NormNum.NormNums.eraseCore : Mathlib.Meta.NormNum.NormNums → Lean.Name → Mathlib.Meta.NormNum.NormNums
-- Mathlib.Data.Set.Functor
Set.seqLeft_def : ∀ {α β : Type u} (s : Set α) (t : Set β), s <* t = {a | a ∈ s ∧ t.Nonempty}
-- Mathlib.FieldTheory.Perfect
iterateFrobeniusEquiv_symm_add_apply : ∀ (R : Type u_1) (p m n : ℕ) [inst : CommSemiring R] [inst_1 : ExpChar R p] [inst_2 : PerfectRing R p] (x : R),
  (iterateFrobeniusEquiv R p (m + n)).symm x = (iterateFrobeniusEquiv R p m).symm ((iterateFrobeniusEquiv R p n).symm x)
-- Mathlib.CategoryTheory.Limits.Cones
/-- **Alias** of `CategoryTheory.Limits.Cocone.forget`.

---

Forget the cocone structure and obtain just the cocone point.  -/
CategoryTheory.Limits.Cocones.forget : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        (F : CategoryTheory.Functor J C) → CategoryTheory.Functor (CategoryTheory.Limits.Cocone F) C
-- Mathlib.Algebra.Quandle
Rack.PreEnvelGroup.unit : {R : Type u} → Rack.PreEnvelGroup R
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.mem_of_mem_erase : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k a : α},
  a ∈ t.erase k → a ∈ t
-- Lean.Server.CodeActions.Attr
/-- A hole code action extension.  -/
Lean.CodeAction.HoleCodeAction : Type
-- Mathlib.Analysis.Calculus.LocalExtr.LineDeriv
IsLocalMax.lineDeriv_eq_zero : ∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : Module ℝ E] [inst_2 : TopologicalSpace E] [ContinuousAdd E]
  [ContinuousSMul ℝ E] {f : E → ℝ} {a : E}, IsLocalMax f a → lineDeriv ℝ f a = 0
-- Mathlib.Analysis.Complex.Conformal
/-- In cases where the **Cauchy-Riemann Equation** guarantees complex differentiability at `x`, the
complex derivative equals `ContinuousLinearMap.complexOfReal` of the real derivative.
 -/
complexOfReal_fderivWithin : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : ℂ → E} {x : ℂ} {s : Set ℂ},
  DifferentiableWithinAt ℝ f s x →
    ∀ (h₂ : (fderivWithin ℝ f s x) Complex.I = Complex.I • (fderivWithin ℝ f s x) 1),
      UniqueDiffWithinAt ℝ s x → fderivWithin ℂ f s x = (fderivWithin ℝ f s x).complexOfReal h₂
-- Mathlib.Analysis.Normed.Unbundled.AlgebraNorm
AlgebraNormClass.mk : ∀ {F : Type u_1} {R : outParam (Type u_2)} [inst : SeminormedCommRing R] {S : outParam (Type u_3)} [inst_1 : Ring S]
  [inst_2 : Algebra R S] [inst_3 : FunLike F S ℝ] [toRingNormClass : RingNormClass F S ℝ],
  (∀ (f : F) (a : R) (x : S), f (a • x) = ‖a‖ * f x) → AlgebraNormClass F R S
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.takeWhile_eq_self_iff : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.ForwardPattern pat] {s : String.Slice},
  s.takeWhile pat = s ↔ s.all pat = true