R : Type u
M : Type v
F : Type ?u.37815
G : Type ?u.37818
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I J : Ideal R
N P : Submodule R M
p : M → Prop
x : M
H : x ∈ I • N
Hb : ∀ (r : R), r ∈ I → ∀ (n : M), n ∈ N → p (r • n)
H1 : ∀ (x y : M), p x → p y → p (x + y)
H0 : p 0
⊢ p x
R : Type u
M : Type v
F : Type ?u.37815
G : Type ?u.37818
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I J : Ideal R
N P : Submodule R M
p : M → Prop
x : M
H : x ∈ I • N
Hb : ∀ (r : R), r ∈ I → ∀ (n : M), n ∈ N → p (r • n)
H1 : ∀ (x y : M), p x → p y → p (x + y)
⊢ p x
have H0 : p 0 := by simpa only [zero_smul] using Hb 0 I.zero_mem 0 N.zero_mem
R : Type u
M : Type v
F : Type ?u.37815
G : Type ?u.37818
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I J : Ideal R
N P : Submodule R M
p : M → Prop
x : M
H : x ∈ I • N
Hb : ∀ (r : R), r ∈ I → ∀ (n : M), n ∈ N → p (r • n)
H1 : ∀ (x y : M), p x → p y → p (x + y)
H0 : p 0
⊢ ∀ (i : { x // x ∈ I }) (x : M), x ∈ map (↑(LinearMap.lsmul R M) ↑i) N → p x
R : Type u
M : Type v
F : Type ?u.37815
G : Type ?u.37818
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I J : Ideal R
N P : Submodule R M
p : M → Prop
x : M
H : x ∈ I • N
Hb : ∀ (r : R), r ∈ I → ∀ (n : M), n ∈ N → p (r • n)
H1 : ∀ (x y : M), p x → p y → p (x + y)
H0 : p 0
⊢ p x
refine Submodule.iSup_induction (x := x) _ H ?_ H0 H1
case mk.intro.intro
R : Type u
M : Type v
F : Type ?u.37815
G : Type ?u.37818
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I J : Ideal R
N P : Submodule R M
p : M → Prop
x : M
H : x ∈ I • N
Hb : ∀ (r : R), r ∈ I → ∀ (n : M), n ∈ N → p (r • n)
H1 : ∀ (x y : M), p x → p y → p (x + y)
H0 : p 0
i : R
hi : i ∈ I
m j : M
hj : j ∈ ↑N
hj' : ↑(↑(LinearMap.lsmul R M) ↑{ val := i, property := hi }) j = m
⊢ p m
R : Type u
M : Type v
F : Type ?u.37815
G : Type ?u.37818
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I J : Ideal R
N P : Submodule R M
p : M → Prop
x : M
H : x ∈ I • N
Hb : ∀ (r : R), r ∈ I → ∀ (n : M), n ∈ N → p (r • n)
H1 : ∀ (x y : M), p x → p y → p (x + y)
H0 : p 0
⊢ ∀ (i : { x // x ∈ I }) (x : M), x ∈ map (↑(LinearMap.lsmul R M) ↑i) N → p x
rintro ⟨i, hi⟩ m ⟨j, hj, hj'⟩
case mk.intro.intro
R : Type u
M : Type v
F : Type ?u.37815
G : Type ?u.37818
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I J : Ideal R
N P : Submodule R M
p : M → Prop
x : M
H : x ∈ I • N
Hb : ∀ (r : R), r ∈ I → ∀ (n : M), n ∈ N → p (r • n)
H1 : ∀ (x y : M), p x → p y → p (x + y)
H0 : p 0
i : R
hi : i ∈ I
m j : M
hj : j ∈ ↑N
hj' : ↑(↑(LinearMap.lsmul R M) ↑{ val := i, property := hi }) j = m
⊢ p (↑(↑(LinearMap.lsmul R M) ↑{ val := i, property := hi }) j)
case mk.intro.intro
R : Type u
M : Type v
F : Type ?u.37815
G : Type ?u.37818
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I J : Ideal R
N P : Submodule R M
p : M → Prop
x : M
H : x ∈ I • N
Hb : ∀ (r : R), r ∈ I → ∀ (n : M), n ∈ N → p (r • n)
H1 : ∀ (x y : M), p x → p y → p (x + y)
H0 : p 0
i : R
hi : i ∈ I
m j : M
hj : j ∈ ↑N
hj' : ↑(↑(LinearMap.lsmul R M) ↑{ val := i, property := hi }) j = m
⊢ p m
rw [← hj']
no goals
case mk.intro.intro
R : Type u
M : Type v
F : Type ?u.37815
G : Type ?u.37818
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I J : Ideal R
N P : Submodule R M
p : M → Prop
x : M
H : x ∈ I • N
Hb : ∀ (r : R), r ∈ I → ∀ (n : M), n ∈ N → p (r • n)
H1 : ∀ (x y : M), p x → p y → p (x + y)
H0 : p 0
i : R
hi : i ∈ I
m j : M
hj : j ∈ ↑N
hj' : ↑(↑(LinearMap.lsmul R M) ↑{ val := i, property := hi }) j = m
⊢ p (↑(↑(LinearMap.lsmul R M) ↑{ val := i, property := hi }) j)
exact Hb _ hi _ hj
no goals
R : Type u
M : Type v
F : Type ?u.37815
G : Type ?u.37818
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I J : Ideal R
N P : Submodule R M
p : M → Prop
x : M
H : x ∈ I • N
Hb : ∀ (r : R), r ∈ I → ∀ (n : M), n ∈ N → p (r • n)
H1 : ∀ (x y : M), p x → p y → p (x + y)
⊢ p 0
simpa only [zero_smul] using Hb 0 I.zero_mem 0 N.zero_mem