-- Mathlib/NumberTheory/Dioph.lean
theorem mod_dioph : DiophFn fun v => f v % g v :=
  have : Dioph fun v : Vector3 ℕ 3 => (v &2 = 0 ∨ v &0 < v &2) ∧ ∃ x : ℕ, v &0 + v &2 * x = v &1 :=
    (D&2 D= D.0 D∨ D&0 D< D&2) D∧ (D∃) 3 <| D&1 D+ D&3 D* D&0 D= D&2
  diophFn_comp2 df dg <|
    (diophFn_vec _).2 <|
      ext this <|
        (vectorAll_iff_forall _).1 fun z x y =>
          show ((y = 0 ∨ z < y) ∧ ∃ c, z + y * c = x) ↔ x % y = z from
            ⟨fun ⟨h, c, hc⟩ => by
              rw [← hc]; simp only [add_mul_mod_self_left]; rcases h with x0 | hl
              · rw [x0, mod_zero]
              exact mod_eq_of_lt hl, fun e => by
                rw [← e]
                exact ⟨or_iff_not_imp_left.2 fun h => mod_lt _ (Nat.pos_of_ne_zero h), x / y,
                  mod_add_div _ _⟩⟩

Proof state:
α : Type
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
this : Dioph fun v => (v &2 = 0 ∨ v &0 < v &2) ∧ ∃ x, v &0 + v &2 * x = v &1
z x y : ℕ
e : x % y = z
⊢ (y = 0 ∨ z < y) ∧ ∃ c, z + y * c = x

Tactic:
rw [← e]

Result:
α : Type
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
this : Dioph fun v => (v &2 = 0 ∨ v &0 < v &2) ∧ ∃ x, v &0 + v &2 * x = v &1
z x y : ℕ
e : x % y = z
⊢ (y = 0 ∨ x % y < y) ∧ ∃ c, x % y + y * c = x

Proof state:
α : Type
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
this : Dioph fun v => (v &2 = 0 ∨ v &0 < v &2) ∧ ∃ x, v &0 + v &2 * x = v &1
z x y : ℕ
x✝ : (y = 0 ∨ z < y) ∧ ∃ c, z + y * c = x
h : y = 0 ∨ z < y
c : ℕ
hc : z + y * c = x
⊢ (z + y * c) % y = z

Tactic:
simp only [add_mul_mod_self_left]

Result:
α : Type
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
this : Dioph fun v => (v &2 = 0 ∨ v &0 < v &2) ∧ ∃ x, v &0 + v &2 * x = v &1
z x y : ℕ
x✝ : (y = 0 ∨ z < y) ∧ ∃ c, z + y * c = x
h : y = 0 ∨ z < y
c : ℕ
hc : z + y * c = x
⊢ z % y = z

Proof state:
case inl
α : Type
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
this : Dioph fun v => (v &2 = 0 ∨ v &0 < v &2) ∧ ∃ x, v &0 + v &2 * x = v &1
z x y : ℕ
x✝ : (y = 0 ∨ z < y) ∧ ∃ c, z + y * c = x
c : ℕ
hc : z + y * c = x
x0 : y = 0
⊢ z % y = z

Tactic:
rw [x0, mod_zero]

Result:
no goals

Proof state:
α : Type
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
this : Dioph fun v => (v &2 = 0 ∨ v &0 < v &2) ∧ ∃ x, v &0 + v &2 * x = v &1
z x y : ℕ
x✝ : (y = 0 ∨ z < y) ∧ ∃ c, z + y * c = x
h : y = 0 ∨ z < y
c : ℕ
hc : z + y * c = x
⊢ x % y = z

Tactic:
rw [← hc]

Result:
α : Type
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
this : Dioph fun v => (v &2 = 0 ∨ v &0 < v &2) ∧ ∃ x, v &0 + v &2 * x = v &1
z x y : ℕ
x✝ : (y = 0 ∨ z < y) ∧ ∃ c, z + y * c = x
h : y = 0 ∨ z < y
c : ℕ
hc : z + y * c = x
⊢ (z + y * c) % y = z

Proof state:
case inr
α : Type
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
this : Dioph fun v => (v &2 = 0 ∨ v &0 < v &2) ∧ ∃ x, v &0 + v &2 * x = v &1
z x y : ℕ
x✝ : (y = 0 ∨ z < y) ∧ ∃ c, z + y * c = x
c : ℕ
hc : z + y * c = x
hl : z < y
⊢ z % y = z

Tactic:
exact mod_eq_of_lt hl

Result:
no goals

Proof state:
α : Type
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
this : Dioph fun v => (v &2 = 0 ∨ v &0 < v &2) ∧ ∃ x, v &0 + v &2 * x = v &1
z x y : ℕ
x✝ : (y = 0 ∨ z < y) ∧ ∃ c, z + y * c = x
h : y = 0 ∨ z < y
c : ℕ
hc : z + y * c = x
⊢ z % y = z

Tactic:
rcases h with x0 | hl

Result:
case inl
α : Type
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
this : Dioph fun v => (v &2 = 0 ∨ v &0 < v &2) ∧ ∃ x, v &0 + v &2 * x = v &1
z x y : ℕ
x✝ : (y = 0 ∨ z < y) ∧ ∃ c, z + y * c = x
c : ℕ
hc : z + y * c = x
x0 : y = 0
⊢ z % y = z

case inr
α : Type
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
this : Dioph fun v => (v &2 = 0 ∨ v &0 < v &2) ∧ ∃ x, v &0 + v &2 * x = v &1
z x y : ℕ
x✝ : (y = 0 ∨ z < y) ∧ ∃ c, z + y * c = x
c : ℕ
hc : z + y * c = x
hl : z < y
⊢ z % y = z

Proof state:
α : Type
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
this : Dioph fun v => (v &2 = 0 ∨ v &0 < v &2) ∧ ∃ x, v &0 + v &2 * x = v &1
z x y : ℕ
e : x % y = z
⊢ (y = 0 ∨ x % y < y) ∧ ∃ c, x % y + y * c = x

Tactic:
exact ⟨or_iff_not_imp_left.2 fun h => mod_lt _ (Nat.pos_of_ne_zero h), x / y,
  mod_add_div _ _⟩

Result:
no goals