mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.mapLeftId_hom_app_left : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) {P : CategoryTheory.MorphismProperty T}
  {Q : CategoryTheory.MorphismProperty A} {W : CategoryTheory.MorphismProperty B} [inst_3 : Q.IsMultiplicative]
  [inst_4 : W.IsMultiplicative] [inst_5 : Q.RespectsIso] [inst_6 : W.RespectsIso]
  (X : CategoryTheory.MorphismProperty.Comma L R P Q W),
  ((CategoryTheory.MorphismProperty.Comma.mapLeftId L R).hom.app X).left = CategoryTheory.CategoryStruct.id X.left
-- Lean.Compiler.InlineAttrs
Lean.Compiler.instBEqInlineAttributeKind : BEq Lean.Compiler.InlineAttributeKind
-- Mathlib.Analysis.Calculus.Deriv.ZPow
hasStrictDerivAt_zpow : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] (m : ℤ) (x : 𝕜),
  x ≠ 0 ∨ 0 ≤ m → HasStrictDerivAt (fun x => x ^ m) (↑m * x ^ (m - 1)) x
-- Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
CategoryTheory.Pseudofunctor.mapComp'_inv_whiskerRight_mapComp'₀₂₃_inv_app : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] [inst_1 : CategoryTheory.Bicategory.Strict B]
  (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {b₀ b₁ b₂ b₃ : B} (f₀₁ : b₀ ⟶ b₁) (f₁₂ : b₁ ⟶ b₂)
  (f₂₃ : b₂ ⟶ b₃) (f₀₂ : b₀ ⟶ b₂) (f₁₃ : b₁ ⟶ b₃) (f : b₀ ⟶ b₃) (h₀₂ : CategoryTheory.CategoryStruct.comp f₀₁ f₁₂ = f₀₂)
  (h₁₃ : CategoryTheory.CategoryStruct.comp f₁₂ f₂₃ = f₁₃) (hf : CategoryTheory.CategoryStruct.comp f₀₂ f₂₃ = f)
  (X : ↑(F.obj b₀)),
  CategoryTheory.CategoryStruct.comp ((F.map f₂₃).toFunctor.map ((F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).inv.toNatTrans.app X))
      ((F.mapComp' f₀₂ f₂₃ f ⋯).inv.toNatTrans.app X) =
    CategoryTheory.CategoryStruct.comp ((F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).inv.toNatTrans.app ((F.map f₀₁).toFunctor.obj X))
      ((F.mapComp' f₀₁ f₁₃ f ⋯).inv.toNatTrans.app X)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.of_constToList_perm : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap.Raw α (fun x => β) cmp},
  (Std.DTreeMap.Raw.Const.toList t₁).Perm (Std.DTreeMap.Raw.Const.toList t₂) → t₁.Equiv t₂
-- Mathlib.Tactic.TFAE
/-- `tfae_have i → j := t`, where the goal is `TFAE [P₁, P₂, ...]` introduces a hypothesis
`tfae_i_to_j : Pᵢ → Pⱼ` and proof `t` to the local context. Note that `i` and `j` are
natural number literals (beginning at 1) used as indices to specify the propositions
`P₁, P₂, ...` that appear in the goal.

Once sufficient hypotheses have been introduced by `tfae_have`, `tfae_finish` can be used to close
the goal.

All features of `have` are supported by `tfae_have`, including naming, matching,
destructuring, and goal creation.

* `tfae_have i ← j := t` adds a hypothesis in the reverse direction, of type `Pⱼ → Pᵢ`.
* `tfae_have i ↔ j := t` adds a hypothesis in the both directions, of type `Pᵢ ↔ Pⱼ`.
* `tfae_have hij : i → j := t` names the introduced hypothesis `hij` instead of `tfae_i_to_j`.
* `tfae_have i j | p₁ => t₁ | ...` matches on the assumption `p : Pᵢ`.
* `tfae_have ⟨hij, hji⟩ : i ↔ j := t` destructures the bi-implication into `hij : Pᵢ → Pⱼ`
  and `hji : Pⱼ → Pⱼ`.
* `tfae_have i → j := t ?a` creates a new goal for `?a`.

Examples:
```lean4
example (h : P → R) : TFAE [P, Q, R] := by
  tfae_have 1 → 3 := h
  -- The resulting context now includes `tfae_1_to_3 : P → R`.
  sorry
```

```lean4
-- An example of `tfae_have` and `tfae_finish`:
example : TFAE [P, Q, R] := by
  tfae_have 1 → 2 := sorry /- proof of P → Q -/
  tfae_have 2 → 1 := sorry /- proof of Q → P -/
  tfae_have 2 ↔ 3 := sorry /- proof of Q ↔ R -/
  tfae_finish
```

```lean4
-- All features of `have` are supported by `tfae_have`:
example : TFAE [P, Q] := by
  -- assert `tfae_1_to_2 : P → Q`:
  tfae_have 1 → 2 := sorry

  -- assert `hpq : P → Q`:
  tfae_have hpq : 1 → 2 := sorry

  -- match on `p : P` and prove `Q` via `f p`:
  tfae_have 1 → 2
  | p => f p

  -- assert `pq : P → Q`, `qp : Q → P`:
  tfae_have ⟨pq, qp⟩ : 1 ↔ 2 := sorry

  -- assert `h : P → Q`; `?a` is a new goal:
  tfae_have h : 1 → 2 := f ?a

  sorry
```
 -/
Mathlib.Tactic.TFAE.tfaeHave : Lean.ParserDescr
-- Mathlib.Control.Monad.Writer
WriterT.run : {M : Type u → Type v} → {α ω : Type u} → WriterT ω M α → M (α × ω)
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.op_X₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C), sq.op.X₂ = Opposite.op sq.X₂
-- Mathlib.Topology.Category.Profinite.EffectiveEpi
Profinite.effectiveEpiFamily_of_jointly_surjective : ∀ {α : Type} [Finite α] {B : Profinite} (X : α → Profinite) (π : (a : α) → X a ⟶ B),
  (∀ (b : ↑B.toTop), ∃ a x, (CategoryTheory.ConcreteCategory.hom (π a)) x = b) → CategoryTheory.EffectiveEpiFamily X π
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
EisensteinSeries.auxbound2 : ∀ (z : UpperHalfPlane) (c : ℝ) {d : ℝ}, 1 ≤ d ^ 2 → EisensteinSeries.r z ≤ ‖↑c * ↑z + ↑d‖
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
/-- The intersection between the fundamental cone and the `integerLattice`.  -/
NumberField.mixedEmbedding.fundamentalCone.integerSet : (K : Type u_1) → [inst : Field K] → [NumberField K] → Set (NumberField.mixedEmbedding.mixedSpace K)
-- Mathlib.Data.Real.Basic
Real.ofCauchy.injEq : ∀ (cauchy cauchy_1 : CauSeq.Completion.Cauchy abs),
  ({ cauchy := cauchy } = { cauchy := cauchy_1 }) = (cauchy = cauchy_1)
-- Mathlib.Algebra.Group.Subgroup.Map
Subgroup.comap_inf : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] (H K : Subgroup N) (f : G →* N),
  Subgroup.comap f (H ⊓ K) = Subgroup.comap f H ⊓ Subgroup.comap f K
-- Mathlib.Analysis.Quaternion
Quaternion.instCoeComplexReal : Coe ℂ (Quaternion ℝ)
-- Mathlib.Data.Nat.Factorial.Basic
Nat.factorial_eq_one : ∀ {n : ℕ}, n.factorial = 1 ↔ n ≤ 1
-- Mathlib.RingTheory.Polynomial.ContentIdeal
Polynomial.contentIdeal_eq_bot_iff : ∀ {R : Type u_1} [inst : Semiring R] (p : Polynomial R), p.contentIdeal = ⊥ ↔ p = 0
-- Lean.Meta.Sym.Arith.Poly
/-- Coefficient applied to polynomial `p₂`.  -/
Lean.Grind.CommRing.SPolResult.k₂ : Lean.Grind.CommRing.SPolResult → ℤ
-- Mathlib.MeasureTheory.Constructions.Cylinders
MeasureTheory.disjoint_cylinder_iff : ∀ {ι : Type u_1} {α : ι → Type u_2} [Nonempty ((i : ι) → α i)] {s t : Finset ι} {S : Set ((i : ↥s) → α ↑i)}
  {T : Set ((i : ↥t) → α ↑i)} [inst : DecidableEq ι],
  Disjoint (MeasureTheory.cylinder s S) (MeasureTheory.cylinder t T) ↔
    Disjoint (Finset.restrict₂ ⋯ ⁻¹' S) (Finset.restrict₂ ⋯ ⁻¹' T)
-- Mathlib.LinearAlgebra.BilinearMap
LinearMap.ext₂ : ∀ {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 g : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P}, (∀ (m : M) (n : N), (f m) n = (g m) n) → f = g
-- Mathlib.Topology.Clopen
isClopen_biUnion_finset : ∀ {X : Type u} [inst : TopologicalSpace X] {Y : Type u_2} {s : Finset Y} {f : Y → Set X},
  (∀ i ∈ s, IsClopen (f i)) → IsClopen (⋃ i ∈ s, f i)
-- Mathlib.Analysis.Normed.Group.Seminorm
NonarchAddGroupSeminorm.mk.sizeOf_spec : ∀ {G : Type u_6} [inst : AddGroup G] [inst_1 : SizeOf G] (toZeroHom : ZeroHom G ℝ)
  (add_le_max' : ∀ (r s : G), toZeroHom.toFun (r + s) ≤ max (toZeroHom.toFun r) (toZeroHom.toFun s))
  (neg' : ∀ (r : G), toZeroHom.toFun (-r) = toZeroHom.toFun r),
  sizeOf { toZeroHom := toZeroHom, add_le_max' := add_le_max', neg' := neg' } = 1 + sizeOf toZeroHom
-- Init.Data.UInt.Bitwise
UInt32.xor_left_inj : ∀ {a b : UInt32} (c : UInt32), a ^^^ c = b ^^^ c ↔ a = b
-- Mathlib.Algebra.Homology.CochainComplexOpposite
CochainComplex.exactAt_op : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {K : CochainComplex C ℤ} {n : ℤ},
  HomologicalComplex.ExactAt K n →
    ∀ (m : ℤ),
      autoParam (n + m = 0) CochainComplex.exactAt_op._auto_1 →
        HomologicalComplex.ExactAt ((CochainComplex.opEquivalence C).functor.obj (Opposite.op K)) m
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.chainsMap_id_comp : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A B C : Rep.{u, u, u} k G} (φ : A ⟶ B) (ψ : B ⟶ C),
  groupHomology.chainsMap (MonoidHom.id G) (CategoryTheory.CategoryStruct.comp φ ψ) =
    CategoryTheory.CategoryStruct.comp (groupHomology.chainsMap (MonoidHom.id G) φ)
      (groupHomology.chainsMap (MonoidHom.id G) ψ)
-- Mathlib.AlgebraicGeometry.Birational.Birational
AlgebraicGeometry.Scheme.PartialIso.restrictSource_target : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X.PartialIso Y) (U : X.Opens) (hU : Dense ↑U) (hU' : U ≤ f.source),
  (f.restrictSource U hU hU').target =
    (AlgebraicGeometry.Scheme.Hom.opensFunctor f.target.ι).obj
      ((AlgebraicGeometry.Scheme.Hom.opensFunctor f.iso.hom).obj ((TopologicalSpace.Opens.map f.source.ι.base).obj U))
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
/-- A multiplicative morphism between commutative monoids gives a braided functor between
the corresponding discrete braided monoidal categories.
 -/
CategoryTheory.Discrete.monoidalFunctorBraided : {M : Type u} →
  [inst : CommMonoid M] →
    {N : Type u} → [inst_1 : CommMonoid N] → (F : M →* N) → (CategoryTheory.Discrete.monoidalFunctor F).Braided
-- Init.Data.List.Lex
List.le_trans : ∀ {α : Type u_1} [inst : LT α] [inst_1 : LE α] [Std.IsLinearOrder α] [Std.LawfulOrderLT α] {l₁ l₂ l₃ : List α},
  l₁ ≤ l₂ → l₂ ≤ l₃ → l₁ ≤ l₃
-- Mathlib.Algebra.Ring.Torsion
MonoidHom.map_neg : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : Monoid M] [IsMulTorsionFree M] (f : R →* M) (x : R),
  f (-x) = f x
-- Mathlib.Combinatorics.SimpleGraph.LapMatrix
SimpleGraph.lapMatrix_toLinearMap₂'_apply'_eq_zero_iff_forall_reachable : ∀ {V : Type u_1} [inst : Fintype V] (G : SimpleGraph V) [inst_1 : DecidableRel G.Adj] [inst_2 : DecidableEq V]
  (x : V → ℝ),
  (((Matrix.toLinearMap₂' ℝ) (SimpleGraph.lapMatrix ℝ G)) x) x = 0 ↔ ∀ (i j : V), G.Reachable i j → x i = x j
-- Mathlib.RingTheory.Localization.LocalizationLocalization
/-- Given submodules `M ⊆ R` and `N ⊆ S = M⁻¹R`, with `f : R →+* S` the localization map, we have
`N ⁻¹ S = T = (f⁻¹ (N • f(M))) ⁻¹ R`. I.e., the localization of a localization is a localization.
 -/
IsLocalization.localization_localization_isLocalization : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] (N : Submonoid S) (T : Type u_3) [inst_3 : CommSemiring T] [inst_4 : Algebra R T]
  [inst_5 : Algebra S T] [IsScalarTower R S T] [IsLocalization M S] [IsLocalization N T],
  IsLocalization (IsLocalization.localizationLocalizationSubmodule M N) T
-- Mathlib.Analysis.BoxIntegral.Partition.Filter
BoxIntegral.IntegrationParams.mk.inj : ∀ {bRiemann bHenstock bDistortion bRiemann_1 bHenstock_1 bDistortion_1 : Bool},
  { bRiemann := bRiemann, bHenstock := bHenstock, bDistortion := bDistortion } =
      { bRiemann := bRiemann_1, bHenstock := bHenstock_1, bDistortion := bDistortion_1 } →
    bRiemann = bRiemann_1 ∧ bHenstock = bHenstock_1 ∧ bDistortion = bDistortion_1
-- Aesop.Script.StructureDynamic
Aesop.Script.DynStructureResult.mk.injEq : ∀ (script : List Aesop.Script.Step) (postState : Lean.Meta.SavedState) (script_1 : List Aesop.Script.Step)
  (postState_1 : Lean.Meta.SavedState),
  ({ script := script, postState := postState } = { script := script_1, postState := postState_1 }) =
    (script = script_1 ∧ postState = postState_1)
-- Init.Omega.Constraint
Lean.Omega.normalize_sat : ∀ {s : Lean.Omega.Constraint} {x v : Lean.Omega.Coeffs},
  s.sat' x v = true → (Lean.Omega.normalizeConstraint s x).sat' (Lean.Omega.normalizeCoeffs s x) v = true
-- Mathlib.Geometry.Manifold.Notation
/-- Attempt to find a model with corners on the units in a normed algebra  -/
_private.Mathlib.Geometry.Manifold.Notation.0.Manifold.Elab.findModelInner.fromUnitsOfAlgebra : Lean.Expr → Lean.Elab.TermElabM Lean.Expr
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.neighborSet.decidablePred : {V : Type u} →
  {G : SimpleGraph V} →
    (G' : G.Subgraph) → [h : DecidableRel G'.Adj] → (v : V) → DecidablePred fun x => x ∈ G'.neighborSet v
-- Mathlib.CategoryTheory.Preadditive.Mat
/-- A functor induces a functor of matrix categories.
 -/
CategoryTheory.Functor.mapMat_ : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {D : Type u_1} →
        [inst_2 : CategoryTheory.Category.{v₁, u_1} D] →
          [inst_3 : CategoryTheory.Preadditive D] →
            (F : CategoryTheory.Functor C D) →
              [F.Additive] → CategoryTheory.Functor (CategoryTheory.Mat_ C) (CategoryTheory.Mat_ D)
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
AlgebraicGeometry.Scheme.IdealSheafData.ker_glueDataObjι_appTop : ∀ {X : AlgebraicGeometry.Scheme} (I : X.IdealSheafData) (U : ↑X.affineOpens),
  RingHom.ker (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appTop (I.glueDataObjι U))) =
    Ideal.comap (CommRingCat.Hom.hom (↑U).topIso.hom) (I.ideal U)
-- Mathlib.Geometry.Manifold.VectorBundle.FiberwiseLinear
/-- For `B` a manifold and `F` a normed space, the groupoid on `B × F` consisting of local
homeomorphisms which are bi-`C^n` and fiberwise linear, and induce the identity on `B`.
When a (topological) vector bundle is `C^n`, then the composition of charts associated
to the vector bundle belong to this groupoid.  -/
contMDiffFiberwiseLinear : {𝕜 : Type u_1} →
  (B : Type u_2) →
    (F : Type u_3) →
      [inst : TopologicalSpace B] →
        [inst_1 : NontriviallyNormedField 𝕜] →
          [inst_2 : NormedAddCommGroup F] →
            [NormedSpace 𝕜 F] →
              {EB : Type u_4} →
                [inst_4 : NormedAddCommGroup EB] →
                  [inst_5 : NormedSpace 𝕜 EB] →
                    {HB : Type u_5} →
                      [inst_6 : TopologicalSpace HB] →
                        [ChartedSpace HB B] → ModelWithCorners 𝕜 EB HB → WithTop ℕ∞ → StructureGroupoid (B × F)
-- Mathlib.Combinatorics.HalesJewett
Combinatorics.Subspace.reindex_isMono : ∀ {η : Type u_5} {α : Type u_6} {ι : Type u_7} {κ : Type u_8} {l : Combinatorics.Subspace η α ι} {η' : Type u_9}
  {α' : Type u_10} {ι' : Type u_11} {eη : η ≃ η'} {eα : α ≃ α'} {eι : ι ≃ ι'} {C : (ι' → α') → κ},
  Combinatorics.Subspace.IsMono C (l.reindex eη eα eι) ↔
    Combinatorics.Subspace.IsMono (fun x => C (⇑eα ∘ x ∘ ⇑eι.symm)) l
-- Mathlib.Topology.EMetricSpace.Defs
/-- Every `EMetricSpace` has a `WeakEMetricSpace` structure by using the topology induced by edist.  -/
EMetricSpace.toWeakEMetricSpace : (α : Type u) → [inst : EMetricSpace α] → WeakEMetricSpace α
-- Mathlib.RingTheory.Binomial
Ring.choose_add_smul_choose : ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : Pow R ℕ] [inst_2 : BinomialRing R] [NatPowAssoc R] (r : R) (n k : ℕ),
  (n + k).choose k • Ring.choose (r + ↑k) (n + k) = Ring.choose (r + ↑k) k * Ring.choose r n
-- Mathlib.GroupTheory.GroupAction.Blocks
/-- A trivial block is a `Set X` which is either a subsingleton or `univ`.

Note: It is not necessarily a block when the action is not by a group.  -/
AddAction.IsTrivialBlock : {X : Type u_2} → Set X → Prop
-- Mathlib.Analysis.InnerProductSpace.Positive
LinearMap.IsPositive.add : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {T S : E →ₗ[𝕜] E}, T.IsPositive → S.IsPositive → (T + S).IsPositive
-- Mathlib.MeasureTheory.Function.LpSpace.InfiniteSum
_private.Mathlib.MeasureTheory.Function.LpSpace.InfiniteSum.0.MeasureTheory.Lp.hasSum_coeFn_tsum_nat : ∀ {X : Type u_1} {E : Type u_2} {x : MeasurableSpace X} {μ : MeasureTheory.Measure X} [inst : NormedAddCommGroup E]
  {p : ENNReal} [hp : Fact (1 ≤ p)] [CompleteSpace E] {f : ℕ → ↥(MeasureTheory.Lp E p μ)},
  ∑' (n : ℕ), ‖f n‖ₑ ≠ ⊤ → ∀ᵐ (a : X) ∂μ, HasSum (fun n => ↑↑(f n) a) (↑↑(∑' (n : ℕ), f n) a)
-- Std.Data.Internal.List.Associative
Std.Internal.List.isNone_minKey?_eq_isEmpty : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] {l : List ((a : α) × β a)},
  (Std.Internal.List.minKey? l).isNone = l.isEmpty
-- Lean.Elab.MutualInductive
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.withInductiveLocalDecls.loop : {α : Type} →
  Array Lean.Elab.Command.PreElabHeaderResult →
    (Array Lean.Expr → Array Lean.Expr → Lean.Elab.TermElabM α) →
      Array Lean.Expr → ℕ → Array Lean.Expr → Lean.Elab.TermElabM α
-- Mathlib.Analysis.Calculus.ContDiff.Defs
contDiffOn_of_differentiableOn : ∀ {𝕜 : 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] {s : Set E}
  {f : E → F} {n : ℕ∞},
  (∀ (m : ℕ), ↑m ≤ n → DifferentiableOn 𝕜 (iteratedFDerivWithin 𝕜 m f s) s) → ContDiffOn 𝕜 (↑n) f s
-- Mathlib.Tactic.Attr.Register
/-- A simp set for pushing coercions from `ℕ` to `ℕ∞` in `enat_to_nat`.  -/
Parser.Attr.enat_to_nat_coe : Lean.ParserDescr
-- Mathlib.Order.Interval.Finset.Defs
Finset.subtype_Ioi_eq : ∀ {α : Type u_1} [inst : Preorder α] (p : α → Prop) [inst_1 : DecidablePred p] [inst_2 : LocallyFiniteOrderTop α]
  (a : Subtype p), Finset.Ioi a = Finset.subtype p (Finset.Ioi ↑a)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.foldM_eq_foldlM_toArray : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {δ : Type w} {m' : Type w → Type w'} {β : Type v}
  {m : Std.DHashMap.Raw α fun x => β} [inst_2 : Monad m'] [LawfulMonad m'] {f : δ → α → β → m' δ} {init : δ},
  m.WF → Std.DHashMap.Raw.foldM f init m = Array.foldlM (fun a b => f a b.1 b.2) init (Std.DHashMap.Raw.Const.toArray m)
-- Mathlib.LinearAlgebra.Matrix.Reindex
Matrix.toAddEquiv_reindexRingEquiv : ∀ {m : Type u_2} {n : Type u_3} (R : Type u_11) [inst : Fintype m] [inst_1 : Fintype n] [inst_2 : Mul R]
  [inst_3 : AddCommMonoid R] (e : m ≃ n), ↑(Matrix.reindexRingEquiv R e) = Matrix.reindexAddEquiv R e e
-- Mathlib.Algebra.Group.Prod
Prod.instIsRightCancelMul : ∀ {G : Type u_1} {H : Type u_2} [inst : Mul G] [inst_1 : Mul H] [IsRightCancelMul G] [IsRightCancelMul H],
  IsRightCancelMul (G × H)
-- Mathlib.Order.OrderIsoNat
RelEmbedding.coe_natLT : ∀ {α : Type u_1} {r : α → α → Prop} [inst : IsStrictOrder α r] {f : ℕ → α} {H : ∀ (n : ℕ), r (f n) (f (n + 1))},
  ⇑(RelEmbedding.natLT f H) = f
-- Lean.Compiler.IR.Basic
Lean.IR.CtorInfo.isScalar : Lean.IR.CtorInfo → Bool
-- Mathlib.Algebra.Group.Submonoid.Operations
AddMonoidHom.domRestrictHom_apply : ∀ {M : Type u_1} [inst : AddZeroClass M] {S : Type u_5} [inst_1 : SetLike S M] [inst_2 : AddSubmonoidClass S M] (M' : S)
  (A : Type u_6) [inst_3 : AddCommMonoid A] (f : M →+ A), (AddMonoidHom.domRestrictHom M' A) f = f.domRestrict M'
-- Mathlib.RingTheory.MvPowerSeries.PiTopology
MvPowerSeries.WithPiTopology.variables_tendsto_zero : ∀ {σ : Type u_1} {R : Type u_2} [inst : TopologicalSpace R] [inst_1 : Semiring R],
  Filter.Tendsto (fun x => MvPowerSeries.X x) Filter.cofinite (nhds 0)
-- Mathlib.Tactic.Simps.Basic
/-- TransparencyMode used to reduce the type in order to detect whether it is a structure.  -/
Simps.Config.typeMd : Simps.Config → Lean.Meta.TransparencyMode
-- Mathlib.Topology.Algebra.Group.Pointwise
/-- Given a neighborhood `U` of the identity, one may find a neighborhood `V` of the
identity which is closed, symmetric, and satisfies `V + V ⊆ U`.  -/
exists_closed_nhds_zero_neg_eq_add_subset : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [IsTopologicalAddGroup G] {U : Set G},
  U ∈ nhds 0 → ∃ V ∈ nhds 0, IsClosed V ∧ -V = V ∧ V + V ⊆ U
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.integral_const : ∀ {α : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} [hE : CompleteSpace E] (c : E), ∫ (x : α), c ∂μ = μ.real Set.univ • c
-- Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
/-- Left homotopy classes of maps between bifibrant objects identify
to morphisms in the homotopy category `BifibrantObject.HoCat`.  -/
HomotopicalAlgebra.BifibrantObject.HoCat.homEquivLeft : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : HomotopicalAlgebra.ModelCategory C] →
      {X Y : C} →
        [inst_2 : HomotopicalAlgebra.IsCofibrant X] →
          [inst_3 : HomotopicalAlgebra.IsCofibrant Y] →
            [inst_4 : HomotopicalAlgebra.IsFibrant X] →
              [inst_5 : HomotopicalAlgebra.IsFibrant Y] →
                HomotopicalAlgebra.LeftHomotopyClass X Y ≃
                  (HomotopicalAlgebra.BifibrantObject.toHoCat.obj (HomotopicalAlgebra.BifibrantObject.mk X) ⟶
                    HomotopicalAlgebra.BifibrantObject.toHoCat.obj (HomotopicalAlgebra.BifibrantObject.mk Y))
-- Mathlib.Data.Finset.Lattice.Fold
Finset.sup_attach : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeSup α] [inst_1 : OrderBot α] (s : Finset β) (f : β → α),
  (s.attach.sup fun x => f ↑x) = s.sup f
-- Init.Data.String.Basic
ByteArray.validateUTF8.go.eq_def : ∀ (b : ByteArray) (i : ℕ) (hi : i ≤ b.size),
  ByteArray.validateUTF8.go b i hi =
    if hi : i < b.size then
      match h : b.validateUTF8At i with
      | false => false
      | true => ByteArray.validateUTF8.go b (i + b[i].utf8ByteSize ⋯) ⋯
    else true
-- Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric
ordinaryHypergeometricSeries_apply_eq : ∀ {𝕂 : Type u_1} {𝔸 : Type u_2} [inst : Field 𝕂] [inst_1 : Ring 𝔸] [inst_2 : Algebra 𝕂 𝔸] [inst_3 : TopologicalSpace 𝔸]
  [inst_4 : IsTopologicalRing 𝔸] (a b c : 𝕂) (x : 𝔸) (n : ℕ),
  ((ordinaryHypergeometricSeries 𝔸 a b c n) fun x_1 => x) =
    ((↑n.factorial)⁻¹ * Polynomial.eval a (ascPochhammer 𝕂 n) * Polynomial.eval b (ascPochhammer 𝕂 n) *
        (Polynomial.eval c (ascPochhammer 𝕂 n))⁻¹) •
      x ^ n
-- Mathlib.Order.Filter.AtTopBot.Basic
Filter.map_val_atBot_of_Iic_subset : ∀ {α : Type u_3} [inst : Preorder α] [IsCodirectedOrder α] {a : α} {s : Set α},
  Set.Iic a ⊆ s → Filter.map Subtype.val Filter.atBot = Filter.atBot
-- Mathlib.Topology.DiscreteQuotient
DiscreteQuotient.leComap_id : ∀ {X : Type u_2} [inst : TopologicalSpace X] (A : DiscreteQuotient X), DiscreteQuotient.LEComap (ContinuousMap.id X) A A
-- Mathlib.Algebra.QuadraticAlgebra.Basic
QuadraticAlgebra.norm_intCast : ∀ {R : Type u_2} {a b : R} [inst : CommRing R] (n : ℤ), QuadraticAlgebra.norm ↑n = ↑n ^ 2
-- Mathlib.Order.Category.Lat
Lat.mk.injEq : ∀ (carrier : Type u_1) [str : Lattice carrier] (carrier_1 : Type u_1) (str_1 : Lattice carrier_1),
  ({ carrier := carrier, str := str } = { carrier := carrier_1, str := str_1 }) = (carrier = carrier_1 ∧ str ≍ str_1)
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.LawfulForwardPatternModel.skipPrefix?_sliceFrom_eq_none_iff : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.ForwardPattern pat]
  [inst_1 : String.Slice.Pattern.Model.PatternModel pat] [String.Slice.Pattern.Model.LawfulForwardPatternModel pat]
  {s : String.Slice} {p₀ : s.Pos},
  String.Slice.Pattern.ForwardPattern.skipPrefix? pat (s.sliceFrom p₀) = none ↔
    ¬String.Slice.Pattern.Model.MatchesAt pat p₀
-- Init.Tactics
/-- This tactic applies to a goal whose target has the form `x ~ x`,
where `~` is equality, heterogeneous equality or any relation that
has a reflexivity lemma tagged with the attribute @[refl].
 -/
Lean.Parser.Tactic.tacticRfl : Lean.ParserDescr
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.get!_union_of_not_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeSet α cmp} [inst : Inhabited α] [inst_1 : Std.TransCmp cmp]
  {k : α}, k ∉ t₂ → (t₁ ∪ t₂).get! k = t₁.get! k