mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
/-- Given `F : WalkingParallelFamily ⥤ C`, which is really the same as
`parallelFamily (F.map left) (F.map right)` and a cocone on `F`, we get a cotrident on
`fun j ↦ F.map (line j)`.  -/
CategoryTheory.Limits.Cotrident.ofCocone : {J : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {F : CategoryTheory.Functor (CategoryTheory.Limits.WalkingParallelFamily J) C} →
        CategoryTheory.Limits.Cocone F →
          CategoryTheory.Limits.Cotrident fun j => F.map (CategoryTheory.Limits.WalkingParallelFamily.Hom.line j)
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.counitIsoAux_inv : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (F : CategoryTheory.AddMon C),
  (CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.counitIsoAux C F).inv = CategoryTheory.CategoryStruct.id F.X
-- Init.Data.Function
Function.RightInverse.id : ∀ {α : Sort u_1} {β : Sort u_2} {g : β → α} {f : α → β}, Function.RightInverse g f → f ∘ g = id
-- Lean.Elab.Attributes
Lean.Elab.Attribute.mk : Lean.AttributeKind → Lean.Name → Lean.Syntax → Lean.Elab.Attribute
-- Lean.Language.Basic
Lean.Language.instInhabitedDynamicSnapshot : Inhabited Lean.Language.DynamicSnapshot
-- Mathlib.Algebra.Group.Commute.Basic
AddCommute.sub_add_sub_comm : ∀ {G : Type u_1} [inst : SubtractionMonoid G] {a b c d : G},
  AddCommute b d → AddCommute (-b) c → a - b + (c - d) = a + c - (b + d)
-- Init.Data.String.Lemmas.Order
String.Slice.Pos.ofSliceFrom_lt_iff : ∀ {s : String.Slice} {p₀ : s.Pos} {p : (s.sliceFrom p₀).Pos} {q : s.Pos},
  String.Slice.Pos.ofSliceFrom p < q ↔ ∃ (h : p₀ ≤ q), p < p₀.sliceFrom q h
-- Mathlib.Order.SupIndep
sSupIndep_singleton : ∀ {α : Type u_1} [inst : CompleteLattice α] (a : α), sSupIndep {a}
-- Aesop.Tree.RunMetaM
Aesop.Rapp.runMetaM : {m : Type → Type u_1} →
  [Monad m] →
    [MonadLiftT Lean.MetaM m] → [MonadFinally m] → {α : Type} → m α → Aesop.Rapp → m (α × Lean.Meta.SavedState)
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.gamma_lt_gamma : ∀ {a b : Ordinal.{u}}, a.gamma < b.gamma ↔ a < b
-- Mathlib.CategoryTheory.MorphismProperty.FunctorCategory
CategoryTheory.MorphismProperty.instIsStableUnderTransfiniteCompositionOfShapeFunctorMonomorphismsOfHasPullbacksOfHasIterationOfShape : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : Type u'') [inst_1 : CategoryTheory.Category.{v'', u''} J]
  (K : Type u') [inst_2 : LinearOrder K] [inst_3 : SuccOrder K] [inst_4 : OrderBot K] [inst_5 : WellFoundedLT K]
  [(CategoryTheory.MorphismProperty.monomorphisms C).IsStableUnderTransfiniteCompositionOfShape K]
  [CategoryTheory.Limits.HasPullbacks C] [CategoryTheory.Limits.HasIterationOfShape K C],
  (CategoryTheory.MorphismProperty.monomorphisms
        (CategoryTheory.Functor J C)).IsStableUnderTransfiniteCompositionOfShape
    K
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.smul.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β], Set.smul = { smul := Set.image2 fun x1 x2 => x1 • x2 }
-- Lean.Parser.Command
/-- Registers an error explanation.

Note that the error name is not relativized to the current namespace.
 -/
Lean.Parser.Command.registerErrorExplanationStx : Lean.Parser.Parser
-- Mathlib.Data.Finset.BooleanAlgebra
Finset.univ_nonempty_iff : ∀ {α : Type u_1} [inst : Fintype α], Finset.univ.Nonempty ↔ Nonempty α
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.minKeyD_erase_eq_of_not_compare_minKeyD_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k fallback : α},
  (t.erase k).isEmpty = false →
    ¬cmp k (t.minKeyD fallback) = Ordering.eq → (t.erase k).minKeyD fallback = t.minKeyD fallback
-- Mathlib.Topology.Algebra.Module.ModuleTopology
/-- Addition `+ : A × A → A` is continuous if `R` is a topological
ring, and `A` is an `R` module with the module topology.  -/
ModuleTopology.continuousAdd : ∀ (R : Type u_1) [inst : TopologicalSpace R] (A : Type u_2) [inst_1 : Add A] [inst_2 : SMul R A], ContinuousAdd A
-- Std.Time.Date.Unit.Week
Std.Time.Week.instDecidableEqOrdinal : DecidableEq Std.Time.Week.Ordinal
-- Mathlib.Analysis.InnerProductSpace.LinearPMap
/-- The unique continuous extension of the operator `adjointDomainMkCLM` to `E`.  -/
LinearPMap.adjointDomainMkCLMExtend : {𝕜 : Type u_1} →
  {E : Type u_2} →
    {F : Type u_3} →
      [inst : RCLike 𝕜] →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : InnerProductSpace 𝕜 E] →
            [inst_3 : NormedAddCommGroup F] →
              [inst_4 : InnerProductSpace 𝕜 F] → (T : E →ₗ.[𝕜] F) → ↥T.adjointDomain → StrongDual 𝕜 E
-- Init.Core
instSubsingletonPEmpty : Subsingleton PEmpty.{u_1}
-- Init.Grind.Ring.CommSolver
_private.Init.Grind.Ring.CommSolver.0.Lean.Grind.CommRing.Poly.insert.go.match_1.eq_2 : ∀ (motive : Ordering → Sort u_1) (h_1 : Unit → motive Ordering.eq) (h_2 : Unit → motive Ordering.gt)
  (h_3 : Unit → motive Ordering.lt),
  (match Ordering.gt with
    | Ordering.eq => h_1 ()
    | Ordering.gt => h_2 ()
    | Ordering.lt => h_3 ()) =
    h_2 ()
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.toSubring : {K : Type u} → [inst : Field K] → ValuationSubring K → Subring K
-- Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen
/-- A generalizing morphism, locally of finite presentation is open.  -/
AlgebraicGeometry.isOpenMap_of_generalizingMap : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.LocallyOfFinitePresentation f],
  GeneralizingMap ⇑f → IsOpenMap ⇑f
-- Mathlib.Topology.Separation.Regular
T3Space.toT0Space : ∀ {X : Type u} {inst : TopologicalSpace X} [self : T3Space X], T0Space X
-- Mathlib.Data.Real.ConjExponents
Real.HolderTriple.inv_eq : ∀ {p q r : ℝ}, p.HolderTriple q r → r⁻¹ = p⁻¹ + q⁻¹
-- Mathlib.Topology.Category.Profinite.Nobeling.Successor
/-- The intersection of `C0` and the projection of `C1`. We will apply the inductive hypothesis to
this set.
 -/
Profinite.NobelingProof.C' : {I : Type u} →
  Set (I → Bool) →
    [inst : LinearOrder I] →
      [inst_1 : WellFoundedLT I] → {o : Ordinal.{u}} → (o < Ordinal.type fun x1 x2 => x1 < x2) → Set (I → Bool)
-- Mathlib.Algebra.Group.Subsemigroup.Defs
Subsemigroup.copy.eq_1 : ∀ {M : Type u_1} [inst : Mul M] (S : Subsemigroup M) (s : Set M) (hs : s = ↑S),
  S.copy s hs = { carrier := s, mul_mem' := ⋯ }
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
SimpleGraph.Walk.toSubgraph_map : ∀ {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} {u v : V} (f : G →g G') (p : G.Walk u v),
  (SimpleGraph.Walk.map f p).toSubgraph = SimpleGraph.Subgraph.map f p.toSubgraph
-- Mathlib.RingTheory.DedekindDomain.Basic
Ring.DimensionLEOne.instKrullDimLEOfNatNat : ∀ {R : Type u_4} [inst : CommRing R] [Ring.DimensionLEOne R], Ring.KrullDimLE 1 R
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.filterMap!_equiv_map : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} {γ : α → Type w}
  {f : (a : α) → β a → γ a},
  t.WF → (Std.DTreeMap.Internal.Impl.filterMap! (fun k v => some (f k v)) t).Equiv (Std.DTreeMap.Internal.Impl.map f t)
-- Lean.Meta.Tactic.Grind.Arith.CommRing.RingM
/-- Returns `true` if the current ring has a `IsCharP` instance.  -/
Lean.Meta.Grind.Arith.CommRing.hasChar : Lean.Meta.Grind.Arith.CommRing.RingM Bool
-- Mathlib.Algebra.Polynomial.Laurent
/-- **Alias** of `LaurentPolynomial.support_coeff_C_mul_T_of_ne_zero`. -/
LaurentPolynomial.support_C_mul_T_of_ne_zero : ∀ {R : Type u_1} [inst : Semiring R] {a : R},
  a ≠ 0 → ∀ (n : ℤ), (LaurentPolynomial.C a * LaurentPolynomial.T n).coeff.support = {n}
-- Mathlib.Algebra.Order.Group.Abs
abs_add' : ∀ {G : Type u_1} [inst : AddCommGroup G] [inst_1 : LinearOrder G] [IsOrderedAddMonoid G] (a b : G), |a| ≤ |b| + |b + a|
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.add_pf_add_overlap : ∀ {R : Type u_1} [inst : CommSemiring R] {a₁ a₂ b₁ b₂ c₁ c₂ : R},
  a₁ + b₁ = c₁ → a₂ + b₂ = c₂ → a₁ + a₂ + (b₁ + b₂) = c₁ + c₂
-- Mathlib.RepresentationTheory.Rep.Basic
/-- The natural linear equivalence between functions `α → A` and representation morphisms
`(α →₀ k[G]) ⟶ A`.  -/
Rep.freeLiftLEquiv : (k : Type u) →
  (G : Type v) →
    [inst : CommRing k] →
      [inst_1 : Monoid G] → (α : Type u') → (A : Rep.{max (max u u') v, u, v} k G) → (Rep.free k G α ⟶ A) ≃ₗ[k] α → ↑A
-- Mathlib.Topology.ContinuousMap.StoneWeierstrass
/-- An alternative statement of the Stone-Weierstrass theorem,
for those who like their epsilons and don't like bundled continuous functions.

If `A` is a subalgebra of `C(X, ℝ)` which separates points (and `X` is compact),
every real-valued continuous function on `X` is within any `ε > 0` of some element of `A`.
 -/
ContinuousMap.exists_mem_subalgebra_near_continuous_of_separatesPoints : ∀ {X : Type u_1} [inst : TopologicalSpace X] [CompactSpace X] (A : Subalgebra ℝ C(X, ℝ)),
  A.SeparatesPoints → ∀ (f : X → ℝ), Continuous f → ∀ (ε : ℝ), 0 < ε → ∃ g, ∀ (x : X), ‖↑g x - f x‖ < ε
-- Mathlib.Topology.UniformSpace.Equiv
UniformEquiv.symm_apply_apply : ∀ {α : Type u} {β : Type u_1} [inst : UniformSpace α] [inst_1 : UniformSpace β] (h : α ≃ᵤ β) (x : α), h.symm (h x) = x
-- Mathlib.CategoryTheory.Products.Basic
/-- Any morphism in a product factors as a morphism whose left component is an identity
followed by a morphism whose right component is an identity.  -/
CategoryTheory.Prod.fac : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {x y : C × D} (f : x ⟶ y),
  f =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id x.1) f.2)
      (CategoryTheory.Prod.mkHom f.1 (CategoryTheory.CategoryStruct.id y.2))
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.size_insertIfNew : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {v : β k}, (m.insertIfNew k v).size = if k ∈ m then m.size else m.size + 1
-- Mathlib.Topology.DenseEmbedding
IsDenseEmbedding.subtypeEmb_coe : ∀ {β : Type u_2} [inst : TopologicalSpace β] {α : Type u_5} (p : α → Prop) (e : α → β) (x : { x // p x }),
  ↑(IsDenseEmbedding.subtypeEmb p e x) = e ↑x
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.maxEntryD.match_1.eq_3 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : Std.DTreeMap.Internal.Impl α β → (a : α) × β a → Sort u_3) (size : ℕ)
  (k : α) (v : β k) (l : Std.DTreeMap.Internal.Impl α β) (size_1 : ℕ) (k_1 : α) (v_1 : β k_1)
  (l_1 r : Std.DTreeMap.Internal.Impl α β) (fallback : (a : α) × β a)
  (h_1 : (fallback : (a : α) × β a) → motive Std.DTreeMap.Internal.Impl.leaf fallback)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l : Std.DTreeMap.Internal.Impl α β) →
            (x : (a : α) × β a) →
              motive (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf) x)
  (h_3 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l r : Std.DTreeMap.Internal.Impl α β) →
            (size_2 : ℕ) →
              (k_2 : α) →
                (v_2 : β k_2) →
                  (l_2 r_1 : Std.DTreeMap.Internal.Impl α β) →
                    r = Std.DTreeMap.Internal.Impl.inner size_2 k_2 v_2 l_2 r_1 →
                      (fallback : (a : α) × β a) →
                        motive
                          (Std.DTreeMap.Internal.Impl.inner size k v l
                            (Std.DTreeMap.Internal.Impl.inner size_2 k_2 v_2 l_2 r_1))
                          fallback),
  (match Std.DTreeMap.Internal.Impl.inner size k v l (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r),
      fallback with
    | Std.DTreeMap.Internal.Impl.leaf, fallback => h_1 fallback
    | Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf, x => h_2 size k v l x
    | Std.DTreeMap.Internal.Impl.inner size k v l r@h:(Std.DTreeMap.Internal.Impl.inner size_2 k_2 v_2 l_2 r_1),
      fallback => h_3 size k v l r size_2 k_2 v_2 l_2 r_1 h fallback) =
    h_3 size k v l (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r) size_1 k_1 v_1 l_1 r ⋯ fallback
-- Mathlib.Computability.TuringMachine.ToPartrec
_private.Mathlib.Computability.TuringMachine.ToPartrec.0.Turing.PartrecToTM2.tr.match_1.eq_10 : ∀ (motive : Turing.PartrecToTM2.Λ' → Sort u_1) (f : Turing.ToPartrec.Code) (k : Turing.PartrecToTM2.Cont')
  (h_1 :
    (p : Turing.PartrecToTM2.Γ' → Bool) →
      (k₁ k₂ : Turing.PartrecToTM2.K') → (q : Turing.PartrecToTM2.Λ') → motive (Turing.PartrecToTM2.Λ'.move p k₁ k₂ q))
  (h_2 :
    (k : Turing.PartrecToTM2.K') →
      (f : Option Turing.PartrecToTM2.Γ' → Option Turing.PartrecToTM2.Γ') →
        (q : Turing.PartrecToTM2.Λ') → motive (Turing.PartrecToTM2.Λ'.push k f q))
  (h_3 : (q : Option Turing.PartrecToTM2.Γ' → Turing.PartrecToTM2.Λ') → motive (Turing.PartrecToTM2.Λ'.read q))
  (h_4 :
    (p : Turing.PartrecToTM2.Γ' → Bool) →
      (k : Turing.PartrecToTM2.K') → (q : Turing.PartrecToTM2.Λ') → motive (Turing.PartrecToTM2.Λ'.clear p k q))
  (h_5 : (q : Turing.PartrecToTM2.Λ') → motive q.copy) (h_6 : (q : Turing.PartrecToTM2.Λ') → motive q.succ)
  (h_7 : (q₁ q₂ : Turing.PartrecToTM2.Λ') → motive (q₁.pred q₂))
  (h_8 :
    (fs : Turing.ToPartrec.Code) →
      (k : Turing.PartrecToTM2.Cont') → motive (Turing.PartrecToTM2.Λ'.ret (Turing.PartrecToTM2.Cont'.cons₁ fs k)))
  (h_9 : (k : Turing.PartrecToTM2.Cont') → motive (Turing.PartrecToTM2.Λ'.ret k.cons₂))
  (h_10 :
    (f : Turing.ToPartrec.Code) →
      (k : Turing.PartrecToTM2.Cont') → motive (Turing.PartrecToTM2.Λ'.ret (Turing.PartrecToTM2.Cont'.comp f k)))
  (h_11 :
    (f : Turing.ToPartrec.Code) →
      (k : Turing.PartrecToTM2.Cont') → motive (Turing.PartrecToTM2.Λ'.ret (Turing.PartrecToTM2.Cont'.fix f k)))
  (h_12 : Unit → motive (Turing.PartrecToTM2.Λ'.ret Turing.PartrecToTM2.Cont'.halt)),
  (match Turing.PartrecToTM2.Λ'.ret (Turing.PartrecToTM2.Cont'.comp f k) with
    | Turing.PartrecToTM2.Λ'.move p k₁ k₂ q => h_1 p k₁ k₂ q
    | Turing.PartrecToTM2.Λ'.push k f q => h_2 k f q
    | Turing.PartrecToTM2.Λ'.read q => h_3 q
    | Turing.PartrecToTM2.Λ'.clear p k q => h_4 p k q
    | q.copy => h_5 q
    | q.succ => h_6 q
    | q₁.pred q₂ => h_7 q₁ q₂
    | Turing.PartrecToTM2.Λ'.ret (Turing.PartrecToTM2.Cont'.cons₁ fs k) => h_8 fs k
    | Turing.PartrecToTM2.Λ'.ret k.cons₂ => h_9 k
    | Turing.PartrecToTM2.Λ'.ret (Turing.PartrecToTM2.Cont'.comp f k) => h_10 f k
    | Turing.PartrecToTM2.Λ'.ret (Turing.PartrecToTM2.Cont'.fix f k) => h_11 f k
    | Turing.PartrecToTM2.Λ'.ret Turing.PartrecToTM2.Cont'.halt => h_12 ()) =
    h_10 f k
-- Mathlib.Topology.Algebra.Group.Pointwise
IsCompact.locallyCompactSpace_of_mem_nhds_of_addGroup : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [IsTopologicalAddGroup G] {K : Set G},
  IsCompact K → ∀ {x : G}, K ∈ nhds x → LocallyCompactSpace G
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKeyD_filterMap : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp}
  [inst : Std.TransCmp cmp] {f : α → β → Option γ} {k fallback : α} (h : t.WF),
  (Std.TreeMap.Raw.filterMap f t).getKeyD k fallback =
    ((t.getKey? k).pfilter fun x h' => (f x t[x]).isSome).getD fallback
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
CategoryTheory.Triangulated.TStructure.to_truncLE_obj_ext : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) {n : ℤ} {Y X : C} {f₁ f₂ : Y ⟶ (t.truncLE n).obj X},
  CategoryTheory.CategoryStruct.comp f₁ ((t.truncLEι n).app X) =
      CategoryTheory.CategoryStruct.comp f₂ ((t.truncLEι n).app X) →
    ∀ [t.IsLE Y n], f₁ = f₂
-- Mathlib.RingTheory.Localization.Basic
/-- If `R` is a field, then localizing at a submonoid not containing `0` adds no new elements.  -/
Field.localization_map_bijective : ∀ {K : Type u_4} {Kₘ : Type u_5} [inst : Field K] [inst_1 : CommRing Kₘ] {M : Submonoid K},
  0 ∉ M → ∀ [inst_2 : Algebra K Kₘ] [IsLocalization M Kₘ], Function.Bijective ⇑(algebraMap K Kₘ)
-- Init.Data.Slice.Array.Lemmas
Array.toList_mkSlice_rco : ∀ {α : Type u_1} {xs : Array α} {lo hi : ℕ},
  Std.Slice.toList (Std.Rco.Sliceable.mkSlice xs lo...hi) = List.drop lo (List.take hi xs.toList)
-- Mathlib.MeasureTheory.Measure.Regular
MeasureTheory.Measure.Regular.toOuterRegular : ∀ {α : Type u_1} {inst : MeasurableSpace α} {inst_1 : TopologicalSpace α} {μ : MeasureTheory.Measure α}
  [self : μ.Regular], μ.OuterRegular
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.minKey?_insertIfNew_of_isEmpty : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β}, t.isEmpty = true → (t.insertIfNew k v).minKey? = some k
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.instIsCentralScalarSubtypeMem : ∀ (R : Type u) (L : Type v) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {R₁ : Type u_1}
  [inst_3 : Semiring R₁] [inst_4 : SMul R₁ R] [inst_5 : SMul R₁ᵐᵒᵖ R] [inst_6 : Module R₁ L] [inst_7 : Module R₁ᵐᵒᵖ L]
  [inst_8 : IsScalarTower R₁ R L] [inst_9 : IsScalarTower R₁ᵐᵒᵖ R L] [IsCentralScalar R₁ L] (L' : LieSubalgebra R L),
  IsCentralScalar R₁ ↥L'
-- Std.Http.Protocol.H1.Reader
/-- Updates the message head being constructed.
 -/
Std.Http.Protocol.H1.Reader.setMessageHead : {dir : Std.Http.Protocol.H1.Direction} →
  Std.Http.Protocol.H1.Message.Head dir → Std.Http.Protocol.H1.Reader dir → Std.Http.Protocol.H1.Reader dir
-- Mathlib.LinearAlgebra.Projection
LinearMap.linearProjOfIsCompl_apply_right : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] (q : Submodule R E)
  {F : Type u_7} [inst_3 : AddCommGroup F] [inst_4 : Module R F] (i : F →ₗ[R] E) (hi : Function.Injective ⇑i)
  (h : IsCompl i.range q) (x : ↥q), (LinearMap.linearProjOfIsCompl q i hi h) ↑x = 0
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.mem_erase : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k a : α}, a ∈ m.erase k ↔ (k == a) = false ∧ a ∈ m
-- Mathlib.Combinatorics.Enumerative.Composition
instDecidableEqCompositionAsSet : {n : ℕ} → DecidableEq (CompositionAsSet n)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.minKeyD_erase_eq_of_not_compare_minKeyD_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k fallback : α},
      (t.erase k).isEmpty = false →
        ¬cmp k (t.minKeyD fallback) = Ordering.eq → (t.erase k).minKeyD fallback = t.minKeyD fallback
-- Mathlib.Analysis.Calculus.FDeriv.Basic
hasFDerivWithinAt_univ : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {f' : E →L[𝕜] F} {x : E},
  HasFDerivWithinAt f f' Set.univ x ↔ HasFDerivAt f f' x
-- Batteries.Lean.Meta.UnusedNames
/-- Succeeds if `n` is equal to `query`, except `n` may have an additional `_i`
suffix for some natural number `i`. More specifically:

- If `n = query`, the result is `exactMatch`.
- If `n = query ++ "_i"` for some natural number `i`, the result is
  `suffixMatch i`.
- Otherwise the result is `noMatch`.
 -/
Lean.Name.matchUpToIndexSuffix : Lean.Name → Lean.Name → Lean.Name.MatchUpToIndexSuffix
-- Lean.Elab.DocString
Lean.Doc.instMonadLiftTermElabMDocM : MonadLift Lean.Elab.TermElabM Lean.Doc.DocM
-- Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
MvPolynomial.aeval_esymm_eq_multiset_esymm : ∀ {S : Type u_4} (σ : Type u_5) (R : Type u_6) [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Fintype σ]
  [inst_3 : Algebra R S] (n : ℕ) (f : σ → S),
  (MvPolynomial.aeval f) (MvPolynomial.esymm σ R n) = (Multiset.map f Finset.univ.val).esymm n
-- Init.GrindInstances.Ring.Fin
Lean.Grind.Fin.neg_add_cancel : ∀ {n : ℕ} [inst : NeZero n] (a : Fin n), -a + a = 0
-- Init.Data.String.Basic
_private.Init.Data.String.Basic.0.ByteArray.isSome_utf8Decode?go_iff : ∀ {i : ℕ} {b : ByteArray} {hi : i ≤ b.size} {acc : Array Char},
  (ByteArray.utf8Decode?.go b i acc hi).isSome = true ↔ (b.extract i b.size).IsValidUTF8
-- Mathlib.Topology.Semicontinuity.Basic
upperSemicontinuousOn_iff_preimage_Iio : ∀ {α : Type u_4} [inst : TopologicalSpace α] {β : Type u_5} {f : α → β} {s : Set α} [inst_1 : Preorder β],
  UpperSemicontinuousOn f s ↔ ∀ (b : β), ∃ u, IsOpen u ∧ s ∩ f ⁻¹' Set.Iio b = s ∩ u
-- Std.Data.DTreeMap.Internal.Queries
/-- Implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.Const.getEntryGED : {α : Type u} → {β : Type v} → [Ord α] → α → (Std.DTreeMap.Internal.Impl α fun x => β) → α × β → α × β
-- Mathlib.Combinatorics.SimpleGraph.Maps
/-- A graph homomorphism is a map on vertex sets that respects adjacency relations.

The notation `G →g G'` represents the type of graph homomorphisms.  -/
SimpleGraph.Hom : {V : Type u_1} → {W : Type u_2} → SimpleGraph V → SimpleGraph W → Type (max u_1 u_2)
-- Lean.Server.RequestCancellation
Lean.Server.RequestCancellationToken.requestCancellationTask : Lean.Server.RequestCancellationToken → Lean.Server.ServerTask Unit
-- Mathlib.RingTheory.MvPowerSeries.Equiv
MvPowerSeries.isNoetherianRing : ∀ {σ : Type u_1} (S : Type u_3) [inst : CommRing S] [IsNoetherianRing S] [Finite σ],
  IsNoetherianRing (MvPowerSeries σ S)
-- Init.Data.Vector.Lemmas
Vector.toArray_inj : ∀ {α : Type u_1} {n : ℕ} {xs ys : Vector α n}, xs.toArray = ys.toArray ↔ xs = ys
-- Mathlib.Topology.Order
nhds_top : ∀ {α : Type u} {a : α}, nhds a = ⊤
-- Mathlib.Order.Filter.Tendsto
Filter.le_map_of_right_inverse : ∀ {α : Type u_1} {β : Type u_2} {mab : α → β} {mba : β → α} {f : Filter α} {g : Filter β},
  mab ∘ mba =ᶠ[g] id → Filter.Tendsto mba g f → g ≤ Filter.map mab f
-- Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
SSet.N.mk_dim : ∀ {X : SSet} {n : ℕ} (x : X.obj (Opposite.op { len := n })) (hx : x ∈ X.nonDegenerate n), (SSet.N.mk x hx).dim = n
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
ModuleCat.MonoidalCategory.associator_hom_apply : ∀ {R : Type u} [inst : CommRing R] {M N K : ModuleCat R} (m : ↑M) (n : ↑N) (k : ↑K),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.associator M N K).hom)
      (m ⊗ₜ[R] n ⊗ₜ[R] k) =
    m ⊗ₜ[R] (n ⊗ₜ[R] k)
-- Init.Data.SInt.Lemmas
Int64.toBitVec_ofInt : ∀ (i : ℤ), (Int64.ofInt i).toBitVec = BitVec.ofInt 64 i
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.instInhabitedRuleExpr.default : Aesop.Frontend.RuleExpr
-- Mathlib.Algebra.Ring.CompTypeclasses
RingHomInvPair.triples : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁}
  [RingHomInvPair σ₁₂ σ₂₁], RingHomCompTriple σ₁₂ σ₂₁ (RingHom.id R₁)
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
UniformContinuous.const_nsmul : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : AddGroup α] [IsUniformAddGroup α]
  [inst_3 : UniformSpace β] {f : β → α}, UniformContinuous f → ∀ (n : ℕ), UniformContinuous fun x => n • f x
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
/-- **Kronecker's Theorem:** A non-zero algebraic integer whose conjugates are all inside the closed
unit disk is a root of unity.  -/
NumberField.Embeddings.pow_eq_one_of_norm_le_one : ∀ (K : Type u_1) [inst : Field K] [NumberField K] (A : Type u_2) [inst_2 : NormedField A] [IsAlgClosed A]
  [NormedAlgebra ℚ A] {x : K}, x ≠ 0 → IsIntegral ℤ x → (∀ (φ : K →+* A), ‖φ x‖ ≤ 1) → ∃ n, ∃ (_ : 0 < n), x ^ n = 1
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.mem_of_mem_erase : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {k a : α},
  (t.erase k).contains a = true → t.contains a = true