mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.lieSpan_le : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] {s : Set M} {N : LieSubmodule R L M},
  LieSubmodule.lieSpan R L s ≤ N ↔ s ⊆ ↑N
-- Lean.Language.Basic
Lean.Language.SnapshotLeaf.toSnapshot : Lean.Language.SnapshotLeaf → Lean.Language.Snapshot
-- Mathlib.Data.Set.Operations
/-- **Alias** of `Set.mem_sdiff_of_mem`. -/
Set.mem_diff_of_mem : ∀ {α : Type u} {s t : Set α} {x : α}, x ∈ s → x ∉ t → x ∈ s \ t
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.beq_iff_equiv : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} [inst : BEq β] {m₁ m₂ : Std.DTreeMap.Internal.Impl α fun x => β}
  [Std.TransOrd α] [Std.LawfulEqOrd α] [LawfulBEq β],
  m₁.WF → m₂.WF → (Std.DTreeMap.Internal.Impl.Const.beq m₁ m₂ = true ↔ m₁.Equiv m₂)
-- Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts
CategoryTheory.extendCofan_ι_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {n : ℕ} {f : Fin (n + 1) → C}
  (c₁ : CategoryTheory.Limits.Cofan fun i => f i.succ) (c₂ : CategoryTheory.Limits.BinaryCofan (f 0) c₁.pt)
  (X : CategoryTheory.Discrete (Fin (n + 1))),
  (CategoryTheory.extendCofan c₁ c₂).ι.app X =
    Fin.cases c₂.inl (fun i => CategoryTheory.CategoryStruct.comp (c₁.ι.app { as := i }) c₂.inr) X.as
-- Mathlib.Order.Filter.AtTopBot.Basic
Filter.HasAntitoneBasis.comp_mono : ∀ {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} [Nonempty ι] [inst : Preorder ι] [IsDirectedOrder ι]
  [inst_2 : Preorder ι'] {l : Filter α} {s : ι' → Set α},
  l.HasAntitoneBasis s →
    ∀ {φ : ι → ι'}, Monotone φ → Filter.Tendsto φ Filter.atTop Filter.atTop → l.HasAntitoneBasis (s ∘ φ)
-- Mathlib.Analysis.Convolution
MeasureTheory.convolution_smul : ∀ {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup E'] [inst_2 : NormedAddCommGroup F] {f : G → E} {g : G → E'}
  [inst_3 : NontriviallyNormedField 𝕜] [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜 E'] [inst_6 : NormedSpace 𝕜 F]
  {L : E →L[𝕜] E' →L[𝕜] F} [inst_7 : MeasurableSpace G] {μ : MeasureTheory.Measure G} [inst_8 : NormedSpace ℝ F]
  [inst_9 : AddGroup G] [SMulCommClass ℝ 𝕜 F] {y : 𝕜},
  MeasureTheory.convolution f (y • g) L μ = y • MeasureTheory.convolution f g L μ
-- Mathlib.Analysis.Convex.Strong
StrongConcaveOn.eq_1 : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (s : Set E) (m : ℝ),
  StrongConcaveOn s m = UniformConcaveOn s fun r => m / 2 * r ^ 2
-- Mathlib.CategoryTheory.WithTerminal.Basic
/-- Identity morphisms for `WithTerminal C`.  -/
CategoryTheory.WithTerminal.id : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → (X : CategoryTheory.WithTerminal C) → X.Hom X
-- Lean.Data.Trie
Lean.Data.Trie.leaf.injEq : ∀ {α : Type} (a a_1 : Option α), (Lean.Data.Trie.leaf a = Lean.Data.Trie.leaf a_1) = (a = a_1)
-- Mathlib.Order.Bounds.Basic
IsLeast.lt_iff : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α} {a b : α}, IsLeast s a → (b < a ↔ ∀ x ∈ s, b < x)
-- Mathlib.Order.SuccPred.IntervalSucc
/-- Union formula for `Set.Ico (f i) (f (Order.succ i))` over `i ∈ Ici a`. See also
`iUnion_Ico_map_succ_eq_Ici` for the specialization `a = ⊥`.  -/
biUnion_Ici_Ico_map_succ : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : SuccOrder α] [IsSuccArchimedean α]
  [inst_3 : LinearOrder β] {f : α → β} {a : α},
  (∀ i ∈ Set.Ici a, f a ≤ f i) →
    ¬BddAbove (f '' Set.Ici a) → ⋃ i ∈ Set.Ici a, Set.Ico (f i) (f (Order.succ i)) = Set.Ici (f a)
-- Mathlib.RingTheory.Spectrum.Prime.Topology
IsLocalRing.Ring.KrullDimLE.eq_bot_or_eq_top : ∀ {R : Type u} [inst : CommSemiring R] [inst_1 : IsLocalRing R] [inst_2 : IsDomain R] [Ring.KrullDimLE 1 R]
  (x : PrimeSpectrum R), x = ⊥ ∨ x = ⊤
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.Scheme.Hom.opensRange_localizationAway : ∀ {R : CommRingCat} (g : ↑R),
  AlgebraicGeometry.Scheme.Hom.opensRange
      (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away g)))) =
    PrimeSpectrum.basicOpen g
-- Mathlib.Algebra.Lie.Sl2
_private.Mathlib.Algebra.Lie.Sl2.0.IsSl2Triple.HasPrimitiveVectorWith.termψ_ : Lean.ParserDescr
-- Mathlib.Topology.FiberBundle.Trivialization
/-- The source is homeomorphic to the product of the base set with the fiber.  -/
Bundle.Trivialization.sourceHomeomorphBaseSetProd : {B : Type u_1} →
  {F : Type u_2} →
    {Z : Type u_4} →
      [inst : TopologicalSpace B] →
        [inst_1 : TopologicalSpace F] →
          {proj : Z → B} →
            [inst_2 : TopologicalSpace Z] → (e : Bundle.Trivialization F proj) → ↑e.source ≃ₜ ↑e.baseSet × F
-- Lean.Meta.Sym.SymM
Lean.Meta.Sym.ProofInstInfo.mk : Array Lean.Meta.Sym.ProofInstArgInfo → Lean.Meta.Sym.ProofInstInfo
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.aevalTower_X : ∀ {R : Type u} {S : Type v} {A' : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring A'] [inst_2 : CommSemiring S]
  [inst_3 : Algebra S R] [inst_4 : Algebra S A'] (g : R →ₐ[S] A') (y : A'), (Polynomial.aevalTower g y) Polynomial.X = y
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.size_filter_le_size : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {f : α → Bool}, (Std.ExtHashSet.filter f m).size ≤ m.size
-- Init.Data.Int.DivMod.Lemmas
Int.tdiv_eq_ediv_of_dvd : ∀ {a b : ℤ}, b ∣ a → a.tdiv b = a / b
-- Mathlib.CategoryTheory.Functor.ReflectsIso.Exact
CategoryTheory.JointlyReflectIsomorphisms.exact_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {I : Type u_2} {D : I → Type u_3}
  [inst_1 : (i : I) → CategoryTheory.Category.{v_2, u_3} (D i)] {F : (i : I) → CategoryTheory.Functor C (D i)},
  CategoryTheory.JointlyReflectIsomorphisms F →
    ∀ [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
      [inst_3 : (i : I) → CategoryTheory.Limits.HasZeroMorphisms (D i)]
      [inst_4 : ∀ (i : I), (F i).PreservesZeroMorphisms] [CategoryTheory.CategoryWithHomology C]
      [∀ (i : I), (F i).PreservesHomology] [CategoryTheory.Limits.HasZeroObject C] (S : CategoryTheory.ShortComplex C),
      S.Exact ↔ ∀ (i : I), (S.map (F i)).Exact
-- Lean.Data.JsonRpc
_private.Lean.Data.JsonRpc.0.Lean.JsonRpc.messageMetaDataParser.parseRequestID : Std.Internal.Parsec.String.Parser Lean.JsonRpc.RequestID
-- Mathlib.Probability.Independence.Conditional
/-- Two random variables `f, g` are conditionally independent given a third `k` iff the
joint distribution of `k, f, g` factors into a product of their conditional distributions
given `k`.  -/
ProbabilityTheory.condIndepFun_iff_map_prod_eq_prod_condDistrib_prod_condDistrib : ∀ {Ω : Type u_1} {β : Type u_3} {β' : Type u_4} {mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω]
  {μ : MeasureTheory.Measure Ω} [inst_1 : MeasureTheory.IsFiniteMeasure μ] {f : Ω → β} {g : Ω → β'} {γ : Type u_5}
  {mγ : MeasurableSpace γ} {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'} [inst_2 : StandardBorelSpace β]
  [inst_3 : Nonempty β] [inst_4 : StandardBorelSpace β'] [inst_5 : Nonempty β'],
  Measurable f →
    Measurable g →
      ∀ {k : Ω → γ} (hk : Measurable k),
        ProbabilityTheory.CondIndepFun (MeasurableSpace.comap k inferInstance) ⋯ f g μ ↔
          MeasureTheory.Measure.map (fun ω => (k ω, f ω, g ω)) μ =
            (MeasureTheory.Measure.map k μ).bind
              ⇑(ProbabilityTheory.Kernel.id.prod
                  ((ProbabilityTheory.condDistrib f k μ).prod (ProbabilityTheory.condDistrib g k μ)))
-- Mathlib.Algebra.Module.Submodule.Defs
/-- `Submodule R M` almost never has decidable equality.
Given an element `m ≠ 0` in `M`, `Submodule R M` has decidable equality iff
all propositions are decidable. We add a global instance that `Submodule R M` has decidable
equality, coming from the choice axiom, so that we don't have to provide
`[DecidableEq (Submodule R M)]` arguments in lemma statements.  -/
Submodule.decidableEq : {R : Type u} →
  {M : Type v} → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → DecidableEq (Submodule R M)
-- Mathlib.CategoryTheory.Monoidal.Hopf_
CategoryTheory.HopfObj.antipode_comul : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (A : C) [inst_3 : CategoryTheory.HopfObj A],
  CategoryTheory.CategoryStruct.comp CategoryTheory.HopfObj.antipode CategoryTheory.ComonObj.comul =
    CategoryTheory.CategoryStruct.comp CategoryTheory.ComonObj.comul
      (CategoryTheory.CategoryStruct.comp (β_ A A).hom
        (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.HopfObj.antipode
          CategoryTheory.HopfObj.antipode))
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.updateCell.match_1.splitter : {α : Type u_2} →
  {β : α → Type u_1} →
    (motive : Option ((a : α) × β a) → Sort u_3) →
      (x : Option ((a : α) × β a)) → (Unit → motive none) → ((k' : α) → (v' : β k') → motive (some ⟨k', v'⟩)) → motive x
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddEquiv.instAddEquivClass : ∀ {M : Type u_1} {N : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace N] [inst_2 : Add M]
  [inst_3 : Add N], AddEquivClass (M ≃ₜ+ N) M N
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.ker.condition : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasKernels C],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.ker.ι C) CategoryTheory.Arrow.leftToRight = 0
-- Mathlib.Order.Hom.WithTopBot
LatticeHom.coe_withTopWithBot : ∀ {α : Type u_1} {β : Type u_2} [inst : Lattice α] [inst_1 : Lattice β] (f : LatticeHom α β),
  ⇑f.withTopWithBot = WithTop.map (WithBot.map ⇑f)
-- Aesop.Script.Util
Aesop.Script.findFirstStep? : {α β : Type} → Array α → (α → Option β) → (β → ℕ) → Option (ℕ × α × β)
-- Mathlib.Analysis.SpecialFunctions.Log.ERealExp
EReal.exp_lt_exp_iff : ∀ {a b : EReal}, a.exp < b.exp ↔ a < b
-- Init.Data.String.Lemmas.Pattern.String.ForwardSearcher
_private.Init.Data.String.Lemmas.Pattern.String.ForwardSearcher.0.String.Slice.Pattern.Model.ForwardSliceSearcher.prefixFunctionRecurrence.congr_simp : ∀ (pat pat_1 : ByteArray) (e_pat : pat = pat_1) (stackPos stackPos_1 : ℕ) (e_stackPos : stackPos = stackPos_1)
  (hst : stackPos < pat.size) (guess guess_1 : ℕ) (e_guess : guess = guess_1) (hg : guess < stackPos),
  String.Slice.Pattern.Model.ForwardSliceSearcher.prefixFunctionRecurrence✝ pat stackPos hst guess hg =
    String.Slice.Pattern.Model.ForwardSliceSearcher.prefixFunctionRecurrence✝ pat_1 stackPos_1 ⋯ guess_1 ⋯
-- Mathlib.RingTheory.Smooth.IntegralClosure
StandardEtalePresentation.mk.congr_simp : ∀ {R : Type u_4} {S : Type u_5} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P P_1 : StandardEtalePair R) (e_P : P = P_1) (x x_1 : S) (e_x : x = x_1) (hasMap : P.HasMap x)
  (lift_bijective : Function.Bijective ⇑(P.lift x hasMap)),
  { P := P, x := x, hasMap := hasMap, lift_bijective := lift_bijective } =
    { P := P_1, x := x_1, hasMap := ⋯, lift_bijective := ⋯ }
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.limit.w_assoc : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Functor J C) [inst_2 : CategoryTheory.Limits.HasLimit F] {j j' : J} (f : j ⟶ j') {Z : C}
  (h : F.obj j' ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π F j)
      (CategoryTheory.CategoryStruct.comp (F.map f) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π F j') h
-- Mathlib.Tactic.Linarith.Verification
/-- `mkNegOneLtZeroProof tp` returns a proof of `-1 < 0`,
where the numerals are natively of type `tp`.
 -/
Mathlib.Tactic.Linarith.mkNegOneLtZeroProof : Lean.Expr → Lean.MetaM Lean.Expr
-- Std.Time.Zoned.Database.TZdb
Std.Time.Database.TZdb.mk : Array System.FilePath → Std.Time.Database.TZdb
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.maxKey?_modify : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {f : β → β}, (t.modify k f).maxKey? = Option.map (fun km => if cmp km k = Ordering.eq then k else km) t.maxKey?
-- Mathlib.Tactic.Explode.Datatypes
/-- `Entry.depth` * `│`  -/
Mathlib.Explode.Status.lam : Mathlib.Explode.Status
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Add
Std.Tactic.BVDecide.BVExpr.bitblast.mkFullAdder : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      (aig : Std.Sat.AIG α) →
        Std.Tactic.BVDecide.BVExpr.bitblast.FullAdderInput aig → Std.Tactic.BVDecide.BVExpr.bitblast.FullAdderOutput aig
-- Init.Data.Array.Perm
List.Perm.toArray : ∀ {α : Type u_1} {as bs : List α}, as.Perm bs → as.toArray.Perm bs.toArray
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.instAdd.eq_1 : ∀ {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6}
  {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)]
  [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι] [inst_4 : (i : ι) → Add (G i)]
  [inst_5 : ∀ (i j : ι) (h : i ≤ j), AddHomClass (T h) (G i) (G j)],
  DirectLimit.instAdd = { add := DirectLimit.map₂ f f f (fun x x1 x2 => x1 + x2) ⋯ }
-- Mathlib.Algebra.Category.MonCat.FilteredColimits
/-- Given a cocone `t` of `F`, the induced monoid homomorphism from the colimit to the cocone point.
As a function, this is simply given by the induced map of the corresponding cocone in `Type`.
The only thing left to see is that it is a monoid homomorphism.
 -/
MonCat.FilteredColimits.colimitDesc : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    (F : CategoryTheory.Functor J MonCat) →
      [inst_1 : CategoryTheory.IsFiltered J] →
        (t : CategoryTheory.Limits.Cocone F) → MonCat.FilteredColimits.colimit F ⟶ t.pt
-- Mathlib.Algebra.Order.Monoid.Unbundled.Pow
lt_max_of_two_nsmul_lt_add : ∀ {M : Type u_3} [inst : AddMonoid M] [inst_1 : LinearOrder M] [AddLeftMono M] [AddRightMono M] {a b c : M},
  2 • a < b + c → a < max b c
-- Lean.Elab.BuiltinNotation
Lean.Elab.Term.elabBorrowed : Lean.Elab.Term.TermElab
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.indepSet_empty_right : ∀ {Ω : Type u_1} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsZeroOrProbabilityMeasure μ]
  (s : Set Ω), ProbabilityTheory.IndepSet s ∅ μ
-- Mathlib.Topology.SmallInductiveDimension
smallInductiveDimension.eq_1 : ∀ (X : Type u_1) [inst : TopologicalSpace X],
  smallInductiveDimension X = sInf {n | ∀ (i : ℕ), n < ↑i → HasSmallInductiveDimensionLT X i}
-- Mathlib.Order.Bounds.Basic
isGLB_singleton : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, IsGLB {a} a
-- Mathlib.RingTheory.Ideal.Pointwise
Ideal.smul_sup : ∀ {M : Type u_1} {R : Type u_3} [inst : Monoid M] [inst_1 : Semiring R] [inst_2 : MulSemiringAction M R] (a : M)
  (S T : Ideal R), a • (S ⊔ T) = a • S ⊔ a • T
-- Mathlib.Data.FinEnum
FinEnum.card_UInt32 : FinEnum.card UInt32 = 2 ^ 32
-- Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Asymptotics.IsBigO.rpow : ∀ {α : Type u_1} {r : ℝ} {l : Filter α} {f g : α → ℝ},
  0 ≤ r → 0 ≤ᶠ[l] g → f =O[l] g → (fun x => f x ^ r) =O[l] fun x => g x ^ r
-- Mathlib.AlgebraicGeometry.Cover.Open
AlgebraicGeometry.Scheme.instFintypeI₀FiniteSubcover : {X : AlgebraicGeometry.Scheme} → (𝒰 : X.OpenCover) → [H : CompactSpace ↥X] → Fintype 𝒰.finiteSubcover.I₀
-- Mathlib.Analysis.Normed.Algebra.Spectrum
spectrum.SpectralRadius.of_subsingleton : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NormedField 𝕜] [inst_1 : Ring A] [inst_2 : Algebra 𝕜 A] [Subsingleton A]
  (a : A), spectralRadius 𝕜 a = 0
-- Mathlib.Topology.MetricSpace.Isometry
/-- `piFinTwoEquiv` as an `IsometryEquiv`.  -/
IsometryEquiv.piFinTwo : (α : Fin 2 → Type u_3) → [inst : (i : Fin 2) → PseudoEMetricSpace (α i)] → ((i : Fin 2) → α i) ≃ᵢ α 0 × α 1
-- Lean.Data.Lsp.Basic
Lean.Lsp.instFromJsonTextDocumentItem : Lean.FromJson Lean.Lsp.TextDocumentItem
-- Mathlib.MeasureTheory.VectorMeasure.BoundedVariation
BoundedVariationOn.vectorMeasure_Iic : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : DenselyOrdered α] [inst_2 : TopologicalSpace α]
  [inst_3 : OrderTopology α] [inst_4 : SecondCountableTopology α] [inst_5 : CompactIccSpace α] [hα : MeasurableSpace α]
  [inst_6 : BorelSpace α] {E : Type u_2} [inst_7 : NormedAddCommGroup E] [inst_8 : CompleteSpace E] {f : α → E}
  (hf : BoundedVariationOn f Set.univ) (a : α),
  hf.vectorMeasure (Set.Iic a) = Function.rightLim f a - Filter.atBot.limUnder f
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.integral_iUnion : ∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {f : X → E} {μ : MeasureTheory.Measure X} {ι : Type u_5} [Countable ι] {s : ι → Set X},
  (∀ (i : ι), MeasurableSet (s i)) →
    Pairwise (Function.onFun Disjoint s) →
      MeasureTheory.IntegrableOn f (⋃ i, s i) μ → ∫ (x : X) in ⋃ n, s n, f x ∂μ = ∑' (n : ι), ∫ (x : X) in s n, f x ∂μ
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank
SSet.Subcomplex.PairingCore.RankFunction.mk.injEq : ∀ {X : SSet} {A : X.Subcomplex} {h : A.PairingCore} {α : Type v} [inst : PartialOrder α] (rank : h.ι → α)
  (lt : ∀ {x y : h.ι}, h.AncestralRel x y → rank x < rank y) (rank_1 : h.ι → α)
  (lt_1 : ∀ {x y : h.ι}, h.AncestralRel x y → rank_1 x < rank_1 y),
  ({ rank := rank, lt := lt } = { rank := rank_1, lt := lt_1 }) = (rank = rank_1)
-- Lean.AuxRecursor
Lean.brecOnSuffix : String
-- Init.Grind.Ordered.Ring
Lean.Grind.OrderedRing.mul_nonneg : ∀ {R : Type u} [inst : Lean.Grind.Ring R] [inst_1 : LE R] [inst_2 : LT R] [inst_3 : Std.IsPartialOrder R]
  [Lean.Grind.OrderedRing R] [Std.LawfulOrderLT R] {a b : R}, 0 ≤ a → 0 ≤ b → 0 ≤ a * b
-- Mathlib.Topology.MetricSpace.GromovHausdorff
/-- The Gromov-Hausdorff space  -/
GromovHausdorff.GHSpace : Type
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
/-- Interpret `single a` as a linear map.  -/
SkewMonoidAlgebra.lsingle : (R : Type u_3) →
  {M : Type u_4} →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid M] → {α : Type u_6} → α → [inst_2 : Module R M] → M →ₗ[R] SkewMonoidAlgebra M α
-- Mathlib.Topology.Order.Compact
atBot_atTop_le_cocompact : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [NoMinOrder α] [NoMaxOrder α]
  [OrderClosedTopology α], Filter.atBot ⊔ Filter.atTop ≤ Filter.cocompact α
-- Init.Data.List.Sublist
List.takeWhile_subset : ∀ {α : Type u_1} {l : List α} (p : α → Bool), List.takeWhile p l ⊆ l
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.homotopyCofiber.inlX_desc_f_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} {F G K : HomologicalComplex C c} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ]
  [inst_3 : DecidableRel c.Rel] (α : G ⟶ K) (hα : Homotopy (CategoryTheory.CategoryStruct.comp φ α) 0) (i j : ι)
  (hjk : c.Rel j i) {Z : C} (h : K.X j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.inlX φ i j hjk)
      (CategoryTheory.CategoryStruct.comp ((HomologicalComplex.homotopyCofiber.desc φ α hα).f j) h) =
    CategoryTheory.CategoryStruct.comp (hα.hom i j) h
-- Mathlib.Analysis.Calculus.DifferentialForm.Basic
extDeriv.eq_1 : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : ℕ}
  (ω : E → E [⋀^Fin n]→L[𝕜] F) (x : E), extDeriv ω x = ContinuousAlternatingMap.alternatizeUncurryFin (fderiv 𝕜 ω x)
-- Mathlib.RingTheory.Valuation.Integers
Valuation.integer.v_irreducible_lt_one : ∀ {F : Type u} {Γ₀ : Type v} [inst : Field F] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] {v : Valuation F Γ₀}
  {ϖ : ↥v.integer}, Irreducible ϖ → v ↑ϖ < 1
-- Init.Data.Nat.Lemmas
Nat.sub_add_sub_cancel : ∀ {a b c : ℕ}, b ≤ a → c ≤ b → a - b + (b - c) = a - c
-- Mathlib.Algebra.Category.Grp.Basic
/-- An alias for `AddCommGrpCat.{max u v}`, to deal around unification issues.  -/
AddCommGrpMaxAux : Type ((max u1 u2) + 1)
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.IndepFun.neg_right : ∀ {Ω : Type u_1} {β : Type u_6} {β' : Type u_7} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {f : Ω → β}
  {g : Ω → β'} {_mβ : MeasurableSpace β} {_mβ' : MeasurableSpace β'} [inst : Neg β'] [MeasurableNeg β'],
  ProbabilityTheory.IndepFun f g μ → ProbabilityTheory.IndepFun f (-g) μ
-- Mathlib.Data.Set.Finite.Lattice
/-- An increasing union distributes over finite intersection.  -/
Set.iUnion_iInter_of_monotone : ∀ {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} [Finite ι] [inst : Preorder ι'] [IsDirectedOrder ι'] [Nonempty ι']
  {s : ι → ι' → Set α}, (∀ (i : ι), Monotone (s i)) → ⋃ j, ⋂ i, s i j = ⋂ i, ⋃ j, s i j
-- Std.Http.Data.Body.Stream
_private.Std.Http.Data.Body.Stream.0.Std.Http.Body.Stream.mk.inj : ∀ {state state_1 : Std.Mutex Std.Http.Body.Channel.State✝}, { state := state } = { state := state_1 } → state = state_1
-- Mathlib.GroupTheory.Generators
Group.Generators.reindex_val : ∀ {G : Type u_1} {ι : Type u_3} {ι' : Type u_4} [inst : Group G] (P : Group.Generators G ι) (e : ι' ≃ ι),
  (P.reindex e).val = P.val ∘ ⇑e
-- Lean.Meta.HaveTelescope
/-- Information about a single `have` in a `have` telescope.
Created by `getHaveTelescopeInfo`.
 -/
Lean.Meta.HaveInfo : Type
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoMod_lt_right : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α), toIcoMod hp a b < a + p
-- Mathlib.Data.Int.Init
Int.inductionOn'_self : ∀ {motive : ℤ → Sort u_1} {b : ℤ} {zero : motive b} {succ : (k : ℤ) → b ≤ k → motive k → motive (k + 1)}
  {pred : (k : ℤ) → k ≤ b → motive k → motive (k - 1)}, Int.inductionOn' b b zero succ pred = zero
-- Mathlib.Computability.TuringMachine.PostTuringMachine
_private.Mathlib.Computability.TuringMachine.PostTuringMachine.0.Option.getD.match_1.eq_2 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (h_1 : (x : α) → motive (some x)) (h_2 : Unit → motive none),
  (match none with
    | some x => h_1 x
    | none => h_2 ()) =
    h_2 ()
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.maxKey!_eq_getLast!_keys : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.WF → t.maxKey! = t.keys.getLast!
-- Mathlib.Data.Ordmap.Invariants
Ordnode.all_balance' : ∀ {α : Type u_1} {P : α → Prop} {l : Ordnode α} {x : α} {r : Ordnode α},
  Ordnode.All P (l.balance' x r) ↔ Ordnode.All P l ∧ P x ∧ Ordnode.All P r
-- Mathlib.RingTheory.Lasker
Submodule.IsLasker.exists_isMinimalPrimaryDecomposition : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  IsLasker R M → ∀ (N : Submodule R M), ∃ t, N.IsMinimalPrimaryDecomposition t
-- Mathlib.Probability.Distributions.Fernique
ProbabilityTheory.Fernique.normThreshold_strictMono : ∀ {a : ℝ}, 0 < a → StrictMono (ProbabilityTheory.Fernique.normThreshold a)
-- Mathlib.Data.Fin.SuccPred
Fin.castPred_ne_zero : ∀ {n : ℕ} [inst : NeZero n] {i : Fin (n + 1)} (h₁ : i ≠ Fin.last n), i ≠ 0 → i.castPred h₁ ≠ 0
-- Mathlib.LinearAlgebra.RootSystem.Hom
RootPairing.Hom.root_weightMap_apply : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {ι₂ : Type u_5} {M₂ : Type u_6} {N₂ : Type u_7}
  [inst_5 : AddCommGroup M₂] [inst_6 : Module R M₂] [inst_7 : AddCommGroup N₂] [inst_8 : Module R N₂]
  (P : RootPairing ι R M N) (Q : RootPairing ι₂ R M₂ N₂) (i : ι) (f : P.Hom Q),
  f.weightMap (P.root i) = Q.root (f.indexEquiv i)
-- Mathlib.Order.Cover
Pi.covBy_iff_exists_left_eq : ∀ {ι : Type u_3} {α : ι → Type u_4} [inst : (i : ι) → PartialOrder (α i)] {a b : (i : ι) → α i}
  [inst_1 : DecidableEq ι], a ⋖ b ↔ ∃ i x, x ⋖ b i ∧ a = Function.update b i x