mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Analytic.Inverse
FormalMultilinearSeries.comp_rightInv_aux2 : ∀ {𝕜 : 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]
  (p : FormalMultilinearSeries 𝕜 E F) (i : E ≃L[𝕜] F) (x : E) (n : ℕ) (v : Fin (n + 2) → F),
  ∑ c ∈ {c | 1 < c.length}.toFinset,
      (p c.length) (FormalMultilinearSeries.applyComposition (fun k => if k < n + 2 then p.rightInv i x k else 0) c v) =
    ∑ c ∈ {c | 1 < c.length}.toFinset, (p c.length) ((p.rightInv i x).applyComposition c v)
-- Mathlib.RingTheory.WittVector.Basic
_private.Mathlib.RingTheory.WittVector.Basic.0.WittVector.ghostFun_natCast : ∀ {p : ℕ} {R : Type u_1} [inst : CommRing R] [inst_1 : Fact (Nat.Prime p)] (i : ℕ), WittVector.ghostFun✝ ↑i = ↑i
-- Mathlib.NumberTheory.Padics.Hensel
_private.Mathlib.NumberTheory.Padics.Hensel.0.ih_n.congr_simp : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {R : Type u_1} [inst_1 : CommSemiring R] [inst_2 : Algebra R ℤ_[p]]
  {F : Polynomial R} {a : ℤ_[p]}
  (hnorm : ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2) {n : ℕ} {z z_1 : ℤ_[p]}
  (e_z : z = z_1) (hz : ih_gen✝ n z), ih_n✝ hnorm hz = ih_n✝ hnorm ⋯
-- Init.Data.SInt.Bitwise
Int16.not_zero : ~~~0 = -1
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
cauchySeq_finset_iff_nat_tprod_vanishing : ∀ {G : Type u_2} [inst : CommGroup G] [inst_1 : UniformSpace G] [IsUniformGroup G] {f : ℕ → G},
  (CauchySeq fun s => ∏ n ∈ s, f n) ↔ ∀ e ∈ nhds 1, ∃ N, ∀ t ⊆ {n | N ≤ n}, ∏' (n : ↑t), f ↑n ∈ e
-- Mathlib.Topology.Convenient.Category
/-- The unit (isomorphism) of the adjunction `ContinuousGeneratedByCat.adj` between
the categories `ContinuousGeneratedByCat X` and `TopCat`.  -/
ContinuousGeneratedByCat.adjUnitIso : {ι : Type t} →
  {X : ι → Type u} →
    [inst : (i : ι) → TopologicalSpace (X i)] →
      CategoryTheory.Functor.id (ContinuousGeneratedByCat X) ≅
        (ContinuousGeneratedByCat.toTopCat X).comp (TopCat.toContinuousGeneratedByCat X)
-- Init.Data.List.MinMax
_private.Init.Data.List.MinMax.0.List.head.match_1.splitter : {α : Type u_1} →
  (motive : (x : List α) → x ≠ [] → Sort u_2) →
    (x : List α) →
      (x_1 : x ≠ []) → ((a : α) → (tail : List α) → (x : a :: tail ≠ []) → motive (a :: tail) x) → motive x x_1
-- Mathlib.Tactic.CategoryTheory.BicategoryCoherence
Mathlib.Tactic.BicategoryCoherence.LiftHom₂.mk : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b : B} →
      {f g : a ⟶ b} →
        [inst_1 : Mathlib.Tactic.BicategoryCoherence.LiftHom f] →
          [inst_2 : Mathlib.Tactic.BicategoryCoherence.LiftHom g] →
            {η : f ⟶ g} →
              (Mathlib.Tactic.BicategoryCoherence.LiftHom.lift f ⟶ Mathlib.Tactic.BicategoryCoherence.LiftHom.lift g) →
                Mathlib.Tactic.BicategoryCoherence.LiftHom₂ η
-- Mathlib.CategoryTheory.Monoidal.CommMon_
CategoryTheory.Adjunction.mapCommMon_counit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {D : Type u₂} [inst_3 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_4 : CategoryTheory.MonoidalCategory D] [inst_5 : CategoryTheory.BraidedCategory D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (a : F ⊣ G) [inst_6 : F.Braided]
  [inst_7 : G.LaxBraided] [inst_8 : a.IsMonoidal],
  a.mapCommMon.counit =
    CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.mapCommMonCompIso.inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.mapCommMonNatTrans a.counit)
        CategoryTheory.Functor.mapCommMonIdIso.hom)
-- Std.Http.Data.Body.Length
/-- Checks if the `Length` is chunked.
 -/
Std.Http.Body.Length.isChunked : Std.Http.Body.Length → Bool
-- Mathlib.Geometry.Manifold.Algebra.Monoid
/-- If the multiplication is `C^n`, then it is continuous. This is not an instance for technical
reasons, see note [Design choices about smooth algebraic structures].  -/
continuousMul_of_contMDiffMul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] (I : ModelWithCorners 𝕜 E H) (n : WithTop ℕ∞)
  {G : Type u_4} [inst_4 : Mul G] [inst_5 : TopologicalSpace G] [inst_6 : ChartedSpace H G] [ContMDiffMul I n G],
  ContinuousMul G
-- Mathlib.MeasureTheory.MeasurableSpace.EventuallyMeasurable
/-- A function which is `EventuallyEq` to some `EventuallyMeasurable` function
is `EventuallyMeasurable`.  -/
EventuallyMeasurable.congr : ∀ {α : Type u_1} {m : MeasurableSpace α} {l : Filter α} [inst : CountableInterFilter l] {β : Type u_2}
  [inst_1 : MeasurableSpace β] {f g : α → β}, EventuallyMeasurable m l f → g =ᶠ[l] f → EventuallyMeasurable m l g
-- Mathlib.Tactic.FieldSimp.Lemmas
Mathlib.Tactic.FieldSimp.NF.zpow_eq_eval : ∀ {M : Type u_1} [inst : CommGroupWithZero M] {l : Mathlib.Tactic.FieldSimp.NF M} {r : ℤ},
  r ≠ 0 → ∀ {x : M}, x = l.eval → x ^ r = (l ^ r).eval
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.flipEquiv_apply : ∀ (ι : Type u_1) (R : Type u_2) (M : Type u_3) (N : Type u_4) [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R N M),
  (RootPairing.flipEquiv ι R M N) P = P.flip
-- Mathlib.Order.Interval.Set.Image
Set.image_subtype_val_Iio_Ioi : ∀ {α : Type u_1} [inst : Preorder α] {a : α} (b : ↑(Set.Iio a)), Subtype.val '' Set.Ioi b = Set.Ioo (↑b) a
-- Mathlib.Combinatorics.SimpleGraph.Basic
/-- A vertex in a graph is universal if it's adjacent to every other vertex.  -/
SimpleGraph.IsUniversal : {V : Type u} → SimpleGraph V → V → Prop
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
Matrix.matPolyEquiv_charmatrix : ∀ {R : Type u_1} [inst : CommRing R] {n : Type u_4} [inst_1 : DecidableEq n] [inst_2 : Fintype n] (M : Matrix n n R),
  matPolyEquiv M.charmatrix = Polynomial.X - Polynomial.C M
-- Mathlib.Analysis.Asymptotics.Theta
Asymptotics.IsTheta.smul : ∀ {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {𝕜 : Type u_14} {𝕜' : Type u_15} [inst : SeminormedAddCommGroup E']
  [inst_1 : SeminormedAddCommGroup F'] [inst_2 : NormedField 𝕜] [inst_3 : NormedField 𝕜'] {l : Filter α}
  [inst_4 : NormedSpace 𝕜 E'] [inst_5 : NormedSpace 𝕜' F'] {f₁ : α → 𝕜} {f₂ : α → 𝕜'} {g₁ : α → E'} {g₂ : α → F'},
  f₁ =Θ[l] f₂ → g₁ =Θ[l] g₂ → (fun x => f₁ x • g₁ x) =Θ[l] fun x => f₂ x • g₂ x
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.IndepSets_iff : ∀ {Ω : Type u_1} {x : MeasurableSpace Ω} (s1 s2 : Set (Set Ω)) (μ : MeasureTheory.Measure Ω),
  ProbabilityTheory.IndepSets s1 s2 μ ↔ ∀ (t1 t2 : Set Ω), t1 ∈ s1 → t2 ∈ s2 → μ (t1 ∩ t2) = μ t1 * μ t2
-- Mathlib.Data.Finset.Insert
Finset.eq_singleton_iff_unique_mem : ∀ {α : Type u_1} {s : Finset α} {a : α}, s = {a} ↔ a ∈ s ∧ ∀ x ∈ s, x = a
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.getD_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α}
  {fallback : β}, t₁.Equiv t₂ → t₁.getD k fallback = t₂.getD k fallback
-- Init.Grind.Module.OfNatModule
Lean.Grind.IntModule.OfNatModule.of_lt : ∀ {α : Type u_1} [inst : Lean.Grind.NatModule α] [inst_1 : LE α] [inst_2 : LT α] [Std.LawfulOrderLT α]
  [inst_4 : Std.IsPreorder α] [inst_5 : Lean.Grind.OrderedAdd α] {a b : α}
  {a' b' : Lean.Grind.IntModule.OfNatModule.Q α},
  Lean.Grind.IntModule.OfNatModule.toQ a = a' → Lean.Grind.IntModule.OfNatModule.toQ b = b' → a < b → a' < b'
-- Mathlib.Order.Lattice
ULift.instLattice : {α : Type u} → [Lattice α] → Lattice (ULift.{v, u} α)
-- Mathlib.CategoryTheory.Idempotents.FunctorExtension
CategoryTheory.Idempotents.instIsEquivalenceFunctorKaroubiObjWhiskeringLeftToKaroubi : ∀ (C : Type u_1) (D : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.IsIdempotentComplete D],
  ((CategoryTheory.Functor.whiskeringLeft C (CategoryTheory.Idempotents.Karoubi C) D).obj
      (CategoryTheory.Idempotents.toKaroubi C)).IsEquivalence
-- Mathlib.LinearAlgebra.Matrix.Basis
Module.Basis.toMatrix_smul_left : ∀ {ι : Type u_1} {ι' : Type u_2} {R : Type u_5} {M : Type u_6} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] (e : Module.Basis ι R M) (v : ι' → M) {G : Type u_9} [inst_3 : Group G]
  [inst_4 : DistribMulAction G M] [inst_5 : SMulCommClass G R M] (g : G), (g • e).toMatrix v = e.toMatrix (g⁻¹ • v)
-- Mathlib.Analysis.Distribution.SchwartzSpace.Deriv
SchwartzMap.lineDerivOp_compCLMOfContinuousLinearEquiv : ∀ (𝕜 : Type u_2) {D : Type u_4} {E : Type u_5} {F : Type u_8} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace ℝ F] [inst_3 : NormedSpace ℝ E] [inst_4 : RCLike 𝕜]
  [inst_5 : NormedSpace 𝕜 F] [inst_6 : NormedAddCommGroup D] [inst_7 : NormedSpace ℝ D] (m : D) (g : D ≃L[ℝ] E)
  (f : SchwartzMap E F),
  LineDeriv.lineDerivOp m ((SchwartzMap.compCLMOfContinuousLinearEquiv 𝕜 g) f) =
    (SchwartzMap.compCLMOfContinuousLinearEquiv 𝕜 g) (LineDeriv.lineDerivOp (g m) f)
-- Mathlib.LinearAlgebra.Semisimple
Module.End.IsSemisimple.isFinitelySemisimple : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {f : Module.End R M}, f.IsSemisimple → f.IsFinitelySemisimple
-- Mathlib.Topology.Sober
IsGenericPoint.mem : ∀ {α : Type u_1} [inst : TopologicalSpace α] {x : α} {S : Set α}, IsGenericPoint x S → x ∈ S
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.EMatchTheoremKind.eqRhs.inj : ∀ {gen gen_1 : Bool},
  Lean.Meta.Grind.EMatchTheoremKind.eqRhs gen = Lean.Meta.Grind.EMatchTheoremKind.eqRhs gen_1 → gen = gen_1
-- Mathlib.NumberTheory.NumberField.InfiniteAdeleRing
NumberField.InfiniteAdeleRing.algebraMap_apply : ∀ (K : Type u_1) [inst : Field K] (x : K) (v : NumberField.InfinitePlace K),
  (algebraMap K (NumberField.InfiniteAdeleRing K)) x v = { toCompletion := ↑(WithAbs.toAbs (↑v) x) }
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.isSuccLimit_aleph0 : Order.IsSuccLimit Cardinal.aleph0
-- Mathlib.Geometry.Euclidean.Sphere.Basic
/-- The distance from the center of a sphere to the midpoint of a chord
with distinct endpoints is strictly less than the radius.  -/
EuclideanGeometry.Sphere.dist_center_midpoint_lt_radius : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {p₁ p₂ : P} {s : EuclideanGeometry.Sphere P},
  p₁ ∈ s → p₂ ∈ s → p₁ ≠ p₂ → dist s.center (midpoint ℝ p₁ p₂) < s.radius
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
SubAddAction.of_fixingAddSubgroupEmpty_mapScalars_surjective : ∀ {M : Type u_1} {α : Type u_2} [inst : AddGroup M] [inst_1 : AddAction M α],
  Function.Surjective ⇑(fixingAddSubgroup M ∅).subtype
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.Expr.toPoly : Nat.Internal.Linear.Expr → Nat.Internal.Linear.Poly
-- Mathlib.Tactic.FunProp.Types
/-- Custom discharger to satisfy theorem hypotheses.  -/
Mathlib.Meta.FunProp.Context.disch : Mathlib.Meta.FunProp.Context → Lean.Expr → Lean.MetaM (Option Lean.Expr)
-- Init.Data.Array.Attach
Array.unattach_replicate : ∀ {α : Type u_1} {p : α → Prop} {n : ℕ} {x : { x // p x }}, (Array.replicate n x).unattach = Array.replicate n ↑x
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.LetRecToLift.localInstances : Lean.Elab.Term.LetRecToLift → Lean.LocalInstances
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.mapₗ_apply : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} [inst : MeasurableSpace β] {M : Type u_3}
  [inst_1 : AddCommMonoid M] [inst_2 : TopologicalSpace M] {R : Type u_4} [inst_3 : Semiring R] [inst_4 : Module R M]
  [inst_5 : ContinuousConstSMul R M] [inst_6 : ContinuousAdd M] (f : α → β) (v : MeasureTheory.VectorMeasure α M),
  (MeasureTheory.VectorMeasure.mapₗ f) v = v.map f
-- Std.Do.SPred.SPred
Std.Do.SPred.exists_nil : ∀ {α : Sort u_1} {P : α → Std.Do.SPred []}, Std.Do.SPred.exists P = { down := ∃ a, (P a).down }
-- Mathlib.Algebra.BigOperators.Group.List.Basic
List.alternatingProd_nil : ∀ {G : Type u_7} [inst : One G] [inst_1 : Mul G] [inst_2 : Inv G], [].alternatingProd = 1
-- Mathlib.Algebra.Module.Torsion.Basic
Submodule.torsionBySet_univ : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  Submodule.torsionBySet R M Set.univ = ⊥
-- Mathlib.Algebra.Star.Conjneg
conjneg_eq_zero : ∀ {G : Type u_2} {R : Type u_3} [inst : AddGroup G] [inst_1 : CommSemiring R] [inst_2 : StarRing R] {f : G → R},
  conjneg f = 0 ↔ f = 0
-- Mathlib.Data.Sym.Basic
Sym.map_cons : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} (f : α → β) (a : α) (s : Sym α n), Sym.map f (a ::ₛ s) = f a ::ₛ Sym.map f s
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Free
SheafOfModules.inl_freeSumIso_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : CategoryTheory.HasWeakSheafify J AddCommGrpCat]
  [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat] (I J_1 : Type u),
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl (SheafOfModules.freeSumIso I J_1).hom =
    SheafOfModules.freeMap Sum.inl
-- Mathlib.Topology.Compactness.Compact
IsClosed.isCompact : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X} [CompactSpace X], IsClosed s → IsCompact s
-- Mathlib.Order.SymmDiff
/-- The Heyting bi-implication is `(b ⇨ a) ⊓ (a ⇨ b)`. This generalizes equivalence of
propositions.  -/
bihimp : {α : Type u_2} → [Min α] → [HImp α] → α → α → α
-- Mathlib.Algebra.Group.Defs
succ_nsmul' : ∀ {M : Type u_2} [inst : AddMonoid M] (a : M) (n : ℕ), (n + 1) • a = a + n • a
-- Lean.Elab.ConfigEval.Instances
Lean.Elab.ConfigEval.EvalExpr.instArray : {α : Type} → [Lean.Elab.ConfigEval.EvalExpr α] → Lean.Elab.ConfigEval.EvalExpr (Array α)
-- Mathlib.CategoryTheory.Limits.Types.End
CategoryTheory.Limits.chosenCoend.map_apply : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J]
  {F G : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J (Type (max w u)))} (f : F ⟶ G)
  (x : CategoryTheory.Limits.chosenCoend F),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.chosenCoend.map f)) x =
    Quot.lift
      (fun x =>
        Quot.mk (CategoryTheory.Limits.Types.coendRel G)
          ⟨x.fst, (CategoryTheory.ConcreteCategory.hom ((f.app (Opposite.op x.fst)).app x.fst)) x.snd⟩)
      ⋯ x
-- Mathlib.Data.FunLike.Group
FunLike.cancelCommMonoid.eq_1 : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : Mul F] [inst_2 : One F]
  [inst_3 : Pow F ℕ] [inst_4 : CancelCommMonoid β] [inst_5 : IsOneApply F α β] [inst_6 : IsMulApply F α β]
  [inst_7 : IsPowApply ℕ F α β], FunLike.cancelCommMonoid = Function.Injective.cancelCommMonoid (fun f => ⇑f) ⋯ ⋯ ⋯ ⋯
-- Mathlib.Data.Finsupp.Pointwise
Finsupp.instIsScalarTowerForall : ∀ {α : Type u₁} {β : Type u₂} [inst : Semiring β], IsScalarTower β (α → β) (α →₀ β)
-- Mathlib.Topology.Sets.Order
ClopenUpperSet.upper' : ∀ {α : Type u_2} [inst : TopologicalSpace α] [inst_1 : LE α] (self : ClopenUpperSet α), IsUpperSet self.carrier
-- Init.Data.Iterators.Basic
Std.Iter.IsPlausibleStep.isPlausibleSuccessor_of_yield : ∀ {α β : Type w} [inst : Std.Iterator α Id β] {it' it : Std.Iter β} {out : β},
  it.IsPlausibleStep (Std.IterStep.yield it' out) → it'.IsPlausibleSuccessorOf it
-- Mathlib.Order.Interval.Basic
NonemptyInterval.subset_coe_map : ∀ {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst_1 : PartialOrder β] (f : α →o β) (s : NonemptyInterval α),
  ⇑f '' ↑s ⊆ ↑(NonemptyInterval.map f s)
-- Mathlib.Tactic.Order.Preprocessing
Mathlib.Tactic.Order.instBEqOrderType : BEq Mathlib.Tactic.Order.OrderType
-- Mathlib.Algebra.Homology.ShortComplex.Basic
/-- the morphism on the right objects  -/
CategoryTheory.ShortComplex.Hom.τ₃ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} → S₁.Hom S₂ → (S₁.X₃ ⟶ S₂.X₃)
-- Mathlib.MeasureTheory.OuterMeasure.OfFunction
MeasureTheory.OuterMeasure.iSup_sInfGen_nonempty : ∀ {α : Type u_1} {m : Set (MeasureTheory.OuterMeasure α)},
  m.Nonempty → ∀ (t : Set α), ⨆ (_ : t.Nonempty), MeasureTheory.OuterMeasure.sInfGen m t = ⨅ μ ∈ m, μ t
-- Mathlib.Analysis.Complex.Hadamard
/-- **Hadamard three-line theorem**: If `f` is a bounded function, continuous on the
closed strip `re ⁻¹' [l, u]` and differentiable on open strip `re ⁻¹' (l, u)`, then for
`M(x) := sup ((norm ∘ f) '' re ⁻¹' {x})` we have that for all `z` in the closed strip
`re ⁻¹' [a,b]` the inequality
`‖f(z)‖ ≤ M(0) ^ (1 - ((z.re - l) / (u - l))) * M(1) ^ ((z.re - l) / (u - l))`
holds.  -/
Complex.HadamardThreeLines.norm_le_interpStrip_of_mem_verticalClosedStrip : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {l u : ℝ},
  l < u →
    ∀ {f : ℂ → E} {z : ℂ},
      z ∈ Complex.HadamardThreeLines.verticalClosedStrip l u →
        DiffContOnCl ℂ f (Complex.HadamardThreeLines.verticalStrip l u) →
          BddAbove (norm ∘ f '' Complex.HadamardThreeLines.verticalClosedStrip l u) →
            ‖f z‖ ≤ ‖Complex.HadamardThreeLines.interpStrip' f l u z‖
-- Mathlib.Algebra.Ring.Int.Defs
Int.instSemiring : Semiring ℤ
-- Init.Data.SInt.Lemmas
instLawfulCommIdentityInt64HMulOfNat : Std.LawfulCommIdentity (fun x1 x2 => x1 * x2) 1
-- Std.Time.Date.PlainDate
Std.Time.PlainDate.instHSubOffset_1 : HSub Std.Time.PlainDate Std.Time.Week.Offset Std.Time.PlainDate
-- Init.Data.Array.Subarray.Split
/-- Removes the first `i` elements of the subarray. If there are `i` or fewer elements, the resulting
subarray is empty.
 -/
Subarray.drop : {α : Type u_1} → Subarray α → ℕ → Subarray α
-- Mathlib.CategoryTheory.Subfunctor.Finite
CategoryTheory.Subfunctor.isGeneratedBy_of_isFinite : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor Cᵒᵖ (Type w)}
  (G : CategoryTheory.Subfunctor F) [hG : G.IsFinite], G.IsGeneratedBy CategoryTheory.Subfunctor.IsFinite.x
-- Mathlib.Analysis.Normed.Affine.AddTorsor
lipschitzWith_lineMap : ∀ {V : Type u_1} {P : Type u_2} [inst : SeminormedAddCommGroup V] [inst_1 : PseudoMetricSpace P]
  [inst_2 : NormedAddTorsor V P] {𝕜 : Type u_5} [inst_3 : NormedField 𝕜] [inst_4 : NormedSpace 𝕜 V] (p₁ p₂ : P),
  LipschitzWith (nndist p₁ p₂) ⇑(AffineMap.lineMap p₁ p₂)
-- Lean.Meta.Tactic.SplitIf
Lean.Meta.SplitKind.match.sizeOf_spec : sizeOf Lean.Meta.SplitKind.match = 1
-- Mathlib.Geometry.Manifold.ContMDiff.Constructions
/-- `ContMDiffAt.comp₂`, with a separate argument for point equality.  -/
ContMDiffAt.comp₂_of_eq : ∀ {𝕜 : 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] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {F : Type u_8}
  [inst_11 : NormedAddCommGroup F] [inst_12 : NormedSpace 𝕜 F] {G : Type u_9} [inst_13 : TopologicalSpace G]
  {J : ModelWithCorners 𝕜 F G} {N : Type u_10} [inst_14 : TopologicalSpace N] [inst_15 : ChartedSpace G N]
  {F' : Type u_11} [inst_16 : NormedAddCommGroup F'] [inst_17 : NormedSpace 𝕜 F'] {G' : Type u_12}
  [inst_18 : TopologicalSpace G'] {J' : ModelWithCorners 𝕜 F' G'} {N' : Type u_13} [inst_19 : TopologicalSpace N']
  [inst_20 : ChartedSpace G' N'] {n : WithTop ℕ∞} {h : M' × N' → N} {f : M → M'} {g : M → N'} {x : M} {y : M' × N'},
  ContMDiffAt (I'.prod J') J n h y →
    ContMDiffAt I I' n f x → ContMDiffAt I J' n g x → (f x, g x) = y → ContMDiffAt I J n (fun x => h (f x, g x)) x
-- Mathlib.Order.CompleteBooleanAlgebra
_private.Mathlib.Order.CompleteBooleanAlgebra.0.Order.Frame.MinimalAxioms.iSup_inf_eq : ∀ {α : Type u} {ι : Sort w} [inst : CompleteLattice α],
  Order.Frame.MinimalAxioms α → ∀ (f : ι → α) (a : α), (⨆ i, f i) ⊓ a = ⨆ i, f i ⊓ a
-- Mathlib.MeasureTheory.Covering.Differentiation
/-- Given a measurable set `s`, then `μ (s ∩ a) / μ a` converges when `a` shrinks to a typical
point `x` along a Vitali family. The limit is `1` for `x ∈ s` and `0` for `x ∉ s`. This shows that
almost every point of `s` is a Lebesgue density point for `s`. A version for non-measurable sets
holds, but it only gives the first conclusion, see `ae_tendsto_measure_inter_div`.  -/
VitaliFamily.ae_tendsto_measure_inter_div_of_measurableSet : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  (v : VitaliFamily μ) [SecondCountableTopology α] [BorelSpace α] [MeasureTheory.IsLocallyFiniteMeasure μ] {s : Set α},
  MeasurableSet s → ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun a => μ (s ∩ a) / μ a) (v.filterAt x) (nhds (s.indicator 1 x))
-- Std.Data.TreeSet.Lemmas
_private.Std.Data.TreeSet.Lemmas.0.Std.TreeSet.equiv_iff_equiv : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp}, t₁.Equiv t₂ ↔ t₁.inner.Equiv t₂.inner
-- Lean.Elab.App
/-- `true` if `..` was used
 -/
Lean.Elab.Term.ElabAppArgs.Context.ellipsis : Lean.Elab.Term.ElabAppArgs.Context → Bool
-- Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
FreeGroup.reduceCyclically.conj_conjugator_reduceCyclically : ∀ {α : Type u} [inst : DecidableEq α] (L : List (α × Bool)),
  FreeGroup.reduceCyclically.conjugator L ++ FreeGroup.reduceCyclically L ++
      FreeGroup.invRev (FreeGroup.reduceCyclically.conjugator L) =
    L
-- Mathlib.AlgebraicGeometry.Stalk
AlgebraicGeometry.Scheme.SpecMap_stalkMap_fromSpecStalk : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {x : ↥X},
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.Hom.stalkMap f x))
      (Y.fromSpecStalk (f x)) =
    CategoryTheory.CategoryStruct.comp (X.fromSpecStalk x) f
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.mem_keys : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.LawfulEqCmp cmp]
  [Std.TransCmp cmp] {k : α}, k ∈ t.keys ↔ k ∈ t
-- Mathlib.Data.Set.Semiring
SetSemiring.instIsOrderedRing : ∀ {α : Type u_1} [inst : CommMonoid α], IsOrderedRing (SetSemiring α)
-- Mathlib.AlgebraicGeometry.Spec
/-- The spectrum of a commutative ring, as a `SheafedSpace`.
 -/
AlgebraicGeometry.Spec.sheafedSpaceObj : CommRingCat → AlgebraicGeometry.SheafedSpace CommRingCat
-- Mathlib.Order.Filter.NAry
Filter.map_prod_eq_map₂' : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} (m : α × β → γ) (f : Filter α) (g : Filter β),
  Filter.map m (f ×ˢ g) = Filter.map₂ (fun a b => m (a, b)) f g
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
UniformContinuous.const_mul : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : Group α] [IsUniformGroup α] [inst_3 : UniformSpace β]
  {f : β → α}, UniformContinuous f → ∀ (a : α), UniformContinuous fun x => a * f x
-- Mathlib.Order.SuccPred.Basic
WithTop.instPredOrder : {α : Type u_1} → [inst : Preorder α] → [OrderTop α] → [PredOrder α] → PredOrder (WithTop α)
-- Mathlib.RingTheory.AlgebraicIndependent.Basic
/-- A set of algebraically independent elements in an algebra `A` over a ring `K` is also
algebraically independent over a subring `R` of `K`.  -/
AlgebraicIndependent.restrictScalars : ∀ {ι : Type u} {R : Type u_2} {A : Type v} {x : ι → A} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  {K : Type u_3} [inst_3 : CommRing K] [inst_4 : Algebra R K] [inst_5 : Algebra K A] [IsScalarTower R K A],
  Function.Injective ⇑(algebraMap R K) → AlgebraicIndependent K x → AlgebraicIndependent R x
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.eq_top_iff_forall_ne_adj : ∀ {V : Type u} {G : SimpleGraph V}, G = ⊤ ↔ ∀ (a b : V), a ≠ b → G.Adj a b
-- Mathlib.ModelTheory.Graph
SimpleGraph.simpleGraphOfStructure : ∀ {V : Type u} (G : SimpleGraph V), FirstOrder.Language.simpleGraphOfStructure V = G
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.measure_sdiff_lt_of_lt_add : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
  MeasureTheory.NullMeasurableSet s μ → s ⊆ t → μ s ≠ ⊤ → ∀ {ε : ENNReal}, μ t < μ s + ε → μ (t \ s) < ε