ι : 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 : (r : A) → r ∈ M * N → Prop
hm : ∀ (m : A) (x : m ∈ M) (n : A) (x_1 : n ∈ N), C (m * n) (_ : m * n ∈ M * N)
ha : ∀ (x : A) (hx : x ∈ M * N) (y : A) (hy : y ∈ M * N), C x hx → C y hy → C (x + y) (_ : x + y ∈ M * N)
r : A
hr : r ∈ M * N
⊢ ∃ x, C r x
ι : 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 : (r : A) → r ∈ M * N → Prop
hm : ∀ (m : A) (x : m ∈ M) (n : A) (x_1 : n ∈ N), C (m * n) (_ : m * n ∈ M * N)
ha : ∀ (x : A) (hx : x ∈ M * N) (y : A) (hy : y ∈ M * N), C x hx → C y hy → C (x + y) (_ : x + y ∈ M * N)
r : A
hr : r ∈ M * N
⊢ C r hr
refine' Exists.elim _ fun (hr : r ∈ M * N) (hc : C r hr) => hc
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 : (r : A) → r ∈ M * N → Prop
hm : ∀ (m : A) (x : m ∈ M) (n : A) (x_1 : n ∈ N), C (m * n) (_ : m * n ∈ M * N)
ha : ∀ (x : A) (hx : x ∈ M * N) (y : A) (hy : y ∈ M * N), C x hx → C y hy → C (x + y) (_ : x + y ∈ M * N)
r : A
hr : r ∈ M * N
⊢ ∃ x, C r x
exact
  Submodule.mul_induction_on hr (fun x hx y hy => ⟨_, hm _ hx _ hy⟩) fun x y ⟨_, hx⟩ ⟨_, hy⟩ =>
    ⟨_, ha _ _ _ _ hx hy⟩