case refine_1
α✝ β α : Type u
h : Fintype α
⊢ ∀ (α β : Type u) [inst : Fintype β] (e : α ≃ β), (#α) = ↑(Fintype.card α) → (#β) = ↑(Fintype.card β)

case refine_2
α✝ β α : Type u
h : Fintype α
⊢ (#PEmpty) = ↑(Fintype.card PEmpty)

case refine_3
α✝ β α : Type u
h : Fintype α
⊢ ∀ (α : Type u) [inst : Fintype α], (#α) = ↑(Fintype.card α) → (#Option α) = ↑(Fintype.card (Option α))
α✝ β α : Type u
h : Fintype α
⊢ (#α) = ↑(Fintype.card α)
refine Fintype.induction_empty_option ?_ ?_ ?_ α (h_fintype := h)
case refine_1
α✝¹ β✝ α✝ : Type u
h✝ : Fintype α✝
α β : Type u
h : Fintype β
e : α ≃ β
hα : (#α) = ↑(Fintype.card α)
⊢ (#β) = ↑(Fintype.card β)
case refine_1
α✝ β α : Type u
h : Fintype α
⊢ ∀ (α β : Type u) [inst : Fintype β] (e : α ≃ β), (#α) = ↑(Fintype.card α) → (#β) = ↑(Fintype.card β)
intro α β h e hα
case refine_1
α✝¹ β✝ α✝ : Type u
h✝ : Fintype α✝
α β : Type u
h : Fintype β
e : α ≃ β
hα : (#α) = ↑(Fintype.card α)
this : Fintype α := Fintype.ofEquiv β e.symm
⊢ (#β) = ↑(Fintype.card β)
case refine_1
α✝¹ β✝ α✝ : Type u
h✝ : Fintype α✝
α β : Type u
h : Fintype β
e : α ≃ β
hα : (#α) = ↑(Fintype.card α)
⊢ (#β) = ↑(Fintype.card β)
letI := Fintype.ofEquiv β e.symm
no goals
case refine_1
α✝¹ β✝ α✝ : Type u
h✝ : Fintype α✝
α β : Type u
h : Fintype β
e : α ≃ β
hα : (#α) = ↑(Fintype.card α)
this : Fintype α := Fintype.ofEquiv β e.symm
⊢ (#β) = ↑(Fintype.card β)
rwa [mk_congr e, Fintype.card_congr e] at hα
no goals
case refine_2
α✝ β α : Type u
h : Fintype α
⊢ (#PEmpty) = ↑(Fintype.card PEmpty)
rfl
case refine_3
α✝¹ β α✝ : Type u
h✝ : Fintype α✝
α : Type u
h : Fintype α
hα : (#α) = ↑(Fintype.card α)
⊢ (#Option α) = ↑(Fintype.card (Option α))
case refine_3
α✝ β α : Type u
h : Fintype α
⊢ ∀ (α : Type u) [inst : Fintype α], (#α) = ↑(Fintype.card α) → (#Option α) = ↑(Fintype.card (Option α))
intro α h hα
case refine_3
α✝¹ β α✝ : Type u
h✝ : Fintype α✝
α : Type u
h : Fintype α
hα : (#α) = ↑(Fintype.card α)
⊢ ↑(Fintype.card α) + 1 = ↑(Fintype.card α + 1)
case refine_3
α✝¹ β α✝ : Type u
h✝ : Fintype α✝
α : Type u
h : Fintype α
hα : (#α) = ↑(Fintype.card α)
⊢ (#Option α) = ↑(Fintype.card (Option α))
simp [hα]
no goals
case refine_3
α✝¹ β α✝ : Type u
h✝ : Fintype α✝
α : Type u
h : Fintype α
hα : (#α) = ↑(Fintype.card α)
⊢ ↑(Fintype.card α) + 1 = ↑(Fintype.card α + 1)
rfl