mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.FDeriv.Prod
HasFDerivAtFilter.finCons : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {n : ℕ} {F' : Fin n.succ → Type u_6}
  [inst_3 : (i : Fin n.succ) → NormedAddCommGroup (F' i)] [inst_4 : (i : Fin n.succ) → NormedSpace 𝕜 (F' i)]
  {φ : E → F' 0} {φs : E → (i : Fin n) → F' i.succ} {φ' : E →L[𝕜] F' 0} {φs' : E →L[𝕜] (i : Fin n) → F' i.succ}
  {l : Filter (E × E)},
  HasFDerivAtFilter φ φ' l →
    HasFDerivAtFilter φs φs' l → HasFDerivAtFilter (fun x => Fin.cons (φ x) (φs x)) (φ'.finCons φs') l
-- Lean.Data.JsonRpc
Lean.JsonRpc.ErrorCode.noConfusionType : Sort v✝ → Lean.JsonRpc.ErrorCode → Lean.JsonRpc.ErrorCode → Sort v✝
-- Mathlib.AlgebraicTopology.SimplicialSet.Path
SSet.spine_vertex : ∀ (X : SSet) (n : ℕ) (Δ : X.obj (Opposite.op { len := n })) (i : Fin (n + 1)),
  (X.spine n Δ).vertex i = (CategoryTheory.ConcreteCategory.hom (X.map ({ len := 0 }.const { len := n } i).op)) Δ
-- Lean.LibrarySuggestions.Basic
Lean.LibrarySuggestions.Config.mk.injEq : ∀ (maxSuggestions : ℕ) (caller : Option String) (filter : Lean.Name → Lean.MetaM Bool) (hint : Option String)
  (maxSuggestions_1 : ℕ) (caller_1 : Option String) (filter_1 : Lean.Name → Lean.MetaM Bool) (hint_1 : Option String),
  ({ maxSuggestions := maxSuggestions, caller := caller, filter := filter, hint := hint } =
      { maxSuggestions := maxSuggestions_1, caller := caller_1, filter := filter_1, hint := hint_1 }) =
    (maxSuggestions = maxSuggestions_1 ∧ caller = caller_1 ∧ filter = filter_1 ∧ hint = hint_1)
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
/-- A useful constructor of `IdealSheafData`
with the condition on `supportSet` being easier to check.  -/
AlgebraicGeometry.Scheme.IdealSheafData.mkOfMemSupportIff : {X : AlgebraicGeometry.Scheme} →
  (ideal : (U : ↑X.affineOpens) → Ideal ↑(X.presheaf.obj (Opposite.op ↑U))) →
    (∀ (U : ↑X.affineOpens) (f : ↑(X.presheaf.obj (Opposite.op ↑U))),
        Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (CategoryTheory.homOfLE ⋯).op)) (ideal U) =
          ideal (X.affineBasicOpen f)) →
      (supportSet : Set ↥X) →
        (∀ (U : ↑X.affineOpens), ∀ x ∈ ↑U, x ∈ supportSet ↔ x ∈ X.zeroLocus ↑(ideal U)) → X.IdealSheafData
-- Mathlib.CategoryTheory.Limits.Shapes.Terminal
/-- For a functor `F : J ⥤ C`, if `J` has a terminal object and all the morphisms in the diagram
are isomorphisms, then the image of the terminal object is isomorphic to the limit of `F`.  -/
CategoryTheory.Limits.limitOfTerminal : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} J] →
        (F : CategoryTheory.Functor J C) →
          [inst_2 : CategoryTheory.Limits.HasTerminal J] →
            [inst_3 : ∀ (i j : J) (f : i ⟶ j), CategoryTheory.IsIso (F.map f)] →
              CategoryTheory.Limits.limit F ≅ F.obj (⊤_ J)
-- Std.Http.Data.URI.Basic
Std.Http.instBEqURI.beq : Std.Http.URI → Std.Http.URI → Bool
-- Mathlib.MeasureTheory.Integral.Lebesgue.Map
MeasureTheory.setLIntegral_subtype : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α},
  MeasurableSet s →
    ∀ (t : Set ↑s) (f : α → ENNReal),
      ∫⁻ (x : ↑s) in t, f ↑x ∂MeasureTheory.Measure.comap Subtype.val μ = ∫⁻ (x : α) in Subtype.val '' t, f x ∂μ
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.IsBridge.notMem_edges_of_isCycle : ∀ {V : Type u} {G : SimpleGraph V} {e : Sym2 V} {u : V} {p : G.Walk u u}, G.IsBridge e → p.IsCycle → e ∉ p.edges
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.IsAddFundamentalDomain.setLIntegral_eq_tsum' : ∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α] {s : Set α}
  {μ : MeasureTheory.Measure α} [MeasurableConstVAdd G α] [MeasureTheory.VAddInvariantMeasure G α μ] [Countable G],
  MeasureTheory.IsAddFundamentalDomain G s μ →
    ∀ (f : α → ENNReal) (t : Set α), ∫⁻ (x : α) in t, f x ∂μ = ∑' (g : G), ∫⁻ (x : α) in (g +ᵥ t) ∩ s, f (-g +ᵥ x) ∂μ
-- Std.Do.WP.Basic
Std.Do.EStateM.instWP : {ε σ : Type u_1} → Std.Do.WP (EStateM ε σ) (Std.Do.PostShape.except ε (Std.Do.PostShape.arg σ Std.Do.PostShape.pure))
-- Mathlib.Algebra.Group.Conj
conj_zpow : ∀ {α : Type u} [inst : Group α] {i : ℤ} {a b : α}, (a * b * a⁻¹) ^ i = a * b ^ i * a⁻¹
-- Mathlib.Algebra.Order.Field.Power
/-- Bernoulli's inequality reformulated to estimate `(n : α)`.  -/
Nat.cast_le_pow_sub_div_sub : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {a : α},
  1 < a → ∀ (n : ℕ), ↑n ≤ (a ^ n - 1) / (a - 1)
-- Mathlib.Analysis.Distribution.SchwartzSpace.Fourier
SchwartzMap.norm_fourier_Lp_top_leq_toLp_one : ∀ {V : Type u_3} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : FiniteDimensional ℝ V]
  [inst_3 : MeasurableSpace V] [inst_4 : BorelSpace V] {F : Type u_4} [inst_5 : NormedAddCommGroup F]
  [inst_6 : NormedSpace ℂ F] (f : SchwartzMap V F),
  ‖(FourierTransform.fourier f).toLp ⊤ MeasureTheory.volume‖ ≤ ‖f.toLp 1 MeasureTheory.volume‖
-- Mathlib.Tactic.TacticAnalysis
/-- A dummy option for testing the tactic analysis framework  -/
linter.tacticAnalysis.dummy : Lean.Option Bool
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.Indep.not_dep : ∀ {α : Type u_1} {M : Matroid α} {I : Set α}, M.Indep I → ¬M.Dep I
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubMulAction.instSMulSubtypeMem.eq_1 : ∀ {R : Type u} {M : Type v} [inst : SMul R M] (p : SubMulAction R M),
  p.instSMulSubtypeMem = { smul := fun c x => ⟨c • ↑x, ⋯⟩ }
-- Mathlib.Algebra.Group.Units.Defs
/-- `neg` is the left additive inverse of `val` in the base `AddMonoid`.  -/
AddUnits.neg_val : ∀ {α : Type u} [inst : AddMonoid α] (self : AddUnits α), self.neg + ↑self = 0
-- Lean.Elab.Tactic.Basic
/-- Check if any messages in the list are errors.  -/
Lean.Elab.Tactic.hasErrorMessages : List Lean.Message → Bool
-- Init.Data.UInt.Bitwise
USize.shiftLeft_zero : ∀ {a : USize}, a <<< 0 = a
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
CategoryTheory.Functor.PullbackObjObj.mk.injEq : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  {G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)} {X₁ Y₁ : C₁} {f₁ : X₁ ⟶ Y₁} {X₃ Y₃ : C₃}
  {f₃ : X₃ ⟶ Y₃} (pt : C₂) (fst : pt ⟶ (G.obj (Opposite.op X₁)).obj X₃) (snd : pt ⟶ (G.obj (Opposite.op Y₁)).obj Y₃)
  (isPullback : CategoryTheory.IsPullback fst snd ((G.obj (Opposite.op X₁)).map f₃) ((G.map f₁.op).app Y₃))
  (π : (G.obj (Opposite.op Y₁)).obj X₃ ⟶ pt)
  (π_fst :
    autoParam (CategoryTheory.CategoryStruct.comp π fst = (G.map f₁.op).app X₃)
      CategoryTheory.Functor.PullbackObjObj.π_fst._autoParam)
  (π_snd :
    autoParam (CategoryTheory.CategoryStruct.comp π snd = (G.obj (Opposite.op Y₁)).map f₃)
      CategoryTheory.Functor.PullbackObjObj.π_snd._autoParam)
  (pt_1 : C₂) (fst_1 : pt_1 ⟶ (G.obj (Opposite.op X₁)).obj X₃) (snd_1 : pt_1 ⟶ (G.obj (Opposite.op Y₁)).obj Y₃)
  (isPullback_1 : CategoryTheory.IsPullback fst_1 snd_1 ((G.obj (Opposite.op X₁)).map f₃) ((G.map f₁.op).app Y₃))
  (π_1 : (G.obj (Opposite.op Y₁)).obj X₃ ⟶ pt_1)
  (π_fst_1 :
    autoParam (CategoryTheory.CategoryStruct.comp π_1 fst_1 = (G.map f₁.op).app X₃)
      CategoryTheory.Functor.PullbackObjObj.π_fst._autoParam)
  (π_snd_1 :
    autoParam (CategoryTheory.CategoryStruct.comp π_1 snd_1 = (G.obj (Opposite.op Y₁)).map f₃)
      CategoryTheory.Functor.PullbackObjObj.π_snd._autoParam),
  ({ pt := pt, fst := fst, snd := snd, isPullback := isPullback, π := π, π_fst := π_fst, π_snd := π_snd } =
      { pt := pt_1, fst := fst_1, snd := snd_1, isPullback := isPullback_1, π := π_1, π_fst := π_fst_1,
        π_snd := π_snd_1 }) =
    (pt = pt_1 ∧ fst ≍ fst_1 ∧ snd ≍ snd_1 ∧ π ≍ π_1)
-- Mathlib.CategoryTheory.Idempotents.Karoubi
CategoryTheory.Idempotents.Karoubi.ext : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P Q : CategoryTheory.Idempotents.Karoubi C}
  (h_X : P.X = Q.X),
  CategoryTheory.CategoryStruct.comp P.p (CategoryTheory.eqToHom h_X) =
      CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h_X) Q.p →
    P = Q
-- Mathlib.Topology.Compactification.StoneCech
ultrafilter_comap_pure_nhds : ∀ {α : Type u} (b : Ultrafilter α), Filter.comap pure (nhds b) ≤ ↑b
-- Mathlib.Algebra.Homology.ShortComplex.Basic
/-- the right commutative square of a morphism in `ShortComplex`  -/
CategoryTheory.ShortComplex.Hom.comm₂₃ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (self : S₁.Hom S₂),
  CategoryTheory.CategoryStruct.comp self.τ₂ S₂.g = CategoryTheory.CategoryStruct.comp S₁.g self.τ₃
-- Mathlib.Algebra.MonoidAlgebra.Support
MonoidAlgebra.support_coeff_mul_subset : ∀ {k : Type u₁} {G : Type u₂} [inst : Semiring k] [inst_1 : Mul G] [inst_2 : DecidableEq G] (x y : MonoidAlgebra k G),
  (x * y).coeff.support ⊆ x.coeff.support * y.coeff.support
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.map_equiv_eq_comap_symm : ∀ {N : Type u_2} [inst : AddZeroClass N] {M : Type u_5} [inst_1 : AddZeroClass M] (f : M ≃+ N) (K : AddSubmonoid M),
  AddSubmonoid.map f K = AddSubmonoid.comap f.symm K
-- Mathlib.Order.Category.PartOrdEmb
PartOrdEmb.hom_id : ∀ {X : PartOrdEmb}, PartOrdEmb.Hom.hom (CategoryTheory.CategoryStruct.id X) = RelEmbedding.refl fun x1 x2 => x1 ≤ x2
-- Lean.Meta.Tactic.Grind.Intro
/-- Returns `true` if `e` is marked with the `alreadyNorm` gadget.
See `alreadyNorm` documentation for additional details
 -/
_private.Lean.Meta.Tactic.Grind.Intro.0.Lean.Meta.Grind.isAlreadyNorm? : Lean.Expr → Option Lean.Expr
-- Mathlib.Combinatorics.Enumerative.Partition.Basic
Nat.Partition.partitionWithPartEquiv_apply_parts : ∀ {n a : ℕ} (ha1 : 1 ≤ a) (ha : a ≤ n) (p : { p // a ∈ p.parts }),
  ((Nat.Partition.partitionWithPartEquiv ha1 ha) p).parts = (↑p).parts.erase a
-- Mathlib.Analysis.Normed.Lp.PiLp
_private.Mathlib.Analysis.Normed.Lp.PiLp.0.PiLp.uniformity_aux : ∀ (p : ENNReal) {ι : Type u_2} (β : ι → Type u_4) [inst : Fact (1 ≤ p)] [inst_1 : (i : ι) → PseudoEMetricSpace (β i)]
  [inst_2 : Fintype ι], uniformity (PiLp p β) = uniformity (WithLp p ((i : ι) → β i))
-- Mathlib.Computability.RegularExpressions
_private.Mathlib.Computability.RegularExpressions.0.RegularExpression.matches'.match_1.eq_1 : ∀ {α : Type u_1} (motive : RegularExpression α → Sort u_2) (h_1 : Unit → motive RegularExpression.zero)
  (h_2 : Unit → motive RegularExpression.epsilon) (h_3 : (a : α) → motive (RegularExpression.char a))
  (h_4 : (P Q : RegularExpression α) → motive (P.plus Q)) (h_5 : (P Q : RegularExpression α) → motive (P.comp Q))
  (h_6 : (P : RegularExpression α) → motive P.star),
  (match RegularExpression.zero with
    | RegularExpression.zero => h_1 ()
    | RegularExpression.epsilon => h_2 ()
    | RegularExpression.char a => h_3 a
    | P.plus Q => h_4 P Q
    | P.comp Q => h_5 P Q
    | P.star => h_6 P) =
    h_1 ()
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
WithBot.isGLB_sInf' : ∀ {β : Type u_5} [inst : ConditionallyCompleteLattice β] {s : Set (WithBot β)}, s.Nonempty → IsGLB s (sInf s)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.diff_left : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  {t₃ : Std.DTreeMap.Raw α β cmp}, t₁.WF → t₂.WF → t₃.WF → t₁.Equiv t₂ → (t₁ \ t₃).Equiv (t₂ \ t₃)
-- Init.Prelude
Nat.modCore_lt : ∀ {x y : ℕ}, 0 < y → x.modCore y < y
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
/-- the first "projection" from the (pre)path object  -/
HomotopicalAlgebra.PrepathObject.p₀ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → {A : C} → (self : HomotopicalAlgebra.PrepathObject A) → self.P ⟶ A
-- Mathlib.Data.Fin.Fin2
/-- `insertPerm a` is a permutation of `Fin2 n` with the following properties:
* `insertPerm a i = i+1` if `i < a`
* `insertPerm a a = 0`
* `insertPerm a i = i` if `i > a`  -/
Fin2.insertPerm : {n : ℕ} → Fin2 n → Fin2 n → Fin2 n
-- Mathlib.Algebra.MvPolynomial.Supported
MvPolynomial.mem_supported : ∀ {σ : Type u_1} {R : Type u} [inst : CommSemiring R] {p : MvPolynomial σ R} {s : Set σ},
  p ∈ MvPolynomial.supported R s ↔ ↑p.vars ⊆ s
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
IntervalIntegrable.sub : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] {a b : ℝ} {μ : MeasureTheory.Measure ℝ} {f g : ℝ → E},
  IntervalIntegrable f μ a b → IntervalIntegrable g μ a b → IntervalIntegrable (fun x => f x - g x) μ a b
-- Mathlib.Analysis.CStarAlgebra.CompletelyPositiveMap
/-- A linear map `φ : A₁ →ₗ[ℂ] A₂`  is called *completely positive (CP)* if
`CStarMatrix.mapₗ (Fin k) (Fin k) φ` (i.e. applying `φ` to all entries of a k × k matrix) is also
positive for every `k ∈ ℕ`.

Note that `Fin k` here is hardcoded to avoid having to quantify over types and introduce a new
universe parameter. See `CompletelyPositiveMap.map_cstarMatrix_nonneg` for a version of the
property that holds for matrices indexed by any finite type.
 -/
CompletelyPositiveMapClass : (F : Type u_1) →
  (A₁ : Type u_2) →
    (A₂ : Type u_3) →
      [inst : NonUnitalCStarAlgebra A₁] →
        [inst_1 : NonUnitalCStarAlgebra A₂] →
          [inst_2 : PartialOrder A₁] →
            [inst_3 : PartialOrder A₂] → [StarOrderedRing A₁] → [StarOrderedRing A₂] → [FunLike F A₁ A₂] → Prop
-- Mathlib.Algebra.Group.Units.Defs
isAddUnit_zero : ∀ {M : Type u_1} [inst : AddMonoid M], IsAddUnit 0
-- Mathlib.CategoryTheory.MorphismProperty.FunctorCategory
CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeFunctorFunctorCategoryOfHasPullbacks : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W : CategoryTheory.MorphismProperty C}
  [W.IsStableUnderBaseChange] (J : Type u'') [inst_2 : CategoryTheory.Category.{v'', u''} J]
  [CategoryTheory.Limits.HasPullbacks C], (W.functorCategory J).IsStableUnderBaseChange
-- Lean.Data.Lsp.Basic
Lean.Lsp.instToJsonMarkupKind : Lean.ToJson Lean.Lsp.MarkupKind
-- Mathlib.CategoryTheory.Sites.EpiMono
/-- The class of locally surjective morphisms of sheaves, see `Sheaf.IsLocallySurjective`.  -/
CategoryTheory.Sheaf.locallySurjective : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      (A : Type u') →
        [inst_1 : CategoryTheory.Category.{v', u'} A] →
          {FA : A → A → Type u_1} →
            {CA : A → Type w} →
              [inst_2 : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] →
                [CategoryTheory.ConcreteCategory A FA] → CategoryTheory.MorphismProperty (CategoryTheory.Sheaf J A)
-- Mathlib.CategoryTheory.Bicategory.Extension
CategoryTheory.Bicategory.LeftLift.whisker_unit : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a}
  (t : CategoryTheory.Bicategory.LeftLift f g) {x : B} (h : x ⟶ c),
  (t.whisker h).unit =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft h t.unit)
      (CategoryTheory.Bicategory.associator h t.lift f).inv
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.Rel.below.triangle : ∀ {B : Type u} [inst : Quiver B]
  {motive :
    {a b : CategoryTheory.FreeBicategory B} →
      {f g : a ⟶ b} →
        (a_1 a_2 : CategoryTheory.FreeBicategory.Hom₂ f g) → CategoryTheory.FreeBicategory.Rel a_1 a_2 → Prop}
  {a b c : B} (f : CategoryTheory.FreeBicategory.Hom a b) (g : CategoryTheory.FreeBicategory.Hom b c),
  CategoryTheory.FreeBicategory.Rel.below ⋯
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.colimitsOfShape_le_of_final : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) {J : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} J] {J' : Type u_2} [inst_2 : CategoryTheory.Category.{v_2, u_2} J']
  (F : CategoryTheory.Functor J J') [F.Final], W.colimitsOfShape J' ≤ W.colimitsOfShape J
-- Mathlib.FieldTheory.Finite.Basic
FiniteField.frobeniusAlgEquiv_apply : ∀ (K : Type u_1) (R : Type u_2) [inst : Field K] [inst_1 : Fintype K] [inst_2 : CommRing R] [inst_3 : Algebra K R]
  (p : ℕ) [inst_4 : ExpChar R p] [inst_5 : PerfectRing R p] (a : R),
  (FiniteField.frobeniusAlgEquiv K R p) a = a ^ Fintype.card K
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.hom_whiskerRight : ∀ {k : Type u} {G : Type v} [inst : CommRing k] [inst_1 : Monoid G] {X₁ X₂ Y : Rep.{u, u, v} k G} (f : X₁ ⟶ X₂),
  Rep.Hom.hom (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Y) =
    Representation.IntertwiningMap.rTensor Y.ρ (Rep.Hom.hom f)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
IsRightCancelMul.mulRightReflectLE_of_mulRightReflectLT : ∀ (N : Type u_2) [inst : Mul N] [IsRightCancelMul N] [inst_2 : PartialOrder N] [MulRightReflectLT N],
  MulRightReflectLE N
-- Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
/-- The exponents that appear in the unique decomposition of a unit as the product of
a root of unity and powers of the units of the fundamental system `fundSystem` (see
`exist_unique_eq_mul_prod`) are given by the representation of the unit on `basisModTorsion`.  -/
NumberField.Units.fun_eq_repr : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] {x ζ : (NumberField.RingOfIntegers K)ˣ}
  {f : Fin (NumberField.Units.rank K) → ℤ},
  ζ ∈ NumberField.Units.torsion K →
    x = ζ * ∏ i, NumberField.Units.fundSystem K i ^ f i →
      f = ⇑((NumberField.Units.basisModTorsion K).repr (Additive.ofMul ↑x))
-- Mathlib.CategoryTheory.Equivalence
/-- Equivalence of categories is transitive.  -/
CategoryTheory.Equivalence.trans : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {E : Type u₃} → [inst_2 : CategoryTheory.Category.{v₃, u₃} E] → (C ≌ D) → (D ≌ E) → (C ≌ E)
-- Mathlib.Analysis.Normed.Group.Seminorm
AddGroupSeminorm.instAddCommMonoid : {E : Type u_3} → [inst : AddGroup E] → AddCommMonoid (AddGroupSeminorm E)
-- Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
HurwitzZeta.completedHurwitzZetaOdd.eq_1 : ∀ (a : UnitAddCircle) (s : ℂ),
  HurwitzZeta.completedHurwitzZetaOdd a s = (HurwitzZeta.hurwitzOddFEPair a).Λ ((s + 1) / 2) / 2
-- Mathlib.CategoryTheory.Galois.Action
CategoryTheory.PreGaloisCategory.functorToAction_comp_forget₂_eq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (F : CategoryTheory.Functor C FintypeCat),
  (CategoryTheory.PreGaloisCategory.functorToAction F).comp
      (CategoryTheory.forget₂ (Action FintypeCat (CategoryTheory.Aut F)) FintypeCat) =
    F
-- Init.Tactics
/-- The `omega` tactic, for resolving integer and natural linear arithmetic problems.

It is not yet a full decision procedure (no "dark" or "grey" shadows),
but should be effective on many problems.

We handle hypotheses of the form `x = y`, `x < y`, `x ≤ y`, and `k ∣ x` for `x y` in `Nat` or `Int`
(and `k` a literal), along with negations of these statements.

We decompose the sides of the inequalities as linear combinations of atoms.

If we encounter `x / k` or `x % k` for literal integers `k` we introduce new auxiliary variables
and the relevant inequalities.

On the first pass, we do not perform case splits on natural subtraction.
If `omega` fails, we recursively perform a case split on
a natural subtraction appearing in a hypothesis, and try again.

The options
```
omega +splitDisjunctions +splitNatSub +splitNatAbs +splitMinMax
```
can be used to:
* `splitDisjunctions`: split any disjunctions found in the context,
  if the problem is not otherwise solvable.
* `splitNatSub`: for each appearance of `((a - b : Nat) : Int)`, split on `a ≤ b` if necessary.
* `splitNatAbs`: for each appearance of `Int.natAbs a`, split on `0 ≤ a` if necessary.
* `splitMinMax`: for each occurrence of `min a b`, split on `min a b = a ∨ min a b = b`
Currently, all of these are on by default.
 -/
Lean.Parser.Tactic.omega : Lean.ParserDescr
-- Mathlib.Geometry.Manifold.Immersion
/-- If `f` is an immersion at `x` and `g = f` on some neighbourhood of `x`,
then `g` is an immersion at `x`.  -/
Manifold.IsImmersionAt.congr_of_eventuallyEq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup E''] [inst_4 : NormedSpace 𝕜 E''] {H : Type u_7}
  [inst_5 : TopologicalSpace H] {G : Type u_9} [inst_6 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H M]
  {N : Type u_13} [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n : WithTop ℕ∞} {f g : M → N} {x : M},
  Manifold.IsImmersionAt I J n f x → f =ᶠ[nhds x] g → Manifold.IsImmersionAt I J n g x
-- Mathlib.RingTheory.GradedAlgebra.Basic
GradedRing.mem_support_iff : ∀ {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [inst : DecidableEq ι] [inst_1 : AddMonoid ι] [inst_2 : Semiring A]
  [inst_3 : SetLike σ A] [inst_4 : AddSubmonoidClass σ A] (𝒜 : ι → σ) [inst_5 : GradedRing 𝒜]
  [inst_6 : (i : ι) → (x : ↥(𝒜 i)) → Decidable (x ≠ 0)] (r : A) (i : ι),
  i ∈ DFinsupp.support ((DirectSum.decompose 𝒜) r) ↔ (GradedRing.proj 𝒜 i) r ≠ 0
-- Mathlib.NumberTheory.Harmonic.ZetaAsymp
log_riemannZeta_eq_neg_log_sub_add_ofReal : ∀ {s : ℝ}, s > 1 → Real.log (riemannZeta ↑s).re = -Real.log (s - 1) + Real.log (riemannZeta₁ ↑s).re
-- Init.Data.Order.Ord
/-- Transitivity of `cmp`, expressed via `Ordering.isLE`.  -/
Std.TransCmp.isLE_trans : ∀ {α : Type u} {cmp : α → α → Ordering} [self : Std.TransCmp cmp] {a b c : α},
  (cmp a b).isLE = true → (cmp b c).isLE = true → (cmp a c).isLE = true
-- Mathlib.Topology.Algebra.PontryaginDual
PontryaginDual.instCommGroup : {A : Type u_1} → [inst : Monoid A] → [inst_1 : TopologicalSpace A] → CommGroup (PontryaginDual A)
-- Mathlib.Topology.Sheaves.SheafCondition.Sites
coverPreserving_opens_map : ∀ {X Y : TopCat} (f : X ⟶ Y),
  CategoryTheory.CoverPreserving (Opens.grothendieckTopology ↑Y) (Opens.grothendieckTopology ↑X)
    (TopologicalSpace.Opens.map f)
-- Mathlib.RingTheory.TensorProduct.Basic
Algebra.TensorProduct.toLinearMap_includeLeft : ∀ {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : Semiring B] [inst_4 : Algebra R B] [inst_5 : CommSemiring S] [inst_6 : Algebra S A]
  [inst_7 : SMulCommClass R S A],
  Algebra.TensorProduct.includeLeft.toLinearMap = (TensorProduct.AlgebraTensorModule.mk R S A B).flip 1
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.ofCoeff_injective : ∀ {k : Type u_1} {G : Type u_2} [inst : AddMonoid k], Function.Injective SkewMonoidAlgebra.ofCoeff