F : Type ?u.32745
R : Type u_1
S : Type ?u.32751
x y : R
r : ℝ
inst✝ : Ring R
p : RingSeminorm R
hp : ↑p 1 ≤ 1
h : p ≠ 0
⊢ ↑p 1 = 1
F : Type ?u.32745
R : Type u_1
S : Type ?u.32751
x y : R
r : ℝ
inst✝ : Ring R
p : RingSeminorm R
hp : ↑p 1 ≤ 1
⊢ ↑p 1 = 1 ↔ p ≠ 0
refine'
  ⟨fun h =>
    ne_zero_iff.mpr
      ⟨1, by
        rw [h]
        exact one_ne_zero⟩,
    fun h => ?_⟩
case inl
F : Type ?u.32745
R : Type u_1
S : Type ?u.32751
x y : R
r : ℝ
inst✝ : Ring R
p : RingSeminorm R
hp : ↑p 1 ≤ 1
h : p ≠ 0
hp0 : ↑p 1 = 0
⊢ ↑p 1 = 1

case inr
F : Type ?u.32745
R : Type u_1
S : Type ?u.32751
x y : R
r : ℝ
inst✝ : Ring R
p : RingSeminorm R
hp : ↑p 1 ≤ 1
h : p ≠ 0
hp0 : 0 < ↑p 1
⊢ ↑p 1 = 1
F : Type ?u.32745
R : Type u_1
S : Type ?u.32751
x y : R
r : ℝ
inst✝ : Ring R
p : RingSeminorm R
hp : ↑p 1 ≤ 1
h : p ≠ 0
⊢ ↑p 1 = 1
obtain hp0 | hp0 := (map_nonneg p (1 : R)).eq_or_gt
F : Type ?u.32745
R : Type u_1
S : Type ?u.32751
x y : R
r : ℝ
inst✝ : Ring R
p : RingSeminorm R
hp : ↑p 1 ≤ 1
h : ↑p 1 = 1
⊢ 1 ≠ 0
F : Type ?u.32745
R : Type u_1
S : Type ?u.32751
x y : R
r : ℝ
inst✝ : Ring R
p : RingSeminorm R
hp : ↑p 1 ≤ 1
h : ↑p 1 = 1
⊢ ↑p 1 ≠ 0
rw [h]
no goals
F : Type ?u.32745
R : Type u_1
S : Type ?u.32751
x y : R
r : ℝ
inst✝ : Ring R
p : RingSeminorm R
hp : ↑p 1 ≤ 1
h : ↑p 1 = 1
⊢ 1 ≠ 0
exact one_ne_zero
case inl.h
F : Type ?u.32745
R : Type u_1
S : Type ?u.32751
x y : R
r : ℝ
inst✝ : Ring R
p : RingSeminorm R
hp : ↑p 1 ≤ 1
h : p ≠ 0
hp0 : ↑p 1 = 0
⊢ False
case inl
F : Type ?u.32745
R : Type u_1
S : Type ?u.32751
x y : R
r : ℝ
inst✝ : Ring R
p : RingSeminorm R
hp : ↑p 1 ≤ 1
h : p ≠ 0
hp0 : ↑p 1 = 0
⊢ ↑p 1 = 1
exfalso
case inl.h
F : Type ?u.32745
R : Type u_1
S : Type ?u.32751
x✝ y : R
r : ℝ
inst✝ : Ring R
p : RingSeminorm R
hp : ↑p 1 ≤ 1
h : p ≠ 0
hp0 : ↑p 1 = 0
x : R
⊢ ↑p x ≤ 0
case inl.h
F : Type ?u.32745
R : Type u_1
S : Type ?u.32751
x y : R
r : ℝ
inst✝ : Ring R
p : RingSeminorm R
hp : ↑p 1 ≤ 1
h : p ≠ 0
hp0 : ↑p 1 = 0
⊢ False
refine h (ext fun x => (map_nonneg _ _).antisymm' ?_)
no goals
case inl.h
F : Type ?u.32745
R : Type u_1
S : Type ?u.32751
x✝ y : R
r : ℝ
inst✝ : Ring R
p : RingSeminorm R
hp : ↑p 1 ≤ 1
h : p ≠ 0
hp0 : ↑p 1 = 0
x : R
⊢ ↑p x ≤ 0
simpa only [hp0, mul_one, MulZeroClass.mul_zero] using map_mul_le_mul p x 1
case inr
F : Type ?u.32745
R : Type u_1
S : Type ?u.32751
x y : R
r : ℝ
inst✝ : Ring R
p : RingSeminorm R
hp : ↑p 1 ≤ 1
h : p ≠ 0
hp0 : 0 < ↑p 1
⊢ ↑p 1 ≤ ↑p 1 * ↑p 1
case inr
F : Type ?u.32745
R : Type u_1
S : Type ?u.32751
x y : R
r : ℝ
inst✝ : Ring R
p : RingSeminorm R
hp : ↑p 1 ≤ 1
h : p ≠ 0
hp0 : 0 < ↑p 1
⊢ ↑p 1 = 1
refine' hp.antisymm ((le_mul_iff_one_le_left hp0).1 _)
no goals
case inr
F : Type ?u.32745
R : Type u_1
S : Type ?u.32751
x y : R
r : ℝ
inst✝ : Ring R
p : RingSeminorm R
hp : ↑p 1 ≤ 1
h : p ≠ 0
hp0 : 0 < ↑p 1
⊢ ↑p 1 ≤ ↑p 1 * ↑p 1
simpa only [one_mul] using map_mul_le_mul p (1 : R) _