mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
/-- **Alias** of `Submodule.orthogonalProjectionOnto_comp_subtypeL_eq_zero_iff`.

---

The projection into `U` from `V` is the zero map if and only if `U` and `V` are orthogonal.  -/
Submodule.orthogonalProjection_comp_subtypeL_eq_zero_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {U V : Submodule 𝕜 E} [inst_3 : U.HasOrthogonalProjection], U.orthogonalProjectionOnto ∘SL V.subtypeL = 0 ↔ U ⟂ V
-- Mathlib.Algebra.Group.Subgroup.Ker
AddMonoidHom.coe_ker : ∀ {G : Type u_1} [inst : AddGroup G] {M : Type u_7} [inst_1 : AddZeroClass M] (f : G →+ M), ↑f.ker = ⇑f ⁻¹' {0}
-- Mathlib.Algebra.MvPolynomial.Supported
MvPolynomial.supportedEquivMvPolynomial.eq_1 : ∀ {σ : Type u_1} {R : Type u} [inst : CommSemiring R] (s : Set σ),
  MvPolynomial.supportedEquivMvPolynomial s =
    ((MvPolynomial.supported R s).equivOfEq (MvPolynomial.rename Subtype.val).range ⋯).trans
      (AlgEquiv.ofInjective (MvPolynomial.rename Subtype.val) ⋯).symm
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToIntInfo
Lean.Meta.Grind.Arith.Cutsat.ToIntInfo.ofDiseq : Lean.Meta.Grind.Arith.Cutsat.ToIntInfo → Lean.Expr
-- Mathlib.Data.Fintype.BigOperators
Fintype.card_filter_piFinset_eq : ∀ {ι : Type u_4} {α : ι → Type u_6} [inst : DecidableEq ι] [inst_1 : Fintype ι] [inst_2 : (i : ι) → DecidableEq (α i)]
  (s : (i : ι) → Finset (α i)) (i : ι) (a : α i),
  {f ∈ Fintype.piFinset s | f i = a}.card = if a ∈ s i then ∏ b ∈ Finset.univ.erase i, (s b).card else 0
-- Mathlib.CategoryTheory.Category.Pairwise
CategoryTheory.Pairwise.diagramMap.eq_4 : ∀ {ι : Type v} {α : Type u} (U : ι → α) [inst : SemilatticeInf α] (i j : ι),
  CategoryTheory.Pairwise.diagramMap U (CategoryTheory.Pairwise.Hom.right i j) = CategoryTheory.homOfLE ⋯
-- Batteries.Data.List.Basic
List.takeList.eq_def : ∀ {α : Type u_1} (x : List α) (x_1 : List ℕ),
  x.takeList x_1 =
    match x, x_1 with
    | xs, [] => ([], xs)
    | xs, n :: ns =>
      match List.splitAt n xs with
      | (xs₁, xs₂) =>
        match xs₂.takeList ns with
        | (xss, rest) => (xs₁ :: xss, rest)
-- Mathlib.CategoryTheory.Limits.IsConnected
/-- An index category is connected iff the colimit of the constant singleton-valued functor is a
singleton.  -/
CategoryTheory.Limits.Types.isConnected_iff_colimit_constPUnitFunctor_iso_pUnit : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.Types.constPUnitFunctor C)],
  CategoryTheory.IsConnected C ↔
    Nonempty (CategoryTheory.Limits.colimit (CategoryTheory.Limits.Types.constPUnitFunctor C) ≅ PUnit.{w + 1})
-- Std.Sat.AIG.If
Std.Sat.AIG.RefVec.IfInput.discr : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] → {aig : Std.Sat.AIG α} → {w : ℕ} → Std.Sat.AIG.RefVec.IfInput aig w → aig.Ref
-- Lean.Data.Lsp.Basic
Lean.Lsp.WorkDoneProgressOptions.mk.sizeOf_spec : ∀ (workDoneProgress : Bool), sizeOf { workDoneProgress := workDoneProgress } = 1 + sizeOf workDoneProgress
-- Mathlib.Topology.Semicontinuity.Defs
UpperHemicontinuousOn.const : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {s : Set α} {z : Set β},
  UpperHemicontinuousOn (fun _x => z) s
-- Aesop.RuleTac.Descr
Aesop.RuleTacDescr.forward.sizeOf_spec : ∀ (term : Aesop.RuleTerm) (immediate : Aesop.UnorderedArraySet Aesop.PremiseIndex) (isDestruct : Bool),
  sizeOf (Aesop.RuleTacDescr.forward term immediate isDestruct) = 1 + sizeOf term + sizeOf immediate + sizeOf isDestruct
-- Mathlib.Topology.Clopen
continuous_boolIndicator_iff_isClopen : ∀ {X : Type u} [inst : TopologicalSpace X] (U : Set X), Continuous U.boolIndicator ↔ IsClopen U
-- Mathlib.MeasureTheory.Group.Convolution
/-- The convolution of s-finite measures is s-finite.  -/
MeasureTheory.Measure.sfinite_mconv_of_sfinite : ∀ {M : Type u_1} [inst : Monoid M] [inst_1 : MeasurableSpace M] (μ ν : MeasureTheory.Measure M)
  [MeasureTheory.SFinite μ] [MeasureTheory.SFinite ν], MeasureTheory.SFinite (μ.mconv ν)
-- Batteries.Data.List.Lemmas
List.exists_or_eq_self_of_replaceF : ∀ {α : Type u_1} (p : α → Option α) (l : List α),
  List.replaceF p l = l ∨
    ∃ a a' l₁ l₂, (∀ b ∈ l₁, p b = none) ∧ p a = some a' ∧ l = l₁ ++ a :: l₂ ∧ List.replaceF p l = l₁ ++ a' :: l₂
-- Mathlib.Algebra.BigOperators.Finprod
/-- Given a finite set `s`, the product of `f i * g i` over `i ∈ s` equals the product of `f i`
over `i ∈ s` times the product of `g i` over `i ∈ s`.  -/
finprod_mem_mul_distrib : ∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] {f g : α → M} {s : Set α},
  s.Finite → ∏ᶠ (i : α) (_ : i ∈ s), f i * g i = (∏ᶠ (i : α) (_ : i ∈ s), f i) * ∏ᶠ (i : α) (_ : i ∈ s), g i
-- Lean.Meta.Basic
/-- NOTE: value purely intended for equality comparison, *NOT* following the transparency lattice.  -/
Lean.Meta.TransparencyMode.toUInt64 : Lean.Meta.TransparencyMode → UInt64
-- Mathlib.AlgebraicGeometry.AffineScheme
/-- The global section functor of an affine scheme.  -/
AlgebraicGeometry.AffineScheme.Γ : CategoryTheory.Functor AlgebraicGeometry.AffineSchemeᵒᵖ CommRingCat
-- Mathlib.Topology.Order.LocalExtr
IsLocalMaxOn.comp_continuousOn : ∀ {α : Type u} {β : Type v} {δ : Type x} [inst : TopologicalSpace α] [inst_1 : Preorder β] {f : α → β}
  [inst_2 : TopologicalSpace δ] {t : Set α} {s : Set δ} {g : δ → α} {b : δ},
  IsLocalMaxOn f t (g b) → s ⊆ g ⁻¹' t → ContinuousOn g s → b ∈ s → IsLocalMaxOn (f ∘ g) s b
-- Mathlib.Analysis.Normed.Group.Defs
/-- the `ℝ`-valued norm function.  -/
Norm.norm : {E : Type u_8} → [self : Norm E] → E → ℝ
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.HomologyData.op_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h : S.HomologyData), h.op.right = h.left.op
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Tactic.ComputeAsymptotics.MultiseriesExpansion.Approximates.nil_tendsto_zero : ∀ {basis_hd : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis} {f : ℝ → ℝ},
  (Tactic.ComputeAsymptotics.MultiseriesExpansion.mk Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.nil
        f).Approximates →
    Filter.Tendsto f Filter.atTop (nhds 0)
-- Mathlib.Analysis.Normed.Operator.Bilinear
ContinuousLinearMap.opNorm_flip : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {E : Type u_4} {F : Type u_6} {G : Type u_8}
  [inst : SeminormedAddCommGroup E] [inst_1 : SeminormedAddCommGroup F] [inst_2 : SeminormedAddCommGroup G]
  [inst_3 : NontriviallyNormedField 𝕜] [inst_4 : NontriviallyNormedField 𝕜₂] [inst_5 : NontriviallyNormedField 𝕜₃]
  [inst_6 : NormedSpace 𝕜 E] [inst_7 : NormedSpace 𝕜₂ F] [inst_8 : NormedSpace 𝕜₃ G] {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃}
  [inst_9 : RingHomIsometric σ₂₃] [inst_10 : RingHomIsometric σ₁₃] (f : E →SL[σ₁₃] F →SL[σ₂₃] G), ‖f.flip‖ = ‖f‖
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.image_neg_of_apply_neg_eq_neg : ∀ {α : Type u_2} {β : Type u_3} [inst : InvolutiveNeg α] {s : Set α} [inst_1 : InvolutiveNeg β] {f g : α → β},
  (∀ x ∈ s, f (-x) = -g x) → f '' (-s) = -g '' s
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.instNSMul : {R : Type u} → [inst : Semiring R] → SMul ℕ (Polynomial R)
-- Mathlib.Order.Bounded
Set.unbounded_le_of_forall_exists_lt : ∀ {α : Type u_1} {s : Set α} [inst : Preorder α], (∀ (a : α), ∃ b ∈ s, a < b) → Set.Unbounded (fun x1 x2 => x1 ≤ x2) s
-- Mathlib.Data.PEquiv
PEquiv.instSemilatticeInfOfDecidableEq : {α : Type u} → {β : Type v} → [DecidableEq α] → [DecidableEq β] → SemilatticeInf (α ≃. β)
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.isHashSelf_expand : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [LawfulHashable α] [EquivBEq α]
  {buckets : { d // 0 < d.size }}, Std.DHashMap.Internal.IsHashSelf ↑(Std.DHashMap.Internal.Raw₀.expand buckets)
-- Mathlib.Topology.Category.LightProfinite.Basic
instIsEquivalenceLightDiagram'LightDiagramToLightFunctor : LightDiagram'.toLightFunctor.IsEquivalence
-- Mathlib.Tactic.NormNum.Ineq
Mathlib.Meta.NormNum.isNat_le_true : ∀ {α : Type u_1} [inst : Semiring α] [inst_1 : PartialOrder α] [IsOrderedRing α] {a b : α} {a' b' : ℕ},
  Mathlib.Meta.NormNum.IsNat a a' → Mathlib.Meta.NormNum.IsNat b b' → a'.ble b' = true → a ≤ b
-- Mathlib.Topology.ContinuousMap.Polynomial
Polynomial.aeval_continuousMap_apply : ∀ {R : Type u_1} {α : Type u_2} [inst : TopologicalSpace α] [inst_1 : CommSemiring R] [inst_2 : TopologicalSpace R]
  [inst_3 : IsTopologicalSemiring R] (g : Polynomial R) (f : C(α, R)) (x : α),
  ((Polynomial.aeval f) g) x = Polynomial.eval (f x) g
-- Std.Async.Basic
Std.Async.Async.instMonadAwaitAsyncTask : Std.Async.MonadAwait Std.Async.AsyncTask Std.Async.Async
-- Lean.DocString.Parser
Lean.Doc.Parser.OrderedListType.numDot.sizeOf_spec : sizeOf Lean.Doc.Parser.OrderedListType.numDot = 1
-- Mathlib.RingTheory.Length
/-- Length is additive in exact sequences.  -/
Module.length_eq_add_of_exact : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N : Type u_3}
  {P : Type u_4} [inst_3 : AddCommGroup N] [inst_4 : AddCommGroup P] [inst_5 : Module R N] [inst_6 : Module R P]
  (f : N →ₗ[R] M) (g : M →ₗ[R] P),
  Function.Injective ⇑f →
    Function.Surjective ⇑g → Function.Exact ⇑f ⇑g → Module.length R M = Module.length R N + Module.length R P
-- Std.Http.Data.Status
Std.Http.Status.preconditionFailed.sizeOf_spec : sizeOf Std.Http.Status.preconditionFailed = 1
-- Mathlib.Order.SuccPred.Basic
/-- **Alias** of the forward direction of `Order.pred_le_pred_iff`. -/
Order.le_of_pred_le_pred : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : PredOrder α] {a b : α} [NoMinOrder α],
  Order.pred b ≤ Order.pred a → b ≤ a
-- Mathlib.Algebra.Torsor.Defs
Equiv.pointReflection_symm : ∀ {G : Type u_3} {P : Type u_4} [inst : AddGroup G] [inst_1 : AddTorsor G P] (x : P),
  Equiv.symm (Equiv.pointReflection x) = Equiv.pointReflection x
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.maxKey!_eq_default : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.isEmpty = true → t.maxKey! = default
-- Qq.Delab
Qq.Impl.delabQuotedLevel : Lean.PrettyPrinter.Delaborator.DelabM Lean.Syntax.Level
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgEquiv.toNonUnitalStarAlgHom_ofNonUnitalStarAlgHom : ∀ {R : Type u_1} {A₁ : Type u_2} {A₂ : Type u_3} [inst : Monoid R] [inst_1 : NonUnitalNonAssocSemiring A₁]
  [inst_2 : DistribMulAction R A₁] [inst_3 : Star A₁] [inst_4 : NonUnitalNonAssocSemiring A₂]
  [inst_5 : DistribMulAction R A₂] [inst_6 : Star A₂] (f : A₁ →⋆ₙₐ[R] A₂) (g : A₂ →⋆ₙₐ[R] A₁)
  (h₁ : g.comp f = NonUnitalStarAlgHom.id R A₁) (h₂ : f.comp g = NonUnitalStarAlgHom.id R A₂),
  (StarAlgEquiv.ofNonUnitalStarAlgHom f g h₁ h₂).toNonUnitalStarAlgHom = f
-- Mathlib.Algebra.Category.BoolRing
_private.Mathlib.Algebra.Category.BoolRing.0.BoolRing.Hom.mk.injEq : ∀ {R : BoolRing} {S : BoolRing} (hom' hom'_1 : ↑R →+* ↑S), ({ hom' := hom' } = { hom' := hom'_1 }) = (hom' = hom'_1)
-- Lean.Elab.DocString
/-- Reports errors registered via `Term.registerMVarErrorInfo` for any metavariable still appearing in
the types or values of fresh local declarations introduced during docstring elaboration. This
catches unresolved holes from `{given}` and `{givenInstance}` before the term state is rolled back.
 -/
_private.Lean.Elab.DocString.0.Lean.Doc.checkUnsolvedDocMVars : Lean.LocalContext → Lean.Doc.State → Lean.Elab.TermElabM Unit
-- Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
MvPolynomial.coe_mapEquivMonic_comp' : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  [inst_3 : Algebra R S] [inst_4 : Algebra R T] (n : ℕ) (f : MvPolynomial (Fin n) R →ₐ[R] S) (g : S →ₐ[R] T),
  (MvPolynomial.mapEquivMonic R T n) (g.comp f) = ((MvPolynomial.mapEquivMonic R S n) f).map ↑g
-- Init.Grind.Ordered.Linarith
_private.Init.Grind.Ordered.Linarith.0.Lean.Grind.Linarith.Poly.combine.match_1.eq_3 : ∀ (motive : Lean.Grind.Linarith.Poly → Lean.Grind.Linarith.Poly → Sort u_1) (a₁ : ℤ) (x₁ : Lean.Grind.Linarith.Var)
  (p₁ : Lean.Grind.Linarith.Poly) (a₂ : ℤ) (x₂ : Lean.Grind.Linarith.Var) (p₂ : Lean.Grind.Linarith.Poly)
  (h_1 : (p₂ : Lean.Grind.Linarith.Poly) → motive Lean.Grind.Linarith.Poly.nil p₂)
  (h_2 : (p₁ : Lean.Grind.Linarith.Poly) → motive p₁ Lean.Grind.Linarith.Poly.nil)
  (h_3 :
    (a₁ : ℤ) →
      (x₁ : Lean.Grind.Linarith.Var) →
        (p₁ : Lean.Grind.Linarith.Poly) →
          (a₂ : ℤ) →
            (x₂ : Lean.Grind.Linarith.Var) →
              (p₂ : Lean.Grind.Linarith.Poly) →
                motive (Lean.Grind.Linarith.Poly.add a₁ x₁ p₁) (Lean.Grind.Linarith.Poly.add a₂ x₂ p₂)),
  (match Lean.Grind.Linarith.Poly.add a₁ x₁ p₁, Lean.Grind.Linarith.Poly.add a₂ x₂ p₂ with
    | Lean.Grind.Linarith.Poly.nil, p₂ => h_1 p₂
    | p₁, Lean.Grind.Linarith.Poly.nil => h_2 p₁
    | Lean.Grind.Linarith.Poly.add a₁ x₁ p₁, Lean.Grind.Linarith.Poly.add a₂ x₂ p₂ => h_3 a₁ x₁ p₁ a₂ x₂ p₂) =
    h_3 a₁ x₁ p₁ a₂ x₂ p₂
-- Mathlib.RingTheory.AdicCompletion.Algebra
AdicCompletion.instIntCast : {R : Type u_1} → [inst : CommRing R] → (I : Ideal R) → IntCast (AdicCompletion I R)
-- Std.Data.TreeSet.Raw.Basic
Std.TreeSet.Raw.mk.inj : ∀ {α : Type u} {cmp : autoParam (α → α → Ordering) Std.TreeSet.Raw._auto_1}
  {inner inner_1 : Std.TreeMap.Raw α Unit cmp}, { inner := inner } = { inner := inner_1 } → inner = inner_1
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
/-- A combination of two points expressed with `lineMap` (with the two points reversed) lies in
their affine span.  -/
AffineMap.lineMap_rev_mem_affineSpan_pair : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] (r : k) (p₁ p₂ : P), (AffineMap.lineMap p₂ p₁) r ∈ line[k, p₁, p₂]
-- Mathlib.Algebra.Lie.Weights.Killing
/-- The coroot space of `α` viewed as a submodule of the ambient Lie algebra `L`.
This represents the image of the coroot space under the inclusion `H ↪ L`.  -/
LieAlgebra.IsKilling.corootSubmodule : {K : Type u_2} →
  {L : Type u_3} →
    [inst : LieRing L] →
      [inst_1 : Field K] →
        [inst_2 : LieAlgebra K L] →
          [FiniteDimensional K L] →
            {H : LieSubalgebra K L} →
              [inst_4 : H.IsCartanSubalgebra] → LieModule.Weight K (↥H) L → LieSubmodule K (↥H) L
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.NonemptyCompacts.nonempty_iff : ∀ {α : Type u_1} [inst : TopologicalSpace α], Nonempty (TopologicalSpace.NonemptyCompacts α) ↔ Nonempty α
-- Qq.ForLean.ReduceEval
Lean.Meta.instReduceEvalLevelMVarId_qq : Lean.Meta.ReduceEval Lean.LevelMVarId
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.tensorAlgEquiv_of : ∀ {R : Type u_6} {S : Type u_7} {T : Type u_8} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  [inst_3 : Algebra R S] [inst_4 : Algebra R T] (p : Polynomial S) (q : Polynomial (TensorProduct R T S))
  (h : Polynomial.map Algebra.TensorProduct.includeRight.toRingHom p = q) {x : S},
  (AdjoinRoot.tensorAlgEquiv p q h) (1 ⊗ₜ[R] (AdjoinRoot.of p) x) = (AdjoinRoot.of q) (1 ⊗ₜ[R] x)
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.minEntry?.eq_2 : ∀ {α : Type u} {β : α → Type v} (size : ℕ) (k : α) (v : β k) (r : Std.DTreeMap.Internal.Impl α β),
  (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r).minEntry? = some ⟨k, v⟩
-- Mathlib.RingTheory.LocalProperties.Exactness
bijective_of_localized_span : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] (s : Set R),
  Ideal.span s = ⊤ →
    ∀ (f : M →ₗ[R] N),
      (∀ (r : ↑s), Function.Bijective ⇑((LocalizedModule.map (Submonoid.powers ↑r)) f)) → Function.Bijective ⇑f
-- Mathlib.Algebra.Group.ModEq
AddCommGroup.ModEq.add_nsmul : ∀ {M : Type u_1} [inst : AddCommMonoid M] {a b p : M} (n : ℕ), a ≡ b [PMOD p] → a + n • p ≡ b [PMOD p]
-- Mathlib.Order.Directed
DirectedOn.mono' : ∀ {α : Type u_1} {r r' : α → α → Prop} {s : Set α},
  DirectedOn r s → (∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ s → r a b → r' a b) → DirectedOn r' s
-- Mathlib.Data.Finset.Lattice.Basic
Finset.inter_self : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Finset α), s ∩ s = s
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
/-- Union of two disjoint prepartitions.  -/
BoxIntegral.Prepartition.disjUnion : {ι : Type u_1} →
  {I : BoxIntegral.Box ι} →
    (π₁ π₂ : BoxIntegral.Prepartition I) → Disjoint π₁.iUnion π₂.iUnion → BoxIntegral.Prepartition I
-- Mathlib.Probability.Moments.Covariance
ProbabilityTheory.covariance_fun_sub_left : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X Y Z : Ω → ℝ} {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsFiniteMeasure μ],
  MeasureTheory.MemLp X 2 μ →
    MeasureTheory.MemLp Y 2 μ →
      MeasureTheory.MemLp Z 2 μ →
        ProbabilityTheory.covariance (fun ω => X ω - Y ω) Z μ =
          ProbabilityTheory.covariance X Z μ - ProbabilityTheory.covariance Y Z μ
-- Mathlib.Analysis.InnerProductSpace.LinearPMap
LinearPMap.adjoint_apply_eq : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F] {T : E →ₗ.[𝕜] F}
  [inst_5 : CompleteSpace E],
  Dense ↑T.domain →
    ∀ (y : ↥T.adjoint.domain) {x₀ : E}, (∀ (x : ↥T.domain), inner 𝕜 x₀ ↑x = inner 𝕜 (↑y) (↑T x)) → ↑T.adjoint y = x₀
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.getKey!_ofList_of_mem : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] [inst_4 : Inhabited α]
  {l : List (α × β)} {k k' : α},
  (k == k') = true →
    List.Pairwise (fun a b => (a.1 == b.1) = false) l →
      k ∈ List.map Prod.fst l → (Std.DHashMap.Raw.Const.ofList l).getKey! k' = k
-- Mathlib.CategoryTheory.Monad.Algebra
CategoryTheory.Monad.algebraFunctorOfMonadHom_map_f : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {T₁ T₂ : CategoryTheory.Monad C} (h : T₂ ⟶ T₁)
  {X Y : T₁.Algebra} (f : X ⟶ Y), ((CategoryTheory.Monad.algebraFunctorOfMonadHom h).map f).f = f.f
-- Mathlib.Order.BooleanAlgebra.Set
Set.sdiff_subset : ∀ {α : Type u_1} {s t : Set α}, s \ t ⊆ s
-- Mathlib.Data.ZMod.Basic
ZMod.natAbs_mod_two : ∀ (a : ℤ), ↑a.natAbs = ↑a
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.instIsIsoEqToHom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f f' : X ⟶ Y}
  [inst_1 : CategoryTheory.Limits.HasImage f] [inst_2 : CategoryTheory.Limits.HasImage f'] (h : f = f'),
  CategoryTheory.IsIso (CategoryTheory.Limits.image.eqToHom h)
-- Std.Data.ExtTreeMap.Basic
/-- Tries to retrieve the largest key that is less than the given key,
returning `fallback` if no such key exists.
 -/
Std.ExtTreeMap.getKeyLTD : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtTreeMap α β cmp → α → α → α
-- Mathlib.Geometry.Manifold.ContMDiff.Basic
contMDiffWithinAt_of_notMem : ∀ {𝕜 : 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'] {f : M → M'}
  [inst_11 : Zero M'] {x : M}, x ∉ tsupport f → ∀ (n : WithTop ℕ∞) (s : Set M), ContMDiffWithinAt I I' n f s x
-- Mathlib.Analysis.Calculus.FDeriv.Measurable
measurableSet_of_differentiableAt_of_isComplete_with_param : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [LocallyCompactSpace E] {F : Type u_3} [inst_4 : NormedAddCommGroup F]
  [inst_5 : NormedSpace 𝕜 F] {α : Type u_4} [inst_6 : TopologicalSpace α] {f : α → E → F} [inst_7 : MeasurableSpace α]
  [OpensMeasurableSpace α] [inst_9 : MeasurableSpace E] [OpensMeasurableSpace E],
  Continuous (Function.uncurry f) →
    ∀ {K : Set (E →L[𝕜] F)},
      IsComplete K → MeasurableSet {p | DifferentiableAt 𝕜 (f p.1) p.2 ∧ fderiv 𝕜 (f p.1) p.2 ∈ K}
-- Mathlib.GroupTheory.Perm.Finite
Equiv.Perm.Disjoint.orderOf : ∀ {α : Type u} {σ τ : Equiv.Perm α}, σ.Disjoint τ → orderOf (σ * τ) = (orderOf σ).lcm (orderOf τ)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
add_lt_of_neg_of_lt : ∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α] [AddRightStrictMono α] {a b c : α},
  a < 0 → b < c → a + b < c
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Ico_union_Ici_eq_Ici : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, a ≤ b → Set.Ico a b ∪ Set.Ici b = Set.Ici a
-- Mathlib.RingTheory.FractionalIdeal.Inverse
FractionalIdeal.coe_ideal_span_singleton_inv_mul : ∀ (K : Type u_3) [inst : Field K] {R₁ : Type u_4} [inst_1 : CommRing R₁] [inst_2 : IsDomain R₁] [inst_3 : Algebra R₁ K]
  [inst_4 : IsFractionRing R₁ K] {x : R₁}, x ≠ 0 → (↑(Ideal.span {x}))⁻¹ * ↑(Ideal.span {x}) = 1
-- Mathlib.CategoryTheory.Grothendieck
/-- The Grothendieck construction (often written as `∫ F` in mathematics) for a functor `F : C ⥤ Cat`
gives a category whose
* objects `X` consist of `X.base : C` and `X.fiber : F.obj base`
* morphisms `f : X ⟶ Y` consist of
  `base : X.base ⟶ Y.base` and
  `f.fiber : (F.map base).obj X.fiber ⟶ Y.fiber`
 -/
CategoryTheory.Grothendieck : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.Functor C CategoryTheory.Cat → Type (max u u₂)
-- Mathlib.Analysis.Seminorm
Seminorm.sSup_apply : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  {s : Set (Seminorm 𝕜 E)}, BddAbove s → ∀ {x : E}, (sSup s) x = ⨆ p, ↑p x
-- Mathlib.RingTheory.Radical.Basic
EuclideanDomain.divRadical_ne_zero : ∀ {E : Type u_1} [inst : EuclideanDomain E] [inst_1 : NormalizationMonoid E] [inst_2 : UniqueFactorizationMonoid E]
  {a : E}, a ≠ 0 → EuclideanDomain.divRadical a ≠ 0
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
measurableSet_uIoc : ∀ {α : Type u_1} [inst : TopologicalSpace α] {mα : MeasurableSpace α} [OpensMeasurableSpace α] [inst_2 : LinearOrder α]
  {a b : α} [ClosedIicTopology α], MeasurableSet (Set.uIoc a b)
-- Mathlib.Topology.Algebra.Module.Spaces.PointwiseConvergenceCLM
PointwiseConvergenceCLM.isEmbedding_coeFn : ∀ {𝕜₁ : Type u_4} {𝕜₂ : Type u_5} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) (E : Type u_7)
  (F : Type u_8) [inst_2 : AddCommGroup E] [inst_3 : TopologicalSpace E] [inst_4 : AddCommGroup F]
  [inst_5 : TopologicalSpace F] [inst_6 : IsTopologicalAddGroup F] [inst_7 : Module 𝕜₁ E] [inst_8 : Module 𝕜₂ F],
  Topology.IsEmbedding DFunLike.coe
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.limitIsoOfIsRightKanExtension.eq_1 : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  (F' : CategoryTheory.Functor D H) {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H}
  (α : L.comp F' ⟶ F) [inst_3 : F'.IsRightKanExtension α] [inst_4 : CategoryTheory.Limits.HasLimit F]
  [inst_5 : CategoryTheory.Limits.HasLimit F'],
  F'.limitIsoOfIsRightKanExtension α =
    (CategoryTheory.Limits.limit.isLimit F').conePointUniqueUpToIso
      (F'.isLimitConeOfIsRightKanExtension α (CategoryTheory.Limits.limit.isLimit F))