mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.Lattice
inf_rotate' : ∀ {α : Type u} [inst : SemilatticeInf α] (a b c : α), a ⊓ (b ⊓ c) = b ⊓ (c ⊓ a)
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
/-- Define a continuous `𝕜`-linear map from `𝓓^{n₁}_{K₁}(E, F)` to `𝓓^{n₂}_{K₂}(E, F')`.  -/
ContDiffMapSupportedIn.mkCLM : (𝕜 : Type u_1) →
  {E : Type u_2} →
    {F : Type u_3} →
      {F' : Type u_4} →
        [inst : NontriviallyNormedField 𝕜] →
          [inst_1 : NormedAddCommGroup E] →
            [inst_2 : NormedSpace ℝ E] →
              [inst_3 : NormedAddCommGroup F] →
                [inst_4 : NormedSpace ℝ F] →
                  [inst_5 : NormedSpace 𝕜 F] →
                    [inst_6 : SMulCommClass ℝ 𝕜 F] →
                      [inst_7 : NormedAddCommGroup F'] →
                        [inst_8 : NormedSpace ℝ F'] →
                          [inst_9 : NormedSpace 𝕜 F'] →
                            [inst_10 : SMulCommClass ℝ 𝕜 F'] →
                              {n₁ n₂ : ℕ∞} →
                                {K₁ K₂ : TopologicalSpace.Compacts E} →
                                  (A : ContDiffMapSupportedIn E F n₁ K₁ → E → F') →
                                    (∀ (f g : ContDiffMapSupportedIn E F n₁ K₁) (x : E), A (f + g) x = A f x + A g x) →
                                      (∀ (c : 𝕜) (f : ContDiffMapSupportedIn E F n₁ K₁) (x : E),
                                          A (c • f) x = c • A f x) →
                                        (∀ (f : ContDiffMapSupportedIn E F n₁ K₁), ContDiff ℝ (↑n₂) (A f)) →
                                          (∀ (f : ContDiffMapSupportedIn E F n₁ K₁), Set.EqOn (A f) 0 (↑K₂)ᶜ) →
                                            (∀ (i : ℕ),
                                                ↑i ≤ n₂ →
                                                  ∃ s C,
                                                    0 ≤ C ∧
                                                      ∀ (f : ContDiffMapSupportedIn E F n₁ K₁),
                                                        ∀ x ∈ K₂,
                                                          ‖iteratedFDeriv ℝ i (A f) x‖ ≤
                                                            C *
                                                              (s.sup fun j =>
                                                                  ContDiffMapSupportedIn.seminorm 𝕜 E F n₁ K₁ j)
                                                                f) →
                                              ContDiffMapSupportedIn E F n₁ K₁ →L[𝕜] ContDiffMapSupportedIn E F' n₂ K₂
-- Mathlib.AlgebraicGeometry.Pullbacks
/-- We show that the map `W ×[X] Uᵢ ⟶ Uᵢ ×[Z] Y ⟶ W` is the first projection, where the
first map is given by the lift of `W ×[X] Uᵢ ⟶ Uᵢ` and `W ×[X] Uᵢ ⟶ W ⟶ Y`.

It suffices to show that the two map agrees when restricted onto `Uⱼ ×[Z] Y`. In this case,
both maps factor through `V j i` via `pullback_fst_ι_to_V`  -/
AlgebraicGeometry.Scheme.Pullback.lift_comp_ι : ∀ {X Y Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst : ∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g] (i : 𝒰.I₀),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.lift
        (CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.Scheme.Pullback.p1 𝒰 f g) (𝒰.f i))
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Scheme.Pullback.p1 𝒰 f g) (𝒰.f i))
          (AlgebraicGeometry.Scheme.Pullback.p2 𝒰 f g))
        ⋯)
      ((AlgebraicGeometry.Scheme.Pullback.gluing 𝒰 f g).ι i) =
    CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Scheme.Pullback.p1 𝒰 f g) (𝒰.f i)
-- Mathlib.Order.UpperLower.Closure
upperClosure_iUnion : ∀ {α : Type u_1} {ι : Sort u_3} [inst : Preorder α] (f : ι → Set α), upperClosure (⋃ i, f i) = ⨅ i, upperClosure (f i)
-- Mathlib.Probability.Independence.Kernel.IndepFun
/-- A family of functions defined on the same space `Ω` and taking values in possibly different
spaces, each with a measurable space structure, is independent if the family of measurable space
structures they generate on `Ω` is independent. For a function `g` with codomain having measurable
space structure `m`, the generated measurable space structure is `MeasurableSpace.comap g m`.  -/
ProbabilityTheory.Kernel.iIndepFun : {α : Type u_1} →
  {Ω : Type u_2} →
    {ι : Type u_3} →
      {mα : MeasurableSpace α} →
        {mΩ : MeasurableSpace Ω} →
          {β : ι → Type u_8} →
            [m : (x : ι) → MeasurableSpace (β x)] →
              ((x : ι) → Ω → β x) →
                ProbabilityTheory.Kernel α Ω →
                  autoParam (MeasureTheory.Measure α) ProbabilityTheory.Kernel.iIndepFun._auto_1 → Prop
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
CategoryTheory.MorphismProperty.regularEpi_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y),
  CategoryTheory.MorphismProperty.regularEpi C f ↔ CategoryTheory.IsRegularEpi f
-- Init.Data.Order.Ord
Std.LawfulBEqOrd.opposite : ∀ {α : Type u} [inst : BEq α] [inst_1 : Ord α] [Std.OrientedOrd α] [Std.LawfulBEqOrd α], Std.LawfulBEqOrd α
-- Mathlib.Analysis.Meromorphic.NormalForm
/-- If a function is meromorphic in normal form at `x`, then it has non-negative order iff it is
analytic.  -/
MeromorphicNFAt.meromorphicOrderAt_nonneg_iff_analyticAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜}, MeromorphicNFAt f x → (0 ≤ meromorphicOrderAt f x ↔ AnalyticAt 𝕜 f x)
-- Mathlib.Geometry.Manifold.PartitionOfUnity
/-- The `tsupport`s of a smooth partition of unity are locally finite.  -/
SmoothPartitionOfUnity.finite_tsupport : ∀ {ι : Type uι} {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH}
  [inst_2 : TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_3 : TopologicalSpace M]
  [inst_4 : ChartedSpace H M] {s : Set M} (ρ : SmoothPartitionOfUnity ι I M s) (x₀ : M),
  {i | x₀ ∈ tsupport ⇑(ρ i)}.Finite
-- Mathlib.Data.Sym.Basic
Sym.cast_cast : ∀ {α : Type u_1} {n n' : ℕ} {s : Sym α n} {n'' : ℕ} (h : n = n') (h' : n' = n''),
  (Sym.cast h') ((Sym.cast h) s) = (Sym.cast ⋯) s
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey?_alter_self : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [inst_2 : EquivBEq α]
  [LawfulHashable α] {k : α} {f : Option β → Option β},
  m.WF → (m.alter k f).getKey? k = if (f m[k]?).isSome = true then some k else none
-- Mathlib.Algebra.DirectSum.Basic
DirectSum.of_eq_same : ∀ {ι : Type v} {β : ι → Type w} [inst : (i : ι) → AddCommMonoid (β i)] [inst_1 : DecidableEq ι] (i : ι) (x : β i),
  ((DirectSum.of β i) x) i = x
-- Mathlib.LinearAlgebra.Matrix.ConjTranspose
Matrix.conjTranspose_neg : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : AddGroup α] [inst_1 : StarAddMonoid α] (M : Matrix m n α),
  (-M).conjTranspose = -M.conjTranspose
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.CoreMonoidal.μIso_hom_natural_left_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  {F : CategoryTheory.Functor C D} (self : F.CoreMonoidal) {X Y : C} (f : X ⟶ Y) (X' : C) {Z : D}
  (h : F.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj Y X') ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (F.map f) (F.obj X'))
      (CategoryTheory.CategoryStruct.comp (self.μIso Y X').hom h) =
    CategoryTheory.CategoryStruct.comp (self.μIso X X').hom
      (CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategoryStruct.whiskerRight f X')) h)
-- Mathlib.Topology.Order
discreteTopology_iff_singleton_mem_nhds : ∀ {α : Type u_1} [inst : TopologicalSpace α], DiscreteTopology α ↔ ∀ (x : α), {x} ∈ nhds x
-- Mathlib.Algebra.Group.Commute.Basic
Commute.inv_mul_cancel_assoc : ∀ {G : Type u_1} [inst : Group G] {a b : G}, Commute a b → a⁻¹ * (b * a) = b
-- Mathlib.Analysis.Calculus.Deriv.Basic
deriv_zero : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F], deriv 0 = 0
-- Mathlib.Analysis.Normed.Module.RCLike.Extend
StrongDual.toLinearEquiv_extendRCLikeL : ∀ {𝕜 : Type u_4} {F : Type u_5} [inst : RCLike 𝕜] [inst_1 : TopologicalSpace F] [inst_2 : AddCommGroup F]
  [inst_3 : Module 𝕜 F] [inst_4 : ContinuousSMul 𝕜 F] [inst_5 : Module ℝ F] [inst_6 : IsScalarTower ℝ 𝕜 F],
  ↑StrongDual.extendRCLikeL = StrongDual.extendRCLikeₗ
-- Lean.Parser.Types
/-- A syntax array with an inaccessible prefix, used for sound caching.  -/
Lean.Parser.SyntaxStack : Type
-- Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
/-- The Law of Quadratic Reciprocity for the Jacobi symbol: if `a` and `b` are natural numbers
both congruent to `3` mod `4`, then `J(a | b) = -J(b | a)`.  -/
jacobiSym.quadratic_reciprocity_three_mod_four : ∀ {a b : ℕ}, a % 4 = 3 → b % 4 = 3 → jacobiSym (↑a) b = -jacobiSym (↑b) a
-- Mathlib.Data.Sym.Basic
SymOptionSuccEquiv.decode.eq_1 : ∀ {α : Type u_1} {n : ℕ} (s : Sym (Option α) n), SymOptionSuccEquiv.decode (Sum.inl s) = none ::ₛ s
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MultispanShape.ofLinearOrder_R : ∀ (ι : Type w) [inst : LinearOrder ι], (CategoryTheory.Limits.MultispanShape.ofLinearOrder ι).R = ι
-- Lean.Declaration
Lean.instBEqDefinitionVal.beq : Lean.DefinitionVal → Lean.DefinitionVal → Bool
-- Mathlib.Algebra.Category.ModuleCat.Sheaf
SheafOfModules.unitHomEquiv_apply_coe : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} (M : SheafOfModules R) (f : SheafOfModules.unit R ⟶ M) (X : Cᵒᵖ),
  ↑(M.unitHomEquiv f) X = (CategoryTheory.ConcreteCategory.hom (f.val.app X)) 1
-- Aesop.Index
Aesop.Index.unindex : {α : Type} → Aesop.Index α → (Aesop.Rule α → Bool) → Aesop.Index α
-- Mathlib.Logic.Function.Basic
Function.Bijective.of_comp_iff : ∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (f : α → β) {g : γ → α},
  Function.Bijective g → (Function.Bijective (f ∘ g) ↔ Function.Bijective f)
-- Mathlib.ModelTheory.LanguageMap
/-- The mapping of functions  -/
FirstOrder.Language.LHom.onFunction : {L : FirstOrder.Language} → {L' : FirstOrder.Language} → (L →ᴸ L') → ⦃n : ℕ⦄ → L.Functions n → L'.Functions n
-- Mathlib.CategoryTheory.Monoidal.Preadditive
CategoryTheory.leftDistributor_ext₂_right_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C]
  [inst_4 : CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [inst_5 : Finite J] {X Y Z : C} {f : J → C}
  {g h :
    X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj Y (CategoryTheory.MonoidalCategoryStruct.tensorObj Z (⨁ f))},
  g = h ↔
    ∀ (j : J),
      CategoryTheory.CategoryStruct.comp g
          (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y
            (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Z (CategoryTheory.Limits.biproduct.π f j))) =
        CategoryTheory.CategoryStruct.comp h
          (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y
            (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Z (CategoryTheory.Limits.biproduct.π f j)))
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.instInhabitedActionResult : Inhabited Lean.Meta.Grind.ActionResult
-- Mathlib.Topology.EMetricSpace.BoundedVariation
LipschitzWith.comp_boundedVariationOn : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] {F : Type u_3}
  [inst_2 : PseudoEMetricSpace F] {f : E → F} {C : NNReal},
  LipschitzWith C f → ∀ {g : α → E} {s : Set α}, BoundedVariationOn g s → BoundedVariationOn (f ∘ g) s
-- Mathlib.Algebra.EuclideanDomain.Field
Field.toEuclideanDomain : {K : Type u_1} → [Field K] → EuclideanDomain K
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.dropSuffix?_eq_none_iff : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.BackwardPattern pat]
  [String.Slice.Pattern.LawfulBackwardPattern pat] {s : String.Slice}, s.dropSuffix? pat = none ↔ s.endsWith pat = false
-- Aesop.Rule.Name
_private.Aesop.Rule.Name.0.Aesop.RuleName.Json.builder : Aesop.RuleName.Json✝ → Aesop.BuilderName
-- Mathlib.MeasureTheory.Integral.Average
MeasureTheory.laverage_zero_measure : ∀ {α : Type u_1} {m0 : MeasurableSpace α} (f : α → ENNReal), ⨍⁻ (x : α), f x ∂0 = 0
-- Mathlib.Algebra.Lie.Ideal
LieHom.mem_idealRange : ∀ {R : Type u} {L : Type v} {L' : Type w₂} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieRing L']
  [inst_3 : LieAlgebra R L'] [inst_4 : LieAlgebra R L] (f : L →ₗ⁅R⁆ L') (x : L), f x ∈ f.idealRange
-- Mathlib.Tactic.DepRewrite
/-- Monad for computing `dabstract`.

The `Nat` state tracks which occurrence of the pattern we are about to see, 1-indexed
(so the initial value is `1`).

The cache stores results of `visit` together with
- the `Nat` state before the cached call; and
- the difference in the state resulting from the call.

We store these because even if the cache hits,
we must update the state as if the call had been made.
Storing the difference suffices because the state increases monotonically.
See also `canUseCache`.  -/
Mathlib.Tactic.DepRewrite.M : Type → Type
-- Init.Data.UInt.Basic
instAndOpUInt32 : AndOp UInt32
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
/-- In a space with second countable topology, measurable implies strongly measurable.  -/
Measurable.stronglyMeasurable : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {mα : MeasurableSpace α} [inst : MeasurableSpace β]
  [inst_1 : TopologicalSpace β] [TopologicalSpace.PseudoMetrizableSpace β] [SecondCountableTopology β]
  [OpensMeasurableSpace β], Measurable f → MeasureTheory.StronglyMeasurable f
-- Mathlib.CategoryTheory.Preadditive.Mat
CategoryTheory.Mat.id_apply_self : ∀ (R : Type u) [inst : Semiring R] (M : CategoryTheory.Mat R) (i : M.obj), CategoryTheory.CategoryStruct.id M i i = 1
-- Lean.Elab.DeclModifiers
Lean.Elab.Visibility.isPublic : Lean.Elab.Visibility → Bool
-- Mathlib.Algebra.Homology.DerivedCategory.SingleTriangle
CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_inv_hom₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact),
  hS.singleTriangleIso.inv.hom₂ = ((DerivedCategory.singleFunctorsPostcompQIso C).inv.hom 0).app S.X₂
-- Mathlib.Analysis.Analytic.Inverse
FormalMultilinearSeries.rightInv.eq_def : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  (p : FormalMultilinearSeries 𝕜 E F) (i : E ≃L[𝕜] F) (x : E) (x_1 : ℕ),
  p.rightInv i x x_1 =
    match x_1 with
    | 0 => ContinuousMultilinearMap.uncurry0 𝕜 F x
    | 1 => (continuousMultilinearCurryFin1 𝕜 F E).symm ↑i.symm
    | n.succ.succ =>
      have q := fun k => if k < n + 2 then p.rightInv i x k else 0;
      -(↑i.symm).compContinuousMultilinearMap (p.comp q (n + 2))
-- Init.Data.UInt.Lemmas
UInt64.toUInt16_ofNatTruncate_of_lt : ∀ {n : ℕ}, n < UInt64.size → (UInt64.ofNatClamp n).toUInt16 = UInt16.ofNat n
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.smulSet.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β], Set.smulSet = { smul := fun a => Set.image fun x => a • x }
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.negDblY_of_Y_eq' : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} [NoZeroDivisors R] {P Q : Fin 3 → R},
  W'.Equation P →
    Q 2 ≠ 0 →
      P 0 * Q 2 = Q 0 * P 2 →
        P 1 * Q 2 = Q 1 * P 2 →
          P 1 * Q 2 = W'.negY Q * P 2 → W'.negDblY P * P 2 ^ 2 = -(MvPolynomial.eval P) W'.polynomialX ^ 3
-- Init.Data.SInt.Bitwise
instLawfulCommIdentityInt64HAndNegOfNat : Std.LawfulCommIdentity (fun x1 x2 => x1 &&& x2) (-1)
-- Init.Data.SInt.Basic
/-- Converts a word-sized signed integer into the word-sized unsigned integer that is its two's
complement encoding.
 -/
ISize.toUSize : ISize → USize
-- Mathlib.Geometry.Manifold.VectorField.LieBracket
VectorField.mpullbackWithin_mlieBracketWithin_of_isSymmSndFDerivWithinAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {H' : Type u_5} [inst_6 : TopologicalSpace H']
  {E' : Type u_6} [inst_7 : NormedAddCommGroup E'] [inst_8 : NormedSpace 𝕜 E'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] [IsManifold I 2 M]
  [inst_12 : IsManifold I' 2 M'] [CompleteSpace E] {f : M → M'} {V W : (x : M') → TangentSpace I' x} {x₀ : M}
  {s : Set M} {t : Set M'},
  MDiffAt[t] (T% V) (f x₀) →
    MDiffAt[t] (T% W) (f x₀) →
      UniqueMDiff[s] →
        ContMDiffWithinAt I I' 2 f s x₀ →
          x₀ ∈ s →
            f ⁻¹' t ∈ nhdsWithin x₀ s →
              IsSymmSndFDerivWithinAt 𝕜 (↑(extChartAt I' (f x₀)) ∘ f ∘ ↑(extChartAt I x₀).symm)
                  (↑(extChartAt I x₀).symm ⁻¹' s ∩ Set.range ↑I) (↑(extChartAt I x₀) x₀) →
                VectorField.mpullbackWithin I I' f (VectorField.mlieBracketWithin I' V W t) s x₀ =
                  VectorField.mlieBracketWithin I (VectorField.mpullbackWithin I I' f V s)
                    (VectorField.mpullbackWithin I I' f W s) s x₀
-- Mathlib.Data.Finset.Union
Finset.Nonempty.biUnion : ∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {t : α → Finset β} [inst : DecidableEq β],
  s.Nonempty → (∀ x ∈ s, (t x).Nonempty) → (s.biUnion t).Nonempty
-- Mathlib.MeasureTheory.MeasurableSpace.Instances
Subsingleton.measurableSingletonClass : ∀ {α : Type u_1} [inst : MeasurableSpace α] [Subsingleton α], MeasurableSingletonClass α
-- Mathlib.Algebra.Category.ModuleCat.Topology.Homology
TopModuleCat.kerι_comp : ∀ {R : Type u} [inst : Ring R] [inst_1 : TopologicalSpace R] {M N : TopModuleCat R} (φ : M ⟶ N),
  CategoryTheory.CategoryStruct.comp (TopModuleCat.kerι φ) φ = 0
-- Mathlib.Algebra.Star.TensorProduct
TensorProduct.instStar : {R : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : StarRing R] →
          [inst_2 : AddCommMonoid A] →
            [inst_3 : StarAddMonoid A] →
              [inst_4 : Module R A] →
                [StarModule R A] →
                  [inst_6 : AddCommMonoid B] →
                    [inst_7 : StarAddMonoid B] → [inst_8 : Module R B] → [StarModule R B] → Star (TensorProduct R A B)
-- Mathlib.CategoryTheory.Sites.Sheaf
/-- The map `pr₀*` of the Stacks entry.  -/
CategoryTheory.Presheaf.firstMap : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {A : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} A] →
        {U : C} →
          (R : CategoryTheory.Presieve U) →
            (P : CategoryTheory.Functor Cᵒᵖ A) →
              [inst_2 : CategoryTheory.Limits.HasProducts A] →
                [inst_3 : CategoryTheory.Limits.HasPullbacks C] →
                  CategoryTheory.Presheaf.firstObj R P ⟶ CategoryTheory.Presheaf.secondObj R P
-- Mathlib.Order.Filter.Pointwise
Filter.NeBot.div_zero_nonneg : ∀ {α : Type u_2} [inst : GroupWithZero α] {f : Filter α}, f.NeBot → 0 ≤ f / 0
-- Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
CategoryTheory.Abelian.SpectralObject.spectralSequence_page_d_eq : ∀ {C : Type u_1} {ι : Type u_2} {κ : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Abelian C] [inst_2 : Preorder ι] (X : CategoryTheory.Abelian.SpectralObject C ι)
  {c : ℤ → ComplexShape κ} {r₀ : ℤ} (data : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀)
  [inst_3 : X.HasSpectralSequence data] (r : ℤ) (hr : r₀ ≤ r) (pq pq' : κ) (hpq : (c r).Rel pq pq')
  {i₀ i₁ i₂ i₃ i₄ i₅ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₅ : i₄ ⟶ i₅)
  (h₀ : i₀ = data.i₀ r pq' ⋯) (h₁ : i₁ = data.i₁ pq') (h₂ : i₂ = data.i₀ r pq ⋯) (h₃ : i₃ = data.i₁ pq)
  (h₄ : i₄ = data.i₂ pq) (h₅ : i₅ = data.i₃ r pq ⋯) (n₀ n₁ n₂ n₃ : ℤ) (hn₁' : n₁ = data.deg pq)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.spectralSequence_page_d_eq._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.spectralSequence_page_d_eq._auto_3)
  (hn₃ : autoParam (n₂ + 1 = n₃) CategoryTheory.Abelian.SpectralObject.spectralSequence_page_d_eq._auto_5),
  ((X.spectralSequence data).page r ⋯).d pq pq' =
    CategoryTheory.CategoryStruct.comp
      (X.spectralSequencePageXIso data r hr pq i₂ i₃ i₄ i₅ h₂ h₃ h₄ h₅ n₀ n₁ n₂ hn₁' ⋯ ⋯).hom
      (CategoryTheory.CategoryStruct.comp (X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃)
        (X.spectralSequencePageXIso data r hr pq' i₀ i₁ i₂ i₃ h₀ h₁ ⋯ ⋯ n₁ n₂ n₃ ⋯ ⋯ ⋯).inv)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKey_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l : List ((a : α) × β a)} {k : α}
  (contains_eq_false : (List.map Sigma.fst l).contains k = false) {h : k ∈ m.insertMany l},
  (m.insertMany l).getKey k h = m.getKey k ⋯
-- Mathlib.Data.Matrix.Basic
LinearEquiv.mapMatrix_trans : ∀ {m : Type u_2} {n : Type u_3} {R : Type u_7} {S : Type u_8} {T : Type u_9} {α : Type u_11} {β : Type u_12}
  {γ : Type u_13} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : Semiring T] [inst_3 : AddCommMonoid α]
  [inst_4 : AddCommMonoid β] [inst_5 : AddCommMonoid γ] [inst_6 : Module R α] [inst_7 : Module S β]
  [inst_8 : Module T γ] {σᵣₛ : R →+* S} {σₛₜ : S →+* T} {σᵣₜ : R →+* T} [inst_9 : RingHomCompTriple σᵣₛ σₛₜ σᵣₜ]
  {σₛᵣ : S →+* R} {σₜₛ : T →+* S} {σₜᵣ : T →+* R} [inst_10 : RingHomCompTriple σₜₛ σₛᵣ σₜᵣ]
  [inst_11 : RingHomInvPair σᵣₛ σₛᵣ] [inst_12 : RingHomInvPair σₛᵣ σᵣₛ] [inst_13 : RingHomInvPair σₛₜ σₜₛ]
  [inst_14 : RingHomInvPair σₜₛ σₛₜ] [inst_15 : RingHomInvPair σᵣₜ σₜᵣ] [inst_16 : RingHomInvPair σₜᵣ σᵣₜ]
  (f : α ≃ₛₗ[σᵣₛ] β) (g : β ≃ₛₗ[σₛₜ] γ), f.mapMatrix.trans g.mapMatrix = (f.trans g).mapMatrix
-- Mathlib.MeasureTheory.Integral.IntervalAverage
/-- `⨍ x in a..b, f x` is the average of `f` over the interval `Ι a b` w.r.t. the Lebesgue
measure.  -/
«term⨍_In_.._,_» : Lean.ParserDescr
-- Mathlib.RingTheory.Ideal.Quotient.Operations
Ideal.quotientKerAlgEquivOfRightInverse_apply : ∀ {R₁ : Type u_1} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R₁] [inst_1 : Ring A] [inst_2 : Algebra R₁ A]
  [inst_3 : Semiring B] [inst_4 : Algebra R₁ B] {f : A →ₐ[R₁] B} {g : B → A} (hf : Function.RightInverse g ⇑f)
  (a : A ⧸ RingHom.ker f.toRingHom), (Ideal.quotientKerAlgEquivOfRightInverse hf) a = (↑f).kerLift a
-- Mathlib.MeasureTheory.Measure.Haar.Unique
MeasureTheory.Measure.measurePreserving_zpow : ∀ {G : Type u_1} [inst : CommGroup G] [inst_1 : TopologicalSpace G] [IsTopologicalGroup G] [inst_3 : MeasurableSpace G]
  [BorelSpace G] (μ : MeasureTheory.Measure G) [μ.IsHaarMeasure] [CompactSpace G] [RootableBy G ℤ] {n : ℤ},
  n ≠ 0 → MeasureTheory.MeasurePreserving (fun g => g ^ n) μ μ
-- Mathlib.Logic.Function.Basic
Function.FactorsThrough.comp_left : ∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {δ : Sort u_4} {f : α → β} {g : α → γ},
  Function.FactorsThrough g f → ∀ (g' : γ → δ), Function.FactorsThrough (g' ∘ g) f
-- Mathlib.Geometry.Manifold.ContMDiff.Basic
contMDiffAt_zero : ∀ {𝕜 : 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] {E' : Type u_5} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E']
  {H' : Type u_6} [inst_7 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7}
  [inst_8 : TopologicalSpace M'] [inst_9 : ChartedSpace H M] [inst_10 : ChartedSpace H' M'] {x : M} {n : WithTop ℕ∞}
  [inst_11 : Zero M'], ContMDiffAt I I' n 0 x