mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Elab.PreDefinition.PartialFixpoint.Eqns
_private.Lean.Elab.PreDefinition.PartialFixpoint.Eqns.0.Lean.Elab.PartialFixpoint.rwFixUnder : Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover
/-- Given a presheaf `F` on the topological space `X` and a presieve `R` whose generated sieve
is covering for the associated Grothendieck topology (equivalently, the presieve is covering
for the associated pretopology), the natural cone associated to `F` and the family of opens
associated to `R` is a limit cone iff the natural cone associated to `F` and the generated
sieve is a limit cone.
Since only the existence of a 1-1 correspondence will be used, the exact definition does
not matter, so tactics are used liberally.  -/
TopCat.Presheaf.isLimitOpensLeEquivGenerate₂ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {X : TopCat} →
      (F : TopCat.Presheaf C X) →
        {Y : TopologicalSpace.Opens ↑X} →
          (R : CategoryTheory.Presieve Y) →
            CategoryTheory.Sieve.generate R ∈ (Opens.grothendieckTopology ↑X) Y →
              CategoryTheory.Limits.IsLimit
                  (CategoryTheory.Functor.mapCone F
                    (TopCat.Presheaf.SheafCondition.opensLeCoverCocone (TopCat.Presheaf.coveringOfPresieve Y R)).op) ≃
                CategoryTheory.Limits.IsLimit
                  (CategoryTheory.Functor.mapCone F (CategoryTheory.Sieve.generate R).arrows.cocone.op)
-- Mathlib.Combinatorics.Enumerative.Composition
/-- Reverse the order of blocks in a composition.  -/
Composition.reverse : {n : ℕ} → Composition n → Composition n
-- Mathlib.CategoryTheory.Sites.Point.Basic
/-- If `Φ` is a point of a site and `F : A ⥤ B` is a functor which preserves
filtered colimits, then taking fibers of sheaves at `Φ` commutes with `F`.  -/
CategoryTheory.GrothendieckTopology.Point.sheafFiberCompIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      (Φ : J.Point) →
        {A : Type u'} →
          [inst_1 : CategoryTheory.Category.{v', u'} A] →
            {B : Type u''} →
              [inst_2 : CategoryTheory.Category.{v'', u''} B] →
                [inst_3 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] →
                  [inst_4 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v'', u''} B] →
                    (F : CategoryTheory.Functor A B) →
                      [CategoryTheory.LocallySmall.{w, v, u} C] →
                        [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', v'', u', u''} F] →
                          [inst_7 : J.HasSheafCompose F] →
                            (CategoryTheory.sheafCompose J F).comp Φ.sheafFiber ≅ Φ.sheafFiber.comp F
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.minD_eq_getD_toArray : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → ∀ {fallback : α}, t.minD fallback = t.toArray.getD 0 fallback
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKeyD_ofList_of_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {l : List ((a : α) × β a)}
  {k k' fallback : α},
  cmp k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬cmp a.fst b.fst = Ordering.eq) l →
      k ∈ List.map Sigma.fst l → (Std.ExtDTreeMap.ofList l cmp).getKeyD k' fallback = k
-- Lean.HeadIndex
Lean.HeadIndex.const.sizeOf_spec : ∀ (constName : Lean.Name), sizeOf (Lean.HeadIndex.const constName) = 1 + sizeOf constName
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.getD_erase : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {k a : α} {fallback : β},
  Std.ExtDTreeMap.Const.getD (t.erase k) a fallback =
    if cmp k a = Ordering.eq then fallback else Std.ExtDTreeMap.Const.getD t a fallback
-- Mathlib.Data.List.Nodup
List.Nodup.eq_of_head_mem_of_getLast_mem_of_infix : ∀ {α : Type u} {l₁ l₂ : List α},
  l₁ <:+: l₂ → ∀ {hne : l₂ ≠ []}, l₂.head hne ∈ l₁ → l₂.getLast hne ∈ l₁ → l₂.Nodup → l₁ = l₂
-- Mathlib.Topology.Algebra.Group.Basic
Filter.map_subRight_nhds : ∀ {G : Type w} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [IsTopologicalAddGroup G] {c a : G},
  Filter.map (fun x => x - c) (nhds a) = nhds (a - c)
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
/-- The type of morphisms for the diagram indexing reflexive (co)equalizers  -/
CategoryTheory.Limits.WalkingReflexivePair.Hom : CategoryTheory.Limits.WalkingReflexivePair → CategoryTheory.Limits.WalkingReflexivePair → Type
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
/-- Pairs `(x, n)` s.t. we have expanded the theorems
- `Int.Internal.Linear.ediv_emod`
- `Int.Internal.Linear.emod_nonneg`
- `Int.Internal.Linear.emod_le`
 -/
Lean.Meta.Grind.Arith.Cutsat.State.divMod : Lean.Meta.Grind.Arith.Cutsat.State → Lean.PHashSet (Lean.Expr × ℤ)
-- Lean.Server.Requests
Lean.Server.RequestM.mapRequestTaskCostly : {α : Type u_1} →
  {β : Type} →
    Lean.Server.RequestTask α → (α → Lean.Server.RequestM β) → Lean.Server.RequestM (Lean.Server.RequestTask β)
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
CochainComplex.mappingCocone.id_X : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} (φ : K ⟶ L) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] (p q : ℤ)
  (hpq : p + -1 = q),
  CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCocone.fst φ).f p)
        ((CochainComplex.mappingCocone.inl φ).v p p ⋯) +
      CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCocone.snd φ).v p q hpq)
        ((↑(CochainComplex.mappingCocone.inr φ)).v q p ⋯) =
    CategoryTheory.CategoryStruct.id ((CochainComplex.mappingCocone φ).X p)
-- Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
MeasureTheory.lpNorm_add_le : ∀ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] {f g : α → E},
  MeasureTheory.MemLp f p μ →
    1 ≤ p → MeasureTheory.lpNorm (f + g) p μ ≤ MeasureTheory.lpNorm f p μ + MeasureTheory.lpNorm g p μ
-- Mathlib.Geometry.Euclidean.Sphere.Tangent
EuclideanGeometry.Sphere.isTangent_of_mem_tangentsFrom : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {as : AffineSubspace ℝ P} {s : EuclideanGeometry.Sphere P} {p : P},
  as ∈ s.tangentsFrom p → s.IsTangent as
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2.Stmt.branch.inj : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} {a : σ → Bool} {a_1 a_2 : Turing.TM2.Stmt Γ Λ σ}
  {a_3 : σ → Bool} {a_4 a_5 : Turing.TM2.Stmt Γ Λ σ},
  Turing.TM2.Stmt.branch a a_1 a_2 = Turing.TM2.Stmt.branch a_3 a_4 a_5 → a = a_3 ∧ a_1 = a_4 ∧ a_2 = a_5
-- Mathlib.AlgebraicTopology.SimplicialSet.RelativeMorphism
SSet.RelativeMorphism.Homotopy.h₁ : ∀ {X Y : SSet} {A : X.Subcomplex} {B : Y.Subcomplex} {φ : A.toSSet ⟶ B.toSSet} {f g : SSet.RelativeMorphism A B φ}
  (self : f.Homotopy g), CategoryTheory.CategoryStruct.comp SSet.ι₁ self.h = g.map
-- Mathlib.MeasureTheory.Measure.FiniteMeasurePi
/-- The product of finitely many finite measures.  -/
MeasureTheory.FiniteMeasure.pi : {ι : Type u_1} →
  {α : ι → Type u_2} →
    [Fintype ι] →
      [inst : (i : ι) → MeasurableSpace (α i)] →
        ((i : ι) → MeasureTheory.FiniteMeasure (α i)) → MeasureTheory.FiniteMeasure ((i : ι) → α i)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.getKey_ofList_of_mem : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] {l : List (α × β)}
  {k k' : α},
  (k == k') = true →
    List.Pairwise (fun a b => (a.1 == b.1) = false) l →
      k ∈ List.map Prod.fst l →
        ∀ {h' : k' ∈ Std.DHashMap.Raw.Const.ofList l}, (Std.DHashMap.Raw.Const.ofList l).getKey k' h' = k
-- Mathlib.RingTheory.Ideal.Maps
RingHom.liftOfRightInverseAux.congr_simp : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} [inst : Ring A] [inst_1 : Ring B] [inst_2 : Ring C] (f f_1 : A →+* B)
  (e_f : f = f_1) (f_inv f_inv_1 : B → A) (e_f_inv : f_inv = f_inv_1) (hf : Function.RightInverse f_inv ⇑f)
  (g g_1 : A →+* C) (e_g : g = g_1) (hg : RingHom.ker f ≤ RingHom.ker g),
  f.liftOfRightInverseAux f_inv hf g hg = f_1.liftOfRightInverseAux f_inv_1 ⋯ g_1 ⋯
-- Mathlib.Tactic.Peel
/-- Applies a "peel theorem" with two main arguments, where the first is the new goal
and the second can be filled in using `e`. Then it intros two variables with the
provided names.

If, for example, `goal : ∃ y : α, q y` and `thm := Exists.imp`, the metavariable returned has
type `q x` where `x : α` has been introduced into the context.  -/
Mathlib.Tactic.Peel.applyPeelThm : Lean.Name →
  Lean.MVarId → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Name → Lean.Name → Lean.MetaM (Lean.FVarId × List Lean.MVarId)
-- Mathlib.Combinatorics.SimpleGraph.Paths
/-- **Alias** of `SimpleGraph.Walk.isCycle_map_iff_of_injective`. -/
SimpleGraph.Walk.map_isCycle_iff_of_injective : ∀ {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} {f : G →g G'} {u : V} {p : G.Walk u u},
  Function.Injective ⇑f → ((SimpleGraph.Walk.map f p).IsCycle ↔ p.IsCycle)
-- Mathlib.Topology.Algebra.InfiniteSum.Group
tprod_inv : ∀ {α : Type u_1} {β : Type u_2} {L : SummationFilter β} [inst : CommGroup α] [inst_1 : TopologicalSpace α]
  [IsTopologicalGroup α] {f : β → α} [T2Space α], ∏'[L] (b : β), (f b)⁻¹ = (∏'[L] (b : β), f b)⁻¹
-- Mathlib.MeasureTheory.Constructions.HaarToSphere
MeasureTheory.Measure.toSphereBallBound_pos : ∀ (n : ℕ) (ε : ℝ), 0 < MeasureTheory.Measure.toSphereBallBound n ε
-- Mathlib.Data.Finset.Card
Finset.three_lt_card : ∀ {α : Type u_1} {s : Finset α},
  3 < s.card ↔ ∃ a ∈ s, ∃ b ∈ s, ∃ c ∈ s, ∃ d ∈ s, a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d
-- Batteries.Data.List.Interleave
_private.Batteries.Data.List.Interleave.0.List.interleave.match_1.splitter : {α : Type u_1} →
  (motive : List α → List α → Sort u_2) →
    (x x_1 : List α) →
      ((l₂ : List α) → motive [] l₂) → ((a : α) → (l₁ l₂ : List α) → motive (a :: l₁) l₂) → motive x x_1
-- Mathlib.Analysis.Normed.Group.Basic
dist_inv : ∀ {E : Type u_5} [inst : SeminormedCommGroup E] (x y : E), dist x⁻¹ y = dist x y⁻¹
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.walkingCospanOpEquiv_functor_map : ∀ {X Y : (CategoryTheory.Limits.WidePullbackShape CategoryTheory.Limits.WalkingPair)ᵒᵖ} (f : X ⟶ Y),
  CategoryTheory.Limits.walkingCospanOpEquiv.functor.map f =
    (CategoryTheory.Limits.widePullbackShapeOpMap CategoryTheory.Limits.WalkingPair (Opposite.unop Y) (Opposite.unop X)
        f.unop).unop
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
CategoryTheory.Limits.CatCospanTransform.id_squareRight : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B),
  (CategoryTheory.Limits.CatCospanTransform.id F G).squareRight = inferInstance
-- Mathlib.Algebra.Group.Hom.Defs
MulHom.funLike : {M : Type u_4} → {N : Type u_5} → [inst : Mul M] → [inst_1 : Mul N] → FunLike (M →ₙ* N) M N
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.mapNatIso_unitIso_hom_app_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : D} {T T' : CategoryTheory.Functor C D} (i : T ≅ T')
  (X : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit S) T),
  ((CategoryTheory.StructuredArrow.mapNatIso i).unitIso.hom.app X).right = CategoryTheory.CategoryStruct.id X.right
-- Std.Data.DTreeMap.Internal.Model
/-- Needle was equal to key at this node: return key-value pair and both unexplored subtrees,
recursion will terminate.  -/
Std.DTreeMap.Internal.Impl.ExplorationStep.eq : {α : Type u} →
  {β : α → Type v} →
    [inst : Ord α] →
      {k : α → Ordering} →
        List ((a : α) × β a) →
          Std.DTreeMap.Internal.Cell α β k → List ((a : α) × β a) → Std.DTreeMap.Internal.Impl.ExplorationStep α β k
-- Std.Time.Date.Unit.Weekday
_private.Std.Time.Date.Unit.Weekday.0.Std.Time.Weekday.toOrdinal.eq_7 : Std.Time.Weekday.sunday.toOrdinal = 7
-- Mathlib.Algebra.Order.Interval.Set.Group
Set.neg_mem_Ioo_iff : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] {a c d : α},
  -a ∈ Set.Ioo c d ↔ a ∈ Set.Ioo (-d) (-c)
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.coxeterWeight.eq_1 : ∀ {ι : 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) (i j : ι),
  P.coxeterWeight i j = P.pairing i j * P.pairing j i
-- Mathlib.MeasureTheory.SpecificCodomains.WithLp
MeasureTheory.MemLp.prodLp_fst : ∀ {X : Type u_1} {mX : MeasurableSpace X} {μ : MeasureTheory.Measure X} {p q : ENNReal} [inst : Fact (1 ≤ q)]
  {E : Type u_2} {F : Type u_3} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedAddCommGroup F]
  {f : X → WithLp q (E × F)}, MeasureTheory.MemLp f p μ → MeasureTheory.MemLp (fun x => (f x).fst) p μ
-- Mathlib.Algebra.Group.Action.Defs
VAdd.comp.eq_1 : ∀ {M : Type u_1} {N : Type u_2} (α : Type u_5) [inst : VAdd M α] (g : N → M),
  VAdd.comp α g = { vadd := VAdd.comp.vadd g }
-- Mathlib.LinearAlgebra.Multilinear.FiniteDimensional
Module.Free.multilinearMap : ∀ {ι : Type u_1} {R : Type u_2} {M₂ : Type u_3} {M₁ : ι → Type u_4} [Finite ι] [inst : CommRing R]
  [inst_1 : AddCommGroup M₂] [inst_2 : Module R M₂] [Module.Finite R M₂] [Module.Free R M₂]
  [inst_5 : (i : ι) → AddCommGroup (M₁ i)] [inst_6 : (i : ι) → Module R (M₁ i)] [∀ (i : ι), Module.Finite R (M₁ i)]
  [∀ (i : ι), Module.Free R (M₁ i)], Module.Free R (MultilinearMap R M₁ M₂)
-- Mathlib.Data.ENNReal.Operations
ENNReal.toNNReal_sub : ∀ {a b : ENNReal}, b ≠ ⊤ → (a - b).toNNReal = a.toNNReal - b.toNNReal
-- Lean.Meta.WHNF
Lean.Meta.reduceNat? : Lean.Expr → Lean.MetaM (Option Lean.Expr)
-- Init.Grind.AC
Lean.Grind.AC.simp_prefix_cert.eq_1 : ∀ (lhs rhs tail s s' : Lean.Grind.AC.Seq),
  Lean.Grind.AC.simp_prefix_cert lhs rhs tail s s' = (s.beq' (lhs.concat_k tail)).and' (s'.beq' (rhs.concat_k tail))
-- Lean.Server.Completion.CompletionUtils
/-- Gets type names for resolving `id` in `.id x₁ ... xₙ` notation.
The process mimics the dotted identifier notation elaboration procedure at `Lean.Elab.App`.
Catches and ignores all errors, so no need to run this within `try`/`catch`.
 -/
Lean.Server.Completion.getDotIdCompletionTypeNames : Lean.Expr → Lean.MetaM (Array Lean.Name)
-- Mathlib.Algebra.Group.Basic
leftInverse_mul_right_inv_mul : ∀ {G : Type u_3} [inst : Group G] (c : G), Function.LeftInverse (fun x => c * x) fun x => c⁻¹ * x
-- Lean.Expr
Lean.Expr.bindingName! : Lean.Expr → Lean.Name
-- Mathlib.AlgebraicGeometry.Sites.Representability
/-- Suppose
* F is a `Type u`-valued sheaf on `Sch` with respect to the Zariski topology
* X : ι → Sch is a family of schemes
* f : Π i, yoneda.obj (X i) ⟶ F is a family of relatively representable open immersions
* f is jointly surjective

Then `F` is representable.
 -/
AlgebraicGeometry.Scheme.LocalRepresentability.isRepresentable : ∀ {F : CategoryTheory.Sheaf AlgebraicGeometry.Scheme.zariskiTopology (Type u)} {ι : Type u}
  {X : ι → AlgebraicGeometry.Scheme} {f : (i : ι) → CategoryTheory.yoneda.obj (X i) ⟶ F.obj},
  (∀ (i : ι), AlgebraicGeometry.IsOpenImmersion.presheaf (f i)) →
    ∀
      [CategoryTheory.Presheaf.IsLocallySurjective AlgebraicGeometry.Scheme.zariskiTopology
          (CategoryTheory.Limits.Sigma.desc f)],
      F.obj.IsRepresentable
-- Mathlib.Tactic.FunProp.Theorems
/-- Convert `LambdaTheoremArgs` to `LambdaTheoremType`.  -/
Mathlib.Meta.FunProp.LambdaTheoremArgs.type : Mathlib.Meta.FunProp.LambdaTheoremArgs → Mathlib.Meta.FunProp.LambdaTheoremType
-- Mathlib.Topology.Algebra.Module.Spaces.WeakBilin
WeakBilin.instAddCommGroup : {𝕜 : Type u_2} →
  {E : Type u_4} →
    {F : Type u_5} →
      [inst : CommSemiring 𝕜] →
        [inst_1 : AddCommGroup E] →
          [inst_2 : Module 𝕜 E] →
            [inst_3 : AddCommMonoid F] → [inst_4 : Module 𝕜 F] → (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) → AddCommGroup (WeakBilin B)
-- Batteries.Data.UInt
UInt64.toNat_min : ∀ (x y : UInt64), (x ⊓ y).toNat = min x.toNat y.toNat
-- Mathlib.Control.Monad.Writer
WriterT.instMonadExceptOf : {M : Type u → Type v} → {ω : Type u} → {ε : Type u_1} → [MonadExceptOf ε M] → MonadExceptOf ε (WriterT ω M)
-- Mathlib.Analysis.SpecialFunctions.Complex.Arg
Complex.arg_of_re_nonneg : ∀ {x : ℂ}, 0 ≤ x.re → x.arg = Real.arcsin (x.im / ‖x‖)
-- Std.Time.DateTime.PlainDateTime
/-- Getter for the `Year` inside of a `PlainDateTime`.
 -/
Std.Time.PlainDateTime.year : Std.Time.PlainDateTime → Std.Time.Year.Offset
-- Mathlib.Tactic.Order.Preprocessing
Mathlib.Tactic.Order.OrderType.part : Mathlib.Tactic.Order.OrderType
-- Mathlib.Topology.DenseEmbedding
IsDenseEmbedding.id : ∀ {α : Type u_5} [inst : TopologicalSpace α], IsDenseEmbedding id
-- Init.Data.BitVec.Lemmas
/-- If the msb is `true`, the arithmetic shift right equals negating,
then logical shifting right, then negating again.
The double negation preserves the lower bits that have been shifted,
and the outer negation ensures that the high bits are '1'.  -/
BitVec.sshiftRight_eq_of_msb_true : ∀ {w : ℕ} {x : BitVec w} {s : ℕ}, x.msb = true → x.sshiftRight s = ~~~(~~~x >>> s)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.instInhabitedDvdCnstr : Inhabited Lean.Meta.Grind.Arith.Cutsat.DvdCnstr
-- Mathlib.LinearAlgebra.RootSystem.Finite.G2
RootPairing.EmbeddedG2.threeShortAddLong.eq_1 : ∀ {ι : 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)
  [inst_5 : P.EmbeddedG2],
  RootPairing.EmbeddedG2.threeShortAddLong P =
    (P.reflectionPerm (RootPairing.EmbeddedG2.short P)) (RootPairing.EmbeddedG2.long P)
-- Mathlib.Data.Finsupp.Basic
/-- **Alias** of `Finsupp.mem_support_finsetSum`. -/
Finsupp.mem_support_finset_sum : ∀ {α : Type u_1} {ι : Type u_4} {M : Type u_5} [inst : AddCommMonoid M] {s : Finset ι} {h : ι → α →₀ M},
  ∀ a ∈ (∑ c ∈ s, h c).support, ∃ c ∈ s, a ∈ (h c).support
-- Init.Core
instInhabitedPNonScalar.default : PNonScalar
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKeyD_unitOfList_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] [inst : BEq α] [Std.LawfulBEqCmp cmp] {l : List α}
  {k fallback : α}, l.contains k = false → (Std.TreeMap.Raw.unitOfList l cmp).getKeyD k fallback = fallback
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.add_sub_cancel_of_le : ∀ {a b : Ordinal.{u_4}}, b ≤ a → b + (a - b) = a
-- Mathlib.CategoryTheory.Limits.Presentation
/-- If `F : J ⥤ C` is a functor that has a limit, then this is the obvious
limit presentation of `limit F`.  -/
CategoryTheory.Limits.LimitPresentation.limit : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type w} →
      [inst_1 : CategoryTheory.Category.{t, w} J] →
        (F : CategoryTheory.Functor J C) →
          [inst_2 : CategoryTheory.Limits.HasLimit F] →
            CategoryTheory.Limits.LimitPresentation J (CategoryTheory.Limits.limit F)
-- Lean.Elab.App
Lean.Elab.Term.LValResolution.localRec.injEq : ∀ (baseName : Lean.Name) (fvar : Lean.Expr) (baseName_1 : Lean.Name) (fvar_1 : Lean.Expr),
  (Lean.Elab.Term.LValResolution.localRec baseName fvar = Lean.Elab.Term.LValResolution.localRec baseName_1 fvar_1) =
    (baseName = baseName_1 ∧ fvar = fvar_1)
-- Mathlib.Order.Antisymmetrization
AntisymmRel.symmGen : ∀ {α : Type u_1} {a b : α} {r : α → α → Prop}, AntisymmRel r a b → Relation.SymmGen r a b
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.SimplicialObject.Augmented.rightOp_hom_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject.Augmented C)
  (x : SimplexCategory), X.rightOp.hom.app x = (X.hom.app (Opposite.op x)).op
-- Mathlib.MeasureTheory.VectorMeasure.Integral
MeasureTheory.VectorMeasure.variation_transpose_map_le : ∀ {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G]
  [inst_5 : NormedSpace ℝ G] {μ : MeasureTheory.VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G} {β : Type u_9}
  [inst_6 : MeasurableSpace β] {φ : X → β},
  ((μ.map φ).transpose B).variation ≤ MeasureTheory.Measure.map φ (μ.transpose B).variation
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
MeasureTheory.SignedMeasure.totalVariation_absolutelyContinuous_iff : ∀ {α : Type u_1} [inst : MeasurableSpace α] (s : MeasureTheory.SignedMeasure α) (μ : MeasureTheory.Measure α),
  s.totalVariation.AbsolutelyContinuous μ ↔
    s.toJordanDecomposition.posPart.AbsolutelyContinuous μ ∧ s.toJordanDecomposition.negPart.AbsolutelyContinuous μ
-- Aesop.Saturate
Aesop.SaturateM.Context : Type
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.size_alter_eq_self_of_mem : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {f : Option β → Option β},
  k ∈ m → (f m[k]?).isSome = true → (m.alter k f).size = m.size
-- Mathlib.Algebra.Polynomial.Degree.Defs
/-- `natDegree p` forces `degree p` to ℕ, by defining `natDegree 0 = 0`.  -/
Polynomial.natDegree : {R : Type u} → [inst : Semiring R] → Polynomial R → ℕ
-- Mathlib.Algebra.Star.Basic
RingHom.star_apply : ∀ {R : Type u} [inst : CommSemiring R] [inst_1 : StarRing R] {S : Type u_1} [inst_2 : NonAssocSemiring S] (f : S →+* R)
  (s : S), (star f) s = star (f s)
-- Init.Data.Slice.List.Iterator
/-- `ListSlice` representation.  -/
List.ListSlice.repr : {α : Type u} → [Repr α] → ListSlice α → Std.Format
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
/-- The distance between two functions is controlled by the supremum of the pointwise distances.  -/
BoundedContinuousFunction.dist_le : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β]
  {f g : BoundedContinuousFunction α β} {C : ℝ}, 0 ≤ C → (dist f g ≤ C ↔ ∀ (x : α), dist (f x) (g x) ≤ C)
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.Measure.toENNRealVectorMeasure_ennrealToMeasure : ∀ {α : Type u_1} {m : MeasurableSpace α} (μ : MeasureTheory.VectorMeasure α ENNReal),
  μ.ennrealToMeasure.toENNRealVectorMeasure = μ
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.lift_fac : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : AlgebraicGeometry.PresheafedSpace C} (f : X ⟶ Z)
  [hf : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f] (g : Y ⟶ Z)
  (H :
    Set.range ⇑(CategoryTheory.ConcreteCategory.hom g.base) ⊆ Set.range ⇑(CategoryTheory.ConcreteCategory.hom f.base)),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.lift f g H) f = g
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.toList_toArray : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β},
  (Std.DHashMap.Const.toArray m).toList = Std.DHashMap.Const.toList m
-- Init.Data.Array.Lemmas
/-- Use this as `induction ass using array₂_induction` on a hypothesis of the form `ass : Array (Array α)`.
The hypothesis `ass` will be replaced with a hypothesis `ass : List (List α)`,
and former appearances of `ass` in the goal will be replaced with `(ass.map List.toArray).toArray`.
 -/
Array.array₂_induction : ∀ {α : Type u_1} (P : Array (Array α) → Prop),
  (∀ (xss : List (List α)), P (List.map List.toArray xss).toArray) → ∀ (xss : Array (Array α)), P xss
-- Init.Data.UInt.Lemmas
UInt16.toUInt64_ofNatClamp_of_le : ∀ {n : ℕ},
  UInt16.size ≤ n →
    (UInt16.ofNatClamp n).toUInt64 = UInt64.ofNatLT (UInt16.size - 1) UInt16.toUInt64_ofNatClamp_of_le._proof_1