-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem add_one_le_succ (c : Cardinal.{u}) : c + 1 ≤ succ c

Proof state:
case mk.mk.intro.intro
c b✝ : Cardinal.{u}
β γ : Type u
this : {c' | Quot.mk (⇑isEquivalent) γ < c'}.Nonempty
hlt : Quot.mk (⇑isEquivalent) γ < Quot.mk (⇑isEquivalent) β
f : γ ↪ β
b : β
hb : ¬∃ a, f a = b
⊢ Quot.mk (⇑isEquivalent) γ + 1 ≤ Quot.mk (⇑isEquivalent) β

Tactic:
calc
  #γ + 1 = #(Option γ) := mk_option.symm
  _ ≤ #β := (f.optionElim b hb).cardinal_le

Result:
no goals

Proof state:
c : Cardinal.{u}
this : {c' | c < c'}.Nonempty
⊢ c + 1 ≤ succ c

Tactic:
simp_rw [succ_def, le_csInf_iff'' this, mem_setOf]

Result:
c : Cardinal.{u}
this : {c' | c < c'}.Nonempty
⊢ ∀ (b : Cardinal.{u}), c < b → c + 1 ≤ b

Proof state:
case mk.mk.intro
c b : Cardinal.{u}
β γ : Type u
this : {c' | Quot.mk (⇑isEquivalent) γ < c'}.Nonempty
hlt : Quot.mk (⇑isEquivalent) γ < Quot.mk (⇑isEquivalent) β
f : γ ↪ β
⊢ Quot.mk (⇑isEquivalent) γ + 1 ≤ Quot.mk (⇑isEquivalent) β

Tactic:
have : ¬Surjective f := fun hn => (not_le_of_lt hlt) (mk_le_of_surjective hn)

Result:
case mk.mk.intro
c b : Cardinal.{u}
β γ : Type u
this✝ : {c' | Quot.mk (⇑isEquivalent) γ < c'}.Nonempty
hlt : Quot.mk (⇑isEquivalent) γ < Quot.mk (⇑isEquivalent) β
f : γ ↪ β
this : ¬Surjective ⇑f
⊢ Quot.mk (⇑isEquivalent) γ + 1 ≤ Quot.mk (⇑isEquivalent) β

Proof state:
c : Cardinal.{u}
this : {c' | c < c'}.Nonempty
⊢ ∀ (b : Cardinal.{u}), c < b → c + 1 ≤ b

Tactic:
intro b hlt

Result:
c : Cardinal.{u}
this : {c' | c < c'}.Nonempty
b : Cardinal.{u}
hlt : c < b
⊢ c + 1 ≤ b

Proof state:
c : Cardinal.{u}
⊢ c + 1 ≤ succ c

Tactic:
have : Set.Nonempty { c' | c < c' } := exists_gt c

Result:
c : Cardinal.{u}
this : {c' | c < c'}.Nonempty
⊢ c + 1 ≤ succ c

Proof state:
case mk.mk.intro
c b : Cardinal.{u}
β γ : Type u
this✝ : {c' | Quot.mk (⇑isEquivalent) γ < c'}.Nonempty
hlt : Quot.mk (⇑isEquivalent) γ < Quot.mk (⇑isEquivalent) β
f : γ ↪ β
this : ¬Surjective ⇑f
⊢ Quot.mk (⇑isEquivalent) γ + 1 ≤ Quot.mk (⇑isEquivalent) β

Tactic:
simp only [Surjective, not_forall] at this

Result:
case mk.mk.intro
c b : Cardinal.{u}
β γ : Type u
this✝ : {c' | Quot.mk (⇑isEquivalent) γ < c'}.Nonempty
hlt : Quot.mk (⇑isEquivalent) γ < Quot.mk (⇑isEquivalent) β
f : γ ↪ β
this : ∃ x, ¬∃ a, f a = x
⊢ Quot.mk (⇑isEquivalent) γ + 1 ≤ Quot.mk (⇑isEquivalent) β

Proof state:
case mk.mk
c b : Cardinal.{u}
β γ : Type u
this : {c' | Quot.mk (⇑isEquivalent) γ < c'}.Nonempty
hlt : Quot.mk (⇑isEquivalent) γ < Quot.mk (⇑isEquivalent) β
⊢ Quot.mk (⇑isEquivalent) γ + 1 ≤ Quot.mk (⇑isEquivalent) β

Tactic:
obtain ⟨f⟩ := le_of_lt hlt

Result:
case mk.mk.intro
c b : Cardinal.{u}
β γ : Type u
this : {c' | Quot.mk (⇑isEquivalent) γ < c'}.Nonempty
hlt : Quot.mk (⇑isEquivalent) γ < Quot.mk (⇑isEquivalent) β
f : γ ↪ β
⊢ Quot.mk (⇑isEquivalent) γ + 1 ≤ Quot.mk (⇑isEquivalent) β

Proof state:
c : Cardinal.{u}
this : {c' | c < c'}.Nonempty
b : Cardinal.{u}
hlt : c < b
⊢ c + 1 ≤ b

Tactic:
rcases b, c with ⟨⟨β⟩, ⟨γ⟩⟩

Result:
case mk.mk
c b : Cardinal.{u}
β γ : Type u
this : {c' | Quot.mk (⇑isEquivalent) γ < c'}.Nonempty
hlt : Quot.mk (⇑isEquivalent) γ < Quot.mk (⇑isEquivalent) β
⊢ Quot.mk (⇑isEquivalent) γ + 1 ≤ Quot.mk (⇑isEquivalent) β

Proof state:
case mk.mk.intro
c b : Cardinal.{u}
β γ : Type u
this✝ : {c' | Quot.mk (⇑isEquivalent) γ < c'}.Nonempty
hlt : Quot.mk (⇑isEquivalent) γ < Quot.mk (⇑isEquivalent) β
f : γ ↪ β
this : ∃ x, ¬∃ a, f a = x
⊢ Quot.mk (⇑isEquivalent) γ + 1 ≤ Quot.mk (⇑isEquivalent) β

Tactic:
rcases this with ⟨b, hb⟩

Result:
case mk.mk.intro.intro
c b✝ : Cardinal.{u}
β γ : Type u
this : {c' | Quot.mk (⇑isEquivalent) γ < c'}.Nonempty
hlt : Quot.mk (⇑isEquivalent) γ < Quot.mk (⇑isEquivalent) β
f : γ ↪ β
b : β
hb : ¬∃ a, f a = b
⊢ Quot.mk (⇑isEquivalent) γ + 1 ≤ Quot.mk (⇑isEquivalent) β