Theorem: BishopFin.card_nonempty (Fifteen/Logic/BishopFin.lean)

State before:
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ : BishopFin β
inst✝ : Nonempty α
⊢ card α ≥ 1
Tactic:
cases Nat.eq_zero_or_pos (card α) with
| inl h0 =>
  dsimp [card] at h0
  rcases ‹Nonempty α› with ⟨a⟩
  have := List.eq_nil_of_length_eq_zero h0
  have : a ∈ [] := this ▸ mem_elems a
  cases this
| inr h => exact h
State after:
no goals

State before:
case inl
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ : BishopFin β
inst✝ : Nonempty α
h0 : card α = 0
⊢ card α ≥ 1
Tactic:
dsimp [card] at h0
State after:
case inl
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ : BishopFin β
inst✝ : Nonempty α
h0 : List.length (elems α) = 0
⊢ card α ≥ 1

State before:
case inl
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ : BishopFin β
inst✝ : Nonempty α
h0 : List.length (elems α) = 0
⊢ card α ≥ 1
Tactic:
rcases ‹Nonempty α› with ⟨a⟩
State after:
case inl.intro
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ : BishopFin β
inst✝ : Nonempty α
h0 : List.length (elems α) = 0
a : α
⊢ card α ≥ 1

State before:
case inl.intro
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ : BishopFin β
inst✝ : Nonempty α
h0 : List.length (elems α) = 0
a : α
⊢ card α ≥ 1
Tactic:
have := List.eq_nil_of_length_eq_zero h0
State after:
case inl.intro
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ : BishopFin β
inst✝ : Nonempty α
h0 : List.length (elems α) = 0
a : α
this : elems α = []
⊢ card α ≥ 1

State before:
case inl.intro
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ : BishopFin β
inst✝ : Nonempty α
h0 : List.length (elems α) = 0
a : α
this : elems α = []
⊢ card α ≥ 1
Tactic:
have : a ∈ [] := this ▸ mem_elems a
State after:
case inl.intro
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ : BishopFin β
inst✝ : Nonempty α
h0 : List.length (elems α) = 0
a : α
this✝ : elems α = []
this : a ∈ []
⊢ card α ≥ 1

State before:
case inl.intro
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ : BishopFin β
inst✝ : Nonempty α
h0 : List.length (elems α) = 0
a : α
this✝ : elems α = []
this : a ∈ []
⊢ card α ≥ 1
Tactic:
cases this
State after:
no goals

State before:
case inr
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ : BishopFin β
inst✝ : Nonempty α
h : card α > 0
⊢ card α ≥ 1
Tactic:
exact h
State after:
no goals