mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.List.Dedup
List.Nodup.dedup : ∀ {α : Type u_1} [inst : DecidableEq α] {l : List α}, l.Nodup → l.dedup = l
-- Mathlib.Order.Interval.Basic
NonemptyInterval.coe_coeHom : ∀ {α : Type u_1} [inst : PartialOrder α], ⇑NonemptyInterval.coeHom = SetLike.coe
-- Mathlib.AlgebraicTopology.ModelCategory.Instances
HomotopicalAlgebra.instFibrationCompOfIsStableUnderCompositionFibrations : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z)
  [inst_1 : HomotopicalAlgebra.CategoryWithFibrations C] [(HomotopicalAlgebra.fibrations C).IsStableUnderComposition]
  [hf : HomotopicalAlgebra.Fibration f] [hg : HomotopicalAlgebra.Fibration g],
  HomotopicalAlgebra.Fibration (CategoryTheory.CategoryStruct.comp f g)
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
ModuleCat.homEquiv_extendScalarsComp : ∀ {R₁ R₂ R₃ : Type u₁} [inst : CommRing R₁] [inst_1 : CommRing R₂] [inst_2 : CommRing R₃] (f₁₂ : R₁ →+* R₂)
  (f₂₃ : R₂ →+* R₃) (M : ModuleCat R₁),
  ((ModuleCat.extendRestrictScalarsAdj (f₂₃.comp f₁₂)).homEquiv M
        (((ModuleCat.extendScalars f₁₂).comp (ModuleCat.extendScalars f₂₃)).obj M))
      ((ModuleCat.extendScalarsComp f₁₂ f₂₃).hom.app M) =
    CategoryTheory.CategoryStruct.comp ((ModuleCat.extendRestrictScalarsAdj f₁₂).unit.app M)
      (CategoryTheory.CategoryStruct.comp
        ((ModuleCat.restrictScalars f₁₂).map
          ((ModuleCat.extendRestrictScalarsAdj f₂₃).unit.app (ModuleCat.ExtendScalars.obj' f₁₂ M)))
        ((ModuleCat.restrictScalarsComp f₁₂ f₂₃).inv.app
          ((ModuleCat.extendScalars f₂₃).obj (ModuleCat.ExtendScalars.obj' f₁₂ M))))
-- Std.Sat.AIG.Lemmas
Std.Sat.AIG.denote_invert_true : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {assign : α → Bool} {aig : Std.Sat.AIG α} {gate : ℕ}
  {hgate : gate < aig.decls.size},
  ⟦assign, { aig := aig, ref := { gate := gate, invert := true, hgate := hgate } }⟧ =
    !⟦assign, { aig := aig, ref := { gate := gate, invert := false, hgate := hgate } }⟧
-- Init.Data.UInt.Bitwise
USize.not_zero : ~~~0 = -1
-- Mathlib.Topology.MetricSpace.Ultra.Basic
dist_triangle_max : ∀ {X : Type u_1} [inst : PseudoMetricSpace X] [IsUltrametricDist X] (x y z : X), dist x z ≤ max (dist x y) (dist y z)
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
LinearIndependent.linearCombinationEquiv_symm_apply : ∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] (hv : LinearIndependent R v) (a : ↥(Submodule.span R (Set.range v))),
  hv.linearCombinationEquiv.symm a =
    ((LinearEquiv.ofInjective (LinearMap.codRestrict (Submodule.span R (Set.range v)) (Finsupp.linearCombination R v) ⋯)
                ⋯).toEquiv.trans
          (LinearEquiv.ofTop
              (LinearMap.codRestrict (Submodule.span R (Set.range v)) (Finsupp.linearCombination R v) ⋯).range
              ⋯).toEquiv).invFun
      a
-- Mathlib.Algebra.Homology.ExactSequence
CategoryTheory.ShortComplex.exact_iff_exact_toComposableArrows : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C), S.Exact ↔ S.toComposableArrows.Exact
-- Mathlib.SetTheory.Ordinal.Principal
Ordinal.isPrincipal_swap_iff : ∀ {o : Ordinal.{u}} {op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}},
  Ordinal.IsPrincipal (Function.swap op) o ↔ Ordinal.IsPrincipal op o
-- Mathlib.Algebra.Group.Translate
/-- Translation of a function in a group by an element of that group.
`τ a f` is defined as `x ↦ f (x - a)`.  -/
translate : {α : Type u_2} → {G : Type u_5} → [AddCommGroup G] → G → (G → α) → G → α
-- Mathlib.Algebra.Lie.Ideal
lie_mem_right : ∀ (R : Type u) (L : Type v) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (I : LieIdeal R L)
  (x y : L), y ∈ I → ⁅x, y⁆ ∈ I
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.Equiv.map_constants : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N] (φ : L.Equiv M N)
  (c : L.Constants), φ ↑c = ↑c
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
/-- **Alias** of `Metric.closedBall_sdiff_sphere`. -/
Metric.closedBall_diff_sphere : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x : α} {ε : ℝ}, Metric.closedBall x ε \ Metric.sphere x ε = Metric.ball x ε
-- Mathlib.Analysis.Asymptotics.ExpGrowth
ExpGrowth.expGrowthSup_zero : ExpGrowth.expGrowthSup 0 = ⊥
-- Mathlib.Analysis.Normed.Group.Basic
ofReal_norm' : ∀ {E : Type u_5} [inst : SeminormedGroup E] (x : E), ENNReal.ofReal ‖x‖ = ‖x‖ₑ
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.containsₘ_eq_containsKey : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α] {k : α}
  {l : Std.DTreeMap.Internal.Impl α β}, l.Ordered → l.containsₘ k = Std.Internal.List.containsKey k l.toListModel
-- Mathlib.Data.Finset.Interval
Finset.Ioo_eq_filter_ssubsets : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Finset α), Finset.Ioo s t = {u ∈ t.ssubsets | s ⊂ u}
-- Mathlib.Order.BooleanAlgebra.Set
/-- **Alias** of `Set.sdiff_subset_sdiff`. -/
Set.diff_subset_diff : ∀ {α : Type u_1} {s₁ s₂ t₁ t₂ : Set α}, s₁ ⊆ s₂ → t₂ ⊆ t₁ → s₁ \ t₁ ⊆ s₂ \ t₂
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.instReprCtorInfo : Repr Lean.Compiler.LCNF.CtorInfo
-- Mathlib.RingTheory.Invariant.Basic
/-- Characteristic polynomial of a finite group action on a ring.  -/
MulSemiringAction.charpoly : {B : Type u_2} →
  (G : Type u_3) → [inst : CommRing B] → [inst_1 : Group G] → [MulSemiringAction G B] → [Fintype G] → B → Polynomial B
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
mulEquivOfOrderOfEq.eq_1 : ∀ {G : Type u_2} {G' : Type u_3} [inst : Group G] [inst_1 : Group G'] {g : G} (hg : ∀ (x : G), x ∈ Subgroup.zpowers g)
  {g' : G'} (hg' : ∀ (x : G'), x ∈ Subgroup.zpowers g') (h : orderOf g = orderOf g'),
  mulEquivOfOrderOfEq hg hg' h = (monoidHomOfForallMemZpowers hg ⋯).toMulEquiv (monoidHomOfForallMemZpowers hg' ⋯) ⋯ ⋯
-- Mathlib.MeasureTheory.Function.AEEqOfIntegral
MeasureTheory.ae_nonneg_of_forall_setIntegral_nonneg_of_sigmaFinite : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ] {f : α → ℝ},
  (∀ (s : Set α), MeasurableSet s → μ s < ⊤ → MeasureTheory.IntegrableOn f s μ) →
    (∀ (s : Set α), MeasurableSet s → μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ) → 0 ≤ᵐ[μ] f
-- Mathlib.CategoryTheory.Localization.DerivabilityStructure.PointwiseRightDerived
CategoryTheory.LocalizerMorphism.hasPointwiseRightDerivedFunctor_iff_of_isRightDerivabilityStructure : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {H : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} H]
  {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂}
  (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) (F : CategoryTheory.Functor C₂ H) [Φ.IsRightDerivabilityStructure],
  F.HasPointwiseRightDerivedFunctor W₂ ↔ (Φ.functor.comp F).HasPointwiseRightDerivedFunctor W₁
-- Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Subgroup.eq_bot_or_eq_top_of_prime_card : ∀ {G : Type u_2} [inst : Group G] (H : Subgroup G) [hp : Fact (Nat.Prime (Nat.card G))], H = ⊥ ∨ H = ⊤
-- Mathlib.GroupTheory.FreeAbelianGroup
FreeAbelianGroup.induction_on : ∀ {α : Type u} {motive : FreeAbelianGroup α → Prop} (z : FreeAbelianGroup α),
  motive 0 →
    (∀ (x : α), motive (FreeAbelianGroup.of x)) →
      (∀ (x : α), motive (FreeAbelianGroup.of x) → motive (-FreeAbelianGroup.of x)) →
        (∀ (x y : FreeAbelianGroup α), motive x → motive y → motive (x + y)) → motive z
-- Mathlib.SetTheory.Cardinal.Defs
Cardinal.mk_ne_zero_iff : ∀ {α : Type u}, Cardinal.mk α ≠ 0 ↔ Nonempty α
-- Mathlib.Algebra.Order.Archimedean.Class
MulArchimedeanClass.ballSubgroup_antitone : ∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M],
  Antitone MulArchimedeanClass.ballSubgroup
-- Mathlib.Order.OrderIsoNat
/-- A value is accessible iff it isn't contained in any infinite decreasing sequence.  -/
RelEmbedding.acc_iff_isEmpty_subtype_mem_range : ∀ {α : Type u_1} {r : α → α → Prop} [IsStrictOrder α r] {x : α}, Acc r x ↔ IsEmpty { f // x ∈ Set.range ⇑f }
-- Mathlib.Data.Fin.SuccPred
/-- Sending `Fin n` into `Fin (n + 1)` with a gap at `p`
then back to `Fin n` by subtracting one from anything above `p` is the identity.  -/
Fin.predAbove_succAbove : ∀ {n : ℕ} (p i : Fin n), p.predAbove (p.castSucc.succAbove i) = i
-- Mathlib.CategoryTheory.Limits.Types.Coproducts
CategoryTheory.Limits.Types.binaryCoproductIso_inr_comp_inv_apply : ∀ (X Y : Type u) (x : Y),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Types.binaryCoproductIso X Y).inv) (Sum.inr x) =
    (CategoryTheory.ConcreteCategory.hom CategoryTheory.Limits.coprod.inr) x
-- Mathlib.Algebra.Category.ModuleCat.Kernels
ModuleCat.kernelIsoKer_inv_kernel_ι : ∀ {R : Type u} [inst : Ring R] {G H : ModuleCat R} (f : G ⟶ H),
  CategoryTheory.CategoryStruct.comp (ModuleCat.kernelIsoKer f).inv (CategoryTheory.Limits.kernel.ι f) =
    ModuleCat.ofHom (ModuleCat.Hom.hom f).ker.subtype
-- Mathlib.Logic.Equiv.Basic
Equiv.piCongrSet_apply : ∀ {α : Type u_11} {W : α → Sort w} {s t : Set α} (h : s = t) (f : (i : { i // i ∈ s }) → W ↑i) (i : { i // i ∈ t }),
  (Equiv.piCongrSet h) f i = f ⟨↑i, ⋯⟩
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.Code.nil_eval : ∀ (v : List ℕ), Turing.ToPartrec.Code.nil.eval v = pure []
-- Init.Data.Nat.Lemmas
Nat.pow_mod : ∀ (a b n : ℕ), a ^ b % n = (a % n) ^ b % n
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Projective
Matrix.ProjectiveSpecialLinearGroup.toPGL_injective : ∀ {n : Type u_1} {R : Type u_2} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing R],
  Function.Injective ⇑Matrix.ProjectiveSpecialLinearGroup.toPGL
-- Std.Http.Data.Method
Std.Http.Method.instToString : ToString Std.Http.Method
-- Mathlib.Topology.Order.OrderClosed
Subtype.instOrderClosedTopology : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : Preorder α] [t : OrderClosedTopology α] {p : α → Prop},
  OrderClosedTopology (Subtype p)
-- Mathlib.Algebra.Order.Monoid.Units
Units.instMinOfLinearOrder : {α : Type u_1} → [inst : Monoid α] → [LinearOrder α] → Min αˣ
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.containsThenInsertIfNew_fst : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {v : β k}, (m.containsThenInsertIfNew k v).1 = m.contains k
-- Mathlib.Logic.Equiv.Defs
/-- Transfer `Min` across an `Equiv`.  -/
Equiv.min : {α : Type u_1} → {β : Type u_2} → α ≃ β → [Min β] → Min α
-- Mathlib.MeasureTheory.Group.IntegralConvolution
MeasureTheory.integral_mconv : ∀ {M : Type u_1} {F : Type u_2} [inst : Monoid M] {mM : MeasurableSpace M} [MeasurableMul₂ M]
  [inst_2 : NormedAddCommGroup F] {μ ν : MeasureTheory.Measure M} {f : M → F} [inst_3 : NormedSpace ℝ F]
  [MeasureTheory.SFinite μ] [MeasureTheory.SFinite ν],
  MeasureTheory.Integrable f (μ.mconv ν) → ∫ (x : M), f x ∂μ.mconv ν = ∫ (x : M), ∫ (y : M), f (x * y) ∂ν ∂μ
-- Mathlib.Algebra.Group.Subgroup.Basic
AddAut.characteristic.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G) [inst_1 : H.Characteristic],
  AddAut.characteristic H =
    {
      toFun := fun φ =>
        { toFun := fun h => ⟨φ ↑h, ⋯⟩, invFun := fun h => ⟨(AddEquiv.symm φ) ↑h, ⋯⟩, left_inv := ⋯, right_inv := ⋯,
          map_add' := ⋯ },
      map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.Topology.Category.Profinite.Nobeling.Basic
Profinite.NobelingProof.πs'_apply_apply : ∀ {I : Type u} (C : Set (I → Bool)) [inst : LinearOrder I] [inst_1 : WellFoundedLT I] {o₁ o₂ : Ordinal.{u}}
  (h : o₁ ≤ o₂) (g : LocallyConstant ↑(Profinite.NobelingProof.π C fun x => Profinite.NobelingProof.ord I x < o₁) ℤ)
  (a : ↑(Profinite.NobelingProof.π C fun x => Profinite.NobelingProof.ord I x < o₂)),
  ((Profinite.NobelingProof.πs' C h) g) a = g (Profinite.NobelingProof.ProjRestricts C ⋯ a)
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.hasColimit_equivalence_comp : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  {C : Type u} [inst_2 : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor J C} (e : K ≌ J)
  [CategoryTheory.Limits.HasColimit F], CategoryTheory.Limits.HasColimit (e.functor.comp F)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
WeierstrassCurve.Jacobian.nonsingularLift_addMap : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Jacobian F} {P Q : WeierstrassCurve.Jacobian.PointClass F},
  W.NonsingularLift P → W.NonsingularLift Q → W.NonsingularLift (W.addMap P Q)
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.leftFractionRel_op_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty C} {X Y : C}
  (z₁ z₂ : W.RightFraction X Y),
  CategoryTheory.MorphismProperty.LeftFractionRel z₁.op z₂.op ↔ CategoryTheory.MorphismProperty.RightFractionRel z₁ z₂
-- Mathlib.Topology.Instances.ENNReal.Lemmas
ENNReal.le_of_forall_lt_one_mul_le : ∀ {x y : ENNReal}, (∀ a < 1, a * x ≤ y) → x ≤ y
-- Mathlib.GroupTheory.Congruence.Defs
Con.commGroup.eq_1 : ∀ {M : Type u_4} [inst : CommGroup M] (c : Con M), c.commGroup = { toGroup := c.group, mul_comm := ⋯ }
-- Mathlib.MeasureTheory.Group.Arithmetic
IsAddUnit.measurable_const_vadd_iff : ∀ {M : Type u_4} {β : Type u_5} {α : Type u_6} [inst : MeasurableSpace β] [inst_1 : MeasurableSpace α] {f : α → β}
  [inst_2 : AddMonoid M] [inst_3 : AddAction M β] [MeasurableConstVAdd M β] {c : M},
  IsAddUnit c → ((Measurable fun x => c +ᵥ f x) ↔ Measurable f)
-- Lean.Syntax
Lean.Syntax.getAntiquotSuffixSpliceInner : Lean.Syntax → Lean.Syntax
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsBigO.congr_of_sub : ∀ {α : Type u_1} {F : Type u_4} {E' : Type u_6} [inst : Norm F] [inst_1 : SeminormedAddCommGroup E'] {g : α → F}
  {l : Filter α} {f₁ f₂ : α → E'}, (fun x => f₁ x - f₂ x) =O[l] g → (f₁ =O[l] g ↔ f₂ =O[l] g)
-- Mathlib.Topology.Bornology.Constructions
/-- Inverse image of a bornology.  -/
Bornology.induced : {α : Type u_5} → {β : Type u_6} → [Bornology β] → (α → β) → Bornology α
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.isIso₁_truncLT_map_of_isGE : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) [CategoryTheory.IsTriangulated C],
  ∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles,
    ∀ (n : ℤ), t.IsGE T.obj₃ n → CategoryTheory.IsIso ((t.truncLT n).map T.mor₁)
-- Init.Data.Order.PackageFactories
/-- This structure contains all the data needed to create a `PartialOrderPakckage α` instance. Its
fields are automatically provided if possible. For the detailed rules how the fields are inferred,
see `PartialOrderPackage.ofLE`.
 -/
Std.Packages.PartialOrderOfLEArgs : Type u → Type u
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.insert_eq_insert : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] {a : α}, insert a m = m.insert a
-- Mathlib.RingTheory.SimpleModule.Basic
IsSemisimpleModule.quotient : ∀ {R : Type u_2} [inst : Ring R] {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {m : Submodule R M}
  [IsSemisimpleModule R M], IsSemisimpleModule R (M ⧸ m)
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.snd_map_prod_id : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) {f : β → γ},
  Measurable f → (κ.map fun a => (f a, a)).snd = κ
-- Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant
AlgebraicGeometry.instIsDominantOfIsSchemeTheoreticallyDominantOfQuasiCompact : ∀ {X S : AlgebraicGeometry.Scheme} (f : X ⟶ S) [AlgebraicGeometry.IsSchemeTheoreticallyDominant f]
  [AlgebraicGeometry.QuasiCompact f], AlgebraicGeometry.IsDominant f
-- Aesop.Index
Aesop.Index.mk.sizeOf_spec : ∀ {α : Type} [inst : SizeOf α] (byTarget byHyp : Lean.Meta.DiscrTree (Aesop.Rule α))
  (unindexed : Lean.PHashSet (Aesop.Rule α)),
  sizeOf { byTarget := byTarget, byHyp := byHyp, unindexed := unindexed } =
    1 + sizeOf byTarget + sizeOf byHyp + sizeOf unindexed
-- Lean.Data.Lsp.InitShutdown
Lean.Lsp.InitializeResult.mk : Lean.Lsp.ServerCapabilities → Option Lean.Lsp.ServerInfo → Lean.Lsp.InitializeResult
-- Lean.Environment
Lean.Kernel.Exception.invalidProj : Lean.Kernel.Environment → Lean.LocalContext → Lean.Expr → Lean.Kernel.Exception
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Units.continuousOn_zpow₀_spectrum : ∀ {R : Type u_3} {A : Type u_4} [inst : Semifield R] [inst_1 : Ring A] [inst_2 : TopologicalSpace R] [ContinuousInv₀ R]
  [inst_4 : Algebra R A] [ContinuousMul R] (a : Aˣ) (n : ℤ), ContinuousOn (fun x => x ^ n) (spectrum R ↑a)
-- Mathlib.RingTheory.Noetherian.Defs
/-- **Alias** of the forward direction of `isNoetherian_iff'`. -/
IsNoetherian.wellFoundedGT : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  IsNoetherian R M → WellFoundedGT (Submodule R M)
-- Mathlib.MeasureTheory.Function.EssSup
essInf_measure_zero : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice β] {x : MeasurableSpace α} {f : α → β}, essInf f 0 = ⊤
-- Mathlib.LinearAlgebra.Projectivization.PSL.Stabilizer
PSL.smul_submodule : ∀ {F : Type u_1} [inst : Field F] {ι : Type u_2} [inst_1 : DecidableEq ι] [inst_2 : Fintype ι]
  (g : Matrix.SpecialLinearGroup ι F) (p : Projectivization F (ι → F)), (g • p).submodule = g • p.submodule
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.d₀₁_comp_d₁₂_apply : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{max u u_1, u, u} k G) (x : ↑A),
  (CategoryTheory.ConcreteCategory.hom (groupCohomology.d₁₂ A))
      ((CategoryTheory.ConcreteCategory.hom (groupCohomology.d₀₁ A)) x) =
    0
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.IsCoseparator.isCodetector : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Balanced C] {G : C},
  CategoryTheory.IsCoseparator G → CategoryTheory.IsCodetector G
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomMulAct.smul_monoidHom_apply : ∀ {M : Type u_5} {A : Type u_7} {B : Type u_8} [inst : Monoid M] [inst_1 : Monoid A] [inst_2 : MulDistribMulAction M A]
  [inst_3 : MulOneClass B] (c : Mᵈᵐᵃ) (f : A →* B) (a : A), (c • f) a = f (DomMulAct.mk.symm c • a)
-- Mathlib.Analysis.LocallyConvex.Bounded
NormedSpace.isBounded_iff_subset_smul_closedBall : ∀ (𝕜 : Type u_1) {E : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {s : Set E}, Bornology.IsBounded s ↔ ∃ a, s ⊆ a • Metric.closedBall 0 1
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
MeasurableSet.union : ∀ {α : Type u_1} {m : MeasurableSpace α} {s₁ s₂ : Set α}, MeasurableSet s₁ → MeasurableSet s₂ → MeasurableSet (s₁ ∪ s₂)
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.ext : ∀ {p : ENNReal} {ι : Type u_1} {α : ι → Type u_2} {x y : PiLp p α}, (∀ (i : ι), x.ofLp i = y.ofLp i) → x = y
-- Mathlib.Algebra.Order.Interval.Set.Instances
Set.Ico.instSemigroup : {R : Type u_1} → [inst : Semiring R] → [inst_1 : PartialOrder R] → [IsOrderedRing R] → Semigroup ↑(Set.Ico 0 1)
-- Init.Data.String.Basic
String.Slice.str_sliceTo : ∀ {s : String.Slice} {pos : s.Pos}, (s.sliceTo pos).str = s.str
-- Mathlib.Computability.AkraBazzi.GrowsPolynomially
AkraBazziRecurrence.GrowsPolynomially.of_isTheta : ∀ {f g : ℝ → ℝ},
  AkraBazziRecurrence.GrowsPolynomially g →
    f =Θ[Filter.atTop] g → (∀ᶠ (x : ℝ) in Filter.atTop, 0 ≤ f x) → AkraBazziRecurrence.GrowsPolynomially f
-- Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy
/-- Left homotopies in a full subcategory identify to left homotopies in the
ambient category.  -/
HomotopicalAlgebra.Precylinder.LeftHomotopy.fullSubcategoryEquiv : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {P : CategoryTheory.ObjectProperty C} →
      {X Y : P.FullSubcategory} →
        {Q : HomotopicalAlgebra.Precylinder X} →
          {f g : X ⟶ Y} → Q.LeftHomotopy f g ≃ (Q.map P.ι).LeftHomotopy f.hom g.hom
-- Lean.Elab.MutualInductive
Lean.Elab.Command.ComputedFieldView.mk : Lean.Syntax →
  Lean.Syntax → Lean.Name → Lean.Term → Lean.TSyntax `Lean.Parser.Term.matchAlts → Lean.Elab.Command.ComputedFieldView
-- Mathlib.Algebra.Group.Indicator
Set.indicator_compl : ∀ {α : Type u_1} {G : Type u_6} [inst : AddGroup G] (s : Set α) (f : α → G), sᶜ.indicator f = f - s.indicator f
-- Mathlib.CategoryTheory.Monoidal.Category
/-- The right unitor as a natural isomorphism.  -/
CategoryTheory.MonoidalCategory.rightUnitorNatIso : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      CategoryTheory.MonoidalCategory.tensorUnitRight C ≅ CategoryTheory.Functor.id C
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.ext_ring_iff : ∀ {R₁ : Type u_1} [inst : Semiring R₁] {M₁ : Type u_4} [inst_1 : TopologicalSpace M₁] [inst_2 : AddCommMonoid M₁]
  [inst_3 : Module R₁ M₁] [inst_4 : TopologicalSpace R₁] {f g : R₁ →L[R₁] M₁}, f = g ↔ f 1 = g 1
-- Init.Omega.Int
Lean.Omega.Int.lt_of_not_ge : ∀ {x y : ℤ}, ¬x ≤ y → y < x
-- Mathlib.Data.Int.GCD
_private.Mathlib.Data.Int.GCD.0.Nat.P.eq_1 : ∀ (x y r : ℕ) (s t : ℤ), Nat.P✝ x y (r, s, t) = (↑r = ↑x * s + ↑y * t)
-- Mathlib.RingTheory.ClassGroup.Basic
/-- If the class group is trivial, any unit fractional ideal is principal.  -/
ClassGroup.isPrincipal_coeSubmodule_of_isUnit : ∀ {R : Type u_1} {K : Type u_2} [inst : CommRing R] [inst_1 : Field K] [inst_2 : Algebra R K] [IsFractionRing R K]
  [inst_4 : IsDomain R] [Subsingleton (ClassGroup R)] (I : FractionalIdeal (nonZeroDivisors R) K),
  IsUnit I → (↑I).IsPrincipal
-- Init.Data.String.Modify
/-- The position just after the position that was modified in a `Pos.modify` call.  -/
String.Pos.pastModify : {s : String} → (p : s.Pos) → (f : Char → Char) → (hp : p ≠ s.endPos) → (p.modify f hp).Pos
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
CategoryTheory.Abelian.SpectralObject.kernelSequenceOpcycles_X₃ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k)
  (h : CategoryTheory.CategoryStruct.comp f g = fg) (n : ℤ),
  (X.kernelSequenceOpcycles f g fg h n).X₃ = (X.H n).obj (CategoryTheory.ComposableArrows.mk₁ g)