-- Mathlib/NumberTheory/Padics/PadicNumbers.lean
theorem norm_nonarchimedean (f g : PadicSeq p) : (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
hfg' : f + g ≈ g
hcfg : (f + g).norm = g.norm
⊢ (f + g).norm ≤ f.norm ⊔ g.norm

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

Result:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : f ≈ 0
hfg' : f + g ≈ g
hcfg : (f + g).norm = g.norm
hcl : f.norm = 0
⊢ (f + g).norm ≤ 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
hfg' : f + g ≈ f
hcfg : (f + g).norm = f.norm
hcl : g.norm = 0
this : f.norm ⊔ g.norm = f.norm
⊢ (f + g).norm ≤ f.norm ⊔ g.norm

Tactic:
rw [this, hcfg]

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
hfg' : f + g ≈ f
hcfg : (f + g).norm = f.norm
hcl : g.norm = 0
⊢ f.norm ⊔ 0 = f.norm

Tactic:
exact max_eq_left (norm_nonneg _)

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : f ≈ 0
⊢ f + g ≈ g

Tactic:
change LimZero (f - 0) at hf

Result:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : (f - 0).LimZero
⊢ f + g ≈ g

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : f ≈ 0
hfg' : f + g ≈ g
hcfg : (f + g).norm = g.norm
hcl : f.norm = 0
⊢ (f + g).norm ≤ f.norm ⊔ g.norm

Tactic:
have : max f.norm g.norm = g.norm := by rw [hcl]; exact max_eq_right (norm_nonneg _)

Result:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : f ≈ 0
hfg' : f + g ≈ g
hcfg : (f + g).norm = g.norm
hcl : f.norm = 0
this : f.norm ⊔ g.norm = g.norm
⊢ (f + g).norm ≤ f.norm ⊔ g.norm

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

Tactic:
have hcfg : (f + g).norm = g.norm := norm_equiv hfg'

Result:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : f ≈ 0
hfg' : f + g ≈ g
hcfg : (f + g).norm = g.norm
⊢ (f + g).norm ≤ f.norm ⊔ g.norm

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : f ≈ 0
hfg' : f + g ≈ g
hcfg : (f + g).norm = g.norm
hcl : f.norm = 0
this : f.norm ⊔ g.norm = g.norm
⊢ (f + g).norm ≤ f.norm ⊔ g.norm

Tactic:
rw [this, hcfg]

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : f + g ≈ 0
this : 0 ≤ f.norm ⊔ g.norm
⊢ (f + g).norm ≤ f.norm ⊔ g.norm

Tactic:
simpa only [hfg, norm]

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
hfg' : f + g ≈ f
hcfg : (f + g).norm = f.norm
hcl : g.norm = 0
⊢ f.norm ⊔ g.norm = f.norm

Tactic:
rw [hcl]

Result:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : g ≈ 0
hfg' : f + g ≈ f
hcfg : (f + g).norm = f.norm
hcl : g.norm = 0
⊢ f.norm ⊔ 0 = f.norm

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

Tactic:
have : max f.norm g.norm = f.norm := by rw [hcl]; exact max_eq_left (norm_nonneg _)

Result:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : g ≈ 0
hfg' : f + g ≈ f
hcfg : (f + g).norm = f.norm
hcl : g.norm = 0
this : f.norm ⊔ g.norm = f.norm
⊢ (f + g).norm ≤ 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).LimZero
⊢ f + g ≈ f

Tactic:
show LimZero (f + g - f)

Result:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : (g - 0).LimZero
⊢ LimZero (f + g - f)

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : f + g ≈ 0
⊢ (f + g).norm ≤ f.norm ⊔ g.norm

Tactic:
have : 0 ≤ max f.norm g.norm := le_max_of_le_left (norm_nonneg _)

Result:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : f + g ≈ 0
this : 0 ≤ f.norm ⊔ g.norm
⊢ (f + g).norm ≤ f.norm ⊔ g.norm

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

Tactic:
exact max_eq_right (norm_nonneg _)

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
hfg' : f + g ≈ f
hcfg : (f + g).norm = f.norm
⊢ (f + g).norm ≤ f.norm ⊔ g.norm

Tactic:
have hcl : g.norm = 0 := (norm_zero_iff g).2 hg

Result:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : g ≈ 0
hfg' : f + g ≈ f
hcfg : (f + g).norm = f.norm
hcl : g.norm = 0
⊢ (f + g).norm ≤ f.norm ⊔ g.norm

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

Tactic:
show LimZero (f + g - g)

Result:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : (f - 0).LimZero
⊢ LimZero (f + g - g)

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

Tactic:
simpa only [sub_zero, add_sub_cancel_right] using hf

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).LimZero
⊢ LimZero (f + g - f)

Tactic:
simpa only [add_sub_cancel_left, sub_zero] using hg

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
⊢ f + g ≈ f

Tactic:
change LimZero (g - 0) at hg

Result:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : (g - 0).LimZero
⊢ f + g ≈ f

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

Tactic:
rw [hcl]

Result:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : f ≈ 0
hfg' : f + g ≈ g
hcfg : (f + g).norm = g.norm
hcl : f.norm = 0
⊢ 0 ⊔ g.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
hfg' : f + g ≈ f
⊢ (f + g).norm ≤ f.norm ⊔ g.norm

Tactic:
have hcfg : (f + g).norm = f.norm := norm_equiv hfg'

Result:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : g ≈ 0
hfg' : f + g ≈ f
hcfg : (f + g).norm = f.norm
⊢ (f + g).norm ≤ f.norm ⊔ g.norm