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

State before:
p : ℕ
gt1 : 1 < p
⊢ gaussian_val p ↑p = 1
Tactic:
rw [gaussian_val]
State after:
p : ℕ
gt1 : 1 < p
⊢ min (Int.int_val p (↑p).b1) (Int.int_val p (↑p).b2) = 1

State before:
p : ℕ
gt1 : 1 < p
⊢ min (Int.int_val p (↑p).b1) (Int.int_val p (↑p).b2) = 1
Tactic:
simp [gt1]
State after:
no goals