mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DHashMap.Internal.Defs
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.Raw₀.reinsertAux : {α : Type u} → {β : α → Type v} → (α → UInt64) → { d // 0 < d.size } → (a : α) → β a → { d // 0 < d.size }
-- Mathlib.Geometry.Diffeology.Basic
Diffeology.DSmooth.continuous : ∀ {X : Type u_1} {Y : Type u_2} [inst : DiffeologicalSpace X] [inst_1 : DiffeologicalSpace Y] {f : X → Y},
  Diffeology.DSmooth f → Continuous f
-- Mathlib.Data.List.Rotate
List.cyclicPermutations_nil : ∀ {α : Type u}, [].cyclicPermutations = [[]]
-- Mathlib.GroupTheory.Coset.Defs
QuotientAddGroup.leftRel.eq_1 : ∀ {α : Type u_1} [inst : AddGroup α] (s : AddSubgroup α), QuotientAddGroup.leftRel s = AddAction.orbitRel (↥s.op) α
-- Mathlib.Algebra.Polynomial.Laurent
AddMonoidAlgebra.comapDomainAddMonoidHom.congr_simp : ∀ {R : Type u_3} {M : Type u_6} {N : Type u_7} [inst : Semiring R] (f f_1 : M → N) (e_f : f = f_1)
  (hf : Function.Injective f),
  AddMonoidAlgebra.comapDomainAddMonoidHom f hf = AddMonoidAlgebra.comapDomainAddMonoidHom f_1 ⋯
-- Init.Data.Option.Lemmas
_private.Init.Data.Option.Lemmas.0.Option.isSome.match_1.eq_2 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (h_1 : (val : α) → motive (some val)) (h_2 : Unit → motive none),
  (match none with
    | some val => h_1 val
    | none => h_2 ()) =
    h_2 ()
-- Mathlib.Geometry.Euclidean.NinePointCircle
Affine.Triangle.altitudeFoot_mem_ninePointCircle : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (s : Affine.Triangle ℝ P) (i : Fin 3),
  Affine.Simplex.altitudeFoot s i ∈ Affine.Simplex.ninePointCircle s
-- Mathlib.Combinatorics.Matroid.Basic
/-- For any two sets `B₁`, `B₂` in a family with the exchange property, the differences `B₁ \ B₂`
and `B₂ \ B₁` have the same `ℕ∞`-cardinality.  -/
Matroid.ExchangeProperty.encard_sdiff_eq : ∀ {α : Type u_1} {IsBase : Set α → Prop} {B₁ B₂ : Set α},
  Matroid.ExchangeProperty IsBase → IsBase B₁ → IsBase B₂ → (B₁ \ B₂).encard = (B₂ \ B₁).encard
-- Mathlib.CategoryTheory.Monad.Adjunction
CategoryTheory.Adjunction.toMonad_η : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R), h.toMonad.η = h.unit
-- Std.Data.DHashMap.Internal.Defs
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.IsHashSelf : {α : Type u} → {β : α → Type v} → [BEq α] → [Hashable α] → Array (Std.DHashMap.Internal.AssocList α β) → Prop
-- Mathlib.Probability.Kernel.RadonNikodym
ProbabilityTheory.Kernel.setLIntegral_rnDerivAux : ∀ {α : Type u_1} {γ : Type u_2} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ}
  [hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ] (κ η : ProbabilityTheory.Kernel α γ)
  [ProbabilityTheory.IsFiniteKernel κ] [ProbabilityTheory.IsFiniteKernel η] (a : α) {s : Set γ},
  MeasurableSet s → ∫⁻ (x : γ) in s, ENNReal.ofReal (κ.rnDerivAux (κ + η) a x) ∂(κ + η) a = (κ a) s
-- Mathlib.Tactic.NormNum.Result
Mathlib.Meta.NormNum.IsNat.to_eq : ∀ {α : Type u} [inst : AddMonoidWithOne α] {n : ℕ} {a a' : α}, Mathlib.Meta.NormNum.IsNat a n → ↑n = a' → a = a'
-- Init.Data.Range.Polymorphic.Map
Std.PRange.UpwardEnumerable.Map.PreservesLT.mk : ∀ {α : Type u_1} {β : Type u_2} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.PRange.UpwardEnumerable β]
  [inst_2 : LT α] [inst_3 : LT β] {f : Std.PRange.UpwardEnumerable.Map α β},
  (∀ {a b : α}, a < b ↔ f.toFun a < f.toFun b) → f.PreservesLT
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.Const.minEntry.match_1.eq_2 : ∀ {α : Type u_1} {β : Type u_2} (motive : (x : Std.DTreeMap.Internal.Impl α fun x => β) → x.isEmpty = false → Sort u_3)
  (size : ℕ) (k : α) (v : β) (size_1 : ℕ) (k_1 : α) (v_1 : β) (l r r_1 : Std.DTreeMap.Internal.Impl α fun x => β)
  (h :
    (Std.DTreeMap.Internal.Impl.inner size k v (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) r_1).isEmpty =
      false)
  (h_1 :
    (size : ℕ) →
      (k : α) →
        (v : β) →
          (r : Std.DTreeMap.Internal.Impl α fun x => β) →
            (x : (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r).isEmpty = false) →
              motive (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r) x)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β) →
          (l : Std.DTreeMap.Internal.Impl α fun x => β) →
            (size_2 : ℕ) →
              (k_2 : α) →
                (v_2 : β) →
                  (l_1 r : Std.DTreeMap.Internal.Impl α fun x => β) →
                    l = Std.DTreeMap.Internal.Impl.inner size_2 k_2 v_2 l_1 r →
                      (r_2 : Std.DTreeMap.Internal.Impl α fun x => β) →
                        (h :
                            (Std.DTreeMap.Internal.Impl.inner size k v
                                  (Std.DTreeMap.Internal.Impl.inner size_2 k_2 v_2 l_1 r) r_2).isEmpty =
                              false) →
                          motive
                            (Std.DTreeMap.Internal.Impl.inner size k v
                              (Std.DTreeMap.Internal.Impl.inner size_2 k_2 v_2 l_1 r) r_2)
                            h),
  (match Std.DTreeMap.Internal.Impl.inner size k v (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) r_1, h with
    | Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r, x => h_1 size k v r x
    | Std.DTreeMap.Internal.Impl.inner size k v (l@h:(Std.DTreeMap.Internal.Impl.inner size_2 k_2 v_2 l_1 r)) r_2,
      h_3 => h_2 size k v l size_2 k_2 v_2 l_1 r h r_2 h_3) =
    h_2 size k v (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) size_1 k_1 v_1 l r ⋯ r_1 h
-- Mathlib.NumberTheory.ModularForms.LevelOne.Basic
_private.Mathlib.NumberTheory.ModularForms.LevelOne.Basic.0.ModularFormClass.levelOne_nonpos_wt_const : ∀ {F : Type u_1} [inst : FunLike F UpperHalfPlane ℂ] {k : ℤ}
  [ModularFormClass F (Matrix.SpecialLinearGroup.mapGL ℝ).range k],
  k ≤ 0 → ∀ (f : F), ⇑f = Function.const UpperHalfPlane (UpperHalfPlane.cuspFunction 1 (⇑f) 0)
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.mkIso'.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {M N : C}
  [inst_2 : CategoryTheory.AddMonObj M] [inst_3 : CategoryTheory.AddMonObj N] (e : M ≅ N)
  [inst_4 : CategoryTheory.IsAddMonHom e.hom],
  CategoryTheory.AddMon.mkIso' e =
    { hom := { hom := e.hom, isAddMonHom_hom := inst_4 }, inv := { hom := e.inv, isAddMonHom_hom := ⋯ },
      hom_inv_id := ⋯, inv_hom_id := ⋯ }
-- Mathlib.MeasureTheory.Integral.IntegrableOn
ContinuousOn.integrableAt_nhdsWithin_of_isSeparable : ∀ {α : Type u_1} {E : Type u_5} {mα : MeasurableSpace α} [inst : NormedAddCommGroup E] [inst_1 : TopologicalSpace α]
  [TopologicalSpace.PseudoMetrizableSpace α] [OpensMeasurableSpace α] {μ : MeasureTheory.Measure α}
  [MeasureTheory.IsLocallyFiniteMeasure μ] {a : α} {t : Set α} {f : α → E},
  ContinuousOn f t →
    MeasurableSet t → TopologicalSpace.IsSeparable t → a ∈ t → MeasureTheory.IntegrableAtFilter f (nhdsWithin a t) μ
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithTerminal.ofCommaObject_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  (c : CategoryTheory.Comma (CategoryTheory.Functor.id (CategoryTheory.Functor C D)) (CategoryTheory.Functor.const C))
  (X : CategoryTheory.WithTerminal C),
  (CategoryTheory.WithTerminal.ofCommaObject c).obj X =
    match X with
    | CategoryTheory.WithTerminal.of x => c.left.obj x
    | CategoryTheory.WithTerminal.star => c.right
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise
Finpartition.card_filter_equitabilise_small : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α} {m a b : ℕ} (P : Finpartition s)
  (h : a * m + b * (m + 1) = s.card), m ≠ 0 → {u ∈ (Finpartition.equitabilise h).parts | u.card = m}.card = a
-- Mathlib.RingTheory.Valuation.Basic
Valuation.toAddValuation_apply : ∀ {R : Type u_3} {Γ₀ : Type u_5} [inst : Ring R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀)
  (r : R), (Valuation.toAddValuation v) r = OrderDual.toDual (Additive.ofMul (v r))
-- Mathlib.Order.Max
not_isMax_iff : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, ¬IsMax a ↔ ∃ b, a < b
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.Scheme.Hom.appIso_inv_appLE_assoc : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.IsOpenImmersion f] {U V : X.Opens}
  (e : V ≤ (TopologicalSpace.Opens.map f.base).obj ((AlgebraicGeometry.Scheme.Hom.opensFunctor f).obj U))
  {Z : CommRingCat} (h : X.presheaf.obj (Opposite.op V) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.appIso f U).inv
      (CategoryTheory.CategoryStruct.comp
        (AlgebraicGeometry.Scheme.Hom.appLE f ((AlgebraicGeometry.Scheme.Hom.opensFunctor f).obj U) V e) h) =
    CategoryTheory.CategoryStruct.comp (X.presheaf.map (CategoryTheory.homOfLE ⋯).op) h
-- Std.Time.DateTime
/-- Creates a new `DateTime` by adjusting the `hour` component.
 -/
Std.Time.DateTime.withHours : Std.Time.DateTime → Std.Time.Hour.Ordinal → Std.Time.DateTime
-- Mathlib.CategoryTheory.Monoidal.Cartesian.CommGrp_
CategoryTheory.yonedaCommGrpGrp_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (G : CategoryTheory.CommGrp C),
  CategoryTheory.yonedaCommGrpGrp.obj G = CategoryTheory.yonedaCommGrpGrpObj G
-- Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
/-- Coercion to a function as a `RingHom`.  -/
ContMDiffMap.coeFnRingHom : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {E' : Type u_3} →
            [inst_3 : NormedAddCommGroup E'] →
              [inst_4 : NormedSpace 𝕜 E'] →
                {H : Type u_4} →
                  [inst_5 : TopologicalSpace H] →
                    {I : ModelWithCorners 𝕜 E H} →
                      {H' : Type u_5} →
                        [inst_6 : TopologicalSpace H'] →
                          {I' : ModelWithCorners 𝕜 E' H'} →
                            {N : Type u_6} →
                              [inst_7 : TopologicalSpace N] →
                                [inst_8 : ChartedSpace H N] →
                                  {n : WithTop ℕ∞} →
                                    {R : Type u_10} →
                                      [inst_9 : CommRing R] →
                                        [inst_10 : TopologicalSpace R] →
                                          [inst_11 : ChartedSpace H' R] →
                                            [inst_12 : ContMDiffRing I' n R] → ContMDiffMap I I' N R n →+* N → R
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getEntryGT!_eq_get!_getEntryGT? : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] {t : Std.DTreeMap.Internal.Impl α β} {k : α}
  [inst_1 : Inhabited ((a : α) × β a)],
  Std.DTreeMap.Internal.Impl.getEntryGT! k t = (Std.DTreeMap.Internal.Impl.getEntryGT? k t).get!
-- Mathlib.Topology.Order.DenselyOrdered
nonempty_nhds_inter_Ioi : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [DenselyOrdered α] {x : α}
  {u : Set α}, u ∈ nhds x → ¬IsMax x → (u ∩ Set.Ioi x).Nonempty
-- Mathlib.Computability.ContextFreeGrammar
instReprContextFreeRule : {T : Type u_1} → {N : Type u_2} → [Repr T] → [Repr N] → Repr (ContextFreeRule T N)
-- Mathlib.Topology.Algebra.Group.Basic
Continuous.zpow : ∀ {G : Type w} {α : Type u} [inst : TopologicalSpace G] [inst_1 : Group G] [IsTopologicalGroup G]
  [inst_3 : TopologicalSpace α] {f : α → G}, Continuous f → ∀ (z : ℤ), Continuous (f ^ z)
-- Mathlib.Order.BoundedOrder.Basic
/-- An order is an `OrderBot` if it has a least element.
We state this using a data mixin, holding the value of `⊥` and the least element constraint.  -/
OrderBot : (α : Type u) → [LE α] → Type u
-- Mathlib.Topology.Separation.SeparatedNhds
SeparatedNhds.empty_left : ∀ {X : Type u_1} [inst : TopologicalSpace X] (s : Set X), SeparatedNhds ∅ s
-- Mathlib.Algebra.Algebra.Basic
Module.isTorsionFree_iff_algebraMap_injective : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] [IsDomain R] [IsDomain A],
  Module.IsTorsionFree R A ↔ Function.Injective ⇑(algebraMap R A)
-- Mathlib.Order.WithBot
WithBot.exists_coe_lt : ∀ {α : Type u_1} {a : α} [inst : Preorder α] {p : WithBot α → Prop}, (∃ x, ↑a < x ∧ p x) ↔ ∃ b, a < b ∧ p ↑b
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Expr.mul.injEq : ∀ (a b a_1 b_1 : Lean.Grind.CommRing.Expr), (a.mul b = a_1.mul b_1) = (a = a_1 ∧ b = b_1)
-- Init.Meta.Defs
Lean.TSyntax.instCoeNumLitPrio : Coe Lean.NumLit Lean.Prio
-- Init.Data.BitVec.Lemmas
BitVec.setWidth_append : ∀ {w v k : ℕ} {x : BitVec w} {y : BitVec v},
  BitVec.setWidth k (x ++ y) = if h : k ≤ v then BitVec.setWidth k y else BitVec.cast ⋯ (BitVec.setWidth (k - v) x ++ y)
-- Mathlib.Combinatorics.SimpleGraph.Hamiltonian
SimpleGraph.Walk.IsHamiltonian.getVert_surjective : ∀ {α : Type u_1} [inst : DecidableEq α] {G : SimpleGraph α} {a b : α} {p : G.Walk a b},
  p.IsHamiltonian → Function.Surjective p.getVert
-- Init.Data.List.MinMaxIdx
_private.Init.Data.List.MinMaxIdx.0.List.minIdxOn.match_3.eq_1 : ∀ {α : Type u_1} (motive : (xs : List α) → xs ≠ [] → Sort u_2) (y : α) (ys : List α) (h : y :: ys ≠ [])
  (h_1 : (y : α) → (ys : List α) → (h : y :: ys ≠ []) → motive (y :: ys) h),
  (match y :: ys, h with
    | y :: ys, h => h_1 y ys h) =
    h_1 y ys h
-- Mathlib.CategoryTheory.Category.Basic
CategoryTheory.instMonoId : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : C),
  CategoryTheory.Mono (CategoryTheory.CategoryStruct.id X)
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackFree
SheafOfModules.pullbackObjFreeIso_hom_naturality_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D}
  {F : CategoryTheory.Functor C D} {S : CategoryTheory.Sheaf J RingCat} {R : CategoryTheory.Sheaf K RingCat}
  [inst_2 : F.IsContinuous J K] (φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R)
  [inst_3 : (SheafOfModules.pushforward φ).IsRightAdjoint] [inst_4 : CategoryTheory.HasWeakSheafify J AddCommGrpCat]
  [inst_5 : CategoryTheory.HasWeakSheafify K AddCommGrpCat] [inst_6 : J.WEqualsLocallyBijective AddCommGrpCat]
  [inst_7 : K.WEqualsLocallyBijective AddCommGrpCat] [inst_8 : F.Final] {I J_1 : Type u} (f : I → J_1)
  {Z : SheafOfModules R} (h : SheafOfModules.free J_1 ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((SheafOfModules.pullback φ).map (SheafOfModules.freeMap f))
      (CategoryTheory.CategoryStruct.comp (SheafOfModules.pullbackObjFreeIso φ J_1).hom h) =
    CategoryTheory.CategoryStruct.comp (SheafOfModules.pullbackObjFreeIso φ I).hom
      (CategoryTheory.CategoryStruct.comp (SheafOfModules.freeMap f) h)
-- Mathlib.Analysis.Distribution.FourierMultiplier
TemperedDistribution.lineDeriv_eq_fourierMultiplierCLM : ∀ {E : Type u_3} {F : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F]
  [inst_2 : InnerProductSpace ℝ E] [inst_3 : NormedSpace ℂ F] [inst_4 : FiniteDimensional ℝ E]
  [inst_5 : MeasurableSpace E] [inst_6 : BorelSpace E] (m : E) (f : TemperedDistribution E F),
  LineDeriv.lineDerivOp m f =
    (2 * ↑Real.pi * Complex.I) • (TemperedDistribution.fourierMultiplierCLM F fun x => ↑(inner ℝ x m)) f
-- Mathlib.Algebra.Category.MonCat.Basic
/-- Turn a morphism in `AddMonCat` back into an `AddMonoidHom`.  -/
AddMonCat.Hom.hom : {X Y : AddMonCat} → X.Hom Y → ↑X →+ ↑Y
-- Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
SSet.PtSimplex.MulStruct.δ_map_of_lt_assoc : ∀ {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} {f g fg : X.PtSimplex n x} {i : Fin n}
  (self : f.MulStruct g fg i),
  ∀ j < i.castSucc.castSucc,
    ∀ {Z : SSet} (h : X ⟶ Z),
      CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ j) (CategoryTheory.CategoryStruct.comp self.map h) =
        CategoryTheory.CategoryStruct.comp (SSet.const x) h
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.triangle_assoc_comp_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X Y : C),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.associator X (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) Y).inv
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom Y) =
    CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.MonoidalCategoryStruct.leftUnitor Y).hom
-- Mathlib.RingTheory.Extension.Cotangent.BaseChange
Algebra.Extension.tensorH1CotangentOfFlat_tmul : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : Algebra.Extension R S) (T : Type u_3) [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Module.Flat R T]
  (t : T) (x : P.H1Cotangent),
  (P.tensorH1CotangentOfFlat T) (t ⊗ₜ[R] x) =
    t • (Algebra.Extension.H1Cotangent.map (Algebra.Extension.toBaseChange T)) x
-- Mathlib.Algebra.Category.Ring.Topology
CommRingCat.HomTopology.mvPolynomialHomeomorph.congr_simp : ∀ (σ : Type v) (R A : CommRingCat) [inst : TopologicalSpace ↑R] [inst_1 : IsTopologicalRing ↑R],
  CommRingCat.HomTopology.mvPolynomialHomeomorph σ R A = CommRingCat.HomTopology.mvPolynomialHomeomorph σ R A
-- Mathlib.Topology.Category.Profinite.Extend
/-- Given a cone in `Profinite`, consisting of finite sets and indexed by a cofiltered category,
we obtain a functor from the opposite of the indexing category to
`CostructuredArrow toProfinite.op ⟨c.pt⟩`.
 -/
Profinite.Extend.functorOp : {I : Type u} →
  [inst : CategoryTheory.SmallCategory I] →
    {F : CategoryTheory.Functor I FintypeCat} →
      (c : CategoryTheory.Limits.Cone (F.comp FintypeCat.toProfinite)) →
        CategoryTheory.Functor Iᵒᵖ (CategoryTheory.CostructuredArrow FintypeCat.toProfinite.op (Opposite.op c.pt))
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toList_rcc_eq_nil_iff : ∀ {m n : ℤ}, (m...=n).toList = [] ↔ n < m
-- Mathlib.RingTheory.Multiplicity
multiplicity_zero_eq_zero_of_ne_zero : ∀ {α : Type u_1} [inst : MonoidWithZero α] (a : α), a ≠ 0 → multiplicity 0 a = 0
-- Mathlib.RingTheory.PowerSeries.Order
/-- The order of the product of two formal power series
is at least the sum of their orders.  -/
PowerSeries.le_order_mul : ∀ {R : Type u_1} [inst : Semiring R] (φ ψ : PowerSeries R), φ.order + ψ.order ≤ (φ * ψ).order
-- Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic
/-- The second leg of a pushout cocone is a normal epimorphism if the right component is too.

See also `pushout.sndOfEpi` for the basic epimorphism version, and
`normalOfIsPushoutFstOfNormal` for the flipped version.
 -/
CategoryTheory.normalOfIsPushoutSndOfNormal : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {P Q R S : C} →
        {f : P ⟶ Q} →
          {g : P ⟶ R} →
            {h : Q ⟶ S} →
              {k : R ⟶ S} →
                [gn : CategoryTheory.NormalEpi g] →
                  (comm : CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g k) →
                    CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.PushoutCocone.mk h k comm) →
                      CategoryTheory.NormalEpi h
-- Mathlib.AlgebraicTopology.SimplicialNerve
CategoryTheory.SimplicialThickening.hom_ext : ∀ {J : Type u_1} [inst : LinearOrder J] (i j : CategoryTheory.SimplicialThickening J) (x y : i ⟶ j),
  (∀ (t : J), t ∈ x.I ↔ t ∈ y.I) → x = y
-- Mathlib.AlgebraicGeometry.Limits
AlgebraicGeometry.isOpenImmersion_sigmaDesc : ∀ {σ : Type v} (g : σ → AlgebraicGeometry.Scheme) [inst : Small.{u, v} σ] {X : AlgebraicGeometry.Scheme}
  (α : (i : σ) → g i ⟶ X) [∀ (i : σ), AlgebraicGeometry.IsOpenImmersion (α i)],
  Pairwise (Function.onFun Disjoint fun x => Set.range ⇑(α x)) →
    AlgebraicGeometry.IsOpenImmersion (CategoryTheory.Limits.Sigma.desc α)
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.X_pow_mul_inj : ∀ {R : Type u_1} [inst : Semiring R] {k : ℕ} {φ ψ : PowerSeries R},
  PowerSeries.X ^ k * φ = PowerSeries.X ^ k * ψ ↔ φ = ψ
-- Mathlib.RingTheory.Localization.Away.Basic
IsLocalization.away_of_isUnit_of_bijective : ∀ {R : Type u_4} (S : Type u_5) [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S] {r : R},
  IsUnit r → Function.Bijective ⇑(algebraMap R S) → IsLocalization.Away r S
-- Aesop.RuleTac.Forward
_private.Aesop.RuleTac.Forward.0.Aesop.RuleTac.makeForwardHypProofs.isRedundant : Lean.Expr → Aesop.RuleTac.ForwardM Bool
-- Lean.Elab.Tactic.Location
Lean.Elab.Tactic.expandLocation : Lean.Syntax → Lean.Elab.Tactic.Location
-- Mathlib.Topology.Metrizable.Basic
TopologicalSpace.pseudoMetrizableSpace_prod : ∀ {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [TopologicalSpace.PseudoMetrizableSpace X] [TopologicalSpace.PseudoMetrizableSpace Y],
  TopologicalSpace.PseudoMetrizableSpace (X × Y)
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.translationNumber_zpow : ∀ (f : CircleDeg1Liftˣ) (n : ℤ), (↑(f ^ n)).translationNumber = ↑n * (↑f).translationNumber
-- Mathlib.Algebra.Lie.Solvable
LieAlgebra.abelian_of_solvable_ideal_eq_bot_iff : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (I : LieIdeal R L)
  [h : LieAlgebra.IsSolvable ↥I], LieAlgebra.derivedAbelianOfIdeal I = ⊥ ↔ I = ⊥
-- Mathlib.Algebra.Group.Pi.Lemmas
/-- The additive monoid homomorphism including a single additive monoid into a dependent family
of additive monoids, as functions supported at a point.

This is the `AddMonoidHom` version of `Pi.single`.  -/
AddMonoidHom.single : {I : Type u} →
  (f : I → Type v) → [DecidableEq I] → [inst : (i : I) → AddZeroClass (f i)] → (i : I) → f i →+ (i : I) → f i
-- Mathlib.Algebra.GroupWithZero.Units.Basic
/-- An alternative version of `Units.exists0`. This one is useful if Lean cannot
figure out `p` when using `Units.exists0` from right to left.  -/
Units.exists0' : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {p : (g : G₀) → g ≠ 0 → Prop}, (∃ g, ∃ (hg : g ≠ 0), p g hg) ↔ ∃ g, p ↑g ⋯
-- Mathlib.Analysis.Calculus.Deriv.Inverse
/-- If a function frequently (in `𝓝[≠] x`) takes values in a set `t` that does not
accumulate at `f x`, then its derivative at `x` equals zero,
either because it has derivative zero or because it isn't differentiable at this point.  -/
deriv_zero_of_frequently_mem : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {x : 𝕜} (t : Set F),
  ¬AccPt (f x) (Filter.principal t) → (∃ᶠ (y : 𝕜) in nhdsWithin x {x}ᶜ, f y ∈ t) → deriv f x = 0
-- Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv
Complex.isOpenMap_exp : IsOpenMap Complex.exp
-- Lean.ProjFns
/-- If `projName` is the name of a projection function, return the associated structure name  -/
Lean.Environment.getProjectionStructureName? : Lean.Environment → Lean.Name → Option Lean.Name
-- Lean.Meta.Tactic.Ext
Lean.Meta.Ext.ExtTheorem.mk.injEq : ∀ (declName : Lean.Name) (priority : ℕ) (keys : Array Lean.Meta.DiscrTree.Key) (declName_1 : Lean.Name) (priority_1 : ℕ)
  (keys_1 : Array Lean.Meta.DiscrTree.Key),
  ({ declName := declName, priority := priority, keys := keys } =
      { declName := declName_1, priority := priority_1, keys := keys_1 }) =
    (declName = declName_1 ∧ priority = priority_1 ∧ keys = keys_1)
-- Init.Grind.Config
/-- When `true`, use reducible transparency when trying to close goals.
In this setting, only declarations marked with `@[reducible]` are unfolded during
definitional equality tests.

This option does not affect the canonicalizer or how theorem patterns are internalized;
reducible declarations are always unfolded in those contexts.
 -/
Lean.Grind.Config.reducible : Lean.Grind.Config → Bool