mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.Context.mk.sizeOf_spec : ∀ (declName? : Option Lean.Name) (macroStack : Lean.Elab.MacroStack) (mayPostpone errToSorry : Bool)
  (autoBoundImplicitContext : Option Lean.Elab.AutoBoundImplicitContext) (autoBoundImplicitForbidden : Lean.Name → Bool)
  (sectionVars : Lean.NameMap Lean.Name) (sectionFVars : Lean.NameMap Lean.Expr)
  (implicitLambda heedElabAsElim isNoncomputableSection isMetaSection ignoreTCFailures inPattern : Bool)
  (tacSnap? : Option (Lean.Language.SnapshotBundle Lean.Elab.Tactic.TacticParsedSnapshot))
  (saveRecAppSyntax holesAsSyntheticOpaque checkDeprecated : Bool)
  (fixedTermElabs : Array Lean.Elab.Term.FixedTermElabRef),
  sizeOf
      { declName? := declName?, macroStack := macroStack, mayPostpone := mayPostpone, errToSorry := errToSorry,
        autoBoundImplicitContext := autoBoundImplicitContext, autoBoundImplicitForbidden := autoBoundImplicitForbidden,
        sectionVars := sectionVars, sectionFVars := sectionFVars, implicitLambda := implicitLambda,
        heedElabAsElim := heedElabAsElim, isNoncomputableSection := isNoncomputableSection,
        isMetaSection := isMetaSection, ignoreTCFailures := ignoreTCFailures, inPattern := inPattern,
        tacSnap? := tacSnap?, saveRecAppSyntax := saveRecAppSyntax, holesAsSyntheticOpaque := holesAsSyntheticOpaque,
        checkDeprecated := checkDeprecated, fixedTermElabs := fixedTermElabs } =
    1 + sizeOf declName? + sizeOf macroStack + sizeOf mayPostpone + sizeOf errToSorry +
                                sizeOf autoBoundImplicitContext +
                              sizeOf sectionVars +
                            sizeOf sectionFVars +
                          sizeOf implicitLambda +
                        sizeOf heedElabAsElim +
                      sizeOf isNoncomputableSection +
                    sizeOf isMetaSection +
                  sizeOf ignoreTCFailures +
                sizeOf inPattern +
              sizeOf tacSnap? +
            sizeOf saveRecAppSyntax +
          sizeOf holesAsSyntheticOpaque +
        sizeOf checkDeprecated +
      sizeOf fixedTermElabs
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.maxKey?_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {km : α}, t.maxKey? = some km → km ∈ t
-- Mathlib.AlgebraicTopology.SimplicialSet.Horn
SSet.horn.yonedaEquiv_ι : ∀ {n : ℕ} (i j : Fin (n + 2)) (hij : j ≠ i), SSet.yonedaEquiv (SSet.horn.ι i j hij) = SSet.horn.face i j hij
-- Aesop.RuleSet.Filter
Aesop.RuleFilter.mk.injEq : ∀ (name : Lean.Name) (scope : Aesop.ScopeName) (builders : Array Aesop.BuilderName) (phases : Array Aesop.PhaseName)
  (name_1 : Lean.Name) (scope_1 : Aesop.ScopeName) (builders_1 : Array Aesop.BuilderName)
  (phases_1 : Array Aesop.PhaseName),
  ({ name := name, scope := scope, builders := builders, phases := phases } =
      { name := name_1, scope := scope_1, builders := builders_1, phases := phases_1 }) =
    (name = name_1 ∧ scope = scope_1 ∧ builders = builders_1 ∧ phases = phases_1)
-- Mathlib.Topology.Homotopy.HomotopyGroup
HomotopyGroup.isUnital_auxGroup : ∀ {N : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {x : X} [inst_1 : DecidableEq N] (i : N),
  EckmannHilton.IsUnital Mul.mul ⟦GenLoop.const⟧
-- Std.Time.Format.Modifier
Std.Time.Modifier.G.inj : ∀ {presentation presentation_1 : Std.Time.Text},
  Std.Time.Modifier.G presentation = Std.Time.Modifier.G presentation_1 → presentation = presentation_1
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.toAlgHom_toLinearMap : ∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Semiring A₂]
  [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂] (e : A₁ ≃ₐ[R] A₂), (↑e).toLinearMap = ↑↑e
-- Mathlib.Algebra.Module.Presentation.Basic
Module.Relations.Solution.surjective_fromQuotient_iff_surjective_π : ∀ {A : Type u} [inst : Ring A] {relations : Module.Relations A} {M : Type v} [inst_1 : AddCommGroup M]
  [inst_2 : Module A M] (solution : relations.Solution M),
  Function.Surjective ⇑solution.fromQuotient ↔ Function.Surjective ⇑solution.π
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.reorder : Lean.Meta.Grind.Arith.Cutsat.DvdCnstr → Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof
-- Mathlib.RepresentationTheory.Character
Representation.card_inv_mul_sum_char_eq_finrank : ∀ {G : Type u_1} {k : Type u_2} {V : Type u_3} [inst : Group G] [inst_1 : Field k] [inst_2 : AddCommGroup V]
  [inst_3 : Module k V] [FiniteDimensional k V] (ρ : Representation k G V) [inst_5 : Fintype G]
  [Invertible ↑(Nat.card G)], (↑(Nat.card G))⁻¹ * ∑ g, ρ.character g = ↑(Module.finrank k ↥ρ.invariants)
-- Init.Data.Nat.Lemmas
Nat.min_self_assoc : ∀ {m n : ℕ}, min m (min m n) = min m n
-- Mathlib.Combinatorics.Graph.Delete
Graph.restrict_eq_deleteEdges : ∀ {α : Type u_1} {β : Type u_2} (G : Graph α β) (F : Set β), G.restrict F = G.deleteEdges (G.edgeSet \ F)
-- Mathlib.RingTheory.WittVector.Truncated
/-- Create a `TruncatedWittVector` from a vector `x`.  -/
TruncatedWittVector.mk : (p : ℕ) → {n : ℕ} → {R : Type u_1} → (Fin n → R) → TruncatedWittVector p n R
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.pred_ok : ∀ (q₁ q₂ : Turing.PartrecToTM2.Λ') (s : Option Turing.PartrecToTM2.Γ') (v : List ℕ) (c d : List Turing.PartrecToTM2.Γ'),
  ∃ s',
    StateTransition.Reaches₁ (Turing.TM2.step Turing.PartrecToTM2.tr)
      { l := some (q₁.pred q₂), var := s, stk := Turing.PartrecToTM2.K'.elim (Turing.PartrecToTM2.trList v) [] c d }
      (Nat.rec
        { l := some q₁, var := s', stk := Turing.PartrecToTM2.K'.elim (Turing.PartrecToTM2.trList v.tail) [] c d }
        (fun n x =>
          { l := some q₂, var := s',
            stk := Turing.PartrecToTM2.K'.elim (Turing.PartrecToTM2.trList (n :: v.tail)) [] c d })
        v.headI)
-- Mathlib.Combinatorics.Matroid.Map
Matroid.Indep.map : ∀ {α : Type u_1} {β : Type u_2} {I : Set α} {M : Matroid α},
  M.Indep I → ∀ (f : α → β) (hf : Set.InjOn f M.E), (M.map f hf).Indep (f '' I)
-- Mathlib.Analysis.InnerProductSpace.Basic
inner_eq_norm_sq_left_iff : ∀ {F : Type u_3} [inst : SeminormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] {v w : F},
  inner ℝ v w = ‖v‖ ^ 2 ↔ inner ℝ v (v - w) = 0
-- Mathlib.Topology.Bornology.Absorbs
Absorbent.absorbs : ∀ {M : Type u_1} {α : Type u_2} [inst : Bornology M] [inst_1 : SMul M α] {s : Set α},
  Absorbent M s → ∀ {x : α}, Absorbs M s {x}
-- Mathlib.Topology.Constructions
/-- Continuous maps between `ULift X` and `ULift Y` are equivalent to continuous maps between `X`
and `Y`.  -/
ContinuousMap.uliftEquiv : (X : Type u) →
  (Y : Type v) →
    [inst : TopologicalSpace X] → [inst_1 : TopologicalSpace Y] → C(ULift.{v, u} X, ULift.{u, v} Y) ≃ C(X, Y)
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
/-- **Alias** of the reverse direction of `lt_sub_iff_add_lt'`. -/
lt_sub_left_of_add_lt : ∀ {α : Type u} [inst : AddCommGroup α] [inst_1 : LT α] [AddLeftStrictMono α] {a b c : α}, a + b < c → b < c - a
-- Mathlib.Algebra.Star.Subalgebra
StarAlgebra.subset_adjoin : ∀ (R : Type u_2) {A : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] [inst_4 : StarRing A] [inst_5 : StarModule R A] (s : Set A), s ⊆ ↑(StarAlgebra.adjoin R s)
-- Mathlib.Algebra.Order.ZeroLEOne
/-- Zero is less than or equal to one.  -/
ZeroLEOneClass.zero_le_one : ∀ {α : Type u_2} {inst : Zero α} {inst_1 : One α} {inst_2 : LE α} [self : ZeroLEOneClass α], 0 ≤ 1
-- Lean.Language.Basic
/-- Applies the current `SnapshotTreeTransform` to a `Snapshot`.  -/
Lean.Language.Snapshot.transform : Lean.Language.Snapshot → Lean.Language.ToSnapshotTreeM Lean.Language.Snapshot
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Connected
/-- Let `F` and `G` be two diagrams indexed by a connected `I`, and `X` and `Y` be two cocones over
`F` and `G` respectively, with maps `α : F ⟶ G` and `f : X ⟶ Y` that commutes with the cocone maps.
Suppose `Y = X ⨿[F i] G i` for all `i` and `Y = colim G`, then `X = colim F`.
 -/
CategoryTheory.Limits.isColimitOfIsPushoutOfIsConnected : {I : Type u_1} →
  {C : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} I] →
      [CategoryTheory.IsConnected I] →
        [inst_2 : CategoryTheory.Category.{v_2, u_2} C] →
          {F G : CategoryTheory.Functor I C} →
            (α : F ⟶ G) →
              (cF : CategoryTheory.Limits.Cocone F) →
                (cG : CategoryTheory.Limits.Cocone G) →
                  (f : cF ⟶ (CategoryTheory.Limits.Cocone.precompose α).obj cG) →
                    (∀ (i : I), CategoryTheory.IsPushout (cF.ι.app i) (α.app i) f.hom (cG.ι.app i)) →
                      CategoryTheory.Limits.IsColimit cF → CategoryTheory.Limits.IsColimit cG
-- Mathlib.Analysis.Calculus.VectorField
/-- The differentiation operator along `[W, V]`
is the commutator of the differentiation operators along `W` and `V`.  -/
VectorField.fderiv_apply_lieBracket_of_isSymmSndFDerivAt : ∀ {𝕜 : 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] {V W : E → E}
  {x : E} {f : E → F},
  ContDiffAt 𝕜 2 f x →
    IsSymmSndFDerivAt 𝕜 f x →
      DifferentiableAt 𝕜 W x →
        DifferentiableAt 𝕜 V x →
          (fderiv 𝕜 f x) (VectorField.lieBracket 𝕜 V W x) =
            (fderiv 𝕜 (fun x => (fderiv 𝕜 f x) (W x)) x) (V x) - (fderiv 𝕜 (fun x => (fderiv 𝕜 f x) (V x)) x) (W x)
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
_private.Mathlib.Analysis.Distribution.SchwartzSpace.Basic.0.SchwartzMap.seminormAux_nonneg : ∀ {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 : SchwartzMap E F), 0 ≤ SchwartzMap.seminormAux✝ k n f
-- Mathlib.GroupTheory.Congruence.Defs
Con.le_comap_conGen : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] (r : N → N → Prop) (f : M → N)
  (hf : ∀ (x y : M), f (x * y) = f x * f y), conGen (Function.onFun r f) ≤ Con.comap f hf (conGen r)
-- Init.Data.Char.Lemmas
Char.ltIrrefl : Std.Irrefl fun x1 x2 => x1 < x2
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.coeffs_C_subset : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] (r : R), (MvPolynomial.C r).coeffs ⊆ {r}
-- Mathlib.AlgebraicGeometry.Morphisms.Constructors
/-- If a property of maps of topological spaces is stable under composition, the induced
morphism property of schemes is stable under composition.  -/
AlgebraicGeometry.topologically_isStableUnderComposition : ∀ (P : {α β : Type u} → [TopologicalSpace α] → [TopologicalSpace β] → (α → β) → Prop),
  (∀ {α β γ : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : TopologicalSpace γ]
      (f : α → β) (g : β → γ), P f → P g → P (g ∘ f)) →
    (AlgebraicGeometry.topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] => P).IsStableUnderComposition
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.minEntry!.eq_3 : ∀ {α : Type u} {β : Type v} [inst : Inhabited (α × β)] (size : ℕ) (k : α) (v : β) (size_1 : ℕ) (k_1 : α) (v_1 : β)
  (l r r_1 : Std.DTreeMap.Internal.Impl α fun x => β),
  Std.DTreeMap.Internal.Impl.Const.minEntry!
      (Std.DTreeMap.Internal.Impl.inner size k v (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) r_1) =
    Std.DTreeMap.Internal.Impl.Const.minEntry! (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r)
-- Std.Data.DTreeMap.Basic
/-- Tries to retrieve the key-value pair with the smallest key that is greater than or equal to the
given key, panicking if no such pair exists.
 -/
Std.DTreeMap.Const.getEntryGE! : {α : Type u} →
  {cmp : α → α → Ordering} → {β : Type v} → [Inhabited (α × β)] → Std.DTreeMap α (fun x => β) cmp → α → α × β
-- Mathlib.Tactic.Linarith.Frontend
_private.Mathlib.Tactic.Linarith.Frontend.0.Mathlib.Tactic.minimize : Mathlib.Tactic.Linarith.LinarithConfig →
  Lean.Elab.Tactic.SavedState → Lean.MVarId → List Lean.Expr → ℕ → Lean.Elab.Tactic.TacticM (List Lean.Expr)
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.π_natTransTruncGEOfLE_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (a b : ℤ) (h : a ≤ b) (X : C),
  CategoryTheory.CategoryStruct.comp ((t.truncGEπ a).app X) ((t.natTransTruncGEOfLE a b h).app X) = (t.truncGEπ b).app X
-- Mathlib.Combinatorics.Matroid.Minor.Restrict
Matroid.instPartialOrderMatroidᵣ : {α : Type u_2} → PartialOrder (Matroid.Matroidᵣ α)
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Tactic.ComputeAsymptotics.MultiseriesExpansion.instInhabited : (basis : Tactic.ComputeAsymptotics.Basis) → Inhabited (Tactic.ComputeAsymptotics.MultiseriesExpansion basis)
-- Init.Data.String.Lemmas.Order
String.Pos.offset_lt_rawEndPos_iff : ∀ {s : String} {p : s.Pos}, p.offset < s.rawEndPos ↔ p ≠ s.endPos
-- Mathlib.Probability.UniformOn
ProbabilityTheory.uniformOn.eq_1 : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] (s : Set Ω), ProbabilityTheory.uniformOn s = MeasureTheory.Measure.count[|s]
-- Mathlib.NumberTheory.Padics.PadicNumbers
Padic.norm_eq_of_norm_sub_lt_left : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {z1 z2 : ℚ_[p]}, ‖z1 - z2‖ < ‖z1‖ → ‖z1‖ = ‖z2‖
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Coalgebra.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Functor C C} → (V : C) → (V ⟶ F.obj V) → CategoryTheory.Endofunctor.Coalgebra F
-- Init.Data.Vector.Monadic
_private.Init.Data.Vector.Monadic.0.Vector.forIn'_eq_foldlM.match_1.eq_2 : ∀ {β : Type u_1} (motive : ForInStep β → Sort u_2) (b : β) (h_1 : (b : β) → motive (ForInStep.yield b))
  (h_2 : (b : β) → motive (ForInStep.done b)),
  (match ForInStep.done b with
    | ForInStep.yield b => h_1 b
    | ForInStep.done b => h_2 b) =
    h_2 b
-- Init.Data.Range.Polymorphic.Iterators
Std.Rxi.Iterator.upwardEnumerableLe_of_isPlausibleIndirectOutput : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerable α] {it : Std.Iter α} {out : α},
  it.IsPlausibleIndirectOutput out → ∃ a, it.internalState.next = some a ∧ Std.PRange.UpwardEnumerable.LE a out
-- Std.Sync.Channel
_private.Std.Sync.Channel.0.Std.CloseableChannel.Bounded.incMod_lt : ∀ {idx cap : ℕ}, idx < cap → Std.CloseableChannel.Bounded.incMod✝ idx cap < cap
-- Mathlib.Analysis.BoxIntegral.Integrability
/-- A simple function is McShane integrable w.r.t. any locally finite measure.  -/
MeasureTheory.SimpleFunc.hasBoxIntegral : ∀ {ι : Type u} {E : Type v} [inst : Fintype ι] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E]
  (f : MeasureTheory.SimpleFunc (ι → ℝ) E) (μ : MeasureTheory.Measure (ι → ℝ))
  [inst_3 : MeasureTheory.IsLocallyFiniteMeasure μ] (I : BoxIntegral.Box ι) (l : BoxIntegral.IntegrationParams),
  l.bRiemann = false →
    BoxIntegral.HasIntegral I l (⇑f) μ.toBoxAdditive.toSMul (MeasureTheory.SimpleFunc.integral (μ.restrict ↑I) f)
-- Mathlib.Probability.Independence.Kernel.Indep
ProbabilityTheory.Kernel.indepSets_of_indepSets_of_le_right : ∀ {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {s₁ s₂ s₃ : Set (Set Ω)} {_mΩ : MeasurableSpace Ω}
  {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α},
  ProbabilityTheory.Kernel.IndepSets s₁ s₂ κ μ → s₃ ⊆ s₂ → ProbabilityTheory.Kernel.IndepSets s₁ s₃ κ μ
-- Mathlib.Analysis.SpecialFunctions.Stirling
Stirling.stirlingSeq_zero : Stirling.stirlingSeq 0 = 0
-- Mathlib.Analysis.Complex.Trigonometric
Real.cosh_sub : ∀ (x y : ℝ), Real.cosh (x - y) = Real.cosh x * Real.cosh y - Real.sinh x * Real.sinh y
-- Mathlib.Analysis.Analytic.IteratedFDeriv
/-- If a function has a power series in a ball, then its `n`-th iterated derivative is given by
`(v₁, ..., vₙ) ↦ ∑ pₙ (v_{σ (1)}, ..., v_{σ (n)})` where the sum is over all
permutations of `{1, ..., n}`.  -/
HasFPowerSeriesWithinOnBall.iteratedFDerivWithin_eq_sum_of_completeSpace : ∀ {𝕜 : 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] {f : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} {r : ENNReal} [CompleteSpace F],
  HasFPowerSeriesWithinOnBall f p s x r →
    UniqueDiffOn 𝕜 s →
      x ∈ s → ∀ {n : ℕ} (v : Fin n → E), (iteratedFDerivWithin 𝕜 n f s x) v = ∑ σ, (p n) fun i => v (σ i)
-- Std.Time.Format.DateFormat
/-- `DateFormat` contains locale-specific configuration for date/time formatting and parsing,
combining calendar conventions (e.g. first day of week) with locale symbols.
 -/
Std.Time.DateFormat : Type
-- Mathlib.Order.Filter.SmallSets
Filter.smallSets_neBot : ∀ {α : Type u_1} (l : Filter α), l.smallSets.NeBot
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.incidenceFinset.eq_1 : ∀ {V : Type u_1} (G : SimpleGraph V) (v : V) [inst : Fintype ↑(G.neighborSet v)] [inst_1 : DecidableEq V],
  G.incidenceFinset v = (G.incidenceSet v).toFinset
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.involutiveInv : {α : Type u_2} → [InvolutiveInv α] → InvolutiveInv (Set α)
-- Mathlib.Data.Fintype.EquivFin
/-- Noncomputable equivalence between two finsets `s` and `t` as fintypes when there is a proof
that `#s = #t`.  -/
Finset.equivOfCardEq : {α : Type u_1} → {β : Type u_2} → {s : Finset α} → {t : Finset β} → s.card = t.card → ↥s ≃ ↥t
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Real.borelSpace : BorelSpace ℝ
-- Mathlib.RingTheory.HopkinsLevitzki
IsArtinianRing.eq_1 : ∀ (R : Type u_1) [inst : Semiring R], IsArtinianRing R = IsArtinian R R
-- Init.Grind.ToIntLemmas
_private.Init.Grind.ToIntLemmas.0.Lean.Grind.IntInterval.lo?.match_1.eq_2 : ∀ (motive : Lean.Grind.IntInterval → Sort u_1) (lo : ℤ) (h_1 : (lo hi : ℤ) → motive (Lean.Grind.IntInterval.co lo hi))
  (h_2 : (lo : ℤ) → motive (Lean.Grind.IntInterval.ci lo)) (h_3 : (hi : ℤ) → motive (Lean.Grind.IntInterval.io hi))
  (h_4 : Unit → motive Lean.Grind.IntInterval.ii),
  (match Lean.Grind.IntInterval.ci lo with
    | Lean.Grind.IntInterval.co lo hi => h_1 lo hi
    | Lean.Grind.IntInterval.ci lo => h_2 lo
    | Lean.Grind.IntInterval.io hi => h_3 hi
    | Lean.Grind.IntInterval.ii => h_4 ()) =
    h_2 lo
-- Mathlib.CategoryTheory.Localization.Construction
/-- The counit isomorphism of the equivalence of categories `WhiskeringLeftEquivalence W D`.  -/
CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.counitIso : {C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    (W : CategoryTheory.MorphismProperty C) →
      (D : Type uD) →
        [inst_1 : CategoryTheory.Category.{uD', uD} D] →
          (CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.inverse W D).comp
              (CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.functor W D) ≅
            CategoryTheory.Functor.id (W.FunctorsInverting D)
-- Mathlib.Topology.MetricSpace.Cover
/-- **Alias** of the reverse direction of `Metric.isCover_iff_subset_iUnion_closedBall`. -/
Metric.IsCover.of_subset_iUnion_closedBall : ∀ {X : Type u_1} [inst : PseudoMetricSpace X] {ε : NNReal} {s N : Set X},
  s ⊆ ⋃ y ∈ N, Metric.closedBall y ↑ε → Metric.IsCover ε s N
-- Mathlib.CategoryTheory.Idempotents.Karoubi
/-- an object of the underlying category  -/
CategoryTheory.Idempotents.Karoubi.X : {C : Type u_1} → [inst : CategoryTheory.Category.{v_1, u_1} C] → CategoryTheory.Idempotents.Karoubi C → C
-- Mathlib.Topology.Algebra.Module.ClosedSubmodule
ClosedSubmodule.mem_inf : ∀ {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : TopologicalSpace M]
  [inst_3 : Module R M] {s t : ClosedSubmodule R M} {x : M}, x ∈ s ⊓ t ↔ x ∈ s ∧ x ∈ t
-- Mathlib.Algebra.Order.Interval.Basic
instMulInterval : {α : Type u_2} → [inst : Preorder α] → [inst_1 : Mul α] → [MulLeftMono α] → [MulRightMono α] → Mul (Interval α)
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.map_apply_div_ne_zero : ∀ {K : Type u} [inst : CommRing K] [inst_1 : IsDomain K] {R : Type u_1} {F : Type u_2} [inst_2 : CommRing R]
  [inst_3 : IsDomain R] [inst_4 : FunLike F (Polynomial K) (Polynomial R)]
  [inst_5 : MonoidHomClass F (Polynomial K) (Polynomial R)] (φ : F)
  (hφ : nonZeroDivisors (Polynomial K) ≤ Submonoid.comap φ (nonZeroDivisors (Polynomial R))) (p q : Polynomial K),
  q ≠ 0 →
    (RatFunc.map φ hφ) ((algebraMap (Polynomial K) (RatFunc K)) p / (algebraMap (Polynomial K) (RatFunc K)) q) =
      (algebraMap (Polynomial R) (RatFunc R)) (φ p) / (algebraMap (Polynomial R) (RatFunc R)) (φ q)
-- Init.Data.List.Control
/-- Applies the monadic predicate `p` to every element in the list, in order from left to right, and
returns the list of elements for which `p` returns `true`.

`O(|l|)`.

Example:
```lean example
#eval [1, 2, 5, 2, 7, 7].filterM fun x => do
  IO.println s!"Checking {x}"
  return x < 3
```
```output
Checking 1
Checking 2
Checking 5
Checking 2
Checking 7
Checking 7
```
```output
[1, 2, 2]
```
 -/
List.filterM : {m : Type → Type v} → [Monad m] → {α : Type} → (α → m Bool) → List α → m (List α)
-- Mathlib.Data.List.Basic
List.foldr_ext : ∀ {α : Type u} {β : Type v} (f g : α → β → β) (b : β) {l : List α},
  (∀ a ∈ l, ∀ (b : β), f a b = g a b) → List.foldr f b l = List.foldr g b l
-- Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
_private.Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity.0.ChevalleyThm.PolynomialC.InductionObj.mk.sizeOf_spec : ∀ {R : Type u_2} [inst : CommRing R] {n : ℕ} [inst_1 : SizeOf R] (val : Fin n → Polynomial R), sizeOf { val := val } = 1
-- Mathlib.FieldTheory.PrimitiveElement
/-- **Steinitz theorem**: an algebraic extension `E` of `F` has a
primitive element (i.e. there is an `α ∈ E` such that `F⟮α⟯ = (⊤ : Subalgebra F E)`)
if and only if there exist only finitely many intermediate fields between `E` and `F`.  -/
Field.exists_primitive_element_iff_finite_intermediateField : ∀ (F : Type u_1) (E : Type u_2) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E],
  (Algebra.IsAlgebraic F E ∧ ∃ α, F⟮α⟯ = ⊤) ↔ Finite (IntermediateField F E)
-- Init.Data.BitVec.Lemmas
BitVec.shiftLeft_eq' : ∀ {w₁ w₂ : ℕ} {x : BitVec w₁} {y : BitVec w₂}, x <<< y = x <<< y.toNat
-- Mathlib.Algebra.Group.Hom.Basic
negAddMonoidHom_comp_negAddMonoidHom : ∀ {α : Type u_1} [inst : SubtractionCommMonoid α], negAddMonoidHom.comp negAddMonoidHom = AddMonoidHom.id α
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.homEquiv_id : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) (X : C),
  (adj.homEquiv X (F.obj X)) (CategoryTheory.CategoryStruct.id (F.obj X)) = adj.unit.app X
-- Mathlib.Data.ENat.Basic
ENat.zero_ne_top : 0 ≠ ⊤
-- Mathlib.LinearAlgebra.Matrix.RowCol
Matrix.updateRow_ne : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} {M : Matrix m n α} {i : m} {b : n → α} [inst : DecidableEq m] {i' : m},
  i' ≠ i → M.updateRow i b i' = M i'
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.ofList_singleton : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {k : α} {v : β}, Std.TreeMap.Raw.ofList [(k, v)] cmp = ∅.insert k v
-- Mathlib.LinearAlgebra.LinearIndependent.Basic
LinearIndepOn_iff_linearIndepOn_image_injOn : ∀ {ι : Type u'} {R : Type u_2} {s : Set ι} {M : Type u_4} {v : ι → M} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [Nontrivial R], LinearIndepOn R v s ↔ LinearIndepOn R id (v '' s) ∧ Set.InjOn v s
-- Lean.Data.PersistentArray
Lean.PersistentArray.instAppend : {α : Type u} → Append (Lean.PersistentArray α)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get?_union_of_not_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {m₁ m₂ : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  m₁.WF → m₂.WF → ∀ {k : α}, k ∉ m₂ → Std.DTreeMap.Raw.Const.get? (m₁ ∪ m₂) k = Std.DTreeMap.Raw.Const.get? m₁ k
-- Mathlib.Combinatorics.Digraph.Basic
Digraph.distribLattice : {V : Type u_2} → DistribLattice (Digraph V)