mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Probability.Martingale.Basic
MeasureTheory.Submartingale.sum_smul_sub : ∀ {Ω : Type u_1} {E : Type u_2} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] {𝒢 : MeasureTheory.Filtration ℕ m0} [CompleteSpace E] [inst_3 : PartialOrder E]
  [IsOrderedModule ℝ E] [ClosedIciTopology E] [IsOrderedAddMonoid E] [MeasureTheory.IsFiniteMeasure μ] {R : ℝ}
  {f : ℕ → Ω → E} {ξ : ℕ → Ω → ℝ},
  MeasureTheory.Submartingale f 𝒢 μ →
    MeasureTheory.StronglyAdapted 𝒢 ξ →
      (∀ (n : ℕ) (ω : Ω), ξ n ω ≤ R) →
        (∀ (n : ℕ) (ω : Ω), 0 ≤ ξ n ω) →
          MeasureTheory.Submartingale (fun n => ∑ k ∈ Finset.range n, ξ k • (f (k + 1) - f k)) 𝒢 μ
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.lt_bsup : ∀ {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}) {a : Ordinal.{max u v}},
  a < o.bsup f ↔ ∃ i, ∃ (hi : i < o), a < f i hi
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.InternalState.footnotes : Lean.Doc.InternalState → Std.HashMap String (Lean.Doc.Ref✝ (Lean.Doc.Inline Lean.ElabInline))
-- Init.Data.List.Find
_private.Init.Data.List.Find.0.List.filterMap.match_1.eq_2 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (b : β) (h_1 : Unit → motive none) (h_2 : (b : β) → motive (some b)),
  (match some b with
    | none => h_1 ()
    | some b => h_2 b) =
    h_2 b
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
CategoryTheory.IsPullback.isIso_fst_of_mono : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P X Y : C} {fst snd : P ⟶ X} {f : X ⟶ Y},
  CategoryTheory.IsPullback fst snd f f →
    autoParam (CategoryTheory.Mono f) CategoryTheory.IsPullback.isIso_fst_of_mono._auto_1 → CategoryTheory.IsIso fst
-- Mathlib.Algebra.Group.Torsion
/-- See `sq_eq_one_iff` for a version that holds in rings.  -/
sq_eq_one : ∀ {M : Type u_1} [inst : Monoid M] [IsMulTorsionFree M] {a : M}, a ^ 2 = 1 ↔ a = 1
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.p_opcyclesToE : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃)
  (f₁₂ : i₀ ⟶ i₂) (h₁₂ : CategoryTheory.CategoryStruct.comp f₁ f₂ = f₁₂) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.p_opcyclesToE._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.p_opcyclesToE._auto_3),
  CategoryTheory.CategoryStruct.comp (X.pOpcycles f₁₂ f₃ n₁) (X.opcyclesToE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂) =
    CategoryTheory.CategoryStruct.comp (X.toCycles f₁ f₂ f₁₂ h₁₂ n₁) (X.πE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂)
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_inv_fst_assoc : ∀ {X Y Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst : ∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g] (i : 𝒰.I₀)
  {Z_1 : AlgebraicGeometry.Scheme} (h : (AlgebraicGeometry.Scheme.Pullback.gluing 𝒰 f g).glued ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso 𝒰 f g i).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Scheme.Pullback.p1 𝒰 f g) (𝒰.f i)) h) =
    CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Scheme.Pullback.gluing 𝒰 f g).ι i) h
-- Mathlib.NumberTheory.DirichletCharacter.Basic
/-- The primitive character of `changeLevel hm χ` is equal to the primitive character of `χ`.
This is stated as a pointwise equality because the equality of Dirichlet characters does
not typecheck.  -/
DirichletCharacter.primitiveCharacter_changeLevel_apply : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] {n : ℕ} [Nontrivial R] {m : ℕ} [NeZero m] (hm : n ∣ m)
  (χ : DirichletCharacter R n) (a : ℤ),
  ((DirichletCharacter.changeLevel hm) χ).primitiveCharacter ↑a = χ.primitiveCharacter ↑a
-- Mathlib.MeasureTheory.VectorMeasure.Variation.Basic
/-- Measure version of `preVariation.exists_Finpartition_sum_ge'`.  -/
MeasureTheory.VectorMeasure.exists_variation_le_add' : ∀ {X : Type u_1} {V : Type u_2} {mX : MeasurableSpace X} [inst : TopologicalSpace V] [inst_1 : ENormedAddCommMonoid V]
  [inst_2 : T2Space V] (μ : MeasureTheory.VectorMeasure X V) {s : Set X},
  MeasurableSet s →
    ∀ {ε : ENNReal},
      0 < ε →
        μ.variation s ≠ ⊤ →
          ∃ P,
            (∀ t ∈ P, t ⊆ s) ∧
              (↑P).PairwiseDisjoint id ∧ (∀ t ∈ P, MeasurableSet t) ∧ μ.variation s ≤ ∑ p ∈ P, ‖μ p‖ₑ + ε
-- Mathlib.Analysis.InnerProductSpace.Basic
/-- **Cauchy–Schwarz inequality**.  -/
inner_mul_inner_self_le : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (x y : E), ‖inner 𝕜 x y‖ * ‖inner 𝕜 y x‖ ≤ RCLike.re (inner 𝕜 x x) * RCLike.re (inner 𝕜 y y)
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
/-- The upper part of the second column of the snake diagram is exact.  -/
CategoryTheory.ShortComplex.SnakeInput.exact_C₂_up : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex.SnakeInput C),
  { X₁ := S.L₀.X₂, X₂ := S.L₁.X₂, X₃ := S.L₂.X₂, f := S.v₀₁.τ₂, g := S.v₁₂.τ₂, zero := ⋯ }.Exact
-- Aesop.Rule.Basic
Aesop.Rule.map : {α β : Type} → (α → β) → Aesop.Rule α → Aesop.Rule β
-- Mathlib.Order.BooleanAlgebra.Set
Set.subset_compl_iff_disjoint_left : ∀ {α : Type u_1} {s t : Set α}, s ⊆ tᶜ ↔ Disjoint t s
-- Mathlib.LinearAlgebra.Matrix.Rank
Matrix.rank_mul_le_left : ∀ {m : Type um} {n : Type un} {o : Type uo} {R : Type uR} [inst : Fintype n] [inst_1 : Fintype o]
  [inst_2 : CommSemiring R] [StrongRankCondition R] (A : Matrix m n R) (B : Matrix n o R), (A * B).rank ≤ A.rank
-- Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Complex.betaIntegral_eval_one_right : ∀ {u : ℂ}, 0 < u.re → u.betaIntegral 1 = 1 / u
-- Mathlib.CategoryTheory.ShrinkYoneda
CategoryTheory.shrinkCoyonedaEquiv_symm_map_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C] {X Y : C}
  (f : X ⟶ Y) {P : CategoryTheory.Functor C (Type w)} (t : P.obj X) {Z : CategoryTheory.Functor C (Type w)} (h : P ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.shrinkCoyonedaEquiv.symm ((CategoryTheory.ConcreteCategory.hom (P.map f)) t)) h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.shrinkCoyoneda.{w, v, u}.map f.op)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.shrinkCoyonedaEquiv.symm t) h)
-- Mathlib.RingTheory.PowerSeries.Basic
/-- The natural inclusion from polynomials into formal power series.  -/
Polynomial.coeToPowerSeries : {R : Type u_1} → [inst : Semiring R] → Coe (Polynomial R) (PowerSeries R)
-- Mathlib.GroupTheory.FreeAbelianGroup
FreeAbelianGroup.map_add : ∀ {α β : Type u} (f : α → β) (x y : FreeAbelianGroup α), f <$> (x + y) = f <$> x + f <$> y
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt
_private.Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt.0.Lean.Meta.Grind.Arith.Cutsat.toInt' : Lean.Expr → Lean.Meta.Grind.Arith.Cutsat.ToIntM (Lean.Expr × Lean.Expr)
-- Mathlib.Algebra.GCDMonoid.Basic
instNonemptyNormalizedGCDMonoidOfIsGCDMonoid : ∀ (α : Type u_2) [inst : CommMonoidWithZero α] [IsGCDMonoid α], Nonempty (NormalizedGCDMonoid α)
-- Mathlib.Analysis.Complex.UpperHalfPlane.Topology
UpperHalfPlane.verticalStrip_anti_right : ∀ (A : ℝ) {B B' : ℝ}, B' ≤ B → UpperHalfPlane.verticalStrip A B ⊆ UpperHalfPlane.verticalStrip A B'
-- Mathlib.Data.Finmap
Finmap.liftOn.congr_simp : ∀ {α : Type u} {β : α → Type v} {γ : Type u_1} (s s_1 : Finmap β),
  s = s_1 →
    ∀ (f f_1 : AList β → γ) (e_f : f = f_1) (H : ∀ (a b : AList β), a.entries.Perm b.entries → f a = f b),
      s.liftOn f H = s_1.liftOn f_1 ⋯
-- Mathlib.Analysis.Calculus.FDeriv.CompCLM
/-- Application of a `ContinuousAlternatingMap` to a constant commutes with `fderivWithin`.  -/
fderivWithin_continuousAlternatingMap_apply_const_apply : ∀ {𝕜 : 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] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {x : E} {s : Set E} {ι : Type u_5} {c : E → F [⋀^ι]→L[𝕜] G}
  [Finite ι],
  UniqueDiffWithinAt 𝕜 s x →
    DifferentiableWithinAt 𝕜 c s x →
      ∀ (u : ι → F) (m : E), (fderivWithin 𝕜 (fun y => (c y) u) s x) m = ((fderivWithin 𝕜 c s x) m) u
-- Mathlib.CategoryTheory.Limits.HasLimits
/-- `C` has colimits of shape `J` if there exists a colimit for every functor `F : J ⥤ C`.  -/
CategoryTheory.Limits.HasColimitsOfShape : (J : Type u₁) → [CategoryTheory.Category.{v₁, u₁} J] → (C : Type u) → [CategoryTheory.Category.{v, u} C] → Prop
-- Mathlib.Algebra.CharP.Basic
CharP.natCast_injOn_Iio : ∀ (R : Type u_1) [inst : AddMonoidWithOne R] (p : ℕ) [CharP R p] [IsRightCancelAdd R], Set.InjOn Nat.cast (Set.Iio p)
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
/-- An explicit bound on the size of the equipartition whose existence is given by Szemerédi's
regularity lemma.  -/
SzemerediRegularity.bound : ℝ → ℕ → ℕ
-- Lean.DocString.Parser
Lean.Doc.Parser.InList.mk.sizeOf_spec : ∀ (indentation : ℕ) (type : Lean.Doc.Parser.OrderedListType ⊕ Lean.Doc.Parser.UnorderedListType),
  sizeOf { indentation := indentation, type := type } = 1 + sizeOf indentation + sizeOf type
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.ModuleDocstringState : Type
-- Mathlib.Algebra.Category.MonCat.Adjunctions
AddMonCat.hasForgetToAddSemigroup : CategoryTheory.HasForget₂ AddMonCat AddSemigrp
-- Mathlib.Topology.Instances.TrivSqZeroExt
/-- `TrivSqZeroExt.inr` as a continuous linear map.  -/
TrivSqZeroExt.inrCLM : (R : Type u_3) →
  (M : Type u_4) →
    [inst : TopologicalSpace R] →
      [inst_1 : TopologicalSpace M] →
        [inst_2 : CommSemiring R] → [inst_3 : AddCommMonoid M] → [inst_4 : Module R M] → M →L[R] TrivSqZeroExt R M
-- Mathlib.Analysis.SpecialFunctions.Arsinh
Real.arsinh_surjective : Function.Surjective Real.arsinh
-- Mathlib.Tactic.Linter.HaveLetLinter
/-- given a `ContextInfo`, a `LocalContext` and an `Array` of `Expr`essions `es` with a `Name`,
`toFormat_propTypes` creates a `MetaM` context, and returns an array of
the pretty-printed `Format` of `e`, together with the (unchanged) name
for each `Expr`ession `e` in `es` whose type is a `Prop`.

Concretely, `toFormat_propTypes` runs `inferType` in `CommandElabM`.
This is the kind of monadic lift that `nonPropHaves` uses to decide whether the Type of a `have`
is in `Prop` or not.
The output `Format` is just so that the linter displays a better message.  -/
_private.Mathlib.Tactic.Linter.HaveLetLinter.0.Mathlib.Linter.haveLet.toFormat_propTypes : Lean.Elab.ContextInfo →
  Lean.LocalContext → Array (Lean.Expr × Lean.Name) → Lean.Elab.Command.CommandElabM (Array (Std.Format × Lean.Name))
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.mul.go.match_1.congr_eq_2 : ∀ (motive : Lean.Grind.CommRing.Mon → Lean.Grind.CommRing.Mon → Sort u_1) (m₁ m₂ : Lean.Grind.CommRing.Mon)
  (h_1 : (m₁ : Lean.Grind.CommRing.Mon) → motive m₁ Lean.Grind.CommRing.Mon.unit)
  (h_2 : (m₂ : Lean.Grind.CommRing.Mon) → motive Lean.Grind.CommRing.Mon.unit m₂)
  (h_3 :
    (pw₁ : Lean.Grind.CommRing.Power) →
      (m₁ : Lean.Grind.CommRing.Mon) →
        (pw₂ : Lean.Grind.CommRing.Power) →
          (m₂ : Lean.Grind.CommRing.Mon) →
            motive (Lean.Grind.CommRing.Mon.mult pw₁ m₁) (Lean.Grind.CommRing.Mon.mult pw₂ m₂))
  (m₂_1 : Lean.Grind.CommRing.Mon),
  m₁ = Lean.Grind.CommRing.Mon.unit →
    m₂ = m₂_1 →
      (m₂_1 = Lean.Grind.CommRing.Mon.unit → False) →
        (match m₁, m₂ with
          | m₁, Lean.Grind.CommRing.Mon.unit => h_1 m₁
          | Lean.Grind.CommRing.Mon.unit, m₂ => h_2 m₂
          | Lean.Grind.CommRing.Mon.mult pw₁ m₁, Lean.Grind.CommRing.Mon.mult pw₂ m₂ => h_3 pw₁ m₁ pw₂ m₂) ≍
          h_2 m₂_1
-- Mathlib.GroupTheory.Index
Subgroup.index_eq_zero_of_relIndex_eq_zero : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G}, H.relIndex K = 0 → H.index = 0
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : AlgebraicGeometry.PresheafedSpace C} (f : X ⟶ Y)
  [H : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f] (U : TopologicalSpace.Opens ↑↑X),
  AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp f U =
    CategoryTheory.CategoryStruct.comp (X.presheaf.map (CategoryTheory.eqToHom ⋯))
      (CategoryTheory.inv
        (f.c.app (Opposite.op ((AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.opensFunctor f).obj U))))
-- Mathlib.RingTheory.MvPolynomial.EulerIdentity
MvPolynomial.IsHomogeneous.pderiv : ∀ {R : Type u_1} {σ : Type u_2} [inst : CommSemiring R] {φ : MvPolynomial σ R} {n : ℕ} {i : σ},
  φ.IsHomogeneous n → ((MvPolynomial.pderiv i) φ).IsHomogeneous (n - 1)
-- Mathlib.Tactic.Positivity.Basic
Mathlib.Meta.Positivity.ite_ne_zero_of_pos_of_ne_zero : ∀ {α : Type u_1} [inst : Zero α] (p : Prop) [inst_1 : Decidable p] {a b : α} [inst_2 : Preorder α],
  0 < a → b ≠ 0 → (if p then a else b) ≠ 0
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableEquiv.curry_symm_apply : ∀ (ι : Type u_6) (κ : Type u_7) (X : Type u_8) [inst : MeasurableSpace X] (a : ι → κ → X) (a_1 : ι × κ),
  (MeasurableEquiv.curry ι κ X).symm a a_1 = Function.uncurry a a_1
-- Mathlib.GroupTheory.GroupExtension.Defs
AddGroupExtension.mk.sizeOf_spec : ∀ {N : Type u_1} {E : Type u_2} {G : Type u_3} [inst : AddGroup N] [inst_1 : AddGroup E] [inst_2 : AddGroup G]
  [inst_3 : SizeOf N] [inst_4 : SizeOf E] [inst_5 : SizeOf G] (inl : N →+ E) (rightHom : E →+ G)
  (inl_injective : Function.Injective ⇑inl) (range_inl_eq_ker_rightHom : inl.range = rightHom.ker)
  (rightHom_surjective : Function.Surjective ⇑rightHom),
  sizeOf
      { inl := inl, rightHom := rightHom, inl_injective := inl_injective,
        range_inl_eq_ker_rightHom := range_inl_eq_ker_rightHom, rightHom_surjective := rightHom_surjective } =
    1 + sizeOf inl + sizeOf rightHom + sizeOf range_inl_eq_ker_rightHom
-- Mathlib.Analysis.Calculus.MeanValue
/-- Over the reals or the complexes, a continuously differentiable function is strictly
differentiable.  -/
hasStrictDerivAt_of_hasDerivAt_of_continuousAt : ∀ {𝕜 : Type u_3} [inst : RCLike 𝕜] {G : Type u_4} [inst_1 : NormedAddCommGroup G] [inst_2 : NormedSpace 𝕜 G]
  {f f' : 𝕜 → G} {x : 𝕜},
  (∀ᶠ (y : 𝕜) in nhds x, HasDerivAt f (f' y) y) → ContinuousAt f' x → HasStrictDerivAt f (f' x) x
-- Mathlib.Topology.Semicontinuity.Defs
semicontinuousWithinAt_univ_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {r : α → β → Prop} {x : α},
  SemicontinuousWithinAt r Set.univ x ↔ SemicontinuousAt r x
-- Mathlib.GroupTheory.MonoidLocalization.Maps
/-- Given Localization maps `f : M →+ N, k : P →+ Q` for AddSubmonoids `S, T` respectively, if an
`AddCommMonoid` homomorphism `g : M →+ P` induces a `f.map hy k : N →+ Q`, then for all `z : N`,
`u : Q`, we have `f.map hy k z = u ↔ k (g x) = k (g y) + u` where `x : M, y ∈ S` are such that
`z + f y = f x`.  -/
AddSubmonoid.LocalizationMap.map_spec : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N] {P : Type u_3}
  [inst_2 : AddCommMonoid P] (f : S.LocalizationMap N) {g : M →+ P} {T : AddSubmonoid P} (hy : ∀ (y : ↥S), g ↑y ∈ T)
  {Q : Type u_4} [inst_3 : AddCommMonoid Q] {k : T.LocalizationMap Q} (z : N) (u : Q),
  (f.map hy k) z = u ↔ k (g (f.sec z).1) = k (g ↑(f.sec z).2) + u
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic
_private.Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic.0.CategoryTheory.WithTerminal.id.match_1.splitter : {C : Type u_1} →
  (motive : CategoryTheory.WithTerminal C → Sort u_2) →
    (x : CategoryTheory.WithTerminal C) →
      ((a : C) → motive (CategoryTheory.WithTerminal.of a)) →
        (Unit → motive CategoryTheory.WithTerminal.star) → motive x
-- Mathlib.Analysis.Calculus.VectorField
VectorField.DifferentiableWithinAt.pullbackWithin : ∀ {𝕜 : 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] [CompleteSpace E]
  {f : E → F} {V : F → F} {s : Set E} {t : Set F} {x : E},
  DifferentiableWithinAt 𝕜 V t (f x) →
    ContDiffWithinAt 𝕜 2 f s x →
      (fderivWithin 𝕜 f s x).IsInvertible →
        UniqueDiffOn 𝕜 s → x ∈ s → Set.MapsTo f s t → DifferentiableWithinAt 𝕜 (VectorField.pullbackWithin 𝕜 f V s) s x
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.mk.sizeOf_spec : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : SizeOf R] [inst_6 : SizeOf A] [inst_7 : SizeOf B]
  (toEquiv : A ≃ B) (map_mul' : ∀ (x y : A), toEquiv.toFun (x * y) = toEquiv.toFun x * toEquiv.toFun y)
  (map_add' : ∀ (x y : A), toEquiv.toFun (x + y) = toEquiv.toFun x + toEquiv.toFun y)
  (commutes' : ∀ (r : R), toEquiv.toFun ((algebraMap R A) r) = (algebraMap R B) r),
  sizeOf { toEquiv := toEquiv, map_mul' := map_mul', map_add' := map_add', commutes' := commutes' } = 1 + sizeOf toEquiv
-- Mathlib.Analysis.InnerProductSpace.PiL2
OrthonormalBasis.equiv_self_rfl : ∀ {ι : Type u_1} {𝕜 : Type u_3} [inst : RCLike 𝕜] {E : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : Fintype ι] (b : OrthonormalBasis ι 𝕜 E),
  b.equiv b (Equiv.refl ι) = LinearIsometryEquiv.refl 𝕜 E
-- Mathlib.AlgebraicTopology.DoldKan.Compatibility
AlgebraicTopology.DoldKan.Compatibility.equivalence₂_inverse : ∀ {A : Type u_1} {A' : Type u_2} {B : Type u_3} {B' : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} A'] [inst_2 : CategoryTheory.Category.{v_3, u_3} B]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} B'] {eA : A ≌ A'} (eB : B ≌ B') {e' : A' ≌ B'}
  {F : CategoryTheory.Functor A B'} (hF : eA.functor.comp e'.functor ≅ F),
  (AlgebraicTopology.DoldKan.Compatibility.equivalence₂ eB hF).inverse = eB.functor.comp (e'.inverse.comp eA.inverse)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokenType.typeParameter.sizeOf_spec : sizeOf Lean.Lsp.SemanticTokenType.typeParameter = 1
-- Std.Http.Protocol.H1
/-- Set when a previous `pullBody` call could not make progress in `.readBody`.
Cleared on new input or state reset.
 -/
Std.Http.Protocol.H1.Machine.pullBodyStalled : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Machine dir → Bool
-- Mathlib.LinearAlgebra.Dual.Basis
Module.Basis.eval_range : ∀ {R : Type uR} {M : Type uM} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {ι : Type u_1}
  [Finite ι] (b : Module.Basis ι R M), (Module.Dual.eval R M).range = ⊤
-- Mathlib.Analysis.Normed.Field.Basic
NontriviallyNormedField.toNormedField : {α : Type u_5} → [self : NontriviallyNormedField α] → NormedField α
-- Mathlib.Order.BourbakiWitt
CompleteLattice.ωScottContinuous.iSup : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_3} [inst : OmegaCompletePartialOrder α] [inst_1 : CompleteLattice β]
  {f : ι → α → β},
  (∀ (i : ι), OmegaCompletePartialOrder.ωScottContinuous (f i)) → OmegaCompletePartialOrder.ωScottContinuous (⨆ i, f i)
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.ExprCnstr.rhs : Nat.Internal.Linear.ExprCnstr → Nat.Internal.Linear.Expr
-- Mathlib.Topology.Order.LowerUpperTopology
/-- `ofLower` is the identity function from the `WithLower` of a type.  -/
Topology.WithLower.ofLower : {α : Type u_1} → Topology.WithLower α ≃ α
-- Std.Do.PostCond
_private.Std.Do.PostCond.0.Std.Do.PostShape.args.match_1.eq_1 : ∀ (motive : Std.Do.PostShape → Sort u_2) (h_1 : Unit → motive Std.Do.PostShape.pure)
  (h_2 : (σ : Type u_1) → (s : Std.Do.PostShape) → motive (Std.Do.PostShape.arg σ s))
  (h_3 : (ε : Type u_1) → (s : Std.Do.PostShape) → motive (Std.Do.PostShape.except ε s)),
  (match Std.Do.PostShape.pure with
    | Std.Do.PostShape.pure => h_1 ()
    | Std.Do.PostShape.arg σ s => h_2 σ s
    | Std.Do.PostShape.except ε s => h_3 ε s) =
    h_1 ()
-- Mathlib.Data.Finsupp.Basic
Finsupp.mapDomain_apply_eq_sum : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : DecidableEq β] [inst_1 : AddCommMonoid M] (f : α → β)
  (x : α →₀ M) {a : α}, (Finsupp.mapDomain f x) (f a) = ∑ i ∈ x.support with f i = f a, x i
-- Mathlib.Geometry.Manifold.Riemannian.PathELength
Manifold.pathELength_def : ∀ {E : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_5} [inst_2 : TopologicalSpace H]
  (I : ModelWithCorners ℝ E H) {M : Type u_6} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M]
  [inst_5 : (x : M) → ENorm (TangentSpace I x)] (γ : ℝ → M) (a b : ℝ),
  Manifold.pathELength I γ a b = ∫⁻ (t : ℝ) in Set.Icc a b, ‖(mfderiv% γ t) 1‖ₑ
-- Mathlib.CategoryTheory.Monoidal.End
CategoryTheory.obj_μ_inv_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {M : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} M]
  [inst_2 : CategoryTheory.MonoidalCategory M] (F : CategoryTheory.Functor M (CategoryTheory.Functor C C))
  (m₁ m₂ m₃ : M) (X : C) [inst_3 : F.Monoidal],
  (F.obj m₃).map ((CategoryTheory.Functor.OplaxMonoidal.δ F m₁ m₂).app X) =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Functor.LaxMonoidal.μ F (CategoryTheory.MonoidalCategoryStruct.tensorObj m₁ m₂) m₃).app X)
      (CategoryTheory.CategoryStruct.comp
        ((F.map (CategoryTheory.MonoidalCategoryStruct.associator m₁ m₂ m₃).hom).app X)
        (CategoryTheory.CategoryStruct.comp
          ((CategoryTheory.Functor.OplaxMonoidal.δ F m₁ (CategoryTheory.MonoidalCategoryStruct.tensorObj m₂ m₃)).app X)
          ((CategoryTheory.Functor.OplaxMonoidal.δ F m₂ m₃).app ((F.obj m₁).obj X))))
-- Mathlib.Analysis.InnerProductSpace.LaxMilgram
IsCoercive.continuousLinearEquivOfBilin_apply : ∀ {V : Type u} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : CompleteSpace V]
  {B : V →L[ℝ] V →L[ℝ] ℝ} (coercive : IsCoercive B) (v w : V),
  inner ℝ (coercive.continuousLinearEquivOfBilin v) w = (B v) w
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
/-- One form of **Cramer's rule**. See `Matrix.mulVec_cramer` for a stronger form.  -/
Matrix.det_smul_inv_vecMul_eq_cramer_transpose : ∀ {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α] (A : Matrix n n α)
  (b : n → α), IsUnit A.det → A.det • Matrix.vecMul b A⁻¹ = A.transpose.cramer b
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Matrix.det_one_add_X_smul : ∀ {R : Type u} [inst : CommRing R] {n : Type v} [inst_1 : DecidableEq n] [inst_2 : Fintype n] (M : Matrix n n R),
  (1 + Polynomial.X • M.map ⇑Polynomial.C).det =
    1 + M.trace • Polynomial.X + (1 + Polynomial.X • M.map ⇑Polynomial.C).det.divX.divX * Polynomial.X ^ 2
-- Lean.Meta.Tactic.Util
Lean.MVarId.setTag : Lean.MVarId → Lean.Name → Lean.MetaM Unit
-- Mathlib.MeasureTheory.Function.LpSpace.Indicator
/-- A version of `Set.indicator_add` for `MeasureTheory.indicatorConstLp`  -/
MeasureTheory.indicatorConstLp_add : ∀ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] {s : Set α} {hs : MeasurableSet s} {hμs : μ s ≠ ⊤} {c c' : E},
  MeasureTheory.indicatorConstLp p hs hμs c + MeasureTheory.indicatorConstLp p hs hμs c' =
    MeasureTheory.indicatorConstLp p hs hμs (c + c')
-- Mathlib.Data.Rat.Cast.Order
Rat.cast_le_intCast : ∀ {K : Type u_5} [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] {m : ℚ} {n : ℤ}, ↑m ≤ ↑n ↔ m ≤ ↑n