mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Comma.Basic
/-- `Comma.preRight` is a particular case of `Comma.map`,
but with better definitional properties.  -/
CategoryTheory.Comma.preRightIso : {B : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} B] →
    {A : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} A] →
        {T : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} T] →
            {C : Type u₄} →
              [inst_3 : CategoryTheory.Category.{v₄, u₄} C] →
                (L : CategoryTheory.Functor A T) →
                  (F : CategoryTheory.Functor C B) →
                    (R : CategoryTheory.Functor B T) →
                      CategoryTheory.Comma.preRight L F R ≅
                        CategoryTheory.Comma.map (CategoryTheory.CategoryStruct.comp L.leftUnitor.hom L.rightUnitor.inv)
                          (F.comp R).rightUnitor.hom
-- Mathlib.Algebra.Group.Units.Hom
AddMonoidHom.toHomAddUnits.eq_1 : ∀ {G : Type u_1} {M : Type u_2} [inst : AddGroup G] [inst_1 : AddMonoid M] (f : G →+ M),
  f.toHomAddUnits = AddUnits.liftRight f (fun g => { val := f g, neg := f (-g), val_neg := ⋯, neg_val := ⋯ }) ⋯
-- Mathlib.Order.Filter.Bases.Basic
Filter.inf_neBot_iff : ∀ {α : Type u_1} {l l' : Filter α}, (l ⊓ l').NeBot ↔ ∀ ⦃s : Set α⦄, s ∈ l → ∀ ⦃s' : Set α⦄, s' ∈ l' → (s ∩ s').Nonempty
-- Mathlib.NumberTheory.NumberField.House
/-- `a' K a` returns the integer coefficients of the basis vector in the
expansion of the product of an algebraic integer and a basis vectors.  -/
_private.Mathlib.NumberTheory.NumberField.House.0.NumberField.house.a' : (K : Type u_1) →
  [inst : Field K] →
    [NumberField K] →
      {α : Type u_2} → {β : Type u_3} → Matrix α β (NumberField.RingOfIntegers K) → α → β → (K →+* ℂ) → (K →+* ℂ) → ℤ
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toList_rco_eq_singleton_iff : ∀ {k m n : ℤ}, (m...n).toList = [k] ↔ n = m + 1 ∧ m = k
-- Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
AlgebraicGeometry.affineAnd_apply : ∀ (Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop) {X Y : AlgebraicGeometry.Scheme}
  (f : X ⟶ Y) [inst : AlgebraicGeometry.IsAffine Y],
  AlgebraicGeometry.affineAnd (fun {R S} [CommRing R] [CommRing S] => Q) f ↔
    AlgebraicGeometry.IsAffine X ∧ Q (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appTop f))
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.Parser.phaseSafe : Lean.ParserDescr
-- Mathlib.AlgebraicTopology.RelativeCellComplex.Basic
/-- If `f` is a relative cell complex with respect to a constant
family of morphisms `g`, then `f` is a transfinite composition
of pushouts of coproducts of morphisms in the family `g`.  -/
HomotopicalAlgebra.RelativeCellComplex.transfiniteCompositionOfShape : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type w'} →
      [inst_1 : LinearOrder J] →
        [inst_2 : OrderBot J] →
          [inst_3 : SuccOrder J] →
            [inst_4 : WellFoundedLT J] →
              {X Y : C} →
                {f : X ⟶ Y} →
                  {α : Type u_1} →
                    {A B : α → C} →
                      (g : (i : α) → A i ⟶ B i) →
                        HomotopicalAlgebra.RelativeCellComplex (fun x => g) f →
                          (CategoryTheory.MorphismProperty.coproducts.{w, v, u}
                                  (CategoryTheory.MorphismProperty.ofHoms g)).pushouts.TransfiniteCompositionOfShape
                            J f
-- Mathlib.Data.Set.Semiring
SetSemiring.instNonAssocSemiringOfMulOneClass : {α : Type u_1} → [MulOneClass α] → NonAssocSemiring (SetSemiring α)
-- Lean.Elab.Util
Lean.Elab.MonadMacroAdapter.setNextMacroScope : {m : Type → Type} → [self : Lean.Elab.MonadMacroAdapter m] → Lean.MacroScope → m Unit
-- Mathlib.GroupTheory.Submonoid.Center
MulOpposite.unop_mem_center_iff : ∀ {M : Type u_2} [inst : Mul M] {x : Mᵐᵒᵖ}, MulOpposite.unop x ∈ Set.center M ↔ x ∈ Set.center Mᵐᵒᵖ
-- Mathlib.Algebra.Category.ModuleCat.Differentials.Basic
CommRingCat.KaehlerDifferential.map_d : ∀ {A B A' B' : CommRingCat} {f : A ⟶ B} {f' : A' ⟶ B'} {g : A ⟶ A'} {g' : B ⟶ B'}
  (fac : CategoryTheory.CategoryStruct.comp g f' = CategoryTheory.CategoryStruct.comp f g') (b : ↑B),
  (CategoryTheory.ConcreteCategory.hom (CommRingCat.KaehlerDifferential.map fac))
      (CommRingCat.KaehlerDifferential.d b) =
    CommRingCat.KaehlerDifferential.d ((CategoryTheory.ConcreteCategory.hom g') b)
-- Mathlib.Probability.Independence.Kernel.IndepFun
ProbabilityTheory.Kernel.iIndepFun.indepFun_finsetSum_of_notMem₀ : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω}
  {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {β : Type u_8} {m : MeasurableSpace β}
  [inst : AddCommMonoid β] [MeasurableAdd₂ β] {f : ι → Ω → β},
  ProbabilityTheory.Kernel.iIndepFun f κ μ →
    (∀ (i : ι), AEMeasurable (f i) (μ.bind ⇑κ)) →
      ∀ {s : Finset ι} {i : ι}, i ∉ s → ProbabilityTheory.Kernel.IndepFun (∑ j ∈ s, f j) (f i) κ μ
-- Init.Data.List.Basic
_private.Init.Data.List.Basic.0.List.replicateTR.loop.match_1.splitter : {α : Type u_1} →
  (motive : ℕ → List α → Sort u_2) →
    (x : ℕ) →
      (x_1 : List α) → ((as : List α) → motive 0 as) → ((n : ℕ) → (as : List α) → motive n.succ as) → motive x x_1
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.finSuccEquiv_X_succ : ∀ {R : Type u} [inst : CommSemiring R] {n : ℕ} {j : Fin n},
  (MvPolynomial.finSuccEquiv R n) (MvPolynomial.X j.succ) = Polynomial.C (MvPolynomial.X j)
-- Mathlib.Algebra.Group.Pi.Lemmas
Pi.update_eq_div_mul_mulSingle : ∀ {I : Type u} {f : I → Type v} (i : I) [inst : DecidableEq I] [inst_1 : (i : I) → Group (f i)] (g : (i : I) → f i)
  (x : f i), Function.update g i x = g / Pi.mulSingle i (g i) * Pi.mulSingle i x
-- Mathlib.Analysis.Normed.Group.Seminorm
AddGroupNorm.funLike.eq_1 : ∀ {E : Type u_3} [inst : AddGroup E], AddGroupNorm.funLike = { coe := fun f => f.toFun, coe_injective := ⋯ }
-- Mathlib.FieldTheory.LinearDisjoint
/-- If `A` and `B` are field extensions of `F`, one of them is algebraic, such that there exists a
field `E` that `A` and `B` embeds into with linearly disjoint images, then `A ⊗[F] B`
is a field.  -/
IntermediateField.LinearDisjoint.isField_of_isAlgebraic' : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {A : Type u_1} {B : Type u_2}
  [inst_3 : Field A] [inst_4 : Algebra F A] [inst_5 : Field B] [inst_6 : Algebra F B] {fa : A →ₐ[F] E} {fb : B →ₐ[F] E},
  fa.fieldRange.LinearDisjoint ↥fb.fieldRange →
    Algebra.IsAlgebraic F A ∨ Algebra.IsAlgebraic F B → IsField (TensorProduct F A B)
-- Mathlib.Algebra.Category.ModuleCat.Basic
CategoryTheory.Iso.toLinearMap_toLinearEquiv : ∀ {R : Type u} [inst : Ring R] {X Y : ModuleCat R} (i : X ≅ Y), ↑i.toLinearEquiv = ModuleCat.Hom.hom i.hom
-- Mathlib.GroupTheory.GroupAction.ConjAct
/-- The stabilizer of `Mˣ` acting on itself by conjugation at `x : Mˣ` is exactly the
units of the centralizer of `x : M`.  -/
unitsCentralizerEquiv : (M : Type u_2) →
  [inst : Monoid M] → (x : Mˣ) → (↥(Submonoid.centralizer {↑x}))ˣ ≃* ↥(MulAction.stabilizer (ConjAct Mˣ) x)
-- Mathlib.Data.Nat.Totient
Nat.totient_one : Nat.totient 1 = 1
-- Mathlib.Topology.ContinuousMap.Compact
ContinuousMap.instNormedAddCommGroup : {α : Type u_1} →
  [inst : TopologicalSpace α] →
    [CompactSpace α] → {E : Type u_4} → [inst_2 : NormedAddCommGroup E] → NormedAddCommGroup C(α, E)
-- Mathlib.MeasureTheory.Integral.CircleIntegral
/-- If `f` is circle integrable, then so are its scalar multiples.  -/
CircleIntegrable.const_smul : ∀ {c : ℂ} {R : ℝ} {A : Type u_2} [inst : NormedRing A] {a : A} {f : ℂ → A},
  CircleIntegrable f c R → CircleIntegrable (a • f) c R
-- Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
CategoryTheory.Triangulated.TStructure.eTruncLTGEIsoGELT_hom_naturality_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) [inst_6 : CategoryTheory.IsTriangulated C] (a b : EInt) {X Y : C}
  (f : X ⟶ Y) {Z : C} (h : (t.eTruncGE.obj a).obj ((t.eTruncLT.obj b).obj Y) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((t.eTruncLT.obj b).map ((t.eTruncGE.obj a).map f))
      (CategoryTheory.CategoryStruct.comp ((t.eTruncLTGEIsoGELT a b).hom.app Y) h) =
    CategoryTheory.CategoryStruct.comp ((t.eTruncLTGEIsoGELT a b).hom.app X)
      (CategoryTheory.CategoryStruct.comp ((t.eTruncGE.obj a).map ((t.eTruncLT.obj b).map f)) h)
-- Lean.Declaration
Lean.instInhabitedReducibilityHints : Inhabited Lean.ReducibilityHints
-- Mathlib.Topology.Algebra.InfiniteSum.Defs
HasSum.tsum_eq : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {L : SummationFilter β}
  {f : β → α} {a : α} [T2Space α] [L.NeBot], HasSum f a L → ∑'[L] (b : β), f b = a
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.mem_cocycles₁_def : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A : Rep.{u_1, u, u} k G} (f : G → ↑A),
  f ∈ groupCohomology.cocycles₁ A ↔ ∀ (g h : G), (A.ρ g) (f h) - f (g * h) + f g = 0
-- Mathlib.Geometry.Manifold.VectorBundle.Riemannian
/-- A trivial vector bundle, in which the model fiber has a scalar product,
is a Riemannian bundle.  -/
instIsContMDiffRiemannianBundleTrivial : ∀ {EB : Type u_1} [inst : NormedAddCommGroup EB] [inst_1 : NormedSpace ℝ EB] {HB : Type u_2}
  [inst_2 : TopologicalSpace HB] {IB : ModelWithCorners ℝ EB HB} {n : WithTop ℕ∞} {B : Type u_3}
  [inst_3 : TopologicalSpace B] [inst_4 : ChartedSpace HB B] {F₁ : Type u_6} [inst_5 : NormedAddCommGroup F₁]
  [inst_6 : InnerProductSpace ℝ F₁], IsContMDiffRiemannianBundle IB n F₁ (Bundle.Trivial B F₁)
-- Mathlib.CategoryTheory.ObjectProperty.Shift
/-- The closure by shifts and isomorphism of a predicate on objects in a category.  -/
CategoryTheory.ObjectProperty.shiftClosure : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    CategoryTheory.ObjectProperty C →
      (A : Type u_2) → [inst_1 : AddMonoid A] → [CategoryTheory.HasShift C A] → CategoryTheory.ObjectProperty C
-- Mathlib.Order.CompleteBooleanAlgebra
Order.Frame.toDistribLattice : {α : Type u} → [Order.Frame α] → DistribLattice α
-- Init.RCases
/-- `_` is a pattern which ignores the value and gives it an inaccessible name  -/
Lean.Parser.Tactic.rcasesPat.ignore : Lean.ParserDescr
-- Mathlib.CategoryTheory.Retract
/-- An object `X` is a retract of `Y` if there are morphisms `i : X ⟶ Y` and `r : Y ⟶ X` such
that `i ≫ r = 𝟙 X`.  -/
CategoryTheory.Retract : {C : Type u} → [CategoryTheory.Category.{v, u} C] → C → C → Type v
-- Mathlib.Data.Set.Card
Set.ncard_empty : ∀ (α : Type u_3), ∅.ncard = 0
-- Mathlib.Algebra.Group.Basic
sub_eq_sub_iff_sub_eq_sub : ∀ {G : Type u_3} [inst : AddCommGroup G] {a b c d : G}, a - b = c - d ↔ a - c = b - d
-- Std.Internal.Do.ExceptPost
/-- Exception postcondition type notation: `EPost⟨ε₁ → l, ε₂ → l⟩` for nested `EPost.Cons`.  -/
Std.Internal.Do.«termEPost⟨_⟩» : Lean.ParserDescr
-- Mathlib.Algebra.Algebra.Spectrum.Basic
_private.Mathlib.Algebra.Algebra.Spectrum.Basic.0.spectrum.termσ : Lean.ParserDescr
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Functor.instMonoidalMonMapAddMon.eq_1 : ∀ {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) [inst_4 : CategoryTheory.BraidedCategory C]
  [inst_5 : CategoryTheory.BraidedCategory D] [inst_6 : F.Braided],
  F.instMonoidalMonMapAddMon =
    { εIso := CategoryTheory.AddMon.mkIso (CategoryTheory.Functor.Monoidal.εIso F) ⋯ ⋯,
        μIso := fun M N => CategoryTheory.AddMon.mkIso (CategoryTheory.Functor.Monoidal.μIso F M.X N.X) ⋯ ⋯,
        μIso_hom_natural_left := ⋯, μIso_hom_natural_right := ⋯, associativity := ⋯, left_unitality := ⋯,
        right_unitality := ⋯ }.toMonoidal
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
/-- For all `0 < x < π/2` we have `x < tan x`.

This is proved by checking that the function `tan x - x` vanishes
at zero and has non-negative derivative.  -/
Real.lt_tan : ∀ {x : ℝ}, 0 < x → x < Real.pi / 2 → x < Real.tan x
-- Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal
/-- Given a term in the cone over the diagram
`(proj (op ⦋n⦌) ((Truncated.inclusion 2).op ⋙ (Truncated.inclusion 2).op ⋙ X)` where `X` is
Strict Segal, one can produce an `n`-simplex in `X`.  -/
SSet.StrictSegal.isPointwiseRightKanExtensionAt.lift : {X : SSet} →
  X.StrictSegal →
    {n : ℕ} →
      (s :
          CategoryTheory.Limits.Cone
            ((CategoryTheory.StructuredArrow.proj (Opposite.op { len := n })
                  (SimplexCategory.Truncated.inclusion 2).op).comp
              ((SimplexCategory.Truncated.inclusion 2).op.comp X))) →
        s.pt → X.obj (Opposite.op { len := n })
-- Mathlib.Analysis.InnerProductSpace.Harmonic.HarmonicContOnCl
/-- Eta-expanded form of `InnerProductSpace.HarmonicContOnCl.sub_const` -/
InnerProductSpace.HarmonicContOnCl.fun_sub_const : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  {F : Type u_2} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] {f : E → F} {s : Set E},
  InnerProductSpace.HarmonicContOnCl f s → ∀ (c : F), InnerProductSpace.HarmonicContOnCl (fun i => f i - c) s
-- Mathlib.Data.Set.Lattice.Image
Set.biUnion_range : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {f : ι → α} {g : α → Set β}, ⋃ x ∈ Set.range f, g x = ⋃ y, g (f y)
-- Mathlib.Algebra.Lie.Weights.Basic
LieModule.finite_genWeightSpaceOf_ne_bot : ∀ (R : Type u_2) (L : Type u_3) (M : Type u_4) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L] [IsDomain R] [Module.IsTorsionFree R M] [IsNoetherian R M] (x : L),
  {χ | LieModule.genWeightSpaceOf M χ x ≠ ⊥}.Finite
-- Lean.Util.CollectMVars
Lean.CollectMVars.State.mk.sizeOf_spec : ∀ (visitedExpr : Lean.ExprSet) (result : Array Lean.MVarId),
  sizeOf { visitedExpr := visitedExpr, result := result } = 1 + sizeOf visitedExpr + sizeOf result
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey!_eq_of_contains : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] [inst_2 : Inhabited α] {k : α}, t.contains k = true → t.getKey! k = k
-- Mathlib.CategoryTheory.Sites.Coherent.ExtensiveSheaves
CategoryTheory.instHasPairwisePullbacksOfExtensive : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.FinitaryPreExtensive C] {X : C}
  (S : CategoryTheory.Presieve X) [S.Extensive], S.HasPairwisePullbacks
-- Mathlib.Analysis.Calculus.IteratedDeriv.Defs
iteratedDeriv_one : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F}, iteratedDeriv 1 f = deriv f
-- Mathlib.Topology.LocallyConstant.Algebra
/-- `LocallyConstant.comap` as an `AlgHom`  -/
LocallyConstant.comapₐ : {X : Type u_1} →
  {Y : Type u_2} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] →
        {Z : Type u_6} →
          (R : Type u_7) →
            [inst_2 : CommSemiring R] →
              [inst_3 : Semiring Z] → [inst_4 : Algebra R Z] → C(X, Y) → LocallyConstant Y Z →ₐ[R] LocallyConstant X Z
-- Mathlib.AlgebraicGeometry.Morphisms.FlatDescent
/-- Surjective satisfies fpqc descent.  -/
AlgebraicGeometry.Flat.surjective_descendsAlong_surjective_inf_flat_inf_quasicompact : CategoryTheory.MorphismProperty.DescendsAlong (@AlgebraicGeometry.Surjective)
  (@AlgebraicGeometry.Surjective ⊓ @AlgebraicGeometry.Flat ⊓ @AlgebraicGeometry.QuasiCompact)
-- Mathlib.LinearAlgebra.StdBasis
Pi.basisFun_apply : ∀ (R : Type u_2) (η : Type u_4) [inst : Semiring R] [inst_1 : Finite η] [inst_2 : DecidableEq η] (i : η),
  (Pi.basisFun R η) i = Pi.single i 1
-- Mathlib.Algebra.Category.HopfAlgCat.Basic
HopfAlgCat.forget₂_bialgebra_map : ∀ {R : Type u} [inst : CommRing R] (X Y : HopfAlgCat R) (f : X ⟶ Y),
  (CategoryTheory.forget₂ (HopfAlgCat R) (BialgCat R)).map f = BialgCat.ofHom (HopfAlgCat.Hom.toBialgHom f)
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
measurable_inr : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β], Measurable Sum.inr
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- A point is in an affine subspace coerced to a set if and only if it is in that affine
subspace.  -/
AffineSubspace.mem_coe : ∀ {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] (p : P) (s : AffineSubspace k P), p ∈ ↑s ↔ p ∈ s
-- Mathlib.NumberTheory.Padics.PadicNumbers
Padic.norm_intCast_eq_one_iff : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {z : ℤ}, ‖↑z‖ = 1 ↔ IsCoprime z ↑p
-- Mathlib.FieldTheory.Galois.GaloisClosure
FiniteGaloisIntermediateField.adjoin_simple_map_algHom : ∀ {k : Type u_1} {K : Type u_2} [inst : Field k] [inst_1 : Field K] [inst_2 : Algebra k K] [inst_3 : IsGalois k K]
  (f : K →ₐ[k] K) (x : K), FiniteGaloisIntermediateField.adjoin k {f x} = FiniteGaloisIntermediateField.adjoin k {x}
-- Mathlib.Order.Category.BddOrd
_private.Mathlib.Order.Category.BddOrd.0.BddOrd.Hom.mk.sizeOf_spec : ∀ {X Y : BddOrd} (hom' : BoundedOrderHom ↑X.toPartOrd ↑Y.toPartOrd), sizeOf { hom' := hom' } = 1 + sizeOf hom'
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.le_minKey : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {he : t ≠ ∅}, (cmp k (t.minKey he)).isLE = true ↔ ∀ k' ∈ t, (cmp k k').isLE = true
-- Std.Data.Internal.List.Associative
Std.Internal.List.insertEntry_cons_of_beq : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {l : List ((a : α) × β a)} {k k' : α} {v : β k} {v' : β k'},
  (k' == k) = true → Std.Internal.List.insertEntry k v (⟨k', v'⟩ :: l) = ⟨k, v⟩ :: l
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.mulSingle_ne_one_iff : ∀ {ι : Type u_1} {S : ι → Type u_3} {G : ι → Type u_4} [inst : (i : ι) → SetLike (S i) (G i)] (A : (i : ι) → S i)
  [inst_1 : DecidableEq ι] [inst_2 : (i : ι) → One (G i)] [inst_3 : ∀ (i : ι), OneMemClass (S i) (G i)] (i : ι)
  {x : G i}, RestrictedProduct.mulSingle A i x ≠ 1 ↔ x ≠ 1
-- Mathlib.NumberTheory.KummerDedekind
KummerDedekind.Ideal.irreducible_map_of_irreducible_minpoly : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {x : S} {I : Ideal R}
  [IsDomain R] [IsIntegrallyClosed R] [IsDedekindDomain S] [Module.IsTorsionFree R S],
  I.IsMaximal →
    I ≠ ⊥ →
      Ideal.comap (algebraMap R S) (conductor R x) ⊔ I = ⊤ →
        IsIntegral R x →
          Irreducible (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)) → Irreducible (Ideal.map (algebraMap R S) I)
-- Lean.Linter.TacticTypeCheck
/-- Warn when the goal target is not type-correct at `.implicit` transparency.
This can happen when e.g. `unfold` leaves hypotheses whose types still refer to
the pre-unfolded definition, preventing `rw`/`simp` from matching patterns.
 -/
_private.Lean.Linter.TacticTypeCheck.0.Lean.Linter.linter.tacticCheckInstances : Lean.Option Bool
-- Mathlib.GroupTheory.Nilpotent
/-- Quotienting the `center G` reduces the nilpotency class by 1.  -/
Group.nilpotencyClass_quotient_center : ∀ {G : Type u_1} [inst : Group G], Group.nilpotencyClass (G ⧸ Subgroup.center G) = Group.nilpotencyClass G - 1
-- Mathlib.Analysis.Normed.Algebra.QuaternionExponential
Quaternion.normSq_exp : ∀ (q : Quaternion ℝ), Quaternion.normSq (NormedSpace.exp q) = NormedSpace.exp q.re ^ 2
-- Mathlib.Combinatorics.Quiver.Symmetric
Quiver.Symmetrify.lift_reverse : ∀ {V : Type u_2} [inst : Quiver V] {V' : Type u_4} [inst_1 : Quiver V'] [h : Quiver.HasInvolutiveReverse V']
  (φ : V ⥤q V') {X Y : Quiver.Symmetrify V} (f : X ⟶ Y),
  (Quiver.Symmetrify.lift φ).map (Quiver.reverse f) = Quiver.reverse ((Quiver.Symmetrify.lift φ).map f)
-- Mathlib.Analysis.Complex.Order
/-- **Alias** of the reverse direction of `Complex.zero_le_real`. -/
Mathlib.Meta.Positivity.ofReal_nonneg : ∀ {x : ℝ}, 0 ≤ x → 0 ≤ ↑x
-- Mathlib.Data.Finite.Defs
Finite.nonempty_decidableEq : ∀ (α : Sort u_1) [Finite α], Nonempty (DecidableEq α)
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.EqCnstr.brecOn.eq : ∀ {motive_1 : Lean.Meta.Grind.Arith.Linear.EqCnstr → Sort u}
  {motive_2 : Lean.Meta.Grind.Arith.Linear.EqCnstrProof → Sort u}
  {motive_3 : Lean.Meta.Grind.Arith.Linear.IneqCnstr → Sort u}
  {motive_4 : Lean.Meta.Grind.Arith.Linear.IneqCnstrProof → Sort u}
  {motive_5 : Lean.Meta.Grind.Arith.Linear.DiseqCnstr → Sort u}
  {motive_6 : Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof → Sort u}
  {motive_7 : Lean.Meta.Grind.Arith.Linear.UnsatProof → Sort u} (t : Lean.Meta.Grind.Arith.Linear.EqCnstr)
  (F_1 : (t : Lean.Meta.Grind.Arith.Linear.EqCnstr) → t.below → motive_1 t)
  (F_2 : (t : Lean.Meta.Grind.Arith.Linear.EqCnstrProof) → t.below → motive_2 t)
  (F_3 : (t : Lean.Meta.Grind.Arith.Linear.IneqCnstr) → t.below → motive_3 t)
  (F_4 : (t : Lean.Meta.Grind.Arith.Linear.IneqCnstrProof) → t.below → motive_4 t)
  (F_5 : (t : Lean.Meta.Grind.Arith.Linear.DiseqCnstr) → t.below → motive_5 t)
  (F_6 : (t : Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof) → t.below → motive_6 t)
  (F_7 : (t : Lean.Meta.Grind.Arith.Linear.UnsatProof) → t.below → motive_7 t),
  t.brecOn F_1 F_2 F_3 F_4 F_5 F_6 F_7 =
    F_1 t (Lean.Meta.Grind.Arith.Linear.EqCnstr.brecOn.go t F_1 F_2 F_3 F_4 F_5 F_6 F_7).2
-- Mathlib.RingTheory.Congruence.Opposite
/-- The congruences of a ring `R` biject to the congruences of the opposite ring `Rᵐᵒᵖ`.
 -/
RingCon.opOrderIso : {R : Type u_1} → [inst : Add R] → [inst_1 : Mul R] → RingCon R ≃o RingCon Rᵐᵒᵖ
-- Init.Tactics
/-- Use this rewrite rule before entering the subterms  -/
Lean.Parser.Tactic.simpPre : Lean.ParserDescr
-- Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
CategoryTheory.Triangulated.TStructure.instIsIsoFunctorETruncLTGELTSelfToLTGE : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) [CategoryTheory.IsTriangulated C] (a b : EInt),
  CategoryTheory.IsIso (t.eTruncLTGELTSelfToLTGE a b)
-- Mathlib.MeasureTheory.Measure.Haar.Unique
MeasureTheory.Measure.addHaarScalarFactor_domSMul : ∀ {G : Type u_1} {A : Type u_2} [inst : Group G] [inst_1 : AddCommGroup A] [inst_2 : DistribMulAction G A]
  [inst_3 : MeasurableSpace A] [inst_4 : TopologicalSpace A] [inst_5 : BorelSpace A] [inst_6 : IsTopologicalAddGroup A]
  [LocallyCompactSpace A] [inst_8 : ContinuousConstSMul G A] (μ ν : MeasureTheory.Measure A)
  [inst_9 : μ.IsAddHaarMeasure] [inst_10 : ν.IsAddHaarMeasure] (g : Gᵈᵐᵃ),
  (g • μ).addHaarScalarFactor (g • ν) = μ.addHaarScalarFactor ν
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.coeIdeal_eq_zero : ∀ {R : Type u_1} [inst : CommRing R] {K : Type u_3} [inst_1 : Field K] [inst_2 : Algebra R K] [IsFractionRing R K]
  {I : Ideal R}, ↑I = 0 ↔ I = ⊥
-- Mathlib.Topology.EMetricSpace.PairReduction
PairReduction.one_le_radius_logSizeBallSeq : ∀ {T : Type u_1} [inst : PseudoEMetricSpace T] {a c : ENNReal} {J : Finset T} [inst_1 : DecidableEq T]
  (hJ : J.Nonempty), 1 < a → ∀ (i : ℕ), 1 ≤ (PairReduction.logSizeBallSeq J hJ a c i).radius
-- Init.ShareCommon
MonadShareCommon.withShareCommon : {m : Type u → Type v} → [self : MonadShareCommon m] → {α : Type u} → α → m α
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
IsUniformAddGroup.mk' : ∀ {α : Type u_3} [inst : UniformSpace α] [inst_1 : AddGroup α],
  (UniformContinuous fun p => p.1 + p.2) → (UniformContinuous fun p => -p) → IsUniformAddGroup α