Theorem: Matroid.cl_biInter_eq_biInter_cl_of_biUnion_indep (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
A : Set ι
hA : A.Nonempty
I : ι → Set α
h : M.Indep (⋃ i ∈ A, I i)
⊢ M.cl (⋂ i ∈ A, I i) = ⋂ i ∈ A, M.cl (I i)
Tactic:
have := hA.coe_sort
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
A : Set ι
hA : A.Nonempty
I : ι → Set α
h : M.Indep (⋃ i ∈ A, I i)
this : Nonempty ↑A
⊢ M.cl (⋂ i ∈ A, I i) = ⋂ i ∈ A, M.cl (I 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
A : Set ι
hA : A.Nonempty
I : ι → Set α
h : M.Indep (⋃ i ∈ A, I i)
this : Nonempty ↑A
⊢ M.cl (⋂ i ∈ A, I i) = ⋂ i ∈ A, M.cl (I i)
Tactic:
convert cl_iInter_eq_iInter_cl_of_iUnion_indep (ι := A) (Is := fun i ↦ I i) (by simpa) <;> simp
State after:
no goals

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
A : Set ι
hA : A.Nonempty
I : ι → Set α
h : M.Indep (⋃ i ∈ A, I i)
this : Nonempty ↑A
⊢ ?m.45300.Indep (⋃ i, (fun i => I ↑i) i)
Tactic:
simpa
State after:
no goals