mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Module.Submodule.Map
Submodule.comap_id : ∀ {R : Type u_1} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (p : Submodule R M), Submodule.comap LinearMap.id p = p
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr
Std.Tactic.BVDecide.BVExpr.Cache.hbound : ∀ {aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit} (self : Std.Tactic.BVDecide.BVExpr.Cache aig) {i : ℕ}
  (k : Std.Tactic.BVDecide.BVExpr.Cache.Key) (h1 : k ∈ self.map) (h2 : i < k.w),
  (self.map.get k h1)[i].gate < aig.decls.size
-- Mathlib.MeasureTheory.Order.Group.Lattice
Measurable.negPart : ∀ {α : Type u_1} {β : Type u_2} [inst : Lattice α] [inst_1 : AddGroup α] [inst_2 : MeasurableSpace α]
  [inst_3 : MeasurableSpace β] {f : β → α} [MeasurableNeg α] [MeasurableSup α],
  Measurable f → Measurable fun x => (f x)⁻
-- Mathlib.Algebra.Homology.Factorizations.CM5a
_private.Mathlib.Algebra.Homology.Factorizations.CM5a.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₂.homologyShortComplex_g : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {K L : CochainComplex C ℤ} (f : K ⟶ L) [inst_2 : CategoryTheory.EnoughInjectives C] (n : ℤ),
  (CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₂.homologyShortComplex✝ f n).g =
    HomologicalComplex.homologyMap (CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₂.α✝ f n) n
-- Mathlib.MeasureTheory.PiSystem
/-- Given a collection `S` of subsets of `α`, then `generatePiSystem S` is the smallest
π-system containing `S`.  -/
generatePiSystem : {α : Type u_1} → Set (Set α) → Set (Set α)
-- Mathlib.Algebra.Ring.CentroidHom
CentroidHom.add_apply : ∀ {α : Type u_5} [inst : NonUnitalNonAssocSemiring α] (f g : CentroidHom α) (a : α), (f + g) a = f a + g a
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.bypass_eq_self_of_length_le_length_bypass : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} [inst : DecidableEq V] (p : G.Walk u v),
  p.length ≤ p.bypass.length → p.bypass = p
-- Mathlib.Data.Real.Basic
IsPowMul.map_one_le_one : ∀ {R : Type u_1} [inst : Monoid R] {f : R → ℝ}, IsPowMul f → f 1 ≤ 1
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.le_iff_mem_closure : ∀ {R : Type u} [inst : CommSemiring R] (x y : PrimeSpectrum R), x ≤ y ↔ y ∈ closure {x}
-- Mathlib.Data.Rat.Cast.Defs
MonoidWithZeroHomClass.ext_rat_iff : ∀ {M₀ : Type u_5} [inst : MonoidWithZero M₀] {f g : ℚ →*₀ M₀},
  f = g ↔
    f.comp (MonoidWithZeroHom.ofClass (Int.castRingHom ℚ)) = g.comp (MonoidWithZeroHom.ofClass (Int.castRingHom ℚ))
-- Mathlib.NumberTheory.NumberField.Discriminant.Defs
Module.Basis.indexEquiv.congr_simp : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {ι : Type w}
  {ι' : Type w'} [inst_3 : InvariantBasisNumber R] (v v_1 : Module.Basis ι R M),
  v = v_1 → ∀ (v' v'_1 : Module.Basis ι' R M), v' = v'_1 → v.indexEquiv v' = v_1.indexEquiv v'_1
-- Lean.Elab.Do.Basic
/-- The cached `PUnit.unit` expression.  -/
Lean.Elab.Do.MonadInfo.cachedPUnitUnit : Lean.Elab.Do.MonadInfo → Lean.Expr
-- Mathlib.Order.KrullDimension
/-- The **Krull dimension** of a preorder `α` is the supremum of the rightmost index of all relation
series of `α` ordered by `<`. If there is no series `a₀ < a₁ < ... < aₙ` in `α`, then its Krull
dimension is defined to be negative infinity; if the length of all series `a₀ < a₁ < ... < aₙ` is
unbounded, its Krull dimension is defined to be positive infinity.
 -/
Order.krullDim : (α : Type u_1) → [Preorder α] → WithBot ℕ∞
-- Mathlib.Order.CountableSupClosed
subset_countableSupClosure : ∀ {α : Type u_2} {s : Set α} [inst : Preorder α], s ⊆ countableSupClosure s
-- Mathlib.Algebra.Category.ModuleCat.Adjunctions
ModuleCat.freeDesc_apply : ∀ {R : Type u} [inst : Ring R] {X : Type u} {M : ModuleCat R} (f : X ⟶ ↑M) (x : X),
  (CategoryTheory.ConcreteCategory.hom (ModuleCat.freeDesc f)) (ModuleCat.freeMk x) =
    (CategoryTheory.ConcreteCategory.hom f) x
-- Mathlib.Algebra.Order.Module.Defs
/-- Scalar multiplication on the left by a nonnegative element preserves monotonicity.  -/
Monotone.const_smul : ∀ {α : Type u_1} {β : Type u_2} {a : α} [inst : SMul α β] [inst_1 : Preorder α] [inst_2 : Preorder β] [inst_3 : Zero α]
  [PosSMulMono α β] {γ : Type u_3} [inst_5 : Preorder γ] {f : γ → β}, Monotone f → 0 ≤ a → Monotone fun x => a • f x
-- Mathlib.Data.Vector3
/-- Recursion principle for a nonempty vector.  -/
Vector3.consElim : {α : Type u_1} →
  {n : ℕ} →
    {C : Vector3 α (n + 1) → Sort u} →
      ((a : α) → (t : Vector3 α n) → C (Vector3.cons a t)) → (v : Vector3 α (n + 1)) → C v
-- Mathlib.Analysis.Real.Sqrt
/-- Extension for the `positivity` tactic: a square root is nonnegative, and is strictly positive if
its input is.  -/
Mathlib.Meta.Positivity.evalSqrt : Mathlib.Meta.Positivity.PositivityExt
-- Mathlib.MeasureTheory.Group.FoelnerFilter
IsAddFoelner.mean_univ_eq_zero : ∀ {G : Type u_1} {X : Type u_2} [inst : MeasurableSpace X] {μ : MeasureTheory.Measure X} [inst_1 : AddGroup G]
  [inst_2 : AddAction G X] {ι : Type u_3} {u : Ultrafilter ι} {F : ι → Set X},
  IsAddFoelner G μ (↑u) F → IsAddFoelner.mean μ u F Set.univ = 1
-- Mathlib.Algebra.Lie.Weights.Killing
LieAlgebra.IsKilling.coroot.congr_simp : ∀ {K : Type u_2} {L : Type u_3} [inst : LieRing L] [inst_1 : Field K] [inst_2 : LieAlgebra K L]
  [inst_3 : FiniteDimensional K L] {H : LieSubalgebra K L} [inst_4 : H.IsCartanSubalgebra]
  [inst_5 : LieAlgebra.IsKilling K L] (α α_1 : LieModule.Weight K (↥H) L),
  α = α_1 → LieAlgebra.IsKilling.coroot α = LieAlgebra.IsKilling.coroot α_1
-- Init.Data.SInt.Lemmas
Int8.toInt64_div_of_ne_right : ∀ (a b : Int8), b ≠ -1 → (a / b).toInt64 = a.toInt64 / b.toInt64
-- Lean.PrettyPrinter.Parenthesizer
Lean.PrettyPrinter.Parenthesizer.many1Unbox.parenthesizer : Lean.PrettyPrinter.Parenthesizer → Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Order.Category.BddLat
/-- Construct a bundled `BddLat` from `Lattice` + `BoundedOrder`.  -/
BddLat.of : (α : Type u_1) → [inst : Lattice α] → [BoundedOrder α] → BddLat
-- Mathlib.Combinatorics.HalesJewett
Combinatorics.Line.apply_some : ∀ {α : Type u_2} {ι : Type u_3} {l : Combinatorics.Line α ι} {i : ι} {a x : α}, l.idxFun i = some a → ↑l x i = a
-- Mathlib.RingTheory.Polynomial.Basic
/-- Transport an ideal of `R[X]` to an `R`-submodule of `R[X]`.  -/
Ideal.ofPolynomial : {R : Type u} → [inst : Semiring R] → Ideal (Polynomial R) → Submodule R (Polynomial R)
-- Mathlib.Data.Ordering.Lemmas
cmpUsing_eq_gt : ∀ {α : Type u} {lt : α → α → Prop} [inst : DecidableRel lt] [IsStrictOrder α lt] (a b : α),
  cmpUsing lt a b = Ordering.gt ↔ lt b a
-- Mathlib.NumberTheory.RamificationInertia.Inertia
/-- **Alias** of `Ideal.inertiaDeg'_algebra_tower`.

---

Let `T / S / R` be a tower of algebras, `p, P, I` be ideals in `R, S, T`, respectively,
and `p` and `P` are maximal. If `p = P ∩ S` and `P = I ∩ S`,
then `f (I | p) = f (P | p) * f (I | P)`.  -/
Ideal.inertiaDeg_algebra_tower : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  [inst_3 : Algebra R S] [inst_4 : Algebra S T] [inst_5 : Algebra R T] [IsScalarTower R S T] (p : Ideal R) (P : Ideal S)
  (I : Ideal T) [p.IsMaximal] [P.IsMaximal] [P.LiesOver p] [I.LiesOver P],
  p.inertiaDeg' I = p.inertiaDeg' P * P.inertiaDeg' I
-- Init.Data.Array.Lemmas
Array.filterMap_push_some : ∀ {α : Type u_1} {β : Type u_2} {stop : ℕ} {f : α → Option β} {a : α} {xs : Array α} {b : β},
  f a = some b → stop = xs.size + 1 → Array.filterMap f (xs.push a) 0 stop = (Array.filterMap f xs).push b
-- Mathlib.Algebra.Algebra.Operations
Submodule.map_op_one : ∀ {R : Type u} [inst : CommSemiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Algebra R A],
  Submodule.map (↑(MulOpposite.opLinearEquiv R)) 1 = 1
-- Mathlib.AlgebraicTopology.SimplicialSet.FiniteColimits
SSet.iSup_range_eq_top_of_isColimit : ∀ {J : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} J] [CategoryTheory.Limits.HasColimitsOfShape J (Type u)]
  {F : CategoryTheory.Functor J SSet} {c : CategoryTheory.Limits.Cocone F} (hc : CategoryTheory.Limits.IsColimit c),
  ⨆ j, SSet.Subcomplex.range (c.ι.app j) = ⊤
-- Mathlib.NumberTheory.Chebyshev
/-- `ψ x = θ x + O( √x )`.  -/
Chebyshev.psi_sub_theta_le_mul_sqrt : ∃ C, ∀ (x : ℝ), Chebyshev.psi x - Chebyshev.theta x ≤ C * √x
-- Init.Data.UInt.Bitwise
UInt32.toFin_not : ∀ (a : UInt32), (~~~a).toFin = a.toFin.rev
-- Mathlib.Data.DFinsupp.Order
DFinsupp.decidableLE : {ι : Type u_1} →
  (α : ι → Type u_2) →
    [inst : (i : ι) → AddCommMonoid (α i)] →
      [inst_1 : (i : ι) → PartialOrder (α i)] →
        [∀ (i : ι), CanonicallyOrderedAdd (α i)] →
          [DecidableEq ι] →
            [(i : ι) → (x : α i) → Decidable (x ≠ 0)] → [(i : ι) → DecidableLE (α i)] → DecidableLE (Π₀ (i : ι), α i)
-- Lean.ScopedEnvExtension
Lean.registerScopedEnvExtensionUnsafe : {α β σ : Type} → Lean.ScopedEnvExtension.Descr α β σ → IO (Lean.ScopedEnvExtension α β σ)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.maxKey?_bind_getKey? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → t.maxKey?.bind t.getKey? = t.maxKey?
-- Mathlib.Algebra.Group.Basic
eq_mul_of_inv_mul_eq : ∀ {G : Type u_3} [inst : Group G] {a b c : G}, b⁻¹ * a = c → a = b * c
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.IsFundamentalDomain.aestronglyMeasurable_on_iff : ∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α] {s t : Set α}
  {μ : MeasureTheory.Measure α} [MeasurableConstSMul G α] [MeasureTheory.SMulInvariantMeasure G α μ] [Countable G]
  {β : Type u_6} [inst_6 : TopologicalSpace β] [TopologicalSpace.PseudoMetrizableSpace β],
  MeasureTheory.IsFundamentalDomain G s μ →
    MeasureTheory.IsFundamentalDomain G t μ →
      ∀ {f : α → β},
        (∀ (g : G) (x : α), f (g • x) = f x) →
          (MeasureTheory.AEStronglyMeasurable f (μ.restrict s) ↔ MeasureTheory.AEStronglyMeasurable f (μ.restrict t))
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.Indep.mem_closure_iff_of_notMem : ∀ {α : Type u_2} {M : Matroid α} {e : α} {I : Set α}, M.Indep I → e ∉ I → (e ∈ M.closure I ↔ M.Dep (insert e I))
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.apply_coe_mem_map : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [inst : L.Structure M] [inst_1 : L.Structure N] (f : L.Hom M N)
  (S : L.Substructure M) (x : ↥S), f ↑x ∈ FirstOrder.Language.Substructure.map f S
-- Std.Data.ExtDTreeMap.Basic
Std.ExtDTreeMap.instEmptyCollection : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → EmptyCollection (Std.ExtDTreeMap α β cmp)
-- Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
MeasureTheory.LevyProkhorov.edist_finiteMeasure_def : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : PseudoEMetricSpace Ω] [inst_2 : OpensMeasurableSpace Ω]
  (μ ν : MeasureTheory.LevyProkhorov (MeasureTheory.FiniteMeasure Ω)),
  edist μ ν = MeasureTheory.levyProkhorovEDist ↑μ.toMeasure ↑ν.toMeasure
-- Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
CategoryTheory.regularTopology.EqualizerCondition.mk' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.Functor Cᵒᵖ (Type u_4)),
  (∀ (X B : C) (π : X ⟶ B) [CategoryTheory.EffectiveEpi π] (c : CategoryTheory.Limits.PullbackCone π π)
      (x : CategoryTheory.Limits.IsLimit c),
      Function.Bijective
        ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.regularTopology.mapToEqualizer P π c.fst c.snd ⋯))) →
    CategoryTheory.regularTopology.EqualizerCondition P
-- Mathlib.GroupTheory.Finiteness
Monoid.FG.mk : ∀ {M : Type u_1} [inst : Monoid M], ⊤.FG → Monoid.FG M
-- Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Ordinal.le_cof_iff_lsub : ∀ {o : Ordinal.{u}} {a : Cardinal.{u}},
  a ≤ o.cof ↔ ∀ {ι : Type u} (f : ι → Ordinal.{u}), Ordinal.lsub f = o → a ≤ Cardinal.mk ι
-- Mathlib.LinearAlgebra.Dimension.Finite
finrank_eq_zero_of_basis_imp_not_finite : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Module.Free R M],
  (∀ (s : Set M) (a : Module.Basis (↑s) R M), ¬s.Finite) → Module.finrank R M = 0
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
CategoryTheory.ChosenPullbacksAlong.iso_pullback_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Y X : C} (f : Y ≅ X) (Z : CategoryTheory.Over X),
  (CategoryTheory.ChosenPullbacksAlong.pullback f.hom).obj Z =
    CategoryTheory.Over.mk (CategoryTheory.CategoryStruct.comp Z.hom f.inv)
-- Mathlib.RingTheory.DividedPowers.SubDPIdeal
DividedPowers.SubDPIdeal.instCoeOutElemIdealIic : {A : Type u_1} → [inst : CommSemiring A] → {I : Ideal A} → {hI : DividedPowers I} → CoeOut hI.SubDPIdeal ↑(Set.Iic I)
-- Init.Data.Order.PackageFactories
Std.Packages.LinearOrderOfOrdArgs.max_eq : ∀ {α : Type u} (self : Std.Packages.LinearOrderOfOrdArgs α),
  let this := self.ord;
  let this_1 := self.le;
  let this_2 := self.max;
  have this_3 := ⋯;
  ∀ (a b : α), a ⊔ b = if (compare a b).isGE = true then a else b
-- Mathlib.Topology.Bornology.Constructions
boundedSpace_val_set_iff : ∀ {α : Type u_1} [inst : Bornology α] {s : Set α}, BoundedSpace ↑s ↔ Bornology.IsBounded s
-- Mathlib.Topology.Semicontinuity.Basic
lowerSemicontinuousWithinAt_tsum : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} {x : α} {ι : Type u_4} {f : ι → α → ENNReal},
  (∀ (i : ι), LowerSemicontinuousWithinAt (f i) s x) → LowerSemicontinuousWithinAt (fun x' => ∑' (i : ι), f i x') s x
-- Mathlib.Algebra.Group.Basic
neg_sub' : ∀ {α : Type u_1} [inst : SubtractionCommMonoid α] (a b : α), -(a - b) = -a - -b
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.Const.modify.eq_2 : ∀ {α : Type u} [inst : BEq α] {β : Type v} (a : α) (f : β → β) (k : α) (v : β)
  (es : Std.DHashMap.Internal.AssocList α fun x => β),
  Std.DHashMap.Internal.AssocList.Const.modify a f (Std.DHashMap.Internal.AssocList.cons k v es) =
    if (k == a) = true then Std.DHashMap.Internal.AssocList.cons a (f v) es
    else Std.DHashMap.Internal.AssocList.cons k v (Std.DHashMap.Internal.AssocList.Const.modify a f es)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem!_insert_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : Inhabited β]
  {k : α} {v : β}, (t.insert k v)[k]! = v
-- Mathlib.CategoryTheory.Limits.Final
/-- Final functors preserve filteredness.

This can be seen as a generalization of `IsFiltered.of_right_adjoint` (which states that right
adjoints preserve filteredness), as right adjoints are always final, see `final_of_adjunction`.
 -/
CategoryTheory.IsFiltered.of_final : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [F.Final] [CategoryTheory.IsFiltered C], CategoryTheory.IsFiltered D
-- Mathlib.Data.Fin.Tuple.NatAntidiagonal
/-- The disjoint union of antidiagonal tuples `Σ n, antidiagonalTuple k n` is equivalent to the
`k`-tuple `Fin k → ℕ`. This is such an equivalence, obtained by mapping `(n, x)` to `x`.

This is the tuple version of `Finset..HasAntidiagonal.sigmaAntidiagonalEquivProd`.  -/
Finset.Nat.sigmaAntidiagonalTupleEquivTuple : (k : ℕ) → (n : ℕ) × ↥(Finset.Nat.antidiagonalTuple k n) ≃ (Fin k → ℕ)
-- Mathlib.Analysis.RCLike.Basic
RCLike.I_mul_I_of_nonzero : ∀ {K : Type u_1} [inst : RCLike K], RCLike.I ≠ 0 → RCLike.I * RCLike.I = -1
-- Mathlib.Analysis.Calculus.BumpFunction.Basic
ContDiffBumpBase.mem_Icc : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (self : ContDiffBumpBase E) (R : ℝ) (x : E),
  self.toFun R x ∈ Set.Icc 0 1
-- Mathlib.RingTheory.AdicCompletion.Basic
AdicCompletion.AdicCauchySequence.instCoeFunForallNat : {R : Type u_1} →
  [inst : CommRing R] →
    (I : Ideal R) →
      (M : Type u_4) →
        [inst_1 : AddCommGroup M] →
          [inst_2 : Module R M] → CoeFun (AdicCompletion.AdicCauchySequence I M) fun x => ℕ → M
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.lift_uniq : ∀ {X Y Z : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Z) (g : Y ⟶ Z)
  [H : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion f]
  (H' :
    Set.range ⇑(CategoryTheory.ConcreteCategory.hom g.base) ⊆ Set.range ⇑(CategoryTheory.ConcreteCategory.hom f.base))
  (l : Y ⟶ X),
  CategoryTheory.CategoryStruct.comp l f = g → l = AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.lift f g H'
-- Init.SizeOf
Lean.ParserDescr.symbol.sizeOf_spec : ∀ (val : String), sizeOf (Lean.ParserDescr.symbol val) = 1 + sizeOf val
-- Lean.Meta.HaveTelescope
Lean.Meta.instInhabitedHaveTelescopeInfo.default : Lean.Meta.HaveTelescopeInfo
-- Mathlib.GroupTheory.GroupAction.Defs
MulAction.orbitRel.Quotient.mem_orbit : ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] {a : α} {x : MulAction.orbitRel.Quotient G α},
  a ∈ x.orbit ↔ Quotient.mk'' a = x
-- Lean.Server.RequestCancellation
Lean.Server.instMonadCancellableCancellableTOfMonadOfMonadLiftTBaseIO : {m : Type → Type u_1} → [Monad m] → [MonadLiftT BaseIO m] → Lean.Server.MonadCancellable (Lean.Server.CancellableT m)
-- Mathlib.Order.Filter.Bases.Basic
Filter.HasAntitoneBasis.comap : ∀ {α : Type u_1} {β : Type u_2} {ι'' : Type u_6} [inst : Preorder ι''] {l : Filter α} {s : ι'' → Set α},
  l.HasAntitoneBasis s → ∀ (m : β → α), (Filter.comap m l).HasAntitoneBasis fun x => m ⁻¹' s x
-- Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
SSet.exists_nonDegenerate : ∀ (X : SSet) {n : ℕ} (x : X.obj (Opposite.op { len := n })),
  ∃ m f, ∃ (_ : CategoryTheory.Epi f), ∃ y, x = (CategoryTheory.ConcreteCategory.hom (X.map f.op)) ↑y
-- Init.Data.UInt.Bitwise
UInt16.or_self : ∀ {a : UInt16}, a ||| a = a
-- Std.Data.HashMap.Lemmas
Std.HashMap.get?_inter_of_not_mem_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α}, k ∉ m₁ → (m₁ ∩ m₂).get? k = none
-- Mathlib.Order.Grade
grade_bot : ∀ {𝕆 : Type u_1} {α : Type u_3} [inst : PartialOrder 𝕆] [inst_1 : Preorder α] [inst_2 : OrderBot 𝕆]
  [inst_3 : OrderBot α] [inst_4 : GradeMinOrder 𝕆 α], grade 𝕆 ⊥ = ⊥
-- Mathlib.Order.UpperLower.Basic
isLowerSet_iInter₂ : ∀ {α : Type u_1} {ι : Sort u_3} {κ : ι → Sort u_4} [inst : LE α] {f : (i : ι) → κ i → Set α},
  (∀ (i : ι) (j : κ i), IsLowerSet (f i j)) → IsLowerSet (⋂ i, ⋂ j, f i j)
-- Mathlib.Algebra.QuadraticAlgebra.Defs
QuadraticAlgebra.instFree : ∀ {R : Type u_1} (a b : R) [inst : Semiring R], Module.Free R (QuadraticAlgebra R a b)
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.skewProd_apply : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  {M₂ : Type u_3} [inst_3 : TopologicalSpace M₂] [inst_4 : AddCommGroup M₂] {M₃ : Type u_4}
  [inst_5 : TopologicalSpace M₃] [inst_6 : AddCommGroup M₃] {M₄ : Type u_5} [inst_7 : TopologicalSpace M₄]
  [inst_8 : AddCommGroup M₄] [inst_9 : Module R M] [inst_10 : Module R M₂] [inst_11 : Module R M₃]
  [inst_12 : Module R M₄] [inst_13 : IsTopologicalAddGroup M₄] (e : M ≃L[R] M₂) (e' : M₃ ≃L[R] M₄) (f : M →L[R] M₄)
  (x : M × M₃), (e.skewProd e' f) x = (e x.1, e' x.2 + f x.1)
-- Mathlib.Data.ULift
ULift.instIsEmpty : ∀ {α : Type u} [IsEmpty α], IsEmpty (ULift.{u_1, u} α)
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
CategoryTheory.Abelian.SpectralObject.instEpiGCokernelSequenceCycles : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k)
  (h : CategoryTheory.CategoryStruct.comp f g = fg) (n : ℤ), CategoryTheory.Epi (X.cokernelSequenceCycles f g fg h n).g
-- Init.GrindInstances.Ring.UInt
UInt8.intCast_ofNat : ∀ (x : ℕ), ↑(OfNat.ofNat x) = OfNat.ofNat x
-- Mathlib.Algebra.CubicDiscriminant
Cubic.of_c_eq_zero : ∀ {R : Type u_1} {P : Cubic R} [inst : Semiring R], P.a = 0 → P.b = 0 → P.c = 0 → P.toPoly = Polynomial.C P.d
-- Mathlib.MeasureTheory.Integral.IntegrableOn
/-- A function is `IntegrableOn` a set `s` if it is almost everywhere strongly measurable on `s`
and if the integral of its pointwise norm over `s` is less than infinity.  -/
MeasureTheory.IntegrableOn : {α : Type u_1} →
  {ε : Type u_3} →
    {mα : MeasurableSpace α} →
      [inst : TopologicalSpace ε] →
        [ContinuousENorm ε] →
          (α → ε) → Set α → autoParam (MeasureTheory.Measure α) MeasureTheory.IntegrableOn._auto_1 → Prop
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
CategoryTheory.Subgroupoid.instTop : {C : Type u} → [inst : CategoryTheory.Groupoid C] → Top (CategoryTheory.Subgroupoid C)
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.minKey!_alterKey_eq_self : ∀ {α : Type u} {β : Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α] [inst_4 : Inhabited α]
  {l : List ((_ : α) × β)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k : α} {f : Option β → Option β},
      (Std.Internal.List.Const.alterKey k f l).isEmpty = false →
        (Std.Internal.List.minKey! (Std.Internal.List.Const.alterKey k f l) = k ↔
          (f (Std.Internal.List.getValue? k l)).isSome = true ∧
            ∀ (k' : α), Std.Internal.List.containsKey k' l = true → (compare k k').isLE = true)
-- Mathlib.Topology.UniformSpace.CompactConvergence
ContinuousMap.isUniformEmbedding_uniformFunOfFun : ∀ {α : Type u₁} {β : Type u₂} [inst : TopologicalSpace α] [inst_1 : UniformSpace β] [CompactSpace α],
  IsUniformEmbedding fun x => UniformFun.ofFun ⇑x
-- Mathlib.Topology.Algebra.RestrictedProduct.Units
/-- The ring isomorphism between the units of a restricted product `Πʳ i, [R i, B i]_[𝓕]` and
the restricted product of `(R i)ˣ` with respect to `(B i)ˣ`.  -/
RestrictedProduct.unitsEquiv : {ι : Type u_1} →
  (R : ι → Type u_2) →
    [inst : (i : ι) → Monoid (R i)] →
      {S : ι → Type u_3} →
        [inst_1 : (i : ι) → SetLike (S i) (R i)] →
          [inst_2 : ∀ (i : ι), SubmonoidClass (S i) (R i)] →
            {B : (i : ι) → S i} →
              {𝓕 : Filter ι} →
                (RestrictedProduct (fun i => R i) (fun i => ↑(B i)) 𝓕)ˣ ≃*
                  RestrictedProduct (fun i => (R i)ˣ) (fun i => ↑(Submonoid.ofClass (B i)).units) 𝓕
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
ContinuousMultilinearMap.norm_compContinuousLinearMapL_le : ∀ {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {E₁ : ι → Type wE₁} (G : Type wG) [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)]
  [inst_3 : (i : ι) → SeminormedAddCommGroup (E₁ i)] [inst_4 : (i : ι) → NormedSpace 𝕜 (E₁ i)]
  [inst_5 : SeminormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] [inst_7 : Fintype ι] (f : (i : ι) → E i →L[𝕜] E₁ i),
  ‖ContinuousMultilinearMap.compContinuousLinearMapL f‖ ≤ ∏ i, ‖f i‖
-- Mathlib.Order.Hom.Set
OrderIso.preimage_symm_preimage : ∀ {α : Type u_1} {β : Type u_2} [inst : LE α] [inst_1 : LE β] (e : α ≃o β) (s : Set α), ⇑e ⁻¹' ⇑e.symm ⁻¹' s = s
-- Aesop.RuleSet
Aesop.GlobalRuleSet.trace : Aesop.GlobalRuleSet → Aesop.TraceOption → Lean.CoreM Unit
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.and_mono_r : ∀ {σs : List (Type u)} {P Q Q' : Std.Do.SPred σs}, (Q ⊢ₛ Q') → P ∧ Q ⊢ₛ P ∧ Q'
-- Mathlib.Data.List.Cycle
/-- Return the `z` such that `x :: z :: _` appears in `xs`, or `default` if there is no such `z`.  -/
List.nextOr : {α : Type u_1} → [DecidableEq α] → List α → α → α → α
-- Lean.Meta.HaveTelescope
/-- The level of the type for this `have`, cached.  -/
Lean.Meta.HaveInfo.level : Lean.Meta.HaveInfo → Lean.Level
-- Mathlib.Order.Filter.Bases.Basic
Filter.HasAntitoneBasis.map : ∀ {α : Type u_1} {β : Type u_2} {ι'' : Type u_6} [inst : Preorder ι''] {l : Filter α} {s : ι'' → Set α},
  l.HasAntitoneBasis s → ∀ (m : α → β), (Filter.map m l).HasAntitoneBasis fun x => m '' s x