mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Localization.Bousfield
CategoryTheory.ObjectProperty.galoisConnection_isColocal : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C],
  GaloisConnection (⇑OrderDual.toDual ∘ CategoryTheory.ObjectProperty.isColocal)
    (CategoryTheory.MorphismProperty.isColocal ∘ ⇑OrderDual.ofDual)
-- Init.Grind.AC
Lean.Grind.AC.instReprExpr.repr : Lean.Grind.AC.Expr → ℕ → Std.Format
-- Mathlib.Order.Filter.ENNReal
ENNReal.ofReal_limsup_toReal : ∀ {α : Type u_1} {f : Filter α} [f.NeBot] {u : α → ENNReal} {C : NNReal},
  (∀ᶠ (a : α) in f, u a ≤ ↑C) → ENNReal.ofReal (Filter.limsup (fun a => (u a).toReal) f) = Filter.limsup u f
-- Mathlib.Analysis.Normed.Ring.Lemmas
/-- A seminormed ring is a topological ring.  -/
NonUnitalSeminormedRing.toIsTopologicalRing : ∀ {α : Type u_1} [inst : NonUnitalSeminormedRing α], IsTopologicalRing α
-- Mathlib.Probability.Moments.Basic
ProbabilityTheory.mgf_neg : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t : ℝ},
  ProbabilityTheory.mgf (-X) μ t = ProbabilityTheory.mgf X μ (-t)
-- Mathlib.Probability.Independence.Kernel.Indep
ProbabilityTheory.Kernel.Indep.indepSets : ∀ {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω}
  {μ : MeasureTheory.Measure α} {s1 s2 : Set (Set Ω)},
  ProbabilityTheory.Kernel.Indep (MeasurableSpace.generateFrom s1) (MeasurableSpace.generateFrom s2) κ μ →
    ProbabilityTheory.Kernel.IndepSets s1 s2 κ μ
-- Mathlib.LinearAlgebra.Matrix.Hadamard
Matrix.hadamard_zero : ∀ {α : Type u_1} {m : Type u_2} {n : Type u_3} (A : Matrix m n α) [inst : MulZeroClass α], A.hadamard 0 = 0
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrpObj.lift_comp_neg_right_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {A B : C} [inst_2 : CategoryTheory.AddGrpObj B] (f : A ⟶ B) {Z : C} (h : B ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CartesianMonoidalCategory.lift f
        (CategoryTheory.CategoryStruct.comp f CategoryTheory.AddGrpObj.neg))
      (CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit A)
      (CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.zero h)
-- Mathlib.Tactic.Peel
Mathlib.Tactic.Peel.eventually_congr : ∀ {α : Type u_1} {p q : α → Prop} {f : Filter α},
  (∀ (x : α), p x ↔ q x) → ((∀ᶠ (x : α) in f, p x) ↔ ∀ᶠ (x : α) in f, q x)
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
AddEquiv.toContinuousAddEquiv_symm_apply : ∀ {G : Type u} [inst : TopologicalSpace G] {H : Type v} [inst_1 : TopologicalSpace H] [inst_2 : Add G] [inst_3 : Add H]
  (e : G ≃+ H) (he : ∀ (s : Set H), IsOpen (⇑e ⁻¹' s) ↔ IsOpen s) (a : H), (e.toContinuousAddEquiv he).symm a = e.symm a
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.MonoidalOpposite.mop.injEq : ∀ {C : Type u₁} (unmop unmop_1 : C), ({ unmop := unmop } = { unmop := unmop_1 }) = (unmop = unmop_1)
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.getKey!_modifyKey : ∀ {α : Type u} {β : Type v} [inst : BEq α] [EquivBEq α] [inst_2 : Inhabited α] {k k' : α} {f : β → β}
  (l : List ((_ : α) × β)),
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.getKey! k' (Std.Internal.List.Const.modifyKey k f l) =
      if (k == k') = true then if Std.Internal.List.containsKey k l = true then k else default
      else Std.Internal.List.getKey! k' l
-- Mathlib.Topology.Order.IntermediateValue
isPreconnected_uIoc : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLinearOrder α] [OrderTopology α]
  [DenselyOrdered α] {a b : α}, IsPreconnected (Set.uIoc a b)
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableEquiv.piUnique_apply : ∀ {δ' : Type u_5} (π : δ' → Type u_6) [inst : (x : δ') → MeasurableSpace (π x)] [inst_1 : Unique δ'],
  ⇑(MeasurableEquiv.piUnique π) = fun f => f default
-- Mathlib.Analysis.Convex.Exposed
IsExposed.inter_left : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : TopologicalSpace 𝕜] [inst_1 : Ring 𝕜] [inst_2 : PartialOrder 𝕜]
  [inst_3 : AddCommMonoid E] [inst_4 : TopologicalSpace E] [inst_5 : Module 𝕜 E] {A B C : Set E},
  IsExposed 𝕜 A C → C ⊆ B → IsExposed 𝕜 (A ∩ B) C
-- Mathlib.RingTheory.IsTensorProduct
/-- Suppose `f : M →ₗ[R] N` is the base change of `M` along `R → S`. Then any `R`-linear map from
`M` to an `S`-module factors through `f`.  -/
IsBaseChange.lift : {R : Type u_1} →
  {M : Type v₁} →
    {N : Type v₂} →
      {S : Type v₃} →
        [inst : AddCommMonoid M] →
          [inst_1 : AddCommMonoid N] →
            [inst_2 : CommSemiring R] →
              [inst_3 : CommSemiring S] →
                [inst_4 : Algebra R S] →
                  [inst_5 : Module R M] →
                    [inst_6 : Module R N] →
                      [inst_7 : Module S N] →
                        [inst_8 : IsScalarTower R S N] →
                          {f : M →ₗ[R] N} →
                            IsBaseChange S f →
                              {Q : Type u_3} →
                                [inst_9 : AddCommMonoid Q] →
                                  [inst_10 : Module S Q] →
                                    [inst_11 : Module R Q] → [IsScalarTower R S Q] → (M →ₗ[R] Q) → N →ₗ[S] Q
-- Mathlib.Topology.MetricSpace.DilationEquiv
DilationEquiv.coe_symm_toHomeomorph : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] (e : X ≃ᵈ Y),
  ⇑e.toHomeomorph.symm = ⇑e.symm
-- Init.Data.Nat.Basic
_private.Init.Data.Nat.Basic.0.Nat.beq.match_1.eq_2 : ∀ (motive : ℕ → ℕ → Sort u_1) (n : ℕ) (h_1 : Unit → motive Nat.zero Nat.zero) (h_2 : (n : ℕ) → motive Nat.zero n.succ)
  (h_3 : (n : ℕ) → motive n.succ Nat.zero) (h_4 : (n m : ℕ) → motive n.succ m.succ),
  (match Nat.zero, n.succ with
    | Nat.zero, Nat.zero => h_1 ()
    | Nat.zero, n.succ => h_2 n
    | n.succ, Nat.zero => h_3 n
    | n.succ, m.succ => h_4 n m) =
    h_2 n
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.MonoidalOpposite.mop_injective : ∀ {C : Type u₁}, Function.Injective CategoryTheory.MonoidalOpposite.mop
-- Mathlib.Algebra.Group.Units.Defs
AddGroup.isAddUnit : ∀ {α : Type u} [inst : AddGroup α] (a : α), IsAddUnit a
-- Mathlib.CategoryTheory.Bicategory.Coherence
CategoryTheory.FreeBicategory.quot_whisker_left : ∀ {B : Type u} [inst : Quiver B] {a b c : CategoryTheory.FreeBicategory B} (f : a ⟶ b) {g h : b ⟶ c}
  (η : CategoryTheory.FreeBicategory.Hom₂ g h),
  Quot.mk CategoryTheory.FreeBicategory.Rel (CategoryTheory.FreeBicategory.Hom₂.whisker_left f η) =
    CategoryTheory.Bicategory.whiskerLeft f (Quot.mk CategoryTheory.FreeBicategory.Rel η)
-- Mathlib.RingTheory.Localization.AtPrime.Basic
Localization.instFaithfulSMulAtPrimeOfNoZeroDivisors : ∀ {R : Type u_4} [inst : CommRing R] [NoZeroDivisors R] (P : Ideal R) [hp : P.IsPrime],
  FaithfulSMul R (Localization.AtPrime P)
-- Mathlib.Data.Finset.Image
Finset.mem_map' : ∀ {α : Type u_1} {β : Type u_2} (f : α ↪ β) {a : α} {s : Finset α}, f a ∈ Finset.map f s ↔ a ∈ s
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.mem_def : ∀ {α : Type u_1} {cmp : α → α → Ordering} {x : α} {t : RBTree.RBNode α},
  RBTree.RBNode.Mem cmp x t ↔ ∃ y ∈ t, cmp x y = Ordering.eq
-- Mathlib.Combinatorics.Additive.AP.Three.Defs
threeAPFree_insert_of_lt : ∀ {α : Type u_2} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [IsOrderedCancelAddMonoid α] {s : Set α} {a : α},
  (∀ i ∈ s, i < a) →
    (ThreeAPFree (insert a s) ↔ ThreeAPFree s ∧ ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → a + c = b + b → a = b)
-- Mathlib.Data.QPF.Multivariate.Constructions.Quot
/-- `Quot1` is a QPF  -/
MvQPF.relQuot : {n : ℕ} →
  {F : TypeVec.{u} n → Type u} →
    (R : ⦃α : TypeVec.{u} n⦄ → F α → F α → Prop) →
      [q : MvQPF F] →
        (∀ ⦃α β : TypeVec.{u} n⦄ (a b : F α) (f : α.Arrow β), R a b → R (MvFunctor.map f a) (MvFunctor.map f b)) →
          MvQPF (MvQPF.Quot1 R)
-- Mathlib.LinearAlgebra.Quotient.Defs
Submodule.Quotient.mk_smul : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (p : Submodule R M)
  {S : Type u_3} [inst_3 : SMul S R] [inst_4 : SMul S M] [inst_5 : IsScalarTower S R M] (r : S) (x : M),
  Submodule.Quotient.mk (r • x) = r • Submodule.Quotient.mk x
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getEntryGE?.go.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α) (best : Option ((a : α) × β a)),
  Std.DTreeMap.Internal.Impl.getEntryGE?.go k best Std.DTreeMap.Internal.Impl.leaf = best
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.mapLeftIso_inverse_map_right : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  (R : CategoryTheory.Functor B T) {P : CategoryTheory.MorphismProperty T} {Q : CategoryTheory.MorphismProperty A}
  {W : CategoryTheory.MorphismProperty B} [inst_3 : Q.IsMultiplicative] [inst_4 : W.IsMultiplicative]
  {L₁ L₂ : CategoryTheory.Functor A T} [inst_5 : P.RespectsIso] [inst_6 : Q.RespectsIso] [inst_7 : W.RespectsIso]
  (e : L₁ ≅ L₂) {X Y : CategoryTheory.MorphismProperty.Comma L₂ R P Q W} (f : X ⟶ Y),
  ((CategoryTheory.MorphismProperty.Comma.mapLeftIso R e).inverse.map f).right =
    (CategoryTheory.MorphismProperty.Comma.Hom.hom f).right
-- Init.Data.Range.Polymorphic.RangeIterator
Std.Rxi.Iterator.isPlausibleSuccessorOf_iff : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] {it' it : Std.Iter α},
  it'.IsPlausibleSuccessorOf it ↔ ∃ a, it.internalState.next = some a ∧ Std.PRange.succ? a = it'.internalState.next
-- Mathlib.Algebra.Category.Ring.Colimits
CommRingCat.Colimits.Relation.mul_assoc : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CommRingCat}
  (x y z : CommRingCat.Colimits.Prequotient F), CommRingCat.Colimits.Relation F ((x.mul y).mul z) (x.mul (y.mul z))
-- Mathlib.Algebra.Lie.Weights.Basic
/-- **Alias** of `FunLike.coe_zero`. -/
LieModule.Weight.coe_zero : ∀ {F : Type u_3} {α : Type u_5} {β : Type u_6} [inst : FunLike F α β] [inst_1 : Zero F] [inst_2 : Zero β]
  [IsZeroApply F α β], ⇑0 = 0
-- Mathlib.CategoryTheory.Monad.Products
CategoryTheory.algebraEquivUnder_inverse : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : C) [inst_1 : CategoryTheory.Limits.HasBinaryCoproducts C],
  (CategoryTheory.algebraEquivUnder X).inverse = CategoryTheory.underToAlgebra X
-- LeanSearchClient.Syntax
LeanSearchClient.searchCommandImpl : Lean.Elab.Command.CommandElab
-- Mathlib.GroupTheory.Sylow
Sylow.toSubgroup : {p : ℕ} → {G : Type u_1} → [inst : Group G] → Sylow p G → Subgroup G
-- Lean.Expr
/-- Given `f a₁ ... aᵢ`, returns true if `f` is a constant
with name `n` and has the correct number of arguments.
 -/
Lean.Expr.isAppOfArity : Lean.Expr → Lean.Name → ℕ → Bool
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getD_erase_self : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α],
  m.WF → ∀ {k : α} {fallback : β k}, (m.erase k).getD k fallback = fallback
-- Lean.Meta.Tactic.Grind.Types
/-- A mapping from each function application index (`HeadIndex`) to a list of applications with that index.
Recall that the `HeadIndex` for a constant is its constant name, and for a free variable,
it is its unique id.
 -/
Lean.Meta.Grind.GoalState.appMap : Lean.Meta.Grind.GoalState → Lean.PHashMap Lean.HeadIndex (List Lean.Expr)
-- Init.Data.Int.LemmasAux
Int.min_self_assoc' : ∀ {m n : ℤ}, min n (min m n) = min n m
-- Mathlib.Analysis.LocallyConvex.AbsConvexOpen
AbsConvexOpenSets.coe_zero_mem : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : TopologicalSpace E] [inst_1 : AddCommMonoid E] [inst_2 : SeminormedRing 𝕜]
  [inst_3 : SMul 𝕜 E] [inst_4 : PartialOrder 𝕜] (s : AbsConvexOpenSets 𝕜 E), 0 ∈ ↑s
-- Mathlib.RingTheory.Finiteness.Finsupp
FreeAbelianGroup.instFG : ∀ {σ : Type u_1} [Finite σ], AddMonoid.FG (FreeAbelianGroup σ)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.mem_toArray_iff_getKey?_eq_some_and_get?_eq_some : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [EquivBEq α] [LawfulHashable α],
  (↑m).WF →
    ∀ {k : α} {v : β},
      (k, v) ∈ Std.DHashMap.Raw.Const.toArray ↑m ↔
        m.getKey? k = some k ∧ Std.DHashMap.Internal.Raw₀.Const.get? m k = some v
-- Init.Data.UInt.Lemmas
USize.toFin_ofNatLT : ∀ {n : ℕ} (hn : n < USize.size), (USize.ofNatLT n hn).toFin = ⟨n, hn⟩
-- Init.Data.Int.Linear
Int.Internal.Linear.instLawfulBEqPoly : LawfulBEq Int.Internal.Linear.Poly
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Algebra.adjoin_eq : ∀ {R : Type uR} {A : Type uA} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (S : Subalgebra R A),
  Algebra.adjoin R ↑S = S
-- Init.Data.List.Basic
List.set.eq_2 : ∀ {α : Type u_1} (x a : α) (as : List α) (n : ℕ), (a :: as).set n.succ x = a :: as.set n x
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.mem_keysArray : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [LawfulBEq α] {k : α},
  m.WF → (k ∈ m.keysArray ↔ k ∈ m)
-- Mathlib.AlgebraicGeometry.Morphisms.Smooth
AlgebraicGeometry.instSmoothResLE : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (U : X.Opens) (V : Y.Opens)
  (e : U ≤ (TopologicalSpace.Opens.map f.base).obj V) [AlgebraicGeometry.Smooth f],
  AlgebraicGeometry.Smooth (AlgebraicGeometry.Scheme.Hom.resLE f V U e)
-- Lean.Meta.Tactic.AuxLemma
Lean.Meta.AuxLemmaKey.mk : Lean.Expr → Bool → Bool → Lean.Meta.AuxLemmaKey
-- Mathlib.Algebra.RingQuot
RingQuot.instMul : {R : Type uR} → [inst : Semiring R] → (r : R → R → Prop) → Mul (RingQuot r)
-- Mathlib.Combinatorics.Graph.Basic
Graph.Compatible.refl : ∀ {α : Type u_1} {β : Type u_2} (G : Graph α β), G.Compatible G
-- Mathlib.AlgebraicGeometry.Sites.AffineEtale
/-- The category of sheaves on the small affine étale site is equivalent to the category of
sheaves on the small étale site.  -/
AlgebraicGeometry.Scheme.AffineEtale.sheafEquiv : (S : AlgebraicGeometry.Scheme) →
  (A : Type u') →
    [inst : CategoryTheory.Category.{u, u'} A] →
      [CategoryTheory.Limits.HasLimits A] →
        CategoryTheory.Sheaf (AlgebraicGeometry.Scheme.AffineEtale.topology S) A ≌
          CategoryTheory.Sheaf S.smallEtaleTopology A
-- Mathlib.Algebra.Group.Submonoid.Membership
AddSubmonoid.isAddCommutative_iSup : ∀ {M : Type u_1} [inst : AddZeroClass M] {ι : Sort u_4} [Nonempty ι] {S : ι → AddSubmonoid M}
  [hS : ∀ (i : ι), IsAddCommutative ↥(S i)], Directed (fun x1 x2 => x1 ≤ x2) S → IsAddCommutative ↥(⨆ i, S i)
-- Mathlib.Analysis.InnerProductSpace.GramMatrix
/-- In a normed space, positive definiteness of `gram 𝕜 v` implies linear independence of `v`.  -/
Matrix.linearIndependent_of_posDef_gram : ∀ {E : Type u_1} {n : Type u_2} {𝕜 : Type u_4} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [Finite n] {v : n → E}, (Matrix.gram 𝕜 v).PosDef → LinearIndependent 𝕜 v
-- Mathlib.CategoryTheory.Sites.SheafCohomology.Basic
CategoryTheory.Sheaf.instSubsingletonHHAddNatOfNat : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  [inst_1 : CategoryTheory.HasSheafify J AddCommGrpCat]
  [inst_2 : CategoryTheory.HasExt (CategoryTheory.Sheaf J AddCommGrpCat)] (F : CategoryTheory.Sheaf J AddCommGrpCat)
  {n : ℕ} [CategoryTheory.Injective F], Subsingleton (F.H (n + 1))
-- Mathlib.Algebra.Group.Pi.Basic
Sum.elim_mulSingle_one : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : DecidableEq α] [inst_1 : DecidableEq β] [inst_2 : One γ] (i : α)
  (c : γ), Sum.elim (Pi.mulSingle i c) 1 = Pi.mulSingle (Sum.inl i) c
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
/-- Naturality of the `prodComparison` morphism in the left argument.  -/
CategoryTheory.CartesianMonoidalCategory.prodComparison_natural_whiskerRight : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₁} [inst_2 : CategoryTheory.Category.{v₁, u₁} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  (F : CategoryTheory.Functor C D) {A B A' : C} (f : A ⟶ A'),
  CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategoryStruct.whiskerRight f B))
      (CategoryTheory.CartesianMonoidalCategory.prodComparison F A' B) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.prodComparison F A B)
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (F.map f) (F.obj B))
-- Lean.Data.Lsp.Diagnostics
Lean.Lsp.instToJsonDiagnosticCode : Lean.ToJson Lean.Lsp.DiagnosticCode
-- Mathlib.GroupTheory.GroupAction.Hom
VAddAssocClass.vaddHomClass : ∀ (M' : Type u_1) (X : Type u_5) [inst : VAdd M' X] (Y : Type u_6) [inst_1 : VAdd M' Y] (F : Type u_8)
  [inst_2 : FunLike F X Y] [inst_3 : AddZeroClass X] [inst_4 : VAdd X Y] [VAddAssocClass M' X Y]
  [AddActionHomClass F X X Y], AddActionHomClass F M' X Y
-- Init.Data.Ord.Basic
_private.Init.Data.Ord.Basic.0.List.compareLex.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → List α → Sort u_2) (h_1 : Unit → motive [] []) (h_2 : (x : List α) → motive [] x)
  (h_3 : (x : List α) → motive x [])
  (h_4 : (x : α) → (xs : List α) → (y : α) → (ys : List α) → motive (x :: xs) (y :: ys)),
  (match [], [] with
    | [], [] => h_1 ()
    | [], x => h_2 x
    | x, [] => h_3 x
    | x :: xs, y :: ys => h_4 x xs y ys) =
    h_1 ()
-- Mathlib.Algebra.Ring.Subsemiring.Pointwise
/-- The action on a subsemiring corresponding to applying the action to every element.

This is available as an instance in the `Pointwise` locale.  -/
Subsemiring.pointwiseMulAction : {M : Type u_1} →
  {R : Type u_2} → [inst : Monoid M] → [inst_1 : Semiring R] → [MulSemiringAction M R] → MulAction M (Subsemiring R)
-- Mathlib.Order.Lattice
eq_of_inf_eq_sup_eq : ∀ {α : Type u} [inst : DistribLattice α] {a b c : α}, b ⊓ a = c ⊓ a → b ⊔ a = c ⊔ a → b = c
-- Mathlib.RingTheory.WittVector.Basic
WittVector.ghostEquiv_coe : ∀ (p : ℕ) (R : Type u_1) [inst : CommRing R] [inst_1 : Fact (Nat.Prime p)] [inst_2 : Invertible ↑p],
  ↑(WittVector.ghostEquiv p R) = WittVector.ghostMap
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.inl_mul : ∀ {R : Type u} (M : Type v) [inst : Monoid R] [inst_1 : AddMonoid M] [inst_2 : DistribMulAction R M]
  [inst_3 : DistribMulAction Rᵐᵒᵖ M] (r₁ r₂ : R),
  TrivSqZeroExt.inl (r₁ * r₂) = TrivSqZeroExt.inl r₁ * TrivSqZeroExt.inl r₂
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get!_map : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {γ : Type w} {t : Std.DTreeMap α (fun x => β) cmp}
  [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [inst : Inhabited γ] {f : α → β → γ} {k : α},
  Std.DTreeMap.Const.get! (Std.DTreeMap.map f t) k = (Option.map (f k) (Std.DTreeMap.Const.get? t k)).get!
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
CochainComplex.mappingCone.liftCocycle_coe : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] {K : CochainComplex C ℤ}
  {n m : ℤ} (α : CochainComplex.HomComplex.Cocycle K F m) (β : CochainComplex.HomComplex.Cochain K G n) (h : n + 1 = m)
  (eq : CochainComplex.HomComplex.δ n m β + (↑α).comp (CochainComplex.HomComplex.Cochain.ofHom φ) ⋯ = 0),
  ↑(CochainComplex.mappingCone.liftCocycle φ α β h eq) = CochainComplex.mappingCone.liftCochain φ (↑α) β h
-- Lean.Data.PersistentHashMap
Lean.PersistentHashMap.findEntryAtAux : {α : Type u_1} →
  {β : Type u_2} → [BEq α] → (keys : Array α) → (vals : Array β) → keys.size = vals.size → ℕ → α → Option (α × β)
-- Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
/-- A countable set of sets that generate the measurable space.
We insert `∅` to ensure it is nonempty.  -/
MeasurableSpace.countableGeneratingSet : (α : Type u_3) → [inst : MeasurableSpace α] → [h : MeasurableSpace.CountablyGenerated α] → Set (Set α)
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHom_def' : ∀ {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] [inst_2 : CategoryTheory.MonoidalCategory C]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D] {x₁ y₁ : D} {x₂ y₂ : C} (f : x₁ ⟶ y₁)
  (g : x₂ ⟶ y₂),
  CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHom f g =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight x₁ g)
      (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft f y₂)
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
IntermediateField.instIsScalarTowerSubtypeMemSubalgebraAdjoinSingletonSetAdjoinCoeRingHomAlgebraMap : ∀ {A : Type u_3} {B : Type u_4} {C : Type u_5} [inst : Field A] [inst_1 : CommSemiring B] [inst_2 : Field C]
  [inst_3 : Algebra A B] [inst_4 : Algebra B C] [inst_5 : Algebra A C] [inst_6 : IsScalarTower A B C] (b : B),
  IsScalarTower (↥A[b]) (↥A⟮(algebraMap B C) b⟯) C
-- Mathlib.SetTheory.Ordinal.FundamentalSequence
Ordinal.IsFundamentalSequence.lt : ∀ {a o : Ordinal.{u_1}} {s : (p : Ordinal.{u_1}) → p < o → Ordinal.{u_1}},
  a.IsFundamentalSequence o s → ∀ {p : Ordinal.{u_1}} (hp : p < o), s p hp < a
-- Mathlib.CategoryTheory.Triangulated.Functor
CategoryTheory.Functor.mapTriangleCommShiftIso_hom_app_hom₃ : ∀ {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] [inst_2 : CategoryTheory.HasShift C ℤ]
  [inst_3 : CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [inst_4 : F.CommShift ℤ]
  [inst_5 : CategoryTheory.Preadditive C] [inst_6 : CategoryTheory.Preadditive D] [inst_7 : F.Additive] (n : ℤ)
  (X : CategoryTheory.Pretriangulated.Triangle C),
  ((F.mapTriangleCommShiftIso n).hom.app X).hom₃ = (CategoryTheory.Functor.commShiftIso F n).hom.app X.obj₃
-- Mathlib.NumberTheory.NumberField.Completion.FinitePlace
/-- **Alias** of `NumberField.HeightOneSpectrum.adicAbv`.

---

The `v`-adic absolute value on `K` defined as the norm of `v` raised to negative `v`-adic
valuation  -/
NumberField.HeightOneSpectrum.NumberField.RingOfIntegers.HeightOneSpectrum.adicAbv : (K : Type u_1) →
  [inst : Field K] →
    {R : Type u_2} →
      [inst_1 : CommRing R] →
        [inst_2 : Algebra R K] →
          [IsDedekindDomain R] →
            [IsFractionRing R K] →
              IsDedekindDomain.HeightOneSpectrum R → [Module.Finite ℤ R] → [Module.Free ℤ R] → AbsoluteValue K ℝ
-- Mathlib.LinearAlgebra.RootSystem.Reduced
RootPairing.isReduced_iff' : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N),
  P.IsReduced ↔ ∀ (i j : ι), i ≠ j → ¬LinearIndependent R ![P.root i, P.root j] → P.root i = -P.root j
-- Mathlib.Algebra.Lie.Weights.Chain
LieModule.eventually_genWeightSpace_smul_add_eq_bot : ∀ {R : Type u_1} {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (M : Type u_3)
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L] (χ₁ χ₂ : L → R) [IsAddTorsionFree R] [IsDomain R] [Module.IsTorsionFree R M]
  [IsNoetherian R M], χ₁ ≠ 0 → ∀ᶠ (k : ℕ) in Filter.atTop, LieModule.genWeightSpace M (k • χ₁ + χ₂) = ⊥
-- Mathlib.Analysis.Calculus.FDeriv.Mul
fderiv_inverse : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {R : Type u_5} [inst_1 : NormedRing R] [HasSummableGeomSeries R]
  [inst_3 : NormedAlgebra 𝕜 R] (x : Rˣ), fderiv 𝕜 Ring.inverse ↑x = -((ContinuousLinearMap.mulLeftRight 𝕜 R) ↑x⁻¹) ↑x⁻¹
-- Mathlib.RingTheory.LocalIso
Algebra.IsLocalIso.iff_span_isStandardOpenImmersion_eq_top : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S],
  Algebra.IsLocalIso R S ↔ Ideal.span {g | Algebra.IsStandardOpenImmersion R (Localization.Away g)} = ⊤
-- Lean.Data.Lsp.Diagnostics
Lean.Lsp.instOrdDiagnosticTag.ord : Lean.Lsp.DiagnosticTag → Lean.Lsp.DiagnosticTag → Ordering