mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells
HomotopicalAlgebra.AttachCells.ofArrowIso_cofan₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {α : Type t} {A B : α → C} {g : (a : α) → A a ⟶ B a}
  {X₁ X₂ : C} {f : X₁ ⟶ X₂} (c : HomotopicalAlgebra.AttachCells g f) {Y₁ Y₂ : C} {f' : Y₁ ⟶ Y₂}
  (e : CategoryTheory.Arrow.mk f ≅ CategoryTheory.Arrow.mk f'), (c.ofArrowIso e).cofan₂ = c.cofan₂
-- Mathlib.Analysis.Calculus.DiffContOnCl
DiffContOnCl.continuousOn_ball : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedSpace 𝕜 F] {f : E → F} [NormedSpace ℝ E]
  {x : E} {r : ℝ}, DiffContOnCl 𝕜 f (Metric.ball x r) → ContinuousOn f (Metric.closedBall x r)
-- Init.Data.Fin.Fold
/-- Combine all the values that can be represented by `Fin n` with an initial value, starting at `n - 1`
and nesting to the right.

Example:
 * `Fin.foldr 3 (·.val + ·) (0 : Nat) = (0 : Fin 3).val + ((1 : Fin 3).val + ((2 : Fin 3).val + 0))`
 -/
Fin.foldr : {α : Sort u_1} → (n : ℕ) → (Fin n → α → α) → α → α
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.card_mul_iff : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Mul α] {s t : Finset α},
  (s * t).card = s.card * t.card ↔ Set.InjOn (fun p => p.1 * p.2) (↑s ×ˢ ↑t)
-- Mathlib.Topology.Connected.Basic
/-- Theorem of bark and tree: if a set is within a preconnected set and its closure, then it is
preconnected as well. See also `IsConnected.subset_closure`.  -/
IsPreconnected.subset_closure : ∀ {α : Type u} [inst : TopologicalSpace α] {s t : Set α}, IsPreconnected s → s ⊆ t → t ⊆ closure s → IsPreconnected t
-- Lean.Linter.Deprecated
Lean.Linter.DeprecationEntry.newName? : Lean.Linter.DeprecationEntry → Option Lean.Name
-- Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
CliffordAlgebraQuaternion.ofQuaternion_comp_toQuaternion : ∀ {R : Type u_1} [inst : CommRing R] {c₁ c₂ : R},
  CliffordAlgebraQuaternion.ofQuaternion.comp CliffordAlgebraQuaternion.toQuaternion =
    AlgHom.id R (CliffordAlgebra (CliffordAlgebraQuaternion.Q c₁ c₂))
-- Mathlib.CategoryTheory.Category.Preorder
CategoryTheory.homOfLE_comp : ∀ {X : Type u} [inst : Preorder X] {x y z : X} (h : x ≤ y) (k : y ≤ z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.homOfLE h) (CategoryTheory.homOfLE k) = CategoryTheory.homOfLE ⋯
-- Mathlib.SetTheory.Ordinal.Principal
/-- **Alias** of `Ordinal.isPrincipal_zero`. -/
Ordinal.principal_zero : ∀ {op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}}, Ordinal.IsPrincipal op 0
-- Init.Data.Nat.Lcm
Nat.instIdempotentOpLcm : Std.IdempotentOp Nat.lcm
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.minKey!_insert_of_isEmpty : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α] {k : α} {v : β k}, t.isEmpty = true → (t.insert k v).minKey! = k
-- Mathlib.AlgebraicTopology.SimplicialSet.RelativeMorphism
SSet.RelativeMorphism.map_eq_of_mem : ∀ {X Y : SSet} {A : X.Subcomplex} {B : Y.Subcomplex} {φ : A.toSSet ⟶ B.toSSet} (f : SSet.RelativeMorphism A B φ)
  {n : SimplexCategoryᵒᵖ} (a : X.obj n) (ha : a ∈ A.obj n),
  (CategoryTheory.ConcreteCategory.hom (f.map.app n)) a = ↑((CategoryTheory.ConcreteCategory.hom (φ.app n)) ⟨a, ha⟩)
-- Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf
PresheafOfModules.Derivation.instSubsingletonUniversal : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : CategoryTheory.Functor Cᵒᵖ CommRingCat} {F : CategoryTheory.Functor C D}
  {R : CategoryTheory.Functor Dᵒᵖ CommRingCat}
  {M : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))} {φ : S ⟶ F.op.comp R}
  (d : M.Derivation φ), Subsingleton d.Universal
-- Mathlib.Probability.Independence.BoundedContinuousFunction
indepSets_comap_pi_of_prod_bcf : ∀ {Ω : Type u_1} {S : Type u_2} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {E : S → Type u_4}
  [inst : (s : S) → TopologicalSpace (E s)] [inst_1 : (s : S) → MeasurableSpace (E s)] [∀ (s : S), BorelSpace (E s)]
  [∀ (s : S), HasOuterApproxClosed (E s)] {X : (s : S) → Ω → E s} [inst_4 : Fintype S]
  [MeasureTheory.IsProbabilityMeasure P] {𝒜 : Set (Set Ω)},
  (∀ A ∈ 𝒜, MeasureTheory.NullMeasurableSet A P) →
    (∀ (s : S), AEMeasurable (X s) P) →
      (∀ A ∈ 𝒜,
          ∀ (f : (s : S) → BoundedContinuousFunction (E s) ℝ),
            ∫ (ω : Ω) in A, ∏ s, (f s) (X s ω) ∂P = P.real A * ∫ (ω : Ω), ∏ s, (f s) (X s ω) ∂P) →
        ProbabilityTheory.IndepSets 𝒜 {A | MeasurableSet A} P
-- Init.Data.Int.DivMod.Bootstrap
Int.sub_ediv_of_dvd : ∀ (a : ℤ) {b c : ℤ}, c ∣ b → (a - b) / c = a / c - b / c
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
/-- `Scheme.Modules.restrict` along an open immersion `X ⟶ Y` sends `𝒪_Y` to `𝒪_X`.  -/
AlgebraicGeometry.Scheme.Modules.restrictUnitIso : {X Y : AlgebraicGeometry.Scheme} →
  (f : X ⟶ Y) →
    [inst : AlgebraicGeometry.IsOpenImmersion f] →
      AlgebraicGeometry.Scheme.Modules.restrict (SheafOfModules.unit Y.ringCatSheaf) f ≅
        SheafOfModules.unit X.ringCatSheaf
-- Mathlib.Order.Filter.Extr
/-- If `f` is antitone on `Ioc a b` and monotone on `Ico b c`, then the minimum of `f` on
`Ioo a c` is attained at `b`.  -/
isMinOn_Ioo_of_anti_mono : ∀ {α : Type u} {β : Type u_1} [inst : LinearOrder α] [inst_1 : Preorder β] {a b c : α} {f : α → β},
  AntitoneOn f (Set.Ioc a b) → MonotoneOn f (Set.Ico b c) → IsMinOn f (Set.Ioo a c) b
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
SubMulAction.ofFixingSubgroup_insert_map_apply : ∀ {M : Type u_1} {α : Type u_2} [inst : Group M] [inst_1 : MulAction M α] {a : α}
  {s : Set ↥(SubMulAction.ofStabilizer M a)} {x : α}
  (hx : x ∈ SubMulAction.ofFixingSubgroup M (insert a (Subtype.val '' s))),
  ↑↑((SubMulAction.ofFixingSubgroup_insert_map a s) ⟨x, hx⟩) = x
-- Mathlib.RingTheory.LocalProperties.Submodule
Module.eq_of_localization_maximal : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_5) [inst_3 : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)]
  [inst_4 : (P : Ideal R) → [inst_4 : P.IsMaximal] → Module R (Mₚ P)]
  (f : (P : Ideal R) → [inst_5 : P.IsMaximal] → M →ₗ[R] Mₚ P)
  [∀ (P : Ideal R) [inst_5 : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)] (m m' : M),
  (∀ (P : Ideal R) [inst_6 : P.IsMaximal], (f P) m = (f P) m') → m = m'
-- Init.WFTactics
/-- Constructs a proof of decreasing along a well founded relation, by simplifying, then applying
lexicographic order lemmas and finally using `ts` to solve the base case. If it fails,
it prints a message to help the user diagnose an ill-founded recursive definition.  -/
tacticDecreasing_with_ : Lean.ParserDescr
-- Mathlib.LinearAlgebra.Basis.VectorSpace
Module.Basis.coe_extend : ∀ {K : Type u_3} {V : Type u_4} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {s : Set V}
  (hs : LinearIndepOn K id s), ⇑(Module.Basis.extend hs) = Subtype.val
-- Mathlib.GroupTheory.Coset.Basic
AddSubgroup.quotientiInfEmbedding_apply_mk : ∀ {α : Type u_1} [inst : AddGroup α] {ι : Type u_2} (f : ι → AddSubgroup α) (g : α) (i : ι),
  (AddSubgroup.quotientiInfEmbedding f) (↑g) i = ↑g
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
SheafOfModules.instIsFinitePresentationOfIsIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : ∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat]
  [inst_2 : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M N : SheafOfModules R} (f : M ⟶ N)
  [inst_3 : CategoryTheory.IsIso f] (σ : M.QuasicoherentData) [σ.IsFinitePresentation],
  (SheafOfModules.QuasicoherentData.ofIsIso f σ).IsFinitePresentation
-- Mathlib.CategoryTheory.ComposableArrows.Basic
/-- Constructor for isomorphisms in `ComposableArrows C 3`.  -/
CategoryTheory.ComposableArrows.isoMk₃ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {f g : CategoryTheory.ComposableArrows C 3} →
      (app₀ : f.obj' 0 _proof_297✝ ≅ g.obj' 0 _proof_297✝) →
        (app₁ : f.obj' 1 _proof_298✝ ≅ g.obj' 1 _proof_298✝) →
          (app₂ : f.obj' 2 _proof_299✝ ≅ g.obj' 2 _proof_299✝) →
            (app₃ : f.obj' 3 _proof_300✝ ≅ g.obj' 3 _proof_300✝) →
              CategoryTheory.CategoryStruct.comp
                    (f.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 _proof_298✝) app₁.hom =
                  CategoryTheory.CategoryStruct.comp app₀.hom
                    (g.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 _proof_298✝) →
                CategoryTheory.CategoryStruct.comp (f.map' 1 2 _proof_246✝ _proof_299✝) app₂.hom =
                    CategoryTheory.CategoryStruct.comp app₁.hom (g.map' 1 2 _proof_246✝ _proof_299✝) →
                  CategoryTheory.CategoryStruct.comp (f.map' 2 3 _proof_299✝ _proof_300✝) app₃.hom =
                      CategoryTheory.CategoryStruct.comp app₂.hom (g.map' 2 3 _proof_299✝ _proof_300✝) →
                    (f ≅ g)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.mul_inter_subset : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Mul α] {s t₁ t₂ : Finset α}, s * (t₁ ∩ t₂) ⊆ s * t₁ ∩ (s * t₂)
-- Mathlib.Topology.LocallyConstant.Basic
IsLocallyConstant.inv : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : Inv Y] ⦃f : X → Y⦄,
  IsLocallyConstant f → IsLocallyConstant f⁻¹
-- Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno
iteratedDerivWithin_vcomp_two : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {g : E → F} {f : 𝕜 → E}
  {s : Set 𝕜} {t : Set E} {x : 𝕜},
  ContDiffWithinAt 𝕜 2 g t (f x) →
    ContDiffWithinAt 𝕜 2 f s x →
      UniqueDiffOn 𝕜 t →
        UniqueDiffOn 𝕜 s →
          x ∈ s →
            Set.MapsTo f s t →
              iteratedDerivWithin 2 (g ∘ f) s x =
                ((iteratedFDerivWithin 𝕜 2 g t (f x)) fun x_1 => derivWithin f s x) +
                  (fderivWithin 𝕜 g t (f x)) (iteratedDerivWithin 2 f s x)
-- Init.SizeOf
instSizeOfForallUnit : {α : Sort u_1} → [SizeOf α] → SizeOf (Unit → α)
-- Mathlib.NumberTheory.WellApproximable
/-- **Dirichlet's approximation theorem**

See also `Real.exists_rat_abs_sub_le_and_den_le`.  -/
AddCircle.exists_norm_nsmul_le : ∀ {T : ℝ} [hT : Fact (0 < T)] (ξ : AddCircle T) {n : ℕ}, 0 < n → ∃ j ∈ Set.Icc 1 n, ‖j • ξ‖ ≤ T / ↑(n + 1)
-- Mathlib.Tactic.DeriveCountable
/-- The deriving handler for the `Countable` class.
Handles non-nested non-reflexive inductive types.
They can be mutual too — in that case, there is an optimization to re-use all the generated
functions and proofs.
 -/
Mathlib.Deriving.Countable.mkCountableInstance : Array Lean.Name → Lean.Elab.Command.CommandElabM Bool
-- Mathlib.FieldTheory.SeparableDegree
/-- A field is a perfect field (which means that any irreducible polynomial is separable)
if and only if every separable degree one polynomial splits.  -/
perfectField_iff_splits_of_natSepDegree_eq_one : ∀ (F : Type u_1) [inst : Field F], PerfectField F ↔ ∀ (f : Polynomial F), f.natSepDegree = 1 → f.Splits
-- Init.Data.ByteArray.Basic
/-- Computes a hash for a `ByteArray`.
 -/
ByteArray.hash : ByteArray → UInt64
-- Mathlib.Data.NNReal.Defs
Real.toNNReal_zero : Real.toNNReal 0 = 0
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.of_toArray_perm : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp},
  t₁.toArray.Perm t₂.toArray → t₁.Equiv t₂
-- Mathlib.CategoryTheory.Sums.Products
CategoryTheory.Sum.functorEquiv_unitIso_inv_app_app_inl : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {A' : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} A'] {B : Type u} [inst_2 : CategoryTheory.Category.{v, u} B]
  (X : CategoryTheory.Functor (A ⊕ A') B) (a : A),
  ((CategoryTheory.Sum.functorEquiv A A' B).unitIso.inv.app X).app (Sum.inl a) =
    CategoryTheory.CategoryStruct.id (X.obj (Sum.inl a))
-- Init.Data.Option.Lemmas
_private.Init.Data.Option.Lemmas.0.Option.pfilter.match_1.eq_1 : ∀ {α : Type u_1} (motive : (o : Option α) → ((a : α) → o = some a → Bool) → Sort u_2)
  (p : (a : α) → none = some a → Bool) (h_1 : (p : (a : α) → none = some a → Bool) → motive none p)
  (h_2 : (a : α) → (p : (a_1 : α) → some a = some a_1 → Bool) → motive (some a) p),
  (match none, p with
    | none, p => h_1 p
    | some a, p => h_2 a p) =
    h_1 p
-- Init.Data.List.Monadic
_private.Init.Data.List.Monadic.0.List.anyM.match_1.eq_1 : ∀ (motive : Bool → Sort u_1) (h_1 : Unit → motive true) (h_2 : Unit → motive false),
  (match true with
    | true => h_1 ()
    | false => h_2 ()) =
    h_1 ()
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.isOpenImmersion_respectsIso : AlgebraicGeometry.IsOpenImmersion.RespectsIso
-- Mathlib.AlgebraicTopology.DoldKan.Compatibility
AlgebraicTopology.DoldKan.Compatibility.equivalence₂CounitIso_inv_app : ∀ {A : Type u_1} {A' : Type u_2} {B : Type u_3} {B' : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} A'] [inst_2 : CategoryTheory.Category.{v_3, u_3} B]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} B'] {eA : A ≌ A'} (eB : B ≌ B') {e' : A' ≌ B'}
  {F : CategoryTheory.Functor A B'} (hF : eA.functor.comp e'.functor ≅ F) (X : B),
  (AlgebraicTopology.DoldKan.Compatibility.equivalence₂CounitIso eB hF).inv.app X =
    CategoryTheory.CategoryStruct.comp (eB.unitIso.hom.app X)
      (CategoryTheory.CategoryStruct.comp (eB.inverse.map (e'.counitIso.inv.app (eB.functor.obj X)))
        (CategoryTheory.CategoryStruct.comp
          (eB.inverse.map (e'.functor.map (eA.counitIso.inv.app (e'.inverse.obj (eB.functor.obj X)))))
          (eB.inverse.map (hF.hom.app (eA.inverse.obj (e'.inverse.obj (eB.functor.obj X)))))))
-- Mathlib.GroupTheory.Subgroup.Center
Subgroup.centerCongr.eq_1 : ∀ {G : Type u_1} [inst : Group G] {H : Type u_2} [inst_1 : Group H] (e : G ≃* H),
  Subgroup.centerCongr e = Submonoid.centerCongr e
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.filter.eq_def : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (f : (a : α) → β a → Bool) (t : Std.DTreeMap.Internal.Impl α β)
  (hl : t.Balanced),
  Std.DTreeMap.Internal.Impl.filter f t hl =
    match t, hl with
    | Std.DTreeMap.Internal.Impl.leaf, hl => { impl := Std.DTreeMap.Internal.Impl.leaf, balanced_impl := ⋯ }
    | Std.DTreeMap.Internal.Impl.inner sz k v l r, hl =>
      match f k v with
      | false =>
        match Std.DTreeMap.Internal.Impl.filter f l ⋯ with
        | { impl := l', balanced_impl := hl' } =>
          match Std.DTreeMap.Internal.Impl.filter f r ⋯ with
          | { impl := r', balanced_impl := hr' } => { impl := (l'.link2 r' ⋯ ⋯).impl, balanced_impl := ⋯ }
      | true =>
        match Std.DTreeMap.Internal.Impl.filter f l ⋯ with
        | { impl := l', balanced_impl := hl' } =>
          match Std.DTreeMap.Internal.Impl.filter f r ⋯ with
          | { impl := r', balanced_impl := hr' } =>
            { impl := (Std.DTreeMap.Internal.Impl.link k v l' r' ⋯ ⋯).impl, balanced_impl := ⋯ }
-- Mathlib.RingTheory.WittVector.InitTail
WittVector.init_sub : ∀ {p : ℕ} {R : Type u_1} [inst : CommRing R] [inst_1 : Fact (Nat.Prime p)] (x y : WittVector p R) (n : ℕ),
  WittVector.init n (x - y) = WittVector.init n (WittVector.init n x - WittVector.init n y)
-- Init.Data.Vector.Lex
Vector.le_antisymm : ∀ {α : Type u_1} {n : ℕ} [inst : LT α] [inst_1 : LE α] [Std.IsLinearOrder α] [Std.LawfulOrderLT α] {xs ys : Vector α n},
  xs ≤ ys → ys ≤ xs → xs = ys
-- Mathlib.LinearAlgebra.BilinearForm.Properties
LinearMap.BilinForm.isAlt_zero : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  LinearMap.BilinForm.IsAlt 0
-- Mathlib.Analysis.Calculus.FDeriv.Analytic
ContinuousMultilinearMap.changeOrigin_toFormalMultilinearSeries : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {ι : Type u_2} {E : ι → Type u_3} [inst_3 : (i : ι) → NormedAddCommGroup (E i)]
  [inst_4 : (i : ι) → NormedSpace 𝕜 (E i)] [inst_5 : Fintype ι] (f : ContinuousMultilinearMap 𝕜 E F) (x : (i : ι) → E i)
  [inst_6 : DecidableEq ι],
  (continuousMultilinearCurryFin1 𝕜 ((i : ι) → E i) F) (f.toFormalMultilinearSeries.changeOrigin x 1) = f.linearDeriv x
-- Mathlib.Topology.UniformSpace.UniformConvergence
/-- A sequence that converges uniformly is also uniformly Cauchy  -/
TendstoUniformlyOn.uniformCauchySeqOn : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α}
  {p : Filter ι}, TendstoUniformlyOn F f p s → UniformCauchySeqOn F p s
-- Mathlib.GroupTheory.Transfer
/-- The homomorphism `G →* P` in Burnside's transfer theorem.  -/
MonoidHom.transferSylow : {G : Type u_1} →
  [inst : Group G] →
    {p : ℕ} → (P : Sylow p G) → Subgroup.normalizer ↑P ≤ Subgroup.centralizer ↑P → [(↑P).FiniteIndex] → G →* ↥↑P
-- Mathlib.Util.AtLocation
Mathlib.Tactic.instBEqBehaviorIfUnchanged.beq : Mathlib.Tactic.BehaviorIfUnchanged → Mathlib.Tactic.BehaviorIfUnchanged → Bool
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.toContinuousMapAddMonoidHom.eq_1 : ∀ (α : Type u) (R : Type u_2) [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace R] [inst_2 : AddMonoid R]
  [inst_3 : BoundedAdd R] [inst_4 : ContinuousAdd R],
  BoundedContinuousFunction.toContinuousMapAddMonoidHom α R =
    { toFun := BoundedContinuousFunction.toContinuousMap, map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.Data.Fin.SuccPred
finCongr_apply : ∀ {n m : ℕ} (eq : n = m) (i : Fin n), (finCongr eq) i = Fin.cast eq i
-- Mathlib.Data.EReal.Basic
EReal.real_coe_toENNReal : ∀ (x : ℝ), (↑x).toENNReal = ENNReal.ofReal x
-- Mathlib.Algebra.Category.ModuleCat.Topology.Basic
TopModuleCat.instPreservesLimitsOfShapeTopCatForget₂ContinuousLinearMapIdCarrierContinuousMapCarrierOfHasLimitsOfShapeOfModuleCatForgetLinearMap : ∀ {R : Type u} [inst : Ring R] [inst_1 : TopologicalSpace R] {J : Type u_2}
  [inst_2 : CategoryTheory.Category.{v_1, u_2} J] [CategoryTheory.Limits.HasLimitsOfShape J (ModuleCat R)]
  [CategoryTheory.Limits.PreservesLimitsOfShape J (CategoryTheory.forget (ModuleCat R))],
  CategoryTheory.Limits.PreservesLimitsOfShape J (CategoryTheory.forget₂ (TopModuleCat R) TopCat)
-- Mathlib.CategoryTheory.Localization.Monoidal.Basic
CategoryTheory.Localization.Monoidal.associator_naturality₁_assoc : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D)
  (W : CategoryTheory.MorphismProperty C) [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : W.IsMonoidal]
  [inst_4 : L.IsLocalization W] {unit : D} (ε : L.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ≅ unit)
  {X₁ X₂ X₃ Y₁ : CategoryTheory.LocalizedMonoidal L W ε} (f₁ : X₁ ⟶ Y₁) {Z : CategoryTheory.LocalizedMonoidal L W ε}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj Y₁ (CategoryTheory.MonoidalCategoryStruct.tensorObj X₂ X₃) ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.whiskerRight f₁ X₂) X₃)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Y₁ X₂ X₃).hom h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X₁ X₂ X₃).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight f₁ (CategoryTheory.MonoidalCategoryStruct.tensorObj X₂ X₃))
        h)
-- Mathlib.Condensed.TopCatAdjunction
/-- The functor `CondensedSet ⥤ TopCat`  -/
condensedSetToTopCat : CategoryTheory.Functor CondensedSet TopCat
-- Init.Grind.AC
_private.Init.Grind.AC.0.Lean.Grind.AC.Seq.unionFuel.match_1.eq_4 : ∀ (motive : Lean.Grind.AC.Seq → Lean.Grind.AC.Seq → Sort u_1) (x₁ : Lean.Grind.AC.Var) (s₁ : Lean.Grind.AC.Seq)
  (x₂ : Lean.Grind.AC.Var) (s₂ : Lean.Grind.AC.Seq)
  (h_1 : (x₁ x₂ : Lean.Grind.AC.Var) → motive (Lean.Grind.AC.Seq.var x₁) (Lean.Grind.AC.Seq.var x₂))
  (h_2 :
    (x₁ x : Lean.Grind.AC.Var) →
      (s : Lean.Grind.AC.Seq) → motive (Lean.Grind.AC.Seq.var x₁) (Lean.Grind.AC.Seq.cons x s))
  (h_3 :
    (x : Lean.Grind.AC.Var) →
      (s : Lean.Grind.AC.Seq) →
        (x₂ : Lean.Grind.AC.Var) → motive (Lean.Grind.AC.Seq.cons x s) (Lean.Grind.AC.Seq.var x₂))
  (h_4 :
    (x₁ : Lean.Grind.AC.Var) →
      (s₁ : Lean.Grind.AC.Seq) →
        (x₂ : Lean.Grind.AC.Var) →
          (s₂ : Lean.Grind.AC.Seq) → motive (Lean.Grind.AC.Seq.cons x₁ s₁) (Lean.Grind.AC.Seq.cons x₂ s₂)),
  (match Lean.Grind.AC.Seq.cons x₁ s₁, Lean.Grind.AC.Seq.cons x₂ s₂ with
    | Lean.Grind.AC.Seq.var x₁, Lean.Grind.AC.Seq.var x₂ => h_1 x₁ x₂
    | Lean.Grind.AC.Seq.var x₁, Lean.Grind.AC.Seq.cons x s => h_2 x₁ x s
    | Lean.Grind.AC.Seq.cons x s, Lean.Grind.AC.Seq.var x₂ => h_3 x s x₂
    | Lean.Grind.AC.Seq.cons x₁ s₁, Lean.Grind.AC.Seq.cons x₂ s₂ => h_4 x₁ s₁ x₂ s₂) =
    h_4 x₁ s₁ x₂ s₂
-- Mathlib.Data.Rat.Lemmas
Rat.pnatDen_eq_iff_den_eq : ∀ {x : ℚ} {n : ℕ+}, x.pnatDen = n ↔ x.den = ↑n
-- Init.Internal.Order.Basic
Lean.Order.instMonoBindOptionT : ∀ {m : Type u_1 → Type u_2} [inst : Monad m] [inst_1 : (α : Type u_1) → Lean.Order.PartialOrder (m α)]
  [Lean.Order.MonoBind m], Lean.Order.MonoBind (OptionT m)
-- Mathlib.Algebra.Category.Grp.Biproducts
AddCommGrpCat.biprodIsoProd_inv_comp_fst : ∀ (G H : AddCommGrpCat),
  CategoryTheory.CategoryStruct.comp (G.biprodIsoProd H).inv CategoryTheory.Limits.biprod.fst =
    AddCommGrpCat.ofHom (AddMonoidHom.fst ↑G ↑H)
-- Mathlib.CategoryTheory.Category.Factorisation
CategoryTheory.Factorisation.forget_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y}
  {X_1 Y_1 : CategoryTheory.Factorisation f} (f_1 : X_1 ⟶ Y_1), CategoryTheory.Factorisation.forget.map f_1 = f_1.h
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.Red.length_le : ∀ {α : Type u} {L₁ L₂ : List (α × Bool)}, FreeGroup.Red L₁ L₂ → L₂.length ≤ L₁.length
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.map_map : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} {M : Matrix m n α} {β : Type u_10} {γ : Type u_11} {f : α → β} {g : β → γ},
  (M.map f).map g = M.map (g ∘ f)
-- Mathlib.Data.Option.NAry
Option.map₂_curry : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α × β → γ) (a : Option α) (b : Option β),
  Option.map₂ (Function.curry f) a b = Option.map f (Option.map₂ Prod.mk a b)
-- Mathlib.Logic.Function.Basic
instDecidableCurryOfMk_mathlib : {α : Type u_3} →
  {β : Type u_4} → {r : α × β → Prop} → {a : α} → {b : β} → [Decidable (r (a, b))] → Decidable (Function.curry r a b)
-- Lean.Server.References
/-- Definition `Reference` of the identifier.
Is equal to `none` if e.g. the definition is outside of the module where this `RefInfo` is used.
 -/
Lean.Server.RefInfo.definition : Lean.Server.RefInfo → Option Lean.Server.Reference
-- Init.Data.List.Lemmas
List.isEmpty_eq_false_iff : ∀ {α : Type u_1} {l : List α}, l.isEmpty = false ↔ l ≠ []
-- Mathlib.Analysis.Polynomial.MahlerMeasure
Polynomial.norm_coeff_le_choose_mul_mapMahlerMeasure : ∀ {A : Type u_2} [inst : NormedRing A] (v : A →+* ℂ),
  Isometry ⇑v → ∀ (n : ℕ) (p : Polynomial A), ‖p.coeff n‖ ≤ ↑(p.natDegree.choose n) * p.mapMahlerMeasure v
-- Mathlib.NumberTheory.Padics.Measure.Basic
AbstractMeasure.map_dirac : ∀ {X : Type u_1} {Y : Type u_2} {R : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : CommRing R] [inst_3 : TopologicalSpace R] [inst_4 : IsTopologicalRing R] (f : C(X, Y)) (x : X),
  (AbstractMeasure.map f) (AbstractMeasure.dirac R x) = AbstractMeasure.dirac R (f x)
-- Init.Data.Array.DecidableEq
Array.instDecidableEmpEq_csimp : @Array.instDecidableEmpEq = @Array.instDecidableEmpEqImpl
-- Mathlib.CategoryTheory.Action.Basic
/-- The underlying monoid homomorphism of this action  -/
Action.ρ : {V : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    {G : Type u_2} → [inst_1 : Monoid G] → (self : Action V G) → G →* CategoryTheory.End self.V