-- Mathlib/Analysis/Normed/Ring/SeminormFromConst.lean
theorem seminormFromConst_isNonarchimedean (hna : IsNonarchimedean f) :
    IsNonarchimedean (seminormFromConst' hf1 hc hpm) := fun x y ↦ by
  apply le_of_tendsto_of_tendsto' (seminormFromConst_isLimit hf1 hc hpm (x + y))
    ((seminormFromConst_isLimit hf1 hc hpm x).max (seminormFromConst_isLimit hf1 hc hpm y))
  intro n
  have hmax : f ((x + y) * c ^ n) ≤ max (f (x * c ^ n)) (f (y * c ^ n))

Proof state:
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
hna : IsNonarchimedean ⇑f
x y : R
n : ℕ
⊢ f ((x + y) * c ^ n) ≤ f (x * c ^ n) ⊔ f (y * c ^ n)

Tactic:
simp only [add_mul, hna _ _]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
hna : IsNonarchimedean ⇑f
x y : R
n : ℕ
hmax : f ((x + y) * c ^ n) ≤ f (x * c ^ n) ∨ f ((x + y) * c ^ n) ≤ f (y * c ^ n)
⊢ f ((x + y) * c ^ n) / f c ^ n ≤ f (x * c ^ n) / f c ^ n ∨ f ((x + y) * c ^ n) / f c ^ n ≤ f (y * c ^ n) / f c ^ n

Tactic:
apply hmax.imp <;> intro <;> gcongr

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
hna : IsNonarchimedean ⇑f
x y : R
n : ℕ
⊢ seminormFromConst_seq c f (x + y) n ≤ seminormFromConst_seq c f x n ⊔ seminormFromConst_seq c f y n

Tactic:
have hmax : f ((x + y) * c ^ n) ≤ max (f (x * c ^ n)) (f (y * c ^ n)) := by
  simp only [add_mul, hna _ _]

Result:
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
hna : IsNonarchimedean ⇑f
x y : R
n : ℕ
hmax : f ((x + y) * c ^ n) ≤ f (x * c ^ n) ⊔ f (y * c ^ n)
⊢ seminormFromConst_seq c f (x + y) n ≤ seminormFromConst_seq c f x n ⊔ seminormFromConst_seq c f y n

Proof state:
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
hna : IsNonarchimedean ⇑f
x y : R
⊢ ∀ (x_1 : ℕ), seminormFromConst_seq c f (x + y) x_1 ≤ seminormFromConst_seq c f x x_1 ⊔ seminormFromConst_seq c f y x_1

Tactic:
intro n

Result:
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
hna : IsNonarchimedean ⇑f
x y : R
n : ℕ
⊢ seminormFromConst_seq c f (x + y) n ≤ seminormFromConst_seq c f x n ⊔ seminormFromConst_seq c f y n

Proof state:
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
hna : IsNonarchimedean ⇑f
x y : R
n : ℕ
hmax : f ((x + y) * c ^ n) ≤ f (x * c ^ n) ∨ f ((x + y) * c ^ n) ≤ f (y * c ^ n)
⊢ seminormFromConst_seq c f (x + y) n ≤ seminormFromConst_seq c f x n ∨
    seminormFromConst_seq c f (x + y) n ≤ seminormFromConst_seq c f y n

Tactic:
unfold seminormFromConst_seq

Result:
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
hna : IsNonarchimedean ⇑f
x y : R
n : ℕ
hmax : f ((x + y) * c ^ n) ≤ f (x * c ^ n) ∨ f ((x + y) * c ^ n) ≤ f (y * c ^ n)
⊢ f ((x + y) * c ^ n) / f c ^ n ≤ f (x * c ^ n) / f c ^ n ∨ f ((x + y) * c ^ n) / f c ^ n ≤ f (y * c ^ n) / f c ^ n

Proof state:
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
hna : IsNonarchimedean ⇑f
x y : R
n : ℕ
hmax : f ((x + y) * c ^ n) ≤ f (x * c ^ n) ⊔ f (y * c ^ n)
⊢ seminormFromConst_seq c f (x + y) n ≤ seminormFromConst_seq c f x n ⊔ seminormFromConst_seq c f y n

Tactic:
rw [le_max_iff] at hmax ⊢

Result:
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
hna : IsNonarchimedean ⇑f
x y : R
n : ℕ
hmax : f ((x + y) * c ^ n) ≤ f (x * c ^ n) ∨ f ((x + y) * c ^ n) ≤ f (y * c ^ n)
⊢ seminormFromConst_seq c f (x + y) n ≤ seminormFromConst_seq c f x n ∨
    seminormFromConst_seq c f (x + y) n ≤ seminormFromConst_seq c f y n

Proof state:
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
hna : IsNonarchimedean ⇑f
x y : R
⊢ seminormFromConst' hf1 hc hpm (x + y) ≤ seminormFromConst' hf1 hc hpm x ⊔ seminormFromConst' hf1 hc hpm y

Tactic:
apply le_of_tendsto_of_tendsto' (seminormFromConst_isLimit hf1 hc hpm (x + y))
  ((seminormFromConst_isLimit hf1 hc hpm x).max (seminormFromConst_isLimit hf1 hc hpm y))

Result:
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
hna : IsNonarchimedean ⇑f
x y : R
⊢ ∀ (x_1 : ℕ), seminormFromConst_seq c f (x + y) x_1 ≤ seminormFromConst_seq c f x x_1 ⊔ seminormFromConst_seq c f y x_1