mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.Std.DHashMap.Internal.Raw₀.insertMany.eq_1 : ∀ {α : Type u} {β : α → Type v} {ρ : Type w} [inst : ForIn Id ρ ((a : α) × β a)] [inst_1 : BEq α] [inst_2 : Hashable α]
  (m : Std.DHashMap.Internal.Raw₀ α β) (l : ρ),
  m.insertMany l =
    (have r := ⟨m, ⋯⟩;
      do
      let __s ←
        forIn l r fun x __s =>
            let r := __s;
            match x with
            | ⟨a, b⟩ =>
              have r := ⟨(↑r).insert a b, ⋯⟩;
              pure (ForInStep.yield r)
      have r :
        { m' //
          ∀ (P : Std.DHashMap.Internal.Raw₀ α β → Prop),
            (∀ {m'' : Std.DHashMap.Internal.Raw₀ α β} {a : α} {b : β a}, P m'' → P (m''.insert a b)) → P m → P m' } :=
        __s
      pure r).run
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
IntermediateField.isAlgebraic_adjoin_simple : ∀ {K : Type u} [inst : Field K] {L : Type u_3} [inst_1 : Field L] [inst_2 : Algebra K L] {x : L},
  IsIntegral K x → Algebra.IsAlgebraic K ↥K⟮x⟯
-- Init.Data.Range.Polymorphic.SInt
_private.Init.Data.Range.Polymorphic.SInt.0.HasModel.instRxiHasSize : {α : Type u} →
  [inst : LE α] →
    [inst_1 : LT α] →
      {β : Type v} →
        [inst_2 : LE β] →
          [inst_3 : LT β] →
            [inst_4 : Std.PRange.UpwardEnumerable β] →
              [inst_5 : Std.PRange.LawfulUpwardEnumerable β] →
                [inst_6 : Std.PRange.LawfulUpwardEnumerableLE β] →
                  [inst_7 : Std.PRange.LawfulUpwardEnumerableLT β] →
                    [m : HasModel✝ α β] → [Std.Rxi.HasSize β] → Std.Rxi.HasSize α
-- Mathlib.Algebra.Group.AddChar
AddChar.compAddMonoidHom_injective_left : ∀ {A : Type u_1} {B : Type u_2} {M : Type u_3} [inst : AddMonoid A] [inst_1 : AddMonoid B] [inst_2 : Monoid M]
  (f : A →+ B), Function.Surjective ⇑f → Function.Injective fun ψ => ψ.compAddMonoidHom f
-- Init.Data.BitVec.Lemmas
BitVec.toNat_ofInt : ∀ {n : ℕ} (i : ℤ), (BitVec.ofInt n i).toNat = (i % ↑(2 ^ n)).toNat
-- Mathlib.Dynamics.Ergodic.RadonNikodym
/-- The absolutely continuous part of a finite invariant measure of a self-map
with respect to a σ-finite invariant measure is an invariant measure.  -/
MeasureTheory.MeasurePreserving.withDensity_rnDeriv : ∀ {X : Type u_1} {m : MeasurableSpace X} {μ ν : MeasureTheory.Measure X} [MeasureTheory.IsFiniteMeasure μ]
  [MeasureTheory.SigmaFinite ν] {f : X → X},
  MeasureTheory.MeasurePreserving f μ μ →
    MeasureTheory.MeasurePreserving f ν ν →
      MeasureTheory.MeasurePreserving f (ν.withDensity (μ.rnDeriv ν)) (ν.withDensity (μ.rnDeriv ν))
-- Lean.Elab.Tactic.RCases
/-- The terminating continuation used in `rcasesCore` and `rcasesContinue`. We specialize the type
`α` to `Array MVarId` to collect the list of goals, and given the list of `clears`, it attempts to
clear them from the goal and adds the goal to the list.
 -/
_private.Lean.Elab.Tactic.RCases.0.Lean.Elab.Tactic.RCases.finish : optParam (Array (Lean.Ident × Lean.FVarId)) #[] →
  Lean.MVarId → Lean.Meta.FVarSubst → Array Lean.FVarId → Array Lean.MVarId → Lean.Elab.TermElabM (Array Lean.MVarId)
-- Mathlib.Algebra.Homology.DifferentialObject
CategoryTheory.DifferentialObject.d_squared_apply : ∀ {β : Type u_1} [inst : AddCommGroup β] {b : β} {V : Type u_2} [inst_1 : CategoryTheory.Category.{v_1, u_2} V]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms V]
  (X : CategoryTheory.DifferentialObject ℤ (CategoryTheory.GradedObjectWithShift b V)) {x : β},
  CategoryTheory.CategoryStruct.comp (X.d x) (X.d ((fun b_1 => b_1 + { as := 1 }.as • b) x)) = 0
-- Mathlib.Topology.Compactness.Lindelof
/-- Countable topological spaces are Lindelof.  -/
Countable.LindelofSpace : ∀ {X : Type u} [inst : TopologicalSpace X] [Countable X], LindelofSpace X
-- Mathlib.Analysis.SpecialFunctions.Gamma.Basic
_private.Mathlib.Analysis.SpecialFunctions.Gamma.Basic.0.Complex.Gamma_integrand_deriv_integrable_A : ∀ {s : ℂ},
  0 < s.re → ∀ {X : ℝ}, 0 ≤ X → IntervalIntegrable (fun x => -(↑(Real.exp (-x)) * ↑x ^ s)) MeasureTheory.volume 0 X
-- Mathlib.Data.WSeq.Relation
/-- lift a relation to a relation over weak sequences  -/
Stream'.WSeq.LiftRelO : {α : Type u} →
  {β : Type v} →
    (α → β → Prop) →
      (Stream'.WSeq α → Stream'.WSeq β → Prop) → Option (α × Stream'.WSeq α) → Option (β × Stream'.WSeq β) → Prop
-- Mathlib.Analysis.LocallyConvex.Bounded
Bornology.isVonNBounded_pi_iff : ∀ {𝕜 : Type u_6} {ι : Type u_7} {E : ι → Type u_8} [inst : NormedDivisionRing 𝕜] [inst_1 : (i : ι) → AddCommGroup (E i)]
  [inst_2 : (i : ι) → Module 𝕜 (E i)] [inst_3 : (i : ι) → TopologicalSpace (E i)] {S : Set ((i : ι) → E i)},
  Bornology.IsVonNBounded 𝕜 S ↔ ∀ (i : ι), Bornology.IsVonNBounded 𝕜 (Function.eval i '' S)
-- Mathlib.CategoryTheory.Opposites
/-- A functor is fully faithful when its opposite is fully faithful.  -/
CategoryTheory.Functor.FullyFaithful.unop : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ} → F.FullyFaithful → F.unop.FullyFaithful
-- Mathlib.Topology.Algebra.Monoid
/-- If a submonoid of a topological monoid is commutative, then so is its topological closure.  -/
Submonoid.commMonoidTopologicalClosure : {M : Type u_3} →
  [inst : TopologicalSpace M] →
    [inst_1 : Monoid M] →
      [inst_2 : SeparatelyContinuousMul M] →
        [T2Space M] → (s : Submonoid M) → (∀ (x y : ↥s), x * y = y * x) → CommMonoid ↥s.topologicalClosure
-- Mathlib.Probability.Distributions.Gaussian.Fernique
/-- Eta-expanded form of `ProbabilityTheory.IsGaussian.integrable_id` -/
ProbabilityTheory.IsGaussian.integrable_fun_id : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E]
  {μ : MeasureTheory.Measure E} [ProbabilityTheory.IsGaussian μ] [CompleteSpace E] [SecondCountableTopology E],
  MeasureTheory.Integrable (fun x => x) μ
-- Mathlib.Algebra.Order.Group.Abs
neg_le_of_abs_le : ∀ {G : Type u_1} [inst : AddCommGroup G] [inst_1 : LinearOrder G] [IsOrderedAddMonoid G] {a b : G}, |a| ≤ b → -b ≤ a
-- Lean.Elab.Syntax
/-- Elaborates the given `syntax` command and returns the new node kind.  -/
Lean.Elab.Command.elabSyntax : Lean.Syntax → Lean.Elab.Command.CommandElabM Lean.Name
-- Mathlib.Order.Filter.Ker
Filter.ker_principal : ∀ {α : Type u_2} (s : Set α), (Filter.principal s).ker = s
-- Mathlib.GroupTheory.PGroup
IsPGroup.orderOf_coprime : ∀ {p : ℕ} {G : Type u_1} [inst : Group G], IsPGroup p G → ∀ {n : ℕ}, p.Coprime n → ∀ (g : G), (orderOf g).Coprime n
-- Batteries.Data.String.Lemmas
_private.Batteries.Data.String.Lemmas.0.String.Legacy.Iterator.nextn.eq_def : ∀ (x : String.Legacy.Iterator) (x_1 : ℕ),
  x.nextn x_1 =
    match x, x_1 with
    | it, 0 => it
    | it, i.succ => it.next.nextn i
-- Mathlib.Analysis.Complex.HasPrimitives
/-- **Morera's theorem for a disk** On a disk, a continuous function whose integrals on rectangles
vanish, has primitives.  -/
Complex.IsConservativeOn.isExactOn_ball : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {c : ℂ} {r : ℝ} {f : ℂ → E} [CompleteSpace E],
  ContinuousOn f (Metric.ball c r) →
    Complex.IsConservativeOn f (Metric.ball c r) → Complex.IsExactOn f (Metric.ball c r)
-- Mathlib.Data.Matrix.Mul
neg_dotProduct_neg : ∀ {m : Type u_2} {α : Type v} [inst : Fintype m] [inst_1 : NonUnitalNonAssocRing α] (v w : m → α), -v ⬝ᵥ -w = v ⬝ᵥ w
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.Homotopy.ext_iff : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {inst_1 : CategoryTheory.Preadditive C}
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ₁ φ₂ : S₁ ⟶ S₂} {x y : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂},
  x = y ↔ x.h₀ = y.h₀ ∧ x.h₁ = y.h₁ ∧ x.h₂ = y.h₂ ∧ x.h₃ = y.h₃
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
MeasureTheory.JordanDecomposition.posPart_finite : ∀ {α : Type u_2} [inst : MeasurableSpace α] (self : MeasureTheory.JordanDecomposition α),
  MeasureTheory.IsFiniteMeasure self.posPart
-- Init.Data.Order.Ord
Std.LawfulBEqCmp.lawfulBEq : ∀ {α : Type u} [inst : BEq α] {cmp : α → α → Ordering} [inst_1 : Std.LawfulBEqCmp cmp] [Std.LawfulEqCmp cmp],
  LawfulBEq α
-- Mathlib.Geometry.Manifold.Algebra.Monoid
/-- Left multiplication by `g`. It is meant to mimic the usual notation in Lie groups.
Used mostly through the notation `𝑳`.
Lemmas involving `smoothLeftMul` with the notation `𝑳` usually use `L` instead of `𝑳` in the
names.  -/
LieGroup.«term𝑳» : Lean.ParserDescr
-- Mathlib.Topology.CWComplex.Classical.Finite
Topology.CWComplex.mkFiniteType_cell : ∀ {X : Type u} [inst : TopologicalSpace X] (C : Set X) (cell : ℕ → Type u)
  (map : (n : ℕ) → cell n → PartialEquiv (Fin n → ℝ) X) (finite_cell : ∀ (n : ℕ), Finite (cell n))
  (source_eq : ∀ (n : ℕ) (i : cell n), (map n i).source = Metric.ball 0 1)
  (continuousOn : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i)) (Metric.closedBall 0 1))
  (continuousOn_symm : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i).symm) (map n i).target)
  (pairwiseDisjoint' : Set.univ.PairwiseDisjoint fun ni => ↑(map ni.fst ni.snd) '' Metric.ball 0 1)
  (mapsTo :
    ∀ (n : ℕ) (i : cell n),
      Set.MapsTo (↑(map n i)) (Metric.sphere 0 1) (⋃ m, ⋃ (_ : m < n), ⋃ j, ↑(map m j) '' Metric.closedBall 0 1))
  (closed' : ∀ A ⊆ C, (∀ (n : ℕ) (j : cell n), IsClosed (A ∩ ↑(map n j) '' Metric.closedBall 0 1)) → IsClosed A)
  (union' : ⋃ n, ⋃ j, ↑(map n j) '' Metric.closedBall 0 1 = C) (n : ℕ), Topology.CWComplex.cell C n = cell n
-- Mathlib.Algebra.BigOperators.Balance
Fintype.balance_zero : ∀ {ι : Type u_1} {G : Type u_4} [inst : Fintype ι] [inst_1 : AddCommGroup G] [inst_2 : Module ℚ≥0 G],
  Fintype.balance 0 = 0
-- Mathlib.Algebra.Group.Basic
eq_mul_inv_of_mul_eq : ∀ {G : Type u_3} [inst : Group G] {a b c : G}, a * c = b → a = b * c⁻¹
-- Mathlib.Data.Sum.Order
Sum.not_inl_lt_inr : ∀ {α : Type u_1} {β : Type u_2} [inst : LT α] [inst_1 : LT β] {a : α} {b : β}, ¬Sum.inl b < Sum.inr a
-- Mathlib.RingTheory.Localization.LocalizationLocalization
IsLocalization.localizationLocalizationSubmodule.eq_1 : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] (N : Submonoid S),
  IsLocalization.localizationLocalizationSubmodule M N =
    Submonoid.comap (algebraMap R S) (N ⊔ Submonoid.map (algebraMap R S) M)
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
CategoryTheory.Oplax.OplaxTrans.mk.sizeOf_spec : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.OplaxFunctor B C} [inst_2 : SizeOf B] [inst_3 : SizeOf C] (app : (a : B) → F.obj a ⟶ G.obj a)
  (naturality :
    {a b : B} →
      (f : a ⟶ b) →
        CategoryTheory.CategoryStruct.comp (F.map f) (app b) ⟶ CategoryTheory.CategoryStruct.comp (app a) (G.map f))
  (naturality_naturality :
    autoParam
      (∀ {a b : B} {f g : a ⟶ b} (η : f ⟶ g),
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.map₂ η) (app b)) (naturality g) =
          CategoryTheory.CategoryStruct.comp (naturality f) (CategoryTheory.Bicategory.whiskerLeft (app a) (G.map₂ η)))
      CategoryTheory.Oplax.OplaxTrans.naturality_naturality._autoParam)
  (naturality_id :
    autoParam
      (∀ (a : B),
        CategoryTheory.CategoryStruct.comp (naturality (CategoryTheory.CategoryStruct.id a))
            (CategoryTheory.Bicategory.whiskerLeft (app a) (G.mapId a)) =
          CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapId a) (app a))
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor (app a)).hom
              (CategoryTheory.Bicategory.rightUnitor (app a)).inv))
      CategoryTheory.Oplax.OplaxTrans.naturality_id._autoParam)
  (naturality_comp :
    autoParam
      (∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c),
        CategoryTheory.CategoryStruct.comp (naturality (CategoryTheory.CategoryStruct.comp f g))
            (CategoryTheory.Bicategory.whiskerLeft (app a) (G.mapComp f g)) =
          CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapComp f g) (app c))
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f) (F.map g) (app c)).hom
              (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (naturality g))
                (CategoryTheory.CategoryStruct.comp
                  (CategoryTheory.Bicategory.associator (F.map f) (app b) (G.map g)).inv
                  (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (naturality f) (G.map g))
                    (CategoryTheory.Bicategory.associator (app a) (G.map f) (G.map g)).hom)))))
      CategoryTheory.Oplax.OplaxTrans.naturality_comp._autoParam),
  sizeOf
      { app := app, naturality := naturality, naturality_naturality := naturality_naturality,
        naturality_id := naturality_id, naturality_comp := naturality_comp } =
    1
-- Init.Data.Int.Gcd
Int.lcm_mul_right : ∀ (m n k : ℤ), (m * n).lcm (k * n) = m.lcm k * n.natAbs
-- Mathlib.Order.BooleanAlgebra.Set
/-- **Alias** of `Set.sdiff_subset_sdiff_left`. -/
Set.diff_subset_diff_left : ∀ {α : Type u_1} {s₁ s₂ t : Set α}, s₁ ⊆ s₂ → s₁ \ t ⊆ s₂ \ t
-- Batteries.Recycling.RBTree.Basic
RBTree.RBNode.any.eq_1 : ∀ {α : Type u_1} (p : α → Bool), RBTree.RBNode.any p RBTree.RBNode.nil = false
-- Lean.Compiler.IR.CompilerM
Lean.IR.LogEntry.instToFormat : Std.ToFormat Lean.IR.LogEntry
-- Lean.Data.Lsp.Basic
/-- An array of `TextEdit`s to be performed in sequence.  -/
Lean.Lsp.TextEditBatch : Type
-- Mathlib.FieldTheory.Normal.Closure
normalClosure.instIsScalarTowerSubtypeMemIntermediateFieldNormalClosure : ∀ (F : Type u_1) (K : Type u_2) (L : Type u_3) [inst : Field F] [inst_1 : Field K] [inst_2 : Field L]
  [inst_3 : Algebra F K] [inst_4 : Algebra F L] [inst_5 : Algebra K L] [inst_6 : IsScalarTower F K L],
  IsScalarTower F K ↥(IntermediateField.normalClosure F K L)
-- Mathlib.CategoryTheory.Adjunction.Reflective
CategoryTheory.Coreflective.mk : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {L : CategoryTheory.Functor C D} →
          [toFull : L.Full] →
            [toFaithful : L.Faithful] → (R : CategoryTheory.Functor D C) → (L ⊣ R) → CategoryTheory.Coreflective L
-- Mathlib.MeasureTheory.Integral.Lebesgue.Markov
MeasureTheory.lintegral_strict_mono_of_ae_le_of_frequently_ae_lt : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : α → ENNReal},
  AEMeasurable g μ →
    ∫⁻ (x : α), f x ∂μ ≠ ⊤ → f ≤ᵐ[μ] g → (∃ᵐ (x : α) ∂μ, f x ≠ g x) → ∫⁻ (x : α), f x ∂μ < ∫⁻ (x : α), g x ∂μ
-- Mathlib.GroupTheory.Nilpotent
AddSubgroup.upperCentralSeries_one : ∀ (G : Type u_2) [inst : AddGroup G], AddSubgroup.upperCentralSeries G 1 = AddSubgroup.center G
-- Init.Core
iff_def : ∀ {a b : Prop}, (a ↔ b) ↔ (a → b) ∧ (b → a)
-- Mathlib.Algebra.Homology.LeftResolution.Transport
/-- If we have an isomorphism `e : G ⋙ ι' ≅ ι`, then any `Λ : LeftResolution ι`
induces `Λ.ofCompIso e : LeftResolution ι'`.  -/
CategoryTheory.Abelian.LeftResolution.ofCompIso : {A : Type u_1} →
  {C : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_2} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_1} A] →
        {C' : Type u_4} →
          [inst_2 : CategoryTheory.Category.{v_3, u_4} C'] →
            {ι : CategoryTheory.Functor C A} →
              CategoryTheory.Abelian.LeftResolution ι →
                {ι' : CategoryTheory.Functor C' A} →
                  {G : CategoryTheory.Functor C C'} → (G.comp ι' ≅ ι) → CategoryTheory.Abelian.LeftResolution ι'
-- Mathlib.CategoryTheory.Preadditive.Projective.Basic
CategoryTheory.ProjectivePresentation.projective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} (self : CategoryTheory.ProjectivePresentation X),
  CategoryTheory.Projective self.p
-- Mathlib.CategoryTheory.ComposableArrows.Four
CategoryTheory.ComposableArrows.fourδ₄Toδ₃_app_one : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {i₀ i₁ i₂ i₃ i₄ : C} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂)
  (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₃₄ : i₂ ⟶ i₄) (h₃₄ : CategoryTheory.CategoryStruct.comp f₃ f₄ = f₃₄),
  (CategoryTheory.ComposableArrows.fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄ h₃₄).app 1 =
    CategoryTheory.CategoryStruct.id ((CategoryTheory.ComposableArrows.mk₃ f₁ f₂ f₃).obj 1)
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rco.size_eq_if_roo : ∀ {α : Type u} {r : Std.Rco α} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.Rxo.HasSize α] [Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLT α]
  [Std.Rxo.IsAlwaysFinite α] [Std.Rxo.LawfulHasSize α],
  r.size = if r.lower < r.upper then (r.lower<...r.upper).size + 1 else 0
-- Std.Http.Protocol.H1.Error
Std.Http.Protocol.H1.instBEqError.beq : Std.Http.Protocol.H1.Error → Std.Http.Protocol.H1.Error → Bool
-- Init.Data.ByteArray.Basic
ByteArray.Iterator.mk.sizeOf_spec : ∀ (array : ByteArray) (idx : ℕ), sizeOf { array := array, idx := idx } = 1 + sizeOf array + sizeOf idx
-- Mathlib.Order.SuccPred.Archimedean
le_total_of_codirected : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : SuccOrder α] [IsSuccArchimedean α] {r v₁ v₂ : α},
  r ≤ v₁ → r ≤ v₂ → v₁ ≤ v₂ ∨ v₂ ≤ v₁
-- Mathlib.MeasureTheory.Measure.Regular
/-- If the restrictions of a measure to countably many open sets covering the space are
outer regular, then the measure itself is outer regular.  -/
MeasureTheory.Measure.OuterRegular.of_restrict : ∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α] [OpensMeasurableSpace α]
  {μ : MeasureTheory.Measure α} {s : ℕ → Set α},
  (∀ (n : ℕ), (μ.restrict (s n)).OuterRegular) → (∀ (n : ℕ), IsOpen (s n)) → Set.univ ⊆ ⋃ n, s n → μ.OuterRegular
-- Mathlib.Probability.ProbabilityMassFunction.Constructions
PMF.bind_pure_comp : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (p : PMF α), p.bind (PMF.pure ∘ f) = PMF.map f p
-- Mathlib.FieldTheory.PurelyInseparable.Tower
/-- The same-universe version of `Field.lift_rank_mul_lift_sepDegree_of_isSeparable`.  -/
Field.rank_mul_sepDegree_of_isSeparable : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (K : Type v) [inst_3 : Field K]
  [inst_4 : Algebra F K] [inst_5 : Algebra E K] [IsScalarTower F E K] [Algebra.IsSeparable F E],
  Module.rank F E * Field.sepDegree E K = Field.sepDegree F K
-- Init.Meta.Defs
/-- Constructs a typed separated array from elements by adding suitable separators.
The provided array should not include the separators.
The generated separators' source location is that of the syntax returned by `getRef`.
 -/
Lean.Syntax.SepArray.ofElemsUsingRef : {m : Type → Type} → [Monad m] → [Lean.MonadRef m] → {sep : String} → Array Lean.Syntax → m (Lean.Syntax.SepArray sep)
-- Mathlib.CategoryTheory.Limits.Comma
CategoryTheory.StructuredArrow.createsLimitsOfShape : {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} →
                [CategoryTheory.Limits.PreservesLimitsOfShape J G] →
                  CategoryTheory.CreatesLimitsOfShape J (CategoryTheory.StructuredArrow.proj X G)
-- Mathlib.NumberTheory.LSeries.AbstractFuncEq
WeakFEPair.hg_top : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (self : WeakFEPair E) (r : ℝ),
  (fun x => self.g x - self.g₀) =O[Filter.atTop] fun x => x ^ r
-- Mathlib.GroupTheory.Perm.Cycle.Factors
Equiv.Perm.mem_support_cycleOf_iff' : ∀ {α : Type u_2} {f : Equiv.Perm α} {x y : α},
  f x ≠ x → ∀ [inst : DecidableEq α] [inst_1 : Fintype α], y ∈ (f.cycleOf x).support ↔ f.SameCycle x y
-- Mathlib.Algebra.Order.Ring.Abs
pow_eq_pow_iff_of_ne_zero : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] {a b : R} {n : ℕ},
  n ≠ 0 → (a ^ n = b ^ n ↔ a = b ∨ a = -b ∧ Even n)
-- Mathlib.CategoryTheory.Types.Basic
TypeCat.Hom.ext_iff : ∀ {X Y : Type u} {x y : TypeCat.Hom X Y}, x = y ↔ x.hom' = y.hom'
-- Init.Data.Fin.OverflowAware
Fin.addNat?_eq_dif : ∀ {n m : ℕ} {i : Fin n}, i.addNat? m = if h : ↑i + m < n then some ⟨↑i + m, h⟩ else none
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.size_ofList : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} [Std.TransCmp cmp] {l : List (α × β)},
  List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l → (Std.DTreeMap.Raw.Const.ofList l cmp).size = l.length
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
CategoryTheory.Limits.cospanExt_hom_app_left : ∀ {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.left = iX.hom
-- Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
SimpleGraph.Walk.lastDart_eq : ∀ {V : Type u} {G : SimpleGraph V} {v w : V} {p : G.Walk v w} (h₁ : ¬p.Nil) (h₂ : 0 < p.darts.length),
  p.lastDart h₁ = p.darts[p.darts.length - 1]
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
IsFreeGroup.lift_symm_apply : ∀ {G : Type u_1} [inst : Group G] [inst_1 : IsFreeGroup G] {H : Type u_2} [inst_2 : Group H] (f : G →* H)
  (a : IsFreeGroup.Generators G), IsFreeGroup.lift.symm f a = f (IsFreeGroup.of a)
-- Mathlib.SetTheory.Cardinal.Defs
Cardinal.mk_congr_lift : ∀ {α : Type u} {β : Type v} (e : α ≃ β), Cardinal.lift.{v, u} (Cardinal.mk α) = Cardinal.lift.{u, v} (Cardinal.mk β)
-- Mathlib.Tactic.TacticAnalysis.Declarations
_private.Mathlib.Tactic.TacticAnalysis.Declarations.0.Mathlib.TacticAnalysis.TerminalReplacementOutcome.remainingGoals.sizeOf_spec : ∀ (stx : Lean.TSyntax `tactic) (goals : List Lean.MessageData),
  sizeOf (Mathlib.TacticAnalysis.TerminalReplacementOutcome.remainingGoals✝ stx goals) = 1 + sizeOf stx + sizeOf goals
-- Std.Time.Zoned
/-- Converts a `PlainDate` to a `Timestamp` using the `ZoneRules`.
 -/
Std.Time.PlainDate.toTimestamp : Std.Time.PlainDate → Std.Time.TimeZone.ZoneRules → Std.Time.Timestamp
-- Init.Data.SInt.Bitwise
Int64.xor_self : ∀ {a : Int64}, a ^^^ a = 0
-- Lean.Declaration
Lean.ConstantInfo.isDefinition : Lean.ConstantInfo → Bool
-- Mathlib.Geometry.Manifold.VectorBundle.FiberwiseLinear
mem_contMDiffFiberwiseLinear_iff : ∀ {𝕜 : Type u_1} (B : Type u_2) (F : Type u_3) [inst : TopologicalSpace B] [inst_1 : NontriviallyNormedField 𝕜]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace 𝕜 F] {EB : Type u_4} [inst_4 : NormedAddCommGroup EB]
  [inst_5 : NormedSpace 𝕜 EB] {HB : Type u_5} [inst_6 : TopologicalSpace HB] [inst_7 : ChartedSpace HB B]
  (IB : ModelWithCorners 𝕜 EB HB) {n : WithTop ℕ∞} (e : OpenPartialHomeomorph (B × F) (B × F)),
  e ∈ contMDiffFiberwiseLinear B F IB n ↔
    ∃ φ U,
      ∃ (hU : IsOpen U) (hφ : ContMDiffOn IB (modelWithCornersSelf 𝕜 (F →L[𝕜] F)) n (fun x => ↑(φ x)) U) (h2φ :
        ContMDiffOn IB (modelWithCornersSelf 𝕜 (F →L[𝕜] F)) n (fun x => ↑(φ x).symm) U),
        e.EqOnSource (FiberwiseLinear.openPartialHomeomorph φ hU ⋯ ⋯)
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
/-- If a function is the greatest lower bound of countably many measurable functions,
then it is measurable.  -/
Measurable.isGLB : ∀ {α : Type u_1} {δ : Type u_4} [inst : TopologicalSpace α] {mα : MeasurableSpace α} [BorelSpace α]
  {mδ : MeasurableSpace δ} [inst_2 : LinearOrder α] [OrderTopology α] [SecondCountableTopology α] {ι : Sort u_5}
  [Countable ι] {f : ι → δ → α} {g : δ → α},
  (∀ (i : ι), Measurable (f i)) → (∀ (b : δ), IsGLB {a | ∃ i, f i b = a} (g b)) → Measurable g