awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Filtration
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
F : I.Filtration M
n₀ : ℕ
H :
  ∀ (i : ℕ),
    (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M) ⊆
      (↑(Submodule.span (↥(reesAlgebra I))
            (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))) :
        Set (PolynomialModule R M))
n : ℕ
hn : n ≥ n₀
x : M
hx : x ∈ F.N (n + 1)
l :
  Finsupp.{u_2, u_1}
    (↑(⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)) : Type u_2)
    ↥(reesAlgebra I)
hl :
  (((Finsupp.linearCombination (↥(reesAlgebra I))
                (Subtype.val (p := fun (x : PolynomialModule R M) ↦
                  Membership.mem (γ := Set (PolynomialModule R M))
                    (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))
                    x)) :
              (a :
                  (↑(⋃ (i : ℕ),
                          ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)) :
                      Type u_2) →₀
                    ↥(reesAlgebra I)) →
                PolynomialModule R M)
            l :
          PolynomialModule R M) :
        (a : ℕ) → M)
      (n + 1) =
    x
mp :
  (l.sum
      fun
        (a₁ :
          (↑(⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)) :
            Type u_2))
        (b : ↥(reesAlgebra I)) ↦
      (b • (↑a₁ : PolynomialModule R M) : (a : ℕ) → M) (n + 1)) ∈
    I • F.N n
⊢ x ∈ I • F.N n

Tactic:
rw [← hl, Finsupp.linearCombination_apply, Finsupp.sum_apply]

Premises used: Finsupp.linearCombination_apply, Finsupp.sum_apply
-- Module: Mathlib.RingTheory.Filtration
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
F : I.Filtration M
n₀ : ℕ
H :
  ∀ (i : ℕ),
    (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M) ⊆
      (↑(Submodule.span (↥(reesAlgebra I))
            (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))) :
        Set (PolynomialModule R M))
n : ℕ
hn : n ≥ n₀
x : M
hx : x ∈ F.N (n + 1)
l :
  Finsupp.{u_2, u_1}
    (↑(⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)) : Type u_2)
    ↥(reesAlgebra I)
hl :
  (((Finsupp.linearCombination (↥(reesAlgebra I))
                (Subtype.val (p := fun (x : PolynomialModule R M) ↦
                  Membership.mem (γ := Set (PolynomialModule R M))
                    (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))
                    x)) :
              (a :
                  (↑(⋃ (i : ℕ),
                          ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)) :
                      Type u_2) →₀
                    ↥(reesAlgebra I)) →
                PolynomialModule R M)
            l :
          PolynomialModule R M) :
        (a : ℕ) → M)
      (n + 1) =
    x
apply :
  ∀ c ∈ l.support,
    (fun
            (a₁ :
              (↑(⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)) :
                Type u_2))
            (b : ↥(reesAlgebra I)) ↦
          ((b • (↑a₁ : PolynomialModule R M) : (a : ℕ) → M) (n + 1) : M))
        c
        ((l :
            (a :
                (↑(⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)) :
                  Type u_2)) →
              ↥(reesAlgebra I))
          c) ∈
      I • F.N n
⊢ (l.sum
      fun
        (a₁ :
          (↑(⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)) :
            Type u_2))
        (b : ↥(reesAlgebra I)) ↦
      (b • (↑a₁ : PolynomialModule R M) : (a : ℕ) → M) (n + 1)) ∈
    I • F.N n

Tactic:
apply Submodule.sum_mem _ _

Premises used: Submodule.sum_mem
-- Module: Mathlib.RingTheory.Filtration
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
F : I.Filtration M
n₀ : ℕ
H :
  ∀ (i : ℕ),
    (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M) ⊆
      (↑(Submodule.span (↥(reesAlgebra I))
            (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))) :
        Set (PolynomialModule R M))
n : ℕ
hn : n ≥ n₀
x : M
hx : x ∈ F.N (n + 1)
l :
  Finsupp.{u_2, u_1}
    (↑(⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)) : Type u_2)
    ↥(reesAlgebra I)
hl :
  (((Finsupp.linearCombination (↥(reesAlgebra I))
                (Subtype.val (p := fun (x : PolynomialModule R M) ↦
                  Membership.mem (γ := Set (PolynomialModule R M))
                    (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))
                    x)) :
              (a :
                  (↑(⋃ (i : ℕ),
                          ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)) :
                      Type u_2) →₀
                    ↥(reesAlgebra I)) →
                PolynomialModule R M)
            l :
          PolynomialModule R M) :
        (a : ℕ) → M)
      (n + 1) =
    x
n' : ℕ
hn' : n' ≤ n₀
m : M
hm : m ∈ (↑(F.N n') : Set M)
⊢ n' ≤ n + 1

Tactic:
lia
-- Module: Mathlib.RingTheory.Filtration
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
F : I.Filtration M
n₀ : ℕ
H :
  ∀ (i : ℕ),
    (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M) ⊆
      (↑(Submodule.span (↥(reesAlgebra I))
            (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))) :
        Set (PolynomialModule R M))
n : ℕ
hn : n ≥ n₀
x : M
hx : x ∈ F.N (n + 1)
l :
  Finsupp.{u_2, u_1}
    (↑(⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)) : Type u_2)
    ↥(reesAlgebra I)
hl :
  (((Finsupp.linearCombination (↥(reesAlgebra I))
                (Subtype.val (p := fun (x : PolynomialModule R M) ↦
                  Membership.mem (γ := Set (PolynomialModule R M))
                    (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))
                    x)) :
              (a :
                  (↑(⋃ (i : ℕ),
                          ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)) :
                      Type u_2) →₀
                    ↥(reesAlgebra I)) →
                PolynomialModule R M)
            l :
          PolynomialModule R M) :
        (a : ℕ) → M)
      (n + 1) =
    x
n' : ℕ
hn' : n' ≤ n₀
m : M
hm : m ∈ (↑(F.N n') : Set M)
⊢ n' ≤ n

Tactic:
lia
-- Module: Mathlib.RingTheory.Filtration
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
F : I.Filtration M
n₀ : ℕ
H :
  ∀ (i : ℕ),
    (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M) ⊆
      (↑(Submodule.span (↥(reesAlgebra I))
            (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))) :
        Set (PolynomialModule R M))
n : ℕ
hn : n ≥ n₀
x : M
hx : x ∈ F.N (n + 1)
l :
  Finsupp.{u_2, u_1}
    (↑(⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)) : Type u_2)
    ↥(reesAlgebra I)
hl :
  (((Finsupp.linearCombination (↥(reesAlgebra I))
                (Subtype.val (p := fun (x : PolynomialModule R M) ↦
                  Membership.mem (γ := Set (PolynomialModule R M))
                    (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))
                    x)) :
              (a :
                  (↑(⋃ (i : ℕ),
                          ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)) :
                      Type u_2) →₀
                    ↥(reesAlgebra I)) →
                PolynomialModule R M)
            l :
          PolynomialModule R M) :
        (a : ℕ) → M)
      (n + 1) =
    x
n' : ℕ
hn' : n' ≤ n₀
m : M
hm : m ∈ (↑(F.N n') : Set M)
⊢ n' ≤ n

Tactic:
have e : n' ≤ n := by lia
-- Module: Mathlib.RingTheory.Filtration
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
F : I.Filtration M
n₀ : ℕ
H :
  ∀ (i : ℕ),
    (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M) ⊆
      (↑(Submodule.span (↥(reesAlgebra I))
            (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))) :
        Set (PolynomialModule R M))
n : ℕ
hn : n ≥ n₀
x : M
hx : x ∈ F.N (n + 1)
l :
  Finsupp.{u_2, u_1}
    (↑(⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)) : Type u_2)
    ↥(reesAlgebra I)
hl :
  (((Finsupp.linearCombination (↥(reesAlgebra I))
                (Subtype.val (p := fun (x : PolynomialModule R M) ↦
                  Membership.mem (γ := Set (PolynomialModule R M))
                    (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))
                    x)) :
              (a :
                  (↑(⋃ (i : ℕ),
                          ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)) :
                      Type u_2) →₀
                    ↥(reesAlgebra I)) →
                PolynomialModule R M)
            l :
          PolynomialModule R M) :
        (a : ℕ) → M)
      (n + 1) =
    x
n' : ℕ
hn' : n' ≤ n₀
m : M
hm : m ∈ (↑(F.N n') : Set M)
e : n' ≤ n
⊢ I ^ (n - n' + 1) • F.N n' ≤ HPow.hPow (β := ℕ) I 1 • F.N (n - n' + n')

Tactic:
have := F.pow_smul_le_pow_smul (n - n') n' 1
-- Module: Mathlib.RingTheory.Filtration
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
F : I.Filtration M
n₀ : ℕ
H :
  ∀ (i : ℕ),
    (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M) ⊆
      (↑(Submodule.span (↥(reesAlgebra I))
            (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))) :
        Set (PolynomialModule R M))
n : ℕ
hn : n ≥ n₀
x : M
hx : x ∈ F.N (n + 1)
l :
  Finsupp.{u_2, u_1}
    (↑(⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)) : Type u_2)
    ↥(reesAlgebra I)
hl :
  (((Finsupp.linearCombination (↥(reesAlgebra I))
                (Subtype.val (p := fun (x : PolynomialModule R M) ↦
                  Membership.mem (γ := Set (PolynomialModule R M))
                    (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))
                    x)) :
              (a :
                  (↑(⋃ (i : ℕ),
                          ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)) :
                      Type u_2) →₀
                    ↥(reesAlgebra I)) →
                PolynomialModule R M)
            l :
          PolynomialModule R M) :
        (a : ℕ) → M)
      (n + 1) =
    x
n' : ℕ
hn' : n' ≤ n₀
m : M
hm : m ∈ (↑(F.N n') : Set M)
e : n' ≤ n
this : I ^ (n - n' + 1) • F.N n' ≤ HPow.hPow (β := ℕ) I 1 • F.N (n - n' + n')
⊢ I ^ (n + 1 - n') • F.N n' ≤ I • F.N n

Tactic:
rw [tsub_add_cancel_of_le e, pow_one, add_comm _ 1, ← add_tsub_assoc_of_le e, add_comm] at this

Premises used: add_tsub_assoc_of_le, tsub_add_cancel_of_le, add_comm, pow_one, OfNat.ofNat
-- Module: Mathlib.RingTheory.Filtration
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
F : I.Filtration M
n₀ : ℕ
H :
  ∀ (i : ℕ),
    (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M) ⊆
      (↑(Submodule.span (↥(reesAlgebra I))
            (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))) :
        Set (PolynomialModule R M))
n : ℕ
hn : n ≥ n₀
x : M
hx : x ∈ F.N (n + 1)
l :
  Finsupp.{u_2, u_1}
    (↑(⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)) : Type u_2)
    ↥(reesAlgebra I)
hl :
  (((Finsupp.linearCombination (↥(reesAlgebra I))
                (Subtype.val (p := fun (x : PolynomialModule R M) ↦
                  Membership.mem (γ := Set (PolynomialModule R M))
                    (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))
                    x)) :
              (a :
                  (↑(⋃ (i : ℕ),
                          ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)) :
                      Type u_2) →₀
                    ↥(reesAlgebra I)) →
                PolynomialModule R M)
            l :
          PolynomialModule R M) :
        (a : ℕ) → M)
      (n + 1) =
    x
n' : ℕ
hn' : n' ≤ n₀
m : M
hm : m ∈ (↑(F.N n') : Set M)
e : n' ≤ n
this : I ^ (n + 1 - n') • F.N n' ≤ I • F.N n
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := R)
      (coeff
        (↑((l :
                (a :
                    (↑(⋃ (i : ℕ),
                          ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)) :
                      Type u_2)) →
                  ↥(reesAlgebra I))
              (Subtype.mk (p := fun (x : PolynomialModule R M) ↦
                Membership.mem (γ := Set (PolynomialModule R M))
                  (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)) x)
                ((single R n' : (a : M) → PolynomialModule R M) m) ⋯)) :
          R[X])
        (n + 1 - n'))
      m ∈
    I • F.N n

Tactic:
this (Submodule.smul_mem_smul ((l _).2 <| n + 1 - n') hm)

Premises used: HSub.hSub, HAdd.hAdd, Submodule.smul_mem_smul, OfNat.ofNat, DFunLike.coe, Subtype.property
-- Module: Mathlib.RingTheory.Filtration
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
F : I.Filtration M
n₀ : ℕ
H :
  ∀ (i : ℕ),
    (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M) ⊆
      (↑(Submodule.span (↥(reesAlgebra I))
            (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))) :
        Set (PolynomialModule R M))
n : ℕ
hn : n ≥ n₀
x : M
hx : x ∈ F.N (n + 1)
l :
  Finsupp.{u_2, u_1}
    (↑(⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)) : Type u_2)
    ↥(reesAlgebra I)
hl :
  (((Finsupp.linearCombination (↥(reesAlgebra I))
                (Subtype.val (p := fun (x : PolynomialModule R M) ↦
                  Membership.mem (γ := Set (PolynomialModule R M))
                    (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))
                    x)) :
              (a :
                  (↑(⋃ (i : ℕ),
                          ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)) :
                      Type u_2) →₀
                    ↥(reesAlgebra I)) →
                PolynomialModule R M)
            l :
          PolynomialModule R M) :
        (a : ℕ) → M)
      (n + 1) =
    x
n' : ℕ
hn' : n' ≤ n₀
m : M
hm : m ∈ (↑(F.N n') : Set M)
e : n' ≤ n
this : I ^ (n + 1 - n') • F.N n' ≤ I • F.N n
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := R)
      (coeff
        (↑((l :
                (a :
                    (↑(⋃ (i : ℕ),
                          ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)) :
                      Type u_2)) →
                  ↥(reesAlgebra I))
              (Subtype.mk (p := fun (x : PolynomialModule R M) ↦
                Membership.mem (γ := Set (PolynomialModule R M))
                  (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)) x)
                ((single R n' : (a : M) → PolynomialModule R M) m) ⋯)) :
          R[X])
        (n + 1 - n'))
      m ∈
    I • F.N n

Tactic:
exact this (Submodule.smul_mem_smul ((l _).2 <| n + 1 - n') hm)

Premises used: HSub.hSub, HAdd.hAdd, Submodule.smul_mem_smul, OfNat.ofNat, DFunLike.coe, Subtype.property
-- Module: Mathlib.RingTheory.Filtration
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
F : I.Filtration M
n₀ : ℕ
F' : Submodule.{u_1, u_2} (↥(reesAlgebra I)) (PolynomialModule R M) :=
  Submodule.span (↥(reesAlgebra I))
    (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))
hF : ∀ n ≥ n₀, I • F.N n = F.N (n + 1)
i : ℕ
⊢ ∀ i ≤ n₀, (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M) ⊆ (↑F' : Set (PolynomialModule R M))

Tactic:
have : ∀ i ≤ n₀, single R i '' (F.N i : Set M) ⊆ F' := fun i hi =>
      -- Porting note: need to add hint for `s`
      (Set.subset_iUnion₂ (s := fun i _ => (single R i '' (N F i : Set M))) i hi).trans
        Submodule.subset_span
-- Module: Mathlib.RingTheory.Filtration
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
F : I.Filtration M
n₀ : ℕ
F' : Submodule.{u_1, u_2} (↥(reesAlgebra I)) (PolynomialModule R M) :=
  Submodule.span (↥(reesAlgebra I))
    (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))
hF : ∀ n ≥ n₀, I • F.N n = F.N (n + 1)
this :
  ∀ i ≤ n₀, (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M) ⊆ (↑F' : Set (PolynomialModule R M))
⊢ (⇑(single R 0) : (a : M) → PolynomialModule R M) '' (↑(F.N 0) : Set M) ⊆
    (↑(Submodule.span (↥(reesAlgebra I))
          (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))) :
      Set (PolynomialModule R M))

Tactic:
this _ zero_le

Premises used: zero_le
-- Module: Mathlib.RingTheory.Filtration
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
F : I.Filtration M
n₀ : ℕ
F' : Submodule.{u_1, u_2} (↥(reesAlgebra I)) (PolynomialModule R M) :=
  Submodule.span (↥(reesAlgebra I))
    (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))
hF : ∀ n ≥ n₀, I • F.N n = F.N (n + 1)
this :
  ∀ i ≤ n₀, (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M) ⊆ (↑F' : Set (PolynomialModule R M))
⊢ (⇑(single R 0) : (a : M) → PolynomialModule R M) '' (↑(F.N 0) : Set M) ⊆
    (↑(Submodule.span (↥(reesAlgebra I))
          (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))) :
      Set (PolynomialModule R M))

Tactic:
exact this _ zero_le

Premises used: zero_le
-- Module: Mathlib.RingTheory.Filtration
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
F : I.Filtration M
n₀ : ℕ
F' : Submodule.{u_1, u_2} (↥(reesAlgebra I)) (PolynomialModule R M) :=
  Submodule.span (↥(reesAlgebra I))
    (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))
hF : ∀ n ≥ n₀, I • F.N n = F.N (n + 1)
this :
  ∀ i ≤ n₀, (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M) ⊆ (↑F' : Set (PolynomialModule R M))
j : ℕ
hj :
  (⇑(single R j) : (a : M) → PolynomialModule R M) '' (↑(F.N j) : Set M) ⊆
    (↑(Submodule.span (↥(reesAlgebra I))
          (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))) :
      Set (PolynomialModule R M))
⊢ (⇑(single R (j + 1)) : (a : M) → PolynomialModule R M) '' (↑(F.N (j + 1)) : Set M) ⊆
    (↑(Submodule.span (↥(reesAlgebra I))
          (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))) :
      Set (PolynomialModule R M))

Tactic:
?_
-- Module: Mathlib.RingTheory.Filtration
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
F : I.Filtration M
n₀ : ℕ
F' : Submodule.{u_1, u_2} (↥(reesAlgebra I)) (PolynomialModule R M) :=
  Submodule.span (↥(reesAlgebra I))
    (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))
hF : ∀ n ≥ n₀, I • F.N n = F.N (n + 1)
i : ℕ
this :
  ∀ i ≤ n₀, (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M) ⊆ (↑F' : Set (PolynomialModule R M))
mpr :
  ∀ (j : ℕ)
    (hj :
      (⇑(single R j) : (a : M) → PolynomialModule R M) '' (↑(F.N j) : Set M) ⊆
        (↑(Submodule.span (↥(reesAlgebra I))
              (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))) :
          Set (PolynomialModule R M))),
    (⇑(single R (j + 1)) : (a : M) → PolynomialModule R M) '' (↑(F.N (j + 1)) : Set M) ⊆
      (↑(Submodule.span (↥(reesAlgebra I))
            (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))) :
        Set (PolynomialModule R M))
⊢ (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M) ⊆
    (↑(Submodule.span (↥(reesAlgebra I))
          (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))) :
      Set (PolynomialModule R M))

Tactic:
induction i with
    | zero => exact this _ zero_le
    | succ j hj => ?_

Premises used: zero_le
-- Module: Mathlib.RingTheory.Filtration
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
F : I.Filtration M
n₀ : ℕ
F' : Submodule.{u_1, u_2} (↥(reesAlgebra I)) (PolynomialModule R M) :=
  Submodule.span (↥(reesAlgebra I))
    (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))
hF : ∀ n ≥ n₀, I • F.N n = F.N (n + 1)
this :
  ∀ i ≤ n₀, (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M) ⊆ (↑F' : Set (PolynomialModule R M))
j : ℕ
hj :
  (⇑(single R j) : (a : M) → PolynomialModule R M) '' (↑(F.N j) : Set M) ⊆
    (↑(Submodule.span (↥(reesAlgebra I))
          (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))) :
      Set (PolynomialModule R M))
pos :
  ∀ (hj' : j.succ ≤ n₀),
    (⇑(single R (j + 1)) : (a : M) → PolynomialModule R M) '' (↑(F.N (j + 1)) : Set M) ⊆
      (↑(Submodule.span (↥(reesAlgebra I))
            (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))) :
        Set (PolynomialModule R M))
neg :
  ∀ (hj' : ¬j.succ ≤ n₀),
    (⇑(single R (j + 1)) : (a : M) → PolynomialModule R M) '' (↑(F.N (j + 1)) : Set M) ⊆
      (↑(Submodule.span (↥(reesAlgebra I))
            (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))) :
        Set (PolynomialModule R M))
⊢ (⇑(single R (j + 1)) : (a : M) → PolynomialModule R M) '' (↑(F.N (j + 1)) : Set M) ⊆
    (↑(Submodule.span (↥(reesAlgebra I))
          (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))) :
      Set (PolynomialModule R M))

Tactic:
by_cases hj' : j.succ ≤ n₀

Premises used: Nat.succ