mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.Enumerative.Partition.Glaisher
Nat.Partition.card_restricted_eq_card_countRestricted : ∀ (n : ℕ) {m : ℕ}, 0 < m → (Nat.Partition.restricted n fun x => ¬m ∣ x).card = (Nat.Partition.countRestricted n m).card
-- Mathlib.Topology.Hom.Open
/-- `ContinuousOpenMapClass F α β` states that `F` is a type of continuous open maps.

You should extend this class when you extend `ContinuousOpenMap`.  -/
ContinuousOpenMapClass : (F : Type u_6) →
  (α : outParam (Type u_7)) →
    (β : outParam (Type u_8)) → [TopologicalSpace α] → [TopologicalSpace β] → [FunLike F α β] → Prop
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.eLpNormEssSup_lt_top_of_ae_bound : ∀ {α : Type u_1} {F : Type u_5} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup F]
  {f : α → F} {C : ℝ}, (∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C) → MeasureTheory.eLpNormEssSup f μ < ⊤
-- Mathlib.Topology.Algebra.Polynomial
Polynomial.continuousWithinAt_aeval : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : TopologicalSpace A] [IsTopologicalSemiring A] (p : Polynomial R) {s : Set A} {a : A},
  ContinuousWithinAt (fun x => (Polynomial.aeval x) p) s a
-- Mathlib.Algebra.CubicDiscriminant
Cubic.coeff_eq_b : ∀ {R : Type u_1} {P : Cubic R} [inst : Semiring R], P.toPoly.coeff 2 = P.b
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get?_unitOfList : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] [inst : BEq α] [Std.LawfulBEqCmp cmp] {l : List α} {k : α},
  Std.DTreeMap.Const.get? (Std.DTreeMap.Const.unitOfList l cmp) k = if l.contains k = true then some () else none
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalAlgebra.instIsMulCommutative_adjoin : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : NonUnitalSemiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] [inst_4 : SMulCommClass R A A] {S : Type u_3} [inst_5 : SetLike S A]
  [inst_6 : MulMemClass S A] (s : S) [IsMulCommutative ↥s], IsMulCommutative ↥(NonUnitalAlgebra.adjoin R ↑s)
-- Mathlib.Analysis.RCLike.Lemmas
/-- This instance generates a type-class problem with a metavariable `?m` that should satisfy
`RCLike ?m`. Since this can only be satisfied by `ℝ` or `ℂ`, this does not cause problems.  -/
LibraryNote.RCLike_instance : Batteries.Util.LibraryNote
-- Mathlib.NumberTheory.LegendreSymbol.Basic
/-- Euler's Criterion: a nonzero `a : ZMod p` is a square if and only if `x ^ (p / 2) = 1`.  -/
ZMod.euler_criterion : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)] {a : ZMod p}, a ≠ 0 → (IsSquare a ↔ a ^ (p / 2) = 1)
-- Mathlib.MeasureTheory.Measure.MeasureSpace
_private.Mathlib.MeasureTheory.Measure.MeasureSpace.0.MeasureTheory.Measure.measure_sInf_le : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {m : Set (MeasureTheory.Measure α)},
  μ ∈ m → sInf m ≤ μ
-- Mathlib.Topology.Sheaves.Stalks
TopCat.Presheaf.stalkSpecializes_stalkFunctor_map_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C] {X : TopCat}
  {F G : TopCat.Presheaf C X} (f : F ⟶ G) {x y : ↑X} (h : x ⤳ y) {Z : C}
  (h_1 : (TopCat.Presheaf.stalkFunctor C x).obj G ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.stalkSpecializes h)
      (CategoryTheory.CategoryStruct.comp ((TopCat.Presheaf.stalkFunctor C x).map f) h_1) =
    CategoryTheory.CategoryStruct.comp ((TopCat.Presheaf.stalkFunctor C y).map f)
      (CategoryTheory.CategoryStruct.comp (G.stalkSpecializes h) h_1)
-- Init.Data.List.Erase
List.Nodup.not_mem_erase : ∀ {α : Type u_1} [inst : BEq α] {l : List α} [LawfulBEq α] {a : α}, l.Nodup → a ∉ l.erase a
-- Std.Data.DTreeMap.Raw.Basic
Std.DTreeMap.Raw.empty_eq_emptyc : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering}, Std.DTreeMap.Raw.empty = ∅
-- Mathlib.Topology.Algebra.InfiniteSum.Defs
Summable.mono_filter : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α}
  {L₁ L₂ : SummationFilter β}, Summable f L₂ → L₁.filter ≤ L₂.filter → Summable f L₁
-- Lean.Elab.InfoTree.Types
Lean.Elab.ErrorNameInfo.mk.injEq : ∀ (stx : Lean.Syntax) (errorName : Lean.Name) (stx_1 : Lean.Syntax) (errorName_1 : Lean.Name),
  ({ stx := stx, errorName := errorName } = { stx := stx_1, errorName := errorName_1 }) =
    (stx = stx_1 ∧ errorName = errorName_1)
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.IsNonloop.mem_ground : ∀ {α : Type u_1} {M : Matroid α} {e : α}, M.IsNonloop e → e ∈ M.E
-- Batteries.Tactic.Case
/-- Clause for a `case ... : ...` tactic.  -/
Batteries.Tactic.casePattArg : Lean.ParserDescr
-- Mathlib.CategoryTheory.Localization.Resolution
CategoryTheory.LocalizerMorphism.LeftResolution.mk_surjective : ∀ {C₁ : Type u_1} {C₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} {X₂ : C₂}
  (L : Φ.LeftResolution X₂), ∃ X₁ w, ∃ (hw : W₂ w), L = { X₁ := X₁, w := w, hw := hw }
-- Mathlib.CategoryTheory.Limits.ConeCategory
CategoryTheory.Limits.Cocone.toCostructuredArrowCompProj_hom_app : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cocone F) (X : J),
  c.toCostructuredArrowCompProj.hom.app X = CategoryTheory.CategoryStruct.id X
-- Init.Data.SInt.Bitwise
Int32.neg_eq_not_add : ∀ (a : Int32), -a = ~~~a + 1
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.CoordinateRing.basis_one : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Affine R},
  (WeierstrassCurve.Affine.CoordinateRing.basis W') 1 = (WeierstrassCurve.Affine.CoordinateRing.mk W') Polynomial.X
-- Mathlib.CategoryTheory.CommSq
/-- Equivalences of `LiftStruct` for a square and the corresponding square
in the opposite category.  -/
CategoryTheory.CommSq.LiftStruct.opEquiv : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {A B X Y : C} →
      {f : A ⟶ X} →
        {i : A ⟶ B} → {p : X ⟶ Y} → {g : B ⟶ Y} → (sq : CategoryTheory.CommSq f i p g) → sq.LiftStruct ≃ ⋯.LiftStruct
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.Γ'.enumList_getElem?_ctorIdx_eq : ∀ (x : Turing.PartrecToTM2.Γ'), Turing.PartrecToTM2.Γ'.enumList[x.ctorIdx]? = some x
-- Mathlib.GroupTheory.MonoidLocalization.Maps
Submonoid.LocalizationMap.ofMulEquivOfLocalizations_apply : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N] {P : Type u_3}
  [inst_2 : CommMonoid P] (f : S.LocalizationMap N) {k : N ≃* P} (x : M), (f.ofMulEquivOfLocalizations k) x = k (f x)
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.Monoidal.ext_iff : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C} {D : Type u₂}
  {inst_2 : CategoryTheory.Category.{v₂, u₂} D} {inst_3 : CategoryTheory.MonoidalCategory D}
  {F : CategoryTheory.Functor C D} {x y : F.Monoidal},
  x = y ↔
    CategoryTheory.Functor.LaxMonoidal.ε F = CategoryTheory.Functor.LaxMonoidal.ε F ∧
      CategoryTheory.Functor.LaxMonoidal.μ F = CategoryTheory.Functor.LaxMonoidal.μ F ∧
        CategoryTheory.Functor.OplaxMonoidal.η F = CategoryTheory.Functor.OplaxMonoidal.η F ∧
          CategoryTheory.Functor.OplaxMonoidal.δ F = CategoryTheory.Functor.OplaxMonoidal.δ F
-- Aesop.Index
Aesop.Index.instEmptyCollection : {α : Type} → EmptyCollection (Aesop.Index α)
-- Mathlib.Topology.Algebra.UniformConvergence
UniformFun.toFun_sum : ∀ {α : Type u_1} {ι : Type u_3} {β : Type u_4} [inst : AddCommMonoid β] {f : ι → α → β} (I : Finset ι),
  UniformFun.toFun (∑ i ∈ I, f i) = ∑ i ∈ I, UniformFun.toFun (f i)
-- Mathlib.SetTheory.Ordinal.Basic
Cardinal.ord_le_type : ∀ {α : Type u} (r : α → α → Prop) [h : IsWellOrder α r], (Cardinal.mk α).ord ≤ Ordinal.type r
-- Mathlib.Analysis.Normed.Module.Multilinear.Curry
/-- Given a continuous multilinear map `f` in `n+1` variables, split the last variable to obtain
a continuous multilinear map in `n` variables into continuous linear maps, given by
`m ↦ (x ↦ f (snoc m x))`.  -/
ContinuousMultilinearMap.curryRight : {𝕜 : Type u} →
  {n : ℕ} →
    {Ei : Fin n.succ → Type wEi} →
      {G : Type wG} →
        [inst : NontriviallyNormedField 𝕜] →
          [inst_1 : (i : Fin n.succ) → NormedAddCommGroup (Ei i)] →
            [inst_2 : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)] →
              [inst_3 : NormedAddCommGroup G] →
                [inst_4 : NormedSpace 𝕜 G] →
                  ContinuousMultilinearMap 𝕜 Ei G → Ei i.castSucc [×n]→L[𝕜] Ei (Fin.last n) →L[𝕜] G
-- Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
/-- Same as `partialTraj_comp_partialTraj` but only assuming `b ≤ c`. It requires Markov kernels.  -/
ProbabilityTheory.Kernel.partialTraj_comp_partialTraj'' : ∀ {X : ℕ → Type u_1} {mX : (n : ℕ) → MeasurableSpace (X n)} {a : ℕ}
  {κ : (n : ℕ) → ProbabilityTheory.Kernel ((i : ↥(Finset.Iic n)) → X ↑i) (X (n + 1))}
  [∀ (n : ℕ), ProbabilityTheory.IsMarkovKernel (κ n)] {b c : ℕ},
  c ≤ b →
    (ProbabilityTheory.Kernel.partialTraj κ b c).comp (ProbabilityTheory.Kernel.partialTraj κ a b) =
      ProbabilityTheory.Kernel.partialTraj κ a c
-- Mathlib.Algebra.Group.Action.Faithful
/-- `instVAddOfAdd` is faithful when there is a (right) identity.  -/
instFaithfulVAdd : ∀ (R : Type u_4) [inst : AddZeroClass R], FaithfulVAdd R R
-- Mathlib.Data.Nat.Squarefree
_private.Mathlib.Data.Nat.Squarefree.0.Nat.minSqFacAux.match_1.splitter : (motive : ℕ → ℕ → Sort u_1) → (x x_1 : ℕ) → ((n k : ℕ) → motive n k) → motive x x_1
-- Mathlib.Logic.Equiv.Fin.Basic
finSuccEquiv_eq_some : ∀ {n : ℕ} {i : Fin (n + 1)} {j : Fin n}, (finSuccEquiv n) i = some j ↔ i = j.succ
-- Mathlib.Algebra.Algebra.Spectrum.Basic
spectrum.add_singleton_eq : ∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] (a : A) (r : R),
  spectrum R a + {r} = spectrum R (a + (algebraMap R A) r)
-- Lean.DocString.Types
/-- Multiple blocks, merged.
 -/
Lean.Doc.Block.concat : {i : Type u} → {b : Type v} → Array (Lean.Doc.Block i b) → Lean.Doc.Block i b
-- Init.Data.UInt.Bitwise
USize.ofFin_shiftLeft : ∀ (a b : Fin USize.size), ↑b < System.Platform.numBits → USize.ofFin (a <<< b) = USize.ofFin a <<< USize.ofFin b
-- Mathlib.LinearAlgebra.Matrix.SchurComplement
/-- If a block matrix is invertible and so is its bottom left element, then so is the corresponding
Schur complement.  -/
Matrix.invertibleOfFromBlocks₂₂Invertible : {m : Type u_2} →
  {n : Type u_3} →
    {α : Type u_4} →
      [inst : Fintype m] →
        [inst_1 : Fintype n] →
          [inst_2 : DecidableEq m] →
            [inst_3 : DecidableEq n] →
              [inst_4 : CommRing α] →
                (A : Matrix m m α) →
                  (B : Matrix m n α) →
                    (C : Matrix n m α) →
                      (D : Matrix n n α) →
                        [inst_5 : Invertible D] → [Invertible (Matrix.fromBlocks A B C D)] → Invertible (A - B * ⅟D * C)
-- Init.Data.String.Lemmas.Pattern.Pred
String.Slice.all_prop_eq_all_decide : ∀ {p : Char → Prop} [inst : DecidablePred p] {s : String.Slice}, s.all p = s.all fun x => decide (p x)
-- Mathlib.Algebra.Category.ModuleCat.Topology.Basic
TopModuleCat.instPreservesLimitsTopCatForget₂ContinuousLinearMapIdCarrierContinuousMapCarrier : ∀ {R : Type u} [inst : Ring R] [inst_1 : TopologicalSpace R],
  CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget₂ (TopModuleCat R) TopCat)
-- Mathlib.CategoryTheory.Sites.MorphismProperty
/-- The weakest morphism property satisfied by all morphisms in covering families.  -/
CategoryTheory.Precoverage.morphismProperty : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] → CategoryTheory.Precoverage C → CategoryTheory.MorphismProperty C
-- Mathlib.Algebra.Polynomial.Splits
Polynomial.Splits.degree_eq_one_of_irreducible : ∀ {R : Type u_1} [inst : Field R] {f : Polynomial R}, f.Splits → Irreducible f → f.degree = 1
-- Init.Data.List.Pairwise
List.Nodup.sublist : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Sublist l₂ → l₂.Nodup → l₁.Nodup
-- Mathlib.RingTheory.IntegralClosure.IntegralRestrict
Algebra.intNorm_intNorm : ∀ (A : Type u_1) (B : Type u_6) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B]
  [inst_3 : IsIntegrallyClosed A] [inst_4 : IsDomain A] [inst_5 : IsDomain B] [inst_6 : IsIntegrallyClosed B]
  [inst_7 : Algebra.IsIntegral A B] [inst_8 : Module.IsTorsionFree A B] {C : Type u_9} [inst_9 : CommRing C]
  [inst_10 : IsDomain C] [inst_11 : IsIntegrallyClosed C] [inst_12 : Algebra A C] [inst_13 : Algebra B C]
  [IsScalarTower A B C] [inst_15 : Algebra.IsIntegral A C] [inst_16 : Algebra.IsIntegral B C]
  [inst_17 : Module.IsTorsionFree A C] [inst_18 : Module.IsTorsionFree B C] (x : C),
  (Algebra.intNorm A B) ((Algebra.intNorm B C) x) = (Algebra.intNorm A C) x
-- Mathlib.Geometry.Manifold.Instances.Real
instLocallyPathConnectedSpaceEuclideanQuadrant : ∀ {n : ℕ}, LocallyPathConnectedSpace (EuclideanQuadrant n)
-- Mathlib.Analysis.Calculus.FDeriv.Const
fderiv_fun_const : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] (c : F), (fderiv 𝕜 fun x => c) = 0
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank
SSet.Subcomplex.PairingCore.WeakRankFunction.mk.inj : ∀ {X : SSet} {A : X.Subcomplex} {h : A.PairingCore} {α : Type v} {inst : PartialOrder α} {rank : h.ι → α}
  {lt : ∀ {x y : h.ι}, h.AncestralRel x y → h.dim x = h.dim y → rank x < rank y} {rank_1 : h.ι → α}
  {lt_1 : ∀ {x y : h.ι}, h.AncestralRel x y → h.dim x = h.dim y → rank_1 x < rank_1 y},
  { rank := rank, lt := lt } = { rank := rank_1, lt := lt_1 } → rank = rank_1
-- Mathlib.GroupTheory.Subgroup.Center
/-- The center of a group `G` is the set of elements that commute with everything in `G`  -/
Subgroup.center : (G : Type u_1) → [inst : Group G] → Subgroup G
-- Mathlib.CategoryTheory.EqToHom
CategoryTheory.eqToHom_comp_heq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W X Y : C} (f : Y ⟶ X) (h : W = Y),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h) f ≍ f
-- Mathlib.Algebra.Order.ToIntervalMod
toIocDiv_mul_sub_self : ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : LinearOrder R] [inst_2 : IsOrderedAddMonoid R]
  [inst_3 : Archimedean R] {p : R} (hp : 0 < p) (a b : R), ↑(toIocDiv hp a b) * p - b = -toIocMod hp a b
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.size_filterMap_eq_size_iff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} {γ : α → Type w}
  [inst : LawfulBEq α] {f : (a : α) → β a → Option (γ a)},
  (Std.ExtDHashMap.filterMap f m).size = m.size ↔ ∀ (a : α) (h : a ∈ m), (f a (m.get a h)).isSome = true
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.size_filter!_eq_size_iff : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  {f : α → β → Bool},
  t.WF →
    ((Std.DTreeMap.Internal.Impl.filter! f t).size = t.size ↔
      ∀ (a : α) (h : Std.DTreeMap.Internal.Impl.contains a t = true),
        f (t.getKey a h) (Std.DTreeMap.Internal.Impl.Const.get t a h) = true)
-- Mathlib.Topology.Clopen
Set.Finite.isClopen_biInter : ∀ {X : Type u} [inst : TopologicalSpace X] {Y : Type u_2} {s : Set Y},
  s.Finite → ∀ {f : Y → Set X}, (∀ i ∈ s, IsClopen (f i)) → IsClopen (⋂ i ∈ s, f i)
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.revSkip?_eq_revSkip?_toSlice : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.BackwardPattern pat] {s : String} {pos : s.Pos},
  pos.revSkip? pat = Option.map String.Pos.ofToSlice (pos.toSlice.revSkip? pat)
-- Init.Data.List.Lemmas
List.map_id_fun : ∀ {α : Type u_1}, List.map id = id
-- Mathlib.CategoryTheory.Limits.Types.ColimitType
CategoryTheory.Functor.CoconeTypes.IsColimit.equiv_symm_ι_apply : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {F : CategoryTheory.Functor J (Type w₀)} {c : F.CoconeTypes}
  (hc : c.IsColimit) (j : J) (x : F.obj j), hc.equiv.symm (c.ι j x) = F.ιColimitType j x
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
AlgebraicGeometry.Proj.fromOfGlobalSections_preimage_basicOpen : ∀ {σ : Type u_1} {A : Type u} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] {X : AlgebraicGeometry.Scheme} (f : A →+* ↑(X.presheaf.obj (Opposite.op ⊤)))
  (hf : Ideal.map f (HomogeneousIdeal.irrelevant 𝒜).toIdeal = ⊤) {r : A} {n : ℕ},
  0 < n →
    r ∈ 𝒜 n →
      (TopologicalSpace.Opens.map (AlgebraicGeometry.Proj.fromOfGlobalSections 𝒜 f hf).base).obj
          (AlgebraicGeometry.Proj.basicOpen 𝒜 r) =
        X.basicOpen (f r)
-- Mathlib.NumberTheory.Dioph
Dioph.diophFn_comp : ∀ {α : Type} {n : ℕ} {f : Vector3 ℕ n → ℕ},
  Dioph.DiophFn f →
    ∀ (g : Vector3 ((α → ℕ) → ℕ) n), VectorAllP Dioph.DiophFn g → Dioph.DiophFn fun v => f fun i => g i v
-- Mathlib.Lean.Expr.Basic
/-- Returns `true` if `type` is an application of a constant `declName`, or a
forall with return type of the same form (i.e. of the form `∀ (x₀ : X₀) (x₁ : X₁) ⋯, declName ..`).

Runs `cleanupAnnotations` on `type` and `forallE` bodies, and ignores metadata in applications.
 -/
Lean.Expr.isAppOrForallOfConst : Lean.Name → Lean.Expr → Bool
-- Mathlib.RingTheory.Algebraic.Basic
Algebra.IsAlgebraic.of_ringHom_of_comp_eq : ∀ {R : Type u} {S : Type u_1} {A : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Ring A]
  [inst_3 : Algebra R A] {B : Type u_2} [inst_4 : Ring B] [inst_5 : Algebra S B] {FRS : Type u_3} {FAB : Type u_4}
  [inst_6 : FunLike FRS R S] [inst_7 : RingHomClass FRS R S] [inst_8 : FunLike FAB A B] [inst_9 : RingHomClass FAB A B]
  (f : FRS) (g : FAB) [Algebra.IsAlgebraic S B],
  Function.Surjective ⇑f →
    Function.Injective ⇑g → (algebraMap S B).comp ↑f = (↑g).comp (algebraMap R A) → Algebra.IsAlgebraic R A
-- Mathlib.Analysis.SpecificLimits.Basic
tsum_geometric_two : ∑' (n : ℕ), (1 / 2) ^ n = 2
-- Init.Data.AC
Lean.Data.AC.Expr.var.injEq : ∀ (x x_1 : ℕ), (Lean.Data.AC.Expr.var x = Lean.Data.AC.Expr.var x_1) = (x = x_1)
-- Mathlib.Algebra.Homology.Embedding.Extend
HomologicalComplex.extendSingleIso_hom_f : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : DecidableEq ι] (e : c.Embedding c') (X : C)
  [inst_4 : DecidableEq ι'] (i : ι) (i' : ι') (h : e.f i = i'),
  (HomologicalComplex.extendSingleIso e X i i' h).hom.f i' =
    CategoryTheory.CategoryStruct.comp (((HomologicalComplex.single C c i).obj X).extendXIso e h).hom
      (CategoryTheory.CategoryStruct.comp (HomologicalComplex.singleObjXSelf c i X).hom
        (HomologicalComplex.singleObjXSelf c' i' X).inv)
-- Lean.Meta.Tactic.Grind.Action
Lean.Meta.Grind.TGrindStep : Type
-- Mathlib.Analysis.Normed.Lp.PiLp
/-- The product of finitely many normed spaces is a normed space, with the `L^p` norm.  -/
PiLp.normedSpace : (p : ENNReal) →
  (𝕜 : Type u_1) →
    {ι : Type u_2} →
      (β : ι → Type u_4) →
        [hp : Fact (1 ≤ p)] →
          [inst : Fintype ι] →
            [inst_1 : NormedField 𝕜] →
              [inst_2 : (i : ι) → SeminormedAddCommGroup (β i)] →
                [(i : ι) → NormedSpace 𝕜 (β i)] → NormedSpace 𝕜 (PiLp p β)
-- Mathlib.Order.UpperLower.Basic
isLowerSet_iInter : ∀ {α : Type u_1} {ι : Sort u_3} [inst : LE α] {f : ι → Set α}, (∀ (i : ι), IsLowerSet (f i)) → IsLowerSet (⋂ i, f i)
-- Mathlib.NumberTheory.ModularForms.BoundedAtCusp
OnePoint.isBoundedAt_infty_iff : ∀ {f : UpperHalfPlane → ℂ} {k : ℤ}, OnePoint.infty.IsBoundedAt f k ↔ UpperHalfPlane.IsBoundedAtImInfty f
-- Init.Data.String.Subslice
String.Slice.subslice.congr_simp : ∀ (s : String.Slice) (newStart newStart_1 : s.Pos) (e_newStart : newStart = newStart_1) (newEnd newEnd_1 : s.Pos)
  (e_newEnd : newEnd = newEnd_1) (h : newStart ≤ newEnd),
  s.subslice newStart newEnd h = s.subslice newStart_1 newEnd_1 ⋯
-- Mathlib.Algebra.MvPolynomial.Counit
MvPolynomial.counit_C : ∀ (R : Type u_3) [inst : CommRing R] (n : ℤ), (MvPolynomial.counit R) (MvPolynomial.C n) = ↑n
-- Mathlib.LinearAlgebra.Span.Defs
Submodule.span_eq_span : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {s t : Set M},
  s ⊆ ↑(Submodule.span R t) → t ⊆ ↑(Submodule.span R s) → Submodule.span R s = Submodule.span R t
-- Mathlib.Combinatorics.Matroid.Minor.Contract
Matroid.delete_contract_eq_sdiff : ∀ {α : Type u_1} (M : Matroid α) (D C : Set α), (M.delete D).contract C = (M.delete D).contract (C \ D)
-- Mathlib.LinearAlgebra.AffineSpace.Independent
/-- A family is affinely independent if and only if the differences
from a base point in that family are linearly independent.  -/
affineIndependent_iff_linearIndependent_vsub : ∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {ι : Type u_4} (p : ι → P) (i1 : ι),
  AffineIndependent k p ↔ LinearIndependent k fun i => p ↑i -ᵥ p i1
-- Mathlib.GroupTheory.Perm.Cycle.Factors
Equiv.Perm.cycleFactorsFinset_eq_finset : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Fintype α] {σ : Equiv.Perm α} {s : Finset (Equiv.Perm α)},
  σ.cycleFactorsFinset = s ↔ (∀ f ∈ s, f.IsCycle) ∧ ∃ (h : (↑s).Pairwise Equiv.Perm.Disjoint), s.noncommProd id ⋯ = σ
-- Mathlib.Data.Finset.Max
Finset.min.eq_1 : ∀ {α : Type u_2} [inst : LinearOrder α] (s : Finset α), s.min = s.inf WithTop.some
-- Mathlib.NumberTheory.ModularForms.SlashActions
_private.Mathlib.NumberTheory.ModularForms.SlashActions.0.ModularForm.slash_mul : ∀ (k : ℤ) (A B : GL (Fin 2) ℝ) (f : UpperHalfPlane → ℂ),
  ModularForm.privateSlash✝ k (A * B) f = ModularForm.privateSlash✝ k B (ModularForm.privateSlash✝ k A f)
-- Mathlib.CategoryTheory.Limits.Shapes.Diagonal
CategoryTheory.Limits.pullback.instIsIsoDiagonalOfMono : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : C} (f : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasPullback f f] [CategoryTheory.Mono f],
  CategoryTheory.IsIso (CategoryTheory.Limits.pullback.diagonal f)
-- Mathlib.Topology.MetricSpace.Pseudo.Constructions
NNReal.le_add_nndist : ∀ (a b : NNReal), a ≤ b + nndist a b
-- Mathlib.Algebra.Group.Subsemigroup.Basic
AddSubsemigroup.closure.eq_1 : ∀ {M : Type u_1} [inst : Add M] (s : Set M), AddSubsemigroup.closure s = sInf {S | s ⊆ ↑S}
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
CategoryTheory.Limits.CatCospanTransform.isIso_base : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆}
  [inst : CategoryTheory.Category.{v₁, u₁} A] [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] [inst_4 : CategoryTheory.Category.{v₅, u₅} B']
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'}
  {ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'} (f : ψ' ⟶ ψ') [CategoryTheory.IsIso f],
  CategoryTheory.IsIso f.base
-- Aesop.Stats.Basic
Aesop.RuleStats.successful : Aesop.RuleStats → Bool
-- Mathlib.Analysis.InnerProductSpace.Coalgebra
/-- A finite-dimensional inner product space with a coalgebra structure induces a ring structure,
where multiplication is given by `x * y = (adjoint comul) (x ⊗ₜ y)` and
`1 = (adjoint counit) (1 : 𝕜)`.

See note [reducible non-instances].  -/
InnerProductSpace.ringOfCoalgebra : {𝕜 : Type u_1} →
  {E : Type u_2} →
    [inst : RCLike 𝕜] →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : InnerProductSpace 𝕜 E] → [FiniteDimensional 𝕜 E] → [Coalgebra 𝕜 E] → Ring E