α✝ : Type ?u.105347
β : Type ?u.105350
γ : Type ?u.105353
ι✝ : Sort ?u.105356
ι' : Sort ?u.105359
ι₂ : Sort ?u.105362
κ : ι✝ → Sort ?u.105367
κ₁ : ι✝ → Sort ?u.105372
κ₂ : ι✝ → Sort ?u.105377
κ' : ι' → Sort ?u.105382
ι : Type u_1
α : Type u_2
s : Set ι
hs : Set.Nonempty s
f : ι → Set α
t : Set α
⊢ (⋂ (i : ι) (_ : i ∈ s), t ∩ f i) = ⋂ (i : ι) (_ : i ∈ s), f i ∩ t
α✝ : Type ?u.105347
β : Type ?u.105350
γ : Type ?u.105353
ι✝ : Sort ?u.105356
ι' : Sort ?u.105359
ι₂ : Sort ?u.105362
κ : ι✝ → Sort ?u.105367
κ₁ : ι✝ → Sort ?u.105372
κ₂ : ι✝ → Sort ?u.105377
κ' : ι' → Sort ?u.105382
ι : Type u_1
α : Type u_2
s : Set ι
hs : Set.Nonempty s
f : ι → Set α
t : Set α
⊢ (⋂ (i : ι) (_ : i ∈ s), t ∩ f i) = t ∩ ⋂ (i : ι) (_ : i ∈ s), f i
rw [inter_comm, ← biInter_inter hs]
no goals
α✝ : Type ?u.105347
β : Type ?u.105350
γ : Type ?u.105353
ι✝ : Sort ?u.105356
ι' : Sort ?u.105359
ι₂ : Sort ?u.105362
κ : ι✝ → Sort ?u.105367
κ₁ : ι✝ → Sort ?u.105372
κ₂ : ι✝ → Sort ?u.105377
κ' : ι' → Sort ?u.105382
ι : Type u_1
α : Type u_2
s : Set ι
hs : Set.Nonempty s
f : ι → Set α
t : Set α
⊢ (⋂ (i : ι) (_ : i ∈ s), t ∩ f i) = ⋂ (i : ι) (_ : i ∈ s), f i ∩ t
simp [inter_comm]