mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Tactic.Do.Syntax
/-- `mvcgen` will break down a Hoare triple proof goal like `⦃P⦄ prog ⦃Q⦄` into verification conditions,
provided that all functions used in `prog` have specifications registered with `@[spec]`.

### Verification Conditions and specifications

A verification condition is an entailment in the stateful logic of `Std.Do.SPred`
in which the original program `prog` no longer occurs.
Verification conditions are introduced by the `mspec` tactic; see the `mspec` tactic for what they
look like.
When there's no applicable `mspec` spec, `mvcgen` will try and rewrite an application
`prog = f a b c` with the simp set registered via `@[spec]`.

### Features

When used like `mvcgen +noLetElim [foo_spec, bar_def, instBEqFloat]`, `mvcgen` will additionally

* add a Hoare triple specification `foo_spec : ... → ⦃P⦄ foo ... ⦃Q⦄` to `spec` set for a
  function `foo` occurring in `prog`,
* unfold a definition `def bar_def ... := ...` in `prog`,
* unfold any method of the `instBEqFloat : BEq Float` instance in `prog`.
* it will no longer substitute away `let`-expressions that occur at most once in `P`, `Q` or `prog`.

### Config options

`+noLetElim` is just one config option of many. Check out `Lean.Elab.Tactic.Do.VCGen.Config` for all
options. Of particular note is `stepLimit = some 42`, which is useful for bisecting bugs in
`mvcgen` and tracing its execution.

### Extended syntax

Often, `mvcgen` will be used like this:
```
mvcgen [...]
case inv1 => exact I1
case inv2 => exact I2
all_goals (mleave; try grind)
```
There is special syntax for this:
```
mvcgen [...] invariants
· I1
· I2
with grind
```
When `I1` and `I2` need to refer to inaccessibles (`mvcgen` will introduce a lot of them for program
variables), you can use case label syntax:
```
mvcgen [...] invariants
| inv1 _ acc _ => I1 acc
| _ => I2
with grind
```
This is more convenient than the equivalent `· by rename_i _ acc _; exact I1 acc`.

### Invariant suggestions

`mvcgen` will suggest invariants for you if you use the `invariants?` keyword.
```
mvcgen [...] invariants?
```
This is useful if you do not recall the exact syntax to construct invariants.
Furthermore, it will suggest a concrete invariant encoding "this holds at the start of the loop and
this must hold at the end of the loop" by looking at the corresponding VCs.
Although the suggested invariant is a good starting point, it is too strong and requires users to
interpolate it such that the inductive step can be proved. Example:
```
def mySum (l : List Nat) : Nat := Id.run do
  let mut acc := 0
  for x in l do
    acc := acc + x
  return acc

/--
info: Try this:
  invariants
    · ⇓⟨xs, letMuts⟩ => ⌜xs.prefix = [] ∧ letMuts = 0 ∨ xs.suffix = [] ∧ letMuts = l.sum⌝
-/
#guard_msgs (info) in
theorem mySum_suggest_invariant (l : List Nat) : mySum l = l.sum := by
  generalize h : mySum l = r
  apply Id.of_wp_run_eq h
  mvcgen invariants?
  all_goals admit
```
 -/
Lean.Parser.Tactic.mvcgen : Lean.ParserDescr
-- Lean.Meta.Tactic.Grind.EMatchTheorem
_private.Lean.Meta.Tactic.Grind.EMatchTheorem.0.Lean.Meta.Grind.NormalizePattern.saveSymbolsAt : Lean.Expr → Lean.Meta.Grind.NormalizePattern.M✝ Unit
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
CategoryTheory.Bicategory.Equivalence.instInhabited : {B : Type u₁} → [inst : CategoryTheory.Bicategory B] → {a : B} → Inhabited (CategoryTheory.Bicategory.Equivalence a a)
-- Mathlib.Algebra.Category.ModuleCat.Topology.Basic
/-- The functor equipping a module over a topological ring with the finest possible
topology making it into a topological module. This is left adjoint to the forgetful functor.  -/
TopModuleCat.withModuleTopology : (R : Type u) → [inst : Ring R] → [inst_1 : TopologicalSpace R] → CategoryTheory.Functor (ModuleCat R) (TopModuleCat R)
-- Mathlib.MeasureTheory.Measure.AbsolutelyContinuous
MeasureTheory.Measure.AbsolutelyContinuous.map : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ ν : MeasureTheory.Measure α},
  μ.AbsolutelyContinuous ν →
    ∀ {f : α → β}, Measurable f → (MeasureTheory.Measure.map f μ).AbsolutelyContinuous (MeasureTheory.Measure.map f ν)
-- Mathlib.NumberTheory.Fermat
Nat.fermatNumber_one : Nat.fermatNumber 1 = 5
-- Mathlib.CategoryTheory.Sites.Limits
CategoryTheory.Sheaf.instHasFiniteProducts : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w}
  [inst_1 : CategoryTheory.Category.{w', w} D] [CategoryTheory.Limits.HasFiniteProducts D],
  CategoryTheory.Limits.HasFiniteProducts (CategoryTheory.Sheaf J D)
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.ClosedUnder.inter : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {n : ℕ} {f : L.Functions n} {s t : Set M},
  FirstOrder.Language.ClosedUnder f s → FirstOrder.Language.ClosedUnder f t → FirstOrder.Language.ClosedUnder f (s ∩ t)
-- Mathlib.Data.List.Basic
List.idxOf_append_of_mem : ∀ {α : Type u} {l₁ l₂ : List α} [inst : BEq α] [LawfulBEq α] {a : α}, a ∈ l₁ → List.idxOf a (l₁ ++ l₂) = List.idxOf a l₁
-- Std.Data.Iterators.Lemmas.Equivalence.HetT
Std.Iterators.HetT.map_pure : ∀ {m : Type w → Type w'} [inst : Monad m] [LawfulMonad m] {α : Type u} {β : Type v} {f : α → β} {a : α},
  Std.Iterators.HetT.map f (Std.Iterators.HetT.pure a) = Std.Iterators.HetT.pure (f a)
-- Mathlib.GroupTheory.GroupAction.Blocks
/-- If `B` is a block containing `a`, then the stabilizer of `B` contains the stabilizer of `a`  -/
MulAction.IsBlock.stabilizer_le : ∀ {G : Type u_1} [inst : Group G] {X : Type u_2} [inst_1 : MulAction G X] {B : Set X},
  MulAction.IsBlock G B → ∀ {a : X}, a ∈ B → MulAction.stabilizer G a ≤ MulAction.stabilizer G B
-- Mathlib.Data.Fintype.Basic
Finset.map.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (f : α ↪ β) (s : Finset α),
  Finset.map f s = { val := Multiset.map (⇑f) s.val, nodup := ⋯ }
-- Init.Data.Int.Lemmas
Int.zero_sub : ∀ (a : ℤ), 0 - a = -a
-- Mathlib.CategoryTheory.Abelian.RightDerived
CategoryTheory.Functor.rightDerivedZeroIsoSelf.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  [inst_2 : CategoryTheory.Abelian C] [inst_3 : CategoryTheory.HasInjectiveResolutions C]
  [inst_4 : CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [inst_5 : F.Additive]
  [inst_6 : CategoryTheory.Limits.PreservesFiniteLimits F], F.rightDerivedZeroIsoSelf = F.rightDerivedZeroIsoSelf
-- Mathlib.CategoryTheory.NatIso
CategoryTheory.Iso.app_inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} (α : F ≅ G) (X : C), (α.app X).inv = α.inv.app X
-- Std.Data.ExtTreeMap.Basic
/-- Computes the union of the given tree maps. If a key appears in both maps, the entry contained in
the second argument will appear in the result.

This function always merges the smaller map into the larger map.
 -/
Std.ExtTreeMap.inter : {α : Type u} →
  {β : Type v} →
    {cmp : α → α → Ordering} →
      [Std.TransCmp cmp] → Std.ExtTreeMap α β cmp → Std.ExtTreeMap α β cmp → Std.ExtTreeMap α β cmp
-- Mathlib.Topology.Algebra.Group.Pointwise
IsOpen.mul_closure : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Group G] [IsTopologicalGroup G] {s : Set G},
  IsOpen s → ∀ (t : Set G), s * closure t = s * t
-- Mathlib.Data.Set.Prod
Set.subsingleton_univ_pi : ∀ {ι : Type u_1} {α : ι → Type u_2} {t : (i : ι) → Set (α i)},
  (∀ (i : ι), (t i).Subsingleton) → (Set.univ.pi t).Subsingleton
-- Mathlib.ModelTheory.FinitelyGenerated
/-- A structure is finitely generated if it is the closure of a finite subset.  -/
FirstOrder.Language.Structure.FG : (L : FirstOrder.Language) → (M : Type u_1) → [L.Structure M] → Prop
-- Mathlib.FieldTheory.IsSepClosed
/-- The absolute separable closure is defined to be the relative separable closure inside the
algebraic closure. It is indeed a separable closure (`IsSepClosure`) by
`separableClosure.isSepClosure`, and it is Galois (`IsGalois`) by `separableClosure.isGalois`
or `IsSepClosure.isGalois`, and every separable extension embeds into it (`IsSepClosed.lift`).  -/
SeparableClosure : (F : Type u_1) → [Field F] → Type u_1
-- Mathlib.Algebra.Category.ModuleCat.Colimits
ModuleCat.HasColimit.colimitCocone_ι_app : ∀ {R : Type w} [inst : Ring R] {J : Type u} [inst_1 : CategoryTheory.Category.{v, u} J]
  (F : CategoryTheory.Functor J (ModuleCat R))
  [inst_2 : CategoryTheory.Limits.HasColimit (F.comp (CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat))] (j : J),
  (ModuleCat.HasColimit.colimitCocone F).ι.app j =
    ModuleCat.homMk (CategoryTheory.Limits.colimit.ι (F.comp (CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat)) j) ⋯
-- Mathlib.AlgebraicGeometry.RelativeGluing
AlgebraicGeometry.Scheme.Cover.RelativeGluingData.mk.sizeOf_spec : ∀ {S : AlgebraicGeometry.Scheme} {𝒰 : S.OpenCover} [inst : CategoryTheory.Category.{u_2, u_1} 𝒰.I₀]
  [inst_1 : AlgebraicGeometry.Scheme.Cover.LocallyDirected 𝒰]
  (functor : CategoryTheory.Functor 𝒰.I₀ AlgebraicGeometry.Scheme)
  (natTrans : functor ⟶ AlgebraicGeometry.Scheme.Cover.functorOfLocallyDirected 𝒰)
  (equifibered : CategoryTheory.NatTrans.Equifibered natTrans),
  sizeOf { functor := functor, natTrans := natTrans, equifibered := equifibered } = 1 + sizeOf functor + sizeOf natTrans
-- Mathlib.Topology.Algebra.Group.Basic
ContinuousInv.induced : ∀ {α : Type u_1} {β : Type u_2} {F : Type u_3} [inst : FunLike F α β] [inst_1 : Group α] [inst_2 : DivisionMonoid β]
  [MonoidHomClass F α β] [tβ : TopologicalSpace β] [ContinuousInv β] (f : F), ContinuousInv α
-- Lean.Level
/-- `occurs u l` return `true` iff `u` occurs in `l`.  -/
Lean.Level.occurs : Lean.Level → Lean.Level → Bool
-- Mathlib.GroupTheory.OreLocalization.Basic
AddOreLocalization.oreSubAddChar'.eq_1 : ∀ {R : Type u_1} [inst : AddMonoid R] {S : AddSubmonoid R} [inst_1 : AddOreLocalization.AddOreSet S] (r₁ r₂ : R)
  (s₁ s₂ : ↥S),
  AddOreLocalization.oreSubAddChar' r₁ r₂ s₁ s₂ =
    ⟨AddOreLocalization.oreMin r₁ s₂, ⟨AddOreLocalization.oreSubtra r₁ s₂, ⋯⟩⟩
-- Mathlib.Tactic.Widget.Conv
Mathlib.Tactic.Conv.Path.brecOn.eq : ∀ {motive : Mathlib.Tactic.Conv.Path → Sort u} (t : Mathlib.Tactic.Conv.Path)
  (F_1 : (t : Mathlib.Tactic.Conv.Path) → Mathlib.Tactic.Conv.Path.below t → motive t),
  Mathlib.Tactic.Conv.Path.brecOn t F_1 = F_1 t (Mathlib.Tactic.Conv.Path.brecOn.go t F_1).2
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
/-- `single` as an `AddMonoidHom`.

See `lsingle` for the stronger version as a linear map.  -/
SkewMonoidAlgebra.singleAddHom : {k : Type u_1} → {G : Type u_2} → [inst : AddCommMonoid k] → G → k →+ SkewMonoidAlgebra k G
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
CategoryTheory.Limits.Cofork.unop_π_app_one : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : Cᵒᵖ} {f g : X ⟶ Y}
  (c : CategoryTheory.Limits.Cofork f g),
  c.unop.π.app CategoryTheory.Limits.WalkingParallelPair.one =
    (c.ι.app CategoryTheory.Limits.WalkingParallelPair.zero).unop
-- Mathlib.Topology.Sober
IsGenericPoint.isClosed : ∀ {α : Type u_1} [inst : TopologicalSpace α] {x : α} {S : Set α}, IsGenericPoint x S → IsClosed S
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
CategoryTheory.Bicategory.Adjunction.id.eq_1 : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] (a : B),
  CategoryTheory.Bicategory.Adjunction.id a =
    { unit := (CategoryTheory.Bicategory.rightUnitor (CategoryTheory.CategoryStruct.id a)).inv,
      counit := (CategoryTheory.Bicategory.rightUnitor (CategoryTheory.CategoryStruct.id a)).hom, left_triangle := ⋯,
      right_triangle := ⋯ }
-- Mathlib.GroupTheory.Nilpotent
Subgroup.lowerCentralSeries_eq_bot_iff_nilpotencyClass_le : ∀ {G : Type u_1} [inst : Group G] [hG : Group.IsNilpotent G] {n : ℕ},
  ⊤.lowerCentralSeries n = ⊥ ↔ Group.nilpotencyClass G ≤ n
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
CategoryTheory.Limits.ChosenPullback.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X₁ X₂ S : C} →
      {f₁ : X₁ ⟶ S} →
        {f₂ : X₂ ⟶ S} →
          (pullback : C) →
            (p₁ : pullback ⟶ X₁) →
              (p₂ : pullback ⟶ X₂) →
                (condition : CategoryTheory.CategoryStruct.comp p₁ f₁ = CategoryTheory.CategoryStruct.comp p₂ f₂) →
                  CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.PullbackCone.mk p₁ p₂ condition) →
                    (p : pullback ⟶ S) →
                      autoParam (CategoryTheory.CategoryStruct.comp p₁ f₁ = p)
                          CategoryTheory.Limits.ChosenPullback.hp₁._autoParam →
                        CategoryTheory.Limits.ChosenPullback f₁ f₂
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.monadMap_ReaderT : ∀ {m : Type u → Type v} {Pred EPred : Type u} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] {ρ : Type u}
  {epost : EPred} (f : {β : Type u} → m β → m β) {α : Type u} (x : ReaderT ρ m α) (post : α → ρ → Pred),
  ⦃ fun r => Std.Internal.Do.wp (f (x.run r)) (fun a => post a r) epost ⦄ MonadFunctor.monadMap (fun {β} => f) x ⦃ post;
    epost ⦄
-- Mathlib.CategoryTheory.Sites.Continuous
/-- If `F : C ⥤ D`, `P : Dᵒᵖ ⥤ A` and `E` is a 1-pre-hypercover of an object of `X`,
then `(E.map F).multifork P` is a limit iff `E.multifork (F.op ⋙ P)` is a limit.  -/
CategoryTheory.PreOneHypercover.isLimitMapMultiforkEquiv : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {X : C} →
          (E : CategoryTheory.PreOneHypercover X) →
            (F : CategoryTheory.Functor C D) →
              {A : Type u} →
                [inst_2 : CategoryTheory.Category.{t, u} A] →
                  (P : CategoryTheory.Functor Dᵒᵖ A) →
                    CategoryTheory.Limits.IsLimit ((E.map F).multifork P) ≃
                      CategoryTheory.Limits.IsLimit (E.multifork (F.op.comp P))
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
CategoryTheory.Limits.pushoutIsoOpPullback_inv_snd : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : Cᵒᵖ} (f : X ⟶ Z) (g : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasPushout f g],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushoutIsoOpPullback f g).inv.unop
      (CategoryTheory.Limits.pullback.snd f.unop g.unop) =
    (CategoryTheory.Limits.pushout.inr f g).unop
-- Mathlib.Algebra.Group.Subgroup.Defs
InvMemClass.mk : ∀ {S : Type u_3} {G : outParam (Type u_4)} [inst : Inv G] [inst_1 : SetLike S G],
  (∀ {s : S} {x : G}, x ∈ s → x⁻¹ ∈ s) → InvMemClass S G
-- Mathlib.Algebra.Group.TypeTags.Basic
instSubsingletonMultiplicative : ∀ {α : Type u} [Subsingleton α], Subsingleton (Multiplicative α)
-- Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Asymptotics.isEquivalent_map : ∀ {α : Type u_1} {β : Type u_2} [inst : NormedAddCommGroup β] {l : Filter α} {α₂ : Type u_4} {f g : α₂ → β}
  {k : α → α₂}, Asymptotics.IsEquivalent (Filter.map k l) f g ↔ Asymptotics.IsEquivalent l (f ∘ k) (g ∘ k)
-- Mathlib.Algebra.Homology.DerivedCategory.KInjective
/-- When `L` is a K-injective cochain complex, cohomology classes
in `CohomologyClass K L n` identify to elements in a type `SmallShiftedHom` relatively
to quasi-isomorphisms.  -/
CochainComplex.HomComplex.CohomologyClass.equivOfIsKInjective : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {K L : CochainComplex C ℤ} →
        {n : ℤ} →
          [inst_2 :
              CategoryTheory.Localization.HasSmallLocalizedShiftedHom
                (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) ℤ K L] →
            [L.IsKInjective] →
              CochainComplex.HomComplex.CohomologyClass K L n ≃
                CategoryTheory.Localization.SmallShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) K L n
-- Mathlib.CategoryTheory.Monoidal.Functor
/-- The `Functor.CoreMonoidal` structure given by an oplax monoidal functor such
that `η` and `δ` are isomorphisms.  -/
CategoryTheory.Functor.CoreMonoidal.ofOplaxMonoidal : {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 D] →
            (F : CategoryTheory.Functor C D) →
              [inst_4 : F.OplaxMonoidal] →
                [CategoryTheory.IsIso (CategoryTheory.Functor.OplaxMonoidal.η F)] →
                  [∀ (X Y : C), CategoryTheory.IsIso (CategoryTheory.Functor.OplaxMonoidal.δ F X Y)] → F.CoreMonoidal
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
/-- The sum of two squares is zero iff both elements are zero.  -/
mul_self_add_mul_self_eq_zero : ∀ {R : Type u} [inst : Semiring R] [inst_1 : LinearOrder R] {a b : R} [NoZeroDivisors R] [ExistsAddOfLE R]
  [PosMulMono R] [AddLeftMono R], a * a + b * b = 0 ↔ a = 0 ∧ b = 0
-- Mathlib.Topology.Separation.Hausdorff
/-- If the codomain of an injective continuous function is a Hausdorff space, then so is its
domain.  -/
T2Space.of_injective_continuous : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [T2Space Y] {f : X → Y},
  Function.Injective f → Continuous f → T2Space X
-- Mathlib.Algebra.Polynomial.EraseLead
/-- `eraseLead f` for a polynomial `f` is the polynomial obtained by
subtracting from `f` the leading term of `f`.  -/
Polynomial.eraseLead : {R : Type u_1} → [inst : Semiring R] → Polynomial R → Polynomial R
-- Mathlib.Algebra.Group.Center
Set.mem_center_iff : ∀ {M : Type u_1} [inst : Mul M] {z : M}, z ∈ Set.center M ↔ IsMulCentral z
-- Mathlib.Algebra.BigOperators.Group.Multiset.Basic
AddHom.map_multiset_ne_zero_sum : ∀ {M : Type u_5} {N : Type u_6} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N] (f : M →ₙ+ N) (s : Multiset M),
  s ≠ 0 → f s.sum = (Multiset.map (⇑f) s).sum
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Submonoid.LocalizationMap.map_isRegular : ∀ {M : Type u_1} {N : Type u_2} [inst : CommMonoid M] {S : Submonoid M} [inst_1 : CommMonoid N]
  (f : S.LocalizationMap N) {m : M}, IsRegular m → IsRegular (f m)
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Char
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.Char.0.Char.reduceBinPred : Lean.Name → ℕ → (Char → Char → Bool) → Lean.Expr → Lean.Meta.SimpM Lean.Meta.Simp.Step
-- Mathlib.RingTheory.Polynomial.ScaleRoots
Polynomial.zero_scaleRoots : ∀ {R : Type u_1} [inst : Semiring R] (s : R), Polynomial.scaleRoots 0 s = 0
-- Init.Data.BitVec.Lemmas
BitVec.msb_append : ∀ {w v : ℕ} {x : BitVec w} {y : BitVec v}, (x ++ y).msb = if w = 0 then y.msb else x.msb
-- Mathlib.Data.ENNReal.Real
ENNReal.ofReal_le_ofNat : ∀ {r : ℝ} {n : ℕ} [inst : n.AtLeastTwo], ENNReal.ofReal r ≤ OfNat.ofNat n ↔ r ≤ OfNat.ofNat n
-- Init.Classical
Classical.propComplete : ∀ (a : Prop), a = True ∨ a = False
-- Mathlib.Data.Finsupp.Multiset
Finsupp.toMultiset_add : ∀ {α : Type u_1} (m n : α →₀ ℕ), Finsupp.toMultiset (m + n) = Finsupp.toMultiset m + Finsupp.toMultiset n
-- Std.Data.DTreeMap.Internal.WF.Defs
/-- `insertIfNew` preserves well-formedness. Later shown to be subsumed by `.wf`.  -/
Std.DTreeMap.Internal.Impl.WF.insertIfNew : ∀ {α : Type u} [inst : Ord α] {x : α → Type v} {t : Std.DTreeMap.Internal.Impl α x} {h : t.Balanced} {k : α} {v : x k},
  t.WF → (Std.DTreeMap.Internal.Impl.insertIfNew k v t h).impl.WF
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.L₁'_X₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex.SnakeInput C), S.L₁'.X₂ = S.L₀.X₃
-- Mathlib.Algebra.Field.Basic
inv_eq_self₀ : ∀ {K : Type u_1} [inst : DivisionRing K] {a : K}, a⁻¹ = a ↔ a = -1 ∨ a = 0 ∨ a = 1
-- Mathlib.RingTheory.Finiteness.Ideal
Ideal.fg_ker_comp : ∀ {R : Type u_3} {S : Type u_4} {A : Type u_5} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing A]
  (f : R →+* S) (g : S →+* A),
  (RingHom.ker f).FG → (RingHom.ker g).FG → Function.Surjective ⇑f → (RingHom.ker (g.comp f)).FG
-- Init.Data.Int.Linear
Int.Internal.Linear.norm_dvd : ∀ (ctx : Int.Internal.Linear.Context) (k : ℤ) (e : Int.Internal.Linear.Expr) (p : Int.Internal.Linear.Poly),
  e.norm.beq' p = true → (k ∣ Int.Internal.Linear.Expr.denote ctx e) = (k ∣ Int.Internal.Linear.Poly.denote' ctx p)
-- Mathlib.Algebra.GroupWithZero.Hom
MonoidWithZeroHom.mk.injEq : ∀ {α : Type u_7} {β : Type u_8} [inst : MulZeroOneClass α] [inst_1 : MulZeroOneClass β] (toZeroHom : ZeroHom α β)
  (map_one' : toZeroHom.toFun 1 = 1)
  (map_mul' : ∀ (x y : α), toZeroHom.toFun (x * y) = toZeroHom.toFun x * toZeroHom.toFun y) (toZeroHom_1 : ZeroHom α β)
  (map_one'_1 : toZeroHom_1.toFun 1 = 1)
  (map_mul'_1 : ∀ (x y : α), toZeroHom_1.toFun (x * y) = toZeroHom_1.toFun x * toZeroHom_1.toFun y),
  ({ toZeroHom := toZeroHom, map_one' := map_one', map_mul' := map_mul' } =
      { toZeroHom := toZeroHom_1, map_one' := map_one'_1, map_mul' := map_mul'_1 }) =
    (toZeroHom = toZeroHom_1)
-- Init.Data.List.Count
/-- This lemma is only relevant for `grind`.  -/
Std.Internal.List.not_of_countP_eq_zero_of_mem : ∀ {α : Type u_1} {p : α → Bool} {x : α} {xs : List α}, List.countP p xs = 0 → x ∈ xs → ¬p x = true
-- Mathlib.Algebra.Lie.Weights.RootSystem
LieAlgebra.IsKilling.reflectRoot_isNonZero : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : CharZero K] [inst_2 : LieRing L] [inst_3 : LieAlgebra K L]
  [inst_4 : LieAlgebra.IsKilling K L] [inst_5 : FiniteDimensional K L] {H : LieSubalgebra K L}
  [inst_6 : H.IsCartanSubalgebra] [inst_7 : LieModule.IsTriangularizable K (↥H) L] (α β : LieModule.Weight K (↥H) L),
  β.IsNonZero → (LieAlgebra.IsKilling.reflectRoot α β).IsNonZero
-- Mathlib.Order.WithBot
WithBot.lt_def : ∀ {α : Type u_1} [inst : LT α] {x y : WithBot α}, x < y ↔ (x = ⊥ ∧ ∃ b, y = ↑b) ∨ ∃ a b, a < b ∧ x = ↑a ∧ y = ↑b
-- Batteries.Recycling.RBTree.WF
_private.Batteries.Recycling.RBTree.WF.0.RBTree.RBNode.isRed.match_1.eq_1 : ∀ {α : Type u_1} (motive : RBTree.RBNode α → Sort u_2) (c : RBTree.RBColor) (l : RBTree.RBNode α) (v : α)
  (r : RBTree.RBNode α)
  (h_1 :
    (c : RBTree.RBColor) →
      (l : RBTree.RBNode α) → (v : α) → (r : RBTree.RBNode α) → motive (RBTree.RBNode.node c l v r))
  (h_2 : (x : RBTree.RBNode α) → motive x),
  (match RBTree.RBNode.node c l v r with
    | RBTree.RBNode.node c l v r => h_1 c l v r
    | x => h_2 x) =
    h_1 c l v r
-- Mathlib.CategoryTheory.Sites.ConstantSheaf
/-- If the constant sheaf functor is fully faithful, then a sheaf is constant if and only if the
counit of the constant sheaf adjunction applied to it is an isomorphism.
 -/
CategoryTheory.Sheaf.isConstant_iff_isIso_counit_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (J : CategoryTheory.GrothendieckTopology C)
  {D : Type u_2} [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.HasWeakSheafify J D]
  [(CategoryTheory.constantSheaf J D).Faithful] [(CategoryTheory.constantSheaf J D).Full] (F : CategoryTheory.Sheaf J D)
  {T : C} (hT : CategoryTheory.Limits.IsTerminal T),
  CategoryTheory.Sheaf.IsConstant J F ↔ CategoryTheory.IsIso ((CategoryTheory.constantSheafAdj J D hT).counit.app F)
-- Mathlib.Algebra.Ring.NonZeroDivisors
le_nonZeroDivisors_iff_isRegular : ∀ {R : Type u_1} [inst : Ring R] {S : Submonoid R}, S ≤ nonZeroDivisors R ↔ ∀ (s : ↥S), IsRegular ↑s
-- Std.Time.Zoned
/-- Get the current time, in the local timezone.
 -/
Std.Time.PlainTime.now : IO Std.Time.PlainTime
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.setIntegral_nonneg : ∀ {X : Type u_1} {mX : MeasurableSpace X} {μ : MeasureTheory.Measure X} {f : X → ℝ} {s : Set X},
  MeasurableSet s → (∀ x ∈ s, 0 ≤ f x) → 0 ≤ ∫ (x : X) in s, f x ∂μ
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.contains_map : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  {γ : α → Type w} [EquivBEq α] [LawfulHashable α] {f : (a : α) → β a → γ a} {k : α},
  (↑m).WF → (Std.DHashMap.Internal.Raw₀.map f m).contains k = m.contains k
-- Init.Data.ByteArray.Basic
ByteArray.toList.loop.eq_def : ∀ (bs : ByteArray) (i : ℕ) (r : List UInt8),
  ByteArray.toList.loop bs i r = if i < bs.size then ByteArray.toList.loop bs (i + 1) (bs.get! i :: r) else r.reverse