R✝ : Type ?u.23931
M✝ : Type ?u.23934
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
hn : ∃ S, Set.Finite S ∧ span R S = N
hin : N ≤ I • N
⊢ ∃ r, r - 1 ∈ I ∧ ∀ (n : M), n ∈ N → r • n = 0
R✝ : Type ?u.23931
M✝ : Type ?u.23934
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
hn : FG N
hin : N ≤ I • N
⊢ ∃ r, r - 1 ∈ I ∧ ∀ (n : M), n ∈ N → r • n = 0
rw [fg_def] at hn
case intro.intro
R✝ : Type ?u.23931
M✝ : Type ?u.23934
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
hin : N ≤ I • N
s : Set M
hfs : Set.Finite s
hs : span R s = N
⊢ ∃ r, r - 1 ∈ I ∧ ∀ (n : M), n ∈ N → r • n = 0
R✝ : Type ?u.23931
M✝ : Type ?u.23934
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
hn : ∃ S, Set.Finite S ∧ span R S = N
hin : N ≤ I • N
⊢ ∃ r, r - 1 ∈ I ∧ ∀ (n : M), n ∈ N → r • n = 0
rcases hn with ⟨s, hfs, hs⟩
case intro.intro
R✝ : Type ?u.23931
M✝ : Type ?u.23934
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s : Set M
hfs : Set.Finite s
this : ∃ r, r - 1 ∈ I ∧ N ≤ comap (↑(LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N
⊢ ∃ r, r - 1 ∈ I ∧ ∀ (n : M), n ∈ N → r • n = 0
case intro.intro
R✝ : Type ?u.23931
M✝ : Type ?u.23934
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
hin : N ≤ I • N
s : Set M
hfs : Set.Finite s
hs : span R s = N
this : ∃ r, r - 1 ∈ I ∧ N ≤ comap (↑(LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N
⊢ ∃ r, r - 1 ∈ I ∧ ∀ (n : M), n ∈ N → r • n = 0
clear hin hs
case intro.intro
R✝ : Type ?u.23931
M✝ : Type ?u.23934
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s : Set M
hfs : Set.Finite s
⊢ (∃ r, r - 1 ∈ I ∧ N ≤ comap (↑(LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N) →
    ∃ r, r - 1 ∈ I ∧ ∀ (n : M), n ∈ N → r • n = 0
case intro.intro
R✝ : Type ?u.23931
M✝ : Type ?u.23934
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s : Set M
hfs : Set.Finite s
this : ∃ r, r - 1 ∈ I ∧ N ≤ comap (↑(LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N
⊢ ∃ r, r - 1 ∈ I ∧ ∀ (n : M), n ∈ N → r • n = 0
revert this
case intro.intro.refine'_1
R✝ : Type ?u.23931
M✝ : Type ?u.23934
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s : Set M
hfs : Set.Finite s
H : ∃ r, r - 1 ∈ I ∧ N ≤ comap (↑(LinearMap.lsmul R M) r) (I • span R ∅) ∧ ∅ ⊆ ↑N
⊢ ∃ r, r - 1 ∈ I ∧ ∀ (n : M), n ∈ N → r • n = 0

case intro.intro.refine'_2
R✝ : Type ?u.23931
M✝ : Type ?u.23934
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s✝ : Set M
hfs : Set.Finite s✝
i : M
s : Set M
x✝¹ : ¬i ∈ s
x✝ : Set.Finite s
ih :
  (∃ r, r - 1 ∈ I ∧ N ≤ comap (↑(LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N) →
    ∃ r, r - 1 ∈ I ∧ ∀ (n : M), n ∈ N → r • n = 0
H : ∃ r, r - 1 ∈ I ∧ N ≤ comap (↑(LinearMap.lsmul R M) r) (I • span R (insert i s)) ∧ insert i s ⊆ ↑N
⊢ ∃ r, r - 1 ∈ I ∧ ∀ (n : M), n ∈ N → r • n = 0
case intro.intro
R✝ : Type ?u.23931
M✝ : Type ?u.23934
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s : Set M
hfs : Set.Finite s
⊢ (∃ r, r - 1 ∈ I ∧ N ≤ comap (↑(LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N) →
    ∃ r, r - 1 ∈ I ∧ ∀ (n : M), n ∈ N → r • n = 0
refine' Set.Finite.dinduction_on _ hfs (fun H => _) @fun i s _ _ ih H => _
case intro.intro.refine'_2
R✝ : Type ?u.23931
M✝ : Type ?u.23934
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s✝ : Set M
hfs : Set.Finite s✝
i : M
s : Set M
x✝¹ : ¬i ∈ s
x✝ : Set.Finite s
ih :
  (∃ r, r - 1 ∈ I ∧ N ≤ comap (↑(LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N) →
    ∃ r, r - 1 ∈ I ∧ ∀ (n : M), n ∈ N → r • n = 0
H : ∃ r, r - 1 ∈ I ∧ N ≤ comap (↑(LinearMap.lsmul R M) r) (I • span R (insert i s)) ∧ insert i s ⊆ ↑N
⊢ ∃ r, r - 1 ∈ I ∧ N ≤ comap (↑(LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N
case intro.intro.refine'_2
R✝ : Type ?u.23931
M✝ : Type ?u.23934
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s✝ : Set M
hfs : Set.Finite s✝
i : M
s : Set M
x✝¹ : ¬i ∈ s
x✝ : Set.Finite s
ih :
  (∃ r, r - 1 ∈ I ∧ N ≤ comap (↑(LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N) →
    ∃ r, r - 1 ∈ I ∧ ∀ (n : M), n ∈ N → r • n = 0
H : ∃ r, r - 1 ∈ I ∧ N ≤ comap (↑(LinearMap.lsmul R M) r) (I • span R (insert i s)) ∧ insert i s ⊆ ↑N
⊢ ∃ r, r - 1 ∈ I ∧ ∀ (n : M), n ∈ N → r • n = 0
apply ih
case intro.intro.refine'_2.intro.intro.intro
R✝ : Type ?u.23931
M✝ : Type ?u.23934
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s✝ : Set M
hfs : Set.Finite s✝
i : M
s : Set M
x✝¹ : ¬i ∈ s
x✝ : Set.Finite s
ih :
  (∃ r, r - 1 ∈ I ∧ N ≤ comap (↑(LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N) →
    ∃ r, r - 1 ∈ I ∧ ∀ (n : M), n ∈ N → r • n = 0
r : R
hr1 : r - 1 ∈ I
hrn : N ≤ comap (↑(LinearMap.lsmul R M) r) (I • span R (insert i s))
hs : insert i s ⊆ ↑N
⊢ ∃ r, r - 1 ∈ I ∧ N ≤ comap (↑(LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N
case intro.intro.refine'_2
R✝ : Type ?u.23931
M✝ : Type ?u.23934
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s✝ : Set M
hfs : Set.Finite s✝
i : M
s : Set M
x✝¹ : ¬i ∈ s
x✝ : Set.Finite s
ih :
  (∃ r, r - 1 ∈ I ∧ N ≤ comap (↑(LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N) →
    ∃ r, r - 1 ∈ I ∧ ∀ (n : M), n ∈ N → r • n = 0
H : ∃ r, r - 1 ∈ I ∧ N ≤ comap (↑(LinearMap.lsmul R M) r) (I • span R (insert i s)) ∧ insert i s ⊆ ↑N
⊢ ∃ r, r - 1 ∈ I ∧ N ≤ comap (↑(LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N
rcases H with ⟨r, hr1, hrn, hs⟩
case intro.intro.refine'_2.intro.intro.intro
R✝ : Type ?u.23931
M✝ : Type ?u.23934
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s✝ : Set M
hfs : Set.Finite s✝
i : M
s : Set M
x✝¹ : ¬i ∈ s
x✝ : Set.Finite s
ih :
  (∃ r, r - 1 ∈ I ∧ N ≤ comap (↑(LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N) →
    ∃ r, r - 1 ∈ I ∧ ∀ (n : M), n ∈ N → r • n = 0
r : R
hr1 : r - 1 ∈ I
hrn : N ≤ comap (↑(LinearMap.lsmul R M) r) (I • span R {i} ⊔ I • span R s)
hs : insert i s ⊆ ↑N
⊢ ∃ r, r - 1 ∈ I ∧ N ≤ comap (↑(LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N
case intro.intro.refine'_2.intro.intro.intro
R✝ : Type ?u.23931
M✝ : Type ?u.23934
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s✝ : Set M
hfs : Set.Finite s✝
i : M
s : Set M
x✝¹ : ¬i ∈ s
x✝ : Set.Finite s
ih :
  (∃ r, r - 1 ∈ I ∧ N ≤ comap (↑(LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N) →
    ∃ r, r - 1 ∈ I ∧ ∀ (n : M), n ∈ N → r • n = 0
r : R
hr1 : r - 1 ∈ I
hrn : N ≤ comap (↑(LinearMap.lsmul R M) r) (I • span R (insert i s))
hs : insert i s ⊆ ↑N
⊢ ∃ r, r - 1 ∈ I ∧ N ≤ comap (↑(LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N
rw [← Set.singleton_union, span_union, smul_sup] at hrn
case intro.intro.refine'_2.intro.intro.intro
R✝ : Type ?u.23931
M✝ : Type ?u.23934
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s✝ : Set M
hfs : Set.Finite s✝
i : M
s : Set M
x✝¹ : ¬i ∈ s
x✝ : Set.Finite s
ih :
  (∃ r, r - 1 ∈ I ∧ N ≤ comap (↑(LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N) →
    ∃ r, r - 1 ∈ I ∧ ∀ (n : M), n ∈ N → r • n = 0
r : R
hr1 : r - 1 ∈ I
hrn : N ≤ comap (↑(LinearMap.lsmul R M) r) (I • span R {i} ⊔ I • span R s)
hs : i ∈ ↑N ∧ s ⊆ ↑N
⊢ ∃ r, r - 1 ∈ I ∧ N ≤ comap (↑(LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N
case intro.intro.refine'_2.intro.intro.intro
R✝ : Type ?u.23931
M✝ : Type ?u.23934
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s✝ : Set M
hfs : Set.Finite s✝
i : M
s : Set M
x✝¹ : ¬i ∈ s
x✝ : Set.Finite s
ih :
  (∃ r, r - 1 ∈ I ∧ N ≤ comap (↑(LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N) →
    ∃ r, r - 1 ∈ I ∧ ∀ (n : M), n ∈ N → r • n = 0
r : R
hr1 : r - 1 ∈ I
hrn : N ≤ comap (↑(LinearMap.lsmul R M) r) (I • span R {i} ⊔ I • span R s)
hs : insert i s ⊆ ↑N
⊢ ∃ r, r - 1 ∈ I ∧ N ≤ comap (↑(LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N
rw [Set.insert_subset] at hs
case intro.intro.refine'_2.intro.intro.intro.intro.intro
R✝ : Type ?u.23931
M✝ : Type ?u.23934
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s✝ : Set M
hfs : Set.Finite s✝
i : M
s : Set M
x✝¹ : ¬i ∈ s
x✝ : Set.Finite s
ih :
  (∃ r, r - 1 ∈ I ∧ N ≤ comap (↑(LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N) →
    ∃ r, r - 1 ∈ I ∧ ∀ (n : M), n ∈ N → r • n = 0
r : R
hr1 : r - 1 ∈ I
hrn : N ≤ comap (↑(LinearMap.lsmul R M) r) (I • span R {i} ⊔ I • span R s)
hs : i ∈ ↑N ∧ s ⊆ ↑N
c : R
hc1 : c - 1 ∈ I
hci : c • i ∈ I • span R s
⊢ ∃ r, r - 1 ∈ I ∧ N ≤ comap (↑(LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N
case intro.intro.refine'_2.intro.intro.intro
R✝ : Type ?u.23931
M✝ : Type ?u.23934
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s✝ : Set M
hfs : Set.Finite s✝
i : M
s : Set M
x✝¹ : ¬i ∈ s
x✝ : Set.Finite s
ih :
  (∃ r, r - 1 ∈ I ∧ N ≤ comap (↑(LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N) →
    ∃ r, r - 1 ∈ I ∧ ∀ (n : M), n ∈ N → r • n = 0
r : R
hr1 : r - 1 ∈ I
hrn : N ≤ comap (↑(LinearMap.lsmul R M) r) (I • span R {i} ⊔ I • span R s)
hs : i ∈ ↑N ∧ s ⊆ ↑N
this : ∃ c, c - 1 ∈ I ∧ c • i ∈ I • span R s
⊢ ∃ r, r - 1 ∈ I ∧ N ≤ comap (↑(LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N
rcases this with ⟨c, hc1, hci⟩
case intro.intro.refine'_2.intro.intro.intro.intro.intro.refine'_1
R✝ : Type ?u.23931
M✝ : Type ?u.23934
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s✝ : Set M
hfs : Set.Finite s✝
i : M
s : Set M
x✝¹ : ¬i ∈ s
x✝ : Set.Finite s
ih :
  (∃ r, r - 1 ∈ I ∧ N ≤ comap (↑(LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N) →
    ∃ r, r - 1 ∈ I ∧ ∀ (n : M), n ∈ N → r • n = 0
r : R
hr1 : r - 1 ∈ I
hrn : N ≤ comap (↑(LinearMap.lsmul R M) r) (I • span R {i} ⊔ I • span R s)
hs : i ∈ ↑N ∧ s ⊆ ↑N
c : R
hc1 : c - 1 ∈ I
hci : c • i ∈ I • span R s
⊢ c * r - 1 ∈ I

case intro.intro.refine'_2.intro.intro.intro.intro.intro.refine'_2
R✝ : Type ?u.23931
M✝ : Type ?u.23934
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s✝ : Set M
hfs : Set.Finite s✝
i : M
s : Set M
x✝¹ : ¬i ∈ s
x✝ : Set.Finite s
ih :
  (∃ r, r - 1 ∈ I ∧ N ≤ comap (↑(LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N) →
    ∃ r, r - 1 ∈ I ∧ ∀ (n : M), n ∈ N → r • n = 0
r : R
hr1 : r - 1 ∈ I
hrn : N ≤ comap (↑(LinearMap.lsmul R M) r) (I • span R {i} ⊔ I • span R s)
hs : i ∈ ↑N ∧ s ⊆ ↑N
c : R
hc1 : c - 1 ∈ I
hci : c • i ∈ I • span R s
⊢ N ≤ comap (↑(LinearMap.lsmul R M) (c * r)) (I • span R s)
case intro.intro.refine'_2.intro.intro.intro.intro.intro
R✝ : Type ?u.23931
M✝ : Type ?u.23934
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s✝ : Set M
hfs : Set.Finite s✝
i : M
s : Set M
x✝¹ : ¬i ∈ s
x✝ : Set.Finite s
ih :
  (∃ r, r - 1 ∈ I ∧ N ≤ comap (↑(LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N) →
    ∃ r, r - 1 ∈ I ∧ ∀ (n : M), n ∈ N → r • n = 0
r : R
hr1 : r - 1 ∈ I
hrn : N ≤ comap (↑(LinearMap.lsmul R M) r) (I • span R {i} ⊔ I • span R s)
hs : i ∈ ↑N ∧ s ⊆ ↑N
c : R
hc1 : c - 1 ∈ I
hci : c • i ∈ I • span R s
⊢ ∃ r, r - 1 ∈ I ∧ N ≤ comap (↑(LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N
refine' ⟨c * r, _, _, hs.2⟩
case refine'_1
R✝ : Type ?u.23931
M✝ : Type ?u.23934
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
hin : N ≤ I • N
s : Set M
hfs : Set.Finite s
hs : span R s = N
⊢ 1 - 1 ∈ I

case refine'_2
R✝ : Type ?u.23931
M✝ : Type ?u.23934
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
hin : N ≤ I • N
s : Set M
hfs : Set.Finite s
hs : span R s = N
⊢ N ≤ comap (↑(LinearMap.lsmul R M) 1) (I • span R s)

case refine'_3
R✝ : Type ?u.23931
M✝ : Type ?u.23934
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
hin : N ≤ I • N
s : Set M
hfs : Set.Finite s
hs : span R s = N
⊢ s ⊆ ↑N
R✝ : Type ?u.23931
M✝ : Type ?u.23934
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
hin : N ≤ I • N
s : Set M
hfs : Set.Finite s
hs : span R s = N
⊢ ∃ r, r - 1 ∈ I ∧ N ≤ comap (↑(LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N
refine' ⟨1, _, _, _⟩
case refine'_1
R✝ : Type ?u.23931
M✝ : Type ?u.23934
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
hin : N ≤ I • N
s : Set M
hfs : Set.Finite s
hs : span R s = N
⊢ 0 ∈ I
case refine'_1
R✝ : Type ?u.23931
M✝ : Type ?u.23934
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
hin : N ≤ I • N
s : Set M
hfs : Set.Finite s
hs : span R s = N
⊢ 1 - 1 ∈ I
rw [sub_self]
no goals
case refine'_1
R✝ : Type ?u.23931
M✝ : Type ?u.23934
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
hin : N ≤ I • N
s : Set M
hfs : Set.Finite s
hs : span R s = N
⊢ 0 ∈ I
exact I.zero_mem
case refine'_2
R✝ : Type ?u.23931
M✝ : Type ?u.23934
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
hin : N ≤ I • N
s : Set M
hfs : Set.Finite s
hs : span R s = N
⊢ N ≤ comap (↑(LinearMap.lsmul R M) 1) (I • N)
case refine'_2
R✝ : Type ?u.23931
M✝ : Type ?u.23934
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
hin : N ≤ I • N
s : Set M
hfs : Set.Finite s
hs : span R s = N
⊢ N ≤ comap (↑(LinearMap.lsmul R M) 1) (I • span R s)
rw [hs]
case refine'_2
R✝ : Type ?u.23931
M✝ : Type ?u.23934
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
hin : N ≤ I • N
s : Set M
hfs : Set.Finite s
hs : span R s = N
n : M
hn : n ∈ N
⊢ n ∈ comap (↑(LinearMap.lsmul R M) 1) (I • N)
case refine'_2
R✝ : Type ?u.23931
M✝ : Type ?u.23934
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
hin : N ≤ I • N
s : Set M
hfs : Set.Finite s
hs : span R s = N
⊢ N ≤ comap (↑(LinearMap.lsmul R M) 1) (I • N)
intro n hn
case refine'_2
R✝ : Type ?u.23931
M✝ : Type ?u.23934
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
hin : N ≤ I • N
s : Set M
hfs : Set.Finite s
hs : span R s = N
n : M
hn : n ∈ N
⊢ ↑(↑(LinearMap.lsmul R M) 1) n ∈ I • N
case refine'_2
R✝ : Type ?u.23931
M✝ : Type ?u.23934
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
hin : N ≤ I • N
s : Set M
hfs : Set.Finite s
hs : span R s = N
n : M
hn : n ∈ N
⊢ n ∈ comap (↑(LinearMap.lsmul R M) 1) (I • N)
rw [mem_comap]
case refine'_2
R✝ : Type ?u.23931
M✝ : Type ?u.23934
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
hin : N ≤ I • N
s : Set M
hfs : Set.Finite s
hs : span R s = N
n : M
hn : n ∈ N
⊢ 1 • n ∈ I • N
case refine'_2
R✝ : Type ?u.23931
M✝ : Type ?u.23934
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
hin : N ≤ I • N
s : Set M
hfs : Set.Finite s
hs : span R s = N
n : M
hn : n ∈ N
⊢ ↑(↑(LinearMap.lsmul R M) 1) n ∈ I • N
change (1 : R) • n ∈ I • N
case refine'_2
R✝ : Type ?u.23931
M✝ : Type ?u.23934
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
hin : N ≤ I • N
s : Set M
hfs : Set.Finite s
hs : span R s = N
n : M
hn : n ∈ N
⊢ n ∈ I • N
case refine'_2
R✝ : Type ?u.23931
M✝ : Type ?u.23934
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
hin : N ≤ I • N
s : Set M
hfs : Set.Finite s
hs : span R s = N
n : M
hn : n ∈ N
⊢ 1 • n ∈ I • N
rw [one_smul]
no goals
case refine'_2
R✝ : Type ?u.23931
M✝ : Type ?u.23934
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
hin : N ≤ I • N
s : Set M
hfs : Set.Finite s
hs : span R s = N
n : M
hn : n ∈ N
⊢ n ∈ I • N
exact hin hn
no goals
case refine'_3
R✝ : Type ?u.23931
M✝ : Type ?u.23934
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
hin : N ≤ I • N
s : Set M
hfs : Set.Finite s
hs : span R s = N
⊢ s ⊆ ↑N
rw [← span_le, hs]
case intro.intro.refine'_1.intro.intro.intro
R✝ : Type ?u.23931
M✝ : Type ?u.23934
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s : Set M
hfs : Set.Finite s
r : R
hr1 : r - 1 ∈ I
hrn : N ≤ comap (↑(LinearMap.lsmul R M) r) (I • span R ∅)
right✝ : ∅ ⊆ ↑N
⊢ ∃ r, r - 1 ∈ I ∧ ∀ (n : M), n ∈ N → r • n = 0
case intro.intro.refine'_1
R✝ : Type ?u.23931
M✝ : Type ?u.23934
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s : Set M
hfs : Set.Finite s
H : ∃ r, r - 1 ∈ I ∧ N ≤ comap (↑(LinearMap.lsmul R M) r) (I • span R ∅) ∧ ∅ ⊆ ↑N
⊢ ∃ r, r - 1 ∈ I ∧ ∀ (n : M), n ∈ N → r • n = 0
rcases H with ⟨r, hr1, hrn, _⟩
case intro.intro.refine'_1.intro.intro.intro
R✝ : Type ?u.23931
M✝ : Type ?u.23934
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s : Set M
hfs : Set.Finite s
r : R
hr1 : r - 1 ∈ I
hrn : N ≤ comap (↑(LinearMap.lsmul R M) r) (I • span R ∅)
right✝ : ∅ ⊆ ↑N
n : M
hn : n ∈ N
⊢ r • n = 0
case intro.intro.refine'_1.intro.intro.intro
R✝ : Type ?u.23931
M✝ : Type ?u.23934
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s : Set M
hfs : Set.Finite s
r : R
hr1 : r - 1 ∈ I
hrn : N ≤ comap (↑(LinearMap.lsmul R M) r) (I • span R ∅)
right✝ : ∅ ⊆ ↑N
⊢ ∃ r, r - 1 ∈ I ∧ ∀ (n : M), n ∈ N → r • n = 0
refine' ⟨r, hr1, fun n hn => _⟩
case intro.intro.refine'_1.intro.intro.intro
R✝ : Type ?u.23931
M✝ : Type ?u.23934
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s : Set M
hfs : Set.Finite s
r : R
hr1 : r - 1 ∈ I
right✝ : ∅ ⊆ ↑N
n : M
hn : n ∈ N
hrn : n ∈ comap (↑(LinearMap.lsmul R M) r) (I • span R ∅)
⊢ r • n = 0
case intro.intro.refine'_1.intro.intro.intro
R✝ : Type ?u.23931
M✝ : Type ?u.23934
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s : Set M
hfs : Set.Finite s
r : R
hr1 : r - 1 ∈ I
hrn : N ≤ comap (↑(LinearMap.lsmul R M) r) (I • span R ∅)
right✝ : ∅ ⊆ ↑N
n : M
hn : n ∈ N
⊢ r • n = 0
specialize hrn hn
no goals
case intro.intro.refine'_1.intro.intro.intro
R✝ : Type ?u.23931
M✝ : Type ?u.23934
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s : Set M
hfs : Set.Finite s
r : R
hr1 : r - 1 ∈ I
right✝ : ∅ ⊆ ↑N
n : M
hn : n ∈ N
hrn : n ∈ comap (↑(LinearMap.lsmul R M) r) (I • span R ∅)
⊢ r • n = 0
rwa [mem_comap, span_empty, smul_bot, mem_bot] at hrn
R✝ : Type ?u.23931
M✝ : Type ?u.23934
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s✝ : Set M
hfs : Set.Finite s✝
i : M
s : Set M
x✝¹ : ¬i ∈ s
x✝ : Set.Finite s
ih :
  (∃ r, r - 1 ∈ I ∧ N ≤ comap (↑(LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N) →
    ∃ r, r - 1 ∈ I ∧ ∀ (n : M), n ∈ N → r • n = 0
r : R
hr1 : r - 1 ∈ I
hs : i ∈ ↑N ∧ s ⊆ ↑N
hrn : i ∈ comap (↑(LinearMap.lsmul R M) r) (I • span R {i} ⊔ I • span R s)
⊢ ∃ c, c - 1 ∈ I ∧ c • i ∈ I • span R s
R✝ : Type ?u.23931
M✝ : Type ?u.23934
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s✝ : Set M
hfs : Set.Finite s✝
i : M
s : Set M
x✝¹ : ¬i ∈ s
x✝ : Set.Finite s
ih :
  (∃ r, r - 1 ∈ I ∧ N ≤ comap (↑(LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N) →
    ∃ r, r - 1 ∈ I ∧ ∀ (n : M), n ∈ N → r • n = 0
r : R
hr1 : r - 1 ∈ I
hrn : N ≤ comap (↑(LinearMap.lsmul R M) r) (I • span R {i} ⊔ I • span R s)
hs : i ∈ ↑N ∧ s ⊆ ↑N
⊢ ∃ c, c - 1 ∈ I ∧ c • i ∈ I • span R s
specialize hrn hs.1
R✝ : Type ?u.23931
M✝ : Type ?u.23934
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s✝ : Set M
hfs : Set.Finite s✝
i : M
s : Set M
x✝¹ : ¬i ∈ s
x✝ : Set.Finite s
ih :
  (∃ r, r - 1 ∈ I ∧ N ≤ comap (↑(LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N) →
    ∃ r, r - 1 ∈ I ∧ ∀ (n : M), n ∈ N → r • n = 0
r : R
hr1 : r - 1 ∈ I
hs : i ∈ ↑N ∧ s ⊆ ↑N
hrn : ∃ y, y ∈ I • span R {i} ∧ ∃ z, z ∈ I • span R s ∧ y + z = ↑(↑(LinearMap.lsmul R M) r) i
⊢ ∃ c, c - 1 ∈ I ∧ c • i ∈ I • span R s
R✝ : Type ?u.23931
M✝ : Type ?u.23934
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s✝ : Set M
hfs : Set.Finite s✝
i : M
s : Set M
x✝¹ : ¬i ∈ s
x✝ : Set.Finite s
ih :
  (∃ r, r - 1 ∈ I ∧ N ≤ comap (↑(LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N) →
    ∃ r, r - 1 ∈ I ∧ ∀ (n : M), n ∈ N → r • n = 0
r : R
hr1 : r - 1 ∈ I
hs : i ∈ ↑N ∧ s ⊆ ↑N
hrn : i ∈ comap (↑(LinearMap.lsmul R M) r) (I • span R {i} ⊔ I • span R s)
⊢ ∃ c, c - 1 ∈ I ∧ c • i ∈ I • span R s
rw [mem_comap, mem_sup] at hrn
case intro.intro.intro.intro
R✝ : Type ?u.23931
M✝ : Type ?u.23934
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s✝ : Set M
hfs : Set.Finite s✝
i : M
s : Set M
x✝¹ : ¬i ∈ s
x✝ : Set.Finite s
ih :
  (∃ r, r - 1 ∈ I ∧ N ≤ comap (↑(LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N) →
    ∃ r, r - 1 ∈ I ∧ ∀ (n : M), n ∈ N → r • n = 0
r : R
hr1 : r - 1 ∈ I
hs : i ∈ ↑N ∧ s ⊆ ↑N
y : M
hy : y ∈ I • span R {i}
z : M
hz : z ∈ I • span R s
hyz : y + z = ↑(↑(LinearMap.lsmul R M) r) i
⊢ ∃ c, c - 1 ∈ I ∧ c • i ∈ I • span R s
R✝ : Type ?u.23931
M✝ : Type ?u.23934
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s✝ : Set M
hfs : Set.Finite s✝
i : M
s : Set M
x✝¹ : ¬i ∈ s
x✝ : Set.Finite s
ih :
  (∃ r, r - 1 ∈ I ∧ N ≤ comap (↑(LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N) →
    ∃ r, r - 1 ∈ I ∧ ∀ (n : M), n ∈ N → r • n = 0
r : R
hr1 : r - 1 ∈ I
hs : i ∈ ↑N ∧ s ⊆ ↑N
hrn : ∃ y, y ∈ I • span R {i} ∧ ∃ z, z ∈ I • span R s ∧ y + z = ↑(↑(LinearMap.lsmul R M) r) i
⊢ ∃ c, c - 1 ∈ I ∧ c • i ∈ I • span R s
rcases hrn with ⟨y, hy, z, hz, hyz⟩
case intro.intro.intro.intro
R✝ : Type ?u.23931
M✝ : Type ?u.23934
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s✝ : Set M
hfs : Set.Finite s✝
i : M
s : Set M
x✝¹ : ¬i ∈ s
x✝ : Set.Finite s
ih :
  (∃ r, r - 1 ∈ I ∧ N ≤ comap (↑(LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N) →
    ∃ r, r - 1 ∈ I ∧ ∀ (n : M), n ∈ N → r • n = 0
r : R
hr1 : r - 1 ∈ I
hs : i ∈ ↑N ∧ s ⊆ ↑N
y : M
hy : y ∈ I • span R {i}
z : M
hz : z ∈ I • span R s
hyz : y + z = r • i
⊢ ∃ c, c - 1 ∈ I ∧ c • i ∈ I • span R s
case intro.intro.intro.intro
R✝ : Type ?u.23931
M✝ : Type ?u.23934
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s✝ : Set M
hfs : Set.Finite s✝
i : M
s : Set M
x✝¹ : ¬i ∈ s
x✝ : Set.Finite s
ih :
  (∃ r, r - 1 ∈ I ∧ N ≤ comap (↑(LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N) →
    ∃ r, r - 1 ∈ I ∧ ∀ (n : M), n ∈ N → r • n = 0
r : R
hr1 : r - 1 ∈ I
hs : i ∈ ↑N ∧ s ⊆ ↑N
y : M
hy : y ∈ I • span R {i}
z : M
hz : z ∈ I • span R s
hyz : y + z = ↑(↑(LinearMap.lsmul R M) r) i
⊢ ∃ c, c - 1 ∈ I ∧ c • i ∈ I • span R s
dsimp at hyz
case intro.intro.intro.intro
R✝ : Type ?u.23931
M✝ : Type ?u.23934
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s✝ : Set M
hfs : Set.Finite s✝
i : M
s : Set M
x✝¹ : ¬i ∈ s
x✝ : Set.Finite s
ih :
  (∃ r, r - 1 ∈ I ∧ N ≤ comap (↑(LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N) →
    ∃ r, r - 1 ∈ I ∧ ∀ (n : M), n ∈ N → r • n = 0
r : R
hr1 : r - 1 ∈ I
hs : i ∈ ↑N ∧ s ⊆ ↑N
y : M
hy : ∃ y_1, y_1 ∈ I ∧ y_1 • i = y
z : M
hz : z ∈ I • span R s
hyz : y + z = r • i
⊢ ∃ c, c - 1 ∈ I ∧ c • i ∈ I • span R s
case intro.intro.intro.intro
R✝ : Type ?u.23931
M✝ : Type ?u.23934
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s✝ : Set M
hfs : Set.Finite s✝
i : M
s : Set M
x✝¹ : ¬i ∈ s
x✝ : Set.Finite s
ih :
  (∃ r, r - 1 ∈ I ∧ N ≤ comap (↑(LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N) →
    ∃ r, r - 1 ∈ I ∧ ∀ (n : M), n ∈ N → r • n = 0
r : R
hr1 : r - 1 ∈ I
hs : i ∈ ↑N ∧ s ⊆ ↑N
y : M
hy : y ∈ I • span R {i}
z : M
hz : z ∈ I • span R s
hyz : y + z = r • i
⊢ ∃ c, c - 1 ∈ I ∧ c • i ∈ I • span R s
rw [mem_smul_span_singleton] at hy
case intro.intro.intro.intro.intro.intro
R✝ : Type ?u.23931
M✝ : Type ?u.23934
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s✝ : Set M
hfs : Set.Finite s✝
i : M
s : Set M
x✝¹ : ¬i ∈ s
x✝ : Set.Finite s
ih :
  (∃ r, r - 1 ∈ I ∧ N ≤ comap (↑(LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N) →
    ∃ r, r - 1 ∈ I ∧ ∀ (n : M), n ∈ N → r • n = 0
r : R
hr1 : r - 1 ∈ I
hs : i ∈ ↑N ∧ s ⊆ ↑N
z : M
hz : z ∈ I • span R s
c : R
hci : c ∈ I
hyz : c • i + z = r • i
⊢ ∃ c, c - 1 ∈ I ∧ c • i ∈ I • span R s
case intro.intro.intro.intro
R✝ : Type ?u.23931
M✝ : Type ?u.23934
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s✝ : Set M
hfs : Set.Finite s✝
i : M
s : Set M
x✝¹ : ¬i ∈ s
x✝ : Set.Finite s
ih :
  (∃ r, r - 1 ∈ I ∧ N ≤ comap (↑(LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N) →
    ∃ r, r - 1 ∈ I ∧ ∀ (n : M), n ∈ N → r • n = 0
r : R
hr1 : r - 1 ∈ I
hs : i ∈ ↑N ∧ s ⊆ ↑N
y : M
hy : ∃ y_1, y_1 ∈ I ∧ y_1 • i = y
z : M
hz : z ∈ I • span R s
hyz : y + z = r • i
⊢ ∃ c, c - 1 ∈ I ∧ c • i ∈ I • span R s
rcases hy with ⟨c, hci, rfl⟩
case intro.intro.intro.intro.intro.intro
R✝ : Type ?u.23931
M✝ : Type ?u.23934
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s✝ : Set M
hfs : Set.Finite s✝
i : M
s : Set M
x✝¹ : ¬i ∈ s
x✝ : Set.Finite s
ih :
  (∃ r, r - 1 ∈ I ∧ N ≤ comap (↑(LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N) →
    ∃ r, r - 1 ∈ I ∧ ∀ (n : M), n ∈ N → r • n = 0
r : R
hr1 : r - 1 ∈ I
hs : i ∈ ↑N ∧ s ⊆ ↑N
z : M
hz : z ∈ I • span R s
c : R
hci : c ∈ I
hyz : c • i + z = r • i
⊢ r - c - 1 ∈ I ∧ (r - c) • i ∈ I • span R s
case intro.intro.intro.intro.intro.intro
R✝ : Type ?u.23931
M✝ : Type ?u.23934
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s✝ : Set M
hfs : Set.Finite s✝
i : M
s : Set M
x✝¹ : ¬i ∈ s
x✝ : Set.Finite s
ih :
  (∃ r, r - 1 ∈ I ∧ N ≤ comap (↑(LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N) →
    ∃ r, r - 1 ∈ I ∧ ∀ (n : M), n ∈ N → r • n = 0
r : R
hr1 : r - 1 ∈ I
hs : i ∈ ↑N ∧ s ⊆ ↑N
z : M
hz : z ∈ I • span R s
c : R
hci : c ∈ I
hyz : c • i + z = r • i
⊢ ∃ c, c - 1 ∈ I ∧ c • i ∈ I • span R s
use r - c
case intro.intro.intro.intro.intro.intro.left
R✝ : Type ?u.23931
M✝ : Type ?u.23934
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s✝ : Set M
hfs : Set.Finite s✝
i : M
s : Set M
x✝¹ : ¬i ∈ s
x✝ : Set.Finite s
ih :
  (∃ r, r - 1 ∈ I ∧ N ≤ comap (↑(LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N) →
    ∃ r, r - 1 ∈ I ∧ ∀ (n : M), n ∈ N → r • n = 0
r : R
hr1 : r - 1 ∈ I
hs : i ∈ ↑N ∧ s ⊆ ↑N
z : M
hz : z ∈ I • span R s
c : R
hci : c ∈ I
hyz : c • i + z = r • i
⊢ r - c - 1 ∈ I

case intro.intro.intro.intro.intro.intro.right
R✝ : Type ?u.23931
M✝ : Type ?u.23934
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s✝ : Set M
hfs : Set.Finite s✝
i : M
s : Set M
x✝¹ : ¬i ∈ s
x✝ : Set.Finite s
ih :
  (∃ r, r - 1 ∈ I ∧ N ≤ comap (↑(LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N) →
    ∃ r, r - 1 ∈ I ∧ ∀ (n : M), n ∈ N → r • n = 0
r : R
hr1 : r - 1 ∈ I
hs : i ∈ ↑N ∧ s ⊆ ↑N
z : M
hz : z ∈ I • span R s
c : R
hci : c ∈ I
hyz : c • i + z = r • i
⊢ (r - c) • i ∈ I • span R s
case intro.intro.intro.intro.intro.intro
R✝ : Type ?u.23931
M✝ : Type ?u.23934
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s✝ : Set M
hfs : Set.Finite s✝
i : M
s : Set M
x✝¹ : ¬i ∈ s
x✝ : Set.Finite s
ih :
  (∃ r, r - 1 ∈ I ∧ N ≤ comap (↑(LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N) →
    ∃ r, r - 1 ∈ I ∧ ∀ (n : M), n ∈ N → r • n = 0
r : R
hr1 : r - 1 ∈ I
hs : i ∈ ↑N ∧ s ⊆ ↑N
z : M
hz : z ∈ I • span R s
c : R
hci : c ∈ I
hyz : c • i + z = r • i
⊢ r - c - 1 ∈ I ∧ (r - c) • i ∈ I • span R s
constructor
case intro.intro.intro.intro.intro.intro.left
R✝ : Type ?u.23931
M✝ : Type ?u.23934
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s✝ : Set M
hfs : Set.Finite s✝
i : M
s : Set M
x✝¹ : ¬i ∈ s
x✝ : Set.Finite s
ih :
  (∃ r, r - 1 ∈ I ∧ N ≤ comap (↑(LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N) →
    ∃ r, r - 1 ∈ I ∧ ∀ (n : M), n ∈ N → r • n = 0
r : R
hr1 : r - 1 ∈ I
hs : i ∈ ↑N ∧ s ⊆ ↑N
z : M
hz : z ∈ I • span R s
c : R
hci : c ∈ I
hyz : c • i + z = r • i
⊢ r - 1 - c ∈ I
case intro.intro.intro.intro.intro.intro.left
R✝ : Type ?u.23931
M✝ : Type ?u.23934
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s✝ : Set M
hfs : Set.Finite s✝
i : M
s : Set M
x✝¹ : ¬i ∈ s
x✝ : Set.Finite s
ih :
  (∃ r, r - 1 ∈ I ∧ N ≤ comap (↑(LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N) →
    ∃ r, r - 1 ∈ I ∧ ∀ (n : M), n ∈ N → r • n = 0
r : R
hr1 : r - 1 ∈ I
hs : i ∈ ↑N ∧ s ⊆ ↑N
z : M
hz : z ∈ I • span R s
c : R
hci : c ∈ I
hyz : c • i + z = r • i
⊢ r - c - 1 ∈ I
rw [sub_right_comm]
no goals
case intro.intro.intro.intro.intro.intro.left
R✝ : Type ?u.23931
M✝ : Type ?u.23934
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s✝ : Set M
hfs : Set.Finite s✝
i : M
s : Set M
x✝¹ : ¬i ∈ s
x✝ : Set.Finite s
ih :
  (∃ r, r - 1 ∈ I ∧ N ≤ comap (↑(LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N) →
    ∃ r, r - 1 ∈ I ∧ ∀ (n : M), n ∈ N → r • n = 0
r : R
hr1 : r - 1 ∈ I
hs : i ∈ ↑N ∧ s ⊆ ↑N
z : M
hz : z ∈ I • span R s
c : R
hci : c ∈ I
hyz : c • i + z = r • i
⊢ r - 1 - c ∈ I
exact I.sub_mem hr1 hci
case intro.intro.intro.intro.intro.intro.right
R✝ : Type ?u.23931
M✝ : Type ?u.23934
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s✝ : Set M
hfs : Set.Finite s✝
i : M
s : Set M
x✝¹ : ¬i ∈ s
x✝ : Set.Finite s
ih :
  (∃ r, r - 1 ∈ I ∧ N ≤ comap (↑(LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N) →
    ∃ r, r - 1 ∈ I ∧ ∀ (n : M), n ∈ N → r • n = 0
r : R
hr1 : r - 1 ∈ I
hs : i ∈ ↑N ∧ s ⊆ ↑N
z : M
hz : z ∈ I • span R s
c : R
hci : c ∈ I
hyz : c • i + z = r • i
⊢ z ∈ I • span R s
case intro.intro.intro.intro.intro.intro.right
R✝ : Type ?u.23931
M✝ : Type ?u.23934
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s✝ : Set M
hfs : Set.Finite s✝
i : M
s : Set M
x✝¹ : ¬i ∈ s
x✝ : Set.Finite s
ih :
  (∃ r, r - 1 ∈ I ∧ N ≤ comap (↑(LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N) →
    ∃ r, r - 1 ∈ I ∧ ∀ (n : M), n ∈ N → r • n = 0
r : R
hr1 : r - 1 ∈ I
hs : i ∈ ↑N ∧ s ⊆ ↑N
z : M
hz : z ∈ I • span R s
c : R
hci : c ∈ I
hyz : c • i + z = r • i
⊢ (r - c) • i ∈ I • span R s
rw [sub_smul, ← hyz, add_sub_cancel']
no goals
case intro.intro.intro.intro.intro.intro.right
R✝ : Type ?u.23931
M✝ : Type ?u.23934
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s✝ : Set M
hfs : Set.Finite s✝
i : M
s : Set M
x✝¹ : ¬i ∈ s
x✝ : Set.Finite s
ih :
  (∃ r, r - 1 ∈ I ∧ N ≤ comap (↑(LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N) →
    ∃ r, r - 1 ∈ I ∧ ∀ (n : M), n ∈ N → r • n = 0
r : R
hr1 : r - 1 ∈ I
hs : i ∈ ↑N ∧ s ⊆ ↑N
z : M
hz : z ∈ I • span R s
c : R
hci : c ∈ I
hyz : c • i + z = r • i
⊢ z ∈ I • span R s
exact hz
no goals
case intro.intro.refine'_2.intro.intro.intro.intro.intro.refine'_1
R✝ : Type ?u.23931
M✝ : Type ?u.23934
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s✝ : Set M
hfs : Set.Finite s✝
i : M
s : Set M
x✝¹ : ¬i ∈ s
x✝ : Set.Finite s
ih :
  (∃ r, r - 1 ∈ I ∧ N ≤ comap (↑(LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N) →
    ∃ r, r - 1 ∈ I ∧ ∀ (n : M), n ∈ N → r • n = 0
r : R
hr1 : r - 1 ∈ I
hrn : N ≤ comap (↑(LinearMap.lsmul R M) r) (I • span R {i} ⊔ I • span R s)
hs : i ∈ ↑N ∧ s ⊆ ↑N
c : R
hc1 : c - 1 ∈ I
hci : c • i ∈ I • span R s
⊢ c * r - 1 ∈ I
simpa only [mul_sub, mul_one, sub_add_sub_cancel] using I.add_mem (I.mul_mem_left c hr1) hc1
case intro.intro.refine'_2.intro.intro.intro.intro.intro.refine'_2
R✝ : Type ?u.23931
M✝ : Type ?u.23934
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s✝ : Set M
hfs : Set.Finite s✝
i : M
s : Set M
x✝¹ : ¬i ∈ s
x✝ : Set.Finite s
ih :
  (∃ r, r - 1 ∈ I ∧ N ≤ comap (↑(LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N) →
    ∃ r, r - 1 ∈ I ∧ ∀ (n : M), n ∈ N → r • n = 0
r : R
hr1 : r - 1 ∈ I
hrn : N ≤ comap (↑(LinearMap.lsmul R M) r) (I • span R {i} ⊔ I • span R s)
hs : i ∈ ↑N ∧ s ⊆ ↑N
c : R
hc1 : c - 1 ∈ I
hci : c • i ∈ I • span R s
n : M
hn : n ∈ N
⊢ n ∈ comap (↑(LinearMap.lsmul R M) (c * r)) (I • span R s)
case intro.intro.refine'_2.intro.intro.intro.intro.intro.refine'_2
R✝ : Type ?u.23931
M✝ : Type ?u.23934
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s✝ : Set M
hfs : Set.Finite s✝
i : M
s : Set M
x✝¹ : ¬i ∈ s
x✝ : Set.Finite s
ih :
  (∃ r, r - 1 ∈ I ∧ N ≤ comap (↑(LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N) →
    ∃ r, r - 1 ∈ I ∧ ∀ (n : M), n ∈ N → r • n = 0
r : R
hr1 : r - 1 ∈ I
hrn : N ≤ comap (↑(LinearMap.lsmul R M) r) (I • span R {i} ⊔ I • span R s)
hs : i ∈ ↑N ∧ s ⊆ ↑N
c : R
hc1 : c - 1 ∈ I
hci : c • i ∈ I • span R s
⊢ N ≤ comap (↑(LinearMap.lsmul R M) (c * r)) (I • span R s)
intro n hn
case intro.intro.refine'_2.intro.intro.intro.intro.intro.refine'_2
R✝ : Type ?u.23931
M✝ : Type ?u.23934
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s✝ : Set M
hfs : Set.Finite s✝
i : M
s : Set M
x✝¹ : ¬i ∈ s
x✝ : Set.Finite s
ih :
  (∃ r, r - 1 ∈ I ∧ N ≤ comap (↑(LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N) →
    ∃ r, r - 1 ∈ I ∧ ∀ (n : M), n ∈ N → r • n = 0
r : R
hr1 : r - 1 ∈ I
hs : i ∈ ↑N ∧ s ⊆ ↑N
c : R
hc1 : c - 1 ∈ I
hci : c • i ∈ I • span R s
n : M
hn : n ∈ N
hrn : n ∈ comap (↑(LinearMap.lsmul R M) r) (I • span R {i} ⊔ I • span R s)
⊢ n ∈ comap (↑(LinearMap.lsmul R M) (c * r)) (I • span R s)
case intro.intro.refine'_2.intro.intro.intro.intro.intro.refine'_2
R✝ : Type ?u.23931
M✝ : Type ?u.23934
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s✝ : Set M
hfs : Set.Finite s✝
i : M
s : Set M
x✝¹ : ¬i ∈ s
x✝ : Set.Finite s
ih :
  (∃ r, r - 1 ∈ I ∧ N ≤ comap (↑(LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N) →
    ∃ r, r - 1 ∈ I ∧ ∀ (n : M), n ∈ N → r • n = 0
r : R
hr1 : r - 1 ∈ I
hrn : N ≤ comap (↑(LinearMap.lsmul R M) r) (I • span R {i} ⊔ I • span R s)
hs : i ∈ ↑N ∧ s ⊆ ↑N
c : R
hc1 : c - 1 ∈ I
hci : c • i ∈ I • span R s
n : M
hn : n ∈ N
⊢ n ∈ comap (↑(LinearMap.lsmul R M) (c * r)) (I • span R s)
specialize hrn hn
case intro.intro.refine'_2.intro.intro.intro.intro.intro.refine'_2
R✝ : Type ?u.23931
M✝ : Type ?u.23934
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s✝ : Set M
hfs : Set.Finite s✝
i : M
s : Set M
x✝¹ : ¬i ∈ s
x✝ : Set.Finite s
ih :
  (∃ r, r - 1 ∈ I ∧ N ≤ comap (↑(LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N) →
    ∃ r, r - 1 ∈ I ∧ ∀ (n : M), n ∈ N → r • n = 0
r : R
hr1 : r - 1 ∈ I
hs : i ∈ ↑N ∧ s ⊆ ↑N
c : R
hc1 : c - 1 ∈ I
hci : c • i ∈ I • span R s
n : M
hn : n ∈ N
hrn : ∃ y, y ∈ I • span R {i} ∧ ∃ z, z ∈ I • span R s ∧ y + z = ↑(↑(LinearMap.lsmul R M) r) n
⊢ n ∈ comap (↑(LinearMap.lsmul R M) (c * r)) (I • span R s)
case intro.intro.refine'_2.intro.intro.intro.intro.intro.refine'_2
R✝ : Type ?u.23931
M✝ : Type ?u.23934
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s✝ : Set M
hfs : Set.Finite s✝
i : M
s : Set M
x✝¹ : ¬i ∈ s
x✝ : Set.Finite s
ih :
  (∃ r, r - 1 ∈ I ∧ N ≤ comap (↑(LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N) →
    ∃ r, r - 1 ∈ I ∧ ∀ (n : M), n ∈ N → r • n = 0
r : R
hr1 : r - 1 ∈ I
hs : i ∈ ↑N ∧ s ⊆ ↑N
c : R
hc1 : c - 1 ∈ I
hci : c • i ∈ I • span R s
n : M
hn : n ∈ N
hrn : n ∈ comap (↑(LinearMap.lsmul R M) r) (I • span R {i} ⊔ I • span R s)
⊢ n ∈ comap (↑(LinearMap.lsmul R M) (c * r)) (I • span R s)
rw [mem_comap, mem_sup] at hrn
case intro.intro.refine'_2.intro.intro.intro.intro.intro.refine'_2.intro.intro.intro.intro
R✝ : Type ?u.23931
M✝ : Type ?u.23934
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s✝ : Set M
hfs : Set.Finite s✝
i : M
s : Set M
x✝¹ : ¬i ∈ s
x✝ : Set.Finite s
ih :
  (∃ r, r - 1 ∈ I ∧ N ≤ comap (↑(LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N) →
    ∃ r, r - 1 ∈ I ∧ ∀ (n : M), n ∈ N → r • n = 0
r : R
hr1 : r - 1 ∈ I
hs : i ∈ ↑N ∧ s ⊆ ↑N
c : R
hc1 : c - 1 ∈ I
hci : c • i ∈ I • span R s
n : M
hn : n ∈ N
y : M
hy : y ∈ I • span R {i}
z : M
hz : z ∈ I • span R s
hyz : y + z = ↑(↑(LinearMap.lsmul R M) r) n
⊢ n ∈ comap (↑(LinearMap.lsmul R M) (c * r)) (I • span R s)
case intro.intro.refine'_2.intro.intro.intro.intro.intro.refine'_2
R✝ : Type ?u.23931
M✝ : Type ?u.23934
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s✝ : Set M
hfs : Set.Finite s✝
i : M
s : Set M
x✝¹ : ¬i ∈ s
x✝ : Set.Finite s
ih :
  (∃ r, r - 1 ∈ I ∧ N ≤ comap (↑(LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N) →
    ∃ r, r - 1 ∈ I ∧ ∀ (n : M), n ∈ N → r • n = 0
r : R
hr1 : r - 1 ∈ I
hs : i ∈ ↑N ∧ s ⊆ ↑N
c : R
hc1 : c - 1 ∈ I
hci : c • i ∈ I • span R s
n : M
hn : n ∈ N
hrn : ∃ y, y ∈ I • span R {i} ∧ ∃ z, z ∈ I • span R s ∧ y + z = ↑(↑(LinearMap.lsmul R M) r) n
⊢ n ∈ comap (↑(LinearMap.lsmul R M) (c * r)) (I • span R s)
rcases hrn with ⟨y, hy, z, hz, hyz⟩
case intro.intro.refine'_2.intro.intro.intro.intro.intro.refine'_2.intro.intro.intro.intro
R✝ : Type ?u.23931
M✝ : Type ?u.23934
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s✝ : Set M
hfs : Set.Finite s✝
i : M
s : Set M
x✝¹ : ¬i ∈ s
x✝ : Set.Finite s
ih :
  (∃ r, r - 1 ∈ I ∧ N ≤ comap (↑(LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N) →
    ∃ r, r - 1 ∈ I ∧ ∀ (n : M), n ∈ N → r • n = 0
r : R
hr1 : r - 1 ∈ I
hs : i ∈ ↑N ∧ s ⊆ ↑N
c : R
hc1 : c - 1 ∈ I
hci : c • i ∈ I • span R s
n : M
hn : n ∈ N
y : M
hy : y ∈ I • span R {i}
z : M
hz : z ∈ I • span R s
hyz : y + z = r • n
⊢ n ∈ comap (↑(LinearMap.lsmul R M) (c * r)) (I • span R s)
case intro.intro.refine'_2.intro.intro.intro.intro.intro.refine'_2.intro.intro.intro.intro
R✝ : Type ?u.23931
M✝ : Type ?u.23934
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s✝ : Set M
hfs : Set.Finite s✝
i : M
s : Set M
x✝¹ : ¬i ∈ s
x✝ : Set.Finite s
ih :
  (∃ r, r - 1 ∈ I ∧ N ≤ comap (↑(LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N) →
    ∃ r, r - 1 ∈ I ∧ ∀ (n : M), n ∈ N → r • n = 0
r : R
hr1 : r - 1 ∈ I
hs : i ∈ ↑N ∧ s ⊆ ↑N
c : R
hc1 : c - 1 ∈ I
hci : c • i ∈ I • span R s
n : M
hn : n ∈ N
y : M
hy : y ∈ I • span R {i}
z : M
hz : z ∈ I • span R s
hyz : y + z = ↑(↑(LinearMap.lsmul R M) r) n
⊢ n ∈ comap (↑(LinearMap.lsmul R M) (c * r)) (I • span R s)
dsimp at hyz
case intro.intro.refine'_2.intro.intro.intro.intro.intro.refine'_2.intro.intro.intro.intro
R✝ : Type ?u.23931
M✝ : Type ?u.23934
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s✝ : Set M
hfs : Set.Finite s✝
i : M
s : Set M
x✝¹ : ¬i ∈ s
x✝ : Set.Finite s
ih :
  (∃ r, r - 1 ∈ I ∧ N ≤ comap (↑(LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N) →
    ∃ r, r - 1 ∈ I ∧ ∀ (n : M), n ∈ N → r • n = 0
r : R
hr1 : r - 1 ∈ I
hs : i ∈ ↑N ∧ s ⊆ ↑N
c : R
hc1 : c - 1 ∈ I
hci : c • i ∈ I • span R s
n : M
hn : n ∈ N
y : M
hy : ∃ y_1, y_1 ∈ I ∧ y_1 • i = y
z : M
hz : z ∈ I • span R s
hyz : y + z = r • n
⊢ n ∈ comap (↑(LinearMap.lsmul R M) (c * r)) (I • span R s)
case intro.intro.refine'_2.intro.intro.intro.intro.intro.refine'_2.intro.intro.intro.intro
R✝ : Type ?u.23931
M✝ : Type ?u.23934
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s✝ : Set M
hfs : Set.Finite s✝
i : M
s : Set M
x✝¹ : ¬i ∈ s
x✝ : Set.Finite s
ih :
  (∃ r, r - 1 ∈ I ∧ N ≤ comap (↑(LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N) →
    ∃ r, r - 1 ∈ I ∧ ∀ (n : M), n ∈ N → r • n = 0
r : R
hr1 : r - 1 ∈ I
hs : i ∈ ↑N ∧ s ⊆ ↑N
c : R
hc1 : c - 1 ∈ I
hci : c • i ∈ I • span R s
n : M
hn : n ∈ N
y : M
hy : y ∈ I • span R {i}
z : M
hz : z ∈ I • span R s
hyz : y + z = r • n
⊢ n ∈ comap (↑(LinearMap.lsmul R M) (c * r)) (I • span R s)
rw [mem_smul_span_singleton] at hy
case intro.intro.refine'_2.intro.intro.intro.intro.intro.refine'_2.intro.intro.intro.intro.intro.intro
R✝ : Type ?u.23931
M✝ : Type ?u.23934
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s✝ : Set M
hfs : Set.Finite s✝
i : M
s : Set M
x✝¹ : ¬i ∈ s
x✝ : Set.Finite s
ih :
  (∃ r, r - 1 ∈ I ∧ N ≤ comap (↑(LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N) →
    ∃ r, r - 1 ∈ I ∧ ∀ (n : M), n ∈ N → r • n = 0
r : R
hr1 : r - 1 ∈ I
hs : i ∈ ↑N ∧ s ⊆ ↑N
c : R
hc1 : c - 1 ∈ I
hci : c • i ∈ I • span R s
n : M
hn : n ∈ N
z : M
hz : z ∈ I • span R s
d : R
left✝ : d ∈ I
hyz : d • i + z = r • n
⊢ n ∈ comap (↑(LinearMap.lsmul R M) (c * r)) (I • span R s)
case intro.intro.refine'_2.intro.intro.intro.intro.intro.refine'_2.intro.intro.intro.intro
R✝ : Type ?u.23931
M✝ : Type ?u.23934
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s✝ : Set M
hfs : Set.Finite s✝
i : M
s : Set M
x✝¹ : ¬i ∈ s
x✝ : Set.Finite s
ih :
  (∃ r, r - 1 ∈ I ∧ N ≤ comap (↑(LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N) →
    ∃ r, r - 1 ∈ I ∧ ∀ (n : M), n ∈ N → r • n = 0
r : R
hr1 : r - 1 ∈ I
hs : i ∈ ↑N ∧ s ⊆ ↑N
c : R
hc1 : c - 1 ∈ I
hci : c • i ∈ I • span R s
n : M
hn : n ∈ N
y : M
hy : ∃ y_1, y_1 ∈ I ∧ y_1 • i = y
z : M
hz : z ∈ I • span R s
hyz : y + z = r • n
⊢ n ∈ comap (↑(LinearMap.lsmul R M) (c * r)) (I • span R s)
rcases hy with ⟨d, _, rfl⟩
case intro.intro.refine'_2.intro.intro.intro.intro.intro.refine'_2.intro.intro.intro.intro.intro.intro
R✝ : Type ?u.23931
M✝ : Type ?u.23934
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s✝ : Set M
hfs : Set.Finite s✝
i : M
s : Set M
x✝¹ : ¬i ∈ s
x✝ : Set.Finite s
ih :
  (∃ r, r - 1 ∈ I ∧ N ≤ comap (↑(LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N) →
    ∃ r, r - 1 ∈ I ∧ ∀ (n : M), n ∈ N → r • n = 0
r : R
hr1 : r - 1 ∈ I
hs : i ∈ ↑N ∧ s ⊆ ↑N
c : R
hc1 : c - 1 ∈ I
hci : c • i ∈ I • span R s
n : M
hn : n ∈ N
z : M
hz : z ∈ I • span R s
d : R
left✝ : d ∈ I
hyz : d • i + z = r • n
⊢ (c * r) • n ∈ I • span R s
case intro.intro.refine'_2.intro.intro.intro.intro.intro.refine'_2.intro.intro.intro.intro.intro.intro
R✝ : Type ?u.23931
M✝ : Type ?u.23934
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s✝ : Set M
hfs : Set.Finite s✝
i : M
s : Set M
x✝¹ : ¬i ∈ s
x✝ : Set.Finite s
ih :
  (∃ r, r - 1 ∈ I ∧ N ≤ comap (↑(LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N) →
    ∃ r, r - 1 ∈ I ∧ ∀ (n : M), n ∈ N → r • n = 0
r : R
hr1 : r - 1 ∈ I
hs : i ∈ ↑N ∧ s ⊆ ↑N
c : R
hc1 : c - 1 ∈ I
hci : c • i ∈ I • span R s
n : M
hn : n ∈ N
z : M
hz : z ∈ I • span R s
d : R
left✝ : d ∈ I
hyz : d • i + z = r • n
⊢ n ∈ comap (↑(LinearMap.lsmul R M) (c * r)) (I • span R s)
simp only [mem_comap, LinearMap.lsmul_apply]
case intro.intro.refine'_2.intro.intro.intro.intro.intro.refine'_2.intro.intro.intro.intro.intro.intro
R✝ : Type ?u.23931
M✝ : Type ?u.23934
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s✝ : Set M
hfs : Set.Finite s✝
i : M
s : Set M
x✝¹ : ¬i ∈ s
x✝ : Set.Finite s
ih :
  (∃ r, r - 1 ∈ I ∧ N ≤ comap (↑(LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N) →
    ∃ r, r - 1 ∈ I ∧ ∀ (n : M), n ∈ N → r • n = 0
r : R
hr1 : r - 1 ∈ I
hs : i ∈ ↑N ∧ s ⊆ ↑N
c : R
hc1 : c - 1 ∈ I
hci : c • i ∈ I • span R s
n : M
hn : n ∈ N
z : M
hz : z ∈ I • span R s
d : R
left✝ : d ∈ I
hyz : d • i + z = r • n
⊢ d • c • i + c • z ∈ I • span R s
case intro.intro.refine'_2.intro.intro.intro.intro.intro.refine'_2.intro.intro.intro.intro.intro.intro
R✝ : Type ?u.23931
M✝ : Type ?u.23934
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s✝ : Set M
hfs : Set.Finite s✝
i : M
s : Set M
x✝¹ : ¬i ∈ s
x✝ : Set.Finite s
ih :
  (∃ r, r - 1 ∈ I ∧ N ≤ comap (↑(LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N) →
    ∃ r, r - 1 ∈ I ∧ ∀ (n : M), n ∈ N → r • n = 0
r : R
hr1 : r - 1 ∈ I
hs : i ∈ ↑N ∧ s ⊆ ↑N
c : R
hc1 : c - 1 ∈ I
hci : c • i ∈ I • span R s
n : M
hn : n ∈ N
z : M
hz : z ∈ I • span R s
d : R
left✝ : d ∈ I
hyz : d • i + z = r • n
⊢ (c * r) • n ∈ I • span R s
rw [mul_smul, ← hyz, smul_add, smul_smul, mul_comm, mul_smul]
no goals
case intro.intro.refine'_2.intro.intro.intro.intro.intro.refine'_2.intro.intro.intro.intro.intro.intro
R✝ : Type ?u.23931
M✝ : Type ?u.23934
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s✝ : Set M
hfs : Set.Finite s✝
i : M
s : Set M
x✝¹ : ¬i ∈ s
x✝ : Set.Finite s
ih :
  (∃ r, r - 1 ∈ I ∧ N ≤ comap (↑(LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N) →
    ∃ r, r - 1 ∈ I ∧ ∀ (n : M), n ∈ N → r • n = 0
r : R
hr1 : r - 1 ∈ I
hs : i ∈ ↑N ∧ s ⊆ ↑N
c : R
hc1 : c - 1 ∈ I
hci : c • i ∈ I • span R s
n : M
hn : n ∈ N
z : M
hz : z ∈ I • span R s
d : R
left✝ : d ∈ I
hyz : d • i + z = r • n
⊢ d • c • i + c • z ∈ I • span R s
exact add_mem (smul_mem _ _ hci) (smul_mem _ _ hz)