-- Lean 4 proof step from Mathlib.Algebra.CharP.Defs (goal)
Goal:
R : Type u_1
inst : NonAssocSemiring R
this : DecidableEq R := Classical.decEq R
H : ¬∀ (p : ℕ), Eq.{u_1 + 1} (α := R) (↑p : R) 0 → p = 0
x : ℕ
H1 : Eq.{u_1 + 1} (α := R) (↑x : R) 0
H2 : ¬x % Nat.find (p := fun (n : ℕ) ↦ ¬(Eq.{u_1 + 1} (α := R) (↑n : R) 0 → n = 0)) ⋯ = 0
rwa :
  ∀
    (H1 :
      Eq.{u_1 + 1} (α := R)
        (↑(x % Nat.find (p := fun (n : ℕ) ↦ ¬(Eq.{u_1 + 1} (α := R) (↑n : R) 0 → n = 0)) ⋯ +
              Nat.find (p := fun (n : ℕ) ↦ ¬(Eq.{u_1 + 1} (α := R) (↑n : R) 0 → n = 0)) ⋯ *
                (x / Nat.find (p := fun (n : ℕ) ↦ ¬(Eq.{u_1 + 1} (α := R) (↑n : R) 0 → n = 0)) ⋯)) :
          R)
        0)
    (H2 : ¬x % Nat.find (p := fun (n : ℕ) ↦ ¬(Eq.{u_1 + 1} (α := R) (↑n : R) 0 → n = 0)) ⋯ = 0),
    Eq.{u_1 + 1} (α := R) (↑(x % Nat.find (p := fun (n : ℕ) ↦ ¬(Eq.{u_1 + 1} (α := R) (↑n : R) 0 → n = 0)) ⋯) : R) 0
rwa₁ :
  ∀
    (H1 :
      HAdd.hAdd (α := R) (↑(x % Nat.find (p := fun (n : ℕ) ↦ ¬(Eq.{u_1 + 1} (α := R) (↑n : R) 0 → n = 0)) ⋯) : R)
          (↑(Nat.find (p := fun (n : ℕ) ↦ ¬(Eq.{u_1 + 1} (α := R) (↑n : R) 0 → n = 0)) ⋯ *
                (x / Nat.find (p := fun (n : ℕ) ↦ ¬(Eq.{u_1 + 1} (α := R) (↑n : R) 0 → n = 0)) ⋯)) :
            R) =
        0)
    (H2 : ¬x % Nat.find (p := fun (n : ℕ) ↦ ¬(Eq.{u_1 + 1} (α := R) (↑n : R) 0 → n = 0)) ⋯ = 0),
    Eq.{u_1 + 1} (α := R) (↑(x % Nat.find (p := fun (n : ℕ) ↦ ¬(Eq.{u_1 + 1} (α := R) (↑n : R) 0 → n = 0)) ⋯) : R) 0
rwa₂ :
  ∀
    (H1 :
      (↑(x % Nat.find (p := fun (n : ℕ) ↦ ¬(Eq.{u_1 + 1} (α := R) (↑n : R) 0 → n = 0)) ⋯) : R) +
          HMul.hMul (α := R) (↑(Nat.find (p := fun (n : ℕ) ↦ ¬(Eq.{u_1 + 1} (α := R) (↑n : R) 0 → n = 0)) ⋯) : R)
            (↑(x / Nat.find (p := fun (n : ℕ) ↦ ¬(Eq.{u_1 + 1} (α := R) (↑n : R) 0 → n = 0)) ⋯) : R) =
        0)
    (H2 : ¬x % Nat.find (p := fun (n : ℕ) ↦ ¬(Eq.{u_1 + 1} (α := R) (↑n : R) 0 → n = 0)) ⋯ = 0),
    Eq.{u_1 + 1} (α := R) (↑(x % Nat.find (p := fun (n : ℕ) ↦ ¬(Eq.{u_1 + 1} (α := R) (↑n : R) 0 → n = 0)) ⋯) : R) 0
rwa₃ :
  ∀
    (H1 :
      (↑(x % Nat.find (p := fun (n : ℕ) ↦ ¬(Eq.{u_1 + 1} (α := R) (↑n : R) 0 → n = 0)) ⋯) : R) +
          HMul.hMul (α := R) 0
            (↑(x / Nat.find (p := fun (n : ℕ) ↦ ¬(Eq.{u_1 + 1} (α := R) (↑n : R) 0 → n = 0)) ⋯) : R) =
        0)
    (H2 : ¬x % Nat.find (p := fun (n : ℕ) ↦ ¬(Eq.{u_1 + 1} (α := R) (↑n : R) 0 → n = 0)) ⋯ = 0),
    Eq.{u_1 + 1} (α := R) (↑(x % Nat.find (p := fun (n : ℕ) ↦ ¬(Eq.{u_1 + 1} (α := R) (↑n : R) 0 → n = 0)) ⋯) : R) 0
⊢ Eq.{u_1 + 1} (α := R) (↑(x % Nat.find (p := fun (n : ℕ) ↦ ¬(Eq.{u_1 + 1} (α := R) (↑n : R) 0 → n = 0)) ⋯) : R) 0
have rwa₄ : ∀
  (H1 :
    HAdd.hAdd (α := R) (↑(x % Nat.find (p := fun (n : ℕ) ↦ ¬(Eq.{u_1 + 1} (α := R) (↑n : R) 0 → n = 0)) sorry) : R) 0 = 0)
  (H2 : ¬x % Nat.find (p := fun (n : ℕ) ↦ ¬(Eq.{u_1 + 1} (α := R) (↑n : R) 0 → n = 0)) sorry = 0),
  Eq.{u_1 + 1} (α := R) (↑(x % Nat.find (p := fun (n : ℕ) ↦ ¬(Eq.{u_1 + 1} (α := R) (↑n : R) 0 → n = 0)) sorry) : R) 0
Tactic: 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)),
                      zero_mul, add_zero] at H1
Cleared hypotheses: H1, H2