mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Probability.Kernel.Disintegration.Density
ProbabilityTheory.Kernel.measurable_density_left : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} [inst : MeasurableSpace.CountablyGenerated γ] (κ : ProbabilityTheory.Kernel α (γ × β))
  (ν : ProbabilityTheory.Kernel α γ) (x : γ) {s : Set β}, MeasurableSet s → Measurable fun a => κ.density ν a x s
-- Mathlib.RingTheory.Localization.LocalizationLocalization
IsLocalization.localization_localization_surj : ∀ {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] (x : T),
  ∃ y, x * (algebraMap R T) ↑y.2 = (algebraMap R T) y.1
-- Lean.Data.Lsp.Basic
Lean.Lsp.DocumentChange.create.inj : ∀ {a a_1 : Lean.Lsp.CreateFile}, Lean.Lsp.DocumentChange.create a = Lean.Lsp.DocumentChange.create a_1 → a = a_1
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.concat_cons : ∀ {V : Type u} {G : SimpleGraph V} {u v w x : V} (h : G.Adj u v) (p : G.Walk v w) (h' : G.Adj w x),
  (SimpleGraph.Walk.cons h p).concat h' = SimpleGraph.Walk.cons h (p.concat h')
-- Std.Do.Triple.Basic
Std.Do.Triple.bind : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} [inst : Monad m] [inst_1 : Std.Do.WPMonad m ps] {α β : Type u}
  {P : Std.Do.Assertion ps} {Q : α → Std.Do.Assertion ps} {R : Std.Do.PostCond β ps} (x : m α) (f : α → m β),
  ⦃P⦄ x ⦃(Q, R.2)⦄ → (∀ (b : α), ⦃Q b⦄ f b ⦃R⦄) → ⦃P⦄ (x >>= f) ⦃R⦄
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKeyD_minKeyD : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp],
  t ≠ ∅ → ∀ {fallback fallback' : α}, t.getKeyD (t.minKeyD fallback) fallback' = t.minKeyD fallback
-- Mathlib.RingTheory.Extension.Presentation.Submersive
/-- Given a submersive presentation `P` and equivalences `ι' ≃ ι` and
`σ' ≃ σ`, this is the induced submersive presentation with variables indexed
by `ι'` and relations indexed by `σ'`  -/
Algebra.SubmersivePresentation.reindex : {R : Type u} →
  {S : Type v} →
    {ι : Type w} →
      {σ : Type t} →
        [inst : CommRing R] →
          [inst_1 : CommRing S] →
            [inst_2 : Algebra R S] →
              [inst_3 : Finite σ] →
                Algebra.SubmersivePresentation R S ι σ →
                  {ι' : Type u_1} →
                    {σ' : Type u_2} → [inst_4 : Finite σ'] → ι' ≃ ι → σ' ≃ σ → Algebra.SubmersivePresentation R S ι' σ'
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.coeff_single : ∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : Zero R] {a b : Γ} {r : R},
  ((HahnSeries.single a) r).coeff b = if b = a then r else 0
-- Mathlib.FieldTheory.RatFunc.Valuation
RatFunc.inftyValuation.X_inv : ∀ (F : Type u_1) [inst : Field F] [inst_1 : DecidableEq (RatFunc F)],
  (RatFunc.inftyValuation F) (1 / RatFunc.X) = WithZero.exp (-1)
-- Mathlib.Analysis.Calculus.FDeriv.Pow
differentiableAt_pow : ∀ {𝕜 : Type u_1} {𝔸 : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedRing 𝔸] [inst_2 : NormedAlgebra 𝕜 𝔸]
  (n : ℕ) {x : 𝔸}, DifferentiableAt 𝕜 (fun x => x ^ n) x
-- Mathlib.Algebra.Lie.EngelSubalgebra
/-- The Engel subalgebra `Engel R x` consists of
all `y : L` such that `(ad R L x)^n` kills `y` for some `n`.

Engel subalgebras are self-normalizing (`LieSubalgebra.normalizer_engel`),
and minimal ones are nilpotent, hence Cartan subalgebras.  -/
LieSubalgebra.engel : (R : Type u_1) →
  {L : Type u_2} → [inst : CommRing R] → [inst_1 : LieRing L] → [inst_2 : LieAlgebra R L] → L → LieSubalgebra R L
-- Mathlib.RingTheory.SurjectiveOnStalks
RingHom.SurjectiveOnStalks.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] {S : Type u_2} [inst_1 : CommRing S] (f : R →+* S),
  f.SurjectiveOnStalks =
    ∀ (P : Ideal S) (x : P.IsPrime), Function.Surjective ⇑(Localization.localRingHom (Ideal.comap f P) P f ⋯)
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
ciInf_le' : ∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompleteLinearOrderBot α] (f : ι → α) (i : ι), iInf f ≤ f i
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- A functor from the costructured arrow category on the projection functor for any costructured
arrow category.  -/
CategoryTheory.CostructuredArrow.ofCostructuredArrowProjEquivalence.functor : {T : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} T] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor T D) →
          (Y : D) →
            (X : T) →
              CategoryTheory.Functor (CategoryTheory.CostructuredArrow (CategoryTheory.CostructuredArrow.proj F Y) X)
                (CategoryTheory.CostructuredArrow ((CategoryTheory.Over.forget X).comp F) Y)
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.comp_X : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p.comp Polynomial.X = p
-- Mathlib.FieldTheory.AlgebraicClosure
/-- If `K / E / F` is a field extension tower, then `algebraicClosure F K` is contained in
`algebraicClosure E K`.  -/
algebraicClosure.le_restrictScalars : ∀ (F : Type u_1) (E : Type u_2) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (K : Type u_3)
  [inst_3 : Field K] [inst_4 : Algebra F K] [inst_5 : Algebra E K] [inst_6 : IsScalarTower F E K],
  algebraicClosure F K ≤ IntermediateField.restrictScalars F (algebraicClosure E K)
-- Mathlib.CategoryTheory.Sites.SheafCohomology.Basic
CategoryTheory.Adjunction.homAddEquiv.congr_simp : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Preadditive D] {F : CategoryTheory.Functor C D}
  {G : CategoryTheory.Functor D C} (adj adj_1 : F ⊣ G),
  adj = adj_1 → ∀ [inst_4 : F.Additive] (X : C) (Y : D), adj.homAddEquiv X Y = adj_1.homAddEquiv X Y
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.card_zero : ∀ {α : Type u_2} [inst : Zero α], Finset.card 0 = 1
-- Std.Data.DTreeMap.Raw.Basic
/-- Given a proof that a mapping for the given key is present, retrieves the mapping for the given key.

Uses the `LawfulEqCmp` instance to cast the retrieved value to the correct type.
 -/
Std.DTreeMap.Raw.Const.get : {α : Type u} → {cmp : α → α → Ordering} → {β : Type v} → (t : Std.DTreeMap.Raw α (fun x => β) cmp) → (a : α) → a ∈ t → β
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Tactic.ComputeAsymptotics.Seq.FriendlyOperation.id : ∀ {α : Type u_1}, Tactic.ComputeAsymptotics.Seq.FriendlyOperation id
-- Mathlib.Algebra.Algebra.Subalgebra.MulOpposite
Subalgebra.linearEquivOp_symm_apply_coe : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  (S : Subalgebra R A) (a : ↥S.op), ↑(S.linearEquivOp.symm a) = MulOpposite.unop ↑a
-- Mathlib.GroupTheory.Nilpotent
/-- The nilpotency class of a nilpotent `G` is equal to the length of the lower central series.  -/
Subgroup.lowerCentralSeries_length_eq_nilpotencyClass : ∀ {G : Type u_1} [inst : Group G] [hG : Group.IsNilpotent G], Nat.find ⋯ = Group.nilpotencyClass G
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.prod_uniformContinuous_toLp : ∀ (p : ENNReal) (α : Type u_2) (β : Type u_3) [inst : UniformSpace α] [inst_1 : UniformSpace β],
  UniformContinuous (WithLp.toLp p)
-- Init.Data.Array.Monadic
Array.forIn'_map : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} {γ : Type u_1} {init : γ} [inst : Monad m] [LawfulMonad m]
  {xs : Array α} (g : α → β) (f : (b : β) → b ∈ Array.map g xs → γ → m (ForInStep γ)),
  forIn' (Array.map g xs) init f = forIn' xs init fun a h y => f (g a) ⋯ y
-- Mathlib.Topology.Filter
Filter.mem_nhds_iff' : ∀ {α : Type u_2} {l : Filter α} {S : Set (Filter α)}, S ∈ nhds l ↔ ∃ t ∈ l, ∀ ⦃l' : Filter α⦄, t ∈ l' → l' ∈ S
-- Mathlib.Algebra.Algebra.Spectrum.Basic
spectrum.singleton_sub_eq : ∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] (a : A) (r : R),
  {r} - spectrum R a = spectrum R ((algebraMap R A) r - a)
-- Lean.Meta.Basic
_private.Lean.Meta.Basic.0.Lean.Meta.RealizeConstantResult.snap? : Lean.Meta.RealizeConstantResult✝ → Option Lean.Language.SnapshotTree
-- Mathlib.Algebra.Lie.Free
FreeLieAlgebra.hom_ext_iff : ∀ {R : Type u} {X : Type v} [inst : CommRing R] {L : Type w} [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  {F₁ F₂ : FreeLieAlgebra R X →ₗ⁅R⁆ L}, F₁ = F₂ ↔ ∀ (x : X), F₁ (FreeLieAlgebra.of R x) = F₂ (FreeLieAlgebra.of R x)
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.Tactic.Cases.and_2 : ∀ {σs : List (Type u_1)} {Q H₁' H₂ T : Std.Do.SPred σs}, ((Q ∧ H₁') ∧ H₂ ⊢ₛ T) → (Q ∧ H₂) ∧ H₁' ⊢ₛ T
-- Init.Coe
subtypeCoe : {α : Sort u} → {p : α → Prop} → CoeOut (Subtype p) α
-- Mathlib.CategoryTheory.Triangulated.TStructure.Induced
CategoryTheory.Triangulated.TStructure.instHasInducedTStructureMinus : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) [CategoryTheory.IsTriangulated C], t.minus.HasInducedTStructure t
-- Init.Data.UInt.Lemmas
UInt32.toNat_toUInt8 : ∀ (x : UInt32), x.toUInt8.toNat = x.toNat % 2 ^ 8
-- Init.SizeOfLemmas
USize.sizeOf : ∀ (a : USize), sizeOf a = a.toNat + 3
-- Mathlib.Analysis.Normed.Unbundled.RingSeminorm
MulRingNorm.toMulRingSeminorm : {R : Type u_2} → [inst : NonAssocRing R] → MulRingNorm R → MulRingSeminorm R
-- Mathlib.Data.Prod.PProd
PProd.exists' : ∀ {α : Sort u_1} {β : Sort u_2} {p : α → β → Prop}, (∃ x, p x.fst x.snd) ↔ ∃ a b, p a b
-- Mathlib.GroupTheory.GroupAction.Blocks
AddAction.isBlock_iff_vadd_eq_vadd_or_disjoint : ∀ {G : Type u_1} {X : Type u_2} [inst : VAdd G X] {B : Set X},
  AddAction.IsBlock G B ↔ ∀ (g₁ g₂ : G), g₁ +ᵥ B = g₂ +ᵥ B ∨ Disjoint (g₁ +ᵥ B) (g₂ +ᵥ B)
-- Std.Sat.AIG.RelabelNat
_private.Std.Sat.AIG.RelabelNat.0.Std.Sat.AIG.relabelNat'.match_1.eq_1 : ∀ (motive : Option ℕ → Sort u_1) (var : ℕ) (h_1 : (var : ℕ) → motive (some var)) (h_2 : Unit → motive none),
  (match some var with
    | some var => h_1 var
    | none => h_2 ()) =
    h_1 var
-- Mathlib.LinearAlgebra.PerfectPairing.Restrict
_private.Mathlib.LinearAlgebra.PerfectPairing.Restrict.0.LinearMap.restrictScalars_surjective_aux : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] (p : M →ₗ[R] N →ₗ[R] R) [inst_5 : p.IsPerfPair] {S : Type u_4}
  {M' : Type u_5} {N' : Type u_6} [inst_6 : CommRing S] [inst_7 : IsDomain S] [inst_8 : Algebra S R]
  [inst_9 : Module S M] [inst_10 : Module S N] [inst_11 : IsScalarTower S R M] [inst_12 : IsScalarTower S R N]
  [inst_13 : Module.IsTorsionFree S R] [inst_14 : Nontrivial R] [inst_15 : AddCommGroup M'] [inst_16 : Module S M']
  [inst_17 : AddCommGroup N'] [inst_18 : Module S N'] (i : M' →ₗ[S] M) (j : N' →ₗ[S] N),
  (∀ (g : Module.Dual S N'), ∃ m, ↑S (p.toPerfPair (i m)) ∘ₗ j = Algebra.linearMap S R ∘ₗ g) →
    ∀ (hp : ∀ (m : M') (n : N'), (p (i m)) (j n) ∈ (algebraMap S R).range),
      Function.Surjective ⇑(i.restrictScalarsRange₂ j (Algebra.linearMap S R) ⋯ p hp)
-- Mathlib.NumberTheory.Padics.PadicNumbers
instSubPadic : (p : ℕ) → [inst : Fact (Nat.Prime p)] → Sub ℚ_[p]
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.WalkingParallelPairHom.assoc : ∀ {X Y Z W : CategoryTheory.Limits.WalkingParallelPair} (f : CategoryTheory.Limits.WalkingParallelPairHom X Y)
  (g : CategoryTheory.Limits.WalkingParallelPairHom Y Z) (h : CategoryTheory.Limits.WalkingParallelPairHom Z W),
  (f.comp g).comp h = f.comp (g.comp h)
-- Std.Http.Data.URI.Encoding
Std.Http.URI.EncodedQueryString.instInhabited : {r : UInt8 → Bool} → Inhabited (Std.Http.URI.EncodedQueryString r)
-- Mathlib.RingTheory.Valuation.Basic
Valuation.IsEquiv.valueGroup₀Fun_spec : ∀ {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [inst : LinearOrderedCommGroupWithZero Γ₀]
  [inst_1 : LinearOrderedCommGroupWithZero Γ'₀] [inst_2 : Ring R] {v : Valuation R Γ₀} {w : Valuation R Γ'₀}
  (h : v.IsEquiv w) {r s : R} (hr : (MonoidWithZeroHom.ofClass v) r ≠ 0) (hs : (MonoidWithZeroHom.ofClass v) s ≠ 0)
  (hr' : optParam ((MonoidWithZeroHom.ofClass w) r ≠ 0) ⋯) (hs' : optParam ((MonoidWithZeroHom.ofClass w) s ≠ 0) ⋯),
  h.valueGroup₀Fun ↑(MonoidWithZeroHom.valueGroup.mk (MonoidWithZeroHom.ofClass v) r s hr hs) =
    ↑(MonoidWithZeroHom.valueGroup.mk (MonoidWithZeroHom.ofClass w) r s hr' hs')
-- Mathlib.GroupTheory.GroupExtension.Defs
/-- The inclusion map is injective.  -/
GroupExtension.inl_injective : ∀ {N : Type u_1} {E : Type u_2} {G : Type u_3} [inst : Group N] [inst_1 : Group E] [inst_2 : Group G]
  (self : GroupExtension N E G), Function.Injective ⇑self.inl
-- Mathlib.Topology.Category.DeltaGenerated
/-- The category of delta-generated topological spaces.  -/
DeltaGenerated : Type (u + 1)
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.rpow_le_rpow_iff_of_neg : ∀ {x y z : ℝ}, 0 < x → 0 < y → z < 0 → (x ^ z ≤ y ^ z ↔ y ≤ x)
-- Mathlib.CategoryTheory.Monoidal.Action.End
CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionOfMonoidalFunctorToEndofunctorMop_actionObj : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  (F : CategoryTheory.Functor C (CategoryTheory.Functor D D)ᴹᵒᵖ) [inst_3 : F.Monoidal] (c : C) (d : D),
  CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj c d = (F.obj c).unmop.obj d
-- Mathlib.Algebra.Order.Hom.MonoidWithZero
OrderMonoidWithZeroHom.mk_coe : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : MulZeroOneClass α]
  [inst_3 : MulZeroOneClass β] (f : α →*₀o β) (h : Monotone (↑(MonoidWithZeroHom.ofClass f)).toFun),
  { toMonoidWithZeroHom := MonoidWithZeroHom.ofClass f, monotone' := h } = f
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.Atom₁.mk.injEq : ∀ (e : Lean.Expr) (src tgt : Mathlib.Tactic.BicategoryLike.Obj) (e_1 : Lean.Expr)
  (src_1 tgt_1 : Mathlib.Tactic.BicategoryLike.Obj),
  ({ e := e, src := src, tgt := tgt } = { e := e_1, src := src_1, tgt := tgt_1 }) =
    (e = e_1 ∧ src = src_1 ∧ tgt = tgt_1)
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rco.nodup_toList : ∀ {α : Type u} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.Rxo.IsAlwaysFinite α] [inst_4 : Std.PRange.LawfulUpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerableLT α] {a b : α}, (a...b).toList.Nodup
-- Mathlib.CategoryTheory.Comma.Final
/-- `Comma L R` with `L : A ⥤ T` and `R : B ⥤ T` is connected if `R` is final and `A` is
connected.  -/
CategoryTheory.Comma.isConnected_comma_of_final : ∀ {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] (L : CategoryTheory.Functor A T)
  (R : CategoryTheory.Functor B T) [CategoryTheory.IsConnected A] [R.Final],
  CategoryTheory.IsConnected (CategoryTheory.Comma L R)
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.lineMap.eq_1 : ∀ {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V1] [inst_2 : Module k V1]
  [inst_3 : AddTorsor V1 P1] (p₀ p₁ : P1),
  AffineMap.lineMap p₀ p₁ = (LinearMap.id.smulRight (p₁ -ᵥ p₀)).toAffineMap +ᵥ AffineMap.const k k p₀
-- Mathlib.Order.Interval.Set.SurjOn
surjOn_Ioi_of_monotone_surjective : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : PartialOrder β] {f : α → β},
  Monotone f → Function.Surjective f → ∀ (a : α), Set.SurjOn f (Set.Ioi a) (Set.Ioi (f a))
-- Mathlib.Algebra.Module.Submodule.Defs
Submodule.coe_toAddSubmonoid : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (p : Submodule R M),
  ↑p.toAddSubmonoid = ↑p
-- Mathlib.Algebra.Order.Pi
Function.one_lt_const : ∀ {α : Type u_2} {β : Type u_3} [inst : One α] [inst_1 : Preorder α] {a : α} [Nonempty β],
  1 < Function.const β a ↔ 1 < a
-- Mathlib.Topology.Algebra.ContinuousAffineMap
ContinuousAffineMap.prodMap_toAffineMap : ∀ {k : Type u_10} {P₁ : Type u_11} {P₂ : Type u_12} {P₃ : Type u_13} {P₄ : Type u_14} {V₁ : Type u_15} {V₂ : Type u_16}
  {V₃ : Type u_17} {V₄ : Type u_18} [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁]
  [inst_3 : AddTorsor V₁ P₁] [inst_4 : TopologicalSpace P₁] [inst_5 : AddCommGroup V₂] [inst_6 : Module k V₂]
  [inst_7 : AddTorsor V₂ P₂] [inst_8 : TopologicalSpace P₂] [inst_9 : AddCommGroup V₃] [inst_10 : Module k V₃]
  [inst_11 : AddTorsor V₃ P₃] [inst_12 : TopologicalSpace P₃] [inst_13 : AddCommGroup V₄] [inst_14 : Module k V₄]
  [inst_15 : AddTorsor V₄ P₄] [inst_16 : TopologicalSpace P₄] (f : P₁ →ᴬ[k] P₂) (g : P₃ →ᴬ[k] P₄),
  ↑(f.prodMap g) = (↑f).prodMap ↑g
-- Mathlib.Topology.Continuous
Continuous.continuousAt : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y} {x : X},
  Continuous f → ContinuousAt f x
-- Mathlib.Analysis.Convex.Join
convexJoin_mono_right : ∀ {𝕜 : Type u_2} {E : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : Module 𝕜 E] {s t₁ t₂ : Set E}, t₁ ⊆ t₂ → convexJoin 𝕜 s t₁ ⊆ convexJoin 𝕜 s t₂
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.getEntryGE!_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited ((a : α) × β a)] {k : α}, t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.getEntryGE! k = t₂.getEntryGE! k
-- Mathlib.MeasureTheory.Measure.MeasureSpace
/-- **Alias** of `MeasureTheory.measure_sdiff_eq_top`. -/
MeasureTheory.measure_diff_eq_top : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α}, μ s = ⊤ → μ t ≠ ⊤ → μ (s \ t) = ⊤
-- Init.Data.Dyadic.Inv
/-- For a positive dyadic `x`, `invAtPrec x prec * x ≤ 1`.  -/
Dyadic.invAtPrec_mul_le_one : ∀ {x : Dyadic}, 0 < x → ∀ (prec : ℤ), x.invAtPrec prec * x ≤ 1
-- Mathlib.NumberTheory.NumberField.Completion.FinitePlace
/-- **Alias** of `NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv`.

---

The `v`-adic absolute value is nonarchimedean  -/
NumberField.HeightOneSpectrum.NumberField.RingOfIntegers.HeightOneSpectrum.isNonarchimedean_adicAbv : ∀ (K : Type u_1) [inst : Field K] {R : Type u_2} [inst_1 : CommRing R] [inst_2 : Algebra R K]
  [inst_3 : IsDedekindDomain R] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R)
  [inst_5 : Module.Finite ℤ R] [inst_6 : Module.Free ℤ R], IsNonarchimedean ⇑(NumberField.HeightOneSpectrum.adicAbv K v)
-- Mathlib.Analysis.Calculus.TangentCone.Defs
/-- If `y` belongs to the tangent cone of `s` at `x`, then there exist

- an index type `α` and a nontrivial filter `l` on `α`;
- a family of scalars `c n`, `n : α`, and a family of vectors `d n`, `n : α` such that
- `d n → 0` along `l`;
- `x + d n ∈ s` eventually along `l`;
- `c n • d n → y` along `l`.

In fact, one can take `α = R × E`, `c = Prod.fst`, and `d = Prod.snd`, but this is not important,
so the lemma statement hides these details.

This lemma provides a convenient way to unfold the definition of `tangentConeAt`.  -/
exists_fun_of_mem_tangentConeAt : ∀ {R : Type u} {E : Type v} [inst : AddCommGroup E] [inst_1 : SMul R E] [inst_2 : TopologicalSpace E] {s : Set E}
  {x y : E},
  y ∈ tangentConeAt R s x →
    ∃ α l,
      ∃ (_ : l.NeBot),
        ∃ c d,
          Filter.Tendsto d l (nhds 0) ∧ (∀ᶠ (n : α) in l, x + d n ∈ s) ∧ Filter.Tendsto (fun n => c n • d n) l (nhds y)
-- Mathlib.Order.Filter.Map
Filter.frequently_comap : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {l : Filter β} {p : α → Prop},
  (∃ᶠ (a : α) in Filter.comap f l, p a) ↔ ∃ᶠ (b : β) in l, ∃ a, f a = b ∧ p a
-- Mathlib.Algebra.BigOperators.Finprod
finprod_eq_prod_of_mulSupport_toFinset_subset : ∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] (f : α → M) (hf : Function.HasFiniteMulSupport f) {s : Finset α},
  Set.Finite.toFinset hf ⊆ s → ∏ᶠ (i : α), f i = ∏ i ∈ s, f i
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.sub_nonempty : ∀ {α : Type u_2} [inst : Sub α] {s t : Set α}, (s - t).Nonempty ↔ s.Nonempty ∧ t.Nonempty
-- Lean.Meta.Tactic.Simp.LoopProtection
Lean.Meta.Simp.withFreshUsedTheorems : {α : Type} → Lean.Meta.SimpM α → Lean.Meta.SimpM α
-- Mathlib.RingTheory.MvPowerSeries.Trunc
MvPowerSeries.coeff_mul_eq_coeff_trunc'_mul_trunc' : ∀ {σ : Type u_1} {R : Type u_2} [inst : DecidableEq σ] [inst_1 : CommSemiring R] (n : σ →₀ ℕ) (f g : MvPowerSeries σ R)
  {m : σ →₀ ℕ},
  m ≤ n →
    (MvPowerSeries.coeff m) (f * g) = MvPolynomial.coeff m ((MvPowerSeries.trunc' R n) f * (MvPowerSeries.trunc' R n) g)
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
ProjectiveSpectrum.zeroLocus_bUnion : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubmonoidClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] (s : Set (Set A)),
  ProjectiveSpectrum.zeroLocus 𝒜 (⋃ s' ∈ s, s') = ⋂ s' ∈ s, ProjectiveSpectrum.zeroLocus 𝒜 s'
-- Lean.Compiler.ExternAttr
_private.Lean.Compiler.ExternAttr.0.Lean.parseOptNum : (pattern : String.Slice) → pattern.Pos → ℕ → pattern.Pos × ℕ
-- Mathlib.Geometry.Euclidean.Projection
/-- `p` is equidistant from two points in `s` if and only if its
`orthogonalProjection` is.  -/
EuclideanGeometry.dist_eq_iff_dist_orthogonalProjection_eq : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup V]
  [inst_2 : InnerProductSpace 𝕜 V] [inst_3 : MetricSpace P] [inst_4 : NormedAddTorsor V P] {s : AffineSubspace 𝕜 P}
  [inst_5 : Nonempty ↥s] [inst_6 : s.direction.HasOrthogonalProjection] {p₁ p₂ : P} (p₃ : P),
  p₁ ∈ s →
    p₂ ∈ s →
      (dist p₁ p₃ = dist p₂ p₃ ↔
        dist p₁ ↑((EuclideanGeometry.orthogonalProjection s) p₃) =
          dist p₂ ↑((EuclideanGeometry.orthogonalProjection s) p₃))
-- Mathlib.Data.Set.Function
Set.BijOn.subset_range : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β}, Set.BijOn f s t → t ⊆ Set.range f
-- Mathlib.SetTheory.Descriptive.Tree
Descriptive.Tree.mem_pullSub_long : ∀ {A : Type u_1} {T : ↥(Descriptive.tree A)} {x y : List A},
  x.length ≤ y.length → (y ∈ Descriptive.Tree.pullSub T x ↔ ∃ z ∈ T, y = x ++ z)
-- Lean.MetavarContext
Lean.instInhabitedLevelMetavarDecl : Inhabited Lean.LevelMetavarDecl
-- Mathlib.Algebra.Group.Equiv.Defs
MulEquiv.ofBijective.eq_1 : ∀ {M : Type u_9} {N : Type u_10} {F : Type u_11} [inst : Mul M] [inst_1 : Mul N] [inst_2 : FunLike F M N]
  [inst_3 : MulHomClass F M N] (f : F) (hf : Function.Bijective ⇑f),
  MulEquiv.ofBijective f hf = { toEquiv := Equiv.ofBijective (⇑f) hf, map_mul' := ⋯ }
-- Mathlib.Topology.NoetherianSpace
TopologicalSpace.NoetherianSpace.eq_1 : ∀ (α : Type u_1) [inst : TopologicalSpace α],
  TopologicalSpace.NoetherianSpace α = WellFoundedGT (TopologicalSpace.Opens α)
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.IsComonHom.hom_counit_assoc : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C} {M N : C}
  {inst_2 : CategoryTheory.ComonObj M} {inst_3 : CategoryTheory.ComonObj N} (f : M ⟶ N)
  [self : CategoryTheory.IsComonHom f] {Z : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ Z),
  CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp CategoryTheory.ComonObj.counit h) =
    CategoryTheory.CategoryStruct.comp CategoryTheory.ComonObj.counit h