α β : Type u
c : Cardinal
this : Set.Nonempty {c' | c < c'}
⊢ c + 1 ≤ succ c
α β : Type u
c : Cardinal
⊢ c + 1 ≤ succ c
have : Set.Nonempty { c' | c < c' } := exists_gt c
α β : Type u
c : Cardinal
this : Set.Nonempty {c' | c < c'}
⊢ ∀ (b : Cardinal), c < b → c + 1 ≤ b
α β : Type u
c : Cardinal
this : Set.Nonempty {c' | c < c'}
⊢ c + 1 ≤ succ c
simp_rw [succ_def, le_csInf_iff'' this, mem_setOf]
α β : Type u
c : Cardinal
this : Set.Nonempty {c' | c < c'}
b : Cardinal
hlt : c < b
⊢ c + 1 ≤ b
α β : Type u
c : Cardinal
this : Set.Nonempty {c' | c < c'}
⊢ ∀ (b : Cardinal), c < b → c + 1 ≤ b
intro b hlt
case mk.mk
α β✝ : Type u
c b : Cardinal
β γ : Type u
this : Set.Nonempty {c' | Quot.mk Setoid.r γ < c'}
hlt : Quot.mk Setoid.r γ < Quot.mk Setoid.r β
⊢ Quot.mk Setoid.r γ + 1 ≤ Quot.mk Setoid.r β
α β : Type u
c : Cardinal
this : Set.Nonempty {c' | c < c'}
b : Cardinal
hlt : c < b
⊢ c + 1 ≤ b
rcases b, c with ⟨⟨β⟩, ⟨γ⟩⟩
case mk.mk.intro
α β✝ : Type u
c b : Cardinal
β γ : Type u
this : Set.Nonempty {c' | Quot.mk Setoid.r γ < c'}
hlt : Quot.mk Setoid.r γ < Quot.mk Setoid.r β
f : γ ↪ β
⊢ Quot.mk Setoid.r γ + 1 ≤ Quot.mk Setoid.r β
case mk.mk
α β✝ : Type u
c b : Cardinal
β γ : Type u
this : Set.Nonempty {c' | Quot.mk Setoid.r γ < c'}
hlt : Quot.mk Setoid.r γ < Quot.mk Setoid.r β
⊢ Quot.mk Setoid.r γ + 1 ≤ Quot.mk Setoid.r β
cases' le_of_lt hlt with f
case mk.mk.intro
α β✝ : Type u
c b : Cardinal
β γ : Type u
this✝ : Set.Nonempty {c' | Quot.mk Setoid.r γ < c'}
hlt : Quot.mk Setoid.r γ < Quot.mk Setoid.r β
f : γ ↪ β
this : ¬Surjective ↑f
⊢ Quot.mk Setoid.r γ + 1 ≤ Quot.mk Setoid.r β
case mk.mk.intro
α β✝ : Type u
c b : Cardinal
β γ : Type u
this : Set.Nonempty {c' | Quot.mk Setoid.r γ < c'}
hlt : Quot.mk Setoid.r γ < Quot.mk Setoid.r β
f : γ ↪ β
⊢ Quot.mk Setoid.r γ + 1 ≤ Quot.mk Setoid.r β
have : ¬Surjective f := fun hn => (not_le_of_lt hlt) (mk_le_of_surjective hn)
case mk.mk.intro
α β✝ : Type u
c b : Cardinal
β γ : Type u
this✝ : Set.Nonempty {c' | Quot.mk Setoid.r γ < c'}
hlt : Quot.mk Setoid.r γ < Quot.mk Setoid.r β
f : γ ↪ β
this : ∃ x, ¬∃ a, ↑f a = x
⊢ Quot.mk Setoid.r γ + 1 ≤ Quot.mk Setoid.r β
case mk.mk.intro
α β✝ : Type u
c b : Cardinal
β γ : Type u
this✝ : Set.Nonempty {c' | Quot.mk Setoid.r γ < c'}
hlt : Quot.mk Setoid.r γ < Quot.mk Setoid.r β
f : γ ↪ β
this : ¬Surjective ↑f
⊢ Quot.mk Setoid.r γ + 1 ≤ Quot.mk Setoid.r β
simp only [Surjective, not_forall] at this
case mk.mk.intro.intro
α β✝ : Type u
c b✝ : Cardinal
β γ : Type u
this : Set.Nonempty {c' | Quot.mk Setoid.r γ < c'}
hlt : Quot.mk Setoid.r γ < Quot.mk Setoid.r β
f : γ ↪ β
b : β
hb : ¬∃ a, ↑f a = b
⊢ Quot.mk Setoid.r γ + 1 ≤ Quot.mk Setoid.r β
case mk.mk.intro
α β✝ : Type u
c b : Cardinal
β γ : Type u
this✝ : Set.Nonempty {c' | Quot.mk Setoid.r γ < c'}
hlt : Quot.mk Setoid.r γ < Quot.mk Setoid.r β
f : γ ↪ β
this : ∃ x, ¬∃ a, ↑f a = x
⊢ Quot.mk Setoid.r γ + 1 ≤ Quot.mk Setoid.r β
rcases this with ⟨b, hb⟩
no goals
case mk.mk.intro.intro
α β✝ : Type u
c b✝ : Cardinal
β γ : Type u
this : Set.Nonempty {c' | Quot.mk Setoid.r γ < c'}
hlt : Quot.mk Setoid.r γ < Quot.mk Setoid.r β
f : γ ↪ β
b : β
hb : ¬∃ a, ↑f a = b
⊢ Quot.mk Setoid.r γ + 1 ≤ Quot.mk Setoid.r β
calc
  (#γ) + 1 = (#Option γ) := mk_option.symm
  _ ≤ (#β) := (f.optionElim b hb).cardinal_le