-- 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 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

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

Result:
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)) g ≠ 0

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 n : ℕ
hm : (coeff (ModP O p) p (m ⊔ n)) f ≠ 0
hn : (coeff (ModP O p) p (m ⊔ n)) g ≠ 0
hfg : (coeff (ModP O p) p (m ⊔ n + 1)) (f * g) ≠ 0
⊢ ModP.preVal K v O p ((coeff (ModP O p) p (m ⊔ n + 1)) (f * g)) ^ p ^ (m ⊔ n + 1) =
    ModP.preVal K v O p ((coeff (ModP O p) p (m ⊔ n + 1)) f) ^ p ^ (m ⊔ n + 1) *
      ModP.preVal K v O p ((coeff (ModP O p) p (m ⊔ n + 1)) g) ^ p ^ (m ⊔ n + 1)

Tactic:
rw [RingHom.map_mul] at hfg ⊢

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 : ℕ
hm : (coeff (ModP O p) p (m ⊔ n)) f ≠ 0
hn : (coeff (ModP O p) p (m ⊔ n)) g ≠ 0
hfg : (coeff (ModP O p) p (m ⊔ n + 1)) f * (coeff (ModP O p) p (m ⊔ n + 1)) g ≠ 0
⊢ ModP.preVal K v O p ((coeff (ModP O p) p (m ⊔ n + 1)) f * (coeff (ModP O p) p (m ⊔ n + 1)) g) ^ p ^ (m ⊔ n + 1) =
    ModP.preVal K v O p ((coeff (ModP O p) p (m ⊔ n + 1)) f) ^ p ^ (m ⊔ n + 1) *
      ModP.preVal K v O p ((coeff (ModP O p) p (m ⊔ n + 1)) g) ^ p ^ (m ⊔ n + 1)

Proof state:
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

Tactic:
obtain ⟨n, hn⟩ : ∃ n, coeff _ _ n g ≠ 0 := not_forall.1 fun h => hg <| Perfection.ext h

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 : ℕ
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

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
⊢ valAux K v O p (f * g) = valAux K v O p f * valAux K v O p g

Tactic:
by_cases hg : g = 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
hg : g = 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
hg : ¬g = 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 n : ℕ
hm : (coeff (ModP O p) p (m ⊔ n)) f ≠ 0
hn : (coeff (ModP O p) p (m ⊔ n)) g ≠ 0
hfg : (coeff (ModP O p) p (m ⊔ n + 1)) (f * g) ≠ 0
⊢ valAux K v O p (f * g) = valAux K v O p f * valAux K v O p g

Tactic:
rw [valAux_eq hv (coeff_add_ne_zero hm 1),
    valAux_eq hv (coeff_add_ne_zero hn 1), valAux_eq hv hfg]

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 : ℕ
hm : (coeff (ModP O p) p (m ⊔ n)) f ≠ 0
hn : (coeff (ModP O p) p (m ⊔ n)) g ≠ 0
hfg : (coeff (ModP O p) p (m ⊔ n + 1)) (f * g) ≠ 0
⊢ ModP.preVal K v O p ((coeff (ModP O p) p (m ⊔ n + 1)) (f * g)) ^ p ^ (m ⊔ n + 1) =
    ModP.preVal K v O p ((coeff (ModP O p) p (m ⊔ n + 1)) f) ^ p ^ (m ⊔ n + 1) *
      ModP.preVal K v O p ((coeff (ModP O p) p (m ⊔ n + 1)) g) ^ p ^ (m ⊔ n + 1)

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)) f ≠ 0

Tactic:
assumption

Result:
no goals

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 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

Tactic:
replace hn := coeff_ne_zero_of_le hn (le_max_right 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 : ℕ
hm : (coeff (ModP O p) p (m ⊔ n)) f ≠ 0
hn : (coeff (ModP O p) p (m ⊔ n)) g ≠ 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 n : ℕ
hm : (coeff (ModP O p) p (m ⊔ n)) f ≠ 0
hn : (coeff (ModP O p) p (m ⊔ n)) g ≠ 0
hfg : (coeff (ModP O p) p (m ⊔ n + 1)) f * (coeff (ModP O p) p (m ⊔ n + 1)) g ≠ 0
⊢ ModP.preVal K v O p ((coeff (ModP O p) p (m ⊔ n + 1)) f * (coeff (ModP O p) p (m ⊔ n + 1)) g) ^ p ^ (m ⊔ n + 1) =
    ModP.preVal K v O p ((coeff (ModP O p) p (m ⊔ n + 1)) f) ^ p ^ (m ⊔ n + 1) *
      ModP.preVal K v O p ((coeff (ModP O p) p (m ⊔ n + 1)) g) ^ p ^ (m ⊔ n + 1)

Tactic:
rw [ModP.preVal_mul hv hfg, mul_pow]

Result:
no goals

Proof state:
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)) g ≠ 0

Tactic:
assumption

Result:
no goals