α✝ : Type ?u.3562
β✝ : Type ?u.3565
inst✝² : Denumerable α✝
inst✝¹ : Denumerable β✝
α : Type u_1
β : Type u_2
inst✝ : Denumerable α
e : β ≃ α
n : ℕ
this : Denumerable β := ofEquiv α e
⊢ ofNat β n = ↑e.symm (ofNat α n)
α✝ : Type ?u.3562
β✝ : Type ?u.3565
inst✝² : Denumerable α✝
inst✝¹ : Denumerable β✝
α : Type u_1
β : Type u_2
inst✝ : Denumerable α
e : β ≃ α
n : ℕ
⊢ ofNat β n = ↑e.symm (ofNat α n)
letI := ofEquiv _ e
α✝ : Type ?u.3562
β✝ : Type ?u.3565
inst✝² : Denumerable α✝
inst✝¹ : Denumerable β✝
α : Type u_1
β : Type u_2
inst✝ : Denumerable α
e : β ≃ α
n : ℕ
this : Denumerable β := ofEquiv α e
⊢ decode n = some (↑e.symm (ofNat α n))
α✝ : Type ?u.3562
β✝ : Type ?u.3565
inst✝² : Denumerable α✝
inst✝¹ : Denumerable β✝
α : Type u_1
β : Type u_2
inst✝ : Denumerable α
e : β ≃ α
n : ℕ
this : Denumerable β := ofEquiv α e
⊢ ofNat β n = ↑e.symm (ofNat α n)
refine ofNat_of_decode ?_
α✝ : Type ?u.3562
β✝ : Type ?u.3565
inst✝² : Denumerable α✝
inst✝¹ : Denumerable β✝
α : Type u_1
β : Type u_2
inst✝ : Denumerable α
e : β ≃ α
n : ℕ
this : Denumerable β := ofEquiv α e
⊢ Option.map (↑e.symm) (decode n) = some (↑e.symm (ofNat α n))
α✝ : Type ?u.3562
β✝ : Type ?u.3565
inst✝² : Denumerable α✝
inst✝¹ : Denumerable β✝
α : Type u_1
β : Type u_2
inst✝ : Denumerable α
e : β ≃ α
n : ℕ
this : Denumerable β := ofEquiv α e
⊢ decode n = some (↑e.symm (ofNat α n))
rw [decode_ofEquiv e]
no goals
α✝ : Type ?u.3562
β✝ : Type ?u.3565
inst✝² : Denumerable α✝
inst✝¹ : Denumerable β✝
α : Type u_1
β : Type u_2
inst✝ : Denumerable α
e : β ≃ α
n : ℕ
this : Denumerable β := ofEquiv α e
⊢ Option.map (↑e.symm) (decode n) = some (↑e.symm (ofNat α n))
simp