mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.toAdditive_apply : ∀ {M : Type u_1} {G : Type u_2} [inst : Monoid M] [inst_1 : CommGroup G] [inst_2 : MulDistribMulAction M G]
  (a : ↑(Rep.ofMulDistribMulAction M G)), Rep.toAdditive a = a
-- Mathlib.Algebra.Group.Center
/-- associative property for left addition  -/
IsAddCentral.left_assoc : ∀ {M : Type u_1} [inst : Add M] {z : M}, IsAddCentral z → ∀ (b c : M), z + (b + c) = z + b + c
-- Init.Data.String.Lemmas.Pattern.Pred
String.Slice.Pattern.Model.CharPred.Decidable.matchAt?_eq : ∀ {s : String.Slice} {pos : s.Pos} {p : Char → Prop} [inst : DecidablePred p],
  String.Slice.Pattern.Model.matchAt? p pos =
    if h₀ : ∃ (h : pos ≠ s.endPos), p (pos.get h) then some (pos.next ⋯) else none
-- Init.Data.BitVec.Lemmas
_private.Init.Data.BitVec.Lemmas.0.BitVec.flattenList.toNatAux.eq_def : ∀ {n : ℕ} (x : List (BitVec n)),
  BitVec.flattenList.toNatAux x =
    match x with
    | [] => 0
    | [x] => x.toNat
    | x :: y :: rest =>
      have xs := x :: y :: rest;
      have mid := xs.length / 2;
      BitVec.flattenList.toNatAux (List.take mid xs) <<< (n * (List.drop mid xs).length) |||
        BitVec.flattenList.toNatAux (List.drop mid xs)
-- Mathlib.FieldTheory.RatFunc.Luroth
_private.Mathlib.FieldTheory.RatFunc.Luroth.0.RatFunc.Luroth.c_ne_zero : ∀ {K : Type u_1} [inst : Field K] {E : IntermediateField K (RatFunc K)}, E ≠ ⊥ → RatFunc.Luroth.c✝ E ≠ 0
-- Init.Data.List.Int.Prod
List.prod_replicate_int : ∀ {n : ℕ} {a : ℤ}, (List.replicate n a).prod = a ^ n
-- Aesop.RuleSet.Member
Aesop.BaseRuleSetMember.name : Aesop.BaseRuleSetMember → Aesop.RuleName
-- Init.Data.String.Extra
/-- Consistently de-indents the lines in a string, removing the same amount of leading whitespace from
each line such that the least-indented line has no leading whitespace.

The number of leading whitespace characters to remove from each line is determined by counting the
number of leading space (`' '`) and tab (`'\t'`) characters on lines after the first line that also
contain non-whitespace characters. No distinction is made between tab and space characters; both
count equally.

The least number of leading whitespace characters found is then removed from the beginning of each
line. The first line's leading whitespace is not counted when determining how far to de-indent the
string, but leading whitespace is removed from it.

Examples:
* `"Here:\n  fun x =>\n    x + 1".removeLeadingSpaces = "Here:\nfun x =>\n  x + 1"`
* `"Here:\n\t\tfun x =>\n\t  \tx + 1".removeLeadingSpaces = "Here:\nfun x =>\n \tx + 1"`
* `"Here:\n\t\tfun x =>\n \n\t  \tx + 1".removeLeadingSpaces = "Here:\nfun x =>\n\n \tx + 1"`
 -/
String.removeLeadingSpaces : String → String
-- Lean.Meta.Tactic.ElimInfo
Lean.Meta.CustomEliminator.mk : Bool → Array Lean.Name → Lean.Name → Lean.Meta.CustomEliminator
-- Mathlib.Algebra.Polynomial.Derivative
Polynomial.iterate_derivative_eq_sum : ∀ {R : Type u} [inst : Semiring R] (p : Polynomial R) (k : ℕ),
  (⇑Polynomial.derivative)^[k] p =
    ∑ x ∈ ((⇑Polynomial.derivative)^[k] p).support,
      Polynomial.C ((x + k).descFactorial k • p.coeff (x + k)) * Polynomial.X ^ x
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.coe_add : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : AddZeroClass β]
  [inst_3 : ContinuousAdd β] (f g : CompactlySupportedContinuousMap α β), ⇑(f + g) = ⇑f + ⇑g
-- Mathlib.Analysis.Normed.Algebra.Spectrum
_private.Mathlib.Analysis.Normed.Algebra.Spectrum.0.termσ : Lean.ParserDescr
-- Aesop.Tree.ExtractProof
_private.Aesop.Tree.ExtractProof.0.Aesop.SafePrefixM : Type → Type
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.BinaryBiproductData.mk.injEq : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {P Q : C} (bicone : CategoryTheory.Limits.BinaryBicone P Q) (isBilimit : bicone.IsBilimit)
  (bicone_1 : CategoryTheory.Limits.BinaryBicone P Q) (isBilimit_1 : bicone_1.IsBilimit),
  ({ bicone := bicone, isBilimit := isBilimit } = { bicone := bicone_1, isBilimit := isBilimit_1 }) =
    (bicone = bicone_1 ∧ isBilimit ≍ isBilimit_1)
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.Option.any_dmap : ∀ {α : Type u_1} {β : Type u_2} {x : Option α} {f : (a : α) → x = some a → β} {p : β → Bool},
  Option.any p (Std.Internal.List.Option.dmap✝ x f) =
    Option.any
      (fun x_1 =>
        match x_1 with
        | ⟨a, h⟩ => p (f a h))
      x.attach
-- Std.Do.Triple.SpecLemmas
List.Cursor.mk.injEq : ∀ {α : Type u} {l : List α} («prefix» suffix : List α) (property : «prefix» ++ suffix = l) (prefix_1 suffix_1 : List α)
  (property_1 : prefix_1 ++ suffix_1 = l),
  ({ «prefix» := «prefix», suffix := suffix, property := property } =
      { «prefix» := prefix_1, suffix := suffix_1, property := property_1 }) =
    («prefix» = prefix_1 ∧ suffix = suffix_1)
-- Mathlib.Analysis.Calculus.Deriv.Linear
ContinuousLinearMap.derivWithin : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {x : 𝕜} {s : Set 𝕜} (e : 𝕜 →L[𝕜] F), UniqueDiffWithinAt 𝕜 s x → derivWithin (⇑e) s x = e 1
-- Mathlib.Analysis.Complex.Exponential
Complex.norm_exp_sub_one_sub_id_le : ∀ {x : ℂ}, ‖x‖ ≤ 1 → ‖Complex.exp x - 1 - x‖ ≤ ‖x‖ ^ 2
-- Mathlib.Order.RelClasses
/-- **Alias** of `Eq.subset`.

---

Set notation form of `Eq.le` -/
Eq.subset' : ∀ {α : Type u_1} [UsesSetNotationForOrder α] [inst : Preorder α] {a b : α}, a = b → a ⊆ b
-- Mathlib.Algebra.Order.Group.Abs
mabs_mul_eq_mul_mabs_iff : ∀ {G : Type u_1} [inst : CommGroup G] [inst_1 : LinearOrder G] [IsOrderedMonoid G] (a b : G),
  |a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1
-- Mathlib.GroupTheory.Nilpotent
Subgroup.upperCentralSeriesAux.eq_1 : ∀ (G : Type u_1) [inst : Group G], Subgroup.upperCentralSeriesAux G 0 = ⟨⊥, ⋯⟩
-- Mathlib.Algebra.Algebra.NonUnitalHom
NonUnitalAlgHom.coe_inl : ∀ {R : Type u} [inst : Monoid R] {A : Type v} {B : Type w} [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : DistribMulAction R A] [inst_3 : NonUnitalNonAssocSemiring B] [inst_4 : DistribMulAction R B],
  ⇑(NonUnitalAlgHom.inl R A B) = fun x => (x, 0)
-- Mathlib.Algebra.TrivSqZeroExt.Basic
/-- The second element of a product $\prod_{i=0}^n (r_i + m_i)$ is a sum of terms of the form
$r_0\cdots r_{i-1}m_ir_{i+1}\cdots r_n$.  -/
TrivSqZeroExt.snd_list_prod : ∀ {R : Type u} {M : Type v} [inst : Monoid R] [inst_1 : AddCommMonoid M] [inst_2 : DistribMulAction R M]
  [inst_3 : DistribMulAction Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M] (l : List (TrivSqZeroExt R M)),
  l.prod.snd =
    (List.map
        (fun x =>
          MulOpposite.op (List.drop x.2.succ (List.map TrivSqZeroExt.fst l)).prod •
            (List.take x.2 (List.map TrivSqZeroExt.fst l)).prod • x.1.snd)
        l.zipIdx).sum
-- Lean.Language.Basic
/-- Composes an outer transformation with a snapshot-transform pair.  -/
Lean.Language.TransformedSnap.compose : {α : Type} → Lean.Language.SnapshotTreeTransform → Lean.Language.TransformedSnap α → Lean.Language.TransformedSnap α
-- Init.Grind.Offset
Lean.Grind.Nat.le_ro : ∀ (u w v k : ℕ), u ≤ w → w ≤ v + k → u ≤ v + k
-- Mathlib.CategoryTheory.Shift.CommShift
CategoryTheory.NatTrans.CommShiftCore.add : ∀ {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] {F₁ F₂ : CategoryTheory.Functor C D} {τ : F₁ ⟶ F₂} {A : Type u_5}
  [inst_2 : AddMonoid A] [inst_3 : CategoryTheory.HasShift C A] [inst_4 : CategoryTheory.HasShift D A]
  [inst_5 : F₁.CommShift A] [inst_6 : F₂.CommShift A] {a b : A},
  CategoryTheory.NatTrans.CommShiftCore τ a →
    CategoryTheory.NatTrans.CommShiftCore τ b → CategoryTheory.NatTrans.CommShiftCore τ (a + b)
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.RxoIterator.step.match_1.eq_2 : ∀ {α : Type u_1} {β : α → Type u_2} [inst : Ord α] (motive : Std.DTreeMap.Internal.RxoIterator α β → Sort u_3) (k : α)
  (v : β k) (t : Std.DTreeMap.Internal.Impl α β) (it : Std.DTreeMap.Internal.Zipper α β) (upper : α)
  (h_1 : (upper : α) → motive { iter := Std.DTreeMap.Internal.Zipper.done, upper := upper })
  (h_2 :
    (k : α) →
      (v : β k) →
        (t : Std.DTreeMap.Internal.Impl α β) →
          (it : Std.DTreeMap.Internal.Zipper α β) →
            (upper : α) → motive { iter := Std.DTreeMap.Internal.Zipper.cons k v t it, upper := upper }),
  (match { iter := Std.DTreeMap.Internal.Zipper.cons k v t it, upper := upper } with
    | { iter := Std.DTreeMap.Internal.Zipper.done, upper := upper } => h_1 upper
    | { iter := Std.DTreeMap.Internal.Zipper.cons k v t it, upper := upper } => h_2 k v t it upper) =
    h_2 k v t it upper
-- Mathlib.Algebra.Group.Units.Basic
AddLeftCancelMonoid.eq_zero_of_add_left : ∀ {α : Type u} [inst : AddLeftCancelMonoid α] [Subsingleton (AddUnits α)] {a b : α}, a + b = 0 → b = 0
-- Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
BoundedContinuousFunction.innerProbChar.eq_1 : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] (t : E),
  BoundedContinuousFunction.innerProbChar t = BoundedContinuousFunction.char Real.continuous_probChar ⋯ t
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Real
AEMeasurable.coe_nnreal_ennreal : ∀ {α : Type u_1} {mα : MeasurableSpace α} {f : α → NNReal} {μ : MeasureTheory.Measure α},
  AEMeasurable f μ → AEMeasurable (fun x => ↑(f x)) μ
-- Lean.Meta.Injective
_private.Lean.Meta.Injective.0.Lean.Meta.throwInjectiveTheoremFailure : {α : Type} → Lean.Name → Lean.MVarId → Lean.MetaM α
-- Mathlib.Order.Atoms
IsAtom.eq_1 : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : OrderBot α] (a : α), IsAtom a = (a ≠ ⊥ ∧ ∀ b < a, b = ⊥)
-- Mathlib.Algebra.Ring.Defs
/-- Typeclass for a negation operator that distributes across multiplication.

This is useful for dealing with submonoids of a ring that contain `-1` without having to duplicate
lemmas.  -/
HasDistribNeg : (α : Type u_1) → [Mul α] → Type u_1
-- Mathlib.LinearAlgebra.BilinearMap
/-- Create a bilinear map from a function that is semilinear in each component.
See `mk₂'` and `mk₂` for the linear case.  -/
LinearMap.mk₂'ₛₗ : {R : Type u_1} →
  {R₂ : Type u_2} →
    {S : Type u_3} →
      {S₂ : Type u_4} →
        [inst : Semiring R] →
          [inst_1 : Semiring R₂] →
            [inst_2 : Semiring S] →
              [inst_3 : Semiring S₂] →
                {M : Type u_5} →
                  {N : Type u_7} →
                    {P : Type u_9} →
                      [inst_4 : AddCommMonoid M] →
                        [inst_5 : AddCommMonoid N] →
                          [inst_6 : AddCommMonoid P] →
                            [inst_7 : Module R M] →
                              [inst_8 : Module S N] →
                                [inst_9 : Module R₂ P] →
                                  [inst_10 : Module S₂ P] →
                                    [inst_11 : SMulCommClass S₂ R₂ P] →
                                      (ρ₁₂ : R →+* R₂) →
                                        (σ₁₂ : S →+* S₂) →
                                          (f : M → N → P) →
                                            (∀ (m₁ m₂ : M) (n : N), f (m₁ + m₂) n = f m₁ n + f m₂ n) →
                                              (∀ (c : R) (m : M) (n : N), f (c • m) n = ρ₁₂ c • f m n) →
                                                (∀ (m : M) (n₁ n₂ : N), f m (n₁ + n₂) = f m n₁ + f m n₂) →
                                                  (∀ (c : S) (m : M) (n : N), f m (c • n) = σ₁₂ c • f m n) →
                                                    M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P
-- Mathlib.NumberTheory.NumberField.EquivReindex
NumberField.inverse_basisMatrix_mulVec_eq_repr : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] [inst_2 : DecidableEq (K →+* ℂ)]
  (α : NumberField.RingOfIntegers K) (i : K →+* ℂ),
  (NumberField.basisMatrix K).transpose⁻¹.mulVec
      (fun j => (NumberField.canonicalEmbedding K) ((algebraMap (NumberField.RingOfIntegers K) K) α) j) i =
    ↑((((NumberField.integralBasis K).reindex (NumberField.equivReindex K).symm).repr ↑α) i)
-- Mathlib.Data.Matrix.Block
Matrix.blockDiagonal_apply : ∀ {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} [inst : DecidableEq o] [inst_1 : Zero α]
  (M : o → Matrix m n α) (ik : m × o) (jk : n × o),
  Matrix.blockDiagonal M ik jk = if ik.2 = jk.2 then M ik.2 ik.1 jk.1 else 0
-- Mathlib.Algebra.Polynomial.Splits
Polynomial.Splits.of_degree_le_one_of_monic : ∀ {R : Type u_1} [inst : Semiring R] {f : Polynomial R}, f.degree ≤ 1 → f.Monic → f.Splits
-- Mathlib.Algebra.Homology.ExactSequenceFour
CategoryTheory.ComposableArrows.Exact.cokerIsoKer'_hom_inv_id : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Balanced C] {n : ℕ} {S : CategoryTheory.ComposableArrows C (n + 3)} (hS : S.Exact) (k : ℕ)
  (hk : k ≤ n) (cc : CategoryTheory.Limits.CokernelCofork (S.map' k (k + 1) ⋯ ⋯))
  (kf : CategoryTheory.Limits.KernelFork (S.map' (k + 2) (k + 3) ⋯ ⋯)) (hcc : CategoryTheory.Limits.IsColimit cc)
  (hkf : CategoryTheory.Limits.IsLimit kf),
  CategoryTheory.CategoryStruct.comp (hS.cokerToKer' k hk cc kf hcc hkf) (hS.cokerIsoKer' k hk cc kf hcc hkf).inv =
    CategoryTheory.CategoryStruct.id cc.pt
-- Mathlib.CategoryTheory.Sites.Point.Conservative
/-- [Stacks Tag 00YL](https://stacks.math.columbia.edu/tag/00YL) ((1)) -/
CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.jointlyReflectMonomorphisms : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  {P : CategoryTheory.ObjectProperty J.Point},
  P.IsConservativeFamilyOfPoints →
    ∀ (A : Type u') [inst_1 : CategoryTheory.Category.{v', u'} A] [CategoryTheory.LocallySmall.{w, v, u} C]
      [inst_3 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] {FC : A → A → Type u_1} {CC : A → Type w}
      [inst_4 : (X Y : A) → FunLike (FC X Y) (CC X) (CC Y)] [inst_5 : CategoryTheory.ConcreteCategory A FC]
      [(CategoryTheory.forget A).ReflectsIsomorphisms]
      [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', w, u', w + 1} (CategoryTheory.forget A)]
      [hJ : J.HasSheafCompose (CategoryTheory.forget A)] [CategoryTheory.AB5OfSize.{w, w, v', u'} A]
      [CategoryTheory.Limits.HasFiniteLimits A], CategoryTheory.JointlyReflectMonomorphisms fun Φ => Φ.obj.sheafFiber
-- Mathlib.Algebra.Group.Torsion
pow_eq_one_iff_right : ∀ {M : Type u_1} [inst : Monoid M] [IsMulTorsionFree M] {n : ℕ} {a : M}, a ≠ 1 → (a ^ n = 1 ↔ n = 0)
-- Mathlib.Algebra.Order.Nonneg.Field
nnqsmul_nonneg : ∀ {α : Type u_1} [inst : Semifield α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {a : α} (q : ℚ≥0),
  0 ≤ a → 0 ≤ q • a
-- Mathlib.Tactic.ClickSuggestions.SectionState
Mathlib.Tactic.ClickSuggestions.SectionKind.imported : Mathlib.Tactic.ClickSuggestions.SectionKind
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
EulerSine.tendsto_integral_cos_pow_mul_div : ∀ {f : ℝ → ℂ},
  ContinuousOn f (Set.Icc 0 (Real.pi / 2)) →
    Filter.Tendsto
      (fun n => (∫ (x : ℝ) in 0..Real.pi / 2, ↑(Real.cos x) ^ n * f x) / ↑(∫ (x : ℝ) in 0..Real.pi / 2, Real.cos x ^ n))
      Filter.atTop (nhds (f 0))
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.delayImage : String → Lean.StrLit → Lean.ElabInline
-- Mathlib.RingTheory.AdicCompletion.Algebra
AdicCompletion.liftRingHom.congr_simp : ∀ {R : Type u_4} {S : Type u_5} [inst : NonAssocSemiring R] [inst_1 : CommRing S] (I : Ideal S)
  (f f_1 : (n : ℕ) → R →+* S ⧸ I ^ n) (e_f : f = f_1)
  (hf : ∀ {m n : ℕ} (hle : m ≤ n), (Ideal.Quotient.factorPow I hle).comp (f n) = f m),
  AdicCompletion.liftRingHom I f hf = AdicCompletion.liftRingHom I f_1 ⋯
-- Mathlib.Algebra.Module.Equiv.Defs
LinearEquiv.apply_symm_apply : ∀ {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₂) (c : M₂),
  e (e.symm c) = c
-- Mathlib.Data.Seq.Basic
_private.Mathlib.Data.Seq.Basic.0.Stream'.Seq1.toSeq.match_1.eq_1 : ∀ {α : Type u_1} (motive : Stream'.Seq1 α → Sort u_2) (a : α) (s : Stream'.Seq α)
  (h_1 : (a : α) → (s : Stream'.Seq α) → motive (a, s)),
  (match (a, s) with
    | (a, s) => h_1 a s) =
    h_1 a s
-- Batteries.Data.Char.Basic
Char.all.eq_1 : ∀ (p : Char → Bool),
  Char.all p =
    ((Char.minSurrogate.all fun c h₁ => p (Char.ofNatAux c ⋯)) &&
      (Char.max - Char.maxSurrogate).all fun c h₂ => p (Char.ofNatAux (c + (Char.maxSurrogate + 1)) ⋯))
-- Init.Data.Int.Order
Int.neg_neg_iff_pos : ∀ {a : ℤ}, -a < 0 ↔ 0 < a
-- Mathlib.Topology.UniformSpace.Equicontinuity
Filter.HasBasis.equicontinuousAt_iff : ∀ {ι : Type u_1} {X : Type u_3} {α : Type u_6} [tX : TopologicalSpace X] [uα : UniformSpace α] {κ₁ : Type u_11}
  {κ₂ : Type u_12} {p₁ : κ₁ → Prop} {s₁ : κ₁ → Set X} {p₂ : κ₂ → Prop} {s₂ : κ₂ → Set (α × α)} {F : ι → X → α} {x₀ : X},
  (nhds x₀).HasBasis p₁ s₁ →
    (uniformity α).HasBasis p₂ s₂ →
      (EquicontinuousAt F x₀ ↔ ∀ (k₂ : κ₂), p₂ k₂ → ∃ k₁, p₁ k₁ ∧ ∀ x ∈ s₁ k₁, ∀ (i : ι), (F i x₀, F i x) ∈ s₂ k₂)
-- Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
iteratedDerivWithin_smul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {n : ℕ} {x : 𝕜} {s : Set 𝕜},
  x ∈ s →
    UniqueDiffOn 𝕜 s →
      ∀ {𝔸 : Type u_5} [inst_3 : NormedRing 𝔸] [inst_4 : NormedAlgebra 𝕜 𝔸] [inst_5 : Module 𝔸 F] [IsBoundedSMul 𝔸 F]
        [IsScalarTower 𝕜 𝔸 F] {f : 𝕜 → 𝔸} {g : 𝕜 → F},
        ContDiffWithinAt 𝕜 (↑n) f s x →
          ContDiffWithinAt 𝕜 (↑n) g s x →
            iteratedDerivWithin n (f • g) s x =
              ∑ i ∈ Finset.range (n + 1), n.choose i • iteratedDerivWithin i f s x • iteratedDerivWithin (n - i) g s x
-- Mathlib.LinearAlgebra.BilinearForm.Properties
LinearMap.BilinForm.IsRefl.eq_zero : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {B : LinearMap.BilinForm R M}, B.IsRefl → ∀ {x y : M}, (B x) y = 0 → (B y) x = 0
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.Entry.funCC.inj : ∀ {declName declName_1 : Lean.Name},
  Lean.Meta.Grind.Entry.funCC declName = Lean.Meta.Grind.Entry.funCC declName_1 → declName = declName_1
-- Lean.Meta.MethodSpecs
_private.Lean.Meta.MethodSpecs.0.Lean.genSpecs.doRealize : Lean.Name → Lean.MetaM Unit
-- Mathlib.NumberTheory.Real.GoldenRatio
/-- The characteristic polynomial of `fibRec` is `X² - (X + 1)`.  -/
Real.fibRec_charPoly_eq : ∀ {β : Type u_2} [inst : CommRing β], Real.fibRec.charPoly = Polynomial.X ^ 2 - (Polynomial.X + 1)
-- Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric
_private.Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric.0.Complex.multiset_prod_div_multiset_prod_mul : ∀ {n : ℕ} (a b : Multiset ℂ),
  n ≠ 0 →
    (Multiset.map (fun x => x + ↑n) a).prod / ((Multiset.map (fun x => x + ↑n) b).prod * (↑n + 1)) =
      ↑n ^ (↑a.card - ↑b.card - 1) * (Multiset.map (fun x => x / ↑n + 1) a).prod /
        ((Multiset.map (fun x => x / ↑n + 1) b).prod * (1 + (↑n)⁻¹))
-- Mathlib.NumberTheory.ClassNumber.Finite
ClassGroup.finsetApprox.eq_1 : ∀ {R : Type u_1} {S : Type u_2} [inst : EuclideanDomain R] [inst_1 : CommRing S] [inst_2 : IsDomain S]
  [inst_3 : Algebra R S] {abv : AbsoluteValue R ℤ} {ι : Type u_5} [inst_4 : DecidableEq ι] [inst_5 : Fintype ι]
  (bS : Module.Basis ι R S) (adm : abv.IsAdmissible) [inst_6 : Infinite R] [inst_7 : DecidableEq R],
  ClassGroup.finsetApprox bS adm =
    (Finset.image (fun xy => (ClassGroup.distinctElems bS adm) xy.1 - (ClassGroup.distinctElems bS adm) xy.2)
          Finset.univ).erase
      0
-- Mathlib.Analysis.Normed.Module.FiniteDimension
/-- **Riesz's theorem**: if a closed ball of positive radius is compact in a vector space, then the
space is finite-dimensional.  -/
FiniteDimensional.of_isCompact_closedBall : ∀ (𝕜 : Type u) [inst : NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] {V : Type u_1} [inst_2 : NormedAddCommGroup V]
  [inst_3 : Module 𝕜 V] [ContinuousSMul 𝕜 V] {r : ℝ},
  0 < r → ∀ {c : V}, IsCompact (Metric.closedBall c r) → FiniteDimensional 𝕜 V
-- Mathlib.Geometry.Manifold.LocalInvariantProperties
StructureGroupoid.LocalInvariantProp.liftPropWithinAt_congr_of_eventuallyEq : ∀ {H : Type u_1} {M : Type u_2} {H' : Type u_3} {M' : Type u_4} [inst : TopologicalSpace H]
  [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M] [inst_3 : TopologicalSpace H']
  [inst_4 : TopologicalSpace M'] [inst_5 : ChartedSpace H' M'] {G : StructureGroupoid H} {G' : StructureGroupoid H'}
  {P : (H → H') → Set H → H → Prop} {g g' : M → M'} {s : Set M} {x : M},
  G.LocalInvariantProp G' P →
    ChartedSpace.LiftPropWithinAt P g s x →
      g' =ᶠ[nhdsWithin x s] g → g' x = g x → ChartedSpace.LiftPropWithinAt P g' s x
-- Mathlib.Algebra.GroupWithZero.Associated
associated_mul_unit_right_iff : ∀ {N : Type u_2} [inst : Monoid N] {a b : N} {u : Nˣ}, Associated a (b * ↑u) ↔ Associated a b
-- Mathlib.RingTheory.PowerSeries.Log
PowerSeries.logOf_eq : ∀ {A : Type u_1} [inst : CommRing A] [inst_1 : Algebra ℚ A] (f : PowerSeries A),
  f.logOf = PowerSeries.subst (f - 1) (PowerSeries.log A)
-- Mathlib.Probability.Distributions.Binomial
ProbabilityTheory.map_cast_binomial_real_self : ∀ {R : Type u_1} [inst : MeasurableSpace R] [inst_1 : AddMonoidWithOne R] [MeasurableSingletonClass R] [CharZero R]
  (n : ℕ) (p : ↑unitInterval), (MeasureTheory.Measure.map Nat.cast (ProbabilityTheory.binomial n p)).real {↑n} = ↑p ^ n
-- Mathlib.Combinatorics.SimpleGraph.Density
Rel.interedges_disjoint_right : ∀ {α : Type u_4} {β : Type u_5} (r : α → β → Prop) [inst : (a : α) → DecidablePred (r a)] (s : Finset α)
  {t t' : Finset β}, Disjoint t t' → Disjoint (Rel.interedges r s t) (Rel.interedges r s t')
-- Mathlib.Topology.Order.NhdsSet
Iio_mem_nhdsSet_Iic_iff : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderClosedTopology α] {a b : α},
  Set.Iio b ∈ nhdsSet (Set.Iic a) ↔ a < b
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.vietoris.isPreconnected_nonempty_finite_subsets : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α},
  IsPreconnected s → IsPreconnected {t | t.Nonempty ∧ t.Finite ∧ t ⊆ s}
-- Lean.Data.PersistentHashMap
Lean.PersistentHashMap.empty : {α : Type u_1} → {β : Type u_2} → [inst : BEq α] → [inst_1 : Hashable α] → Lean.PersistentHashMap α β
-- Mathlib.AlgebraicGeometry.AffineSpace
AlgebraicGeometry.AffineSpace.SpecIso_inv_appTop_coord : ∀ {n : Type u} (R : CommRingCat) (i : n),
  (CategoryTheory.ConcreteCategory.hom
        (AlgebraicGeometry.Scheme.Hom.appTop (AlgebraicGeometry.AffineSpace.SpecIso n R).inv))
      (AlgebraicGeometry.AffineSpace.coord (AlgebraicGeometry.Spec R) i) =
    (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑R))).inv)
      (MvPolynomial.X i)
-- Mathlib.Combinatorics.Pigeonhole
/-- The pigeonhole principle for finitely many pigeons counted by weight, non-strict inequality
version: if the total weight of a finite set of pigeons is greater than or equal to `n • b`, they
are sorted into some pigeonholes, and for all but `n > 0` pigeonholes the total weight of the
pigeons there is nonpositive, then for at least one of these `n` pigeonholes, the total weight of
the pigeons in this pigeonhole is greater than or equal to `b`.  -/
Finset.exists_le_sum_fiber_of_sum_fiber_nonpos_of_nsmul_le_sum : ∀ {α : Type u} {β : Type v} {M : Type w} [inst : DecidableEq β] {s : Finset α} {t : Finset β} {f : α → β} {w : α → M}
  {b : M} [inst_1 : AddCommMonoid M] [inst_2 : LinearOrder M] [IsOrderedCancelAddMonoid M],
  (∀ y ∉ t, ∑ x ∈ s with f x = y, w x ≤ 0) →
    t.Nonempty → t.card • b ≤ ∑ x ∈ s, w x → ∃ y ∈ t, b ≤ ∑ x ∈ s with f x = y, w x