mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.realize_formula_top : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u_3} {φ : L.Formula α} {v : α → ↥⊤},
  φ.Realize v ↔ φ.Realize (Subtype.val ∘ v)
-- Mathlib.GroupTheory.GroupAction.Hom
MulActionHom.ofEq.eq_1 : ∀ {M : Type u_2} {N : Type u_3} {φ : M → N} {X : Type u_5} [inst : SMul M X] {Y : Type u_6} [inst_1 : SMul N Y]
  {φ' : M → N} (h : φ = φ') (f : X →ₑ[φ] Y), MulActionHom.ofEq h f = { toFun := f.toFun, map_smul' := ⋯ }
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.mk.inj : ∀ {α : Type u} {inst : MeasurableSpace α} {β : Type v} {toFun : α → β}
  {measurableSet_fiber' : ∀ (x : β), MeasurableSet (toFun ⁻¹' {x})} {finite_range' : (Set.range toFun).Finite}
  {toFun_1 : α → β} {measurableSet_fiber'_1 : ∀ (x : β), MeasurableSet (toFun_1 ⁻¹' {x})}
  {finite_range'_1 : (Set.range toFun_1).Finite},
  { toFun := toFun, measurableSet_fiber' := measurableSet_fiber', finite_range' := finite_range' } =
      { toFun := toFun_1, measurableSet_fiber' := measurableSet_fiber'_1, finite_range' := finite_range'_1 } →
    toFun = toFun_1
-- Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
/-- The (distinguished) triangle in the homotopy category that is associated to
a morphism `φ : K ⟶ L` in the category `CochainComplex C ℤ`.  -/
CochainComplex.mappingCone.triangleh : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [CategoryTheory.Limits.HasBinaryBiproducts C] →
        {K L : CochainComplex C ℤ} →
          (K ⟶ L) → CategoryTheory.Pretriangulated.Triangle (HomotopyCategory C (ComplexShape.up ℤ))
-- Mathlib.MeasureTheory.Integral.Average
MeasureTheory.setLAverage_const : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α},
  μ s ≠ 0 → μ s ≠ ⊤ → ∀ (c : ENNReal), ⨍⁻ (_x : α) in s, c ∂μ = c
-- Mathlib.Data.DFinsupp.Order
DFinsupp.support_mono : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → AddCommMonoid (α i)] [inst_1 : (i : ι) → PartialOrder (α i)]
  [∀ (i : ι), CanonicallyOrderedAdd (α i)] [inst_3 : DecidableEq ι] [inst_4 : (i : ι) → (x : α i) → Decidable (x ≠ 0)]
  {f g : Π₀ (i : ι), α i}, f ≤ g → f.support ⊆ g.support
-- Mathlib.Analysis.Convex.Combination
/-- The `vectorSpan` of a segment is the span of the difference of its endpoints.  -/
vectorSpan_segment : ∀ {R : Type u_1} {E : Type u_3} [inst : Field R] [inst_1 : AddCommGroup E] [inst_2 : Module R E]
  [inst_3 : LinearOrder R] [IsStrictOrderedRing R] {p₁ p₂ : E}, vectorSpan R (segment R p₁ p₂) = R ∙ (p₂ -ᵥ p₁)
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf
AlgebraicGeometry.Proj.res_apply : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] {U V : (TopologicalSpace.Opens ↑(ProjectiveSpectrum.top 𝒜))ᵒᵖ} (i : V ⟶ U)
  (s : ↑((AlgebraicGeometry.ProjectiveSpectrum.Proj.structureSheaf 𝒜).obj.obj V)) (x : ↥(Opposite.unop U)),
  ↑((CategoryTheory.ConcreteCategory.hom ((AlgebraicGeometry.ProjectiveSpectrum.Proj.structureSheaf 𝒜).obj.map i)) s)
      x =
    ↑s (i.unop x)
-- Mathlib.Analysis.Rat.NatSqrt.Real
Nat.realSqrt_lt_ratSqrt_add_inv_prec : ∀ (x : ℕ) {prec : ℕ}, 0 < prec → √↑x < ↑(x.ratSqrt prec) + 1 / ↑prec
-- Lean.PrettyPrinter.Delaborator.Attributes
/-- Marks a declaration to never be pretty printed using field notation.  -/
Lean.ppNoDotAttr : Lean.TagAttribute
-- Mathlib.Combinatorics.Additive.VerySmallDoubling
_private.Mathlib.Combinatorics.Additive.VerySmallDoubling.0.Finset.le_card_smul_inter_smul : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] {K : ℝ} {A B : Finset G} {a b : G},
  ↑(B * A).card ≤ K * ↑A.card → a ∈ B → b ∈ B → (2 - K) * ↑A.card ≤ ↑(a • A ∩ b • A).card
-- Mathlib.Algebra.GroupWithZero.Defs
mul_ne_zero_iff_right : ∀ {M₀ : Type u_1} [inst : MulZeroClass M₀] [NoZeroDivisors M₀] {a b : M₀}, b ≠ 0 → (a * b ≠ 0 ↔ a ≠ 0)
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.coconeOpEquiv_unitIso : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C},
  CategoryTheory.Limits.coconeOpEquiv.unitIso =
    CategoryTheory.Iso.refl (CategoryTheory.Functor.id (CategoryTheory.Limits.Cocone F)ᵒᵖ)
-- Mathlib.RingTheory.MatrixPolynomialAlgebra
/-- Extend a ring hom `A → Mₙ(R)` to a ring hom `A[X] → Mₙ(R[X])`.  -/
RingHom.polyToMatrix : {R : Type u_1} →
  {A : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : Semiring A] →
        {n : Type w} →
          [inst_2 : DecidableEq n] →
            [inst_3 : Fintype n] → (A →+* Matrix n n R) → Polynomial A →+* Matrix n n (Polynomial R)
-- Mathlib.Data.PNat.Find
PNat.decidablePredExistsNat : {p : ℕ+ → Prop} → [DecidablePred p] → DecidablePred fun n' => ∃ n, ∃ (_ : n' = ↑n), p n
-- Mathlib.Order.UpperLower.Relative
instSetLikeRelLowerSet : {α : Type u_1} → {P : α → Prop} → [inst : LE α] → SetLike (RelLowerSet P) α
-- Mathlib.Topology.Order.WithTop
WithBot.isOpenEmbedding_coe : ∀ {ι : Type u_1} [inst : LinearOrder ι] [inst_1 : TopologicalSpace ι] [inst_2 : OrderTopology ι],
  Topology.IsOpenEmbedding WithBot.some
-- Mathlib.FieldTheory.Separable
/-- A polynomial is separable iff it is coprime with its derivative.  -/
Polynomial.Separable : {R : Type u} → [inst : CommSemiring R] → Polynomial R → Prop
-- Mathlib.Analysis.Calculus.ContDiffHolder.Pointwise
ContDiffPointwiseHolderAt.of_order_lt : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {k l : ℕ} {α β : ↑unitInterval} {f : E → F} {a : E},
  ContDiffPointwiseHolderAt k α f a → l < k → ContDiffPointwiseHolderAt l β f a
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.closure_insert_intCast : ∀ {R : Type u} [inst : NonAssocRing R] (n : ℤ) (s : Set R), Subring.closure (insert (↑n) s) = Subring.closure s
-- Mathlib.Tactic.Contrapose
_private.Mathlib.Tactic.Contrapose.0.Mathlib.Tactic.Contrapose.tacticTry_push_neg_ : Lean.ParserDescr
-- Mathlib.NumberTheory.SumFourSquares
/-- **Four squares theorem**  -/
Nat.sum_four_squares : ∀ (n : ℕ), ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = n
-- Init.Data.String.Lemmas.FindPos
String.Slice.le_posLT_iff : ∀ {s : String.Slice} {p : String.Pos.Raw} {h : 0 < p} {q : s.Pos}, q ≤ s.posLT p h ↔ q.offset < p
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roi.toArray_eq_match_rci : ∀ {α : Type u} {r : Std.Roi α} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.PRange.LawfulUpwardEnumerable α]
  [inst_2 : Std.Rxi.IsAlwaysFinite α],
  r.toArray =
    match Std.PRange.succ? r.lower with
    | none => #[]
    | some next => next...*.toArray
-- Mathlib.Algebra.Category.Grp.Basic
CategoryTheory.Iso.commGroupIsoToMulEquiv_apply : ∀ {X Y : CommGrpCat} (i : X ≅ Y) (a : ↑X), i.commGroupIsoToMulEquiv a = (CommGrpCat.Hom.hom i.hom) a
-- Mathlib.Analysis.Convex.Intrinsic
intrinsicFrontier_empty : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [inst : Ring 𝕜] [inst_1 : AddCommGroup V] [inst_2 : Module 𝕜 V]
  [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P], intrinsicFrontier 𝕜 ∅ = ∅
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
AlgebraicGeometry.Scheme.Modules.instAbelian : {X : AlgebraicGeometry.Scheme} → CategoryTheory.Abelian X.Modules
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.hom_hom_associator : ∀ {k : Type u} {G : Type v} [inst : CommRing k] [inst_1 : Monoid G] {X Y Z : Rep.{u, u, v} k G},
  Rep.Hom.hom (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom =
    ↑(Representation.TensorProduct.assoc X.ρ Y.ρ Z.ρ)
-- Mathlib.Data.Set.PowersetCard
Set.powersetCard.coe_nontrivial_iff : ∀ {α : Type u_1} {n : ℕ} {s : ↑(Set.powersetCard α n)}, (↑s).Nontrivial ↔ 1 < n
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getD_modify : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp],
  t.WF →
    ∀ {k k' : α} {fallback : β k'} {f : β k → β k},
      (t.modify k f).getD k' fallback =
        if heq : cmp k k' = Ordering.eq then (Option.map (cast ⋯) (Option.map f (t.get? k))).getD fallback
        else t.getD k' fallback
-- Mathlib.MeasureTheory.Measure.Stieltjes
StieltjesFunction.measure_const : ∀ {R : Type u_1} [inst : LinearOrder R] [inst_1 : TopologicalSpace R] [inst_2 : OrderTopology R]
  [inst_3 : CompactIccSpace R] [inst_4 : MeasurableSpace R] [inst_5 : BorelSpace R] [inst_6 : SecondCountableTopology R]
  [inst_7 : DenselyOrdered R] (c : ℝ), (StieltjesFunction.const R c).measure = 0
-- Lean.Meta.PPGoal
_private.Lean.Meta.PPGoal.0.Lean.Meta.ppGoal.pushPending : ℤ → List Lean.Name → Option Lean.Expr → Std.Format → Lean.MetaM Std.Format
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.getKeyDₘ_eq_getKeyD : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  {m : Std.DHashMap.Internal.Raw₀ α β},
  Std.DHashMap.Internal.Raw.WFImp ↑m →
    ∀ {a fallback : α},
      m.getKeyDₘ a fallback = Std.Internal.List.getKeyD a (Std.DHashMap.Internal.toListModel (↑m).buckets) fallback
-- Mathlib.Algebra.Group.Subsemigroup.MulOpposite
Subsemigroup.mem_op : ∀ {M : Type u_2} [inst : Mul M] {x : Mᵐᵒᵖ} {S : Subsemigroup M}, x ∈ S.op ↔ MulOpposite.unop x ∈ S
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.iIndepFun.of_subsingleton : ∀ {Ω : Type u_1} {ι : Type u_2} {x : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [Subsingleton ι]
  {β : ι → Type u_7} {m : (i : ι) → MeasurableSpace (β i)} {f : (i : ι) → Ω → β i}
  [MeasureTheory.IsProbabilityMeasure μ], ProbabilityTheory.iIndepFun f μ
-- Lean.Data.Lsp.Internal
Lean.Lsp.RefInfo.Location.mk'.injEq : ∀ (startPosLine startPosCharacter endPosLine endPosCharacter : ℕ) (parentDecl : String)
  (startPosLine_1 startPosCharacter_1 endPosLine_1 endPosCharacter_1 : ℕ) (parentDecl_1 : String),
  ({ startPosLine := startPosLine, startPosCharacter := startPosCharacter, endPosLine := endPosLine,
        endPosCharacter := endPosCharacter, parentDecl := parentDecl } =
      { startPosLine := startPosLine_1, startPosCharacter := startPosCharacter_1, endPosLine := endPosLine_1,
        endPosCharacter := endPosCharacter_1, parentDecl := parentDecl_1 }) =
    (startPosLine = startPosLine_1 ∧
      startPosCharacter = startPosCharacter_1 ∧
        endPosLine = endPosLine_1 ∧ endPosCharacter = endPosCharacter_1 ∧ parentDecl = parentDecl_1)
-- Lean.Meta.Tactic.Simp.Main
Lean.Meta.Simp.backward.dsimp.proofs : Lean.Option Bool
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrp.instCategory.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C],
  CategoryTheory.AddGrp.instCategory =
    { Hom := CategoryTheory.AddGrp.instCategory._aux_1, id := CategoryTheory.AddGrp.instCategory._aux_3,
      comp := @CategoryTheory.AddGrp.instCategory._aux_5 C inst inst_1, id_comp := ⋯, comp_id := ⋯, assoc := ⋯ }
-- Lean.Data.Json.FromToJson.Basic
Lean.FromJson.fromJson? : {α : Type u} → [self : Lean.FromJson α] → Lean.Json → Except String α
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
/-- Synonym of `Matrix.IsHyperbolic`, for dot-notation.  -/
Matrix.GeneralLinearGroup.IsHyperbolic : {R : Type u_1} → [inst : CommRing R] → [Preorder R] → GL (Fin 2) R → Prop
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.RingDiseqCnstr.mk.sizeOf_spec : ∀ (p : Lean.Grind.CommRing.Poly) (h : Lean.Meta.Grind.Arith.Linear.RingDiseqCnstrProof),
  sizeOf { p := p, h := h } = 1 + sizeOf p + sizeOf h
-- Mathlib.GroupTheory.Perm.Centralizer
/-- The parametrization of the kernel of `toPermHom`  -/
Equiv.Perm.OnCycleFactors.kerParam : {α : Type u_1} →
  [inst : DecidableEq α] →
    [inst_1 : Fintype α] →
      (g : Equiv.Perm α) →
        Equiv.Perm ↑(Function.fixedPoints ⇑g) × ((c : ↥g.cycleFactorsFinset) → ↥(Subgroup.zpowers ↑c)) →* Equiv.Perm α
-- Std.Http.Protocol.H1
/-- Dispatch for fixed-length body writing, including omitted-body fast path and
zero/non-zero remaining-length handling.
 -/
_private.Std.Http.Protocol.H1.0.Std.Http.Protocol.H1.Machine.processFixedBody : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Machine dir → ℕ → Std.Http.Protocol.H1.Machine dir
-- Mathlib.RingTheory.DividedPowers.DPMorphism
DividedPowers.DPMorphism.ext_iff : ∀ {A : Type u_3} {B : Type u_4} {inst : CommSemiring A} {inst_1 : CommSemiring B} {I : Ideal A} {J : Ideal B}
  {hI : DividedPowers I} {hJ : DividedPowers J} {x y : hI.DPMorphism hJ},
  x = y ↔ (↑↑x.toRingHom).toFun = (↑↑y.toRingHom).toFun
-- Mathlib.Order.Interval.Finset.Defs
/-- A fintype is a locally finite order.

This is not an instance as it would not be defeq to better instances such as
`Fin.locallyFiniteOrder`.
 -/
Fintype.toLocallyFiniteOrder : {α : Type u_1} → [inst : Preorder α] → [Fintype α] → [DecidableLT α] → [DecidableLE α] → LocallyFiniteOrder α
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.get!_modify : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k k' : α} [hi : Inhabited (β k')] {f : β k → β k},
  (t.modify k f).get! k' =
    if heq : cmp k k' = Ordering.eq then (Option.map (cast ⋯) (Option.map f (t.get? k))).get! else t.get! k'
-- Mathlib.Topology.Constructions
nhds_ne_subtype_neBot_iff : ∀ {X : Type u} [inst : TopologicalSpace X] {S : Set X} {x : ↑S},
  (nhdsWithin x {x}ᶜ).NeBot ↔ (nhdsWithin ↑x {↑x}ᶜ ⊓ Filter.principal S).NeBot
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonPrepareRenameParams : Lean.ToJson Lean.Lsp.PrepareRenameParams
-- Mathlib.Analysis.Normed.Group.Real
Real.toNNReal_eq_nnnorm_of_nonneg : ∀ {r : ℝ}, 0 ≤ r → r.toNNReal = ‖r‖₊
-- Init.Data.Dyadic.Basic
Dyadic.blt.eq_1 : Dyadic.zero.blt Dyadic.zero = false
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
CategoryTheory.Oplax.StrongTrans.Modification.ext : ∀ {B : Type u₁} {inst : CategoryTheory.Bicategory B} {C : Type u₂} {inst_1 : CategoryTheory.Bicategory C}
  {F G : CategoryTheory.OplaxFunctor B C} {η θ : F ⟶ G} {x y : CategoryTheory.Oplax.StrongTrans.Modification η θ},
  x.app = y.app → x = y
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.HasColimit.mk : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor J C} (d : CategoryTheory.Limits.ColimitCocone F), CategoryTheory.Limits.HasColimit F
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2to1.stRun.eq_2 : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} {k : K} (f : σ → Option (Γ k) → σ),
  Turing.TM2to1.stRun (Turing.TM2to1.StAct.peek f) = Turing.TM2.Stmt.peek k f
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify
PresheafOfModules.Sheafify.one_smul : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R₀ : CategoryTheory.Functor Cᵒᵖ RingCat} {R : CategoryTheory.Sheaf J RingCat} (α : R₀ ⟶ R.obj)
  [inst_1 : CategoryTheory.Presheaf.IsLocallyInjective J α] [inst_2 : CategoryTheory.Presheaf.IsLocallySurjective J α]
  {M₀ : PresheafOfModules R₀} {A : CategoryTheory.Sheaf J AddCommGrpCat} (φ : M₀.presheaf ⟶ A.obj)
  [inst_3 : CategoryTheory.Presheaf.IsLocallyInjective J φ] [inst_4 : CategoryTheory.Presheaf.IsLocallySurjective J φ]
  {X : Cᵒᵖ} (m : ↑(A.obj.obj X)), PresheafOfModules.Sheafify.smul α φ 1 m = m
-- Mathlib.Algebra.Homology.ComplexShapeSigns
ComplexShape.instTensorSignsIntUp : (ComplexShape.up ℤ).TensorSigns
-- Mathlib.Algebra.Category.Grp.Basic
_private.Mathlib.Algebra.Category.Grp.Basic.0.AddGrpCat.Hom.mk.inj : ∀ {A B : AddGrpCat} {hom' hom'_1 : ↑A →+ ↑B}, { hom' := hom' } = { hom' := hom'_1 } → hom' = hom'_1
-- Init.Data.Bool
Bool.false_beq : ∀ (b : Bool), (false == b) = !b
-- Mathlib.Data.Fin.Parity
Fin.even_succAbove_add_predAbove : ∀ {n : ℕ} (i : Fin (n + 1)) (j : Fin n), Even (↑(i.succAbove j) + ↑(j.predAbove i)) ↔ Odd (↑i + ↑j)
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
/-- If two functions agree in a neighborhood, then so do their iterated derivatives.  -/
Filter.EventuallyEq.iteratedFDeriv : ∀ (𝕜 : Type u) [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f₁ f₂ : E → F}
  {x : E}, f₁ =ᶠ[nhds x] f₂ → ∀ (n : ℕ), iteratedFDeriv 𝕜 n f₁ =ᶠ[nhds x] iteratedFDeriv 𝕜 n f₂
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
/-- Change of variables, general form. If `f` is continuous on `[a, b]` and has
right-derivative `f'` in `(a, b)`, `g` is continuous on `f '' (a, b)` and integrable on
`f '' [a, b]`, and `f' x • (g ∘ f) x` is integrable on `[a, b]`,
then we can substitute `u = f x` to get `∫ x in a..b, f' x • (g ∘ f) x = ∫ u in f a..f b, g u`.

If the function `f` is monotone or antitone, see also `integral_deriv_smul_comp_of_deriv_nonneg`
and `integral_deriv_smul_comp_of_deriv_nonpos` dropping all assumptions on `g`.  -/
intervalIntegral.integral_deriv_smul_comp''' : ∀ {a b : ℝ} {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f f' : ℝ → ℝ} {g : ℝ → E},
  ContinuousOn f (Set.uIcc a b) →
    (∀ x ∈ Set.Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Set.Ioi x) x) →
      ContinuousOn g (f '' Set.Ioo (min a b) (max a b)) →
        MeasureTheory.IntegrableOn g (f '' Set.uIcc a b) MeasureTheory.volume →
          MeasureTheory.IntegrableOn (fun x => f' x • (g ∘ f) x) (Set.uIcc a b) MeasureTheory.volume →
            ∫ (x : ℝ) in a..b, f' x • (g ∘ f) x = ∫ (u : ℝ) in f a..f b, g u
-- Std.Data.DTreeMap.Internal.Queries
/-- Implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.getKey : {α : Type u} →
  {β : α → Type v} →
    [inst : Ord α] → (t : Std.DTreeMap.Internal.Impl α β) → (k : α) → Std.DTreeMap.Internal.Impl.contains k t = true → α
-- Lean.Data.Lsp.Extra
Lean.Lsp.HighlightMatchesOptions.mk : Lean.Lsp.HighlightMatchesOptions
-- Mathlib.Data.Finsupp.Fin
Finsupp.tail_cons : ∀ {n : ℕ} {M : Type u_1} [inst : Zero M] (y : M) (s : Fin n →₀ M), (Finsupp.cons y s).tail = s
-- Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
IsLocalFrameOn.mono : ∀ {𝕜 : 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_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → AddCommGroup (V x)] [inst_10 : (x : M) → Module 𝕜 (V x)]
  [inst_11 : (x : M) → TopologicalSpace (V x)] [inst_12 : FiberBundle F V] {ι : Type u_7} {s : ι → (x : M) → V x}
  {u u' : Set M} {n : WithTop ℕ∞}, IsLocalFrameOn I F n s u → u' ⊆ u → IsLocalFrameOn I F n s u'
-- Mathlib.Algebra.FreeAbelianGroup.Finsupp
/-- The group homomorphism `(X →₀ ℤ) →+ FreeAbelianGroup X`.  -/
Finsupp.toFreeAbelianGroup : {X : Type u_1} → (X →₀ ℤ) →+ FreeAbelianGroup X
-- Init.Data.UInt.Lemmas
UInt64.ofNatClamp_uInt8ToNat : ∀ (n : UInt8), UInt64.ofNatClamp n.toNat = n.toUInt64
-- Init.Data.BitVec.Lemmas
BitVec.toInt_and : ∀ {w : ℕ} (x y : BitVec w), (x &&& y).toInt = (↑(x.toNat &&& y.toNat)).bmod (2 ^ w)
-- Lean.Meta.Tactic.Grind.Types
/-- Creates an auxiliary metavariable with the same type and context of `goal.mvarId`.
We use this function to perform `cases` on the current goal without eagerly assigning it.
 -/
Lean.Meta.Grind.Goal.mkAuxMVar : Lean.Meta.Grind.Goal → Lean.MetaM Lean.MVarId
-- Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
SimpleGraph.Walk.support_takeUntil_prefix_support : ∀ {V : Type u} {G : SimpleGraph V} {v w u : V} [inst : DecidableEq V] (p : G.Walk v w) (h : u ∈ p.support),
  (p.takeUntil u h).support <+: p.support
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.mem_iff_contains : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {a : α}, a ∈ m ↔ m.contains a = true
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.all_eq_not_any_not : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} {p : (a : α) → β a → Bool},
  m.all p = !m.any fun a b => !p a b
-- Mathlib.Order.SuccPred.Limit
Order.not_isSuccLimit_succ_of_not_isMax : ∀ {α : Type u_1} {a : α} [inst : Preorder α] [inst_1 : SuccOrder α], ¬IsMax a → ¬Order.IsSuccLimit (Order.succ a)
-- Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular
/-- If `A` is totally unimodular and each row of `B` is all zeros except for at most a single `1` or
a single `-1` then `fromRows A B` is totally unimodular.  -/
Matrix.IsTotallyUnimodular.fromRows_unitlike : ∀ {m : Type u_1} {m' : Type u_2} {n : Type u_3} {R : Type u_5} [inst : CommRing R] [inst_1 : DecidableEq n]
  {A : Matrix m n R} {B : Matrix m' n R},
  A.IsTotallyUnimodular → (Nonempty n → ∀ (i : m'), ∃ j s, B i = Pi.single j ↑s) → (A.fromRows B).IsTotallyUnimodular
-- Mathlib.Algebra.Category.AlgCat.Basic
/-- Turn a morphism in `AlgCat` back into an `AlgHom`.  -/
AlgCat.Hom.hom : {R : Type u} → [inst : CommRing R] → {A B : AlgCat R} → A.Hom B → ↑A →ₐ[R] ↑B
-- Mathlib.Computability.Primrec.List
Nat.Primrec'.below.zero : ∀ {motive : {n : ℕ} → (a : List.Vector ℕ n → ℕ) → Nat.Primrec' a → Prop}, Nat.Primrec'.below Nat.Primrec'.zero
-- Mathlib.Order.Lattice.Congruence
_private.Mathlib.Order.Lattice.Congruence.0.LatticeCon.transitive : ∀ {α : Type u_2} [inst : Lattice α] {r : α → α → Prop},
  (∀ ⦃x y : α⦄, r x y ↔ r (x ⊓ y) (x ⊔ y)) →
    (∀ ⦃x y z : α⦄, x ≤ y → y ≤ z → r x y → r y z → r x z) →
      (∀ ⦃x y t : α⦄, x ≤ y → r x y → r (x ⊓ t) (y ⊓ t) ∧ r (x ⊔ t) (y ⊔ t)) → ∀ {x y z : α}, r x y → r y z → r x z
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
measurable_equivCurry_symm : ∀ {ι : Type u_6} {κ : Type u_7} {X : Type u_8} [inst : MeasurableSpace X], Measurable ⇑(Equiv.curry ι κ X).symm
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToIntInfo
Lean.Meta.Grind.Arith.Cutsat.SymbolicBound.mk.sizeOf_spec : ∀ (val : Lean.Expr) (ival? : Option ℤ), sizeOf { val := val, ival? := ival? } = 1 + sizeOf val + sizeOf ival?
-- Mathlib.Topology.Algebra.Group.Basic
nhds_inv : ∀ (G : Type w) [inst : TopologicalSpace G] [inst_1 : InvolutiveInv G] [ContinuousInv G] (a : G), nhds a⁻¹ = (nhds a)⁻¹
-- Mathlib.Topology.Convenient.GeneratedBy
Topology.IsGeneratedBy.instWithGeneratedByTopology : ∀ {ι : Type t} {X : ι → Type u} [inst : (i : ι) → TopologicalSpace (X i)] {Y : Type v} [tY : TopologicalSpace Y],
  Topology.IsGeneratedBy X (Topology.WithGeneratedByTopology X Y)
-- Mathlib.Analysis.BoxIntegral.UnitPartition
/-- Let `s` be a bounded, measurable set of `ι → ℝ` whose frontier has zero volume and let `F`
be a continuous function. Then the limit as `n → ∞` of `∑ F x / n ^ card ι`, where the sum is
over the points in `s ∩ n⁻¹ • (ι → ℤ)`, tends to the integral of `F` over `s`.  -/
tendsto_tsum_div_pow_atTop_integral : ∀ {ι : Type u_1} (s : Set (ι → ℝ)) (F : (ι → ℝ) → ℝ) [inst : Fintype ι],
  Continuous F →
    Bornology.IsBounded s →
      MeasurableSet s →
        MeasureTheory.volume (frontier s) = 0 →
          Filter.Tendsto
            (fun n =>
              (∑' (x : ↑(s ∩ (↑n)⁻¹ • ↑(Submodule.span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))), F ↑x) / ↑n ^ Fintype.card ι)
            Filter.atTop (nhds (∫ (x : ι → ℝ) in s, F x))
-- Mathlib.Algebra.Group.Submonoid.Units
Submonoid.units_bot : ∀ {M : Type u_1} [inst : Monoid M], ⊥.units = ⊥
-- Init.Grind.AC
Lean.Grind.AC.eq_norm_aci : ∀ {α : Sort u_1} (ctx : Lean.Grind.AC.Context α) {x : Std.Associative ctx.op} {x : Std.Commutative ctx.op}
  {x : Std.LawfulIdentity ctx.op (Lean.Grind.AC.Var.denote ctx 0)} (lhs rhs : Lean.Grind.AC.Expr)
  (lhs' rhs' : Lean.Grind.AC.Seq),
  Lean.Grind.AC.eq_norm_aci_cert lhs rhs lhs' rhs' = true →
    Lean.Grind.AC.Expr.denote ctx lhs = Lean.Grind.AC.Expr.denote ctx rhs →
      Lean.Grind.AC.Seq.denote ctx lhs' = Lean.Grind.AC.Seq.denote ctx rhs'