mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Elab.InfoTree.Main
/-- Returns the current array of InfoTrees and resets it to an empty array.  -/
Lean.Elab.getResetInfoTrees : {m : Type → Type} → [Monad m] → [Lean.Elab.MonadInfoTree m] → m (Lean.PersistentArray Lean.Elab.InfoTree)
-- Mathlib.Data.List.Flatten
/-- See also `head_flatten_eq_head_head`, which switches around the proof obligations.  -/
List.head_head_eq_head_flatten : ∀ {α : Type u_1} {l : List (List α)} (hl : l ≠ []) (hl' : l.head hl ≠ []), (l.head hl).head hl' = l.flatten.head ⋯
-- Mathlib.Topology.Compactness.Lindelof
/-- A sigma-compact space `X` is Lindelöf.  -/
instLindelofSpaceOfSigmaCompactSpace : ∀ {X : Type u} [inst : TopologicalSpace X] [SigmaCompactSpace X], LindelofSpace X
-- Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
Matrix.Represents.one : ∀ {ι : Type u_1} [inst : Fintype ι] {M : Type u_2} [inst_1 : AddCommGroup M] {R : Type u_3} [inst_2 : CommRing R]
  [inst_3 : Module R M] {b : ι → M} [inst_4 : DecidableEq ι], Matrix.Represents b 1 1
-- Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
/-- If a functor creates initial objects and pushouts, it creates finite colimits.

We additionally require the rather strong condition that the functor reflects isomorphisms. It is
unclear whether the statement remains true without this condition. There are various definitions of
"creating colimits" in the literature, and whether or not the condition can be dropped seems to
depend on the specific definition that is used.  -/
CategoryTheory.Limits.createsFiniteColimitsOfCreatesInitialAndPushouts : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        [CategoryTheory.Limits.HasInitial D] →
          [CategoryTheory.Limits.HasPushouts D] →
            (G : CategoryTheory.Functor C D) →
              [G.ReflectsIsomorphisms] →
                [CategoryTheory.CreatesColimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) G] →
                  [CategoryTheory.CreatesColimitsOfShape CategoryTheory.Limits.WalkingSpan G] →
                    CategoryTheory.Limits.CreatesFiniteColimits G
-- Std.Data.Iterators.Combinators.Monadic.Drop
Std.Iterators.Types.Drop.mk.sizeOf_spec : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} [inst : SizeOf α] [inst_1 : (a : Type w) → SizeOf (m a)]
  [inst_2 : SizeOf β] (remaining : ℕ) (inner : Std.IterM m β),
  sizeOf { remaining := remaining, inner := inner } = 1 + sizeOf remaining + sizeOf inner
-- Lean.Parser.Basic
Lean.Parser.setExpectedFn : List String → Lean.Parser.ParserFn → Lean.Parser.ParserFn
-- Mathlib.Data.Set.Subsingleton
Set.nontrivial_of_univ_nontrivial : ∀ {α : Type u}, Set.univ.Nontrivial → Nontrivial α
-- Mathlib.LinearAlgebra.Dimension.Constructions
finrank_span_finset_le_card : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [StrongRankCondition R]
  (s : Finset M), Set.finrank R ↑s ≤ s.card
-- Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
LiouvilleWith.rat_mul : ∀ {p x : ℝ} {r : ℚ}, LiouvilleWith p x → r ≠ 0 → LiouvilleWith p (↑r * x)
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
/-- Monomial degree of product  -/
MonomialOrder.degree_mul_of_isRegular_right : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] {f g : MvPolynomial σ R},
  f ≠ 0 → IsRegular (m.leadingCoeff g) → m.degree (f * g) = m.degree f + m.degree g
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.isEmpty_insertMany_emptyWithCapacity_list : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  {l : List ((a : α) × β a)}, (↑↑(Std.DHashMap.Internal.Raw₀.emptyWithCapacity.insertMany l)).isEmpty = l.isEmpty
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.prodComparisonBifunctorNatTrans_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₁} [inst_2 : CategoryTheory.Category.{v₁, u₁} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  (F : CategoryTheory.Functor C D) {E : Type u₂} [inst_4 : CategoryTheory.Category.{v₂, u₂} E]
  [inst_5 : CategoryTheory.CartesianMonoidalCategory E] (G : CategoryTheory.Functor D E),
  CategoryTheory.CartesianMonoidalCategory.prodComparisonBifunctorNatTrans (F.comp G) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Functor.whiskerRight (CategoryTheory.CartesianMonoidalCategory.prodComparisonBifunctorNatTrans F)
        ((CategoryTheory.Functor.whiskeringRight C D E).obj G))
      (F.whiskerLeft
        (CategoryTheory.Functor.whiskerRight
          (CategoryTheory.CartesianMonoidalCategory.prodComparisonBifunctorNatTrans G)
          ((CategoryTheory.Functor.whiskeringLeft C D E).obj F)))
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
CategoryTheory.Limits.CatCospanTransform.associator_hom_base_app : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} {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] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] [inst_4 : CategoryTheory.Category.{v₅, u₅} B']
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'}
  [inst_6 : CategoryTheory.Category.{v₇, u₇} A''] [inst_7 : CategoryTheory.Category.{v₈, u₈} B'']
  [inst_8 : CategoryTheory.Category.{v₉, u₉} C''] {F'' : CategoryTheory.Functor A'' B''}
  {G'' : CategoryTheory.Functor C'' B''} {A''' : Type u₁₀} {B''' : Type u₁₁} {C''' : Type u₁₂}
  [inst_9 : CategoryTheory.Category.{v₁₀, u₁₀} A'''] [inst_10 : CategoryTheory.Category.{v₁₁, u₁₁} B''']
  [inst_11 : CategoryTheory.Category.{v₁₂, u₁₂} C'''] {F''' : CategoryTheory.Functor A''' B'''}
  {G''' : CategoryTheory.Functor C''' B'''} (φ : CategoryTheory.Limits.CatCospanTransform F G F' G')
  (φ' : CategoryTheory.Limits.CatCospanTransform F' G' F'' G'')
  (φ'' : CategoryTheory.Limits.CatCospanTransform F'' G'' F''' G''') (x : B),
  (φ.associator φ' φ'').hom.base.app x = CategoryTheory.CategoryStruct.id (φ''.base.obj (φ'.base.obj (φ.base.obj x)))
-- Lean.Linter.Init
Lean.Options.toLinterOptions : {m : Type → Type} → [Monad m] → [Lean.MonadEnv m] → Lean.Options → m Lean.Linter.LinterOptions
-- Mathlib.CategoryTheory.Bicategory.InducedBicategory
_private.Mathlib.CategoryTheory.Bicategory.InducedBicategory.0.CategoryTheory.Bicategory.InducedBicategory.Hom.mk.sizeOf_spec : ∀ {B : Type u_1} {C : Type u_2} [inst : CategoryTheory.Bicategory C] {F : B → C}
  {X Y : CategoryTheory.Bicategory.InducedBicategory C F} [inst_1 : SizeOf B] [inst_2 : SizeOf C] (hom : F X ⟶ F Y),
  sizeOf { hom := hom } = 1 + sizeOf hom
-- Mathlib.Algebra.Group.Units.Defs
/-- `IsAddUnit x` is decidable if we can decide if `x` comes from `AddUnits M`.  -/
IsAddUnit.instDecidableOfExistsAddUnitsEqVal : {M : Type u_1} → [inst : AddMonoid M] → (x : M) → [h : Decidable (∃ u, ↑u = x)] → Decidable (IsAddUnit x)
-- Mathlib.Order.BooleanAlgebra.Basic
inf_sdiff_self_left : ∀ {α : Type u} {x y : α} [inst : GeneralizedBooleanAlgebra α], y \ x ⊓ x = ⊥
-- Mathlib.Algebra.BigOperators.Option
Finset.prod_insertNone : ∀ {α : Type u_1} {M : Type u_2} [inst : CommMonoid M] (f : Option α → M) (s : Finset α),
  ∏ x ∈ Finset.insertNone s, f x = f none * ∏ x ∈ s, f (some x)
-- Mathlib.CategoryTheory.Bicategory.Modification.Pseudo
CategoryTheory.Pseudofunctor.StrongTrans.Hom.of.injEq : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.Pseudofunctor B C} {η θ : F ⟶ G}
  (as as_1 : CategoryTheory.Pseudofunctor.StrongTrans.Modification η θ), ({ as := as } = { as := as_1 }) = (as = as_1)
-- Mathlib.Logic.Equiv.Basic
PLift.eq_up_iff_down_eq : ∀ {α : Sort u_1} {x : PLift α} {y : α}, x = { down := y } ↔ x.down = y
-- Mathlib.Algebra.Ring.BooleanRing
/-- A Boolean ring is a ring where multiplication is idempotent.  -/
BooleanRing : Type u_4 → Type u_4
-- Mathlib.Data.W.Basic
/-- The depth of a finitely branching tree.  -/
WType.depth : {α : Type u_1} → {β : α → Type u_2} → [(a : α) → Fintype (β a)] → WType β → ℕ
-- Mathlib.NumberTheory.Modular
ModularGroup.exists_one_half_le_im_smul : ∀ (τ : UpperHalfPlane), ∃ γ, 1 / 2 ≤ (γ • τ).im
-- Mathlib.Algebra.Homology.HomotopyCategory.ShortExact
CochainComplex.mappingCone.mapHomologicalComplexIso_hom_descShortComplex : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C] {D : Type u_2}
  [inst_2 : CategoryTheory.Category.{v_2, u_2} D] [inst_3 : CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D)
  [inst_4 : F.Additive] (S : CategoryTheory.ShortComplex (CochainComplex C ℤ)),
  CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.mapHomologicalComplexIso S.f F).hom
      (CochainComplex.mappingCone.descShortComplex (S.map (F.mapHomologicalComplex (ComplexShape.up ℤ)))) =
    (F.mapHomologicalComplex (ComplexShape.up ℤ)).map (CochainComplex.mappingCone.descShortComplex S)
-- Mathlib.MeasureTheory.Measure.Sub
/-- See `sub_le_iff_le_add` for the case where both measures are finite, which does not need the
hypothesis `ν ≤ μ`.  -/
MeasureTheory.Measure.sub_le_iff_le_add_of_le : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ ν ξ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure ν],
  ν ≤ μ → (μ - ν ≤ ξ ↔ μ ≤ ξ + ν)
-- Aesop.Util.Tactic.Ext
Aesop.ExtResult.commonFVarIds : Aesop.ExtResult → Array Lean.FVarId
-- Mathlib.Topology.Algebra.Order.LiminfLimsup
/-- `liminf (c + xᵢ) = c + liminf xᵢ`.  -/
limsup_const_add : ∀ {ι : Type u_1} {R : Type u_4} [inst : ConditionallyCompleteLinearOrder R] [inst_1 : TopologicalSpace R]
  [OrderTopology R] (F : Filter ι) [F.NeBot] [inst_4 : Add R] [ContinuousAdd R] [AddLeftMono R] (f : ι → R) (c : R),
  Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) F f →
    Filter.IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) F f → Filter.limsup (fun i => c + f i) F = c + Filter.limsup f F
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks
CategoryTheory.Limits.instIsIsoPullbackComparison : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} [inst_2 : CategoryTheory.Limits.HasPullback f g]
  [inst_3 : CategoryTheory.Limits.HasPullback (G.map f) (G.map g)]
  [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) G],
  CategoryTheory.IsIso (CategoryTheory.Limits.pullbackComparison G f g)
-- Mathlib.GroupTheory.FiniteIndexNormalSubgroup
FiniteIndexNormalAddSubgroup.toAddSubgroup_injective : ∀ {G : Type u_1} [inst : AddGroup G], Function.Injective fun H => H.toAddSubgroup
-- Lean.Elab.InfoTree.Types
Lean.Elab.PartialContextInfo.commandCtx : Lean.Elab.CommandContextInfo → Lean.Elab.PartialContextInfo
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.δ_add : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (n m : ℤ) (z₁ z₂ : CochainComplex.HomComplex.Cochain F G n),
  CochainComplex.HomComplex.δ n m (z₁ + z₂) = CochainComplex.HomComplex.δ n m z₁ + CochainComplex.HomComplex.δ n m z₂
-- Mathlib.Algebra.Homology.CochainComplexPlus
CategoryTheory.Functor.mapCochainComplexPlusCompι_inv_app_f : ∀ {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] (F : CategoryTheory.Functor C D)
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  [inst_4 : F.PreservesZeroMorphisms] (X : CochainComplex.Plus C) (x : ℤ),
  (F.mapCochainComplexPlusCompι.inv.app X).f x = CategoryTheory.CategoryStruct.id (F.obj (X.obj.X x))
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.Monoidal.μNatIso_inv_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.Monoidal] (X : C × C),
  (CategoryTheory.Functor.Monoidal.μNatIso F).inv.app X = CategoryTheory.Functor.OplaxMonoidal.δ F X.1 X.2
-- Mathlib.RingTheory.Spectrum.Prime.FreeLocus
Module.rankAtStalk_isBaseChange : ∀ {R : Type uR} {M : Type uM} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Module.Flat R M]
  [Module.Finite R M] {S : Type u_1} {Mₛ : Type u_2} [inst_5 : CommRing S] [inst_6 : Algebra R S]
  [inst_7 : AddCommGroup Mₛ] [inst_8 : Module R Mₛ] [inst_9 : Module S Mₛ] [inst_10 : IsScalarTower R S Mₛ]
  {f : M →ₗ[R] Mₛ},
  IsBaseChange S f →
    ∀ (p : PrimeSpectrum S), Module.rankAtStalk Mₛ p = Module.rankAtStalk M (PrimeSpectrum.comap (algebraMap R S) p)
-- Mathlib.Algebra.Notation.Pi.Defs
Pi.mul_comp : ∀ {α : Type u_2} {β : Type u_3} {M : Type u_7} [inst : Mul M] (f g : β → M) (z : α → β), (f * g) ∘ z = f ∘ z * g ∘ z
-- Mathlib.RingTheory.DedekindDomain.Factorization
/-- The ideal `I` equals the finprod `∏_v v^(val_v(I))`.  -/
Ideal.finprod_heightOneSpectrum_factorization : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] {I : Ideal R},
  I ≠ 0 → ∏ᶠ (v : IsDedekindDomain.HeightOneSpectrum R), v.maxPowDividing I = I
-- Mathlib.Analysis.Normed.Group.AddTorsor
nndist_vadd_cancel_right : ∀ {V : Type u_2} {P : Type u_3} [inst : SeminormedAddCommGroup V] [inst_1 : PseudoMetricSpace P]
  [inst_2 : NormedAddTorsor V P] (v₁ v₂ : V) (x : P), nndist (v₁ +ᵥ x) (v₂ +ᵥ x) = nndist v₁ v₂
-- Lean.Language.Basic
/-- Promise of snapshot value for the current document. When resolved, the language server will
report its result even before the current elaborator invocation has finished.
 -/
Lean.Language.SnapshotBundle.new : {α : Type} → Lean.Language.SnapshotBundle α → IO.Promise α
-- Mathlib.Data.List.SplitBy
List.flatten_splitBy : ∀ {α : Type u_1} (r : α → α → Bool) (l : List α), (List.splitBy r l).flatten = l
-- Std.Tactic.BVDecide.LRAT.Internal.Entails
/-- `a ⊨ f` reads formula `f` is true under assignment `a`.
 -/
Std.Tactic.BVDecide.LRAT.Internal.«term_⊨_» : Lean.TrailingParserDescr
-- Mathlib.Combinatorics.Quiver.ReflQuiver
CategoryTheory.ReflQuiver.discreteReflQuiver : (V : Type u) → CategoryTheory.ReflQuiver (CategoryTheory.Discrete V)
-- Mathlib.Topology.Compactness.Lindelof
Filter.coLindelof_neBot_iff : ∀ {X : Type u} [inst : TopologicalSpace X], (Filter.coLindelof X).NeBot ↔ NonLindelofSpace X
-- Mathlib.Order.Interval.Set.Fin
Fin.image_castSucc_uIcc : ∀ {n : ℕ} (i j : Fin n), Fin.castSucc '' Set.uIcc i j = Set.uIcc i.castSucc j.castSucc
-- Init.Data.Vector.Find
Vector.find?_replicate_of_size_pos : ∀ {n : ℕ} {α : Type} {p : α → Bool} {a : α},
  0 < n → Vector.find? p (Vector.replicate n a) = if p a = true then some a else none
-- Mathlib.LinearAlgebra.TensorProduct.Graded.External
TensorProduct.gradedMul_assoc : ∀ {R : Type u_1} {ι : Type u_2} [inst : CommSemiring ι] [inst_1 : Module ι (Additive ℤˣ)] [inst_2 : DecidableEq ι]
  (𝒜 : ι → Type u_3) (ℬ : ι → Type u_4) [inst_3 : CommRing R] [inst_4 : (i : ι) → AddCommGroup (𝒜 i)]
  [inst_5 : (i : ι) → AddCommGroup (ℬ i)] [inst_6 : (i : ι) → Module R (𝒜 i)] [inst_7 : (i : ι) → Module R (ℬ i)]
  [inst_8 : DirectSum.GRing 𝒜] [inst_9 : DirectSum.GRing ℬ] [inst_10 : DirectSum.GAlgebra R 𝒜]
  [inst_11 : DirectSum.GAlgebra R ℬ] (x y z : TensorProduct R (DirectSum ι 𝒜) (DirectSum ι ℬ)),
  ((TensorProduct.gradedMul R 𝒜 ℬ) (((TensorProduct.gradedMul R 𝒜 ℬ) x) y)) z =
    ((TensorProduct.gradedMul R 𝒜 ℬ) x) (((TensorProduct.gradedMul R 𝒜 ℬ) y) z)
-- Mathlib.LinearAlgebra.RootSystem.WeylGroup
RootPairing.weylGroup.induction' : ∀ {ι : 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] (P : RootPairing ι R M N) [Nonempty ι]
  {pred : (g : P.Aut) → g ∈ P.weylGroup → Prop},
  (∀ (i : ι), pred (RootPairing.Equiv.reflection P i) ⋯) →
    (∀ (x y : P.Aut) (hx : x ∈ P.weylGroup) (hy : y ∈ P.weylGroup), pred x hx → pred y hy → pred (x * y) ⋯) →
      ∀ {x : P.Aut} (hx : x ∈ P.weylGroup), pred x hx
-- Mathlib.Algebra.GradedMonoid
/-- `GOne` implies `One (GradedMonoid A)`  -/
GradedMonoid.GOne.toOne : {ι : Type u_1} → (A : ι → Type u_2) → [inst : Zero ι] → [GradedMonoid.GOne A] → One (GradedMonoid A)
-- Mathlib.Algebra.Lie.Abelian
LieSubmodule.trivial_lie_oper_zero : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] (N : LieSubmodule R L M)
  (I : LieIdeal R L) [LieModule.IsTrivial L M], ⁅I, N⁆ = ⊥
-- Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Multiset.sum_nsmul : ∀ {M : Type u_5} [inst : AddCommMonoid M] (m : Multiset M) (n : ℕ), (n • m).sum = n • m.sum
-- Lean.Data.Json.FromToJson.Basic
Lean.instFromJsonFilePath : Lean.FromJson System.FilePath
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.ofWithBot.eq_1 : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} (boxes : Finset (WithBot (BoxIntegral.Box ι)))
  (le_of_mem : ∀ J ∈ boxes, J ≤ ↑I) (pairwise_disjoint : (↑boxes).Pairwise Disjoint),
  BoxIntegral.Prepartition.ofWithBot boxes le_of_mem pairwise_disjoint =
    { boxes := Finset.eraseNone boxes, le_of_mem' := ⋯, pairwiseDisjoint := ⋯ }
-- Mathlib.CategoryTheory.Presentable.OrthogonalReflection
CategoryTheory.OrthogonalReflection.iteration_map_succ_surjectivity : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W : CategoryTheory.MorphismProperty C} {Z : C}
  [inst_1 : CategoryTheory.Limits.HasPushouts C]
  [inst_2 : ∀ (Z : C), CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₁]
  [inst_3 : ∀ (Z : C), CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₂]
  [inst_4 :
    ∀ (Z : C), CategoryTheory.Limits.HasMulticoequalizer (CategoryTheory.OrthogonalReflection.D₂.multispanIndex W Z)]
  {κ : Cardinal.{w}} [inst_5 : OrderBot κ.ord.ToType]
  [inst_6 : CategoryTheory.Limits.HasIterationOfShape κ.ord.ToType C] [Fact κ.IsRegular] {X Y : C} (f : X ⟶ Y),
  W f →
    ∀ {j : κ.ord.ToType} (g : X ⟶ (CategoryTheory.OrthogonalReflection.iteration W Z κ).obj j),
      ∃ g',
        CategoryTheory.CategoryStruct.comp f g' =
          CategoryTheory.CategoryStruct.comp g
            ((CategoryTheory.OrthogonalReflection.iteration W Z κ).map (CategoryTheory.homOfLE ⋯))
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.IsTrail.of_cons : ∀ {V : Type u} {G : SimpleGraph V} {u v w : V} {h : G.Adj u v} {p : G.Walk v w},
  (SimpleGraph.Walk.cons h p).IsTrail → p.IsTrail
-- Mathlib.SetTheory.Cardinal.Finite
ENat.card_eq_zero_iff_empty : ∀ (α : Type u_3), ENat.card α = 0 ↔ IsEmpty α
-- Mathlib.Algebra.Module.GradedModule
DirectSum.GdistribMulAction.smul_zero : ∀ {ιA : Type u_1} {ιB : Type u_2} {A : ιA → Type u_3} {M : ιB → Type u_4} {inst : AddMonoid ιA} {inst_1 : VAdd ιA ιB}
  {inst_2 : GradedMonoid.GMonoid A} {inst_3 : (i : ιB) → AddMonoid (M i)} [self : DirectSum.GdistribMulAction A M]
  {i : ιA} {j : ιB} (a : A i), GradedMonoid.GSMul.smul a 0 = 0
-- Mathlib.Data.Sigma.Order
Sigma.Lex.noMinOrder_of_nonempty : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : Preorder ι] [inst_1 : (i : ι) → Preorder (α i)] [NoMinOrder ι]
  [∀ (i : ι), Nonempty (α i)], NoMinOrder (Σₗ (i : ι), α i)
-- Mathlib.Combinatorics.SimpleGraph.Copy
/-- **Alias** of the reverse direction of `SimpleGraph.free_congr_right`. -/
SimpleGraph.Free.congr_right : ∀ {α : Type u_4} {β : Type u_5} {γ : Type u_6} {A : SimpleGraph α} {B : SimpleGraph β} {C : SimpleGraph γ}
  (e₂ : B ≃g C), A.Free C → A.Free B
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.flipEquivalence_counitIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C],
  CategoryTheory.Square.flipEquivalence.counitIso =
    CategoryTheory.Iso.refl (CategoryTheory.Square.flipFunctor.comp CategoryTheory.Square.flipFunctor)
-- Mathlib.LinearAlgebra.Matrix.ConjTranspose
Matrix.conjTranspose_ofNat : ∀ {n : Type u_3} {α : Type v} [inst : DecidableEq n] [inst_1 : NonAssocSemiring α] [inst_2 : StarRing α] (d : ℕ)
  [inst_3 : d.AtLeastTwo], (OfNat.ofNat d).conjTranspose = OfNat.ofNat d
-- Mathlib.Algebra.Module.ZLattice.Basic
ZSpan.measure_fundamentalDomain : ∀ {E : Type u_1} {ι : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (b : Module.Basis ι ℝ E)
  [inst_2 : Fintype ι] [inst_3 : DecidableEq ι] [inst_4 : MeasurableSpace E] (μ : MeasureTheory.Measure E)
  [BorelSpace E] [μ.IsAddHaarMeasure] (b₀ : Module.Basis ι ℝ E),
  μ (ZSpan.fundamentalDomain b) = ENNReal.ofReal |b₀.det ⇑b| * μ (ZSpan.fundamentalDomain b₀)
-- Mathlib.Algebra.Group.Submonoid.Saturation
SaturatedSubmonoid.sSup_def : ∀ {M : Type u_1} [inst : MulOneClass M] {f : Set (SaturatedSubmonoid M)},
  sSup f = (sSup (SaturatedSubmonoid.toSubmonoid '' f)).saturation
-- Mathlib.Algebra.Homology.Embedding.ExtendHomology
HomologicalComplex.extend.leftHomologyData_K : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C c) (e : c.Embedding c') {i j k : ι}
  {i' j' k' : ι'} (hj' : e.f j = j') (hi : c.prev j = i) (hi' : c'.prev j' = i') (hk : c.next j = k)
  (hk' : c'.next j' = k') (h : (K.sc' i j k).LeftHomologyData),
  (HomologicalComplex.extend.leftHomologyData K e hj' hi hi' hk hk' h).K = h.K
-- Mathlib.AlgebraicGeometry.Morphisms.Integral
AlgebraicGeometry.IsIntegralHom.instHasOfPostcompPropertySchemeIsSeparated : CategoryTheory.MorphismProperty.HasOfPostcompProperty @AlgebraicGeometry.IsIntegralHom @AlgebraicGeometry.IsSeparated
-- Lean.Meta.AbstractMVars
_private.Lean.Meta.AbstractMVars.0.Lean.Meta.AbstractMVars.abstractLevelMVars : Lean.Level → Lean.Meta.AbstractMVars.M Lean.Level
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.opFunctorCompSnd_inv_app : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T)
  (R : CategoryTheory.Functor B T) (X : (CategoryTheory.Comma L R)ᵒᵖ),
  (CategoryTheory.Comma.opFunctorCompSnd L R).inv.app X =
    CategoryTheory.CategoryStruct.id (Opposite.op (Opposite.unop X).left)
-- Mathlib.RingTheory.Spectrum.Prime.Basic
PrimeSpectrum.vanishingIdeal_iUnion : ∀ {R : Type u} [inst : CommSemiring R] {ι : Sort u_1} (t : ι → Set (PrimeSpectrum R)),
  PrimeSpectrum.vanishingIdeal (⋃ i, t i) = ⨅ i, PrimeSpectrum.vanishingIdeal (t i)
-- Init.Data.List.MinMaxOn
List.minOn_id : ∀ {α : Type u_1} [inst : Min α] [inst_1 : LE α] [inst_2 : DecidableLE α] [Std.LawfulOrderLeftLeaningMin α] {xs : List α}
  (h : xs ≠ []), List.minOn id xs h = xs.min h
-- Mathlib.Probability.Distributions.Gaussian.Real
/-- If `X` is a real random variable with Gaussian law with mean `μ` and variance `v`, then `y + X`
has Gaussian law with mean `μ + y` and variance `v`.  -/
ProbabilityTheory.gaussianReal_const_add : ∀ {μ : ℝ} {v : NNReal} {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X : Ω → ℝ},
  ProbabilityTheory.HasLaw X (ProbabilityTheory.gaussianReal μ v) P →
    ∀ (y : ℝ), ProbabilityTheory.HasLaw (fun ω => y + X ω) (ProbabilityTheory.gaussianReal (μ + y) v) P
-- Mathlib.ModelTheory.Algebra.Field.Basic
FirstOrder.Field.FieldAxiom.toSentence.eq_5 : FirstOrder.Field.FieldAxiom.mulComm.toSentence =
  (((FirstOrder.Language.var ∘ Sum.inr) 0 * (FirstOrder.Language.var ∘ Sum.inr) 1).bdEqual
        ((FirstOrder.Language.var ∘ Sum.inr) 1 * (FirstOrder.Language.var ∘ Sum.inr) 0)).all.all
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get?_ofList_of_contains_eq_false : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] {l : List (α × β)}
  {k : α},
  (List.map Prod.fst l).contains k = false → Std.DHashMap.Raw.Const.get? (Std.DHashMap.Raw.Const.ofList l) k = none