mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Complex.Circle
/-- The additive character from `ℝ` onto the circle, given by `fun x ↦ exp (2 * π * x * I)`.
Denoted as `𝐞` within the `Real.FourierTransform` namespace. This uses the analyst convention that
there is a `2 * π` in the exponent.  -/
FourierTransform.«term𝐞» : Lean.ParserDescr
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.inl_intCast : ∀ {R : Type u} {M : Type v} [inst : AddGroupWithOne R] [inst_1 : AddGroup M] (z : ℤ), TrivSqZeroExt.inl ↑z = ↑z
-- Mathlib.Analysis.Normed.MulAction
enorm_smul_le : ∀ {α : Type u_1} {β : Type u_2} [inst : SeminormedAddGroup α] [inst_1 : SeminormedAddGroup β]
  [inst_2 : SMulZeroClass α β] [IsBoundedSMul α β] {r : α} {x : β}, ‖r • x‖ₑ ≤ ‖r‖ₑ * ‖x‖ₑ
-- Mathlib.LinearAlgebra.Reflection
Module.reflection_apply : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {x : M}
  {f : Module.Dual R M} (y : M) (h : f x = 2), (Module.reflection h) y = y - f y • x
-- Mathlib.GroupTheory.OrderOfElement
/-- The submonoid generated by an element is a group if that element has finite order.  -/
IsOfFinOrder.groupPowers : {G : Type u_1} → [inst : Monoid G] → {x : G} → IsOfFinOrder x → Group ↥(Submonoid.powers x)
-- Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
/-- `f` is a right inverse of `algebraMap R S` when restricted to `quasispectrum S a`.  -/
QuasispectrumRestricts.rightInvOn : ∀ {R : Type u_3} {S : Type u_4} {A : Type u_5} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : NonUnitalRing A] [inst_3 : Module R A] [inst_4 : Module S A] [inst_5 : Algebra R S] {a : A} {f : S → R},
  QuasispectrumRestricts a f → Set.RightInvOn f (⇑(algebraMap R S)) (quasispectrum S a)
-- Mathlib.RingTheory.TotallySplit
Algebra.IsFiniteSplit.nonempty_algEquiv_fun : ∀ (R : Type u_1) (S : Type u_2) {inst : CommRing R} {inst_1 : CommRing S} {inst_2 : Algebra R S}
  [self : Algebra.IsFiniteSplit R S], ∃ n, Nonempty (S ≃ₐ[R] Fin n → R)
-- Mathlib.Topology.Order.LeftRightLim
rightLim_leftLim : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace β] [inst_2 : TopologicalSpace α]
  [OrderTopology α] [T3Space β] {f : α → β} {a : α},
  Filter.Tendsto f (nhdsWithin a (Set.Ioi a)) (nhds (Function.rightLim f a)) →
    ∀ [h' : (nhdsWithin a (Set.Ioi a)).NeBot], Function.rightLim (Function.leftLim f) a = Function.rightLim f a
-- Mathlib.Data.Int.Init
Int.le_add_iff_lt_of_dvd_sub : ∀ {a b c : ℤ}, 0 < a → a ∣ c - b → (a + b ≤ c ↔ b < c)
-- Mathlib.Topology.Bornology.Basic
Bornology.IsBounded.union : ∀ {α : Type u_2} {x : Bornology α} {s t : Set α},
  Bornology.IsBounded s → Bornology.IsBounded t → Bornology.IsBounded (s ∪ t)
-- Mathlib.Analysis.RCLike.Basic
/-- Left scalar multiplication of a unit with norm one and a linear isometric equivalence,
as a linear isometric equivalence.  -/
LinearIsometryEquiv.instSMulSubtypeMemSubmonoidUnitaryId : {𝕜 : Type u_3} →
  {V : Type u_4} →
    {W : Type u_5} →
      [inst : RCLike 𝕜] →
        [inst_1 : SeminormedAddCommGroup V] →
          [inst_2 : Module 𝕜 V] →
            [inst_3 : SeminormedAddCommGroup W] → [inst_4 : NormedSpace 𝕜 W] → SMul (↥(unitary 𝕜)) (V ≃ₗᵢ[𝕜] W)
-- Mathlib.Order.Interval.Basic
NonemptyInterval.mem_pure_self : ∀ {α : Type u_1} [inst : Preorder α] (a : α), a ∈ NonemptyInterval.pure a
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.induction_left : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] {motive : Monoid.CoprodI M → Prop}
  (m : Monoid.CoprodI M),
  motive 1 → (∀ {i : ι} (m : M i) (x : Monoid.CoprodI M), motive x → motive (Monoid.CoprodI.of m * x)) → motive m
-- Mathlib.CategoryTheory.MorphismProperty.LiftingProperty
CategoryTheory.MorphismProperty.llp_of_isIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (T : CategoryTheory.MorphismProperty C) {A B : C} (i : A ⟶ B)
  [CategoryTheory.IsIso i], T.llp i
-- Mathlib.Data.Int.Init
Int.inductionOn'.pos.eq_2 : ∀ {motive : ℤ → Sort u_1} (b : ℤ) (zero : motive b) (succ : (k : ℤ) → b ≤ k → motive k → motive (k + 1)) (n_1 : ℕ),
  Int.inductionOn'.pos b zero succ n_1.succ = cast ⋯ (succ (b + ↑n_1) ⋯ (Int.inductionOn'.pos b zero succ n_1))
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.Mor₂Iso.coherenceComp.sizeOf_spec : ∀ (e : Lean.Expr) (f g h i : Mathlib.Tactic.BicategoryLike.Mor₁) (α : Mathlib.Tactic.BicategoryLike.CoherenceHom)
  (η θ : Mathlib.Tactic.BicategoryLike.Mor₂Iso),
  sizeOf (Mathlib.Tactic.BicategoryLike.Mor₂Iso.coherenceComp e f g h i α η θ) =
    1 + sizeOf e + sizeOf f + sizeOf g + sizeOf h + sizeOf i + sizeOf α + sizeOf η + sizeOf θ
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKeyD_insertMany_list_of_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {l : List ((a : α) × β a)} {k k' fallback : α},
      cmp k k' = Ordering.eq →
        List.Pairwise (fun a b => ¬cmp a.fst b.fst = Ordering.eq) l →
          k ∈ List.map Sigma.fst l → (t.insertMany l).getKeyD k' fallback = k
-- Mathlib.RingTheory.DividedPowerAlgebra.Init
DividedPowerAlgebra.dp_zero : ∀ {R : Type u_2} {M : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {m : M},
  DividedPowerAlgebra.dp R 0 m = 1
-- Lean.Data.FuzzyMatching
_private.Lean.Data.FuzzyMatching.0.Lean.FuzzyMatching.containsInOrderLower.go : String → String → String.Pos.Raw → String.Pos.Raw → Bool
-- Mathlib.Analysis.Calculus.Deriv.Add
deriv_fun_sub : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f g : 𝕜 → F} {x : 𝕜},
  DifferentiableAt 𝕜 f x → DifferentiableAt 𝕜 g x → deriv (fun y => f y - g y) x = deriv f x - deriv g x
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.lift.congr_simp : ∀ {S : Type u_1} {R : Type u} {M : Type v} [inst : CommSemiring S] [inst_1 : Semiring R] [inst_2 : AddCommMonoid M]
  [inst_3 : Algebra S R] [inst_4 : Module S M] [inst_5 : Module R M] [inst_6 : Module Rᵐᵒᵖ M]
  [inst_7 : SMulCommClass R Rᵐᵒᵖ M] [inst_8 : IsScalarTower S R M] [inst_9 : IsScalarTower S Rᵐᵒᵖ M] {A : Type u_2}
  [inst_10 : Semiring A] [inst_11 : Algebra S A] (f f_1 : R →ₐ[S] A) (e_f : f = f_1) (g g_1 : M →ₗ[S] A) (e_g : g = g_1)
  (hg : ∀ (x y : M), g x * g y = 0) (hfg : ∀ (r : R) (x : M), g (r • x) = f r * g x)
  (hgf : ∀ (r : R) (x : M), g (MulOpposite.op r • x) = g x * f r),
  TrivSqZeroExt.lift f g hg hfg hgf = TrivSqZeroExt.lift f_1 g_1 ⋯ ⋯ ⋯
-- Mathlib.Probability.ProbabilityMassFunction.Basic
PMF.apply_pos_iff : ∀ {α : Type u_1} (p : PMF α) (a : α), 0 < p a ↔ a ∈ p.support
-- Mathlib.Analysis.Normed.Group.Basic
norm_natAbs_smul : ∀ {E : Type u_5} [inst : SeminormedAddGroup E] (a : E) (n : ℤ), ‖n.natAbs • a‖ = ‖n • a‖
-- Lean.Elab.DeprecatedSyntax
Lean.Elab.SyntaxDeprecationEntry.mk.inj : ∀ {kind : Lean.SyntaxNodeKind} {text? since? : Option String} {kind_1 : Lean.SyntaxNodeKind}
  {text?_1 since?_1 : Option String},
  { kind := kind, text? := text?, since? := since? } = { kind := kind_1, text? := text?_1, since? := since?_1 } →
    kind = kind_1 ∧ text? = text?_1 ∧ since? = since?_1
-- Mathlib.AlgebraicGeometry.Morphisms.Immersion
AlgebraicGeometry.IsImmersion.instMorphismRestrict : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (V : Y.Opens) [AlgebraicGeometry.IsImmersion f],
  AlgebraicGeometry.IsImmersion (f ∣_ V)
-- Mathlib.RingTheory.Spectrum.Prime.Module
Module.stableUnderSpecialization_support : ∀ {R : Type u_1} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  StableUnderSpecialization (Module.support R M)
-- Mathlib.LinearAlgebra.QuadraticForm.Basis
/-- From a free module, every quadratic map can be built from a bilinear form.

See `BilinMap.not_forall_toQuadraticMap_surjective` for a counterexample when the module is
not free.  -/
LinearMap.BilinMap.toQuadraticMap_surjective : ∀ {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup N]
  [inst_3 : Module R M] [inst_4 : Module R N] [Module.Free R M], Function.Surjective LinearMap.BilinMap.toQuadraticMap
-- Init.Data.List.Erase
_private.Init.Data.List.Erase.0.List.eraseIdx.match_1.eq_3 : ∀ {α : Type u_1} (motive : List α → ℕ → Sort u_2) (a : α) (as : List α) (n : ℕ) (h_1 : (x : ℕ) → motive [] x)
  (h_2 : (head : α) → (as : List α) → motive (head :: as) 0)
  (h_3 : (a : α) → (as : List α) → (n : ℕ) → motive (a :: as) n.succ),
  (match a :: as, n.succ with
    | [], x => h_1 x
    | head :: as, 0 => h_2 head as
    | a :: as, n.succ => h_3 a as n) =
    h_3 a as n
-- Mathlib.Algebra.Order.Archimedean.Class
MulArchimedeanClass.closedBallSubgroup_top : ∀ (M : Type u_1) [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M], ⊤.closedBallSubgroup = ⊥
-- Mathlib.Algebra.Order.Archimedean.Basic
pow_unbounded_of_one_lt : ∀ {R : Type u_3} [inst : Semiring R] [inst_1 : PartialOrder R] [IsStrictOrderedRing R] [Archimedean R] {y : R}
  [ExistsAddOfLE R] (x : R), 1 < y → ∃ n, x < y ^ n
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
/-- Uniformizers are nonzero.  -/
IsDedekindDomain.HeightOneSpectrum.valuation_uniformizer_ne_zero : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (K : Type u_2) [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R),
  Classical.choose ⋯ ≠ 0
-- Mathlib.Algebra.Algebra.Bilinear
/-- The multiplication in a non-unital algebra is a bilinear map.

A weaker version of this for non-unital non-associative algebras exists as `LinearMap.mul`.  -/
NonUnitalAlgHom.lmul : (R : Type u_1) →
  (A : Type u_2) →
    [inst : CommSemiring R] →
      [inst_1 : NonUnitalSemiring A] →
        [inst_2 : Module R A] → [SMulCommClass R A A] → [IsScalarTower R A A] → A →ₙₐ[R] Module.End R A
-- Lean.Parser.Types
Lean.Parser.ParserState.setPos : Lean.Parser.ParserState → String.Pos.Raw → Lean.Parser.ParserState
-- Lean.Data.PersistentHashMap
Lean.PersistentHashMap.maxCollisions : ℕ
-- Mathlib.Algebra.Group.Subgroup.Defs
AddSubgroup.mem_carrier : ∀ {G : Type u_1} [inst : AddGroup G] {s : AddSubgroup G} {x : G}, x ∈ s.carrier ↔ x ∈ s
-- Lean.Expr
Lean.mkAppEx : Lean.Expr → Lean.Expr → Lean.Expr
-- Mathlib.Tactic.NormNum.Irrational
/-- `norm_num` extension that proves `Irrational √x` for rational `x`.  -/
Mathlib.Meta.NormNum.evalIrrationalSqrt : Mathlib.Meta.NormNum.NormNumExt
-- Std.Data.HashMap.Lemmas
Std.HashMap.isEmpty_filterMap_iff : ∀ {α : Type u} {β : Type v} {γ : Type w} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α]
  [LawfulHashable α] {f : α → β → Option γ},
  (Std.HashMap.filterMap f m).isEmpty = true ↔ ∀ (k : α) (h : k ∈ m), f (m.getKey k h) m[k] = none
-- Mathlib.Algebra.Order.Antidiag.Finsupp
Finset.finsuppAntidiag_empty : ∀ {ι : Type u_1} {μ : Type u_2} [inst : DecidableEq ι] [inst_1 : AddCommMonoid μ] [inst_2 : Finset.HasAntidiagonal μ]
  [inst_3 : DecidableEq μ] (n : μ), ∅.finsuppAntidiag n = if n = 0 then {0} else ∅
-- Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex
/-- The binary product `Δ[p] ⊗ Δ[q]` identifies to the nerve
of `ULift (Fin (p + 1) × Fin (q + 1))`.  -/
SSet.prodStdSimplex.isoNerve : (p q : ℕ) →
  CategoryTheory.MonoidalCategoryStruct.tensorObj (SSet.stdSimplex.obj { len := p })
      (SSet.stdSimplex.obj { len := q }) ≅
    CategoryTheory.nerve (ULift.{u, 0} (Fin (p + 1) × Fin (q + 1)))
-- Mathlib.SetTheory.Cardinal.Order
/-- **Cantor's theorem**  -/
Cardinal.cantor : ∀ (a : Cardinal.{u}), a < 2 ^ a
-- Mathlib.Algebra.Category.CoalgCat.Basic
CoalgCat.mk.sizeOf_spec : ∀ {R : Type u} [inst : CommRing R] [inst_1 : SizeOf R] (toModuleCat : ModuleCat R)
  (instCoalgebra : Coalgebra R ↑toModuleCat),
  sizeOf { toModuleCat := toModuleCat, instCoalgebra := instCoalgebra } = 1 + sizeOf toModuleCat + sizeOf instCoalgebra
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.FilterMap.0.Std.Iter.step_filterMapWithPostcondition.match_3.eq_2 : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] {it : Std.Iter β} (motive : it.Step → Sort u_2) (it' : Std.Iter β)
  (h : it.IsPlausibleStep (Std.IterStep.skip it'))
  (h_1 :
    (it' : Std.Iter β) →
      (out : β) → (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 : (it' : Std.Iter β) → (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (h : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩),
  (match ⟨Std.IterStep.skip it', h⟩ with
    | ⟨Std.IterStep.yield it' out, h⟩ => h_1 it' out h
    | ⟨Std.IterStep.skip it', h⟩ => h_2 it' h
    | ⟨Std.IterStep.done, h⟩ => h_3 h) =
    h_2 it' h
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.maxKey?_le_maxKey?_insertIfNew! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  (h : t.WF) {k : α} {v : β k} {km kmi : α},
  t.maxKey? = some km →
    (Std.DTreeMap.Internal.Impl.insertIfNew! k v t).maxKey?.get ⋯ = kmi → (compare km kmi).isLE = true
-- Mathlib.Algebra.Star.SelfAdjoint
IsSelfAdjoint.eq_1 : ∀ {R : Type u_1} [inst : Star R] (x : R), IsSelfAdjoint x = (star x = x)
-- Mathlib.CategoryTheory.Limits.Final
CategoryTheory.Functor.Initial.out : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} D}
  {F : CategoryTheory.Functor C D} [self : F.Initial] (d : D),
  CategoryTheory.IsConnected (CategoryTheory.CostructuredArrow F d)
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.Mor₂Iso.coherenceComp.injEq : ∀ (e : Lean.Expr) (f g h i : Mathlib.Tactic.BicategoryLike.Mor₁) (α : Mathlib.Tactic.BicategoryLike.CoherenceHom)
  (η θ : Mathlib.Tactic.BicategoryLike.Mor₂Iso) (e_1 : Lean.Expr) (f_1 g_1 h_1 i_1 : Mathlib.Tactic.BicategoryLike.Mor₁)
  (α_1 : Mathlib.Tactic.BicategoryLike.CoherenceHom) (η_1 θ_1 : Mathlib.Tactic.BicategoryLike.Mor₂Iso),
  (Mathlib.Tactic.BicategoryLike.Mor₂Iso.coherenceComp e f g h i α η θ =
      Mathlib.Tactic.BicategoryLike.Mor₂Iso.coherenceComp e_1 f_1 g_1 h_1 i_1 α_1 η_1 θ_1) =
    (e = e_1 ∧ f = f_1 ∧ g = g_1 ∧ h = h_1 ∧ i = i_1 ∧ α = α_1 ∧ η = η_1 ∧ θ = θ_1)
-- Mathlib.Data.Fintype.Card
Fintype.card_compl_set : ∀ {α : Type u_1} [inst : Fintype α] (s : Set α) [inst_1 : Fintype ↑s] [inst_2 : Fintype ↑sᶜ],
  Fintype.card ↑sᶜ = Fintype.card α - Fintype.card ↑s
-- Mathlib.FieldTheory.SeparableClosure
/-- An intermediate field of `E / F` is contained in the separable closure of `F` in `E`
if all of its elements are separable over `F`.  -/
le_separableClosure' : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {L : IntermediateField F E},
  (∀ (x : ↥L), IsSeparable F x) → L ≤ separableClosure F E
-- Mathlib.CategoryTheory.Extensive
CategoryTheory.FinitaryPreExtensive.hasPullbacksOfInclusions : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.FinitaryPreExtensive C],
  CategoryTheory.HasPullbacksOfInclusions C
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKeyD_union_of_contains_eq_false_left : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h₁ : m₁.WF)
  (h₂ : m₂.WF) {k fallback : α},
  Std.DTreeMap.Internal.Impl.contains k m₁ = false → (m₁.union m₂ ⋯ ⋯).getKeyD k fallback = m₂.getKeyD k fallback
-- Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Real.tendsto_deriv_mul_log_atTop : Filter.Tendsto (fun x => deriv (fun x => x * Real.log x) x) Filter.atTop Filter.atTop
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.rpow_le_self_of_one_le : ∀ {x y : ℝ}, 1 ≤ x → y ≤ 1 → x ^ y ≤ x
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.ext_iff_val : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A] {𝒜 : ι → σ} {x : Submonoid A}
  (f g : HomogeneousLocalization 𝒜 x), f = g ↔ f.val = g.val
-- Mathlib.Tactic.CategoryTheory.Coherence
/-- The same as `pure_coherence`, but used internally in `coherence` without the warning.  -/
Mathlib.Tactic.Coherence.pure_coherence_internal : Lean.ParserDescr
-- Mathlib.Data.Finset.Powerset
Finset.notMem_of_mem_powerset_of_notMem : ∀ {α : Type u_1} {s t : Finset α} {a : α}, t ∈ s.powerset → a ∉ s → a ∉ t
-- Lean.Compiler.IR.Basic
Lean.IR.Alt.modifyBodyM : {m : Type → Type} → [Monad m] → (Lean.IR.FnBody → m Lean.IR.FnBody) → Lean.IR.Alt → m Lean.IR.Alt
-- Std.Async.UDP
Std.Async.UDP.Membership.enterGroup.sizeOf_spec : sizeOf Std.Async.UDP.Membership.enterGroup = 1
-- Mathlib.CategoryTheory.Shift.SingleFunctors
CategoryTheory.SingleFunctors.Hom.mk.inj : ∀ {C : Type u_1} {D : Type u_2} {inst : CategoryTheory.Category.{v_1, u_1} C}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} D} {A : Type u_5} {inst_2 : AddMonoid A}
  {inst_3 : CategoryTheory.HasShift D A} {F G : CategoryTheory.SingleFunctors C D A}
  {hom : (a : A) → F.functor a ⟶ G.functor a}
  {comm :
    autoParam
      (∀ (n a a' : A) (ha' : n + a = a'),
        CategoryTheory.CategoryStruct.comp (F.shiftIso n a a' ha').hom (hom a) =
          CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Functor.whiskerRight (hom a') (CategoryTheory.shiftFunctor D n))
            (G.shiftIso n a a' ha').hom)
      CategoryTheory.SingleFunctors.Hom.comm._autoParam}
  {hom_1 : (a : A) → F.functor a ⟶ G.functor a}
  {comm_1 :
    autoParam
      (∀ (n a a' : A) (ha' : n + a = a'),
        CategoryTheory.CategoryStruct.comp (F.shiftIso n a a' ha').hom (hom_1 a) =
          CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Functor.whiskerRight (hom_1 a') (CategoryTheory.shiftFunctor D n))
            (G.shiftIso n a a' ha').hom)
      CategoryTheory.SingleFunctors.Hom.comm._autoParam},
  { hom := hom, comm := comm } = { hom := hom_1, comm := comm_1 } → hom = hom_1
-- Mathlib.Algebra.RingQuot
RingQuot.pow_quot : ∀ {R : Type uR} [inst : Semiring R] (r : R → R → Prop) {a : R} {n : ℕ},
  { toQuot := Quot.mk (RingQuot.Rel r) a } ^ n = { toQuot := Quot.mk (RingQuot.Rel r) (a ^ n) }
-- Mathlib.Analysis.Convex.StdSimplex
stdSimplex_fin_two : ∀ (𝕜 : Type u_2) [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [ZeroLEOneClass 𝕜] [IsOrderedRing 𝕜],
  stdSimplex 𝕜 (Fin 2) = segment 𝕜 (Pi.single 0 1) (Pi.single 1 1)
-- Init.Data.UInt.Bitwise
UInt16.ofNatLT_xor : ∀ (a b : ℕ) (ha : a < 2 ^ 16) (hb : b < 2 ^ 16),
  UInt16.ofNatLT (a ^^^ b) ⋯ = UInt16.ofNatLT a ha ^^^ UInt16.ofNatLT b hb
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.LeftFraction.map_ofHom : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (W : CategoryTheory.MorphismProperty C) {X Y : C} (f : X ⟶ Y)
  (L : CategoryTheory.Functor C D) (hL : W.IsInvertedBy L) [inst_2 : W.ContainsIdentities],
  (CategoryTheory.MorphismProperty.LeftFraction.ofHom W f).map L hL = L.map f
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toArray_rco_eq_empty : ∀ {m n : ℕ}, n ≤ m → (m...n).toArray = #[]
-- Mathlib.GroupTheory.Perm.Cycle.Factors
Equiv.Perm.cycleOf_mul_of_apply_right_eq_self : ∀ {α : Type u_2} {f g : Equiv.Perm α} [inst : DecidableRel f.SameCycle] [inst_1 : DecidableRel (f * g).SameCycle],
  Commute f g → ∀ (x : α), g x = x → (f * g).cycleOf x = f.cycleOf x
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.interSmallerFn.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (l sofar : List ((a : α) × β a)) (k : α),
  Std.Internal.List.interSmallerFn l sofar k =
    match Std.Internal.List.getEntry? k l with
    | some kv' => Std.Internal.List.insertEntry kv'.fst kv'.snd sofar
    | none => sofar
-- Mathlib.SetTheory.Ordinal.Notation
ONote.lt_def : ∀ {x y : ONote}, x < y ↔ x.repr < y.repr
-- Mathlib.NumberTheory.ModularForms.LevelOne.Basic
/-- If a constant function is modular of weight `k`, then either `k = 0`, or the constant is `0`.  -/
SlashInvariantForm.wt_eq_zero_of_eq_const : ∀ {F : Type u_1} [inst : FunLike F UpperHalfPlane ℂ] (k : ℤ)
  [SlashInvariantFormClass F (Matrix.SpecialLinearGroup.mapGL ℝ).range k] {f : F} {c : ℂ},
  ⇑f = Function.const UpperHalfPlane c → k = 0 ∨ c = 0
-- Mathlib.Algebra.Algebra.Subalgebra.MulOpposite
Subalgebra.op_sInf : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  (S : Set (Subalgebra R A)), (sInf S).op = sInf (Subalgebra.unop ⁻¹' S)
-- Mathlib.GroupTheory.PGroup
IsPGroup.of_pow : ∀ {p : ℕ} {G : Type u_1} [inst : Group G] {n : ℕ}, IsPGroup (p ^ n) G → IsPGroup p G
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Real
NNReal.instMeasurableSMul₂ENNReal : MeasurableSMul₂ NNReal ENNReal
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp.Completion
SemiNormedGrp.completion_map : ∀ {X Y : SemiNormedGrp} (f : X ⟶ Y),
  SemiNormedGrp.completion.map f = SemiNormedGrp.ofHom (SemiNormedGrp.Hom.hom f).completion
-- Init.Data.SInt.Lemmas
Int8.toISize_le : ∀ {a b : Int8}, a.toISize ≤ b.toISize ↔ a ≤ b
-- Mathlib.Algebra.Group.InjSurj
Function.Surjective.group.eq_1 : ∀ {M₁ : Type u_1} {M₂ : Type u_2} [inst : Mul M₂] [inst_1 : One M₂] [inst_2 : Pow M₂ ℕ] [inst_3 : Inv M₂]
  [inst_4 : Div M₂] [inst_5 : Pow M₂ ℤ] [inst_6 : Group M₁] (f : M₁ → M₂) (hf : Function.Surjective f) (one : f 1 = 1)
  (mul : ∀ (x y : M₁), f (x * y) = f x * f y) (inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹)
  (div : ∀ (x y : M₁), f (x / y) = f x / f y) (npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n)
  (zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n),
  Function.Surjective.group f hf one mul inv div npow zpow =
    { toDivInvMonoid := Function.Surjective.divInvMonoid f hf one mul inv div npow zpow, inv_mul_cancel := ⋯ }
-- Mathlib.Analysis.Calculus.ContDiff.Basic
/-- Composition with a linear isometry on the left preserves the norm of the iterated
derivative within a set.  -/
LinearIsometry.norm_iteratedFDerivWithin_comp_left : ∀ {𝕜 : 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] {s : Set E} {x : E} {n : WithTop ℕ∞} {f : E → F}
  (g : F →ₗᵢ[𝕜] G),
  ContDiffWithinAt 𝕜 n f s x →
    UniqueDiffOn 𝕜 s →
      x ∈ s → ∀ {i : ℕ}, ↑i ≤ n → ‖iteratedFDerivWithin 𝕜 i (⇑g ∘ f) s x‖ = ‖iteratedFDerivWithin 𝕜 i f s x‖
-- Std.Data.Iterators.Lemmas.Equivalence.HetT
Std.Iterators.instLawfulMonadHetT : ∀ {m : Type u_1 → Type u_2} [inst : Monad m] [LawfulMonad m], LawfulMonad (Std.Iterators.HetT m)
-- Std.Async.Basic
/-- Maps a function over a `MaybeTask`.
 -/
Std.Async.MaybeTask.map : {α β : Type} →
  (α → β) →
    optParam Task.Priority Task.Priority.default → optParam Bool false → Std.Async.MaybeTask α → Std.Async.MaybeTask β
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.Lp.eq_zero_iff_ae_eq_zero : ∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] {f : ↥(MeasureTheory.Lp E p μ)}, f = 0 ↔ ↑↑f =ᵐ[μ] 0
-- Mathlib.CategoryTheory.Galois.IsFundamentalgroup
/-- If `G` is a compact, topological group that acts continuously and naturally on the
fibers of `F`, `toAut F G` is surjective if and only if it acts transitively on the fibers
of all Galois objects. This is the `if` direction. For the `only if` see
`isPretransitive_of_surjective`.  -/
CategoryTheory.PreGaloisCategory.toAut_surjective_of_isPretransitive : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) (G : Type u_1)
  [inst_1 : Group G] [inst_2 : (X : C) → MulAction G (F.obj X).obj]
  [inst_3 : CategoryTheory.PreGaloisCategory.IsNaturalSMul F G] [inst_4 : CategoryTheory.GaloisCategory C]
  [CategoryTheory.PreGaloisCategory.FiberFunctor F] [inst_6 : TopologicalSpace G] [IsTopologicalGroup G]
  [CompactSpace G] [∀ (X : C), ContinuousSMul G (F.obj X).obj],
  (∀ (X : C) [CategoryTheory.PreGaloisCategory.IsGalois X], MulAction.IsPretransitive G (F.obj X).obj) →
    Function.Surjective ⇑(CategoryTheory.PreGaloisCategory.toAut F G)
-- Mathlib.Computability.Primrec.Basic
Primrec.nat_sub : Primrec₂ fun x1 x2 => x1 - x2