case intro
α✝ : Type ?u.86132
β : Type ?u.86135
γ : Type ?u.86138
P : (α : Type u_1) → [inst : Fintype α] → Prop
α : Type u_1
inst✝ : Fintype α
hbase : ∀ (α : Type u_1) [inst : Fintype α] [inst_1 : Subsingleton α], P α
hstep :
  ∀ (α : Type u_1) [inst : Fintype α] [inst_1 : Nontrivial α],
    (∀ (β : Type u_1) [inst_2 : Fintype β], card β < card α → P β) → P α
n : ℕ
hn : card α = n
⊢ P α
α✝ : Type ?u.86132
β : Type ?u.86135
γ : Type ?u.86138
P : (α : Type u_1) → [inst : Fintype α] → Prop
α : Type u_1
inst✝ : Fintype α
hbase : ∀ (α : Type u_1) [inst : Fintype α] [inst_1 : Subsingleton α], P α
hstep :
  ∀ (α : Type u_1) [inst : Fintype α] [inst_1 : Nontrivial α],
    (∀ (β : Type u_1) [inst_2 : Fintype β], card β < card α → P β) → P α
⊢ P α
obtain ⟨n, hn⟩ : ∃ n, Fintype.card α = n := ⟨Fintype.card α, rfl⟩
case intro.h
α✝¹ : Type ?u.86132
β : Type ?u.86135
γ : Type ?u.86138
P : (α : Type u_1) → [inst : Fintype α] → Prop
α✝ : Type u_1
inst✝¹ : Fintype α✝
hbase : ∀ (α : Type u_1) [inst : Fintype α] [inst_1 : Subsingleton α], P α
hstep :
  ∀ (α : Type u_1) [inst : Fintype α] [inst_1 : Nontrivial α],
    (∀ (β : Type u_1) [inst_2 : Fintype β], card β < card α → P β) → P α
n✝ : ℕ
hn✝ : card α✝ = n✝
n : ℕ
ih : ∀ (m : ℕ), m < n → ∀ (α : Type u_1) [inst : Fintype α], card α = m → P α
α : Type u_1
inst✝ : Fintype α
hn : card α = n
⊢ P α
case intro
α✝ : Type ?u.86132
β : Type ?u.86135
γ : Type ?u.86138
P : (α : Type u_1) → [inst : Fintype α] → Prop
α : Type u_1
inst✝ : Fintype α
hbase : ∀ (α : Type u_1) [inst : Fintype α] [inst_1 : Subsingleton α], P α
hstep :
  ∀ (α : Type u_1) [inst : Fintype α] [inst_1 : Nontrivial α],
    (∀ (β : Type u_1) [inst_2 : Fintype β], card β < card α → P β) → P α
n : ℕ
hn : card α = n
⊢ P α
induction' n using Nat.strong_induction_on with n ih generalizing α
case intro.h.inl
α✝¹ : Type ?u.86132
β : Type ?u.86135
γ : Type ?u.86138
P : (α : Type u_1) → [inst : Fintype α] → Prop
α✝ : Type u_1
inst✝¹ : Fintype α✝
hbase : ∀ (α : Type u_1) [inst : Fintype α] [inst_1 : Subsingleton α], P α
hstep :
  ∀ (α : Type u_1) [inst : Fintype α] [inst_1 : Nontrivial α],
    (∀ (β : Type u_1) [inst_2 : Fintype β], card β < card α → P β) → P α
n✝ : ℕ
hn✝ : card α✝ = n✝
n : ℕ
ih : ∀ (m : ℕ), m < n → ∀ (α : Type u_1) [inst : Fintype α], card α = m → P α
α : Type u_1
inst✝ : Fintype α
hn : card α = n
hsing : Subsingleton α
⊢ P α

case intro.h.inr
α✝¹ : Type ?u.86132
β : Type ?u.86135
γ : Type ?u.86138
P : (α : Type u_1) → [inst : Fintype α] → Prop
α✝ : Type u_1
inst✝¹ : Fintype α✝
hbase : ∀ (α : Type u_1) [inst : Fintype α] [inst_1 : Subsingleton α], P α
hstep :
  ∀ (α : Type u_1) [inst : Fintype α] [inst_1 : Nontrivial α],
    (∀ (β : Type u_1) [inst_2 : Fintype β], card β < card α → P β) → P α
n✝ : ℕ
hn✝ : card α✝ = n✝
n : ℕ
ih : ∀ (m : ℕ), m < n → ∀ (α : Type u_1) [inst : Fintype α], card α = m → P α
α : Type u_1
inst✝ : Fintype α
hn : card α = n
hnontriv : Nontrivial α
⊢ P α
case intro.h
α✝¹ : Type ?u.86132
β : Type ?u.86135
γ : Type ?u.86138
P : (α : Type u_1) → [inst : Fintype α] → Prop
α✝ : Type u_1
inst✝¹ : Fintype α✝
hbase : ∀ (α : Type u_1) [inst : Fintype α] [inst_1 : Subsingleton α], P α
hstep :
  ∀ (α : Type u_1) [inst : Fintype α] [inst_1 : Nontrivial α],
    (∀ (β : Type u_1) [inst_2 : Fintype β], card β < card α → P β) → P α
n✝ : ℕ
hn✝ : card α✝ = n✝
n : ℕ
ih : ∀ (m : ℕ), m < n → ∀ (α : Type u_1) [inst : Fintype α], card α = m → P α
α : Type u_1
inst✝ : Fintype α
hn : card α = n
⊢ P α
cases' subsingleton_or_nontrivial α with hsing hnontriv
no goals
case intro.h.inl
α✝¹ : Type ?u.86132
β : Type ?u.86135
γ : Type ?u.86138
P : (α : Type u_1) → [inst : Fintype α] → Prop
α✝ : Type u_1
inst✝¹ : Fintype α✝
hbase : ∀ (α : Type u_1) [inst : Fintype α] [inst_1 : Subsingleton α], P α
hstep :
  ∀ (α : Type u_1) [inst : Fintype α] [inst_1 : Nontrivial α],
    (∀ (β : Type u_1) [inst_2 : Fintype β], card β < card α → P β) → P α
n✝ : ℕ
hn✝ : card α✝ = n✝
n : ℕ
ih : ∀ (m : ℕ), m < n → ∀ (α : Type u_1) [inst : Fintype α], card α = m → P α
α : Type u_1
inst✝ : Fintype α
hn : card α = n
hsing : Subsingleton α
⊢ P α
apply hbase
case intro.h.inr._ih
α✝¹ : Type ?u.86132
β : Type ?u.86135
γ : Type ?u.86138
P : (α : Type u_1) → [inst : Fintype α] → Prop
α✝ : Type u_1
inst✝¹ : Fintype α✝
hbase : ∀ (α : Type u_1) [inst : Fintype α] [inst_1 : Subsingleton α], P α
hstep :
  ∀ (α : Type u_1) [inst : Fintype α] [inst_1 : Nontrivial α],
    (∀ (β : Type u_1) [inst_2 : Fintype β], card β < card α → P β) → P α
n✝ : ℕ
hn✝ : card α✝ = n✝
n : ℕ
ih : ∀ (m : ℕ), m < n → ∀ (α : Type u_1) [inst : Fintype α], card α = m → P α
α : Type u_1
inst✝ : Fintype α
hn : card α = n
hnontriv : Nontrivial α
⊢ ∀ (β : Type u_1) [inst : Fintype β], card β < card α → P β
case intro.h.inr
α✝¹ : Type ?u.86132
β : Type ?u.86135
γ : Type ?u.86138
P : (α : Type u_1) → [inst : Fintype α] → Prop
α✝ : Type u_1
inst✝¹ : Fintype α✝
hbase : ∀ (α : Type u_1) [inst : Fintype α] [inst_1 : Subsingleton α], P α
hstep :
  ∀ (α : Type u_1) [inst : Fintype α] [inst_1 : Nontrivial α],
    (∀ (β : Type u_1) [inst_2 : Fintype β], card β < card α → P β) → P α
n✝ : ℕ
hn✝ : card α✝ = n✝
n : ℕ
ih : ∀ (m : ℕ), m < n → ∀ (α : Type u_1) [inst : Fintype α], card α = m → P α
α : Type u_1
inst✝ : Fintype α
hn : card α = n
hnontriv : Nontrivial α
⊢ P α
apply hstep
case intro.h.inr._ih
α✝¹ : Type ?u.86132
β✝ : Type ?u.86135
γ : Type ?u.86138
P : (α : Type u_1) → [inst : Fintype α] → Prop
α✝ : Type u_1
inst✝² : Fintype α✝
hbase : ∀ (α : Type u_1) [inst : Fintype α] [inst_1 : Subsingleton α], P α
hstep :
  ∀ (α : Type u_1) [inst : Fintype α] [inst_1 : Nontrivial α],
    (∀ (β : Type u_1) [inst_2 : Fintype β], card β < card α → P β) → P α
n✝ : ℕ
hn✝ : card α✝ = n✝
n : ℕ
ih : ∀ (m : ℕ), m < n → ∀ (α : Type u_1) [inst : Fintype α], card α = m → P α
α : Type u_1
inst✝¹ : Fintype α
hn : card α = n
hnontriv : Nontrivial α
β : Type u_1
inst✝ : Fintype β
hlt : card β < card α
⊢ P β
case intro.h.inr._ih
α✝¹ : Type ?u.86132
β : Type ?u.86135
γ : Type ?u.86138
P : (α : Type u_1) → [inst : Fintype α] → Prop
α✝ : Type u_1
inst✝¹ : Fintype α✝
hbase : ∀ (α : Type u_1) [inst : Fintype α] [inst_1 : Subsingleton α], P α
hstep :
  ∀ (α : Type u_1) [inst : Fintype α] [inst_1 : Nontrivial α],
    (∀ (β : Type u_1) [inst_2 : Fintype β], card β < card α → P β) → P α
n✝ : ℕ
hn✝ : card α✝ = n✝
n : ℕ
ih : ∀ (m : ℕ), m < n → ∀ (α : Type u_1) [inst : Fintype α], card α = m → P α
α : Type u_1
inst✝ : Fintype α
hn : card α = n
hnontriv : Nontrivial α
⊢ ∀ (β : Type u_1) [inst : Fintype β], card β < card α → P β
intro β _ hlt
case intro.h.inr._ih
α✝¹ : Type ?u.86132
β✝ : Type ?u.86135
γ : Type ?u.86138
P : (α : Type u_1) → [inst : Fintype α] → Prop
α✝ : Type u_1
inst✝² : Fintype α✝
hbase : ∀ (α : Type u_1) [inst : Fintype α] [inst_1 : Subsingleton α], P α
hstep :
  ∀ (α : Type u_1) [inst : Fintype α] [inst_1 : Nontrivial α],
    (∀ (β : Type u_1) [inst_2 : Fintype β], card β < card α → P β) → P α
n✝ : ℕ
hn✝ : card α✝ = n✝
n : ℕ
ih : ∀ (m : ℕ), m < n → ∀ (α : Type u_1) [inst : Fintype α], card α = m → P α
α : Type u_1
inst✝¹ : Fintype α
hn : card α = n
hnontriv : Nontrivial α
β : Type u_1
inst✝ : Fintype β
hlt : card β < n
⊢ P β
case intro.h.inr._ih
α✝¹ : Type ?u.86132
β✝ : Type ?u.86135
γ : Type ?u.86138
P : (α : Type u_1) → [inst : Fintype α] → Prop
α✝ : Type u_1
inst✝² : Fintype α✝
hbase : ∀ (α : Type u_1) [inst : Fintype α] [inst_1 : Subsingleton α], P α
hstep :
  ∀ (α : Type u_1) [inst : Fintype α] [inst_1 : Nontrivial α],
    (∀ (β : Type u_1) [inst_2 : Fintype β], card β < card α → P β) → P α
n✝ : ℕ
hn✝ : card α✝ = n✝
n : ℕ
ih : ∀ (m : ℕ), m < n → ∀ (α : Type u_1) [inst : Fintype α], card α = m → P α
α : Type u_1
inst✝¹ : Fintype α
hn : card α = n
hnontriv : Nontrivial α
β : Type u_1
inst✝ : Fintype β
hlt : card β < card α
⊢ P β
rw [hn] at hlt
no goals
case intro.h.inr._ih
α✝¹ : Type ?u.86132
β✝ : Type ?u.86135
γ : Type ?u.86138
P : (α : Type u_1) → [inst : Fintype α] → Prop
α✝ : Type u_1
inst✝² : Fintype α✝
hbase : ∀ (α : Type u_1) [inst : Fintype α] [inst_1 : Subsingleton α], P α
hstep :
  ∀ (α : Type u_1) [inst : Fintype α] [inst_1 : Nontrivial α],
    (∀ (β : Type u_1) [inst_2 : Fintype β], card β < card α → P β) → P α
n✝ : ℕ
hn✝ : card α✝ = n✝
n : ℕ
ih : ∀ (m : ℕ), m < n → ∀ (α : Type u_1) [inst : Fintype α], card α = m → P α
α : Type u_1
inst✝¹ : Fintype α
hn : card α = n
hnontriv : Nontrivial α
β : Type u_1
inst✝ : Fintype β
hlt : card β < n
⊢ P β
exact ih (Fintype.card β) hlt _ rfl