mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Matrix.Basic
LinearEquiv.mapMatrix_symm : ∀ {m : Type u_2} {n : Type u_3} {R : Type u_7} {S : Type u_8} {α : Type u_11} {β : Type u_12} [inst : Semiring R]
  [inst_1 : Semiring S] [inst_2 : AddCommMonoid α] [inst_3 : AddCommMonoid β] [inst_4 : Module R α]
  [inst_5 : Module S β] {σᵣₛ : R →+* S} {σₛᵣ : S →+* R} [inst_6 : RingHomInvPair σᵣₛ σₛᵣ]
  [inst_7 : RingHomInvPair σₛᵣ σᵣₛ] (f : α ≃ₛₗ[σᵣₛ] β), f.mapMatrix.symm = f.symm.mapMatrix
-- Mathlib.Combinatorics.Enumerative.Composition
CompositionAsSet.boundary_zero : ∀ {n : ℕ} (c : CompositionAsSet n), c.boundary ⟨0, ⋯⟩ = 0
-- Mathlib.Algebra.Group.Int.Even
Int.even_add_one : ∀ {n : ℤ}, Even (n + 1) ↔ ¬Even n
-- Mathlib.RepresentationTheory.Subrepresentation
Subrepresentation.ext_iff : ∀ {A : Type u_1} {G : Type u_2} {W : Type u_3} {inst : Semiring A} {inst_1 : Monoid G} {inst_2 : AddCommMonoid W}
  {inst_3 : Module A W} {ρ : Representation A G W} {x y : Subrepresentation ρ}, x = y ↔ x.toSubmodule = y.toSubmodule
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
WeierstrassCurve.ψ.eq_1 : ∀ {R : Type r} [inst : CommRing R] (W : WeierstrassCurve R) (n : ℤ),
  W.ψ n = normEDS W.ψ₂ (Polynomial.C W.Ψ₃) (Polynomial.C W.preΨ₄) n
-- Init.Data.UInt.Lemmas
UInt64.toUInt32_ofNatTruncate_of_lt : ∀ {n : ℕ}, n < UInt64.size → (UInt64.ofNatClamp n).toUInt32 = UInt32.ofNat n
-- Mathlib.LinearAlgebra.TensorProduct.Decomposition
DirectSum.Decomposition.baseChange : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      {S : Type u_4} →
        [inst : CommSemiring R] →
          [inst_1 : AddCommMonoid M] →
            [inst_2 : Module R M] →
              (ℳ : ι → Submodule R M) →
                [inst_3 : DecidableEq ι] →
                  [DirectSum.Decomposition ℳ] →
                    [inst_5 : CommSemiring S] →
                      [inst_6 : Algebra R S] → DirectSum.Decomposition fun i => Submodule.baseChange S (ℳ i)
-- Mathlib.RingTheory.Adjoin.Basic
/-- If `K / E / F` is a ring extension tower, `L` is a subalgebra of `K / F`,
then `E[L]` is generated by any basis of `L / F` as an `E`-module.  -/
Subalgebra.adjoin_eq_span_basis : ∀ {F : Type u_1} (E : Type u_2) {K : Type u_3} [inst : CommSemiring E] [inst_1 : Semiring K] [inst_2 : SMul F E]
  [inst_3 : Algebra E K] [inst_4 : CommSemiring F] [inst_5 : Algebra F K] [IsScalarTower F E K] (L : Subalgebra F K)
  {ι : Type u_4} (bL : Module.Basis ι F ↥L),
  Subalgebra.toSubmodule (Algebra.adjoin E ↑L) = Submodule.span E (Set.range fun i => ↑(bL i))
-- Mathlib.Algebra.Tropical.Basic
Tropical.instCommGroupOfAddCommGroup : {R : Type u} → [AddCommGroup R] → CommGroup (Tropical R)
-- Init.Data.String.Basic
/-- Converts a string to a list of characters.

Since strings are represented as dynamic arrays of bytes containing the string encoded using
UTF-8, this operation takes time and space linear in the length of the string.

Examples:
 * `"abc".toList = ['a', 'b', 'c']`
 * `"".toList = []`
 * `"\n".toList = ['\n']`
 -/
String.data : String → List Char
-- Mathlib.CategoryTheory.Bicategory.End
CategoryTheory.instCategoryEndMonoidal : {C : Type u} →
  [inst : CategoryTheory.Bicategory C] → (X : C) → CategoryTheory.Category.{w, v} (CategoryTheory.EndMonoidal X)
-- Mathlib.CategoryTheory.Shift.SingleFunctors
CategoryTheory.SingleFunctors.comp_hom_assoc : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {A : Type u_5} [inst_2 : AddMonoid A]
  [inst_3 : CategoryTheory.HasShift D A] {F G H : CategoryTheory.SingleFunctors C D A} (f : F ⟶ G) (g : G ⟶ H) (a : A)
  {Z : CategoryTheory.Functor C D} (h : H.functor a ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.CategoryStruct.comp f g).hom a) h =
    CategoryTheory.CategoryStruct.comp (f.hom a) (CategoryTheory.CategoryStruct.comp (g.hom a) h)
-- Std.Data.DHashMap.Basic
/-- Creates a new empty hash map. The optional parameter `capacity` can be supplied to presize the
map so that it can hold the given number of mappings without reallocating. It is also possible to
use the empty collection notations `∅` and `{}` to create an empty hash map with the default
capacity.
 -/
Std.DHashMap.emptyWithCapacity : {α : Type u} → {β : α → Type v} → [inst : BEq α] → [inst_1 : Hashable α] → optParam ℕ 8 → Std.DHashMap α β
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Algebra.adjoin_int : ∀ {R : Type u_1} [inst : Ring R] (s : Set R), Algebra.adjoin ℤ s = subalgebraOfSubring (Subring.closure s)
-- Lean.Parser.Syntax
Lean.Parser.Command.binderPredicate.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
_private.Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense.0.CategoryTheory.Functor.OneHypercoverDenseData.isSheaf_iff.liftAux_fac : ∀ {C₀ : Type u₀} {C : Type u} [inst : CategoryTheory.Category.{v₀, u₀} C₀] [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor C₀ C} {J₀ : CategoryTheory.GrothendieckTopology C₀}
  {J : CategoryTheory.GrothendieckTopology C} {A : Type u'} [inst_2 : CategoryTheory.Category.{v', u'} A]
  [inst_3 : CategoryTheory.Functor.IsDenseSubsite J₀ J F] {data : (X : C) → F.OneHypercoverDenseData J₀ J X}
  {G : CategoryTheory.Functor Cᵒᵖ A} (hG₀ : CategoryTheory.Presheaf.IsSheaf J₀ (F.op.comp G)) {X : C} {S : J.Cover X}
  (s : CategoryTheory.Limits.Multifork (S.index G)) {i : (data X).I₀} {W₀ : C₀} (a : W₀ ⟶ (data X).X i)
  (ha : (↑S).arrows (CategoryTheory.CategoryStruct.comp (F.map a) ((data X).f i))),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OneHypercoverDenseData.isSheaf_iff.liftAux✝ hG₀ s i)
      (G.map (F.map a).op) =
    s.ι { Y := F.obj W₀, f := CategoryTheory.CategoryStruct.comp (F.map a) ((data X).f i), hf := ha }
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.mem_of_mem_erase : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k a : α}, a ∈ t.erase k → a ∈ t
-- Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
/-- `WeierstrassCurve.IsElliptic` is a typeclass which asserts that a Weierstrass curve is an
elliptic curve: that its discriminant is a unit. Note that this definition is only mathematically
accurate for certain rings whose Picard group has trivial 12-torsion, such as a field or a PID.  -/
WeierstrassCurve.IsElliptic : {R : Type u} → [CommRing R] → WeierstrassCurve R → Prop
-- Mathlib.Algebra.Module.Bimodule
/-- A `Submodule` over `R ⊗[ℤ] S` is naturally also a `Submodule` over the canonically-isomorphic
ring `R ⊗[ℕ] S`.  -/
Subbimodule.toSubbimoduleNat : (R : Type u_1) →
  (S : Type u_2) →
    (M : Type u_3) →
      [inst : Ring R] →
        [inst_1 : Ring S] →
          [inst_2 : AddCommGroup M] →
            [inst_3 : Module R M] →
              [inst_4 : Module S M] →
                [inst_5 : SMulCommClass R S M] → Submodule (TensorProduct ℤ R S) M → Submodule (TensorProduct ℕ R S) M
-- Mathlib.Order.Hom.Bounded
TopHom.instPreorder : {α : Type u_2} → {β : Type u_3} → [inst : Top α] → [Preorder β] → [inst_2 : Top β] → Preorder (TopHom α β)
-- Mathlib.Topology.MetricSpace.Isometry
Isometry.inl : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] [inst_2 : AddZeroClass α]
  [inst_3 : AddZeroClass β], Isometry ⇑(AddMonoidHom.inl α β)
-- Mathlib.GroupTheory.Congruence.Basic
/-- The first isomorphism theorem for Monoids in the case of a surjective homomorphism.

For a `computable` version, see `Con.quotientKerEquivOfRightInverse`.
 -/
Con.quotientKerEquivOfSurjective : {M : Type u_1} →
  {P : Type u_3} →
    [inst : MulOneClass M] →
      [inst_1 : MulOneClass P] → (f : M →* P) → Function.Surjective ⇑f → (Con.ker f).Quotient ≃* P
-- Mathlib.Analysis.Normed.Group.Basic
mem_closedBall_iff_norm''' : ∀ {E : Type u_5} [inst : SeminormedCommGroup E] {a b : E} {r : ℝ}, b ∈ Metric.closedBall a r ↔ ‖a / b‖ ≤ r
-- Mathlib.Topology.Covering.Basic
IsEvenlyCovered.discreteTopology_fiber : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X} {I : Type u_3}
  [inst_2 : TopologicalSpace I] {x : X}, IsEvenlyCovered f x I → DiscreteTopology ↑(f ⁻¹' {x})
-- Std.Sync.Semaphore
_private.Std.Sync.Semaphore.0.Std.SemaphoreState.mk.injEq : ∀ (permits : ℕ) (waiters : Std.Queue (IO.Promise Unit)) (permits_1 : ℕ) (waiters_1 : Std.Queue (IO.Promise Unit)),
  ({ permits := permits, waiters := waiters } = { permits := permits_1, waiters := waiters_1 }) =
    (permits = permits_1 ∧ waiters = waiters_1)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.DTreeMap.Internal.Cell.Const.alter.match_1.eq_1 : ∀ {α : Type u_2} {β : Type u_1} (motive : Option ((_ : α) × β) → Sort u_3) (h_1 : Unit → motive none)
  (h_2 : (fst : α) → (v' : β) → motive (some ⟨fst, v'⟩)),
  (match none with
    | none => h_1 ()
    | some ⟨fst, v'⟩ => h_2 fst v') =
    h_1 ()
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.omega_ne_zero : Hyperreal.omega ≠ 0
-- Mathlib.CategoryTheory.Quotient.Preadditive
/-- The negation on the morphisms in the category `Quotient r` when `r` is compatible
with the addition.  -/
CategoryTheory.Quotient.Preadditive.neg : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      (r : HomRel C) →
        [CategoryTheory.Congruence r] →
          (∀ ⦃X Y : C⦄ (f₁ f₂ g₁ g₂ : X ⟶ Y), r f₁ f₂ → r g₁ g₂ → r (f₁ + g₁) (f₂ + g₂)) →
            {X Y : CategoryTheory.Quotient r} → (X ⟶ Y) → (X ⟶ Y)
-- Mathlib.Probability.Process.Adapted
/-- **Alias** of `MeasureTheory.IsStronglyProgressive.finsetProd`. -/
MeasureTheory.IsStronglyProgressive.finset_prod : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] {f : MeasureTheory.Filtration ι m}
  {β : Type u_3} [inst_1 : TopologicalSpace β] [inst_2 : MeasurableSpace ι] {γ : Type u_4} [inst_3 : CommMonoid β]
  [ContinuousMul β] {U : γ → ι → Ω → β} {s : Finset γ},
  (∀ c ∈ s, MeasureTheory.IsStronglyProgressive f (U c)) →
    MeasureTheory.IsStronglyProgressive f fun i a => ∏ c ∈ s, U c i a
-- Mathlib.RepresentationTheory.Coinvariants
/-- Given a `G`-representation `(V, ρ)` and a type `α`, this is the map `(α →₀ V_G) →ₗ (α →₀ V)_G`
sending `single a ⟦v⟧ ↦ ⟦single a v⟧`.  -/
Representation.finsuppToCoinvariants : {k : Type u_6} →
  {G : Type u_7} →
    {V : Type u_8} →
      [inst : CommRing k] →
        [inst_1 : Group G] →
          [inst_2 : AddCommGroup V] →
            [inst_3 : Module k V] →
              (ρ : Representation k G V) → (α : Type u_9) → (α →₀ ρ.Coinvariants) →ₗ[k] (ρ.finsupp α).Coinvariants
-- Mathlib.Algebra.Order.Group.Synonym
pow_toColex : ∀ {α : Type u_1} {β : Type u_2} [inst : Pow α β] (a : α) (b : β), a ^ toColex b = a ^ b
-- Mathlib.Topology.ContinuousOn
ContinuousOn.uncurry_left : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : TopologicalSpace γ] {f : α → β → γ} {sα : Set α} {sβ : Set β},
  ∀ a ∈ sα, ContinuousOn (Function.uncurry f) (sα ×ˢ sβ) → ContinuousOn (f a) sβ
-- Mathlib.Topology.MetricSpace.IsometricSMul
edist_inv_inv : ∀ {G : Type v} [inst : Group G] [inst_1 : PseudoEMetricSpace G] [IsIsometricSMul G G] [IsIsometricSMul Gᵐᵒᵖ G]
  (a b : G), edist a⁻¹ b⁻¹ = edist a b
-- Mathlib.Analysis.RCLike.Basic
RCLike.realLinearIsometryEquiv_apply : ∀ {K : Type u_1} [inst : RCLike K] (h : RCLike.I = 0) (a : K),
  (RCLike.realLinearIsometryEquiv h) a = (RCLike.realRingEquiv h).toFun a
-- Init.Grind.Offset
Lean.Grind.Nat.lo_eq_false_of_ro : ∀ (u v k₁ k₂ : ℕ), Lean.Grind.isLt k₁ k₂ = true → u ≤ v + k₁ → (v + k₂ ≤ u) = False
-- Std.Data.TreeMap.Raw.WF
Std.TreeMap.Raw.WF.insertMany : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] {ρ : Type u_1} [inst : ForIn Id ρ (α × β)]
  {l : ρ} {t : Std.TreeMap.Raw α β cmp}, t.WF → (t.insertMany l).WF
-- Lean.Meta.Sym.Apply
/-- Creates a `BackwardRule` from an expression.

`levelParams` is not `[]` if the expression is supposed to be
universe polymorphic.

The `num?` parameter optionally limits how many arguments are included in the pattern
(useful for partially applying theorems).
 -/
Lean.Meta.Sym.mkBackwardRuleFromExpr : Lean.Expr → optParam (List Lean.Name) [] → optParam (Option ℕ) none → Lean.MetaM Lean.Meta.Sym.BackwardRule
-- Mathlib.Geometry.Manifold.Bordism
SingularManifold.instBoundarylessManifoldRealM : ∀ {X : Type u_1} [inst : TopologicalSpace X] {k : WithTop ℕ∞} {E : Type u_4} {H : Type u_5}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E] [inst_3 : FiniteDimensional ℝ E]
  [inst_4 : TopologicalSpace H] {I : ModelWithCorners ℝ E H} {s : SingularManifold X k I}, BoundarylessManifold I s.M
-- Mathlib.Algebra.Group.Prod
addAddHom.eq_1 : ∀ {α : Type u_6} [inst : AddCommSemigroup α], addAddHom = { toFun := fun a => a.1 + a.2, map_add' := ⋯ }
-- Mathlib.Algebra.Order.Archimedean.Real.Basic
Real.iInf_of_isEmpty : ∀ {ι : Sort u_1} [IsEmpty ι] (f : ι → ℝ), ⨅ i, f i = 0
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.contains_minKeyD : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → t.isEmpty = false → ∀ {fallback : α}, t.contains (t.minKeyD fallback) = true
-- Std.Http.Data.Body.Stream
_private.Std.Http.Data.Body.Stream.0.Std.Http.Body.Channel.recvReady' : {m : Type → Type} → [Monad m] → [MonadLiftT (ST IO.RealWorld) m] → Std.AtomicT Std.Http.Body.Channel.State✝ m Bool
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey?_eq_some_iff : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k k' : α}, t.getKey? k = some k' ↔ ∃ (h : k ∈ t), t.getKey k h = k'
-- Mathlib.Data.Finset.Max
Finset.min'.congr_simp : ∀ {α : Type u_2} [inst : LinearOrder α] (s s_1 : Finset α) (e_s : s = s_1) (H : s.Nonempty), s.min' H = s_1.min' ⋯
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCast!_insertList_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {l toInsert : List ((a : α) × β a)} {k : α}
  [inst_2 : Inhabited (β k)],
  (List.map Sigma.fst toInsert).contains k = false →
    Std.Internal.List.getValueCast! k (Std.Internal.List.insertList l toInsert) = Std.Internal.List.getValueCast! k l
-- Mathlib.Data.Int.Bitwise
Int.xor.eq_3 : ∀ (m n : ℕ), (Int.negSucc m).xor (Int.ofNat n) = Int.negSucc (m ^^^ n)
-- Mathlib.FieldTheory.IsAlgClosed.Basic
/-- All `F`-embeddings of a field `K` into another field `A` factor through any intermediate
field of `A/F` in which the minimal polynomial of elements of `K` splits.  -/
IntermediateField.algHomEquivAlgHomOfSplits : {F : Type u_1} →
  {K : Type u_2} →
    (A : Type u_3) →
      [inst : Field F] →
        [inst_1 : Field K] →
          [inst_2 : Field A] →
            [inst_3 : Algebra F K] →
              [inst_4 : Algebra F A] →
                [Algebra.IsAlgebraic F K] →
                  (L : IntermediateField F A) →
                    (∀ (x : K), (Polynomial.map (algebraMap F ↥L) (minpoly F x)).Splits) → (K →ₐ[F] ↥L) ≃ (K →ₐ[F] A)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Replicate
Std.Tactic.BVDecide.BVExpr.bitblast.blastReplicate.go.eq_def : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {aig : Std.Sat.AIG α} {w : ℕ} (n : ℕ) (input : aig.RefVec w)
  (curr : ℕ) (hcurr : curr ≤ n) (s : aig.RefVec (w * curr)),
  Std.Tactic.BVDecide.BVExpr.bitblast.blastReplicate.go n input curr hcurr s =
    if h : curr < n then
      have s := s.append input;
      Std.Tactic.BVDecide.BVExpr.bitblast.blastReplicate.go n input (curr + 1) ⋯ s
    else
      have this := ⋯;
      this ▸ s
-- Mathlib.Algebra.Group.ModEq
/-- **Alias** of the reverse direction of `AddCommGroup.modEq_neg`. -/
AddCommGroup.ModEq.neg' : ∀ {G : Type u_1} [inst : AddCommGroup G] {p a b : G}, a ≡ b [PMOD p] → a ≡ b [PMOD -p]
-- Batteries.Data.BinomialHeap.Basic
/-- A forest of rank `r + 1` consists of a root `a`,
a forest `child` of rank `r` elements greater than `a`,
and another forest `sibling` of rank `r`.  -/
Batteries.BinomialHeap.Imp.HeapNode.node : {α : Type u} →
  α →
    Batteries.BinomialHeap.Imp.HeapNode α →
      Batteries.BinomialHeap.Imp.HeapNode α → Batteries.BinomialHeap.Imp.HeapNode α
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.re_one : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} [inst : Zero R] [inst_1 : One R], QuaternionAlgebra.re 1 = 1
-- Std.Http.Data.Status
/-- 417 Expectation Failed
 -/
Std.Http.Status.expectationFailed : Std.Http.Status
-- Mathlib.MeasureTheory.Measure.Prokhorov
/-- **Prokhorov theorem**: the closure of a tight set of probability measures is compact.
We only require the space to be T2.  -/
isCompact_closure_of_isTightMeasureSet : ∀ {E : Type u_1} [inst : MeasurableSpace E] [inst_1 : TopologicalSpace E] [T2Space E] [inst_3 : BorelSpace E]
  {S : Set (MeasureTheory.ProbabilityMeasure E)},
  MeasureTheory.IsTightMeasureSet {x | ∃ μ ∈ S, ↑μ = x} → IsCompact (closure S)
-- Init.Data.SInt.Lemmas
Int8.ne_iff_toBitVec_ne : ∀ {a b : Int8}, a ≠ b ↔ a.toBitVec ≠ b.toBitVec
-- Mathlib.Order.Interval.Finset.Basic
Finset.Icc_bot : ∀ {α : Type u_2} {a : α} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] [inst_2 : OrderBot α],
  Finset.Icc ⊥ a = Finset.Iic a
-- Mathlib.Analysis.Seminorm
Seminorm.coe_sSup_eq' : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  {s : Set (Seminorm 𝕜 E)}, BddAbove (DFunLike.coe '' s) → ⇑(sSup s) = ⨆ p, ⇑↑p
-- Init.Data.Range.Polymorphic.Lemmas
_private.Init.Data.Range.Polymorphic.Lemmas.0.Std.Rxc.Iterator.toList_eq_match.match_1.eq_1 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (h_1 : Unit → motive none) (h_2 : (a : α) → motive (some a)),
  (match none with
    | none => h_1 ()
    | some a => h_2 a) =
    h_1 ()
-- Init.Core
PSum.inr.sizeOf_spec : ∀ {α : Sort u} {β : Sort v} [inst : SizeOf α] [inst_1 : SizeOf β] (val : β), sizeOf (PSum.inr val) = 1 + sizeOf val
-- Mathlib.RingTheory.Unramified.Finite
/-- Proposition I.2.3 + I.2.6 of [iversen]
A finite-type `R`-algebra `S` is (formally) unramified iff there exists a `t : S ⊗[R] S` satisfying
1. `t` annihilates every `1 ⊗ s - s ⊗ 1`.
2. the image of `t` is `1` under the map `S ⊗[R] S → S`.
 -/
Algebra.FormallyUnramified.iff_exists_tensorProduct : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [Algebra.EssFiniteType R S],
  Algebra.FormallyUnramified R S ↔
    ∃ t, (∀ (s : S), (1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) * t = 0) ∧ (Algebra.TensorProduct.lmul' R) t = 1
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.any_eq_true_iff_exists_mem_getKey_getElem : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [LawfulHashable α]
  [EquivBEq α] {p : α → β → Bool}, m.WF → (m.any p = true ↔ ∃ a, ∃ (h : a ∈ m), p (m.getKey a h) m[a] = true)
-- Init.System.IO
/-- A child process that was spawned with configuration `cfg`.

The configuration determines whether the child process's standard input, standard output, and
standard error are `IO.FS.Handle`s or `Unit`.
 -/
IO.Process.Child : IO.Process.StdioConfig → Type
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.algHom_subsingleton : ∀ {R : Type u_1} [inst : CommRing R] {S : Type u_6} [inst_1 : CommRing S] [inst_2 : Algebra R S] {r : R},
  Subsingleton (AdjoinRoot (Polynomial.C r * Polynomial.X - 1) →ₐ[R] S)
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.instLinearOrder : LinearOrder ℝ*
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
/-- Fundamental theorem of calculus: if `f : ℝ → E` is integrable on `a..b` and `f x` is continuous
on the right or on the left at `a`, then the right (resp., left) derivative of
`u ↦ ∫ x in u..b, f x` at `a` equals `-f a`.  -/
intervalIntegral.derivWithin_integral_left : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E} {a b : ℝ},
  IntervalIntegrable f MeasureTheory.volume a b →
    ∀ {s t : Set ℝ} [intervalIntegral.FTCFilter a (nhdsWithin a s) (nhdsWithin a t)],
      StronglyMeasurableAtFilter f (nhdsWithin a t) MeasureTheory.volume →
        ContinuousWithinAt f t a →
          autoParam (UniqueDiffWithinAt ℝ s a) intervalIntegral.derivWithin_integral_left._auto_1 →
            derivWithin (fun u => ∫ (x : ℝ) in u..b, f x) s a = -f a
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.ByteArray.utf8DecodeChar?.isInvalidContinuationByte_eq_false_iff : ∀ {b : UInt8}, ByteArray.utf8DecodeChar?.isInvalidContinuationByte b = false ↔ b &&& 192 = 128
-- Std.Data.Iterators.Combinators.Monadic.Zip
Std.Iterators.Types.Zip.PlausibleStep.yieldRight : ∀ {m : Type w → Type w'} {α₁ β₁ : Type w} [inst : Std.Iterator α₁ m β₁] {α₂ β₂ : Type w} [inst_1 : Std.Iterator α₂ m β₂]
  {it : Std.IterM m (β₁ × β₂)} {out₁ : { out // ∃ it, it.IsPlausibleOutput out }},
  it.internalState.memoizedLeft = some out₁ →
    ∀ {it₂' : Std.IterM m β₂} {out₂ : β₂},
      it.internalState.right.IsPlausibleStep (Std.IterStep.yield it₂' out₂) →
        Std.Iterators.Types.Zip.PlausibleStep it
          (Std.IterStep.yield
            { internalState := { left := it.internalState.left, memoizedLeft := none, right := it₂' } } (↑out₁, out₂))
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.presieve₀_shrink : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreZeroHypercover S),
  E.shrink.presieve₀ = E.presieve₀
-- Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative
/-- If `f` maps `p ^ i` to `(f p) ^ i` for primes `p`, and `f`
is multiplicative on coprime elements, then `f` is multiplicative everywhere.  -/
UniqueFactorizationMonoid.multiplicative_of_coprime : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [UniqueFactorizationMonoid α] {β : Type u_3}
  [inst_2 : CommMonoidWithZero β] (f : α → β) (a b : α),
  f 0 = 0 →
    (∀ {x y : α}, IsUnit y → f (x * y) = f x * f y) →
      (∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i) →
        (∀ {x y : α}, IsRelPrime x y → f (x * y) = f x * f y) → f (a * b) = f a * f b
-- Mathlib.Algebra.Category.ModuleCat.Topology.Basic
/-- Cast a hom in `TopModuleCat` into a continuous linear map.  -/
TopModuleCat.Hom.hom : {R : Type u} →
  [inst : Ring R] →
    [inst_1 : TopologicalSpace R] → {X Y : TopModuleCat R} → X.Hom Y → ↑X.toModuleCat →L[R] ↑Y.toModuleCat
-- Mathlib.CategoryTheory.Preadditive.Biproducts
CategoryTheory.Limits.biproduct.lift_matrix_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {J : Type}
  [inst_2 : Fintype J] {K : Type} [inst_3 : Finite K] [inst_4 : CategoryTheory.Limits.HasFiniteBiproducts C] {f : J → C}
  {g : K → C} {P : C} (x : (j : J) → P ⟶ f j) (m : (j : J) → (k : K) → f j ⟶ g k) {Z : C} (h : ⨁ g ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.lift x)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.matrix m) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.biproduct.lift fun k => ∑ j, CategoryTheory.CategoryStruct.comp (x j) (m j k)) h
-- Mathlib.Tactic.Translate.UnfoldBoundary
_private.Mathlib.Tactic.Translate.UnfoldBoundary.0.Mathlib.Tactic.UnfoldBoundary.run.pre : Mathlib.Tactic.UnfoldBoundary.UnfoldBoundaries → Lean.Expr → Lean.Meta.SimpM Lean.Meta.Simp.Step
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.p₁_sigmaOfIsColimit : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreOneHypercover S)
  {c : CategoryTheory.Limits.Cofan E.X} (hc : CategoryTheory.Limits.IsColimit c) {d : CategoryTheory.Limits.Cofan E.Y'}
  (hd : CategoryTheory.Limits.IsColimit d) (i : E.I₁') {a b : PUnit.{w + 1}} (r : (E.sigmaOfIsColimit hc hd).I₁ a b),
  CategoryTheory.CategoryStruct.comp (d.inj i) ((E.sigmaOfIsColimit hc hd).p₁ r) =
    CategoryTheory.CategoryStruct.comp (E.p₁ i.snd) (c.inj i.fst.1)
-- Mathlib.Combinatorics.Matroid.Rank.ENat
Matroid.IsRkFinite.eRk_lt_top : ∀ {α : Type u_1} {M : Matroid α} {X : Set α}, M.IsRkFinite X → M.eRk X < ⊤
-- Init.Data.Array.Find
Array.getElem_zero_filter : ∀ {α : Type u_1} {p : α → Bool} {xs : Array α} (h : 0 < (Array.filter p xs).size),
  (Array.filter p xs)[0] = (Array.find? p xs).get ⋯