[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ t✝ s : Set α
t : Set β
inst✝² : Fintype ↑s
inst✝¹ : Fintype ↑t
inst✝ : Fintype ↑(s ×ˢ t)
⊢ toFinset (s ×ˢ t) = toFinset s ×ˢ toFinset t
[PROOFSTEP]
ext
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ t✝ s : Set α
t : Set β
inst✝² : Fintype ↑s
inst✝¹ : Fintype ↑t
inst✝ : Fintype ↑(s ×ˢ t)
a✝ : α × β
⊢ a✝ ∈ toFinset (s ×ˢ t) ↔ a✝ ∈ toFinset s ×ˢ toFinset t
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ t s : Set α
inst✝² : DecidableEq α
inst✝¹ : Fintype ↑s
inst✝ : Fintype ↑(offDiag s)
⊢ ∀ (a : α × α), a ∈ toFinset (offDiag s) ↔ a ∈ Finset.offDiag (toFinset s)
[PROOFSTEP]
simp
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Fintype α
inst✝ : Fintype β
x✝ : α × β
a : α
b : β
⊢ (a, b) ∈ univ ×ˢ univ
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ Infinite (α × β) ↔ Infinite α ∧ Nonempty β ∨ Nonempty α ∧ Infinite β
[PROOFSTEP]
refine'
  ⟨fun H => _, fun H => H.elim (and_imp.2 <| @Prod.infinite_of_left α β) (and_imp.2 <| @Prod.infinite_of_right α β)⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
H : Infinite (α × β)
⊢ Infinite α ∧ Nonempty β ∨ Nonempty α ∧ Infinite β
[PROOFSTEP]
rw [and_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
H : Infinite (α × β)
⊢ Nonempty β ∧ Infinite α ∨ Nonempty α ∧ Infinite β
[PROOFSTEP]
contrapose! H
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
H : (Nonempty β → ¬Infinite α) ∧ (Nonempty α → ¬Infinite β)
⊢ ¬Infinite (α × β)
[PROOFSTEP]
intro H'
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
H : (Nonempty β → ¬Infinite α) ∧ (Nonempty α → ¬Infinite β)
H' : Infinite (α × β)
⊢ False
[PROOFSTEP]
rcases Infinite.nonempty (α × β) with ⟨a, b⟩
[GOAL]
case intro.mk
α : Type u_1
β : Type u_2
γ : Type u_3
H : (Nonempty β → ¬Infinite α) ∧ (Nonempty α → ¬Infinite β)
H' : Infinite (α × β)
a : α
b : β
⊢ False
[PROOFSTEP]
haveI := fintypeOfNotInfinite (H.1 ⟨b⟩)
[GOAL]
case intro.mk
α : Type u_1
β : Type u_2
γ : Type u_3
H : (Nonempty β → ¬Infinite α) ∧ (Nonempty α → ¬Infinite β)
H' : Infinite (α × β)
a : α
b : β
this : Fintype α
⊢ False
[PROOFSTEP]
haveI := fintypeOfNotInfinite (H.2 ⟨a⟩)
[GOAL]
case intro.mk
α : Type u_1
β : Type u_2
γ : Type u_3
H : (Nonempty β → ¬Infinite α) ∧ (Nonempty α → ¬Infinite β)
H' : Infinite (α × β)
a : α
b : β
this✝ : Fintype α
this : Fintype β
⊢ False
[PROOFSTEP]
exact H'.false
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : ι → Type ?u.4746
inst✝¹ : ∀ (i : ι), Nontrivial (π i)
inst✝ : Infinite ι
⊢ Infinite ((i : ι) → π i)
[PROOFSTEP]
choose m n hm using fun i => exists_pair_ne (π i)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : ι → Type ?u.4746
inst✝¹ : ∀ (i : ι), Nontrivial (π i)
inst✝ : Infinite ι
m n : (i : ι) → π i
hm : ∀ (i : ι), m i ≠ n i
⊢ Infinite ((i : ι) → π i)
[PROOFSTEP]
refine' Infinite.of_injective (fun i => update m i (n i)) fun x y h => of_not_not fun hne => _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : ι → Type ?u.4746
inst✝¹ : ∀ (i : ι), Nontrivial (π i)
inst✝ : Infinite ι
m n : (i : ι) → π i
hm : ∀ (i : ι), m i ≠ n i
x y : ι
h : (fun i => update m i (n i)) x = (fun i => update m i (n i)) y
hne : ¬x = y
⊢ False
[PROOFSTEP]
simp_rw [update_eq_iff, update_noteq hne] at h 
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : ι → Type ?u.4746
inst✝¹ : ∀ (i : ι), Nontrivial (π i)
inst✝ : Infinite ι
m n : (i : ι) → π i
hm : ∀ (i : ι), m i ≠ n i
x y : ι
hne : ¬x = y
h : n x = m x ∧ ∀ (x_1 : ι), x_1 ≠ x → m x_1 = update m y (n y) x_1
⊢ False
[PROOFSTEP]
exact (hm x h.1.symm).elim
