mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.dvdTight : Lean.Meta.Grind.Arith.Cutsat.DvdCnstr → Lean.Meta.Grind.Arith.Cutsat.LeCnstr → Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof
-- Mathlib.Order.Hom.Basic
OrderHom.id_coe : ∀ {α : Type u_2} [inst : Preorder α], ⇑OrderHom.id = id
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem?_union_of_not_mem_left : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k : α}, k ∉ m₁ → (m₁ ∪ m₂)[k]? = m₂[k]?
-- Mathlib.Data.Complex.Basic
/-- Scalar multiplication by `R` on `ℝ` extends to `ℂ`. This is used here and in
`Mathlib/LinearAlgebra/Complex/Module.lean` to transfer instances from `ℝ` to `ℂ`, but is not
needed outside, so we make it scoped.  -/
Complex.SMul.instSMulRealComplex : {R : Type u_1} → [SMul R ℝ] → SMul R ℂ
-- Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
AlgebraicGeometry.Scheme.IdealSheafData.comap.eq_1 : ∀ {X Y : AlgebraicGeometry.Scheme} (I : Y.IdealSheafData) (f : X ⟶ Y),
  I.comap f = AlgebraicGeometry.Scheme.Hom.ker (CategoryTheory.Limits.pullback.fst f I.subschemeι)
-- Mathlib.Analysis.Calculus.FDeriv.Equiv
ContinuousLinearEquiv.differentiableOn : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  (iso : E ≃L[𝕜] F), DifferentiableOn 𝕜 (⇑iso) s
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem_toArray_ric : ∀ {n i : ℕ} (_h : i < (*...=n).toArray.size), (*...=n).toArray[i] = i
-- Mathlib.Probability.Kernel.Disintegration.StandardBorel
MeasureTheory.Measure.condKernel_apply : ∀ {α : Type u_1} {Ω : Type u_4} {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω]
  [inst_1 : Nonempty Ω] (ρ : MeasureTheory.Measure (α × Ω)) [inst_2 : MeasureTheory.IsFiniteMeasure ρ] (a : α),
  ρ.condKernel a = (ProbabilityTheory.Kernel.const Unit ρ).condKernelUnitBorel ((), a)
-- Std.Data.DTreeMap.Internal.WF.Defs
/-- `modify` preserves well-formedness. Later shown to be subsumed by `.wf`.  -/
Std.DTreeMap.Internal.Impl.WF.modify : ∀ {α : Type u} [inst : Ord α] {x : α → Type v} [inst_1 : Std.LawfulEqOrd α] {t : Std.DTreeMap.Internal.Impl α x} {k : α}
  {f : x k → x k}, t.WF → (Std.DTreeMap.Internal.Impl.modify k f t).WF
-- Mathlib.RingTheory.Etale.StandardEtale
StandardEtalePair.HasMap.eq_1 : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : StandardEtalePair R) (x : S), P.HasMap x = ((Polynomial.aeval x) P.f = 0 ∧ IsUnit ((Polynomial.aeval x) P.g))
-- Mathlib.GroupTheory.GroupAction.Defs
AddAction.orbit.eq_1 : ∀ (γ : Type u_2) {α : Type u_3} [inst : VAdd γ α] (a : α), AddAction.orbit γ a = Set.range fun m => m +ᵥ a
-- Mathlib.Topology.Sheaves.CommRingCat
/-- Pulling back functions into a topological ring along a continuous map is a ring homomorphism.  -/
TopCat.continuousFunctions.pullback : {X Y : TopCatᵒᵖ} → (X ⟶ Y) → (R : TopCommRingCat) → TopCat.continuousFunctions X R ⟶ TopCat.continuousFunctions Y R
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.isChain_adj_cons_support : ∀ {V : Type u} {G : SimpleGraph V} {u v w : V}, G.Adj u v → ∀ (p : G.Walk v w), List.IsChain G.Adj (u :: p.support)
-- Mathlib.CategoryTheory.MorphismProperty.LiftingProperty
CategoryTheory.MorphismProperty.llp_isStableUnderCoproductsOfShape : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (T : CategoryTheory.MorphismProperty C) (J : Type u_1),
  T.llp.IsStableUnderCoproductsOfShape J
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.toList_filter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {f : (a : α) → β a → Bool}, (Std.ExtDTreeMap.filter f t).toList = List.filter (fun p => f p.fst p.snd) t.toList
-- Mathlib.Order.SuccPred.Limit
Order.not_isSuccPrelimit_of_noMax : ∀ {α : Type u_1} {a : α} [inst : Preorder α] [inst_1 : SuccOrder α] [IsSuccArchimedean α] [NoMaxOrder α] [NoMinOrder α],
  ¬Order.IsSuccPrelimit a
-- Mathlib.Analysis.Asymptotics.Defs
/-- Eta-expanded form of `Asymptotics.IsLittleO.sum` -/
Asymptotics.IsLittleO.fun_sum : ∀ {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [inst : SeminormedAddCommGroup E'] [inst_1 : SeminormedAddCommGroup F']
  {g' : α → F'} {l : Filter α} {ι : Type u_18} {A : ι → α → E'} {s : Finset ι},
  (∀ i ∈ s, A i =o[l] g') → (fun a => ∑ c ∈ s, A c a) =o[l] g'
-- Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
/-- Given a family of functors `I i ⥤ C` for `i : α`, we obtain a functor `(∀ i, I i) ⥤ C` which
maps `k : ∀ i, I i` to `∏ᶜ fun (s : α) => (F s).obj (k s)`.  -/
CategoryTheory.Limits.pointwiseProduct : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {α : Type u_1} →
      {I : α → Type u_2} →
        [inst_1 : (i : α) → CategoryTheory.Category.{v_1, u_2} (I i)] →
          [CategoryTheory.Limits.HasProductsOfShape α C] →
            ((i : α) → CategoryTheory.Functor (I i) C) → CategoryTheory.Functor ((i : α) → I i) C
-- Mathlib.Topology.Algebra.ClopenNhdofOne
ProfiniteGrp.exist_openNormalSubgroup_sub_open_nhds_of_one : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G]
  [TotallyDisconnectedSpace G] {U : Set G}, IsOpen U → 1 ∈ U → ∃ H, ↑H ⊆ U
-- Mathlib.Probability.Process.Filtration
MeasureTheory.Filtration.memLp_limitProcess_of_eLpNorm_bdd : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {R : NNReal} {p : ENNReal} {F : Type u_5}
  [inst : NormedAddCommGroup F] {ℱ : MeasureTheory.Filtration ℕ m} {f : ℕ → Ω → F},
  (∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (f n) μ) →
    (∀ (n : ℕ), MeasureTheory.eLpNorm (f n) p μ ≤ ↑R) →
      MeasureTheory.MemLp (MeasureTheory.Filtration.limitProcess f ℱ μ) p μ
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.support_zero : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R], MvPolynomial.support 0 = ∅
-- Mathlib.MeasureTheory.Group.FundamentalDomain
/-- We say a quotient of `α` by `G` `HasFundamentalDomain` if there is a measurable set `s` for
which `IsFundamentalDomain G s` holds.  -/
MeasureTheory.HasFundamentalDomain : (G : Type u_6) →
  (α : Type u_7) →
    [One G] →
      [SMul G α] →
        [inst : MeasurableSpace α] →
          autoParam (MeasureTheory.Measure α) MeasureTheory.HasFundamentalDomain._auto_1 → Prop
-- Mathlib.LinearAlgebra.Prod
LinearMap.fst_apply : ∀ {R : Type u} {M : Type v} {M₂ : Type w} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M₂]
  [inst_3 : Module R M] [inst_4 : Module R M₂] (x : M × M₂), (LinearMap.fst R M M₂) x = x.1
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.Internal.List.getKey?.eq_def : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (a : α) (x : List ((a : α) × β a)),
  Std.Internal.List.getKey? a x =
    match x with
    | [] => none
    | ⟨k, snd⟩ :: l => bif k == a then some k else Std.Internal.List.getKey? a l
-- Mathlib.Order.Fin.Tuple
/-- Order isomorphism between tuples of length `n + 1` and pairs of an element and a tuple of length
`n` given by separating out the first element of the tuple.

This is `Fin.cons` as an `OrderIso`.  -/
Fin.consOrderIso : {n : ℕ} →
  (α : Fin (n + 1) → Type u_2) →
    [inst : (i : Fin (n + 1)) → LE (α i)] → α 0 × ((i : Fin n) → α i.succ) ≃o ((i : Fin (n + 1)) → α i)
-- Mathlib.Order.SuccPred.Limit
Order.IsPredLimit.nonempty_Ioi : ∀ {α : Type u_1} {a : α} [inst : Preorder α], Order.IsPredLimit a → (Set.Ioi a).Nonempty
-- Mathlib.CategoryTheory.Products.Associator
CategoryTheory.prod.associativity_inverse : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (E : Type u₃) [inst_2 : CategoryTheory.Category.{v₃, u₃} E],
  (CategoryTheory.prod.associativity C D E).inverse = CategoryTheory.prod.inverseAssociator C D E
-- Mathlib.Algebra.Order.WithTop.Untop0
WithTop.untop₀_le_untop₀ : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] {a b : WithTop α},
  b ≠ ⊤ → a ≤ b → a.untop₀ ≤ b.untop₀
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
NonUnitalSubsemiring.coe_iInf : ∀ {R : Type u} [inst : NonUnitalNonAssocSemiring R] {ι : Sort u_1} {S : ι → NonUnitalSubsemiring R},
  ↑(⨅ i, S i) = ⋂ i, ↑(S i)
-- Mathlib.CategoryTheory.Products.Basic
CategoryTheory.prod_comp : ∀ {C : Type u₁} [inst : CategoryTheory.CategoryStruct.{v₁, u₁} C] {D : Type u₂}
  [inst_1 : CategoryTheory.CategoryStruct.{v₂, u₂} D] {P Q R : C} {S T U : D} (f : (P, S) ⟶ (Q, T))
  (g : (Q, T) ⟶ (R, U)),
  CategoryTheory.CategoryStruct.comp f g =
    CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.comp f.1 g.1) (CategoryTheory.CategoryStruct.comp f.2 g.2)
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
AlgebraicGeometry.instRespectsSchemeLocallyQuasiFiniteIsOpenImmersion : CategoryTheory.MorphismProperty.Respects (@AlgebraicGeometry.LocallyQuasiFinite) AlgebraicGeometry.IsOpenImmersion
-- Std.Data.HashMap.Lemmas
Std.HashMap.toArray_toList : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β}, m.toList.toArray = m.toArray
-- Mathlib.Analysis.Complex.CanonicalDecomposition
/-- The divisor of `CanonicalFactor R w` is `-w`.  In other words, the divisor function takes the value
-1 at `w` and is zero elsewhere.
 -/
Complex.divisor_canonicalFactor : ∀ {R : ℝ} {w : ℂ},
  w ∈ Metric.ball 0 R →
    MeromorphicOn.divisor (Complex.canonicalFactor R w) (Metric.ball 0 R) =
      -Function.locallyFinsuppWithin.restrict (Function.locallyFinsuppWithin.single w 1) ⋯
-- Batteries.Lean.Meta.SavedState
/-- Run the action `x` in state `s`. Returns the result of `x`. The global state
remains unchanged.
 -/
Lean.Meta.SavedState.runMetaM' : {α : Type} → Lean.Meta.SavedState → Lean.MetaM α → Lean.MetaM α
-- Mathlib.Analysis.Calculus.InverseFunctionTheorem.FDeriv
HasStrictFDerivAt.map_nhds_eq_of_surj : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] [CompleteSpace E]
  [CompleteSpace F] {f : E → F} {f' : E →L[𝕜] F} {a : E},
  HasStrictFDerivAt f f' a → (↑f').range = ⊤ → Filter.map f (nhds a) = nhds (f a)
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.isMaximumIndepSet_compl : ∀ {α : Type u_3} {G : SimpleGraph α} [inst : Finite α] (s : Finset α), Gᶜ.IsMaximumIndepSet s ↔ G.IsMaximumClique s
-- Mathlib.Topology.ContinuousMap.ContinuousMapZero
/-- The type of continuous maps which map zero to zero.

Note that one should never use the structure projection `ContinuousMapZero.toContinuousMap` and
instead favor the coercion `(↑) : C(X, R)₀ → C(X, R)` available from the instance of
`ContinuousMapClass`. All the instances on `C(X, R)₀` from `C(X, R)` passes through this coercion,
not the structure projection. Of course, the two are definitionally equal, but not reducibly so.  -/
ContinuousMapZero.«termC(_,_)₀» : Lean.ParserDescr
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
Mathlib.Tactic.BicategoryLike.MonadNormalExpr.toMonadWhiskerLeft : {m : Type → Type} →
  [self : Mathlib.Tactic.BicategoryLike.MonadNormalExpr m] → Mathlib.Tactic.BicategoryLike.MonadWhiskerLeft m
-- Mathlib.RingTheory.DividedPowers.RatAlgebra
DividedPowers.OfInvertibleFactorial.dpow_zero : ∀ {A : Type u_1} [inst : CommSemiring A] {I : Ideal A} [inst_1 : DecidablePred fun x => x ∈ I] {x : A},
  x ∈ I → DividedPowers.OfInvertibleFactorial.dpow I 0 x = 1
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Series
/-- The power series expansion of `Complex.sin`.  -/
Complex.hasSum_sin : ∀ (z : ℂ), HasSum (fun n => (-1) ^ n * z ^ (2 * n + 1) / ↑(2 * n + 1).factorial) (Complex.sin z)
-- Mathlib.Analysis.Normed.Field.Approximation
/-- If `K` is a dense subfield of `L`, then every monic polynomial in `L` can be
approximated by a monic polynomial in `K` of the same degree.  -/
Polynomial.exists_monic_and_natDegree_eq_and_norm_map_algebraMap_coeff_sub_lt : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : NormedField L] [inst_2 : Algebra K L],
  DenseRange ⇑(algebraMap K L) →
    ∀ {f : Polynomial L},
      f.Monic →
        ∀ {ε : ℝ},
          ε > 0 →
            ∃ g,
              g.Monic ∧
                f.natDegree = g.natDegree ∧ ∀ (n : ℕ), ‖(Polynomial.map (algebraMap K L) g).coeff n - f.coeff n‖ < ε
-- Mathlib.Topology.UniformSpace.Closeds
TopologicalSpace.Closeds.uniformContinuous_singleton : ∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : T0Space α], UniformContinuous fun x => {x}
-- Mathlib.Order.ModularLattice
/-- Whenever `x ≤ z`, then for any `y`, `(x ⊔ y) ⊓ z ≤ x ⊔ (y ⊓ z)`  -/
IsModularLattice.sup_inf_le_assoc_of_le : ∀ {α : Type u_2} {inst : Lattice α} [self : IsModularLattice α] {x : α} (y : α) {z : α}, x ≤ z → (x ⊔ y) ⊓ z ≤ x ⊔ y ⊓ z
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
csInf_le : ∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {s : Set α} {a : α}, BddBelow s → a ∈ s → sInf s ≤ a
-- Mathlib.CategoryTheory.Bicategory.LocallyDiscrete
CategoryTheory.LocallyDiscrete.ext_iff : ∀ {C : Type u} {x y : CategoryTheory.LocallyDiscrete C}, x = y ↔ x.as = y.as
-- Mathlib.CategoryTheory.GlueData
CategoryTheory.GlueData.mk.injEq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v, u₁} C] (J : Type v) (U : J → C) (V : J × J → C)
  (f : (i j : J) → V (i, j) ⟶ U i)
  (f_mono : autoParam (∀ (i j : J), CategoryTheory.Mono (f i j)) CategoryTheory.GlueData.f_mono._autoParam)
  (f_hasPullback :
    autoParam (∀ (i j k : J), CategoryTheory.Limits.HasPullback (f i j) (f i k))
      CategoryTheory.GlueData.f_hasPullback._autoParam)
  (f_id : autoParam (∀ (i : J), CategoryTheory.IsIso (f i i)) CategoryTheory.GlueData.f_id._autoParam)
  (t : (i j : J) → V (i, j) ⟶ V (j, i)) (t_id : ∀ (i : J), t i i = CategoryTheory.CategoryStruct.id (V (i, i)))
  (t' : (i j k : J) → CategoryTheory.Limits.pullback (f i j) (f i k) ⟶ CategoryTheory.Limits.pullback (f j k) (f j i))
  (t_fac :
    ∀ (i j k : J),
      CategoryTheory.CategoryStruct.comp (t' i j k) (CategoryTheory.Limits.pullback.snd (f j k) (f j i)) =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (f i j) (f i k)) (t i j))
  (cocycle :
    ∀ (i j k : J),
      CategoryTheory.CategoryStruct.comp (t' i j k) (CategoryTheory.CategoryStruct.comp (t' j k i) (t' k i j)) =
        CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.pullback (f i j) (f i k)))
  (J_1 : Type v) (U_1 : J_1 → C) (V_1 : J_1 × J_1 → C) (f_1 : (i j : J_1) → V_1 (i, j) ⟶ U_1 i)
  (f_mono_1 : autoParam (∀ (i j : J_1), CategoryTheory.Mono (f_1 i j)) CategoryTheory.GlueData.f_mono._autoParam)
  (f_hasPullback_1 :
    autoParam (∀ (i j k : J_1), CategoryTheory.Limits.HasPullback (f_1 i j) (f_1 i k))
      CategoryTheory.GlueData.f_hasPullback._autoParam)
  (f_id_1 : autoParam (∀ (i : J_1), CategoryTheory.IsIso (f_1 i i)) CategoryTheory.GlueData.f_id._autoParam)
  (t_1 : (i j : J_1) → V_1 (i, j) ⟶ V_1 (j, i))
  (t_id_1 : ∀ (i : J_1), t_1 i i = CategoryTheory.CategoryStruct.id (V_1 (i, i)))
  (t'_1 :
    (i j k : J_1) →
      CategoryTheory.Limits.pullback (f_1 i j) (f_1 i k) ⟶ CategoryTheory.Limits.pullback (f_1 j k) (f_1 j i))
  (t_fac_1 :
    ∀ (i j k : J_1),
      CategoryTheory.CategoryStruct.comp (t'_1 i j k) (CategoryTheory.Limits.pullback.snd (f_1 j k) (f_1 j i)) =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (f_1 i j) (f_1 i k)) (t_1 i j))
  (cocycle_1 :
    ∀ (i j k : J_1),
      CategoryTheory.CategoryStruct.comp (t'_1 i j k) (CategoryTheory.CategoryStruct.comp (t'_1 j k i) (t'_1 k i j)) =
        CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.pullback (f_1 i j) (f_1 i k))),
  ({ J := J, U := U, V := V, f := f, f_mono := f_mono, f_hasPullback := f_hasPullback, f_id := f_id, t := t,
        t_id := t_id, t' := t', t_fac := t_fac, cocycle := cocycle } =
      { J := J_1, U := U_1, V := V_1, f := f_1, f_mono := f_mono_1, f_hasPullback := f_hasPullback_1, f_id := f_id_1,
        t := t_1, t_id := t_id_1, t' := t'_1, t_fac := t_fac_1, cocycle := cocycle_1 }) =
    (J = J_1 ∧ U ≍ U_1 ∧ V ≍ V_1 ∧ f ≍ f_1 ∧ t ≍ t_1 ∧ t' ≍ t'_1)
-- Mathlib.Topology.Category.LightProfinite.Injective
/-- A categorically stated version of `exists_lift_of_finite_of_injective_of_surjective` in the
category `Profinite`.  -/
Profinite.exists_lift_of_finite_of_mono_of_epi : ∀ {X Y S T : Profinite} [Finite ↑S.toTop] (f : X ⟶ Y) [CategoryTheory.Mono f] (f' : S ⟶ T) [CategoryTheory.Epi f']
  (g : X ⟶ S) (g' : Y ⟶ T),
  CategoryTheory.CategoryStruct.comp f g' = CategoryTheory.CategoryStruct.comp g f' →
    ∃ k, CategoryTheory.CategoryStruct.comp k f' = g' ∧ CategoryTheory.CategoryStruct.comp f k = g
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
/-- The action by a subalgebra is the action by the underlying algebra.  -/
Subalgebra.toAlgebra : {α : Type u_1} →
  {R : Type u_3} →
    {A : Type u_4} →
      [inst : CommSemiring R] →
        [inst_1 : CommSemiring A] →
          [inst_2 : Semiring α] → [inst_3 : Algebra R A] → [Algebra A α] → (S : Subalgebra R A) → Algebra (↥S) α
-- Mathlib.Topology.Sheaves.SheafCondition.Sites
/-- An index `i : ι` can be turned into a dependent pair `(V, f)`, where `V` is an open set and
`f : V ⟶ iSup U` is a member of `presieveOfCovering U f`.
 -/
TopCat.Presheaf.presieveOfCovering.homOfIndex : {X : TopCat} →
  {ι : Type v} →
    (U : ι → TopologicalSpace.Opens ↑X) →
      ι → (V : TopologicalSpace.Opens ↑X) × { f // TopCat.Presheaf.presieveOfCovering U f }
-- Mathlib.Order.Atoms
instIsStronglyAtomicElemOfOrdConnected : ∀ {α : Type u_4} [inst : Preorder α] [IsStronglyAtomic α] {s : Set α} [s.OrdConnected], IsStronglyAtomic ↑s
-- Mathlib.CategoryTheory.Localization.Trifunctor
/-- Classes of morphisms `W₁ : MorphismProperty C₁`, `W₂ : MorphismProperty C₂` and
`W₃ : MorphismProperty C₃` are said to be inverted by `F : C₁ ⥤ C₂ ⥤ C₃ ⥤ E` if
`W₁.prod (W₂.prod W₃)` is inverted by the
functor `currying₃.functor.obj F : C₁ × C₂ × C₃ ⥤ E`.  -/
CategoryTheory.MorphismProperty.IsInvertedBy₃ : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {C₃ : Type u_3} →
      {E : Type u_13} →
        [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₃] →
              [inst_3 : CategoryTheory.Category.{v_13, u_13} E] →
                CategoryTheory.MorphismProperty C₁ →
                  CategoryTheory.MorphismProperty C₂ →
                    CategoryTheory.MorphismProperty C₃ →
                      CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ E)) → Prop
-- Mathlib.Topology.Algebra.InfiniteSum.Order
Multipliable.tprod_strict_mono : ∀ {ι : Type u_1} {α : Type u_3} {L : SummationFilter ι} [inst : CommGroup α] [inst_1 : PartialOrder α]
  [IsOrderedMonoid α] [inst_3 : TopologicalSpace α] [IsTopologicalGroup α] [OrderClosedTopology α] {f g : ι → α}
  [L.NeBot] [L.LeAtTop], Multipliable f L → Multipliable g L → f < g → ∏'[L] (n : ι), f n < ∏'[L] (n : ι), g n
-- Mathlib.Data.Set.Image
Function.Involutive.image_eq_preimage_symm : ∀ {α : Type u_1} {f : α → α}, Function.Involutive f → Set.image f = Set.preimage f
-- Mathlib.RingTheory.IntegralClosure.Algebra.Ideal
Polynomial.exists_monic_aeval_eq_zero_forall_mem_pow_of_mem_map : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [Algebra.IsIntegral R S] {I : Ideal R} {x : S},
  x ∈ Ideal.map (algebraMap R S) I →
    ∃ p, p.Monic ∧ (Polynomial.aeval x) p = 0 ∧ ∀ (i : ℕ), p.coeff i ∈ I ^ (p.natDegree - i)
-- Mathlib.Analysis.Calculus.FDeriv.Add
DifferentiableWithinAt.const_smul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {x : E} {s : Set E} {R : Type u_4} [inst_5 : Monoid R] [inst_6 : DistribMulAction R F] [SMulCommClass 𝕜 R F]
  [ContinuousConstSMul R F], DifferentiableWithinAt 𝕜 f s x → ∀ (c : R), DifferentiableWithinAt 𝕜 (c • f) s x
-- Mathlib.Algebra.Group.Submonoid.Defs
AddSubmonoid.instPartialOrder : {M : Type u_1} → [inst : AddZeroClass M] → PartialOrder (AddSubmonoid M)
-- Mathlib.RingTheory.DiscreteValuationRing.TFAE
/-- Let `(R, m, k)` be a Noetherian local domain (possibly a field).
The following are equivalent:
0. `R` is a PID
1. `R` is a valuation ring
2. `R` is a Dedekind domain
3. `R` is integrally closed with at most one non-zero prime ideal
4. `m` is principal
5. `dimₖ m/m² ≤ 1`
6. Every nonzero ideal is a power of `m`.

Also see `IsDiscreteValuationRing.TFAE` for a version assuming `¬ IsField R`.
 -/
tfae_of_isNoetherianRing_of_isLocalRing_of_isDomain : ∀ (R : Type u_1) [inst : CommRing R] [IsNoetherianRing R] [inst_2 : IsLocalRing R] [inst_3 : IsDomain R],
  [IsPrincipalIdealRing R, ValuationRing R, IsDedekindDomain R,
      IsIntegrallyClosed R ∧ ∀ (P : Ideal R), P ≠ ⊥ → P.IsPrime → P = IsLocalRing.maximalIdeal R,
      Submodule.IsPrincipal (IsLocalRing.maximalIdeal R),
      Module.finrank (IsLocalRing.ResidueField R) (IsLocalRing.CotangentSpace R) ≤ 1,
      ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = IsLocalRing.maximalIdeal R ^ n].TFAE
-- Mathlib.Algebra.Notation.Prod
Prod.instVAdd.eq_1 : ∀ {E : Type u_8} {α : Type u_9} {β : Type u_10} [inst : VAdd E α] [inst_1 : VAdd E β],
  Prod.instVAdd = { vadd := fun c p => (c +ᵥ p.1, c +ᵥ p.2) }
-- Init.Data.List.MinMaxIdx
List.isSome_maxIdxOn?_iff : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] {f : α → β} {xs : List α},
  (List.maxIdxOn? f xs).isSome = true ↔ xs ≠ []
-- Init.Data.String.Lemmas.Splits
String.Slice.Pos.sliceFrom_cast : ∀ {s t : String.Slice} {hst : s.copy = t.copy} (p q : s.Pos) {h : p.cast hst ≤ q.cast hst},
  (p.cast hst).sliceFrom (q.cast hst) h = (p.sliceFrom q ⋯).cast ⋯
-- Mathlib.RingTheory.Localization.Basic
localizationAlgebraMap_def : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] (Rₘ : Type u_4) (Sₘ : Type u_5) [inst_3 : CommSemiring Rₘ] [inst_4 : CommSemiring Sₘ]
  [inst_5 : Algebra R Rₘ] [inst_6 : IsLocalization M Rₘ] [inst_7 : Algebra S Sₘ]
  [i : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ], algebraMap Rₘ Sₘ = IsLocalization.map Sₘ (algebraMap R S) ⋯
-- Init.Data.String.Lemmas.Order
String.Slice.Pos.startPos_lt_iff : ∀ {s : String.Slice} (p : s.Pos), s.startPos < p ↔ p ≠ s.startPos
-- Mathlib.Data.Nat.Factorial.BigOperators
Nat.descFactorial_eq_prod_range : ∀ (n k : ℕ), n.descFactorial k = ∏ i ∈ Finset.range k, (n - i)
-- Mathlib.Algebra.Group.Defs
nsmul_zero : ∀ {M : Type u_2} [inst : AddMonoid M] (n : ℕ), n • 0 = 0
-- Mathlib.Topology.Separation.Hausdorff
T2Quotient.inductionOn₂ : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  {motive : T2Quotient X → T2Quotient Y → Prop} (q : T2Quotient X) (q' : T2Quotient Y),
  (∀ (x : X) (y : Y), motive (T2Quotient.mk x) (T2Quotient.mk y)) → motive q q'
-- Init.Data.BitVec.Lemmas
BitVec.sub_toNat_mod_cancel_of_toNat : ∀ {w : ℕ} {x : BitVec w}, x.toNat ≠ 0 → (2 ^ w - x.toNat) % 2 ^ w = 2 ^ w - x.toNat
-- Init.Data.Nat.Fold
_private.Init.Data.Nat.Fold.0.Nat.any.match_1.eq_2 : ∀ (motive : (x : ℕ) → ((i : ℕ) → i < x → Bool) → Sort u_1) (n : ℕ) (f : (i : ℕ) → i < n.succ → Bool)
  (h_1 : (f : (i : ℕ) → i < 0 → Bool) → motive 0 f)
  (h_2 : (n : ℕ) → (f : (i : ℕ) → i < n.succ → Bool) → motive n.succ f),
  (match n.succ, f with
    | 0, f => h_1 f
    | n.succ, f => h_2 n f) =
    h_2 n f
-- Mathlib.Analysis.Normed.Group.Ultra
/-- Nonarchimedean norm of a product is less than or equal to the largest norm of a term in the
product.  -/
Finset.nnnorm_prod_le_sup_nnnorm : ∀ {M : Type u_1} {ι : Type u_2} [inst : SeminormedCommGroup M] [IsUltrametricDist M] (s : Finset ι) (f : ι → M),
  ‖∏ i ∈ s, f i‖₊ ≤ s.sup fun x => ‖f x‖₊