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

State before:
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ : BishopFin β
inst✝ : Subsingleton α
⊢ card α ≤ 1
Tactic:
dsimp [card]
State after:
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ : BishopFin β
inst✝ : Subsingleton α
⊢ List.length (elems α) ≤ 1

State before:
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ : BishopFin β
inst✝ : Subsingleton α
⊢ List.length (elems α) ≤ 1
Tactic:
cases hl : elems α <;> dsimp
State after:
case nil
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ : BishopFin β
inst✝ : Subsingleton α
hl : elems α = []
⊢ 0 ≤ 1

case cons
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ : BishopFin β
inst✝ : Subsingleton α
head✝ : α
tail✝ : List α
hl : elems α = head✝ :: tail✝
⊢ Nat.succ (List.length tail✝) ≤ 1

State before:
case nil
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ : BishopFin β
inst✝ : Subsingleton α
hl : elems α = []
⊢ 0 ≤ 1

case cons
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ : BishopFin β
inst✝ : Subsingleton α
head✝ : α
tail✝ : List α
hl : elems α = head✝ :: tail✝
⊢ Nat.succ (List.length tail✝) ≤ 1
Tactic:
. decide
State after:
case cons
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ : BishopFin β
inst✝ : Subsingleton α
head✝ : α
tail✝ : List α
hl : elems α = head✝ :: tail✝
⊢ Nat.succ (List.length tail✝) ≤ 1

State before:
case cons
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ : BishopFin β
inst✝ : Subsingleton α
head✝ : α
tail✝ : List α
hl : elems α = head✝ :: tail✝
⊢ Nat.succ (List.length tail✝) ≤ 1
Tactic:
rename_i a l
State after:
case cons
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ : BishopFin β
inst✝ : Subsingleton α
a : α
l : List α
hl : elems α = a :: l
⊢ Nat.succ (List.length l) ≤ 1

State before:
case cons
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ : BishopFin β
inst✝ : Subsingleton α
a : α
l : List α
hl : elems α = a :: l
⊢ Nat.succ (List.length l) ≤ 1
Tactic:
cases l <;> dsimp
State after:
case cons.nil
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ : BishopFin β
inst✝ : Subsingleton α
a : α
hl : elems α = [a]
⊢ Nat.succ 0 ≤ 1

case cons.cons
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ : BishopFin β
inst✝ : Subsingleton α
a head✝ : α
tail✝ : List α
hl : elems α = a :: head✝ :: tail✝
⊢ Nat.succ (Nat.succ (List.length tail✝)) ≤ 1

State before:
case cons.nil
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ : BishopFin β
inst✝ : Subsingleton α
a : α
hl : elems α = [a]
⊢ Nat.succ 0 ≤ 1

case cons.cons
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ : BishopFin β
inst✝ : Subsingleton α
a head✝ : α
tail✝ : List α
hl : elems α = a :: head✝ :: tail✝
⊢ Nat.succ (Nat.succ (List.length tail✝)) ≤ 1
Tactic:
. decide
State after:
case cons.cons
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ : BishopFin β
inst✝ : Subsingleton α
a head✝ : α
tail✝ : List α
hl : elems α = a :: head✝ :: tail✝
⊢ Nat.succ (Nat.succ (List.length tail✝)) ≤ 1

State before:
case cons.cons
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ : BishopFin β
inst✝ : Subsingleton α
a head✝ : α
tail✝ : List α
hl : elems α = a :: head✝ :: tail✝
⊢ Nat.succ (Nat.succ (List.length tail✝)) ≤ 1
Tactic:
exfalso
State after:
case cons.cons.h
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ : BishopFin β
inst✝ : Subsingleton α
a head✝ : α
tail✝ : List α
hl : elems α = a :: head✝ :: tail✝
⊢ False

State before:
case cons.cons.h
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ : BishopFin β
inst✝ : Subsingleton α
a head✝ : α
tail✝ : List α
hl : elems α = a :: head✝ :: tail✝
⊢ False
Tactic:
rename_i b l
State after:
case cons.cons.h
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ : BishopFin β
inst✝ : Subsingleton α
a b : α
l : List α
hl : elems α = a :: b :: l
⊢ False

State before:
case cons.cons.h
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ : BishopFin β
inst✝ : Subsingleton α
a b : α
l : List α
hl : elems α = a :: b :: l
⊢ False
Tactic:
cases Subsingleton.allEq a b
State after:
case cons.cons.h.refl
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ : BishopFin β
inst✝ : Subsingleton α
a : α
l : List α
hl : elems α = a :: a :: l
⊢ False

State before:
case cons.cons.h.refl
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ : BishopFin β
inst✝ : Subsingleton α
a : α
l : List α
hl : elems α = a :: a :: l
⊢ False
Tactic:
have : List.Nodup (a :: a :: l) := hl ▸ nodup_elems
State after:
case cons.cons.h.refl
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ : BishopFin β
inst✝ : Subsingleton α
a : α
l : List α
hl : elems α = a :: a :: l
this : List.Nodup (a :: a :: l)
⊢ False

State before:
case cons.cons.h.refl
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ : BishopFin β
inst✝ : Subsingleton α
a : α
l : List α
hl : elems α = a :: a :: l
this : List.Nodup (a :: a :: l)
⊢ False
Tactic:
exact this.head (List.mem_cons_self a l)
State after:
no goals

State before:
case nil
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ : BishopFin β
inst✝ : Subsingleton α
hl : elems α = []
⊢ 0 ≤ 1
Tactic:
decide
State after:
no goals

State before:
case cons.nil
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ : BishopFin β
inst✝ : Subsingleton α
a : α
hl : elems α = [a]
⊢ Nat.succ 0 ≤ 1
Tactic:
decide
State after:
no goals