mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
/-- **Alias** of `lt_add_of_neg_add_lt`.

---

**Alias** of the forward direction of `neg_add_lt_iff_lt_add`. -/
lt_add_of_neg_add_lt_left : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LT α] [AddLeftStrictMono α] {a b c : α}, -b + a < c → a < b + c
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Free
SheafOfModules.ιFree_mapFree : ∀ {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] {C' : Type u₂} [inst_3 : CategoryTheory.Category.{v₂, u₂} C']
  {J' : CategoryTheory.GrothendieckTopology C'} {S : CategoryTheory.Sheaf J' RingCat}
  [inst_4 : CategoryTheory.HasSheafify J' AddCommGrpCat] [inst_5 : J'.WEqualsLocallyBijective AddCommGrpCat]
  (F : CategoryTheory.Functor (SheafOfModules R) (SheafOfModules S)) (I : Type u)
  (η : SheafOfModules.unit S ⟶ F.obj (SheafOfModules.unit R)) (i : I),
  CategoryTheory.CategoryStruct.comp (SheafOfModules.ιFree i) (SheafOfModules.mapFree F I η) =
    CategoryTheory.CategoryStruct.comp η (F.map (SheafOfModules.ιFree i))
-- Mathlib.GroupTheory.FiniteIndexNormalSubgroup
FiniteIndexNormalAddSubgroup.instPartialOrder.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G],
  FiniteIndexNormalAddSubgroup.instPartialOrder = PartialOrder.ofSetLike (FiniteIndexNormalAddSubgroup G) G
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
SemiNormedGrp.explicitCokernelIso_inv_π : ∀ {X Y : SemiNormedGrp} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π f) (SemiNormedGrp.explicitCokernelIso f).inv =
    SemiNormedGrp.explicitCokernelπ f
-- Mathlib.CategoryTheory.Limits.WeakLimits.WeakEqualizers
/-- Two parallel morphisms `f` and `g` have a weak equalizer if the diagram `parallelPair f g`
has a weak limit.  -/
CategoryTheory.Limits.HasWeakEqualizer : {C : Type u_1} → [inst : CategoryTheory.Category.{v_1, u_1} C] → {X Y : C} → (X ⟶ Y) → (X ⟶ Y) → Prop
-- Mathlib.RingTheory.MvPowerSeries.Equiv
_private.Mathlib.RingTheory.MvPowerSeries.Equiv.0.MvPowerSeries.optionFunLeft_monomial : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] (x : Option σ →₀ ℕ) (r : R),
  MvPowerSeries.optionFunLeft✝ σ R ((MvPowerSeries.monomial x) r) =
    (PowerSeries.monomial (x none)) ((MvPowerSeries.monomial x.some) r)
-- Mathlib.LinearAlgebra.TensorProduct.Map
TensorProduct.map_add_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₂] (f₁ f₂ : M →ₛₗ[σ₁₂] M₂) (g : N →ₛₗ[σ₁₂] N₂),
  TensorProduct.map (f₁ + f₂) g = TensorProduct.map f₁ g + TensorProduct.map f₂ g
-- Mathlib.Topology.MetricSpace.Pseudo.Constructions
Subtype.image_closedBall : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] {p : α → Prop} (a : { a // p a }) (r : ℝ),
  Subtype.val '' Metric.closedBall a r = Metric.closedBall (↑a) r ∩ {a | p a}
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.support_update_ne_zero : ∀ {ι : Type u} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → Zero (β i)]
  [inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] (f : Π₀ (i : ι), β i) (i : ι) {b : β i},
  b ≠ 0 → (f.update i b).support = insert i f.support
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
/-- If a function is integrable with respect to a given measure `μ` then it is interval integrable
with respect to `μ` on `uIcc a b`.  -/
MeasureTheory.Integrable.intervalIntegrable : ∀ {ε : Type u_3} [inst : TopologicalSpace ε] [inst_1 : ENormedAddMonoid ε] {f : ℝ → ε} {a b : ℝ}
  {μ : MeasureTheory.Measure ℝ}, MeasureTheory.Integrable f μ → IntervalIntegrable f μ a b
-- Mathlib.CategoryTheory.Sites.LocallySurjective
CategoryTheory.Presheaf.instIsLocallySurjectiveFunToRangeSheafify : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C)
  {F₁ F₂ : CategoryTheory.Functor Cᵒᵖ (Type w)} (f : F₁ ⟶ F₂),
  CategoryTheory.Presheaf.IsLocallySurjective J (CategoryTheory.Subfunctor.toRangeSheafify J f)
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
MeasureTheory.finStronglyMeasurable_iff_stronglyMeasurable_and_exists_set_sigmaFinite : ∀ {α : Type u_5} {β : Type u_6} {f : α → β} [inst : TopologicalSpace β] [T2Space β] [inst_2 : Zero β]
  {x : MeasurableSpace α} {μ : MeasureTheory.Measure α},
  MeasureTheory.FinStronglyMeasurable f μ ↔
    MeasureTheory.StronglyMeasurable f ∧
      ∃ t, MeasurableSet t ∧ (∀ x ∈ tᶜ, f x = 0) ∧ MeasureTheory.SigmaFinite (μ.restrict t)
-- Mathlib.CategoryTheory.Monoidal.Subcategory
CategoryTheory.ObjectProperty.instMonoidalPreadditiveFullSubcategory : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (P : CategoryTheory.ObjectProperty C) [inst_2 : P.IsMonoidal] [inst_3 : CategoryTheory.Preadditive C]
  [CategoryTheory.MonoidalPreadditive C], CategoryTheory.MonoidalPreadditive P.FullSubcategory
-- Mathlib.Topology.Algebra.ConstMulAction
instContinuousConstVAddForall : ∀ {M : Type u_1} {ι : Type u_4} {γ : ι → Type u_5} [inst : (i : ι) → TopologicalSpace (γ i)]
  [inst_1 : (i : ι) → VAdd M (γ i)] [∀ (i : ι), ContinuousConstVAdd M (γ i)], ContinuousConstVAdd M ((i : ι) → γ i)
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
/-- If `c` is a pushout cocone in `Cᵒᵖ`, then `c.unop.op` is isomorphic to `c`.  -/
CategoryTheory.Limits.PushoutCocone.unopOpIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y Z : Cᵒᵖ} → {f : X ⟶ Y} → {g : X ⟶ Z} → (c : CategoryTheory.Limits.PushoutCocone f g) → c.unop.op ≅ c
-- Init.Data.Order.PackageFactories
Std.Packages.PreorderOfLEArgs.mk : {α : Type u} →
  (le : autoParam (LE α) Std.Packages.PreorderOfLEArgs.le._autoParam) →
    (decidableLE : autoParam (DecidableLE α) Std.Packages.PreorderOfLEArgs.decidableLE._autoParam) →
      (lt :
          autoParam
            (let this := le;
            LT α)
            Std.Packages.PreorderOfLEArgs.lt._autoParam) →
        (beq :
            autoParam
              (let this := le;
              let this := decidableLE;
              BEq α)
              Std.Packages.PreorderOfLEArgs.beq._autoParam) →
          (lt_iff :
              autoParam
                (let this := le;
                let this_1 := lt;
                ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a)
                Std.Packages.PreorderOfLEArgs.lt_iff._autoParam) →
            autoParam
                (let this := le;
                let this := decidableLE;
                let this := lt;
                have this_1 := lt_iff;
                DecidableLT α)
                Std.Packages.PreorderOfLEArgs.decidableLT._autoParam →
              autoParam
                  (let this := le;
                  let this_1 := decidableLE;
                  let this_2 := beq;
                  ∀ (a b : α), (a == b) = true ↔ a ≤ b ∧ b ≤ a)
                  Std.Packages.PreorderOfLEArgs.beq_iff_le_and_ge._autoParam →
                autoParam
                    (let this := le;
                    ∀ (a : α), a ≤ a)
                    Std.Packages.PreorderOfLEArgs.le_refl._autoParam →
                  autoParam
                      (let this := le;
                      ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c)
                      Std.Packages.PreorderOfLEArgs.le_trans._autoParam →
                    Std.Packages.PreorderOfLEArgs α
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.map.id' : ∀ {α : Type u} (x : FreeAddGroup α), (FreeAddGroup.map fun z => z) x = x
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- The inverse of the restriction to `ball 0 1` is continuous on the image.  -/
Topology.RelCWComplex.continuousOn_symm : ∀ {X : Type u} {inst : TopologicalSpace X} {C : Set X} {D : outParam (Set X)} [self : Topology.RelCWComplex C D] (n : ℕ)
  (i : Topology.RelCWComplex.cell C n),
  ContinuousOn (↑(Topology.RelCWComplex.map n i).symm) (Topology.RelCWComplex.map n i).target
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
CategoryTheory.CostructuredArrow.commaToGrothendieckPrecompFunctor_obj_base : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (L : CategoryTheory.Functor C D)
  (R : CategoryTheory.Functor E D) (X : CategoryTheory.Comma L R),
  ((CategoryTheory.CostructuredArrow.commaToGrothendieckPrecompFunctor L R).obj X).base = X.right
-- Init.Data.String.Lemmas.Order
String.Slice.Pos.getUTF8Byte_offset : ∀ {s : String.Slice} {p : s.Pos} {h : p.offset < s.rawEndPos}, s.getUTF8Byte p.offset h = p.byte ⋯
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.uliftCoyonedaIsoCoyoneda_hom_app_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{max w v₁, u₁} C] (X : Cᵒᵖ) (X_1 : C),
  (CategoryTheory.uliftCoyonedaIsoCoyoneda.hom.app X).app X_1 = Equiv.ulift.toIso.hom
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.image_support_finSuccEquiv : ∀ {R : Type u} [inst : CommSemiring R] {n : ℕ} {f : MvPolynomial (Fin (n + 1)) R} {i : ℕ},
  Finset.image (Finsupp.cons i) (((MvPolynomial.finSuccEquiv R n) f).coeff i).support = {m ∈ f.support | m 0 = i}
-- Std.Data.Internal.List.Associative
Std.Internal.List.perm_filter_self_iff : ∀ {α : Type u} {f : α → Bool} {l : List α}, (List.filter f l).Perm l ↔ ∀ a ∈ l, f a = true
-- Mathlib.Probability.Kernel.Disintegration.StandardBorel
/-- Auxiliary definition for `ProbabilityTheory.Kernel.condKernel`.
A conditional kernel for `κ : Kernel α (γ × Ω)` where `γ` is countably generated and `Ω` is
standard Borel.  -/
ProbabilityTheory.Kernel.condKernelBorel : {α : Type u_1} →
  {γ : Type u_3} →
    {Ω : Type u_4} →
      {mα : MeasurableSpace α} →
        {mγ : MeasurableSpace γ} →
          [MeasurableSpace.CountablyGenerated γ] →
            {mΩ : MeasurableSpace Ω} →
              [StandardBorelSpace Ω] →
                [Nonempty Ω] →
                  (κ : ProbabilityTheory.Kernel α (γ × Ω)) →
                    [ProbabilityTheory.IsFiniteKernel κ] → ProbabilityTheory.Kernel (α × γ) Ω
-- Mathlib.AlgebraicGeometry.Morphisms.Smooth
/-- **Alias** of `AlgebraicGeometry.Smooth`.

---

A morphism of schemes `f : X ⟶ Y` is smooth if for each affine `U ⊆ Y` and
`V ⊆ f ⁻¹' U`, The induced map `Γ(Y, U) ⟶ Γ(X, V)` is smooth.  -/
AlgebraicGeometry.IsSmooth : {X Y : AlgebraicGeometry.Scheme} → (X ⟶ Y) → Prop
-- Mathlib.Algebra.Group.Hom.Defs
OneHom.comp.eq_1 : ∀ {M : Type u_4} {N : Type u_5} {P : Type u_6} [inst : One M] [inst_1 : One N] [inst_2 : One P] (hnp : OneHom N P)
  (hmn : OneHom M N), hnp.comp hmn = { toFun := fun x => hnp (hmn x), map_one' := ⋯ }
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
/-- In a `p`-th cyclotomic extension of `ℚ `, we have that `ζ` is not congruent to an
integer modulo `p` if `p ≠ 2`.  -/
IsPrimitiveRoot.not_exists_int_prime_dvd_sub_of_prime_ne_two' : ∀ {p : ℕ} {K : Type u} [inst : Field K] {ζ : K} [hp : Fact (Nat.Prime p)] [inst_1 : CharZero K]
  [hcycl : IsCyclotomicExtension {p} ℚ K] (hζ : IsPrimitiveRoot ζ p), p ≠ 2 → ¬∃ n, ↑p ∣ hζ.toInteger - ↑n
-- Mathlib.Tactic.Linter.Style
/-- `findCDot stx` extracts from `stx` the syntax nodes of `kind` `Lean.Parser.Term.cdot` or `cdotTk`.
 -/
_private.Mathlib.Tactic.Linter.Style.0.Mathlib.Linter.findCDot : Lean.Syntax → Array Lean.Syntax
-- Std.Data.Iterators.Lemmas.Combinators.DropWhile
_private.Std.Data.Iterators.Lemmas.Combinators.DropWhile.0.Std.Iter.val_step_intermediateDropWhile.match_3.eq_1 : ∀ {α β : Type u_1} (motive : Std.IterStep (Std.Iter β) β → Sort u_2) (it' : Std.Iter β) (out : β)
  (h_1 : (it' : Std.Iter β) → (out : β) → motive (Std.IterStep.yield it' out))
  (h_2 : (it' : Std.Iter β) → motive (Std.IterStep.skip it')) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.yield it' out with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it' => h_2 it'
    | Std.IterStep.done => h_3 ()) =
    h_1 it' out
-- Mathlib.CategoryTheory.Idempotents.HomologicalComplex
CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_counitIso_inv : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] (α : Type u_3)
  [inst_2 : AddRightCancelSemigroup α] [inst_3 : One α],
  (CategoryTheory.Idempotents.karoubiCochainComplexEquivalence C α).counitIso.inv = CategoryTheory.eqToHom ⋯
-- Lean.Parser.Extension
/-- If the parsing stack's last element is a `set_option` command, then its value is set in the context
while parsing `p`.
 -/
Lean.Parser.withSetOptionFn : Lean.Parser.ParserFn → Lean.Parser.ParserFn
-- Mathlib.Analysis.SpecialFunctions.Log.Monotone
Real.log_div_sqrt_antitoneOn : AntitoneOn (fun x => Real.log x / √x) (Set.Ici (Real.exp 2))
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
cfcₙHom_predicate : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [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] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p] {a : A} (ha : p a)
  (f : ContinuousMapZero (↑(quasispectrum R a)) R), p ((cfcₙHom ha) f)
-- Mathlib.AlgebraicGeometry.StructureSheaf
/-- The map `M_{f y} ⟶ N_{y}` used to build maps between structure sheaves.  -/
AlgebraicGeometry.StructureSheaf.Localizations.comapFun : {R M : Type u} →
  [inst : CommRing R] →
    [inst_1 : AddCommGroup M] →
      [inst_2 : Module R M] →
        {S : Type u} →
          [inst_3 : CommRing S] →
            {N : Type u} →
              [inst_4 : AddCommGroup N] →
                [inst_5 : Module S N] →
                  {σ : R →+* S} →
                    (M →ₛₗ[σ] N) →
                      (y : ↑(AlgebraicGeometry.PrimeSpectrum.Top S)) →
                        AlgebraicGeometry.StructureSheaf.Localizations M (PrimeSpectrum.comap σ y) →ₛₗ[σ]
                          AlgebraicGeometry.StructureSheaf.Localizations N y
-- Init.Core
beq_iff_eq : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {a b : α}, (a == b) = true ↔ a = b
-- Lean.Elab.DefView
/-- An unstructured syntax object that comprises the "header" of the definition, i.e. everything up
to the value. Used as a more specific ref for header elaboration.
 -/
Lean.Elab.DefView.headerRef : Lean.Elab.DefView → Lean.Syntax
-- Mathlib.Topology.Category.Stonean.Basic
/-- Construct a term of `Stonean` from a type endowed with the structure of a
compact, Hausdorff and extremally disconnected topological space.
 -/
Stonean.of : (X : Type u_1) → [inst : TopologicalSpace X] → [CompactSpace X] → [T2Space X] → [ExtremallyDisconnected X] → Stonean
-- Mathlib.Analysis.InnerProductSpace.NormPow
Differentiable.norm_rpow : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {F : Type u_2}
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {f : F → E},
  Differentiable ℝ f → ∀ {p : ℝ}, 1 < p → Differentiable ℝ fun x => ‖f x‖ ^ p
-- Mathlib.Algebra.Algebra.Hom.Rat
/-- The equivalence between `RingEquiv` and `ℚ`-algebra isomorphisms.  -/
RingEquiv.equivRatAlgEquiv : (R : Type u_1) →
  (S : Type u_2) →
    [inst : Ring R] → [inst_1 : Ring S] → [inst_2 : Algebra ℚ R] → [inst_3 : Algebra ℚ S] → R ≃+* S ≃ R ≃ₐ[ℚ] S
-- Std.Sync.Channel
/-- Try to send a value to the channel. If this can be completed right away without blocking return
`true`; otherwise, don't send the value and return `false`.
 -/
Std.CloseableChannel.trySend : {α : Type} → Std.CloseableChannel α → α → BaseIO Bool
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
/-- Vertices of a trail with 2-edge reachable endpoints are 2-edge reachable.  -/
SimpleGraph.Walk.IsTrail.isEdgeReachable_two_of_isEdgeReachable_two : ∀ {V : Type u_1} {G : SimpleGraph V} {u v x y : V} {w : G.Walk u v},
  w.IsTrail → G.IsEdgeReachable 2 u v → x ∈ w.support → y ∈ w.support → G.IsEdgeReachable 2 x y
-- Std.Sync.CancellationToken
/-- Creates a selector that waits for cancellation.
 -/
Std.CancellationToken.selector : Std.CancellationToken → Std.Async.Selector Unit
-- Mathlib.Data.Finsupp.Lex
Finsupp.Lex.addRightStrictMono : ∀ {α : Type u_1} {N : Type u_2} [inst : LinearOrder α] [inst_1 : AddMonoid N] [inst_2 : LinearOrder N]
  [AddRightStrictMono N], AddRightStrictMono (Lex (α →₀ N))
-- Mathlib.Topology.Closure
frontier_empty : ∀ {X : Type u} [inst : TopologicalSpace X], frontier ∅ = ∅
-- Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Submodule.eq_top_iff_finrank_eq : ∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] [Module.Finite K V]
  {W : Submodule K V}, W = ⊤ ↔ Module.finrank K ↥W = Module.finrank K V
-- Mathlib.CategoryTheory.Enriched.Limits.HasConicalLimits
/-- `C` has all conical limits of size `v₁ u₁` (`HasLimitsOfSize.{v₁ u₁} C`)
if it has conical limits of every shape `J : Type u₁` with `[Category.{v₁} J]`.
 -/
CategoryTheory.Enriched.HasConicalLimitsOfSize : (V : outParam (Type u')) →
  [inst : CategoryTheory.Category.{v', u'} V] →
    [inst_1 : CategoryTheory.MonoidalCategory V] →
      (C : Type u) → [inst_2 : CategoryTheory.Category.{v, u} C] → [CategoryTheory.EnrichedOrdinaryCategory V C] → Prop
-- Mathlib.Topology.Order.UpperLowerSetTopology
/-- `toUpperSet` is the identity function to the `WithUpperSet` of a type.  -/
Topology.WithUpperSet.toUpperSet : {α : Type u_1} → α ≃ Topology.WithUpperSet α
-- Mathlib.Analysis.Meromorphic.Basic
/-- A function is meromorphic iff it is meromorphic on Set.univ.  -/
meromorphicOn_univ : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E}, MeromorphicOn f Set.univ ↔ Meromorphic f
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.d₁₂_comp_d₂₃_apply : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u_1, u, u} k G) (x : G → ↑A),
  (CategoryTheory.ConcreteCategory.hom (groupCohomology.d₂₃ A))
      ((CategoryTheory.ConcreteCategory.hom (groupCohomology.d₁₂ A)) x) =
    0
-- Mathlib.Data.Seq.Computation
_private.Mathlib.Data.Seq.Computation.0.Computation.BisimO.match_1.eq_3 : ∀ {α : Type u_1} (motive : α ⊕ Computation α → α ⊕ Computation α → Sort u_2) (x x_1 : α ⊕ Computation α)
  (h_1 : (a a' : α) → motive (Sum.inl a) (Sum.inl a')) (h_2 : (s s' : Computation α) → motive (Sum.inr s) (Sum.inr s'))
  (h_3 : (x x_2 : α ⊕ Computation α) → motive x x_2),
  (∀ (a a' : α), x = Sum.inl a → x_1 = Sum.inl a' → False) →
    (∀ (s s' : Computation α), x = Sum.inr s → x_1 = Sum.inr s' → False) →
      (match x, x_1 with
        | Sum.inl a, Sum.inl a' => h_1 a a'
        | Sum.inr s, Sum.inr s' => h_2 s s'
        | x, x_4 => h_3 x x_4) =
        h_3 x x_1
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.mem_of_mem_union_of_not_mem_left : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [EquivBEq α] [LawfulHashable α],
  m₁.WF → m₂.WF → ∀ {k : α}, k ∈ m₁ ∪ m₂ → k ∉ m₁ → k ∈ m₂
-- Init.Data.Nat.Basic
Nat.eq_zero_of_add_eq_zero : ∀ {n m : ℕ}, n + m = 0 → n = 0 ∧ m = 0
-- Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
WeierstrassCurve.HasMultiplicativeReduction.not_hasAdditiveReduction : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsDiscreteValuationRing R] {K : Type u_2}
  [inst_3 : Field K] [inst_4 : Algebra R K] [inst_5 : IsFractionRing R K] {W : WeierstrassCurve K},
  WeierstrassCurve.HasMultiplicativeReduction R W → ¬WeierstrassCurve.HasAdditiveReduction R W
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
HasSumUniformlyOn.hasSumLocallyUniformlyOn : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : AddCommMonoid α] {f : ι → β → α} {g : β → α} {s : Set β}
  [inst_1 : UniformSpace α] [inst_2 : TopologicalSpace β], HasSumUniformlyOn f g s → HasSumLocallyUniformlyOn f g s
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.minKey!_eq_minKeyD_default : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.minKey! = t.minKeyD default
-- Mathlib.CategoryTheory.Sites.Continuous
/-- The functor `F.sheafPushforwardContinuous A J K : Sheaf K A ⥤ Sheaf J A`
is induced by the precomposition with `F.op`.  -/
CategoryTheory.Functor.sheafPushforwardContinuousCompSheafToPresheafIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C D) →
          (A : Type u) →
            [inst_2 : CategoryTheory.Category.{t, u} A] →
              (J : CategoryTheory.GrothendieckTopology C) →
                (K : CategoryTheory.GrothendieckTopology D) →
                  [inst_3 : F.IsContinuous J K] →
                    (F.sheafPushforwardContinuous A J K).comp (CategoryTheory.sheafToPresheaf J A) ≅
                      (CategoryTheory.sheafToPresheaf K A).comp
                        ((CategoryTheory.Functor.whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj F.op)
-- Mathlib.Data.Seq.Basic
Stream'.Seq.ofStream_append : ∀ {α : Type u} (l : List α) (s : Stream' α), ↑(l ++ₛ s) = (↑l).append ↑s
-- Mathlib.Analysis.Complex.ReImTopology
Complex.frontier_setOfPred_le_re : ∀ (a : ℝ), frontier {z | a ≤ z.re} = {z | z.re = a}
-- Lean.Server.Completion.SyntheticCompletion
_private.Lean.Server.Completion.SyntheticCompletion.0.Lean.Server.Completion.findOutermostContextInfo? : Lean.Elab.InfoTree → Option Lean.Elab.ContextInfo
-- Mathlib.Analysis.Normed.Module.FiniteDimension
/-- An affine isometry between finite-dimensional spaces of equal dimension can be upgraded
to an affine isometry equivalence.  -/
AffineIsometry.toAffineIsometryEquiv : {𝕜 : Type u_1} →
  {V₁ : Type u_2} →
    {V₂ : Type u_3} →
      {P₁ : Type u_4} →
        {P₂ : Type u_5} →
          [inst : NormedField 𝕜] →
            [inst_1 : NormedAddCommGroup V₁] →
              [inst_2 : SeminormedAddCommGroup V₂] →
                [inst_3 : NormedSpace 𝕜 V₁] →
                  [inst_4 : NormedSpace 𝕜 V₂] →
                    [inst_5 : MetricSpace P₁] →
                      [inst_6 : PseudoMetricSpace P₂] →
                        [inst_7 : NormedAddTorsor V₁ P₁] →
                          [inst_8 : NormedAddTorsor V₂ P₂] →
                            [FiniteDimensional 𝕜 V₁] →
                              [FiniteDimensional 𝕜 V₂] →
                                [Inhabited P₁] →
                                  (P₁ →ᵃⁱ[𝕜] P₂) → Module.finrank 𝕜 V₁ = Module.finrank 𝕜 V₂ → P₁ ≃ᵃⁱ[𝕜] P₂
-- Mathlib.LinearAlgebra.AffineSpace.Combination
/-- Affine maps commute with affine combinations.  -/
Finset.map_affineCombination : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) {V₂ : Type u_6} {P₂ : Type u_7} [inst_3 : AddCommGroup V₂]
  [inst_4 : Module k V₂] [inst_5 : AddTorsor V₂ P₂] (p : ι → P) (w : ι → k),
  s.sum w = 1 → ∀ (f : P →ᵃ[k] P₂), f ((Finset.affineCombination k s p) w) = (Finset.affineCombination k s (⇑f ∘ p)) w
-- Mathlib.LinearAlgebra.Matrix.DotProduct
/-- Note that this applies to `ℂ` via `RCLike.toStarOrderedRing`.  -/
Matrix.dotProduct_star_self_pos_iff : ∀ {n : Type u_2} {R : Type u_4} [inst : Fintype n] [inst_1 : PartialOrder R] [inst_2 : NonUnitalRing R]
  [inst_3 : StarRing R] [StarOrderedRing R] [NoZeroDivisors R] {v : n → R}, 0 < star v ⬝ᵥ v ↔ v ≠ 0
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
EisensteinSeries.summable_e2Summand_symmetricIcc : ∀ (z : UpperHalfPlane), Summable (fun x => EisensteinSeries.e2Summand x z) (SummationFilter.symmetricIcc ℤ)
-- Mathlib.Order.Max
IsMin.fst : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {x : α × β}, IsMin x → IsMin x.1