mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Sites.GlobalSections
/-- Every site `C` admits a global sections functor for `A`-valued sheaves when `A` has limits of
shape `Cᵒᵖ`.  -/
CategoryTheory.hasGlobalSectionsFunctor_of_hasLimitsOfShape : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u₂)
  [inst_1 : CategoryTheory.Category.{v₂, u₂} A] [inst_2 : CategoryTheory.HasWeakSheafify J A]
  [CategoryTheory.Limits.HasLimitsOfShape Cᵒᵖ A], CategoryTheory.HasGlobalSectionsFunctor J A
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKey_union_of_contains_eq_false_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] (h₁ : (↑m₁).WF) (h₂ : (↑m₂).WF) {k : α}
  (contains_eq_false : m₂.contains k = false) {h' : (m₁.union m₂).contains k = true},
  (m₁.union m₂).getKey k h' = m₁.getKey k ⋯
-- Mathlib.RingTheory.Smooth.IntegralClosure
TensorProduct.toIntegralClosure.eq_1 : ∀ (R : Type u_1) (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (B : Type u_4)
  [inst_3 : CommRing B] [inst_4 : Algebra R B],
  TensorProduct.toIntegralClosure R S B =
    (Algebra.TensorProduct.map (AlgHom.id S S) (integralClosure R B).val).codRestrict
      (integralClosure S (TensorProduct R S B)) ⋯
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.maxKey_insert : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β k}, (t.insert k v).maxKey ⋯ = t.maxKey?.elim k fun k' => if (cmp k' k).isLE = true then k else k'
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.homMk₅_app_zero : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {f g : CategoryTheory.ComposableArrows C 5}
  (app₀ : f.obj' 0 _proof_449✝ ⟶ g.obj' 0 _proof_449✝) (app₁ : f.obj' 1 _proof_450✝ ⟶ g.obj' 1 _proof_450✝)
  (app₂ : f.obj' 2 _proof_451✝ ⟶ g.obj' 2 _proof_451✝) (app₃ : f.obj' 3 _proof_452✝ ⟶ g.obj' 3 _proof_452✝)
  (app₄ : f.obj' 4 _proof_453✝ ⟶ g.obj' 4 _proof_453✝) (app₅ : f.obj' 5 _proof_454✝ ⟶ g.obj' 5 _proof_454✝)
  (w₀ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (f.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 _proof_450✝)
          app₁ =
        CategoryTheory.CategoryStruct.comp app₀
          (g.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 _proof_450✝))
      _auto_458✝)
  (w₁ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (f.map' 1 2 _proof_246✝ _proof_451✝) app₂ =
        CategoryTheory.CategoryStruct.comp app₁ (g.map' 1 2 _proof_246✝ _proof_451✝))
      _auto_460✝)
  (w₂ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (f.map' 2 3 _proof_299✝ _proof_452✝) app₃ =
        CategoryTheory.CategoryStruct.comp app₂ (g.map' 2 3 _proof_299✝ _proof_452✝))
      _auto_462✝)
  (w₃ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (f.map' 3 4 _proof_364✝ _proof_453✝) app₄ =
        CategoryTheory.CategoryStruct.comp app₃ (g.map' 3 4 _proof_364✝ _proof_453✝))
      _auto_464✝)
  (w₄ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (f.map' 4 5 _proof_453✝ _proof_454✝) app₅ =
        CategoryTheory.CategoryStruct.comp app₄ (g.map' 4 5 _proof_453✝ _proof_454✝))
      _auto_466✝),
  (CategoryTheory.ComposableArrows.homMk₅ app₀ app₁ app₂ app₃ app₄ app₅ w₀ w₁ w₂ w₃ w₄).app 0 = app₀
-- Mathlib.Topology.UrysohnsBounded
/-- Urysohn's lemma: if `s` and `t` are two disjoint closed sets in a normal topological space `X`,
and `a ≤ b` are two real numbers, then there exists a continuous function `f : X → ℝ` such that

* `f` equals `a` on `s`;
* `f` equals `b` on `t`;
* `a ≤ f x ≤ b` for all `x`.
 -/
exists_bounded_mem_Icc_of_closed_of_le : ∀ {X : Type u_1} [inst : TopologicalSpace X] [NormalSpace X] {s t : Set X},
  IsClosed s →
    IsClosed t →
      Disjoint s t →
        ∀ {a b : ℝ},
          a ≤ b →
            ∃ f,
              Set.EqOn (⇑f) (Function.const X a) s ∧ Set.EqOn (⇑f) (Function.const X b) t ∧ ∀ (x : X), f x ∈ Set.Icc a b
-- Init.Data.Iterators.Lemmas.Combinators.FlatMap
_private.Init.Data.Iterators.Lemmas.Combinators.FlatMap.0.Std.Iter.step_filterMapWithPostcondition.match_3.eq_2 : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] {it : Std.Iter β} (motive : it.Step → Sort u_2) (it' : Std.Iter β)
  (h : it.IsPlausibleStep (Std.IterStep.skip it'))
  (h_1 :
    (it' : Std.Iter β) →
      (out : β) → (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 : (it' : Std.Iter β) → (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (h : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩),
  (match ⟨Std.IterStep.skip it', h⟩ with
    | ⟨Std.IterStep.yield it' out, h⟩ => h_1 it' out h
    | ⟨Std.IterStep.skip it', h⟩ => h_2 it' h
    | ⟨Std.IterStep.done, h⟩ => h_3 h) =
    h_2 it' h
-- Init.Data.Nat.Bitwise.Basic
Nat.shiftLeft_eq : ∀ (a b : ℕ), a <<< b = a * 2 ^ b
-- Mathlib.Analysis.Analytic.Order
/-- If two functions have unequal orders, then the order of their sum is exactly the minimum
of the orders of the summands.  -/
analyticOrderAt_add_of_ne : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f g : 𝕜 → E} {z₀ : 𝕜},
  analyticOrderAt f z₀ ≠ analyticOrderAt g z₀ →
    analyticOrderAt (f + g) z₀ = min (analyticOrderAt f z₀) (analyticOrderAt g z₀)
-- Mathlib.Analysis.Normed.Group.Uniform
/-- **Alias** of the forward direction of `lipschitzOnWith_iff_norm_div_le`. -/
LipschitzOnWith.norm_div_le : ∀ {E : Type u_2} {F : Type u_3} [inst : SeminormedCommGroup E] [inst_1 : SeminormedCommGroup F] {f : E → F} {C : NNReal}
  {s : Set E}, LipschitzOnWith C f s → ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ‖f x / f y‖ ≤ ↑C * ‖x / y‖
-- Init.Omega.IntList
Lean.Omega.IntList.smul_cons : ∀ {x : ℤ} {xs : List ℤ} {i : ℤ}, i * (x :: xs) = i * x :: i * xs
-- Std.Sat.AIG.Basic
Std.Sat.AIG.Ref.mk.inj : ∀ {α : Type} {inst : Hashable α} {inst_1 : DecidableEq α} {aig : Std.Sat.AIG α} {gate : ℕ} {invert : Bool}
  {hgate : gate < aig.decls.size} {gate_1 : ℕ} {invert_1 : Bool} {hgate_1 : gate_1 < aig.decls.size},
  { gate := gate, invert := invert, hgate := hgate } = { gate := gate_1, invert := invert_1, hgate := hgate_1 } →
    gate = gate_1 ∧ invert = invert_1
-- Init.Data.String.Basic
_private.Init.Data.String.Basic.0.String.Pos.Raw.get?.match_1.eq_1 : ∀ (motive : String → String.Pos.Raw → Sort u_1) (s : String) (p : String.Pos.Raw)
  (h_1 : (s : String) → (p : String.Pos.Raw) → motive s p),
  (match s, p with
    | s, p => h_1 s p) =
    h_1 s p
-- Std.Data.Iterators.Lemmas.Combinators.Zip
_private.Std.Data.Iterators.Lemmas.Combinators.Zip.0.Std.IterM.step_intermediateZip.match_1.eq_3 : ∀ {α₁ β₁ : Type u_1} {m : Type u_1 → Type u_2} [inst : Std.Iterator α₁ m β₁] {it₁ : Std.IterM m β₁}
  (motive : it₁.Step → Sort u_3) (hp : it₁.IsPlausibleStep Std.IterStep.done)
  (h_1 :
    (it₁' : Std.IterM m β₁) →
      (out : β₁) → (hp : it₁.IsPlausibleStep (Std.IterStep.yield it₁' out)) → motive ⟨Std.IterStep.yield it₁' out, hp⟩)
  (h_2 :
    (it₁' : Std.IterM m β₁) → (hp : it₁.IsPlausibleStep (Std.IterStep.skip it₁')) → motive ⟨Std.IterStep.skip it₁', hp⟩)
  (h_3 : (hp : it₁.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, hp⟩),
  (match ⟨Std.IterStep.done, hp⟩ with
    | ⟨Std.IterStep.yield it₁' out, hp⟩ => h_1 it₁' out hp
    | ⟨Std.IterStep.skip it₁', hp⟩ => h_2 it₁' hp
    | ⟨Std.IterStep.done, hp⟩ => h_3 hp) =
    h_3 hp
-- Mathlib.Data.EReal.Inv
EReal.abs_bot : ⊥.abs = ⊤
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get?_filterMap! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} {γ : α → Type w} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] {f : (a : α) → β a → Option (γ a)} {k : α},
  t.WF → (Std.DTreeMap.Internal.Impl.filterMap! f t).get? k = (t.get? k).bind (f k)
-- Init.Data.String.Lemmas.Pattern.Find.Pred
String.Slice.find?_prop_eq_some_iff : ∀ {p : Char → Prop} [inst : DecidablePred p] {s : String.Slice} {pos : s.Pos},
  s.find? p = some pos ↔ ∃ (h : pos ≠ s.endPos), p (pos.get h) ∧ ∀ (pos' : s.Pos) (h' : pos' < pos), ¬p (pos'.get ⋯)
-- Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
CategoryTheory.Abelian.SpectralObject.SpectralSequence.HomologyData.isIso_mapFourδ₁Toδ₀' : ∀ {C : Type u_1} {ι : Type u_2} {κ : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Abelian C] [inst_2 : Preorder ι] (X : CategoryTheory.Abelian.SpectralObject C ι)
  {c : ℤ → ComplexShape κ} {r₀ : ℤ} (data : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀)
  (r r' : ℤ) (hrr' : r + 1 = r') (hr : r₀ ≤ r) (pq' pq'' : κ),
  (c r).next pq' = pq'' →
    ∀ (i₀' i₀ i₁ i₂ i₃ : ι) (hi₀' : i₀' = data.i₀ r' pq' ⋯) (hi₀ : i₀ = data.i₀ r pq' ⋯) (hi₁ : i₁ = data.i₁ pq')
      (hi₂ : i₂ = data.i₂ pq') (hi₃ : i₃ = data.i₃ r pq' ⋯) (n₀ n₁ n₂ : ℤ),
      n₁ = data.deg pq' →
        ∀ [X.HasSpectralSequence data],
          ¬(c r).Rel pq' pq'' →
            ∀
              (hn₁ :
                autoParam (n₀ + 1 = n₁)
                  CategoryTheory.Abelian.SpectralObject.SpectralSequence.HomologyData.isIso_mapFourδ₁Toδ₀'._auto_1)
              (hn₂ :
                autoParam (n₁ + 1 = n₂)
                  CategoryTheory.Abelian.SpectralObject.SpectralSequence.HomologyData.isIso_mapFourδ₁Toδ₀'._auto_3),
              CategoryTheory.IsIso (X.mapFourδ₁Toδ₀' i₀' i₀ i₁ i₂ i₃ ⋯ ⋯ ⋯ ⋯ n₀ n₁ n₂ hn₁ hn₂)
-- Mathlib.Tactic.DeriveEncodable
_private.Mathlib.Tactic.DeriveEncodable.0.Mathlib.Deriving.Encodable.S.nat.sizeOf_spec : ∀ (n : ℕ), sizeOf (Mathlib.Deriving.Encodable.S.nat✝ n) = 1 + sizeOf n
-- Lean.Data.Json.FromToJson.Basic
Lean.FromJson.mk : {α : Type u} → (Lean.Json → Except String α) → Lean.FromJson α
-- Mathlib.Data.List.TFAE
List.tfae_nil : [].TFAE
-- Init.SizeOf
Lean.ParserDescr.nodeWithAntiquot.sizeOf_spec : ∀ (name : String) (kind : Lean.SyntaxNodeKind) (p : Lean.ParserDescr),
  sizeOf (Lean.ParserDescr.nodeWithAntiquot name kind p) = 1 + sizeOf name + sizeOf kind + sizeOf p
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Iio_injective : ∀ {α : Type u_1} [inst : LinearOrder α], Function.Injective Set.Iio
-- Mathlib.RingTheory.WittVector.Teichmuller
WittVector.teichmuller_coeff_zero : ∀ (p : ℕ) {R : Type u_1} [hp : Fact (Nat.Prime p)] [inst : CommRing R] (r : R),
  ((WittVector.teichmuller p) r).coeff 0 = r
-- Mathlib.Order.Filter.Basic
Filter.EventuallyLE.refl : ∀ {α : Type u} {β : Type v} [inst : Preorder β] (l : Filter α) (f : α → β), f ≤ᶠ[l] f
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt
/-- Given `x` whose denotation is `e`, if `e` is of the form `ToInt a`,
asserts its lower and upper bounds if available
 -/
Lean.Meta.Grind.Arith.Cutsat.assertToIntBounds : Lean.Expr → Int.Internal.Linear.Var → Lean.Meta.Grind.GoalM Unit
-- Mathlib.Order.Basic
Pi.instCompl.eq_1 : ∀ {ι : Type u_1} {π : ι → Type u_4} [inst : (i : ι) → Compl (π i)], Pi.instCompl = { compl := fun x i => (x i)ᶜ }
-- Mathlib.Analysis.Calculus.FDeriv.Star
HasFDerivAtFilter.star : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : StarRing 𝕜] {E : Type u_2} [inst_2 : NormedAddCommGroup E]
  [inst_3 : NormedSpace 𝕜 E] {F : Type u_3} [inst_4 : NormedAddCommGroup F] [inst_5 : StarAddMonoid F]
  [inst_6 : NormedSpace 𝕜 F] [inst_7 : StarModule 𝕜 F] [inst_8 : ContinuousStar F] {f : E → F} {f' : E →L[𝕜] F}
  {L : Filter (E × E)} [inst_9 : TrivialStar 𝕜],
  HasFDerivAtFilter f f' L → HasFDerivAtFilter (fun x => star (f x)) (↑(starL' 𝕜) ∘SL f') L
-- Mathlib.GroupTheory.GroupAction.Quotient
AddAction.selfEquivSigmaOrbitsQuotientStabilizer'.eq_1 : ∀ (G : Type u) (X : Type v) [inst : AddGroup G] [inst_1 : AddAction G X] {φ : Quotient (AddAction.orbitRel G X) → X}
  (hφ : Function.LeftInverse Quotient.mk'' φ),
  AddAction.selfEquivSigmaOrbitsQuotientStabilizer' G X hφ =
    Trans.trans (AddAction.selfEquivSigmaOrbits' G X)
      (Equiv.sigmaCongrRight fun ω => (Equiv.setCongr ⋯).trans (AddAction.orbitEquivQuotientStabilizer G (φ ω)))
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Ioc_ae_eq_Icc' : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : PartialOrder α] {a b : α},
  μ {a} = 0 → Set.Ioc a b =ᵐ[μ] Set.Icc a b
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
mem_pairSelfAdjointMatricesSubmodule : ∀ {R : Type u_1} {n : Type u_11} [inst : CommRing R] [inst_1 : Fintype n] (J J₂ A₁ : Matrix n n R)
  [inst_2 : DecidableEq n], A₁ ∈ pairSelfAdjointMatricesSubmodule J J₂ ↔ J.IsAdjointPair J₂ A₁ A₁
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
/-- The `SubAddAction` of `fixingAddSubgroup M s` on the complement of `s`.  -/
SubAddAction.ofFixingAddSubgroup : (M : Type u_1) →
  {α : Type u_2} →
    [inst : AddGroup M] → [inst_1 : AddAction M α] → (s : Set α) → SubAddAction (↥(fixingAddSubgroup M s)) α
-- Mathlib.CategoryTheory.Monoidal.Grp
/-- Natural isomorphisms between functors lift to group objects.  -/
CategoryTheory.Functor.mapGrpNatIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.CartesianMonoidalCategory D] →
            {F F' : CategoryTheory.Functor C D} →
              [inst_4 : F.Monoidal] → [inst_5 : F'.Monoidal] → (F ≅ F') → (F.mapGrp ≅ F'.mapGrp)
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass
CategoryTheory.ShortComplex.ShortExact.extClass_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact)
  [inst_3 : HasDerivedCategory C], hS.extClass.hom = hS.singleδ
-- Init.RCases
Lean.Parser.Tactic.rcasesPat.quot : Lean.ParserDescr
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.hasCoproduct_unique : ∀ {β : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [Nonempty β] [Subsingleton β] (f : β → C),
  CategoryTheory.Limits.HasCoproduct f
-- Mathlib.RingTheory.HopfAlgebra.Convolution
HopfAlgebra.antipodeAlgHomOp_apply : ∀ (R : Type u_1) (A : Type u_2) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : HopfAlgebra R A] (a : A),
  (HopfAlgebra.antipodeAlgHomOp R A) a = MulOpposite.op ((HopfAlgebraStruct.antipode R) a)
-- Mathlib.Analysis.Convex.Body
ConvexBody.coe_zero : ∀ {V : Type u_1} [inst : TopologicalSpace V] [inst_1 : AddCommGroup V] [inst_2 : Module ℝ V], ↑0 = 0
-- Mathlib.Topology.EMetricSpace.Defs
/-- **Alias** of `PseudoEMetricSpace.ofEDistOfTopology`.

---

Consider an extended distance on a topological space, for which the neighborhoods can be
expressed in terms of the distance. Then we define the emetric space structure associated to this
distance, with a topology defeq to the initial one.  -/
PseudoEmetricSpace.ofEdistOfTopology : {α : Type u_2} →
  [inst : TopologicalSpace α] →
    (d : α → α → ENNReal) →
      (∀ (x : α), d x x = 0) →
        (∀ (x y : α), d x y = d y x) →
          (∀ (x y z : α), d x z ≤ d x y + d y z) →
            (∀ (x : α), (nhds x).HasBasis (fun c => 0 < c) fun c => {y | d x y < c}) → PseudoEMetricSpace α
-- Mathlib.Analysis.InnerProductSpace.Spectrum
/-- The **Spectral Theorem** for compact self-adjoint operators: the eigenspaces of a compact
self-adjoint operator are finite-dimensional.  -/
ContinuousLinearMap.finite_dimensional_eigenspace : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [CompleteSpace E] {T : E →L[𝕜] E},
  IsCompactOperator ⇑T → ∀ (μ : 𝕜), μ ≠ 0 → FiniteDimensional 𝕜 ↥(Module.End.eigenspace (↑T) μ)
-- Mathlib.CategoryTheory.Bicategory.Grothendieck
CategoryTheory.Pseudofunctor.Grothendieck.Hom.congr : ∀ {𝒮 : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮) CategoryTheory.Cat} {a b : F.Grothendieck}
  {f g : a ⟶ b} (h : f = g), f.fiber = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) g.fiber
-- Mathlib.Data.Int.Init
Int.div_le_div_iff_of_dvd_of_neg_of_neg : ∀ {a b c d : ℤ}, b < 0 → d < 0 → b ∣ a → d ∣ c → (a / b ≤ c / d ↔ d * a ≤ c * b)
-- Mathlib.Topology.UniformSpace.ProdApproximation
/-- Tensor product version of `ContinuousMap.prodMul`.  -/
ContinuousMap.tensorHom : {X : Type u_5} →
  {Y : Type u_6} →
    {R : Type u_7} →
      [inst : TopologicalSpace X] →
        [inst_1 : TopologicalSpace Y] →
          [inst_2 : CommRing R] →
            [inst_3 : TopologicalSpace R] →
              [inst_4 : IsTopologicalRing R] → TensorProduct R C(X, R) C(Y, R) →ₗ[R] C(X × Y, R)
-- Mathlib.Algebra.Group.Units.Basic
IsUnit.inv_mul_eq_iff_eq_mul : ∀ {α : Type u} [inst : DivisionMonoid α] {a b c : α}, IsUnit a → (a⁻¹ * b = c ↔ b = a * c)
-- Mathlib.Order.WellFoundedSet
Set.PartiallyWellOrderedOn.prod : ∀ {α : Type u_2} {β : Type u_3} {r : α → α → Prop} {r' : β → β → Prop} {s : Set α} [IsPreorder α r] {t : Set β},
  s.PartiallyWellOrderedOn r →
    t.PartiallyWellOrderedOn r' → (s ×ˢ t).PartiallyWellOrderedOn fun x y => r x.1 y.1 ∧ r' x.2 y.2
-- Mathlib.MeasureTheory.Measure.Tilted
MeasureTheory.tilted_zero' : ∀ {α : Type u_1} {mα : MeasurableSpace α} (μ : MeasureTheory.Measure α), μ.tilted 0 = (μ Set.univ)⁻¹ • μ
-- Init.Grind.Ring.Envelope
Lean.Grind.CommRing.OfCommSemiring.instCommutativeHMul : ∀ (α : Type u) [inst : Lean.Grind.CommSemiring α], Std.Commutative fun x1 x2 => x1 * x2
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
NumberField.InfinitePlace.isReal_mk_iff : ∀ {K : Type u_1} [inst : Field K] {φ : K →+* ℂ},
  (NumberField.InfinitePlace.mk φ).IsReal ↔ NumberField.ComplexEmbedding.IsReal φ
-- Mathlib.RingTheory.Polynomial.Pochhammer
factorial_mul_ascPochhammer : ∀ (S : Type u_2) [inst : Semiring S] (r n : ℕ),
  ↑r.factorial * Polynomial.eval (↑r + 1) (ascPochhammer S n) = ↑(r + n).factorial
-- Mathlib.Data.Semiquot
Semiquot.instLawfulMonad : LawfulMonad Semiquot
-- Mathlib.Analysis.Asymptotics.SpecificAsymptotics
Asymptotics.IsEquivalent.log : ∀ {α : Type u_1} {l : Filter α} {f g : α → ℝ},
  Asymptotics.IsEquivalent l f g →
    Filter.Tendsto g l Filter.atTop → Asymptotics.IsEquivalent l (fun n => Real.log (f n)) fun n => Real.log (g n)
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrp.comp' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {A₁ A₂ A₃ : CategoryTheory.AddGrp C} (f : A₁ ⟶ A₂) (g : A₂ ⟶ A₃),
  (CategoryTheory.CategoryStruct.comp f g).hom = CategoryTheory.CategoryStruct.comp f.hom g.hom
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
/-- (Implementation). Given a hom between the pullbacks of two sheaves, we can whisker it with
`coyoneda` to obtain a hom between the pullbacks of the sheaves of maps from `X`.
 -/
CategoryTheory.Functor.IsCoverDense.homOver : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {D : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        {K : CategoryTheory.GrothendieckTopology D} →
          {A : Type u_4} →
            [inst_2 : CategoryTheory.Category.{v_4, u_4} A] →
              {G : CategoryTheory.Functor C D} →
                {ℱ : CategoryTheory.Functor Dᵒᵖ A} →
                  {ℱ' : CategoryTheory.Sheaf K A} →
                    (G.op.comp ℱ ⟶ G.op.comp ℱ'.obj) →
                      (X : A) →
                        G.op.comp (ℱ.comp (CategoryTheory.coyoneda.obj (Opposite.op X))) ⟶
                          G.op.comp (CategoryTheory.sheafOver ℱ' X).obj
-- Std.Time.Duration
Std.Time.instLawfulEqOrdDuration : Std.LawfulEqOrd Std.Time.Duration
-- Mathlib.CategoryTheory.Bicategory.Kan.IsKan
/-- A right Kan extension of `g` along `f` is a terminal object in `RightExtension f g`.  -/
CategoryTheory.Bicategory.RightExtension.IsKan : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} → {f : a ⟶ b} → {g : a ⟶ c} → CategoryTheory.Bicategory.RightExtension f g → Type (max (max v w) w)
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
LipschitzWith.continuous_compLp : ∀ {α : Type u_1} {E : Type u_4} {F : Type u_5} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F] {g : E → F} {c : NNReal} [inst_2 : Fact (1 ≤ p)]
  (hg : LipschitzWith c g) (g0 : g 0 = 0), Continuous (hg.compLp g0)
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
/-- **Alias** of `Left.neg_pos_iff`.

---

Uses `left` co(ntra)variant.  -/
neg_pos : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LT α] [AddLeftStrictMono α] {a : α}, 0 < -a ↔ a < 0
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalAlgebra.adjoin_union : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] [inst_4 : SMulCommClass R A A] (s t : Set A),
  NonUnitalAlgebra.adjoin R (s ∪ t) = NonUnitalAlgebra.adjoin R s ⊔ NonUnitalAlgebra.adjoin R t
-- Mathlib.Order.Hom.CompleteLattice
CompleteLatticeHom.toFun_eq_coe : ∀ {α : Type u_2} {β : Type u_3} [inst : CompleteLattice α] [inst_1 : CompleteLattice β] (f : CompleteLatticeHom α β),
  f.toFun = ⇑f
-- Mathlib.Topology.Closure
frontier_union_subset : ∀ {X : Type u} [inst : TopologicalSpace X] (s t : Set X),
  frontier (s ∪ t) ⊆ frontier s ∩ closure tᶜ ∪ closure sᶜ ∩ frontier t
-- Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
/-- The q-expansion of a level-1 modular form whose zeroth coefficient vanishes factors as
the q-expansion of `Δ` times the q-expansion of the corresponding form of weight `k - 12`
obtained via `discriminantEquiv`.  -/
ModularForm.qExpansion_eq_qExpansion_discriminant_mul : ∀ {k : ℤ} (f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k)
  (hcusp : (PowerSeries.coeff 0) (UpperHalfPlane.qExpansion 1 ⇑f) = 0),
  UpperHalfPlane.qExpansion 1 ⇑f =
    UpperHalfPlane.qExpansion 1 ModularForm.discriminant *
      UpperHalfPlane.qExpansion 1 ⇑(CuspForm.discriminantEquiv (f.toCuspForm hcusp))
-- Init.Data.List.Attach
List.foldl_wfParam : ∀ {α : Type u_1} {β : Type u_2} {xs : List α} {f : β → α → β} {x : β},
  List.foldl f x (wfParam xs) = List.foldl f x xs.attach.unattach
-- Mathlib.LinearAlgebra.RootSystem.Reduced
RootPairing.linearIndependent_of_sub_mem_range_root' : ∀ {ι : 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 M N) [CharZero R]
  [IsDomain R] [P.IsReduced] {i j : ι},
  P.root i - P.root j ∈ Set.range ⇑P.root → LinearIndependent R ![P.root i, P.root j]
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.natTransTruncGEOfLE_trans_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (a b c : ℤ) (hab : a ≤ b) (hbc : b ≤ c) (X : C),
  CategoryTheory.CategoryStruct.comp ((t.natTransTruncGEOfLE a b hab).app X) ((t.natTransTruncGEOfLE b c hbc).app X) =
    (t.natTransTruncGEOfLE a c ⋯).app X
-- Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects
/-- A zero object is a right unit for categorical coproduct.  -/
CategoryTheory.Limits.coprodZeroIso : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroObject C] →
      [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] → (X : C) → X ⨿ 0 ≅ X
-- Mathlib.GroupTheory.Divisible
ULift.instDivisibleBy : (A : Type u_1) →
  (α : Type u_2) →
    [inst : AddMonoid A] →
      [inst_1 : SMul α A] → [inst_2 : Zero α] → [DivisibleBy A α] → DivisibleBy (ULift.{u_3, u_1} A) α
-- Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
IncidenceAlgebra.coe_constSMul : ∀ {𝕜 : Type u_2} {α : Type u_5} {M : Type u_7} [inst : Zero 𝕜] [inst_1 : LE α] [inst_2 : SMulZeroClass M 𝕜] (c : M)
  (f : IncidenceAlgebra 𝕜 α), ⇑(c • f) = c • ⇑f