mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.DirectSum.Ring
DirectSum.mulHom_apply : ∀ {ι : Type u_1} [inst : DecidableEq ι] {A : ι → Type u_2} [inst_1 : Add ι] [inst_2 : (i : ι) → AddCommMonoid (A i)]
  [inst_3 : DirectSum.GNonUnitalNonAssocSemiring A] (a b : DirectSum ι fun i => A i), ((DirectSum.mulHom A) a) b = a * b
-- Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Asymptotics.isBigO_atTop_natCast_rpow_of_tendsto_div_rpow : ∀ {𝕜 : Type u_2} [inst : RCLike 𝕜] {g : ℕ → 𝕜} {a : 𝕜} {r : ℝ},
  Filter.Tendsto (fun n => g n / ↑(↑n ^ r)) Filter.atTop (nhds a) → g =O[Filter.atTop] fun n => ↑n ^ r
-- Mathlib.CategoryTheory.Triangulated.Triangulated
CategoryTheory.Triangulated.Octahedron.mk : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
        [inst_3 : CategoryTheory.HasShift C ℤ] →
          [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
            [inst_5 : CategoryTheory.Pretriangulated C] →
              {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} →
                {u₁₂ : X₁ ⟶ X₂} →
                  {u₂₃ : X₂ ⟶ X₃} →
                    {u₁₃ : X₁ ⟶ X₃} →
                      {comm : CategoryTheory.CategoryStruct.comp u₁₂ u₂₃ = u₁₃} →
                        {v₁₂ : X₂ ⟶ Z₁₂} →
                          {w₁₂ : Z₁₂ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁} →
                            {h₁₂ :
                                CategoryTheory.Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈
                                  CategoryTheory.Pretriangulated.distinguishedTriangles} →
                              {v₂₃ : X₃ ⟶ Z₂₃} →
                                {w₂₃ : Z₂₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₂} →
                                  {h₂₃ :
                                      CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈
                                        CategoryTheory.Pretriangulated.distinguishedTriangles} →
                                    {v₁₃ : X₃ ⟶ Z₁₃} →
                                      {w₁₃ : Z₁₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁} →
                                        {h₁₃ :
                                            CategoryTheory.Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈
                                              CategoryTheory.Pretriangulated.distinguishedTriangles} →
                                          (m₁ : Z₁₂ ⟶ Z₁₃) →
                                            (m₃ : Z₁₃ ⟶ Z₂₃) →
                                              CategoryTheory.CategoryStruct.comp v₁₂ m₁ =
                                                  CategoryTheory.CategoryStruct.comp u₂₃ v₁₃ →
                                                CategoryTheory.CategoryStruct.comp m₁ w₁₃ = w₁₂ →
                                                  CategoryTheory.CategoryStruct.comp v₁₃ m₃ = v₂₃ →
                                                    CategoryTheory.CategoryStruct.comp w₁₃
                                                          ((CategoryTheory.shiftFunctor C 1).map u₁₂) =
                                                        CategoryTheory.CategoryStruct.comp m₃ w₂₃ →
                                                      CategoryTheory.Pretriangulated.Triangle.mk m₁ m₃
                                                            (CategoryTheory.CategoryStruct.comp w₂₃
                                                              ((CategoryTheory.shiftFunctor C 1).map v₁₂)) ∈
                                                          CategoryTheory.Pretriangulated.distinguishedTriangles →
                                                        CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃
-- Mathlib.Tactic.Order.Preprocessing
/-- Replaces facts of the form `x = ⊤` with `y ≤ x` for all `y`, and similarly for `x = ⊥`.  -/
Mathlib.Tactic.Order.replaceBotTop : Array Mathlib.Tactic.Order.AtomicFact → Mathlib.Tactic.AtomM (Array Mathlib.Tactic.Order.AtomicFact)
-- Mathlib.LinearAlgebra.PerfectPairing.Restrict
_private.Mathlib.LinearAlgebra.PerfectPairing.Restrict.0.LinearMap.restrictScalars_injective_aux : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] (p : M →ₗ[R] N →ₗ[R] R) [p.IsPerfPair] {S : Type u_4} {M' : Type u_5}
  {N' : Type u_6} [inst_6 : CommRing S] [inst_7 : IsDomain S] [inst_8 : Algebra S R] [inst_9 : Module S M]
  [inst_10 : Module S N] [inst_11 : IsScalarTower S R M] [inst_12 : IsScalarTower S R N]
  [inst_13 : Module.IsTorsionFree S R] [inst_14 : Nontrivial R] [inst_15 : AddCommGroup M'] [inst_16 : Module S M']
  [inst_17 : AddCommGroup N'] [inst_18 : Module S N'] (i : M' →ₗ[S] M) (j : N' →ₗ[S] N),
  Function.Injective ⇑i →
    Submodule.span R ↑j.range = ⊤ →
      ∀ (hp : ∀ (m : M') (n : N'), (p (i m)) (j n) ∈ (algebraMap S R).range),
        Function.Injective ⇑(i.restrictScalarsRange₂ j (Algebra.linearMap S R) ⋯ p hp)
-- Mathlib.Order.UpperLower.Relative
isRelUpperSet_empty : ∀ {α : Type u_1} {P : α → Prop} [inst : LE α], IsRelUpperSet ∅ P
-- Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
CategoryTheory.kernelCokernelCompSequence.snakeInput_v₀₁_τ₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X Y Z : C} (f : X ⟶ Y)
  (g : Y ⟶ Z), (CategoryTheory.kernelCokernelCompSequence.snakeInput f g).v₀₁.τ₁ = CategoryTheory.Limits.kernel.ι f
-- Mathlib.NumberTheory.ModularForms.SlashActions
/-- A function `f : ℍ → ℂ` is slash-invariant, of weight `k ∈ ℤ` and level `Γ`,
if for every matrix `γ ∈ Γ` we have `f(γ • z)= (c*z+d)^k f(z)` where `γ= ![![a, b], ![c, d]]`,
and it acts on `ℍ` via Möbius transformations.  -/
ModularForm.slash_action_eq'_iff : ∀ (k : ℤ) (f : UpperHalfPlane → ℂ) (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) (z : UpperHalfPlane),
  SlashAction.map k γ f z = f z ↔ f (γ • z) = (↑(↑γ 1 0) * ↑z + ↑(↑γ 1 1)) ^ k * f z
-- Mathlib.Data.DFinsupp.Sigma
DFinsupp.sigmaUncurry_single : ∀ {ι : Type u} {α : ι → Type u_2} {δ : (i : ι) → α i → Type v} [inst : DecidableEq ι]
  [inst_1 : (i : ι) → (j : α i) → Zero (δ i j)] [inst_2 : (i : ι) → DecidableEq (α i)] (i : ι) (j : α i) (x : δ i j),
  (fun₀ | i => fun₀ | j => x).sigmaUncurry = fun₀ | ⟨i, j⟩ => x
-- Mathlib.Algebra.BigOperators.Group.List.Lemmas
List.alternatingSum_append : ∀ {G : Type u_7} [inst : AddCommGroup G] (l₁ l₂ : List G),
  (l₁ ++ l₂).alternatingSum = l₁.alternatingSum + (-1) ^ l₁.length • l₂.alternatingSum
-- Mathlib.Algebra.Group.Action.Pointwise.Finset
Finset.smulCommClass_finset'' : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : DecidableEq γ] [inst_1 : SMul α γ] [inst_2 : SMul β γ]
  [SMulCommClass α β γ], SMulCommClass (Finset α) β (Finset γ)
-- Init.Data.Vector.Attach
Vector.all_subtype : ∀ {α : Type u_1} {n : ℕ} {p : α → Prop} {xs : Vector { x // p x } n} {f : { x // p x } → Bool} {g : α → Bool},
  (∀ (x : α) (h : p x), f ⟨x, h⟩ = g x) → xs.all f = xs.unattach.all g
-- Mathlib.FieldTheory.RatFunc.AsPolynomial
/-- If a valuation `v` is trivial on constants then for every `n : ℕ` the valuation of
`(monomial n a)` is equal to `(v RatFunc.X) ^ n`.  -/
Polynomial.valuation_monomial_eq_valuation_X_pow : ∀ (K : Type u_1) [inst : Field K] {Γ : Type u_2} [inst_1 : LinearOrderedCommGroupWithZero Γ]
  {v : Valuation (RatFunc K) Γ} [hv : Valuation.IsTrivialOn K v] (n : ℕ) {a : K},
  a ≠ 0 → v ↑((Polynomial.monomial n) a) = v RatFunc.X ^ n
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.mk.eta : ∀ {R : Type u_1} {c₁ c₂ c₃ : R} (a : QuaternionAlgebra R c₁ c₂ c₃),
  { re := a.re, imI := a.imI, imJ := a.imJ, imK := a.imK } = a
-- Mathlib.Order.Concept
upperPolar_le : ∀ {α : Type u_2} {s : Set α} [inst : LE α], upperPolar (fun x1 x2 => x1 ≤ x2) s = upperBounds s
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Cat
CategoryTheory.Cat.instCartesianMonoidalCategory : CategoryTheory.CartesianMonoidalCategory CategoryTheory.Cat
-- Mathlib.Logic.Function.Basic
Function.Injective.isPartialOrder_onFun : ∀ {α : Sort u_1} {β : Sort u_2} (r : β → β → Prop) {f : α → β},
  Function.Injective f → ∀ [IsPartialOrder β r], IsPartialOrder α (Function.onFun r f)
-- Mathlib.CategoryTheory.Bicategory.Modification.Pseudo
CategoryTheory.Pseudofunctor.StrongTrans.Hom.of.sizeOf_spec : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.Pseudofunctor B C} {η θ : F ⟶ G} [inst_2 : SizeOf B] [inst_3 : SizeOf C]
  (as : CategoryTheory.Pseudofunctor.StrongTrans.Modification η θ), sizeOf { as := as } = 1 + sizeOf as
-- Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
WeierstrassCurve.c₄_of_char_two : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) [CharP R 2], W.c₄ = W.a₁ ^ 4
-- Mathlib.LinearAlgebra.Dual.Defs
/-- The transposition of linear maps, as a linear map from `M →ₗ[R] M'` to
`Dual R M' →ₗ[R] Dual R M`.  -/
Module.Dual.transpose : {R : Type u_1} →
  {M : Type u_3} →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] →
          {M' : Type u_4} →
            [inst_3 : AddCommMonoid M'] →
              [inst_4 : Module R M'] → (M →ₗ[R] M') →ₗ[R] Module.Dual R M' →ₗ[R] Module.Dual R M
-- Mathlib.Algebra.Module.Submodule.LinearMap
LinearMap.comp_codLift : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {σ₁₂ : R →+* R₂}
  (f : M →ₛₗ[σ₁₂] M₂) {M₂' : Type u_10} [inst_6 : AddCommMonoid M₂'] [inst_7 : Module R₂ M₂'] (p : M₂' →ₗ[R₂] M₂)
  (hp : Function.Injective ⇑p) (h : ∀ (c : M), f c ∈ Set.range ⇑p), p ∘ₛₗ f.codLift p hp h = f
-- Mathlib.Data.Nat.Prime.Basic
Nat.Prime.coprime_pow_of_not_dvd : ∀ {p m a : ℕ}, Nat.Prime p → ¬p ∣ a → a.Coprime (p ^ m)
-- Mathlib.Data.Finset.Insert
Finset.empty_ssubset_singleton : ∀ {α : Type u_1} {a : α}, ∅ ⊂ {a}
-- Mathlib.Analysis.Normed.Module.RCLike.Basic
/-- If a map `f` over an `RCLike` space satisfies `‖x‖ = 1 → 1 ≤ K * ‖f x‖`, then
`f` is antilipschitz with constant `K`.
We require that the map is an additive monoid homomorphism, and acts as a multiplicative action:
in practice this means `f` is a linear map, but we allow the flexibility so it is convenient
to apply for eg continuous linear maps also, without a coercion in the goal.
 -/
antilipschitz_of_bound_of_norm_one : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {𝓕 : Type u_3} {E : Type u_4} {F : Type u_5} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedSpace 𝕜 F] [inst_5 : FunLike 𝓕 E F]
  [AddMonoidHomClass 𝓕 E F] [MulActionHomClass 𝓕 𝕜 E F] (f : 𝓕) {K : NNReal},
  (∀ (x : E), ‖x‖ = 1 → 1 ≤ ↑K * ‖f x‖) → AntilipschitzWith K ⇑f
-- Mathlib.Data.Nat.Choose.Sum
/-- A version of `Commute.add_pow` that avoids ℕ-subtraction by summing over the antidiagonal and
also with the binomial coefficient applied via scalar action of ℕ.  -/
Commute.add_pow' : ∀ {R : Type u_1} [inst : Semiring R] {x y : R},
  Commute x y → ∀ (n : ℕ), (x + y) ^ n = ∑ m ∈ Finset.HasAntidiagonal.antidiagonal n, n.choose m.1 • (x ^ m.1 * y ^ m.2)
-- Mathlib.Data.Nat.Choose.Dvd
Nat.Prime.dvd_choose_add : ∀ {p a b : ℕ}, Nat.Prime p → a < p → b < p → p ≤ a + b → p ∣ (a + b).choose a
-- Mathlib.GroupTheory.GroupAction.Quotient
Subgroup.normalCore_eq_ker : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G), H.normalCore = (MulAction.toPermHom G (G ⧸ H)).ker
-- Lean.Parser.Basic
/-- The `colGt` parser requires that the next token starts a strictly greater column than the saved
position (see `withPosition`). This can be used for whitespace sensitive syntax for the arguments
to a tactic, to ensure that the following tactic is not interpreted as an argument.
```
example (x : False) : False := by
  revert x
  exact id
```
Here, the `revert` tactic is followed by a list of `colGt ident`, because otherwise it would
interpret `exact` as an identifier and try to revert a variable named `exact`.

This parser has arity 0 - it does not capture anything.  -/
Lean.Parser.checkColGt : optParam String "checkColGt" → Lean.Parser.Parser
-- Std.Tactic.BVDecide.Reflect
_private.Std.Tactic.BVDecide.Reflect.0.Std.Tactic.BVDecide.Reflect.verifyCert.match_1.splitter : (motive : Except String (Array Std.Tactic.BVDecide.LRAT.IntAction) → Sort u_1) →
  (x : Except String (Array Std.Tactic.BVDecide.LRAT.IntAction)) →
    ((lratProof : Array Std.Tactic.BVDecide.LRAT.IntAction) → motive (Except.ok lratProof)) →
      ((a : String) → motive (Except.error a)) → motive x
-- Mathlib.Topology.Order.LowerUpperTopology
Topology.WithLower.toLower_symm : ∀ {α : Type u_1}, Topology.WithLower.toLower.symm = Topology.WithLower.ofLower
-- Lean.Parser.Extension
Lean.Parser.ParserExtension.Entry : Type
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.getD_map : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {γ : Type w} {m : Std.DHashMap.Raw α fun x => β}
  [LawfulBEq α] {f : α → β → γ} {k : α} {fallback : γ},
  m.WF →
    Std.DHashMap.Raw.Const.getD (Std.DHashMap.Raw.map f m) k fallback =
      (Option.map (f k) (Std.DHashMap.Raw.Const.get? m k)).getD fallback
-- Mathlib.RingTheory.Localization.AtPrime.Extension
IsDedekindDomain.primesOverEquivPrimesOver_symm_apply : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal R)
  [inst_3 : p.IsPrime] (Rₚ : Type u_3) [inst_4 : CommRing Rₚ] [inst_5 : Algebra R Rₚ]
  [inst_6 : IsLocalization.AtPrime Rₚ p] [inst_7 : IsLocalRing Rₚ] (Sₚ : Type u_4) [inst_8 : CommRing Sₚ]
  [inst_9 : Algebra S Sₚ] [inst_10 : IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ]
  [inst_11 : Algebra Rₚ Sₚ] [inst_12 : IsDomain R] [inst_13 : IsDedekindDomain S] [inst_14 : Module.IsTorsionFree R S]
  [inst_15 : Algebra R Sₚ] [inst_16 : IsScalarTower R S Sₚ] [inst_17 : IsScalarTower R Rₚ Sₚ] (hp : p ≠ ⊥)
  (Q : ↑((IsLocalRing.maximalIdeal Rₚ).primesOver Sₚ)),
  ↑((IsDedekindDomain.primesOverEquivPrimesOver p Rₚ Sₚ hp).symm Q) = Ideal.comap (algebraMap S Sₚ) ↑Q
-- Mathlib.Analysis.Calculus.FDeriv.Mul
/-- Eta-expanded form of `Differentiable.smul` -/
Differentiable.fun_smul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {𝕜' : Type u_5} [inst_5 : NormedRing 𝕜'] [inst_6 : NormedAlgebra 𝕜 𝕜'] [inst_7 : Module 𝕜' F] [IsBoundedSMul 𝕜' F]
  [IsScalarTower 𝕜 𝕜' F] {c : E → 𝕜'}, Differentiable 𝕜 c → Differentiable 𝕜 f → Differentiable 𝕜 fun i => c i • f i
-- Mathlib.Topology.Connected.PathConnected
/-- When `x` and `y` are joined in `F`, choose a path from `x` to `y` inside `F`  -/
JoinedIn.somePath : {X : Type u_1} → [inst : TopologicalSpace X] → {x y : X} → {F : Set X} → JoinedIn F x y → Path x y
-- Mathlib.SetTheory.ZFC.PSet
PSet.instLawfulSingleton : LawfulSingleton PSet.{u_1} PSet.{u_1}
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
/-- Shorthand for the 2nd group homology of a `k`-linear `G`-representation `A`, `H₂(G, A)`,
defined as the 2nd homology of the complex of inhomogeneous chains of `A`.  -/
groupHomology.H2 : {k G : Type u} → [inst : CommRing k] → [inst_1 : Group G] → Rep.{u, u, u} k G → ModuleCat k
-- Mathlib.Algebra.Polynomial.Monic
Polynomial.Monic.mul_left_ne_zero : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p.Monic → ∀ {q : Polynomial R}, q ≠ 0 → q * p ≠ 0
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKey_diff : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] (h₁ : (↑m₁).WF) (h₂ : (↑m₂).WF) {k : α}
  {h_contains : (m₁.diff m₂).contains k = true}, (m₁.diff m₂).getKey k h_contains = m₁.getKey k ⋯
-- Init.Prelude
/-- Make name `s₁.s₂.s₃.s₄.s₅`  -/
Lean.Name.mkStr5 : String → String → String → String → String → Lean.Name
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
SimpleGraph.chromaticNumber_bot : ∀ {V : Type u} [Nonempty V], ⊥.chromaticNumber = 1
-- Mathlib.CategoryTheory.Monoidal.Grp
/-- The trivial additive group object.  -/
CategoryTheory.AddGrp.trivial : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] → CategoryTheory.AddGrp C
-- Mathlib.Data.List.MinMax
List.maximum_of_length_pos.congr_simp : ∀ {α : Type u_1} [inst : LinearOrder α] {l l_1 : List α} (e_l : l = l_1) (h : 0 < l.length),
  List.maximum_of_length_pos h = List.maximum_of_length_pos ⋯
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.sub_equiv_sub : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α]
  [inst_3 : Ring β] {abv : β → α} [inst_4 : IsAbsoluteValue abv] {f1 f2 g1 g2 : CauSeq β abv},
  f1 ≈ f2 → g1 ≈ g2 → f1 - g1 ≈ f2 - g2
-- Std.Internal.Parsec.ByteArray
/-- Parses while a predicate is satisfied, consuming at most `limit` bytes, requiring at least one.
Unlike `takeWhileUpTo1`, succeeds even if input ends before the predicate stops holding.
 -/
Std.Internal.Parsec.ByteArray.takeWhile1AtMost : (UInt8 → Bool) → ℕ → Std.Internal.Parsec.ByteArray.Parser ByteSlice
-- Mathlib.GroupTheory.Coxeter.Basic
_private.Mathlib.GroupTheory.Coxeter.Basic.0.CoxeterSystem.alternatingWord.match_1.splitter : (motive : ℕ → Sort u_1) → (m : ℕ) → (Unit → motive 0) → ((m : ℕ) → motive m.succ) → motive m
-- Mathlib.Topology.Semicontinuity.Hemicontinuity
/-- A correspondence `f : α → Set β` is upper hemicontinuous if and only if its *lower inverse*
(i.e., `u : Set β ↦ (f ⁻¹' (Iic uᶜ))ᶜ`, note that `f ⁻¹' (Iic u) = {x | (f x ∩ u).Nonempty}`)
sends closed sets to closed sets.  -/
upperHemicontinuous_iff_isClosed_compl_preimage_Iic_compl : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {f : α → Set β} [inst_1 : TopologicalSpace β],
  UpperHemicontinuous f ↔ ∀ (u : Set β), IsClosed u → IsClosed (f ⁻¹' Set.Iic uᶜ)ᶜ
-- Init.Data.SInt.Bitwise
ISize.xor_not : ∀ {a b : ISize}, a ^^^ ~~~b = ~~~(a ^^^ b)
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
/-- `ζ - 1` is prime if `ζ` is a primitive `2 ^ (k + 1)`-th root of unity.
See `zeta_sub_one_prime` for a general statement.  -/
IsPrimitiveRoot.zeta_sub_one_prime_of_two_pow : ∀ {k : ℕ} {K : Type u} [inst : Field K] {ζ : K} [inst_1 : CharZero K] [IsCyclotomicExtension {2 ^ (k + 1)} ℚ K]
  (hζ : IsPrimitiveRoot ζ (2 ^ (k + 1))), Prime (hζ.toInteger - 1)
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubAddAction.instCompleteLattice.eq_1 : ∀ {R : Type u} {M : Type v} [inst : VAdd R M],
  SubAddAction.instCompleteLattice = Function.Injective.completeLattice SetLike.coe ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
-- Mathlib.CategoryTheory.Skeletal
CategoryTheory.ThinSkeleton.isSkeletonOfInhabited : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : Quiver.IsThin C] →
      Inhabited
        (CategoryTheory.IsSkeletonOf C (CategoryTheory.ThinSkeleton C) (CategoryTheory.ThinSkeleton.fromThinSkeleton C))
-- Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
CochainComplex.shiftShortComplexFunctorIso_inv_app_τ₁ : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] (n i i' : ℤ)
  (hi : n + i = i') (X : CochainComplex C ℤ),
  ((CochainComplex.shiftShortComplexFunctorIso C n i i' hi).inv.app X).τ₁ =
    (n.negOnePow •
        (CochainComplex.shiftEval C n ((ComplexShape.up ℤ).prev i) ((ComplexShape.up ℤ).prev i') ⋯).app X).inv
-- Mathlib.AlgebraicGeometry.Spec
AlgebraicGeometry.Spec.locallyRingedSpaceObj_presheaf_map : ∀ (R : CommRingCat)
  {U V : (TopologicalSpace.Opens ↑↑(AlgebraicGeometry.Spec.locallyRingedSpaceObj R).toPresheafedSpace)ᵒᵖ} (i : U ⟶ V),
  (AlgebraicGeometry.Spec.locallyRingedSpaceObj R).presheaf.map i = (AlgebraicGeometry.Spec.structureSheaf ↑R).obj.map i
-- Mathlib.CategoryTheory.Sigma.Basic
CategoryTheory.Sigma.natIso_hom : ∀ {I : Type w₁} {C : I → Type u₁} [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] {q₁ q₂ : CategoryTheory.Functor ((i : I) × C i) D}
  (h : (i : I) → (CategoryTheory.Sigma.incl i).comp q₁ ≅ (CategoryTheory.Sigma.incl i).comp q₂),
  (CategoryTheory.Sigma.natIso h).hom = CategoryTheory.Sigma.natTrans fun i => (h i).hom
-- Mathlib.Order.UpperLower.Basic
isLowerSet_setOfPred : ∀ {α : Type u_1} [inst : Preorder α] {p : α → Prop}, IsLowerSet {a | p a} ↔ Antitone p
-- Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity
SimpleGraph.isGLB_turanDensity : ∀ {W : Type u_1} (H : SimpleGraph W),
  IsGLB {x | ∃ n ∈ Set.Ici 2, ↑(SimpleGraph.extremalNumber n H) / ↑(n.choose 2) = x} H.turanDensity
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.isEmpty_iff_forall_not_mem : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α],
  m.isEmpty = true ↔ ∀ (a : α), a ∉ m
-- Batteries.Recycling.RBTree.Basic
/-- `O(log n)`. Turn a node into a stream, by descending along the left spine.  -/
RBTree.RBNode.toStream : {α : Type u_1} → RBTree.RBNode α → optParam (RBTree.RBNode.Stream α) RBTree.RBNode.Stream.nil → RBTree.RBNode.Stream α
-- Init.GrindInstances.Ring.Nat
Lean.Grind.instNoNatZeroDivisorsNat : Lean.Grind.NoNatZeroDivisors ℕ
-- Mathlib.Data.Finset.Dedup
List.toFinset_surjective : ∀ {α : Type u_1} [inst : DecidableEq α], Function.Surjective List.toFinset
-- Mathlib.RingTheory.AdicCompletion.Basic
IsAdicComplete.of_comp_lift : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {N : Type u_5} [inst_3 : AddCommGroup N] [inst_4 : Module R N] [inst_5 : IsAdicComplete I N]
  (f : (n : ℕ) → M →ₗ[R] N ⧸ I ^ n • ⊤) (h : ∀ {m n : ℕ} (hle : m ≤ n), Submodule.factorPow I N hle ∘ₗ f n = f m),
  AdicCompletion.of I N ∘ₗ IsAdicComplete.lift I f ⋯ = AdicCompletion.lift I f ⋯
-- Mathlib.Data.Finset.Union
Finset.biUnion_mono : ∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {t₁ t₂ : α → Finset β} [inst : DecidableEq β],
  (∀ a ∈ s, t₁ a ⊆ t₂ a) → s.biUnion t₁ ⊆ s.biUnion t₂
-- Init.Tactics
/-- `assumption_mod_cast` is a variant of `assumption` that solves the goal
using a hypothesis. Unlike `assumption`, it first pre-processes the goal and
each hypothesis to move casts as far outwards as possible, so it can be used
in more situations.

Concretely, it runs `norm_cast` on the goal. For each local hypothesis `h`, it also
normalizes `h` with `norm_cast` and tries to use that to close the goal.  -/
Lean.Parser.Tactic.tacticAssumption_mod_cast_ : Lean.ParserDescr
-- Mathlib.LinearAlgebra.AffineSpace.Slope
slope_same : ∀ {k : Type u_1} {E : Type u_2} {PE : Type u_3} [inst : Field k] [inst_1 : AddCommGroup E] [inst_2 : Module k E]
  [inst_3 : AddTorsor E PE] (f : k → PE) (a : k), slope f a a = 0
-- Mathlib.CategoryTheory.Limits.Preserves.Finite
/-- If we reflect colimits of some arbitrary size, then we reflect all finite colimits.  -/
CategoryTheory.Limits.ReflectsColimitsOfSize.reflectsFiniteColimits : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.ReflectsColimitsOfSize.{w, w₂, v₁, v₂, u₁, u₂} F],
  CategoryTheory.Limits.ReflectsFiniteColimits F
-- Mathlib.Tactic.Rify
Mathlib.Tactic.Rify.ratCast_le : ∀ (a b : ℚ), a ≤ b ↔ ↑a ≤ ↑b
-- Lean.Meta.Sym.Pattern
/-- Structural definitional equality for lists of universe levels.
Returns `true` iff the lists have the same length and corresponding elements are structurally equal.
 -/
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.isLevelDefEqListS : List Lean.Level → List Lean.Level → Lean.MetaM Bool
-- Mathlib.GroupTheory.OreLocalization.OreSet
/-- Common summands on the right can be turned into common summands on the left, a weak form of
cancellability.  -/
AddOreLocalization.AddOreSet.ore_right_cancel : ∀ {R : Type u_1} {inst : AddMonoid R} {S : AddSubmonoid R} [self : AddOreLocalization.AddOreSet S] (r₁ r₂ : R) (s : ↥S),
  r₁ + ↑s = r₂ + ↑s → ∃ s', ↑s' + r₁ = ↑s' + r₂