mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.Iterators.Lemmas.Combinators.Zip
_private.Std.Data.Iterators.Lemmas.Combinators.Zip.0.Std.Iter.atIdxSlow?.match_1.eq_2 : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] (it : Std.Iter β)
  (motive :
    (n : ℕ) →
      ((a' : Std.Iter β) →
          (b' : ℕ) →
            InvImage (Prod.Lex WellFoundedRelation.rel Std.IterM.TerminationMeasures.Productive.Rel)
                (fun p => (p.snd, p.fst.finitelyManySkips!)) ⟨a', b'⟩ ⟨it, n⟩ →
              Option β) →
        Sort u_2)
  (k : ℕ)
  (recur :
    (a' : Std.Iter β) →
      (b' : ℕ) →
        InvImage (Prod.Lex WellFoundedRelation.rel Std.IterM.TerminationMeasures.Productive.Rel)
            (fun p => (p.snd, p.fst.finitelyManySkips!)) ⟨a', b'⟩ ⟨it, k + 1⟩ →
          Option β)
  (h_1 :
    (recur :
        (a' : Std.Iter β) →
          (b' : ℕ) →
            InvImage (Prod.Lex WellFoundedRelation.rel Std.IterM.TerminationMeasures.Productive.Rel)
                (fun p => (p.snd, p.fst.finitelyManySkips!)) ⟨a', b'⟩ ⟨it, 0⟩ →
              Option β) →
      motive 0 recur)
  (h_2 :
    (k : ℕ) →
      (recur :
          (a' : Std.Iter β) →
            (b' : ℕ) →
              InvImage (Prod.Lex WellFoundedRelation.rel Std.IterM.TerminationMeasures.Productive.Rel)
                  (fun p => (p.snd, p.fst.finitelyManySkips!)) ⟨a', b'⟩ ⟨it, k + 1⟩ →
                Option β) →
        motive k.succ recur),
  (match k.succ, recur with
    | 0, recur => h_1 recur
    | k.succ, recur => h_2 k recur) =
    h_2 k recur
-- Mathlib.CategoryTheory.Limits.Opposites
CategoryTheory.Limits.limitOpIsoOpColimit.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} J]
  (F : CategoryTheory.Functor J C) [inst_2 : CategoryTheory.Limits.HasColimit F],
  CategoryTheory.Limits.limitOpIsoOpColimit F =
    CategoryTheory.Limits.limit.isoLimitCone
      { cone := (CategoryTheory.Limits.colimit.cocone F).op, isLimit := (CategoryTheory.Limits.colimit.isColimit F).op }
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
IsEllipticNet.atomRel_abs₄ : ∀ {R : Type u_1} [inst : CommRing R] (W : ℤ → R) (a b c d : ℤ),
  IsEllipticNet.atomRel W a b c |d| = IsEllipticNet.atomRel W a b c d
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.ne_zero_of_mem_nthRootsFinset : ∀ {R : Type u} {n : ℕ} [inst : CommRing R] [inst_1 : IsDomain R] {η a : R},
  a ≠ 0 → η ∈ Polynomial.nthRootsFinset n a → η ≠ 0
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Var
Std.Tactic.BVDecide.BVExpr.bitblast.BVVar.ident : {width : ℕ} → Std.Tactic.BVDecide.BVExpr.bitblast.BVVar width → ℕ
-- Std.Data.HashSet.Lemmas
Std.HashSet.mem_union_iff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {k : α},
  (m₁ ∪ m₂).contains k = true ↔ m₁.contains k = true ∨ m₂.contains k = true
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- Helper function for constructing morphisms between equalizer forks.
 -/
CategoryTheory.Limits.Fork.mkHom : {C : Type u} →
  {X Y : C} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {f g : X ⟶ Y} →
        {s t : CategoryTheory.Limits.Fork f g} →
          (k : s.pt ⟶ t.pt) → CategoryTheory.CategoryStruct.comp k t.ι = s.ι → (s ⟶ t)
-- Mathlib.MeasureTheory.Measure.MeasureSpaceDef
/-- `∃ᵐ a, p a` means that `p` holds frequently, i.e. on a set of positive measure,
w.r.t. the volume measure.

This is notation for `Filter.Frequently P (MeasureTheory.ae MeasureSpace.volume)`.  -/
MeasureTheory.«term∃ᵐ_,_» : Lean.ParserDescr
-- Mathlib.Algebra.Homology.QuasiIso
/-- The morphism property on `HomologicalComplex C c` given by quasi-isomorphisms.  -/
HomologicalComplex.quasiIso : {ι : Type u_1} →
  (C : Type u) →
    [inst : CategoryTheory.Category.{v, u} C] →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
        (c : ComplexShape ι) →
          [CategoryTheory.CategoryWithHomology C] → CategoryTheory.MorphismProperty (HomologicalComplex C c)
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cocone.functorialityEquivalence_unitIso : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {D : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} D] (F : CategoryTheory.Functor J C) (e : C ≌ D),
  (CategoryTheory.Limits.Cocone.functorialityEquivalence F e).unitIso =
    CategoryTheory.NatIso.ofComponents'
      (fun c =>
        CategoryTheory.Limits.Cocone.extInv
          (e.unitIso.app ((CategoryTheory.Functor.id (CategoryTheory.Limits.Cocone F)).obj c).pt) ⋯)
      ⋯
-- Mathlib.Topology.DerivedSet
derivedSet_subset_closure : ∀ {X : Type u_1} [inst : TopologicalSpace X] (A : Set X), derivedSet A ⊆ closure A
-- Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.inverse_map_hom_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.MonoidalCategory D] [inst_3 : CategoryTheory.BraidedCategory D]
  {X Y : CategoryTheory.Functor C (CategoryTheory.CommMon D)} (α : X ⟶ Y) (X_1 : C),
  (CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.inverse.map α).hom.hom.app X_1 = (α.app X_1).hom.hom
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
hasMFDerivWithinAt_inr : ∀ {𝕜 : 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] {M' : Type u_21} [inst_6 : TopologicalSpace M']
  [inst_7 : ChartedSpace H M'] {q' : M'} {t : Set M'},
  HasMFDerivAt[t] Sum.inr q' (ContinuousLinearMap.id 𝕜 (TangentSpace I q'))
-- Mathlib.Analysis.LocallyConvex.Separation
geometric_hahn_banach_point_closed : ∀ {E : Type u_2} [inst : TopologicalSpace E] [inst_1 : AddCommGroup E] [inst_2 : Module ℝ E] {t : Set E} {x : E}
  [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E],
  Convex ℝ t → IsClosed t → x ∉ t → ∃ f u, f x < u ∧ ∀ b ∈ t, u < f b
-- Mathlib.CategoryTheory.Extensive
CategoryTheory.PreservesPullbacksOfInclusions.preservesPullbackInr' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  [inst_2 : CategoryTheory.Limits.HasBinaryCoproducts C] (F : CategoryTheory.Functor C D)
  [CategoryTheory.PreservesPullbacksOfInclusions F] {X Y Z : C} (f : Z ⟶ X ⨿ Y),
  CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f CategoryTheory.Limits.coprod.inr) F
-- Mathlib.RepresentationTheory.Induced
Rep.indResHomEquiv_apply : ∀ {k : Type u} {G : Type v} {H : Type v'} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] (φ : G →* H)
  (A : Rep.{max w v' u, u, v} k G) (B : Rep.{max w v' u, u, v'} k H) (f : Rep.ind φ A ⟶ B),
  (Rep.indResHomEquiv φ A B) f =
    Rep.ofHom { toLinearMap := (Rep.Hom.hom f).toLinearMap ∘ₗ Representation.IndV.mk φ A.ρ 1, isIntertwining' := ⋯ }
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.contains_union : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [EquivBEq α] [LawfulHashable α],
  (↑m₁).WF → (↑m₂).WF → ∀ {k : α}, (m₁.union m₂).contains k = (m₁.contains k || m₂.contains k)
-- Mathlib.Order.PrimeIdeal
/-- Create an element of type `Order.Ideal.PrimePair` from a filter satisfying the predicate
`Order.PFilter.IsPrime`.  -/
Order.PFilter.IsPrime.toPrimePair : {P : Type u_1} → [inst : Preorder P] → {F : Order.PFilter P} → F.IsPrime → Order.Ideal.PrimePair P
-- Mathlib.Algebra.Category.Ring.Basic
/-- The type of morphisms in `SemiRingCat`.  -/
SemiRingCat.Hom : SemiRingCat → SemiRingCat → Type u
-- Mathlib.Order.WellFoundedSet
Set.IsWF.eq_1 : ∀ {α : Type u_2} [inst : LT α] (s : Set α), s.IsWF = s.WellFoundedOn fun x1 x2 => x1 < x2
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
/-- Eta-expanded form of `TendstoUniformlyOnFilter.inv` -/
TendstoUniformlyOnFilter.fun_inv : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : Group α] [IsUniformGroup α] {ι : Type u_3}
  {l : Filter ι} {l' : Filter β} {f : ι → β → α} {g : β → α},
  TendstoUniformlyOnFilter f g l l' → TendstoUniformlyOnFilter (fun i i_1 => (f i i_1)⁻¹) (fun i => (g i)⁻¹) l l'
-- Mathlib.Order.Filter.Bases.Basic
Filter.HasBasis.congr : ∀ {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α},
  l.HasBasis p s →
    ∀ {p' : ι → Prop} {s' : ι → Set α}, (∀ (i : ι), p i ↔ p' i) → (∀ (i : ι), p i → s i = s' i) → l.HasBasis p' s'
-- Mathlib.Analysis.Normed.Module.Ray
SameRay.norm_sub : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {x y : E},
  SameRay ℝ x y → ‖x - y‖ = |‖x‖ - ‖y‖|
-- Mathlib.CategoryTheory.MorphismProperty.Basic
/-- The `MorphismProperty C` satisfied by epimorphisms in `C`.  -/
CategoryTheory.MorphismProperty.epimorphisms : (C : Type u) → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.MorphismProperty C
-- Mathlib.Algebra.Group.Subgroup.Actions
/-- The action by a subgroup is the action by the underlying group.  -/
Subgroup.instMulDistribMulActionSubtypeMem : {G : Type u_1} →
  {α : Type u_2} →
    [inst : Group G] → [inst_1 : Monoid α] → [MulDistribMulAction G α] → (S : Subgroup G) → MulDistribMulAction (↥S) α
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.counitIso_hom_inv_id_app_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : C ≌ D) (Y : D) {Z : D} (h : e.functor.obj (e.inverse.obj Y) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (e.counit.app Y) (CategoryTheory.CategoryStruct.comp (e.counitInv.app Y) h) = h
-- Mathlib.Order.CompactlyGenerated.Basic
le_iff_compact_le_imp : ∀ {α : Type u_2} [inst : CompleteLattice α] [IsCompactlyGenerated α] {a b : α},
  a ≤ b ↔ ∀ (c : α), IsCompactElement c → c ≤ a → c ≤ b
-- Mathlib.GroupTheory.GroupAction.Basic
/-- The action of a group on an orbit is transitive.  -/
MulAction.instIsPretransitiveElemOrbit : ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] (a : α),
  MulAction.IsPretransitive G ↑(MulAction.orbit G a)
-- Mathlib.CategoryTheory.Monoidal.DayConvolution.Braided
CategoryTheory.MonoidalCategory.DayConvolution.braiding.eq_1 : ∀ {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.BraidedCategory C]
  [inst_4 : CategoryTheory.MonoidalCategory V] [inst_5 : CategoryTheory.BraidedCategory V]
  (F G : CategoryTheory.Functor C V) [inst_6 : CategoryTheory.MonoidalCategory.DayConvolution F G]
  [inst_7 : CategoryTheory.MonoidalCategory.DayConvolution G F],
  CategoryTheory.MonoidalCategory.DayConvolution.braiding F G =
    {
      hom :=
        (CategoryTheory.MonoidalCategory.DayConvolution.corepresentableBy F G).homEquiv.symm
          (CategoryTheory.MonoidalCategory.DayConvolution.braidingHomCorepresenting F G),
      inv :=
        (CategoryTheory.MonoidalCategory.DayConvolution.corepresentableBy G F).homEquiv.symm
          (CategoryTheory.MonoidalCategory.DayConvolution.braidingInvCorepresenting F G),
      hom_inv_id := ⋯, inv_hom_id := ⋯ }
-- Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
ContMDiff.smul_section : ∀ {𝕜 : 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] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → TopologicalSpace (V x)] [inst_10 : FiberBundle F V] [inst_11 : (x : M) → AddCommGroup (V x)]
  [inst_12 : (x : M) → Module 𝕜 (V x)] [VectorBundle 𝕜 F V] {f : M → 𝕜} {s : (x : M) → V x},
  ContMDiff I (modelWithCornersSelf 𝕜 𝕜) n f →
    (ContMDiff I (I.prod (modelWithCornersSelf 𝕜 F)) n fun x => ⟨x, s x⟩) →
      ContMDiff I (I.prod (modelWithCornersSelf 𝕜 F)) n fun x => ⟨x, (f • s) x⟩
-- Mathlib.Data.Finset.Fin
Finset.image_val_attachFin : ∀ {n : ℕ} {s : Finset ℕ} (h : ∀ m ∈ s, m < n), Finset.image Fin.val (s.attachFin h) = s
-- Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction
UpperHalfPlane.σ_eventuallyEq : ∀ (g : GL (Fin 2) ℝ), UpperHalfPlane.σ =ᶠ[nhds g] fun x => UpperHalfPlane.σ g
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.dist_snd_le : ∀ {p : ENNReal} {α : Type u_2} {β : Type u_3} [hp : Fact (1 ≤ p)] [inst : PseudoMetricSpace α]
  [inst_1 : PseudoMetricSpace β] (x y : WithLp p (α × β)), dist x.snd y.snd ≤ dist x y
-- Mathlib.Combinatorics.Additive.CovBySMul
CovByVAdd.trans : ∀ {M : Type u_1} {N : Type u_2} {X : Type u_3} [inst : AddMonoid M] [inst_1 : AddMonoid N] [inst_2 : AddAction M X]
  [inst_3 : AddAction N X] {K L : ℝ} {A B C : Set X} [inst_4 : VAdd M N] [VAddAssocClass M N X],
  CovByVAdd M K A B → CovByVAdd N L B C → CovByVAdd N (K * L) A C
-- Mathlib.Algebra.Order.ToIntervalMod
AddCommGroup.not_modEq_iff_toIcoMod_eq_toIocMod : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) {a b : α}, ¬a ≡ b [PMOD p] ↔ toIcoMod hp a b = toIocMod hp a b
-- Mathlib.Algebra.Group.Pi.Basic
Pi.cancelMonoid : {I : Type u} → {f : I → Type v₁} → [(i : I) → CancelMonoid (f i)] → CancelMonoid ((i : I) → f i)
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.isCodetector_codetector : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.HasCodetector C],
  CategoryTheory.IsCodetector (CategoryTheory.codetector C)
-- Mathlib.Topology.Algebra.Module.Basic
Submodule.topologicalClosure_coe : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : TopologicalSpace M] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] [inst_4 : ContinuousConstSMul R M] [inst_5 : ContinuousAdd M] (s : Submodule R M),
  ↑s.topologicalClosure = closure ↑s
-- Init.Data.Fin.Lemmas
Fin.zero_eq_last_iff : ∀ {n : ℕ}, 0 = Fin.last n ↔ n = 0
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.mul.go.match_1.congr_eq_3 : ∀ (motive : Lean.Grind.CommRing.Mon → Lean.Grind.CommRing.Mon → Sort u_1) (m₁ m₂ : Lean.Grind.CommRing.Mon)
  (h_1 : (m₁ : Lean.Grind.CommRing.Mon) → motive m₁ Lean.Grind.CommRing.Mon.unit)
  (h_2 : (m₂ : Lean.Grind.CommRing.Mon) → motive Lean.Grind.CommRing.Mon.unit m₂)
  (h_3 :
    (pw₁ : Lean.Grind.CommRing.Power) →
      (m₁ : Lean.Grind.CommRing.Mon) →
        (pw₂ : Lean.Grind.CommRing.Power) →
          (m₂ : Lean.Grind.CommRing.Mon) →
            motive (Lean.Grind.CommRing.Mon.mult pw₁ m₁) (Lean.Grind.CommRing.Mon.mult pw₂ m₂))
  (pw₁ : Lean.Grind.CommRing.Power) (m₁_1 : Lean.Grind.CommRing.Mon) (pw₂ : Lean.Grind.CommRing.Power)
  (m₂_1 : Lean.Grind.CommRing.Mon),
  m₁ = Lean.Grind.CommRing.Mon.mult pw₁ m₁_1 →
    m₂ = Lean.Grind.CommRing.Mon.mult pw₂ m₂_1 →
      (match m₁, m₂ with
        | m₁, Lean.Grind.CommRing.Mon.unit => h_1 m₁
        | Lean.Grind.CommRing.Mon.unit, m₂ => h_2 m₂
        | Lean.Grind.CommRing.Mon.mult pw₁ m₁, Lean.Grind.CommRing.Mon.mult pw₂ m₂ => h_3 pw₁ m₁ pw₂ m₂) ≍
        h_3 pw₁ m₁_1 pw₂ m₂_1
-- Mathlib.AlgebraicGeometry.Group.Affine
AlgebraicGeometry.preservesTerminalIso_algSpec : ∀ {R : CommRingCat},
  CategoryTheory.CartesianMonoidalCategory.preservesTerminalIso (AlgebraicGeometry.algSpec R) =
    CategoryTheory.Over.isoMk (CategoryTheory.Iso.refl (AlgebraicGeometry.Spec R)) ⋯
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
/-- If `M` is an additive monoid object, then `Hom(-, M)` is a presheaf of additive monoids.  -/
CategoryTheory.yonedaAddMonObj : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v, u_1} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      (M : C) → [CategoryTheory.AddMonObj M] → CategoryTheory.Functor Cᵒᵖ AddMonCat
-- Mathlib.Data.Part
Part.ext_iff : ∀ {α : Type u_1} {o p : Part α}, o = p ↔ ∀ (a : α), a ∈ o ↔ a ∈ p
-- Init.Data.SInt.Lemmas
Int64.toInt_ofIntTruncate : ∀ {x : ℤ}, Int64.minValue.toInt ≤ x → x ≤ Int64.maxValue.toInt → (Int64.ofIntClamp x).toInt = x
-- Mathlib.Data.List.Range
_private.Mathlib.Data.List.Range.0.List.ranges.match_1.eq_2 : ∀ (motive : List ℕ → Sort u_1) (a : ℕ) (l : List ℕ) (h_1 : Unit → motive [])
  (h_2 : (a : ℕ) → (l : List ℕ) → motive (a :: l)),
  (match a :: l with
    | [] => h_1 ()
    | a :: l => h_2 a l) =
    h_2 a l
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.keys_filter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {f : α → β → Bool},
  (Std.DHashMap.filter f m).keys.Perm
    (List.filter
        (fun x_2 =>
          match x_2 with
          | ⟨x_3, h'⟩ => f x_3 (Std.DHashMap.Const.get m x_3 ⋯))
        m.keys.attach).unattach
-- Lean.Data.PersistentHashSet
Lean.PersistentHashSet.erase : {α : Type u_1} → {x : BEq α} → {x_1 : Hashable α} → Lean.PersistentHashSet α → α → Lean.PersistentHashSet α
-- Aesop.Options.Public
Aesop.Options.mk.sizeOf_spec : ∀ (strategy : Aesop.Strategy)
  (maxRuleApplicationDepth maxRuleApplications maxGoals maxNormIterations maxSafePrefixRuleApplications : ℕ)
  (applyHypsTransparency assumptionTransparency destructProductsTransparency : Lean.Meta.TransparencyMode)
  (introsTransparency? : Option Lean.Meta.TransparencyMode)
  (terminal warnOnNonterminal traceScript enableSimp useSimpAll useDefaultSimpSet enableUnfold : Bool),
  sizeOf
      { strategy := strategy, maxRuleApplicationDepth := maxRuleApplicationDepth,
        maxRuleApplications := maxRuleApplications, maxGoals := maxGoals, maxNormIterations := maxNormIterations,
        maxSafePrefixRuleApplications := maxSafePrefixRuleApplications, applyHypsTransparency := applyHypsTransparency,
        assumptionTransparency := assumptionTransparency, destructProductsTransparency := destructProductsTransparency,
        introsTransparency? := introsTransparency?, terminal := terminal, warnOnNonterminal := warnOnNonterminal,
        traceScript := traceScript, enableSimp := enableSimp, useSimpAll := useSimpAll,
        useDefaultSimpSet := useDefaultSimpSet, enableUnfold := enableUnfold } =
    1 + sizeOf strategy + sizeOf maxRuleApplicationDepth + sizeOf maxRuleApplications + sizeOf maxGoals +
                              sizeOf maxNormIterations +
                            sizeOf maxSafePrefixRuleApplications +
                          sizeOf applyHypsTransparency +
                        sizeOf assumptionTransparency +
                      sizeOf destructProductsTransparency +
                    sizeOf introsTransparency? +
                  sizeOf terminal +
                sizeOf warnOnNonterminal +
              sizeOf traceScript +
            sizeOf enableSimp +
          sizeOf useSimpAll +
        sizeOf useDefaultSimpSet +
      sizeOf enableUnfold
-- Mathlib.RingTheory.Congruence.Defs
RingConGen.Rel.trans : ∀ {R : Type u_1} [inst : Add R] [inst_1 : Mul R] {r : R → R → Prop} {x y z : R},
  RingConGen.Rel r x y → RingConGen.Rel r y z → RingConGen.Rel r x z
-- Mathlib.Algebra.Order.Star.Basic
star_neg_iff : ∀ {R : Type u_1} [inst : NonUnitalSemiring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] [StarOrderedRing R]
  {x : R}, star x < 0 ↔ x < 0
-- Mathlib.GroupTheory.GroupAction.Pointwise
vadd_preimage_set_subset : ∀ {M : Type u_1} {α : Type u_2} {β : Type u_3} {F : Type u_4} [inst : VAdd M α] [inst_1 : VAdd M β]
  [inst_2 : FunLike F α β] [AddActionHomClass F M α β] (f : F) (c : M) (t : Set β), c +ᵥ ⇑f ⁻¹' t ⊆ ⇑f ⁻¹' (c +ᵥ t)
-- Mathlib.Combinatorics.Nullstellensatz
/-- A multivariate polynomial that vanishes on a large product finset is the zero polynomial.  -/
MvPolynomial.eq_zero_of_eval_zero_at_prod_finset : ∀ {R : Type u_1} [inst : CommRing R] {σ : Type u_2} [Finite σ] [IsDomain R] (P : MvPolynomial σ R) (S : σ → Finset R),
  (∀ (i : σ), MvPolynomial.degreeOf i P < (S i).card) →
    (∀ (x : σ → R), (∀ (i : σ), x i ∈ S i) → (MvPolynomial.eval x) P = 0) → P = 0
-- Mathlib.Data.Seq.Computation
/-- `LiftRel R ca cb` is a generalization of `Equiv` to relations other than
equality. It asserts that if `ca` terminates with `a`, then `cb` terminates with
some `b` such that `R a b`, and if `cb` terminates with `b` then `ca` terminates
with some `a` such that `R a b`.  -/
Computation.LiftRel : {α : Type u} → {β : Type v} → (α → β → Prop) → Computation α → Computation β → Prop
-- Lean.PrettyPrinter.Delaborator.Builtins
Lean.PrettyPrinter.Delaborator.AppImplicitArg.regular.sizeOf_spec : ∀ (s : Lean.Term), sizeOf (Lean.PrettyPrinter.Delaborator.AppImplicitArg.regular s) = 1 + sizeOf s
-- Mathlib.CategoryTheory.Limits.Elements
CategoryTheory.CategoryOfElements.CreatesLimitsAux.liftedConeElement.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor C (Type w)} {I : Type u₁}
  [inst_1 : CategoryTheory.Category.{v₁, u₁} I] [inst_2 : Small.{w, u₁} I] (F : CategoryTheory.Functor I A.Elements)
  [inst_3 : CategoryTheory.Limits.HasLimitsOfShape I C] [inst_4 : CategoryTheory.Limits.PreservesLimitsOfShape I A],
  CategoryTheory.CategoryOfElements.CreatesLimitsAux.liftedConeElement F =
    CategoryTheory.CategoryOfElements.CreatesLimitsAux.liftedConeElement F
-- Mathlib.CategoryTheory.Limits.FinallySmall
CategoryTheory.instInitiallySmallOppositeOfFinallySmall : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] [CategoryTheory.FinallySmall J],
  CategoryTheory.InitiallySmall Jᵒᵖ
-- Mathlib.Algebra.Polynomial.Splits
Polynomial.Splits.natDegree_le_one_of_irreducible : ∀ {R : Type u_1} [inst : CommSemiring R] {f : Polynomial R}, f.Splits → Irreducible f → f.natDegree ≤ 1
-- Init.Data.BitVec.Lemmas
/-- Combine adjacent `~~~ (extractLsb _)'` operations into a single `~~~ (extractLsb _)'`.  -/
BitVec.not_extractLsb'_append_not_extractLsb'_eq_not_extractLsb' : ∀ {w start₂ start₁ len₁ len₂ : ℕ} {x : BitVec w},
  start₂ = start₁ + len₁ →
    ~~~BitVec.extractLsb' start₂ len₂ x ++ ~~~BitVec.extractLsb' start₁ len₁ x =
      BitVec.cast ⋯ (~~~BitVec.extractLsb' start₁ (len₁ + len₂) x)
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
SimplexCategoryGenRel.P_σ.σ : ∀ {n : ℕ} (i : Fin (n + 1)), SimplexCategoryGenRel.P_σ (SimplexCategoryGenRel.σ i)
-- Mathlib.Analysis.Asymptotics.LinearGrowth
LinearGrowth.Real.eventually_atTop_exists_int_between : ∀ {a b : ℝ}, a < b → ∀ᶠ (x : ℝ) in Filter.atTop, ∃ n, a * x ≤ ↑n ∧ ↑n ≤ b * x
-- Mathlib.Combinatorics.Quiver.Cast
Quiver.Hom.cast_heq : ∀ {U : Type u_1} [inst : Quiver U] {u v u' v' : U} (hu : u = u') (hv : v = v') (e : u ⟶ v), Quiver.Hom.cast hu hv e ≍ e