mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.DocString.DeferredCheck
/-- A collection of deferred docstring checks.

While docstrings are part of the server olean for a module, deferred checks are part of the public
information so they can be found by the linter.
 -/
Lean.Doc.deferredCheckExt : Lean.PersistentEnvExtension Lean.Doc.DeferredCheck Lean.Doc.DeferredCheck (Array Lean.Doc.DeferredCheck)
-- Mathlib.Topology.Inseparable
SeparationQuotient.tendsto_lift₂_nhds : ∀ {X : Type u_1} {Y : Type u_2} {α : Type u_4} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y → α}
  {hf : ∀ (a : X) (b : Y) (c : X) (d : Y), Inseparable a c → Inseparable b d → f a b = f c d} {x : X} {y : Y}
  {l : Filter α},
  Filter.Tendsto (Function.uncurry (SeparationQuotient.lift₂ f hf))
      (nhds (SeparationQuotient.mk x, SeparationQuotient.mk y)) l ↔
    Filter.Tendsto (Function.uncurry f) (nhds (x, y)) l
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
WeierstrassCurve.Affine.map_linePolynomial : ∀ {R : Type r} {S : Type s} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) (x y ℓ : R),
  WeierstrassCurve.Affine.linePolynomial (f x) (f y) (f ℓ) =
    Polynomial.map f (WeierstrassCurve.Affine.linePolynomial x y ℓ)
-- Mathlib.GroupTheory.GroupAction.Hom
/-- The inverse of a bijective equivariant map is equivariant.  -/
AddActionHom.inverse : {M : Type u_2} →
  {X : Type u_5} →
    [inst : VAdd M X] →
      {Y₁ : Type u_8} →
        [inst_1 : VAdd M Y₁] →
          (f : X →ₑ[id] Y₁) → (g : Y₁ → X) → Function.LeftInverse g ⇑f → Function.RightInverse g ⇑f → Y₁ →ₑ[id] X
-- Mathlib.Algebra.Order.Sub.Defs
lt_add_of_tsub_lt_left : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [OrderedSub α] {a b c : α}
  [AddLeftReflectLE α], a - b < c → a < b + c
-- Mathlib.Analysis.Normed.Module.Basic
NormedAlgebra.toNormedSpace : {𝕜 : Type u_1} →
  (𝕜' : Type u_2) → [inst : NormedField 𝕜] → [inst_1 : SeminormedRing 𝕜'] → [NormedAlgebra 𝕜 𝕜'] → NormedSpace 𝕜 𝕜'
-- Mathlib.SetTheory.Cardinal.Free
Cardinal.mk_freeGroup : ∀ (α : Type u) [Nonempty α], Cardinal.mk (FreeGroup α) = max (Cardinal.mk α) Cardinal.aleph0
-- Lean.Meta.Match.Basic
Lean.Meta.Match.Problem.mk.sizeOf_spec : ∀ (mvarId : Lean.MVarId) (vars : List Lean.Expr) (alts : List Lean.Meta.Match.Alt)
  (examples : List Lean.Meta.Match.Example),
  sizeOf { mvarId := mvarId, vars := vars, alts := alts, examples := examples } =
    1 + sizeOf mvarId + sizeOf vars + sizeOf alts + sizeOf examples
-- Mathlib.Data.Seq.Computation
Computation.head_empty : ∀ {α : Type u}, (Computation.empty α).head = none
-- Init.Data.Array.Lex.Lemmas
Array.lex_eq_false_iff_ge : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] [inst_2 : LT α] [inst_3 : DecidableLT α] {xs ys : Array α},
  (xs.lex ys fun x1 x2 => decide (x1 < x2)) = false ↔ ys ≤ xs
-- Mathlib.Algebra.Group.Subgroup.Pointwise
Subgroup.smul_opposite_image_mul_preimage : ∀ {G : Type u_2} [inst : Group G] {H : Subgroup G} (g : G) (h : ↥H.op) (s : Set G),
  (fun y => h • y) '' (fun x => g * x) ⁻¹' s = (fun x => g * x) ⁻¹' (fun y => h • y) '' s
-- Mathlib.GroupTheory.Congruence.Defs
Con.ext_iff : ∀ {M : Type u_1} [inst : Mul M] {c d : Con M}, c = d ↔ ∀ (x y : M), c x y ↔ d x y
-- Mathlib.Data.ZMod.Basic
ZMod.val_sub : ∀ {n : ℕ} [NeZero n] {a b : ZMod n}, b.val ≤ a.val → (a - b).val = a.val - b.val
-- Mathlib.Topology.DiscreteQuotient
DiscreteQuotient.refl : ∀ {X : Type u_2} [inst : TopologicalSpace X] (S : DiscreteQuotient X) (x : X), S.toSetoid x x
-- Mathlib.CategoryTheory.Monad.Coequalizer
CategoryTheory.Monad.beckCoequalizer_desc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} (X : T.Algebra)
  (s : CategoryTheory.Limits.Cofork (T.map X.a) (T.μ.app X.A)),
  (CategoryTheory.Monad.beckCoequalizer X).desc s = CategoryTheory.CategoryStruct.comp (T.η.app X.A) s.π
-- Mathlib.Algebra.Quandle
/-- Given a map from a rack to a group, lift it to being a map from the enveloping group.
More precisely, the `EnvelGroup` functor is left adjoint to `Quandle.Conj`.
 -/
Rack.toEnvelGroup.map : {R : Type u_1} →
  [inst : Rack R] → {G : Type u_2} → [inst_1 : Group G] → ShelfHom R (Quandle.Conj G) ≃ (Rack.EnvelGroup R →* G)
-- Lean.LibrarySuggestions.Basic
Lean.LibrarySuggestions.Config.mk.inj : ∀ {maxSuggestions : ℕ} {caller : Option String} {filter : Lean.Name → Lean.MetaM Bool} {hint : Option String}
  {maxSuggestions_1 : ℕ} {caller_1 : Option String} {filter_1 : Lean.Name → Lean.MetaM Bool} {hint_1 : Option String},
  { maxSuggestions := maxSuggestions, caller := caller, filter := filter, hint := hint } =
      { maxSuggestions := maxSuggestions_1, caller := caller_1, filter := filter_1, hint := hint_1 } →
    maxSuggestions = maxSuggestions_1 ∧ caller = caller_1 ∧ filter = filter_1 ∧ hint = hint_1
-- Mathlib.Topology.Constructions
/-- The composition of `Quotient.mk'` and a function with dense range has dense range.  -/
DenseRange.quotient : ∀ {X : Type u} {Y : Type v} [inst : Setoid X] [inst_1 : TopologicalSpace X] {f : Y → X},
  DenseRange f → DenseRange (Quotient.mk' ∘ f)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Real.sin_arctan_le_zero : ∀ {x : ℝ}, Real.sin (Real.arctan x) ≤ 0 ↔ x ≤ 0
-- Mathlib.Algebra.Ring.Periodic
Function.Periodic.const_add : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [inst : AddSemigroup α],
  Function.Periodic f c → ∀ (a : α), Function.Periodic (fun x => f (a + x)) c
-- Mathlib.Data.Nat.Bits
/-- `size n` : Returns the size of a natural number in
bits i.e. the length of its binary representation  -/
Nat.size : ℕ → ℕ
-- Mathlib.Data.Finset.Sups
Finset.singleton_infs : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SemilatticeInf α] {t : Finset α} {a : α},
  {a} ⊼ t = Finset.image (fun x => a ⊓ x) t
-- Std.Data.Internal.List.Associative
Std.Internal.List.maxKey!_le_maxKey!_insertEntry : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  [inst_4 : Inhabited α] {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    l.isEmpty = false →
      ∀ {k : α} {v : β k},
        (compare (Std.Internal.List.maxKey! l) (Std.Internal.List.maxKey! (Std.Internal.List.insertEntry k v l))).isLE =
          true
-- Batteries.Recycling.RBTree.Basic
RBTree.RBMap.instStreamStream : {α : Type u} → {β : Type v} → Std.Stream (RBTree.RBMap.Keys.Stream α β) α
-- Mathlib.Data.Set.MemPartition
instFintype_memPartition : {α : Type u_1} → (f : ℕ → Set α) → (n : ℕ) → Fintype ↑(memPartition f n)
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.natAddLEFunctor_map_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {n k l : ℕ} (h : k + l ≤ n)
  {X Y : CategoryTheory.ComposableArrows C n} (f : X ⟶ Y) (X_1 : Fin (l + 1)),
  ((CategoryTheory.ComposableArrows.natAddLEFunctor h).map f).app X_1 = f.app ((Fin.natAddLEFunctor h).obj X_1)
-- Mathlib.Algebra.Homology.QuasiIso
isoOfQuasiIsoAt.congr_simp : ∀ {ι : Type u_1} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K L : HomologicalComplex C c}
  (f f_1 : K ⟶ L) (e_f : f = f_1) (i : ι) [inst_2 : K.HasHomology i] [inst_3 : L.HasHomology i]
  [inst_4 : QuasiIsoAt f i], isoOfQuasiIsoAt f i = isoOfQuasiIsoAt f_1 i
-- Mathlib.Data.Matrix.Composition
Matrix.isUnit_comp_iff : ∀ (I : Type u_1) (J : Type u_2) (R : Type u_5) [inst : Semiring R] [inst_1 : Fintype I] [inst_2 : Fintype J]
  [inst_3 : DecidableEq I] [inst_4 : DecidableEq J] {M : Matrix I I (Matrix J J R)},
  IsUnit ((Matrix.comp I I J J R) M) ↔ IsUnit M
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
/-- If `E / F` is a finite extension such that `E = F(α)`, then for any intermediate field `K`, the
`F` adjoin the coefficients of `minpoly K α` is equal to `K` itself.  -/
IntermediateField.adjoin_minpoly_coeff_of_exists_primitive_element : ∀ (F : Type u_1) [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] {α : E}
  [FiniteDimensional F E],
  F⟮α⟯ = ⊤ →
    ∀ (K : IntermediateField F E),
      IntermediateField.adjoin F ↑(Polynomial.map (algebraMap (↥K) E) (minpoly (↥K) α)).coeffs = K
-- Mathlib.LinearAlgebra.Dimension.Finite
/-- See `rank_zero_iff` for a stronger version with `IsTorsionFree R M`.  -/
rank_eq_zero_iff : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  Module.rank R M = 0 ↔ ∀ (x : M), ∃ a, a ≠ 0 ∧ a • x = 0
-- Mathlib.RingTheory.AlgebraicIndependent.Basic
AlgebraicIndependent.image : ∀ {R : Type u_2} {A : Type v} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] {ι : Type u_3}
  {s : Set ι} {f : ι → A}, (AlgebraicIndependent R fun x => f ↑x) → AlgebraicIndependent R fun x => ↑x
-- Mathlib.Analysis.Normed.Group.Basic
IndiscreteTopology.nnnorm_eq_zero' : ∀ {E : Type u_5} [inst : SeminormedGroup E] [IndiscreteTopology E] (x : E), ‖x‖₊ = 0
-- Mathlib.LinearAlgebra.Span.Defs
/-- An induction principle for span membership. If `p` holds for 0 and all elements of `s`, and is
preserved under addition and scalar multiplication, then `p` holds for all elements of the span of
`s`.  -/
Submodule.span_induction : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {s : Set M}
  {p : (x : M) → x ∈ Submodule.span R s → Prop},
  (∀ (x : M) (h : x ∈ s), p x ⋯) →
    p 0 ⋯ →
      (∀ (x y : M) (hx : x ∈ Submodule.span R s) (hy : y ∈ Submodule.span R s), p x hx → p y hy → p (x + y) ⋯) →
        (∀ (a : R) (x : M) (hx : x ∈ Submodule.span R s), p x hx → p (a • x) ⋯) →
          ∀ {x : M} (hx : x ∈ Submodule.span R s), p x hx
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get!_alter : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k k' : α} [inst : Inhabited β] {f : Option β → Option β},
      Std.DTreeMap.Raw.Const.get! (Std.DTreeMap.Raw.Const.alter t k f) k' =
        if cmp k k' = Ordering.eq then (f (Std.DTreeMap.Raw.Const.get? t k)).get! else Std.DTreeMap.Raw.Const.get! t k'
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.instIsTopologicalAddGroup : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] {m : Type u_2} {n : Type u_3},
  IsTopologicalAddGroup (CStarMatrix m n A)
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.Pattern.Model.Pos.isLongestRevMatchAtChain_revSkipWhile : ∀ {ρ : Type} (pat : ρ) [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.BackwardPattern pat] [String.Slice.Pattern.Model.LawfulBackwardPatternModel pat]
  {s : String.Slice} (pos : s.Pos), String.Slice.Pattern.Model.IsLongestRevMatchAtChain pat (pos.revSkipWhile pat) pos
-- Mathlib.CategoryTheory.WithTerminal.Cone
_private.Mathlib.CategoryTheory.WithTerminal.Cone.0.CategoryTheory.WithInitial.id.match_1.splitter : {C : Type u_1} →
  (motive : CategoryTheory.WithInitial C → Sort u_2) →
    (x : CategoryTheory.WithInitial C) →
      ((a : C) → motive (CategoryTheory.WithInitial.of a)) → (Unit → motive CategoryTheory.WithInitial.star) → motive x
-- Mathlib.GroupTheory.Coprod.Basic
/-- The natural projection `FreeAddMonoid (M ⊕ N) →+ AddMonoid.Coprod M N`.  -/
AddMonoid.Coprod.mk : {M : Type u_1} →
  {N : Type u_2} → [inst : AddZeroClass M] → [inst_1 : AddZeroClass N] → FreeAddMonoid (M ⊕ N) →+ AddMonoid.Coprod M N
-- Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
/-- Radon-Nikodym derivative of the scalar multiple of a measure.
See also `rnDeriv_smul_left_of_ne_top`, which has no hypothesis on `μ` but requires finite `ν`.  -/
MeasureTheory.Measure.rnDeriv_smul_left_of_ne_top' : ∀ {α : Type u_1} {m : MeasurableSpace α} (ν μ : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite ν]
  [MeasureTheory.SigmaFinite μ] {r : ENNReal}, r ≠ ⊤ → (r • ν).rnDeriv μ =ᵐ[μ] r • ν.rnDeriv μ
-- Mathlib.Analysis.SpecialFunctions.JapaneseBracket
le_rpow_one_add_norm_iff_norm_le : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {r t : ℝ},
  0 < r → 0 < t → ∀ (x : E), t ≤ (1 + ‖x‖) ^ (-r) ↔ ‖x‖ ≤ t ^ (-r⁻¹) - 1
-- Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
curveIntegral_segment : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] [inst_5 : NormedSpace ℝ E]
  [inst_6 : NormedSpace ℝ F] (ω : E → E →L[𝕜] F) (a b : E),
  ∫ᶜ (x : E) in Path.segment a b, ω x = ∫ (t : ℝ) in 0..1, (ω ((AffineMap.lineMap a b) t)) (b - a)
-- Mathlib.Dynamics.Ergodic.Ergodic
/-- On a probability space, the (pre)ergodicity condition is a zero-one law.  -/
PreErgodic.prob_eq_zero_or_one : ∀ {α : Type u_1} {m : MeasurableSpace α} {s : Set α} {f : α → α} {μ : MeasureTheory.Measure α}
  [MeasureTheory.IsProbabilityMeasure μ], PreErgodic f μ → MeasurableSet s → f ⁻¹' s = s → μ s = 0 ∨ μ s = 1
-- Mathlib.LinearAlgebra.BilinearForm.DualLattice
LinearMap.BilinForm.dualSubmoduleToDual_injective : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : Field S] [inst_2 : AddCommGroup M]
  [inst_3 : Algebra R S] [inst_4 : Module R M] [inst_5 : Module S M] [inst_6 : IsScalarTower R S M]
  (B : LinearMap.BilinForm S M) [inst_7 : IsDomain R],
  B.Nondegenerate →
    ∀ [inst_8 : Module.IsTorsionFree R S] (N : Submodule R M),
      Submodule.span S ↑N = ⊤ → Function.Injective ⇑(B.dualSubmoduleToDual N)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
/-- A walk is a sequence of adjacent vertices.  For vertices `u v : V`,
the type `walk u v` consists of all walks starting at `u` and ending at `v`.

We say that a walk *visits* the vertices it contains.  The set of vertices a
walk visits is `SimpleGraph.Walk.support`.

See `SimpleGraph.Walk.nil'` and `SimpleGraph.Walk.cons'` for patterns that
can be useful in definitions since they make the vertices explicit.  -/
SimpleGraph.Walk : {V : Type u} → SimpleGraph V → V → V → Type u
-- Mathlib.Algebra.Order.Nonneg.Basic
Nonneg.pow : {α : Type u_1} →
  [inst : MonoidWithZero α] → [inst_1 : Preorder α] → [ZeroLEOneClass α] → [PosMulMono α] → Pow { x // 0 ≤ x } ℕ
-- Mathlib.Data.Int.LeastGreatest
/-- `Int.greatestOfBdd` is the greatest integer satisfying a predicate which is false for all
`z : ℤ` with `b < z` for some fixed `b : ℤ`.  -/
Int.isGreatest_coe_greatestOfBdd : ∀ {P : ℤ → Prop} [inst : DecidablePred P] (b : ℤ) (Hb : ∀ (z : ℤ), P z → z ≤ b) (Hinh : ∃ z, P z),
  IsGreatest {z | P z} ↑(b.greatestOfBdd Hb Hinh)
-- Mathlib.Data.Fintype.Card
Bool.instWellFoundedLT : WellFoundedLT Bool
-- Mathlib.Probability.Martingale.Basic
/-- A predictable submartingale is a.e. greater than or equal to its initial state.  -/
MeasureTheory.Submartingale.zero_le_of_predictable : ∀ {Ω : Type u_1} {E : Type u_2} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] {𝒢 : MeasureTheory.Filtration ℕ m0} [inst_2 : Preorder E]
  [MeasureTheory.SigmaFiniteFiltration μ 𝒢] {f : ℕ → Ω → E},
  MeasureTheory.Submartingale f 𝒢 μ → (MeasureTheory.StronglyAdapted 𝒢 fun n => f (n + 1)) → ∀ (n : ℕ), f 0 ≤ᵐ[μ] f n
-- Lean.Data.Lsp.Extra
Lean.Lsp.ModuleHierarchyOptions.mk.sizeOf_spec : sizeOf { } = 1
-- Mathlib.Order.Basic
/-- Pull back a `LinearOrder` instance along an injective function.

See note [reducible non-instances].  -/
Function.Injective.linearOrder : {α : Type u_2} →
  {β : Type u_3} →
    [inst : LinearOrder β] →
      [inst_1 : LE α] →
        [inst_2 : LT α] →
          [inst_3 : Max α] →
            [inst_4 : Min α] →
              [inst_5 : Ord α] →
                [DecidableEq α] →
                  [DecidableLE α] →
                    [DecidableLT α] →
                      (f : α → β) →
                        Function.Injective f →
                          (∀ {x y : α}, f x ≤ f y ↔ x ≤ y) →
                            (∀ {x y : α}, f x < f y ↔ x < y) →
                              (∀ (x y : α), f (x ⊓ y) = min (f x) (f y)) →
                                (∀ (x y : α), f (x ⊔ y) = max (f x) (f y)) →
                                  (∀ (x y : α), compare (f x) (f y) = compare x y) → LinearOrder α
-- Mathlib.Algebra.BigOperators.Fin
Fin.prod_Ioc_castLE : ∀ {M : Type u_2} [inst : CommMonoid M] {n m : ℕ} (h : n ≤ m) (f : Fin m → M) (a b : Fin n),
  ∏ i ∈ Finset.Ioc (Fin.castLE h a) (Fin.castLE h b), f i = ∏ i ∈ Finset.Ioc a b, f (Fin.castLE h i)
-- Mathlib.Topology.Order.HullKernel
/-- Every relative-open set of the form `T ↓∩ (↑(upperClosure F))ᶜ` for `F` finite
is a relative-open set of the form `(hull T a)ᶜ` where `a = ⨅ F`.  -/
PrimitiveSpectrum.preimage_upperClosure_compl_finset : ∀ {α : Type u_1} [inst : SemilatticeInf α] {T : Set α} [inst_1 : OrderTop α],
  (∀ p ∈ T, InfPrime p) →
    ∀ (F : Finset α), Subtype.val ⁻¹' (↑(upperClosure ↑F))ᶜ = (PrimitiveSpectrum.hull T (F.inf id))ᶜ
-- Mathlib.Analysis.InnerProductSpace.Symmetric
/-- If a symmetric operator preserves a submodule, its restriction to that submodule is
symmetric.  -/
LinearMap.IsSymmetric.restrict_invariant : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {T : E →ₗ[𝕜] E}, T.IsSymmetric → ∀ {V : Submodule 𝕜 E} (hV : ∀ v ∈ V, T v ∈ V), (T.restrict hV).IsSymmetric
-- Mathlib.Tactic.Simps.Basic
_private.Mathlib.Tactic.Simps.Basic.0.NameStruct.mk : Lean.Name → List String → NameStruct✝
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.pow_right_monotone : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Monoid α] {s : Finset α}, 1 ∈ s → Monotone fun x => s ^ x
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.SummableFamily.sub_apply : ∀ {Γ : Type u_1} {R : Type u_3} {α : Type u_5} [inst : PartialOrder Γ] [inst_1 : AddCommGroup R]
  {s t : HahnSeries.SummableFamily Γ R α} {a : α}, (s - t) a = s a - t a
-- Mathlib.Algebra.Group.Subsemigroup.Operations
MulHom.srange_eq_top_iff_surjective : ∀ {M : Type u_1} [inst : Mul M] {N : Type u_5} [inst_1 : Mul N] {f : M →ₙ* N}, f.srange = ⊤ ↔ Function.Surjective ⇑f
-- Mathlib.CategoryTheory.Abelian.Basic
/-- The canonical map `pullback f g ⟶ X ⊞ Y` induces a kernel cone on the map
`biproduct X Y ⟶ Z` induced by `f` and `g`. A slightly more intuitive way to think of
this may be that it induces an equalizer fork on the maps induced by `(f, 0)` and
`(0, g)`.  -/
CategoryTheory.Abelian.PullbackToBiproductIsKernel.pullbackToBiproductFork : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      [CategoryTheory.Limits.HasPullbacks C] →
        {X Y Z : C} →
          (f : X ⟶ Z) → (g : Y ⟶ Z) → CategoryTheory.Limits.KernelFork (CategoryTheory.Limits.biprod.desc f (-g))
-- Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
Subgroup.op_bot : ∀ {G : Type u_2} [inst : Group G], ⊥.op = ⊥
-- Init.Data.Array.Attach
Array.pmap_eq_attachWith : ∀ {α : Type u_1} {p q : α → Prop} {f : ∀ (a : α), p a → q a} {xs : Array α} (H : ∀ a ∈ xs, p a),
  Array.pmap (fun a h => ⟨a, ⋯⟩) xs H = xs.attachWith q ⋯
-- Lean.Elab.Do.Basic
/-- Elaboration of a `do` block `do $e; $rest`, results in a call
``elabTerm `(do $e; $rest) = elabDoElem e dec``, where `elabDoElem e ·` is the elaborator for `do`
element `e`, and `dec` is the `DoElemCont` describing the elaboration of the rest of the block
`rest`.

If the semantics of `e` resumes its continuation `rest`, its elaborator must bind its result to
`resultName`, ensure that it has type `resultType` and then elaborate `rest` using `dec`.

Clearly, for term elements `e : m α`, the result has type `α`.
More subtly, for binding elements `let x := e` or `let x ← e`, the result has type `PUnit` and is
unrelated to the type of the bound variable `x`.

Examples:
* `return` drops the continuation; `return x; pure ()` elaborates to `pure x`.
* `let x ← e; rest x` elaborates to `e >>= fun x => rest x`.
* `let x := 3; let y ← (let x ← e); rest x` elaborates to
  `let x := 3; e >>= fun x_1 => let y := (); rest x`, which is immediately zeta-reduced to
  `let x := 3; e >>= fun x_1 => rest x`.
* `one; two` elaborates to `one >>= fun (_ : PUnit) => two`; it is an error if `one` does not have
  type `PUnit`.
 -/
Lean.Elab.Do.DoElemCont : Type
-- Mathlib.GroupTheory.Focal
/-- The focal subgroup considered as a subgroup of `H`.
Note that `focalSubgroup H` is always contained in `H`.
 -/
Subgroup.focalSubgroupOf : {G : Type u_1} → [inst : Group G] → (H : Subgroup G) → Subgroup ↥H
-- Std.Data.String.ToNat
_private.Std.Data.String.ToNat.0.noRepetition_append_cons_of_noRepetition_append_singleton : ∀ {α : Type u} {a : α} {l m : List α},
  NoRepetition✝ a (l ++ [a]) → NoRepetition✝ a (a :: m) → NoRepetition✝ a (l ++ a :: m)
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
ModuleCat.instIsRightAdjointCoextendScalars : ∀ {R : Type u₁} {S : Type u₂} [inst : Ring R] [inst_1 : Ring S] (f : R →+* S),
  (ModuleCat.coextendScalars f).IsRightAdjoint
-- Init.Omega.Constraint
_private.Init.Omega.Constraint.0.Lean.Omega.Constraint.isImpossible.match_1.eq_2 : ∀ (motive : Lean.Omega.Constraint → Sort u_1) (x : Lean.Omega.Constraint)
  (h_1 : (x y : ℤ) → motive { lowerBound := some x, upperBound := some y })
  (h_2 : (x : Lean.Omega.Constraint) → motive x),
  (∀ (x_1 y : ℤ), x = { lowerBound := some x_1, upperBound := some y } → False) →
    (match x with
      | { lowerBound := some x, upperBound := some y } => h_1 x y
      | x => h_2 x) =
      h_2 x
-- Lean.Data.Lsp.TextSync
Lean.Lsp.instFromJsonTextDocumentSyncKind : Lean.FromJson Lean.Lsp.TextDocumentSyncKind
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField
AlgebraicGeometry.LocallyRingedSpace.residue_comp_residueFieldMap_eq_stalkMap_comp_residue_assoc : ∀ {X Y : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Y) (x : ↑X.toTopCat) {Z : CommRingCat}
  (h : X.residueField x ⟶ Z),
  CategoryTheory.CategoryStruct.comp (Y.residue ((CategoryTheory.ConcreteCategory.hom f.base) x))
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.LocallyRingedSpace.residueFieldMap f x) h) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap f x)
      (CategoryTheory.CategoryStruct.comp (X.residue x) h)
-- Mathlib.Order.Interval.Set.Pi
Set.image_mulSingle_Icc : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : DecidableEq ι] [inst_1 : (i : ι) → PartialOrder (α i)]
  [inst_2 : (i : ι) → One (α i)] (i : ι) (a b : α i),
  Pi.mulSingle i '' Set.Icc a b = Set.Icc (Pi.mulSingle i a) (Pi.mulSingle i b)
-- Mathlib.Analysis.Calculus.Deriv.Inv
hasFDerivWithinAt_inv : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {s : Set 𝕜},
  x ≠ 0 → HasFDerivWithinAt (fun x => x⁻¹) (ContinuousLinearMap.toSpanSingleton 𝕜 (-(x ^ 2)⁻¹)) s x
-- Mathlib.Topology.Connected.LocallyPathConnected
/-- The product of two locally path-connected spaces is locally path-connected.  -/
Prod.locallyPathConnectedSpace : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [LocallyPathConnectedSpace X]
  [LocallyPathConnectedSpace Y], LocallyPathConnectedSpace (X × Y)
-- Batteries.Data.BitVec.Lemmas
BitVec.getLsbD_ofFnLE : ∀ {n : ℕ} (f : Fin n → Bool) (i : ℕ), (BitVec.ofFnLE f).getLsbD i = if h : i < n then f ⟨i, h⟩ else false
-- Mathlib.AlgebraicGeometry.Morphisms.Flat
CategoryTheory.Under.liftCone.eq_1 : ∀ {J : Type w} [inst : CategoryTheory.Category.{w', w} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F) {X : C} (f : X ⟶ c.pt),
  CategoryTheory.Under.liftCone c f =
    { pt := CategoryTheory.Under.mk f,
      π := { app := fun j => CategoryTheory.Under.homMk (c.π.app j) ⋯, naturality := ⋯ } }
-- Lean.Parser.Extra
Lean.Parser.withAntiquotSpliceAndSuffix.parenthesizer : Lean.SyntaxNodeKind →
  Lean.PrettyPrinter.Parenthesizer → Lean.PrettyPrinter.Parenthesizer → Lean.PrettyPrinter.Parenthesizer
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.foldl_eq_foldl_keys : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} {δ : Type w} [inst : Std.TransCmp cmp]
  {f : δ → α → δ} {init : δ}, Std.ExtTreeMap.foldl (fun d a x => f d a) init t = List.foldl f init t.keys
-- Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
SimpleGraph.Walk.support_dropUntil_subset_support : ∀ {V : Type u} {G : SimpleGraph V} {v w u : V} [inst : DecidableEq V] (p : G.Walk v w) (h : u ∈ p.support),
  (p.dropUntil u h).support ⊆ p.support