mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.ExternalProduct.Basic
CategoryTheory.MonoidalCategory.prodCompExternalProduct_inv_app : ∀ {J₁ : Type u₁} {J₂ : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} J₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} J₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  [inst_3 : CategoryTheory.MonoidalCategory C] {I₁ : Type u₃} {I₂ : Type u₄}
  [inst_4 : CategoryTheory.Category.{v₃, u₃} I₁] [inst_5 : CategoryTheory.Category.{v₄, u₄} I₂]
  (F₁ : CategoryTheory.Functor I₁ J₁) (G₁ : CategoryTheory.Functor J₁ C) (F₂ : CategoryTheory.Functor I₂ J₂)
  (G₂ : CategoryTheory.Functor J₂ C) (X : I₁ × I₂),
  (CategoryTheory.MonoidalCategory.prodCompExternalProduct F₁ G₁ F₂ G₂).inv.app X =
    CategoryTheory.CategoryStruct.id
      (CategoryTheory.MonoidalCategoryStruct.tensorObj (G₁.obj (F₁.obj X.1)) (G₂.obj (F₂.obj X.2)))
-- Mathlib.Algebra.Order.BigOperators.Group.Multiset
Multiset.pow_card_le_prod : ∀ {α : Type u_2} [inst : CommMonoid α] [inst_1 : Preorder α] {s : Multiset α} {a : α} [MulLeftMono α],
  (∀ x ∈ s, a ≤ x) → a ^ s.card ≤ s.prod
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.Const.maxEntry?.match_1.eq_2 : ∀ {α : Type u_1} {β : Type u_2} (motive : (Std.DTreeMap.Internal.Impl α fun x => β) → Sort u_3) (size : ℕ) (k : α)
  (v : β) (l : Std.DTreeMap.Internal.Impl α fun x => β) (h_1 : Unit → motive Std.DTreeMap.Internal.Impl.leaf)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β) →
          (l : Std.DTreeMap.Internal.Impl α fun x => β) →
            motive (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf))
  (h_3 :
    (size : ℕ) →
      (k : α) →
        (v : β) →
          (l r : Std.DTreeMap.Internal.Impl α fun x => β) →
            (size_1 : ℕ) →
              (k_1 : α) →
                (v_1 : β) →
                  (l_1 r_1 : Std.DTreeMap.Internal.Impl α fun x => β) →
                    r = Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r_1 →
                      motive
                        (Std.DTreeMap.Internal.Impl.inner size k v l
                          (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r_1))),
  (match Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf with
    | Std.DTreeMap.Internal.Impl.leaf => h_1 ()
    | Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf => h_2 size k v l
    | Std.DTreeMap.Internal.Impl.inner size k v l r@h:(Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r_1) =>
      h_3 size k v l r size_1 k_1 v_1 l_1 r_1 h) =
    h_2 size k v l
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
LinearIsometry.lTensor_def : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : InnerProductSpace 𝕜 G] (f : F →ₗᵢ[𝕜] G),
  LinearIsometry.lTensor E f = TensorProduct.mapIsometry LinearIsometry.id f
-- Mathlib.Topology.Connected.PathConnected
Joined.mem_pathComponent : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y z : X}, Joined y z → y ∈ pathComponent x → z ∈ pathComponent x
-- Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective
AlgebraicGeometry.universallyInjective_iff : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y),
  AlgebraicGeometry.UniversallyInjective f ↔
    (AlgebraicGeometry.topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] x =>
          Function.Injective x).universally
      f
-- Lean.Meta.Sym.Simp.SimpM
Lean.Meta.Sym.Simp.instInhabitedResult.default : Lean.Meta.Sym.Simp.Result
-- Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
CategoryTheory.ObjectProperty.IsClosedUnderColimitsOfShape.mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P : CategoryTheory.ObjectProperty C} {J : Type u'}
  [inst_1 : CategoryTheory.Category.{v', u'} J], P.colimitsOfShape J ≤ P → P.IsClosedUnderColimitsOfShape J
-- Mathlib.Algebra.Order.Ring.Archimedean
ArchimedeanClass.eq_zero_or_top_of_archimedean : ∀ {S : Type u_3} [inst : LinearOrder S] [inst_1 : CommRing S] [inst_2 : IsStrictOrderedRing S] [Archimedean S]
  (x : ArchimedeanClass S), x = 0 ∨ x = ⊤
-- Mathlib.NumberTheory.Pell
/-- When `d` is positive and not a square, then the group of solutions to the Pell equation
`x^2 - d*y^2 = 1` has a unique positive generator (up to sign).  -/
Pell.existsUnique_pos_generator : ∀ {d : ℤ}, 0 < d → ¬IsSquare d → ∃! a₁, 1 < a₁.x ∧ 0 < a₁.y ∧ ∀ (a : Pell.Solution₁ d), ∃ n, a = a₁ ^ n ∨ a = -a₁ ^ n
-- Mathlib.Data.Finsupp.Multiset
Finsupp.toMultiset_strictMono : ∀ {ι : Type u_3}, StrictMono ⇑Finsupp.toMultiset
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.isEmptyRingEquiv_apply : ∀ (R : Type u) (σ : Type u_1) [inst : CommSemiring R] [inst_1 : IsEmpty σ] (a : AddMonoidAlgebra R (σ →₀ ℕ)),
  (MvPolynomial.isEmptyRingEquiv R σ) a = a.coeff 0
-- Mathlib.RingTheory.Extension.Cotangent.Basic
Algebra.Extension.Hom.sub_one_tmul : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {P : Algebra.Extension R S}
  {R' : Type u'} {S' : Type v'} [inst_3 : CommRing R'] [inst_4 : CommRing S'] [inst_5 : Algebra R' S']
  {P' : Algebra.Extension R' S'} [inst_6 : Algebra R R'] [inst_7 : Algebra S S'] [inst_8 : Algebra R S']
  [inst_9 : IsScalarTower R R' S'] [inst_10 : IsScalarTower R S S'] (f g : P.Hom P') (x : P.Ring),
  (f.sub g) (1 ⊗ₜ[P.Ring] (KaehlerDifferential.D R P.Ring) x) = Algebra.Extension.Cotangent.mk ((f.subToKer g) x)
-- Init.Data.Int.DivMod.Bootstrap
Int.mul_ediv_self : ∀ (a b : ℤ), b * (a / b) = a - a % b
-- Mathlib.Algebra.Module.LinearMap.Defs
/-- `SemilinearMapClass F σ M M₂` asserts `F` is a type of bundled `σ`-semilinear maps `M → M₂`.

See also `LinearMapClass F R M M₂` for the case where `σ` is the identity map on `R`.

A map `f` between an `R`-module and an `S`-module over a ring homomorphism `σ : R →+* S`
is semilinear if it satisfies the two properties `f (x + y) = f x + f y` and
`f (c • x) = (σ c) • f x`.  -/
SemilinearMapClass : (F : Type u_14) →
  {R : outParam (Type u_15)} →
    {S : outParam (Type u_16)} →
      [inst : Semiring R] →
        [inst_1 : Semiring S] →
          outParam (R →+* S) →
            (M : outParam (Type u_17)) →
              (M₂ : outParam (Type u_18)) →
                [inst_2 : AddCommMonoid M] →
                  [inst_3 : AddCommMonoid M₂] → [Module R M] → [Module S M₂] → [FunLike F M M₂] → Prop
-- Mathlib.Combinatorics.SimpleGraph.Cayley
SimpleGraph.addCayley_adj_add_iff_right : ∀ {M : Type u_1} [inst : AddSemigroup M] [IsLeftCancelAdd M] {s : Set M} {u v d : M},
  (SimpleGraph.addCayley s).Adj (d + u) (d + v) ↔ (SimpleGraph.addCayley s).Adj u v
-- Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
/-- The `turanGraph` is, up to isomorphism, the unique extremal graph forbidding `⊤`.

This is **Turán's theorem** restated in terms of the extremal numbers of `⊤`.
See `SimpleGraph.isTuranMaximal_iff_nonempty_iso_turanGraph`.  -/
SimpleGraph.card_edgeFinset_eq_extremalNumber_top_iff_nonempty_iso_turanGraph : ∀ {V : Type u_1} [inst : Fintype V] {G : SimpleGraph V} [inst_1 : DecidableRel G.Adj] {α : Type u_2}
  [inst_2 : Fintype α] [Nontrivial α],
  ⊤.Free G ∧ G.edgeFinset.card = SimpleGraph.extremalNumber (Fintype.card V) ⊤ ↔
    Nonempty (G ≃g SimpleGraph.turanGraph (Fintype.card V) (Fintype.card α - 1))
-- Mathlib.SetTheory.Cardinal.Embedding
Fin.Embedding.exists_embedding_disjoint_range_of_add_le_ENat_card : ∀ {α : Type u_1} {n : ℕ} {s : Set α} [Finite ↑s], ↑s.ncard + ↑n ≤ ENat.card α → ∃ y, Disjoint s (Set.range ⇑y)
-- Mathlib.Topology.EMetricSpace.Lipschitz
LocallyLipschitz.locallyLipschitzOn : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {s : Set α} {f : α → β},
  LocallyLipschitz f → LocallyLipschitzOn s f
-- Mathlib.Tactic.ClickSuggestions.Util
/-- Signify that at least one suggestion has been made.  -/
Mathlib.Tactic.ClickSuggestions.markProgress : Mathlib.Tactic.ClickSuggestions.ClickSuggestionsM Unit
-- Init.Data.String.Defs
List.utf8Encode_singleton : ∀ {c : Char}, [c].utf8Encode = (String.utf8EncodeChar c).toByteArray
-- Mathlib.Combinatorics.Additive.ETransform
Finset.addETransformLeft_zero : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : AddGroup α] (x : Finset α × Finset α),
  Finset.addETransformLeft 0 x = x
-- Init.Data.List.Nat.TakeDrop
List.reverse_take : ∀ {α : Type u_1} {l : List α} {i : ℕ}, (List.take i l).reverse = List.drop (l.length - i) l.reverse
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
/-- The indexed minimum of a function is bounded below by a uniform lower bound  -/
le_ciInf : ∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompleteLattice α] [Nonempty ι] {f : ι → α} {c : α},
  (∀ (x : ι), c ≤ f x) → c ≤ iInf f
-- Mathlib.Tactic.MoveAdd
/-- `rankSums op tgt instructions` takes as input
* the name `op` of a binary operation,
* an `Expr`ession `tgt`,
* a list `instructions` of pair `(expression, Boolean)`.

It extracts the maximal subexpressions of `tgt` whose head symbol is `op`
(i.e. the maximal subexpressions that consist only of applications of the binary operation `op`),
it rearranges the operands of such subexpressions following the order implied by `instructions`
(as in `reorderUsing`),
it returns the list of pairs of expressions `(old_sum, new_sum)`, for which `old_sum ≠ new_sum`
sorted by decreasing value of `Lean.Expr.size`.
In particular, a subexpression of an `old_sum` can only appear *after* its over-expression.
 -/
Mathlib.MoveAdd.rankSums : Lean.Name → Lean.Expr → List (Lean.Expr × Bool) → Lean.MetaM (List (Lean.Expr × Lean.Expr))
-- Mathlib.LinearAlgebra.Matrix.ToLin
LinearMap.toMatrixAlgEquiv_apply : ∀ {R : Type u_1} [inst : CommSemiring R] {n : Type u_4} [inst_1 : Fintype n] [inst_2 : DecidableEq n] {M₁ : Type u_5}
  [inst_3 : AddCommMonoid M₁] [inst_4 : Module R M₁] (v₁ : Module.Basis n R M₁) (f : M₁ →ₗ[R] M₁) (i j : n),
  (LinearMap.toMatrixAlgEquiv v₁) f i j = (v₁.repr (f (v₁ j))) i
-- Lean.Server.FileWorker.SemanticHighlighting
/-- Start position of the semantic token.  -/
Lean.Server.FileWorker.AbsoluteLspSemanticToken.type : Lean.Server.FileWorker.AbsoluteLspSemanticToken → Lean.Lsp.SemanticTokenType
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Real.logb_neg_iff_of_base_lt_one : ∀ {b x : ℝ}, 0 < b → b < 1 → 0 < x → (Real.logb b x < 0 ↔ 1 < x)
-- Init.Data.Int.Gcd
Int.natAbs_div_gcd_pos_of_ne_zero_left : ∀ {a : ℤ} (b : ℤ), a ≠ 0 → 0 < a.natAbs / a.gcd b
-- Mathlib.Analysis.SpecialFunctions.Pow.Complex
Complex.conj_cpow_eq_ite : ∀ (x n : ℂ), (starRingEnd ℂ) x ^ n = if x.arg = Real.pi then x ^ n else (starRingEnd ℂ) (x ^ (starRingEnd ℂ) n)
-- Mathlib.Data.Int.WithZero
WithZeroMulInt.toNNReal_lt_one_iff : ∀ {e : NNReal} {m : WithZero (Multiplicative ℤ)} (he : 1 < e), (WithZeroMulInt.toNNReal ⋯) m < 1 ↔ m < 1
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.map_mul_right_eq_self : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Mul G] (μ : MeasureTheory.Measure G) [μ.IsMulRightInvariant]
  (g : G), MeasureTheory.Measure.map (fun x => x * g) μ = μ
-- Mathlib.LinearAlgebra.Matrix.WithConv
WithConv.symm_matrixToLin'StarAlgEquiv_apply : ∀ {m : Type u_1} {n : Type u_2} {α : Type u_3} [inst : CommSemiring α] [inst_1 : StarRing α] [inst_2 : Fintype n]
  [inst_3 : DecidableEq n] (x : WithConv ((n → α) →ₗ[α] m → α)),
  (WithConv.matrixToLin'StarAlgEquiv m n α).symm x = WithConv.toConv (LinearMap.toMatrix' x.ofConv)
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
/-- `comapSMul` is multiplicative  -/
SkewMonoidAlgebra.comapMulAction : {G : Type u_2} →
  {M : Type u_6} →
    {α : Type u_7} →
      [inst : Monoid G] → [inst_1 : AddCommMonoid M] → [MulAction G α] → MulAction G (SkewMonoidAlgebra M α)
-- Lean.Meta.Sym.InstantiateS
/-- Internal variant of `betaRevS` that runs in `AlphaShareBuilderM`.  -/
_private.Lean.Meta.Sym.InstantiateS.0.Lean.Meta.Sym.betaRevS' : Lean.Expr → Array Lean.Expr → Lean.Meta.Sym.Internal.AlphaShareBuilderM Lean.Expr
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.optionEquivRight_X_none : ∀ (R : Type u) (S₁ : Type v) [inst : CommSemiring R],
  (MvPolynomial.optionEquivRight R S₁) (MvPolynomial.X none) = MvPolynomial.C Polynomial.X
-- Mathlib.Order.OmegaCompletePartialOrder
OmegaCompletePartialOrder.ωSup_eq_of_isLUB : ∀ {α : Type u_2} [inst : OmegaCompletePartialOrder α] {c : OmegaCompletePartialOrder.Chain α} {a : α},
  IsLUB (Set.range ⇑c) a → a = OmegaCompletePartialOrder.ωSup c
-- Lean.Compiler.ExternAttr
Lean.ExternEntry.inline.injEq : ∀ (backend : Lean.Name) (pattern : String) (backend_1 : Lean.Name) (pattern_1 : String),
  (Lean.ExternEntry.inline backend pattern = Lean.ExternEntry.inline backend_1 pattern_1) =
    (backend = backend_1 ∧ pattern = pattern_1)
-- Mathlib.Tactic.SplitIfs
/-- Main loop of `split_ifs`. Pulls names for new hypotheses from `hNames`.
Stops if it encounters a condition in the passed-in `List Expr`.
 -/
_private.Mathlib.Tactic.SplitIfs.0.Mathlib.Tactic.splitIfsCore : Lean.Elab.Tactic.Location →
  IO.Ref (List (Lean.TSyntax `Lean.binderIdent)) → List Lean.Expr → Lean.Elab.Tactic.TacticM Unit
-- Std.Http.Server.Connection
_private.Std.Http.Server.Connection.0.Std.Http.Server.Connection.ConnectionState.mk : {β : Type} →
  Std.Http.Protocol.H1.Machine Std.Http.Protocol.H1.Direction.receiving →
    Std.Http.Body.Stream →
      Option Std.Time.Millisecond.Offset →
        Std.Time.Millisecond.Offset →
          Option Std.Time.Timestamp →
            Std.Channel (Except IO.Error (Std.Http.Response β)) →
              Option β →
                Bool → Option ℕ → Bool → Option Std.Http.Request.Head → Std.Http.Server.Connection.ConnectionState✝ β
-- Mathlib.Data.Ordmap.Ordset
Ordnode.Valid'.node3R : ∀ {α : Type u_1} [inst : Preorder α] {l : Ordnode α} {x : α} {m : Ordnode α} {y : α} {r : Ordnode α} {o₁ : WithBot α}
  {o₂ : WithTop α},
  Ordnode.Valid' o₁ l ↑x →
    Ordnode.Valid' (↑x) m ↑y →
      Ordnode.Valid' (↑y) r o₂ →
        Ordnode.BalancedSz l.size (m.size + r.size + 1) →
          Ordnode.BalancedSz m.size r.size → Ordnode.Valid' o₁ (l.node3R x m y r) o₂
-- Mathlib.Algebra.Group.Prod
addAddMonoidHom_apply : ∀ {α : Type u_6} [inst : AddCommMonoid α] (a : α × α), addAddMonoidHom a = addAddHom.toFun a
-- Mathlib.LinearAlgebra.RootSystem.Finite.G2
RootPairing.EmbeddedG2.mem_allRoots : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N)
  [inst_5 : P.EmbeddedG2] [Finite ι] [CharZero R] [IsDomain R] [P.IsIrreducible] (i : ι),
  P.root i ∈ RootPairing.EmbeddedG2.allRoots P
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
WeierstrassCurve.ψ₂_sq : ∀ {R : Type r} [inst : CommRing R] (W : WeierstrassCurve R), W.ψ₂ ^ 2 = Polynomial.C W.Ψ₂Sq + 4 * W.toAffine.polynomial
-- Mathlib.Algebra.Order.Module.Defs
/-- Do not use this. Use `lt_of_smul_lt_smul_left` instead.  -/
PosSMulReflectLT.lt_of_smul_lt_smul_left : ∀ {α : Type u_1} {β : Type u_2} {inst : SMul α β} {inst_1 : Preorder α} {inst_2 : Preorder β} {inst_3 : Zero α}
  [self : PosSMulReflectLT α β] ⦃a : α⦄, 0 ≤ a → ∀ ⦃b₁ b₂ : β⦄, a • b₁ < a • b₂ → b₁ < b₂
-- Mathlib.LinearAlgebra.BilinearForm.Isometry
LinearMap.BilinForm.Isometry.ofEq_apply : ∀ {R : Type u_1} {M₁ : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁] [inst_2 : Module R M₁]
  {B₁ B₂ : LinearMap.BilinForm R M₁} (h : B₁ = B₂) (x : M₁), (LinearMap.BilinForm.Isometry.ofEq h) x = x
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometryEquiv.trans_refl : ∀ {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [inst : NormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup V] [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P]
  [inst_4 : NormedAddTorsor V P] [inst_5 : SeminormedAddCommGroup V₂] [inst_6 : NormedSpace 𝕜 V₂]
  [inst_7 : PseudoMetricSpace P₂] [inst_8 : NormedAddTorsor V₂ P₂] (e : P ≃ᵃⁱ[𝕜] P₂),
  e.trans (AffineIsometryEquiv.refl 𝕜 P₂) = e
-- Mathlib.Order.CompleteLattice.Finset
/-- Union of an indexed family of sets `s : ι → Set α` is equal to the union of the unions
of finite subfamilies. This version works for `ι : Sort*`. See also `iUnion_eq_iUnion_finset` for
a version that assumes `ι : Type*` but avoids `PLift`s in the right-hand side.  -/
Set.iUnion_eq_iUnion_finset' : ∀ {α : Type u_2} {ι' : Sort u_7} (s : ι' → Set α), ⋃ i, s i = ⋃ t, ⋃ i ∈ t, s i.down
-- Mathlib.Analysis.Normed.Ring.WithAbs
/-- **Alias** of `WithAbs.norm_eq_apply_ofAbs`. -/
WithAbs.norm_eq_abv : ∀ {R : Type u_1} [inst : Ring R] (v : AbsoluteValue R ℝ) (x : WithAbs v), ‖x‖ = v x.ofAbs
-- Mathlib.RingTheory.RingHom.Locally
/-- In the definition of `Locally` we may replace `Localization.Away` with an arbitrary
algebra satisfying `IsLocalization.Away`.  -/
RingHom.locally_iff_isLocalization : ∀ {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} {R S : Type u}
  [inst : CommRing R] [inst_1 : CommRing S],
  (RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => P) →
    ∀ (f : R →+* S),
      RingHom.Locally (fun {R S} [CommRing R] [CommRing S] => P) f ↔
        ∃ s,
          ∃ (_ : Ideal.span ↑s = ⊤),
            ∀ t ∈ s,
              ∀ (Sₜ : Type u) [inst_2 : CommRing Sₜ] [inst_3 : Algebra S Sₜ] [IsLocalization.Away t Sₜ],
                P ((algebraMap S Sₜ).comp f)
-- Mathlib.Algebra.Pointwise.Stabilizer
MulAction.stabilizer_finset_empty : ∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : DecidableEq α],
  MulAction.stabilizer G ∅ = ⊤
-- Mathlib.Topology.Metrizable.Uniformity
EMetricSpace.metrizableSpace : ∀ {α : Type u_2} [inst : EMetricSpace α], TopologicalSpace.MetrizableSpace α
-- Mathlib.Tactic.SimpRw
/-- `simp_rw` functions as a mix of `simp` and `rw`. Like `rw`, it applies each
rewrite rule in the given order, but like `simp` it repeatedly applies these
rules and also under binders like `∀ x, ...`, `∃ x, ...` and `fun x ↦...`.
Usage:

- `simp_rw [lemma_1, ..., lemma_n]` will rewrite the goal by applying the
  lemmas in that order. A lemma preceded by `←` is applied in the reverse direction.
- `simp_rw [lemma_1, ..., lemma_n] at h₁ ... hₙ` will rewrite the given hypotheses.
- `simp_rw [...] at *` rewrites in the whole context: all hypotheses and the goal.

Lemmas passed to `simp_rw` must be expressions that are valid arguments to `simp`.
For example, neither `simp` nor `rw` can solve the following, but `simp_rw` can:

```lean
example {a : ℕ}
    (h1 : ∀ a b : ℕ, a - 1 ≤ b ↔ a ≤ b + 1)
    (h2 : ∀ a b : ℕ, a ≤ b ↔ ∀ c, c < a → c < b) :
    (∀ b, a - 1 ≤ b) = ∀ b c : ℕ, c < a → c < b + 1 := by
  simp_rw [h1, h2]
```
 -/
Mathlib.Tactic.tacticSimp_rw___ : Lean.ParserDescr
-- Mathlib.Analysis.Complex.Circle
Real.probChar_apply : ∀ (x : ℝ), ↑(Real.probChar x) = Complex.exp (↑x * Complex.I)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
WeierstrassCurve.Affine.map_negAddY : ∀ {R : Type r} {S : Type s} [inst : CommRing R] [inst_1 : CommRing S] {W' : WeierstrassCurve.Affine R} (f : R →+* S)
  (x₁ y₁ x₂ ℓ : R), (W'.map f).negAddY (f x₁) (f x₂) (f y₁) (f ℓ) = f (W'.negAddY x₁ x₂ y₁ ℓ)
-- Init.Data.SInt.Bitwise
Int8.zero_shiftRight : ∀ {a : Int8}, 0 >>> a = 0
-- Mathlib.Algebra.Lie.Prod
LieHom.snd_comp_inl : ∀ (R : Type u_1) (L₁ : Type u_2) (L₂ : Type u_3) [inst : CommRing R] [inst_1 : LieRing L₁] [inst_2 : LieAlgebra R L₁]
  [inst_3 : LieRing L₂] [inst_4 : LieAlgebra R L₂], (LieHom.snd R L₁ L₂).comp (LieHom.inl R L₁ L₂) = 0
-- Mathlib.GroupTheory.GroupAction.FixedPoints
MulAction.fixedBy_subset_fixedBy_zpow : ∀ (α : Type u_1) {G : Type u_2} [inst : Group G] [inst_1 : MulAction G α] (g : G) (j : ℤ),
  MulAction.fixedBy α g ⊆ MulAction.fixedBy α (g ^ j)
-- Mathlib.GroupTheory.Complement
Subgroup.IsComplement.encard_right : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} {T : Set G} [H.FiniteIndex],
  Subgroup.IsComplement (↑H) T → T.encard = ↑H.index
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.homEquiv_naturality_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) {X' X : C} {Y : D} (f : X' ⟶ X)
  (g : F.obj X ⟶ Y),
  (adj.homEquiv X' Y) (CategoryTheory.CategoryStruct.comp (F.map f) g) =
    CategoryTheory.CategoryStruct.comp f ((adj.homEquiv X Y) g)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.contains_eq_false_iff_not_mem : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] {k : α},
  m.contains k = false ↔ k ∉ m
-- Mathlib.Topology.Closure
frontier_interior_subset : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, frontier (interior s) ⊆ frontier s
-- Mathlib.Tactic.FunProp.Types
Mathlib.Meta.FunProp.Origin.fvar.injEq : ∀ (fvarId fvarId_1 : Lean.FVarId),
  (Mathlib.Meta.FunProp.Origin.fvar fvarId = Mathlib.Meta.FunProp.Origin.fvar fvarId_1) = (fvarId = fvarId_1)
-- Mathlib.Combinatorics.SimpleGraph.Metric
/-- The ball of radius `⊤` is the connected component of the center.  -/
SimpleGraph.ball_top : ∀ {V : Type u_1} {G : SimpleGraph V} {c : V}, G.ball c ⊤ = (G.connectedComponentMk c).supp
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.Poly.combine.induct_unfolding : ∀ (motive : Lean.Grind.Linarith.Poly → Lean.Grind.Linarith.Poly → Lean.Grind.Linarith.Poly → Prop),
  (∀ (p₂ : Lean.Grind.Linarith.Poly), motive Lean.Grind.Linarith.Poly.nil p₂ p₂) →
    (∀ (p₁ : Lean.Grind.Linarith.Poly),
        (p₁ = Lean.Grind.Linarith.Poly.nil → False) → motive p₁ Lean.Grind.Linarith.Poly.nil p₁) →
      (∀ (a₁ : ℤ) (x₁ : Lean.Grind.Linarith.Var) (p₁ : Lean.Grind.Linarith.Poly) (a₂ : ℤ) (x₂ : Lean.Grind.Linarith.Var)
          (p₂ : Lean.Grind.Linarith.Poly),
          Nat.beq x₁ x₂ = true →
            have a := a₁ + a₂;
            (a == 0) = true →
              motive p₁ p₂ (p₁.combine p₂) →
                motive (Lean.Grind.Linarith.Poly.add a₁ x₁ p₁) (Lean.Grind.Linarith.Poly.add a₂ x₂ p₂)
                  (p₁.combine p₂)) →
        (∀ (a₁ : ℤ) (x₁ : Lean.Grind.Linarith.Var) (p₁ : Lean.Grind.Linarith.Poly) (a₂ : ℤ)
            (x₂ : Lean.Grind.Linarith.Var) (p₂ : Lean.Grind.Linarith.Poly),
            Nat.beq x₁ x₂ = true →
              have a := a₁ + a₂;
              (a == 0) = false →
                motive p₁ p₂ (p₁.combine p₂) →
                  motive (Lean.Grind.Linarith.Poly.add a₁ x₁ p₁) (Lean.Grind.Linarith.Poly.add a₂ x₂ p₂)
                    (Lean.Grind.Linarith.Poly.add a x₁ (p₁.combine p₂))) →
          (∀ (a₁ : ℤ) (x₁ : Lean.Grind.Linarith.Var) (p₁ : Lean.Grind.Linarith.Poly) (a₂ : ℤ)
              (x₂ : Lean.Grind.Linarith.Var) (p₂ : Lean.Grind.Linarith.Poly),
              Nat.beq x₁ x₂ = false →
                Nat.blt x₂ x₁ = true →
                  motive p₁ (Lean.Grind.Linarith.Poly.add a₂ x₂ p₂)
                      (p₁.combine (Lean.Grind.Linarith.Poly.add a₂ x₂ p₂)) →
                    motive (Lean.Grind.Linarith.Poly.add a₁ x₁ p₁) (Lean.Grind.Linarith.Poly.add a₂ x₂ p₂)
                      (Lean.Grind.Linarith.Poly.add a₁ x₁ (p₁.combine (Lean.Grind.Linarith.Poly.add a₂ x₂ p₂)))) →
            (∀ (a₁ : ℤ) (x₁ : Lean.Grind.Linarith.Var) (p₁ : Lean.Grind.Linarith.Poly) (a₂ : ℤ)
                (x₂ : Lean.Grind.Linarith.Var) (p₂ : Lean.Grind.Linarith.Poly),
                Nat.beq x₁ x₂ = false →
                  Nat.blt x₂ x₁ = false →
                    motive (Lean.Grind.Linarith.Poly.add a₁ x₁ p₁) p₂
                        ((Lean.Grind.Linarith.Poly.add a₁ x₁ p₁).combine p₂) →
                      motive (Lean.Grind.Linarith.Poly.add a₁ x₁ p₁) (Lean.Grind.Linarith.Poly.add a₂ x₂ p₂)
                        (Lean.Grind.Linarith.Poly.add a₂ x₂ ((Lean.Grind.Linarith.Poly.add a₁ x₁ p₁).combine p₂))) →
              ∀ (p₁ p₂ : Lean.Grind.Linarith.Poly), motive p₁ p₂ (p₁.combine p₂)
-- Mathlib.Topology.MetricSpace.Kuratowski
/-- Every separable metric space embeds isometrically in `ℓ^∞(ℕ)`.  -/
KuratowskiEmbedding.exists_isometric_embedding : ∀ (α : Type u) [inst : MetricSpace α] [TopologicalSpace.SeparableSpace α], ∃ f, Isometry f
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.le_def : ∀ {x y : ZFSet.{u}}, x ⊆ y ↔ x ⊆ y