mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey?_inter_of_not_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α}, k ∉ t₂ → (t₁ ∩ t₂).getKey? k = none
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Real.sin_arctan_nonneg : ∀ {x : ℝ}, 0 ≤ Real.sin (Real.arctan x) ↔ 0 ≤ x
-- Mathlib.Analysis.Convex.Cone.Dual
ProperCone.dual_iUnion : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommRing R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : TopologicalSpace R] [inst_4 : ClosedIciTopology R] [inst_5 : AddCommGroup M] [inst_6 : Module R M]
  [inst_7 : TopologicalSpace M] [inst_8 : AddCommGroup N] [inst_9 : Module R N] [inst_10 : TopologicalSpace N]
  {p : M →ₗ[R] N →ₗ[R] R} [inst_11 : p.IsContPerfPair] {ι : Sort u_4} (f : ι → Set M),
  ProperCone.dual p (⋃ i, f i) = ⨅ i, ProperCone.dual p (f i)
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.commute_int_add : ∀ (f : CircleDeg1Lift) (n : ℤ), Function.Commute ⇑f fun x => ↑n + x
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKey_eq : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [LawfulBEq α] {k : α} (h : k ∈ m),
  m.getKey k h = k
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Submonoid.LocalizationMap.instSubsingletonLocalization : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} [Subsingleton M], Subsingleton (Localization S)
-- Init.Grind.ToInt
_private.Init.Grind.ToInt.0.Lean.Grind.IntInterval.lo?.match_1.splitter : (motive : Lean.Grind.IntInterval → Sort u_1) →
  (i : Lean.Grind.IntInterval) →
    ((lo hi : ℤ) → motive (Lean.Grind.IntInterval.co lo hi)) →
      ((lo : ℤ) → motive (Lean.Grind.IntInterval.ci lo)) →
        ((hi : ℤ) → motive (Lean.Grind.IntInterval.io hi)) → (Unit → motive Lean.Grind.IntInterval.ii) → motive i
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.length_toList : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp],
  t.toList.length = t.size
-- Mathlib.Tactic.DepRewrite
_private.Mathlib.Tactic.DepRewrite.0.Mathlib.Tactic.DepRewrite.instEvalExprConfig : Lean.Elab.ConfigEval.EvalExpr Mathlib.Tactic.DepRewrite.Config
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.le_min! : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] [inst_1 : Inhabited α],
  t ≠ ∅ → ∀ {k : α}, (cmp k t.min!).isLE = true ↔ ∀ k' ∈ t, (cmp k k').isLE = true
-- Mathlib.Analysis.FunctionalSpaces.SobolevInequality
/-- The "grid-lines operation" (not a standard name) which is central in the inductive proof of the
Sobolev inequality.

For a finite dependent product `Π i : ι, A i` of sigma-finite measure spaces, a finite set `s` of
indices from `ι`, and a (later assumed nonnegative) real number `p`, this operation acts on a
function `f` from `Π i, A i` into the extended nonnegative reals.  The operation is to partially
integrate, in the `s` co-ordinates, the function whose value at `x : Π i, A i` is obtained by
multiplying a certain power of `f` with the product, for each co-ordinate `i` in `s`, of a certain
power of the integral of `f` along the "grid line" in the `i` direction through `x`.

We are most interested in this operation when the set `s` is the universe in `ι`, but as a proxy for
"induction on dimension" we define it for a general set `s` of co-ordinates: the `s`-grid-lines
operation on a function `f` which is constant along the co-ordinates in `sᶜ` is morally (that is, up
to type-theoretic nonsense) the same thing as the universe-grid-lines operation on the associated
function on the "lower-dimensional" space `Π i : s, A i`.  -/
MeasureTheory.GridLines.T : {ι : Type u_1} →
  {A : ι → Type u_2} →
    [inst : (i : ι) → MeasurableSpace (A i)] →
      ((i : ι) → MeasureTheory.Measure (A i)) →
        [DecidableEq ι] → ℝ → (((i : ι) → A i) → ENNReal) → Finset ι → ((i : ι) → A i) → ENNReal
-- Init.WFExtrinsicFix
WellFounded.extrinsicFix_eq_apply : ∀ {α : Sort u_2} {C : α → Sort u_1} [inst : ∀ (a : α), Nonempty (C a)] {R : α → α → Prop}
  {F : (a : α) → ((a' : α) → R a' a → C a') → C a},
  WellFounded R → ∀ {a : α}, WellFounded.extrinsicFix R F a = F a fun a_1 x => WellFounded.extrinsicFix R F a_1
-- Mathlib.NumberTheory.Modular
ModularGroup.I_mem_fd : UpperHalfPlane.I ∈ ModularGroup.fd
-- Mathlib.Data.Matrix.Mul
Matrix.addMonoidHomMulLeft_apply : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type v} [inst : NonUnitalNonAssocSemiring α] [inst_1 : Fintype m]
  (M : Matrix l m α) (x : Matrix m n α), M.addMonoidHomMulLeft x = M * x
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf
AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.SectionSubring.neg_mem' : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] {𝒜 : ℕ → σ}
  [inst_3 : GradedRing 𝒜] (U : (TopologicalSpace.Opens ↑(ProjectiveSpectrum.top 𝒜))ᵒᵖ)
  (a : (x : ↥(Opposite.unop U)) → HomogeneousLocalization.AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal),
  (AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.isLocallyFraction 𝒜).pred a →
    (AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.isLocallyFraction 𝒜).pred (-a)
-- Mathlib.Algebra.Category.ModuleCat.FilteredColimits
ModuleCat.FilteredColimits.ι_colimitDesc : ∀ {R : Type u} [inst : Ring R] {J : Type v} [inst_1 : CategoryTheory.SmallCategory J]
  [inst_2 : CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J (ModuleCat R))
  (t : CategoryTheory.Limits.Cocone F) (j : J),
  CategoryTheory.CategoryStruct.comp ((ModuleCat.FilteredColimits.colimitCocone F).ι.app j)
      (ModuleCat.FilteredColimits.colimitDesc F t) =
    t.ι.app j
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.not_isSuccLimit_of_lt_aleph0 : ∀ {c : Cardinal.{u_1}}, c < Cardinal.aleph0 → ¬Order.IsSuccLimit c
-- Mathlib.AlgebraicGeometry.Limits
AlgebraicGeometry.instHasStrictInitialObjectsScheme : CategoryTheory.Limits.HasStrictInitialObjects AlgebraicGeometry.Scheme
-- Lean.Data.Lsp.Basic
/-- A flag which indicates that user confirmation is needed before applying the change.  -/
Lean.Lsp.ChangeAnnotation.needsConfirmation : Lean.Lsp.ChangeAnnotation → Bool
-- Mathlib.Order.CompleteLattice.Basic
iSup₂_le_iff : ∀ {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_6} [inst : CompleteLattice α] {a : α} {f : (i : ι) → κ i → α},
  ⨆ i, ⨆ j, f i j ≤ a ↔ ∀ (i : ι) (j : κ i), f i j ≤ a
-- Init.Data.UInt.Lemmas
UInt32.le_ofNat_iff : ∀ {n : UInt32} {m : ℕ}, m < UInt32.size → (n ≤ UInt32.ofNat m ↔ n.toNat ≤ m)
-- Mathlib.Order.Filter.IsBounded
Filter.IsBoundedUnder.mono_le : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder β] {l : Filter α} {u v : α → β},
  Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l u → v ≤ᶠ[l] u → Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l v
-- Mathlib.Probability.Distributions.Pareto
/-- The Pareto pdf is measurable.  -/
ProbabilityTheory.measurable_paretoPDFReal : ∀ (t r : ℝ), Measurable (ProbabilityTheory.paretoPDFReal t r)
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
/-- The `i`th homology functor `HomologicalComplex C c ⥤ C`.  -/
HomologicalComplex.homologyFunctor : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {ι : Type u_2} →
        (c : ComplexShape ι) →
          ι → [CategoryTheory.CategoryWithHomology C] → CategoryTheory.Functor (HomologicalComplex C c) C
-- Mathlib.SetTheory.Cardinal.Cofinality.Basic
Order.cof_ne_one : ∀ {α : Type u} [inst : Preorder α] [h : NoTopOrder α], Order.cof α ≠ 1
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.CliqueFreeOn.subset : ∀ {α : Type u_1} (G : SimpleGraph α) {s₁ s₂ : Set α} {n : ℕ}, s₁ ⊆ s₂ → G.CliqueFreeOn s₂ n → G.CliqueFreeOn s₁ n
-- Mathlib.Analysis.SpecificLimits.Normed
mul_neg_geom_series : ∀ {R : Type u_4} [inst : NormedRing R] [HasSummableGeomSeries R] (x : R), ‖x‖ < 1 → (1 - x) * ∑' (i : ℕ), x ^ i = 1
-- Mathlib.Analysis.Calculus.Gradient.Basic
_private.Mathlib.Analysis.Calculus.Gradient.Basic.0.«term⟪_,_⟫» : Lean.ParserDescr
-- Mathlib.LinearAlgebra.Matrix.Reindex
Matrix.coe_reindexAddEquiv : ∀ {m : Type u_2} {n : Type u_3} {m' : Type u_6} {n' : Type u_7} (R : Type u_11) [inst : Add R] (eₘ : m ≃ m')
  (eₙ : n ≃ n'), ⇑(Matrix.reindexAddEquiv R eₘ eₙ) = ⇑(Matrix.reindex eₘ eₙ)
-- Mathlib.AlgebraicGeometry.Morphisms.Constructors
AlgebraicGeometry.topologically_isZariskiLocalAtSource : ∀ (P : {α β : Type u} → [TopologicalSpace α] → [TopologicalSpace β] → (α → β) → Prop)
  [(AlgebraicGeometry.topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] => P).RespectsIso],
  (∀ {X Y : Type u} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : X → Y),
      Continuous f → ∀ (U : TopologicalSpace.Opens X), P f → P (f ∘ Subtype.val)) →
    (∀ {X Y : Type u} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : X → Y),
        Continuous f →
          ∀ {ι : Type u} (U : ι → TopologicalSpace.Opens X),
            TopologicalSpace.IsOpenCover U → (∀ (i : ι), P (f ∘ Subtype.val)) → P f) →
      AlgebraicGeometry.IsZariskiLocalAtSource
        (AlgebraicGeometry.topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] => P)
-- Mathlib.CategoryTheory.Monoidal.Closed.Cartesian
CategoryTheory.zeroMul_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] {A : C}
  [inst_2 : CategoryTheory.Closed A] {I : C} (t : CategoryTheory.Limits.IsInitial I),
  (CategoryTheory.zeroMul t).hom = CategoryTheory.SemiCartesianMonoidalCategory.snd A I
-- Mathlib.Algebra.Order.Module.HahnEmbedding
/-- For each `FiniteArchimedeanClass`, specify a corresponding submodule.  -/
HahnEmbedding.ArchimedeanStrata.stratum : {K : Type u_1} →
  [inst : DivisionRing K] →
    [inst_1 : LinearOrder K] →
      [inst_2 : IsOrderedRing K] →
        [inst_3 : Archimedean K] →
          {M : Type u_2} →
            [inst_4 : AddCommGroup M] →
              [inst_5 : LinearOrder M] →
                [inst_6 : IsOrderedAddMonoid M] →
                  [inst_7 : Module K M] →
                    [inst_8 : IsOrderedModule K M] →
                      HahnEmbedding.ArchimedeanStrata K M → FiniteArchimedeanClass M → Submodule K M
-- Init.MetaTypes
Lean.NameGenerator.namePrefix : Lean.NameGenerator → Lean.Name
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Real.inv_logb_div_base : ∀ {a b : ℝ}, a ≠ 0 → b ≠ 0 → ∀ (c : ℝ), (Real.logb (a / b) c)⁻¹ = (Real.logb a c)⁻¹ - (Real.logb b c)⁻¹
-- Mathlib.Topology.Order.CountableSeparating
Filter.EventuallyEq.of_forall_eventually_gt_iff : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : LinearOrder X] [OrderTopology X] [SecondCountableTopology X]
  {α : Type u_2} {l : Filter α} [CountableInterFilter l] {f g : α → X},
  (∀ (x : X), ∀ᶠ (a : α) in l, x < f a ↔ x < g a) → f =ᶠ[l] g
-- Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
AlgebraicGeometry.IsClosedImmersion.lift.congr_simp : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f f_1 : X ⟶ Z) (e_f : f = f_1) (g g_1 : Y ⟶ Z) (e_g : g = g_1)
  [inst : AlgebraicGeometry.IsClosedImmersion f]
  (H : AlgebraicGeometry.Scheme.Hom.ker f ≤ AlgebraicGeometry.Scheme.Hom.ker g),
  AlgebraicGeometry.IsClosedImmersion.lift f g H = AlgebraicGeometry.IsClosedImmersion.lift f_1 g_1 ⋯
-- Mathlib.Combinatorics.Enumerative.Partition.Basic
/-- The number of times a positive integer `i` appears in the partition `ofSums n l hl` is the same
as the number of times it appears in the multiset `l`.
(For `i = 0`, `Partition.non_zero` combined with `Multiset.count_eq_zero_of_notMem` gives that
this is `0` instead.)
 -/
Nat.Partition.count_ofSums_of_ne_zero : ∀ {n : ℕ} {l : Multiset ℕ} (hl : l.sum = n) {i : ℕ},
  i ≠ 0 → Multiset.count i (Nat.Partition.ofSums n l hl).parts = Multiset.count i l
-- Mathlib.Combinatorics.Derangements.Exponential
numDerangements_tendsto_inv_e : Filter.Tendsto (fun n => ↑(numDerangements n) / ↑n.factorial) Filter.atTop (nhds (Real.exp (-1)))
-- Init.Tactics
/-- `done` succeeds iff there are no remaining goals.  -/
Lean.Parser.Tactic.done : Lean.ParserDescr
-- Mathlib.Algebra.BigOperators.Group.List.Basic
/-- A non-commutative variant of `List.prod_reverse`  -/
List.prod_reverse_noncomm : ∀ {G : Type u_7} [inst : Group G] (L : List G), L.reverse.prod = (List.map (fun x => x⁻¹) L).prod⁻¹
-- Mathlib.Order.Filter.ENNReal
NNReal.isCoboundedUnder_ge_toReal : ∀ {ι : Type u_1} {f : Filter ι} {u : ι → NNReal},
  (Filter.IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) f fun i => ↑(u i)) ↔
    Filter.IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) f u
-- Std.Http.Data.Body.Length
Std.Http.Body.instBEqLength.beq : Std.Http.Body.Length → Std.Http.Body.Length → Bool
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.max!_insert : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.WF → ∀ {k : α}, (t.insert k).max! = t.max?.elim k fun k' => if cmp k' k = Ordering.lt then k else k'
-- Mathlib.Topology.Instances.NNReal.Lemmas
NNReal.isOpen_Ico_zero : ∀ {x : NNReal}, IsOpen (Set.Ico 0 x)
-- Lean.Data.Lsp.CodeActions
Lean.Lsp.CodeActionClientCapabilities.mk.inj : ∀ {dynamicRegistration? isPreferredSupport? disabledSupport? dataSupport? honorsChangeAnnotations? : Option Bool}
  {codeActionLiteralSupport? : Option Lean.Lsp.CodeActionLiteralSupport}
  {resolveSupport? : Option Lean.Lsp.ResolveSupport}
  {dynamicRegistration?_1 isPreferredSupport?_1 disabledSupport?_1 dataSupport?_1 honorsChangeAnnotations?_1 :
    Option Bool}
  {codeActionLiteralSupport?_1 : Option Lean.Lsp.CodeActionLiteralSupport}
  {resolveSupport?_1 : Option Lean.Lsp.ResolveSupport},
  { dynamicRegistration? := dynamicRegistration?, isPreferredSupport? := isPreferredSupport?,
        disabledSupport? := disabledSupport?, dataSupport? := dataSupport?,
        honorsChangeAnnotations? := honorsChangeAnnotations?, codeActionLiteralSupport? := codeActionLiteralSupport?,
        resolveSupport? := resolveSupport? } =
      { dynamicRegistration? := dynamicRegistration?_1, isPreferredSupport? := isPreferredSupport?_1,
        disabledSupport? := disabledSupport?_1, dataSupport? := dataSupport?_1,
        honorsChangeAnnotations? := honorsChangeAnnotations?_1,
        codeActionLiteralSupport? := codeActionLiteralSupport?_1, resolveSupport? := resolveSupport?_1 } →
    dynamicRegistration? = dynamicRegistration?_1 ∧
      isPreferredSupport? = isPreferredSupport?_1 ∧
        disabledSupport? = disabledSupport?_1 ∧
          dataSupport? = dataSupport?_1 ∧
            honorsChangeAnnotations? = honorsChangeAnnotations?_1 ∧
              codeActionLiteralSupport? = codeActionLiteralSupport?_1 ∧ resolveSupport? = resolveSupport?_1
-- Mathlib.NumberTheory.Modular
/-- non-strict variant of `ModularGroup.three_le_four_mul_im_sq_of_mem_fdo`  -/
ModularGroup.three_le_four_mul_im_sq_of_mem_fd : ∀ {τ : UpperHalfPlane}, τ ∈ ModularGroup.fd → 3 ≤ 4 * τ.im ^ 2
-- Mathlib.RingTheory.Polynomial.ShiftedLegendre
/-- The values of the Legendre polynomial at `x` and `1 - x` differ by a factor `(-1)ⁿ`.  -/
Polynomial.shiftedLegendre_eval_symm : ∀ (n : ℕ) {R : Type u_1} [inst : Ring R] (x : R),
  (Polynomial.aeval x) (Polynomial.shiftedLegendre n) =
    (-1) ^ n * (Polynomial.aeval (1 - x)) (Polynomial.shiftedLegendre n)
-- Mathlib.MeasureTheory.Measure.Map
MeasureTheory.Measure.map_id : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α}, MeasureTheory.Measure.map id μ = μ
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.Hom.inv_app : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : CategoryTheory.IsIso f] (U : X.Opens),
  AlgebraicGeometry.Scheme.Hom.app (CategoryTheory.inv f) U =
    CategoryTheory.CategoryStruct.comp (X.presheaf.map (CategoryTheory.eqToHom ⋯).op)
      (CategoryTheory.inv
        (AlgebraicGeometry.Scheme.Hom.app f ((TopologicalSpace.Opens.map (CategoryTheory.inv f).base).obj U)))
-- Mathlib.MeasureTheory.Integral.Indicator
/-- If `μ` is a finite measure and the indicators of measurable sets `Aᵢ` tend pointwise to
the indicator of a set `A`, then the measures `μ Aᵢ` tend to the measure `μ A`.  -/
MeasureTheory.tendsto_measure_of_tendsto_indicator_of_isFiniteMeasure : ∀ {α : Type u_1} [inst : MeasurableSpace α] {A : Set α} {ι : Type u_2} (L : Filter ι) [L.IsCountablyGenerated]
  {As : ι → Set α} (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ],
  (∀ (i : ι), MeasurableSet (As i)) →
    (∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A) → Filter.Tendsto (fun i => μ (As i)) L (nhds (μ A))
-- Mathlib.MeasureTheory.Constructions.Polish.Basic
MeasureTheory.AnalyticSet.image_of_continuous : ∀ {α : Type u_1} [inst : TopologicalSpace α] {β : Type u_3} [inst_1 : TopologicalSpace β] {s : Set α},
  MeasureTheory.AnalyticSet s → ∀ {f : α → β}, Continuous f → MeasureTheory.AnalyticSet (f '' s)
-- Mathlib.CategoryTheory.Sites.Hypercover.ZeroFamily
CategoryTheory.PreZeroHypercoverFamily.iff_shrink : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (self : CategoryTheory.PreZeroHypercoverFamily C) {X : C}
  {E : CategoryTheory.PreZeroHypercover X}, self.property E ↔ self.property E.shrink
-- Mathlib.Combinatorics.Hypergraph.Basic
/-- `E(H)` denotes the `edgeSet` of a hypergraph `H`  -/
Hypergraph.«termE(_)» : Lean.ParserDescr
-- Init.Grind.AC
Lean.Grind.AC.Seq.denote_sort' : ∀ {α : Sort u_1} (ctx : Lean.Grind.AC.Context α) {inst₁ : Std.Associative ctx.op} {inst₂ : Std.Commutative ctx.op}
  (s acc : Lean.Grind.AC.Seq),
  Lean.Grind.AC.Seq.denote ctx (s.sort' acc) =
    ctx.op (Lean.Grind.AC.Seq.denote ctx s) (Lean.Grind.AC.Seq.denote ctx acc)
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitDisc.instCoe : Coe Complex.UnitDisc ℂ
-- Lean.Parser.Extra
Lean.Parser.setExpected.formatter : List String → Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter
-- Init.Data.UInt.Lemmas
UInt8.toBitVec_ofNatTruncate_of_le : ∀ {n : ℕ}, UInt8.size ≤ n → (UInt8.ofNatClamp n).toBitVec = (UInt8.size - 1)#'UInt8.toBitVec_ofNatClamp_of_le._proof_1
-- Mathlib.Data.List.MinMax
/-- The minimum value in a non-empty `List`.  -/
List.minimum_of_length_pos : {α : Type u_1} → [LinearOrder α] → {l : List α} → 0 < l.length → α
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
/-- The equivalence between `integerSet K` and the product of the set of nonzero principal
ideals of `K` and the torsion of `K`.  -/
NumberField.mixedEmbedding.fundamentalCone.integerSetEquiv : (K : Type u_1) →
  [inst : Field K] →
    [inst_1 : NumberField K] →
      ↑(NumberField.mixedEmbedding.fundamentalCone.integerSet K) ≃
        { I // Submodule.IsPrincipal ↑I } × ↥(NumberField.Units.torsion K)
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.vle_trans' : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R] {x y z : R}, y ≤ᵥ z → x ≤ᵥ y → x ≤ᵥ z
-- Mathlib.Algebra.Group.Submonoid.Units
Subgroup.exists_mem_ofUnits_val_eq : ∀ {M : Type u_1} [inst : Monoid M] (S : Subgroup Mˣ) {x : M}, x ∈ S.ofUnits → ∃ y ∈ S, ↑y = x
-- Mathlib.Algebra.DirectSum.Basic
DirectSum.sigmaFiberAddEquiv_apply : ∀ {ι₁ ι₂ : Type v} [inst : DecidableEq ι₂] (f : ι₁ → ι₂) {β : ι₁ → Type w} [inst_1 : (i : ι₁) → AddCommMonoid (β i)]
  (x : DirectSum ι₁ fun i => β i),
  (DirectSum.sigmaFiberAddEquiv f) x =
    DirectSum.sigmaCurry ((DirectSum.equivCongrLeft (Equiv.sigmaFiberEquiv f).symm) x)
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.Attach
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.Attach.0.Std.Iterators.Types.Attach.Monadic.modifyStep.match_1.eq_1 : ∀ {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [inst : Std.Iterator α m β] {P : β → Prop}
  (it : Std.IterM m { out // P out }) (motive : it.internalState.inner.Step → Sort u_3) (it' : Std.IterM m β) (out : β)
  (h : it.internalState.inner.IsPlausibleStep (Std.IterStep.yield it' out))
  (h_1 :
    (it' : Std.IterM m β) →
      (out : β) →
        (h : it.internalState.inner.IsPlausibleStep (Std.IterStep.yield it' out)) →
          motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 :
    (it' : Std.IterM m β) →
      (h : it.internalState.inner.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (property : it.internalState.inner.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, property⟩),
  (match ⟨Std.IterStep.yield it' out, h⟩ with
    | ⟨Std.IterStep.yield it' out, h⟩ => h_1 it' out h
    | ⟨Std.IterStep.skip it', h⟩ => h_2 it' h
    | ⟨Std.IterStep.done, property⟩ => h_3 property) =
    h_1 it' out h
-- Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic
/-- Transport a `NormalMono` structure via an isomorphism of arrows.  -/
CategoryTheory.NormalMono.ofArrowIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} →
        {f : X ⟶ Y} →
          CategoryTheory.NormalMono f →
            {X' Y' : C} →
              {f' : X' ⟶ Y'} → (CategoryTheory.Arrow.mk f ≅ CategoryTheory.Arrow.mk f') → CategoryTheory.NormalMono f'
-- Mathlib.Topology.UniformSpace.Equicontinuity
uniformEquicontinuous_unique : ∀ {ι : Type u_1} {α : Type u_6} {β : Type u_8} [uα : UniformSpace α] [uβ : UniformSpace β] [inst : Unique ι]
  {F : ι → β → α}, UniformEquicontinuous F ↔ UniformContinuous (F default)
-- Init.Data.UInt.Bitwise
UInt64.toNat_shiftLeft : ∀ (a b : UInt64), (a <<< b).toNat = a.toNat <<< (b.toNat % 64) % 2 ^ 64
-- Mathlib.Analysis.Analytic.ConvergenceRadius
FormalMultilinearSeries.const_smul_sum_apply : ∀ {𝕜 : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Semiring 𝕜] [inst_1 : AddCommMonoid E] [inst_2 : AddCommMonoid F]
  [inst_3 : Module 𝕜 E] [inst_4 : Module 𝕜 F] [inst_5 : TopologicalSpace E] [inst_6 : TopologicalSpace F]
  [inst_7 : ContinuousAdd E] [inst_8 : ContinuousAdd F] [inst_9 : ContinuousConstSMul 𝕜 E]
  [inst_10 : ContinuousConstSMul 𝕜 F] {𝕜' : Type} [inst_11 : DivisionSemiring 𝕜'] [inst_12 : Module 𝕜' F]
  [inst_13 : ContinuousConstSMul 𝕜' F] [inst_14 : SMulCommClass 𝕜 𝕜' F] [T2Space F] (a : 𝕜')
  (f : FormalMultilinearSeries 𝕜 E F) (z : E), a • f.sum z = (a • f).sum z
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MultispanIndex.toLinearOrder_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {ι : Type w}
  (I : CategoryTheory.Limits.MultispanIndex (CategoryTheory.Limits.MultispanShape.prod ι) C) [inst_1 : LinearOrder ι]
  (i : (CategoryTheory.Limits.MultispanShape.ofLinearOrder ι).R), I.toLinearOrder.right i = I.right i