mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Ring.Hom.Defs
NonUnitalRingHom.mk_coe : ∀ {α : Type u_2} {β : Type u_3} [inst : NonUnitalNonAssocSemiring α] [inst_1 : NonUnitalNonAssocSemiring β]
  (f : α →ₙ+* β) (h₁ : ∀ (x y : α), f (x * y) = f x * f y) (h₂ : { toFun := ⇑f, map_mul' := h₁ }.toFun 0 = 0)
  (h₃ :
    ∀ (x y : α),
      { toFun := ⇑f, map_mul' := h₁ }.toFun (x + y) =
        { toFun := ⇑f, map_mul' := h₁ }.toFun x + { toFun := ⇑f, map_mul' := h₁ }.toFun y),
  { toFun := ⇑f, map_mul' := h₁, map_zero' := h₂, map_add' := h₃ } = f
-- Mathlib.MeasureTheory.Function.UniformIntegrable
MeasureTheory.UnifIntegrable.add : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup β] {f g : ι → α → β} {p : ENNReal},
  MeasureTheory.UnifIntegrable f p μ →
    MeasureTheory.UnifIntegrable g p μ →
      1 ≤ p →
        (∀ (i : ι), MeasureTheory.AEStronglyMeasurable (f i) μ) →
          (∀ (i : ι), MeasureTheory.AEStronglyMeasurable (g i) μ) → MeasureTheory.UnifIntegrable (f + g) p μ
-- Init.Data.Ord.Basic
Ordering.then'_eq_then : ∀ (a b : Ordering), a.then' b = a.then b
-- Mathlib.Analysis.Real.OfDigits
Real.ofDigits_eq_sum_add_ofDigits : ∀ {b : ℕ} (a : ℕ → Fin b) (n : ℕ),
  Real.ofDigits a = ∑ i ∈ Finset.range n, Real.ofDigitsTerm a i + (↑b ^ n)⁻¹ * Real.ofDigits fun i => a (i + n)
-- Mathlib.MeasureTheory.Measure.Haar.OfBasis
Module.Basis.addHaar_def : ∀ {ι : Type u_5} {E : Type u_6} [inst : Fintype ι] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E]
  [inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E] (b : Module.Basis ι ℝ E),
  b.addHaar = MeasureTheory.Measure.addHaarMeasure b.parallelepiped
-- Lean.Language.Basic
/-- Creates a `DynamicSnapshot` from a typed snapshot value.  -/
Lean.Language.DynamicSnapshot.ofTyped : {α : Type} → [TypeName α] → [Lean.Language.ToSnapshotTree α] → α → Lean.Language.DynamicSnapshot
-- Mathlib.Probability.Process.Stopping
MeasureTheory.stoppedProcess_add : ∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : Nonempty ι] {u v : ι → Ω → β} {τ : Ω → WithTop ι}
  [inst_1 : LinearOrder ι] [inst_2 : Add β],
  MeasureTheory.stoppedProcess (u + v) τ = MeasureTheory.stoppedProcess u τ + MeasureTheory.stoppedProcess v τ
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
measurableSet_Icc : ∀ {α : Type u_1} [inst : TopologicalSpace α] {mα : MeasurableSpace α} [OpensMeasurableSpace α] [inst_2 : Preorder α]
  {a b : α} [OrderClosedTopology α], MeasurableSet (Set.Icc a b)
-- Mathlib.GroupTheory.GroupAction.Blocks
MulAction.isBlock_iff_smul_eq_or_disjoint : ∀ {G : Type u_1} [inst : Group G] {X : Type u_2} [inst_1 : MulAction G X] {B : Set X},
  MulAction.IsBlock G B ↔ ∀ (g : G), g • B = B ∨ Disjoint (g • B) B
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey?_inter_of_not_mem_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α}, k ∉ t₁ → (t₁ ∩ t₂).getKey? k = none
-- Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Associates.instLattice : {α : Type u_1} → [inst : CommMonoidWithZero α] → [UniqueFactorizationMonoid α] → Lattice (Associates α)
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
Finsupp.sum_onFinset : ∀ {α : Type u_1} {M : Type u_8} {N : Type u_10} [inst : Zero M] [inst_1 : AddCommMonoid N] (s : Finset α) (f : α → M)
  (hf : ∀ (a : α), f a ≠ 0 → a ∈ s) (g : α → M → N),
  (∀ i ∈ s, g i 0 = 0) → (Finsupp.onFinset s f hf).sum g = ∑ a ∈ s, g a (f a)
-- Mathlib.Analysis.RCLike.Basic
RCLike.normSq_one : ∀ {K : Type u_1} [inst : RCLike K], RCLike.normSq 1 = 1
-- Mathlib.Data.Finset.Max
Finset.exists_max_image : ∀ {α : Type u_2} {β : Type u_3} [inst : LinearOrder α] (s : Finset β) (f : β → α),
  s.Nonempty → ∃ x ∈ s, ∀ x' ∈ s, f x' ≤ f x
-- Std.Internal.Parsec.String
/-- Parse one or more ASCII digits into a `Nat`.
 -/
Std.Internal.Parsec.String.digits : Std.Internal.Parsec.String.Parser ℕ
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.UnfoldLift.monadLift_trans : ∀ {m : Type u → Type v} {n : Type u → Type u_1} {o : Type u → Type u_2} {α : Type u} [inst : MonadLift n o]
  [inst_1 : MonadLiftT m n] (x : m α), monadLift x = MonadLift.monadLift (monadLift x)
-- Lean.Data.Lsp.Extra
Lean.Lsp.RpcCallParams.sessionId : Lean.Lsp.RpcCallParams → UInt64
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
LinearIsometryEquiv.lTensor_def : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : InnerProductSpace 𝕜 G] (f : F ≃ₗᵢ[𝕜] G),
  LinearIsometryEquiv.lTensor E f = TensorProduct.congrIsometry (LinearIsometryEquiv.refl 𝕜 E) f
-- Init.Data.Option.Lemmas
Option.le_none : ∀ {α : Type u_1} [inst : LE α] {a : Option α}, a ≤ none ↔ a = none
-- Mathlib.RingTheory.SurjectiveOnStalks
RingHom.surjectiveOnStalks_of_surjective : ∀ {R : Type u_1} [inst : CommRing R] {S : Type u_2} [inst_1 : CommRing S] {f : R →+* S},
  Function.Surjective ⇑f → f.SurjectiveOnStalks
-- Init.Data.Int.Linear
Int.Internal.Linear.diseq_norm : ∀ (ctx : Int.Internal.Linear.Context) (p₁ p₂ : Int.Internal.Linear.Poly),
  p₁.norm.beq' p₂ = true → Int.Internal.Linear.Poly.denote' ctx p₁ ≠ 0 → Int.Internal.Linear.Poly.denote' ctx p₂ ≠ 0
-- Mathlib.Algebra.Free
/-- Representation of an element of a free additive magma.  -/
FreeAddMagma.repr : {α : Type u} → [Repr α] → FreeAddMagma α → Std.Format
-- Lean.Syntax
Lean.Syntax.Traverser.setCur : Lean.Syntax.Traverser → Lean.Syntax → Lean.Syntax.Traverser
-- Mathlib.LinearAlgebra.RootSystem.IsValuedIn
RootPairing.IsValuedIn.trans : ∀ {ι : 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_6)
  [inst_5 : CommRing S] [inst_6 : Algebra S R] (T : Type u_7) [inst_7 : CommRing T] [inst_8 : Algebra T S]
  [inst_9 : Algebra T R] [IsScalarTower T S R] [P.IsValuedIn T], P.IsValuedIn S
-- Lean.Elab.InfoTree.Types
Lean.Elab.ElabInfo.mk : Lean.Name → Lean.Syntax → Lean.Elab.ElabInfo
-- Std.Data.ExtDTreeMap.Basic
/-- Given a proof that such a mapping exists, retrieves the key-value pair with the smallest key that is
greater than or equal to the given key.
 -/
Std.ExtDTreeMap.getEntryGE : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} →
      [inst : Std.TransCmp cmp] →
        (t : Std.ExtDTreeMap α β cmp) → (k : α) → (∃ a ∈ t, (cmp a k).isGE = true) → (a : α) × β a
-- Mathlib.CategoryTheory.Sites.Grothendieck
CategoryTheory.GrothendieckTopology.eq_top_of_isEmpty : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [IsEmpty C] (J : CategoryTheory.GrothendieckTopology C), J = ⊤
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
/-- A chosen `S.RightHomologyData` for a short complex `S` that has right homology  -/
CategoryTheory.ShortComplex.rightHomologyData : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      (S : CategoryTheory.ShortComplex C) → [S.HasRightHomology] → S.RightHomologyData
-- Mathlib.Data.Seq.Basic
Stream'.Seq.length_cons : ∀ {α : Type u} {x : α} {s : Stream'.Seq α} (h : s.Terminates), (Stream'.Seq.cons x s).length ⋯ = s.length h + 1
-- Init.WF
/-- A well-founded fixpoint. If satisfying the motive `C` for all values that are smaller according to a
well-founded relation allows it to be satisfied for the current value, then it is satisfied for all
values.

This function is used as part of the elaboration of well-founded recursion.
 -/
WellFounded.fix : {α : Sort u} →
  {C : α → Sort v} → {r : α → α → Prop} → WellFounded r → ((x : α) → ((y : α) → r y x → C y) → C x) → (x : α) → C x
-- Std.Net.Addr
Std.Net.SocketAddressV6.mk.sizeOf_spec : ∀ (addr : Std.Net.IPv6Addr) (port : UInt16), sizeOf { addr := addr, port := port } = 1 + sizeOf addr + sizeOf port
-- Mathlib.Analysis.Normed.Lp.lpSpace
/-- If a sequence is Cauchy in the `lp E p` topology and pointwise convergent to an element `f` of
`lp E p`, then it converges to `f` in the `lp E p` topology.  -/
lp.tendsto_lp_of_tendsto_pi : ∀ {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [inst : (i : α) → NormedAddCommGroup (E i)] [_i : Fact (1 ≤ p)]
  {F : ℕ → ↥(lp E p)},
  CauchySeq F →
    ∀ {f : ↥(lp E p)},
      Filter.Tendsto (id fun i => ↑(F i)) Filter.atTop (nhds ↑f) → Filter.Tendsto F Filter.atTop (nhds f)
-- Batteries.Data.Fin.Lemmas
Fin.countP_eq_countP_map_finRange : ∀ {n : ℕ} (x : Fin n → Bool), Fin.countP x = List.countP x (List.finRange n)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem!_inter_of_not_mem_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α}
  [inst : Inhabited β], k ∉ t₁ → (t₁ ∩ t₂)[k]! = default
-- Mathlib.Analysis.SpecialFunctions.Pow.Complex
/-- The complex power function `x ^ y`, given by `x ^ y = exp(y log x)` (where `log` is the
principal determination of the logarithm), unless `x = 0` where one sets `0 ^ 0 = 1` and
`0 ^ y = 0` for `y ≠ 0`.  -/
Complex.cpow : ℂ → ℂ → ℂ
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.Formatter.withoutInfo.formatter : Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter
-- Mathlib.Algebra.Category.MonCat.Basic
/-- The type of morphisms in `AddCommMonCat`.  -/
AddCommMonCat.Hom : AddCommMonCat → AddCommMonCat → Type u
-- Mathlib.LinearAlgebra.TensorProduct.Associator
TensorProduct.tensorTensorTensorAssoc_symm_tmul : ∀ (R : Type u_1) [inst : CommSemiring R] {M : Type u_5} {N : Type u_6} {P : Type u_7} {Q : Type u_8}
  [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : AddCommMonoid Q]
  [inst_5 : Module R M] [inst_6 : Module R N] [inst_7 : Module R Q] [inst_8 : Module R P] (m : M) (n : N) (p : P)
  (q : Q),
  (TensorProduct.tensorTensorTensorAssoc R M N P Q).symm (m ⊗ₜ[R] (n ⊗ₜ[R] p) ⊗ₜ[R] q) = m ⊗ₜ[R] n ⊗ₜ[R] (p ⊗ₜ[R] q)
-- Mathlib.Data.Fin.Tuple.Reflection
_private.Mathlib.Data.Fin.Tuple.Reflection.0.FinVec.seq.match_1.eq_2 : ∀ {α : Type u_2} {β : Type u_3} (motive : (x : ℕ) → (Fin x → α → β) → (Fin x → α) → Sort u_1) (n : ℕ)
  (f : Fin (n + 1) → α → β) (v : Fin (n + 1) → α) (h_1 : (x : Fin 0 → α → β) → (x_1 : Fin 0 → α) → motive 0 x x_1)
  (h_2 : (n : ℕ) → (f : Fin (n + 1) → α → β) → (v : Fin (n + 1) → α) → motive n.succ f v),
  (match n.succ, f, v with
    | 0, x, x_1 => h_1 x x_1
    | n.succ, f, v => h_2 n f v) =
    h_2 n f v
-- Mathlib.Analysis.Calculus.ContDiff.Operations
/-- The product map of two `C^n` functions is `C^n`.  -/
ContDiff.prodMap : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : WithTop ℕ∞}
  {E' : Type u_3} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E'] {F' : Type u_4}
  [inst_7 : NormedAddCommGroup F'] [inst_8 : NormedSpace 𝕜 F'] {f : E → F} {g : E' → F'},
  ContDiff 𝕜 n f → ContDiff 𝕜 n g → ContDiff 𝕜 n (Prod.map f g)
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Const.RicSlice : (α : Type u_1) → Type u_2 → [Ord α] → Type (max u_2 u_1)
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.Compacts.mk : {α : Type u_4} → [inst : TopologicalSpace α] → (carrier : Set α) → IsCompact carrier → TopologicalSpace.Compacts α
-- Mathlib.FieldTheory.Finite.Basic
FiniteField.frobeniusAlgEquivOfAlgebraic.congr_simp : ∀ (K : Type u_1) [inst : Field K] [inst_1 : Fintype K] (L : Type u_3) [inst_2 : Field L] [inst_3 : Algebra K L]
  [inst_4 : Algebra.IsAlgebraic K L],
  FiniteField.frobeniusAlgEquivOfAlgebraic K L = FiniteField.frobeniusAlgEquivOfAlgebraic K L
-- Mathlib.CategoryTheory.Sites.ConcreteSheafification
/-- The canonical map from `P` to its sheafification.  -/
CategoryTheory.GrothendieckTopology.toSheafify : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      {D : Type w} →
        [inst_1 : CategoryTheory.Category.{w', w} D] →
          [inst_2 :
              ∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X),
                CategoryTheory.Limits.HasMultiequalizer (S.index P)] →
            [inst_3 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] →
              (P : CategoryTheory.Functor Cᵒᵖ D) → P ⟶ J.sheafify P
-- Mathlib.Topology.PartialHomeomorph.Basic
PartialHomeomorph.homeomorphOfImageSubsetSource_apply : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : PartialHomeomorph X Y)
  {s : Set X} {t : Set Y} (hs : s ⊆ e.source) (ht : ↑e '' s = t) (a : ↑s),
  (e.homeomorphOfImageSubsetSource hs ht) a = Set.MapsTo.restrict (↑e) s t ⋯ a
-- Mathlib.Algebra.Order.ToIntervalMod
/-- **Alias** of the reverse direction of `toIocDiv_eq_iff`. -/
toIocDiv_eq_of_sub_zsmul_mem_Ioc : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) {a b : α} {n : ℤ}, b - n • p ∈ Set.Ioc a (a + p) → toIocDiv hp a b = n
-- Mathlib.LinearAlgebra.Transvection.Basic
LinearEquiv.inv_mem_dilatransvections_iff : ∀ {R : Type u_1} {V : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup V] [inst_2 : Module R V] {e : V ≃ₗ[R] V},
  e⁻¹ ∈ LinearEquiv.dilatransvections R V ↔ e ∈ LinearEquiv.dilatransvections R V
-- ProofWidgets.Component.Panel.Basic
/-- Locations currently selected in the goal state.  -/
ProofWidgets.PanelWidgetProps.selectedLocations : ProofWidgets.PanelWidgetProps → Array Lean.SubExpr.GoalsLocation
-- Mathlib.NumberTheory.Padics.Measure.Basic
/-- "Right-handed" version of the natural product map on measures (acting on functions
as first integrating along `Y`, and then integrating the result along `X`).  -/
AbstractMeasure.prodMk' : {X : Type u_1} →
  {Y : Type u_2} →
    {R : Type u_3} →
      [inst : TopologicalSpace X] →
        [inst_1 : TopologicalSpace Y] →
          [inst_2 : CommRing R] →
            [inst_3 : TopologicalSpace R] →
              [inst_4 : IsTopologicalRing R] →
                [LocallyCompactSpace X] →
                  [LocallyCompactSpace Y] →
                    AbstractMeasure X R R →ₗ[R] AbstractMeasure Y R R →ₗ[R] AbstractMeasure (X × Y) R R
-- Mathlib.LinearAlgebra.Lagrange
Lagrange.basisDivisor_add_symm : ∀ {F : Type u_1} [inst : Field F] {x y : F}, x ≠ y → Lagrange.basisDivisor x y + Lagrange.basisDivisor y x = 1
-- Mathlib.Algebra.Module.Submodule.Defs
Submodule.neg_mem : ∀ {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] {module_M : Module R M} (p : Submodule R M)
  {x : M}, x ∈ p → -x ∈ p
-- Mathlib.Data.Sum.Order
OrderIso.sumCongr_symm : ∀ {α₁ : Type u_4} {α₂ : Type u_5} {β₁ : Type u_6} {β₂ : Type u_7} [inst : LE α₁] [inst_1 : LE α₂] [inst_2 : LE β₁]
  [inst_3 : LE β₂] (ea : α₁ ≃o α₂) (eb : β₁ ≃o β₂), (ea.sumCongr eb).symm = ea.symm.sumCongr eb.symm
-- Mathlib.RingTheory.MvPolynomial.FreeCommRing
/-- Collections of `MvPolynomial`s, `p : ι → MvPolynomial κ R` such
that `∀ i, (p i).support ⊆ monoms i` can be identified with functions
`(Σ i, monoms i) → R` by using the coefficient function  -/
FirstOrder.Ring.mvPolynomialSupportLEEquiv : {ι : Type u_1} →
  {κ : Type u_2} →
    {R : Type u_3} →
      [DecidableEq κ] →
        [inst : CommRing R] →
          [DecidableEq R] →
            (monoms : ι → Finset (κ →₀ ℕ)) → { p // ∀ (i : ι), (p i).support ⊆ monoms i } ≃ ((i : ι) × ↥(monoms i) → R)
-- Lean.Parser.Command
/-- `end` closes a `section` or `namespace` scope. If the scope is named `<id>`, it has to be closed
with `end <id>`. The `end` command is optional at the end of a file.
 -/
Lean.Parser.Command.end : Lean.Parser.Parser
-- Mathlib.CategoryTheory.Monoidal.Rigid.Basic
/-- The tensor product of exact pairings. Given exact pairings `(X₁, Y₁)` and `(X₂, Y₂)`,
we get an exact pairing `(X₁ ⊗ X₂, Y₂ ⊗ Y₁)`. Note the reversed order in the second factor.  -/
CategoryTheory.ExactPairing.tensor : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {X₁ X₂ Y₁ Y₂ : C} →
        [CategoryTheory.ExactPairing X₁ Y₁] →
          [CategoryTheory.ExactPairing X₂ Y₂] →
            CategoryTheory.ExactPairing (CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ X₂)
              (CategoryTheory.MonoidalCategoryStruct.tensorObj Y₂ Y₁)
-- Mathlib.Algebra.Module.Injective
/-- We can finally define a linear map `M ⊔ ⟨y⟩ ⟶ Q` by `x + r • y ↦ f x + φ r`
 -/
Module.Baer.ExtensionOfMaxAdjoin.extensionToFun : {R : Type u} →
  [inst : Ring R] →
    {Q : Type v} →
      [inst_1 : AddCommGroup Q] →
        [inst_2 : Module R Q] →
          {M : Type u_1} →
            {N : Type u_2} →
              [inst_3 : AddCommGroup M] →
                [inst_4 : AddCommGroup N] →
                  [inst_5 : Module R M] →
                    [inst_6 : Module R N] →
                      (i : M →ₗ[R] N) →
                        (f : M →ₗ[R] Q) →
                          [inst_7 : Fact (Function.Injective ⇑i)] →
                            Module.Baer R Q → {y : N} → ↥(Module.Baer.supExtensionOfMaxSingleton i f y) → Q
-- Mathlib.RingTheory.Ideal.MinimalPrime.Localization
Ideal.iUnion_minimalPrimes : ∀ {R : Type u_1} [inst : CommSemiring R] {I : Ideal R},
  ⋃ p ∈ I.minimalPrimes, ↑p = {x | ∃ y ∉ I.radical, x * y ∈ I.radical}
-- Mathlib.CategoryTheory.Sites.Equivalence
CategoryTheory.Equivalence.sheafCongr.inverse_obj_obj_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] (K : CategoryTheory.GrothendieckTopology D) (e : C ≌ D) (A : Type u₃)
  [inst_2 : CategoryTheory.Category.{v₃, u₃} A] [inst_3 : CategoryTheory.Functor.IsDenseSubsite K J e.inverse]
  (X : CategoryTheory.Sheaf K A) (X_1 : Cᵒᵖ),
  ((CategoryTheory.Equivalence.sheafCongr.inverse J K e A).obj X).obj.obj X_1 =
    X.obj.obj (Opposite.op (e.functor.obj (Opposite.unop X_1)))
-- ImportGraph.Imports.RequiredModules
/-- Return the names of the modules in which constants used transitively
in the specified declaration were defined.

Note that this will *not* account for tactics and syntax used in the declaration,
so the results may not suffice as imports.
 -/
Lean.Name.transitivelyRequiredModules : Lean.Name → Lean.Environment → Lean.CoreM Lean.NameSet
-- Init.Data.UInt.Lemmas
UInt64.toUSize_mod : ∀ (a b : UInt64), a < 4294967296 → b < 4294967296 → (a % b).toUSize = a.toUSize % b.toUSize
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.get!_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α],
  m.WF →
    ∀ {l : List ((a : α) × β a)} {k : α} [inst_3 : Inhabited (β k)],
      (List.map Sigma.fst l).contains k = false → (m.insertMany l).get! k = m.get! k
-- Lean.Parser.Extension
Lean.Parser.parserAliasesRef : IO.Ref (Lean.NameMap Lean.Parser.ParserAliasValue)
-- Lean.Expr
Lean.Int.mkInstDiv : Lean.Expr
-- Init.Prelude
/-- Reader monads provide the ability to implicitly thread a value through a computation. The value can
be read, but not written. A `MonadWithReader ρ` instance additionally allows the value to be locally
overridden for a sub-computation.

In this class, `ρ` is a `semiOutParam`, which means that it can influence the choice of instance.
`MonadReader ρ` provides the same operations, but requires that `ρ` be inferable from `m`.
 -/
MonadReaderOf : semiOutParam (Type u) → (Type u → Type v) → Type v
-- Lean.Data.Lsp.Extra
Lean.Lsp.RpcKeepAliveParams.mk.inj : ∀ {uri : Lean.Lsp.DocumentUri} {sessionId : UInt64} {uri_1 : Lean.Lsp.DocumentUri} {sessionId_1 : UInt64},
  { uri := uri, sessionId := sessionId } = { uri := uri_1, sessionId := sessionId_1 } →
    uri = uri_1 ∧ sessionId = sessionId_1
-- Mathlib.RingTheory.Jacobson.Ring
isJacobsonRing_of_finiteType : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] [IsJacobsonRing A]
  [Algebra.FiniteType A B], IsJacobsonRing B
-- Mathlib.Combinatorics.Additive.FreimanHom
/-- If `f` is an additive Freiman isomorphism from `A` to `B`, then `f.invFunOn A` is
an additive Freiman isomorphism from `B` to `A`.  -/
IsAddFreimanIso.invFunOn : ∀ {α : Type u_2} {β : Type u_3} [inst : AddCommMonoid α] [inst_1 : AddCommMonoid β] {A : Set α} {B : Set β} {f : α → β}
  {n : ℕ}, IsAddFreimanIso n A B f → IsAddFreimanIso n B A (Function.invFunOn f A)
-- Mathlib.Algebra.Group.Subgroup.Map
/-- An isomorphism of groups gives an order isomorphism between the lattices of subgroups,
defined by sending subgroups to their inverse images.

See also `AddEquiv.mapAddSubgroup` which maps subgroups to their forward images.  -/
AddEquiv.comapAddSubgroup : {G : Type u_1} → [inst : AddGroup G] → {H : Type u_5} → [inst_1 : AddGroup H] → G ≃+ H → AddSubgroup H ≃o AddSubgroup G
-- Mathlib.Topology.Order
generateFrom_insert_empty : ∀ {α : Type u_1} {s : Set (Set α)}, TopologicalSpace.generateFrom (insert ∅ s) = TopologicalSpace.generateFrom s
-- Mathlib.GroupTheory.GroupAction.Basic
AddAction.orbit_eq_univ : ∀ (M : Type u) [inst : AddMonoid M] {α : Type v} [inst_1 : AddAction M α] [AddAction.IsPretransitive M α] (a : α),
  AddAction.orbit M a = Set.univ
-- Mathlib.Combinatorics.SetFamily.Shatter
Finset.isLowerSet_shatterer : ∀ {α : Type u_1} [inst : DecidableEq α] (𝒜 : Finset (Finset α)), IsLowerSet ↑𝒜.shatterer
-- Init.Data.List.Basic
List.Sublist.below.slnil : ∀ {α : Type u_1} {motive : (a a_1 : List α) → a.Sublist a_1 → Prop}, List.Sublist.below ⋯
-- Mathlib.CategoryTheory.Bicategory.Modification.Pseudo
/-- The underlying family of 2-morphism.  -/
CategoryTheory.Pseudofunctor.StrongTrans.Modification.app : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.Pseudofunctor B C} →
          {η θ : F ⟶ G} → CategoryTheory.Pseudofunctor.StrongTrans.Modification η θ → (a : B) → η.app a ⟶ θ.app a
-- Mathlib.Analysis.SpecialFunctions.Log.Summable
Complex.multipliable_one_add_of_summable : ∀ {ι : Type u_1} {f : ι → ℂ}, Summable f → Multipliable fun i => 1 + f i
-- Init.Data.UInt.Lemmas
UInt8.toFin_div : ∀ (a b : UInt8), (a / b).toFin = a.toFin / b.toFin
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
not_linearIndependent_iff_linearCombination : ∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {v : ι → M}, ¬LinearIndependent R v ↔ ∃ l, (Finsupp.linearCombination R v) l = 0 ∧ l ≠ 0
-- Init.Data.Order.PackageFactories
Std.Packages.LinearPreorderOfOrdArgs.ord : {α : Type u} → Std.Packages.LinearPreorderOfOrdArgs α → Ord α
-- Mathlib.RingTheory.Nilpotent.Exp
IsNilpotent.exp_add_of_commute : ∀ {A : Type u_1} [inst : Ring A] [inst_1 : Module ℚ A] {a b : A},
  Commute a b → IsNilpotent a → IsNilpotent b → IsNilpotent.exp (a + b) = IsNilpotent.exp a * IsNilpotent.exp b
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.coeff_single_mul_eq_mul_coeff : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] {x : MonoidAlgebra R M} {r : R} {m m₁ : M} [inst_1 : Mul M]
  (m₂ : M), (∀ m' ∈ x.coeff.support, m * m' = m₁ ↔ m' = m₂) → (MonoidAlgebra.single m r * x).coeff m₁ = r * x.coeff m₂
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.continuousLinearEquiv_symm_apply : ∀ (p : ENNReal) (𝕜 : Type u_1) {ι : Type u_2} (β : ι → Type u_4) [inst : Semiring 𝕜]
  [inst_1 : (i : ι) → AddCommGroup (β i)] [inst_2 : (i : ι) → Module 𝕜 (β i)]
  [inst_3 : (i : ι) → TopologicalSpace (β i)] (a : (i : ι) → β i),
  (PiLp.continuousLinearEquiv p 𝕜 β).symm a = WithLp.toLp p a