case refine'_1
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
t : Set β
h : Set.Infinite (s ×ˢ t)
⊢ Set.Infinite s ∧ Set.Nonempty t ∨ Set.Infinite t ∧ Set.Nonempty s

case refine'_2
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
t : Set β
⊢ Set.Infinite s ∧ Set.Nonempty t ∨ Set.Infinite t ∧ Set.Nonempty s → Set.Infinite (s ×ˢ t)
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
t : Set β
⊢ Set.Infinite (s ×ˢ t) ↔ Set.Infinite s ∧ Set.Nonempty t ∨ Set.Infinite t ∧ Set.Nonempty s
refine' ⟨fun h => _, _⟩
case refine'_1
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
t : Set β
h : Set.Infinite (s ×ˢ t)
⊢ ¬(Set.Nonempty t → Set.Finite s) ∨ ¬(Set.Nonempty s → Set.Finite t)
case refine'_1
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
t : Set β
h : Set.Infinite (s ×ˢ t)
⊢ Set.Infinite s ∧ Set.Nonempty t ∨ Set.Infinite t ∧ Set.Nonempty s
simp_rw [Set.Infinite, @and_comm ¬_, ← not_imp]
case refine'_1
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
t : Set β
h : Set.Infinite (s ×ˢ t)
this : (Set.Nonempty t → Set.Finite s) ∧ (Set.Nonempty s → Set.Finite t)
⊢ False
case refine'_1
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
t : Set β
h : Set.Infinite (s ×ˢ t)
⊢ ¬(Set.Nonempty t → Set.Finite s) ∨ ¬(Set.Nonempty s → Set.Finite t)
by_contra'
no goals
case refine'_1
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
t : Set β
h : Set.Infinite (s ×ˢ t)
this : (Set.Nonempty t → Set.Finite s) ∧ (Set.Nonempty s → Set.Finite t)
⊢ False
exact h ((this.1 h.nonempty.snd).prod $ this.2 h.nonempty.fst)
case refine'_2.inl
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
t : Set β
h : Set.Infinite s ∧ Set.Nonempty t
⊢ Set.Infinite (s ×ˢ t)

case refine'_2.inr
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
t : Set β
h : Set.Infinite t ∧ Set.Nonempty s
⊢ Set.Infinite (s ×ˢ t)
case refine'_2
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
t : Set β
⊢ Set.Infinite s ∧ Set.Nonempty t ∨ Set.Infinite t ∧ Set.Nonempty s → Set.Infinite (s ×ˢ t)
rintro (h | h)
no goals
case refine'_2.inl
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
t : Set β
h : Set.Infinite s ∧ Set.Nonempty t
⊢ Set.Infinite (s ×ˢ t)
exact h.1.prod_left h.2
no goals
case refine'_2.inr
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
t : Set β
h : Set.Infinite t ∧ Set.Nonempty s
⊢ Set.Infinite (s ×ˢ t)
exact h.1.prod_right h.2