mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Finiteness.Finsupp
Module.Finite.of_submodule_quotient : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (N : Submodule R M)
  [Module.Finite R ↥N] [Module.Finite R (M ⧸ N)], Module.Finite R M
-- Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
fourierIntegral_gaussian : ∀ {b : ℂ},
  0 < b.re →
    ∀ (t : ℂ),
      ∫ (x : ℝ), Complex.exp (Complex.I * t * ↑x) * Complex.exp (-b * ↑x ^ 2) =
        (↑Real.pi / b) ^ (1 / 2) * Complex.exp (-t ^ 2 / (4 * b))
-- Mathlib.Analysis.Analytic.ConvergenceRadius
/-- If the radius of `p` is positive, then `‖pₙ‖` grows at most geometrically.  -/
FormalMultilinearSeries.le_mul_pow_of_radius_pos : ∀ {𝕜 : Type u_1} {E : Type u_3} {F : Type u_4} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  (p : FormalMultilinearSeries 𝕜 E F), 0 < p.radius → ∃ C r, ∃ (_ : 0 < C) (_ : 0 < r), ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n
-- Mathlib.Data.Finsupp.Single
Finsupp.card_support_le_one : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] [Nonempty α] {f : α →₀ M}, f.support.card ≤ 1 ↔ ∃ a, f = fun₀ | a => f a
-- Mathlib.Topology.Constructions.SumProd
continuous_sumMap : ∀ {X : Type u} {Y : Type v} {W : Type u_1} {Z : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace W] [inst_3 : TopologicalSpace Z] {f : X → Y} {g : Z → W},
  Continuous (Sum.map f g) ↔ Continuous f ∧ Continuous g
-- Mathlib.Data.Quot
/-- Places an element of a type into the quotient that equates terms according to the provided relation.

Given `v : α` and relation `r : α → α → Prop`, `Quot.mk r v : Quot r` is like `v`, except all
observations of `v`'s value must respect `r`.

`Quot.mk` is a built-in primitive:
 * `Quot` is the built-in quotient type.
 * `Quot.lift` allows the definition of functions from the quotient to some other type.
 * `Quot.sound` asserts the equality of elements related by `r`.
 * `Quot.ind` is used to write proofs about quotients by assuming that all elements are constructed
   with `Quot.mk`.
 -/
_private.Mathlib.Data.Quot.0.Quot.«term⟦_⟧» : Lean.ParserDescr
-- Std.Sat.CNF.RelabelFin
Std.Sat.CNF.of_maxLiteral_eq_some' : ∀ {maxLit localMax : ℕ} (f : Std.Sat.CNF ℕ),
  f.maxLiteral = some maxLit → ∀ clause ∈ f, clause.maxLiteral = some localMax → localMax ≤ maxLit
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.Impl.toList_pruneLE : ∀ {α : Type u_1} {β : α → Type u_2} [inst : Ord α] [Std.TransOrd α] (t : Std.DTreeMap.Internal.Impl α β),
  t.Ordered →
    ∀ (lowerBound : α),
      (Std.DTreeMap.Internal.Impl.pruneLE✝ t lowerBound).toList =
        List.filter (fun e => (compare e.fst lowerBound).isGE) t.toList
-- Mathlib.CategoryTheory.Limits.Shapes.Products
/-- A colimit cocone for `X : Discrete α ⥤ C` that is given
by `∐ (fun j => X.obj (Discrete.mk j))`.  -/
CategoryTheory.Limits.Sigma.cocone : {α : Type w₂} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      (X : CategoryTheory.Functor (CategoryTheory.Discrete α) C) →
        [CategoryTheory.Limits.HasCoproduct fun j => X.obj { as := j }] → CategoryTheory.Limits.Cocone X
-- Std.Data.DTreeMap.Raw.Basic
/-- Tries to retrieve the key-value pair with the largest key that is less than the given key,
returning `none` if no such pair exists.
 -/
Std.DTreeMap.Raw.getEntryLT? : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → Std.DTreeMap.Raw α β cmp → α → Option ((a : α) × β a)
-- Mathlib.CategoryTheory.Limits.Filtered
CategoryTheory.Limits.hasColimitsOfShape_of_has_filtered_colimits : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasFilteredColimitsOfSize.{w', w, v, u} C] (I : Type w)
  [inst_2 : CategoryTheory.Category.{w', w} I] [CategoryTheory.IsFiltered I],
  CategoryTheory.Limits.HasColimitsOfShape I C
-- Std.Tactic.BVDecide.LRAT.Parser
_private.Std.Tactic.BVDecide.LRAT.Parser.0.Std.Tactic.BVDecide.LRAT.lratProofToBinary.zeroByte : ByteArray → ByteArray
-- Lean.Elab.InfoTree.Types
/-- Name of the projection.  -/
Lean.Elab.FieldInfo.projName : Lean.Elab.FieldInfo → Lean.Name
-- Mathlib.Algebra.Ring.Submonoid.Pointwise
/-- For `M : Submonoid R` and `N : AddSubmonoid A`, `M • N` is the additive submonoid
generated by all `m • n` where `m ∈ M` and `n ∈ N`.  -/
AddSubmonoid.smul : {R : Type u_2} →
  {A : Type u_3} →
    [inst : AddMonoid R] → [inst_1 : AddMonoid A] → [DistribSMul R A] → SMul (AddSubmonoid R) (AddSubmonoid A)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getKey!_insertMany!_list_of_contains_eq_false : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  [inst : BEq α] [Std.LawfulBEqOrd α] [inst_2 : Inhabited α],
  t.WF →
    ∀ {l : List (α × β)} {k : α},
      (List.map Prod.fst l).contains k = false →
        (↑(Std.DTreeMap.Internal.Impl.Const.insertMany! t l)).getKey! k = t.getKey! k
-- Init.Data.String.Slice
/-- If `pat` matches a prefix at `pos`, returns the position after the end of the match.
Returns `none` otherwise.

This function is generic over all currently supported patterns.
 -/
String.Slice.Pos.skip? : {ρ : Type} → {s : String.Slice} → s.Pos → (pat : ρ) → [String.Slice.Pattern.ForwardPattern pat] → Option s.Pos
-- Std.Time.Date.Unit.Weekday
_private.Std.Time.Date.Unit.Weekday.0.Std.Time.instReprWeekday.repr.match_1.eq_2 : ∀ (motive : Std.Time.Weekday → Sort u_1) (h_1 : Unit → motive Std.Time.Weekday.monday)
  (h_2 : Unit → motive Std.Time.Weekday.tuesday) (h_3 : Unit → motive Std.Time.Weekday.wednesday)
  (h_4 : Unit → motive Std.Time.Weekday.thursday) (h_5 : Unit → motive Std.Time.Weekday.friday)
  (h_6 : Unit → motive Std.Time.Weekday.saturday) (h_7 : Unit → motive Std.Time.Weekday.sunday),
  (match Std.Time.Weekday.tuesday with
    | Std.Time.Weekday.monday => h_1 ()
    | Std.Time.Weekday.tuesday => h_2 ()
    | Std.Time.Weekday.wednesday => h_3 ()
    | Std.Time.Weekday.thursday => h_4 ()
    | Std.Time.Weekday.friday => h_5 ()
    | Std.Time.Weekday.saturday => h_6 ()
    | Std.Time.Weekday.sunday => h_7 ()) =
    h_2 ()
-- Mathlib.MeasureTheory.VectorMeasure.Integral
MeasureTheory.VectorMeasure.Integrable.neg : ∀ {X : Type u_2} {E : Type u_4} {F : Type u_5} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup F] {f : X → E} {μ : MeasureTheory.VectorMeasure X F}, μ.Integrable f → μ.Integrable (-f)
-- Mathlib.FieldTheory.Perfect
frobeniusEquiv_symm_apply_frobenius : ∀ (R : Type u_1) (p : ℕ) [inst : CommSemiring R] [inst_1 : ExpChar R p] [inst_2 : PerfectRing R p] (x : R),
  (frobeniusEquiv R p).symm ((frobenius R p) x) = x
-- Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal
PositiveLinearMap.gnsNonUnitalStarAlgHom_apply : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] (f : A →ₚ[ℂ] ℂ) [inst_2 : StarOrderedRing A]
  {a : A}, f.gnsNonUnitalStarAlgHom a = (f.leftMulMapPreGNS a).completion
-- Mathlib.RingTheory.PicardGroup
Module.Invertible.rank_eq_one : ∀ (R : Type u) (M : Type v) [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [Module.Invertible R M] [Module.Free R M], Module.rank R M = 1
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.erasePTR.go.eq_1 : ∀ {α : Type u_1} (p : α → Bool) (l : List α) (a : Array α), List.erasePTR.go✝ p l [] a = l
-- Mathlib.LinearAlgebra.Finsupp.LSum
/-- An equivalence of domain and a linear equivalence of codomain induce a linear equivalence of the
corresponding finitely supported functions.  -/
Finsupp.lcongr : {M : Type u_2} →
  {N : Type u_3} →
    {R : Type u_5} →
      {R₂ : Type u_6} →
        [inst : Semiring R] →
          [inst_1 : Semiring R₂] →
            [inst_2 : AddCommMonoid M] →
              [inst_3 : Module R M] →
                [inst_4 : AddCommMonoid N] →
                  [inst_5 : Module R₂ N] →
                    {σ : R →+* R₂} →
                      {σ_inv : R₂ →+* R} →
                        [inst_6 : RingHomInvPair σ σ_inv] →
                          [inst_7 : RingHomInvPair σ_inv σ] →
                            {ι : Type u_9} → {κ : Type u_10} → ι ≃ κ → (M ≃ₛₗ[σ] N) → (ι →₀ M) ≃ₛₗ[σ] κ →₀ N
-- Mathlib.CategoryTheory.Monad.Algebra
CategoryTheory.Monad.free_map_f : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C) {X Y : C} (f : X ⟶ Y),
  (T.free.map f).f = T.map f
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Equiv.Perm.subtypePermOfSupport.eq_1 : ∀ {α : Type u_2} [inst : Fintype α] [inst_1 : DecidableEq α] (c : Equiv.Perm α),
  c.subtypePermOfSupport = c.subtypePerm ⋯
-- Mathlib.Analysis.Distribution.TestFunction
/-- Fix a locally convex topology `t` on `𝓓^{n}(Ω, F)`. `t` is coarser than the canonical topology
on `𝓓^{n}(Ω, F)` if and only if it is coarser than the "original topology" given by
`TestFunction.originalTop`.  -/
TestFunction.topologicalSpace_le_iff : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4}
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {n : ℕ∞} {t : TopologicalSpace (TestFunction Ω F n)}
  [IsTopologicalAddGroup (TestFunction Ω F n)] [ContinuousSMul ℝ (TestFunction Ω F n)]
  [LocallyConvexSpace ℝ (TestFunction Ω F n)],
  TestFunction.topologicalSpace Ω F n ≤ t ↔ TestFunction.originalTop Ω F n ≤ t
-- Mathlib.Data.Matrix.Mul
Matrix.vecMul_apply : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : NonUnitalNonAssocSemiring α] [inst_1 : Fintype m] (v : m → α)
  (M : Matrix m n α) (i : n), Matrix.vecMul v M i = v ⬝ᵥ M.col i
-- Mathlib.Order.CompleteBooleanAlgebra
/-- The infimum distributes over the supremum  -/
CompleteBooleanAlgebra.le_sup_inf : ∀ {α : Type u_1} [self : CompleteBooleanAlgebra α] (x y z : α), (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z
-- Mathlib.GroupTheory.Exponent
Monoid.exp_eq_one_of_subsingleton : ∀ {G : Type u} [inst : Monoid G] [hs : Subsingleton G], Monoid.exponent G = 1
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
deriv_sinh : ∀ {f : ℝ → ℝ} {x : ℝ}, DifferentiableAt ℝ f x → deriv (fun x => Real.sinh (f x)) x = Real.cosh (f x) * deriv f x
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Udiv
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Udiv.0.Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.go.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (curr : ℕ) (h_1 : Unit → motive 0) (h_2 : (curr : ℕ) → motive curr.succ),
  (match curr.succ with
    | 0 => h_1 ()
    | curr.succ => h_2 curr) =
    h_2 curr
-- Mathlib.Data.Fin.Basic
/-- Elimination principle for the empty set `Fin 0`, dependent version.  -/
finZeroElim : {α : Fin 0 → Sort u_1} → (x : Fin 0) → α x
-- Mathlib.Combinatorics.SetFamily.FourFunctions
/-- The `n = 1` case of the Ahlswede-Daykin inequality. Note that we can't just expand everything
out and bound termwise since `c₀ * d₁` appears twice on the RHS of the assumptions while `c₁ * d₀`
does not appear.  -/
_private.Mathlib.Combinatorics.SetFamily.FourFunctions.0.ineq : ∀ {β : Type u_2} [inst : CommSemiring β] [inst_1 : LinearOrder β] [IsStrictOrderedRing β] [ExistsAddOfLE β]
  {a₀ a₁ b₀ b₁ c₀ c₁ d₀ d₁ : β},
  0 ≤ a₀ →
    0 ≤ a₁ →
      0 ≤ b₀ →
        0 ≤ b₁ →
          0 ≤ c₀ →
            0 ≤ c₁ →
              0 ≤ d₀ →
                0 ≤ d₁ →
                  a₀ * b₀ ≤ c₀ * d₀ →
                    a₁ * b₀ ≤ c₀ * d₁ →
                      a₀ * b₁ ≤ c₀ * d₁ → a₁ * b₁ ≤ c₁ * d₁ → (a₀ + a₁) * (b₀ + b₁) ≤ (c₀ + c₁) * (d₀ + d₁)
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
/-- The forgetful map from `NonUnitalStarSubalgebra` to `NonUnitalSubalgebra` as an
`OrderEmbedding`  -/
NonUnitalStarSubalgebra.toNonUnitalSubalgebra' : {R : Type u} →
  {A : Type v} →
    [inst : CommSemiring R] →
      [inst_1 : NonUnitalNonAssocSemiring A] →
        [inst_2 : Module R A] → [inst_3 : Star A] → NonUnitalStarSubalgebra R A ↪o NonUnitalSubalgebra R A
-- Init.System.IO
IO.FS.instBEqFileType : BEq IO.FS.FileType
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometry.antilipschitz : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} [inst_2 : SeminormedAddCommGroup E] [inst_3 : SeminormedAddCommGroup E₂] [inst_4 : Module R E]
  [inst_5 : Module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂), AntilipschitzWith 1 ⇑f
-- Mathlib.FieldTheory.Finite.Polynomial
MvPolynomial.indicator_mem_restrictDegree : ∀ {K : Type u_1} {σ : Type u_2} [inst : Fintype K] [inst_1 : Fintype σ] [inst_2 : CommRing K] (c : σ → K),
  MvPolynomial.indicator c ∈ MvPolynomial.restrictDegree σ K (Fintype.card K - 1)
-- Mathlib.Logic.Equiv.List
Encodable.decode_list_succ : ∀ {α : Type u_1} [inst : Encodable α] (v : ℕ),
  Encodable.decode v.succ =
    (fun x1 x2 => x1 :: x2) <$> Encodable.decode (Nat.unpair v).1 <*> Encodable.decode (Nat.unpair v).2
-- Mathlib.Algebra.BigOperators.Fin
Fin.prod_uIcc_succ : ∀ {M : Type u_2} [inst : CommMonoid M] {n : ℕ} (f : Fin (n + 1) → M) (a b : Fin n),
  ∏ i ∈ Finset.uIcc a.succ b.succ, f i = ∏ i ∈ Finset.uIcc a b, f i.succ
-- Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
HomotopicalAlgebra.RightHomotopyClass.precomp_mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C}
  [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C] (f : X ⟶ Y) (g : Y ⟶ Z),
  (HomotopicalAlgebra.RightHomotopyClass.mk g).precomp f =
    HomotopicalAlgebra.RightHomotopyClass.mk (CategoryTheory.CategoryStruct.comp f g)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
mul_le_iff_le_one_right' : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : LE α] [MulLeftMono α] [MulLeftReflectLE α] (a : α) {b : α},
  a * b ≤ a ↔ b ≤ 1
-- Mathlib.NumberTheory.SelbergSieve
/-- A sequence representing how much each element of `support` should be weighted.  -/
BoundingSieve.weights : BoundingSieve → ℕ → ℝ
-- Mathlib.Algebra.Order.SuccPred
Order.IsSuccLimit.add_natCast_lt : ∀ {α : Type u_1} {x y : α} [inst : PartialOrder α] [inst_1 : AddMonoidWithOne α] [SuccAddOrder α],
  Order.IsSuccLimit x → y < x → ∀ (n : ℕ), y + ↑n < x
-- Mathlib.Order.CountableSupClosed
countableInfClosure_univ : ∀ {α : Type u_2} [inst : Preorder α], countableInfClosure Set.univ = Set.univ
-- Mathlib.RepresentationTheory.Intertwining
Representation.TensorProduct.toLinearMap_rid : ∀ {A : Type u_1} {G : Type u_2} {W : Type u_4} [inst : CommSemiring A] [inst_1 : Monoid G] [inst_2 : AddCommMonoid W]
  [inst_3 : Module A W] (σ : Representation A G W),
  (↑(Representation.TensorProduct.rid A σ)).toLinearMap = ↑(TensorProduct.rid A W)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
_private.Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point.0.WeierstrassCurve.Affine.Point.add.match_1.eq_3 : ∀ {F : Type u_1} [inst : Field F] {W : WeierstrassCurve.Affine F} (motive : W.Point → W.Point → Sort u_2) (x₁ y₁ : F)
  (h₁ : W.Nonsingular x₁ y₁) (x₂ y₂ : F) (h₂ : W.Nonsingular x₂ y₂)
  (h_1 : (P : W.Point) → motive WeierstrassCurve.Affine.Point.zero P)
  (h_2 : (P : W.Point) → motive P WeierstrassCurve.Affine.Point.zero)
  (h_3 :
    (x₁ y₁ : F) →
      (h₁ : W.Nonsingular x₁ y₁) →
        (x₂ y₂ : F) →
          (h₂ : W.Nonsingular x₂ y₂) →
            motive (WeierstrassCurve.Affine.Point.some x₁ y₁ h₁) (WeierstrassCurve.Affine.Point.some x₂ y₂ h₂)),
  (match WeierstrassCurve.Affine.Point.some x₁ y₁ h₁, WeierstrassCurve.Affine.Point.some x₂ y₂ h₂ with
    | WeierstrassCurve.Affine.Point.zero, P => h_1 P
    | P, WeierstrassCurve.Affine.Point.zero => h_2 P
    | WeierstrassCurve.Affine.Point.some x₁ y₁ h₁, WeierstrassCurve.Affine.Point.some x₂ y₂ h₂ =>
      h_3 x₁ y₁ h₁ x₂ y₂ h₂) =
    h_3 x₁ y₁ h₁ x₂ y₂ h₂
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.insertManyIfNewUnit_nil : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtDHashMap α fun x => Unit} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α], Std.ExtDHashMap.Const.insertManyIfNewUnit m [] = m
-- Mathlib.Data.Ordering.Basic
Ordering.compares_eq : ∀ {α : Type u_1} [inst : LT α] (a b : α), Ordering.eq.Compares a b = (a = b)
-- Mathlib.GroupTheory.Exponent
Monoid.exponent_pos : ∀ {G : Type u} [inst : Monoid G], 0 < Monoid.exponent G ↔ Monoid.ExponentExists G
-- Lean.Meta.ArgsPacker
_private.Lean.Meta.ArgsPacker.0.Lean.Meta.ArgsPacker.Mutual.mkCodomain.go : Array Lean.Expr → Lean.Level → Lean.Expr → ℕ → Lean.MetaM Lean.Expr
-- Lean.Meta.Tactic.Grind.EMatchAction
_private.Lean.Meta.Tactic.Grind.EMatchAction.0.Lean.Meta.Grind.Action.mkMask : Lean.Meta.Grind.Action.EMatchTheoremIds✝ → Array Lean.Meta.Grind.EMatchTheorem → Lean.CoreM (Array Bool)
-- Init.Data.Array.Lemmas
Array.push_inj_right : ∀ {α : Type u_1} {a b : α} {xs : Array α}, xs.push a = xs.push b ↔ a = b
-- Init.Meta.Defs
Lean.TSyntax.instCoeDepTermMkIdentIdent : {info : Lean.SourceInfo} →
  {ss : Substring.Raw} →
    {n : Lean.Name} →
      {res : List Lean.Syntax.Preresolved} → CoeDep Lean.Term { raw := Lean.Syntax.ident info ss n res } Lean.Ident
-- Mathlib.Algebra.Module.Submodule.Union
Module.Dual.exists_forall_ne_zero_of_forall_exists : ∀ {ι : Type u_1} {K : Type u_2} {M : Type u_3} [inst : Field K] [inst_1 : AddCommGroup M] [inst_2 : Module K M]
  [Finite ι] [Infinite K] (f : ι → Module.Dual K M), (∀ (i : ι), ∃ x, (f i) x ≠ 0) → ∃ x, ∀ (i : ι), (f i) x ≠ 0
-- Mathlib.Tactic.CancelDenoms.Core
/-- Theorems to get expression into a form that `findCancelFactor` and `mkProdPrf`
can more easily handle. These are important for dividing by rationals and negative integers.  -/
Mathlib.Tactic.CancelDenoms.deriveThms : List Lean.Name
-- Batteries.Data.String.Lemmas
_private.Batteries.Data.String.Lemmas.0.String.Legacy.Iterator.nextn.eq_2 : ∀ (x : String.Legacy.Iterator) (n : ℕ), x.nextn n.succ = x.next.nextn n
-- Init.Data.Array.Lemmas
Array.filterMap_push_none : ∀ {α : Type u_1} {β : Type u_2} {stop : ℕ} {f : α → Option β} {a : α} {xs : Array α},
  f a = none → stop = xs.size + 1 → Array.filterMap f (xs.push a) 0 stop = Array.filterMap f xs
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero
SSet.π₀.d_fromChainComplexXZero_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasCoproducts C]
  [inst_2 : CategoryTheory.Preadditive C] (X : SSet) (R : C) (n : ℕ) {Z : C} (h : (∐ fun x => R) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((X.chainComplex R).d n 0)
      (CategoryTheory.CategoryStruct.comp (SSet.π₀.fromChainComplexXZero X R) h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.Algebra.Homology.Embedding.Extend
/-- The extension functor attached to an embedding of complex shapes is fully faithful.  -/
ComplexShape.Embedding.fullyFaithfulExtendFunctor : {ι : Type u_1} →
  {ι' : Type u_2} →
    {c : ComplexShape ι} →
      {c' : ComplexShape ι'} →
        (e : c.Embedding c') →
          (C : Type u_3) →
            [inst : CategoryTheory.Category.{v_1, u_3} C] →
              [inst_1 : CategoryTheory.Limits.HasZeroObject C] →
                [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] → (e.extendFunctor C).FullyFaithful
-- Mathlib.Topology.Path
Path.ext : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X} {γ₁ γ₂ : Path x y}, ⇑γ₁ = ⇑γ₂ → γ₁ = γ₂
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Real.arctan_eq_neg_pi_div_four : ∀ {x : ℝ}, Real.arctan x = -(Real.pi / 4) ↔ x = -1
-- Mathlib.Algebra.Homology.SingleHomology
HomologicalComplex.singleObjOpcyclesSelfIso_hom_naturality : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {ι : Type u_1} [inst_3 : DecidableEq ι] (c : ComplexShape ι) (j : ι)
  {A B : C} (f : A ⟶ B),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.singleObjOpcyclesSelfIso c j A).hom
      (HomologicalComplex.opcyclesMap ((HomologicalComplex.single C c j).map f) j) =
    CategoryTheory.CategoryStruct.comp f (HomologicalComplex.singleObjOpcyclesSelfIso c j B).hom
-- Init.Data.UInt.Lemmas
USize.ofFin_toFin : ∀ (n : USize), USize.ofFin n.toFin = n
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.not_mem_inter_of_not_mem_left : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α}, k ∉ t₁ → k ∉ t₁ ∩ t₂
-- Mathlib.Analysis.Calculus.FDeriv.Mul
HasFDerivWithinAt.mul_const' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : E} {s : Set E} {𝔸 : Type u_5} [inst_3 : NormedRing 𝔸] [inst_4 : NormedAlgebra 𝕜 𝔸]
  {a : E → 𝔸} {a' : E →L[𝕜] 𝔸},
  HasFDerivWithinAt a a' s x → ∀ (b : 𝔸), HasFDerivWithinAt (fun y => a y * b) (MulOpposite.op b • a') s x
-- Mathlib.Analysis.Calculus.FDeriv.Pow
HasStrictFDerivAt.pow : ∀ {𝕜 : Type u_1} {𝔸 : Type u_2} {E : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedCommRing 𝔸]
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedAlgebra 𝕜 𝔸] [inst_4 : NormedSpace 𝕜 E] {f : E → 𝔸} {f' : E →L[𝕜] 𝔸}
  {x : E}, HasStrictFDerivAt f f' x → ∀ (n : ℕ), HasStrictFDerivAt (fun x => f x ^ n) ((n • f x ^ (n - 1)) • f') x
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
ModuleCat.CoextendScalars.smul_apply' : ∀ {R : Type u₁} {S : Type u₂} [inst : Ring R] [inst_1 : Ring S] (f : R →+* S) (M : Type v) [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] (s : S) (g : ↑((ModuleCat.restrictScalars f).obj (ModuleCat.of S S)) →ₗ[R] M) (s' : S),
  (s • g) s' = g (s' * s)
-- Mathlib.Geometry.Manifold.MFDeriv.Tangent
mfderiv_chartAt_eq_tangentCoordChange : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [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] [inst_6 : IsManifold I 1 M] {x y : M},
  x ∈ (chartAt H y).source → mfderiv% ↑(chartAt H y) x = tangentCoordChange I x y x
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
/-- Candidate tensor unit.  -/
CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore.tensorUnit : (C : Type u₁) →
  {inst : CategoryTheory.Category.{v₁, u₁} C} →
    (V : Type u₂) →
      {inst_1 : CategoryTheory.Category.{v₂, u₂} V} →
        {inst_2 : CategoryTheory.MonoidalCategory C} →
          {inst_3 : CategoryTheory.MonoidalCategory V} →
            (D : Type u₃) →
              {inst_4 : CategoryTheory.Category.{v₃, u₃} D} →
                [self : CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore C V D] → D
-- Mathlib.Data.Analysis.Filter
Filter.Realizer.map_F : ∀ {α : Type u_1} {β : Type u_2} (m : α → β) {f : Filter α} (F : f.Realizer) (s : (Filter.Realizer.map m F).σ),
  (Filter.Realizer.map m F).F.f s = m '' F.F.f s
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey?_maxKey! : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α], t ≠ ∅ → t.getKey? t.maxKey! = some t.maxKey!
-- Mathlib.Topology.UniformSpace.UniformEmbedding
Filter.HasBasis.isUniformEmbedding_iff : ∀ {α : Type u} {β : Type v} [inst : UniformSpace α] [inst_1 : UniformSpace β] {ι : Sort u_1} {ι' : Sort u_2}
  {p : ι → Prop} {p' : ι' → Prop} {s : ι → Set (α × α)} {s' : ι' → Set (β × β)},
  (uniformity α).HasBasis p s →
    (uniformity β).HasBasis p' s' →
      ∀ {f : α → β},
        IsUniformEmbedding f ↔
          Function.Injective f ∧
            UniformContinuous f ∧ ∀ (j : ι), p j → ∃ i, p' i ∧ ∀ (x y : α), (f x, f y) ∈ s' i → (x, y) ∈ s j
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
CategoryTheory.Limits.WalkingParallelFamily.category : {J : Type w} → CategoryTheory.SmallCategory (CategoryTheory.Limits.WalkingParallelFamily J)
-- Mathlib.Analysis.InnerProductSpace.l2Space
OrthogonalFamily.linearIsometry_apply_single : ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : RCLike 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] {G : ι → Type u_4} [inst_3 : (i : ι) → NormedAddCommGroup (G i)]
  [inst_4 : (i : ι) → InnerProductSpace 𝕜 (G i)] [inst_5 : CompleteSpace E] {V : (i : ι) → G i →ₗᵢ[𝕜] E}
  (hV : OrthogonalFamily 𝕜 G V) [inst_6 : DecidableEq ι] {i : ι} (x : G i),
  hV.linearIsometry (lp.single 2 i x) = (V i) x