mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.mkNatIso_inv_app_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 : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} X]
  {J K : CategoryTheory.Functor X (CategoryTheory.Limits.CategoricalPullback F G)}
  (e₁ :
    J.comp (CategoryTheory.Limits.CategoricalPullback.π₁ F G) ≅
      K.comp (CategoryTheory.Limits.CategoricalPullback.π₁ F G))
  (e₂ :
    J.comp (CategoryTheory.Limits.CategoricalPullback.π₂ F G) ≅
      K.comp (CategoryTheory.Limits.CategoricalPullback.π₂ F G))
  (coh :
    autoParam
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight e₁.hom F)
          (CategoryTheory.CategoryStruct.comp (K.associator (CategoryTheory.Limits.CategoricalPullback.π₁ F G) F).hom
            (CategoryTheory.CategoryStruct.comp
              (K.whiskerLeft
                (CategoryTheory.CatCommSq.iso (CategoryTheory.Limits.CategoricalPullback.π₁ F G)
                    (CategoryTheory.Limits.CategoricalPullback.π₂ F G) F G).hom)
              (K.associator (CategoryTheory.Limits.CategoricalPullback.π₂ F G) G).inv)) =
        CategoryTheory.CategoryStruct.comp (J.associator (CategoryTheory.Limits.CategoricalPullback.π₁ F G) F).hom
          (CategoryTheory.CategoryStruct.comp
            (J.whiskerLeft
              (CategoryTheory.CatCommSq.iso (CategoryTheory.Limits.CategoricalPullback.π₁ F G)
                  (CategoryTheory.Limits.CategoricalPullback.π₂ F G) F G).hom)
            (CategoryTheory.CategoryStruct.comp (J.associator (CategoryTheory.Limits.CategoricalPullback.π₂ F G) G).inv
              (CategoryTheory.Functor.whiskerRight e₂.hom G))))
      CategoryTheory.Limits.CategoricalPullback.mkNatIso._auto_1)
  (X_1 : X), ((CategoryTheory.Limits.CategoricalPullback.mkNatIso e₁ e₂ coh).inv.app X_1).snd = e₂.inv.app X_1
-- Init.Data.Iterators.Basic
Std.Iter.IsPlausibleOutput.eq_1 : ∀ {α β : Type w} [inst : Std.Iterator α Id β] (it : Std.Iter β) (out : β),
  it.IsPlausibleOutput out = it.toIterM.IsPlausibleOutput out
-- Mathlib.RingTheory.Valuation.Basic
Valuation.map_sum_lt' : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀)
  {ι : Type u_7} {s : Finset ι} {f : ι → R} {g : Γ₀}, 0 < g → (∀ i ∈ s, v (f i) < g) → v (∑ i ∈ s, f i) < g
-- Mathlib.Dynamics.Ergodic.Action.Basic
/-- A group action of `G` on a space `α` with measure `μ` is called *ergodic*,
if for any (null) measurable set `s`,
if it is a.e.-invariant under each scalar multiplication `(g • ·)`, `g : G`,
then it is either null or conull.
 -/
ErgodicSMul : (G : Type u_1) → (α : Type u_2) → [SMul G α] → {x : MeasurableSpace α} → MeasureTheory.Measure α → Prop
-- Mathlib.LinearAlgebra.Transvection.Basic
LinearEquiv.dilatransvection_mem_dilatransvections : ∀ {R : Type u_1} {V : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup V] [inst_2 : Module R V] {f : Module.Dual R V}
  {v : V} {h : IsUnit (1 + f v)}, LinearEquiv.dilatransvection h ∈ LinearEquiv.dilatransvections R V
-- Mathlib.Topology.MetricSpace.Infsep
Set.infsep_zero : ∀ {α : Type u_1} [inst : EDist α] {s : Set α}, s.infsep = 0 ↔ s.einfsep = 0 ∨ s.einfsep = ⊤
-- Mathlib.Tactic.Inhabit
/-- `inhabit α` tries to derive a `Nonempty α` instance and
then uses it to make an `Inhabited α` instance.
If the target is a `Prop`, this is done constructively. Otherwise, it uses `Classical.choice`.
 -/
Lean.Elab.Tactic.inhabit : Lean.ParserDescr
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instOne.eq_1 : ∀ {α : Type u_1} {l : Filter α} {M : Type u_5} [inst : One M], Filter.Germ.instOne = { one := ↑1 }
-- Mathlib.Order.Hom.Basic
OrderIso.coe_toRelIsoGT : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] (e : α ≃o β), ⇑e.toRelIsoGT = ⇑e
-- Mathlib.CategoryTheory.Linear.LinearFunctor
CategoryTheory.Functor.objPreimage.congr_simp : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F F_1 : CategoryTheory.Functor C D) (e_F : F = F_1) [inst_2 : F.EssSurj] (Y Y_1 : D),
  Y = Y_1 → F.objPreimage Y = F_1.objPreimage Y_1
-- Init.Grind.Config
/-- If `verbose` is `false`, additional diagnostics information is not collected.  -/
Lean.Grind.Config.verbose : Lean.Grind.Config → Bool
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.forIn_eq_forInUncurried : ∀ {α : Type u} {δ : Type w} {m' : Type w → Type w'} {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [inst : Monad m']
  [LawfulMonad m'] {f : α → β → δ → m' (ForInStep δ)} {init : δ},
  Std.DHashMap.Raw.forIn f init m = Std.DHashMap.Raw.Const.forInUncurried (fun a b => f a.1 a.2 b) init m
-- Mathlib.RingTheory.RingHom.Unramified
RingHom.formallyUnramified_algebraMap : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S],
  (algebraMap R S).FormallyUnramified ↔ Algebra.FormallyUnramified R S
-- Lean.Data.Lsp.Internal
Lean.Lsp.LeanLocationLink.toLocationLink : Lean.Lsp.LeanLocationLink → Lean.Lsp.LocationLink
-- Mathlib.Analysis.BoxIntegral.Partition.Tagged
BoxIntegral.TaggedPrepartition.iUnion_single : ∀ {ι : Type u_1} {I J : BoxIntegral.Box ι} {x : ι → ℝ} (hJ : J ≤ I) (h : x ∈ BoxIntegral.Box.Icc I),
  (BoxIntegral.TaggedPrepartition.single I J hJ x h).iUnion = ↑J
-- Mathlib.Topology.Connected.TotallyDisconnected
Topology.IsEmbedding.isTotallyDisconnected : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {s : Set α},
  Topology.IsEmbedding f → IsTotallyDisconnected (f '' s) → IsTotallyDisconnected s
-- Aesop.Rule.Name
Aesop.instBEqScopeName.beq : Aesop.ScopeName → Aesop.ScopeName → Bool
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
/-- The linear map on the result of subtracting two points is the
result of subtracting the result of the affine map on those two
points.  -/
AffineMap.linearMap_vsub : ∀ {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [inst : Ring k]
  [inst_1 : AddCommGroup V1] [inst_2 : Module k V1] [inst_3 : AddTorsor V1 P1] [inst_4 : AddCommGroup V2]
  [inst_5 : Module k V2] [inst_6 : AddTorsor V2 P2] (f : P1 →ᵃ[k] P2) (p1 p2 : P1), f.linear (p1 -ᵥ p2) = f p1 -ᵥ f p2
-- Mathlib.Tactic.TermCongr
/-- Ensures the expected type is an equality. Returns the equality.
The returned expression satisfies `Lean.Expr.eq?`.  -/
Mathlib.Tactic.TermCongr.mkEqForExpectedType : Option Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Combinatorics.Additive.AP.Three.Behrend
Behrend.exists_large_sphere : ∀ (n d : ℕ), ∃ k, ↑(d ^ n) / ↑(n * d ^ 2) ≤ ↑(Behrend.sphere n d k).card
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyData.ofHasKernel_Q : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : CategoryTheory.Limits.HasKernel S.g] (hf : S.f = 0),
  (CategoryTheory.ShortComplex.RightHomologyData.ofHasKernel S hf).Q = S.X₂
-- Mathlib.RingTheory.Jacobson.Ring
Polynomial.comp_C_integral_of_surjective_of_isJacobsonRing : ∀ {R : Type u_1} [inst : CommRing R] [IsJacobsonRing R] {S : Type u_2} [inst_2 : Field S] (f : Polynomial R →+* S),
  Function.Surjective ⇑f → (f.comp Polynomial.C).IsIntegral
-- Mathlib.Algebra.Prime.Lemmas
/-- **Alias** of `DvdNotUnit.not_isUnit`. -/
DvdNotUnit.not_unit : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] {p q : M}, DvdNotUnit p q → ¬IsUnit q
-- Mathlib.Analysis.Normed.Module.Basic
Algebra.norm_smul_one_eq_norm : ∀ {𝕜 : Type u_1} (𝕜' : Type u_2) [inst : NormedField 𝕜] [inst_1 : SeminormedRing 𝕜'] [inst_2 : NormedAlgebra 𝕜 𝕜']
  [NormOneClass 𝕜'] (x : 𝕜), ‖x • 1‖ = ‖x‖
-- Init.Data.BitVec.Lemmas
BitVec.zero_eq_neg_one_iff : ∀ {w : ℕ}, 0#w = -1#w ↔ w = 0
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cocone.precomposeComp_hom_app_hom : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F G H : CategoryTheory.Functor J C} (β : H ⟶ G) (α : G ⟶ F) (X : CategoryTheory.Limits.Cocone F),
  ((CategoryTheory.Limits.Cocone.precomposeComp β α).hom.app X).hom = CategoryTheory.CategoryStruct.id X.pt
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.image_op_one : ∀ {α : Type u_2} [inst : One α], MulOpposite.op '' 1 = 1
-- Lean.Data.Lsp.Ipc
Lean.Lsp.Ipc.ModuleHierarchy.item : Lean.Lsp.Ipc.ModuleHierarchy → Lean.Lsp.LeanImport
-- Lean.Elab.InfoTree.Types
Lean.Elab.CompletionInfo.dotId.injEq : ∀ (stx : Lean.Syntax) (id : Lean.Name) (lctx : Lean.LocalContext) (expectedType? : Option Lean.Expr)
  (stx_1 : Lean.Syntax) (id_1 : Lean.Name) (lctx_1 : Lean.LocalContext) (expectedType?_1 : Option Lean.Expr),
  (Lean.Elab.CompletionInfo.dotId stx id lctx expectedType? =
      Lean.Elab.CompletionInfo.dotId stx_1 id_1 lctx_1 expectedType?_1) =
    (stx = stx_1 ∧ id = id_1 ∧ lctx = lctx_1 ∧ expectedType? = expectedType?_1)
-- Init.Data.Vector.Lemmas
Vector.reverse_empty : ∀ {α : Type u_1}, #v[].reverse = #v[]
-- Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations
/-- Lemma 3.5 from [Geck](Geck2017).  -/
RootPairing.GeckConstruction.lie_e_f_ne : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Finite ι] [inst_1 : CommRing R]
  [inst_2 : IsDomain R] [inst_3 : CharZero R] [inst_4 : AddCommGroup M] [inst_5 : Module R M] [inst_6 : AddCommGroup N]
  [inst_7 : Module R N] {P : RootPairing ι R M N} [inst_8 : P.IsCrystallographic] {b : P.Base} [inst_9 : Fintype ι]
  {i j : ↥b.support},
  i ≠ j → ∀ [P.IsReduced] [P.IsIrreducible], ⁅RootPairing.GeckConstruction.e i, RootPairing.GeckConstruction.f j⁆ = 0
-- Mathlib.ModelTheory.Order
FirstOrder.Language.Term.lt.eq_1 : ∀ {L : FirstOrder.Language} {α : Type w} {n : ℕ} [inst : L.IsOrdered] (t₁ t₂ : L.Term (α ⊕ Fin n)),
  t₁.lt t₂ = t₁.le t₂ ⊓ (t₂.le t₁).not
-- Mathlib.Topology.Category.LightProfinite.Basic
LightDiagram.mk : (diagram : CategoryTheory.Functor ℕᵒᵖ FintypeCat) →
  (cone : CategoryTheory.Limits.Cone (diagram.comp FintypeCat.toProfinite)) →
    CategoryTheory.Limits.IsLimit cone → LightDiagram
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
/-- Restrict an injective algebra homomorphism to an algebra isomorphism  -/
AlgEquiv.ofInjective : {R : Type u} →
  {A : Type v} →
    {B : Type w} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Semiring B] →
            [inst_3 : Algebra R A] → [inst_4 : Algebra R B] → (f : A →ₐ[R] B) → Function.Injective ⇑f → A ≃ₐ[R] ↥f.range
-- Init.Control.Lawful.Basic
seqRight_eq_bind : ∀ {m : Type u_1 → Type u_2} {α β : Type u_1} [inst : Monad m] [LawfulMonad m] (x : m α) (y : m β),
  x *> y = do
    let _ ← x
    y
-- Mathlib.AlgebraicGeometry.Normalization
AlgebraicGeometry.Scheme.Hom.fromNormalization_app : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.QuasiCompact f]
  [inst_1 : AlgebraicGeometry.QuasiSeparated f] {U : Y.Opens} (hU : AlgebraicGeometry.IsAffineOpen U),
  AlgebraicGeometry.Scheme.Hom.app (AlgebraicGeometry.Scheme.Hom.fromNormalization f) U =
    CategoryTheory.CategoryStruct.comp
      (CommRingCat.ofHom
        (algebraMap ↑(Y.presheaf.1 (Opposite.op U))
          ↥(integralClosure ↑(Y.presheaf.obj (Opposite.op U))
              ↑(X.presheaf.obj (Opposite.op ((TopologicalSpace.Opens.map f.base).obj U))))))
      (AlgebraicGeometry.Scheme.Hom.normalizationObjIso f hU).inv
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.keysArray_insertIfNew_perm : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [inst : BEq α]
  [Std.TransCmp cmp] [Std.LawfulBEqCmp cmp],
  t.WF → ∀ {k : α} {v : β k}, (t.insertIfNew k v).keysArray.Perm (if k ∈ t then t.keysArray else t.keysArray.push k)
-- Std.Data.DTreeMap.Internal.Cell
/-- Internal implementation detail of the tree map  -/
Std.DTreeMap.Internal.List.findCell : {α : Type u} →
  {β : α → Type v} → [inst : Ord α] → List ((a : α) × β a) → (k : α → Ordering) → Std.DTreeMap.Internal.Cell α β k
-- Mathlib.Algebra.CubicDiscriminant
Cubic.degree_of_b_ne_zero : ∀ {R : Type u_1} {P : Cubic R} [inst : Semiring R], P.a = 0 → P.b ≠ 0 → P.toPoly.degree = 2
-- Mathlib.Order.Types.Arithmetic
OrderType.card_one : OrderType.card 1 = 1
-- Mathlib.Probability.Kernel.Category.SFinKer
SFinKer.tensorObj_str : ∀ (X Y : SFinKer), (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).str = Prod.instMeasurableSpace
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
/-- The covering map from `ℝ` to the "additive circle" `ℝ ⧸ (ℤ ∙ T)` is measure-preserving,
considered with respect to the standard measure (defined to be the Haar measure of total mass `T`)
on the additive circle, and with respect to the restriction of Lebesgue measure on `ℝ` to an
interval $(t, t + T]$.  -/
AddCircle.measurePreserving_mk : ∀ (T : ℝ) [hT : Fact (0 < T)] (t : ℝ),
  MeasureTheory.MeasurePreserving QuotientAddGroup.mk (MeasureTheory.volume.restrict (Set.Ioc t (t + T)))
    MeasureTheory.volume
-- Mathlib.Algebra.Group.Defs
Group.toDivisionMonoid : {G : Type u_1} → [Group G] → DivisionMonoid G
-- Mathlib.Computability.TuringMachine.Tape
Turing.Tape.mk'_nth_nat : ∀ {Γ : Type u_1} [inst : Inhabited Γ] (L R : Turing.ListBlank Γ) (n : ℕ), (Turing.Tape.mk' L R).nth ↑n = R.nth n
-- Mathlib.Order.Max
noBotOrder_iff : ∀ {α : Type u_1} [inst : LE α], NoBotOrder α ↔ ∀ (x : α), ¬IsBot x
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get_inter : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α fun x => β}
  [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] (h₁ : (↑m₁).WF) (h₂ : (↑m₂).WF) {k : α}
  {h_contains : (m₁.inter m₂).contains k = true},
  Std.DHashMap.Internal.Raw₀.Const.get (m₁.inter m₂) k h_contains = Std.DHashMap.Internal.Raw₀.Const.get m₁ k ⋯
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.ext_iff : ∀ {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [inst : (i : α) → NormedAddCommGroup (E i)] {f g : ↥(lp E p)},
  f = g ↔ ↑f = ↑g
-- Mathlib.Algebra.Ring.Subsemiring.Basic
/-- A subsemiring is isomorphic to its image under an injective function  -/
Subsemiring.equivMapOfInjective : {R : Type u} →
  {S : Type v} →
    [inst : NonAssocSemiring R] →
      [inst_1 : NonAssocSemiring S] →
        (s : Subsemiring R) → (f : R →+* S) → Function.Injective ⇑f → ↥s ≃+* ↥(Subsemiring.map f s)
-- Mathlib.LinearAlgebra.Matrix.Symmetric
Matrix.isSymm_transpose_add_self : ∀ {α : Type u_1} {n : Type u_3} [inst : AddCommSemigroup α] (A : Matrix n n α), (A.transpose + A).IsSymm
-- Mathlib.NumberTheory.LSeries.RiemannZeta
/-- The Riemann zeta function is differentiable away from `s = 1`.  -/
differentiableAt_riemannZeta : ∀ {s : ℂ}, s ≠ 1 → DifferentiableAt ℂ riemannZeta s
-- Mathlib.Topology.EMetricSpace.Defs
/-- Two pseudo emetric space structures with the same edistance function coincide.  -/
PseudoEMetricSpace.ext : ∀ {α : Type u_2} {m m' : PseudoEMetricSpace α}, m.toEDist = m'.toEDist → m = m'
-- Mathlib.Order.Interval.Set.ProjIcc
/-- Projection of `α` to the closed interval `(-∞, b]`.  -/
Set.projIic : {α : Type u_1} → [inst : LinearOrder α] → (b : α) → α → ↑(Set.Iic b)
-- Init.Data.Dyadic.Inv
/-- For a positive dyadic `b`, `a < (divAtPrec a b prec + 2^(-prec)) * b`.  -/
Dyadic.lt_divAtPrec_add_inc_mul : ∀ {a b : Dyadic}, 0 < b → ∀ (prec : ℤ), a < (a.divAtPrec b prec + Dyadic.ofIntWithPrec 1 prec) * b
-- Mathlib.Analysis.Normed.Ring.WithAbs
/-- **Alias** of `WithAbs.instModule`. -/
WithAbs.instModule_right : {S : Type u_2} →
  [inst : Semiring S] →
    [inst_1 : PartialOrder S] →
      {R : Type u_3} →
        {T : Type u_4} →
          [inst_2 : Semiring R] → (v : AbsoluteValue R S) → [inst_3 : Semiring T] → [Module T R] → Module T (WithAbs v)
-- Init.Data.String.Lemmas.FindPos
String.Slice.offset_posLT_lt : ∀ {s : String.Slice} {p : String.Pos.Raw} {h : 0 < p}, (s.posLT p h).offset < p
-- Mathlib.Topology.Category.Profinite.Nobeling.Basic
Profinite.NobelingProof.projRestricts_comp_projRestrict : ∀ {I : Type u} (C : Set (I → Bool)) {J K : I → Prop} [inst : (i : I) → Decidable (J i)]
  [inst_1 : (i : I) → Decidable (K i)] (h : ∀ (i : I), J i → K i),
  Profinite.NobelingProof.ProjRestricts C h ∘ Profinite.NobelingProof.ProjRestrict C K =
    Profinite.NobelingProof.ProjRestrict C J
-- Mathlib.Algebra.CubicDiscriminant
Cubic.prod_X_sub_C_eq : ∀ {S : Type u_2} [inst : CommRing S] {x y z : S},
  (Polynomial.X - Polynomial.C x) * (Polynomial.X - Polynomial.C y) * (Polynomial.X - Polynomial.C z) =
    { a := 1, b := -(x + y + z), c := x * y + x * z + y * z, d := -(x * y * z) }.toPoly
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.ball_subset_ball : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x : α} {ε₁ ε₂ : ℝ}, ε₁ ≤ ε₂ → Metric.ball x ε₁ ⊆ Metric.ball x ε₂
-- Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Real.volume_singleton : ∀ {a : ℝ}, MeasureTheory.volume {a} = 0
-- Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
NumberField.InfinitePlace.Completion.ofCompletion.sizeOf_spec : ∀ {K : Type u_1} [inst : Field K] {v : NumberField.InfinitePlace K} [inst_1 : SizeOf K]
  (toCompletion : (↑v).Completion), sizeOf { toCompletion := toCompletion } = 1 + sizeOf toCompletion
-- Init.Omega.Int
_private.Init.Omega.Int.0.Int.neg.match_1.eq_2 : ∀ (motive : ℤ → Sort u_1) (n : ℕ) (h_1 : (n : ℕ) → motive (Int.ofNat n)) (h_2 : (n : ℕ) → motive (Int.negSucc n)),
  (match Int.negSucc n with
    | Int.ofNat n => h_1 n
    | Int.negSucc n => h_2 n) =
    h_2 n
-- Mathlib.Condensed.Light.InternallyProjective
LightCondensed.ihomPoints_symm_apply : ∀ (R : Type u) [inst : CommRing R] (A B : LightCondMod R) (S : LightProfinite)
  (x : CategoryTheory.MonoidalCategoryStruct.tensorObj A ((LightCondensed.free R).obj S.toCondensed) ⟶ B),
  (LightCondensed.ihomPoints R A B S).symm x =
    (CategoryTheory.coherentTopology LightProfinite).yonedaEquiv
      (((LightCondensed.freeForgetAdjunction R).homEquiv ((CategoryTheory.coherentTopology LightProfinite).yoneda.obj S)
          (A ⟹ B))
        (CategoryTheory.MonoidalClosed.curry x))
-- Aesop.Search.Expansion.Norm
Aesop.NormStep : Type
-- Lean.PrettyPrinter.Delaborator.SubExpr
/-- Merges two collections of options, where the second overrides the first.  -/
Lean.PrettyPrinter.Delaborator.OptionsPerPos.merge : Lean.PrettyPrinter.Delaborator.OptionsPerPos →
  Lean.PrettyPrinter.Delaborator.OptionsPerPos → Lean.PrettyPrinter.Delaborator.OptionsPerPos
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Stepwise.d_step1_certC.eq_1 : ∀ (p₁ : Lean.Grind.CommRing.Poly) (k₂ : ℤ) (m₂ : Lean.Grind.CommRing.Mon) (p₂ p : Lean.Grind.CommRing.Poly) (c : ℕ),
  Lean.Grind.CommRing.Stepwise.d_step1_certC p₁ k₂ m₂ p₂ p c =
    p.beq' (p₁.combineC (Lean.Grind.CommRing.Poly.mulMonC k₂ m₂ p₂ c) c)
-- Mathlib.LinearAlgebra.AffineSpace.Midpoint
/-- A map `f : E → F` sending zero to zero and midpoints to midpoints is an `AddMonoidHom`.  -/
AddMonoidHom.ofMapMidpoint : (R : Type u_1) →
  (R' : Type u_2) →
    {E : Type u_3} →
      {F : Type u_4} →
        [inst : Ring R] →
          [inst_1 : Invertible 2] →
            [inst_2 : AddCommGroup E] →
              [inst_3 : Module R E] →
                [inst_4 : Ring R'] →
                  [inst_5 : Invertible 2] →
                    [inst_6 : AddCommGroup F] →
                      [inst_7 : Module R' F] →
                        (f : E → F) → f 0 = 0 → (∀ (x y : E), f (midpoint R x y) = midpoint R' (f x) (f y)) → E →+ F
-- Std.Time.Internal.UnitVal
Std.Time.Internal.instOrientedOrdUnitVal : ∀ {x : ℚ}, Std.OrientedOrd (Std.Time.Internal.UnitVal x)
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Grp.instBraidedCategory.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C],
  CategoryTheory.Grp.instBraidedCategory =
    CategoryTheory.BraidedCategory.ofFaithful (CategoryTheory.Grp.forget₂Mon C)
      (fun G H => CategoryTheory.Grp.mkIso (β_ G.X H.X) ⋯ ⋯) ⋯
-- Mathlib.Algebra.Algebra.Bilinear
LinearMap.mul'.eq_1 : ∀ (R : Type u_1) (A : Type u_2) [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  [inst_3 : SMulCommClass R A A] [inst_4 : IsScalarTower R A A],
  LinearMap.mul' R A = TensorProduct.lift (LinearMap.mul R A)
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.Cont'.cons₁.injEq : ∀ (a : Turing.ToPartrec.Code) (a_1 : Turing.PartrecToTM2.Cont') (a_2 : Turing.ToPartrec.Code)
  (a_3 : Turing.PartrecToTM2.Cont'),
  (Turing.PartrecToTM2.Cont'.cons₁ a a_1 = Turing.PartrecToTM2.Cont'.cons₁ a_2 a_3) = (a = a_2 ∧ a_1 = a_3)
-- Mathlib.Algebra.Group.Units.Basic
IsUnit.mul_left_injective : ∀ {M : Type u_1} [inst : Monoid M] {b : M}, IsUnit b → Function.Injective fun x => x * b
-- Mathlib.FieldTheory.CardinalEmb
Field.Emb.Cardinal.eq_bot_of_not_nonempty : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E]
  [rank_inf : Fact (Cardinal.aleph0 ≤ Module.rank F E)] [inst_3 : Algebra.IsAlgebraic F E]
  {i : WithTop (Module.rank F E).ord.ToType},
  Order.IsSuccPrelimit i → ¬Nonempty ↑(Set.Iio i) → Field.Emb.Cardinal.filtration i = ⊥
-- Mathlib.Algebra.Order.UpperLower
UpperSet.coe_mul : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : Preorder α] [inst_2 : IsOrderedMonoid α] (s t : UpperSet α),
  ↑(s * t) = ↑s * ↑t
-- Mathlib.Combinatorics.Matroid.Rank.Cardinal
Matroid.IsBasis'.cardinalMk_eq_cRk : ∀ {α : Type u} {M : Matroid α} {I X : Set α} [M.InvariantCardinalRank], M.IsBasis' I X → Cardinal.mk ↑I = M.cRk X
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.image_const_sub_Ioo : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] (a b c : α),
  (fun x => a - x) '' Set.Ioo b c = Set.Ioo (a - c) (a - b)
-- Mathlib.Tactic.Rify
/-- `rify` rewrites the main goal by shifting propositions from `ℕ`, `ℤ`, `ℚ` or `ℝ≥0` to `ℝ`.
Although less useful than its cousins `zify` and `qify`, it can be useful when your
goal or context already involves real numbers.

`rify` makes use of the `@[zify_simps]`, `@[qify_simps]` and `@[rify_simps]` attributes to insert
casts into propositions, and the `push_cast` tactic to simplify the `ℝ`-valued expressions.

`rify` is in some sense dual to the `lift` tactic. `lift (r : ℝ) to ℚ` will change the type of a
real number `r` (in the supertype) to `ℚ` (the subtype), given a proof that `r` is rational;
propositions concerning `r` will still be over `ℝ`. `rify` changes propositions about `ℕ`, `ℤ`, `ℚ`
or `ℝ≥0` (the subtype) to propositions about `ℝ` (the supertype), without changing the type of any
variable.

* `rify at l1 l2 ...` rewrites at the given locations.
* `rify [h₁, ..., hₙ]` uses the expressions `h₁`, ..., `hₙ` as extra lemmas for simplification.
  This is especially useful in the presence of nat subtraction or of division: passing arguments of
  type `· ≤ ·` or `· ∣ ·` will allow `push_cast` to do more work.

Examples:
```
/--
import Mathlib

open Real
Here, the assumption `hn` is about natural numbers, `hk` is about integers
and involves casting a natural number to `ℤ`, and the conclusion is about real numbers.
-/
example {n : ℕ} {k : ℤ} (hn : 8 ≤ n) (hk : 2 * k ≤ n + 2) :
    (0 : ℝ) < n - k - 1 := by
  rify at hn hk /- Now have hn : 8 ≤ (n : ℝ)   hk : 2 * (k : ℝ) ≤ (n : ℝ) + 2 -/
  linarith

-- Extra hypotheses allow `push_cast` to do more work.
example (a b c : ℕ) (h : a - b < c) (hab : b ≤ a) : a < b + c := by
  rify [hab] at h ⊢ -- Here `zify` or `qify` would have also worked.
  linarith

example (a b : ℕ) (ha : π ≤ a) : 3 ≤ a + b := by
  rify
  linarith [pi_gt_three]
```
 -/
Mathlib.Tactic.Rify.rify : Lean.ParserDescr
-- Mathlib.RingTheory.Nilpotent.Lemmas
mem_nilradical : ∀ {R : Type u_1} [inst : CommSemiring R] {x : R}, x ∈ nilradical R ↔ IsNilpotent x