mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.OreLocalization.Basic
AddOreLocalization.instVAddCommClass : ∀ {R : Type u_1} {R' : Type u_2} {M : Type u_3} {X : Type u_4} [inst : AddMonoid M] {S : AddSubmonoid M}
  [inst_1 : AddOreLocalization.AddOreSet S] [inst_2 : AddAction M X] [inst_3 : VAdd R X] [inst_4 : VAdd R M]
  [inst_5 : VAddAssocClass R M M] [inst_6 : VAddAssocClass R M X] [inst_7 : VAdd R' X] [inst_8 : VAdd R' M]
  [inst_9 : VAddAssocClass R' M M] [inst_10 : VAddAssocClass R' M X] [VAddCommClass R R' M],
  VAddCommClass R R' (AddOreLocalization S X)
-- Mathlib.CategoryTheory.Sites.Coherent.SheafComparison
/-- The equivalence from regular sheaves on `C` to regular sheaves on `D`, given a fully faithful
functor `F : C ⥤ D` to a preregular category, which preserves and reflects effective
epimorphisms and satisfies `F.EffectivelyEnough`.
 -/
CategoryTheory.regularTopology.equivalence : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C D) →
          [inst_2 : F.PreservesEffectiveEpis] →
            [inst_3 : F.ReflectsEffectiveEpis] →
              [inst_4 : F.Full] →
                [inst_5 : F.Faithful] →
                  [inst_6 : CategoryTheory.Preregular D] →
                    [inst_7 : F.EffectivelyEnough] →
                      (A : Type u₃) →
                        [inst_8 : CategoryTheory.Category.{v₃, u₃} A] →
                          [∀ (X : Dᵒᵖ),
                                CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.StructuredArrow X F.op) A] →
                            CategoryTheory.Sheaf (CategoryTheory.regularTopology C) A ≌
                              CategoryTheory.Sheaf (CategoryTheory.regularTopology D) A
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
IsFreeGroup.toFreeGroup_apply : ∀ (G : Type u_1) [inst : Group G] [inst_1 : IsFreeGroup G] (a : G),
  (IsFreeGroup.toFreeGroup G) a = (IsFreeGroup.mulEquiv G).symm a
-- Mathlib.Data.Finset.Lattice.Fold
Finset.inf'_union : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeInf α] [inst_1 : DecidableEq β] {s₁ s₂ : Finset β} (h₁ : s₁.Nonempty)
  (h₂ : s₂.Nonempty) (f : β → α), (s₁ ∪ s₂).inf' ⋯ f = s₁.inf' h₁ f ⊓ s₂.inf' h₂ f
-- Mathlib.Algebra.Category.Grp.FilteredColimits
AddCommGrpCat.FilteredColimits.colimitCoconeIsColimit.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] [inst_1 : CategoryTheory.IsFiltered J]
  (F : CategoryTheory.Functor J AddCommGrpCat),
  AddCommGrpCat.FilteredColimits.colimitCoconeIsColimit F =
    CategoryTheory.Limits.isColimitOfReflects (CategoryTheory.forget₂ AddCommGrpCat AddGrpCat)
      (AddGrpCat.FilteredColimits.colimitCoconeIsColimit (F.comp (CategoryTheory.forget₂ AddCommGrpCat AddGrpCat)))
-- Mathlib.Order.CompleteLattice.Basic
iInf_pair : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {f : β → α} {a b : β}, ⨅ x ∈ {a, b}, f x = f a ⊓ f b
-- Mathlib.Algebra.Ring.Action.Subobjects
instMulSemiringActionSubtypeMem : {M : Type u_1} →
  {R : Type u_3} →
    [inst : Monoid M] →
      [inst_1 : Semiring R] →
        [MulSemiringAction M R] →
          {S : Type u_4} → [inst_3 : SetLike S M] → (s : S) → [inst_4 : SubmonoidClass S M] → MulSemiringAction (↥s) R
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
CStarAlgebra.inv_le_one : ∀ {A : Type u_1} [inst : CStarAlgebra A] [inst_1 : PartialOrder A] [StarOrderedRing A] {a : Aˣ}, 1 ≤ a → ↑a⁻¹ ≤ 1
-- Init.Grind.Util
/-- `Classical.em` variant where disjuncts are marked with `alreadyNorm` gadget.
See comment at `alreadyNorm`
 -/
Lean.Grind.em : ∀ (p : Prop), Lean.Grind.alreadyNorm p ∨ Lean.Grind.alreadyNorm ¬p
-- Mathlib.Analysis.InnerProductSpace.Calculus
DifferentiableAt.norm_sq : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [InnerProductSpace 𝕜 E]
  [inst : NormedSpace ℝ E] {G : Type u_4} [inst_2 : NormedAddCommGroup G] [inst_3 : NormedSpace ℝ G] {f : G → E}
  {x : G}, DifferentiableAt ℝ f x → DifferentiableAt ℝ (fun y => ‖f y‖ ^ 2) x
-- Mathlib.GroupTheory.GroupAction.Transitive
MulAction.IsPretransitive.of_surjective_map : ∀ {M : Type u_3} {N : Type u_4} {α : Type u_5} {β : Type u_6} [inst : Monoid M] [inst_1 : Monoid N]
  [inst_2 : MulAction M α] [inst_3 : MulAction N β] {φ : M → N} {f : α →ₑ[φ] β},
  Function.Surjective ⇑f → MulAction.IsPretransitive M α → MulAction.IsPretransitive N β
-- Init.Data.Vector.Lemmas
Vector.map_eq_iff : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} {f : α → β} {as : Vector α n} {bs : Vector β n},
  Vector.map f as = bs ↔ ∀ (i : ℕ) (h : i < n), bs[i] = f as[i]
-- Std.Data.ExtHashSet.Basic
Std.ExtHashSet.mk : {α : Type u} → [inst : BEq α] → [inst_1 : Hashable α] → Std.ExtHashMap α Unit → Std.ExtHashSet α
-- Mathlib.Order.SuccPred.Basic
SuccOrder.ofLinearWellFoundedLT.eq_1 : ∀ (α : Type u_1) [inst : LinearOrder α] [inst_1 : WellFoundedLT α],
  SuccOrder.ofLinearWellFoundedLT α =
    SuccOrder.ofCore (fun a => if h : (Set.Ioi a).Nonempty then ⋯.min (Set.Ioi a) h else a) ⋯ ⋯
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.root_or_root_of_root_mul : ∀ {R : Type u} {a : R} [inst : CommSemiring R] {p q : Polynomial R} [NoZeroDivisors R],
  (p * q).IsRoot a → p.IsRoot a ∨ q.IsRoot a
-- Mathlib.Data.List.Cycle
Cycle.reverse_reverse : ∀ {α : Type u_1} (s : Cycle α), s.reverse.reverse = s
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
/-- The function `Complex.cos` is complex analytic.  -/
Complex.analyticWithinAt_cos : ∀ {x : ℂ} {s : Set ℂ}, AnalyticWithinAt ℂ Complex.cos s x
-- Init.Data.Vector.Lemmas
Vector.any_mk : ∀ {α : Type u_1} {n : ℕ} {p : α → Bool} {xs : Array α} (h : xs.size = n), (Vector.mk xs h).any p = xs.any p
-- Init.Data.Range.Polymorphic.SInt
ISize.instRxoIsAlwaysFinite : Std.Rxo.IsAlwaysFinite ISize
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.Const.getₘ_eq_getValue : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : PartialEquivBEq α]
  [inst_3 : LawfulHashable α] {m : Std.DHashMap.Internal.Raw₀ α fun x => β} (hm : Std.DHashMap.Internal.Raw.WFImp ↑m)
  {a : α} {h : m.containsₘ a = true},
  Std.DHashMap.Internal.Raw₀.Const.getₘ m a h =
    Std.Internal.List.getValue a (Std.DHashMap.Internal.toListModel (↑m).buckets) ⋯
-- Mathlib.FieldTheory.PurelyInseparable.PerfectClosure
/-- For an extension `E / F` of exponential characteristic `q` and a separable element `a : E`, the
minimal polynomial of `a ^ q` equals the minimal polynomial of `a` mapped via `(⬝ ^ q)`.  -/
minpoly.frobenius_of_isSeparable : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (q : ℕ) [hF : ExpChar F q]
  [inst_3 : ExpChar E q] {a : E},
  IsSeparable F a → minpoly F ((frobenius E q) a) = Polynomial.map (frobenius F q) (minpoly F a)
-- Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset
/-- **Alias** of `CategoryTheory.CardinalDirectedPoset.propSetWithTop_pair`. -/
CategoryTheory.CardinalFilteredPoset.propSetWithTop_pair : ∀ {κ : Cardinal.{u}} [inst : Fact κ.IsRegular] {J : CategoryTheory.CardinalDirectedPoset κ} (κ' : Cardinal.{u})
  [inst_1 : Fact κ'.IsRegular] (j : ↑J.obj), J.PropSetWithTop κ' {↑j, ⊤}
-- Mathlib.Order.Sublattice
/-- The product of sublattices is isomorphic to their product as lattices.  -/
Sublattice.prodEquiv : {α : Type u_2} →
  {β : Type u_3} →
    [inst : Lattice α] → [inst_1 : Lattice β] → (L : Sublattice α) → (M : Sublattice β) → ↥(L.prod M) ≃o ↥L × ↥M
-- Mathlib.FieldTheory.Relrank
IntermediateField.relrank_comap_comap_eq_relrank_of_surjective : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (A B : IntermediateField F E)
  {L : Type v} [inst_3 : Field L] [inst_4 : Algebra F L] (f : L →ₐ[F] E),
  Function.Surjective ⇑f → (IntermediateField.comap f A).relrank (IntermediateField.comap f B) = A.relrank B
-- Mathlib.Data.Multiset.Range
/-- `range n` is the multiset lifted from the list `range n`,
that is, the set `{0, 1, ..., n-1}`.  -/
Multiset.range : ℕ → Multiset ℕ
-- Std.Data.HashSet.Raw
/-- Folds the given function over the elements of the hash set in some order.  -/
Std.HashSet.Raw.fold : {α : Type u} → {β : Type v} → (β → α → β) → β → Std.HashSet.Raw α → β
-- Std.Sat.CNF.Basic
/-- A clause in a CNF.

The literal `(i, b)` is satisfied if the assignment to `i` agrees with `b`.
 -/
Std.Sat.CNF.Clause : Type u → Type u
-- Init.Grind.Ordered.Linarith
_private.Init.Grind.Ordered.Linarith.0.Lean.Grind.Linarith.Expr.denote.match_1.eq_4 : ∀ (motive : Lean.Grind.Linarith.Expr → Sort u_1) (a b : Lean.Grind.Linarith.Expr)
  (h_1 : Unit → motive Lean.Grind.Linarith.Expr.zero)
  (h_2 : (v : Lean.Grind.Linarith.Var) → motive (Lean.Grind.Linarith.Expr.var v))
  (h_3 : (a b : Lean.Grind.Linarith.Expr) → motive (a.add b))
  (h_4 : (a b : Lean.Grind.Linarith.Expr) → motive (a.sub b))
  (h_5 : (k : ℕ) → (a : Lean.Grind.Linarith.Expr) → motive (Lean.Grind.Linarith.Expr.natMul k a))
  (h_6 : (k : ℤ) → (a : Lean.Grind.Linarith.Expr) → motive (Lean.Grind.Linarith.Expr.intMul k a))
  (h_7 : (a : Lean.Grind.Linarith.Expr) → motive a.neg),
  (match a.sub b with
    | Lean.Grind.Linarith.Expr.zero => h_1 ()
    | Lean.Grind.Linarith.Expr.var v => h_2 v
    | a.add b => h_3 a b
    | a.sub b => h_4 a b
    | Lean.Grind.Linarith.Expr.natMul k a => h_5 k a
    | Lean.Grind.Linarith.Expr.intMul k a => h_6 k a
    | a.neg => h_7 a) =
    h_4 a b
-- Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
/-- If `‖f x‖ₑ ≤ c * ‖g x‖ₑ`, then `eLpNorm f p μ ≤ c * eLpNorm g p μ`.

This version assumes `c` is finite, but requires no measurability hypothesis on `g`.  -/
MeasureTheory.eLpNorm_le_mul_eLpNorm_of_ae_le_mul' : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ε : Type u_5} {ε' : Type u_6}
  [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε] [inst_2 : TopologicalSpace ε'] [inst_3 : ContinuousENorm ε']
  {f : α → ε} {g : α → ε'} {c : NNReal},
  (∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ↑c * ‖g x‖ₑ) →
    ∀ (p : ENNReal), MeasureTheory.eLpNorm f p μ ≤ ↑c * MeasureTheory.eLpNorm g p μ
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
/-- Given a pullback square assembled from a commuting square on the top and
a pullback square on the bottom, the top square is a pullback square.

The objects in the statement fit into the following diagram:
```
X₁₁ - h₁₁ -> X₁₂
|            |
v₁₁          v₁₂
↓            ↓
X₂₁ - h₂₁ -> X₂₂
|            |
v₂₁          v₂₂
↓            ↓
X₃₁ - h₃₁ -> X₃₂
```
 -/
CategoryTheory.IsPullback.of_bot : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X₁₁ X₁₂ X₂₁ X₂₂ X₃₁ X₃₂ : C} {h₁₁ : X₁₁ ⟶ X₁₂}
  {h₂₁ : X₂₁ ⟶ X₂₂} {h₃₁ : X₃₁ ⟶ X₃₂} {v₁₁ : X₁₁ ⟶ X₂₁} {v₁₂ : X₁₂ ⟶ X₂₂} {v₂₁ : X₂₁ ⟶ X₃₁} {v₂₂ : X₂₂ ⟶ X₃₂},
  CategoryTheory.IsPullback h₁₁ (CategoryTheory.CategoryStruct.comp v₁₁ v₂₁)
      (CategoryTheory.CategoryStruct.comp v₁₂ v₂₂) h₃₁ →
    CategoryTheory.CategoryStruct.comp h₁₁ v₁₂ = CategoryTheory.CategoryStruct.comp v₁₁ h₂₁ →
      CategoryTheory.IsPullback h₂₁ v₂₁ v₂₂ h₃₁ → CategoryTheory.IsPullback h₁₁ v₁₁ v₁₂ h₂₁
-- Mathlib.Algebra.Group.End
AddAut.add_def : ∀ (M : Type u_2) [inst : Add M] (e₁ e₂ : AddAut M), e₁ + e₂ = AddEquiv.trans e₂ e₁
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.diff!_right : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ m₃ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  m₁.WF → m₂.WF → m₃.WF → m₂.Equiv m₃ → (m₁.diff! m₂).Equiv (m₁.diff! m₃)
-- Init.System.IOError
IO.Error.noSuchThing.injEq : ∀ (filename : Option String) (osCode : UInt32) (details : String) (filename_1 : Option String) (osCode_1 : UInt32)
  (details_1 : String),
  (IO.Error.noSuchThing filename osCode details = IO.Error.noSuchThing filename_1 osCode_1 details_1) =
    (filename = filename_1 ∧ osCode = osCode_1 ∧ details = details_1)
-- Init.Data.List.Lex
_private.Init.Data.List.Lex.0.List.lex.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → List α → Sort u_2) (head : α) (tail : List α)
  (h_1 : (head : α) → (tail : List α) → motive [] (head :: tail)) (h_2 : (x : List α) → motive x [])
  (h_3 : (a : α) → (as : List α) → (b : α) → (bs : List α) → motive (a :: as) (b :: bs)),
  (match [], head :: tail with
    | [], head :: tail => h_1 head tail
    | x, [] => h_2 x
    | a :: as, b :: bs => h_3 a as b bs) =
    h_1 head tail
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
WeierstrassCurve.Affine.CoordinateRing.mk_ψ : ∀ {R : Type r} [inst : CommRing R] (W : WeierstrassCurve R) (n : ℤ),
  (WeierstrassCurve.Affine.CoordinateRing.mk W) (W.ψ n) = (WeierstrassCurve.Affine.CoordinateRing.mk W) (W.Ψ n)
-- Mathlib.Tactic.Recall
/-- The `recall?` command looks up a previous definition and suggests the correct
`recall` statement for it.
```
recall? Nat.add_comm
-- Try this: recall Nat.add_comm (n m : Nat) : n + m = m + n
```
 -/
Mathlib.Tactic.Recall.recall? : Lean.ParserDescr
-- Mathlib.RingTheory.Perfection
PreTilt.coeff_nat_find_add_ne_zero : ∀ {O : Type u₂} [inst : CommRing O] {p : ℕ} [inst_1 : Fact (Nat.Prime p)] [inst_2 : Fact ¬IsUnit ↑p] {f : PreTilt O p}
  {h : ∃ n, (PreTilt.coeff n) f ≠ 0} (k : ℕ), (PreTilt.coeff (Nat.find h + k)) f ≠ 0
-- Mathlib.Tactic.FieldSimp.Lemmas
Mathlib.Tactic.FieldSimp.NF.div_eq_eval : ∀ {M : Type u_1} [inst : GroupWithZero M] {l₁ l₂ l : Mathlib.Tactic.FieldSimp.NF M} {x₁ x₂ : M},
  x₁ = l₁.eval → x₂ = l₂.eval → l₁.eval / l₂.eval = l.eval → x₁ / x₂ = l.eval
-- Mathlib.Geometry.RingedSpace.SheafedSpace
AlgebraicGeometry.SheafedSpace.mono_of_base_injective_of_stalk_epi : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type v}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [instCC : CategoryTheory.ConcreteCategory C FC]
  [inst_2 : CategoryTheory.Limits.HasColimits C] [CategoryTheory.Limits.HasLimits C]
  [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget C)]
  [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)]
  [(CategoryTheory.forget C).ReflectsIsomorphisms] {X Y : AlgebraicGeometry.SheafedSpace C} (f : X ⟶ Y),
  Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom f.hom.base) →
    (∀ (x : ↑↑X.toPresheafedSpace), CategoryTheory.Epi (AlgebraicGeometry.PresheafedSpace.Hom.stalkMap f.hom x)) →
      CategoryTheory.Mono f
-- Mathlib.Probability.Independence.Basic
/-- If `f` is a family of mutually independent random variables (`iIndepFun m f μ`) and `S, T` are
two disjoint finite index sets, then the tuple formed by `f i` for `i ∈ S` is independent of the
tuple `(f i)_i` for `i ∈ T`.  -/
ProbabilityTheory.iIndepFun.indepFun_finset₀ : ∀ {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {β : ι → Type u_10}
  {m : (i : ι) → MeasurableSpace (β i)} {f : (i : ι) → Ω → β i} (S T : Finset ι),
  Disjoint S T →
    ProbabilityTheory.iIndepFun f μ →
      (∀ (i : ι), AEMeasurable (f i) μ) → ProbabilityTheory.IndepFun (fun a i => f (↑i) a) (fun a i => f (↑i) a) μ
-- Mathlib.Data.Erased
Erased.nonempty_iff : ∀ {α : Sort u_1}, Nonempty (Erased α) ↔ Nonempty α
-- Mathlib.Analysis.InnerProductSpace.LinearPMap
LinearPMap.adjoint_graph_eq_graph_adjoint : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F] {T : E →ₗ.[𝕜] F}
  [inst_5 : CompleteSpace E], Dense ↑T.domain → T.adjoint.graph = T.graph.adjoint
-- Mathlib.Geometry.Convex.Cone.Basic
ConvexCone.IsReproducing.eq_1 : ∀ {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] (C : ConvexCone R M), C.IsReproducing = (↑C - ↑C = Set.univ)
-- Init.Data.Array.Count
Array.countP_congr : ∀ {α : Type u_1} {p q : α → Bool} {xs : Array α},
  (∀ x ∈ xs, p x = true ↔ q x = true) → Array.countP p xs = Array.countP q xs
-- Mathlib.NumberTheory.Chebyshev
Chebyshev.theta_pos : ∀ {x : ℝ}, 2 ≤ x → 0 < Chebyshev.theta x
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoMod_eq_iff : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) {a b c : α}, toIcoMod hp a b = c ↔ c ∈ Set.Ico a (a + p) ∧ ∃ z, b = c + z • p
-- Mathlib.Analysis.Normed.Unbundled.RingSeminorm
RingSeminorm.instInhabited : {R : Type u_1} → [inst : NonUnitalRing R] → Inhabited (RingSeminorm R)
-- Init.Classical
/-- **Diaconescu's theorem**: excluded middle from choice, Function extensionality and propositional extensionality.  -/
Classical.em : ∀ (p : Prop), p ∨ ¬p
-- Init.Data.Int.Order
Int.sub_right_le_iff_le_add : ∀ {a b c : ℤ}, a - c ≤ b ↔ a ≤ b + c
-- Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
SpectrumRestricts.subset_preimage : ∀ {R : Type u_3} {S : Type u_4} {A : Type u_5} [inst : Semifield R] [inst_1 : Semifield S] [inst_2 : Ring A]
  [inst_3 : Algebra R S] [inst_4 : Algebra R A] [inst_5 : Algebra S A] {a : A} {f : S → R} [IsScalarTower R S A],
  SpectrumRestricts a f → spectrum S a ⊆ f ⁻¹' spectrum R a
-- Mathlib.Algebra.Module.Equiv.Defs
LinearEquiv.eq_toLinearMap_symm_comp : ∀ {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M₁ : Type u_8} {M₂ : Type u_9} {M₃ : Type u_10} [inst : Semiring R₁]
  [inst_1 : Semiring R₂] [inst_2 : Semiring R₃] [inst_3 : AddCommMonoid M₁] [inst_4 : AddCommMonoid M₂]
  [inst_5 : AddCommMonoid M₃] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃}
  {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} {σ₃₁ : R₃ →+* R₁} {σ₃₂ : R₃ →+* R₂} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁}
  {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} [inst_6 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁] {e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂}
  [inst_7 : RingHomCompTriple σ₃₁ σ₁₂ σ₃₂] (f : M₃ →ₛₗ[σ₃₁] M₁) (g : M₃ →ₛₗ[σ₃₂] M₂),
  f = ↑e₁₂.symm ∘ₛₗ g ↔ ↑e₁₂ ∘ₛₗ f = g
-- Mathlib.Order.Monotone.Monovary
Antitone.monovary : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β}
  [inst_2 : LinearOrder ι], Antitone f → Antitone g → Monovary f g
-- Mathlib.Algebra.Group.Subsemigroup.Operations
MulHom.srange.eq_1 : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] (f : M →ₙ* N),
  f.srange = (Subsemigroup.map f ⊤).copy (Set.range ⇑f) ⋯
-- Init.Data.BitVec.Lemmas
/-- Definition of bitvector addition as a nat.
 -/
BitVec.toNat_add : ∀ {w : ℕ} (x y : BitVec w), (x + y).toNat = (x.toNat + y.toNat) % 2 ^ w
-- Lean.Util.NumApps
Lean.Expr.NumApps.State.visited : Lean.Expr.NumApps.State → Lean.PtrSet Lean.Expr
-- Mathlib.Data.Finset.Insert
Finset.eq_of_mem_insert_of_notMem : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α} {a b : α}, b ∈ insert a s → b ∉ s → b = a
-- Mathlib.Algebra.MonoidAlgebra.Defs
/-- Replace the `m`-th coefficient of an element `x` of the monoid algebra by a given value `r : R`.
If `r = 0`, this is equal to `x.erase m`.  -/
MonoidAlgebra.update : {R : Type u_1} → {M : Type u_4} → [inst : Semiring R] → M → R → MonoidAlgebra R M → MonoidAlgebra R M
-- Mathlib.Algebra.Category.AlgCat.Basic
AlgCat.Hom.ext_iff : ∀ {R : Type u} {inst : CommRing R} {A B : AlgCat R} {x y : A.Hom B}, x = y ↔ x.hom' = y.hom'
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
/-- Partial assignment being constructed by cutsat.  -/
Lean.Meta.Grind.Arith.Cutsat.State.assignment : Lean.Meta.Grind.Arith.Cutsat.State → Lean.PArray ℚ
-- Mathlib.Algebra.Group.NatPowAssoc
/-- Exponent zero is one.  -/
NatPowAssoc.npow_zero : ∀ {M : Type u_2} {inst : MulOneClass M} {inst_1 : Pow M ℕ} [self : NatPowAssoc M] (x : M), x ^ 0 = 1
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.IsImage.e_isoExt_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y}
  {F F' : CategoryTheory.Limits.MonoFactorisation f} (hF : CategoryTheory.Limits.IsImage F)
  (hF' : CategoryTheory.Limits.IsImage F'), CategoryTheory.CategoryStruct.comp F.e (hF.isoExt hF').hom = F'.e
-- Mathlib.AlgebraicTopology.MooreComplex
/-- The normalized Moore complex functor, on morphisms.
 -/
AlgebraicTopology.NormalizedMooreComplex.map : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {X Y : CategoryTheory.SimplicialObject C} →
        (X ⟶ Y) → (AlgebraicTopology.NormalizedMooreComplex.obj X ⟶ AlgebraicTopology.NormalizedMooreComplex.obj Y)
-- Aesop.Tree.Data
Aesop.GoalId.zero : Aesop.GoalId
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
AddEquiv.coe_withTopCongr : ∀ {α : Type u} {β : Type v} [inst : Add α] [inst_1 : Add β] (e : α ≃+ β), ⇑e.withTopCongr = WithTop.map ⇑e
-- Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory
/-- If `A` and `B` are triangulated subcategories of a (pre)triangulated
category `C` (with `B` closed under isomorphisms), we say that `A` is
right `B`-localizing if any morphism `X ⟶ Y` with `X` in `B` and
`Y` in `A` factors through an object that is in `A` and `B`.
Note that the definition does not use the (pre)triangulated structure:
see `isVerdierRightLocalizing_iff` for a characterization which
relies on it.  -/
CategoryTheory.ObjectProperty.IsVerdierRightLocalizing : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    CategoryTheory.ObjectProperty C → CategoryTheory.ObjectProperty C → Prop
-- Mathlib.Order.Hom.Set
OrderIso.unique_of_wellFoundedLT : {α : Type u_1} → [inst : LinearOrder α] → [WellFoundedLT α] → Unique (α ≃o α)
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.MkTableKey.normLevel : Lean.Level → Lean.Meta.SynthInstance.MkTableKey.M Lean.Level
-- Init.Notation
/-- `a ^ b` computes `a` to the power of `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `^` in identifiers is `pow`. -/
«term_^_» : Lean.TrailingParserDescr
-- Mathlib.RingTheory.Valuation.Basic
/-- If `v` is an additive valuation on a division ring then `v(x) = ⊤` iff `x = 0`.  -/
AddValuation.top_iff : ∀ {K : Type u_1} [inst : DivisionRing K] {Γ₀ : Type u_4} [inst_1 : LinearOrderedAddCommMonoidWithTop Γ₀] [Nontrivial Γ₀]
  (v : AddValuation K Γ₀) {x : K}, v x = ⊤ ↔ x = 0
-- Mathlib.Combinatorics.Configuration
Configuration.Dual.Nondegenerate : ∀ (P : Type u_1) (L : Type u_2) [inst : Membership P L] [Configuration.Nondegenerate P L],
  Configuration.Nondegenerate (Configuration.Dual L) (Configuration.Dual P)
-- Lean.Meta.ExprLens
/-- Get the raw subexpression without performing any instantiation.  -/
_private.Lean.Meta.ExprLens.0.Lean.Core.viewCoordRaw : {M : Type → Type} → [Monad M] → [Lean.MonadError M] → Lean.Expr → ℕ → M Lean.Expr
-- Mathlib.Algebra.Order.Ring.WithTop
WithTop.mul_lt_top : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : MulZeroClass α] [inst_2 : LT α] {a b : WithTop α},
  a < ⊤ → b < ⊤ → a * b < ⊤
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.instBEqCtorInfo : BEq Lean.Compiler.LCNF.CtorInfo
-- Lean.Meta.Constructions.SparseCasesOn
_private.Lean.Meta.Constructions.SparseCasesOn.0.Lean.Meta.SparseCasesOnKey.mk.inj : ∀ {indName : Lean.Name} {ctors : Array Lean.Name} {isPrivate : Bool} {indName_1 : Lean.Name} {ctors_1 : Array Lean.Name}
  {isPrivate_1 : Bool},
  { indName := indName, ctors := ctors, isPrivate := isPrivate } =
      { indName := indName_1, ctors := ctors_1, isPrivate := isPrivate_1 } →
    indName = indName_1 ∧ ctors = ctors_1 ∧ isPrivate = isPrivate_1
-- Mathlib.Data.Set.Basic
Set.ssubset_univ_iff : ∀ {α : Type u} {s : Set α}, s ⊂ Set.univ ↔ s ≠ Set.univ
-- Mathlib.Analysis.Meromorphic.Basic
/-- Eta-expanded form of `MeromorphicAt.pow` -/
MeromorphicAt.fun_pow : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {x : 𝕜} {f : 𝕜 → 𝕜'}, MeromorphicAt f x → ∀ (n : ℕ), MeromorphicAt (fun i => f i ^ n) x
-- Init.Control.Basic
MonadControlT.mk : {m : Type u → Type v} →
  {n : Type u → Type w} →
    (stM : Type u → Type u) →
      ({α : Type u} → (({β : Type u} → n β → m (stM β)) → m α) → n α) → ({α : Type u} → stM α → n α) → MonadControlT m n
-- Lean.DocString.Extension
Lean.ModuleDoc.declarationRange : Lean.ModuleDoc → Lean.DeclarationRange
-- Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Finset.prod_ite_of_true : ∀ {ι : Type u_1} {M : Type u_3} {s : Finset ι} [inst : CommMonoid M] {p : ι → Prop} [inst_1 : DecidablePred p],
  (∀ x ∈ s, p x) → ∀ (f g : ι → M), (∏ x ∈ s, if p x then f x else g x) = ∏ x ∈ s, f x