mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.Archimedean.Class
MulArchimedeanClass.instLinearOrder.eq_1 : ∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M],
  MulArchimedeanClass.instLinearOrder =
    { le := fun a a_1 => Quot.lift (fun a₁ => Quotient.lift ((fun x1 x2 => x1 ≤ x2) a₁) ⋯ a_1) ⋯ a,
      lt := fun a a_1 => Quot.lift (fun a₁ => Quotient.lift ((fun x1 x2 => x1 < x2) a₁) ⋯ a_1) ⋯ a, le_refl := ⋯,
      le_trans := ⋯, lt_iff_le_not_ge := ⋯, le_antisymm := ⋯, min := fun a a_1 => if a ≤ a_1 then a else a_1,
      max := fun a a_1 => if a ≤ a_1 then a_1 else a, compare := fun a a_1 => compareOfLessAndEq a a_1, le_total := ⋯,
      toDecidableLE := fun a b =>
        ⋯ ▸
          (Quot.lift
              (Quot.indep fun a =>
                (fun a => Quot.recOnSubsingleton b fun a_1 => (fun a b => Classical.propDecidable (a ≤ b)) a a_1) a)
              ⋯ a).snd,
      toDecidableEq := fun a b => decidableEqOfDecidableLE a b,
      toDecidableLT := fun a b =>
        ⋯ ▸
          (Quot.lift
              (Quot.indep fun a =>
                (fun a => Quot.recOnSubsingleton b fun a_1 => (fun a b => Classical.propDecidable (a < b)) a a_1) a)
              ⋯ a).snd,
      min_def := ⋯, max_def := ⋯, compare_eq_compareOfLessAndEq := ⋯ }
-- Mathlib.Topology.MetricSpace.Thickening
Metric.thickening_closure : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {δ : ℝ} {s : Set α},
  Metric.thickening δ (closure s) = Metric.thickening δ s
-- Mathlib.Data.List.Duplicate
List.Duplicate.cons_duplicate : ∀ {α : Type u_1} {x y : α} {l : List α}, List.Duplicate x l → List.Duplicate x (y :: l)
-- Mathlib.Algebra.Module.Injective
Module.Baer.ExtensionOf.toLinearPMap_injective : ∀ {R : Type u} [inst : Ring R] {Q : Type v} [inst_1 : AddCommGroup Q] [inst_2 : Module R Q] {M : Type u_1}
  {N : Type u_2} [inst_3 : AddCommGroup M] [inst_4 : AddCommGroup N] [inst_5 : Module R M] [inst_6 : Module R N]
  {i : M →ₗ[R] N} {f : M →ₗ[R] Q}, Function.Injective Module.Baer.ExtensionOf.toLinearPMap
-- Mathlib.Topology.VectorBundle.Hom
/-- Rewrite `ContinuousLinearMap.inCoordinates` using continuous linear equivalences, in the
bundle of bilinear maps.  -/
inCoordinates_apply_eq₂ : ∀ {𝕜 : Type u_8} {B : Type u_9} {F₁ : Type u_10} {F₂ : Type u_11} {F₃ : Type u_12} [inst : NontriviallyNormedField 𝕜]
  {E₁ : B → Type u_14} [inst_1 : (x : B) → AddCommGroup (E₁ x)] [inst_2 : (x : B) → Module 𝕜 (E₁ x)]
  [inst_3 : NormedAddCommGroup F₁] [inst_4 : NormedSpace 𝕜 F₁] [inst_5 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)]
  [inst_6 : (x : B) → TopologicalSpace (E₁ x)] {E₂ : B → Type u_15} [inst_7 : (x : B) → AddCommGroup (E₂ x)]
  [inst_8 : (x : B) → Module 𝕜 (E₂ x)] [inst_9 : NormedAddCommGroup F₂] [inst_10 : NormedSpace 𝕜 F₂]
  [inst_11 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)] [inst_12 : (x : B) → TopologicalSpace (E₂ x)]
  {E₃ : B → Type u_16} [inst_13 : (x : B) → AddCommGroup (E₃ x)] [inst_14 : (x : B) → Module 𝕜 (E₃ x)]
  [inst_15 : NormedAddCommGroup F₃] [inst_16 : NormedSpace 𝕜 F₃] [inst_17 : TopologicalSpace (Bundle.TotalSpace F₃ E₃)]
  [inst_18 : (x : B) → TopologicalSpace (E₃ x)] [inst_19 : TopologicalSpace B] [inst_20 : FiberBundle F₁ E₁]
  [inst_21 : VectorBundle 𝕜 F₁ E₁] [inst_22 : FiberBundle F₂ E₂] [inst_23 : VectorBundle 𝕜 F₂ E₂]
  [inst_24 : FiberBundle F₃ E₃] [inst_25 : VectorBundle 𝕜 F₃ E₃] [inst_26 : ∀ (x : B), IsTopologicalAddGroup (E₃ x)]
  [inst_27 : ∀ (x : B), ContinuousSMul 𝕜 (E₃ x)] {x₀ x : B} {ϕ : E₁ x →L[𝕜] E₂ x →L[𝕜] E₃ x} {v : F₁} {w : F₂},
  x ∈ (trivializationAt F₁ E₁ x₀).baseSet →
    x ∈ (trivializationAt F₂ E₂ x₀).baseSet →
      x ∈ (trivializationAt F₃ E₃ x₀).baseSet →
        ((ContinuousLinearMap.inCoordinates F₁ E₁ (F₂ →L[𝕜] F₃) (fun x => E₂ x →L[𝕜] E₃ x) x₀ x x₀ x ϕ) v) w =
          (Bundle.Trivialization.linearMapAt 𝕜 (trivializationAt F₃ E₃ x₀) x)
            ((ϕ ((trivializationAt F₁ E₁ x₀).symm x v)) ((trivializationAt F₂ E₂ x₀).symm x w))
-- Std.Data.DHashMap.Internal.Model
Std.DHashMap.Internal.Raw₀.getKey_eq_getKeyₘ : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (a : α)
  (h : m.contains a = true), m.getKey a h = m.getKeyₘ a h
-- Init.Data.SInt.Lemmas
USize.toISize_add : ∀ (a b : USize), (a + b).toISize = a.toISize + b.toISize
-- Std.Time.Internal.UnitVal
/-- Value inside the UnitVal Value.
 -/
Std.Time.Internal.UnitVal.val : {α : ℚ} → Std.Time.Internal.UnitVal α → ℤ
-- Mathlib.Probability.Moments.Covariance
ProbabilityTheory.covariance_fun_sub_right : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X Y Z : Ω → ℝ} {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsFiniteMeasure μ],
  MeasureTheory.MemLp X 2 μ →
    MeasureTheory.MemLp Y 2 μ →
      MeasureTheory.MemLp Z 2 μ →
        ProbabilityTheory.covariance X (fun ω => Y ω - Z ω) μ =
          ProbabilityTheory.covariance X Y μ - ProbabilityTheory.covariance X Z μ
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.parallelPairHom_app_one : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {X' Y' : C} (f g : X ⟶ Y) (f' g' : X' ⟶ Y')
  (p : X ⟶ X') (q : Y ⟶ Y') (wf : CategoryTheory.CategoryStruct.comp f q = CategoryTheory.CategoryStruct.comp p f')
  (wg : CategoryTheory.CategoryStruct.comp g q = CategoryTheory.CategoryStruct.comp p g'),
  (CategoryTheory.Limits.parallelPairHom f g f' g' p q wf wg).app CategoryTheory.Limits.WalkingParallelPair.one = q
-- Mathlib.Topology.MetricSpace.GromovHausdorffRealized
/-- Now that we have proved that the set of candidates is compact, and that `HD` is continuous,
we can finally select a candidate minimizing `HD`. This will be the candidate realizing the
optimal coupling.  -/
_private.Mathlib.Topology.MetricSpace.GromovHausdorffRealized.0.GromovHausdorff.exists_minimizer : ∀ (X : Type u) (Y : Type v) [inst : MetricSpace X] [CompactSpace X] [Nonempty X] [inst_3 : MetricSpace Y]
  [CompactSpace Y] [Nonempty Y],
  ∃ f ∈ GromovHausdorff.candidatesB✝ X Y,
    ∀ g ∈ GromovHausdorff.candidatesB✝ X Y, GromovHausdorff.HD f ≤ GromovHausdorff.HD g
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
/-- Characterizing the forward direction of `rightUnitor` via the universal maps.  -/
CategoryTheory.MonoidalCategory.DayConvolutionUnit.rightUnitor_hom_unit_app_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalCategory V]
  (U : CategoryTheory.Functor C V) [inst_4 : CategoryTheory.MonoidalCategory.DayConvolutionUnit U]
  (F : CategoryTheory.Functor C V)
  [inst_5 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow
          (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) d)
        (CategoryTheory.MonoidalCategory.tensorLeft v)]
  [inst_6 : CategoryTheory.MonoidalCategory.DayConvolution F U] (x : C) {Z : V}
  (h :
    F.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj x (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj x)
        CategoryTheory.MonoidalCategory.DayConvolutionUnit.can)
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.MonoidalCategory.DayConvolution.unit F U).app
          (x, CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
        (CategoryTheory.CategoryStruct.comp
          ((CategoryTheory.MonoidalCategory.DayConvolutionUnit.rightUnitor U F).hom.app
            (CategoryTheory.MonoidalCategoryStruct.tensorObj x (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)))
          h)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor (F.obj x)).hom
      (CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategoryStruct.rightUnitor x).inv) h)
-- Mathlib.Algebra.FreeAlgebra
FreeAlgebra.Pre.mul.inj : ∀ {R : Type u_1} {X : Type u_2} {a a_1 a_2 a_3 : FreeAlgebra.Pre R X}, a.mul a_1 = a_2.mul a_3 → a = a_2 ∧ a_1 = a_3
-- Init.Data.Int.Gcd
Int.lcm_lcm_self_right_left : ∀ (m n : ℤ), m.lcm ↑(m.lcm n) = m.lcm n
-- Mathlib.Topology.EMetricSpace.Defs
Metric.mem_closedEBall' : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {x y : α} {ε : ENNReal}, y ∈ Metric.closedEBall x ε ↔ edist x y ≤ ε
-- Mathlib.Probability.Process.Stopping
MeasureTheory.stoppedValue_sub_eq_sum' : ∀ {Ω : Type u_1} {β : Type u_2} {u : ℕ → Ω → β} {τ π : Ω → ℕ∞} [inst : AddCommGroup β],
  τ ≤ π →
    ∀ {N : ℕ},
      (∀ (ω : Ω), π ω ≤ ↑N) →
        MeasureTheory.stoppedValue u π - MeasureTheory.stoppedValue u τ = fun ω =>
          (∑ i ∈ Finset.range (N + 1), {ω | τ ω ≤ ↑i ∧ ↑i < π ω}.indicator (u (i + 1) - u i)) ω
-- Mathlib.Data.Matrix.Block
Matrix.blockDiag_smul : ∀ {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} {R : Type u_14} [inst : SMul R α] (x : R)
  (M : Matrix (m × o) (n × o) α), (x • M).blockDiag = x • M.blockDiag
-- Mathlib.Algebra.Group.Submonoid.Defs
Submonoid.instUniqueOfSubsingleton.eq_1 : ∀ {M : Type u_1} [inst : MulOneClass M] [inst_1 : Subsingleton M],
  Submonoid.instUniqueOfSubsingleton = { default := ⊥, uniq := ⋯ }
-- Mathlib.Data.Finset.NoncommProd
Multiset.noncommProd.congr_simp : ∀ {α : Type u_3} [inst : Monoid α] (s s_1 : Multiset α) (e_s : s = s_1) (comm : {x | x ∈ s}.Pairwise Commute),
  s.noncommProd comm = s_1.noncommProd ⋯
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.size_insertMany_list_le : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {l : List (α × β)}, (Std.ExtDTreeMap.Const.insertMany t l).size ≤ t.size + l.length
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.X_mul_injective : ∀ {R : Type u_1} [inst : Semiring R], Function.Injective fun x => PowerSeries.X * x
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.vadd_set_sUnion : ∀ {α : Type u_2} {β : Type u_3} [inst : VAdd α β] (a : α) (S : Set (Set β)), a +ᵥ ⋃₀ S = ⋃ s ∈ S, a +ᵥ s
-- Mathlib.Data.Seq.Basic
Stream'.Seq.zip_map_right : ∀ {α : Type u} {β : Type v} {β' : Type v'} (s₁ : Stream'.Seq α) (s₂ : Stream'.Seq β) (f : β → β'),
  s₁.zip (Stream'.Seq.map f s₂) = Stream'.Seq.map (Prod.map id f) (s₁.zip s₂)
-- Mathlib.MeasureTheory.MeasurableSpace.Card
/-- If a sigma-algebra is generated by a set of sets `s`, then the sigma-algebra has cardinality at
most `max #s 2 ^ ℵ₀`.  -/
MeasurableSpace.cardinal_generateMeasurable_le : ∀ {α : Type u} (s : Set (Set α)),
  Cardinal.mk ↑{t | MeasurableSpace.GenerateMeasurable s t} ≤ max (Cardinal.mk ↑s) 2 ^ Cardinal.aleph0
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.integral_comp_add_mul : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b c : ℝ} (f : ℝ → E),
  c ≠ 0 → ∀ (d : ℝ), ∫ (x : ℝ) in a..b, f (d + c * x) = c⁻¹ • ∫ (x : ℝ) in d + c * a..d + c * b, f x
-- Std.Data.ExtTreeMap.Basic
/-- Carries out a monadic action on each mapping in the tree map in ascending order.  -/
Std.ExtTreeMap.forM : {α : Type u} →
  {β : Type v} →
    {cmp : α → α → Ordering} →
      {m : Type w → Type w₂} →
        [inst : Monad m] →
          [LawfulMonad m] → [Std.TransCmp cmp] → (α → β → m PUnit.{w + 1}) → Std.ExtTreeMap α β cmp → m PUnit.{w + 1}
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Map
CategoryTheory.Abelian.Ext.mapExactFunctor_extClass : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {D : Type u'}
  [inst_2 : CategoryTheory.Category.{v', u'} D] [inst_3 : CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D)
  [inst_4 : F.Additive] [inst_5 : CategoryTheory.Limits.PreservesFiniteLimits F]
  [inst_6 : CategoryTheory.Limits.PreservesFiniteColimits F] [inst_7 : CategoryTheory.HasExt C]
  [inst_8 : CategoryTheory.HasExt D] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact),
  CategoryTheory.Abelian.Ext.mapExactFunctor F hS.extClass = ⋯.extClass
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr
Std.Tactic.BVDecide.BVExpr.bitblast.goCache_decl_eq : ∀ {w : ℕ} (aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit) (expr : Std.Tactic.BVDecide.BVExpr w)
  (cache : Std.Tactic.BVDecide.BVExpr.Cache aig) (idx : ℕ) (h1 : idx < aig.decls.size)
  (h2 : idx < (↑(Std.Tactic.BVDecide.BVExpr.bitblast.goCache aig expr cache).result).aig.decls.size),
  (↑(Std.Tactic.BVDecide.BVExpr.bitblast.goCache aig expr cache).result).aig.decls[idx] = aig.decls[idx]
-- Init.Data.Int.DivMod.Lemmas
Int.bmod_one : ∀ (x : ℤ), x.bmod 1 = 0
-- Lean.Meta.Tactic.Grind.EMatch
/-- `useMT` is `true` if we are using the mod-time optimization. It is always set to false for new `EMatchTheorem`s.  -/
Lean.Meta.Grind.EMatch.Context.useMT : Lean.Meta.Grind.EMatch.Context → Bool
-- Mathlib.CategoryTheory.ConcreteCategory.EpiMono
CategoryTheory.ConcreteCategory.surjective_eq_epimorphisms : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type w}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC]
  [(CategoryTheory.forget C).PreservesEpimorphisms],
  CategoryTheory.MorphismProperty.surjective C = CategoryTheory.MorphismProperty.epimorphisms C
-- Mathlib.Data.Finset.Sigma
Finset.notMem_sigmaLift_of_ne_right : ∀ {ι : Type u_1} {α : ι → Type u_2} {β : ι → Type u_3} {γ : ι → Type u_4} [inst : DecidableEq ι]
  (f : ⦃i : ι⦄ → α i → β i → Finset (γ i)) {a : Sigma α} (b : Sigma β) {x : Sigma γ},
  b.fst ≠ x.fst → x ∉ Finset.sigmaLift f a b
-- Mathlib.Order.Interval.Set.Image
Set.image_subtype_val_Icc_Iic : ∀ {α : Type u_1} [inst : Preorder α] {a b : α} (c : ↑(Set.Icc a b)), Subtype.val '' Set.Iic c = Set.Icc a ↑c
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.ConnectedComponent.eq : ∀ {V : Type u} {G : SimpleGraph V} {v w : V}, G.connectedComponentMk v = G.connectedComponentMk w ↔ G.Reachable v w
-- Mathlib.Data.Matrix.Diagonal
Matrix.diagonal_add : ∀ {n : Type u_3} {α : Type v} [inst : DecidableEq n] [inst_1 : AddZeroClass α] (d₁ d₂ : n → α),
  Matrix.diagonal d₁ + Matrix.diagonal d₂ = Matrix.diagonal fun i => d₁ i + d₂ i
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.get!_maxD : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.WF → t.isEmpty = false → ∀ {fallback : α}, t.get! (t.maxD fallback) = t.maxD fallback
-- Mathlib.Analysis.Convex.StdSimplex
stdSimplexHomeomorphUnitInterval_zero : stdSimplexHomeomorphUnitInterval ⟨Pi.single 0 1, ⋯⟩ = 0
-- Mathlib.Data.ENNReal.Real
ENNReal.toReal_inf : ∀ {a b : ENNReal}, a ≠ ⊤ → b ≠ ⊤ → (min a b).toReal = min a.toReal b.toReal
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.inv_Iic : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] (a : α), (Set.Iic a)⁻¹ = Set.Ici a⁻¹
-- Mathlib.Topology.Order.MonotoneConvergence
tendsto_atBot_iInf : ∀ {α : Type u_1} {ι : Type u_3} [inst : Preorder ι] [inst_1 : TopologicalSpace α] [inst_2 : CompleteLattice α]
  [InfConvergenceClass α] {f : ι → α}, Monotone f → Filter.Tendsto f Filter.atBot (nhds (⨅ i, f i))
-- Mathlib.Probability.Martingale.Basic
MeasureTheory.supermartingale_nat : ∀ {Ω : Type u_1} {E : Type u_2} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] {𝒢 : MeasureTheory.Filtration ℕ m0} [CompleteSpace E] [inst_3 : PartialOrder E]
  [IsOrderedAddMonoid E] [ClosedIciTopology E] [IsOrderedModule ℝ E] [MeasureTheory.IsFiniteMeasure μ] {f : ℕ → Ω → E},
  MeasureTheory.StronglyAdapted 𝒢 f →
    (∀ (i : ℕ), MeasureTheory.Integrable (f i) μ) →
      (∀ (i : ℕ), μ[f (i + 1) | ↑𝒢 i] ≤ᵐ[μ] f i) → MeasureTheory.Supermartingale f 𝒢 μ
-- Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic
/-- **Alias** of `MeromorphicOn.intervalIntegrable_posLog_norm`.

---

If `f` is real-meromorphic on a compact interval, then `log ‖f ·‖` is interval integrable on this
interval.
 -/
MeromorphicOn.intervalIntegrable_posLog_norm_meromorphicOn : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E} {a b : ℝ},
  MeromorphicOn f (Set.uIcc a b) → IntervalIntegrable (fun x => ‖f x‖.posLog) MeasureTheory.volume a b
-- Mathlib.MeasureTheory.Integral.IntegrableOn
MeasureTheory.IntegrableOn.integrable : ∀ {α : Type u_1} {ε : Type u_3} {mα : MeasurableSpace α} {f : α → ε} {s : Set α} {μ : MeasureTheory.Measure α}
  [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε],
  MeasureTheory.IntegrableOn f s μ → MeasureTheory.Integrable f (μ.restrict s)
-- Mathlib.Data.Ordmap.Ordset
Ordnode.Valid'.node' : ∀ {α : Type u_1} [inst : Preorder α] {l : Ordnode α} {x : α} {r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α},
  Ordnode.Valid' o₁ l ↑x →
    Ordnode.Valid' (↑x) r o₂ → Ordnode.BalancedSz l.size r.size → Ordnode.Valid' o₁ (l.node' x r) o₂
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
/-- A more convenient version of `le_sup_seminorm_apply`.

The set `Finset.Iic m` is the set of all pairs `(k', n')` with `k' ≤ m.1` and `n' ≤ m.2`.
Note that the constant is far from optimal.  -/
SchwartzMap.one_add_le_sup_seminorm_apply : ∀ {𝕜 : Type u_2} {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedField 𝕜] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : SMulCommClass ℝ 𝕜 F] {m : ℕ × ℕ} {k n : ℕ},
  k ≤ m.1 →
    n ≤ m.2 →
      ∀ (f : SchwartzMap E F) (x : E),
        (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤
          2 ^ m.1 * ((Finset.Iic m).sup fun m => SchwartzMap.seminorm 𝕜 m.1 m.2) f
-- Mathlib.Algebra.Group.Prod
MonoidHom.commute_inl_inr : ∀ {M : Type u_3} {N : Type u_4} [inst : MulOneClass M] [inst_1 : MulOneClass N] (m : M) (n : N),
  Commute ((MonoidHom.inl M N) m) ((MonoidHom.inr M N) n)
-- Mathlib.NumberTheory.Height.Projectivization
/-- Extension for the `positivity` tactic: `Projectivization.logHeight` is always nonnegative.  -/
Mathlib.Meta.Positivity.evalProjLogHeight : Mathlib.Meta.Positivity.PositivityExt
-- Mathlib.Analysis.Analytic.OfScalars
FormalMultilinearSeries.ofScalarsSum_op : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Field 𝕜] [inst_1 : Ring E] [inst_2 : Algebra 𝕜 E] [inst_3 : TopologicalSpace E]
  [inst_4 : IsTopologicalRing E] (c : ℕ → 𝕜) [T2Space E] (x : E),
  FormalMultilinearSeries.ofScalarsSum c (MulOpposite.op x) = MulOpposite.op (FormalMultilinearSeries.ofScalarsSum c x)
-- Mathlib.Order.Hom.BoundedLattice
InfTopHom.id.eq_1 : ∀ (α : Type u_2) [inst : Min α] [inst_1 : Top α], InfTopHom.id α = { toInfHom := InfHom.id α, map_top' := ⋯ }
-- Mathlib.AlgebraicGeometry.Geometrically.Integral
/-- We say that morphism `f : X ⟶ Y` is geometrically integral if for all `Spec K ⟶ Y` with `K`
a field, `X ×[Y] Spec K` is integral.  -/
AlgebraicGeometry.GeometricallyIntegral : {X Y : AlgebraicGeometry.Scheme} → (X ⟶ Y) → Prop
-- Mathlib.Algebra.Order.Ring.WithTop
WithBot.instMulPosReflectLE : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : MulZeroClass α] [inst_2 : Preorder α] [MulPosReflectLE α],
  MulPosReflectLE (WithBot α)
-- Mathlib.Algebra.Category.ModuleCat.Ulift
ModuleCat.instAdditiveUliftFunctor : ∀ (R : Type u) [inst : Ring R], (ModuleCat.uliftFunctor.{u_2, u_1, u} R).Additive
-- Mathlib.Algebra.Ring.Idempotent
IsIdempotentElem.one_sub : ∀ {R : Type u_1} [inst : NonAssocRing R] {a : R}, IsIdempotentElem a → IsIdempotentElem (1 - a)
-- Lean.Meta.Tactic.Subst
/-- If `hFVarId` is an `Eq` (or a `HEq` that can be turned into an `Eq`) with a free variable
on the LHS or RHS, eliminates the variable by substitution.
 -/
Lean.Meta.substEq : Lean.MVarId → Lean.FVarId → optParam Lean.Meta.FVarSubst { } → Lean.MetaM (Lean.Meta.FVarSubst × Lean.MVarId)
-- Mathlib.Order.Interval.Set.Basic
Set.Icc_subset_Icc_right : ∀ {α : Type u_1} [inst : Preorder α] {a₁ a₂ b : α}, a₂ ≤ a₁ → Set.Icc b a₂ ⊆ Set.Icc b a₁
-- Mathlib.Topology.Constructions
/-- If `s` is dense in `X` and `u` is open and dense in `s`, then `u = v ∩ s` for some `v` that is
open and dense in `X`.  -/
exists_open_dense_of_open_dense_subtype : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X},
  Dense s → ∀ {u : Set ↑s}, IsOpen u → Dense u → ∃ v, IsOpen v ∧ Dense v ∧ Subtype.val ⁻¹' v = u
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic
_private.Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic.0.CategoryTheory.WithTerminal.map.match_1.eq_3 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C]
  (motive : (X Y : CategoryTheory.WithTerminal C) → (X ⟶ Y) → Sort u_3)
  (x : CategoryTheory.WithTerminal.star ⟶ CategoryTheory.WithTerminal.star)
  (h_1 :
    (a a_1 : C) →
      (f : CategoryTheory.WithTerminal.of a ⟶ CategoryTheory.WithTerminal.of a_1) →
        motive (CategoryTheory.WithTerminal.of a) (CategoryTheory.WithTerminal.of a_1) f)
  (h_2 :
    (a : C) →
      (x : CategoryTheory.WithTerminal.of a ⟶ CategoryTheory.WithTerminal.star) →
        motive (CategoryTheory.WithTerminal.of a) CategoryTheory.WithTerminal.star x)
  (h_3 :
    (x : CategoryTheory.WithTerminal.star ⟶ CategoryTheory.WithTerminal.star) →
      motive CategoryTheory.WithTerminal.star CategoryTheory.WithTerminal.star x),
  (match CategoryTheory.WithTerminal.star, CategoryTheory.WithTerminal.star, x with
    | CategoryTheory.WithTerminal.of a, CategoryTheory.WithTerminal.of a_1, f => h_1 a a_1 f
    | CategoryTheory.WithTerminal.of a, CategoryTheory.WithTerminal.star, x => h_2 a x
    | CategoryTheory.WithTerminal.star, CategoryTheory.WithTerminal.star, x => h_3 x) =
    h_3 x
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Finite
CategoryTheory.Limits.CreatesFiniteColimits.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F : CategoryTheory.Functor C D} →
          autoParam
              ((J : Type) →
                [inst_2 : CategoryTheory.SmallCategory J] →
                  [CategoryTheory.FinCategory J] → CategoryTheory.CreatesColimitsOfShape J F)
              CategoryTheory.Limits.CreatesFiniteColimits.createsFiniteColimits._autoParam →
            CategoryTheory.Limits.CreatesFiniteColimits F
-- Mathlib.GroupTheory.HNNExtension
/-- The action of `t^u` on `ofGroup g`. The normal form will be
`a * t^u * g'` where `a ∈ toSubgroup A B (-u)`  -/
HNNExtension.NormalWord.unitsSMulGroup : {G : Type u_1} →
  [inst : Group G] →
    {A B : Subgroup G} →
      ↥A ≃* ↥B →
        (d : HNNExtension.NormalWord.TransversalPair G A B) →
          (u : ℤˣ) → G → ↥(HNNExtension.toSubgroup A B (-u)) × ↑(d.set u)
-- Mathlib.Algebra.Group.ULift
ULift.leftCancelMonoid : {α : Type u} → [LeftCancelMonoid α] → LeftCancelMonoid (ULift.{u_1, u} α)
-- Mathlib.Data.Finset.Sum
Finset.val_disjSum : ∀ {α : Type u_1} {β : Type u_2} (s : Finset α) (t : Finset β), (s.disjSum t).val = s.val.disjSum t.val
-- Mathlib.Data.Finset.Piecewise
Finset.piecewise_congr : ∀ {ι : Type u_1} {π : ι → Sort u_2} (s : Finset ι) [inst : (j : ι) → Decidable (j ∈ s)] {f f' g g' : (i : ι) → π i},
  (∀ i ∈ s, f i = f' i) → (∀ i ∉ s, g i = g' i) → s.piecewise f g = s.piecewise f' g'
-- Mathlib.Combinatorics.SimpleGraph.Metric
SimpleGraph.edist_top_of_ne : ∀ {V : Type u_1} {u v : V}, u ≠ v → ⊤.edist u v = 1
-- Mathlib.LinearAlgebra.Alternating.Basic
AlternatingMap.coe_add : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {ι : Type u_7} (f f' : M [⋀^ι]→ₗ[R] N), ↑(f + f') = ↑f + ↑f'
-- Mathlib.GroupTheory.MonoidLocalization.DivPairs
/-- Given a commutative monoid `M`, a localization map `f` to its Grothendieck group `G` and
a submonoid `s` of `G`, `s.divPairs f` is the submonoid of pairs `(a, b)`
such that `f a / f b ∈ s`.  -/
Submonoid.divPairs : {M : Type u_1} →
  {G : Type u_2} →
    [inst : CommMonoid M] → [inst_1 : CommGroup G] → ⊤.LocalizationMap G → Submonoid G → Submonoid (M × M)