mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.CStarAlgebra.Hom
NonUnitalStarAlgHom.isometry : ∀ {F : Type u_1} {A : Type u_2} {B : Type u_3} [inst : NonUnitalCStarAlgebra A] [inst_1 : NonUnitalCStarAlgebra B]
  [inst_2 : FunLike F A B] [NonUnitalAlgHomClass F ℂ A B] [StarHomClass F A B] (φ : F),
  Function.Injective ⇑φ → Isometry ⇑φ
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq
CategoryTheory.IsPullback.of_isBilimit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} {b : CategoryTheory.Limits.BinaryBicone X Y}
  (h : b.IsBilimit), CategoryTheory.IsPullback b.fst b.snd 0 0
-- Lean.Parser.Attr
Lean.Parser.priorityParser.parenthesizer : optParam ℕ 0 → Lean.PrettyPrinter.Parenthesizer
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
EisensteinSeries.summable_linear_left_mul_linear_left : ∀ {z : ℂ}, z ≠ 0 → ∀ (c₁ c₂ : ℤ), Summable fun n => ((↑n * z + ↑c₁) * (↑n * z + ↑c₂))⁻¹
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.constGetEntryLE?_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  {k : α}, t₁.Equiv t₂ → Std.DTreeMap.Const.getEntryLE? t₁ k = Std.DTreeMap.Const.getEntryLE? t₂ k
-- Mathlib.Algebra.Star.Unitary
IsStarProjection.two_mul_sub_one_mem_unitary : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : StarRing R] {p : R}, IsStarProjection p → 2 * p - 1 ∈ unitary R
-- Mathlib.Algebra.Order.Monoid.Defs
IsOrderedCancelMonoid.le_of_mul_le_mul_left : ∀ {α : Type u_2} {inst : CommMonoid α} {inst_1 : Preorder α} [self : IsOrderedCancelMonoid α] (a b c : α),
  a * b ≤ a * c → b ≤ c
-- Mathlib.Data.List.Nodup
List.Nodup.of_append_left : ∀ {α : Type u} {l₁ l₂ : List α}, (l₁ ++ l₂).Nodup → l₁.Nodup
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.IneqCnstr.mk.inj : ∀ {p : Lean.Grind.Linarith.Poly} {strict : Bool} {h : Lean.Meta.Grind.Arith.Linear.IneqCnstrProof}
  {p_1 : Lean.Grind.Linarith.Poly} {strict_1 : Bool} {h_1 : Lean.Meta.Grind.Arith.Linear.IneqCnstrProof},
  { p := p, strict := strict, h := h } = { p := p_1, strict := strict_1, h := h_1 } →
    p = p_1 ∧ strict = strict_1 ∧ h = h_1
-- Init.Data.ULift
instDecidableEqULift : {α : Type u_1} → [DecidableEq α] → DecidableEq (ULift.{u_2, u_1} α)
-- Lean.Meta.Tactic.Grind.Simp
/-- Simplifies the given expression using the `grind` simprocs and normalization theorems.  -/
Lean.Meta.Grind.simpCore : Lean.Expr → Lean.Meta.Grind.GrindM Lean.Meta.Simp.Result
-- Mathlib.Analysis.Seminorm
Seminorm.comp_apply : ∀ {𝕜 : Type u_3} {𝕜₂ : Type u_4} {E : Type u_7} {E₂ : Type u_8} [inst : SeminormedRing 𝕜] [inst_1 : SeminormedRing 𝕜₂]
  {σ₁₂ : 𝕜 →+* 𝕜₂} [inst_2 : RingHomIsometric σ₁₂] [inst_3 : AddCommGroup E] [inst_4 : AddCommGroup E₂]
  [inst_5 : Module 𝕜 E] [inst_6 : Module 𝕜₂ E₂] (p : Seminorm 𝕜₂ E₂) (f : E →ₛₗ[σ₁₂] E₂) (x : E), (p.comp f) x = p (f x)
-- Lean.DocString.Types
Lean.Doc.MathMode.inline.sizeOf_spec : sizeOf Lean.Doc.MathMode.inline = 1
-- Init.Data.List.Count
List.countP_reverse : ∀ {α : Type u_1} {p : α → Bool} {l : List α}, List.countP p l.reverse = List.countP p l
-- Mathlib.Order.Filter.Pi
Filter.tendsto_piMap_pi : ∀ {ι : Type u_1} {α : ι → Type u_2} {β : ι → Type u_3} {f : (i : ι) → α i → β i} {l : (i : ι) → Filter (α i)}
  {l' : (i : ι) → Filter (β i)},
  (∀ (i : ι), Filter.Tendsto (f i) (l i) (l' i)) → Filter.Tendsto (Pi.map f) (Filter.pi l) (Filter.pi l')
-- Mathlib.Topology.MetricSpace.Bounded
Metric.disjoint_nhdsSet_cobounded : ∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α}, IsCompact s → Disjoint (nhdsSet s) (Bornology.cobounded α)
-- Mathlib.MeasureTheory.Measure.Support
MeasureTheory.Measure.support_eq_sInter : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : MeasurableSpace X] {μ : MeasureTheory.Measure X},
  μ.support = ⋂₀ {t | IsClosed t ∧ μ tᶜ = 0}
-- Mathlib.Algebra.Order.Monoid.Basic
/-- Pullback an `IsOrderedMonoid` under a strictly monotone map.  -/
StrictMono.isOrderedMonoid : ∀ {α : Type u} {β : Type u_1} [inst : CommMonoid α] [inst_1 : Preorder α] [IsOrderedMonoid α] [inst_3 : CommMonoid β]
  [inst_4 : LinearOrder β] (f : β → α), StrictMono f → (∀ (x y : β), f (x * y) = f x * f y) → IsOrderedMonoid β
-- Std.Data.Internal.List.Associative
Std.Internal.List.isEmpty_insertListIfNewUnit : ∀ {α : Type u} [inst : BEq α] {l : List ((_ : α) × Unit)} {toInsert : List α},
  (Std.Internal.List.insertListIfNewUnit l toInsert).isEmpty = (l.isEmpty && toInsert.isEmpty)
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect
Std.IterM.toList_toArray_ensureTermination : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : Std.Iterator α m β]
  [inst_2 : Std.Iterators.Finite α m] {it : Std.IterM m β}, Array.toList <$> it.ensureTermination.toArray = it.toList
-- Mathlib.LinearAlgebra.Alternating.Basic
AlternatingMap.domDomCongrEquiv_symm_apply : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {ι : Type u_7} {ι' : Type u_8} (σ : ι ≃ ι') (f : M [⋀^ι']→ₗ[R] N),
  (AlternatingMap.domDomCongrEquiv σ).symm f = AlternatingMap.domDomCongr σ.symm f
-- Mathlib.SetTheory.Ordinal.Basic
Cardinal.ord_lt_ord : ∀ {c₁ c₂ : Cardinal.{u_1}}, c₁.ord < c₂.ord ↔ c₁ < c₂
-- Mathlib.Algebra.Notation.Pi.Defs
Pi.smul_def : ∀ {ι : Type u_1} {α : Type u_2} {M : ι → Type u_5} [inst : (i : ι) → SMul α (M i)] (a : α) (f : (i : ι) → M i),
  a • f = fun i => a • f i
-- Mathlib.AlgebraicGeometry.Morphisms.Basic
AlgebraicGeometry.HasAffineProperty.restrict : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {Q : AlgebraicGeometry.AffineTargetMorphismProperty}
  [AlgebraicGeometry.HasAffineProperty P Q] {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y},
  P f → ∀ (U : ↑Y.affineOpens), Q (f ∣_ ↑U)
-- Init.Data.UInt.Lemmas
UInt8.neg_mul_not_eq_add_mul : ∀ {a b : UInt8}, -(a * ~~~b) = a + a * b
-- Mathlib.Algebra.Order.Group.Synonym
isAddRegular_ofDual : ∀ {α : Type u_1} [inst : AddMonoid α] {a : αᵒᵈ}, IsAddRegular (OrderDual.ofDual a) ↔ IsAddRegular a
-- Mathlib.Analysis.Analytic.Constructions
HasFPowerSeriesAt.add : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f g : E → F}
  {pf pg : FormalMultilinearSeries 𝕜 E F} {x : E},
  HasFPowerSeriesAt f pf x → HasFPowerSeriesAt g pg x → HasFPowerSeriesAt (f + g) (pf + pg) x
-- Mathlib.RingTheory.PicardGroup
/-- Every `R`-algebra `A` gives rise to a homomorphism between Picard groups of `R` and `A`.  -/
CommRing.Pic.mapAlgebra : (R : Type u) →
  [inst : CommSemiring R] →
    (A : Type u_5) → [inst_1 : CommSemiring A] → [Algebra R A] → CommRing.Pic R →* CommRing.Pic A
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get?_alter! : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t.WF →
    ∀ {k k' : α} {f : Option β → Option β},
      Std.DTreeMap.Internal.Impl.Const.get? (Std.DTreeMap.Internal.Impl.Const.alter! k f t) k' =
        if compare k k' = Ordering.eq then f (Std.DTreeMap.Internal.Impl.Const.get? t k)
        else Std.DTreeMap.Internal.Impl.Const.get? t k'
-- Mathlib.Order.WithBot
WithTop.coe_untop : ∀ {α : Type u_1} (x : WithTop α) (hx : x ≠ ⊤), ↑(x.untop hx) = x
-- Mathlib.Analysis.RCLike.Basic
RCLike.ofReal_re : ∀ {K : Type u_1} [inst : RCLike K] (r : ℝ), RCLike.re ↑r = r
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
CategoryTheory.Limits.π_colimitOfIsReflexivePairIsoCoequalizer_inv_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A B : C} {f g : A ⟶ B}
  [inst_1 : CategoryTheory.IsReflexivePair f g] [h : CategoryTheory.Limits.HasCoequalizer f g] {Z : C}
  (h_1 : CategoryTheory.Limits.colimit (CategoryTheory.Limits.ofIsReflexivePair f g) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coequalizer.π f g)
      (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.colimitOfIsReflexivePairIsoCoequalizer.inv h_1) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.colimit.ι (CategoryTheory.Limits.ofIsReflexivePair f g)
        CategoryTheory.Limits.WalkingReflexivePair.zero)
      h_1
-- Mathlib.Algebra.Lie.Weights.Basic
LieModule.mem_genWeightSpaceOf : ∀ {R : Type u_2} {L : Type u_3} (M : Type u_4) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L] (χ : R) (x : L) (m : M),
  m ∈ LieModule.genWeightSpaceOf M χ x ↔ ∃ k, (((LieModule.toEnd R L M) x - χ • 1) ^ k) m = 0
-- Mathlib.Algebra.Order.Module.HahnEmbedding
HahnEmbedding.Partial.extendFun_strictMono : ∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : IsOrderedRing K] [inst_3 : Archimedean K]
  {M : Type u_2} [inst_4 : AddCommGroup M] [inst_5 : LinearOrder M] [inst_6 : IsOrderedAddMonoid M]
  [inst_7 : Module K M] [inst_8 : IsOrderedModule K M] {R : Type u_3} [inst_9 : AddCommGroup R]
  [inst_10 : LinearOrder R] [inst_11 : Module K R] {seed : HahnEmbedding.Seed K M R} (f : HahnEmbedding.Partial seed)
  [inst_12 : IsOrderedAddMonoid R] [inst_13 : Archimedean R] {x : M} (hx : x ∉ (↑f).domain),
  StrictMono ↑(f.extendFun hx)
-- Mathlib.Topology.Inseparable
specializes_iff_forall_closed : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X}, x ⤳ y ↔ ∀ (s : Set X), IsClosed s → x ∈ s → y ∈ s
-- Init.Data.Float.Model.Float32
/-- Converts a `Float32.Model` to a `UInt32`, truncating after the decimal point, sending `NaN` to
`0` and clamping out-of-range values and infinities.
 -/
Float32.Model.toUInt32 : Float32.Model → UInt32
-- Init.Data.String.Lemmas.Pattern.Pred
String.Slice.Pattern.Model.CharPred.instLawfulForwardPatternModelForallCharBool : ∀ {p : Char → Bool}, String.Slice.Pattern.Model.LawfulForwardPatternModel p
-- Mathlib.MeasureTheory.Measure.OpenPos
IsOpen.measure_pos_iff : ∀ {X : Type u_1} [inst : TopologicalSpace X] {m : MeasurableSpace X} (μ : MeasureTheory.Measure X) [μ.IsOpenPosMeasure]
  {U : Set X}, IsOpen U → (0 < μ U ↔ U.Nonempty)
-- Mathlib.AlgebraicTopology.SingularHomology.HomotopyInvariance
/-- Two homotopic morphisms in `TopCat` induce equal morphisms on the
singular homology with coefficients in `R` (e.g. `R := ℤ` considered as
an object of the category of abelian groups).  -/
TopCat.Homotopy.congr_homologyMap_singularChainComplexFunctor : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasCoproducts C] {X Y : TopCat} {f g : X ⟶ Y}
  [inst_3 : CategoryTheory.CategoryWithHomology C] (H : TopCat.Homotopy f g) (R : C) (n : ℕ),
  HomologicalComplex.homologyMap (((AlgebraicTopology.singularChainComplexFunctor C).obj R).map f) n =
    HomologicalComplex.homologyMap (((AlgebraicTopology.singularChainComplexFunctor C).obj R).map g) n
-- Mathlib.GroupTheory.Exponent
mul_notMem_of_orderOf_eq_two : ∀ {G : Type u} [inst : Group G] {x y : G}, orderOf x = 2 → orderOf y = 2 → x ≠ y → x * y ∉ {x, y, 1}
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.get!_inter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k : α} [inst_2 : Inhabited (β k)],
  (t₁ ∩ t₂).get! k = if k ∈ t₂ then t₁.get! k else default
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.map_map : ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : MulOneClass M] [inst_1 : MulOneClass N] [inst_2 : MulOneClass P]
  (S : Submonoid M) (g : N →* P) (f : M →* N), Submonoid.map g (Submonoid.map f S) = Submonoid.map (g.comp f) S
-- Init.Control.State
/-- Returns the given value without modifying the state. Typically used via `Pure.pure`.
 -/
StateT.pure : {σ : Type u} → {m : Type u → Type v} → [Monad m] → {α : Type u} → α → StateT σ m α
-- Mathlib.GroupTheory.Perm.Cycle.Factors
/-- `x` is in the support of `f` iff `Equiv.Perm.cycle_of f x` is a cycle.  -/
Equiv.Perm.isCycle_cycleOf_iff : ∀ {α : Type u_2} {x : α} (f : Equiv.Perm α) [inst : DecidableRel f.SameCycle], (f.cycleOf x).IsCycle ↔ f x ≠ x
-- Mathlib.NumberTheory.Real.GoldenRatio
Real.neg_one_lt_goldenConj : -1 < Real.goldenConj
-- Mathlib.Logic.Embedding.Basic
/-- An embedding is an injective function. Use `Function.Embedding.injective` instead.  -/
Function.Embedding.inj' : ∀ {α : Sort u_1} {β : Sort u_2} (self : α ↪ β), Function.Injective self.toFun
-- Mathlib.Combinatorics.Enumerative.DyckWord
DyckWord.outsidePart_add : ∀ {p q : DyckWord}, p ≠ 0 → (p + q).outsidePart = p.outsidePart + q
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getD_union_of_not_mem_left : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k : α} {fallback : β k}, k ∉ t₁ → (t₁ ∪ t₂).getD k fallback = t₂.getD k fallback
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.getKey!_filter : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {f : α → β → Bool} {k : α},
  (Std.DTreeMap.filter f t).getKey! k = ((t.getKey? k).pfilter fun x h' => f x (Std.DTreeMap.Const.get t x ⋯)).get!
-- Mathlib.Geometry.Manifold.IntegralCurve.UniformTime
/-- The existence of a global integral curve is equivalent to the existence of a family of local
integral curves `γ : ℝ → ℝ → M` with the same starting point `γ 0 = x` such that each `γ a` is
defined on `Ioo (-a) a`.  -/
exists_isMIntegralCurve_iff_exists_isMIntegralCurveOn_Ioo : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_2} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type u_3} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M]
  [inst_5 : IsManifold I 1 M] [T2Space M] {v : (x : M) → TangentSpace I x} [BoundarylessManifold I M],
  (ContMDiff I I.tangent 1 fun x => ⟨x, v x⟩) →
    ∀ (x : M), (∃ γ, γ 0 = x ∧ IsMIntegralCurve γ v) ↔ ∀ (a : ℝ), ∃ γ, γ 0 = x ∧ IsMIntegralCurveOn γ v (Set.Ioo (-a) a)
-- Mathlib.Order.BoundedOrder.Basic
ne_bot_of_le_ne_bot : ∀ {α : Type u} [inst : PartialOrder α] [inst_1 : OrderBot α] {a b : α}, b ≠ ⊥ → b ≤ a → a ≠ ⊥
-- Init.Grind.Ordered.Linarith
_private.Init.Grind.Ordered.Linarith.0.Lean.Grind.Linarith.Expr.denote.match_1.eq_3 : ∀ (motive : Lean.Grind.Linarith.Expr → Sort u_1) (a b : Lean.Grind.Linarith.Expr)
  (h_1 : Unit → motive Lean.Grind.Linarith.Expr.zero)
  (h_2 : (v : Lean.Grind.Linarith.Var) → motive (Lean.Grind.Linarith.Expr.var v))
  (h_3 : (a b : Lean.Grind.Linarith.Expr) → motive (a.add b))
  (h_4 : (a b : Lean.Grind.Linarith.Expr) → motive (a.sub b))
  (h_5 : (k : ℕ) → (a : Lean.Grind.Linarith.Expr) → motive (Lean.Grind.Linarith.Expr.natMul k a))
  (h_6 : (k : ℤ) → (a : Lean.Grind.Linarith.Expr) → motive (Lean.Grind.Linarith.Expr.intMul k a))
  (h_7 : (a : Lean.Grind.Linarith.Expr) → motive a.neg),
  (match a.add b with
    | Lean.Grind.Linarith.Expr.zero => h_1 ()
    | Lean.Grind.Linarith.Expr.var v => h_2 v
    | a.add b => h_3 a b
    | a.sub b => h_4 a b
    | Lean.Grind.Linarith.Expr.natMul k a => h_5 k a
    | Lean.Grind.Linarith.Expr.intMul k a => h_6 k a
    | a.neg => h_7 a) =
    h_3 a b
-- Mathlib.Order.Closure
LowerAdjoint.closure_eq_self_of_mem_closed : ∀ {α : Type u_1} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] {u : β → α} (l : LowerAdjoint u) {x : α},
  x ∈ l.closed → u (l.toFun x) = x
-- Std.Http.Transport
/-- Gets the send channel for a client (client to server direction).
 -/
Std.Http.Internal.Mock.Client.getSendChan : Std.Http.Internal.Mock.Client → Std.CloseableChannel ByteArray
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
IsEllipticNet.atomRel_neg₃ : ∀ {R : Type u_1} [inst : CommRing R] {W : ℤ → R},
  Function.Odd W → ∀ (a b c d : ℤ), IsEllipticNet.atomRel W a b (-c) d = IsEllipticNet.atomRel W a b c d
-- Init.Data.List.Perm
List.reverse_perm : ∀ {α : Type u_1} (l : List α), l.reverse.Perm l
-- Lean.LibrarySuggestions.SineQuaNon
_private.Lean.LibrarySuggestions.SineQuaNon.0.Lean.LibrarySuggestions.SineQuaNon.instOrdProdFloatName_lean : Ord (Float × Lean.Name)
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic
CFC.log_smul : ∀ {A : Type u_1} [inst : NormedRing A] [inst_1 : StarRing A] [inst_2 : NormedAlgebra ℝ A]
  [inst_3 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] {r : ℝ} (a : A),
  (∀ x ∈ spectrum ℝ a, x ≠ 0) →
    r ≠ 0 →
      autoParam (IsSelfAdjoint a) CFC.log_smul._auto_1 → CFC.log (r • a) = (algebraMap ℝ A) (Real.log r) + CFC.log a
-- Init.Data.Nat.Internal.Linear
_private.Init.Data.Nat.Internal.Linear.0.Nat.Internal.Linear.Poly.cancelAux.match_1.splitter : (motive : Nat.Internal.Linear.Poly → Nat.Internal.Linear.Poly → Sort u_1) →
  (m₁ m₂ : Nat.Internal.Linear.Poly) →
    ((m₁ : Nat.Internal.Linear.Poly) → motive m₁ []) →
      ((m₂ : Nat.Internal.Linear.Poly) → (m₂ = [] → False) → motive [] m₂) →
        ((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₂)) →
          motive m₁ m₂
-- Mathlib.Analysis.Fourier.Notation
FourierTransform.fourierCLE_symm_apply : ∀ {R : Type u_5} {E : Type u_6} {F : Type u_7} [inst : Semiring R] [inst_1 : AddCommMonoid E] [inst_2 : AddCommMonoid F]
  [inst_3 : Module R E] [inst_4 : Module R F] [inst_5 : FourierTransform E F] [inst_6 : FourierAdd E F]
  [inst_7 : FourierSMul R E F] [inst_8 : FourierTransformInv F E] [inst_9 : FourierPair E F]
  [inst_10 : FourierInvPair F E] [inst_11 : TopologicalSpace E] [inst_12 : TopologicalSpace F]
  [inst_13 : ContinuousFourier E F] [inst_14 : ContinuousFourierInv F E] (f : F),
  (FourierTransform.fourierCLE R E).symm f = FourierTransformInv.fourierInv f
-- Mathlib.CategoryTheory.MorphismProperty.WeakFactorizationSystem
CategoryTheory.MorphismProperty.llp_eq_of_wfs : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W₁ W₂ : CategoryTheory.MorphismProperty C)
  [W₁.IsWeakFactorizationSystem W₂], W₂.llp = W₁
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.PIsoUnopOpP'.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex.SnakeInput C),
  S.PIsoUnopOpP' = CategoryTheory.Limits.pullbackIsoUnopPushout S.L₁.g S.v₀₁.τ₃
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
CategoryTheory.Limits.spanExt_inv_app_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z X' Y' Z' : C} (iX : X ≅ X') (iY : Y ≅ Y') (iZ : Z ≅ Z')
  {f : X ⟶ Y} {g : X ⟶ Z} {f' : X' ⟶ Y'} {g' : X' ⟶ Z'}
  (wf : CategoryTheory.CategoryStruct.comp iX.hom f' = CategoryTheory.CategoryStruct.comp f iY.hom)
  (wg : CategoryTheory.CategoryStruct.comp iX.hom g' = CategoryTheory.CategoryStruct.comp g iZ.hom),
  (CategoryTheory.Limits.spanExt iX iY iZ wf wg).inv.app CategoryTheory.Limits.WalkingSpan.right = iZ.inv
-- Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
MvPolynomial.rename_psum : ∀ {τ : Type u_2} (σ : Type u_5) (R : Type u_6) [inst : CommSemiring R] [inst_1 : Fintype σ] [inst_2 : Fintype τ] (n : ℕ)
  (e : σ ≃ τ), (MvPolynomial.rename ⇑e) (MvPolynomial.psum σ R n) = MvPolynomial.psum τ R n
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
/-- The walk obtained by removing the last dart of a walk. A nil walk stays nil.  -/
SimpleGraph.Walk.dropLast : {V : Type u} → {G : SimpleGraph V} → {u v : V} → (p : G.Walk u v) → G.Walk u p.penultimate
-- Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
MeasureTheory.Lp.simpleFunc.aestronglyMeasurable : ∀ {α : Type u_1} {E : Type u_4} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E] {p : ENNReal}
  {μ : MeasureTheory.Measure α} (f : ↥(MeasureTheory.Lp.simpleFunc E p μ)),
  MeasureTheory.AEStronglyMeasurable (⇑(MeasureTheory.Lp.simpleFunc.toSimpleFunc f)) μ
-- Mathlib.Geometry.Manifold.IsManifold.Basic
instTopologicalSpaceTangentSpace : {𝕜 : Type u_2} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_1} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {H : Type u_3} →
            [inst_3 : TopologicalSpace H] →
              (I : ModelWithCorners 𝕜 E H) →
                {M : Type u_4} →
                  [inst_4 : TopologicalSpace M] →
                    [inst_5 : ChartedSpace H M] → (_x : M) → TopologicalSpace (TangentSpace I _x)
-- Mathlib.Algebra.Polynomial.Module.Basic
PolynomialModule.monomial_smul_lsingle : ∀ {R : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (i : ℕ) (r : R)
  (j : ℕ) (m : M),
  (Polynomial.monomial i) r • (PolynomialModule.lsingle R j) m = (PolynomialModule.lsingle R (i + j)) (r • m)
-- Init.Data.Char.Ordinal
Char.le_iff_ofOrdinal_le : ∀ {f g : Fin Char.numCodePoints}, f ≤ g ↔ Char.ofOrdinal f ≤ Char.ofOrdinal g
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKeyD_eq_fallback : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {a fallback : α}, a ∉ m → m.getKeyD a fallback = fallback
-- Mathlib.Order.SuccPred.Limit
Order.isSuccPrelimit_iff_isMin : ∀ {α : Type u_1} {a : α} [inst : PartialOrder α] [inst_1 : SuccOrder α] [IsSuccArchimedean α],
  Order.IsSuccPrelimit a ↔ IsMin a
-- Mathlib.Order.Filter.Basic
Filter.frequently_mem_iff_neBot : ∀ {α : Type u} {l : Filter α} {s : Set α}, (∃ᶠ (x : α) in l, x ∈ s) ↔ (l ⊓ Filter.principal s).NeBot
-- Mathlib.Order.SuccPred.Limit
WithBot.isSuccPrelimit_iff : ∀ {α : Type u_1} [inst : Preorder α] {x : WithBot α}, Order.IsSuccPrelimit x ↔ x = ⊥ ∨ ∃ y, x = ↑y ∧ Order.IsSuccLimit y
-- Mathlib.Tactic.Linarith.Oracle.FourierMotzkin
/-- The union of all variables appearing in those original assumptions
which appear in the `history` set.  -/
Mathlib.Tactic.Linarith.PComp.vars : Mathlib.Tactic.Linarith.PComp → Std.TreeSet ℕ compare
-- Mathlib.Analysis.Distribution.FourierMultiplier
TemperedDistribution.fourierMultiplierCLM_fourierMultiplierCLM_apply : ∀ {E : Type u_3} {F : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F]
  [inst_2 : InnerProductSpace ℝ E] [inst_3 : NormedSpace ℂ F] [inst_4 : FiniteDimensional ℝ E]
  [inst_5 : MeasurableSpace E] [inst_6 : BorelSpace E] {g₁ g₂ : E → ℂ},
  Function.HasTemperateGrowth g₁ →
    Function.HasTemperateGrowth g₂ →
      ∀ (f : TemperedDistribution E F),
        (TemperedDistribution.fourierMultiplierCLM F g₂) ((TemperedDistribution.fourierMultiplierCLM F g₁) f) =
          (TemperedDistribution.fourierMultiplierCLM F (g₁ * g₂)) f
-- Init.Data.Array.Basic
/-- Returns `true` if the monadic predicate `p` returns `true` for every element of `as`.

Short-circuits upon encountering the first `false`. The elements in `as` are examined in order from
left to right.

The optional parameters `start` and `stop` control the region of the array to be checked. Only the
elements with indices from `start` (inclusive) to `stop` (exclusive) are checked. By default, the
entire array is checked.
 -/
Array.allM : {α : Type u} →
  {m : Type → Type w} → [Monad m] → (α → m Bool) → (as : Array α) → optParam ℕ 0 → optParam ℕ as.size → m Bool
-- Mathlib.Algebra.GroupWithZero.Action.Defs
SMulZeroClass.mk : {M : Type u_12} → {A : Type u_13} → [inst : Zero A] → [toSMul : SMul M A] → (∀ (a : M), a • 0 = 0) → SMulZeroClass M A
-- Lean.Compiler.IR.Basic
Lean.IR.Alt.default.injEq : ∀ (b b_1 : Lean.IR.FnBody), (Lean.IR.Alt.default b = Lean.IR.Alt.default b_1) = (b = b_1)
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.Priority.instToString : ToString Aesop.Frontend.Priority
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.smul_of : ∀ {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} [inst : SMul R α] (r : R) (f : m → n → α),
  r • Matrix.of f = Matrix.of (r • f)