mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.getKey!_modifyKey_self : ∀ {α : Type u} {β : Type v} [inst : BEq α] [EquivBEq α] [inst_2 : Inhabited α] {k : α} {f : β → β}
  (l : List ((_ : α) × β)),
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.getKey! k (Std.Internal.List.Const.modifyKey k f l) =
      if Std.Internal.List.containsKey k l = true then k else default
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.injOn_sin : Set.InjOn Real.sin (Set.Icc (-(Real.pi / 2)) (Real.pi / 2))
-- Mathlib.SetTheory.Cardinal.ENat
Cardinal.ofENat_injective : Function.Injective Cardinal.ofENat
-- Mathlib.Data.DFinsupp.NeLocus
DFinsupp.zipWith_neLocus_eq_right : ∀ {α : Type u_1} {N : α → Type u_2} [inst : DecidableEq α] {M : α → Type u_3} {P : α → Type u_4}
  [inst_1 : (a : α) → Zero (N a)] [inst_2 : (a : α) → Zero (M a)] [inst_3 : (a : α) → Zero (P a)]
  [inst_4 : (a : α) → DecidableEq (M a)] [inst_5 : (a : α) → DecidableEq (P a)] {F : (a : α) → M a → N a → P a}
  (F0 : ∀ (a : α), F a 0 0 = 0) (f₁ f₂ : Π₀ (a : α), M a) (g : Π₀ (a : α), N a),
  (∀ (a : α) (g : N a), Function.Injective fun f => F a f g) →
    (DFinsupp.zipWith F F0 f₁ g).neLocus (DFinsupp.zipWith F F0 f₂ g) = f₁.neLocus f₂
-- Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting
CategoryTheory.MorphismProperty.isStableUnderTransfiniteCompositionOfShape_llp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) (J : Type w)
  [inst_1 : LinearOrder J] [inst_2 : SuccOrder J] [inst_3 : OrderBot J] [inst_4 : WellFoundedLT J],
  W.llp.IsStableUnderTransfiniteCompositionOfShape J
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
mul_inv_lt_iff_lt_mul : ∀ {α : Type u} [inst : Group α] [inst_1 : LT α] [MulRightStrictMono α] {a b c : α}, a * b⁻¹ < c ↔ a < c * b
-- Mathlib.CategoryTheory.Idempotents.FunctorExtension
/-- The canonical functor `(C ⥤ Karoubi D) ⥤ (Karoubi C ⥤ Karoubi D)`  -/
CategoryTheory.Idempotents.functorExtension₁ : (C : Type u_1) →
  (D : Type u_2) →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        CategoryTheory.Functor (CategoryTheory.Functor C (CategoryTheory.Idempotents.Karoubi D))
          (CategoryTheory.Functor (CategoryTheory.Idempotents.Karoubi C) (CategoryTheory.Idempotents.Karoubi D))
-- Mathlib.MeasureTheory.Order.Group.Lattice
AEMeasurable.abs : ∀ {α : Type u_1} {β : Type u_2} [inst : Lattice α] [inst_1 : AddGroup α] [inst_2 : MeasurableSpace α]
  [inst_3 : MeasurableSpace β] {f : β → α} [MeasurableNeg α] [MeasurableSup₂ α] {μ : MeasureTheory.Measure β},
  AEMeasurable f μ → AEMeasurable (fun x => |f x|) μ
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.isEmpty_eq_size_eq_zero : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β}, m.isEmpty = (m.size == 0)
-- Mathlib.Data.Multiset.Count
Multiset.Rel.countP_eq : ∀ {α : Type u_1} (r : α → α → Prop) [IsTrans α r] [Std.Symm r] {s t : Multiset α} (x : α) [inst : DecidablePred (r x)],
  Multiset.Rel r s t → Multiset.countP (r x) s = Multiset.countP (r x) t
-- Mathlib.RingTheory.Localization.Ideal
/-- `quotientMap` applied to maximal ideals of a localization is `surjective`.
The quotient by a maximal ideal is a field, so inverses to elements already exist,
and the localization necessarily maps the equivalence class of the inverse in the localization  -/
IsLocalization.surjective_quotientMap_of_maximal_of_localization : ∀ {R : Type u_1} [inst : CommRing R] (M : Submonoid R) (S : Type u_2) [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [IsLocalization M S] {I : Ideal S} [I.IsPrime] {J : Ideal R} {H : J ≤ Ideal.under R I},
  (Ideal.under R I).IsMaximal → Function.Surjective ⇑(Ideal.quotientMap I (algebraMap R S) H)
-- Mathlib.RepresentationTheory.FDRep
FDRep.endRingEquiv_symm_comp_ρ : ∀ {R : Type u} {G : Type v} [inst : CommRing R] [inst_1 : Monoid G] (V : FDRep R G),
  (↑V.V.obj.endRingEquiv.symm).comp V.ρ = CategoryTheory.InducedCategory.endEquiv.toMonoidHom.comp V.ρ
-- Init.Data.Fin.Fold
_private.Init.Data.Fin.Fold.0.Fin.foldr.loop.match_1.splitter : {α : Sort u_2} →
  (n : ℕ) →
    (motive : (x : ℕ) → x ≤ n → α → Sort u_1) →
      (x : ℕ) →
        (x_1 : x ≤ n) →
          (x_2 : α) →
            ((x : 0 ≤ n) → (x_3 : α) → motive 0 x x_3) →
              ((i : ℕ) → (h : i + 1 ≤ n) → (x : α) → motive i.succ h x) → motive x x_1 x_2
-- Mathlib.Analysis.InnerProductSpace.PiL2
Complex.isometryOfOrthonormal_apply : ∀ {F : Type u_5} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] (v : OrthonormalBasis (Fin 2) ℝ F)
  (z : ℂ), (Complex.isometryOfOrthonormal v) z = z.re • v 0 + z.im • v 1
-- Mathlib.Probability.Moments.SubGaussian
ProbabilityTheory.Kernel.HasSubgaussianMGF.neg : ∀ {Ω : Type u_1} {Ω' : Type u_2} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {ν : MeasureTheory.Measure Ω'}
  {κ : ProbabilityTheory.Kernel Ω' Ω} {X : Ω → ℝ} {c : NNReal},
  ProbabilityTheory.Kernel.HasSubgaussianMGF X c κ ν → ProbabilityTheory.Kernel.HasSubgaussianMGF (-X) c κ ν
-- Init.Data.Fin.Lemmas
Fin.succRecOn_succ : ∀ {motive : (n : ℕ) → Fin n → Sort u_1} {zero : (n : ℕ) → motive (n + 1) 0}
  {succ : (n : ℕ) → (i : Fin n) → motive n i → motive n.succ i.succ} {n : ℕ} (i : Fin n),
  i.succ.succRecOn zero succ = succ n i (i.succRecOn zero succ)
-- Mathlib.Data.Sign.Defs
SignType.neg_one_lt_iff : ∀ {a : SignType}, -1 < a ↔ 0 ≤ a
-- Mathlib.Algebra.Group.ForwardDiff
Polynomial.fwdDiff_iter_eq_zero_of_degree_lt : ∀ {R : Type u_3} [inst : CommRing R] {P : Polynomial R} {n : ℕ},
  P.natDegree < n → ((fwdDiff 1)^[n] fun x => Polynomial.eval x P) = 0
-- Mathlib.Geometry.Euclidean.SignedDist
signedDist_apply_linear : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (v : V) (p : P), (↑((signedDist v) p)).linear = (innerₗ V) (NormedSpace.normalize v)
-- Mathlib.Topology.VectorBundle.FiniteDimensional
VectorBundle.finiteDimensional : ∀ (R : Type u_1) {B : Type u_2} (F : Type u_3) (E : B → Type u_4) [inst : NontriviallyNormedField R]
  [inst_1 : TopologicalSpace B] [inst_2 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_3 : NormedAddCommGroup F]
  [inst_4 : NormedSpace R F] [inst_5 : (x : B) → TopologicalSpace (E x)] [inst_6 : FiberBundle F E]
  [inst_7 : (x : B) → AddCommGroup (E x)] [inst_8 : (x : B) → Module R (E x)] [VectorBundle R F E] (b : B)
  [FiniteDimensional R F], FiniteDimensional R (E b)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get!_union_of_not_mem_left : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {m₁ m₂ : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : Inhabited β],
  m₁.WF → m₂.WF → ∀ {k : α}, k ∉ m₁ → Std.DTreeMap.Raw.Const.get! (m₁ ∪ m₂) k = Std.DTreeMap.Raw.Const.get! m₂ k
-- Mathlib.Topology.EMetricSpace.Weak
/-- The one point compactification of a weak extended metric space is again a weak extended metric
space.  -/
instWeakEMetricSpaceOnePoint : {α : Type u} → [t : TopologicalSpace α] → [m : WeakEMetricSpace α] → WeakEMetricSpace (OnePoint α)
-- Lean.Elab.BuiltinCommand
/-- Elaborate `deprecated_module`, marking the current module as deprecated.  -/
Lean.Elab.Command.elabDeprecatedModule : Lean.Elab.Command.CommandElab
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKeyD_insertManyIfNewUnit_list_of_not_mem_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α Unit} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l : List α} {k k' fallback : α},
  (k == k') = true →
    k ∉ m → List.Pairwise (fun a b => (a == b) = false) l → k ∈ l → (m.insertManyIfNewUnit l).getKeyD k' fallback = k
-- Mathlib.Order.Lattice
le_iff_exists_inf : ∀ {α : Type u} [inst : SemilatticeInf α] {a b : α}, b ≤ a ↔ ∃ c, b = a ⊓ c
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.Functor.FullyFaithful.homNatIso'_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful) (X X_1 : C),
  (hF.homNatIso' X).hom.app X_1 = (Equiv.ulift.trans (hF.homEquiv.symm.trans Equiv.ulift.symm)).toIso.hom
-- Mathlib.GroupTheory.Torsion
CommGroup.freeRank_eq_zero_iff : ∀ {G : Type u_1} [inst : CommGroup G] [inst_1 : Group.FG G], CommGroup.freeRank G = 0 ↔ IsMulTorsion G
-- Mathlib.LinearAlgebra.Finsupp.LinearCombination
/-- A family `v : α → V` is generating `V` iff every element `(x : V)`
can be written as sum `∑ cᵢ • vᵢ = x`.
 -/
Submodule.top_le_span_range_iff_forall_exists_fun : ∀ {α : Type u_1} {M : Type u_2} (R : Type u_3) [inst : Fintype α] [inst_1 : Semiring R] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] {v : α → M}, ⊤ ≤ Submodule.span R (Set.range v) ↔ ∀ (x : M), ∃ c, ∑ i, c i • v i = x
-- Init.Data.String.Lemmas.Iterate
_private.Init.Data.String.Lemmas.Iterate.0.String.Slice.Model.revPositionsFrom.eq_def : ∀ {s : String.Slice} (p : s.Pos),
  String.Slice.Model.revPositionsFrom p =
    if h : p = s.startPos then [] else ⟨p.prev h, ⋯⟩ :: String.Slice.Model.revPositionsFrom (p.prev h)
-- Mathlib.Algebra.CubicDiscriminant
Cubic.natDegree_of_b_ne_zero : ∀ {R : Type u_1} {P : Cubic R} [inst : Semiring R], P.a = 0 → P.b ≠ 0 → P.toPoly.natDegree = 2
-- Mathlib.RingTheory.MvPowerSeries.Substitution
MvPowerSeries.HasSubst.map : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommRing R] {τ : Type u_4} {S : Type u_5} [inst_1 : CommRing S]
  {a : σ → MvPowerSeries τ R},
  MvPowerSeries.HasSubst a → ∀ (h : R →+* S), MvPowerSeries.HasSubst fun i => (MvPowerSeries.map h) (a i)
-- Init.Data.String.Lemmas.Pattern.Find.Basic
String.find?_eq_find?_toSlice : ∀ {ρ : Type} {pat : ρ} {σ : String.Slice → Type}
  [inst : (s : String.Slice) → Std.Iterator (σ s) Id (String.Slice.Pattern.SearchStep s)]
  [inst_1 : (s : String.Slice) → Std.IteratorLoop (σ s) Id Id] [inst_2 : String.Slice.Pattern.ToForwardSearcher pat σ]
  {s : String}, s.find? pat = Option.map String.Pos.ofToSlice (s.toSlice.find? pat)
-- Mathlib.Combinatorics.Graph.Subgraph
Graph.IsClosedSubgraph.mem_tfae_of_isLink : ∀ {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G H : Graph α β},
  G.IsLink e x y → H.IsClosedSubgraph G → [x ∈ H.vertexSet, y ∈ H.vertexSet, e ∈ H.edgeSet].TFAE
-- Mathlib.LinearAlgebra.CliffordAlgebra.Basic
CliffordAlgebra.equivOfIsometry_trans : ∀ {R : Type u_1} [inst : CommRing R] {M₁ : Type u_4} {M₂ : Type u_5} {M₃ : Type u_6} [inst_1 : AddCommGroup M₁]
  [inst_2 : AddCommGroup M₂] [inst_3 : AddCommGroup M₃] [inst_4 : Module R M₁] [inst_5 : Module R M₂]
  [inst_6 : Module R M₃] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} {Q₃ : QuadraticForm R M₃}
  (e₁₂ : QuadraticMap.IsometryEquiv Q₁ Q₂) (e₂₃ : QuadraticMap.IsometryEquiv Q₂ Q₃),
  (CliffordAlgebra.equivOfIsometry e₁₂).trans (CliffordAlgebra.equivOfIsometry e₂₃) =
    CliffordAlgebra.equivOfIsometry (e₁₂.trans e₂₃)
-- Lean.Parser.Basic
Lean.Parser.longestMatchFn : Option Lean.Syntax → List (Lean.Parser.Parser × ℕ) → Lean.Parser.ParserFn
-- Mathlib.Analysis.Analytic.CPolynomialDef
/-- The terms of the formal multilinear series `p.changeOrigin` are continuously polynomial
as we vary the origin  -/
FormalMultilinearSeries.cpolynomialAt_changeOrigin_of_finite : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  (p : FormalMultilinearSeries 𝕜 E F) {n : ℕ},
  (∀ (m : ℕ), n ≤ m → p m = 0) → ∀ (k : ℕ), CPolynomialAt 𝕜 (fun x => p.changeOrigin x k) 0
-- Mathlib.Combinatorics.Additive.PluenneckeRuzsa
/-- **Ruzsa's triangle inequality**. Add-addneg-add version.  -/
Finset.ruzsa_triangle_inequality_add_addNeg_add : ∀ {G : Type u_1} [inst : DecidableEq G] [inst_1 : AddGroup G] (A B C : Finset G),
  B.card * (A + C).card ≤ (B + -A).card * (B + C).card
-- Std.Internal.Do.Triple.Basic
Std.Internal.Do.Triple.iff : ∀ {Pred EPred : Type u} {Prog : Type v} {Value : Type u} [inst : Std.Internal.Do.Assertion Pred]
  [inst_1 : Std.Internal.Do.Assertion EPred] [inst_2 : Std.Internal.Do.WP Prog Value Pred EPred] {x : Prog} {pre : Pred}
  {post : Value → Pred} {epost : EPred},
  ⦃ pre ⦄ x ⦃ post; epost ⦄ ↔ Lean.Order.PartialOrder.rel pre (Std.Internal.Do.wp x post epost)
-- Mathlib.Analysis.Normed.Group.Continuity
Filter.Tendsto.norm' : ∀ {α : Type u_1} {E : Type u_4} [inst : SeminormedGroup E] {a : E} {l : Filter α} {f : α → E},
  Filter.Tendsto f l (nhds a) → Filter.Tendsto (fun x => ‖f x‖) l (nhds ‖a‖)
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.homMk'_mk_id : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : D} {Y : C} {T : CategoryTheory.Functor C D} (f : S ⟶ T.obj Y),
  (CategoryTheory.StructuredArrow.mk f).homMk' (CategoryTheory.CategoryStruct.id Y) = CategoryTheory.eqToHom ⋯
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Real.arctan_eq_zero_iff : ∀ {x : ℝ}, Real.arctan x = 0 ↔ x = 0
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.prod_eq_of_fintype : ∀ {α : Type u} [h : Fintype α] (f : α → Cardinal.{v}), Cardinal.prod f = Cardinal.lift.{u, v} (∏ i, f i)
-- Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
AlgebraicGeometry.targetAffineLocally_affineAnd_iff : ∀ {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop},
  (RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => Q) →
    ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y),
      AlgebraicGeometry.targetAffineLocally (AlgebraicGeometry.affineAnd fun {R S} [CommRing R] [CommRing S] => Q) f ↔
        ∀ (U : Y.Opens),
          AlgebraicGeometry.IsAffineOpen U →
            AlgebraicGeometry.IsAffineOpen ((TopologicalSpace.Opens.map f.base).obj U) ∧
              Q (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.app f U))
-- Mathlib.Computability.Primrec.List
Primrec.list_range : Primrec List.range
-- Mathlib.CategoryTheory.Monad.Monadicity
CategoryTheory.Monad.MonadicityInternal.comparisonAdjunction_counit_app : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₁, u₂} D]
  {G : CategoryTheory.Functor D C} {F : CategoryTheory.Functor C D} (adj : F ⊣ G)
  [inst_2 : ∀ (A : adj.toMonad.Algebra), CategoryTheory.Limits.HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))]
  (B : D),
  (CategoryTheory.Monad.MonadicityInternal.comparisonAdjunction adj).counit.app B =
    CategoryTheory.Limits.colimit.desc
      (CategoryTheory.Limits.parallelPair (F.map (G.map (adj.counit.app B))) (adj.counit.app (F.obj (G.obj B))))
      (CategoryTheory.Monad.MonadicityInternal.counitCofork adj B)
-- Mathlib.Algebra.Lie.Basis.Basic
LieAlgebra.Basis.iSupIndep_rootSpace : ∀ {ι : Type u_1} {R : Type u_2} {L : Type u_3} [inst : Finite ι] [inst_1 : CommRing R] [inst_2 : LieRing L]
  [inst_3 : LieAlgebra R L] {H : LieSubalgebra R L} (b : LieAlgebra.Basis ι H) [inst_4 : Fintype ι] [IsDomain R]
  [CharZero R] [Module.IsTorsionFree R L],
  iSupIndep
    ![LieAlgebra.rootSpace H 0, ⨆ n, ⨆ (_ : n ≠ 0), LieAlgebra.rootSpace H (∑ i, n i • ⇑((-b.baseSupp) i)),
      ⨆ n, ⨆ (_ : n ≠ 0), LieAlgebra.rootSpace H (∑ i, n i • ⇑(b.baseSupp i))]
-- Mathlib.Topology.Instances.EReal.Lemmas
/-- The addition on `EReal` is continuous except where it doesn't make sense (i.e., at `(⊥, ⊤)`
and at `(⊤, ⊥)`).  -/
EReal.continuousAt_add : ∀ {p : EReal × EReal}, p.1 ≠ ⊤ ∨ p.2 ≠ ⊥ → p.1 ≠ ⊥ ∨ p.2 ≠ ⊤ → ContinuousAt (fun p => p.1 + p.2) p
-- Init.Tactics
/-- `trivial` tries different simple tactics (e.g., `rfl`, `contradiction`, ...)
to close the current goal.
You can use the command `macro_rules` to extend the set of tactics used. Example:
```
macro_rules | `(tactic| trivial) => `(tactic| simp)
```
 -/
Lean.Parser.Tactic.tacticTrivial : Lean.ParserDescr
-- Lean.Elab.Tactic.Omega.Core
Lean.Elab.Tactic.Omega.Justification.assumption.sizeOf_spec : ∀ (s : Lean.Omega.Constraint) (x : Lean.Omega.Coeffs) (i : ℕ),
  sizeOf (Lean.Elab.Tactic.Omega.Justification.assumption s x i) = 1 + sizeOf s + sizeOf x + sizeOf i
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- **Alias** of `Topology.RelCWComplex.skeletonLT_monotone`. -/
Topology.CWComplex.skeletonLT_monotone : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : T2Space X] [inst_1 : Topology.RelCWComplex C D],
  Monotone (Topology.RelCWComplex.skeletonLT C)
-- Mathlib.FieldTheory.IsAlgClosed.Basic
IsAlgClosed.dvd_iff_roots_le_roots : ∀ {k : Type u} [inst : Field k] [IsAlgClosed k] {p q : Polynomial k}, p ≠ 0 → q ≠ 0 → (p ∣ q ↔ p.roots ≤ q.roots)
-- Mathlib.LinearAlgebra.TensorProduct.Tower
TensorProduct.AlgebraTensorModule.lTensor_id : ∀ {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module A M]
  [inst_6 : IsScalarTower R A M] [inst_7 : AddCommMonoid N] [inst_8 : Module R N],
  (TensorProduct.AlgebraTensorModule.lTensor A M) LinearMap.id = LinearMap.id
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
/-- If `K` is a `p ^ k`-th cyclotomic extension of `ℚ`, then `(adjoin ℤ {ζ})` is the
integral closure of `ℤ` in `K`.  -/
IsCyclotomicExtension.Rat.isIntegralClosure_adjoin_singleton_of_prime_pow : ∀ {p k : ℕ} {K : Type u} [inst : Field K] {ζ : K} [hp : Fact (Nat.Prime p)] [inst_1 : CharZero K]
  [hcycl : IsCyclotomicExtension {p ^ k} ℚ K], IsPrimitiveRoot ζ (p ^ k) → IsIntegralClosure ↥ℤ[ζ] ℤ K
-- Lean.Data.JsonRpc
Lean.JsonRpc.Request.ofMessage? : Lean.JsonRpc.Message → Option (Lean.JsonRpc.Request Lean.Json)
-- Mathlib.NumberTheory.Real.Irrational
Irrational.of_add_intCast : ∀ {x : ℝ} (m : ℤ), Irrational (x + ↑m) → Irrational x
-- Mathlib.CategoryTheory.Abelian.NonPreadditive
CategoryTheory.NonPreadditiveAbelian.mono_r : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.NonPreadditiveAbelian C] {A : C},
  CategoryTheory.Mono (CategoryTheory.NonPreadditiveAbelian.r A)
-- Mathlib.Data.EReal.Basic
EReal.natCast_le_iff : ∀ {m n : ℕ}, ↑m ≤ ↑n ↔ m ≤ n
-- Batteries.Recycling.RBTree.WF
/-- The `erase` function preserves the balance invariants.  -/
RBTree.RBNode.Balanced.erase : ∀ {α : Type u_1} {c : RBTree.RBColor} {n : ℕ} {cut : α → Ordering} {t : RBTree.RBNode α},
  t.Balanced c n → ∃ n, (RBTree.RBNode.erase cut t).Balanced RBTree.RBColor.black n
-- Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
AlgebraicGeometry.IsClosedImmersion.overEquivIdealSheafData.eq_1 : ∀ (X : AlgebraicGeometry.Scheme),
  AlgebraicGeometry.IsClosedImmersion.overEquivIdealSheafData X =
    {
      functor :=
        (CategoryTheory.MorphismProperty.Over.forget @AlgebraicGeometry.IsClosedImmersion ⊤ X).op.comp X.kerFunctor,
      inverse :=
        { obj := fun I => Opposite.op (CategoryTheory.MorphismProperty.Over.mk ⊤ I.subschemeι ⋯),
          map := fun {I J} h =>
            (CategoryTheory.MorphismProperty.Over.homMk (AlgebraicGeometry.Scheme.IdealSheafData.inclusion ⋯) ⋯ ⋯).op,
          map_id := ⋯, map_comp := ⋯ },
      unitIso :=
        CategoryTheory.NatIso.ofComponents
          (fun Y =>
            (CategoryTheory.MorphismProperty.Over.isoMk
                (CategoryTheory.asIso (AlgebraicGeometry.Scheme.Hom.toImage (Opposite.unop Y).hom)).symm ⋯).op)
          ⋯,
      counitIso := CategoryTheory.NatIso.ofComponents (fun I => CategoryTheory.eqToIso ⋯) ⋯, functor_unitIso_comp := ⋯ }
-- Init.Core
DoResultPRBC.return.injEq : ∀ {α β σ : Type u} (a : β) (a_1 : σ) (a_2 : β) (a_3 : σ),
  (DoResultPRBC.return a a_1 = DoResultPRBC.return a_2 a_3) = (a = a_2 ∧ a_1 = a_3)
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.morphismRestrict_morphismRestrict_ι_isoImage_hom_assoc : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (U : Y.Opens) (V : (↑U).Opens) {Z : AlgebraicGeometry.Scheme}
  (h : ↑((AlgebraicGeometry.Scheme.Hom.opensFunctor U.ι).obj V) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (f ∣_ U ∣_ V)
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.isoImage U.ι V).hom h) =
    CategoryTheory.CategoryStruct.comp
      (AlgebraicGeometry.Scheme.Hom.isoImage ((TopologicalSpace.Opens.map f.base).obj U).ι
          ((TopologicalSpace.Opens.map (f ∣_ U).base).obj V)).hom
      (CategoryTheory.CategoryStruct.comp (X.homOfLE ⋯)
        (CategoryTheory.CategoryStruct.comp (f ∣_ (AlgebraicGeometry.Scheme.Hom.opensFunctor U.ι).obj V) h))
-- Init.Data.UInt.Lemmas
UInt8.sub_eq_iff_eq_add : ∀ {a b c : UInt8}, a - b = c ↔ a = c + b
-- Mathlib.CategoryTheory.Functor.FunctorHom
CategoryTheory.Functor.HomObj.ext : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {D : Type u'} {inst_1 : CategoryTheory.Category.{v', u'} D}
  {F G : CategoryTheory.Functor C D} {A : CategoryTheory.Functor C (Type w)} {x y : F.HomObj G A}, x.app = y.app → x = y
-- Mathlib.Topology.Algebra.MulAction
IsCompact.vadd_set : ∀ {M : Type u_1} {X : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace X] [inst_2 : VAdd M X]
  [ContinuousVAdd M X] {k : Set M} {u : Set X}, IsCompact k → IsCompact u → IsCompact (k +ᵥ u)
-- Mathlib.RingTheory.Polynomial.Pochhammer
/-- `ascPochhammer S n` is the polynomial `X * (X + 1) * ... * (X + n - 1)`,
with coefficients in the semiring `S`.
 -/
ascPochhammer : (S : Type u) → [inst : Semiring S] → ℕ → Polynomial S
-- Mathlib.SetTheory.Cardinal.Ordinal
Ordinal.IsInitial.isPrincipal_mul : ∀ {o : Ordinal.{u_1}}, o.IsInitial → Ordinal.omega0 ≤ o → Ordinal.IsPrincipal (fun x1 x2 => x1 * x2) o
-- Mathlib.Analysis.Polynomial.Norm
Polynomial.isGreatest_supNorm : ∀ {A : Type u_1} [inst : SeminormedRing A] (p : Polynomial A), IsGreatest (Set.range fun x => ‖p.coeff x‖) p.supNorm
-- Mathlib.GroupTheory.GroupAction.CardCommute
/-- **Class formula** for a finite group acting on a finite type.  -/
MulAction.card_eq_sum_card_group_div_card_stabilizer : ∀ (α : Type u_1) (β : Type u_2) [inst : Group α] [inst_1 : MulAction α β] [inst_2 : Fintype α] [inst_3 : Fintype β]
  [inst_4 : Fintype (Quotient (MulAction.orbitRel α β))] [inst_5 : (b : β) → Fintype ↥(MulAction.stabilizer α b)],
  Fintype.card β = ∑ ω, Fintype.card α / Fintype.card ↥(MulAction.stabilizer α ω.out)
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.isLE_iff_orthogonal : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} 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]
  (t : CategoryTheory.Triangulated.TStructure C) (n₀ n₁ : ℤ),
  n₀ + 1 = n₁ → ∀ (X : C), t.IsLE X n₀ ↔ ∀ (Y : C) (f : X ⟶ Y), t.IsGE Y n₁ → f = 0
-- Mathlib.Algebra.Homology.DerivedCategory.HomologySequence
DerivedCategory.homologyFunctorFactors_hom_naturality_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] {K L : CochainComplex C ℤ} (f : K ⟶ L) (n : ℤ) {Z : C}
  (h : (HomologicalComplex.homologyFunctor C (ComplexShape.up ℤ) n).obj L ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((DerivedCategory.homologyFunctor C n).map (DerivedCategory.Q.map f))
      (CategoryTheory.CategoryStruct.comp ((DerivedCategory.homologyFunctorFactors C n).hom.app L) h) =
    CategoryTheory.CategoryStruct.comp ((DerivedCategory.homologyFunctorFactors C n).hom.app K)
      (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap f n) h)
-- Lean.Data.Lsp.Internal
Lean.Lsp.instToJsonLeanImportClosureParams : Lean.ToJson Lean.Lsp.LeanImportClosureParams
-- Lean.Meta.Match.Basic
Lean.Meta.Match.counterExampleToMessageData : Lean.Meta.Match.CounterExample → Lean.MessageData
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.contractibleTriangle_obj₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C] (X : C),
  (CategoryTheory.Pretriangulated.contractibleTriangle X).obj₂ = X