-- Mathlib/NumberTheory/Padics/PadicNumbers.lean
theorem norm_mul (f g : PadicSeq p) : (f * g).norm = f.norm * g.norm

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : g ≈ 0
⊢ (f * g).norm = f.norm * g.norm

Tactic:
have hf : f * g ≈ 0 := mul_equiv_zero _ hg

Result:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf✝ : ¬f ≈ 0
hg : g ≈ 0
hf : f * g ≈ 0
⊢ (f * g).norm = f.norm * g.norm

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ (f * g).norm = f.norm * g.norm

Tactic:
unfold norm

Result:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ (if hf : f * g ≈ 0 then 0 else padicNorm p (↑(f * g) (stationaryPoint hf))) =
    (if hf : f ≈ 0 then 0 else padicNorm p (↑f (stationaryPoint hf))) *
      if hf : g ≈ 0 then 0 else padicNorm p (↑g (stationaryPoint hf))

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : ¬f * g ≈ 0
⊢ padicNorm p (↑(f * g) (stationaryPoint ⋯)) =
    padicNorm p (↑f (stationaryPoint ⋯)) * padicNorm p (↑g (stationaryPoint ⋯))

Tactic:
rw [lift_index_left_left hfg, lift_index_left hf, lift_index_right hg]

Result:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : ¬f * g ≈ 0
⊢ padicNorm p (↑(f * g) (stationaryPoint hfg ⊔ (?v2 ⊔ ?v3))) =
    padicNorm p (↑f (?v1 ⊔ (stationaryPoint hf ⊔ ?v3))) * padicNorm p (↑g (?v1 ⊔ (?v2 ⊔ stationaryPoint hg)))

case v1
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : ¬f * g ≈ 0
⊢ ℕ

case v2
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : ¬f * g ≈ 0
⊢ ℕ

case v1
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : ¬f * g ≈ 0
⊢ ℕ

case v3
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : ¬f * g ≈ 0
⊢ ℕ

case v2
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : ¬f * g ≈ 0
⊢ ℕ

case v3
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : ¬f * g ≈ 0
⊢ ℕ

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
⊢ (f * g).norm = f.norm * g.norm

Tactic:
exact if hf : f ≈ 0 then by
  have hg : f * g ≈ 0 := mul_equiv_zero' _ hf
  simp only [hf, hg, norm, dif_pos, zero_mul]
else
  if hg : g ≈ 0 then by
    have hf : f * g ≈ 0 := mul_equiv_zero _ hg
    simp only [hf, hg, norm, dif_pos, mul_zero]
  else by
    unfold norm
    have hfg := mul_not_equiv_zero hf hg
    simp only [hfg, hf, hg, dite_false]
    rw [lift_index_left_left hfg, lift_index_left hf, lift_index_right hg]
    apply padicNorm.mul

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf✝ : ¬f ≈ 0
hg : g ≈ 0
hf : f * g ≈ 0
⊢ (f * g).norm = f.norm * g.norm

Tactic:
simp only [hf, hg, norm, dif_pos, mul_zero]

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : ¬f * g ≈ 0
⊢ padicNorm p (↑(f * g) (stationaryPoint hfg ⊔ (?v2 ⊔ ?v3))) =
    padicNorm p (↑f (?v1 ⊔ (stationaryPoint hf ⊔ ?v3))) * padicNorm p (↑g (?v1 ⊔ (?v2 ⊔ stationaryPoint hg)))

case v1
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : ¬f * g ≈ 0
⊢ ℕ

case v2
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : ¬f * g ≈ 0
⊢ ℕ

case v1
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : ¬f * g ≈ 0
⊢ ℕ

case v3
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : ¬f * g ≈ 0
⊢ ℕ

case v2
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : ¬f * g ≈ 0
⊢ ℕ

case v3
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : ¬f * g ≈ 0
⊢ ℕ

Tactic:
apply padicNorm.mul

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : f ≈ 0
⊢ (f * g).norm = f.norm * g.norm

Tactic:
have hg : f * g ≈ 0 := mul_equiv_zero' _ hf

Result:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : f ≈ 0
hg : f * g ≈ 0
⊢ (f * g).norm = f.norm * g.norm

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : f ≈ 0
hg : f * g ≈ 0
⊢ (f * g).norm = f.norm * g.norm

Tactic:
simp only [hf, hg, norm, dif_pos, zero_mul]

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : ¬f * g ≈ 0
⊢ (if hf : f * g ≈ 0 then 0 else padicNorm p (↑(f * g) (stationaryPoint hf))) =
    (if hf : f ≈ 0 then 0 else padicNorm p (↑f (stationaryPoint hf))) *
      if hf : g ≈ 0 then 0 else padicNorm p (↑g (stationaryPoint hf))

Tactic:
simp only [hfg, hf, hg, dite_false]

Result:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : ¬f * g ≈ 0
⊢ padicNorm p (↑(f * g) (stationaryPoint ⋯)) =
    padicNorm p (↑f (stationaryPoint ⋯)) * padicNorm p (↑g (stationaryPoint ⋯))

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
⊢ (f * g).norm = f.norm * g.norm

Tactic:
classical
exact if hf : f ≈ 0 then by
  have hg : f * g ≈ 0 := mul_equiv_zero' _ hf
  simp only [hf, hg, norm, dif_pos, zero_mul]
else
  if hg : g ≈ 0 then by
    have hf : f * g ≈ 0 := mul_equiv_zero _ hg
    simp only [hf, hg, norm, dif_pos, mul_zero]
  else by
    unfold norm
    have hfg := mul_not_equiv_zero hf hg
    simp only [hfg, hf, hg, dite_false]
    rw [lift_index_left_left hfg, lift_index_left hf, lift_index_right hg]
    apply padicNorm.mul

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ (if hf : f * g ≈ 0 then 0 else padicNorm p (↑(f * g) (stationaryPoint hf))) =
    (if hf : f ≈ 0 then 0 else padicNorm p (↑f (stationaryPoint hf))) *
      if hf : g ≈ 0 then 0 else padicNorm p (↑g (stationaryPoint hf))

Tactic:
have hfg := mul_not_equiv_zero hf hg

Result:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : ¬f * g ≈ 0
⊢ (if hf : f * g ≈ 0 then 0 else padicNorm p (↑(f * g) (stationaryPoint hf))) =
    (if hf : f ≈ 0 then 0 else padicNorm p (↑f (stationaryPoint hf))) *
      if hf : g ≈ 0 then 0 else padicNorm p (↑g (stationaryPoint hf))