mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Server.FileWorker.SemanticHighlighting
/-- End position of the semantic token.  -/
Lean.Server.FileWorker.AbsoluteLspSemanticToken.tailPos : Lean.Server.FileWorker.AbsoluteLspSemanticToken → Lean.Lsp.Position
-- Mathlib.Analysis.BoxIntegral.Partition.Filter
BoxIntegral.IntegrationParams.hasBasis_toFilteriUnion_top : ∀ {ι : Type u_1} [inst : Fintype ι] (l : BoxIntegral.IntegrationParams) (I : BoxIntegral.Box ι),
  (BoxIntegral.IntegrationParams.toFilteriUnion I ⊤).HasBasis (fun r => ∀ (c : NNReal), l.RCond (r c)) fun r =>
    {π | ∃ c, l.MemBaseSet I c (r c) π ∧ π.IsPartition}
-- Mathlib.Algebra.GCDMonoid.Multiset
Multiset.dvd_lcm : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] {s : Multiset α} {a : α},
  a ∈ s → a ∣ s.lcm
-- Mathlib.Data.ENNReal.Basic
ENNReal.instDenselyOrdered : DenselyOrdered ENNReal
-- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
MeasureTheory.lintegral_indicator_one₀ : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α},
  MeasureTheory.NullMeasurableSet s μ → ∫⁻ (a : α), s.indicator 1 a ∂μ = μ s
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
sign_cases_of_C_mul_pow_nonneg : ∀ {R : Type u} [inst : Semiring R] [inst_1 : LinearOrder R] {a b : R} [PosMulStrictMono R],
  (∀ (n : ℕ), 0 ≤ a * b ^ n) → a = 0 ∨ 0 < a ∧ 0 ≤ b
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
/-- If `f` is locally integrable and `g` is continuous with compact support,
then `g • f` is integrable.  -/
MeasureTheory.LocallyIntegrable.integrable_smul_left_of_hasCompactSupport : ∀ {X : Type u_1} {E : Type u_6} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] [inst_2 : NormedAddCommGroup E]
  {μ : MeasureTheory.Measure X} {𝕜 : Type u_9} [inst_3 : NormedRing 𝕜] [inst_4 : Module 𝕜 E] [IsBoundedSMul 𝕜 E]
  [OpensMeasurableSpace X] [T2Space X] {f : X → E},
  MeasureTheory.LocallyIntegrable f μ →
    ∀ {g : X → 𝕜}, Continuous g → HasCompactSupport g → MeasureTheory.Integrable (fun x => g x • f x) μ
-- Mathlib.CategoryTheory.Category.Cat.Limit
CategoryTheory.Cat.instPreservesLimitsObjects : CategoryTheory.Limits.PreservesLimits CategoryTheory.Cat.objects
-- Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
SSet.Truncated.HomotopyCategory.mkNatTrans_app_mk : ∀ {V : SSet.Truncated 2} {D : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} D]
  {F G : CategoryTheory.Functor V.HomotopyCategory D}
  (φ :
    (x : V.obj (Opposite.op { obj := { len := 0 }, property := SSet.OneTruncation₂._proof_1 })) →
      F.obj (SSet.Truncated.HomotopyCategory.mk x) ⟶ G.obj (SSet.Truncated.HomotopyCategory.mk x))
  (hφ :
    autoParam
      (∀ ⦃x y : V.obj (Opposite.op { obj := { len := 0 }, property := SSet.OneTruncation₂._proof_1 })⦄
        (e : SSet.Truncated.Edge x y),
        CategoryTheory.CategoryStruct.comp (F.map (SSet.Truncated.HomotopyCategory.homMk e)) (φ y) =
          CategoryTheory.CategoryStruct.comp (φ x) (G.map (SSet.Truncated.HomotopyCategory.homMk e)))
      _auto_140✝)
  (v : V.obj (Opposite.op { obj := { len := 0 }, property := SSet.OneTruncation₂._proof_1 })),
  (SSet.Truncated.HomotopyCategory.mkNatTrans φ hφ).app (SSet.Truncated.HomotopyCategory.mk v) = φ v
-- Mathlib.Analysis.Analytic.Composition
/-- If two functions `g` and `f` are continuously polynomial respectively on `s.image f` and `s`,
then `g ∘ f` is continuously polynomial on `s`.  -/
CPolynomialOn.comp' : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {s : Set E} {g : F → G} {f : E → F},
  CPolynomialOn 𝕜 g (f '' s) → CPolynomialOn 𝕜 f s → CPolynomialOn 𝕜 (g ∘ f) s
-- Mathlib.GroupTheory.Index
Subgroup.fintypeQuotientOfFiniteIndex.eq_1 : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} [inst_1 : H.FiniteIndex],
  Subgroup.fintypeQuotientOfFiniteIndex = Subgroup.fintypeOfIndexNeZero ⋯
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.add_mk_eq_self : ∀ {α : Type u_1} [Infinite α], Cardinal.mk α + Cardinal.mk α = Cardinal.mk α
-- Mathlib.Topology.Compactness.Compact
/-- If `y` is a unique `MapClusterPt` for `f` along `l`
and the codomain of `f` is a compact space,
then `f` tends to `𝓝 y` along `l`.  -/
tendsto_nhds_of_unique_mapClusterPt : ∀ {X : Type u} [inst : TopologicalSpace X] [CompactSpace X] {Y : Type u_2} {l : Filter Y} {y : X} {f : Y → X},
  (∀ (x : X), MapClusterPt x l f → x = y) → Filter.Tendsto f l (nhds y)
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.Zipper.step.eq_1 : ∀ {α : Type u} {β : α → Type v}, Std.DTreeMap.Internal.Zipper.done.step = Std.IterStep.done
-- Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
MeasureTheory.eLpNorm_le_eLpNorm_mul_rpow_measure_univ : ∀ {α : Type u_1} {ε : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ε}
  [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε] {p q : ENNReal},
  p ≤ q →
    MeasureTheory.AEStronglyMeasurable f μ →
      MeasureTheory.eLpNorm f p μ ≤ MeasureTheory.eLpNorm f q μ * μ Set.univ ^ (1 / p.toReal - 1 / q.toReal)
-- Init.Data.Iterators.Combinators.Monadic.Attach
Std.Iterators.Types.Attach.mk.congr_simp : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} [inst : Std.Iterator α m β] {P : β → Prop}
  (inner inner_1 : Std.IterM m β) (e_inner : inner = inner_1)
  (invariant : ∀ (out : β), inner.IsPlausibleIndirectOutput out → P out),
  { inner := inner, invariant := invariant } = { inner := inner_1, invariant := ⋯ }
-- Mathlib.Topology.Algebra.Group.Basic
Homeomorph.mulLeft.eq_1 : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Group G] [inst_2 : SeparatelyContinuousMul G] (a : G),
  Homeomorph.mulLeft a = { toEquiv := Equiv.mulLeft a, continuous_toFun := ⋯, continuous_invFun := ⋯ }
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat.0.Nat.EqResult.decide : Bool → Nat.EqResult✝
-- Mathlib.Algebra.Category.AlgCat.Basic
/-- The underlying algebra map.  -/
AlgCat.Hom.hom' : {R : Type u} → [inst : CommRing R] → {A B : AlgCat R} → A.Hom B → ↑A →ₐ[R] ↑B
-- Mathlib.CategoryTheory.Bicategory.Modification.Lax
CategoryTheory.Lax.LaxTrans.Modification.instInhabited : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.LaxFunctor B C} → {η : F ⟶ G} → Inhabited (CategoryTheory.Lax.LaxTrans.Modification η η)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.denote'.eq_1 : ∀ {α : Type u_1} [inst : Lean.Grind.Ring α] (ctx : Lean.Grind.CommRing.Context α) (k : ℤ),
  Lean.Grind.CommRing.Poly.denote' ctx (Lean.Grind.CommRing.Poly.num k) = ↑k
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
/-- Writing explicitly the derivative of the `n`-th derivative as the composition of a currying
linear equiv, and the `n + 1`-th derivative.  -/
fderiv_iteratedFDeriv : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {n : ℕ},
  fderiv 𝕜 (iteratedFDeriv 𝕜 n f) = ⇑(continuousMultilinearCurryLeftEquiv 𝕜 (fun x => E) F) ∘ iteratedFDeriv 𝕜 (n + 1) f
-- Mathlib.RingTheory.TwoSidedIdeal.Operations
TwoSidedIdeal.mem_asIdealOpposite : ∀ {R : Type u_1} [inst : Ring R] {I : TwoSidedIdeal R} {x : Rᵐᵒᵖ},
  x ∈ TwoSidedIdeal.asIdealOpposite I ↔ MulOpposite.unop x ∈ I
-- Mathlib.Combinatorics.Matroid.Minor.Delete
Matroid.delete_closure_eq : ∀ {α : Type u_1} (M : Matroid α) (D X : Set α), (M.delete D).closure X = M.closure (X \ D) \ D
-- Mathlib.SetTheory.ZFC.Class
Class.powerset_apply : ∀ {A : Class.{u}} {x : ZFSet.{u}}, A.powerset x ↔ ↑x ⊆ A
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.homologyFunctorIso_hom_app : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} (c : ComplexShape ι) (i : ι) [inst_2 : CategoryTheory.CategoryWithHomology C]
  (X : HomologicalComplex C c),
  (HomologicalComplex.homologyFunctorIso C c i).hom.app X = CategoryTheory.CategoryStruct.id (X.homology i)
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.exact_and_mono_f_iff_of_iso : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (e : S₁ ≅ S₂),
  S₁.Exact ∧ CategoryTheory.Mono S₁.f ↔ S₂.Exact ∧ CategoryTheory.Mono S₂.f
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
CategoryTheory.IsPushout.inr_isoIsPushout_inv_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Z : C} (X Y : C) {P : C} {f : Z ⟶ X} {g : Z ⟶ Y}
  {inl : X ⟶ P} {inr : Y ⟶ P} {P' : C} {inl' : X ⟶ P'} {inr' : Y ⟶ P'} (h : CategoryTheory.IsPushout f g inl inr)
  (h' : CategoryTheory.IsPushout f g inl' inr') {Z_1 : C} (h_1 : P ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp inr'
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.IsPushout.isoIsPushout X Y h h').inv h_1) =
    CategoryTheory.CategoryStruct.comp inr h_1
-- Mathlib.LinearAlgebra.Basis.Defs
/-- The sum of the coordinates of an element `m : M` with respect to a basis.  -/
Module.Basis.sumCoords : {ι : Type u_10} →
  {R : Type u_11} →
    {M : Type u_12} →
      [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → Module.Basis ι R M → M →ₗ[R] R
-- Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
GaloisConnection.u_ciInf_set_of_directedOn : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : ConditionallyCompletePartialOrderInf α]
  [inst_1 : ConditionallyCompletePartialOrderInf β] {l : α → β} {u : β → α},
  GaloisConnection u l →
    ∀ {s : Set γ} {f : γ → α},
      DirectedOn (fun x1 x2 => x2 ≤ x1) (f '' s) → BddBelow (f '' s) → s.Nonempty → l (⨅ i, f ↑i) = ⨅ i, l (f ↑i)
-- Mathlib.Data.Finset.NAry
Finset.image₂_inter_union_subset : ∀ {α : Type u_1} {β : Type u_3} [inst : DecidableEq α] [inst_1 : DecidableEq β] {f : α → α → β} {s t : Finset α},
  (∀ (a b : α), f a b = f b a) → Finset.image₂ f (s ∩ t) (s ∪ t) ⊆ Finset.image₂ f s t
-- Mathlib.AlgebraicTopology.ModelCategory.Cylinder
HomotopicalAlgebra.Cylinder.exists_very_good : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C] (A : C),
  ∃ P, P.IsVeryGood
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
_private.Init.Data.String.Lemmas.Pattern.TakeDrop.Basic.0.String.Slice.Pos.revSkipWhile.eq_def : ∀ {ρ : Type} {s : String.Slice} (pos : s.Pos) (pat : ρ) [inst : String.Slice.Pattern.BackwardPattern pat],
  pos.revSkipWhile pat =
    match pos.revSkip? pat with
    | some nextCurr => if nextCurr < pos then nextCurr.revSkipWhile pat else pos
    | none => pos
-- Lean.Meta.Tactic.Grind.Arith.EvalNum
_private.Lean.Meta.Tactic.Grind.Arith.EvalNum.0.Lean.Meta.Grind.Arith.evalIntCore : Lean.Expr → OptionT Lean.Meta.Grind.GrindM ℤ
-- Mathlib.Data.Real.Embedding
Archimedean.ratLt_bddAbove : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [IsOrderedAddMonoid M] [inst_3 : One M]
  [ZeroLEOneClass M] [NeZero 1] [Archimedean M] (x : M), BddAbove (Archimedean.ratLt x)
-- Mathlib.Probability.Independence.Kernel.Indep
/-- Two sets of sets `s₁, s₂` are independent with respect to a kernel `κ` and a measure `μ` if for
any sets `t₁ ∈ s₁, t₂ ∈ s₂`, then `∀ᵐ a ∂μ, κ a (t₁ ∩ t₂) = κ a (t₁) * κ a (t₂)`  -/
ProbabilityTheory.Kernel.IndepSets : {α : Type u_1} →
  {Ω : Type u_2} →
    {_mα : MeasurableSpace α} →
      {_mΩ : MeasurableSpace Ω} →
        Set (Set Ω) →
          Set (Set Ω) →
            ProbabilityTheory.Kernel α Ω →
              autoParam (MeasureTheory.Measure α) ProbabilityTheory.Kernel.IndepSets._auto_1 → Prop
-- Mathlib.AlgebraicGeometry.StructureSheaf
/-- The structure sheaf of a module as a presheaf of modules on `Spec R`.
We will later package this into a `Scheme.Modules` in `Tilde.lean`.  -/
AlgebraicGeometry.moduleStructurePresheaf : (R M : Type u) →
  [inst : CommRing R] →
    [inst_1 : AddCommGroup M] →
      [Module R M] →
        PresheafOfModules
          (CategoryTheory.Functor.comp (AlgebraicGeometry.structurePresheafInCommRingCat R)
            (CategoryTheory.forget₂ CommRingCat RingCat))
-- Mathlib.Algebra.Group.UniqueProds.Basic
UniqueAdd.iff_addOpposite : ∀ {G : Type u_1} [inst : Add G] {A B : Finset G} {a0 b0 : G},
  UniqueAdd (Finset.map { toFun := AddOpposite.op, inj' := ⋯ } B) (Finset.map { toFun := AddOpposite.op, inj' := ⋯ } A)
      (AddOpposite.op b0) (AddOpposite.op a0) ↔
    UniqueAdd A B a0 b0
-- Mathlib.CategoryTheory.Limits.Chosen.End
CategoryTheory.Limits.chosenEndFunctor_map : ∀ {J : Type u_3} {C : Type u_4} [inst : CategoryTheory.Category.{v_3, u_4} C]
  [inst_1 : CategoryTheory.Category.{v_4, u_3} J] [inst_2 : CategoryTheory.Limits.ChosenEndsOfShape J C]
  {X Y : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} (f : X ⟶ Y),
  CategoryTheory.Limits.chosenEndFunctor.map f = CategoryTheory.Limits.chosenEnd.map f
-- Mathlib.RingTheory.GradedAlgebra.AlgHom
GradedAlgHom.comp_apply : ∀ {R : Type u_1} {A : Type u_6} {B : Type u_7} {C : Type u_8} {ι : Type u_10} [inst : CommSemiring R]
  [inst_1 : Semiring A] [inst_2 : Semiring B] [inst_3 : Semiring C] [inst_4 : Algebra R A] [inst_5 : Algebra R B]
  [inst_6 : Algebra R C] [inst_7 : DecidableEq ι] [inst_8 : AddMonoid ι] {𝒜 : ι → Submodule R A} {ℬ : ι → Submodule R B}
  {𝒞 : ι → Submodule R C} [inst_9 : GradedAlgebra 𝒜] [inst_10 : GradedAlgebra ℬ] [inst_11 : GradedAlgebra 𝒞]
  (g : ℬ →ₐᵍ[R] 𝒞) (f : 𝒜 →ₐᵍ[R] ℬ) (x : A), (g.comp f) x = g (f x)
-- Mathlib.Algebra.Module.LocalizedModule.AtPrime
/-- Given a prime ideal `P`, `LocalizedModule.AtPrime P M` is a localization of `M`
at the complement of `P`.  -/
LocalizedModule.AtPrime : {R : Type u_1} →
  [inst : CommSemiring R] →
    (P : Ideal R) → [P.IsPrime] → (M : Type u_2) → [inst_2 : AddCommMonoid M] → [Module R M] → Type (max u_1 u_2)
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.piComparison_comp_π_assoc : ∀ {β : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) (f : β → C)
  [inst_2 : CategoryTheory.Limits.HasProduct f] [inst_3 : CategoryTheory.Limits.HasProduct fun b => G.obj (f b)] (b : β)
  {Z : D} (h : G.obj (f b) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.piComparison G f)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π (fun b => G.obj (f b)) b) h) =
    CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.Pi.π f b)) h
-- Mathlib.Topology.Bornology.Absorbs
Absorbs.mono_right : ∀ {M : Type u_1} {α : Type u_2} [inst : Bornology M] [inst_1 : SMul M α] {s t₁ t₂ : Set α},
  Absorbs M s t₁ → t₂ ⊆ t₁ → Absorbs M s t₂
-- Mathlib.CategoryTheory.Presentable.Directed
CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.hW : ∀ {J : Type w} [inst : CategoryTheory.SmallCategory J] {κ : Cardinal.{w}}
  (self : CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram J κ), self.W.HasCardinalLT κ
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
Set.conj_mem_fixingSubgroup : ∀ {M : Type u_1} {α : Type u_2} [inst : Group M] [inst_1 : MulAction M α] {s t : Set α} {g : M},
  g • t = s → ∀ {k : M}, k ∈ fixingSubgroup M t → (MulAut.conj g) k ∈ fixingSubgroup M s
-- Batteries.Lean.EStateM
_private.Batteries.Lean.EStateM.0.EStateM.run_orElse.match_1.splitter : {σ ε α : Type u_1} →
  (motive : EStateM.Result ε σ α → Sort u_2) →
    (x : EStateM.Result ε σ α) →
      ((x : α) → (s : σ) → motive (EStateM.Result.ok x s)) →
        ((a : ε) → (s' : σ) → motive (EStateM.Result.error a s')) → motive x
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.mul_natCast_inj : ∀ {n : ℕ} {a b : Cardinal.{u_1}}, n ≠ 0 → (a * ↑n = b * ↑n ↔ a = b)
-- Mathlib.Analysis.Asymptotics.Defs
/-- We say that `f` is `Θ(g)` along a filter `l` (notation: `f =Θ[l] g`) if `f =O[l] g` and
`g =O[l] f`.  -/
Asymptotics.«term_=Θ[_]_» : Lean.TrailingParserDescr
-- Mathlib.Combinatorics.Hypergraph.Basic
Hypergraph.ne_bot_iff : ∀ {α : Type u_1} {H : Hypergraph α}, H ≠ ⊥ ↔ H.IsNonempty
-- Mathlib.Algebra.Star.Conjneg
conjneg_eq_one : ∀ {G : Type u_2} {R : Type u_3} [inst : AddGroup G] [inst_1 : CommSemiring R] [inst_2 : StarRing R] {f : G → R},
  conjneg f = 1 ↔ f = 1
-- Mathlib.NumberTheory.NumberField.Discriminant.Different
/-- Let `K₁` and `K₂` be two number fields and assume that their different ideals (over ℤ) are coprime.
Then, the absolute value of the discriminant of their compositum is equal to
`|discr K₁| ^ [K₂ : ℚ] * |discr K₂| ^ [K₁ : ℚ]`.
 -/
NumberField.natAbs_discr_eq_natAbs_discr_pow_mul_natAbs_discr_pow : ∀ (L : Type u_3) [inst : Field L] [inst_1 : NumberField L] (K₁ K₂ : IntermediateField ℚ L),
  K₁.LinearDisjoint ↥K₂ →
    K₁ ⊔ K₂ = ⊤ →
      IsCoprime
          (Ideal.map (algebraMap (NumberField.RingOfIntegers ↥K₁) (NumberField.RingOfIntegers L))
            (differentIdeal ℤ (NumberField.RingOfIntegers ↥K₁)))
          (Ideal.map (algebraMap (NumberField.RingOfIntegers ↥K₂) (NumberField.RingOfIntegers L))
            (differentIdeal ℤ (NumberField.RingOfIntegers ↥K₂))) →
        (NumberField.discr L).natAbs =
          (NumberField.discr ↥K₁).natAbs ^ Module.finrank ℚ ↥K₂ * (NumberField.discr ↥K₂).natAbs ^ Module.finrank ℚ ↥K₁
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
mem_nonUnitalSubalgebraOfNonUnitalSubsemiring : ∀ {R : Type u_1} [inst : NonUnitalNonAssocSemiring R] {x : R} {S : NonUnitalSubsemiring R},
  x ∈ nonUnitalSubalgebraOfNonUnitalSubsemiring S ↔ x ∈ S
-- Mathlib.Algebra.Group.Subgroup.Ker
AddSubgroup.map_le_map_iff' : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] {f : G →+ N} {H K : AddSubgroup G},
  AddSubgroup.map f H ≤ AddSubgroup.map f K ↔ H ⊔ f.ker ≤ K ⊔ f.ker
-- Mathlib.Data.Finset.Sups
Finset.disjSups_subset_iff : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SemilatticeSup α] [inst_2 : OrderBot α]
  [inst_3 : DecidableRel Disjoint] {s t u : Finset α}, s.disjSups t ⊆ u ↔ ∀ a ∈ s, ∀ b ∈ t, Disjoint a b → a ⊔ b ∈ u
-- Mathlib.Topology.Algebra.Constructions.DomMulAct
DomAddAct.map_mk_nhds : ∀ {M : Type u_1} [inst : TopologicalSpace M] (x : M), Filter.map (⇑DomAddAct.mk) (nhds x) = nhds (DomAddAct.mk x)
-- Lean.Elab.InfoTree.Types
Lean.Elab.instInhabitedTacticInfo.default : Lean.Elab.TacticInfo
-- Lean.Parser.Extension
Lean.Parser.ParserExtension.State.kinds : Lean.Parser.ParserExtension.State → Lean.Parser.SyntaxNodeKindSet
-- Init.Data.Int.DivMod.Lemmas
Int.fmod_add_mul_fdiv : ∀ (a b : ℤ), a.fmod b + b * a.fdiv b = a
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
/-- The following diagram is a pullback
```
X --id--> X
|         |
f         f
v         v
Z --id--> Z
```
 -/
CategoryTheory.IsPullback.id_horiz : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Z : C} (f : X ⟶ Z),
  CategoryTheory.IsPullback (CategoryTheory.CategoryStruct.id X) f f (CategoryTheory.CategoryStruct.id Z)
-- Mathlib.RepresentationTheory.Homological.GroupHomology.FiniteCyclic
Representation.ofCoinvariantsTprodLeftRegular.eq_1 : ∀ {k : Type u_6} {G : Type u_7} {V : Type u_8} [inst : CommRing k] [inst_1 : Group G] [inst_2 : AddCommGroup V]
  [inst_3 : Module k V] (ρ : Representation k G V),
  ρ.ofCoinvariantsTprodLeftRegular =
    Representation.Coinvariants.lift (ρ.tprod (Representation.leftRegular k G))
      (TensorProduct.lift ((Finsupp.linearCombination k fun g => ρ g⁻¹) ∘ₗ ↑(MonoidAlgebra.coeffLinearEquiv k)) ∘ₗ
        ↑(TensorProduct.comm k V (MonoidAlgebra k G)))
      ⋯
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.sub_subset_sub : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Sub α] {s₁ s₂ t₁ t₂ : Finset α}, s₁ ⊆ s₂ → t₁ ⊆ t₂ → s₁ - t₁ ⊆ s₂ - t₂
-- Mathlib.CategoryTheory.Limits.Presentation
/-- Map a limit presentation under an isomorphism.  -/
CategoryTheory.Limits.LimitPresentation.ofIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type w} →
      [inst_1 : CategoryTheory.Category.{t, w} J] →
        {X : C} →
          CategoryTheory.Limits.LimitPresentation J X → {Y : C} → (X ≅ Y) → CategoryTheory.Limits.LimitPresentation J Y
-- Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
MeasureTheory.HasFiniteIntegral.smul_enorm : ∀ {α : Type u_1} {ε'' : Type u_6} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : TopologicalSpace ε'']
  [inst_1 : ESeminormedAddMonoid ε''] {𝕜 : Type u_7} [inst_2 : NormedAddGroup 𝕜] [inst_3 : SMul 𝕜 ε'']
  [ENormSMulClass 𝕜 ε''] (c : 𝕜) {f : α → ε''},
  MeasureTheory.HasFiniteIntegral f μ → MeasureTheory.HasFiniteIntegral (c • f) μ
-- Mathlib.Logic.Equiv.Option
Equiv.optionEquivSumPUnit_none : ∀ {α : Type u_4}, (Equiv.optionEquivSumPUnit α) none = Sum.inr PUnit.unit
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.LawfulToForwardSearcherModel.isValidSearchFrom_toList : ∀ {ρ : Type} {pat : ρ} {inst : String.Slice.Pattern.Model.PatternModel pat} {σ : String.Slice → Type}
  {inst_1 : String.Slice.Pattern.ToForwardSearcher pat σ}
  {inst_2 : (s : String.Slice) → Std.Iterator (σ s) Id (String.Slice.Pattern.SearchStep s)}
  {inst_3 : ∀ (s : String.Slice), Std.Iterators.Finite (σ s) Id}
  [self : String.Slice.Pattern.Model.LawfulToForwardSearcherModel pat] (s : String.Slice),
  String.Slice.Pattern.Model.IsValidSearchFrom pat s.startPos
    (String.Slice.Pattern.ToForwardSearcher.toSearcher pat s).toList
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey!_union_of_not_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Inhabited α]
  [inst_1 : Std.TransCmp cmp] {k : α}, k ∉ t₂ → (t₁ ∪ t₂).getKey! k = t₁.getKey! k
-- Mathlib.RingTheory.PicardGroup
Module.Invertible.instLocalizationLocalizedModule : ∀ (R : Type u) (M : Type v) [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [Module.Invertible R M] (S : Submonoid R), Module.Invertible (Localization S) (LocalizedModule S M)
-- Mathlib.Analysis.Normed.Group.Constructions
/-- Finite product of seminormed groups, using the sup norm.  -/
Pi.seminormedGroup : {ι : Type u_1} → {G : ι → Type u_4} → [Fintype ι] → [(i : ι) → SeminormedGroup (G i)] → SeminormedGroup ((i : ι) → G i)
-- Mathlib.Topology.Algebra.FilterBasis
RingFilterBasis.mul : ∀ {R : Type u} [inst : Ring R] (B : RingFilterBasis R) {U : Set R}, U ∈ B → ∃ V ∈ B, V * V ⊆ U
-- Mathlib.GroupTheory.Divisible
/-- A group is `ℤ`-rootable if it is `ℕ`-rootable.
 -/
Group.rootableByIntOfRootableByNat : (A : Type u_1) → [inst : Group A] → [RootableBy A ℕ] → RootableBy A ℤ
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.nat_cast_mul : ∀ {R : Type u_5} [inst : Semiring R] (n : ℕ) (p : SkewPolynomial R) [inst_1 : MulSemiringAction (Multiplicative ℕ) R],
  ↑n * p = n • p
-- Mathlib.RingTheory.Ideal.HasGoingUp
/-- An `R`-algebra `S` has the going up property if and only if specializations lift
along `Spec S → Spec R`.  -/
Algebra.HasGoingUp.iff_specializingMap_primeSpectrumComap : ∀ {R : Type u_3} {S : Type u_4} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S],
  Algebra.HasGoingUp R S ↔ SpecializingMap (PrimeSpectrum.comap (algebraMap R S))
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
Nat.reduceSubDiff : Lean.Meta.Simp.Simproc
-- Mathlib.CategoryTheory.Presentable.SharplyLT.Basic
/-- This is the implication (i) → (iii) in the characterizations
of `SharplyLT κ₁ κ₂` in the docstring of this file.  -/
Cardinal.SharplyLT.exists_cofinal_of_isCardinalAccessibleCategory_cardinalDirectedPoset : ∀ {κ₁ κ₂ : Cardinal.{w}} [inst : Fact κ₁.IsRegular] [inst_1 : Fact κ₂.IsRegular],
  κ₁ ≤ κ₂ →
    ∀ [CategoryTheory.IsCardinalAccessibleCategory (CategoryTheory.CardinalDirectedPoset κ₁) κ₂] {X : Type w},
      HasCardinalLT X κ₂ → ∃ Y, HasCardinalLT (↑Y) κ₂ ∧ IsCofinal Y
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.isCycle_iff_isPath_tail_and_le_length : ∀ {V : Type u} {G : SimpleGraph V} {u : V} {p : G.Walk u u}, p.IsCycle ↔ p.tail.IsPath ∧ 3 ≤ p.length
-- Aesop.Search.Expansion
Aesop.SafeRulesResult.succeeded : Array Aesop.RappRef → Aesop.SafeRulesResult
-- Init.Grind.Norm
Lean.Grind.not_not : ∀ (p : Prop), (¬¬p) = p