ι : Type u_2
α : ι → Type u_1
β : ι → Type ?u.155680
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
i : ι
h : pi s t₁ ⊆ pi s t₂
⊢ ¬pi s t₁ = ∅ → ∀ (i : ι), i ∈ s → t₁ i ⊆ t₂ i
ι : Type u_2
α : ι → Type u_1
β : ι → Type ?u.155680
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
i : ι
⊢ pi s t₁ ⊆ pi s t₂ ↔ (∀ (i : ι), i ∈ s → t₁ i ⊆ t₂ i) ∨ pi s t₁ = ∅
refine'
  ⟨fun h => or_iff_not_imp_right.2 _, fun h => h.elim pi_mono fun h' => h'.symm ▸ empty_subset _⟩
ι : Type u_2
α : ι → Type u_1
β : ι → Type ?u.155680
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
i : ι
h : pi s t₁ ⊆ pi s t₂
⊢ Set.Nonempty (pi s t₁) → ∀ (i : ι), i ∈ s → t₁ i ⊆ t₂ i
ι : Type u_2
α : ι → Type u_1
β : ι → Type ?u.155680
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
i : ι
h : pi s t₁ ⊆ pi s t₂
⊢ ¬pi s t₁ = ∅ → ∀ (i : ι), i ∈ s → t₁ i ⊆ t₂ i
rw [← Ne.def, ← nonempty_iff_ne_empty]
ι : Type u_2
α : ι → Type u_1
β : ι → Type ?u.155680
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
i✝ : ι
h : pi s t₁ ⊆ pi s t₂
hne : Set.Nonempty (pi s t₁)
i : ι
hi : i ∈ s
⊢ t₁ i ⊆ t₂ i
ι : Type u_2
α : ι → Type u_1
β : ι → Type ?u.155680
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
i : ι
h : pi s t₁ ⊆ pi s t₂
⊢ Set.Nonempty (pi s t₁) → ∀ (i : ι), i ∈ s → t₁ i ⊆ t₂ i
intro hne i hi
no goals
ι : Type u_2
α : ι → Type u_1
β : ι → Type ?u.155680
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
i✝ : ι
h : pi s t₁ ⊆ pi s t₂
hne : Set.Nonempty (pi s t₁)
i : ι
hi : i ∈ s
⊢ t₁ i ⊆ t₂ i
simpa only [eval_image_pi hi hne, eval_image_pi hi (hne.mono h)] using
  image_subset (fun f : ∀ i, α i => f i) h