mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
/-- **Fundamental theorem of calculus-1**, local version for any measure.

Let filters `l` and `l'` be related by `[intervalIntegral.FTCFilter a l l']`; let `μ` be a locally
finite measure.  If `f` has a finite limit `c` at `l' ⊓ ae μ`, then
`∫ x in u..v, f x ∂μ = ∫ x in u..v, c ∂μ + o(∫ x in u..v, 1 ∂μ)` as both `u` and `v` tend to `l`.

See also `measure_integral_sub_linear_isLittleO_of_tendsto_ae'` for a version that also works, e.g.,
for `l = l' = Filter.atTop`.

We use integrals of constants instead of measures because this way it is easier to formulate
a statement that works in both cases `u ≤ v` and `v ≤ u`.  -/
intervalIntegral.measure_integral_sub_linear_isLittleO_of_tendsto_ae : ∀ {ι : Type u_1} {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E} {a : ℝ} {c : E}
  {l l' : Filter ℝ} {lt : Filter ι} {μ : MeasureTheory.Measure ℝ} {u v : ι → ℝ} [MeasureTheory.IsLocallyFiniteMeasure μ]
  [intervalIntegral.FTCFilter a l l'],
  StronglyMeasurableAtFilter f l' μ →
    Filter.Tendsto f (l' ⊓ MeasureTheory.ae μ) (nhds c) →
      Filter.Tendsto u lt l →
        Filter.Tendsto v lt l →
          (fun t => ∫ (x : ℝ) in u t..v t, f x ∂μ - ∫ (x : ℝ) in u t..v t, c ∂μ) =o[lt] fun t =>
            ∫ (x : ℝ) in u t..v t, 1 ∂μ
-- Mathlib.RingTheory.FractionalIdeal.Basic
/-- `FractionalIdeal.coeToSubmodule` as a bundled `RingHom`.  -/
FractionalIdeal.coeSubmoduleHom : {R : Type u_1} →
  [inst : CommRing R] →
    (S : Submonoid R) →
      (P : Type u_2) → [inst_1 : CommRing P] → [inst_2 : Algebra R P] → FractionalIdeal S P →+* Submodule R P
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.CoreMonoidal.ofOplaxMonoidal_μIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.OplaxMonoidal]
  [inst_5 : CategoryTheory.IsIso (CategoryTheory.Functor.OplaxMonoidal.η F)]
  [inst_6 : ∀ (X Y : C), CategoryTheory.IsIso (CategoryTheory.Functor.OplaxMonoidal.δ F X Y)] (X Y : C),
  (CategoryTheory.Functor.CoreMonoidal.ofOplaxMonoidal F).μIso X Y =
    (CategoryTheory.asIso (CategoryTheory.Functor.OplaxMonoidal.δ F X Y)).symm
-- Mathlib.AlgebraicGeometry.SpreadingOut
/-- Suppose `X` is a scheme, `x : X` such that the germ map at `x` is (locally) injective,
and `U` is a neighborhood of `x`.
Given a commutative diagram of `CommRingCat`
```
R ⟶ Γ(X, U)
↓    ↓
A ⟶ 𝒪_{X, x}
```
such that `R` is of finite type over `A`, we may lift `A ⟶ 𝒪_{X, x}` to some `A ⟶ Γ(X, V)`.
 -/
AlgebraicGeometry.exists_lift_of_germInjective : ∀ {X : AlgebraicGeometry.Scheme} {R A : CommRingCat} {x : ↥X} [X.IsGermInjectiveAt x] {U : X.Opens} (hxU : x ∈ U)
  (φ : A ⟶ X.presheaf.stalk x) (φRA : R ⟶ A) (φRX : R ⟶ X.presheaf.obj (Opposite.op U)),
  (CommRingCat.Hom.hom φRA).FiniteType →
    CategoryTheory.CategoryStruct.comp φRA φ = CategoryTheory.CategoryStruct.comp φRX (X.presheaf.germ U x hxU) →
      ∃ V,
        ∃ (hxV : x ∈ V),
          ∃ φ',
            ∃ (i : V ≤ U),
              AlgebraicGeometry.IsAffineOpen V ∧
                φ = CategoryTheory.CategoryStruct.comp φ' (X.presheaf.germ V x hxV) ∧
                  CategoryTheory.CategoryStruct.comp φRX (X.presheaf.map i.hom.op) =
                    CategoryTheory.CategoryStruct.comp φRA φ'
-- Mathlib.Tactic.Algebra.Basic
/-- Create a new cache for `A` by doing the necessary instance searches.  -/
Mathlib.Tactic.Algebra.mkCache : {u : Lean.Level} → {A : Q(Type u)} → (sA : Q(CommSemiring «$A»)) → Lean.MetaM (Mathlib.Tactic.Algebra.Cache sA)
-- Mathlib.Probability.Kernel.Composition.MeasureComp
MeasureTheory.Measure.snd_compProd : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (μ : MeasureTheory.Measure α)
  [MeasureTheory.SFinite μ] (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsSFiniteKernel κ],
  (μ.compProd κ).snd = μ.bind ⇑κ
-- Qq.ForLean.ReduceEval
Lean.Meta.throwFailedToEval : {α : Type} → Lean.Expr → Lean.MetaM α
-- Std.Data.DTreeMap.Raw.WF
Std.DTreeMap.Raw.WF.constModify : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {a : α} {f : β → β} {t : Std.DTreeMap.Raw α (fun x => β) cmp},
  t.WF → (Std.DTreeMap.Raw.Const.modify t a f).WF
-- Mathlib.RingTheory.Localization.Basic
IsLocalization.algEquiv_symm_mk' : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [inst_3 : IsLocalization M S] {Q : Type u_4} [inst_4 : CommSemiring Q] [inst_5 : Algebra R Q]
  [inst_6 : IsLocalization M Q] (x : R) (y : ↥M),
  (IsLocalization.algEquiv M S Q).symm (IsLocalization.mk' Q x y) = IsLocalization.mk' S x y
-- Init.Grind.AC
Lean.Grind.AC.Seq.denote_eraseDup : ∀ {α : Sort u_1} (ctx : Lean.Grind.AC.Context α) {inst₁ : Std.Associative ctx.op} {inst₂ : Std.IdempotentOp ctx.op}
  (s : Lean.Grind.AC.Seq), Lean.Grind.AC.Seq.denote ctx s.eraseDup = Lean.Grind.AC.Seq.denote ctx s
-- Mathlib.Analysis.InnerProductSpace.Completion
UniformSpace.Completion.continuous_inner : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E],
  Continuous (Function.uncurry (inner 𝕜))
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.Equiv.filter : ∀ {α₁ α₂ β : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : LawfulMonad m] [inst_2 : Std.Iterator α₁ m β]
  [inst_3 : Std.Iterator α₂ m β] {f : β → Bool} {ita : Std.IterM m β} {itb : Std.IterM m β},
  ita.Equiv itb → (Std.IterM.filter f ita).Equiv (Std.IterM.filter f itb)
-- Mathlib.ModelTheory.Substructures
/-- If two `L.Hom`s are equal on a set, then they are equal on its substructure closure.  -/
FirstOrder.Language.Hom.eqOn_closure : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [inst : L.Structure M] [inst_1 : L.Structure N]
  {f g : L.Hom M N} {s : Set M},
  Set.EqOn (⇑f) (⇑g) s → Set.EqOn ⇑f ⇑g ↑((FirstOrder.Language.Substructure.closure L).toFun s)
-- Lean.Meta.DiscrTree.Main
/-- Inserts a value into a discrimination tree,
but only if its key is not of the form `#[*]` or `#[=, *, *, *]`.
 -/
Lean.Meta.DiscrTree.insertIfSpecific : {α : Type} → [BEq α] → Lean.Meta.DiscrTree α → Lean.Expr → α → optParam Bool false → Lean.MetaM (Lean.Meta.DiscrTree α)
-- Mathlib.ModelTheory.Complexity
FirstOrder.Language.BoundedFormula.IsPrenex.castLE : ∀ {L : FirstOrder.Language} {α : Type u'} {l : ℕ} {φ : L.BoundedFormula α l},
  φ.IsPrenex → ∀ {n : ℕ} {h : l ≤ n}, (FirstOrder.Language.BoundedFormula.castLE h φ).IsPrenex
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.NatTrans.op_whiskerLeft_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} {E : Type u_1} [inst_2 : CategoryTheory.Category.{v_1, u_1} E]
  {H : CategoryTheory.Functor E C} (α : F ⟶ G) {Z : CategoryTheory.Functor Eᵒᵖ Dᵒᵖ} (h : (H.comp F).op ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.NatTrans.op (H.whiskerLeft α)) h =
    CategoryTheory.CategoryStruct.comp (H.opComp G).hom
      (CategoryTheory.CategoryStruct.comp (H.op.whiskerLeft (CategoryTheory.NatTrans.op α))
        (CategoryTheory.CategoryStruct.comp (H.opComp F).inv h))
-- Mathlib.Topology.Constructions
Pi.topologicalSpace.eq_1 : ∀ {ι : Type u_5} {Y : ι → Type v} [t₂ : (i : ι) → TopologicalSpace (Y i)],
  Pi.topologicalSpace = ⨅ i, TopologicalSpace.induced (fun f => f i) (t₂ i)
-- Mathlib.SetTheory.Cardinal.Regular
Cardinal.isRegular_aleph_one : (Cardinal.aleph 1).IsRegular
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getD_toList_roc : ∀ {m n i fallback : ℕ}, (m<...=n).toList.getD i fallback = if i < n - m then m + 1 + i else fallback
-- Mathlib.NumberTheory.Padics.PadicNumbers
Padic.coe_div : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)] {x y : ℚ}, ↑(x / y) = ↑x / ↑y
-- Init.Data.Int.Linear
_private.Init.Data.Int.Linear.0.Int.Internal.Linear.mul_le_zero_iff : ∀ (a k : ℤ), k > 0 → (k * a ≤ 0 ↔ a ≤ 0)
-- Mathlib.LinearAlgebra.TensorProduct.Map
TensorProduct.map_zero_left : ∀ {R : Type u_1} {R₂ : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7}
  {N : Type u_8} {M₂ : Type u_12} {N₂ : Type u_14} [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid N]
  [inst_4 : AddCommMonoid M₂] [inst_5 : AddCommMonoid N₂] [inst_6 : Module R M] [inst_7 : Module R N]
  [inst_8 : Module R₂ M₂] [inst_9 : Module R₂ N₂] (g : N →ₛₗ[σ₁₂] N₂), TensorProduct.map 0 g = 0
-- Std.Sat.AIG.CNF
/-- State extension are `Cache.IsExtensionBy` for now.
 -/
_private.Std.Sat.AIG.CNF.0.Std.Sat.AIG.toCNF.State.IsExtensionBy : {aig : Std.Sat.AIG ℕ} →
  Std.Sat.AIG.toCNF.State✝ aig → Std.Sat.AIG.toCNF.State✝ aig → (new : ℕ) → new < aig.decls.size → Prop
-- Mathlib.Algebra.DirectSum.Ring
/-- The `CommRing` derived from `GCommSemiring A`.  -/
DirectSum.commRing : {ι : Type u_1} →
  [DecidableEq ι] →
    (A : ι → Type u_2) →
      [inst : (i : ι) → AddCommGroup (A i)] →
        [inst_1 : AddCommMonoid ι] → [DirectSum.GCommRing A] → CommRing (DirectSum ι fun i => A i)
-- Mathlib.Order.Filter.Tendsto
Filter.tendsto_comap_iff : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {g : β → γ} {a : Filter α} {c : Filter γ},
  Filter.Tendsto f a (Filter.comap g c) ↔ Filter.Tendsto (g ∘ f) a c
-- Mathlib.Analysis.SpecialFunctions.Arsinh
Real.cosh_arsinh : ∀ (x : ℝ), Real.cosh (Real.arsinh x) = √(1 + x ^ 2)
-- Mathlib.Data.Real.Basic
Real.instIsOrderedRing : IsOrderedRing ℝ
-- Mathlib.AlgebraicGeometry.RelativeGluing
/-- The structure map from the colimit of the `Xᵢ` to `S`.  -/
AlgebraicGeometry.Scheme.Cover.RelativeGluingData.toBase : {S : AlgebraicGeometry.Scheme} →
  {𝒰 : S.OpenCover} →
    [inst : CategoryTheory.Category.{u_2, u_1} 𝒰.I₀] →
      [inst_1 : AlgebraicGeometry.Scheme.Cover.LocallyDirected 𝒰] →
        (d : AlgebraicGeometry.Scheme.Cover.RelativeGluingData 𝒰) →
          [inst_2 : Small.{u, u_1} 𝒰.I₀] → [inst_3 : Quiver.IsThin 𝒰.I₀] → d.glued ⟶ S
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
/-- `SummableUniformlyOn f s` means that there is some infinite sum to
which `f` converges uniformly on `s`. Use fun x ↦ ∑' i, f i x to get the sum function.  -/
SummableUniformlyOn : {α : Type u_1} → {β : Type u_2} → {ι : Type u_3} → [AddCommMonoid α] → (ι → β → α) → Set β → [UniformSpace α] → Prop
-- Mathlib.Analysis.Complex.Harmonic.Analytic
/-- If `f : ℂ → ℝ` is harmonic at `x`, then `∂f/∂1 - I • ∂f/∂I` is complex differentiable at `x`.
 -/
HarmonicAt.differentiableAt_complex_partial : ∀ {f : ℂ → ℝ} {x : ℂ},
  InnerProductSpace.HarmonicAt f x →
    DifferentiableAt ℂ (fun z => ↑((fderiv ℝ f z) 1) - Complex.I * ↑((fderiv ℝ f z) Complex.I)) x
-- Mathlib.Data.NNReal.Defs
NNReal.instCanonicallyOrderedAdd : CanonicallyOrderedAdd NNReal
-- Mathlib.CategoryTheory.Join.Basic
CategoryTheory.Join.id.eq_2 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (x_1 : D), (CategoryTheory.Join.right x_1).id = { down := CategoryTheory.CategoryStruct.id x_1 }
-- Mathlib.Algebra.Group.Units.Defs
Units.isUnit : ∀ {M : Type u_1} [inst : Monoid M] (u : Mˣ), IsUnit ↑u
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.dropLast_nil : ∀ {V : Type u} {G : SimpleGraph V} {v : V}, SimpleGraph.Walk.nil.dropLast = SimpleGraph.Walk.nil
-- Mathlib.Computability.Primrec.Basic
Primrec.list_idxOf₁ : ∀ {α : Type u_1} [inst : Primcodable α] [inst_1 : DecidableEq α] (l : List α), Primrec fun a => List.idxOf a l
-- Mathlib.Topology.Convenient.Category
ContinuousGeneratedByCat.instIsLeftAdjointTopCatToTopCat : ∀ {ι : Type t} {X : ι → Type u} [inst : (i : ι) → TopologicalSpace (X i)],
  (ContinuousGeneratedByCat.toTopCat X).IsLeftAdjoint
-- Mathlib.Algebra.Tropical.Basic
Tropical.instTopTropical : {R : Type u} → [Top R] → Top (Tropical R)
-- Init.Data.Ord.UInt
UInt8.instTransOrd : Std.TransOrd UInt8
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem?_toArray_rcc_eq_none_iff : ∀ {m n i : ℕ}, (m...=n).toArray[i]? = none ↔ n + 1 ≤ i + m
-- Mathlib.NumberTheory.Height.MvPolynomial
/-- If
* `p : ι' → MvPolynomial ι K` is a family of polynomials (which in practice will be homogeneous
  of the same degree `N`),
* `q : ι × ι' → MvPolynomial ι K` is a family of homogeneous polynomials of the same degree `M`,
* `x : ι → K` is such that for all `k : ι`,
  `∑ j, (q (k, j)).eval x * (p j).eval x = (x k) ^ (M + N)`,

then the logarithmic height of `fun j ↦ (p j).eval x` is bounded below by a
constant plus `N` times the logarithmic height of `x`.

The difference to `logHeight_eval_ge` is that the constant is not made explicit.  -/
Height.logHeight_eval_ge' : ∀ {K : Type u_6} [inst : Field K] {ι : Type u_7} {ι' : Type u_8} [inst_1 : Fintype ι']
  [inst_2 : Height.AdmissibleAbsValues K] [Finite ι] {M N : ℕ} {q : ι × ι' → MvPolynomial ι K},
  (∀ (a : ι × ι'), (q a).IsHomogeneous M) →
    ∃ C,
      ∀ (p : ι' → MvPolynomial ι K) {x : ι → K},
        (∀ (k : ι), ∑ j, (MvPolynomial.eval x) (q (k, j)) * (MvPolynomial.eval x) (p j) = x k ^ (M + N)) →
          C + ↑N * Height.logHeight x ≤ Height.logHeight fun j => (MvPolynomial.eval x) (p j)
-- Mathlib.RingTheory.Polynomial.Pochhammer
ascPochhammer_eval_neg_eq_descPochhammer : ∀ (R : Type u) [inst : Ring R] (r : R) (k : ℕ),
  Polynomial.eval (-r) (ascPochhammer R k) = (-1) ^ k * Polynomial.eval r (descPochhammer R k)
-- Mathlib.Order.CompleteLattice.Finset
Finset.iInf_coe : ∀ {α : Type u_2} {β : Type u_3} [inst : InfSet β] (f : α → β) (s : Finset α), ⨅ x ∈ ↑s, f x = ⨅ x ∈ s, f x
-- Mathlib.RingTheory.Extension.Cotangent.Basic
Algebra.Extension.H1Cotangent.map_comp : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {P : Algebra.Extension R S}
  {R' : Type u'} {S' : Type v'} [inst_3 : CommRing R'] [inst_4 : CommRing S'] [inst_5 : Algebra R' S']
  {P' : Algebra.Extension R' S'} [inst_6 : Algebra R R'] [inst_7 : Algebra S S'] [inst_8 : Algebra R S']
  [inst_9 : IsScalarTower R R' S'] {R'' : Type u''} {S'' : Type v''} [inst_10 : CommRing R''] [inst_11 : CommRing S'']
  [inst_12 : Algebra R'' S''] {P'' : Algebra.Extension R'' S''} [inst_13 : Algebra R R''] [inst_14 : Algebra S S'']
  [inst_15 : Algebra R S''] [inst_16 : IsScalarTower R R'' S''] [inst_17 : Algebra R' R''] [inst_18 : Algebra S' S'']
  [inst_19 : Algebra R' S''] [inst_20 : IsScalarTower R' R'' S''] [inst_21 : IsScalarTower R R' R'']
  [inst_22 : IsScalarTower S S' S''] (f : P.Hom P') (g : P'.Hom P''),
  Algebra.Extension.H1Cotangent.map (g.comp f) =
    ↑S (Algebra.Extension.H1Cotangent.map g) ∘ₗ Algebra.Extension.H1Cotangent.map f
-- Mathlib.RingTheory.MvPowerSeries.Evaluation
MvPowerSeries.HasEval.add : ∀ {σ : Type u_1} {S : Type u_3} [inst : CommRing S] [inst_1 : TopologicalSpace S] [ContinuousAdd S]
  [IsLinearTopology S S] {a b : σ → S},
  MvPowerSeries.HasEval a → MvPowerSeries.HasEval b → MvPowerSeries.HasEval (a + b)
-- Mathlib.Geometry.Euclidean.SignedDist
signedDist_smul_of_neg : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (v : V) (p q : P) {r : ℝ}, r < 0 → ((signedDist (r • v)) p) q = -((signedDist v) p) q
-- Std.Time.Format.Modifier
Std.Time.Modifier.L.inj : ∀ {presentation presentation_1 : Std.Time.Number ⊕ Std.Time.Text},
  Std.Time.Modifier.L presentation = Std.Time.Modifier.L presentation_1 → presentation = presentation_1
-- Init.Data.UInt.Lemmas
UInt64.toBitVec_inj : ∀ {a b : UInt64}, a.toBitVec = b.toBitVec ↔ a = b
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rcc.toArray_eq_if_roc : ∀ {α : Type u} {r : Std.Rcc α} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLE α]
  [inst_5 : Std.Rxc.IsAlwaysFinite α],
  r.toArray = if r.lower ≤ r.upper then #[r.lower] ++ (r.lower<...=r.upper).toArray else #[]
-- Mathlib.Topology.Inseparable
stableUnderGeneralization_iUnion : ∀ {X : Type u_1} [inst : TopologicalSpace X] {ι : Sort u_7} (S : ι → Set X),
  (∀ (i : ι), StableUnderGeneralization (S i)) → StableUnderGeneralization (⋃ i, S i)
-- Mathlib.Analysis.Normed.Operator.Banach
ContinuousLinearMap.frontier_preimage : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜'] {σ : 𝕜 →+* 𝕜'}
  {E : Type u_3} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {F : Type u_4}
  [inst_4 : NormedAddCommGroup F] [inst_5 : NormedSpace 𝕜' F] (f : E →SL[σ] F) {σ' : 𝕜' →+* 𝕜} [RingHomInvPair σ σ']
  [RingHomIsometric σ] [RingHomIsometric σ'] [CompleteSpace F] [CompleteSpace E],
  Function.Surjective ⇑f → ∀ (s : Set F), frontier (⇑f ⁻¹' s) = ⇑f ⁻¹' frontier s
-- Mathlib.AlgebraicTopology.SimplicialComplex.Basic
/-- Map each vertex in each face of a PreAbstractSimplicialComplex through a function,
producing a new PreAbstractSimplicialComplex.
 -/
PreAbstractSimplicialComplex.map : {α : Type u_2} →
  {β : Type u_3} → [DecidableEq β] → PreAbstractSimplicialComplex α → (α → β) → PreAbstractSimplicialComplex β
-- Mathlib.Logic.Function.Basic
Function.update.congr_simp : ∀ {α : Sort u} {β : α → Sort v} {inst : DecidableEq α} [inst_1 : DecidableEq α] (f f_1 : (a : α) → β a),
  f = f_1 → ∀ (a' : α) (v v_1 : β a'), v = v_1 → ∀ (a : α), Function.update f a' v a = Function.update f_1 a' v_1 a
-- Init.Data.Vector.Algebra
Vector.left_distrib : ∀ {α : Type u_1} {n : ℕ} [inst : Add α] [inst_1 : Mul α],
  (∀ (x y z : α), x * (y + z) = x * y + x * z) → ∀ (xs ys zs : Vector α n), xs * (ys + zs) = xs * ys + xs * zs
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.tendsto_iff_forall : ∀ {x : ℝ*} {r : ℝ}, Filter.Germ.Tendsto x (nhds r) ↔ (∀ s < r, ↑s ≤ x) ∧ ∀ s > r, x ≤ ↑s
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.MonoidalOpposite.tensorLeftIso_hom_app_unmop : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X X_1 : Cᴹᵒᵖ),
  (X.tensorLeftIso.hom.app X_1).unmop =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj X_1.unmop X.unmop)
-- Mathlib.Algebra.GroupWithZero.Units.Fintype
Nat.card_eq_card_units_add_one : ∀ (α : Type u_1) [inst : GroupWithZero α] [Finite α], Nat.card α = Nat.card αˣ + 1
-- Mathlib.Algebra.Order.Sub.Defs
add_tsub_add_eq_tsub_left : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [OrderedSub α] [AddLeftMono α]
  [AddLeftReflectLE α] (a b c : α), a + b - (a + c) = b - c
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.mem_toSublattice : ∀ {α : Type u_2} [inst : BooleanAlgebra α] {L : BooleanSubalgebra α} {a : α}, a ∈ L.toSublattice ↔ a ∈ L
-- Mathlib.Data.ENNReal.Basic
ENNReal.toReal_ne_one : ∀ {a : ENNReal}, a.toReal ≠ 1 ↔ a ≠ 1
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.ImportFailure.mk.sizeOf_spec : ∀ (module const : Lean.Name) (exception : Lean.Exception),
  sizeOf { module := module, const := const, exception := exception } =
    1 + sizeOf module + sizeOf const + sizeOf exception
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
extChartAt_source_mem_nhdsWithin : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  {I : ModelWithCorners 𝕜 E H} {s : Set M} [inst_5 : ChartedSpace H M] (x : M), (extChartAt I x).source ∈ nhdsWithin x s
-- Mathlib.Algebra.Group.Prod
AddEquiv.prodProdProdComm_apply : ∀ (M : Type u_3) (N : Type u_4) [inst : AddZeroClass M] [inst_1 : AddZeroClass N] (M' : Type u_6) (N' : Type u_7)
  [inst_2 : AddZeroClass N'] [inst_3 : AddZeroClass M'] (mnmn : (M × N) × M' × N'),
  (AddEquiv.prodProdProdComm M N M' N') mnmn = ((mnmn.1.1, mnmn.2.1), mnmn.1.2, mnmn.2.2)
-- Mathlib.Order.Interval.Set.ProjIcc
Set.projIcc_surjOn : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α} (h : a ≤ b), Set.SurjOn (Set.projIcc a b h) (Set.Icc a b) Set.univ
-- Mathlib.RingTheory.Etale.StandardEtale
/-- Maps out of `R[X][Y]/⟨f, Yg-1⟩` corresponds bijectively with
`x` such that `f(x) = 0` and `g(x)` is invertible.  -/
StandardEtalePair.homEquiv : {R : Type u_1} →
  {S : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] → (P : StandardEtalePair R) → (P.Ring →ₐ[R] S) ≃ { x // P.HasMap x }
-- Mathlib.RingTheory.Spectrum.Prime.RingHom
range_comap_of_surjective : ∀ {R : Type u} (S : Type v) [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
  Function.Surjective ⇑f → Set.range (PrimeSpectrum.comap f) = PrimeSpectrum.zeroLocus ↑(RingHom.ker f)
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.self_comp_symm : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂]
  [inst_4 : SeminormedAddCommGroup E] [inst_5 : SeminormedAddCommGroup E₂] [inst_6 : Module R E] [inst_7 : Module R₂ E₂]
  (e : E ≃ₛₗᵢ[σ₁₂] E₂), ⇑e ∘ ⇑e.symm = id
-- Mathlib.Analysis.InnerProductSpace.Reproducing
/-- If the kernel functions are uniformly bounded on a set `s` (`‖kerFun H x‖ ≤ C` for `x ∈ s`),
then convergence in `H`-norm implies uniform convergence of the underlying functions on `s`.  -/
RKHS.tendstoUniformlyOn_of_norm_kerFun_le : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {X : Type u_2} {V : Type u_3} [inst_1 : NormedAddCommGroup V]
  [inst_2 : InnerProductSpace 𝕜 V] {H : Type u_4} [inst_3 : NormedAddCommGroup H] [inst_4 : InnerProductSpace 𝕜 H]
  [inst_5 : RKHS 𝕜 H X V] [inst_6 : CompleteSpace H] [inst_7 : CompleteSpace V] {C : ℝ} {s : Set X},
  (∀ x ∈ s, ‖RKHS.kerFun H x‖ ≤ C) →
    ∀ {ι : Type u_5} {l : Filter ι} {F : ι → H} {f : H},
      Filter.Tendsto F l (nhds f) → TendstoUniformlyOn (fun n => ⇑(F n)) (⇑f) l s
-- Mathlib.Order.Hom.CompleteLattice
CompleteLatticeHomClass.tosInfHomClass : ∀ {F : Type u_8} {α : Type u_9} {β : Type u_10} {inst : CompleteLattice α} {inst_1 : CompleteLattice β}
  {inst_2 : FunLike F α β} [self : CompleteLatticeHomClass F α β], sInfHomClass F α β
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
/-- To prove that a property holds for any strongly measurable function, it is enough to show
that it holds for constant functions and that it is closed under piecewise combination of functions
and pointwise limits.

To use in an induction proof, the syntax is
`induction f, hf using StronglyMeasurable.induction' with`.  -/
MeasureTheory.StronglyMeasurable.induction' : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [Nonempty β] [inst_2 : TopologicalSpace β]
  {P : (f : α → β) → MeasureTheory.StronglyMeasurable f → Prop},
  (∀ (c : β), P (fun x => c) ⋯) →
    (∀ ⦃f g : α → β⦄ {s : Set α} (hf : MeasureTheory.StronglyMeasurable f) (hg : MeasureTheory.StronglyMeasurable g)
        (hs : MeasurableSet s), P f hf → P g hg → P (s.piecewise f g) ⋯) →
      (∀ ⦃f : ℕ → α → β⦄ ⦃g : α → β⦄ (hf : ∀ (n : ℕ), MeasureTheory.StronglyMeasurable (f n))
          (hg : MeasureTheory.StronglyMeasurable g),
          (∀ (n : ℕ), P (f n) ⋯) →
            (∀ (x : α), Filter.Tendsto (fun x_1 => f x_1 x) Filter.atTop (nhds (g x))) → P g hg) →
        ∀ (f : α → β) (hf : MeasureTheory.StronglyMeasurable f), P f hf
-- Mathlib.RingTheory.Valuation.Extension
Valuation.HasExtension.mk_smul_mk : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] {ΓR : Type u_6}
  {ΓA : Type u_7} [inst_3 : LinearOrderedCommGroupWithZero ΓR] [inst_4 : LinearOrderedCommGroupWithZero ΓA]
  {vR : Valuation R ΓR} {vA : Valuation A ΓA} [inst_5 : vR.HasExtension vA] (r : R) (hr : r ∈ vR.integer) (a : A)
  (ha : a ∈ vA.integer), ⟨r, hr⟩ • ⟨a, ha⟩ = ⟨r • a, ⋯⟩
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
/-- A `AddEquiv` version of `Equiv.withBotCongr`.  -/
AddEquiv.withBotCongr : {α : Type u} → {β : Type v} → [inst : Add α] → [inst_1 : Add β] → α ≃+ β → WithBot α ≃+ WithBot β
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
SimplexCategory.len_lt_of_mono : ∀ {Δ' Δ : SimplexCategory} (i : Δ' ⟶ Δ) [CategoryTheory.Mono i], Δ ≠ Δ' → Δ'.len < Δ.len