mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RepresentationTheory.Subrepresentation
/-- An order-preserving equivalence between `A[G]`-submodules of an `A[G]`-module M and
subrepresentations of `ρ`.  -/
Subrepresentation.submoduleSubrepresentationOrderIso : {A : Type u_1} →
  {G : Type u_2} →
    {M : Type u_4} →
      [inst : CommSemiring A] →
        [inst_1 : Monoid G] →
          [inst_2 : AddCommMonoid M] →
            [inst_3 : Module (MonoidAlgebra A G) M] →
              Submodule (MonoidAlgebra A G) M ≃o Subrepresentation (Representation.ofModule M)
-- Mathlib.Tactic.Positivity.Core
Mathlib.Meta.Positivity.Strictness.nonzero.sizeOf_spec : ∀ {u : Lean.Level} {α : Q(Type u)} {zα : Q(Zero «$α»)} {e : Q(«$α»)} {pα? : Option Q(PartialOrder «$α»)}
  (pf : Q(«$e» ≠ 0)), sizeOf (Mathlib.Meta.Positivity.Strictness.nonzero pf) = 1 + sizeOf pα? + sizeOf pf
-- Mathlib.Algebra.BigOperators.Group.Finset.Powerset
/-- A sum over `powerset s` is equal to the double sum over sets of subsets of `s`
with `#s = k`, for `k = 0, ..., #s`  -/
Finset.sum_powerset : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid β] (s : Finset α) (f : Finset α → β),
  ∑ t ∈ s.powerset, f t = ∑ j ∈ Finset.range (s.card + 1), ∑ t ∈ Finset.powersetCard j s, f t
-- Mathlib.Analysis.Normed.Group.FunctionSeries
/-- An infinite sum of functions with summable sup norm is the uniform limit of its partial sums.
Version relative to a set, with index set `ℕ`.  -/
tendstoUniformlyOn_tsum_nat : ∀ {β : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup F] [CompleteSpace F] {f : ℕ → β → F} {u : ℕ → ℝ},
  Summable u →
    ∀ {s : Set β},
      (∀ (n : ℕ), ∀ x ∈ s, ‖f n x‖ ≤ u n) →
        TendstoUniformlyOn (fun N x => ∑ n ∈ Finset.range N, f n x) (fun x => ∑' (n : ℕ), f n x) Filter.atTop s
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.contains_minKey : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → ∀ {he : t.isEmpty = false}, Std.DTreeMap.Internal.Impl.contains (t.minKey he) t = true
-- Mathlib.Algebra.Ring.GeomSum
Commute.geom_sum₂_Ico_mul : ∀ {R : Type u_1} [inst : Ring R] {x y : R},
  Commute x y →
    ∀ {m n : ℕ}, m ≤ n → (∑ i ∈ Finset.Ico m n, x ^ i * y ^ (n - 1 - i)) * (x - y) = x ^ n - y ^ (n - m) * x ^ m
-- Mathlib.RingTheory.LittleWedderburn
/-- **Alias** of `littleWedderburn`.

---

A finite division ring is a field. See `Finite.isDomain_to_isField` and
`Fintype.divisionRingOfIsDomain` for more general statements, but these create data, and therefore
may cause diamonds if used improperly.  -/
Finite.divisionRing_to_field : (D : Type u_1) → [DivisionRing D] → [Finite D] → Field D
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.LeftHomologyData.leftHomologyIso_hom_naturality_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} [inst_2 : S₁.HasHomology] [inst_3 : S₂.HasHomology] (φ : S₁ ⟶ S₂)
  (h₁ : S₁.LeftHomologyData) (h₂ : S₂.LeftHomologyData) {Z : C} (h : h₂.H ⟶ Z),
  CategoryTheory.CategoryStruct.comp h₁.homologyIso.hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftHomologyMap' φ h₁ h₂) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyMap φ)
      (CategoryTheory.CategoryStruct.comp h₂.homologyIso.hom h)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
CategoryTheory.Limits.cospanExt_hom_app_one : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z X' Y' Z' : C} (iX : X ≅ X') (iY : Y ≅ Y') (iZ : Z ≅ Z')
  {f : X ⟶ Z} {g : Y ⟶ Z} {f' : X' ⟶ Z'} {g' : Y' ⟶ Z'}
  (wf : CategoryTheory.CategoryStruct.comp iX.hom f' = CategoryTheory.CategoryStruct.comp f iZ.hom)
  (wg : CategoryTheory.CategoryStruct.comp iY.hom g' = CategoryTheory.CategoryStruct.comp g iZ.hom),
  (CategoryTheory.Limits.cospanExt iX iY iZ wf wg).hom.app CategoryTheory.Limits.WalkingCospan.one = iZ.hom
-- Mathlib.AlgebraicGeometry.QuasiAffine
AlgebraicGeometry.Scheme.IsQuasiAffine.isBasis_basicOpen : ∀ (X : AlgebraicGeometry.Scheme) [X.IsQuasiAffine],
  TopologicalSpace.Opens.IsBasis {x | ∃ r, ∃ (_ : AlgebraicGeometry.IsAffineOpen (X.basicOpen r)), X.basicOpen r = x}
-- Mathlib.Order.Closure
ClosureOperator.closure_inf_le : ∀ {α : Type u_1} [inst : SemilatticeInf α] (c : ClosureOperator α) (x y : α), c (x ⊓ y) ≤ c x ⊓ c y
-- Std.Data.HashMap.Lemmas
Std.HashMap.toList_filterMap : ∀ {α : Type u} {β : Type v} {γ : Type w} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} {f : α → β → Option γ},
  (Std.HashMap.filterMap f m).toList.Perm
    (List.filterMap (fun p => Option.map (fun x => (p.1, x)) (f p.1 p.2)) m.toList)
-- Mathlib.Analysis.Calculus.FDeriv.Add
HasFDerivAt.const_smul : ∀ {𝕜 : 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] {f : E → F}
  {f' : E →L[𝕜] F} {x : E} {R : Type u_4} [inst_5 : Monoid R] [inst_6 : DistribMulAction R F]
  [inst_7 : SMulCommClass 𝕜 R F] [inst_8 : ContinuousConstSMul R F],
  HasFDerivAt f f' x → ∀ (c : R), HasFDerivAt (c • f) (c • f') x
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Measure.ofMeasurable_zero : ∀ {α : Type u_1} {m0 : MeasurableSpace α}, MeasureTheory.Measure.ofMeasurable (fun x x_1 => 0) ⋯ ⋯ = 0
-- Lean.Data.PersistentHashMap
Lean.PersistentHashMap.isEmpty : {α : Type u_1} → {β : Type u_2} → {x : BEq α} → {x_1 : Hashable α} → Lean.PersistentHashMap α β → Bool
-- Mathlib.Data.Rat.Defs
/-- A version of `Rat.casesOn` that uses `/` instead of `Rat.mk'`. Use as
```lean
cases r with
| div p q nonzero coprime =>
```
 -/
Rat.divCasesOn : {C : ℚ → Sort u_1} → (a : ℚ) → ((n : ℤ) → (d : ℕ) → d ≠ 0 → n.natAbs.Coprime d → C (↑n / ↑d)) → C a
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.union_smul : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : SMul α β] {s₁ s₂ : Finset α} {t : Finset β}
  [inst_2 : DecidableEq α], (s₁ ∪ s₂) • t = s₁ • t ∪ s₂ • t
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomMulAct.instDivisionMonoidOfMulOpposite : {M : Type u_1} → [DivisionMonoid Mᵐᵒᵖ] → DivisionMonoid Mᵈᵐᵃ
-- Mathlib.Order.Category.DistLat
DistLat.ofHom_comp : ∀ {X Y Z : Type u} [inst : DistribLattice X] [inst_1 : DistribLattice Y] [inst_2 : DistribLattice Z]
  (f : LatticeHom X Y) (g : LatticeHom Y Z),
  DistLat.ofHom (g.comp f) = CategoryTheory.CategoryStruct.comp (DistLat.ofHom f) (DistLat.ofHom g)
-- Std.Http.Data.Body.Full
/-- Non-blocking receive. `Full` bodies are always in-memory, so data is always
immediately available. Returns `some chunk` on first call, `some none` (EOF)
once consumed or closed.
 -/
Std.Http.Body.Full.tryRecv : Std.Http.Body.Full → Std.Async.Async (Option (Option Std.Http.Chunk))
-- Mathlib.Algebra.Ring.Equiv
/-- If a ring homomorphism has an inverse, it is a ring isomorphism.  -/
RingEquiv.ofRingHom : {R : Type u_4} →
  {S : Type u_5} →
    [inst : NonAssocSemiring R] →
      [inst_1 : NonAssocSemiring S] →
        (f : R →+* S) → (g : S →+* R) → f.comp g = RingHom.id S → g.comp f = RingHom.id R → R ≃+* S
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Matrix.submatrixEquivInvertibleEquivInvertible_apply : ∀ {m : Type u} {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α]
  [inst_3 : Fintype m] [inst_4 : DecidableEq m] (A : Matrix m m α) (e₁ e₂ : n ≃ m)
  (x : Invertible (A.submatrix ⇑e₁ ⇑e₂)),
  (A.submatrixEquivInvertibleEquivInvertible e₁ e₂) x = A.invertibleOfSubmatrixEquivInvertible e₁ e₂
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Submonoid.LocalizationMap.sec.eq_1 : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N]
  (f : S.LocalizationMap N) (z : N), f.sec z = Classical.choose ⋯
-- Mathlib.Probability.Independence.Process.HasIndepIncrements.IsGaussianProcess
/-- Given a finite set `I : Finset T` of cardinality `n`,
`I.orderEmbOfFinWithBot : Fin (#I + 1) → T` is the map `(⊥, t₁, ..., tₙ)`,
where `t₁ < ... < tₙ` are the elements of `I` and `⊥` is the smallest element of `T`.  -/
_private.Mathlib.Probability.Independence.Process.HasIndepIncrements.IsGaussianProcess.0.Finset.orderEmbOfFinWithBot : {T : Type u_1} → [LinearOrder T] → (I : Finset T) → [Bot T] → Fin (I.card + 1) → T
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.ofList_eq_insertMany_empty : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {l : List ((a : α) × β a)},
  Std.DTreeMap.Raw.ofList l cmp = ∅.insertMany l
-- Init.Data.UInt.Basic
UInt32.modn : UInt32 → ℕ → UInt32
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Pullback
PresheafOfModules.pullback_id_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {R : CategoryTheory.Functor Dᵒᵖ RingCat} {S : CategoryTheory.Functor Cᵒᵖ RingCat}
  (φ : S ⟶ F.op.comp R) [inst_2 : (PresheafOfModules.pushforward φ).IsRightAdjoint],
  PresheafOfModules.pullbackComp (CategoryTheory.CategoryStruct.id S) φ =
    CategoryTheory.Functor.isoWhiskerRight (PresheafOfModules.pullbackId S) (PresheafOfModules.pullback φ) ≪≫
      (PresheafOfModules.pullback φ).leftUnitor
-- Mathlib.Algebra.Group.Subgroup.Lattice
AddSubgroup.eq_bot_iff_forall : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G), H = ⊥ ↔ ∀ x ∈ H, x = 0
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding_injective : ∀ (K : Type u_1) [inst : Field K] [NumberField K], Function.Injective ⇑(NumberField.mixedEmbedding K)
-- Init.Data.Order.Lemmas
Std.le_iff_lt_or_eq : ∀ {α : Type u_1} [inst : LE α] [inst_1 : LT α] [Std.LawfulOrderLT α] [Std.IsPartialOrder α] {a b : α},
  a ≤ b ↔ a < b ∨ a = b
-- Mathlib.Analysis.Analytic.Constructions
HasFPowerSeriesAt.const_smul : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {pf : FormalMultilinearSeries 𝕜 E F} {x : E} {R : Type u_9} [inst_5 : NormedRing R] [inst_6 : Module R F]
  [inst_7 : IsBoundedSMul R F] [inst_8 : SMulCommClass 𝕜 R F] {c : R},
  HasFPowerSeriesAt f pf x → HasFPowerSeriesAt (c • f) (c • pf) x
-- Mathlib.CategoryTheory.Adjunction.Lifting.Left
CategoryTheory.LiftLeftAdjoint.otherMap.eq_1 : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  {U : CategoryTheory.Functor B C} {F : CategoryTheory.Functor C B} (R : CategoryTheory.Functor A B)
  (F' : CategoryTheory.Functor C A) (adj₁ : F ⊣ U) (adj₂ : F' ⊣ R.comp U) (X : B),
  CategoryTheory.LiftLeftAdjoint.otherMap R F' adj₁ adj₂ X =
    CategoryTheory.CategoryStruct.comp
      (F'.map
        (U.map
          (CategoryTheory.CategoryStruct.comp (F.map (adj₂.unit.app (U.1 X)))
            (adj₁.counit.app (R.obj (F'.obj (U.1 X)))))))
      (adj₂.counit.app (F'.obj (U.1 X)))
-- Mathlib.RingTheory.Valuation.Basic
Valuation.comap_comp : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀)
  {S₁ : Type u_7} {S₂ : Type u_8} [inst_2 : Ring S₁] [inst_3 : Ring S₂] (f : S₁ →+* S₂) (g : S₂ →+* R),
  Valuation.comap (g.comp f) v = Valuation.comap f (Valuation.comap g v)
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous
/-- The pushforward functor by the identity morphism identifies to
the identify functor of the category of sheaves of modules.  -/
SheafOfModules.pushforwardId : {D : Type u₂} →
  [inst : CategoryTheory.Category.{v₂, u₂} D] →
    {K : CategoryTheory.GrothendieckTopology D} →
      (R : CategoryTheory.Sheaf K RingCat) →
        SheafOfModules.pushforward (CategoryTheory.CategoryStruct.id R) ≅ CategoryTheory.Functor.id (SheafOfModules R)
-- Mathlib.CategoryTheory.Subobject.Basic
CategoryTheory.Subobject.isoOfMkEq_inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {B A : C} (f : A ⟶ B) [inst_1 : CategoryTheory.Mono f]
  (X : CategoryTheory.Subobject B) (h : CategoryTheory.Subobject.mk f = X),
  (CategoryTheory.Subobject.isoOfMkEq f X h).inv = X.ofLEMk f ⋯
-- Mathlib.MeasureTheory.Group.Integral
MeasureTheory.integral_vadd_eq_self : ∀ {α : Type u_3} {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {G : Type u_7}
  [inst_2 : AddGroup G] [inst_3 : MeasurableSpace α] [inst_4 : AddAction G α] [MeasurableConstVAdd G α]
  {μ : MeasureTheory.Measure α} [MeasureTheory.VAddInvariantMeasure G α μ] (f : α → E) {g : G},
  ∫ (x : α), f (g +ᵥ x) ∂μ = ∫ (x : α), f x ∂μ
-- Mathlib.Analysis.InnerProductSpace.Basic
real_inner_self_nonpos : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] {x : F}, inner ℝ x x ≤ 0 ↔ x = 0
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.isomorphisms.infer_property : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [hf : CategoryTheory.IsIso f],
  CategoryTheory.MorphismProperty.isomorphisms C f
-- Mathlib.Order.Interval.Finset.Defs
LocallyFiniteOrderTop.mk : {α : Type u_1} →
  [inst : Preorder α] →
    (finsetIoi finsetIci : α → Finset α) →
      (∀ (a x : α), x ∈ finsetIci a ↔ a ≤ x) → (∀ (a x : α), x ∈ finsetIoi a ↔ a < x) → LocallyFiniteOrderTop α
-- Mathlib.Data.Nat.Digits.Defs
_private.Mathlib.Data.Nat.Digits.Defs.0.Nat.toDigitsCore.match_1.eq_1 : ∀ (motive : ℕ → ℕ → List Char → Sort u_1) (x : ℕ) (ds : List Char) (h_1 : (x : ℕ) → (ds : List Char) → motive 0 x ds)
  (h_2 : (fuel n : ℕ) → (ds : List Char) → motive fuel.succ n ds),
  (match 0, x, ds with
    | 0, x, ds => h_1 x ds
    | fuel.succ, n, ds => h_2 fuel n ds) =
    h_1 x ds
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.isDetector_separator : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Balanced C]
  [inst_2 : CategoryTheory.HasSeparator C], CategoryTheory.IsDetector (CategoryTheory.separator C)
-- Init.Grind.Ring.CommSemiringAdapter
_private.Init.Grind.Ring.CommSemiringAdapter.0.Lean.Grind.CommRing.Expr.toPolyS.match_4.splitter : (motive : Lean.Grind.CommRing.Expr → Sort u_1) →
  (x : Lean.Grind.CommRing.Expr) →
    ((n : ℤ) → motive (Lean.Grind.CommRing.Expr.num n)) →
      ((x : Lean.Grind.CommRing.Var) → motive (Lean.Grind.CommRing.Expr.var x)) →
        ((a b : Lean.Grind.CommRing.Expr) → motive (a.add b)) →
          ((a b : Lean.Grind.CommRing.Expr) → motive (a.mul b)) →
            ((a : Lean.Grind.CommRing.Expr) → (k : ℕ) → motive (a.pow k)) →
              ((n : ℕ) → motive (Lean.Grind.CommRing.Expr.natCast n)) →
                ((a b : Lean.Grind.CommRing.Expr) → motive (a.sub b)) →
                  ((a : Lean.Grind.CommRing.Expr) → motive a.neg) →
                    ((k : ℤ) → motive (Lean.Grind.CommRing.Expr.intCast k)) → motive x
-- Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
AlgebraicGeometry.PresheafedSpace.GlueData.f_open : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (self : AlgebraicGeometry.PresheafedSpace.GlueData C)
  (i j : self.J), AlgebraicGeometry.PresheafedSpace.IsOpenImmersion (self.f i j)
-- Mathlib.Data.Finset.Card
Finset.card_eq_three : ∀ {α : Type u_1} {s : Finset α} [inst : DecidableEq α], s.card = 3 ↔ ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate
SSet.ιNormalizedChainComplex_d_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasCoproducts C]
  [inst_2 : CategoryTheory.Preadditive C] (X : SSet) {R : C} {n : ℕ} (x : X.obj (Opposite.op { len := n + 1 })) {Z : C}
  (h : (X.normalizedChainComplex R).X n ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.ιNormalizedChainComplex x)
      (CategoryTheory.CategoryStruct.comp ((X.normalizedChainComplex R).d (n + 1) n) h) =
    CategoryTheory.CategoryStruct.comp
      (∑ x_1,
        (-1) ^ ↑x_1 •
          X.ιNormalizedChainComplex ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X x_1)) x))
      h
-- Mathlib.Algebra.Module.Equiv.Defs
LinearEquiv.coe_toAddEquiv_symm : ∀ {R₁ : Type u_2} {R₂ : Type u_3} {M₁ : Type u_8} {M₂ : Type u_9} [inst : Semiring R₁] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M₁] [inst_3 : AddCommMonoid M₂] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂}
  {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂}
  {e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂}, ↑e₁₂.symm = (↑e₁₂).symm
-- Mathlib.MeasureTheory.Integral.Prod
/-- **Fubini's Theorem**: For integrable functions on `α × β`,
the Bochner integral of `f` is equal to the iterated Bochner integral.
`integrable_prod_iff` can be useful to show that the function in question in integrable.
`MeasureTheory.Integrable.integral_prod_right` is useful to show that the inner integral
of the right-hand side is integrable.  -/
MeasureTheory.integral_prod : ∀ {α : Type u_1} {β : Type u_2} {E : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [inst_2 : NormedAddCommGroup E] [MeasureTheory.SFinite ν]
  [inst_4 : NormedSpace ℝ E] [MeasureTheory.SFinite μ] (f : α × β → E),
  MeasureTheory.Integrable f (μ.prod ν) → ∫ (z : α × β), f z ∂μ.prod ν = ∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ
-- Mathlib.Algebra.Ring.InjSurj
/-- A type endowed with `0`, `1` and `+` is an additive monoid with one, if it admits a surjective
map that preserves `0`, `1` and `*` from an additive monoid with one. See note
[reducible non-instances].  -/
Function.Surjective.addMonoidWithOne : {R : Type u_1} →
  {S : Type u_2} →
    (f : R → S) →
      Function.Surjective f →
        [inst : Add S] →
          [inst_1 : Zero S] →
            [inst_2 : One S] →
              [inst_3 : SMul ℕ S] →
                [inst_4 : NatCast S] →
                  [inst_5 : AddMonoidWithOne R] →
                    f 0 = 0 →
                      f 1 = 1 →
                        (∀ (x y : R), f (x + y) = f x + f y) →
                          (∀ (n : ℕ) (x : R), f (n • x) = n • f x) → (∀ (n : ℕ), f ↑n = ↑n) → AddMonoidWithOne S
-- Mathlib.Topology.Algebra.Group.Basic
AddSubgroup.topologicalClosure.eq_1 : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [inst_2 : IsTopologicalAddGroup G] (s : AddSubgroup G),
  s.topologicalClosure = { carrier := closure ↑s, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }
-- Mathlib.CategoryTheory.IsoCat
CategoryTheory.IsoCat.mk.injEq : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (functor : CategoryTheory.Functor C D)
  (inverse : CategoryTheory.Functor D C) (unit_eq : CategoryTheory.Functor.id C = functor.comp inverse)
  (counit_eq : inverse.comp functor = CategoryTheory.Functor.id D) (functor_1 : CategoryTheory.Functor C D)
  (inverse_1 : CategoryTheory.Functor D C) (unit_eq_1 : CategoryTheory.Functor.id C = functor_1.comp inverse_1)
  (counit_eq_1 : inverse_1.comp functor_1 = CategoryTheory.Functor.id D),
  ({ functor := functor, inverse := inverse, unit_eq := unit_eq, counit_eq := counit_eq } =
      { functor := functor_1, inverse := inverse_1, unit_eq := unit_eq_1, counit_eq := counit_eq_1 }) =
    (functor = functor_1 ∧ inverse = inverse_1)
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.homMk₃_app_zero : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {f g : CategoryTheory.ComposableArrows C 3}
  (app₀ : f.obj' 0 _proof_297✝ ⟶ g.obj' 0 _proof_297✝) (app₁ : f.obj' 1 _proof_298✝ ⟶ g.obj' 1 _proof_298✝)
  (app₂ : f.obj' 2 _proof_299✝ ⟶ g.obj' 2 _proof_299✝) (app₃ : f.obj' 3 _proof_300✝ ⟶ g.obj' 3 _proof_300✝)
  (w₀ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (f.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 _proof_298✝)
          app₁ =
        CategoryTheory.CategoryStruct.comp app₀
          (g.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 _proof_298✝))
      _auto_304✝)
  (w₁ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (f.map' 1 2 _proof_246✝ _proof_299✝) app₂ =
        CategoryTheory.CategoryStruct.comp app₁ (g.map' 1 2 _proof_246✝ _proof_299✝))
      _auto_306✝)
  (w₂ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (f.map' 2 3 _proof_299✝ _proof_300✝) app₃ =
        CategoryTheory.CategoryStruct.comp app₂ (g.map' 2 3 _proof_299✝ _proof_300✝))
      _auto_308✝),
  (CategoryTheory.ComposableArrows.homMk₃ app₀ app₁ app₂ app₃ w₀ w₁ w₂).app 0 = app₀
-- Mathlib.Algebra.Module.Equiv.Defs
/-- `M ≃ₗ[R] M₂` denotes the type of linear equivalences between `M` and `M₂` over
a plain linear map `M →ₗ M₂`.  -/
«term_≃ₗ[_]_» : Lean.TrailingParserDescr
-- Mathlib.Order.CompleteLattice.Defs
CompleteLattice.toLattice : {α : Type u_8} → [self : CompleteLattice α] → Lattice α
-- Mathlib.LinearAlgebra.QuadraticForm.Isometry
/-- An isometry between two quadratic spaces `M₁, Q₁` and `M₂, Q₂` over a ring `R`,
is a linear map between `M₁` and `M₂` that commutes with the quadratic forms.  -/
QuadraticMap.Isometry : {R : Type u_1} →
  {M₁ : Type u_3} →
    {M₂ : Type u_4} →
      {N : Type u_7} →
        [inst : CommSemiring R] →
          [inst_1 : AddCommMonoid M₁] →
            [inst_2 : AddCommMonoid M₂] →
              [inst_3 : AddCommMonoid N] →
                [inst_4 : Module R M₁] →
                  [inst_5 : Module R M₂] →
                    [inst_6 : Module R N] → QuadraticMap R M₁ N → QuadraticMap R M₂ N → Type (max u_3 u_4)
-- Init.PropLemmas
exists₃_congr : ∀ {α : Sort u_1} {β : α → Sort u_2} {γ : (a : α) → β a → Sort u_3} {p q : (a : α) → (b : β a) → γ a b → Prop},
  (∀ (a : α) (b : β a) (c : γ a b), p a b c ↔ q a b c) → ((∃ a b c, p a b c) ↔ ∃ a b c, q a b c)
-- Init.Data.UInt.Lemmas
UInt8.ofNat_add : ∀ (a b : ℕ), UInt8.ofNat (a + b) = UInt8.ofNat a + UInt8.ofNat b
-- Mathlib.Topology.Algebra.ProperAction.Basic
/-- The action `G ↷ G` by left translations is proper.  -/
instProperVAddOfIsTopologicalAddGroup : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [IsTopologicalAddGroup G], ProperVAdd G G
-- Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu
/-- `tensorObj G` is left exact: it is additive and preserves monomorphisms and cokernels,
so it preserves homology and therefore finite limits.  -/
CategoryTheory.IsGrothendieckAbelian.GabrielPopescu.preservesFiniteLimits : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.IsGrothendieckAbelian.{v, v, u} C] (G : C),
  CategoryTheory.IsSeparator G →
    CategoryTheory.Limits.PreservesFiniteLimits (CategoryTheory.IsGrothendieckAbelian.tensorObj G)
-- Mathlib.CategoryTheory.Preadditive.Mat
CategoryTheory.Mat_.additiveObjIsoBiproduct_naturality_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Preadditive C] {D : Type u₁}
  [inst_2 : CategoryTheory.Category.{v₁, u₁} D] [inst_3 : CategoryTheory.Preadditive D]
  [inst_4 : CategoryTheory.Limits.HasFiniteBiproducts D] (F : CategoryTheory.Functor (CategoryTheory.Mat_ C) D)
  [inst_5 : F.Additive] {M N : CategoryTheory.Mat_ C} (f : M ⟶ N) {Z : D}
  (h : (⨁ fun i => F.obj ((CategoryTheory.Mat_.embedding C).obj (N.X i))) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.map f)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Mat_.additiveObjIsoBiproduct F N).hom h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Mat_.additiveObjIsoBiproduct F M).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.biproduct.matrix fun i j => F.map ((CategoryTheory.Mat_.embedding C).map (f i j))) h)
-- Std.Data.Iterators.Lemmas.Combinators.Zip
Std.Iter.toList_zip_of_finite : ∀ {α₁ α₂ β₁ β₂ : Type u_1} [inst : Std.Iterator α₁ Id β₁] [inst_1 : Std.Iterator α₂ Id β₂] {it₁ : Std.Iter β₁}
  {it₂ : Std.Iter β₂} [Std.Iterators.Finite α₁ Id] [Std.Iterators.Finite α₂ Id],
  (it₁.zip it₂).toList = it₁.toList.zip it₂.toList