mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
/-- The induced map `∐ I.left ⟶ ∐ I.right` via `I.fst`.  -/
CategoryTheory.Limits.MultispanIndex.fstSigmaMap : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.Limits.MultispanShape} →
      (I : CategoryTheory.Limits.MultispanIndex J C) →
        [inst_1 : CategoryTheory.Limits.HasCoproduct I.left] →
          [inst_2 : CategoryTheory.Limits.HasCoproduct I.right] → ∐ I.left ⟶ ∐ I.right
-- Lean.Log
/-- The name of the file being processed.  -/
Lean.MonadLog.getFileName : {m : Type → Type} → [self : Lean.MonadLog m] → m String
-- Mathlib.Topology.Algebra.InfiniteSum.ENNReal
ENNReal.tsum_iSup_eq : ∀ {α : Type u_4} (a : α) {f : α → ENNReal}, ∑' (b : α), ⨆ (_ : a = b), f b = f a
-- Mathlib.CategoryTheory.Adjunction.Triple
CategoryTheory.Adjunction.Triple.mk : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        {F : CategoryTheory.Functor C D} →
          {G : CategoryTheory.Functor D C} →
            {H : CategoryTheory.Functor C D} → (F ⊣ G) → (G ⊣ H) → CategoryTheory.Adjunction.Triple F G H
-- Mathlib.MeasureTheory.MeasurableSpace.Basic
measurable_comap_iff : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ} {f : α → β}
  {g : β → γ}, Measurable f ↔ Measurable (g ∘ f)
-- Mathlib.CategoryTheory.Shift.Adjunction
/-- The identity equivalence is compatible with shifts.
 -/
CategoryTheory.Equivalence.CommShift.instRefl : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (A : Type u_3) [inst_1 : AddMonoid A]
  [inst_2 : CategoryTheory.HasShift C A], CategoryTheory.Equivalence.refl.CommShift A
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SignatureHelpOptions.mk.injEq : ∀ (toWorkDoneProgressOptions : Lean.Lsp.WorkDoneProgressOptions)
  (triggerCharacters? retriggerCharacters? : Option (Array String))
  (toWorkDoneProgressOptions_1 : Lean.Lsp.WorkDoneProgressOptions)
  (triggerCharacters?_1 retriggerCharacters?_1 : Option (Array String)),
  ({ toWorkDoneProgressOptions := toWorkDoneProgressOptions, triggerCharacters? := triggerCharacters?,
        retriggerCharacters? := retriggerCharacters? } =
      { toWorkDoneProgressOptions := toWorkDoneProgressOptions_1, triggerCharacters? := triggerCharacters?_1,
        retriggerCharacters? := retriggerCharacters?_1 }) =
    (toWorkDoneProgressOptions = toWorkDoneProgressOptions_1 ∧
      triggerCharacters? = triggerCharacters?_1 ∧ retriggerCharacters? = retriggerCharacters?_1)
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.FunDecl.beq : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.FunDecl pu → Lean.Compiler.LCNF.FunDecl pu → Bool
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.get?_diff_of_not_mem_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  k ∉ t₁ → (t₁ \ t₂).get? k = none
-- Mathlib.Algebra.Category.Semigrp.Basic
MagmaCat.comp_apply : ∀ {M N T : MagmaCat} (f : M ⟶ N) (g : N ⟶ T) (x : ↑M),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) x =
    (CategoryTheory.ConcreteCategory.hom g) ((CategoryTheory.ConcreteCategory.hom f) x)
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1.Stmt.brecOn.go : {Γ : Type u_1} →
  {Λ : Type u_2} →
    {σ : Type u_3} →
      {motive : Turing.TM1.Stmt Γ Λ σ → Sort u} →
        (t : Turing.TM1.Stmt Γ Λ σ) →
          ((t : Turing.TM1.Stmt Γ Λ σ) → Turing.TM1.Stmt.below t → motive t) → motive t ×' Turing.TM1.Stmt.below t
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.mk_sub : ∀ {α : Type u_1} {γ : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace γ]
  [inst_2 : AddGroup γ] [inst_3 : IsTopologicalAddGroup γ] (f g : α → γ) (hf : MeasureTheory.AEStronglyMeasurable f μ)
  (hg : MeasureTheory.AEStronglyMeasurable g μ),
  MeasureTheory.AEEqFun.mk (f - g) ⋯ = MeasureTheory.AEEqFun.mk f hf - MeasureTheory.AEEqFun.mk g hg
-- Mathlib.Algebra.Group.Subgroup.Defs
AddSubgroup.sub.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G), H.sub = { sub := fun a b => ⟨↑a - ↑b, ⋯⟩ }
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.RciSliceData.mk.inj : ∀ {α : Type u} {β : α → Type v} {inst : Ord α} {treeMap : Std.DTreeMap.Internal.Impl α β} {range : Std.Rci α}
  {treeMap_1 : Std.DTreeMap.Internal.Impl α β} {range_1 : Std.Rci α},
  { treeMap := treeMap, range := range } = { treeMap := treeMap_1, range := range_1 } →
    treeMap = treeMap_1 ∧ range = range_1
-- Mathlib.Data.Set.Function
Set.BijOn.subset_right : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} {r : Set β},
  Set.BijOn f s t → r ⊆ t → Set.BijOn f (s ∩ f ⁻¹' r) r
-- Mathlib.Analysis.Normed.Group.Uniform
dist_div_div_le : ∀ {E : Type u_2} [inst : SeminormedCommGroup E] (a₁ a₂ b₁ b₂ : E), dist (a₁ / a₂) (b₁ / b₂) ≤ dist a₁ b₁ + dist a₂ b₂
-- Mathlib.GroupTheory.Divisible
/-- A `Monoid A` is `α`-rootable iff `xⁿ = a` has a solution for all `n ≠ 0 ∈ α` and `a ∈ A`.
Here we adopt a constructive approach where we ask an explicit `root : A → α → A` function such that
* `root a 0 = 1` for all `a ∈ A`
* `(root a n)ⁿ = a` for all `n ≠ 0 ∈ α` and `a ∈ A`.
 -/
RootableBy : (A : Type u_1) → (α : Type u_2) → [Monoid A] → [Pow A α] → [Zero α] → Type (max u_1 u_2)
-- Mathlib.Data.Finsupp.Antidiagonal
Finsupp.antidiagonal_zero : ∀ {α : Type u} [inst : DecidableEq α], Finset.HasAntidiagonal.antidiagonal 0 = {(0, 0)}
-- Mathlib.SetTheory.Ordinal.Veblen
/-- `veblen o` is the `o`-th function in the Veblen hierarchy starting with `ω ^ ·`. That is:

- `veblen 0 a = ω ^ a`.
- `veblen o` for `o ≠ 0` enumerates the fixed points of `veblen o'` for `o' < o`.
 -/
Ordinal.veblen : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.getD_emptyc : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} [Std.TransCmp cmp] {a : α} {fallback : β},
  Std.DTreeMap.Raw.Const.getD ∅ a fallback = fallback
-- Mathlib.Order.Bounds.Defs
/-- `a` is a greatest lower bound of a set `s`; for a partial order, it is unique if exists.  -/
IsGLB : {α : Type u_1} → [LE α] → Set α → α → Prop
-- Mathlib.AlgebraicGeometry.Gluing
AlgebraicGeometry.Scheme.GlueData.mk.inj : ∀ {toGlueData : CategoryTheory.GlueData AlgebraicGeometry.Scheme}
  {f_open : ∀ (i j : toGlueData.J), AlgebraicGeometry.IsOpenImmersion (toGlueData.f i j)}
  {toGlueData_1 : CategoryTheory.GlueData AlgebraicGeometry.Scheme}
  {f_open_1 : ∀ (i j : toGlueData_1.J), AlgebraicGeometry.IsOpenImmersion (toGlueData_1.f i j)},
  { toGlueData := toGlueData, f_open := f_open } = { toGlueData := toGlueData_1, f_open := f_open_1 } →
    toGlueData = toGlueData_1
-- Mathlib.MeasureTheory.Covering.VitaliFamily
VitaliFamily.mk : {X : Type u_1} →
  [inst : PseudoMetricSpace X] →
    {m : MeasurableSpace X} →
      {μ : MeasureTheory.Measure X} →
        (setsAt : X → Set (Set X)) →
          (∀ (x : X), ∀ s ∈ setsAt x, MeasurableSet s) →
            (∀ (x : X), ∀ s ∈ setsAt x, (interior s).Nonempty) →
              (∀ (x : X), ∀ ε > 0, ∃ s ∈ setsAt x, s ⊆ Metric.closedBall x ε) →
                (∀ (s : Set X) (f : X → Set (Set X)),
                    (∀ x ∈ s, f x ⊆ setsAt x) →
                      (∀ x ∈ s, ∀ ε > 0, ∃ t ∈ f x, t ⊆ Metric.closedBall x ε) →
                        ∃ t,
                          (∀ p ∈ t, p.1 ∈ s) ∧
                            (t.PairwiseDisjoint fun p => p.2) ∧ (∀ p ∈ t, p.2 ∈ f p.1) ∧ μ (s \ ⋃ p ∈ t, p.2) = 0) →
                  VitaliFamily μ
-- Batteries.Data.List.Basic
_private.Batteries.Data.List.Basic.0.List.takeD.match_1.eq_2 : ∀ {α : Type u_1} (motive : ℕ → List α → α → Sort u_2) (n : ℕ) (l : List α) (x : α)
  (h_1 : (x : List α) → (x_1 : α) → motive 0 x x_1) (h_2 : (n : ℕ) → (l : List α) → (x : α) → motive n.succ l x),
  (match n.succ, l, x with
    | 0, x, x_1 => h_1 x x_1
    | n.succ, l, x => h_2 n l x) =
    h_2 n l x
-- Mathlib.Tactic.FBinop
_private.Mathlib.Tactic.FBinop.0.FBinopElab.Tree.binop.injEq : ∀ (ref : Lean.Syntax) (f : Lean.Expr) (lhs rhs : FBinopElab.Tree✝) (ref_1 : Lean.Syntax) (f_1 : Lean.Expr)
  (lhs_1 rhs_1 : FBinopElab.Tree✝),
  (FBinopElab.Tree.binop✝ ref f lhs rhs = FBinopElab.Tree.binop✝ ref_1 f_1 lhs_1 rhs_1) =
    (ref = ref_1 ∧ f = f_1 ∧ lhs = lhs_1 ∧ rhs = rhs_1)
-- Mathlib.MeasureTheory.Group.Integral
MeasureTheory.Integrable.comp_sub_left : ∀ {G : Type u_4} {F : Type u_6} [inst : MeasurableSpace G] [inst_1 : NormedAddCommGroup F] {μ : MeasureTheory.Measure G}
  [inst_2 : AddGroup G] [MeasurableAdd G] [MeasurableNeg G] {f : G → F} [μ.IsNegInvariant] [μ.IsAddLeftInvariant],
  MeasureTheory.Integrable f μ → ∀ (g : G), MeasureTheory.Integrable (fun t => f (g - t)) μ
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.whiskerRight_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X : CategoryTheory.Mon C) {Y Z : CategoryTheory.Mon C} (f : Y ⟶ Z),
  (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f).hom =
    CategoryTheory.MonoidalCategoryStruct.whiskerLeft X.X f.hom
-- Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
/-- Give the morphism from an initial object to any other.  -/
CategoryTheory.Limits.IsInitial.to : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] → {X : C} → CategoryTheory.Limits.IsInitial X → (Y : C) → X ⟶ Y
-- Mathlib.AlgebraicGeometry.Group.Affine
/-- `Spec` is fully faithful on `R`-algebras, with inverse `Gamma`.  -/
AlgebraicGeometry.algSpec.fullyFaithful : {R : CommRingCat} → (AlgebraicGeometry.algSpec R).FullyFaithful
-- Mathlib.RingTheory.QuasiFinite.Weakly
/-- (Implementation) An a priori weaker notion of being quasi-finite at a prime,
which turns out to be equivalent to `Algebra.QuasiFiniteAt` (for finite type algebras)
due to Zariski's main theorem.

This class should not be used outside of this context,
and `Algebra.QuasiFiniteAt` should be used instead.
See `Algebra.QuasiFiniteAt.of_weaklyQuasiFiniteAt`.  -/
Algebra.WeaklyQuasiFiniteAt : (R : Type u_1) →
  {S : Type u_2} → [inst : CommRing R] → [inst_1 : CommRing S] → [Algebra R S] → (q : Ideal S) → [q.IsPrime] → Prop
-- Mathlib.Analysis.Calculus.LocalExtr.Rolle
/-- **Rolle's Theorem** `HasDerivAt` version  -/
exists_hasDerivAt_eq_zero : ∀ {f f' : ℝ → ℝ} {a b : ℝ},
  a < b →
    ContinuousOn f (Set.Icc a b) → f a = f b → (∀ x ∈ Set.Ioo a b, HasDerivAt f (f' x) x) → ∃ c ∈ Set.Ioo a b, f' c = 0
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Equiv.union_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : α → Type v} {m₁ m₂ m₃ : Std.DHashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → m₃.WF → m₂.Equiv m₃ → (m₁ ∪ m₂).Equiv (m₁ ∪ m₃)
-- Mathlib.GroupTheory.GroupAction.SubMulAction
VAddMemClass.mk : ∀ {S : Type u_1} {R : outParam (Type u_2)} {M : Type u_3} [inst : VAdd R M] [inst_1 : SetLike S M],
  (∀ {s : S} (r : R) {m : M}, m ∈ s → r +ᵥ m ∈ s) → VAddMemClass S R M
-- Mathlib.RingTheory.Adjoin.Field
minpoly_algebraMap_add_splits : ∀ {K : Type u_2} {L : Type u_3} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {x : L} (r : K),
  (Polynomial.map (algebraMap K L) (minpoly K x)).Splits →
    (Polynomial.map (algebraMap K L) (minpoly K ((algebraMap K L) r + x))).Splits
-- Mathlib.Data.ENNReal.Inv
ENNReal.eq_inv_of_mul_eq_one_left : ∀ {a b : ENNReal}, a * b = 1 → a = b⁻¹
-- Mathlib.Analysis.Normed.Group.Seminorm
/-- **Alias** of `smul_apply`. -/
AddGroupSeminorm.smul_apply : ∀ {M : Type u_1} {F : Type u_2} {α : outParam (Type u_3)} {β : outParam (Type u_4)} {inst : FunLike F α β}
  {inst_1 : SMul M β} {inst_2 : SMul M F} [self : IsSMulApply M F α β] (f : F) (r : M) (x : α), (r • f) x = r • f x
-- Mathlib.Order.OmegaCompletePartialOrder
OmegaCompletePartialOrder.ContinuousHom.const_apply : ∀ {α : Type u_2} {β : Type u_3} [inst : OmegaCompletePartialOrder α] [inst_1 : OmegaCompletePartialOrder β] (x : β)
  (a : α), (OmegaCompletePartialOrder.ContinuousHom.const x) a = x
-- Std.Http.Data.Response
/-- The HTTP protocol version used in the response, e.g. `HTTP/1.1`.
 -/
Std.Http.Response.Head.version : Std.Http.Response.Head → Std.Http.Version
-- Mathlib.RingTheory.PicardGroup
/-- If an `R`-algebra `A` is also an invertible `R`-module, then it is in fact isomorphic to the
base ring `R`. The algebra structure gives us a map `A ⊗ A → A`, which after tensoring by `Aᵛ`
becomes a map `A → R`, which is the inverse map we seek.  -/
Module.Invertible.algEquivOfRing : (R : Type u) →
  (A : Type u_4) →
    [inst : CommSemiring R] → [inst_1 : Semiring A] → [inst_2 : Algebra R A] → [Module.Invertible R A] → R ≃ₐ[R] A
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.cocones_obj_map : ∀ (J : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} J] (C : Type u₃) [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  (F : (CategoryTheory.Functor J C)ᵒᵖ) {X Y : C} (f : X ⟶ Y),
  ((CategoryTheory.cocones J C).obj F).map f =
    TypeCat.ofHom fun g => CategoryTheory.CategoryStruct.comp g ((CategoryTheory.Functor.const J).map f)
-- Mathlib.Topology.Sheaves.Presheaf
/-- If `H : X ≅ Y` is a homeomorphism,
then given an `H _* ℱ ⟶ 𝒢`, we may obtain an `ℱ ⟶ H ⁻¹ _* 𝒢`.
 -/
TopCat.Presheaf.toPushforwardOfIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : TopCat} →
      (H : X ≅ Y) →
        {ℱ : TopCat.Presheaf C X} →
          {𝒢 : TopCat.Presheaf C Y} →
            ((TopCat.Presheaf.pushforward C H.hom).obj ℱ ⟶ 𝒢) → (ℱ ⟶ (TopCat.Presheaf.pushforward C H.inv).obj 𝒢)
-- Batteries.Data.BitVec.Lemmas
BitVec.getElem_ofFnLEAux : ∀ {n m : ℕ} (f : Fin n → Bool) (i : ℕ) (h : i < n) (h' : i < m), (BitVec.ofFnLEAux m f)[i] = f ⟨i, h⟩
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Expr.denote_toPolyC_nc : ∀ {α : Type u_1} {c : ℕ} [inst : Lean.Grind.Ring α] [Lean.Grind.IsCharP α c] (ctx : Lean.Grind.CommRing.Context α)
  (e : Lean.Grind.CommRing.Expr),
  Lean.Grind.CommRing.Poly.denote ctx (e.toPolyC_nc c) = Lean.Grind.CommRing.Expr.denote ctx e
-- Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
integral_withDensity_eq_integral_toReal_smul : ∀ {X : Type u_1} {E : Type u_3} [inst : MeasurableSpace X] {μ : MeasureTheory.Measure X} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] {f : X → ENNReal},
  Measurable f →
    (∀ᵐ (x : X) ∂μ, f x < ⊤) → ∀ (g : X → E), ∫ (x : X), g x ∂μ.withDensity f = ∫ (x : X), (f x).toReal • g x ∂μ
-- Mathlib.CategoryTheory.Limits.Shapes.StrongEpi
/-- If `f ≫ g` is a strong epimorphism, then so is `g`.  -/
CategoryTheory.strongEpi_of_strongEpi : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P Q R : C} (f : P ⟶ Q) (g : Q ⟶ R)
  [CategoryTheory.StrongEpi (CategoryTheory.CategoryStruct.comp f g)], CategoryTheory.StrongEpi g
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
CategoryTheory.Limits.comp_reflectsColimits : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [ℰ : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D)
  (G : CategoryTheory.Functor D E) [CategoryTheory.Limits.ReflectsColimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F]
  [CategoryTheory.Limits.ReflectsColimitsOfSize.{w', w, v₂, v₃, u₂, u₃} G],
  CategoryTheory.Limits.ReflectsColimitsOfSize.{w', w, v₁, v₃, u₁, u₃} (F.comp G)
-- Mathlib.Order.Interval.Finset.Fin
Fin.finsetImage_rev_Ici : ∀ {n : ℕ} (i : Fin n), Finset.image Fin.rev (Finset.Ici i) = Finset.Iic i.rev
-- Lean.Data.PersistentArray
Lean.PersistentArray.mod2Shift : USize → USize → USize
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square
CategoryTheory.Square.IsPullback.iff_of_iso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {sq₁ sq₂ : CategoryTheory.Square C} (e : sq₁ ≅ sq₂),
  sq₁.IsPullback ↔ sq₂.IsPullback
-- Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
/-- If `E` is a normed space, `Lp.simpleFunc E p μ` is a normed space. Not declared as an
instance as it is (as of writing) used only in the construction of the Bochner integral.  -/
MeasureTheory.Lp.simpleFunc.isBoundedSMul : ∀ {α : Type u_1} {E : Type u_4} {𝕜 : Type u_6} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E] {p : ENNReal}
  {μ : MeasureTheory.Measure α} [inst_2 : NormedRing 𝕜] [inst_3 : Module 𝕜 E] [inst_4 : IsBoundedSMul 𝕜 E]
  [inst_5 : Fact (1 ≤ p)], IsBoundedSMul 𝕜 ↥(MeasureTheory.Lp.simpleFunc E p μ)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.size_empty : ∀ {α : Type u} {β : α → Type v}, ∅.size = 0
-- Mathlib.MeasureTheory.Function.Holder
ContinuousLinearMap.memLp_of_bilin : ∀ {α : Type u_1} {𝕜 : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {p q : ENNReal} (r : ENNReal) [hpqr : p.HolderTriple q r]
  [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜 F] [inst_6 : NormedSpace 𝕜 G]
  (B : E →L[𝕜] F →L[𝕜] G) {f : α → E} {g : α → F},
  MeasureTheory.MemLp f p μ → MeasureTheory.MemLp g q μ → MeasureTheory.MemLp (fun x => (B (f x)) (g x)) r μ
-- Mathlib.Order.SuccPred.LinearLocallyFinite
LinearLocallyFiniteOrder.instIsPredArchimedeanOfLocallyFiniteOrder : ∀ {ι : Type u_1} [inst : LinearOrder ι] [LocallyFiniteOrder ι] [inst_2 : PredOrder ι], IsPredArchimedean ι
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.Scheme.AffineOpenCover.ofIsOpenCover_f : ∀ {X : AlgebraicGeometry.Scheme} {ι : Type u_1} (U : ι → X.Opens) (hU : TopologicalSpace.IsOpenCover U)
  (hU' : ∀ (i : ι), AlgebraicGeometry.IsAffineOpen (U i)) (i : ι),
  (AlgebraicGeometry.Scheme.AffineOpenCover.ofIsOpenCover U hU hU').f i = ⋯.fromSpec
-- Mathlib.LinearAlgebra.FreeModule.PID
Ideal.ringBasis.congr_simp : ∀ {ι : Type u_1} {R : Type u_2} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsPrincipalIdealRing R]
  {S : Type u_4} [inst_3 : CommRing S] [inst_4 : IsDomain S] [inst_5 : Algebra R S] [inst_6 : Finite ι]
  (b b_1 : Module.Basis ι R S),
  b = b_1 → ∀ (I I_1 : Ideal S) (e_I : I = I_1) (hI : I ≠ ⊥), Ideal.ringBasis b I hI = Ideal.ringBasis b_1 I_1 ⋯
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.Cont.halt : Turing.ToPartrec.Cont
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
BoundedContinuousFunction.coe_ofNormedAddCommGroupDiscrete : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : DiscreteTopology α]
  [inst_2 : SeminormedAddCommGroup β] (f : α → β) (C : ℝ) (H : ∀ (x : α), ‖f x‖ ≤ C),
  ⇑(BoundedContinuousFunction.ofNormedAddCommGroupDiscrete f C H) = f
-- Mathlib.Analysis.LocallyConvex.Bounded
/-- The union of two bounded sets is bounded.  -/
Bornology.IsVonNBounded.union : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : SeminormedRing 𝕜] [inst_1 : SMul 𝕜 E] [inst_2 : Zero E]
  [inst_3 : TopologicalSpace E] {s₁ s₂ : Set E},
  Bornology.IsVonNBounded 𝕜 s₁ → Bornology.IsVonNBounded 𝕜 s₂ → Bornology.IsVonNBounded 𝕜 (s₁ ∪ s₂)
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.CoreMonoidal.left_unitality : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  {F : CategoryTheory.Functor C D} (self : F.CoreMonoidal) (X : C),
  (CategoryTheory.MonoidalCategoryStruct.leftUnitor (F.obj X)).hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight self.εIso.hom (F.obj X))
      (CategoryTheory.CategoryStruct.comp (self.μIso (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) X).hom
        (F.map (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom))
-- Mathlib.Order.Atoms
Pi.isCoatomic : ∀ {ι : Type u_4} {π : ι → Type u} [inst : (i : ι) → PartialOrder (π i)] [inst_1 : (i : ι) → OrderTop (π i)]
  [∀ (i : ι), IsCoatomic (π i)], IsCoatomic ((i : ι) → π i)
-- Std.Sat.AIG.Relabel
Std.Sat.AIG.Decl.relabel : {α β : Type} → (α → β) → Std.Sat.AIG.Decl α → Std.Sat.AIG.Decl β
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
/-- The addition of two projective point classes on a Weierstrass curve `W`.

If `P` and `Q` are two projective point representatives on `W`, then `W.addMap ⟦P⟧ ⟦Q⟧` is
definitionally equivalent to `W.add P Q`.  -/
WeierstrassCurve.Projective.addMap : {R : Type r} →
  [inst : CommRing R] →
    WeierstrassCurve.Projective R →
      WeierstrassCurve.Projective.PointClass R →
        WeierstrassCurve.Projective.PointClass R → WeierstrassCurve.Projective.PointClass R
-- Mathlib.GroupTheory.FreeGroup.Reduce
FreeGroup.Red.enum.complete : ∀ {α : Type u_1} {L₁ L₂ : List (α × Bool)} [inst : DecidableEq α], FreeGroup.Red L₁ L₂ → L₂ ∈ FreeGroup.Red.enum L₁
-- Mathlib.Data.Multiset.ZeroCons
Multiset.instSingleton : {α : Type u_1} → Singleton α (Multiset α)
-- Mathlib.CategoryTheory.ObjectProperty.Ind
CategoryTheory.ObjectProperty.ind_inverseImage_eq_of_isEquivalence : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{u_2, u_1} D]
  (P : CategoryTheory.ObjectProperty D) (F : CategoryTheory.Functor C D) [P.IsClosedUnderIsomorphisms]
  [F.IsEquivalence], (P.inverseImage F).ind = P.ind.inverseImage F
-- Mathlib.Topology.Compactification.OnePoint.Basic
OnePoint.exists : ∀ {X : Type u_1} {p : OnePoint X → Prop}, (∃ x, p x) ↔ p OnePoint.infty ∨ ∃ x, p ↑x
-- Mathlib.RingTheory.MvPolynomial.Ideal
MonomialOrder.span_leadingTerm_eq_span_monomial₀ : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] {m : MonomialOrder σ} {B : Set (MvPolynomial σ R)},
  (∀ p ∈ B, IsUnit (m.leadingCoeff p) ∨ p = 0) →
    Ideal.span (m.leadingTerm '' B) = Ideal.span ((fun p => (MvPolynomial.monomial (m.degree p)) 1) '' (B \ {0}))
-- Lean.Meta.Tactic.Replace
/-- Converts the given goal `Ctx |- target` into `Ctx |- targetNew`. It assumes the goals are definitionally equal.
We use the proof term
```
@id target mvarNew
```
to create a checkpoint.

If `targetNew` is equal to `target`, then returns `mvarId` unchanged.
Uses `Expr.equal` for the comparison so that it is possible to update binder names, etc., which are user-visible.
 -/
Lean.MVarId.replaceTargetDefEq : Lean.MVarId → Lean.Expr → Lean.MetaM Lean.MVarId
-- Mathlib.RingTheory.Ideal.Lattice
Ideal.ne_top_iff_one : ∀ {α : Type u} [inst : Semiring α] (I : Ideal α), I ≠ ⊤ ↔ 1 ∉ I
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- Structure witnessing that a binary bicone is a limit cone and a limit cocone.  -/
CategoryTheory.Limits.BinaryBicone.IsBilimit.isLimit : {C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {P Q : C} → {b : CategoryTheory.Limits.BinaryBicone P Q} → b.IsBilimit → CategoryTheory.Limits.IsLimit b.toCone
-- Mathlib.Data.Finsupp.Defs
Finsupp.zipWith.congr_simp : ∀ {α : Type u_1} {M : Type u_4} {N : Type u_5} {O : Type u_6} [inst : Zero M] [inst_1 : Zero N] [inst_2 : Zero O]
  (f f_1 : M → N → O) (e_f : f = f_1) (hf : f 0 0 = 0) (g₁ g₁_1 : α →₀ M),
  g₁ = g₁_1 → ∀ (g₂ g₂_1 : α →₀ N), g₂ = g₂_1 → Finsupp.zipWith f hf g₁ g₂ = Finsupp.zipWith f_1 ⋯ g₁_1 g₂_1
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
/-- The inclusion `Z^n(f, g) ⟶ H^n(g)` of the kernel of `δ`.  -/
CategoryTheory.Abelian.SpectralObject.iCycles : {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 : ι} →
              (f : i ⟶ j) → (g : j ⟶ k) → (n : ℤ) → X.cycles f g n ⟶ (X.H n).obj (CategoryTheory.ComposableArrows.mk₁ g)
-- Lean.Parser.Extra
/-- No-op parser that advises the pretty printer to emit a non-breaking space.  -/
Lean.Parser.ppHardSpace : Lean.Parser.Parser
-- Mathlib.NumberTheory.NumberField.EquivReindex
NumberField.det_of_basisMatrix_non_zero : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] [inst_2 : DecidableEq (K →+* ℂ)],
  (NumberField.basisMatrix K).det ≠ 0