mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.FieldTheory.Differential.Basic
Differential.logDeriv_pow : ∀ {R : Type u_1} [inst : Field R] [inst_1 : Differential R] (n : ℕ) (a : R),
  Differential.logDeriv (a ^ n) = ↑n * Differential.logDeriv a
-- Init.Data.Nat.Dvd
Nat.eq_zero_of_zero_dvd : ∀ {a : ℕ}, 0 ∣ a → a = 0
-- Mathlib.Algebra.Group.Nat.Units
Nat.unique_units : Unique ℕˣ
-- Mathlib.LinearAlgebra.TensorProduct.Map
TensorProduct.congr_mul : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_7} {N : Type u_8} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] (f : M ≃ₗ[R] M) (g : N ≃ₗ[R] N)
  (f' : M ≃ₗ[R] M) (g' : N ≃ₗ[R] N),
  TensorProduct.congr (f * f') (g * g') = TensorProduct.congr f g * TensorProduct.congr f' g'
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.smul_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α]
  [inst_3 : Ring β] {abv : β → α} [inst_4 : IsAbsoluteValue abv] {G : Type u_3} [inst_5 : SMul G β]
  [inst_6 : IsScalarTower G β β] (a : G) (f : CauSeq β abv) (i : ℕ), ↑(a • f) i = a • ↑f i
-- Mathlib.Data.Set.UnionLift
/-- `iUnionLift_unary` is useful for proving that `iUnionLift` is a homomorphism
of algebraic structures when defined on the Union of algebraic subobjects.
For example, it could be used to prove that the lift of a collection
of `LinearMap`s on a union of submodules preserves scalar multiplication.  -/
Set.iUnionLift_unary : ∀ {α : Type u_1} {ι : Sort u_2} {β : Sort u_3} {S : ι → Set α} {f : (i : ι) → ↑(S i) → β}
  {hf : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩} {T : Set α}
  (hT' : T = Set.iUnion S) (u : ↑T → ↑T) (ui : (i : ι) → ↑(S i) → ↑(S i)),
  (∀ (i : ι) (x : ↑(S i)), u (Set.inclusion ⋯ x) = Set.inclusion ⋯ (ui i x)) →
    ∀ (uβ : β → β),
      (∀ (i : ι) (x : ↑(S i)), f i (ui i x) = uβ (f i x)) →
        ∀ (x : ↑T), Set.iUnionLift S f hf T ⋯ (u x) = uβ (Set.iUnionLift S f hf T ⋯ x)
-- Mathlib.Algebra.Group.Action.Defs
AddSemiconjBy.vadd_left_iff : ∀ {G : Type u_3} {H : Type u_4} [inst : AddGroup G] [inst_1 : Add H] [inst_2 : AddAction G H] [VAddCommClass G H H]
  [VAddAssocClass G H H] {a b x : H} {r : G}, AddSemiconjBy (r +ᵥ x) a b ↔ AddSemiconjBy x a b
-- Mathlib.Order.SupIndep
/-- Bind operation for `SupIndep`.  -/
Finset.SupIndep.sigma : ∀ {α : Type u_1} {ι : Type u_3} [inst : Lattice α] [IsModularLattice α] [inst_2 : OrderBot α] {β : ι → Type u_5}
  {s : Finset ι} {g : (i : ι) → Finset (β i)} {f : Sigma β → α},
  (s.SupIndep fun i => (g i).sup fun b => f ⟨i, b⟩) →
    (∀ i ∈ s, (g i).SupIndep fun b => f ⟨i, b⟩) → (s.sigma g).SupIndep f
-- Lean.Elab.PreDefinition.TerminationHint
Lean.Elab.instInhabitedTerminationBy.default : Lean.Elab.TerminationBy
-- Mathlib.Order.CompleteLattice.Finset
/-- Union of an indexed family of sets `s : ι → Set α` is equal to the union of the unions
of finite subfamilies. This version assumes `ι : Type*`. See also `iUnion_eq_iUnion_finset'` for
a version that works for `ι : Sort*`.  -/
Set.iUnion_eq_iUnion_finset : ∀ {α : Type u_2} {ι : Type u_5} (s : ι → Set α), ⋃ i, s i = ⋃ t, ⋃ i ∈ t, s i
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.reorder.inj : ∀ {c c_1 : Lean.Meta.Grind.Arith.Cutsat.DvdCnstr},
  Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.reorder c = Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.reorder c_1 →
    c = c_1
-- Mathlib.RingTheory.PiTensorProduct
PiTensorProduct.smul_tprod_mul_smul_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)] (r s : R)
  (x y : (i : ι) → A i),
  r • (PiTensorProduct.tprod R) x * s • (PiTensorProduct.tprod R) y = (r * s) • (PiTensorProduct.tprod R) (x * y)
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.coe_toContinuousMap : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : Zero β]
  (f : CompactlySupportedContinuousMap α β), ⇑f.toContinuousMap = ⇑f
-- Mathlib.Tactic.FunProp.FunctionData
Mathlib.Meta.FunProp.MorApplication.overApplied.sizeOf_spec : sizeOf Mathlib.Meta.FunProp.MorApplication.overApplied = 1
-- Mathlib.Probability.Independence.Conditional
ProbabilityTheory.condIndepSets_singleton_iff : ∀ {Ω : Type u_1} (m' : MeasurableSpace Ω) {mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω] (hm' : m' ≤ mΩ)
  {μ : MeasureTheory.Measure Ω} [inst_1 : MeasureTheory.IsFiniteMeasure μ] {s t : Set Ω},
  MeasurableSet s →
    MeasurableSet t →
      (ProbabilityTheory.CondIndepSets m' hm' {s} {t} μ ↔
        μ[(s ∩ t).indicator fun ω => 1 | m'] =ᵐ[μ] μ[s.indicator fun ω => 1 | m'] * μ[t.indicator fun ω => 1 | m'])
-- Mathlib.Order.CompleteLattice.Basic
iSup_eq_dif : ∀ {α : Type u_1} [inst : CompleteLattice α] {p : Prop} [inst_1 : Decidable p] (a : p → α),
  ⨆ (h : p), a h = if h : p then a h else ⊥
-- Mathlib.Algebra.Category.Grp.Basic
AddCommGrpCat.asHom_hom_apply : ∀ {G : AddCommGrpCat} (g : ↑G) (n : ℤ), (AddCommGrpCat.Hom.hom (AddCommGrpCat.asHom g)) n = n • g
-- Mathlib.Analysis.Calculus.LocalExtr.Basic
/-- **Fermat's Theorem**: the derivative of a function at a local extremum equals zero.  -/
IsLocalExtr.fderiv_eq_zero : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {a : E},
  IsLocalExtr f a → fderiv ℝ f a = 0
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.leadCoeff : Int.Internal.Linear.Poly → ℤ
-- Lean.Declaration
Lean.instBEqAxiomVal : BEq Lean.AxiomVal
-- Mathlib.Analysis.Complex.Basic
imaginaryPart.norm_le : ∀ {A : Type u_1} [inst : SeminormedAddCommGroup A] [inst_1 : StarAddMonoid A] [inst_2 : NormedSpace ℂ A]
  [inst_3 : StarModule ℂ A] [NormedStarGroup A] (x : A), ‖imaginaryPart x‖ ≤ ‖x‖
-- Mathlib.Combinatorics.SimpleGraph.Partition
SimpleGraph.partitionable_iff_colorable : ∀ {V : Type u} {G : SimpleGraph V} {n : ℕ}, G.Partitionable n ↔ G.Colorable n
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
/-- This is equivalent to the type `Over.mk s ⟶ Over.mk η`, but that lives in the wrong universe.
However, if `F = yoneda.obj Y` for some `Y`, then (using that the Yoneda embedding is fully
faithful) we get a good statement, see `OverArrow.costructuredArrowIso`.  -/
CategoryTheory.OverPresheafAux.OverArrows : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A F : CategoryTheory.Functor Cᵒᵖ (Type v)} → (F ⟶ A) → {X : C} → (CategoryTheory.yoneda.obj X ⟶ A) → Type v
-- Mathlib.Geometry.Convex.Cone.Pointed
/-- A pointed cone is salient iff the intersection of the cone with its negative
is the set `{0}`.  -/
PointedCone.salient_iff_inter_neg_eq_singleton : ∀ {R : Type u_1} {E : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommGroup E] [inst_4 : Module R E] (C : PointedCone R E), (↑C).Salient ↔ ↑C ∩ -↑C = {0}
-- Plausible.Testable
Plausible.«command#test_» : Lean.ParserDescr
-- Mathlib.Analysis.SpecialFunctions.Arcosh
Real.cosh_surjOn : Set.SurjOn Real.cosh (Set.Ici 0) (Set.Ici 1)
-- Std.Data.HashMap.Lemmas
Std.HashMap.contains_ofList : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k : α},
  (Std.HashMap.ofList l).contains k = (List.map Prod.fst l).contains k
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
/-- The `vectorSpan` of an indexed family is the span of the pairwise subtractions with a given
point on the right, excluding the subtraction of that point from itself.  -/
vectorSpan_range_eq_span_range_vsub_right_ne : ∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {ι : Type u_4} (p : ι → P) (i₀ : ι),
  vectorSpan k (Set.range p) = Submodule.span k (Set.range fun i => p ↑i -ᵥ p i₀)
-- Mathlib.Data.Nat.Bits
Nat.div2_one : Nat.div2 1 = 0
-- Mathlib.Combinatorics.Matroid.Basic
/-- A family of sets with the exchange property is an antichain.  -/
Matroid.ExchangeProperty.antichain : ∀ {α : Type u_1} {IsBase : Set α → Prop} {B B' : Set α},
  Matroid.ExchangeProperty IsBase → IsBase B → IsBase B' → B ⊆ B' → B = B'
-- Mathlib.Algebra.Order.Monovary
Antivary.div_left₀ : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Semifield α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α]
  [inst_3 : LinearOrder β] {f₁ f₂ : ι → α} {g : ι → β},
  0 ≤ f₁ → StrongLT 0 f₂ → Antivary f₁ g → Monovary f₂ g → Antivary (f₁ / f₂) g
-- Init.Data.Slice.Array.Lemmas
Array.array_mkSlice_ric : ∀ {α : Type u_1} {xs : Array α} {hi : ℕ}, (Std.Ric.Sliceable.mkSlice xs *...=hi).array = xs
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
ContinuousLinearMapWOT.linearEquiv_symm_apply_toCLM : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_3}
  {F : Type u_4} [inst_2 : AddCommGroup E] [inst_3 : TopologicalSpace E] [inst_4 : Module 𝕜₁ E]
  [inst_5 : AddCommGroup F] [inst_6 : TopologicalSpace F] [inst_7 : Module 𝕜₂ F] (S : Type u_5) [inst_8 : Semiring S]
  [inst_9 : Module S F] [inst_10 : SMulCommClass 𝕜₂ S F] [inst_11 : ContinuousConstSMul S F]
  [inst_12 : IsTopologicalAddGroup F] (a : E →SL[σ] F), ((ContinuousLinearMapWOT.linearEquiv S).symm a).toCLM = a
-- Lean.Meta.Sym.Canon
/-- Returns `true` if `e` is a Nat arithmetic expression that should be normalized
(ground evaluation or offset normalization).  -/
_private.Lean.Meta.Sym.Canon.0.Lean.Meta.Sym.Canon.isNatArithApp : Lean.Expr → Bool
-- Mathlib.Topology.Connected.PathConnected
JoinedIn.add : ∀ {M : Type u_4} [inst : Add M] [inst_1 : TopologicalSpace M] [ContinuousAdd M] {s t : Set M} {a b c d : M},
  JoinedIn s a b → JoinedIn t c d → JoinedIn (s + t) (a + c) (b + d)
-- Mathlib.Analysis.Normed.Module.Complemented
/-- If `f : E →L[R] F` and `g : E →L[R] G` are two surjective linear maps and
their kernels are complement of each other, then `x ↦ (f x, g x)` defines
a linear equivalence `E ≃L[R] F × G`.  -/
ContinuousLinearMap.equivProdOfSurjectiveOfIsCompl : {𝕜 : 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] →
                      [CompleteSpace E] →
                        [CompleteSpace (F × G)] →
                          (f : E →L[𝕜] F) →
                            (g : E →L[𝕜] G) →
                              (↑f).range = ⊤ → (↑g).range = ⊤ → IsCompl (↑f).ker (↑g).ker → E ≃L[𝕜] F × G
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgEquiv.toNonUnitalStarAlgHom_refl : ∀ {R : Type u_1} {A₁ : Type u_2} [inst : Monoid R] [inst_1 : NonUnitalNonAssocSemiring A₁]
  [inst_2 : DistribMulAction R A₁] [inst_3 : Star A₁],
  (StarAlgEquiv.refl R A₁).toNonUnitalStarAlgHom = NonUnitalStarAlgHom.id R A₁
-- Mathlib.Topology.LocallyConstant.Basic
LocallyConstant.mk.sizeOf_spec : ∀ {X : Type u_5} {Y : Type u_6} [inst : TopologicalSpace X] [inst_1 : SizeOf X] [inst_2 : SizeOf Y] (toFun : X → Y)
  (isLocallyConstant : IsLocallyConstant toFun), sizeOf { toFun := toFun, isLocallyConstant := isLocallyConstant } = 1
-- Std.Data.ExtDTreeMap.Basic
/-- Tries to retrieve the key-value pair with the largest key that is less than or equal to the
given key, panicking if no such pair exists.
 -/
Std.ExtDTreeMap.getEntryLE! : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} → [Std.TransCmp cmp] → [Inhabited (Sigma β)] → Std.ExtDTreeMap α β cmp → α → (a : α) × β a
-- Mathlib.Order.JordanHolder
JordanHolderLattice.isMaximal_of_eq_inf : ∀ {X : Type u} [inst : Lattice X] [inst_1 : JordanHolderLattice X] (x b : X) {a y : X},
  x ⊓ y = a →
    x ≠ y → JordanHolderLattice.IsMaximal x b → JordanHolderLattice.IsMaximal y b → JordanHolderLattice.IsMaximal a y
-- Init.Data.List.Sublist
_private.Init.Data.List.Sublist.0.List.getLast?.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (a : α) (as : List α) (h_1 : Unit → motive [])
  (h_2 : (a : α) → (as : List α) → motive (a :: as)),
  (match a :: as with
    | [] => h_1 ()
    | a :: as => h_2 a as) =
    h_2 a as
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.distribSMul : {R : Type u_1} →
  {M : Type u_4} → {N : Type u_5} → [inst : Semiring R] → [DistribSMul N R] → DistribSMul N (MonoidAlgebra R M)
-- Mathlib.Analysis.Normed.Lp.ProdLp
IsometryEquiv.withLpProdAssoc_apply : ∀ (p : ENNReal) (α : Type u_2) (β : Type u_3) (γ : Type u_4) [hp : Fact (1 ≤ p)] [inst : PseudoEMetricSpace α]
  [inst_1 : PseudoEMetricSpace β] [inst_2 : PseudoEMetricSpace γ] (x : WithLp p (WithLp p (α × β) × γ)),
  (IsometryEquiv.withLpProdAssoc p α β γ) x = WithLp.toLp p (x.fst.fst, WithLp.toLp p (x.fst.snd, x.snd))
-- Mathlib.Analysis.SpecialFunctions.Complex.Arg
Complex.continuousWithinAt_arg_of_re_neg_of_im_zero : ∀ {z : ℂ}, z.re < 0 → z.im = 0 → ContinuousWithinAt Complex.arg {z | 0 ≤ z.im} z
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.TGrind : Type
-- Mathlib.Algebra.Order.Group.Synonym
isAddLeftRegular_toDual : ∀ {α : Type u_1} [inst : AddMonoid α] {a : α}, IsAddLeftRegular (OrderDual.toDual a) ↔ IsAddLeftRegular a
-- Init.Data.Option.Lemmas
Option.or_self : ∀ {α : Type u_1} {o : Option α}, o.or o = o
-- Lean.Elab.RecAppSyntax
_private.Lean.Elab.RecAppSyntax.0.Lean.recAppKey : Lean.Name
-- Mathlib.CategoryTheory.Monad.Basic
/-- The counit for the comonad.  -/
CategoryTheory.Comonad.ε : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (self : CategoryTheory.Comonad C) → self.toFunctor ⟶ CategoryTheory.Functor.id C
-- Mathlib.Topology.Homeomorph.Defs
Homeomorph.coinduced_eq : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (h : X ≃ₜ Y),
  TopologicalSpace.coinduced (⇑h) inst = inst_1
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.equiv_iff_keys_perm_keys : ∀ {α : Type u} (m₁ m₂ : Std.DHashMap.Raw α fun x => Unit), m₁.Equiv m₂ ↔ m₁.keys.Perm m₂.keys
-- Std.Http.Data.Headers.Basic
/-- Host name (reg-name, IPv4, or IPv6 literal).
 -/
Std.Http.Header.Host.host : Std.Http.Header.Host → Std.Http.URI.Host
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.fullSubcategory_associator_inv_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {P : CategoryTheory.ObjectProperty C} [inst_2 : P.IsClosedUnderLimitsOfShape (CategoryTheory.Discrete PEmpty.{1})]
  [inst_3 : P.IsClosedUnderLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair)]
  (X Y Z : P.FullSubcategory),
  (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv.hom =
    (CategoryTheory.MonoidalCategoryStruct.associator X.obj Y.obj Z.obj).inv
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.ModuleDiscrTreeRef.mk.sizeOf_spec : ∀ {α : Type} [inst : SizeOf α] (ref : IO.Ref (Lean.Meta.LazyDiscrTree α)), sizeOf { ref := ref } = 1 + sizeOf ref
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.isEmpty_modify : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {k : α}
  {f : β k → β k}, (m.modify k f).isEmpty = m.isEmpty
-- Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn
/-- This is a version of `hasProdLocallyUniformlyOn_one_add` for sequences indexed by `ℕ`.  -/
Summable.hasProdLocallyUniformlyOn_nat_one_add : ∀ {α : Type u_1} {K : Set α} {R : Type u_3} [inst : NormedCommRing R] [NormOneClass R] [CompleteSpace R]
  [inst_3 : TopologicalSpace α] [LocallyCompactSpace α] {f : ℕ → α → R},
  IsOpen K →
    ∀ {u : ℕ → ℝ},
      Summable u →
        (∀ᶠ (n : ℕ) in Filter.atTop, ∀ x ∈ K, ‖f n x‖ ≤ u n) →
          (∀ (n : ℕ), ContinuousOn (f n) K) →
            HasProdLocallyUniformlyOn (fun n x => 1 + f n x) (fun x => ∏' (i : ℕ), (1 + f i x)) K
-- Mathlib.Computability.RegularExpressions
RegularExpression.matchEpsilon.eq_3 : ∀ {α : Type u_1} (a : α), (RegularExpression.char a).matchEpsilon = false
-- Mathlib.RingTheory.TensorProduct.IsBaseChangeHom
IsBaseChange.endHom_one : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_2} [inst_1 : CommSemiring S] [inst_2 : Algebra R S] {M : Type u_3}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] {P : Type u_5} [inst_5 : AddCommMonoid P] [inst_6 : Module R P]
  [inst_7 : Module S P] [inst_8 : IsScalarTower R S P] {α : M →ₗ[R] P} (j : IsBaseChange S α), j.endHom 1 = 1
-- Mathlib.RingTheory.Spectrum.Prime.FreeLocus
Module.mem_freeLocus_iff_tensor : ∀ {R : Type uR} {M : Type uM} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (p : PrimeSpectrum R)
  (Rₚ : Type u_1) [inst_3 : CommRing Rₚ] [inst_4 : Algebra R Rₚ] [IsLocalization.AtPrime Rₚ p.asIdeal],
  p ∈ Module.freeLocus R M ↔ Module.Free Rₚ (TensorProduct R Rₚ M)
-- Mathlib.Tactic.ClickSuggestions.Apply
Mathlib.Tactic.ClickSuggestions.ApplyKey.mk.inj : ∀ {numGoals nameLength replacementSize : ℕ} {name : String} {newGoals : Array Lean.Meta.AbstractMVarsResult}
  {numGoals_1 nameLength_1 replacementSize_1 : ℕ} {name_1 : String} {newGoals_1 : Array Lean.Meta.AbstractMVarsResult},
  { numGoals := numGoals, nameLength := nameLength, replacementSize := replacementSize, name := name,
        newGoals := newGoals } =
      { numGoals := numGoals_1, nameLength := nameLength_1, replacementSize := replacementSize_1, name := name_1,
        newGoals := newGoals_1 } →
    numGoals = numGoals_1 ∧
      nameLength = nameLength_1 ∧ replacementSize = replacementSize_1 ∧ name = name_1 ∧ newGoals = newGoals_1
-- Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
Complex.differentiable_Gammaℝ_inv : Differentiable ℂ fun s => s.Gammaℝ⁻¹
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
/-- The left fraction corresponding to a right fraction in the opposite category.  -/
CategoryTheory.MorphismProperty.RightFraction.unop : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {W : CategoryTheory.MorphismProperty Cᵒᵖ} →
      {X Y : Cᵒᵖ} → W.RightFraction X Y → W.unop.LeftFraction (Opposite.unop Y) (Opposite.unop X)
-- Std.Internal.Do.ExceptPost
/-- Extract a tail ordering from an `EPost.Cons` ordering.  -/
Std.Internal.Do.EPost.Cons.le_tail : ∀ {eh : Type u_1} {et : Type u_2} [inst : Lean.Order.PartialOrder eh] [inst_1 : Lean.Order.PartialOrder et]
  {p q : EPost.Cons✝ eh et}, Lean.Order.PartialOrder.rel p q → Lean.Order.PartialOrder.rel p.tail q.tail
-- Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
minpoly.instIsScalarTowerSubtypeMemSubringSubalgebraIntegralClosure : ∀ {K : Type u_3} {L : Type u_4} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (A : Subring K),
  IsScalarTower (↥A) (↥(integralClosure (↥A) L)) L
-- Init.Data.String.Lemmas.IsEmpty
String.startPos_ne_endPos : ∀ {s : String}, s ≠ "" → s.startPos ≠ s.endPos
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Expr.toPoly.eq_13 : ∀ (a : Lean.Grind.CommRing.Expr) (k : ℕ),
  (∀ (n : ℤ), a = Lean.Grind.CommRing.Expr.num n → False) →
    (∀ (n : ℤ), a = Lean.Grind.CommRing.Expr.intCast n → False) →
      (∀ (n : ℕ), a = Lean.Grind.CommRing.Expr.natCast n → False) →
        (∀ (x : Lean.Grind.CommRing.Var), a = Lean.Grind.CommRing.Expr.var x → False) →
          (a.pow k).toPoly = bif k == 0 then Lean.Grind.CommRing.Poly.num 1 else a.toPoly.pow k
-- Mathlib.LinearAlgebra.TensorPower.Symmetric
/-- The `n`th symmetric tensor power of a semimodule `M` over a commutative semiring `R`  -/
TensorProduct.«termSym[_]^__» : Lean.ParserDescr
-- Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Defs
/-- Sum `f lo + ... + f (n - 1)`. Returns zero when `n <= lo`.  -/
BirdDet.sumFrom : {R : Type u_1} → [CommRing R] → ℕ → ℕ → (ℕ → R) → R
-- Mathlib.Data.Int.Bitwise
Int.bodd_one : Int.bodd 1 = true
-- Lean.Elab.DocString
/-- After fixing up the references, check to see which were not used and emit a suitable warning.
 -/
_private.Lean.Elab.DocString.0.Lean.Doc.warnUnusedRefs : Lean.Doc.DocM Unit
-- Mathlib.Order.DirSupClosed
IsLowerSet.dirSupInaccOn : ∀ {α : Type u_1} {s : Set α} {D : Set (Set α)} [inst : Preorder α], IsLowerSet s → DirSupInaccOn D s
-- Mathlib.FieldTheory.Minpoly.MinpolyDiv
coeff_minpolyDiv_sub_pow_mem_span : ∀ {R : Type u_2} {S : Type u_1} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {x : S},
  IsIntegral R x →
    ∀ {i : ℕ},
      i ≤ (minpolyDiv R x).natDegree →
        (minpolyDiv R x).coeff ((minpolyDiv R x).natDegree - i) - x ^ i ∈
          Submodule.span R ((fun x_1 => x ^ x_1) '' Set.Iio i)
-- Init.Prelude
/-- Lean syntax trees.

Syntax trees are used pervasively throughout Lean: they are produced by the parser, transformed by
the macro expander, and elaborated. They are also produced by the delaborator and presented to
users.
 -/
Lean.Syntax : Type
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
/-- Express `f n` as `f 0` plus the telescoping sum of consecutive differences from
`0` to `n - 1`.  -/
Finset.eq_sum_range_sub : ∀ {G : Type u_3} [inst : AddCommGroup G] (f : ℕ → G) (n : ℕ), f n = f 0 + ∑ i ∈ Finset.range n, (f (i + 1) - f i)
-- Std.Data.HashMap.IteratorLemmas
_private.Std.Data.HashMap.IteratorLemmas.0.Std.HashMap.keysIter.eq_1 : ∀ {α β : Type u} [inst : BEq α] [inst_1 : Hashable α] (m : Std.HashMap α β), m.keysIter = m.inner.keysIter
-- Mathlib.CategoryTheory.Iso
CategoryTheory.Iso.inv_eq_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f g : X ≅ Y), f.inv = g.inv ↔ f.hom = g.hom
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps
ContinuousMap.Homotopy.eq_diag_path : ∀ {X Y : TopCat} {f g : C(↑X, ↑Y)} (H : f.Homotopy g) {x₀ x₁ : ↑X}
  (p : FundamentalGroupoid.fromTop x₀ ⟶ FundamentalGroupoid.fromTop x₁),
  CategoryTheory.CategoryStruct.comp ((FundamentalGroupoid.fundamentalGroupoidFunctor.map (TopCat.ofHom f)).map p)
        ⟦H.evalAt x₁⟧ =
      H.diagonalPath' p ∧
    CategoryTheory.CategoryStruct.comp ⟦H.evalAt x₀⟧
        ((FundamentalGroupoid.fundamentalGroupoidFunctor.map (TopCat.ofHom g)).map p) =
      H.diagonalPath' p
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
WeierstrassCurve.baseChange_Ψ₂Sq : ∀ {R : Type r} {S : Type s} [inst : CommRing R] [inst_1 : CommRing S] (W : WeierstrassCurve R) [inst_2 : Algebra R S]
  {A : Type u} [inst_3 : CommRing A] [inst_4 : Algebra R A] [inst_5 : Algebra S A] [IsScalarTower R S A] {B : Type v}
  [inst_7 : CommRing B] [inst_8 : Algebra R B] [inst_9 : Algebra S B] [IsScalarTower R S B] (f : A →ₐ[S] B),
  (W.baseChange B).Ψ₂Sq = Polynomial.map (↑f) (W.baseChange A).Ψ₂Sq
-- Mathlib.Topology.SeparatedMap
Continuous.mapPullback : ∀ {X₁ : Type u_1} {X₂ : Type u_2} {Y₁ : Sort u_3} {Y₂ : Sort u_4} {Z₁ : Type u_5} {Z₂ : Type u_6}
  [inst : TopologicalSpace X₁] [inst_1 : TopologicalSpace X₂] [inst_2 : TopologicalSpace Z₁]
  [inst_3 : TopologicalSpace Z₂] {f₁ : X₁ → Y₁} {g₁ : Z₁ → Y₁} {f₂ : X₂ → Y₂} {g₂ : Z₂ → Y₂} {mapX : X₁ → X₂},
  Continuous mapX →
    ∀ {mapY : Y₁ → Y₂} {mapZ : Z₁ → Z₂},
      Continuous mapZ →
        ∀ {commX : f₂ ∘ mapX = mapY ∘ f₁} {commZ : g₂ ∘ mapZ = mapY ∘ g₁},
          Continuous (Function.mapPullback mapX mapY mapZ commX commZ)
-- Mathlib.Topology.Order.Monotone
/-- If a function is monotone on a set in a second countable topological space, then there
are only countably many points that have several preimages.  -/
MonotoneOn.countable_setOfPred_two_preimages : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α]
  [inst_3 : LinearOrder β] {s : Set α} {f : α → β} [SecondCountableTopology α],
  MonotoneOn f s → {c | ∃ x y, x ∈ s ∧ y ∈ s ∧ x < y ∧ f x = c ∧ f y = c}.Countable
-- Init.Data.Rat.Lemmas
Rat.ceil_le_iff : ∀ {x : ℚ} {y : ℤ}, x.ceil ≤ y ↔ x ≤ ↑y
-- Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
/-- The binary coproduct of `X` and `Y` is disjoint if the coproduct of the family `{X, Y}` is
disjoint.  -/
CategoryTheory.Limits.BinaryCoproductDisjoint : {C : Type u} → [CategoryTheory.Category.{v, u} C] → C → C → Prop