-- Mathlib/RingTheory/Perfection.lean
theorem mul_ne_zero_of_pow_p_ne_zero {x y : ModP O p} (hx : x ^ p ≠ 0) (hy : y ^ p ≠ 0) :
    x * y ≠ 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 : ℕ
hp : Fact (Nat.Prime p)
r : O
hx : v ↑p < v ((algebraMap O K) (r ^ p))
s : O
hy : v ↑p < v ((algebraMap O K) (s ^ p))
h1p : 0 < 1 / ↑p
⊢ v ↑p < v ((algebraMap O K) (r * s))

Tactic:
rw [RingHom.map_pow, v.map_pow, ← rpow_lt_rpow_iff h1p, ← rpow_natCast, ← rpow_mul,
  mul_one_div_cancel (Nat.cast_ne_zero.2 hp.1.ne_zero : (p : ℝ) ≠ 0), rpow_one] at hx hy

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 : ℕ
hp : Fact (Nat.Prime p)
r : O
hx : v ↑p ^ (1 / ↑p) < v ((algebraMap O K) r)
s : O
hy : v ↑p ^ (1 / ↑p) < v ((algebraMap O K) s)
h1p : 0 < 1 / ↑p
⊢ v ↑p < v ((algebraMap O K) (r * s))

Proof state:
case neg
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 : ℕ
hp : Fact (Nat.Prime p)
r : O
hx : v ↑p ^ (1 / ↑p) < v ((algebraMap O K) r)
s : O
hy : v ↑p ^ (1 / ↑p) < v ((algebraMap O K) s)
h1p : 0 < 1 / ↑p
hvp : 0 < v ↑p
⊢ 1 / ↑p + 1 / ↑p ≤ 1

Tactic:
rw [← add_div, div_le_one (Nat.cast_pos.2 hp.1.pos : 0 < (p : ℝ))]

Result:
case neg
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 : ℕ
hp : Fact (Nat.Prime p)
r : O
hx : v ↑p ^ (1 / ↑p) < v ((algebraMap O K) r)
s : O
hy : v ↑p ^ (1 / ↑p) < v ((algebraMap O K) s)
h1p : 0 < 1 / ↑p
hvp : 0 < v ↑p
⊢ 1 + 1 ≤ ↑p

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 : ℕ
hp : Fact (Nat.Prime p)
r : O
hx : (Ideal.Quotient.mk (Ideal.span {↑p})) r ^ p ≠ 0
s : O
hy : (Ideal.Quotient.mk (Ideal.span {↑p})) s ^ p ≠ 0
⊢ (Ideal.Quotient.mk (Ideal.span {↑p})) r * (Ideal.Quotient.mk (Ideal.span {↑p})) s ≠ 0

Tactic:
have h1p : (0 : ℝ) < 1 / p := one_div_pos.2 (Nat.cast_pos.2 hp.1.pos)

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 : ℕ
hp : Fact (Nat.Prime p)
r : O
hx : (Ideal.Quotient.mk (Ideal.span {↑p})) r ^ p ≠ 0
s : O
hy : (Ideal.Quotient.mk (Ideal.span {↑p})) s ^ p ≠ 0
h1p : 0 < 1 / ↑p
⊢ (Ideal.Quotient.mk (Ideal.span {↑p})) r * (Ideal.Quotient.mk (Ideal.span {↑p})) s ≠ 0

Proof state:
case neg
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 : ℕ
hp : Fact (Nat.Prime p)
r : O
hx : v ↑p ^ (1 / ↑p) < v ((algebraMap O K) r)
s : O
hy : v ↑p ^ (1 / ↑p) < v ((algebraMap O K) s)
h1p : 0 < 1 / ↑p
hvp : 0 < v ↑p
⊢ v ↑p ^ 1 ≤ v ↑p ^ (1 / ↑p + 1 / ↑p)

Tactic:
refine rpow_le_rpow_of_exponent_ge hvp (map_natCast (algebraMap O K) p ▸ hv.2 _) ?_

Result:
case neg
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 : ℕ
hp : Fact (Nat.Prime p)
r : O
hx : v ↑p ^ (1 / ↑p) < v ((algebraMap O K) r)
s : O
hy : v ↑p ^ (1 / ↑p) < v ((algebraMap O K) s)
h1p : 0 < 1 / ↑p
hvp : 0 < v ↑p
⊢ 1 / ↑p + 1 / ↑p ≤ 1

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 : ℕ
hp : Fact (Nat.Prime p)
r : O
hx : (Ideal.Quotient.mk (Ideal.span {↑p})) (r ^ p) ≠ 0
s : O
hy : (Ideal.Quotient.mk (Ideal.span {↑p})) (s ^ p) ≠ 0
h1p : 0 < 1 / ↑p
⊢ (Ideal.Quotient.mk (Ideal.span {↑p})) (r * s) ≠ 0

Tactic:
rw [← v_p_lt_val hv] at hx hy ⊢

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 : ℕ
hp : Fact (Nat.Prime p)
r : O
hx : v ↑p < v ((algebraMap O K) (r ^ p))
s : O
hy : v ↑p < v ((algebraMap O K) (s ^ p))
h1p : 0 < 1 / ↑p
⊢ v ↑p < v ((algebraMap O K) (r * s))

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 : ℕ
hp : Fact (Nat.Prime p)
r : O
hx : v ↑p ^ (1 / ↑p) < v ((algebraMap O K) r)
s : O
hy : v ↑p ^ (1 / ↑p) < v ((algebraMap O K) s)
h1p : 0 < 1 / ↑p
⊢ v ↑p < v ((algebraMap O K) r) * v ((algebraMap O K) s)

Tactic:
refine lt_of_le_of_lt ?_ (mul_lt_mul'' hx hy zero_le' zero_le')

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 : ℕ
hp : Fact (Nat.Prime p)
r : O
hx : v ↑p ^ (1 / ↑p) < v ((algebraMap O K) r)
s : O
hy : v ↑p ^ (1 / ↑p) < v ((algebraMap O K) s)
h1p : 0 < 1 / ↑p
⊢ v ↑p ≤ v ↑p ^ (1 / ↑p) * v ↑p ^ (1 / ↑p)

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 : ℕ
hp : Fact (Nat.Prime p)
r : O
hx : (Ideal.Quotient.mk (Ideal.span {↑p})) r ^ p ≠ 0
s : O
hy : (Ideal.Quotient.mk (Ideal.span {↑p})) s ^ p ≠ 0
h1p : 0 < 1 / ↑p
⊢ (Ideal.Quotient.mk (Ideal.span {↑p})) (r * s) ≠ 0

Tactic:
rw [← (Ideal.Quotient.mk (Ideal.span {(p : O)})).map_pow] at hx hy

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 : ℕ
hp : Fact (Nat.Prime p)
r : O
hx : (Ideal.Quotient.mk (Ideal.span {↑p})) (r ^ p) ≠ 0
s : O
hy : (Ideal.Quotient.mk (Ideal.span {↑p})) (s ^ p) ≠ 0
h1p : 0 < 1 / ↑p
⊢ (Ideal.Quotient.mk (Ideal.span {↑p})) (r * s) ≠ 0