α✝ : Type ?u.149865
r : α✝ → α✝ → Prop
α : Type u_1
β : Type u_2
inst✝ : Infinite β
f : α → Finset β
w : (⋃ (a : α), ↑(f a)) = ⊤
k : Infinite ↑(range f)
⊢ (#β) ≤ (#↑(range f))
α✝ : Type ?u.149865
r : α✝ → α✝ → Prop
α : Type u_1
β : Type u_2
inst✝ : Infinite β
f : α → Finset β
w : (⋃ (a : α), ↑(f a)) = ⊤
⊢ (#β) ≤ (#↑(range f))
have k : _root_.Infinite (range f) := by
  rw [infinite_coe_iff]
  apply mt (union_finset_finite_of_range_finite f)
  rw [w]
  exact infinite_univ
α✝ : Type ?u.149865
r : α✝ → α✝ → Prop
α : Type u_1
β : Type u_2
inst✝ : Infinite β
f : α → Finset β
w : (⋃ (a : α), ↑(f a)) = ⊤
k : Infinite ↑(range f)
h : ¬(#β) ≤ (#↑(range f))
⊢ False
α✝ : Type ?u.149865
r : α✝ → α✝ → Prop
α : Type u_1
β : Type u_2
inst✝ : Infinite β
f : α → Finset β
w : (⋃ (a : α), ↑(f a)) = ⊤
k : Infinite ↑(range f)
⊢ (#β) ≤ (#↑(range f))
by_contra h
α✝ : Type ?u.149865
r : α✝ → α✝ → Prop
α : Type u_1
β : Type u_2
inst✝ : Infinite β
f : α → Finset β
w : (⋃ (a : α), ↑(f a)) = ⊤
k : Infinite ↑(range f)
h : (#↑(range f)) < (#β)
⊢ False
α✝ : Type ?u.149865
r : α✝ → α✝ → Prop
α : Type u_1
β : Type u_2
inst✝ : Infinite β
f : α → Finset β
w : (⋃ (a : α), ↑(f a)) = ⊤
k : Infinite ↑(range f)
h : ¬(#β) ≤ (#↑(range f))
⊢ False
simp only [not_le] at h
α✝ : Type ?u.149865
r : α✝ → α✝ → Prop
α : Type u_1
β : Type u_2
inst✝ : Infinite β
f : α → Finset β
w : (⋃ (a : α), ↑(f a)) = ⊤
k : Infinite ↑(range f)
h : (#↑(range f)) < (#β)
u : ∀ (b : β), ∃ a, b ∈ f a :=
  fun b =>
    Eq.mp
      (Eq.trans Mathlib.Data.Set.Lattice._auxLemma.3
        (congrArg Exists (funext fun i => Mathlib.Data.Finset.Basic._auxLemma.4)))
      (Eq.ge w (mem_univ b))
⊢ False
α✝ : Type ?u.149865
r : α✝ → α✝ → Prop
α : Type u_1
β : Type u_2
inst✝ : Infinite β
f : α → Finset β
w : (⋃ (a : α), ↑(f a)) = ⊤
k : Infinite ↑(range f)
h : (#↑(range f)) < (#β)
⊢ False
let u : ∀ b, ∃ a, b ∈ f a := fun b => by simpa using (w.ge : _) (Set.mem_univ b)
α✝ : Type ?u.149865
r : α✝ → α✝ → Prop
α : Type u_1
β : Type u_2
inst✝ : Infinite β
f : α → Finset β
w : (⋃ (a : α), ↑(f a)) = ⊤
k : Infinite ↑(range f)
h : (#↑(range f)) < (#β)
u : ∀ (b : β), ∃ a, b ∈ f a :=
  fun b =>
    Eq.mp
      (Eq.trans Mathlib.Data.Set.Lattice._auxLemma.3
        (congrArg Exists (funext fun i => Mathlib.Data.Finset.Basic._auxLemma.4)))
      (Eq.ge w (mem_univ b))
u' : β → ↑(range f) :=
  fun b =>
    { val := f (Exists.choose (_ : ∃ a, b ∈ f a)), property := (_ : f (Exists.choose (_ : ∃ a, b ∈ f a)) ∈ range f) }
⊢ False
α✝ : Type ?u.149865
r : α✝ → α✝ → Prop
α : Type u_1
β : Type u_2
inst✝ : Infinite β
f : α → Finset β
w : (⋃ (a : α), ↑(f a)) = ⊤
k : Infinite ↑(range f)
h : (#↑(range f)) < (#β)
u : ∀ (b : β), ∃ a, b ∈ f a :=
  fun b =>
    Eq.mp
      (Eq.trans Mathlib.Data.Set.Lattice._auxLemma.3
        (congrArg Exists (funext fun i => Mathlib.Data.Finset.Basic._auxLemma.4)))
      (Eq.ge w (mem_univ b))
⊢ False
let u' : β → range f := fun b => ⟨f (u b).choose, by simp⟩
α✝ : Type ?u.149865
r : α✝ → α✝ → Prop
α : Type u_1
β : Type u_2
inst✝ : Infinite β
f : α → Finset β
w : (⋃ (a : α), ↑(f a)) = ⊤
k : Infinite ↑(range f)
h : (#↑(range f)) < (#β)
u : ∀ (b : β), ∃ a, b ∈ f a :=
  fun b =>
    Eq.mp
      (Eq.trans Mathlib.Data.Set.Lattice._auxLemma.3
        (congrArg Exists (funext fun i => Mathlib.Data.Finset.Basic._auxLemma.4)))
      (Eq.ge w (mem_univ b))
u' : β → ↑(range f) :=
  fun b =>
    { val := f (Exists.choose (_ : ∃ a, b ∈ f a)), property := (_ : f (Exists.choose (_ : ∃ a, b ∈ f a)) ∈ range f) }
v' : ∀ (a : α), u' ⁻¹' {{ val := f a, property := (_ : f a ∈ range f) }} ≤ ↑(f a)
⊢ False
α✝ : Type ?u.149865
r : α✝ → α✝ → Prop
α : Type u_1
β : Type u_2
inst✝ : Infinite β
f : α → Finset β
w : (⋃ (a : α), ↑(f a)) = ⊤
k : Infinite ↑(range f)
h : (#↑(range f)) < (#β)
u : ∀ (b : β), ∃ a, b ∈ f a :=
  fun b =>
    Eq.mp
      (Eq.trans Mathlib.Data.Set.Lattice._auxLemma.3
        (congrArg Exists (funext fun i => Mathlib.Data.Finset.Basic._auxLemma.4)))
      (Eq.ge w (mem_univ b))
u' : β → ↑(range f) :=
  fun b =>
    { val := f (Exists.choose (_ : ∃ a, b ∈ f a)), property := (_ : f (Exists.choose (_ : ∃ a, b ∈ f a)) ∈ range f) }
⊢ False
have v' : ∀ a, u' ⁻¹' {⟨f a, by simp⟩} ≤ f a := by
  rintro a p m
  simp at m
  rw [← m]
  apply fun b => (u b).choose_spec
case intro.mk.intro
α✝ : Type ?u.149865
r : α✝ → α✝ → Prop
α : Type u_1
β : Type u_2
inst✝ : Infinite β
f : α → Finset β
w : (⋃ (a : α), ↑(f a)) = ⊤
k : Infinite ↑(range f)
h : (#↑(range f)) < (#β)
u : ∀ (b : β), ∃ a, b ∈ f a :=
  fun b =>
    Eq.mp
      (Eq.trans Mathlib.Data.Set.Lattice._auxLemma.3
        (congrArg Exists (funext fun i => Mathlib.Data.Finset.Basic._auxLemma.4)))
      (Eq.ge w (mem_univ b))
u' : β → ↑(range f) :=
  fun b =>
    { val := f (Exists.choose (_ : ∃ a, b ∈ f a)), property := (_ : f (Exists.choose (_ : ∃ a, b ∈ f a)) ∈ range f) }
v' : ∀ (a : α), u' ⁻¹' {{ val := f a, property := (_ : f a ∈ range f) }} ≤ ↑(f a)
a : α
p : Infinite ↑(u' ⁻¹' {{ val := f a, property := (_ : ∃ y, f y = f a) }})
⊢ False
α✝ : Type ?u.149865
r : α✝ → α✝ → Prop
α : Type u_1
β : Type u_2
inst✝ : Infinite β
f : α → Finset β
w : (⋃ (a : α), ↑(f a)) = ⊤
k : Infinite ↑(range f)
h : (#↑(range f)) < (#β)
u : ∀ (b : β), ∃ a, b ∈ f a :=
  fun b =>
    Eq.mp
      (Eq.trans Mathlib.Data.Set.Lattice._auxLemma.3
        (congrArg Exists (funext fun i => Mathlib.Data.Finset.Basic._auxLemma.4)))
      (Eq.ge w (mem_univ b))
u' : β → ↑(range f) :=
  fun b =>
    { val := f (Exists.choose (_ : ∃ a, b ∈ f a)), property := (_ : f (Exists.choose (_ : ∃ a, b ∈ f a)) ∈ range f) }
v' : ∀ (a : α), u' ⁻¹' {{ val := f a, property := (_ : f a ∈ range f) }} ≤ ↑(f a)
⊢ False
obtain ⟨⟨-, ⟨a, rfl⟩⟩, p⟩ := exists_infinite_fiber u' h k
no goals
case intro.mk.intro
α✝ : Type ?u.149865
r : α✝ → α✝ → Prop
α : Type u_1
β : Type u_2
inst✝ : Infinite β
f : α → Finset β
w : (⋃ (a : α), ↑(f a)) = ⊤
k : Infinite ↑(range f)
h : (#↑(range f)) < (#β)
u : ∀ (b : β), ∃ a, b ∈ f a :=
  fun b =>
    Eq.mp
      (Eq.trans Mathlib.Data.Set.Lattice._auxLemma.3
        (congrArg Exists (funext fun i => Mathlib.Data.Finset.Basic._auxLemma.4)))
      (Eq.ge w (mem_univ b))
u' : β → ↑(range f) :=
  fun b =>
    { val := f (Exists.choose (_ : ∃ a, b ∈ f a)), property := (_ : f (Exists.choose (_ : ∃ a, b ∈ f a)) ∈ range f) }
v' : ∀ (a : α), u' ⁻¹' {{ val := f a, property := (_ : f a ∈ range f) }} ≤ ↑(f a)
a : α
p : Infinite ↑(u' ⁻¹' {{ val := f a, property := (_ : ∃ y, f y = f a) }})
⊢ False
exact (@Infinite.of_injective _ _ p (inclusion (v' a)) (inclusion_injective _)).false
α✝ : Type ?u.149865
r : α✝ → α✝ → Prop
α : Type u_1
β : Type u_2
inst✝ : Infinite β
f : α → Finset β
w : (⋃ (a : α), ↑(f a)) = ⊤
⊢ Set.Infinite (range f)
α✝ : Type ?u.149865
r : α✝ → α✝ → Prop
α : Type u_1
β : Type u_2
inst✝ : Infinite β
f : α → Finset β
w : (⋃ (a : α), ↑(f a)) = ⊤
⊢ Infinite ↑(range f)
rw [infinite_coe_iff]
α✝ : Type ?u.149865
r : α✝ → α✝ → Prop
α : Type u_1
β : Type u_2
inst✝ : Infinite β
f : α → Finset β
w : (⋃ (a : α), ↑(f a)) = ⊤
⊢ ¬Set.Finite (⋃ (a : α), ↑(f a))
α✝ : Type ?u.149865
r : α✝ → α✝ → Prop
α : Type u_1
β : Type u_2
inst✝ : Infinite β
f : α → Finset β
w : (⋃ (a : α), ↑(f a)) = ⊤
⊢ Set.Infinite (range f)
apply mt (union_finset_finite_of_range_finite f)
α✝ : Type ?u.149865
r : α✝ → α✝ → Prop
α : Type u_1
β : Type u_2
inst✝ : Infinite β
f : α → Finset β
w : (⋃ (a : α), ↑(f a)) = ⊤
⊢ ¬Set.Finite ⊤
α✝ : Type ?u.149865
r : α✝ → α✝ → Prop
α : Type u_1
β : Type u_2
inst✝ : Infinite β
f : α → Finset β
w : (⋃ (a : α), ↑(f a)) = ⊤
⊢ ¬Set.Finite (⋃ (a : α), ↑(f a))
rw [w]
no goals
α✝ : Type ?u.149865
r : α✝ → α✝ → Prop
α : Type u_1
β : Type u_2
inst✝ : Infinite β
f : α → Finset β
w : (⋃ (a : α), ↑(f a)) = ⊤
⊢ ¬Set.Finite ⊤
exact infinite_univ
no goals
α✝ : Type ?u.149865
r : α✝ → α✝ → Prop
α : Type u_1
β : Type u_2
inst✝ : Infinite β
f : α → Finset β
w : (⋃ (a : α), ↑(f a)) = ⊤
k : Infinite ↑(range f)
h : (#↑(range f)) < (#β)
b : β
⊢ ∃ a, b ∈ f a
simpa using (w.ge : _) (Set.mem_univ b)
no goals
α✝ : Type ?u.149865
r : α✝ → α✝ → Prop
α : Type u_1
β : Type u_2
inst✝ : Infinite β
f : α → Finset β
w : (⋃ (a : α), ↑(f a)) = ⊤
k : Infinite ↑(range f)
h : (#↑(range f)) < (#β)
u : ∀ (b : β), ∃ a, b ∈ f a :=
  fun b =>
    Eq.mp
      (Eq.trans Mathlib.Data.Set.Lattice._auxLemma.3
        (congrArg Exists (funext fun i => Mathlib.Data.Finset.Basic._auxLemma.4)))
      (Eq.ge w (mem_univ b))
b : β
⊢ f (Exists.choose (_ : ∃ a, b ∈ f a)) ∈ range f
simp
no goals
α✝ : Type ?u.149865
r : α✝ → α✝ → Prop
α : Type u_1
β : Type u_2
inst✝ : Infinite β
f : α → Finset β
w : (⋃ (a : α), ↑(f a)) = ⊤
k : Infinite ↑(range f)
h : (#↑(range f)) < (#β)
u : ∀ (b : β), ∃ a, b ∈ f a :=
  fun b =>
    Eq.mp
      (Eq.trans Mathlib.Data.Set.Lattice._auxLemma.3
        (congrArg Exists (funext fun i => Mathlib.Data.Finset.Basic._auxLemma.4)))
      (Eq.ge w (mem_univ b))
u' : β → ↑(range f) :=
  fun b =>
    { val := f (Exists.choose (_ : ∃ a, b ∈ f a)), property := (_ : f (Exists.choose (_ : ∃ a, b ∈ f a)) ∈ range f) }
a : α
⊢ f a ∈ range f
simp
α✝ : Type ?u.149865
r : α✝ → α✝ → Prop
α : Type u_1
β : Type u_2
inst✝ : Infinite β
f : α → Finset β
w : (⋃ (a : α), ↑(f a)) = ⊤
k : Infinite ↑(range f)
h : (#↑(range f)) < (#β)
u : ∀ (b : β), ∃ a, b ∈ f a :=
  fun b =>
    Eq.mp
      (Eq.trans Mathlib.Data.Set.Lattice._auxLemma.3
        (congrArg Exists (funext fun i => Mathlib.Data.Finset.Basic._auxLemma.4)))
      (Eq.ge w (mem_univ b))
u' : β → ↑(range f) :=
  fun b =>
    { val := f (Exists.choose (_ : ∃ a, b ∈ f a)), property := (_ : f (Exists.choose (_ : ∃ a, b ∈ f a)) ∈ range f) }
a : α
p : β
m : p ∈ u' ⁻¹' {{ val := f a, property := (_ : f a ∈ range f) }}
⊢ p ∈ ↑(f a)
α✝ : Type ?u.149865
r : α✝ → α✝ → Prop
α : Type u_1
β : Type u_2
inst✝ : Infinite β
f : α → Finset β
w : (⋃ (a : α), ↑(f a)) = ⊤
k : Infinite ↑(range f)
h : (#↑(range f)) < (#β)
u : ∀ (b : β), ∃ a, b ∈ f a :=
  fun b =>
    Eq.mp
      (Eq.trans Mathlib.Data.Set.Lattice._auxLemma.3
        (congrArg Exists (funext fun i => Mathlib.Data.Finset.Basic._auxLemma.4)))
      (Eq.ge w (mem_univ b))
u' : β → ↑(range f) :=
  fun b =>
    { val := f (Exists.choose (_ : ∃ a, b ∈ f a)), property := (_ : f (Exists.choose (_ : ∃ a, b ∈ f a)) ∈ range f) }
⊢ ∀ (a : α), u' ⁻¹' {{ val := f a, property := (_ : f a ∈ range f) }} ≤ ↑(f a)
rintro a p m
α✝ : Type ?u.149865
r : α✝ → α✝ → Prop
α : Type u_1
β : Type u_2
inst✝ : Infinite β
f : α → Finset β
w : (⋃ (a : α), ↑(f a)) = ⊤
k : Infinite ↑(range f)
h : (#↑(range f)) < (#β)
u : ∀ (b : β), ∃ a, b ∈ f a :=
  fun b =>
    Eq.mp
      (Eq.trans Mathlib.Data.Set.Lattice._auxLemma.3
        (congrArg Exists (funext fun i => Mathlib.Data.Finset.Basic._auxLemma.4)))
      (Eq.ge w (mem_univ b))
u' : β → ↑(range f) :=
  fun b =>
    { val := f (Exists.choose (_ : ∃ a, b ∈ f a)), property := (_ : f (Exists.choose (_ : ∃ a, b ∈ f a)) ∈ range f) }
a : α
p : β
m : f (Exists.choose (_ : ∃ a, p ∈ f a)) = f a
⊢ p ∈ ↑(f a)
α✝ : Type ?u.149865
r : α✝ → α✝ → Prop
α : Type u_1
β : Type u_2
inst✝ : Infinite β
f : α → Finset β
w : (⋃ (a : α), ↑(f a)) = ⊤
k : Infinite ↑(range f)
h : (#↑(range f)) < (#β)
u : ∀ (b : β), ∃ a, b ∈ f a :=
  fun b =>
    Eq.mp
      (Eq.trans Mathlib.Data.Set.Lattice._auxLemma.3
        (congrArg Exists (funext fun i => Mathlib.Data.Finset.Basic._auxLemma.4)))
      (Eq.ge w (mem_univ b))
u' : β → ↑(range f) :=
  fun b =>
    { val := f (Exists.choose (_ : ∃ a, b ∈ f a)), property := (_ : f (Exists.choose (_ : ∃ a, b ∈ f a)) ∈ range f) }
a : α
p : β
m : p ∈ u' ⁻¹' {{ val := f a, property := (_ : f a ∈ range f) }}
⊢ p ∈ ↑(f a)
simp at m
α✝ : Type ?u.149865
r : α✝ → α✝ → Prop
α : Type u_1
β : Type u_2
inst✝ : Infinite β
f : α → Finset β
w : (⋃ (a : α), ↑(f a)) = ⊤
k : Infinite ↑(range f)
h : (#↑(range f)) < (#β)
u : ∀ (b : β), ∃ a, b ∈ f a :=
  fun b =>
    Eq.mp
      (Eq.trans Mathlib.Data.Set.Lattice._auxLemma.3
        (congrArg Exists (funext fun i => Mathlib.Data.Finset.Basic._auxLemma.4)))
      (Eq.ge w (mem_univ b))
u' : β → ↑(range f) :=
  fun b =>
    { val := f (Exists.choose (_ : ∃ a, b ∈ f a)), property := (_ : f (Exists.choose (_ : ∃ a, b ∈ f a)) ∈ range f) }
a : α
p : β
m : f (Exists.choose (_ : ∃ a, p ∈ f a)) = f a
⊢ p ∈ ↑(f (Exists.choose (_ : ∃ a, p ∈ f a)))
α✝ : Type ?u.149865
r : α✝ → α✝ → Prop
α : Type u_1
β : Type u_2
inst✝ : Infinite β
f : α → Finset β
w : (⋃ (a : α), ↑(f a)) = ⊤
k : Infinite ↑(range f)
h : (#↑(range f)) < (#β)
u : ∀ (b : β), ∃ a, b ∈ f a :=
  fun b =>
    Eq.mp
      (Eq.trans Mathlib.Data.Set.Lattice._auxLemma.3
        (congrArg Exists (funext fun i => Mathlib.Data.Finset.Basic._auxLemma.4)))
      (Eq.ge w (mem_univ b))
u' : β → ↑(range f) :=
  fun b =>
    { val := f (Exists.choose (_ : ∃ a, b ∈ f a)), property := (_ : f (Exists.choose (_ : ∃ a, b ∈ f a)) ∈ range f) }
a : α
p : β
m : f (Exists.choose (_ : ∃ a, p ∈ f a)) = f a
⊢ p ∈ ↑(f a)
rw [← m]
no goals
α✝ : Type ?u.149865
r : α✝ → α✝ → Prop
α : Type u_1
β : Type u_2
inst✝ : Infinite β
f : α → Finset β
w : (⋃ (a : α), ↑(f a)) = ⊤
k : Infinite ↑(range f)
h : (#↑(range f)) < (#β)
u : ∀ (b : β), ∃ a, b ∈ f a :=
  fun b =>
    Eq.mp
      (Eq.trans Mathlib.Data.Set.Lattice._auxLemma.3
        (congrArg Exists (funext fun i => Mathlib.Data.Finset.Basic._auxLemma.4)))
      (Eq.ge w (mem_univ b))
u' : β → ↑(range f) :=
  fun b =>
    { val := f (Exists.choose (_ : ∃ a, b ∈ f a)), property := (_ : f (Exists.choose (_ : ∃ a, b ∈ f a)) ∈ range f) }
a : α
p : β
m : f (Exists.choose (_ : ∃ a, p ∈ f a)) = f a
⊢ p ∈ ↑(f (Exists.choose (_ : ∃ a, p ∈ f a)))
apply fun b => (u b).choose_spec