mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Probability.UniformOn
/-- A version of the law of total probability for counting probabilities.  -/
ProbabilityTheory.uniformOn_add_compl_eq : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [MeasurableSingletonClass Ω] {s : Set Ω} (u t : Set Ω),
  s.Finite →
    (ProbabilityTheory.uniformOn (s ∩ u)) t * (ProbabilityTheory.uniformOn s) u +
        (ProbabilityTheory.uniformOn (s ∩ uᶜ)) t * (ProbabilityTheory.uniformOn s) uᶜ =
      (ProbabilityTheory.uniformOn s) t
-- Mathlib.Data.EReal.Inv
EReal.coe_coe_sign : ∀ (x : SignType), ↑↑x = ↑x
-- Mathlib.Analysis.InnerProductSpace.l2Space
OrthogonalFamily.linearIsometry_apply_dfinsupp_sum_single : ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : RCLike 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] {G : ι → Type u_4} [inst_3 : (i : ι) → NormedAddCommGroup (G i)]
  [inst_4 : (i : ι) → InnerProductSpace 𝕜 (G i)] [inst_5 : CompleteSpace E] {V : (i : ι) → G i →ₗᵢ[𝕜] E}
  (hV : OrthogonalFamily 𝕜 G V) [inst_6 : DecidableEq ι] [inst_7 : (i : ι) → DecidableEq (G i)] (W₀ : Π₀ (i : ι), G i),
  hV.linearIsometry (W₀.sum (lp.single 2)) = W₀.sum fun i => ⇑(V i)
-- Std.Tactic.BVDecide.Normalize.BitVec
Std.Tactic.BVDecide.Normalize.BitVec.shiftLeft_neg : ∀ {w₁ w₂ : ℕ} {x : BitVec w₁} {y : BitVec w₂}, (~~~x + 1#w₁) <<< y = ~~~(x <<< y) + 1
-- Mathlib.Combinatorics.Additive.PluenneckeRuzsa
_private.Mathlib.Combinatorics.Additive.PluenneckeRuzsa.0.Finset.card_add_nsmul_le : ∀ {G : Type u_1} [inst : DecidableEq G] [inst_1 : AddCommGroup G] {A B : Finset G},
  (∀ A' ⊆ A, (A + B).card * A'.card ≤ (A' + B).card * A.card) →
    ∀ (n : ℕ), ↑(A + n • B).card ≤ (↑(A + B).card / ↑A.card) ^ n * ↑A.card
-- Batteries.Data.Fin.Coding
/-- Decode `Fin m × Fin n` from `Fin (m * n)`.  -/
Fin.decodeProd : {m n : ℕ} → Fin (m * n) → Fin m × Fin n
-- Mathlib.Order.Defs.Unbundled
Std.Refl.decide : ∀ {α : Sort u_1} {r : α → α → Prop} [inst : DecidableRel r] [Std.Refl r], Std.Refl fun a b => decide (r a b) = true
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.instHashableBVBinOp.hash : Std.Tactic.BVDecide.BVBinOp → UInt64
-- Mathlib.MeasureTheory.Measure.GiryMonad
MeasureTheory.Measure.bind_zero_right : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (m : MeasureTheory.Measure α),
  m.bind 0 = 0
-- Mathlib.CategoryTheory.DifferentialObject
/-- The differential `d` satisfies that `d² = 0`.  -/
CategoryTheory.DifferentialObject.d_squared_assoc : ∀ {S : Type u_1} [inst : AddMonoidWithOne S] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.HasShift C S]
  (self : CategoryTheory.DifferentialObject S C) {Z : C}
  (h : (CategoryTheory.shiftFunctor C 1).obj ((CategoryTheory.shiftFunctor C 1).obj self.obj) ⟶ Z),
  CategoryTheory.CategoryStruct.comp self.d
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C 1).map self.d) h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.RingTheory.PowerBasis
/-- `pb : PowerBasis R S` states that `1, pb.gen, ..., pb.gen ^ (pb.dim - 1)`
is a basis for the `R`-algebra `S` (viewed as `R`-module).

This is a structure, not a class, since the same algebra can have many power bases.
For the common case where `S` is defined by adjoining an integral element to `R`,
the canonical power basis is given by `{Algebra,IntermediateField}.adjoin.powerBasis`.
 -/
PowerBasis : (R : Type u_7) → (S : Type u_8) → [inst : CommRing R] → [inst_1 : Ring S] → [Algebra R S] → Type (max u_7 u_8)
-- Lean.PrettyPrinter.Delaborator.Options
Lean.pp.maxSteps : Lean.Option ℕ
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKey?_eq_some_getKeyD_of_contains : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {a fallback : α}, m.contains a = true → m.getKey? a = some (m.getKeyD a fallback)
-- Mathlib.Algebra.Star.StarAlgHom
/-- The composition of non-unital ⋆-algebra homomorphisms, as a non-unital ⋆-algebra
homomorphism.  -/
NonUnitalStarAlgHom.comp : {R : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      {C : Type u_4} →
        [inst : Monoid R] →
          [inst_1 : NonUnitalNonAssocSemiring A] →
            [inst_2 : DistribMulAction R A] →
              [inst_3 : Star A] →
                [inst_4 : NonUnitalNonAssocSemiring B] →
                  [inst_5 : DistribMulAction R B] →
                    [inst_6 : Star B] →
                      [inst_7 : NonUnitalNonAssocSemiring C] →
                        [inst_8 : DistribMulAction R C] →
                          [inst_9 : Star C] → (B →⋆ₙₐ[R] C) → (A →⋆ₙₐ[R] B) → A →⋆ₙₐ[R] C
-- Std.Data.ExtDHashMap.Basic
/-- Checks if a mapping for the given key exists and returns the key if it does, otherwise `none`.
The result in the `some` case is guaranteed to be pointer equal to the key in the map.
 -/
Std.ExtDHashMap.getKey? : {α : Type u} →
  {β : α → Type v} →
    {x : BEq α} → {x_1 : Hashable α} → [EquivBEq α] → [LawfulHashable α] → Std.ExtDHashMap α β → α → Option α
-- Mathlib.CategoryTheory.Iso
CategoryTheory.Functor.mapIso_trans : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {X Y Z : C} (i : X ≅ Y) (j : Y ≅ Z), F.mapIso (i ≪≫ j) = F.mapIso i ≪≫ F.mapIso j
-- Mathlib.CategoryTheory.Limits.Types.Filtered
CategoryTheory.Limits.Types.FilteredColimit.rel_of_colimitTypeRel : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J (Type u))
  (x y : (j : J) × F.obj j), F.ColimitTypeRel x y → CategoryTheory.Limits.Types.FilteredColimit.Rel F x y
-- Mathlib.Topology.Constructible
Topology.IsLocallyConstructible.iUnion : ∀ {ι : Sort u_1} {X : Type u_2} [inst : TopologicalSpace X] [Finite ι] {f : ι → Set X},
  (∀ (i : ι), Topology.IsLocallyConstructible (f i)) → Topology.IsLocallyConstructible (⋃ i, f i)
-- Mathlib.GroupTheory.Coset.Basic
/-- An equivalence between any two non-empty fibers of a `MonoidHom`.  -/
MonoidHom.fiberEquiv : {α : Type u_1} →
  [inst : Group α] → {H : Type u_2} → [inst_1 : Group H] → (f : α →* H) → (a b : α) → ↑(⇑f ⁻¹' {f a}) ≃ ↑(⇑f ⁻¹' {f b})
-- Mathlib.NumberTheory.SelbergSieve
BoundingSieve.multSum.eq_1 : ∀ {s : BoundingSieve} (d : ℕ), BoundingSieve.multSum d = ∑ n ∈ s.support, if d ∣ n then s.weights n else 0
-- Init.Data.String.Lemmas.Splits
String.splits_next_startPos : ∀ {s : String} {h : s.startPos ≠ s.endPos},
  (s.startPos.next h).Splits (String.singleton (s.startPos.get h)) (s.sliceFrom (s.startPos.next h)).copy
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.values_eq_map_snd : ∀ {α : Type u} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β},
  t.values = List.map (fun x => x.snd) t.toListModel
-- Mathlib.GroupTheory.Sylow
Sylow.coe_comapOfKerIsPGroup : ∀ {p : ℕ} {G : Type u_1} [inst : Group G] (P : Sylow p G) {K : Type u_2} [inst_1 : Group K] (ϕ : K →* G)
  (hϕ : IsPGroup p ↥ϕ.ker) (h : ↑P ≤ ϕ.range), ↑(P.comapOfKerIsPGroup ϕ hϕ h) = Subgroup.comap ϕ ↑P
-- Mathlib.Algebra.Order.Rearrangement
/-- **Strict inequality case of the Rearrangement Inequality**: Pointwise multiplication of
`f` and `g`, which antivary together on `s`, is strictly decreased by a permutation if and only if
`f` and `g ∘ σ` do not antivary together on `s`. Stated by permuting the entries of `g`.  -/
AntivaryOn.sum_mul_lt_sum_mul_comp_perm_iff : ∀ {ι : Type u_1} {α : Type u_2} [inst : Semiring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α]
  {s : Finset ι} {σ : Equiv.Perm ι} {f g : ι → α},
  AntivaryOn f g ↑s → {x | σ x ≠ x} ⊆ ↑s → (∑ i ∈ s, f i * g i < ∑ i ∈ s, f i * g (σ i) ↔ ¬AntivaryOn f (g ∘ ⇑σ) ↑s)
-- Mathlib.Geometry.Manifold.ContMDiff.NormedSpace
ContMDiffWithinAt.clm_prodMap : ∀ {𝕜 : 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] {F₁ : Type u_8} [inst_6 : NormedAddCommGroup F₁]
  [inst_7 : NormedSpace 𝕜 F₁] {F₂ : Type u_9} [inst_8 : NormedAddCommGroup F₂] [inst_9 : NormedSpace 𝕜 F₂]
  {F₃ : Type u_10} [inst_10 : NormedAddCommGroup F₃] [inst_11 : NormedSpace 𝕜 F₃] {F₄ : Type u_11}
  [inst_12 : NormedAddCommGroup F₄] [inst_13 : NormedSpace 𝕜 F₄] {n : WithTop ℕ∞} {g : M → F₁ →L[𝕜] F₃}
  {f : M → F₂ →L[𝕜] F₄} {s : Set M} {x : M},
  ContMDiffWithinAt I (modelWithCornersSelf 𝕜 (F₁ →L[𝕜] F₃)) n g s x →
    ContMDiffWithinAt I (modelWithCornersSelf 𝕜 (F₂ →L[𝕜] F₄)) n f s x →
      ContMDiffWithinAt I (modelWithCornersSelf 𝕜 (F₁ × F₂ →L[𝕜] F₃ × F₄)) n (fun x => (g x).prodMap (f x)) s x
-- Mathlib.CategoryTheory.Sites.Hypercover.One
/-- The multifork associated to a pre-`1`-hypercover is limiting if and only if
the fork induced by taking the coproduct of the components is limiting.  -/
CategoryTheory.PreOneHypercover.isLimitMultiforkEquivIsLimitFork : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A : Type u_1} →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} A] →
        {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) →
                    (F : CategoryTheory.Functor Cᵒᵖ A) →
                      [CategoryTheory.Limits.PreservesLimit
                            (CategoryTheory.Discrete.functor fun i => Opposite.op (E.X i)) F] →
                        [CategoryTheory.Limits.PreservesLimit
                              (CategoryTheory.Discrete.functor fun i => Opposite.op (E.Y' i)) F] →
                          CategoryTheory.Limits.IsLimit (E.multifork F) ≃
                            CategoryTheory.Limits.IsLimit (E.forkOfIsColimit hc hd F)
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
/-- An alias of `ContinuousMultilinearMap.normedSpace` with non-dependent types to help typeclass
search.  -/
ContinuousMultilinearMap.normedSpace' : {𝕜 : Type u} →
  {ι : Type v} →
    {G : Type wG} →
      {G' : Type wG'} →
        [inst : NontriviallyNormedField 𝕜] →
          [inst_1 : SeminormedAddCommGroup G] →
            [inst_2 : NormedSpace 𝕜 G] →
              [inst_3 : SeminormedAddCommGroup G'] →
                [inst_4 : NormedSpace 𝕜 G'] →
                  [inst_5 : Fintype ι] →
                    {𝕜' : Type u_2} →
                      [inst_6 : NormedField 𝕜'] →
                        [inst_7 : NormedSpace 𝕜' G] →
                          [SMulCommClass 𝕜 𝕜' G] → NormedSpace 𝕜' (ContinuousMultilinearMap 𝕜 (fun x => G') G)
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.diff_eq : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashSet.Raw α}, m₁.diff m₂ = m₁ \ m₂
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank
SSet.Subcomplex.Pairing.RankFunction.lt : ∀ {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {α : Type v} [inst : PartialOrder α] (self : P.RankFunction α)
  {x y : ↑P.II}, P.AncestralRel x y → self.rank x < self.rank y
-- Mathlib.Topology.MetricSpace.Similarity
/-- Similarity holds if and only if all non-negative distances between points with different
indices are proportional.  -/
similar_iff_exists_pairwise_nndist_eq : ∀ {ι : Type u_1} {P₁ : Type u_3} {P₂ : Type u_4} {v₁ : ι → P₁} {v₂ : ι → P₂} [inst : PseudoMetricSpace P₁]
  [inst_1 : PseudoMetricSpace P₂],
  Similar v₁ v₂ ↔ ∃ r, r ≠ 0 ∧ Pairwise fun i₁ i₂ => nndist (v₁ i₁) (v₁ i₂) = r * nndist (v₂ i₁) (v₂ i₂)
-- Mathlib.Data.DFinsupp.BigOperators
DFinsupp.sum_neg_index : ∀ {ι : Type u} {γ : Type w} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → AddGroup (β i)]
  [inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] [inst_3 : AddCommMonoid γ] {g : Π₀ (i : ι), β i}
  {h : (i : ι) → β i → γ}, (∀ (i : ι), h i 0 = 0) → (-g).sum h = g.sum fun i b => h i (-b)
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
/-- The integral representation of the function `x ↦ x ^ p` (where `p ∈ (0, 1)`) .  -/
Real.exists_measure_rpow_eq_integral_rpowIntegrand₀₁ : ∀ {p : ℝ},
  p ∈ Set.Ioo 0 1 →
    ∃ μ,
      ∀ x ∈ Set.Ici 0,
        MeasureTheory.IntegrableOn (fun t => p.rpowIntegrand₀₁ t x) (Set.Ioi 0) μ ∧
          x ^ p = ∫ (t : ℝ) in Set.Ioi 0, p.rpowIntegrand₀₁ t x ∂μ
-- Mathlib.Data.Fintype.Card
Fintype.two_lt_card_iff : ∀ {α : Type u_1} [inst : Fintype α], 2 < Fintype.card α ↔ ∃ a b c, a ≠ b ∧ a ≠ c ∧ b ≠ c
-- Mathlib.Topology.Compactification.StoneCech
denseRange_preStoneCechUnit : ∀ {α : Type u} [inst : TopologicalSpace α], DenseRange preStoneCechUnit
-- Mathlib.Topology.ContinuousMap.CocompactMap
/-- If the codomain is Hausdorff, preimages of compact sets are compact under a cocompact
continuous map.  -/
CocompactMap.isCompact_preimage : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [T2Space β]
  (f : CocompactMap α β) ⦃s : Set β⦄, IsCompact s → IsCompact (⇑f ⁻¹' s)
-- Mathlib.CategoryTheory.Limits.IsLimit
/-- The map `desc` makes the diagram with the natural transformations commute  -/
CategoryTheory.Limits.IsColimit.fac : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {t : CategoryTheory.Limits.Cocone F} (self : CategoryTheory.Limits.IsColimit t)
  (s : CategoryTheory.Limits.Cocone F) (j : J), CategoryTheory.CategoryStruct.comp (t.ι.app j) (self.desc s) = s.ι.app j
-- Lean.Meta.Instances
Lean.Meta.DefaultInstances.defaultInstances : Lean.Meta.DefaultInstances → Lean.NameMap (List (Lean.Name × ℕ))
-- Init.Data.UInt.Lemmas
USize.toUInt64_ofNatLT : ∀ {n : ℕ} (h : n < USize.size), (USize.ofNatLT n h).toUInt64 = UInt64.ofNatLT n ⋯
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.InjectiveTheorem.mk.sizeOf_spec : ∀ (levelParams : Array Lean.Name) (proof : Lean.Expr) (symbols : List Lean.HeadIndex) (origin : Lean.Meta.Grind.Origin),
  sizeOf { levelParams := levelParams, proof := proof, symbols := symbols, origin := origin } =
    1 + sizeOf levelParams + sizeOf proof + sizeOf symbols + sizeOf origin
-- Mathlib.Analysis.CStarAlgebra.ApproximateUnit
/-- The sections of positive strict contractions form a filter basis.  -/
CStarAlgebra.isBasis_nonneg_sections : ∀ (A : Type u_1) [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] [StarOrderedRing A],
  Filter.IsBasis (fun x => 0 ≤ x ∧ ‖x‖ < 1) fun x => {x_1 | x ≤ x_1}
-- Init.Data.Vector.Lemmas
Vector.foldr_map_hom : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} {g : α → β} {f : α → α → α} {f' : β → β → β} {a : α} {xs : Vector α n},
  (∀ (x y : α), f' (g x) (g y) = g (f x y)) → Vector.foldr f' (g a) (Vector.map g xs) = g (Vector.foldr f a xs)
-- Std.Time.Internal.UnitVal
Std.Time.Internal.UnitVal.ofInt.inj : ∀ {α : ℚ} {val val_1 : ℤ}, { val := val } = { val := val_1 } → val = val_1
-- Mathlib.Probability.Independence.ZeroOne
ProbabilityTheory.indep_iSup_limsup : ∀ {Ω : Type u_2} {ι : Type u_3} {s : ι → MeasurableSpace Ω} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω}
  {β : Type u_4} {p : Set ι → Prop} {f : Filter ι} {ns : β → Set ι},
  (∀ (n : ι), s n ≤ m0) →
    ProbabilityTheory.iIndep s μ →
      (∀ (t : Set ι), p t → tᶜ ∈ f) →
        Directed (fun x1 x2 => x1 ⊆ x2) ns →
          (∀ (a : β), p (ns a)) → (∀ (n : ι), ∃ a, n ∈ ns a) → ProbabilityTheory.Indep (⨆ n, s n) (Filter.limsup s f) μ
-- Mathlib.Analysis.MeanInequalities
/-- **Minkowski inequality**: the `L_p` seminorm of the sum of two vectors is less than or equal
to the sum of the `L_p`-seminorms of the summands. A version for `Real`-valued functions.  -/
Real.Lp_add_le : ∀ {ι : Type u} (s : Finset ι) (f g : ι → ℝ) {p : ℝ},
  1 ≤ p → (∑ i ∈ s, |f i + g i| ^ p) ^ (1 / p) ≤ (∑ i ∈ s, |f i| ^ p) ^ (1 / p) + (∑ i ∈ s, |g i| ^ p) ^ (1 / p)
-- Mathlib.Data.Matrix.Diagonal
Matrix.map_one : ∀ {n : Type u_3} {α : Type v} {β : Type w} [inst : DecidableEq n] [inst_1 : Zero α] [inst_2 : One α] [inst_3 : Zero β]
  [inst_4 : One β] (f : α → β), f 0 = 0 → f 1 = 1 → Matrix.map 1 f = 1
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.Sigma.constCompSigmaIsoConst_inv_app : ∀ {α : Type w₂} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasCoproductsOfShape α C] {I : α → Type u_1}
  [inst_2 : (i : α) → CategoryTheory.Category.{v_1, u_1} (I i)] (X : α → C) (X_1 : (i : α) → I i),
  (CategoryTheory.Limits.Sigma.constCompSigmaIsoConst X).inv.app X_1 = CategoryTheory.CategoryStruct.id (∐ fun i => X i)
-- Mathlib.AlgebraicGeometry.Stalk
AlgebraicGeometry.Scheme.instIsOverFromSpecStalkOfMem : ∀ {X : AlgebraicGeometry.Scheme} (U : X.Opens) (x : ↥X) (hxU : x ∈ U),
  AlgebraicGeometry.Scheme.Hom.IsOver (U.fromSpecStalkOfMem x hxU) X
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.inter_vadd_subset : ∀ {α : Type u_2} {β : Type u_3} [inst : VAdd α β] {s₁ s₂ : Set α} {t : Set β}, s₁ ∩ s₂ +ᵥ t ⊆ (s₁ +ᵥ t) ∩ (s₂ +ᵥ t)
-- Lean.Meta.Tactic.Grind.Arith.CommRing.RingId
_private.Lean.Meta.Tactic.Grind.Arith.CommRing.RingId.0.Lean.Meta.Grind.Arith.CommRing.getCommRingId?.go? : Lean.Expr → Lean.Meta.Grind.GoalM (Option ℕ)
-- Mathlib.GroupTheory.Submonoid.Inverses
AddSubmonoid.fromLeftNeg_zero : ∀ {M : Type u_1} [inst : AddMonoid M] (S : AddSubmonoid M), S.fromLeftNeg 0 = 0
-- Mathlib.Analysis.InnerProductSpace.StarOrder
ContinuousLinearMap.instStarOrderedRing : ∀ {H : Type u_3} [inst : NormedAddCommGroup H] [inst_1 : InnerProductSpace ℂ H] [inst_2 : CompleteSpace H],
  StarOrderedRing (H →L[ℂ] H)
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.maxD_insert : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {k fallback : α},
  (t.insert k).maxD fallback = t.max?.elim k fun k' => if cmp k' k = Ordering.lt then k else k'
-- Mathlib.AlgebraicGeometry.Gluing
AlgebraicGeometry.Scheme.IsLocallyDirected.V_self : ∀ {J : Type w} [inst : CategoryTheory.Category.{v, w} J] (F : CategoryTheory.Functor J AlgebraicGeometry.Scheme)
  [inst_1 : ∀ {i j : J} (f : i ⟶ j), AlgebraicGeometry.IsOpenImmersion (F.map f)] (i : J),
  AlgebraicGeometry.Scheme.IsLocallyDirected.V F i i = ⊤
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.center_toSubsemiring : ∀ (R : Type u) [inst : NonAssocRing R], (Subring.center R).toSubsemiring = Subsemiring.center R
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.instEssSurjCompPreLeft : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] {C : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} C] (F : CategoryTheory.Functor C A) (L : CategoryTheory.Functor A T)
  (R : CategoryTheory.Functor B T) [F.EssSurj], (CategoryTheory.Comma.preLeft F L R).EssSurj
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.pow.eq_def : ∀ (p : Lean.Grind.CommRing.Poly) (k : ℕ),
  p.pow k =
    match k with
    | 0 => Lean.Grind.CommRing.Poly.num 1
    | 1 => p
    | k.succ => p.mul (p.pow k)
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.leftRightHomologyComparison_eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} [inst_2 : S.HasLeftHomology] [inst_3 : S.HasRightHomology]
  (h₁ : S.LeftHomologyData) (h₂ : S.RightHomologyData),
  S.leftRightHomologyComparison =
    CategoryTheory.CategoryStruct.comp h₁.leftHomologyIso.hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftRightHomologyComparison' h₁ h₂)
        h₂.rightHomologyIso.inv)
-- Mathlib.GroupTheory.Coset.Basic
/-- If `s ≤ t`, then there is an embedding `s ⧸ H.subgroupOf s ↪ t ⧸ H.subgroupOf t`.  -/
Subgroup.quotientSubgroupOfEmbeddingOfLE : {α : Type u_1} →
  [inst : Group α] → {s t : Subgroup α} → (H : Subgroup α) → s ≤ t → ↥s ⧸ H.subgroupOf s ↪ ↥t ⧸ H.subgroupOf t
-- Mathlib.Algebra.Homology.Embedding.IsSupported
HomologicalComplex.IsStrictlySupportedOutside.isSupportedOutside : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {K : HomologicalComplex C c'} {e : c.Embedding c'}, K.IsStrictlySupportedOutside e → K.IsSupportedOutside e
-- Mathlib.Algebra.Category.CommAlgCat.Monoidal
CommAlgCat.whiskerRight_hom : ∀ {R : Type u} [inst : CommRing R] {A B : CommAlgCat R} (C : CommAlgCat R) (f : A ⟶ B),
  CommAlgCat.Hom.hom (CategoryTheory.MonoidalCategoryStruct.whiskerRight f C) =
    Algebra.TensorProduct.map (CommAlgCat.Hom.hom f) (AlgHom.id R ↑C)
-- Mathlib.SetTheory.Cardinal.Continuum
Cardinal.aleph_one_le_continuum : Cardinal.aleph 1 ≤ Cardinal.continuum
-- Mathlib.CategoryTheory.Localization.Resolution
CategoryTheory.LocalizerMorphism.essSurj_of_hasLeftResolutions : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D₂ : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_4, u_4} D₂]
  {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂}
  (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) (L₂ : CategoryTheory.Functor C₂ D₂) [L₂.IsLocalization W₂]
  [Φ.HasLeftResolutions], (Φ.functor.comp L₂).EssSurj
-- Init.Data.Nat.Fold
_private.Init.Data.Nat.Fold.0.Nat.anyTR.loop.match_1.eq_2 : ∀ (n : ℕ) (motive : (x : ℕ) → x ≤ n → Sort u_1) (m : ℕ) (h : m.succ ≤ n) (h_1 : (h : 0 ≤ n) → motive 0 h)
  (h_2 : (m : ℕ) → (h : m.succ ≤ n) → motive m.succ h),
  (match m.succ, h with
    | 0, h => h_1 h
    | m.succ, h => h_2 m h) =
    h_2 m h
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.whiskerLeft_rightUnitor_inv_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X Y : C) {Z : C}
  (h :
    CategoryTheory.MonoidalCategoryStruct.tensorObj X
        (CategoryTheory.MonoidalCategoryStruct.tensorObj Y (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.MonoidalCategoryStruct.rightUnitor Y).inv)
      h =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.rightUnitor (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.associator X Y (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom
        h)
-- Mathlib.Data.Sum.Interval
Finset.sumLexLift.eq_2 : ∀ {α₁ : Type u_1} {α₂ : Type u_2} {β₁ : Type u_3} {β₂ : Type u_4} {γ₁ : Type u_5} {γ₂ : Type u_6}
  (f₁ : α₁ → β₁ → Finset γ₁) (f₂ : α₂ → β₂ → Finset γ₂) (g₁ : α₁ → β₂ → Finset γ₁) (g₂ : α₁ → β₂ → Finset γ₂) (val : α₁)
  (val_1 : β₂), Finset.sumLexLift f₁ f₂ g₁ g₂ (Sum.inl val) (Sum.inr val_1) = (g₁ val val_1).disjSum (g₂ val val_1)
-- Mathlib.RingTheory.Spectrum.Prime.FreeLocus
Module.freeLocus_localization : ∀ {R : Type uR} {M : Type uM} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (S : Submonoid R),
  Module.freeLocus (Localization S) (LocalizedModule S M) =
    PrimeSpectrum.comap (algebraMap R (Localization S)) ⁻¹' Module.freeLocus R M
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
/-- `F[S][T] = F[T][S]`  -/
IntermediateField.adjoin_adjoin_comm : ∀ (F : Type u_1) [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] (S T : Set E),
  IntermediateField.restrictScalars F (IntermediateField.adjoin (↥(IntermediateField.adjoin F S)) T) =
    IntermediateField.restrictScalars F (IntermediateField.adjoin (↥(IntermediateField.adjoin F T)) S)