-- Mathlib/SetTheory/Cardinal/Cofinality.lean
theorem le_range_of_union_finset_eq_top {α β : Type*} [Infinite β] (f : α → Finset β)
    (w : ⋃ a, (f a : Set β) = ⊤) : #β ≤ #(range f)

Proof state:
α : 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.Order.SetNotation._auxLemma.3
        (congrArg Exists (funext fun i => Mathlib.Data.Finset.Defs._auxLemma.6)))
      (Eq.ge w (mem_univ b))
u' : β → ↑(range f) := fun b => ⟨f ⋯.choose, ⋯⟩
v' : ∀ (a : α), u' ⁻¹' {⟨f a, ⋯⟩} ≤ ↑(f a)
⊢ False

Tactic:
obtain ⟨⟨-, ⟨a, rfl⟩⟩, p⟩ := exists_infinite_fiber u' h k

Result:
case intro.mk.intro
α : 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.Order.SetNotation._auxLemma.3
        (congrArg Exists (funext fun i => Mathlib.Data.Finset.Defs._auxLemma.6)))
      (Eq.ge w (mem_univ b))
u' : β → ↑(range f) := fun b => ⟨f ⋯.choose, ⋯⟩
v' : ∀ (a : α), u' ⁻¹' {⟨f a, ⋯⟩} ≤ ↑(f a)
a : α
p : Infinite ↑(u' ⁻¹' {⟨f a, ⋯⟩})
⊢ False

Proof state:
α : 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.Order.SetNotation._auxLemma.3
        (congrArg Exists (funext fun i => Mathlib.Data.Finset.Defs._auxLemma.6)))
      (Eq.ge w (mem_univ b))
u' : β → ↑(range f) := fun b => ⟨f ⋯.choose, ⋯⟩
⊢ False

Tactic:
have v' : ∀ a, u' ⁻¹' {⟨f a, by simp⟩} ≤ f a := by
  rintro a p m
  simp? [u']  at m says simp only [mem_preimage, mem_singleton_iff, Subtype.mk.injEq, u'] at m
  rw [← m]
  apply fun b => (u b).choose_spec

Result:
α : 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.Order.SetNotation._auxLemma.3
        (congrArg Exists (funext fun i => Mathlib.Data.Finset.Defs._auxLemma.6)))
      (Eq.ge w (mem_univ b))
u' : β → ↑(range f) := fun b => ⟨f ⋯.choose, ⋯⟩
v' : ∀ (a : α), u' ⁻¹' {⟨f a, ⋯⟩} ≤ ↑(f a)
⊢ False

Proof state:
α : 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.Order.SetNotation._auxLemma.3
        (congrArg Exists (funext fun i => Mathlib.Data.Finset.Defs._auxLemma.6)))
      (Eq.ge w (mem_univ b))
u' : β → ↑(range f) := fun b => ⟨f ⋯.choose, ⋯⟩
a : α
p : β
m : f ⋯.choose = f a
⊢ p ∈ ↑(f a)

Tactic:
rw [← m]

Result:
α : 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.Order.SetNotation._auxLemma.3
        (congrArg Exists (funext fun i => Mathlib.Data.Finset.Defs._auxLemma.6)))
      (Eq.ge w (mem_univ b))
u' : β → ↑(range f) := fun b => ⟨f ⋯.choose, ⋯⟩
a : α
p : β
m : f ⋯.choose = f a
⊢ p ∈ ↑(f ⋯.choose)

Proof state:
α : Type u_1
β : Type u_2
inst✝ : Infinite β
f : α → Finset β
w : ⋃ a, ↑(f a) = ⊤
⊢ Infinite ↑(range f)

Tactic:
rw [infinite_coe_iff]

Result:
α : Type u_1
β : Type u_2
inst✝ : Infinite β
f : α → Finset β
w : ⋃ a, ↑(f a) = ⊤
⊢ (range f).Infinite

Proof state:
α : 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

Tactic:
simpa using (w.ge :) (Set.mem_univ b)

Result:
no goals

Proof state:
α : 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.Order.SetNotation._auxLemma.3
        (congrArg Exists (funext fun i => Mathlib.Data.Finset.Defs._auxLemma.6)))
      (Eq.ge w (mem_univ b))
u' : β → ↑(range f) := fun b => ⟨f ⋯.choose, ⋯⟩
a : α
⊢ f a ∈ range f

Tactic:
simp

Result:
no goals