-- Mathlib/RingTheory/Perfection.lean
theorem preVal_mul {x y : ModP O p} (hxy0 : x * y ≠ 0) :
    preVal K v O p (x * y) = preVal K v O p x * preVal K v O p y

Proof state:
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : v.Integers O
p : ℕ
x y : ModP O p
hxy0 : x * y ≠ 0
hx0 : x ≠ 0
⊢ preVal K v O p (x * y) = preVal K v O p x * preVal K v O p y

Tactic:
have hy0 : y ≠ 0 := mt (by rintro rfl; rw [mul_zero]) hxy0

Result:
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : v.Integers O
p : ℕ
x y : ModP O p
hxy0 : x * y ≠ 0
hx0 : x ≠ 0
hy0 : y ≠ 0
⊢ preVal K v O p (x * y) = preVal K v O p x * preVal K v O p y

Proof state:
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : v.Integers O
p : ℕ
x y : ModP O p
hxy0 : x * y ≠ 0
hx0 : x ≠ 0
⊢ y = 0 → x * y = 0

Tactic:
rintro rfl

Result:
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : v.Integers O
p : ℕ
x : ModP O p
hx0 : x ≠ 0
hxy0 : x * 0 ≠ 0
⊢ x * 0 = 0

Proof state:
case intro.intro
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : v.Integers O
p : ℕ
r : O
hx0 : (Ideal.Quotient.mk (Ideal.span {↑p})) r ≠ 0
s : O
hy0 : (Ideal.Quotient.mk (Ideal.span {↑p})) s ≠ 0
hxy0 : (Ideal.Quotient.mk (Ideal.span {↑p})) (r * s) ≠ 0
⊢ preVal K v O p ((Ideal.Quotient.mk (Ideal.span {↑p})) (r * s)) =
    preVal K v O p ((Ideal.Quotient.mk (Ideal.span {↑p})) r) * preVal K v O p ((Ideal.Quotient.mk (Ideal.span {↑p})) s)

Tactic:
rw [preVal_mk hv hx0, preVal_mk hv hy0, preVal_mk hv hxy0, RingHom.map_mul, v.map_mul]

Result:
no goals

Proof state:
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : v.Integers O
p : ℕ
x y : ModP O p
hxy0 : x * y ≠ 0
hx0 : x ≠ 0
hy0 : y ≠ 0
⊢ preVal K v O p (x * y) = preVal K v O p x * preVal K v O p y

Tactic:
obtain ⟨r, rfl⟩ := Ideal.Quotient.mk_surjective x

Result:
case intro
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : v.Integers O
p : ℕ
y : ModP O p
hy0 : y ≠ 0
r : O
hxy0 : (Ideal.Quotient.mk (Ideal.span {↑p})) r * y ≠ 0
hx0 : (Ideal.Quotient.mk (Ideal.span {↑p})) r ≠ 0
⊢ preVal K v O p ((Ideal.Quotient.mk (Ideal.span {↑p})) r * y) =
    preVal K v O p ((Ideal.Quotient.mk (Ideal.span {↑p})) r) * preVal K v O p y

Proof state:
case intro.intro
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : v.Integers O
p : ℕ
r : O
hx0 : (Ideal.Quotient.mk (Ideal.span {↑p})) r ≠ 0
s : O
hy0 : (Ideal.Quotient.mk (Ideal.span {↑p})) s ≠ 0
hxy0 : (Ideal.Quotient.mk (Ideal.span {↑p})) r * (Ideal.Quotient.mk (Ideal.span {↑p})) s ≠ 0
⊢ preVal K v O p ((Ideal.Quotient.mk (Ideal.span {↑p})) r * (Ideal.Quotient.mk (Ideal.span {↑p})) s) =
    preVal K v O p ((Ideal.Quotient.mk (Ideal.span {↑p})) r) * preVal K v O p ((Ideal.Quotient.mk (Ideal.span {↑p})) s)

Tactic:
rw [← map_mul (Ideal.Quotient.mk (Ideal.span {↑p})) r s] at hxy0 ⊢

Result:
case intro.intro
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : v.Integers O
p : ℕ
r : O
hx0 : (Ideal.Quotient.mk (Ideal.span {↑p})) r ≠ 0
s : O
hy0 : (Ideal.Quotient.mk (Ideal.span {↑p})) s ≠ 0
hxy0 : (Ideal.Quotient.mk (Ideal.span {↑p})) (r * s) ≠ 0
⊢ preVal K v O p ((Ideal.Quotient.mk (Ideal.span {↑p})) (r * s)) =
    preVal K v O p ((Ideal.Quotient.mk (Ideal.span {↑p})) r) * preVal K v O p ((Ideal.Quotient.mk (Ideal.span {↑p})) s)

Proof state:
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : v.Integers O
p : ℕ
x y : ModP O p
hxy0 : x * y ≠ 0
⊢ preVal K v O p (x * y) = preVal K v O p x * preVal K v O p y

Tactic:
have hx0 : x ≠ 0 := mt (by rintro rfl; rw [zero_mul]) hxy0

Result:
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : v.Integers O
p : ℕ
x y : ModP O p
hxy0 : x * y ≠ 0
hx0 : x ≠ 0
⊢ preVal K v O p (x * y) = preVal K v O p x * preVal K v O p y

Proof state:
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : v.Integers O
p : ℕ
x : ModP O p
hx0 : x ≠ 0
hxy0 : x * 0 ≠ 0
⊢ x * 0 = 0

Tactic:
rw [mul_zero]

Result:
no goals

Proof state:
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : v.Integers O
p : ℕ
y : ModP O p
hxy0 : 0 * y ≠ 0
⊢ 0 * y = 0

Tactic:
rw [zero_mul]

Result:
no goals

Proof state:
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : v.Integers O
p : ℕ
x y : ModP O p
hxy0 : x * y ≠ 0
⊢ x = 0 → x * y = 0

Tactic:
rintro rfl

Result:
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : v.Integers O
p : ℕ
y : ModP O p
hxy0 : 0 * y ≠ 0
⊢ 0 * y = 0

Proof state:
case intro
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : v.Integers O
p : ℕ
y : ModP O p
hy0 : y ≠ 0
r : O
hxy0 : (Ideal.Quotient.mk (Ideal.span {↑p})) r * y ≠ 0
hx0 : (Ideal.Quotient.mk (Ideal.span {↑p})) r ≠ 0
⊢ preVal K v O p ((Ideal.Quotient.mk (Ideal.span {↑p})) r * y) =
    preVal K v O p ((Ideal.Quotient.mk (Ideal.span {↑p})) r) * preVal K v O p y

Tactic:
obtain ⟨s, rfl⟩ := Ideal.Quotient.mk_surjective y

Result:
case intro.intro
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : v.Integers O
p : ℕ
r : O
hx0 : (Ideal.Quotient.mk (Ideal.span {↑p})) r ≠ 0
s : O
hy0 : (Ideal.Quotient.mk (Ideal.span {↑p})) s ≠ 0
hxy0 : (Ideal.Quotient.mk (Ideal.span {↑p})) r * (Ideal.Quotient.mk (Ideal.span {↑p})) s ≠ 0
⊢ preVal K v O p ((Ideal.Quotient.mk (Ideal.span {↑p})) r * (Ideal.Quotient.mk (Ideal.span {↑p})) s) =
    preVal K v O p ((Ideal.Quotient.mk (Ideal.span {↑p})) r) * preVal K v O p ((Ideal.Quotient.mk (Ideal.span {↑p})) s)