mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Array.Attach
Array.attach_append : ∀ {α : Type u_1} {xs ys : Array α},
  (xs ++ ys).attach =
    Array.map
        (fun x =>
          match x with
          | ⟨x, h⟩ => ⟨x, ⋯⟩)
        xs.attach ++
      Array.map
        (fun x =>
          match x with
          | ⟨x, h⟩ => ⟨x, ⋯⟩)
        ys.attach
-- Mathlib.CategoryTheory.MorphismProperty.Comma
/-- Make an isomorphism in `P.Over Q X` from an isomorphism in `T` with compatibilities.  -/
CategoryTheory.MorphismProperty.Over.isoMk : {T : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} T] →
    {P Q : CategoryTheory.MorphismProperty T} →
      {X : T} →
        [inst_1 : Q.IsMultiplicative] →
          [Q.RespectsIso] →
            {A B : P.Over Q X} →
              (f : A.left ≅ B.left) →
                autoParam (CategoryTheory.CategoryStruct.comp f.hom B.hom = A.hom)
                    CategoryTheory.MorphismProperty.Over.isoMk._auto_1 →
                  (A ≅ B)
-- Lean.Meta.IndPredBelow
/-- Generates the auxiliary lemmas `below` and `brecOn` for a recursive inductive predicate.  -/
Lean.Meta.IndPredBelow.mkBelow : Lean.Name → Lean.MetaM Unit
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.tensor_id_comp_id_tensor_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {W X Y Z : C}
  (f : W ⟶ X) (g : Y ⟶ Z) {Z_1 : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj Z X ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom g (CategoryTheory.CategoryStruct.id W))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id Z) f) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom g f) h
-- Mathlib.RingTheory.LocalRing.ResidueField.Defs
IsLocalRing.instInhabitedResidueField : (R : Type u_1) → [inst : CommRing R] → [inst_1 : IsLocalRing R] → Inhabited (IsLocalRing.ResidueField R)
-- Mathlib.CategoryTheory.Join.Pseudofunctor
/-- The pseudofunctor sending `C` to `C ⋆ D`.  -/
CategoryTheory.Join.pseudofunctorLeft : (D : Type u₂) →
  [CategoryTheory.Category.{v₂, u₂} D] → CategoryTheory.Pseudofunctor CategoryTheory.Cat CategoryTheory.Cat
-- Mathlib.Topology.Separation.Basic
T1Space.t0Space : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T1Space X], T0Space X
-- Mathlib.Geometry.Manifold.VectorField.LieBracket
VectorField.mlieBracket_const_smul_right : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {x : M} {V W : (x : M) → TangentSpace I x} {c : 𝕜}
  [inst_6 : IsManifold I 2 M] [CompleteSpace E],
  MDiffAt (T% W) x → VectorField.mlieBracket I V (c • W) x = c • VectorField.mlieBracket I V W x
-- Init.Data.UInt.Lemmas
UInt8.toFin_ofNatTruncate_of_le : ∀ {n : ℕ}, UInt8.size ≤ n → (UInt8.ofNatClamp n).toFin = ⟨UInt8.size - 1, UInt8.toFin_ofNatClamp_of_le._proof_1⟩
-- Mathlib.Algebra.Category.AlgCat.Limits
AlgCat.algebraObj : {R : Type u} →
  [inst : CommRing R] →
    {J : Type v} →
      [inst_1 : CategoryTheory.Category.{t, v} J] →
        (F : CategoryTheory.Functor J (AlgCat R)) →
          (j : J) → Algebra R ((F.comp (CategoryTheory.forget (AlgCat R))).obj j)
-- Mathlib.Analysis.Calculus.Deriv.Mul
deriv_const_mul_field' : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {𝕜' : Type u_2} [inst_1 : NormedDivisionRing 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {v : 𝕜 → 𝕜'} (u : 𝕜'), (deriv fun x => u * v x) = fun x => u * deriv v x
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Finset.sum_le_sum_of_subset_of_nonneg : ∀ {ι : Type u_1} {N : Type u_5} [inst : AddCommMonoid N] [inst_1 : Preorder N] {f : ι → N} {s t : Finset ι}
  [AddLeftMono N], s ⊆ t → (∀ i ∈ t, i ∉ s → 0 ≤ f i) → ∑ i ∈ s, f i ≤ ∑ i ∈ t, f i
-- Init.Data.Range.Polymorphic.UInt
UInt32.instUpwardEnumerable : Std.PRange.UpwardEnumerable UInt32
-- Mathlib.CategoryTheory.Action.Concrete
Action.ofMulAction_V : ∀ (G : Type u_1) (H : Type u) [inst : Monoid G] [inst_1 : MulAction G H], (Action.ofMulAction G H).V = H
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
IsUniformAddGroup.uniformContinuous_sub : ∀ {α : Type u_3} {inst : UniformSpace α} {inst_1 : AddGroup α} [self : IsUniformAddGroup α],
  UniformContinuous fun p => p.1 - p.2
-- Mathlib.Topology.Algebra.Order.Field
/-- The function `r ↦ r⁻¹` tends to `0` on the left as `r → -∞`.  -/
tendsto_inv_atBot_nhdsLT_zero : ∀ {𝕜 : Type u_1} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [inst_3 : TopologicalSpace 𝕜]
  [OrderTopology 𝕜], Filter.Tendsto (fun r => r⁻¹) Filter.atBot (nhdsWithin 0 (Set.Iio 0))
-- Mathlib.CategoryTheory.LocallyCartesianClosed.Over
CategoryTheory.toOverUnitPullback_inv_app_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (X X_1 : C),
  ((CategoryTheory.toOverUnitPullback X).inv.app X_1).left =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj X_1 X)
-- Mathlib.Data.Seq.Defs
/-- Separate a sequence of pairs into two sequences  -/
Stream'.Seq.unzip : {α : Type u} → {β : Type v} → Stream'.Seq (α × β) → Stream'.Seq α × Stream'.Seq β
-- Mathlib.Data.String.Basic
/-- Induction on `String.ltb`.  -/
String.ltb.inductionOn : {motive : String.Legacy.Iterator → String.Legacy.Iterator → Sort u} →
  (it₁ it₂ : String.Legacy.Iterator) →
    ((s₁ s₂ : String) →
        (i₁ i₂ : String.Pos.Raw) →
          { s := s₂, i := i₂ }.hasNext = true →
            { s := s₁, i := i₁ }.hasNext = true →
              String.Pos.Raw.get s₁ i₁ = String.Pos.Raw.get s₂ i₂ →
                motive { s := s₁, i := i₁ }.next { s := s₂, i := i₂ }.next →
                  motive { s := s₁, i := i₁ } { s := s₂, i := i₂ }) →
      ((s₁ s₂ : String) →
          (i₁ i₂ : String.Pos.Raw) →
            { s := s₂, i := i₂ }.hasNext = true →
              { s := s₁, i := i₁ }.hasNext = true →
                ¬String.Pos.Raw.get s₁ i₁ = String.Pos.Raw.get s₂ i₂ →
                  motive { s := s₁, i := i₁ } { s := s₂, i := i₂ }) →
        ((s₁ s₂ : String) →
            (i₁ i₂ : String.Pos.Raw) →
              { s := s₂, i := i₂ }.hasNext = true →
                ¬{ s := s₁, i := i₁ }.hasNext = true → motive { s := s₁, i := i₁ } { s := s₂, i := i₂ }) →
          ((s₁ s₂ : String) →
              (i₁ i₂ : String.Pos.Raw) →
                ¬{ s := s₂, i := i₂ }.hasNext = true → motive { s := s₁, i := i₁ } { s := s₂, i := i₂ }) →
            motive it₁ it₂
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getElem!_diff_of_not_mem_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  [inst_1 : Inhabited β], k ∉ t₁ → (t₁ \ t₂)[k]! = default
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
NonUnitalSubsemiring.coe_sInf : ∀ {R : Type u} [inst : NonUnitalNonAssocSemiring R] (S : Set (NonUnitalSubsemiring R)), ↑(sInf S) = ⋂ s ∈ S, ↑s
-- Mathlib.Combinatorics.Enumerative.Composition
/-- If one splits a list along a composition, and then flattens the sublists, one gets back the
original list.  -/
List.flatten_splitWrtComposition : ∀ {α : Type u_1} (l : List α) (c : Composition l.length), (l.splitWrtComposition c).flatten = l
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.roleExpandersForUnsafe : Lean.Ident →
  Lean.Elab.TermElabM
    (Array
      (Lean.Name ×
        (Lean.TSyntaxArray `inline →
          StateT (Array (Lean.TSyntax `doc_arg)) Lean.Doc.DocM (Lean.Doc.Inline Lean.ElabInline))))
-- Mathlib.Data.Finset.Defs
Finset.Subset.trans : ∀ {α : Type u_1} {s₁ s₂ s₃ : Finset α}, s₁ ⊆ s₂ → s₂ ⊆ s₃ → s₁ ⊆ s₃
-- Std.Data.DTreeMap.Internal.Operations
_private.Std.Data.DTreeMap.Internal.Operations.0.Std.DTreeMap.Internal.Impl.link2.match_1.splitter : {α : Type u_1} →
  {β : α → Type u_2} →
    (l l'' : Std.DTreeMap.Internal.Impl α β) →
      (motive : Std.DTreeMap.Internal.Impl.Tree α β (l.size + l''.size) → Sort u_3) →
        (x : Std.DTreeMap.Internal.Impl.Tree α β (l.size + l''.size)) →
          ((ℓ : Std.DTreeMap.Internal.Impl α β) →
              (hℓ₁ : ℓ.Balanced) →
                (hℓ₂ : ℓ.size = l.size + l''.size) → motive { impl := ℓ, balanced_impl := hℓ₁, size_impl := hℓ₂ }) →
            motive x
-- Lean.Widget.InteractiveCode
Lean.Widget.instFromJsonDiffTag.fromJson : Lean.Json → Except String Lean.Widget.DiffTag
-- Mathlib.Data.Finset.Insert
Finset.pair_comm : ∀ {α : Type u_1} [inst : DecidableEq α] (a b : α), {a, b} = {b, a}
-- Mathlib.Algebra.Lie.Ideal
LieHom.idealRange_eq_map : ∀ {R : Type u} {L : Type v} {L' : Type w₂} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieRing L']
  [inst_3 : LieAlgebra R L'] [inst_4 : LieAlgebra R L] (f : L →ₗ⁅R⁆ L'), f.idealRange = LieIdeal.map f ⊤
-- Mathlib.Topology.Order.OrderClosed
isOpen_lt_prod : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderClosedTopology α], IsOpen {p | p.1 < p.2}
-- Mathlib.Data.Set.Lattice
Set.iInter_mono' : ∀ {α : Type u_1} {ι : Sort u_5} {ι' : Sort u_6} {s : ι → Set α} {t : ι' → Set α},
  (∀ (j : ι'), ∃ i, s i ⊆ t j) → ⋂ i, s i ⊆ ⋂ j, t j
-- Mathlib.Order.Filter.Extr
IsExtrOn.on_subset : ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {s : Set α} {a : α} {t : Set α},
  IsExtrOn f t a → s ⊆ t → IsExtrOn f s a
-- Mathlib.AlgebraicTopology.SimplicialObject.Coskeletal
/-- A simplicial object `X` is `n`-coskeletal when it is the right Kan extension of its restriction
along `(Truncated.inclusion n).op` via the identity natural transformation.  -/
CategoryTheory.SimplicialObject.IsCoskeletal : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.SimplicialObject C → ℕ → Prop
-- Mathlib.FieldTheory.IntermediateField.Algebraic
/-- Turn an algebraic subalgebra into an intermediate field, `Algebra.IsAlgebraic` version.  -/
Algebra.IsAlgebraic.toIntermediateField : {K : Type u_1} →
  {L : Type u_2} →
    [inst : Field K] →
      [inst_1 : Field L] →
        [inst_2 : Algebra K L] → (S : Subalgebra K L) → [Algebra.IsAlgebraic K ↥S] → IntermediateField K L
-- Mathlib.Order.Filter.Basic
Filter.EventuallyEq.mul : ∀ {α : Type u} {β : Type v} [inst : Mul β] {f f' g g' : α → β} {l : Filter α},
  f =ᶠ[l] g → f' =ᶠ[l] g' → f * f' =ᶠ[l] g * g'
-- Mathlib.Algebra.Lie.Free
/-- The functor `X ↦ FreeLieAlgebra R X` from the category of types to the category of Lie
algebras over `R` is adjoint to the forgetful functor in the other direction.  -/
FreeLieAlgebra.lift : (R : Type u) →
  {X : Type v} →
    [inst : CommRing R] →
      {L : Type w} → [inst_1 : LieRing L] → [inst_2 : LieAlgebra R L] → (X → L) ≃ (FreeLieAlgebra R X →ₗ⁅R⁆ L)
-- Init.Data.BitVec.Lemmas
BitVec.msb_sshiftRight' : ∀ {w : ℕ} {x y : BitVec w}, (x.sshiftRight' y).msb = x.msb
-- Std.Data.DHashMap.Internal.Defs
/-- Inner loop of `expand`. Copies elements `source[i...*]` into `target`,
destroying `source` in the process.  -/
_private.Std.Data.DHashMap.Internal.Defs.0.Std.DHashMap.Internal.Raw₀.expand.go : {α : Type u} →
  {β : α → Type v} →
    [Hashable α] → ℕ → Array (Std.DHashMap.Internal.AssocList α β) → { d // 0 < d.size } → { d // 0 < d.size }
-- Mathlib.CategoryTheory.Dialectica.Monoidal
CategoryTheory.Dial.rightUnitorImpl_inv_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasFiniteProducts C]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C] (X : CategoryTheory.Dial C),
  X.rightUnitorImpl.inv.f =
    CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.id X.src) (CategoryTheory.Limits.terminal.from X.src)
-- Mathlib.LinearAlgebra.Prod
/-- `N` as a submodule of `M × N`.  -/
Submodule.snd : (R : Type u) →
  (M : Type v) →
    (M₂ : Type w) →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : AddCommMonoid M₂] → [inst_3 : Module R M] → [inst_4 : Module R M₂] → Submodule R (M × M₂)
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
/-- If a function is differentiable on two open sets, it is also differentiable on their union.  -/
MDifferentiableOn.union_of_isOpen : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {s t : Set M},
  MDiff[s] f → MDiff[t] f → IsOpen s → IsOpen t → MDiff[s ∪ t] f
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.instSMulZeroClass : {k : Type u_1} →
  {G : Type u_2} → [inst : AddMonoid k] → {S : Type u_3} → [SMulZeroClass S k] → SMulZeroClass S (SkewMonoidAlgebra k G)
-- Mathlib.Analysis.LocallyConvex.Separation
RCLike.geometric_hahn_banach_point_closed : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : TopologicalSpace E] [inst_1 : AddCommGroup E] [inst_2 : Module ℝ E] {t : Set E}
  {x : E} [inst_3 : RCLike 𝕜] [inst_4 : Module 𝕜 E] [IsScalarTower ℝ 𝕜 E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E]
  [LocallyConvexSpace ℝ E], Convex ℝ t → IsClosed t → x ∉ t → ∃ f u, RCLike.re (f x) < u ∧ ∀ b ∈ t, u < RCLike.re (f b)
-- Batteries.Control.AlternativeMonad
/-- Lifting preserves `failure`.  -/
LawfulAlternativeLift.monadLift_failure : ∀ {m : semiOutParam (Type u → Type v)} {n : Type u → Type w} {inst : Alternative m} {inst_1 : Alternative n}
  {inst_2 : MonadLift m n} [self : LawfulAlternativeLift m n] {α : Type u}, monadLift failure = failure
-- Init.Data.Iterators.Combinators.Monadic.Attach
_private.Init.Data.Iterators.Combinators.Monadic.Attach.0.Std.Iterators.Types.Attach.Monadic.modifyStep.eq_2 : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} [inst : Std.Iterator α m β] {P : β → Prop}
  (it : Std.IterM m { out // P out }) (it' : Std.IterM m β)
  (h : it.internalState.inner.IsPlausibleStep (Std.IterStep.skip it')),
  Std.Iterators.Types.Attach.Monadic.modifyStep it ⟨Std.IterStep.skip it', h⟩ =
    Std.IterStep.skip { internalState := { inner := it', invariant := ⋯ } }
-- Mathlib.Algebra.Homology.HomotopyCategory
/-- An additive functor induces a functor between homotopy categories.  -/
CategoryTheory.Functor.mapHomotopyCategory : {ι : Type u_2} →
  {V : Type u} →
    [inst : CategoryTheory.Category.{v, u} V] →
      [inst_1 : CategoryTheory.Preadditive V] →
        {W : Type u_3} →
          [inst_2 : CategoryTheory.Category.{v_1, u_3} W] →
            [inst_3 : CategoryTheory.Preadditive W] →
              (F : CategoryTheory.Functor V W) →
                [F.Additive] →
                  (c : ComplexShape ι) → CategoryTheory.Functor (HomotopyCategory V c) (HomotopyCategory W c)
-- Init.Data.ByteArray.Basic
ByteArray.instAppend : Append ByteArray
-- Mathlib.LinearAlgebra.TensorProduct.Associator
TensorProduct.lid_tmul : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_5} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (m : M)
  (r : R), (TensorProduct.lid R M) (r ⊗ₜ[R] m) = r • m
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.ofList_nil : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering}, Std.ExtTreeMap.ofList [] cmp = ∅
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.UseImplicitLambdaResult.postpone : Lean.Elab.Term.UseImplicitLambdaResult
-- Mathlib.Analysis.Fourier.ZMod
ZMod.dft_def : ∀ {N : ℕ} [inst : NeZero N] {E : Type u_1} [inst_1 : AddCommGroup E] [inst_2 : Module ℂ E] (Φ : ZMod N → E),
  ZMod.dft Φ = fun k => ∑ j, ZMod.stdAddChar (-(j * k)) • Φ j
-- Mathlib.Algebra.Order.Group.PosPart
oneLePart_def : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : DivInvMonoid α] (a : α), a⁺ᵐ = a ⊔ 1
-- Mathlib.CategoryTheory.Subfunctor.SubmonoidFunctor
/-- The submonoid functor defined by the preimage along a morphism of functors of monoids.  -/
CategoryTheory.SubmonoidFunctor.comap : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {M M' : CategoryTheory.Functor C MonCat} →
      (M ⟶ M') → CategoryTheory.SubmonoidFunctor M' → CategoryTheory.SubmonoidFunctor M
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
cbiInf_of_not_bddBelow : ∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompleteLinearOrder α] {p : ι → Prop} {f : (i : ι) → p i → α},
  ¬BddBelow (Set.range fun i => f ↑i ⋯) → ⨅ i, ⨅ (h : p i), f i h = sInf ∅
-- Init.Data.Bool
Bool.not_eq_self : ∀ (b : Bool), (!b) = b ↔ False
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.Ref.mk.inj : ∀ {α : Sort u_1} {content : α} {location : Lean.Syntax} {seen : Bool} {content_1 : α} {location_1 : Lean.Syntax}
  {seen_1 : Bool},
  { content := content, location := location, seen := seen } =
      { content := content_1, location := location_1, seen := seen_1 } →
    content = content_1 ∧ location = location_1 ∧ seen = seen_1
-- Mathlib.Probability.Process.LocalProperty
ProbabilityTheory.Locally.congr_simp : ∀ {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} [inst : LinearOrder ι] [inst_1 : OrderBot ι]
  [inst_2 : TopologicalSpace ι] [inst_3 : OrderTopology ι] [inst_4 : Zero E] (p p_1 : (ι → Ω → E) → Prop),
  p = p_1 →
    ∀ (𝓕 𝓕_1 : MeasureTheory.Filtration ι mΩ),
      𝓕 = 𝓕_1 →
        ∀ (X X_1 : ι → Ω → E),
          X = X_1 →
            ∀ (P P_1 : MeasureTheory.Measure Ω),
              P = P_1 → ProbabilityTheory.Locally p 𝓕 X P = ProbabilityTheory.Locally p_1 𝓕_1 X_1 P_1
-- Mathlib.Topology.Sion
/-- The minimax theorem, in the saddle point form,
when `β` is given a Dedekind-MacNeille completion `ι : β ↪o γ`  -/
Sion.DMCompletion.exists_isSaddlePointOn : ∀ {E : Type u_1} {F : Type u_2} {β : Type u_3} [inst : LinearOrder β] {X : Set E} {Y : Set F} {f : E → F → β}
  [inst_1 : TopologicalSpace E] [inst_2 : AddCommGroup E] [inst_3 : Module ℝ E] [IsTopologicalAddGroup E]
  [ContinuousSMul ℝ E],
  X.Nonempty →
    Convex ℝ X →
      IsCompact X →
        (∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X) →
          (∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y) →
            ∀ [inst_6 : TopologicalSpace F] [inst_7 : AddCommGroup F] [inst_8 : Module ℝ F] [IsTopologicalAddGroup F]
              [ContinuousSMul ℝ F],
              Convex ℝ Y →
                Y.Nonempty →
                  IsCompact Y →
                    (∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y) →
                      (∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y) →
                        ∀ [inst_11 : TopologicalSpace β] [OrderTopology β] {γ : Type u_5}
                          [inst_13 : CompleteLinearOrder γ] [DenselyOrdered γ] [inst_15 : TopologicalSpace γ]
                          [OrderTopology γ] {ι : β ↪o γ}, Continuous ⇑ι → ∃ a ∈ X, ∃ b ∈ Y, IsSaddlePointOn X Y f a b
-- Mathlib.CategoryTheory.Limits.Comma
CategoryTheory.StructuredArrow.createsLimit : {J : Type w} →
  [inst : CategoryTheory.Category.{w', w} J] →
    {A : Type u₁} →
      [inst_1 : CategoryTheory.Category.{v₁, u₁} A] →
        {T : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} T] →
            {X : T} →
              {G : CategoryTheory.Functor A T} →
                (F : CategoryTheory.Functor J (CategoryTheory.StructuredArrow X G)) →
                  [i : CategoryTheory.Limits.PreservesLimit (F.comp (CategoryTheory.StructuredArrow.proj X G)) G] →
                    CategoryTheory.CreatesLimit F (CategoryTheory.StructuredArrow.proj X G)
-- Mathlib.Topology.Homotopy.Lifting
IsQuotientCoveringMap.fundamentalGroupToMulOpposite.eq_1 : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {p : E → X} {G : Type u_4}
  [inst_2 : Group G] [inst_3 : MulAction G E] (hp : IsQuotientCoveringMap p G) {x : X} (e : ↑(p ⁻¹' {x})),
  hp.fundamentalGroupToMulOpposite e =
    { toFun := fun γ => MulOpposite.op ((hp.fiberEquivGroup e) (⋯.monodromy γ e)), map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Real.pi_div_two_eq_arcsin : ∀ {x : ℝ}, Real.pi / 2 = Real.arcsin x ↔ 1 ≤ x
-- Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
/-- The left multiplication with a `C^n` scalar function commutes with composition.  -/
ContMDiffMap.smul_comp' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_4} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {N : Type u_6}
  [inst_4 : TopologicalSpace N] [inst_5 : ChartedSpace H N] {E'' : Type u_7} [inst_6 : NormedAddCommGroup E'']
  [inst_7 : NormedSpace 𝕜 E''] {H'' : Type u_8} [inst_8 : TopologicalSpace H''] {I'' : ModelWithCorners 𝕜 E'' H''}
  {N' : Type u_9} [inst_9 : TopologicalSpace N'] [inst_10 : ChartedSpace H'' N'] {n : WithTop ℕ∞} {V : Type u_10}
  [inst_11 : NormedAddCommGroup V] [inst_12 : NormedSpace 𝕜 V] (f : ContMDiffMap I'' (modelWithCornersSelf 𝕜 𝕜) N' 𝕜 n)
  (g : ContMDiffMap I'' (modelWithCornersSelf 𝕜 V) N' V n) (h : ContMDiffMap I I'' N N' n),
  (f • g).comp h = f.comp h • g.comp h
-- Mathlib.RingTheory.LocalProperties.Exactness
bijective_of_isLocalization_isMaximal : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  (Rₚ : (p : Ideal R) → [p.IsMaximal] → Type u_3) [inst_3 : (p : Ideal R) → [inst : p.IsMaximal] → CommSemiring (Rₚ p)]
  [inst_4 : (p : Ideal R) → [inst_4 : p.IsMaximal] → Algebra R (Rₚ p)] (Sₚ : (p : Ideal R) → [p.IsMaximal] → Type u_4)
  [inst_5 : (p : Ideal R) → [inst : p.IsMaximal] → CommSemiring (Sₚ p)]
  [inst_6 : (p : Ideal R) → [inst : p.IsMaximal] → Algebra S (Sₚ p)]
  [inst_7 : (p : Ideal R) → [inst : p.IsMaximal] → Algebra (Rₚ p) (Sₚ p)]
  [inst_8 : (p : Ideal R) → [inst_8 : p.IsMaximal] → Algebra R (Sₚ p)]
  [∀ (p : Ideal R) [inst_9 : p.IsMaximal], IsScalarTower R (Rₚ p) (Sₚ p)]
  [inst_10 : ∀ (p : Ideal R) [inst_10 : p.IsMaximal], IsScalarTower R S (Sₚ p)]
  [∀ (p : Ideal R) [inst_11 : p.IsMaximal], IsLocalization.AtPrime (Rₚ p) p]
  [∀ (p : Ideal R) [inst_12 : p.IsMaximal], IsLocalizedModule.AtPrime p ↑(IsScalarTower.toAlgHom R S (Sₚ p))],
  (∀ (p : Ideal R) [inst : p.IsMaximal], Function.Bijective ⇑(algebraMap (Rₚ p) (Sₚ p))) →
    Function.Bijective ⇑(algebraMap R S)
-- Mathlib.LinearAlgebra.Dimension.StrongRankCondition
LinearMap.finrank_range_le : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [StrongRankCondition R]
  {M' : Type u_2} [inst_4 : AddCommMonoid M'] [inst_5 : Module R M'] [Module.Finite R M] (f : M →ₗ[R] M'),
  Module.finrank R ↥f.range ≤ Module.finrank R M
-- Init.Data.SInt.Lemmas
ISize.sub_self : ∀ (a : ISize), a - a = 0
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKeyD_union_of_not_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k fallback : α}, k ∉ t₂ → (t₁ ∪ t₂).getKeyD k fallback = t₁.getKeyD k fallback
-- Std.Data.HashMap.Lemmas
Std.HashMap.get?_eq_getElem? : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} {a : α}, m.get? a = m[a]?