α : Type u_1
β : Type ?u.22499
γ : Type ?u.22502
inst✝¹ : Fintype α
inst✝ : Fintype β
n : ℕ := card α
hn : n = card α
ha : 1 = card α
_h : card α ≤ 1
a b x : α
hx : ∀ (y : α), y = x
⊢ a = b
α : Type u_1
β : Type ?u.22499
γ : Type ?u.22502
inst✝¹ : Fintype α
inst✝ : Fintype β
n : ℕ := card α
hn : n = card α
ha : 1 = card α
_h : card α ≤ 1
a b : α
⊢ a = b
let ⟨x, hx⟩ := card_eq_one_iff.1 ha.symm
no goals
α : Type u_1
β : Type ?u.22499
γ : Type ?u.22502
inst✝¹ : Fintype α
inst✝ : Fintype β
n : ℕ := card α
hn : n = card α
ha : 1 = card α
_h : card α ≤ 1
a b x : α
hx : ∀ (y : α), y = x
⊢ a = b
rw [hx a, hx b]
α : Type u_1
β : Type ?u.22499
γ : Type ?u.22502
inst✝¹ : Fintype α
inst✝ : Fintype β
n✝ : ℕ := card α
hn : n✝ = card α
n : ℕ
ha : n + 2 = card α
h : n + 2 ≤ 1
⊢ False
α : Type u_1
β : Type ?u.22499
γ : Type ?u.22502
inst✝¹ : Fintype α
inst✝ : Fintype β
n✝ : ℕ := card α
hn : n✝ = card α
n : ℕ
ha : n + 2 = card α
h : card α ≤ 1
⊢ False
rw [← ha] at h
no goals
α : Type u_1
β : Type ?u.22499
γ : Type ?u.22502
inst✝¹ : Fintype α
inst✝ : Fintype β
n✝ : ℕ := card α
hn : n✝ = card α
n : ℕ
ha : n + 2 = card α
h : n + 2 ≤ 1
⊢ False
cases h with | step h => cases h; done
no goals
case step
α : Type u_1
β : Type ?u.22499
γ : Type ?u.22502
inst✝¹ : Fintype α
inst✝ : Fintype β
n✝ : ℕ := card α
hn : n✝ = card α
n : ℕ
ha : n + 2 = card α
h : Nat.le (n + 2) 0
⊢ False
cases h