Theorem: QuadRing.gaussian_val_mul_eq_add (ECTate/Algebra/QuadRing/Valuations.lean)

State before:
p : ℕ
prime : Nat.Prime p
a b : QuadRing ℤ 0 (-1)
⊢ gaussian_val p (a * b) = gaussian_val p a + gaussian_val p b
Tactic:
simp [gaussian_val]
State after:
p : ℕ
prime : Nat.Prime p
a b : QuadRing ℤ 0 (-1)
⊢ min (Int.int_val p (a.b1 * b.b1 + -(a.b2 * b.b2))) (Int.int_val p (a.b2 * b.b1 + a.b1 * b.b2)) =
    min (Int.int_val p a.b1) (Int.int_val p a.b2) + min (Int.int_val p b.b1) (Int.int_val p b.b2)

State before:
p : ℕ
prime : Nat.Prime p
a b : QuadRing ℤ 0 (-1)
⊢ min (Int.int_val p (a.b1 * b.b1 + -(a.b2 * b.b2))) (Int.int_val p (a.b2 * b.b1 + a.b1 * b.b2)) =
    min (Int.int_val p a.b1) (Int.int_val p a.b2) + min (Int.int_val p b.b1) (Int.int_val p b.b2)
Tactic:
sorry
State after:
no goals