mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
CategoryTheory.Limits.Cofork.op_ι : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {f g : X ⟶ Y}
  (c : CategoryTheory.Limits.Cofork f g), c.op.ι = c.π.op
-- Mathlib.Algebra.Group.Subsemigroup.Operations
MulHom.subsemigroupMap_surjective : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] (f : M →ₙ* N) (M' : Subsemigroup M),
  Function.Surjective ⇑(f.subsemigroupMap M')
-- Lean.Data.Lsp.Basic
Lean.Lsp.ResolveSupport.mk : Array String → Lean.Lsp.ResolveSupport
-- Mathlib.Data.List.SplitBy
List.head_head_splitBy : ∀ {α : Type u_1} (r : α → α → Bool) {l : List α} (hn : l ≠ []), ((List.splitBy r l).head ⋯).head ⋯ = l.head hn
-- Init.Data.List.ToArray
_private.Init.Data.List.ToArray.0.List.findM?.match_1.splitter : {α : Type} →
  (motive : List α → Sort u_1) →
    (x : List α) → (Unit → motive []) → ((a : α) → (as : List α) → motive (a :: as)) → motive x
-- Mathlib.NumberTheory.ModularForms.QExpansion
UpperHalfPlane.qExpansionFormalMultilinearSeries.eq_1 : ∀ {F : Type u_1} [inst : FunLike F UpperHalfPlane ℂ] (h : ℝ) (f : F),
  UpperHalfPlane.qExpansionFormalMultilinearSeries h f =
    FormalMultilinearSeries.ofScalars ℂ fun m => (PowerSeries.coeff m) (UpperHalfPlane.qExpansion h ⇑f)
-- Mathlib.Topology.ContinuousMap.CocompactMap
CocompactMap.ext : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f g : CocompactMap α β},
  (∀ (x : α), f x = g x) → f = g
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Polynomial.Chebyshev.one_lt_eval_T_real : ∀ {n : ℤ}, n ≠ 0 → ∀ {x : ℝ}, 1 < x → 1 < Polynomial.eval x (Polynomial.Chebyshev.T ℝ n)
-- Mathlib.Combinatorics.Hypergraph.Basic
Hypergraph.Adj.eq_1 : ∀ {α : Type u_1} (H : Hypergraph α) (x y : α), H.Adj x y = ∃ e ∈ H.edgeSet, x ∈ e ∧ y ∈ e
-- Mathlib.Order.Bounds.Basic
exists_glb_Ioi : ∀ {γ : Type u_3} [inst : LinearOrder γ] (i : γ), ∃ j, IsGLB (Set.Ioi i) j
-- Init.Data.Vector.Lemmas
Vector.foldr_append : ∀ {α : Type u_1} {β : Type u_2} {n k : ℕ} {f : α → β → β} {b : β} {xs : Vector α n} {ys : Vector α k},
  Vector.foldr f b (xs ++ ys) = Vector.foldr f (Vector.foldr f b ys) xs
-- Mathlib.RingTheory.Bialgebra.Equiv
BialgEquiv.toCoalgEquiv_toCoalgHom : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : CoalgebraStruct R A] [inst_6 : CoalgebraStruct R B]
  (e : A ≃ₐc[R] B), ↑e = ↑↑e
-- Mathlib.RingTheory.SimpleModule.WedderburnArtin
/-- The **Wedderburn–Artin Theorem**, algebra form: a semisimple algebra is isomorphic to a
product of matrix algebras over division algebras.  -/
IsSemisimpleRing.exists_algEquiv_pi_matrix_divisionRing : ∀ (R₀ : Type u_1) (R : Type u) [inst : CommSemiring R₀] [inst_1 : Ring R] [inst_2 : Algebra R₀ R] [IsSemisimpleRing R],
  ∃ n D d x x_1, (∀ (i : Fin n), NeZero (d i)) ∧ Nonempty (R ≃ₐ[R₀] (i : Fin n) → Matrix (Fin (d i)) (Fin (d i)) (D i))
-- Mathlib.Order.Filter.Tendsto
Filter.tendsto_id : ∀ {α : Type u_1} {x : Filter α}, Filter.Tendsto id x x
-- Mathlib.Algebra.Order.Floor.Ring
Int.floor_ofNat_add : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] [IsOrderedRing R] (n : ℕ)
  [inst_4 : n.AtLeastTwo] (a : R), ⌊OfNat.ofNat n + a⌋ = OfNat.ofNat n + ⌊a⌋
-- Mathlib.Tactic.Ring.Compare
/-- Prove goals of the form `A < B` in an ordered commutative semiring, if the ring-normal forms of
`A` and `B` differ by a positive (additive) constant.  -/
Mathlib.Tactic.Ring.proveLT : Lean.MVarId → Lean.MetaM Unit
-- Mathlib.CategoryTheory.Bicategory.CatEnriched
CategoryTheory.CatEnrichedOrdinary.Hom.base_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.EnrichedOrdinaryCategory CategoryTheory.Cat C] {X Y : CategoryTheory.CatEnrichedOrdinary C}
  {f g h : X ⟶ Y} (α : f ⟶ g) (β : g ⟶ h),
  CategoryTheory.CatEnrichedOrdinary.Hom.base (CategoryTheory.CategoryStruct.comp α β) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CatEnrichedOrdinary.Hom.base α)
      (CategoryTheory.CatEnrichedOrdinary.Hom.base β)
-- Init.Prelude
/-- Locally modifies the reader monad's value while running an action.

During the inner action `x`, reading the value returns `f` applied to the original value. After
control returns from `x`, the reader monad's value is restored.
 -/
MonadWithReaderOf.withReader : {ρ : semiOutParam (Type u)} →
  {m : Type u → Type v} → [self : MonadWithReaderOf ρ m] → {α : Type u} → (ρ → ρ) → m α → m α
-- Init.Meta.Defs
_private.Init.Meta.Defs.0.Lean.Name.needsNoEscapeAsciiRest : String → ℕ → Bool
-- Mathlib.Analysis.Calculus.FDeriv.Prod
DifferentiableAt.fderiv_prodMk : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f₁ : E → F} {x : E} {f₂ : E → G},
  DifferentiableAt 𝕜 f₁ x →
    DifferentiableAt 𝕜 f₂ x → fderiv 𝕜 (fun x => (f₁ x, f₂ x)) x = (fderiv 𝕜 f₁ x).prod (fderiv 𝕜 f₂ x)
-- Mathlib.CategoryTheory.Limits.Fubini
CategoryTheory.Limits.DiagramOfCones.mk.injEq : ∀ {J : Type u_1} {K : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} K] {C : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  {F : CategoryTheory.Functor J (CategoryTheory.Functor K C)} (obj : (j : J) → CategoryTheory.Limits.Cone (F.obj j))
  (map : {j j' : J} → (f : j ⟶ j') → (CategoryTheory.Limits.Cone.postcompose (F.map f)).obj (obj j) ⟶ obj j')
  (id :
    autoParam
      (∀ (j : J),
        (map (CategoryTheory.CategoryStruct.id j)).hom =
          CategoryTheory.CategoryStruct.id
            ((CategoryTheory.Limits.Cone.postcompose (F.map (CategoryTheory.CategoryStruct.id j))).obj (obj j)).pt)
      CategoryTheory.Limits.DiagramOfCones.id._autoParam)
  (comp :
    autoParam
      (∀ {j₁ j₂ j₃ : J} (f : j₁ ⟶ j₂) (g : j₂ ⟶ j₃),
        (map (CategoryTheory.CategoryStruct.comp f g)).hom = CategoryTheory.CategoryStruct.comp (map f).hom (map g).hom)
      CategoryTheory.Limits.DiagramOfCones.comp._autoParam)
  (obj_1 : (j : J) → CategoryTheory.Limits.Cone (F.obj j))
  (map_1 : {j j' : J} → (f : j ⟶ j') → (CategoryTheory.Limits.Cone.postcompose (F.map f)).obj (obj_1 j) ⟶ obj_1 j')
  (id_1 :
    autoParam
      (∀ (j : J),
        (map_1 (CategoryTheory.CategoryStruct.id j)).hom =
          CategoryTheory.CategoryStruct.id
            ((CategoryTheory.Limits.Cone.postcompose (F.map (CategoryTheory.CategoryStruct.id j))).obj (obj_1 j)).pt)
      CategoryTheory.Limits.DiagramOfCones.id._autoParam)
  (comp_1 :
    autoParam
      (∀ {j₁ j₂ j₃ : J} (f : j₁ ⟶ j₂) (g : j₂ ⟶ j₃),
        (map_1 (CategoryTheory.CategoryStruct.comp f g)).hom =
          CategoryTheory.CategoryStruct.comp (map_1 f).hom (map_1 g).hom)
      CategoryTheory.Limits.DiagramOfCones.comp._autoParam),
  ({ obj := obj, map := map, id := id, comp := comp } = { obj := obj_1, map := map_1, id := id_1, comp := comp_1 }) =
    (obj = obj_1 ∧ map ≍ map_1)
-- Mathlib.Algebra.Group.Pi.Lemmas
Pi.monoidHom.eq_1 : @Pi.monoidHom = @MonoidHom.pi
-- Mathlib.Topology.MetricSpace.Polish
PolishSpace.instENNReal : PolishSpace ENNReal
-- Aesop.Rule
Aesop.instInhabitedLocalNormSimpRule : Inhabited Aesop.LocalNormSimpRule
-- Mathlib.MeasureTheory.Measure.Trim
MeasureTheory.measure_trim_toMeasurable_eq_zero : ∀ {α : Type u_1} {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {hm : m ≤ m0},
  (μ.trim hm) s = 0 → μ (MeasureTheory.toMeasurable (μ.trim hm) s) = 0
-- Mathlib.Analysis.Matrix.Order
/-- The preorder on matrices given by `A ≤ B := (B - A).PosSemidef`.  -/
Matrix.instPreOrder : {𝕜 : Type u_1} → {n : Type u_2} → [RCLike 𝕜] → Preorder (Matrix n n 𝕜)
-- Init.Data.List.Lex
List.le_trans' : ∀ {α : Type u_1} [inst : LT α] [Std.Asymm fun x1 x2 => x1 < x2] [Std.Trichotomous fun x1 x2 => x1 < x2]
  [Trans (fun x1 x2 => ¬x1 < x2) (fun x1 x2 => ¬x1 < x2) fun x1 x2 => ¬x1 < x2] {l₁ l₂ l₃ : List α},
  l₁ ≤ l₂ → l₂ ≤ l₃ → l₁ ≤ l₃
-- Mathlib.Order.Interval.Finset.Defs
/-- The finset $[a, b)$ of elements `x` such that `a ≤ x` and `x < b`. Basically `Set.Ico a b` as a
finset.  -/
Finset.Ico : {α : Type u_1} → [inst : Preorder α] → [LocallyFiniteOrder α] → α → α → Finset α
-- Mathlib.GroupTheory.QuotientGroup.Basic
QuotientAddGroup.quotientBot_symm_apply : ∀ {G : Type u} [inst : AddGroup G] (a : G), QuotientAddGroup.quotientBot.symm a = ↑a
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
HasProdLocallyUniformlyOn.tprod_eqOn : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : CommMonoid α] {f : ι → β → α} {g : β → α} {s : Set β}
  [inst_1 : UniformSpace α] [inst_2 : TopologicalSpace β] [T2Space α],
  HasProdLocallyUniformlyOn f g s → Set.EqOn (fun x => ∏' (i : ι), f i x) g s
-- Mathlib.MeasureTheory.Function.ConditionalLExpectation
MeasureTheory.lintegral_condLExp : ∀ {Ω : Type u_1} {mΩ₀ mΩ : MeasurableSpace Ω} (hm : mΩ ≤ mΩ₀) (P : MeasureTheory.Measure Ω)
  [hσ : MeasureTheory.SigmaFinite (P.trim hm)] (X : Ω → ENNReal), ∫⁻ (ω : Ω), P⁻[X | mΩ] ω ∂P = ∫⁻ (ω : Ω), X ω ∂P
-- Mathlib.Order.Defs.LinearOrder
/-- The minimum function is equivalent to the one you get from `maxOfLe`.  -/
LinearOrder.max_def : ∀ {α : Type u_2} [self : LinearOrder α] (a b : α), max a b = if a ≤ b then b else a
-- Mathlib.CategoryTheory.Abelian.Projective.Dimension
CategoryTheory.ShortComplex.ShortExact.hasProjectiveDimensionLT_X₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  {S : CategoryTheory.ShortComplex C},
  S.ShortExact →
    ∀ (n : ℕ),
      CategoryTheory.HasProjectiveDimensionLT S.X₂ n →
        CategoryTheory.HasProjectiveDimensionLT S.X₃ (n + 1) → CategoryTheory.HasProjectiveDimensionLT S.X₁ n
-- Std.Data.String.ToInt
String.Slice.toInt?_copy : ∀ {s : String.Slice}, s.copy.toInt? = s.toInt?
-- Mathlib.NumberTheory.LSeries.ZMod
ZMod.completedLFunction.eq_1 : ∀ {N : ℕ} [inst : NeZero N] (Φ : ZMod N → ℂ) (s : ℂ),
  ZMod.completedLFunction Φ s =
    ↑N ^ (-s) * ∑ j, Φ j * HurwitzZeta.completedHurwitzZetaEven (ZMod.toAddCircle j) s +
      ↑N ^ (-s) * ∑ j, Φ j * HurwitzZeta.completedHurwitzZetaOdd (ZMod.toAddCircle j) s
-- Mathlib.Order.GaloisConnection.Basic
GaloisConnection.u_iInf₂ : ∀ {α : Type u} {β : Type v} {ι : Sort x} {κ : ι → Sort u_1} [inst : CompleteLattice α] [inst_1 : CompleteLattice β]
  {u : α → β} {l : β → α}, GaloisConnection l u → ∀ {f : (i : ι) → κ i → α}, u (⨅ i, ⨅ j, f i j) = ⨅ i, ⨅ j, u (f i j)
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.preimage_mul_const_Iic₀ : ∀ {G₀ : Type u_2} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [MulPosReflectLT G₀] {c : G₀} (a : G₀),
  0 < c → (fun x => x * c) ⁻¹' Set.Iic a = Set.Iic (a / c)
-- Mathlib.Computability.Ackermann
Nat.Partrec.Code.pappAck.eq_def : ∀ (x : ℕ),
  Nat.Partrec.Code.pappAck x =
    match x with
    | 0 => Nat.Partrec.Code.succ
    | n.succ => Nat.Partrec.Code.pappAck.step (Nat.Partrec.Code.pappAck n)
-- Mathlib.Algebra.Polynomial.Mirror
Polynomial.mirror_C : ∀ {R : Type u_1} [inst : Semiring R] (a : R), (Polynomial.C a).mirror = Polynomial.C a
-- Mathlib.Algebra.Module.Submodule.RestrictScalars
Submodule.restrictScalars_injective : ∀ (S : Type u_1) (R : Type u_2) (M : Type u_3) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Semiring S]
  [inst_3 : Module S M] [inst_4 : Module R M] [inst_5 : SMul S R] [inst_6 : IsScalarTower S R M],
  Function.Injective (Submodule.restrictScalars S)
-- Mathlib.Topology.Instances.EReal.Lemmas
EReal.limsup_add_le : ∀ {α : Type u_3} {f : Filter α} {u v : α → EReal},
  Filter.limsup u f ≠ ⊥ ∨ Filter.limsup v f ≠ ⊤ →
    Filter.limsup u f ≠ ⊤ ∨ Filter.limsup v f ≠ ⊥ → Filter.limsup (u + v) f ≤ Filter.limsup u f + Filter.limsup v f
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokensOptions.mk : Lean.Lsp.SemanticTokensLegend → Bool → Bool → Lean.Lsp.SemanticTokensOptions
-- Std.Data.String.ToNat
Nat.repr_injective : ∀ {m n : ℕ}, m.repr = n.repr → m = n
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.C_eq_S_sub_X_mul_S : ∀ (R : Type u_1) [inst : CommRing R] (n : ℤ),
  Polynomial.Chebyshev.C R n = 2 * Polynomial.Chebyshev.S R n - Polynomial.X * Polynomial.Chebyshev.S R (n - 1)
-- Mathlib.Topology.VectorBundle.Basic
Bundle.Trivialization.coe_symmₗ : ∀ {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [inst : Semiring R] [inst_1 : TopologicalSpace F]
  [inst_2 : TopologicalSpace B] [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_4 : AddCommMonoid F]
  [inst_5 : Module R F] [inst_6 : (x : B) → AddCommMonoid (E x)] [inst_7 : (x : B) → Module R (E x)]
  (e : Bundle.Trivialization F Bundle.TotalSpace.proj) [inst_8 : Bundle.Trivialization.IsLinear R e] {b : B},
  b ∈ e.baseSet → ⇑(Bundle.Trivialization.symmₗ R e b) = e.symm b
-- Init.Data.UInt.Bitwise
UInt8.shiftLeft_eq_shiftLeft_mod : ∀ (a b : UInt8), a <<< b = a <<< (b % 8)
-- Mathlib.AlgebraicGeometry.StructureSheaf
_private.Mathlib.AlgebraicGeometry.StructureSheaf.0.AlgebraicGeometry.StructureSheaf.localizationToStalk_stalkToFiberRingHom : ∀ {R M : Type u} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (x : ↑(AlgebraicGeometry.PrimeSpectrum.Top R)),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.StructureSheaf.localizationtoStalkₗ✝ R M x)
      (AlgebraicGeometry.StructureSheaf.stalkToLocalizationₗ✝ R M x) =
    CategoryTheory.CategoryStruct.id (ModuleCat.of R (LocalizedModule x.asIdeal.primeCompl M))
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
/-- Constructor for isomorphisms between multiforks.  -/
CategoryTheory.Limits.Multifork.ext : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.Limits.MulticospanShape} →
      {I : CategoryTheory.Limits.MulticospanIndex J C} →
        {t s : CategoryTheory.Limits.Multifork I} →
          (e : t.pt ≅ s.pt) →
            autoParam (∀ (i : J.L), CategoryTheory.CategoryStruct.comp e.hom (s.ι i) = t.ι i)
                CategoryTheory.Limits.Multifork.ext._auto_1 →
              (t ≅ s)
-- Lean.Elab.Parallel
/-- Runs a list of MetaM computations in parallel and returns the first successful result
(by completion order, not list order).

If `cancel := true` (the default), cancels all remaining tasks after the first success.
 -/
Lean.Meta.MetaM.parFirst : {α : Type} → List (Lean.MetaM α) → optParam Bool true → Lean.MetaM α
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidHom.copy.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : MulOneClass α]
  [inst_3 : MulOneClass β] (f : α →*o β) (f' : α → β) (h : f' = ⇑f),
  f.copy f' h = { toFun := f', map_one' := ⋯, map_mul' := ⋯, monotone' := ⋯ }
-- Lean.Meta.Basic
Lean.Meta.liftMetaM : {m : Type → Type u_1} → {α : Type} → [MonadLiftT Lean.MetaM m] → Lean.MetaM α → m α
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.FoldingRangeKind.region.sizeOf_spec : sizeOf Lean.Lsp.FoldingRangeKind.region = 1
-- Mathlib.Data.Int.Cast.Lemmas
RingHom.eq_intCast' : ∀ {α : Type u_3} [inst : NonAssocRing α] (f : ℤ →+* α), f = Int.castRingHom α
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.map_comp : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] [inst_1 : Ring R] (v : Valuation R Γ₀)
  {S : Type u_3} [inst_2 : Ring S] {Λ₀ : Type u_4} [inst_3 : LinearOrderedCommGroupWithZero Λ₀] (w : Valuation S Λ₀)
  {T : Type u_5} [inst_4 : Ring T] (u : Valuation T Γ₀) (f : S →+* T) (g : R →+* S),
  WithVal.map v u (f.comp g) = (WithVal.map w u f).comp (WithVal.map v w g)
-- Init.Data.SInt.Basic
instLTInt32 : LT Int32
-- Mathlib.Probability.ProbabilityMassFunction.Basic
/-- Slightly stronger than `OuterMeasure.mono` having an intersection with `p.support`.  -/
PMF.toOuterMeasure_mono : ∀ {α : Type u_1} (p : PMF α) {s t : Set α}, s ∩ p.support ⊆ t → p.toOuterMeasure s ≤ p.toOuterMeasure t
-- Mathlib.Topology.MetricSpace.Defs
instMetricSpaceMultiplicative : {X : Type u_1} → [MetricSpace X] → MetricSpace (Multiplicative X)
-- Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
MeasureTheory.Measure.QuasiMeasurePreserving.image_zpow_ae_eq : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {e : α ≃ α},
  MeasureTheory.Measure.QuasiMeasurePreserving (⇑e) μ μ →
    MeasureTheory.Measure.QuasiMeasurePreserving (⇑e.symm) μ μ → ∀ (k : ℤ), ⇑e '' s =ᵐ[μ] s → ⇑(e ^ k) '' s =ᵐ[μ] s
-- Mathlib.NumberTheory.DirichletCharacter.Basic
DirichletCharacter.conductor_dvd_level : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] {n : ℕ} (χ : DirichletCharacter R n), χ.conductor ∣ n
-- Mathlib.GroupTheory.GroupAction.FixingSubgroup
fixingSubgroup_antitone : ∀ (M : Type u_1) (α : Type u_2) [inst : Group M] [inst_1 : MulAction M α], Antitone (fixingSubgroup M)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.instBEqPower.beq_spec : ∀ (x x_1 : Lean.Grind.CommRing.Power), (x == x_1) = (x.x == x_1.x && x.k == x_1.k)
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientGroup.leftRel_eq_top : ∀ {G : Type u_1} [inst : Group G] {N : Subgroup G}, QuotientGroup.leftRel N = ⊤ ↔ N = ⊤
-- Std.Data.Internal.List.Associative
Std.Internal.List.containsKey_of_getValue_eq_some : ∀ {α : Type u} [inst : BEq α] [LawfulBEq α] {β : Type v} {l : List ((_ : α) × β)} {a : α} {b : β},
  Std.Internal.List.getValue? a l = some b → Std.Internal.List.containsKey a l = true
-- Lean.Parser.Extra
Lean.Parser.withSetOptionValue.formatter : Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter
-- Mathlib.Logic.Encodable.Basic
_private.Mathlib.Logic.Encodable.Basic.0.Directed.sequence.match_1.splitter : {α : Type u_1} →
  (motive : Option α → Sort u_2) → (x : Option α) → (Unit → motive none) → ((a : α) → motive (some a)) → motive x
-- Init.Data.List.Monadic
List.allM_eq_not_anyM_not : ∀ {m : Type → Type u_1} {α : Type u_2} [inst : Monad m] [LawfulMonad m] {p : α → m Bool} {as : List α},
  List.allM p as = (fun x => !x) <$> List.anyM (fun x => (fun x => !x) <$> p x) as
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
_private.Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality.0.InnerProductGeometry.angle_le_angle_add_angle_of_norm_eq_one : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y z : V},
  ‖x‖ = 1 →
    ‖y‖ = 1 → ‖z‖ = 1 → InnerProductGeometry.angle x z ≤ InnerProductGeometry.angle x y + InnerProductGeometry.angle y z
-- Mathlib.SetTheory.Cardinal.Ordinal
Ordinal.card_omega0_opow : ∀ {a : Ordinal.{u_1}}, a ≠ 0 → (Ordinal.omega0 ^ a).card = max Cardinal.aleph0 a.card
-- Mathlib.Algebra.Lie.Basic
/-- The inverse function of an equivalence of Lie modules is a right inverse of the underlying
function.  -/
LieModuleEquiv.right_inv : ∀ {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : AddCommGroup M] [inst_3 : AddCommGroup N] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : LieRingModule L M] [inst_7 : LieRingModule L N] (self : M ≃ₗ⁅R,L⁆ N),
  Function.RightInverse self.invFun (↑self.toLieModuleHom).toFun
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.mem_extendScalars : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {F E : IntermediateField K L}
  (h : F ≤ E) {x : L}, x ∈ IntermediateField.extendScalars h ↔ x ∈ E
-- Batteries.Data.Vector.Basic
/-- Fold a function `f` over the list from the right, returning the vector of partial results.
 -/
Vector.scanr : {α : Type u_1} → {β : Type u_2} → {n : ℕ} → (α → β → β) → β → Vector α n → Vector β (n + 1)
-- Mathlib.CategoryTheory.MorphismProperty.LocalClosure
CategoryTheory.MorphismProperty.sourceLocalClosure.instIsLocalAtSource : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {K : CategoryTheory.Precoverage C}
  {P : CategoryTheory.MorphismProperty C}, (CategoryTheory.MorphismProperty.sourceLocalClosure K P).IsLocalAtSource K
-- Mathlib.Data.WSeq.Relation
Stream'.WSeq.mem_congr : ∀ {α : Type u} {s t : Stream'.WSeq α}, s ~ʷ t → ∀ (a : α), a ∈ s ↔ a ∈ t
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.throwTypeMismatchError : {α : Type} →
  Option Lean.MessageData →
    Lean.Expr →
      Lean.Expr → Lean.Expr → optParam (Option Lean.Expr) none → optParam (Option Lean.MessageData) none → Lean.MetaM α
-- Mathlib.Order.Filter.Germ.Basic
/-- Lift a function `β → γ` to a function `Germ l β → Germ l γ`.  -/
Filter.Germ.map : {α : Type u_1} → {β : Type u_2} → {γ : Type u_3} → {l : Filter α} → (β → γ) → l.Germ β → l.Germ γ
-- Mathlib.Algebra.Order.Group.DenselyOrdered
le_of_forall_pos_sub_le : ∀ {α : Type u_1} [inst : AddGroup α] [inst_1 : LinearOrder α] [AddLeftMono α] [DenselyOrdered α] {a b : α},
  (∀ (ε : α), 0 < ε → a - ε ≤ b) → a ≤ b
-- Mathlib.Data.Matrix.Basic
instIsStablyFiniteRingMulOpposite : ∀ (α : Type u_14) [inst : MulOne α] [inst_1 : AddCommMonoid α] [IsStablyFiniteRing α], IsStablyFiniteRing αᵐᵒᵖ
-- Mathlib.Order.SupClosed
supClosure_univ : ∀ {α : Type u_3} [inst : SemilatticeSup α], supClosure Set.univ = Set.univ
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.CoherenceHom.mk.injEq : ∀ (e : Lean.Expr) (src tgt : Mathlib.Tactic.BicategoryLike.Mor₁) (inst unfold e_1 : Lean.Expr)
  (src_1 tgt_1 : Mathlib.Tactic.BicategoryLike.Mor₁) (inst_1 unfold_1 : Lean.Expr),
  ({ e := e, src := src, tgt := tgt, inst := inst, unfold := unfold } =
      { e := e_1, src := src_1, tgt := tgt_1, inst := inst_1, unfold := unfold_1 }) =
    (e = e_1 ∧ src = src_1 ∧ tgt = tgt_1 ∧ inst = inst_1 ∧ unfold = unfold_1)
-- Mathlib.GroupTheory.Coset.Basic
QuotientGroup.quotientEquivSelf.eq_1 : ∀ (α : Type u_1) [inst : Group α],
  QuotientGroup.quotientEquivSelf α =
    { toFun := Quotient.lift id ⋯, invFun := QuotientGroup.mk, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.Computability.TuringMachine.ToPartrec
_private.Mathlib.Computability.TuringMachine.ToPartrec.0.Turing.PartrecToTM2.trNormal.match_1.eq_3 : ∀ (motive : Turing.ToPartrec.Code → Turing.PartrecToTM2.Cont' → Sort u_1) (k : Turing.PartrecToTM2.Cont')
  (h_1 : (k : Turing.PartrecToTM2.Cont') → motive Turing.ToPartrec.Code.zero' k)
  (h_2 : (k : Turing.PartrecToTM2.Cont') → motive Turing.ToPartrec.Code.succ k)
  (h_3 : (k : Turing.PartrecToTM2.Cont') → motive Turing.ToPartrec.Code.tail k)
  (h_4 : (f fs : Turing.ToPartrec.Code) → (k : Turing.PartrecToTM2.Cont') → motive (f.cons fs) k)
  (h_5 : (f g : Turing.ToPartrec.Code) → (k : Turing.PartrecToTM2.Cont') → motive (f.comp g) k)
  (h_6 : (f g : Turing.ToPartrec.Code) → (k : Turing.PartrecToTM2.Cont') → motive (f.case g) k)
  (h_7 : (f : Turing.ToPartrec.Code) → (k : Turing.PartrecToTM2.Cont') → motive f.fix k),
  (match Turing.ToPartrec.Code.tail, k with
    | Turing.ToPartrec.Code.zero', k => h_1 k
    | Turing.ToPartrec.Code.succ, k => h_2 k
    | Turing.ToPartrec.Code.tail, k => h_3 k
    | f.cons fs, k => h_4 f fs k
    | f.comp g, k => h_5 f g k
    | f.case g, k => h_6 f g k
    | f.fix, k => h_7 f k) =
    h_3 k
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.image_inv_Ioc : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] (a b : α),
  Inv.inv '' Set.Ioc a b = Set.Ico b⁻¹ a⁻¹
-- Mathlib.RingTheory.Spectrum.Prime.Polynomial
MvPolynomial.isOpenMap_comap_C : ∀ {R : Type u_2} [inst : CommRing R] {σ : Type u_1}, IsOpenMap (PrimeSpectrum.comap MvPolynomial.C)
-- Mathlib.GroupTheory.Index
Subgroup.index.eq_1 : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G), H.index = Nat.card (G ⧸ H)
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
WeierstrassCurve.map_ψ₂ : ∀ {R : Type r} {S : Type s} [inst : CommRing R] [inst_1 : CommRing S] (W : WeierstrassCurve R) (f : R →+* S),
  (W.map f).ψ₂ = Polynomial.map (Polynomial.mapRingHom f) W.ψ₂
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise
Finpartition.equitabilise_isEquipartition : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α} {m a b : ℕ} {P : Finpartition s}
  {h : a * m + b * (m + 1) = s.card}, (Finpartition.equitabilise h).IsEquipartition
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.coe_eq_zero : ∀ {α : Type u_2} [inst : Zero α] {s : Finset α}, ↑s = 0 ↔ s = 0