mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Abelian.Projective.Dimension
CategoryTheory.HasProjectiveDimensionLT.subsingleton' : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.Abelian C} {X : C} {n : ℕ}
  [self : CategoryTheory.HasProjectiveDimensionLT X n] (i : ℕ),
  n ≤ i → ∀ ⦃Y : C⦄, Subsingleton (CategoryTheory.Abelian.Ext X Y i)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
addRightReflectLT_of_addLeftReflectLT : ∀ (N : Type u_2) [inst : AddCommSemigroup N] [inst_1 : LT N] [AddLeftReflectLT N], AddRightReflectLT N
-- Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
/-- The minimal polynomial of `x : L` over `K` agrees with its minimal polynomial over the
integrally closed subring `A`.  -/
minpoly.ofSubring : ∀ {K : Type u_3} {L : Type u_4} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (A : Subring K)
  [IsIntegrallyClosed ↥A] [IsFractionRing (↥A) K] (x : ↥(integralClosure (↥A) L)),
  Polynomial.map (algebraMap (↥A) K) (minpoly (↥A) x) = minpoly K ↑x
-- Mathlib.Combinatorics.Enumerative.Partition.Glaisher
Nat.Partition.powerSeriesMk_card_restricted_eq_powerSeriesMk_card_countRestricted : ∀ (R : Type u_1) [inst : CommRing R] [NoZeroDivisors R] {m : ℕ},
  0 < m →
    (PowerSeries.mk fun n => ↑(Nat.Partition.restricted n fun x => ¬m ∣ x).card) =
      PowerSeries.mk fun n => ↑(Nat.Partition.countRestricted n m).card
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.shortComplexH0_g : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{max u u_1, u, u} k G),
  (groupCohomology.shortComplexH0 A).g = groupCohomology.d₀₁ A
-- Mathlib.Algebra.Group.Subgroup.Finsupp
Subgroup.exists_finsupp_of_mem_closure_range : ∀ {M : Type u_1} [inst : CommGroup M] {ι : Type u_2} (f : ι → M),
  ∀ x ∈ Subgroup.closure (Set.range f), ∃ a, x = a.prod fun x1 x2 => f x1 ^ x2
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.homology_π_ι : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} {K : HomologicalComplex C c} (i : ι) [inst_2 : K.HasHomology i],
  CategoryTheory.CategoryStruct.comp (K.homologyπ i) (K.homologyι i) =
    CategoryTheory.CategoryStruct.comp (K.iCycles i) (K.pOpcycles i)
-- Mathlib.Probability.Moments.SubGaussian
ProbabilityTheory.HasSubgaussianMGF.const_mul : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {c : NNReal},
  ProbabilityTheory.HasSubgaussianMGF X c μ →
    ∀ (r : ℝ), ProbabilityTheory.HasSubgaussianMGF (fun ω => r * X ω) (⟨r ^ 2, ⋯⟩ * c) μ
-- Mathlib.RingTheory.Adjoin.PowerBasis
/-- If `x` generates `S` over `K` and is integral over `K`, then it defines a power basis.
See `PowerBasis.ofAdjoinEqTop'` for a version over a more general base ring.
 -/
PowerBasis.ofAdjoinEqTop : {K : Type u_1} →
  {S : Type u_2} →
    [inst : Field K] →
      [inst_1 : CommRing S] → [inst_2 : Algebra K S] → {x : S} → IsIntegral K x → K[x] = ⊤ → PowerBasis K S
-- Mathlib.Tactic.CategoryTheory.Bicategory.Datatypes
/-- The codomain of a morphism.  -/
Mathlib.Tactic.Bicategory.tgtExpr : Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Combinatorics.SimpleGraph.VertexCover
SimpleGraph.isVertexCover_image_iso : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} (f : G ≃g H) {c : Set V},
  H.IsVertexCover (⇑f '' c) ↔ G.IsVertexCover c
-- Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
/-- `C` has all wide pullbacks for any Finite `J`  -/
CategoryTheory.Limits.HasFiniteWidePullbacks.out : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.Limits.HasFiniteWidePullbacks C]
  (J : Type) [Finite J], CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WidePullbackShape J) C
-- Mathlib.Computability.TuringMachine.Computable
Turing.FinTM2.step.eq_1 : ∀ (tm : Turing.FinTM2), tm.step = Turing.TM2.step tm.m
-- Mathlib.NumberTheory.ModularForms.Cusps
/-- The action of `𝒢` on its own cusps.  -/
cuspsSubMulAction : (𝒢 : Subgroup (GL (Fin 2) ℝ)) → SubMulAction (↥𝒢) (OnePoint ℝ)
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.Code.matchExpr.sizeOf_spec : ∀ (ref : Lean.Syntax) («meta» : Bool) (discr : Lean.Syntax)
  (alts : Array (Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code)) (elseBranch : Lean.Elab.Term.Do.Code),
  sizeOf (Lean.Elab.Term.Do.Code.matchExpr ref «meta» discr alts elseBranch) =
    1 + sizeOf ref + sizeOf «meta» + sizeOf discr + sizeOf alts + sizeOf elseBranch
-- Mathlib.Analysis.Normed.Group.Defs
NormedCommGroup.mk : {E : Type u_8} →
  [toNorm : Norm E] →
    [toCommGroup : CommGroup E] →
      [toMetricSpace : MetricSpace E] →
        autoParam (∀ (x y : E), dist x y = ‖x⁻¹ * y‖) NormedCommGroup.dist_eq._autoParam → NormedCommGroup E
-- Lean.Meta.AppBuilder
/-- Returns `id e`  -/
Lean.Meta.mkId : Lean.Expr → Lean.MetaM Lean.Expr
-- Init.Data.BitVec.Lemmas
BitVec.lt_asymm : ∀ {n : ℕ} {x y : BitVec n}, x < y → ¬y < x
-- Mathlib.ModelTheory.PartialEquiv
FirstOrder.Language.DirectLimit.dom_partialEquivLimit : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N] {ι : Type u_1}
  [inst_2 : Preorder ι] [inst_3 : Nonempty ι] [inst_4 : IsDirectedOrder ι] (S : ι →o L.PartialEquiv M N),
  (FirstOrder.Language.DirectLimit.partialEquivLimit S).dom = ⨆ x, (S x).dom
-- Mathlib.Order.SuccPred.Basic
Order.pred_lt : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : PredOrder α] [NoMinOrder α] (a : α), Order.pred a < a
-- Init.Data.UInt.Bitwise
UInt8.xor_comm : ∀ (a b : UInt8), a ^^^ b = b ^^^ a
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.Compacts.ext : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s t : TopologicalSpace.Compacts α}, ↑s = ↑t → s = t
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F.leftOp : Cᵒᵖ ⥤ D` reflects finite colimits, then `F : C ⥤ Dᵒᵖ` reflects finite
limits.  -/
CategoryTheory.Limits.reflectsFiniteLimits_of_leftOp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C Dᵒᵖ) [CategoryTheory.Limits.ReflectsFiniteColimits F.leftOp],
  CategoryTheory.Limits.ReflectsFiniteLimits F
-- Mathlib.CategoryTheory.FiberedCategory.Cartesian
/-- A morphism `φ : a ⟶ b` in `𝒳` lying over `f : R ⟶ S` in `𝒮` is Cartesian if for all
morphisms `φ' : a' ⟶ b`, also lying over `f`, there exists a unique morphism `χ : a' ⟶ a` lifting
`𝟙 R` such that `φ' = χ ≫ φ`.

See SGA 1 VI 5.1.  -/
CategoryTheory.Functor.IsCartesian : {𝒮 : Type u₁} →
  {𝒳 : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳] →
        CategoryTheory.Functor 𝒳 𝒮 → {R S : 𝒮} → {a b : 𝒳} → (R ⟶ S) → (a ⟶ b) → Prop
-- Mathlib.Tactic.NormNum.Prime
Mathlib.Meta.NormNum.minFacHelper_2 : ∀ {n k k' : ℕ},
  k + 2 = k' → ¬Nat.Prime k → Mathlib.Meta.NormNum.MinFacHelper n k → Mathlib.Meta.NormNum.MinFacHelper n k'
-- Mathlib.Algebra.BigOperators.Fin
Fin.sum_univ_five : ∀ {M : Type u_2} [inst : AddCommMonoid M] (f : Fin 5 → M), ∑ i, f i = f 0 + f 1 + f 2 + f 3 + f 4
-- Mathlib.Tactic.Widget.StringDiagram
/-- Given an equality between 2-morphisms, return a string diagram of the LHS and RHS.
Otherwise `none`.  -/
Mathlib.Tactic.Widget.StringDiagram.stringEqM? : Lean.Expr → Lean.MetaM (Option ProofWidgets.Html)
-- Std.Data.TreeMap.Raw.Basic
/-- Removes all mappings of the map for which the given function returns `false`.  -/
Std.TreeMap.Raw.filter : {α : Type u} →
  {β : Type v} → {cmp : α → α → Ordering} → (α → β → Bool) → Std.TreeMap.Raw α β cmp → Std.TreeMap.Raw α β cmp
-- Mathlib.Algebra.BigOperators.Finprod
finprod_cond_eq_right : ∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] {f : α → M} {a : α}, ∏ᶠ (i : α) (_ : a = i), f i = f a
-- Init.Data.List.TakeDrop
List.take_concat_get : ∀ {α : Type u_1} {l : List α} {i : ℕ} (h : i < l.length), (List.take i l).concat l[i] = List.take (i + 1) l
-- Mathlib.Algebra.Homology.ShortComplex.QuasiIso
CategoryTheory.ShortComplex.quasiIso_unopMap : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex Cᵒᵖ} [inst_2 : S₁.HasHomology] [inst_3 : S₂.HasHomology]
  [inst_4 : S₁.unop.HasHomology] [inst_5 : S₂.unop.HasHomology] (φ : S₁ ⟶ S₂) [CategoryTheory.ShortComplex.QuasiIso φ],
  CategoryTheory.ShortComplex.QuasiIso (CategoryTheory.ShortComplex.unopMap φ)
-- Mathlib.NumberTheory.Padics.PadicVal.Basic
range_pow_padicValNat_subset_divisors' : ∀ {p n : ℕ} [hp : Fact (Nat.Prime p)],
  Finset.image (fun t => p ^ (t + 1)) (Finset.range (padicValNat p n)) ⊆ n.divisors.erase 1
-- Mathlib.GroupTheory.SpecificGroups.Dihedral
/-- If n is odd, then the Dihedral group of order $2n$ has $n(n+3)$ pairs (represented as
$n + n + n + n*n$) of commuting elements.  -/
DihedralGroup.oddCommuteEquiv : {n : ℕ} → Odd n → { p // Commute p.1 p.2 } ≃ ZMod n ⊕ ZMod n ⊕ ZMod n ⊕ ZMod n × ZMod n
-- Mathlib.Analysis.InnerProductSpace.NormDet
LinearMap.normDet_codRestrict : ∀ {𝕜 : Type u_1} {U : Type u_2} {V : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup U]
  [inst_2 : InnerProductSpace 𝕜 U] [inst_3 : FiniteDimensional 𝕜 U] [inst_4 : NormedAddCommGroup V]
  [inst_5 : InnerProductSpace 𝕜 V] {p : Submodule 𝕜 V} {f : U →ₗ[𝕜] V} (h : ∀ (c : U), f c ∈ p),
  (LinearMap.codRestrict p f h).normDet = f.normDet
-- Mathlib.Order.Filter.Basic
/-- See `EventuallyEq.comp_tendsto` in Mathlib.Order.Filter.Tendsto for a similar statement w.r.t.
composition on the right.  -/
Filter.EventuallyEq.fun_comp : ∀ {α : Type u} {β : Type v} {γ : Type w} {f g : α → β} {l : Filter α}, f =ᶠ[l] g → ∀ (h : β → γ), h ∘ f =ᶠ[l] h ∘ g
-- Mathlib.Algebra.EuclideanDomain.Basic
EuclideanDomain.div_dvd_of_dvd : ∀ {R : Type u} [inst : EuclideanDomain R] {p q : R}, q ∣ p → p / q ∣ p
-- Mathlib.Algebra.Category.Semigrp.Basic
MagmaCat.inv_hom_apply : ∀ {M N : MagmaCat} (e : M ≅ N) (x : ↑M),
  (CategoryTheory.ConcreteCategory.hom e.inv) ((CategoryTheory.ConcreteCategory.hom e.hom) x) = x
-- Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
IsPrimitiveRoot.embeddingsEquivPrimitiveRoots.congr_simp : ∀ {n : ℕ} [inst : NeZero n] {K : Type u} {L : Type v} [inst_1 : Field K] [inst_2 : CommRing L] [inst_3 : IsDomain L]
  [inst_4 : Algebra K L] [inst_5 : IsCyclotomicExtension {n} K L] {ζ ζ_1 : L} (e_ζ : ζ = ζ_1) (hζ : IsPrimitiveRoot ζ n)
  (C : Type u_1) [inst_6 : CommRing C] [inst_7 : IsDomain C] [inst_8 : Algebra K C]
  (hirr : Irreducible (Polynomial.cyclotomic n K)),
  hζ.embeddingsEquivPrimitiveRoots C hirr = ⋯.embeddingsEquivPrimitiveRoots C hirr
-- Init.ShareCommon
ShareCommonT : ShareCommon.StateFactory → (Type u → Type v) → Type u → Type (max u v)
-- Init.Grind.Module.Envelope
_private.Init.Grind.Module.Envelope.0.Lean.Grind.IntModule.OfNatModule.exists_true : ∀ (α : Type u) [Lean.Grind.NatModule α], ∃ x, True
-- Mathlib.Algebra.Star.StarRingHom
StarRingEquiv.mk.inj : ∀ {A : Type u_1} {B : Type u_2} {inst : Add A} {inst_1 : Add B} {inst_2 : Mul A} {inst_3 : Mul B} {inst_4 : Star A}
  {inst_5 : Star B} {toRingEquiv : A ≃+* B}
  {map_star' : ∀ (a : A), toRingEquiv.toFun (star a) = star (toRingEquiv.toFun a)} {toRingEquiv_1 : A ≃+* B}
  {map_star'_1 : ∀ (a : A), toRingEquiv_1.toFun (star a) = star (toRingEquiv_1.toFun a)},
  { toRingEquiv := toRingEquiv, map_star' := map_star' } = { toRingEquiv := toRingEquiv_1, map_star' := map_star'_1 } →
    toRingEquiv = toRingEquiv_1
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
MeasureTheory.FiniteMeasure.ennreal_coeFn_eq_coeFn_toMeasure : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] (ν : MeasureTheory.FiniteMeasure Ω) (s : Set Ω), ↑(ν s) = ↑ν s
-- Mathlib.LinearAlgebra.Dimension.Free
Module.finrank_div_finrank_cancel_left : ∀ (F : Type u) (K : Type v) (A : Type w) [inst : Semiring F] [inst_1 : Semiring K] [inst_2 : AddCommMonoid A]
  [inst_3 : Module F K] [inst_4 : Module K A] [inst_5 : Module F A] [IsScalarTower F K A] [StrongRankCondition F]
  [StrongRankCondition K] [Module.Free F K] [Module.Free K A],
  Module.finrank F K ≠ 0 → Module.finrank F A / Module.finrank F K = Module.finrank K A
-- Mathlib.Algebra.Order.CompleteField
/-- Preparatory lemma for `inducedOrderRingHom`.  -/
ConditionallyCompleteLinearOrderedField.le_inducedMap_mul_self_of_mem_cutMap : ∀ {α : Type u_2} {β : Type u_3} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [inst_3 : Field β]
  [inst_4 : ConditionallyCompleteLinearOrder β] [IsStrictOrderedRing β] [Archimedean α] {a : α},
  0 < a →
    ∀ b ∈ LinearOrderedField.cutMap β (a * a),
      b ≤
        ConditionallyCompleteLinearOrderedField.inducedMap α β a *
          ConditionallyCompleteLinearOrderedField.inducedMap α β a
-- Lean.Meta.Tactic.Grind.PP
/-- Returns `true` if `e` is an expression constructed using numerals,
`grind` cast-like operations, and arithmetic terms. Moreover, the
expression contains at least one cast-like application.
This kind of term is constructed by `grind` satellite solvers.
 -/
_private.Lean.Meta.Tactic.Grind.PP.0.Lean.Meta.Grind.isArithOfCastLike : Lean.Expr → Bool
-- Lean.Parser.Types
/-- Extracts a substring of the input string, bounded by `startPos` and `stopPos`.
 -/
Lean.Parser.InputContext.substring : Lean.Parser.InputContext → String.Pos.Raw → String.Pos.Raw → Substring.Raw
-- Std.Time.Duration
/-- Adds a `Millisecond.Offset` to a `Duration`
 -/
Std.Time.Duration.addMilliseconds : Std.Time.Duration → Std.Time.Millisecond.Offset → Std.Time.Duration
-- Mathlib.Order.Defs.LinearOrder
min_left_comm : ∀ {α : Type u_1} [inst : LinearOrder α] (a b c : α), min a (min b c) = min b (min a c)
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
LinearMap.mul_toMatrix₂_mul : ∀ {R : Type u_1} {M₁ : Type u_6} {M₂ : Type u_7} {M₁' : Type u_8} {M₂' : Type u_9} {n : Type u_11} {m : Type u_12}
  {n' : Type u_13} {m' : Type u_14} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁] [inst_2 : Module R M₁]
  [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M₂] [inst_5 : Fintype n] [inst_6 : Fintype m] [inst_7 : DecidableEq m]
  [inst_8 : DecidableEq n] (b₁ : Module.Basis n R M₁) (b₂ : Module.Basis m R M₂) [inst_9 : AddCommMonoid M₁']
  [inst_10 : Module R M₁'] [inst_11 : AddCommMonoid M₂'] [inst_12 : Module R M₂'] (b₁' : Module.Basis n' R M₁')
  (b₂' : Module.Basis m' R M₂') [inst_13 : Fintype n'] [inst_14 : Fintype m'] [inst_15 : DecidableEq n']
  [inst_16 : DecidableEq m'] (B : M₁ →ₗ[R] M₂ →ₗ[R] R) (M : Matrix n' n R) (N : Matrix m m' R),
  M * (LinearMap.toMatrix₂ b₁ b₂) B * N =
    (LinearMap.toMatrix₂ b₁' b₂') (B.compl₁₂ ((Matrix.toLin b₁' b₁) M.transpose) ((Matrix.toLin b₂' b₂) N))
-- Mathlib.Analysis.Distribution.TestFunction
TestFunction.monoCLM_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] {Ω₁ Ω₂ : TopologicalSpace.Opens E} {F : Type u_4} [inst_3 : NormedAddCommGroup F]
  [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace 𝕜 F] {n₁ n₂ : ℕ∞} [inst_6 : Algebra ℝ 𝕜]
  [inst_7 : IsScalarTower ℝ 𝕜 F] (f : TestFunction Ω₁ F n₁),
  ⇑((TestFunction.monoCLM 𝕜) f) = ⇑(if n₂ ≤ n₁ ∧ Ω₁ ≤ Ω₂ then f else 0)
-- Lean.Elab.Level
Lean.Elab.Level.instMonadRefLevelElabM : Lean.MonadRef Lean.Elab.Level.LevelElabM
-- Mathlib.MeasureTheory.VectorMeasure.SetIntegral
MeasureTheory.VectorMeasure.enorm_setIntegral_le_lintegral_enorm : ∀ {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedAddCommGroup G] {μ : MeasureTheory.VectorMeasure X F} {f : X → E}
  {s : Set X} [inst_3 : NormedSpace ℝ E] [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G},
  ‖∫ᵛ (x : X) in s, f x ∂[B; μ]‖ₑ ≤ ‖B‖ₑ * ∫⁻ (x : X) in s, ‖f x‖ₑ ∂μ.variation
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.closure_union : ∀ {R : Type u} [inst : NonAssocRing R] (s t : Set R), Subring.closure (s ∪ t) = Subring.closure s ⊔ Subring.closure t
-- Mathlib.CategoryTheory.Groupoid.FreeGroupoid
Quiver.FreeGroupoid.lift_spec : ∀ {V : Type u} [inst : Quiver V] {V' : Type u'} [inst_1 : CategoryTheory.Groupoid V'] (φ : V ⥤q V'),
  Quiver.FreeGroupoid.of V ⋙q (Quiver.FreeGroupoid.lift φ).toPrefunctor = φ
-- Mathlib.CategoryTheory.Category.Cat.Limit
CategoryTheory.Cat.HasLimits.limitCone_pt : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CategoryTheory.Cat),
  (CategoryTheory.Cat.HasLimits.limitCone F).pt = CategoryTheory.Cat.HasLimits.limitConeX F
-- Init.Data.Int.DivMod.Lemmas
Int.one_bmod : ∀ {b : ℕ}, 3 ≤ b → Int.bmod 1 b = 1
-- Std.Sat.AIG.RefVec
Std.Sat.AIG.RefVec.get_push_ref_eq' : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {aig : Std.Sat.AIG α} {len : ℕ} (s : aig.RefVec len)
  (ref : aig.Ref) (idx : ℕ) (hidx : idx = len), (s.push ref).get idx ⋯ = ref
-- Mathlib.Algebra.BigOperators.Group.Finset.Sigma
Finset.prod_finset_product_right' : ∀ {α : Type u_3} {β : Type u_4} {γ : Type u_5} [inst : CommMonoid β] (r : Finset (α × γ)) (s : Finset γ)
  (t : γ → Finset α),
  (∀ (p : α × γ), p ∈ r ↔ p.2 ∈ s ∧ p.1 ∈ t p.2) → ∀ {f : α → γ → β}, ∏ p ∈ r, f p.1 p.2 = ∏ c ∈ s, ∏ a ∈ t c, f a c
-- Mathlib.CategoryTheory.Monoidal.Bimon_
CategoryTheory.Bimon.ofMonComonObj_comon_counit_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (M : CategoryTheory.Mon (CategoryTheory.Comon C)),
  CategoryTheory.ComonObj.counit.hom = CategoryTheory.ComonObj.counit
-- Mathlib.Analysis.Normed.Group.Basic
/-- **Alias** of `mem_eball_one_iff`. -/
mem_emetric_ball_one_iff : ∀ {E : Type u_5} [inst : SeminormedGroup E] {a : E} {r : ENNReal}, a ∈ Metric.eball 1 r ↔ ‖a‖ₑ < r
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
/-- Given `x, y : E ⊗ F ⊗ G`, `x = y` iff `⟪x, a ⊗ₜ b ⊗ₜ c⟫ = ⟪y, a ⊗ₜ b ⊗ₜ c⟫` for all `a, b, c`.

See also `ext_iff_inner_right_threefold'` for when `x, y : E ⊗ (F ⊗ G)`.  -/
TensorProduct.ext_iff_inner_right_threefold : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : InnerProductSpace 𝕜 G] {x y : TensorProduct 𝕜 (TensorProduct 𝕜 E F) G},
  x = y ↔ ∀ (a : E) (b : F) (c : G), inner 𝕜 x (a ⊗ₜ[𝕜] b ⊗ₜ[𝕜] c) = inner 𝕜 y (a ⊗ₜ[𝕜] b ⊗ₜ[𝕜] c)
-- Aesop.Tree.Tracing
Aesop.Goal.traceTreeCore : Aesop.Goal → Aesop.TraceOption → Lean.MetaM Unit
-- Mathlib.CategoryTheory.Shift.ShiftSequence
CategoryTheory.Functor.ShiftSequence.shiftIso_zero : ∀ {C : Type u_1} {A : Type u_3} {inst : CategoryTheory.Category.{v_1, u_1} C}
  {inst_1 : CategoryTheory.Category.{v_3, u_3} A} {F : CategoryTheory.Functor C A} {M : Type u_4} {inst_2 : AddMonoid M}
  {inst_3 : CategoryTheory.HasShift C M} [self : F.ShiftSequence M] (a : M),
  CategoryTheory.Functor.ShiftSequence.shiftIso 0 a a ⋯ =
    CategoryTheory.Functor.isoWhiskerRight (CategoryTheory.shiftFunctorZero C M)
        (CategoryTheory.Functor.ShiftSequence.sequence F a) ≪≫
      (CategoryTheory.Functor.ShiftSequence.sequence F a).leftUnitor
-- Mathlib.Analysis.Complex.Basic
Complex.re_nonneg_iff_nonneg : ∀ {x : ℂ}, IsSelfAdjoint x → (0 ≤ x.re ↔ 0 ≤ x)
-- Init.Data.Option.Lemmas
Option.get_bind : ∀ {α : Type u_1} {β : Type u_2} {x : Option α} {f : α → Option β} (h : (x.bind f).isSome = true),
  (x.bind f).get h = (f (x.get ⋯)).get ⋯
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.getD_insert : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {k a fallback : α},
  (t.insert k).getD a fallback = if cmp k a = Ordering.eq ∧ k ∉ t then k else t.getD a fallback
-- Mathlib.Algebra.FreeAlgebra.Cardinality
Algebra.cardinalMk_adjoin_le : ∀ (R : Type u) [inst : CommSemiring R] {A : Type u} [inst_1 : Semiring A] [inst_2 : Algebra R A] (s : Set A),
  Cardinal.mk ↥(Algebra.adjoin R s) ≤ max (max (Cardinal.mk R) (Cardinal.mk ↑s)) Cardinal.aleph0
-- Mathlib.Order.Hom.Basic
/-- `OrderHomClass F α b` asserts that `F` is a type of `≤`-preserving morphisms.  -/
OrderHomClass : (F : Type u_6) → (α : outParam (Type u_7)) → (β : outParam (Type u_8)) → [LE α] → [LE β] → [FunLike F α β] → Prop
-- Mathlib.CategoryTheory.Sums.Products
CategoryTheory.Sum.associativityFunctorEquivNaturalityFunctorIso_hom_app_snd_snd : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {A' : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} A'] {B : Type u} [inst_2 : CategoryTheory.Category.{v, u} B]
  (T : Type u_3) [inst_3 : CategoryTheory.Category.{v_3, u_3} T] (X : CategoryTheory.Functor ((A ⊕ A') ⊕ T) B),
  ((CategoryTheory.Sum.associativityFunctorEquivNaturalityFunctorIso T).hom.app X).2.2 =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Sum.inr_ A' T).whiskerLeft
        ((CategoryTheory.Sum.inr_ A (A' ⊕ T)).associator (CategoryTheory.sum.inverseAssociator A A' T) X).inv)
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.Sum.inr_ A' T).associator
            ((CategoryTheory.Sum.inr_ A (A' ⊕ T)).comp (CategoryTheory.sum.inverseAssociator A A' T)) X).inv
        (CategoryTheory.Functor.whiskerRight (CategoryTheory.sum.inrCompInrCompInverseAssociator A A' T).hom X))
-- Mathlib.Analysis.Calculus.LineDeriv.Basic
lineDerivWithin.eq_1 : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type u_3} [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] (f : E → F) (s : Set E)
  (x v : E), lineDerivWithin 𝕜 f s x v = derivWithin (fun t => f (x + t • v)) ((fun t => x + t • v) ⁻¹' s) 0
-- Mathlib.AlgebraicGeometry.RelativeGluing
/-- A relative gluing datum over a locally directed cover `𝒰` of `S` is a scheme `Xᵢ` for every
`i : 𝒰.I₀` and natural maps `Xᵢ ⟶ Uᵢ` such that for every `i ⟶ j`, the diagram
```
Xᵢ --> Uᵢ
|      |
v      v
Xⱼ --> Uⱼ
```
is a pullback square. We bundle this in the form of a functor and an equifibered natural
transformation.
The `Xᵢ` then glue to a scheme over `S`
(see `AlgebraicGeometry.Scheme.Cover.RelativeGluingData.glued`).
 -/
AlgebraicGeometry.Scheme.Cover.RelativeGluingData : {S : AlgebraicGeometry.Scheme} →
  (𝒰 : S.OpenCover) →
    [inst : CategoryTheory.Category.{u_2, u_1} 𝒰.I₀] →
      [AlgebraicGeometry.Scheme.Cover.LocallyDirected 𝒰] → Type (max (max (u + 1) u_1) u_2)
-- Mathlib.SetTheory.Cardinal.Cofinality.Enum
StrictMono.orderIso.congr_simp : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : Preorder β] (f : α → β) (h_mono : StrictMono f),
  StrictMono.orderIso f h_mono = StrictMono.orderIso f h_mono
-- Mathlib.Algebra.ContinuedFractions.Translations
GenContFract.zeroth_den_eq_one : ∀ {K : Type u_1} {g : GenContFract K} [inst : DivisionRing K], g.dens 0 = 1
-- Lean.Util.MonadCache
Lean.MonadCacheT.instAlternative : {ω α β : Type} →
  {m : Type → Type} →
    [inst : STWorld ω m] →
      [inst_1 : BEq α] → [inst_2 : Hashable α] → [Monad m] → [Alternative m] → Alternative (Lean.MonadCacheT α β m)
-- Mathlib.Topology.Algebra.Valued.ValuedField
/-- The zero-preserving monoid homomorphism from the `ValueGroup₀` of the valuation on `K` to
that of the extension to its completion.  -/
Valued.valueGroup₀_equiv_extensionValuation : {K : Type u_1} →
  [inst : Field K] →
    {Γ₀ : Type u_2} →
      [inst_1 : LinearOrderedCommGroupWithZero Γ₀] →
        [hv : Valued K Γ₀] →
          (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ ≃*
            (MonoidWithZeroHom.ofClass Valued.extensionValuation).ValueGroup₀
-- Mathlib.RingTheory.Spectrum.Maximal.Localization
PrimeSpectrum.piLocalizationToMaximal_bijective : ∀ {R : Type u_1} [inst : CommSemiring R],
  (∀ (I : Ideal R), I.IsPrime → I.IsMaximal) → Function.Bijective ⇑(PrimeSpectrum.piLocalizationToMaximal R)
-- Lean.Elab.MutualInductive
Lean.Elab.Command.ElabHeaderResult.indFVar : Lean.Elab.Command.ElabHeaderResult → Lean.Expr
-- Mathlib.Combinatorics.Additive.ErdosGinzburgZiv
/-- The **Erdős–Ginzburg–Ziv theorem** for `ℤ/nℤ`.

Any sequence of at least `2 * n - 1` elements of `ZMod n` contains a subsequence of `n` elements
whose sum is zero.  -/
ZMod.erdos_ginzburg_ziv : ∀ {ι : Type u_1} {n : ℕ} {s : Finset ι} (a : ι → ZMod n), 2 * n - 1 ≤ s.card → ∃ t ⊆ s, t.card = n ∧ ∑ i ∈ t, a i = 0