mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.mem_alter : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β}
  [inst_2 : EquivBEq α] [LawfulHashable α] {k k' : α} {f : Option β → Option β},
  m.WF →
    (k' ∈ Std.DHashMap.Raw.Const.alter m k f ↔
      if (k == k') = true then (f (Std.DHashMap.Raw.Const.get? m k)).isSome = true else k' ∈ m)
-- Mathlib.CategoryTheory.Limits.Shapes.Preorder.WellOrderContinuous
CategoryTheory.Functor.IsWellOrderContinuous.nonempty_isColimit : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {J : Type w} {inst_1 : PartialOrder J}
  {F : CategoryTheory.Functor J C} [self : F.IsWellOrderContinuous] (m : J),
  Order.IsSuccLimit m → Nonempty (CategoryTheory.Limits.IsColimit ((Set.principalSegIio m).cocone F))
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.walkingParallelPairOp_one : CategoryTheory.Limits.walkingParallelPairOp.obj CategoryTheory.Limits.WalkingParallelPair.one =
  Opposite.op CategoryTheory.Limits.WalkingParallelPair.zero
-- Init.MacroTrace
Lean.«termMacro.trace[_]_» : Lean.ParserDescr
-- Mathlib.Algebra.GroupWithZero.Units.Basic
zpow_natCast_sub_one₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {a : G₀}, a ≠ 0 → ∀ (n : ℕ), a ^ (↑n - 1) = a ^ n / a
-- Mathlib.Algebra.FreeAbelianGroup.Finsupp
FreeAbelianGroup.equivFinsupp_apply : ∀ (X : Type u_1) (a : FreeAbelianGroup X), (FreeAbelianGroup.equivFinsupp X) a = FreeAbelianGroup.toFinsupp a
-- Lean.Environment
Lean.PersistentEnvExtensionDescrCore : Type → Type → Type → Type
-- Mathlib.Algebra.Lie.Normalizer
LieSubalgebra.le_normalizer : ∀ {R : Type u_1} {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  (H : LieSubalgebra R L), H ≤ H.normalizer
-- Mathlib.Analysis.InnerProductSpace.Defs
/-- Local notation for `RCLike.ext_iff 𝕜`  -/
_private.Mathlib.Analysis.InnerProductSpace.Defs.0.InnerProductSpace.Core.termExt_iff : Lean.ParserDescr
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.L1.setToL1_simpleFunc_indicatorConst : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_4 : CompleteSpace F] {T : Set α → E →L[ℝ] F} {C : ℝ} (hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
  {s : Set α} (hs : MeasurableSet s) (hμs : μ s < ⊤) (x : E),
  (MeasureTheory.L1.setToL1 hT) ↑(MeasureTheory.Lp.simpleFunc.indicatorConst 1 hs ⋯ x) = (T s) x
-- Mathlib.Algebra.Order.Interval.Set.Group
Set.inv_mem_Ioo_iff : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] {a c d : α},
  a⁻¹ ∈ Set.Ioo c d ↔ a ∈ Set.Ioo d⁻¹ c⁻¹
-- Mathlib.Tactic.ClickSuggestions.FindPremises
/-- Push the discrimination tree entry `key => a` onto the array.  -/
_private.Mathlib.Tactic.ClickSuggestions.FindPremises.0.Mathlib.Tactic.ClickSuggestions.pushEntry : {α : Type} →
  Array (Lean.Meta.RefinedDiscrTree.Key × Lean.Meta.RefinedDiscrTree.LazyEntry × α) →
    Lean.Expr → α → Lean.MetaM (Array (Lean.Meta.RefinedDiscrTree.Key × Lean.Meta.RefinedDiscrTree.LazyEntry × α))
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStruct
SSet.Edge.InvStruct.invStructId_inv : ∀ {X : SSet} (x : X.obj (Opposite.op { len := 0 })), (SSet.Edge.InvStruct.invStructId x).inv = SSet.Edge.id x
-- Mathlib.Algebra.Group.Commute.Units
Commute.units_val : ∀ {M : Type u_1} [inst : Monoid M] {u₁ u₂ : Mˣ}, Commute u₁ u₂ → Commute ↑u₁ ↑u₂
-- Mathlib.LinearAlgebra.AffineSpace.Defs
/-- An `AddTorsor G P` gives a structure to the nonempty type `P`,
acted on by an `AddGroup G` with a transitive and free action given
by the `+ᵥ` operation and a corresponding subtraction given by the
`-ᵥ` operation. In the case of a vector space, it is an affine
space.  -/
Affine.termAffineSpace : Lean.ParserDescr
-- Mathlib.Topology.Order.LowerUpperTopology
Topology.IsLower.tendsto_nhds_iff_lt : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [Topology.IsLower α] {β : Type u_3} {f : β → α}
  {l : Filter β} {x : α}, Filter.Tendsto f l (nhds x) ↔ ∀ (y : α), x < y → ∀ᶠ (z : β) in l, f z < y
-- Mathlib.Algebra.Order.Group.Defs
le_neg_self_iff : ∀ {α : Type u} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [IsOrderedAddMonoid α] {a : α}, a ≤ -a ↔ a ≤ 0
-- Mathlib.Tactic.Linarith.Lemmas
Mathlib.Tactic.Linarith.add_neg : ∀ {α : Type u} [inst : Semiring α] [inst_1 : PartialOrder α] [IsStrictOrderedRing α] {a b : α},
  a < 0 → b < 0 → a + b < 0
-- Mathlib.Data.Multiset.AddSub
Multiset.card_erase_eq_ite : ∀ {α : Type u_1} [inst : DecidableEq α] {a : α} {s : Multiset α},
  (s.erase a).card = if a ∈ s then s.card.pred else s.card
-- Mathlib.Combinatorics.Quiver.ConnectedComponent
Quiver.IsSStronglyConnected.exists_pos_cycle : ∀ (V : Type u_2) [inst : Quiver V], Quiver.IsSStronglyConnected V → ∀ (i : V), ∃ p, 0 < p.length
-- Mathlib.Order.Bounds.Image
IsGreatest.isLeast_image2 : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ] {f : α → β → γ}
  {s : Set α} {t : Set β} {a : α} {b : β},
  (∀ (b : β), Antitone (Function.swap f b)) →
    (∀ (a : α), Antitone (f a)) → IsGreatest s a → IsGreatest t b → IsLeast (Set.image2 f s t) (f a b)
-- Mathlib.CategoryTheory.Monoidal.End
CategoryTheory.equivOfTensorIsoUnit_counitIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {M : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} M]
  [inst_2 : CategoryTheory.MonoidalCategory M] (F : CategoryTheory.Functor M (CategoryTheory.Functor C C)) (m n : M)
  (h₁ : CategoryTheory.MonoidalCategoryStruct.tensorObj m n ≅ CategoryTheory.MonoidalCategoryStruct.tensorUnit M)
  (h₂ : CategoryTheory.MonoidalCategoryStruct.tensorObj n m ≅ CategoryTheory.MonoidalCategoryStruct.tensorUnit M)
  (H :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight h₁.hom m)
        (CategoryTheory.MonoidalCategoryStruct.leftUnitor m).hom =
      CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator m n m).hom
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft m h₂.hom)
          (CategoryTheory.MonoidalCategoryStruct.rightUnitor m).hom))
  [inst_3 : F.Monoidal],
  (CategoryTheory.equivOfTensorIsoUnit F m n h₁ h₂ H).counitIso = CategoryTheory.unitOfTensorIsoUnit F n m h₂
-- Mathlib.RingTheory.OrderOfVanishing.Noetherian
/-- In a discrete valuation ring, `ord R x` is the same as `addVal R x`. We prefer the second spelling
here for most purposes.
 -/
Ring.ord_eq_addVal : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsDiscreteValuationRing R] (x : R),
  Ring.ord R x = (IsDiscreteValuationRing.addVal R) x
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.mem_erase : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {k a : α}, a ∈ m.erase k ↔ (k == a) = false ∧ a ∈ m
-- Mathlib.Topology.Semicontinuity.Defs
LowerSemicontinuousOn.mono : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : Preorder β] {f : α → β} {s t : Set α},
  LowerSemicontinuousOn f s → t ⊆ s → LowerSemicontinuousOn f t
-- Init.Data.List.Monadic
List.zipWithM.eq_1 : ∀ {m : Type u → Type v} [inst : Monad m] {α : Type w} {β : Type x} {γ : Type u} (f : α → β → m γ) (as : List α)
  (bs : List β), List.zipWithM f as bs = List.zipWithM.loop f as bs #[]
-- Lean.Meta.Sym.ExprPtr
Lean.Meta.Sym.ExprPtr.mk.sizeOf_spec : ∀ (expr : Lean.Expr), sizeOf { expr := expr } = 1 + sizeOf expr
-- Mathlib.Data.Set.Lattice.Image
Set.sInter_prod : ∀ {α : Type u_1} {β : Type u_2} {S : Set (Set α)}, S.Nonempty → ∀ (t : Set β), ⋂₀ S ×ˢ t = ⋂ s ∈ S, s ×ˢ t
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem_modify_self : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [inst_2 : EquivBEq α]
  [inst_3 : LawfulHashable α] {k : α} {f : β → β} (h : m.WF) {hc : k ∈ m.modify k f}, (m.modify k f)[k] = f m[k]
-- Mathlib.Algebra.Star.LinearMap
Pi.intrinsicStar_comul_commSemiring : ∀ {R : Type u_5} [inst : CommSemiring R] [inst_1 : StarRing R] {n : Type u_8} [inst_2 : DecidableEq n]
  [inst_3 : Fintype n],
  star (WithConv.toConv CoalgebraStruct.comul) =
    WithConv.toConv (↑(TensorProduct.comm R (n → R) (n → R)) ∘ₗ CoalgebraStruct.comul)
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Pretrivialization.symm_apply_apply : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  (e : Bundle.Pretrivialization F proj) {x : Z}, x ∈ e.source → ↑e.symm (↑e x) = x
-- Mathlib.Analysis.Normed.Group.Submodule
/-- A submodule of a seminormed group is also a seminormed group, with the restriction of the norm.
 -/
Submodule.seminormedAddCommGroup : {𝕜 : Type u_1} →
  {E : Type u_2} →
    [inst : Ring 𝕜] →
      [inst_1 : SeminormedAddCommGroup E] → [inst_2 : Module 𝕜 E] → (s : Submodule 𝕜 E) → SeminormedAddCommGroup ↥s
-- Mathlib.CategoryTheory.Action
CategoryTheory.ActionCategory.uncurry_map : ∀ {X : Type u} {G : Type u_2} [inst : Group G] [inst_1 : MulAction G X] {H : Type u_3} [inst_2 : Group H]
  (F : G →* (X → H) ⋊[mulAutArrow] G) (sane : ∀ (g : G), (F g).right = g) {x b : CategoryTheory.ActionCategory G X}
  (f : x ⟶ b), (CategoryTheory.ActionCategory.uncurry F sane).map f = (F ↑f).left b.back
-- Mathlib.Analysis.SpecialFunctions.Bernstein
bernsteinApproximation.apply_one : ∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : TopologicalSpace E] [inst_2 : IsTopologicalAddGroup E]
  [inst_3 : Module ℝ E] [inst_4 : ContinuousSMul ℝ E] {n : ℕ},
  n ≠ 0 → ∀ (f : C(↑unitInterval, E)), (bernsteinApproximation n f) 1 = f 1
-- Std.Internal.UV.System
Std.Internal.UV.System.CPUTimes.nice : Std.Internal.UV.System.CPUTimes → UInt64
-- Mathlib.Combinatorics.Graph.Basic
Graph.Inc.eq_or_eq_of_isLink : ∀ {α : Type u_1} {β : Type u_2} {x y z : α} {e : β} {G : Graph α β}, G.Inc e x → G.IsLink e y z → x = y ∨ x = z
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
NumberField.mixedEmbedding.fundamentalCone.intNorm_idealSetEquiv_apply : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K]
  {J : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))}
  (a : ↑(NumberField.mixedEmbedding.fundamentalCone.idealSet K J)),
  ↑(NumberField.mixedEmbedding.fundamentalCone.intNorm
        ↑((NumberField.mixedEmbedding.fundamentalCone.idealSetEquiv K J) a)) =
    NumberField.mixedEmbedding.norm ↑a
-- Mathlib.Algebra.Group.Even
isSquare_subset_image_isSquare : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : MulOneClass α] [inst_1 : MulOneClass β] [inst_2 : FunLike F α β]
  [MonoidHomClass F α β] {f : F}, Function.Surjective ⇑f → {b | IsSquare b} ⊆ ⇑f '' {a | IsSquare a}
-- Mathlib.RingTheory.MvPowerSeries.Substitution
MvPowerSeries.HasSubst.mul_right : ∀ {σ : Type u_1} {τ : Type u_4} {S : Type u_5} [inst : CommRing S] (b : σ → MvPowerSeries τ S)
  {a : σ → MvPowerSeries τ S}, MvPowerSeries.HasSubst a → MvPowerSeries.HasSubst (a * b)
-- Mathlib.CategoryTheory.Pi.Monoidal
/-- The counit for the adjunction `tensorLeft X ⊣ ihom X`.  -/
CategoryTheory.Pi.closedCounit : {I : Type w₁} →
  {C : I → Type u₁} →
    [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] →
      [inst_1 : (i : I) → CategoryTheory.MonoidalCategory (C i)] →
        [inst_2 : (i : I) → CategoryTheory.MonoidalClosed (C i)] →
          (X : (i : I) → C i) →
            (CategoryTheory.Pi.ihom X).comp (CategoryTheory.MonoidalCategory.tensorLeft X) ⟶
              CategoryTheory.Functor.id ((i : I) → C i)
-- Lean.Elab.Tactic.Grind.Config
_private.Lean.Elab.Tactic.Grind.Config.0.Lean.Elab.Tactic.instEvalExprConfigInteractive : Lean.Elab.ConfigEval.EvalExpr Lean.Grind.ConfigInteractive
-- Mathlib.Data.Opposite
Opposite.unop_surjective : ∀ {α : Sort u}, Function.Surjective Opposite.unop
-- Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
AffineBasis.finiteDimensional : ∀ {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [inst : AddCommGroup V] [inst_1 : AddTorsor V P]
  [inst_2 : DivisionRing k] [inst_3 : Module k V] [Finite ι] (b : AffineBasis ι k P), FiniteDimensional k V
-- Mathlib.GroupTheory.Exponent
/-- Any additive group of exponent two is abelian.  -/
addCommMonoidOfExponentTwo : {G : Type u} → [inst : AddMonoid G] → [IsCancelAdd G] → AddMonoid.exponent G = 2 → AddCommMonoid G
-- Mathlib.Logic.Small.List
smallVector : ∀ {α : Type v} {n : ℕ} [Small.{u, v} α], Small.{u, v} (List.Vector α n)
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.values.eq_2 : ∀ {α : Type u} {β : Type v} (fst : α) (v : β) (l : List ((_ : α) × β)),
  Std.Internal.List.values (⟨fst, v⟩ :: l) = v :: Std.Internal.List.values l
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.instInvolutiveStarOfContinuousStar : {α : Type u_1} →
  [inst : MeasurableSpace α] →
    {μ : MeasureTheory.Measure α} →
      {R : Type u_5} →
        [inst_1 : TopologicalSpace R] → [inst_2 : InvolutiveStar R] → [ContinuousStar R] → InvolutiveStar (α →ₘ[μ] R)
-- Mathlib.Analysis.Calculus.Deriv.Shift
/-- Translation in the domain does not change the derivative.  -/
HasDerivAt.comp_const_sub : ∀ {𝕜 : Type u_1} {F : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} (a x : 𝕜),
  HasDerivAt f f' (a - x) → HasDerivAt (fun x => f (a - x)) (-f') x
-- Mathlib.Analysis.Normed.Ring.Lemmas
Filter.isBoundedUnder_le_mul_tendsto_zero : ∀ {α : Type u_1} {ι : Type u_3} [inst : NonUnitalSeminormedRing α] {f g : ι → α} {l : Filter ι},
  Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l (norm ∘ f) →
    Filter.Tendsto g l (nhds 0) → Filter.Tendsto (fun x => f x * g x) l (nhds 0)
-- Mathlib.MeasureTheory.Group.Action
MeasureTheory.measurePreserving_vadd : ∀ {M : Type v} {α : Type w} {m : MeasurableSpace α} [inst : VAdd M α] [MeasurableConstVAdd M α] (c : M)
  (μ : MeasureTheory.Measure α) [MeasureTheory.VAddInvariantMeasure M α μ],
  MeasureTheory.MeasurePreserving (fun x => c +ᵥ x) μ μ
-- Mathlib.LinearAlgebra.Matrix.Adjugate
Matrix.adjugate_reindex : ∀ {m : Type u} {n : Type v} {α : Type w} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : DecidableEq m]
  [inst_3 : Fintype m] [inst_4 : CommRing α] (e : m ≃ n) (A : Matrix m m α),
  ((Matrix.reindex e e) A).adjugate = (Matrix.reindex e e) A.adjugate
-- Mathlib.Data.Sign.Basic
self_mul_sign : ∀ {α : Type u} [inst : Ring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] (x : α), x * ↑(SignType.sign x) = |x|
-- Init.Data.UInt.Bitwise
UInt8.and_assoc : ∀ (a b c : UInt8), a &&& b &&& c = a &&& (b &&& c)
-- Mathlib.CategoryTheory.Monoidal.Category
/-- In a monoidal category, we can take the tensor product of objects, `X ⊗ Y` and of morphisms
`f ⊗ₘ g`.
Tensor product does not need to be strictly associative on objects, but there is a
specified associator, `α_ X Y Z : (X ⊗ Y) ⊗ Z ≅ X ⊗ (Y ⊗ Z)`. There is a tensor unit `𝟙_ C`,
with specified left and right unitor isomorphisms `λ_ X : 𝟙_ C ⊗ X ≅ X` and `ρ_ X : X ⊗ 𝟙_ C ≅ X`.
These associators and unitors satisfy the pentagon and triangle equations.  -/
CategoryTheory.MonoidalCategory : (C : Type u) → [𝒞 : CategoryTheory.Category.{v, u} C] → Type (max u v)
-- Mathlib.Algebra.Group.Units.Opposite
AddUnits.coe_opEquiv_symm : ∀ {M : Type u_2} [inst : AddMonoid M] (u : (AddUnits M)ᵃᵒᵖ),
  ↑(AddUnits.opEquiv.symm u) = AddOpposite.op ↑(AddOpposite.unop u)
-- Mathlib.Tactic.Translate.ToDual
/-- `to_dual_name_hint src₁ tgt₁, ..., srcₙ tgtₙ` lets `to_dual` translate between the name segments
`srcᵢ` and `tgtᵢ` for the rest of the file current. The name segments should be capitalized.  -/
Mathlib.Tactic.ToDual.«commandTo_dual_name_hint__,,» : Lean.ParserDescr
-- Std.Data.Internal.List.Associative
Std.Internal.List.maxKeyD_eq_iff_mem_and_forall : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  [Std.LawfulEqOrd α] {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    l.isEmpty = false →
      ∀ {km fallback : α},
        Std.Internal.List.maxKeyD l fallback = km ↔
          Std.Internal.List.containsKey km l = true ∧
            ∀ (k : α), Std.Internal.List.containsKey k l = true → (compare k km).isLE = true
-- Mathlib.Order.SuccPred.Basic
Order.le_pred_iff_eq_bot : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : PredOrder α] {a : α} [inst_2 : OrderBot α], a ≤ Order.pred a ↔ a = ⊥
-- Mathlib.Data.Finset.SDiff
Finset.union_eq_sdiff_union_sdiff_union_inter : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Finset α), s ∪ t = s \ t ∪ t \ s ∪ s ∩ t
-- Mathlib.Tactic.DepRewrite
Mathlib.Tactic.DepRewrite.heqL : ∀ {α β : Sort u} {a : α} {b : β} (h : a ≍ b), a = cast ⋯ b
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.normal_addSubgroupOf_iff : ∀ {G : Type u_1} [inst : AddGroup G] {H K : AddSubgroup G},
  H ≤ K → ((H.addSubgroupOf K).Normal ↔ ∀ (h k : G), h ∈ H → k ∈ K → k + h + -k ∈ H)
-- Init.Data.UInt.Lemmas
UInt8.toNat_toUInt16 : ∀ (x : UInt8), x.toUInt16.toNat = x.toNat
-- Mathlib.CategoryTheory.Sites.Sieves
/-- Uncurry a presieve to one set over the sigma type.  -/
CategoryTheory.Presieve.uncurry : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] → {X : C} → CategoryTheory.Presieve X → Set ((Y : C) × (Y ⟶ X))
-- Init.Data.Iterators.Consumers.Monadic.Loop
/-- Folds a monadic function over an iterator from the left, accumulating a value starting with `init`.
The accumulated value is combined with the each element of the list in order, using `f`.

The monadic effects of `f` are interleaved with potential effects caused by the iterator's step
function. Therefore, it may *not* be equivalent to `it.toList.foldlM`.

This function is deprecated. Instead of `it.allowNontermination.foldM`, use `it.foldM`.
 -/
Std.IterM.Partial.foldM : {m n : Type w → Type w'} →
  [Monad n] →
    {α β γ : Type w} →
      [inst : Std.Iterator α m β] →
        [Std.IteratorLoop α m n] → [MonadLiftT m n] → (γ → β → n γ) → γ → Std.IterM.Partial m β → n γ
-- Mathlib.Algebra.Order.Group.Abs
abs_sub_pos : ∀ {G : Type u_1} [inst : AddCommGroup G] [inst_1 : LinearOrder G] [IsOrderedAddMonoid G] {a b : G}, 0 < |a - b| ↔ a ≠ b
-- Mathlib.Tactic.IntervalCases
/-- Given `a, b, a', p` where `p` proves `a ≱ b` and `a' := a+1`, prove `a' ≤ b`.  -/
Mathlib.Tactic.IntervalCases.Methods.roundUp : Mathlib.Tactic.IntervalCases.Methods → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr
-- Batteries.Recycling.RBTree.Basic
/-- `O(log n)`. Remove an element `k` from the map.  -/
RBTree.RBMap.erase : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → RBTree.RBMap α β cmp → α → RBTree.RBMap α β cmp
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgEquiv.arrowCongr_comp : ∀ {R : Type u_1} {A₁ : Type u_2} {A₂ : Type u_3} {A₃ : Type u_4} {A₁' : Type u_5} {A₂' : Type u_6} {A₃' : Type u_7}
  [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Semiring A₂] [inst_3 : Semiring A₃] [inst_4 : Semiring A₁']
  [inst_5 : Semiring A₂'] [inst_6 : Semiring A₃'] [inst_7 : Algebra R A₁] [inst_8 : Algebra R A₂]
  [inst_9 : Algebra R A₃] [inst_10 : Algebra R A₁'] [inst_11 : Algebra R A₂'] [inst_12 : Algebra R A₃']
  [inst_13 : Star A₁] [inst_14 : Star A₂] [inst_15 : Star A₃] [inst_16 : Star A₁'] [inst_17 : Star A₂']
  [inst_18 : Star A₃'] (e₁ : A₁ ≃⋆ₐ[R] A₁') (e₂ : A₂ ≃⋆ₐ[R] A₂') (e₃ : A₃ ≃⋆ₐ[R] A₃') (f : A₁ →⋆ₐ[R] A₂)
  (g : A₂ →⋆ₐ[R] A₃), (e₁.arrowCongr e₃) (g.comp f) = ((e₂.arrowCongr e₃) g).comp ((e₁.arrowCongr e₂) f)
-- Mathlib.ModelTheory.Types
FirstOrder.Language.Theory.CompleteType.instNonempty : ∀ {L : FirstOrder.Language} {α : Type w}, Nonempty (∅.CompleteType α)
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.inv_def : ∀ {K : Type u_1} [inst : CommRing K] [inst_1 : IsDomain K] (x : RatFunc K),
  x.inv =
    match x with
    | { toFractionRing := p } => { toFractionRing := p⁻¹ }
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
/-- For `x : prime ideal of A`, `HomogeneousLocalization 𝒜 x` is `NumDenSameDeg 𝒜 x` modulo the
kernel of `embedding 𝒜 x`. This is essentially the subring of `Aₓ` where the numerator and
denominator share the same grading.
 -/
HomogeneousLocalization : {ι : Type u_1} →
  {A : Type u_2} → {σ : Type u_3} → [inst : CommRing A] → [SetLike σ A] → (ι → σ) → Submonoid A → Type (max u_1 u_2)
-- Init.PropLemmas
Exists.imp : ∀ {α : Sort u_1} {p q : α → Prop}, (∀ (a : α), p a → q a) → (∃ a, p a) → ∃ a, q a
-- Mathlib.Topology.Constructions
Continuous.restrictPreimage : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y} {s : Set Y},
  Continuous f → Continuous (s.restrictPreimage f)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.mulMon_k : ℤ → Lean.Grind.CommRing.Mon → Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly
-- Mathlib.Algebra.Order.Group.Multiset
/-- `Multiset.map` as an `AddMonoidHom`.  -/
Multiset.mapAddMonoidHom : {α : Type u_1} → {β : Type u_2} → (α → β) → Multiset α →+ Multiset β
-- Mathlib.Geometry.Euclidean.Angle.Sphere
/-- Given two points on a circle, the center of that circle may be expressed explicitly as a
multiple (by half the tangent of the angle between the chord and the radius at one of those
points) of a `π / 2` rotation of the vector between those points, plus the midpoint of those
points.  -/
EuclideanGeometry.Sphere.tan_div_two_smul_rotation_pi_div_two_vadd_midpoint_eq_center : ∀ {V : Type u_3} {P : Type u_4} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {s : EuclideanGeometry.Sphere P} {p₁ p₂ : P},
  p₁ ∈ s →
    p₂ ∈ s →
      p₁ ≠ p₂ →
        ((EuclideanGeometry.oangle p₂ p₁ s.center).tan / 2) •
              (EuclideanGeometry.o.rotation ↑(Real.pi / 2)) (p₂ -ᵥ p₁) +ᵥ
            midpoint ℝ p₁ p₂ =
          s.center
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.le_mul : ∀ {α : Type u_1} [inst : Lean.Grind.CommRing α] [inst_1 : LE α] [inst_2 : LT α] [inst_3 : Std.IsPreorder α]
  [Lean.Grind.OrderedRing α] (ctx : Lean.Grind.CommRing.Context α) (p₁ : Lean.Grind.CommRing.Poly) (k : ℤ)
  (p : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.mul_ineq_cert p₁ k p = true →
    Lean.Grind.CommRing.Poly.denote ctx p₁ ≤ 0 → Lean.Grind.CommRing.Poly.denote ctx p ≤ 0
-- Mathlib.MeasureTheory.SetSemiring
MeasureTheory.IsSetRing.disjointed_mem : ∀ {α : Type u_1} {C : Set (Set α)} {ι : Type u_2} [inst : Preorder ι] [inst_1 : LocallyFiniteOrderBot ι],
  MeasureTheory.IsSetRing C → ∀ {s : ι → Set α}, (∀ (j : ι), s j ∈ C) → ∀ (i : ι), disjointed s i ∈ C
-- Lean.Meta.Sym.AlphaShareCommon
_private.Lean.Meta.Sym.AlphaShareCommon.0.Lean.Meta.Sym.shareCommonAlphaInc.go : Lean.Expr → Lean.Meta.Sym.AlphaShareCommonM Lean.Expr
-- Std.Time.DateTime
/-- Returns the local (civil) date of the `DateTime` as a `Day.Offset` relative to 1970-01-01.
 -/
Std.Time.DateTime.toEpochDay : Std.Time.DateTime → Std.Time.Day.Offset
-- Mathlib.NumberTheory.LucasLehmer
/-- Generalization of `sModNat` with arbitrary base case,
useful for proving `sModNatTR` and `sModNat` agree.
 -/
LucasLehmer.norm_num_ext.sModNatAux : ℕ → ℕ → ℕ → ℕ
-- Mathlib.MeasureTheory.Constructions.BorelSpace.ContinuousLinearMap
ContinuousLinearMap.measurable_coe : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_4} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : MeasurableSpace F] [BorelSpace F], Measurable fun f x => f x
-- Mathlib.Algebra.Module.Submodule.Bilinear
Submodule.map₂_le_map₂ : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : Module R P] {f : M →ₗ[R] N →ₗ[R] P} {p₁ p₂ : Submodule R M} {q₁ q₂ : Submodule R N},
  p₁ ≤ p₂ → q₁ ≤ q₂ → Submodule.map₂ f p₁ q₁ ≤ Submodule.map₂ f p₂ q₂
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Equiv.Perm.IsCycleOn.of_pow : ∀ {α : Type u_2} {f : Equiv.Perm α} {s : Set α} {n : ℕ}, (f ^ n).IsCycleOn s → Set.BijOn (⇑f) s s → f.IsCycleOn s