-- Mathlib/Algebra/Group/Submonoid/Pointwise.lean
theorem closure_mul_closure (S T : Set R) : closure S * closure T = closure (S * T)

Proof state:
case a
R : Type u_4
inst✝ : NonUnitalNonAssocSemiring R
S T : Set R
⊢ closure (S * T) ≤ closure S * closure T

Tactic:
rw [closure_le]

Result:
case a
R : Type u_4
inst✝ : NonUnitalNonAssocSemiring R
S T : Set R
⊢ S * T ⊆ ↑(closure S * closure T)

Proof state:
case a
R : Type u_4
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))

Tactic:
refine (closure_le.2 fun a' ha' => ?_) ha

Result:
case a
R : Type u_4
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)))

Proof state:
case a
R : Type u_4
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)))

Tactic:
change a' * b' ∈ closure (S * T)

Result:
case a
R : Type u_4
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)

Proof state:
R : Type u_4
inst✝ : NonUnitalNonAssocSemiring R
S T : Set R
⊢ closure S * closure T = closure (S * T)

Tactic:
apply le_antisymm

Result:
case a
R : Type u_4
inst✝ : NonUnitalNonAssocSemiring R
S T : Set R
⊢ closure S * closure T ≤ closure (S * T)

case a
R : Type u_4
inst✝ : NonUnitalNonAssocSemiring R
S T : Set R
⊢ closure (S * T) ≤ closure S * closure T

Proof state:
case a
R : Type u_4
inst✝ : NonUnitalNonAssocSemiring R
S T : Set R
⊢ S * T ⊆ ↑(closure S * closure T)

Tactic:
rintro _ ⟨a, ha, b, hb, rfl⟩

Result:
case a.intro.intro.intro.intro
R : Type u_4
inst✝ : NonUnitalNonAssocSemiring R
S T : Set R
a : R
ha : a ∈ S
b : R
hb : b ∈ T
⊢ (fun x1 x2 => x1 * x2) a b ∈ ↑(closure S * closure T)

Proof state:
case a
R : Type u_4
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))

Tactic:
refine (closure_le.2 fun b' hb' => ?_) hb

Result:
case a
R : Type u_4
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)))

Proof state:
case a
R : Type u_4
inst✝ : NonUnitalNonAssocSemiring R
S T : Set R
⊢ closure S * closure T ≤ closure (S * T)

Tactic:
refine mul_le.2 fun a ha b hb => ?_

Result:
case a
R : Type u_4
inst✝ : NonUnitalNonAssocSemiring R
S T : Set R
a : R
ha : a ∈ closure S
b : R
hb : b ∈ closure T
⊢ a * b ∈ closure (S * T)

Proof state:
case a
R : Type u_4
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)))

Tactic:
change b ∈ (closure (S * T)).comap (AddMonoidHom.mulLeft a')

Result:
case a
R : Type u_4
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))

Proof state:
case a
R : Type u_4
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)

Tactic:
exact subset_closure (Set.mul_mem_mul ha' hb')

Result:
no goals

Proof state:
case a
R : Type u_4
inst✝ : NonUnitalNonAssocSemiring R
S T : Set R
a : R
ha : a ∈ closure S
b : R
hb : b ∈ closure T
⊢ a * b ∈ closure (S * T)

Tactic:
rw [← AddMonoidHom.mulRight_apply, ← AddSubmonoid.mem_comap]

Result:
case a
R : Type u_4
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))

Proof state:
case a.intro.intro.intro.intro
R : Type u_4
inst✝ : NonUnitalNonAssocSemiring R
S T : Set R
a : R
ha : a ∈ S
b : R
hb : b ∈ T
⊢ (fun x1 x2 => x1 * x2) a b ∈ ↑(closure S * closure T)

Tactic:
exact mul_mem_mul (subset_closure ha) (subset_closure hb)

Result:
no goals