ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M N P Q : Submodule R A
m n : A
C : A → Prop
r : A
hr : r ∈ M.toAddSubmonoid * N.toAddSubmonoid
hm : ∀ (m : A), m ∈ M → ∀ (n : A), n ∈ N → C (m * n)
ha : ∀ (x y : A), C x → C y → C (x + y)
⊢ C r
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M N P Q : Submodule R A
m n : A
C : A → Prop
r : A
hr : r ∈ M * N
hm : ∀ (m : A), m ∈ M → ∀ (n : A), n ∈ N → C (m * n)
ha : ∀ (x y : A), C x → C y → C (x + y)
⊢ C r
rw [← mem_toAddSubmonoid, mul_toAddSubmonoid] at hr
no goals
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M N P Q : Submodule R A
m n : A
C : A → Prop
r : A
hr : r ∈ M.toAddSubmonoid * N.toAddSubmonoid
hm : ∀ (m : A), m ∈ M → ∀ (n : A), n ∈ N → C (m * n)
ha : ∀ (x y : A), C x → C y → C (x + y)
⊢ C r
exact AddSubmonoid.mul_induction_on hr hm ha