α✝ : Type ?u.109224
r : α✝ → α✝ → Prop
β α : Type u
f : β → α
h₁ : ℵ₀ ≤ (#β)
h₂ : (#α) < cof (ord (#β))
this : ∃ a, (#β) ≤ (#↑(f ⁻¹' {a}))
⊢ ∃ a, (#↑(f ⁻¹' {a})) = (#β)
α✝ : Type ?u.109224
r : α✝ → α✝ → Prop
β α : Type u
f : β → α
h₁ : ℵ₀ ≤ (#β)
h₂ : (#α) < cof (ord (#β))
⊢ ∃ a, (#↑(f ⁻¹' {a})) = (#β)
have : ∃ a, (#β) ≤ (#f ⁻¹' {a}) := by
  by_contra' h
  apply mk_univ.not_lt
  rw [← preimage_univ, ← iUnion_of_singleton, preimage_iUnion]
  exact
    mk_iUnion_le_sum_mk.trans_lt
      ((sum_le_iSup _).trans_lt <| mul_lt_of_lt h₁ (h₂.trans_le <| cof_ord_le _) (iSup_lt h₂ h))
case intro
α✝ : Type ?u.109224
r : α✝ → α✝ → Prop
β α : Type u
f : β → α
h₁ : ℵ₀ ≤ (#β)
h₂ : (#α) < cof (ord (#β))
x : α
h : (#β) ≤ (#↑(f ⁻¹' {x}))
⊢ ∃ a, (#↑(f ⁻¹' {a})) = (#β)
α✝ : Type ?u.109224
r : α✝ → α✝ → Prop
β α : Type u
f : β → α
h₁ : ℵ₀ ≤ (#β)
h₂ : (#α) < cof (ord (#β))
this : ∃ a, (#β) ≤ (#↑(f ⁻¹' {a}))
⊢ ∃ a, (#↑(f ⁻¹' {a})) = (#β)
cases' this with x h
case intro
α✝ : Type ?u.109224
r : α✝ → α✝ → Prop
β α : Type u
f : β → α
h₁ : ℵ₀ ≤ (#β)
h₂ : (#α) < cof (ord (#β))
x : α
h : (#β) ≤ (#↑(f ⁻¹' {x}))
⊢ (#↑(f ⁻¹' {x})) ≤ (#β)
case intro
α✝ : Type ?u.109224
r : α✝ → α✝ → Prop
β α : Type u
f : β → α
h₁ : ℵ₀ ≤ (#β)
h₂ : (#α) < cof (ord (#β))
x : α
h : (#β) ≤ (#↑(f ⁻¹' {x}))
⊢ ∃ a, (#↑(f ⁻¹' {a})) = (#β)
refine' ⟨x, h.antisymm' _⟩
case intro
α✝ : Type ?u.109224
r : α✝ → α✝ → Prop
β α : Type u
f : β → α
h₁ : ℵ₀ ≤ (#β)
h₂ : (#α) < cof (ord (#β))
x : α
h : (#β) ≤ (#↑(f ⁻¹' {x}))
⊢ ∃ p, (#↑p) = (#↑(f ⁻¹' {x}))
case intro
α✝ : Type ?u.109224
r : α✝ → α✝ → Prop
β α : Type u
f : β → α
h₁ : ℵ₀ ≤ (#β)
h₂ : (#α) < cof (ord (#β))
x : α
h : (#β) ≤ (#↑(f ⁻¹' {x}))
⊢ (#↑(f ⁻¹' {x})) ≤ (#β)
rw [le_mk_iff_exists_set]
no goals
case intro
α✝ : Type ?u.109224
r : α✝ → α✝ → Prop
β α : Type u
f : β → α
h₁ : ℵ₀ ≤ (#β)
h₂ : (#α) < cof (ord (#β))
x : α
h : (#β) ≤ (#↑(f ⁻¹' {x}))
⊢ ∃ p, (#↑p) = (#↑(f ⁻¹' {x}))
exact ⟨_, rfl⟩
α✝ : Type ?u.109224
r : α✝ → α✝ → Prop
β α : Type u
f : β → α
h₁ : ℵ₀ ≤ (#β)
h₂ : (#α) < cof (ord (#β))
h : ∀ (a : α), (#↑(f ⁻¹' {a})) < (#β)
⊢ False
α✝ : Type ?u.109224
r : α✝ → α✝ → Prop
β α : Type u
f : β → α
h₁ : ℵ₀ ≤ (#β)
h₂ : (#α) < cof (ord (#β))
⊢ ∃ a, (#β) ≤ (#↑(f ⁻¹' {a}))
by_contra' h
α✝ : Type ?u.109224
r : α✝ → α✝ → Prop
β α : Type u
f : β → α
h₁ : ℵ₀ ≤ (#β)
h₂ : (#α) < cof (ord (#β))
h : ∀ (a : α), (#↑(f ⁻¹' {a})) < (#β)
⊢ (#↑Set.univ) < (#?m.110149)

α✝ : Type ?u.109224
r : α✝ → α✝ → Prop
β α : Type u
f : β → α
h₁ : ℵ₀ ≤ (#β)
h₂ : (#α) < cof (ord (#β))
h : ∀ (a : α), (#↑(f ⁻¹' {a})) < (#β)
⊢ Type ?u.110148
α✝ : Type ?u.109224
r : α✝ → α✝ → Prop
β α : Type u
f : β → α
h₁ : ℵ₀ ≤ (#β)
h₂ : (#α) < cof (ord (#β))
h : ∀ (a : α), (#↑(f ⁻¹' {a})) < (#β)
⊢ False
apply mk_univ.not_lt
α✝ : Type ?u.109224
r : α✝ → α✝ → Prop
β α : Type u
f : β → α
h₁ : ℵ₀ ≤ (#β)
h₂ : (#α) < cof (ord (#β))
h : ∀ (a : α), (#↑(f ⁻¹' {a})) < (#β)
⊢ (#↑(⋃ (i : ?m.110216), ?m.110217 ⁻¹' {i})) < (#?m.110214)

α✝ : Type ?u.109224
r : α✝ → α✝ → Prop
β α : Type u
f : β → α
h₁ : ℵ₀ ≤ (#β)
h₂ : (#α) < cof (ord (#β))
h : ∀ (a : α), (#↑(f ⁻¹' {a})) < (#β)
⊢ Type ?u.110212

α✝ : Type ?u.109224
r : α✝ → α✝ → Prop
β α : Type u
f : β → α
h₁ : ℵ₀ ≤ (#β)
h₂ : (#α) < cof (ord (#β))
h : ∀ (a : α), (#↑(f ⁻¹' {a})) < (#β)
⊢ Type ?u.110211

α✝ : Type ?u.109224
r : α✝ → α✝ → Prop
β α : Type u
f : β → α
h₁ : ℵ₀ ≤ (#β)
h₂ : (#α) < cof (ord (#β))
h : ∀ (a : α), (#↑(f ⁻¹' {a})) < (#β)
⊢ ?m.110214 → ?m.110216
α✝ : Type ?u.109224
r : α✝ → α✝ → Prop
β α : Type u
f : β → α
h₁ : ℵ₀ ≤ (#β)
h₂ : (#α) < cof (ord (#β))
h : ∀ (a : α), (#↑(f ⁻¹' {a})) < (#β)
⊢ (#↑Set.univ) < (#?m.110149)

α✝ : Type ?u.109224
r : α✝ → α✝ → Prop
β α : Type u
f : β → α
h₁ : ℵ₀ ≤ (#β)
h₂ : (#α) < cof (ord (#β))
h : ∀ (a : α), (#↑(f ⁻¹' {a})) < (#β)
⊢ Type ?u.110148
rw [← preimage_univ, ← iUnion_of_singleton, preimage_iUnion]
no goals
α✝ : Type ?u.109224
r : α✝ → α✝ → Prop
β α : Type u
f : β → α
h₁ : ℵ₀ ≤ (#β)
h₂ : (#α) < cof (ord (#β))
h : ∀ (a : α), (#↑(f ⁻¹' {a})) < (#β)
⊢ (#↑(⋃ (i : ?m.110216), ?m.110217 ⁻¹' {i})) < (#?m.110214)

α✝ : Type ?u.109224
r : α✝ → α✝ → Prop
β α : Type u
f : β → α
h₁ : ℵ₀ ≤ (#β)
h₂ : (#α) < cof (ord (#β))
h : ∀ (a : α), (#↑(f ⁻¹' {a})) < (#β)
⊢ Type ?u.110212

α✝ : Type ?u.109224
r : α✝ → α✝ → Prop
β α : Type u
f : β → α
h₁ : ℵ₀ ≤ (#β)
h₂ : (#α) < cof (ord (#β))
h : ∀ (a : α), (#↑(f ⁻¹' {a})) < (#β)
⊢ Type ?u.110211

α✝ : Type ?u.109224
r : α✝ → α✝ → Prop
β α : Type u
f : β → α
h₁ : ℵ₀ ≤ (#β)
h₂ : (#α) < cof (ord (#β))
h : ∀ (a : α), (#↑(f ⁻¹' {a})) < (#β)
⊢ ?m.110214 → ?m.110216
exact
  mk_iUnion_le_sum_mk.trans_lt
    ((sum_le_iSup _).trans_lt <| mul_lt_of_lt h₁ (h₂.trans_le <| cof_ord_le _) (iSup_lt h₂ h))