mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Asymptotics.Defs
/-- **Alias** of the forward direction of `Asymptotics.isBigO_neg_left`. -/
Asymptotics.IsBigO.of_neg_left : ∀ {α : Type u_1} {F : Type u_4} {E' : Type u_6} [inst : Norm F] [inst_1 : SeminormedAddCommGroup E'] {g : α → F}
  {f' : α → E'} {l : Filter α}, (fun x => -f' x) =O[l] g → f' =O[l] g
-- Mathlib.NumberTheory.NumberField.Basic
NumberField.RingOfIntegers.instIsScalarTower_1 : ∀ (K : Type u_4) (L : Type u_5) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L],
  IsScalarTower (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers L) L
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.cocyclesMk₂_eq : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) (x : ↥(groupCohomology.cocycles₂ A)),
  groupCohomology.cocyclesMk ((CategoryTheory.ConcreteCategory.hom (groupCohomology.cochainsIso₂ A).inv) ⇑x) ⋯ =
    (CategoryTheory.ConcreteCategory.hom (groupCohomology.isoCocycles₂ A).inv) x
-- Mathlib.NumberTheory.SiegelsLemma
_private.Mathlib.NumberTheory.SiegelsLemma.0.Int.Matrix.termN_1 : Lean.ParserDescr
-- Mathlib.Algebra.GCDMonoid.PUnit
PUnit.normalizedGCDMonoid : NormalizedGCDMonoid PUnit.{u_1 + 1}
-- Mathlib.RingTheory.Localization.Away.Basic
IsLocalization.Away.instMapRingHomPowersOfCoe : ∀ {A : Type u_5} [inst : CommSemiring A] {B : Type u_6} [inst_1 : CommSemiring B] (Bₚ : Type u_8)
  [inst_2 : CommSemiring Bₚ] [inst_3 : Algebra B Bₚ] {f : A →+* B} (a : A) [IsLocalization.Away (f a) Bₚ],
  IsLocalization (Submonoid.map f (Submonoid.powers a)) Bₚ
-- Std.Tactic.Do.Syntax
/-- If `true` (the default in grind mode), `vcgen` calls `Grind.processHypotheses` on
each emitted VC, internalising local hypotheses into the parent's E-graph so that
downstream grind steps share context. The tactic-level entry point disables this
when there is no `with` clause (no grind step will consume the E-graph anyway).
Ignored by `mvcgen`.
 -/
Lean.Elab.Tactic.Do.VCGen.Config.internalize : Lean.Elab.Tactic.Do.VCGen.Config → Bool
-- Mathlib.Analysis.Normed.Group.Basic
zero_lt_one_add_norm_sq' : ∀ {E : Type u_5} [inst : SeminormedGroup E] (x : E), 0 < 1 + ‖x‖ ^ 2
-- Mathlib.NumberTheory.Height.MvPolynomial
IsNonarchimedean.iSup_abv_linearMap_apply_le : ∀ {K : Type u_1} [inst : Field K] {ι : Type u_2} {ι' : Type u_3} [inst_1 : Fintype ι] [Finite ι']
  {v : AbsoluteValue K ℝ},
  IsNonarchimedean ⇑v → ∀ (A : ι' × ι → K) (x : ι → K), ⨆ j, v (∑ i, A (j, i) * x i) ≤ (⨆ ji, v (A ji)) * ⨆ i, v (x i)
-- Mathlib.RingTheory.Finiteness.Small
Module.Finite.small : ∀ (R : Type u_1) (M : Type u_2) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Small.{u, u_1} R]
  [Module.Finite R M], Small.{u, u_2} M
-- Lean.Meta.Match.Match
_private.Lean.Meta.Match.Match.0.Lean.Meta.Match.hasValPattern : Lean.Meta.Match.Problem → Bool
-- Mathlib.MeasureTheory.Integral.DominatedConvergence
/-- Lebesgue dominated convergence theorem for parametric interval integrals.  -/
intervalIntegral.hasSum_integral_of_dominated_convergence : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b : ℝ} {f : ℝ → E}
  {μ : MeasureTheory.Measure ℝ} {ι : Type u_3} [Countable ι] {F : ι → ℝ → E} (bound : ι → ℝ → ℝ),
  (∀ (n : ι), MeasureTheory.AEStronglyMeasurable (F n) (μ.restrict (Set.uIoc a b))) →
    (∀ (n : ι), ∀ᵐ (t : ℝ) ∂μ, t ∈ Set.uIoc a b → ‖F n t‖ ≤ bound n t) →
      (∀ᵐ (t : ℝ) ∂μ, t ∈ Set.uIoc a b → Summable fun n => bound n t) →
        IntervalIntegrable (fun t => ∑' (n : ι), bound n t) μ a b →
          (∀ᵐ (t : ℝ) ∂μ, t ∈ Set.uIoc a b → HasSum (fun n => F n t) (f t)) →
            HasSum (fun n => ∫ (t : ℝ) in a..b, F n t ∂μ) (∫ (t : ℝ) in a..b, f t ∂μ)
-- Mathlib.MeasureTheory.Function.UnifTight
MeasureTheory.UnifTight.exists_measurableSet_indicator : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup β] {f : ι → α → β} {p : ENNReal},
  MeasureTheory.UnifTight f p μ →
    ∀ {ε : ENNReal},
      ε ≠ 0 → ∃ s, MeasurableSet s ∧ μ s < ⊤ ∧ ∀ (i : ι), MeasureTheory.eLpNorm (sᶜ.indicator (f i)) p μ ≤ ε
-- Mathlib.Algebra.Lie.Derivation.Basic
/-- Alternate version of the general Leibniz rule for Lie derivatives.  -/
LieDerivation.iterate_apply_lie' : ∀ {R : Type u_1} {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  (D : LieDerivation R L L) (n : ℕ) (a b : L),
  (⇑D)^[n] ⁅a, b⁆ = ∑ i ∈ Finset.range (n + 1), n.choose i • ⁅(⇑D)^[i] a, (⇑D)^[n - i] b⁆
-- Lean.Compiler.InlineAttrs
/-- Changes the inlining behavior. This attribute comes in several variants:
- `@[inline]`: marks the definition to be inlined when it is appropriate.
- `@[inline_if_reduce]`: marks the definition to be inlined if an application of it after inlining
  and applying reduction isn't a `match` expression. This attribute can be used for inlining
  structurally recursive functions.
- `@[noinline]`: marks the definition to never be inlined.
- `@[always_inline]`: marks the definition to always be inlined.
- `@[macro_inline]`: marks the definition to always be inlined at the beginning of compilation.
  This makes it possible to define functions that evaluate some of their parameters lazily.
  Example:
  ```
  @[macro_inline]
  def test (x y : Nat) : Nat :=
    if x = 42 then x else y

  #eval test 42 (2^1000000000000) -- doesn't compute 2^1000000000000
  ```
  Only non-recursive functions may be marked `@[macro_inline]`.
 -/
Lean.Compiler.inlineAttrs : Lean.EnumAttributes Lean.Compiler.InlineAttributeKind
-- Mathlib.Topology.Algebra.TopologicallyNilpotent
/-- If `a` and `b` commute and `b` is topologically nilpotent,
then `a * b` is topologically nilpotent.  -/
IsTopologicallyNilpotent.mul_left_of_commute : ∀ {R : Type u_1} [inst : TopologicalSpace R] [inst_1 : Ring R] [IsLinearTopology R R] {a b : R},
  IsTopologicallyNilpotent b → Commute a b → IsTopologicallyNilpotent (a * b)
-- Mathlib.Combinatorics.SimpleGraph.Hamiltonian
/-- A Hamiltonian cycle visits every vertex.  -/
SimpleGraph.Walk.IsHamiltonianCycle.mem_support : ∀ {α : Type u_1} [inst : DecidableEq α] {G : SimpleGraph α} {a : α} {p : G.Walk a a},
  p.IsHamiltonianCycle → ∀ (b : α), b ∈ p.support
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
LinearMap.BilinForm.toMatrix_mul : ∀ {R₁ : Type u_1} {M₁ : Type u_2} [inst : CommSemiring R₁] [inst_1 : AddCommMonoid M₁] [inst_2 : Module R₁ M₁]
  {n : Type u_5} [inst_3 : Fintype n] [inst_4 : DecidableEq n] (b : Module.Basis n R₁ M₁)
  (B : LinearMap.BilinForm R₁ M₁) (M : Matrix n n R₁),
  (LinearMap.BilinForm.toMatrix b) B * M = (LinearMap.BilinForm.toMatrix b) (B.compRight ((Matrix.toLin b b) M))
-- Mathlib.Topology.Algebra.PontryaginDual
/-- `PontryaginDual` is a contravariant functor.  -/
PontryaginDual.map : {A : Type u_1} →
  {B : Type u_2} →
    [inst : Monoid A] →
      [inst_1 : Monoid B] →
        [inst_2 : TopologicalSpace A] →
          [inst_3 : TopologicalSpace B] → (A →ₜ* B) → PontryaginDual B →ₜ* PontryaginDual A
-- Mathlib.Data.Fin.SuccPred
Fin.predAbove_castSucc_of_lt : ∀ {n : ℕ} (p i : Fin n) (h : p < i), p.predAbove i.castSucc = i.castSucc.pred ⋯
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.coe_algebraMap_apply : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (S : IntermediateField K L)
  (x : K), ↑((algebraMap K ↥S) x) = (algebraMap K L) x
-- Mathlib.Topology.Order.LowerUpperTopology
Topology.IsUpper.isLowerSet_of_isClosed : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : TopologicalSpace α] [Topology.IsUpper α] {s : Set α},
  IsClosed s → IsLowerSet s
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
NonUnitalRingHom.coe_srangeRestrict : ∀ {R : Type u} {S : Type v} [inst : NonUnitalNonAssocSemiring R] {F : Type u_1} [inst_1 : FunLike F R S]
  [inst_2 : NonUnitalNonAssocSemiring S] [inst_3 : NonUnitalRingHomClass F R S] (f : F) (x : R),
  ↑((NonUnitalRingHom.srangeRestrict f) x) = f x
-- Batteries.Data.Fin.Coding
_private.Batteries.Data.Fin.Coding.0.Fin.encodeFun.match_1.eq_1 : ∀ {n : ℕ} (motive : (x : ℕ) → (Fin x → Fin n) → Sort u_1) (x : Fin 0 → Fin n) (h_1 : (x : Fin 0 → Fin n) → motive 0 x)
  (h_2 : (m : ℕ) → (f : Fin (m + 1) → Fin n) → motive m.succ f),
  (match 0, x with
    | 0, x => h_1 x
    | m.succ, f => h_2 m f) =
    h_1 x
-- Init.Data.Array.Lemmas
Array.map_reverse : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {xs : Array α}, Array.map f xs.reverse = (Array.map f xs).reverse
-- Mathlib.Order.WithBot
WithTop.untopD_lt_iff : ∀ {α : Type u_1} {a b : α} [inst : LT α] {x : WithTop α}, x ≠ ⊤ → (WithTop.untopD a x < b ↔ x < ↑b)
-- Mathlib.Algebra.Group.Equiv.Opposite
MonoidHom.toOpposite_apply : ∀ {M : Type u_3} {N : Type u_4} [inst : MulOneClass M] [inst_1 : MulOneClass N] (f : M →* N)
  (hf : ∀ (x y : M), Commute (f x) (f y)), ⇑(f.toOpposite hf) = MulOpposite.op ∘ ⇑f
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Real.arcsin_le_iff_le_sin' : ∀ {x y : ℝ}, y ∈ Set.Ico (-(Real.pi / 2)) (Real.pi / 2) → (Real.arcsin x ≤ y ↔ x ≤ Real.sin y)
-- Mathlib.Order.Hom.Basic
OrderHom.onDiag_coe : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] (f : α →o α →o β) (a : α),
  f.onDiag a = (f a) a
-- Mathlib.RingTheory.IsGaloisGroup.Basic
IsGaloisGroup.algebraMap_smulOfNormal : ∀ (G : Type u_1) [inst : Group G] (B : Type u_3) (C : Type u_4) [inst_1 : Semiring C] [inst_2 : MulSemiringAction G C]
  (N : Subgroup G) [inst_3 : CommSemiring B] [inst_4 : Algebra B C] [inst_5 : N.Normal]
  [inst_6 : IsGaloisGroup (↥N) B C] (g : G) (x : B), (algebraMap B C) (g • x) = g • (algebraMap B C) x
-- Mathlib.LinearAlgebra.Span.Defs
Submodule.span_range_eq_iSup : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {ι : Sort u_9}
  {v : ι → M}, Submodule.span R (Set.range v) = ⨆ i, R ∙ v i
-- Mathlib.CategoryTheory.Functor.Const
CategoryTheory.Functor.compConstIso_hom_app_app : ∀ (J : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} C]
  {D : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} D] (F : CategoryTheory.Functor C D) (X : C) (X_1 : J),
  ((CategoryTheory.Functor.compConstIso J F).hom.app X).app X_1 = CategoryTheory.CategoryStruct.id (F.obj X)
-- Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
MeasureTheory.lpNorm_fun_div_natCast : ∀ {α : Type u_1} {m : MeasurableSpace α} {𝕜 : Type u_3} [inst : NormedField 𝕜] [NormedSpace ℝ 𝕜] [CharZero 𝕜] {n : ℕ},
  n ≠ 0 →
    ∀ (f : α → 𝕜) (p : ENNReal) (μ : MeasureTheory.Measure α),
      MeasureTheory.lpNorm (fun x => f x / ↑n) p μ = MeasureTheory.lpNorm f p μ / ↑n
-- Mathlib.Algebra.Homology.Opposite
HomologicalComplex.instHasHomologyObjOppositeSymmUnopFunctorOp : ∀ {ι : Type u_1} (V : Type u_2) [inst : CategoryTheory.Category.{v_1, u_2} V] (c : ComplexShape ι)
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] (K : HomologicalComplex Vᵒᵖ c) (i : ι) [K.HasHomology i],
  ((HomologicalComplex.unopFunctor V c).obj (Opposite.op K)).HasHomology i
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.compare_minKey_modify_eq : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [inst : Std.TransOrd α]
  (h : t.WF) {k : α} {f : β → β} {he : (Std.DTreeMap.Internal.Impl.Const.modify k f t).isEmpty = false},
  compare ((Std.DTreeMap.Internal.Impl.Const.modify k f t).minKey he) (t.minKey ⋯) = Ordering.eq
-- Mathlib.Logic.Encodable.Pi
Encodable.finPi : (n : ℕ) → (π : Fin n → Type u_2) → [(i : Fin n) → Encodable (π i)] → Encodable ((i : Fin n) → π i)
-- Mathlib.Analysis.Meromorphic.Order
/-- The order of a meromorphic function `f` at `z₀` is finite iff `f` does not have
any zeros in a sufficiently small neighborhood of `z₀`.
 -/
meromorphicOrderAt_ne_top_iff_eventually_ne_zero : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : 𝕜} {f : 𝕜 → E},
  MeromorphicAt f x → (meromorphicOrderAt f x ≠ ⊤ ↔ ∀ᶠ (x : 𝕜) in nhdsWithin x {x}ᶜ, f x ≠ 0)
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.MonoidalCategory.tensorμ_tensorδ : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X₁ X₂ Y₁ Y₂ : C),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ X₁ X₂ Y₁ Y₂)
      (CategoryTheory.MonoidalCategory.tensorδ X₁ X₂ Y₁ Y₂) =
    CategoryTheory.CategoryStruct.id
      (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ X₂)
        (CategoryTheory.MonoidalCategoryStruct.tensorObj Y₁ Y₂))
-- Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
RestrictedProduct.topologicalSpace_eq_of_principal : ∀ {ι : Type u_1} {R : ι → Type u_2} {A : (i : ι) → Set (R i)} [inst : (i : ι) → TopologicalSpace (R i)] {S : Set ι},
  RestrictedProduct.topologicalSpace R A (Filter.principal S) = TopologicalSpace.induced DFunLike.coe inferInstance
-- Lean.Elab.Binders
Lean.Elab.Term.elabFunBinders : {α : Type} →
  Array Lean.Syntax →
    Option Lean.Expr → (Array Lean.Expr → Option Lean.Expr → Lean.Elab.TermElabM α) → Lean.Elab.TermElabM α
-- Mathlib.Algebra.Homology.Opposite
/-- The canonical isomorphism `K.op.opcycles i ≅ op (K.cycles i)`.  -/
HomologicalComplex.opcyclesOpIso : {ι : Type u_1} →
  {V : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_2} V] →
      {c : ComplexShape ι} →
        [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] →
          (K : HomologicalComplex V c) →
            (i : ι) → [inst_2 : K.HasHomology i] → K.op.opcycles i ≅ Opposite.op (K.cycles i)
-- Init.Data.SInt.Bitwise
Int64.neg_one_and : ∀ {a : Int64}, -1 &&& a = a
-- Mathlib.Logic.Equiv.Basic
Equiv.subtypeEquivRight_symm_apply : ∀ {α : Sort u_1} {p q : α → Prop} (e : ∀ (x : α), p x ↔ q x) (z : { x // q x }),
  (Equiv.subtypeEquivRight e).symm z = ⟨↑z, ⋯⟩
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toList_ric_eq_cons : ∀ {n : ℕ}, (*...=n).toList = 0 :: (1...=n).toList
-- Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
AlgebraicGeometry.Scheme.AffineZariskiSite.instIsLocallyFullOpensToOpensFunctorGrothendieckTopologyCarrierCarrierCommRingCat : ∀ {X : AlgebraicGeometry.Scheme},
  (AlgebraicGeometry.Scheme.AffineZariskiSite.toOpensFunctor X).IsLocallyFull (Opens.grothendieckTopology ↥X)
-- Mathlib.CategoryTheory.Preadditive.FreydCategory.RightFreyd
CategoryTheory.Preadditive.instCategoryRightFreyd : (V : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    [inst_1 : CategoryTheory.Preadditive V] →
      CategoryTheory.Category.{v_1, max u_1 v_1} (CategoryTheory.Preadditive.RightFreyd V)
-- Mathlib.Order.WellFoundedSet
Finset.partiallyWellOrderedOn_sup : ∀ {ι : Type u_1} {α : Type u_2} {r : α → α → Prop} (s : Finset ι) {f : ι → Set α},
  (s.sup f).PartiallyWellOrderedOn r ↔ ∀ i ∈ s, (f i).PartiallyWellOrderedOn r
-- Init.Data.Array.Bootstrap
Array.foldrM.fold.eq_def : ∀ {α : Type u} {β : Type v} {m : Type v → Type w} [inst : Monad m] (f : α → β → m β) (as : Array α) (stop i : ℕ)
  (h : i ≤ as.size) (b : β),
  Array.foldrM.fold f as stop i h b =
    if (i == stop) = true then pure b
    else
      match i, h with
      | 0, x => pure b
      | i.succ, h =>
        have this := ⋯;
        do
        let __do_lift ← f as[i] b
        Array.foldrM.fold f as stop i ⋯ __do_lift
-- Mathlib.Algebra.GroupWithZero.Divisibility
IsRelPrime.ne_zero_or_ne_zero : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] {x y : α} [Nontrivial α], IsRelPrime x y → x ≠ 0 ∨ y ≠ 0
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.sqrtTwoAddSeries_monotone_left : ∀ {x y : ℝ}, x ≤ y → ∀ (n : ℕ), x.sqrtTwoAddSeries n ≤ y.sqrtTwoAddSeries n
-- Mathlib.Analysis.Calculus.ContDiff.Defs
contDiffWithinAt_inter' : ∀ {𝕜 : 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] {s t : Set E}
  {f : E → F} {x : E} {n : WithTop ℕ∞},
  t ∈ nhdsWithin x s → (ContDiffWithinAt 𝕜 n f (s ∩ t) x ↔ ContDiffWithinAt 𝕜 n f s x)
-- Mathlib.Data.Finsupp.Basic
/-- `Finsupp.filter` as an `AddMonoidHom`.  -/
Finsupp.filterAddHom : {α : Type u_1} → {M : Type u_5} → [inst : AddZeroClass M] → (p : α → Prop) → [DecidablePred p] → (α →₀ M) →+ α →₀ M
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.mem_mk : ∀ {α : Type u_2} [inst : BooleanAlgebra α] {a : α} {L : Sublattice α}
  (h_compl : ∀ {a : α}, a ∈ L.carrier → aᶜ ∈ L.carrier) (h_bot : ⊥ ∈ L.carrier),
  a ∈ { toSublattice := L, compl_mem' := h_compl, bot_mem' := h_bot } ↔ a ∈ L
-- Mathlib.Combinatorics.Enumerative.Pentagonal.Ring
/-- And a second auxiliary sequence

$$ b_{k, n} = x^{(k+1)n} (x^{2k + n + 3} - 1) \prod_{i=0}^{n-1} (1 - x^{k + i + 2}) $$  -/
_private.Mathlib.Combinatorics.Enumerative.Pentagonal.Ring.0.Pentagonal.aux : {R : Type u_1} → [CommRing R] → ℕ → ℕ → R → R
-- Mathlib.Topology.Category.TopPair
TopPair.Hom.w : ∀ {X Y : TopPair} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp (TopPair.Hom.snd f) TopPair.map =
    CategoryTheory.CategoryStruct.comp TopPair.map (TopPair.Hom.fst f)
-- Mathlib.CategoryTheory.Grothendieck
CategoryTheory.Grothendieck.ιCompMap_hom_app_fiber : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F F' : CategoryTheory.Functor C CategoryTheory.Cat}
  (α : F ⟶ F') (c : C) (X : ↑(F.obj c)),
  ((CategoryTheory.Grothendieck.ιCompMap α c).hom.app X).fiber = CategoryTheory.eqToHom ⋯
-- Lean.Elab.Syntax
Lean.Elab.Term.ToParserDescrContext.leftRec : Lean.Elab.Term.ToParserDescrContext → Bool
-- Mathlib.CategoryTheory.Endofunctor.Algebra
/-- The inverse of the structure map of an initial algebra  -/
CategoryTheory.Endofunctor.Algebra.Initial.strInv : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Functor C C} →
      {A : CategoryTheory.Endofunctor.Algebra F} → CategoryTheory.Limits.IsInitial A → (A.a ⟶ F.obj A.a)
-- Lean.Declaration
Lean.ConstantInfo.defnInfo : Lean.DefinitionVal → Lean.ConstantInfo
-- Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
mvfderiv_comp_apply_of_eq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M' → M} {g : M → 𝕜} {y : M}
  (x : M'),
  MDiffAt g y → MDiffAt f x → f x = y → ∀ (v : TangentSpace I' x), (d% (g ∘ f) x) v = (d% g y) ((mfderiv% f x) v)
-- Mathlib.LinearAlgebra.Matrix.Hermitian
Matrix.isHermitian_intCast : ∀ {α : Type u_1} {n : Type u_4} [inst : Ring α] [inst_1 : StarRing α] [inst_2 : DecidableEq n] (d : ℤ), (↑d).IsHermitian
-- Mathlib.FieldTheory.Galois.Infinite
InfiniteGalois.normal_iff_isGalois : ∀ {k : Type u_1} {K : Type u_2} [inst : Field k] [inst_1 : Field K] [inst_2 : Algebra k K] (L : IntermediateField k K)
  [IsGalois k K], L.fixingSubgroup.Normal ↔ IsGalois k ↥L
-- Mathlib.Geometry.Euclidean.Circumcenter
/-- Given a point in the affine span from which all the points are
equidistant, that distance is the circumradius.  -/
Affine.Simplex.eq_circumradius_of_dist_eq : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P n) {p : P},
  p ∈ affineSpan ℝ (Set.range s.points) → ∀ {r : ℝ}, (∀ (i : Fin (n + 1)), dist (s.points i) p = r) → r = s.circumradius
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.symm_mk : ∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Semiring A₂]
  [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂] (e : A₁ ≃ A₂)
  (h₁ : ∀ (x y : A₁), e.toFun (x * y) = e.toFun x * e.toFun y)
  (h₂ : ∀ (x y : A₁), e.toFun (x + y) = e.toFun x + e.toFun y)
  (h₃ : ∀ (r : R), e.toFun ((algebraMap R A₁) r) = (algebraMap R A₂) r),
  { toEquiv := e, map_mul' := h₁, map_add' := h₂, commutes' := h₃ }.symm =
    { toEquiv := e.symm, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
-- Mathlib.Analysis.Meromorphic.Basic
Meromorphic.div : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {f g : 𝕜 → 𝕜'}, Meromorphic f → Meromorphic g → Meromorphic (f / g)
-- Mathlib.Data.Complex.Basic
Complex.mk_mul_mk : ∀ (x₁ x₂ y₁ y₂ : ℝ),
  { re := x₁, im := y₁ } * { re := x₂, im := y₂ } = { re := x₁ * x₂ - y₁ * y₂, im := x₁ * y₂ + y₁ * x₂ }
-- Mathlib.Tactic.Translate.UnfoldBoundary
/-- Set up the monadic context:
- Set the transparency to `.all`, just like is done in `Meta.check`.
- Use `withCanUnfoldPred` to not allow unfolding the constants for which we want to insert casts.
- Set up the `SimpM` context so that `Simp.simp` will unfold constants from `b.unfolds`.
 -/
_private.Mathlib.Tactic.Translate.UnfoldBoundary.0.Mathlib.Tactic.UnfoldBoundary.run : {α : Type} → Mathlib.Tactic.UnfoldBoundary.UnfoldBoundaries → Lean.Meta.SimpM α → Lean.MetaM α
-- Mathlib.FieldTheory.Galois.IsGaloisGroup
/-- **Alias** of `IsGaloisGroup.mulEquivCongr`.

---

If `G` and `G'` are finite Galois groups for `B/A`, then `G` is isomorphic to `G'`.  -/
IsGaloisGroup.mulEquivCongr' : (G : Type u_1) →
  (G' : Type u_2) →
    [inst : Group G] →
      [inst_1 : Group G'] →
        (A : Type u_5) →
          (B : Type u_6) →
            [inst_2 : CommRing A] →
              [inst_3 : CommRing B] →
                [IsDomain B] →
                  [inst_5 : Algebra A B] →
                    [FaithfulSMul A B] →
                      [inst_7 : MulSemiringAction G B] →
                        [inst_8 : MulSemiringAction G' B] →
                          [IsGaloisGroup G A B] → [IsGaloisGroup G' A B] → [Finite G] → [Finite G'] → G ≃* G'
-- Mathlib.Data.List.AList
/-- Two associative lists are disjoint if they have no common keys.  -/
AList.Disjoint : {α : Type u} → {β : α → Type v} → AList β → AList β → Prop
-- Mathlib.Algebra.Order.Hom.Ring
OrderRingIso.coe_toOrderRingHom_refl : ∀ {α : Type u_2} [inst : NonAssocSemiring α] [inst_1 : Preorder α], ↑(OrderRingIso.refl α) = OrderRingHom.id α
-- Mathlib.Algebra.Module.Equiv.Defs
SemilinearEquivClass.instSemilinearMapClass : ∀ {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} (F : Type u_14) [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module S M₂] {σ : R →+* S}
  {σ' : S →+* R} [inst_6 : RingHomInvPair σ σ'] [inst_7 : RingHomInvPair σ' σ] [inst_8 : EquivLike F M M₂]
  [s : SemilinearEquivClass F σ M M₂], SemilinearMapClass F σ M M₂
-- Mathlib.Algebra.FreeAlgebra
FreeAlgebra.lift_symm_apply : ∀ (R : Type u_1) {X : Type u_2} [inst : CommSemiring R] {A : Type u_3} [inst_1 : Semiring A] [inst_2 : Algebra R A]
  (F : FreeAlgebra R X →ₐ[R] A), (FreeAlgebra.lift R).symm F = ⇑F ∘ FreeAlgebra.ι R
-- Init.Data.String.Legacy
String.splitAux : String → (Char → Bool) → String.Pos.Raw → String.Pos.Raw → List String → List String
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
ContinuousMultilinearMap.prod_ext : ∀ {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} {M₃ : Type w₃} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M₃]
  [inst_4 : (i : ι) → Module R (M₁ i)] [inst_5 : Module R M₂] [inst_6 : Module R M₃]
  [inst_7 : (i : ι) → TopologicalSpace (M₁ i)] [inst_8 : TopologicalSpace M₂] [inst_9 : TopologicalSpace M₃]
  {f g : ContinuousMultilinearMap R M₁ (M₂ × M₃)},
  (ContinuousLinearMap.fst R M₂ M₃).compContinuousMultilinearMap f =
      (ContinuousLinearMap.fst R M₂ M₃).compContinuousMultilinearMap g →
    (ContinuousLinearMap.snd R M₂ M₃).compContinuousMultilinearMap f =
        (ContinuousLinearMap.snd R M₂ M₃).compContinuousMultilinearMap g →
      f = g
-- Mathlib.Data.Sum.Order
Sum.Lex.partialOrder : {α : Type u_1} → {β : Type u_2} → [PartialOrder α] → [PartialOrder β] → PartialOrder (α ⊕ₗ β)