R : Type u_2
R₂ : Type ?u.215996
K : Type ?u.215999
M : Type u_3
M₂ : Type ?u.216005
V : Type ?u.216008
S : Type ?u.216011
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
x✝ : M
p✝ p' : Submodule R M
inst✝² : Semiring R₂
σ₁₂ : R →+* R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
s t : Set M
ι : Sort u_1
p : ι → Submodule R M
C : M → Prop
x : M
hx : x ∈ ⨆ (i : ι), (p i).toAddSubmonoid
hp : ∀ (i : ι) (x : M), x ∈ p i → C x
h0 : C 0
hadd : ∀ (x y : M), C x → C y → C (x + y)
⊢ C x
R : Type u_2
R₂ : Type ?u.215996
K : Type ?u.215999
M : Type u_3
M₂ : Type ?u.216005
V : Type ?u.216008
S : Type ?u.216011
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
x✝ : M
p✝ p' : Submodule R M
inst✝² : Semiring R₂
σ₁₂ : R →+* R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
s t : Set M
ι : Sort u_1
p : ι → Submodule R M
C : M → Prop
x : M
hx : x ∈ ⨆ (i : ι), p i
hp : ∀ (i : ι) (x : M), x ∈ p i → C x
h0 : C 0
hadd : ∀ (x y : M), C x → C y → C (x + y)
⊢ C x
rw [← mem_toAddSubmonoid, iSup_toAddSubmonoid] at hx
no goals
R : Type u_2
R₂ : Type ?u.215996
K : Type ?u.215999
M : Type u_3
M₂ : Type ?u.216005
V : Type ?u.216008
S : Type ?u.216011
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
x✝ : M
p✝ p' : Submodule R M
inst✝² : Semiring R₂
σ₁₂ : R →+* R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
s t : Set M
ι : Sort u_1
p : ι → Submodule R M
C : M → Prop
x : M
hx : x ∈ ⨆ (i : ι), (p i).toAddSubmonoid
hp : ∀ (i : ι) (x : M), x ∈ p i → C x
h0 : C 0
hadd : ∀ (x y : M), C x → C y → C (x + y)
⊢ C x
exact AddSubmonoid.iSup_induction (x := x) _ hx hp h0 hadd