mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rio.toList_eq_toList_rco : ∀ {α : Type u} {r : Std.Rio α} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.Least? α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerableLT α] [inst_6 : Std.PRange.LawfulUpwardEnumerableLeast? α]
  [inst_7 : Std.Rxo.IsAlwaysFinite α], r.toList = (Std.PRange.UpwardEnumerable.least...r.upper).toList
-- Init.Data.SInt.Bitwise
Int64.zero_shiftLeft : ∀ {a : Int64}, 0 <<< a = 0
-- Mathlib.CategoryTheory.Presentable.OrthogonalReflection
CategoryTheory.OrthogonalReflection.D₂.condition_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W : CategoryTheory.MorphismProperty C} {Z : C}
  [inst_1 : CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₁]
  [inst_2 : CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₂]
  [inst_3 : CategoryTheory.Limits.HasPushouts C]
  [inst_4 : CategoryTheory.Limits.HasMulticoequalizer (CategoryTheory.OrthogonalReflection.D₂.multispanIndex W Z)]
  {X Y : C} (f : X ⟶ Y),
  W f →
    ∀ {g₁ g₂ : Y ⟶ CategoryTheory.OrthogonalReflection.step W Z},
      CategoryTheory.CategoryStruct.comp f g₁ = CategoryTheory.CategoryStruct.comp f g₂ →
        ∀ {Z_1 : C} (h : CategoryTheory.OrthogonalReflection.succ W Z ⟶ Z_1),
          CategoryTheory.CategoryStruct.comp g₁
              (CategoryTheory.CategoryStruct.comp (CategoryTheory.OrthogonalReflection.fromStep W Z) h) =
            CategoryTheory.CategoryStruct.comp g₂
              (CategoryTheory.CategoryStruct.comp (CategoryTheory.OrthogonalReflection.fromStep W Z) h)
-- Mathlib.Order.UpperLower.Relative
IsRelLowerSet.iInter : ∀ {α : Type u_1} {ι : Sort u_2} {P : α → Prop} [inst : LE α] [Nonempty ι] {f : ι → Set α},
  (∀ (i : ι), IsRelLowerSet (f i) P) → IsRelLowerSet (⋂ i, f i) P
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.GrindTactic : Type
-- Mathlib.Data.DFinsupp.Order
DFinsupp.lattice : {ι : Type u_1} →
  {α : ι → Type u_2} → [inst : (i : ι) → Zero (α i)] → [(i : ι) → Lattice (α i)] → Lattice (Π₀ (i : ι), α i)
-- Mathlib.Data.Finset.Sups
Finset.infs_comm : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SemilatticeInf α] (s t : Finset α), s ⊼ t = t ⊼ s
-- Mathlib.Order.Filter.Prod
Filter.prod_inf_prod : ∀ {α : Type u_1} {β : Type u_2} {f₁ f₂ : Filter α} {g₁ g₂ : Filter β}, f₁ ×ˢ g₁ ⊓ f₂ ×ˢ g₂ = (f₁ ⊓ f₂) ×ˢ (g₁ ⊓ g₂)
-- Lean.Meta.Tactic.Cases
Lean.Meta.Cases.cases : Lean.MVarId →
  Lean.FVarId →
    optParam (Array Lean.Meta.AltVarNames) #[] →
      optParam Bool false → optParam (Option (Array Lean.Name)) none → Lean.MetaM (Array Lean.Meta.CasesSubgoal)
-- Mathlib.Geometry.Diffeology.Basic
Diffeology.isPlot_reparam : ∀ {X : Type u_1} [inst : DiffeologicalSpace X] {n m : ℕ} {p : EuclideanSpace ℝ (Fin m) → X}
  {f : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin m)},
  Diffeology.IsPlot p → ContDiff ℝ (↑⊤) f → Diffeology.IsPlot (p ∘ f)
-- Std.Tactic.Do.Syntax
Lean.Parser.Tactic.«mrefinePat□_» : Lean.ParserDescr
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.X_pow_mul : ∀ {R : Type u_1} [inst : Semiring R] {φ : PowerSeries R} {n : ℕ}, PowerSeries.X ^ n * φ = φ * PowerSeries.X ^ n
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgEquiv.symm_mk : ∀ {R : Type u_2} {A : Type u_3} {B : Type u_4} [inst : Add A] [inst_1 : Add B] [inst_2 : Mul A] [inst_3 : Mul B]
  [inst_4 : SMul R A] [inst_5 : SMul R B] [inst_6 : Star A] [inst_7 : Star B] (e : A ≃⋆+* B)
  (h₁ : ∀ (r : R) (a : A), e.toFun (r • a) = r • e.toFun a),
  { toStarRingEquiv := e, map_smul' := h₁ }.symm = { toStarRingEquiv := e.symm, map_smul' := ⋯ }
-- Lean.Elab.PatternVar
Lean.Elab.Term.CollectPatternVars.Context.namedArgs : Lean.Elab.Term.CollectPatternVars.Context → Array Lean.Elab.Term.NamedArg
-- Mathlib.Topology.ContinuousMap.ContinuousMapZero
ContinuousMapZero.coe_add : ∀ {X : Type u_1} {R : Type u_2} [inst : Zero X] [inst_1 : TopologicalSpace X] [inst_2 : TopologicalSpace R]
  [inst_3 : AddZeroClass R] [inst_4 : ContinuousAdd R] (f g : ContinuousMapZero X R), ⇑(f + g) = ⇑f + ⇑g
-- Mathlib.CategoryTheory.Limits.Types.Limits
CategoryTheory.Limits.Types.isLimitEquivSections_symm_apply : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] {F : CategoryTheory.Functor J (Type u)}
  {c : CategoryTheory.Limits.Cone F} (t : CategoryTheory.Limits.IsLimit c) (x : ↑F.sections) (j : J),
  (CategoryTheory.ConcreteCategory.hom (c.π.app j)) ((CategoryTheory.Limits.Types.isLimitEquivSections t).symm x) = ↑x j
-- Mathlib.Topology.Category.DeltaGenerated
/-- Constructor for objects of the category `DeltaGenerated`  -/
DeltaGenerated.of : (X : Type u) → [inst : TopologicalSpace X] → [DeltaGeneratedSpace X] → DeltaGenerated
-- Mathlib.Topology.Order.OrderClosed
bddBelow_closure : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : Preorder α] [ClosedIciTopology α] {s : Set α},
  BddBelow (closure s) ↔ BddBelow s
-- Init.Data.List.TakeDrop
Option.toList.eq_2 : ∀ {α : Type u_1} (val : α), (some val).toList = [val]
-- Mathlib.Order.RelIso.Basic
RelEmbedding.injective : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ↪r s), Function.Injective ⇑f
-- Mathlib.Dynamics.TopologicalEntropy.Semiconj
Dynamics.IsDynCoverOf.image : ∀ {X : Type u_1} {Y : Type u_2} {s F : Set X} {V : SetRel Y Y} {S : X → X} {T : Y → Y} {φ : X → Y} {n : ℕ},
  Function.Semiconj φ S T →
    Dynamics.IsDynCoverOf S F (Prod.map φ φ ⁻¹' V) n s → Dynamics.IsDynCoverOf T (φ '' F) V n (φ '' s)
-- Init.Data.String.Lemmas.FindPos
String.posLT.congr_simp : ∀ (s : String) (offset offset_1 : String.Pos.Raw) (e_offset : offset = offset_1) (h : 0 < offset),
  s.posLT offset h = s.posLT offset_1 ⋯
-- Batteries.Data.Float.Basic
/-- Divide two integers, to produce a correctly rounded (nearest-ties-to-even) `Float` result.
 -/
Int.divFloat : ℤ → ℤ → Float
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.getKey?_modify_self : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp}
  {k : α} {f : β → β}, (Std.ExtDTreeMap.Const.modify t k f).getKey? k = if k ∈ t then some k else none
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
/-- If `u₁` and `u₂` are two uniform structures on `γ` and `u₁ ≤ u₂`, then
`𝒰(α, γ, u₁) ≤ 𝒰(α, γ, u₂)`.  -/
UniformFun.mono : ∀ {α : Type u_1} {γ : Type u_3}, Monotone (@UniformFun.uniformSpace α γ)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonCompletionItem.fromJson : Lean.Json → Except String Lean.Lsp.CompletionItem
-- Mathlib.Algebra.Lie.Basic
/-- A tower of Lie bracket actions encapsulates the Leibniz rule for Lie bracket actions.

More precisely, it does so in a relative setting:
Let `L₁` and `L₂` be two types with Lie bracket actions on a type `M` endowed with an addition,
and additionally assume a Lie bracket action of `L₁` on `L₂`.
Then the Leibniz rule asserts for all `x : L₁`, `y : L₂`, and `m : M` that
`⁅x, ⁅y, m⁆⁆ = ⁅⁅x, y⁆, m⁆ + ⁅y, ⁅x, m⁆⁆` holds.

Common examples include the case where `L₁` is a Lie subalgebra of `L₂`
and the case where `L₂` is a Lie ideal of `L₁`.  -/
IsLieTower : (L₁ : Type u_1) → (L₂ : Type u_2) → (M : Type u_3) → [Bracket L₁ L₂] → [Bracket L₁ M] → [Bracket L₂ M] → [Add M] → Prop
-- Mathlib.Order.SuccPred.Basic
Order.Icc_pred_right_of_not_isMin : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : PredOrder α] {a b : α}, ¬IsMin a → Set.Icc b (Order.pred a) = Set.Ico b a
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits
/-- The projection from `P` to the quotient by an open normal subgroup.  -/
ProfiniteGrp.proj : {P : ProfiniteGrp.{u}} → (U : OpenNormalSubgroup ↑P.toProfinite.toTop) → P ⟶ P.diagram.obj U
-- Mathlib.LinearAlgebra.AffineSpace.Ordered
/-- Given `c = lineMap a b r`, `a < c < b`, the point `(c, f c)` is non-strictly below the
segment `[(a, f a), (b, f b)]` if and only if `slope f a c ≤ slope f c b`.  -/
map_le_lineMap_iff_slope_le_slope : ∀ {k : Type u_1} {E : Type u_2} [inst : Field k] [inst_1 : LinearOrder k] [IsStrictOrderedRing k]
  [inst_3 : AddCommGroup E] [inst_4 : PartialOrder E] [IsOrderedAddMonoid E] [inst_6 : Module k E]
  [IsStrictOrderedModule k E] [PosSMulReflectLE k E] {f : k → E} {a b r : k},
  a < b →
    0 < r →
      r < 1 →
        (f ((AffineMap.lineMap a b) r) ≤ (AffineMap.lineMap (f a) (f b)) r ↔
          slope f a ((AffineMap.lineMap a b) r) ≤ slope f ((AffineMap.lineMap a b) r) b)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.isSome_minKey?_of_contains : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k : α}, t.contains k = true → t.minKey?.isSome = true
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.isEmpty_eq_false_iff_exists_contains_eq_true : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp],
  t.isEmpty = false ↔ ∃ a, t.contains a = true
-- Mathlib.Order.RelClasses
/-- The value from `WellFoundedLT.fix` is built from the previous ones as specified.  -/
WellFoundedLT.fix_eq : ∀ {α : Type u} [inst : LT α] [inst_1 : WellFoundedLT α] {motive : α → Sort u_1}
  (ind : (x : α) → ((y : α) → y < x → motive y) → motive x) (x : α),
  WellFoundedLT.fix ind x = ind x fun y x => WellFoundedLT.fix ind y
-- Mathlib.Data.List.OfFn
List.ofFn_const : ∀ {α : Type u} (n : ℕ) (c : α), (List.ofFn fun x => c) = List.replicate n c
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.restrictScalars_apply : ∀ (R : Type u_1) {S : Type u_5} {M : Type u_8} {M₂ : Type u_10} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R M₂]
  [inst_6 : Module S M] [inst_7 : Module S M₂] [inst_8 : LinearMap.CompatibleSMul M M₂ R S] (fₗ : M →ₗ[S] M₂) (x : M),
  (↑R fₗ) x = fₗ x
-- Mathlib.CategoryTheory.Galois.Basic
/-- The cardinality of the fiber of a coproduct is the sum of the cardinalities of the fibers.  -/
CategoryTheory.PreGaloisCategory.card_fiber_coprod_eq_sum : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat)
  [inst_1 : CategoryTheory.PreGaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F] (X Y : C),
  Nat.card (F.obj (X ⨿ Y)).obj = Nat.card (F.obj X).obj + Nat.card (F.obj Y).obj
-- Mathlib.Topology.MetricSpace.UniformConvergence
UniformOnFun.lipschitzWith_one_ofFun_toFun : ∀ {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [inst : PseudoEMetricSpace β] [inst_1 : Finite ↑𝔖],
  LipschitzWith 1 (⇑(UniformOnFun.ofFun 𝔖) ∘ ⇑UniformFun.toFun)
-- Mathlib.NumberTheory.Chebyshev
Chebyshev.psi_nonneg : ∀ (x : ℝ), 0 ≤ Chebyshev.psi x
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
MeasureTheory.isComplete_aestronglyMeasurable : ∀ {α : Type u_1} {F : Type u_2} {p : ENNReal} [inst : NormedAddCommGroup F] {m m0 : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} [hp : Fact (1 ≤ p)] [CompleteSpace F],
  m ≤ m0 → IsComplete {f | MeasureTheory.AEStronglyMeasurable (↑↑f) μ}
-- Mathlib.AlgebraicTopology.SimplicialSet.Basic
SSet.hom_ext_iff : ∀ {X Y : SSet} {f g : X ⟶ Y}, f = g ↔ ∀ (n : SimplexCategoryᵒᵖ), f.app n = g.app n
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithInitial.lift_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  {Z : D} (F : CategoryTheory.Functor C D) (M : (x : C) → Z ⟶ F.obj x)
  (hM : ∀ (x y : C) (f : x ⟶ y), CategoryTheory.CategoryStruct.comp (M x) (F.map f) = M y)
  (X : CategoryTheory.WithInitial C),
  (CategoryTheory.WithInitial.lift F M hM).obj X =
    match X with
    | CategoryTheory.WithInitial.of x => F.obj x
    | CategoryTheory.WithInitial.star => Z
-- Init.Data.List.Sublist
List.nil_prefix : ∀ {α : Type u_1} {l : List α}, [] <+: l
-- Mathlib.GroupTheory.GroupAction.Basic
Finite.finite_addAction_orbit : ∀ {M : Type u} [inst : AddMonoid M] {α : Type v} [inst_1 : AddAction M α] [Finite M] (a : α),
  (AddAction.orbit M a).Finite
-- Mathlib.Data.Finset.Lattice.Fold
Finset.subset_range_sup_succ : ∀ (s : Finset ℕ), s ⊆ Finset.range (s.sup id).succ
-- Mathlib.LinearAlgebra.AffineSpace.Ordered
/-- Given `c = lineMap a b r`, `c < b`, the point `(c, f c)` is strictly below the
segment `[(a, f a), (b, f b)]` if and only if `slope f a b < slope f c b`.  -/
map_lt_lineMap_iff_slope_lt_slope_right : ∀ {k : Type u_1} {E : Type u_2} [inst : Field k] [inst_1 : LinearOrder k] [inst_2 : AddCommGroup E]
  [inst_3 : PartialOrder E] [IsOrderedAddMonoid E] [inst_5 : Module k E] [IsStrictOrderedModule k E]
  [PosSMulReflectLE k E] {f : k → E} {a b r : k},
  0 < (1 - r) * (b - a) →
    (f ((AffineMap.lineMap a b) r) < (AffineMap.lineMap (f a) (f b)) r ↔
      slope f a b < slope f ((AffineMap.lineMap a b) r) b)
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.kernelFactorThruImage_inv_comp_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  (f : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasKernel f] [inst_3 : CategoryTheory.Limits.HasImage f]
  [inst_4 : CategoryTheory.Limits.HasKernel (CategoryTheory.Limits.factorThruImage f)],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelFactorThruImage f).inv
      (CategoryTheory.Limits.kernel.ι (CategoryTheory.Limits.factorThruImage f)) =
    CategoryTheory.Limits.kernel.ι f
-- Mathlib.Analysis.Normed.Group.Real
Real.nnnorm_nnratCast : ∀ (q : ℚ≥0), ‖↑q‖₊ = ↑q
-- Mathlib.Analysis.Complex.Trigonometric
Real.exp_sub_sinh : ∀ (x : ℝ), Real.exp x - Real.sinh x = Real.cosh x
-- Lean.Elab.Tactic.Simp
Lean.Elab.Tactic.ElabSimpArgResult.eraseSimproc.inj : ∀ {toErase toErase_1 : Lean.Name},
  Lean.Elab.Tactic.ElabSimpArgResult.eraseSimproc toErase = Lean.Elab.Tactic.ElabSimpArgResult.eraseSimproc toErase_1 →
    toErase = toErase_1
-- Mathlib.MeasureTheory.Integral.Bochner.Set
Topology.IsClosedEmbedding.setIntegral_map : ∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {μ : MeasureTheory.Measure X} [inst_2 : TopologicalSpace X] [BorelSpace X] {Y : Type u_5} [inst_4 : MeasurableSpace Y]
  [inst_5 : TopologicalSpace Y] [BorelSpace Y] {g : X → Y} {f : Y → E} (s : Set Y),
  Topology.IsClosedEmbedding g → ∫ (y : Y) in s, f y ∂MeasureTheory.Measure.map g μ = ∫ (x : X) in g ⁻¹' s, f (g x) ∂μ
-- Mathlib.Algebra.Algebra.Unitization
Unitization.fst_inr : ∀ (R : Type u_1) {A : Type u_2} [inst : Zero R] (a : A), (↑a).toProd.1 = 0
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
/-- **Integration by parts on (-∞, ∞).**
Version assuming that the total function is integrable  -/
MeasureTheory.integral_mul_deriv_eq_deriv_mul_of_integrable : ∀ {A : Type u_1} [inst : NormedRing A] [inst_1 : NormedAlgebra ℝ A] {u v u' v' : ℝ → A},
  (∀ x ∈ tsupport v, HasDerivAt u (u' x) x) →
    (∀ x ∈ tsupport u, HasDerivAt v (v' x) x) →
      MeasureTheory.Integrable (u * v') MeasureTheory.volume →
        MeasureTheory.Integrable (u' * v) MeasureTheory.volume →
          MeasureTheory.Integrable (u * v) MeasureTheory.volume → ∫ (x : ℝ), u x * v' x = -∫ (x : ℝ), u' x * v x
-- Mathlib.Order.Disjoint
Disjoint.out : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : OrderBot α] {a b : α}, Disjoint a b → ∀ x ≤ a, x ≤ b → x = ⊥
-- Mathlib.Algebra.Order.Ring.Unbundled.Rat
Rat.den_abs_eq_den : ∀ (q : ℚ), |q|.den = q.den
-- Mathlib.Topology.DiscreteQuotient
DiscreteQuotient.instInhabited : {X : Type u_2} → [inst : TopologicalSpace X] → Inhabited (DiscreteQuotient X)
-- Mathlib.Algebra.Polynomial.Derivative
Polynomial.derivative_neg : ∀ {R : Type u} [inst : Ring R] (f : Polynomial R), Polynomial.derivative (-f) = -Polynomial.derivative f
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
/-- A uniform additive group is an additive group in which addition and negation are
uniformly continuous.

`IsUniformAddGroup G` is equivalent to the fact that `G` is a topological additive group, and the
uniformity coincides with **both** the associated left and right uniformities
(see `IsUniformAddGroup.isRightUniformAddGroup`, `IsUniformAddGroup.isLeftUniformAddGroup` and
`IsUniformAddGroup.of_left_right`).

Since there are topological groups where these two uniformities do **not** coincide,
not all topological groups admit a uniform group structure in this sense. This is however the
case for commutative groups, which are the main motivation for the existence of this
typeclass.  -/
IsUniformAddGroup : (α : Type u_3) → [UniformSpace α] → [AddGroup α] → Prop
-- Mathlib.Order.Heyting.Regular
/-- The coercion `Regular α → α`  -/
Heyting.Regular.val : {α : Type u_1} → [inst : HeytingAlgebra α] → Heyting.Regular α → α
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.IdealSheafData.inf_mul : ∀ {X : AlgebraicGeometry.Scheme} (I J K : X.IdealSheafData), (I ⊔ J) * K = I * K ⊔ J * K
-- Init.Data.Float.Float
instMaxFloat : Max Float
-- Std.Data.Internal.List.Associative
Std.Internal.List.containsKey_filter_containsKey_eq_false_of_containsKey_eq_false_left : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l₁ l₂ : List ((a : α) × β a)}
  {hl₁ : Std.Internal.List.DistinctKeys l₁} {k : α},
  Std.Internal.List.containsKey k l₁ = false →
    Std.Internal.List.containsKey k (List.filter (fun p => Std.Internal.List.containsKey p.fst l₂) l₁) = false
-- Mathlib.Analysis.Calculus.FDeriv.Prod
HasFDerivAtFilter.prodMk : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f₁ : E → F} {f₁' : E →L[𝕜] F} {L : Filter (E × E)}
  {f₂ : E → G} {f₂' : E →L[𝕜] G},
  HasFDerivAtFilter f₁ f₁' L → HasFDerivAtFilter f₂ f₂' L → HasFDerivAtFilter (fun x => (f₁ x, f₂ x)) (f₁'.prod f₂') L
-- Mathlib.GroupTheory.Coprod.Basic
AddEquiv.punitCoprod_apply : ∀ (M : Type u_1) [inst : AddMonoid M], ⇑(AddEquiv.punitCoprod M) = ⇑AddMonoid.Coprod.snd
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.map_comp_assoc : ∀ {k : Type u} [inst : CommRing k] {G H K : Type u} [inst_1 : Group G] [inst_2 : Group H] [inst_3 : Group K]
  {A : Rep.{u, u, u} k G} {B : Rep.{u, u, u} k H} {C : Rep.{u, u, u} k K} (f : G →* H) (g : H →* K)
  (φ : A ⟶ Rep.res f B) (ψ : B ⟶ Rep.res g C) (n : ℕ) {Z : ModuleCat k} (h : groupHomology C n ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (groupHomology.map (g.comp f) (CategoryTheory.CategoryStruct.comp φ (Rep.resMap f ψ)) n) h =
    CategoryTheory.CategoryStruct.comp (groupHomology.map f φ n)
      (CategoryTheory.CategoryStruct.comp (groupHomology.map g ψ n) h)
-- Mathlib.Analysis.Calculus.ContDiff.Operations
HasFTaylorSeriesUpToOn.add : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f : E → F} {p : E → FormalMultilinearSeries 𝕜 E F} {n : WithTop ℕ∞} {q : E → FormalMultilinearSeries 𝕜 E F}
  {g : E → F},
  HasFTaylorSeriesUpToOn n f p s → HasFTaylorSeriesUpToOn n g q s → HasFTaylorSeriesUpToOn n (f + g) (p + q) s
-- Mathlib.CategoryTheory.Distributive.Monoidal
/-- In a symmetric monoidal category, the right distributivity is equal to
the left distributivity up to braiding isomorphisms.  -/
CategoryTheory.coprodComparison_tensorRight_braiding_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Limits.HasBinaryCoproducts C] [inst_3 : CategoryTheory.SymmetricCategory C] {X Y Z : C},
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.coprodComparison (CategoryTheory.MonoidalCategory.tensorRight X) Y Z) (β_ (Y ⨿ Z) X).hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map (β_ Y X).hom (β_ Z X).hom)
      (CategoryTheory.Limits.coprodComparison (CategoryTheory.MonoidalCategory.tensorLeft X) Y Z)
-- Mathlib.RingTheory.MvPowerSeries.Equiv
MvPowerSeries.finSuccEquiv_X_zero : ∀ {R : Type u_2} [inst : CommSemiring R] {n : ℕ}, (MvPowerSeries.finSuccEquiv R n) (MvPowerSeries.X 0) = PowerSeries.X
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.instFunLike : {R : Type u_3} →
  {M : Type u_4} →
    {N : Type u_5} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : Module R M] → [inst_3 : AddCommMonoid N] → [inst_4 : Module R N] → FunLike (QuadraticMap R M N) M N
-- Mathlib.Topology.Compactification.StoneCech
instInhabitedPreStoneCech : {α : Type u} → [inst : TopologicalSpace α] → [Inhabited α] → Inhabited (PreStoneCech α)
-- Mathlib.Combinatorics.SetFamily.Shadow
/-- The shadow of a set family `𝒜` is all sets we can get by removing one element from any set in
`𝒜`, and the (`k` times) iterated shadow (`shadow^[k]`) is all sets we can get by removing `k`
elements from any set in `𝒜`.  -/
FinsetFamily.«term∂» : Lean.ParserDescr
-- Mathlib.Geometry.Convex.Cone.Pointed
/-- A pointed cone is a submodule of a module with scalars restricted to being nonnegative.  -/
PointedCone : (R : Type u_5) →
  (E : Type u_6) →
    [inst : Semiring R] →
      [inst_1 : PartialOrder R] → [IsOrderedRing R] → [inst_3 : AddCommMonoid E] → [Module R E] → Type u_6
-- Mathlib.Algebra.Group.Subsemigroup.Operations
Subsemigroup.srange_fst : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] [Nonempty N], (MulHom.fst M N).srange = ⊤
-- Mathlib.Dynamics.PeriodicPts.Defs
Function.isFixedPt_prodMap : ∀ {α : Type u_1} {β : Type u_2} {f : α → α} {g : β → β} (x : α × β),
  Function.IsFixedPt (Prod.map f g) x ↔ Function.IsFixedPt f x.1 ∧ Function.IsFixedPt g x.2
-- Mathlib.Dynamics.PeriodicPts.Defs
Function.IsPeriodicPt.gcd : ∀ {α : Type u_1} {f : α → α} {x : α} {m n : ℕ},
  Function.IsPeriodicPt f m x → Function.IsPeriodicPt f n x → Function.IsPeriodicPt f (m.gcd n) x
-- Mathlib.Analysis.Calculus.ContDiff.Operations
OpenPartialHomeomorph.contDiffOn_restrContDiff_source : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  (f : OpenPartialHomeomorph E F) {n : WithTop ℕ∞} (hn : n ≠ ↑⊤),
  ContDiffOn 𝕜 n (↑f) (OpenPartialHomeomorph.restrContDiff 𝕜 f n hn).source
-- Mathlib.RingTheory.Etale.StandardEtale
StandardEtalePresentation.toSubmersivePresentation_toPreSubmersivePresentation_toPresentation : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : StandardEtalePresentation R S), P.toSubmersivePresentation.toPresentation = P.toPresentation
-- Std.Time.Time.Unit.Basic
/-- Converts a `Millisecond.Offset` to a `Second.Offset`.
 -/
Std.Time.Second.Offset.ofMilliseconds : Std.Time.Millisecond.Offset → Std.Time.Second.Offset
-- Mathlib.MeasureTheory.SetSemiring
MeasureTheory.IsSetSemiring.empty_notMem_disjointOfUnion : ∀ {α : Type u_1} {C : Set (Set α)} {j : Set α} {J : Finset (Set α)} (hC : MeasureTheory.IsSetSemiring C) (hJ : ↑J ⊆ C),
  j ∈ J → ∅ ∉ hC.disjointOfUnion hJ j
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Lemmas
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.readyForRatAdd_delete : ∀ {n : ℕ} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (arr : Array ℕ),
  f.ReadyForRatAdd → (f.delete arr).ReadyForRatAdd
-- Mathlib.Topology.Separation.SeparatedNhds
/-- Used to prove that a regular topological space with Lindelöf topology is a normal space,
and a perfectly normal space is a completely normal space.  -/
hasSeparatingCovers_iff_separatedNhds : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s t : Set X},
  HasSeparatingCover s t ∧ HasSeparatingCover t s ↔ SeparatedNhds s t
-- Std.Internal.UV.System
Std.Internal.UV.System.instInhabitedCPUInfo : Inhabited Std.Internal.UV.System.CPUInfo
-- Mathlib.Topology.ContinuousMap.Defs
ContinuousMap.instFunLike : {X : Type u_1} → {Y : Type u_2} → [inst : TopologicalSpace X] → [inst_1 : TopologicalSpace Y] → FunLike C(X, Y) X Y