mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
CategoryTheory.Functor.IsDenseSubsite.sheafifyHomEquivOfIsEquivalence_naturality_left : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (J : CategoryTheory.GrothendieckTopology C)
  (K : CategoryTheory.GrothendieckTopology D) (G : CategoryTheory.Functor C D) {A : Type u_4}
  [inst_2 : CategoryTheory.Category.{v_4, u_4} A] [inst_3 : CategoryTheory.Functor.IsDenseSubsite J K G]
  [inst_4 : (G.sheafPushforwardContinuous A J K).IsEquivalence] [inst_5 : CategoryTheory.HasWeakSheafify J A]
  {P₁ P₂ : CategoryTheory.Functor Dᵒᵖ A} (f : P₁ ⟶ P₂) {Q : CategoryTheory.Sheaf K A}
  (g : (CategoryTheory.Functor.IsDenseSubsite.sheafifyOfIsEquivalence J K G A).obj P₂ ⟶ Q),
  (CategoryTheory.Functor.IsDenseSubsite.sheafifyHomEquivOfIsEquivalence J K G)
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.Functor.IsDenseSubsite.sheafifyOfIsEquivalence J K G A).map f) g) =
    CategoryTheory.CategoryStruct.comp f
      ((CategoryTheory.Functor.IsDenseSubsite.sheafifyHomEquivOfIsEquivalence J K G) g)
-- Mathlib.LinearAlgebra.Finsupp.Pi
Finsupp.range_mapRange_linearMap : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] (f : M →ₗ[R] N),
  f.ker = ⊥ → ∀ (I : Type u_6), (Finsupp.mapRange.linearMap f).range = Finsupp.submodule fun x => f.range
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddHom.mem_srange : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] {f : M →ₙ+ N} {y : N}, y ∈ f.srange ↔ ∃ x, f x = y
-- Mathlib.Analysis.Calculus.IteratedDeriv.Defs
iteratedDerivWithin_of_isOpen : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {n : ℕ} {f : 𝕜 → F} {s : Set 𝕜},
  IsOpen s → Set.EqOn (iteratedDerivWithin n f s) (iteratedDeriv n f) s
-- Mathlib.Order.Atoms
/-- **Alias** of `exists_le_covBy_of_lt`. -/
LT.lt.exists_le_covby : ∀ {α : Type u_4} {a b : α} [inst : Preorder α] [IsStronglyCoatomic α], a < b → ∃ x, a ≤ x ∧ x ⋖ b
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousSemilinearEquivClass.continuousSemilinearMapClass : ∀ (F : Type u_1) {R : Type u_2} {S : Type u_3} [inst : Semiring R] [inst_1 : Semiring S] (σ : R →+* S) {σ' : S →+* R}
  [inst_2 : RingHomInvPair σ σ'] [inst_3 : RingHomInvPair σ' σ] (M : Type u_4) [inst_4 : TopologicalSpace M]
  [inst_5 : AddCommMonoid M] (M₂ : Type u_5) [inst_6 : TopologicalSpace M₂] [inst_7 : AddCommMonoid M₂]
  [inst_8 : Module R M] [inst_9 : Module S M₂] [inst_10 : EquivLike F M M₂]
  [s : ContinuousSemilinearEquivClass F σ M M₂], ContinuousSemilinearMapClass F σ M M₂
-- Mathlib.Algebra.Ring.Associator
/-- The associator for a non-associative ring is `(x * y) * z - x * (y * z)`. It is an
`AddMonoidHom` in each argument.  -/
AddMonoidHom.associator : {R : Type u_1} → [inst : NonUnitalNonAssocRing R] → R →+ R →+ R →+ R
-- Mathlib.Logic.Small.Defs
small_self : ∀ (α : Type v), Small.{v, v} α
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.size_inter_le_size_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp],
  (t₁ ∩ t₂).size ≤ t₂.size
-- Mathlib.Order.Category.BddDistLat
BddDistLat.hasForgetToDistLat : CategoryTheory.HasForget₂ BddDistLat DistLat
-- Mathlib.Order.Category.BddOrd
BddOrd.instInhabited : Inhabited BddOrd
-- Mathlib.Algebra.Polynomial.Div
Polynomial.rootMultiplicity_eq_natFind_of_ne_zero : ∀ {R : Type u} [inst : Ring R] {p : Polynomial R} (p0 : p ≠ 0) {a : R}
  [inst_1 : DecidablePred fun n => ¬(Polynomial.X - Polynomial.C a) ^ (n + 1) ∣ p],
  Polynomial.rootMultiplicity a p = Nat.find ⋯
-- Mathlib.Topology.Constructions.SumProd
/-- A version of `continuous_inf_dom_right` for binary functions  -/
continuous_inf_dom_right₂ : ∀ {X : Type u_5} {Y : Type u_6} {Z : Type u_7} {f : X → Y → Z} {ta1 ta2 : TopologicalSpace X}
  {tb1 tb2 : TopologicalSpace Y} {tc1 : TopologicalSpace Z},
  (Continuous fun p => f p.1 p.2) → Continuous fun p => f p.1 p.2
-- Mathlib.Algebra.Lie.IdealOperations
LieSubmodule.le_comap_map : ∀ {R : Type u} {L : Type v} {M : Type w} {M₂ : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : AddCommGroup M] [inst_3 : Module R M] [inst_4 : LieRingModule L M] [inst_5 : AddCommGroup M₂]
  [inst_6 : Module R M₂] [inst_7 : LieRingModule L M₂] (N : LieSubmodule R L M) (f : M →ₗ⁅R,L⁆ M₂),
  N ≤ LieSubmodule.comap f (LieSubmodule.map f N)
-- Mathlib.CategoryTheory.MorphismProperty.Basic
/-- If `W₁` and `W₂` are morphism properties on two categories `C₁` and `C₂`,
this is the induced morphism property on `C₁ × C₂`.  -/
CategoryTheory.MorphismProperty.prod : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    [inst : CategoryTheory.CategoryStruct.{u_3, u_1} C₁] →
      [inst_1 : CategoryTheory.CategoryStruct.{u_4, u_2} C₂] →
        CategoryTheory.MorphismProperty C₁ →
          CategoryTheory.MorphismProperty C₂ → CategoryTheory.MorphismProperty (C₁ × C₂)
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring
HomogeneousSubsemiring.ext' : ∀ {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [inst : AddMonoid ι] [inst_1 : Semiring A] [inst_2 : SetLike σ A]
  [inst_3 : AddSubmonoidClass σ A] {𝒜 : ι → σ} [inst_4 : DecidableEq ι] [inst_5 : GradedRing 𝒜]
  {R S : HomogeneousSubsemiring 𝒜}, (∀ (i : ι), ∀ a ∈ 𝒜 i, a ∈ R ↔ a ∈ S) → R = S
-- Lean.Environment
_private.Lean.Environment.0.Lean.AsyncConsts.add : Lean.AsyncConsts✝ → Lean.AsyncConst✝ → Lean.AsyncConsts✝
-- Mathlib.NumberTheory.Padics.HeightOneSpectrum
Rat.int_algebraMap_injective : ∀ (R : Type u_1) [inst : CommRing R] [Algebra R ℚ], Function.Injective ⇑(algebraMap ℤ R)
-- Mathlib.Probability.ProbabilityMassFunction.Basic
PMF.toMeasure_eq_iff_eq_toPMF : ∀ {α : Type u_1} [inst : Countable α] [inst_1 : MeasurableSpace α] [inst_2 : MeasurableSingletonClass α] (p : PMF α)
  (μ : MeasureTheory.Measure α) [inst_3 : MeasureTheory.IsProbabilityMeasure μ], p.toMeasure = μ ↔ p = μ.toPMF
-- Mathlib.Order.SymmDiff
Codisjoint.bihimp_inf_bihimp_le_right : ∀ {α : Type u_2} [inst : BooleanAlgebra α] {a b c : α}, Codisjoint b c → bihimp a b ⊓ bihimp a c ≤ a
-- Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral
/-- The integral of `mulExpNegMulSq ε ∘ g` with respect to a finite measure `P` converges to the
integral of `g`, as `ε → 0` from above.  -/
tendsto_integral_mulExpNegMulSq_comp : ∀ {E : Type u_1} [inst : TopologicalSpace E] [inst_1 : MeasurableSpace E] [BorelSpace E] {P : MeasureTheory.Measure E}
  [MeasureTheory.IsFiniteMeasure P] (g : BoundedContinuousFunction E ℝ),
  Filter.Tendsto (fun ε => ∫ (x : E), ε.mulExpNegMulSq (g x) ∂P) (nhdsWithin 0 (Set.Ioi 0)) (nhds (∫ (x : E), g x ∂P))
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Equiv.Perm.SameCycle.rfl : ∀ {α : Type u_2} {f : Equiv.Perm α} {x : α}, f.SameCycle x x
-- Mathlib.NumberTheory.LSeries.AbstractFuncEq
IsStrongFEPair.mk : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {P : WeakFEPair E},
  P.f₀ = 0 → P.g₀ = 0 → IsStrongFEPair P
-- Mathlib.Topology.Semicontinuity.Defs
lowerHemicontinuousOn_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → Set β} {s : Set α},
  LowerHemicontinuousOn f s ↔ ∀ x ∈ s, LowerHemicontinuousWithinAt f s x
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous
/-- If `f : X ⟶ Y`, this is the pushforward of sheaves of modules along `Over.map f`.  -/
SheafOfModules.overMap : {D : Type u₂} →
  [inst : CategoryTheory.Category.{v₂, u₂} D] →
    {K : CategoryTheory.GrothendieckTopology D} →
      (R : CategoryTheory.Sheaf K RingCat) →
        {X Y : D} → (X ⟶ Y) → CategoryTheory.Functor (SheafOfModules (R.over Y)) (SheafOfModules (R.over X))
-- Mathlib.LinearAlgebra.RootSystem.CartanMatrix
/-- The Cartan matrix of a root pairing, taking values in `S`, with respect to a base `b`.

See also `RootPairing.Base.cartanMatrix`.  -/
RootPairing.Base.cartanMatrixIn : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      {N : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] →
              [inst_3 : AddCommGroup N] →
                [inst_4 : Module R N] →
                  (S : Type u_5) →
                    [inst_5 : CommRing S] →
                      [inst_6 : Algebra S R] →
                        {P : RootPairing ι R M N} → [P.IsValuedIn S] → (b : P.Base) → Matrix (↥b.support) (↥b.support) S
-- Init.Data.List.Nat.TakeDrop
List.false_of_mem_take_findIdx : ∀ {α : Type u_1} {x : α} {xs : List α} {p : α → Bool}, x ∈ List.take (List.findIdx p xs) xs → p x = false
-- Mathlib.Data.Num.Basic
ZNum.pos : PosNum → ZNum
-- Mathlib.Algebra.Homology.DerivedCategory.DerivabilityStructureInjectives
CochainComplex.Plus.instIsRightDerivabilityStructureInjectiveObjectInverseImageQuasiIsoMapCochainComplexPlusιLocalizerMorphism : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [CategoryTheory.EnoughInjectives C], (CochainComplex.Plus.localizerMorphism C).IsRightDerivabilityStructure
-- Init.Data.String.Lemmas.Pattern.Split.Char
String.Slice.toList_split_intercalate : ∀ {c : Char} {l : List String.Slice},
  (∀ s ∈ l, c ∉ s.copy.toList) →
    List.map String.Slice.copy (((String.singleton c).toSlice.intercalate l).split c).toList =
      if l = [] then [""] else List.map String.Slice.copy l
-- Mathlib.Data.TypeVec
TypeVec.prod_snd_mk : ∀ {n : ℕ} {α β : TypeVec.{u_1} n} (i : Fin2 n) (a : α i) (b : β i), TypeVec.prod.snd i (TypeVec.prod.mk i a b) = b
-- Mathlib.Data.List.Flatten
/-- **Alias** of `List.getLast_getLast_eq_getLast_flatten`.

---

See also `getLast_flatten_eq_getLast_getLast`, which switches around the proof obligations.  -/
List.getLast_flatten_of_getLast_ne_nil : ∀ {α : Type u_1} {l : List (List α)} (hl : l ≠ []) (hl' : l.getLast hl ≠ []),
  (l.getLast hl).getLast hl' = l.flatten.getLast ⋯
-- Mathlib.Algebra.Group.Prod
AddMonoidHom.coe_fst : ∀ {M : Type u_3} {N : Type u_4} [inst : AddZeroClass M] [inst_1 : AddZeroClass N], ⇑(AddMonoidHom.fst M N) = Prod.fst
-- Mathlib.LinearAlgebra.Determinant
LinearMap.det_eq_one_of_finrank_eq_zero : ∀ {𝕜 : Type u_7} [inst : Field 𝕜] {M : Type u_8} [inst_1 : AddCommGroup M] [inst_2 : Module 𝕜 M],
  Module.finrank 𝕜 M = 0 → ∀ (f : M →ₗ[𝕜] M), LinearMap.det f = 1
-- Mathlib.Data.Sum.Order
OrderIso.sumLexAssoc_symm_apply_inr_inl : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : LE α] [inst_1 : LE β] [inst_2 : LE γ] (b : β),
  (OrderIso.sumLexAssoc α β γ).symm (Sum.inr (Sum.inl b)) = Sum.inl (Sum.inr b)
-- Mathlib.Algebra.Homology.SpectralObject.Homology
CategoryTheory.Abelian.SpectralObject.dKernelSequence_X₁ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.Category.{v_2, u_2} ι] (X : CategoryTheory.Abelian.SpectralObject C ι)
  {i₀ i₁ i₂ i₃ i₄ i₅ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₅ : i₄ ⟶ i₅) (f₂₃ : i₁ ⟶ i₃)
  (h₂₃ : CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ n₂ n₃ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.dKernelSequence._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.dKernelSequence._auto_3)
  (hn₃ : autoParam (n₂ + 1 = n₃) CategoryTheory.Abelian.SpectralObject.dKernelSequence._auto_5),
  (X.dKernelSequence f₁ f₂ f₃ f₄ f₅ f₂₃ h₂₃ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃).X₁ = X.E f₂₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯
-- Aesop.Rule
/-- A local rule for the norm simplifier.
 -/
Aesop.LocalNormSimpRule : Type
-- Mathlib.Order.Hom.Lex
OrderIso.sumLexIioIci_symm_apply_Iio : ∀ {α : Type u_1} [inst : LinearOrder α] {x : α} (a : ↑(Set.Iio x)),
  (OrderIso.sumLexIioIci x).symm ↑a = toLex (Sum.inl a)
-- Batteries.Data.List.Interleave
List.right_sublist_interleave : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₂.Sublist (l₁.interleave l₂)
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.restrictScalars_sup : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] (K : Type u_3)
  [inst_3 : Field K] [inst_4 : Algebra K E] [inst_5 : Algebra K F] [inst_6 : IsScalarTower K F E]
  (L L' : IntermediateField F E),
  IntermediateField.restrictScalars K L ⊔ IntermediateField.restrictScalars K L' =
    IntermediateField.restrictScalars K (L ⊔ L')
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.ofLp_snd : ∀ {p : ENNReal} {α : Type u_2} {β : Type u_3} (x : WithLp p (α × β)), x.ofLp.2 = x.snd
-- Mathlib.CategoryTheory.Monoidal.Closed.InternalCurrying
CategoryTheory.MonoidalClosed.ihomUncurry_ihomCurry : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (x y z : C)
  [inst_2 : CategoryTheory.Closed x] [inst_3 : CategoryTheory.Closed y]
  [inst_4 : CategoryTheory.Closed (CategoryTheory.MonoidalCategoryStruct.tensorObj x y)],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalClosed.ihomUncurry x y z)
      (CategoryTheory.MonoidalClosed.ihomCurry x y z) =
    CategoryTheory.CategoryStruct.id (y ⟹ x ⟹ z)
-- Mathlib.RingTheory.Localization.FractionRing
IsFractionRing.nonZeroDivisors_eq_isUnit : ∀ (R : Type u_1) [inst : CommRing R] (K : Type u_5) [inst_1 : CommRing K] [inst_2 : Algebra R K] [IsFractionRing R K],
  nonZeroDivisors K = IsUnit.submonoid K
-- Mathlib.RingTheory.PiTensorProduct
PiTensorProduct.tprod_mul_tprod : ∀ {ι : Type u_1} {R : Type u_3} {A : ι → Type u_4} [inst : CommSemiring R]
  [inst_1 : (i : ι) → NonUnitalNonAssocSemiring (A i)] [inst_2 : (i : ι) → Module R (A i)]
  [inst_3 : ∀ (i : ι), SMulCommClass R (A i) (A i)] [inst_4 : ∀ (i : ι), IsScalarTower R (A i) (A i)]
  (x y : (i : ι) → A i), (PiTensorProduct.tprod R) x * (PiTensorProduct.tprod R) y = (PiTensorProduct.tprod R) (x * y)
-- Mathlib.Topology.Algebra.Order.Field
tendsto_inv_atBot_zero : ∀ {𝕜 : Type u_1} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [inst_3 : TopologicalSpace 𝕜]
  [OrderTopology 𝕜], Filter.Tendsto (fun r => r⁻¹) Filter.atBot (nhds 0)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.map_negY : ∀ {R : Type r} {S : Type s} [inst : CommRing R] [inst_1 : CommRing S] {W' : WeierstrassCurve.Projective R} (f : R →+* S)
  (P : Fin 3 → R), (W'.map f).negY (⇑f ∘ P) = f (W'.negY P)
-- Mathlib.GroupTheory.OrderOfElement
orderOf_dvd_of_mem_zpowers : ∀ {G : Type u_1} [inst : Group G] {x y : G}, y ∈ Subgroup.zpowers x → orderOf y ∣ orderOf x
-- Mathlib.NumberTheory.HeckeRing.Defs
/-- A *Hecke triple* `(H₁, Δ, H₂)`: the compatibility conditions on a submonoid `Δ` and a pair
of subgroups `H₁, H₂` of `G` making the double cosets `H₁\Δ/H₂` finite unions of left cosets:
both subgroups are contained in `Δ`, they are commensurable, and `Δ` commensurates them. The
classical Hecke pair `(H, Δ)` of [Shimura][shimura1971], Chapter 3, is the diagonal case
`IsHeckeTriple Δ H H`.  -/
IsHeckeTriple : {G : Type u_1} → [inst : Group G] → Submonoid G → Subgroup G → Subgroup G → Prop
-- Mathlib.CategoryTheory.Types.Basic
TypeCat.congr_arg : ∀ {X Y : Type u} (f : X ⟶ Y) {x x' : X},
  x = x' → (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom f) x'
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.isoWhiskerLeft_symm : ∀ {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] (F : CategoryTheory.Functor C D)
  {G H : CategoryTheory.Functor D E} (α : G ≅ H), (F.isoWhiskerLeft α).symm = F.isoWhiskerLeft α.symm
-- Mathlib.Combinatorics.Optimization.ValuedCSP
ValuedCSP.Term.mk.inj : ∀ {D : Type u_1} {C : Type u_2} {inst : AddCommMonoid C} {inst_1 : PartialOrder C} {inst_2 : IsOrderedAddMonoid C}
  {Γ : ValuedCSP D C} {ι : Type u_3} {n : ℕ} {f : (Fin n → D) → C} {inΓ : ⟨n, f⟩ ∈ Γ} {app : Fin n → ι} {n_1 : ℕ}
  {f_1 : (Fin n_1 → D) → C} {inΓ_1 : ⟨n_1, f_1⟩ ∈ Γ} {app_1 : Fin n_1 → ι},
  { n := n, f := f, inΓ := inΓ, app := app } = { n := n_1, f := f_1, inΓ := inΓ_1, app := app_1 } →
    n = n_1 ∧ f ≍ f_1 ∧ app ≍ app_1
-- Mathlib.Combinatorics.SimpleGraph.Hamiltonian
/-- A finite simple graph with a bridge is not hamiltonian.  -/
SimpleGraph.IsBridge.not_isHamiltonian : ∀ {α : Type u_1} [inst : DecidableEq α] {G : SimpleGraph α} [inst_1 : Fintype α] {e : Sym2 α},
  G.IsBridge e → ¬G.IsHamiltonian
-- Mathlib.Order.Minimal
/-- **Alias** of `image_monotone_setOfPred_maximal_mem`. -/
image_monotone_setOf_maximal_mem : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {s : Set α} {f : α → β},
  (∀ ⦃y x : α⦄, y ∈ s → x ∈ s → (f y ≤ f x ↔ y ≤ x)) →
    f '' {x | Maximal (fun x => x ∈ s) x} = {x | Maximal (fun x => x ∈ f '' s) x}
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
HasDerivAt.rpow : ∀ {f g : ℝ → ℝ} {f' g' x : ℝ},
  HasDerivAt f f' x →
    HasDerivAt g g' x →
      0 < f x → HasDerivAt (fun x => f x ^ g x) (f' * g x * f x ^ (g x - 1) + g' * f x ^ g x * Real.log (f x)) x
-- Mathlib.Computability.TuringMachine.PostTuringMachine
_private.Mathlib.Computability.TuringMachine.PostTuringMachine.0.Turing.TM0.step.match_1.eq_1 : ∀ {Γ : Type u_1} (motive : Turing.TM0.Stmt Γ → Sort u_2) (d : Turing.Dir)
  (h_1 : (d : Turing.Dir) → motive (Turing.TM0.Stmt.move d)) (h_2 : (a : Γ) → motive (Turing.TM0.Stmt.write a)),
  (match Turing.TM0.Stmt.move d with
    | Turing.TM0.Stmt.move d => h_1 d
    | Turing.TM0.Stmt.write a => h_2 a) =
    h_1 d
-- Init.Data.Nat.ToString
Nat.toDigits_of_base_le : ∀ {b n : ℕ}, 1 < b → b ≤ n → b.toDigits n = b.toDigits (n / b) ++ [(n % b).digitChar]
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.getEntryLT?_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  t₁.Equiv t₂ → t₁.getEntryLT? k = t₂.getEntryLT? k
-- Mathlib.NumberTheory.Padics.PadicVal.Basic
padicValRat.eq_1 : ∀ (p : ℕ) (q : ℚ), padicValRat p q = ↑(padicValInt p q.num) - ↑(padicValNat p q.den)
-- Lean.Elab.MutualDef
_private.Lean.Elab.MutualDef.0.Lean.Elab.Term.instantiateMVarsAtLetRecToLift : Lean.Elab.Term.LetRecToLift → Lean.Elab.TermElabM Lean.Elab.Term.LetRecToLift
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.getD_erase : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [EquivBEq α] [LawfulHashable α],
  (↑m).WF →
    ∀ {k a : α} {fallback : β},
      Std.DHashMap.Internal.Raw₀.Const.getD (m.erase k) a fallback =
        if (k == a) = true then fallback else Std.DHashMap.Internal.Raw₀.Const.getD m a fallback
-- Mathlib.AlgebraicGeometry.Morphisms.Separated
AlgebraicGeometry.IsAffineHom.comp_iff : ∀ {X Y Z : AlgebraicGeometry.Scheme} {f : X ⟶ Y} {g : Y ⟶ Z} [AlgebraicGeometry.IsAffineHom g],
  AlgebraicGeometry.IsAffineHom (CategoryTheory.CategoryStruct.comp f g) ↔ AlgebraicGeometry.IsAffineHom f
-- Lean.Elab.Tactic.BuiltinTactic
Lean.Elab.Tactic.evalSubstVars : Lean.Elab.Tactic.Tactic
-- Mathlib.Algebra.Polynomial.Coeff
Polynomial.coeff_X_pow : ∀ {R : Type u} [inst : Semiring R] (k n : ℕ), (Polynomial.X ^ k).coeff n = if n = k then 1 else 0
-- Mathlib.Order.Filter.FilterProduct
Filter.Germ.max_def : ∀ {α : Type u} {β : Type v} {φ : Ultrafilter α} [inst : LinearOrder β] (x y : (↑φ).Germ β),
  max x y = Filter.Germ.map₂ max x y
-- Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Subgroup.isCyclic_iff_exists_zpowers_eq_top : ∀ {α : Type u_1} [inst : Group α] (H : Subgroup α), IsCyclic ↥H ↔ ∃ g, Subgroup.zpowers g = H
-- Mathlib.Tactic.Widget.StringDiagram
/-- The RPC method for displaying string diagrams.  -/
Mathlib.Tactic.Widget.StringDiagram.rpc : ProofWidgets.PanelWidgetProps → Lean.Server.RequestM (Lean.Server.RequestTask ProofWidgets.Html)
-- Std.Net.Addr
Std.Net.SocketAddress.v6 : Std.Net.SocketAddressV6 → Std.Net.SocketAddress
-- Init.Grind.ToIntLemmas
Lean.Grind.ToInt.le_upper : ∀ {α : Type u_1} {i : Lean.Grind.IntInterval} [inst : Lean.Grind.ToInt α i] (hi' : ℤ),
  (i.hi? == some (-hi' + 1)) = true → ∀ (a : α), ↑a + hi' ≤ 0
-- Mathlib.Data.List.Lex
List.head_le_of_lt : ∀ {α : Type u} [inst : Preorder α] {a a' : α} {l l' : List α}, a' :: l' < a :: l → a' ≤ a
-- Mathlib.Data.List.Zip
List.unzip_swap : ∀ {α : Type u} {β : Type u_1} (l : List (α × β)), (List.map Prod.swap l).unzip = l.unzip.swap
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Over
CategoryTheory.Over.η_pullback_left : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] {X R : C}
  {f : R ⟶ X},
  CategoryTheory.Over.Hom.left (CategoryTheory.Functor.OplaxMonoidal.η (CategoryTheory.Over.pullback f)) =
    CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.id X) f
-- Mathlib.Order.RelIso.Basic
Quotient.mkRelHom_apply : ∀ {α : Type u_1} {x : Setoid α} {r : α → α → Prop} (H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂)
  (a : α), (Quotient.mkRelHom H) a = ⟦a⟧
-- Mathlib.Algebra.Group.Embedding
addLeftEmbedding.congr_simp : ∀ {G : Type u_1} [inst : Add G] [inst_1 : IsLeftCancelAdd G] (g g_1 : G),
  g = g_1 → addLeftEmbedding g = addLeftEmbedding g_1
-- Mathlib.Dynamics.TopologicalEntropy.Subset
Dynamics.coverMincard_monotone_subset : ∀ {X : Type u_1} (T : X → X) (U : SetRel X X) (n : ℕ), Monotone fun F => Dynamics.coverMincard T F U n
-- Init.Data.String.Lemmas.Basic
String.Slice.copy_pos : ∀ {s : String.Slice} {p : String.Pos.Raw} {h : String.Pos.Raw.IsValidForSlice s p}, (s.pos p h).copy = s.copy.pos p ⋯
-- Mathlib.Data.Set.Basic
Set.union_self : ∀ {α : Type u} (a : Set α), a ∪ a = a
-- Mathlib.Topology.Algebra.FilterBasis
AddGroupFilterBasis.addConj : ∀ {G : Type u} [inst : AddGroup G] {B : AddGroupFilterBasis G} (x₀ : G) {U : Set G},
  U ∈ B → ∃ V ∈ B, V ⊆ (fun x => x₀ + x + -x₀) ⁻¹' U
-- Mathlib.Topology.MetricSpace.DilationEquiv
DilationEquiv.coe_toHomeomorph : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] (e : X ≃ᵈ Y),
  ⇑e.toHomeomorph = ⇑e
-- Mathlib.Algebra.Group.Subgroup.Defs
AddSubgroup.le_normalizer : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G}, H ≤ AddSubgroup.normalizer ↑H
-- Init.Control.Except
/-- Adds exceptions of type `ε` to a monad `m`.
 -/
ExceptT : Type u → (Type u → Type v) → Type u → Type v
-- Mathlib.RingTheory.Polynomial.Pochhammer
ascPochhammer_succ_right : ∀ (S : Type u) [inst : Semiring S] (n : ℕ), ascPochhammer S (n + 1) = ascPochhammer S n * (Polynomial.X + ↑n)
-- Mathlib.LinearAlgebra.Matrix.PosDef
/-- For an invertible matrix `U`, `U * x * star U` is positive definite iff `x` is.
This works on any ⋆-ring with a partial order.

See `IsUnit.isStrictlyPositive_star_right_conjugate_iff` for a similar statement for star-ordered
rings. For matrices, positive definiteness is equivalent to strict positivity when the underlying
field is `ℝ` or `ℂ` (see `Matrix.isStrictlyPositive_iff_posDef`).  -/
Matrix.IsUnit.posDef_star_right_conjugate_iff : ∀ {n : Type u_2} {R : Type u_3} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] [inst_3 : Fintype n]
  [inst_4 : DecidableEq n] {x U : Matrix n n R}, IsUnit U → ((U * x * star U).PosDef ↔ x.PosDef)
-- Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
/-- If an `n`-th cyclotomic extension of `ℚ` contains a primitive `l`-th root of unity, then
`l ∣ 2 * n`.  -/
IsPrimitiveRoot.dvd_of_isCyclotomicExtension : ∀ (n : ℕ) [NeZero n] {K : Type u} [inst : Field K] [inst_1 : NumberField K] [IsCyclotomicExtension {n} ℚ K] {ζ : K}
  {l : ℕ}, IsPrimitiveRoot ζ l → l ≠ 0 → l ∣ 2 * n
-- Mathlib.RingTheory.MvPowerSeries.Order
/-- **Alias** of `MvPowerSeries.le_weightedOrder_mul`.

---

The `weightedOrder` of the product of two formal power series
is at least the sum of their orders.  -/
MvPowerSeries.weightedOrder_mul_ge : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] (w : σ → ℕ) {f g : MvPowerSeries σ R},
  MvPowerSeries.weightedOrder w f + MvPowerSeries.weightedOrder w g ≤ MvPowerSeries.weightedOrder w (f * g)
-- Mathlib.Data.Finset.Image
Finset.image_sdiff_of_injOn : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] {f : α → β} {s : Finset α} [inst_1 : DecidableEq α]
  {t : Finset α}, Set.InjOn f ↑s → t ⊆ s → Finset.image f (s \ t) = Finset.image f s \ Finset.image f t