mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.coequalizerComparison_map_desc : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] (f g : X ⟶ Y) {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D)
  [inst_2 : CategoryTheory.Limits.HasCoequalizer f g]
  [inst_3 : CategoryTheory.Limits.HasCoequalizer (G.map f) (G.map g)] {Z : C} {h : Y ⟶ Z}
  (w : CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g h),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coequalizerComparison f g G)
      (G.map (CategoryTheory.Limits.coequalizer.desc h w)) =
    CategoryTheory.Limits.coequalizer.desc (G.map h) ⋯
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.union_add_inter_subset : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : AddCommSemigroup α] {s t : Finset α}, s ∪ t + s ∩ t ⊆ s + t
-- Lean.Meta.Basic
/-- Replace free (or meta) variables `xs` with loose bound variables.
Similar to `Expr.abstract`, but handles metavariables correctly.
 -/
Lean.Expr.abstractM : Lean.Expr → Array Lean.Expr → Lean.MetaM Lean.Expr
-- Init.Data.UInt.Lemmas
USize.toBitVec_neg : ∀ {a : USize}, (-a).toBitVec = -a.toBitVec
-- Mathlib.Data.Sum.Order
Sum.Lex.toLexRelIsoLT_symm_coe : ∀ {α : Type u_1} {β : Type u_2} [inst : LT α] [inst_1 : LT β], ⇑Sum.Lex.toLexRelIsoLT.symm = ⇑ofLex
-- Mathlib.Algebra.Group.UniqueProds.Basic
/-- This instance asserts that if `G` has a left-cancellative addition, a linear order, and
addition is strictly monotone w.r.t. the first argument, then `G` has `TwoUniqueSums`.  -/
TwoUniqueSums.of_covariant_left : ∀ {G : Type u} [inst : Add G] [IsLeftCancelAdd G] [inst_2 : LinearOrder G] [AddRightStrictMono G], TwoUniqueSums G
-- Init.Data.List.ToArray
Array.insertIdx.congr_simp : ∀ {α : Type u} (as as_1 : Array α) (e_as : as = as_1) (i i_1 : ℕ) (e_i : i = i_1) (a a_1 : α),
  a = a_1 → ∀ (x : i ≤ as.size), as.insertIdx i a x = as_1.insertIdx i_1 a_1 ⋯
-- Mathlib.MeasureTheory.Group.Arithmetic
MulOpposite.instMeasurableMul₂ : ∀ {M : Type u_2} [inst : Mul M] [inst_1 : MeasurableSpace M] [MeasurableMul₂ M], MeasurableMul₂ Mᵐᵒᵖ
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
/-- The type of continuous functions vanishing at infinity, with the uniform distance induced by the
inclusion `ZeroAtInftyContinuousMap.toBCF`, is a pseudo-metric space.  -/
ZeroAtInftyContinuousMap.instPseudoMetricSpace : {α : Type u} →
  {β : Type v} →
    [inst : TopologicalSpace α] →
      [inst_1 : PseudoMetricSpace β] → [inst_2 : Zero β] → PseudoMetricSpace (ZeroAtInftyContinuousMap α β)
-- Mathlib.RingTheory.WittVector.Defs
WittVector.constantCoeff_wittNeg : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] (n : ℕ), MvPolynomial.constantCoeff (WittVector.wittNeg p n) = 0
-- Mathlib.CategoryTheory.Functor.Basic
CategoryTheory.Functor.id_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y),
  (CategoryTheory.Functor.id C).map f = f
-- Init.Data.List.ToArray
List.toArray_inj : ∀ {α : Type u_1} {as bs : List α}, as.toArray = bs.toArray → as = bs
-- Init.Data.Range.Polymorphic.SInt
Int16.le.eq_1 : ∀ (a b : Int16), a.le b = (a.toBitVec.sle b.toBitVec = true)
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.IsColoop.mem_of_isBase : ∀ {α : Type u_1} {M : Matroid α} {e : α} {B : Set α}, M.IsColoop e → M.IsBase B → e ∈ B
-- Mathlib.Data.NNRat.Defs
NNRat.exists : ∀ {p : ℚ≥0 → Prop}, (∃ q, p q) ↔ ∃ q, ∃ (hq : 0 ≤ q), p ⟨q, hq⟩
-- Lean.Parser.Term
Lean.Parser.Command.plainDocComment.formatter : Lean.PrettyPrinter.Formatter
-- Batteries.Data.BinomialHeap.Basic
_private.Batteries.Data.BinomialHeap.Basic.0.Batteries.BinomialHeap.Imp.HeapNode.WF.toHeap.go : ∀ {α : Type u_1} {le : α → α → Bool} {a : α} {res : Batteries.BinomialHeap.Imp.Heap α} {n : ℕ}
  {s : Batteries.BinomialHeap.Imp.HeapNode α},
  Batteries.BinomialHeap.Imp.HeapNode.WF le a s n →
    Batteries.BinomialHeap.Imp.Heap.WF le s.rank res →
      Batteries.BinomialHeap.Imp.Heap.WF le 0 (Batteries.BinomialHeap.Imp.HeapNode.toHeap.go s s.rank res)
-- Batteries.Data.Int
_private.Batteries.Data.Int.0.Int.testBit.match_1.eq_1 : ∀ (motive : ℤ → ℕ → Sort u_1) (m n : ℕ) (h_1 : (m n : ℕ) → motive (Int.ofNat m) n)
  (h_2 : (m n : ℕ) → motive (Int.negSucc m) n),
  (match Int.ofNat m, n with
    | Int.ofNat m, n => h_1 m n
    | Int.negSucc m, n => h_2 m n) =
    h_1 m n
-- Mathlib.Algebra.Group.Action.Pi
Pi.mulAction.eq_1 : ∀ {ι : Type u_1} {α : ι → Type u_4} (M : Type u_7) {m : Monoid M} [inst : (i : ι) → MulAction M (α i)],
  Pi.mulAction M = { toSMul := Pi.instSMul, mul_smul := ⋯, one_smul := ⋯ }
-- Mathlib.Geometry.Euclidean.Angle.Bisector
/-- Auxiliary lemma for the special case of
`dist_orthogonalProjection_line_eq_of_two_zsmul_oangle_eq` where the orthogonal projection of `p`
to the line `p₁ p₂` or `p₁ p₃` is `p₁`.  -/
_private.Mathlib.Geometry.Euclidean.Angle.Bisector.0.EuclideanGeometry.dist_orthogonalProjection_line_eq_of_two_zsmul_oangle_eq_aux₂ : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [inst_4 : Fact (Module.finrank ℝ V = 2)] [inst_5 : Module.Oriented ℝ V (Fin 2)]
  {p p₁ p₂ p₃ : P},
  p₁ ≠ p₂ →
    p₁ ≠ p₃ →
      2 • EuclideanGeometry.oangle p₂ p₁ p = 2 • EuclideanGeometry.oangle p p₁ p₃ →
        ↑((EuclideanGeometry.orthogonalProjection line[ℝ, p₁, p₂]) p) = p₁ ∨
            ↑((EuclideanGeometry.orthogonalProjection line[ℝ, p₁, p₃]) p) = p₁ →
          dist p ↑((EuclideanGeometry.orthogonalProjection line[ℝ, p₁, p₂]) p) =
            dist p ↑((EuclideanGeometry.orthogonalProjection line[ℝ, p₁, p₃]) p)
-- Mathlib.Order.CompleteLattice.Basic
sInf_le_sSup_of_nonempty_inter : ∀ {α : Type u_1} [inst : CompleteLattice α] {s t : Set α}, (s ∩ t).Nonempty → sInf s ≤ sSup t
-- Mathlib.Order.Interval.Set.Basic
Set.instNoMinOrderElemIio : ∀ {α : Type u_1} [inst : Preorder α] {a : α} [NoMinOrder α], NoMinOrder ↑(Set.Iio a)
-- Mathlib.RingTheory.SimpleModule.Basic
/-- Schur's Lemma makes the endomorphism ring of a simple module a division ring.  -/
Module.End.instDivisionRing : {R : Type u_2} →
  [inst : Ring R] →
    {M : Type u_4} →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] → [DecidableEq (Module.End R M)] → [IsSimpleModule R M] → DivisionRing (Module.End R M)
-- Lean.Server.Completion.CompletionUtils
Lean.Server.Completion.ContextualizedCompletionInfo.mk : Lean.Server.Completion.HoverInfo →
  Lean.Elab.ContextInfo → Lean.Elab.CompletionInfo → Lean.Server.Completion.ContextualizedCompletionInfo
-- Mathlib.Algebra.Group.Finsupp
Finsupp.coeFnAddHom_apply : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddZeroClass M] (a : ι →₀ M) (a_1 : ι), Finsupp.coeFnAddHom a a_1 = a a_1
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.ConnectedComponent.maximal_connected_induce_iff : ∀ {V : Type u} {G : SimpleGraph V} (s : Set V),
  Maximal (fun x => (SimpleGraph.induce x G).Connected) s ↔ ∃ C, C.supp = s
-- Mathlib.Geometry.Manifold.Immersion
/-- If `f: M → N` and `g: M' × N'` are immersions at `x` and `x'` (w.r.t. `F` and `F'`),
respectively, then `f × g: M × N → M' × N'` is an immersion at `(x, x')` w.r.t. `F × F'`.  -/
Manifold.IsImmersionOfComplement.prodMap : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} {E' : Type u_3} {E''' : Type u_4} {E'' : Type u}
  {F : Type u_5} {F' : Type u_6} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] [inst_5 : NormedAddCommGroup E'']
  [inst_6 : NormedSpace 𝕜 E''] [inst_7 : NormedAddCommGroup E'''] [inst_8 : NormedSpace 𝕜 E''']
  [inst_9 : NormedAddCommGroup F] [inst_10 : NormedSpace 𝕜 F] [inst_11 : NormedAddCommGroup F']
  [inst_12 : NormedSpace 𝕜 F'] {H : Type u_7} [inst_13 : TopologicalSpace H] {H' : Type u_8}
  [inst_14 : TopologicalSpace H'] {G : Type u_9} [inst_15 : TopologicalSpace G] {G' : Type u_10}
  [inst_16 : TopologicalSpace G'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'}
  {J : ModelWithCorners 𝕜 E'' G} {J' : ModelWithCorners 𝕜 E''' G'} {M : Type u_11} [inst_17 : TopologicalSpace M]
  [inst_18 : ChartedSpace H M] {M' : Type u_12} [inst_19 : TopologicalSpace M'] [inst_20 : ChartedSpace H' M']
  {N : Type u_13} [inst_21 : TopologicalSpace N] [inst_22 : ChartedSpace G N] {N' : Type u_14}
  [inst_23 : TopologicalSpace N'] [inst_24 : ChartedSpace G' N'] {n : WithTop ℕ∞} {f : M → N} {g : M' → N'}
  [IsManifold I n M] [IsManifold I' n M'] [IsManifold J n N] [⋯], ⋯
-- Lean.Server.References
Lean.Server.References.MatchedDefinition.mk.sizeOf_spec : ∀ {α : Type} [inst : SizeOf α] (mod : Lean.Name) (modUri : Lean.Lsp.DocumentUri) (ident : α) (range : Lean.Lsp.Range),
  sizeOf { mod := mod, modUri := modUri, ident := ident, range := range } =
    1 + sizeOf mod + sizeOf modUri + sizeOf ident + sizeOf range
-- Mathlib.Algebra.Group.Units.Hom
/-- Prefer `IsLocalHom.of_leftInverse`, but we can't get rid of this because of `ToAdditive`.  -/
isUnit_map_of_leftInverse : ∀ {F : Type u_1} {G : Type u_2} {M : Type u_3} {N : Type u_4} [inst : FunLike F M N] [inst_1 : FunLike G N M]
  [inst_2 : Monoid M] [inst_3 : Monoid N] [MonoidHomClass F M N] [MonoidHomClass G N M] {f : F} {x : M} (g : G),
  Function.LeftInverse ⇑g ⇑f → (IsUnit (f x) ↔ IsUnit x)
-- Init.Grind.Ring.CommSolver
_private.Init.Grind.Ring.CommSolver.0.Lean.Grind.CommRing.Expr.toPoly.match_4.eq_8 : ∀ (motive : Lean.Grind.CommRing.Expr → Sort u_1) (a b : Lean.Grind.CommRing.Expr)
  (h_1 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.num k))
  (h_2 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.intCast k))
  (h_3 : (k : ℕ) → motive (Lean.Grind.CommRing.Expr.natCast k))
  (h_4 : (x : Lean.Grind.CommRing.Var) → motive (Lean.Grind.CommRing.Expr.var x))
  (h_5 : (a b : Lean.Grind.CommRing.Expr) → motive (a.add b))
  (h_6 : (a b : Lean.Grind.CommRing.Expr) → motive (a.mul b)) (h_7 : (a : Lean.Grind.CommRing.Expr) → motive a.neg)
  (h_8 : (a b : Lean.Grind.CommRing.Expr) → motive (a.sub b))
  (h_9 : (a : Lean.Grind.CommRing.Expr) → (k : ℕ) → motive (a.pow k)),
  (match a.sub b with
    | Lean.Grind.CommRing.Expr.num k => h_1 k
    | Lean.Grind.CommRing.Expr.intCast k => h_2 k
    | Lean.Grind.CommRing.Expr.natCast k => h_3 k
    | Lean.Grind.CommRing.Expr.var x => h_4 x
    | a.add b => h_5 a b
    | a.mul b => h_6 a b
    | a.neg => h_7 a
    | a.sub b => h_8 a b
    | a.pow k => h_9 a k) =
    h_8 a b
-- Mathlib.Analysis.Calculus.LocalExtr.LineDeriv
IsLocalMax.hasLineDerivAt_eq_zero : ∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : Module ℝ E] [inst_2 : TopologicalSpace E] [ContinuousAdd E]
  [ContinuousSMul ℝ E] {f : E → ℝ} {a b : E} {f' : ℝ}, IsLocalMax f a → HasLineDerivAt ℝ f f' a b → f' = 0
-- Lean.LoadDynlib
_private.Lean.LoadDynlib.0.Lean.loadDynlib.unsafe_impl_2 : Lean.Dynlib → BaseIO Lean.Dynlib
-- Mathlib.Analysis.SpecialFunctions.Arsinh
Real.sinhEquiv_apply : ∀ (x : ℝ), Real.sinhEquiv x = Real.sinh x
-- Mathlib.Order.Lex
Colex.forall : ∀ {α : Type u_1} {p : Colex α → Prop}, (∀ (a : Colex α), p a) ↔ ∀ (a : α), p (toColex a)
-- Lean.Elab.Tactic.Grind.Main
_private.Lean.Elab.Tactic.Grind.Main.0.Lean.Elab.Tactic.elabGrindPattern.findLHS : Array Lean.Expr → Lean.Syntax → Lean.Elab.TermElabM (Lean.LocalDecl × ℕ)
-- Mathlib.Algebra.Group.Subgroup.Pointwise
Subgroup.coe_pointwise_smul : ∀ {α : Type u_1} {G : Type u_2} [inst : Group G] [inst_1 : Monoid α] [inst_2 : MulDistribMulAction α G] (a : α)
  (S : Subgroup G), ↑(a • S) = a • ↑S
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.Term.relabel_relabel : ∀ {L : FirstOrder.Language} {α : Type u'} {β : Type v'} {γ : Type u_1} (f : α → β) (g : β → γ) (t : L.Term α),
  FirstOrder.Language.Term.relabel g (FirstOrder.Language.Term.relabel f t) = FirstOrder.Language.Term.relabel (g ∘ f) t
-- Mathlib.CategoryTheory.MorphismProperty.Factorization
/-- A chosen term in `FunctorialFactorizationData W₁ W₂` when the functorial factorization
axiom `HasFunctorialFactorization W₁ W₂` holds.  -/
CategoryTheory.MorphismProperty.functorialFactorizationData : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    (W₁ W₂ : CategoryTheory.MorphismProperty C) → [W₁.HasFunctorialFactorization W₂] → W₁.FunctorialFactorizationData W₂
-- Mathlib.Algebra.Order.BigOperators.Expect
Finset.expect_pos : ∀ {ι : Type u_1} {α : Type u_2} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [IsOrderedCancelAddMonoid α]
  [inst_3 : Module ℚ≥0 α] [PosSMulStrictMono ℚ≥0 α] {s : Finset ι} {f : ι → α},
  (∀ i ∈ s, 0 < f i) → s.Nonempty → 0 < s.expect fun i => f i
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.instCommRingOfIsTopologicalRing : {α : Type u_1} →
  {β : Type u_2} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] → [inst_2 : CommRing β] → [IsTopologicalRing β] → CommRing C(α, β)
-- Mathlib.RingTheory.Bialgebra.Convolution
_private.Mathlib.RingTheory.Bialgebra.Convolution.0.AlgHom.convPow_succ : ∀ {R : Type u_1} {A : Type u_2} {C : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Semiring C]
  [inst_3 : Bialgebra R C] [inst_4 : Algebra R A] (f : WithConv (C →ₐ[R] A)) (n : ℕ), f ^ (n + 1) = f ^ n * f
-- Mathlib.Order.Hom.Basic
OrderIso.coe_symm_toRelIsoLT : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] (e : α ≃o β), ⇑e.toRelIsoLT.symm = ⇑e.symm
-- Mathlib.Algebra.Group.Pi.Lemmas
/-- Monoid homomorphism between the function spaces `I → α` and `I → β`, induced by a monoid
homomorphism `f` between `α` and `β`.  -/
MonoidHom.compLeft : {α : Type u_5} →
  {β : Type u_6} → [inst : MulOneClass α] → [inst_1 : MulOneClass β] → (α →* β) → (I : Type u_7) → (I → α) →* I → β
-- Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
/-- The morphism `Π F.obj (U i) ⟶ Π F.obj (U i) ⊓ (U j)` whose components
are given by the restriction maps from `U j` to `U i ⊓ U j`.
 -/
TopCat.Presheaf.SheafConditionEqualizerProducts.rightRes : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasProducts C] →
      {X : TopCat} →
        (F : TopCat.Presheaf C X) →
          {ι : Type v'} →
            (U : ι → TopologicalSpace.Opens ↑X) →
              TopCat.Presheaf.SheafConditionEqualizerProducts.piOpens F U ⟶
                TopCat.Presheaf.SheafConditionEqualizerProducts.piInters F U
-- Mathlib.CategoryTheory.ObjectProperty.Basic
CategoryTheory.ObjectProperty.ofObj_subtypeVal : ∀ {C : Type u} [inst : CategoryTheory.CategoryStruct.{v, u} C] (P : CategoryTheory.ObjectProperty C),
  CategoryTheory.ObjectProperty.ofObj Subtype.val = P
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.Indep.eq_1 : ∀ {Ω : Type u_1} (m₁ m₂ : MeasurableSpace Ω) {_mΩ : MeasurableSpace Ω} (μ : MeasureTheory.Measure Ω),
  ProbabilityTheory.Indep m₁ m₂ μ =
    ProbabilityTheory.Kernel.Indep m₁ m₂ (ProbabilityTheory.Kernel.const Unit μ) (MeasureTheory.Measure.dirac ())
-- Mathlib.RingTheory.Unramified.Basic
/-- This holds in general for epimorphisms.  -/
Algebra.FormallyUnramified.of_isLocalization : ∀ {R : Type u_1} {Rₘ : Type u_3} [inst : CommRing R] [inst_1 : CommRing Rₘ] (M : Submonoid R) [inst_2 : Algebra R Rₘ]
  [IsLocalization M Rₘ], Algebra.FormallyUnramified R Rₘ
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
HasProdUniformlyOn.hasProdLocallyUniformlyOn : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : CommMonoid α] {f : ι → β → α} {g : β → α} {s : Set β}
  [inst_1 : UniformSpace α] [inst_2 : TopologicalSpace β], HasProdUniformlyOn f g s → HasProdLocallyUniformlyOn f g s
-- Mathlib.Analysis.Normed.Lp.WithLp
WithLp.instVAddAssocClass : ∀ (p : ENNReal) {K : Type u_1} (K' : Type u_2) {V : Type u_4} [inst : VAdd K K'] [inst_1 : VAdd K V]
  [inst_2 : VAdd K' V] [VAddAssocClass K K' V], VAddAssocClass K K' (WithLp p V)
-- Init.Data.Nat.Div.Lemmas
Nat.div_lt_of_lt : ∀ {a b c : ℕ}, a < c → a / b < c
-- Mathlib.Algebra.Order.Group.Pointwise.Bounds
subset_upperBounds_add : ∀ {M : Type u_3} [inst : Add M] [inst_1 : Preorder M] [AddLeftMono M] [AddRightMono M] (s t : Set M),
  upperBounds s + upperBounds t ⊆ upperBounds (s + t)
-- Lean.Util.LeanOptions
Lean.instFromJsonLeanOptionValue : Lean.FromJson Lean.LeanOptionValue
-- Mathlib.CategoryTheory.Sites.Types
CategoryTheory.discreteSieve_mem : ∀ (α : Type u), CategoryTheory.discreteSieve α ∈ CategoryTheory.typesGrothendieckTopology α
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
Seminorm.IsBounded.eq_1 : ∀ {𝕜 : Type u_2} {𝕜₂ : Type u_3} {E : Type u_6} {F : Type u_7} {ι : Type u_9} {ι' : Type u_10} [inst : SeminormedRing 𝕜]
  [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] [inst_3 : SeminormedRing 𝕜₂] [inst_4 : AddCommGroup F]
  [inst_5 : Module 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [inst_6 : RingHomIsometric σ₁₂] (p : ι → Seminorm 𝕜 E)
  (q : ι' → Seminorm 𝕜₂ F) (f : E →ₛₗ[σ₁₂] F), Seminorm.IsBounded p q f = ∀ (i : ι'), ∃ s C, (q i).comp f ≤ C • s.sup p
-- Mathlib.Order.WithBot
WithBot.instPreorder : {α : Type u_1} → [Preorder α] → Preorder (WithBot α)
-- Mathlib.Topology.ContinuousMap.Basic
/-- To give a continuous map out of a disjoint union, it suffices to give a continuous map out of
each term. This is `Sigma.uncurry` for continuous maps.
 -/
ContinuousMap.sigma : {I : Type u_5} →
  {A : Type u_6} →
    {X : I → Type u_7} →
      [inst : TopologicalSpace A] →
        [inst_1 : (i : I) → TopologicalSpace (X i)] → ((i : I) → C(X i, A)) → C((i : I) × X i, A)
-- Mathlib.CategoryTheory.Noetherian
CategoryTheory.Artinian.isArtinianObject : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} [self : CategoryTheory.Artinian C] (X : C),
  CategoryTheory.IsArtinianObject X
-- Mathlib.Analysis.Calculus.TangentCone.Basic
mem_closure_of_nonempty_tangentConeAt : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : AddCommGroup E] [inst_1 : SMul 𝕜 E] [inst_2 : TopologicalSpace E] {s : Set E}
  {x : E} [ContinuousAdd E], (tangentConeAt 𝕜 s x).Nonempty → x ∈ closure s
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
/-- `sinh` is strictly monotone.  -/
Real.sinh_strictMono : StrictMono Real.sinh
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.Scheme.Opens.toSpecΓ.eq_1 : ∀ {X : AlgebraicGeometry.Scheme} (U : X.Opens),
  U.toSpecΓ = CategoryTheory.CategoryStruct.comp (↑U).toSpecΓ (AlgebraicGeometry.Spec.map U.topIso.inv)
-- Std.Data.DHashMap.Internal.Model
Std.DHashMap.Internal.Raw₀.getKey!ₘ.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : Inhabited α]
  (m : Std.DHashMap.Internal.Raw₀ α β) (a : α), m.getKey!ₘ a = (m.getKey?ₘ a).get!
-- Lean.Elab.Tactic.Omega.Frontend
_private.Lean.Elab.Tactic.Omega.Frontend.0.Lean.Elab.Tactic.Omega.formatErrorMessage.mentioned : Array Lean.Expr → Std.HashMap Lean.Omega.Coeffs Lean.Elab.Tactic.Omega.Fact → Lean.MetaM (Array Bool)
-- Lean.Data.JsonRpc
Lean.JsonRpc.instBEqResponseError : {α : Type u_1} → [BEq α] → BEq (Lean.JsonRpc.ResponseError α)
-- Mathlib.Analysis.Asymptotics.ExpGrowth
ExpGrowth.expGrowthSup_inv : ∀ {u : ℕ → ENNReal}, ExpGrowth.expGrowthSup u⁻¹ = -ExpGrowth.expGrowthInf u
-- Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind
NumberField.Ideal.liesOver_primesOverSpanEquivMonicFactorsMod_symm : ∀ {K : Type u_1} [inst : Field K] {θ : NumberField.RingOfIntegers K} {p : ℕ} [inst_1 : Fact (Nat.Prime p)]
  [NumberField K],
  ¬p ∣ RingOfIntegers.exponent θ →
    ∀ {Q : Polynomial ℤ},
      Polynomial.map (Int.castRingHom (ZMod p)) Q ∈ RingOfIntegers.monicFactorsMod θ p →
        (Ideal.span {↑p, (Polynomial.aeval θ) Q}).LiesOver (Ideal.span {↑p})
-- Mathlib.CategoryTheory.Monoidal.Arrow
CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.tensorObj_def : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPushouts C]
  [inst_2 : CategoryTheory.Limits.HasInitial C] [inst_3 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_4 : CategoryTheory.MonoidalClosed C] [inst_5 : CategoryTheory.BraidedCategory C] (X Y : CategoryTheory.Arrow C),
  CategoryTheory.MonoidalCategoryStruct.tensorObj X Y = X □ Y
-- Mathlib.ModelTheory.LanguageMap
/-- The inverse language homomorphism  -/
FirstOrder.Language.LEquiv.invLHom : {L : FirstOrder.Language} → {L' : FirstOrder.Language} → (L ≃ᴸ L') → (L' →ᴸ L)
-- Init.Data.SInt.Lemmas
Int16.toBitVec_inj : ∀ {a b : Int16}, a.toBitVec = b.toBitVec ↔ a = b
-- Init.Data.Nat.Lemmas
Nat.mod_eq_iff_lt : ∀ {n m : ℕ}, n ≠ 0 → (m % n = m ↔ m < n)
-- Init.Data.Nat.Lemmas
Nat.add_right_max_self : ∀ {a b : ℕ}, max (a + b) a = a + b
-- Mathlib.Computability.TuringMachine.StackTuringMachine
_private.Mathlib.Computability.TuringMachine.StackTuringMachine.0.Turing.TM2.stmts₁.match_1.eq_7 : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} (motive : Turing.TM2.Stmt Γ Λ σ → Sort u_5)
  (h_1 :
    (Q : Turing.TM2.Stmt Γ Λ σ) →
      (k : K) →
        (a : σ → Γ k) →
          (q : Turing.TM2.Stmt Γ Λ σ) → Q = Turing.TM2.Stmt.push k a q → motive (Turing.TM2.Stmt.push k a q))
  (h_2 :
    (Q : Turing.TM2.Stmt Γ Λ σ) →
      (k : K) →
        (a : σ → Option (Γ k) → σ) →
          (q : Turing.TM2.Stmt Γ Λ σ) → Q = Turing.TM2.Stmt.peek k a q → motive (Turing.TM2.Stmt.peek k a q))
  (h_3 :
    (Q : Turing.TM2.Stmt Γ Λ σ) →
      (k : K) →
        (a : σ → Option (Γ k) → σ) →
          (q : Turing.TM2.Stmt Γ Λ σ) → Q = Turing.TM2.Stmt.pop k a q → motive (Turing.TM2.Stmt.pop k a q))
  (h_4 :
    (Q : Turing.TM2.Stmt Γ Λ σ) →
      (a : σ → σ) → (q : Turing.TM2.Stmt Γ Λ σ) → Q = Turing.TM2.Stmt.load a q → motive (Turing.TM2.Stmt.load a q))
  (h_5 :
    (Q : Turing.TM2.Stmt Γ Λ σ) →
      (a : σ → Bool) →
        (q₁ q₂ : Turing.TM2.Stmt Γ Λ σ) → Q = Turing.TM2.Stmt.branch a q₁ q₂ → motive (Turing.TM2.Stmt.branch a q₁ q₂))
  (h_6 : (Q : Turing.TM2.Stmt Γ Λ σ) → (a : σ → Λ) → Q = Turing.TM2.Stmt.goto a → motive (Turing.TM2.Stmt.goto a))
  (h_7 : (Q : Turing.TM2.Stmt Γ Λ σ) → Q = Turing.TM2.Stmt.halt → motive Turing.TM2.Stmt.halt),
  (match Turing.TM2.Stmt.halt with
    | Q@h:(Turing.TM2.Stmt.push k a q) => h_1 Q k a q h
    | Q@h:(Turing.TM2.Stmt.peek k a q) => h_2 Q k a q h
    | Q@h:(Turing.TM2.Stmt.pop k a q) => h_3 Q k a q h
    | Q@h:(Turing.TM2.Stmt.load a q) => h_4 Q a q h
    | Q@h:(Turing.TM2.Stmt.branch a q₁ q₂) => h_5 Q a q₁ q₂ h
    | Q@h:(Turing.TM2.Stmt.goto a) => h_6 Q a h
    | Q@h:Turing.TM2.Stmt.halt => h_7 Q h) =
    h_7 Turing.TM2.Stmt.halt ⋯
-- Mathlib.Algebra.Ring.Pi
Pi.addMonoidWithOne : {I : Type u} → {f : I → Type v} → [(i : I) → AddMonoidWithOne (f i)] → AddMonoidWithOne ((i : I) → f i)
-- Mathlib.CategoryTheory.Limits.Opposites
CategoryTheory.Limits.instHasFiniteWidePushoutsOppositeOfHasFiniteWidePullbacks : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasFiniteWidePullbacks C],
  CategoryTheory.Limits.HasFiniteWidePushouts Cᵒᵖ
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.mk_preimage_of_injective_lift : ∀ {α : Type u} {β : Type v} (f : α → β) (s : Set β),
  Function.Injective f → Cardinal.lift.{v, u} (Cardinal.mk ↑(f ⁻¹' s)) ≤ Cardinal.lift.{u, v} (Cardinal.mk ↑s)
-- Mathlib.Algebra.Group.Hom.Defs
AddMonoidHom.copy.eq_1 : ∀ {M : Type u_4} {N : Type u_5} [inst : AddZero M] [inst_1 : AddZero N] (f : M →+ N) (f' : M → N) (h : f' = ⇑f),
  f.copy f' h = { toZeroHom := (↑f).copy f' h, map_add' := ⋯ }
-- Mathlib.RingTheory.TensorProduct.Maps
Module.endTensorEndAlgHom_apply : ∀ {R : Type u_1} {S : Type u_2} {A : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommSemiring R]
  [inst_1 : CommSemiring S] [inst_2 : Semiring A] [inst_3 : AddCommMonoid M] [inst_4 : AddCommMonoid N]
  [inst_5 : Algebra R S] [inst_6 : Algebra S A] [inst_7 : Algebra R A] [inst_8 : Module R M] [inst_9 : Module S M]
  [inst_10 : Module A M] [inst_11 : Module R N] [inst_12 : IsScalarTower R A M] [inst_13 : IsScalarTower S A M]
  [inst_14 : IsScalarTower R S M] (f : Module.End A M) (g : Module.End R N),
  Module.endTensorEndAlgHom (f ⊗ₜ[R] g) = TensorProduct.AlgebraTensorModule.map f g