-- Mathlib/RingTheory/Perfection.lean
theorem valAux_mul (f g : PreTilt O p) :
    valAux K v O p (f * g) = valAux K v O p f * valAux K v O p g

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 : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
f g : PreTilt O p
hf : ¬f = 0
hg : ¬g = 0
⊢ valAux K v O p (f * g) = valAux K v O p f * valAux K v O p g

Tactic:
obtain ⟨m, hm⟩ : ∃ n, coeff _ _ n f ≠ 0 := not_forall.1 fun h => hf <| Perfection.ext h

Result:
case neg.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 : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
f g : PreTilt O p
hf : ¬f = 0
hg : ¬g = 0
m : ℕ
hm : (coeff (ModP O p) p m) f ≠ 0
⊢ valAux K v O p (f * g) = valAux K v O p f * valAux K v O p g

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 : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
f g : PreTilt O p
⊢ valAux K v O p (f * g) = valAux K v O p f * valAux K v O p g

Tactic:
by_cases hf : f = 0

Result:
case pos
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 : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
f g : PreTilt O p
hf : f = 0
⊢ valAux K v O p (f * g) = valAux K v O p f * valAux K v O p g

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 : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
f g : PreTilt O p
hf : ¬f = 0
⊢ valAux K v O p (f * g) = valAux K v O p f * valAux K v O p g

Proof state:
case neg.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 : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
f g : PreTilt O p
hf : ¬f = 0
hg : ¬g = 0
m : ℕ
hm : (coeff (ModP O p) p m) f ≠ 0
n : ℕ
hn : (coeff (ModP O p) p n) g ≠ 0
⊢ valAux K v O p (f * g) = valAux K v O p f * valAux K v O p g

Tactic:
replace hm := coeff_ne_zero_of_le hm (le_max_left m n)

Result:
case neg.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 : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
f g : PreTilt O p
hf : ¬f = 0
hg : ¬g = 0
m n : ℕ
hn : (coeff (ModP O p) p n) g ≠ 0
hm : (coeff (ModP O p) p (m ⊔ n)) f ≠ 0
⊢ valAux K v O p (f * g) = valAux K v O p f * valAux K v O p g

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 : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
f g : PreTilt O p
hf : ¬f = 0
hg : ¬g = 0
m n : ℕ
hm : (coeff (ModP O p) p (m ⊔ n)) f ≠ 0
hn : (coeff (ModP O p) p (m ⊔ n)) g ≠ 0
⊢ (coeff (ModP O p) p (m ⊔ n + 1)) (f * g) ≠ 0

Tactic:
rw [RingHom.map_mul]

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 : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
f g : PreTilt O p
hf : ¬f = 0
hg : ¬g = 0
m n : ℕ
hm : (coeff (ModP O p) p (m ⊔ n)) f ≠ 0
hn : (coeff (ModP O p) p (m ⊔ n)) g ≠ 0
⊢ (coeff (ModP O p) p (m ⊔ n + 1)) f * (coeff (ModP O p) p (m ⊔ n + 1)) g ≠ 0

Proof state:
case refine_1
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 : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
f g : PreTilt O p
hf : ¬f = 0
hg : ¬g = 0
m n : ℕ
hm : (coeff (ModP O p) p (m ⊔ n)) f ≠ 0
hn : (coeff (ModP O p) p (m ⊔ n)) g ≠ 0
⊢ (coeff (ModP O p) p (m ⊔ n + 1)) f ^ p ≠ 0

Tactic:
rw [← RingHom.map_pow, coeff_pow_p f]

Result:
case refine_1
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 : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
f g : PreTilt O p
hf : ¬f = 0
hg : ¬g = 0
m n : ℕ
hm : (coeff (ModP O p) p (m ⊔ n)) f ≠ 0
hn : (coeff (ModP O p) p (m ⊔ n)) g ≠ 0
⊢ (coeff (ModP O p) p (m ⊔ n)) f ≠ 0

Proof state:
case pos
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 : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
f g : PreTilt O p
hf : f = 0
⊢ valAux K v O p (f * g) = valAux K v O p f * valAux K v O p g

Tactic:
rw [hf, zero_mul, valAux_zero, zero_mul]

Result:
no goals

Proof state:
case pos
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 : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
f g : PreTilt O p
hf : ¬f = 0
hg : g = 0
⊢ valAux K v O p (f * g) = valAux K v O p f * valAux K v O p g

Tactic:
rw [hg, mul_zero, valAux_zero, 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 : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
f g : PreTilt O p
hf : ¬f = 0
hg : ¬g = 0
m n : ℕ
hm : (coeff (ModP O p) p (m ⊔ n)) f ≠ 0
hn : (coeff (ModP O p) p (m ⊔ n)) g ≠ 0
⊢ (coeff (ModP O p) p (m ⊔ n + 1)) f * (coeff (ModP O p) p (m ⊔ n + 1)) g ≠ 0

Tactic:
refine ModP.mul_ne_zero_of_pow_p_ne_zero (hv := hv) ?_ ?_

Result:
case refine_1
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 : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
f g : PreTilt O p
hf : ¬f = 0
hg : ¬g = 0
m n : ℕ
hm : (coeff (ModP O p) p (m ⊔ n)) f ≠ 0
hn : (coeff (ModP O p) p (m ⊔ n)) g ≠ 0
⊢ (coeff (ModP O p) p (m ⊔ n + 1)) f ^ p ≠ 0

case refine_2
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 : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
f g : PreTilt O p
hf : ¬f = 0
hg : ¬g = 0
m n : ℕ
hm : (coeff (ModP O p) p (m ⊔ n)) f ≠ 0
hn : (coeff (ModP O p) p (m ⊔ n)) g ≠ 0
⊢ (coeff (ModP O p) p (m ⊔ n + 1)) g ^ p ≠ 0