mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Array.MinMax
Array.le_min_iff : ∀ {α : Type u_1} [inst : Min α] [inst_1 : LE α] [Std.LawfulOrderInf α] {xs : Array α} (h : xs ≠ #[]) {x : α},
  x ≤ xs.min h ↔ ∀ b ∈ xs, x ≤ b
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
cfc_eval_X : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : TopologicalSpace A] [inst_6 : Ring A]
  [inst_7 : StarRing A] [inst_8 : Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] (a : A),
  autoParam (p a) cfc_eval_X._auto_1 → cfc (fun x => Polynomial.eval x Polynomial.X) a = a
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.nsmul_mk : ∀ {α : Type u} {L : List (α × Bool)} (n : ℕ), n • FreeAddGroup.mk L = FreeAddGroup.mk (List.replicate n L).flatten
-- Mathlib.Order.GaloisConnection.Defs
/-- A constructive choice function for images of `u`.  -/
GaloisCoinsertion.choice : {α : Type u} →
  {β : Type v} →
    [inst : Preorder α] →
      [inst_1 : Preorder β] → {l : α → β} → {u : β → α} → GaloisCoinsertion l u → (x : β) → x ≤ l (u x) → α
-- Mathlib.Control.Functor
/-- `Functor.Comp` is a wrapper around `Function.Comp` for types.
It prevents Lean's type class resolution mechanism from trying
a `Functor (Comp F id)` when `Functor F` would do.  -/
Functor.Comp : (Type u → Type w) → (Type v → Type u) → Type v → Type w
-- Mathlib.Topology.Order.Hom.Esakia
PseudoEpimorphism.mk.injEq : ∀ {α : Type u_6} {β : Type u_7} [inst : Preorder α] [inst_1 : Preorder β] (toOrderHom : α →o β)
  (exists_map_eq_of_map_le' : ∀ ⦃a : α⦄ ⦃b : β⦄, toOrderHom.toFun a ≤ b → ∃ c, a ≤ c ∧ toOrderHom.toFun c = b)
  (toOrderHom_1 : α →o β)
  (exists_map_eq_of_map_le'_1 : ∀ ⦃a : α⦄ ⦃b : β⦄, toOrderHom_1.toFun a ≤ b → ∃ c, a ≤ c ∧ toOrderHom_1.toFun c = b),
  ({ toOrderHom := toOrderHom, exists_map_eq_of_map_le' := exists_map_eq_of_map_le' } =
      { toOrderHom := toOrderHom_1, exists_map_eq_of_map_le' := exists_map_eq_of_map_le'_1 }) =
    (toOrderHom = toOrderHom_1)
-- Mathlib.RepresentationTheory.Intertwining
Representation.Equiv.mk'.sizeOf_spec : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Semiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : Module A V] [inst_5 : Module A W]
  {ρ : Representation A G V} {σ : Representation A G W} [inst_6 : SizeOf A] [inst_7 : SizeOf G] [inst_8 : SizeOf V]
  [inst_9 : SizeOf W] (toIntertwiningMap : ρ.IntertwiningMap σ) (invFun : W → V)
  (left_inv : autoParam (Function.LeftInverse invFun toIntertwiningMap.toFun) Equiv.left_inv._autoParam)
  (right_inv : autoParam (Function.RightInverse invFun toIntertwiningMap.toFun) Equiv.right_inv._autoParam),
  sizeOf { toIntertwiningMap := toIntertwiningMap, invFun := invFun, left_inv := left_inv, right_inv := right_inv } =
    1 + sizeOf toIntertwiningMap
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.max!_eq_back!_toArray : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.WF → t.max! = t.toArray.back!
-- Init.Data.Int.Linear
Int.not_lt_eq : ∀ (a b : ℤ), (¬a < b) = (b ≤ a)
-- Mathlib.RepresentationTheory.Basic
Representation.inv_self_apply : ∀ {k : Type u_1} {G : Type u_2} {V : Type u_3} [inst : Semiring k] [inst_1 : Group G] [inst_2 : AddCommMonoid V]
  [inst_3 : Module k V] (ρ : Representation k G V) (g : G) (x : V), (ρ g⁻¹) ((ρ g) x) = x
-- Mathlib.Data.Fintype.Card
/-- A `Fintype` with positive cardinality constructively contains an element.
 -/
truncOfCardPos : {α : Type u_4} → [inst : Fintype α] → 0 < Fintype.card α → Trunc α
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.blsub_le_iff : ∀ {o : Ordinal.{u}} {f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}} {a : Ordinal.{max u v}},
  o.blsub f ≤ a ↔ ∀ (i : Ordinal.{u}) (h : i < o), f i h < a
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.ext_get?_iff : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] [inst_1 : Std.LawfulEqCmp cmp]
  {t₁ t₂ : Std.ExtDTreeMap α β cmp}, t₁ = t₂ ↔ ∀ (k : α), t₁.get? k = t₂.get? k
-- Mathlib.Topology.Sheaves.Over
TopologicalSpace.Opens.sheafEquivOver_inverse_map_hom_app : ∀ {X : Type u} [inst : TopologicalSpace X] (U : TopologicalSpace.Opens X) {A : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} A] {X_1 Y : CategoryTheory.Sheaf (Opens.grothendieckTopology ↥U) A}
  (f : X_1 ⟶ Y) (X_2 : (CategoryTheory.Over U)ᵒᵖ),
  (U.sheafEquivOver.inverse.map f).hom.app X_2 =
    f.hom.app (Opposite.op (U.overEquivalence.functor.obj (Opposite.unop X_2)))
-- Mathlib.RingTheory.Coalgebra.Quotient
Coalgebra.Quotient.comul_comp_mkQ : ∀ {R : Type u_1} {C : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup C] [inst_2 : Module R C]
  [inst_3 : CoalgebraStruct R C] (I : Submodule R C) [inst_4 : I.IsCoideal],
  CoalgebraStruct.comul ∘ₗ I.mkQ = TensorProduct.map I.mkQ I.mkQ ∘ₗ CoalgebraStruct.comul
-- Mathlib.CategoryTheory.Sites.Hypercover.IsSheaf
CategoryTheory.GrothendieckTopology.OneHypercoverFamily.exists_oneHypercover : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  (H : J.OneHypercoverFamily) [H.IsGenerating] {X : C}, ∀ S ∈ J X, ∃ E, ∃ (_ : H E), E.sieve₀ ≤ S
-- Mathlib.Algebra.Polynomial.RingDivision
Polynomial.degree_pos_of_aeval_root : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Semiring S] [inst_2 : Algebra R S] {p : Polynomial R},
  p ≠ 0 → ∀ {z : S}, (Polynomial.aeval z) p = 0 → (∀ (x : R), (algebraMap R S) x = 0 → x = 0) → 0 < p.degree
-- Mathlib.Tactic.Determinant.Bird.Meta
/-- Recognise a `birdDet` call and reify it into an evaluator context.  -/
Mathlib.Tactic.Determinant.reifyBirdDet : Lean.Expr → Lean.MetaM Mathlib.Tactic.Determinant.ReifiedBirdDet
-- Mathlib.CategoryTheory.Preadditive.Projective.Basic
/-- An object `P` is called *projective* if every morphism out of `P` factors through every epimorphism.
 -/
CategoryTheory.Projective : {C : Type u} → [CategoryTheory.Category.{v, u} C] → C → Prop
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rcc.forIn'_toArray_eq_forIn' : ∀ {α : Type u} {r : Std.Rcc α} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerableLE α] [inst_4 : Std.Rxc.IsAlwaysFinite α]
  [inst_5 : Std.PRange.LawfulUpwardEnumerable α] {γ : Type u} {init : γ} {m : Type u → Type w} [inst_6 : Monad m]
  [LawfulMonad m] {f : (a : α) → a ∈ r.toArray → γ → m (ForInStep γ)},
  forIn' r.toArray init f = forIn' r init fun a ha acc => f a ⋯ acc
-- Init.Data.Nat.Bitwise.Lemmas
Nat.xor_mod_two_eq_one : ∀ {a b : ℕ}, (a ^^^ b) % 2 = 1 ↔ ¬(a % 2 = 1 ↔ b % 2 = 1)
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Over.homMk_left : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X : T} {U V : CategoryTheory.Over X} (f : U.left ⟶ V.left)
  (w : autoParam (CategoryTheory.CategoryStruct.comp f V.hom = U.hom) CategoryTheory.Over.homMk._auto_1),
  (CategoryTheory.Over.homMk f w).left = f
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
/-- Population count.
 -/
Std.Tactic.BVDecide.BVUnOp.cpop : Std.Tactic.BVDecide.BVUnOp
-- Mathlib.Order.Category.PartOrd
PartOrd.Hom.ext : ∀ {X Y : PartOrd} {x y : X.Hom Y}, x.hom' = y.hom' → x = y
-- Init.Grind.Norm
Lean.Grind.imp_false_eq : ∀ (p : Prop), (p → False) = ¬p
-- Lean.Meta.Basic
Lean.Meta.Context.config : Lean.Meta.Context → Lean.Meta.Config
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.tr.eq_7 : ∀ (q₁ q₂ : Turing.PartrecToTM2.Λ'),
  Turing.PartrecToTM2.tr (q₁.pred q₂) =
    Turing.PartrecToTM2.pop' Turing.PartrecToTM2.K'.main
      (Turing.TM2.Stmt.branch (fun s => decide (s = some Turing.PartrecToTM2.Γ'.bit0))
        (Turing.TM2.Stmt.push Turing.PartrecToTM2.K'.rev (fun x => Turing.PartrecToTM2.Γ'.bit1)
          (Turing.TM2.Stmt.goto fun x => q₁.pred q₂))
        (Turing.TM2.Stmt.branch (fun s => Turing.PartrecToTM2.natEnd (s.getD default))
          (Turing.TM2.Stmt.goto fun x => q₁)
          (Turing.PartrecToTM2.peek' Turing.PartrecToTM2.K'.main
            (Turing.TM2.Stmt.branch (fun s => Turing.PartrecToTM2.natEnd (s.getD default))
              (Turing.TM2.Stmt.goto fun x => Turing.PartrecToTM2.unrev q₂)
              (Turing.TM2.Stmt.push Turing.PartrecToTM2.K'.rev (fun x => Turing.PartrecToTM2.Γ'.bit0)
                (Turing.TM2.Stmt.goto fun x => Turing.PartrecToTM2.unrev q₂))))))
-- Mathlib.Algebra.Regular.ULift
ULift.isAddRightRegular_up : ∀ {R : Type v} [inst : Add R] {a : R}, IsAddRightRegular { down := a } ↔ IsAddRightRegular a
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.vsub_card_le : ∀ {α : Type u_2} {β : Type u_3} [inst : VSub α β] [inst_1 : DecidableEq α] {s t : Finset β},
  (s -ᵥ t).card ≤ s.card * t.card
-- Std.Data.DHashMap.Internal.RawLemmas
_private.Std.Data.DHashMap.Internal.RawLemmas.0.Std.DHashMap.Internal.Raw₀.getKey?.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (a : α) (size : ℕ)
  (buckets : Array (Std.DHashMap.Internal.AssocList α β)) (hm : 0 < { size := size, buckets := buckets }.buckets.size),
  Std.DHashMap.Internal.Raw₀.getKey? ⟨{ size := size, buckets := buckets }, hm⟩ a =
    match Std.DHashMap.Internal.mkIdx buckets.size hm (hash a) with
    | ⟨i, h⟩ => Std.DHashMap.Internal.AssocList.getKey? a buckets[i]
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (K : Type u_2) [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R)
  {x y : IsDedekindDomain.HeightOneSpectrum.adicCompletion K v}, x.toCompletion = y.toCompletion → x = y
-- Mathlib.CategoryTheory.Limits.Comma
/-- Provided that `L` preserves the appropriate colimit, then the cocone in `coconeOfPreserves` is
a colimit.  -/
CategoryTheory.Comma.coconeOfPreservesIsColimit : {J : Type w} →
  [inst : CategoryTheory.Category.{w', w} J] →
    {A : Type u₁} →
      [inst_1 : CategoryTheory.Category.{v₁, u₁} A] →
        {B : Type u₂} →
          [inst_2 : CategoryTheory.Category.{v₂, u₂} B] →
            {T : Type u₃} →
              [inst_3 : CategoryTheory.Category.{v₃, u₃} T] →
                {L : CategoryTheory.Functor A T} →
                  {R : CategoryTheory.Functor B T} →
                    (F : CategoryTheory.Functor J (CategoryTheory.Comma L R)) →
                      [inst_4 : CategoryTheory.Limits.PreservesColimit (F.comp (CategoryTheory.Comma.fst L R)) L] →
                        {c₁ : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.Comma.fst L R))} →
                          (t₁ : CategoryTheory.Limits.IsColimit c₁) →
                            {c₂ : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.Comma.snd L R))} →
                              CategoryTheory.Limits.IsColimit c₂ →
                                CategoryTheory.Limits.IsColimit (CategoryTheory.Comma.coconeOfPreserves F t₁ c₂)
-- Mathlib.Probability.Kernel.Disintegration.StandardBorel
ProbabilityTheory.Kernel.isCondKernelCDF_condKernelCDF : ∀ {α : Type u_1} {γ : Type u_3} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ}
  [inst : MeasurableSpace.CountablyGenerated γ] (κ : ProbabilityTheory.Kernel α (γ × ℝ))
  [inst_1 : ProbabilityTheory.IsFiniteKernel κ], ProbabilityTheory.IsCondKernelCDF κ.condKernelCDF κ κ.fst
-- Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Matrix.det_updateRow_add : ∀ {n : Type u_2} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] (M : Matrix n n R)
  (j : n) (u v : n → R), (M.updateRow j (u + v)).det = (M.updateRow j u).det + (M.updateRow j v).det
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.LitValue.uint8.injEq : ∀ (val val_1 : UInt8), (Lean.Compiler.LCNF.LitValue.uint8 val = Lean.Compiler.LCNF.LitValue.uint8 val_1) = (val = val_1)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.pairFunction_right : ∀ {C : Type u} (X Y : C), CategoryTheory.Limits.pairFunction X Y CategoryTheory.Limits.WalkingPair.right = Y
-- Mathlib.CategoryTheory.Adjunction.FullyFaithful
/-- If the unit of an adjunction is an isomorphism, then one has an isomorphism `L ⋙ R ⋙ L ≅ L`.  -/
CategoryTheory.Adjunction.whiskerLeftLCounitIsoOfIsIsoUnit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {L : CategoryTheory.Functor C D} →
          {R : CategoryTheory.Functor D C} → (h : L ⊣ R) → [CategoryTheory.IsIso h.unit] → L.comp (R.comp L) ≅ L
-- Mathlib.LinearAlgebra.TensorProduct.Map
LinearEquiv.rTensor_tmul : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} [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 : N ≃ₗ[R] P) (m : M) (n : N), (LinearEquiv.rTensor M f) (n ⊗ₜ[R] m) = f n ⊗ₜ[R] m
-- Mathlib.Algebra.Order.GroupWithZero.Basic
/-- See `lt_inv_mul_iff₀` for a version with multiplication on the other side.  -/
lt_inv_mul_iff₀' : ∀ {G₀ : Type u_3} [inst : CommGroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] {a b c : G₀},
  0 < c → (a < c⁻¹ * b ↔ a * c < b)
-- Mathlib.Algebra.Group.End
MulAut.eq_1 : ∀ (M : Type u_7) [inst : Mul M], MulAut M = (M ≃* M)
-- Mathlib.Combinatorics.Young.YoungDiagram
YoungDiagram.mem_row_iff : ∀ {μ : YoungDiagram} {i : ℕ} {c : ℕ × ℕ}, c ∈ μ.row i ↔ c ∈ μ ∧ c.1 = i
-- Mathlib.Order.UpperLower.Relative
IsRelLowerSet.iUnion : ∀ {α : Type u_1} {ι : Sort u_2} {P : α → Prop} [inst : LE α] {f : ι → Set α},
  (∀ (i : ι), IsRelLowerSet (f i) P) → IsRelLowerSet (⋃ i, f i) P
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat.0.Nat.mkLENat : Lean.Expr → Lean.Expr → Lean.Expr
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
IsFreeAddGroup.lift_symm_apply : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : IsFreeAddGroup G] {H : Type u_2} [inst_2 : AddGroup H] (f : G →+ H)
  (a : IsFreeAddGroup.Generators G), IsFreeAddGroup.lift.symm f a = f (IsFreeAddGroup.of a)
-- Mathlib.AlgebraicGeometry.Sites.Proetale
AlgebraicGeometry.Scheme.ProEt.bot_mem_topology : ∀ {S : AlgebraicGeometry.Scheme} (X : S.ProEt) [IsEmpty ↥X.left], ⊥ ∈ (AlgebraicGeometry.Scheme.ProEt.topology S) X
-- Mathlib.RingTheory.Derivation.Basic
Derivation.hasCoeToLinearMap : {R : Type u_1} →
  {A : Type u_2} →
    {M : Type u_4} →
      [inst : CommSemiring R] →
        [inst_1 : CommSemiring A] →
          [inst_2 : AddCommMonoid M] →
            [inst_3 : Algebra R A] → [inst_4 : Module A M] → [inst_5 : Module R M] → Coe (Derivation R A M) (A →ₗ[R] M)
-- Init.Data.BEq
/-- Symmetry for `BEq`. If `a == b` then `b == a`.  -/
PartialEquivBEq.symm : ∀ {α : Type u_1} {inst : BEq α} [self : PartialEquivBEq α] {a b : α}, (a == b) = true → (b == a) = true
-- Mathlib.Condensed.Discrete.Colimit
Condensed.lanPresheafExt_inv : ∀ {F G : CategoryTheory.Functor Profiniteᵒᵖ (Type (u + 1))} (S : Profiniteᵒᵖ)
  (i : FintypeCat.toProfinite.op.comp F ≅ FintypeCat.toProfinite.op.comp G),
  (Condensed.lanPresheafExt i).inv.app S =
    CategoryTheory.Limits.colimMap
      ((CategoryTheory.CostructuredArrow.proj FintypeCat.toProfinite.op S).whiskerLeft i.inv)
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
tangentMapWithin_univ : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'},
  tangentMapWithin I I' f Set.univ = tangentMap I I' f
-- Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
CategoryTheory.Limits.IsLimit.isIso_π_app_of_isInitial : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [inst_1 : CategoryTheory.Category.{v, u} J]
  {F : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cone F} (hc : CategoryTheory.Limits.IsLimit c) (X : J)
  (hX : CategoryTheory.Limits.IsInitial X), CategoryTheory.IsIso (c.π.app X)
-- Mathlib.Algebra.Group.Subgroup.Lattice
AddSubgroup.mem_iSup_of_mem : ∀ {G : Type u_1} [inst : AddGroup G] {ι : Sort u_2} {S : ι → AddSubgroup G} (i : ι) {x : G}, x ∈ S i → x ∈ iSup S
-- Mathlib.RingTheory.TensorProduct.Basic
Algebra.TensorProduct.ext_ring_iff : ∀ {R : Type u_4} {S : Type u_5} {A : Type u_6} {B : Type u_7} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : Semiring A] [inst_3 : Semiring B] [inst_4 : Algebra R A] [inst_5 : Algebra S B] [inst_6 : Algebra R S]
  [inst_7 : Algebra R B] [inst_8 : IsScalarTower R S B] {f g : TensorProduct R S A →ₐ[S] B},
  f = g ↔
    (AlgHom.restrictScalars R f).comp Algebra.TensorProduct.includeRight =
      (AlgHom.restrictScalars R g).comp Algebra.TensorProduct.includeRight
-- Mathlib.Order.Category.CompleteLat
CompleteLat.of.injEq : ∀ (carrier : Type u_1) [str : CompleteLattice carrier] (carrier_1 : Type u_1) (str_1 : CompleteLattice carrier_1),
  ({ carrier := carrier, str := str } = { carrier := carrier_1, str := str_1 }) = (carrier = carrier_1 ∧ str ≍ str_1)
-- Mathlib.Algebra.Category.ModuleCat.Kernels
/-- The categorical kernel of a morphism in `ModuleCat`
agrees with the usual module-theoretical kernel.
 -/
ModuleCat.kernelIsoKer : {R : Type u} →
  [inst : Ring R] →
    {G H : ModuleCat R} → (f : G ⟶ H) → CategoryTheory.Limits.kernel f ≅ ModuleCat.of R ↥(ModuleCat.Hom.hom f).ker
-- Mathlib.LinearAlgebra.TensorProduct.Pi
TensorProduct.piScalarRightInv.eq_1 : ∀ (R : Type u_1) [inst : CommSemiring R] (S : Type u_2) [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (N : Type u_3)
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] [inst_5 : Module S N] [inst_6 : IsScalarTower R S N] (ι : Type u_4)
  [inst_7 : Fintype ι] [inst_8 : DecidableEq ι],
  TensorProduct.piScalarRightInv R S N ι =
    (LinearMap.lsum S (fun x => N) S) fun i =>
      { toFun := fun n => n ⊗ₜ[R] Pi.single i 1, map_add' := ⋯, map_smul' := ⋯ }
-- Mathlib.Algebra.Order.Group.Synonym
toColex_mul : ∀ {α : Type u_1} [inst : Mul α] (a b : α), toColex (a * b) = toColex a * toColex b
-- Mathlib.Topology.Order.LeftRightLim
tendsto_leftLim_atTop_of_tendsto : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace β] [inst_2 : TopologicalSpace α]
  [OrderTopology α] [NoTopOrder α] [T3Space β] {f : α → β} {b : β},
  Filter.Tendsto f Filter.atTop (nhds b) → Filter.Tendsto (Function.leftLim f) Filter.atTop (nhds b)
-- Mathlib.Order.Sublattice
SupHom.mk.congr_simp : ∀ {α : Type u_6} {β : Type u_7} [inst : Max α] [inst_1 : Max β] (toFun toFun_1 : α → β) (e_toFun : toFun = toFun_1)
  (map_sup' : ∀ (a b : α), toFun (a ⊔ b) = toFun a ⊔ toFun b),
  { toFun := toFun, map_sup' := map_sup' } = { toFun := toFun_1, map_sup' := ⋯ }
-- Mathlib.Topology.Semicontinuity.Defs
LowerHemicontinuousWithinAt.mono : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → Set β} {x : α}
  {s t : Set α}, LowerHemicontinuousWithinAt f s x → t ⊆ s → LowerHemicontinuousWithinAt f t x
-- Mathlib.Topology.Algebra.UniformConvergence
UniformOnFun.ofFun_add : ∀ {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [inst : Add β] (f g : α → β),
  (UniformOnFun.ofFun 𝔖) (f + g) = (UniformOnFun.ofFun 𝔖) f + (UniformOnFun.ofFun 𝔖) g
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
contravariant_le_iff_contravariant_lt_and_eq : ∀ (M : Type u_1) (N : Type u_2) (μ : M → N → N) [inst : PartialOrder N],
  (Contravariant M N μ fun x1 x2 => x1 ≤ x2) ↔
    (Contravariant M N μ fun x1 x2 => x1 < x2) ∧ Contravariant M N μ fun x1 x2 => x1 = x2
-- Mathlib.RingTheory.FractionalIdeal.Basic
FractionalIdeal.eq_zero_iff : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  {I : FractionalIdeal S P}, I = 0 ↔ ∀ x ∈ I, x = 0
-- Mathlib.Algebra.Lie.Weights.RootSystem
LieAlgebra.IsKilling.chainLength_of_eq_zsmul_add : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : CharZero K] [inst_2 : LieRing L] [inst_3 : LieAlgebra K L]
  [inst_4 : LieAlgebra.IsKilling K L] [inst_5 : FiniteDimensional K L] {H : LieSubalgebra K L}
  [inst_6 : H.IsCartanSubalgebra] [inst_7 : LieModule.IsTriangularizable K (↥H) L] (α β β' : LieModule.Weight K (↥H) L)
  (n : ℤ), ⇑β' = n • ⇑α + ⇑β → LieAlgebra.IsKilling.chainLength α β' = LieAlgebra.IsKilling.chainLength α β
-- Mathlib.Analysis.Convex.Function
/-- A linear map is convex.  -/
LinearMap.convexOn : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommMonoid β] [inst_4 : PartialOrder β] [inst_5 : Module 𝕜 E] [inst_6 : Module 𝕜 β] (f : E →ₗ[𝕜] β)
  {s : Set E}, Convex 𝕜 s → ConvexOn 𝕜 s ⇑f
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.unitors_inv_equal : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a : B},
  (CategoryTheory.Bicategory.leftUnitor (CategoryTheory.CategoryStruct.id a)).inv =
    (CategoryTheory.Bicategory.rightUnitor (CategoryTheory.CategoryStruct.id a)).inv
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddSubsemigroup.comap_iInf : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] {ι : Sort u_5} (f : M →ₙ+ N)
  (s : ι → AddSubsemigroup N), AddSubsemigroup.comap f (iInf s) = ⨅ i, AddSubsemigroup.comap f (s i)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.get!_inter_of_not_mem_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited β], t₁.WF → t₂.WF → ∀ {k : α}, k ∉ t₁ → (t₁ ∩ t₂).get! k = default
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
/-- The type of morphisms in the category `CostructuredArrow`.  -/
CategoryTheory.CostructuredArrow.Hom : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {S : CategoryTheory.Functor C D} →
          {T : D} → CategoryTheory.CostructuredArrow S T → CategoryTheory.CostructuredArrow S T → Type (max v₁ 0)
-- Mathlib.NumberTheory.Harmonic.EulerMascheroni
/-- Lower bound for `γ`. (The true value is about 0.57.)  -/
Real.one_half_lt_eulerMascheroniConstant : 1 / 2 < Real.eulerMascheroniConstant
-- Mathlib.Order.CompleteLattice.Basic
iInf₂_eq_bot : ∀ {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_6} [inst : CompleteLinearOrder α] (f : (i : ι) → κ i → α),
  ⨅ i, ⨅ j, f i j = ⊥ ↔ ∀ (b : α), ⊥ < b → ∃ i j, f i j < b
-- Mathlib.Algebra.Module.FinitePresentation
instFiniteOfFinitePresentation : ∀ (R : Type u_1) (M : Type u_2) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [h : Module.FinitePresentation R M], Module.Finite R M
-- Mathlib.Logic.Encodable.Basic
Encodable.decode₂_inj : ∀ {α : Type u_1} [inst : Encodable α] {n : ℕ} {a₁ a₂ : α},
  a₁ ∈ Encodable.decode₂ α n → a₂ ∈ Encodable.decode₂ α n → a₁ = a₂
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.toCategoryStruct : {B : Type u} → [self : CategoryTheory.Bicategory B] → CategoryTheory.CategoryStruct.{v, u} B
-- Std.Sync.Channel
/-- Send a value through the channel, blocking until the transmission could be completed. Note that this
function may throw an error when trying to send to an already closed channel.
 -/
Std.CloseableChannel.Sync.send : {α : Type} → Std.CloseableChannel.Sync α → α → EIO Std.CloseableChannel.Error Unit
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.setIntegral_nonneg_ae : ∀ {X : Type u_1} {mX : MeasurableSpace X} {μ : MeasureTheory.Measure X} {f : X → ℝ} {s : Set X},
  MeasurableSet s → (∀ᵐ (x : X) ∂μ, x ∈ s → 0 ≤ f x) → 0 ≤ ∫ (x : X) in s, f x ∂μ