mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.Monoid
Specializes.nsmul : ∀ {M : Type u_6} [inst : AddMonoid M] [inst_1 : TopologicalSpace M] [ContinuousAdd M] {a b : M},
  a ⤳ b → ∀ (n : ℕ), (n • a) ⤳ (n • b)
-- Mathlib.Topology.MetricSpace.HausdorffDistance
Metric.le_infEDist : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {x : α} {s : Set α} {d : ENNReal},
  d ≤ Metric.infEDist x s ↔ ∀ y ∈ s, d ≤ edist x y
-- Mathlib.Data.Nat.Cast.Commute
Commute.self_natCast_mul_natCast_mul : ∀ {α : Type u_1} [inst : Semiring α] (a : α) (m n : ℕ), Commute (↑m * a) (↑n * a)
-- Mathlib.Algebra.Polynomial.Degree.Lemmas
Polynomial.eq_natDegree_of_le_mem_support : ∀ {R : Type u} {n : ℕ} [inst : Semiring R] {p : Polynomial R}, p.natDegree ≤ n → n ∈ p.support → p.natDegree = n
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
/-- Angles in a vector space are translation invariant.  -/
EuclideanGeometry.angle_add_const : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] (v₁ v₂ v₃ v : V),
  EuclideanGeometry.angle (v₁ + v) (v₂ + v) (v₃ + v) = EuclideanGeometry.angle v₁ v₂ v₃
-- Init.Data.Array.Lemmas
Array.foldr_eq_apply_foldl : ∀ {α : Type u_1} {init x : α} {xs : Array α} {f : α → α → α} [Std.Associative f] [Std.LawfulLeftIdentity f init],
  Array.foldr f x xs = f (Array.foldl f init xs) x
-- Mathlib.Algebra.Group.ULift
ULift.addCommSemigroup.eq_1 : ∀ {α : Type u} [inst : AddCommSemigroup α],
  ULift.addCommSemigroup = Function.Injective.addCommSemigroup ⇑Equiv.ulift ⋯ ⋯
-- Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument
/-- The natural "inclusion" `𝟭 (Arrow C) ⟶ iteration I κ`.  -/
CategoryTheory.SmallObject.ιIteration : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (I : CategoryTheory.MorphismProperty C) →
      (κ : Cardinal.{w}) →
        [inst_1 : Fact κ.IsRegular] →
          [inst_2 : OrderBot κ.ord.ToType] →
            [inst_3 : I.IsCardinalForSmallObjectArgument κ] →
              CategoryTheory.Functor.id (CategoryTheory.Arrow C) ⟶ CategoryTheory.SmallObject.iteration I κ
-- Mathlib.Topology.MetricSpace.HausdorffDimension
dimH_le_of_hausdorffMeasure_ne_top : ∀ {X : Type u_2} [inst : EMetricSpace X] [inst_1 : MeasurableSpace X] [inst_2 : BorelSpace X] {s : Set X} {d : NNReal},
  (MeasureTheory.Measure.hausdorffMeasure ↑d) s ≠ ⊤ → dimH s ≤ ↑d
-- Mathlib.Algebra.Divisibility.Basic
dvd_iff_exists_eq_mul_left : ∀ {α : Type u_1} [inst : CommSemigroup α] {a b : α}, a ∣ b ↔ ∃ c, b = c * a
-- Init.Core
Iff.of_eq : ∀ {a b : Prop}, a = b → (a ↔ b)
-- Mathlib.NumberTheory.ModularForms.Bounds
/-- Bound for the coefficients of a modular form: if `f` is a weight `k` modular form for an
arithmetic subgroup, then its `q`-expansion coefficients are `O (n ^ k)`.

This is not optimal -- the optimal exponent is `k - 1 + ε` for any `0 < ε`, at least for congruence
levels -- but is much easier to prove than the optimal result.

See `CuspFormClass.qExpansion_isBigO` for a sharper bound assuming `f` is cuspidal.  -/
ModularFormClass.qExpansion_isBigO : ∀ {k : ℤ},
  0 ≤ k →
    ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.IsArithmetic] {F : Type u_2} [inst : FunLike F UpperHalfPlane ℂ]
      [ModularFormClass F Γ k] (f : F),
      (fun n => (PowerSeries.coeff n) (UpperHalfPlane.qExpansion Γ.strictWidthInfty ⇑f)) =O[Filter.atTop] fun n =>
        ↑n ^ k
-- Mathlib.MeasureTheory.Measure.Regular
MeasurableSet.exists_isClosed_sdiff_lt : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace α]
  [OpensMeasurableSpace α] [μ.WeaklyRegular] ⦃A : Set α⦄,
  MeasurableSet A → μ A ≠ ⊤ → ∀ {ε : ENNReal}, ε ≠ 0 → ∃ F ⊆ A, IsClosed F ∧ μ (A \ F) < ε
-- Mathlib.Analysis.Convex.Gauge
/-- **Alias** of `Convex.setOfPred_gauge_le`. -/
Convex.setOf_gauge_le : ∀ {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {s : Set E},
  Convex ℝ s → 0 ∈ s → Absorbent ℝ s → ∀ (a : ℝ), Convex ℝ {x | gauge s x ≤ a}
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.coneOfCoconeLeftOp.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J Cᵒᵖ} (c : CategoryTheory.Limits.Cocone F.leftOp),
  CategoryTheory.Limits.coneOfCoconeLeftOp c = { pt := Opposite.op c.pt, π := CategoryTheory.NatTrans.removeLeftOp c.ι }
-- Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
Subgroup.unop_sSup : ∀ {G : Type u_2} [inst : Group G] (S : Set (Subgroup Gᵐᵒᵖ)), (sSup S).unop = sSup (Subgroup.op ⁻¹' S)
-- Init.Data.String.Basic
String.Slice.getUTF8Byte_eq_getUTF8Byte_copy : ∀ {s : String.Slice} {p : String.Pos.Raw} {h : p < s.rawEndPos}, s.getUTF8Byte p h = s.copy.getUTF8Byte p ⋯
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.DiseqCnstr.mk : Lean.Expr →
  Lean.Expr →
    Lean.Meta.Grind.Arith.CommRing.RingExpr →
      Lean.Meta.Grind.Arith.CommRing.RingExpr →
        Lean.Meta.Grind.Arith.CommRing.PolyDerivation →
          Option (Lean.Meta.Grind.Arith.CommRing.SemiringExpr × Lean.Meta.Grind.Arith.CommRing.SemiringExpr) →
            Lean.Meta.Grind.Arith.CommRing.DiseqCnstr
-- Mathlib.Algebra.Polynomial.Laurent
/-- When we have `[CommSemiring R]`, the function `C` is the same as `algebraMap R R[T;T⁻¹]`.
(But note that `C` is defined when `R` is not necessarily commutative, in which case
`algebraMap` is not available.)
 -/
LaurentPolynomial.C_eq_algebraMap : ∀ {R : Type u_3} [inst : CommSemiring R] (r : R), LaurentPolynomial.C r = (algebraMap R (LaurentPolynomial R)) r
-- Mathlib.Analysis.SpecialFunctions.Pow.Complex
Complex.cpow_nat_mul : ∀ (x : ℂ) (n : ℕ) (y : ℂ), x ^ (↑n * y) = (x ^ y) ^ n
-- Aesop.RuleSet.Member
Aesop.GlobalRuleSetMember.normSimpRule.injEq : ∀ (e e_1 : Aesop.NormSimpRule),
  (Aesop.GlobalRuleSetMember.normSimpRule e = Aesop.GlobalRuleSetMember.normSimpRule e_1) = (e = e_1)
-- Mathlib.Probability.Kernel.Defs
ProbabilityTheory.Kernel.sum_apply' : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [inst : Countable ι]
  (κ : ι → ProbabilityTheory.Kernel α β) (a : α) {s : Set β},
  MeasurableSet s → ((ProbabilityTheory.Kernel.sum κ) a) s = ∑' (n : ι), ((κ n) a) s
-- Mathlib.Analysis.Convex.SpecificFunctions.Basic
Real.exp_mul_le_cosh_add_mul_sinh : ∀ {t : ℝ}, |t| ≤ 1 → ∀ (x : ℝ), Real.exp (t * x) ≤ Real.cosh x + t * Real.sinh x
-- Mathlib.NumberTheory.Padics.RingHoms
PadicInt.denseRange_natCast : ∀ {p : ℕ} [hp_prime : Fact (Nat.Prime p)], DenseRange Nat.cast
-- Lean.Elab.Tactic.Omega.Core
Lean.Elab.Tactic.Omega.Justification.combo.sizeOf_spec : ∀ {s t : Lean.Omega.Constraint} {x y : Lean.Omega.Coeffs} (a : ℤ) (j : Lean.Elab.Tactic.Omega.Justification s x) (b : ℤ)
  (k : Lean.Elab.Tactic.Omega.Justification t y),
  sizeOf (Lean.Elab.Tactic.Omega.Justification.combo a j b k) =
    1 + sizeOf s + sizeOf t + sizeOf x + sizeOf y + sizeOf a + sizeOf j + sizeOf b + sizeOf k
-- Lean.Data.DeclarationRange
Lean.instReprDeclarationRange.repr : Lean.DeclarationRange → ℕ → Std.Format
-- Init.Data.Slice.Array.Lemmas
Array.stop_mkSlice_rcc : ∀ {α : Type u_1} {xs : Array α} {lo hi : ℕ}, (Std.Rcc.Sliceable.mkSlice xs lo...=hi).stop = min (hi + 1) xs.size
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.LetDecl.value : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.LetDecl pu → Lean.Compiler.LCNF.LetValue pu
-- Mathlib.Topology.Covering.Quotient
/-- If a group `G` acts on a space `E` and `U` is an open subset disjoint from all other
`G`-translates of itself, and `p` is a quotient map by this action, then `p` admits a
`Bundle.Trivialization` over the base set `p(U)`.  -/
Topology.IsQuotientMap.trivializationOfSMulDisjoint : {E : Type u_1} →
  {X : Type u_2} →
    [inst : TopologicalSpace E] →
      [inst_1 : TopologicalSpace X] →
        {f : E → X} →
          {G : Type u_3} →
            [inst_2 : Group G] →
              [inst_3 : MulAction G E] →
                Topology.IsQuotientMap f →
                  [ContinuousConstSMul G E] →
                    (∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit G e₂) →
                      [inst_5 : TopologicalSpace G] →
                        [DiscreteTopology G] →
                          (U : Set E) →
                            IsOpen U →
                              (∀ (g : G), ((fun x => g • x) '' U ∩ U).Nonempty → g = 1) → Bundle.Trivialization G f
-- Mathlib.Algebra.Homology.ExactSequence
CategoryTheory.ComposableArrows.Exact.exact' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {n : ℕ} {S : CategoryTheory.ComposableArrows C n} (hS : S.Exact) (i j k : ℕ)
  (hij : autoParam (i + 1 = j) CategoryTheory.ComposableArrows.Exact.exact'._auto_1)
  (hjk : autoParam (j + 1 = k) CategoryTheory.ComposableArrows.Exact.exact'._auto_3)
  (hk : autoParam (k ≤ n) CategoryTheory.ComposableArrows.Exact.exact'._auto_5), (S.sc' ⋯ i j k hij hjk hk).Exact
-- Init.Data.Nat.Basic
Nat.sub_succ_lt_self : ∀ (a i : ℕ), i < a → a - (i + 1) < a - i
-- Mathlib.SetTheory.Ordinal.Basic
/-- **Alias** of `Cardinal.ord_natCast`. -/
Cardinal.ord_nat : ∀ (n : ℕ), (↑n).ord = ↑n
-- Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
IntermediateField.instIsAlgClosureAlgebraicClosureSubtypeMemOfIsAlgebraic : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (E : IntermediateField K L)
  [Algebra.IsAlgebraic K ↥E], IsAlgClosure K (AlgebraicClosure ↥E)
-- Mathlib.Tactic.NormNum.IsSquare
Mathlib.Meta.NormNum.iff_isSquare_of_isInt_int : ∀ (a : ℤ) (n : ℕ), Mathlib.Meta.NormNum.IsInt a (Int.negOfNat n) → (n = 0 ↔ IsSquare a)
-- Mathlib.Data.Finsupp.Defs
Finsupp.mapRange.equiv_refl : ∀ {ι : Type u_3} {M : Type u_4} [inst : Zero M], Finsupp.mapRange.equiv (Equiv.refl M) ⋯ = Equiv.refl (ι →₀ M)
-- Lean.Meta.Tactic.Grind.Types
/-- Removes the entry `e ↦ parents` from the parent map.
 -/
Lean.Meta.Grind.resetParentsOf : Lean.Expr → Lean.Meta.Grind.GoalM Unit
-- Mathlib.Algebra.Group.Submonoid.Units
AddSubgroup.ofAddUnits_iSup₂ : ∀ {M : Type u_1} [inst : AddMonoid M] {ι : Sort u_2} {κ : ι → Sort u_3} (f : (i : ι) → κ i → AddSubgroup (AddUnits M)),
  (⨆ i, ⨆ j, f i j).ofAddUnits = ⨆ i, ⨆ j, (f i j).ofAddUnits
-- Std.Do.SPred.Laws
Std.Do.SPred.imp_intro : ∀ {σs : List (Type u)} {P Q R : Std.Do.SPred σs}, (P ∧ Q ⊢ₛ R) → P ⊢ₛ Q → R
-- Mathlib.Order.Interval.Finset.Defs
LocallyFiniteOrder.toLocallyFiniteOrderTop.eq_1 : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] [inst_2 : OrderTop α],
  LocallyFiniteOrder.toLocallyFiniteOrderTop =
    { finsetIoi := fun b => Finset.Ioc b ⊤, finsetIci := fun b => Finset.Icc b ⊤, finset_mem_Ici := ⋯,
      finset_mem_Ioi := ⋯ }
-- Mathlib.Algebra.Lie.DirectSum
DirectSum.lieRing : {ι : Type v} → (L : ι → Type w) → [inst : (i : ι) → LieRing (L i)] → LieRing (DirectSum ι fun i => L i)
-- Mathlib.FieldTheory.RatFunc.Luroth
_private.Mathlib.FieldTheory.RatFunc.Luroth.0.RatFunc.Luroth.Φ_ne_zero : ∀ {K : Type u_1} [inst : Field K] {E : IntermediateField K (RatFunc K)}, E ≠ ⊥ → RatFunc.Luroth.Φ✝ E ≠ 0
-- Mathlib.GroupTheory.Coxeter.Inversion
CoxeterSystem.IsReflection.length_mul_left_ne : ∀ {B : Type u_1} {W : Type u_2} [inst : Group W] {M : CoxeterMatrix B} {cs : CoxeterSystem M W} {t : W},
  cs.IsReflection t → ∀ (w : W), cs.length (w * t) ≠ cs.length w
-- Mathlib.Data.Finsupp.Multiset
Finsupp.toMultiset_eq_iff : ∀ {α : Type u_1} [inst : DecidableEq α] {f : α →₀ ℕ} {s : Multiset α},
  Finsupp.toMultiset f = s ↔ f = Multiset.toFinsupp s
-- Init.SizeOf
Lean.Macro.Context.mk.sizeOf_spec : ∀ (methods : Lean.Macro.MethodsRef) (quotContext : Lean.Name) (currMacroScope : Lean.MacroScope)
  (currRecDepth maxRecDepth : ℕ) (ref : Lean.Syntax),
  sizeOf
      { methods := methods, quotContext := quotContext, currMacroScope := currMacroScope, currRecDepth := currRecDepth,
        maxRecDepth := maxRecDepth, ref := ref } =
    1 + sizeOf methods + sizeOf quotContext + sizeOf currMacroScope + sizeOf currRecDepth + sizeOf maxRecDepth +
      sizeOf ref
-- Mathlib.CategoryTheory.SingleObj
CategoryTheory.SingleObj.comp_as_mul : ∀ (M : Type u) [inst : Monoid M] {x y z : CategoryTheory.SingleObj M} (f : x ⟶ y) (g : y ⟶ z),
  CategoryTheory.CategoryStruct.comp f g = g * f
-- Mathlib.Algebra.BigOperators.Expect
Finset.expect_sub_distrib : ∀ {ι : Type u_1} {M : Type u_4} [inst : AddCommGroup M] [inst_1 : Module ℚ≥0 M] (s : Finset ι) (f g : ι → M),
  (s.expect fun i => f i - g i) = (s.expect fun i => f i) - s.expect fun i => g i
-- Aesop.Index
_private.Aesop.Index.0.Aesop.Index.applicableRules.addRules : {α : Type} →
  Aesop.RulePatternSubstMap →
    Array (Aesop.IndexMatchResult (Aesop.Rule α)) →
      Array (Array (Aesop.Rule α × Array Aesop.IndexMatchLocation)) →
        Lean.MetaM (Array (Aesop.IndexMatchResult (Aesop.Rule α)))
-- Mathlib.Order.Defs.Unbundled
isTrans_def : ∀ {α : Sort u_2} {r : α → α → Prop}, IsTrans α r ↔ ∀ ⦃a b c : α⦄, r a b → r b c → r a c
-- Batteries.Data.UnionFind.Basic
/-- Parent of a union-find node, defaults to self when the node is a root  -/
Batteries.UnionFind.parentD : Array Batteries.UFNode → ℕ → ℕ
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorEquivalence_functor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (L : CategoryTheory.Functor C D)
  (R : CategoryTheory.Functor E D),
  (CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorEquivalence L R).functor =
    CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorToComma L R
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.isEquivalence_functor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : C ≌ D), F.functor.IsEquivalence
-- Mathlib.Order.PiLex
Pi.Lex.eq_1 : ∀ {ι : Type u_1} {β : ι → Type u_2} (r : ι → ι → Prop) (s : {i : ι} → β i → β i → Prop) (x y : (i : ι) → β i),
  Pi.Lex r s x y = ∃ i, (∀ (j : ι), r j i → x j = y j) ∧ s (x i) (y i)
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.add_lt_add_left : ∀ {d : ℕ} [dnsq : Zsqrtd.Nonsquare d] (a b : ℤ√↑d), a < b → ∀ (c : ℤ√↑d), c + a < c + b
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Affine.Simplex.points_notMem_affineSpan_faceOpposite : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_5} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] [Nontrivial k] {n : ℕ} [inst_5 : NeZero n] (s : Affine.Simplex k P n) (i : Fin (n + 1)),
  s.points i ∉ affineSpan k (Set.range (s.faceOpposite i).points)
-- Lean.Level
Lean.Level.PP.Result.imax : Lean.Level.PP.Result → Lean.Level.PP.Result → Lean.Level.PP.Result
-- Aesop.Forward.Match.Types
/-- The pattern substitutions that have been added to the match.  -/
Aesop.Match.patInstSubsts : Aesop.Match → Array Aesop.Substitution
-- Init.Data.Array.Find
Array.findIdx?_eq_guard_findIdx_lt : ∀ {α : Type u_1} {xs : Array α} {p : α → Bool},
  Array.findIdx? p xs = Option.guard (fun i => decide (i < xs.size)) (Array.findIdx p xs)
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.coeff_natCast : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : MulOneClass M] (n : ℕ), (↑n).coeff = fun₀ | 1 => ↑n
-- Mathlib.NumberTheory.FunctionField
FunctionField.finiteDimensional_ratFunc_of_constantExtension : ∀ {F : Type u_1} (K : Type u_2) [inst : Field F] [inst_1 : Field K] [inst_2 : Algebra (Polynomial F) K]
  [inst_3 : FaithfulSMul (Polynomial F) K] [FunctionField F K] {E : Type u_3} [inst_5 : Field E] [inst_6 : Algebra F E]
  [inst_7 : Algebra (Polynomial E) K] [FaithfulSMul (Polynomial E) K] [IsScalarTower (Polynomial F) (Polynomial E) K],
  FiniteDimensional (RatFunc F) (RatFunc E)
-- Mathlib.RingTheory.Ideal.Over
Ideal.map_equiv_liesOver : ∀ {A : Type u_2} [inst : CommSemiring A] {B : Type u_3} {C : Type u_4} [inst_1 : Semiring B] [inst_2 : Semiring C]
  [inst_3 : Algebra A B] [inst_4 : Algebra A C] (P : Ideal B) (p : Ideal A) [P.LiesOver p] {E : Type u_6}
  [inst_6 : EquivLike E B C] [AlgEquivClass E A B C] (σ : E), (Ideal.map σ P).LiesOver p
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
cfcₙ_const_mul : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : Nontrivial R] [inst_2 : StarRing R]
  [inst_3 : MetricSpace R] [inst_4 : IsTopologicalSemiring R] [inst_5 : ContinuousStar R] [inst_6 : NonUnitalRing A]
  [inst_7 : StarRing A] [inst_8 : TopologicalSpace A] [inst_9 : Module R A] [inst_10 : IsScalarTower R A A]
  [inst_11 : SMulCommClass R A A] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p] (r : R) (f : R → R) (a : A),
  autoParam (ContinuousOn f (quasispectrum R a)) cfcₙ_const_mul._auto_1 →
    autoParam (f 0 = 0) cfcₙ_const_mul._auto_3 → cfcₙ (fun x => r * f x) a = r • cfcₙ f a
-- Mathlib.Geometry.Euclidean.PerpBisector
AffineSubspace.perpBisector_comm : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (p₁ p₂ : P), AffineSubspace.perpBisector p₁ p₂ = AffineSubspace.perpBisector p₂ p₁
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.endsWith_congr : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.BackwardPattern pat] [String.Slice.Pattern.Model.LawfulBackwardPatternModel pat]
  {s t : String.Slice}, s.copy = t.copy → s.endsWith pat = t.endsWith pat
-- Mathlib.Logic.Function.Basic
Function.extend_const : ∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (f : α → β) (c : γ),
  (Function.extend f (fun x => c) fun x => c) = fun x => c
-- Init.WF
/-- A well-founded relation on `α`.  -/
WellFoundedRelation.rel : {α : Sort u} → [self : WellFoundedRelation α] → α → α → Prop
-- Mathlib.Algebra.Group.Commute.Units
/-- If a natural power of `x` is a unit, then `x` is a unit.  -/
Units.ofPow : {M : Type u_1} → [inst : Monoid M] → (u : Mˣ) → (x : M) → {n : ℕ} → n ≠ 0 → x ^ n = ↑u → Mˣ
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.zipWith_single_single : ∀ {ι : Type u} {β : ι → Type v} {β₁ : ι → Type v₁} {β₂ : ι → Type v₂} [inst : (i : ι) → Zero (β i)]
  [inst_1 : DecidableEq ι] [inst_2 : (i : ι) → Zero (β₁ i)] [inst_3 : (i : ι) → Zero (β₂ i)]
  (f : (i : ι) → β₁ i → β₂ i → β i) (hf : ∀ (i : ι), f i 0 0 = 0) {i : ι} (b₁ : β₁ i) (b₂ : β₂ i),
  (DFinsupp.zipWith f hf (fun₀ | i => b₁) fun₀ | i => b₂) = fun₀ | i => f i b₁ b₂
-- Batteries.Linter.UnnecessarySeqFocus
/-- Search for tactic executions in the info tree and remove executed tactic syntaxes.  -/
Batteries.Linter.UnnecessarySeqFocus.markUsedTactics : Lean.Environment → {ω : Type} → Lean.Elab.InfoTree → Batteries.Linter.UnnecessarySeqFocus.M ω Unit
-- Mathlib.Order.Hom.CompleteLattice
sSupHom.instPartialOrder.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : SupSet α] {x : CompleteLattice β},
  sSupHom.instPartialOrder = PartialOrder.lift DFunLike.coe ⋯
-- Mathlib.Analysis.RCLike.Basic
RCLike.ofRealAm_coe : ∀ {K : Type u_1} [inst : RCLike K], ⇑RCLike.ofRealAm = RCLike.ofReal
-- Mathlib.Analysis.Calculus.DerivativeTest
/-- Suppose `f : ℝ → ℝ` is continuous at `b` and `c`, the derivative `f'` is nonnegative on
`Ioo a b` and nonpositive on `Ioo b c`. Then `f` attains its maximum on `Ioc a c` at `b`.  -/
isMaxOn_Ioc_of_deriv : ∀ {f : ℝ → ℝ} {a b c : ℝ},
  ContinuousAt f b →
    ContinuousAt f c →
      DifferentiableOn ℝ f (Set.Ioo a b) →
        DifferentiableOn ℝ f (Set.Ioo b c) →
          (∀ x ∈ Set.Ioo a b, 0 ≤ deriv f x) → (∀ x ∈ Set.Ioo b c, deriv f x ≤ 0) → IsMaxOn f (Set.Ioc a c) b
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.keys.match_1.eq_1 : ∀ {α : Type u_2} {β : α → Type u_1} (motive : List ((a : α) × β a) → Sort u_3) (h_1 : Unit → motive [])
  (h_2 : (k : α) → (snd : β k) → (l : List ((a : α) × β a)) → motive (⟨k, snd⟩ :: l)),
  (match [] with
    | [] => h_1 ()
    | ⟨k, snd⟩ :: l => h_2 k snd l) =
    h_1 ()
-- Mathlib.CategoryTheory.Preadditive.Injective.Basic
CategoryTheory.Limits.IsZero.injective : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C},
  CategoryTheory.Limits.IsZero X → CategoryTheory.Injective X
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.zeroLocus_setMul : ∀ (X : AlgebraicGeometry.Scheme) {U : X.Opens} (s t : Set ↑(X.presheaf.obj (Opposite.op U))),
  X.zeroLocus (s * t) = X.zeroLocus s ∪ X.zeroLocus t
-- Mathlib.Algebra.BigOperators.Module
/-- **Summation by parts**, also known as **Abel's lemma** or an **Abel transformation**  -/
Finset.sum_Ico_by_parts : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (f : ℕ → R) (g : ℕ → M)
  {m n : ℕ},
  m < n →
    ∑ i ∈ Finset.Ico m n, f i • g i =
      f (n - 1) • ∑ i ∈ Finset.range n, g i - f m • ∑ i ∈ Finset.range m, g i -
        ∑ i ∈ Finset.Ico m (n - 1), (f (i + 1) - f i) • ∑ i ∈ Finset.range (i + 1), g i
-- Mathlib.Topology.Order.Category.FrameAdjunction
/-- The forgetful functor `topToLocale` is left adjoint to the functor `pt`.  -/
Locale.adjunctionTopToLocalePT : topToLocale ⊣ Locale.pt
-- Init.Data.List.Lemmas
List.reverse_eq_append_iff : ∀ {α : Type u_1} {xs ys zs : List α}, xs.reverse = ys ++ zs ↔ xs = zs.reverse ++ ys.reverse
-- Mathlib.LinearAlgebra.Finsupp.Pi
Finsupp.LinearEquiv.finsuppUnique_symm_apply : ∀ {R : Type u_1} {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : Semiring R] [inst_2 : Module R M] (α : Type u_5)
  [inst_3 : Unique α] (m : M), (Finsupp.LinearEquiv.finsuppUnique R M α).symm m = fun₀ | default => m
-- Lean.Language.Lean.Types
Lean.Language.Lean.instToSnapshotTreeHeaderParsedSnapshot : Lean.Language.ToSnapshotTree Lean.Language.Lean.HeaderParsedSnapshot
-- Lean.Meta.Tactic.Grind.EMatch
_private.Lean.Meta.Tactic.Grind.EMatch.0.Lean.Meta.Grind.EMatch.assignUnassignedLevelMVars.match_1.splitter : (motive : Lean.Expr × Array Lean.Expr → Sort u_1) →
  (x : Lean.Expr × Array Lean.Expr) → ((c₂ : Lean.Expr) → (cs₂ : Array Lean.Expr) → motive (c₂, cs₂)) → motive x
-- Mathlib.Algebra.GroupWithZero.Units.Basic
div_eq_one_iff_eq : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {a b : G₀}, b ≠ 0 → (a / b = 1 ↔ a = b)
-- Mathlib.NumberTheory.Real.Irrational
irrational_natCast_add_iff : ∀ {n : ℕ} {x : ℝ}, Irrational (↑n + x) ↔ Irrational x
-- Batteries.Data.DList.Lemmas
Batteries.DList.push.eq_1 : ∀ {α : Type u} (x : α) (f : List α → List α) (h : ∀ (l : List α), f l = f [] ++ l),
  { apply := f, invariant := h }.push x = { apply := fun t => f (x :: t), invariant := ⋯ }
-- Mathlib.Algebra.GCDMonoid.Finset
Finset.gcd_eq_gcd_image : ∀ {α : Type u_2} {β : Type u_3} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] {s : Finset β}
  {f : β → α} [inst_2 : DecidableEq α], s.gcd f = (Finset.image f s).gcd id
-- Mathlib.Topology.Continuous
Continuous.iterate : ∀ {X : Type u_1} [inst : TopologicalSpace X] {f : X → X}, Continuous f → ∀ (n : ℕ), Continuous f^[n]
-- Mathlib.CategoryTheory.Monoidal.Closed.Ideal
/-- If `i` witnesses that `D` is a reflective subcategory and an exponential ideal, then `D` is
itself Cartesian closed.

To allow for better control of definitional equality, this construction
takes in an explicit choice of lift of the essential image of `i` to `D`, in the form of a functor
`l : i.EssImageSubcategory ⥤ D` and natural isomorphism `φ : l ⋙ i ≅ i.essImage.ι`. When
`l ⋙ i` is defeq to `i.essImage.ι`, images of exponential objects in `D` under `i` will be defeq
to the respective exponential objects in `C`.  -/
CategoryTheory.cartesianClosedOfReflective' : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₁, u₂} D] →
        (i : CategoryTheory.Functor D C) →
          [inst_2 : CategoryTheory.CartesianMonoidalCategory C] →
            [CategoryTheory.Reflective i] →
              [inst_4 : CategoryTheory.MonoidalClosed C] →
                [inst_5 : CategoryTheory.CartesianMonoidalCategory D] →
                  [CategoryTheory.ExponentialIdeal i] →
                    (l : CategoryTheory.Functor i.EssImageSubcategory D) →
                      (l.comp i ≅ i.essImage.ι) → CategoryTheory.MonoidalClosed D
-- Mathlib.Data.Finsupp.Basic
Finsupp.frange_single : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] {x : α} {y : M}, (fun₀ | x => y).frange ⊆ {y}