case a
α : Type ?u.244690
G : Type ?u.244693
M : Type ?u.244696
R : Type u_1
A : Type ?u.244702
inst✝² : Monoid M
inst✝¹ : AddMonoid A
inst✝ : NonUnitalNonAssocSemiring R
S T : Set R
⊢ closure S * closure T ≤ closure (S * T)

case a
α : Type ?u.244690
G : Type ?u.244693
M : Type ?u.244696
R : Type u_1
A : Type ?u.244702
inst✝² : Monoid M
inst✝¹ : AddMonoid A
inst✝ : NonUnitalNonAssocSemiring R
S T : Set R
⊢ closure (S * T) ≤ closure S * closure T
α : Type ?u.244690
G : Type ?u.244693
M : Type ?u.244696
R : Type u_1
A : Type ?u.244702
inst✝² : Monoid M
inst✝¹ : AddMonoid A
inst✝ : NonUnitalNonAssocSemiring R
S T : Set R
⊢ closure S * closure T = closure (S * T)
apply le_antisymm
case a
α : Type ?u.244690
G : Type ?u.244693
M : Type ?u.244696
R : Type u_1
A : Type ?u.244702
inst✝² : Monoid M
inst✝¹ : AddMonoid A
inst✝ : NonUnitalNonAssocSemiring R
S T : Set R
a : R
ha : a ∈ closure S
b : R
hb : b ∈ closure T
⊢ a * b ∈ closure (S * T)
case a
α : Type ?u.244690
G : Type ?u.244693
M : Type ?u.244696
R : Type u_1
A : Type ?u.244702
inst✝² : Monoid M
inst✝¹ : AddMonoid A
inst✝ : NonUnitalNonAssocSemiring R
S T : Set R
⊢ closure S * closure T ≤ closure (S * T)
refine mul_le.2 fun a ha b hb => ?_
case a
α : Type ?u.244690
G : Type ?u.244693
M : Type ?u.244696
R : Type u_1
A : Type ?u.244702
inst✝² : Monoid M
inst✝¹ : AddMonoid A
inst✝ : NonUnitalNonAssocSemiring R
S T : Set R
a : R
ha : a ∈ closure S
b : R
hb : b ∈ closure T
⊢ a ∈ comap (AddMonoidHom.mulRight b) (closure (S * T))
case a
α : Type ?u.244690
G : Type ?u.244693
M : Type ?u.244696
R : Type u_1
A : Type ?u.244702
inst✝² : Monoid M
inst✝¹ : AddMonoid A
inst✝ : NonUnitalNonAssocSemiring R
S T : Set R
a : R
ha : a ∈ closure S
b : R
hb : b ∈ closure T
⊢ a * b ∈ closure (S * T)
rw [← AddMonoidHom.mulRight_apply, ← AddSubmonoid.mem_comap]
case a
α : Type ?u.244690
G : Type ?u.244693
M : Type ?u.244696
R : Type u_1
A : Type ?u.244702
inst✝² : Monoid M
inst✝¹ : AddMonoid A
inst✝ : NonUnitalNonAssocSemiring R
S T : Set R
a : R
ha : a ∈ closure S
b : R
hb : b ∈ closure T
a' : R
ha' : a' ∈ S
⊢ a' ∈ ↑(comap (AddMonoidHom.mulRight b) (closure (S * T)))
case a
α : Type ?u.244690
G : Type ?u.244693
M : Type ?u.244696
R : Type u_1
A : Type ?u.244702
inst✝² : Monoid M
inst✝¹ : AddMonoid A
inst✝ : NonUnitalNonAssocSemiring R
S T : Set R
a : R
ha : a ∈ closure S
b : R
hb : b ∈ closure T
⊢ a ∈ comap (AddMonoidHom.mulRight b) (closure (S * T))
refine (closure_le.2 fun a' ha' => ?_) ha
case a
α : Type ?u.244690
G : Type ?u.244693
M : Type ?u.244696
R : Type u_1
A : Type ?u.244702
inst✝² : Monoid M
inst✝¹ : AddMonoid A
inst✝ : NonUnitalNonAssocSemiring R
S T : Set R
a : R
ha : a ∈ closure S
b : R
hb : b ∈ closure T
a' : R
ha' : a' ∈ S
⊢ b ∈ comap (AddMonoidHom.mulLeft a') (closure (S * T))
case a
α : Type ?u.244690
G : Type ?u.244693
M : Type ?u.244696
R : Type u_1
A : Type ?u.244702
inst✝² : Monoid M
inst✝¹ : AddMonoid A
inst✝ : NonUnitalNonAssocSemiring R
S T : Set R
a : R
ha : a ∈ closure S
b : R
hb : b ∈ closure T
a' : R
ha' : a' ∈ S
⊢ a' ∈ ↑(comap (AddMonoidHom.mulRight b) (closure (S * T)))
change b ∈ (closure (S * T)).comap (AddMonoidHom.mulLeft a')
case a
α : Type ?u.244690
G : Type ?u.244693
M : Type ?u.244696
R : Type u_1
A : Type ?u.244702
inst✝² : Monoid M
inst✝¹ : AddMonoid A
inst✝ : NonUnitalNonAssocSemiring R
S T : Set R
a : R
ha : a ∈ closure S
b : R
hb : b ∈ closure T
a' : R
ha' : a' ∈ S
b' : R
hb' : b' ∈ T
⊢ b' ∈ ↑(comap (AddMonoidHom.mulLeft a') (closure (S * T)))
case a
α : Type ?u.244690
G : Type ?u.244693
M : Type ?u.244696
R : Type u_1
A : Type ?u.244702
inst✝² : Monoid M
inst✝¹ : AddMonoid A
inst✝ : NonUnitalNonAssocSemiring R
S T : Set R
a : R
ha : a ∈ closure S
b : R
hb : b ∈ closure T
a' : R
ha' : a' ∈ S
⊢ b ∈ comap (AddMonoidHom.mulLeft a') (closure (S * T))
refine (closure_le.2 fun b' hb' => ?_) hb
case a
α : Type ?u.244690
G : Type ?u.244693
M : Type ?u.244696
R : Type u_1
A : Type ?u.244702
inst✝² : Monoid M
inst✝¹ : AddMonoid A
inst✝ : NonUnitalNonAssocSemiring R
S T : Set R
a : R
ha : a ∈ closure S
b : R
hb : b ∈ closure T
a' : R
ha' : a' ∈ S
b' : R
hb' : b' ∈ T
⊢ a' * b' ∈ closure (S * T)
case a
α : Type ?u.244690
G : Type ?u.244693
M : Type ?u.244696
R : Type u_1
A : Type ?u.244702
inst✝² : Monoid M
inst✝¹ : AddMonoid A
inst✝ : NonUnitalNonAssocSemiring R
S T : Set R
a : R
ha : a ∈ closure S
b : R
hb : b ∈ closure T
a' : R
ha' : a' ∈ S
b' : R
hb' : b' ∈ T
⊢ b' ∈ ↑(comap (AddMonoidHom.mulLeft a') (closure (S * T)))
change a' * b' ∈ closure (S * T)
no goals
case a
α : Type ?u.244690
G : Type ?u.244693
M : Type ?u.244696
R : Type u_1
A : Type ?u.244702
inst✝² : Monoid M
inst✝¹ : AddMonoid A
inst✝ : NonUnitalNonAssocSemiring R
S T : Set R
a : R
ha : a ∈ closure S
b : R
hb : b ∈ closure T
a' : R
ha' : a' ∈ S
b' : R
hb' : b' ∈ T
⊢ a' * b' ∈ closure (S * T)
exact subset_closure (Set.mul_mem_mul ha' hb')
case a
α : Type ?u.244690
G : Type ?u.244693
M : Type ?u.244696
R : Type u_1
A : Type ?u.244702
inst✝² : Monoid M
inst✝¹ : AddMonoid A
inst✝ : NonUnitalNonAssocSemiring R
S T : Set R
⊢ S * T ⊆ ↑(closure S * closure T)
case a
α : Type ?u.244690
G : Type ?u.244693
M : Type ?u.244696
R : Type u_1
A : Type ?u.244702
inst✝² : Monoid M
inst✝¹ : AddMonoid A
inst✝ : NonUnitalNonAssocSemiring R
S T : Set R
⊢ closure (S * T) ≤ closure S * closure T
rw [closure_le]
case a.intro.intro.intro.intro
α : Type ?u.244690
G : Type ?u.244693
M : Type ?u.244696
R : Type u_1
A : Type ?u.244702
inst✝² : Monoid M
inst✝¹ : AddMonoid A
inst✝ : NonUnitalNonAssocSemiring R
S T : Set R
a b : R
ha : a ∈ S
hb : b ∈ T
⊢ (fun x x_1 => x * x_1) a b ∈ ↑(closure S * closure T)
case a
α : Type ?u.244690
G : Type ?u.244693
M : Type ?u.244696
R : Type u_1
A : Type ?u.244702
inst✝² : Monoid M
inst✝¹ : AddMonoid A
inst✝ : NonUnitalNonAssocSemiring R
S T : Set R
⊢ S * T ⊆ ↑(closure S * closure T)
rintro _ ⟨a, b, ha, hb, rfl⟩
no goals
case a.intro.intro.intro.intro
α : Type ?u.244690
G : Type ?u.244693
M : Type ?u.244696
R : Type u_1
A : Type ?u.244702
inst✝² : Monoid M
inst✝¹ : AddMonoid A
inst✝ : NonUnitalNonAssocSemiring R
S T : Set R
a b : R
ha : a ∈ S
hb : b ∈ T
⊢ (fun x x_1 => x * x_1) a b ∈ ↑(closure S * closure T)
exact mul_mem_mul (subset_closure ha) (subset_closure hb)