mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Matrix.ToLin
Matrix.toLinAlgEquiv_symm : ∀ {R : Type u_1} [inst : CommSemiring R] {n : Type u_4} [inst_1 : Fintype n] [inst_2 : DecidableEq n] {M₁ : Type u_5}
  [inst_3 : AddCommMonoid M₁] [inst_4 : Module R M₁] (v₁ : Module.Basis n R M₁),
  (Matrix.toLinAlgEquiv v₁).symm = LinearMap.toMatrixAlgEquiv v₁
-- Mathlib.Order.WellFounded
StrictAnti.range_inj : ∀ {β : Type u_2} {γ : Type u_3} [inst : LinearOrder β] [inst_1 : Preorder γ] [WellFoundedGT β] {f g : β → γ},
  StrictAnti f → StrictAnti g → (Set.range f = Set.range g ↔ f = g)
-- Mathlib.Algebra.Group.Conj
AddConjClasses.mkEquiv.eq_1 : ∀ {α : Type u} [inst : AddCommMonoid α],
  AddConjClasses.mkEquiv = { toFun := AddConjClasses.mk, invFun := Quotient.lift id ⋯, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Ioi_union_Iio : ∀ {α : Type u_1} [inst : LinearOrder α] {a : α}, Set.Ioi a ∪ Set.Iio a = {a}ᶜ
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toList_rcc_add_right_eq_map : ∀ {m n : ℕ}, (m...=m + n).toList = List.map (fun x => x + m) (0...=n).toList
-- Mathlib.Topology.Algebra.Group.GroupTopology
AddGroupTopology.instBot : {α : Type u} → [inst : AddGroup α] → Bot (AddGroupTopology α)
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
/-- The norm `intNorm` lifts to a function on `integerSet K` modulo `torsion K`.  -/
NumberField.mixedEmbedding.fundamentalCone.quotIntNorm : {K : Type u_1} →
  [inst : Field K] →
    [inst_1 : NumberField K] →
      Quotient
          (MulAction.orbitRel ↥(NumberField.Units.torsion K)
            ↑(NumberField.mixedEmbedding.fundamentalCone.integerSet K)) →
        ℕ
-- Mathlib.Data.ENat.Basic
ENat.exists_ne_top : ∀ {p : ℕ∞ → Prop}, (∃ x, x ≠ ⊤ ∧ p x) ↔ ∃ x, p ↑x
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.MemLp.continuousLinearMap_comp : ∀ {α : Type u_1} {𝕜 : Type u_2} {E : Type u_4} {F : Type u_5} {m : MeasurableSpace α} {p : ENNReal}
  {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedSpace 𝕜 F] {f : α → E},
  MeasureTheory.MemLp f p μ → ∀ (L : E →L[𝕜] F), MeasureTheory.MemLp (fun x => L (f x)) p μ
-- Mathlib.Algebra.Homology.Embedding.CochainComplex
CochainComplex.quasiIso_πTruncGE_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : CochainComplex C ℤ) [inst_2 : CategoryTheory.Limits.HasZeroObject C]
  [inst_3 : ∀ (i : ℤ), HomologicalComplex.HasHomology K i] (n : ℤ), QuasiIso (K.πTruncGE n) ↔ K.IsGE n
-- Mathlib.Algebra.Order.Interval.Basic
NonemptyInterval.divisionCommMonoid : {α : Type u_2} →
  [inst : CommGroup α] → [inst_1 : PartialOrder α] → [IsOrderedMonoid α] → DivisionCommMonoid (NonemptyInterval α)
-- Init.Meta.Defs
/-- Syntax that represents a numeric literal.
 -/
Lean.Syntax.NumLit : Type
-- Mathlib.Combinatorics.Quiver.Symmetric
Quiver.Path.reverse_comp : ∀ {V : Type u_2} [inst : Quiver V] [inst_1 : Quiver.HasReverse V] {a b c : V} (p : Quiver.Path a b)
  (q : Quiver.Path b c), (p.comp q).reverse = q.reverse.comp p.reverse
-- Mathlib.Algebra.Field.Subfield.Defs
/-- A `Subring` containing inverses is a `Subfield`.  -/
Subring.toSubfield : {K : Type u} → [inst : DivisionRing K] → (s : Subring K) → (∀ x ∈ s, x⁻¹ ∈ s) → Subfield K
-- Lean.Data.Lsp.Extra
Lean.Lsp.LeanFileProgressParams.processing : Lean.Lsp.LeanFileProgressParams → Array Lean.Lsp.LeanFileProgressProcessingInfo
-- Init.Data.Option.Lemmas
Option.not_isSome_iff_eq_none : ∀ {α : Type u_1} {o : Option α}, ¬o.isSome = true ↔ o = none
-- Mathlib.Combinatorics.SimpleGraph.Metric
/-- Ball membership is symmetric in center and point.  -/
SimpleGraph.mem_ball_comm : ∀ {V : Type u_1} {G : SimpleGraph V} {c v : V} {r : ℕ∞}, v ∈ G.ball c r ↔ c ∈ G.ball v r
-- Mathlib.CategoryTheory.Localization.Monoidal.Braided
CategoryTheory.Localization.Monoidal.braidingNatIso_hom_app_naturality_μ_right_assoc : ∀ {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) [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : W.IsMonoidal]
  [inst_4 : L.IsLocalization W] {unit : D} (ε : L.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ≅ unit)
  [inst_5 : CategoryTheory.BraidedCategory C] (X Y Z : C) {Z_1 : CategoryTheory.LocalizedMonoidal L W ε}
  (h :
    CategoryTheory.MonoidalCategoryStruct.tensorObj
        ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Z)
        ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj
          (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)) ⟶
      Z_1),
  CategoryTheory.CategoryStruct.comp
      (((CategoryTheory.Localization.Monoidal.braidingNatIso L W ε).hom.app
            (CategoryTheory.MonoidalCategoryStruct.tensorObj
              ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj X)
              ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Y))).app
        ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Z))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft
          ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Z)
          (CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε) X Y))
        h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight
        (CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε) X Y)
        ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Z))
      (CategoryTheory.CategoryStruct.comp
        (((CategoryTheory.Localization.Monoidal.braidingNatIso L W ε).hom.app
              ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj
                (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y))).app
          ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Z))
        h)
-- Mathlib.Data.Set.Lattice
Set.iInter_const : ∀ {β : Type u_2} {ι : Sort u_5} [Nonempty ι] (s : Set β), ⋂ x, s = s
-- Mathlib.Algebra.ContinuedFractions.Basic
GenContFract.mk.inj : ∀ {α : Type u_1} {h : α} {s : Stream'.Seq (GenContFract.Pair α)} {h_1 : α} {s_1 : Stream'.Seq (GenContFract.Pair α)},
  { h := h, s := s } = { h := h_1, s := s_1 } → h = h_1 ∧ s = s_1
-- Batteries.Data.Float.Basic
/-- The floating point value "positive infinity", also used to represent numerical computations
which produce finite values outside of the representable range of `Float32`.
 -/
Float32.inf : Float32
-- Mathlib.Data.Finset.Image
Finset.map_comm : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Finset α} {β' : Type u_4} {f : β ↪ γ} {g : α ↪ β} {f' : α ↪ β'}
  {g' : β' ↪ γ}, (∀ (a : α), f (g a) = g' (f' a)) → Finset.map f (Finset.map g s) = Finset.map g' (Finset.map f' s)
-- Mathlib.ModelTheory.FinitelyGenerated
FirstOrder.Language.Substructure.cg_iff_empty_or_exists_nat_generating_family : ∀ {L : FirstOrder.Language} {M : Type u_1} [inst : L.Structure M] {N : L.Substructure M},
  N.CG ↔ ↑N = ∅ ∨ ∃ s, (FirstOrder.Language.Substructure.closure L).toFun (Set.range s) = N
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.mem_of_mem_insertIfNew : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {k a : α} {v : β}, a ∈ m.insertIfNew k v → (k == a) = false → a ∈ m
-- Mathlib.Topology.Clopen
isClopen_compl_iff : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, IsClopen sᶜ ↔ IsClopen s
-- Mathlib.Analysis.Complex.CauchyIntegral
/-- **Cauchy integral formula for derivatives**, assuming `f` is continuous on a closed ball and
differentiable on its interior.  -/
DiffContOnCl.circleIntegral_one_div_sub_center_pow_smul : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [CompleteSpace E] {R : ℝ} {f : ℂ → E} {c : ℂ},
  0 < R →
    ∀ (n : ℕ),
      DiffContOnCl ℂ f (Metric.ball c R) →
        ∮ (z : ℂ) in C(c, R), (1 / (z - c) ^ (n + 1)) • f z =
          (2 * ↑Real.pi * Complex.I / ↑n.factorial) • iteratedDeriv n f c
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.forMUncurried_eq_forM_toList : ∀ {α : Type u} {cmp : α → α → Ordering} {m : Type w → Type w'} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp}
  [inst : Monad m] [LawfulMonad m] {f : α × β → m PUnit.{w + 1}},
  Std.DTreeMap.Raw.Const.forMUncurried f t = (Std.DTreeMap.Raw.Const.toList t).forM f
-- Mathlib.CategoryTheory.Limits.Constructions.Over.Products
/-- (Implementation)
Given a product diagram in `C/B`, construct the corresponding wide pullback diagram
in `C`.
 -/
CategoryTheory.Over.ConstructProducts.widePullbackDiagramOfDiagramOver : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (B : C) →
      {J : Type w} →
        CategoryTheory.Functor (CategoryTheory.Discrete J) (CategoryTheory.Over B) →
          CategoryTheory.Functor (CategoryTheory.Limits.WidePullbackShape J) C
-- Mathlib.RingTheory.DedekindDomain.LinearDisjoint
Module.Basis.ofIsCoprimeDifferentIdeal_apply : ∀ (A : Type u_1) (B : Type u_2) {K : Type u_3} {L : Type u_4} [inst : CommRing A] [inst_1 : Field K]
  [inst_2 : Algebra A K] [inst_3 : IsFractionRing A K] [inst_4 : CommRing B] [inst_5 : Field L] [inst_6 : Algebra B L]
  [inst_7 : Algebra A L] [inst_8 : Algebra K L] [inst_9 : FiniteDimensional K L] [inst_10 : IsScalarTower A K L]
  (R₁ : Type u_5) (R₂ : Type u_6) [inst_11 : CommRing R₁] [inst_12 : CommRing R₂] [inst_13 : IsDomain R₁]
  [inst_14 : Algebra A R₁] [inst_15 : Algebra A R₂] [inst_16 : Algebra R₁ B] [inst_17 : Algebra R₂ B]
  [inst_18 : Algebra R₁ L] [inst_19 : Algebra R₂ L] [inst_20 : IsScalarTower A R₁ L] [inst_21 : IsScalarTower R₁ B L]
  [inst_22 : IsScalarTower R₂ B L] [inst_23 : Module.Finite A R₂] {F₁ F₂ : IntermediateField K L}
  [inst_24 : Algebra R₁ ↥F₁] [inst_25 : Algebra R₂ ↥F₂] [inst_26 : Module.IsTorsionFree R₁ ↥F₁]
  [inst_27 : IsScalarTower A (↥F₂) L] [inst_28 : IsScalarTower A R₂ ↥F₂] [inst_29 : IsScalarTower R₁ (↥F₁) L]
  [inst_30 : IsScalarTower R₂ (↥F₂) L] [inst_31 : Algebra.IsSeparable K ↥F₂] [inst_32 : Algebra.IsSeparable (↥F₁) L]
  [inst_33 : IsDomain A] [inst_34 : IsDedekindDomain B] [inst_35 : IsDedekindDomain R₁] [inst_36 : IsDedekindDomain R₂]
  [inst_37 : IsFractionRing B L] [inst_38 : IsFractionRing R₁ ↥F₁] [inst_39 : IsFractionRing R₂ ↥F₂]
  [inst_40 : IsIntegrallyClosed A] [inst_41 : IsIntegralClosure B R₁ L] [inst_42 : Module.IsTorsionFree R₁ B]
  [inst_43 : Module.IsTorsionFree R₂ B], ⋯
-- Mathlib.Probability.Martingale.Basic
MeasureTheory.Martingale.add : ∀ {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [inst : Preorder ι] {m0 : MeasurableSpace Ω}
  {μ : MeasureTheory.Measure Ω} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E] {f g : ι → Ω → E}
  {ℱ : MeasureTheory.Filtration ι m0} [CompleteSpace E],
  MeasureTheory.Martingale f ℱ μ → MeasureTheory.Martingale g ℱ μ → MeasureTheory.Martingale (f + g) ℱ μ
-- Init.Data.SInt.Lemmas
Int16.toISize_ofBitVec : ∀ (b : BitVec 16), (Int16.ofBitVec b).toISize = ISize.ofBitVec (BitVec.signExtend System.Platform.numBits b)
-- Lean.Meta.Tactic.Grind.Types
/-- Returns `true` if `s` has been already added to the case-split list at one point.
Remark: this function returns `true` even if the split has already been resolved
and is not in the list anymore.
 -/
Lean.Meta.Grind.isKnownCaseSplit : Lean.Meta.Grind.SplitInfo → Lean.Meta.Grind.GoalM Bool
-- Lean.Elab.Tactic.RCases
Lean.Elab.Tactic.RCases.instCoeTSyntaxConsSyntaxNodeKindMkStr1NilMkStr4_lean : Coe (Lean.TSyntax `rcasesPat) (Lean.TSyntax `Lean.Parser.Tactic.rcasesPatMed)
-- Mathlib.Algebra.Order.Module.Field
PosSMulMono.toPosSMulReflectLE : ∀ {𝕜 : Type u_1} {G : Type u_2} [inst : Semifield 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : PartialOrder G] [inst_4 : MulAction 𝕜 G] [PosSMulMono 𝕜 G], PosSMulReflectLE 𝕜 G
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.DTreeMap.Internal.Impl.updateCell.match_1.splitter : {α : Type u_2} →
  {β : α → Type u_1} →
    (motive : Option ((a : α) × β a) → Sort u_3) →
      (x : Option ((a : α) × β a)) → (Unit → motive none) → ((k' : α) → (v' : β k') → motive (some ⟨k', v'⟩)) → motive x
-- Mathlib.Algebra.Order.BigOperators.Expect
Finset.lt_expect : ∀ {ι : Type u_1} {α : Type u_2} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [IsOrderedCancelAddMonoid α]
  [inst_3 : Module ℚ≥0 α] [PosSMulStrictMono ℚ≥0 α] {s : Finset ι} {f : ι → α} {a : α},
  (∀ x ∈ s, a ≤ f x) → (∃ x ∈ s, a < f x) → a < s.expect fun i => f i
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Umod
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Umod.0.Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.go.eq_2 : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (n d : aig.RefVec w) (wn wr : ℕ)
  (q r : aig.RefVec w) (curr_2 : ℕ),
  Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.go aig curr_2.succ n d wn wr q r =
    {
      aig :=
        (Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.go
            (Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.blastDivSubtractShift aig n d wn wr q r).aig curr_2
            (n.cast ⋯) (d.cast ⋯)
            (Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.blastDivSubtractShift aig n d wn wr q r).wn
            (Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.blastDivSubtractShift aig n d wn wr q r).wr
            (Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.blastDivSubtractShift aig n d wn wr q r).q
            (Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.blastDivSubtractShift aig n d wn wr q r).r).aig,
      q :=
        (Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.go
            (Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.blastDivSubtractShift aig n d wn wr q r).aig curr_2
            (n.cast ⋯) (d.cast ⋯)
            (Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.blastDivSubtractShift aig n d wn wr q r).wn
            (Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.blastDivSubtractShift aig n d wn wr q r).wr
            (Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.blastDivSubtractShift aig n d wn wr q r).q
            (Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.blastDivSubtractShift aig n d wn wr q r).r).q,
      r :=
        (Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.go
            (Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.blastDivSubtractShift aig n d wn wr q r).aig curr_2
            (n.cast ⋯) (d.cast ⋯)
            (Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.blastDivSubtractShift aig n d wn wr q r).wn
            (Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.blastDivSubtractShift aig n d wn wr q r).wr
            (Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.blastDivSubtractShift aig n d wn wr q r).q
            (Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.blastDivSubtractShift aig n d wn wr q r).r).r,
      hle := ⋯ }
-- Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
MeasureTheory.Lp.simpleFunc.toLp_sub : ∀ {α : Type u_1} {E : Type u_4} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E] {p : ENNReal}
  {μ : MeasureTheory.Measure α} (f g : MeasureTheory.SimpleFunc α E) (hf : MeasureTheory.MemLp (⇑f) p μ)
  (hg : MeasureTheory.MemLp (⇑g) p μ), (f - g).toLp ⋯ = f.toLp hf - g.toLp hg
-- Mathlib.Topology.Defs.Sequences
/-- A space `X` is sequentially compact if every sequence in `X` has a
converging subsequence.  -/
SeqCompactSpace : (X : Type u_1) → [TopologicalSpace X] → Prop
-- Mathlib.Algebra.Category.Ring.Topology
CommRingCat.HomTopology.isHomeomorph_precomp : ∀ {R A B : CommRingCat} [inst : TopologicalSpace ↑R] (f : A ⟶ B) [CategoryTheory.IsIso f],
  IsHomeomorph fun x => CategoryTheory.CategoryStruct.comp f x
-- Std.Data.DTreeMap.Internal.WF.Defs
Std.DTreeMap.Internal.Impl.WF.diff : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] {t₁ : Std.DTreeMap.Internal.Impl α β} {h₁ : t₁.WF}
  {t₂ : Std.DTreeMap.Internal.Impl α β}, (t₁.diff t₂ ⋯).WF
-- Init.System.IOError
IO.Error.unsupportedOperation.sizeOf_spec : ∀ (osCode : UInt32) (details : String),
  sizeOf (IO.Error.unsupportedOperation osCode details) = 1 + sizeOf osCode + sizeOf details
-- Mathlib.Algebra.Lie.Basic
LieEquiv.injective : ∀ {R : Type u} {L₁ : Type v} {L₂ : Type w} [inst : CommRing R] [inst_1 : LieRing L₁] [inst_2 : LieRing L₂]
  [inst_3 : LieAlgebra R L₁] [inst_4 : LieAlgebra R L₂] (e : L₁ ≃ₗ⁅R⁆ L₂), Function.Injective ⇑e.toLieHom
-- Mathlib.NumberTheory.Padics.RingHoms
PadicInt.norm_natCast_zmodRepr_eq_one_iff_ne : ∀ {p : ℕ} [hp_prime : Fact (Nat.Prime p)] (x : ℤ_[p]), ‖↑x.zmodRepr‖ = 1 ↔ x.zmodRepr ≠ 0
-- Mathlib.CategoryTheory.Monoidal.Bimod
Bimod.comp_whiskerRight_bimod : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Limits.HasCoequalizers C]
  [inst_3 :
    ∀ (X : C),
      CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁}
        (CategoryTheory.MonoidalCategory.tensorLeft X)]
  [inst_4 :
    ∀ (X : C),
      CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁}
        (CategoryTheory.MonoidalCategory.tensorRight X)]
  {X Y Z : CategoryTheory.Mon C} {M N P : Bimod X Y} (f : M ⟶ N) (g : N ⟶ P) (Q : Bimod Y Z),
  Bimod.whiskerRight (CategoryTheory.CategoryStruct.comp f g) Q =
    CategoryTheory.CategoryStruct.comp (Bimod.whiskerRight f Q) (Bimod.whiskerRight g Q)
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
CategoryTheory.Limits.ι_reflexiveCoequalizerIsoCoequalizer_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Functor CategoryTheory.Limits.WalkingReflexivePair C)
  [inst_1 :
    CategoryTheory.Limits.HasCoequalizer (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.left)
      (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.right)],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι F CategoryTheory.Limits.WalkingReflexivePair.zero)
      (CategoryTheory.Limits.reflexiveCoequalizerIsoCoequalizer F).hom =
    CategoryTheory.Limits.coequalizer.π (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.left)
      (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.right)
-- Std.Time.DateTime.WallTime
/-- Creates a `WallTime` from a `Second.Offset`. The epoch is 1970-01-01 00:00:00 in local
(civil) time, not UTC.
 -/
Std.Time.WallTime.ofSeconds : Std.Time.Second.Offset → Std.Time.WallTime
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
Lean.Meta.RefinedDiscrTree.ExprInfo.mk.sizeOf_spec : ∀ (expr : Lean.Expr) (bvars : List Lean.FVarId) (lctx : Lean.LocalContext) (localInsts : Lean.LocalInstances)
  (cfg : Lean.Meta.Config),
  sizeOf { expr := expr, bvars := bvars, lctx := lctx, localInsts := localInsts, cfg := cfg } =
    1 + sizeOf expr + sizeOf bvars + sizeOf lctx + sizeOf localInsts + sizeOf cfg
-- Mathlib.Topology.Algebra.ConstMulAction
Homeomorph.smul_symm_apply : ∀ {α : Type u_2} {G : Type u_4} [inst : TopologicalSpace α] [inst_1 : Group G] [inst_2 : MulAction G α]
  [inst_3 : ContinuousConstSMul G α] (γ : G) (x : α), (Homeomorph.smul γ).symm x = γ⁻¹ • x
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKeyD_modifyKey_self : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {k fallback : α} {f : β k → β k}
  (l : List ((a : α) × β a)),
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.getKeyD k (Std.Internal.List.modifyKey k f l) fallback =
      if Std.Internal.List.containsKey k l = true then k else fallback
-- Mathlib.Topology.Constructions.SumProd
Filter.Tendsto.prodMk_nhds : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {γ : Type u_5} {x : X} {y : Y}
  {f : Filter γ} {mx : γ → X} {my : γ → Y},
  Filter.Tendsto mx f (nhds x) → Filter.Tendsto my f (nhds y) → Filter.Tendsto (fun c => (mx c, my c)) f (nhds (x, y))
-- Mathlib.Topology.OpenPartialHomeomorph.Basic
OpenPartialHomeomorph.homeomorphOfImageSubsetSource_symm_apply_coe : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y) {s : Set X} {t : Set Y} (hs : s ⊆ e.source) (ht : ↑e '' s = t) (a : ↑t),
  ↑((e.homeomorphOfImageSubsetSource hs ht).symm a) = ↑e.symm ↑a
-- Mathlib.Analysis.InnerProductSpace.Basic
parallelogram_law_with_nnnorm_mul : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x y : E),
  ‖x + y‖₊ * ‖x + y‖₊ + ‖x - y‖₊ * ‖x - y‖₊ = 2 * (‖x‖₊ * ‖x‖₊ + ‖y‖₊ * ‖y‖₊)
-- Init.Data.UInt.Lemmas
UInt8.mul_comm : ∀ (a b : UInt8), a * b = b * a
-- Mathlib.RingTheory.Kaehler.Polynomial
KaehlerDifferential.mvPolynomialBasis_apply : ∀ (R : Type u) [inst : CommRing R] (σ : Type u_1) (i : σ),
  (KaehlerDifferential.mvPolynomialBasis R σ) i = (KaehlerDifferential.D R (MvPolynomial σ R)) (MvPolynomial.X i)
-- Lean.Elab.BuiltinTerm
Lean.Elab.Term.elabPrivateDecl : Lean.Elab.Term.TermElab
-- Mathlib.Analysis.CStarAlgebra.Multiplier
DoubleCentralizer.zero_toProd : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : NormedSpace 𝕜 A] [inst_3 : SMulCommClass 𝕜 A A] [inst_4 : IsScalarTower 𝕜 A A],
  DoubleCentralizer.toProd 0 = 0
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.size_alter_eq_add_one : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {k : α} {f : Option β → Option β},
  k ∉ m → (f (Std.DHashMap.Const.get? m k)).isSome = true → (Std.DHashMap.Const.alter m k f).size = m.size + 1
-- Mathlib.Topology.Connected.PathConnected
IsPathConnected.union : ∀ {X : Type u_1} [inst : TopologicalSpace X] {U V : Set X},
  IsPathConnected U → IsPathConnected V → (U ∩ V).Nonempty → IsPathConnected (U ∪ V)
-- Mathlib.SetTheory.Cardinal.Embedding
Fin.Embedding.restrictSurjective_of_add_le_natCard : ∀ {α : Type u_1} {m n : ℕ} [Finite α], m + n ≤ Nat.card α → Function.Surjective fun x => (Fin.castAddEmb n).trans x
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getD_modify : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k k' : α}
  {fallback : β} {f : β → β},
  (t.modify k f).getD k' fallback =
    if cmp k k' = Ordering.eq then (Option.map f t[k]?).getD fallback else t.getD k' fallback
-- Mathlib.CategoryTheory.Abelian.Opposite
CategoryTheory.cokernelUnopUnop_inv : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C] {A B : Cᵒᵖ}
  (g : A ⟶ B),
  (CategoryTheory.cokernelUnopUnop g).inv =
    (CategoryTheory.Limits.kernel.lift g (CategoryTheory.Limits.cokernel.π g.unop).op ⋯).unop
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
/-- The functor `(Type t)ᵒᵖ ⥤ FormalCoproduct.{w} C ⥤ FormalCoproduct.{max w t} C`
which sends a type `α` and `U : FormalCoproduct C` to `U.power α`.  -/
CategoryTheory.Limits.FormalCoproduct.powerBifunctor : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Limits.HasProducts C] →
      CategoryTheory.Functor Type tᵒᵖ
        (CategoryTheory.Functor (CategoryTheory.Limits.FormalCoproduct C) (CategoryTheory.Limits.FormalCoproduct C))
-- Init.Data.String.Modify
String.Pos.Raw.IsValid.modify_of_le : ∀ {s : String} {p : s.Pos} {f : Char → Char} {hp : p ≠ s.endPos} {q : String.Pos.Raw},
  String.Pos.Raw.IsValid s q → q ≤ p.offset → String.Pos.Raw.IsValid (p.modify f hp) q
-- Mathlib.Analysis.InnerProductSpace.Basic
innerₛₗ_apply_apply : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (v w : E), ((innerₛₗ 𝕜) v) w = inner 𝕜 v w
-- Mathlib.Topology.Maps.Proper.Basic
/-- If the composition of two continuous functions `f : X → Y` and `g : Y → Z` is proper
and `Y` is T2, then `f` is proper.  -/
isProperMap_of_comp_of_t2 : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] {f : X → Y} {g : Y → Z} [T2Space Y],
  Continuous f → Continuous g → IsProperMap (g ∘ f) → IsProperMap f