mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Set.Lattice
Set.inter_iUnion₂ : ∀ {α : Type u_1} {ι : Sort u_5} {κ : ι → Sort u_8} (s : Set α) (t : (i : ι) → κ i → Set α),
  s ∩ ⋃ i, ⋃ j, t i j = ⋃ i, ⋃ j, s ∩ t i j
-- Mathlib.Algebra.Algebra.Tower
/-- Any `f : A ≃ₐ[R] B` is also an `S`-algebra isomorphism if the `R`-algebra structure on
`A` and `B` factors via a surjective ring homomorphism `R →+* S`.  -/
AlgEquiv.extendScalarsHomOfSurjective : {R : Type u} →
  {S : Type v} →
    {A : Type w} →
      [inst : CommSemiring R] →
        [inst_1 : CommSemiring S] →
          [inst_2 : Semiring A] →
            [inst_3 : Algebra R S] →
              [inst_4 : Algebra S A] →
                [inst_5 : Algebra R A] →
                  [IsScalarTower R S A] → Function.Surjective ⇑(algebraMap R S) → (A ≃ₐ[R] A) ≃* A ≃ₐ[S] A
-- Mathlib.MeasureTheory.Function.Egorov
MeasureTheory.Egorov.measure_iUnionNotConvergentSeq : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace α} [inst : PseudoEMetricSpace β]
  {μ : MeasureTheory.Measure α} {s : Set α} {ε : ℝ} {f : ι → α → β} {g : α → β} [inst_1 : SemilatticeSup ι]
  [inst_2 : Nonempty ι] [inst_3 : Countable ι] (hε : 0 < ε) (hf : ∀ (n : ι), Measurable fun a => edist (f n a) (g a))
  (hsm : MeasurableSet s) (hs : μ s ≠ ⊤)
  (hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Filter.Tendsto (fun n => f n x) Filter.atTop (nhds (g x))),
  μ (MeasureTheory.Egorov.iUnionNotConvergentSeq hε hf hsm hs hfg) ≤ ENNReal.ofReal ε
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.iSup_mem : ∀ {ι : Sort u_1} {α : Type u_2} [inst : CompleteBooleanAlgebra α] {L : BooleanSubalgebra α} {f : ι → α} [Finite ι],
  (∀ (i : ι), f i ∈ L) → ⨆ i, f i ∈ L
-- Std.Tactic.BVDecide.LRAT.Internal.LRATChecker
Std.Tactic.BVDecide.LRAT.Internal.Result.rupFailure.sizeOf_spec : sizeOf Std.Tactic.BVDecide.LRAT.Internal.Result.rupFailure = 1
-- Mathlib.Algebra.Homology.ComplexShapeSigns
/-- A total complex shape symmetry contains the data and properties which allow the
identification of the two total complex functors
`HomologicalComplex₂ C c₁ c₂ ⥤ HomologicalComplex C c₁₂`
and `HomologicalComplex₂ C c₂ c₁ ⥤ HomologicalComplex C c₁₂` via the flip.  -/
TotalComplexShapeSymmetry : {I₁ : Type u_1} →
  {I₂ : Type u_2} →
    {I₁₂ : Type u_4} →
      (c₁ : ComplexShape I₁) →
        (c₂ : ComplexShape I₂) →
          (c₁₂ : ComplexShape I₁₂) → [TotalComplexShape c₁ c₂ c₁₂] → [TotalComplexShape c₂ c₁ c₁₂] → Type (max u_1 u_2)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKey_union_of_mem_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : α → Type v} {m₁ m₂ : Std.DHashMap.Raw α β}
  [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} (mem : k ∈ m₂),
  (m₁ ∪ m₂).getKey k ⋯ = m₂.getKey k mem
-- Mathlib.Topology.Order.Real
ENNReal.instT5Space : T5Space ENNReal
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.instMulActionOfMulActionHomClass : {R : Type u_1} →
  {ι : Type u_2} →
    [inst : Preorder ι] →
      {G : ι → Type u_3} →
        {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} →
          {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} →
            [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] →
              [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] →
                [inst_3 : IsDirectedOrder ι] →
                  [inst_4 : Monoid R] →
                    [inst_5 : (i : ι) → MulAction R (G i)] →
                      [∀ (i j : ι) (h : i ≤ j), MulActionHomClass (T h) R (G i) (G j)] → MulAction R (DirectLimit G f)
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
LinearIsometry.intervalIntegral_comp_comm : ∀ {𝕜 : Type u_2} {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b : ℝ}
  {μ : MeasureTheory.Measure ℝ} [inst_2 : RCLike 𝕜] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 E]
  [inst_5 : NormedSpace 𝕜 F] [inst_6 : NormedSpace ℝ F] [CompleteSpace E] [CompleteSpace F] (L : E →ₗᵢ[𝕜] F)
  (f : ℝ → E), ∫ (x : ℝ) in a..b, L (f x) ∂μ = L (∫ (x : ℝ) in a..b, f x ∂μ)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
WeierstrassCurve.Jacobian.nonsingularLift_some : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} (a b : R),
  W'.NonsingularLift ⟦![a, b, 1]⟧ ↔ W'.toAffine.Nonsingular a b
-- Mathlib.Analysis.Fourier.FourierTransform
Real.fourierIntegral_convergent_iff : ∀ {V : Type u_1} {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [inst_2 : NormedAddCommGroup V]
  [inst_3 : InnerProductSpace ℝ V] [inst_4 : MeasurableSpace V] [BorelSpace V] {μ : MeasureTheory.Measure V} {f : V → E}
  (w : V), MeasureTheory.Integrable (fun v => Real.fourierChar (-inner ℝ v w) • f v) μ ↔ MeasureTheory.Integrable f μ
-- Mathlib.LinearAlgebra.Matrix.PosDef
Matrix.posSemidef_sum : ∀ {n : Type u_2} {R : Type u_3} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] {ι : Type u_5}
  [AddLeftMono R] {x : ι → Matrix n n R} (s : Finset ι), (∀ i ∈ s, (x i).PosSemidef) → (∑ i ∈ s, x i).PosSemidef
-- Mathlib.RingTheory.LocalProperties.Submodule
Module.eq_zero_of_isLocalized_span : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (s : Set R),
  Ideal.span s = ⊤ →
    ∀ (Mₚ : ↑s → Type u_5) [inst_3 : (r : ↑s) → AddCommMonoid (Mₚ r)] [inst_4 : (r : ↑s) → Module R (Mₚ r)]
      (f : (r : ↑s) → M →ₗ[R] Mₚ r) [∀ (r : ↑s), IsLocalizedModule.Away (↑r) (f r)] (x : M),
      (∀ (r : ↑s), (f r) x = 0) → x = 0
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.isEmpty_filter_eq_false_iff : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {f : (a : α) → β a → Bool},
  (Std.DTreeMap.filter f t).isEmpty = false ↔ ∃ k, ∃ (h : k ∈ t), f k (t.get k h) = true
-- Mathlib.CategoryTheory.Sites.Types
/-- Given a sheaf `S`, construct an isomorphism `S ≅ [-, S(*)]`.  -/
CategoryTheory.equivYoneda' : (S : CategoryTheory.Sheaf CategoryTheory.typesGrothendieckTopology (Type u)) →
  S ≅ CategoryTheory.yoneda'.obj (S.obj.obj (Opposite.op PUnit.{u + 1}))
-- Mathlib.Combinatorics.Graph.Subgraph
Graph.IsNonloopAt.mono : ∀ {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G H : Graph α β}, H ≤ G → H.IsNonloopAt e x → G.IsNonloopAt e x
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.coe_neg : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : AddGroup β]
  [inst_3 : IsTopologicalAddGroup β] (f : CompactlySupportedContinuousMap α β), ⇑(-f) = -⇑f
-- Mathlib.CategoryTheory.Limits.FunctorCategory.EpiMono
CategoryTheory.instEpiAppOfFunctor : ∀ {K : Type u} [inst : CategoryTheory.Category.{v, u} K] {C : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} C]
  {F G : CategoryTheory.Functor K C} (f : F ⟶ G) [CategoryTheory.Limits.HasPushouts C] [CategoryTheory.Epi f] (k : K),
  CategoryTheory.Epi (f.app k)
-- Std.Data.DHashMap.Internal.Model
Std.DHashMap.Internal.Raw₀.Const.alterₘ.eq_1 : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] (m : Std.DHashMap.Internal.Raw₀ α fun x => β) (a : α)
  (f : Option β → Option β),
  Std.DHashMap.Internal.Raw₀.Const.alterₘ m a f =
    if h : m.containsₘ a = true then
      let buckets' :=
        Std.DHashMap.Internal.updateBucket (↑m).buckets ⋯ a fun l => Std.DHashMap.Internal.AssocList.Const.alter a f l;
      have size' :=
        if Std.DHashMap.Internal.Raw₀.containsₘ ⟨Std.DHashMap.Internal.withComputedSize buckets', ⋯⟩ a = true then
          (↑m).size
        else (↑m).size - 1;
      ⟨{ size := size', buckets := buckets' }, ⋯⟩
    else
      match f none with
      | none => m
      | some b => (m.consₘ a b).expandIfNecessary
-- Mathlib.Topology.Closure
subset_closure_inter_union_closure_compl_right : ∀ {X : Type u} [inst : TopologicalSpace X] {s t : Set X}, closure s ⊆ closure (s ∩ t) ∪ closure tᶜ
-- Std.Do.WP.SimpLemmas
Std.Do.WP.throw_ExceptT : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {ε α : Type u} {e : ε}
  {Q : Std.Do.PostCond α (Std.Do.PostShape.except ε ps)} [inst : Monad m] [inst_1 : Std.Do.WPMonad m ps],
  (Std.Do.wp (MonadExceptOf.throw e)).apply Q = Q.2.1 e
-- Mathlib.Order.Bounds.Image
Antitone.mem_lowerBounds_image : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  Antitone f → ∀ {a : α} {s : Set α}, a ∈ upperBounds s → f a ∈ lowerBounds (f '' s)
-- Mathlib.CategoryTheory.Functor.Currying
CategoryTheory.Functor.whiskeringRight₂_obj_obj_map_app : ∀ (B : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} B] (C : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} C]
  (D : Type u₃) [inst_2 : CategoryTheory.Category.{v₃, u₃} D] (E : Type u₄)
  [inst_3 : CategoryTheory.Category.{v₄, u₄} E] (X : CategoryTheory.Functor C (CategoryTheory.Functor D E))
  (X_1 : CategoryTheory.Functor B C) {X_2 Y : CategoryTheory.Functor B D} (g : X_2 ⟶ Y) (X_3 : B),
  ((((CategoryTheory.Functor.whiskeringRight₂ B C D E).obj X).obj X_1).map g).app X_3 =
    (X.obj (X_1.obj X_3)).map (g.app X_3)
-- Mathlib.Order.Completion
DedekindCut.image_left_subset_lowerBounds : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  Monotone f → ∀ (A : DedekindCut α), f '' A.left ⊆ lowerBounds (f '' A.right)
-- Mathlib.Order.SuccPred.Archimedean
instIsSuccArchimedeanOrderDualOfIsPredArchimedean : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : PredOrder α] [IsPredArchimedean α], IsSuccArchimedean αᵒᵈ
-- Mathlib.Dynamics.BirkhoffSum.Average
birkhoffAverage_zero' : ∀ (R : Type u_1) {α : Type u_2} {M : Type u_3} [inst : DivisionSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] (f : α → α) (g : α → M), birkhoffAverage R f g 0 = 0
-- Batteries.Tactic.GeneralizeProofs
/-- Main loop for `Lean.MVarId.generalizeProofs`.
The `fvars` array is the array of fvars to generalize proofs for,
and `rfvars` is the array of fvars that have been reverted.
The `g` metavariable has all of these fvars reverted.
 -/
Batteries.Tactic.GeneralizeProofs.generalizeProofsCore : Lean.MVarId →
  Array Lean.FVarId → Array Lean.FVarId → Bool → Batteries.Tactic.GeneralizeProofs.MGen (Array Lean.Expr × Lean.MVarId)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
/-- An abbreviation for a Weierstrass curve in projective coordinates.  -/
WeierstrassCurve.Projective : Type r → Type r
-- Std.Time.Time.Unit.Nanosecond
Std.Time.Nanosecond.instInhabitedOrdinal : Inhabited Std.Time.Nanosecond.Ordinal
-- Mathlib.Data.ZMod.Basic
_private.Mathlib.Data.ZMod.Basic.0.ZMod.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (n : ℕ) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match n.succ with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_2 n
-- Batteries.Recycling.RBTree.Basic
/-- The stream is empty.  -/
RBTree.RBNode.Stream.nil : {α : Type u_1} → RBTree.RBNode.Stream α
-- Mathlib.Topology.Connected.Clopen
connectedSpace_iff_clopen : ∀ {α : Type u} [inst : TopologicalSpace α],
  ConnectedSpace α ↔ Nonempty α ∧ ∀ (s : Set α), IsClopen s → s = ∅ ∨ s = Set.univ
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.nextCoeff_of_natDegree_pos : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, 0 < p.natDegree → p.nextCoeff = p.coeff (p.natDegree - 1)
-- Lean.Data.PersistentArray
Lean.PersistentArray.mk.injEq : ∀ {α : Type u} (root : Lean.PersistentArrayNode α) (tail : Array α) (size : ℕ) (shift : USize) (tailOff : ℕ)
  (root_1 : Lean.PersistentArrayNode α) (tail_1 : Array α) (size_1 : ℕ) (shift_1 : USize) (tailOff_1 : ℕ),
  ({ root := root, tail := tail, size := size, shift := shift, tailOff := tailOff } =
      { root := root_1, tail := tail_1, size := size_1, shift := shift_1, tailOff := tailOff_1 }) =
    (root = root_1 ∧ tail = tail_1 ∧ size = size_1 ∧ shift = shift_1 ∧ tailOff = tailOff_1)
-- Mathlib.Combinatorics.SimpleGraph.Maps
/-- A graph isomorphism induces an equivalence of neighbor sets.  -/
SimpleGraph.Iso.mapNeighborSet : {V : Type u_1} →
  {W : Type u_2} →
    {G : SimpleGraph V} → {G' : SimpleGraph W} → (f : G ≃g G') → (v : V) → ↑(G.neighborSet v) ≃ ↑(G'.neighborSet (f v))
-- Mathlib.Algebra.Group.Hom.Basic
AddHom.add_comp : ∀ {M : Type u_2} {N : Type u_3} {P : Type u_4} [inst : Add M] [inst_1 : Add N] [inst_2 : AddCommSemigroup P]
  (g₁ g₂ : N →ₙ+ P) (f : M →ₙ+ N), (g₁ + g₂).comp f = g₁.comp f + g₂.comp f
-- Init.Data.BitVec.Lemmas
BitVec.ofBool_eq_iff_eq : ∀ {b b' : Bool}, BitVec.ofBool b = BitVec.ofBool b' ↔ b = b'
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.instInhabitedSplitInfo.default : Lean.Meta.Grind.SplitInfo
-- Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Polynomial.natTrailingDegree_eq_zero : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p.natTrailingDegree = 0 ↔ p = 0 ∨ p.coeff 0 ≠ 0
-- Init.Data.UInt.Lemmas
UInt16.instLawfulOrderLT : Std.LawfulOrderLT UInt16
-- Mathlib.LinearAlgebra.FreeModule.ModN
/-- The universal property of `ModN G n` in terms of monoids: Monoid homomorphisms from `ModN G n`
are the same as monoid homomorphisms from `G` whose values are `n`-torsion.  -/
ModN.liftEquiv : {G : Type u_1} →
  {M : Type u_3} →
    [inst : AddCommGroup G] → {n : ℕ} → [inst_1 : AddMonoid M] → (ModN G n →+ M) ≃ { φ // ∀ (g : G), n • φ g = 0 }
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
/-- The "left" map `Y ⟶ Z`.  -/
CategoryTheory.IsRegularMono.left : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y : C} → (f : X ⟶ Y) → [inst_1 : CategoryTheory.IsRegularMono f] → Y ⟶ CategoryTheory.IsRegularMono.Z f
-- Lean.Meta.Tactic.Grind.Types
/-- Asserted facts  -/
Lean.Meta.Grind.GoalState.facts : Lean.Meta.Grind.GoalState → Lean.PArray Lean.Expr
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
/-- The coercion from `Finset` to `Set` as a `MonoidHom`.  -/
Finset.coeMonoidHom : {α : Type u_2} → [inst : DecidableEq α] → [inst_1 : MulOneClass α] → Finset α →* Set α
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FlatMap
Std.IterM.step_flatMapAfterM : ∀ {α β α₂ γ : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : MonadAttach m] [inst_2 : LawfulMonad m]
  [WeaklyLawfulMonadAttach m] [inst_4 : Std.Iterator α m β] [inst_5 : Std.Iterator α₂ m γ] {f : β → m (Std.IterM m γ)}
  {it₁ : Std.IterM m β} {it₂ : Option (Std.IterM m γ)},
  (Std.IterM.flatMapAfterM f it₁ it₂).step =
    match it₂ with
    | none => do
      let __do_lift ← it₁.step
      match __do_lift.inflate with
        | ⟨Std.IterStep.yield it₁' b, h⟩ => do
          let fx ← MonadAttach.attach (f b)
          pure (Std.Shrink.deflate (Std.PlausibleIterStep.skip (Std.IterM.flatMapAfterM f it₁' (some ↑fx)) ⋯))
        | ⟨Std.IterStep.skip it₁', h⟩ =>
          pure (Std.Shrink.deflate (Std.PlausibleIterStep.skip (Std.IterM.flatMapAfterM f it₁' none) ⋯))
        | ⟨Std.IterStep.done, h⟩ => pure (Std.Shrink.deflate (Std.PlausibleIterStep.done ⋯))
    | some it₂ => do
      let __do_lift ← it₂.step
      match __do_lift.inflate with
        | ⟨Std.IterStep.yield it₂' out, h⟩ =>
          pure (Std.Shrink.deflate (Std.PlausibleIterStep.yield (Std.IterM.flatMapAfterM f it₁ (some it₂')) out ⋯))
        | ⟨Std.IterStep.skip it₂', h⟩ =>
          pure (Std.Shrink.deflate (Std.PlausibleIterStep.skip (Std.IterM.flatMapAfterM f it₁ (some it₂')) ⋯))
        | ⟨Std.IterStep.done, h⟩ =>
          pure (Std.Shrink.deflate (Std.PlausibleIterStep.skip (Std.IterM.flatMapAfterM f it₁ none) ⋯))
-- Mathlib.RingTheory.Invariant.Basic
IsFractionRing.stabilizerHom_apply_apply_mk : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] (G : Type u_3)
  [inst_3 : Group G] [inst_4 : MulSemiringAction G B] [inst_5 : SMulCommClass G A B] (P : Ideal A) (Q : Ideal B)
  [inst_6 : Q.LiesOver P] (K : Type u_4) (L : Type u_5) [inst_7 : Field K] [inst_8 : Field L]
  [inst_9 : Algebra (A ⧸ P) K] [inst_10 : Algebra (B ⧸ Q) L] [inst_11 : Algebra (A ⧸ P) L]
  [inst_12 : IsScalarTower (A ⧸ P) (B ⧸ Q) L] [inst_13 : Algebra K L] [inst_14 : IsScalarTower (A ⧸ P) K L]
  [inst_15 : IsFractionRing (A ⧸ P) K] [inst_16 : IsFractionRing (B ⧸ Q) L] (σ : ↥(MulAction.stabilizer G Q)) (x : B),
  ((IsFractionRing.stabilizerHom G P Q K L) σ) ((algebraMap (B ⧸ Q) L) ((Ideal.Quotient.mk Q) x)) =
    (algebraMap (B ⧸ Q) L) ((Ideal.Quotient.mk Q) (↑σ • x))
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.minEntry!_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited ((a : α) × β a)], t₁.Equiv t₂ → t₁.minEntry! = t₂.minEntry!
-- Mathlib.CategoryTheory.Action.Monoidal
/-- If `V` is left rigid, so is `Action V G`.  -/
Action.instLeftRigidCategory : (V : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    [inst_1 : CategoryTheory.MonoidalCategory V] →
      (H : Type u_3) →
        [inst_2 : Group H] → [CategoryTheory.LeftRigidCategory V] → CategoryTheory.LeftRigidCategory (Action V H)
-- Mathlib.Data.Multiset.Powerset
Multiset.powersetCardAux_perm : ∀ {α : Type u_1} {n : ℕ} {l₁ l₂ : List α},
  l₁.Perm l₂ → (Multiset.powersetCardAux n l₁).Perm (Multiset.powersetCardAux n l₂)
-- Mathlib.Algebra.Module.Equiv.Basic
/-- Each element of the group defines a linear equivalence.

This is a stronger version of `DistribMulAction.toAddEquiv`.  -/
DistribMulAction.toLinearEquiv : (R : Type u_1) →
  {S : Type u_4} →
    (M : Type u_5) →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : Module R M] →
            [inst_3 : Group S] → [inst_4 : DistribMulAction S M] → [SMulCommClass S R M] → S → M ≃ₗ[R] M
-- Mathlib.Algebra.Group.Defs
isCancelAdd_iff_forall_isAddRegular : ∀ {R : Type u_2} [inst : Add R], IsCancelAdd R ↔ ∀ (r : R), IsAddRegular r
-- Mathlib.CategoryTheory.Sites.Coverage
CategoryTheory.Presheaf.isSheaf_iff_isLimit_coverage : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (K : CategoryTheory.Coverage C) (P : CategoryTheory.Functor Cᵒᵖ D),
  CategoryTheory.Presheaf.IsSheaf K.toGrothendieck P ↔
    ∀ ⦃X : C⦄,
      ∀ R ∈ K.coverings X,
        Nonempty (CategoryTheory.Limits.IsLimit (P.mapCone (CategoryTheory.Sieve.generate R).arrows.cocone.op))
-- Mathlib.Algebra.Lie.TransferInstance
LinearEquiv.lieEquiv_apply : ∀ {R : Type u_1} {M : Type u_2} {L : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : LieRing L] [inst_4 : LieAlgebra R L] (e : M ≃ₗ[R] L) (a : M), (LinearEquiv.lieEquiv R e) a = e a
-- Mathlib.GroupTheory.IsSubnormal
_private.Mathlib.GroupTheory.IsSubnormal.0.Subgroup.IsSubnormal.isSubnormal_iff.match_1_1.splitter : (motive : ℕ → Sort u_1) → (x : ℕ) → (Unit → motive 0) → ((n : ℕ) → motive n.succ) → motive x
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
_private.Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex.0.SSet.stdSimplex.bijective_image_objEquiv_toOrderHom_univ : ∀ (n m : ℕ),
  Function.Bijective fun x =>
    match x with
    | ⟨x, hx⟩ => ⟨Finset.image (⇑(SimplexCategory.Hom.toOrderHom (SSet.stdSimplex.objEquiv x))) Finset.univ, ⋯⟩
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.inter_sub_subset : ∀ {α : Type u_2} [inst : Sub α] {s₁ s₂ t : Set α}, s₁ ∩ s₂ - t ⊆ (s₁ - t) ∩ (s₂ - t)
-- Init.Data.Option.Attach
Option.toArray_attachWith : ∀ {α : Type u_1} {p : α → Prop} {o : Option α} {h : ∀ (x : α), o = some x → p x},
  (o.attachWith p h).toArray = Array.map (fun x => ⟨↑x, ⋯⟩) o.toArray.attach
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.DocumentSymbol.brecOn_2.eq : ∀ {motive_1 : Lean.Lsp.DocumentSymbol → Sort u} {motive_2 : Lean.Lsp.DocumentSymbolAux Lean.Lsp.DocumentSymbol → Sort u}
  {motive_3 : Option (Array Lean.Lsp.DocumentSymbol) → Sort u} {motive_4 : Array Lean.Lsp.DocumentSymbol → Sort u}
  {motive_5 : List Lean.Lsp.DocumentSymbol → Sort u} (t : Option (Array Lean.Lsp.DocumentSymbol))
  (F_1 : (t : Lean.Lsp.DocumentSymbol) → t.below → motive_1 t)
  (F_2 : (t : Lean.Lsp.DocumentSymbolAux Lean.Lsp.DocumentSymbol) → Lean.Lsp.DocumentSymbol.below_1 t → motive_2 t)
  (F_3 : (t : Option (Array Lean.Lsp.DocumentSymbol)) → Lean.Lsp.DocumentSymbol.below_2 t → motive_3 t)
  (F_4 : (t : Array Lean.Lsp.DocumentSymbol) → Lean.Lsp.DocumentSymbol.below_3 t → motive_4 t)
  (F_5 : (t : List Lean.Lsp.DocumentSymbol) → Lean.Lsp.DocumentSymbol.below_4 t → motive_5 t),
  Lean.Lsp.DocumentSymbol.brecOn_2 t F_1 F_2 F_3 F_4 F_5 =
    F_3 t (Lean.Lsp.DocumentSymbol.brecOn_2.go t F_1 F_2 F_3 F_4 F_5).2
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq
/-- ```
 X ⊞ Y --fst--> X
   |            |
  snd           0
   |            |
   v            v
   Y -----0---> 0
```
is a bi-Cartesian square.
 -/
CategoryTheory.BicartesianSq.of_has_biproduct₁ : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} [inst_3 : CategoryTheory.Limits.HasBinaryBiproduct X Y],
  CategoryTheory.BicartesianSq CategoryTheory.Limits.biprod.fst CategoryTheory.Limits.biprod.snd 0 0
-- Mathlib.Topology.MetricSpace.Thickening
/-- A point in a metric space belongs to the (open) `δ`-thickening of a subset `E` if and only if
it is at distance less than `δ` from some point of `E`.  -/
Metric.mem_thickening_iff : ∀ {δ : ℝ} {X : Type u} [inst : PseudoMetricSpace X] {E : Set X} {x : X},
  x ∈ Metric.thickening δ E ↔ ∃ z ∈ E, dist x z < δ
-- Mathlib.Data.List.Prime
mem_list_primes_of_dvd_prod : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] [IsCancelMulZero M] [Subsingleton Mˣ] {p : M},
  Prime p → ∀ {L : List M}, (∀ q ∈ L, Prime q) → p ∣ L.prod → p ∈ L
-- Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace
/-- A smooth manifold can be considered as a locally ringed space.  -/
ChartedSpace.locallyRingedSpace : {𝕜 : Type u} →
  [inst : NontriviallyNormedField 𝕜] →
    {EM : Type u_1} →
      [inst_1 : NormedAddCommGroup EM] →
        [inst_2 : NormedSpace 𝕜 EM] →
          {HM : Type u_2} →
            [inst_3 : TopologicalSpace HM] →
              ModelWithCorners 𝕜 EM HM →
                (M : Type u) → [inst : TopologicalSpace M] → [ChartedSpace HM M] → AlgebraicGeometry.LocallyRingedSpace
-- Init.Data.Nat.Sqrt.Basic
/-- Auxiliary for `sqrt`. If `guess` is greater than the integer square root of `n`,
returns the integer square root of `n`.  -/
Nat.sqrt.iter : ℕ → ℕ → ℕ
-- Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
HomotopicalAlgebra.BifibrantObject.congr_simp : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithCofibrations C]
  [inst_2 : CategoryTheory.Limits.HasInitial C] [inst_3 : HomotopicalAlgebra.CategoryWithFibrations C]
  [inst_4 : CategoryTheory.Limits.HasTerminal C],
  HomotopicalAlgebra.BifibrantObject C = HomotopicalAlgebra.BifibrantObject C
-- Mathlib.Algebra.Category.Semigrp.Basic
MagmaCat.hom_comp : ∀ {M N T : MagmaCat} (f : M ⟶ N) (g : N ⟶ T),
  MagmaCat.Hom.hom (CategoryTheory.CategoryStruct.comp f g) = (MagmaCat.Hom.hom g).comp (MagmaCat.Hom.hom f)
-- Mathlib.Analysis.RCLike.Basic
RCLike.toZeroLEOneClass : ∀ {K : Type u_1} [inst : RCLike K], ZeroLEOneClass K
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Measurable.nnreal_mk : ∀ {α : Type u_1} {mα : MeasurableSpace α} {f : α → ℝ},
  Measurable f → ∀ {h'f : ∀ (x : α), 0 ≤ f x}, Measurable fun x => NNReal.mk (f x) ⋯
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roo.size_toArray : ∀ {α : Type u} {r : Std.Roo α} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.Rxo.HasSize α] [inst_4 : Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLT α]
  [inst_6 : Std.Rxo.IsAlwaysFinite α] [Std.Rxo.LawfulHasSize α], r.toArray.size = r.size
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
ProjectiveSpectrum.isPrime : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubmonoidClass σ A] {𝒜 : ℕ → σ}
  [inst_3 : GradedRing 𝒜] (self : ProjectiveSpectrum 𝒜), self.asHomogeneousIdeal.toIdeal.IsPrime
-- Mathlib.Combinatorics.Enumerative.Partition.Basic
/-- The finset of those partitions in which every part is used less than `m` times.  -/
Nat.Partition.countRestricted : (n : ℕ) → ℕ → Finset n.Partition