mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
SemiNormedGrp₁.hom_comp : ∀ {M N O : SemiNormedGrp₁} (f : M ⟶ N) (g : N ⟶ O),
  ↑(SemiNormedGrp₁.Hom.hom (CategoryTheory.CategoryStruct.comp f g)) =
    (↑(SemiNormedGrp₁.Hom.hom g)).comp ↑(SemiNormedGrp₁.Hom.hom f)
-- Mathlib.Data.Real.Basic
Real.mk_sup : ∀ (a b : CauSeq ℚ abs), Real.mk (a ⊔ b) = max (Real.mk a) (Real.mk b)
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.mk_div : ∀ {α : Type u_1} {γ : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace γ]
  [inst_2 : Group γ] [inst_3 : IsTopologicalGroup γ] (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.Order.Interval.Set.Pi
Set.pi_univ_Ioc_update_union : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : DecidableEq ι] [inst_1 : (i : ι) → LinearOrder (α i)] (x y : (i : ι) → α i)
  (i₀ : ι),
  ∀ m ∈ Set.Icc (x i₀) (y i₀),
    ((Set.univ.pi fun i => Set.Ioc (x i) (Function.update y i₀ m i)) ∪
        Set.univ.pi fun i => Set.Ioc (Function.update x i₀ m i) (y i)) =
      Set.univ.pi fun i => Set.Ioc (x i) (y i)
-- Init.Data.SInt.Lemmas
Int8.toInt16_ne_minValue : ∀ (a : Int8), a.toInt16 ≠ Int16.minValue
-- Mathlib.Order.FixedPoints
OrderHom.lfp_lfp : ∀ {α : Type u} [inst : CompleteLattice α] (h : α →o α →o α), OrderHom.lfp (OrderHom.lfp.comp h) = OrderHom.lfp h.onDiag
-- Mathlib.Topology.Constructions.SumProd
isEmbedding_sumElim : ∀ {X : Type u} {Y : Type v} {Z : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] {f : X → Z} {g : Y → Z},
  Topology.IsEmbedding (Sum.elim f g) ↔
    Topology.IsEmbedding f ∧
      Topology.IsEmbedding g ∧
        Disjoint (closure (Set.range f)) (Set.range g) ∧ Disjoint (Set.range f) (closure (Set.range g))
-- Lean.Environment
/-- Whether the import's `.olean*` data has been loaded (otherwise only the `.ir` is).  -/
Lean.EffectiveImport.hasData : Lean.EffectiveImport → Bool
-- Mathlib.GroupTheory.GroupAction.Basic
AddAction.vadd_orbit : ∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] (g : G) (a : α),
  g +ᵥ AddAction.orbit G a = AddAction.orbit G a
-- Init.Data.String.Lemmas.IsEmpty
String.Slice.isEmpty_copy : ∀ {s : String.Slice}, s.copy.isEmpty = s.isEmpty
-- Mathlib.Tactic.Linter.MinImports
/-- The `minImports` linter incrementally computes the minimal imports needed for each file to build.
Whenever it detects that a new command requires an increase in the (transitive) imports that it
computed so far, it emits a warning mentioning the bigger minimal imports.

Unlike the related `#min_imports` command, the linter takes into account notation and tactic
information.
It also works incrementally, providing information that is better suited, for instance, to split
files.

Another important difference is that the `minImports` *linter* starts counting imports from
where the option is set to `true` *downwards*, whereas the `#min_imports` *command* looks at the
imports needed from the command *upwards*.
 -/
_private.Mathlib.Tactic.Linter.MinImports.0.Mathlib.Linter.MinImports.minImportsLinter : Lean.Linter
-- Init.Data.Array.Lemmas
Array.back_filterMap_of_eq_some : ∀ {α : Type u_1} {β : Type u_2} {f : α → Option β} {xs : Array α} {w : 0 < xs.size} {b : β}
  (h : f (xs.back w) = some b), (Array.filterMap f xs).back ⋯ = b
-- Init.Data.SInt.Bitwise
ISize.shiftLeft_xor : ∀ {a b c : ISize}, (a ^^^ b) <<< c = a <<< c ^^^ b <<< c
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddMonoidHom.ofClass.eq_1 : ∀ (A : Type u_2) (B : Type u_3) [inst : AddMonoid A] [inst_1 : AddMonoid B] [inst_2 : TopologicalSpace A]
  [inst_3 : TopologicalSpace B] (F : Type u_7) [inst_4 : FunLike F A B] [inst_5 : ContinuousMapClass F A B]
  [inst_6 : AddMonoidHomClass F A B] (f : F), ContinuousAddMonoidHom.ofClass A B F f = ↑f
-- Mathlib.NumberTheory.ModularForms.Basic
/-- **Alias** of `FunLike.coeMonoidHom_apply`. -/
CuspForm.coeHom_apply : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : MulOne F] [inst_2 : MulOneClass β]
  [inst_3 : IsOneApply F α β] [inst_4 : IsMulApply F α β] (f : F), (FunLike.coeMonoidHom F α β) f = ⇑f
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.State.mk.inj : ∀ {structs : Array Lean.Meta.Grind.Arith.Linear.Struct} {typeIdOf : Lean.PHashMap Lean.Meta.Sym.ExprPtr (Option ℕ)}
  {exprToStructId : Lean.PHashMap Lean.Meta.Sym.ExprPtr ℕ} {exprToStructIdEntries : Lean.PArray (Lean.Expr × ℕ)}
  {forbiddenNatModules : Lean.PHashSet Lean.Meta.Sym.ExprPtr}
  {natStructs : Array Lean.Meta.Grind.Arith.Linear.NatStruct}
  {natTypeIdOf : Lean.PHashMap Lean.Meta.Sym.ExprPtr (Option ℕ)}
  {exprToNatStructId : Lean.PHashMap Lean.Meta.Sym.ExprPtr ℕ} {structs_1 : Array Lean.Meta.Grind.Arith.Linear.Struct}
  {typeIdOf_1 : Lean.PHashMap Lean.Meta.Sym.ExprPtr (Option ℕ)}
  {exprToStructId_1 : Lean.PHashMap Lean.Meta.Sym.ExprPtr ℕ} {exprToStructIdEntries_1 : Lean.PArray (Lean.Expr × ℕ)}
  {forbiddenNatModules_1 : Lean.PHashSet Lean.Meta.Sym.ExprPtr}
  {natStructs_1 : Array Lean.Meta.Grind.Arith.Linear.NatStruct}
  {natTypeIdOf_1 : Lean.PHashMap Lean.Meta.Sym.ExprPtr (Option ℕ)}
  {exprToNatStructId_1 : Lean.PHashMap Lean.Meta.Sym.ExprPtr ℕ},
  { structs := structs, typeIdOf := typeIdOf, exprToStructId := exprToStructId,
        exprToStructIdEntries := exprToStructIdEntries, forbiddenNatModules := forbiddenNatModules,
        natStructs := natStructs, natTypeIdOf := natTypeIdOf, exprToNatStructId := exprToNatStructId } =
      { structs := structs_1, typeIdOf := typeIdOf_1, exprToStructId := exprToStructId_1,
        exprToStructIdEntries := exprToStructIdEntries_1, forbiddenNatModules := forbiddenNatModules_1,
        natStructs := natStructs_1, natTypeIdOf := natTypeIdOf_1, exprToNatStructId := exprToNatStructId_1 } →
    structs = structs_1 ∧
      typeIdOf = typeIdOf_1 ∧
        exprToStructId = exprToStructId_1 ∧
          exprToStructIdEntries = exprToStructIdEntries_1 ∧
            forbiddenNatModules = forbiddenNatModules_1 ∧
              natStructs = natStructs_1 ∧ natTypeIdOf = natTypeIdOf_1 ∧ exprToNatStructId = exprToNatStructId_1
-- Mathlib.Algebra.Module.ZLattice.Basic
ZSpan.instDiscreteTopologySubtypeMemAddSubgroupToAddSubgroupIntSpanRangeCoeBasisRealOfFinite : ∀ {E : Type u_1} {ι : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (b : Module.Basis ι ℝ E)
  [Finite ι], DiscreteTopology ↥(Submodule.span ℤ (Set.range ⇑b)).toAddSubgroup
-- Mathlib.MeasureTheory.Measure.Support
MeasureTheory.Measure.support_eq_univ : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : MeasurableSpace X] {μ : MeasureTheory.Measure X}
  [μ.IsOpenPosMeasure], μ.support = Set.univ
-- Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
/-- The `a₃` coefficient of a Weierstrass curve.  -/
WeierstrassCurve.a₃ : {R : Type u} → WeierstrassCurve R → R
-- Mathlib.Combinatorics.Matroid.Constructions
Matroid.freeOn_isBasis'_iff : ∀ {α : Type u_1} {E I X : Set α}, (Matroid.freeOn E).IsBasis' I X ↔ I = X ∩ E
-- Mathlib.CategoryTheory.Simple
CategoryTheory.instNontrivialSubobjectOfSimple : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [CategoryTheory.Limits.HasZeroObject C] {X : C} [CategoryTheory.Simple X], Nontrivial (CategoryTheory.Subobject X)
-- Mathlib.Order.RelIso.Basic
/-- A relation is well founded iff its lift to a quotient is.  -/
wellFounded_lift₂_iff : ∀ {α : Type u_1} {x : Setoid α} {r : α → α → Prop} {H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂},
  WellFounded (Quotient.lift₂ r H) ↔ WellFounded r
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
MeasureTheory.locallyIntegrableOn_neg_iff : ∀ {X : Type u_1} {E : Type u_6} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] [inst_2 : NormedAddCommGroup E]
  {μ : MeasureTheory.Measure X} {s : Set X} {f : X → E},
  MeasureTheory.LocallyIntegrableOn (-f) s μ ↔ MeasureTheory.LocallyIntegrableOn f s μ
-- Mathlib.Topology.ContinuousOn
Filter.EventuallyEq.congr_continuousWithinAt_of_mem : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f g : α → β} {s : Set α}
  {x : α}, f =ᶠ[nhdsWithin x s] g → x ∈ s → (ContinuousWithinAt f s x ↔ ContinuousWithinAt g s x)
-- Mathlib.Order.WithBot
WithBot.map.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (f : α → β), WithBot.map f = Option.map f
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
/-- The functor sending a topological space `X` to its fundamental groupoid.  -/
FundamentalGroupoid.termπ : Lean.ParserDescr
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.SimplicialObject.δ_comp_σ_self'_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) {n : ℕ}
  {j : Fin (n + 2)} {i : Fin (n + 1)},
  j = i.castSucc →
    ∀ {Z : C} (h : X.obj (Opposite.op { len := n }) ⟶ Z),
      CategoryTheory.CategoryStruct.comp (X.σ i) (CategoryTheory.CategoryStruct.comp (X.δ j) h) = h
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.Compacts.coe_bot : ∀ {α : Type u_1} [inst : TopologicalSpace α], ↑⊥ = ∅
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instBEqInsertReplaceEdit.beq : Lean.Lsp.InsertReplaceEdit → Lean.Lsp.InsertReplaceEdit → Bool
-- Mathlib.Algebra.Ring.Int.Parity
Int.not_odd_iff : ∀ {n : ℤ}, ¬Odd n ↔ n % 2 = 0
-- Mathlib.RingTheory.Extension.Presentation.Submersive
/-- If `P` is submersive, `PreSubmersivePresentation.aevalDifferential` is an isomorphism.  -/
Algebra.SubmersivePresentation.aevalDifferentialEquiv : {R : Type u} →
  {S : Type v} →
    {ι : Type w} →
      {σ : Type t} →
        [inst : CommRing R] →
          [inst_1 : CommRing S] →
            [inst_2 : Algebra R S] → [inst_3 : Finite σ] → Algebra.SubmersivePresentation R S ι σ → (σ → S) ≃ₗ[S] σ → S
-- Init.Data.Int.Order
Int.neg_nonneg : ∀ {a : ℤ}, 0 ≤ -a ↔ a ≤ 0
-- Mathlib.Data.Set.Image
Set.image_empty : ∀ {α : Type u_1} {β : Type u_2} (f : α → β), f '' ∅ = ∅
-- Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
/-- Pre-composition by a *fixed* continuous linear map as a continuous linear map for the uniform
convergence topology.  -/
ContinuousLinearMap.precompUniformConvergenceCLM : {𝕜₁ : Type u_6} →
  {𝕜₂ : Type u_7} →
    {𝕜₃ : Type u_8} →
      [inst : NormedField 𝕜₁] →
        [inst_1 : NormedField 𝕜₂] →
          [inst_2 : NormedField 𝕜₃] →
            {σ : 𝕜₁ →+* 𝕜₂} →
              {τ : 𝕜₂ →+* 𝕜₃} →
                {ρ : 𝕜₁ →+* 𝕜₃} →
                  [RingHomCompTriple σ τ ρ] →
                    {E : Type u_9} →
                      {F : Type u_10} →
                        (G : Type u_11) →
                          [inst_4 : AddCommGroup E] →
                            [inst_5 : Module 𝕜₁ E] →
                              [inst_6 : AddCommGroup F] →
                                [inst_7 : Module 𝕜₂ F] →
                                  [inst_8 : AddCommGroup G] →
                                    [inst_9 : Module 𝕜₃ G] →
                                      [inst_10 : TopologicalSpace E] →
                                        [inst_11 : TopologicalSpace F] →
                                          [inst_12 : TopologicalSpace G] →
                                            (𝔖 : Set (Set E)) →
                                              (𝔗 : Set (Set F)) →
                                                [inst_13 : IsTopologicalAddGroup G] →
                                                  [inst_14 : ContinuousConstSMul 𝕜₃ G] →
                                                    (L : E →SL[σ] F) →
                                                      Set.MapsTo (fun x => ⇑L '' x) 𝔖 𝔗 →
                                                        UniformConvergenceCLM τ G 𝔗 →L[𝕜₃] UniformConvergenceCLM ρ G 𝔖
-- Mathlib.SetTheory.Lists
Lists'.subset_nil : ∀ {α : Type u_1} {l : Lists' α true}, l ⊆ Lists'.nil → l = Lists'.nil
-- Mathlib.Algebra.Module.Submodule.Bilinear
Submodule.map₂_iSup_left : ∀ {ι : Sort uι} {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [inst : CommSemiring R]
  [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : Module R M]
  [inst_5 : Module R N] [inst_6 : Module R P] (f : M →ₗ[R] N →ₗ[R] P) (s : ι → Submodule R M) (t : Submodule R N),
  Submodule.map₂ f (⨆ i, s i) t = ⨆ i, Submodule.map₂ f (s i) t
-- Mathlib.RingTheory.OrderOfVanishing.Basic
/-- The sequence `R ⧸ I →ₗ[R] R ⧸ (a • I) →ₗ[R] R ⧸ (Ideal.span {a})` given by multiplication
by `a` then quotienting by the ideal generated by `a` is exact.
 -/
Ideal.exact_mulQuot_quotOfMul : ∀ {R : Type u_1} [inst : CommRing R] {a : R} (I : Ideal R), Function.Exact ⇑(Ideal.mulQuot a I) ⇑(Ideal.quotOfMul a I)
-- Mathlib.Data.Part
Part.ne_none_iff : ∀ {α : Type u_1} {o : Part α}, o ≠ Part.none ↔ ∃ x, o = Part.some x
-- Mathlib.Order.Filter.Pointwise
Filter.principal_zero : ∀ {α : Type u_2} [inst : Zero α], Filter.principal 0 = 0
-- Mathlib.CategoryTheory.Monoidal.Grp
/-- An additive group object internal to a cartesian monoidal category.
Also see the bundled `AddGrp`.  -/
CategoryTheory.AddGrpObj : {C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → [CategoryTheory.CartesianMonoidalCategory C] → C → Type v₁
-- Mathlib.Order.Category.BddDistLat
_private.Mathlib.Order.Category.BddDistLat.0.BddDistLat.Hom.mk : {X Y : BddDistLat} → BoundedLatticeHom ↑X.toDistLat ↑Y.toDistLat → X.Hom Y
-- Init.Data.Vector.Lemmas
Vector.flatten_replicate_replicate : ∀ {n m : ℕ} {α : Type u_1} {a : α}, (Vector.replicate n (Vector.replicate m a)).flatten = Vector.replicate (n * m) a
-- Lean.Parser.Term
Lean.Parser.semicolonOrLinebreak.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Topology.UrysohnsLemma
/-- The proof that we can divide `CU` pairs in half  -/
Urysohns.CU.hP : ∀ {X : Type u_2} [inst : TopologicalSpace X] {P : Set X → Set X → Prop} (self : Urysohns.CU P) {c u : Set X},
  IsClosed c → P c u → IsOpen u → c ⊆ u → ∃ v, IsOpen v ∧ c ⊆ v ∧ closure v ⊆ u ∧ P c v ∧ P (closure v) u
-- Init.Data.UInt.Lemmas
UInt8.toUInt32_ofNatTruncate_of_lt : ∀ {n : ℕ} (hn : n < UInt8.size), (UInt8.ofNatClamp n).toUInt32 = UInt32.ofNatLT n ⋯
-- Mathlib.Topology.ContinuousMap.StoneWeierstrass
ContinuousMap.ker_evalStarAlgHom_inter_adjoin_id : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] (s : Set 𝕜) (h0 : 0 ∈ s),
  ↑(StarAlgebra.adjoin 𝕜 {ContinuousMap.restrict s (ContinuousMap.id 𝕜)}) ∩
      ↑(RingHom.ker (ContinuousMap.evalStarAlgHom 𝕜 𝕜 ⟨0, h0⟩)) =
    ↑(NonUnitalStarAlgebra.adjoin 𝕜 {ContinuousMap.restrict s (ContinuousMap.id 𝕜)})
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Matrix.GeneralLinearGroup.map_mul_map_inv : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] {S : Type u_1}
  [inst_3 : CommRing S] (f : R →+* S) (g : GL n R),
  (Matrix.GeneralLinearGroup.map f) g * (Matrix.GeneralLinearGroup.map f) g⁻¹ = 1
-- Std.Http.Protocol.H1
/-- Advances reader-side state machine by one logical transition.

Dispatches parsing work according to current reader state (start-line, headers,
body, completion, or failure handling).
 -/
Std.Http.Protocol.H1.Machine.processRead : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Machine dir → Std.Http.Protocol.H1.Machine dir
-- Mathlib.Probability.Kernel.Composition.CompProd
ProbabilityTheory.Kernel.compProd_sum_right : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} {ι : Type u_4} [inst : Countable ι] {κ : ProbabilityTheory.Kernel α β}
  {η : ι → ProbabilityTheory.Kernel (α × β) γ} [∀ (i : ι), ProbabilityTheory.IsSFiniteKernel (η i)],
  κ.compProd (ProbabilityTheory.Kernel.sum η) = ProbabilityTheory.Kernel.sum fun i => κ.compProd (η i)
-- Mathlib.AlgebraicGeometry.Properties
AlgebraicGeometry.instIsDomainCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensTopOfIsIntegral : ∀ (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsIntegral X], IsDomain ↑(X.presheaf.obj (Opposite.op ⊤))
-- Mathlib.Algebra.Order.Quantale
IsAddQuantale.mk : ∀ {α : Type u_1} [inst : AddSemigroup α] [inst_1 : CompleteLattice α],
  (∀ (x : α) (s : Set α), x + sSup s = ⨆ y ∈ s, x + y) →
    (∀ (s : Set α) (y : α), sSup s + y = ⨆ x ∈ s, x + y) → IsAddQuantale α
-- Mathlib.Data.Finset.Lattice.Fold
Finset.codisjoint_inf_right : ∀ {α : Type u_2} {ι : Type u_5} [inst : DistribLattice α] [inst_1 : OrderTop α] {s : Finset ι} {f : ι → α} {a : α},
  Codisjoint a (s.inf f) ↔ ∀ ⦃i : ι⦄, i ∈ s → Codisjoint a (f i)
-- Mathlib.GroupTheory.GroupAction.Basic
AddAction.stabilizerEquivStabilizer_apply : ∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] {g : G} {a b : α} (hg : b = g +ᵥ a)
  (x : ↥(AddAction.stabilizer G a)), ↑((AddAction.stabilizerEquivStabilizer hg) x) = (AddAut.addConj g) ↑x
-- Mathlib.RingTheory.AdicCompletion.Topology
Submodule.mul.congr_simp : ∀ {R : Type u} [inst : Semiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A], Submodule.mul = Submodule.mul
-- Mathlib.LinearAlgebra.TensorProduct.Basic
TensorProduct.ext_threefold : ∀ {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} {P : Type u_9} {P₂ : Type u_17} [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid N]
  [inst_4 : AddCommMonoid P] [inst_5 : AddCommMonoid P₂] [inst_6 : Module R M] [inst_7 : Module R N]
  [inst_8 : Module R₂ P₂] [inst_9 : Module R P] {g h : TensorProduct R (TensorProduct R M N) P →ₛₗ[σ₁₂] P₂},
  (∀ (x : M) (y : N) (z : P), g (x ⊗ₜ[R] y ⊗ₜ[R] z) = h (x ⊗ₜ[R] y ⊗ₜ[R] z)) → g = h
-- Mathlib.Algebra.Category.Grp.Limits
AddCommGrpCat.hasLimits : CategoryTheory.Limits.HasLimits AddCommGrpCat
-- Mathlib.Topology.Bornology.BoundedOperation
isBounded_nsmul : ∀ {R : Type u_2} [inst : Bornology R] [inst_1 : AddMonoid R] [BoundedAdd R] {s : Set R},
  Bornology.IsBounded s → ∀ (n : ℕ), Bornology.IsBounded ((fun x => n • x) '' s)
-- Init.WFExtrinsicFix
WellFounded.partialExtrinsicFix₃_eq_apply : ∀ {α : Sort u_2} {β : α → Sort u_4} {γ : (a : α) → β a → Sort u_3} {C₃ : (a : α) → (b : β a) → γ a b → Sort u_1}
  [inst : ∀ (a : α) (b : β a) (c : γ a b), Nonempty (C₃ a b c)]
  {R : (a : α) ×' (b : β a) ×' γ a b → (a : α) ×' (b : β a) ×' γ a b → Prop}
  {F :
    (a : α) →
      (b : β a) →
        (c : γ a b) → ((a' : α) → (b' : β a') → (c' : γ a' b') → R ⟨a', ⟨b', c'⟩⟩ ⟨a, ⟨b, c⟩⟩ → C₃ a' b' c') → C₃ a b c}
  {a : α} {b : β a} {c : γ a b},
  WellFounded R →
    WellFounded.partialExtrinsicFix₃ R F a b c =
      F a b c fun a_1 b_1 c_1 x => WellFounded.partialExtrinsicFix₃ R F a_1 b_1 c_1
-- Mathlib.CategoryTheory.Monoidal.Subcategory
CategoryTheory.ObjectProperty.tensorObj_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (P : CategoryTheory.ObjectProperty C) [inst_2 : P.IsMonoidal] (X Y : P.FullSubcategory),
  (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).obj =
    CategoryTheory.MonoidalCategoryStruct.tensorObj X.obj Y.obj
-- Mathlib.Data.ENNReal.Holder
ENNReal.HolderConjugate.unique : ∀ (p q : ENNReal) [p.HolderConjugate q] (q' : ENNReal) [hq' : p.HolderConjugate q'], q = q'
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.baseChange_dblX : ∀ {R : Type r} {S : Type s} {A : Type u} {B : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing A]
  [inst_3 : CommRing B] {W' : WeierstrassCurve.Jacobian R} [inst_4 : Algebra R S] [inst_5 : Algebra R A]
  [inst_6 : Algebra S A] [IsScalarTower R S A] [inst_8 : Algebra R B] [inst_9 : Algebra S B] [IsScalarTower R S B]
  (f : A →ₐ[S] B) (P : Fin 3 → A), (W'.baseChange B).dblX (⇑f ∘ P) = f ((W'.baseChange A).dblX P)
-- Mathlib.Algebra.Homology.SpectralObject.Basic
CategoryTheory.Abelian.SpectralObject.zero₁ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{u_3, u_1} C]
  [inst_1 : CategoryTheory.Category.{u_4, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k)
  (h : CategoryTheory.CategoryStruct.comp f g = fg) (n₀ n₁ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.zero₁._auto_1),
  CategoryTheory.CategoryStruct.comp (X.δ f g n₀ n₁ hn₁)
      ((X.H n₁).map (CategoryTheory.ComposableArrows.twoδ₂Toδ₁ f g fg h)) =
    0
-- Mathlib.Analysis.Analytic.Composition
/-- The auxiliary set corresponding to the composition of partial sums asymptotically contains
all possible compositions.  -/
FormalMultilinearSeries.compPartialSumTarget_tendsto_prod_atTop : Filter.Tendsto (fun p => FormalMultilinearSeries.compPartialSumTarget 0 p.1 p.2) Filter.atTop Filter.atTop
-- Mathlib.Analysis.Complex.UpperHalfPlane.Topology
Continuous.upperHalfPlaneMk : ∀ {X : Type u_1} [inst : TopologicalSpace X] {f : X → ℂ},
  Continuous f → ∀ (hf₀ : ∀ (x : X), 0 < (f x).im), Continuous fun x => { coe := f x, coe_im_pos := ⋯ }
-- Mathlib.RingTheory.PowerBasis
PowerBasis.mk : {R : Type u_7} →
  {S : Type u_8} →
    [inst : CommRing R] →
      [inst_1 : Ring S] →
        [inst_2 : Algebra R S] →
          (gen : S) →
            (dim : ℕ) → (basis : Module.Basis (Fin dim) R S) → (∀ (i : Fin dim), basis i = gen ^ ↑i) → PowerBasis R S
-- Mathlib.NumberTheory.Zsqrtd.GaussianInt
GaussianInt.toComplex_zero : GaussianInt.toComplex 0 = 0
-- Qq.Match
Qq.Impl.PatternVar.mvar : Qq.Impl.PatternVar → Lean.Expr
-- Mathlib.Tactic.IntervalCases
/-- Given a proof `pf`, attempts to parse it as an upper (`lb = false`) or lower (`lb = true`)
bound on `n`. If successful, it returns `(bound, n, pf')` where `n` is a numeral and
`pf'` proves `n ≤ e` or `n ≱ e` (as described by `bound`).
 -/
Mathlib.Tactic.IntervalCases.Methods.getBound : Mathlib.Tactic.IntervalCases.Methods →
  Lean.Expr → Lean.Expr → Bool → Lean.MetaM (Mathlib.Tactic.IntervalCases.Bound × Lean.Expr × Lean.Expr)
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
_private.Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass.0.PeriodPair.relation.eq_1 : ∀ (L : PeriodPair) (z : ℂ),
  PeriodPair.relation✝ L z =
    if z ∈ L.lattice then 0 else L.derivWeierstrassP z ^ 2 - 4 * L.weierstrassP z ^ 3 + L.g₂ * L.weierstrassP z + L.g₃
-- Mathlib.Logic.Godel.GodelBetaFunction
_private.Mathlib.Logic.Godel.GodelBetaFunction.0.Nat.coprimes : {m : ℕ} → (Fin m → ℕ) → Fin m → ℕ
-- Mathlib.Topology.LocallyFinsupp
Function.locallyFinsuppWithin.coe_add : ∀ {X : Type u_1} [inst : TopologicalSpace X] {U : Set X} {Y : Type u_2} [inst_1 : AddMonoid Y]
  (D₁ D₂ : Function.locallyFinsuppWithin U Y), ⇑(D₁ + D₂) = ⇑D₁ + ⇑D₂
-- Init.Data.Vector.Stream
Vector.instToStreamSubarray : {α : Type u_1} → {n : ℕ} → Std.ToStream (Vector α n) (Subarray α)
-- Mathlib.Algebra.Group.Commute.Basic
AddCommute.zsmul_zsmul_self : ∀ {G : Type u_1} [inst : AddGroup G] (a : G) (m n : ℤ), AddCommute (m • a) (n • a)
-- Mathlib.RepresentationTheory.Rep.Basic
/-- An object of `Rep k G` is zero iff the underlying `k`-module is zero.  -/
Rep.isZero_iff : ∀ (k : Type u) (G : Type v) [inst : Ring k] [inst_1 : Monoid G] (M : Rep.{u_1, u, v} k G),
  CategoryTheory.Limits.IsZero M ↔ Subsingleton ↑M
-- Mathlib.Algebra.Ring.CompTypeclasses
RingHomInvPair.comp_apply_eq : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ : R₁ →+* R₂} {σ' : R₂ →+* R₁}
  [RingHomInvPair σ σ'] {x : R₁}, σ' (σ x) = x