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

Tactic:
split_ifs at hfgne ⊢

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))
⊢ padicNorm p (↑(f + g) (stationaryPoint hfg)) =
    padicNorm p (↑f (stationaryPoint hf)) ⊔ padicNorm p (↑g (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
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

Tactic:
rw [h1, h2, max_eq_right (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
this✝ : (f - 0).LimZero
this : f + g ≈ g
⊢ (f + g).norm = f.norm ⊔ g.norm

Tactic:
have h1 : (f + g).norm = g.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
this✝ : (f - 0).LimZero
this : f + g ≈ g
h1 : (f + g).norm = g.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
this : (f - 0).LimZero
⊢ (f + g).norm = f.norm ⊔ g.norm

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

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
⊢ (f + g).norm = f.norm ⊔ g.norm

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfgne : f.norm ≠ g.norm
⊢ (f + g).norm = f.norm ⊔ g.norm

Tactic:
have hfg : ¬f + g ≈ 0 := mt norm_eq_of_add_equiv_zero hfgne

Result:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfgne : f.norm ≠ g.norm
hfg : ¬f + g ≈ 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
⊢ (f + g).norm = f.norm ⊔ g.norm

Tactic:
have : LimZero (g - 0) := hg

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
⊢ (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
⊢ (f + g).norm = f.norm ⊔ g.norm

Tactic:
have : LimZero (f - 0) := 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
⊢ (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
this : (f - 0).LimZero
⊢ LimZero (f + g - g)

Tactic:
simpa only [sub_zero, add_sub_cancel_right]

Result:
no goals

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 ⊔ (?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)))
⊢ ℕ

Tactic:
exact padicNorm.add_eq_max_of_ne hfgne

Result:
no goals