mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.Basic
Lean.Meta.AbstractMVarsResult.expr : Lean.Meta.AbstractMVarsResult → Lean.Expr
-- Mathlib.Order.RelIso.Basic
RelHom.instFunLike : {α : Type u_1} → {β : Type u_2} → {r : α → α → Prop} → {s : β → β → Prop} → FunLike (r →r s) α β
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.minKey!_modify : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] [inst_2 : Inhabited α] {k : α} {f : β k → β k}, (t.modify k f).minKey! = t.minKey!
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
CategoryTheory.ChosenPullbacksAlong.pullbackMap_snd : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Y Z X : C} {f : Y ⟶ X} {g : Z ⟶ X}
  [inst_1 : CategoryTheory.ChosenPullbacksAlong g] {Y' Z' X' : C} {f' : Y' ⟶ X'} {g' : Z' ⟶ X'}
  [inst_2 : CategoryTheory.ChosenPullbacksAlong g'] {γ₁ : Y' ⟶ Y} {γ₂ : Z' ⟶ Z} {γ₃ : X' ⟶ X}
  (comm₁ :
    autoParam (CategoryTheory.CategoryStruct.comp f' γ₃ = CategoryTheory.CategoryStruct.comp γ₁ f)
      CategoryTheory.ChosenPullbacksAlong.pullbackMap_snd._auto_1)
  (comm₂ :
    autoParam (CategoryTheory.CategoryStruct.comp g' γ₃ = CategoryTheory.CategoryStruct.comp γ₂ g)
      CategoryTheory.ChosenPullbacksAlong.pullbackMap_snd._auto_3),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenPullbacksAlong.pullbackMap f g f' g' γ₁ γ₂ γ₃ comm₁ comm₂)
      (CategoryTheory.ChosenPullbacksAlong.snd f g) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenPullbacksAlong.snd f' g') γ₂
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Triplet.mk.injEq : ∀ {n : ℤ} (p q : ℤ) (hpq : p + n = q) (p_1 q_1 : ℤ) (hpq_1 : p_1 + n = q_1),
  ({ p := p, q := q, hpq := hpq } = { p := p_1, q := q_1, hpq := hpq_1 }) = (p = p_1 ∧ q = q_1)
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.nonUnitalSemiring.eq_1 : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddSemigroup M],
  AddMonoidAlgebra.nonUnitalSemiring =
    { toNonUnitalNonAssocSemiring := AddMonoidAlgebra.nonUnitalNonAssocSemiring, mul_assoc := ⋯ }
-- Mathlib.CategoryTheory.Limits.IndYoneda
/-- Hom is cocontinuous: homomorphisms from a colimit is the limit over yoneda of the diagram.  -/
CategoryTheory.Limits.colimitHomIsoLimitYoneda : {C : Type u₁} →
  [inst : CategoryTheory.Category.{u₂, u₁} C] →
    {I : Type v₁} →
      [inst_1 : CategoryTheory.Category.{v₂, v₁} I] →
        (F : CategoryTheory.Functor I C) →
          [inst_2 : CategoryTheory.Limits.HasColimit F] →
            [CategoryTheory.Limits.HasLimitsOfShape Iᵒᵖ (Type u₂)] →
              (A : C) →
                (CategoryTheory.Limits.colimit F ⟶ A) ≅
                  CategoryTheory.Limits.limit (F.op.comp (CategoryTheory.yoneda.obj A))
-- Mathlib.AlgebraicGeometry.Geometrically.Basic
AlgebraicGeometry.geometrically_iff_of_isClosedUnderIsomorphisms : ∀ {P : CategoryTheory.ObjectProperty AlgebraicGeometry.Scheme} {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y}
  [P.IsClosedUnderIsomorphisms],
  AlgebraicGeometry.geometrically P f ↔
    ∀ (K : Type u) [inst : Field K] (y : AlgebraicGeometry.Spec (CommRingCat.of K) ⟶ Y),
      P (CategoryTheory.Limits.pullback f y)
-- Mathlib.SetTheory.Ordinal.Basic
/-- `o₁ + o₂` is the order on the disjoint union of `o₁` and `o₂` obtained by declaring that
every element of `o₁` is smaller than every element of `o₂`.  -/
Ordinal.add : Add Ordinal.{u}
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr
Std.Tactic.BVDecide.BVExpr.bitblast_denote_mem_prefix : ∀ {w : ℕ} {inv : Bool} (aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit)
  (input : Std.Tactic.BVDecide.BVExpr.WithCache (Std.Tactic.BVDecide.BVExpr w) aig)
  (assign : Std.Tactic.BVDecide.BVExpr.Assignment) (start : ℕ) (hstart : start < aig.decls.size),
  ⟦assign.toAIGAssignment,
      { aig := (↑(Std.Tactic.BVDecide.BVExpr.bitblast aig input).result).aig,
        ref := { gate := start, invert := inv, hgate := ⋯ } }⟧ =
    ⟦assign.toAIGAssignment, { aig := aig, ref := { gate := start, invert := inv, hgate := hstart } }⟧
-- Mathlib.Order.Filter.NAry
Filter.map₂_sup_left : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {m : α → β → γ} {f₁ f₂ : Filter α} {g : Filter β},
  Filter.map₂ m (f₁ ⊔ f₂) g = Filter.map₂ m f₁ g ⊔ Filter.map₂ m f₂ g
-- Mathlib.Order.BooleanAlgebra.Set
Set.sdiff_inter_self : ∀ {α : Type u_1} {a b : Set α}, b \ a ∩ a = ∅
-- Mathlib.Order.RelIso.Basic
RelIso.toEquiv_symm_toMap : ∀ {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (f : α ≃ β), ↑(RelIso.toMap r f).symm = f.symm
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.getEntryGTD_eq : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t₁.WF →
    t₂.WF →
      t₁.Equiv t₂ →
        ∀ {k : α} {fallback : (a : α) × β a},
          Std.DTreeMap.Internal.Impl.getEntryGTD k t₁ fallback = Std.DTreeMap.Internal.Impl.getEntryGTD k t₂ fallback
-- Mathlib.Topology.MetricSpace.Dilation
/-- A dilation scales the diameter of the range by `ratio f`.  -/
Dilation.ediam_range : ∀ {α : Type u_1} {β : Type u_2} {F : Type u_4} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β]
  [inst_2 : FunLike F α β] [inst_3 : DilationClass F α β] (f : F),
  Metric.ediam (Set.range ⇑f) = ↑(Dilation.ratio f) * Metric.ediam Set.univ
-- Std.Internal.Do.WP.Basic
/-- Soundness for `Id`: if `wp prog P` holds, then `P` holds of the result.  -/
Std.Internal.Do.Id.of_wp_run_eq : ∀ {α : Type u} {x : α} {prog : Id α}, prog.run = x → ∀ (P : α → Prop), Std.Internal.Do.wp prog P epost⟨⟩ → P x
-- Mathlib.Analysis.InnerProductSpace.Symmetric
LinearMap.IsSymmetric.coe_re_inner_apply_self : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {T : E →ₗ[𝕜] E}, T.IsSymmetric → ∀ (x : E), ↑(RCLike.re (inner 𝕜 (T x) x)) = inner 𝕜 (T x) x
-- Init.Data.Option.Monadic
Option.tryCatch_eq_or : ∀ {α : Type u_1} (o : Option α) (alternative : Unit → Option α), tryCatch o alternative = o.or (alternative ())
-- Mathlib.Topology.ContinuousMap.Algebra
/-- Coercion to a function as a `RingHom`.  -/
ContinuousMap.coeFnRingHom : {α : Type u_1} →
  {β : Type u_2} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] → [inst_2 : Semiring β] → [inst_3 : IsTopologicalSemiring β] → C(α, β) →+* α → β
-- Std.Do.PostCond
/-- Extracts the list of state types under `PostShape.arg` constructors, discarding exception types.

The state types determine the shape of assertions in the monad.
 -/
Std.Do.PostShape.args : Std.Do.PostShape → List (Type u)
-- Mathlib.Topology.Algebra.Module.ModuleTopology
/-- Every `R`-linear map between two topological `R`-modules, where the source has the module
topology, is continuous.  -/
IsModuleTopology.continuous_of_linearMap : ∀ {R : Type u_1} [τR : TopologicalSpace R] [inst : Semiring R] {A : Type u_3} [inst_1 : AddCommMonoid A]
  [inst_2 : Module R A] [aA : TopologicalSpace A] [IsModuleTopology R A] {B : Type u_4} [inst_4 : AddCommMonoid B]
  [inst_5 : Module R B] [aB : TopologicalSpace B] [ContinuousAdd B] [ContinuousSMul R B] (φ : A →ₗ[R] B), Continuous ⇑φ
-- Mathlib.MeasureTheory.Integral.Lebesgue.Map
MeasureTheory.lintegral_comp : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {f : β → ENNReal} {g : α → β},
  Measurable f → Measurable g → MeasureTheory.lintegral μ (f ∘ g) = ∫⁻ (a : β), f a ∂MeasureTheory.Measure.map g μ
-- Lean.Server.References
/-- Reference information from a loaded ILean file.  -/
Lean.Server.LoadedILean : Type
-- Mathlib.Analysis.Convex.Jensen
/-- Concave **Jensen's inequality** where an element plays a distinguished role.  -/
ConcaveOn.map_add_sum_le : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} {ι : Type u_5} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜]
  [IsStrictOrderedRing 𝕜] [inst_3 : AddCommGroup E] [inst_4 : AddCommGroup β] [inst_5 : PartialOrder β]
  [IsOrderedAddMonoid β] [inst_7 : Module 𝕜 E] [inst_8 : Module 𝕜 β] [IsStrictOrderedModule 𝕜 β] {s : Set E} {f : E → β}
  {t : Finset ι} {w : ι → 𝕜} {p : ι → E} {v : 𝕜} {q : E},
  ConcaveOn 𝕜 s f →
    (∀ i ∈ t, 0 ≤ w i) →
      v + ∑ i ∈ t, w i = 1 →
        (∀ i ∈ t, p i ∈ s) → 0 ≤ v → q ∈ s → v • f q + ∑ i ∈ t, w i • f (p i) ≤ f (v • q + ∑ i ∈ t, w i • p i)
-- Std.Time.Internal.UnitVal
Std.Time.Internal.UnitVal.ext : ∀ {α : ℚ} {x y : Std.Time.Internal.UnitVal α}, x.val = y.val → x = y
-- Mathlib.Algebra.FreeAlgebra
/-- If `α` is a type, and `R` is a commutative semiring, then `FreeAlgebra R α` is the
free (unital, associative) `R`-algebra generated by `α`.
This is an `R`-algebra equipped with a function `FreeAlgebra.ι R : α → FreeAlgebra R α` which has
the following universal property: if `A` is any `R`-algebra, and `f : α → A` is any function,
then this function is the composite of `FreeAlgebra.ι R` and a unique `R`-algebra homomorphism
`FreeAlgebra.lift R f : FreeAlgebra R α →ₐ[R] A`.

A typical element of `FreeAlgebra R α` is an `R`-linear
combination of formal products of elements of `α`.
For example if `x` and `y` are terms of type `α` and `a`, `b` are terms of type `R` then
`(3 * a * a) • (x * y * x) + (2 * b + 1) • (y * x) + (a * b * b + 3)` is a
"typical" element of `FreeAlgebra R α`. In particular if `α` is empty
then `FreeAlgebra R α` is isomorphic to `R`, and if `α` has one term `t`
then `FreeAlgebra R α` is isomorphic to the polynomial ring `R[t]`.
If `α` has two or more terms then `FreeAlgebra R α` is not commutative.
One can think of `FreeAlgebra R α` as the free non-commutative polynomial ring
with coefficients in `R` and variables indexed by `α`.
 -/
FreeAlgebra : (R : Type u_1) → Type u_2 → [CommSemiring R] → Type (max u_1 u_2)
-- Lean.Parser.Basic
Lean.Parser.ParserCategories : Type
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.minKey?_modify_eq_minKey? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp], t.WF → ∀ {k : α} {f : β → β}, (t.modify k f).minKey? = t.minKey?
-- Init.Data.Char.Ordinal
Char.lt_iff_ordinal_lt : ∀ {c d : Char}, c < d ↔ c.ordinal < d.ordinal
-- Mathlib.Topology.Algebra.Module.ClosedSubmodule
ClosedSubmodule.ext : ∀ {R : Type u_2} {M : Type u_3} {inst : Semiring R} {inst_1 : AddCommMonoid M} {inst_2 : TopologicalSpace M}
  {inst_3 : Module R M} {x y : ClosedSubmodule R M}, (↑x).carrier = (↑y).carrier → x = y
-- Mathlib.GroupTheory.FiniteIndexNormalSubgroup
FiniteIndexNormalSubgroup.toSubgroup_injective : ∀ {G : Type u_1} [inst : Group G], Function.Injective fun H => H.toSubgroup
-- Mathlib.CategoryTheory.Triangulated.Rotate
CategoryTheory.Pretriangulated.rotCompInvRot_inv_app_hom₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  (X : CategoryTheory.Pretriangulated.Triangle C),
  (CategoryTheory.Pretriangulated.rotCompInvRot.inv.app X).hom₁ =
    (CategoryTheory.shiftFunctorCompIsoId C 1 (-1) ⋯).hom.app X.obj₁
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Equivalence.functor_map_μ_inverse_comp_counitIso_hom_app_tensor : ∀ {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] (e : C ≌ D)
  [inst_4 : e.functor.Monoidal] [inst_5 : e.inverse.Monoidal] [e.IsMonoidal] (X Y : D),
  CategoryTheory.CategoryStruct.comp (e.functor.map (CategoryTheory.Functor.LaxMonoidal.μ e.inverse X Y))
      (e.counitIso.hom.app (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Functor.OplaxMonoidal.δ e.functor (e.inverse.obj X) (e.inverse.obj Y))
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (e.counitIso.hom.app X) (e.counitIso.hom.app Y))
-- Mathlib.Data.Set.Pairwise.Basic
/-- **Alias** of `Std.Symm.pairwise_on`. -/
Symmetric.pairwise_on : ∀ {α : Type u_1} {ι : Type u_4} {r : α → α → Prop} [inst : LinearOrder ι] [Std.Symm r] (f : ι → α),
  Pairwise (Function.onFun r f) ↔ ∀ ⦃m n : ι⦄, m < n → r (f m) (f n)
-- Init.Grind.Ordered.Ring
Lean.Grind.OrderedRing.mul_neg_of_pos_of_neg : ∀ {R : Type u} [inst : Lean.Grind.Ring R] [inst_1 : LE R] [inst_2 : LT R] [inst_3 : Std.IsPartialOrder R]
  [Lean.Grind.OrderedRing R] [Std.LawfulOrderLT R] {a b : R}, 0 < a → b < 0 → a * b < 0
-- Mathlib.Geometry.Manifold.IsManifold.Basic
/-- Given a model with corners `(E, H)`, we define the groupoid of invertible `C^n` transformations
of `H` as the invertible maps that are `C^n` when read in `E` through `I`.  -/
contDiffGroupoid : WithTop ℕ∞ →
  {𝕜 : Type u_1} →
    [inst : NontriviallyNormedField 𝕜] →
      {E : Type u_2} →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : NormedSpace 𝕜 E] →
            {H : Type u_3} → [inst_3 : TopologicalSpace H] → ModelWithCorners 𝕜 E H → StructureGroupoid H
-- Mathlib.Order.Interval.Set.SuccPred
Set.Ico_succ_succ_eq_Ioc : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : SuccOrder α] [NoMaxOrder α] (a b : α),
  Set.Ico (Order.succ a) (Order.succ b) = Set.Ioc a b
-- Mathlib.Topology.MetricSpace.Cauchy
/-- A pseudo-metric space is complete iff every Cauchy sequence converges.  -/
Metric.complete_of_cauchySeq_tendsto : ∀ {α : Type u} [inst : PseudoMetricSpace α],
  (∀ (u : ℕ → α), CauchySeq u → ∃ a, Filter.Tendsto u Filter.atTop (nhds a)) → CompleteSpace α
-- Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
/-- For integrally closed rings, the minimal polynomial divides any polynomial that has the
integral element as root. See also `minpoly.dvd` which relaxes the assumptions on `S`
in exchange for stronger assumptions on `R`.  -/
minpoly.isIntegrallyClosed_dvd : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [IsDomain R] [inst_3 : Algebra R S]
  [IsIntegrallyClosed R] [IsDomain S] [Module.IsTorsionFree R S] {s : S},
  IsIntegral R s → ∀ {p : Polynomial R}, (Polynomial.aeval s) p = 0 → minpoly R s ∣ p
-- Mathlib.RingTheory.LaurentSeries
/-- Conversely, all elements in the unit ball inside the completion of `K⟮X⟯` come from a power
series through the isomorphism `LaurentSeriesRingEquiv`.  -/
LaurentSeries.exists_powerSeries_of_memIntegers : ∀ (K : Type u_2) [inst : Field K] {x : LaurentSeries.RatFuncAdicCompl K},
  x ∈ IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers (RatFunc K) (Polynomial.idealX K) →
    ∃ F, (LaurentSeries.LaurentSeriesRingEquiv K) ((HahnSeries.ofPowerSeries ℤ K) F) = x
-- Std.Tactic.BVDecide.Normalize.Equal
Std.Tactic.BVDecide.Frontend.Normalize.Bool.not_bif_eq_bif' : ∀ (d a b c : Bool), ((!bif d then a else c) == bif d then b else c) = (d && (!a) == b)
-- Mathlib.GroupTheory.GroupAction.Defs
MulAction.orbitRel.quotient_eq_of_quotient_subgroup_eq' : ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] {H : Subgroup G} {a b : α},
  Quotient.mk'' a = Quotient.mk'' b → Quotient.mk'' a = Quotient.mk'' b
-- Mathlib.Algebra.Order.Archimedean.Defs
/-- For any two elements `x`, `y` such that `1 < y`, there exists a natural number `n`
such that `x ≤ y ^ n`.  -/
MulArchimedean.arch : ∀ {R : Type u_2} {inst : CommMonoid R} {inst_1 : PartialOrder R} [self : MulArchimedean R] (x : R) {y : R},
  1 < y → ∃ n, x ≤ y ^ n
-- Mathlib.Order.Bounds.Image
BddBelow.range_comp_left : ∀ {α : Type u} {β : Type v} {γ : Type u_1} [inst : Preorder β] [inst_1 : Preorder γ] {f : α → β} {g : β → γ},
  BddBelow (Set.range f) → Monotone g → BddBelow (Set.range fun x => g (f x))
-- Init.Data.String.Lemmas.Basic
String.Pos.get_ofToSlice : ∀ {s : String} {p : s.toSlice.Pos} {h : String.Pos.ofToSlice p ≠ s.endPos}, (String.Pos.ofToSlice p).get h = p.get ⋯
-- Mathlib.Data.QPF.Multivariate.Constructions.Prj
/-- Polynomial representation of the projection functor  -/
MvQPF.Prj.P : {n : ℕ} → Fin2 n → MvPFunctor.{u} n
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.PartialMatch.mk.sizeOf_spec : ∀ (todo : Array Lean.Expr) (score : ℕ) (c : Lean.Meta.LazyDiscrTree.TrieIndex),
  sizeOf { todo := todo, score := score, c := c } = 1 + sizeOf todo + sizeOf score + sizeOf c
-- Mathlib.AlgebraicGeometry.Morphisms.Basic
AlgebraicGeometry.IsZariskiLocalAtSource.comp : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsZariskiLocalAtSource P]
  {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} {UX : AlgebraicGeometry.Scheme},
  P f → ∀ (i : UX ⟶ X) [AlgebraicGeometry.IsOpenImmersion i], P (CategoryTheory.CategoryStruct.comp i f)
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
BoundedContinuousFunction.instNormedAddCommGroup : {α : Type u_1} →
  {β : Type u_2} →
    [inst : TopologicalSpace α] → [inst_1 : NormedAddCommGroup β] → NormedAddCommGroup (BoundedContinuousFunction α β)
-- Lean.Meta.Tactic.Simp.SimpTheorems
Lean.Meta.instInhabitedSimpTheorems.default : Lean.Meta.SimpTheorems
-- Mathlib.RingTheory.LocalRing.ResidueField.Basic
IsLocalRing.instFiniteResidueField : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsLocalRing R] {R₀ : Type u_4} [inst_2 : CommRing R₀]
  [inst_3 : Algebra R₀ R] [Module.Finite R₀ R], Module.Finite R₀ (IsLocalRing.ResidueField R)
-- Mathlib.CategoryTheory.Pi.Basic
CategoryTheory.Pi.comp_apply : ∀ {I : Type w₀} (C : I → Type u₁) [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {X Y Z : (i : I) → C i}
  (f : X ⟶ Y) (g : Y ⟶ Z) (i : I),
  CategoryTheory.CategoryStruct.comp f g i = CategoryTheory.CategoryStruct.comp (f i) (g i)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Complex.exp_add_pi_mul_I : ∀ (z : ℂ), Complex.exp (z + ↑Real.pi * Complex.I) = -Complex.exp z
-- Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
AddSubgroup.vadd_opposite_add : ∀ {G : Type u_2} [inst : AddGroup G] {H : AddSubgroup G} (x g : G) (h : ↥H.op), h +ᵥ g + x = g + (h +ᵥ x)
-- Mathlib.Data.PNat.Prime
PNat.gcd_one : ∀ {n : ℕ+}, n.gcd 1 = 1
-- Mathlib.CategoryTheory.Subobject.Basic
CategoryTheory.Subobject.pullback_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  (f : X ⟶ Y) (g : Y ⟶ Z) (x : CategoryTheory.Subobject Z),
  (CategoryTheory.Subobject.pullback (CategoryTheory.CategoryStruct.comp f g)).obj x =
    (CategoryTheory.Subobject.pullback f).obj ((CategoryTheory.Subobject.pullback g).obj x)
-- Mathlib.Algebra.Module.Submodule.Map
/-- The infimum of a family of invariant submodule of an endomorphism is also an invariant
submodule.  -/
LinearMap.iInf_invariant : ∀ {R : Type u_1} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {σ : R →+* R}
  {ι : Sort u_9} (f : M →ₛₗ[σ] M) {p : ι → Submodule R M},
  (∀ (i : ι), ∀ v ∈ p i, f v ∈ p i) → ∀ v ∈ iInf p, f v ∈ iInf p
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
/-- The top `IntermediateField` is isomorphic to the field.

This is the intermediate field version of `Subalgebra.topEquiv`.  -/
IntermediateField.topEquiv : {F : Type u_1} → [inst : Field F] → {E : Type u_2} → [inst_1 : Field E] → [inst_2 : Algebra F E] → ↥⊤ ≃ₐ[F] E
-- Mathlib.Analysis.InnerProductSpace.Dual
/-- The kernel of the map `x ↦ ⟪·, x⟫` includes the null space.  -/
InnerProductSpace.nullSubmodule_le_ker_toDualMap_left : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E],
  nullSubmodule 𝕜 E ≤ (InnerProductSpace.toDualMap 𝕜 E).ker
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.GrpObj.comp_zpow : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {G X Y : C} [inst_2 : CategoryTheory.GrpObj G] (f : X ⟶ Y) (g : Y ⟶ G) (n : ℤ),
  CategoryTheory.CategoryStruct.comp f (g ^ n) = CategoryTheory.CategoryStruct.comp f g ^ n
-- Mathlib.Topology.Bornology.Constructions
Bornology.IsBounded.image_fst : ∀ {α : Type u_1} {β : Type u_2} [inst : Bornology α] [inst_1 : Bornology β] {s : Set (α × β)},
  Bornology.IsBounded s → Bornology.IsBounded (Prod.fst '' s)
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.ext : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} {M N : Matrix m n α}, (∀ (i : m) (j : n), M i j = N i j) → M = N
-- Mathlib.Algebra.Star.SelfAdjoint
selfAdjoint.val_pow : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : StarRing R] (x : ↥(selfAdjoint R)) (n : ℕ), ↑(x ^ n) = ↑x ^ n
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
/-- Any intersection of translates of two sets `s` and `t` can be covered by a single translate of
`(s⁻¹ * s) ∩ (t⁻¹ * t)`.

This is useful to show that the intersection of approximate subgroups is an approximate subgroup.  -/
Set.exists_smul_inter_smul_subset_smul_inv_mul_inter_inv_mul : ∀ {α : Type u_2} [inst : Group α] (s t : Set α) (a b : α), ∃ z, a • s ∩ b • t ⊆ z • (s⁻¹ * s ∩ (t⁻¹ * t))
-- Init.Grind.Ring.Basic
Lean.Grind.IsCharP.natCast_eq_iff_of_lt : ∀ {α : Type u_1} (p : ℕ) [inst : Lean.Grind.Semiring α] [Lean.Grind.IsCharP α p] {x y : ℕ},
  x < p → y < p → (↑x = ↑y ↔ x = y)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
logDeriv_sineTerm_eq_cotTerm : ∀ {x : ℂ}, x ∈ Complex.integerComplement → ∀ (i : ℕ), logDeriv (fun z => 1 + sineTerm z i) x = cotTerm x i
-- Mathlib.Combinatorics.Young.YoungDiagram
YoungDiagram.mk.congr_simp : ∀ (cells cells_1 : Finset (ℕ × ℕ)) (e_cells : cells = cells_1) (isLowerSet : IsLowerSet ↑cells),
  { cells := cells, isLowerSet := isLowerSet } = { cells := cells_1, isLowerSet := ⋯ }
-- Mathlib.Order.CompleteLattice.Basic
iInf_subtype'' : ∀ {α : Type u_1} [inst : CompleteLattice α] {ι : Type u_8} (s : Set ι) (f : ι → α), ⨅ i, f ↑i = ⨅ t ∈ s, f t
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.mem_of_getKey?_eq_some : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {a a' : α}, t.getKey? a = some a' → a' ∈ t
-- Init.Data.List.Sort.Basic
_private.Init.Data.List.Sort.Basic.0.List.mergeSort.eq_def : ∀ {α : Type u_1} (x : List α) (x_1 : α → α → Bool),
  x.mergeSort x_1 =
    match x, x_1 with
    | [], x => []
    | [a], x => [a]
    | a :: b :: xs, le =>
      have lr := List.MergeSort.Internal.splitInTwo ⟨a :: b :: xs, ⋯⟩;
      have this := ⋯;
      have this := ⋯;
      ((↑lr.1).mergeSort le).merge ((↑lr.2).mergeSort le) le
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.pullbackSpecIso_inv_fst' : ∀ (R S T : Type u) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
  [inst_4 : Algebra R T],
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.pullbackSpecIso R S T).inv
      (CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R S)))
        (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R T)))) =
    AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap S (TensorProduct R S T)))
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.Red.append_append_left_iff : ∀ {α : Type u} {L₁ L₂ : List (α × Bool)} (L : List (α × Bool)),
  FreeAddGroup.Red (L ++ L₁) (L ++ L₂) ↔ FreeAddGroup.Red L₁ L₂
-- Mathlib.Analysis.Normed.Group.Basic
preimage_mul_closedBall : ∀ {E : Type u_5} [inst : SeminormedCommGroup E] (a b : E) (r : ℝ),
  (fun x => b * x) ⁻¹' Metric.closedBall a r = Metric.closedBall (a / b) r
-- Mathlib.Topology.IsLocalHomeomorph
IsLocalHomeomorph.isLocalHomeomorphOn : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y} {s : Set X},
  IsLocalHomeomorph f → IsLocalHomeomorphOn f s
-- Mathlib.RingTheory.LocalRing.Quotient
_private.Mathlib.RingTheory.LocalRing.Quotient.0.IsLocalRing.termP : Lean.ParserDescr
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Equiv.getD_eq : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [inst : LawfulBEq α] {k : α}
  {fallback : β k}, m₁.Equiv m₂ → m₁.getD k fallback = m₂.getD k fallback
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddSubsemigroup.mem_map_iff_mem : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] {f : M →ₙ+ N},
  Function.Injective ⇑f → ∀ {S : AddSubsemigroup M} {x : M}, f x ∈ AddSubsemigroup.map f S ↔ x ∈ S
-- Init.Prelude
/-- The typeclass behind the notation `~~~a : α` where `a : α`.  -/
Complement : Type u → Type u