mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RepresentationTheory.Induced
Rep.coinvariantsTensorIndNatIso_hom_app : ∀ {k : Type u} [inst : CommRing k] {G H : Type u} [inst_1 : Group G] [inst_2 : Group H] (φ : G →* H)
  (A : Rep.{u, u, u} k G) (X : Rep.{u, u, u} k H),
  (Rep.coinvariantsTensorIndNatIso φ A).hom.app X = Rep.coinvariantsTensorIndHom φ A X
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
SimplexCategoryGenRel.IsAdmissible.brecOn : ∀ {motive : (m : ℕ) → (L : List ℕ) → SimplexCategoryGenRel.IsAdmissible m L → Prop} {m : ℕ} {L : List ℕ}
  (t : SimplexCategoryGenRel.IsAdmissible m L),
  (∀ (m : ℕ) (L : List ℕ) (t : SimplexCategoryGenRel.IsAdmissible m L),
      SimplexCategoryGenRel.IsAdmissible.below t → motive m L t) →
    motive m L t
-- Mathlib.Algebra.Group.Invertible.Defs
invOf_mul_eq_iff_eq_mul_left : ∀ {α : Type u} [inst : Monoid α] {a b c : α} [inst_1 : Invertible c], ⅟c * a = b ↔ a = c * b
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
IsPreconnected.measurableSet : ∀ {α : Type u_1} {s : Set α} [inst : TopologicalSpace α] {mα : MeasurableSpace α} [OpensMeasurableSpace α]
  [inst_2 : LinearOrder α] [OrderClosedTopology α], IsPreconnected s → MeasurableSet s
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products
CategoryTheory.Limits.inv_piComparison_comp_map_π : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) {J : Type w} (f : J → C) [inst_2 : CategoryTheory.Limits.HasProduct f]
  [inst_3 : CategoryTheory.Limits.HasProduct fun j => G.obj (f j)]
  [inst_4 : CategoryTheory.IsIso (CategoryTheory.Limits.piComparison G f)] (j : J),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.Limits.piComparison G f))
      (G.map (CategoryTheory.Limits.Pi.π f j)) =
    CategoryTheory.Limits.Pi.π (fun x => G.obj (f x)) j
-- Mathlib.RingTheory.Localization.Away.Basic
/-- Given `x : R`, a localization map `F : R →+* S` away from `x`, and a map of `CommSemiring`s
`g : R →+* P` such that `g x` is invertible, the homomorphism induced from `S` to `P` sending
`z : S` to `g y * (g x)⁻ⁿ`, where `y : R, n : ℕ` are such that `z = F y * (F x)⁻ⁿ`.  -/
IsLocalization.Away.lift : {R : Type u_1} →
  [inst : CommSemiring R] →
    {S : Type u_2} →
      [inst_1 : CommSemiring S] →
        [inst_2 : Algebra R S] →
          {P : Type u_3} →
            [inst_3 : CommSemiring P] → (x : R) → [IsLocalization.Away x S] → {g : R →+* P} → IsUnit (g x) → S →+* P
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap.0.Std.IterM.forIn_filterMapWithPostcondition.match_1.eq_1 : ∀ {β₂ : Type u_1} (motive : Option β₂ → Sort u_2) (c : β₂) (h_1 : (c : β₂) → motive (some c))
  (h_2 : Unit → motive none),
  (match some c with
    | some c => h_1 c
    | none => h_2 ()) =
    h_1 c
-- Mathlib.Topology.LocallyConstant.Basic
LocallyConstant.mulIndicator_of_mem : ∀ {X : Type u_1} [inst : TopologicalSpace X] {R : Type u_5} [inst_1 : One R] {U : Set X} (f : LocallyConstant X R)
  {a : X} (hU : IsClopen U), a ∈ U → (f.mulIndicator hU) a = f a
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.size_filterMap_le_size : ∀ {α : Type u} {β : Type v} {γ : Type w} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {f : α → β → Option γ}, (Std.ExtHashMap.filterMap f m).size ≤ m.size
-- Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Real.mul_log_pos : ∀ {x : ℝ}, 1 < x → 0 < x * Real.log x
-- Lean.Server.FileWorker.SemanticHighlighting
/-- Keywords for which a specific semantic token is provided.  -/
Lean.Server.FileWorker.keywordSemanticTokenMap : Std.TreeMap String Lean.Lsp.SemanticTokenType compare
-- Mathlib.AlgebraicTopology.SimplexCategory.SemiSimplexCategory
SemiSimplexCategory.homOfMono.congr_simp : ∀ {n m : SemiSimplexCategory}
  (f f_1 : SemiSimplexCategory.toSimplexCategory.obj n ⟶ SemiSimplexCategory.toSimplexCategory.obj m) (e_f : f = f_1)
  [inst : CategoryTheory.Mono f], SemiSimplexCategory.homOfMono f = SemiSimplexCategory.homOfMono f_1
-- Init.Data.List.Attach
List.attachWith_append : ∀ {α : Type u_1} {P : α → Prop} {xs ys : List α} {H : ∀ a ∈ xs ++ ys, P a},
  (xs ++ ys).attachWith P H = xs.attachWith P ⋯ ++ ys.attachWith P ⋯
-- Mathlib.Combinatorics.HalesJewett
Combinatorics.Line.ColorFocused.mk.sizeOf_spec : ∀ {α : Type u_5} {ι : Type u_6} {κ : Type u_7} {C : (ι → Option α) → κ} [inst : SizeOf α] [inst_1 : SizeOf ι]
  [inst_2 : SizeOf κ] (lines : Multiset (Combinatorics.Line.AlmostMono C)) (focus : ι → Option α)
  (is_focused : ∀ p ∈ lines, ↑p.line none = focus)
  (distinct_colors : (Multiset.map Combinatorics.Line.AlmostMono.color lines).Nodup),
  sizeOf { lines := lines, focus := focus, is_focused := is_focused, distinct_colors := distinct_colors } =
    1 + sizeOf lines + sizeOf distinct_colors
-- Lean.Data.Lsp.InitShutdown
Lean.Lsp.InitializeParams.processId? : Lean.Lsp.InitializeParams → Option ℤ
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.coe_sInf : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] (S : Set (L.Substructure M)), ↑(sInf S) = ⋂ s ∈ S, ↑s
-- Mathlib.Algebra.Group.Hom.Defs
AddHom.id_comp : ∀ {M : Type u_4} {N : Type u_5} [inst : Add M] [inst_1 : Add N] (f : M →ₙ+ N), (AddHom.id N).comp f = f
-- Mathlib.Algebra.Order.Hom.TypeTags
/-- The multiplicative version of an additivized ordered monoid is order-mul-equivalent to itself.
 -/
OrderMonoidIso.toMultiplicative_toAdditive : {G : Type u_1} → [inst : CommMonoid G] → [inst_1 : PartialOrder G] → Multiplicative (Additive G) ≃*o G
-- Mathlib.ModelTheory.Algebra.Field.Basic
FirstOrder.Field.FieldAxiom.existsPairNE : FirstOrder.Field.FieldAxiom
-- Mathlib.RingTheory.DedekindDomain.Factorization
IsDedekindDomain.HeightOneSpectrum.maxPowDividing_eq_pow_multiset_count : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R)
  {I : Ideal R},
  I ≠ 0 → v.maxPowDividing I = v.asIdeal ^ Multiset.count v.asIdeal (UniqueFactorizationMonoid.normalizedFactors I)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.insertMany_list_singleton : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {k : α} {v : β}, Std.ExtDTreeMap.Const.insertMany t [(k, v)] = t.insert k v
-- Mathlib.GroupTheory.OrderOfElement
Nat.Coprime.nsmul_right_bijective : ∀ {n : ℕ} {G : Type u_6} [inst : AddGroup G], (Nat.card G).Coprime n → Function.Bijective fun x => n • x
-- Mathlib.Data.Matrix.Basic
Matrix.sum_mulVec : ∀ {m : Type u_2} {n : Type u_3} {α : Type u_11} {ι : Type u_14} [inst : NonUnitalNonAssocSemiring α]
  [inst_1 : Fintype n] (s : Finset ι) (x : ι → Matrix m n α) (y : n → α),
  (∑ i ∈ s, x i).mulVec y = ∑ i ∈ s, (x i).mulVec y
-- Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant
CategoryTheory.Functor.IsEventuallyConstantTo.isoMap_inv_hom_id_assoc : ∀ {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] {F : CategoryTheory.Functor J C} {i₀ : J}
  (h : F.IsEventuallyConstantTo i₀) {i j : J} (φ : i ⟶ j) (hφ : Nonempty (j ⟶ i₀)) {Z : C} (h_1 : F.obj j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (h.isoMap φ hφ).inv (CategoryTheory.CategoryStruct.comp (F.map φ) h_1) = h_1
-- Mathlib.MeasureTheory.Group.Arithmetic
/-- **Alias** of `AEMeasurable.mul`. -/
AEMeasurable.mul' : ∀ {M : Type u_2} {α : Type u_3} [inst : MeasurableSpace M] [inst_1 : Mul M] {m : MeasurableSpace α} {f g : α → M}
  {μ : MeasureTheory.Measure α} [MeasurableMul₂ M], AEMeasurable f μ → AEMeasurable g μ → AEMeasurable (f * g) μ
-- Mathlib.Order.Interval.Set.LinearOrder
/-- This is a special case of `Ico_union_Ico`  -/
Set.Ico_union_Ico' : ∀ {α : Type u_1} [inst : LinearOrder α] {a b c d : α},
  c ≤ b → a ≤ d → Set.Ico a b ∪ Set.Ico c d = Set.Ico (min a c) (max b d)
-- Mathlib.Topology.DenseEmbedding
DenseRange.induction_on : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {e : α → β},
  DenseRange e → ∀ {p : β → Prop} (b₀ : β), IsClosed {b | p b} → (∀ (a : α), p (e a)) → p b₀
-- Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Dynamics.coverEntropy.eq_1 : ∀ {X : Type u_1} [inst : UniformSpace X] (T : X → X) (F : Set X),
  Dynamics.coverEntropy T F = ⨆ U ∈ uniformity X, Dynamics.coverEntropyEntourage T F U
-- Mathlib.Geometry.Manifold.Algebra.Monoid
ContMDiffOn.add : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞}
  {G : Type u_4} [inst_4 : Add G] [inst_5 : TopologicalSpace G] [inst_6 : ChartedSpace H G] {E' : Type u_5}
  [inst_7 : NormedAddCommGroup E'] [inst_8 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_9 : TopologicalSpace H']
  {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [inst_10 : TopologicalSpace M] [inst_11 : ChartedSpace H' M]
  [ContMDiffAdd I n G] {f g : M → G} {s : Set M},
  ContMDiffOn I' I n f s → ContMDiffOn I' I n g s → ContMDiffOn I' I n (f + g) s
-- Mathlib.AlgebraicGeometry.Gluing
AlgebraicGeometry.Scheme.GlueData.mk.injEq : ∀ (toGlueData : CategoryTheory.GlueData AlgebraicGeometry.Scheme)
  (f_open : ∀ (i j : toGlueData.J), AlgebraicGeometry.IsOpenImmersion (toGlueData.f i j))
  (toGlueData_1 : CategoryTheory.GlueData AlgebraicGeometry.Scheme)
  (f_open_1 : ∀ (i j : toGlueData_1.J), AlgebraicGeometry.IsOpenImmersion (toGlueData_1.f i j)),
  ({ toGlueData := toGlueData, f_open := f_open } = { toGlueData := toGlueData_1, f_open := f_open_1 }) =
    (toGlueData = toGlueData_1)
-- Mathlib.GroupTheory.Submonoid.Inverses
AddSubmonoid.leftNegEquiv_symm_add : ∀ {M : Type u_1} [inst : AddCommMonoid M] (S : AddSubmonoid M) (hS : S ≤ IsAddUnit.addSubmonoid M) (x : ↥S),
  ↑((S.leftNegEquiv hS).symm x) + ↑x = 0
-- Init.Data.Dyadic.Basic
Dyadic.instIsPartialOrder : Std.IsPartialOrder Dyadic
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.IsPath.disjoint_support_of_append : ∀ {V : Type u} {G : SimpleGraph V} {u v w : V} {p : G.Walk u v} {q : G.Walk v w},
  (p.append q).IsPath → ¬q.Nil → p.support.Disjoint q.tail.support
-- Mathlib.MeasureTheory.Function.ConditionalLExpectation
MeasureTheory.condLExp_eq_self : ∀ {Ω : Type u_1} {mΩ₀ mΩ : MeasurableSpace Ω} {X : Ω → ENNReal} (hm : mΩ ≤ mΩ₀) (P : MeasureTheory.Measure Ω)
  [hσ : MeasureTheory.SigmaFinite (P.trim hm)], Measurable X → P⁻[X | mΩ] = X
-- Mathlib.Analysis.Normed.Operator.Prod
ContinuousOn.prod_map_equivL : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {M₁ : Type u_5} {M₂ : Type u_6} {M₃ : Type u_7} {M₄ : Type u_8}
  [inst_1 : SeminormedAddCommGroup M₁] [inst_2 : NormedSpace 𝕜 M₁] [inst_3 : SeminormedAddCommGroup M₂]
  [inst_4 : NormedSpace 𝕜 M₂] [inst_5 : SeminormedAddCommGroup M₃] [inst_6 : NormedSpace 𝕜 M₃]
  [inst_7 : SeminormedAddCommGroup M₄] [inst_8 : NormedSpace 𝕜 M₄] {X : Type u_9} [inst_9 : TopologicalSpace X]
  {f : X → M₁ ≃L[𝕜] M₂} {g : X → M₃ ≃L[𝕜] M₄} {s : Set X},
  ContinuousOn (fun x => ↑(f x)) s →
    ContinuousOn (fun x => ↑(g x)) s → ContinuousOn (fun x => ↑((f x).prodCongr (g x))) s
-- Mathlib.Tactic.Linter.TextBased
_private.Mathlib.Tactic.Linter.TextBased.0.Mathlib.Linter.TextBased.instInhabitedStyleError : Inhabited Mathlib.Linter.TextBased.StyleError✝
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.Drop
_private.Std.Data.Iterators.Lemmas.Combinators.Monadic.Drop.0.Std.IterM.step_drop.match_3.eq_3 : ∀ {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [inst : Std.Iterator α m β] {it : Std.IterM m β}
  (motive : it.Step → Sort u_3) (h : it.IsPlausibleStep Std.IterStep.done)
  (h_1 :
    (it' : Std.IterM m β) →
      (out : β) → (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 : (it' : Std.IterM m β) → (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.Tactic.TermCongr
/-- Returns whether the proof is by reflexivity.
Such congruence proofs are trivial.  -/
Mathlib.Tactic.TermCongr.CongrResult.isRfl : Mathlib.Tactic.TermCongr.CongrResult → Bool
-- Mathlib.Topology.UniformSpace.Dini
/-- **Dini's theorem**: if `F n` is a monotone increasing collection of continuous functions on a
compact space converging pointwise to a continuous function `f`, then `F n` converges uniformly to
`f`.  -/
Monotone.tendstoUniformly_of_forall_tendsto : ∀ {ι : Type u_1} {α : Type u_2} {G : Type u_3} [inst : Preorder ι] [inst_1 : TopologicalSpace α]
  [inst_2 : NormedAddCommGroup G] [inst_3 : Lattice G] [HasSolidNorm G] [IsOrderedAddMonoid G] {F : ι → α → G}
  {f : α → G} [CompactSpace α],
  (∀ (i : ι), Continuous (F i)) →
    Monotone F →
      Continuous f →
        (∀ (x : α), Filter.Tendsto (fun x_1 => F x_1 x) Filter.atTop (nhds (f x))) → TendstoUniformly F f Filter.atTop
-- Mathlib.Algebra.Star.CHSH
IsCHSHTuple.A₁_sa : ∀ {R : Type u_1} [inst : Monoid R] [inst_1 : StarMul R] {A₀ A₁ B₀ B₁ : R}, IsCHSHTuple A₀ A₁ B₀ B₁ → star A₁ = A₁
-- Mathlib.Tactic.Push.Attr
/-- The `pull` environment extension  -/
Mathlib.Tactic.Push.pullExt : Lean.SimpleScopedEnvExtension Mathlib.Tactic.Push.PullTheorem (Lean.Meta.DiscrTree Mathlib.Tactic.Push.PullTheorem)
-- Init.Core
/-- `NonScalar` is a type that is not a scalar value in our runtime.
It is used as a stand-in for an arbitrary boxed value to avoid excessive
monomorphization, and it is only created using `unsafeCast`. It is somewhat
analogous to C `void*` in usage, but the type itself is not special.
 -/
NonScalar : Type
-- Lean.MetavarContext
Lean.MetavarContext.MkBindingM.Context.mk.inj : ∀ {quotContext : Lean.Name} {lctx : Lean.LocalContext} {quotContext_1 : Lean.Name} {lctx_1 : Lean.LocalContext},
  { quotContext := quotContext, lctx := lctx } = { quotContext := quotContext_1, lctx := lctx_1 } →
    quotContext = quotContext_1 ∧ lctx = lctx_1
-- Mathlib.Topology.ContinuousOn
ContinuousWithinAt.preimage_mem_nhdsWithin'' : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {x : α} {y : β}
  {s t : Set β}, ContinuousWithinAt f (f ⁻¹' s) x → t ∈ nhdsWithin y s → y = f x → f ⁻¹' t ∈ nhdsWithin x (f ⁻¹' s)
-- Mathlib.Algebra.Polynomial.Bivariate
/-- Evaluating `swap p` at `x`, `y` is the same as evaluating `p` at `y` `x`.  -/
Polynomial.Bivariate.aevalAeval_swap : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Algebra R A] (x y : A)
  (p : Polynomial (Polynomial R)),
  (Polynomial.aevalAeval x y) (Polynomial.Bivariate.swap p) = (Polynomial.aevalAeval y x) p
-- Mathlib.Geometry.Manifold.IsManifold.Basic
modelWithCorners_prod_toPartialEquiv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_4} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {H : Type u_5}
  [inst_5 : TopologicalSpace H] {G : Type u_7} [inst_6 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 F G}, (I.prod J).toPartialEquiv = I.prod J.toPartialEquiv
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Under.opEquivOpOver_functor_obj : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] (X : T) (Y : CategoryTheory.Under (Opposite.op X)),
  (CategoryTheory.Under.opEquivOpOver X).functor.obj Y = Opposite.op (CategoryTheory.Over.mk Y.hom.unop)
-- Mathlib.Combinatorics.SimpleGraph.Copy
SimpleGraph.IsContained.rfl : ∀ {V : Type u_1} {G : SimpleGraph V}, G.IsContained G
-- Mathlib.Algebra.Ring.Rat
Rat.commRing : CommRing ℚ
-- Mathlib.Algebra.Polynomial.Module.Basic
PolynomialModule.comp_smul : ∀ {R : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (p p' : Polynomial R) (q : PolynomialModule R M),
  (PolynomialModule.comp p) (p' • q) = p'.comp p • (PolynomialModule.comp p) q
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.NonUnitalRing.hom_ext : ∀ {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6}
  {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)]
  [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι]
  [inst_4 : (i : ι) → NonUnitalNonAssocSemiring (G i)]
  [inst_5 : ∀ (i j : ι) (h : i ≤ j), NonUnitalRingHomClass (T h) (G i) (G j)] [inst_6 : Nonempty ι] (P : Type u_7)
  [inst_7 : NonUnitalNonAssocSemiring P] {g₁ g₂ : DirectLimit G f →ₙ+* P},
  (∀ (i : ι), g₁.comp (DirectLimit.NonUnitalRing.of G f i) = g₂.comp (DirectLimit.NonUnitalRing.of G f i)) → g₁ = g₂
-- Mathlib.Order.Interval.Set.LinearOrder
Set.compl_Ioi : ∀ {α : Type u_1} [inst : LinearOrder α] {a : α}, (Set.Ioi a)ᶜ = Set.Iic a
-- Init.Data.Vector.Range
Vector.zipIdx_eq_append_iff : ∀ {α : Type u_1} {n m : ℕ} {ys : Vector (α × ℕ) n} {zs : Vector (α × ℕ) m} {xs : Vector α (n + m)} {k : ℕ},
  xs.zipIdx k = ys ++ zs ↔ ∃ ys' zs', xs = ys' ++ zs' ∧ ys = ys'.zipIdx k ∧ zs = zs'.zipIdx (k + n)
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.mapRightIso_inverse_obj_right : ∀ {B : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} B] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T)
  {R₁ R₂ : CategoryTheory.Functor B T} (i : R₁ ≅ R₂) (X : CategoryTheory.Comma L R₂),
  ((CategoryTheory.Comma.mapRightIso L i).inverse.obj X).right = X.right
-- Lean.Data.Lsp.Basic
Lean.Lsp.instFromJsonPartialResultParams.fromJson : Lean.Json → Except String Lean.Lsp.PartialResultParams
-- Mathlib.SetTheory.ZFC.Basic
/-- The binary union operation  -/
ZFSet.union : ZFSet.{u} → ZFSet.{u} → ZFSet.{u}
-- Mathlib.Analysis.Calculus.Taylor
/-- **Taylor's theorem** with the Integral form of the remainder.

We assume that `f` is `n`-times continuously differentiable on the closed set `uIcc x₀ x` and
its `n`-th derivative is absolutely continuous on `uIcc x₀ x`. Then
$$f(x) - (P_n f)(x₀, x) = \int_{x_0}^x \frac{f^{(n+1)}(t) (x - t)^n}{n!} dt,$$
where $P_n f$ denotes the Taylor polynomial of degree $n$ and $f^{(n+1)}$ is the $n+1$-th iterated
derivative.  -/
taylor_integral_remainder_of_absolutelyContinuous : ∀ {f : ℝ → ℝ} {x x₀ : ℝ} {n : ℕ},
  ContDiffOn ℝ (↑n) f (Set.uIcc x₀ x) →
    AbsolutelyContinuousOnInterval (iteratedDerivWithin n f (Set.uIcc x₀ x)) x₀ x →
      f x - taylorWithinEval f n (Set.uIcc x₀ x) x₀ x =
        ∫ (t : ℝ) in x₀..x, (x - t) ^ n / ↑n.factorial * iteratedDerivWithin (n + 1) f (Set.uIcc x₀ x) t
-- Lean.Elab.App
/-- fType may become a forallE after we synthesize pending metavariables.  -/
_private.Lean.Elab.App.0.Lean.Elab.Term.ElabAppArgs.synthesizePendingAndNormalizeFunType : Lean.Elab.Term.ElabAppArgs.M Unit
-- Init.Data.UInt.Lemmas
UInt8.ofNatTruncate_finVal : ∀ (n : Fin UInt8.size), UInt8.ofNatClamp ↑n = UInt8.ofFin n
-- Mathlib.CategoryTheory.Triangulated.Yoneda
CategoryTheory.Pretriangulated.preadditiveCoyoneda_homologySequenceδ_apply : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.HasShift C ℤ] (T : CategoryTheory.Pretriangulated.Triangle C) (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁)
  {A : Cᵒᵖ} (x : Opposite.unop A ⟶ (CategoryTheory.shiftFunctor C n₀).obj T.obj₃),
  (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.preadditiveCoyoneda.obj A).homologySequenceδ T n₀ n₁ h)) x =
    CategoryTheory.CategoryStruct.comp x
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C n₀).map T.mor₃)
        ((CategoryTheory.shiftFunctorAdd' C 1 n₀ n₁ ⋯).inv.app T.obj₁))
-- Mathlib.Topology.Filter
Filter.nhds_pure : ∀ {α : Type u_2} (x : α), nhds (pure x) = Filter.principal {⊥, pure x}
-- Mathlib.Algebra.CharP.CharAndCard
/-- The prime divisors of the characteristic of a finite commutative ring are exactly
the prime divisors of its cardinality.  -/
prime_dvd_char_iff_dvd_card : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : Fintype R] (p : ℕ) [Fact (Nat.Prime p)],
  p ∣ ringChar R ↔ p ∣ Fintype.card R
-- Std.Tactic.BVDecide.LRAT.Internal.Clause
Std.Tactic.BVDecide.LRAT.Internal.Clause.mk : {α : outParam (Type u)} →
  {β : Type v} →
    (toList : β → Std.Sat.CNF.Clause α) →
      (∀ (c : β) (l : Std.Sat.Literal α), l ∉ toList c ∨ l.negate ∉ toList c) →
        (Array (Std.Sat.Literal α) → Option β) →
          (empty : β) →
            toList empty = [] →
              (unit : Std.Sat.Literal α → β) →
                (∀ (l : Std.Sat.Literal α), toList (unit l) = [l]) →
                  (isUnit : β → Option (Std.Sat.Literal α)) →
                    (∀ (c : β) (l : Std.Sat.Literal α), isUnit c = some l ↔ toList c = [l]) →
                      (negate : β → Std.Sat.CNF.Clause α) →
                        (∀ (c : β), negate c = List.map Std.Sat.Literal.negate (toList c)) →
                          (delete : β → Std.Sat.Literal α → β) →
                            (∀ (c : β) (l l' : Std.Sat.Literal α), l' ∈ toList (delete c l) ↔ l' ≠ l ∧ l' ∈ toList c) →
                              (contains : β → Std.Sat.Literal α → Bool) →
                                (∀ (c : β) (l : Std.Sat.Literal α), contains c l = true ↔ l ∈ toList c) →
                                  (β →
                                      Array Std.Tactic.BVDecide.LRAT.Internal.Assignment →
                                        Std.Tactic.BVDecide.LRAT.Internal.ReduceResult α) →
                                    Std.Tactic.BVDecide.LRAT.Internal.Clause α β
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.coeff_smul : ∀ {R : Type u_1} [inst : Semiring R] {S : Type u_2} [inst_1 : Semiring S] [inst_2 : Module R S] (n : ℕ)
  (φ : PowerSeries S) (a : R), (PowerSeries.coeff n) (a • φ) = a • (PowerSeries.coeff n) φ
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
preNormEDS_zero : ∀ {R : Type u_1} [inst : CommRing R] (b c d : R), preNormEDS b c d 0 = 0
-- Mathlib.Algebra.Order.Ring.Canonical
CanonicallyOrderedAdd.toIsOrderedRing : ∀ {R : Type u} [inst : CommSemiring R] [inst_1 : PartialOrder R] [CanonicallyOrderedAdd R], IsOrderedRing R
-- Mathlib.Analysis.InnerProductSpace.Calculus
differentiable_euclidean : ∀ {𝕜 : Type u_1} {ι : Type u_2} {H : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup H]
  [inst_2 : NormedSpace 𝕜 H] {f : H → EuclideanSpace 𝕜 ι} [Finite ι],
  Differentiable 𝕜 f ↔ ∀ (i : ι), Differentiable 𝕜 fun x => (f x).ofLp i
-- Mathlib.Topology.Continuous
DenseRange.exists_mem_open : ∀ {X : Type u_1} [inst : TopologicalSpace X] {α : Type u_4} {f : α → X} {s : Set X},
  DenseRange f → IsOpen s → s.Nonempty → ∃ a, f a ∈ s
-- Mathlib.Data.Set.Image
Set.image_surjective : ∀ {α : Type u} {β : Type v} {f : α → β}, Function.Surjective (Set.image f) ↔ Function.Surjective f
-- Mathlib.CategoryTheory.Sites.Subsheaf
CategoryTheory.Subfunctor.toRangeSheafify.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C)
  {F F' : CategoryTheory.Functor Cᵒᵖ (Type w)} (f : F' ⟶ F),
  CategoryTheory.Subfunctor.toRangeSheafify J f =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Subfunctor.toRange f) (CategoryTheory.Subfunctor.homOfLe ⋯)
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.SInt
Int64.reduceLT : Lean.Meta.Simp.Simproc
-- Mathlib.Geometry.Euclidean.Sphere.Basic
EuclideanGeometry.Sphere.IsDiameter.left_eq_of_isDiameter : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : EuclideanGeometry.Sphere P} {p₁ p₂ p₃ : P},
  s.IsDiameter p₁ p₃ → s.IsDiameter p₂ p₃ → p₁ = p₂
-- Mathlib.Data.Int.Cast.Lemmas
Int.commute_cast : ∀ {α : Type u_3} [inst : NonAssocRing α] (a : α) (n : ℤ), Commute a ↑n