mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Under.inv_right_hom_right : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X : T} {f g : CategoryTheory.Under X} (e : f ≅ g),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Under.Hom.right e.inv) (CategoryTheory.Under.Hom.right e.hom) =
    CategoryTheory.CategoryStruct.id g.right
-- Mathlib.Topology.Compactness.Compact
Quotient.compactSpace : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Setoid X} [CompactSpace X], CompactSpace (Quotient s)
-- Mathlib.Algebra.Group.Units.Opposite
Units.coe_unop_opEquiv : ∀ {M : Type u_2} [inst : Monoid M] (u : Mᵐᵒᵖˣ), ↑(MulOpposite.unop (Units.opEquiv u)) = MulOpposite.unop ↑u
-- Std.Do.PostCond
/-- Lifts a proposition `p` to a set of assertions about the possible exceptions in `ps`. Each
exception's postcondition holds when `p` is true.
 -/
Std.Do.ExceptConds.const : {ps : Std.Do.PostShape} → Prop → Std.Do.ExceptConds ps
-- Mathlib.Topology.OpenPartialHomeomorph.Defs
OpenPartialHomeomorph.symm_bijective : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  Function.Bijective OpenPartialHomeomorph.symm
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Pretrivialization.domExtend.eq_1 : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  {s : Set B} (e : Bundle.Pretrivialization F fun z => proj ↑z) [inst_2 : Nonempty (Z → F)],
  e.domExtend =
    { toFun := fun z => if h : proj z ∈ s then ↑e ⟨z, h⟩ else (proj z, Classical.arbitrary (Z → F) z),
      invFun := fun x => ↑(e.invFun x), source := Subtype.val '' e.source, target := e.target, map_source' := ⋯,
      map_target' := ⋯, left_inv' := ⋯, right_inv' := ⋯, open_target := ⋯, baseSet := e.baseSet, open_baseSet := ⋯,
      source_eq := ⋯, target_eq := ⋯, proj_toFun := ⋯ }
-- Mathlib.Topology.Sets.Opens
TopologicalSpace.Opens.comap_mono : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : C(α, β))
  {s t : TopologicalSpace.Opens β}, s ≤ t → (TopologicalSpace.Opens.comap f) s ≤ (TopologicalSpace.Opens.comap f) t
-- Init.Data.List.Lemmas
List.intercalate_cons_cons_left : ∀ {α : Type u_1} {ys l : List α} {x : α} {zs : List (List α)},
  ys.intercalate ((x :: l) :: zs) = x :: ys.intercalate (l :: zs)
-- Mathlib.CategoryTheory.Sites.SheafCohomology.MayerVietoris
/-- The difference of two restriction maps in sheaf cohomology.  -/
CategoryTheory.GrothendieckTopology.MayerVietorisSquare.fromBiprod : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      [inst_1 : CategoryTheory.HasWeakSheafify J (Type v)] →
        [inst_2 : CategoryTheory.HasSheafify J AddCommGrpCat] →
          [inst_3 : CategoryTheory.HasExt (CategoryTheory.Sheaf J AddCommGrpCat)] →
            (S : J.MayerVietorisSquare) →
              (F : CategoryTheory.Sheaf J AddCommGrpCat) → (n : ℕ) → F.H' n S.X₂ ⊞ F.H' n S.X₃ ⟶ F.H' n S.X₁
-- Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv
_private.Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv.0.GenContFract.contsAux.match_1.eq_2 : ∀ {K : Type u_1} (motive : Option (GenContFract.Pair K) → Sort u_2) (gp : GenContFract.Pair K)
  (h_1 : Unit → motive none) (h_2 : (gp : GenContFract.Pair K) → motive (some gp)),
  (match some gp with
    | none => h_1 ()
    | some gp => h_2 gp) =
    h_2 gp
-- Init.System.Uri
_private.Init.System.Uri.0.System.Uri.normalizeDriveLetter : String → String
-- Init.Data.Vector.Lemmas
/-- `map_id'` differs from `map_id` by representing the identity function as a lambda, rather than `id`.  -/
Vector.map_id' : ∀ {α : Type u_1} {n : ℕ} (xs : Vector α n), Vector.map (fun a => a) xs = xs
-- Mathlib.Tactic.Linter.FlexibleLinter
/-- `goalsCreatedBy t` are the `MVarId`s after the `TacticInfo` `t` that were not present before.
They should correspond to the goals created or changed by the tactic `t`.  -/
_private.Mathlib.Tactic.Linter.FlexibleLinter.0.Lean.Elab.TacticInfo.goalsCreatedBy : Lean.Elab.TacticInfo → List Lean.MVarId
-- Mathlib.Data.Finsupp.Lex
Finsupp.Colex.orderBot : {α : Type u_1} →
  {N : Type u_2} →
    [inst : LinearOrder α] →
      [inst_1 : AddCommMonoid N] → [inst_2 : PartialOrder N] → [IsBotZeroClass N] → OrderBot (Colex (α →₀ N))
-- Init.Data.BitVec.Lemmas
BitVec.msb_setWidth' : ∀ {w v : ℕ} (x : BitVec w) (h : w ≤ v), (BitVec.setWidth' h x).msb = (decide (0 < v) && x.getLsbD (v - 1))
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
Std.IterM.allM_eq_forIn : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Std.Iterator α m β] [Std.Iterators.Finite α m] [inst_2 : Monad m]
  [LawfulMonad m] [inst_4 : Std.IteratorLoop α m m] [Std.LawfulIteratorLoop α m m] {it : Std.IterM m β}
  {p : β → m (ULift.{w, 0} Bool)},
  Std.IterM.allM p it =
    forIn it { down := true } fun x x_1 => do
      let __do_lift ← p x
      if __do_lift.down = true then pure (ForInStep.yield { down := true }) else pure (ForInStep.done { down := false })
-- Mathlib.Topology.Algebra.NonUnitalAlgebra
NonUnitalSubalgebra.topologicalClosure_mono : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : TopologicalSpace A] [inst_2 : NonUnitalSemiring A]
  [inst_3 : Module R A] [inst_4 : ContinuousConstSMul R A] [inst_5 : IsSemitopologicalSemiring A]
  {s t : NonUnitalSubalgebra R A}, s ≤ t → s.topologicalClosure ≤ t.topologicalClosure
-- Mathlib.ModelTheory.Types
FirstOrder.Language.Theory.realizedTypes.eq_1 : ∀ {L : FirstOrder.Language} (T : L.Theory) (M : Type w') [inst : L.Structure M] [inst_1 : Nonempty M] [inst_2 : M ⊨ T]
  (α : Type w), T.realizedTypes M α = Set.range T.typeOf
-- Mathlib.Order.Interval.Set.Basic
Set.Ioo_eq_empty_iff : ∀ {α : Type u_1} [inst : Preorder α] {a b : α} [DenselyOrdered α], Set.Ioo a b = ∅ ↔ ¬a < b
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Over
CategoryTheory.Limits.PreservesLimitsOfShape.ofWidePullbacks : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {J : Type u_1}
  [CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Limits.WidePullbackShape J) F],
  CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.WithTerminal (CategoryTheory.Discrete J)) F
-- Mathlib.Data.List.Nodup
/-- **Alias** of `List.disjoint_of_nodup_append`. -/
List.Nodup.disjoint : ∀ {α : Type u} {l₁ l₂ : List α}, (l₁ ++ l₂).Nodup → l₁.Disjoint l₂
-- Lean.Elab.App
/-- If it seems that the user may be attempting to project out the `n`th element of a tuple, or that the
nesting behavior of n-ary products is otherwise relevant, generates a corresponding hint; otherwise,
produces an empty message.
 -/
_private.Lean.Elab.App.0.Lean.Elab.Term.mkTupleHint : Lean.Expr → ℕ → Lean.Syntax → Lean.Elab.TermElabM Lean.MessageData
-- Init.Data.String.Substring
/-- Returns the region of the substring delimited by the provided start and stop positions, as a
substring. The positions are interpreted with respect to the substring's start position, rather than
the underlying string.

If the resulting substring is empty, then the resulting substring is a substring of the empty string
`""`. Otherwise, the underlying string is that of the input substring with the beginning and end
positions adjusted.
 -/
Substring.Raw.extract : Substring.Raw → String.Pos.Raw → String.Pos.Raw → Substring.Raw
-- Init.Data.Array.Lemmas
Array.replicate_eq_empty_iff : ∀ {α : Type u_1} {n : ℕ} {a : α}, Array.replicate n a = #[] ↔ n = 0
-- Mathlib.LinearAlgebra.LinearIndependent.Lemmas
LinearIndepOn.mem_span_iff : ∀ {ι : Type u'} {K : Type u_3} {V : Type u} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  {s : Set ι} {a : ι} {f : ι → V},
  LinearIndepOn K f s → (f a ∈ Submodule.span K (f '' s) ↔ LinearIndepOn K f (insert a s) → a ∈ s)
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toList_rcc_eq_cons : ∀ {m n : ℕ}, m ≤ n → (m...=n).toList = m :: ((m + 1)...=n).toList
-- Mathlib.Topology.Category.LightProfinite.Limits
LightProfinite.instEpiCompHausLikeAndTotallyDisconnectedSpaceCarrierSecondCountableTopologySnd : ∀ {X Y Z : LightProfinite} (f : X ⟶ Z) (g : Y ⟶ Z) [h : CategoryTheory.Epi f],
  CategoryTheory.Epi (CompHausLike.pullback.snd f g)
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.Take
Std.IterM.step_take : ∀ {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [inst : Monad m] [inst_1 : Std.Iterator α m β] {n : ℕ}
  {it : Std.IterM m β},
  (Std.IterM.take n it).step =
    match n with
    | 0 => pure (Std.Shrink.deflate (Std.PlausibleIterStep.done ⋯))
    | k.succ => do
      let __do_lift ← it.step
      match __do_lift.inflate with
        | ⟨Std.IterStep.yield it' out, h⟩ =>
          pure (Std.Shrink.deflate (Std.PlausibleIterStep.yield (Std.IterM.take k it') out ⋯))
        | ⟨Std.IterStep.skip it', h⟩ =>
          pure (Std.Shrink.deflate (Std.PlausibleIterStep.skip (Std.IterM.take (k + 1) it') ⋯))
        | ⟨Std.IterStep.done, h⟩ => pure (Std.Shrink.deflate (Std.PlausibleIterStep.done ⋯))
-- Mathlib.Topology.MetricSpace.Pseudo.Constructions
continuous_iff_continuous_dist : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoMetricSpace α] [inst_1 : TopologicalSpace β] {f : β → α},
  Continuous f ↔ Continuous fun x => dist (f x.1) (f x.2)
-- Mathlib.CategoryTheory.Category.Cat
CategoryTheory.Functor.equivCatHom_symm_apply : ∀ (C D : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Category.{v, u} D]
  (self : (CategoryTheory.Cat.of C).Hom (CategoryTheory.Cat.of D)),
  (CategoryTheory.Functor.equivCatHom C D).symm self = self.toFunctor
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.TableEntry.mk : Array Lean.Meta.SynthInstance.Waiter → Array Lean.Meta.SynthInstance.Answer → Lean.Meta.SynthInstance.TableEntry
-- Mathlib.Order.Hom.Set
OrderIso.unique_of_wellFoundedGT : {α : Type u_1} → [inst : LinearOrder α] → [WellFoundedGT α] → Unique (α ≃o α)
-- Std.Do.WP.Monad
Std.Do.EStateM.instWPMonad : {ε σ : Type u_1} →
  Std.Do.WPMonad (EStateM ε σ) (Std.Do.PostShape.except ε (Std.Do.PostShape.arg σ Std.Do.PostShape.pure))
-- Mathlib.Analysis.Real.Pi.Bounds
Real.pi_gt_d2 : 3.14 < Real.pi
-- Mathlib.Topology.Algebra.GroupCompletion
instNegCompletion : {α : Type u_3} → [inst : UniformSpace α] → [Neg α] → Neg (UniformSpace.Completion α)
-- Mathlib.Algebra.Order.Floor.Defs
Int.floor_toNat : ∀ {α : Type u_2} [inst : Ring α] [inst_1 : LinearOrder α] [inst_2 : FloorRing α] (a : α), ⌊a⌋.toNat = ⌊a⌋₊
-- Mathlib.Algebra.Category.MonCat.Limits
CommMonCat.instSmallElemForallObjCompMonCatForget₂MonoidHomCarrierCarrierForgetSections : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J CommMonCat)
  [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget CommMonCat)).sections],
  Small.{u, max u v} ↑((F.comp (CategoryTheory.forget₂ CommMonCat MonCat)).comp (CategoryTheory.forget MonCat)).sections
-- Mathlib.RingTheory.Coprime.Basic
IsRelPrime.add_mul_right_left : ∀ {R : Type u_1} [inst : CommRing R] {x y : R}, IsRelPrime x y → ∀ (z : R), IsRelPrime (x + z * y) y
-- Mathlib.Algebra.Polynomial.Taylor
Polynomial.taylor_zero : ∀ {R : Type u_1} [inst : Semiring R] (f : Polynomial R), (Polynomial.taylor 0) f = f
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.le_induce_union_right : ∀ {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph} {s s' : Set V}, G'.induce s' ≤ G'.induce (s ∪ s')
-- Mathlib.GroupTheory.Index
Subgroup.finiteIndex_of_le : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G} [H.FiniteIndex], H ≤ K → K.FiniteIndex
-- Std.Time.Time.Unit.Nanosecond
Std.Time.Nanosecond.instOrdOffset : Ord Std.Time.Nanosecond.Offset
-- Mathlib.Algebra.Free
FreeSemigroup.map_mul' : ∀ {α β : Type u} (f : α → β) (x y : FreeSemigroup α), f <$> (x * y) = f <$> x * f <$> y
-- Lean.Meta.Constructions.CtorElim
Lean.mkCtorElimName : Lean.Name → Lean.Name
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
AntitoneOn.intervalIntegrable : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsLocallyFiniteMeasure μ]
  [inst_2 : ConditionallyCompleteLinearOrder E] [OrderTopology E] [SecondCountableTopology E] {u : ℝ → E} {a b : ℝ},
  AntitoneOn u (Set.uIcc a b) → IntervalIntegrable u μ a b
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Tactic.ComputeAsymptotics.MultiseriesExpansion.toReal_ofReal : ∀ (ms : Tactic.ComputeAsymptotics.MultiseriesExpansion []),
  Tactic.ComputeAsymptotics.MultiseriesExpansion.ofReal ms.toReal = ms
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.IdealSheafData.support_mul : ∀ {X : AlgebraicGeometry.Scheme} (I J : X.IdealSheafData), (I * J).support = I.support ⊔ J.support
-- Mathlib.Data.Set.Sigma
Set.mk_sigma_iff : ∀ {ι : Type u_1} {α : ι → Type u_3} {s : Set ι} {t : (i : ι) → Set (α i)} {i : ι} {a : α i},
  ⟨i, a⟩ ∈ s.sigma t ↔ i ∈ s ∧ a ∈ t i
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.Integrable.inf : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_8} [inst : NormedAddCommGroup β]
  [inst_1 : Lattice β] [HasSolidNorm β] [IsOrderedAddMonoid β] {f g : α → β},
  MeasureTheory.Integrable f μ → MeasureTheory.Integrable g μ → MeasureTheory.Integrable (f ⊓ g) μ
-- Mathlib.Data.Finmap
Finmap.disjoint_union_left : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] (x y z : Finmap β),
  (x ∪ y).Disjoint z ↔ x.Disjoint z ∧ y.Disjoint z
-- Mathlib.Combinatorics.Configuration
Configuration.ProjectivePlane.pointCount_eq : ∀ (P : Type u_1) {L : Type u_2} [inst : Membership P L] [inst_1 : Configuration.ProjectivePlane P L] [Finite P]
  [Finite L] (l : L), Configuration.pointCount P l = Configuration.ProjectivePlane.order P L + 1
-- Mathlib.Algebra.Order.Antidiag.Prod
Finset.HasAntidiagonal.map_prodComm_antidiagonal : ∀ {A : Type u_1} [inst : AddCommMonoid A] [inst_1 : Finset.HasAntidiagonal A] {n : A},
  Finset.map (Equiv.prodComm A A).toEmbedding (Finset.HasAntidiagonal.antidiagonal n) =
    Finset.HasAntidiagonal.antidiagonal n
-- Mathlib.Algebra.Homology.Embedding.Basic
/-- An embedding of a complex shape `c : ComplexShape ι` into a complex shape
`c' : ComplexShape ι'` consists of an injective map `f : ι → ι'` which satisfies
a compatibility with respect to the relations `c.Rel` and `c'.Rel`.  -/
ComplexShape.Embedding : {ι : Type u_1} → {ι' : Type u_2} → ComplexShape ι → ComplexShape ι' → Type (max u_1 u_2)
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.restrictScalarsₗ_apply : ∀ (R : Type u_14) (S : Type u_15) (M : Type u_16) (N : Type u_17) [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid N] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : Module S M] [inst_7 : Module S N] [inst_8 : LinearMap.CompatibleSMul M N R S] (R₁ : Type u_19)
  [inst_9 : Semiring R₁] [inst_10 : Module R₁ N] [inst_11 : SMulCommClass S R₁ N] [inst_12 : SMulCommClass R R₁ N]
  (fₗ : M →ₗ[S] N), (LinearMap.restrictScalarsₗ R S M N R₁) fₗ = ↑R fₗ
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.Step.addExtraArgs : Lean.Meta.Simp.Step → Array Lean.Expr → Lean.MetaM Lean.Meta.Simp.Step
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.baseChange_negDblY : ∀ {R : Type r} {S : Type s} {A : Type u} {B : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing A]
  [inst_3 : CommRing B] {W' : WeierstrassCurve.Projective R} [inst_4 : Algebra R S] [inst_5 : Algebra R A]
  [inst_6 : Algebra S A] [IsScalarTower R S A] [inst_8 : Algebra R B] [inst_9 : Algebra S B] [IsScalarTower R S B]
  (f : A →ₐ[S] B) (P : Fin 3 → A), (W'.baseChange B).negDblY (⇑f ∘ P) = f ((W'.baseChange A).negDblY P)
-- Mathlib.Algebra.Module.LinearMap.Index
LinearMap.index_of_injective : ∀ {M : Type u_1} {N : Type u_2} [inst : AddCommGroup M] [inst_1 : AddCommGroup N] {R : Type u_3} [inst_2 : Ring R]
  [inst_3 : Module R M] [inst_4 : Module R N] {f : M →ₗ[R] N} [Nontrivial R],
  Function.Injective ⇑f → f.index = -↑(Module.finrank R (N ⧸ f.range))
-- Mathlib.Topology.Algebra.Module.FiniteDimension
/-- The space of continuous linear maps between finite-dimensional spaces is finite-dimensional.

This theorem is here to match searches looking for `FiniteDimensional` instead of `Module.Finite`.
We use a strictly more general `ContinuousLinearMap.instModuleFinite` as an instance.  -/
ContinuousLinearMap.finiteDimensional : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : AddCommGroup E] [inst_1 : TopologicalSpace E]
  [inst_2 : AddCommGroup F] [inst_3 : TopologicalSpace F] [inst_4 : IsTopologicalAddGroup F] [inst_5 : Field 𝕜]
  [inst_6 : Module 𝕜 E] [FiniteDimensional 𝕜 E] [inst_8 : Module 𝕜 F] [FiniteDimensional 𝕜 F]
  [inst_10 : ContinuousConstSMul 𝕜 F], FiniteDimensional 𝕜 (E →L[𝕜] F)
-- Init.Data.UInt.Lemmas
UInt32.zero_mod : ∀ {a : UInt32}, 0 % a = 0
-- Mathlib.MeasureTheory.Function.SimpleFunc
/-- A sequence of `ℝ≥0∞`s such that its range is the set of non-negative rational numbers.  -/
MeasureTheory.SimpleFunc.ennrealRatEmbed : ℕ → ENNReal
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddSubmonoid.LocalizationMap.mk'_add_eq_mk'_of_add : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N]
  (f : S.LocalizationMap N) (x₁ x₂ : M) (y : ↥S), f.mk' x₂ y + f x₁ = f.mk' (x₁ + x₂) y
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.instPartialOrder : {L : FirstOrder.Language} → {M : Type w} → [inst : L.Structure M] → PartialOrder (L.Substructure M)
-- Mathlib.Algebra.CubicDiscriminant
Cubic.monic_of_c_eq_one' : ∀ {R : Type u_1} {d : R} [inst : Semiring R], { a := 0, b := 0, c := 1, d := d }.toPoly.Monic
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
/-- Distinct vertices are not reachable in the empty graph.  -/
SimpleGraph.reachable_bot : ∀ {V : Type u} {u v : V}, ⊥.Reachable u v ↔ u = v
-- Mathlib.Algebra.Polynomial.GroupRingAction
prodXSubSMul.smul : ∀ (G : Type u_2) [inst : Group G] [inst_1 : Fintype G] (R : Type u_3) [inst_2 : CommRing R]
  [inst_3 : MulSemiringAction G R] (x : R) (g : G), g • prodXSubSMul G R x = prodXSubSMul G R x
-- Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
WeierstrassCurve.ofJ_0_of_three_ne_zero : ∀ {F : Type u_2} [inst : Field F] [inst_1 : DecidableEq F], 3 ≠ 0 → WeierstrassCurve.ofJ 0 = WeierstrassCurve.ofJ0 F
-- Mathlib.Data.Nat.Hyperoperation
hyperoperation.eq_2 : ∀ (x : ℕ), hyperoperation 1 x 0 = x
-- Mathlib.Data.Fintype.Order
Directed.finite_le : ∀ {α : Type u_2} {r : α → α → Prop} [IsTrans α r] {ι : Sort u_4} {κ : Sort u_5} [Nonempty ι] [Finite κ] {f : ι → α},
  Directed r f → ∀ (g : κ → ι), ∃ z, ∀ (i : κ), r (f (g i)) (f z)
-- Init.Prelude
HAndThen.mk : {α : Type u} → {β : Type v} → {γ : outParam (Type w)} → (α → (Unit → β) → γ) → HAndThen α β γ
-- Mathlib.Analysis.Normed.Group.AddTorsor
edist_vsub_vsub_le : ∀ {V : Type u_2} {P : Type u_3} [inst : SeminormedAddCommGroup V] [inst_1 : PseudoMetricSpace P]
  [inst_2 : NormedAddTorsor V P] (p₁ p₂ p₃ p₄ : P), edist (p₁ -ᵥ p₂) (p₃ -ᵥ p₄) ≤ edist p₁ p₃ + edist p₂ p₄
-- Mathlib.GroupTheory.Complement
AddSubgroup.isComplement_addSubgroup_left_iff_existsUnique_quotientMk'' : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G} {T : Set G},
  AddSubgroup.IsComplement (↑H) T ↔ ∀ (q : Quotient (QuotientAddGroup.rightRel H)), ∃! t, Quotient.mk'' ↑t = q
-- Mathlib.Topology.Algebra.Valued.WithVal
/-- Converts an element of `WithVal v` to an element of `R`.  -/
WithVal.ofVal : {R : Type u_1} →
  {Γ₀ : Type u_2} →
    [inst : LinearOrderedCommGroupWithZero Γ₀] → [inst_1 : Ring R] → {v : Valuation R Γ₀} → WithVal v → R
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.image_neg_Iio : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] (a : α),
  Neg.neg '' Set.Iio a = Set.Ioi (-a)
-- Lean.Meta.Tactic.Grind.Proof
_private.Lean.Meta.Tactic.Grind.Proof.0.Lean.Meta.Grind.mkCongrProofFunCC.go : Lean.Expr → Lean.Expr → Bool → Lean.Expr → Lean.Expr → ℕ → Lean.Meta.Grind.GoalM Lean.Expr
-- Std.Internal.Do.Order.Lemmas
Std.Internal.Do.CompleteLattice.meet_self : ∀ {l : Type u} [inst : Lean.Order.CompleteLattice l] {P : l}, Lean.Order.meet P P = P
-- Mathlib.Topology.Order
coinduced_iSup : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {ι : Sort w} {t : ι → TopologicalSpace α},
  TopologicalSpace.coinduced f (⨆ i, t i) = ⨆ i, TopologicalSpace.coinduced f (t i)
-- Mathlib.SetTheory.Ordinal.Topology
Ordinal.mem_closure_iff_iSup : ∀ {s : Set Ordinal.{u}} {a : Ordinal.{u}},
  a ∈ closure s ↔ ∃ ι, ∃ (_ : Nonempty ι), ∃ f, (∀ (i : ι), f i ∈ s) ∧ ⨆ i, f i = a
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Products
CategoryTheory.Limits.piObjIso_hom_comp_π : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} D]
  {α : Type w} [inst_2 : CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Discrete α) C]
  (f : α → CategoryTheory.Functor D C) (d : D) (s : α),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.piObjIso f d).hom
      (CategoryTheory.Limits.Pi.π (fun s => (f s).obj d) s) =
    (CategoryTheory.Limits.Pi.π f s).app d
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
csInf_eq_univ_of_not_bddBelow : ∀ {α : Type u_1} [inst : ConditionallyCompleteLinearOrder α] {s : Set α}, ¬BddBelow s → sInf s = sInf Set.univ
-- Mathlib.Topology.UniformSpace.Completion
CauchyFilter.pureCauchy.eq_1 : ∀ {α : Type u} [inst : UniformSpace α] (a : α), CauchyFilter.pureCauchy a = ⟨pure a, ⋯⟩
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.kernelSequenceCyclesE_exact : ∀ {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₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃)
  (f₂₃ : i₁ ⟶ i₃) (h₂₃ : CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.kernelSequenceCyclesE_exact._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.kernelSequenceCyclesE_exact._auto_3),
  (X.kernelSequenceCyclesE f₁ f₂ f₃ f₂₃ h₂₃ n₀ n₁ n₂ hn₁ hn₂).Exact
-- Mathlib.Data.ENNReal.Operations
ENNReal.sub_sub_sub_cancel_left : ∀ {a b c : ENNReal}, a ≠ ⊤ → b ≤ a → a - c - (a - b) = b - c
-- Aesop.Script.StructureStatic
Aesop.Script.StaticStructureM.State.perfect : Aesop.Script.StaticStructureM.State → Bool
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.ofArray_eq_ofList : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (a : Array ((a : α) × β a)),
  Std.DHashMap.Raw.ofArray a = Std.DHashMap.Raw.ofList a.toList
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.whiskerRight_tensor_symm_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X X' : C}
  (f : X ⟶ X') (Y Z : C) {Z_1 : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X' Y) Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Y) Z)
      h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight f (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z))
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X' Y Z).inv h))
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.tendsto_integral_norm_approxOn_sub : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_7} [inst : NormedAddCommGroup E]
  [inst_1 : MeasurableSpace E] [inst_2 : BorelSpace E] {f : α → E} (fmeas : Measurable f),
  MeasureTheory.Integrable f μ →
    ∀ [inst_3 : TopologicalSpace.SeparableSpace ↑(Set.range f ∪ {0})],
      Filter.Tendsto
        (fun n => ∫ (x : α), ‖(MeasureTheory.SimpleFunc.approxOn f fmeas (Set.range f ∪ {0}) 0 ⋯ n) x - f x‖ ∂μ)
        Filter.atTop (nhds 0)