no goals
R : Type u
A : Type v
B : Type w
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Semiring B
inst✝² : Algebra R A
inst✝¹ : Algebra R B
s✝ t : Set A
inst✝ : DecidableEq A
α : Type u_1
s : Finset α
f : { x // x ∈ s } → Finset A
⊢ adjoin R ↑(Finset.biUnion (Finset.attach s) f) = ⨆ (x : { x // x ∈ s }), adjoin R ↑(f x)
simp [adjoin_iUnion]