Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: 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 (max ?v1✝ (max (stationaryPoint hf) ?v3))) ≠ padicNorm p (↑g (stationaryPoint hg))
hfgne :
  padicNorm p (↑f (max ?v1✝ (max (stationaryPoint hf) ?v3))) ≠ padicNorm p (↑g (max ?v1 (max ?v2 (stationaryPoint hg))))
⊢ padicNorm p (↑(f + g) (stationaryPoint hfg)) =
    max (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]

Goal state after:
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 (max ?v1✝ (max (stationaryPoint hf) ?v3✝))) ≠ padicNorm p (↑g (stationaryPoint hg))
hfgne :
  padicNorm p (↑f (max ?v1✝ (max (stationaryPoint hf) ?v3✝))) ≠
    padicNorm p (↑g (max ?v1✝¹ (max ?v2✝ (stationaryPoint hg))))
⊢ padicNorm p (↑(f + g) (max (stationaryPoint hfg) (max ?v2✝ ?v3✝))) =
    max (padicNorm p (↑f (max ?v1✝ (max (stationaryPoint hf) ?v3))))
      (padicNorm p (↑g (max ?v1 (max ?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 (max ?v1✝ (max (stationaryPoint hf) ?v3✝))) ≠ padicNorm p (↑g (stationaryPoint hg))
hfgne :
  padicNorm p (↑f (max ?v1✝ (max (stationaryPoint hf) ?v3✝))) ≠
    padicNorm p (↑g (max ?v1✝¹ (max ?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 (max ?v1✝ (max (stationaryPoint hf) ?v3✝))) ≠ padicNorm p (↑g (stationaryPoint hg))
hfgne :
  padicNorm p (↑f (max ?v1✝ (max (stationaryPoint hf) ?v3✝))) ≠
    padicNorm p (↑g (max ?v1✝¹ (max ?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 (max ?v1✝ (max (stationaryPoint hf) ?v3✝))) ≠ padicNorm p (↑g (stationaryPoint hg))
hfgne :
  padicNorm p (↑f (max ?v1✝ (max (stationaryPoint hf) ?v3✝))) ≠
    padicNorm p (↑g (max ?v1✝¹ (max ?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 (max ?v1✝ (max (stationaryPoint hf) ?v3✝))) ≠ padicNorm p (↑g (stationaryPoint hg))
hfgne :
  padicNorm p (↑f (max ?v1✝ (max (stationaryPoint hf) ?v3✝))) ≠
    padicNorm p (↑g (max ?v1✝¹ (max ?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 (max ?v1✝ (max (stationaryPoint hf) ?v3✝))) ≠ padicNorm p (↑g (stationaryPoint hg))
hfgne :
  padicNorm p (↑f (max ?v1✝ (max (stationaryPoint hf) ?v3✝))) ≠
    padicNorm p (↑g (max ?v1✝¹ (max ?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 (max ?v1✝ (max (stationaryPoint hf) ?v3✝))) ≠ padicNorm p (↑g (stationaryPoint hg))
hfgne :
  padicNorm p (↑f (max ?v1✝ (max (stationaryPoint hf) ?v3✝))) ≠
    padicNorm p (↑g (max ?v1✝¹ (max ?v2✝ (stationaryPoint hg))))
⊢ ℕ