mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Set.Prod
Set.union_prod : ∀ {α : Type u_1} {β : Type u_2} {s₁ s₂ : Set α} {t : Set β}, (s₁ ∪ s₂) ×ˢ t = s₁ ×ˢ t ∪ s₂ ×ˢ t
-- Lean.Elab.Do.Switch
Lean.Elab.Term.expandTermReturn : Lean.Macro
-- Mathlib.Topology.Algebra.Support
/-- The topological support of a function is the closure of its support. i.e. the
closure of the set of all elements where the function is nonzero.  -/
tsupport : {X : Type u_1} → {α : Type u_2} → [Zero α] → [TopologicalSpace X] → (X → α) → Set X
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
/-- A version of `LinearIndependent.linearIndepOn_id` with the set range equality as a hypothesis.
 -/
LinearIndependent.linearIndepOn_id' : ∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M], LinearIndependent R v → ∀ {t : Set M}, Set.range v = t → LinearIndepOn R id t
-- Mathlib.CategoryTheory.Sites.Equivalence
CategoryTheory.GrothendieckTopology.instPreservesSheafification_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u₃}
  [inst_1 : CategoryTheory.Category.{v₃, u₃} A] (B : Type u₄) [inst_2 : CategoryTheory.Category.{v₄, u₄} B]
  (F : CategoryTheory.Functor A B) [inst_3 : CategoryTheory.EssentiallySmall.{w, v₁, u₁} C]
  [∀ (X : Cᵒᵖ),
      CategoryTheory.Limits.HasLimitsOfShape
        (CategoryTheory.StructuredArrow X (CategoryTheory.equivSmallModel C).inverse.op) A]
  [∀ (X : Cᵒᵖ),
      CategoryTheory.Limits.HasLimitsOfShape
        (CategoryTheory.StructuredArrow X (CategoryTheory.equivSmallModel C).inverse.op) B]
  [((CategoryTheory.equivSmallModel C).inverse.inducedTopology J).PreservesSheafification F],
  J.PreservesSheafification F
-- Mathlib.LinearAlgebra.UnitaryGroup
Matrix.instStarMulSubtypeMemSubmonoidSpecialUnitaryGroup : {n : Type u} →
  [inst : DecidableEq n] →
    [inst_1 : Fintype n] →
      {α : Type v} → [inst_2 : CommRing α] → [inst_3 : StarRing α] → StarMul ↥(Matrix.specialUnitaryGroup n α)
-- Mathlib.Topology.UniformSpace.Basic
uniformContinuous_inr : ∀ {α : Type ua} {β : Type ub} [inst : UniformSpace α] [inst_1 : UniformSpace β], UniformContinuous Sum.inr
-- Mathlib.Analysis.Complex.Exponential
Real.one_add_inv_pow_le_exp : ∀ {n : ℕ}, (1 + (↑n)⁻¹) ^ n ≤ Real.exp 1
-- Mathlib.LinearAlgebra.AffineSpace.Midpoint
right_vsub_midpoint : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : Invertible 2] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] (p₁ p₂ : P), p₂ -ᵥ midpoint R p₁ p₂ = ⅟2 • (p₂ -ᵥ p₁)
-- Mathlib.Tactic.NormNum.GCD
/-- Evaluates the `Rat.den` function.  -/
Mathlib.Meta.NormNum.evalRatDen : Mathlib.Meta.NormNum.NormNumExt
-- Mathlib.RingTheory.Regular.Flat
RingTheory.Sequence.IsRegular.of_faithfullyFlat : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [Module.FaithfullyFlat R S] {rs : List R},
  RingTheory.Sequence.IsRegular R rs → RingTheory.Sequence.IsRegular S (List.map (⇑(algebraMap R S)) rs)
-- Lean.Meta.Tactic.Grind.EMatchTheorem
_private.Lean.Meta.Tactic.Grind.EMatchTheorem.0.Lean.Meta.Grind.collect.go : Bool → Lean.Expr → Lean.Meta.Grind.CollectorM✝ Unit
-- Mathlib.Dynamics.Flow
/-- If `τ` is a `CanonicallyOrderedAdd` monoid (e.g., `ℕ` or `ℝ≥0`), then the notions
`IsForwardInvariant` and `IsInvariant` are equivalent.  -/
IsForwardInvariant.isInvariant : ∀ {τ : Type u_1} {α : Type u_2} [inst : AddMonoid τ] [inst_1 : PartialOrder τ] [CanonicallyOrderedAdd τ] {ϕ : τ → α → α}
  {s : Set α}, IsForwardInvariant ϕ s → IsInvariant ϕ s
-- Lean.Meta.Instances
Lean.Meta.DefaultInstanceEntry.mk.sizeOf_spec : ∀ (className instanceName : Lean.Name) (priority : ℕ),
  sizeOf { className := className, instanceName := instanceName, priority := priority } =
    1 + sizeOf className + sizeOf instanceName + sizeOf priority
-- Mathlib.Algebra.Order.Group.Synonym
Colex.instOne : {α : Type u_1} → [One α] → One (Colex α)
-- Lean.Meta.Tactic.Simp.Main
_private.Lean.Meta.Tactic.Simp.Main.0.Lean.Meta.Simp.simpLoop.visitPreContinue : Lean.Expr → Lean.Meta.Simp.Config → Lean.Meta.Simp.Result → Lean.Meta.SimpM Lean.Meta.Simp.Result
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- Negating the first vector passed to `oangle` adds `π` to the angle.  -/
Orientation.oangle_neg_left : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y : V}, x ≠ 0 → y ≠ 0 → o.oangle (-x) y = o.oangle x y + ↑Real.pi
-- Mathlib.Combinatorics.SetFamily.Shadow
Finset.insert_mem_upShadow : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {𝒜 : Finset (Finset α)} {s : Finset α} {a : α},
  s ∈ 𝒜 → a ∉ s → insert a s ∈ 𝒜.upShadow
-- Mathlib.CategoryTheory.Monoidal.Comon_
/-- The forgetful functor from `Comon C` to `C` is monoidal when `C` is monoidal.  -/
CategoryTheory.Comon.instMonoidalForget : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] → (CategoryTheory.Comon.forget C).Monoidal
-- Std.Time.Zoned.TimeZone
/-- The same timezone offset in seconds.
 -/
Std.Time.TimeZone.Offset.second : Std.Time.TimeZone.Offset → Std.Time.Second.Offset
-- Mathlib.LinearAlgebra.Matrix.Hermitian
/-- A diagonal matrix is Hermitian if the entries have the trivial `star` operation
(such as on the reals).  -/
Matrix.isHermitian_diagonal : ∀ {α : Type u_1} {n : Type u_4} [inst : AddMonoid α] [inst_1 : StarAddMonoid α] [TrivialStar α] [inst_3 : DecidableEq n]
  (v : n → α), (Matrix.diagonal v).IsHermitian
-- Mathlib.GroupTheory.OrderOfElement
/-- This is the same as `IsOfFinOrder.orderOf_pos` but with one fewer explicit assumption since this
is automatic in case of a finite cancellative monoid.  -/
orderOf_pos : ∀ {G : Type u_1} [inst : LeftCancelMonoid G] [Finite G] (x : G), 0 < orderOf x
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
/-- There exists a non-null vector with respect to any quadratic form `Q` whose associated
bilinear form is non-zero, i.e. there exists `x` such that `Q x ≠ 0`.  -/
QuadraticMap.exists_quadraticMap_ne_zero : ∀ {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] [inst_5 : Invertible 2] {Q : QuadraticMap R M N},
  QuadraticMap.associated' Q ≠ 0 → ∃ x, Q x ≠ 0
-- Mathlib.Algebra.Category.Ring.Basic
/-- The underlying ring hom.  -/
CommRingCat.Hom.hom' : {R S : CommRingCat} → R.Hom S → ↑R →+* ↑S
-- Mathlib.GroupTheory.GroupAction.Blocks
/-- If a block has too many translates, then it is a (sub)singleton  -/
AddAction.IsBlock.subsingleton_of_card_lt : ∀ {G : Type u_1} [inst : AddGroup G] {X : Type u_2} [inst_1 : AddAction G X] [AddAction.IsPretransitive G X] {B : Set X}
  [Finite X], AddAction.IsBlock G B → Nat.card X < 2 * (AddAction.orbit G B).ncard → B.Subsingleton
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey?_minKeyD : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp],
  t.isEmpty = false → ∀ {fallback : α}, t.getKey? (t.minKeyD fallback) = some (t.minKeyD fallback)
-- Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Complex.continuous_ofReal_cpow_const : ∀ {y : ℂ}, 0 < y.re → Continuous fun x => ↑x ^ y
-- Mathlib.Topology.ContinuousMap.Compact
ContinuousMap.isometryEquivBoundedOfCompact_apply : ∀ (α : Type u_1) (β : Type u_2) [inst : TopologicalSpace α] [inst_1 : CompactSpace α] [inst_2 : PseudoMetricSpace β],
  ⇑(ContinuousMap.isometryEquivBoundedOfCompact α β) = BoundedContinuousFunction.mkOfCompact
-- Mathlib.Algebra.Field.Basic
Lex.instSemifield : {K : Type u_1} → [Semifield K] → Semifield (Lex K)
-- Mathlib.GroupTheory.PushoutI
Monoid.PushoutI.NormalWord.mk.injEq : ∀ {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [inst : (i : ι) → Group (G i)] [inst_1 : Group H]
  {φ : (i : ι) → H →* G i} {d : Monoid.PushoutI.NormalWord.Transversal φ} (toWord : Monoid.CoprodI.Word G) (head : H)
  (normalized : ∀ (i : ι) (g : G i), ⟨i, g⟩ ∈ toWord.toList → g ∈ d.set i) (toWord_1 : Monoid.CoprodI.Word G)
  (head_1 : H) (normalized_1 : ∀ (i : ι) (g : G i), ⟨i, g⟩ ∈ toWord_1.toList → g ∈ d.set i),
  ({ toWord := toWord, head := head, normalized := normalized } =
      { toWord := toWord_1, head := head_1, normalized := normalized_1 }) =
    (toWord = toWord_1 ∧ head = head_1)
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.mkIso_inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {e f : C ≌ D} (η : e.functor ≅ f.functor),
  (CategoryTheory.Equivalence.mkIso η).inv = CategoryTheory.Equivalence.mkHom η.inv
-- Mathlib.Analysis.InnerProductSpace.Positive
ContinuousLinearMap.nonneg_iff_isPositive : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (f : E →L[𝕜] E), 0 ≤ f ↔ f.IsPositive
-- Init.Data.List.TakeDrop
List.dropWhile_beq_eq_self_of_head?_ne : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {a : α} {l : List α},
  l.head? ≠ some a → List.dropWhile (fun x => x == a) l = l
-- Mathlib.LinearAlgebra.SpecialLinearGroup
SpecialLinearGroup.center_eq_bot_of_finrank_le_one : ∀ {R : Type u_1} {V : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup V] [inst_2 : Module R V] [Module.Free R V]
  [Module.Finite R V], Module.finrank R V ≤ 1 → Subgroup.center (SpecialLinearGroup R V) = ⊥
-- Mathlib.LinearAlgebra.Dual.Basis
/-- linear combinations of elements of `e`.
This is a convenient abbreviation for `Finsupp.linearCombination R e l`  -/
Module.DualBases.lc : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommSemiring R] → [inst_1 : AddCommMonoid M] → [Module R M] → {ι : Type u_4} → (ι → M) → (ι →₀ R) → M
-- Mathlib.Data.Sum.Order
WithTop.orderIsoSumLexPUnit_symm_inr : ∀ {α : Type u_1} [inst : LE α] (x : PUnit.{u_4 + 1}), WithTop.orderIsoSumLexPUnit.symm (toLex (Sum.inr x)) = ⊤
-- Mathlib.Logic.Function.Basic
Function.instReflSwapProp : ∀ {α : Sort u_1} (r : α → α → Prop) [Std.Refl r], Std.Refl (Function.swap r)
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Cochain.comp_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G K : CochainComplex C ℤ} {n₁ n₂ n₁₂ : ℤ} (z₁ : CochainComplex.HomComplex.Cochain F G n₁) (h : n₁ + n₂ = n₁₂),
  z₁.comp 0 h = 0
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.ext_closure : ∀ {α : Type u_2} {M₁ M₂ : Matroid α}, (∀ (X : Set α), M₁.closure X = M₂.closure X) → M₁ = M₂
-- Mathlib.Algebra.Algebra.Spectrum.Basic
spectrum.units_smul_resolvent : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Ring A] [inst_2 : Algebra R A] {r : Rˣ} {s : R} {a : A},
  r • resolvent a s = resolvent (r⁻¹ • a) (r⁻¹ • s)
-- Lean.Meta.Basic
_private.Lean.Meta.Basic.0.Lean.Meta.mkLevelErrorMessageCore : String → Lean.Meta.PostponedEntry → Lean.MetaM Lean.MessageData
-- Init.Sym.Lemmas
Lean.Sym.Int.le_eq_true : ∀ (a b : ℤ), decide (a ≤ b) = true → (a ≤ b) = True
-- Init.Data.BitVec.Lemmas
BitVec.getLsbD_ofBoolListBE : ∀ {bs : List Bool} {i : ℕ},
  (BitVec.ofBoolListBE bs).getLsbD i = (decide (i < bs.length) && bs.getD (bs.length - 1 - i) false)
-- Mathlib.CategoryTheory.Monoidal.End
CategoryTheory.unitOfTensorIsoUnit_inv_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {M : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} M]
  [inst_2 : CategoryTheory.MonoidalCategory M] (F : CategoryTheory.Functor M (CategoryTheory.Functor C C)) (m n : M)
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj m n ≅ CategoryTheory.MonoidalCategoryStruct.tensorUnit M)
  [inst_3 : F.Monoidal] (X : C),
  (CategoryTheory.unitOfTensorIsoUnit F m n h).inv.app X =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.LaxMonoidal.ε F).app X)
      (CategoryTheory.CategoryStruct.comp ((F.map h.inv).app X) ((CategoryTheory.Functor.OplaxMonoidal.δ F m n).app X))
-- Mathlib.Algebra.Order.Module.Defs
neg_of_smul_neg_left : ∀ {α : Type u_1} {β : Type u_2} {a : α} {b : β} [inst : Zero α] [inst_1 : Zero β] [inst_2 : SMulZeroClass α β]
  [inst_3 : Preorder α] [inst_4 : Preorder β] [PosSMulReflectLT α β], a • b < 0 → 0 ≤ a → b < 0
-- Mathlib.AlgebraicGeometry.Scheme
/-- A variant of `mem_basicOpen` for bundled `x : U`.  -/
AlgebraicGeometry.Scheme.mem_basicOpen' : ∀ (X : AlgebraicGeometry.Scheme) {U : X.Opens} (f : ↑(X.presheaf.obj (Opposite.op U))) (x : ↥U),
  ↑x ∈ X.basicOpen f ↔ IsUnit ((CategoryTheory.ConcreteCategory.hom (X.presheaf.germ U ↑x ⋯)) f)
-- Init.Data.Iterators.Producers.Monadic.List
Std.Iterators.Types.ListIterator.instIteratorLoop : {m : Type w → Type w'} →
  {α : Type w} →
    [inst : Monad m] → {n : Type x → Type x'} → [Monad n] → Std.IteratorLoop (Std.Iterators.Types.ListIterator α) m n
-- Mathlib.RingTheory.Smooth.Basic
Algebra.FormallySmooth.instTensorProduct : ∀ {R : Type u_4} [inst : CommRing R] {A : Type u_5} [inst_1 : CommRing A] [inst_2 : Algebra R A] (B : Type u_6)
  [inst_3 : CommRing B] [inst_4 : Algebra R B] [Algebra.FormallySmooth R A],
  Algebra.FormallySmooth B (TensorProduct R B A)
-- Mathlib.Data.NNReal.Defs
/-- Every real number is either zero, positive or negative, phrased using `ℝ≥0`.  -/
Real.nnreal_trichotomy : ∀ (r : ℝ), r = 0 ∨ ∃ x, 0 < x ∧ (r = ↑x ∨ r = -↑x)
-- Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
SSet.Subcomplex.range_eq_top : ∀ {X Y : SSet} (f : X ⟶ Y) [CategoryTheory.Epi f], SSet.Subcomplex.range f = ⊤
-- Mathlib.Algebra.Homology.HomotopyCofiber
/-- The composition `φ ≫ mappingCone.inr φ` is homotopic to `0`.  -/
HomologicalComplex.homotopyCofiber.inrCompHomotopy : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {ι : Type u_2} →
        {c : ComplexShape ι} →
          {F G : HomologicalComplex C c} →
            (φ : F ⟶ G) →
              [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] →
                [inst_3 : DecidableRel c.Rel] →
                  (∀ (j : ι), ∃ i, c.Rel i j) →
                    Homotopy (CategoryTheory.CategoryStruct.comp φ (HomologicalComplex.homotopyCofiber.inr φ)) 0
-- Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
cyclotomicCharacter.spec : ∀ {L : Type u} [inst : CommRing L] [inst_1 : IsDomain L] (p : ℕ) [inst_2 : Fact (Nat.Prime p)] {n : ℕ}
  [∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)] (g : L ≃+* L) (t : L),
  t ^ p ^ n = 1 → g t = t ^ ((PadicInt.toZModPow n) ↑((cyclotomicCharacter L p) g)).val
-- Mathlib.Analysis.CStarAlgebra.Basic
/-- The `star` map in a normed star group is a normed group homomorphism.  -/
starNormedAddGroupHom : {E : Type u_2} →
  [inst : SeminormedAddCommGroup E] → [inst_1 : StarAddMonoid E] → [NormedStarGroup E] → NormedAddGroupHom E E
-- Init.Control.Lawful.MonadLift.Lemmas
liftM_seq : ∀ {m : Type u → Type v} {n : Type u → Type w} [inst : Monad m] [inst_1 : Monad n] [inst_2 : MonadLiftT m n]
  [LawfulMonadLiftT m n] {α β : Type u} [LawfulMonad m] [LawfulMonad n] (mf : m (α → β)) (ma : m α),
  liftM (mf <*> ma) = liftM mf <*> liftM ma
-- Mathlib.Analysis.Normed.Lp.WithLp
WithLp.instAddAction : (p : ENNReal) → (K : Type u_1) → (V : Type u_4) → [inst : AddMonoid K] → [AddAction K V] → AddAction K (WithLp p V)
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometry.mk.inj : ∀ {R : Type u_1} {R₂ : Type u_2} {inst : Semiring R} {inst_1 : Semiring R₂} {σ₁₂ : R →+* R₂} {E : Type u_11}
  {E₂ : Type u_12} {inst_2 : SeminormedAddCommGroup E} {inst_3 : SeminormedAddCommGroup E₂} {inst_4 : Module R E}
  {inst_5 : Module R₂ E₂} {toLinearMap : E →ₛₗ[σ₁₂] E₂} {norm_map' : ∀ (x : E), ‖toLinearMap x‖ = ‖x‖}
  {toLinearMap_1 : E →ₛₗ[σ₁₂] E₂} {norm_map'_1 : ∀ (x : E), ‖toLinearMap_1 x‖ = ‖x‖},
  { toLinearMap := toLinearMap, norm_map' := norm_map' } = { toLinearMap := toLinearMap_1, norm_map' := norm_map'_1 } →
    toLinearMap = toLinearMap_1
-- Mathlib.Data.Set.Prod
Set.mk_preimage_prod_left_eq_if : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {b : β} [inst : DecidablePred fun x => x ∈ t],
  (fun a => (a, b)) ⁻¹' s ×ˢ t = if b ∈ t then s else ∅
-- Mathlib.Topology.Algebra.Group.Pointwise
subset_interior_sub : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [IsTopologicalAddGroup G] {s t : Set G},
  interior s - interior t ⊆ interior (s - t)
-- Init.Data.String.Decode
ByteArray.utf8DecodeChar?_utf8EncodeChar_append : ∀ {b : ByteArray} {c : Char}, ((String.utf8EncodeChar c).toByteArray ++ b).utf8DecodeChar? 0 = some c
-- Mathlib.RingTheory.Smooth.NoetherianDescent
/-- Let `A` be an `R`-algebra. If `B` is a smooth `A`-algebra, there exists an
`R`-algebra of finite type `A₀` and a smooth `A₀`-algebra `B₀` such that `B ≃ₐ A ⊗[A₀] B₀`
with `A₀ → A` injective.
See `Algebra.Smooth.exists_subalgebra_fg` for a version in terms of `Subalgebra`.
 -/
Algebra.Smooth.exists_finiteType : ∀ (R : Type u_1) [inst : CommRing R] (A : Type u) (B : Type u_2) [inst_1 : CommRing A] [Algebra R A]
  [inst_3 : CommRing B] [inst_4 : Algebra A B] [Algebra.Smooth A B],
  ∃ A₀ B₀ x x_1 x_2 x_3 x_4,
    Function.Injective ⇑(algebraMap A₀ A) ∧
      Algebra.FiniteType R A₀ ∧ Algebra.Smooth A₀ B₀ ∧ Nonempty (B ≃ₐ[A] TensorProduct A₀ A B₀)
-- Std.Http.Server.Connection
/-- Events produced by the async select loop in `receiveWithTimeout`.
Each variant corresponds to one possible outcome of waiting for I/O.
 -/
_private.Std.Http.Server.Connection.0.Std.Http.Server.Connection.Recv : Type → Type
-- Mathlib.RingTheory.DividedPowers.SubDPIdeal
DividedPowers.SubDPIdeal.inf_carrier_def : ∀ {A : Type u_1} [inst : CommSemiring A] {I : Ideal A} {hI : DividedPowers I} (J J' : hI.SubDPIdeal),
  (J ⊓ J').carrier = J.carrier ⊓ J'.carrier
-- Mathlib.Data.Sym.Sym2
Sym2.pmap_map : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {P : α → Prop} {Q : β → Prop} (f : (a : α) → P a → β) (g : β → γ)
  (z : Sym2 α) (h : ∀ a ∈ z, P a),
  (∀ b ∈ Sym2.pmap f z h, Q b) → Sym2.map g (Sym2.pmap f z h) = Sym2.pmap (fun a ha => g (f a ⋯)) z ⋯
-- Mathlib.Probability.Distributions.Beta
ProbabilityTheory.betaPDF_eq_zero_of_nonpos : ∀ {α β x : ℝ}, x ≤ 0 → ProbabilityTheory.betaPDF α β x = 0
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictPseudofunctor
CategoryTheory.StrictPseudofunctorPreCore.mk : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        (toPrelaxFunctor : CategoryTheory.PrelaxFunctor B C) →
          autoParam
              (∀ (X : B),
                toPrelaxFunctor.map (CategoryTheory.CategoryStruct.id X) =
                  CategoryTheory.CategoryStruct.id (toPrelaxFunctor.obj X))
              CategoryTheory.StrictPseudofunctorPreCore.map_id._autoParam →
            (map_comp :
                autoParam
                  (∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c),
                    toPrelaxFunctor.map (CategoryTheory.CategoryStruct.comp f g) =
                      CategoryTheory.CategoryStruct.comp (toPrelaxFunctor.map f) (toPrelaxFunctor.map g))
                  CategoryTheory.StrictPseudofunctorPreCore.map_comp._autoParam) →
              autoParam
                  (∀ {a b c : B} (f : a ⟶ b) {g g' : b ⟶ c} (η : g ⟶ g'),
                    toPrelaxFunctor.map₂ (CategoryTheory.Bicategory.whiskerLeft f η) =
                      CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
                        (CategoryTheory.CategoryStruct.comp
                          (CategoryTheory.Bicategory.whiskerLeft (toPrelaxFunctor.map f) (toPrelaxFunctor.map₂ η))
                          (CategoryTheory.eqToHom ⋯)))
                  CategoryTheory.StrictPseudofunctorPreCore.map₂_whisker_left._autoParam →
                autoParam
                    (∀ {a b c : B} {f f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c),
                      toPrelaxFunctor.map₂ (CategoryTheory.Bicategory.whiskerRight η g) =
                        CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
                          (CategoryTheory.CategoryStruct.comp
                            (CategoryTheory.Bicategory.whiskerRight (toPrelaxFunctor.map₂ η) (toPrelaxFunctor.map g))
                            (CategoryTheory.eqToHom ⋯)))
                    CategoryTheory.StrictPseudofunctorPreCore.map₂_whisker_right._autoParam →
                  CategoryTheory.StrictPseudofunctorPreCore B C
-- Mathlib.Algebra.Opposites
MulOpposite.instInvolutiveInv.eq_1 : ∀ {α : Type u_1} [inst : InvolutiveInv α],
  MulOpposite.instInvolutiveInv = { toInv := MulOpposite.instInv, inv_inv := ⋯ }
-- Mathlib.RingTheory.SimpleModule.Basic
/-- A module is simple when it has only two submodules, `⊥` and `⊤`.  -/
IsSimpleModule : (R : Type u_2) → [inst : Ring R] → (M : Type u_4) → [inst_1 : AddCommGroup M] → [Module R M] → Prop
-- Lean.Data.Lsp.Extra
Lean.Lsp.WaitForDiagnosticsParams.mk.sizeOf_spec : ∀ (uri : Lean.Lsp.DocumentUri) (version : ℕ),
  sizeOf { uri := uri, version := version } = 1 + sizeOf uri + sizeOf version
-- Mathlib.CategoryTheory.Endomorphism
/-- `mulEquivAut` as an isomorphism between automorphism groups.  -/
CategoryTheory.Functor.FullyFaithful.autMulEquivOfFullyFaithful : {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.FullyFaithful → (X : C) → CategoryTheory.Aut X ≃* CategoryTheory.Aut (f.obj X)
-- Mathlib.CategoryTheory.Idempotents.HomologicalComplex
CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_counitIso_hom : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] (α : Type u_3)
  [inst_2 : AddRightCancelSemigroup α] [inst_3 : One α],
  (CategoryTheory.Idempotents.karoubiCochainComplexEquivalence C α).counitIso.hom = CategoryTheory.eqToHom ⋯
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
/-- The obvious homotopy between a morphism of short complexes and itself.  -/
CategoryTheory.ShortComplex.Homotopy.refl : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} → (φ : S₁ ⟶ S₂) → CategoryTheory.ShortComplex.Homotopy φ φ
-- Mathlib.Topology.Maps.Basic
IsOpenMap.clusterPt_comap_iff : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  IsOpenMap f → Continuous f → ∀ {x : X} {l : Filter Y}, ClusterPt x (Filter.comap f l) ↔ ClusterPt (f x) l
-- Mathlib.Tactic.NormNum.Irrational
/-- Weaker version of `not_power_rat_of_num` with extra `q ≥ 0` assumption.  -/
_private.Mathlib.Tactic.NormNum.Irrational.0.Mathlib.Meta.NormNum.not_power_rat_of_num_aux : ∀ {a b d : ℕ}, a.Coprime b → (∀ (x : ℕ), a ≠ x ^ d) → ∀ {q : ℚ}, 0 ≤ q → ↑a / ↑b ≠ q ^ d
-- Mathlib.Data.Seq.Defs
_private.Mathlib.Data.Seq.Defs.0.Stream'.Seq.omap.match_1.splitter : {α : Type u_2} →
  {β : Type u_1} →
    (motive : Option (α × β) → Sort u_3) →
      (x : Option (α × β)) → (Unit → motive none) → ((a : α) → (b : β) → motive (some (a, b))) → motive x