mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.iteratedFDerivLM.eq_1 : ∀ (𝕜 : Type u_1) {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : SMulCommClass ℝ 𝕜 F] (n k : ℕ∞) {K : TopologicalSpace.Compacts E} (i : ℕ),
  ContDiffMapSupportedIn.iteratedFDerivLM 𝕜 n k i =
    { toFun := fun f => if hi : k + ↑i ≤ n then ContDiffMapSupportedIn.of_support_subset ⋯ ⋯ else 0, map_add' := ⋯,
      map_smul' := ⋯ }
-- Mathlib.Topology.Algebra.RestrictedProduct.Units
/-- **Alias** of `RestrictedProduct.eventually_isUnit_of_isUnit`. -/
RestrictedProduct.eventualy_isUnit_of_isUnit : ∀ {ι : Type u_1} {R : ι → Type u_2} [inst : (i : ι) → Monoid (R i)] {S : ι → Type u_3}
  [inst_1 : (i : ι) → SetLike (S i) (R i)] [inst_2 : ∀ (i : ι), SubmonoidClass (S i) (R i)] {B : (i : ι) → S i}
  {𝓕 : Filter ι} {x : RestrictedProduct (fun i => R i) (fun i => ↑(B i)) 𝓕},
  IsUnit x → (∀ (i : ι), IsUnit (x i)) ∧ ∀ᶠ (i : ι) in 𝓕, ∃ (h : x i ∈ B i), IsUnit ⟨x i, h⟩
-- Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
SSet.ι₁_comp_assoc : ∀ {X Y : SSet} (f : X ⟶ Y) {Z : SSet}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj Y (SSet.stdSimplex.obj { len := 1 }) ⟶ Z),
  CategoryTheory.CategoryStruct.comp SSet.ι₁
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight f (SSet.stdSimplex.obj { len := 1 })) h) =
    CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp SSet.ι₁ h)
-- Mathlib.GroupTheory.Coxeter.Inversion
CoxeterSystem.getElem_leftInvSeq : ∀ {B : Type u_1} {W : Type u_2} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (ω : List B) (j : ℕ)
  (h : j < ω.length),
  (cs.leftInvSeq ω)[j] = cs.wordProd (List.take j ω) * cs.simple ω[j] * (cs.wordProd (List.take j ω))⁻¹
-- Lean.Parser.Term
Lean.Parser.Term.scientific.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
cfc_comp_zpow : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : Semifield 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] [inst_9 : ContinuousFunctionalCalculus R A p] [ContinuousInv₀ R]
  [ContinuousMap.UniqueHom R A] (f : R → R) (n : ℤ) (a : Aˣ),
  autoParam (ContinuousOn f ((fun x => x ^ n) '' spectrum R ↑a)) cfc_comp_zpow._auto_1 →
    autoParam (p ↑a) cfc_comp_zpow._auto_3 → cfc (fun x => f (x ^ n)) ↑a = cfc f ↑(a ^ n)
-- Mathlib.Analysis.SpecialFunctions.Sqrt
fderiv_sqrt : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {x : E},
  DifferentiableAt ℝ f x → f x ≠ 0 → fderiv ℝ (fun x => √(f x)) x = (1 / (2 * √(f x))) • fderiv ℝ f x
-- Mathlib.Algebra.Group.Subgroup.Even
AddSubsemigroup.even.eq_1 : ∀ (S : Type u_1) [inst : AddCommSemigroup S], AddSubsemigroup.even S = { carrier := {s | Even s}, add_mem' := ⋯ }
-- Init.Data.Hashable
instHashablePEmpty : Hashable PEmpty.{u}
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.sum_le_sum : ∀ {ι : Type u_1} (f g : ι → Cardinal.{u_2}), (∀ (i : ι), f i ≤ g i) → Cardinal.sum f ≤ Cardinal.sum g
-- Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Asymptotics.IsEquivalent.inv : ∀ {α : Type u_1} {β : Type u_3} [inst : NormedField β] {u v : α → β} {l : Filter α},
  Asymptotics.IsEquivalent l u v → Asymptotics.IsEquivalent l u⁻¹ v⁻¹
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.Monoidal.instIsIsoη : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.Monoidal],
  CategoryTheory.IsIso (CategoryTheory.Functor.OplaxMonoidal.η F)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
/-- If `f : X → R → R` tends to `f x₀` uniformly (along `𝓝[s] x₀`) on the spectrum of `a`,
and eventually each `f x` is continuous on the spectrum of `a`, then `fun x ↦ cfc (f x) a` is
continuous at `x₀` within `s`.  -/
continuousWithinAt_cfc_fun : ∀ {X : Type u_1} {R : Type u_2} {A : Type u_3} {p : A → Prop} [inst : CommSemiring R] [inst_1 : StarRing R]
  [inst_2 : MetricSpace R] [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : Ring A]
  [inst_6 : StarRing A] [inst_7 : TopologicalSpace A] [inst_8 : Algebra R A]
  [inst_9 : ContinuousFunctionalCalculus R A p] [inst_10 : TopologicalSpace X] {f : X → R → R} {a : A} {x₀ : X}
  {s : Set X},
  TendstoUniformlyOn f (f x₀) (nhdsWithin x₀ s) (spectrum R a) →
    (∀ᶠ (x : X) in nhdsWithin x₀ s, ContinuousOn (f x) (spectrum R a)) → ContinuousWithinAt (fun x => cfc (f x) a) s x₀
-- Mathlib.Topology.OpenPartialHomeomorph.Basic
OpenPartialHomeomorph.isOpen_inter_preimage_symm : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y) {s : Set X}, IsOpen s → IsOpen (e.target ∩ ↑e.symm ⁻¹' s)
-- Mathlib.Tactic.Conv
/-- Use `refine` in `conv` mode.  -/
Mathlib.Tactic.Conv.convRefine_ : Lean.ParserDescr
-- Mathlib.Data.Set.Lattice
/-- Equivalence between a disjoint union and a dependent sum.  -/
Set.unionEqSigmaOfDisjoint : {α : Type u_1} →
  {β : Type u_2} → {t : α → Set β} → Pairwise (Function.onFun Disjoint t) → ↑(⋃ i, t i) ≃ (i : α) × ↑(t i)
-- Mathlib.Order.Preorder.Finite
Set.Finite.exists_minimal : ∀ {α : Type u_2} [inst : LE α] [IsTrans α fun a a_1 => a_1 ≤ a] {s : Set α},
  s.Finite → s.Nonempty → ∃ i, Minimal (fun x => x ∈ s) i
-- Lean.Meta.Tactic.Simp.Main
_private.Lean.Meta.Tactic.Simp.Main.0.Lean.Meta.Simp.reduceStep : Lean.Expr → Lean.Meta.SimpM Lean.Expr
-- Mathlib.Algebra.Divisibility.Finite
instDecidableDvdOfFintypeOfDecidableEq : {M : Type u_1} → [inst : Semigroup M] → [Fintype M] → [DecidableEq M] → (a b : M) → Decidable (a ∣ b)
-- Mathlib.Analysis.Complex.Trigonometric
Complex.sin_eq : ∀ (z : ℂ), Complex.sin z = Complex.sin ↑z.re * Complex.cosh ↑z.im + Complex.cos ↑z.re * Complex.sinh ↑z.im * Complex.I
-- Mathlib.CategoryTheory.CofilteredSystem
CategoryTheory.Functor.eventually_injective : ∀ {J : Type u} [inst : CategoryTheory.Category.{v_1, u} J] (F : CategoryTheory.Functor J (Type v))
  [CategoryTheory.IsCofilteredOrEmpty J] [∀ (j : J), Nonempty (F.obj j)] [∀ (j : J), Finite (F.obj j)],
  (∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (F.map f))) →
    ∀ [Nonempty J] [Finite ↑F.sections],
      ∃ j, ∀ (i : J) (f : i ⟶ j), Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (F.map f))
-- Init.Data.String.PosRaw
String.Pos.Raw.lt_inc_iff : ∀ {p q : String.Pos.Raw}, p < q.inc ↔ p ≤ q
-- Mathlib.Order.CountableSupClosed
countableInfClosure_eq_self : ∀ {α : Type u_2} {s : Set α} [inst : Preorder α], countableInfClosure s = s ↔ CountableInfClosed s
-- Mathlib.Order.OrderDual
OrderDual.instPartialOrder.dual_dual : ∀ (α : Type u_2) [H : PartialOrder α], OrderDual.instPartialOrder αᵒᵈ = H
-- Mathlib.MeasureTheory.Function.LpSpace.Indicator
MeasureTheory.Lp.norm_const' : ∀ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} (p : ENNReal) (μ : MeasureTheory.Measure α)
  [inst : NormedAddCommGroup E] [inst_1 : MeasureTheory.IsFiniteMeasure μ] (c : E),
  p ≠ 0 → p ≠ ⊤ → ‖(MeasureTheory.Lp.const p μ) c‖ = ‖c‖ * μ.real Set.univ ^ (1 / p.toReal)
-- Init.Internal.Order.Basic
Lean.Order.FlatOrder.mk_inner : ∀ {α : Sort u} {b : α} {x : Lean.Order.FlatOrder b}, Lean.Order.FlatOrder.mk b x.inner = x
-- Mathlib.Order.Preorder.Chain
/-- The `carrier` of a flag is the underlying set.  -/
Flag.carrier : {α : Type u_4} → [inst : LE α] → Flag α → Set α
-- Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup
/-- See `star_mem_iff` for both directions.  -/
pinGroup.star_mem : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} {x : CliffordAlgebra Q}, x ∈ pinGroup Q → star x ∈ pinGroup Q
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.Waiter.root : Lean.Meta.SynthInstance.Waiter
-- Mathlib.CategoryTheory.GuitartExact.Opposite
CategoryTheory.TwoSquare.structuredArrowRightwardsOpEquivalence.functor_obj_right_as : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} {C₄ : Type u₄} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  [inst_3 : CategoryTheory.Category.{v₄, u₄} C₄] {T : CategoryTheory.Functor C₁ C₂} {L : CategoryTheory.Functor C₁ C₃}
  {R : CategoryTheory.Functor C₂ C₄} {B : CategoryTheory.Functor C₃ C₄} (w : CategoryTheory.TwoSquare T L R B)
  {X₃ : C₃ᵒᵖ} {X₂ : C₂ᵒᵖ} (g : B.op.obj X₃ ⟶ R.op.obj X₂) (f : (w.op.StructuredArrowRightwards g)ᵒᵖ),
  ((CategoryTheory.TwoSquare.structuredArrowRightwardsOpEquivalence.functor w g).obj f).right.as = PUnit.unit
-- Init.Data.String.Lemmas.Pattern.String.ForwardSearcher
_private.Init.Data.String.Lemmas.Pattern.String.ForwardSearcher.0.String.Slice.Pattern.Model.ForwardSliceSearcher.Invariants.base.congr_simp : ∀ {pat pat_1 : String.Slice} (e_pat : pat = pat_1) {s : String.Slice} {needlePos needlePos_1 : String.Pos.Raw}
  (e_needlePos : needlePos = needlePos_1) {stackPos stackPos_1 : String.Pos.Raw} (e_stackPos : stackPos = stackPos_1)
  (h : String.Slice.Pattern.Model.ForwardSliceSearcher.Invariants✝ pat s needlePos stackPos),
  String.Slice.Pattern.Model.ForwardSliceSearcher.Invariants.base✝ h =
    String.Slice.Pattern.Model.ForwardSliceSearcher.Invariants.base✝ ⋯
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getD_union : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {fallback : β}, (m₁ ∪ m₂).getD k fallback = m₂.getD k (m₁.getD k fallback)
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.isDetector_op_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (G : C),
  CategoryTheory.IsDetector (Opposite.op G) ↔ CategoryTheory.IsCodetector G
-- Mathlib.Analysis.CStarAlgebra.Unitary.Connected
selfAdjoint.expUnitaryPathToOne_apply : ∀ {A : Type u_1} [inst : CStarAlgebra A] (x : ↥(selfAdjoint A)) (t : ↑unitInterval),
  (selfAdjoint.expUnitaryPathToOne x) t = selfAdjoint.expUnitary (↑t • x)
-- Batteries.Tactic.PrintPrefix
_private.Batteries.Tactic.PrintPrefix.0.Batteries.Tactic.instEvalExprPrintPrefixConfig : Lean.Elab.ConfigEval.EvalExpr Batteries.Tactic.PrintPrefixConfig
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
/-- **Alias** of `Convexity.convexCombPair_same`.

---

A convex combination of a point with itself is that point.  -/
Convexity.convexComboPair_symm : ∀ {R : Type u_1} {M : Type u_3} [inst : PartialOrder R] [inst_1 : Semiring R] [inst_2 : IsStrictOrderedRing R]
  [inst_3 : Convexity.ConvexSpace R M] {s t : R} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) {x : M},
  Convexity.convexCombPair s t hs ht h x x = x
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.Red.invRev : ∀ {α : Type u} {L₁ L₂ : List (α × Bool)},
  FreeGroup.Red L₁ L₂ → FreeGroup.Red (FreeGroup.invRev L₁) (FreeGroup.invRev L₂)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.fold_eq_foldl_toList : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) {δ : Type w} {f : δ → (a : α) → β a → δ}
  {init : δ}, Std.DHashMap.Raw.fold f init ↑m = List.foldl (fun a b => f a b.fst b.snd) init (↑m).toList
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.preimage_const_add_Iic : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] (a b : α),
  (fun x => a + x) ⁻¹' Set.Iic b = Set.Iic (b - a)
-- Init.Data.List.Lemmas
List.ne_cons_self : ∀ {α : Type u_1} {a : α} {l : List α}, l ≠ a :: l
-- Mathlib.GroupTheory.Congruence.Basic
AddCon.instVAdd : {α : Type u_4} →
  {M : Type u_5} →
    [inst : AddZeroClass M] → [inst_1 : VAdd α M] → [VAddAssocClass α M M] → (c : AddCon M) → VAdd α c.Quotient
-- Mathlib.LinearAlgebra.Matrix.Integer
Matrix.num.eq_1 : ∀ {m : Type u_1} {n : Type u_2} [inst : Fintype m] [inst_1 : Fintype n] (A : Matrix m n ℚ),
  A.num = (↑A.den • A).map Rat.num
-- Mathlib.Algebra.Group.Prod
Prod.instAddCancelMonoid.eq_1 : ∀ {M : Type u_3} {N : Type u_4} [inst : AddCancelMonoid M] [inst_1 : AddCancelMonoid N],
  Prod.instAddCancelMonoid = { toAddLeftCancelMonoid := Prod.instAddLeftCancelMonoid, toIsRightCancelAdd := ⋯ }
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.simplicialCosimplicialEquiv_functor_obj_obj : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (F : (CategoryTheory.Functor SimplexCategoryᵒᵖ C)ᵒᵖ)
  (X : SimplexCategory),
  ((CategoryTheory.simplicialCosimplicialEquiv C).functor.obj F).obj X =
    Opposite.op ((Opposite.unop F).obj (Opposite.op X))
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.toStream_toList' : ∀ {α : Type u_1} {t : RBTree.RBNode α} {s : RBTree.RBNode.Stream α}, (t.toStream s).toList = t.toList ++ s.toList
-- Mathlib.CategoryTheory.Category.Pairwise
/-- A "proxy type" equivalent to `CategoryTheory.Pairwise` that is constructed from `Unit`, `PLift`, `Sigma`, `Empty`, and `Sum`. See `CategoryTheory.Pairwise.proxyTypeEquiv` for the equivalence. (Generated by the `proxy_equiv%` elaborator.) -/
CategoryTheory.Pairwise.proxyType : Type v → Type v
-- Mathlib.Algebra.Homology.SpectralObject.Page
/-- An homology data for `X.shortComplex n₀ n₁ n₂ hn₁ hn₂ (𝟙 i) f (𝟙 j)`,
expressing `H^n₁(f)` as the homology of this short complex,
see `EIsoH`.  -/
CategoryTheory.Abelian.SpectralObject.homologyDataIdId : {C : Type u_1} →
  {ι : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] →
        [inst_2 : CategoryTheory.Abelian C] →
          (X : CategoryTheory.Abelian.SpectralObject C ι) →
            {i j : ι} →
              (f : i ⟶ j) →
                (n₀ n₁ n₂ : ℤ) →
                  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.homologyDataIdId._auto_1) →
                    (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.homologyDataIdId._auto_3) →
                      (X.shortComplex (CategoryTheory.CategoryStruct.id i) f (CategoryTheory.CategoryStruct.id j) n₀ n₁
                          n₂ hn₁ hn₂).HomologyData
-- Mathlib.Order.Filter.AtTopBot.CountablyGenerated
Filter.frequently_iff_seq_forall : ∀ {ι : Type u_3} {l : Filter ι} {p : ι → Prop} [l.IsCountablyGenerated],
  (∃ᶠ (n : ι) in l, p n) ↔ ∃ ns, Filter.Tendsto ns Filter.atTop l ∧ ∀ (n : ℕ), p (ns n)
-- Std.Data.HashMap.Lemmas
Std.HashMap.Equiv.mem_iff : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α}, m₁.Equiv m₂ → (k ∈ m₁ ↔ k ∈ m₂)
-- Mathlib.Analysis.Normed.Module.Ray
/-- Two vectors of the same norm are on the same ray if and only if they are equal.  -/
sameRay_iff_of_norm_eq : ∀ {F : Type u_2} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] {x y : F}, ‖x‖ = ‖y‖ → (SameRay ℝ x y ↔ x = y)
-- Mathlib.Data.Finset.Interval
Finset.Ioc_eq_filter_powerset : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Finset α), Finset.Ioc s t = {u ∈ t.powerset | s ⊂ u}
-- Mathlib.CategoryTheory.Limits.Final
/-- Alternative equational lemma for `(extendCone c).π.app` in case a lift of the object
is given explicitly.  -/
CategoryTheory.Functor.Initial.extendCone_obj_π_app' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} [inst_2 : F.Initial] {E : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} E]
  {G : CategoryTheory.Functor D E} (c : CategoryTheory.Limits.Cone (F.comp G)) {X : C} {Y : D} (f : F.obj X ⟶ Y),
  (CategoryTheory.Functor.Initial.extendCone.obj c).π.app Y = CategoryTheory.CategoryStruct.comp (c.π.app X) (G.map f)
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.union_div : ∀ {α : Type u_2} [inst : Div α] {s₁ s₂ t : Set α}, (s₁ ∪ s₂) / t = s₁ / t ∪ s₂ / t
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.mem_one : ∀ {α : Type u_2} [inst : One α] {a : α}, a ∈ 1 ↔ a = 1
-- Mathlib.Analysis.Calculus.FDeriv.Basic
HasFDerivAt.continuousAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {f' : E →L[𝕜] F} {x : E} [ContinuousAdd E] [ContinuousSMul 𝕜 E]
  [ContinuousAdd F] [ContinuousSMul 𝕜 F], HasFDerivAt f f' x → ContinuousAt f x
-- Mathlib.Data.Finset.Pi
/-- Given a finset `s` of `α` and for all `a : α` a finset `t a` of `β a`, then one can define the
finset `s.pi t` of all functions defined on elements of `s` taking values in `t a` for `a ∈ s`.
Note that the elements of `s.pi t` are only partially defined, on `s`.  -/
Finset.pi : {α : Type u_1} →
  {β : α → Type u} → [DecidableEq α] → (s : Finset α) → ((a : α) → Finset (β a)) → Finset ((a : α) → a ∈ s → β a)
-- Mathlib.Data.Finset.MulAntidiagonal
Finset.support_mulAntidiagonal_subset_mul : ∀ {α : Type u_1} [inst : CommMonoid α] [inst_1 : PartialOrder α] [inst_2 : IsOrderedCancelMonoid α] {s t : Set α}
  {hs : s.IsPWO} {ht : t.IsPWO}, {a | (Finset.mulAntidiagonal hs ht a).Nonempty} ⊆ s * t
-- Mathlib.Topology.Hom.ContinuousEvalConst
Filter.Tendsto.eval_const : ∀ {F : Type u_1} {α : Type u_2} {X : Type u_3} [inst : FunLike F α X] [inst_1 : TopologicalSpace F]
  [inst_2 : TopologicalSpace X] [ContinuousEvalConst F α X] {ι : Type u_5} {l : Filter ι} {f : ι → F} {g : F},
  Filter.Tendsto f l (nhds g) → ∀ (a : α), Filter.Tendsto (fun x => (f x) a) l (nhds (g a))
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKeyD_unitOfList_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] [inst_1 : BEq α] [Std.LawfulBEqCmp cmp] {l : List α}
  {k fallback : α}, l.contains k = false → (Std.ExtTreeMap.unitOfList l cmp).getKeyD k fallback = fallback
-- Mathlib.Order.SuccPred.Basic
coe_pred_of_mem : ∀ {α : Type u_3} [inst : PartialOrder α] {s : Set α} [inst_1 : s.OrdConnected] [inst_2 : PredOrder α] {a : ↑s},
  Order.pred ↑a ∈ s → ↑(Order.pred a) = Order.pred ↑a
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKey?_eq_some_getKeyD : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {a fallback : α}, a ∈ m → m.getKey? a = some (m.getKeyD a fallback)
-- Lean.Elab.ConfigEval.Commands
/-- `declare_core_config_elab f struct binders* [where ...]` defines a configuration elaborator
```lean
f binders* (cfg : Syntax) (init : struct := {}) (logExceptions : Bool := true) : CommandElabM struct
```
that evaluates the `cfg` configuration items to update `init`.
Acceptable configuration syntax is documented in `Lean.Elab.ConfigEval.foldConfigM`,
which includes anything that looks like `Lean.Parser.Term.optConfig`, possibly wrapped
in null nodes.

The command will transitively derive any necessary `ConfigEval.EvalTerm`/`ConfigEval.EvalExpr`
instances to support evaluation of configuration options for structure fields.
These instances will be `private local`.

See `ConfigEval.defEvalConfigItemCmd` for further documentation.

See also `declare_core_config_elab`, `declare_term_config_elab`, and `declare_config_elab`.
 -/
Lean.Elab.ConfigEval.declareCommandConfig : Lean.ParserDescr
-- Mathlib.CategoryTheory.PEmpty
/-- Any two functors out of an empty category are isomorphic.  -/
CategoryTheory.Functor.isEmptyExt : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} D] → [IsEmpty C] → (F G : CategoryTheory.Functor C D) → F ≅ G
-- Mathlib.Data.Nat.Count
/-- **Alias** of the reverse direction of `Nat.count_iff_forall`. -/
Nat.count_of_forall : ∀ {p : ℕ → Prop} [inst : DecidablePred p] {n : ℕ}, (∀ n' < n, p n') → Nat.count p n = n
-- Mathlib.MeasureTheory.Integral.Bochner.L1
/-- `SimpleFunc.integral` and `SimpleFunc.lintegral` agree when the integrand has type
`α →ₛ ℝ≥0∞`. But since `ℝ≥0∞` is not a `NormedSpace`, we need some form of coercion.  -/
MeasureTheory.SimpleFunc.integral_eq_lintegral : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : MeasureTheory.SimpleFunc α ℝ},
  MeasureTheory.Integrable (⇑f) μ →
    0 ≤ᵐ[μ] ⇑f → MeasureTheory.SimpleFunc.integral μ f = (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal
-- Mathlib.Analysis.Complex.Exponential
Complex.exp_multiset_sum : ∀ (s : Multiset ℂ), Complex.exp s.sum = (Multiset.map Complex.exp s).prod
-- Mathlib.Data.PNat.Xgcd
/-- Extended Euclidean algorithm  -/
PNat.xgcd : ℕ+ → ℕ+ → PNat.XgcdType
-- Init.Prelude
/-- Resolves the given name to an overload list of namespaces.  -/
Lean.Macro.resolveNamespace : Lean.Name → Lean.MacroM (List Lean.Name)
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.mk_lt_mk : ∀ {α : Type u_2} [inst : BooleanAlgebra α] {L M : Sublattice α} (hL_compl : ∀ {a : α}, a ∈ L.carrier → aᶜ ∈ L.carrier)
  (hL_bot : ⊥ ∈ L.carrier) (hM_compl : ∀ {a : α}, a ∈ M.carrier → aᶜ ∈ M.carrier) (hM_bot : ⊥ ∈ M.carrier),
  { toSublattice := L, compl_mem' := hL_compl, bot_mem' := hL_bot } <
      { toSublattice := M, compl_mem' := hM_compl, bot_mem' := hM_bot } ↔
    L < M
-- Mathlib.LinearAlgebra.Quotient.Pi
Submodule.quotientPi_aux.left_inv : ∀ {ι : Type u_1} {R : Type u_2} [inst : CommRing R] {Ms : ι → Type u_3} [inst_1 : (i : ι) → AddCommGroup (Ms i)]
  [inst_2 : (i : ι) → Module R (Ms i)] (p : (i : ι) → Submodule R (Ms i)) [inst_3 : Fintype ι] [inst_4 : DecidableEq ι],
  Function.LeftInverse (Submodule.quotientPi_aux.invFun p) (Submodule.quotientPi_aux.toFun p)
-- Aesop.Util.EqualUpToIds
Aesop.EqualUpToIds.Unsafe.localContextsEqualUpToIdsCore : Lean.LocalContext →
  Lean.LocalContext →
    Lean.LocalInstances → Lean.LocalInstances → Aesop.EqualUpToIdsM (Option Aesop.EqualUpToIds.GoalContext)
-- Mathlib.Analysis.LocallyConvex.AbsConvexOpen
/-- The family of seminorms defined by the gauges of absolute convex open sets.  -/
gaugeSeminormFamily : (𝕜 : Type u_1) →
  (E : Type u_2) →
    [inst : RCLike 𝕜] →
      [inst_1 : AddCommGroup E] →
        [inst_2 : TopologicalSpace E] →
          [inst_3 : Module 𝕜 E] →
            [inst_4 : Module ℝ E] →
              [IsScalarTower ℝ 𝕜 E] → [ContinuousSMul ℝ E] → SeminormFamily 𝕜 E (AbsConvexOpenSets 𝕜 E)
-- Mathlib.Data.Real.ConjExponents
Real.HolderTriple.one_div_eq : ∀ {p q r : ℝ}, p.HolderTriple q r → 1 / r = 1 / p + 1 / q
-- Mathlib.Algebra.Order.Archimedean.Class
FiniteMulArchimedeanClass.min_le_mk_mul : ∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M] {a b : M} (ha : a ≠ 1)
  (hb : b ≠ 1) (hab : a * b ≠ 1),
  min (FiniteMulArchimedeanClass.mk a ha) (FiniteMulArchimedeanClass.mk b hb) ≤ FiniteMulArchimedeanClass.mk (a * b) hab
-- Mathlib.Order.Bounds.Defs
BddBelow.eq_1 : ∀ {α : Type u_1} [inst : LE α] (s : Set α), BddBelow s = (lowerBounds s).Nonempty
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get?_union_of_not_mem_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {k : α}, k ∉ m₁ → Std.DHashMap.Const.get? (m₁.union m₂) k = Std.DHashMap.Const.get? m₂ k
-- Mathlib.Algebra.Notation.Support
Function.support_extend_zero : ∀ {ι : Type u_1} {κ : Type u_2} {N : Type u_4} [inst : Zero N] {f : ι → κ} {g : ι → N},
  Function.Injective f → Function.support (Function.extend f g 0) = f '' Function.support g
-- Mathlib.Geometry.Manifold.MFDeriv.FDeriv
/-- For maps between vector spaces, `mfderiv` and `fderiv` coincide  -/
mfderiv_eq_fderiv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {f : E → E'}
  {x : E}, mfderiv% f x = fderiv 𝕜 f x
-- Mathlib.Data.Fintype.Sum
instFintypeSum : (α : Type u) → (β : Type v) → [Fintype α] → [Fintype β] → Fintype (α ⊕ β)