no goals
α : Type u_1
β : Type u_2
γ : Type ?u.83632
inst✝¹ : Infinite α
inst✝ : Finite β
f : α → β
⊢ ∃ y, Infinite ↑(f ⁻¹' {y})
classical
  by_contra' hf
  cases nonempty_fintype β
  haveI := fun y => fintypeOfNotInfinite <| hf y
  let key : Fintype α :=
    { elems := univ.biUnion fun y : β => (f ⁻¹' {y}).toFinset
      complete := by simp }
  exact key.false
α : Type u_1
β : Type u_2
γ : Type ?u.83632
inst✝¹ : Infinite α
inst✝ : Finite β
f : α → β
hf : ∀ (y : β), ¬Infinite ↑(f ⁻¹' {y})
⊢ False
α : Type u_1
β : Type u_2
γ : Type ?u.83632
inst✝¹ : Infinite α
inst✝ : Finite β
f : α → β
⊢ ∃ y, Infinite ↑(f ⁻¹' {y})
by_contra' hf
case intro
α : Type u_1
β : Type u_2
γ : Type ?u.83632
inst✝¹ : Infinite α
inst✝ : Finite β
f : α → β
hf : ∀ (y : β), ¬Infinite ↑(f ⁻¹' {y})
val✝ : Fintype β
⊢ False
α : Type u_1
β : Type u_2
γ : Type ?u.83632
inst✝¹ : Infinite α
inst✝ : Finite β
f : α → β
hf : ∀ (y : β), ¬Infinite ↑(f ⁻¹' {y})
⊢ False
cases nonempty_fintype β
case intro
α : Type u_1
β : Type u_2
γ : Type ?u.83632
inst✝¹ : Infinite α
inst✝ : Finite β
f : α → β
hf : ∀ (y : β), ¬Infinite ↑(f ⁻¹' {y})
val✝ : Fintype β
this : (y : β) → Fintype ↑(f ⁻¹' {y})
⊢ False
case intro
α : Type u_1
β : Type u_2
γ : Type ?u.83632
inst✝¹ : Infinite α
inst✝ : Finite β
f : α → β
hf : ∀ (y : β), ¬Infinite ↑(f ⁻¹' {y})
val✝ : Fintype β
⊢ False
haveI := fun y => fintypeOfNotInfinite <| hf y
case intro
α : Type u_1
β : Type u_2
γ : Type ?u.83632
inst✝¹ : Infinite α
inst✝ : Finite β
f : α → β
hf : ∀ (y : β), ¬Infinite ↑(f ⁻¹' {y})
val✝ : Fintype β
this : (y : β) → Fintype ↑(f ⁻¹' {y})
key : Fintype α :=
  { elems := Finset.biUnion univ fun y => Set.toFinset (f ⁻¹' {y}),
    complete := (_ : ∀ (a : α), a ∈ Finset.biUnion univ fun y => Set.toFinset (f ⁻¹' {y})) }
⊢ False
case intro
α : Type u_1
β : Type u_2
γ : Type ?u.83632
inst✝¹ : Infinite α
inst✝ : Finite β
f : α → β
hf : ∀ (y : β), ¬Infinite ↑(f ⁻¹' {y})
val✝ : Fintype β
this : (y : β) → Fintype ↑(f ⁻¹' {y})
⊢ False
let key : Fintype α :=
  { elems := univ.biUnion fun y : β => (f ⁻¹' {y}).toFinset
    complete := by simp }
no goals
case intro
α : Type u_1
β : Type u_2
γ : Type ?u.83632
inst✝¹ : Infinite α
inst✝ : Finite β
f : α → β
hf : ∀ (y : β), ¬Infinite ↑(f ⁻¹' {y})
val✝ : Fintype β
this : (y : β) → Fintype ↑(f ⁻¹' {y})
key : Fintype α :=
  { elems := Finset.biUnion univ fun y => Set.toFinset (f ⁻¹' {y}),
    complete := (_ : ∀ (a : α), a ∈ Finset.biUnion univ fun y => Set.toFinset (f ⁻¹' {y})) }
⊢ False
exact key.false
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.83632
inst✝¹ : Infinite α
inst✝ : Finite β
f : α → β
hf : ∀ (y : β), ¬Infinite ↑(f ⁻¹' {y})
val✝ : Fintype β
this : (y : β) → Fintype ↑(f ⁻¹' {y})
⊢ ∀ (x : α), x ∈ Finset.biUnion univ fun y => Set.toFinset (f ⁻¹' {y})
simp