mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.Indep.exists_isBase_superset : ∀ {α : Type u_1} {M : Matroid α} {I : Set α}, M.Indep I → ∃ B, M.IsBase B ∧ I ⊆ B
-- Mathlib.RingTheory.LocalRing.LocalSubring
LocalSubring.isLocalRing : ∀ {R : Type u_1} [inst : CommRing R] (self : LocalSubring R), IsLocalRing ↥self.toSubring
-- Mathlib.Order.Restriction
Preorder.frestrictLe_apply : ∀ {α : Type u_1} [inst : Preorder α] {π : α → Type u_2} [inst_1 : LocallyFiniteOrderBot α] (a : α) (f : (a : α) → π a)
  (i : ↥(Finset.Iic a)), Preorder.frestrictLe a f i = f ↑i
-- Mathlib.Analysis.Normed.Module.Span
LinearEquiv.toSpanNonzeroSingleton_homothety : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : NormedDivisionRing 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : Module 𝕜 E]
  [NormSMulClass 𝕜 E] (x : E) (h : x ≠ 0) (c : 𝕜), ‖(LinearEquiv.toSpanNonzeroSingleton 𝕜 E x h) c‖ = ‖x‖ * ‖c‖
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
/-- Suppose `a : X → Set A` is continuous on `t : Set X` and `a x` satisfies the predicate `p` for
all `x ∈ t`. Suppose further that `s : X → Set 𝕜` is a family of sets with `s x` compact when
`x ∈ t` such that `s x₀` contains the spectrum of `a x` for all sufficiently close `x ∈ t`.
If `f : 𝕜 → 𝕜` is continuous on `s x`, for each `x ∈ t`, then `fun x ↦ cfc f (a x)` is
continuous on `t`.  -/
ContinuousOn.cfc : ∀ {X : Type u_1} {𝕜 : Type u_2} {A : Type u_3} {p : A → Prop} [inst : RCLike 𝕜] [inst_1 : NormedRing A]
  [inst_2 : StarRing A] [inst_3 : NormedAlgebra 𝕜 A] [inst_4 : IsometricContinuousFunctionalCalculus 𝕜 A p]
  [ContinuousStar A] [inst_6 : TopologicalSpace X] {s : X → Set 𝕜} (f : 𝕜 → 𝕜) {a : X → A} {t : Set X},
  (∀ x ∈ t, IsCompact (s x)) →
    ContinuousOn a t →
      (∀ x₀ ∈ t, ∀ᶠ (x : X) in nhdsWithin x₀ t, spectrum 𝕜 (a x) ⊆ s x₀) →
        (∀ x ∈ t, p (a x)) →
          autoParam (∀ x ∈ t, ContinuousOn f (s x)) ContinuousOn.cfc._auto_1 → ContinuousOn (fun x => cfc f (a x)) t
-- Mathlib.Topology.Algebra.Module.Multilinear.Topology
/-- The application of a multilinear map as a `ContinuousLinearMap`.  -/
ContinuousMultilinearMap.apply : (𝕜 : Type u_1) →
  {ι : Type u_2} →
    (E : ι → Type u_3) →
      (F : Type u_4) →
        [inst : NormedField 𝕜] →
          [inst_1 : (i : ι) → TopologicalSpace (E i)] →
            [inst_2 : (i : ι) → AddCommGroup (E i)] →
              [inst_3 : (i : ι) → Module 𝕜 (E i)] →
                [inst_4 : AddCommGroup F] →
                  [inst_5 : Module 𝕜 F] →
                    [inst_6 : TopologicalSpace F] →
                      [inst_7 : IsTopologicalAddGroup F] →
                        [∀ (i : ι), ContinuousSMul 𝕜 (E i)] →
                          [inst_9 : ContinuousConstSMul 𝕜 F] → ((i : ι) → E i) → ContinuousMultilinearMap 𝕜 E F →L[𝕜] F
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.normEq0 : Lean.Grind.CommRing.Poly → ℕ → Lean.Grind.CommRing.Poly
-- Mathlib.Combinatorics.Additive.VerySmallDoubling
/-- If `A` has doubling strictly less than `3 / 2`, then there exists a subgroup `H` of the
normaliser of `A` of size strictly less than `3 / 2 * #A` such that `A` is a subset of a coset of
`H` (in fact a subset of `a • H` for every `a ∈ A`).

Note that this is sharp: `A = {0, 1}` in `ℤ` has doubling `3 / 2` and can't be covered by a subgroup
of size at most `2`.

This is Theorem 2.2.1 in [tointon2020].  -/
Finset.doubling_lt_three_halves : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] {A : Finset G},
  ↑(A * A).card < 3 / 2 * ↑A.card →
    ∃ H x, ↑(Fintype.card ↥H) < 3 / 2 * ↑A.card ∧ ∀ a ∈ A, ↑A ⊆ a • ↑H ∧ a • ↑H = MulOpposite.op a • ↑H
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCast_filter_containsKey : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {l₁ l₂ : List ((a : α) × β a)} {k : α},
  Std.Internal.List.DistinctKeys l₁ →
    ∀ {h₁ : Std.Internal.List.containsKey k (List.filter (fun p => Std.Internal.List.containsKey p.fst l₂) l₁) = true}
      {h₂ : Std.Internal.List.containsKey k l₁ = true},
      Std.Internal.List.getValueCast k (List.filter (fun p => Std.Internal.List.containsKey p.fst l₂) l₁) h₁ =
        Std.Internal.List.getValueCast k l₁ h₂
-- Mathlib.Algebra.Group.Units.Basic
divp_left_inj : ∀ {α : Type u} [inst : Monoid α] (u : αˣ) {a b : α}, a /ₚ u = b /ₚ u ↔ a = b
-- Std.Data.HashMap.Basic
/-- Modifies in place the value associated with a given key,
allowing creating new values and deleting values via an `Option` valued replacement function.

This function ensures that the value is used linearly.
 -/
Std.HashMap.alter : {α : Type u} →
  {β : Type v} → {x : BEq α} → {x_1 : Hashable α} → Std.HashMap α β → α → (Option β → Option β) → Std.HashMap α β
-- Lean.Hygiene
/-- Erase macro scopes from `userName` and add "tombstone" + superscript (or `._hyg`).  -/
Lean.sanitizeName : Lean.Name → StateM Lean.NameSanitizerState Lean.Name
-- Init.Data.Iterators.Basic
/-- Asserts that a certain iterator `it` could plausibly yield the value `out` after an arbitrary
number of steps.
 -/
Std.Iter.IsPlausibleIndirectOutput : {α β : Type w} → [Std.Iterator α Id β] → Std.Iter β → β → Prop
-- Mathlib.Data.ENNReal.Inv
ENNReal.mul_sSup : ∀ {s : Set ENNReal} {a : ENNReal}, a * sSup s = ⨆ b ∈ s, a * b
-- Mathlib.Algebra.MonoidAlgebra.Module
AddMonoidAlgebra.distribMulAction.eq_1 : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} [inst : Monoid S] [inst_1 : Semiring R] [inst_2 : DistribMulAction S R],
  AddMonoidAlgebra.distribMulAction =
    { toSMul := AddMonoidAlgebra.smulZeroClass.toSMul, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯ }
-- Mathlib.RingTheory.IdealFilter.Basic
IdealFilter.isTorsionQuot_self : ∀ {A : Type u_1} [inst : Ring A] (F : IdealFilter A) (I : Ideal A), F.IsTorsionQuot I I
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.Hom.w₁₁_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S}
  {F : CategoryTheory.PreOneHypercover S} (self : E.Hom F) {i j : E.I₀} (k : E.I₁ i j) {Z : C}
  (h : F.X (self.s₀ i) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (self.h₁ k) (CategoryTheory.CategoryStruct.comp (F.p₁ (self.s₁ k)) h) =
    CategoryTheory.CategoryStruct.comp (E.p₁ k) (CategoryTheory.CategoryStruct.comp (self.h₀ i) h)
-- Mathlib.Order.Interval.Set.WithBotTop
WithTop.image_coe_Icc : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, WithTop.some '' Set.Icc a b = Set.Icc ↑a ↑b
-- Mathlib.Order.Disjoint
codisjoint_top_left : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : OrderTop α] {a : α}, Codisjoint ⊤ a
-- Mathlib.Analysis.Calculus.FDeriv.Basic
differentiableWithinAt_congr_nhds : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {x : E} {s t : Set E},
  nhdsWithin x s = nhdsWithin x t → (DifferentiableWithinAt 𝕜 f s x ↔ DifferentiableWithinAt 𝕜 f t x)
-- Init.Data.SInt.Basic
/-- Converts a word-sized signed integer to an arbitrary-precision integer that denotes the same number.

This function is overridden at runtime with an efficient implementation.
 -/
ISize.toInt : ISize → ℤ
-- Mathlib.GroupTheory.Congruence.Defs
/-- Definition of `≤` for congruence relations.  -/
Con.le_def : ∀ {M : Type u_1} [inst : Mul M] {c d : Con M}, c ≤ d ↔ ∀ {x y : M}, c x y → d x y
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
/-- Variant of `prod_empty` not applied to a function.  -/
Finset.prod_empty' : ∀ {ι : Type u_1} {M : Type u_3} [inst : CommMonoid M], ∅.prod = fun x => 1
-- Mathlib.GroupTheory.Subgroup.Center
AddSubgroup.centerToAddOpposite_apply_coe : ∀ (G : Type u_1) [inst : AddGroup G] (r : ↥(AddSubsemigroup.center G)),
  ↑((AddSubgroup.centerToAddOpposite G) r) = AddOpposite.op ↑r
-- Mathlib.LinearAlgebra.Eigenspace.Basic
Module.End.Eigenvalues.mk_val : ∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {f : Module.End R M}
  (μ : f.Eigenvalues), ⟨↑f μ, ⋯⟩ = μ
-- Mathlib.Tactic.Translate.Core
/-- The `(rename := ...)` option takes a comma-separated list of rename rules of the form
`oldName → newName` specifying the argument names of the translated constant. The syntax
`firstName ↔ secondName` can also be used for swapping two argument names.
 -/
Mathlib.Tactic.Translate.renameOption : Lean.ParserDescr
-- Mathlib.Algebra.Homology.SpectralObject.Page
/-- The functoriality of `shortComplex` with respect to morphisms
in `ComposableArrows ι 3`.  -/
CategoryTheory.Abelian.SpectralObject.shortComplexMap : {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) →
                    {i' j' k' l' : ι} →
                      (f₁' : i' ⟶ j') →
                        (f₂' : j' ⟶ k') →
                          (f₃' : k' ⟶ l') →
                            (CategoryTheory.ComposableArrows.mk₃ f₁ f₂ f₃ ⟶
                                CategoryTheory.ComposableArrows.mk₃ f₁' f₂' f₃') →
                              (n₀ n₁ n₂ : ℤ) →
                                (hn₁ :
                                    autoParam (n₀ + 1 = n₁)
                                      CategoryTheory.Abelian.SpectralObject.shortComplexMap._auto_1) →
                                  (hn₂ :
                                      autoParam (n₁ + 1 = n₂)
                                        CategoryTheory.Abelian.SpectralObject.shortComplexMap._auto_3) →
                                    X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯ ⟶ X.shortComplex f₁' f₂' f₃' n₀ n₁ n₂ ⋯ ⋯
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
CategoryTheory.Limits.WalkingParallelFamily.instDecidableEqHom : {J : Type u_1} →
  {a a_1 : CategoryTheory.Limits.WalkingParallelFamily J} →
    [DecidableEq J] → DecidableEq (CategoryTheory.Limits.WalkingParallelFamily.Hom J a a_1)
-- Mathlib.Data.List.Permutation
_private.Mathlib.Data.List.Permutation.0.List.permutationsAux.rec.match_1.splitter : {α : Type u_1} →
  (motive : List α → List α → Sort u_2) →
    (x x_1 : List α) →
      ((is : List α) → motive [] is) → ((t : α) → (ts is : List α) → motive (t :: ts) is) → motive x x_1
-- Mathlib.Algebra.Torsor.Defs
vsub_ne_zero : ∀ {G : Type u_1} {P : Type u_2} [inst : AddGroup G] [T : AddTorsor G P] {p q : P}, p -ᵥ q ≠ 0 ↔ p ≠ q
-- Mathlib.MeasureTheory.Group.Action
MeasureTheory.VAddInvariantMeasure.zero : ∀ {M : Type v} {α : Type w} [inst : MeasurableSpace α] [inst_1 : VAdd M α], MeasureTheory.VAddInvariantMeasure M α 0
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.mem_edgeSet : ∀ {V : Type u} (G : SimpleGraph V) {v w : V}, s(v, w) ∈ G.edgeSet ↔ G.Adj v w
-- Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Real.BohrMollerup.ge_logGammaSeq : ∀ {f : ℝ → ℝ} {x : ℝ} {n : ℕ},
  ConvexOn ℝ (Set.Ioi 0) f →
    (∀ {y : ℝ}, 0 < y → f (y + 1) = f y + Real.log y) → 0 < x → n ≠ 0 → f 1 + Real.BohrMollerup.logGammaSeq x n ≤ f x
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
cfcₙ_nonneg_of_predicate : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Nontrivial R] [inst_2 : StarRing R]
  [inst_3 : MetricSpace R] [inst_4 : IsTopologicalSemiring R] [inst_5 : ContinuousStar R] [inst_6 : NonUnitalRing A]
  [inst_7 : StarRing A] [inst_8 : TopologicalSpace A] [inst_9 : Module R A] [inst_10 : IsScalarTower R A A]
  [inst_11 : SMulCommClass R A A] [inst_12 : LE A] [inst_13 : NonUnitalContinuousFunctionalCalculus R A fun x => 0 ≤ x]
  {f : R → R} {a : A}, 0 ≤ cfcₙ f a
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
ModuleCat.restrictScalarsComp'App_hom_apply : ∀ {R₁ : Type u₁} {R₂ : Type u₂} {R₃ : Type u₃} [inst : Ring R₁] [inst_1 : Ring R₂] [inst_2 : Ring R₃] (f : R₁ →+* R₂)
  (g : R₂ →+* R₃) (gf : R₁ →+* R₃) (hgf : gf = g.comp f) (M : ModuleCat R₃) (x : ↑M),
  (CategoryTheory.ConcreteCategory.hom (ModuleCat.restrictScalarsComp'App f g gf hgf M).hom) x = x
-- Mathlib.Algebra.Group.End
Equiv.Perm.ofSubtype_subtypePerm : ∀ {α : Type u_4} {p : α → Prop} [inst : DecidablePred p] {f : Equiv.Perm α} (h₁ : ∀ (x : α), p (f x) ↔ p x),
  (∀ (x : α), f x ≠ x → p x) → Equiv.Perm.ofSubtype (f.subtypePerm h₁) = f
-- Aesop.RuleSet.Member
Aesop.BaseRuleSetMember.normForwardRule : Aesop.ForwardRule → Aesop.NormRule → Aesop.BaseRuleSetMember
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.Opens.mem_basicOpen_toScheme : ∀ {X : AlgebraicGeometry.Scheme} {U : X.Opens} {V : (↑U).Opens} {r : ↑((↑U).presheaf.obj (Opposite.op V))} {x : ↥U},
  x ∈ (↑U).basicOpen r ↔ ↑x ∈ X.basicOpen r
-- Mathlib.RepresentationTheory.Homological.Resolution
CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.homotopyEquiv.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {X : CategoryTheory.SimplicialObject.Augmented C}
  (ed : X.ExtraDegeneracy),
  ed.homotopyEquiv =
    { hom := AlgebraicTopology.AlternatingFaceMapComplex.ε.app X,
      inv :=
        ((AlgebraicTopology.AlternatingFaceMapComplex.obj
                  (CategoryTheory.SimplicialObject.Augmented.drop.obj X)).fromSingle₀Equiv
              (CategoryTheory.SimplicialObject.Augmented.point.obj X)).symm
          ed.s',
      homotopyHomInvId := { hom := fun i => Pi.single (i + 1) (-ed.s i), zero := ⋯, comm := ⋯ },
      homotopyInvHomId := Homotopy.ofEq ⋯ }
-- Mathlib.CategoryTheory.LiftingProperties.PushoutProduct
/-- `f □ g` lifts against `h` if and only if `f` lifts against `g ⋔ h`.  -/
CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.hasLiftingProperty_mk_iff' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPushouts C]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C] [inst_3 : CategoryTheory.MonoidalCategory C]
  [inst_4 : CategoryTheory.MonoidalClosed C] [CategoryTheory.BraidedCategory C] {A B K L X Y : C} {f : A ⟶ B}
  {g : K ⟶ L} {h : X ⟶ Y},
  CategoryTheory.HasLiftingProperty (CategoryTheory.Arrow.mk f □ CategoryTheory.Arrow.mk g).hom h ↔
    CategoryTheory.HasLiftingProperty f (Opposite.op (CategoryTheory.Arrow.mk g) ⋔ CategoryTheory.Arrow.mk h).hom
-- Std.Http.Data.Status
/-- 204 No Content
 -/
Std.Http.Status.noContent : Std.Http.Status
-- Mathlib.Order.WellFoundedSet
Set.PartiallyWellOrderedOn.insert : ∀ {α : Type u_2} {r : α → α → Prop} {s : Set α} [Std.Refl r],
  s.PartiallyWellOrderedOn r → ∀ (a : α), (insert a s).PartiallyWellOrderedOn r
-- Mathlib.CategoryTheory.Category.ULift
/-- One half of the equivalence between `C` and `ULiftHom C`.  -/
CategoryTheory.ULiftHom.down : {C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → CategoryTheory.Functor (CategoryTheory.ULiftHom C) C
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.tensor_add_left : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [inst : CommSemiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : AddCommMonoid U] [inst_5 : Module A V]
  [inst_6 : Module A W] [inst_7 : Module A U] {ρ : Representation A G V} {σ : Representation A G W}
  {τ : Representation A G U} {P : Type u_6} [inst_8 : AddCommMonoid P] [inst_9 : Module A P] {π : Representation A G P}
  (f₁ f₂ : ρ.IntertwiningMap σ) (g : τ.IntertwiningMap π), (f₁ + f₂).tensor g = f₁.tensor g + f₂.tensor g
-- Plausible.Testable
_private.Plausible.Testable.0.Plausible.elabConfig.evalConfigItem : Lean.Elab.ConfigEval.EvalConfigItem Plausible.Configuration
-- Mathlib.Algebra.Lie.SerreConstruction
CartanMatrix.Generators.F.inj : ∀ {B : Type v} {a a_1 : B}, CartanMatrix.Generators.F a = CartanMatrix.Generators.F a_1 → a = a_1
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SymbolInformation : Type
-- Lean.Util.Profile
Lean.profiler : Lean.Option Bool
-- Mathlib.Probability.Independence.Conditional
ProbabilityTheory.iCondIndepFun_iff_condExp_inter_preimage_eq_mul : ∀ {Ω : Type u_1} {ι : Type u_2} {m' mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω] {hm' : m' ≤ mΩ}
  {μ : MeasureTheory.Measure Ω} [inst_1 : MeasureTheory.IsFiniteMeasure μ] {β : ι → Type u_5}
  (m : (x : ι) → MeasurableSpace (β x)) (f : (i : ι) → Ω → β i),
  (∀ (i : ι), Measurable (f i)) →
    (ProbabilityTheory.iCondIndepFun m' hm' f μ ↔
      ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)},
        (∀ i ∈ S, MeasurableSet (sets i)) →
          μ[(⋂ i ∈ S, f i ⁻¹' sets i).indicator fun ω => 1 | m'] =ᵐ[μ]
            ∏ i ∈ S, μ[(f i ⁻¹' sets i).indicator fun ω => 1 | m'])
-- Mathlib.Analysis.Complex.CauchyIntegral
/-- **Cauchy-Goursat theorem** for a rectangle: the integral of a complex differentiable function
over the boundary of a rectangle equals zero. More precisely, if `f` is continuous on a closed
rectangle and is complex differentiable at all but countably many points of the corresponding open
rectangle, then its integral over the boundary of the rectangle equals zero.  -/
Complex.integral_boundary_rect_eq_zero_of_differentiable_on_off_countable : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (f : ℂ → E) (z w : ℂ) (s : Set ℂ),
  s.Countable →
    ContinuousOn f (Set.uIcc z.re w.re ×ℂ Set.uIcc z.im w.im) →
      (∀ x ∈ Set.Ioo (min z.re w.re) (max z.re w.re) ×ℂ Set.Ioo (min z.im w.im) (max z.im w.im) \ s,
          DifferentiableAt ℂ f x) →
        (((∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * Complex.I)) - ∫ (x : ℝ) in z.re..w.re, f (↑x + ↑w.im * Complex.I)) +
              Complex.I • ∫ (y : ℝ) in z.im..w.im, f (↑w.re + ↑y * Complex.I)) -
            Complex.I • ∫ (y : ℝ) in z.im..w.im, f (↑z.re + ↑y * Complex.I) =
          0
-- Init.Data.Int.Linear
Int.Internal.Linear.cooper_dvd_left_split.eq_1 : ∀ (ctx : Int.Internal.Linear.Context) (p₁ p₂ p₃ : Int.Internal.Linear.Poly) (d : ℤ) (k : ℕ),
  Int.Internal.Linear.cooper_dvd_left_split ctx p₁ p₂ p₃ d k =
    (Int.Internal.Linear.Poly.denote' ctx
          (((p₁.tail.mul p₂.leadCoeff).combine (p₂.tail.mul (-p₁.leadCoeff))).addConst (p₂.leadCoeff * ↑k)) ≤
        0 ∧
      p₁.leadCoeff ∣ Int.Internal.Linear.Poly.denote' ctx (p₁.tail.addConst ↑k) ∧
        p₁.leadCoeff * d ∣
          Int.Internal.Linear.Poly.denote' ctx
            (((p₁.tail.mul p₃.leadCoeff).combine (p₃.tail.mul (-p₁.leadCoeff))).addConst (p₃.leadCoeff * ↑k)))
-- Init.Data.Int.Lemmas
_private.Init.Data.Int.Lemmas.0.Int.ofNat_mul_negSucc' : ∀ (m n : ℕ), ↑m * Int.negSucc n = Int.negOfNat (m * n.succ)
-- Mathlib.MeasureTheory.Integral.IntegrableOn
MeasureTheory.integrableAtFilter_atTop_iff : ∀ {α : Type u_1} {ε : Type u_3} {mα : MeasurableSpace α} {f : α → ε} {μ : MeasureTheory.Measure α}
  [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε] [inst_2 : Preorder α] [IsDirectedOrder α] [Nonempty α],
  MeasureTheory.IntegrableAtFilter f Filter.atTop μ ↔ ∃ a, MeasureTheory.IntegrableOn f (Set.Ici a) μ
-- Mathlib.MeasureTheory.Measure.PreVariation
MeasureTheory.preVariation.sum_le' : ∀ {X : Type u_1} [inst : MeasurableSpace X] (f : Set X → ENNReal) {s : Set X},
  MeasurableSet s →
    ∀ (P : Finpartition s), (∀ p ∈ P.parts, MeasurableSet p) → ∑ p ∈ P.parts, f p ≤ MeasureTheory.preVariationFun f s
-- Lean.DocString.Parser
Lean.Doc.Parser.metadataContents.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Init.Data.UInt.Lemmas
UInt16.toUSize_ofNat' : ∀ {n : ℕ}, n < UInt16.size → (UInt16.ofNat n).toUSize = USize.ofNat n
-- Mathlib.CategoryTheory.Localization.Resolution
CategoryTheory.LocalizerMorphism.LeftResolution.mk.inj : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {inst : CategoryTheory.Category.{v_1, u_1} C₁}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} C₂} {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} {X₂ : C₂} {X₁ : C₁}
  {w : Φ.functor.obj X₁ ⟶ X₂} {hw : W₂ w} {X₁_1 : C₁} {w_1 : Φ.functor.obj X₁_1 ⟶ X₂} {hw_1 : W₂ w_1},
  { X₁ := X₁, w := w, hw := hw } = { X₁ := X₁_1, w := w_1, hw := hw_1 } → X₁ = X₁_1 ∧ w ≍ w_1
-- Init.Data.List.Lex
List.not_nil_lex_iff : ∀ {α : Type u_1} {r : α → α → Prop} {l : List α}, ¬List.Lex r [] l ↔ l = []
-- Mathlib.GroupTheory.Perm.Cycle.Type
card_support_eq_three_iff : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {σ : Equiv.Perm α}, σ.support.card = 3 ↔ σ.IsThreeCycle
-- Mathlib.Algebra.Lie.Basis.Base
LieAlgebra.Basis.coroot_eq_h' : ∀ {ι : Type u_1} {K : Type u_2} {L : Type u_3} [inst : Fintype ι] [inst_1 : Field K] [inst_2 : CharZero K]
  [inst_3 : LieRing L] [inst_4 : LieAlgebra K L] [inst_5 : FiniteDimensional K L] {H : LieSubalgebra K L}
  (b : LieAlgebra.Basis ι H) [inst_6 : LieModule.IsTriangularizable K (↥H) L] [inst_7 : LieAlgebra.IsKilling K L]
  (i : ι), LieAlgebra.IsKilling.coroot ↑↑(b.baseSupportEquiv i) = b.h' i
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenAddSubgroup.toOpens_inf : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] {U V : OpenAddSubgroup G}, ↑(U ⊓ V) = ↑U ⊓ ↑V
-- Mathlib.CategoryTheory.Localization.Resolution
CategoryTheory.LocalizerMorphism.isIso_iff_of_hasLeftResolutions : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D₂ : Type u_4} {H : Type u_5} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_4, u_4} D₂]
  [inst_3 : CategoryTheory.Category.{v_5, u_5} H] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂)
  (L₂ : CategoryTheory.Functor C₂ D₂) [L₂.IsLocalization W₂] [Φ.HasLeftResolutions] {F G : CategoryTheory.Functor D₂ H}
  (α : F ⟶ G), CategoryTheory.IsIso α ↔ ∀ (X₁ : C₁), CategoryTheory.IsIso (α.app (L₂.obj (Φ.functor.obj X₁)))
-- Mathlib.RingTheory.TensorProduct.Maps
/-- `ULift` commutes with tensor products of algebras.  -/
Algebra.TensorProduct.uliftEquiv : (R : Type u_4) →
  (S : Type u_5) →
    (A : Type u_6) →
      (B : Type u_7) →
        [inst : CommSemiring R] →
          [inst_1 : CommSemiring S] →
            [inst_2 : Algebra R S] →
              [inst_3 : Semiring A] →
                [inst_4 : Algebra R A] →
                  [inst_5 : Algebra S A] →
                    [inst_6 : IsScalarTower R S A] →
                      [inst_7 : Semiring B] →
                        [inst_8 : Algebra R B] →
                          ULift.{u₁, max u_7 u_6} (TensorProduct R A B) ≃ₐ[S]
                            TensorProduct (ULift.{u₃, u_4} R) (ULift.{u₂, u_6} A) (ULift.{u₄, u_7} B)
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roo.pairwise_toList_lt : ∀ {α : Type u} {r : Std.Roo α} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLT α]
  [inst_5 : Std.Rxo.IsAlwaysFinite α], List.Pairwise (fun a b => a < b) r.toList
-- Mathlib.RingTheory.MvPolynomial.Homogeneous
MvPolynomial.decomposition.decompose'_apply : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommSemiring R] (φ : MvPolynomial σ R) (i : ℕ),
  ↑((DirectSum.Decomposition.decompose' φ) i) = (MvPolynomial.homogeneousComponent i) φ
-- Mathlib.Analysis.RCLike.Basic
RCLike.norm_sq_re_add_conj : ∀ {K : Type u_1} [inst : RCLike K] (x : K), ‖x + (starRingEnd K) x‖ ^ 2 = RCLike.re (x + (starRingEnd K) x) ^ 2
-- Mathlib.Geometry.Manifold.Algebra.Structures
ContMDiffRing.toContMDiffMul : ∀ {𝕜 : 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] {n : WithTop ℕ∞} (I : ModelWithCorners 𝕜 E H)
  (R : Type u_4) [inst_4 : Semiring R] [inst_5 : TopologicalSpace R] [inst_6 : ChartedSpace H R]
  [h : ContMDiffRing I n R], ContMDiffMul I n R