mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.map_iInf : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] {K : Type u_3}
  [inst_3 : Field K] [inst_4 : Algebra F K] {ι : Sort u_4} [Nonempty ι] (f : E →ₐ[F] K) (s : ι → IntermediateField F E),
  IntermediateField.map f (iInf s) = ⨅ i, IntermediateField.map f (s i)
-- Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
/-- If `P` and `Q` are stable under base change and pullbacks along `f` exist for morphisms in `P`,
this is the functor `P.Over Q Y ⥤ P.Over Q X` given by base change along `f`.  -/
CategoryTheory.MorphismProperty.Over.pullback : {T : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} T] →
    (P Q : CategoryTheory.MorphismProperty T) →
      [inst_1 : Q.IsMultiplicative] →
        {X Y : T} →
          (f : X ⟶ Y) →
            [P.HasPullbacksAlong f] →
              [P.IsStableUnderBaseChangeAlong f] →
                [Q.IsStableUnderBaseChange] → CategoryTheory.Functor (P.Over Q Y) (P.Over Q X)
-- Init.Data.Nat.MinMax
Nat.le_max_left : ∀ (a b : ℕ), a ≤ max a b
-- Init.Data.List.Find
List.head_flatten : ∀ {α : Type u_1} {L : List (List α)} (h : ∃ l ∈ L, l ≠ []), L.flatten.head ⋯ = (List.findSome? List.head? L).get ⋯
-- Mathlib.Geometry.Manifold.PartitionOfUnity
/-- Let `M` be a smooth manifold modelled on a finite-dimensional real vector space.
Suppose also that `M` is a Hausdorff `σ`-compact topological space. Let `s` be a closed set
in `M` and `U : M → Set M` be a collection of sets such that `U x ∈ 𝓝 x` for every `x ∈ s`.
Then there exists a smooth bump covering of `s` that is subordinate to `U`.  -/
SmoothBumpCovering.exists_isSubordinate : ∀ {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH} [inst_2 : TopologicalSpace H]
  (I : ModelWithCorners ℝ E H) {M : Type uM} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M]
  [inst_5 : FiniteDimensional ℝ E] {s : Set M} {U : M → Set M} [T2Space M] [SigmaCompactSpace M],
  IsClosed s → (∀ x ∈ s, U x ∈ nhds x) → ∃ ι f, f.IsSubordinate U
-- Mathlib.Analysis.LocallyConvex.Bounded
TotallyBounded.isVonNBounded : ∀ (𝕜 : Type u_1) {E : Type u_3} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : UniformSpace E] [IsUniformAddGroup E] [ContinuousSMul 𝕜 E] {s : Set E},
  TotallyBounded s → Bornology.IsVonNBounded 𝕜 s
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.yonedaEquiv_const : ∀ {X : SSet} (x : X.obj (Opposite.op { len := 0 })), SSet.yonedaEquiv (SSet.const x) = x
-- Std.Data.Iterators.Lemmas.Combinators.Zip
_private.Std.Data.Iterators.Lemmas.Combinators.Zip.0.Std.Iter.atIdxSlow?.match_3.splitter : {α β : Type u_1} →
  [inst : Std.Iterator α Id β] →
    (it : Std.Iter β) →
      (motive : it.Step → Sort u_2) →
        (x : it.Step) →
          ((it' : Std.Iter β) →
              (out : β) →
                (property : it.IsPlausibleStep (Std.IterStep.yield it' out)) →
                  motive ⟨Std.IterStep.yield it' out, property⟩) →
            ((it' : Std.Iter β) →
                (property : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', property⟩) →
              ((property : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, property⟩) → motive x
-- Mathlib.MeasureTheory.Measure.MeasureSpaceDef
MeasureTheory.exists_measure_pos_of_not_measure_iUnion_null : ∀ {α : Type u_1} {ι : Sort u_5} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [Countable ι] {s : ι → Set α},
  μ (⋃ n, s n) ≠ 0 → ∃ n, 0 < μ (s n)
-- Mathlib.NumberTheory.BernoulliPolynomials
Polynomial.bernoulli_comp_one_sub_X : ∀ (n : ℕ), (Polynomial.bernoulli n).comp (1 - Polynomial.X) = (-1) ^ n * Polynomial.bernoulli n
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get!_diff! : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {m₁ m₂ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  [inst : Inhabited β],
  m₁.WF →
    m₂.WF →
      ∀ {k : α},
        Std.DTreeMap.Internal.Impl.Const.get! (m₁.diff! m₂) k =
          if Std.DTreeMap.Internal.Impl.contains k m₂ = true then default
          else Std.DTreeMap.Internal.Impl.Const.get! m₁ k
-- Lean.Meta.Sym.Canon
_private.Lean.Meta.Sym.Canon.0.Lean.Meta.Sym.Canon.isNat : Lean.Expr → Bool
-- Mathlib.AlgebraicTopology.SimplicialObject.II
SimplexCategory.II.map'.eq_1 : ∀ {n m : ℕ} (f : Fin (n + 1) →o Fin (m + 1)) (x : Fin (m + 2)),
  SimplexCategory.II.map' f x = (SimplexCategory.II.finset f x).min' ⋯
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.map_sup : ∀ {α : Type u_2} {β : Type u_3} [inst : BooleanAlgebra α] [inst_1 : BooleanAlgebra β] (f : BoundedLatticeHom α β)
  (L M : BooleanSubalgebra α), BooleanSubalgebra.map f (L ⊔ M) = BooleanSubalgebra.map f L ⊔ BooleanSubalgebra.map f M
-- Mathlib.Data.Nat.ModEq
Nat.ModEq.of_dvd : ∀ {m n a b : ℕ}, m ∣ n → a ≡ b [MOD n] → a ≡ b [MOD m]
-- Mathlib.Algebra.Torsor.Basic
/-- Dividing by the point `p` is an injective function.  -/
sdiv_left_injective : ∀ {G : Type u_1} {P : Type u_2} [inst : Group G] [T : Torsor G P] (p : P), Function.Injective fun x => x /ₛ p
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
ENNReal.zero_rpow_mul_self : ∀ (y : ℝ), 0 ^ y * 0 ^ y = 0 ^ y
-- Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
CochainComplex.mappingCone.triangle_obj₃ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {K L : CochainComplex C ℤ} (φ : K ⟶ L),
  (CochainComplex.mappingCone.triangle φ).obj₃ = CochainComplex.mappingCone φ
-- Mathlib.Algebra.Module.LinearMap.Polynomial
LinearMap.toMvPolynomial_zero : ∀ {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} {ι₁ : Type u_4} {ι₂ : Type u_5} [inst : CommRing R]
  [inst_1 : AddCommGroup M₁] [inst_2 : AddCommGroup M₂] [inst_3 : Module R M₁] [inst_4 : Module R M₂]
  [inst_5 : Fintype ι₁] [inst_6 : Finite ι₂] [inst_7 : DecidableEq ι₁] (b₁ : Module.Basis ι₁ R M₁)
  (b₂ : Module.Basis ι₂ R M₂), LinearMap.toMvPolynomial b₁ b₂ 0 = 0
-- Std.Async.Basic
/-- Converts `Except` to `Async`.
 -/
Std.Async.Async.ofExcept : {α : Type} → Except IO.Error α → Std.Async.Async α
-- Mathlib.MeasureTheory.Constructions.HaarToSphere
MeasureTheory.Measure.toSphere_apply_univ : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E]
  (μ : MeasureTheory.Measure E) [BorelSpace E] [FiniteDimensional ℝ E] [μ.IsAddHaarMeasure],
  μ.toSphere Set.univ = ↑(Module.finrank ℝ E) * μ (Metric.ball 0 1)
-- Mathlib.Algebra.Homology.TotalComplex
HomologicalComplex₂.total.mapAux.d₂_mapMap : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {I₁ : Type u_2}
  {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {K L : HomologicalComplex₂ C c₁ c₂}
  (φ : K ⟶ L) (c₁₂ : ComplexShape I₁₂) [inst_2 : TotalComplexShape c₁ c₂ c₁₂] [inst_3 : DecidableEq I₁₂]
  [inst_4 : K.HasTotal c₁₂] [inst_5 : L.HasTotal c₁₂] (i₁ : I₁) (i₂ : I₂) (i₁₂ : I₁₂),
  CategoryTheory.CategoryStruct.comp (K.d₂ c₁₂ i₁ i₂ i₁₂)
      (CategoryTheory.GradedObject.mapMap (HomologicalComplex₂.toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂) =
    CategoryTheory.CategoryStruct.comp ((φ.f i₁).f i₂) (L.d₂ c₁₂ i₁ i₂ i₁₂)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.union_eq : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : α → Type v} {m₁ m₂ : Std.DHashMap.Raw α β},
  m₁.union m₂ = m₁ ∪ m₂
-- Mathlib.Algebra.Order.Nonneg.Basic
Nonneg.mk_add_mk : ∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α] [inst_2 : AddLeftMono α] {x y : α} (hx : 0 ≤ x)
  (hy : 0 ≤ y), ⟨x, hx⟩ + ⟨y, hy⟩ = ⟨x + y, ⋯⟩
-- Mathlib.Algebra.Polynomial.Bivariate
Polynomial.Bivariate.equivMvPolynomial_X : ∀ {R : Type u_1} [inst : CommSemiring R], (Polynomial.Bivariate.equivMvPolynomial R) Polynomial.X = MvPolynomial.X 1
-- Batteries.Data.UnionFind.Basic
Batteries.UnionFind.rootD_ext : ∀ {m1 m2 : Batteries.UnionFind}, (∀ (x : ℕ), m1.parent x = m2.parent x) → ∀ {x : ℕ}, m1.rootD x = m2.rootD x
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
MeasureTheory.LocallyIntegrable.indicator : ∀ {X : Type u_1} {ε'' : Type u_5} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X]
  [inst_2 : TopologicalSpace ε''] [inst_3 : ESeminormedAddMonoid ε''] {μ : MeasureTheory.Measure X} {f : X → ε''},
  MeasureTheory.LocallyIntegrable f μ →
    ∀ {s : Set X}, MeasurableSet s → MeasureTheory.LocallyIntegrable (s.indicator f) μ
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.rpow_le_iff_le_log : ∀ {x y z : ℝ}, 0 < x → 0 < y → (x ^ z ≤ y ↔ z * Real.log x ≤ Real.log y)
-- Mathlib.Order.Filter.CountableInter
/-- Supremum of two `CountableInterFilter`s is a `CountableInterFilter`.  -/
countableInterFilter_sup : ∀ {α : Type u_2} (l₁ l₂ : Filter α) [CountableInterFilter l₁] [CountableInterFilter l₂], CountableInterFilter (l₁ ⊔ l₂)
-- Mathlib.Analysis.RCLike.Basic
RCLike.conj_eq_iff_re : ∀ {K : Type u_1} [inst : RCLike K] {z : K}, (starRingEnd K) z = z ↔ ↑(RCLike.re z) = z
-- Mathlib.Tactic.NormNum.LegendreSymbol
/-- The Jacobi symbol restricted to natural numbers in both arguments.  -/
Mathlib.Meta.NormNum.jacobiSymNat : ℕ → ℕ → ℤ
-- Mathlib.NumberTheory.Cyclotomic.Basic
/-- Given a nonzero `n : ℕ` and a field `K`, we define `CyclotomicField n K` as the
splitting field of `cyclotomic n K`. If `n` is nonzero in `K`, it has
the instance `IsCyclotomicExtension {n} K (CyclotomicField n K)`.  -/
CyclotomicField : ℕ → (K : Type w) → [Field K] → Type w
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
/-- The basis on `SkewMonoidAlgebra k G` with basis vectors `fun i ↦ single i 1`  -/
SkewMonoidAlgebra.basisSingleOne : {k : Type u_1} → {G : Type u_2} → [inst : Semiring k] → Module.Basis G k (SkewMonoidAlgebra k G)
-- Mathlib.RingTheory.Flat.Equalizer
LinearMap.tensorEqLocusInv.congr_simp : ∀ {R : Type u_1} (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (M : Type u_3)
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : Module S M] [inst_6 : IsScalarTower R S M] {N : Type u_4}
  {P : Type u_5} [inst_7 : AddCommGroup N] [inst_8 : AddCommGroup P] [inst_9 : Module R N] [inst_10 : Module R P]
  (f g : N →ₗ[R] P) [inst_11 : Module.Flat R M], LinearMap.tensorEqLocusInv S M f g = LinearMap.tensorEqLocusInv S M f g
-- Std.Data.HashMap.Lemmas
Std.HashMap.isEmpty_iff_forall_not_mem : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α],
  m.isEmpty = true ↔ ∀ (a : α), a ∉ m
-- Mathlib.Analysis.Convex.Gauge
/-- **Alias** of `setOfPred_gauge_lt_one_subset_self`. -/
gauge_lt_one_subset_self : ∀ {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {s : Set E},
  Convex ℝ s → 0 ∈ s → Absorbent ℝ s → {x | gauge s x < 1} ⊆ s
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.contains_inter : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α}, (t₁ ∩ t₂).contains k = (t₁.contains k && t₂.contains k)
-- Mathlib.Algebra.MvPolynomial.CommRing
MvPolynomial.totalDegree_sub : ∀ {R : Type u} {σ : Type u_1} [inst : CommRing R] (a b : MvPolynomial σ R),
  (a - b).totalDegree ≤ max a.totalDegree b.totalDegree
-- Mathlib.AlgebraicTopology.SimplexCategory.SemiSimplexCategory
/-- The inclusion functor `SemiSimplexCategory ⥤ SimplexCategory`.  -/
SemiSimplexCategory.toSimplexCategory : CategoryTheory.Functor SemiSimplexCategory SimplexCategory
-- Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
jacobiTheta₂_undef : ∀ (z : ℂ) {τ : ℂ}, τ.im ≤ 0 → jacobiTheta₂ z τ = 0
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
NumberField.ComplexEmbedding.LiesOver.over : ∀ {K : Type u_3} {L : Type u_4} {inst : Field K} {inst_1 : Field L} {inst_2 : Algebra K L} (φ : L →+* ℂ) (ψ : K →+* ℂ)
  [self : NumberField.ComplexEmbedding.LiesOver φ ψ], φ.comp (algebraMap K L) = ψ
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.preimage_vadd_neg : ∀ {α : Type u_2} {β : Type u_3} [inst : AddGroup α] [inst_1 : AddAction α β] (a : α) (t : Set β),
  (fun x => -a +ᵥ x) ⁻¹' t = a +ᵥ t
-- Mathlib.AlgebraicTopology.SimplexCategory.Defs
/-- The fully faithful inclusion of the truncated simplex category into the usual
simplex category.
 -/
SimplexCategory.Truncated.inclusion : (n : ℕ) → CategoryTheory.Functor (SimplexCategory.Truncated n) SimplexCategory
-- Mathlib.Order.BooleanAlgebra.Basic
disjoint_compl_right_iff : ∀ {α : Type u} {x y : α} [inst : BooleanAlgebra α], Disjoint x yᶜ ↔ x ≤ y
-- Mathlib.Analysis.InnerProductSpace.Positive
LinearMap.le_def : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (f g : E →ₗ[𝕜] E), f ≤ g ↔ (g - f).IsPositive
-- Lean.Compiler.IR.Basic
Lean.IR.Alt.default.sizeOf_spec : ∀ (b : Lean.IR.FnBody), sizeOf (Lean.IR.Alt.default b) = 1 + sizeOf b
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
CategoryTheory.Bicategory.Adj.Hom₂.ext : ∀ {B : Type u} {inst : CategoryTheory.Bicategory B} {a b : CategoryTheory.Bicategory.Adj B} {α β : a ⟶ b}
  {x y : CategoryTheory.Bicategory.Adj.Hom₂ α β}, x.τl = y.τl → x.τr = y.τr → x = y
-- Mathlib.RingTheory.Unramified.Locus
/-- If `A` is an `R`-algebra unramified at `Q`, `P` is the prime of `R` lying under `Q`,
then `κ(P) ⊗ A` is unramified at `Q'` (the prime corresponding to `Q`) over `κ(P)`.  -/
Algebra.IsUnramifiedAt.residueField : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] (P : Ideal R)
  [inst_3 : P.IsPrime] (Q : Ideal A) [inst_4 : Q.IsPrime] [Q.LiesOver P] [Algebra.IsUnramifiedAt R Q]
  (Q' : Ideal (P.Fiber A)) [inst_7 : Q'.IsPrime],
  Q = Ideal.comap Algebra.TensorProduct.includeRight.toRingHom Q' → Algebra.IsUnramifiedAt P.ResidueField Q'
-- Mathlib.CategoryTheory.Subterminal
CategoryTheory.IsSubterminal.def : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A : C},
  CategoryTheory.IsSubterminal A ↔ ∀ ⦃Z : C⦄ (f g : Z ⟶ A), f = g
-- Init.Meta
Lean.termEval_prec_ : Lean.ParserDescr
-- Init.Data.String.Lemmas.FindPos
String.Pos.prevn_toSlice : ∀ {n : ℕ} {s : String} {p : s.Pos}, p.toSlice.prevn n = (p.prevn n).toSlice
-- Mathlib.CategoryTheory.ComposableArrows.Four
/-- Variant of `fourδ₃Toδ₂` for preorders.  -/
CategoryTheory.ComposableArrows.fourδ₃Toδ₂' : {ι : Type u_1} →
  [inst : Preorder ι] →
    (i₀ i₁ i₂ i₃ i₄ : ι) →
      (hi₀₁ : i₀ ≤ i₁) →
        (hi₁₂ : i₁ ≤ i₂) →
          (hi₂₃ : i₂ ≤ i₃) →
            (hi₃₄ : i₃ ≤ i₄) →
              CategoryTheory.ComposableArrows.mk₃ (CategoryTheory.homOfLE hi₀₁) (CategoryTheory.homOfLE hi₁₂)
                  (CategoryTheory.homOfLE ⋯) ⟶
                CategoryTheory.ComposableArrows.mk₃ (CategoryTheory.homOfLE hi₀₁) (CategoryTheory.homOfLE ⋯)
                  (CategoryTheory.homOfLE hi₃₄)
-- Mathlib.Analysis.Complex.Arg
Complex.sameRay_of_arg_eq : ∀ {x y : ℂ}, x.arg = y.arg → SameRay ℝ x y
-- Mathlib.NumberTheory.Cyclotomic.Basic
IntermediateField.isCyclotomicExtension_le_of_dvd : ∀ (K : Type w) (L : Type z) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (n₁ n₂ : ℕ)
  (F₁ F₂ : IntermediateField K L) [h₁ : IsCyclotomicExtension {n₁} K ↥F₁] [h₂ : IsCyclotomicExtension {n₂} K ↥F₂]
  [NeZero n₂], n₁ ∣ n₂ → F₁ ≤ F₂
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites
/-- If `F.op : Cᵒᵖ ⥤ Dᵒᵖ` creates colimits of shape `Jᵒᵖ`, then `F : C ⥤ D` creates limits
of shape `J`.  -/
CategoryTheory.Limits.createsLimitsOfShapeOfOp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (J : Type w) →
          [inst_2 : CategoryTheory.Category.{w', w} J] →
            (F : CategoryTheory.Functor C D) →
              [CategoryTheory.CreatesColimitsOfShape Jᵒᵖ F.op] → CategoryTheory.CreatesLimitsOfShape J F
-- Batteries.Data.List.Lemmas
List.isPrefixOf?.eq_2 : ∀ {α : Type u} [inst : BEq α] (x : List α), (x = [] → False) → x.isPrefixOf? [] = none
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.DocumentColorParams : Type
-- Mathlib.Algebra.Group.Subgroup.Map
MulEquiv.subgroupCongr_apply : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G} (h : H = K) (x : ↥H), ↑((MulEquiv.subgroupCongr h) x) = ↑x
-- Lean.Meta.AppBuilder
/-- Returns `propext h`  -/
Lean.Meta.mkPropExt : Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
IsPrimitiveRoot.of_subsingleton : ∀ {M : Type u_1} [inst : CommMonoid M] [Subsingleton M] (x : M), IsPrimitiveRoot x 1
-- Mathlib.Tactic.TermCongr
/-- Tries to make a congruence between `lhs` and `rhs` automatically.
1. If they are defeq, returns a trivial congruence.
2. Tries using `Subsingleton.elim`.
3. Tries `proof_irrel_heq` as another effort to avoid doing congruence on proofs.
3. Otherwise throws an error.

Note: `mkAppM` uses `withNewMCtxDepth`, which prevents typeclass inference
from accidentally specializing `Sort _` to `Prop`, which could otherwise happen
because there is a `Subsingleton Prop` instance.  -/
Mathlib.Tactic.TermCongr.CongrResult.mkDefault : Lean.Expr → Lean.Expr → Lean.MetaM Mathlib.Tactic.TermCongr.CongrResult
-- Init.Data.UInt.Lemmas
UInt16.lt_of_le_of_lt : ∀ {a b c : UInt16}, a ≤ b → b < c → a < c
-- Init.Omega.IntList
Lean.Omega.IntList.mul_def : ∀ (xs ys : Lean.Omega.IntList), xs * ys = List.zipWith (fun x1 x2 => x1 * x2) xs ys
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.maxKey_insert : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β}, (t.insert k v).maxKey ⋯ = t.maxKey?.elim k fun k' => if (cmp k' k).isLE = true then k else k'
-- Mathlib.RingTheory.Algebraic.Defs
Algebra.Transcendental.transcendental : ∀ {R : Type u} {A : Type v} {inst : CommRing R} {inst_1 : Ring A} {inst_2 : Algebra R A}
  [self : Algebra.Transcendental R A], ∃ x, Transcendental R x
-- Mathlib.Algebra.Module.CharacterModule
/-- The `ℤ`-submodule spanned by a single element `a` is isomorphic to the quotient of `ℤ`
by the ideal generated by the order of `a`.  -/
CharacterModule.intSpanEquivQuotAddOrderOf : {A : Type uA} → [inst : AddCommGroup A] → (a : A) → ↥(ℤ ∙ a) ≃ₗ[ℤ] ℤ ⧸ Ideal.span {↑(addOrderOf a)}
-- Mathlib.Data.Seq.Computation
Computation.bind_pure : ∀ {α : Type u} {β : Type v} (f : α → β) (s : Computation α), s.bind (Computation.pure ∘ f) = Computation.map f s
-- Mathlib.Order.Filter.Pointwise
Filter.smul_filter_neBot_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β] {f : Filter β} {a : α}, (a • f).NeBot ↔ f.NeBot
-- Aesop.Options.Public
/-- (aesop) Only for use by Aesop developers. Uses static structuring instead of
dynamic structuring if no metavariables appear in the proof.
 -/
Aesop.aesop.dev.optimizedDynamicStructuring : Lean.Option Bool
-- Mathlib.MeasureTheory.Group.Arithmetic
MeasurableInv.measurable_inv : ∀ {G : Type u_2} {inst : Inv G} {inst_1 : MeasurableSpace G} [self : MeasurableInv G], Measurable Inv.inv
-- Mathlib.Combinatorics.Matroid.Circuit
Matroid.mem_closure_iff_exists_isCircuit : ∀ {α : Type u_1} {M : Matroid α} {X : Set α} {e : α},
  e ∉ X → (e ∈ M.closure X ↔ ∃ C ⊆ insert e X, M.IsCircuit C ∧ e ∈ C)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.contains_iff_mem : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} {a : α},
  m.contains a = true ↔ a ∈ m
-- Mathlib.MeasureTheory.Measure.NullMeasurable
MeasureTheory.measure_preimage_snd_singleton_eq_tsum : ∀ {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [MeasurableSingletonClass α] {mβ : MeasurableSpace β}
  [MeasurableSingletonClass β] [Countable α] (μ : MeasureTheory.Measure (α × β)) (y : β),
  μ (Prod.snd ⁻¹' {y}) = ∑' (x : α), μ {(x, y)}
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.imp_mono_r : ∀ {σs : List (Type u)} {P Q Q' : Std.Do.SPred σs}, (Q ⊢ₛ Q') → (P → Q) ⊢ₛ P → Q'
-- Mathlib.RingTheory.WittVector.Truncated
WittVector.truncateFun_sub : ∀ {p : ℕ} (n : ℕ) {R : Type u_1} [inst : CommRing R] [inst_1 : Fact (Nat.Prime p)] (x y : WittVector p R),
  WittVector.truncateFun n (x - y) = WittVector.truncateFun n x - WittVector.truncateFun n y
-- Mathlib.RingTheory.NonUnitalSubring.Basic
NonUnitalSubring.mem_sInf : ∀ {R : Type u} [inst : NonUnitalNonAssocRing R] {S : Set (NonUnitalSubring R)} {x : R}, x ∈ sInf S ↔ ∀ p ∈ S, x ∈ p
-- Mathlib.Data.Nat.MaxPowDiv
padicValNat_one_left : ∀ (n : ℕ), padicValNat 1 n = 0
-- Mathlib.CategoryTheory.Localization.LocalizerMorphism
CategoryTheory.LocalizerMorphism.instIsInducedArrowArrowArrow : ∀ {C₁ : Type u₁} {C₂ : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) [Φ.IsInduced],
  Φ.arrow.IsInduced
-- Mathlib.LinearAlgebra.Matrix.Notation
/-- Delaborator for the `!![]` notation.  -/
Matrix.delabMatrixNotation : Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.Algebra.Group.Finsupp
Finsupp.support_single_add : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddZeroClass M] {a : ι} {b : M} {f : ι →₀ M} (ha : a ∉ f.support),
  b ≠ 0 → ((fun₀ | a => b) + f).support = Finset.cons a f.support ha
-- Batteries.Control.ForInStep.Lemmas
ForInStep.bind_done : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} [inst : Monad m] (a : α) (f : α → m (ForInStep α)),
  (ForInStep.done a).bind f = pure (ForInStep.done a)
-- Lean.Elab.App
Lean.Elab.Term.ElabElim.State.mk : Lean.Expr →
  Lean.Expr →
    List Lean.Elab.Term.NamedArg →
      List Lean.Elab.Term.Arg → Array Lean.MVarId → ℕ → Option Lean.Expr → Lean.Elab.Term.ElabElim.State
-- Mathlib.Tactic.ClickSuggestions.SectionState
_private.Mathlib.Tactic.ClickSuggestions.SectionState.0.Mathlib.Tactic.ClickSuggestions.renderSection.renderErrors : Array ProofWidgets.Html → ProofWidgets.Html
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.ParameterInformationLabel.range.sizeOf_spec : ∀ (startUtf16Offset endUtf16Offset : ℕ),
  sizeOf (Lean.Lsp.ParameterInformationLabel.range startUtf16Offset endUtf16Offset) =
    1 + sizeOf startUtf16Offset + sizeOf endUtf16Offset
-- Std.Async.Select
/-- Performs fair and data-loss free non-blocking multiplexing on the `Selectable`s in `selectables`.

This function only tries the non-blocking `tryFn` for each `Selectable` without registering
waiters or blocking. It returns `some result` if any `Selectable` is immediately available,
or `none` if all would block.

The protocol for this is as follows:
1. The `selectables` are shuffled randomly for fairness.
2. Run `Selector.tryFn` for each element in `selectables`. If any succeed, the corresponding
   `Selectable.cont` is executed and its result is returned as `some result`.
3. If none succeed, `none` is returned immediately without blocking.
 -/
Std.Async.Selectable.tryOne : {α : Type} → Array (Std.Async.Selectable α) → Std.Async.Async (Option α)
-- Mathlib.FieldTheory.Differential.Liouville
/-- We say that a differential field extension `K / F` is Liouville if, whenever an element `a ∈ F` can
be written as `a = v + ∑ cᵢ * logDeriv uᵢ` for `v, cᵢ, uᵢ ∈ K` and `cᵢ` constant, it can also be
written in that way with `v, cᵢ, uᵢ ∈ F`.
 -/
IsLiouville : (F : Type u_1) →
  (K : Type u_2) → [inst : Field F] → [inst_1 : Field K] → [Differential F] → [Differential K] → [Algebra F K] → Prop
-- Mathlib.Dynamics.BirkhoffSum.NormedSpace
dist_birkhoffAverage_apply_birkhoffAverage : ∀ {α : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] (𝕜 : Type u_3) [inst_1 : RCLike 𝕜]
  [inst_2 : NormedSpace 𝕜 E] (f : α → α) (g : α → E) (n : ℕ) (x : α),
  dist (birkhoffAverage 𝕜 f g n (f x)) (birkhoffAverage 𝕜 f g n x) = dist (g (f^[n] x)) (g x) / ↑n
-- Mathlib.Algebra.Colimit.Module
Module.DirectLimit.addCommGroup : {R : Type u_1} →
  [inst : Semiring R] →
    {ι : Type u_2} →
      [inst_1 : Preorder ι] →
        [inst_2 : DecidableEq ι] →
          (G : ι → Type u_4) →
            [inst_3 : (i : ι) → AddCommGroup (G i)] →
              [inst_4 : (i : ι) → Module R (G i)] →
                (f : (i j : ι) → i ≤ j → G i →ₗ[R] G j) → AddCommGroup (Module.DirectLimit G f)