mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.SpectralSequence.Basic
/-- A cohomological spectral sequence has differentials given by the
vector `(r, 1 - r)` on the `r`th page.  -/
CategoryTheory.CohomologicalSpectralSequence : (C : Type u_1) → [inst : CategoryTheory.Category.{u_3, u_1} C] → [CategoryTheory.Abelian C] → ℤ → Type (max u_1 u_3)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Add
Std.Tactic.BVDecide.BVExpr.bitblast.instLawfulOperatorFullAdderInputMkFullAdderCarry : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α],
  Std.Sat.AIG.LawfulOperator α Std.Tactic.BVDecide.BVExpr.bitblast.FullAdderInput
    Std.Tactic.BVDecide.BVExpr.bitblast.mkFullAdderCarry
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.Equiv.congr_right : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ t₃ : Std.TreeSet.Raw α cmp}, t₁.Equiv t₂ → (t₃.Equiv t₁ ↔ t₃.Equiv t₂)
-- Mathlib.Combinatorics.Hall.Basic
/-- Given a matching on a finset, construct the restriction of that matching to a subset.  -/
hallMatchingsOn.restrict : {ι : Type u} →
  {α : Type v} →
    (t : ι → Finset α) → {ι' ι'' : Finset ι} → ι' ⊆ ι'' → ↑(hallMatchingsOn t ι'') → ↑(hallMatchingsOn t ι')
-- Lean.Server.Requests
Lean.Language.SnapshotTree.foldSnaps.Control.proceed.injEq : ∀ (foldChildren foldChildren_1 : Bool),
  (Lean.Language.SnapshotTree.foldSnaps.Control.proceed foldChildren =
      Lean.Language.SnapshotTree.foldSnaps.Control.proceed foldChildren_1) =
    (foldChildren = foldChildren_1)
-- Mathlib.Tactic.FieldSimp.Lemmas
Mathlib.Tactic.FieldSimp.NF.eval.eq_1 : ∀ {M : Type u_1} [inst : GroupWithZero M] (l : Mathlib.Tactic.FieldSimp.NF M),
  l.eval =
    (List.map
        (fun x =>
          match x with
          | (r, x) => Mathlib.Tactic.FieldSimp.zpow' x r)
        l).prod
-- Lean.Elab.PreDefinition.WF.GuessLex
/-- Create a cache to memoize calls to `evalRecCall descTactic? rcc`  -/
Lean.Elab.WF.GuessLex.RecCallCache.mk : Array Lean.Name →
  Array (Option Lean.Elab.DecreasingBy) →
    Array (Array Lean.Elab.WF.GuessLex.BasicMeasure) →
      Lean.Elab.WF.GuessLex.RecCallWithContext → BaseIO Lean.Elab.WF.GuessLex.RecCallCache
-- Mathlib.Tactic.Positivity.Basic
/-- The `positivity` extension which identifies expressions of the form `a / b`,
where `a` and `b` are integers.  -/
Mathlib.Meta.Positivity.evalIntDiv : Mathlib.Meta.Positivity.PositivityExt
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.incidenceFinset_eq_filter : ∀ {V : Type u_1} (G : SimpleGraph V) (v : V) [inst : Fintype ↑(G.neighborSet v)] [inst_1 : DecidableEq V]
  [inst_2 : Fintype ↑G.edgeSet], G.incidenceFinset v = {e ∈ G.edgeFinset | v ∈ e}
-- Init.System.IO
/-- Runs an action with the specified stream `h` as standard input, restoring the original standard
input stream afterwards.
 -/
IO.withStdin : {m : Type → Type u_1} → {α : Type} → [Monad m] → [MonadFinally m] → [MonadLiftT BaseIO m] → IO.FS.Stream → m α → m α
-- Std.Time.Time.Unit.Basic
/-- Converts a `Minute.Offset` to a `Millisecond.Offset`.
 -/
Std.Time.Minute.Offset.toMilliseconds : Std.Time.Minute.Offset → Std.Time.Millisecond.Offset
-- Init.Meta.Defs
_private.Init.Meta.Defs.0.Lean.Name.beq.eq_def : ∀ (x x_1 : Lean.Name),
  x.beq x_1 =
    match x, x_1 with
    | Lean.Name.anonymous, Lean.Name.anonymous => true
    | p₁.str s₁, p₂.str s₂ => s₁ == s₂ && p₁.beq p₂
    | p₁.num n₁, p₂.num n₂ => n₁ == n₂ && p₁.beq p₂
    | x, x_2 => false
-- Lean.Environment
_private.Lean.Environment.0.Lean.setImportedEntries : Array Lean.EnvExtensionState → Array Lean.ModuleData → optParam ℕ 0 → IO (Array Lean.EnvExtensionState)
-- Mathlib.MeasureTheory.Integral.MeanInequalities
ENNReal.fun_eq_funMulInvSnorm_mul_eLpNorm : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {p : ℝ} (f : α → ENNReal),
  ∫⁻ (a : α), f a ^ p ∂μ ≠ 0 →
    ∫⁻ (a : α), f a ^ p ∂μ ≠ ⊤ → ∀ {a : α}, f a = ENNReal.funMulInvSnorm f p μ a * (∫⁻ (c : α), f c ^ p ∂μ) ^ (1 / p)
-- Mathlib.Condensed.Light.Sequence
_private.Mathlib.Condensed.Light.Sequence.0.InternalProjectivityProof.y : {S : Type u_1} → {T : Type u_2} → {X : Type u_3} → (π : T → S × OnePoint X) → ↑(InternalProjectivityProof.S'✝ π) → S
-- Mathlib.CategoryTheory.Presentable.Directed
CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.IsTerminal.comm_assoc : ∀ {J : Type w} [inst : CategoryTheory.SmallCategory J] {κ : Cardinal.{w}}
  {D : CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram J κ} {e : J} (self : D.IsTerminal e) {i j : J}
  (f : i ⟶ j) (hf : D.W f) {Z : J} (h : e ⟶ Z),
  CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (self.lift ⋯) h) =
    CategoryTheory.CategoryStruct.comp (self.lift ⋯) h
-- Mathlib.Order.RelClasses
/-- Derive a `WellFoundedRelation` instance from an `IsWellOrder` instance.  -/
IsWellOrder.toHasWellFounded : {α : Type u} → [inst : LT α] → [hwo : IsWellOrder α fun x1 x2 => x1 < x2] → WellFoundedRelation α
-- Init.Data.String.Lemmas.Pattern.String.ForwardSearcher
String.Slice.Pattern.Model.ForwardStringSearcher.toSearcher_empty : ∀ (s : String.Slice),
  String.Slice.Pattern.ToForwardSearcher.toSearcher "" s =
    { internalState := String.Slice.Pattern.ForwardSliceSearcher.emptyBefore s.startPos }
-- Init.Data.Int.DivMod.Lemmas
Int.fdiv_eq_iff_eq_mul_right : ∀ {a b c : ℤ}, b ≠ 0 → b ∣ a → (a.fdiv b = c ↔ a = b * c)
-- Batteries.Data.AssocList
Batteries.AssocList.beq_nil₂ : ∀ {α : Type u_1} {β : Type u_2} [inst : BEq α] [inst_1 : BEq β],
  (Batteries.AssocList.nil == Batteries.AssocList.nil) = true
-- Mathlib.Algebra.Group.Subgroup.Defs
AddSubgroup.ext_iff : ∀ {G : Type u_1} [inst : AddGroup G] {H K : AddSubgroup G}, H = K ↔ ∀ (x : G), x ∈ H ↔ x ∈ K
-- Init.Data.SInt.Lemmas
Int32.ofIntClamp_int16ToInt : ∀ (x : Int16), Int32.ofIntClamp x.toInt = x.toInt32
-- Mathlib.SetTheory.ZFC.PSet
PSet.equiv_iff : ∀ {x : PSet.{u_1}} {y : PSet.{u_2}},
  x.Equiv y ↔ (∀ (i : x.Type), ∃ j, (x.Func i).Equiv (y.Func j)) ∧ ∀ (j : y.Type), ∃ i, (x.Func i).Equiv (y.Func j)
-- Mathlib.NumberTheory.FLT.Three
/-- Let `u₄ := η * S.u₃ * S.u₂⁻¹`  -/
_private.Mathlib.NumberTheory.FLT.Three.0.FermatLastTheoremForThreeGen.Solution.u₄ : {K : Type u_1} →
  [inst : Field K] →
    {ζ : K} →
      {hζ : IsPrimitiveRoot ζ 3} →
        FermatLastTheoremForThreeGen.Solution✝ hζ →
          [inst_1 : NumberField K] → [IsCyclotomicExtension {3} ℚ K] → (NumberField.RingOfIntegers K)ˣ
-- Mathlib.LinearAlgebra.Dimension.Free
Module.finrank_div_finrank_cancel_right_of_nontrivial : ∀ (F : Type u) (K : Type v) (A : Type w) [inst : Semiring F] [inst_1 : Semiring K] [inst_2 : AddCommMonoid A]
  [inst_3 : Module F K] [inst_4 : Module K A] [inst_5 : Module F A] [IsScalarTower F K A] [StrongRankCondition F]
  [StrongRankCondition K] [Module.Free F K] [Module.Free K A] [Nontrivial A] [Module.Finite K A],
  Module.finrank F A / Module.finrank K A = Module.finrank F K
-- Init.Data.SInt.Lemmas
Int32.zero_add : ∀ (a : Int32), 0 + a = a
-- Mathlib.Topology.ContinuousMap.CocompactMap
/-- Copy of a `CocompactMap` with a new `toFun` equal to the old one. Useful
to fix definitional equalities.  -/
CocompactMap.copy : {α : Type u_1} →
  {β : Type u_2} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] → (f : CocompactMap α β) → (f' : α → β) → f' = ⇑f → CocompactMap α β
-- Mathlib.RingTheory.UniqueFactorizationDomain.Moebius
UniqueFactorizationMonoid.moebius_one : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α],
  UniqueFactorizationMonoid.moebius 1 = 1
-- Mathlib.Algebra.Opposites
MulOpposite.instNeg : {α : Type u_1} → [Neg α] → Neg αᵐᵒᵖ
-- Batteries.Data.MLList.Basic
/-- The implementation of `ForIn`, which enables `for a in L do ...` notation.  -/
MLList.forIn : {m : Type u_1 → Type u_1} →
  {n : Type u_1 → Type u_2} →
    {α δ : Type u_1} → [Monad m] → [Monad n] → [MonadLiftT m n] → MLList m α → δ → (α → δ → n (ForInStep δ)) → n δ
-- Mathlib.FieldTheory.SeparableClosure
Field.instNeZeroSepDegree : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E], NeZero (Field.sepDegree F E)
-- Mathlib.RingTheory.HahnSeries.Lex
HahnSeries.archimedeanClassMk_le_archimedeanClassMk_iff_of_orderTop_ofLex : ∀ {Γ : Type u_1} {R : Type u_2} [inst : LinearOrder Γ] [inst_1 : LinearOrder R] [inst_2 : AddCommGroup R]
  [inst_3 : IsOrderedAddMonoid R] {x y : Lex (HahnSeries Γ R)},
  (ofLex x).orderTop = (ofLex y).orderTop →
    (ArchimedeanClass.mk x ≤ ArchimedeanClass.mk y ↔
      ArchimedeanClass.mk (ofLex x).leadingCoeff ≤ ArchimedeanClass.mk (ofLex y).leadingCoeff)
-- Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
/-- The canonical projection from `1`-hypercovers to `1`-hypercovers up to homotopy.  -/
CategoryTheory.GrothendieckTopology.OneHypercover.toHOneHypercover : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      (S : C) → CategoryTheory.Functor (J.OneHypercover S) (J.HOneHypercover S)
-- Mathlib.Algebra.Homology.HomologySequenceLemmas
HomologicalComplex.HomologySequence.epi_homologyMap_τ₃ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {c : ComplexShape ι} {S₁ S₂ : CategoryTheory.ShortComplex (HomologicalComplex C c)} (φ : S₁ ⟶ S₂),
  S₁.ShortExact →
    S₂.ShortExact →
      ∀ (i : ι),
        CategoryTheory.Epi (HomologicalComplex.homologyMap φ.τ₂ i) →
          (∀ (j : ι), c.Rel i j → CategoryTheory.Epi (HomologicalComplex.homologyMap φ.τ₁ j)) →
            (∀ (j : ι), c.Rel i j → CategoryTheory.Mono (HomologicalComplex.homologyMap φ.τ₂ j)) →
              CategoryTheory.Epi (HomologicalComplex.homologyMap φ.τ₃ i)
-- Mathlib.Algebra.CharP.Defs
CharP.cast_eq_mod : ∀ (R : Type u_1) [inst : AddMonoidWithOne R] (p : ℕ) [CharP R p] (k : ℕ), ↑k = ↑(k % p)
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
SimplexCategoryGenRel.mem_isAdmissible_of_lt_and_eval_eq_eval_add_one : ∀ {m : ℕ} (L : List ℕ),
  SimplexCategoryGenRel.IsAdmissible m L →
    ∀ j < m + L.length,
      SimplexCategoryGenRel.simplicialEvalσ L j = SimplexCategoryGenRel.simplicialEvalσ L (j + 1) → j ∈ L
-- Mathlib.MeasureTheory.Integral.CircleAverage
/-- Circle averages commute with continuous linear maps.  -/
ContinuousLinearMap.circleAverage_comp_comm : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {F : Type u_2} [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] [CompleteSpace F] {c : ℂ} {R : ℝ} [CompleteSpace E] (L : E →L[ℝ] F) {f : ℂ → E},
  CircleIntegrable f c R → Real.circleAverage (⇑L ∘ f) c R = L (Real.circleAverage f c R)
-- Mathlib.Algebra.Order.Group.Defs
inv_le_inv' : ∀ {α : Type u} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] {a b : α}, a ≤ b → b⁻¹ ≤ a⁻¹
-- Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
HomotopicalAlgebra.RightHomotopyRel.symm : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C}
  [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C] {f g : X ⟶ Y},
  HomotopicalAlgebra.RightHomotopyRel f g → HomotopicalAlgebra.RightHomotopyRel g f
-- Mathlib.CategoryTheory.Galois.IsFundamentalgroup
CategoryTheory.PreGaloisCategory.toAut_surjective_isGalois_finite_family : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) (G : Type u_1)
  [inst_1 : Group G] [inst_2 : (X : C) → MulAction G (F.obj X).obj] [CategoryTheory.PreGaloisCategory.IsNaturalSMul F G]
  [inst_4 : CategoryTheory.GaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F]
  (t : CategoryTheory.Aut F) {ι : Type u_2} [Finite ι] (X : ι → C)
  [∀ (i : ι), CategoryTheory.PreGaloisCategory.IsGalois (X i)],
  (∀ (X : C) [CategoryTheory.PreGaloisCategory.IsGalois X], MulAction.IsPretransitive G (F.obj X).obj) →
    ∃ g, ∀ (i : ι) (x : (F.obj (X i)).obj), g • x = (CategoryTheory.ConcreteCategory.hom (t.hom.app (X i))) x
-- Init.PropLemmas
forall_prop_of_true : ∀ {p : Prop} {q : p → Prop} (h : p), (∀ (h' : p), q h') ↔ q h
-- Init.Data.UInt.Lemmas
UInt64.add_mul : ∀ {a b c : UInt64}, (a + b) * c = a * c + b * c
-- Mathlib.RingTheory.Coalgebra.Basic
Pi.instIsCocomm : ∀ {R : Type u_1} {n : Type u_2} [inst : CommSemiring R] [inst_1 : Fintype n] [inst_2 : DecidableEq n] {A : n → Type u_3}
  [inst_3 : (i : n) → AddCommMonoid (A i)] [inst_4 : (i : n) → Module R (A i)] [inst_5 : (i : n) → Coalgebra R (A i)]
  [∀ (i : n), Coalgebra.IsCocomm R (A i)], Coalgebra.IsCocomm R ((i : n) → A i)
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.Equiv.getGT?_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [Std.TransCmp cmp] {k : α},
  t₁.Equiv t₂ → t₁.getGT? k = t₂.getGT? k
-- Init.Data.BitVec.Bitblast
BitVec.getLsbD_add_add_bool : ∀ {w i : ℕ},
  i < w →
    ∀ (x y : BitVec w) (c : Bool),
      (x + y + BitVec.setWidth w (BitVec.ofBool c)).getLsbD i = (x.getLsbD i ^^ (y.getLsbD i ^^ BitVec.carry i x y c))
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.Code.seq.sizeOf_spec : ∀ (action : Lean.Syntax) (k : Lean.Elab.Term.Do.Code),
  sizeOf (Lean.Elab.Term.Do.Code.seq action k) = 1 + sizeOf action + sizeOf k
-- Mathlib.Analysis.Normed.Group.Completion
UniformSpace.Completion.norm_coe : ∀ {E : Type u_2} [inst : SeminormedAddCommGroup E] (x : E), ‖↑x‖ = ‖x‖
-- Lean.Environment
Lean.ImportStateM : Type → Type
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
IsDedekindDomain.primesOver_finite : ∀ {A : Type u_4} [inst : CommRing A] (p : Ideal A) [hpm : p.IsMaximal] (B : Type u_5) [inst_1 : CommRing B]
  [IsDedekindDomain B] [inst_3 : Algebra A B] [IsDomain A] [Module.IsTorsionFree A B] [Algebra.IsIntegral A B],
  (p.primesOver B).Finite
-- Mathlib.Algebra.Order.Group.Lattice
add_inf : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : AddGroup α] [AddLeftMono α] (a b c : α), c + a ⊓ b = (c + a) ⊓ (c + b)
-- Mathlib.Algebra.Order.GroupWithZero.Basic
/-- Equality holds when `c ≠ 0`. See `mul_div_mul_right`.  -/
le_mul_div_mul_right : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : Preorder G₀] {a b c : G₀}, a / b ≤ 0 → a / b ≤ a * c / (b * c)
-- Mathlib.Topology.Order.MonotoneConvergence
tendsto_atBot_of_antitone : ∀ {ι : Type u_3} {α : Type u_4} [inst : Preorder ι] [inst_1 : TopologicalSpace α]
  [inst_2 : ConditionallyCompleteLinearOrder α] [OrderTopology α] {f : ι → α},
  Antitone f → Filter.Tendsto f Filter.atBot Filter.atTop ∨ ∃ l, Filter.Tendsto f Filter.atBot (nhds l)
-- Mathlib.MeasureTheory.Measure.Regular
MeasureTheory.Measure.Regular.comap' : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α] [BorelSpace α]
  {mβ : MeasurableSpace β} [inst_3 : TopologicalSpace β] [BorelSpace β] (μ : MeasureTheory.Measure β) [μ.Regular]
  {f : α → β}, Topology.IsOpenEmbedding f → (MeasureTheory.Measure.comap f μ).Regular
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.maxKey_alter_eq_self : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp] {k : α}
  {f : Option β → Option β} {he : (Std.DTreeMap.Const.alter t k f).isEmpty = false},
  (Std.DTreeMap.Const.alter t k f).maxKey he = k ↔
    (f (Std.DTreeMap.Const.get? t k)).isSome = true ∧ ∀ k' ∈ t, (cmp k' k).isLE = true
-- Mathlib.CategoryTheory.Limits.Opposites
/-- Turn a colimit for `F : Jᵒᵖ ⥤ C` into a limit for `F.rightOp : J ⥤ Cᵒᵖ`.  -/
CategoryTheory.Limits.isLimitConeRightOpOfCocone : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} J] →
        (F : CategoryTheory.Functor Jᵒᵖ C) →
          {c : CategoryTheory.Limits.Cocone F} →
            CategoryTheory.Limits.IsColimit c →
              CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.coneRightOpOfCocone c)
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
/-- A sheaf of modules is quasi-coherent if it is locally the cokernel of a
morphism between coproducts of copies of the sheaf of rings.  -/
SheafOfModules.isQuasicoherent : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      (R : CategoryTheory.Sheaf J RingCat) →
        [∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] →
          [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] →
            CategoryTheory.ObjectProperty (SheafOfModules R)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.mulMonC_nc.go.induct_unfolding : ∀ (k : ℤ) (m : Lean.Grind.CommRing.Mon) (c : ℕ)
  (motive : Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly → Prop),
  (∀ (acc : Lean.Grind.CommRing.Poly) (k_1 : ℤ),
      motive (Lean.Grind.CommRing.Poly.num k_1) acc (Lean.Grind.CommRing.Poly.insert (k * k_1 % ↑c) m acc)) →
    (∀ (acc : Lean.Grind.CommRing.Poly) (k_1 : ℤ) (m_1 : Lean.Grind.CommRing.Mon) (p : Lean.Grind.CommRing.Poly),
        motive p (Lean.Grind.CommRing.Poly.insert (k * k_1 % ↑c) (m.mul_nc m_1) acc)
            (Lean.Grind.CommRing.Poly.mulMonC_nc.go k m c p
              (Lean.Grind.CommRing.Poly.insert (k * k_1 % ↑c) (m.mul_nc m_1) acc)) →
          motive (Lean.Grind.CommRing.Poly.add k_1 m_1 p) acc
            (Lean.Grind.CommRing.Poly.mulMonC_nc.go k m c p
              (Lean.Grind.CommRing.Poly.insert (k * k_1 % ↑c) (m.mul_nc m_1) acc))) →
      ∀ (p acc : Lean.Grind.CommRing.Poly), motive p acc (Lean.Grind.CommRing.Poly.mulMonC_nc.go k m c p acc)
-- Init.Data.Array.Lemmas
Array.map_push : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {as : Array α} {x : α},
  Array.map f (as.push x) = (Array.map f as).push (f x)
-- Init.Data.List.Find
List.lookup_singleton : ∀ {α : Type u_1} [inst : BEq α] {c a b : α}, List.lookup c [(a, b)] = if (c == a) = true then some b else none
-- Mathlib.Algebra.GroupWithZero.Units.Basic
isUnit_zero_iff : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀], IsUnit 0 ↔ 0 = 1
-- Mathlib.Topology.Compactness.CompactlyCoherentSpace
/-- If every set `A` is closed if for every compact `K` the intersection `K ∩ A` is closed in `K`,
then the space is a compactly coherent space.  -/
CompactlyCoherentSpace.of_isClosed : ∀ {X : Type u} [inst : TopologicalSpace X],
  (∀ (A : Set X), (∀ (K : Set X), IsCompact K → IsClosed (Subtype.val ⁻¹' A)) → IsClosed A) → CompactlyCoherentSpace X
-- Mathlib.Algebra.Group.Action.Pi
Pi.smulCommClass'' : ∀ {ι : Type u_1} {α : ι → Type u_4} {β : ι → Type u_5} {γ : ι → Type u_6} [inst : (i : ι) → SMul (β i) (γ i)]
  [inst_1 : (i : ι) → SMul (α i) (γ i)] [∀ (i : ι), SMulCommClass (α i) (β i) (γ i)],
  SMulCommClass ((i : ι) → α i) ((i : ι) → β i) ((i : ι) → γ i)
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
/-- Recursion principle for a normalised EDS: if we have
* `P 0`, `P 1`, `P 2`, `P 3`, and `P 4`,
* for all `m : ℕ` we can prove `P (2 * (m + 3))` from `P (m + 1)`, `P (m + 2)`, `P (m + 3)`,
  `P (m + 4)`, and `P (m + 5)`, and
* for all `m : ℕ` we can prove `P (2 * (m + 2) + 1)` from `P (m + 1)`, `P (m + 2)`, `P (m + 3)`,
  and `P (m + 4)`,

then we have `P n` for all `n : ℕ`.  -/
normEDSRec : {P : ℕ → Sort u_4} →
  P 0 →
    P 1 →
      P 2 →
        P 3 →
          P 4 →
            ((m : ℕ) → P (m + 1) → P (m + 2) → P (m + 3) → P (m + 4) → P (m + 5) → P (2 * (m + 3))) →
              ((m : ℕ) → P (m + 1) → P (m + 2) → P (m + 3) → P (m + 4) → P (2 * (m + 2) + 1)) → (n : ℕ) → P n
-- Init.Data.Option.Lemmas
Option.filter_join : ∀ {α : Type u_1} {p : α → Bool} {o : Option (Option α)}, Option.filter p o.join = (Option.filter (Option.any p) o).join
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toList_toArray_roc : ∀ {m n : ℕ}, (m<...=n).toArray.toList = (m<...=n).toList
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.mapRange_zero : ∀ {ι : Type u} {β₁ : ι → Type v₁} {β₂ : ι → Type v₂} [inst : (i : ι) → Zero (β₁ i)] [inst_1 : (i : ι) → Zero (β₂ i)]
  (f : (i : ι) → β₁ i → β₂ i) (hf : ∀ (i : ι), f i 0 = 0), DFinsupp.mapRange f hf 0 = 0
-- Mathlib.Algebra.Group.Submonoid.Units
AddSubgroup.mem_ofAddUnits : ∀ {M : Type u_1} [inst : AddMonoid M] (S : AddSubgroup (AddUnits M)) {x : M} {y : AddUnits M},
  y ∈ S → ↑y = x → x ∈ S.ofAddUnits
-- Mathlib.Analysis.Normed.Group.Real
nnnorm_norm : ∀ {E : Type u_5} [inst : SeminormedAddCommGroup E] (x : E), ‖‖x‖‖₊ = ‖x‖₊
-- Lean.Parser.Term
Lean.Parser.Term.clear.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
MultipliableLocallyUniformlyOn.multipliableUniformlyOn_of_isCompact : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : CommMonoid α] {f : ι → β → α} {s : Set β}
  [inst_1 : UniformSpace α] [inst_2 : TopologicalSpace β],
  MultipliableLocallyUniformlyOn f s → IsCompact s → MultipliableUniformlyOn f s
-- Mathlib.CategoryTheory.Abelian.Injective.Resolution
CategoryTheory.InjectiveResolution.iso_hom_naturality_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasInjectiveResolutions C] {X Y : C} (f : X ⟶ Y) (I : CategoryTheory.InjectiveResolution X)
  (J : CategoryTheory.InjectiveResolution Y) (φ : I.cocomplex ⟶ J.cocomplex),
  CategoryTheory.CategoryStruct.comp (I.ι.f 0) (φ.f 0) = CategoryTheory.CategoryStruct.comp f (J.ι.f 0) →
    ∀ {Z : HomotopyCategory C (ComplexShape.up ℕ)}
      (h : (HomotopyCategory.quotient C (ComplexShape.up ℕ)).obj J.cocomplex ⟶ Z),
      CategoryTheory.CategoryStruct.comp ((CategoryTheory.injectiveResolutions C).map f)
          (CategoryTheory.CategoryStruct.comp J.iso.hom h) =
        CategoryTheory.CategoryStruct.comp I.iso.hom
          (CategoryTheory.CategoryStruct.comp ((HomotopyCategory.quotient C (ComplexShape.up ℕ)).map φ) h)
-- Mathlib.RingTheory.AdicCompletion.Functoriality
/-- Adic completion of `R^n` is `(AdicCompletion I R)^n`.  -/
AdicCompletion.piEquivFin : {R : Type u_1} →
  [inst : CommRing R] →
    (I : Ideal R) → (n : ℕ) → AdicCompletion I (Fin n → R) ≃ₗ[AdicCompletion I R] Fin n → AdicCompletion I R
-- Std.Time.Zoned.Database.Windows
Std.Time.Database.WindowsDb.mk : Std.Time.Database.WindowsDb
-- Mathlib.Logic.Equiv.Basic
/-- If the outer subtype has more restrictive predicate than the inner one,
then we can drop the latter.  -/
Equiv.subtypeSubtypeEquivSubtype : {α : Type u_9} → {p q : α → Prop} → (∀ {x : α}, q x → p x) → { x // q ↑x } ≃ Subtype q
-- Std.Time.Date.Unit.Weekday
Std.Time.Weekday.friday.sizeOf_spec : sizeOf Std.Time.Weekday.friday = 1
-- Mathlib.RingTheory.Coalgebra.Equiv
CoalgEquiv.coe_ofCoalgHom : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid A]
  [inst_2 : AddCommMonoid B] [inst_3 : Module R A] [inst_4 : Module R B] [inst_5 : CoalgebraStruct R A]
  [inst_6 : CoalgebraStruct R B] (f : A →ₗc[R] B) (g : B →ₗc[R] A) (h₁ : f.comp g = CoalgHom.id R B)
  (h₂ : g.comp f = CoalgHom.id R A), ↑(CoalgEquiv.ofCoalgHom f g h₁ h₂) = f
-- Mathlib.Analysis.Fourier.AddCircle
fourierCoeffOn.eq_1 : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {a b : ℝ} (hab : a < b) (f : ℝ → E) (n : ℤ),
  fourierCoeffOn hab f n = fourierCoeff (AddCircle.liftIoc (b - a) a f) n
-- Mathlib.Algebra.Homology.SpectralObject.Page
/-- For any morphism `f : i ⟶ j`, this is the isomorphism from
`E^n₁(𝟙 i, f, 𝟙 j)` to `H^n₁(f)`.  -/
CategoryTheory.Abelian.SpectralObject.EIsoH : {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 j : ι} →
              (f : i ⟶ j) →
                (n₀ n₁ n₂ : ℤ) →
                  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.EIsoH._auto_1) →
                    (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.EIsoH._auto_3) →
                      X.E (CategoryTheory.CategoryStruct.id i) f (CategoryTheory.CategoryStruct.id j) n₀ n₁ n₂ hn₁ hn₂ ≅
                        (X.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ f)
-- Init.Data.Range.Polymorphic.SInt
Int64.le.eq_1 : ∀ (a b : Int64), a.le b = (a.toBitVec.sle b.toBitVec = true)
-- Mathlib.Topology.Connected.Basic
/-- The closure of a connected set is connected as well.  -/
IsConnected.closure : ∀ {α : Type u} [inst : TopologicalSpace α] {s : Set α}, IsConnected s → IsConnected (closure s)
-- Mathlib.Data.Int.Basic
Int.natCast_dvd : ∀ {n : ℤ} {m : ℕ}, ↑m ∣ n ↔ m ∣ n.natAbs