mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
/-- **Alias** of `Submodule.ker_orthogonalProjectionOnto`. -/
Submodule.ker_orthogonalProjection : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {K : Submodule 𝕜 E} [inst_3 : K.HasOrthogonalProjection], (↑K.orthogonalProjectionOnto).ker = Kᗮ
-- Mathlib.Order.Preorder.Chain
IsMaxChain.bot_mem : ∀ {α : Type u_1} {s : Set α} [inst : LE α] [inst_1 : OrderBot α], IsMaxChain (fun x1 x2 => x1 ≤ x2) s → ⊥ ∈ s
-- Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt
ArithmeticFunction.vonMangoldt_apply_pow : ∀ {n k : ℕ}, k ≠ 0 → ArithmeticFunction.vonMangoldt (n ^ k) = ArithmeticFunction.vonMangoldt n
-- Mathlib.Algebra.Module.ZLattice.Covolume
ZLattice.covolume.tendsto_card_div_pow : ∀ {ι : Type u_1} [inst : Fintype ι] (L : Submodule ℤ (ι → ℝ)) [inst_1 : DiscreteTopology ↥L] [IsZLattice ℝ L]
  (b : Module.Basis ι ℤ ↥L) {s : Set (ι → ℝ)},
  Bornology.IsBounded s →
    MeasurableSet s →
      MeasureTheory.volume (frontier s) = 0 →
        Filter.Tendsto (fun n => ↑(Nat.card ↑(s ∩ (↑n)⁻¹ • ↑L)) / ↑n ^ Fintype.card ι) Filter.atTop
          (nhds (MeasureTheory.volume.real s / ZLattice.covolume L MeasureTheory.volume))
-- Mathlib.NumberTheory.Primorial
primorial_mono : ∀ {m n : ℕ}, m ≤ n → primorial m ≤ primorial n
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getD_filter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {f : α → β → Bool} {k : α} {fallback : β},
  (Std.ExtTreeMap.filter f t).getD k fallback = (t[k]?.pfilter fun x h' => f (t.getKey k ⋯) x).getD fallback
-- Mathlib.RingTheory.KrullDimension.Basic
nilradical_le_jacobson : ∀ (R : Type u_3) [inst : CommRing R], nilradical R ≤ Ring.jacobson R
-- Mathlib.Order.Interval.Set.Basic
Set.Ici_inter_Ico_of_le : ∀ {α : Type u_1} [inst : Preorder α] {a b c : α}, c ≤ a → Set.Ici a ∩ Set.Ico c b = Set.Ico a b
-- Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
Complex.Gammaℝ_add_two : ∀ {s : ℂ}, s ≠ 0 → (s + 2).Gammaℝ = s.Gammaℝ * s / 2 / ↑Real.pi
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
EisensteinSeries.eisensteinSeries_slash_apply : ∀ {N : ℕ} (a : Fin 2 → ZMod N) (k : ℤ) (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ),
  SlashAction.map k γ (eisensteinSeries a k) =
    eisensteinSeries (Matrix.vecMul a ↑((Matrix.SpecialLinearGroup.map (Int.castRingHom (ZMod N))) γ)) k
-- Mathlib.RingTheory.Ideal.Quotient.Nilpotent
/-- Let `P` be a property on ideals. If `P` holds for square-zero ideals, and if
`P I → P (J ⧸ I) → P J`, then `P` holds for all nilpotent ideals.  -/
Ideal.IsNilpotent.induction_on : ∀ {S : Type u_1} [inst : CommRing S] (I : Ideal S),
  IsNilpotent I →
    ∀ {P : ⦃S : Type u_1⦄ → [inst : CommRing S] → Ideal S → Prop},
      (∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I : Ideal S), I ^ 2 = ⊥ → P I) →
        (∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I J : Ideal S),
            I ≤ J → P I → P (Ideal.map (Ideal.Quotient.mk I) J) → P J) →
          P I
-- Init.Data.Order.MinMaxOn
minOn_eq_right : ∀ {β : Type u_1} {α : Sort u_2} [inst : LE β] [inst_1 : DecidableLE β] {f : α → β} {x y : α},
  ¬f x ≤ f y → minOn f x y = y
-- Mathlib.Algebra.QuaternionBasis
QuaternionAlgebra.Basis.lift_mul : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] {c₁ c₂ c₃ : R}
  (q : QuaternionAlgebra.Basis A c₁ c₂ c₃) (x y : QuaternionAlgebra R c₁ c₂ c₃), q.lift (x * y) = q.lift x * q.lift y
-- Mathlib.Data.ENNReal.Basic
ENNReal.instMax : Max ENNReal
-- Mathlib.Util.Superscript
/-- Shorthand for `subscript(term)`.

This is needed because the initializer below does not always run, and if it has not run then
downstream parsers using the combinators will crash.

See https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Non-builtin.20parser.20aliases/near/365125476
for some context.  -/
Mathlib.Tactic.subscriptTerm : Lean.Parser.Parser
-- Aesop.Tree.Data
Aesop.Goal.isUnsafeExhausted : Aesop.Goal → Bool
-- Mathlib.CategoryTheory.Limits.Indization.Category
/-- A way to understand morphisms in `Ind C`: every morphism is induced by a natural transformation
of diagrams.  -/
CategoryTheory.Ind.exists_nonempty_arrow_mk_iso_ind_lim : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A B : CategoryTheory.Ind C} {f : A ⟶ B},
  ∃ I x,
    ∃ (x_1 : CategoryTheory.IsFiltered I),
      ∃ F G φ, Nonempty (CategoryTheory.Arrow.mk f ≅ CategoryTheory.Arrow.mk ((CategoryTheory.Ind.lim I).map φ))
-- Mathlib.RingTheory.Polynomial.ScaleRoots
Polynomial.scaleRoots_aeval_eq_zero : ∀ {R : Type u_1} {A : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] {p : Polynomial R}
  {a : A} {r : R}, (Polynomial.aeval a) p = 0 → (Polynomial.aeval ((algebraMap R A) r * a)) (p.scaleRoots r) = 0
-- Init.GrindInstances.ToInt
Lean.Grind.instModUInt16UintOfNatNat : Lean.Grind.ToInt.Mod UInt16 (Lean.Grind.IntInterval.uint 16)
-- Mathlib.Topology.Algebra.Group.Basic
continuousNeg_sInf : ∀ {G : Type w} [inst : Neg G] {ts : Set (TopologicalSpace G)}, (∀ t ∈ ts, ContinuousNeg G) → ContinuousNeg G
-- Mathlib.Data.Set.SMulAntidiagonal
Set.VAddAntidiagonal.eq_of_fst_le_fst_of_snd_le_snd : ∀ {G : Type u_1} {P : Type u_2} {s : Set G} {t : Set P} {a : P} [inst : PartialOrder G] [inst_1 : PartialOrder P]
  [inst_2 : VAdd G P] [IsOrderedCancelVAdd G P] {x y : ↑(s.vaddAntidiagonal t a)},
  (↑x).1 ≤ (↑y).1 → (↑x).2 ≤ (↑y).2 → x = y
-- Std.Data.DTreeMap.Raw.Lemmas
_private.Std.Data.DTreeMap.Raw.Lemmas.0.Break.runK.match_1.eq_2 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (h_1 : (a : α) → motive (some a)) (h_2 : Unit → motive none),
  (match none with
    | some a => h_1 a
    | none => h_2 ()) =
    h_2 ()
-- Mathlib.Analysis.Convex.Segment
/-- Open segment in a vector space. Note that `openSegment 𝕜 x x = {x}` instead of being `∅` when
the base semiring has some element between `0` and `1`.  -/
openSegment : (𝕜 : Type u_1) → {E : Type u_2} → [Semiring 𝕜] → [PartialOrder 𝕜] → [AddCommMonoid E] → [SMul 𝕜 E] → E → E → Set E
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
MeasureTheory.SignedMeasure.toJordanDecompositionEquiv_symm_apply : ∀ (α : Type u_2) [inst : MeasurableSpace α] (j : MeasureTheory.JordanDecomposition α),
  (MeasureTheory.SignedMeasure.toJordanDecompositionEquiv α).symm j = j.toSignedMeasure
-- Batteries.Data.String.Lemmas
String.toList_takeWhile : ∀ (p : Char → Bool) (s : String), (String.Legacy.takeWhile s p).toList = List.takeWhile p s.toList
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
/-- Given an equivalence `e : A ≃ₐ[R] B` of `R`-algebras and a subalgebra `S` of `A`,
`subalgebraMap` is the induced equivalence between `S` and `S.map e`  -/
AlgEquiv.subalgebraMap : {R : Type u} →
  {A : Type v} →
    {B : Type w} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Semiring B] →
            [inst_3 : Algebra R A] →
              [inst_4 : Algebra R B] → (e : A ≃ₐ[R] B) → (S : Subalgebra R A) → ↥S ≃ₐ[R] ↥(Subalgebra.map (↑e) S)
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
SimpleGraph.Colorable.of_isEmpty : ∀ {V : Type u} {G : SimpleGraph V} [IsEmpty V] (n : ℕ), G.Colorable n
-- Init.Data.String.Basic
String.Slice.Pos.ofSliceFrom_sliceFrom : ∀ {s : String.Slice} {p₀ p : s.Pos} {h : p₀ ≤ p}, String.Slice.Pos.ofSliceFrom (p₀.sliceFrom p h) = p
-- Mathlib.Data.Nat.Prime.Basic
Nat.coprime_primes : ∀ {p q : ℕ}, Nat.Prime p → Nat.Prime q → (p.Coprime q ↔ p ≠ q)
-- Mathlib.Algebra.Homology.HomotopyCategory
/-- If two complexes become isomorphic in the homotopy category,
then they were homotopy equivalent.  -/
HomotopyCategory.homotopyEquivOfIso : {ι : Type u_2} →
  {V : Type u} →
    [inst : CategoryTheory.Category.{v, u} V] →
      [inst_1 : CategoryTheory.Preadditive V] →
        {c : ComplexShape ι} →
          {C D : HomologicalComplex V c} →
            ((HomotopyCategory.quotient V c).obj C ≅ (HomotopyCategory.quotient V c).obj D) → HomotopyEquiv C D
-- Mathlib.Algebra.Homology.Embedding.TruncGEHomology
/-- Auxiliary definition for `truncGE'.homologyData`.  -/
HomologicalComplex.truncGE'.isLimitKernelFork : {ι : Type u_1} →
  {ι' : Type u_2} →
    {c : ComplexShape ι} →
      {c' : ComplexShape ι'} →
        {C : Type u_3} →
          [inst : CategoryTheory.Category.{v_1, u_3} C] →
            [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
              (K : HomologicalComplex C c') →
                (e : c.Embedding c') →
                  [inst_2 : e.IsTruncGE] →
                    [inst_3 : ∀ (i' : ι'), K.HasHomology i'] →
                      (j k : ι) →
                        c.next j = k →
                          {j' : ι'} →
                            (hj' : e.f j = j') →
                              (hj : e.BoundaryGE j) →
                                CategoryTheory.Limits.IsLimit
                                  (CategoryTheory.Limits.KernelFork.ofι
                                    (CategoryTheory.CategoryStruct.comp (K.homologyι j')
                                      (K.truncGE'XIsoOpcycles e hj' hj).inv)
                                    ⋯)
-- Init.Data.List.ToArray
Array.forIn'.loop.eq_def : ∀ {α : Type u} {β : Type v} {m : Type v → Type w} [inst : Monad m] (as : Array α)
  (f : (a : α) → a ∈ as → β → m (ForInStep β)) (i : ℕ) (h : i ≤ as.size) (b : β),
  Array.forIn'.loop as f i h b =
    match i, h with
    | 0, x => pure b
    | i.succ, h =>
      have h' := ⋯;
      have this := ⋯;
      have this := ⋯;
      do
      let __do_lift ← f as[as.size - 1 - i] ⋯ b
      match __do_lift with
        | ForInStep.done b => pure b
        | ForInStep.yield b => Array.forIn'.loop as f i ⋯ b
-- Mathlib.Topology.Order
discreteTopology_iff_nhds_ne : ∀ {α : Type u_1} [inst : TopologicalSpace α], DiscreteTopology α ↔ ∀ (x : α), nhdsWithin x {x}ᶜ = ⊥
-- Init.Data.Iterators.Lemmas.Combinators.ULift
_private.Init.Data.Iterators.Lemmas.Combinators.ULift.0.Std.IterM.step_uLift.match_1.splitter : {α : Type u_1} →
  {m : Type u_1 → Type u_2} →
    {β : Type u_1} →
      [inst : Std.Iterator α m β] →
        {it : Std.IterM m β} →
          (motive : it.Step → Sort u_3) →
            (x : it.Step) →
              ((it' : Std.IterM m β) →
                  (out : β) →
                    (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩) →
                ((it' : Std.IterM m β) →
                    (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩) →
                  ((h : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩) → motive x
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.pi_div_two_le_two : Real.pi / 2 ≤ 2
-- Init.Grind.Lemmas
Lean.Grind.Bool.eq_true_of_and_eq_true_left : ∀ {a b : Bool}, (a && b) = true → a = true
-- Mathlib.Data.Matrix.Mul
dotProduct_zero : ∀ {m : Type u_2} {α : Type v} [inst : Fintype m] [inst_1 : NonUnitalNonAssocSemiring α] (v : m → α), v ⬝ᵥ 0 = 0
-- Mathlib.Algebra.Ring.Subring.MulOpposite
Subring.op_le_op_iff : ∀ {R : Type u_2} [inst : NonAssocRing R] {S₁ S₂ : Subring R}, S₁.op ≤ S₂.op ↔ S₁ ≤ S₂
-- Init.Data.BitVec.Lemmas
BitVec.getLsbD_extractLsb' : ∀ {n : ℕ} (start len : ℕ) (x : BitVec n) (i : ℕ),
  (BitVec.extractLsb' start len x).getLsbD i = (decide (i < len) && x.getLsbD (start + i))
-- Mathlib.Lean.Meta.RefinedDiscrTree.Lookup
/-- Create a new trie with the given lazy entry.  -/
_private.Mathlib.Lean.Meta.RefinedDiscrTree.Lookup.0.Lean.Meta.RefinedDiscrTree.newTrie : {α : Type} →
  Lean.Meta.RefinedDiscrTree.LazyEntry × α → Lean.Meta.RefinedDiscrTree.TreeM✝ α Lean.Meta.RefinedDiscrTree.TrieIndex
-- Init.ShareCommon
ShareCommon.StateFactoryBuilder.mk : (Map : (α : Type) → Type → [BEq α] → [Hashable α] → Type) →
  ({α β : Type} → [inst : BEq α] → [inst_1 : Hashable α] → ℕ → Map α β) →
    ({α β : Type} → [inst : BEq α] → [inst_1 : Hashable α] → Map α β → α → Option β) →
      ({α β : Type} → [inst : BEq α] → [inst_1 : Hashable α] → Map α β → α → β → Map α β) →
        (Set : (α : Type) → [BEq α] → [Hashable α] → Type) →
          ({α : Type} → [inst : BEq α] → [inst_1 : Hashable α] → ℕ → Set α) →
            ({α : Type} → [inst : BEq α] → [inst_1 : Hashable α] → Set α → α → Option α) →
              ({α : Type} → [inst : BEq α] → [inst_1 : Hashable α] → Set α → α → Set α) →
                ShareCommon.StateFactoryBuilder
-- Lean.Widget.Diff
_private.Lean.Widget.Diff.0.Lean.Widget.exprDiffCore.piDiff : Lean.SubExpr → Lean.SubExpr → Lean.MetaM Lean.Widget.ExprDiff✝
-- Mathlib.Geometry.RingedSpace.SheafedSpace
AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace_full : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C], AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace.Full
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
/-- If `f : ℝ≥0 → ℝ≥0` is continuous on a compact set `s` and `a : X → A` tends to `a₀ : A` along a
filter `l` (such that eventually `0 ≤ a x` and has spectrum contained in `s`, as does `a₀`), then
`fun x ↦ cfc f (a x)` tends to `cfc f a₀`.  -/
Filter.Tendsto.cfc_nnreal : ∀ {X : Type u_1} {A : Type u_2} [inst : NormedRing A] [inst_1 : StarRing A] [inst_2 : NormedAlgebra ℝ A]
  [inst_3 : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [ContinuousStar A] [inst_5 : PartialOrder A]
  [inst_6 : StarOrderedRing A] [inst_7 : NonnegSpectrumClass ℝ A] [T2Space A] [IsSemitopologicalRing A]
  {s : Set NNReal},
  IsCompact s →
    ∀ (f : NNReal → NNReal) {a : X → A} {a₀ : A} {l : Filter X},
      Filter.Tendsto a l (nhds a₀) →
        (∀ᶠ (x : X) in l, spectrum NNReal (a x) ⊆ s) →
          (∀ᶠ (x : X) in l, 0 ≤ a x) →
            spectrum NNReal a₀ ⊆ s →
              0 ≤ a₀ →
                autoParam (ContinuousOn f s) Filter.Tendsto.cfc_nnreal._auto_1 →
                  Filter.Tendsto (fun x => cfc f (a x)) l (nhds (cfc f a₀))
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- Given two forks with isomorphic components in such a way that the natural diagrams commute, then if
one is a limit, then the other one is as well.
 -/
CategoryTheory.Limits.Fork.isLimitOfIsos : {C : Type u} →
  {X Y : C} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {f g : X ⟶ Y} →
        {X' Y' : C} →
          (c : CategoryTheory.Limits.Fork f g) →
            CategoryTheory.Limits.IsLimit c →
              {f' g' : X' ⟶ Y'} →
                (c' : CategoryTheory.Limits.Fork f' g') →
                  (e₀ : X ≅ X') →
                    (e₁ : Y ≅ Y') →
                      (e : c.pt ≅ c'.pt) →
                        autoParam
                            (CategoryTheory.CategoryStruct.comp e₀.hom f' = CategoryTheory.CategoryStruct.comp f e₁.hom)
                            CategoryTheory.Limits.Fork.isLimitOfIsos._auto_1 →
                          autoParam
                              (CategoryTheory.CategoryStruct.comp e₀.hom g' =
                                CategoryTheory.CategoryStruct.comp g e₁.hom)
                              CategoryTheory.Limits.Fork.isLimitOfIsos._auto_3 →
                            autoParam
                                (CategoryTheory.CategoryStruct.comp e.hom c'.ι =
                                  CategoryTheory.CategoryStruct.comp c.ι e₀.hom)
                                CategoryTheory.Limits.Fork.isLimitOfIsos._auto_5 →
                              CategoryTheory.Limits.IsLimit c'
-- Mathlib.Algebra.Module.LocalizedModule.Basic
_private.Mathlib.Algebra.Module.LocalizedModule.Basic.0.LocalizedModule.one_smul_aux : ∀ {R : Type u} [inst : CommSemiring R] {S : Submonoid R} {M : Type v} [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {T : Type u_1} [inst_3 : CommSemiring T] [inst_4 : Algebra R T] [inst_5 : IsLocalization S T]
  (p : LocalizedModule S M), 1 • p = p
-- Mathlib.LinearAlgebra.PiTensorProduct.Dual
/-- The canonical linear map from `⨂[R] i, Dual R (M i)` to `Dual R (⨂[R] i, M i)`,
sending `⨂ₜ[R] i, f i` to the composition of `PiTensorProduct.map f` with
the linear equivalence `⨂[R] i, R →ₗ R` given by multiplication.  -/
PiTensorProduct.dualDistrib : {ι : Type u_1} →
  {R : Type u_2} →
    {M : ι → Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : (i : ι) → AddCommMonoid (M i)] →
          [inst_2 : (i : ι) → Module R (M i)] →
            [Finite ι] →
              (PiTensorProduct R fun i => Module.Dual R (M i)) →ₗ[R] Module.Dual R (PiTensorProduct R fun i => M i)
-- Qq.Typ
/-- Check that the claim `$lhs =Q $rhs` is actually true; that the two terms are defeq.  -/
Qq.QuotedDefEq.check : {u : Lean.Level} → {α : Q(Sort u)} → {lhs rhs : Q(«$α»)} → «$lhs» =Q «$rhs» → Lean.MetaM Unit
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.ObjectProperty.IsCoseparating.epi_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.ObjectProperty C},
  P.IsCoseparating →
    ∀ {X Y : C} (f : X ⟶ Y),
      CategoryTheory.Epi f ↔
        ∀ (G : C),
          P G →
            ∀ (g₁ g₂ : Y ⟶ G),
              CategoryTheory.CategoryStruct.comp f g₁ = CategoryTheory.CategoryStruct.comp f g₂ → g₁ = g₂
-- Mathlib.Combinatorics.Optimization.ValuedCSP
/-- Valid fractional operation contains an operation.  -/
FractionalOperation.IsValid.contains : ∀ {D : Type u_1} {m : ℕ} {ω : FractionalOperation D m}, ω.IsValid → ∃ g, g ∈ ω
-- Mathlib.Topology.Algebra.ProperAction.Basic
/-- If a T1 group acts properly on a topological space,
then this topological space is T2.  -/
t2Space_of_properVAdd_of_t1AddGroup : ∀ {G : Type u_1} {X : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G X] [inst_2 : TopologicalSpace G]
  [inst_3 : TopologicalSpace X] [h_proper : ProperVAdd G X] [T1Space G], T2Space X
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
SimplexCategory.hom_zero_zero : ∀ (f : { len := 0 } ⟶ { len := 0 }), f = CategoryTheory.CategoryStruct.id { len := 0 }
-- Mathlib.Data.ENNReal.Inv
ENNReal.inv_div : ∀ {a b : ENNReal}, b ≠ ⊤ ∨ a ≠ ⊤ → b ≠ 0 ∨ a ≠ 0 → (a / b)⁻¹ = b / a
-- Lean.Server.Requests
Lean.Server.RequestContext.serverRequestEmitter : Lean.Server.RequestContext → Lean.Server.ServerRequestEmitter
-- Mathlib.Algebra.Star.StarAlgHom
NonUnitalStarAlgHom.coe_comp : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [inst : Monoid R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : DistribMulAction R A] [inst_3 : Star A] [inst_4 : NonUnitalNonAssocSemiring B]
  [inst_5 : DistribMulAction R B] [inst_6 : Star B] [inst_7 : NonUnitalNonAssocSemiring C]
  [inst_8 : DistribMulAction R C] [inst_9 : Star C] (f : B →⋆ₙₐ[R] C) (g : A →⋆ₙₐ[R] B), ⇑(f.comp g) = ⇑f ∘ ⇑g
-- Mathlib.NumberTheory.ModularForms.Petersson
UpperHalfPlane.petersson_continuous : ∀ (k : ℤ) {f f' : UpperHalfPlane → ℂ}, Continuous f → Continuous f' → Continuous (UpperHalfPlane.petersson k f f')
-- Mathlib.MeasureTheory.SetSemiring
MeasureTheory.IsSetSemiring.empty_notMem_disjointOfDiff : ∀ {α : Type u_1} {C : Set (Set α)} {s t : Set α} (hC : MeasureTheory.IsSetSemiring C) (hs : s ∈ C) (ht : t ∈ C),
  ∅ ∉ hC.disjointOfDiff hs ht
-- Mathlib.RingTheory.MvPowerSeries.Rename
MvPowerSeries.rename_rename : ∀ {σ : Type u_1} {τ : Type u_2} {γ : Type u_3} {R : Type u_4} (f : σ → τ) (g : τ → γ) [inst : Filter.TendstoCofinite f]
  [inst_1 : CommSemiring R] [inst_2 : Filter.TendstoCofinite g] (p : MvPowerSeries σ R),
  (MvPowerSeries.rename g) ((MvPowerSeries.rename f) p) = (MvPowerSeries.rename (g ∘ f)) p
-- Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
RingHom.IsIntegralElem.map : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_4} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Ring T] {f : R →+* S}
  {x : S}, f.IsIntegralElem x → ∀ (g : S →+* T), (g.comp f).IsIntegralElem (g x)