mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.AdicCompletion.Functoriality
AdicCompletion.map_ext'_iff : ∀ {R : Type u_1} [inst : CommRing R] {I : Ideal R} {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {T : Type u_5} [inst_3 : AddCommGroup T] [inst_4 : Module (AdicCompletion I R) T]
  {f g : AdicCompletion I M →ₗ[AdicCompletion I R] T},
  f = g ↔ ∀ (a : AdicCompletion.AdicCauchySequence I M), f ((AdicCompletion.mk I M) a) = g ((AdicCompletion.mk I M) a)
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
ModuleCat.ExtendRestrictScalarsAdj.unit_app : ∀ {R : Type u₁} {S : Type u₂} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) (x : ModuleCat R),
  (ModuleCat.ExtendRestrictScalarsAdj.unit f).app x = ModuleCat.ExtendRestrictScalarsAdj.Unit.map f
-- Mathlib.Topology.FiberPartition
TopologicalSpace.Fiber.sigmaIncl.eq_1 : ∀ {S : Type u_1} {Y : Type u_2} (f : S → Y) [inst : TopologicalSpace S] (a : Function.Fiber f),
  TopologicalSpace.Fiber.sigmaIncl f a = { toFun := fun x => ↑x, continuous_toFun := ⋯ }
-- Mathlib.RingTheory.Congruence.Defs
RingConGen.Rel.below.add : ∀ {R : Type u_1} [inst : Add R] [inst_1 : Mul R] {r : R → R → Prop}
  {motive : (a a_1 : R) → RingConGen.Rel r a a_1 → Prop} {w x y z : R} (a : RingConGen.Rel r w x)
  (a_1 : RingConGen.Rel r y z),
  RingConGen.Rel.below a → motive w x a → RingConGen.Rel.below a_1 → motive y z a_1 → RingConGen.Rel.below ⋯
-- Mathlib.Computability.AkraBazzi.SumTransform
AkraBazziRecurrence.max_bi_le : ∀ {α : Type u_1} [inst : Finite α] [inst_1 : Nonempty α] {b : α → ℝ} (i : α), b i ≤ b (AkraBazziRecurrence.max_bi b)
-- Mathlib.Algebra.Order.Archimedean.Class
MulArchimedeanClass.mem_subgroup_iff : ∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M] {a : M}
  {s : UpperSet (MulArchimedeanClass M)}, s ≠ ⊤ → (a ∈ MulArchimedeanClass.subgroup s ↔ MulArchimedeanClass.mk a ∈ s)
-- Mathlib.LinearAlgebra.SpecialLinearGroup
SpecialLinearGroup.ext_iff : ∀ {R : Type u_1} {V : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup V] [inst_2 : Module R V]
  (u v : SpecialLinearGroup R V), u = v ↔ ∀ (x : V), (fun x => ↑u x) x = (fun x => ↑v x) x
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.mem_unitOfList : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α] {l : List α} {k : α},
  k ∈ Std.DHashMap.Raw.Const.unitOfList l ↔ l.contains k = true
-- Mathlib.Analysis.Distribution.TemperedDistribution
MeasureTheory.Lp.toTemperedDistribution_apply : ∀ {E : Type u_3} {F : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℂ F] [inst_4 : CompleteSpace F] [inst_5 : MeasurableSpace E] [inst_6 : BorelSpace E]
  {μ : MeasureTheory.Measure E} [hμ : μ.HasTemperateGrowth] {p : ENNReal} [hp : Fact (1 ≤ p)]
  (f : ↥(MeasureTheory.Lp F p μ)) (g : SchwartzMap E ℂ),
  (MeasureTheory.Lp.toTemperedDistribution f) g = ∫ (x : E), g x • ↑↑f x ∂μ
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.max!_eq_maxD_default : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] [inst_1 : Inhabited α],
  t.max! = t.maxD default
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.eLpNormEssSup_count : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {ε : Type u_8} [inst : ENorm ε] [MeasurableSingletonClass α] (f : α → ε),
  MeasureTheory.eLpNormEssSup f MeasureTheory.Measure.count = ⨆ a, ‖f a‖ₑ
-- Mathlib.Data.List.Cycle
List.next_getElem : ∀ {α : Type u_1} [inst : DecidableEq α] (l : List α),
  l.Nodup → ∀ (i : ℕ) (hi : i < l.length), l.next l[i] ⋯ = l[(i + 1) % l.length]
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.maxD_le : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp],
  t.isEmpty = false → ∀ {k fallback : α}, (cmp (t.maxD fallback) k).isLE = true ↔ ∀ k' ∈ t, (cmp k' k).isLE = true
-- Mathlib.NumberTheory.PrimeCounting
Nat.primesBelow_eq_filter_Ico_two : ∀ (n : ℕ), n.primesBelow = Finset.filter Nat.Prime (Finset.Ico 2 n)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.pullbackProdSndIsoProd_hom_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) (Z : C)
  [inst_1 : CategoryTheory.Limits.HasBinaryProduct Z Y] [inst_2 : CategoryTheory.Limits.HasBinaryProduct Z X]
  [inst_3 : CategoryTheory.Limits.HasPullback CategoryTheory.Limits.prod.snd f],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackProdSndIsoProd f Z).hom
      CategoryTheory.Limits.prod.snd =
    CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.prod.snd f
-- Mathlib.NumberTheory.Padics.PadicIntegers
/-- The `p`-adic integers as a subring of `ℚ_[p]`.  -/
PadicInt.subring : (p : ℕ) → [hp : Fact (Nat.Prime p)] → Subring ℚ_[p]
-- Mathlib.Order.SupClosed
InfClosed.eq_1 : ∀ {α : Type u_3} [inst : SemilatticeInf α] (s : Set α), InfClosed s = ∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ s → a ⊓ b ∈ s
-- Mathlib.Topology.UniformSpace.Defs
UniformSpace.ext_iff : ∀ {α : Type ua} {u₁ u₂ : UniformSpace α}, u₁ = u₂ ↔ ∀ (s : Set (α × α)), s ∈ uniformity α ↔ s ∈ uniformity α
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarSubalgebra.instInhabited : {R : Type u} →
  {A : Type v} →
    [inst : CommSemiring R] →
      [inst_1 : NonUnitalNonAssocSemiring A] →
        [inst_2 : Module R A] → [inst_3 : Star A] → (S : NonUnitalStarSubalgebra R A) → Inhabited ↥S
-- Mathlib.Data.EReal.Basic
EReal.zero_ne_bot : 0 ≠ ⊥
-- Mathlib.CategoryTheory.Comma.Over.StrictInitial
CategoryTheory.underEquivOfIsTerminal_unitIso : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Limits.HasStrictTerminalObjects C] (X : C) (h : CategoryTheory.Limits.IsTerminal X),
  (CategoryTheory.underEquivOfIsTerminal.{w, v_1, u_1} X h).unitIso =
    CategoryTheory.NatIso.ofComponents (fun A => CategoryTheory.Under.isoMk (CategoryTheory.asIso A.hom).symm ⋯) ⋯
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometry.mk.congr_simp : ∀ {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [inst : NormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup V] [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P]
  [inst_4 : NormedAddTorsor V P] [inst_5 : SeminormedAddCommGroup V₂] [inst_6 : NormedSpace 𝕜 V₂]
  [inst_7 : PseudoMetricSpace P₂] [inst_8 : NormedAddTorsor V₂ P₂] (toAffineMap toAffineMap_1 : P →ᵃ[𝕜] P₂)
  (e_toAffineMap : toAffineMap = toAffineMap_1) (norm_map : ∀ (x : V), ‖toAffineMap.linear x‖ = ‖x‖),
  { toAffineMap := toAffineMap, norm_map := norm_map } = { toAffineMap := toAffineMap_1, norm_map := ⋯ }
-- Mathlib.CategoryTheory.Monoidal.Action.Opposites
CategoryTheory.MonoidalCategory.MonoidalLeftAction.leftActionOfOppositeLeftAction_actionHom : ∀ (C : Type u_1) (D : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction Cᵒᵖ Dᵒᵖ] {c c' : C} {d d_1 : D} (f : c ⟶ c')
  (g : d ⟶ d_1),
  CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHom f g =
    (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHom f.op g.op).unop
-- Mathlib.Topology.Constructions.SumProd
/-- **Alias** of `Continuous.curry_left`.

---

Continuous functions on products are continuous in their first argument  -/
Continuous.along_fst : ∀ {X : Type u} {Y : Type v} {Z : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] {f : X × Y → Z}, Continuous f → ∀ {y : Y}, Continuous fun x => f (x, y)
-- Lean.Data.JsonRpc
Lean.JsonRpc.MessageMetaData.response.inj : ∀ {id id_1 : Lean.JsonRpc.RequestID},
  Lean.JsonRpc.MessageMetaData.response id = Lean.JsonRpc.MessageMetaData.response id_1 → id = id_1
-- Mathlib.GroupTheory.Goursat
Subgroup.goursatFst_prod_goursatSnd_le : ∀ {G : Type u_1} {H : Type u_2} [inst : Group G] [inst_1 : Group H] (I : Subgroup (G × H)),
  I.goursatFst.prod I.goursatSnd ≤ I
-- Lean.Meta.InferType
_private.Lean.Meta.InferType.0.Lean.Meta.ArrowPropResult.undef.sizeOf_spec : sizeOf Lean.Meta.ArrowPropResult.undef✝ = 1
-- Mathlib.Topology.ContinuousMap.Algebra
/-- A version of `Set.SeparatesPoints` for subalgebras of the continuous functions,
used for stating the Stone-Weierstrass theorem.
 -/
Subalgebra.SeparatesPoints : {α : Type u_1} →
  [inst : TopologicalSpace α] →
    {R : Type u_2} →
      [inst_1 : CommSemiring R] →
        {A : Type u_3} →
          [inst_2 : TopologicalSpace A] →
            [inst_3 : Semiring A] →
              [inst_4 : Algebra R A] → [inst_5 : IsTopologicalSemiring A] → Subalgebra R C(α, A) → Prop
-- Mathlib.Algebra.MonoidAlgebra.Basic
MonoidAlgebra.liftNCRingHom.eq_1 : ∀ {k : Type u₁} {G : Type u₂} {R : Type u_2} [inst : Semiring k] [inst_1 : Monoid G] [inst_2 : Semiring R] (f : k →+* R)
  (g : G →* R) (h_comm : ∀ (x : k) (y : G), Commute (f x) (g y)),
  MonoidAlgebra.liftNCRingHom f g h_comm =
    { toFun := (↑(MonoidAlgebra.liftNC ↑f ⇑g)).toFun, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.Topology.Algebra.Group.Basic
nhds_zero_symm : ∀ (G : Type w) [inst : TopologicalSpace G] [inst_1 : AddGroup G] [IsTopologicalAddGroup G],
  Filter.comap Neg.neg (nhds 0) = nhds 0
-- Init.Data.Vector.Lemmas
_private.Init.Data.Vector.Lemmas.0.Array.isEqv.eq_1 : ∀ {α : Type u} (xs ys : Array α) (p : α → α → Bool),
  xs.isEqv ys p = if h : xs.size = ys.size then xs.isEqvAux ys h p xs.size ⋯ else false
-- Mathlib.CategoryTheory.Adjunction.Limits
CategoryTheory.Functor.instPreservesLimitsOfSizeOfIsRightAdjoint : ∀ {C : Type u_2} {D : Type u_3} [inst : CategoryTheory.Category.{v_2, u_2} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} D] (F : CategoryTheory.Functor C D) [F.IsRightAdjoint],
  CategoryTheory.Limits.PreservesLimitsOfSize.{v, u, v_2, v_3, u_2, u_3} F
-- Init.Grind.Config
Lean.Grind.GrobnerConfig.mk.injEq : ∀ (toNoopConfig toNoopConfig_1 : Lean.Grind.NoopConfig),
  ({ toNoopConfig := toNoopConfig } = { toNoopConfig := toNoopConfig_1 }) = (toNoopConfig = toNoopConfig_1)
-- Mathlib.Order.Notation
Min.ext : ∀ {α : Type u} {x y : Min α}, min = min → x = y
-- Mathlib.RingTheory.OrderOfVanishing.Noetherian
Ring.ordFrac_eq_valuation_inv : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsDiscreteValuationRing R] {K : Type u_2}
  [inst_3 : Field K] [inst_4 : Algebra R K] [inst_5 : IsFractionRing R K] (x : K),
  (Ring.ordFrac R) x = ((IsDedekindDomain.HeightOneSpectrum.valuation K (IsDiscreteValuationRing.maximalIdeal R)) x)⁻¹
-- Mathlib.Analysis.Normed.Group.Constructions
Pi.seminormedCommGroup.eq_1 : ∀ {ι : Type u_1} {G : ι → Type u_4} [inst : Fintype ι] [inst_1 : (i : ι) → SeminormedCommGroup (G i)],
  Pi.seminormedCommGroup =
    { toNorm := Pi.seminormedGroup.toNorm, toGroup := Pi.seminormedGroup.toGroup, mul_comm := ⋯,
      toPseudoMetricSpace := Pi.seminormedGroup.toPseudoMetricSpace, dist_eq := ⋯ }
-- Init.Data.SInt.Basic
/-- Bitwise or for 64-bit signed integers. Usually accessed via the `|||` operator.

Each bit of the resulting integer is set if at least one of the corresponding bits of the input
integers is set, according to the two's complement representation.

This function is overridden at runtime with an efficient implementation.
 -/
Int64.lor : Int64 → Int64 → Int64
-- Mathlib.CategoryTheory.MorphismProperty.Representable
CategoryTheory.MorphismProperty.relative_isStableUnderBaseChange : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} (P : CategoryTheory.MorphismProperty C),
  (CategoryTheory.MorphismProperty.relative F P).IsStableUnderBaseChange
-- Mathlib.CategoryTheory.Monad.Equalizer
CategoryTheory.Comonad.beckCoalgebraFork.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Comonad C} (X : T.Coalgebra),
  CategoryTheory.Comonad.beckCoalgebraFork X =
    CategoryTheory.Limits.Fork.ofι (CategoryTheory.Comonad.CofreeEqualizer.ι X) ⋯
-- Mathlib.Logic.Equiv.Prod
Equiv.sumProdDistrib_apply_left : ∀ {α : Type u_9} {β : Type u_10} {γ : Type u_11} (a : α) (c : γ),
  (Equiv.sumProdDistrib α β γ) (Sum.inl a, c) = Sum.inl (a, c)
-- Mathlib.Order.Lattice
ULift.instSemilatticeInf : {α : Type u} → [SemilatticeInf α] → SemilatticeInf (ULift.{v, u} α)
-- Mathlib.Order.WellFounded
WellFounded.lt_sup : ∀ {α : Type u_1} {r : α → α → Prop} (wf : WellFounded r) {s : Set α} (h : Set.Bounded r s) {x : α},
  x ∈ s → r x (wf.sup s h)
-- Mathlib.NumberTheory.Padics.PadicNumbers
Padic.denseRange_ratCast : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)], DenseRange Rat.cast
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.coe_symm_comp_coe : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁}
  [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [inst_4 : TopologicalSpace M₁]
  [inst_5 : AddCommMonoid M₁] {M₂ : Type u_5} [inst_6 : TopologicalSpace M₂] [inst_7 : AddCommMonoid M₂]
  [inst_8 : Module R₁ M₁] [inst_9 : Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂), ↑e.symm ∘SL ↑e = ContinuousLinearMap.id R₁ M₁
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.size_diff_le_size_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp],
  (t₁ \ t₂).size ≤ t₁.size
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Series
/-- The power series expansion of `Complex.cosh`.  -/
Complex.hasSum_cosh : ∀ (z : ℂ), HasSum (fun n => z ^ (2 * n) / ↑(2 * n).factorial) (Complex.cosh z)
-- Mathlib.CategoryTheory.Monoidal.Grp
/-- A monoid object with invertible homs is a group object.  -/
CategoryTheory.GrpObj.ofInvertible : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      (G : C) → [inst_2 : CategoryTheory.MonObj G] → ((X : C) → (f : X ⟶ G) → Invertible f) → CategoryTheory.GrpObj G
-- Mathlib.Combinatorics.Enumerative.DyckWord
DyckWord.mk : (toList : List DyckStep) →
  List.count DyckStep.U toList = List.count DyckStep.D toList →
    (∀ (i : ℕ), List.count DyckStep.D (List.take i toList) ≤ List.count DyckStep.U (List.take i toList)) → DyckWord
-- Mathlib.Analysis.Normed.Field.Basic
/-- The norm is multiplicative.  -/
NormedDivisionRing.norm_mul : ∀ {α : Type u_5} [self : NormedDivisionRing α] (a b : α), ‖a * b‖ = ‖a‖ * ‖b‖
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.mem_closure_image_of : ∀ {R : Type u} {S : Type v} [inst : NonAssocRing R] [inst_1 : NonAssocRing S] (f : R →+* S) {s : Set R} {x : R},
  x ∈ Subring.closure s → f x ∈ Subring.closure (⇑f '' s)
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
CFC.cfcₙ_rpowIntegrand₀₁_eq_cfcₙ_rpowIntegrand₀₁_one : ∀ {A : Type u_1} [inst : NonUnitalNormedRing A] [inst_1 : StarRing A] [inst_2 : NormedSpace ℝ A]
  [inst_3 : SMulCommClass ℝ A A] [inst_4 : IsScalarTower ℝ A A] [inst_5 : PartialOrder A] [StarOrderedRing A]
  [NonnegSpectrumClass ℝ A] [inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] {p t : ℝ},
  p ∈ Set.Ioo 0 1 →
    0 < t → ∀ (a : A), 0 ≤ a → cfcₙ (p.rpowIntegrand₀₁ t) a = t ^ (p - 1) • cfcₙ (p.rpowIntegrand₀₁ 1) (t⁻¹ • a)
-- Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling
SimpleGraph.EdgeLabeling.pairwiseDisjoint_univ_labelGraph : ∀ {V : Type u_1} {G : SimpleGraph V} {K : Type u_3} {C : G.EdgeLabeling K}, Set.univ.PairwiseDisjoint C.labelGraph
-- Mathlib.Topology.Order.WithTop
WithTop.neTopHomeomorph.eq_1 : ∀ (ι : Type u_1) [inst : LinearOrder ι] [inst_1 : TopologicalSpace ι] [inst_2 : OrderTopology ι],
  WithTop.neTopHomeomorph ι = { toEquiv := Equiv.withTopSubtypeNe, continuous_toFun := ⋯, continuous_invFun := ⋯ }
-- Init.Internal.Order.Lemmas
_private.Init.Internal.Order.Lemmas.0.Array.findSomeRevM?.find.match_1.eq_1 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (val : β) (h_1 : (val : β) → motive (some val))
  (h_2 : Unit → motive none),
  (match some val with
    | some val => h_1 val
    | none => h_2 ()) =
    h_1 val
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddEquiv.instInhabited.eq_1 : ∀ (M : Type u_1) [inst : TopologicalSpace M] [inst_1 : Add M],
  ContinuousAddEquiv.instInhabited M = { default := ContinuousAddEquiv.refl M }
-- Mathlib.Algebra.Group.Pi.Lemmas
Sigma.curry_mulSingle : ∀ {α : Type u_5} {β : α → Type u_6} {γ : (a : α) → β a → Type u_7} [inst : DecidableEq α]
  [inst_1 : (a : α) → DecidableEq (β a)] [inst_2 : (a : α) → (b : β a) → One (γ a b)] (i : (a : α) × β a)
  (x : γ i.fst i.snd), Sigma.curry (Pi.mulSingle i x) = Pi.mulSingle i.fst (Pi.mulSingle i.snd x)
-- Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
/-- **Alias** of `ContinuousLinearMap.postcompUniformConvergenceCLM_apply`. -/
ContinuousLinearMap.postcomp_uniformConvergenceCLM_apply : ∀ {𝕜₁ : Type u_6} {𝕜₂ : Type u_7} {𝕜₃ : Type u_8} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂]
  [inst_2 : NormedField 𝕜₃] {σ : 𝕜₁ →+* 𝕜₂} {τ : 𝕜₂ →+* 𝕜₃} {ρ : 𝕜₁ →+* 𝕜₃} [inst_3 : RingHomCompTriple σ τ ρ]
  {E : Type u_9} {F : Type u_10} {G : Type u_11} [inst_4 : AddCommGroup E] [inst_5 : Module 𝕜₁ E]
  [inst_6 : AddCommGroup F] [inst_7 : Module 𝕜₂ F] [inst_8 : AddCommGroup G] [inst_9 : Module 𝕜₃ G]
  [inst_10 : TopologicalSpace E] [inst_11 : TopologicalSpace F] [inst_12 : TopologicalSpace G] (𝔖 : Set (Set E))
  [inst_13 : IsTopologicalAddGroup F] [inst_14 : IsTopologicalAddGroup G] [inst_15 : ContinuousConstSMul 𝕜₃ G]
  [inst_16 : ContinuousConstSMul 𝕜₂ F] (L : F →SL[τ] G) (f : UniformConvergenceCLM σ F 𝔖),
  (ContinuousLinearMap.postcompUniformConvergenceCLM 𝔖 L) f = L ∘SL f
-- Mathlib.Data.Nat.Prime.Basic
/-- **Alias** of the reverse direction of `Nat.coprime_two_right`. -/
Odd.coprime_two_right : ∀ {n : ℕ}, Odd n → n.Coprime 2
-- Init.Data.SInt.Lemmas
Int16.toInt8_toISize : ∀ (n : Int16), n.toISize.toInt8 = n.toInt8
-- Mathlib.FieldTheory.Galois.GaloisClosure
FiniteGaloisIntermediateField.isGalois : ∀ {k : Type u_1} {K : Type u_2} [inst : Field k] [inst_1 : Field K] [inst_2 : Algebra k K]
  (self : FiniteGaloisIntermediateField k K), IsGalois k ↥self.toIntermediateField
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.LetValue.fap.injEq : ∀ {pu : Lean.Compiler.LCNF.Purity} (fn : Lean.Name) (args : Array (Lean.Compiler.LCNF.Arg pu))
  (h : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.LetValue._auto_13) (fn_1 : Lean.Name)
  (args_1 : Array (Lean.Compiler.LCNF.Arg pu))
  (h_1 : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.LetValue._auto_13),
  (Lean.Compiler.LCNF.LetValue.fap fn args h = Lean.Compiler.LCNF.LetValue.fap fn_1 args_1 h_1) =
    (fn = fn_1 ∧ args = args_1)
-- Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
/-- The gluing as sheafed spaces is isomorphic to the gluing as presheafed spaces.  -/
AlgebraicGeometry.SheafedSpace.GlueData.isoPresheafedSpace : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (D : AlgebraicGeometry.SheafedSpace.GlueData C) →
      [inst_1 : CategoryTheory.Limits.HasLimits C] → D.glued.toPresheafedSpace ≅ D.toPresheafedSpaceGlueData.glued
-- Mathlib.Analysis.Distribution.SchwartzSpace.Deriv
SchwartzMap.hasFDerivAt : ∀ {E : Type u_5} {F : Type u_8} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace ℝ F]
  [inst_3 : NormedSpace ℝ E] (f : SchwartzMap E F) (x : E), HasFDerivAt (⇑f) (fderiv ℝ (⇑f) x) x
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokenType.comment.sizeOf_spec : sizeOf Lean.Lsp.SemanticTokenType.comment = 1
-- Mathlib.Algebra.Group.Subgroup.Basic
AddGroup.subset_addConjugatesOfSet : ∀ {G : Type u_1} [inst : AddGroup G] {s : Set G}, s ⊆ AddGroup.addConjugatesOfSet s
-- Mathlib.MeasureTheory.Group.Arithmetic
Pi.measurableVAdd : ∀ {M : Type u_2} [inst : MeasurableSpace M] {ι : Type u_6} {α : ι → Type u_7} [inst_1 : (i : ι) → VAdd M (α i)]
  [inst_2 : (i : ι) → MeasurableSpace (α i)] [∀ (i : ι), MeasurableVAdd M (α i)], MeasurableVAdd M ((i : ι) → α i)
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.derivWeierstrassPExcept_of_notMem : ∀ (L : PeriodPair), ∀ l₀ ∉ L.lattice, L.derivWeierstrassPExcept l₀ = L.derivWeierstrassP
-- Mathlib.Algebra.Homology.ShortComplex.ModuleCat
CategoryTheory.ShortComplex.Exact.moduleCat_range_eq_ker : ∀ {R : Type u} [inst : Ring R] {S : CategoryTheory.ShortComplex (ModuleCat R)},
  S.Exact → (ModuleCat.Hom.hom S.f).range = (ModuleCat.Hom.hom S.g).ker
-- Mathlib.Algebra.Module.Equiv.Defs
LinearEquiv.invFun_eq_symm : ∀ {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂}
  {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M ≃ₛₗ[σ] M₂),
  e.invFun = ⇑e.symm
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.RuleExpr.toAdditionalGlobalRules : {m : Type → Type} →
  [Monad m] → [Lean.MonadError m] → Option Lean.Name → Aesop.Frontend.RuleExpr → m (Array Aesop.Frontend.RuleConfig)
-- Init.Data.Vector.Attach
Vector.back?_pmap : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} {P : α → Prop} {f : (a : α) → P a → β} {xs : Vector α n} (H : ∀ a ∈ xs, P a),
  (Vector.pmap f xs H).back? =
    Option.map
      (fun x =>
        match x with
        | ⟨a, m⟩ => f a ⋯)
      xs.attach.back?
-- Mathlib.Logic.Embedding.Basic
Function.Embedding.mk.injEq : ∀ {α : Sort u_1} {β : Sort u_2} (toFun : α → β) (inj' : Function.Injective toFun) (toFun_1 : α → β)
  (inj'_1 : Function.Injective toFun_1),
  ({ toFun := toFun, inj' := inj' } = { toFun := toFun_1, inj' := inj'_1 }) = (toFun = toFun_1)
-- Mathlib.Analysis.Asymptotics.ExpGrowth
ExpGrowth.expGrowthSup_comp_le : ∀ {u : ℕ → ENNReal} {v : ℕ → ℕ},
  (∃ᶠ (n : ℕ) in Filter.atTop, 1 ≤ u n) →
    (LinearGrowth.linearGrowthSup fun n => ↑(v n)) ≠ 0 →
      (LinearGrowth.linearGrowthSup fun n => ↑(v n)) ≠ ⊤ →
        Filter.Tendsto v Filter.atTop Filter.atTop →
          ExpGrowth.expGrowthSup (u ∘ v) ≤ (LinearGrowth.linearGrowthSup fun n => ↑(v n)) * ExpGrowth.expGrowthSup u
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.UInt
UInt8.reduceOfNatLT : Lean.Meta.Simp.DSimproc
-- Mathlib.Combinatorics.Graph.Delete
Graph.deleteEdges_mono_left : ∀ {α : Type u_1} {β : Type u_2} {G H : Graph α β}, H ≤ G → ∀ (F : Set β), H.deleteEdges F ≤ G.deleteEdges F
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey_insertMany_list_of_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {l : List (α × β)} {k k' : α},
  cmp k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l →
      k ∈ List.map Prod.fst l → ∀ {h' : k' ∈ t.insertMany l}, (t.insertMany l).getKey k' h' = k
-- Mathlib.Data.Nat.Cast.Defs
Nat.cast_four : ∀ {R : Type u_1} [inst : NatCast R], ↑4 = 4
-- Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
CategoryTheory.Triangulated.TStructure.eTriangleLTGE_map_app_hom₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) {X Y : EInt} (f : X ⟶ Y) (j : C),
  ((t.eTriangleLTGE.map f).app j).hom₂ = CategoryTheory.CategoryStruct.id j
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.norm_setIntegral_le_of_norm_le_const : ∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {f : X → E} {s : Set X} {μ : MeasureTheory.Measure X} {C : ℝ},
  μ s < ⊤ → (∀ x ∈ s, ‖f x‖ ≤ C) → ‖∫ (x : X) in s, f x ∂μ‖ ≤ C * μ.real s