-- Mathlib/NumberTheory/Padics/PadicNumbers.lean
theorem add_eq_max_of_ne {f g : PadicSeq p} (hfgne : f.norm ≠ g.norm) :
    (f + g).norm = max f.norm g.norm

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

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
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfgne✝¹ : padicNorm p (↑f (stationaryPoint hf)) ≠ padicNorm p (↑g (stationaryPoint hg))
hfgne✝ : padicNorm p (↑f (?v1 ⊔ (stationaryPoint hf ⊔ ?v3))) ≠ padicNorm p (↑g (stationaryPoint hg))
hfgne : padicNorm p (↑f (?v1 ⊔ (stationaryPoint hf ⊔ ?v3))) ≠ padicNorm p (↑g (?v1 ⊔ (?v2 ⊔ stationaryPoint hg)))
⊢ 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
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfgne✝¹ : padicNorm p (↑f (stationaryPoint hf)) ≠ padicNorm p (↑g (stationaryPoint hg))
hfgne✝ : padicNorm p (↑f (?v1 ⊔ (stationaryPoint hf ⊔ ?v3))) ≠ padicNorm p (↑g (stationaryPoint hg))
hfgne : padicNorm p (↑f (?v1 ⊔ (stationaryPoint hf ⊔ ?v3))) ≠ padicNorm p (↑g (?v1 ⊔ (?v2 ⊔ stationaryPoint hg)))
⊢ ℕ

case v2
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfgne✝¹ : padicNorm p (↑f (stationaryPoint hf)) ≠ padicNorm p (↑g (stationaryPoint hg))
hfgne✝ : padicNorm p (↑f (?v1 ⊔ (stationaryPoint hf ⊔ ?v3))) ≠ padicNorm p (↑g (stationaryPoint hg))
hfgne : 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
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfgne✝¹ : padicNorm p (↑f (stationaryPoint hf)) ≠ padicNorm p (↑g (stationaryPoint hg))
hfgne✝ : padicNorm p (↑f (?v1 ⊔ (stationaryPoint hf ⊔ ?v3))) ≠ padicNorm p (↑g (stationaryPoint hg))
hfgne : padicNorm p (↑f (?v1 ⊔ (stationaryPoint hf ⊔ ?v3))) ≠ padicNorm p (↑g (?v1 ⊔ (?v2 ⊔ stationaryPoint hg)))
⊢ ℕ

case v3
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfgne✝¹ : padicNorm p (↑f (stationaryPoint hf)) ≠ padicNorm p (↑g (stationaryPoint hg))
hfgne✝ : padicNorm p (↑f (?v1 ⊔ (stationaryPoint hf ⊔ ?v3))) ≠ padicNorm p (↑g (stationaryPoint hg))
hfgne : padicNorm p (↑f (?v1 ⊔ (stationaryPoint hf ⊔ ?v3))) ≠ padicNorm p (↑g (?v1 ⊔ (?v2 ⊔ stationaryPoint hg)))
⊢ ℕ

case v2
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfgne✝¹ : padicNorm p (↑f (stationaryPoint hf)) ≠ padicNorm p (↑g (stationaryPoint hg))
hfgne✝ : padicNorm p (↑f (?v1 ⊔ (stationaryPoint hf ⊔ ?v3))) ≠ padicNorm p (↑g (stationaryPoint hg))
hfgne : padicNorm p (↑f (?v1 ⊔ (stationaryPoint hf ⊔ ?v3))) ≠ padicNorm p (↑g (?v1 ⊔ (?v2 ⊔ stationaryPoint hg)))
⊢ ℕ

case v3
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfgne✝¹ : padicNorm p (↑f (stationaryPoint hf)) ≠ padicNorm p (↑g (stationaryPoint hg))
hfgne✝ : padicNorm p (↑f (?v1 ⊔ (stationaryPoint hf ⊔ ?v3))) ≠ padicNorm p (↑g (stationaryPoint hg))
hfgne : padicNorm p (↑f (?v1 ⊔ (stationaryPoint hf ⊔ ?v3))) ≠ padicNorm p (↑g (?v1 ⊔ (?v2 ⊔ stationaryPoint hg)))
⊢ ℕ

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfgne : f.norm ≠ g.norm
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : g ≈ 0
this✝ : (g - 0).LimZero
this : f + g ≈ f
h1 : (f + g).norm = f.norm
h2 : g.norm = 0
⊢ (f + g).norm = f.norm ⊔ g.norm

Tactic:
rw [h1, h2, max_eq_left (norm_nonneg _)]

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfgne : f.norm ≠ g.norm
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : g ≈ 0
this : (g - 0).LimZero
⊢ LimZero (f + g - f)

Tactic:
simpa only [add_sub_cancel_left, sub_zero]

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfgne : f.norm ≠ g.norm
hfg : ¬f + g ≈ 0
hf : f ≈ 0
this✝ : (f - 0).LimZero
this : f + g ≈ g
h1 : (f + g).norm = g.norm
⊢ (f + g).norm = f.norm ⊔ g.norm

Tactic:
have h2 : f.norm = 0 := (norm_zero_iff _).2 hf

Result:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfgne : f.norm ≠ g.norm
hfg : ¬f + g ≈ 0
hf : f ≈ 0
this✝ : (f - 0).LimZero
this : f + g ≈ g
h1 : (f + g).norm = g.norm
h2 : f.norm = 0
⊢ (f + g).norm = f.norm ⊔ g.norm

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfgne : f.norm ≠ g.norm
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : g ≈ 0
this : (g - 0).LimZero
⊢ (f + g).norm = f.norm ⊔ g.norm

Tactic:
have : f + g ≈ f := show LimZero (f + g - f) by simpa only [add_sub_cancel_left, sub_zero]

Result:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfgne : f.norm ≠ g.norm
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : g ≈ 0
this✝ : (g - 0).LimZero
this : f + g ≈ f
⊢ (f + g).norm = f.norm ⊔ g.norm

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfgne : f.norm ≠ g.norm
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : g ≈ 0
this✝ : (g - 0).LimZero
this : f + g ≈ f
⊢ (f + g).norm = f.norm ⊔ g.norm

Tactic:
have h1 : (f + g).norm = f.norm := norm_equiv this

Result:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfgne : f.norm ≠ g.norm
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : g ≈ 0
this✝ : (g - 0).LimZero
this : f + g ≈ f
h1 : (f + g).norm = f.norm
⊢ (f + g).norm = f.norm ⊔ g.norm

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfgne : f.norm ≠ g.norm
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ (f + g).norm = f.norm ⊔ g.norm

Tactic:
unfold norm at hfgne ⊢

Result:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfgne :
  (if hf : f ≈ 0 then 0 else padicNorm p (↑f (stationaryPoint hf))) ≠
    if hf : g ≈ 0 then 0 else padicNorm p (↑g (stationaryPoint hf))
hfg : ¬f + g ≈ 0
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))