case refine'_1
α : Type u
β : Type v
ι : Sort w
γ : Type x
f : α → β → γ
s : Set α
t : Set β
a : α
b : β
hfs : ∀ (b : β), b ∈ t → InjOn (fun a => f a b) s
hft : ∀ (a : α), a ∈ s → InjOn (f a) t
h : Set.Infinite (image2 f s t)
⊢ Set.Infinite (s ×ˢ t)

case refine'_2
α : Type u
β : Type v
ι : Sort w
γ : Type x
f : α → β → γ
s : Set α
t : Set β
a : α
b : β
hfs : ∀ (b : β), b ∈ t → InjOn (fun a => f a b) s
hft : ∀ (a : α), a ∈ s → InjOn (f a) t
⊢ Set.Infinite s ∧ Set.Nonempty t ∨ Set.Infinite t ∧ Set.Nonempty s → Set.Infinite (image2 f s t)
α : Type u
β : Type v
ι : Sort w
γ : Type x
f : α → β → γ
s : Set α
t : Set β
a : α
b : β
hfs : ∀ (b : β), b ∈ t → InjOn (fun a => f a b) s
hft : ∀ (a : α), a ∈ s → InjOn (f a) t
⊢ Set.Infinite (image2 f s t) ↔ Set.Infinite s ∧ Set.Nonempty t ∨ Set.Infinite t ∧ Set.Nonempty s
refine' ⟨fun h => Set.infinite_prod.1 _, _⟩
case refine'_1
α : Type u
β : Type v
ι : Sort w
γ : Type x
f : α → β → γ
s : Set α
t : Set β
a : α
b : β
hfs : ∀ (b : β), b ∈ t → InjOn (fun a => f a b) s
hft : ∀ (a : α), a ∈ s → InjOn (f a) t
h : Set.Infinite (uncurry f '' s ×ˢ t)
⊢ Set.Infinite (s ×ˢ t)
case refine'_1
α : Type u
β : Type v
ι : Sort w
γ : Type x
f : α → β → γ
s : Set α
t : Set β
a : α
b : β
hfs : ∀ (b : β), b ∈ t → InjOn (fun a => f a b) s
hft : ∀ (a : α), a ∈ s → InjOn (f a) t
h : Set.Infinite (image2 f s t)
⊢ Set.Infinite (s ×ˢ t)
rw [← image_uncurry_prod] at h
no goals
case refine'_1
α : Type u
β : Type v
ι : Sort w
γ : Type x
f : α → β → γ
s : Set α
t : Set β
a : α
b : β
hfs : ∀ (b : β), b ∈ t → InjOn (fun a => f a b) s
hft : ∀ (a : α), a ∈ s → InjOn (f a) t
h : Set.Infinite (uncurry f '' s ×ˢ t)
⊢ Set.Infinite (s ×ˢ t)
exact h.of_image _
case refine'_2.inl.intro.intro
α : Type u
β : Type v
ι : Sort w
γ : Type x
f : α → β → γ
s : Set α
t : Set β
a : α
b✝ : β
hfs : ∀ (b : β), b ∈ t → InjOn (fun a => f a b) s
hft : ∀ (a : α), a ∈ s → InjOn (f a) t
hs : Set.Infinite s
b : β
hb : b ∈ t
⊢ Set.Infinite (image2 f s t)

case refine'_2.inr.intro.intro
α : Type u
β : Type v
ι : Sort w
γ : Type x
f : α → β → γ
s : Set α
t : Set β
a✝ : α
b : β
hfs : ∀ (b : β), b ∈ t → InjOn (fun a => f a b) s
hft : ∀ (a : α), a ∈ s → InjOn (f a) t
ht : Set.Infinite t
a : α
ha : a ∈ s
⊢ Set.Infinite (image2 f s t)
case refine'_2
α : Type u
β : Type v
ι : Sort w
γ : Type x
f : α → β → γ
s : Set α
t : Set β
a : α
b : β
hfs : ∀ (b : β), b ∈ t → InjOn (fun a => f a b) s
hft : ∀ (a : α), a ∈ s → InjOn (f a) t
⊢ Set.Infinite s ∧ Set.Nonempty t ∨ Set.Infinite t ∧ Set.Nonempty s → Set.Infinite (image2 f s t)
rintro (⟨hs, b, hb⟩ | ⟨ht, a, ha⟩)
no goals
case refine'_2.inl.intro.intro
α : Type u
β : Type v
ι : Sort w
γ : Type x
f : α → β → γ
s : Set α
t : Set β
a : α
b✝ : β
hfs : ∀ (b : β), b ∈ t → InjOn (fun a => f a b) s
hft : ∀ (a : α), a ∈ s → InjOn (f a) t
hs : Set.Infinite s
b : β
hb : b ∈ t
⊢ Set.Infinite (image2 f s t)
exact hs.image2_left hb (hfs _ hb)
no goals
case refine'_2.inr.intro.intro
α : Type u
β : Type v
ι : Sort w
γ : Type x
f : α → β → γ
s : Set α
t : Set β
a✝ : α
b : β
hfs : ∀ (b : β), b ∈ t → InjOn (fun a => f a b) s
hft : ∀ (a : α), a ∈ s → InjOn (f a) t
ht : Set.Infinite t
a : α
ha : a ∈ s
⊢ Set.Infinite (image2 f s t)
exact ht.image2_right ha (hft _ ha)