[GOAL]
K : Type u_1
inst✝¹ : Field K
t : ℕ
inst✝ : Invertible ↑t
⊢ ¬ringChar K ∣ t
[PROOFSTEP]
rw [← ringChar.spec, ← Ne.def]
[GOAL]
K : Type u_1
inst✝¹ : Field K
t : ℕ
inst✝ : Invertible ↑t
⊢ ↑t ≠ 0
[PROOFSTEP]
exact nonzero_of_invertible (t : K)
[GOAL]
K : Type u_1
inst✝¹ : DivisionRing K
inst✝ : CharZero K
⊢ 2 ≠ 0
[PROOFSTEP]
exact_mod_cast (by decide : 2 ≠ 0)
[GOAL]
K : Type u_1
inst✝¹ : DivisionRing K
inst✝ : CharZero K
⊢ 2 ≠ 0
[PROOFSTEP]
decide
[GOAL]
K : Type u_1
inst✝¹ : DivisionRing K
inst✝ : CharZero K
⊢ 3 ≠ 0
[PROOFSTEP]
exact_mod_cast (by decide : 3 ≠ 0)
[GOAL]
K : Type u_1
inst✝¹ : DivisionRing K
inst✝ : CharZero K
⊢ 3 ≠ 0
[PROOFSTEP]
decide
