mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKeyD_alter_self : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} [inst_2 : LawfulBEq α]
  [Inhabited α] {k fallback : α} {f : Option (β k) → Option (β k)},
  m.WF → (m.alter k f).getKeyD k fallback = if (f (m.get? k)).isSome = true then k else fallback
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.OplaxMonoidal.δ_comp_tensorHom_η_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.OplaxMonoidal] {X : C} {Y : D} (f : F.obj X ⟶ Y) {Z : D}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj Y (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Functor.OplaxMonoidal.δ F X (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.tensorHom f (CategoryTheory.Functor.OplaxMonoidal.η F)) h) =
    CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor (F.obj X)).inv
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.whiskerRight f (CategoryTheory.MonoidalCategoryStruct.tensorUnit D))
          h))
-- Mathlib.Tactic.ITauto
Mathlib.Tactic.ITauto.instToExprAndKind.toExpr : Mathlib.Tactic.ITauto.AndKind → Lean.Expr
-- Init.Internal.Order.Basic
Lean.Order.ImplicationOrder.instOrder : Lean.Order.PartialOrder Lean.Order.ImplicationOrder
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.const_lintegral_restrict : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (c : ENNReal) (s : Set α),
  (MeasureTheory.SimpleFunc.const α c).lintegral (μ.restrict s) = c * μ s
-- Mathlib.Probability.Martingale.Upcrossing
_private.Mathlib.Probability.Martingale.Upcrossing.0.MeasureTheory.upperCrossingTime.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (n : ℕ) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match n.succ with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_2 n
-- Init.Data.String.Substring
Substring.toString : Substring.Raw → String
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F.unop : C ⥤ D` preserves finite limits, then `F : Cᵒᵖ ⥤ Dᵒᵖ` preserves finite colimits.  -/
CategoryTheory.Limits.preservesFiniteColimits_of_unop : ∀ {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.PreservesFiniteLimits F.unop],
  CategoryTheory.Limits.PreservesFiniteColimits F
-- Mathlib.Analysis.Calculus.Deriv.Inv
Differentiable.div : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {𝕜' : Type u_1} [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {c d : 𝕜 → 𝕜'},
  Differentiable 𝕜 c → Differentiable 𝕜 d → (∀ (x : 𝕜), d x ≠ 0) → Differentiable 𝕜 (c / d)
-- Mathlib.Tactic.Algebraize
Mathlib.Tactic.Algebraize.instInhabitedConfig.default : Mathlib.Tactic.Algebraize.Config
-- Init.Meta.Defs
Lean.Parser.Tactic.mkOptConfig : Lean.TSyntaxArray `Lean.Parser.Tactic.configItem → Lean.TSyntax `Lean.Parser.Tactic.optConfig
-- Mathlib.Data.Matrix.Mul
Matrix.single_vecMul : ∀ {m : Type u_2} {n : Type u_3} {R : Type u_7} [inst : Fintype m] [inst_1 : DecidableEq m]
  [inst_2 : NonUnitalNonAssocSemiring R] (M : Matrix m n R) (i : m) (x : R),
  Matrix.vecMul (Pi.single i x) M = x • M.row i
-- Init.Data.List.MinMax
/-- This lemma is also applicable given the following instances:

```
[LE α] [Min α] [IsLinearOrder α] [LawfulOrderMin α]
```
 -/
List.foldl_min : ∀ {α : Type u_1} [inst : Min α] [Std.IdempotentOp min] [Std.Associative min] {l : List α} {a : α},
  List.foldl min a l = a ⊓ l.min?.getD a
-- Mathlib.GroupTheory.MonoidLocalization.Basic
/-- Copy of `Quotient.recOnSubsingleton₂` for `AddLocalization`  -/
AddLocalization.recOnSubsingleton₂ : {M : Type u_1} →
  [inst : AddCommMonoid M] →
    {S : AddSubmonoid M} →
      {r : AddLocalization S → AddLocalization S → Sort u} →
        [h : ∀ (a c : M) (b d : ↥S), Subsingleton (r (AddLocalization.mk a b) (AddLocalization.mk c d))] →
          (x y : AddLocalization S) →
            ((a c : M) → (b d : ↥S) → r (AddLocalization.mk a b) (AddLocalization.mk c d)) → r x y
-- Mathlib.Analysis.Convex.Gauge
gaugeSeminorm_ball_one : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {s : Set E} [inst_2 : RCLike 𝕜]
  [inst_3 : Module 𝕜 E] [inst_4 : IsScalarTower ℝ 𝕜 E] {hs₀ : Balanced 𝕜 s} {hs₁ : Convex ℝ s} {hs₂ : Absorbent ℝ s}
  [inst_5 : TopologicalSpace E] [ContinuousSMul ℝ E], IsOpen s → (gaugeSeminorm hs₀ hs₁ hs₂).ball 0 1 = s
-- Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
RestrictedProduct.continuousSMul : ∀ {ι : Type u_1} (R : ι → Type u_2) {S : ι → Type u_3} [inst : (i : ι) → SetLike (S i) (R i)] {B : (i : ι) → S i}
  [inst_1 : (i : ι) → TopologicalSpace (R i)] [hBopen : Fact (∀ (i : ι), IsOpen ↑(B i))] {G : Type u_4}
  [inst_2 : TopologicalSpace G] [inst_3 : (i : ι) → SMul G (R i)] [inst_4 : ∀ (i : ι), SMulMemClass (S i) G (R i)]
  [∀ (i : ι), ContinuousSMul G (R i)],
  ContinuousSMul G (RestrictedProduct (fun i => R i) (fun i => ↑(B i)) Filter.cofinite)
-- Std.Data.Iterators.Lemmas.Equivalence.HetT
Std.Internal.ComputableSmall.mk : {α : Type v} →
  (Target : Type u) →
    (deflate : α → Target) →
      (inflate : Target → α) →
        (∀ {a : Target}, deflate (inflate a) = a) →
          (∀ {a : α}, inflate (deflate a) = a) → Std.Internal.ComputableSmall α
-- Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
/-- A class for `𝕜`-algebras with a partial order where the ordering is compatible with the
(quasi)spectrum.  -/
NonnegSpectrumClass : (𝕜 : Type u_3) →
  (A : Type u_4) →
    [inst : CommSemiring 𝕜] → [PartialOrder 𝕜] → [inst_2 : NonUnitalRing A] → [PartialOrder A] → [Module 𝕜 A] → Prop
-- Init.Data.Array.Lemmas
Array.contains_flatten : ∀ {α : Type u_1} [inst : BEq α] {xs : Array (Array α)} {x : α}, xs.flatten.contains x = xs.any fun xs => xs.contains x
-- Mathlib.RingTheory.Congruence.Defs
RingCon.coe_one : ∀ {R : Type u_1} [inst : Add R] [inst_1 : MulOneClass R] (c : RingCon R), ↑1 = 1
-- Init.Grind.ToInt
/-- `ToInt α I` asserts that `α` can be embedded faithfully into an interval `I` in the integers.
 -/
Lean.Grind.ToInt : Type u → outParam Lean.Grind.IntInterval → Type u
-- Std.Data.DHashMap.IteratorLemmas
Std.DHashMap.toListRev_keysIter : ∀ {α : Type u} {β : α → Type u} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap α β} [EquivBEq α]
  [LawfulHashable α], m.keysIter.toListRev = m.keys.reverse
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Fin
Fin.reduceFinMk : Lean.Meta.Simp.DSimproc
-- Lean.Elab.Do.Basic
/-- The identifier of the `let mut` declaration.  -/
Lean.Elab.Do.MutVar.ident : Lean.Elab.Do.MutVar → Lean.Ident
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
CategoryTheory.Limits.pullbackRightPullbackFstIso_hom_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) (f' : W ⟶ X)
  [inst_1 : CategoryTheory.Limits.HasPullback f g]
  [inst_2 : CategoryTheory.Limits.HasPullback f' (CategoryTheory.Limits.pullback.fst f g)],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackRightPullbackFstIso f g f').hom
      (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp f' f) g) =
    CategoryTheory.Limits.pullback.fst f' (CategoryTheory.Limits.pullback.fst f g)
-- Lean.Environment
/-- Updates `env.isExporting`. Ignored if `env.header.isModule` is false.  -/
Lean.Environment.setExporting : Lean.Environment → Bool → Lean.Environment
-- Mathlib.Combinatorics.Matroid.Constructions
Matroid.loopyOn_ground : ∀ {α : Type u_1} (E : Set α), (Matroid.loopyOn E).E = E
-- Mathlib.Order.Interval.Set.Image
Set.preimage_subtype_val_Icc : ∀ {α : Type u_1} [inst : Preorder α] {p : α → Prop} (a b : { x // p x }), Subtype.val ⁻¹' Set.Icc ↑a ↑b = Set.Icc a b
-- Mathlib.NumberTheory.LSeries.Convolution
LSeries.convolution_def : ∀ {R : Type u_1} [inst : Semiring R] (f g : ℕ → R),
  LSeries.convolution f g = fun n => ∑ p ∈ n.divisorsAntidiagonal, f p.1 * g p.2
-- Mathlib.Analysis.Calculus.ImplicitFunction.Bivariate
implicitFunctionOfBivariate_def : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : IsRCLikeNormedField 𝕜] {E₁ : Type u_2}
  [inst_2 : NormedAddCommGroup E₁] [inst_3 : NormedSpace 𝕜 E₁] [inst_4 : CompleteSpace E₁] {E₂ : Type u_3}
  [inst_5 : NormedAddCommGroup E₂] [inst_6 : NormedSpace 𝕜 E₂] [inst_7 : CompleteSpace E₂] {F : Type u_4}
  [inst_8 : NormedAddCommGroup F] [inst_9 : NormedSpace 𝕜 F] [inst_10 : CompleteSpace F] {u : E₁ × E₂} {f : E₁ → E₂ → F}
  {f₁ : E₁ → E₂ → E₁ →L[𝕜] F} {f₂ : E₁ → E₂ → E₂ →L[𝕜] F}
  (df₁ : ∀ᶠ (v : E₁ × E₂) in nhds u, HasFDerivAt (fun x => f x v.2) (f₁ v.1 v.2) v.1)
  (df₂ : ∀ᶠ (v : E₁ × E₂) in nhds u, HasFDerivAt (fun x => f v.1 x) (f₂ v.1 v.2) v.2) (cf₁ : ContinuousAt (↿f₁) u)
  (cf₂ : ContinuousAt (↿f₂) u) (if₂u : (f₂ u.1 u.2).IsInvertible),
  implicitFunctionOfBivariate df₁ df₂ cf₁ cf₂ if₂u = ⋯.implicitFunctionOfProdDomain ⋯
-- Std.Http.Server
Std.Http.Server.mk.sizeOf_spec : ∀ (context : Std.CancellationContext) (activeConnections : Std.Mutex ℕ) (connectionLimit : Option Std.Semaphore)
  (shutdownPromise : Std.Channel Unit) (config : Std.Http.Config) (localAddr : Option Std.Net.SocketAddress),
  sizeOf
      { context := context, activeConnections := activeConnections, connectionLimit := connectionLimit,
        shutdownPromise := shutdownPromise, config := config, localAddr := localAddr } =
    1 + sizeOf context + sizeOf activeConnections + sizeOf connectionLimit + sizeOf shutdownPromise + sizeOf config +
      sizeOf localAddr
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
/-- The chosen wide pullback of `(f₁, f₂, f₃)`.  -/
CategoryTheory.Limits.ChosenPullback₃.pullback : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X₁ X₂ X₃ S : C} →
      {f₁ : X₁ ⟶ S} →
        {f₂ : X₂ ⟶ S} →
          {f₃ : X₃ ⟶ S} →
            {h₁₂ : CategoryTheory.Limits.ChosenPullback f₁ f₂} →
              {h₂₃ : CategoryTheory.Limits.ChosenPullback f₂ f₃} →
                {h₁₃ : CategoryTheory.Limits.ChosenPullback f₁ f₃} →
                  CategoryTheory.Limits.ChosenPullback₃ h₁₂ h₂₃ h₁₃ → C
-- Mathlib.Algebra.Lie.Basic
/-- A module of Lie algebra modules is compatible with the action of the Lie algebra on the
modules.  -/
LieModuleHom.map_lie' : ∀ {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : AddCommGroup M] [inst_3 : AddCommGroup N] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : LieRingModule L M] [inst_7 : LieRingModule L N] (self : M →ₗ⁅R,L⁆ N) {x : L} {m : M},
  (↑self).toFun ⁅x, m⁆ = ⁅x, (↑self).toFun m⁆
-- Mathlib.Analysis.Oscillation
/-- The oscillation of `f : E → F` within `D` at `x`.  -/
oscillationWithin : {E : Type u} → {F : Type v} → [PseudoEMetricSpace F] → [TopologicalSpace E] → (E → F) → Set E → E → ENNReal
-- Mathlib.Analysis.PSeries
Finset.sum_schlomilch_le' : ∀ {M : Type u_1} [inst : AddCommMonoid M] [inst_1 : PartialOrder M] [IsOrderedAddMonoid M] {f : ℕ → M} {u : ℕ → ℕ},
  (∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m) →
    (∀ (n : ℕ), 0 < u n) →
      Monotone u →
        ∀ (n : ℕ), ∑ k ∈ Finset.range n, (u (k + 1) - u k) • f (u (k + 1)) ≤ ∑ k ∈ Finset.Ico (u 0 + 1) (u n + 1), f k
-- Mathlib.Algebra.Regular.Opposite
isLeftRegular_unop : ∀ {R : Type u_1} [inst : Mul R] {a : Rᵐᵒᵖ}, IsLeftRegular (MulOpposite.unop a) ↔ IsRightRegular a
-- Mathlib.Analysis.Calculus.SmoothSeries
/-- Consider a series of functions `∑' n, f n x` on a preconnected open set. If the series converges
at a point, and all functions in the series are differentiable with a summable bound on the
derivatives, then the series converges everywhere on the set.  -/
summable_of_summable_hasFDerivAt_of_isPreconnected : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜]
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedAddCommGroup F] [CompleteSpace F]
  {u : α → ℝ} [inst_6 : NormedSpace 𝕜 F] {f : α → E → F} {f' : α → E → E →L[𝕜] F} {s : Set E} {x₀ x : E},
  Summable u →
    IsOpen s →
      IsPreconnected s →
        (∀ (n : α), ∀ x ∈ s, HasFDerivAt (f n) (f' n x) x) →
          (∀ (n : α), ∀ x ∈ s, ‖f' n x‖ ≤ u n) → x₀ ∈ s → (Summable fun x => f x x₀) → x ∈ s → Summable fun n => f n x
-- Mathlib.Data.Multiset.ZeroCons
Multiset.zero_le : ∀ {α : Type u_1} (s : Multiset α), 0 ≤ s
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict
/-- Given a `NonUnitalContinuousFunctionalCalculus S A q`. If we form the predicate `p` for `a : A`
characterized by: `q a` and the quasispectrum of `a` restricts to the scalar subring `R` via
`f : C(S, R)`, then we can get a restricted functional calculus
`NonUnitalContinuousFunctionalCalculus R A p`.  -/
QuasispectrumRestricts.cfc : ∀ {R : Type u_1} {S : Type u_2} {A : Type u_3} {p q : A → Prop} [inst : Semifield R] [inst_1 : StarRing R]
  [inst_2 : MetricSpace R] [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : Field S]
  [inst_6 : StarRing S] [inst_7 : MetricSpace S] [inst_8 : IsTopologicalRing S] [inst_9 : ContinuousStar S]
  [inst_10 : NonUnitalRing A] [inst_11 : StarRing A] [inst_12 : Module S A] [inst_13 : IsScalarTower S A A]
  [inst_14 : SMulCommClass S A A] [inst_15 : Algebra R S] [inst_16 : Module R A] [IsScalarTower R S A] [StarModule R S]
  [ContinuousSMul R S] [inst_20 : TopologicalSpace A] [NonUnitalContinuousFunctionalCalculus S A q]
  [inst_22 : IsScalarTower R A A] [inst_23 : SMulCommClass R A A] (f : C(S, R)),
  Topology.IsClosedEmbedding ⇑(algebraMap R S) →
    p 0 → (∀ (a : A), p a ↔ q a ∧ QuasispectrumRestricts a ⇑f) → NonUnitalContinuousFunctionalCalculus R A p
-- Mathlib.CategoryTheory.Monoidal.CommGrp_
CategoryTheory.Functor.mapCommpGrp_id_mul : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (A : CategoryTheory.CommGrp C),
  CategoryTheory.MonObj.mul =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj A.X A.X))
      CategoryTheory.MonObj.mul
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.sphere_isEmpty_of_subsingleton : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x : α} {ε : ℝ} [Subsingleton α] [NeZero ε], IsEmpty ↑(Metric.sphere x ε)
-- Mathlib.Topology.Category.Profinite.Nobeling.Successor
Profinite.NobelingProof.mem_C'_eq_false : ∀ {I : Type u} (C : Set (I → Bool)) [inst : LinearOrder I] [inst_1 : WellFoundedLT I] {o : Ordinal.{u}}
  (ho : o < Ordinal.type fun x1 x2 => x1 < x2),
  ∀ x ∈ Profinite.NobelingProof.C' C ho, x (Profinite.NobelingProof.term I ho) = false
-- Mathlib.Analysis.Calculus.DerivativeTest
/-- Suppose `f : ℝ → ℝ` is continuous at `b` and `c`, the derivative `f'` is nonnegative on
`Iio b` and nonpositive on `Ioo b c`. Then `f` attains its maximum on `Iic c` at `b`.  -/
isMaxOn_Iic_of_deriv : ∀ {f : ℝ → ℝ} {b c : ℝ},
  ContinuousAt f b →
    ContinuousAt f c →
      DifferentiableOn ℝ f (Set.Iio b) →
        DifferentiableOn ℝ f (Set.Ioo b c) →
          (∀ x ∈ Set.Iio b, 0 ≤ deriv f x) → (∀ x ∈ Set.Ioo b c, deriv f x ≤ 0) → IsMaxOn f (Set.Iic c) b
-- Mathlib.Logic.Basic
BEx.elim : ∀ {α : Sort u_1} {p : α → Prop} {P : (x : α) → p x → Prop} {b : Prop},
  (∃ x, ∃ (h : p x), P x h) → (∀ (a : α) (h : p a), P a h → b) → b
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Functor.IsEquivalence.essSurj : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} D}
  {F : CategoryTheory.Functor C D} [self : F.IsEquivalence], F.EssSurj
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.CliqueFree.eq_1 : ∀ {α : Type u_1} (G : SimpleGraph α) (n : ℕ), G.CliqueFree n = ∀ (t : Finset α), ¬G.IsNClique n t
-- Init.Sym.DSimp.DSimprocDSL
/-- Do nothing  -/
Lean.Parser.Sym.DSimp.none : Lean.ParserDescr
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.isoCyclesOfIsLimit_inv_ι : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasLeftHomology] {kf : CategoryTheory.Limits.KernelFork S.g}
  (hkf : CategoryTheory.Limits.IsLimit kf),
  CategoryTheory.CategoryStruct.comp (S.isoCyclesOfIsLimit hkf).inv (CategoryTheory.Limits.Fork.ι kf) = S.iCycles
-- Mathlib.Analysis.Calculus.FDeriv.Add
Differentiable.fun_sum : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {ι : Type u_4}
  {u : Finset ι} {A : ι → E → F}, (∀ i ∈ u, Differentiable 𝕜 (A i)) → Differentiable 𝕜 fun y => ∑ i ∈ u, A i y
-- Init.Data.List.ToArray
Array.forIn'.eq_1 : ∀ {α : Type u} {β : Type v} {m : Type v → Type w} [inst : Monad m] (as : Array α) (b : β)
  (f : (a : α) → a ∈ as → β → m (ForInStep β)), as.forIn' b f = Array.forIn'.loop as f as.size ⋯ b
-- Mathlib.Topology.UniformSpace.Separation
SeparationQuotient.map_unique : ∀ {α : Type u} {β : Type v} [inst : UniformSpace α] [inst_1 : UniformSpace β] {f : α → β},
  UniformContinuous f →
    ∀ {g : SeparationQuotient α → SeparationQuotient β},
      SeparationQuotient.mk ∘ f = g ∘ SeparationQuotient.mk → SeparationQuotient.map f = g
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.Poly.combine.match_1.congr_eq_1 : ∀ (motive : Lean.Grind.Linarith.Poly → Lean.Grind.Linarith.Poly → Sort u_1) (p₁ p₂ : Lean.Grind.Linarith.Poly)
  (h_1 : (p₂ : Lean.Grind.Linarith.Poly) → motive Lean.Grind.Linarith.Poly.nil p₂)
  (h_2 : (p₁ : Lean.Grind.Linarith.Poly) → motive p₁ Lean.Grind.Linarith.Poly.nil)
  (h_3 :
    (a₁ : ℤ) →
      (x₁ : Lean.Grind.Linarith.Var) →
        (p₁ : Lean.Grind.Linarith.Poly) →
          (a₂ : ℤ) →
            (x₂ : Lean.Grind.Linarith.Var) →
              (p₂ : Lean.Grind.Linarith.Poly) →
                motive (Lean.Grind.Linarith.Poly.add a₁ x₁ p₁) (Lean.Grind.Linarith.Poly.add a₂ x₂ p₂))
  (p₂_1 : Lean.Grind.Linarith.Poly),
  p₁ = Lean.Grind.Linarith.Poly.nil →
    p₂ = p₂_1 →
      (match p₁, p₂ with
        | Lean.Grind.Linarith.Poly.nil, p₂ => h_1 p₂
        | p₁, Lean.Grind.Linarith.Poly.nil => h_2 p₁
        | Lean.Grind.Linarith.Poly.add a₁ x₁ p₁, Lean.Grind.Linarith.Poly.add a₂ x₂ p₂ => h_3 a₁ x₁ p₁ a₂ x₂ p₂) ≍
        h_1 p₂_1
-- Mathlib.Algebra.Star.SelfAdjoint
selfAdjoint.isStarNormal : ∀ {R : Type u_1} [inst : NonUnitalRing R] [inst_1 : StarRing R] (x : ↥(selfAdjoint R)), IsStarNormal ↑x
-- Mathlib.Order.BooleanAlgebra.Basic
inf_inf_sdiff : ∀ {α : Type u} [inst : GeneralizedBooleanAlgebra α] (x y : α), x ⊓ y ⊓ x \ y = ⊥
-- Mathlib.Dynamics.PeriodicPts.Defs
Function.IsPeriodicPt.apply : ∀ {α : Type u_1} {f : α → α} {x : α} {n : ℕ}, Function.IsPeriodicPt f n x → Function.IsPeriodicPt f n (f x)
-- Mathlib.Topology.LocallyConstant.Algebra
/-- `LocallyConstant.const` as an `AlgHom`  -/
LocallyConstant.constₐ : {X : Type u_1} →
  {Y : Type u_2} →
    [inst : TopologicalSpace X] →
      (R : Type u_6) →
        [inst_1 : CommSemiring R] → [inst_2 : Semiring Y] → [inst_3 : Algebra R Y] → Y →ₐ[R] LocallyConstant X Y
-- Init.NotationExtra
unexpandListCons : Lean.PrettyPrinter.Unexpander
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Append
Std.Tactic.BVDecide.BVExpr.bitblast.AppendTarget.h : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {aig : Std.Sat.AIG α} {combined : ℕ}
  (self : Std.Tactic.BVDecide.BVExpr.bitblast.AppendTarget aig combined), combined = self.rw + self.lw
-- Mathlib.Analysis.Calculus.FDeriv.Analytic
ContinuousMultilinearMap.toFormalMultilinearSeries.congr_simp : ∀ {𝕜 : Type u} {F : Type w} [inst : Semiring 𝕜] [inst_1 : AddCommMonoid F] [inst_2 : Module 𝕜 F]
  [inst_3 : TopologicalSpace F] [inst_4 : ContinuousAdd F] [inst_5 : ContinuousConstSMul 𝕜 F] {ι : Type u_1}
  {E : ι → Type u_2} [inst_6 : (i : ι) → AddCommGroup (E i)] [inst_7 : (i : ι) → Module 𝕜 (E i)]
  [inst_8 : (i : ι) → TopologicalSpace (E i)] [inst_9 : ∀ (i : ι), IsTopologicalAddGroup (E i)]
  [inst_10 : ∀ (i : ι), ContinuousConstSMul 𝕜 (E i)] [inst_11 : Fintype ι] (f f_1 : ContinuousMultilinearMap 𝕜 E F),
  f = f_1 → ∀ (n : ℕ), f.toFormalMultilinearSeries n = f_1.toFormalMultilinearSeries n
-- Mathlib.MeasureTheory.Integral.DivergenceTheorem
/-- **Fundamental theorem of calculus, part 2**. This version assumes that `f` is continuous on the
interval and is differentiable off a countable set `s`.

See also

* `intervalIntegral.integral_eq_sub_of_hasDeriv_right_of_le` for a version that only assumes right
  differentiability of `f`;
* `MeasureTheory.integral_eq_of_hasDerivWithinAt_off_countable` for a version that works both
  for `a ≤ b` and `b ≤ a` at the expense of using unordered intervals instead of `Set.Icc`.  -/
MeasureTheory.integral_eq_of_hasDerivAt_off_countable_of_le : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] (f f' : ℝ → E) {a b : ℝ},
  a ≤ b →
    ∀ {s : Set ℝ},
      s.Countable →
        ContinuousOn f (Set.Icc a b) →
          (∀ x ∈ Set.Ioo a b \ s, HasDerivAt f (f' x) x) →
            IntervalIntegrable f' MeasureTheory.volume a b → ∫ (x : ℝ) in a..b, f' x = f b - f a
-- Mathlib.Order.Filter.AtTopBot.Monoid
Filter.Tendsto.atBot_of_isBoundedUnder_ge_add : ∀ {α : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] [inst_1 : Preorder M] [IsOrderedCancelAddMonoid M]
  {l : Filter α} {f g : α → M},
  Filter.IsBoundedUnder (fun x1 x2 => x1 ≥ x2) l f →
    Filter.Tendsto (fun x => f x + g x) l Filter.atBot → Filter.Tendsto g l Filter.atBot
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.mem_carrier_iff_of_mem : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] {𝒜 : ℕ → σ}
  [inst_3 : GradedRing 𝒜] {f : A} {m : ℕ} (f_deg : f ∈ 𝒜 m),
  0 < m →
    ∀
      (q :
        ↑↑(AlgebraicGeometry.Spec.locallyRingedSpaceObj
                (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f))).toPresheafedSpace)
      (a : A) {n : ℕ} (hn : a ∈ 𝒜 n),
      a ∈ AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier f_deg q ↔
        HomogeneousLocalization.mk { deg := m * n, num := ⟨a ^ m, ⋯⟩, den := ⟨f ^ n, ⋯⟩, den_mem := ⋯ } ∈ q.asIdeal
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
/-- Let `l'` be a measurably generated filter; let `l` be a of filter such that each `s ∈ l'`
eventually includes `Ioc u v` as both `u` and `v` tend to `l`. Let `μ` be a measure finite at `l'`.

Suppose that `f : ℝ → E` has a finite limit at `l`. Then `f` is interval integrable on `u..v`
provided that both `u` and `v` tend to `l`.

Typeclass instances allow Lean to find `l'` based on `l` but not vice versa, so
`apply Tendsto.eventually_intervalIntegrable` will generate goals `Filter ℝ` and
`TendstoIxxClass Ioc ?m_1 l'`.  -/
Filter.Tendsto.eventually_intervalIntegrable : ∀ {ι : Type u_1} {E : Type u_5} [inst : NormedAddCommGroup E] {f : ℝ → E} {μ : MeasureTheory.Measure ℝ}
  {l l' : Filter ℝ},
  StronglyMeasurableAtFilter f l' μ →
    ∀ [Filter.TendstoIxxClass Set.Ioc l l'] [l'.IsMeasurablyGenerated],
      μ.FiniteAtFilter l' →
        ∀ {c : E},
          Filter.Tendsto f l' (nhds c) →
            ∀ {u v : ι → ℝ} {lt : Filter ι},
              Filter.Tendsto u lt l → Filter.Tendsto v lt l → ∀ᶠ (t : ι) in lt, IntervalIntegrable f μ (u t) (v t)
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
ContinuousInf.measurableInf : ∀ {γ : Type u_3} [inst : TopologicalSpace γ] {mγ : MeasurableSpace γ} [BorelSpace γ] [inst_2 : Min γ] [ContinuousInf γ],
  MeasurableInf γ
-- Std.Time.Notation
_private.Std.Time.Notation.0.Std.Time.convertOffsetZ : Std.Time.OffsetZ → Lean.MacroM (Lean.TSyntax `term)