p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : f + g ≈ 0
this : 0 ≤ max (norm f) (norm g)
⊢ norm (f + g) ≤ max (norm f) (norm g)
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : f + g ≈ 0
⊢ norm (f + g) ≤ max (norm f) (norm g)
have : 0 ≤ max f.norm g.norm := le_max_of_le_left (norm_nonneg _)
no goals
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : f + g ≈ 0
this : 0 ≤ max (norm f) (norm g)
⊢ norm (f + g) ≤ max (norm f) (norm g)
simpa only [hfg, norm]
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : f ≈ 0
hfg' : f + g ≈ g
hcfg : norm (f + g) = norm g
⊢ norm (f + g) ≤ max (norm f) (norm g)
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : f ≈ 0
hfg' : f + g ≈ g
⊢ norm (f + g) ≤ max (norm f) (norm g)
have hcfg : (f + g).norm = g.norm := norm_equiv hfg'
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : f ≈ 0
hfg' : f + g ≈ g
hcfg : norm (f + g) = norm g
hcl : norm f = 0
⊢ norm (f + g) ≤ max (norm f) (norm g)
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : f ≈ 0
hfg' : f + g ≈ g
hcfg : norm (f + g) = norm g
⊢ norm (f + g) ≤ max (norm f) (norm g)
have hcl : f.norm = 0 := (norm_zero_iff f).2 hf
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : f ≈ 0
hfg' : f + g ≈ g
hcfg : norm (f + g) = norm g
hcl : norm f = 0
this : max (norm f) (norm g) = norm g
⊢ norm (f + g) ≤ max (norm f) (norm g)
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : f ≈ 0
hfg' : f + g ≈ g
hcfg : norm (f + g) = norm g
hcl : norm f = 0
⊢ norm (f + g) ≤ max (norm f) (norm g)
have : max f.norm g.norm = g.norm := by rw [hcl]; exact max_eq_right (norm_nonneg _)
no goals
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : f ≈ 0
hfg' : f + g ≈ g
hcfg : norm (f + g) = norm g
hcl : norm f = 0
this : max (norm f) (norm g) = norm g
⊢ norm (f + g) ≤ max (norm f) (norm g)
rw [this, hcfg]
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : LimZero (f - 0)
⊢ f + g ≈ g
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : f ≈ 0
⊢ f + g ≈ g
change LimZero (f - 0) at hf
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : LimZero (f - 0)
⊢ LimZero (f + g - g)
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : LimZero (f - 0)
⊢ f + g ≈ g
show LimZero (f + g - g)
no goals
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : LimZero (f - 0)
⊢ LimZero (f + g - g)
simpa only [sub_zero, add_sub_cancel] using hf
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : f ≈ 0
hfg' : f + g ≈ g
hcfg : norm (f + g) = norm g
hcl : norm f = 0
⊢ max 0 (norm g) = norm g
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : f ≈ 0
hfg' : f + g ≈ g
hcfg : norm (f + g) = norm g
hcl : norm f = 0
⊢ max (norm f) (norm g) = norm g
rw [hcl]
no goals
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : f ≈ 0
hfg' : f + g ≈ g
hcfg : norm (f + g) = norm g
hcl : norm f = 0
⊢ max 0 (norm g) = norm g
exact max_eq_right (norm_nonneg _)
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 : norm (f + g) = norm f
⊢ norm (f + g) ≤ max (norm f) (norm g)
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : g ≈ 0
hfg' : f + g ≈ f
⊢ norm (f + g) ≤ max (norm f) (norm g)
have hcfg : (f + g).norm = f.norm := norm_equiv hfg'
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 : norm (f + g) = norm f
hcl : norm g = 0
⊢ norm (f + g) ≤ max (norm f) (norm g)
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 : norm (f + g) = norm f
⊢ norm (f + g) ≤ max (norm f) (norm g)
have hcl : g.norm = 0 := (norm_zero_iff g).2 hg
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 : norm (f + g) = norm f
hcl : norm g = 0
this : max (norm f) (norm g) = norm f
⊢ norm (f + g) ≤ max (norm f) (norm g)
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 : norm (f + g) = norm f
hcl : norm g = 0
⊢ norm (f + g) ≤ max (norm f) (norm g)
have : max f.norm g.norm = f.norm := by rw [hcl]; exact max_eq_left (norm_nonneg _)
no goals
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 : norm (f + g) = norm f
hcl : norm g = 0
this : max (norm f) (norm g) = norm f
⊢ norm (f + g) ≤ max (norm f) (norm g)
rw [this, hcfg]
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : LimZero (g - 0)
⊢ f + g ≈ f
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : g ≈ 0
⊢ f + g ≈ f
change LimZero (g - 0) at hg
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : LimZero (g - 0)
⊢ LimZero (f + g - f)
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : LimZero (g - 0)
⊢ f + g ≈ f
show LimZero (f + g - f)
no goals
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : LimZero (g - 0)
⊢ LimZero (f + g - f)
simpa only [add_sub_cancel', sub_zero] using hg
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 : norm (f + g) = norm f
hcl : norm g = 0
⊢ max (norm f) 0 = norm f
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 : norm (f + g) = norm f
hcl : norm g = 0
⊢ max (norm f) (norm g) = norm f
rw [hcl]
no goals
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 : norm (f + g) = norm f
hcl : norm g = 0
⊢ max (norm f) 0 = norm f
exact max_eq_left (norm_nonneg _)