mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.TensorProduct.Decomposition
DirectSum.decomposeTensorEquiv_apply : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (ℳ : ι → Submodule R M) (N : Type u_5) [inst_3 : AddCommMonoid N] [inst_4 : Module R N] [inst_5 : DecidableEq ι]
  [inst_6 : DirectSum.Decomposition ℳ] {i : ι} (x : TensorProduct R (↥(ℳ i)) N),
  (DirectSum.decomposeTensorEquiv ℳ N i) x = ⟨(LinearMap.rTensor N (ℳ i).subtype) x, ⋯⟩
-- Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Ordinal.lsub_lt_ord : ∀ {ι : Type u} {f : ι → Ordinal.{u}} {c : Ordinal.{u}},
  Cardinal.mk ι < c.cof → (∀ (i : ι), f i < c) → Ordinal.lsub f < c
-- Mathlib.Analysis.Normed.Group.Continuity
SeminormedGroup.uniformCauchySeqOn_iff_tendstoUniformlyOn_one : ∀ {ι : Type u_2} {κ : Type u_3} {G : Type u_6} [inst : SeminormedGroup G] {f : ι → κ → G} {s : Set κ} {l : Filter ι},
  UniformCauchySeqOn f l s ↔ TendstoUniformlyOn (fun n z => (f n.1 z)⁻¹ * f n.2 z) 1 (l ×ˢ l) s
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.π_comp_H2Iso_inv_apply : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G)
  (x : ↑(groupHomology.shortComplexH2 A).moduleCatLeftHomologyData.K),
  (CategoryTheory.ConcreteCategory.hom (groupHomology.H2Iso A).inv)
      ((CategoryTheory.ConcreteCategory.hom (groupHomology.shortComplexH2 A).moduleCatLeftHomologyData.π) x) =
    (CategoryTheory.ConcreteCategory.hom (groupHomology.H2π A)) x
-- Mathlib.RingTheory.Algebraic.Integral
IsAlgebraic.restrictScalars : ∀ (R : Type u_1) {S : Type u_2} {A : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Ring A]
  [inst_3 : Algebra R S] [inst_4 : Algebra R A] [inst_5 : Algebra S A] [IsScalarTower R S A] [NoZeroDivisors S]
  [Algebra.IsAlgebraic R S] {a : A}, IsAlgebraic S a → IsAlgebraic R a
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Extract
Std.Tactic.BVDecide.BVExpr.bitblast.denote_blastExtract : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {newWidth : ℕ} (aig : Std.Sat.AIG α)
  (target : Std.Tactic.BVDecide.BVExpr.bitblast.ExtractTarget aig newWidth) (assign : α → Bool) (idx : ℕ)
  (hidx : idx < newWidth),
  ⟦assign,
      { aig := (Std.Tactic.BVDecide.BVExpr.bitblast.blastExtract aig target).aig,
        ref := (Std.Tactic.BVDecide.BVExpr.bitblast.blastExtract aig target).vec.get idx hidx }⟧ =
    if h : target.start + idx < target.w then ⟦assign, { aig := aig, ref := target.vec.get (target.start + idx) h }⟧
    else false
-- Mathlib.Topology.Continuous
DenseRange.closure_range : ∀ {X : Type u_1} [inst : TopologicalSpace X] {α : Type u_4} {f : α → X}, DenseRange f → closure (Set.range f) = Set.univ
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
CategoryTheory.Limits.preservesColimitsOfShape_iff_of_natIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] {F G : CategoryTheory.Functor C D} (h : F ≅ G),
  CategoryTheory.Limits.PreservesColimitsOfShape J F ↔ CategoryTheory.Limits.PreservesColimitsOfShape J G
-- Mathlib.RingTheory.Valuation.Basic
Valuation.not_isNontrivial_one : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀] [inst_2 : IsDomain R]
  [inst_3 : DecidablePred fun x => x = 0], ¬Valuation.IsNontrivial 1
-- Mathlib.Analysis.Normed.Module.Alternating.Basic
/-- Flip arguments in `f : F →L[𝕜] E [⋀^ι]→L[𝕜] G` to get `⋀^ι⟮𝕜; E; F →L[𝕜] G⟯`  -/
ContinuousLinearMap.flipAlternating : {𝕜 : Type u} →
  {E : Type wE} →
    {F : Type wF} →
      {G : Type wG} →
        {ι : Type v} →
          [inst : NontriviallyNormedField 𝕜] →
            [inst_1 : SeminormedAddCommGroup E] →
              [inst_2 : NormedSpace 𝕜 E] →
                [inst_3 : SeminormedAddCommGroup F] →
                  [inst_4 : NormedSpace 𝕜 F] →
                    [inst_5 : SeminormedAddCommGroup G] →
                      [inst_6 : NormedSpace 𝕜 G] → [Fintype ι] → (F →L[𝕜] E [⋀^ι]→L[𝕜] G) → E [⋀^ι]→L[𝕜] (F →L[𝕜] G)
-- Mathlib.Topology.Algebra.Module.Determinant
ContinuousLinearMap.det_toSpanSingleton : ∀ {𝕜 : Type u_1} [inst : CommRing 𝕜] [inst_1 : TopologicalSpace 𝕜] [inst_2 : ContinuousMul 𝕜] (v : 𝕜),
  (ContinuousLinearMap.toSpanSingleton 𝕜 v).det = v
-- Mathlib.CategoryTheory.GradedObject.Bifunctor
/-- The maps `mapBifunctorMapObj F p X₁ Y₁ ⟶ mapBifunctorMapObj F p X₂ Y₂` which express
the functoriality of `mapBifunctorMapObj`, see `mapBifunctorMap`.  -/
CategoryTheory.GradedObject.mapBifunctorMapMap : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {C₃ : Type u_3} →
      [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] →
            (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)) →
              {I : Type u_4} →
                {J : Type u_5} →
                  {K : Type u_6} →
                    (p : I × J → K) →
                      {X₁ X₂ : CategoryTheory.GradedObject I C₁} →
                        (X₁ ⟶ X₂) →
                          {Y₁ Y₂ : CategoryTheory.GradedObject J C₂} →
                            (Y₁ ⟶ Y₂) →
                              [inst_3 : (((CategoryTheory.GradedObject.mapBifunctor F I J).obj X₁).obj Y₁).HasMap p] →
                                [inst_4 : (((CategoryTheory.GradedObject.mapBifunctor F I J).obj X₂).obj Y₂).HasMap p] →
                                  CategoryTheory.GradedObject.mapBifunctorMapObj F p X₁ Y₁ ⟶
                                    CategoryTheory.GradedObject.mapBifunctorMapObj F p X₂ Y₂
-- Mathlib.Order.Basic
Subtype.preorder : {α : Type u_2} → [Preorder α] → (p : α → Prop) → Preorder (Subtype p)
-- Mathlib.Algebra.Ring.Periodic
/-- **Alias** of the forward direction of `Function.periodic_iterate_iff`.

---

The iterates `a`, `f a`, `f^[2] a` etc form a periodic sequence with period `n`
iff `a` is a periodic point for `f`.  -/
Function.Periodic.isPeriodicPt : ∀ {α : Type u_1} {f : α → α} {n : ℕ} {a : α}, Function.Periodic (fun x => f^[x] a) n → Function.IsPeriodicPt f n a
-- Mathlib.RingTheory.DividedPowers.SubDPIdeal
DividedPowers.SubDPIdeal.instSupSet : {A : Type u_1} → [inst : CommSemiring A] → {I : Ideal A} → {hI : DividedPowers I} → SupSet hI.SubDPIdeal
-- Mathlib.Topology.UniformSpace.Equicontinuity
/-- Given `u : α → γ` a uniform inducing map, a family `𝓕 : ι → β → α` is uniformly equicontinuous
iff the family `𝓕'`, obtained by composing each function of `𝓕` by `u`, is uniformly
equicontinuous.  -/
IsUniformInducing.uniformEquicontinuous_iff : ∀ {ι : Type u_1} {α : Type u_6} {β : Type u_8} {γ : Type u_10} [uα : UniformSpace α] [uβ : UniformSpace β]
  [uγ : UniformSpace γ] {F : ι → β → α} {u : α → γ},
  IsUniformInducing u → (UniformEquicontinuous F ↔ UniformEquicontinuous ((fun x => u ∘ x) ∘ F))
-- Lean.Elab.Tactic.BuiltinTactic
Lean.Elab.Tactic.evalIntroMatch : Lean.Elab.Tactic.Tactic
-- Mathlib.Tactic.SudoSetOption
_private.Mathlib.Tactic.SudoSetOption.0.setOption : {m : Type → Type} → [Monad m] → [Lean.MonadError m] → Lean.Syntax → Lean.Syntax → Lean.Options → m Lean.Options
-- Mathlib.Analysis.Convex.Topology
closure_openSegment : ∀ {𝕜 : Type u_2} {E : Type u_3} [inst : Ring 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [DenselyOrdered 𝕜]
  [inst_4 : PseudoMetricSpace 𝕜] [OrderTopology 𝕜] [ProperSpace 𝕜] [CompactIccSpace 𝕜] [inst_8 : AddCommGroup E]
  [inst_9 : TopologicalSpace E] [T2Space E] [ContinuousAdd E] [inst_12 : Module 𝕜 E] [ContinuousSMul 𝕜 E] (x y : E),
  closure (openSegment 𝕜 x y) = segment 𝕜 x y
-- Mathlib.Analysis.Normed.Group.Uniform
/-- **Alias** of the reverse direction of `lipschitzOnWith_neg_iff`. -/
LipschitzOnWith.neg : ∀ {α : Type u_4} {E : Type u_5} [inst : SeminormedAddCommGroup E] [inst_1 : PseudoEMetricSpace α] {K : NNReal}
  {f : α → E} {s : Set α}, LipschitzOnWith K f s → LipschitzOnWith K (-f) s
-- Mathlib.Probability.Process.Adapted
MeasureTheory.IsProgressive.mul : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] {f : MeasureTheory.Filtration ι m}
  {β : Type u_3} {u v : ι → Ω → β} {mi : MeasurableSpace ι} {mβ : MeasurableSpace β} [inst_1 : Mul β]
  [MeasurableMul₂ β],
  MeasureTheory.IsProgressive f u →
    MeasureTheory.IsProgressive f v → MeasureTheory.IsProgressive f fun i ω => u i ω * v i ω
-- Mathlib.MeasureTheory.Group.Convolution
MeasureTheory.Measure.dirac_mconv_dirac : ∀ {M : Type u_1} [inst : Monoid M] [inst_1 : MeasurableSpace M] [MeasurableMul₂ M] (x y : M),
  (MeasureTheory.Measure.dirac x).mconv (MeasureTheory.Measure.dirac y) = MeasureTheory.Measure.dirac (x * y)
-- Mathlib.Probability.HasCondDistrib
ProbabilityTheory.HasCondDistrib.comp_left : ∀ {Ω : Type u_1} {𝓧 : Type u_2} {𝓨 : Type u_3} {𝓩 : Type u_4} {mΩ : MeasurableSpace Ω} {m𝓧 : MeasurableSpace 𝓧}
  {m𝓨 : MeasurableSpace 𝓨} {m𝓩 : MeasurableSpace 𝓩} {P : MeasureTheory.Measure Ω} {X : Ω → 𝓧} {Y : Ω → 𝓨}
  {κ : ProbabilityTheory.Kernel 𝓧 𝓨} [MeasureTheory.SFinite P] [ProbabilityTheory.IsSFiniteKernel κ],
  ProbabilityTheory.HasCondDistrib Y X κ P →
    ∀ {f : 𝓨 → 𝓩}, Measurable f → ProbabilityTheory.HasCondDistrib (f ∘ Y) X (κ.map f) P
-- Mathlib.FieldTheory.IntermediateField.ExtendRight
IntermediateField.algebraMap_extendRightEquiv : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (F : IntermediateField K L)
  (M : Type u_3) [inst_3 : Field M] [inst_4 : Algebra K M] [inst_5 : Algebra L M] [inst_6 : IsScalarTower K L M]
  (a : ↥F), (algebraMap (↥(F.extendRight M)) M) ((F.extendRightEquiv M) a) = (algebraMap (↥F) M) a
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidHom.coe_comp : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  [inst_3 : MulOneClass α] [inst_4 : MulOneClass β] [inst_5 : MulOneClass γ] (f : β →*o γ) (g : α →*o β),
  ⇑(f.comp g) = ⇑f ∘ ⇑g
-- Mathlib.NumberTheory.AlmostPrime
Nat.IsAlmostPrime.isAtMost : ∀ {k l n : ℕ}, k.IsAlmostPrime n → k ≤ l → l.IsAtMostAlmostPrime n
-- Init.Data.List.Basic
List.Lex.below : {α : Type u} →
  {r : α → α → Prop} →
    {motive : (as bs : List α) → List.Lex r as bs → Prop} → {as bs : List α} → List.Lex r as bs → Prop
-- Mathlib.Data.Finset.Prod
Finset.offDiag_card : ∀ {α : Type u_1} (s : Finset α), s.offDiag.card = s.card * s.card - s.card
-- Mathlib.LinearAlgebra.RootSystem.IsValuedIn
/-- A variant of `RootPairing.coxeterWeight` for root pairings which are valued in a smaller set of
coefficients.

Note that it is uniquely-defined only when the map `S → R` is injective, i.e., when we have
`[FaithfulSMul S R]`.  -/
RootPairing.coxeterWeightIn : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_4} →
      {N : Type u_5} →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] →
              [inst_3 : AddCommGroup N] →
                [inst_4 : Module R N] →
                  (P : RootPairing ι R M N) →
                    (S : Type u_7) → [inst_5 : CommRing S] → [inst_6 : Algebra S R] → [P.IsValuedIn S] → ι → ι → S
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.size_diff!_le_size_left : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  m₁.WF → m₂.WF → (m₁.diff! m₂).size ≤ m₁.size
-- Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Ideal.height_le_card_of_mem_minimalPrimes_span : ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] {p : Ideal R} {s : Set R},
  s.Finite → p ∈ (Ideal.span s).minimalPrimes → p.height ≤ ↑s.ncard
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.get?.congr_simp : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} [inst : LawfulBEq α] (m m_1 : Std.DHashMap α β),
  m = m_1 → ∀ (a : α), m.get? a = m_1.get? a
-- Mathlib.Topology.EMetricSpace.Lipschitz
/-- The inclusion of a subset is 1-Lipschitz.  -/
LipschitzWith.subtype_val : ∀ {α : Type u} [inst : PseudoEMetricSpace α] (s : Set α), LipschitzWith 1 Subtype.val
-- Mathlib.Algebra.GroupWithZero.WithZero
WithZero.coe_pow : ∀ {α : Type u_1} [inst : One α] [inst_1 : Pow α ℕ] (a : α) (n : ℕ), ↑(a ^ n) = ↑a ^ n
-- Mathlib.Order.WithBot
WithBot.forall_coe_le : ∀ {α : Type u_1} {a : α} [inst : Preorder α] {p : WithBot α → Prop},
  (∀ (x : WithBot α), ↑a ≤ x → p x) ↔ ∀ (b : α), a ≤ b → p ↑b
-- Lean.Elab.PreDefinition.TerminationHint
Lean.Elab.PartialFixpointType : Type
-- Std.Data.TreeMap.Basic
/-- Tries to retrieve the smallest key in the tree map, returning `none` if the map is empty.
 -/
Std.TreeMap.minKey? : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap α β cmp → Option α
-- Mathlib.Algebra.Prime.Lemmas
IsSquare.not_prime : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] [IsCancelMulZero M] {a : M}, IsSquare a → ¬Prime a
-- Mathlib.Condensed.Light.Sequence
_private.Mathlib.Condensed.Light.Sequence.0.InternalProjectivityProof.π_r_apply : ∀ {S : Type u_1} {T : Type u_2} {X : Type u_3} (π : T → S × Option X) (σ : Option X → S → T)
  (x : ↑(InternalProjectivityProof.fibres✝ π σ)), InternalProjectivityProof.π_r✝ π σ x = π ↑x
-- Lean.Meta.Tactic.Simp.Attr
Lean.Meta.sevalSimpExtension : Lean.Meta.SimpExtension
-- Mathlib.Algebra.Module.LinearMap.Polynomial
Matrix.toMvPolynomial_isHomogeneous : ∀ {m : Type u_1} {n : Type u_2} {R : Type u_4} [inst : Fintype n] [inst_1 : CommSemiring R] (M : Matrix m n R) (i : m),
  (M.toMvPolynomial i).IsHomogeneous 1
-- Mathlib.Data.Set.Finite.Basic
Set.Finite.toFinset_union : ∀ {α : Type u} {s t : Set α} [inst : DecidableEq α] (hs : s.Finite) (ht : t.Finite) (h : (s ∪ t).Finite),
  h.toFinset = hs.toFinset ∪ ht.toFinset
-- Mathlib.MeasureTheory.Measure.GiryMonad
Measurable.measure_of_isPiSystem : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : α → MeasureTheory.Measure β}
  [∀ (a : α), MeasureTheory.IsFiniteMeasure (μ a)] {S : Set (Set β)},
  mβ = MeasurableSpace.generateFrom S →
    IsPiSystem S → (∀ s ∈ S, Measurable fun a => (μ a) s) → (Measurable fun a => (μ a) Set.univ) → Measurable μ
-- Init.Data.SInt.Lemmas
Int16.ofInt_eq_ofIntLE_div : ∀ {a b : ℤ} (ha₁ : Int16.minValue.toInt ≤ a) (ha₂ : a ≤ Int16.maxValue.toInt) (hb₁ : Int16.minValue.toInt ≤ b)
  (hb₂ : b ≤ Int16.maxValue.toInt), Int16.ofInt (a.tdiv b) = Int16.ofIntLE a ha₁ ha₂ / Int16.ofIntLE b hb₁ hb₂
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getD_modify : ∀ {α : Type u} {instOrd : Ord α} [Std.TransOrd α] {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β},
  t.WF →
    ∀ {k k' : α} {fallback : β} {f : β → β},
      Std.DTreeMap.Internal.Impl.Const.getD (Std.DTreeMap.Internal.Impl.Const.modify k f t) k' fallback =
        if compare k k' = Ordering.eq then (Option.map f (Std.DTreeMap.Internal.Impl.Const.get? t k)).getD fallback
        else Std.DTreeMap.Internal.Impl.Const.getD t k' fallback
-- Mathlib.Analysis.InnerProductSpace.TwoDim
/-- An isometric automorphism of an oriented real inner product space of dimension 2 (usual notation
`J`). This automorphism squares to -1. We will define rotations in such a way that this
automorphism is equal to rotation by 90 degrees.  -/
Orientation.rightAngleRotation : {E : Type u_2} →
  [inst : NormedAddCommGroup E] →
    [inst_1 : InnerProductSpace ℝ E] → [Fact (Module.finrank ℝ E = 2)] → Orientation ℝ E (Fin 2) → E ≃ₗᵢ[ℝ] E
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated
/-- The constant edge on a `0`-simplex.  -/
SSet.Truncated.Edge.id : {X : SSet.Truncated 2} →
  (x : X.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge._proof_1 })) → SSet.Truncated.Edge x x
-- Mathlib.CategoryTheory.Monoidal.Mon
/-- Implementation of `Mon.equivLaxMonoidalFunctorPUnit`.  -/
CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidalObj : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      CategoryTheory.Mon C → CategoryTheory.Functor (CategoryTheory.Discrete PUnit.{w + 1}) C
-- Mathlib.Dynamics.PeriodicPts.Defs
/-- A point `x` is a periodic point of `f : α → α` of period `n` if `f^[n] x = x`.
Note that we do not require `0 < n` in this definition. Many theorems about periodic points
need this assumption.  -/
Function.IsPeriodicPt : {α : Type u_1} → (α → α) → ℕ → α → Prop
-- Mathlib.Order.SetDissipate
Set.dissipate_def : ∀ {α : Type u_1} {β : Type u_2} {s : α → Set β} [inst : LE α] {x : α}, Set.dissipate s x = ⋂ y, ⋂ (_ : y ≤ x), s y
-- Lean.Environment
Lean.Kernel.Exception.appTypeMismatch.injEq : ∀ (env : Lean.Kernel.Environment) (lctx : Lean.LocalContext) (app funType argType : Lean.Expr)
  (env_1 : Lean.Kernel.Environment) (lctx_1 : Lean.LocalContext) (app_1 funType_1 argType_1 : Lean.Expr),
  (Lean.Kernel.Exception.appTypeMismatch env lctx app funType argType =
      Lean.Kernel.Exception.appTypeMismatch env_1 lctx_1 app_1 funType_1 argType_1) =
    (env = env_1 ∧ lctx = lctx_1 ∧ app = app_1 ∧ funType = funType_1 ∧ argType = argType_1)
-- Mathlib.RingTheory.Perfection
Perfection.extMonoid_iff : ∀ {M : Type u_1} [inst : CommMonoid M] {p : ℕ} {f g : Perfection M p},
  f = g ↔ ∀ (n : ℕ), (Perfection.coeffMonoidHom M p n) f = (Perfection.coeffMonoidHom M p n) g
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getElem_union_of_not_mem_left : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} (not_mem : k ∉ m₁) {h' : k ∈ m₁ ∪ m₂}, (m₁ ∪ m₂)[k] = m₂[k]
-- Mathlib.Algebra.Order.Field.Basic
abs_one_div : ∀ {α : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] (a : α), |1 / a| = 1 / |a|
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.isEmpty_eq_size_beq_zero : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp}, t.isEmpty = (t.size == 0)
-- Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
IsIntegrallyClosed.isIntegral_iff : ∀ {R : Type u_1} [inst : CommRing R] {K : Type u_3} [inst_1 : CommRing K] [inst_2 : Algebra R K]
  [ifr : IsFractionRing R K] [IsIntegrallyClosed R] {x : K}, IsIntegral R x ↔ ∃ y, (algebraMap R K) y = x
-- Init.SizeOf
Lean.SourceInfo.synthetic.sizeOf_spec : ∀ (pos endPos : String.Pos.Raw) (canonical : optParam Bool false),
  sizeOf (Lean.SourceInfo.synthetic pos endPos canonical) = 1 + sizeOf pos + sizeOf endPos + sizeOf canonical
-- Mathlib.RingTheory.Ideal.GoingDown
/-- An `R`-algebra `S` satisfies `Algebra.HasGoingDown R S` if for every pair of
prime ideals `p ≤ q` of `R` with `Q` a prime of `S` lying above `q`, there exists a
prime `P ≤ Q` of `S` lying above `p`.

The condition only asks for `<` which is easier to prove, use
`Ideal.exists_ideal_le_liesOver_of_le` for applying it.
 -/
Algebra.HasGoingDown : (R : Type u_1) → (S : Type u_2) → [inst : CommRing R] → [inst_1 : CommRing S] → [Algebra R S] → Prop
-- Lean.Elab.App
/-- Auxiliary function for `propagateExpectedType`. Returns the inferred type of the function
application, if enough information is currently known.
 -/
_private.Lean.Elab.App.0.Lean.Elab.Term.ElabAppArgs.getResultingType? : Lean.Elab.Term.ElabAppArgs.M (Option Lean.Expr)
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.nonUnitalNonAssocRing.eq_1 : ∀ {R : Type u_1} {M : Type u_4} [inst : Ring R] [inst_1 : Mul M],
  MonoidAlgebra.nonUnitalNonAssocRing =
    { toAddCommGroup := MonoidAlgebra.addCommGroup, toMul := MonoidAlgebra.nonUnitalNonAssocSemiring.toMul,
      left_distrib := ⋯, right_distrib := ⋯, zero_mul := ⋯, mul_zero := ⋯ }
-- Mathlib.CategoryTheory.Sites.Sheafification
CategoryTheory.instHasWeakSheafifyOfHasSheafify : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u₂)
  [inst_1 : CategoryTheory.Category.{v₂, u₂} A] [CategoryTheory.HasSheafify J A], CategoryTheory.HasWeakSheafify J A
-- Std.Time.Notation
_private.Std.Time.Notation.0.Std.Time.syntaxNat : ℕ → Lean.MacroM (Lean.TSyntax `term)
-- Mathlib.Data.List.Dedup
List.dedup_cons' : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (l : List α),
  (a :: l).dedup = if a ∈ l.dedup then l.dedup else a :: l.dedup
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.ValueGroupWithZero.lift_mk : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R] {α : Sort u_2}
  (f : R → ↥(ValuativeRel.posSubmonoid R) → α)
  (hf : ∀ (x y : R) (t s : ↥(ValuativeRel.posSubmonoid R)), x * ↑t ≤ᵥ y * ↑s → y * ↑s ≤ᵥ x * ↑t → f x s = f y t) (x : R)
  (y : ↥(ValuativeRel.posSubmonoid R)),
  ValuativeRel.ValueGroupWithZero.lift f hf (ValuativeRel.ValueGroupWithZero.mk x y) = f x y
-- Mathlib.RingTheory.Ideal.Lattice
Ideal.mem_sup_right : ∀ {R : Type u} [inst : Semiring R] {S T : Ideal R} {x : R}, x ∈ T → x ∈ S ⊔ T
-- Mathlib.LinearAlgebra.Matrix.Kronecker
Matrix.kronecker_smul : ∀ {R : Type u_1} {α : Type u_3} {l : Type u_9} {m : Type u_10} {n : Type u_11} {p : Type u_12} [inst : Mul α]
  [inst_1 : SMul R α] [SMulCommClass R α α] (r : R) (A : Matrix l m α) (B : Matrix n p α),
  Matrix.kroneckerMap (fun x1 x2 => x1 * x2) A (r • B) = r • Matrix.kroneckerMap (fun x1 x2 => x1 * x2) A B
-- Mathlib.Analysis.Analytic.Constructions
/-- Multiplication of analytic functions (valued in a normed `𝕜`-algebra) is analytic.  -/
AnalyticAt.mul : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {A : Type u_7} [inst_3 : NormedRing A] [inst_4 : NormedAlgebra 𝕜 A] {f g : E → A} {z : E},
  AnalyticAt 𝕜 f z → AnalyticAt 𝕜 g z → AnalyticAt 𝕜 (f * g) z
-- Mathlib.Topology.Algebra.Group.Pointwise
IsTopologicalGroup.t2Space_of_one_sep : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Group G] [IsTopologicalGroup G],
  (∀ (x : G), x ≠ 1 → ∃ U ∈ nhds 1, x ∉ U) → T2Space G
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.coeff_C_mul : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] (n : σ →₀ ℕ) (φ : MvPowerSeries σ R) (a : R),
  (MvPowerSeries.coeff n) (MvPowerSeries.C a * φ) = a * (MvPowerSeries.coeff n) φ
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.PolyCnstr.isUnsat.eq_1 : ∀ (c : Nat.Internal.Linear.PolyCnstr),
  c.isUnsat =
    bif c.eq then c.lhs.isZero && c.rhs.isNonZero || c.lhs.isNonZero && c.rhs.isZero
    else c.lhs.isNonZero && c.rhs.isZero
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.integral_Iio_add_Ici : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {b : ℝ} {f : ℝ → E}
  {μ : MeasureTheory.Measure ℝ},
  MeasureTheory.IntegrableOn f (Set.Iio b) μ →
    MeasureTheory.IntegrableOn f (Set.Ici b) μ →
      ∫ (x : ℝ) in Set.Iio b, f x ∂μ + ∫ (x : ℝ) in Set.Ici b, f x ∂μ = ∫ (x : ℝ), f x ∂μ
-- Mathlib.Analysis.Calculus.ContDiff.Basic
/-- The natural equivalence `(E × F) × G ≃ E × (F × G)` is smooth.

Warning: if you think you need this lemma, it is likely that you can simplify your proof by
reformulating the lemma that you're applying next using the tips in
Note [continuity lemma statement]
 -/
contDiff_prodAssoc : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {n : WithTop ℕ∞}, ContDiff 𝕜 n ⇑(Equiv.prodAssoc E F G)
-- Mathlib.Analysis.Calculus.ContDiff.Defs
contDiffOn_succ_of_fderivWithin : ∀ {𝕜 : 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 : Set E}
  {f : E → F} {n : WithTop ℕ∞},
  DifferentiableOn 𝕜 f s →
    (n = ⊤ → AnalyticOn 𝕜 f s) → ContDiffOn 𝕜 n (fun y => fderivWithin 𝕜 f s y) s → ContDiffOn 𝕜 (n + 1) f s
-- Init.Data.Ord.Basic
Ordering.isGT_eq_beq_gt : ∀ {o : Ordering}, o.isGT = (o == Ordering.gt)
-- Mathlib.AlgebraicTopology.SimplexCategory.Defs
/-- Identity morphisms of `SimplexCategory`.  -/
SimplexCategory.Hom.id : (a : SimplexCategory) → a.Hom a