Theorem: biUnion_insert_eq (Matroid/ForMathlib/Other.lean)

State before:
α : Type u_1
β : Type u_2
s s₁ s₂ t t' : Set α
f : α → β
X : Set α
hX : X.Nonempty
Y : Set α
⊢ ⋃ x ∈ X, insert x Y = X ∪ Y
Tactic:
have := hX.to_subtype
State after:
α : Type u_1
β : Type u_2
s s₁ s₂ t t' : Set α
f : α → β
X : Set α
hX : X.Nonempty
Y : Set α
this : Nonempty ↑X
⊢ ⋃ x ∈ X, insert x Y = X ∪ Y

State before:
α : Type u_1
β : Type u_2
s s₁ s₂ t t' : Set α
f : α → β
X : Set α
hX : X.Nonempty
Y : Set α
this : Nonempty ↑X
⊢ ⋃ x ∈ X, insert x Y = X ∪ Y
Tactic:
simp_rw [← singleton_union, biUnion_eq_iUnion, ← iUnion_union, iUnion_singleton_eq_range,
  Subtype.range_coe_subtype, setOf_mem_eq]
State after:
no goals