mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.NumberTheory.Divisors
Int.divisorsAntidiag_natCast : ∀ (n : ℕ),
  (↑n).divisorsAntidiag =
    (Finset.map (Nat.castEmbedding.prodMap Nat.castEmbedding) n.divisorsAntidiagonal).disjUnion
      (Finset.map
        ((Nat.castEmbedding.trans (Equiv.toEmbedding (Equiv.neg ℤ))).prodMap
          (Nat.castEmbedding.trans (Equiv.toEmbedding (Equiv.neg ℤ))))
        n.divisorsAntidiagonal)
      ⋯
-- Mathlib.RingTheory.Artinian.Module
IsArtinianRing.quotNilradicalEquivPi_symm_apply : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsArtinianRing R] (a : (I : MaximalSpectrum R) → R ⧸ I.asIdeal),
  (IsArtinianRing.quotNilradicalEquivPi R).symm a =
    (Ideal.quotientEquivAlgOfEq R ⋯) ((Ideal.quotientInfRingEquivPiQuotient MaximalSpectrum.asIdeal ⋯).symm a)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.isEmpty_iff_forall_not_mem : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → (m.isEmpty = true ↔ ∀ (a : α), a ∉ m)
-- Mathlib.Data.Sum.Order
OrderIso.sumLexCongr_trans : ∀ {α₁ : Type u_4} {α₂ : Type u_5} {β₁ : Type u_6} {β₂ : Type u_7} {γ₁ : Type u_8} {γ₂ : Type u_9} [inst : LE α₁]
  [inst_1 : LE α₂] [inst_2 : LE β₁] [inst_3 : LE β₂] [inst_4 : LE γ₁] [inst_5 : LE γ₂] (e₁ : α₁ ≃o β₁) (e₂ : α₂ ≃o β₂)
  (f₁ : β₁ ≃o γ₁) (f₂ : β₂ ≃o γ₂),
  (e₁.sumLexCongr e₂).trans (f₁.sumLexCongr f₂) = (e₁.trans f₁).sumLexCongr (e₂.trans f₂)
-- Std.Data.HashSet.Lemmas
Std.HashSet.foldM_eq_foldlM_toList : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} {δ : Type v} {m' : Type v → Type w} [inst : Monad m']
  [LawfulMonad m'] {f : δ → α → m' δ} {init : δ}, Std.HashSet.foldM f init m = List.foldlM f init m.toList
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStruct
SSet.Edge.InvStruct.invStructId_invHomId : ∀ {X : SSet} (x : X.obj (Opposite.op { len := 0 })),
  (SSet.Edge.InvStruct.invStructId x).invHomId = SSet.Edge.CompStruct.idCompId x
-- Mathlib.Data.Tree.Basic
/-- **Alias** of `BinaryTree.right`.  -/
Tree.right : {α : Type u_1} → Tree α → Tree α
-- Init.Data.UInt.Bitwise
Bool.toBitVec_toUInt64 : ∀ {b : Bool}, b.toUInt64.toBitVec = BitVec.setWidth 64 (BitVec.ofBool b)
-- Mathlib.RingTheory.Extension.Cotangent.Basic
Algebra.Extension.subsingleton_h1Cotangent : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : Algebra.Extension R S), Subsingleton P.H1Cotangent ↔ Function.Injective ⇑P.cotangentComplex
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.getD_filter_of_getKey?_eq_some : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {f : α → β → Bool} {k k' : α} {fallback : β},
  t.getKey? k = some k' →
    Std.ExtDTreeMap.Const.getD (Std.ExtDTreeMap.filter f t) k fallback =
      (Option.filter (fun x => f k' x) (Std.ExtDTreeMap.Const.get? t k)).getD fallback
-- Mathlib.GroupTheory.Perm.Support
Equiv.Perm.disjoint_inv_right_iff : ∀ {α : Type u_1} {f g : Equiv.Perm α}, f.Disjoint g⁻¹ ↔ f.Disjoint g
-- Init.Data.Iterators.Combinators.Monadic.FilterMap
Std.Iterators.Types.FilterMap.instIterator : {α β γ : Type w} →
  {m : Type w → Type w'} →
    {n : Type w → Type w''} →
      {lift : ⦃α : Type w⦄ → m α → n α} →
        {f : β → Std.Iterators.PostconditionT n (Option γ)} →
          [Std.Iterator α m β] → [Monad n] → Std.Iterator (Std.Iterators.Types.FilterMap α m n lift f) n γ
-- Init.Data.Array.Count
Array.count_eq_countP : ∀ {α : Type u_1} [inst : BEq α] {a : α} {xs : Array α}, Array.count a xs = Array.countP (fun x => x == a) xs
-- Std.Data.ExtDHashMap.Basic
/-- Internal implementation detail of the hash map.  -/
Std.ExtDHashMap.pliftOn : {α : Type u} →
  {β : α → Type v} →
    {x : BEq α} →
      {x_1 : Hashable α} →
        {γ : Sort w} →
          (m : Std.ExtDHashMap α β) →
            (f : (a : Std.DHashMap α β) → m = Std.ExtDHashMap.mk a → γ) →
              (∀ (a b : Std.DHashMap α β) (h₁ : m = Std.ExtDHashMap.mk a) (h₂ : m = Std.ExtDHashMap.mk b),
                  a.Equiv b → f a h₁ = f b h₂) →
                γ
-- Mathlib.CategoryTheory.Category.Basic
CategoryTheory.dite_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : Prop} [inst_1 : Decidable P] {X Y Z : C} (g : P → (Z ⟶ Y))
  (g' : ¬P → (Z ⟶ Y)) (f : Y ⟶ X),
  CategoryTheory.CategoryStruct.comp (if h : P then g h else g' h) f =
    if h : P then CategoryTheory.CategoryStruct.comp (g h) f else CategoryTheory.CategoryStruct.comp (g' h) f
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Matrix.SpecialLinearGroup.ext_iff : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R]
  (A B : Matrix.SpecialLinearGroup n R), A = B ↔ ∀ (i j : n), ↑A i j = ↑B i j
-- Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
UniformConvergenceCLM.uniformSpace_mono : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {E : Type u_3}
  (F : Type u_4) [inst_2 : AddCommGroup E] [inst_3 : Module 𝕜₁ E] [inst_4 : TopologicalSpace E]
  [inst_5 : AddCommGroup F] [inst_6 : Module 𝕜₂ F] {𝔖₁ 𝔖₂ : Set (Set E)} [inst_7 : UniformSpace F]
  [inst_8 : IsUniformAddGroup F],
  𝔖₂ ⊆ 𝔖₁ → UniformConvergenceCLM.instUniformSpace σ F 𝔖₁ ≤ UniformConvergenceCLM.instUniformSpace σ F 𝔖₂
-- Mathlib.SetTheory.Cardinal.Embedding
Fin.Embedding.restrictSurjective_of_le_natCard : ∀ {α : Type u_1} {m n : ℕ} [Finite α] (hmn : m ≤ n),
  n ≤ Nat.card α → Function.Surjective fun x => (Fin.castLEEmb hmn).trans x
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgHom.coe_prod : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : Star A] [inst_4 : Semiring B] [inst_5 : Algebra R B] [inst_6 : Star B]
  [inst_7 : Semiring C] [inst_8 : Algebra R C] [inst_9 : Star C] (f : A →⋆ₐ[R] B) (g : A →⋆ₐ[R] C),
  ⇑(f.prod g) = Function.prod ⇑f ⇑g
-- Mathlib.GroupTheory.GroupAction.Quotient
/-- Orbit-stabilizer theorem.  -/
MulAction.card_orbit_mul_card_stabilizer_eq_card_group : ∀ (G : Type u) {X : Type v} [inst : Group G] [inst_1 : MulAction G X] (b : X) [inst_2 : Fintype G]
  [inst_3 : Fintype ↑(MulAction.orbit G b)] [inst_4 : Fintype ↥(MulAction.stabilizer G b)],
  Fintype.card ↑(MulAction.orbit G b) * Fintype.card ↥(MulAction.stabilizer G b) = Fintype.card G
-- Mathlib.CategoryTheory.Category.Quiv
/-- Naturality of `Paths.of`, which defines a natural transformation
` 𝟭 _⟶ Cat.free ⋙ Quiv.forget`.  -/
CategoryTheory.Quiv.pathsOf_freeMap_toPrefunctor : ∀ {V : Type u} {W : Type u₁} [inst : Quiver V] [inst_1 : Quiver W] (F : V ⥤q W),
  CategoryTheory.Paths.of V ⋙q (CategoryTheory.Cat.freeMap F).toPrefunctor = F ⋙q CategoryTheory.Paths.of W
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.pullbackProdSndIsoProd_inv_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) (Z : C)
  [inst_1 : CategoryTheory.Limits.HasBinaryProduct Z Y] [inst_2 : CategoryTheory.Limits.HasBinaryProduct Z X]
  [inst_3 : CategoryTheory.Limits.HasPullback CategoryTheory.Limits.prod.snd f],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackProdSndIsoProd f Z).inv
      (CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.prod.snd f) =
    CategoryTheory.Limits.prod.snd
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalLeftAction.leftUnitor_actionHom : ∀ {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} {inst_2 : CategoryTheory.MonoidalCategory C}
  [self : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] (c : C) (d : D),
  CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft
      (CategoryTheory.MonoidalCategoryStruct.leftUnitor c).hom d =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso
          (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) c d).hom
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso
          (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj c d)).hom
-- Mathlib.AlgebraicTopology.SimplicialSet.Simplices
SSet.S.cast_eq_self : ∀ {X : SSet} (s : X.S) {d : ℕ} (hd : s.dim = d), s.cast hd = s
-- Mathlib.Analysis.Convex.Between
Set.InjOn.sbtw_map_iff : ∀ {R : Type u_1} {V : Type u_2} {V' : Type u_3} {P : Type u_4} {P' : Type u_5} [inst : Ring R] [inst_1 : PartialOrder R]
  [inst_2 : AddCommGroup V] [inst_3 : Module R V] [inst_4 : AddTorsor V P] [inst_5 : AddCommGroup V']
  [inst_6 : Module R V'] [inst_7 : AddTorsor V' P'] {x y z : P} {f : P →ᵃ[R] P'} {s : AffineSubspace R P},
  Set.InjOn ⇑f ↑s → x ∈ s → y ∈ s → z ∈ s → (Sbtw R (f x) (f y) (f z) ↔ Sbtw R x y z)
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
deriv_cpow_const : ∀ {f : ℂ → ℂ} {x c : ℂ},
  DifferentiableAt ℂ f x → f x ∈ Complex.slitPlane → deriv (fun x => f x ^ c) x = c * f x ^ (c - 1) * deriv f x
-- Init.Data.BitVec.Lemmas
/-- Given the definition of ediv/emod for signed integer division (https://dl.acm.org/doi/pdf/10.1145/128861.128862)
we have that for two integers `x` and `y`: `x/y = q ↔ x.ediv y = q ↔ r = x.emod y`
and in particular: `-1/y = q ↔ -1.ediv y = q ↔ r = -1.emod y`.
from which it follows that:
(-1)/0 = 0
(-1)/y = -1 when 0 < y
(-1)/(-5) = 1 when y < 0
 -/
BitVec.neg_one_ediv_toInt_eq : ∀ {w : ℕ} {y : BitVec w}, -1 / y.toInt = if y.toInt = 0 then 0 else if 0 < y.toInt then -1 else 1
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
NNReal.spectrum_nonempty : ∀ {A : Type u_2} [inst : Ring A] [inst_1 : StarRing A] [inst_2 : LE A] [inst_3 : TopologicalSpace A]
  [inst_4 : Algebra NNReal A] [ContinuousFunctionalCalculus NNReal A fun x => 0 ≤ x] [Nontrivial A] {a : A},
  0 ≤ a → (spectrum NNReal a).Nonempty
-- Mathlib.Algebra.Order.AddTorsor
instIsCancelSMulOfIsOrderedCancelSMul : ∀ {G : Type u_1} {P : Type u_2} [inst : PartialOrder G] [inst_1 : PartialOrder P] [inst_2 : SMul G P]
  [IsOrderedCancelSMul G P], IsCancelSMul G P
-- Mathlib.LinearAlgebra.QuadraticForm.Prod
QuadraticMap.Isometry.fst_apply : ∀ {R : Type u_2} {M₁ : Type u_3} (M₂ : Type u_4) {P : Type u_7} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid P] [inst_4 : Module R M₁] [inst_5 : Module R M₂]
  [inst_6 : Module R P] (Q₁ : QuadraticMap R M₁ P) (self : M₁ × M₂), (QuadraticMap.Isometry.fst M₂ Q₁) self = self.1
-- Mathlib.Analysis.InnerProductSpace.WeakOperatorTopology
ContinuousLinearMapWOT.instStarRingId : {𝕜 : Type u_1} →
  {F : Type u_3} →
    [inst : RCLike 𝕜] →
      [inst_1 : NormedAddCommGroup F] → [inst_2 : InnerProductSpace 𝕜 F] → [CompleteSpace F] → StarRing (F →WOT[𝕜] F)
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.isLoop_iff_forall_mem_compl_isBase : ∀ {α : Type u_1} {M : Matroid α} {e : α}, M.IsLoop e ↔ ∀ (B : Set α), M.IsBase B → e ∈ M.E \ B
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.map_insertEntry_perm_filter_map : ∀ {α : Type u} {β : Type v} [inst : BEq α] [EquivBEq α] (k : α) (v : β) {l : List ((_ : α) × β)},
  Std.Internal.List.DistinctKeys l →
    (List.map (fun x => (x.fst, x.snd)) (Std.Internal.List.insertEntry k v l)).Perm
      ((k, v) :: List.filter (fun x => !k == x.1) (List.map (fun x => (x.fst, x.snd)) l))
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
/-- The embedding of a monoid into its skew monoid algebra.  -/
SkewMonoidAlgebra.of : (k : Type u_1) →
  (G : Type u_2) →
    [inst : Semiring k] → [inst_1 : Monoid G] → [inst_2 : MulSemiringAction G k] → G →* SkewMonoidAlgebra k G
-- Mathlib.Analysis.Calculus.BumpFunction.InnerProduct
/-- A base bump function in an inner product space. This construction works in any space with a
norm smooth away from zero but we do not have a typeclass for this.  -/
ContDiffBumpBase.ofInnerProductSpace : (E : Type u_1) → [inst : NormedAddCommGroup E] → [inst_1 : InnerProductSpace ℝ E] → ContDiffBumpBase E
-- Mathlib.RingTheory.Algebraic.Integral
instIsAlgebraicPolynomialOfNoZeroDivisors : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [alg : Algebra.IsAlgebraic R S] [NoZeroDivisors R], Algebra.IsAlgebraic (Polynomial R) (Polynomial S)
-- Mathlib.Analysis.CStarAlgebra.Spectrum
StarAlgEquiv.norm_map : ∀ {F : Type u_1} {A : Type u_2} {B : Type u_3} [inst : NonUnitalCStarAlgebra A] [inst_1 : NonUnitalCStarAlgebra B]
  [inst_2 : EquivLike F A B] [NonUnitalAlgEquivClass F ℂ A B] [StarHomClass F A B] (φ : F) (a : A), ‖φ a‖ = ‖a‖
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
/-- Monomial degree of product  -/
MonomialOrder.degree_mul_of_mul_leadingCoeff_ne_zero : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] {f g : MvPolynomial σ R},
  m.leadingCoeff f * m.leadingCoeff g ≠ 0 → m.degree (f * g) = m.degree f + m.degree g
-- Mathlib.Algebra.CharP.Invertible
invOf_eq_of_coprime : ∀ {R : Type u_1} [inst : Ring R] {p : ℕ} [CharP R p] {n : ℕ} [inst_2 : Invertible ↑n], n.Coprime p → ⅟↑n = ↑(n.gcdA p)
-- Mathlib.AlgebraicGeometry.Modules.Tilde
AlgebraicGeometry.tilde.toOpen_map_app_assoc : ∀ {R : CommRingCat} {M N : ModuleCat ↑R} (f : M ⟶ N) (U : TopologicalSpace.Opens (PrimeSpectrum ↑R)) {Z : ModuleCat ↑R}
  (h : (AlgebraicGeometry.modulesSpecToSheaf.obj (AlgebraicGeometry.tilde N)).obj.obj (Opposite.op U) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.tilde.toOpen M U)
      (CategoryTheory.CategoryStruct.comp
        ((AlgebraicGeometry.modulesSpecToSheaf.map (AlgebraicGeometry.tilde.map f)).hom.app (Opposite.op U)) h) =
    CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.tilde.toOpen N U) h)
-- Mathlib.Analysis.Convex.Basic
Convex.exists_mem_add_smul_eq : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] {s : Set E},
  Convex 𝕜 s → ∀ {x y : E} {p q : 𝕜}, x ∈ s → y ∈ s → 0 ≤ p → 0 ≤ q → ∃ z ∈ s, (p + q) • z = p • x + q • y
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.contains_alter_of_not_compare_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k k' : α} {f : Option β → Option β},
      ¬cmp k k' = Ordering.eq → (Std.DTreeMap.Raw.Const.alter t k f).contains k' = t.contains k'
-- Mathlib.Tactic.Linter.Multigoal
/-- The "multiGoal" linter emits a warning when there are multiple active goals.  -/
Mathlib.Linter.linter.style.multiGoal : Lean.Option Bool
-- Mathlib.Analysis.Complex.CanonicalDecomposition
/-- The canonical factor `CanonicalFactor R w` takes values of norm one on `sphere 0 R`.
 -/
Complex.norm_canonicalFactor_eval_circle_eq_one : ∀ {R : ℝ} {w z : ℂ}, w ∈ Metric.ball 0 R → z ∈ Metric.sphere 0 R → ‖Complex.canonicalFactor R w z‖ = 1
-- Mathlib.Algebra.Group.Defs
AddGroup.toSubtractionMonoid : {G : Type u_1} → [AddGroup G] → SubtractionMonoid G
-- Mathlib.LinearAlgebra.Alternating.Basic
AlternatingMap.mk.inj : ∀ {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} {toMultilinearMap : MultilinearMap R (fun x => M) N}
  {map_eq_zero_of_eq' : ∀ (v : ι → M) (i j : ι), v i = v j → i ≠ j → toMultilinearMap.toFun v = 0}
  {toMultilinearMap_1 : MultilinearMap R (fun x => M) N}
  {map_eq_zero_of_eq'_1 : ∀ (v : ι → M) (i j : ι), v i = v j → i ≠ j → toMultilinearMap_1.toFun v = 0},
  { toMultilinearMap := toMultilinearMap, map_eq_zero_of_eq' := map_eq_zero_of_eq' } =
      { toMultilinearMap := toMultilinearMap_1, map_eq_zero_of_eq' := map_eq_zero_of_eq'_1 } →
    toMultilinearMap = toMultilinearMap_1
-- Mathlib.Analysis.Convex.SimplicialComplex.Basic
Geometry.SimplicialComplex.hasBot : (𝕜 : Type u_1) →
  (E : Type u_2) →
    [inst : Ring 𝕜] →
      [inst_1 : PartialOrder 𝕜] →
        [inst_2 : AddCommGroup E] → [inst_3 : Module 𝕜 E] → Bot (Geometry.SimplicialComplex 𝕜 E)
-- Init.Data.String.Lemmas.FindPos
String.Pos.prevn_startPos : ∀ {n : ℕ} {s : String}, s.startPos.prevn n = s.startPos
-- Std.Data.DTreeMap.Internal.Queries
_private.Std.Data.DTreeMap.Internal.Queries.0.Std.DTreeMap.Internal.Impl.contains.match_1.eq_2 : ∀ (motive : Ordering → Sort u_1) (h_1 : Unit → motive Ordering.lt) (h_2 : Unit → motive Ordering.gt)
  (h_3 : Unit → motive Ordering.eq),
  (match Ordering.gt with
    | Ordering.lt => h_1 ()
    | Ordering.gt => h_2 ()
    | Ordering.eq => h_3 ()) =
    h_2 ()
-- Lean.Widget.InteractiveDiagnostic
Lean.Widget.instRpcEncodableMsgEmbed : Lean.Server.RpcEncodable Lean.Widget.MsgEmbed
-- Mathlib.SetTheory.Ordinal.Notation
/-- Asserts that `repr a < ω ^ repr b`. Used in `NONote.recOn`.  -/
NONote.below : NONote → NONote → Prop
-- Mathlib.MeasureTheory.OuterMeasure.Operations
/-- Restrict an `OuterMeasure` to a set.  -/
MeasureTheory.OuterMeasure.restrict : {α : Type u_1} → Set α → MeasureTheory.OuterMeasure α →ₗ[ENNReal] MeasureTheory.OuterMeasure α
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toArray_rio_ne_nil_iff : ∀ {n : ℕ}, (*...n).toArray ≠ #[] ↔ 0 < n
-- Init.Data.String.Lemmas.Iter
_private.Init.Data.String.Lemmas.Iter.0.Std.Iter.intercalateString_eq.match_1_4.eq_1 : ∀ (motive : Option String → String → Sort u_1) (sl : String) (h_1 : (sl : String) → motive none sl)
  (h_2 : (str sl : String) → motive (some str) sl),
  (match none, sl with
    | none, sl => h_1 sl
    | some str, sl => h_2 str sl) =
    h_1 sl
-- Mathlib.RingTheory.RingHom.Locally
/-- **Alias** of `RingHom.locally_stableUnderCompositionWithLocalizationAwayTarget`.

---

If `P` is stable under composition with localization away maps on the right,
then so is `Locally P`.  -/
RingHom.locally_StableUnderCompositionWithLocalizationAwayTarget : ∀ {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop},
  (RingHom.StableUnderCompositionWithLocalizationAwayTarget fun {R S} [CommRing R] [CommRing S] => P) →
    RingHom.StableUnderCompositionWithLocalizationAwayTarget fun {R S} [CommRing R] [CommRing S] =>
      RingHom.Locally fun {R S} [CommRing R] [CommRing S] => P
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.getD_insertMany_list_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  {l : List (α × β)} {k k' : α},
  cmp k k' = Ordering.eq →
    ∀ {v fallback : β},
      List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l →
        (k, v) ∈ l → Std.DTreeMap.Const.getD (Std.DTreeMap.Const.insertMany t l) k' fallback = v
-- Mathlib.Topology.Sets.Compacts
/-- The set of opens neighbourhood of a compact subset  -/
TopologicalSpace.Compacts.openNhds : {α : Type u_1} → [inst : TopologicalSpace α] → TopologicalSpace.Compacts α → Set (TopologicalSpace.Opens α)
-- Mathlib.Algebra.AddConstMap.Equiv
/-- Composition of `AddConstEquiv`s, as an `AddConstEquiv`.  -/
AddConstEquiv.trans : {G : Type u_1} →
  {H : Type u_2} →
    {K : Type u_3} →
      [inst : Add G] →
        [inst_1 : Add H] →
          [inst_2 : Add K] →
            {a : G} → {b : H} → {c : K} → AddConstEquiv G H a b → AddConstEquiv H K b c → AddConstEquiv G K a c
-- Mathlib.Data.Matrix.Reflection
_private.Mathlib.Data.Matrix.Reflection.0.Matrix.Forall.match_1.eq_1 : ∀ {α : Type u_1} (motive : (x x_1 : ℕ) → (Matrix (Fin x) (Fin x_1) α → Prop) → Sort u_2) (x : ℕ)
  (P : Matrix (Fin 0) (Fin x) α → Prop) (h_1 : (x : ℕ) → (P : Matrix (Fin 0) (Fin x) α → Prop) → motive 0 x P)
  (h_2 : (n x : ℕ) → (P : Matrix (Fin (n + 1)) (Fin x) α → Prop) → motive n.succ x P),
  (match 0, x, P with
    | 0, x, P => h_1 x P
    | n.succ, x, P => h_2 n x P) =
    h_1 x P
-- Mathlib.LinearAlgebra.Multilinear.Basic
LinearMap.add_compMultilinearMap : ∀ {R : Type uR} {ι : Type uι} {M₁ : ι → Type v₁} {M₂ : Type v₂} {M₃ : Type v₃} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M₃]
  [inst_4 : (i : ι) → Module R (M₁ i)] [inst_5 : Module R M₂] [inst_6 : Module R M₃] (g₁ g₂ : M₂ →ₗ[R] M₃)
  (f : MultilinearMap R M₁ M₂), (g₁ + g₂).compMultilinearMap f = g₁.compMultilinearMap f + g₂.compMultilinearMap f
-- Mathlib.Topology.Inseparable
SeparationQuotient.comap_mk_nhds_mk : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x : X},
  Filter.comap SeparationQuotient.mk (nhds (SeparationQuotient.mk x)) = nhds x
-- Mathlib.Algebra.Order.Group.Abs
apply_abs_le_mul_of_one_le' : ∀ {G : Type u_1} [inst : AddCommGroup G] [inst_1 : LinearOrder G] [IsOrderedAddMonoid G] {H : Type u_2}
  [inst_3 : MulOneClass H] [inst_4 : LE H] [MulLeftMono H] [MulRightMono H] {f : G → H} {a : G},
  1 ≤ f a → 1 ≤ f (-a) → f |a| ≤ f a * f (-a)
-- Mathlib.Algebra.FiveLemma
/-- One four lemma in terms of additive groups.
For a diagram explaining the variables, see the module docstring.  -/
AddMonoidHom.injective_of_surjective_of_injective_of_injective : ∀ {M₁ : Type u_1} {M₂ : Type u_2} {M₃ : Type u_3} {M₄ : Type u_4} {N₁ : Type u_6} {N₂ : Type u_7} {N₃ : Type u_8}
  {N₄ : Type u_9} [inst : AddGroup M₁] [inst_1 : AddGroup M₂] [inst_2 : AddGroup M₃] [inst_3 : AddGroup M₄]
  [inst_4 : AddGroup N₁] [inst_5 : AddGroup N₂] [inst_6 : AddGroup N₃] [inst_7 : AddGroup N₄] (f₁ : M₁ →+ M₂)
  (f₂ : M₂ →+ M₃) (f₃ : M₃ →+ M₄) (g₁ : N₁ →+ N₂) (g₂ : N₂ →+ N₃) (g₃ : N₃ →+ N₄) (i₁ : M₁ →+ N₁) (i₂ : M₂ →+ N₂)
  (i₃ : M₃ →+ N₃) (i₄ : M₄ →+ N₄),
  g₁.comp i₁ = i₂.comp f₁ →
    g₂.comp i₂ = i₃.comp f₂ →
      g₃.comp i₃ = i₄.comp f₃ →
        Function.Exact ⇑f₁ ⇑f₂ →
          Function.Exact ⇑f₂ ⇑f₃ →
            Function.Exact ⇑g₁ ⇑g₂ →
              Function.Surjective ⇑i₁ → Function.Injective ⇑i₂ → Function.Injective ⇑i₄ → Function.Injective ⇑i₃
-- Mathlib.Algebra.Group.TypeTags.Basic
toAdd_pow : ∀ {α : Type u} [inst : AddMonoid α] (a : Multiplicative α) (n : ℕ),
  Multiplicative.toAdd (a ^ n) = n • Multiplicative.toAdd a
-- Mathlib.Topology.UnitInterval
unitInterval.add_pos : ∀ {t : ↑unitInterval} {x : ℝ}, 0 < x → 0 < x + ↑t
-- Batteries.Data.Array.Scan
Array.extract.hcongr_4 : ∀ (α α' : Type u_1),
  α = α' →
    ∀ (as : Array α) (as' : Array α'),
      as ≍ as' →
        ∀ (start start' : ℕ),
          start = start' → ∀ (stop stop' : ℕ), stop = stop' → as.extract start stop ≍ as'.extract start' stop'
-- Mathlib.GroupTheory.Focal
/-- In the quotient `H / H*`, conjugation by any element of `G` preserves equivalence classes.
If `h ∈ H` and `g⁻¹ * h * g ∈ H`, then `g⁻¹hg ≡ h (mod H*)`.
 -/
Subgroup.focalSubgroupOf.mk'_conj_eq : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G) {h : G} (hh : h ∈ H) (g : G) (hconj : g⁻¹ * h * g ∈ H),
  (QuotientGroup.mk' H.focalSubgroupOf) ⟨g⁻¹ * h * g, hconj⟩ = (QuotientGroup.mk' H.focalSubgroupOf) ⟨h, hh⟩
-- Mathlib.MeasureTheory.Measure.ProbabilityMeasure
/-- The characterization of weak convergence of probability measures by the condition that the
integrals of every continuous bounded nonnegative function converge to the integral of the function
against the limit measure.  -/
MeasureTheory.ProbabilityMeasure.tendsto_iff_forall_lintegral_tendsto : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω] [inst_2 : OpensMeasurableSpace Ω]
  {γ : Type u_2} {F : Filter γ} {μs : γ → MeasureTheory.ProbabilityMeasure Ω} {μ : MeasureTheory.ProbabilityMeasure Ω},
  Filter.Tendsto μs F (nhds μ) ↔
    ∀ (f : BoundedContinuousFunction Ω NNReal),
      Filter.Tendsto (fun i => ∫⁻ (ω : Ω), ↑(f ω) ∂↑(μs i)) F (nhds (∫⁻ (ω : Ω), ↑(f ω) ∂↑μ))
-- Mathlib.Probability.Kernel.Disintegration.CondCDF
MeasureTheory.Measure.IsFiniteMeasure.IicSnd : ∀ {α : Type u_1} {mα : MeasurableSpace α} {ρ : MeasureTheory.Measure (α × ℝ)} [MeasureTheory.IsFiniteMeasure ρ] (r : ℝ),
  MeasureTheory.IsFiniteMeasure (ρ.IicSnd r)
-- Init.Data.UInt.Lemmas
UInt8.add_left_inj : ∀ {a b : UInt8} (c : UInt8), a + c = b + c ↔ a = b
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.mem_of_mem_insert : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k a : α} {v : β k}, a ∈ t.insert k v → cmp k a ≠ Ordering.eq → a ∈ t