mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.QPF.Univariate.Basic
/-- Given a qpf `F` and a well-behaved surjection `FG_abs` from `F α` to
functor `G α`, `G` is a qpf. We can consider `G` a quotient on `F` where
elements `x y : F α` are in the same equivalence class if
`FG_abs x = FG_abs y`.  -/
QPF.quotientQPF : {F : Type u → Type u} →
  [q : QPF F] →
    {G : Type u → Type u} →
      [inst : Functor G] →
        {FG_abs : {α : Type u} → F α → G α} →
          {FG_repr : {α : Type u} → G α → F α} →
            (∀ {α : Type u} (x : G α), FG_abs (FG_repr x) = x) →
              (∀ {α β : Type u} (f : α → β) (x : F α), FG_abs (f <$> x) = f <$> FG_abs x) → QPF G
-- Mathlib.Algebra.Group.Equiv.Basic
MulEquiv.piCongrRight_trans : ∀ {η : Type u_16} {Ms : η → Type u_17} {Ns : η → Type u_18} {Ps : η → Type u_19} [inst : (j : η) → Mul (Ms j)]
  [inst_1 : (j : η) → Mul (Ns j)] [inst_2 : (j : η) → Mul (Ps j)] (es : (j : η) → Ms j ≃* Ns j)
  (fs : (j : η) → Ns j ≃* Ps j),
  (MulEquiv.piCongrRight es).trans (MulEquiv.piCongrRight fs) = MulEquiv.piCongrRight fun i => (es i).trans (fs i)
-- Mathlib.ModelTheory.Encoding
FirstOrder.Language.Term.listEncode.eq_2 : ∀ {L : FirstOrder.Language} {α : Type u'} (l : ℕ) (f : L.Functions l) (ts : Fin l → L.Term α),
  (FirstOrder.Language.func f ts).listEncode =
    Sum.inr ⟨l, f⟩ :: List.flatMap (fun i => (ts i).listEncode) (List.finRange l)
-- Std.Data.DTreeMap.Internal.Operations
Std.DTreeMap.Internal.Impl.BalancedTree.mk.injEq : ∀ {α : Type u} {β : α → Type v} (impl : Std.DTreeMap.Internal.Impl α β) (balanced_impl : impl.Balanced)
  (impl_1 : Std.DTreeMap.Internal.Impl α β) (balanced_impl_1 : impl_1.Balanced),
  ({ impl := impl, balanced_impl := balanced_impl } = { impl := impl_1, balanced_impl := balanced_impl_1 }) =
    (impl = impl_1)
-- Mathlib.Algebra.Category.MonCat.Colimits
MonCat.Colimits.Prequotient.mul.sizeOf_spec : ∀ {J : Type v} [inst : CategoryTheory.Category.{u, v} J] {F : CategoryTheory.Functor J MonCat} [inst_1 : SizeOf J]
  (a a_1 : MonCat.Colimits.Prequotient F), sizeOf (a.mul a_1) = 1 + sizeOf a + sizeOf a_1
-- Mathlib.Order.BourbakiWitt
CompleteLattice.ωScottContinuous.bot : ∀ {α : Type u_1} {β : Type u_2} [inst : OmegaCompletePartialOrder α] [inst_1 : CompleteLattice β],
  OmegaCompletePartialOrder.ωScottContinuous ⊥
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.inhabitedConeMorphism.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} (A : CategoryTheory.Limits.Cone F),
  CategoryTheory.Limits.inhabitedConeMorphism A =
    { default := { hom := CategoryTheory.CategoryStruct.id A.pt, w := ⋯ } }
-- Mathlib.RingTheory.Invariant.Basic
MulSemiringAction.monic_charpoly : ∀ {B : Type u_2} (G : Type u_3) [inst : CommRing B] [inst_1 : Group G] [inst_2 : MulSemiringAction G B]
  [inst_3 : Fintype G] (b : B), (MulSemiringAction.charpoly G b).Monic
-- Mathlib.CategoryTheory.Limits.Cones
/-- Change a `Cocone F` into a `Cone F.op`.  -/
CategoryTheory.Limits.Cocone.op : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} → CategoryTheory.Limits.Cocone F → CategoryTheory.Limits.Cone F.op
-- Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
/-- For a ring seminorm `f` on `R` and `c ∈ R`, the sequence given by `(f (x * c^n))/((f c)^n)`.  -/
seminormFromConst_seq : {R : Type u_1} → [inst : CommRing R] → R → RingSeminorm R → R → ℕ → ℝ
-- Mathlib.Topology.Order.Monotone
/-- In a second countable space, the set of points where a monotone function is not continuous
within a set is at most countable.  -/
MonotoneOn.countable_not_continuousWithinAt : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α]
  [inst_3 : LinearOrder β] {s : Set α} {f : α → β} [inst_4 : TopologicalSpace β] [OrderTopology β]
  [SecondCountableTopology β], MonotoneOn f s → {x | x ∈ s ∧ ¬ContinuousWithinAt f s x}.Countable
-- Mathlib.Topology.Algebra.Module.TransferInstance
/-- Given a continuous additive equivalence `e : α ≃ₜ+ β`, if `β` is a topological additive group,
then so is `α`.  -/
ContinuousAddEquiv.isTopologicalAddGroup : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace β] [inst_1 : AddGroup β] [IsTopologicalAddGroup β]
  [inst_3 : TopologicalSpace α] [inst_4 : AddGroup α] (e : α ≃ₜ+ β), IsTopologicalAddGroup α
-- Mathlib.Algebra.Group.End
AddAut.symm_neg : ∀ (M : Type u_2) [inst : Add M] (e : AddAut M), -AddEquiv.symm e = e
-- Mathlib.RingTheory.WittVector.WittPolynomial
wittPolynomial_eq_sum_C_mul_X_pow : ∀ (p : ℕ) (R : Type u_1) [inst : CommRing R] (n : ℕ),
  wittPolynomial p R n = ∑ i ∈ Finset.range (n + 1), MvPolynomial.C (↑p ^ i) * MvPolynomial.X i ^ p ^ (n - i)
-- Mathlib.NumberTheory.Height.Basic
Height.logHeight₁_eq_logHeight : ∀ {K : Type u_1} [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K] (x : K),
  Height.logHeight₁ x = Height.logHeight ![x, 1]
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Finset.sum_lt_sum : ∀ {ι : Type u_1} {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : Preorder M] [IsOrderedCancelAddMonoid M]
  {f g : ι → M} {s : Finset ι} [AddLeftStrictMono M],
  (∀ i ∈ s, f i ≤ g i) → (∃ i ∈ s, f i < g i) → ∑ i ∈ s, f i < ∑ i ∈ s, g i
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
/-- `MultipliableLocallyUniformlyOn f s` means that the product `∏' i, f i b` converges locally
uniformly on `s` to something.  -/
MultipliableLocallyUniformlyOn : {α : Type u_1} →
  {β : Type u_2} →
    {ι : Type u_3} → [CommMonoid α] → (ι → β → α) → Set β → [UniformSpace α] → [TopologicalSpace β] → Prop
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
/-- The q-Expansion of normalised Eisenstein series of level one with `riemannZeta` term.  -/
EisensteinSeries.q_expansion_riemannZeta : ∀ {k : ℕ} (hk : 3 ≤ k),
  Even k →
    ∀ (z : UpperHalfPlane),
      (ModularForm.E hk) z =
        1 +
          (riemannZeta ↑k)⁻¹ * (-2 * ↑Real.pi * Complex.I) ^ k / ↑(k - 1).factorial *
            ∑' (n : ℕ+), ↑((ArithmeticFunction.sigma (k - 1)) ↑n) * Complex.exp (2 * ↑Real.pi * Complex.I * ↑z) ^ ↑↑n
-- Mathlib.Data.Ordmap.Ordnode
/-- **Internal use only**

The maximal relative difference between the sizes of
two trees, it corresponds with the `w` in Adams' paper.

According to the Haskell comment, only `(delta, ratio)` settings
of `(3, 2)` and `(4, 2)` will work, and the proofs in
`Ordset.lean` assume `delta := 3` and `ratio := 2`.  -/
Ordnode.delta : ℕ
-- Lean.Declaration
Lean.instInhabitedDefinitionSafety : Inhabited Lean.DefinitionSafety
-- Init.Data.Int.Bitwise.Lemmas
Int.shiftRight.eq_1 : ∀ (x n : ℕ), (Int.ofNat n).shiftRight x = Int.ofNat (n >>> x)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.maxKeyD_alter_eq_self : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α] (h : t.WF)
  {k : α} {f : Option β → Option β},
  (Std.DTreeMap.Internal.Impl.Const.alter k f t ⋯).impl.isEmpty = false →
    ∀ {fallback : α},
      (Std.DTreeMap.Internal.Impl.Const.alter k f t ⋯).impl.maxKeyD fallback = k ↔
        (f (Std.DTreeMap.Internal.Impl.Const.get? t k)).isSome = true ∧ ∀ k' ∈ t, (compare k' k).isLE = true
-- Lean.Message
Lean.TraceResult.noConfusionType : Sort v✝ → Lean.TraceResult → Lean.TraceResult → Sort v✝
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Equiv.getKeyGT!_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α] {k : α}, t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.getKeyGT! k = t₂.getKeyGT! k
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.OneLine.instMonadPrettyFormatM : Std.Format.MonadPrettyFormat Lean.PrettyPrinter.OneLine.M
-- Mathlib.Tactic.CategoryTheory.Slice
/-- `evalSlice`
- rewrites the target expression using `Category.assoc`.
- uses `congr` to split off the first `a-1` terms and rotates to `a`-th (last) term
- counts the number `k` of rewrites as it uses `← Category.assoc` to bring the target to
  left associated form; from the first step this is the total number of remaining terms from `C`
- it now splits off `b-a` terms from target using `congr` leaving the desired subterm
- finally, it rewrites it once more using `Category.assoc` to bring it to right-associated
  normal form
 -/
Mathlib.Tactic.Slice.evalSlice : ℕ → ℕ → Lean.Elab.Tactic.TacticM Unit
-- Mathlib.Algebra.Homology.Embedding.StupidTrunc
HomologicalComplex.instIsStrictlySupportedStupidTrunc : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C c') (e : c.Embedding c')
  [inst_3 : e.IsRelIff], (K.stupidTrunc e).IsStrictlySupported e
-- Mathlib.Order.Filter.Pointwise
/-- `Filter α` is a commutative division monoid under pointwise operations if `α` is.  -/
Filter.divisionCommMonoid : {α : Type u_2} → [DivisionCommMonoid α] → DivisionCommMonoid (Filter α)
-- Mathlib.Analysis.SpecialFunctions.Integrability.Basic
intervalIntegral.intervalIntegrable_exp : ∀ {a b : ℝ} {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsLocallyFiniteMeasure μ], IntervalIntegrable Real.exp μ a b
-- Mathlib.CategoryTheory.Sums.Associator
CategoryTheory.sum.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.sum.associativity C D E).inverse = CategoryTheory.sum.inverseAssociator C D E
-- Std.Time.Date.PlainDate
/-- Adds a given number of months to a `PlainDate`, clipping the day to the last valid day of the month.
 -/
Std.Time.PlainDate.addMonthsClip : Std.Time.PlainDate → Std.Time.Month.Offset → Std.Time.PlainDate
-- Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
/-- The terms in the sequence `seminormFromConst_seq c f x` are nonnegative.  -/
seminormFromConst_seq_nonneg : ∀ {R : Type u_1} [inst : CommRing R] (c : R) (f : RingSeminorm R) (x : R), 0 ≤ seminormFromConst_seq c f x
-- Mathlib.Analysis.Normed.Module.Basic
Filter.IsBoundedUnder.smul_tendsto_zero : ∀ {𝕜 : Type u_1} {E : Type u_3} {α : Type u_5} [inst : NormedField 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : α → 𝕜} {g : α → E} {l : Filter α},
  Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l (norm ∘ f) →
    Filter.Tendsto g l (nhds 0) → Filter.Tendsto (fun x => f x • g x) l (nhds 0)
-- Mathlib.RingTheory.OreLocalization.Basic
OreLocalization.instAddMonoid : {R : Type u_1} →
  [inst : Monoid R] →
    {S : Submonoid R} →
      [inst_1 : OreLocalization.OreSet S] →
        {X : Type u_2} → [inst_2 : AddMonoid X] → [inst_3 : DistribMulAction R X] → AddMonoid (OreLocalization S X)
-- Lean.Language.Lean.Types
Lean.Language.Lean.CommandResultSnapshot.mk.injEq : ∀ (toSnapshot : Lean.Language.Snapshot) (cmdState : Lean.Elab.Command.State) (toSnapshot_1 : Lean.Language.Snapshot)
  (cmdState_1 : Lean.Elab.Command.State),
  ({ toSnapshot := toSnapshot, cmdState := cmdState } = { toSnapshot := toSnapshot_1, cmdState := cmdState_1 }) =
    (toSnapshot = toSnapshot_1 ∧ cmdState = cmdState_1)
-- Mathlib.CategoryTheory.Sites.Hypercover.One
/-- The shape of the multiforks attached to `E : PreOneHypercover S`.  -/
CategoryTheory.PreOneHypercover.multicospanShape : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {S : C} → CategoryTheory.PreOneHypercover S → CategoryTheory.Limits.MulticospanShape
-- Mathlib.CategoryTheory.Localization.Equivalence
/-- Basic constructor of an equivalence between localized categories  -/
CategoryTheory.Localization.equivalence : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {D₁ : Type u_4} →
      {D₂ : Type u_5} →
        [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
          [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
            [inst_2 : CategoryTheory.Category.{v_4, u_4} D₁] →
              [inst_3 : CategoryTheory.Category.{v_5, u_5} D₂] →
                (L₁ : CategoryTheory.Functor C₁ D₁) →
                  (W₁ : CategoryTheory.MorphismProperty C₁) →
                    [L₁.IsLocalization W₁] →
                      (L₂ : CategoryTheory.Functor C₂ D₂) →
                        (W₂ : CategoryTheory.MorphismProperty C₂) →
                          [L₂.IsLocalization W₂] →
                            (G : CategoryTheory.Functor C₁ D₂) →
                              (G' : CategoryTheory.Functor D₁ D₂) →
                                [CategoryTheory.Localization.Lifting L₁ W₁ G G'] →
                                  (F : CategoryTheory.Functor C₂ D₁) →
                                    (F' : CategoryTheory.Functor D₂ D₁) →
                                      [CategoryTheory.Localization.Lifting L₂ W₂ F F'] →
                                        (G.comp F' ≅ L₁) → (F.comp G' ≅ L₂) → (D₁ ≌ D₂)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get_insertMany_list_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l : List (α × β)} {k k' : α},
  (k == k') = true →
    ∀ {v : β},
      List.Pairwise (fun a b => (a.1 == b.1) = false) l →
        (k, v) ∈ l →
          ∀ {h : k' ∈ Std.ExtDHashMap.Const.insertMany m l},
            Std.ExtDHashMap.Const.get (Std.ExtDHashMap.Const.insertMany m l) k' h = v
-- Init.Data.Option.Basic
/-- Lifts an ordering relation to `Option`, such that `none` is the least element.

It can be understood as adding a distinguished least element, represented by `none`, to both `α` and
`β`.

This definition is part of the implementation of the `LT (Option α)` instance. However, because it
can be used with heterogeneous relations, it is sometimes useful on its own.

Examples:
 * `Option.lt (fun n k : Nat => n < k) none none = False`
 * `Option.lt (fun n k : Nat => n < k) none (some 3) = True`
 * `Option.lt (fun n k : Nat => n < k) (some 3) none = False`
 * `Option.lt (fun n k : Nat => n < k) (some 4) (some 5) = True`
 * `Option.lt (fun n k : Nat => n < k) (some 4) (some 4) = False`
 -/
Option.lt : {α : Type u_1} → {β : Type u_2} → (α → β → Prop) → Option α → Option β → Prop
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.piEquivalenceFunctorDiscreteCompColim_comp_functorι_assoc : ∀ {α : Type w₂} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasCoproductsOfShape α C] (a : α) {Z : CategoryTheory.Functor (α → C) C}
  (h : CategoryTheory.Limits.Sigma.functor α ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.piEquivalenceFunctorDiscrete α C).functor.whiskerLeft
        (CategoryTheory.Limits.colim.ι { as := a }))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.piEquivalenceFunctorDiscreteCompColim α).hom h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.piEquivalenceFunctorDiscreteCompEvaluationIso C a).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.functorι a) h)
-- Mathlib.Analysis.Complex.Trigonometric
Complex.cos_bound : ∀ {x : ℂ}, ‖x‖ ≤ 1 → ‖Complex.cos x - (1 - x ^ 2 / 2)‖ ≤ ‖x‖ ^ 4 * (5 / 96)
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.prodMkRight_apply : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) (ca : α × γ),
  (ProbabilityTheory.Kernel.prodMkRight γ κ) ca = κ ca.1
-- Mathlib.Topology.Algebra.ProperAction.CompactlyGenerated
properlyDiscontinuousVAdd_iff_properVAdd : ∀ {G : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] [inst_1 : AddGroup G] [inst_2 : TopologicalSpace G]
  [inst_3 : AddAction G X] [CompactlyGeneratedSpace (X × X)] [T2Space X] [DiscreteTopology G] [ContinuousConstVAdd G X],
  ProperlyDiscontinuousVAdd G X ↔ ProperVAdd G X
-- Mathlib.Algebra.Lie.Nilpotent
LieModule.isNilpotent_iff_exists_ucs_eq_top : ∀ (R : Type u) {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M],
  LieModule.IsNilpotent L M ↔ ∃ k, LieSubmodule.ucs k ⊥ = ⊤
-- Mathlib.Topology.Category.TopCat.ULift
TopCat.instFullUliftFunctor : TopCat.uliftFunctor.Full
-- Mathlib.FieldTheory.RatFunc.IntermediateField
/-- The equivalence between `E⟮X⟯` and `K⟮X⟯` as `E`-algebras.  -/
RatFunc.IntermediateField.adjoinXEquiv : {K : Type u_1} → [inst : Field K] → (E : IntermediateField K (RatFunc K)) → ↥(↥E)⟮RatFunc.X⟯ ≃ₐ[↥E] RatFunc K
-- Mathlib.Data.List.Intervals
List.Ico.pairwise_lt : ∀ (n m : ℕ), List.Pairwise (fun x1 x2 => x1 < x2) (List.Ico n m)
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.liftRingHom_apply_div' : ∀ {K : Type u} [inst : CommRing K] [inst_1 : IsDomain K] {L : Type u_1} [inst_2 : Field L] (φ : Polynomial K →+* L)
  (hφ : nonZeroDivisors (Polynomial K) ≤ Submonoid.comap φ (nonZeroDivisors L)) (p q : Polynomial K),
  (RatFunc.liftRingHom φ hφ) ((algebraMap (Polynomial K) (RatFunc K)) p) /
      (RatFunc.liftRingHom φ hφ) ((algebraMap (Polynomial K) (RatFunc K)) q) =
    φ p / φ q
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.NonemptyCompacts.isOpen_inter_nonempty_of_isOpen : ∀ {α : Type u_1} [inst : TopologicalSpace α] {U : Set α}, IsOpen U → IsOpen {K | (↑K ∩ U).Nonempty}
-- Init.Grind.Config
Lean.Grind.LinarithConfig.mk.injEq : ∀ (toNoopConfig toNoopConfig_1 : Lean.Grind.NoopConfig),
  ({ toNoopConfig := toNoopConfig } = { toNoopConfig := toNoopConfig_1 }) = (toNoopConfig = toNoopConfig_1)
-- Mathlib.Algebra.Category.AlgCat.Basic
/-- The underlying type.  -/
AlgCat.carrier : {R : Type u} → [inst : CommRing R] → AlgCat R → Type v
-- Mathlib.RingTheory.AdicCompletion.Functoriality
AdicCompletion.map_surjective_of_mkQ_comp_surjective : ∀ {R : Type u_1} [inst : CommRing R] {I : Ideal R} {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {N : Type u_3} [inst_3 : AddCommGroup N] [inst_4 : Module R N] {f : M →ₗ[R] N},
  Function.Surjective ⇑((I • ⊤).mkQ ∘ₗ f) → Function.Surjective ⇑(AdicCompletion.map I f)
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.toCycles_cyclesIsoSc'_hom_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i j k : ι) (hi : c.prev j = i) (hk : c.next j = k)
  [inst_2 : K.HasHomology j] [inst_3 : (K.sc' i j k).HasHomology] {Z : C} (h : (K.sc' i j k).cycles ⟶ Z),
  CategoryTheory.CategoryStruct.comp (K.toCycles i j)
      (CategoryTheory.CategoryStruct.comp (K.cyclesIsoSc' i j k hi hk).hom h) =
    CategoryTheory.CategoryStruct.comp (K.sc' i j k).toCycles h
-- Mathlib.Probability.Kernel.Defs
ProbabilityTheory.isFiniteKernel_zero : ∀ (α : Type u_4) (β : Type u_5) {x : MeasurableSpace α} {x_1 : MeasurableSpace β}, ProbabilityTheory.IsFiniteKernel 0
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.contains_diff_iff : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  (h₁ : m₁.WF),
  m₂.WF →
    ∀ {k : α},
      Std.DTreeMap.Internal.Impl.contains k (m₁.diff m₂ ⋯) = true ↔
        Std.DTreeMap.Internal.Impl.contains k m₁ = true ∧ ¬Std.DTreeMap.Internal.Impl.contains k m₂ = true
-- Init.Data.String.Lemmas.Splits
String.Pos.Splits.toByteArray_right_eq : ∀ {s : String} {p : s.Pos} {t₁ t₂ : String},
  p.Splits t₁ t₂ → t₂.toByteArray = s.toByteArray.extract p.offset.byteIdx s.utf8ByteSize
-- Mathlib.Order.SuccPred.LinearLocallyFinite
toZ_iterate_succ_of_not_isMax : ∀ {ι : Type u_1} [inst : LinearOrder ι] [inst_1 : SuccOrder ι] [inst_2 : IsSuccArchimedean ι] [inst_3 : PredOrder ι]
  {i0 : ι} (n : ℕ), ¬IsMax (Order.succ^[n] i0) → toZ i0 (Order.succ^[n] i0) = ↑n
-- Mathlib.Algebra.EuclideanDomain.Defs
EuclideanDomain.gcd.eq_1 : ∀ {R : Type u} [inst : EuclideanDomain R] [inst_1 : DecidableEq R] (a b : R),
  EuclideanDomain.gcd a b =
    if a0 : a = 0 then b
    else
      have x := ⋯;
      EuclideanDomain.gcd (b % a) a
-- Mathlib.Data.Nat.Factorization.LCM
Nat.coprime_factorizationLCMLeft_factorizationLCMRight : ∀ (a b : ℕ), (a.factorizationLCMLeft b).Coprime (a.factorizationLCMRight b)
-- Mathlib.Data.Set.Operations
/-- `g` is a right inverse to `f` on `t` if `f (g x) = x` for all `x ∈ t`.  -/
Set.RightInvOn : {α : Type u} → {β : Type v} → (β → α) → (α → β) → Set β → Prop
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.PolyCnstr.eq : Nat.Internal.Linear.PolyCnstr → Bool
-- Mathlib.Order.RelIso.Basic
RelHomClass.acc : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} {F : Type u_5} [inst : FunLike F α β]
  [RelHomClass F r s] (f : F) (a : α), Acc s (f a) → Acc r a
-- Mathlib.Order.InitialSeg
/-- An `InitialSeg` between the `<` relations of two types.  -/
«term_≤i_» : Lean.TrailingParserDescr
-- Mathlib.Data.ENNReal.Basic
ENNReal.toReal_ofReal : ∀ {r : ℝ}, 0 ≤ r → (ENNReal.ofReal r).toReal = r
-- Mathlib.Algebra.Star.Module
/-- The self-adjoint part of an element of a star module, as a linear map.  -/
selfAdjointPart : (R : Type u_1) →
  {A : Type u_2} →
    [inst : Semiring R] →
      [inst_1 : StarMul R] →
        [inst_2 : TrivialStar R] →
          [inst_3 : AddCommGroup A] →
            [inst_4 : Module R A] →
              [inst_5 : StarAddMonoid A] → [inst_6 : StarModule R A] → [Invertible 2] → A →ₗ[R] ↥(selfAdjoint A)
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.prod_insert : ∀ {ι : Type u_1} {M : Type u_4} {s : Finset ι} {a : ι} [inst : CommMonoid M] {f : ι → M} [inst_1 : DecidableEq ι],
  a ∉ s → ∏ x ∈ insert a s, f x = f a * ∏ x ∈ s, f x
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.EMatchTheoremKind.bwd.sizeOf_spec : ∀ (gen : Bool), sizeOf (Lean.Meta.Grind.EMatchTheoremKind.bwd gen) = 1 + sizeOf gen
-- Mathlib.Analysis.Calculus.Deriv.Comp
HasDerivAt.comp_hasDerivWithinAt : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] (x : 𝕜) {s : Set 𝕜} {𝕜' : Type u_1}
  [inst_1 : NontriviallyNormedField 𝕜'] [inst_2 : NormedAlgebra 𝕜 𝕜'] {h : 𝕜 → 𝕜'} {h₂ : 𝕜' → 𝕜'} {h' h₂' : 𝕜'},
  HasDerivAt h₂ h₂' (h x) → HasDerivWithinAt h h' s x → HasDerivWithinAt (h₂ ∘ h) (h₂' * h') s x
-- Mathlib.Geometry.Euclidean.Sphere.Tangent
/-- The set of all maximal common internal tangent spaces to the spheres `s₁` and `s₂`: tangent
spaces containing a point weakly between the centers of the spheres.  -/
EuclideanGeometry.Sphere.commonIntTangents : {V : Type u_1} →
  {P : Type u_2} →
    [inst : NormedAddCommGroup V] →
      [inst_1 : InnerProductSpace ℝ V] →
        [inst_2 : MetricSpace P] →
          [inst_3 : NormedAddTorsor V P] →
            EuclideanGeometry.Sphere P → EuclideanGeometry.Sphere P → Set (AffineSubspace ℝ P)
-- Mathlib.Order.Interval.Finset.Defs
Finset.Ici_product_Ici : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : LocallyFiniteOrderTop α]
  [inst_3 : LocallyFiniteOrderTop β] [inst_4 : DecidableLE (α × β)] (a : α) (b : β),
  Finset.Ici a ×ˢ Finset.Ici b = Finset.Ici (a, b)
-- Mathlib.Algebra.LinearRecurrence
/-- A "linear recurrence relation" over a commutative semiring is given by its
order `n` and `n` coefficients.  -/
LinearRecurrence : (R : Type u_1) → [CommSemiring R] → Type u_1
-- Mathlib.Analysis.AbsoluteValue.Equivalence
/-- **Alias** of the forward direction of `AbsoluteValue.IsEquiv.isNontrivial_congr`. -/
AbsoluteValue.IsEquiv.isNontrivial : ∀ {R : Type u_1} [inst : Semiring R] {S : Type u_2} [inst_1 : Semiring S] [inst_2 : PartialOrder S]
  {v : AbsoluteValue R S} [IsDomain S] [Nontrivial R] {w : AbsoluteValue R S},
  v.IsEquiv w → v.IsNontrivial → w.IsNontrivial
-- Mathlib.Logic.Function.Conjugate
Function.Commute.symm : ∀ {α : Type u_1} {f g : α → α}, Function.Commute f g → Function.Commute g f
-- Mathlib.Topology.Homeomorph.Defs
/-- Bundled homeomorphism constructed from a map that is a homeomorphism.  -/
IsHomeomorph.homeomorph : {X : Type u_1} →
  {Y : Type u_2} → [inst : TopologicalSpace X] → [inst_1 : TopologicalSpace Y] → (f : X → Y) → IsHomeomorph f → X ≃ₜ Y