mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
SchwartzMap.compCLM_apply : ∀ (𝕜 : Type u_2) {D : Type u_4} {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : RCLike 𝕜] [inst_5 : NormedAddCommGroup D]
  [inst_6 : NormedSpace ℝ D] [inst_7 : NormedSpace 𝕜 F] {g : D → E} (hg : Function.HasTemperateGrowth g)
  (hg_upper : ∃ k C, ∀ (x : D), ‖x‖ ≤ C * (1 + ‖g x‖) ^ k) (f : SchwartzMap E F),
  ⇑((SchwartzMap.compCLM 𝕜 hg hg_upper) f) = ⇑f ∘ g
-- Mathlib.Algebra.Category.Grp.IsFinite
/-- The Serre class of finite abelian groups
in the category of abelian groups.  -/
AddCommGrpCat.isFinite : CategoryTheory.ObjectProperty AddCommGrpCat
-- Mathlib.Tactic.ClickSuggestions.TryPremises
/-- Get the candidate theorems from imported files.  -/
_private.Mathlib.Tactic.ClickSuggestions.TryPremises.0.Mathlib.Tactic.ClickSuggestions.getImportCandidates : Lean.Expr →
  Lean.Expr →
    Array Mathlib.Tactic.ClickSuggestions.GrwPos →
      Mathlib.Tactic.ClickSuggestions.RwKind →
        Option Lean.Expr →
          (String → BaseIO Unit) →
            Mathlib.Tactic.ClickSuggestions.ClickSuggestionsM (Array Mathlib.Tactic.ClickSuggestions.Candidates✝)
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
AlgebraicGeometry.LocallyRingedSpace.stalkMap_congr_point_assoc : ∀ {X Y : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Y) (x x' : ↑X.toTopCat) (hxx' : x = x') {Z : CommRingCat}
  (h : X.presheaf.stalk x' ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap f x)
      (CategoryTheory.CategoryStruct.comp (X.presheaf.stalkSpecializes ⋯) h) =
    CategoryTheory.CategoryStruct.comp (Y.presheaf.stalkSpecializes ⋯)
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap f x') h)
-- Mathlib.RingTheory.FractionalIdeal.Basic
FractionalIdeal.mul_induction_on : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  {I J : FractionalIdeal S P} {C : P → Prop} {r : P},
  r ∈ I * J → (∀ i ∈ I, ∀ j ∈ J, C (i * j)) → (∀ (x y : P), C x → C y → C (x + y)) → C r
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.op_vadd_set_subset_add : ∀ {α : Type u_2} [inst : Add α] {s t : Set α} {a : α}, a ∈ t → AddOpposite.op a +ᵥ s ⊆ s + t
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
MeasureTheory.SignedMeasure.totalVariation.eq_1 : ∀ {α : Type u_1} [inst : MeasurableSpace α] (s : MeasureTheory.SignedMeasure α),
  s.totalVariation = s.toJordanDecomposition.posPart + s.toJordanDecomposition.negPart
-- Mathlib.Probability.Process.Stopping
MeasureTheory.IsStoppingTime.measurableSet_le : ∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : Preorder ι] {f : MeasureTheory.Filtration ι m}
  {τ : Ω → WithTop ι}, MeasureTheory.IsStoppingTime f τ → ∀ (i : ι), MeasurableSet {ω | τ ω ≤ ↑i}
-- Mathlib.Topology.Algebra.Module.ClosedSubmodule
ClosedSubmodule.map_le_iff_le_comap : ∀ {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : TopologicalSpace M] [inst_3 : Module R M] [inst_4 : AddCommMonoid N] [inst_5 : TopologicalSpace N]
  [inst_6 : Module R N] [inst_7 : ContinuousAdd N] [inst_8 : ContinuousConstSMul R N] {f : M →L[R] N}
  {s : ClosedSubmodule R M} {t : ClosedSubmodule R N}, ClosedSubmodule.map f s ≤ t ↔ s ≤ ClosedSubmodule.comap f t
-- Mathlib.Algebra.Group.ULift
ULift.commMonoid.eq_1 : ∀ {α : Type u} [inst : CommMonoid α], ULift.commMonoid = Function.Injective.commMonoid ⇑Equiv.ulift ⋯ ⋯ ⋯ ⋯
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.transpose_reindex : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} (eₘ : m ≃ l) (eₙ : n ≃ o) (M : Matrix m n α),
  ((Matrix.reindex eₘ eₙ) M).transpose = (Matrix.reindex eₙ eₘ) M.transpose
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.Hom.comp_f₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {S₁ S₂ S₃ : CategoryTheory.ShortComplex.SnakeInput C} (f : S₁.Hom S₂) (g : S₂.Hom S₃),
  (f.comp g).f₂ = CategoryTheory.CategoryStruct.comp f.f₂ g.f₂
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
AlgebraicGeometry.Scheme.IdealSheafData.glueDataT'Aux.congr_simp : ∀ {X : AlgebraicGeometry.Scheme} (I : X.IdealSheafData) (U V W U₀ : ↑X.affineOpens) (hU₀ : ↑U ⊓ ↑W ≤ ↑U₀),
  I.glueDataT'Aux U V W U₀ hU₀ = I.glueDataT'Aux U V W U₀ hU₀
-- Mathlib.Tactic.Linter.TextBased
_private.Mathlib.Tactic.Linter.TextBased.0.Mathlib.Linter.TextBased.UnicodeLinter.findBadUnicodeAux.match_1.eq_1 : ∀ (motive : Option Char → Sort u_1) (h_1 : Unit → motive none) (h_2 : (cₙ : Char) → motive (some cₙ)),
  (match none with
    | none => h_1 ()
    | some cₙ => h_2 cₙ) =
    h_1 ()
-- Mathlib.Analysis.Calculus.Deriv.Polynomial
Polynomial.hasFDerivAt_aeval : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {R : Type u_1} [inst_1 : CommSemiring R] [inst_2 : Algebra R 𝕜]
  (q : Polynomial R) (x : 𝕜),
  HasFDerivAt (fun x => (Polynomial.aeval x) q)
    (ContinuousLinearMap.smulRight 1 ((Polynomial.aeval x) (Polynomial.derivative q))) x
-- Mathlib.Data.Sum.Interval
Sum.Ioc_inr_inr : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : LocallyFiniteOrder α]
  [inst_3 : LocallyFiniteOrder β] (b₁ b₂ : β),
  Finset.Ioc (Sum.inr b₁) (Sum.inr b₂) = Finset.map Function.Embedding.inr (Finset.Ioc b₁ b₂)
-- Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Multiset.sum_map_singleton : ∀ {M : Type u_5} (s : Multiset M), (Multiset.map (fun a => {a}) s).sum = s
-- Mathlib.RingTheory.Bialgebra.Convolution
BialgHom.instOneWithConv : {R : Type u_1} →
  {A : Type u_2} →
    {C : Type u_4} →
      [inst : CommSemiring R] →
        [inst_1 : CommSemiring A] →
          [inst_2 : Semiring C] → [inst_3 : Bialgebra R A] → [inst_4 : Bialgebra R C] → One (WithConv (C →ₐc[R] A))
-- Mathlib.Geometry.Manifold.IsManifold.Basic
ModelWithCorners.Boundaryless.mk : ∀ {𝕜 : 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},
  Set.range ↑I = Set.univ → I.Boundaryless
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.comp_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α}
  [inst_1 : TopologicalSpace δ] [inst_2 : TopologicalSpace β] [inst_3 : TopologicalSpace γ] (g : γ → δ) (g' : β → γ)
  (hg : Continuous g) (hg' : Continuous g') (f : α →ₘ[μ] β),
  MeasureTheory.AEEqFun.comp g hg (MeasureTheory.AEEqFun.comp g' hg' f) = MeasureTheory.AEEqFun.comp (g ∘ g') ⋯ f
-- Mathlib.FieldTheory.AbsoluteGaloisGroup
/-- The absolute Galois group of `K`, defined as the Galois group of the field extension `K^al/K`,
where `K^al` is an algebraic closure of `K`.  -/
Field.absoluteGaloisGroup : (K : Type u_1) → [Field K] → Type u_1
-- Mathlib.LinearAlgebra.Finsupp.LinearCombination
Submodule.mem_span_finset : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {s : Finset M}
  {x : M}, x ∈ Submodule.span R ↑s ↔ ∃ f, Function.support f ⊆ ↑s ∧ ∑ a ∈ s, f a • a = x
-- Mathlib.Analysis.Asymptotics.TVS
Asymptotics.isLittleOTVS_iff : ∀ (𝕜 : Type u_1) {α : Type u_2} {E : Type u_3} {F : Type u_4} [inst : ENorm 𝕜] [inst_1 : TopologicalSpace E]
  [inst_2 : TopologicalSpace F] [inst_3 : Zero E] [inst_4 : Zero F] [inst_5 : SMul 𝕜 E] [inst_6 : SMul 𝕜 F]
  (l : Filter α) (f : α → E) (g : α → F),
  f =o[𝕜; l] g ↔
    ∀ U ∈ nhds 0, ∃ V ∈ nhds 0, ∀ (ε : NNReal), ε ≠ 0 → (fun x => egauge 𝕜 U (f x)) ≤ᶠ[l] fun x => ↑ε * egauge 𝕜 V (g x)
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
/-- Eta-expanded form of `UniformCauchySeqOn.neg` -/
UniformCauchySeqOn.fun_neg : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : AddGroup α] [IsUniformAddGroup α] {ι : Type u_3}
  {l : Filter ι} {f : ι → β → α} {s : Set β}, UniformCauchySeqOn f l s → UniformCauchySeqOn (fun i i_1 => -f i i_1) l s
-- Mathlib.LinearAlgebra.Matrix.Hermitian
Matrix.IsHermitian.submatrix : ∀ {α : Type u_1} {m : Type u_3} {n : Type u_4} [inst : Star α] {A : Matrix n n α},
  A.IsHermitian → ∀ (f : m → n), (A.submatrix f f).IsHermitian
-- Init.Data.Iterators.Consumers.Monadic.Loop
Std.IteratorLoop.WithWF.mk.injEq : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} [inst : Std.Iterator α m β] {γ : Type x}
  {PlausibleForInStep : β → γ → ForInStep γ → Prop} {hwf : Std.IteratorLoop.WellFounded α m PlausibleForInStep}
  (it : Std.IterM m β) (acc : γ) (it_1 : Std.IterM m β) (acc_1 : γ),
  ({ it := it, acc := acc } = { it := it_1, acc := acc_1 }) = (it = it_1 ∧ acc = acc_1)
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
SimpleGraph.regularityReduced_anti : ∀ {α : Type u_1} {𝕜 : Type u_2} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [inst_2 : DecidableEq α] {A : Finset α}
  {P : Finpartition A} {G : SimpleGraph α} [inst_3 : DecidableRel G.Adj] {ε δ₁ δ₂ : 𝕜},
  δ₁ ≤ δ₂ → SimpleGraph.regularityReduced P G ε δ₂ ≤ SimpleGraph.regularityReduced P G ε δ₁
-- Mathlib.Order.Fin.Tuple
monotone_vecCons : ∀ {α : Type u_1} [inst : Preorder α] {n : ℕ} {f : Fin (n + 1) → α} {a : α},
  Monotone (Matrix.vecCons a f) ↔ a ≤ f 0 ∧ Monotone f
-- Mathlib.Topology.Order.OrderClosed
Dense.exists_ge : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [ClosedIicTopology α] [NoMaxOrder α] {s : Set α},
  Dense s → ∀ (x : α), ∃ y ∈ s, x ≤ y
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.size_filter_eq_size_iff : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] {f : α → Bool},
  t.WF → ((Std.TreeSet.Raw.filter f t).size = t.size ↔ ∀ (k : α) (h : k ∈ t), f (t.get k h) = true)
-- Mathlib.Order.ConditionallyCompletePartialOrder.Basic
OrderDual.instConditionallyCompletePartialOrder : {α : Type u_1} → [ConditionallyCompletePartialOrder α] → ConditionallyCompletePartialOrder αᵒᵈ
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.Iter.forIn_filterMapWithPostcondition : ∀ {α β β₂ γ : Type w} {n : Type w → Type w'} {o : Type w → Type w''} {Pred EPred : Type w} [inst : Std.Iterator α Id β]
  [inst_1 : Monad n] [LawfulMonad n] [inst_3 : Monad o] [inst_4 : Std.Internal.Do.Assertion Pred]
  [inst_5 : Std.Internal.Do.Assertion EPred] [inst_6 : Std.Internal.Do.WPMonad o Pred EPred] [inst_7 : MonadLiftT n o]
  [LawfulMonadLiftT n o] [Std.Iterators.Finite α Id] [inst_10 : Std.IteratorLoop α Id o] [Std.LawfulIteratorLoop α Id o]
  {it : Std.Iter β} {f : β → Std.Iterators.PostconditionT n (Option β₂)} {init : γ} {g : β₂ → γ → o (ForInStep γ)}
  {P : Pred} {Q : γ → Pred} {eQ : EPred},
  ⦃ P ⦄
      forIn it init fun out acc => do
        let __do_lift ← liftM (f out).run
        match __do_lift with
          | some c => g c acc
          | none => pure (ForInStep.yield acc) ⦃
      Q; eQ ⦄ →
    ⦃ P ⦄ forIn (Std.Iter.filterMapWithPostcondition f it) init g ⦃ Q; eQ ⦄
-- Mathlib.Dynamics.BirkhoffSum.Basic
birkhoffSum_zero : ∀ {α : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] (f : α → α) (g : α → M) (x : α), birkhoffSum f g 0 x = 0
-- Mathlib.Data.Rat.Cast.CharZero
NNRat.cast_eq_zero : ∀ {α : Type u_3} [inst : DivisionSemiring α] [CharZero α] {q : ℚ≥0}, ↑q = 0 ↔ q = 0
-- Mathlib.Algebra.Category.Ring.Basic
/-- Typecheck a `RingHom` as a morphism in `RingCat`.  -/
RingCat.ofHom : {R S : Type u} → [inst : Ring R] → [inst_1 : Ring S] → (R →+* S) → (RingCat.of R ⟶ RingCat.of S)
-- Lean.Parser.Basic
Lean.Parser.symbolNoAntiquot : String → Lean.Parser.Parser
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.SInt
Int8.reduceOfIntLE : Lean.Meta.Simp.DSimproc
-- Mathlib.Algebra.Homology.Embedding.TruncLE
/-- The isomorphism `(K.truncLE e).X i' ≅ K.X i'` when `e.f i = i'`
and `e.BoundaryLE i` does not hold.  -/
HomologicalComplex.truncLEXIso : {ι : 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.IsTruncLE] →
                    [inst_3 : ∀ (i' : ι'), K.HasHomology i'] →
                      [inst_4 : CategoryTheory.Limits.HasZeroObject C] →
                        {i : ι} → {i' : ι'} → e.f i = i' → ¬e.BoundaryLE i → ((K.truncLE e).X i' ≅ K.X i')
-- Mathlib.Algebra.Group.Basic
sub_right_injective : ∀ {G : Type u_3} [inst : AddGroup G] {b : G}, Function.Injective fun a => b - a
-- Mathlib.MeasureTheory.Function.LpSeminorm.Trim
MeasureTheory.memLp_of_memLp_trim : ∀ {α : Type u_1} {ε : Type u_3} {m m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε] (hm : m ≤ m0) {f : α → ε},
  MeasureTheory.MemLp f p (μ.trim hm) → MeasureTheory.MemLp f p μ
-- Init.Data.Iterators.PostconditionMonad
/-- `PostconditionT m α` represents an operation in the monad `m` together with a
intrinsic proof that some postcondition holds for the `α` valued monadic result.
It consists of a predicate `P` about `α` and an element of `m ({ a // P a })` and is a helpful tool
for intrinsic verification, notably termination proofs, in the context of iterators.

`PostconditionT m` is a monad if `m` is. However, note that `PostconditionT m α` is a structure,
so that the compiler will generate inefficient code from recursive functions returning
`PostconditionT m α`. Optimizations for `ReaderT`, `StateT` etc. aren't applicable for structures.

Moreover, `PostconditionT m α` is not a well-behaved monad transformer because `PostconditionT.lift`
neither commutes with `pure` nor with `bind`.
 -/
Std.Iterators.PostconditionT : (Type w → Type w') → Type w → Type (max w w')
-- Mathlib.Topology.EMetricSpace.Defs
/-- Weak pseudo-emetric space instance on subsets of weak pseudo-emetric spaces  -/
instWeakPseudoEMetricSpaceSubtype : {α : Type u_2} →
  {p : α → Prop} → [inst : TopologicalSpace α] → [WeakPseudoEMetricSpace α] → WeakPseudoEMetricSpace (Subtype p)
-- Mathlib.Analysis.RCLike.ContinuousMap
ContinuousMap.realToRCLikeStarAlgHom_apply : ∀ {X : Type u_1} (𝕜 : Type u_2) [inst : TopologicalSpace X] [inst_1 : RCLike 𝕜] (f : C(X, ℝ)),
  (ContinuousMap.realToRCLikeStarAlgHom X 𝕜) f = ContinuousMap.realToRCLike 𝕜 f
-- Mathlib.Topology.Algebra.Algebra.Equiv
ContinuousAlgEquiv.coe_inj : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : TopologicalSpace A] [inst_3 : Semiring B] [inst_4 : TopologicalSpace B] [inst_5 : Algebra R A]
  [inst_6 : Algebra R B] {f g : A ≃A[R] B}, ↑f = ↑g ↔ f = g
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getD_alter_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k : α} {fallback : β k} {f : Option (β k) → Option (β k)},
  (t.alter k f).getD k fallback = (f (t.get? k)).getD fallback
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instAddCommMonoid.eq_1 : ∀ {M : Type u_1} [inst : TopologicalSpace M] [inst_1 : AddCommMonoid M] [inst_2 : ContinuousAdd M],
  SeparationQuotient.instAddCommMonoid = { toAddMonoid := SeparationQuotient.instAddMonoid, add_comm := ⋯ }
-- Mathlib.Geometry.Euclidean.Altitude
Affine.Simplex.height_pos : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n) (i : Fin (n + 1)),
  0 < s.height i
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.eq_loopyOn_iff_loops : ∀ {α : Type u_1} {M : Matroid α} {E : Set α}, M = Matroid.loopyOn E ↔ M.loops = E ∧ M.E = E
-- Init.Data.BitVec.Lemmas
BitVec.smtSDiv.eq_1 : ∀ {n : ℕ} (x y : BitVec n),
  x.smtSDiv y =
    match x.msb, y.msb with
    | false, false => x.smtUDiv y
    | false, true => (x.smtUDiv y.neg).neg
    | true, false => (x.neg.smtUDiv y).neg
    | true, true => x.neg.smtUDiv y.neg
-- Mathlib.Data.Fintype.Card
/-- Given an injective map `f : α → β` such that `β` has cardinality one more
than `α`, there exists a unique element of `β` not in the image of `f`.  -/
Fintype.existsUnique_notMem_image_of_injective_of_card_eq_add_one : ∀ {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst_1 : Fintype β] [inst_2 : DecidableEq β] (f : α → β),
  Function.Injective f → Fintype.card β = Fintype.card α + 1 → ∃! x, x ∉ Finset.image f Finset.univ
-- Mathlib.RingTheory.Localization.NumDen
IsFractionRing.num_mul_den_eq_num_iff_eq : ∀ {A : Type u_1} [inst : CommRing A] [inst_1 : IsDomain A] [inst_2 : UniqueFactorizationMonoid A] {K : Type u_2}
  [inst_3 : Field K] [inst_4 : Algebra A K] [inst_5 : IsFractionRing A K] {x y : K},
  x * (algebraMap A K) ↑(IsFractionRing.den A y) = (algebraMap A K) (IsFractionRing.num A y) ↔ x = y
-- Mathlib.GroupTheory.Exponent
AddMonoid.neZero_exponent_of_finite : ∀ {G : Type u} [inst : AddLeftCancelMonoid G] [Finite G], NeZero (AddMonoid.exponent G)
-- Lean.Elab.Tactic.BuiltinTactic
_private.Lean.Elab.Tactic.BuiltinTactic.0.Lean.Elab.Tactic.evalFirst.loop : Array Lean.Syntax → ℕ → Lean.Elab.Tactic.TacticM Unit
-- Std.Internal.Do.Order.Basic
Lean.Order.meet_le_left : ∀ {α : Type u} [inst : Lean.Order.CompleteLattice α] (x y : α), Lean.Order.PartialOrder.rel (Lean.Order.meet x y) x
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey!_unitOfList_of_contains_eq_false : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α] [inst_4 : Inhabited α] {l : List α}
  {k : α}, l.contains k = false → (Std.HashMap.Raw.unitOfList l).getKey! k = default
-- Init.Grind.Ring.Basic
/-- Addition is commutative.  -/
Lean.Grind.Semiring.add_comm : ∀ {α : Type u} [self : Lean.Grind.Semiring α] (a b : α), a + b = b + a
-- Mathlib.Topology.Order.Basic
exists_Ioc_subset_of_mem_nhds : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] {a : α} {s : Set α},
  s ∈ nhds a → (∃ l, l < a) → ∃ l < a, Set.Ioc l a ⊆ s
-- Mathlib.LinearAlgebra.CliffordAlgebra.Even
CliffordAlgebra.even.lift_ι : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (Q : QuadraticForm R M) {A : Type u_3} [inst_3 : Ring A] [inst_4 : Algebra R A] (f : CliffordAlgebra.EvenHom Q A)
  (m₁ m₂ : M), ((CliffordAlgebra.even.lift Q) f) (((CliffordAlgebra.even.ι Q).bilin m₁) m₂) = (f.bilin m₁) m₂
-- Mathlib.RepresentationTheory.Continuous.Basic
ContIntertwiningMap.toFun_injective : ∀ {R : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Monoid G] [inst_1 : Ring R]
  [inst_2 : AddCommGroup V] [inst_3 : TopologicalSpace V] [inst_4 : IsTopologicalAddGroup V] [inst_5 : Module R V]
  [inst_6 : AddCommGroup W] [inst_7 : TopologicalSpace W] [inst_8 : IsTopologicalAddGroup W] [inst_9 : Module R W]
  {π₁ : ContRepresentation R G V} {π₂ : ContRepresentation R G W},
  Function.Injective fun f => (↑f.toContinuousLinearMap).toFun
-- Mathlib.CategoryTheory.Limits.Fubini
/-- Extract the functor `J ⥤ C` consisting of the cocone points and the maps between them,
from a `DiagramOfCocones`.
 -/
CategoryTheory.Limits.DiagramOfCocones.coconePoints : {J : Type u_1} →
  {K : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} J] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} K] →
        {C : Type u_3} →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} C] →
            {F : CategoryTheory.Functor J (CategoryTheory.Functor K C)} →
              CategoryTheory.Limits.DiagramOfCocones F → CategoryTheory.Functor J C
-- Mathlib.Tactic.Linter.FlexibleLinter
/-- `SyntaxNodeKind`s that are mostly "formatting": mostly they are ignored
because we do not want the linter to spend time on them.
The nodes that they contain will be visited by the linter anyway.
The nodes that *follow* them, though, will *not* be visited by the linter.
 -/
_private.Mathlib.Tactic.Linter.FlexibleLinter.0.Mathlib.Linter.Flexible.stoppers : Std.HashSet Lean.Name
-- Mathlib.Topology.Order.Compact
/-- A closed interval `Set.Icc a b` is a compact set for all `a` and `b`.  -/
CompactIccSpace.isCompact_Icc : ∀ {α : Type u_1} {inst : TopologicalSpace α} {inst_1 : Preorder α} [self : CompactIccSpace α] {a b : α},
  IsCompact (Set.Icc a b)
-- Mathlib.Order.Monotone.Defs
StrictAnti.prodMap : ∀ {α : Type u} {β : Type v} {γ : Type w} {δ : Type u_2} [inst : PartialOrder α] [inst_1 : PartialOrder β]
  [inst_2 : Preorder γ] [inst_3 : Preorder δ] {f : α → γ} {g : β → δ},
  StrictAnti f → StrictAnti g → StrictAnti (Prod.map f g)
-- Mathlib.Order.Irreducible
SupPrime.le_sup : ∀ {α : Type u_2} [inst : SemilatticeSup α] {a b c : α}, SupPrime a → (a ≤ b ⊔ c ↔ a ≤ b ∨ a ≤ c)
-- Mathlib.Analysis.SpecialFunctions.Pow.Continuity
ENNReal.continuous_rpow_const : ∀ {y : ℝ}, Continuous fun a => a ^ y
-- Lean.Data.Lsp.InitShutdown
Lean.Lsp.instFromJsonClientInfo.fromJson : Lean.Json → Except String Lean.Lsp.ClientInfo
-- Mathlib.Order.GaloisConnection.Basic
GaloisConnection.l_iSup : ∀ {α : Type u} {β : Type v} {ι : Sort x} [inst : CompleteLattice α] [inst_1 : CompleteLattice β] {l : α → β}
  {u : β → α}, GaloisConnection l u → ∀ {f : ι → α}, l (iSup f) = ⨆ i, l (f i)
-- Mathlib.Algebra.Module.LinearMap.End
LinearMap.applyₗ'_apply_apply : ∀ {R : Type u_1} (S : Type u_3) {M : Type u_4} {M₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R M₂]
  [inst_6 : Module S M₂] [inst_7 : SMulCommClass R S M₂] (v : M) (f : M →ₗ[R] M₂), ((LinearMap.applyₗ' S) v) f = f v
-- Mathlib.Order.Heyting.Hom
/-- Composition of `BiheytingHom`s as a `BiheytingHom`.  -/
BiheytingHom.comp : {α : Type u_2} →
  {β : Type u_3} →
    {γ : Type u_4} →
      [inst : BiheytingAlgebra α] →
        [inst_1 : BiheytingAlgebra β] →
          [inst_2 : BiheytingAlgebra γ] → BiheytingHom β γ → BiheytingHom α β → BiheytingHom α γ
-- Mathlib.Algebra.Group.Action.Defs
smul_iterate_apply : ∀ {M : Type u_1} {α : Type u_5} [inst : Monoid M] [inst_1 : MulAction M α] (a : M) (n : ℕ) (x : α),
  (fun x => a • x)^[n] x = a ^ n • x
-- Mathlib.Combinatorics.Matroid.Map
/-- `M.restrictSubtype X` is isomorphic to `M ↾ X`.  -/
Matroid.map_val_restrictSubtype_eq : ∀ {α : Type u_1} (M : Matroid α) (X : Set α), (M.restrictSubtype X).map Subtype.val ⋯ = M.restrict X
-- Std.Do.SPred.Notation.Basic
/-- Removes an `spred` layer from a `term` syntax object.  -/
Std.Do.SPred.Notation.unpack : {m : Type → Type} → [Monad m] → [Lean.MonadRef m] → [Lean.MonadQuotation m] → Lean.Term → m Lean.Term
-- Mathlib.MeasureTheory.Measure.MeasureSpace
/-- Some version of continuity of a measure in the empty set using the intersection along a set of
sets.  -/
MeasureTheory.exists_measure_iInter_lt : ∀ {α : Type u_8} {ι : Type u_9} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : SemilatticeSup ι]
  [Countable ι] {f : ι → Set α},
  (∀ (i : ι), MeasureTheory.NullMeasurableSet (f i) μ) →
    ∀ {ε : ENNReal}, 0 < ε → (∃ i, μ (f i) ≠ ⊤) → ⋂ n, f n = ∅ → ∃ m, μ (⋂ n, ⋂ (_ : n ≤ m), f n) < ε
-- Mathlib.Algebra.Order.Monoid.Unbundled.Pow
pow_right_monotone : ∀ {M : Type u_3} [inst : Monoid M] [inst_1 : Preorder M] [MulLeftMono M] {a : M}, 1 ≤ a → Monotone fun n => a ^ n
-- Mathlib.Order.ConditionallyCompleteLattice.Defs
/-- Every nonempty subset which is bounded below has a greatest lower bound.  -/
ConditionallyCompleteLattice.isGLB_csInf : ∀ {α : Type u_5} [self : ConditionallyCompleteLattice α] (s : Set α), s.Nonempty → BddBelow s → IsGLB s (sInf s)
-- Mathlib.SetTheory.Ordinal.Basic
/-- `lift.{max u v, u}` equals `lift.{v, u}`.

Unfortunately, the simp lemma doesn't seem to work.  -/
Ordinal.lift_umax : Ordinal.lift.{max u v, u} = Ordinal.lift.{v, u}
-- Mathlib.CategoryTheory.Abelian.Basic
CategoryTheory.Abelian.toIsNormalMonoCategory : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.Abelian C],
  CategoryTheory.IsNormalMonoCategory C