mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.strictMono_rpow_of_base_gt_one : ∀ {b : ℝ}, 1 < b → StrictMono fun x => b ^ x
-- Mathlib.RingTheory.Radical.NatInt
Int.radical_eq_prod_primeFactors : ∀ {z : ℤ}, UniqueFactorizationMonoid.radical z = ↑(∏ p ∈ z.natAbs.primeFactors, p)
-- Mathlib.LinearAlgebra.CliffordAlgebra.Basic
/-- The Clifford algebra of an `R`-module `M` equipped with a `QuadraticForm` `Q`.
 -/
CliffordAlgebra : {R : Type u_1} →
  [inst : CommRing R] →
    {M : Type u_2} → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → QuadraticForm R M → Type (max u_1 u_2)
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
CategoryTheory.Functor.inr_biprodComparison'_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  (F : CategoryTheory.Functor C D) (X Y : C) [inst_4 : CategoryTheory.Limits.HasBinaryBiproduct X Y]
  [inst_5 : CategoryTheory.Limits.HasBinaryBiproduct (F.obj X) (F.obj Y)] {Z : D} (h : F.obj (X ⊞ Y) ⟶ Z),
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr
      (CategoryTheory.CategoryStruct.comp (F.biprodComparison' X Y) h) =
    CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.biprod.inr) h
-- Mathlib.Analysis.Fourier.ZMod
ZMod.dft_comp_unitMul : ∀ {N : ℕ} [inst : NeZero N] {E : Type u_1} [inst_1 : AddCommGroup E] [inst_2 : Module ℂ E] (Φ : ZMod N → E)
  (u : (ZMod N)ˣ) (k : ZMod N), ZMod.dft (fun j => Φ (↑u * j)) k = ZMod.dft Φ (↑u⁻¹ * k)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.contains_minKey! : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.WF → t.isEmpty = false → t.contains t.minKey! = true
-- Mathlib.LinearAlgebra.Multilinear.Basic
MultilinearMap.ofSubsingletonₗ_apply : ∀ (R : Type uR) (S : Type uS) {ι : Type uι} (M₂ : Type v₂) (M₃ : Type v₃) [inst : Semiring R]
  [inst_1 : AddCommMonoid M₂] [inst_2 : Module R M₂] [inst_3 : Semiring S] [inst_4 : AddCommMonoid M₃]
  [inst_5 : Module S M₃] [inst_6 : Module R M₃] [inst_7 : SMulCommClass R S M₃] [inst_8 : Subsingleton ι] (i : ι)
  (a : M₂ →ₗ[R] M₃), (MultilinearMap.ofSubsingletonₗ R S M₂ M₃ i) a = (MultilinearMap.ofSubsingleton R M₂ M₃ i) a
-- Mathlib.LinearAlgebra.ExteriorPower.Basic
/-- The image of `exteriorPower.ιMulti` spans `⋀[R]^n M`.  -/
exteriorPower.ιMulti_span : ∀ (R : Type u) [inst : CommRing R] (n : ℕ) (M : Type u_1) [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  Submodule.span R (Set.range ⇑(exteriorPower.ιMulti R n)) = ⊤
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.IsMarkovKernel.comap : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4}
  {mγ : MeasurableSpace γ} {g : γ → α} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsMarkovKernel κ]
  (hg : Measurable g), ProbabilityTheory.IsMarkovKernel (κ.comap g hg)
-- Init.Data.Int.DivMod.Lemmas
Int.tdiv.eq_3 : ∀ (m n : ℕ), (Int.negSucc m).tdiv (Int.ofNat n) = -Int.ofNat (m.succ / n)
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.homotopyCofiber.inlX_XIsoBiprod_hom_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} {F G : HomologicalComplex C c} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ]
  [inst_3 : DecidableRel c.Rel] (i j : ι) (hij : c.Rel j i) {Z : C} (h : F.X i ⊞ G.X j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.inlX φ i j hij)
      (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.XIsoBiprod φ j i hij).hom h) =
    CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl h
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.exists_idempotent_basicOpen_eq_of_isClopen : ∀ {R : Type u} [inst : CommSemiring R] {s : Set (PrimeSpectrum R)},
  IsClopen s → ∃ e, IsIdempotentElem e ∧ s = ↑(PrimeSpectrum.basicOpen e)
-- Std.Data.DTreeMap.Internal.Def
Std.DTreeMap.Internal.Impl.leaf.sizeOf_spec : ∀ {α : Type u} {β : α → Type v} [inst : SizeOf α] [inst_1 : (a : α) → SizeOf (β a)],
  sizeOf Std.DTreeMap.Internal.Impl.leaf = 1
-- Mathlib.GroupTheory.Subsemigroup.Centralizer
Subsemigroup.decidableMemCentralizer.eq_1 : ∀ {M : Type u_1} {S : Set M} [inst : Semigroup M] (a : M) [inst_1 : Decidable (∀ b ∈ S, b * a = a * b)],
  Subsemigroup.decidableMemCentralizer a = decidable_of_iff' (∀ g ∈ S, g * a = a * g) ⋯
-- Mathlib.Data.Option.NAry
Option.map₂_map_right : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {a : Option α} {b : Option β} (f : α → γ → δ) (g : β → γ),
  Option.map₂ f a (Option.map g b) = Option.map₂ (fun a b => f a (g b)) a b
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.minKey?.congr_simp : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] (t t_1 : Std.ExtTreeMap α β cmp),
  t = t_1 → t.minKey? = t_1.minKey?
-- Mathlib.Algebra.Homology.ShortComplex.Basic
/-- The canonical isomorphism `S.op.unop ≅ S` for a short complex `S`  -/
CategoryTheory.ShortComplex.opUnop : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] → (S : CategoryTheory.ShortComplex C) → S.op.unop ≅ S
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get!_ofList_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} [inst : Std.TransCmp cmp] {l : List (α × β)} {k k' : α},
  cmp k k' = Ordering.eq →
    ∀ {v : β} [inst_1 : Inhabited β],
      List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l →
        (k, v) ∈ l → Std.ExtDTreeMap.Const.get! (Std.ExtDTreeMap.Const.ofList l cmp) k' = v
-- Mathlib.Control.Functor.Multivariate
MvFunctor.LiftR_def : ∀ {n : ℕ} {α : TypeVec.{u} n} {F : TypeVec.{u} n → Type v} [inst : MvFunctor F]
  (R : (α.prod α).Arrow (TypeVec.repeat n Prop)) [LawfulMvFunctor F] (x y : F α),
  MvFunctor.LiftR' R x y ↔
    ∃ u,
      MvFunctor.map (TypeVec.comp TypeVec.prod.fst (TypeVec.subtypeVal R)) u = x ∧
        MvFunctor.map (TypeVec.comp TypeVec.prod.snd (TypeVec.subtypeVal R)) u = y
-- Mathlib.Algebra.Order.Interval.Basic
Interval.add_eq_zero_iff : ∀ {α : Type u_2} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [inst_2 : IsOrderedAddMonoid α] {s t : Interval α},
  s + t = 0 ↔ ∃ a b, s = Interval.pure a ∧ t = Interval.pure b ∧ a + b = 0
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.Equiv.symm : ∀ {α : Type u} {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β}, m₁.Equiv m₂ → m₂.Equiv m₁
-- Mathlib.Order.BooleanAlgebra.Basic
le_iff_eq_sup_sdiff : ∀ {α : Type u} {x y z : α} [inst : GeneralizedBooleanAlgebra α], z ≤ y → x ≤ y → (x ≤ z ↔ y = z ⊔ y \ x)
-- Mathlib.CategoryTheory.DifferentialObject
CategoryTheory.DifferentialObject.instHasShift : {S : Type u_1} →
  [inst : AddCommGroupWithOne S] →
    (C : Type u) →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
          [inst_3 : CategoryTheory.HasShift C S] → CategoryTheory.HasShift (CategoryTheory.DifferentialObject S C) S
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.isUnsatEq : Int.Internal.Linear.Poly → Bool
-- Mathlib.Combinatorics.SimpleGraph.Basic
/-- The adjacency relation of a simple graph.  -/
SimpleGraph.Adj : {V : Type u} → SimpleGraph V → V → V → Prop
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.continuous_coe : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β], Continuous fun f x => f x
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.insphere_reindex : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {m n : ℕ} [inst_4 : NeZero m] [inst_5 : NeZero n] (s : Affine.Simplex ℝ P n)
  (e : Fin (n + 1) ≃ Fin (m + 1)), (s.reindex e).insphere = s.insphere
-- Mathlib.NumberTheory.Padics.PadicNumbers
/-- The `p`-adic norm of the entries of a nonzero Cauchy sequence of rationals is eventually
constant.  -/
PadicSeq.stationary : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {f : CauSeq ℚ (padicNorm p)},
  ¬f ≈ 0 → ∃ N, ∀ (m n : ℕ), N ≤ m → N ≤ n → padicNorm p (↑f n) = padicNorm p (↑f m)
-- Mathlib.Dynamics.PeriodicPts.Defs
Function.bijOn_ptsOfPeriod : ∀ {α : Type u_1} (f : α → α) {n : ℕ}, 0 < n → Set.BijOn f (Function.ptsOfPeriod f n) (Function.ptsOfPeriod f n)
-- Mathlib.NumberTheory.NumberField.Units.Basic
NumberField.Units.coe_coe : ∀ {K : Type u_1} [inst : Field K] (u : (NumberField.RingOfIntegers K)ˣ),
  ↑↑u = (algebraMap (NumberField.RingOfIntegers K) K) ↑u
-- Mathlib.GroupTheory.Divisible
QuotientAddGroup.divisibleBy.eq_1 : ∀ {A : Type u_2} [inst : AddCommGroup A] (B : AddSubgroup A) [inst_1 : DivisibleBy A ℕ],
  QuotientAddGroup.divisibleBy B = Function.Surjective.divisibleBy QuotientAddGroup.mk ⋯ ⋯
-- Mathlib.Order.BoundedOrder.Lattice
WellFoundedLT.induction_bot : ∀ {α : Type u_1} [inst : Preorder α] [WellFoundedLT α] [inst_2 : OrderBot α] {P : α → Prop},
  (∃ M, P M) → (∀ (N : α), N ≠ ⊥ → P N → ∃ M, N > M ∧ P M) → P ⊥
-- Mathlib.Algebra.Order.Group.MinMax
/-- **Alias** of `max_zero_sub_max_neg_zero_eq_self`. -/
max_zero_sub_eq_self : ∀ {α : Type u_1} [inst : AddGroup α] [inst_1 : LinearOrder α] [AddLeftMono α] (a : α), max a 0 - max (-a) 0 = a
-- Mathlib.CategoryTheory.Functor.Currying
/-- The equivalence of functor categories given by currying/uncurrying.
 -/
CategoryTheory.Functor.currying : {C : Type u₂} →
  [inst : CategoryTheory.Category.{v₂, u₂} C] →
    {D : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} D] →
        {E : Type u₄} →
          [inst_2 : CategoryTheory.Category.{v₄, u₄} E] →
            CategoryTheory.Functor C (CategoryTheory.Functor D E) ≌ CategoryTheory.Functor (C × D) E
-- Mathlib.Combinatorics.SimpleGraph.DeleteEdges
/-- A graph is `r`-*delete-far* from a property `p` if we must delete at least `r` edges from it to
get a graph with the property `p`.  -/
SimpleGraph.DeleteFar : {V : Type u_1} →
  (G : SimpleGraph V) →
    {𝕜 : Type u_2} → [Ring 𝕜] → [PartialOrder 𝕜] → [Fintype ↑G.edgeSet] → (SimpleGraph V → Prop) → 𝕜 → Prop
-- Mathlib.RingTheory.Discriminant
/-- Formula for the discriminant of a power basis using the norm of the field extension.  -/
Algebra.discr_powerBasis_eq_norm : ∀ (K : Type u) {L : Type v} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] [Module.Finite K L]
  (pb : PowerBasis K L) [Algebra.IsSeparable K L],
  Algebra.discr K ⇑pb.basis =
    (-1) ^ (Module.finrank K L * (Module.finrank K L - 1) / 2) *
      (Algebra.norm K) ((Polynomial.aeval pb.gen) (Polynomial.derivative (minpoly K pb.gen)))
-- Mathlib.Topology.Algebra.LinearMapCompletion
/-- Extension of a linear function to a linear function over the completion. This is the continuous
linear version of `UniformSpace.Completion.extension`.  -/
ContinuousLinearMap.fromCompletion : {α : Type u_1} →
  {β : Type u_2} →
    {R₁ : Type u_3} →
      {R₂ : Type u_4} →
        [inst : UniformSpace α] →
          [inst_1 : AddCommGroup α] →
            [inst_2 : IsUniformAddGroup α] →
              [inst_3 : Semiring R₁] →
                [inst_4 : Module R₁ α] →
                  [inst_5 : UniformContinuousConstSMul R₁ α] →
                    [inst_6 : Semiring R₂] →
                      [inst_7 : UniformSpace β] →
                        [inst_8 : AddCommGroup β] →
                          [IsUniformAddGroup β] →
                            [inst_10 : Module R₂ β] →
                              [UniformContinuousConstSMul R₂ β] →
                                {σ : R₁ →+* R₂} →
                                  [T0Space β] → [CompleteSpace β] → (α →SL[σ] β) → UniformSpace.Completion α →SL[σ] β
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra
/-- The compatibility morphisms.  -/
CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.hom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F :
        CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ)
          (CategoryTheory.Bicategory.Adj CategoryTheory.Cat)} →
      {ι : Type t} →
        {S : C} →
          {X : ι → C} →
            {f : (i : ι) → X i ⟶ S} →
              (self : F.DescentDataAsCoalgebra f) →
                (i₁ i₂ : ι) →
                  self.obj i₁ ⟶
                    (F.map (f i₁).op.toLoc).l.toFunctor.obj ((F.map (f i₂).op.toLoc).r.toFunctor.obj (self.obj i₂))
-- Mathlib.Combinatorics.SimpleGraph.Prod
SimpleGraph.boxProdFintypeNeighborSet : {α : Type u_1} →
  {β : Type u_2} →
    {G : SimpleGraph α} →
      {H : SimpleGraph β} →
        (x : α × β) → [Fintype ↑(G.neighborSet x.1)] → [Fintype ↑(H.neighborSet x.2)] → Fintype ↑((G □ H).neighborSet x)
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
_private.Std.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap.0.Std.IterM.stepAsHetT_filterMapWithPostcondition.match_3.splitter : {m : Type u_1 → Type u_2} →
  {α β : Type u_1} →
    (motive : Std.IterStep (Std.IterM m β) β → Sort u_3) →
      (x : Std.IterStep (Std.IterM m β) β) →
        ((it' : Std.IterM m β) → (out : β) → motive (Std.IterStep.yield it' out)) →
          ((it' : Std.IterM m β) → motive (Std.IterStep.skip it')) → (Unit → motive Std.IterStep.done) → motive x
-- Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple
/-- Lemma 4.3 from [Geck](Geck2017).  -/
RootPairing.GeckConstruction.instHasTrivialRadical : ∀ {ι : Type u_1} {K : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Field K] [inst_1 : CharZero K]
  [inst_2 : DecidableEq ι] [inst_3 : Fintype ι] [inst_4 : AddCommGroup M] [inst_5 : Module K M]
  [inst_6 : AddCommGroup N] [inst_7 : Module K N] {P : RootPairing ι K M N} [P.IsRootSystem]
  [inst_9 : P.IsCrystallographic] {b : P.Base} [P.IsReduced] [P.IsIrreducible] [IsAlgClosed K],
  LieAlgebra.HasTrivialRadical K ↥(RootPairing.GeckConstruction.lieAlgebra b)
-- Lean.Meta.AppBuilder
/-- Returns `of_eq_true h`  -/
Lean.Meta.mkOfEqTrue : Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.CategoryTheory.Monoidal.Grp
/-- The underlying object in the ambient monoidal category  -/
CategoryTheory.Grp.X : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] → CategoryTheory.Grp C → C
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.GoalM : Type → Type
-- Init.Grind.Order
_private.Init.Grind.Order.0.Lean.Grind.Order.add_lt_add_of_lt_of_le : ∀ {α : Type u_1} [inst : LE α] [inst_1 : LT α] [Std.LawfulOrderLT α] [inst_3 : Std.IsPreorder α]
  [inst_4 : Lean.Grind.Ring α] [Lean.Grind.OrderedRing α] {a b c d : α}, a < b → c ≤ d → a + c < b + d
-- Mathlib.LinearAlgebra.Projection
Submodule.projection_apply_right : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {p q : Submodule R E}
  (h : IsCompl p q) (x : ↥q), (p.projection q h) ↑x = 0
-- Mathlib.Order.RelSeries
RelSeries.instIsEmpty : ∀ {α : Type u_1} (r : SetRel α α) [IsEmpty α], IsEmpty (RelSeries r)
-- Mathlib.Data.Finset.Sym
Finset.sym_zero : ∀ {α : Type u_1} {s : Finset α} [inst : DecidableEq α], s.sym 0 = {∅}
-- Mathlib.Topology.MetricSpace.Snowflaking
Metric.Snowflaking.homeomorph_apply : ∀ {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [inst : TopologicalSpace X],
  ⇑Metric.Snowflaking.homeomorph = ⇑Metric.Snowflaking.ofSnowflaking
-- Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
MeasureTheory.lpNorm_neg : ∀ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} [inst : NormedAddCommGroup E] (f : α → E) (p : ENNReal)
  (μ : MeasureTheory.Measure α), MeasureTheory.lpNorm (-f) p μ = MeasureTheory.lpNorm f p μ
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
WellFounded.extrinsicFix₃.congr_simp : ∀ {α : Sort u_1} {β : α → Sort u_2} {γ : (a : α) → β a → Sort u_3} {C₃ : (a : α) → (b : β a) → γ a b → Sort u_4}
  [inst : ∀ (a : α) (b : β a) (c : γ a b), Nonempty (C₃ a b c)]
  (R : (a : α) ×' (b : β a) ×' γ a b → (a : α) ×' (b : β a) ×' γ a b → Prop)
  (F F_1 :
    (a : α) →
      (b : β a) →
        (c : γ a b) →
          ((a' : α) → (b' : β a') → (c' : γ a' b') → R ⟨a', ⟨b', c'⟩⟩ ⟨a, ⟨b, c⟩⟩ → C₃ a' b' c') → C₃ a b c),
  F = F_1 → ∀ (a : α) (b : β a) (c : γ a b), WellFounded.extrinsicFix₃ R F a b c = WellFounded.extrinsicFix₃ R F_1 a b c
-- Mathlib.Analysis.Matrix.Normed
/-- Normed ring instance (using the Frobenius norm) for matrices over `ℝ` or `ℂ`.  Not
declared as an instance because there are several natural choices for defining the norm of a
matrix.  -/
Matrix.frobeniusNormedRing : {m : Type u_3} → {α : Type u_5} → [Fintype m] → [RCLike α] → [DecidableEq m] → NormedRing (Matrix m m α)
-- Mathlib.Topology.QuasiSeparated
QuasiSeparatedSpace.isCompact_sInter_of_nonempty : ∀ {α : Type u_1} [inst : TopologicalSpace α] [QuasiSeparatedSpace α] {s : Set (Set α)},
  s.Finite → s.Nonempty → (∀ t ∈ s, IsOpen t ∨ IsClosed t) → (∀ t ∈ s, IsCompact t) → IsCompact (⋂₀ s)
-- Mathlib.Tactic.Lift
/-- A class specifying that you can lift elements from `α` to `β` assuming `cond` is true.
Used by the tactic `lift`.  -/
CanLift : (α : Sort u_1) → (β : Sort u_2) → outParam (β → α) → outParam (α → Prop) → Prop
-- Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
MeasurableSpace.generateFrom_countablePartition_le : ∀ (α : Type u_3) [m : MeasurableSpace α] [inst : MeasurableSpace.CountablyGenerated α] (n : ℕ),
  MeasurableSpace.generateFrom (MeasurableSpace.countablePartition α n) ≤ m
-- Batteries.Tactic.GeneralizeProofs
/-- Map version of `generalizations`. Use `MAbs.findProof?` and `MAbs.insertProof`.  -/
Batteries.Tactic.GeneralizeProofs.AState.propToProof : Batteries.Tactic.GeneralizeProofs.AState → Lean.ExprMap Lean.Expr
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBSet.findP?_some_mem_toList : ∀ {α : Type u_1} {cmp : α → α → Ordering} {cut : α → Ordering} {y : α} {t : RBTree.RBSet α cmp},
  t.findP? cut = some y → y ∈ t.toList
-- Mathlib.MeasureTheory.Measure.Portmanteau
MeasureTheory.tendsto_measure_of_le_liminf_measure_of_limsup_measure_le : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] {ι : Type u_2} {L : Filter ι} {μ : MeasureTheory.Measure Ω}
  {μs : ι → MeasureTheory.Measure Ω} {E₀ E E₁ : Set Ω},
  E₀ ⊆ E →
    E ⊆ E₁ →
      μ (E₁ \ E₀) = 0 →
        μ E₀ ≤ Filter.liminf (fun i => (μs i) E₀) L →
          Filter.limsup (fun i => (μs i) E₁) L ≤ μ E₁ → Filter.Tendsto (fun i => (μs i) E) L (nhds (μ E))
-- Mathlib.FieldTheory.IsAlgClosed.Basic
Polynomial.isCoprime_iff_aeval_ne_zero_of_isAlgClosed : ∀ (k : Type u) [inst : Field k] (K : Type v) [inst_1 : Field K] [IsAlgClosed K] [inst_3 : Algebra k K]
  (p q : Polynomial k), IsCoprime p q ↔ ∀ (a : K), (Polynomial.aeval a) p ≠ 0 ∨ (Polynomial.aeval a) q ≠ 0
-- Mathlib.Tactic.Linter.UnusedInstancesInType
/-- Detects `Fintype` instance hypotheses in the types of theorems which are not used in the
remainder of the type, and suggests replacing them with the corresponding hypothesis of `Finite`
and the use of `Fintype.ofFinite` in the proof.  -/
_private.Mathlib.Tactic.Linter.UnusedInstancesInType.0.Mathlib.Linter.UnusedInstancesInType.unusedFintypeInType : Lean.Linter
-- Mathlib.Tactic.Order.CollectFacts
Mathlib.Tactic.Order.AtomicFact.nle.injEq : ∀ (lhs rhs : ℕ) (proof : Lean.Expr) (lhs_1 rhs_1 : ℕ) (proof_1 : Lean.Expr),
  (Mathlib.Tactic.Order.AtomicFact.nle lhs rhs proof = Mathlib.Tactic.Order.AtomicFact.nle lhs_1 rhs_1 proof_1) =
    (lhs = lhs_1 ∧ rhs = rhs_1 ∧ proof = proof_1)
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.NonemptyCompacts.toCompacts : {α : Type u_4} → [inst : TopologicalSpace α] → TopologicalSpace.NonemptyCompacts α → TopologicalSpace.Compacts α
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Linear
/-- When an instance of `[HasDerivedCategory.{w'} C]` is available, this is the `R`-linear
equivalence between `Ext.{w} X Y n` and a type of morphisms in the derived category
of the `R`-linear abelian category `C`.  -/
CategoryTheory.Abelian.Ext.homLinearEquiv : {R : Type t} →
  [inst : Ring R] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        [inst_2 : CategoryTheory.Abelian C] →
          [inst_3 : CategoryTheory.Linear R C] →
            [inst_4 : CategoryTheory.HasExt C] →
              {X Y : C} →
                {n : ℕ} →
                  [inst_5 : HasDerivedCategory C] →
                    CategoryTheory.Abelian.Ext X Y n ≃ₗ[R]
                      CategoryTheory.ShiftedHom ((DerivedCategory.singleFunctor C 0).obj X)
                        ((DerivedCategory.singleFunctor C 0).obj Y) ↑n
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- A binary cofan with vertex `P` consists of the two inclusions `ι₁ : X ⟶ P` and `ι₂ : Y ⟶ P`.  -/
CategoryTheory.Limits.BinaryCofan.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → {X Y P : C} → (X ⟶ P) → (Y ⟶ P) → CategoryTheory.Limits.BinaryCofan X Y
-- Mathlib.Order.Heyting.Hom
BiheytingHom.mk.injEq : ∀ {α : Type u_6} {β : Type u_7} [inst : BiheytingAlgebra α] [inst_1 : BiheytingAlgebra β]
  (toLatticeHom : LatticeHom α β)
  (map_himp' : ∀ (a b : α), toLatticeHom.toFun (a ⇨ b) = toLatticeHom.toFun a ⇨ toLatticeHom.toFun b)
  (map_sdiff' : ∀ (a b : α), toLatticeHom.toFun (a \ b) = toLatticeHom.toFun a \ toLatticeHom.toFun b)
  (toLatticeHom_1 : LatticeHom α β)
  (map_himp'_1 : ∀ (a b : α), toLatticeHom_1.toFun (a ⇨ b) = toLatticeHom_1.toFun a ⇨ toLatticeHom_1.toFun b)
  (map_sdiff'_1 : ∀ (a b : α), toLatticeHom_1.toFun (a \ b) = toLatticeHom_1.toFun a \ toLatticeHom_1.toFun b),
  ({ toLatticeHom := toLatticeHom, map_himp' := map_himp', map_sdiff' := map_sdiff' } =
      { toLatticeHom := toLatticeHom_1, map_himp' := map_himp'_1, map_sdiff' := map_sdiff'_1 }) =
    (toLatticeHom = toLatticeHom_1)
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
/-- The canonical isomorphism between the chosen biproduct and the chosen coproduct.  -/
CategoryTheory.Limits.biproduct.isoCoproduct : {J : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
        (f : J → C) → [inst_2 : CategoryTheory.Limits.HasBiproduct f] → ⨁ f ≅ ∐ f
-- Mathlib.Algebra.DirectSum.Internal
DirectSum.coe_mul_of_apply_of_not_le : ∀ {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [inst : DecidableEq ι] [inst_1 : Semiring R] [inst_2 : SetLike σ R]
  [inst_3 : AddSubmonoidClass σ R] (A : ι → σ) [inst_4 : AddCommMonoid ι] [inst_5 : PartialOrder ι]
  [CanonicallyOrderedAdd ι] [inst_7 : SetLike.GradedMonoid A] (r : DirectSum ι fun i => ↥(A i)) {i : ι} (r' : ↥(A i))
  (n : ι), ¬i ≤ n → ↑((r * (DirectSum.of (fun i => ↥(A i)) i) r') n) = 0
-- Mathlib.SetTheory.Ordinal.CantorNormalForm
_private.Mathlib.SetTheory.Ordinal.CantorNormalForm.0.List.keys.eq_1 : ∀ {α : Type u} {β : α → Type v}, List.keys = List.map Sigma.fst
-- Std.Tactic.BVDecide.LRAT.Parser
_private.Std.Tactic.BVDecide.LRAT.Parser.0.Std.Tactic.BVDecide.LRAT.Parser.Text.parseIdList.idWs : Std.Internal.Parsec.ByteArray.Parser ℕ
-- Mathlib.CategoryTheory.Category.ULift
CategoryTheory.instInhabitedAsSmall : {C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → [Inhabited C] → Inhabited (CategoryTheory.AsSmall C)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.prod.lift_fst_comp_snd_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C}
  [inst_1 : CategoryTheory.Limits.HasBinaryProduct W Y] [inst_2 : CategoryTheory.Limits.HasBinaryProduct X Z]
  (g : W ⟶ X) (g' : Y ⟶ Z),
  CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst g)
      (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd g') =
    CategoryTheory.Limits.prod.map g g'
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
SimpleGraph.completeMultipartiteGraph.colorable : ∀ {ι : Type u_4} (V : ι → Type u_5) [inst : Fintype ι],
  (SimpleGraph.completeMultipartiteGraph V).Colorable (Fintype.card ι)