mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.UInt.Lemmas
UInt64.zero_mul : ∀ {a : UInt64}, 0 * a = 0
-- Mathlib.Data.Nat.Bits
Nat.boddDiv2.eq_2 : ∀ (n : ℕ),
  n.succ.boddDiv2 =
    match n.boddDiv2 with
    | (false, m) => (true, m)
    | (true, m) => (false, m.succ)
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.CostructuredArrow.ofCostructuredArrowProjEquivalence.functor_obj_left_hom : ∀ {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)
  (Y_1 : CategoryTheory.CostructuredArrow (CategoryTheory.CostructuredArrow.proj F Y) X),
  ((CategoryTheory.CostructuredArrow.ofCostructuredArrowProjEquivalence.functor F Y X).obj Y_1).left.hom = Y_1.hom
-- Lean.Parser.Basic
Lean.Parser.eoiFn : Lean.Parser.ParserFn
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
SimpleGraph.induce_pair_connected_of_adj : ∀ {V : Type u} {G : SimpleGraph V} {u v : V}, G.Adj u v → (SimpleGraph.induce {u, v} G).Connected
-- Mathlib.Order.Filter.Ultrafilter.Defs
Ultrafilter.map_pure : ∀ {α : Type u} {β : Type v} (m : α → β) (a : α), Ultrafilter.map m (pure a) = pure (m a)
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
Std.IterM.count_eq_fold : ∀ {α β : Type u_1} {m : Type u_1 → Type u_2} [inst : Std.Iterator α m β] [Std.Iterators.Finite α m] [inst_2 : Monad m]
  [LawfulMonad m] [inst_4 : Std.IteratorLoop α m m] {it : Std.IterM m β},
  it.length = Std.IterM.fold (fun acc x => { down := acc.down + 1 }) { down := 0 } it
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.formatQuarterNarrow : Std.Time.DateFormatSymbols → Std.Time.Month.Quarter → String
-- Mathlib.Analysis.Calculus.Deriv.Add
deriv_add_const' : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} (c : F), (deriv fun y => f y + c) = deriv f
-- Mathlib.Analysis.Calculus.FDeriv.Measurable
RightDerivMeasurableAux.B_mem_nhdsGT : ∀ {F : Type u_1} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] {f : ℝ → F} {K : Set F} {r s ε x : ℝ},
  x ∈ RightDerivMeasurableAux.B f K r s ε → RightDerivMeasurableAux.B f K r s ε ∈ nhdsWithin x (Set.Ioi x)
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.isScalarTower : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4}
  [inst_2 : TopologicalSpace M₁] [inst_3 : AddCommMonoid M₁] {M₂ : Type u_6} [inst_4 : TopologicalSpace M₂]
  [inst_5 : AddCommMonoid M₂] [inst_6 : Module R₁ M₁] [inst_7 : Module R₂ M₂] {S₂ : Type u_9} {T₂ : Type u_10}
  [inst_8 : DistribSMul S₂ M₂] [inst_9 : SMulCommClass R₂ S₂ M₂] [inst_10 : ContinuousConstSMul S₂ M₂]
  [inst_11 : DistribSMul T₂ M₂] [inst_12 : SMulCommClass R₂ T₂ M₂] [inst_13 : ContinuousConstSMul T₂ M₂]
  [inst_14 : SMul S₂ T₂] [IsScalarTower S₂ T₂ M₂], IsScalarTower S₂ T₂ (M₁ →SL[σ₁₂] M₂)
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticForm.toMatrix'_smul : ∀ {R : Type u_3} {n : Type w} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing R] [inst_3 : Invertible 2]
  (a : R) (Q : QuadraticForm R (n → R)), (a • Q).toMatrix' = a • Q.toMatrix'
-- Mathlib.GroupTheory.Schreier
/-- **Schreier's Lemma**: A finite index additive subgroup of a finitely generated
additive group is finitely generated.  -/
AddSubgroup.fg_of_index_ne_zero : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G) [hG : AddGroup.FG G] [H.FiniteIndex], AddGroup.FG ↥H
-- Lean.Parser.Extra
Lean.Parser.withSetOption.formatter : Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter
-- Mathlib.MeasureTheory.Measure.Haar.Extension
TopologicalGroup.IsSES.pushforward.congr_simp : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} {E : Type u_4} [inst : Group A] [inst_1 : Group B] [inst_2 : Group C]
  [inst_3 : TopologicalSpace A] [inst_4 : TopologicalSpace B] [inst_5 : TopologicalSpace C] {φ φ_1 : A →* B}
  (e_φ : φ = φ_1) {ψ ψ_1 : B →* C} (e_ψ : ψ = ψ_1) (H : TopologicalGroup.IsSES φ ψ) [inst_6 : IsTopologicalGroup A]
  [inst_7 : IsTopologicalGroup B] [inst_8 : NormedAddCommGroup E] [inst_9 : MeasurableSpace A] [inst_10 : BorelSpace A]
  (μA μA_1 : MeasureTheory.Measure A) (e_μA : μA = μA_1) [hμA : μA.IsHaarMeasure] [inst_11 : NormedSpace ℝ E]
  [inst_12 : IsTopologicalGroup C] [inst_13 : LocallyCompactSpace B], H.pushforward μA = ⋯.pushforward μA_1
-- Mathlib.Algebra.Group.Submonoid.Operations
MonoidHom.mem_mrange : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_4} [inst_2 : FunLike F M N]
  [mc : MonoidHomClass F M N] {f : F} {y : N}, y ∈ MonoidHom.mrange f ↔ ∃ x, f x = y
-- Mathlib.Algebra.Pointwise.Stabilizer
MulAction.stabilizer_finset_singleton : ∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : DecidableEq α] (b : α),
  MulAction.stabilizer G {b} = MulAction.stabilizer G b
-- Std.Internal.UV.System
/-- Returns the total system memory in bytes.
 -/
Std.Internal.UV.System.totalMemory : IO UInt64
-- Mathlib.Algebra.GroupWithZero.WithZero
WithZero.instDivisionCommMonoid : {α : Type u_1} → [DivisionCommMonoid α] → DivisionCommMonoid (WithZero α)
-- Lean.Data.Lsp.Basic
Lean.Lsp.instToJsonCommand : Lean.ToJson Lean.Lsp.Command
-- Mathlib.Data.Nat.Cast.Basic
MonoidWithZeroHom.ext_nat_iff : ∀ {A : Type u_3} [inst : MulZeroOneClass A] {f g : ℕ →*₀ A}, f = g ↔ ∀ {n : ℕ}, 0 < n → f n = g n
-- Mathlib.Algebra.Tropical.Basic
Tropical.instDivOfSub : {R : Type u} → [Sub R] → Div (Tropical R)
-- Init.Data.Float.Float32
/-- Computes the cosine of a floating-point number in radians.

This function does not reduce in the kernel. It is implemented in compiled code by the C function
`cosf`.
 -/
Float32.cos : Float32 → Float32
-- Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
/-- A monoid object in a functor category sends any object to a monoid object.  -/
CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.functorObjObj : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        [inst_2 : CategoryTheory.MonoidalCategory D] →
          (A : CategoryTheory.Functor C D) → [CategoryTheory.MonObj A] → C → CategoryTheory.Mon D
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.instWellFoundedRelation : WellFoundedRelation Cardinal.{u}
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.tensor_V : ∀ {k : Type u} {G : Type v} [inst : CommRing k] [inst_1 : Monoid G] {X Y : Rep.{u, u, v} k G},
  ↑(CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) = TensorProduct k ↑X ↑Y
-- Mathlib.Algebra.BigOperators.Pi
/-- This is used as the ext lemma instead of `AddMonoidHom.functions_ext` for reasons
explained in note [partially-applied ext lemmas].  -/
AddMonoidHom.functions_ext' : ∀ {I : Type u_7} [inst : DecidableEq I] {M : I → Type u_8} [inst_1 : (i : I) → AddCommMonoid (M i)] [Finite I]
  (N : Type u_9) [inst_3 : AddCommMonoid N] (g h : ((i : I) → M i) →+ N),
  (∀ (i : I), g.comp (AddMonoidHom.single M i) = h.comp (AddMonoidHom.single M i)) → g = h
-- Mathlib.Topology.MetricSpace.Dilation
/-- A dilation is continuous.  -/
Dilation.toContinuous : ∀ {α : Type u_1} {β : Type u_2} {F : Type u_4} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β]
  [inst_2 : FunLike F α β] [DilationClass F α β] (f : F), Continuous ⇑f
-- Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
/-- See also `Finset.sum_ite_eq'`.  -/
Fintype.sum_ite_eq' : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : Fintype ι] [inst_2 : DecidableEq ι] (i : ι)
  (f : ι → M), (∑ j, if j = i then f j else 0) = f i
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get!_diff_of_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.ExtDTreeMap α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] [inst_1 : Inhabited β] {k : α}, k ∈ t₂ → Std.ExtDTreeMap.Const.get! (t₁ \ t₂) k = default
-- Mathlib.Analysis.Complex.RemovableSingularity
/-- **Removable singularity** theorem: if `s` is a punctured neighborhood of `c : ℂ`, a function
`f : ℂ → E` is complex differentiable on `s`, and $f(z) - f(c)=o((z-c)^{-1})$, then `f` redefined to
be equal to `limUnder (𝓝[≠] c) f` at `c` is complex differentiable on `{c} ∪ s`.  -/
Complex.differentiableOn_update_limUnder_insert_of_isLittleO : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [CompleteSpace E] {f : ℂ → E} {s : Set ℂ}
  {c : ℂ},
  s ∈ nhdsWithin c {c}ᶜ →
    DifferentiableOn ℂ f s →
      ((fun z => f z - f c) =o[nhdsWithin c {c}ᶜ] fun z => (z - c)⁻¹) →
        DifferentiableOn ℂ (Function.update f c ((nhdsWithin c {c}ᶜ).limUnder f)) (insert c s)
-- Init.Data.UInt.Lemmas
UInt16.eq_sub_iff_add_eq : ∀ {a b c : UInt16}, a = c - b ↔ a + b = c
-- Mathlib.RingTheory.Filtration
Ideal.Filtration.ext_iff : ∀ {R : Type u_1} {inst : CommRing R} {I : Ideal R} {M : Type u_3} {inst_1 : AddCommGroup M} {inst_2 : Module R M}
  {x y : I.Filtration M}, x = y ↔ x.N = y.N
-- Mathlib.InformationTheory.KullbackLeibler.ChainRule
/-- If the log-likelihood ration between two composition-products is integrable, then so is the
log-likelihood ratio between the two measures on the first space.  -/
InformationTheory.integrable_llr_of_integrable_llr_compProd : ∀ {𝓧 : Type u_1} {𝓨 : Type u_2} {m𝓧 : MeasurableSpace 𝓧} {m𝓨 : MeasurableSpace 𝓨} {μ ν : MeasureTheory.Measure 𝓧}
  {κ η : ProbabilityTheory.Kernel 𝓧 𝓨} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν]
  [ProbabilityTheory.IsMarkovKernel κ] [ProbabilityTheory.IsMarkovKernel η],
  (μ.compProd κ).AbsolutelyContinuous (ν.compProd η) →
    MeasureTheory.Integrable (MeasureTheory.llr (μ.compProd κ) (ν.compProd η)) (μ.compProd κ) →
      MeasureTheory.Integrable (MeasureTheory.llr μ ν) μ
-- Mathlib.Order.Filter.Basic
Filter.sSup_sets_eq : ∀ {α : Type u} {s : Set (Filter α)}, (sSup s).sets = ⋂ f ∈ s, f.sets
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.Cofork.condition_assoc : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} (t : CategoryTheory.Limits.Cofork f g)
  {Z : C} (h : t.pt ⟶ Z),
  CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp t.π h) =
    CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.comp t.π h)
-- Init.ShareCommon
ShareCommon.StateFactoryImpl.mapInsert : (self : ShareCommon.StateFactoryImpl) → self.Map → ShareCommon.Object → ShareCommon.Object → self.Map
-- Mathlib.Topology.Sheaves.CommRingCat
/-- Given a submonoid at each of the stalks, we may define a submonoid presheaf consisting of
sections whose restriction onto each stalk falls in the given submonoid.  -/
TopCat.Presheaf.submonoidPresheafOfStalk : {X : TopCat} → (F : TopCat.Presheaf CommRingCat X) → ((x : ↑X) → Submonoid ↑(F.stalk x)) → F.SubmonoidPresheaf
-- Mathlib.LinearAlgebra.Finsupp.Defs
/-- Two `R`-linear maps from `Finsupp X M` which agree on each `single x y` agree everywhere.  -/
Finsupp.lhom_ext : ∀ {α : Type u_1} {M : Type u_2} {N : Type u_3} {R : Type u_5} {R₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : Module R M] [inst_4 : AddCommMonoid N] [inst_5 : Module R₂ N] {σ₁₂ : R →+* R₂}
  ⦃φ ψ : (α →₀ M) →ₛₗ[σ₁₂] N⦄, (∀ (a : α) (b : M), (φ fun₀ | a => b) = ψ fun₀ | a => b) → φ = ψ
-- Mathlib.CategoryTheory.Limits.Preserves.SigmaConst
CategoryTheory.Limits.ι_sigmaConstCokernelCofork_π : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] (R : C)
  {α : Type u_1} {β : Type u_2} (f : α → β) [inst_2 : CategoryTheory.Limits.HasCoproduct fun x => R]
  [inst_3 : CategoryTheory.Limits.HasCoproduct fun x => R] [inst_4 : CategoryTheory.Limits.HasCoproduct fun x => R]
  (b : β) (hb : b ∉ Set.range f),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (fun x => R) b)
      (CategoryTheory.Limits.Cofork.π (CategoryTheory.Limits.sigmaConstCokernelCofork R f)) =
    CategoryTheory.Limits.Sigma.ι (fun x => R) ⟨b, hb⟩
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.contains_diff : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [Std.TransCmp cmp] {k : α},
  (t₁ \ t₂).contains k = (t₁.contains k && !t₂.contains k)
-- Mathlib.Algebra.BigOperators.Finprod
/-- If `R` has no zero divisors, then multiplication commutes with `finsum_mem`. See `mul_finsum_mem'`
for a statement assuming finiteness of support.
 -/
mul_finsum_mem : ∀ {α : Type u_1} {R : Type u_7} [inst : NonUnitalNonAssocSemiring R] [NoZeroDivisors R] {s : Set α} (f : α → R) (r : R),
  r * ∑ᶠ (a : α) (_ : a ∈ s), f a = ∑ᶠ (a : α) (_ : a ∈ s), r * f a
-- Mathlib.Analysis.Normed.Module.Alternating.Basic
ContinuousAlternatingMap.opNorm_le_iff : ∀ {𝕜 : Type u} {E : Type wE} {F : Type wF} {ι : Type v} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : SeminormedAddCommGroup F]
  [inst_4 : NormedSpace 𝕜 F] [inst_5 : Fintype ι] {f : E [⋀^ι]→L[𝕜] F} {C : ℝ},
  0 ≤ C → (‖f‖ ≤ C ↔ ∀ (m : ι → E), ‖f m‖ ≤ C * ∏ i, ‖m i‖)
-- Mathlib.CategoryTheory.Comma.Arrow
CategoryTheory.Arrow.comp_right : ∀ {T : Type u} [inst : CategoryTheory.Category.{v, u} T] {X Y Z : CategoryTheory.Arrow T} (g : Z ⟶ Y) (f : Y ⟶ X),
  CategoryTheory.Arrow.Hom.right (CategoryTheory.CategoryStruct.comp g f) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.right g) (CategoryTheory.Arrow.Hom.right f)
-- Mathlib.Data.TypeVec
TypeVec.snd_prod_mk : ∀ {n : ℕ} {α α' β β' : TypeVec.{u_1} n} (f : α.Arrow β) (g : α'.Arrow β'),
  TypeVec.comp TypeVec.prod.snd (TypeVec.prod.map f g) = TypeVec.comp g TypeVec.prod.snd
-- Mathlib.CategoryTheory.Discrete.StructuredArrow
/-- If `F : C ⥤ Discrete T` is a functor with `T` containing
a unique element `t`, then this is the equivalence
`CostructuredArrow F (Discrete.mk t) ≌ C`.  -/
CategoryTheory.Discrete.costructuredArrowEquivalenceOfUnique : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {T : Type w} →
      (F : CategoryTheory.Functor C (CategoryTheory.Discrete T)) →
        (t : T) → [Subsingleton T] → CategoryTheory.CostructuredArrow F { as := t } ≌ C
-- Init.Grind.Module.Envelope
_private.Init.Grind.Module.Envelope.0.Lean.Grind.IntModule.OfNatModule.sub.eq_1 : ∀ {α : Type u} [inst : Lean.Grind.NatModule α] (q₁ q₂ : Lean.Grind.IntModule.OfNatModule.Q α),
  Lean.Grind.IntModule.OfNatModule.sub q₁ q₂ =
    q₁.liftOn₂ q₂
      (fun x x_1 =>
        match x with
        | (a, b) =>
          match x_1 with
          | (c, d) => Lean.Grind.IntModule.OfNatModule.Q.mk (a + d, c + b))
      ⋯
-- Mathlib.Probability.Martingale.Upcrossing
MeasureTheory.upperCrossingTime.eq_2 : ∀ {Ω : Type u_1} {ι : Type u_2} [inst : Preorder ι] [inst_1 : OrderBot ι] [inst_2 : InfSet ι] (a b : ℝ) (f : ι → Ω → ℝ)
  (N : ι) (n : ℕ),
  MeasureTheory.upperCrossingTime a b f N n.succ = fun ω =>
    MeasureTheory.hittingBtwn f (Set.Ici b)
      (MeasureTheory.lowerCrossingTimeAux a f (MeasureTheory.upperCrossingTime a b f N n ω) N ω) N ω
-- Mathlib.Order.KrullDimension
Order.height_ne_zero : ∀ {α : Type u_1} [inst : Preorder α] {x : α}, Order.height x ≠ 0 ↔ ¬IsMin x
-- Mathlib.Topology.Instances.AddCircle.Defs
AddCircle.liftIco_zero_continuous : ∀ {𝕜 : Type u_1} {B : Type u_2} [inst : AddCommGroup 𝕜] [inst_1 : LinearOrder 𝕜] [inst_2 : IsOrderedAddMonoid 𝕜] {p : 𝕜}
  [hp : Fact (0 < p)] [inst_3 : Archimedean 𝕜] [inst_4 : TopologicalSpace 𝕜] [OrderTopology 𝕜]
  [inst_6 : TopologicalSpace B] {f : 𝕜 → B},
  f 0 = f p → ContinuousOn f (Set.Icc 0 p) → Continuous (AddCircle.liftIco p 0 f)
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
CategoryTheory.StrictlyUnitaryPseudofunctor.mk'_mapId : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (S : CategoryTheory.StrictlyUnitaryPseudofunctorCore B C) (x : B),
  (CategoryTheory.StrictlyUnitaryPseudofunctor.mk' S).mapId x = CategoryTheory.eqToIso ⋯
-- Mathlib.Algebra.Order.UpperLower
add_lowerClosure : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : Preorder α] [IsOrderedAddMonoid α] (s t : Set α),
  s + ↑(lowerClosure t) = ↑(lowerClosure (s + t))
-- Init.Data.Array.Find
Array.findFinIdx?_subtype : ∀ {α : Type u_1} {p : α → Prop} {xs : Array { x // p x }} {f : { x // p x } → Bool} {g : α → Bool},
  (∀ (x : α) (h : p x), f ⟨x, h⟩ = g x) →
    Array.findFinIdx? f xs = Option.map (fun i => Fin.cast ⋯ i) (Array.findFinIdx? g xs.unattach)
-- Init.Data.String.Basic
String.Pos.cast_rfl : ∀ {s : String} {pos : s.Pos}, pos.cast ⋯ = pos
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValue_filter_not_contains_map_fst : ∀ {α : Type u} {β : Type v} [inst : BEq α] [EquivBEq α] {l₁ l₂ : List ((_ : α) × β)} {k : α},
  Std.Internal.List.DistinctKeys l₁ →
    ∀ {h₁ : Std.Internal.List.containsKey k (List.filter (fun p => !(List.map Sigma.fst l₂).contains p.fst) l₁) = true}
      {h₂ : Std.Internal.List.containsKey k l₁ = true},
      Std.Internal.List.getValue k (List.filter (fun p => !(List.map Sigma.fst l₂).contains p.fst) l₁) h₁ =
        Std.Internal.List.getValue k l₁ h₂
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.sin_pi_div_two_sub : ∀ (x : ℝ), Real.sin (Real.pi / 2 - x) = Real.cos x
-- Mathlib.Topology.Algebra.UniformMulAction
AddGroup.uniformContinuousConstSMul_int : ∀ (X : Type x) [inst : UniformSpace X] [inst_1 : AddGroup X] [IsUniformAddGroup X], UniformContinuousConstSMul ℤ X
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomAddAct.symm_mk_add : ∀ {M : Type u_1} [inst : Add M] (a b : Mᵈᵃᵃ), DomAddAct.mk.symm (a + b) = DomAddAct.mk.symm b + DomAddAct.mk.symm a
-- Mathlib.Topology.UniformSpace.Defs
UniformSpace.ball_mono : ∀ {β : Type ub} {V W : Set (β × β)}, V ⊆ W → ∀ (x : β), UniformSpace.ball x V ⊆ UniformSpace.ball x W
-- Mathlib.Order.DirSupClosed
dirSupInacc_iff_forall_sSup : ∀ {α : Type u_1} {s : Set α} [inst : CompleteLattice α],
  DirSupInacc s ↔ ∀ ⦃d : Set α⦄, d.Nonempty → DirectedOn (fun x1 x2 => x1 ≤ x2) d → sSup d ∈ s → (d ∩ s).Nonempty
-- Lean.Data.JsonRpc
Lean.JsonRpc.MessageMetaData.request.inj : ∀ {id : Lean.JsonRpc.RequestID} {method : String} {id_1 : Lean.JsonRpc.RequestID} {method_1 : String},
  Lean.JsonRpc.MessageMetaData.request id method = Lean.JsonRpc.MessageMetaData.request id_1 method_1 →
    id = id_1 ∧ method = method_1
-- Mathlib.Algebra.BigOperators.Finprod
finprod_set_coe_eq_finprod_mem : ∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] {f : α → M} (s : Set α),
  ∏ᶠ (j : ↑s), f ↑j = ∏ᶠ (i : α) (_ : i ∈ s), f i
-- Std.Http.Server.Config
/-- Maximum allowed chunk payload size in bytes (default: 8 MiB).
 -/
Std.Http.Config.maxChunkSize : Std.Http.Config → ℕ
-- Mathlib.Probability.Independence.Kernel.Indep
ProbabilityTheory.Kernel.IndepSets.biUnion : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {s : ι → Set (Set Ω)} {s' : Set (Set Ω)}
  {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {u : Set ι},
  (∀ n ∈ u, ProbabilityTheory.Kernel.IndepSets (s n) s' κ μ) → ProbabilityTheory.Kernel.IndepSets (⋃ n ∈ u, s n) s' κ μ
-- Mathlib.CategoryTheory.Monoidal.Functor
/-- Monoidal functors commute with right tensoring up to isomorphism  -/
CategoryTheory.Functor.Monoidal.commTensorRight : {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) →
              [F.Monoidal] →
                (X : C) →
                  F.comp (CategoryTheory.MonoidalCategory.tensorRight (F.obj X)) ≅
                    (CategoryTheory.MonoidalCategory.tensorRight X).comp F
-- Lean.Compiler.LCNF.Types
/-- Return `true` if `type` is a LCNF type former type.

Remark: This is faster than `Lean.Meta.isTypeFormer`, as this
assumes that the input `type` is an LCNF type.
 -/
Lean.Compiler.LCNF.isTypeFormerType : Lean.Expr → Bool
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.isEmpty_insertIfNew : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α}
  {v : β k}, (t.insertIfNew k v).isEmpty = false
-- Lean.Server.GoTo
Lean.Server.GoToContext.mk.sizeOf_spec : ∀ (doc : Lean.Server.DocumentMeta) (kind : Lean.Server.GoToKind) (infoTree? : Option Lean.Elab.InfoTree)
  (originInfo? : Option Lean.Elab.Info) (children : Lean.PersistentArray Lean.Elab.InfoTree),
  sizeOf { doc := doc, kind := kind, infoTree? := infoTree?, originInfo? := originInfo?, children := children } =
    1 + sizeOf doc + sizeOf kind + sizeOf infoTree? + sizeOf originInfo? + sizeOf children
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey!_insert : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : Inhabited α]
  {k a : α} {v : β}, (t.insert k v).getKey! a = if cmp k a = Ordering.eq then k else t.getKey! a
-- Mathlib.Tactic.FailIfNoProgress
/-- `fail_if_no_progress tacs` evaluates `tacs`, and fails if no progress is made on the main goal
or the local context at reducible transparency.  -/
Mathlib.Tactic.failIfNoProgress : Lean.ParserDescr
-- Mathlib.Data.Complex.BigOperators
Complex.im_expect : ∀ {α : Type u_1} (s : Finset α) (f : α → ℂ), (s.expect fun i => f i).im = s.expect fun i => (f i).im
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Limits.isoZeroOfEpiZero_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} (x : CategoryTheory.Epi 0),
  (CategoryTheory.Limits.isoZeroOfEpiZero x).inv = 0
-- Init.Data.Nat.Gcd
Nat.gcd_mul_left_right_of_gcd_eq_one : ∀ {n m k : ℕ}, n.gcd m = 1 → n.gcd (k * m) = n.gcd k
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
_private.Mathlib.Analysis.Distribution.SchwartzSpace.Basic.0.SchwartzMap.seminormAux_add_le : ∀ {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] (k n : ℕ) (f g : SchwartzMap E F),
  SchwartzMap.seminormAux✝ k n (f + g) ≤ SchwartzMap.seminormAux✝ k n f + SchwartzMap.seminormAux✝ k n g
-- Mathlib.Topology.PartialHomeomorph.Basic
/-- A partial homeomorphism whose source is all of `X` defines an embedding of `X` into
`Y`. The converse is also true; see `IsEmbedding.toPartialHomeomorph`.  -/
PartialHomeomorph.isEmbedding : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : PartialHomeomorph X Y),
  e.source = Set.univ → Topology.IsEmbedding ↑e
-- Mathlib.Algebra.Homology.DerivedCategory.TStructure
DerivedCategory.isZero_of_isGE : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] (X : DerivedCategory C) (n i : ℤ),
  i < n → ∀ [hX : X.IsGE n], CategoryTheory.Limits.IsZero ((DerivedCategory.homologyFunctor C i).obj X)
-- Init.Data.Range.Polymorphic.UpwardEnumerable
Std.PRange.LawfulUpwardEnumerableLT.mk : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : LT α],
  (∀ (a b : α), a < b ↔ Std.PRange.UpwardEnumerable.LT a b) → Std.PRange.LawfulUpwardEnumerableLT α
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toList_rio_ne_nil_iff : ∀ {n : ℕ}, (*...n).toList ≠ [] ↔ 0 < n
-- Mathlib.Data.Semiquot
Semiquot.nonempty : ∀ {α : Type u_1} (q : Semiquot α), q.s.Nonempty
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
Tactic.ComputeAsymptotics.Monomial.zeros_append_toFun : ∀ (coef : ℝ) {exps : Tactic.ComputeAsymptotics.UnitMonomial} {left right : Tactic.ComputeAsymptotics.Basis},
  have t := { coef := coef, unit := List.replicate (List.length left) 0 ++ exps };
  t.toFun (left ++ right) = { coef := coef, unit := exps }.toFun right
-- Mathlib.Order.Bounded
Set.bounded_gt_Ico : ∀ {α : Type u_1} [inst : Preorder α] [NoMinOrder α] (a b : α), Set.Bounded (fun x1 x2 => x1 > x2) (Set.Ico a b)
-- Mathlib.CategoryTheory.Limits.Opposites
CategoryTheory.Limits.hasLimit_of_hasColimit_op : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} J]
  (F : CategoryTheory.Functor J C) [CategoryTheory.Limits.HasColimit F.op], CategoryTheory.Limits.HasLimit F