mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Prelude
/-- The typeclass behind the notation `a <|> b : γ` where `a : α`, `b : β`.
Because `b` is "lazy" in this notation, it is passed as `Unit → β` to the
implementation so it can decide when to evaluate it.
 -/
HOrElse : Type u → Type v → outParam (Type w) → Type (max (max u v) w)
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.BoundedFormula.Realize.eq_1 : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} (x : ℕ) (x_1 : α → M) (x_2 : Fin x → M),
  FirstOrder.Language.BoundedFormula.falsum.Realize x_1 x_2 = False
-- Mathlib.Algebra.ContinuedFractions.Computation.Translations
Stream'.Seq.map.eq_1 : ∀ {α : Type u} {β : Type v} (f : α → β) (s : Stream' (Option α)) (al : s.IsSeq),
  Stream'.Seq.map f ⟨s, al⟩ = ⟨Stream'.map (Option.map f) s, ⋯⟩
-- Lean.KeyedDeclsAttribute
Lean.KeyedDeclsAttribute.ExtensionState.table : {γ : Type} → Lean.KeyedDeclsAttribute.ExtensionState γ → Lean.KeyedDeclsAttribute.Table γ
-- Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
ContinuousLinearMap.instCompleteSpace : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_4}
  {F : Type u_5} [inst_2 : AddCommGroup E] [inst_3 : Module 𝕜₁ E] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜₂ F]
  [inst_6 : TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜₁ E] [SequentialSpace E]
  [inst_10 : UniformSpace F] [inst_11 : IsUniformAddGroup F] [ContinuousSMul 𝕜₂ F] [CompleteSpace F],
  CompleteSpace (E →SL[σ] F)
-- Mathlib.Algebra.Free
FreeSemigroup.mk.inj : ∀ {α : Type u} {head : α} {tail : List α} {head_1 : α} {tail_1 : List α},
  { head := head, tail := tail } = { head := head_1, tail := tail_1 } → head = head_1 ∧ tail = tail_1
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
CochainComplex.HomComplex.Cocycle.toSingleMk_precomp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {p q : ℤ} (f : K.X p ⟶ X) {n : ℤ}
  (h : p + n = q) (p' : ℤ) (hp' : p' + 1 = p) (hf : CategoryTheory.CategoryStruct.comp (K.d p' p) f = 0)
  {L : CochainComplex C ℤ} (g : L ⟶ K),
  CochainComplex.HomComplex.Cocycle.toSingleMk (CategoryTheory.CategoryStruct.comp (g.f p) f) h p' hp' ⋯ =
    (CochainComplex.HomComplex.Cocycle.toSingleMk f h p' hp' hf).precomp g
-- Mathlib.Order.SupClosed
isSublattice_latticeClosure : ∀ {α : Type u_3} [inst : Lattice α] {s : Set α}, IsSublattice (latticeClosure s)
-- Mathlib.Data.Finset.SMulAntidiagonal
Finset.support_smulAntidiagonal_subset_smul : ∀ {G : Type u_1} {P : Type u_2} [inst : SMul G P] {s : Set G} {t : Set P}
  (hst : ∀ (a : P), (s.smulAntidiagonal t a).Finite), {a | (Finset.SMulAntidiagonal a ⋯).Nonempty} ⊆ s • t
-- Mathlib.Data.NNReal.Basic
Real.toNNReal_prod_of_nonneg : ∀ {ι : Type u_2} {s : Finset ι} {f : ι → ℝ}, (∀ a ∈ s, 0 ≤ f a) → (∏ a ∈ s, f a).toNNReal = ∏ a ∈ s, (f a).toNNReal
-- Mathlib.FieldTheory.RatFunc.Luroth
RatFunc.Luroth.generator_spec : ∀ {K : Type u_1} [inst : Field K] {E : IntermediateField K (RatFunc K)},
  E ≠ ⊥ → RatFunc.Luroth.generator E ∉ (algebraMap K (RatFunc K)).range
-- Mathlib.MeasureTheory.Function.AEEqFun
/-- If the measure is nonzero, we can strengthen `coeFn_const` to get an equality.  -/
MeasureTheory.AEEqFun.coeFn_const_eq : ∀ (α : Type u_1) {β : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace β]
  [NeZero μ] (b : β) (x : α), ↑(MeasureTheory.AEEqFun.const α b) x = b
-- Mathlib.Probability.Process.Adapted
/-- Strongly progressive process. A sequence of functions `u` is said to be strongly
progressive with respect to a filtration `f` if at each point in time `i`, `u` restricted to
`Set.Iic i × Ω` is strongly measurable with respect to the product `MeasurableSpace` structure
where the σ-algebra used for `Ω` is `f i`.
The usual definition uses the interval `[0,i]`, which we replace by `Set.Iic i`. We recover the
usual definition for index types `ℝ≥0` or `ℕ`.  -/
MeasureTheory.IsStronglyProgressive : {Ω : Type u_1} →
  {ι : Type u_2} →
    {m : MeasurableSpace Ω} →
      [inst : Preorder ι] →
        {β : Type u_3} → [TopologicalSpace β] → [MeasurableSpace ι] → MeasureTheory.Filtration ι m → (ι → Ω → β) → Prop
-- Lean.Meta.Sym.Pattern
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.UnifyM.State.args : Lean.Meta.Sym.UnifyM.State✝ → Array Lean.Expr
-- Mathlib.Logic.Equiv.Prod
/-- Combine two equivalences using `PProd` in the codomain and `Prod` in the domain.  -/
Equiv.prodPProd : {α₂ : Sort u_3} → {β₂ : Sort u_6} → {α₁ : Type u_9} → {β₁ : Type u_10} → α₁ ≃ α₂ → β₁ ≃ β₂ → α₁ × β₁ ≃ α₂ ×' β₂
-- Mathlib.Data.Fin.Pigeonhole
/-- Any map from `Fin m` reaches at most `m` different values.
See also `Fintype.card_range_le` for the generalisation to an arbitrary finite type.
 -/
Fin.card_range_le : ∀ {m : ℕ} {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] (f : Fin m → α), Fintype.card ↑(Set.range f) ≤ m
-- Mathlib.Dynamics.Ergodic.Ergodic
Ergodic.ae_empty_or_univ_of_image_ae_le : ∀ {α : Type u_1} {m : MeasurableSpace α} {s : Set α} {f : α → α} {μ : MeasureTheory.Measure α}
  [MeasureTheory.IsFiniteMeasure μ],
  Ergodic f μ → MeasureTheory.NullMeasurableSet s μ → f '' s ≤ᵐ[μ] s → s =ᵐ[μ] ∅ ∨ s =ᵐ[μ] Set.univ
-- Std.Internal.Do.WP.Lemmas
Std.Internal.Do.WPMonad.le_wp_monadLift_ExceptT_apply : ∀ {Pred : Type u_1} {EPred : Type u_2} {m : Type u → Type v} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] {α ε : Type u} (x : m α)
  (post : α → Pred) (epost : EPost.Cons✝ (ε → Pred) EPred),
  Lean.Order.PartialOrder.rel (Std.Internal.Do.wp x post epost.tail)
    (Std.Internal.Do.wp (MonadLift.monadLift x) post epost)
-- Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Asymptotics.SuperpolynomialDecay.congr' : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α} {k f g : α → β} [inst : TopologicalSpace β] [inst_1 : CommSemiring β],
  Asymptotics.SuperpolynomialDecay l k f → f =ᶠ[l] g → Asymptotics.SuperpolynomialDecay l k g
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
cfc_add_const : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : TopologicalSpace A] [inst_6 : Ring A]
  [inst_7 : StarRing A] [inst_8 : Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] (r : R) (f : R → R)
  (a : A),
  autoParam (ContinuousOn f (spectrum R a)) cfc_add_const._auto_1 →
    autoParam (p a) cfc_add_const._auto_3 → cfc (fun x => f x + r) a = cfc f a + (algebraMap R A) r
-- Init.GrindInstances.Ring.SInt
Lean.Grind.Int32.natCast : NatCast Int32
-- Mathlib.Algebra.Field.Defs
Field.toDivisionRing : {K : Type u} → [self : Field K] → DivisionRing K
-- Lean.Data.Lsp.CodeActions
Lean.Lsp.CodeActionLiteralSupport.mk.sizeOf_spec : ∀ (codeActionKind : Lean.Lsp.CodeActionLiteralSupportValueSet),
  sizeOf { codeActionKind := codeActionKind } = 1 + sizeOf codeActionKind
-- Mathlib.Geometry.Manifold.VectorField.LieBracket
VectorField.mlieBracketWithin_add_left : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {s : Set M} {x : M} {V W V₁ : (x : M) → TangentSpace I x}
  [inst_6 : IsManifold I 2 M] [CompleteSpace E],
  MDiffAt[s] (T% V) x →
    MDiffAt[s] (T% V₁) x →
      UniqueMDiffAt[s] x →
        VectorField.mlieBracketWithin I (V + V₁) W s x =
          VectorField.mlieBracketWithin I V W s x + VectorField.mlieBracketWithin I V₁ W s x
-- Mathlib.Data.Nat.Factors
Nat.pos_of_mem_primeFactorsList : ∀ {n p : ℕ}, p ∈ n.primeFactorsList → 0 < p
-- Mathlib.Algebra.Order.Field.Basic
div_lt_self : ∀ {α : Type u_2} [inst : Semifield α] [inst_1 : PartialOrder α] [PosMulReflectLT α] {a b : α} [IsStrictOrderedRing α],
  0 < a → 1 < b → a / b < a
-- Init.Control.Lawful.Instances
ExceptT.run_throw : ∀ {m : Type u_1 → Type u_2} {ε β : Type u_1} {e : ε} [inst : Monad m], (throw e).run = pure (Except.error e)
-- Mathlib.Algebra.MvPolynomial.Degrees
MvPolynomial.notMem_support_of_degreeOf_lt : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {p : MvPolynomial σ R} (i : σ) {s : σ →₀ ℕ},
  MvPolynomial.degreeOf i p < s i → s ∉ p.support
-- Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
/-- Shorthand notation for the restriction of a function with locally finite support to the closed unit
ball of radius `r`.
 -/
Function.locallyFinsuppWithin.toClosedBall : {E : Type u_1} →
  [inst : NormedAddCommGroup E] →
    (r : ℝ) → Function.locallyFinsupp E ℤ →+ Function.locallyFinsuppWithin (Metric.closedBall 0 |r|) ℤ
-- Mathlib.Geometry.Manifold.GroupLieAlgebra
/-- Invariant vector fields are invariant under pullbacks.  -/
mpullback_mulInvariantVectorField : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4}
  [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : Group G] [LieGroup I (minSmoothness 𝕜 3) G]
  (g : G) (v : GroupLieAlgebra I G),
  VectorField.mpullback I I (fun x => g * x) (mulInvariantVectorField v) = mulInvariantVectorField v
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
WeierstrassCurve.leadingCoeff_ΨSq : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) [NoZeroDivisors R] {n : ℤ},
  ↑n ≠ 0 → (W.ΨSq n).leadingCoeff = ↑n ^ 2
-- Init.Data.Array.MinMax
Array.max_le_iff : ∀ {α : Type u_1} [inst : Max α] [inst_1 : LE α] [Std.LawfulOrderSup α] {xs : Array α} (h : xs ≠ #[]) {x : α},
  xs.max h ≤ x ↔ ∀ b ∈ xs, b ≤ x
-- Mathlib.Geometry.Euclidean.Projection
/-- The nonnegative distance between a point and its orthogonal projection to a subspace equals
the distance to that subspace as given by `Metric.infNndist`. This is not a `simp` lemma since
the simplest form depends on the context (if any calculations are to be done with the distance,
the version with the orthogonal projection gives access to more lemmas about orthogonal
projections that may be useful).  -/
EuclideanGeometry.dist_orthogonalProjection_eq_infNndist : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup V]
  [inst_2 : InnerProductSpace 𝕜 V] [inst_3 : MetricSpace P] [inst_4 : NormedAddTorsor V P] (s : AffineSubspace 𝕜 P)
  [inst_5 : Nonempty ↥s] [inst_6 : s.direction.HasOrthogonalProjection] (p : P),
  nndist p ↑((EuclideanGeometry.orthogonalProjection s) p) = Metric.infNndist p ↑s
-- Mathlib.Combinatorics.Matroid.Circuit
Matroid.IsCircuit.mem_closure_sdiff_singleton_of_mem : ∀ {α : Type u_1} {M : Matroid α} {C : Set α} {e : α}, M.IsCircuit C → e ∈ C → e ∈ M.closure (C \ {e})
-- Mathlib.Topology.Algebra.ContinuousAffineMap
/-- The linear map underlying a continuous affine map is continuous.  -/
ContinuousAffineMap.contLinear : {R : Type u_1} →
  {V : Type u_2} →
    {W : Type u_3} →
      {P : Type u_4} →
        {Q : Type u_5} →
          [inst : Ring R] →
            [inst_1 : AddCommGroup V] →
              [inst_2 : Module R V] →
                [inst_3 : TopologicalSpace P] →
                  [inst_4 : AddTorsor V P] →
                    [inst_5 : AddCommGroup W] →
                      [inst_6 : Module R W] →
                        [inst_7 : TopologicalSpace Q] →
                          [inst_8 : AddTorsor W Q] →
                            [inst_9 : TopologicalSpace V] →
                              [IsTopologicalAddTorsor P] →
                                [inst_11 : TopologicalSpace W] → [IsTopologicalAddTorsor Q] → (P →ᴬ[R] Q) → V →L[R] W
-- Mathlib.Tactic.FBinop
FBinopElab.elabBinOp : Lean.Elab.Term.TermElab
-- Mathlib.Probability.Martingale.Convergence
/-- Part a of the **L¹ martingale convergence theorem**: a uniformly integrable submartingale
strongly adapted to the filtration `ℱ` converges a.e. and in L¹ to an integrable function which is
measurable with respect to the σ-algebra `⨆ n, ℱ n`.  -/
MeasureTheory.Submartingale.tendsto_eLpNorm_one_limitProcess : ∀ {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ℱ : MeasureTheory.Filtration ℕ m0}
  {f : ℕ → Ω → ℝ} [MeasureTheory.IsFiniteMeasure μ],
  MeasureTheory.Submartingale f ℱ μ →
    MeasureTheory.UniformIntegrable f 1 μ →
      Filter.Tendsto (fun n => MeasureTheory.eLpNorm (f n - MeasureTheory.Filtration.limitProcess f ℱ μ) 1 μ)
        Filter.atTop (nhds 0)
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.IsDetector.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (G : C),
  CategoryTheory.IsDetector G = (CategoryTheory.ObjectProperty.singleton G).IsDetecting
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithTop.coe_ne_zero : ∀ {α : Type u} [inst : Zero α] {a : α}, ↑a ≠ 0 ↔ a ≠ 0
-- Mathlib.Topology.Maps.Basic
Topology.isOpenEmbedding_iff_isEmbedding_isOpenMap : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  Topology.IsOpenEmbedding f ↔ Topology.IsEmbedding f ∧ IsOpenMap f
-- Mathlib.Algebra.Star.SelfAdjoint
IsSelfAdjoint.inv₀ : ∀ {R : Type u_1} [inst : GroupWithZero R] [inst_1 : StarMul R] {x : R}, IsSelfAdjoint x → IsSelfAdjoint x⁻¹
-- Mathlib.Algebra.FreeMonoid.Basic
FreeAddMonoid.notMem_zero : ∀ {α : Type u_1} {m : α}, m ∉ 0
-- Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.le₂₃' : ∀ {ι : Type u_2} {κ : Type u_3} [inst : Preorder ι] {c : ℤ → ComplexShape κ} {r₀ : ℤ}
  (data : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀) (r : ℤ) (hr : r₀ ≤ r) (pq' : κ)
  {i₂ i₃ : ι}, i₂ = data.i₂ pq' → i₃ = data.i₃ r pq' ⋯ → i₂ ≤ i₃
-- Mathlib.LinearAlgebra.RootSystem.Hom
RootPairing.Equiv.comp_assoc : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {ι₁ : Type u_8} {M₁ : Type u_9} {N₁ : Type u_10}
  {ι₂ : Type u_11} {M₂ : Type u_12} {N₂ : Type u_13} {ι₃ : Type u_14} {M₃ : Type u_15} {N₃ : Type u_16}
  [inst_5 : AddCommGroup M₁] [inst_6 : Module R M₁] [inst_7 : AddCommGroup N₁] [inst_8 : Module R N₁]
  [inst_9 : AddCommGroup M₂] [inst_10 : Module R M₂] [inst_11 : AddCommGroup N₂] [inst_12 : Module R N₂]
  [inst_13 : AddCommGroup M₃] [inst_14 : Module R M₃] [inst_15 : AddCommGroup N₃] [inst_16 : Module R N₃]
  {P : RootPairing ι R M N} {P₁ : RootPairing ι₁ R M₁ N₁} {P₂ : RootPairing ι₂ R M₂ N₂} {P₃ : RootPairing ι₃ R M₃ N₃}
  (h : P₂.Equiv P₃) (g : P₁.Equiv P₂) (f : P.Equiv P₁), (h.comp g).comp f = h.comp (g.comp f)
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
zmodAddEquivOfGenerator_symm_apply_generator : ∀ {G : Type u_2} [inst : AddGroup G] {g : G} (hg : ∀ (x : G), x ∈ AddSubgroup.zmultiples g) {n : ℕ}
  (hn : Nat.card G = n), (zmodAddEquivOfGenerator hg hn).symm g = 1
-- Mathlib.Algebra.Order.Nonneg.Basic
Nonneg.toNonneg_lt : ∀ {α : Type u_1} [inst : Zero α] [inst_1 : LinearOrder α] {a : { x // 0 ≤ x }} {b : α}, a < Nonneg.toNonneg b ↔ ↑a < b
-- Mathlib.RingTheory.WittVector.StructurePolynomial
wittStructureRat.congr_simp : ∀ (p p_1 : ℕ) (e_p : p = p_1) {idx : Type u_2} [hp : Fact (Nat.Prime p)] (Φ Φ_1 : MvPolynomial idx ℚ),
  Φ = Φ_1 → ∀ (n n_1 : ℕ), n = n_1 → wittStructureRat p Φ n = wittStructureRat p_1 Φ_1 n_1
-- Std.Data.DTreeMap.Internal.Model
Ordering.swap.eq_2 : Ordering.eq.swap = Ordering.eq
-- Mathlib.Lean.Meta.CongrTheorems
Lean.Meta.FastSubsingleton.elim : ∀ {α : Sort u} [h : Lean.Meta.FastSubsingleton α] (a b : α), a = b
-- Mathlib.Algebra.Quaternion
Quaternion.instNontrivial : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R], Nontrivial (Quaternion R)
-- Mathlib.Algebra.Ring.Defs
NonAssocSemiring.mk : {α : Type u} →
  [toNonUnitalNonAssocSemiring : NonUnitalNonAssocSemiring α] →
    [toOne : One α] →
      (∀ (a : α), 1 * a = a) →
        (∀ (a : α), a * 1 = a) →
          [toNatCast : NatCast α] →
            autoParam (↑0 = 0) AddMonoidWithOne.natCast_zero._autoParam →
              autoParam (∀ (n : ℕ), ↑(n + 1) = ↑n + 1) AddMonoidWithOne.natCast_succ._autoParam → NonAssocSemiring α
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonInlayHint : Lean.ToJson Lean.Lsp.InlayHint
-- Lean.Elab.InfoTree.Types
Lean.Elab.ErrorNameInfo.mk.inj : ∀ {stx : Lean.Syntax} {errorName : Lean.Name} {stx_1 : Lean.Syntax} {errorName_1 : Lean.Name},
  { stx := stx, errorName := errorName } = { stx := stx_1, errorName := errorName_1 } →
    stx = stx_1 ∧ errorName = errorName_1
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
iteratedFDeriv.eq_1 : ∀ (𝕜 : Type u) [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] (n : ℕ)
  (f : E → F),
  iteratedFDeriv 𝕜 n f =
    Nat.recOn (motive := fun x => E → E [×x]→L[𝕜] F) n (fun x => ContinuousMultilinearMap.uncurry0 𝕜 E (f x))
      fun x rec x_1 => (fderiv 𝕜 rec x_1).uncurryLeft
-- Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits
CategoryTheory.ObjectProperty.preservesLimitsOfShape_iff : ∀ {J : Type u_1} {C : Type u_3} (K : Type u_5) [inst : CategoryTheory.Category.{v_1, u_5} K]
  [inst_1 : CategoryTheory.Category.{v_3, u_1} J] [inst_2 : CategoryTheory.Category.{v_5, u_3} C]
  (F : CategoryTheory.Functor J C),
  CategoryTheory.ObjectProperty.preservesLimitsOfShape K F ↔ CategoryTheory.Limits.PreservesLimitsOfShape K F
-- Mathlib.Data.Multiset.Range
Multiset.card_range : ∀ (n : ℕ), (Multiset.range n).card = n
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubMulAction.isScalarTower' : ∀ {S : Type u'} {R : Type u} {M : Type v} [inst : Monoid R] [inst_1 : MulAction R M] [inst_2 : SMul S R]
  [inst_3 : SMul S M] [inst_4 : IsScalarTower S R M] (p : SubMulAction R M) {S' : Type u_1} [inst_5 : SMul S' R]
  [inst_6 : SMul S' S] [inst_7 : SMul S' M] [inst_8 : IsScalarTower S' R M] [IsScalarTower S' S M],
  IsScalarTower S' S ↥p
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.isSome_skipSuffix? : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.BackwardPattern pat]
  [String.Slice.Pattern.LawfulBackwardPattern pat] {s : String.Slice}, (s.skipSuffix? pat).isSome = s.endsWith pat
-- Mathlib.CategoryTheory.Category.Cat.Limit
/-- Auxiliary definition:
the diagram whose limit gives the morphism space between two objects of the limit category.  -/
CategoryTheory.Cat.HasLimits.homDiagram : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    {F : CategoryTheory.Functor J CategoryTheory.Cat} →
      CategoryTheory.Limits.limit (F.comp CategoryTheory.Cat.objects) →
        CategoryTheory.Limits.limit (F.comp CategoryTheory.Cat.objects) → CategoryTheory.Functor J (Type v)
-- Mathlib.NumberTheory.WellApproximable
approxAddOrderOf.vadd_eq_of_mul_dvd : ∀ {A : Type u_1} [inst : SeminormedAddCommGroup A] {a : A} {n : ℕ} (δ : ℝ),
  0 < n → addOrderOf a ^ 2 ∣ n → a +ᵥ approxAddOrderOf A n δ = approxAddOrderOf A n δ
-- Std.Internal.Do.Order.Instances
Std.Internal.Do.CompleteLattice.instLawfulIdentityJoinBot : ∀ {l : Type u_1} [inst : Lean.Order.CompleteLattice l],
  Std.LawfulIdentity (fun x1 x2 => Lean.Order.join x1 x2) Lean.Order.bot
-- Mathlib.LinearAlgebra.Multilinear.Basic
MultilinearMap.constOfIsEmpty_apply : ∀ (R : Type uR) {ι : Type uι} (M₁ : ι → Type v₁) {M₂ : Type v₂} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
  [inst_4 : Module R M₂] [inst_5 : IsEmpty ι] (m : M₂),
  ⇑(MultilinearMap.constOfIsEmpty R M₁ m) = Function.const ((i : ι) → M₁ i) m
-- Mathlib.Data.Finset.NoncommProd
Finset.noncommSum_singleton : ∀ {α : Type u_3} {β : Type u_4} [inst : AddMonoid β] (a : α) (f : α → β), {a}.noncommSum f ⋯ = f a
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.RiiSlice.instToIterator : {α : Type u_1} →
  {β : α → Type v} →
    Std.ToIterator (Std.Slice (Std.DTreeMap.Internal.RiiSliceData α β)) Id (Std.DTreeMap.Internal.Zipper α β)
      ((a : α) × β a)
-- Mathlib.GroupTheory.NoncommPiCoprod
AddSubgroup.independent_of_coprime_order : ∀ {G : Type u_1} [inst : AddGroup G] {ι : Type u_2} {H : ι → AddSubgroup G},
  (Pairwise fun i j => ∀ (x y : G), x ∈ H i → y ∈ H j → AddCommute x y) →
    ∀ [Finite ι] [inst_2 : (i : ι) → Fintype ↥(H i)],
      (Pairwise fun i j => (Fintype.card ↥(H i)).Coprime (Fintype.card ↥(H j))) → iSupIndep H
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVBinPred.ult.sizeOf_spec : sizeOf Std.Tactic.BVDecide.BVBinPred.ult = 1
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalAlgHom.comp.congr_simp : ∀ {R : Type u} {S : Type u₁} {T : Type u_1} [inst : Monoid R] [inst_1 : Monoid S] [inst_2 : Monoid T] {φ : R →* S}
  {A : Type v} {B : Type w} {C : Type w₁} [inst_3 : NonUnitalNonAssocSemiring A] [inst_4 : DistribMulAction R A]
  [inst_5 : NonUnitalNonAssocSemiring B] [inst_6 : DistribMulAction S B] [inst_7 : NonUnitalNonAssocSemiring C]
  [inst_8 : DistribMulAction T C] {ψ : S →* T} {χ : R →* T} (f f_1 : B →ₛₙₐ[ψ] C),
  f = f_1 → ∀ (g g_1 : A →ₛₙₐ[φ] B), g = g_1 → ∀ [κ : φ.CompTriple ψ χ], f.comp g = f_1.comp g_1
-- Mathlib.Data.Fin.Tuple.Basic
/-- As a binary function, `Fin.insertNth` is injective.  -/
Fin.insertNth_injective2 : ∀ {n : ℕ} {α : Fin (n + 1) → Sort u_1} {p : Fin (n + 1)}, Function.Injective2 p.insertNth
-- Mathlib.MeasureTheory.Measure.NullMeasurable
MeasureTheory.NullMeasurableSpace.instMeasurableSpace : {α : Type u_2} →
  {m0 : MeasurableSpace α} → {μ : MeasureTheory.Measure α} → MeasurableSpace (MeasureTheory.NullMeasurableSpace α μ)
-- Mathlib.Algebra.Group.Nat.Hom
multiplesHom_symm_apply : ∀ {M : Type u_1} [inst : AddMonoid M] (f : ℕ →+ M), (multiplesHom M).symm f = f 1
-- Std.Sat.AIG.Relabel
Std.Sat.AIG.relabel_unsat_iff_of_not_Nonempty : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {β : Type} [inst_2 : Hashable β] [inst_3 : DecidableEq β]
  {idx : ℕ} {invert : Bool} {aig : Std.Sat.AIG α} {r : α → β} {hidx1 : idx < (Std.Sat.AIG.relabel r aig).decls.size}
  {hidx2 : idx < aig.decls.size},
  ¬Nonempty α → ((Std.Sat.AIG.relabel r aig).UnsatAt idx invert hidx1 ↔ aig.UnsatAt idx invert hidx2)
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.Std.Internal.List.insertListIfNewUnit.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (hd : α) (tl : List α) (h_1 : Unit → motive [])
  (h_2 : (hd : α) → (tl : List α) → motive (hd :: tl)),
  (match hd :: tl with
    | [] => h_1 ()
    | hd :: tl => h_2 hd tl) =
    h_2 hd tl
-- Mathlib.Algebra.Module.ULift
ULift.isScalarTower' : ∀ {R : Type u} {M : Type v} {N : Type w} [inst : SMul R M] [inst_1 : SMul M N] [inst_2 : SMul R N]
  [IsScalarTower R M N], IsScalarTower R (ULift.{u_1, v} M) N
-- Mathlib.Order.Interval.Set.Disjoint
Set.iUnion_Iio : ∀ {α : Type v} [inst : Preorder α] [NoMaxOrder α], ⋃ a, Set.Iio a = Set.univ
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
/-- If `a : Adj B`, `a.obj : B` is the underlying object of the bicategory `B`.  -/
CategoryTheory.Bicategory.Adj.obj : {B : Type u} → [inst : CategoryTheory.Bicategory B] → CategoryTheory.Bicategory.Adj B → B
-- Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument
CategoryTheory.SmallObject.iterationObjRightIso.eq_1 : ∀ {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 κ]
  (f : CategoryTheory.Arrow C),
  CategoryTheory.SmallObject.iterationObjRightIso I κ f =
    CategoryTheory.asIso (CategoryTheory.Arrow.Hom.right ((CategoryTheory.SmallObject.ιIteration I κ).app f))