Theorem: Matroid.cl_iUnion_congr (Matroid/Closure.lean)

State before:
α : Type u_1
ι✝ : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
ι : Type u_3
Xs Ys : ι → Set α
h : ∀ (i : ι), M.cl (Xs i) = M.cl (Ys i)
⊢ M.cl (⋃ i, Xs i) = M.cl (⋃ i, Ys i)
Tactic:
rw [← M.cl_iUnion_cl_eq_cl_iUnion]
State after:
α : Type u_1
ι✝ : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
ι : Type u_3
Xs Ys : ι → Set α
h : ∀ (i : ι), M.cl (Xs i) = M.cl (Ys i)
⊢ M.cl (⋃ i, M.cl (Xs i)) = M.cl (⋃ i, Ys i)

State before:
α : Type u_1
ι✝ : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
ι : Type u_3
Xs Ys : ι → Set α
h : ∀ (i : ι), M.cl (Xs i) = M.cl (Ys i)
⊢ M.cl (⋃ i, M.cl (Xs i)) = M.cl (⋃ i, Ys i)
Tactic:
simp [h, M.cl_iUnion_cl_eq_cl_iUnion]
State after:
no goals