-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Div/Basic.lean
theorem mul_mod_mul_left (z x y : Nat) : (z * x) % (z * y) = z * (x % y) :=
  if y0 : y = 0 then by
    rw [y0, Nat.mul_zero, mod_zero, mod_zero]
  else if z0 : z = 0 then by
    rw [z0, Nat.zero_mul, Nat.zero_mul, Nat.zero_mul, mod_zero]
  else by
    induction x using Nat.strongRecOn with
    | _ n IH =>
      have y0 : y > 0 := Nat.pos_of_ne_zero y0
      have z0 : z > 0 := Nat.pos_of_ne_zero z0
      cases Nat.lt_or_ge n y with
      | inl yn => rw [mod_eq_of_lt yn, mod_eq_of_lt (Nat.mul_lt_mul_of_pos_left yn z0)]
      | inr yn =>
        rw [mod_eq_sub_mod yn, mod_eq_sub_mod (Nat.mul_le_mul_left z yn),
          ← Nat.mul_sub_left_distrib]
        exact IH _ (sub_lt (Nat.lt_of_lt_of_le y0 yn) y0)

Proof state:
case ind
z y : Nat
y0✝ : ¬y = 0
z0✝ : ¬z = 0
n : Nat
IH : ∀ (m : Nat), m < n → z * m % (z * y) = z * (m % y)
y0 : y > 0
z0 : z > 0
⊢ z * n % (z * y) = z * (n % y)

Tactic:
cases Nat.lt_or_ge n y with
| inl yn => rw [mod_eq_of_lt yn, mod_eq_of_lt (Nat.mul_lt_mul_of_pos_left yn z0)]
| inr yn =>
  rw [mod_eq_sub_mod yn, mod_eq_sub_mod (Nat.mul_le_mul_left z yn),
    ← Nat.mul_sub_left_distrib]
  exact IH _ (sub_lt (Nat.lt_of_lt_of_le y0 yn) y0)

Result:
no goals

Proof state:
case ind.inr
z y : Nat
y0✝ : ¬y = 0
z0✝ : ¬z = 0
n : Nat
IH : ∀ (m : Nat), m < n → z * m % (z * y) = z * (m % y)
y0 : y > 0
z0 : z > 0
yn : n ≥ y
⊢ z * n % (z * y) = z * (n % y)

Tactic:
rw [mod_eq_sub_mod yn, mod_eq_sub_mod (Nat.mul_le_mul_left z yn),
  ← Nat.mul_sub_left_distrib]

Result:
case ind.inr
z y : Nat
y0✝ : ¬y = 0
z0✝ : ¬z = 0
n : Nat
IH : ∀ (m : Nat), m < n → z * m % (z * y) = z * (m % y)
y0 : y > 0
z0 : z > 0
yn : n ≥ y
⊢ z * (n - y) % (z * y) = z * ((n - y) % y)

Proof state:
case ind.inl
z y : Nat
y0✝ : ¬y = 0
z0✝ : ¬z = 0
n : Nat
IH : ∀ (m : Nat), m < n → z * m % (z * y) = z * (m % y)
y0 : y > 0
z0 : z > 0
yn : n < y
⊢ z * n % (z * y) = z * (n % y)

Tactic:
rw [mod_eq_of_lt yn, mod_eq_of_lt (Nat.mul_lt_mul_of_pos_left yn z0)]

Result:
no goals

Proof state:
z x y : Nat
y0 : y = 0
⊢ z * x % (z * y) = z * (x % y)

Tactic:
rw [y0, Nat.mul_zero, mod_zero, mod_zero]

Result:
no goals

Proof state:
case ind.inr
z y : Nat
y0✝ : ¬y = 0
z0✝ : ¬z = 0
n : Nat
IH : ∀ (m : Nat), m < n → z * m % (z * y) = z * (m % y)
y0 : y > 0
z0 : z > 0
yn : n ≥ y
⊢ z * (n - y) % (z * y) = z * ((n - y) % y)

Tactic:
exact IH _ (sub_lt (Nat.lt_of_lt_of_le y0 yn) y0)

Result:
no goals

Proof state:
z x y : Nat
y0 : ¬y = 0
z0 : z = 0
⊢ z * x % (z * y) = z * (x % y)

Tactic:
rw [z0, Nat.zero_mul, Nat.zero_mul, Nat.zero_mul, mod_zero]

Result:
no goals

Proof state:
case ind
z y : Nat
y0✝ : ¬y = 0
z0 : ¬z = 0
n : Nat
IH : ∀ (m : Nat), m < n → z * m % (z * y) = z * (m % y)
y0 : y > 0
⊢ z * n % (z * y) = z * (n % y)

Tactic:
have z0 : z > 0 := Nat.pos_of_ne_zero z0

Result:
case ind
z y : Nat
y0✝ : ¬y = 0
z0✝ : ¬z = 0
n : Nat
IH : ∀ (m : Nat), m < n → z * m % (z * y) = z * (m % y)
y0 : y > 0
z0 : z > 0
⊢ z * n % (z * y) = z * (n % y)

Proof state:
case ind
z y : Nat
y0 : ¬y = 0
z0 : ¬z = 0
n : Nat
IH : ∀ (m : Nat), m < n → z * m % (z * y) = z * (m % y)
⊢ z * n % (z * y) = z * (n % y)

Tactic:
have y0 : y > 0 := Nat.pos_of_ne_zero y0

Result:
case ind
z y : Nat
y0✝ : ¬y = 0
z0 : ¬z = 0
n : Nat
IH : ∀ (m : Nat), m < n → z * m % (z * y) = z * (m % y)
y0 : y > 0
⊢ z * n % (z * y) = z * (n % y)

Proof state:
z x y : Nat
y0 : ¬y = 0
z0 : ¬z = 0
⊢ z * x % (z * y) = z * (x % y)

Tactic:
induction x using Nat.strongRecOn with
| _ n IH =>
  have y0 : y > 0 := Nat.pos_of_ne_zero y0
  have z0 : z > 0 := Nat.pos_of_ne_zero z0
  cases Nat.lt_or_ge n y with
  | inl yn => rw [mod_eq_of_lt yn, mod_eq_of_lt (Nat.mul_lt_mul_of_pos_left yn z0)]
  | inr yn =>
    rw [mod_eq_sub_mod yn, mod_eq_sub_mod (Nat.mul_le_mul_left z yn),
      ← Nat.mul_sub_left_distrib]
    exact IH _ (sub_lt (Nat.lt_of_lt_of_le y0 yn) y0)

Result:
no goals