R✝ : Type ?u.100030
A✝ : Type ?u.100033
inst✝⁵ : CommSemiring R✝
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R✝ A✝
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S T : Subalgebra R A
⊢ ↑toSubmodule (S ⊔ T) ≤ ↑toSubmodule S * ↑toSubmodule T
R✝ : Type ?u.100030
A✝ : Type ?u.100033
inst✝⁵ : CommSemiring R✝
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R✝ A✝
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S T : Subalgebra R A
⊢ ↑toSubmodule S * ↑toSubmodule T = ↑toSubmodule (S ⊔ T)
refine' le_antisymm (mul_toSubmodule_le _ _) _
R✝ : Type ?u.100030
A✝ : Type ?u.100033
inst✝⁵ : CommSemiring R✝
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R✝ A✝
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S T : Subalgebra R A
x : A
hx : x ∈ Algebra.adjoin R (↑S ∪ ↑T)
⊢ x ∈ ↑toSubmodule S * ↑toSubmodule T
R✝ : Type ?u.100030
A✝ : Type ?u.100033
inst✝⁵ : CommSemiring R✝
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R✝ A✝
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S T : Subalgebra R A
⊢ ↑toSubmodule (S ⊔ T) ≤ ↑toSubmodule S * ↑toSubmodule T
rintro x (hx : x ∈ Algebra.adjoin R (S ∪ T : Set A))
case refine'_1
R✝ : Type ?u.100030
A✝ : Type ?u.100033
inst✝⁵ : CommSemiring R✝
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R✝ A✝
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S T : Subalgebra R A
x✝ : A
hx✝ : x✝ ∈ Algebra.adjoin R (↑S ∪ ↑T)
x : A
hx : x ∈ ↑S ∪ ↑T
⊢ x ∈ ↑toSubmodule S * ↑toSubmodule T

case refine'_2
R✝ : Type ?u.100030
A✝ : Type ?u.100033
inst✝⁵ : CommSemiring R✝
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R✝ A✝
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S T : Subalgebra R A
x : A
hx : x ∈ Algebra.adjoin R (↑S ∪ ↑T)
r : R
⊢ ↑(algebraMap R A) r ∈ ↑toSubmodule S * ↑toSubmodule T

case refine'_3
R✝ : Type ?u.100030
A✝ : Type ?u.100033
inst✝⁵ : CommSemiring R✝
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R✝ A✝
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S T : Subalgebra R A
x✝ : A
hx✝ : x✝ ∈ Algebra.adjoin R (↑S ∪ ↑T)
x y : A
hx : x ∈ ↑toSubmodule S * ↑toSubmodule T
hy : y ∈ ↑toSubmodule S * ↑toSubmodule T
⊢ x * y ∈ ↑toSubmodule S * ↑toSubmodule T
R✝ : Type ?u.100030
A✝ : Type ?u.100033
inst✝⁵ : CommSemiring R✝
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R✝ A✝
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S T : Subalgebra R A
x : A
hx : x ∈ Algebra.adjoin R (↑S ∪ ↑T)
⊢ x ∈ ↑toSubmodule S * ↑toSubmodule T
refine'
  Algebra.adjoin_induction hx (fun x hx => _) (fun r => _) (fun _ _ => Submodule.add_mem _)
    fun x y hx hy => _
case refine'_3
R✝ : Type ?u.100030
A✝ : Type ?u.100033
inst✝⁵ : CommSemiring R✝
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R✝ A✝
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S T : Subalgebra R A
x✝ : A
hx✝ : x✝ ∈ Algebra.adjoin R (↑S ∪ ↑T)
x y : A
hx : x ∈ ↑toSubmodule S * ↑toSubmodule T
hy : y ∈ ↑toSubmodule S * ↑toSubmodule T
this : x * y ∈ ↑toSubmodule S * ↑toSubmodule T * (↑toSubmodule S * ↑toSubmodule T)
⊢ x * y ∈ ↑toSubmodule S * ↑toSubmodule T
case refine'_3
R✝ : Type ?u.100030
A✝ : Type ?u.100033
inst✝⁵ : CommSemiring R✝
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R✝ A✝
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S T : Subalgebra R A
x✝ : A
hx✝ : x✝ ∈ Algebra.adjoin R (↑S ∪ ↑T)
x y : A
hx : x ∈ ↑toSubmodule S * ↑toSubmodule T
hy : y ∈ ↑toSubmodule S * ↑toSubmodule T
⊢ x * y ∈ ↑toSubmodule S * ↑toSubmodule T
have := Submodule.mul_mem_mul hx hy
no goals
case refine'_3
R✝ : Type ?u.100030
A✝ : Type ?u.100033
inst✝⁵ : CommSemiring R✝
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R✝ A✝
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S T : Subalgebra R A
x✝ : A
hx✝ : x✝ ∈ Algebra.adjoin R (↑S ∪ ↑T)
x y : A
hx : x ∈ ↑toSubmodule S * ↑toSubmodule T
hy : y ∈ ↑toSubmodule S * ↑toSubmodule T
this : x * y ∈ ↑toSubmodule S * ↑toSubmodule T * (↑toSubmodule S * ↑toSubmodule T)
⊢ x * y ∈ ↑toSubmodule S * ↑toSubmodule T
rwa [mul_assoc, mul_comm _ (Subalgebra.toSubmodule T), ← mul_assoc _ _ (Subalgebra.toSubmodule S),
  mul_self, mul_comm (Subalgebra.toSubmodule T), ← mul_assoc, mul_self] at this
case refine'_1.inl
R✝ : Type ?u.100030
A✝ : Type ?u.100033
inst✝⁵ : CommSemiring R✝
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R✝ A✝
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S T : Subalgebra R A
x✝ : A
hx : x✝ ∈ Algebra.adjoin R (↑S ∪ ↑T)
x : A
hxS : x ∈ ↑S
⊢ x ∈ ↑toSubmodule S * ↑toSubmodule T

case refine'_1.inr
R✝ : Type ?u.100030
A✝ : Type ?u.100033
inst✝⁵ : CommSemiring R✝
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R✝ A✝
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S T : Subalgebra R A
x✝ : A
hx : x✝ ∈ Algebra.adjoin R (↑S ∪ ↑T)
x : A
hxT : x ∈ ↑T
⊢ x ∈ ↑toSubmodule S * ↑toSubmodule T
case refine'_1
R✝ : Type ?u.100030
A✝ : Type ?u.100033
inst✝⁵ : CommSemiring R✝
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R✝ A✝
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S T : Subalgebra R A
x✝ : A
hx✝ : x✝ ∈ Algebra.adjoin R (↑S ∪ ↑T)
x : A
hx : x ∈ ↑S ∪ ↑T
⊢ x ∈ ↑toSubmodule S * ↑toSubmodule T
cases' hx with hxS hxT
case refine'_1.inl
R✝ : Type ?u.100030
A✝ : Type ?u.100033
inst✝⁵ : CommSemiring R✝
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R✝ A✝
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S T : Subalgebra R A
x✝ : A
hx : x✝ ∈ Algebra.adjoin R (↑S ∪ ↑T)
x : A
hxS : x ∈ ↑S
⊢ x * 1 ∈ ↑toSubmodule S * ↑toSubmodule T
case refine'_1.inl
R✝ : Type ?u.100030
A✝ : Type ?u.100033
inst✝⁵ : CommSemiring R✝
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R✝ A✝
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S T : Subalgebra R A
x✝ : A
hx : x✝ ∈ Algebra.adjoin R (↑S ∪ ↑T)
x : A
hxS : x ∈ ↑S
⊢ x ∈ ↑toSubmodule S * ↑toSubmodule T
rw [← mul_one x]
no goals
case refine'_1.inl
R✝ : Type ?u.100030
A✝ : Type ?u.100033
inst✝⁵ : CommSemiring R✝
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R✝ A✝
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S T : Subalgebra R A
x✝ : A
hx : x✝ ∈ Algebra.adjoin R (↑S ∪ ↑T)
x : A
hxS : x ∈ ↑S
⊢ x * 1 ∈ ↑toSubmodule S * ↑toSubmodule T
exact Submodule.mul_mem_mul hxS (show (1 : A) ∈ T from one_mem T)
case refine'_1.inr
R✝ : Type ?u.100030
A✝ : Type ?u.100033
inst✝⁵ : CommSemiring R✝
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R✝ A✝
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S T : Subalgebra R A
x✝ : A
hx : x✝ ∈ Algebra.adjoin R (↑S ∪ ↑T)
x : A
hxT : x ∈ ↑T
⊢ 1 * x ∈ ↑toSubmodule S * ↑toSubmodule T
case refine'_1.inr
R✝ : Type ?u.100030
A✝ : Type ?u.100033
inst✝⁵ : CommSemiring R✝
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R✝ A✝
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S T : Subalgebra R A
x✝ : A
hx : x✝ ∈ Algebra.adjoin R (↑S ∪ ↑T)
x : A
hxT : x ∈ ↑T
⊢ x ∈ ↑toSubmodule S * ↑toSubmodule T
rw [← one_mul x]
no goals
case refine'_1.inr
R✝ : Type ?u.100030
A✝ : Type ?u.100033
inst✝⁵ : CommSemiring R✝
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R✝ A✝
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S T : Subalgebra R A
x✝ : A
hx : x✝ ∈ Algebra.adjoin R (↑S ∪ ↑T)
x : A
hxT : x ∈ ↑T
⊢ 1 * x ∈ ↑toSubmodule S * ↑toSubmodule T
exact Submodule.mul_mem_mul (show (1 : A) ∈ S from one_mem S) hxT
case refine'_2
R✝ : Type ?u.100030
A✝ : Type ?u.100033
inst✝⁵ : CommSemiring R✝
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R✝ A✝
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S T : Subalgebra R A
x : A
hx : x ∈ Algebra.adjoin R (↑S ∪ ↑T)
r : R
⊢ 1 * ↑(algebraMap R A) r ∈ ↑toSubmodule S * ↑toSubmodule T
case refine'_2
R✝ : Type ?u.100030
A✝ : Type ?u.100033
inst✝⁵ : CommSemiring R✝
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R✝ A✝
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S T : Subalgebra R A
x : A
hx : x ∈ Algebra.adjoin R (↑S ∪ ↑T)
r : R
⊢ ↑(algebraMap R A) r ∈ ↑toSubmodule S * ↑toSubmodule T
rw [← one_mul (algebraMap _ _ _)]
no goals
case refine'_2
R✝ : Type ?u.100030
A✝ : Type ?u.100033
inst✝⁵ : CommSemiring R✝
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R✝ A✝
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S T : Subalgebra R A
x : A
hx : x ∈ Algebra.adjoin R (↑S ∪ ↑T)
r : R
⊢ 1 * ↑(algebraMap R A) r ∈ ↑toSubmodule S * ↑toSubmodule T
exact Submodule.mul_mem_mul (show (1 : A) ∈ S from one_mem S) (algebraMap_mem _ _)