R : Type u_1
inst✝ : NonAssocSemiring R
this : DecidableEq R := Classical.decEq R
H : ∀ (p : ℕ), ↑p = 0 → p = 0
x : ℕ
⊢ ↑x = 0 ↔ x = 0
R : Type u_1
inst✝ : NonAssocSemiring R
this : DecidableEq R := Classical.decEq R
H : ∀ (p : ℕ), ↑p = 0 → p = 0
x : ℕ
⊢ ↑x = 0 ↔ 0 ∣ x
rw [zero_dvd_iff]
no goals
R : Type u_1
inst✝ : NonAssocSemiring R
this : DecidableEq R := Classical.decEq R
H : ∀ (p : ℕ), ↑p = 0 → p = 0
x : ℕ
⊢ ↑x = 0 ↔ x = 0
exact ⟨H x, by rintro rfl; simp⟩
R : Type u_1
inst✝ : NonAssocSemiring R
this : DecidableEq R := Classical.decEq R
H : ∀ (p : ℕ), ↑p = 0 → p = 0
⊢ ↑0 = 0
R : Type u_1
inst✝ : NonAssocSemiring R
this : DecidableEq R := Classical.decEq R
H : ∀ (p : ℕ), ↑p = 0 → p = 0
x : ℕ
⊢ x = 0 → ↑x = 0
rintro rfl
no goals
R : Type u_1
inst✝ : NonAssocSemiring R
this : DecidableEq R := Classical.decEq R
H : ∀ (p : ℕ), ↑p = 0 → p = 0
⊢ ↑0 = 0
simp
no goals
R : Type u_1
inst✝ : NonAssocSemiring R
this : DecidableEq R := Classical.decEq R
H : ¬∀ (p : ℕ), ↑p = 0 → p = 0
x : ℕ
H1 : ↑x = 0
H2 : ¬x % Nat.find (_ : ∃ x, ¬(↑x = 0 → x = 0)) = 0
⊢ ↑(x % Nat.find (_ : ∃ x, ¬(↑x = 0 → x = 0))) = 0
rwa [← Nat.mod_add_div x (Nat.find (not_forall.1 H)), Nat.cast_add,
  Nat.cast_mul,
  of_not_not (not_not_of_not_imp <| Nat.find_spec (not_forall.1 H)),
  MulZeroClass.zero_mul, add_zero] at H1
no goals
R : Type u_1
inst✝ : NonAssocSemiring R
this : DecidableEq R := Classical.decEq R
H : ¬∀ (p : ℕ), ↑p = 0 → p = 0
x : ℕ
H1 : Nat.find (_ : ∃ x, ¬(↑x = 0 → x = 0)) ∣ x
⊢ ↑x = 0
rw [← Nat.mul_div_cancel' H1, Nat.cast_mul,
  of_not_not (not_not_of_not_imp <| Nat.find_spec (not_forall.1 H)),
  MulZeroClass.zero_mul]