mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.UniformSpace.Closeds
/-- When `Set` is equipped with the Hausdorff uniformity, taking the image under a uniform
embedding is a uniform embedding.  -/
IsUniformEmbedding.image_hausdorff : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : UniformSpace β] {f : α → β},
  IsUniformEmbedding f → IsUniformEmbedding fun x => f '' x
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
IntermediateField.AdjoinSimple.isIntegral_gen : ∀ (F : Type u_1) [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] (α : E),
  IsIntegral F (IntermediateField.AdjoinSimple.gen F α) ↔ IsIntegral F α
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
extChartAt_target_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} [inst_5 : ChartedSpace H M] {x y : M},
  y ∈ (extChartAt I x).source → (extChartAt I x).target ∈ nhdsWithin (↑(extChartAt I x) y) (Set.range ↑I)
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rco.getElem_toList_eq : ∀ {α : Type u} {r : Std.Rco α} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerableLT α]
  [inst_5 : Std.Rxo.IsAlwaysFinite α] {i : ℕ} {h : i < r.toList.length},
  r.toList[i] = (Std.PRange.succMany? i r.lower).get ⋯
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.mkOfOplax'_mapComp_hom : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.OplaxFunctor B C) [inst_2 : ∀ (a : B), CategoryTheory.IsIso (F.mapId a)]
  [inst_3 : ∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), CategoryTheory.IsIso (F.mapComp f g)] {a b c : B} (f : a ⟶ b)
  (g : b ⟶ c), ((CategoryTheory.Pseudofunctor.mkOfOplax' F).mapComp f g).hom = F.mapComp f g
-- Lean.Declaration
/-- Number of indices  -/
Lean.RecursorVal.numIndices : Lean.RecursorVal → ℕ
-- Lean.Data.Lsp.Extra
Lean.Lsp.instToJsonLeanFileProgressKind : Lean.ToJson Lean.Lsp.LeanFileProgressKind
-- Mathlib.Algebra.Group.Basic
inv_ne_one : ∀ {α : Type u_1} [inst : DivisionMonoid α] {a : α}, a⁻¹ ≠ 1 ↔ a ≠ 1
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.mapShortComplexH2_comp_assoc : ∀ {k : Type u} [inst : CommRing k] {G H K : Type u} [inst_1 : Group G] [inst_2 : Group H] [inst_3 : Group K]
  {A : Rep.{u_1, u, u} k K} {B : Rep.{u_1, u, u} k H} {C : Rep.{u_1, u, u} k G} (f : H →* K) (g : G →* H)
  (φ : Rep.res f A ⟶ B) (ψ : Rep.res g B ⟶ C) {Z : CategoryTheory.ShortComplex (ModuleCat k)}
  (h : groupCohomology.shortComplexH2 C ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (groupCohomology.mapShortComplexH2 (f.comp g) (CategoryTheory.CategoryStruct.comp (Rep.resMap g φ) ψ)) h =
    CategoryTheory.CategoryStruct.comp (groupCohomology.mapShortComplexH2 f φ)
      (CategoryTheory.CategoryStruct.comp (groupCohomology.mapShortComplexH2 g ψ) h)
-- Mathlib.Data.Fin.Tuple.Curry
Function.OfArity.uncurry_curry : ∀ {α β : Type u} {n : ℕ} (f : (Fin n → α) → β), (Function.OfArity.curry f).uncurry = f
-- Mathlib.CategoryTheory.Join.Basic
/-- A natural isomorphism `Fᵣ ≅ Gᵣ` induces a natural isomorphism
`mapPair Fₗ H ≅ mapPair Gₗ H` for every `H : C ⥤ E`.  -/
CategoryTheory.Join.mapIsoWhiskerRight : {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] →
            {E' : Type u₄} →
              [inst_3 : CategoryTheory.Category.{v₄, u₄} E'] →
                {Fₗ Gₗ : CategoryTheory.Functor C E} →
                  (Fₗ ≅ Gₗ) →
                    (H : CategoryTheory.Functor D E') →
                      CategoryTheory.Join.mapPair Fₗ H ≅ CategoryTheory.Join.mapPair Gₗ H
-- Mathlib.Topology.Instances.Matrix
HasSum.matrix_transpose : ∀ {X : Type u_1} {m : Type u_4} {n : Type u_5} {R : Type u_8} [inst : AddCommMonoid R] [inst_1 : TopologicalSpace R]
  {L : SummationFilter X} {f : X → Matrix m n R} {a : Matrix m n R},
  HasSum f a L → HasSum (fun x => (f x).transpose) a.transpose L
-- Mathlib.LinearAlgebra.Matrix.WithConv
instSMulCommClassWithConvMatrix : ∀ {m : Type u_1} {n : Type u_2} {α : Type u_3} {β : Type u_4} [inst : Monoid β] [inst_1 : MulAction β α]
  [inst_2 : Mul α] [SMulCommClass β α α], SMulCommClass β (WithConv (Matrix m n α)) (WithConv (Matrix m n α))
-- Mathlib.Algebra.AddConstMap.Basic
AddConstMap.coe_conjNeg_apply : ∀ {G : Type u_1} {H : Type u_2} [inst : AddCommGroup G] [inst_1 : AddCommGroup H] {a : G} {b : H}
  (f : AddConstMap G H a b) (x : G), (AddConstMap.conjNeg f) x = -f (-x)
-- Mathlib.GroupTheory.Coset.Basic
mem_leftCoset_iff : ∀ {α : Type u_1} [inst : Group α] {s : Set α} {x : α} (a : α), x ∈ a • s ↔ a⁻¹ * x ∈ s
-- Mathlib.Topology.Algebra.ContinuousAffineMap
/-- The identity map as a continuous affine map  -/
ContinuousAffineMap.id : (R : Type u_1) →
  {V : Type u_2} →
    (P : Type u_4) →
      [inst : Ring R] →
        [inst_1 : AddCommGroup V] →
          [inst_2 : Module R V] → [inst_3 : TopologicalSpace P] → [inst_4 : AddTorsor V P] → P →ᴬ[R] P
-- Mathlib.Data.Nat.Fib.Zeckendorf
Nat.sum_zeckendorf_fib : ∀ (n : ℕ), (List.map Nat.fib n.zeckendorf).sum = n
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.DTreeMap.Internal.Impl.insertMin.match_3.eq_2 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : (t : Std.DTreeMap.Internal.Impl α β) → t.Balanced → Sort u_3) (sz : ℕ)
  (k' : α) (v' : β k') (l' r' : Std.DTreeMap.Internal.Impl α β)
  (hr : (Std.DTreeMap.Internal.Impl.inner sz k' v' l' r').Balanced)
  (h_1 : (hr : Std.DTreeMap.Internal.Impl.leaf.Balanced) → motive Std.DTreeMap.Internal.Impl.leaf hr)
  (h_2 :
    (sz : ℕ) →
      (k' : α) →
        (v' : β k') →
          (l' r' : Std.DTreeMap.Internal.Impl α β) →
            (hr : (Std.DTreeMap.Internal.Impl.inner sz k' v' l' r').Balanced) →
              motive (Std.DTreeMap.Internal.Impl.inner sz k' v' l' r') hr),
  (match Std.DTreeMap.Internal.Impl.inner sz k' v' l' r', hr with
    | Std.DTreeMap.Internal.Impl.leaf, hr => h_1 hr
    | Std.DTreeMap.Internal.Impl.inner sz k' v' l' r', hr => h_2 sz k' v' l' r' hr) =
    h_2 sz k' v' l' r' hr
-- Mathlib.Algebra.Category.HopfAlgCat.Monoidal
/-- `forget₂ (HopfAlgCat R) (BialgCat R)` is a monoidal functor.  -/
HopfAlgCat.instMonoidalBialgCatForget₂BialgHomCarrierCarrier : (R : Type u) → [inst : CommRing R] → (CategoryTheory.forget₂ (HopfAlgCat R) (BialgCat R)).Monoidal
-- Mathlib.CategoryTheory.Limits.Shapes.Products
/-- Two coproducts which differ by an equivalence in the indexing type,
and up to isomorphism in the factors, are isomorphic.
 -/
CategoryTheory.Limits.Sigma.whiskerEquiv : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type u_1} →
      {K : Type u_2} →
        {f : J → C} →
          {g : K → C} →
            (e : J ≃ K) →
              ((j : J) → g (e j) ≅ f j) →
                [inst_1 : CategoryTheory.Limits.HasCoproduct f] →
                  [inst_2 : CategoryTheory.Limits.HasCoproduct g] → ∐ f ≅ ∐ g
-- Mathlib.RingTheory.Algebraic.Basic
Polynomial.algEquivOfTranscendental_symm_gen : ∀ (R : Type u_1) {S : Type u_2} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] (s : S)
  (h : Transcendental R s), (Polynomial.algEquivOfTranscendental R s h).symm ⟨s, ⋯⟩ = Polynomial.X
-- Mathlib.Topology.Inseparable
/-- The natural map from a topological space to its separation quotient.  -/
SeparationQuotient.mk : {X : Type u_1} → [inst : TopologicalSpace X] → X → SeparationQuotient X
-- Mathlib.Order.RelSeries
/-- End of a series, i.e. for `a₀ -r→ a₁ -r→ ... -r→ aₙ`, its last element is `aₙ`.

Since a relation series is assumed to be non-empty, this is well defined.  -/
RelSeries.last : {α : Type u_1} → {r : SetRel α α} → RelSeries r → α
-- Mathlib.Order.SuccPred.Basic
Order.Ici_subset_Ioi_pred_of_not_isMin : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : PredOrder α] {a : α}, ¬IsMin a → Set.Ici a ⊆ Set.Ioi (Order.pred a)
-- Mathlib.Topology.Algebra.Monoid
mulHomOfTendsto_apply : ∀ {α : Type u_2} {M₁ : Type u_6} {M₂ : Type u_7} [inst : TopologicalSpace M₂] [inst_1 : T2Space M₂] [inst_2 : Mul M₁]
  [inst_3 : Mul M₂] [inst_4 : ContinuousMul M₂] {F : Type u_8} [inst_5 : FunLike F M₁ M₂] [inst_6 : MulHomClass F M₁ M₂]
  {l : Filter α} (f : M₁ → M₂) (g : α → F) [inst_7 : l.NeBot] (h : Filter.Tendsto (fun a x => (g a) x) l (nhds f)),
  ⇑(mulHomOfTendsto f g h) = f
-- Mathlib.Data.PNat.Xgcd
PNat.gcd_props : ∀ (a b : ℕ+),
  have d := a.gcdD b;
  have w := a.gcdW b;
  have x := a.gcdX b;
  have y := a.gcdY b;
  have z := a.gcdZ b;
  have a' := a.gcdA' b;
  have b' := a.gcdB' b;
  w * z = (x * y).succPNat ∧
    a = a' * d ∧
      b = b' * d ∧
        z * a' = (x * ↑b').succPNat ∧ w * b' = (y * ↑a').succPNat ∧ ↑z * ↑a = x * ↑b + ↑d ∧ ↑w * ↑b = y * ↑a + ↑d
-- Mathlib.Analysis.MeanInequalities
/-- **Hölder inequality**: the scalar product of two functions is bounded by the product of their
`L^p` and `L^q` norms when `p` and `q` are conjugate exponents. Version for sums over finite sets,
with `ℝ≥0∞`-valued functions.  -/
ENNReal.inner_le_Lp_mul_Lq : ∀ {ι : Type u} (s : Finset ι) (f g : ι → ENNReal) {p q : ℝ},
  p.HolderConjugate q → ∑ i ∈ s, f i * g i ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p) * (∑ i ∈ s, g i ^ q) ^ (1 / q)
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.eatSpaces : Lean.Parser.ParserFn
-- Init.Data.Array.Lemmas
Array.getElem?_push_lt : ∀ {α : Type u_1} {xs : Array α} {x : α} {i : ℕ} (h : i < xs.size), (xs.push x)[i]? = some xs[i]
-- Std.Internal.Parsec.Basic
Std.Internal.Parsec.ParseResult.error.injEq : ∀ {α ι : Type} (pos : ι) (err : Std.Internal.Parsec.Error) (pos_1 : ι) (err_1 : Std.Internal.Parsec.Error),
  (Std.Internal.Parsec.ParseResult.error pos err = Std.Internal.Parsec.ParseResult.error pos_1 err_1) =
    (pos = pos_1 ∧ err = err_1)
-- Lean.Parser.Command
Lean.Parser.Command.openOnly : Lean.Parser.Parser
-- Init.Data.AC
Lean.Data.AC.mergeIdem.loop.eq_def : ∀ (a : ℕ) (a_1 : List ℕ),
  Lean.Data.AC.mergeIdem.loop a a_1 =
    match a, a_1 with
    | curr, next :: rest =>
      if curr = next then Lean.Data.AC.mergeIdem.loop curr rest else curr :: Lean.Data.AC.mergeIdem.loop next rest
    | curr, [] => [curr]
-- Mathlib.Logic.Basic
forall_and_right : ∀ {α : Sort u_1} [Nonempty α] (p : α → Prop) (q : Prop), (∀ (x : α), p x ∧ q) ↔ (∀ (x : α), p x) ∧ q
-- Lean.Meta.ArgsPacker
/-- Given `value : type` where `type` is
```
(m : (x : a ⊗' b ⊕' c ⊗' d) → s[x]) → r[m]
```
brings `m1 : (x : a) → (y : b) → s[.inl ⟨x,y⟩]` and `m2 : (x : c) → (y : d) → s[.inr ⟨x,y⟩]` into scope. The continuation receives

 * FVars for `m1`…
 * `e[m]`
 * `t[m]`

where `m : a ⊗' b ⊕' c ⊗' d → s` is the uncurried form of `m1` and `m2`.

The variable names `m1` and `m2` are taken from the parameter name in `t`, with numbers added
unless `numFuns = 1`
 -/
Lean.Meta.ArgsPacker.curryParam : {α : Type} →
  Lean.Meta.ArgsPacker → Lean.Expr → Lean.Expr → (Array Lean.Expr → Lean.Expr → Lean.Expr → Lean.MetaM α) → Lean.MetaM α
-- Mathlib.CategoryTheory.ObjectProperty.Equivalence
CategoryTheory.ObjectProperty.isEquivalence_ιOfLE_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P Q : CategoryTheory.ObjectProperty C} (h : P ≤ Q),
  (CategoryTheory.ObjectProperty.ιOfLE h).IsEquivalence ↔ Q ≤ P.isoClosure
-- Mathlib.CategoryTheory.Bicategory.Kan.HasKan
CategoryTheory.Bicategory.LanLift.existsUnique : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a}
  [inst_1 : CategoryTheory.Bicategory.HasLeftKanLift f g] (s : CategoryTheory.Bicategory.LeftLift f g),
  ∃! τ,
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.lanLiftUnit f g)
        (CategoryTheory.Bicategory.whiskerRight τ f) =
      s.unit
-- Init.Data.List.Lemmas
List.append_inj : ∀ {α : Type u_1} {s₁ s₂ t₁ t₂ : List α}, s₁ ++ t₁ = s₂ ++ t₂ → s₁.length = s₂.length → s₁ = s₂ ∧ t₁ = t₂
-- Mathlib.Algebra.Order.Antidiag.Prod
Finset.HasAntidiagonal.congr : ∀ (A : Type u_2) [inst : AddMonoid A] [H1 : Finset.HasAntidiagonal A] [H2 : Finset.HasAntidiagonal A],
  Finset.HasAntidiagonal.antidiagonal = Finset.HasAntidiagonal.antidiagonal
-- Mathlib.Geometry.Euclidean.Incenter
/-- **Alias** of the reverse direction of `Affine.Simplex.sum_excenterWeights_eq_one_iff`. -/
Affine.Simplex.ExcenterExists.sum_excenterWeights_eq_one : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n) {signs : Finset (Fin (n + 1))},
  s.ExcenterExists signs → ∑ i, s.excenterWeights signs i = 1
-- Mathlib.CategoryTheory.Limits.Cones
/-- Cocones on `F : Jᵒᵖ ⥤ Cᵒᵖ` are equivalent to cones on `F.unop : J ⥤ C`.  -/
CategoryTheory.Limits.coneUnopOfCoconeEquiv : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ} → (CategoryTheory.Limits.Cocone F)ᵒᵖ ≌ CategoryTheory.Limits.Cone F.unop
-- Mathlib.Order.Partition.Basic
Partition.subset_of_mem : ∀ {α : Type u_1} {u t : Set α} {P : Partition u}, t ∈ P → t ⊆ u
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
CategoryTheory.Functor.RightExtension.coneAtFunctor_map_hom : ∀ {C : Type u_1} {D : Type u_2} {H : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_4, u_4} H]
  (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H) (Y : D) {E E' : L.RightExtension F} (φ : E ⟶ E'),
  ((CategoryTheory.Functor.RightExtension.coneAtFunctor L F Y).map φ).hom = φ.left.app Y
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Matrix.GeneralLinearGroup.parabolicEigenvalue_ne_zero : ∀ {K : Type u_2} [inst : Field K] {g : GL (Fin 2) K} [NeZero 2], g.IsParabolic → (↑g).parabolicEigenvalue ≠ 0
-- Mathlib.RingTheory.Norm.Transitivity
Algebra.Norm.Transitivity.mul_auxMat_toSquareBlock_eq : ∀ {S : Type u_2} {m : Type u_5} [inst : CommRing S] (M : Matrix m m S) [inst_1 : DecidableEq m] (k : m)
  [inst_2 : Fintype m], (M * Algebra.Norm.Transitivity.auxMat M k).toSquareBlock (fun x => x = k) True = M k k • 1
-- Init.Data.String.Defs
String.Slice.utf8ByteSize_eq : ∀ {s : String.Slice}, s.utf8ByteSize = s.endExclusive.offset.byteIdx - s.startInclusive.offset.byteIdx
-- Mathlib.Data.List.TakeDrop
List.drop_take_append_drop : ∀ {α : Type u} (x : List α) (m n : ℕ), List.take n (List.drop m x) ++ List.drop (m + n) x = List.drop m x
-- Mathlib.Combinatorics.Quiver.Push
/-- The quiver structure obtained by pushing arrows of `V` along the map `σ : V → W`  -/
Quiver.PushQuiver : {V : Type u} → [Quiver V] → {W : Type u₂} → (V → W) → W → W → Type (max u u₂ v)
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
MeasureTheory.FiniteMeasure.zero_mass : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω], MeasureTheory.FiniteMeasure.mass 0 = 0
-- Mathlib.Algebra.Homology.ShortComplex.Basic
CategoryTheory.ShortComplex.Hom.mk.inj : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {inst_1 : CategoryTheory.Limits.HasZeroMorphisms C}
  {S₁ S₂ : CategoryTheory.ShortComplex C} {τ₁ : S₁.X₁ ⟶ S₂.X₁} {τ₂ : S₁.X₂ ⟶ S₂.X₂} {τ₃ : S₁.X₃ ⟶ S₂.X₃}
  {comm₁₂ :
    autoParam (CategoryTheory.CategoryStruct.comp τ₁ S₂.f = CategoryTheory.CategoryStruct.comp S₁.f τ₂)
      CategoryTheory.ShortComplex.Hom.comm₁₂._autoParam}
  {comm₂₃ :
    autoParam (CategoryTheory.CategoryStruct.comp τ₂ S₂.g = CategoryTheory.CategoryStruct.comp S₁.g τ₃)
      CategoryTheory.ShortComplex.Hom.comm₂₃._autoParam}
  {τ₁_1 : S₁.X₁ ⟶ S₂.X₁} {τ₂_1 : S₁.X₂ ⟶ S₂.X₂} {τ₃_1 : S₁.X₃ ⟶ S₂.X₃}
  {comm₁₂_1 :
    autoParam (CategoryTheory.CategoryStruct.comp τ₁_1 S₂.f = CategoryTheory.CategoryStruct.comp S₁.f τ₂_1)
      CategoryTheory.ShortComplex.Hom.comm₁₂._autoParam}
  {comm₂₃_1 :
    autoParam (CategoryTheory.CategoryStruct.comp τ₂_1 S₂.g = CategoryTheory.CategoryStruct.comp S₁.g τ₃_1)
      CategoryTheory.ShortComplex.Hom.comm₂₃._autoParam},
  { τ₁ := τ₁, τ₂ := τ₂, τ₃ := τ₃, comm₁₂ := comm₁₂, comm₂₃ := comm₂₃ } =
      { τ₁ := τ₁_1, τ₂ := τ₂_1, τ₃ := τ₃_1, comm₁₂ := comm₁₂_1, comm₂₃ := comm₂₃_1 } →
    τ₁ = τ₁_1 ∧ τ₂ = τ₂_1 ∧ τ₃ = τ₃_1
-- Mathlib.Topology.Algebra.InfiniteSum.Group
HasProd.div₀ : ∀ {α : Type u_1} {K : Type u_4} [inst : CommGroupWithZero K] [inst_1 : TopologicalSpace K] {f g : α → K}
  {L : SummationFilter α} [ContinuousInv₀ K] [ContinuousMul K] {a b : K},
  HasProd f a L → HasProd g b L → b ≠ 0 → HasProd (fun x => f x / g x) (a / b) L
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.instAddHom : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] → {S₁ S₂ : CategoryTheory.ShortComplex C} → Add (S₁ ⟶ S₂)
-- Mathlib.GroupTheory.GroupAction.Period
/-- If the action is periodic, then a lower bound for its period can be computed.  -/
AddAction.le_period : ∀ {α : Type v} {M : Type u} [inst : AddMonoid M] [inst_1 : AddAction M α] {m : M} {a : α} {n : ℕ},
  0 < AddAction.period m a → (∀ (k : ℕ), 0 < k → k < n → k • m +ᵥ a ≠ a) → n ≤ AddAction.period m a
-- Mathlib.Analysis.Normed.Algebra.Basic
WeakDual.CharacterSpace.norm_le_norm_one : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedRing A] [inst_2 : NormedAlgebra 𝕜 A]
  [CompleteSpace A] (φ : ↑(WeakDual.characterSpace 𝕜 A)), ‖WeakDual.toStrongDual ↑φ‖ ≤ ‖1‖
-- Mathlib.Algebra.BigOperators.Intervals
Finset.sum_Ico_eq_sub : ∀ {δ : Type u_4} [inst : AddCommGroup δ] (f : ℕ → δ) {m n : ℕ},
  m ≤ n → ∑ k ∈ Finset.Ico m n, f k = ∑ k ∈ Finset.range n, f k - ∑ k ∈ Finset.range m, f k
-- Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
AlgebraicIndependent.matroid_cRank_eq : ∀ (R : Type u_1) (A : Type w) [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [inst_3 : FaithfulSMul R A] [inst_4 : NoZeroDivisors A], (AlgebraicIndependent.matroid R A).cRank = Algebra.trdeg R A
-- Lean.Structure
Lean.StructureInfo.mk.sizeOf_spec : ∀ (structName : Lean.Name) (fieldNames : Array Lean.Name) (fieldInfo : Array Lean.StructureFieldInfo)
  (parentInfo : Array Lean.StructureParentInfo),
  sizeOf { structName := structName, fieldNames := fieldNames, fieldInfo := fieldInfo, parentInfo := parentInfo } =
    1 + sizeOf structName + sizeOf fieldNames + sizeOf fieldInfo + sizeOf parentInfo
-- Mathlib.Algebra.Module.LocalizedModule.Basic
IsLocalizedModule.map_mk' : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M'] [inst_3 : Module R M] [inst_4 : Module R M'] (f : M →ₗ[R] M')
  [inst_5 : IsLocalizedModule S f] {N : Type u_6} {N' : Type u_7} [inst_6 : AddCommMonoid N] [inst_7 : AddCommMonoid N']
  [inst_8 : Module R N] [inst_9 : Module R N'] (g : N →ₗ[R] N') [inst_10 : IsLocalizedModule S g] (h : M →ₗ[R] N)
  (x : M) (s : ↥S), ((IsLocalizedModule.map S f g) h) (IsLocalizedModule.mk' f x s) = IsLocalizedModule.mk' g (h x) s
-- Mathlib.Algebra.Module.Equiv.Basic
Units.toEquiv_mulLeftLinearEquiv : ∀ {R : Type u_9} {A : Type u_10} [inst : Semiring R] [inst_1 : Semiring A] [inst_2 : Module R A]
  [inst_3 : SMulCommClass R A A] (u : Aˣ), ((Units.mulLeftLinearEquiv R A) u).toEquiv = u.mulLeft
-- Init.PropLemmas
or_iff_right : ∀ {a b : Prop}, ¬a → (a ∨ b ↔ b)
-- Mathlib.Algebra.Homology.Embedding.Connect
/-- Connecting complexes is functorial.  -/
CochainComplex.ConnectData.map : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {K K' : ChainComplex C ℕ} →
        {L L' : CochainComplex C ℕ} →
          (h : CochainComplex.ConnectData K L) →
            (h' : CochainComplex.ConnectData K' L') →
              (fK : K ⟶ K') →
                (fL : L ⟶ L') →
                  CategoryTheory.CategoryStruct.comp (fK.f 0) h'.d₀ = CategoryTheory.CategoryStruct.comp h.d₀ (fL.f 0) →
                    (h.cochainComplex ⟶ h'.cochainComplex)
-- Mathlib.LinearAlgebra.Matrix.RowCol
Matrix.diagonal_updateRow_single : ∀ {n : Type u_3} {α : Type v} [inst : DecidableEq n] [inst_1 : Zero α] (v : n → α) (i : n) (x : α),
  (Matrix.diagonal v).updateRow i (Pi.single i x) = Matrix.diagonal (Function.update v i x)
-- Mathlib.Algebra.Algebra.Operations
/-- The ring of submodules of the opposite algebra is isomorphic to the opposite ring of
submodules.  -/
Submodule.equivOpposite : {R : Type u} →
  [inst : CommSemiring R] →
    {A : Type v} → [inst_1 : Semiring A] → [inst_2 : Algebra R A] → Submodule R Aᵐᵒᵖ ≃+* (Submodule R A)ᵐᵒᵖ
-- Mathlib.Order.WithBot
WithTop.ne_top_iff_exists : ∀ {α : Type u_1} {x : WithTop α}, x ≠ ⊤ ↔ ∃ a, ↑a = x
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.toListModel_insertₘ : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  {m : Std.DHashMap.Internal.Raw₀ α β},
  Std.DHashMap.Internal.Raw.WFImp ↑m →
    ∀ {a : α} {b : β a},
      (Std.DHashMap.Internal.toListModel (↑(m.insertₘ a b)).buckets).Perm
        (Std.Internal.List.insertEntry a b (Std.DHashMap.Internal.toListModel (↑m).buckets))
-- Mathlib.Algebra.Ring.WithZero
WithZero.instDistrib : {α : Type u_1} → [Distrib α] → Distrib (WithZero α)
-- Init.Data.List.Nat.Modify
List.modify_eq_self : ∀ {α : Type u_1} {f : α → α} {i : ℕ} {l : List α}, l.length ≤ i → l.modify i f = l
-- Mathlib.Geometry.RingedSpace.PresheafedSpace
AlgebraicGeometry.PresheafedSpace.forget_obj : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] (X : AlgebraicGeometry.PresheafedSpace C),
  (AlgebraicGeometry.PresheafedSpace.forget C).obj X = ↑X
-- Mathlib.Algebra.Group.Subgroup.Defs
/-- An `AddSubgroup` of an `AddGroup` inherits an `AddGroup` structure.  -/
AddSubgroup.toAddGroup : {G : Type u_3} → [inst : AddGroup G] → (H : AddSubgroup G) → AddGroup ↥H
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.comp₂Measurable_eq_mk : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α}
  [inst_1 : TopologicalSpace δ] [inst_2 : TopologicalSpace β] [inst_3 : TopologicalSpace γ] [inst_4 : MeasurableSpace β]
  [inst_5 : TopologicalSpace.PseudoMetrizableSpace β] [inst_6 : BorelSpace β] [inst_7 : MeasurableSpace γ]
  [inst_8 : TopologicalSpace.PseudoMetrizableSpace γ] [inst_9 : BorelSpace γ]
  [inst_10 : SecondCountableTopologyEither β γ] [inst_11 : MeasurableSpace δ]
  [inst_12 : TopologicalSpace.PseudoMetrizableSpace δ] [inst_13 : OpensMeasurableSpace δ]
  [inst_14 : SecondCountableTopology δ] (g : β → γ → δ) (hg : Measurable (Function.uncurry g)) (f₁ : α →ₘ[μ] β)
  (f₂ : α →ₘ[μ] γ),
  MeasureTheory.AEEqFun.comp₂Measurable g hg f₁ f₂ = MeasureTheory.AEEqFun.mk (fun a => g (↑f₁ a) (↑f₂ a)) ⋯
-- Std.Sync.Channel
_private.Std.Sync.Channel.0.Std.CloseableChannel.Zero.recvSelector : {α : Type} → Std.CloseableChannel.Zero✝ α → Std.Async.Selector (Option α)
-- Mathlib.Algebra.Module.Presentation.Tautological
Module.Presentation.tautological.R.add.sizeOf_spec : ∀ {A : Type u} {M : Type v} [inst : SizeOf A] [inst_1 : SizeOf M] (m₁ m₂ : M),
  sizeOf (Module.Presentation.tautological.R.add m₁ m₂) = 1 + sizeOf m₁ + sizeOf m₂
-- Mathlib.Algebra.Group.Submonoid.MulOpposite
Submonoid.op_unop : ∀ {M : Type u_2} [inst : MulOneClass M] (S : Submonoid Mᵐᵒᵖ), S.unop.op = S
-- Mathlib.NumberTheory.ModularForms.QExpansion
UpperHalfPlane.qExpansion_mul_coeff_zero : ∀ {h : ℝ} {f g : UpperHalfPlane → ℂ},
  ContinuousAt (UpperHalfPlane.cuspFunction h f) 0 →
    ContinuousAt (UpperHalfPlane.cuspFunction h g) 0 →
      (PowerSeries.coeff 0) (UpperHalfPlane.qExpansion h (f * g)) =
        (PowerSeries.coeff 0) (UpperHalfPlane.qExpansion h f) * (PowerSeries.coeff 0) (UpperHalfPlane.qExpansion h g)