mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Nat.Internal.Linear
_private.Init.Data.Nat.Internal.Linear.0.Nat.Internal.Linear.Poly.cancelAux.match_1.eq_2 : ∀ (motive : Nat.Internal.Linear.Poly → Nat.Internal.Linear.Poly → Sort u_1) (m₂ : Nat.Internal.Linear.Poly)
  (h_1 : (m₁ : Nat.Internal.Linear.Poly) → motive m₁ []) (h_2 : (m₂ : Nat.Internal.Linear.Poly) → motive [] m₂)
  (h_3 :
    (k₁ : ℕ) →
      (v₁ : Nat.Internal.Linear.Var) →
        (m₁ : List (ℕ × Nat.Internal.Linear.Var)) →
          (k₂ : ℕ) →
            (v₂ : Nat.Internal.Linear.Var) →
              (m₂ : List (ℕ × Nat.Internal.Linear.Var)) → motive ((k₁, v₁) :: m₁) ((k₂, v₂) :: m₂)),
  (m₂ = [] → False) →
    (match [], m₂ with
      | m₁, [] => h_1 m₁
      | [], m₂ => h_2 m₂
      | (k₁, v₁) :: m₁, (k₂, v₂) :: m₂ => h_3 k₁ v₁ m₁ k₂ v₂ m₂) =
      h_2 m₂
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
SimpleGraph.IsEdgeConnected.le_degree : ∀ {V : Type u_1} {G : SimpleGraph V} {k : ℕ} {u : V} [inst : Fintype ↑(G.neighborSet u)] [Nontrivial V],
  G.IsEdgeConnected k → k ≤ G.degree u
-- Init.Data.Iterators.Consumers.Total
Std.Iter.Total.mk : {α β : Type w} → Std.Iter β → Std.Iter.Total β
-- Init.Grind.Ring.Envelope
Lean.Grind.Ring.OfSemiring.toQ_pow : ∀ {α : Type u} [inst : Lean.Grind.Semiring α] (a : α) (n : ℕ), ↑(a ^ n) = ↑a ^ n
-- Lean.Util.CollectLooseBVars
Lean.Expr.CollectLooseBVars.main : Lean.Expr → ℕ → Lean.Expr.CollectLooseBVars.M Unit
-- Mathlib.Topology.Sheaves.LocalPredicate
/-- The local predicate of being a partial section of a function.  -/
TopCat.isSection : {X : TopCat} → {T : Type u_3} → (T → ↑X) → TopCat.LocalPredicate fun x => T
-- Mathlib.ModelTheory.Graph
/-- Any simple graph can be thought of as a structure in the language of graphs.  -/
SimpleGraph.structure : {V : Type u} → SimpleGraph V → FirstOrder.Language.graph.Structure V
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
_private.Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk.0.SzemerediRegularity.sum_density_div_card_le_density_add_eps : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {P : Finpartition Finset.univ} {hP : P.IsEquipartition}
  {G : SimpleGraph α} [inst_2 : DecidableRel G.Adj] {ε : ℝ} {U V : Finset α} [Nonempty α],
  P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α →
    100 ≤ 4 ^ P.parts.card * ε ^ 5 →
      ε ≤ 1 →
        ∀ {hU : U ∈ P.parts} {hV : V ∈ P.parts} {A B : Finset (Finset α)},
          A ⊆ (SzemerediRegularity.chunk hP G ε hU).parts →
            B ⊆ (SzemerediRegularity.chunk hP G ε hV).parts →
              (∑ ab ∈ A.product B, ↑(G.edgeDensity ab.1 ab.2)) / (↑A.card * ↑B.card) ≤
                ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) + ε ^ 5 / 49
-- Mathlib.Algebra.GroupWithZero.Associated
Associated.dvdNotUnit_right_iff : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] {p q r : M}, Associated q r → (DvdNotUnit p q ↔ DvdNotUnit p r)
-- Lean.Data.Lsp.BasicAux
Lean.Lsp.instToJsonPosition : Lean.ToJson Lean.Lsp.Position
-- Mathlib.SetTheory.Ordinal.Notation
ONote.fastGrowing_zero' : ∀ (o : ONote), o.fundamentalSequence = Sum.inl none → o.fastGrowing = Nat.succ
-- Mathlib.RingTheory.Smooth.StandardSmoothCotangent
Algebra.IsStandardSmoothOfRelativeDimension.subsingleton_kaehlerDifferential : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [Algebra.IsStandardSmoothOfRelativeDimension 0 R S], Subsingleton Ω[S⁄R]
-- Init.Data.String.Basic
String.getUTF8Byte.eq_1 : ∀ (s : String) (p : String.Pos.Raw) (h : p < s.rawEndPos), s.getUTF8Byte p h = s.toByteArray[p.byteIdx]
-- Mathlib.CategoryTheory.Limits.Pi
/-- Given a family of limit cones over the `F ⋙ Pi.eval C i`,
assembling them together as a `Cone F` produces a limit cone.
 -/
CategoryTheory.pi.coneOfConeEvalIsLimit : {I : Type v₁} →
  {C : I → Type u₁} →
    [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] →
      {J : Type v₁} →
        [inst_1 : CategoryTheory.SmallCategory J] →
          {F : CategoryTheory.Functor J ((i : I) → C i)} →
            {c : (i : I) → CategoryTheory.Limits.Cone (F.comp (CategoryTheory.Pi.eval C i))} →
              ((i : I) → CategoryTheory.Limits.IsLimit (c i)) →
                CategoryTheory.Limits.IsLimit (CategoryTheory.pi.coneOfConeCompEval c)
-- Init.Internal.Order.Basic
Lean.Order.chain_iterates : ∀ {α : Sort u} [inst : Lean.Order.CCPO α] {f : α → α}, Lean.Order.monotone f → Lean.Order.chain (Lean.Order.iterates f)
-- Mathlib.Algebra.Group.Submonoid.MulOpposite
AddSubmonoid.op_eq_top : ∀ {M : Type u_2} [inst : AddZeroClass M] {S : AddSubmonoid M}, S.op = ⊤ ↔ S = ⊤
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.run_ExceptT : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {ε α : Type u} {Q : Std.Do.PostCond (Except ε α) ps}
  [inst : Std.Do.WP m ps] (x : ExceptT ε m α),
  ⦃(Std.Do.wp x).apply (fun a => Q.1 (Except.ok a), fun e => Q.1 (Except.error e), Q.2)⦄ x.run ⦃Q⦄
-- Mathlib.Algebra.Group.Basic
pow_mul_pow_sub : ∀ {M : Type u_4} [inst : Monoid M] {m n : ℕ} (a : M), m ≤ n → a ^ m * a ^ (n - m) = a ^ n
-- Batteries.Data.DList.Basic
Batteries.DList.instAppend : {α : Type u} → Append (Batteries.DList α)
-- Mathlib.Combinatorics.Colex
Finset.Colex.le_iff_sdiff_subset_lowerClosure : ∀ {α : Type u_1} [inst : PartialOrder α] {s t : Colex (Finset α)},
  s ≤ t ↔ ↑(ofColex s) \ ↑(ofColex t) ⊆ ↑(lowerClosure (↑(ofColex t) \ ↑(ofColex s)))
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.mem_adicCompletionIntegers : ∀ (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 : IsDedekindDomain.HeightOneSpectrum.adicCompletion K v},
  x ∈ IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v ↔ Valued.v x ≤ 1
-- Mathlib.Order.Sublattice
Sublattice.prod_right_mono : ∀ {α : Type u_2} {β : Type u_3} [inst : Lattice α] [inst_1 : Lattice β] {L : Sublattice α}, Monotone fun M => L.prod M
-- Mathlib.Algebra.AddConstMap.Equiv
/-- Interpret an `AddConstEquiv` as an `Equiv`.  -/
AddConstEquiv.toEquiv : {G : Type u_1} → {H : Type u_2} → [inst : Add G] → [inst_1 : Add H] → {a : G} → {b : H} → AddConstEquiv G H a b → G ≃ H
-- Init.Data.UInt.Lemmas
UInt32.ofInt_one : UInt32.ofInt 1 = 1
-- Lean.Data.Lsp.Basic
Lean.Lsp.instToJsonApplyWorkspaceEditParams : Lean.ToJson Lean.Lsp.ApplyWorkspaceEditParams
-- Mathlib.Order.Preorder.Chain
IsChain.eq_1 : ∀ {α : Type u_1} (r : α → α → Prop) (s : Set α), IsChain r s = s.Pairwise fun x y => r x y ∨ r y x
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.isLittleO_norm_norm : ∀ {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [inst : SeminormedAddCommGroup E'] [inst_1 : SeminormedAddCommGroup F']
  {f' : α → E'} {g' : α → F'} {l : Filter α}, ((fun x => ‖f' x‖) =o[l] fun x => ‖g' x‖) ↔ f' =o[l] g'
-- Mathlib.NumberTheory.NumberField.CMField
/-- The image of a root of unity by the complex conjugation is its inverse.
This is the version of `Complex.conj_rootsOfUnity` for CM-fields.
 -/
NumberField.IsCMField.complexConj_torsion : ∀ (K : Type u_1) [inst : Field K] [inst_1 : CharZero K] [inst_2 : NumberField.IsCMField K] [inst_3 : NumberField K]
  (ζ : ↥(NumberField.Units.torsion K)),
  (NumberField.IsCMField.complexConj K) ((algebraMap (NumberField.RingOfIntegers K) K) ↑↑ζ) =
    ((algebraMap (NumberField.RingOfIntegers K) K) ↑↑ζ)⁻¹
-- Lean.Parser.Command
Lean.Parser.Term.precheckedQuot.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.RingTheory.HahnSeries.PowerSeries
HahnSeries.ofPowerSeries_apply : ∀ {Γ : Type u_1} {R : Type u_2} [inst : Semiring R] [inst_1 : Semiring Γ] [inst_2 : PartialOrder Γ]
  [inst_3 : IsStrictOrderedRing Γ] (x : PowerSeries R),
  (HahnSeries.ofPowerSeries Γ R) x = HahnSeries.embDomain Nat.castOrderEmbedding (HahnSeries.toPowerSeries.symm x)
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.isDomain_of_prime : ∀ {R : Type u_1} [inst : CommRing R] {f : Polynomial R}, Prime f → IsDomain (AdjoinRoot f)
-- Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
CategoryTheory.Abelian.SpectralObject.HasSpectralSequence.isZero_H_obj_mk₁_i₀_le : ∀ {C : Type u_1} {ι : Type u_2} {κ : Type u_3} {inst : CategoryTheory.Category.{v_1, u_1} C}
  {inst_1 : CategoryTheory.Abelian C} {inst_2 : Preorder ι} {c : ℤ → ComplexShape κ} {r₀ : ℤ}
  {X : CategoryTheory.Abelian.SpectralObject C ι}
  {data : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀} [self : X.HasSpectralSequence data]
  (r r' : ℤ) (pq : κ),
  (∀ (pq' : κ), ¬(c r).Rel pq pq') →
    ∀ (n : ℤ),
      n = data.deg pq + 1 →
        ∀ (hrr' : autoParam (r + 1 = r') CategoryTheory.Abelian.SpectralObject.HasSpectralSequence._auto_1)
          (hr : autoParam (r₀ ≤ r) CategoryTheory.Abelian.SpectralObject.HasSpectralSequence._auto_3),
          CategoryTheory.Limits.IsZero ((X.H n).obj (CategoryTheory.ComposableArrows.mk₁ (CategoryTheory.homOfLE ⋯)))
-- Mathlib.GroupTheory.FreeAbelianGroup
FreeAbelianGroup.map_id_apply : ∀ {α : Type u} (x : FreeAbelianGroup α), (FreeAbelianGroup.map id) x = x
-- Lean.Meta.Tactic.Grind.Types
_private.Lean.Meta.Tactic.Grind.Types.0.Lean.Meta.Grind.PendingSolverPropagationsData.diseqs : ℕ →
  Lean.Meta.Grind.ParentSet →
    Lean.Meta.Grind.PendingSolverPropagationsData✝ → Lean.Meta.Grind.PendingSolverPropagationsData✝
-- Mathlib.GroupTheory.Coset.Defs
QuotientAddGroup.instCoeQuotientAddSubgroup : {α : Type u_1} → [inst : AddGroup α] → {s : AddSubgroup α} → Coe α (α ⧸ s)
-- Std.Data.DTreeMap.Internal.Balancing
Std.DTreeMap.Internal.Impl.doubleR.eq_1 : ∀ {α : Type u} {β : α → Type v} (k : α) (v : β k) (lk : α) (lv : β lk) (ll : Std.DTreeMap.Internal.Impl α β) (lrk : α)
  (lrv : β lrk) (lrl lrr r : Std.DTreeMap.Internal.Impl α β),
  Std.DTreeMap.Internal.Impl.doubleR k v lk lv ll lrk lrv lrl lrr r =
    Std.DTreeMap.Internal.Impl.bin lrk lrv (Std.DTreeMap.Internal.Impl.bin lk lv ll lrl)
      (Std.DTreeMap.Internal.Impl.bin k v lrr r)
-- Mathlib.Geometry.Manifold.BumpFunction
SmoothBumpFunction.eventuallyEq_one_of_dist_lt : ∀ {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M] {c : M}
  (f : SmoothBumpFunction I c) {x : M} [inst_5 : FiniteDimensional ℝ E],
  x ∈ (chartAt H c).source → dist (↑(extChartAt I c) x) (↑(extChartAt I c) c) < f.rIn → ↑f =ᶠ[nhds x] 1
-- Mathlib.Lean.EnvExtension
instInhabitedState_mathlib : {σ : Type} → [Inhabited σ] → Inhabited (Lean.ScopedEnvExtension.State σ)
-- Mathlib.Analysis.AperiodicOrder.Delone.Basic
Delone.DeloneSet.mk.congr_simp : ∀ {X : Type u_3} [inst : MetricSpace X] (carrier carrier_1 : Set X) (e_carrier : carrier = carrier_1)
  (packingRadius packingRadius_1 : NNReal) (e_packingRadius : packingRadius = packingRadius_1)
  (packingRadius_pos : 0 < packingRadius) (isSeparated_packingRadius : Metric.IsSeparated (↑packingRadius) carrier)
  (coveringRadius coveringRadius_1 : NNReal) (e_coveringRadius : coveringRadius = coveringRadius_1)
  (coveringRadius_pos : 0 < coveringRadius) (isCover_coveringRadius : Metric.IsCover coveringRadius Set.univ carrier),
  { carrier := carrier, packingRadius := packingRadius, packingRadius_pos := packingRadius_pos,
      isSeparated_packingRadius := isSeparated_packingRadius, coveringRadius := coveringRadius,
      coveringRadius_pos := coveringRadius_pos, isCover_coveringRadius := isCover_coveringRadius } =
    { carrier := carrier_1, packingRadius := packingRadius_1, packingRadius_pos := ⋯, isSeparated_packingRadius := ⋯,
      coveringRadius := coveringRadius_1, coveringRadius_pos := ⋯, isCover_coveringRadius := ⋯ }
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
CategoryTheory.IsPushout.isoIsPushout.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Z : C} (X Y : C) {P : C} {f f_1 : Z ⟶ X} (e_f : f = f_1)
  {g g_1 : Z ⟶ Y} (e_g : g = g_1) {inl inl_1 : X ⟶ P} (e_inl : inl = inl_1) {inr inr_1 : Y ⟶ P} (e_inr : inr = inr_1)
  {P' : C} {inl' inl'_1 : X ⟶ P'} (e_inl' : inl' = inl'_1) {inr' inr'_1 : Y ⟶ P'} (e_inr' : inr' = inr'_1)
  (h : CategoryTheory.IsPushout f g inl inr) (h' : CategoryTheory.IsPushout f g inl' inr'),
  CategoryTheory.IsPushout.isoIsPushout X Y h h' = CategoryTheory.IsPushout.isoIsPushout X Y ⋯ ⋯
-- Lean.Elab.Syntax
Lean.Elab.Term.ToParserDescrContext.catName : Lean.Elab.Term.ToParserDescrContext → Lean.Name
-- Mathlib.Data.Finsupp.Option
Finsupp.optionElim_ne_zero_of_left : ∀ {α : Type u_1} {M : Type u_2} [inst : Zero M] (y : M) (f : α →₀ M), y ≠ 0 → Finsupp.optionElim y f ≠ 0
-- Init.Data.List.Sublist
List.prefix_append_right_inj : ∀ {α : Type u_1} {l₁ l₂ : List α} (l : List α), l ++ l₁ <+: l ++ l₂ ↔ l₁ <+: l₂
-- Mathlib.Topology.UniformSpace.Equicontinuity
/-- A family `𝓕 : ι → X → α` is equicontinuous at `x₀` within `S` iff the function
`swap 𝓕 : X → ι → α` is continuous at `x₀` within `S`
*when `ι → α` is equipped with the topology of uniform convergence*. This is very useful for
developing the equicontinuity API, but it should not be used directly for other purposes.  -/
equicontinuousWithinAt_iff_continuousWithinAt : ∀ {ι : Type u_1} {X : Type u_3} {α : Type u_6} [tX : TopologicalSpace X] [uα : UniformSpace α] {F : ι → X → α}
  {S : Set X} {x₀ : X}, EquicontinuousWithinAt F S x₀ ↔ ContinuousWithinAt (⇑UniformFun.ofFun ∘ Function.swap F) S x₀
-- Mathlib.Order.SuccPred.Limit
/-- Predecessor limits aren't covered by any other elements.  -/
Order.IsPredLimit.isPredPrelimit : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, Order.IsPredLimit a → Order.IsPredPrelimit a
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.getD_filterMap : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {γ : Type w} {t : Std.DTreeMap α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] {f : α → β → Option γ} {k : α} {fallback : γ},
  Std.DTreeMap.Const.getD (Std.DTreeMap.filterMap f t) k fallback =
    ((Std.DTreeMap.Const.get? t k).pbind fun x h' => f (t.getKey k ⋯) x).getD fallback
-- Mathlib.Order.Bounds.Basic
isLUB_univ : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : OrderTop α], IsLUB Set.univ ⊤
-- Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
MeasureTheory.integrable_rnDeriv_smul_iff : ∀ {α : Type u_3} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} {E : Type u_4} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [μ.HaveLebesgueDecomposition ν] [MeasureTheory.SigmaFinite μ] {f : α → E},
  μ.AbsolutelyContinuous ν →
    (MeasureTheory.Integrable (fun x => (μ.rnDeriv ν x).toReal • f x) ν ↔ MeasureTheory.Integrable f μ)
-- Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
IsIntegralClosure.isTorsionFree : ∀ (R : Type u_1) {A : Type u_2} (B : Type u_3) [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : CommRing B]
  [inst_3 : Algebra R B] [inst_4 : Algebra A B] [IsIntegralClosure A R B] [inst_6 : Module R A] [IsScalarTower R A B]
  [Module.IsTorsionFree R B], Module.IsTorsionFree R A
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.getKey_modify : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp}
  [Inhabited α] {k k' : α} {f : β → β} {hc : k' ∈ Std.ExtDTreeMap.Const.modify t k f},
  (Std.ExtDTreeMap.Const.modify t k f).getKey k' hc = if cmp k k' = Ordering.eq then k else t.getKey k' ⋯
-- Mathlib.Geometry.Euclidean.Sphere.Basic
/-- The center lies on the line through two points of a sphere if and only if those
points are the endpoints of a diameter.  -/
EuclideanGeometry.Sphere.center_mem_affineSpan_pair_iff_isDiameter : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : EuclideanGeometry.Sphere P} {p₁ p₂ : P},
  p₁ ∈ s → p₂ ∈ s → (s.center ∈ line[ℝ, p₁, p₂] ↔ s.IsDiameter p₁ p₂)
-- Mathlib.Order.Preorder.Chain
Flag.symm_map : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (e : α ≃o β),
  (Flag.map e).symm = Flag.map e.symm
-- Init.Data.Slice.Basic
Std.Slice.mk.inj : ∀ {γ : Type u} {internalRepresentation internalRepresentation_1 : γ},
  { internalRepresentation := internalRepresentation } = { internalRepresentation := internalRepresentation_1 } →
    internalRepresentation = internalRepresentation_1
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.registerCustomErrorIfMVar : Lean.Expr → Lean.Syntax → Lean.MessageData → Lean.Elab.TermElabM Unit
-- Init.Data.Nat.Basic
/-- Alias for `Nat.lt_asymm`.  -/
Nat.not_lt_of_gt : ∀ {a b : ℕ}, a < b → ¬b < a
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.induce_mono_left : ∀ {V : Type u} {G : SimpleGraph V} {G' G'' : G.Subgraph} {s : Set V}, G' ≤ G'' → G'.induce s ≤ G''.induce s
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrp.trivial_addGrp_zero : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C],
  CategoryTheory.AddMonObj.zero = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.isEmpty_insertMany_empty_list : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} [Std.TransOrd α] {l : List ((a : α) × β a)},
  (↑(Std.DTreeMap.Internal.Impl.empty.insertMany l ⋯)).isEmpty = l.isEmpty
-- Mathlib.RepresentationTheory.Subrepresentation
Subrepresentation.coe_sup : ∀ {A : Type u_1} {G : Type u_2} {W : Type u_3} [inst : Semiring A] [inst_1 : Monoid G] [inst_2 : AddCommMonoid W]
  [inst_3 : Module A W] {ρ : Representation A G W} (ρ₁ ρ₂ : Subrepresentation ρ), ↑(ρ₁ ⊔ ρ₂) = ↑ρ₁ + ↑ρ₂
-- Mathlib.RingTheory.Artinian.Module
IsArtinian.exists_pow_succ_smul_dvd : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [IsArtinian R M] (r : R) (x : M), ∃ n y, r ^ n.succ • y = r ^ n • x
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.maxKey?_erase!_eq_of_not_compare_eq_maxKey? : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF →
    ∀ {k : α},
      (∀ {km : α}, t.maxKey? = some km → ¬compare k km = Ordering.eq) →
        (Std.DTreeMap.Internal.Impl.erase! k t).maxKey? = t.maxKey?
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.PrettyPrinter.Delaborator.TopDownAnalyze.containsBadMax : Lean.Level → Bool
-- Mathlib.CategoryTheory.LocallyCartesianClosed.Over
CategoryTheory.ChosenPullbacksAlong.Over.lift_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.ChosenPullbacks C] {X : C}
  {W Y Z : CategoryTheory.Over X} (f : W ⟶ Y) (g : W ⟶ Z),
  CategoryTheory.Over.Hom.left (CategoryTheory.CartesianMonoidalCategory.lift f g) =
    CategoryTheory.ChosenPullbacksAlong.lift (CategoryTheory.Over.Hom.left f) (CategoryTheory.Over.Hom.left g) ⋯
-- Std.Time.Date.Basic
Std.Time.instHAddOffsetOffset_16 : HAdd Std.Time.Second.Offset Std.Time.Day.Offset Std.Time.Second.Offset
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
/-- `Matrix.toLinearMapₛₗ₂ b₁ b₂` is the equivalence between `R`-sesquilinear maps
`M₁ →ₛₗ[σ₁] M₂ →ₗ[R] N₂` and `n`-by-`m` matrices with entries in `N₂`,
if `b₁` and `b₂` are `R`-bases for `M₁` and `M₂`,
respectively; this is the reverse direction of `LinearMap.toMatrix₂ b₁ b₂`.  -/
Matrix.toLinearMapₛₗ₂ : {R : Type u_1} →
  {M₁ : Type u_6} →
    {M₂ : Type u_7} →
      {N₂ : Type u_10} →
        {n : Type u_11} →
          {m : Type u_12} →
            [inst : CommSemiring R] →
              [inst_1 : AddCommMonoid M₁] →
                [inst_2 : Module R M₁] →
                  [inst_3 : AddCommMonoid M₂] →
                    [inst_4 : Module R M₂] →
                      [inst_5 : AddCommMonoid N₂] →
                        [inst_6 : Module R N₂] →
                          (σ₁ : R →+* R) →
                            [Fintype n] →
                              [Fintype m] →
                                [DecidableEq m] →
                                  [DecidableEq n] →
                                    Module.Basis n R M₁ →
                                      Module.Basis m R M₂ → Matrix n m N₂ ≃ₗ[R] M₁ →ₛₗ[σ₁] M₂ →ₗ[R] N₂
-- Init.Control.Lawful.Lemmas
map_inj_right : ∀ {m : Type u_1 → Type u_2} {α β : Type u_1} [inst : Monad m] [LawfulMonad m] {f : α → β},
  (∀ {x y : α}, f x = f y → x = y) → ∀ {x y : m α}, f <$> x = f <$> y ↔ x = y
-- Mathlib.RingTheory.Unramified.LocalStructure
/-- [Stacks Tag 00UE](https://stacks.math.columbia.edu/tag/00UE) -/
Algebra.IsEtaleAt.exists_isStandardEtale : ∀ {R : Type u_1} {S : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (Q : Ideal S)
  [inst_3 : Q.IsPrime] [Algebra.FinitePresentation R S] [Algebra.IsEtaleAt R Q],
  ∃ f ∉ Q, Algebra.IsStandardEtale R (Localization.Away f)
-- Mathlib.Analysis.Fourier.LpSpace
/-- The `𝓢'`-Fourier transform and the `L2`-Fourier transform coincide on `L2`.  -/
MeasureTheory.Lp.fourier_toTemperedDistribution_eq : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : MeasurableSpace E] [inst_2 : BorelSpace E]
  [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace ℂ F] [inst_5 : CompleteSpace F]
  [inst_6 : InnerProductSpace ℝ E] [inst_7 : FiniteDimensional ℝ E] (f : ↥(MeasureTheory.Lp F 2 MeasureTheory.volume)),
  FourierTransform.fourier (MeasureTheory.Lp.toTemperedDistribution f) =
    MeasureTheory.Lp.toTemperedDistribution (FourierTransform.fourier f)
-- Mathlib.Topology.MetricSpace.IsometricSMul
IsometryEquiv.addRight.eq_1 : ∀ {G : Type v} [inst : AddGroup G] [inst_1 : PseudoEMetricSpace G] [inst_2 : IsIsometricVAdd Gᵃᵒᵖ G] (c : G),
  IsometryEquiv.addRight c = { toEquiv := Equiv.addRight c, isometry_toFun := ⋯ }
-- Mathlib.Combinatorics.Additive.VerySmallDoubling
_private.Mathlib.Combinatorics.Additive.VerySmallDoubling.0.Finset.A_subset_aH : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] {A : Finset G}, ∀ a ∈ A, A ⊆ a • (A⁻¹ * A)
-- Mathlib.Data.DFinsupp.Module
DFinsupp.coe_smul : ∀ {ι : Type u} {γ : Type w} {β : ι → Type v} [inst : (i : ι) → Zero (β i)] [inst_1 : (i : ι) → SMulZeroClass γ (β i)]
  (b : γ) (v : Π₀ (i : ι), β i), ⇑(b • v) = b • ⇑v
-- Lean.Parser.Types
Lean.Parser.ParserContextCore.mk.sizeOf_spec : ∀ (toInputContext : Lean.Parser.InputContext) (toParserModuleContext : Lean.Parser.ParserModuleContext)
  (toCacheableParserContext : Lean.Parser.CacheableParserContext) (tokens : Lean.Parser.TokenTable),
  sizeOf
      { toInputContext := toInputContext, toParserModuleContext := toParserModuleContext,
        toCacheableParserContext := toCacheableParserContext, tokens := tokens } =
    1 + sizeOf toInputContext + sizeOf toParserModuleContext + sizeOf toCacheableParserContext + sizeOf tokens
-- Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
CategoryTheory.regularTopology.equalizerConditionMap_iff_nonempty_isLimit : ∀ {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] (P : CategoryTheory.Functor Cᵒᵖ D) ⦃X B : C⦄ (π : X ⟶ B)
  [CategoryTheory.Limits.HasPullback π π],
  CategoryTheory.regularTopology.SingleEqualizerCondition P π ↔
    Nonempty
      (CategoryTheory.Limits.IsLimit
        (P.mapCone (CategoryTheory.Sieve.ofArrows (fun x => X) fun x => π).arrows.cocone.op))
-- Mathlib.Data.ENNReal.Basic
ENNReal.coe_ofNat : ∀ (n : ℕ) [inst : n.AtLeastTwo], ↑(OfNat.ofNat n) = OfNat.ofNat n
-- Lean.DocString.Parser
Lean.Doc.Parser.OrderedListType.ofNat_ctorIdx : ∀ (x : Lean.Doc.Parser.OrderedListType), Lean.Doc.Parser.OrderedListType.ofNat x.ctorIdx = x
-- Mathlib.Topology.Homeomorph.Lemmas
/-- A map is a homeomorphism iff it is continuous, closed and bijective.  -/
isHomeomorph_iff_continuous_isClosedMap_bijective : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  IsHomeomorph f ↔ Continuous f ∧ IsClosedMap f ∧ Function.Bijective f