α : Type u_2
β : Type u_1
γ : Type ?u.4496
H : Infinite (α × β)
⊢ Infinite α ∧ Nonempty β ∨ Nonempty α ∧ Infinite β
α : Type u_2
β : Type u_1
γ : Type ?u.4496
⊢ Infinite (α × β) ↔ Infinite α ∧ Nonempty β ∨ Nonempty α ∧ Infinite β
refine'
  ⟨fun H => _, fun H =>
    H.elim (and_imp.2 <| @Prod.infinite_of_left α β) (and_imp.2 <| @Prod.infinite_of_right α β)⟩
α : Type u_2
β : Type u_1
γ : Type ?u.4496
H : Infinite (α × β)
⊢ Nonempty β ∧ Infinite α ∨ Nonempty α ∧ Infinite β
α : Type u_2
β : Type u_1
γ : Type ?u.4496
H : Infinite (α × β)
⊢ Infinite α ∧ Nonempty β ∨ Nonempty α ∧ Infinite β
rw [and_comm]
α : Type u_2
β : Type u_1
γ : Type ?u.4496
H : (Nonempty β → ¬Infinite α) ∧ (Nonempty α → ¬Infinite β)
⊢ ¬Infinite (α × β)
α : Type u_2
β : Type u_1
γ : Type ?u.4496
H : Infinite (α × β)
⊢ Nonempty β ∧ Infinite α ∨ Nonempty α ∧ Infinite β
contrapose! H
α : Type u_2
β : Type u_1
γ : Type ?u.4496
H : (Nonempty β → ¬Infinite α) ∧ (Nonempty α → ¬Infinite β)
H' : Infinite (α × β)
⊢ False
α : Type u_2
β : Type u_1
γ : Type ?u.4496
H : (Nonempty β → ¬Infinite α) ∧ (Nonempty α → ¬Infinite β)
⊢ ¬Infinite (α × β)
intro H'
case intro.mk
α : Type u_2
β : Type u_1
γ : Type ?u.4496
H : (Nonempty β → ¬Infinite α) ∧ (Nonempty α → ¬Infinite β)
H' : Infinite (α × β)
a : α
b : β
⊢ False
α : Type u_2
β : Type u_1
γ : Type ?u.4496
H : (Nonempty β → ¬Infinite α) ∧ (Nonempty α → ¬Infinite β)
H' : Infinite (α × β)
⊢ False
rcases Infinite.nonempty (α × β) with ⟨a, b⟩
case intro.mk
α : Type u_2
β : Type u_1
γ : Type ?u.4496
H : (Nonempty β → ¬Infinite α) ∧ (Nonempty α → ¬Infinite β)
H' : Infinite (α × β)
a : α
b : β
this : Fintype α
⊢ False
case intro.mk
α : Type u_2
β : Type u_1
γ : Type ?u.4496
H : (Nonempty β → ¬Infinite α) ∧ (Nonempty α → ¬Infinite β)
H' : Infinite (α × β)
a : α
b : β
⊢ False
haveI := fintypeOfNotInfinite (H.1 ⟨b⟩)
case intro.mk
α : Type u_2
β : Type u_1
γ : Type ?u.4496
H : (Nonempty β → ¬Infinite α) ∧ (Nonempty α → ¬Infinite β)
H' : Infinite (α × β)
a : α
b : β
this✝ : Fintype α
this : Fintype β
⊢ False
case intro.mk
α : Type u_2
β : Type u_1
γ : Type ?u.4496
H : (Nonempty β → ¬Infinite α) ∧ (Nonempty α → ¬Infinite β)
H' : Infinite (α × β)
a : α
b : β
this : Fintype α
⊢ False
haveI := fintypeOfNotInfinite (H.2 ⟨a⟩)
no goals
case intro.mk
α : Type u_2
β : Type u_1
γ : Type ?u.4496
H : (Nonempty β → ¬Infinite α) ∧ (Nonempty α → ¬Infinite β)
H' : Infinite (α × β)
a : α
b : β
this✝ : Fintype α
this : Fintype β
⊢ False
exact H'.false