mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.GroupAction.Defs
MulAction.subgroup_smul_def : ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] {H : Subgroup G} (a : ↥H) (b : α),
  a • b = ↑a • b
-- Mathlib.Probability.Process.Stopping
MeasureTheory.stoppedProcess_stoppedProcess' : ∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : Nonempty ι] {u : ι → Ω → β} {τ σ : Ω → WithTop ι}
  [inst_1 : LinearOrder ι],
  MeasureTheory.stoppedProcess (MeasureTheory.stoppedProcess u τ) σ =
    MeasureTheory.stoppedProcess u fun ω => min (σ ω) (τ ω)
-- Mathlib.Analysis.Calculus.TangentCone.ProperSpace
/-- In a proper space, the tangent cone at a non-isolated point is nontrivial.  -/
tangentConeAt_nonempty_of_properSpace : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [ProperSpace E] {s : Set E} {x : E},
  AccPt x (Filter.principal s) → (tangentConeAt 𝕜 s x ∩ {0}ᶜ).Nonempty
-- Batteries.Data.BinomialHeap.Basic
Batteries.BinomialHeap.Imp.Heap.length.eq_def : ∀ {α : Type u_1} (x : Batteries.BinomialHeap.Imp.Heap α),
  x.length =
    match x with
    | Batteries.BinomialHeap.Imp.Heap.nil => 0
    | Batteries.BinomialHeap.Imp.Heap.cons rank val node r => r.length + 1
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHomRight_whiskerRight_assoc : ∀ {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.MonoidalRightAction C D] {c' c'' : C} (f : c' ⟶ c'') (c : C) (d : D) {Z : D}
  (h :
    CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj d
        (CategoryTheory.MonoidalCategoryStruct.tensorObj c'' c) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight d
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight f c))
      h =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso d c' c).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft
          (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight d f) c)
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso d c'' c).inv h))
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Limits.Sigma.ι_π_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {β : Type w} [inst_2 : DecidableEq β] (f : β → C) [inst_3 : CategoryTheory.Limits.HasCoproduct f] (b c : β) {Z : C}
  (h : f c ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι f b)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.π f c) h) =
    CategoryTheory.CategoryStruct.comp (if h : b = c then CategoryTheory.eqToHom ⋯ else 0) h
-- Init.Data.UInt.Lemmas
UInt64.mul_one : ∀ (a : UInt64), a * 1 = a
-- Mathlib.Topology.Algebra.Monoid
continuousAdd_induced : ∀ {M : Type u_6} {N : Type u_7} {F : Type u_8} [inst : Add M] [inst_1 : Add N] [inst_2 : FunLike F M N]
  [AddHomClass F M N] [inst_4 : TopologicalSpace N] [ContinuousAdd N] (f : F), ContinuousAdd M
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.Equiv.beq : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α] [inst_4 : BEq β] [ReflBEq β], m₁.WF → m₂.WF → m₁.Equiv m₂ → Std.DHashMap.Raw.Const.beq m₁ m₂ = true
-- Mathlib.CategoryTheory.Sites.Plus
CategoryTheory.GrothendieckTopology.diagram_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w}
  [inst_1 : CategoryTheory.Category.{w', w} D]
  [inst_2 :
    ∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)]
  (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) {S x : (J.Cover X)ᵒᵖ} (f : S ⟶ x),
  (J.diagram P X).map f =
    CategoryTheory.Limits.Multiequalizer.lift ((Opposite.unop x).index P)
      (CategoryTheory.Limits.multiequalizer ((Opposite.unop S).index P))
      (fun I =>
        CategoryTheory.Limits.Multiequalizer.ι ((Opposite.unop S).index P)
          (CategoryTheory.GrothendieckTopology.Cover.Arrow.map I f.unop))
      ⋯
-- Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
HurwitzZeta.jacobiTheta₂''_neg_left : ∀ (z τ : ℂ), HurwitzZeta.jacobiTheta₂'' (-z) τ = -HurwitzZeta.jacobiTheta₂'' z τ
-- Mathlib.Order.ConditionallyCompleteLattice.Finset
iInf_ne_bot : ∀ {α : Type u_5} [inst : CompleteLinearOrder α] {ι : Sort u_6} [Finite ι] [Nontrivial α] {f : ι → α},
  (∀ (x : ι), f x ≠ ⊥) → iInf f ≠ ⊥
-- Std.Sync.Channel
_private.Std.Sync.Channel.0.Std.CloseableChannel.Bounded.Consumer.resolve : {α : Type} → Std.CloseableChannel.Bounded.Consumer✝ α → Bool → BaseIO Unit
-- Mathlib.Algebra.Homology.HomologicalBicomplex
/-- The obvious isomorphism `(K.X x₁).X x₂ ≅ (K.X y₁).X y₂` when `x₁ = y₁` and `x₂ = y₂`.  -/
HomologicalComplex₂.XXIsoOfEq : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {I₁ : Type u_2} →
        {I₂ : Type u_3} →
          (c₁ : ComplexShape I₁) →
            (c₂ : ComplexShape I₂) →
              (K : HomologicalComplex₂ C c₁ c₂) →
                {x₁ y₁ : I₁} → x₁ = y₁ → {x₂ y₂ : I₂} → x₂ = y₂ → ((K.X x₁).X x₂ ≅ (K.X y₁).X y₂)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
WeierstrassCurve.Projective.neg_X : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} (P : Fin 3 → R), W'.neg P 0 = P 0
-- Mathlib.Topology.Algebra.Group.Basic
/-- **Alias** of `isClosed_setOfPred_map_inv`. -/
isClosed_setOf_map_inv : ∀ (G₁ : Type u_2) (G₂ : Type u_3) [inst : TopologicalSpace G₂] [T2Space G₂] [inst_2 : Inv G₁] [inst_3 : Inv G₂]
  [ContinuousInv G₂], IsClosed {f | ∀ (x : G₁), f x⁻¹ = (f x)⁻¹}
-- Mathlib.Probability.Kernel.RadonNikodym
ProbabilityTheory.Kernel.singularPart_of_subset_mutuallySingularSetSlice : ∀ {α : Type u_1} {γ : Type u_2} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ} {κ η : ProbabilityTheory.Kernel α γ}
  [hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ] [inst : ProbabilityTheory.IsFiniteKernel κ]
  [inst_1 : ProbabilityTheory.IsFiniteKernel η] {a : α} {s : Set γ},
  MeasurableSet s → s ⊆ κ.mutuallySingularSetSlice η a → ((κ.singularPart η) a) s = (κ a) s
-- Init.Data.Range.Polymorphic.UInt
USize.instLawfulUpwardEnumerableLT : Std.PRange.LawfulUpwardEnumerableLT USize
-- Mathlib.Order.Filter.AtTopBot.Group
Filter.comap_neg_atTop : ∀ {G : Type u_2} [inst : AddCommGroup G] [inst_1 : PartialOrder G] [IsOrderedAddMonoid G],
  Filter.comap Neg.neg Filter.atTop = Filter.atBot
-- Mathlib.Probability.Moments.Variance
/-- A random variable with variance `0` is almost surely constant.  -/
ProbabilityTheory.ae_eq_integral_of_variance_eq_zero : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ],
  MeasureTheory.MemLp X 2 μ → ProbabilityTheory.variance X μ = 0 → ∀ᵐ (ω : Ω) ∂μ, X ω = ∫ (x : Ω), X x ∂μ
-- Std.Data.ExtTreeMap.Basic
/-- Tries to retrieve the smallest key in the tree map, returning `none` if the map is empty.
 -/
Std.ExtTreeMap.minKey? : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtTreeMap α β cmp → Option α
-- Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective
CategoryTheory.extensiveTopology.isLocallySurjective_iff : ∀ {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] {FD : D → D → Type u_3} {CD : D → Type w}
  [inst_2 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [inst_3 : CategoryTheory.ConcreteCategory D FD]
  [inst_4 : CategoryTheory.FinitaryExtensive C] {F G : CategoryTheory.Sheaf (CategoryTheory.extensiveTopology C) D}
  (f : F ⟶ G) [CategoryTheory.Limits.PreservesFiniteProducts (CategoryTheory.forget D)],
  CategoryTheory.Sheaf.IsLocallySurjective f ↔
    ∀ (X : C), Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (f.hom.app (Opposite.op X)))
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.find?_toList_eq_some_iff_getKey?_eq_some_and_get?_eq_some : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp] {k k' : α}
  {v : β},
  List.find? (fun x => cmp x.1 k == Ordering.eq) (Std.DTreeMap.Const.toList t) = some (k', v) ↔
    t.getKey? k = some k' ∧ Std.DTreeMap.Const.get? t k = some v
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
/-- Given a multicofork, we may obtain a cofork over `∐ I.left ⇉ ∐ I.right`.  -/
CategoryTheory.Limits.Multicofork.toSigmaCofork : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.Limits.MultispanShape} →
      {I : CategoryTheory.Limits.MultispanIndex J C} →
        {c : CategoryTheory.Limits.Cofan I.left} →
          (hc : CategoryTheory.Limits.IsColimit c) →
            {d : CategoryTheory.Limits.Cofan I.right} →
              CategoryTheory.Limits.IsColimit d →
                CategoryTheory.Limits.Multicofork I →
                  CategoryTheory.Limits.Cofork (I.fstSigmaMapOfIsColimit d hc) (I.sndSigmaMapOfIsColimit d hc)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
IsStarProjection.mul_right_and_mul_left_of_nonneg_of_le : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] [StarOrderedRing A] {a e : A},
  IsStarProjection e → 0 ≤ a → a ≤ e → a * e = a ∧ e * a = a
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.forget_obj : ∀ {k : Type u} {G : Type v} [inst : Semiring k] [inst_1 : Monoid G] (A : Rep.{w, u, v} k G),
  (CategoryTheory.forget (Rep.{w, u, v} k G)).obj A = ↑A
-- Mathlib.CategoryTheory.Triangulated.Opposite.Functor
CategoryTheory.Functor.op_commShiftIso_inv_app : ∀ {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.HasShift C ℤ]
  [inst_3 : CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [inst_4 : F.CommShift ℤ] (X : Cᵒᵖ) (n m : ℤ)
  (h : n + m = 0),
  (CategoryTheory.Functor.commShiftIso F.op n).inv.app X =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Pretriangulated.shiftFunctorOpIso D n m h).hom.app (Opposite.op (F.obj (Opposite.unop X))))
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.commShiftIso F m).hom.app (Opposite.unop X)).op
        (F.map ((CategoryTheory.Pretriangulated.shiftFunctorOpIso C n m h).inv.app X).unop).op)
-- Std.Data.Internal.Cut
Std.Internal.IsStrictCut.gt_of_isGE_of_gt : ∀ {α : Type u} {cmp : α → α → Ordering} {cut : α → Ordering} [Std.Internal.IsStrictCut cmp cut] {k k' : α},
  (cut k').isGE = true → cmp k' k = Ordering.gt → cut k = Ordering.gt
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.cokernelIsoOfEq.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  {f g : X ⟶ Y} [inst_2 : CategoryTheory.Limits.HasCokernel f] [inst_3 : CategoryTheory.Limits.HasCokernel g]
  (h : f = g),
  CategoryTheory.Limits.cokernelIsoOfEq h =
    CategoryTheory.Limits.HasColimit.isoOfNatIso
      (⋯.mpr (CategoryTheory.Iso.refl (CategoryTheory.Limits.parallelPair g 0)))
-- Mathlib.Analysis.Normed.Affine.MazurUlam
/-- **Mazur-Ulam Theorem**: if `f` is an isometric bijection between two normed add-torsors over
normed vector spaces over `ℝ`, then `f` is an affine isometry equivalence.  -/
IsometryEquiv.toRealAffineIsometryEquiv : {E : Type u_1} →
  {PE : Type u_2} →
    {F : Type u_3} →
      {PF : Type u_4} →
        [inst : NormedAddCommGroup E] →
          [inst_1 : NormedSpace ℝ E] →
            [inst_2 : MetricSpace PE] →
              [inst_3 : NormedAddTorsor E PE] →
                [inst_4 : NormedAddCommGroup F] →
                  [inst_5 : NormedSpace ℝ F] →
                    [inst_6 : MetricSpace PF] → [inst_7 : NormedAddTorsor F PF] → PE ≃ᵢ PF → PE ≃ᵃⁱ[ℝ] PF
-- Init.Data.List.Control
/-- Applies the monadic predicate `p` on every element in the list in reverse order, from right to left,
and returns those elements for which `p` returns `true`. The elements of the returned list are in
the same order as in the input list.

Example:
```lean example
#eval [1, 2, 5, 2, 7, 7].filterRevM fun x => do
  IO.println s!"Checking {x}"
  return x < 3
```
```output
Checking 7
Checking 7
Checking 2
Checking 5
Checking 2
Checking 1
```
```output
[1, 2, 2]
```
 -/
List.filterRevM : {m : Type → Type v} → [Monad m] → {α : Type} → (α → m Bool) → List α → m (List α)
-- Mathlib.GroupTheory.Index
Subgroup.card_mul_index : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G), Nat.card ↥H * H.index = Nat.card G
-- Mathlib.Topology.EMetricSpace.Basic
lebesgue_number_lemma_of_emetric_nhds : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {s : Set α} {c : α → Set α},
  IsCompact s → (∀ x ∈ s, c x ∈ nhds x) → ∃ δ > 0, ∀ x ∈ s, ∃ y, Metric.eball x δ ⊆ c y
-- Mathlib.Algebra.Module.Submodule.Map
Submodule.comapSubtypeEquivOfLe_apply_coe : ∀ {R : Type u_1} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {p q : Submodule R M} (hpq : p ≤ q) (x : ↥(Submodule.comap q.subtype p)),
  ↑((Submodule.comapSubtypeEquivOfLe hpq) x) = ↑↑x
-- Mathlib.Data.Num.ZNum
Num.sub_to_nat : ∀ (m n : Num), ↑(m - n) = ↑m - ↑n
-- Mathlib.CategoryTheory.Monad.Limits
CategoryTheory.Comonad.ForgetCreatesLimits'.liftedCone_pt : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [inst_1 : CategoryTheory.Category.{v, u} J]
  {T : CategoryTheory.Comonad C} {D : CategoryTheory.Functor J T.Coalgebra}
  (c : CategoryTheory.Limits.Cone (D.comp T.forget)) (t : CategoryTheory.Limits.IsLimit c)
  [inst_2 : CategoryTheory.Limits.PreservesLimit (D.comp T.forget) T.toFunctor]
  [inst_3 : CategoryTheory.Limits.PreservesLimit ((D.comp T.forget).comp T.toFunctor) T.toFunctor],
  (CategoryTheory.Comonad.ForgetCreatesLimits'.liftedCone c t).pt =
    CategoryTheory.Comonad.ForgetCreatesLimits'.conePoint c t
-- Mathlib.RingTheory.Adjoin.FG
Algebra.fg_trans : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Algebra R A] {s t : Set A},
  (Subalgebra.toSubmodule (Algebra.adjoin R s)).FG →
    (Subalgebra.toSubmodule (Algebra.adjoin (↥(Algebra.adjoin R s)) t)).FG →
      (Subalgebra.toSubmodule (Algebra.adjoin R (s ∪ t))).FG
-- Mathlib.Analysis.Complex.Hadamard
Complex.HadamardThreeLines.diffContOnCl_interpStrip : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] (f : ℂ → E),
  DiffContOnCl ℂ (Complex.HadamardThreeLines.interpStrip f) (Complex.HadamardThreeLines.verticalStrip 0 1)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey?_eq_some_getKeyD : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {a fallback : α}, a ∈ m → m.getKey? a = some (m.getKeyD a fallback)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey_insertManyIfNewUnit_list_of_not_mem_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeMap α Unit cmp} [Std.TransCmp cmp] {l : List α} {k k' : α},
  cmp k k' = Ordering.eq →
    ∀ {h' : k' ∈ t.insertManyIfNewUnit l},
      k ∉ t → List.Pairwise (fun a b => ¬cmp a b = Ordering.eq) l → k ∈ l → (t.insertManyIfNewUnit l).getKey k' h' = k
-- Mathlib.Probability.Kernel.RadonNikodym
ProbabilityTheory.Kernel.withDensity_rnDeriv_eq_zero_iff_mutuallySingular : ∀ {α : Type u_1} {γ : Type u_2} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ}
  [hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ] (κ η : ProbabilityTheory.Kernel α γ)
  [ProbabilityTheory.IsFiniteKernel κ] [inst : ProbabilityTheory.IsFiniteKernel η] (a : α),
  (η.withDensity (κ.rnDeriv η)) a = 0 ↔ (κ a).MutuallySingular (η a)
-- Batteries.Recycling.RBTree.Lemmas
_private.Batteries.Recycling.RBTree.Lemmas.0.RBTree.RBNode.balLeft.match_1.eq_3 : ∀ {α : Type u_1} (motive : RBTree.RBNode α → Sort u_2) (r : RBTree.RBNode α)
  (h_1 :
    (a : RBTree.RBNode α) → (y : α) → (b : RBTree.RBNode α) → motive (RBTree.RBNode.node RBTree.RBColor.black a y b))
  (h_2 :
    (a : RBTree.RBNode α) →
      (y : α) →
        (b : RBTree.RBNode α) →
          (z : α) →
            (c : RBTree.RBNode α) →
              motive (RBTree.RBNode.node RBTree.RBColor.red (RBTree.RBNode.node RBTree.RBColor.black a y b) z c))
  (h_3 : (r : RBTree.RBNode α) → motive r),
  (∀ (a : RBTree.RBNode α) (y : α) (b : RBTree.RBNode α), r = RBTree.RBNode.node RBTree.RBColor.black a y b → False) →
    (∀ (a : RBTree.RBNode α) (y : α) (b : RBTree.RBNode α) (z : α) (c : RBTree.RBNode α),
        r = RBTree.RBNode.node RBTree.RBColor.red (RBTree.RBNode.node RBTree.RBColor.black a y b) z c → False) →
      (match r with
        | RBTree.RBNode.node RBTree.RBColor.black a y b => h_1 a y b
        | RBTree.RBNode.node RBTree.RBColor.red (RBTree.RBNode.node RBTree.RBColor.black a y b) z c => h_2 a y b z c
        | r => h_3 r) =
        h_3 r
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.map_root : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) (p : Polynomial R)
  (q : Polynomial S) (h : q ∣ Polynomial.map f p), (AdjoinRoot.map f p q h) (AdjoinRoot.root p) = AdjoinRoot.root q
-- Init.Data.Vector.Basic
Vector.shrink.eq_1 : ∀ {α : Type u_1} {n : ℕ} (xs : Vector α n) (i : ℕ), xs.shrink i = Vector.mk (xs.toArray.shrink i) ⋯
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.op_X₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C), sq.op.X₁ = Opposite.op sq.X₄
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
UniqueMDiffWithinAt.prod : ∀ {𝕜 : 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'] {x : M} {y : M'} {s : Set M}
  {t : Set M'}, UniqueMDiffAt[s] x → UniqueMDiffAt[t] y → UniqueMDiffAt[s ×ˢ t] (x, y)
-- Mathlib.Order.Comparable
IncompRel.not_le : ∀ {α : Type u_1} {a b : α} [inst : LE α], IncompRel (fun x1 x2 => x1 ≤ x2) a b → ¬a ≤ b
-- Mathlib.Algebra.Module.GradedModule
/-- A graded version of `DistribMulAction`.  -/
DirectSum.GdistribMulAction : {ιA : Type u_1} →
  {ιB : Type u_2} →
    (A : ιA → Type u_3) →
      (M : ιB → Type u_4) →
        [inst : AddMonoid ιA] →
          [VAdd ιA ιB] →
            [GradedMonoid.GMonoid A] → [(i : ιB) → AddMonoid (M i)] → Type (max (max (max u_1 u_2) u_3) u_4)
-- Mathlib.Data.Ordmap.Ordset
Ordnode.Valid'.balanceL : ∀ {α : Type u_1} [inst : Preorder α] {l : Ordnode α} {x : α} {r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α},
  Ordnode.Valid' o₁ l ↑x →
    Ordnode.Valid' (↑x) r o₂ →
      ((∃ l', Ordnode.Raised l' l.size ∧ Ordnode.BalancedSz l' r.size) ∨
          ∃ r', Ordnode.Raised r.size r' ∧ Ordnode.BalancedSz l.size r') →
        Ordnode.Valid' o₁ (l.balanceL x r) o₂
-- Mathlib.Data.Finset.Sups
Finset.infs_subset_left : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SemilatticeInf α] {s t₁ t₂ : Finset α}, t₁ ⊆ t₂ → s ⊼ t₁ ⊆ s ⊼ t₂
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarSubalgebra.instSMulMemClass : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  [inst_3 : Star A], SMulMemClass (NonUnitalStarSubalgebra R A) R A
-- Init.Data.BitVec.Lemmas
_private.Init.Data.BitVec.Lemmas.0.BitVec.flattenList.toNatAux.match_1.eq_1 : ∀ {n : ℕ} (motive : List (BitVec n) → Sort u_1) (h_1 : Unit → motive []) (h_2 : (x : BitVec n) → motive [x])
  (h_3 : (x y : BitVec n) → (rest : List (BitVec n)) → motive (x :: y :: rest)),
  (match [] with
    | [] => h_1 ()
    | [x] => h_2 x
    | x :: y :: rest => h_3 x y rest) =
    h_1 ()
-- Mathlib.Order.Filter.Partial
/-- One way of taking the inverse map of a filter under a relation. Generalization of `Filter.comap`
to relations.  -/
Filter.rcomap' : {α : Type u} → {β : Type v} → SetRel α β → Filter β → Filter α
-- Init.Data.List.Lex
List.lt_of_le_of_lt : ∀ {α : Type u_1} [inst : LT α] [inst_1 : LE α] [Std.IsLinearOrder α] [Std.LawfulOrderLT α] {l₁ l₂ l₃ : List α},
  l₁ ≤ l₂ → l₂ < l₃ → l₁ < l₃
-- Mathlib.ModelTheory.Equivalence
/-- Semantic equivalence forms an equivalence relation on formulas.  -/
FirstOrder.Language.Theory.iffSetoid : {L : FirstOrder.Language} → {α : Type w} → {n : ℕ} → L.Theory → Setoid (L.BoundedFormula α n)
-- Mathlib.Algebra.Order.Ring.Synonym
ofLex_intCast : ∀ {R : Type u_1} [inst : IntCast R] (n : ℤ), ofLex ↑n = ↑n
-- Mathlib.CategoryTheory.Limits.MorphismProperty
CategoryTheory.MorphismProperty.Under.instPreservesFiniteColimitsTopUnderForget : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] (P : CategoryTheory.MorphismProperty T) (X : T)
  [CategoryTheory.Limits.HasPushouts T] [P.IsStableUnderComposition] [P.ContainsIdentities]
  [P.IsStableUnderCobaseChange] [P.HasOfPrecompProperty P],
  CategoryTheory.Limits.PreservesFiniteColimits (CategoryTheory.MorphismProperty.Under.forget P ⊤ X)
-- Mathlib.Order.Filter.Pointwise
Filter.covariant_div : ∀ {α : Type u_2} [inst : Div α], CovariantClass (Filter α) (Filter α) (fun x1 x2 => x1 / x2) fun x1 x2 => x1 ≤ x2
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKeyD_union_of_not_mem_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k fallback : α}, k ∉ t₁ → (t₁ ∪ t₂).getKeyD k fallback = t₂.getKeyD k fallback
-- Init.Data.List.Sort.Impl
_private.Init.Data.List.Sort.Impl.0.List.MergeSort.Internal.splitRevAt.go.match_1.splitter : {α : Type u_1} →
  (motive : List α → ℕ → List α → Sort u_2) →
    (x : List α) →
      (x_1 : ℕ) →
        (x_2 : List α) →
          ((x : α) → (xs : List α) → (n : ℕ) → (acc : List α) → motive (x :: xs) n.succ acc) →
            ((xs : List α) →
                (x : ℕ) →
                  (acc : List α) →
                    (∀ (x_3 : α) (xs_1 : List α) (n : ℕ), xs = x_3 :: xs_1 → x = n.succ → False) → motive xs x acc) →
              motive x x_1 x_2
-- Mathlib.Topology.Compactness.Compact
Filter.coclosedCompact.eq_1 : ∀ (X : Type u_1) [inst : TopologicalSpace X],
  Filter.coclosedCompact X = ⨅ s, ⨅ (_ : IsClosed s), ⨅ (_ : IsCompact s), Filter.principal sᶜ
-- Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
/-- Copy of `limit.hom_ext`, specialized to `piOpens` for use by the `ext` tactic.  -/
TopCat.Presheaf.SheafConditionEqualizerProducts.piOpens.hom_ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasProducts C] {X : TopCat}
  (F : TopCat.Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) {X_1 : C}
  {f f' : X_1 ⟶ TopCat.Presheaf.SheafConditionEqualizerProducts.piOpens F U},
  (∀ (j : CategoryTheory.Discrete ι),
      CategoryTheory.CategoryStruct.comp f
          (CategoryTheory.Limits.limit.π (CategoryTheory.Discrete.functor fun i => F.obj (Opposite.op (U i))) j) =
        CategoryTheory.CategoryStruct.comp f'
          (CategoryTheory.Limits.limit.π (CategoryTheory.Discrete.functor fun i => F.obj (Opposite.op (U i))) j)) →
    f = f'
-- Init.System.IO
/-- The file can be read.  -/
IO.AccessRight.read : IO.AccessRight → Bool
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate
SSet.PInfty_toNormalizedChainComplex : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasCoproducts C]
  [inst_2 : CategoryTheory.Preadditive C] (X : SSet) (R : C),
  CategoryTheory.CategoryStruct.comp AlgebraicTopology.DoldKan.PInfty (X.toNormalizedChainComplex R) =
    X.toNormalizedChainComplex R
-- Std.Time.DateTime.Timestamp
Std.Time.Timestamp.instHSubOffset_2 : HSub Std.Time.Timestamp Std.Time.Hour.Offset Std.Time.Timestamp