mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Complex.Schwarz
/-- **Alias** of `Complex.affine_of_mapsTo_ball_of_norm_dslope_eq_div`.

---

Equality case in the **Schwarz Lemma**: in the setup of `norm_dslope_le_div_of_mapsTo_ball`,
if `‖dslope f c z₀‖ = R₂ / R₁` holds at a point in the ball
then the map `f` is affine with slope `dslope f c z₀`.

Note that this lemma requires the codomain to be a strictly convex space.
Indeed, for `E = ℂ × ℂ` there is a counterexample:
the map `f := fun z ↦ (z, z ^ 2)` sends `ball 0 1` to `closedBall 0 1`,
`‖dslope f 0 0‖ = ‖deriv f 0‖ = ‖(1, 0)‖ = 1`, but the map is not an affine map.
 -/
Complex.affine_of_mapsTo_ball_of_exists_norm_dslope_eq_div : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {R₁ R₂ : ℝ} {f : ℂ → E} {c z₀ : ℂ}
  [StrictConvexSpace ℝ E],
  DifferentiableOn ℂ f (Metric.ball c R₁) →
    Set.MapsTo f (Metric.ball c R₁) (Metric.closedBall (f c) R₂) →
      z₀ ∈ Metric.ball c R₁ →
        ‖dslope f c z₀‖ = R₂ / R₁ → Set.EqOn f (fun z => f c + (z - c) • dslope f c z₀) (Metric.ball c R₁)
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.get?_max! : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.isEmpty = false → t.get? t.max! = some t.max!
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.GenericFormat.DateBuilder.S : Std.Time.GenericFormat.DateBuilder✝ → Option Std.Time.Nanosecond.Ordinal
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
MonoidAlgebra.coeff_mapDomainBialgHom_apply : ∀ (R : Type u_1) {M : Type u_8} {N : Type u_9} [inst : CommSemiring R] [inst_1 : Monoid M] [inst_2 : Monoid N]
  (f : M →* N) (a : MonoidAlgebra R M), ((MonoidAlgebra.mapDomainBialgHom R f) a).coeff = Finsupp.mapDomain (⇑f) a.coeff
-- Mathlib.Algebra.Category.Ring.Basic
RingEquiv.toSemiRingCatIso_hom : ∀ {R S : Type u} [inst : Semiring R] [inst_1 : Semiring S] (e : R ≃+* S), e.toSemiRingCatIso.hom = SemiRingCat.ofHom ↑e
-- Mathlib.Algebra.Algebra.Operations
Submodule.smul_induction_on : ∀ {R : Type u} [inst : Semiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Module R A] {M : Type u_1}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module A M] [inst_6 : IsScalarTower R A M]
  {I : Submodule R A} {N : Submodule R M} {p : M → Prop} {x : M},
  x ∈ I • N → (∀ r ∈ I, ∀ n ∈ N, p (r • n)) → (∀ (x y : M), p x → p y → p (x + y)) → p x
-- Lean.Environment
_private.Lean.Environment.0.Lean.Environment.getLocalConstantInfos.go : Bool →
  Lean.AsyncConsts✝ → Array Lean.AsyncConstantInfo → Lean.NameSet → BaseIO (Array Lean.AsyncConstantInfo × Lean.NameSet)
-- Mathlib.Computability.TuringMachine.PostTuringMachine
/-- The semantics of TM1 evaluation.  -/
Turing.TM1.stepAux : {Γ : Type u_1} →
  {Λ : Type u_2} →
    {σ : Type u_3} → [inst : Inhabited Γ] → Turing.TM1.Stmt Γ Λ σ → σ → Turing.Tape Γ → Turing.TM1.Cfg Γ Λ σ
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated
/-- The image of an edge by a morphism of truncated simplicial sets.  -/
SSet.Truncated.Edge.map : {X Y : SSet.Truncated 2} →
  {x₀ x₁ : X.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge._proof_1 })} →
    SSet.Truncated.Edge x₀ x₁ →
      (f : X ⟶ Y) →
        SSet.Truncated.Edge
          ((CategoryTheory.ConcreteCategory.hom
              (f.app (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge._proof_1 })))
            x₀)
          ((CategoryTheory.ConcreteCategory.hom
              (f.app (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge._proof_1 })))
            x₁)
-- Mathlib.Analysis.Complex.Hadamard
/-- `sSup` of `norm` is nonneg applied to the image of `f` on the vertical line `re z = x`  -/
Complex.HadamardThreeLines.sSupNormIm_nonneg : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] (f : ℂ → E) (x : ℝ), 0 ≤ Complex.HadamardThreeLines.sSupNormIm f x
-- Mathlib.Topology.MetricSpace.DilationEquiv
DilationEquiv.ratio_toDilation : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] (e : X ≃ᵈ Y),
  Dilation.ratio e.toDilation = Dilation.ratio e
-- Init.Data.Sum.Lemmas
Sum.getLeft_eq_iff : ∀ {α : Type u_1} {a : α} {β : Type u_2} {x : α ⊕ β} (h : x.isLeft = true), x.getLeft h = a ↔ x = Sum.inl a
-- Lean.DocString.Types
Lean.Doc.Block.brecOn_7.go : {i : Type u} →
  {b : Type v} →
    {motive_1 : Lean.Doc.Block i b → Sort u_1} →
      {motive_2 : Array (Lean.Doc.ListItem (Lean.Doc.Block i b)) → Sort u_1} →
        {motive_3 : Array (Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b)) → Sort u_1} →
          {motive_4 : Array (Lean.Doc.Block i b) → Sort u_1} →
            {motive_5 : List (Lean.Doc.ListItem (Lean.Doc.Block i b)) → Sort u_1} →
              {motive_6 : List (Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b)) → Sort u_1} →
                {motive_7 : List (Lean.Doc.Block i b) → Sort u_1} →
                  {motive_8 : Lean.Doc.ListItem (Lean.Doc.Block i b) → Sort u_1} →
                    {motive_9 : Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b) → Sort u_1} →
                      (t : Lean.Doc.ListItem (Lean.Doc.Block i b)) →
                        ((t : Lean.Doc.Block i b) → t.below → motive_1 t) →
                          ((t : Array (Lean.Doc.ListItem (Lean.Doc.Block i b))) →
                              Lean.Doc.Block.below_1 t → motive_2 t) →
                            ((t : Array (Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b))) →
                                Lean.Doc.Block.below_2 t → motive_3 t) →
                              ((t : Array (Lean.Doc.Block i b)) → Lean.Doc.Block.below_3 t → motive_4 t) →
                                ((t : List (Lean.Doc.ListItem (Lean.Doc.Block i b))) →
                                    Lean.Doc.Block.below_4 t → motive_5 t) →
                                  ((t : List (Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b))) →
                                      Lean.Doc.Block.below_5 t → motive_6 t) →
                                    ((t : List (Lean.Doc.Block i b)) → Lean.Doc.Block.below_6 t → motive_7 t) →
                                      ((t : Lean.Doc.ListItem (Lean.Doc.Block i b)) →
                                          Lean.Doc.Block.below_7 t → motive_8 t) →
                                        ((t : Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b)) →
                                            Lean.Doc.Block.below_8 t → motive_9 t) →
                                          motive_8 t ×' Lean.Doc.Block.below_7 t
-- Mathlib.MeasureTheory.VectorMeasure.Variation.Basic
/-- For `μ : VectorMeasure X ℝ≥0∞` and measurable `s`, the supremum over Finpartitions of
`⟨s, hs⟩ : Subtype MeasurableSet` of the sum of `μ` over parts equals `μ s`.  -/
MeasureTheory.VectorMeasure.iSup_sum_finpartition_parts : ∀ {X : Type u_1} {mX : MeasurableSpace X} (μ : MeasureTheory.VectorMeasure X ENNReal) {s : Set X}
  (hs : MeasurableSet s), ⨆ P, ∑ p ∈ P.parts, μ ↑p = μ s
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey!_alter_self : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited α] {k : α} {f : Option β → Option β},
  (m.alter k f).getKey! k = if (f m[k]?).isSome = true then k else default
-- Mathlib.Combinatorics.Nullstellensatz
/-- The **Combinatorial Nullstellensatz**.

If `f` vanishes at every point `x : σ → R` such that `x s ∈ S s` for all `s`,
then it can be written as a linear combination
`f = linearCombination (MvPolynomial σ R) (fun i ↦ (∏ r ∈ S i, (X i - C r))) h`,
for some `h : σ →₀ MvPolynomial σ R` such that
`((∏ r ∈ S s, (X i - C r)) * h i).totalDegree ≤ f.totalDegree` for all `s`.

[Alon_1999], theorem 1.  -/
MvPolynomial.combinatorial_nullstellensatz_exists_linearCombination : ∀ {R : Type u_1} [inst : CommRing R] {σ : Type u_2} [Finite σ] [IsDomain R] (S : σ → Finset R),
  (∀ (i : σ), (S i).Nonempty) →
    ∀ (f : MvPolynomial σ R),
      (∀ (x : σ → R), (∀ (i : σ), x i ∈ S i) → (MvPolynomial.eval x) f = 0) →
        ∃ h,
          (∀ (i : σ), ((∏ s ∈ S i, (MvPolynomial.X i - MvPolynomial.C s)) * h i).totalDegree ≤ f.totalDegree) ∧
            f =
              (Finsupp.linearCombination (MvPolynomial σ R) fun i => ∏ r ∈ S i, (MvPolynomial.X i - MvPolynomial.C r)) h
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalSubalgebra.mem_toSubmodule : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  (S : NonUnitalSubalgebra R A) {x : A}, x ∈ S.toSubmodule ↔ x ∈ S
-- Batteries.Data.MLList.Basic
/-- Run a lazy list in a `StateRefT'` monad on some initial state.  -/
MLList.runStateRef : {m : Type → Type} → {ω σ α : Type} → [Monad m] → [MonadLiftT (ST ω) m] → MLList (StateRefT' ω σ m) α → σ → MLList m α
-- Mathlib.Topology.EMetricSpace.BoundedVariation
/-- If a function has bounded variation, then the variation on small closed-open
intervals to the left of any point tends to `0`.  -/
BoundedVariationOn.tendsto_eVariationOn_Ico_zero : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] [inst_2 : TopologicalSpace α]
  [OrderTopology α] {f : α → E} {s : Set α},
  BoundedVariationOn f s →
    ∀ (x : α), Filter.Tendsto (fun y => eVariationOn f (s ∩ Set.Ico y x)) (nhdsWithin x s) (nhds 0)
-- Mathlib.RingTheory.Polynomial.Resultant.Basic
Polynomial.resultant_C_right : ∀ {R : Type u_1} [inst : CommRing R] (f : Polynomial R) (m n : ℕ) (r : R),
  f.resultant (Polynomial.C r) m n = f.coeff m ^ n * r ^ m
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.funMap_sumInl : ∀ {L₁ : FirstOrder.Language} {L₂ : FirstOrder.Language} {S : Type u_3} [inst : L₁.Structure S] [inst_1 : L₂.Structure S]
  {n : ℕ} (f : L₁.Functions n),
  FirstOrder.Language.Structure.funMap (Sum.inl f) = FirstOrder.Language.Structure.funMap f
-- Mathlib.GroupTheory.Coset.Defs
QuotientGroup.mk_mul_of_mem : ∀ {α : Type u_1} [inst : Group α] {s : Subgroup α} {b : α} (a : α), b ∈ s → ↑(a * b) = ↑a
-- Mathlib.Data.Stream.Init
Stream'.identity : ∀ {α : Type u} (s : Stream' α), Stream'.pure id ⊛ s = s
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
/-- For any `x ∈ posSubmonoid R`, the trivial valuation `1 : Valuation R Γ` sends `x` to `1`.
In fact, this is true for any `x ≠ 0`. This lemma is a special case useful for shorthand of
`x ∈ posSubmonoid R → x ≠ 0`.  -/
ValuativeRel.one_apply_posSubmonoid : ∀ {R : Type u_2} {Γ : Type u_3} [inst : Ring R] [inst_1 : ValuativeRel R] [inst_2 : LinearOrderedCommGroupWithZero Γ]
  [inst_3 : Nontrivial R] [inst_4 : NoZeroDivisors R] [inst_5 : DecidablePred fun x => x = 0]
  (x : ↥(ValuativeRel.posSubmonoid R)), 1 ↑x = 1
-- Mathlib.NumberTheory.FLT.Three
/-- Given `(S : Solution)`, we have that `λ ^ 2` does not divide `S.a + η ^ 2 * S.b`.  -/
_private.Mathlib.NumberTheory.FLT.Three.0.FermatLastTheoremForThreeGen.Solution.lambda_sq_not_dvd_a_add_eta_sq_mul_b : ∀ {K : Type u_1} [inst : Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3} (S : FermatLastTheoremForThreeGen.Solution✝ hζ)
  [inst_1 : NumberField K] [IsCyclotomicExtension {3} ℚ K],
  ¬(hζ.toInteger - 1) ^ 2 ∣
      FermatLastTheoremForThreeGen.Solution'.a✝ (FermatLastTheoremForThreeGen.Solution.toSolution'✝ S) +
        ↑⋯.unit ^ 2 * FermatLastTheoremForThreeGen.Solution'.b✝ (FermatLastTheoremForThreeGen.Solution.toSolution'✝ S)
-- Init.Data.SInt.Lemmas
Int64.toInt16_neg : ∀ (x : Int64), (-x).toInt16 = -x.toInt16
-- Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
/-- **Alias** of `AlgebraicGeometry.Scheme.Hom.formallyUnramified_appLE`.

---

**Alias** of `AlgebraicGeometry.FormallyUnramified.formallyUnramified_appLE`. -/
AlgebraicGeometry.FormallyUnramified.formallyUnramified_of_affine_subset : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [self : AlgebraicGeometry.FormallyUnramified f] {U : Y.Opens},
  AlgebraicGeometry.IsAffineOpen U →
    ∀ {V : X.Opens},
      AlgebraicGeometry.IsAffineOpen V →
        ∀ (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U),
          (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appLE f U V e)).FormallyUnramified
-- Mathlib.Combinatorics.HalesJewett
Combinatorics.Subspace.ext_iff : ∀ {η : Type u_5} {α : Type u_6} {ι : Type u_7} {x y : Combinatorics.Subspace η α ι}, x = y ↔ x.idxFun = y.idxFun
-- Lean.Server.GoTo
Lean.Server.locationLinksFromOptionInfo : Lean.Elab.OptionInfo → Lean.Server.GoToM (Array Lean.Lsp.LeanLocationLink)
-- Mathlib.Data.Finset.Update
Function.updateFinset_empty : ∀ {ι : Type u_1} {π : ι → Sort u_2} {x : (i : ι) → π i} [inst : DecidableEq ι] {y : (i : ↥∅) → π ↑i},
  Function.updateFinset x ∅ y = x
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.beqModel_iff_perm : ∀ {α : Type u} {β : Type v} [inst : BEq α] [LawfulBEq α] [inst_2 : BEq β] [LawfulBEq β] {l₁ l₂ : List ((_ : α) × β)},
  Std.Internal.List.DistinctKeys l₁ →
    Std.Internal.List.DistinctKeys l₂ → (Std.Internal.List.Const.beqModel l₁ l₂ = true ↔ l₁.Perm l₂)
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnModule.instSMul : {Γ : Type u_1} →
  {Γ' : Type u_2} →
    {R : Type u_3} →
      {V : Type u_5} →
        [inst : PartialOrder Γ] →
          [inst_1 : SMul R V] →
            [inst_2 : PartialOrder Γ'] →
              [inst_3 : VAdd Γ Γ'] →
                [IsOrderedCancelVAdd Γ Γ'] →
                  [inst_5 : Zero R] → [inst_6 : AddCommMonoid V] → SMul (HahnSeries Γ R) (HahnModule Γ' R V)
-- Mathlib.CategoryTheory.Bicategory.Span.Basic
CategoryTheory.Span.mkIso.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {Wₗ Wᵣ : CategoryTheory.MorphismProperty C} {c c' : C}
  {S S' : CategoryTheory.Span Wₗ Wᵣ c c'} (e e_1 : S.apex ≅ S'.apex) (e_e : e = e_1)
  (hₗ : CategoryTheory.CategoryStruct.comp e.hom S'.l = S.l) (hᵣ : CategoryTheory.CategoryStruct.comp e.hom S'.r = S.r),
  CategoryTheory.Span.mkIso e hₗ hᵣ = CategoryTheory.Span.mkIso e_1 ⋯ ⋯
-- Mathlib.CategoryTheory.Sites.Point.Conservative
CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.jointly_reflect_ofArrows_mem_of_small : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  {P : CategoryTheory.ObjectProperty J.Point} [CategoryTheory.LocallySmall.{w, v, u} C]
  [CategoryTheory.HasSheafify J (Type w)] [J.WEqualsLocallyBijective (Type w)],
  P.IsConservativeFamilyOfPoints →
    ∀ [CategoryTheory.ObjectProperty.Small.{w, max u w, max (max u v) (w + 1)} P] {X : C} {ι : Type u_1} {U : ι → C}
      (f : (i : ι) → U i ⟶ X),
      CategoryTheory.Sieve.ofArrows U f ∈ J X ↔
        ∀ (Φ : P.FullSubcategory) (x : Φ.obj.fiber.obj X),
          ∃ i y, (CategoryTheory.ConcreteCategory.hom (Φ.obj.fiber.map (f i))) y = x
-- Mathlib.CategoryTheory.Preadditive.Opposite
CategoryTheory.unop_add : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {X Y : Cᵒᵖ}
  (f g : X ⟶ Y), (f + g).unop = f.unop + g.unop
-- Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
MeasurableSpace.countablyGeneratedAtom.eq_1 : ∀ (α : Type u_3) [inst : MeasurableSpace α] [inst_1 : MeasurableSpace.CountablyGenerated α] (p : ℕ → Prop),
  MeasurableSpace.countablyGeneratedAtom α p =
    ⋂ n, if p n then MeasurableSpace.natGeneratingSequence α n else (MeasurableSpace.natGeneratingSequence α n)ᶜ
-- Mathlib.CategoryTheory.Generator.Basic
/-- The projection morphisms from `∏ᶜ (P.productToFamily X)`.  -/
CategoryTheory.ObjectProperty.πProductTo : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (P : CategoryTheory.ObjectProperty C) →
      {X : C} →
        [inst_1 : CategoryTheory.Limits.HasProduct (P.productToFamily X)] →
          {Y : C} → (X ⟶ Y) → P Y → (∏ᶜ P.productToFamily X ⟶ Y)
-- Init.Data.UInt.Lemmas
UInt32.toUInt16_ofFin : ∀ (n : Fin UInt32.size), (UInt32.ofFin n).toUInt16 = UInt16.ofNat ↑n
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.image_mul_right : ∀ {α : Type u_2} [inst : Group α] {t : Set α} {b : α}, (fun x => x * b) '' t = (fun x => x * b⁻¹) ⁻¹' t
-- Mathlib.Logic.Equiv.Defs
Equiv.exists_congr : ∀ {α : Sort u} {β : Sort v} {p : α → Prop} {q : β → Prop} (e : α ≃ β),
  (∀ (a : α), p a ↔ q (e a)) → ((∃ a, p a) ↔ ∃ b, q b)
-- Init.Prelude
/-- Executes an `EStateM` with the initial state `s` for the returned value `α`, discarding the final
state. Returns `none` if an unhandled exception was thrown.
 -/
EStateM.run' : {ε σ α : Type u} → EStateM ε σ α → σ → Option α
-- Mathlib.Probability.Process.LocalProperty
_private.Mathlib.Probability.Process.LocalProperty.0.ProbabilityTheory.mkStrictMonoAux.eq_2 : ∀ (x : ℕ → ℕ) (n : ℕ),
  ProbabilityTheory.mkStrictMonoAux✝ x n.succ = max (x (n + 1)) (ProbabilityTheory.mkStrictMonoAux✝ x n) + 1
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Coalgebra.equivOfNatIso_unitIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor C C} (α : F ≅ G),
  (CategoryTheory.Endofunctor.Coalgebra.equivOfNatIso α).unitIso =
    CategoryTheory.Endofunctor.Coalgebra.functorOfNatTransId.symm ≪≫
      CategoryTheory.Endofunctor.Coalgebra.functorOfNatTransEq ⋯ ≪≫
        CategoryTheory.Endofunctor.Coalgebra.functorOfNatTransComp α.hom α.inv
-- Mathlib.Data.List.Basic
/-- The images of disjoint lists under a partially defined map are disjoint  -/
List.disjoint_pmap : ∀ {α : Type u} {β : Type v} {p : α → Prop} {f : (a : α) → p a → β} {s t : List α} (hs : ∀ a ∈ s, p a)
  (ht : ∀ a ∈ t, p a),
  (∀ (a a' : α) (ha : p a) (ha' : p a'), f a ha = f a' ha' → a = a') →
    s.Disjoint t → (List.pmap f s hs).Disjoint (List.pmap f t ht)
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
MeasureTheory.LocallyIntegrableOn.aestronglyMeasurable : ∀ {X : Type u_1} {ε : Type u_3} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] [inst_2 : TopologicalSpace ε]
  [inst_3 : ContinuousENorm ε] {f : X → ε} {μ : MeasureTheory.Measure X} {s : Set X}
  [TopologicalSpace.PseudoMetrizableSpace ε] [SecondCountableTopology X],
  MeasureTheory.LocallyIntegrableOn f s μ → MeasureTheory.AEStronglyMeasurable f (μ.restrict s)
-- Mathlib.Tactic.FunProp.Types
/-- function property name  -/
Mathlib.Meta.FunProp.GeneralTheorem.funPropName : Mathlib.Meta.FunProp.GeneralTheorem → Lean.Name
-- Mathlib.Tactic.Linarith.Frontend
Mathlib.Tactic.Linarith.LinarithConfig.mk : Lean.Elab.Tactic.TacticM Unit →
  Bool →
    Lean.Meta.TransparencyMode →
      Bool →
        Bool →
          Bool →
            List Mathlib.Tactic.Linarith.GlobalBranchingPreprocessor →
              Mathlib.Tactic.Linarith.CertificateOracle → Mathlib.Tactic.Linarith.LinarithConfig
-- Lean.Expr
_private.Lean.Expr.0.Lean.intMulFn : Lean.Expr
-- Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
curveIntegral_neg : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {a b : E} {ω : E → E →L[𝕜] F}
  {γ : Path a b}, curveIntegral (-ω) γ = -∫ᶜ (x : E) in γ, ω x
-- Mathlib.Tactic.CategoryTheory.MonoidalComp
CategoryTheory.MonoidalCoherence.refl : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → (X : C) → CategoryTheory.MonoidalCoherence X X
-- Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
AddSubgroup.zmultiples_neg : ∀ {G : Type u_1} [inst : AddGroup G] {g : G}, AddSubgroup.zmultiples (-g) = AddSubgroup.zmultiples g
-- Mathlib.CategoryTheory.Idempotents.Karoubi
CategoryTheory.Idempotents.Karoubi.inclusionHom_apply : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (P Q : CategoryTheory.Idempotents.Karoubi C) (f : P ⟶ Q), (P.inclusionHom Q) f = f.f
-- Mathlib.Data.PNat.Basic
PNat.lt_succ_self : ∀ (a : ℕ+), a < (↑a).succPNat
-- Std.Data.Iterators.Lemmas.Combinators.Zip
Std.Iter.Intermediate.zip.eq_1 : ∀ {α₁ α₂ β₁ β₂ : Type w} [inst : Std.Iterator α₁ Id β₁] (it₁ : Std.Iter β₁)
  (memo : Option { out // ∃ it, it.toIterM.IsPlausibleOutput out }) (it₂ : Std.Iter β₂),
  Std.Iter.Intermediate.zip it₁ memo it₂ =
    (Std.IterM.Intermediate.zip it₁.toIterM ((fun x => ⟨↑x, ⋯⟩) <$> memo) it₂.toIterM).toIter
-- Mathlib.Algebra.Category.Ring.Under.Limits
CommRingCat.Under.instPreservesFiniteLimitsUnderTensorProdOfFlatCarrier : ∀ {R S : CommRingCat} [inst : Algebra ↑R ↑S] [Module.Flat ↑R ↑S],
  CategoryTheory.Limits.PreservesFiniteLimits (R.tensorProd S)
-- Mathlib.Data.Ordmap.Invariants
Ordnode.dual_node' : ∀ {α : Type u_1} (l : Ordnode α) (x : α) (r : Ordnode α), (l.node' x r).dual = r.dual.node' x l.dual
-- Mathlib.Topology.Algebra.ProperAction.Basic
/-- Proper group action in the sense of Bourbaki:
the map `G × X → X × X` is a proper map (see `IsProperMap`).  -/
ProperSMul : (G : Type u_1) →
  (X : Type u_2) → [TopologicalSpace G] → [TopologicalSpace X] → [inst : Group G] → [MulAction G X] → Prop
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.cokernelSequenceCyclesE_g : ∀ {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 j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.cokernelSequenceCyclesE._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.cokernelSequenceCyclesE._auto_3),
  (X.cokernelSequenceCyclesE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).g = X.πE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂
-- Mathlib.Data.Num.Bitwise
/-- `SNum.cAdd n m a` is `n + m + a` (where `a` should be read as either 0 or 1).
`a` represents a carry bit.  -/
SNum.cAdd : SNum → SNum → Bool → SNum
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
exists_square_le : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : LinearOrder α] [MulLeftStrictMono α] (a : α), ∃ b, b * b ≤ a
-- Mathlib.AlgebraicGeometry.Modules.Tilde
AlgebraicGeometry.Scheme.Modules.restrict.congr_simp : ∀ {X Y : AlgebraicGeometry.Scheme} (M M_1 : Y.Modules),
  M = M_1 →
    ∀ (f f_1 : X ⟶ Y) (e_f : f = f_1) [inst : AlgebraicGeometry.IsOpenImmersion f], M.restrict f = M_1.restrict f_1
-- Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.Datatypes
Mathlib.Tactic.Linarith.SimplexAlgorithm.instUsableInSimplexAlgorithmSparseMatrix : Mathlib.Tactic.Linarith.SimplexAlgorithm.UsableInSimplexAlgorithm Mathlib.Tactic.Linarith.SimplexAlgorithm.SparseMatrix
-- Mathlib.Data.Finset.Card
Finset.card_sdiff : ∀ {α : Type u_1} {s t : Finset α} [inst : DecidableEq α], (t \ s).card = t.card - (s ∩ t).card
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime
CategoryTheory.Pseudofunctor.DescentData'.pullHom_pullHom' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} {ι : Type t} {S : C}
  {X : ι → C} {f : (i : ι) → X i ⟶ S} {sq : (i j : ι) → CategoryTheory.Limits.ChosenPullback (f i) (f j)}
  {obj obj' : (i : ι) → ↑(F.obj { as := Opposite.op (X i) })}
  (hom :
    (i j : ι) →
      (F.map (sq i j).p₁.op.toLoc).toFunctor.obj (obj i) ⟶ (F.map (sq i j).p₂.op.toLoc).toFunctor.obj (obj' j))
  ⦃Y Y' : C⦄ (g : Y' ⟶ Y) (q : Y ⟶ S) (q' : Y' ⟶ S) ⦃i₁ i₂ : ι⦄ (f₁ : Y ⟶ X i₁) (f₂ : Y ⟶ X i₂) (gf₁ : Y' ⟶ X i₁)
  (gf₂ : Y' ⟶ X i₂)
  (hq :
    autoParam (CategoryTheory.CategoryStruct.comp g q = q')
      CategoryTheory.Pseudofunctor.DescentData'.pullHom_pullHom'._auto_1)
  (hf₁ :
    autoParam (CategoryTheory.CategoryStruct.comp f₁ (f i₁) = q)
      CategoryTheory.Pseudofunctor.DescentData'.pullHom_pullHom'._auto_3)
  (hf₂ :
    autoParam (CategoryTheory.CategoryStruct.comp f₂ (f i₂) = q)
      CategoryTheory.Pseudofunctor.DescentData'.pullHom_pullHom'._auto_5)
  (hgf₁ :
    autoParam (CategoryTheory.CategoryStruct.comp g f₁ = gf₁)
      CategoryTheory.Pseudofunctor.DescentData'.pullHom_pullHom'._auto_7)
  (hgf₂ :
    autoParam (CategoryTheory.CategoryStruct.comp g f₂ = gf₂)
      CategoryTheory.Pseudofunctor.DescentData'.pullHom_pullHom'._auto_9),
  CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.pullHom
      (CategoryTheory.Pseudofunctor.DescentData'.pullHom' hom q f₁ f₂ hf₁ hf₂) g gf₁ gf₂ ⋯ ⋯ =
    CategoryTheory.Pseudofunctor.DescentData'.pullHom' hom q' gf₁ gf₂ ⋯ ⋯