mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
MeasureTheory.condExpIndL1_smul' : ∀ {α : Type u_1} {F : Type u_2} {𝕜 : Type u_6} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {hm : m ≤ m0}
  [inst_3 : MeasureTheory.SigmaFinite (μ.trim hm)] [inst_4 : NormedSpace ℝ F] [SMulCommClass ℝ 𝕜 F] (c : 𝕜) (x : F),
  MeasureTheory.condExpIndL1 hm μ s (c • x) = c • MeasureTheory.condExpIndL1 hm μ s x
-- Init.Data.Int.Linear
Int.Internal.Linear.Var : Type
-- Mathlib.Analysis.Normed.Operator.Fredholm.Basic
/-- Assume that `u : E →L[𝕜] F` has a continuous quasi-inverse. Then there are closed
subspaces of finite codimensions `E₁` and `F₁` between which `u` induces an isomorphism.

This statement is private because it is superseded by later results: using `isFredholm_tfae`,
you can build a `FredholmPackage` for `u`, and then apply `FredholmPackage.isInvertible_restrict`.
 -/
_private.Mathlib.Analysis.Normed.Operator.Fredholm.Basic.0.ContinuousLinearMap.exists_restrict_isInvertible_of_isQuasiInverse : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : AddCommGroup F] [inst_3 : Module 𝕜 E] [inst_4 : Module 𝕜 F] [inst_5 : TopologicalSpace E]
  [inst_6 : TopologicalSpace F] [T2Space E] [T2Space F] {u : E →L[𝕜] F} {v : F →L[𝕜] E},
  (↑v).IsQuasiInverse ↑u →
    ∃ E₁ F₁,
      IsClosed ↑E₁ ∧ IsClosed ↑F₁ ∧ E₁.CoFG ∧ F₁.CoFG ∧ ∃ (h : Set.MapsTo ⇑u ↑E₁ ↑F₁), (u.restrict h).IsInvertible
-- Mathlib.Topology.PartitionOfUnity
PartitionOfUnity.eventually_finsupport_subset : ∀ {ι : Type u} {X : Type v} [inst : TopologicalSpace X] {s : Set X} (ρ : PartitionOfUnity ι X s) (x₀ : X),
  ∀ᶠ (y : X) in nhds x₀, ρ.finsupport y ⊆ ρ.fintsupport x₀
-- Mathlib.CategoryTheory.Limits.Types.Multiequalizer
CategoryTheory.Limits.Multifork.IsLimit.sectionsEquiv_apply_val : ∀ {J : CategoryTheory.Limits.MulticospanShape} {I : CategoryTheory.Limits.MulticospanIndex J (Type u)}
  {c : CategoryTheory.Limits.Multifork I} (hc : CategoryTheory.Limits.IsLimit c) (s : I.sections) (i : J.L),
  (CategoryTheory.ConcreteCategory.hom (c.ι i)) ((CategoryTheory.Limits.Multifork.IsLimit.sectionsEquiv hc) s) = s.val i
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsLimit.whiskerEquivalenceEquiv.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C}
  {s : CategoryTheory.Limits.Cone F} (e : K ≌ J),
  CategoryTheory.Limits.IsLimit.whiskerEquivalenceEquiv e =
    { toFun := fun h => h.whiskerEquivalence e, invFun := CategoryTheory.Limits.IsLimit.ofWhiskerEquivalence e,
      left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.Data.Matrix.Basic
Matrix.coe_ofLinearEquiv : ∀ {m : Type u_2} {n : Type u_3} (R : Type u_7) {α : Type u_11} [inst : Semiring R] [inst_1 : AddCommMonoid α]
  [inst_2 : Module R α], ⇑(Matrix.ofLinearEquiv R) = ⇑Matrix.of
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.BinaryBicone.op_pt : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {P Q : C} (b : CategoryTheory.Limits.BinaryBicone P Q), b.op.pt = Opposite.op b.pt
-- Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
Subgroup.IsArithmetic.isFiniteRelIndexSL : ∀ (𝒢 : Subgroup (GL (Fin 2) ℝ)) [𝒢.IsArithmetic], 𝒢.IsFiniteRelIndex (Matrix.SpecialLinearGroup.mapGL ℝ).range
-- Mathlib.Analysis.Fourier.FourierTransform
/-- The uniform norm of the Fourier transform of `f` is bounded by the `L¹` norm of `f`.  -/
Fourier.norm_fourierIntegral_le_integral_norm : ∀ {𝕜 : Type u_1} [inst : CommRing 𝕜] [inst_1 : MeasurableSpace 𝕜] {E : Type u_2} [inst_2 : NormedAddCommGroup E]
  [inst_3 : NormedSpace ℂ E] (e : AddChar 𝕜 Circle) (μ : MeasureTheory.Measure 𝕜) (f : 𝕜 → E) (w : 𝕜),
  ‖Fourier.fourierIntegral e μ f w‖ ≤ ∫ (x : 𝕜), ‖f x‖ ∂μ
-- Mathlib.Order.Hom.Basic
instFunLikeOrderIso : (α : Type u_6) → (β : Type u_7) → [inst : LE α] → [inst_1 : LE β] → FunLike (α ≃o β) α β
-- Init.Data.String.PosRaw
String.Pos.Raw.le_of_lt : ∀ {p q : String.Pos.Raw}, p < q → p ≤ q
-- Mathlib.Topology.Algebra.Order.LiminfLimsup
liminf_add_le : ∀ {ι : Type u_1} {α : Type u_2} [inst : AddCommGroup α] [inst_1 : ConditionallyCompleteLinearOrder α] [DenselyOrdered α]
  [AddLeftMono α] {f : Filter ι} [f.NeBot] {u v : ι → α},
  autoParam (Filter.IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f u) liminf_add_le._auto_1 →
    autoParam (Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u) liminf_add_le._auto_3 →
      autoParam (Filter.IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f v) liminf_add_le._auto_5 →
        autoParam (Filter.IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) f v) liminf_add_le._auto_7 →
          Filter.liminf (u + v) f ≤ Filter.limsup u f + Filter.liminf v f
-- Init.Data.ByteArray.Basic
ByteArray.instBEq : BEq ByteArray
-- Mathlib.Algebra.Lie.Cochain
/-- The coboundary operator taking degree 1 cochains to degree 2 cochains.  -/
LieModule.Cohomology.d₁₂ : (R : Type u_1) →
  [inst : CommRing R] →
    (L : Type u_2) →
      [inst_1 : LieRing L] →
        [inst_2 : LieAlgebra R L] →
          (M : Type u_3) →
            [inst_3 : AddCommGroup M] →
              [inst_4 : Module R M] →
                [inst_5 : LieRingModule L M] →
                  [LieModule R L M] →
                    LieModule.Cohomology.oneCochain R L M →ₗ[R] ↥(LieModule.Cohomology.twoCochain R L M)
-- Mathlib.Topology.Algebra.Module.Complement
/-- Two complementary submodules are topological complements if and only if the linear equivalence
`Submodule.prodEquivOfIsCompl` is a homeomorphism.  -/
Submodule.IsCompl.isTopCompl_iff_isHomeomorph_prodEquivOfIsCompl : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] {p q : Submodule R M} [IsTopologicalAddGroup M] (h : IsCompl p q),
  Submodule.IsTopCompl p q ↔ IsHomeomorph ⇑(p.prodEquivOfIsCompl q h)
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.zeroLocus_eq_iff : ∀ {R : Type u} [inst : CommSemiring R] {I J : Ideal R},
  PrimeSpectrum.zeroLocus ↑I = PrimeSpectrum.zeroLocus ↑J ↔ I.radical = J.radical
-- Mathlib.FieldTheory.IsPerfectClosure
/-- If `i : K →+* L` is a homomorphism of characteristic `p` rings, such that
`i` is `p`-radical, and `M` is a perfect ring of characteristic `p`,
then `K →+* M` is in one-to-one correspondence with
`L →+* M`, given by `PerfectRing.lift`. This generalizes `PerfectClosure.lift`.  -/
PerfectRing.liftEquiv : {K : Type u_1} →
  {L : Type u_2} →
    (M : Type u_3) →
      [inst : CommRing K] →
        [inst_1 : CommRing L] →
          [inst_2 : CommRing M] →
            (i : K →+* L) →
              (p : ℕ) →
                [ExpChar M p] →
                  [ExpChar K p] → [PerfectRing M p] → [IsPRadical i p] → [ExpChar L p] → (K →+* M) ≃ (L →+* M)
-- Mathlib.NumberTheory.Chebyshev
Chebyshev.intervalIntegrable_one_div_log_sq : ∀ {a b : ℝ}, 1 < a → 1 < b → IntervalIntegrable (fun x => 1 / Real.log x ^ 2) MeasureTheory.volume a b
-- Mathlib.Order.Filter.Basic
Filter.GenerateSets.below.basic : ∀ {α : Type u} {g : Set (Set α)} {motive : (a : Set α) → Filter.GenerateSets g a → Prop} {s : Set α} (a : s ∈ g),
  Filter.GenerateSets.below ⋯
-- Mathlib.Analysis.Normed.Group.InfiniteSum
tsum_enorm_ne_top_iff_summable_norm : ∀ {E : Type u_3} [inst : SeminormedAddCommGroup E] {ι : Type u_6} {f : ι → E},
  ∑' (i : ι), ‖f i‖ₑ ≠ ⊤ ↔ Summable fun i => ‖f i‖
-- Init.Data.Int.DivMod.Lemmas
Int.emod_natAbs_of_nonneg : ∀ {x : ℤ}, 0 ≤ x → ∀ {n : ℕ}, x.natAbs % n = (x % ↑n).toNat
-- Mathlib.Analysis.Normed.Algebra.Exponential
Pi.exp_def : ∀ {ι : Type u_3} {𝔸 : ι → Type u_4} [Finite ι] [inst : (i : ι) → NormedRing (𝔸 i)] [(i : ι) → NormedAlgebra ℚ (𝔸 i)]
  [∀ (i : ι), CompleteSpace (𝔸 i)] (x : (i : ι) → 𝔸 i), NormedSpace.exp x = fun i => NormedSpace.exp (x i)
-- Batteries.Logic
/-- **Alias** of `congrArg₂`. -/
congr_arg₂ : ∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (f : α → β → γ) {x x' : α} {y y' : β}, x = x' → y = y' → f x y = f x' y'
-- Lean.Elab.MutualInductive
Lean.Elab.Command.InductiveElabStep1.mk.injEq : ∀ (view : Lean.Elab.Command.InductiveView)
  (elabCtors :
    Array Lean.Elab.Command.ElabHeaderResult →
      Lean.Elab.Command.ElabHeaderResult → Array Lean.Expr → Lean.Elab.TermElabM Lean.Elab.Command.InductiveElabStep2)
  (view_1 : Lean.Elab.Command.InductiveView)
  (elabCtors_1 :
    Array Lean.Elab.Command.ElabHeaderResult →
      Lean.Elab.Command.ElabHeaderResult → Array Lean.Expr → Lean.Elab.TermElabM Lean.Elab.Command.InductiveElabStep2),
  ({ view := view, elabCtors := elabCtors } = { view := view_1, elabCtors := elabCtors_1 }) =
    (view = view_1 ∧ elabCtors = elabCtors_1)
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.prod_apply : ∀ {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} {V3 : Type u_6} {P3 : Type u_7}
  [inst : Ring k] [inst_1 : AddCommGroup V1] [inst_2 : Module k V1] [inst_3 : AddTorsor V1 P1]
  [inst_4 : AddCommGroup V2] [inst_5 : Module k V2] [inst_6 : AddTorsor V2 P2] [inst_7 : AddCommGroup V3]
  [inst_8 : Module k V3] [inst_9 : AddTorsor V3 P3] (f : P1 →ᵃ[k] P2) (g : P1 →ᵃ[k] P3) (p : P1),
  (f.prod g) p = (f p, g p)
-- Mathlib.Algebra.Order.Floor.Div
smul_floorDiv_le : ∀ {α : Type u_2} {β : Type u_3} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [inst_2 : AddCommMonoid β]
  [inst_3 : PartialOrder β] [inst_4 : SMulZeroClass α β] [inst_5 : FloorDiv α β] {a : α} {b : β},
  0 < a → a • (b ⌊/⌋ a) ≤ b
-- Mathlib.Topology.UniformSpace.UniformEmbedding
IsUniformEmbedding.comp : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : UniformSpace α] [inst_1 : UniformSpace β] [inst_2 : UniformSpace γ]
  {g : β → γ}, IsUniformEmbedding g → ∀ {f : α → β}, IsUniformEmbedding f → IsUniformEmbedding (g ∘ f)
-- Init.Data.BitVec.Lemmas
BitVec.toNat_cpop_setWidth_eq_of_le : ∀ {w : ℕ} {x : BitVec w} {n : ℕ}, w ≤ n → (BitVec.setWidth n x).cpop.toNat = x.cpop.toNat
-- Init.GetElem
getElem!_pos : ∀ {cont : Type u_1} {idx : Type u_2} {elem : Type u_3} {dom : cont → idx → Prop} [inst : GetElem? cont idx elem dom]
  [LawfulGetElem cont idx elem dom] [inst_2 : Inhabited elem] (c : cont) (i : idx) (h : dom c i), c[i]! = c[i]
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.LocallyFree
SheafOfModules.LocalGeneratorsData.quasiCoherentData_localGeneratorsData : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : ∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat]
  [inst_2 : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R}
  (q : M.LocalGeneratorsData) [inst_3 : q.IsLocallyFreeData], q.quasiCoherentData.localGeneratorsData = q
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
Finsupp.prod_indicator_index : ∀ {α : Type u_1} {M : Type u_8} {N : Type u_10} [inst : Zero M] [inst_1 : CommMonoid N] {s : Finset α} (f : α → M)
  {h : α → M → N}, (∀ a ∈ s, h a 0 = 1) → (Finsupp.indicator s fun x x_1 => f x).prod h = ∏ x ∈ s, h x (f x)
-- Init.Internal.Order.Basic
Lean.Order.PProd.fst : {α : Sort u} →
  {β : Sort v} → [Lean.Order.CompleteLattice α] → [Lean.Order.CompleteLattice β] → (α ×' β → Prop) → α → Prop
-- Mathlib.NumberTheory.Padics.Hensel
_private.Mathlib.NumberTheory.Padics.Hensel.0.deriv_sq_norm_ne_zero : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {R : Type u_1} [inst_1 : CommSemiring R] [inst_2 : Algebra R ℤ_[p]]
  {F : Polynomial R} {a : ℤ_[p]},
  ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2 →
    ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2 ≠ 0
-- Mathlib.LinearAlgebra.Multilinear.Curry
MultilinearMap.curryRight_apply : ∀ {R : Type uR} {n : ℕ} {M : Fin n.succ → Type v} {M₂ : Type v₂} [inst : CommSemiring R]
  [inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)] [inst_2 : AddCommMonoid M₂]
  [inst_3 : (i : Fin n.succ) → Module R (M i)] [inst_4 : Module R M₂] (f : MultilinearMap R M M₂)
  (m : (i : Fin n) → M i.castSucc) (x : M (Fin.last n)), (f.curryRight m) x = f (Fin.snoc m x)
-- Mathlib.Order.SuccPred.Limit
SuccOrder.prelimitRecOn_of_isSuccPrelimit : ∀ {α : Type u_1} {b : α} {motive : α → Sort u_2} [inst : PartialOrder α] [inst_1 : SuccOrder α]
  [inst_2 : WellFoundedLT α] (succ : (a : α) → ¬IsMax a → motive a → motive (Order.succ a))
  (isSuccPrelimit : (a : α) → Order.IsSuccPrelimit a → ((b : α) → b < a → motive b) → motive a)
  (hb : Order.IsSuccPrelimit b),
  SuccOrder.prelimitRecOn b succ isSuccPrelimit =
    isSuccPrelimit b hb fun x x_1 => SuccOrder.prelimitRecOn x succ isSuccPrelimit
-- Mathlib.Algebra.BigOperators.Expect
/-- * `𝔼 i ∈ s, f i` is notation for `Finset.expect s f`. It is the expectation of `f i` where `i`
  ranges over the finite set `s` (either a `Finset` or a `Set` with a `Fintype` instance).
* `𝔼 i, f i` is notation for `Finset.expect Finset.univ f`. It is the expectation of `f i` where `i`
  ranges over the finite domain of `f`.
* `𝔼 i ∈ s with p i, f i` is notation for `Finset.expect (Finset.filter p s) f`.
* `𝔼 (i ∈ s) (j ∈ t), f i j` is notation for `Finset.expect (s ×ˢ t) (fun ⟨i, j⟩ ↦ f i j)`.

These support destructuring, for example `𝔼 ⟨i, j⟩ ∈ s ×ˢ t, f i j`.

Notation: `"𝔼" bigOpBinders* ("with" term)? "," term`  -/
BigOperators.bigexpect : Lean.ParserDescr
-- Mathlib.CategoryTheory.Monoidal.CommComon_
CategoryTheory.CommComon.forget₂Comon_obj_comon : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (A : CategoryTheory.CommComon C),
  ((CategoryTheory.CommComon.forget₂Comon C).obj A).comon = A.comon
-- Mathlib.Order.Category.BddOrd
BddOrd.id_apply : ∀ (X : BddOrd) (x : ↑X.toPartOrd), (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) x = x
-- Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
UniformConvergenceCLM.hasBasis_nhds_zero : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {E : Type u_3}
  (F : Type u_4) [inst_2 : AddCommGroup E] [inst_3 : Module 𝕜₁ E] [inst_4 : TopologicalSpace E]
  [inst_5 : AddCommGroup F] [inst_6 : Module 𝕜₂ F] [inst_7 : TopologicalSpace F] [inst_8 : IsTopologicalAddGroup F]
  (𝔖 : Set (Set E)),
  𝔖.Nonempty →
    DirectedOn (fun x1 x2 => x1 ⊆ x2) 𝔖 →
      (nhds 0).HasBasis (fun SV => SV.1 ∈ 𝔖 ∧ SV.2 ∈ nhds 0) fun SV => {f | ∀ x ∈ SV.1, f x ∈ SV.2}
-- Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular
Matrix.isTotallyUnimodular_iff : ∀ {m : Type u_1} {n : Type u_3} {R : Type u_5} [inst : CommRing R] (A : Matrix m n R),
  A.IsTotallyUnimodular ↔ ∀ (k : ℕ) (f : Fin k → m) (g : Fin k → n), (A.submatrix f g).det ∈ Set.range SignType.cast
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.coe_pi : ∀ {ι : Type u_4} {M : ι → Type u_5} [inst : (i : ι) → MulOneClass (M i)] (I : Set ι) (S : (i : ι) → Submonoid (M i)),
  ↑(Submonoid.pi I S) = I.pi fun i => ↑(S i)
-- Mathlib.CategoryTheory.Dialectica.Monoidal
_private.Mathlib.CategoryTheory.Dialectica.Monoidal.0.CategoryTheory.Dial.termπ₂ : Lean.ParserDescr
-- Mathlib.GroupTheory.Congruence.Defs
Con.liftOn₂.eq_1 : ∀ {M : Type u_1} [inst : Mul M] {β : Sort u_4} {c : Con M} (q r : c.Quotient) (f : M → M → β)
  (h : ∀ (a₁ a₂ b₁ b₂ : M), c a₁ b₁ → c a₂ b₂ → f a₁ a₂ = f b₁ b₂), Con.liftOn₂ q r f h = Quotient.liftOn₂' q r f h
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
/-- The inverse map of a homeomorphism is a continuous function.  -/
ContinuousAddEquiv.continuous_invFun : ∀ {G : Type u} [inst : TopologicalSpace G] {H : Type v} [inst_1 : TopologicalSpace H] [inst_2 : Add G] [inst_3 : Add H]
  (self : G ≃ₜ+ H), Continuous self.invFun
-- Mathlib.Order.Atoms
OrderEmbedding.isAtom_of_map_bot_of_image : ∀ {α : Type u_2} {β : Type u_3} [inst : PartialOrder α] [inst_1 : PartialOrder β] [inst_2 : OrderBot α]
  [inst_3 : OrderBot β] (f : β ↪o α), f ⊥ = ⊥ → ∀ {b : β}, IsAtom (f b) → IsAtom b
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.FundamentalGroup
/-- Get an isomorphism between the fundamental groups at two points given a path  -/
FundamentalGroup.fundamentalGroupMulEquivOfPath : {X : Type u_1} → [inst : TopologicalSpace X] → {x₀ x₁ : X} → Path x₀ x₁ → FundamentalGroup X x₀ ≃* FundamentalGroup X x₁
-- Mathlib.Algebra.Homology.ComplexShape
/-- The complex shape where only differentials from each `X.i` to itself are allowed.

This is mostly only useful so we can describe the relation of "related in `k` steps" below.
 -/
ComplexShape.refl : (ι : Type u_2) → ComplexShape ι
-- Mathlib.LinearAlgebra.DirectSum.Finsupp
finsuppTensorFinsuppRid_symm_single_smul : ∀ (R : Type u_1) (M : Type u_3) (ι : Type u_5) (κ : Type u_6) [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] (i : ι × κ) (m : M) (r : R),
  ((finsuppTensorFinsuppRid R M ι κ).symm fun₀ | i => r • m) = (fun₀ | i.1 => m) ⊗ₜ[R] fun₀ | i.2 => r
-- Mathlib.CategoryTheory.Monad.Basic
CategoryTheory.Monad.mk.injEq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (toFunctor : CategoryTheory.Functor C C)
  (η : CategoryTheory.Functor.id C ⟶ toFunctor) (μ : toFunctor.comp toFunctor ⟶ toFunctor)
  (assoc :
    autoParam
      (∀ (X : C),
        CategoryTheory.CategoryStruct.comp (toFunctor.map (μ.app X)) (μ.app X) =
          CategoryTheory.CategoryStruct.comp (μ.app (toFunctor.obj X)) (μ.app X))
      CategoryTheory.Monad.assoc._autoParam)
  (left_unit :
    autoParam
      (∀ (X : C),
        CategoryTheory.CategoryStruct.comp (η.app (toFunctor.obj X)) (μ.app X) =
          CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.id C).obj (toFunctor.obj X)))
      CategoryTheory.Monad.left_unit._autoParam)
  (right_unit :
    autoParam
      (∀ (X : C),
        CategoryTheory.CategoryStruct.comp (toFunctor.map (η.app X)) (μ.app X) =
          CategoryTheory.CategoryStruct.id (toFunctor.obj ((CategoryTheory.Functor.id C).obj X)))
      CategoryTheory.Monad.right_unit._autoParam)
  (toFunctor_1 : CategoryTheory.Functor C C) (η_1 : CategoryTheory.Functor.id C ⟶ toFunctor_1)
  (μ_1 : toFunctor_1.comp toFunctor_1 ⟶ toFunctor_1)
  (assoc_1 :
    autoParam
      (∀ (X : C),
        CategoryTheory.CategoryStruct.comp (toFunctor_1.map (μ_1.app X)) (μ_1.app X) =
          CategoryTheory.CategoryStruct.comp (μ_1.app (toFunctor_1.obj X)) (μ_1.app X))
      CategoryTheory.Monad.assoc._autoParam)
  (left_unit_1 :
    autoParam
      (∀ (X : C),
        CategoryTheory.CategoryStruct.comp (η_1.app (toFunctor_1.obj X)) (μ_1.app X) =
          CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.id C).obj (toFunctor_1.obj X)))
      CategoryTheory.Monad.left_unit._autoParam)
  (right_unit_1 :
    autoParam
      (∀ (X : C),
        CategoryTheory.CategoryStruct.comp (toFunctor_1.map (η_1.app X)) (μ_1.app X) =
          CategoryTheory.CategoryStruct.id (toFunctor_1.obj ((CategoryTheory.Functor.id C).obj X)))
      CategoryTheory.Monad.right_unit._autoParam),
  ({ toFunctor := toFunctor, η := η, μ := μ, assoc := assoc, left_unit := left_unit, right_unit := right_unit } =
      { toFunctor := toFunctor_1, η := η_1, μ := μ_1, assoc := assoc_1, left_unit := left_unit_1,
        right_unit := right_unit_1 }) =
    (toFunctor = toFunctor_1 ∧ η ≍ η_1 ∧ μ ≍ μ_1)
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.Zip
_private.Std.Data.Iterators.Lemmas.Combinators.Monadic.Zip.0.Std.Iterators.Types.Zip.instIterator.match_1.eq_3 : ∀ {m : Type u_1 → Type u_2} {α₁ β₁ : Type u_1} [inst : Std.Iterator α₁ m β₁] {α₂ β₂ : Type u_1}
  (it : Std.IterM m (β₁ × β₂)) (motive : it.internalState.left.Step → Sort u_3)
  (hp : it.internalState.left.IsPlausibleStep Std.IterStep.done)
  (h_1 :
    (it₁' : Std.IterM m β₁) →
      (out : β₁) →
        (hp : it.internalState.left.IsPlausibleStep (Std.IterStep.yield it₁' out)) →
          motive ⟨Std.IterStep.yield it₁' out, hp⟩)
  (h_2 :
    (it₁' : Std.IterM m β₁) →
      (hp : it.internalState.left.IsPlausibleStep (Std.IterStep.skip it₁')) → motive ⟨Std.IterStep.skip it₁', hp⟩)
  (h_3 : (hp : it.internalState.left.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, hp⟩),
  (match ⟨Std.IterStep.done, hp⟩ with
    | ⟨Std.IterStep.yield it₁' out, hp⟩ => h_1 it₁' out hp
    | ⟨Std.IterStep.skip it₁', hp⟩ => h_2 it₁' hp
    | ⟨Std.IterStep.done, hp⟩ => h_3 hp) =
    h_3 hp
-- Mathlib.Algebra.Order.GroupWithZero.Defs
PosMulMono.mk : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α],
  (∀ ⦃a : α⦄, 0 ≤ a → ∀ ⦃b c : α⦄, b ≤ c → a * b ≤ a * c) → PosMulMono α
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
MeasureTheory.integrable_iff_integrableAtFilter_atBot_atTop : ∀ {X : Type u_1} {ε'' : Type u_5} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X]
  [inst_2 : TopologicalSpace ε''] [inst_3 : ESeminormedAddMonoid ε''] {μ : MeasureTheory.Measure X}
  [TopologicalSpace.PseudoMetrizableSpace ε''] {f : X → ε''} [inst_5 : LinearOrder X] [CompactIccSpace X],
  MeasureTheory.Integrable f μ ↔
    (MeasureTheory.IntegrableAtFilter f Filter.atBot μ ∧ MeasureTheory.IntegrableAtFilter f Filter.atTop μ) ∧
      MeasureTheory.LocallyIntegrable f μ
-- Mathlib.Analysis.Normed.Module.Dual
LinearMap.polar_AbsConvex : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : AddCommMonoid E] [inst_2 : AddCommMonoid F]
  [inst_3 : Module 𝕜 E] [inst_4 : Module 𝕜 F] {B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜} (s : Set E), AbsConvex 𝕜 (B.polar s)
-- Mathlib.Algebra.Order.Monoid.Canonical.Defs
/-- An ordered monoid is `CanonicallyOrderedMul`
if the ordering coincides with the divisibility relation,
which is to say, `a ≤ b` iff there exists `c` with `b = a * c`.
Examples seem rare; it seems more likely that the `OrderDual`
of a naturally-occurring lattice satisfies this than the lattice
itself (for example, dual of the lattice of ideals of a PID or
Dedekind domain satisfy this; collections of all things ≤ 1 seem to
be more natural that collections of all things ≥ 1).  -/
CanonicallyOrderedMul : (α : Type u_1) → [Mul α] → [LE α] → Prop
-- Mathlib.MeasureTheory.Integral.CircleAverage
/-- Circle averages commute with sums.  -/
Real.circleAverage_sum : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {c : ℂ} {R : ℝ} {ι : Type u_4} {s : Finset ι}
  {f : ι → ℂ → E},
  (∀ i ∈ s, CircleIntegrable (f i) c R) → Real.circleAverage (∑ i ∈ s, f i) c R = ∑ i ∈ s, Real.circleAverage (f i) c R
-- Mathlib.CategoryTheory.Comma.Over.OverClass
/-- The structure morphism `X ↘ S : X ⟶ S` given `OverClass X S`.
The instance argument is an `optParam` instead so that it appears in the discrimination tree.
 -/
CategoryTheory.over : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (X S : C) → autoParam (CategoryTheory.OverClass X S) CategoryTheory.over._auto_1 → (X ⟶ S)
-- Mathlib.LinearAlgebra.Matrix.Hermitian
Matrix.schur_complement_eq₁₁ : ∀ {α : Type u_1} {m : Type u_3} {n : Type u_4} [inst : CommRing α] [inst_1 : StarRing α] [inst_2 : Fintype m]
  [inst_3 : DecidableEq m] [inst_4 : Fintype n] {A : Matrix m m α} (B : Matrix m n α) (D : Matrix n n α) (x : m → α)
  (y : n → α) [Invertible A],
  A.IsHermitian →
    Matrix.vecMul (star (Sum.elim x y)) (Matrix.fromBlocks A B B.conjTranspose D) ⬝ᵥ Sum.elim x y =
      Matrix.vecMul (star (x + (A⁻¹ * B).mulVec y)) A ⬝ᵥ (x + (A⁻¹ * B).mulVec y) +
        Matrix.vecMul (star y) (D - B.conjTranspose * A⁻¹ * B) ⬝ᵥ y
-- Init.Data.Range.Polymorphic.SInt
_private.Init.Data.Range.Polymorphic.SInt.0.Int64.minValueSealed : Int64
-- Mathlib.Topology.Convenient.Category
/-- The counit of the adjunction `GeneratedByTopCat.adj` between
the categories `GeneratedByTopCat X` and `TopCat`.  -/
GeneratedByTopCat.adjCounit : {ι : Type t} →
  {X : ι → Type u} →
    [inst : (i : ι) → TopologicalSpace (X i)] →
      TopCat.toGeneratedByTopCat.comp GeneratedByTopCat.toTopCat ⟶ CategoryTheory.Functor.id TopCat
-- Mathlib.Data.Nat.BinaryRec
/-- The same as `binaryRec`, but the induction step can assume that if `n=0`,
the bit being appended is `true`  -/
Nat.binaryRec' : {motive : ℕ → Sort u} →
  motive 0 → ((b : Bool) → (n : ℕ) → (n = 0 → b = true) → motive n → motive (Nat.bit b n)) → (n : ℕ) → motive n