mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.minView!.match_1.eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : Std.DTreeMap.Internal.Impl α β → Sort u_3)
  (h_1 : Unit → motive Std.DTreeMap.Internal.Impl.leaf)
  (h_2 :
    (size : ℕ) →
      (k' : α) →
        (v' : β k') →
          (l' r' : Std.DTreeMap.Internal.Impl α β) → motive (Std.DTreeMap.Internal.Impl.inner size k' v' l' r')),
  (match Std.DTreeMap.Internal.Impl.leaf with
    | Std.DTreeMap.Internal.Impl.leaf => h_1 ()
    | Std.DTreeMap.Internal.Impl.inner size k' v' l' r' => h_2 size k' v' l' r') =
    h_1 ()
-- Mathlib.Algebra.BigOperators.ModEq
Nat.sum_modEq_ite : ∀ {α : Type u_1} {n : ℕ} {f : α → ℕ} [inst : DecidableEq α] {s : Finset α} {a : α},
  (∀ x ∈ s, x ≠ a → f x ≡ 0 [MOD n]) → ∑ x ∈ s, f x ≡ if a ∈ s then f a else 0 [MOD n]
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.isEmpty_modify : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α]
  (m : Std.DHashMap.Internal.Raw₀ α fun x => β),
  (↑m).WF → ∀ {k : α} {f : β → β}, (↑(Std.DHashMap.Internal.Raw₀.Const.modify m k f)).isEmpty = (↑m).isEmpty
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey!_eq_of_contains : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [LawfulBEq α]
  [inst_3 : Inhabited α], m.WF → ∀ {k : α}, m.contains k = true → m.getKey! k = k
-- Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
Bundle.Trivialization.localFrame_apply_of_notMem : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {M : Type u_4} [inst_1 : TopologicalSpace M] {F : Type u_5}
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace 𝕜 F] {V : M → Type u_6}
  [inst_4 : TopologicalSpace (Bundle.TotalSpace F V)] [inst_5 : (x : M) → AddCommGroup (V x)]
  [inst_6 : (x : M) → Module 𝕜 (V x)] [inst_7 : (x : M) → TopologicalSpace (V x)] [inst_8 : FiberBundle F V]
  [inst_9 : VectorBundle 𝕜 F V] {ι : Type u_7} {x : M} (e : Bundle.Trivialization F Bundle.TotalSpace.proj)
  [inst_10 : MemTrivializationAtlas e] (b : Module.Basis ι 𝕜 F) {i : ι}, x ∉ e.baseSet → e.localFrame b i x = 0
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.replace.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (a : α) (b : β a),
  Std.DHashMap.Internal.AssocList.replace a b Std.DHashMap.Internal.AssocList.nil = Std.DHashMap.Internal.AssocList.nil
-- Mathlib.Order.ModularLattice
IsModularLattice.mk : ∀ {α : Type u_2} [inst : Lattice α], (∀ {x : α} (y : α) {z : α}, x ≤ z → (x ⊔ y) ⊓ z ≤ x ⊔ y ⊓ z) → IsModularLattice α
-- Mathlib.Data.ENNReal.Basic
ENNReal.instSemilatticeSup : SemilatticeSup ENNReal
-- Init.Grind.Ring.CommSemiringAdapter
Lean.Grind.CommRing.Poly.insert.fun_cases_unfolding : ∀ (k : ℤ) (m : Lean.Grind.CommRing.Mon) (p : Lean.Grind.CommRing.Poly) (motive : Lean.Grind.CommRing.Poly → Prop),
  ((k == 0) = true → motive p) →
    ((k == 0) = false → (m == Lean.Grind.CommRing.Mon.unit) = true → motive (p.addConst k)) →
      ((k == 0) = false →
          (m == Lean.Grind.CommRing.Mon.unit) = false → motive (Lean.Grind.CommRing.Poly.insert.go k m p)) →
        motive (Lean.Grind.CommRing.Poly.insert k m p)
-- Mathlib.GroupTheory.Sylow
Sylow.card_eq_index_normalizer : ∀ {p : ℕ} {G : Type u_1} [inst : Group G] [Fact (Nat.Prime p)] [Finite (Sylow p G)] (P : Sylow p G),
  Nat.card (Sylow p G) = (Subgroup.normalizer ↑P).index
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
AffineSubspace.instNonemptySubtypeMemTop : ∀ (k : Type u_1) (V : Type u_2) (P : Type u_3) [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P], Nonempty ↥⊤
-- Init.Data.List.ToArray
_private.Init.Data.List.ToArray.0.List.getLast?.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (a : α) (as : List α) (h_1 : Unit → motive [])
  (h_2 : (a : α) → (as : List α) → motive (a :: as)),
  (match a :: as with
    | [] => h_1 ()
    | a :: as => h_2 a as) =
    h_2 a as
-- Mathlib.NumberTheory.NumberField.Units.Regulator
NumberField.Units.regOfFamily_ne_zero_iff : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K]
  {u : Fin (NumberField.Units.rank K) → (NumberField.RingOfIntegers K)ˣ},
  NumberField.Units.regOfFamily u ≠ 0 ↔ NumberField.Units.IsMaxRank u
-- Lean.Util.CollectAxioms
_private.Lean.Util.CollectAxioms.0.Lean.ExportedAxiomsState.mk.sizeOf_spec : ∀ (importedModuleEntries : Array (Array (Lean.Name × Array Lean.Name))),
  sizeOf { importedModuleEntries := importedModuleEntries } = 1 + sizeOf importedModuleEntries
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo
CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_inv_app_assoc : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] {F G : CategoryTheory.Pseudofunctor B CategoryTheory.Cat}
  (α : F ⟶ G) (a : B) (X : ↑(F.obj a)) {Z : ↑(G.obj a)}
  (h : (α.app a).toFunctor.obj ((F.map (CategoryTheory.CategoryStruct.id a)).toFunctor.obj X) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((α.naturality (CategoryTheory.CategoryStruct.id a)).inv.toNatTrans.app X) h =
    CategoryTheory.CategoryStruct.comp ((G.mapId a).hom.toNatTrans.app ((α.app a).toFunctor.obj X))
      (CategoryTheory.CategoryStruct.comp ((α.app a).toFunctor.map ((F.mapId a).inv.toNatTrans.app X)) h)
-- Mathlib.Topology.Sets.Compacts
/-- The product of two `TopologicalSpace.CompactOpens`, as a `TopologicalSpace.CompactOpens` in the
product space.  -/
TopologicalSpace.CompactOpens.instSProdProd : {α : Type u_1} →
  {β : Type u_2} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] →
        SProd (TopologicalSpace.CompactOpens α) (TopologicalSpace.CompactOpens β)
          (TopologicalSpace.CompactOpens (α × β))
-- Mathlib.Combinatorics.SimpleGraph.Bipartite
/-- The subgraph of `G` containing edges that connect a vertex in the set `s` to a vertex in the
set `t`.  -/
SimpleGraph.between : {V : Type u_1} → Set V → Set V → SimpleGraph V → SimpleGraph V
-- Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
NNReal.agm_comm : ∀ {x y : NNReal}, x.agm y = y.agm x
-- Mathlib.Algebra.Lie.Weights.Killing
LieModule.Weight.toLinear_neg : ∀ {K : Type u_2} {L : Type u_3} [inst : LieRing L] [inst_1 : Field K] [inst_2 : LieAlgebra K L]
  [inst_3 : FiniteDimensional K L] [inst_4 : LieAlgebra.IsKilling K L] {H : LieSubalgebra K L}
  [inst_5 : H.IsCartanSubalgebra] [inst_6 : LieModule.IsTriangularizable K (↥H) L] {α : LieModule.Weight K (↥H) L},
  LieModule.Weight.toLinear K (↥H) L (-α) = -LieModule.Weight.toLinear K (↥H) L α
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
OrthonormalBasis.tensorProduct.eq_1 : ∀ {𝕜 : 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] {ι₁ : Type u_6}
  {ι₂ : Type u_7} [inst_5 : Fintype ι₁] [inst_6 : Fintype ι₂] (b₁ : OrthonormalBasis ι₁ 𝕜 E)
  (b₂ : OrthonormalBasis ι₂ 𝕜 F), b₁.tensorProduct b₂ = (b₁.toBasis.tensorProduct b₂.toBasis).toOrthonormalBasis ⋯
-- Mathlib.LinearAlgebra.LinearIndependent.Lemmas
linearIndependent_finSucc : ∀ {K : Type u_3} {V : Type u} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {n : ℕ}
  {v : Fin (n + 1) → V},
  LinearIndependent K v ↔ LinearIndependent K (Fin.tail v) ∧ v 0 ∉ Submodule.span K (Set.range (Fin.tail v))
-- Mathlib.Order.SuccPred.Limit
PredOrder.prelimitRecOn_pred : ∀ {α : Type u_1} {motive : α → Sort u_2} [inst : LinearOrder α] [inst_1 : PredOrder α] [inst_2 : WellFoundedGT α]
  (pred : (a : α) → ¬IsMin a → motive a → motive (Order.pred a))
  (isPredPrelimit : (a : α) → Order.IsPredPrelimit a → ((b : α) → a < b → motive b) → motive a) [inst_3 : NoMinOrder α]
  (b : α),
  PredOrder.prelimitRecOn (Order.pred b) pred isPredPrelimit = pred b ⋯ (PredOrder.prelimitRecOn b pred isPredPrelimit)
-- Mathlib.Analysis.MellinTransform
/-- Suppose `f` is locally integrable on `(0, ∞)`, is `O(x ^ (-a))` as `x → ∞`, and is
`O(x ^ (-b))` as `x → 0`. Then its Mellin transform is differentiable on the domain `b < re s < a`.
 -/
mellin_differentiableAt_of_isBigO_rpow : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {a b : ℝ} {f : ℝ → E} {s : ℂ},
  MeasureTheory.LocallyIntegrableOn f (Set.Ioi 0) MeasureTheory.volume →
    (f =O[Filter.atTop] fun x => x ^ (-a)) →
      s.re < a → (f =O[nhdsWithin 0 (Set.Ioi 0)] fun x => x ^ (-b)) → b < s.re → DifferentiableAt ℂ (mellin f) s
-- Mathlib.Algebra.Homology.SpectralObject.Page
/-- The homology of the short complex `shortComplex` consisting of
two morphisms `X.δ`. In the documentation, we shorten it as `E^n₁(f₁, f₂, f₃)`  -/
CategoryTheory.Abelian.SpectralObject.E : {C : Type u_1} →
  {ι : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] →
        [inst_2 : CategoryTheory.Abelian C] →
          CategoryTheory.Abelian.SpectralObject C ι →
            {i j k l : ι} →
              (i ⟶ j) →
                (j ⟶ k) →
                  (k ⟶ l) →
                    (n₀ n₁ n₂ : ℤ) →
                      autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.E._auto_1 →
                        autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.E._auto_3 → C
-- Init.Data.Int.Gcd
Int.dvd_gcd_mul_iff_dvd_mul : ∀ {k n m : ℤ}, k ∣ ↑(k.gcd n) * m ↔ k ∣ n * m
-- Mathlib.LinearAlgebra.CrossProduct
/-- The three-dimensional vectors together with the operations + and ⨯₃ form a Lie ring.
Note we do not make this an instance as a conflicting one already exists
via `LieRing.ofAssociativeRing`.  -/
Cross.lieRing : {R : Type u_1} → [CommRing R] → LieRing (Fin 3 → R)
-- Mathlib.Order.Category.BoolAlg
/-- Constructs an equivalence between Boolean algebras from an order isomorphism between them.  -/
BoolAlg.Iso.mk : {α β : BoolAlg} → ↑α ≃o ↑β → (α ≅ β)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.reverse_append : ∀ {V : Type u} {G : SimpleGraph V} {u v w : V} (p : G.Walk u v) (q : G.Walk v w),
  (p.append q).reverse = q.reverse.append p.reverse
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.get?_insertMany_list_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {l : List α} {k : α},
  k ∈ t → (t.insertMany l).get? k = t.get? k
-- Mathlib.RingTheory.Perfectoid.FontaineTheta
WittVector.ghostComponentModPPow_map_mk : ∀ {R : Type u} [inst : CommRing R] {p : ℕ} [inst_1 : Fact (Nat.Prime p)] (n : ℕ) (x : WittVector p R),
  (WittVector.ghostComponentModPPow n) ((WittVector.map (Ideal.Quotient.mk (Ideal.span {↑p}))) x) =
    (Ideal.Quotient.mk (Ideal.span {↑p} ^ (n + 1))) ((WittVector.ghostComponent n) x)
-- Mathlib.Order.Interval.Finset.SuccPred
Finset.Ioo_succ_right_eq_Ioc : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : LocallyFiniteOrder α] [inst_2 : SuccOrder α] [NoMaxOrder α] (a b : α),
  Finset.Ioo a (Order.succ b) = Finset.Ioc a b
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instDistrib : {α : Type u_1} → {l : Filter α} → {R : Type u_5} → [Distrib R] → Distrib (l.Germ R)
-- Lean.Data.Lsp.TextSync
Lean.Lsp.instFromJsonDidOpenTextDocumentParams.fromJson : Lean.Json → Except String Lean.Lsp.DidOpenTextDocumentParams
-- Mathlib.LinearAlgebra.LinearPMap
/-- Auxiliary definition to unfold the existential quantifier.  -/
Submodule.valFromGraph : {R : Type u_1} →
  [inst : Ring R] →
    {E : Type u_4} →
      [inst_1 : AddCommGroup E] →
        [inst_2 : Module R E] →
          {F : Type u_5} →
            [inst_3 : AddCommGroup F] →
              [inst_4 : Module R F] →
                {g : Submodule R (E × F)} →
                  (∀ x ∈ g, x.1 = 0 → x.2 = 0) → {a : E} → a ∈ Submodule.map (LinearMap.fst R E F) g → F
-- Mathlib.RingTheory.TwoSidedIdeal.Operations
/-- Preimage of a two-sided ideal, as a two-sided ideal.  -/
TwoSidedIdeal.comap : {R : Type u_1} →
  {S : Type u_2} →
    [inst : NonUnitalNonAssocRing R] →
      [inst_1 : NonUnitalNonAssocRing S] →
        {F : Type u_3} →
          [inst_2 : FunLike F R S] → F → [NonUnitalRingHomClass F R S] → TwoSidedIdeal S →o TwoSidedIdeal R
-- Mathlib.GroupTheory.Congruence.Hom
/-- The natural homomorphism from a monoid to its quotient by a congruence relation is
surjective.  -/
Con.mk'_surjective : ∀ {M : Type u_1} [inst : MulOneClass M] {c : Con M}, Function.Surjective ⇑c.mk'
-- Mathlib.NumberTheory.Padics.RingHoms
PadicInt.norm_sub_zmodRepr_lt_one : ∀ {p : ℕ} [hp_prime : Fact (Nat.Prime p)] (x : ℤ_[p]), ‖x - ↑x.zmodRepr‖ < 1
-- Mathlib.Algebra.GroupWithZero.NonZeroDivisors
IsRightRegular.mem_nonZeroDivisorsRight : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] {r : M₀}, IsRightRegular r → r ∈ nonZeroDivisorsRight M₀
-- Mathlib.RingTheory.Jacobson.Polynomial
Ideal.jacobson_bot_polynomial_le_sInf_map_maximal : ∀ {R : Type u_1} [inst : CommRing R], ⊥.jacobson ≤ sInf (Ideal.map Polynomial.C '' {J | J.IsMaximal})
-- Mathlib.GroupTheory.Perm.Sign
Equiv.Perm.closure_isSwap : ∀ {α : Type u} [inst : DecidableEq α] [Finite α], Subgroup.closure {σ | σ.IsSwap} = ⊤
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace_map : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X.Hom Y), AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace.map f = f.toLRSHom
-- Lean.Meta.Tactic.LibrarySearch
_private.Lean.Meta.Tactic.LibrarySearch.0.Lean.Meta.LibrarySearch.librarySearch' : Lean.MVarId →
  (List Lean.MVarId → Lean.MetaM (List Lean.MVarId)) →
    (Lean.MVarId → Lean.MetaM Bool) →
      ℕ →
        optParam Bool true → optParam Bool false → Lean.MetaM (Option (Array (List Lean.MVarId × Lean.MetavarContext)))
-- Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
/-- **Alias** of `SimpleGraph.Walk.support_dropUntil_subset_support`. -/
SimpleGraph.Walk.support_dropUntil_subset : ∀ {V : Type u} {G : SimpleGraph V} {v w u : V} [inst : DecidableEq V] (p : G.Walk v w) (h : u ∈ p.support),
  (p.dropUntil u h).support ⊆ p.support
-- Init.Data.Array.MinMax
Array.min.congr_simp : ∀ {α : Type u_1} [inst : Min α] (arr arr_1 : Array α) (e_arr : arr = arr_1) (h : arr ≠ #[]), arr.min h = arr_1.min ⋯
-- Mathlib.Algebra.Category.Semigrp.Basic
/-- The type of morphisms in `MagmaCat R`.  -/
MagmaCat.Hom : MagmaCat → MagmaCat → Type u
-- ProofWidgets.Component.RefreshComponent
/-- The data used to call `awaitRefresh`, for updating the HTML display.  -/
ProofWidgets.RefreshComponent.AwaitRefreshParams : Type
-- Mathlib.LinearAlgebra.Dual.Lemmas
/-- For any finite-dimensional vector space, `dualAnnihilator` and `dualCoannihilator` give
an antitone order isomorphism between the subspaces in the vector space and the subspaces
in its dual.  -/
Subspace.orderIsoFiniteDimensional : {K : Type u_4} →
  {V : Type u_5} →
    [inst : Field K] →
      [inst_1 : AddCommGroup V] →
        [inst_2 : Module K V] → [FiniteDimensional K V] → Subspace K V ≃o (Subspace K (Module.Dual K V))ᵒᵈ
-- Std.Time.Format.Modifier
Std.Time.Modifier.w.injEq : ∀ (presentation presentation_1 : Std.Time.Number),
  (Std.Time.Modifier.w presentation = Std.Time.Modifier.w presentation_1) = (presentation = presentation_1)
-- Mathlib.LinearAlgebra.PerfectPairing.Basic
LinearMap.IsPerfectCompl.flip : ∀ {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} [inst_5 : p.IsPerfPair] {U : Submodule R M}
  {V : Submodule R N}, p.IsPerfectCompl U V → p.flip.IsPerfectCompl V U
-- Mathlib.Algebra.Homology.ShortComplex.Limits
CategoryTheory.ShortComplex.hasLimitsOfShape : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [CategoryTheory.Limits.HasLimitsOfShape J C], CategoryTheory.Limits.HasLimitsOfShape J (CategoryTheory.ShortComplex C)
-- Mathlib.Control.Monad.Cont
ContT.run_seqLeft : ∀ {r : Type u} {m : Type u → Type v} {α β : Type w} (x : ContT r m α) (y : ContT r m β) (k : α → m r),
  (x <* y).run k = x.run fun x => y.run fun x_1 => k x
-- Lean.Parser.Syntax
Lean.Parser.Command.infixr.formatter : Lean.PrettyPrinter.Formatter
-- Lean.Meta.WHNF
/-- Auxiliary method for reducing terms of the form `?m t_1 ... t_n` where `?m` is delayed assigned.
Recall that we can only expand a delayed assignment when all holes/metavariables in the assigned value have been "filled".
 -/
_private.Lean.Meta.WHNF.0.Lean.Meta.whnfDelayedAssigned? : Lean.Expr → Lean.Expr → Lean.MetaM (Option Lean.Expr)
-- Std.Data.ExtDTreeMap.Basic
/-- Transforms the tree map into a list of mappings in ascending order.  -/
Std.ExtDTreeMap.toList : {α : Type u} →
  {β : α → Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtDTreeMap α β cmp → List ((a : α) × β a)
-- Mathlib.Algebra.Module.Submodule.Lattice
Submodule.instMin : {R : Type u_1} →
  {M : Type u_3} → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → Min (Submodule R M)
-- Mathlib.RingTheory.Valuation.Basic
/-- The valuation of a sum is less than or equal to the maximum of the valuations.  -/
ValuationClass.map_add_le_max : ∀ {F : Type u_7} {R : outParam (Type u_5)} {Γ₀ : outParam (Type u_6)} {inst : LinearOrderedCommMonoidWithZero Γ₀}
  {inst_1 : Ring R} {inst_2 : FunLike F R Γ₀} [self : ValuationClass F R Γ₀] (f : F) (x y : R),
  f (x + y) ≤ max (f x) (f y)
-- Mathlib.NumberTheory.NumberField.Completion.Ramification
NumberField.InfinitePlace.inertiaDeg_eq_two : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  {v : NumberField.InfinitePlace K} {w : NumberField.InfinitePlace L},
  w ∈ NumberField.InfinitePlace.ramifiedPlacesOver L v → v.inertiaDeg w = 2
-- Mathlib.AlgebraicGeometry.Cover.Open
/-- The pullback of the affine refinement is the pullback of the affine cover.  -/
AlgebraicGeometry.Scheme.OpenCover.pullbackCoverAffineRefinementObjIso : {X Y : AlgebraicGeometry.Scheme} →
  (f : X ⟶ Y) →
    (𝒰 : Y.OpenCover) →
      (i : (CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f 𝒰.affineRefinement.openCover).I₀) →
        (CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f 𝒰.affineRefinement.openCover).X i ≅
          (CategoryTheory.Precoverage.ZeroHypercover.pullback₁ (AlgebraicGeometry.Scheme.Cover.pullbackHom 𝒰 f i.fst)
                (𝒰.X i.fst).affineCover).X
            i.snd
-- Mathlib.Data.List.Sort
List.sortedLT_reverse : ∀ {α : Type u_1} {l : List α} [inst : Preorder α], l.reverse.SortedLT ↔ l.SortedGT
-- Init.Data.Range.Polymorphic.RangeIterator
_private.Init.Data.Range.Polymorphic.RangeIterator.0.Std.Rxi.Iterator.instIteratorLoop.match_1.eq_1 : ∀ {α : Type u_1} [inst : Std.PRange.UpwardEnumerable α] {n : Type u_1 → Type u_3} (γ : Type u_1)
  (Pl : α → γ → ForInStep γ → Prop)
  (motive :
    (it : Std.IterM Id α) → ((b : α) → it.IsPlausibleIndirectOutput b → (c : γ) → n (Subtype (Pl b c))) → Sort u_2)
  (next : α)
  (f :
    (b : α) → { internalState := { next := some next } }.IsPlausibleIndirectOutput b → (c : γ) → n (Subtype (Pl b c)))
  (h_1 :
    (next : α) →
      (f :
          (b : α) →
            { internalState := { next := some next } }.IsPlausibleIndirectOutput b → (c : γ) → n (Subtype (Pl b c))) →
        motive { internalState := { next := some next } } f)
  (h_2 :
    (f : (b : α) → { internalState := { next := none } }.IsPlausibleIndirectOutput b → (c : γ) → n (Subtype (Pl b c))) →
      motive { internalState := { next := none } } f),
  (match { internalState := { next := some next } }, f with
    | { internalState := { next := some next } }, f => h_1 next f
    | { internalState := { next := none } }, f => h_2 f) =
    h_1 next f
-- Mathlib.GroupTheory.Focal
/-- The **Focal Subgroup** of a subgroup `H` (denoted `H*` or `foc(H)`).
It is generated by elements of the form `x⁻¹ * (u * x * u⁻¹)` where both `x` and `x^u` are in `H`.
 -/
Subgroup.focalSubgroup : {G : Type u_1} → [inst : Group G] → Subgroup G → Subgroup G
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.filter_equiv_self_iff : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  {f : α → Bool}, m.WF → ((Std.HashSet.Raw.filter f m).Equiv m ↔ ∀ (a : α) (h : a ∈ m), f (m.get a h) = true)
-- Mathlib.Data.Set.Lattice
Set.iInter_sigma' : ∀ {α : Type u_1} {β : Type u_2} {γ : α → Type u_12} (s : (i : α) → γ i → Set β), ⋂ i, ⋂ a, s i a = ⋂ ia, s ia.fst ia.snd
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.SInt
Int8.reduceAdd : Lean.Meta.Simp.DSimproc
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.ClientCapabilities.mk.inj : ∀ {textDocument? : Option Lean.Lsp.TextDocumentClientCapabilities} {window? : Option Lean.Lsp.WindowClientCapabilities}
  {workspace? : Option Lean.Lsp.WorkspaceClientCapabilities} {lean? : Option Lean.Lsp.LeanClientCapabilities}
  {textDocument?_1 : Option Lean.Lsp.TextDocumentClientCapabilities}
  {window?_1 : Option Lean.Lsp.WindowClientCapabilities} {workspace?_1 : Option Lean.Lsp.WorkspaceClientCapabilities}
  {lean?_1 : Option Lean.Lsp.LeanClientCapabilities},
  { textDocument? := textDocument?, window? := window?, workspace? := workspace?, lean? := lean? } =
      { textDocument? := textDocument?_1, window? := window?_1, workspace? := workspace?_1, lean? := lean?_1 } →
    textDocument? = textDocument?_1 ∧ window? = window?_1 ∧ workspace? = workspace?_1 ∧ lean? = lean?_1
-- Init.Data.String.Slice
_private.Init.Data.String.Slice.0.String.Slice.SplitInclusiveIterator.instIteratorId.match_3.eq_2 : ∀ {ρ : Type} {σ : String.Slice → Type} {pat : ρ} [inst : String.Slice.Pattern.ToForwardSearcher pat σ]
  {s : String.Slice} (motive : Std.IterM Id String.Slice → Sort u_1)
  (h_1 :
    (currPos : s.Pos) →
      (searcher : Std.Iter (String.Slice.Pattern.SearchStep s)) →
        motive { internalState := String.Slice.SplitInclusiveIterator.operating currPos searcher })
  (h_2 : Unit → motive { internalState := String.Slice.SplitInclusiveIterator.atEnd }),
  (match { internalState := String.Slice.SplitInclusiveIterator.atEnd } with
    | { internalState := String.Slice.SplitInclusiveIterator.operating currPos searcher } => h_1 currPos searcher
    | { internalState := String.Slice.SplitInclusiveIterator.atEnd } => h_2 ()) =
    h_2 ()
-- Mathlib.Data.Nat.Prime.Defs
Nat.minFac_eq_two_iff : ∀ (n : ℕ), n.minFac = 2 ↔ 2 ∣ n
-- Mathlib.Topology.Algebra.Group.Defs
Continuous.inv : ∀ {G : Type u_1} {X : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace G] [inst_2 : Inv G]
  [ContinuousInv G] {f : X → G}, Continuous f → Continuous f⁻¹
-- Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
/-- The `n`-th **Ruzsa-Szemerédi number** is the maximum number of edges a locally linear graph on
`n` vertices can have.

In other words, `ruzsaSzemerediNumberNat n` is the maximum number of edges a graph on `n` vertices
can have such that each edge belongs to exactly one triangle.  -/
ruzsaSzemerediNumberNat : ℕ → ℕ
-- Mathlib.Algebra.Order.Group.Cone
PartialOrder.mkOfAddGroupCone.eq_1 : ∀ {S : Type u_1} {G : Type u_2} [inst : AddCommGroup G] [inst_1 : SetLike S G] (C : S) [inst_2 : AddGroupConeClass S G],
  PartialOrder.mkOfAddGroupCone C =
    { le := fun a b => b - a ∈ C, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯, le_antisymm := ⋯ }
-- Mathlib.CategoryTheory.Monoidal.CommGrp_
CategoryTheory.Adjunction.mapCommGrp_counit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {D : Type u₂} [inst_3 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_4 : CategoryTheory.CartesianMonoidalCategory D] [inst_5 : CategoryTheory.BraidedCategory D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (a : F ⊣ G) [inst_6 : F.Braided]
  [inst_7 : G.Braided],
  a.mapCommGrp.counit =
    CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.mapCommGrpCompIso.inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.mapCommGrpNatTrans a.counit)
        CategoryTheory.Functor.mapCommGrpIdIso.hom)
-- Lean.ToExpr
Lean.instToExprInt32 : Lean.ToExpr Int32
-- Mathlib.Topology.DiscreteQuotient
DiscreteQuotient.trans : ∀ {X : Type u_2} [inst : TopologicalSpace X] (S : DiscreteQuotient X) (x y z : X),
  S.toSetoid x y → S.toSetoid y z → S.toSetoid x z