mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Grassmannian
Module.Grassmannian.baseChangeMkQ.congr_simp : ∀ {R : Type u} [inst : CommRing R] {M : Type v} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {A : Type w}
  [inst_3 : CommRing A] [inst_4 : Algebra R A] (B : Type w) [inst_5 : CommRing B] [inst_6 : Algebra R B]
  [inst_7 : Algebra A B] [inst_8 : IsScalarTower R A B] (N : Submodule A (TensorProduct R A M)),
  Module.Grassmannian.baseChangeMkQ B N = Module.Grassmannian.baseChangeMkQ B N
-- Mathlib.Topology.MetricSpace.Basic
/-- Build new pseudoemetric space from an old one where the edistance is provably (but typically
non-definitionally) equal to some given edistance. We also provide convenience versions for
PseudoMetric, Emetric and Metric spaces.  -/
PseudoEMetricSpace.replaceEDist : {X : Type u_2} → (m : PseudoEMetricSpace X) → (d : X → X → ENNReal) → d = edist → PseudoEMetricSpace X
-- Mathlib.NumberTheory.LucasLehmer
/-- We define `α = √3`.  -/
LucasLehmer.X.α : {q : ℕ} → LucasLehmer.X q
-- Init.Data.Array.Sort.Lemmas
Subarray.mergeSort_eq_mergeSort_toArray : ∀ {α : Type u_1} {xs : Subarray α} {le : α → α → Bool}, xs.mergeSort le = (Std.Slice.toArray xs).mergeSort le
-- Mathlib.Order.Filter.IndicatorFunction
Filter.EventuallyEq.indicator_zero : ∀ {α : Type u_1} {β : Type u_2} [inst : Zero β] {l : Filter α} {f : α → β} {s : Set α},
  f =ᶠ[l] 0 → s.indicator f =ᶠ[l] 0
-- Init.Data.Function
Function.Injective.eq_iff' : ∀ {α : Sort u_1} {β : Sort u_2} {f : α → β}, Function.Injective f → ∀ {a b : α} {c : β}, f b = c → (f a = c ↔ a = b)
-- Mathlib.Data.FunLike.Basic
DFunLike.exists_ne : ∀ {F : Sort u_1} {α : Sort u_2} {β : α → Sort u_3} [i : DFunLike F α β] {f g : F}, f ≠ g → ∃ x, f x ≠ g x
-- Mathlib.Algebra.Group.Hom.Defs
/-- Given an AddMonoid homomorphism `f : M →+ N` and an element `x : M`, if `x` has
a left inverse, then `f x` has a left inverse too. For elements invertible on both sides see
`IsAddUnit.map`.  -/
AddMonoidHom.map_exists_left_neg : ∀ {M : Type u_4} {N : Type u_5} {F : Type u_9} [inst : AddZero M] [inst_1 : AddZero N] [inst_2 : FunLike F M N]
  [AddMonoidHomClass F M N] (f : F) {x : M}, (∃ y, y + x = 0) → ∃ y, y + f x = 0
-- Mathlib.Topology.Semicontinuity.Basic
/-- The sum of two lower semicontinuous functions is lower semicontinuous. Formulated with an
explicit continuity assumption on addition, for application to `EReal`. The unprimed version of
the lemma uses `[ContinuousAdd]`.  -/
LowerSemicontinuousOn.add' : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} {γ : Type u_5} [inst_1 : AddCommMonoid γ]
  [inst_2 : LinearOrder γ] [IsOrderedAddMonoid γ] [inst_4 : TopologicalSpace γ] [OrderTopology γ] {f g : α → γ},
  LowerSemicontinuousOn f s →
    LowerSemicontinuousOn g s →
      (∀ x ∈ s, ContinuousAt (fun p => p.1 + p.2) (f x, g x)) → LowerSemicontinuousOn (fun z => f z + g z) s
-- Mathlib.Algebra.NeZero
ne_zero_of_eq_one : ∀ {α : Type u_2} [inst : Zero α] [inst_1 : One α] [NeZero 1] {a : α}, a = 1 → a ≠ 0
-- Mathlib.Data.ZMod.Basic
ZMod.val_coe_unit_coprime : ∀ {n : ℕ} (u : (ZMod n)ˣ), (↑u).val.Coprime n
-- Mathlib.MeasureTheory.VectorMeasure.Integral
MeasureTheory.VectorMeasure.continuousOn_of_dominated : ∀ {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G]
  [inst_5 : NormedSpace ℝ G] {μ : MeasureTheory.VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G} {Y : Type u_8}
  [inst_6 : TopologicalSpace Y] [FirstCountableTopology Y] {F_1 : Y → X → E} {bound : X → ℝ} {s : Set Y},
  (∀ x ∈ s, MeasureTheory.AEStronglyMeasurable (F_1 x) μ.variation) →
    (∀ x ∈ s, ∀ᵐ (a : X) ∂μ.variation, ‖F_1 x a‖ ≤ bound a) →
      MeasureTheory.Integrable bound μ.variation →
        (∀ᵐ (a : X) ∂μ.variation, ContinuousOn (fun x => F_1 x a) s) →
          ContinuousOn (fun x => ∫ᵛ (a : X), F_1 x a ∂[B; μ]) s
-- Mathlib.RingTheory.HahnSeries.Addition
HahnSeries.order_lt_order_of_eq_add_single : ∀ {R : Type u_8} {Γ : Type u_9} [inst : LinearOrder Γ] [inst_1 : Zero Γ] [inst_2 : AddCancelCommMonoid R]
  {x y : HahnSeries Γ R}, x = y + (HahnSeries.single x.order) x.leadingCoeff → y ≠ 0 → x.order < y.order
-- Mathlib.Topology.TietzeExtension
TietzeExtension.exists_restrict_eq' : ∀ {Y : Type v} {inst : TopologicalSpace Y} [self : TietzeExtension Y] {X : Type u} [inst_1 : TopologicalSpace X]
  [NormalSpace X] (s : Set X), IsClosed s → ∀ (f : C(↑s, Y)), ∃ g, ContinuousMap.restrict s g = f
-- Init.Data.Int.Linear
Int.Internal.Linear.Expr.denote_norm : ∀ (ctx : Int.Internal.Linear.Context) (e : Int.Internal.Linear.Expr),
  Int.Internal.Linear.Poly.denote ctx e.norm = Int.Internal.Linear.Expr.denote ctx e
-- Lean.Meta.Tactic.Util
Lean.Meta.TacticResultCNM.modified.inj : ∀ {mvarId mvarId_1 : Lean.MVarId},
  Lean.Meta.TacticResultCNM.modified mvarId = Lean.Meta.TacticResultCNM.modified mvarId_1 → mvarId = mvarId_1
-- Mathlib.Logic.Equiv.Option
Equiv.optionSubtypeNe_symm_of_ne : ∀ {α : Type u_1} [inst : DecidableEq α] {a b : α} (hba : b ≠ a), (Equiv.optionSubtypeNe a).symm b = some ⟨b, hba⟩
-- Init.Omega.Constraint
/-- Shorthand for the second component of `tidy`.  -/
Lean.Omega.tidyCoeffs : Lean.Omega.Constraint → Lean.Omega.Coeffs → Lean.Omega.Coeffs
-- Mathlib.Probability.Moments.CovarianceBilin
ProbabilityTheory.covarianceBilin_apply_basisFun : ∀ {ι : Type u_2} {Ω : Type u_3} [inst : Fintype ι] {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsFiniteMeasure μ] {X : ι → Ω → ℝ},
  (∀ (i : ι), MeasureTheory.MemLp (X i) 2 μ) →
    ∀ (i j : ι),
      ((ProbabilityTheory.covarianceBilin (MeasureTheory.Measure.map (fun ω => WithLp.toLp 2 fun x => X x ω) μ))
            ((EuclideanSpace.basisFun ι ℝ) i))
          ((EuclideanSpace.basisFun ι ℝ) j) =
        ProbabilityTheory.covariance (X i) (X j) μ
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.AddModObj.instTensorAddUnit.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D]
  (X : D),
  CategoryTheory.AddModObj.instTensorAddUnit X =
    { vadd := (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso X).hom, zero_vadd := ⋯,
      add_vadd := ⋯ }
-- Lean.Parser.Extra
Lean.Parser.ppGroup.parenthesizer : Lean.PrettyPrinter.Parenthesizer → Lean.PrettyPrinter.Parenthesizer
-- Qq.Macro
Qq.Impl.MVarSynth.type.sizeOf_spec : ∀ (unquotedMVar : Lean.MVarId), sizeOf (Qq.Impl.MVarSynth.type unquotedMVar) = 1 + sizeOf unquotedMVar
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CallHierarchyIncomingCall.fromRanges : Lean.Lsp.CallHierarchyIncomingCall → Array Lean.Lsp.Range
-- Mathlib.Algebra.QuadraticAlgebra.Defs
QuadraticAlgebra.C_eq_algebraMap : ∀ {R : Type u_1} {a b : R} [inst : CommSemiring R], QuadraticAlgebra.C = ⇑(algebraMap R (QuadraticAlgebra R a b))
-- Mathlib.Data.Finset.Max
/-- Given a nonempty finset `s` in a linear order `α`, then `s.max' H` is its maximum, as an
element of `α`, where `H` is a proof of nonemptiness. Without this assumption, use instead `s.max`,
taking values in `WithBot α`.  -/
Finset.max' : {α : Type u_2} → [LinearOrder α] → (s : Finset α) → s.Nonempty → α
-- Mathlib.Order.Grade
Flag.instGradeMinOrderSubtypeMem : {𝕆 : Type u_1} →
  {α : Type u_3} →
    [inst : PartialOrder α] → [inst_1 : Preorder 𝕆] → [GradeMinOrder 𝕆 α] → (s : Flag α) → GradeMinOrder 𝕆 ↥s
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.mem_single : ∀ {ι : Type u_1} {I J J' : BoxIntegral.Box ι} (h : J ≤ I), J' ∈ BoxIntegral.Prepartition.single I J h ↔ J' = J
-- Lean.Elab.Binders
/-- Given syntax of the form `(ident >> " : ")?`, return `ident`, or a new instance name.  -/
_private.Lean.Elab.Binders.0.Lean.Elab.Term.expandOptIdent : Lean.Syntax → Lean.Elab.TermElabM Lean.Syntax
-- Mathlib.Algebra.Quaternion
Quaternion.normSq_natCast : ∀ {R : Type u_3} [inst : CommRing R] (n : ℕ), Quaternion.normSq ↑n = ↑n ^ 2
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.coe_refl : ∀ {R : Type uR} {A₁ : Type uA₁} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Algebra R A₁],
  ⇑AlgEquiv.refl = id
-- Mathlib.RingTheory.MvPowerSeries.Restricted
MvPowerSeries.isRestricted.mul : ∀ {R : Type u_1} [inst : NormedRing R] {σ : Type u_2} [IsUltrametricDist R] (c : σ → ℝ) {f g : MvPowerSeries σ R},
  MvPowerSeries.IsRestricted c f → MvPowerSeries.IsRestricted c g → MvPowerSeries.IsRestricted c (f * g)
-- Init.Data.Array.Basic
_private.Init.Data.Array.Basic.0.Array.firstM.go : {β : Type v} → {α : Type u} → {m : Type v → Type w} → [Alternative m] → (α → m β) → Array α → ℕ → m β
-- Mathlib.Algebra.Homology.AlternatingConst
/-- Let `c : ComplexShape ℕ` be such that `i j : ℕ` have opposite parity if they are related by
`c`. Let `φ, ψ : A ⟶ A` be such that `φ ∘ ψ = ψ ∘ φ = 0`. This is a complex of shape `c` whose
objects are all `A`. For all `i, j` related by `c`, `dᵢⱼ = φ` when `i` is even, and `dᵢⱼ = ψ` when
`i` is odd.  -/
HomologicalComplex.alternatingConst : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      (A : C) →
        {φ ψ : A ⟶ A} →
          CategoryTheory.CategoryStruct.comp φ ψ = 0 →
            CategoryTheory.CategoryStruct.comp ψ φ = 0 →
              {c : ComplexShape ℕ} →
                [DecidableRel c.Rel] → (∀ (i j : ℕ), c.Rel i j → Odd (i + j)) → HomologicalComplex C c
-- Mathlib.RingTheory.PolynomialLaw.Basic
/-- The extension of `PolynomialLaw.toFun'` to all universes.  -/
PolynomialLaw.toFun : {R : Type u} →
  [inst : CommSemiring R] →
    {M : Type u_1} →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] →
          {N : Type u_2} →
            [inst_3 : AddCommMonoid N] →
              [inst_4 : Module R N] →
                (S : Type v) →
                  [inst_5 : CommSemiring S] →
                    [inst_6 : Algebra R S] → (M →ₚₗ[R] N) → TensorProduct R S M → TensorProduct R S N
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.completeGraph_eq_top : ∀ (V : Type u), SimpleGraph.completeGraph V = ⊤
-- Mathlib.Topology.Algebra.Nonarchimedean.Bases
RingSubgroupsBasis.nonarchimedean : ∀ {A : Type u_1} {ι : Type u_2} [inst : Ring A] [inst_1 : Nonempty ι] {B : ι → AddSubgroup A}
  (hB : RingSubgroupsBasis B), NonarchimedeanRing A
-- Mathlib.RingTheory.MvPowerSeries.Basic
/-- Vanishing of coefficients of powers of multivariate power series
when the constant coefficient is nilpotent
[N. Bourbaki, *Algebra II*, Chapter 4, §4, n°2, proposition 3][bourbaki1981]  -/
MvPowerSeries.coeff_eq_zero_of_constantCoeff_nilpotent : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommSemiring R] {f : MvPowerSeries σ R} {m : ℕ},
  MvPowerSeries.constantCoeff f ^ m = 0 →
    ∀ {d : σ →₀ ℕ} {n : ℕ}, m + Finsupp.degree d ≤ n → (MvPowerSeries.coeff d) (f ^ n) = 0
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
ContinuousAlternatingMap.instAdd : {R : Type u_1} →
  {M : Type u_2} →
    {N : Type u_4} →
      {ι : Type u_6} →
        [inst : Semiring R] →
          [inst_1 : AddCommMonoid M] →
            [inst_2 : Module R M] →
              [inst_3 : TopologicalSpace M] →
                [inst_4 : AddCommMonoid N] →
                  [inst_5 : Module R N] → [inst_6 : TopologicalSpace N] → [ContinuousAdd N] → Add (M [⋀^ι]→L[R] N)
-- Mathlib.NumberTheory.RamificationInertia.Galois
Ideal.inertiaDegIn.eq_1 : ∀ {A : Type u_1} [inst : CommRing A] (p : Ideal A) (B : Type u_2) [inst_1 : CommRing B] [inst_2 : Algebra A B],
  p.inertiaDegIn B = if h : ∃ P, P.IsPrime ∧ P.LiesOver p then h.choose.inertiaDeg A else 0
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
CFC.abs_smul_nonneg : ∀ {A : Type u_2} [inst : NonUnitalRing A] [inst_1 : StarRing A] [inst_2 : TopologicalSpace A] [inst_3 : Module ℝ A]
  [inst_4 : SMulCommClass ℝ A A] [inst_5 : IsScalarTower ℝ A A]
  [inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_7 : PartialOrder A]
  [inst_8 : StarOrderedRing A] [inst_9 : NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] [StarModule ℝ A]
  {R : Type u_3} [inst_13 : Semiring R] [inst_14 : SMulWithZero R NNReal] [inst_15 : SMul R A]
  [IsScalarTower R NNReal A] (r : R) (a : A), CFC.abs (r • a) = r • CFC.abs a
-- Mathlib.Combinatorics.Quiver.Symmetric
/-- A type synonym for the symmetrized quiver (with an arrow both ways for each original arrow).
 -/
Quiver.Symmetrify : Type u_1 → Type u_1
-- Init.Data.Iterators.Consumers.Monadic.Loop
/-- This is the loop implementation of the default instance `IteratorLoop.defaultImplementation`.
 -/
Std.IterM.DefaultConsumers.forIn' : {m : Type w → Type w'} →
  {α β : Type w} →
    [inst : Std.Iterator α m β] →
      {n : Type x → Type x'} →
        [Monad n] →
          ((γ : Type w) → (δ : Type x) → (γ → n δ) → m γ → n δ) →
            (γ : Type x) →
              (PlausibleForInStep : β → γ → ForInStep γ → Prop) →
                (it : Std.IterM m β) →
                  γ →
                    (P : β → Prop) →
                      (∀ (b : β), it.IsPlausibleIndirectOutput b → P b) →
                        ((b : β) → P b → (c : γ) → n (Subtype (PlausibleForInStep b c))) → n γ
-- Mathlib.Analysis.Convex.Star
StarConvex.union : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : SMul 𝕜 E] {x : E} {s t : Set E}, StarConvex 𝕜 x s → StarConvex 𝕜 x t → StarConvex 𝕜 x (s ∪ t)
-- Mathlib.Algebra.AffineMonoid.Basic
IsAffineAddMonoid.toIsCancelAdd : ∀ {M : Type u_1} {inst : AddCommMonoid M} [self : IsAffineAddMonoid M], IsCancelAdd M
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.IsAffineOpen.basicOpen : ∀ {X : AlgebraicGeometry.Scheme} {U : X.Opens},
  AlgebraicGeometry.IsAffineOpen U →
    ∀ (f : ↑(X.presheaf.obj (Opposite.op U))), AlgebraicGeometry.IsAffineOpen (X.basicOpen f)
-- Mathlib.SetTheory.Ordinal.Notation
_private.Mathlib.SetTheory.Ordinal.Notation.0.ONote.FundamentalSequenceProp.match_1.splitter : (motive : Option ONote ⊕ (ℕ → ONote) → Sort u_1) →
  (x : Option ONote ⊕ (ℕ → ONote)) →
    (Unit → motive (Sum.inl none)) →
      ((a : ONote) → motive (Sum.inl (some a))) → ((f : ℕ → ONote) → motive (Sum.inr f)) → motive x
-- Mathlib.Topology.MetricSpace.Isometry
IsometryEquiv.completeSpace : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] [CompleteSpace β]
  (e : α ≃ᵢ β), CompleteSpace α
-- Mathlib.Algebra.Lie.Weights.Chain
LieModule.chainTopCoeff.congr_simp : ∀ {R : Type u_1} {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {M : Type u_3}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L] [inst_8 : IsAddTorsionFree R] [inst_9 : IsDomain R]
  [inst_10 : Module.IsTorsionFree R M] [inst_11 : IsNoetherian R M] (α α_1 : L → R),
  α = α_1 → ∀ (β β_1 : LieModule.Weight R L M), β = β_1 → LieModule.chainTopCoeff α β = LieModule.chainTopCoeff α_1 β_1
-- Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.functorObjObj_mon_mul : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.MonoidalCategory D] (A : CategoryTheory.Functor C D) [inst_3 : CategoryTheory.MonObj A]
  (X : C), CategoryTheory.MonObj.mul = CategoryTheory.MonObj.mul.app X
-- Mathlib.CategoryTheory.Sites.Subsheaf
CategoryTheory.instMonoSheafTypeImageι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  {F F' : CategoryTheory.Sheaf J (Type w)} (f : F ⟶ F'), CategoryTheory.Mono (CategoryTheory.Sheaf.imageι f)
-- Mathlib.CategoryTheory.Sites.Point.Over
CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.over : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C] {P : CategoryTheory.ObjectProperty J.Point}
  [CategoryTheory.ObjectProperty.Small.{w, max u w, max (max u v) (w + 1)} P] [J.WEqualsLocallyBijective (Type w)]
  [CategoryTheory.HasSheafify J (Type w)],
  P.IsConservativeFamilyOfPoints →
    ∀ (X : C) [CategoryTheory.HasSheafify (J.over X) (Type w)],
      (CategoryTheory.ObjectProperty.ofObj fun ψ => ψ.fst.obj.over ψ.snd).IsConservativeFamilyOfPoints
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.isSome_getElem?_toList_roo_eq : ∀ {m n i : ℕ}, ((m<...n).toList[i]?.isSome = true) = (i < n - (m + 1))
-- Mathlib.Combinatorics.Matroid.Basic
/-- `I` is independent if all its finite subsets are independent.  -/
Matroid.Finitary.indep_of_forall_finite : ∀ {α : Type u_1} {M : Matroid α} [self : M.Finitary] (I : Set α), (∀ J ⊆ I, J.Finite → M.Indep J) → M.Indep I
-- Mathlib.GroupTheory.PGroup
isPGroup_one_iff_subsingleton : ∀ {G : Type u_1} [inst : Group G], IsPGroup 1 G ↔ Subsingleton G
-- Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
HomotopicalAlgebra.FibrantObject.congr_simp : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithFibrations C]
  [inst_2 : CategoryTheory.Limits.HasTerminal C],
  HomotopicalAlgebra.FibrantObject C = HomotopicalAlgebra.FibrantObject C
-- Mathlib.CategoryTheory.Monoidal.CommMon_
/-- The trivial commutative monoid object. We later show this is initial in `CommMon C`.
 -/
CategoryTheory.CommMon.trivial : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] → CategoryTheory.CommMon C
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
/-- For `a : integerSet K`, the unique nonzero algebraic integer `x` such that its image by
`mixedEmbedding` is equal to `a`. Note that we state the fact that `x ≠ 0` by saying that `x` is
a nonzero divisors since we will use later on the isomorphism
`Ideal.associatesNonZeroDivisorsEquivIsPrincipal`, see `integerSetEquiv`.  -/
NumberField.mixedEmbedding.fundamentalCone.preimageOfMemIntegerSet : {K : Type u_1} →
  [inst : Field K] →
    [inst_1 : NumberField K] →
      ↑(NumberField.mixedEmbedding.fundamentalCone.integerSet K) → ↥(nonZeroDivisors (NumberField.RingOfIntegers K))
-- Init.Data.ByteArray.Basic
/-- The size of an array iterator is the number of bytes remaining.  -/
ByteArray.instSizeOfIterator : SizeOf ByteArray.Iterator
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.bsup_eq_blsub_of_lt_succ_limit : ∀ {o : Ordinal.{u}} (ho : Order.IsSuccLimit o) {f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}},
  (∀ (a : Ordinal.{u}) (ha : a < o), f a ha < f (Order.succ a) ⋯) → o.bsup f = o.blsub f
-- Mathlib.Analysis.RCLike.Basic
RCLike.normSq_neg : ∀ {K : Type u_1} [inst : RCLike K] (z : K), RCLike.normSq (-z) = RCLike.normSq z
-- Lean.Server.CodeActions.Basic
Lean.Server.instFromJsonCodeActionResolveData.fromJson : Lean.Json → Except String Lean.Server.CodeActionResolveData
-- Mathlib.CategoryTheory.Sites.Point.Basic
CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_map_bijective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point)
  {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A]
  [inst_2 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] {FC : A → A → Type u_1} {CC : A → Type w'}
  [inst_3 : (X Y : A) → FunLike (FC X Y) (CC X) (CC Y)] [inst_4 : CategoryTheory.ConcreteCategory A FC]
  {P Q : CategoryTheory.Functor Cᵒᵖ A}
  [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', w', u', w' + 1} (CategoryTheory.forget A)]
  [CategoryTheory.LocallySmall.{w, v, u} C] (f : P ⟶ Q) [CategoryTheory.Presheaf.IsLocallyInjective J f]
  [CategoryTheory.Presheaf.IsLocallySurjective J f],
  Function.Bijective ⇑(CategoryTheory.ConcreteCategory.hom (Φ.presheafFiber.map f))
-- Mathlib.Algebra.Homology.HomotopyCategory.ShortExact
CochainComplex.mappingCone.inr_descShortComplex : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex (CochainComplex C ℤ)),
  CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.inr S.f)
      (CochainComplex.mappingCone.descShortComplex S) =
    S.g
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.eLpNorm_map_measure : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} {ε : Type u_7}
  [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε] {β : Type u_8} {mβ : MeasurableSpace β} {f : α → β}
  {g : β → ε},
  MeasureTheory.AEStronglyMeasurable g (MeasureTheory.Measure.map f μ) →
    AEMeasurable f μ → MeasureTheory.eLpNorm g p (MeasureTheory.Measure.map f μ) = MeasureTheory.eLpNorm (g ∘ f) p μ
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
CochainComplex.mappingCocone.descCochain.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} (φ : K ⟶ L) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] {M : CochainComplex C ℤ}
  {n m : ℤ} (α : CochainComplex.HomComplex.Cochain K M m) (β : CochainComplex.HomComplex.Cochain L M n) (h : m + 1 = n),
  CochainComplex.mappingCocone.descCochain φ α β h =
    (-m + 1).negOnePow • (CochainComplex.mappingCone.descCochain φ α β h).leftShift (-1) m ⋯
-- Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
SimpleGraph.Walk.support_getElem_length_sub_one_eq_penultimate : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v}, p.support[p.length - 1] = p.penultimate
-- Mathlib.RingTheory.DedekindDomain.GaussLemma
/-- In case `R` is PID, given a polynomial `p` in `R[X]`, `p` is primitive if and only if the
`v`-adic Gauss norms of `p` are equal to 1 for all `v`.  -/
Polynomial.isPrimitive_iff_forall_gaussNorm_eq_one : ∀ {R : Type u_2} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsPrincipalIdealRing R],
  ¬IsField R →
    ∀ {b : NNReal} (hb : 1 < b) (p : Polynomial R),
      p.IsPrimitive ↔ ∀ (v : IsDedekindDomain.HeightOneSpectrum R), Polynomial.gaussNorm (v.intAdicAbv hb) 1 p = 1
-- Mathlib.NumberTheory.EulerProduct.Basic
/-- The *Euler Product* for a multiplicative arithmetic function `f` with values in a
complete normed commutative ring `R`: if `‖f ·‖` is summable, then
`∏' p : Nat.Primes, ∑' e, f (p ^ e) = ∑' n, f n`.
This version is stated in terms of `HasProd`.  -/
ArithmeticFunction.IsMultiplicative.eulerProduct_hasProd : ∀ {R : Type u_1} [inst : NormedCommRing R] [CompleteSpace R] {f : ArithmeticFunction R},
  f.IsMultiplicative → (Summable fun x => ‖f x‖) → HasProd (fun p => ∑' (e : ℕ), f (↑p ^ e)) (∑' (n : ℕ), f n)
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
Lean.Meta.RefinedDiscrTree.Key.const.sizeOf_spec : ∀ (declName : Lean.Name) (nargs : ℕ),
  sizeOf (Lean.Meta.RefinedDiscrTree.Key.const declName nargs) = 1 + sizeOf declName + sizeOf nargs
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.neg_subset_sub_right : ∀ {α : Type u_2} [inst : SubtractionMonoid α] {s t : Set α}, 0 ∈ s → -t ⊆ s - t
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.ι_colimitIsoOfIsLeftKanExtension_inv_assoc : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  (F' : CategoryTheory.Functor D H) {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H}
  (α : F ⟶ L.comp F') [inst_3 : F'.IsLeftKanExtension α] [inst_4 : CategoryTheory.Limits.HasColimit F]
  [inst_5 : CategoryTheory.Limits.HasColimit F'] (i : C) {Z : H} (h : CategoryTheory.Limits.colimit F' ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι F i)
      (CategoryTheory.CategoryStruct.comp (F'.colimitIsoOfIsLeftKanExtension α).inv h) =
    CategoryTheory.CategoryStruct.comp (α.app i)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι F' (L.obj i)) h)