mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Probability.Martingale.OptionalSampling
/-- If `τ` and `σ` are two stopping times with `σ ≤ τ` and `τ` is bounded, then the value of a
martingale `f` at `σ` is the conditional expectation of its value at `τ` with respect to the
σ-algebra generated by `σ`.  -/
MeasureTheory.Martingale.stoppedValue_ae_eq_condExp_of_le_of_countable_range : ∀ {Ω : Type u_1} {E : Type u_2} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {ι : Type u_3} [inst_3 : LinearOrder ι] [inst_4 : TopologicalSpace ι]
  [OrderTopology ι] [FirstCountableTopology ι] {ℱ : MeasureTheory.Filtration ι m}
  [MeasureTheory.SigmaFiniteFiltration μ ℱ] {τ σ : Ω → WithTop ι} {f : ι → Ω → E} {n : ι} [inst_8 : Nonempty ι],
  MeasureTheory.Martingale f ℱ μ →
    MeasureTheory.IsStoppingTime ℱ τ →
      ∀ (hσ : MeasureTheory.IsStoppingTime ℱ σ) (hσ_le_τ : σ ≤ τ) (hτ_le : ∀ (x : Ω), τ x ≤ ↑n),
        (Set.range τ).Countable →
          (Set.range σ).Countable →
            ∀ [MeasureTheory.SigmaFinite (μ.trim ⋯)],
              MeasureTheory.stoppedValue f σ =ᵐ[μ] μ[MeasureTheory.stoppedValue f τ | hσ.measurableSpace]
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.Formatter : Type
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.uniformContinuous_iff : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {f : α → β},
  UniformContinuous f ↔ ∀ ε > 0, ∃ δ > 0, ∀ ⦃a b : α⦄, dist a b < δ → dist (f a) (f b) < ε
-- Init.Data.Bool
Bool.cond_pos : ∀ {α : Sort u_1} {b : Bool} {a a' : α}, b = true → (bif b then a else a') = a
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.singleton_I₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S T : C} (f : S ⟶ T),
  (CategoryTheory.PreZeroHypercover.singleton f).I₀ = PUnit.{w + 1}
-- Mathlib.RingTheory.Derivation.Lie
Derivation.Compatible.apply : ∀ {R : Type u_1} [inst : CommRing R] {A : Type u_2} [inst_1 : CommRing A] [inst_2 : Algebra R A] {A' : Type u_3}
  [inst_3 : CommRing A'] [inst_4 : Algebra R A'] [inst_5 : Algebra A A'] [inst_6 : IsScalarTower R A A']
  (x : ↥(Derivation.couple R A A')) (a : A), (↑x).1 ((Algebra.ofId A A') a) = (Algebra.ofId A A') ((↑x).2 a)
-- Mathlib.NumberTheory.SmoothNumbers
/-- Zero is never a smooth number  -/
Nat.ne_zero_of_mem_smoothNumbers : ∀ {n m : ℕ}, m ∈ n.smoothNumbers → m ≠ 0
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
cbiSup_id : ∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {s : Set α}, BddAbove s → sSup ∅ ≤ sSup s → ⨆ i ∈ s, i = sSup s
-- Mathlib.Order.Filter.Map
Filter.EventuallyEq.comp_comap : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {F : Filter β} {f g : β → γ} (h : α → β),
  f =ᶠ[F] g → f ∘ h =ᶠ[Filter.comap h F] g ∘ h
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
CategoryTheory.Limits.instHasLimitCompOfPreservesLimit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] {K : CategoryTheory.Functor J C}
  [CategoryTheory.Limits.HasLimit K] {F : CategoryTheory.Functor C D} [CategoryTheory.Limits.PreservesLimit K F],
  CategoryTheory.Limits.HasLimit (K.comp F)
-- Init.Data.Order.Classes
Std.LawfulOrderMin.toLawfulOrderInf : ∀ {α : Type u} {inst : Min α} {inst_1 : LE α} [self : Std.LawfulOrderMin α], Std.LawfulOrderInf α
-- Mathlib.Analysis.Normed.Group.Continuity
NormedAddCommGroup.toENormedAddCommMonoid.eq_1 : ∀ {E : Type u_4} [inst : NormedAddCommGroup E],
  NormedAddCommGroup.toENormedAddCommMonoid =
    { toESeminormedAddMonoid := NormedAddGroup.toENormedAddMonoid.toESeminormedAddMonoid, add_comm := ⋯,
      enorm_eq_zero := ⋯ }
-- Init.Data.Array.Subarray
_private.Init.Data.Array.Subarray.0.Subarray.findSomeRevM?.find : {α : Type u} →
  {β : Type v} →
    {m : Type v → Type w} →
      [Monad m] → (as : Subarray α) → (α → m (Option β)) → (i : ℕ) → i ≤ Std.Slice.size as → m (Option β)
-- Init.Data.UInt.Basic
/-- Multiplies two 8-bit unsigned integers, wrapping around on overflow.  Usually accessed via the `*`
operator.

This function is overridden at runtime with an efficient implementation.
 -/
UInt8.mul : UInt8 → UInt8 → UInt8
-- Mathlib.Data.List.Basic
List.filter_true : ∀ {α : Type u} (l : List α), List.filter (fun x => true) l = l
-- Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda
CategoryTheory.IsGrothendieckAbelian.IsPresentable.surjectivity : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [CategoryTheory.IsGrothendieckAbelian.{w, v, u} C] {X : C} {J : Type w} [inst_3 : CategoryTheory.SmallCategory J]
  {Y : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cocone Y} (hc : CategoryTheory.Limits.IsColimit c)
  [∀ (j j' : J) (φ : j ⟶ j'), CategoryTheory.Mono (Y.map φ)] {κ : Cardinal.{w}} [hκ : Fact κ.IsRegular]
  [CategoryTheory.IsCardinalFiltered J κ],
  HasCardinalLT (CategoryTheory.Subobject X) κ →
    ∀ (z : X ⟶ c.pt), ∃ j₀ y, z = CategoryTheory.CategoryStruct.comp y (c.ι.app j₀)
-- Mathlib.Order.Fin.Tuple
finSuccAboveOrderIso_symm_apply_ne_last : ∀ {n : ℕ} {p : Fin (n + 1)} (h : p ≠ Fin.last n) (x : { x // x ≠ p }),
  (finSuccAboveEquiv p).symm x = (p.castLT ⋯).predAbove ↑x
-- Init.Data.BitVec.Bitblast
_private.Init.Data.BitVec.Bitblast.0.BitVec.testBit_limit : ∀ {x i : ℕ}, x < 2 ^ (i + 1) → x.testBit i = decide (x ≥ 2 ^ i)
-- Mathlib.Data.Fintype.Card
Fintype.card_le_of_surjective : ∀ {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst_1 : Fintype β] (f : α → β),
  Function.Surjective f → Fintype.card β ≤ Fintype.card α
-- Mathlib.Algebra.Group.Units.Basic
IsUnit.one_div_mul_cancel : ∀ {α : Type u} [inst : DivisionMonoid α] {a : α}, IsUnit a → 1 / a * a = 1
-- Init.Data.Array.Basic
_private.Init.Data.Array.Basic.0.Array.mapFinIdxMUnsafe.map : {α : Type u} →
  {β : Type v} →
    {m : Type v → Type w} →
      [Monad m] →
        (as : Array α) → ((i : ℕ) → α → i < as.size → m β) → USize → USize → Array NonScalar → m (Array PNonScalar)
-- Mathlib.CategoryTheory.Monad.Limits
/-- (Impl) Construct the lifted cone in `Algebra T` which will be limiting.  -/
CategoryTheory.Monad.ForgetCreatesLimits.liftedCone : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {T : CategoryTheory.Monad C} →
      {J : Type u} →
        [inst_1 : CategoryTheory.Category.{v, u} J] →
          (D : CategoryTheory.Functor J T.Algebra) →
            (c : CategoryTheory.Limits.Cone (D.comp T.forget)) →
              CategoryTheory.Limits.IsLimit c → CategoryTheory.Limits.Cone D
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rii.toList.congr_simp : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.PRange.Least? α] (r r_1 : Std.Rii α),
  r = r_1 →
    ∀ [inst_2 : Std.Iterator (Std.Rxi.Iterator α) Id α] [inst_3 : Std.Iterators.Finite (Std.Rxi.Iterator α) Id],
      r.toList = r_1.toList
-- Mathlib.Algebra.Category.ModuleCat.Basic
ModuleCat.hom_comp : ∀ {R : Type u} [inst : Ring R] {M N O : ModuleCat R} (f : M ⟶ N) (g : N ⟶ O),
  ModuleCat.Hom.hom (CategoryTheory.CategoryStruct.comp f g) = ModuleCat.Hom.hom g ∘ₗ ModuleCat.Hom.hom f
-- Init.Data.Array.Lemmas
/-- Variant of `foldlM_push` with a side condition for the `stop` argument.  -/
Array.foldlM_push' : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [LawfulMonad m] {xs : Array α} {a : α}
  {f : β → α → m β} {b : β} {stop : ℕ},
  stop = xs.size + 1 →
    Array.foldlM f b (xs.push a) 0 stop = do
      let b ← Array.foldlM f b xs
      f b a
-- Mathlib.Topology.Homotopy.Product
/-- Abbreviation for projection onto the left coordinate of a path class.  -/
Path.Homotopic.projLeft : {α : Type u_1} →
  {β : Type u_2} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] →
        {c₁ c₂ : α × β} → Path.Homotopic.Quotient c₁ c₂ → Path.Homotopic.Quotient c₁.1 c₂.1
-- Mathlib.Data.Fin.Tuple.Basic
/-- Appending a one-tuple to the left is the same as `Fin.cons`.  -/
Fin.append_left_eq_cons : ∀ {α : Sort u_1} {n : ℕ} (x₀ : Fin 1 → α) (x : Fin n → α), Fin.append x₀ x = Fin.cons (x₀ 0) x ∘ Fin.cast ⋯
-- Mathlib.Data.Part
Part.bind_dom : ∀ {α : Type u_1} {β : Type u_2} {f : Part α} {g : α → Part β}, (f.bind g).Dom ↔ ∃ (h : f.Dom), (g (f.get h)).Dom
-- Mathlib.NumberTheory.NumberField.FractionalIdeal
/-- The absolute value of the determinant of the base change from `integralBasis` to
`basisOfFractionalIdeal I` is equal to the norm of `I`.  -/
NumberField.det_basisOfFractionalIdeal_eq_absNorm : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K]
  (I : (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K)ˣ)
  (e : Module.Free.ChooseBasisIndex ℤ (NumberField.RingOfIntegers K) ≃ Module.Free.ChooseBasisIndex ℤ ↥↑↑I),
  |(NumberField.integralBasis K).det ⇑((NumberField.basisOfFractionalIdeal K I).reindex e.symm)| =
    FractionalIdeal.absNorm ↑I
-- Init.Data.BitVec.Decidable
/-- For small numerals this isn't necessary (as typeclass search can use the above two instances),
but for large numerals this provides a shortcut.
Note, however, that for large numerals the decision procedure may be very slow.
 -/
BitVec.instDecidableExistsBitVec : (n : ℕ) → (P : BitVec n → Prop) → [DecidablePred P] → Decidable (∃ v, P v)
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- Twice the angle between the negation of a vector and that vector is 0.  -/
Orientation.two_zsmul_oangle_neg_self_left : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) (x : V), 2 • o.oangle (-x) x = 0
-- Init.Data.Int.Linear
Int.Internal.Linear.cooper_dvd_left_split : Int.Internal.Linear.Context →
  Int.Internal.Linear.Poly → Int.Internal.Linear.Poly → Int.Internal.Linear.Poly → ℤ → ℕ → Prop
-- Std.Time.Internal.Bounded
Std.Time.Internal.Bounded.LE.instInhabitedHAddIntCast : {lo : ℤ} → {k : ℕ} → Inhabited (Std.Time.Internal.Bounded.LE lo (lo + ↑k))
-- Lean.Elab.PreDefinition.WF.GuessLex
/-- For `#[x₁, .., xₙ]` create `(x₁, .., xₙ)`.
 -/
Lean.Elab.WF.GuessLex.mkProdElem : Array Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.CategoryTheory.SmallObject.Iteration.Basic
CategoryTheory.SmallObject.SuccStruct.Iteration.subsingleton : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} {Φ : CategoryTheory.SmallObject.SuccStruct C}
  [inst_1 : LinearOrder J] [inst_2 : SuccOrder J] [inst_3 : OrderBot J]
  [inst_4 : CategoryTheory.Limits.HasIterationOfShape J C] [inst_5 : WellFoundedLT J] {j : J},
  Subsingleton (Φ.Iteration j)
-- Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
SimplexCategory.δ₀Iter_σ₀Iter_assoc : ∀ (i : ℕ) {n m : ℕ} (hi : autoParam (n + i = m) SimplexCategory.δ₀Iter_σ₀Iter._auto_1) {Z : SimplexCategory}
  (h : { len := n } ⟶ Z),
  CategoryTheory.CategoryStruct.comp (SimplexCategory.δ₀Iter i hi)
      (CategoryTheory.CategoryStruct.comp (SimplexCategory.σ₀Iter i hi) h) =
    h
-- Mathlib.Algebra.Free
/-- If `α` is a type, then `FreeAddSemigroup α` is the free additive semigroup generated by `α`.
This is an additive semigroup equipped with a function
`FreeAddSemigroup.of : α → FreeAddSemigroup α` which has the following universal property:
if `M` is any additive semigroup, and `f : α → M` is any function,
then this function is the composite of `FreeAddSemigroup.of` and a unique semigroup homomorphism
`FreeAddSemigroup.lift f : FreeAddSemigroup α →ₙ+ M`.

A typical element of `FreeAddSemigroup α` is a nonempty formal sum of elements of `α`.
For example if `x` and `y` are terms of type `α` then `x + y + y + x` is a
"typical" element of `FreeAddSemigroup α`. In particular if `α` is empty
then `FreeAddSemigroup α` is also empty, and if `α` has one term
then `FreeAddSemigroup α` is isomorphic to `ℕ+`.
If `α` has two or more terms then `FreeAddSemigroup α` is not commutative.
One can think of `FreeAddSemigroup α` as the type of nonempty lists of `α`, with addition
given by concatenation.
 -/
FreeAddSemigroup : Type u → Type u
-- Mathlib.Analysis.Convex.Between
mem_vsub_const_affineSegment : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] {x y z : P} (p : P),
  z -ᵥ p ∈ affineSegment R (x -ᵥ p) (y -ᵥ p) ↔ z ∈ affineSegment R x y
-- Init.Data.Fin.Lemmas
Fin.castLE_of_eq : ∀ {m n : ℕ} (h : m = n) {h' : m ≤ n}, Fin.castLE h' = Fin.cast h
-- Mathlib.MeasureTheory.Measure.Prod
MeasureTheory.Measure.fst.instIsFiniteMeasure : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  {ρ : MeasureTheory.Measure (α × β)} [MeasureTheory.IsFiniteMeasure ρ], MeasureTheory.IsFiniteMeasure ρ.fst
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.AddModObj.add_vadd_self_flip : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {M : C}
  [inst_2 : CategoryTheory.AddMonObj M] (X : C) [inst_3 : CategoryTheory.AddModObj M X],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M CategoryTheory.AddModObj.vadd)
      CategoryTheory.AddModObj.vadd =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator M M X).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.AddMonObj.add X)
        CategoryTheory.AddModObj.vadd)
-- Mathlib.Order.Concept
/-- The `extentClosure` of a set is the smallest extent containing it. See
`IsExtent.lowerPolar_upperPolar_subset` for this proof.  -/
extentClosure : {α : Type u_2} → {β : Type u_3} → (α → β → Prop) → ClosureOperator (Set α)
-- Lean.Data.JsonRpc
Lean.JsonRpc.Response.mk.inj : ∀ {α : Type u} {id : Lean.JsonRpc.RequestID} {result : α} {id_1 : Lean.JsonRpc.RequestID} {result_1 : α},
  { id := id, result := result } = { id := id_1, result := result_1 } → id = id_1 ∧ result = result_1
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
CStarAlgebra.nnnorm_le_nnnorm_of_nonneg_of_le : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] [StarOrderedRing A] {a b : A},
  autoParam (0 ≤ a) CStarAlgebra.nnnorm_le_nnnorm_of_nonneg_of_le._auto_1 → a ≤ b → ‖a‖₊ ≤ ‖b‖₊
-- Mathlib.Order.RelClasses
instIsPartialOrderGe : ∀ {α : Type u} [inst : PartialOrder α], IsPartialOrder α fun x1 x2 => x2 ≤ x1
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.drop_add_heq : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) (n m : ℕ), p.drop (n + m) ≍ (p.drop n).drop m
-- Mathlib.Combinatorics.Graph.Basic
Graph.IsLink.of_compatible : ∀ {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G H : Graph α β},
  G.Compatible H → e ∈ H.edgeSet → G.IsLink e x y → H.IsLink e x y
-- Mathlib.RingTheory.IsTensorProduct
/-- A type-class stating that the following diagram of scalar towers
```
R  →  S
↓     ↓
R' →  S'
```
is a pushout diagram (i.e. `S' = S ⊗[R] R'`)
 -/
Algebra.IsPushout : (R : Type u_1) →
  (S : Type v₃) →
    [inst : CommSemiring R] →
      [inst_1 : CommSemiring S] →
        [inst_2 : Algebra R S] →
          (R' : Type u_6) →
            (S' : Type u_7) →
              [inst_3 : CommSemiring R'] →
                [inst_4 : CommSemiring S'] →
                  [inst_5 : Algebra R R'] →
                    [inst_6 : Algebra S S'] →
                      [inst_7 : Algebra R' S'] →
                        [inst_8 : Algebra R S'] → [IsScalarTower R R' S'] → [IsScalarTower R S S'] → Prop
-- Mathlib.CategoryTheory.WithTerminal.Cone
/-- This is the inverse of the previous construction: a cone of an extended functor
`liftFromOver.obj K : WithTerminal J ⥤ C` consists of an object of `C`, together
with morphisms. This same object is a cone of the original functor `K : J ⥤ Over X`.  -/
_private.Mathlib.CategoryTheory.WithTerminal.Cone.0.CategoryTheory.WithTerminal.coneBack : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : Type w} →
      [inst_1 : CategoryTheory.Category.{w', w} J] →
        {X : C} →
          {K : CategoryTheory.Functor J (CategoryTheory.Over X)} →
            CategoryTheory.Functor (CategoryTheory.Limits.Cone (CategoryTheory.WithTerminal.liftFromOver.obj K))
              (CategoryTheory.Limits.Cone K)
-- Mathlib.Topology.Algebra.Module.PerfectPairing
LinearMap.toContPerfPair_apply : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommRing R] [inst_1 : TopologicalSpace R]
  [inst_2 : AddCommGroup M] [inst_3 : Module R M] [inst_4 : TopologicalSpace M] [inst_5 : AddCommGroup N]
  [inst_6 : Module R N] [inst_7 : TopologicalSpace N] (p : M →ₗ[R] N →ₗ[R] R) [inst_8 : p.IsContPerfPair]
  [inst_9 : IsTopologicalRing R] (x : M) (y : N), (p.toContPerfPair x) y = (p x) y
-- Std.Data.Internal.List.Associative
Std.Internal.List.perm_filter_key_self_iff_forall_containsKey : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {f : α → Bool} {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ((List.filter (fun p => f p.fst) l).Perm l ↔
      ∀ (a : α) (h : Std.Internal.List.containsKey a l = true), f (Std.Internal.List.getKey a l h) = true)
-- Mathlib.Tactic.Positivity.Core
/-- The main entry point to the `positivity` tactic. Given a goal `goal` of the form `0 [≤/</≠] e`,
attempts to recurse on the structure of `e` to prove the goal.
It will either close `goal` or fail.  -/
Mathlib.Meta.Positivity.positivity : Lean.MVarId → Lean.MetaM Unit
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.prod_union_inter : ∀ {ι : Type u_1} {M : Type u_4} {s₁ s₂ : Finset ι} [inst : CommMonoid M] {f : ι → M} [inst_1 : DecidableEq ι],
  (∏ x ∈ s₁ ∪ s₂, f x) * ∏ x ∈ s₁ ∩ s₂, f x = (∏ x ∈ s₁, f x) * ∏ x ∈ s₂, f x
-- Init.Data.Array.Range
Array.find?_range'_eq_none : ∀ {s n : ℕ} {p : ℕ → Bool}, Array.find? p (Array.range' s n) = none ↔ ∀ (i : ℕ), s ≤ i → i < s + n → (!p i) = true
-- Mathlib.Algebra.Group.Subsemigroup.MulOpposite
AddSubsemigroup.op_unop : ∀ {M : Type u_2} [inst : Add M] (S : AddSubsemigroup Mᵃᵒᵖ), S.unop.op = S
-- Mathlib.RingTheory.Extension.Basic
Algebra.Extension.Hom.id_toRingHom : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : Algebra.Extension R S), (Algebra.Extension.Hom.id P).toRingHom = RingHom.id P.Ring
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.mapRightComp.congr_simp : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  (L : CategoryTheory.Functor A T) {P : CategoryTheory.MorphismProperty T} {Q : CategoryTheory.MorphismProperty A}
  {W : CategoryTheory.MorphismProperty B} [inst_3 : Q.IsMultiplicative] [inst_4 : W.IsMultiplicative]
  {R₁ R₂ R₃ : CategoryTheory.Functor B T} [inst_5 : Q.RespectsIso] [inst_6 : W.RespectsIso] (r : R₁ ⟶ R₂) (r' : R₂ ⟶ R₃)
  (hr :
    ∀ (X : CategoryTheory.MorphismProperty.Comma L R₁ P Q W),
      P (CategoryTheory.CategoryStruct.comp X.hom (r.app X.right)))
  (hr' :
    ∀ (X : CategoryTheory.MorphismProperty.Comma L R₂ P Q W),
      P (CategoryTheory.CategoryStruct.comp X.hom (r'.app X.right)))
  (hrr' :
    ∀ (X : CategoryTheory.MorphismProperty.Comma L R₁ P Q W),
      P (CategoryTheory.CategoryStruct.comp X.hom ((CategoryTheory.CategoryStruct.comp r r').app X.right))),
  CategoryTheory.MorphismProperty.Comma.mapRightComp L r r' hr hr' hrr' =
    CategoryTheory.MorphismProperty.Comma.mapRightComp L r r' hr hr' hrr'
-- Mathlib.LinearAlgebra.Finsupp.VectorSpace
Module.Free.trans : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S]
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module S M] [IsScalarTower R S M] [Module.Free S M]
  [Module.Free R S], Module.Free R M
-- Mathlib.Topology.AlexandrovDiscrete
AlexandrovDiscrete.toLocallyCompactSpace : ∀ {α : Type u_3} [inst : TopologicalSpace α] [AlexandrovDiscrete α], LocallyCompactSpace α
-- Mathlib.Tactic.Abel
Mathlib.Tactic.Abel.term_smulg : ∀ {α : Type u_1} [inst : AddCommGroup α] (c n : ℤ) (x a : α) (n' : ℤ) (a' : α),
  c * n = n' →
    Mathlib.Tactic.Abel.smulg c a = a' →
      Mathlib.Tactic.Abel.smulg c (Mathlib.Tactic.Abel.termg n x a) = Mathlib.Tactic.Abel.termg n' x a'
-- Mathlib.CategoryTheory.MorphismProperty.Comma
/-- The forgetful functor from the full subcategory of `Over X` defined by `P` to `Over X`.  -/
CategoryTheory.MorphismProperty.Over.forget : {T : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} T] →
    (P Q : CategoryTheory.MorphismProperty T) →
      (X : T) → [inst_1 : Q.IsMultiplicative] → CategoryTheory.Functor (P.Over Q X) (CategoryTheory.Over X)
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap.0.Std.IterM.length_eq_match_step.match_1.splitter : {α β : Type u_1} →
  {m : Type u_1 → Type u_2} →
    (motive : Std.IterStep (Std.IterM m β) β → Sort u_3) →
      (x : Std.IterStep (Std.IterM m β) β) →
        ((it' : Std.IterM m β) → (out : β) → motive (Std.IterStep.yield it' out)) →
          ((it' : Std.IterM m β) → motive (Std.IterStep.skip it')) → (Unit → motive Std.IterStep.done) → motive x
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.Compacts.coe_singleton : ∀ {α : Type u_1} [inst : TopologicalSpace α] (x : α), ↑{x} = {x}
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgEquiv.toAlgEquiv_symm : ∀ {R : Type u_6} {A : Type u_7} {B : Type u_8} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : Star A] [inst_6 : Star B] (f : A ≃⋆ₐ[R] B),
  f.symm.toAlgEquiv = f.toAlgEquiv.symm
-- Mathlib.Analysis.Calculus.ParametricIntervalIntegral
/-- Differentiation under integral of `x ↦ ∫ F x a` at a given point `x₀`, assuming
`F x₀` is integrable, `x ↦ F x a` is differentiable on a neighborhood of `x₀` for ae `a` with
derivative norm uniformly bounded by an integrable function (the neighborhood independent of `a`),
and `F x` is ae-measurable for `x` in a possibly smaller neighborhood of `x₀`.  -/
intervalIntegral.hasFDerivAt_integral_of_dominated_of_fderiv_le : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {μ : MeasureTheory.Measure ℝ} {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] [inst_3 : NormedSpace 𝕜 E] {H : Type u_3} [inst_4 : NormedAddCommGroup H]
  [inst_5 : NormedSpace 𝕜 H] {s : Set H} {a b : ℝ} {bound : ℝ → ℝ} {F : H → ℝ → E} {F' : H → ℝ → H →L[𝕜] E} {x₀ : H},
  s ∈ nhds x₀ →
    (∀ᶠ (x : H) in nhds x₀, MeasureTheory.AEStronglyMeasurable (F x) (μ.restrict (Set.uIoc a b))) →
      IntervalIntegrable (F x₀) μ a b →
        MeasureTheory.AEStronglyMeasurable (F' x₀) (μ.restrict (Set.uIoc a b)) →
          (∀ᵐ (t : ℝ) ∂μ, t ∈ Set.uIoc a b → ∀ x ∈ s, ‖F' x t‖ ≤ bound t) →
            IntervalIntegrable bound μ a b →
              (∀ᵐ (t : ℝ) ∂μ, t ∈ Set.uIoc a b → ∀ x ∈ s, HasFDerivAt (fun x => F x t) (F' x t) x) →
                HasFDerivAt (fun x => ∫ (t : ℝ) in a..b, F x t ∂μ) (∫ (t : ℝ) in a..b, F' x₀ t ∂μ) x₀
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
/-- The coercion from `M →L[R] M₂` to `M →ₗ[R] M₂`, as a linear map.  -/
ContinuousLinearMap.coeLM : {R : Type u_1} →
  (S : Type u_4) →
    [inst : Semiring R] →
      [inst_1 : Semiring S] →
        {M : Type u_6} →
          [inst_2 : TopologicalSpace M] →
            [inst_3 : AddCommMonoid M] →
              [inst_4 : Module R M] →
                {N₃ : Type u_10} →
                  [inst_5 : TopologicalSpace N₃] →
                    [inst_6 : AddCommMonoid N₃] →
                      [inst_7 : Module R N₃] →
                        [inst_8 : Module S N₃] →
                          [inst_9 : SMulCommClass R S N₃] →
                            [inst_10 : ContinuousConstSMul S N₃] →
                              [inst_11 : ContinuousAdd N₃] → (M →L[R] N₃) →ₗ[S] M →ₗ[R] N₃
-- Lean.Elab.PreDefinition.TerminationHint
Lean.Elab.DecreasingBy.mk.sizeOf_spec : ∀ (ref : Lean.Syntax) (tactic : Lean.TSyntax `Lean.Parser.Tactic.tacticSeq),
  sizeOf { ref := ref, tactic := tactic } = 1 + sizeOf ref + sizeOf tactic