case inl
α : Type u_1
β : Type u_2
γ : Type ?u.87049
δ : Type ?u.87052
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
h : s ×ˢ t = ∅
⊢ s ×ˢ t ⊆ s₁ ×ˢ t₁ ↔ s ⊆ s₁ ∧ t ⊆ t₁ ∨ s = ∅ ∨ t = ∅

case inr
α : Type u_1
β : Type u_2
γ : Type ?u.87049
δ : Type ?u.87052
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
h : Set.Nonempty (s ×ˢ t)
⊢ s ×ˢ t ⊆ s₁ ×ˢ t₁ ↔ s ⊆ s₁ ∧ t ⊆ t₁ ∨ s = ∅ ∨ t = ∅
α : Type u_1
β : Type u_2
γ : Type ?u.87049
δ : Type ?u.87052
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
⊢ s ×ˢ t ⊆ s₁ ×ˢ t₁ ↔ s ⊆ s₁ ∧ t ⊆ t₁ ∨ s = ∅ ∨ t = ∅
cases' (s ×ˢ t).eq_empty_or_nonempty with h h
case inr
α : Type u_1
β : Type u_2
γ : Type ?u.87049
δ : Type ?u.87052
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
h : Set.Nonempty (s ×ˢ t)
st : Set.Nonempty s ∧ Set.Nonempty t
⊢ s ×ˢ t ⊆ s₁ ×ˢ t₁ ↔ s ⊆ s₁ ∧ t ⊆ t₁ ∨ s = ∅ ∨ t = ∅
case inr
α : Type u_1
β : Type u_2
γ : Type ?u.87049
δ : Type ?u.87052
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
h : Set.Nonempty (s ×ˢ t)
⊢ s ×ˢ t ⊆ s₁ ×ˢ t₁ ↔ s ⊆ s₁ ∧ t ⊆ t₁ ∨ s = ∅ ∨ t = ∅
have st : s.Nonempty ∧ t.Nonempty := by rwa [prod_nonempty_iff] at h
case inr.refine'_1
α : Type u_1
β : Type u_2
γ : Type ?u.87049
δ : Type ?u.87052
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
h : Set.Nonempty (s ×ˢ t)
st : Set.Nonempty s ∧ Set.Nonempty t
H : s ×ˢ t ⊆ s₁ ×ˢ t₁
⊢ s ⊆ s₁

case inr.refine'_2
α : Type u_1
β : Type u_2
γ : Type ?u.87049
δ : Type ?u.87052
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
h : Set.Nonempty (s ×ˢ t)
st : Set.Nonempty s ∧ Set.Nonempty t
H : s ×ˢ t ⊆ s₁ ×ˢ t₁
⊢ t ⊆ t₁

case inr.refine'_3
α : Type u_1
β : Type u_2
γ : Type ?u.87049
δ : Type ?u.87052
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
h : Set.Nonempty (s ×ˢ t)
st : Set.Nonempty s ∧ Set.Nonempty t
⊢ s ⊆ s₁ ∧ t ⊆ t₁ ∨ s = ∅ ∨ t = ∅ → s ×ˢ t ⊆ s₁ ×ˢ t₁
case inr
α : Type u_1
β : Type u_2
γ : Type ?u.87049
δ : Type ?u.87052
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
h : Set.Nonempty (s ×ˢ t)
st : Set.Nonempty s ∧ Set.Nonempty t
⊢ s ×ˢ t ⊆ s₁ ×ˢ t₁ ↔ s ⊆ s₁ ∧ t ⊆ t₁ ∨ s = ∅ ∨ t = ∅
refine' ⟨fun H => Or.inl ⟨_, _⟩, _⟩
no goals
case inl
α : Type u_1
β : Type u_2
γ : Type ?u.87049
δ : Type ?u.87052
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
h : s ×ˢ t = ∅
⊢ s ×ˢ t ⊆ s₁ ×ˢ t₁ ↔ s ⊆ s₁ ∧ t ⊆ t₁ ∨ s = ∅ ∨ t = ∅
simp [h, prod_eq_empty_iff.1 h]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.87049
δ : Type ?u.87052
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
h : Set.Nonempty (s ×ˢ t)
⊢ Set.Nonempty s ∧ Set.Nonempty t
rwa [prod_nonempty_iff] at h
case inr.refine'_1
α : Type u_1
β : Type u_2
γ : Type ?u.87049
δ : Type ?u.87052
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
h : Set.Nonempty (s ×ˢ t)
st : Set.Nonempty s ∧ Set.Nonempty t
H : s ×ˢ t ⊆ s₁ ×ˢ t₁
this : Prod.fst '' s ×ˢ t ⊆ Prod.fst '' s₁ ×ˢ t₁
⊢ s ⊆ s₁
case inr.refine'_1
α : Type u_1
β : Type u_2
γ : Type ?u.87049
δ : Type ?u.87052
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
h : Set.Nonempty (s ×ˢ t)
st : Set.Nonempty s ∧ Set.Nonempty t
H : s ×ˢ t ⊆ s₁ ×ˢ t₁
⊢ s ⊆ s₁
have := image_subset (Prod.fst : α × β → α) H
no goals
case inr.refine'_1
α : Type u_1
β : Type u_2
γ : Type ?u.87049
δ : Type ?u.87052
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
h : Set.Nonempty (s ×ˢ t)
st : Set.Nonempty s ∧ Set.Nonempty t
H : s ×ˢ t ⊆ s₁ ×ˢ t₁
this : Prod.fst '' s ×ˢ t ⊆ Prod.fst '' s₁ ×ˢ t₁
⊢ s ⊆ s₁
rwa [fst_image_prod _ st.2, fst_image_prod _ (h.mono H).snd] at this
case inr.refine'_2
α : Type u_1
β : Type u_2
γ : Type ?u.87049
δ : Type ?u.87052
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
h : Set.Nonempty (s ×ˢ t)
st : Set.Nonempty s ∧ Set.Nonempty t
H : s ×ˢ t ⊆ s₁ ×ˢ t₁
this : Prod.snd '' s ×ˢ t ⊆ Prod.snd '' s₁ ×ˢ t₁
⊢ t ⊆ t₁
case inr.refine'_2
α : Type u_1
β : Type u_2
γ : Type ?u.87049
δ : Type ?u.87052
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
h : Set.Nonempty (s ×ˢ t)
st : Set.Nonempty s ∧ Set.Nonempty t
H : s ×ˢ t ⊆ s₁ ×ˢ t₁
⊢ t ⊆ t₁
have := image_subset (Prod.snd : α × β → β) H
no goals
case inr.refine'_2
α : Type u_1
β : Type u_2
γ : Type ?u.87049
δ : Type ?u.87052
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
h : Set.Nonempty (s ×ˢ t)
st : Set.Nonempty s ∧ Set.Nonempty t
H : s ×ˢ t ⊆ s₁ ×ˢ t₁
this : Prod.snd '' s ×ˢ t ⊆ Prod.snd '' s₁ ×ˢ t₁
⊢ t ⊆ t₁
rwa [snd_image_prod st.1, snd_image_prod (h.mono H).fst] at this
case inr.refine'_3
α : Type u_1
β : Type u_2
γ : Type ?u.87049
δ : Type ?u.87052
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
h : Set.Nonempty (s ×ˢ t)
st : Set.Nonempty s ∧ Set.Nonempty t
H : s ⊆ s₁ ∧ t ⊆ t₁ ∨ s = ∅ ∨ t = ∅
⊢ s ×ˢ t ⊆ s₁ ×ˢ t₁
case inr.refine'_3
α : Type u_1
β : Type u_2
γ : Type ?u.87049
δ : Type ?u.87052
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
h : Set.Nonempty (s ×ˢ t)
st : Set.Nonempty s ∧ Set.Nonempty t
⊢ s ⊆ s₁ ∧ t ⊆ t₁ ∨ s = ∅ ∨ t = ∅ → s ×ˢ t ⊆ s₁ ×ˢ t₁
intro H
case inr.refine'_3
α : Type u_1
β : Type u_2
γ : Type ?u.87049
δ : Type ?u.87052
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
h : Set.Nonempty (s ×ˢ t)
st : Set.Nonempty s ∧ Set.Nonempty t
H : s ⊆ s₁ ∧ t ⊆ t₁
⊢ s ×ˢ t ⊆ s₁ ×ˢ t₁
case inr.refine'_3
α : Type u_1
β : Type u_2
γ : Type ?u.87049
δ : Type ?u.87052
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
h : Set.Nonempty (s ×ˢ t)
st : Set.Nonempty s ∧ Set.Nonempty t
H : s ⊆ s₁ ∧ t ⊆ t₁ ∨ s = ∅ ∨ t = ∅
⊢ s ×ˢ t ⊆ s₁ ×ˢ t₁
simp only [st.1.ne_empty, st.2.ne_empty, or_false_iff] at H
no goals
case inr.refine'_3
α : Type u_1
β : Type u_2
γ : Type ?u.87049
δ : Type ?u.87052
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
h : Set.Nonempty (s ×ˢ t)
st : Set.Nonempty s ∧ Set.Nonempty t
H : s ⊆ s₁ ∧ t ⊆ t₁
⊢ s ×ˢ t ⊆ s₁ ×ˢ t₁
exact prod_mono H.1 H.2