m k : ℕ+
h₀ : ↑m % ↑k + ↑k * (↑m / ↑k) = ↑m := Nat.mod_add_div ↑m ↑k
⊢ ↑(mod m k) + ↑k * div m k = ↑m
m k : ℕ+
⊢ ↑(mod m k) + ↑k * div m k = ↑m
let h₀ := Nat.mod_add_div (m : ℕ) (k : ℕ)
m k : ℕ+
h₀ : ↑m % ↑k + ↑k * (↑m / ↑k) = ↑m := Nat.mod_add_div ↑m ↑k
this : ¬(↑m % ↑k = 0 ∧ ↑m / ↑k = 0)
⊢ ↑(mod m k) + ↑k * div m k = ↑m
m k : ℕ+
h₀ : ↑m % ↑k + ↑k * (↑m / ↑k) = ↑m := Nat.mod_add_div ↑m ↑k
⊢ ↑(mod m k) + ↑k * div m k = ↑m
have : ¬((m : ℕ) % (k : ℕ) = 0 ∧ (m : ℕ) / (k : ℕ) = 0) := by
  rintro ⟨hr, hq⟩
  rw [hr, hq, mul_zero, zero_add] at h₀
  exact (m.ne_zero h₀.symm).elim
m k : ℕ+
h₀ : ↑m % ↑k + ↑k * (↑m / ↑k) = ↑m := Nat.mod_add_div ↑m ↑k
this✝ : ¬(↑m % ↑k = 0 ∧ ↑m / ↑k = 0)
this : ↑(modDivAux k (↑m % ↑k) (↑m / ↑k)).fst + ↑k * (modDivAux k (↑m % ↑k) (↑m / ↑k)).snd = ↑m % ↑k + ↑k * (↑m / ↑k)
⊢ ↑(mod m k) + ↑k * div m k = ↑m
m k : ℕ+
h₀ : ↑m % ↑k + ↑k * (↑m / ↑k) = ↑m := Nat.mod_add_div ↑m ↑k
this : ¬(↑m % ↑k = 0 ∧ ↑m / ↑k = 0)
⊢ ↑(mod m k) + ↑k * div m k = ↑m
have := modDivAux_spec k ((m : ℕ) % (k : ℕ)) ((m : ℕ) / (k : ℕ)) this
no goals
m k : ℕ+
h₀ : ↑m % ↑k + ↑k * (↑m / ↑k) = ↑m := Nat.mod_add_div ↑m ↑k
this✝ : ¬(↑m % ↑k = 0 ∧ ↑m / ↑k = 0)
this : ↑(modDivAux k (↑m % ↑k) (↑m / ↑k)).fst + ↑k * (modDivAux k (↑m % ↑k) (↑m / ↑k)).snd = ↑m % ↑k + ↑k * (↑m / ↑k)
⊢ ↑(mod m k) + ↑k * div m k = ↑m
exact this.trans h₀
case intro
m k : ℕ+
h₀ : ↑m % ↑k + ↑k * (↑m / ↑k) = ↑m := Nat.mod_add_div ↑m ↑k
hr : ↑m % ↑k = 0
hq : ↑m / ↑k = 0
⊢ False
m k : ℕ+
h₀ : ↑m % ↑k + ↑k * (↑m / ↑k) = ↑m := Nat.mod_add_div ↑m ↑k
⊢ ¬(↑m % ↑k = 0 ∧ ↑m / ↑k = 0)
rintro ⟨hr, hq⟩
case intro
m k : ℕ+
h₀ : 0 = ↑m
hr : ↑m % ↑k = 0
hq : ↑m / ↑k = 0
⊢ False
case intro
m k : ℕ+
h₀ : ↑m % ↑k + ↑k * (↑m / ↑k) = ↑m := Nat.mod_add_div ↑m ↑k
hr : ↑m % ↑k = 0
hq : ↑m / ↑k = 0
⊢ False
rw [hr, hq, mul_zero, zero_add] at h₀
no goals
case intro
m k : ℕ+
h₀ : 0 = ↑m
hr : ↑m % ↑k = 0
hq : ↑m / ↑k = 0
⊢ False
exact (m.ne_zero h₀.symm).elim