α : Type u_1
β : Type ?u.287119
γ : Type ?u.287122
ι : Sort ?u.287125
ι' : Sort ?u.287128
ι₂ : Sort ?u.287131
κ : ι → Sort ?u.287136
κ₁ : ι → Sort ?u.287141
κ₂ : ι → Sort ?u.287146
κ' : ι' → Sort ?u.287151
π : α → Type u_2
i : Set α
s t : (a : α) → Set (π a)
x : (i : α) → π i
hx : x ∈ pi i s \ ⋃ (a : α) (_ : a ∈ i), eval a ⁻¹' (s a \ t a)
a : α
ha : a ∈ i
⊢ x a ∈ t a
α : Type u_1
β : Type ?u.287119
γ : Type ?u.287122
ι : Sort ?u.287125
ι' : Sort ?u.287128
ι₂ : Sort ?u.287131
κ : ι → Sort ?u.287136
κ₁ : ι → Sort ?u.287141
κ₂ : ι → Sort ?u.287146
κ' : ι' → Sort ?u.287151
π : α → Type u_2
i : Set α
s t : (a : α) → Set (π a)
⊢ pi i s \ pi i t ⊆ ⋃ (a : α) (_ : a ∈ i), eval a ⁻¹' (s a \ t a)
refine' diff_subset_comm.2 fun x hx a ha => _
α : Type u_1
β : Type ?u.287119
γ : Type ?u.287122
ι : Sort ?u.287125
ι' : Sort ?u.287128
ι₂ : Sort ?u.287131
κ : ι → Sort ?u.287136
κ₁ : ι → Sort ?u.287141
κ₂ : ι → Sort ?u.287146
κ' : ι' → Sort ?u.287151
π : α → Type u_2
i : Set α
s t : (a : α) → Set (π a)
x : (i : α) → π i
a : α
ha : a ∈ i
hx : (∀ (i_1 : α), i_1 ∈ i → x i_1 ∈ s i_1) ∧ ∀ (x_1 : α), x_1 ∈ i → eval x_1 x ∈ s x_1 → eval x_1 x ∈ t x_1
⊢ x a ∈ t a
α : Type u_1
β : Type ?u.287119
γ : Type ?u.287122
ι : Sort ?u.287125
ι' : Sort ?u.287128
ι₂ : Sort ?u.287131
κ : ι → Sort ?u.287136
κ₁ : ι → Sort ?u.287141
κ₂ : ι → Sort ?u.287146
κ' : ι' → Sort ?u.287151
π : α → Type u_2
i : Set α
s t : (a : α) → Set (π a)
x : (i : α) → π i
hx : x ∈ pi i s \ ⋃ (a : α) (_ : a ∈ i), eval a ⁻¹' (s a \ t a)
a : α
ha : a ∈ i
⊢ x a ∈ t a
simp only [mem_diff, mem_pi, mem_iUnion, not_exists, mem_preimage, not_and, not_not,
  eval_apply] at hx
no goals
α : Type u_1
β : Type ?u.287119
γ : Type ?u.287122
ι : Sort ?u.287125
ι' : Sort ?u.287128
ι₂ : Sort ?u.287131
κ : ι → Sort ?u.287136
κ₁ : ι → Sort ?u.287141
κ₂ : ι → Sort ?u.287146
κ' : ι' → Sort ?u.287151
π : α → Type u_2
i : Set α
s t : (a : α) → Set (π a)
x : (i : α) → π i
a : α
ha : a ∈ i
hx : (∀ (i_1 : α), i_1 ∈ i → x i_1 ∈ s i_1) ∧ ∀ (x_1 : α), x_1 ∈ i → eval x_1 x ∈ s x_1 → eval x_1 x ∈ t x_1
⊢ x a ∈ t a
exact hx.2 _ ha (hx.1 _ ha)