mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.LocallyConvex.Bounded
/-- Given any sequence `ε` of scalars which tends to `𝓝[≠] 0`, we have that a set `S` is bounded
if and only if for any sequence `x : ℕ → S`, `ε • x` tends to 0. This actually works for any
indexing type `ι`, but in the special case `ι = ℕ` we get the important fact that convergent
sequences fully characterize bounded sets.  -/
Bornology.isVonNBounded_iff_smul_tendsto_zero : ∀ {𝕜 : Type u_1} {E : Type u_3} {ι : Type u_5} [inst : NontriviallyNormedField 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : Module 𝕜 E] [inst_3 : TopologicalSpace E] [ContinuousSMul 𝕜 E] {ε : ι → 𝕜} {l : Filter ι} [l.NeBot],
  Filter.Tendsto ε l (nhdsWithin 0 {0}ᶜ) →
    ∀ {S : Set E}, Bornology.IsVonNBounded 𝕜 S ↔ ∀ (x : ι → E), (∀ (n : ι), x n ∈ S) → Filter.Tendsto (ε • x) l (nhds 0)
-- Lean.Data.Json.Basic
Lean.Json.num.injEq : ∀ (n n_1 : Lean.JsonNumber), (Lean.Json.num n = Lean.Json.num n_1) = (n = n_1)
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
Tactic.ComputeAsymptotics.UnitMonomial.toFun.eq_1 : ∀ (m : Tactic.ComputeAsymptotics.UnitMonomial) (basis : Tactic.ComputeAsymptotics.Basis) (x : ℝ),
  m.toFun basis x = (List.zipWith (fun exp b => b x ^ exp) m basis).prod
-- Mathlib.CategoryTheory.Triangulated.Functor
CategoryTheory.Functor.mapTriangleIso_inv_app_hom₁ : ∀ {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] [inst_2 : CategoryTheory.HasShift C ℤ]
  [inst_3 : CategoryTheory.HasShift D ℤ] {F₁ F₂ : CategoryTheory.Functor C D} (e : F₁ ≅ F₂) [inst_4 : F₁.CommShift ℤ]
  [inst_5 : F₂.CommShift ℤ] [inst_6 : CategoryTheory.NatTrans.CommShift e.hom ℤ]
  (X : CategoryTheory.Pretriangulated.Triangle C),
  ((CategoryTheory.Functor.mapTriangleIso e).inv.app X).hom₁ = e.inv.app X.obj₁
-- Mathlib.Algebra.Order.Field.Basic
div_nat_le_self_of_nonnneg : ∀ {α : Type u_2} [inst : Semifield α] [inst_1 : PartialOrder α] [PosMulReflectLT α] {a : α} [IsStrictOrderedRing α],
  0 ≤ a → ∀ (n : ℕ), a / ↑n ≤ a
-- Mathlib.LinearAlgebra.Basis.Defs
Module.Basis.coord_apply : ∀ {ι : Type u_10} {R : Type u_11} {M : Type u_12} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (b : Module.Basis ι R M) (i : ι) (x : M), (b.coord i) x = (b.repr x) i
-- Mathlib.RingTheory.NonUnitalSubring.Basic
NonUnitalSubring.closure_preimage_le : ∀ {F : Type w} {R : Type u} {S : Type v} [inst : NonUnitalNonAssocRing R] [inst_1 : NonUnitalNonAssocRing S]
  [inst_2 : FunLike F R S] [inst_3 : NonUnitalRingHomClass F R S] (f : F) (s : Set S),
  NonUnitalSubring.closure (⇑f ⁻¹' s) ≤ NonUnitalSubring.comap f (NonUnitalSubring.closure s)
-- Mathlib.Topology.PartitionOfUnity
BumpCovering.instFunLikeContinuousMapReal : {ι : Type u} → {X : Type v} → [inst : TopologicalSpace X] → {s : Set X} → FunLike (BumpCovering ι X s) ι C(X, ℝ)
-- Mathlib.CategoryTheory.Limits.FinallySmall
CategoryTheory.finallySmall_of_final_of_essentiallySmall : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {K : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} K]
  [CategoryTheory.EssentiallySmall.{w, v₁, u₁} K] (F : CategoryTheory.Functor K J) [F.Final],
  CategoryTheory.FinallySmall J
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.lift_add_one : ∀ (a : Ordinal.{v}), Ordinal.lift.{u, v} (a + 1) = Ordinal.lift.{u, v} a + 1
-- Mathlib.RingTheory.AdicCompletion.Topology
Submodule.instSMul.congr_simp : ∀ {R : Type u} [inst : Semiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Module R A] {M : Type u_1}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module A M] [inst_6 : IsScalarTower R A M],
  Submodule.instSMul = Submodule.instSMul
-- Mathlib.Algebra.Order.Group.MinMax
max_one_div_max_inv_one_eq_self : ∀ {α : Type u_1} [inst : Group α] [inst_1 : LinearOrder α] [MulLeftMono α] (a : α), max a 1 / max a⁻¹ 1 = a
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Cell.Const.alter.congr_simp : ∀ {α : Type u} {β : Type v} [inst : Ord α] [inst_1 : Std.OrientedOrd α] {k : α} (f f_1 : Option β → Option β),
  f = f_1 →
    ∀ (c c_1 : Std.DTreeMap.Internal.Cell α (fun x => β) (compare k)),
      c = c_1 → Std.DTreeMap.Internal.Cell.Const.alter f c = Std.DTreeMap.Internal.Cell.Const.alter f_1 c_1
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
/-- **Alias** of `MeasureTheory.StronglyMeasurable.fun_const_smul`.

---

Eta-expanded form of `MeasureTheory.StronglyMeasurable.const_smul` -/
MeasureTheory.StronglyMeasurable.const_smul' : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {mα : MeasurableSpace α} [inst : TopologicalSpace β] {𝕜 : Type u_5}
  [inst_1 : SMul 𝕜 β] [ContinuousConstSMul 𝕜 β],
  MeasureTheory.StronglyMeasurable f → ∀ (c : 𝕜), MeasureTheory.StronglyMeasurable fun i => c • f i
-- Init.Data.UInt.Lemmas
UInt16.toUInt8_toUSize : ∀ (n : UInt16), n.toUSize.toUInt8 = n.toUInt8
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.map_add_self : ∀ {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] (Q : QuadraticMap R M N) (x : M), Q (x + x) = 4 • Q x
-- Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
FreeAddGroup.IsCyclicallyReduced.nil : ∀ {α : Type u}, FreeAddGroup.IsCyclicallyReduced []
-- Mathlib.GroupTheory.Perm.Cycle.Factors
/-- If a permutation commutes with every cycle of `g`, then it commutes with `g`

NB. The converse is false. Commuting with every cycle of `g` means that we belong
to the kernel of the action of `Equiv.Perm α` on `g.cycleFactorsFinset`  -/
Equiv.Perm.commute_of_mem_cycleFactorsFinset_commute : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Fintype α] (k g : Equiv.Perm α),
  (∀ c ∈ g.cycleFactorsFinset, Commute k c) → Commute k g
-- Batteries.Data.Nat.Lemmas
Nat.ofBits_lt_two_pow : ∀ {n : ℕ} (f : Fin n → Bool), Nat.ofBits f < 2 ^ n
-- Mathlib.Data.Fin.SuccPred
Fin.predAbove_castSucc_self : ∀ {n : ℕ} (p : Fin n), p.predAbove p.castSucc = p
-- Mathlib.Data.Int.Bitwise
Int.bodd.eq_1 : ∀ (n : ℕ), (Int.ofNat n).bodd = n.bodd
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.map_lt_add_translationNumber_add_one : ∀ (f : CircleDeg1Lift) (x : ℝ), f x < x + f.translationNumber + 1
-- Mathlib.Order.Completion
/-- `DedekindCut.principal` as an `OrderEmbedding`.  -/
DedekindCut.principalEmbedding : {α : Type u_1} → [inst : PartialOrder α] → α ↪o DedekindCut α
-- Mathlib.Topology.Order.Category.FrameAdjunction
Locale.openOfElementHom_toFun : ∀ (L : Type u_1) [inst : CompleteLattice L] (u : L), (Locale.openOfElementHom L) u = {x | x u}
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Functor.instLaxMonoidalMonMapAddMon : {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) →
              [inst_4 : CategoryTheory.BraidedCategory C] →
                [inst_5 : CategoryTheory.BraidedCategory D] → [inst_6 : F.LaxBraided] → F.mapAddMon.LaxMonoidal
-- Mathlib.Analysis.Calculus.ContDiff.Comp
ContDiffAt.clm_apply : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {x : E} {n : WithTop ℕ∞} {f : E → F →L[𝕜] G} {g : E → F},
  ContDiffAt 𝕜 n f x → ContDiffAt 𝕜 n g x → ContDiffAt 𝕜 n (fun x => (f x) (g x)) x
-- Init.Data.Array.Bootstrap
_private.Init.Data.Array.Bootstrap.0.Array.forIn'.loop.match_3.splitter : {α : Type u_1} →
  (as : Array α) →
    (motive : (i : ℕ) → i ≤ as.size → Sort u_2) →
      (i : ℕ) →
        (h : i ≤ as.size) →
          ((x : 0 ≤ as.size) → motive 0 x) → ((i : ℕ) → (h : i + 1 ≤ as.size) → motive i.succ h) → motive i h
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.IterM.forIn_filterM : ∀ {α : Type u₁} {n : Type u₁ → Type u_1} {o : Type u₁ → Type u_2} {γ : Type u₁} {m : Type u₁ → Type u_3} {β : Type u₁}
  {ps : Std.Do.PostShape} [inst : Monad m] [LawfulMonad m] [inst_2 : Monad n] [LawfulMonad n] [inst_4 : Monad o]
  [LawfulMonad o] [inst_6 : Std.Do.WPMonad o ps] [inst_7 : MonadAttach n] [WeaklyLawfulMonadAttach n]
  [inst_9 : MonadLiftT m n] [LawfulMonadLiftT m n] [inst_11 : MonadLiftT n o] [LawfulMonadLiftT n o]
  [inst_13 : Std.Iterator α m β] [Std.Iterators.Finite α m] [inst_15 : Std.IteratorLoop α m o]
  [Std.LawfulIteratorLoop α m o] {it : Std.IterM m β} {f : β → n (ULift.{u₁, 0} Bool)} {init : γ}
  {g : β → γ → o (ForInStep γ)} {P : Std.Do.Assertion ps} {Q : Std.Do.PostCond γ ps},
  ⦃P⦄
      forIn it init fun out acc => do
        let __do_lift ← liftM (f out)
        if __do_lift.down = true then g out acc else pure (ForInStep.yield acc) ⦃Q⦄ →
    ⦃P⦄ forIn (Std.IterM.filterM f it) init g ⦃Q⦄
-- Init.Data.Nat.Coprime
Nat.Coprime.coprime_mul_left_right : ∀ {m k n : ℕ}, m.Coprime (k * n) → m.Coprime n
-- Mathlib.Tactic.MkIffOfInductiveProp
/-- Implementation for both `mk_iff` and `mk_iff_of_inductive_prop`.
 -/
Mathlib.Tactic.MkIff.mkIffOfInductivePropImpl : Lean.Name → Lean.Name → Lean.Syntax → Lean.MetaM Unit
-- Lean.Environment
Lean.instGetElemArrayModuleIdxLtNatToNatSize : {α : Type u_1} → GetElem (Array α) Lean.ModuleIdx α fun a i => i.toNat < a.size
-- Mathlib.Analysis.SpecialFunctions.Complex.Log
Complex.countable_preimage_exp : ∀ {s : Set ℂ}, (Complex.exp ⁻¹' s).Countable ↔ s.Countable
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.get_filter : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α]
  {f : (a : α) → β a → Bool} {k : α} {h' : k ∈ Std.DHashMap.filter f m}, (Std.DHashMap.filter f m).get k h' = m.get k ⋯
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithInitial.mapId_hom_app : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] (X : CategoryTheory.WithInitial C),
  (CategoryTheory.WithInitial.mapId C).hom.app X =
    (match X with
      | CategoryTheory.WithInitial.of a => CategoryTheory.Iso.refl (CategoryTheory.WithInitial.of a)
      | CategoryTheory.WithInitial.star => CategoryTheory.Iso.refl CategoryTheory.WithInitial.star).hom
-- Mathlib.Order.CompactlyGenerated.Basic
WellFoundedGT.finite_ne_bot_of_iSupIndep : ∀ {α : Type u_2} [inst : CompleteLattice α] [WellFoundedGT α] {ι : Type u_3} {t : ι → α},
  iSupIndep t → {i | t i ≠ ⊥}.Finite
-- Mathlib.Order.Filter.Extr
/-- `IsMaxOn f s a` means that `f x ≤ f a` for all `x ∈ s`. Note that we do not assume `a ∈ s`.  -/
IsMaxOn : {α : Type u} → {β : Type v} → [Preorder β] → (α → β) → Set α → α → Prop
-- Mathlib.Data.Rat.Cast.Order
Rat.cast_lt_natCast : ∀ {K : Type u_5} [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] {m : ℚ} {n : ℕ}, ↑m < ↑n ↔ m < ↑n
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
/-- An induction principle for closure membership. If `p` holds for `0`, `1`, and all elements
of `s`, and is preserved under addition and multiplication, then `p` holds for all elements
of the closure of `s`.  -/
NonUnitalSubsemiring.closure_induction : ∀ {R : Type u} [inst : NonUnitalNonAssocSemiring R] {s : Set R}
  {p : (x : R) → x ∈ NonUnitalSubsemiring.closure s → Prop},
  (∀ (x : R) (hx : x ∈ s), p x ⋯) →
    p 0 ⋯ →
      (∀ (x y : R) (hx : x ∈ NonUnitalSubsemiring.closure s) (hy : y ∈ NonUnitalSubsemiring.closure s),
          p x hx → p y hy → p (x + y) ⋯) →
        (∀ (x y : R) (hx : x ∈ NonUnitalSubsemiring.closure s) (hy : y ∈ NonUnitalSubsemiring.closure s),
            p x hx → p y hy → p (x * y) ⋯) →
          ∀ {x : R} (hx : x ∈ NonUnitalSubsemiring.closure s), p x hx
-- Std.Sat.AIG.Basic
Std.Sat.AIG.Fanin.gate_flip : ∀ {v : Bool} (f : Std.Sat.AIG.Fanin), (f.flip v).gate = f.gate
-- Mathlib.Algebra.BigOperators.Group.List.Basic
map_list_sum : ∀ {M : Type u_4} {N : Type u_5} [inst : AddMonoid M] [inst_1 : AddMonoid N] {F : Type u_8} [inst_2 : FunLike F M N]
  [AddMonoidHomClass F M N] (f : F) (l : List M), f l.sum = (List.map (⇑f) l).sum
-- Mathlib.Algebra.Category.Grp.Limits
/-- The forgetful functor from additive commutative groups to types preserves all limits.
(That is, the underlying types could have been computed instead as limits in the category of
types.)  -/
AddCommGrpCat.forget_preservesLimitsOfSize : CategoryTheory.Limits.PreservesLimitsOfSize.{w, v, u, u, u + 1, u + 1} (CategoryTheory.forget AddCommGrpCat)
-- Mathlib.MeasureTheory.VectorMeasure.Integral
/-- The special case of the pairing integral in a set where the pairing is just the flip of the
scalar multiplication by `ℝ` on `F` and `f` is `F`-valued and `μ` is a signed measure.
The resulting integral is `F`-valued. -/
MeasureTheory.VectorMeasure.«term∫ᵛ_In_,_∂<•_» : Lean.ParserDescr
-- Mathlib.NumberTheory.PythagoreanTriples
PythagoreanTriple.even_odd_of_coprime : ∀ {x y z : ℤ}, PythagoreanTriple x y z → x.gcd y = 1 → x % 2 = 0 ∧ y % 2 = 1 ∨ x % 2 = 1 ∧ y % 2 = 0
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.insertManyIfNewUnit_list_singleton : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α Unit},
  m.WF → ∀ {k : α}, m.insertManyIfNewUnit [k] = m.insertIfNew k ()
-- Mathlib.Algebra.Group.TypeTags.Basic
isRegular_toMul : ∀ {α : Type u} [inst : Monoid α] {a : Additive α}, IsRegular (Additive.toMul a) ↔ IsAddRegular a
-- Init.Data.Nat.Bitwise.Basic
Nat.instXorOp : XorOp ℕ
-- Mathlib.Dynamics.BirkhoffSum.NormedSpace
/-- If `f : X → X` is a non-strictly contracting map (i.e., it is Lipschitz with constant `1`),
`g : X → E` is a uniformly continuous, and `l : X → E` is a continuous function,
then the set of points `x`
such that the Birkhoff average of `g` along the orbit of `x` tends to `l x`
is a closed set.  -/
isClosed_setOfPred_tendsto_birkhoffAverage : ∀ (𝕜 : Type u_1) {X : Type u_2} {E : Type u_3} [inst : PseudoEMetricSpace X] [inst_1 : RCLike 𝕜]
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {f : X → X} {g l : X → E},
  LipschitzWith 1 f →
    UniformContinuous g →
      Continuous l → IsClosed {x | Filter.Tendsto (fun x_1 => birkhoffAverage 𝕜 f g x_1 x) Filter.atTop (nhds (l x))}
-- Lean.PrettyPrinter.Delaborator.SubExpr
Lean.PrettyPrinter.Delaborator.SubExpr.HoleIterator.toPos : Lean.PrettyPrinter.Delaborator.SubExpr.HoleIterator → Lean.SubExpr.Pos
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
NumberField.mixedEmbedding.minkowskiBound_pos : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K]
  (I : (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K)ˣ),
  0 < NumberField.mixedEmbedding.minkowskiBound K I
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.ofChosenFiniteProducts.pentagon : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (ℬ : (X Y : C) → CategoryTheory.Limits.LimitCone (CategoryTheory.Limits.pair X Y)) (W X Y Z : C),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CartesianMonoidalCategory.ofChosenFiniteProducts.tensorHom ℬ
        (CategoryTheory.Limits.BinaryFan.associatorOfLimitCone ℬ W X Y).hom (CategoryTheory.CategoryStruct.id Z))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.BinaryFan.associatorOfLimitCone ℬ W
            (CategoryTheory.CartesianMonoidalCategory.ofChosenFiniteProducts.tensorObj ℬ X Y) Z).hom
        (CategoryTheory.CartesianMonoidalCategory.ofChosenFiniteProducts.tensorHom ℬ
          (CategoryTheory.CategoryStruct.id W) (CategoryTheory.Limits.BinaryFan.associatorOfLimitCone ℬ X Y Z).hom)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.BinaryFan.associatorOfLimitCone ℬ
          (CategoryTheory.CartesianMonoidalCategory.ofChosenFiniteProducts.tensorObj ℬ W X) Y Z).hom
      (CategoryTheory.Limits.BinaryFan.associatorOfLimitCone ℬ W X
          (CategoryTheory.CartesianMonoidalCategory.ofChosenFiniteProducts.tensorObj ℬ Y Z)).hom
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.Scheme.Pullback.hasPullback_of_cover : ∀ {X Y Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z)
  [∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g],
  CategoryTheory.Limits.HasPullback f g
-- Mathlib.CategoryTheory.CommSq
CategoryTheory.CommSq.fac_left_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {A B X Y : C} {f : A ⟶ X} {i : A ⟶ B} {p : X ⟶ Y}
  {g : B ⟶ Y} (sq : CategoryTheory.CommSq f i p g) [hsq : sq.HasLift] {Z : C} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp i (CategoryTheory.CategoryStruct.comp sq.lift h) =
    CategoryTheory.CategoryStruct.comp f h
-- Mathlib.RingTheory.Unramified.Basic
Algebra.TensorProduct.algHomOfLinearMapTensorProduct.congr_simp : ∀ {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} {C : Type uC} [inst : CommSemiring R]
  [inst_1 : CommSemiring S] [inst_2 : Algebra R S] [inst_3 : Semiring A] [inst_4 : Algebra R A] [inst_5 : Algebra S A]
  [inst_6 : IsScalarTower R S A] [inst_7 : Semiring B] [inst_8 : Algebra R B] [inst_9 : Semiring C]
  [inst_10 : Algebra S C] (f f_1 : TensorProduct R A B →ₗ[S] C) (e_f : f = f_1)
  (h_mul : ∀ (a₁ a₂ : A) (b₁ b₂ : B), f ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)) = f (a₁ ⊗ₜ[R] b₁) * f (a₂ ⊗ₜ[R] b₂))
  (h_one : f (1 ⊗ₜ[R] 1) = 1),
  Algebra.TensorProduct.algHomOfLinearMapTensorProduct f h_mul h_one =
    Algebra.TensorProduct.algHomOfLinearMapTensorProduct f_1 ⋯ ⋯
-- Init.Data.SInt.Basic
/-- Subtracts one 64-bit signed integer from another, wrapping around on over- or underflow. Usually
accessed via the `-` operator.

This function is overridden at runtime with an efficient implementation.
 -/
Int64.sub : Int64 → Int64 → Int64
-- Mathlib.Data.Stream.Init
Stream'.getElem?_take : ∀ {α : Type u} {s : Stream' α} {k n : ℕ}, k < n → (Stream'.take n s)[k]? = some (s.get k)
-- Mathlib.CategoryTheory.MorphismProperty.Representable
/-- The pullback `(A₁ ×_X A₂) ×_{A₁} (A₁ ×_X A₃)`.  -/
CategoryTheory.Functor.relativelyRepresentable.pullback₃ : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F : CategoryTheory.Functor C D} →
          [inst_2 : F.Full] →
            {A₁ A₂ A₃ : C} →
              {X : D} →
                {f₁ : F.obj A₁ ⟶ X} →
                  (hf₁ : F.relativelyRepresentable f₁) →
                    (f₂ : F.obj A₂ ⟶ X) →
                      (f₃ : F.obj A₃ ⟶ X) → [CategoryTheory.Limits.HasPullback (hf₁.fst' f₂) (hf₁.fst' f₃)] → C
-- Mathlib.Analysis.Matrix.Spectrum
/-- A nonzero Hermitian matrix has an eigenvector with nonzero eigenvalue.  -/
Matrix.IsHermitian.exists_eigenvector_of_ne_zero : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {n : Type u_2} [inst_1 : Fintype n] {A : Matrix n n 𝕜},
  A.IsHermitian → A ≠ 0 → ∃ v t, t ≠ 0 ∧ v ≠ 0 ∧ A.mulVec v = t • v
-- Mathlib.AlgebraicTopology.SimplicialObject.Split
CategoryTheory.SimplicialObject.Split.forget_obj : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] (S : CategoryTheory.SimplicialObject.Split C),
  (CategoryTheory.SimplicialObject.Split.forget C).obj S = S.X
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
le_ciInf_iff' : ∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompleteLinearOrderBot α] [Nonempty ι] {f : ι → α} {a : α},
  a ≤ iInf f ↔ ∀ (i : ι), a ≤ f i
-- Batteries.Data.List.Basic
List.zipWithLeft_eq_zipWithLeftTR : @List.zipWithLeft = @List.zipWithLeftTR
-- Lean.Parser.Command
Lean.Parser.Command.private : Lean.Parser.Parser
-- Init.Data.Range.Polymorphic.SInt
ISize.instRxcHasSize : Std.Rxc.HasSize ISize
-- Init.MetaTypes
/-- Unfolds all constants, even those tagged as `@[irreducible]`.  -/
Lean.Meta.TransparencyMode.all : Lean.Meta.TransparencyMode
-- Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic
Subring.isLocalRing_of_unit : ∀ {R : Type u_1} [inst : Ring R] [IsLocalRing R] (S : Subring R),
  (∀ (x : R) (hx : x ∈ S), IsUnit x → IsUnit ⟨x, hx⟩) → IsLocalRing ↥S
-- Init.Data.BitVec.Lemmas
BitVec.getElem_eq_getElem? : ∀ {w : ℕ} (l : BitVec w) (i : ℕ) (h : i < w), l[i] = l[i]?.get ⋯
-- Aesop.Forward.State
Aesop.VariableMap.mk.sizeOf_spec : ∀ (map : Lean.PHashMap Aesop.PremiseIndex Aesop.InstMap), sizeOf { map := map } = 1 + sizeOf map
-- Lean.Parser.Do
Lean.Parser.Term.doMatch : Lean.Parser.Parser
-- Lean.Meta.Tactic.Grind.Theorems
Lean.Meta.Grind.TheoremLike : Type → Type
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.alter.congr_simp : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α] {β : Type v}
  (m m_1 : Std.ExtDHashMap α fun x => β),
  m = m_1 →
    ∀ (a a_1 : α),
      a = a_1 →
        ∀ (f f_1 : Option β → Option β),
          f = f_1 → Std.ExtDHashMap.Const.alter m a f = Std.ExtDHashMap.Const.alter m_1 a_1 f_1
-- Mathlib.RingTheory.Bialgebra.Hom
BialgHom.mul_apply : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : CoalgebraStruct R A] (φ ψ : A →ₐc[R] A) (x : A), (φ * ψ) x = φ (ψ x)
-- Mathlib.Order.Interval.Set.Basic
Set.Ici_sdiff_left : ∀ {α : Type u_1} [inst : PartialOrder α] {a : α}, Set.Ici a \ {a} = Set.Ioi a
-- Init.Data.UInt.Lemmas
UInt64.ofInt_neg_one : UInt64.ofInt (-1) = -1
-- Init.Data.SInt.Lemmas
Int32.le_iff_toBitVec_sle : ∀ {a b : Int32}, a ≤ b ↔ a.toBitVec.sle b.toBitVec = true
-- Lean.Meta.Tactic.Simp.SimpTheorems
Lean.Meta.Origin.decl.inj : ∀ {declName : Lean.Name} {post inv : Bool} {declName_1 : Lean.Name} {post_1 inv_1 : Bool},
  Lean.Meta.Origin.decl declName post inv = Lean.Meta.Origin.decl declName_1 post_1 inv_1 →
    declName = declName_1 ∧ post = post_1 ∧ inv = inv_1
-- Mathlib.CategoryTheory.Localization.Predicate
CategoryTheory.areEqualizedByLocalization_iff : ∀ {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] (L : CategoryTheory.Functor C D)
  (W : CategoryTheory.MorphismProperty C) {X Y : C} (f g : X ⟶ Y) [L.IsLocalization W],
  CategoryTheory.AreEqualizedByLocalization W f g ↔ L.map f = L.map g
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.Red.to_append_iff : ∀ {α : Type u} {L L₁ L₂ : List (α × Bool)},
  FreeAddGroup.Red L (L₁ ++ L₂) ↔ ∃ L₃ L₄, L = L₃ ++ L₄ ∧ FreeAddGroup.Red L₃ L₁ ∧ FreeAddGroup.Red L₄ L₂