mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.Modules.Tilde
AlgebraicGeometry.tilde.toOpen.eq_1 : ∀ {R : CommRingCat} (M : ModuleCat ↑R) (U : (AlgebraicGeometry.Spec R).Opens),
  AlgebraicGeometry.tilde.toOpen M U =
    CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (AlgebraicGeometry.StructureSheaf.toOpenₗ (↑R) (↑M) U))
      ((AlgebraicGeometry.tilde.modulesSpecToSheafIso M).app (Opposite.op U)).inv
-- Init.Data.Int.Linear
Int.Internal.Linear.Expr.mulR.sizeOf_spec : ∀ (a : Int.Internal.Linear.Expr) (k : ℤ), sizeOf (a.mulR k) = 1 + sizeOf a + sizeOf k
-- Mathlib.Topology.Compactness.CompactlyGeneratedSpace
/-- If the topology of `X` is coinduced by a continuous function whose domain is
compactly generated, then so is `X`.  -/
uCompactlyGeneratedSpace_of_coinduced : ∀ {X : Type w} {Y : Type x} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] [UCompactlyGeneratedSpace X]
  {f : X → Y}, Continuous f → tY = TopologicalSpace.coinduced f tX → UCompactlyGeneratedSpace Y
-- Mathlib.AlgebraicGeometry.Sites.ConstantSheaf
AlgebraicGeometry.isSheaf_zariskiTopology_continuousMapPresheaf : ∀ (T : Type v) [inst : TopologicalSpace T],
  CategoryTheory.Presheaf.IsSheaf AlgebraicGeometry.Scheme.zariskiTopology (AlgebraicGeometry.continuousMapPresheaf T)
-- Mathlib.RingTheory.Idempotents
/-- A family `{ eᵢ }` of idempotent elements is complete orthogonal if
1. (orthogonal) `eᵢ * eⱼ = 0` for all `i ≠ j`.
2. (complete) `∑ eᵢ = 1`
 -/
CompleteOrthogonalIdempotents : {R : Type u_1} → [Semiring R] → {I : Type u_3} → [Fintype I] → (I → R) → Prop
-- Lean.Parser.Term.Basic
Lean.Parser.Tactic.tacticSeqBracketed.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Algebra.Algebra.Tower
AlgEquiv.symm_restrictScalars : ∀ (R : Type u) {S : Type v} {A : Type w} {B : Type u₁} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : Semiring A] [inst_3 : Semiring B] [inst_4 : Algebra R S] [inst_5 : Algebra S A] [inst_6 : Algebra S B]
  [inst_7 : Algebra R A] [inst_8 : Algebra R B] [inst_9 : IsScalarTower R S A] [inst_10 : IsScalarTower R S B]
  (f : A ≃ₐ[S] B), (AlgEquiv.restrictScalars R f).symm = AlgEquiv.restrictScalars R f.symm
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.CostructuredArrow.homMk.congr_simp : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{u_3, u_1} C]
  [inst_1 : CategoryTheory.Category.{u_4, u_2} D] {P : CategoryTheory.MorphismProperty D}
  {Q : CategoryTheory.MorphismProperty C} [inst_2 : Q.IsMultiplicative] {F : CategoryTheory.Functor C D} {X : D}
  {A B : P.CostructuredArrow Q F X} (f f_1 : A.left ⟶ B.left) (e_f : f = f_1) (hf : Q f)
  (w : CategoryTheory.CategoryStruct.comp (F.map f) B.hom = A.hom),
  CategoryTheory.MorphismProperty.CostructuredArrow.homMk f hf w =
    CategoryTheory.MorphismProperty.CostructuredArrow.homMk f_1 ⋯ ⋯
-- Mathlib.SetTheory.Cardinal.Defs
Cardinal.eq : ∀ {α β : Type u}, Cardinal.mk α = Cardinal.mk β ↔ Nonempty (α ≃ β)
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf
_private.Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.0.AlgebraicGeometry.termAt_ : Lean.ParserDescr
-- Lean.DocString.Parser
Lean.Doc.Parser.instOrdOrderedListType : Ord Lean.Doc.Parser.OrderedListType
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.lift_range_le : ∀ {ι : Type u_1} (G : ι → Type u_4) [inst : (i : ι) → Group (G i)] {N : Type u_5} [inst_1 : Group N]
  (f : (i : ι) → G i →* N) {s : Subgroup N}, (∀ (i : ι), (f i).range ≤ s) → (Monoid.CoprodI.lift f).range ≤ s
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
SemiNormedGrp₁.hom_ext_iff : ∀ {M N : SemiNormedGrp₁} {f g : M ⟶ N}, f = g ↔ SemiNormedGrp₁.Hom.hom f = SemiNormedGrp₁.Hom.hom g
-- Mathlib.Combinatorics.SimpleGraph.Finsubgraph
SimpleGraph.Finsubgraph.instHNot : {V : Type u} → {G : SimpleGraph V} → [Finite V] → HNot G.Finsubgraph
-- Init.Data.Ord.Basic
/-- Checks whether the ordering is `lt`.
 -/
Ordering.isLT : Ordering → Bool
-- Mathlib.Algebra.Group.Subsemigroup.Operations
Subsemigroup.map_comap_le : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] {S : Subsemigroup N} {f : M →ₙ* N},
  Subsemigroup.map f (Subsemigroup.comap f S) ≤ S
-- Init.Data.Int.Gcd
Int.lcm_comm : ∀ (a b : ℤ), a.lcm b = b.lcm a
-- Std.Do.PredTrans
Std.Do.PredTrans.apply_pushOption : ∀ {ps : Std.Do.PostShape} {α : Type u} {Q : Std.Do.PostCond α (Std.Do.PostShape.except PUnit.{u + 1} ps)}
  (x : Std.Do.PredTrans ps (Option α)),
  (Std.Do.PredTrans.pushOption x).apply Q =
    x.apply
      (fun x =>
        match x with
        | some a => Q.1 a
        | none => Q.2.1 PUnit.unit,
        Q.2.2)
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basic
/-- `Multiseries`-part of `MultiseriesExpansion.const`.  -/
Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.const : (basis_hd : ℝ → ℝ) →
  (basis_tl : Tactic.ComputeAsymptotics.Basis) →
    ℝ → Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableEquiv.measurable_comp_iff : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  [inst_2 : MeasurableSpace γ] {f : β → γ} (e : α ≃ᵐ β), Measurable (f ∘ ⇑e) ↔ Measurable f
-- Mathlib.Topology.UniformSpace.Basic
Uniform.continuousAt_iff'_right : ∀ {α : Type ua} {β : Type ub} [inst : UniformSpace α] [inst_1 : TopologicalSpace β] {f : β → α} {b : β},
  ContinuousAt f b ↔ Filter.Tendsto (fun x => (f b, f x)) (nhds b) (uniformity α)
-- Mathlib.CategoryTheory.Grothendieck
CategoryTheory.Grothendieck.toTransport_base : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat}
  (x : CategoryTheory.Grothendieck F) {c : C} (t : x.base ⟶ c), (x.toTransport t).base = t
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.CodeDecl.inc : {pu : Lean.Compiler.LCNF.Purity} →
  Lean.FVarId →
    ℕ →
      Bool →
        Bool →
          autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.CodeDecl._auto_11 →
            Lean.Compiler.LCNF.CodeDecl pu
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.instMonad.eq_1 : FreeGroup.instMonad =
  { map := fun {_α _β} {f} => ⇑(FreeGroup.map f), pure := fun {_α} => FreeGroup.of,
    seq := fun {α β} f x {_α _β} {x} {f} => (FreeGroup.lift f) x,
    seqLeft := fun {α β} x y {_α _β} {x} {f} => (FreeGroup.lift f) x,
    seqRight := fun {α β} x y {_α _β} {x} {f} => (FreeGroup.lift f) x,
    bind := fun {_α _β} {x} {f} => (FreeGroup.lift f) x }
-- Mathlib.Data.FunLike.IsApply
IsInvApply.mk : ∀ {F : Type u_1} {α : outParam (Type u_2)} {β : outParam (Type u_3)} [inst : FunLike F α β] [inst_1 : Inv β]
  [inst_2 : Inv F], (∀ (f : F) (x : α), f⁻¹ x = (f x)⁻¹) → IsInvApply F α β
-- Mathlib.Data.List.Find
/-- If two predicates agree on all the elements, so does `find?`.  -/
List.find?_congr : ∀ {α : Type u_1} {p₁ p₂ : α → Bool} {l : List α}, (∀ x ∈ l, p₁ x = p₂ x) → List.find? p₁ l = List.find? p₂ l
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey_insert_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [inst : Std.TransCmp cmp]
  (h : t.WF) {k : α} {v : β k}, (t.insert k v).getKey k ⋯ = k
-- Mathlib.Algebra.Group.Pi.Lemmas
/-- The injection into a pi group with the same values commutes.  -/
Pi.mulSingle_apply_commute : ∀ {I : Type u} {f : I → Type v} [inst : DecidableEq I] [inst_1 : (i : I) → MulOneClass (f i)] (x : (i : I) → f i)
  (i j : I), Commute (Pi.mulSingle i (x i)) (Pi.mulSingle j (x j))
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.monadLift_Id : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} [inst : Monad m] [inst_1 : Std.Do.WPMonad m ps] {α : Type u} (x : Id α)
  (Q : Std.Do.PostCond α ps), ⦃Q.1 x.run⦄ monadLift x ⦃Q⦄
-- Mathlib.RingTheory.Coprime.Basic
IsCoprime.abs_left : ∀ {R : Type u} [inst : CommRing R] [inst_1 : LinearOrder R] [AddLeftMono R] {x y : R}, IsCoprime x y → IsCoprime |x| y
-- Batteries.Data.List.Basic
List.swapTR.go.eq_2 : ∀ {α : Type u_1} (l : List α) (a : Array α) (head : α) (tail : List α), List.swapTR.go l (head :: tail) 0 0 a = l
-- Mathlib.Algebra.Group.Hom.Defs
Monoid.End.instMul.eq_1 : ∀ (M : Type u_4) [inst : MulOne M], Monoid.End.instMul M = { mul := MonoidHom.comp }
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.smul_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] {K : Type u_5} [inst_1 : SMul K β] (k : K)
  (f : MeasureTheory.SimpleFunc α β) (a : α), (k • f) a = k • f a
-- Mathlib.CategoryTheory.MorphismProperty.Composition
CategoryTheory.MorphismProperty.ContainsIdentities.op : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) [W.ContainsIdentities],
  W.op.ContainsIdentities
-- Mathlib.Tactic.NormNum.Pow
Mathlib.Meta.NormNum.isNNRat_pow : ∀ {α : Type u_1} [inst : Semiring α] {f : α → ℕ → α} {a : α} {an cn ad b b' cd : ℕ},
  f = HPow.hPow →
    Mathlib.Meta.NormNum.IsNNRat a an ad →
      Mathlib.Meta.NormNum.IsNat b b' → an.pow b' = cn → ad.pow b' = cd → Mathlib.Meta.NormNum.IsNNRat (f a b) cn cd
-- Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
SSet.PtSimplex.RelStruct.mk : {X : SSet} →
  {n : ℕ} →
    {x : X.obj (Opposite.op { len := 0 })} →
      {f g : X.PtSimplex n x} →
        {i : Fin (n + 1)} →
          (map : SSet.stdSimplex.obj { len := n + 1 } ⟶ X) →
            autoParam (CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ i.castSucc) map = f.map)
                SSet.PtSimplex.RelStruct.δ_castSucc_map._autoParam →
              autoParam (CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ i.succ) map = g.map)
                  SSet.PtSimplex.RelStruct.δ_succ_map._autoParam →
                autoParam
                    (∀ j < i.castSucc, CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ j) map = SSet.const x)
                    SSet.PtSimplex.RelStruct.δ_map_of_lt._autoParam →
                  autoParam
                      (∀ (j : Fin (n + 2)),
                        i.succ < j → CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ j) map = SSet.const x)
                      SSet.PtSimplex.RelStruct.δ_map_of_gt._autoParam →
                    f.RelStruct g i
-- Mathlib.Data.Nat.Choose.Factorization
/-- The factorization of `p` in `(p * (n + 1))!` is one more than the sum of the factorizations of
`p` in `(p * n)!` and `n + 1`.  -/
Nat.factorization_factorial_mul_succ : ∀ {n p : ℕ},
  Nat.Prime p →
    (p * (n + 1)).factorial.factorization p = (p * n).factorial.factorization p + (n + 1).factorization p + 1
-- Mathlib.Topology.CompactOpen
/-- **Alias** of `ContinuousMap.isClosed_setOfPred_mapsTo`. -/
ContinuousMap.isClosed_setOf_mapsTo : ∀ {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {t : Set Y},
  IsClosed t → ∀ (s : Set X), IsClosed {f | Set.MapsTo (⇑f) s t}
-- Mathlib.Topology.Constructible
IsRetrocompact.empty : ∀ {X : Type u_2} [inst : TopologicalSpace X], IsRetrocompact ∅
-- Lean.Meta.Tactic.Grind.Arith.Simproc
Lean.Meta.Grind.Arith.normIntMulInst : Lean.Meta.Simp.DSimproc
-- Mathlib.Data.Nat.Bits
Nat.bit_bodd_div2 : ∀ (n : ℕ), Nat.bit n.bodd n.div2 = n
-- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
MeasureTheory.lintegral_inter_add_sdiff : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {B : Set α} (f : α → ENNReal) (A : Set α),
  MeasurableSet B → ∫⁻ (x : α) in A ∩ B, f x ∂μ + ∫⁻ (x : α) in A \ B, f x ∂μ = ∫⁻ (x : α) in A, f x ∂μ
-- Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
/-- The functor that carries a 2-truncated simplicial set to its underlying refl quiver.  -/
SSet.oneTruncation₂ : CategoryTheory.Functor (SSet.Truncated 2) CategoryTheory.ReflQuiv
-- Mathlib.CategoryTheory.Monoidal.Closed.Types
CategoryTheory.instMonoidalClosedType : CategoryTheory.MonoidalClosed (Type v₁)
-- Mathlib.Order.UpperLower.Basic
/-- **Alias** of the reverse direction of `isLowerSet_preimage_ofDual_iff`. -/
IsUpperSet.toDual : ∀ {α : Type u_1} [inst : LE α] {s : Set α}, IsUpperSet s → IsLowerSet (⇑OrderDual.ofDual ⁻¹' s)
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.snd_inv : ∀ {R : Type u} {M : Type v} [inst : Neg M] [inst_1 : Inv R] [inst_2 : SMul Rᵐᵒᵖ M] [inst_3 : SMul R M]
  (x : TrivSqZeroExt R M), x⁻¹.snd = -(MulOpposite.op x.fst⁻¹ • x.fst⁻¹ • x.snd)
-- Mathlib.Analysis.Normed.Field.Lemmas
NormedField.continuousAt_zpow : ∀ {𝕜 : Type u_4} [inst : NontriviallyNormedField 𝕜] {n : ℤ} {x : 𝕜}, ContinuousAt (fun x => x ^ n) x ↔ x ≠ 0 ∨ 0 ≤ n
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenAddSubgroup.coe_inf : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] {U V : OpenAddSubgroup G}, ↑(U ⊓ V) = ↑U ∩ ↑V
-- Mathlib.MeasureTheory.Group.FoelnerFilter
IsFoelner.mean_smul_eq_mean_smul : ∀ {G : Type u_1} {X : Type u_2} [inst : MeasurableSpace X] {μ : MeasureTheory.Measure X} [inst_1 : Group G]
  [inst_2 : MulAction G X] {ι : Type u_3} {u : Ultrafilter ι} {F : ι → Set X}
  [MeasureTheory.SMulInvariantMeasure G X μ],
  IsFoelner G μ (↑u) F → ∀ (g h : G) (s : Set X), IsFoelner.mean μ u F (g • s) = IsFoelner.mean μ u F (h • s)
-- Mathlib.MeasureTheory.Integral.SetToL1
/-- If `F i → f` in `L1`, then `setToFun μ T hT (F i) → setToFun μ T hT f`.  -/
MeasureTheory.tendsto_setToFun_of_L1 : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {T : Set α → E →L[ℝ] F} {C : ℝ} (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) {ι : Type u_7} (f : α → E),
  MeasureTheory.AEStronglyMeasurable f μ →
    ∀ {fs : ι → α → E} {l : Filter ι},
      (∀ᶠ (i : ι) in l, MeasureTheory.Integrable (fs i) μ) →
        Filter.Tendsto (fun i => ∫⁻ (x : α), ‖fs i x - f x‖ₑ ∂μ) l (nhds 0) →
          Filter.Tendsto (fun i => MeasureTheory.setToFun μ T hT (fs i)) l (nhds (MeasureTheory.setToFun μ T hT f))
-- Mathlib.Order.RelClasses
/-- **Alias** of `LE.le.eq_of_not_ssubset'`.

---

Set notation form of `LE.le.eq_of_not_lt'` -/
LE.le.eq_of_not_ssuperset : ∀ {α : Type u_2} [UsesSetNotationForOrder α] [inst : PartialOrder α] {a b : α}, b ⊆ a → ¬b ⊂ a → a = b
-- Mathlib.CategoryTheory.ObjectProperty.Orthogonal
CategoryTheory.ObjectProperty.rightOrthogonal_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (P : CategoryTheory.ObjectProperty C) (Y : C), P.rightOrthogonal Y ↔ ∀ ⦃X : C⦄ (f : X ⟶ Y), P X → f = 0
-- Mathlib.Data.Matrix.Reflection
/-- This can be used to prove
```lean
example (A : Matrix (Fin 2) (Fin 2) α) :
  A = !![A 0 0, A 0 1;
         A 1 0, A 1 1] :=
(etaExpand_eq _).symm
```
 -/
Matrix.etaExpand_eq : ∀ {α : Type u_1} {m n : ℕ} (A : Matrix (Fin m) (Fin n) α), A.etaExpand = A
-- Mathlib.Order.UpperLower.Prod
/-- The product of two upper sets as an upper set.  -/
UpperSet.prod : {α : Type u_1} →
  {β : Type u_2} → [inst : Preorder α] → [inst_1 : Preorder β] → UpperSet α → UpperSet β → UpperSet (α × β)
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
Std.IterM.any_eq_anyM : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Std.Iterator α m β] [Std.Iterators.Finite α m] [inst_2 : Monad m]
  [LawfulMonad m] [inst_4 : Std.IteratorLoop α m m] [Std.LawfulIteratorLoop α m m] {it : Std.IterM m β} {p : β → Bool},
  Std.IterM.any p it = Std.IterM.anyM (fun x => pure { down := p x }) it
-- Lean.Meta.Basic
/-- The type of the parameter.  -/
Lean.Meta.ExprParamInfo.type : Lean.Meta.ExprParamInfo → Lean.Expr
-- Init.GrindInstances.Ring.UInt
Lean.Grind.instCommRingUSize : Lean.Grind.CommRing USize
-- Mathlib.Data.List.Cycle
Cycle.length_subsingleton_iff : ∀ {α : Type u_1} {s : Cycle α}, s.Subsingleton ↔ s.length ≤ 1
-- Std.Sat.AIG.Basic
_private.Std.Sat.AIG.Basic.0.Std.Sat.AIG.Fanin.invert_eq_testBit : ∀ (f : Std.Sat.AIG.Fanin), f.invert = f.val.testBit 0
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
CategoryTheory.Limits.FormalCoproduct.isPullback : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : CategoryTheory.Limits.FormalCoproduct C} (f : X ⟶ Z)
  (g : Y ⟶ Z)
  (pb :
    (i : Function.Pullback f.f g.f) →
      CategoryTheory.Limits.PullbackCone (CategoryTheory.CategoryStruct.comp (f.φ (↑i).1) (CategoryTheory.eqToHom ⋯))
        (g.φ (↑i).2))
  (hpb : (i : Function.Pullback f.f g.f) → CategoryTheory.Limits.IsLimit (pb i)),
  CategoryTheory.IsPullback (CategoryTheory.Limits.FormalCoproduct.pullbackCone f g pb).fst
    (CategoryTheory.Limits.FormalCoproduct.pullbackCone f g pb).snd f g
-- Mathlib.Topology.Order.DenselyOrdered
right_nhdsWithin_Ico_neBot : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [DenselyOrdered α] {a b : α},
  a < b → (nhdsWithin b (Set.Ico a b)).NeBot
-- Mathlib.Topology.Maps.Basic
Topology.IsOpenEmbedding.of_isEmpty : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [IsEmpty X] (f : X → Y),
  Topology.IsOpenEmbedding f
-- Mathlib.Algebra.Star.Subsemiring
/-- The `carrier` of a `StarSubsemiring` is closed under the `star` operation.  -/
StarSubsemiring.star_mem' : ∀ {R : Type v} [inst : NonAssocSemiring R] [inst_1 : Star R] (self : StarSubsemiring R) {a : R},
  a ∈ self.carrier → star a ∈ self.carrier
-- Init.Data.Array.Lex.Lemmas
Array.le_of_lt : ∀ {α : Type u_1} [inst : LT α] [i : Std.Asymm fun x1 x2 => x1 < x2] {xs ys : Array α}, xs < ys → xs ≤ ys
-- Mathlib.Combinatorics.SimpleGraph.Finsubgraph
SimpleGraph.Finsubgraph.coe_bot : ∀ {V : Type u} {G : SimpleGraph V}, ↑⊥ = ⊥
-- Mathlib.Analysis.Normed.Module.Convex
/-- The segment from `x` to `y` is contained in the closed ball centered at `y` with radius
`dist x y`.  -/
segment_subset_closedBall_right : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (x y : E),
  segment ℝ x y ⊆ Metric.closedBall y (dist x y)
-- Lean.Compiler.IR.Basic
Lean.IR.instInhabitedJoinPointId.default : Lean.IR.JoinPointId
-- Mathlib.RingTheory.Ideal.Quotient.Defs
/-- Quotienting by equal ideals gives equivalent rings.

See also `Submodule.quotEquivOfEq` and `Ideal.quotientEquivAlgOfEq`.
 -/
Ideal.quotEquivOfEq : {R : Type u} →
  [inst : Ring R] → {I J : Ideal R} → [inst_1 : I.IsTwoSided] → [inst_2 : J.IsTwoSided] → I = J → R ⧸ I ≃+* R ⧸ J
-- Mathlib.Data.Analysis.Filter
/-- `Unit` is a realizer for the top filter  -/
Filter.Realizer.top : {α : Type u_1} → ⊤.Realizer
-- Mathlib.ModelTheory.Order
FirstOrder.Language.preorderTheory.eq_1 : ∀ (L : FirstOrder.Language) [inst : L.IsOrdered],
  L.preorderTheory = {FirstOrder.Language.leSymb.reflexive, FirstOrder.Language.leSymb.transitive}
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.isLongestRevMatchAt_endPos_iff : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice} {startPos : s.Pos},
  String.Slice.Pattern.Model.IsLongestRevMatchAt pat startPos s.endPos ↔
    String.Slice.Pattern.Model.IsLongestRevMatch pat startPos
-- Mathlib.LinearAlgebra.Dimension.Constructions
/-- If `m` and `n` are finite, the rank of `m × n` matrices over a module `M` is
`(#m).lift * (#n).lift * rank R M`.  -/
rank_matrix_module : ∀ (R : Type u) (M : Type v) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [StrongRankCondition R]
  [Module.Free R M] (m : Type w) (n : Type w') [Finite m] [Finite n],
  Module.rank R (Matrix m n M) =
    Cardinal.lift.{max v w', w} (Cardinal.mk m) * Cardinal.lift.{max v w, w'} (Cardinal.mk n) *
      Cardinal.lift.{max w w', v} (Module.rank R M)
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
NumberField.InfinitePlace.le_iff_le : ∀ {K : Type u_1} [inst : Field K] (x : K) (r : ℝ),
  (∀ (w : NumberField.InfinitePlace K), w x ≤ r) ↔ ∀ (φ : K →+* ℂ), ‖φ x‖ ≤ r
-- Std.Data.DHashMap.Basic
/-- Creates a hash map from a list of mappings. If the same key appears multiple times, the last
occurrence takes precedence.  -/
Std.DHashMap.Const.ofList : {α : Type u} → {β : Type v} → [inst : BEq α] → [inst_1 : Hashable α] → List (α × β) → Std.DHashMap α fun x => β
-- Init.Data.Nat.Lemmas
Nat.mul_add_mod : ∀ (m x y : ℕ), (m * x + y) % m = y % m
-- Init.Grind.Ring.Envelope
_private.Init.Grind.Ring.Envelope.0.Lean.Grind.Ring.OfSemiring.rel_rfl : ∀ {α : Type u} [inst : Lean.Grind.Semiring α] (h : Equivalence (Lean.Grind.Ring.OfSemiring.r α))
  (q : Lean.Grind.Ring.OfSemiring.Q α), Lean.Grind.Ring.OfSemiring.rel✝ h q q
-- Init.Data.Int.DivMod.Lemmas
Int.fmod.eq_4 : ∀ (m n : ℕ), (Int.negSucc m).fmod (Int.ofNat n) = Int.subNatNat n (m % n).succ
-- Mathlib.Algebra.Category.Ring.Limits
/-- The flat sections of a functor into `RingCat` form a subring of all sections.
 -/
RingCat.sectionsSubring : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] → (F : CategoryTheory.Functor J RingCat) → Subring ((j : J) → ↑(F.obj j))
-- Lean.PrettyPrinter.Delaborator.Options
Lean.getPPTagAppFns : Lean.Options → Bool
-- Mathlib.RingTheory.Ideal.IsPrimary
/-- A proper ideal `I` is primary as a submodule.  -/
Ideal.IsPrimary : {R : Type u_1} → [inst : CommSemiring R] → Ideal R → Prop
-- Mathlib.CategoryTheory.LocallyCartesianClosed.Over
CategoryTheory.equivToOverUnit_counitIso : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C],
  (CategoryTheory.equivToOverUnit C).counitIso =
    CategoryTheory.NatIso.ofComponents
      (fun X =>
        CategoryTheory.Iso.refl
          (((CategoryTheory.toOverUnit C).comp
                (CategoryTheory.Over.forget (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))).obj
            X))
      ⋯
-- Mathlib.FieldTheory.LinearDisjoint
IntermediateField.LinearDisjoint.basisOfBasisRight_apply : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {A B : IntermediateField F E}
  (H : A.LinearDisjoint ↥B) (H' : A.toSubalgebra ⊔ B.toSubalgebra = ⊤) {ι : Type u_1} (b : Module.Basis ι F ↥B) (i : ι),
  (H.basisOfBasisRight H' b) i = (algebraMap (↥B) E) (b i)
-- Mathlib.CategoryTheory.Monad.Kleisli
CategoryTheory.Cokleisli.Hom.mk.injEq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {U : CategoryTheory.Comonad C}
  {c c' : CategoryTheory.Cokleisli U} (of of_1 : U.obj c.of ⟶ c'.of), ({ of := of } = { of := of_1 }) = (of = of_1)
-- Std.Data.ExtTreeMap.Basic
/-- Returns the key-value pair with the `n`-th smallest key.  -/
Std.ExtTreeMap.entryAtIdx : {α : Type u} →
  {β : Type v} →
    {cmp : α → α → Ordering} → [Std.TransCmp cmp] → (t : Std.ExtTreeMap α β cmp) → (n : ℕ) → n < t.size → α × β
-- Mathlib.Order.Interval.Set.Fin
Fin.image_natAdd_Ioo : ∀ {n : ℕ} (m : ℕ) (i j : Fin n), Fin.natAdd m '' Set.Ioo i j = Set.Ioo (Fin.natAdd m i) (Fin.natAdd m j)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Complex.iteratedDeriv_even_sinh : ∀ (n : ℕ), iteratedDeriv (2 * n) Complex.sinh = Complex.sinh
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.prod_mono_right : ∀ {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] (s : Subsemiring R),
  Monotone fun t => s.prod t
-- Mathlib.CategoryTheory.Comma.Over.StrictInitial
CategoryTheory.MorphismProperty.underEquivOfIsTerminal_unitIso : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P Q : CategoryTheory.MorphismProperty C)
  [inst_1 : P.ContainsIdentities] [inst_2 : Q.IsMultiplicative] [inst_3 : Q.RespectsIso]
  [inst_4 : CategoryTheory.Limits.HasStrictTerminalObjects C] (X : C) (h : CategoryTheory.Limits.IsTerminal X),
  (CategoryTheory.MorphismProperty.underEquivOfIsTerminal.{w, v_1, u_1} P Q X h).unitIso =
    CategoryTheory.NatIso.ofComponents
      (fun A => CategoryTheory.MorphismProperty.Under.isoMk (CategoryTheory.asIso A.hom).symm ⋯) ⋯
-- Lean.Expr
Lean.Expr.updateFn : Lean.Expr → Lean.Expr → Lean.Expr
-- Mathlib.Algebra.Group.TransferInstance
/-- Transfer `AddCommSemigroup` across an `Equiv`  -/
Equiv.addCommSemigroup : {α : Type u_2} → {β : Type u_3} → α ≃ β → [AddCommSemigroup β] → AddCommSemigroup α
-- Mathlib.NumberTheory.Harmonic.ZetaAsymp
ZetaAsymptotics.termTSum.eq_1 : ∀ (s : ℝ), ZetaAsymptotics.termTSum s = ∑' (n : ℕ), ZetaAsymptotics.term (n + 1) s
-- Mathlib.Order.BoundedOrder.Basic
Pi.instBotForall.eq_1 : ∀ {ι : Type u_1} {α' : ι → Type u_2} [inst : (i : ι) → Bot (α' i)], Pi.instBotForall = { bot := fun x => ⊥ }