mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Finset.Powerset
Finset.image_surjOn_powerset : ∀ {α : Type u_1} {s : Finset α} {β : Type u_2} [inst : DecidableEq β] {f : α → β},
  Set.SurjOn (fun x => Finset.image f x) ↑s.powerset ↑(Finset.image f s).powerset
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.vadd_set_iUnion : ∀ {α : Type u_2} {β : Type u_3} {ι : Sort u_5} [inst : VAdd α β] (a : α) (s : ι → Set β), a +ᵥ ⋃ i, s i = ⋃ i, a +ᵥ s i
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.Nontrivial.mul : ∀ {α : Type u_2} [inst : Mul α] [IsLeftCancelMul α] {s t : Set α}, s.Nontrivial → t.Nontrivial → (s * t).Nontrivial
-- Mathlib.AlgebraicGeometry.Group.Affine
AlgebraicGeometry.specOverSpec.eq_1 : ∀ {R A : CommRingCat} [inst : Algebra ↑R ↑A],
  AlgebraicGeometry.specOverSpec = { hom := AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap ↑R ↑A)) }
-- Mathlib.Order.Ideal
Order.Ideal.mk.inj : ∀ {P : Type u_2} {inst : LE P} {toLowerSet : LowerSet P} {nonempty' : toLowerSet.carrier.Nonempty}
  {directed' : DirectedOn (fun x1 x2 => x1 ≤ x2) toLowerSet.carrier} {toLowerSet_1 : LowerSet P}
  {nonempty'_1 : toLowerSet_1.carrier.Nonempty} {directed'_1 : DirectedOn (fun x1 x2 => x1 ≤ x2) toLowerSet_1.carrier},
  { toLowerSet := toLowerSet, nonempty' := nonempty', directed' := directed' } =
      { toLowerSet := toLowerSet_1, nonempty' := nonempty'_1, directed' := directed'_1 } →
    toLowerSet = toLowerSet_1
-- Mathlib.FieldTheory.Differential.Basic
Differential.logDeriv_zero : ∀ {R : Type u_1} [inst : Field R] [inst_1 : Differential R], Differential.logDeriv 0 = 0
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.RuleExpr.brecOn_2.eq : ∀ {motive_1 : Aesop.Frontend.RuleExpr → Sort u} {motive_2 : Array Aesop.Frontend.RuleExpr → Sort u}
  {motive_3 : List Aesop.Frontend.RuleExpr → Sort u} (t : List Aesop.Frontend.RuleExpr)
  (F_1 : (t : Aesop.Frontend.RuleExpr) → t.below → motive_1 t)
  (F_2 : (t : Array Aesop.Frontend.RuleExpr) → Aesop.Frontend.RuleExpr.below_1 t → motive_2 t)
  (F_3 : (t : List Aesop.Frontend.RuleExpr) → Aesop.Frontend.RuleExpr.below_2 t → motive_3 t),
  Aesop.Frontend.RuleExpr.brecOn_2 t F_1 F_2 F_3 = F_3 t (Aesop.Frontend.RuleExpr.brecOn_2.go t F_1 F_2 F_3).2
-- Std.Data.DTreeMap.Basic
/-- Returns the key-value pair with the `n`-th smallest key, or `none` if `n` is at least `t.size`.  -/
Std.DTreeMap.Const.entryAtIdx? : {α : Type u} → {cmp : α → α → Ordering} → {β : Type v} → Std.DTreeMap α (fun x => β) cmp → ℕ → Option (α × β)
-- Mathlib.CategoryTheory.Galois.Decomposition
/-- In a Galois category, every object is the sum of connected objects.  -/
CategoryTheory.PreGaloisCategory.has_decomp_connected_components' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] [inst_1 : CategoryTheory.GaloisCategory C] (X : C),
  ∃ ι, ∃ (x : Finite ι), ∃ f x, ∀ (i : ι), CategoryTheory.PreGaloisCategory.IsConnected (f i)
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.dropWhile_toSlice : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.ForwardPattern pat] {s : String},
  s.toSlice.dropWhile pat = s.dropWhile pat
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.tensorLeftTensor_inv_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X Y Z : C),
  (CategoryTheory.MonoidalCategory.tensorLeftTensor X Y).inv.app Z =
    (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv
-- Init.Data.String.Iterator
String.Pos.Raw.atEnd.eq_1 : ∀ (x : String) (x_1 : String.Pos.Raw), String.Pos.Raw.atEnd x x_1 = decide (x_1.byteIdx ≥ x.utf8ByteSize)
-- Mathlib.Algebra.Homology.ComplexShape
/-- An arbitrary choice of index `i` such that `Rel i j`, if such exists.
Returns `j` otherwise.
 -/
ComplexShape.prev : {ι : Type u_1} → ComplexShape ι → ι → ι
-- Batteries.Data.List.Lemmas
List.findIdxNth_lt_length_of_lt_countP : ∀ {α : Type u_1} {n : ℕ} {p : α → Bool} {xs : List α}, n < List.countP p xs → List.findIdxNth p xs n < xs.length
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
SimpleGraph.ConnectedComponent.spanningCoe_toSubgraph : ∀ {V : Type u} {G : SimpleGraph V} (C : G.ConnectedComponent), C.toSubgraph.spanningCoe = C.toSimpleGraph.spanningCoe
-- Mathlib.Analysis.Normed.Unbundled.SpectralNorm
spectralValueTerms_of_lt_natDegree : ∀ {R : Type u_1} [inst : SeminormedRing R] (p : Polynomial R) {n : ℕ},
  n < p.natDegree → spectralValueTerms p n = ‖p.coeff n‖ ^ (1 / (↑p.natDegree - ↑n))
-- Mathlib.Topology.Compactness.CompactlyGeneratedSpace
/-- The quotient of a compactly generated space is compactly generated.  -/
instUCompactlyGeneratedSpaceQuotient : ∀ {X : Type w} [tX : TopologicalSpace X] {S : Setoid X} [UCompactlyGeneratedSpace X],
  UCompactlyGeneratedSpace (Quotient S)
-- Mathlib.Data.Finsupp.MonomialOrder
instIsOrderedCancelAddMonoidLexFinsupp : ∀ {α : Type u_1} {N : Type u_2} [inst : LinearOrder α] [inst_1 : AddCommMonoid N] [inst_2 : PartialOrder N]
  [IsOrderedCancelAddMonoid N], IsOrderedCancelAddMonoid (Lex (α →₀ N))
-- Lean.Level
Lean.Level.PP.Result.offset.inj : ∀ {a : Lean.Level.PP.Result} {a_1 : ℕ} {a_2 : Lean.Level.PP.Result} {a_3 : ℕ},
  a.offset a_1 = a_2.offset a_3 → a = a_2 ∧ a_1 = a_3
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.minKey?_eq_some_minKey! : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.isEmpty = false → t.minKey? = some t.minKey!
-- Mathlib.Topology.NoetherianSpace
TopologicalSpace.instNoetherianSpaceOfIndiscreteTopology : ∀ {α : Type u_1} [inst : TopologicalSpace α] [IndiscreteTopology α], TopologicalSpace.NoetherianSpace α
-- Mathlib.RingTheory.RingInvo
RingInvoClass.toRingEquivClass : ∀ {F : Type u_3} {R : Type u_4} {inst : Semiring R} {inst_1 : EquivLike F R Rᵐᵒᵖ} [self : RingInvoClass F R],
  RingEquivClass F R Rᵐᵒᵖ
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.iUnion_add_right_image : ∀ {α : Type u_2} [inst : Add α] {s t : Set α}, ⋃ a ∈ t, (fun x => x + a) '' s = s + t
-- Mathlib.Analysis.Calculus.FDeriv.Pow
DifferentiableAt.pow : ∀ {𝕜 : Type u_1} {𝔸 : Type u_2} {E : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedRing 𝔸]
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedAlgebra 𝕜 𝔸] [inst_4 : NormedSpace 𝕜 E] {f : E → 𝔸} {x : E},
  DifferentiableAt 𝕜 f x → ∀ (n : ℕ), DifferentiableAt 𝕜 (f ^ n) x
-- Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Dynamics.isDynNetIn_empty : ∀ {X : Type u_1} {T : X → X} {U : SetRel X X} {n : ℕ} {F : Set X}, Dynamics.IsDynNetIn T F U n ∅
-- Mathlib.Topology.NhdsSet
union_mem_nhdsSet : ∀ {X : Type u_2} [inst : TopologicalSpace X] {s₁ s₂ t₁ t₂ : Set X},
  s₁ ∈ nhdsSet t₁ → s₂ ∈ nhdsSet t₂ → s₁ ∪ s₂ ∈ nhdsSet (t₁ ∪ t₂)
-- Init.Data.String.Lemmas.Pattern.String.ForwardSearcher
/-- This is the key lemma for the correctness of KMP. Given a partial match of `pat` in `s`, it shows
that all shorter partial matches of `pat` in `s` ending at the same position are described by
partial matches of `pat` in itself.
 -/
_private.Init.Data.String.Lemmas.Pattern.String.ForwardSearcher.0.String.Slice.Pattern.Model.ForwardSliceSearcher.PartialMatch.partialMatch_iff : ∀ {pat s : ByteArray} {stackPos needlePos : ℕ},
  String.Slice.Pattern.Model.ForwardSliceSearcher.PartialMatch✝ pat s needlePos stackPos →
    ∀ {needlePos' : ℕ},
      String.Slice.Pattern.Model.ForwardSliceSearcher.PartialMatch✝ pat pat needlePos' needlePos ↔
        needlePos' ≤ needlePos ∧ String.Slice.Pattern.Model.ForwardSliceSearcher.PartialMatch✝ pat s needlePos' stackPos
-- Mathlib.Data.Multiset.Count
Multiset.count.congr_simp : ∀ {α : Type u_1} {inst : DecidableEq α} [inst_1 : DecidableEq α] (a a_1 : α),
  a = a_1 → ∀ (a_2 a_3 : Multiset α), a_2 = a_3 → Multiset.count a a_2 = Multiset.count a_1 a_3
-- Mathlib.Data.Multiset.AddSub
/-- This is a special case of `tsub_le_iff_right`, which should be used instead of this.
This is needed to prove `OrderedSub (Multiset α)`.  -/
Multiset.sub_le_iff_le_add : ∀ {α : Type u_1} [inst : DecidableEq α] {s t u : Multiset α}, s - t ≤ u ↔ s ≤ u + t
-- Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset
Finset.smul_finset_subset_iff₀ : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] [inst_1 : GroupWithZero α] [inst_2 : MulAction α β]
  {s t : Finset β} {a : α}, a ≠ 0 → (a • s ⊆ t ↔ s ⊆ a⁻¹ • t)
-- Mathlib.AlgebraicGeometry.Morphisms.Immersion
/-- A morphism of schemes `f : X ⟶ Y` is an immersion if
1. the underlying map of topological spaces is an embedding
2. the range of the map is locally closed
3. the induced morphisms of stalks are all surjective.  -/
AlgebraicGeometry.IsImmersion : {X Y : AlgebraicGeometry.Scheme} → (X ⟶ Y) → Prop
-- Mathlib.Algebra.Homology.ShortComplex.Limits
CategoryTheory.ShortComplex.instPreservesLimitπ₂ : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  (F : CategoryTheory.Functor J (CategoryTheory.ShortComplex C))
  [CategoryTheory.Limits.HasLimit (F.comp CategoryTheory.ShortComplex.π₁)]
  [CategoryTheory.Limits.HasLimit (F.comp CategoryTheory.ShortComplex.π₂)]
  [CategoryTheory.Limits.HasLimit (F.comp CategoryTheory.ShortComplex.π₃)],
  CategoryTheory.Limits.PreservesLimit F CategoryTheory.ShortComplex.π₂
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
/-- Change of variables for continuous integrands. If `f` is continuous on `[a, b]` and has
continuous right-derivative `f'` in `(a, b)`, and `g` is continuous on `f '' [a, b]` then we can
substitute `u = f x` to get `∫ x in a..b, (g ∘ f) x * f' x = ∫ u in f a..f b, g u`.
 -/
intervalIntegral.integral_comp_mul_deriv'' : ∀ {a b : ℝ} {f f' g : ℝ → ℝ},
  ContinuousOn f (Set.uIcc a b) →
    (∀ x ∈ Set.Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Set.Ioi x) x) →
      ContinuousOn f' (Set.uIcc a b) →
        ContinuousOn g (f '' Set.uIcc a b) → ∫ (x : ℝ) in a..b, (g ∘ f) x * f' x = ∫ (u : ℝ) in f a..f b, g u
-- Mathlib.CategoryTheory.Preadditive.Biproducts
/-- A preadditive category with finite products has finite biproducts.  -/
CategoryTheory.Limits.HasFiniteBiproducts.of_hasFiniteProducts : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [CategoryTheory.Limits.HasFiniteProducts C], CategoryTheory.Limits.HasFiniteBiproducts C
-- Mathlib.RepresentationTheory.Continuous.Basic
ContRepresentation.coind₁_apply_apply : ∀ {R : Type u_1} {V : Type u_3} [inst : Ring R] [inst_1 : AddCommGroup V] [inst_2 : TopologicalSpace V]
  [inst_3 : IsTopologicalAddGroup V] [inst_4 : Module R V] {G : Type u_7} [inst_5 : Group G]
  [inst_6 : TopologicalSpace G] [inst_7 : TopologicalSpace R] [inst_8 : ContinuousSMul R V]
  [inst_9 : IsTopologicalGroup G] (π : ContRepresentation R G V) (g : G) (f : C(G, V)) (x : G),
  ((π.coind₁ g) f) x = (π g) (f (g⁻¹ * x))
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.trStmts₁.eq_3 : ∀ (q : Option Turing.PartrecToTM2.Γ' → Turing.PartrecToTM2.Λ'),
  Turing.PartrecToTM2.trStmts₁ (Turing.PartrecToTM2.Λ'.read q) =
    insert (Turing.PartrecToTM2.Λ'.read q) (Finset.univ.biUnion fun s => Turing.PartrecToTM2.trStmts₁ (q s))
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey?_union!_of_contains_eq_false_right : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  m₁.WF → m₂.WF → ∀ {k : α}, Std.DTreeMap.Internal.Impl.contains k m₂ = false → (m₁.union! m₂).getKey? k = m₁.getKey? k
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
/-- Given a rank function `f : P.RankFunction ι` for a
pairing `P` of a subcomplex `A` of `X : SSet`, and `i : ι`,
this is the type of type (II) simplices of rank `i`.  -/
SSet.Subcomplex.Pairing.RankFunction.Cell : {X : SSet} →
  {A : X.Subcomplex} → {P : A.Pairing} → {ι : Type v} → [inst : LinearOrder ι] → P.RankFunction ι → ι → Type u
-- Std.Do.WP.SimpLemmas
_private.Std.Do.WP.SimpLemmas.0.Except.map.match_1.splitter : {ε : Type u_1} →
  {α : Type u_2} →
    (motive : Except ε α → Sort u_3) →
      (x : Except ε α) → ((err : ε) → motive (Except.error err)) → ((v : α) → motive (Except.ok v)) → motive x
-- Mathlib.Computability.StateTransition
/-- Transitivity of `EvalsTo` in the sum of the numbers of steps.  -/
StateTransition.EvalsTo.trans : {σ : Type u_1} →
  (f : σ → Option σ) →
    (a b : σ) →
      (c : Option σ) →
        StateTransition.EvalsTo f a (some b) → StateTransition.EvalsTo f b c → StateTransition.EvalsTo f a c
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
SimplexCategory.Truncated.incl.congr_simp : ∀ (n m : ℕ) (h : n ≤ m), SimplexCategory.Truncated.incl n m h = SimplexCategory.Truncated.incl n m h
-- Mathlib.Logic.Equiv.Defs
EquivLike.coe_symm_comp_self : ∀ {α : Sort u} {β : Sort v} {F : Sort u_1} [inst : EquivLike F α β] (e : F), ⇑(↑e).symm ∘ ⇑e = id
-- Mathlib.Data.Nat.MaxPowDiv
/-- **Alias** of `pow_padicValNat_dvd`. -/
Nat.maxPowDiv.pow_dvd : ∀ {p n : ℕ}, p ^ padicValNat p n ∣ n
-- Mathlib.Order.Interval.Set.Basic
Set.instIccUnique : {α : Type u_1} → [inst : PartialOrder α] → {a : α} → Unique ↑(Set.Icc a a)
-- Mathlib.Combinatorics.Quiver.Symmetric
Quiver.Symmetrify.of_obj : ∀ {V : Type u_2} [inst : Quiver V] (a : V), Quiver.Symmetrify.of.obj a = id a
-- Mathlib.RingTheory.RootsOfUnity.Basic
rootsOfUnity_inf_rootsOfUnity : ∀ {M : Type u_1} [inst : CommMonoid M] {m n : ℕ}, rootsOfUnity m M ⊓ rootsOfUnity n M = rootsOfUnity (m.gcd n) M
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.get!_diff_of_not_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited β], t₁.WF → t₂.WF → ∀ {k : α}, k ∉ t₂ → (t₁ \ t₂).get! k = t₁.get! k
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKeyD_insertList : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l toInsert : List ((a : α) × β a)} {k fallback : α},
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.DistinctKeys toInsert →
      Std.Internal.List.getKeyD k (Std.Internal.List.insertList l toInsert) fallback =
        Std.Internal.List.getKeyD k toInsert (Std.Internal.List.getKeyD k l fallback)
-- Mathlib.Analysis.Asymptotics.Theta
Asymptotics.isTheta_rfl : ∀ {α : Type u_1} {E : Type u_3} [inst : Norm E] {f : α → E} {l : Filter α}, f =Θ[l] f
-- Mathlib.CategoryTheory.Shift.CommShiftTwo
CategoryTheory.Functor.CommShift₂.commShift_map : ∀ {C₁ : Type u_1} {C₂ : Type u_3} {D : Type u_5} {inst : CategoryTheory.Category.{v_1, u_1} C₁}
  {inst_1 : CategoryTheory.Category.{v_3, u_3} C₂} {inst_2 : CategoryTheory.Category.{v_5, u_5} D} {M : Type u_6}
  {inst_3 : AddCommMonoid M} {inst_4 : CategoryTheory.HasShift C₁ M} {inst_5 : CategoryTheory.HasShift C₂ M}
  {inst_6 : CategoryTheory.HasShift D M} {G : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)}
  {h : CategoryTheory.CommShift₂Setup D M} [self : G.CommShift₂ h] {X₁ Y₁ : C₁} (f : X₁ ⟶ Y₁),
  CategoryTheory.NatTrans.CommShift (G.map f) M
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime
/-- The functor `F.DescentData f ⥤ F.DescentData' sq sq₃`.  -/
CategoryTheory.Pseudofunctor.DescentData'.fromDescentDataFunctor : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat) →
      {ι : Type t} →
        {S : C} →
          {X : ι → C} →
            {f : (i : ι) → X i ⟶ S} →
              (sq : (i j : ι) → CategoryTheory.Limits.ChosenPullback (f i) (f j)) →
                (sq₃ : (i₁ i₂ i₃ : ι) → CategoryTheory.Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)) →
                  CategoryTheory.Functor (F.DescentData f) (F.DescentData' sq sq₃)
-- Lean.Data.Options
Lean.instMonadWithOptionsOfMonadFunctor : {m n : Type → Type} → [MonadFunctor m n] → [Lean.MonadWithOptions m] → Lean.MonadWithOptions n
-- Mathlib.Analysis.Complex.Exponential
Real.one_sub_lt_exp_neg : ∀ {x : ℝ}, x ≠ 0 → 1 - x < Real.exp (-x)
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.HasRightHomology.of_hasCokernel_of_hasKernel : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} [inst_2 : CategoryTheory.Limits.HasCokernel S.f]
  [CategoryTheory.Limits.HasKernel (CategoryTheory.Limits.cokernel.desc S.f S.g ⋯)], S.HasRightHomology
-- Lean.Meta.Tactic.Grind.EMatch
_private.Lean.Meta.Tactic.Grind.EMatch.0.Lean.Meta.Grind.EMatch.Choice.updateGen : Lean.Meta.Grind.EMatch.Choice → ℕ → Lean.Meta.Grind.EMatch.Choice
-- Std.Internal.Do.Order.PreservesSup
/-- Landing below the frame closure, transposed across the Galois connection: `pre ⊑ frameClosure op k Q`
holds exactly when `op r pre ⊑ k (fun a => op r (Q a))` for every resource `r`. At a unit resource
(`op e = id`) the `r = e` conjunct is `pre ⊑ k Q`; the remaining conjuncts are the frame conditions on
`pre`, so a `pre` that cannot frame is forced down to the trivial `⊥`.  -/
Lean.Order.PreservesSup.le_frameClosure_iff : ∀ {α : Type u} [inst : Lean.Order.CompleteLattice α] {R : Type v} {β : Type w} (op : R → α → α)
  [∀ (r : R), Lean.Order.PreservesSup (op r)] (k : (β → α) → α) {Q : β → α} {pre : α},
  Lean.Order.PartialOrder.rel pre (Lean.Order.PreservesSup.frameClosure op k Q) ↔
    ∀ (r : R), Lean.Order.PartialOrder.rel (op r pre) (k fun a => op r (Q a))
-- Mathlib.Tactic.ClickSuggestions.Util
/-- Given tactic syntax `tac`, compute the text edit that will paste it into the editor.
We return the range that should be replaced, and the new text that will replace it.  -/
Mathlib.Tactic.ClickSuggestions.mkInsertion : Lean.TSyntax `tactic → Mathlib.Tactic.ClickSuggestions.ClickSuggestionsM (Lean.Lsp.Range × String)
-- Init.Data.Vector.Lemmas
Vector.mem_replicate : ∀ {α : Type u_1} {a b : α} {n : ℕ}, b ∈ Vector.replicate n a ↔ n ≠ 0 ∧ b = a
-- Mathlib.Tactic.Tauto
/-- Debug `grind` by identifying places where it does not yet supersede `tauto`.  -/
tautoToGrindRegressions : Mathlib.TacticAnalysis.Config
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
IsCompl.sum_add_sum : ∀ {ι : Type u_1} {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : Fintype ι] {s t : Finset ι},
  IsCompl s t → ∀ (f : ι → M), ∑ i ∈ s, f i + ∑ i ∈ t, f i = ∑ i, f i
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
_private.Lean.PrettyPrinter.Delaborator.TopDownAnalyze.0.Lean.PrettyPrinter.Delaborator.TopDownAnalyze.analyzeAppStagedCore.applyFunBinderHeuristic.core : Array Lean.Expr →
  Array Lean.Expr →
    Array Lean.BinderInfo → ℕ → Lean.Expr → Lean.PrettyPrinter.Delaborator.TopDownAnalyze.AnalyzeAppM Bool
-- Init.Core
/-- Right injection into the sum type `α ⊕ β`.  -/
Sum.inr : {α : Type u} → {β : Type v} → β → α ⊕ β
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.Internal.List.insertList.eq_def : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (l toInsert : List ((a : α) × β a)),
  Std.Internal.List.insertList l toInsert =
    match toInsert with
    | [] => l
    | ⟨k, v⟩ :: toInsert => Std.Internal.List.insertList (Std.Internal.List.insertEntry k v l) toInsert
-- Mathlib.Analysis.Normed.Operator.Fredholm.Basic
ContinuousLinearMap.FredholmPackage.mapsTo : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : AddCommGroup F] [inst_3 : Module 𝕜 E] [inst_4 : Module 𝕜 F] [inst_5 : TopologicalSpace E]
  [inst_6 : TopologicalSpace F] {u : E →L[𝕜] F} (pkg : u.FredholmPackage), Set.MapsTo ⇑u ↑pkg.decDom.X₁ ↑pkg.decCodom.X₁
-- Lean.PrettyPrinter.Parenthesizer
Lean.PrettyPrinter.CategoryParenthesizer : Type
-- Mathlib.Analysis.SpecialFunctions.Stirling
/-- The sequence `log (stirlingSeq (m + 1)) - log (stirlingSeq (m + 2))` has the series expansion
`∑ 1 / (2 * (k + 1) + 1) * (1 / 2 * (m + 1) + 1)^(2 * (k + 1))`.  -/
Stirling.log_stirlingSeq_sdiff_hasSum : ∀ (m : ℕ),
  HasSum (fun k => 1 / (2 * ↑(k + 1) + 1) * ((1 / (2 * ↑(m + 1) + 1)) ^ 2) ^ (k + 1))
    (Real.log (Stirling.stirlingSeq (m + 1)) - Real.log (Stirling.stirlingSeq (m + 2)))
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
/-- If `x₁ x₂ ... xₙ : E` then `F⟮x₁,x₂,...,xₙ⟯` is the `IntermediateField F E`
generated by these elements.  -/
IntermediateField.«term_⟮_,,⟯» : Lean.TrailingParserDescr
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.size_alter_eq_self_of_not_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k : α} {f : Option (β k) → Option (β k)},
  k ∉ t → (f (t.get? k)).isNone = true → (t.alter k f).size = t.size
-- Init.Omega.Coeffs
Lean.Omega.Coeffs.get_of_length_le : ∀ {i : ℕ} {xs : Lean.Omega.Coeffs}, xs.length ≤ i → xs.get i = 0
-- Mathlib.Algebra.Order.Monovary
monovary_neg_right : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : PartialOrder α] [inst_1 : AddCommGroup β]
  [inst_2 : PartialOrder β] [IsOrderedAddMonoid β] {f : ι → α} {g : ι → β}, Monovary f (-g) ↔ Antivary f g
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
mfderiv_comp_mfderivWithin : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {E'' : Type u_8}
  [inst_11 : NormedAddCommGroup E''] [inst_12 : NormedSpace 𝕜 E''] {H'' : Type u_9} [inst_13 : TopologicalSpace H'']
  {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type u_10} [inst_14 : TopologicalSpace M''] [inst_15 : ChartedSpace H'' M'']
  {f : M → M'} (x : M) {s : Set M} {g : M' → M''},
  MDiffAt g (f x) → MDiffAt[s] f x → UniqueMDiffAt[s] x → mfderiv[s] (g ∘ f) x = mfderiv% g (f x) ∘SL mfderiv[s] f x
-- Mathlib.Topology.Connected.Basic
IsPreconnected.union' : ∀ {α : Type u} [inst : TopologicalSpace α] {s t : Set α},
  (s ∩ t).Nonempty → IsPreconnected s → IsPreconnected t → IsPreconnected (s ∪ t)
-- Mathlib.CategoryTheory.Category.Pairwise
CategoryTheory.Pairwise.Hom.right : {ι : Type v} → (i j : ι) → (CategoryTheory.Pairwise.pair i j).Hom (CategoryTheory.Pairwise.single j)
-- Mathlib.LinearAlgebra.Transvection.Basic
LinearEquiv.transvections_pow_mono : ∀ {R : Type u_1} {V : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup V] [inst_2 : Module R V],
  Monotone fun n => LinearEquiv.transvections R V ^ n
-- Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
LinearIsometryEquiv.ofTop.congr_simp : ∀ (E : Type u_5) [inst : SeminormedAddCommGroup E] {R : Type u_12} [inst_1 : Ring R] [inst_2 : Module R E]
  (p : Submodule R E) (hp : p = ⊤), LinearIsometryEquiv.ofTop E p hp = LinearIsometryEquiv.ofTop E p hp
-- Mathlib.Analysis.Calculus.FDeriv.Norm
DifferentiableAt.fderiv_norm_self : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {x : E},
  DifferentiableAt ℝ (fun x => ‖x‖) x → (fderiv ℝ (fun x => ‖x‖) x) x = ‖x‖
-- Mathlib.Algebra.Lie.Basic
LieModuleEquiv.symm_bijective : ∀ {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : AddCommGroup M] [inst_3 : AddCommGroup N] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : LieRingModule L M] [inst_7 : LieRingModule L N], Function.Bijective LieModuleEquiv.symm
-- Mathlib.Tactic.Abel
Mathlib.Tactic.Abel.zero_smulg : ∀ {α : Type u_1} [inst : AddCommGroup α] (c : ℤ), Mathlib.Tactic.Abel.smulg c 0 = 0
-- Mathlib.Algebra.QuadraticAlgebra.Defs
QuadraticAlgebra.instOne : {R : Type u_1} → {a b : R} → [Zero R] → [One R] → One (QuadraticAlgebra R a b)
-- Aesop.Script.UScriptToSScript
Aesop.Script.instToMessageDataStepTree : Lean.ToMessageData Aesop.Script.StepTree
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.insertC : ℤ → Lean.Grind.CommRing.Mon → Lean.Grind.CommRing.Poly → ℕ → Lean.Grind.CommRing.Poly