mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting
/-- The projective system `sqFunctor c p f g` has a `WellOrderInductionData` structure.  -/
CategoryTheory.HasLiftingProperty.transfiniteComposition.wellOrderInductionData : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type w} →
      [inst_1 : LinearOrder J] →
        [inst_2 : OrderBot J] →
          {F : CategoryTheory.Functor J C} →
            (c : CategoryTheory.Limits.Cocone F) →
              {X Y : C} →
                {p : X ⟶ Y} →
                  (f : F.obj ⊥ ⟶ X) →
                    (g : c.pt ⟶ Y) →
                      [F.IsWellOrderContinuous] →
                        [inst_4 : SuccOrder J] →
                          (∀ (j : J),
                              ¬IsMax j →
                                CategoryTheory.HasLiftingPropertyFixedBot (F.map (CategoryTheory.homOfLE ⋯)) p
                                  (CategoryTheory.CategoryStruct.comp (c.ι.app (Order.succ j)) g)) →
                            (CategoryTheory.HasLiftingProperty.transfiniteComposition.sqFunctor c p f
                                g).WellOrderInductionData
-- Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Module.Basis.card_le_card_of_le : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {ι : Type w}
  {ι' : Type w'} [StrongRankCondition R] {N O : Submodule R M},
  N ≤ O →
    ∀ [inst_4 : Fintype ι] (b : Module.Basis ι R ↥O) [inst_5 : Fintype ι'] (b' : Module.Basis ι' R ↥N),
      Fintype.card ι' ≤ Fintype.card ι
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
/-- Given a connected component `C` of a simple graph `G`, produce the induced graph on `C`.
The declaration `connected_toSimpleGraph` shows it is connected, and `toSimpleGraph_hom`
provides the homomorphism back to `G`.
 -/
SimpleGraph.ConnectedComponent.toSimpleGraph : {V : Type u} → {G : SimpleGraph V} → (C : G.ConnectedComponent) → SimpleGraph ↥C
-- Mathlib.Algebra.Category.Ring.Colimits
/-- The cocone over the proposed colimit ring.  -/
RingCat.Colimits.colimitCocone : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] → (F : CategoryTheory.Functor J RingCat) → CategoryTheory.Limits.Cocone F
-- Lean.Widget.Types
Lean.Widget.WidgetInstance.mk.injEq : ∀ (id : Lean.Name) (javascriptHash : UInt64) (props : StateM Lean.Server.RpcObjectStore Lean.Json) (id_1 : Lean.Name)
  (javascriptHash_1 : UInt64) (props_1 : StateM Lean.Server.RpcObjectStore Lean.Json),
  ({ id := id, javascriptHash := javascriptHash, props := props } =
      { id := id_1, javascriptHash := javascriptHash_1, props := props_1 }) =
    (id = id_1 ∧ javascriptHash = javascriptHash_1 ∧ props = props_1)
-- Mathlib.Geometry.Euclidean.PerpBisector
AffineSubspace.mem_perpBisector_iff_dist_eq : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {c p₁ p₂ : P}, c ∈ AffineSubspace.perpBisector p₁ p₂ ↔ dist c p₁ = dist c p₂
-- Mathlib.GroupTheory.FreeGroup.Reduce
FreeGroup.reduce.Step.eq : ∀ {α : Type u_1} {L₁ L₂ : List (α × Bool)} [inst : DecidableEq α],
  FreeGroup.Red.Step L₁ L₂ → FreeGroup.reduce L₁ = FreeGroup.reduce L₂
-- Mathlib.RingTheory.Congruence.Basic
RingCon.le_comap_ringConGen : ∀ {R : Type u_3} {R' : Type u_4} [inst : Add R] [inst_1 : Mul R] [inst_2 : Add R'] [inst_3 : Mul R'] {F : Type u_5}
  [inst_4 : FunLike F R' R] [inst_5 : MulHomClass F R' R] [inst_6 : AddHomClass F R' R] (r : R → R → Prop) (f : F),
  ringConGen (Function.onFun r ⇑f) ≤ (ringConGen r).comap f
-- Init.Data.UInt.Lemmas
UInt8.mul_assoc : ∀ (a b c : UInt8), a * b * c = a * (b * c)
-- Mathlib.RingTheory.Perfection
/-- A perfection map induces an isomorphism to the perfection.  -/
PerfectionMap.equiv : {p : ℕ} →
  [inst : Fact (Nat.Prime p)] →
    {R : Type u₁} →
      [inst_1 : CommSemiring R] →
        [inst_2 : CharP R p] →
          {P : Type u₃} →
            [inst_3 : CommSemiring P] →
              [inst_4 : CharP P p] →
                [inst_5 : PerfectRing P p] → {π : P →+* R} → PerfectionMap p π → P ≃+* Perfection R p
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.Λ'.ret.sizeOf_spec : ∀ (k : Turing.PartrecToTM2.Cont'), sizeOf (Turing.PartrecToTM2.Λ'.ret k) = 1 + sizeOf k
-- Lean.Elab.Match
/-- ```
leading_parser "match " >> optional generalizingParam >> optional motive >> sepBy1 matchDiscr ", " >> " with " >> ppDedent matchAlts
```
Remark the `optIdent` must be `none` at `matchDiscr`. They are expanded by `expandMatchDiscr?`.
 -/
_private.Lean.Elab.Match.0.Lean.Elab.Term.elabMatchCore : Lean.Syntax → Option Lean.Expr → Lean.Elab.TermElabM Lean.Expr
-- Mathlib.RingTheory.Polynomial.ScaleRoots
Polynomial.rootMultiplicity_scaleRoots : ∀ {R : Type u_1} [inst : CommRing R] (p : Polynomial R) {r a : R},
  IsLeftRegular r → Polynomial.rootMultiplicity (r * a) (p.scaleRoots r) = Polynomial.rootMultiplicity a p
-- Lean.Meta.Tactic.Grind.Parser
Lean.Parser.Command.GrindCnstr.check : Lean.Parser.Parser
-- Mathlib.Algebra.HierarchyDesign
/-- There are places where typeclass arguments are specified with implicit `{}` brackets instead of
the usual `[]` brackets. This is done when the instances can be inferred because they are implicit
arguments to the type of one of the other arguments. There are several reasons for doing so.

When they can be inferred from these other arguments,
it is faster to use this method than to use type class inference.
For example, when writing lemmas about `(f : α →+* β)`, it is faster to specify the fact that `α`
and `β` are `Semiring`s as `{rα : Semiring α} {rβ : Semiring β}` rather than the usual
`[Semiring α] [Semiring β]`.

When handling non-canonical instances, it is necessary that the relevant declarations take these
instance arguments implicitly, otherwise Lean will refuse to apply them.
For example, in measure theory a space `X` will often come equipped with a canonical base
sigma-algebra `MeasurableSpace X` along with many sub-sigma algebras, also of type
`MeasurableSpace X`. In homological algebra, `ModuleCat ℤ` appears regularly as the category of
abelian groups, but terms `A : ModuleCat ℤ` come with two (propeq) `Module ℤ A` instances:
one from being `ℤ`-modules, and one from being abelian groups.
 -/
LibraryNote.implicit_instance_arguments : Batteries.Util.LibraryNote
-- Mathlib.LinearAlgebra.Matrix.SchurComplement
Matrix.det_one_sub_mul_comm : ∀ {m : Type u_2} {n : Type u_3} {α : Type u_4} [inst : Fintype m] [inst_1 : Fintype n] [inst_2 : DecidableEq m]
  [inst_3 : DecidableEq n] [inst_4 : CommRing α] (A : Matrix m n α) (B : Matrix n m α),
  (1 - A * B).det = (1 - B * A).det
-- Batteries.Data.List.Lemmas
List.length_findIdxs : ∀ {α : Type u_1} {xs : List α} {p : α → Bool} {s : ℕ}, (List.findIdxs p xs s).length = List.countP p xs
-- Mathlib.RingTheory.MvPowerSeries.Evaluation
MvPowerSeries.aeval_unique : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommRing R] [inst_1 : UniformSpace R] {S : Type u_3} [inst_2 : CommRing S]
  [inst_3 : UniformSpace S] [inst_4 : IsTopologicalSemiring R] [inst_5 : IsUniformAddGroup R]
  [inst_6 : IsUniformAddGroup S] [inst_7 : CompleteSpace S] [inst_8 : T2Space S] [inst_9 : IsTopologicalRing S]
  [inst_10 : IsLinearTopology S S] [inst_11 : Algebra R S] [inst_12 : ContinuousSMul R S]
  {ε : MvPowerSeries σ R →ₐ[R] S} (hε : Continuous ⇑ε), MvPowerSeries.aeval ⋯ = ε
-- Mathlib.GroupTheory.GroupAction.Defs
MulAction.mem_fixedBy : ∀ {M : Type u_1} {α : Type u_3} [inst : Monoid M] [inst_1 : MulAction M α] {m : M} {a : α},
  a ∈ MulAction.fixedBy α m ↔ m • a = a
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
/-- Multiplication.
 -/
Std.Tactic.BVDecide.BVBinOp.mul : Std.Tactic.BVDecide.BVBinOp
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.mkIso_hom_snd : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B}
  {x y : CategoryTheory.Limits.CategoricalPullback F G} (eₗ : x.fst ≅ y.fst) (eᵣ : x.snd ≅ y.snd)
  (w :
    autoParam
      (CategoryTheory.CategoryStruct.comp (F.map eₗ.hom) y.iso.hom =
        CategoryTheory.CategoryStruct.comp x.iso.hom (G.map eᵣ.hom))
      CategoryTheory.Limits.CategoricalPullback.mkIso._auto_1),
  (CategoryTheory.Limits.CategoricalPullback.mkIso eₗ eᵣ w).hom.snd = eᵣ.hom
-- Mathlib.Algebra.Opposites
MulOpposite.instInhabited.eq_1 : ∀ {α : Type u_1} [inst : Inhabited α], MulOpposite.instInhabited = { default := MulOpposite.op default }
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.minKeyD_insertIfNew_le_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α} {v : β k}
  {fallback : α}, (cmp ((t.insertIfNew k v).minKeyD fallback) k).isLE = true
-- Mathlib.Data.DFinsupp.Order
/-- The order on `DFinsupp`s over a partial order embeds into the order on functions  -/
DFinsupp.orderEmbeddingToFun : {ι : Type u_1} →
  {α : ι → Type u_2} →
    [inst : (i : ι) → Zero (α i)] → [inst_1 : (i : ι) → LE (α i)] → (Π₀ (i : ι), α i) ↪o ((i : ι) → α i)
-- Mathlib.RingTheory.Spectrum.Prime.RingHom
RingHom.strictMono_comap_of_surjective : ∀ {R : Type u} [inst : CommRing R] {S : Type u_1} [inst_1 : CommRing S] {f : R →+* S},
  Function.Surjective ⇑f → StrictMono (PrimeSpectrum.comap f)
-- Mathlib.Data.Fin.SuccPred
Fin.leftInverse_cast : ∀ {n m : ℕ} (eq : n = m), Function.LeftInverse (Fin.cast ⋯) (Fin.cast eq)
-- Mathlib.Topology.Continuous
continuous_id' : ∀ {X : Type u_1} [inst : TopologicalSpace X], Continuous fun x => x
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.normAtAllPlaces_apply : ∀ {K : Type u_1} [inst : Field K] (x : NumberField.mixedEmbedding.mixedSpace K) (w : NumberField.InfinitePlace K),
  NumberField.mixedEmbedding.normAtAllPlaces x w = (NumberField.mixedEmbedding.normAtPlace w) x
-- Mathlib.Order.Interval.Finset.Basic
Finset.Ico_subset_Ico_right : ∀ {α : Type u_2} {a b₁ b₂ : α} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α],
  b₁ ≤ b₂ → Finset.Ico a b₁ ⊆ Finset.Ico a b₂
-- Mathlib.NumberTheory.ZetaValues
bernoulliFun_eval_half : ∀ (k : ℕ), bernoulliFun k 2⁻¹ = (2 / 2 ^ k - 1) * ↑(bernoulli k)
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.leftUnitor_comp_inv : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} (f : a ⟶ b) (g : b ⟶ c),
  (CategoryTheory.Bicategory.leftUnitor (CategoryTheory.CategoryStruct.comp f g)).inv =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.leftUnitor f).inv g)
      (CategoryTheory.Bicategory.associator (CategoryTheory.CategoryStruct.id a) f g).hom
-- Mathlib.Order.Bounds.Basic
lt_isGLB_iff : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α} {a b : α}, IsGLB s a → (b < a ↔ ∃ c ∈ lowerBounds s, b < c)
-- Mathlib.AlgebraicGeometry.AffineTransitionLimit
/-- [Stacks Tag 01Z4](https://stacks.math.columbia.edu/tag/01Z4) ((2)) -/
AlgebraicGeometry.exists_map_preimage_eq_map_preimage : ∀ {I : Type u} [inst : CategoryTheory.Category.{u, u} I] (D : CategoryTheory.Functor I AlgebraicGeometry.Scheme)
  (c : CategoryTheory.Limits.Cone D) (hc : CategoryTheory.Limits.IsLimit c) [CategoryTheory.IsCofiltered I]
  [∀ {i j : I} (f : i ⟶ j), AlgebraicGeometry.IsAffineHom (D.map f)] {i : I} {U V : (D.obj i).Opens},
  IsCompact ↑U →
    IsCompact ↑V →
      (TopologicalSpace.Opens.map (c.π.app i).base).obj U = (TopologicalSpace.Opens.map (c.π.app i).base).obj V →
        ∃ j fji,
          (TopologicalSpace.Opens.map (D.map fji).base).obj U = (TopologicalSpace.Opens.map (D.map fji).base).obj V
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1.Stmt.write : {Γ : Type u_1} → {Λ : Type u_2} → {σ : Type u_3} → (Γ → σ → Γ) → Turing.TM1.Stmt Γ Λ σ → Turing.TM1.Stmt Γ Λ σ
-- Mathlib.Algebra.Polynomial.Eval.Coeff
Polynomial.hom_eval₂ : ∀ {R : Type u} {S : Type v} {T : Type w} [inst : Semiring R] (p : Polynomial R) [inst_1 : Semiring S]
  [inst_2 : Semiring T] (f : R →+* S) (g : S →+* T) (x : S),
  g (Polynomial.eval₂ f x p) = Polynomial.eval₂ (g.comp f) (g x) p
-- Init.Data.Int.Basic
/-- A natural number is an integer.

This constructor covers the non-negative integers (from `0` to `∞`).
 -/
Int.ofNat : ℕ → ℤ
-- Mathlib.Algebra.Group.Units.Basic
IsAddUnit.isAddUnit_iff_addLeft_bijective : ∀ {M : Type u_1} [inst : AddMonoid M] {a : M}, IsAddUnit a ↔ Function.Bijective fun x => a + x
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
/-- The product of two finite additive groups is cyclic
iff both of them are cyclic and their orders are coprime.  -/
AddGroup.isAddCyclic_prod_iff : ∀ {M : Type u_4} {N : Type u_5} [inst : AddGroup M] [inst_1 : AddGroup N],
  IsAddCyclic (M × N) ↔ IsAddCyclic M ∧ IsAddCyclic N ∧ (Nat.card M).Coprime (Nat.card N)
-- Mathlib.Combinatorics.Additive.Corner.Defs
/-- A **corner** of a set `A` in an abelian group is a triple of points of the form
`(x, y), (x + d, y), (x, y + d)`. It is **nontrivial** if `d ≠ 0`.

Here we define it as triples `(x₁, y₁), (x₂, y₁), (x₁, y₂)` where `x₁ + y₂ = x₂ + y₁` in order for
the definition to make sense in commutative monoids, the motivating example being `ℕ`.  -/
IsCorner : {G : Type u_1} → [AddCommMonoid G] → Set (G × G) → G → G → G → G → Prop
-- Mathlib.FieldTheory.Galois.Basic
/-- The intermediate field fixed by a subgroup.  -/
IntermediateField.fixedField : {F : Type u_1} →
  [inst : Field F] →
    {E : Type u_2} → [inst_1 : Field E] → [inst_2 : Algebra F E] → Subgroup Gal(E/F) → IntermediateField F E
-- Mathlib.RingTheory.MvPowerSeries.Expand
MvPowerSeries.expand_mul_eq_comp : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommRing R] (p : ℕ) (hp : p ≠ 0) (q : ℕ) (hq : q ≠ 0),
  MvPowerSeries.expand (p * q) ⋯ = (MvPowerSeries.expand p hp).comp (MvPowerSeries.expand q hq)
-- Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
Lean.Meta.Grind.Arith.CommRing.PolyDerivation.denoteExpr : {M : Type → Type} →
  [Monad M] →
    [Lean.MonadError M] →
      [MonadLiftT Lean.MetaM M] →
        [Lean.Meta.Sym.Arith.MonadCanon M] →
          [Lean.Meta.Grind.Arith.CommRing.MonadRing M] → Lean.Meta.Grind.Arith.CommRing.PolyDerivation → M Lean.Expr
-- Mathlib.Topology.MetricSpace.IsometricSMul
Prod.isIsometricVAdd'' : ∀ {M : Type u} {N : Type u_2} [inst : Add M] [inst_1 : PseudoEMetricSpace M] [IsIsometricVAdd Mᵃᵒᵖ M] [inst_3 : Add N]
  [inst_4 : PseudoEMetricSpace N] [IsIsometricVAdd Nᵃᵒᵖ N], IsIsometricVAdd (M × N)ᵃᵒᵖ (M × N)
-- Mathlib.Logic.Equiv.Defs
/-- An equivalence `e : α ≃ β` generates an equivalence between the quotient space of `α`
by a relation `ra` and the quotient space of `β` by the image of this relation under `e`.  -/
Quot.congrLeft : {α : Sort u} → {β : Sort v} → {r : α → α → Prop} → (e : α ≃ β) → Quot r ≃ Quot fun b b' => r (e.symm b) (e.symm b')
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey?_eq_none : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → ∀ {a : α}, a ∉ t → t.getKey? a = none
-- Mathlib.GroupTheory.Congruence.Basic
AddCon.comap_addConGen_of_bijective : ∀ {M : Type u_4} {N : Type u_5} [inst : Add M] [inst_1 : Add N] (f : M → N),
  Function.Bijective f →
    ∀ (H : ∀ (x y : M), f (x + y) = f x + f y) (rel : N → N → Prop),
      AddCon.comap f H (addConGen rel) = addConGen fun x y => rel (f x) (f y)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
WeierstrassCurve.Jacobian.equiv_zero_of_Z_eq_zero : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Jacobian F} {P : Fin 3 → F},
  W.Nonsingular P → P 2 = 0 → P ≈ ![1, 1, 0]
-- Lean.Elab.Match
Lean.Elab.Term.elabMatch : Lean.Elab.Term.TermElab
-- Mathlib.Topology.MetricSpace.Isometry
/-- An isometry from an emetric space is a uniform embedding  -/
Isometry.isUniformEmbedding : ∀ {α : Type u} {β : Type v} [inst : EMetricSpace α] [inst_1 : PseudoEMetricSpace β] {f : α → β},
  Isometry f → IsUniformEmbedding f
-- Mathlib.Algebra.Ring.Subring.MulOpposite
Subring.mopRingEquivOp_apply_coe : ∀ {R : Type u_2} [inst : NonAssocRing R] (S : Subring R) (a : (↥S.toSubsemiring)ᵐᵒᵖ),
  ↑(S.mopRingEquivOp a) = MulOpposite.op ↑(MulOpposite.unop a)
-- Mathlib.Algebra.MonoidAlgebra.Defs
/-- **Alias** of `MonoidAlgebra.coeff_mul_apply_right`. -/
MonoidAlgebra.mul_apply_right : ∀ {R : Type u_1} {G : Type u_3} [inst : Semiring R] [inst_1 : Group G] (x y : MonoidAlgebra R G) (g : G),
  (x * y).coeff g = y.coeff.sum fun h r => x.coeff (g * h⁻¹) * r
-- Batteries.Data.Float.Lemmas
Float32.beq_self_iff : ∀ {f : Float32}, (f == f) = true ↔ f ≠ Float32.nan
-- Mathlib.Probability.Kernel.Disintegration.Density
ProbabilityTheory.Kernel.lintegral_density : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} [inst : MeasurableSpace.CountablyGenerated γ] {κ : ProbabilityTheory.Kernel α (γ × β)}
  {ν : ProbabilityTheory.Kernel α γ},
  κ.fst ≤ ν →
    ∀ [ProbabilityTheory.IsFiniteKernel ν] (a : α) {s : Set β},
      MeasurableSet s → ∫⁻ (x : γ), ENNReal.ofReal (κ.density ν a x s) ∂ν a = (κ a) (Set.univ ×ˢ s)
-- Init.Data.Nat.Dvd
Nat.dvd_refl : ∀ (a : ℕ), a ∣ a
-- Mathlib.Algebra.Group.Hom.Defs
instCoeTCAddMonoidHomOfAddMonoidHomClass.eq_1 : ∀ {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]
  [inst_3 : AddMonoidHomClass F M N],
  instCoeTCAddMonoidHomOfAddMonoidHomClass = { coe := AddMonoidHomClass.toAddMonoidHom }
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart
cfcₙ_re_id : ∀ {A : Type u_1} [inst : TopologicalSpace A] [inst_1 : NonUnitalRing A] [inst_2 : StarRing A] [inst_3 : Module ℂ A]
  [inst_4 : IsScalarTower ℂ A A] [inst_5 : SMulCommClass ℂ A A] [inst_6 : StarModule ℂ A]
  [inst_7 : NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal] (a : A),
  autoParam (IsStarNormal a) cfcₙ_re_id._auto_1 → cfcₙ (fun x => ↑x.re) a = ↑(realPart a)
-- Mathlib.Topology.MetricSpace.Contracting
ContractingWith.one_sub_K_pos : ∀ {α : Type u_1} [inst : MetricSpace α] {K : NNReal} {f : α → α}, ContractingWith K f → 0 < 1 - ↑K
-- Std.Do.WP.SimpLemmas
Std.Do.WP.withTheReader_MonadWithReaderOf : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {ρ α : Type u} {Q : Std.Do.PostCond α ps} [inst : MonadWithReaderOf ρ m]
  [inst_1 : Std.Do.WP m ps] (f : ρ → ρ) (x : m α),
  (Std.Do.wp (withTheReader ρ f x)).apply Q = (Std.Do.wp (MonadWithReaderOf.withReader f x)).apply Q
-- Mathlib.NumberTheory.Harmonic.ZetaAsymp
riemannZeta₁_one : riemannZeta₁ 1 = 1
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.smul_integral_comp_add_mul : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b : ℝ} (f : ℝ → E) (c d : ℝ),
  c • ∫ (x : ℝ) in a..b, f (d + c * x) = ∫ (x : ℝ) in d + c * a..d + c * b, f x
-- Mathlib.RingTheory.Polynomial.GaussLemma
/-- **Gauss's Lemma** for GCD domains states that a primitive polynomial is irreducible iff it is
irreducible in the fraction field.  -/
Polynomial.IsPrimitive.irreducible_iff_irreducible_map_fraction_map : ∀ {R : Type u_1} [inst : CommRing R] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra R K] [IsFractionRing R K]
  [IsDomain R] [IsGCDMonoid R] {p : Polynomial R},
  p.IsPrimitive → (Irreducible p ↔ Irreducible (Polynomial.map (algebraMap R K) p))
-- Mathlib.Data.Nat.Bits
Nat.bit_cases_on_injective : ∀ {motive : ℕ → Sort u}, Function.Injective fun H n => Nat.bitCasesOn n H
-- Init.System.ST
instSTWorldOfMonadLift : {σ : Type} → {m n : Type → Type} → [MonadLift m n] → [STWorld σ m] → STWorld σ n
-- Mathlib.Condensed.Light.TopComparison
/-- `TopCat.toLightCondSet` yields a functor from `TopCat.{u}` to `LightCondSet.{u}`.
 -/
topCatToLightCondSet : CategoryTheory.Functor TopCat LightCondSet
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CallHierarchyIncomingCall.mk.sizeOf_spec : ∀ («from» : Lean.Lsp.CallHierarchyItem) (fromRanges : Array Lean.Lsp.Range),
  sizeOf { «from» := «from», fromRanges := fromRanges } = 1 + sizeOf «from» + sizeOf fromRanges
-- Mathlib.CategoryTheory.Limits.Cones
/-- The opposite cone of the image of a cocone is the image of the opposite cone.  -/
CategoryTheory.Functor.mapCoconeOp : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {D : Type u₄} →
          [inst_2 : CategoryTheory.Category.{v₄, u₄} D] →
            {F : CategoryTheory.Functor J C} →
              (G : CategoryTheory.Functor C D) →
                (t : CategoryTheory.Limits.Cocone F) → (G.mapCocone t).op ≅ G.op.mapCone t.op
-- Lean.ScopedEnvExtension
Lean.ScopedEnvExtension.mk.injEq : ∀ {α β σ : Type} (descr : Lean.ScopedEnvExtension.Descr α β σ)
  (ext :
    Lean.PersistentEnvExtension (Lean.ScopedEnvExtension.Entry α) (Lean.ScopedEnvExtension.Entry β)
      (Lean.ScopedEnvExtension.StateStack α β σ))
  (descr_1 : Lean.ScopedEnvExtension.Descr α β σ)
  (ext_1 :
    Lean.PersistentEnvExtension (Lean.ScopedEnvExtension.Entry α) (Lean.ScopedEnvExtension.Entry β)
      (Lean.ScopedEnvExtension.StateStack α β σ)),
  ({ descr := descr, ext := ext } = { descr := descr_1, ext := ext_1 }) = (descr = descr_1 ∧ ext = ext_1)
-- Mathlib.Algebra.Homology.Factorizations.CM5b
CochainComplex.cm5b : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [CategoryTheory.EnoughInjectives C] {K L : CochainComplex C ℤ} (f : K ⟶ L) (n : ℤ) [K.IsStrictlyGE (n + 1)]
  [L.IsStrictlyGE n],
  ∃ L',
    ∃ (_ : L'.IsStrictlyGE n),
      ∃ i p,
        ∃ (_ : CategoryTheory.Mono i) (_ : CochainComplex.degreewiseEpiWithInjectiveKernel p) (_ : QuasiIso p),
          CategoryTheory.CategoryStruct.comp i p = f
-- Lean.Level
Lean.Level.mvar : Lean.LMVarId → Lean.Level
-- Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
ContMDiffMap.ring : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {E' : Type u_3} →
            [inst_3 : NormedAddCommGroup E'] →
              [inst_4 : NormedSpace 𝕜 E'] →
                {H : Type u_4} →
                  [inst_5 : TopologicalSpace H] →
                    {I : ModelWithCorners 𝕜 E H} →
                      {H' : Type u_5} →
                        [inst_6 : TopologicalSpace H'] →
                          {I' : ModelWithCorners 𝕜 E' H'} →
                            {N : Type u_6} →
                              [inst_7 : TopologicalSpace N] →
                                [inst_8 : ChartedSpace H N] →
                                  {n : WithTop ℕ∞} →
                                    {R : Type u_10} →
                                      [inst_9 : Ring R] →
                                        [inst_10 : TopologicalSpace R] →
                                          [inst_11 : ChartedSpace H' R] →
                                            [ContMDiffRing I' n R] → Ring (ContMDiffMap I I' N R n)
-- Mathlib.CategoryTheory.Sites.LocalSite
/-- `coconstantSheaf` is fully faithful.  -/
CategoryTheory.GrothendieckTopology.IsLocalSite.fullyFaithfulCoconstantSheaf : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C] →
        [inst_2 : J.IsLocalSite] →
          (A : Type u') →
            [inst_3 : CategoryTheory.Category.{v', u'} A] →
              [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] →
                [inst_5 : CategoryTheory.Limits.HasProducts A] →
                  [CategoryTheory.HasWeakSheafify J A] →
                    (CategoryTheory.GrothendieckTopology.IsLocalSite.coconstantSheaf J A).FullyFaithful
-- Mathlib.CategoryTheory.ObjectProperty.Ind
CategoryTheory.ObjectProperty.ind_iff_of_equivalence : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{u_2, u_1} D]
  (P : CategoryTheory.ObjectProperty D) (e : C ≌ D) [P.IsClosedUnderIsomorphisms] (X : D),
  (P.inverseImage e.functor).ind (e.inverse.obj X) ↔ P.ind X