mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Grind.ToInt
_private.Init.Grind.ToInt.0.Lean.Grind.instBEqIntInterval.beq.match_1.eq_2 : ∀ (motive : Lean.Grind.IntInterval → Lean.Grind.IntInterval → Sort u_1) (a b : ℤ)
  (h_1 : (a a_1 b b_1 : ℤ) → motive (Lean.Grind.IntInterval.co a a_1) (Lean.Grind.IntInterval.co b b_1))
  (h_2 : (a b : ℤ) → motive (Lean.Grind.IntInterval.ci a) (Lean.Grind.IntInterval.ci b))
  (h_3 : (a b : ℤ) → motive (Lean.Grind.IntInterval.io a) (Lean.Grind.IntInterval.io b))
  (h_4 : Unit → motive Lean.Grind.IntInterval.ii Lean.Grind.IntInterval.ii)
  (h_5 : (x x_1 : Lean.Grind.IntInterval) → motive x x_1),
  (match Lean.Grind.IntInterval.ci a, Lean.Grind.IntInterval.ci b with
    | Lean.Grind.IntInterval.co a a_1, Lean.Grind.IntInterval.co b b_1 => h_1 a a_1 b b_1
    | Lean.Grind.IntInterval.ci a, Lean.Grind.IntInterval.ci b => h_2 a b
    | Lean.Grind.IntInterval.io a, Lean.Grind.IntInterval.io b => h_3 a b
    | Lean.Grind.IntInterval.ii, Lean.Grind.IntInterval.ii => h_4 ()
    | x, x_1 => h_5 x x_1) =
    h_2 a b
-- Mathlib.Algebra.Star.Pi
Pi.instStarRingForall : {I : Type u} →
  {f : I → Type v} → [inst : (i : I) → NonUnitalSemiring (f i)] → [(i : I) → StarRing (f i)] → StarRing ((i : I) → f i)
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
Finsupp.sum_indicator_index : ∀ {α : Type u_1} {M : Type u_8} {N : Type u_10} [inst : Zero M] [inst_1 : AddCommMonoid N] {s : Finset α} (f : α → M)
  {h : α → M → N}, (∀ a ∈ s, h a 0 = 0) → (Finsupp.indicator s fun x x_1 => f x).sum h = ∑ x ∈ s, h x (f x)
-- Mathlib.ModelTheory.ElementaryMaps
FirstOrder.Language.ElementaryEmbedding.embeddingLike : ∀ {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [inst : L.Structure M] [inst_1 : L.Structure N],
  EmbeddingLike (L.ElementaryEmbedding M N) M N
-- Mathlib.Data.Set.Image
_private.Mathlib.Data.Set.Image.0.Set.subset_image_sdiff : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (s t : Set α), f '' s \ f '' t ⊆ f '' (s \ t)
-- Mathlib.Algebra.Order.Field.Basic
one_div_le_of_neg : ∀ {α : Type u_2} [inst : Field α] [inst_1 : PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {a b : α},
  a < 0 → b < 0 → (1 / a ≤ b ↔ 1 / b ≤ a)
-- Init.System.IO
IO.FS.Mode.append.sizeOf_spec : sizeOf IO.FS.Mode.append = 1
-- Mathlib.GroupTheory.SpecificGroups.ZGroup
/-- A cyclic Sylow subgroup is either central in its normalizer or contained in the commutator
subgroup.  -/
Sylow.normalizer_le_centralizer_or_le_commutator : ∀ {G : Type u_1} [inst : Group G] {p : ℕ} [Fact (Nat.Prime p)] [Finite G] (P : Sylow p G) [IsCyclic ↥↑P],
  Subgroup.normalizer ↑P ≤ Subgroup.centralizer ↑P ∨ ↑P ≤ commutator G
-- Mathlib.Topology.VectorBundle.Basic
VectorPrebundle.pretrivializationAt : {R : Type u_1} →
  {B : Type u_2} →
    {F : Type u_3} →
      {E : B → Type u_4} →
        [inst : NontriviallyNormedField R] →
          [inst_1 : (x : B) → AddCommMonoid (E x)] →
            [inst_2 : (x : B) → Module R (E x)] →
              [inst_3 : NormedAddCommGroup F] →
                [inst_4 : NormedSpace R F] →
                  [inst_5 : TopologicalSpace B] →
                    [inst_6 : (x : B) → TopologicalSpace (E x)] →
                      VectorPrebundle R F E → B → Bundle.Pretrivialization F Bundle.TotalSpace.proj
-- Mathlib.LinearAlgebra.Alternating.Basic
AlternatingMap.coe_compLinearMap : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {ι : Type u_7} {M₂ : Type u_10} [inst_5 : AddCommMonoid M₂]
  [inst_6 : Module R M₂] (f : M [⋀^ι]→ₗ[R] N) (g : M₂ →ₗ[R] M), ⇑(f.compLinearMap g) = ⇑f ∘ fun x => ⇑g ∘ x
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
/-- `HasWidePushout B objs arrows` means that `wideSpan B objs arrows` has a colimit.  -/
CategoryTheory.Limits.HasWidePushout : {J : Type w} →
  {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → (B : C) → (objs : J → C) → ((j : J) → B ⟶ objs j) → Prop
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.preimage_add_const_uIcc : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [IsOrderedAddMonoid α] (a b c : α),
  (fun x => x + a) ⁻¹' Set.uIcc b c = Set.uIcc (b - a) (c - a)
-- Lean.Elab.SyntheticMVars
_private.Lean.Elab.SyntheticMVars.0.Lean.Elab.Term.synthesizeUsingDefaultPrio.synthesizePendingInstMVar' : Lean.MVarId → Lean.Elab.TermElabM Bool
-- Lean.Data.Lsp.Basic
Lean.Lsp.TextDocumentIdentifier.mk.sizeOf_spec : ∀ (uri : Lean.Lsp.DocumentUri), sizeOf { uri := uri } = 1 + sizeOf uri
-- Mathlib.GroupTheory.CommutingProbability
commProb_eq_one_iff : ∀ {M : Type u_1} [inst : Mul M] [Finite M] [h : Nonempty M], commProb M = 1 ↔ IsMulCommutative M
-- Mathlib.Analysis.Calculus.ContDiff.Comp
/-- The composition of `C^n` functions at points in domains is `C^n`.  -/
ContDiffWithinAt.comp_inter : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {n : WithTop ℕ∞} {s : Set E} {t : Set F} {g : F → G}
  {f : E → F} (x : E),
  ContDiffWithinAt 𝕜 n g t (f x) → ContDiffWithinAt 𝕜 n f s x → ContDiffWithinAt 𝕜 n (g ∘ f) (s ∩ f ⁻¹' t) x
-- Mathlib.Algebra.Order.Module.Defs
StrictOrderedSemiring.toSMulPosStrictMonoNat : ∀ {α : Type u_1} [inst : Semiring α] [inst_1 : PartialOrder α] [IsStrictOrderedRing α], SMulPosStrictMono ℕ α
-- Init.Data.SInt.Lemmas
ISize.zero_mod : ∀ {a : ISize}, 0 % a = 0
-- Lean.Meta.Sym.Simp.SimpM
Lean.Meta.Sym.Simp.Methods.mk.inj : ∀ {pre post pre_1 post_1 : Lean.Meta.Sym.Simp.Simproc},
  { pre := pre, post := post } = { pre := pre_1, post := post_1 } → pre = pre_1 ∧ post = post_1
-- Mathlib.Logic.Equiv.List
/-- A list on a unique type is equivalent to ℕ by sending each list to its length.  -/
Equiv.listUniqueEquiv : (α : Type u_1) → [Unique α] → List α ≃ ℕ
-- Mathlib.Algebra.Pointwise.Stabilizer
MulAction.mem_stabilizer_set' : ∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] {a : G} {s : Set α},
  s.Finite → (a ∈ MulAction.stabilizer G s ↔ ∀ ⦃b : α⦄, b ∈ s → a • b ∈ s)
-- Mathlib.Algebra.Homology.HomotopyCategory.Shift
CochainComplex.shiftFunctorAdd_eq : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] (a b : ℤ),
  CategoryTheory.shiftFunctorAdd (CochainComplex C ℤ) a b = CochainComplex.shiftFunctorAdd' C a b (a + b) ⋯
-- Mathlib.RingTheory.MvPowerSeries.Order
MvPowerSeries.order_zero : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R], MvPowerSeries.order 0 = ⊤
-- Lean.Syntax
Lean.Syntax.mkAntiquotNode : Lean.Name → Lean.Syntax → optParam ℕ 0 → optParam (Option String) none → optParam Bool false → Lean.Syntax
-- Aesop.Rule.Name
Aesop.DisplayRuleName : Type
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Const.Equiv.beq_congr : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {m₁ m₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp] [inst : BEq β]
  {m₃ m₄ : Std.TreeMap.Raw α β cmp}, m₁.WF → m₂.WF → m₃.WF → m₄.WF → m₁.Equiv m₃ → m₂.Equiv m₄ → (m₁ == m₂) = (m₃ == m₄)
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
CategoryTheory.CostructuredArrow.functor_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (T : CategoryTheory.Functor C D) (d : D),
  (CategoryTheory.CostructuredArrow.functor T).obj d = CategoryTheory.Cat.of (CategoryTheory.CostructuredArrow T d)
-- Mathlib.Algebra.Group.TypeTags.Hom
/-- `AddMonoidHom.toMultiplicativeLeft` as an `AddEquiv`.  -/
AddMonoidHom.toMultiplicativeLeftAddEquiv : {M : Type u_1} →
  {N : Type u_2} →
    [inst : AddMonoid M] → [inst_1 : CommMonoid N] → (M →+ Additive N) ≃+ Additive (Multiplicative M →* N)
-- Mathlib.Algebra.Order.Round
round_intCast : ∀ {α : Type u_2} [inst : Ring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [inst_3 : FloorRing α] (n : ℤ),
  round ↑n = n
-- Mathlib.RingTheory.Finiteness.Ideal
/-- The image of a finitely generated ideal is finitely generated.

This is the `Ideal` version of `Submodule.FG.map`.  -/
Ideal.FG.map : ∀ {R : Type u_3} {S : Type u_4} [inst : Semiring R] [inst_1 : Semiring S] {I : Ideal R},
  I.FG → ∀ (f : R →+* S), (Ideal.map f I).FG
-- Mathlib.LinearAlgebra.Matrix.Ideal
/-- Two-sided ideals in $R$ correspond bijectively to those in $Mₙ(R)$.
Given an ideal $I ≤ R$, we send it to $Mₙ(I)$.
Given an ideal $J ≤ Mₙ(R)$, we send it to $\{Nᵢⱼ ∣ ∃ N ∈ J\}$.
 -/
TwoSidedIdeal.equivMatrix : {R : Type u_1} →
  {n : Type u_2} →
    [inst : NonAssocRing R] →
      [inst_1 : Fintype n] → [Nonempty n] → [DecidableEq n] → TwoSidedIdeal R ≃ TwoSidedIdeal (Matrix n n R)
-- Mathlib.Data.Nat.Choose.Vandermonde
/-- Vandermonde's identity  -/
Nat.add_choose_eq : ∀ (m n k : ℕ), (m + n).choose k = ∑ ij ∈ Finset.HasAntidiagonal.antidiagonal k, m.choose ij.1 * n.choose ij.2
-- Mathlib.CategoryTheory.ObjectProperty.ColimitsClosure
CategoryTheory.ObjectProperty.instIsClosedUnderColimitsOfShapeColimitClosure : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) (J : Type u_1)
  [inst_1 : CategoryTheory.Category.{v_1, u_1} J], (P.colimitClosure J).IsClosedUnderColimitsOfShape J
-- Mathlib.Algebra.Category.ModuleCat.Topology.Basic
/-- Use the `ConcreteCategory.hom` projection for `@[simps]` lemmas.  -/
TopModuleCat.Hom.Simps.hom : (R : Type u) →
  [inst : Ring R] →
    [inst_1 : TopologicalSpace R] → (A B : TopModuleCat R) → A.Hom B → ↑A.toModuleCat →L[R] ↑B.toModuleCat
-- Mathlib.Algebra.Order.CompleteField
/-- **Alias** of `ConditionallyCompleteLinearOrderedField.inducedMap_inv_self`. -/
LinearOrderedField.inducedMap_inv_self : ∀ (β : Type u_3) (γ : Type u_4) [inst : Field β] [inst_1 : ConditionallyCompleteLinearOrder β] [IsStrictOrderedRing β]
  [inst_3 : Field γ] [inst_4 : ConditionallyCompleteLinearOrder γ] [IsStrictOrderedRing γ] (b : β),
  ConditionallyCompleteLinearOrderedField.inducedMap γ β (ConditionallyCompleteLinearOrderedField.inducedMap β γ b) = b
-- Init.Data.NeZero
NeZero.ne' : ∀ {R : Type u_1} [inst : Zero R] (n : R) [h : NeZero n], 0 ≠ n
-- Mathlib.Order.Interval.Finset.Basic
Finset.Icc_top : ∀ {α : Type u_2} {a : α} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] [inst_2 : OrderTop α],
  Finset.Icc a ⊤ = Finset.Ici a
-- Mathlib.Data.Nat.Pairing
Nat.pair_lt_max_add_one_sq : ∀ (m n : ℕ), Nat.pair m n < (max m n + 1) ^ 2
-- Mathlib.Algebra.Order.Group.Abs
/-- For an element `a` of an additive linear ordered group,
either `|a| = a` and `0 ≤ a`, or `|a| = -a` and `a < 0`.
Use cases on this lemma to automate linarith in inequalities  -/
abs_cases : ∀ {G : Type u_1} [inst : AddCommGroup G] [inst_1 : LinearOrder G] [IsOrderedAddMonoid G] (a : G),
  |a| = a ∧ 0 ≤ a ∨ |a| = -a ∧ a < 0
-- Batteries.Data.Array.Basic
Array.scanlM.loop.congr_simp : ∀ {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} [inst : Monad m] (f f_1 : β → α → m β),
  f = f_1 →
    ∀ (init init_1 : β),
      init = init_1 →
        ∀ (as as_1 : Array α) (e_as : as = as_1) (start start_1 : ℕ),
          start = start_1 →
            ∀ (stop stop_1 : ℕ) (e_stop : stop = stop_1) (h_stop : stop ≤ as.size) (acc acc_1 : Array β),
              acc = acc_1 →
                Array.scanlM.loop f init as start stop h_stop acc =
                  Array.scanlM.loop f_1 init_1 as_1 start_1 stop_1 ⋯ acc_1
-- Lean.Meta.Tactic.Grind.Types
_private.Lean.Meta.Tactic.Grind.Types.0.Lean.Meta.Grind.mkENodeCore.unsafe_impl_2 : (e : Lean.Expr) →
  (n : Lean.Meta.Grind.ENode) →
    (s : Lean.Meta.Grind.Goal) → Lean.Meta.Grind.CongrTable (Lean.PersistentHashMap.insert s.enodeMap { expr := e } n)
-- Mathlib.RingTheory.Noetherian.Nilpotent
IsNoetherianRing.isNilpotent_nilradical : ∀ (R : Type u_1) [inst : CommSemiring R] [IsNoetherianRing R], IsNilpotent (nilradical R)
-- Mathlib.Geometry.RingedSpace.PresheafedSpace
AlgebraicGeometry.PresheafedSpace.Γ_obj_op : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (X : AlgebraicGeometry.PresheafedSpace C),
  AlgebraicGeometry.PresheafedSpace.Γ.obj (Opposite.op X) = X.presheaf.obj (Opposite.op ⊤)
-- Mathlib.Algebra.Order.Module.Defs
OrderDual.instIsOrderedModule : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : MonoidWithZero α] [inst_2 : AddCommGroup β]
  [inst_3 : PartialOrder β] [IsOrderedAddMonoid β] [inst_5 : DistribMulAction α β] [IsOrderedModule α β],
  IsOrderedModule α βᵒᵈ
-- Init.Data.SInt.Lemmas
Int16.toInt8_ofIntClamp : ∀ {n : ℤ}, -2 ^ 15 ≤ n → n < 2 ^ 15 → (Int16.ofIntClamp n).toInt8 = Int8.ofInt n
-- Mathlib.RingTheory.Flat.Equalizer
/-- Given a surjection of `R`-algebras `S → T` with kernel `I`, such that `T` is flat,
the kernel of the map `A ⊗ S → A ⊗ T` is the base change of `I` along `S → A ⊗ S`.
 -/
Algebra.kerTensorProductMapIdToAlgHomEquiv : (R : Type u_1) →
  (S : Type u_2) →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          (T : Type u_3) →
            [inst_3 : CommRing T] →
              [inst_4 : Algebra R T] →
                [inst_5 : Algebra S T] →
                  [inst_6 : IsScalarTower R S T] →
                    (A : Type u_4) →
                      [inst_7 : CommRing A] →
                        [inst_8 : Algebra R A] →
                          [Module.Flat R T] →
                            Function.Surjective ⇑(algebraMap S T) →
                              ↥(RingHom.ker
                                    (Algebra.TensorProduct.map (AlgHom.id A A)
                                      (IsScalarTower.toAlgHom R S T))) ≃ₗ[TensorProduct R A S]
                                TensorProduct S (TensorProduct R A S) ↥(RingHom.ker (algebraMap S T))
-- Lean.Expr
/-- A (universe polymorphic) constant that has been defined earlier in the module or
by another imported module. For example, `@Eq.{1}` is represented
as ``Expr.const `Eq [.succ .zero]``, and `@Array.map.{0, 0}` is represented
as ``Expr.const `Array.map [.zero, .zero]``.
 -/
Lean.Expr.const : Lean.Name → List Lean.Level → Lean.Expr
-- Mathlib.Algebra.Group.Pointwise.Set.BigOperators
Set.list_sum_singleton : ∀ {M : Type u_5} [inst : AddMonoid M] (s : List M), (List.map (fun i => {i}) s).sum = {s.sum}
-- Init.Data.Option.Lemmas
Option.pbind_eq_bind : ∀ {α : Type u_1} {β : Type u_2} (o : Option α) (f : α → Option β), (o.pbind fun x x_1 => f x) = o.bind f
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getD_union_of_not_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {fallback : β}, k ∉ t₂ → (t₁ ∪ t₂).getD k fallback = t₁.getD k fallback
-- Mathlib.Data.Seq.Computation
Computation.thinkN_equiv : ∀ {α : Type u} (s : Computation α) (n : ℕ), (s.thinkN n).Equiv s
-- Mathlib.Algebra.ContinuedFractions.Translations
GenContFract.terminatedAt_iff_partDen_none : ∀ {α : Type u_1} {g : GenContFract α} {n : ℕ}, g.TerminatedAt n ↔ g.partDens.get? n = none
-- Mathlib.MeasureTheory.Measure.GiryMonad
MeasureTheory.Measure.join_map_join : ∀ {α : Type u_1} {mα : MeasurableSpace α} (μ : MeasureTheory.Measure (MeasureTheory.Measure (MeasureTheory.Measure α))),
  (MeasureTheory.Measure.map MeasureTheory.Measure.join μ).join = μ.join.join
-- Mathlib.Topology.Constructions
Continuous.finTail : ∀ {X : Type u} [inst : TopologicalSpace X] {n : ℕ} {A : Fin (n + 1) → Type u_9}
  [inst_1 : (i : Fin (n + 1)) → TopologicalSpace (A i)] {f : X → (j : Fin (n + 1)) → A j},
  Continuous f → Continuous fun a => Fin.tail (f a)
-- Init.Data.BitVec.Lemmas
BitVec.toFin_extractLsb : ∀ {n hi lo : ℕ} {x : BitVec n}, (BitVec.extractLsb hi lo x).toFin = Fin.ofNat (2 ^ (hi - lo + 1)) (x.toNat >>> lo)
-- Mathlib.Tactic.CategoryTheory.Monoidal.Normalize
Mathlib.Tactic.Monoidal.evalWhiskerRight_nil : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {f g : C}
  (α : f ≅ g) (h : C),
  (CategoryTheory.MonoidalCategory.whiskerRightIso α h).hom = (CategoryTheory.MonoidalCategory.whiskerRightIso α h).hom
-- Mathlib.Data.List.Nodup
List.Nodup.map_on : ∀ {α : Type u} {β : Type v} {l : List α} {f : α → β},
  (∀ x ∈ l, ∀ y ∈ l, f x = f y → x = y) → l.Nodup → (List.map f l).Nodup
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.lintegral_map' : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_5} [inst : MeasurableSpace β]
  {μ' : MeasureTheory.Measure β} (f : MeasureTheory.SimpleFunc α ENNReal) (g : MeasureTheory.SimpleFunc β ENNReal)
  (m' : α → β),
  (∀ (a : α), f a = g (m' a)) → (∀ (s : Set β), MeasurableSet s → μ' s = μ (m' ⁻¹' s)) → f.lintegral μ = g.lintegral μ'
-- Lean.Meta.Tactic.Grind.AC.Seq
_private.Lean.Meta.Tactic.Grind.AC.Seq.0.Lean.Grind.AC.StartsWithResult.prefix.sizeOf_spec : ∀ (s : Lean.Grind.AC.Seq), sizeOf (Lean.Grind.AC.StartsWithResult.prefix✝ s) = 1 + sizeOf s
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.Hom.instIsLocalHomCarrierStalkCommRingCatPresheafCoeContinuousMapCarrierCarrierHomTopCatBaseRingHomHomStalkMap : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (x : ↥X),
  IsLocalHom (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.stalkMap f x))
-- Mathlib.Probability.Process.Stopping
MeasureTheory.memLp_stoppedValue : ∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : Nonempty ι] {μ : MeasureTheory.Measure Ω}
  {τ : Ω → WithTop ι} {E : Type u_4} {p : ENNReal} {u : ι → Ω → E} [inst_1 : PartialOrder ι]
  {ℱ : MeasureTheory.Filtration ι m} [inst_2 : NormedAddCommGroup E] [LocallyFiniteOrderBot ι],
  MeasureTheory.IsStoppingTime ℱ τ →
    (∀ (n : ι), MeasureTheory.MemLp (u n) p μ) →
      ∀ {N : ι}, (∀ (ω : Ω), τ ω ≤ ↑N) → MeasureTheory.MemLp (MeasureTheory.stoppedValue u τ) p μ
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
/-- If `e : S₁ ≅ S₂` is an isomorphism of short complexes and `h₁ : LeftHomologyData S₁`,
this is the left homology data for `S₂` deduced from the isomorphism.  -/
CategoryTheory.ShortComplex.LeftHomologyData.ofIso : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} → (S₁ ≅ S₂) → S₁.LeftHomologyData → S₂.LeftHomologyData
-- Mathlib.CategoryTheory.Monad.Limits
/-- (Impl) The key property defining the map `λ : L ⟶ TL`.  -/
CategoryTheory.Comonad.ForgetCreatesLimits'.commuting : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [inst_1 : CategoryTheory.Category.{v, u} J]
  {T : CategoryTheory.Comonad C} {D : CategoryTheory.Functor J T.Coalgebra}
  (c : CategoryTheory.Limits.Cone (D.comp T.forget)) (t : CategoryTheory.Limits.IsLimit c)
  [inst_2 : CategoryTheory.Limits.PreservesLimit (D.comp T.forget) T.toFunctor] (j : J),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Comonad.ForgetCreatesLimits'.lambda c t) (T.map (c.π.app j)) =
    CategoryTheory.CategoryStruct.comp (c.π.app j) (D.obj j).a
-- Mathlib.Order.Filter.AtTopBot.Basic
Filter.atTop_neBot_iff : ∀ {α : Type u_6} [inst : Preorder α], Filter.atTop.NeBot ↔ Nonempty α ∧ IsDirectedOrder α
-- Mathlib.Algebra.Algebra.Subalgebra.Pi
Subalgebra.mem_pi : ∀ {ι : Type u_1} {R : Type u_2} {S : ι → Type u_3} [inst : CommSemiring R] [inst_1 : (i : ι) → Semiring (S i)]
  [inst_2 : (i : ι) → Algebra R (S i)] {s : Set ι} {t : (i : ι) → Subalgebra R (S i)} {x : (i : ι) → S i},
  x ∈ Subalgebra.pi s t ↔ ∀ i ∈ s, x i ∈ t i
-- Mathlib.Analysis.Normed.Group.Uniform
lipschitzOnWith_neg_iff : ∀ {α : Type u_4} {E : Type u_5} [inst : SeminormedAddCommGroup E] [inst_1 : PseudoEMetricSpace α] {K : NNReal}
  {f : α → E} {s : Set α}, LipschitzOnWith K (-f) s ↔ LipschitzOnWith K f s
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.isEmpty_unitOfList : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {l : List α},
  (Std.DTreeMap.Const.unitOfList l cmp).isEmpty = l.isEmpty
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
/-- If `f` is continuous multilinear, then `f (Σ_{j₁ ∈ A₁} g₁ j₁, ..., Σ_{jₙ ∈ Aₙ} gₙ jₙ)` is the
sum of `f (g₁ (r 1), ..., gₙ (r n))` where `r` ranges over all functions with `r 1 ∈ A₁`, ...,
`r n ∈ Aₙ`. This follows from multilinearity by expanding successively with respect to each
coordinate.  -/
ContinuousMultilinearMap.map_sum_finset : ∀ {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
  [inst_4 : Module R M₂] [inst_5 : (i : ι) → TopologicalSpace (M₁ i)] [inst_6 : TopologicalSpace M₂]
  (f : ContinuousMultilinearMap R M₁ M₂) {α : ι → Type u_1} [inst_7 : Fintype ι] (g : (i : ι) → α i → M₁ i)
  (A : (i : ι) → Finset (α i)) [inst_8 : DecidableEq ι],
  (f fun i => ∑ j ∈ A i, g i j) = ∑ r ∈ Fintype.piFinset A, f fun i => g i (r i)
-- Mathlib.Data.Multiset.Dedup
Multiset.Subset.dedup_add_left : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Multiset α}, t ⊆ s → (s + t).dedup = s.dedup
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.symm_refl : ∀ (k : Type u_1) (P₁ : Type u_2) {V₁ : Type u_6} [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁]
  [inst_3 : AddTorsor V₁ P₁], (AffineEquiv.refl k P₁).symm = AffineEquiv.refl k P₁
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getElem?_eq_none : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {a : α},
  a ∉ t → t[a]? = none
-- Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
rootsOfUnity.integer_power_of_ringEquiv : ∀ {L : Type u} [inst : CommRing L] [IsDomain L] (n : ℕ) [NeZero n] (g : L ≃+* L),
  ∃ m, ∀ (t : ↥(rootsOfUnity n L)), g ↑↑t = ↑(↑t ^ m)
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MultispanIndex.ι_sndSigmaMap : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape}
  (I : CategoryTheory.Limits.MultispanIndex J C) [inst_1 : CategoryTheory.Limits.HasCoproduct I.left]
  [inst_2 : CategoryTheory.Limits.HasCoproduct I.right] (b : J.L),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι I.left b) I.sndSigmaMap =
    CategoryTheory.CategoryStruct.comp (I.snd b) (CategoryTheory.Limits.Sigma.ι I.right (J.snd b))
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.toReal_neg_pi_div_two : (↑(-Real.pi / 2)).toReal = -Real.pi / 2
-- Mathlib.Probability.CentralLimitTheorem
ProbabilityTheory.charFun_inv_sqrt_mul_sum : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X : ℕ → Ω → ℝ},
  ProbabilityTheory.iIndepFun X P →
    (∀ (i : ℕ), ProbabilityTheory.IdentDistrib (X i) (X 0) P P) →
      ∀ {n : ℕ} {t : ℝ},
        MeasureTheory.charFun (MeasureTheory.Measure.map (fun ω => (√↑n)⁻¹ * ∑ k ∈ Finset.range n, X k ω) P) t =
          MeasureTheory.charFun (MeasureTheory.Measure.map (X 0) P) ((√↑n)⁻¹ * t) ^ n
-- Mathlib.Data.Fin.Tuple.Embedding
/-- Two distinct elements of `α` give an embedding `Fin 2 ↪ α`.  -/
Function.Embedding.embFinTwo : {α : Type u_1} → {a b : α} → a ≠ b → Fin 2 ↪ α
-- Aesop.RuleTac.GoalDiff
Aesop.instInhabitedGoalDiff : Inhabited Aesop.GoalDiff
-- Batteries.Data.AssocList
/-- `AssocList α β` is "the same as" `List (α × β)`, but flattening the structure
leads to one fewer pointer indirection (in the current code generator).
It is mainly intended as a component of `HashMap`, but it can also be used as a plain
key-value map.
 -/
Batteries.AssocList : Type u → Type v → Type (max u v)
-- Mathlib.Algebra.MonoidAlgebra.Degree
AddMonoidAlgebra.supDegree_mem_support : ∀ {R : Type u_1} {A : Type u_3} {B : Type u_5} [inst : Semiring R] [inst_1 : LinearOrder B] [inst_2 : OrderBot B]
  {p : AddMonoidAlgebra R A} {D : A → B} [inst_3 : AddZeroClass A],
  Function.Injective D → p ≠ 0 → Function.invFun D (AddMonoidAlgebra.supDegree D p) ∈ p.coeff.support
-- Lean.Meta.Tactic.Simp.Types
/-- Auxiliary method.
Given the current `target` of `mvarId`, apply `r` which is a new target and proof that it is equal to the current one.
 -/
Lean.Meta.applySimpResultToTarget : Lean.MVarId → Lean.Expr → Lean.Meta.Simp.Result → Lean.MetaM Lean.MVarId
-- Init.Data.UInt.Bitwise
UInt16.shiftRight_zero : ∀ {a : UInt16}, a >>> 0 = a