mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Sites.EffectiveEpimorphic
/-- The sieve of morphisms which factor through a given morphism `f`.
This is equal to `Sieve.generate (Presieve.singleton f)`, but has
more convenient definitional properties.
 -/
CategoryTheory.Sieve.generateSingleton : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → {X Y : C} → (Y ⟶ X) → CategoryTheory.Sieve X
-- Mathlib.Geometry.Manifold.Instances.Sphere
/-- The unit sphere in an `n + 1`-dimensional inner product space `E` is an analytic manifold,
modelled on the Euclidean space of dimension `n`.  -/
EuclideanSpace.instIsManifoldSphere : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {n : ℕ}
  [inst_2 : Fact (Module.finrank ℝ E = n + 1)],
  IsManifold (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) ⊤ ↑(Metric.sphere 0 1)
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
SubalgebraClass.coe_algebraMap : ∀ {S : Type u_1} {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : SetLike S A] [inst_4 : SubsemiringClass S A] [hSR : SMulMemClass S R A] (s : S) (r : R),
  ↑((algebraMap R ↥s) r) = (algebraMap R A) r
-- Mathlib.GroupTheory.QuotientGroup.Basic
/-- `(G × H) / (A × B)` is isomorphic to `G / A × H / B`.  -/
QuotientGroup.prodMulEquiv : {G : Type u} →
  [inst : Group G] →
    {H : Type v} →
      [inst_1 : Group H] →
        (A : Subgroup G) →
          (B : Subgroup H) → [inst_2 : A.Normal] → [inst_3 : B.Normal] → (G × H) ⧸ A.prod B ≃* (G ⧸ A) × H ⧸ B
-- Mathlib.Algebra.GCDMonoid.Multiset
Multiset.gcd_ne_zero_iff : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] (s : Multiset α),
  s.gcd ≠ 0 ↔ ∃ x ∈ s, x ≠ 0
-- Mathlib.Algebra.Quandle
/-- A monoid is *graphic* if, for all `x` and `y`, the *graphic identity*
`(x * y) * x = x * y` holds.  For a unital shelf, this graphic
identity holds.
 -/
UnitalShelf.act_act_self_eq : ∀ {S : Type u_1} [inst : UnitalShelf S] (x y : S), Shelf.act (Shelf.act x y) x = Shelf.act x y
-- Mathlib.CategoryTheory.Shift.Induced
CategoryTheory.HasShift.Induced.zero_hom_app_obj : ∀ {C : Type u_3} {D : Type u_1} [inst : CategoryTheory.Category.{v_1, u_3} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_1} D] (F : CategoryTheory.Functor C D) {A : Type u_2} [inst_2 : AddMonoid A]
  [inst_3 : CategoryTheory.HasShift C A] (s : A → CategoryTheory.Functor D D)
  (i : (a : A) → F.comp (s a) ≅ (CategoryTheory.shiftFunctor C a).comp F)
  [inst_4 : ((CategoryTheory.Functor.whiskeringLeft C D D).obj F).Full]
  [inst_5 : ((CategoryTheory.Functor.whiskeringLeft C D D).obj F).Faithful] (X : C),
  (CategoryTheory.HasShift.Induced.zero F s i).hom.app (F.obj X) =
    CategoryTheory.CategoryStruct.comp ((i 0).hom.app X) (F.map ((CategoryTheory.shiftFunctorZero C A).hom.app X))
-- Mathlib.Data.ENNReal.Basic
ENNReal.instBoundedOrder : BoundedOrder ENNReal
-- Mathlib.AlgebraicGeometry.Spec
/-- Under the isomorphisms `stalkIso`, the map `stalkMap (Spec.sheafedSpaceMap f) p` corresponds
to the induced local ring homomorphism `Localization.localRingHom`.
 -/
AlgebraicGeometry.localRingHom_comp_stalkIso_apply : ∀ {R S : CommRingCat} (f : R ⟶ S) (p : PrimeSpectrum ↑S)
  (x : ↑((AlgebraicGeometry.structurePresheafInCommRingCat ↑R).stalk (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p))),
  (IsLocalization.map (↑((AlgebraicGeometry.structurePresheafInCommRingCat ↑S).stalk p)) (RingHom.id ↑S) ⋯)
      ((Localization.localRingHom (Ideal.comap (CommRingCat.Hom.hom f) p.asIdeal) p.asIdeal (CommRingCat.Hom.hom f) ⋯)
        ((AlgebraicGeometry.StructureSheaf.stalkIso (↑R) (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p)).symm x)) =
    (CategoryTheory.ConcreteCategory.hom
        (AlgebraicGeometry.PresheafedSpace.Hom.stalkMap (AlgebraicGeometry.Spec.sheafedSpaceMap f).hom p))
      x
-- Mathlib.RingTheory.TotallySplit
/-- If `S` is finite étale over `R` of (constant) rank `n`, there exists
a finite faithfully flat, étale `R`-algebra `T` such that `T ⊗[R] S` is split of rank `n`
over `T`.
This is the commutative algebra version of
[Lenstra, Galois theory for schemes, 5.10][lenstraGSchemes].
 -/
Algebra.IsFiniteSplit.exists_tensorProduct_of_etale : ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [Algebra.Etale R S]
  [Module.Finite R S] {n : ℕ},
  Module.rankAtStalk S = ↑n →
    ∃ T x x_1,
      ∃ (_ : Module.FaithfullyFlat R T) (_ : Module.Finite R T) (_ : Algebra.Etale R T),
        Algebra.IsFiniteSplit T (TensorProduct R T S)
-- Mathlib.Algebra.Category.Semigrp.Basic
AddMagmaCat.instConcreteCategoryAddHomCarrier : CategoryTheory.ConcreteCategory AddMagmaCat fun x1 x2 => ↑x1 →ₙ+ ↑x2
-- Init.Data.UInt.Bitwise
UInt32.xor_neg_one : ∀ {a : UInt32}, a ^^^ -1 = ~~~a
-- Mathlib.Analysis.Normed.Lp.lpSpace
Memℓp.star_iff : ∀ {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [inst : (i : α) → NormedAddCommGroup (E i)]
  [inst_1 : (i : α) → StarAddMonoid (E i)] [∀ (i : α), NormedStarGroup (E i)] {f : (i : α) → E i},
  Memℓp (star f) p ↔ Memℓp f p
-- Lean.Syntax
/-- Advance to the parent of the current node, if any.  -/
Lean.Syntax.Traverser.up : Lean.Syntax.Traverser → Lean.Syntax.Traverser
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
AntitoneOn.sInf_image_Icc : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : ConditionallyCompleteLattice β] {f : α → β} {a b : α},
  a ≤ b → AntitoneOn f (Set.Icc a b) → sInf (f '' Set.Icc a b) = f b
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.weierstrassP_neg : ∀ (L : PeriodPair) (z : ℂ), L.weierstrassP (-z) = L.weierstrassP z
-- Mathlib.SetTheory.Cardinal.Cofinality.Club
IsClub.sInter : ∀ {α : Type v} [inst : LinearOrder α] [WellFoundedLT α] {s : Set (Set α)},
  Order.cof α ≠ Cardinal.aleph0 → Cardinal.mk ↑s < Order.cof α → (∀ x ∈ s, IsClub x) → IsClub (⋂₀ s)
-- Mathlib.CategoryTheory.Action.Basic
/-- The functor from `Action V H` to `Action V G` induced by a monoid homomorphism
`f : G →* H` is full if `f` is surjective.  -/
Action.full_res : ∀ (V : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_3} {H : Type u_4} [inst_1 : Monoid G]
  [inst_2 : Monoid H] (f : G →* H), Function.Surjective ⇑f → (Action.res V f).Full
-- Mathlib.Geometry.Manifold.HasGroupoid
/-- If a single open partial homeomorphism `e` from a space `α` into `H` has source covering the
whole space `α`, then that open partial homeomorphism induces an `H`-charted space structure on `α`.
(This condition is equivalent to `e` being an open embedding of `α` into `H`; see
`IsOpenEmbedding.singletonChartedSpace`.)  -/
OpenPartialHomeomorph.singletonChartedSpace : {H : Type u} →
  [inst : TopologicalSpace H] →
    {α : Type u_5} →
      [inst_1 : TopologicalSpace α] → (e : OpenPartialHomeomorph α H) → e.source = Set.univ → ChartedSpace H α
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.powerlt_le_powerlt_left : ∀ {a b c : Cardinal.{u_1}}, b ≤ c → a ^< b ≤ a ^< c
-- Mathlib.CategoryTheory.Limits.Bicones
CategoryTheory.biconeCategoryStruct : (J : Type u₁) →
  [CategoryTheory.Category.{v₁, u₁} J] → CategoryTheory.CategoryStruct.{max u₁ v₁, u₁} (CategoryTheory.Bicone J)
-- Mathlib.Control.Random
Random.mk : {m : Type u → Type u_1} → {α : Type u} → ({g : Type} → [RandomGen g] → RandGT g m α) → Random m α
-- Mathlib.Topology.Order.Monotone
AntitoneOn.tendsto_nhdsWithin_Ioo_right : ∀ {α : Type u_3} {β : Type u_4} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α]
  [inst_3 : ConditionallyCompleteLinearOrder β] [inst_4 : TopologicalSpace β] [OrderTopology β] {f : α → β} {x y : α},
  (Set.Ioo x y).Nonempty →
    AntitoneOn f (Set.Ioo x y) →
      BddAbove (f '' Set.Ioo x y) → Filter.Tendsto f (nhdsWithin x (Set.Ioi x)) (nhds (sSup (f '' Set.Ioo x y)))
-- Mathlib.RingTheory.Bialgebra.Hom
/-- Turn a bialgebra homomorphism into an algebra homomorphism.  -/
BialgHom.toAlgHom : {R : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Semiring B] →
            [inst_3 : Algebra R A] →
              [inst_4 : Algebra R B] →
                [inst_5 : CoalgebraStruct R A] → [inst_6 : CoalgebraStruct R B] → (A →ₐc[R] B) → A →ₐ[R] B
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
/-- The canonical map from `Lᵖ ν` to `Lᵖ μ` when `μ` is bounded by a finite multiple of `ν`.
This is the linear map version. Use instead the continuous linear map
version `LpToLpOfMeasureLeSMul`  -/
_private.Mathlib.MeasureTheory.Function.LpSpace.Basic.0.MeasureTheory.Lp.LpToLpOfMeasureLeSMulₗ : {α : Type u_1} →
  {E : Type u_4} →
    {m : MeasurableSpace α} →
      {p : ENNReal} →
        {μ : MeasureTheory.Measure α} →
          [inst : NormedAddCommGroup E] →
            [inst_1 : NormedSpace ℝ E] →
              {ν : MeasureTheory.Measure α} →
                {c : ENNReal} → c ≠ ⊤ → μ ≤ c • ν → ↥(MeasureTheory.Lp E p ν) →ₗ[ℝ] ↥(MeasureTheory.Lp E p μ)
-- Aesop.Util.OrderedHashSet
Aesop.OrderedHashSet.mk : {α : Type u_1} → [inst : BEq α] → [inst_1 : Hashable α] → Array α → Std.HashSet α → Aesop.OrderedHashSet α
-- Mathlib.CategoryTheory.Comma.Basic
/-- The functor `(F ⋙ L, R) ⥤ (L, R)`  -/
CategoryTheory.Comma.preLeft : {A : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} A] →
    {B : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
        {T : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} T] →
            {C : Type u₄} →
              [inst_3 : CategoryTheory.Category.{v₄, u₄} C] →
                (F : CategoryTheory.Functor C A) →
                  (L : CategoryTheory.Functor A T) →
                    (R : CategoryTheory.Functor B T) →
                      CategoryTheory.Functor (CategoryTheory.Comma (F.comp L) R) (CategoryTheory.Comma L R)
-- Mathlib.RingTheory.WittVector.Truncated
WittVector.truncate_comp_lift : ∀ {p : ℕ} (n : ℕ) {R : Type u_1} [inst : CommRing R] [inst_1 : Fact (Nat.Prime p)] {S : Type u_2} [inst_2 : Semiring S]
  {f : (k : ℕ) → S →+* TruncatedWittVector p k R}
  (f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), (TruncatedWittVector.truncate hk).comp (f k₂) = f k₁),
  (WittVector.truncate n).comp (WittVector.lift f f_compat) = f n
-- Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
IsLocalDiffeomorphAt.isBoundaryPoint_iff : ∀ {𝕜 : 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'}
  {N : Type u_7} [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace H' N] {n : WithTop ℕ∞},
  n ≠ 0 → ∀ {f : M → N} {x : M}, IsLocalDiffeomorphAt I I' n f x → (I.IsBoundaryPoint x ↔ I'.IsBoundaryPoint (f x))
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
/-- The norm, relative to `ℤ`, of `ζ - 1` in a `2`-th cyclotomic extension of `ℚ` is `-2`.
 -/
IsPrimitiveRoot.norm_toInteger_sub_one_of_eq_two : ∀ {K : Type u} [inst : Field K] {ζ : K} [inst_1 : CharZero K] [IsCyclotomicExtension {2} ℚ K]
  (hζ : IsPrimitiveRoot ζ 2), (Algebra.norm ℤ) (hζ.toInteger - 1) = -2
-- Mathlib.CategoryTheory.Functor.OfSequence
CategoryTheory.NatTrans.ofSequence_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {F G : CategoryTheory.Functor ℕ C}
  (app : (n : ℕ) → F.obj n ⟶ G.obj n)
  (naturality :
    ∀ (n : ℕ),
      CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.homOfLE ⋯)) (app (n + 1)) =
        CategoryTheory.CategoryStruct.comp (app n) (G.map (CategoryTheory.homOfLE ⋯)))
  (n : ℕ), (CategoryTheory.NatTrans.ofSequence app naturality).app n = app n
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
SubMulAction.ofFixingSubgroup.append.eq_1 : ∀ {M : Type u_1} {α : Type u_2} [inst : Group M] [inst_1 : MulAction M α] {s : Set α} {n : ℕ} [inst_2 : Finite ↑s]
  (x : Fin n ↪ ↥(SubMulAction.ofFixingSubgroup M s)), SubMulAction.ofFixingSubgroup.append x = Fin.Embedding.append ⋯
-- Mathlib.Data.Int.Log
Int.log_zero_right : ∀ {R : Type u_1} [inst : Semifield R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] [inst_3 : FloorSemiring R]
  (b : ℕ), Int.log b 0 = 0
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
NonUnitalSubsemiring.coe_centralizer : ∀ {R : Type u_1} [inst : NonUnitalSemiring R] (s : Set R), ↑(NonUnitalSubsemiring.centralizer s) = s.centralizer
-- Mathlib.Logic.Relation
Relation.map_mono : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {r s : α → β → Prop} {f : α → γ} {g : β → δ},
  r ≤ s → Relation.Map r f g ≤ Relation.Map s f g
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.InlayHintKind.type : Lean.Lsp.InlayHintKind
-- Lean.Data.Lsp.Diagnostics
Lean.Lsp.DiagnosticCode.int.injEq : ∀ (i i_1 : ℤ), (Lean.Lsp.DiagnosticCode.int i = Lean.Lsp.DiagnosticCode.int i_1) = (i = i_1)
-- Init.PropLemmas
exists_eq_right_right : ∀ {α : Sort u_1} {p q : α → Prop} {a' : α}, (∃ a, p a ∧ q a ∧ a = a') ↔ p a' ∧ q a'
-- Mathlib.LinearAlgebra.Prod
LinearMap.prodMap_comap_prod : ∀ {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} {M₄ : Type z} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M₃] [inst_4 : AddCommMonoid M₄] [inst_5 : Module R M]
  [inst_6 : Module R M₂] [inst_7 : Module R M₃] [inst_8 : Module R M₄] (f : M →ₗ[R] M₂) (g : M₃ →ₗ[R] M₄)
  (S : Submodule R M₂) (S' : Submodule R M₄),
  Submodule.comap (f.prodMap g) (S.prod S') = (Submodule.comap f S).prod (Submodule.comap g S')
-- Mathlib.GroupTheory.GroupAction.Blocks
AddAction.IsBlock.of_addSubgroup_of_conjugate : ∀ {G : Type u_1} [inst : AddGroup G] {X : Type u_2} [inst_1 : AddAction G X] {B : Set X} {H : AddSubgroup G},
  AddAction.IsBlock (↥H) B →
    ∀ (g : G), AddAction.IsBlock (↥(AddSubgroup.map (AddEquiv.toAddMonoidHom (AddAut.addConj g)) H)) (g +ᵥ B)
-- Mathlib.RingTheory.RamificationInertia.Ramification
/-- **Alias** of `Ideal.ramificationIdx_below_dvd`. -/
Ideal.ramificationIdx'_below_dvd : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  [inst_3 : Algebra R S] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [IsScalarTower R S T] (q : Ideal S) (r : Ideal T)
  [r.LiesOver q] [Module.Flat S T], q.ramificationIdx R ∣ r.ramificationIdx R
-- Std.Http.Internal.IndexMultiMap
_private.Std.Http.Internal.IndexMultiMap.0.Std.Internal.IndexMultiMap.insert.match_1.congr_eq_1 : ∀ (motive : Option (Array ℕ) → Sort u_1) (x : Option (Array ℕ)) (h_1 : (idxs : Array ℕ) → motive (some idxs))
  (h_2 : Unit → motive none) (idxs : Array ℕ),
  x = some idxs →
    (match x with
      | some idxs => h_1 idxs
      | none => h_2 ()) ≍
      h_1 idxs
-- Mathlib.CategoryTheory.Localization.HomEquiv
CategoryTheory.Localization.homEquiv_map : ∀ {C : Type u_1} {D₁ : Type u_5} {D₂ : Type u_6} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_5, u_5} D₁] [inst_2 : CategoryTheory.Category.{v_6, u_6} D₂]
  (W : CategoryTheory.MorphismProperty C) (L₁ : CategoryTheory.Functor C D₁) [inst_3 : L₁.IsLocalization W]
  (L₂ : CategoryTheory.Functor C D₂) [inst_4 : L₂.IsLocalization W] {X Y : C} (f : X ⟶ Y),
  (CategoryTheory.Localization.homEquiv W L₁ L₂) (L₁.map f) = L₂.map f
-- Mathlib.Topology.MetricSpace.PiNat
/-- `cylinder x n` is equal to the set of sequences `y` with the same restriction to `n` as `x`.  -/
PiNat.cylinder_eq_res : ∀ {α : Type u_2} (x : ℕ → α) (n : ℕ), PiNat.cylinder x n = {y | PiNat.res y n = PiNat.res x n}
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrp.tensorAddUnit_add : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C], CategoryTheory.AddMonObj.add = CategoryTheory.AddMonObj.add
-- Mathlib.Tactic.Translate.Core
/-- Copies equation lemmas and attributes from `src` to `tgt`.  -/
Mathlib.Tactic.Translate.copyMetaData : Mathlib.Tactic.Translate.TranslateData →
  Mathlib.Tactic.Translate.Config → Lean.Name → Lean.Name → Lean.CoreM (Array Lean.Name)
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.insertIdxTR.go.match_1.eq_2 : ∀ {α : Type u_1} (motive : ℕ → List α → Array α → Sort u_2) (x : ℕ) (acc : Array α)
  (h_1 : (l : List α) → (acc : Array α) → motive 0 l acc) (h_2 : (x : ℕ) → (acc : Array α) → motive x [] acc)
  (h_3 : (n : ℕ) → (a : α) → (l : List α) → (acc : Array α) → motive n.succ (a :: l) acc),
  (x = 0 → False) →
    (match x, [], acc with
      | 0, l, acc => h_1 l acc
      | x, [], acc => h_2 x acc
      | n.succ, a :: l, acc => h_3 n a l acc) =
      h_2 x acc
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddMonoidHom.snd_toFun : ∀ (A : Type u_2) (B : Type u_3) [inst : AddMonoid A] [inst_1 : AddMonoid B] [inst_2 : TopologicalSpace A]
  [inst_3 : TopologicalSpace B] (self : A × B), (ContinuousAddMonoidHom.snd A B) self = self.2
-- Mathlib.Analysis.Calculus.VectorField
VectorField.lieBracket_add_right : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {V W W₁ : E → E} {x : E},
  DifferentiableAt 𝕜 W x →
    DifferentiableAt 𝕜 W₁ x →
      VectorField.lieBracket 𝕜 V (W + W₁) x = VectorField.lieBracket 𝕜 V W x + VectorField.lieBracket 𝕜 V W₁ x
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getElem?_inter_of_not_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α},
  k ∉ t₂ → (t₁ ∩ t₂)[k]? = none
-- Mathlib.Topology.DiscreteSubset
IsDiscrete.eq_of_specializes : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X}, IsDiscrete s → ∀ {a b : X}, a ⤳ b → a ∈ s → b ∈ s → a = b
-- Mathlib.Algebra.MonoidAlgebra.Basic
MonoidAlgebra.toAdditiveAlgEquiv_single : ∀ {R : Type u_1} {A : Type u_4} {M : Type u_7} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Monoid M] (m : M) (a : A),
  (MonoidAlgebra.toAdditiveAlgEquiv R A M) (MonoidAlgebra.single m a) = AddMonoidAlgebra.single (Additive.ofMul m) a
-- Init.Data.Format.Basic
_private.Init.Data.Format.Basic.0.Std.Format.State.mk.injEq : ∀ (out : String) (column : ℕ) (out_1 : String) (column_1 : ℕ),
  ({ out := out, column := column } = { out := out_1, column := column_1 }) = (out = out_1 ∧ column = column_1)
-- Lean.Elab.MutualDef
_private.Lean.Elab.MutualDef.0.Lean.Elab.Term.elabMutualDef.elabSync : Array Lean.Expr →
  Lean.Elab.Command.Scope → Array Lean.Elab.DefView → Array Lean.Elab.DefViewElabHeader → Lean.Elab.TermElabM Unit
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.get_eq_getD : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α],
  m.WF → ∀ {a : α} {fallback : β a} {h : a ∈ m}, m.get a h = m.getD a fallback
-- Mathlib.FieldTheory.PurelyInseparable.Exponent
/-- The element `y` of the base field `K` such that
`a ^ ringExpChar K ^ elemExponent K a = algebraMap K L y`.
See `IsPurelyInseparable.algebraMap_elemReduct_eq`.  -/
IsPurelyInseparable.elemReduct : (K : Type u_2) →
  {L : Type u_3} → [inst : Field K] → [inst_1 : Field L] → [inst_2 : Algebra K L] → [IsPurelyInseparable K L] → L → K
-- Init.MetaTypes
Lean.Module.commands : Lean.Module → Array Lean.Syntax
-- Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
_private.Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm.0.mu.congr_simp : ∀ {R : Type u_1} [inst : CommRing R] (μ μ_1 : RingSeminorm R) (e_μ : μ = μ_1) {x x_1 : R} (e_x : x = x_1) {y y_1 : R}
  (e_y : y = y_1) (hn : ∀ (n : ℕ), ∃ m < n + 1, μ ((x + y) ^ n) ^ (1 / ↑n) ≤ (μ (x ^ m) * μ (y ^ (n - m))) ^ (1 / ↑n))
  (a a_1 : ℕ), a = a_1 → mu✝ μ hn a = mu✝ μ_1 ⋯ a_1
-- Mathlib.CategoryTheory.Discrete.Basic
/-- We can convert an equivalence of `discrete` categories to a type-level `Equiv`.  -/
CategoryTheory.Discrete.equivOfEquivalence : {α : Type u₁} → {β : Type u₂} → (CategoryTheory.Discrete α ≌ CategoryTheory.Discrete β) → α ≃ β
-- Lean.Meta.Tactic.Grind.EMatchTheorem
Lean.Meta.Grind.GenPatternInfo.mk.sizeOf_spec : ∀ (heq : Bool) (hIdx xIdx : ℕ),
  sizeOf { heq := heq, hIdx := hIdx, xIdx := xIdx } = 1 + sizeOf heq + sizeOf hIdx + sizeOf xIdx
-- Init.Data.Fin.Lemmas
Fin.rev_castSucc : ∀ {n : ℕ} (k : Fin n), k.castSucc.rev = k.rev.succ
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
CategoryTheory.MonoidalCategory.DayConvolutionUnit.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {V : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} V] →
        [inst_2 : CategoryTheory.MonoidalCategory C] →
          [inst_3 : CategoryTheory.MonoidalCategory V] →
            {F : CategoryTheory.Functor C V} →
              (can :
                  CategoryTheory.MonoidalCategoryStruct.tensorUnit V ⟶
                    F.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) →
                (CategoryTheory.Functor.LeftExtension.mk F
                      { app := fun x => can, naturality := ⋯ }).IsPointwiseLeftKanExtension →
                  CategoryTheory.MonoidalCategory.DayConvolutionUnit F
-- Init.Data.List.Basic
List.range'_succ : ∀ {s n step : ℕ}, List.range' s (n + 1) step = s :: List.range' (s + step) n step
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.dropKeys : {α : Type} →
  Lean.Meta.LazyDiscrTree α → List (List Lean.Meta.LazyDiscrTree.Key) → Lean.MetaM (Lean.Meta.LazyDiscrTree α)
-- Mathlib.Algebra.Notation.Support
Pi.mulSupport_mulSingle_one : ∀ {ι : Type u_1} {M : Type u_3} [inst : DecidableEq ι] [inst_1 : One M] {i : ι},
  Function.mulSupport (Pi.mulSingle i 1) = ∅
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.true_and : ∀ {σs : List (Type u)} {P : Std.Do.SPred σs}, ⌜True⌝ ∧ P ⊣⊢ₛ P
-- Mathlib.ModelTheory.Complexity
FirstOrder.Language.BoundedFormula.IsAtomic.isUniversal : ∀ {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {φ : L.BoundedFormula α n}, φ.IsAtomic → φ.IsUniversal
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.sum_const_nat : ∀ {ι : Type u_1} {s : Finset ι} {m : ℕ} {f : ι → ℕ}, (∀ x ∈ s, f x = m) → ∑ x ∈ s, f x = s.card * m
-- Mathlib.Topology.MetricSpace.Pseudo.Basic
Metric.totallyBounded_iff : ∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α},
  TotallyBounded s ↔ ∀ ε > 0, ∃ t, t.Finite ∧ s ⊆ ⋃ y ∈ t, Metric.ball y ε
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Iio_ssubset_Iio_iff : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, Set.Iio b ⊂ Set.Iio a ↔ b < a
-- Mathlib.SetTheory.Ordinal.Family
/-- `ciSup_le_iff'` whenever the input type is small in the output universe.  -/
Ordinal.iSup_le_iff : ∀ {ι : Type u_3} {f : ι → Ordinal.{u}} {a : Ordinal.{u}} [Small.{u, u_3} ι], ⨆ i, f i ≤ a ↔ ∀ (i : ι), f i ≤ a
-- Batteries.Data.List.Basic
/-- Returns the elements of `l` that satisfy `p` together with their indexes in
`l` added to an optional parameter `start`. The returned list is ordered by index.
We have `l.findIdxsValues p s = (l.findIdxs p s).zip (l.filter p)`.
 -/
List.findIdxsValues : {α : Type u_1} → (α → Bool) → List α → optParam ℕ 0 → List (ℕ × α)
-- Lean.Widget.InteractiveDiagnostic
_private.Lean.Widget.InteractiveDiagnostic.0.Lean.Widget.mkPPContext : Lean.NamingContext → Lean.MessageDataContext → Lean.PPContext
-- Mathlib.LinearAlgebra.AffineSpace.Matrix
AffineBasis.toMatrix_mul_toMatrix : ∀ {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [inst : AddCommGroup V] [inst_1 : AddTorsor V P]
  [inst_2 : Ring k] [inst_3 : Module k V] (b : AffineBasis ι k P) [inst_4 : Fintype ι] (b₂ : AffineBasis ι k P)
  [inst_5 : DecidableEq ι], b.toMatrix ⇑b₂ * b₂.toMatrix ⇑b = 1
-- Init.Data.UInt.Bitwise
UInt16.zero_and : ∀ {a : UInt16}, 0 &&& a = 0
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
sub_le_sub_iff : ∀ {α : Type u} [inst : AddCommGroup α] [inst_1 : LE α] [AddLeftMono α] {a b c d : α}, a - b ≤ c - d ↔ a + d ≤ c + b