no goals
M✝ : Type ?u.75380
inst✝² : Monoid M✝
s✝ : Set M✝
A : Type ?u.75389
inst✝¹ : AddMonoid A
t✝ : Set A
M : Type u_1
inst✝ : CommMonoid M
s t : Set M
x : M
hx : x ∈ Closure (s ∪ t)
L : List M
HL1✝ : ∀ (x : M), x ∈ L → x ∈ s ∪ t
HL2 : List.prod L = x
hd : M
tl : List M
ih : (∀ (x : M), x ∈ tl → x ∈ s ∪ t) → ∃ y, y ∈ Closure s ∧ ∃ z, z ∈ Closure t ∧ y * z = List.prod tl
HL1 : ∀ (x : M), x ∈ hd :: tl → x ∈ s ∪ t
y : M
hy : y ∈ Closure s
z : M
hz : z ∈ Closure t
hyzx : y * z = List.prod tl
hs : hd ∈ s
⊢ hd * y * z = List.prod (hd :: tl)
rw [mul_assoc, List.prod_cons, ← hyzx]
no goals
M✝ : Type ?u.75380
inst✝² : Monoid M✝
s✝ : Set M✝
A : Type ?u.75389
inst✝¹ : AddMonoid A
t✝ : Set A
M : Type u_1
inst✝ : CommMonoid M
s t : Set M
x : M
hx : x ∈ Closure (s ∪ t)
L : List M
HL1✝ : ∀ (x : M), x ∈ L → x ∈ s ∪ t
HL2 : List.prod L = x
hd : M
tl : List M
ih : (∀ (x : M), x ∈ tl → x ∈ s ∪ t) → ∃ y, y ∈ Closure s ∧ ∃ z, z ∈ Closure t ∧ y * z = List.prod tl
HL1 : ∀ (x : M), x ∈ hd :: tl → x ∈ s ∪ t
y : M
hy : y ∈ Closure s
z : M
hz : z ∈ Closure t
hyzx : y * z = List.prod tl
ht : hd ∈ t
⊢ y * (z * hd) = List.prod (hd :: tl)
rw [← mul_assoc, List.prod_cons, ← hyzx, mul_comm hd]