mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.NumberTheory.NumberField.Basic
NumberField.RingOfIntegers.instIsNoetherianInt : ∀ (K : Type u_1) [inst : Field K] [NumberField K], IsNoetherian ℤ (NumberField.RingOfIntegers K)
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
SimpleGraph.Subgraph.Connected.mono : ∀ {V : Type u} {G : SimpleGraph V} {H H' : G.Subgraph}, H ≤ H' → H.verts = H'.verts → H.Connected → H'.Connected
-- Mathlib.MeasureTheory.OuterMeasure.Induced
MeasureTheory.OuterMeasure.trim_sum_ge : ∀ {α : Type u_1} [inst : MeasurableSpace α] {ι : Type u_2} (m : ι → MeasureTheory.OuterMeasure α),
  (MeasureTheory.OuterMeasure.sum fun i => (m i).trim) ≤ (MeasureTheory.OuterMeasure.sum m).trim
-- Mathlib.Data.Multiset.FinsetOps
Multiset.Nodup.ndinsert : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Multiset α} (a : α), s.Nodup → (Multiset.ndinsert a s).Nodup
-- Mathlib.ModelTheory.Definability
Set.DefinableFun.comp : ∀ {M : Type u_1} {L : FirstOrder.Language} [inst : L.Structure M] {α : Type u_2} {β : Type u_3} {A : Set M}
  {f : (α → M) → M} [Finite α] {g : (β → M) → α → M},
  Set.DefinableMap L A g → Set.DefinableFun L A f → Set.DefinableFun L A fun v => f (g v)
-- Mathlib.Algebra.Star.MonoidHom
StarMulEquiv.mk.congr_simp : ∀ {A : Type u_6} {B : Type u_7} [inst : Mul A] [inst_1 : Mul B] [inst_2 : Star A] [inst_3 : Star B]
  (toMulEquiv toMulEquiv_1 : A ≃* B) (e_toMulEquiv : toMulEquiv = toMulEquiv_1)
  (map_star' : ∀ (a : A), toMulEquiv.toFun (star a) = star (toMulEquiv.toFun a)),
  { toMulEquiv := toMulEquiv, map_star' := map_star' } = { toMulEquiv := toMulEquiv_1, map_star' := ⋯ }
-- Mathlib.LinearAlgebra.Alternating.Basic
LinearMap.compAlternatingMapₗ_apply : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {ι : Type u_7} (S : Type u_10) {N₂ : Type u_11}
  [inst_5 : AddCommMonoid N₂] [inst_6 : Module R N₂] [inst_7 : Semiring S] [inst_8 : Module S N] [inst_9 : Module S N₂]
  [inst_10 : SMulCommClass R S N] [inst_11 : SMulCommClass R S N₂] [inst_12 : LinearMap.CompatibleSMul N N₂ S R]
  (g : N →ₗ[R] N₂) (f : M [⋀^ι]→ₗ[R] N), (LinearMap.compAlternatingMapₗ S g) f = g.compAlternatingMap f
-- Lean.Meta.Tactic.Simp.Simproc
Lean.Meta.Simp.SimprocDeclExtState.mk.inj : ∀ {builtin : Std.HashMap Lean.Name (Array Lean.Meta.SimpTheoremKey)}
  {newEntries : Lean.PHashMap Lean.Name (Array Lean.Meta.SimpTheoremKey)}
  {builtin_1 : Std.HashMap Lean.Name (Array Lean.Meta.SimpTheoremKey)}
  {newEntries_1 : Lean.PHashMap Lean.Name (Array Lean.Meta.SimpTheoremKey)},
  { builtin := builtin, newEntries := newEntries } = { builtin := builtin_1, newEntries := newEntries_1 } →
    builtin = builtin_1 ∧ newEntries = newEntries_1
-- Batteries.Data.Fin.Coding
_private.Batteries.Data.Fin.Coding.0.Fin.encodeFun.match_1.splitter : {n : ℕ} →
  (motive : (x : ℕ) → (Fin x → Fin n) → Sort u_1) →
    (x : ℕ) →
      (x_1 : Fin x → Fin n) →
        ((x : Fin 0 → Fin n) → motive 0 x) → ((m : ℕ) → (f : Fin (m + 1) → Fin n) → motive m.succ f) → motive x x_1
-- Init.Data.Iterators.Lemmas.Combinators.Append
_private.Init.Data.Iterators.Lemmas.Combinators.Append.0.Std.Iter.step_append.match_1.eq_3 : ∀ {α₁ β : Type u_1} [inst : Std.Iterator α₁ Id β] {it₁ : Std.Iter β} (motive : it₁.Step → Sort u_2)
  (h : it₁.IsPlausibleStep Std.IterStep.done)
  (h_1 :
    (it₁' : Std.Iter β) →
      (out : β) → (h : it₁.IsPlausibleStep (Std.IterStep.yield it₁' out)) → motive ⟨Std.IterStep.yield it₁' out, h⟩)
  (h_2 : (it₁' : Std.Iter β) → (h : it₁.IsPlausibleStep (Std.IterStep.skip it₁')) → motive ⟨Std.IterStep.skip it₁', h⟩)
  (h_3 : (h : it₁.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩),
  (match ⟨Std.IterStep.done, 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, h⟩ => h_3 h) =
    h_3 h
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.congrLeftₐ_symm_apply_apply : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {Z : Type u_6} (R : Type u_7)
  [inst_2 : CommSemiring R] [inst_3 : Semiring Z] [inst_4 : Algebra R Z] (e : X ≃ₜ Y) (g : LocallyConstant Y Z) (a : X),
  ((LocallyConstant.congrLeftₐ R e).symm g) a = g (e a)
-- Mathlib.Algebra.Category.Grp.Images
/-- the factorisation of any morphism in `AddCommGrpCat` through a mono.  -/
AddCommGrpCat.monoFactorisation : {G H : AddCommGrpCat} → (f : G ⟶ H) → CategoryTheory.Limits.MonoFactorisation f
-- Mathlib.Algebra.Order.Module.HahnEmbedding
/-- **Hahn embedding theorem for an ordered module**

There exists a strictly monotone `M →ₗ[K] Lex R⟦FiniteArchimedeanClass M⟧` that maps
`ArchimedeanClass M` to `HahnSeries.orderTop` in the expected way, as long as
`HahnEmbedding.Seed K M R` is nonempty. The `HahnEmbedding.Partial` with maximal domain is the
desired embedding.  -/
hahnEmbedding_isOrderedModule : ∀ {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] {R : Type u_3} [inst_9 : AddCommGroup R]
  [inst_10 : LinearOrder R] [inst_11 : Module K R] [IsOrderedAddMonoid R] [Archimedean R]
  [h : Nonempty (HahnEmbedding.Seed K M R)],
  ∃ f,
    StrictMono ⇑f ∧ ∀ (a : M), ArchimedeanClass.mk a = (FiniteArchimedeanClass.withTopOrderIso M) (ofLex (f a)).orderTop
-- Mathlib.LinearAlgebra.TensorAlgebra.Basic
TensorAlgebra.lift_ι_apply : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {A : Type u_3}
  [inst_3 : Semiring A] [inst_4 : Algebra R A] (f : M →ₗ[R] A) (x : M),
  ((TensorAlgebra.lift R) f) ((TensorAlgebra.ι R) x) = f x
-- Mathlib.ModelTheory.Equivalence
FirstOrder.Language.Theory.Iff.instIsTransBoundedFormula : ∀ {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : ℕ}, IsTrans (L.BoundedFormula α n) T.Iff
-- Std.Http.Data.Method
Std.Http.Method.unbind.sizeOf_spec : sizeOf Std.Http.Method.unbind = 1
-- Mathlib.Topology.Order.LowerUpperTopology
Topology.WithLower.ofLower_symm : ∀ {α : Type u_1}, Topology.WithLower.ofLower.symm = Topology.WithLower.toLower
-- Mathlib.Tactic.Linarith.Oracle.FourierMotzkin
Mathlib.Tactic.Linarith.CompSource.assump.sizeOf_spec : ∀ (a : ℕ), sizeOf (Mathlib.Tactic.Linarith.CompSource.assump a) = 1 + sizeOf a
-- Lean.Elab.Tactic.Omega.Core
/-- Takes a proof that `s.sat' x v` for some `s` such that `s.isImpossible`,
and constructs a proof of `False`.
 -/
Lean.Elab.Tactic.Omega.Problem.proveFalse : {s : Lean.Omega.Constraint} →
  {x : Lean.Omega.Coeffs} →
    Lean.Elab.Tactic.Omega.Justification s x → Array Lean.Elab.Tactic.Omega.Proof → Lean.Elab.Tactic.Omega.Proof
-- Lean.CoreM
Lean.compileDecls : Array Lean.Name → optParam Bool true → Lean.CoreM Unit
-- Mathlib.NumberTheory.Padics.PadicNorm
/-- `padicNorm p` is symmetric.  -/
padicNorm.neg : ∀ {p : ℕ} (q : ℚ), padicNorm p (-q) = padicNorm p q
-- Mathlib.Order.Bounds.Basic
isGreatest_Icc : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, a ≤ b → IsGreatest (Set.Icc a b) b
-- Mathlib.Algebra.DirectSum.Module
DirectSum.linearEquivFunOnFintype_symm_single : ∀ (R : Type u) [inst : Semiring R] {ι : Type v} {M : ι → Type w} [inst_1 : (i : ι) → AddCommMonoid (M i)]
  [inst_2 : (i : ι) → Module R (M i)] [inst_3 : DecidableEq ι] [inst_4 : Fintype ι] (i : ι) (m : M i),
  (DirectSum.linearEquivFunOnFintype R ι M).symm (Pi.single i m) = (DirectSum.lof R ι M i) m
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.size_insertManyIfNewUnit!_list : ∀ {α : Type u} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α fun x => Unit} [Std.TransOrd α] [inst : BEq α]
  [Std.LawfulBEqOrd α],
  t.WF →
    ∀ {l : List α},
      List.Pairwise (fun a b => ¬compare a b = Ordering.eq) l →
        (∀ a ∈ t, l.contains a = false) →
          (↑(Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit! t l)).size = t.size + l.length
-- Init.Data.List.Find
List.findIdx.go.eq_1 : ∀ {α : Type u} (p : α → Bool) (a : ℕ), List.findIdx.go p [] a = a
-- Mathlib.Tactic.WLOG
/-- `wlog goal h P xs H` will return two goals: the `hypothesisGoal`, which adds an assumption
`h : P` to the context of `goal`, and the `reductionGoal`, which requires showing that the case
`h : ¬ P` can be reduced to the case where `P` holds (typically by symmetry).

In `reductionGoal`, there will be two additional assumptions:
- `h : ¬ P`: the assumption that `P` does not hold
- `H`: which is the statement that in the old context `P` suffices to prove the goal.
  If `H` is `none`, the name `this` is used.

If `xs` is `none`, all hypotheses are reverted to produce the reduction goal's hypothesis `H`.
Otherwise, the `xs` are elaborated to hypotheses in the context of `goal`, and only those
hypotheses are reverted (and any that depend on them).

If `h` is `none`, the hypotheses of types `P` and `¬ P` in both branches will be inaccessible.  -/
Lean.MVarId.wlog : Lean.MVarId →
  Option Lean.Name →
    Lean.Expr →
      optParam (Option (Lean.TSyntaxArray `ident)) none →
        optParam (Option Lean.Name) none → Lean.Elab.Tactic.TacticM Mathlib.Tactic.WLOGResult
-- Init.Prelude
/-- The typeclass behind the notation `a <<< b : γ` where `a : α`, `b : β`.  -/
HShiftLeft : Type u → Type v → outParam (Type w) → Type (max (max u v) w)
-- Init.Data.UInt.Lemmas
UInt32.toNat_ofNat_of_lt' : ∀ {n : ℕ}, n < UInt32.size → (UInt32.ofNat n).toNat = n
-- Mathlib.Algebra.Homology.ShortComplex.ModuleCat
CategoryTheory.ShortComplex.instPreservesHomologyModuleCatAbForget₂LinearMapIdCarrierAddMonoidHomCarrier : ∀ {R : Type u} [inst : Ring R], (CategoryTheory.forget₂ (ModuleCat R) Ab).PreservesHomology
-- Mathlib.SetTheory.Cardinal.Aleph
Ordinal.isInitial_omega : ∀ (o : Ordinal.{u_1}), (Ordinal.omega o).IsInitial
-- Lean.Meta.Tactic.Grind.Parser
Lean.Parser.Command.GrindCnstr.notDefEq : Lean.Parser.Parser
-- Mathlib.Topology.Algebra.TopologicallyNilpotent
coe_topologicalNilradical : ∀ (R : Type u_1) [inst : TopologicalSpace R] [inst_1 : CommRing R] [inst_2 : IsLinearTopology R R],
  ↑(topologicalNilradical R) = {a | IsTopologicallyNilpotent a}
-- Mathlib.Algebra.Order.Monovary
/-- **Alias** of the reverse direction of `monovaryOn_inv_right₀`. -/
AntivaryOn.inv_right₀ : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : LinearOrder α] [inst_1 : Semifield β] [inst_2 : LinearOrder β]
  [IsStrictOrderedRing β] {s : Set ι} {f : ι → α} {g : ι → β},
  (∀ i ∈ s, 0 < g i) → AntivaryOn f g s → MonovaryOn f g⁻¹ s
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.integral_mono_interval : ∀ {f : ℝ → ℝ} {a b : ℝ} {μ : MeasureTheory.Measure ℝ} {c d : ℝ},
  c ≤ a →
    a ≤ b →
      b ≤ d →
        0 ≤ᵐ[μ.restrict (Set.Ioc c d)] f →
          IntervalIntegrable f μ c d → ∫ (x : ℝ) in a..b, f x ∂μ ≤ ∫ (x : ℝ) in c..d, f x ∂μ
-- Mathlib.MeasureTheory.Group.Arithmetic
Measurable.inv : ∀ {G : Type u_2} {α : Type u_3} [inst : Inv G] [inst_1 : MeasurableSpace G] [MeasurableInv G] {m : MeasurableSpace α}
  {f : α → G}, Measurable f → Measurable f⁻¹
-- Mathlib.Combinatorics.Additive.ETransform
/-- An **e-transform**. Turns `(s, t)` into `(s ∩ s • e, t ∪ e⁻¹ • t)`. This reduces the
product of the two sets.  -/
Finset.mulETransformLeft : {α : Type u_1} → [DecidableEq α] → [Group α] → α → Finset α × Finset α → Finset α × Finset α
-- Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit
CategoryTheory.Limits.instPreservesFiniteLimitsFunctorColimOfPreservesColimitsOfShapeOfHasFiniteLimitsOfReflectsIsomorphismsForget : ∀ {K : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} K] [Small.{v, u₂} K] [CategoryTheory.IsFiltered K] {C : Type u}
  [inst_3 : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type v}
  [inst_4 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_5 : CategoryTheory.ConcreteCategory C FC]
  [CategoryTheory.Limits.PreservesFiniteLimits (CategoryTheory.forget C)]
  [CategoryTheory.Limits.PreservesColimitsOfShape K (CategoryTheory.forget C)] [CategoryTheory.Limits.HasFiniteLimits C]
  [inst_9 : CategoryTheory.Limits.HasColimitsOfShape K C] [(CategoryTheory.forget C).ReflectsIsomorphisms],
  CategoryTheory.Limits.PreservesFiniteLimits CategoryTheory.Limits.colim
-- Mathlib.Order.Filter.Cofinite
Filter.coprodᵢ_cofinite : ∀ {ι : Type u_1} {α : ι → Type u_4} [Finite ι], (Filter.coprodᵢ fun i => Filter.cofinite) = Filter.cofinite
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.contains_diff_eq_false_of_contains_eq_false_left : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  (h₁ : m₁.WF),
  m₂.WF →
    ∀ {k : α},
      Std.DTreeMap.Internal.Impl.contains k m₁ = false → Std.DTreeMap.Internal.Impl.contains k (m₁.diff m₂ ⋯) = false
-- Init.Data.Range.Polymorphic.Fin
Fin.instHasSize_2 : {n : ℕ} → Std.Rxi.HasSize (Fin n)
-- Mathlib.LinearAlgebra.TensorAlgebra.Basis
/-- A basis provides an algebra isomorphism with the free algebra, replacing each basis vector
with its index.  -/
TensorAlgebra.equivFreeAlgebra : {κ : Type uκ} →
  {R : Type uR} →
    {M : Type uM} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : Module R M] → Module.Basis κ R M → TensorAlgebra R M ≃ₐ[R] FreeAlgebra R κ
-- Mathlib.Topology.Connected.PathConnected
pathComponent.eq_1 : ∀ {X : Type u_1} [inst : TopologicalSpace X] (x : X), pathComponent x = {y | Joined x y}
-- Lean.Meta.Closure
Lean.Meta.Closure.MkValueTypeClosureResult.levelArgs : Lean.Meta.Closure.MkValueTypeClosureResult → Array Lean.Level
-- Mathlib.Topology.PartialHomeomorph.Defs
Homeomorph.toPartialHomeomorph_symm_apply : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : X ≃ₜ Y),
  ↑e.toPartialHomeomorph.symm = ⇑e.symm
-- Lean.Data.Lsp.LanguageFeatures
/-- The semantic token modifiers included by default in the LSP specification.
Not used by the Lean core, but implementing them here allows them to be
utilized by users extending the Lean server.
 -/
Lean.Lsp.SemanticTokenModifier : Type
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.image_op_zero : ∀ {α : Type u_2} [inst : Zero α] [inst_1 : DecidableEq α], Finset.image AddOpposite.op 0 = 0
-- Mathlib.Analysis.FunctionalSpaces.SobolevInequality
MeasureTheory.SNormLESNormFDerivOfEqConst.congr_simp : ∀ (F : Type u_6) [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] {E : Type u_7} [inst_2 : NormedAddCommGroup E]
  [inst_3 : NormedSpace ℝ E] [inst_4 : MeasurableSpace E] [inst_5 : BorelSpace E] [inst_6 : FiniteDimensional ℝ E]
  (μ μ_1 : MeasureTheory.Measure E) (e_μ : μ = μ_1) [inst_7 : μ.IsAddHaarMeasure] [inst_8 : FiniteDimensional ℝ F]
  (p p_1 : ℝ),
  p = p_1 → MeasureTheory.SNormLESNormFDerivOfEqConst F μ p = MeasureTheory.SNormLESNormFDerivOfEqConst F μ_1 p_1
-- Mathlib.Topology.Algebra.NonUnitalStarAlgebra
/-- If a non-unital star subalgebra of a non-unital topological star algebra is commutative, then
so is its topological closure.

See note [reducible non-instances]  -/
NonUnitalStarSubalgebra.nonUnitalCommSemiringTopologicalClosure : {R : Type u_1} →
  {A : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : TopologicalSpace A] →
        [inst_2 : Star A] →
          [inst_3 : NonUnitalSemiring A] →
            [inst_4 : Module R A] →
              [inst_5 : ContinuousStar A] →
                [inst_6 : ContinuousConstSMul R A] →
                  [inst_7 : IsSemitopologicalSemiring A] →
                    [T2Space A] →
                      (s : NonUnitalStarSubalgebra R A) →
                        (∀ (x y : ↥s), x * y = y * x) → NonUnitalCommSemiring ↥s.topologicalClosure
-- Mathlib.Data.Multiset.UnionInter
Multiset.eq_union_right : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Multiset α}, s ≤ t → s ∪ t = t
-- Init.Data.SInt.Bitwise
Int64.and_self : ∀ {a : Int64}, a &&& a = a
-- Lean.Linter.MissingDocs
Lean.Linter.MissingDocs.checkRegisterBuiltinOption : Lean.Linter.MissingDocs.SimpleHandler
-- Mathlib.RingTheory.Coalgebra.Basic
Prod.counit_comp_inr : ∀ (R : Type u) (A : Type v) (B : Type w) [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : AddCommMonoid B]
  [inst_3 : Module R A] [inst_4 : Module R B] [inst_5 : Coalgebra R A] [inst_6 : Coalgebra R B],
  CoalgebraStruct.counit ∘ₗ LinearMap.inr R A B = CoalgebraStruct.counit
-- Mathlib.CategoryTheory.MorphismProperty.LiftingProperty
CategoryTheory.MorphismProperty.retracts_le_llp_rlp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (T : CategoryTheory.MorphismProperty C), T.retracts ≤ T.rlp.llp
-- Mathlib.Order.Interval.Set.Basic
Set.Icc_subset_Ici_self : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, Set.Icc b a ⊆ Set.Ici b
-- Mathlib.MeasureTheory.Measure.Map
MeasureTheory.Measure.map_of_not_aemeasurable : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α → β}
  {μ : MeasureTheory.Measure α}, ¬AEMeasurable f μ → MeasureTheory.Measure.map f μ = 0
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.Char.utf8ByteSize_getElem_utf8EncodeChar : ∀ {c : Char}, (String.utf8EncodeChar c)[0].utf8ByteSize ⋯ = c.utf8Size
-- Mathlib.Analysis.Analytic.Composition
FormalMultilinearSeries.id_comp : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  (p : FormalMultilinearSeries 𝕜 E F) (v0 : Fin 0 → E), (FormalMultilinearSeries.id 𝕜 F ((p 0) v0)).comp p = p
-- Mathlib.Algebra.Polynomial.FieldDivision
Polynomial.eval_iterate_derivative_rootMultiplicity : ∀ {R : Type u} [inst : CommRing R] {p : Polynomial R} {t : R},
  Polynomial.eval t ((⇑Polynomial.derivative)^[Polynomial.rootMultiplicity t p] p) =
    (Polynomial.rootMultiplicity t p).factorial •
      Polynomial.eval t (p /ₘ (Polynomial.X - Polynomial.C t) ^ Polynomial.rootMultiplicity t p)
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Basic
/-- Given a `k`-linear `G`-representation `A`, the complex of inhomogeneous cochains is isomorphic
to `Hom(P, A)`, where `P` is the bar resolution of `k` as a trivial `G`-representation.  -/
groupCohomology.inhomogeneousCochainsIso : {k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] →
      (A : Rep.{u, u, u} k G) → groupCohomology.inhomogeneousCochains A ≅ (Rep.barComplex k G).linearYonedaObj k A
-- Mathlib.Algebra.Category.MonCat.Limits
CommMonCat.commMonoidObj.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J CommMonCat) (j : J),
  CommMonCat.commMonoidObj F j =
    { toMul := CommMonCat.commMonoidObj._aux_1 F j, mul_assoc := ⋯, toOne := CommMonCat.commMonoidObj._aux_4 F j,
      one_mul := ⋯, mul_one := ⋯, toNPow := CommMonCat.commMonoidObj._aux_8 F j, npow_zero := ⋯, npow_succ := ⋯,
      mul_comm := ⋯ }
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.full_map : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] {A' : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] {B' : Type u₅} [inst_4 : CategoryTheory.Category.{v₅, u₅} B']
  {T' : Type u₆} [inst_5 : CategoryTheory.Category.{v₆, u₆} T'] {L : CategoryTheory.Functor A T}
  {R : CategoryTheory.Functor B T} {L' : CategoryTheory.Functor A' T'} {R' : CategoryTheory.Functor B' T'}
  {F₁ : CategoryTheory.Functor A A'} {F₂ : CategoryTheory.Functor B B'} {F : CategoryTheory.Functor T T'}
  (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') [F.Faithful] [F₁.Full] [F₂.Full] [CategoryTheory.IsIso α]
  [CategoryTheory.IsIso β], (CategoryTheory.Comma.map α β).Full
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F.leftOp : Cᵒᵖ ⥤ D` preserves limits, then `F : C ⥤ Dᵒᵖ` preserves colimits.  -/
CategoryTheory.Limits.preservesColimitsOfSize_of_leftOp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C Dᵒᵖ) [CategoryTheory.Limits.PreservesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F.leftOp],
  CategoryTheory.Limits.PreservesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.canonicalEmbedding.integralBasis_repr_apply : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] (x : K)
  (i : Module.Free.ChooseBasisIndex ℤ (NumberField.RingOfIntegers K)),
  ((NumberField.canonicalEmbedding.latticeBasis K).repr ((NumberField.canonicalEmbedding K) x)) i =
    ↑(((NumberField.integralBasis K).repr x) i)
-- Init.Data.List.Lemmas
List.mem_iff_getElem? : ∀ {α : Type u_1} {a : α} {l : List α}, a ∈ l ↔ ∃ i, l[i]? = some a
-- Mathlib.Topology.Compactification.OnePoint.Basic
OnePoint.continuous_coe : ∀ {X : Type u_1} [inst : TopologicalSpace X], Continuous OnePoint.some
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
MeasureTheory.integral_comp_rpow_Ioi_of_pos' : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {g : ℝ → E} {p : ℝ},
  0 < p → ∀ {c : ℝ}, 0 ≤ c → ∫ (x : ℝ) in Set.Ioi (c ^ p⁻¹), (p * x ^ (p - 1)) • g (x ^ p) = ∫ (y : ℝ) in Set.Ioi c, g y
-- Mathlib.Geometry.Manifold.ContMDiff.Constructions
contMDiff_snd : ∀ {𝕜 : 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] {F : Type u_8} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {G : Type u_9} [inst_8 : TopologicalSpace G] {J : ModelWithCorners 𝕜 F G} {N : Type u_10}
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n : WithTop ℕ∞}, ContMDiff (I.prod J) J n Prod.snd
-- Mathlib.Order.Filter.Pointwise
Filter.pure_mul_pure : ∀ {α : Type u_2} [inst : Mul α] {a b : α}, pure a * pure b = pure (a * b)
-- Lean.Data.Lsp.Internal
Lean.Lsp.LeanImportClosureParams.mk.sizeOf_spec : ∀ (importClosure : Array Lean.Lsp.DocumentUri), sizeOf { importClosure := importClosure } = 1 + sizeOf importClosure
-- Aesop.Tree.Data
Aesop.Goal.setUnsafeQueue : Aesop.UnsafeQueue → Aesop.Goal → Aesop.Goal
-- Mathlib.LinearAlgebra.LinearIndependent.Lemmas
LinearIndependent.pair_add_smul_right_iff : ∀ {R : Type u_2} {M : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {x y : M} {S : Type u_6}
  [inst_3 : CommRing S] [IsDomain S] [inst_5 : Module S R] [inst_6 : Module S M] [SMulCommClass S R M]
  [IsScalarTower S R M] [Module.IsTorsionFree S R] (c : S),
  LinearIndependent R ![x, c • x + y] ↔ LinearIndependent R ![x, y]
-- Mathlib.NumberTheory.ModularForms.Basic
/-- **Alias** of `FunLike.coe_smul`. -/
ModularForm.IsGLPos.coe_smul : ∀ {M : Type u_1} {F : Type u_3} {α : Type u_5} {β : Type u_6} [inst : FunLike F α β] [inst_1 : SMul M F]
  [inst_2 : SMul M β] [IsSMulApply M F α β] (n : M) (f : F), ⇑(n • f) = n • ⇑f
-- Lean.DocString.Types
/-- A genre-specific inline element. `container` specifies what kind of element it is, and `content`
specifies the contained elements.
 -/
Lean.Doc.Inline.other : {i : Type u} → i → Array (Lean.Doc.Inline i) → Lean.Doc.Inline i
-- Mathlib.GroupTheory.OreLocalization.Basic
/-- The universal morphism `universalMulHom` is unique.  -/
OreLocalization.universalMulHom_unique : ∀ {R : Type u_1} [inst : Monoid R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S] {T : Type u_2}
  [inst_2 : Monoid T] (f : R →* T) (fS : ↥S →* Tˣ) (hf : ∀ (s : ↥S), f ↑s = ↑(fS s)) (φ : OreLocalization S R →* T),
  (∀ (r : R), φ (OreLocalization.numeratorHom r) = f r) → φ = OreLocalization.universalMulHom f fS hf
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Hom.mem_eqLocus : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [inst : L.Structure M] [inst_1 : L.Structure N]
  {f g : L.Hom M N} {x : M}, x ∈ f.eqLocus g ↔ f x = g x