Theorem: PartENat.card_option (Matroid/ForMathlib/Card.lean)

State before:
α✝ : Type u_1
β : Type u_2
s t : Set α✝
n : ℕ
α : Type u_3
⊢ card (Option α) = card α + 1
Tactic:
obtain (hα | hα) := finite_or_infinite α
State after:
case inl
α✝ : Type u_1
β : Type u_2
s t : Set α✝
n : ℕ
α : Type u_3
hα : Finite α
⊢ card (Option α) = card α + 1

case inr
α✝ : Type u_1
β : Type u_2
s t : Set α✝
n : ℕ
α : Type u_3
hα : Infinite α
⊢ card (Option α) = card α + 1

State before:
case inr
α✝ : Type u_1
β : Type u_2
s t : Set α✝
n : ℕ
α : Type u_3
hα : Infinite α
⊢ card (Option α) = card α + 1
Tactic:
simp
State after:
no goals

State before:
case inl
α✝ : Type u_1
β : Type u_2
s t : Set α✝
n : ℕ
α : Type u_3
hα : Finite α
⊢ card (Option α) = card α + 1
Tactic:
have _ := Fintype.ofFinite α
State after:
case inl
α✝ : Type u_1
β : Type u_2
s t : Set α✝
n : ℕ
α : Type u_3
hα : Finite α
x✝ : Fintype α
⊢ card (Option α) = card α + 1

State before:
case inl
α✝ : Type u_1
β : Type u_2
s t : Set α✝
n : ℕ
α : Type u_3
hα : Finite α
x✝ : Fintype α
⊢ card (Option α) = card α + 1
Tactic:
simp
State after:
no goals