R : Type u
M : Type v
F : Type ?u.42169
G : Type ?u.42172
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I J : Ideal R
N P : Submodule R M
x : M
hx : x ∈ I • N
p : (x : M) → x ∈ I • N → Prop
Hb : ∀ (r : R) (hr : r ∈ I) (n : M) (hn : n ∈ N), p (r • n) (_ : r • n ∈ I • N)
H1 : ∀ (x : M) (hx : x ∈ I • N) (y : M) (hy : y ∈ I • N), p x hx → p y hy → p (x + y) (_ : x + y ∈ I • N)
⊢ ∃ x_1, p x x_1
R : Type u
M : Type v
F : Type ?u.42169
G : Type ?u.42172
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I J : Ideal R
N P : Submodule R M
x : M
hx : x ∈ I • N
p : (x : M) → x ∈ I • N → Prop
Hb : ∀ (r : R) (hr : r ∈ I) (n : M) (hn : n ∈ N), p (r • n) (_ : r • n ∈ I • N)
H1 : ∀ (x : M) (hx : x ∈ I • N) (y : M) (hy : y ∈ I • N), p x hx → p y hy → p (x + y) (_ : x + y ∈ I • N)
⊢ p x hx
refine' Exists.elim _ fun (h : x ∈ I • N) (H : p x h) => H
no goals
R : Type u
M : Type v
F : Type ?u.42169
G : Type ?u.42172
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I J : Ideal R
N P : Submodule R M
x : M
hx : x ∈ I • N
p : (x : M) → x ∈ I • N → Prop
Hb : ∀ (r : R) (hr : r ∈ I) (n : M) (hn : n ∈ N), p (r • n) (_ : r • n ∈ I • N)
H1 : ∀ (x : M) (hx : x ∈ I • N) (y : M) (hy : y ∈ I • N), p x hx → p y hy → p (x + y) (_ : x + y ∈ I • N)
⊢ ∃ x_1, p x x_1
exact
  smul_induction_on hx (fun a ha x hx => ⟨_, Hb _ ha _ hx⟩) fun x y ⟨_, hx⟩ ⟨_, hy⟩ =>
    ⟨_, H1 _ _ _ _ hx hy⟩