mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.DirectSum.Finsupp
lmap_finsuppLEquivDirectSum_eq : ∀ (R : Type u) (M : Type v) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (ι : Type u_1)
  [inst_3 : DecidableEq ι] {N : Type u_2} [inst_4 : AddCommMonoid N] [inst_5 : Module R N] (ε : M →ₗ[R] N) (m : ι →₀ M),
  (DirectSum.lmap fun x => ε) ((finsuppLEquivDirectSum R M ι) m) =
    (finsuppLEquivDirectSum R N ι) (Finsupp.mapRange ⇑ε ⋯ m)
-- Std.Data.ExtDTreeMap.Lemmas
_private.Std.Data.ExtDTreeMap.Lemmas.0.Std.ExtDTreeMap.union_mk : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {t₁ t₂ : Std.DTreeMap α β cmp},
  (Std.ExtDTreeMap.mk t₁).union (Std.ExtDTreeMap.mk t₂) = Std.ExtDTreeMap.mk (t₁ ∪ t₂)
-- Std.Internal.Do.WP.Lemmas
Std.Internal.Do.WPMonad.wp_restoreM_refl_apply_eq : ∀ {Pred : Type u_1} {EPred : Type u_2} {m : Type u → Type v} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] {α : Type u}
  {post : α → Pred} {epost : EPred} [inst_4 : Pure m] (x : stM m m α),
  Std.Internal.Do.wp (restoreM x) post epost = Std.Internal.Do.wp (pure x) post epost
-- Init.Data.Sum.Basic
Sum.isRight_inl : ∀ {α : Type u_1} {β : Type u_2} {x : α}, (Sum.inl x).isRight = false
-- Init.Data.List.Lex
List.le_of_lt : ∀ {α : Type u_1} [inst : LT α] [i : Std.Asymm fun x1 x2 => x1 < x2] {l₁ l₂ : List α}, l₁ < l₂ → l₁ ≤ l₂
-- Mathlib.RingTheory.Finiteness.Small
Algebra.small_adjoin : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  [Small.{u, u_1} R] {s : Set S} [Small.{u, u_2} ↑s], Small.{u, u_2} ↥(Algebra.adjoin R s)
-- Lean.DocString.Types
Lean.Doc.instReprPart.repr : {i : Type u_1} → {b : Type u_2} → {p : Type u_3} → [Repr i] → [Repr b] → [Repr p] → Lean.Doc.Part i b p → ℕ → Std.Format
-- Mathlib.Algebra.Order.Hom.Monoid
/-- Copy of an `OrderMonoidHom` with a new `toFun` equal to the old one. Useful to fix
definitional equalities.  -/
OrderMonoidHom.copy : {α : Type u_2} →
  {β : Type u_3} →
    [inst : Preorder α] →
      [inst_1 : Preorder β] →
        [inst_2 : MulOneClass α] → [inst_3 : MulOneClass β] → (f : α →*o β) → (f' : α → β) → f' = ⇑f → α →*o β
-- Mathlib.Algebra.Polynomial.Eval.SMul
Polynomial.map_smul : ∀ {R : Type u} {S : Type v} [inst : Semiring R] {p : Polynomial R} [inst_1 : Semiring S] (f : R →+* S) (r : R),
  Polynomial.map f (r • p) = f r • Polynomial.map f p
-- Std.Time.Time.Unit.Basic
/-- Converts a `Minute.Offset` to a `Second.Offset`.
 -/
Std.Time.Second.Offset.ofMinutes : Std.Time.Minute.Offset → Std.Time.Second.Offset
-- Mathlib.Order.Hom.WithTopBot
LatticeHom.withBotWithTop.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : Lattice α] [inst_1 : Lattice β] (f : LatticeHom α β),
  f.withBotWithTop = { toLatticeHom := f.withTop.withBot, map_top' := ⋯, map_bot' := ⋯ }
-- Init.Data.Nat.Fold
_private.Init.Data.Nat.Fold.0.Nat.dfold.loop.eq_def : ∀ (n : ℕ) {α : (i : ℕ) → autoParam (i ≤ n) Nat.dfold._auto_1 → Type u} (f : (i : ℕ) → (h : i < n) → α i ⋯ → α (i + 1) ⋯)
  (j : ℕ) (a : j ≤ n) (a_1 : α (n - j) ⋯),
  Nat.dfold.loop✝ n f j a a_1 =
    match j, a, a_1 with
    | 0, h, a => a
    | m.succ, h, a => Nat.dfold.loop✝ n f m ⋯ (Nat.dfoldCast✝ α ⋯ (f (n - m.succ) ⋯ a))
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.ofNat_le_card : ∀ {o : Ordinal.{u_1}} {n : ℕ} [inst : n.AtLeastTwo], OfNat.ofNat n ≤ o.card ↔ OfNat.ofNat n ≤ o
-- Mathlib.Algebra.Homology.TotalComplex
HomologicalComplex₂.total.mapAux.mapMap_D₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {I₁ : Type u_2}
  {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {K L : HomologicalComplex₂ C c₁ c₂}
  (φ : K ⟶ L) (c₁₂ : ComplexShape I₁₂) [inst_2 : TotalComplexShape c₁ c₂ c₁₂] [inst_3 : DecidableEq I₁₂]
  [inst_4 : K.HasTotal c₁₂] [inst_5 : L.HasTotal c₁₂] (i₁₂ i₁₂' : I₁₂),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.GradedObject.mapMap (HomologicalComplex₂.toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂)
      (L.D₂ c₁₂ i₁₂ i₁₂') =
    CategoryTheory.CategoryStruct.comp (K.D₂ c₁₂ i₁₂ i₁₂')
      (CategoryTheory.GradedObject.mapMap (HomologicalComplex₂.toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂')
-- Mathlib.Topology.MetricSpace.ProperSpace.Real
ENNReal.instSecondCountableTopology : SecondCountableTopology ENNReal
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.normal_le_normalCore : ∀ {G : Type u_1} [inst : Group G] {H N : Subgroup G} [hN : N.Normal], N ≤ H.normalCore ↔ N ≤ H
-- Std.Async.System
Std.Async.System.CPUInfo.mk.inj : ∀ {model : String} {speed : ℕ} {times : Std.Async.System.CPUTimes} {model_1 : String} {speed_1 : ℕ}
  {times_1 : Std.Async.System.CPUTimes},
  { model := model, speed := speed, times := times } = { model := model_1, speed := speed_1, times := times_1 } →
    model = model_1 ∧ speed = speed_1 ∧ times = times_1
-- Init.Data.Bool
Bool.decide_eq_true : ∀ {b : Bool} {x : Decidable (b = true)}, decide (b = true) = b
-- Mathlib.Topology.Constructible
Topology.IsLocallyConstructible.sInter : ∀ {X : Type u_2} [inst : TopologicalSpace X] {S : Set (Set X)},
  S.Finite → (∀ s ∈ S, Topology.IsLocallyConstructible s) → Topology.IsLocallyConstructible (⋂₀ S)
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.iUnion_vadd_right_image : ∀ {α : Type u_2} {β : Type u_3} [inst : VAdd α β] {s : Set α} {t : Set β}, ⋃ a ∈ t, (fun x => x +ᵥ a) '' s = s +ᵥ t
-- Mathlib.MeasureTheory.Covering.VitaliFamily
VitaliFamily.filterAt.eq_1 : ∀ {X : Type u_1} [inst : PseudoMetricSpace X] {m0 : MeasurableSpace X} {μ : MeasureTheory.Measure X}
  (v : VitaliFamily μ) (x : X), v.filterAt x = (nhds x).smallSets ⊓ Filter.principal (v.setsAt x)
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
tprod_mulIndicator_of_notMem : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] (s : γ → Set β)
  (f : β → α) (i : β), (∀ (d : γ), i ∉ s d) → ∏' (d : γ), (s d).mulIndicator f i = 1
-- Lean.Meta.Tactic.Grind.Arith.CommRing.RingM
Lean.Meta.Grind.Arith.CommRing.instMonadCommRingRingM : Lean.Meta.Grind.Arith.CommRing.MonadCommRing Lean.Meta.Grind.Arith.CommRing.RingM
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
/-- Bundle `ρᵣ _` as an isomorphism of functors.  -/
CategoryTheory.MonoidalCategory.MonoidalRightAction.actionUnitNatIso : (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.MonoidalCategory C] →
          [inst_3 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D] →
            CategoryTheory.MonoidalCategory.MonoidalRightAction.actionRight D
                (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ≅
              CategoryTheory.Functor.id D
-- Mathlib.Algebra.Homology.ShortComplex.ModuleCat
CategoryTheory.ShortComplex.moduleCatLeftHomologyData_i_hom : ∀ {R : Type u} [inst : Ring R] (S : CategoryTheory.ShortComplex (ModuleCat R)),
  ModuleCat.Hom.hom S.moduleCatLeftHomologyData.i = (ModuleCat.Hom.hom S.g).ker.subtype
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.getThenInsertIfNew?.congr_simp : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} [inst : Std.TransCmp cmp]
  (t t_1 : Std.ExtDTreeMap α (fun x => β) cmp),
  t = t_1 →
    ∀ (a a_1 : α),
      a = a_1 →
        ∀ (b b_1 : β),
          b = b_1 →
            Std.ExtDTreeMap.Const.getThenInsertIfNew? t a b = Std.ExtDTreeMap.Const.getThenInsertIfNew? t_1 a_1 b_1
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem!_diff_of_not_mem_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited β], m₁.WF → m₂.WF → ∀ {k : α}, k ∉ m₂ → (m₁ \ m₂)[k]! = m₁[k]!
-- Mathlib.Data.List.Sigma
List.kerase_kerase : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {a a' : α} {l : List (Sigma β)},
  List.kerase a (List.kerase a' l) = List.kerase a' (List.kerase a l)
-- Mathlib.Algebra.Lie.Semisimple.Defs
LieSubmodule.eq_top_of_isIrreducible : ∀ (R : Type u_1) (L : Type u_2) (M : Type u_3) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] [LieModule.IsIrreducible R L M] (N : LieSubmodule R L M)
  [Nontrivial ↥N], N = ⊤
-- Mathlib.LinearAlgebra.Matrix.ConjTranspose
Matrix.dotProduct_star : ∀ {m : Type u_2} {α : Type v} [inst : Fintype m] [inst_1 : NonUnitalSemiring α] [inst_2 : StarRing α] (v w : m → α),
  v ⬝ᵥ star w = star (w ⬝ᵥ star v)
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
CategoryTheory.Bicategory.Adj.Bicategory.associator_hom_τr : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c d : CategoryTheory.Bicategory.Adj B} (α : a ⟶ b) (β : b ⟶ c)
  (γ : c ⟶ d),
  (CategoryTheory.Bicategory.Adj.Bicategory.associator α β γ).hom.τr =
    (CategoryTheory.Bicategory.associator γ.r β.r α.r).hom
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.BoundedFormula.freeVarFinset.eq_4 : ∀ {L : FirstOrder.Language} {α : Type u'} [inst : DecidableEq α] (x : ℕ) (f₁ f₂ : L.BoundedFormula α x),
  (f₁.imp f₂).freeVarFinset = f₁.freeVarFinset ∪ f₂.freeVarFinset
-- Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Multiset.coe_sumAddMonoidHom : ∀ {M : Type u_5} [inst : AddCommMonoid M], ⇑Multiset.sumAddMonoidHom = Multiset.sum
-- Mathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy
CategoryTheory.Arrow.RightHomotopy.trans_hom : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] [inst_1 : CategoryTheory.Preadditive V]
  {u v : CategoryTheory.Arrow V} {e f g : u ⟶ v} (h : CategoryTheory.Arrow.RightHomotopy e f)
  (k : CategoryTheory.Arrow.RightHomotopy f g), (h.trans k).hom = h.hom + k.hom
-- Mathlib.GroupTheory.OrderOfElement
addOrderOf_le_card_univ : ∀ {G : Type u_1} [inst : AddMonoid G] {x : G} [inst_1 : Fintype G], addOrderOf x ≤ Fintype.card G
-- Mathlib.FieldTheory.PurelyInseparable.Basic
/-- If `E` is an algebraic closure of `F`, then `F` is separably closed if and only if `E / F` is
purely inseparable.  -/
isSepClosed_iff_isPurelyInseparable_algebraicClosure : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] [IsAlgClosure F E],
  IsSepClosed F ↔ IsPurelyInseparable F E
-- Mathlib.RingTheory.Localization.InvSubmonoid
IsLocalization.toInvSubmonoid_mul : ∀ {R : Type u_1} [inst : CommRing R] (M : Submonoid R) (S : Type u_2) [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : IsLocalization M S] (m : ↥M), ↑((IsLocalization.toInvSubmonoid M S) m) * (algebraMap R S) ↑m = 1
-- Mathlib.Data.Matrix.DMatrix
DMatrix.subsingleton_of_empty_right : ∀ {m : Type u_1} {n : Type u_2} {α : m → n → Type v} [IsEmpty n], Subsingleton (DMatrix m n α)
-- Mathlib.RingTheory.WittVector.Truncated
TruncatedWittVector.coeff_mk : ∀ {p n : ℕ} {R : Type u_1} (x : Fin n → R) (i : Fin n), TruncatedWittVector.coeff i (TruncatedWittVector.mk p x) = x i
-- Mathlib.Analysis.Convex.Strict
/-- The translation of a strictly convex set is also strictly convex.  -/
StrictConvex.preimage_add_right : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : TopologicalSpace E]
  [inst_3 : AddCancelCommMonoid E] [ContinuousAdd E] [inst_5 : Module 𝕜 E] {s : Set E},
  StrictConvex 𝕜 s → ∀ (z : E), StrictConvex 𝕜 ((fun x => z + x) ⁻¹' s)
-- Std.Data.HashMap.RawLemmas
/-- Variant of `getElem_map` that holds with `EquivBEq` (i.e. without `LawfulBEq`).  -/
Std.HashMap.Raw.getElem_map' : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β}
  [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] {f : α → β → γ} {k : α} {h' : k ∈ Std.HashMap.Raw.map f m}
  (h : m.WF), (Std.HashMap.Raw.map f m)[k] = f (m.getKey k ⋯) m[k]
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
OpenPartialHomeomorph.extend_prod : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} {E' : Type u_5} {M' : Type u_6} {H' : Type u_7}
  [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M] (f : OpenPartialHomeomorph M H)
  {I : ModelWithCorners 𝕜 E H} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E']
  [inst_7 : TopologicalSpace H'] [inst_8 : TopologicalSpace M'] {I' : ModelWithCorners 𝕜 E' H'}
  (f' : OpenPartialHomeomorph M' H'), (f.prod f').extend (I.prod I') = (f.extend I).prod (f'.extend I')
-- Mathlib.NumberTheory.Primorial
primorial.eq_1 : ∀ (n : ℕ), primorial n = ∏ p ∈ Finset.range (n + 1) with Nat.Prime p, p
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.lift.eq_1 : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] {N : Type u_3} [inst_1 : Monoid N],
  Monoid.CoprodI.lift =
    { toFun := fun fi => (conGen (Monoid.CoprodI.Rel M)).lift (FreeMonoid.lift fun p => (fi p.fst) p.snd) ⋯,
      invFun := fun f x => f.comp Monoid.CoprodI.of, left_inv := ⋯, right_inv := ⋯ }
-- Aesop.RuleTac.Tactic
Aesop.RuleTac.tacticM : Lean.Name → Aesop.RuleTac
-- Mathlib.Algebra.Order.Archimedean.Real.Basic
Real.iInf_const_zero : ∀ {ι : Sort u_1}, ⨅ x, 0 = 0
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKeyD_diff_of_contains_eq_false_left : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  (h₁ : m₁.WF),
  m₂.WF →
    ∀ {k fallback : α}, Std.DTreeMap.Internal.Impl.contains k m₁ = false → (m₁.diff m₂ ⋯).getKeyD k fallback = fallback
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.maxKey!_le : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α],
  t.WF → t.isEmpty = false → ∀ {k : α}, (cmp t.maxKey! k).isLE = true ↔ ∀ k' ∈ t, (cmp k' k).isLE = true
-- Mathlib.SetTheory.Cardinal.Continuum
Cardinal.nat_mul_continuum : ∀ {n : ℕ}, n ≠ 0 → ↑n * Cardinal.continuum = Cardinal.continuum
-- Mathlib.Order.Filter.Basic
Filter.GenerateSets.basic : ∀ {α : Type u} {g : Set (Set α)} {s : Set α}, s ∈ g → Filter.GenerateSets g s
-- Mathlib.CategoryTheory.Grothendieck
/-- The functor `Grothendieck.map α : Grothendieck F ⥤ Grothendieck G` lies over `C`.  -/
CategoryTheory.Grothendieck.functor_comp_forget : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor C CategoryTheory.Cat}
  {α : F ⟶ G},
  (CategoryTheory.Grothendieck.map α).comp (CategoryTheory.Grothendieck.forget G) = CategoryTheory.Grothendieck.forget F
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unitary
cfc_unitary_iff : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommRing R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalRing R] [inst_4 : ContinuousStar R] [inst_5 : TopologicalSpace A] [inst_6 : Ring A]
  [inst_7 : StarRing A] [inst_8 : Algebra R A] [inst_9 : ContinuousFunctionalCalculus R A p] (f : R → R) (a : A),
  autoParam (p a) cfc_unitary_iff._auto_1 →
    autoParam (ContinuousOn f (spectrum R a)) cfc_unitary_iff._auto_3 →
      (cfc f a ∈ unitary A ↔ ∀ x ∈ spectrum R a, star (f x) * f x = 1)
-- Lean.Parser.Command
Lean.Parser.Command.init_quot.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Init.Data.UInt.Bitwise
instIdempotentOpUInt64HAnd : Std.IdempotentOp fun x1 x2 => x1 &&& x2
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem_insertIfNew : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [inst : Std.TransCmp cmp] (h : t.WF)
  {k a : α} {v : β} {h₁ : a ∈ t.insertIfNew k v},
  (t.insertIfNew k v)[a] = if h₂ : cmp k a = Ordering.eq ∧ k ∉ t then v else t[a]
-- Mathlib.Data.Seq.Computation
Computation.liftRel_pure : ∀ {α : Type u} {β : Type v} (R : α → β → Prop) (a : α) (b : β),
  Computation.LiftRel R (Computation.pure a) (Computation.pure b) ↔ R a b
-- Mathlib.Analysis.Normed.Group.Basic
preimage_mul_sphere : ∀ {E : Type u_5} [inst : SeminormedCommGroup E] (a b : E) (r : ℝ),
  (fun x => b * x) ⁻¹' Metric.sphere a r = Metric.sphere (a / b) r
-- Mathlib.Tactic.Simproc.Divisors
_private.Mathlib.Tactic.Simproc.Divisors.0.Nat.divisors_ofNat.unsafe_impl_2 : ℕ → List ℕ
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
ContinuousLinearMap.rTensor_comp_lTensor : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {H : Type u_5} [inst : RCLike 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F]
  [inst_4 : InnerProductSpace 𝕜 F] [inst_5 : NormedAddCommGroup G] [inst_6 : InnerProductSpace 𝕜 G]
  [inst_7 : NormedAddCommGroup H] [inst_8 : InnerProductSpace 𝕜 H] (f : E →L[𝕜] F) (g : G →L[𝕜] H),
  ContinuousLinearMap.rTensor H f ∘SL ContinuousLinearMap.lTensor E g = TensorProduct.mapL f g
-- Mathlib.Computability.AkraBazzi.SumTransform
/-- The asymptotic bound satisfied by an Akra-Bazzi recurrence, namely
`n^p (1 + ∑_{u < n} g(u) / u^(p+1))`.  -/
AkraBazziRecurrence.asympBound : {α : Type u_1} → [Fintype α] → (ℝ → ℝ) → (α → ℝ) → (α → ℝ) → ℕ → ℝ
-- Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
/-- If `p` is prime and `J(a | p) = 1`, then `a` is a square mod `p`.  -/
ZMod.isSquare_of_jacobiSym_eq_one : ∀ {a : ℤ} {p : ℕ} [inst : Fact (Nat.Prime p)], jacobiSym a p = 1 → IsSquare ↑a
-- Mathlib.Order.Interval.Set.Basic
Set.decidableMemIcc : {α : Type u_1} →
  [inst : Preorder α] → {a b x : α} → [Decidable (a ≤ x)] → [Decidable (x ≤ b)] → Decidable (x ∈ Set.Icc a b)
-- Mathlib.Algebra.Group.Nat.Defs
Nat.instAddSemigroup : AddSemigroup ℕ
-- Mathlib.Algebra.Category.ModuleCat.EpiMono
ModuleCat.range_eq_top_of_epi : ∀ {R : Type u} [inst : Ring R] {X Y : ModuleCat R} (f : X ⟶ Y) [CategoryTheory.Epi f], (ModuleCat.Hom.hom f).range = ⊤
-- Mathlib.Algebra.Category.Ring.Colimits
/-- Evidence that the proposed colimit is the colimit.  -/
CommRingCat.Colimits.colimitIsColimit : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    (F : CategoryTheory.Functor J CommRingCat) → CategoryTheory.Limits.IsColimit (CommRingCat.Colimits.colimitCocone F)
-- Mathlib.Algebra.MonoidAlgebra.Cardinal
MonoidAlgebra.cardinalMk_eq_lift_of_fintype : ∀ (R : Type u) (M' : Type v) [inst : Semiring R] [inst_1 : Fintype M'],
  Cardinal.mk (MonoidAlgebra R M') = Cardinal.lift.{v, u} (Cardinal.mk R) ^ Fintype.card M'
-- Mathlib.Analysis.ODE.PicardLindelof
/-- The `n`-th iterate of `next` is Lipschitz continuous with respect to `FunSpace`, with constant
$(K \max(t_{\mathrm{max}}, t_{\mathrm{min}})^n / n!$.  -/
ODE.FunSpace.dist_iterate_next_iterate_next_le : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E → E} {tmin tmax : ℝ}
  {t₀ : ↑(Set.Icc tmin tmax)} {x₀ x : E} {a r L K : NNReal} (hf : IsPicardLindelof f t₀ x₀ a r L K)
  (hx : x ∈ Metric.closedBall x₀ ↑r) (α β : ODE.FunSpace t₀ x₀ r L) (n : ℕ),
  dist ((ODE.FunSpace.next hf hx)^[n] α) ((ODE.FunSpace.next hf hx)^[n] β) ≤
    (↑K * max (tmax - ↑t₀) (↑t₀ - tmin)) ^ n / ↑n.factorial * dist α β
-- Mathlib.Order.Filter.Pointwise
Filter.NeBot.smul_filter : ∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β] {f : Filter β} {a : α}, f.NeBot → (a • f).NeBot
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
PiTensorProduct.map_tprod : ∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] {s : ι → Type u_7} [inst_1 : (i : ι) → AddCommMonoid (s i)]
  [inst_2 : (i : ι) → Module R (s i)] {t : ι → Type u_11} [inst_3 : (i : ι) → AddCommMonoid (t i)]
  [inst_4 : (i : ι) → Module R (t i)] (f : (i : ι) → s i →ₗ[R] t i) (x : (i : ι) → s i),
  (PiTensorProduct.map f) ((PiTensorProduct.tprod R) x) = ⨂ₜ[R] (i : ι), (f i) (x i)
-- Mathlib.Order.Filter.Basic
Filter.copy_eq : ∀ {α : Type u} {f : Filter α} {S : Set (Set α)} (hmem : ∀ (s : Set α), s ∈ S ↔ s ∈ f), f.copy S hmem = f
-- Mathlib.Topology.Category.Stonean.EffectiveEpi
Stonean.instPreservesEffectiveEpisCompHausToCompHaus : Stonean.toCompHaus.PreservesEffectiveEpis
-- Mathlib.Topology.Order.LawsonTopology
/-- A lower set is Lawson closed if and only if it is closed under sups of directed sets  -/
Topology.lawsonClosed_iff_dirSupClosed_of_isLowerSet : ∀ {α : Type u_1} [inst : Preorder α] (L S : TopologicalSpace α) [Topology.IsLawson α] [Topology.IsScott α Set.univ]
  (s : Set α), IsLowerSet s → (IsClosed s ↔ DirSupClosed s)
-- Mathlib.Order.Hom.Lattice
SupHom.symm_dual_comp : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Max α] [inst_1 : Max β] [inst_2 : Max γ] (g : InfHom βᵒᵈ γᵒᵈ)
  (f : InfHom αᵒᵈ βᵒᵈ), SupHom.dual.symm (g.comp f) = (SupHom.dual.symm g).comp (SupHom.dual.symm f)
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubMulAction.ext_iff : ∀ {R : Type u} {M : Type v} [inst : SMul R M] {p q : SubMulAction R M}, p = q ↔ ∀ (x : M), x ∈ p ↔ x ∈ q
-- Mathlib.Topology.Separation.Basic
instR1SpaceSubtype : ∀ {X : Type u_1} [inst : TopologicalSpace X] [R1Space X] (p : X → Prop), R1Space (Subtype p)
-- Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant
CategoryTheory.Functor.IsEventuallyConstantTo.isIso_map : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] {F : CategoryTheory.Functor J C} {i₀ : J},
  F.IsEventuallyConstantTo i₀ → ∀ {i j : J} (φ : i ⟶ j) (π : j ⟶ i₀), CategoryTheory.IsIso (F.map φ)
-- Std.Time.DateTime
/-- Creates a new `DateTime` by adjusting the `nano` component with a new `millis` that will set
in the millisecond scale.
 -/
Std.Time.DateTime.withMilliseconds : Std.Time.DateTime → Std.Time.Millisecond.Ordinal → Std.Time.DateTime
-- Batteries.Data.Fin.Coding
_private.Batteries.Data.Fin.Coding.0.Fin.encodeOption.match_1.eq_2 : ∀ {n : ℕ} (motive : Option (Fin n) → Sort u_1) (i : ℕ) (h : i < n) (h_1 : Unit → motive none)
  (h_2 : (i : ℕ) → (h : i < n) → motive (some ⟨i, h⟩)),
  (match some ⟨i, h⟩ with
    | none => h_1 ()
    | some ⟨i, h⟩ => h_2 i h) =
    h_2 i h
-- Mathlib.SetTheory.Cardinal.Regular
Cardinal.not_isSingular_aleph0 : ¬Cardinal.aleph0.IsSingular
-- Lean.Elab.InfoTree.Types
Lean.Elab.FieldInfo.mk.sizeOf_spec : ∀ (projName fieldName : Lean.Name) (lctx : Lean.LocalContext) (val : Lean.Expr) (stx : Lean.Syntax),
  sizeOf { projName := projName, fieldName := fieldName, lctx := lctx, val := val, stx := stx } =
    1 + sizeOf projName + sizeOf fieldName + sizeOf lctx + sizeOf val + sizeOf stx
-- Mathlib.Data.Finset.Sups
Finset.diffs_nonempty : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : GeneralizedBooleanAlgebra α] {s t : Finset α},
  (s.diffs t).Nonempty ↔ s.Nonempty ∧ t.Nonempty
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
/-- Custom simps projection for `IdealSheafData`.  -/
AlgebraicGeometry.Scheme.IdealSheafData.Simps.coe_support : {X : AlgebraicGeometry.Scheme} → X.IdealSheafData → Set ↥X
-- Mathlib.Algebra.Order.GroupWithZero.Basic
/-- See `inv_le_iff_one_le_mul₀'` for a version with multiplication on the other side.  -/
inv_le_iff_one_le_mul₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [MulPosReflectLT G₀] {a b : G₀},
  0 < a → (a⁻¹ ≤ b ↔ 1 ≤ b * a)
-- Mathlib.RingTheory.Valuation.Discrete.Basic
Valuation.Uniformizer.ext : ∀ {Γ : Type u_1} {inst : LinearOrderedCommGroupWithZero Γ} {A : Type u_2} {inst_1 : Ring A} {v : Valuation A Γ}
  {hv : v.IsRankOneDiscrete} {x y : v.Uniformizer}, x.val = y.val → x = y
-- Mathlib.RingTheory.Finiteness.Basic
AlgHom.Finite.id : ∀ (R : Type u_1) (A : Type u_2) [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A], (AlgHom.id R A).Finite
-- Init.Data.List.Lemmas
List.tailD_map : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {l l' : List α},
  (List.map f l).tailD (List.map f l') = List.map f (l.tailD l')
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.cons_append : ∀ {α : Type u} (a : α) (s t : Stream'.WSeq α), (Stream'.WSeq.cons a s).append t = Stream'.WSeq.cons a (s.append t)
-- Mathlib.Analysis.Calculus.Deriv.Mul
HasDerivWithinAt.const_smul : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} {s : Set 𝕜} {R : Type u_2} [inst_3 : Monoid R]
  [inst_4 : DistribMulAction R F] [SMulCommClass 𝕜 R F] [ContinuousConstSMul R F] (c : R),
  HasDerivWithinAt f f' s x → HasDerivWithinAt (c • f) (c • f') s x