mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.MFDeriv.Defs
MDifferentiableWithinAt.continuousWithinAt : ∀ {𝕜 : 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] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {s : Set M} {x : M},
  MDiffAt[s] f x → ContinuousWithinAt f s x
-- Mathlib.RingTheory.Adjoin.PowerBasis
Algebra.adjoin.powerBasis_dim : ∀ {K : Type u_1} {S : Type u_2} [inst : Field K] [inst_1 : CommRing S] [inst_2 : Algebra K S] {x : S}
  (hx : IsIntegral K x), (Algebra.adjoin.powerBasis hx).dim = (minpoly K x).natDegree
-- Mathlib.Topology.UniformSpace.Equiv
UniformEquiv.continuous : ∀ {α : Type u} {β : Type u_1} [inst : UniformSpace α] [inst_1 : UniformSpace β] (h : α ≃ᵤ β), Continuous ⇑h
-- Mathlib.GroupTheory.OrderOfElement
/-- An injective homomorphism of additive monoids preserves orders of elements.  -/
addOrderOf_injective : ∀ {G : Type u_1} [inst : AddMonoid G] {H : Type u_6} [inst_1 : AddMonoid H] (f : G →+ H),
  Function.Injective ⇑f → ∀ (x : G), addOrderOf (f x) = addOrderOf x
-- Mathlib.Algebra.Module.Equiv.Defs
LinearEquiv.coe_ofInvolutive : ∀ {R : Type u_1} {M : Type u_7} [inst : Semiring R] [inst_1 : AddCommMonoid M] {σ σ' : R →+* R}
  [inst_2 : RingHomInvPair σ σ'] [inst_3 : RingHomInvPair σ' σ] {x : Module R M} (f : M →ₛₗ[σ] M)
  (hf : Function.Involutive ⇑f), ⇑(LinearEquiv.ofInvolutive f hf) = ⇑f
-- Plausible.Gen
_private.Plausible.Gen.0.Plausible.errorOfGenError : {α : Type} → Except Plausible.GenError α → IO α
-- Mathlib.CategoryTheory.Sites.Grothendieck
/-- The intersection of two covering sieves is covering.

See also [MM92] Chapter III, Section 2, Definition 1 (iv).  -/
CategoryTheory.GrothendieckTopology.intersection_covering : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} {S R : CategoryTheory.Sieve X}
  (J : CategoryTheory.GrothendieckTopology C), R ∈ J X → S ∈ J X → R ⊓ S ∈ J X
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.isoMk_inv_h₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E F : CategoryTheory.PreZeroHypercover S}
  (s₀ : E.I₀ ≃ F.I₀) (h₀ : (i : E.I₀) → E.X i ≅ F.X (s₀ i))
  (w₀ :
    autoParam (∀ (i : E.I₀), CategoryTheory.CategoryStruct.comp (h₀ i).hom (F.f (s₀ i)) = E.f i)
      CategoryTheory.PreZeroHypercover.isoMk._auto_1)
  (i : F.I₀),
  (CategoryTheory.PreZeroHypercover.isoMk s₀ h₀ w₀).inv.h₀ i =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (h₀ (s₀.symm i)).inv
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.String
String.reduceBEq : Lean.Meta.Simp.DSimproc
-- Lean.Parser.Types
Lean.Parser.ParserState.mk.inj : ∀ {stxStack : Lean.Parser.SyntaxStack} {lhsPrec : ℕ} {pos : String.Pos.Raw} {cache : Lean.Parser.ParserCache}
  {errorMsg : Option Lean.Parser.Error}
  {recoveredErrors : Array (String.Pos.Raw × Lean.Parser.SyntaxStack × Lean.Parser.Error)}
  {stxStack_1 : Lean.Parser.SyntaxStack} {lhsPrec_1 : ℕ} {pos_1 : String.Pos.Raw} {cache_1 : Lean.Parser.ParserCache}
  {errorMsg_1 : Option Lean.Parser.Error}
  {recoveredErrors_1 : Array (String.Pos.Raw × Lean.Parser.SyntaxStack × Lean.Parser.Error)},
  { stxStack := stxStack, lhsPrec := lhsPrec, pos := pos, cache := cache, errorMsg := errorMsg,
        recoveredErrors := recoveredErrors } =
      { stxStack := stxStack_1, lhsPrec := lhsPrec_1, pos := pos_1, cache := cache_1, errorMsg := errorMsg_1,
        recoveredErrors := recoveredErrors_1 } →
    stxStack = stxStack_1 ∧
      lhsPrec = lhsPrec_1 ∧ pos = pos_1 ∧ cache = cache_1 ∧ errorMsg = errorMsg_1 ∧ recoveredErrors = recoveredErrors_1
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
/-- If `B` is an `A` algebra and both `A` and `B` have valuative relations,
we say that `B|A` is a valuative extension if the valuative relation on `A` is
induced by the one on `B`.  -/
ValuativeExtension : (A : Type u_1) →
  (B : Type u_2) →
    [inst : CommSemiring A] → [inst_1 : Semiring B] → [ValuativeRel A] → [ValuativeRel B] → [Algebra A B] → Prop
-- Mathlib.SetTheory.ZFC.Rank
IsWellFounded.rank.congr_simp : ∀ {α : Type u} (r r_1 : α → α → Prop) (e_r : r = r_1) [hwf : IsWellFounded α r] (a a_1 : α),
  a = a_1 → IsWellFounded.rank r a = IsWellFounded.rank r_1 a_1
-- Mathlib.Analysis.Normed.Unbundled.AlgebraNorm
/-- A multiplicative `R`-algebra norm extends the norm on `R`.  -/
MulAlgebraNorm.extends_norm' : ∀ {R : outParam (Type u_1)} {S : outParam (Type u_2)} [inst : SeminormedCommRing R] [inst_1 : Ring S]
  [inst_2 : Algebra R S] (f : MulAlgebraNorm R S) (a : R), f (a • 1) = ‖a‖
-- Mathlib.Algebra.Group.Submonoid.Saturation
Submonoid.MulSaturated.inf : ∀ {M : Type u_1} [inst : MulOneClass M] {s₁ s₂ : Submonoid M},
  s₁.MulSaturated → s₂.MulSaturated → (s₁ ⊓ s₂).MulSaturated
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.type_lift_preimage : ∀ {α : Type u} {β : Type v} (r : α → α → Prop) [inst : IsWellOrder α r] (f : β ≃ α),
  Ordinal.lift.{u, v} (Ordinal.type (⇑f ⁻¹'o r)) = Ordinal.lift.{v, u} (Ordinal.type r)
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.instToJsonCompletionItemCapabilities : Lean.ToJson Lean.Lsp.CompletionItemCapabilities
-- Mathlib.LinearAlgebra.FreeModule.Basic
/-- If `M` fits in universe `w`, then freeness is equivalent to existence of a basis in that
universe.

Note that if `M` does not fit in `w`, the reverse direction of this implication is still true as
`Module.Free.of_basis`.  -/
Module.free_def : ∀ (R : Type u) (M : Type v) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Small.{w, v} M],
  Module.Free R M ↔ ∃ I, Nonempty (Module.Basis I R M)
-- Mathlib.Dynamics.Ergodic.MeasurePreserving
MeasureTheory.MeasurePreserving.id : ∀ {α : Type u_1} [inst : MeasurableSpace α] (μ : MeasureTheory.Measure α), MeasureTheory.MeasurePreserving id μ μ
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
/-- The `2`-division polynomial `ψ₂ = Ψ₂`.  -/
WeierstrassCurve.ψ₂ : {R : Type r} → [inst : CommRing R] → WeierstrassCurve R → Polynomial (Polynomial R)
-- Init.Data.BitVec.Lemmas
BitVec.udiv_def : ∀ {n : ℕ} {x y : BitVec n}, x / y = BitVec.ofNat n (x.toNat / y.toNat)
-- Mathlib.Algebra.Order.GroupWithZero.Basic
pow_lt_self_of_lt_one₀ : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] [inst_1 : PartialOrder M₀] {a : M₀} {n : ℕ} [PosMulStrictMono M₀],
  0 < a → a < 1 → 1 < n → a ^ n < a
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.prodMonoidal_associator : ∀ (C₁ : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C₁] [inst_1 : CategoryTheory.MonoidalCategory C₁]
  (C₂ : Type u₂) [inst_2 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_3 : CategoryTheory.MonoidalCategory C₂]
  (X Y Z : C₁ × C₂),
  CategoryTheory.MonoidalCategoryStruct.associator X Y Z =
    (CategoryTheory.MonoidalCategoryStruct.associator X.1 Y.1 Z.1).prod
      (CategoryTheory.MonoidalCategoryStruct.associator X.2 Y.2 Z.2)
-- Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
rpow_mul_exp_neg_mul_sq_isLittleO_exp_neg : ∀ {b : ℝ}, 0 < b → ∀ (s : ℝ), (fun x => x ^ s * Real.exp (-b * x ^ 2)) =o[Filter.atTop] fun x => Real.exp (-(1 / 2) * x)
-- Aesop.Forward.State
/-- Add a match `m`. Precondition: `nextSlot` is the slot with index
`m.level + 1`. Returns `true` if the variable map changed.  -/
Aesop.VariableMap.addMatch : Aesop.VariableMap → Aesop.Slot → Aesop.Match → Aesop.BaseM (Aesop.VariableMap × Bool)
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
/-- If `y : L` is a root of `minpoly K x`, then `minpoly K y = minpoly K x`.  -/
minpoly.eq_of_root : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {x y : L},
  IsAlgebraic K x → (Polynomial.aeval y) (minpoly K x) = 0 → minpoly K y = minpoly K x
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Defs
EisensteinSeries.D2_one : EisensteinSeries.D2 1 = 0
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Metric
/-- If a set has a thickening with finite measure, then the measures of its `r`-thickenings
converge to the measure of its closure as `r > 0` tends to `0`.  -/
tendsto_measure_thickening : ∀ {α : Type u_1} [inst : PseudoEMetricSpace α] [inst_1 : MeasurableSpace α] [OpensMeasurableSpace α]
  {μ : MeasureTheory.Measure α} {s : Set α},
  (∃ R > 0, μ (Metric.thickening R s) ≠ ⊤) →
    Filter.Tendsto (fun r => μ (Metric.thickening r s)) (nhdsWithin 0 (Set.Ioi 0)) (nhds (μ (closure s)))
-- Mathlib.GroupTheory.GroupAction.Blocks
/-- An orbit is a block.  -/
MulAction.IsBlock.orbit : ∀ {G : Type u_1} [inst : Group G] {X : Type u_2} [inst_1 : MulAction G X] (a : X),
  MulAction.IsBlock G (MulAction.orbit G a)
-- Mathlib.Logic.Encodable.Basic
Encodable.decode_option_zero : ∀ {α : Type u_1} [inst : Encodable α], Encodable.decode 0 = some none
-- Init.Data.UInt.Basic
/-- Converts a `Fin UInt64.size` into the corresponding `UInt64`.  -/
UInt64.ofFin : Fin UInt64.size → UInt64
-- Init.Data.BitVec.Bitblast
BitVec.toInt_dvd_toInt_iff : ∀ {w : ℕ} {x y : BitVec w},
  y.toInt ∣ x.toInt ↔ ((if x.msb = true then -x else x) % if y.msb = true then -y else y) = 0#w
-- Mathlib.Order.Lattice
inf_lt_left_or_right : ∀ {α : Type u} [inst : SemilatticeInf α] {a b : α}, a ≠ b → a ⊓ b < a ∨ a ⊓ b < b
-- Mathlib.Algebra.Group.Subgroup.Defs
zpow_mem : ∀ {M : Type u_3} {S : Type u_4} [inst : DivInvMonoid M] [inst_1 : SetLike S M] [hSM : SubgroupClass S M] {K : S}
  {x : M}, x ∈ K → ∀ (n : ℤ), x ^ n ∈ K
-- Mathlib.Algebra.Field.Subfield.Defs
SubfieldClass.qsmul_mem : ∀ {K : Type u} [inst : DivisionRing K] {S : Type u_1} [inst_1 : SetLike S K] [h : SubfieldClass S K] {x : K} (s : S)
  (q : ℚ), x ∈ s → q • x ∈ s
-- Mathlib.Tactic.ITauto
Mathlib.Tactic.ITauto.Proof.app'.inj : ∀ {a a_1 a_2 a_3 : Mathlib.Tactic.ITauto.Proof}, a.app' a_1 = a_2.app' a_3 → a = a_2 ∧ a_1 = a_3
-- Mathlib.CategoryTheory.Functor.KanExtension.Preserves
/-- The cone at a point of the whiskering right by `G` of an extension is isomorphic to the
action of `G` on the cone at that point for the original extension.  -/
CategoryTheory.Functor.RightExtension.coneAtWhiskerRightIso : {A : Type u_1} →
  {B : Type u_2} →
    {C : Type u_3} →
      {D : Type u_4} →
        [inst : CategoryTheory.Category.{v_1, u_1} A] →
          [inst_1 : CategoryTheory.Category.{v_2, u_2} B] →
            [inst_2 : CategoryTheory.Category.{v_3, u_3} C] →
              [inst_3 : CategoryTheory.Category.{v_4, u_4} D] →
                (G : CategoryTheory.Functor B D) →
                  (F : CategoryTheory.Functor A B) →
                    (L : CategoryTheory.Functor A C) →
                      (E : L.RightExtension F) →
                        (c : C) →
                          ((CategoryTheory.Functor.RightExtension.postcompose₂ L F G).obj E).coneAt c ≅
                            G.mapCone (E.coneAt c)
-- Mathlib.LinearAlgebra.QuadraticForm.Isometry
/-- There is a zero map from the trivial module.  -/
QuadraticMap.Isometry.hasZeroOfSubsingleton : {R : Type u_1} →
  {M₁ : Type u_3} →
    {M₂ : Type u_4} →
      {N : Type u_7} →
        [inst : CommSemiring R] →
          [inst_1 : AddCommMonoid M₁] →
            [inst_2 : AddCommMonoid M₂] →
              [inst_3 : AddCommMonoid N] →
                [inst_4 : Module R M₁] →
                  [inst_5 : Module R M₂] →
                    [inst_6 : Module R N] →
                      {Q₁ : QuadraticMap R M₁ N} → {Q₂ : QuadraticMap R M₂ N} → [Subsingleton M₁] → Zero (Q₁ →qᵢ Q₂)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
WeierstrassCurve.baseChange.eq_1 : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) (A : Type v) [inst_1 : CommRing A] [inst_2 : Algebra R A],
  W.baseChange A = W.map (algebraMap R A)
-- Lean.Meta.LetToHave
_private.Lean.Meta.LetToHave.0.Lean.Meta.LetToHave.M : Type → Type
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.prodMonoidal_rightUnitor : ∀ (C₁ : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C₁] [inst_1 : CategoryTheory.MonoidalCategory C₁]
  (C₂ : Type u₂) [inst_2 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_3 : CategoryTheory.MonoidalCategory C₂]
  (x : C₁ × C₂),
  CategoryTheory.MonoidalCategoryStruct.rightUnitor x =
    (CategoryTheory.MonoidalCategoryStruct.rightUnitor x.1).prod (CategoryTheory.MonoidalCategoryStruct.rightUnitor x.2)
-- Mathlib.Algebra.Order.Monovary
monovary_inv_right : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : PartialOrder α] [inst_1 : CommGroup β] [inst_2 : PartialOrder β]
  [IsOrderedMonoid β] {f : ι → α} {g : ι → β}, Monovary f g⁻¹ ↔ Antivary f g
-- Mathlib.NumberTheory.ModularForms.SlashInvariantForms
SlashInvariantForm.coe_constℝ : ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} [inst : Γ.HasDetPlusMinusOne] (x : ℝ),
  ⇑(SlashInvariantForm.constℝ x) = Function.const UpperHalfPlane ↑x
-- Mathlib.CategoryTheory.Limits.MonoCoprod
CategoryTheory.Limits.MonoCoprod.mk' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C],
  (∀ (A B : C), ∃ c x, CategoryTheory.Mono c.inl) → CategoryTheory.Limits.MonoCoprod C
-- Mathlib.RingTheory.DedekindDomain.IntegralClosure
/-- If `L` is a finite separable extension of `Frac(A)`, where `A` is a Dedekind domain,
the integral closure of `A` in `L` is a Dedekind domain.

See also the lemma `integralClosure.isDedekindDomain` where you can choose
the field of fractions yourself.  -/
integralClosure.isDedekindDomain_fractionRing : ∀ (A : Type u_1) [inst : CommRing A] (L : Type u_3) [inst_1 : Field L] [inst_2 : Algebra A L] [inst_3 : IsDomain A]
  [inst_4 : Algebra (FractionRing A) L] [IsScalarTower A (FractionRing A) L] [FiniteDimensional (FractionRing A) L]
  [Algebra.IsSeparable (FractionRing A) L] [IsDedekindDomain A], IsDedekindDomain ↥(integralClosure A L)
-- Mathlib.RingTheory.AlgebraicIndependent.Basic
lift_trdeg_le_of_injective : ∀ {R : Type u_2} {A : Type v} {A' : Type v'} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : CommRing A']
  [inst_3 : Algebra R A] [inst_4 : Algebra R A'] (f : A →ₐ[R] A'),
  Function.Injective ⇑f → Cardinal.lift.{v', v} (Algebra.trdeg R A) ≤ Cardinal.lift.{v, v'} (Algebra.trdeg R A')
-- Mathlib.RingTheory.KrullDimension.Zero
Ring.KrullDimLE.mem_minimalPrimes_iff_le_of_isPrime : ∀ {R : Type u_1} [inst : CommSemiring R] [Ring.KrullDimLE 0 R] {I J : Ideal R} [I.IsPrime], I ∈ J.minimalPrimes ↔ J ≤ I
-- Lean.Parser.Term
/-- Parentheses, used for grouping expressions (e.g., `a * (b + c)`).
Can also be used for creating simple functions when combined with `·`. Here are some examples:
  - `(· + 1)` is shorthand for `fun x => x + 1`
  - `(· + ·)` is shorthand for `fun x y => x + y`
  - `(f · a b)` is shorthand for `fun x => f x a b`
  - `(h (· + 1) ·)` is shorthand for `fun x => h (fun y => y + 1) x`
  - also applies to other parentheses-like notations such as `(·, 1)` and `(· : Nat → Nat)`
 -/
Lean.Parser.Term.paren : Lean.Parser.Parser
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsBigOWith.of_const_mul_right : ∀ {α : Type u_1} {E : Type u_3} {R : Type u_13} [inst : Norm E] [inst_1 : SeminormedRing R] {c' : ℝ} {f : α → E}
  {l : Filter α} {g : α → R} {c : R},
  0 ≤ c' → (Asymptotics.IsBigOWith c' l f fun x => c * g x) → Asymptotics.IsBigOWith (c' * ‖c‖) l f g
-- Mathlib.Topology.FiberBundle.Trivialization
/-- The domain of the local trivialisation (i.e., a subset of the bundle `Z`'s base):
outside of it, the pretrivialisation returns a junk value  -/
Bundle.Pretrivialization.baseSet : {B : Type u_1} →
  {F : Type u_2} →
    {Z : Type u_4} →
      [inst : TopologicalSpace B] →
        [inst_1 : TopologicalSpace F] → {proj : Z → B} → Bundle.Pretrivialization F proj → Set B
-- Mathlib.Algebra.NonAssoc.PreLie.Basic
LeftPreLieRing.toNonUnitalNonAssocRing : {L : Type u_1} → [self : LeftPreLieRing L] → NonUnitalNonAssocRing L
-- Mathlib.Analysis.InnerProductSpace.Orthonormal
/-- A linear equivalence that sends an orthonormal basis to orthonormal vectors is a linear
isometric equivalence.  -/
LinearEquiv.isometryOfOrthonormal : {𝕜 : Type u_1} →
  {E : Type u_2} →
    [inst : RCLike 𝕜] →
      [inst_1 : SeminormedAddCommGroup E] →
        [inst_2 : InnerProductSpace 𝕜 E] →
          {ι : Type u_4} →
            {E' : Type u_7} →
              [inst_3 : SeminormedAddCommGroup E'] →
                [inst_4 : InnerProductSpace 𝕜 E'] →
                  (f : E ≃ₗ[𝕜] E') → {v : Module.Basis ι 𝕜 E} → Orthonormal 𝕜 ⇑v → Orthonormal 𝕜 (⇑f ∘ ⇑v) → E ≃ₗᵢ[𝕜] E'
-- Mathlib.GroupTheory.GroupAction.Blocks
/-- A subgroup containing the stabilizer of `a`
is the stabilizer of the orbit of `a` under that subgroup  -/
MulAction.stabilizer_orbit_eq : ∀ {G : Type u_1} [inst : Group G] {X : Type u_2} [inst_1 : MulAction G X] {a : X} {H : Subgroup G},
  MulAction.stabilizer G a ≤ H → MulAction.stabilizer G (MulAction.orbit (↥H) a) = H
-- Mathlib.Data.Multiset.Defs
Multiset.instDecidableEquivListOfDecidableEq : {α : Type u_1} → [DecidableEq α] → (l₁ l₂ : List α) → Decidable (l₁ ≈ l₂)
-- Mathlib.Analysis.Calculus.FDeriv.Prod
HasFDerivWithinAt.finCons : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : E} {s : Set E} {n : ℕ} {F' : Fin n.succ → Type u_6}
  [inst_3 : (i : Fin n.succ) → NormedAddCommGroup (F' i)] [inst_4 : (i : Fin n.succ) → NormedSpace 𝕜 (F' i)]
  {φ : E → F' 0} {φs : E → (i : Fin n) → F' i.succ} {φ' : E →L[𝕜] F' 0} {φs' : E →L[𝕜] (i : Fin n) → F' i.succ},
  HasFDerivWithinAt φ φ' s x →
    HasFDerivWithinAt φs φs' s x → HasFDerivWithinAt (fun x => Fin.cons (φ x) (φs x)) (φ'.finCons φs') s x
-- Mathlib.FieldTheory.SeparableClosure
/-- If `p` is a separable polynomial with splitting field `E` over `F`, then `E / F` is a
separable extension.  -/
Algebra.isSeparable_of_separable_splitting_field : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {p : Polynomial F}
  [sp : Polynomial.IsSplittingField F E p], p.Separable → Algebra.IsSeparable F E
-- Init.Data.String.Lemmas.Iterate
_private.Init.Data.String.Lemmas.Iterate.0.String.positions.eq_1 : ∀ (s : String), s.positions = s.positionsFrom s.startPos
-- Mathlib.MeasureTheory.Function.ConvergenceInDistribution
MeasureTheory.TendstoInDistribution.tendsto : ∀ {ι : Type u_1} {E : Type u_2} {Ω' : Type u_3} {Ω : ι → Type u_5} {m : (i : ι) → MeasurableSpace (Ω i)}
  {m' : MeasurableSpace Ω'} {mE : MeasurableSpace E} [inst : TopologicalSpace E] [inst_1 : OpensMeasurableSpace E]
  {X : (i : ι) → Ω i → E} {l : Filter ι} {Z : Ω' → E} {μ : (i : ι) → MeasureTheory.Measure (Ω i)}
  [inst_2 : ∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)]
  {μ' : autoParam (MeasureTheory.Measure Ω') MeasureTheory.TendstoInDistribution._auto_1}
  [inst_3 : MeasureTheory.IsProbabilityMeasure μ'] (self : MeasureTheory.TendstoInDistribution X l Z μ μ'),
  Filter.Tendsto (fun n => ⟨MeasureTheory.Measure.map (X n) (μ n), ⋯⟩) l (nhds ⟨MeasureTheory.Measure.map Z μ', ⋯⟩)
-- Lean.Elab.Match
Lean.Elab.Term.PatternElabException.patternIdx : Lean.Elab.Term.PatternElabException → ℕ
-- Lean.Parser.Syntax
/-- - `unicode("→", "->")` parses a symbol matching either `→` or `->`. Each symbol is reserved.
  The second symbol is an ASCII version of the first.
  The  `pp.unicode` option controls which is used when pretty printing.
- `unicode("→", "->", preserveForPP)` is the same except for pretty printing behavior.
  When the `pp.unicode` option is enabled, then the pretty printer uses whichever symbol
  matches the underlying atom in the syntax.
  The intent is that `preserveForPP` means that the ASCII variant is preferred.
  For example, `fun` notation uses `preserveForPP` for its arrow; the delaborator chooses
  `↦` or `=>` depending on the value of `pp.unicode.fun`, letting users opt-in to formatting with `↦`.
  Note that `notation` creates a pretty printer preferring the ASCII version.
 -/
Lean.Parser.Syntax.unicodeAtom : Lean.Parser.Parser
-- Mathlib.Algebra.Quandle
Rack.PreEnvelGroupRel'.refl : {R : Type u} → [inst : Rack R] → {a : Rack.PreEnvelGroup R} → Rack.PreEnvelGroupRel' R a a
-- Mathlib.Data.List.GetD
List.getI_eq_getElem?_getD : ∀ {α : Type u} (l : List α) [inst : Inhabited α] (n : ℕ), l.getI n = l[n]?.getD default
-- Mathlib.CategoryTheory.CatCommSq
/-- The horizontal identity `CatCommSq`  -/
CategoryTheory.CatCommSq.hId : {C₁ : Type u_1} →
  {C₃ : Type u_3} →
    [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
      [inst_1 : CategoryTheory.Category.{v_3, u_3} C₃] →
        (L : CategoryTheory.Functor C₁ C₃) →
          CategoryTheory.CatCommSq (CategoryTheory.Functor.id C₁) L L (CategoryTheory.Functor.id C₃)
-- Std.Data.Internal.List.Associative
Std.Internal.List.keys_filter : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {l : List ((a : α) × β a)}
  {f : (a : α) → β a → Bool},
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.keys (List.filter (fun x => f x.fst x.snd) l) =
      (List.filter (fun x => f (↑x) (Std.Internal.List.getValueCast (↑x) l ⋯))
          (Std.Internal.List.keys l).attach).unattach
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.IrreducibleCloseds.isIrreducible' : ∀ {α : Type u_4} [inst : TopologicalSpace α] (self : TopologicalSpace.IrreducibleCloseds α), IsIrreducible self.carrier
-- Lean.Server.Requests
Lean.Language.SnapshotTree.foldInfosInRange : {α : Type u_1} →
  Lean.Language.SnapshotTree →
    Lean.Syntax.Range → α → (Lean.Elab.ContextInfo → Lean.Elab.Info → α → α) → Lean.Server.ServerTask α
-- Std.Data.Iterators.Lemmas.Combinators.DropWhile
_private.Std.Data.Iterators.Lemmas.Combinators.DropWhile.0.Std.Iter.val_step_intermediateDropWhile.match_1.eq_2 : ∀ (motive : Bool → Sort u_1) (h_1 : Unit → motive true) (h_2 : Unit → motive false),
  (match false with
    | true => h_1 ()
    | false => h_2 ()) =
    h_2 ()
-- Lean.Expr
Lean.instBEqMVarId : BEq Lean.MVarId
-- Lean.Parser.Command
Lean.Parser.Tactic.set_option.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
SSet.Truncated.HomotopyCategory.mkNatIso_inv_app_mk : ∀ {V : SSet.Truncated 2} {D : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} D]
  {F G : CategoryTheory.Functor V.HomotopyCategory D}
  (iso :
    (x : V.obj (Opposite.op { obj := { len := 0 }, property := SSet.OneTruncation₂._proof_1 })) →
      F.obj (SSet.Truncated.HomotopyCategory.mk x) ≅ G.obj (SSet.Truncated.HomotopyCategory.mk x))
  (hiso :
    autoParam
      (∀ ⦃x y : V.obj (Opposite.op { obj := { len := 0 }, property := SSet.OneTruncation₂._proof_1 })⦄
        (e : SSet.Truncated.Edge x y),
        CategoryTheory.CategoryStruct.comp (F.map (SSet.Truncated.HomotopyCategory.homMk e)) (iso y).hom =
          CategoryTheory.CategoryStruct.comp (iso x).hom (G.map (SSet.Truncated.HomotopyCategory.homMk e)))
      _auto_156✝)
  (v : V.obj (Opposite.op { obj := { len := 0 }, property := SSet.OneTruncation₂._proof_1 })),
  (SSet.Truncated.HomotopyCategory.mkNatIso iso hiso).inv.app (SSet.Truncated.HomotopyCategory.mk v) = (iso v).inv
-- Init.Meta.Defs
/-- How to convert the resulting metavariables into  new goals  -/
Lean.Meta.Rewrite.Config.newGoals : Lean.Meta.Rewrite.Config → Lean.Meta.Rewrite.NewGoals
-- Init.Sym.Lemmas
Lean.Sym.Int8.le_eq_true : ∀ (a b : Int8), decide (a ≤ b) = true → (a ≤ b) = True
-- Mathlib.Topology.Connected.PathConnected
/-- A topological space is path-connected if it is non-empty and every two points can be
joined by a continuous path.  -/
PathConnectedSpace : (X : Type u_4) → [TopologicalSpace X] → Prop
-- Mathlib.LinearAlgebra.Matrix.Nondegenerate
Matrix.Nondegenerate.of_det_mem_nonZeroDivisors : ∀ {m : Type u_1} {R : Type u_2} [inst : CommRing R] [inst_1 : Fintype m] [inst_2 : DecidableEq m] {M : Matrix m m R},
  M.det ∈ nonZeroDivisors R → M.Nondegenerate
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Affine.Simplex.affineCombination_mem_closedInterior_iff : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] [inst_4 : PartialOrder k] {n : ℕ} {s : Affine.Simplex k P n} {w : Fin (n + 1) → k},
  ∑ i, w i = 1 →
    ((Finset.affineCombination k Finset.univ s.points) w ∈ s.closedInterior ↔ ∀ (i : Fin (n + 1)), w i ∈ Set.Icc 0 1)