[GOAL]
F : Type u_1
R : Type u_2
S : Type u_3
x y : R
r : ℝ
inst✝ : NonUnitalRing R
f g : RingSeminorm R
h : (fun f => f.toFun) f = (fun f => f.toFun) g
⊢ f = g
[PROOFSTEP]
cases f
[GOAL]
case mk
F : Type u_1
R : Type u_2
S : Type u_3
x y : R
r : ℝ
inst✝ : NonUnitalRing R
g : RingSeminorm R
toAddGroupSeminorm✝ : AddGroupSeminorm R
mul_le'✝ :
  ∀ (x y : R),
    AddGroupSeminorm.toFun toAddGroupSeminorm✝ (x * y) ≤
      AddGroupSeminorm.toFun toAddGroupSeminorm✝ x * AddGroupSeminorm.toFun toAddGroupSeminorm✝ y
h : (fun f => f.toFun) { toAddGroupSeminorm := toAddGroupSeminorm✝, mul_le' := mul_le'✝ } = (fun f => f.toFun) g
⊢ { toAddGroupSeminorm := toAddGroupSeminorm✝, mul_le' := mul_le'✝ } = g
[PROOFSTEP]
cases g
[GOAL]
case mk.mk
F : Type u_1
R : Type u_2
S : Type u_3
x y : R
r : ℝ
inst✝ : NonUnitalRing R
toAddGroupSeminorm✝¹ : AddGroupSeminorm R
mul_le'✝¹ :
  ∀ (x y : R),
    AddGroupSeminorm.toFun toAddGroupSeminorm✝¹ (x * y) ≤
      AddGroupSeminorm.toFun toAddGroupSeminorm✝¹ x * AddGroupSeminorm.toFun toAddGroupSeminorm✝¹ y
toAddGroupSeminorm✝ : AddGroupSeminorm R
mul_le'✝ :
  ∀ (x y : R),
    AddGroupSeminorm.toFun toAddGroupSeminorm✝ (x * y) ≤
      AddGroupSeminorm.toFun toAddGroupSeminorm✝ x * AddGroupSeminorm.toFun toAddGroupSeminorm✝ y
h :
  (fun f => f.toFun) { toAddGroupSeminorm := toAddGroupSeminorm✝¹, mul_le' := mul_le'✝¹ } =
    (fun f => f.toFun) { toAddGroupSeminorm := toAddGroupSeminorm✝, mul_le' := mul_le'✝ }
⊢ { toAddGroupSeminorm := toAddGroupSeminorm✝¹, mul_le' := mul_le'✝¹ } =
    { toAddGroupSeminorm := toAddGroupSeminorm✝, mul_le' := mul_le'✝ }
[PROOFSTEP]
congr
[GOAL]
case mk.mk.e_toAddGroupSeminorm
F : Type u_1
R : Type u_2
S : Type u_3
x y : R
r : ℝ
inst✝ : NonUnitalRing R
toAddGroupSeminorm✝¹ : AddGroupSeminorm R
mul_le'✝¹ :
  ∀ (x y : R),
    AddGroupSeminorm.toFun toAddGroupSeminorm✝¹ (x * y) ≤
      AddGroupSeminorm.toFun toAddGroupSeminorm✝¹ x * AddGroupSeminorm.toFun toAddGroupSeminorm✝¹ y
toAddGroupSeminorm✝ : AddGroupSeminorm R
mul_le'✝ :
  ∀ (x y : R),
    AddGroupSeminorm.toFun toAddGroupSeminorm✝ (x * y) ≤
      AddGroupSeminorm.toFun toAddGroupSeminorm✝ x * AddGroupSeminorm.toFun toAddGroupSeminorm✝ y
h :
  (fun f => f.toFun) { toAddGroupSeminorm := toAddGroupSeminorm✝¹, mul_le' := mul_le'✝¹ } =
    (fun f => f.toFun) { toAddGroupSeminorm := toAddGroupSeminorm✝, mul_le' := mul_le'✝ }
⊢ toAddGroupSeminorm✝¹ = toAddGroupSeminorm✝
[PROOFSTEP]
ext x
[GOAL]
case mk.mk.e_toAddGroupSeminorm.a
F : Type u_1
R : Type u_2
S : Type u_3
x✝ y : R
r : ℝ
inst✝ : NonUnitalRing R
toAddGroupSeminorm✝¹ : AddGroupSeminorm R
mul_le'✝¹ :
  ∀ (x y : R),
    AddGroupSeminorm.toFun toAddGroupSeminorm✝¹ (x * y) ≤
      AddGroupSeminorm.toFun toAddGroupSeminorm✝¹ x * AddGroupSeminorm.toFun toAddGroupSeminorm✝¹ y
toAddGroupSeminorm✝ : AddGroupSeminorm R
mul_le'✝ :
  ∀ (x y : R),
    AddGroupSeminorm.toFun toAddGroupSeminorm✝ (x * y) ≤
      AddGroupSeminorm.toFun toAddGroupSeminorm✝ x * AddGroupSeminorm.toFun toAddGroupSeminorm✝ y
h :
  (fun f => f.toFun) { toAddGroupSeminorm := toAddGroupSeminorm✝¹, mul_le' := mul_le'✝¹ } =
    (fun f => f.toFun) { toAddGroupSeminorm := toAddGroupSeminorm✝, mul_le' := mul_le'✝ }
x : R
⊢ ↑toAddGroupSeminorm✝¹ x = ↑toAddGroupSeminorm✝ x
[PROOFSTEP]
exact congr_fun h x
[GOAL]
F : Type u_1
R : Type u_2
S : Type u_3
x y : R
r : ℝ
inst✝ : NonUnitalRing R
p : RingSeminorm R
⊢ p ≠ 0 ↔ ∃ x, ↑p x ≠ 0
[PROOFSTEP]
simp [eq_zero_iff]
[GOAL]
F : Type u_1
R : Type u_2
S : Type u_3
x✝ y✝ : R
r : ℝ
inst✝¹ : NonUnitalRing R
inst✝ : DecidableEq R
src✝ : AddGroupSeminorm R := 1
x y : R
⊢ AddGroupSeminorm.toFun
      { toFun := src✝.toFun, map_zero' := (_ : AddGroupSeminorm.toFun src✝ 0 = 0),
        add_le' :=
          (_ :
            ∀ (r s : R),
              AddGroupSeminorm.toFun src✝ (r + s) ≤ AddGroupSeminorm.toFun src✝ r + AddGroupSeminorm.toFun src✝ s),
        neg' := (_ : ∀ (r : R), AddGroupSeminorm.toFun src✝ (-r) = AddGroupSeminorm.toFun src✝ r) }
      (x * y) ≤
    AddGroupSeminorm.toFun
        { toFun := src✝.toFun, map_zero' := (_ : AddGroupSeminorm.toFun src✝ 0 = 0),
          add_le' :=
            (_ :
              ∀ (r s : R),
                AddGroupSeminorm.toFun src✝ (r + s) ≤ AddGroupSeminorm.toFun src✝ r + AddGroupSeminorm.toFun src✝ s),
          neg' := (_ : ∀ (r : R), AddGroupSeminorm.toFun src✝ (-r) = AddGroupSeminorm.toFun src✝ r) }
        x *
      AddGroupSeminorm.toFun
        { toFun := src✝.toFun, map_zero' := (_ : AddGroupSeminorm.toFun src✝ 0 = 0),
          add_le' :=
            (_ :
              ∀ (r s : R),
                AddGroupSeminorm.toFun src✝ (r + s) ≤ AddGroupSeminorm.toFun src✝ r + AddGroupSeminorm.toFun src✝ s),
          neg' := (_ : ∀ (r : R), AddGroupSeminorm.toFun src✝ (-r) = AddGroupSeminorm.toFun src✝ r) }
        y
[PROOFSTEP]
by_cases h : x * y = 0
[GOAL]
case pos
F : Type u_1
R : Type u_2
S : Type u_3
x✝ y✝ : R
r : ℝ
inst✝¹ : NonUnitalRing R
inst✝ : DecidableEq R
src✝ : AddGroupSeminorm R := 1
x y : R
h : x * y = 0
⊢ AddGroupSeminorm.toFun
      { toFun := src✝.toFun, map_zero' := (_ : AddGroupSeminorm.toFun src✝ 0 = 0),
        add_le' :=
          (_ :
            ∀ (r s : R),
              AddGroupSeminorm.toFun src✝ (r + s) ≤ AddGroupSeminorm.toFun src✝ r + AddGroupSeminorm.toFun src✝ s),
        neg' := (_ : ∀ (r : R), AddGroupSeminorm.toFun src✝ (-r) = AddGroupSeminorm.toFun src✝ r) }
      (x * y) ≤
    AddGroupSeminorm.toFun
        { toFun := src✝.toFun, map_zero' := (_ : AddGroupSeminorm.toFun src✝ 0 = 0),
          add_le' :=
            (_ :
              ∀ (r s : R),
                AddGroupSeminorm.toFun src✝ (r + s) ≤ AddGroupSeminorm.toFun src✝ r + AddGroupSeminorm.toFun src✝ s),
          neg' := (_ : ∀ (r : R), AddGroupSeminorm.toFun src✝ (-r) = AddGroupSeminorm.toFun src✝ r) }
        x *
      AddGroupSeminorm.toFun
        { toFun := src✝.toFun, map_zero' := (_ : AddGroupSeminorm.toFun src✝ 0 = 0),
          add_le' :=
            (_ :
              ∀ (r s : R),
                AddGroupSeminorm.toFun src✝ (r + s) ≤ AddGroupSeminorm.toFun src✝ r + AddGroupSeminorm.toFun src✝ s),
          neg' := (_ : ∀ (r : R), AddGroupSeminorm.toFun src✝ (-r) = AddGroupSeminorm.toFun src✝ r) }
        y
[PROOFSTEP]
refine' (if_pos h).trans_le (mul_nonneg _ _)
[GOAL]
case pos.refine'_1
F : Type u_1
R : Type u_2
S : Type u_3
x✝ y✝ : R
r : ℝ
inst✝¹ : NonUnitalRing R
inst✝ : DecidableEq R
src✝ : AddGroupSeminorm R := 1
x y : R
h : x * y = 0
⊢ 0 ≤
    AddGroupSeminorm.toFun
      { toFun := src✝.toFun, map_zero' := (_ : AddGroupSeminorm.toFun src✝ 0 = 0),
        add_le' :=
          (_ :
            ∀ (r s : R),
              AddGroupSeminorm.toFun src✝ (r + s) ≤ AddGroupSeminorm.toFun src✝ r + AddGroupSeminorm.toFun src✝ s),
        neg' := (_ : ∀ (r : R), AddGroupSeminorm.toFun src✝ (-r) = AddGroupSeminorm.toFun src✝ r) }
      x
[PROOFSTEP]
change _ ≤ ite _ _ _
[GOAL]
case pos.refine'_1
F : Type u_1
R : Type u_2
S : Type u_3
x✝ y✝ : R
r : ℝ
inst✝¹ : NonUnitalRing R
inst✝ : DecidableEq R
src✝ : AddGroupSeminorm R := 1
x y : R
h : x * y = 0
⊢ 0 ≤ if x = 0 then 0 else 1
[PROOFSTEP]
split_ifs
[GOAL]
case pos
F : Type u_1
R : Type u_2
S : Type u_3
x✝ y✝ : R
r : ℝ
inst✝¹ : NonUnitalRing R
inst✝ : DecidableEq R
src✝ : AddGroupSeminorm R := 1
x y : R
h : x * y = 0
h✝ : x = 0
⊢ 0 ≤ 0
case neg
F : Type u_1
R : Type u_2
S : Type u_3
x✝ y✝ : R
r : ℝ
inst✝¹ : NonUnitalRing R
inst✝ : DecidableEq R
src✝ : AddGroupSeminorm R := 1
x y : R
h : x * y = 0
h✝ : ¬x = 0
⊢ 0 ≤ 1
[PROOFSTEP]
exacts [le_rfl, zero_le_one]
[GOAL]
case pos.refine'_2
F : Type u_1
R : Type u_2
S : Type u_3
x✝ y✝ : R
r : ℝ
inst✝¹ : NonUnitalRing R
inst✝ : DecidableEq R
src✝ : AddGroupSeminorm R := 1
x y : R
h : x * y = 0
⊢ 0 ≤
    AddGroupSeminorm.toFun
      { toFun := src✝.toFun, map_zero' := (_ : AddGroupSeminorm.toFun src✝ 0 = 0),
        add_le' :=
          (_ :
            ∀ (r s : R),
              AddGroupSeminorm.toFun src✝ (r + s) ≤ AddGroupSeminorm.toFun src✝ r + AddGroupSeminorm.toFun src✝ s),
        neg' := (_ : ∀ (r : R), AddGroupSeminorm.toFun src✝ (-r) = AddGroupSeminorm.toFun src✝ r) }
      y
[PROOFSTEP]
change _ ≤ ite _ _ _
[GOAL]
case pos.refine'_2
F : Type u_1
R : Type u_2
S : Type u_3
x✝ y✝ : R
r : ℝ
inst✝¹ : NonUnitalRing R
inst✝ : DecidableEq R
src✝ : AddGroupSeminorm R := 1
x y : R
h : x * y = 0
⊢ 0 ≤ if y = 0 then 0 else 1
[PROOFSTEP]
split_ifs
[GOAL]
case pos
F : Type u_1
R : Type u_2
S : Type u_3
x✝ y✝ : R
r : ℝ
inst✝¹ : NonUnitalRing R
inst✝ : DecidableEq R
src✝ : AddGroupSeminorm R := 1
x y : R
h : x * y = 0
h✝ : y = 0
⊢ 0 ≤ 0
case neg
F : Type u_1
R : Type u_2
S : Type u_3
x✝ y✝ : R
r : ℝ
inst✝¹ : NonUnitalRing R
inst✝ : DecidableEq R
src✝ : AddGroupSeminorm R := 1
x y : R
h : x * y = 0
h✝ : ¬y = 0
⊢ 0 ≤ 1
[PROOFSTEP]
exacts [le_rfl, zero_le_one]
[GOAL]
case neg
F : Type u_1
R : Type u_2
S : Type u_3
x✝ y✝ : R
r : ℝ
inst✝¹ : NonUnitalRing R
inst✝ : DecidableEq R
src✝ : AddGroupSeminorm R := 1
x y : R
h : ¬x * y = 0
⊢ AddGroupSeminorm.toFun
      { toFun := src✝.toFun, map_zero' := (_ : AddGroupSeminorm.toFun src✝ 0 = 0),
        add_le' :=
          (_ :
            ∀ (r s : R),
              AddGroupSeminorm.toFun src✝ (r + s) ≤ AddGroupSeminorm.toFun src✝ r + AddGroupSeminorm.toFun src✝ s),
        neg' := (_ : ∀ (r : R), AddGroupSeminorm.toFun src✝ (-r) = AddGroupSeminorm.toFun src✝ r) }
      (x * y) ≤
    AddGroupSeminorm.toFun
        { toFun := src✝.toFun, map_zero' := (_ : AddGroupSeminorm.toFun src✝ 0 = 0),
          add_le' :=
            (_ :
              ∀ (r s : R),
                AddGroupSeminorm.toFun src✝ (r + s) ≤ AddGroupSeminorm.toFun src✝ r + AddGroupSeminorm.toFun src✝ s),
          neg' := (_ : ∀ (r : R), AddGroupSeminorm.toFun src✝ (-r) = AddGroupSeminorm.toFun src✝ r) }
        x *
      AddGroupSeminorm.toFun
        { toFun := src✝.toFun, map_zero' := (_ : AddGroupSeminorm.toFun src✝ 0 = 0),
          add_le' :=
            (_ :
              ∀ (r s : R),
                AddGroupSeminorm.toFun src✝ (r + s) ≤ AddGroupSeminorm.toFun src✝ r + AddGroupSeminorm.toFun src✝ s),
          neg' := (_ : ∀ (r : R), AddGroupSeminorm.toFun src✝ (-r) = AddGroupSeminorm.toFun src✝ r) }
        y
[PROOFSTEP]
change ite _ _ _ ≤ ite _ _ _ * ite _ _ _
[GOAL]
case neg
F : Type u_1
R : Type u_2
S : Type u_3
x✝ y✝ : R
r : ℝ
inst✝¹ : NonUnitalRing R
inst✝ : DecidableEq R
src✝ : AddGroupSeminorm R := 1
x y : R
h : ¬x * y = 0
⊢ (if x * y = 0 then 0 else 1) ≤ (if x = 0 then 0 else 1) * if y = 0 then 0 else 1
[PROOFSTEP]
simp only [if_false, h, left_ne_zero_of_mul h, right_ne_zero_of_mul h, mul_one, le_refl]
[GOAL]
F : Type u_1
R : Type u_2
S : Type u_3
x y : R
r : ℝ
inst✝ : Ring R
p : RingSeminorm R
hp : ↑p 1 ≤ 1
⊢ ↑p 1 = 1 ↔ p ≠ 0
[PROOFSTEP]
refine'
  ⟨fun h =>
    ne_zero_iff.mpr
      ⟨1, by
        rw [h]
        exact one_ne_zero⟩,
    fun h => ?_⟩
[GOAL]
F : Type u_1
R : Type u_2
S : Type u_3
x y : R
r : ℝ
inst✝ : Ring R
p : RingSeminorm R
hp : ↑p 1 ≤ 1
h : ↑p 1 = 1
⊢ ↑p 1 ≠ 0
[PROOFSTEP]
rw [h]
[GOAL]
F : Type u_1
R : Type u_2
S : Type u_3
x y : R
r : ℝ
inst✝ : Ring R
p : RingSeminorm R
hp : ↑p 1 ≤ 1
h : ↑p 1 = 1
⊢ 1 ≠ 0
[PROOFSTEP]
exact one_ne_zero
[GOAL]
F : Type u_1
R : Type u_2
S : Type u_3
x y : R
r : ℝ
inst✝ : Ring R
p : RingSeminorm R
hp : ↑p 1 ≤ 1
h : p ≠ 0
⊢ ↑p 1 = 1
[PROOFSTEP]
obtain hp0 | hp0 := (map_nonneg p (1 : R)).eq_or_gt
[GOAL]
case inl
F : Type u_1
R : Type u_2
S : Type u_3
x y : R
r : ℝ
inst✝ : Ring R
p : RingSeminorm R
hp : ↑p 1 ≤ 1
h : p ≠ 0
hp0 : ↑p 1 = 0
⊢ ↑p 1 = 1
[PROOFSTEP]
exfalso
[GOAL]
case inl.h
F : Type u_1
R : Type u_2
S : Type u_3
x y : R
r : ℝ
inst✝ : Ring R
p : RingSeminorm R
hp : ↑p 1 ≤ 1
h : p ≠ 0
hp0 : ↑p 1 = 0
⊢ False
[PROOFSTEP]
refine h (ext fun x => (map_nonneg _ _).antisymm' ?_)
[GOAL]
case inl.h
F : Type u_1
R : Type u_2
S : Type u_3
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
[PROOFSTEP]
simpa only [hp0, mul_one, mul_zero] using map_mul_le_mul p x 1
[GOAL]
case inr
F : Type u_1
R : Type u_2
S : Type u_3
x y : R
r : ℝ
inst✝ : Ring R
p : RingSeminorm R
hp : ↑p 1 ≤ 1
h : p ≠ 0
hp0 : 0 < ↑p 1
⊢ ↑p 1 = 1
[PROOFSTEP]
refine' hp.antisymm ((le_mul_iff_one_le_left hp0).1 _)
[GOAL]
case inr
F : Type u_1
R : Type u_2
S : Type u_3
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
[PROOFSTEP]
simpa only [one_mul] using map_mul_le_mul p (1 : R) _
[GOAL]
F : Type u_1
R : Type u_2
S : Type u_3
x y : R
r : ℝ
inst✝ : NonUnitalRing R
f g : RingNorm R
h : (fun f => f.toFun) f = (fun f => f.toFun) g
⊢ f = g
[PROOFSTEP]
cases f
[GOAL]
case mk
F : Type u_1
R : Type u_2
S : Type u_3
x y : R
r : ℝ
inst✝ : NonUnitalRing R
g : RingNorm R
toRingSeminorm✝ : RingSeminorm R
eq_zero_of_map_eq_zero'✝ : ∀ (x : R), AddGroupSeminorm.toFun toRingSeminorm✝.toAddGroupSeminorm x = 0 → x = 0
h :
  (fun f => f.toFun) { toRingSeminorm := toRingSeminorm✝, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'✝ } =
    (fun f => f.toFun) g
⊢ { toRingSeminorm := toRingSeminorm✝, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'✝ } = g
[PROOFSTEP]
cases g
[GOAL]
case mk.mk
F : Type u_1
R : Type u_2
S : Type u_3
x y : R
r : ℝ
inst✝ : NonUnitalRing R
toRingSeminorm✝¹ : RingSeminorm R
eq_zero_of_map_eq_zero'✝¹ : ∀ (x : R), AddGroupSeminorm.toFun toRingSeminorm✝¹.toAddGroupSeminorm x = 0 → x = 0
toRingSeminorm✝ : RingSeminorm R
eq_zero_of_map_eq_zero'✝ : ∀ (x : R), AddGroupSeminorm.toFun toRingSeminorm✝.toAddGroupSeminorm x = 0 → x = 0
h :
  (fun f => f.toFun) { toRingSeminorm := toRingSeminorm✝¹, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'✝¹ } =
    (fun f => f.toFun) { toRingSeminorm := toRingSeminorm✝, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'✝ }
⊢ { toRingSeminorm := toRingSeminorm✝¹, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'✝¹ } =
    { toRingSeminorm := toRingSeminorm✝, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'✝ }
[PROOFSTEP]
congr
[GOAL]
case mk.mk.e_toRingSeminorm
F : Type u_1
R : Type u_2
S : Type u_3
x y : R
r : ℝ
inst✝ : NonUnitalRing R
toRingSeminorm✝¹ : RingSeminorm R
eq_zero_of_map_eq_zero'✝¹ : ∀ (x : R), AddGroupSeminorm.toFun toRingSeminorm✝¹.toAddGroupSeminorm x = 0 → x = 0
toRingSeminorm✝ : RingSeminorm R
eq_zero_of_map_eq_zero'✝ : ∀ (x : R), AddGroupSeminorm.toFun toRingSeminorm✝.toAddGroupSeminorm x = 0 → x = 0
h :
  (fun f => f.toFun) { toRingSeminorm := toRingSeminorm✝¹, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'✝¹ } =
    (fun f => f.toFun) { toRingSeminorm := toRingSeminorm✝, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'✝ }
⊢ toRingSeminorm✝¹ = toRingSeminorm✝
[PROOFSTEP]
ext x
[GOAL]
case mk.mk.e_toRingSeminorm.a
F : Type u_1
R : Type u_2
S : Type u_3
x✝ y : R
r : ℝ
inst✝ : NonUnitalRing R
toRingSeminorm✝¹ : RingSeminorm R
eq_zero_of_map_eq_zero'✝¹ : ∀ (x : R), AddGroupSeminorm.toFun toRingSeminorm✝¹.toAddGroupSeminorm x = 0 → x = 0
toRingSeminorm✝ : RingSeminorm R
eq_zero_of_map_eq_zero'✝ : ∀ (x : R), AddGroupSeminorm.toFun toRingSeminorm✝.toAddGroupSeminorm x = 0 → x = 0
h :
  (fun f => f.toFun) { toRingSeminorm := toRingSeminorm✝¹, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'✝¹ } =
    (fun f => f.toFun) { toRingSeminorm := toRingSeminorm✝, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'✝ }
x : R
⊢ ↑toRingSeminorm✝¹ x = ↑toRingSeminorm✝ x
[PROOFSTEP]
exact congr_fun h x
[GOAL]
F : Type u_1
R : Type u_2
S : Type u_3
x y : R
r : ℝ
inst✝ : NonAssocRing R
f g : MulRingSeminorm R
h : (fun f => f.toFun) f = (fun f => f.toFun) g
⊢ f = g
[PROOFSTEP]
cases f
[GOAL]
case mk
F : Type u_1
R : Type u_2
S : Type u_3
x y : R
r : ℝ
inst✝ : NonAssocRing R
g : MulRingSeminorm R
toAddGroupSeminorm✝ : AddGroupSeminorm R
map_one'✝ : AddGroupSeminorm.toFun toAddGroupSeminorm✝ 1 = 1
map_mul'✝ :
  ∀ (x y : R),
    AddGroupSeminorm.toFun toAddGroupSeminorm✝ (x * y) =
      AddGroupSeminorm.toFun toAddGroupSeminorm✝ x * AddGroupSeminorm.toFun toAddGroupSeminorm✝ y
h :
  (fun f => f.toFun) { toAddGroupSeminorm := toAddGroupSeminorm✝, map_one' := map_one'✝, map_mul' := map_mul'✝ } =
    (fun f => f.toFun) g
⊢ { toAddGroupSeminorm := toAddGroupSeminorm✝, map_one' := map_one'✝, map_mul' := map_mul'✝ } = g
[PROOFSTEP]
cases g
[GOAL]
case mk.mk
F : Type u_1
R : Type u_2
S : Type u_3
x y : R
r : ℝ
inst✝ : NonAssocRing R
toAddGroupSeminorm✝¹ : AddGroupSeminorm R
map_one'✝¹ : AddGroupSeminorm.toFun toAddGroupSeminorm✝¹ 1 = 1
map_mul'✝¹ :
  ∀ (x y : R),
    AddGroupSeminorm.toFun toAddGroupSeminorm✝¹ (x * y) =
      AddGroupSeminorm.toFun toAddGroupSeminorm✝¹ x * AddGroupSeminorm.toFun toAddGroupSeminorm✝¹ y
toAddGroupSeminorm✝ : AddGroupSeminorm R
map_one'✝ : AddGroupSeminorm.toFun toAddGroupSeminorm✝ 1 = 1
map_mul'✝ :
  ∀ (x y : R),
    AddGroupSeminorm.toFun toAddGroupSeminorm✝ (x * y) =
      AddGroupSeminorm.toFun toAddGroupSeminorm✝ x * AddGroupSeminorm.toFun toAddGroupSeminorm✝ y
h :
  (fun f => f.toFun) { toAddGroupSeminorm := toAddGroupSeminorm✝¹, map_one' := map_one'✝¹, map_mul' := map_mul'✝¹ } =
    (fun f => f.toFun) { toAddGroupSeminorm := toAddGroupSeminorm✝, map_one' := map_one'✝, map_mul' := map_mul'✝ }
⊢ { toAddGroupSeminorm := toAddGroupSeminorm✝¹, map_one' := map_one'✝¹, map_mul' := map_mul'✝¹ } =
    { toAddGroupSeminorm := toAddGroupSeminorm✝, map_one' := map_one'✝, map_mul' := map_mul'✝ }
[PROOFSTEP]
congr
[GOAL]
case mk.mk.e_toAddGroupSeminorm
F : Type u_1
R : Type u_2
S : Type u_3
x y : R
r : ℝ
inst✝ : NonAssocRing R
toAddGroupSeminorm✝¹ : AddGroupSeminorm R
map_one'✝¹ : AddGroupSeminorm.toFun toAddGroupSeminorm✝¹ 1 = 1
map_mul'✝¹ :
  ∀ (x y : R),
    AddGroupSeminorm.toFun toAddGroupSeminorm✝¹ (x * y) =
      AddGroupSeminorm.toFun toAddGroupSeminorm✝¹ x * AddGroupSeminorm.toFun toAddGroupSeminorm✝¹ y
toAddGroupSeminorm✝ : AddGroupSeminorm R
map_one'✝ : AddGroupSeminorm.toFun toAddGroupSeminorm✝ 1 = 1
map_mul'✝ :
  ∀ (x y : R),
    AddGroupSeminorm.toFun toAddGroupSeminorm✝ (x * y) =
      AddGroupSeminorm.toFun toAddGroupSeminorm✝ x * AddGroupSeminorm.toFun toAddGroupSeminorm✝ y
h :
  (fun f => f.toFun) { toAddGroupSeminorm := toAddGroupSeminorm✝¹, map_one' := map_one'✝¹, map_mul' := map_mul'✝¹ } =
    (fun f => f.toFun) { toAddGroupSeminorm := toAddGroupSeminorm✝, map_one' := map_one'✝, map_mul' := map_mul'✝ }
⊢ toAddGroupSeminorm✝¹ = toAddGroupSeminorm✝
[PROOFSTEP]
ext x
[GOAL]
case mk.mk.e_toAddGroupSeminorm.a
F : Type u_1
R : Type u_2
S : Type u_3
x✝ y : R
r : ℝ
inst✝ : NonAssocRing R
toAddGroupSeminorm✝¹ : AddGroupSeminorm R
map_one'✝¹ : AddGroupSeminorm.toFun toAddGroupSeminorm✝¹ 1 = 1
map_mul'✝¹ :
  ∀ (x y : R),
    AddGroupSeminorm.toFun toAddGroupSeminorm✝¹ (x * y) =
      AddGroupSeminorm.toFun toAddGroupSeminorm✝¹ x * AddGroupSeminorm.toFun toAddGroupSeminorm✝¹ y
toAddGroupSeminorm✝ : AddGroupSeminorm R
map_one'✝ : AddGroupSeminorm.toFun toAddGroupSeminorm✝ 1 = 1
map_mul'✝ :
  ∀ (x y : R),
    AddGroupSeminorm.toFun toAddGroupSeminorm✝ (x * y) =
      AddGroupSeminorm.toFun toAddGroupSeminorm✝ x * AddGroupSeminorm.toFun toAddGroupSeminorm✝ y
h :
  (fun f => f.toFun) { toAddGroupSeminorm := toAddGroupSeminorm✝¹, map_one' := map_one'✝¹, map_mul' := map_mul'✝¹ } =
    (fun f => f.toFun) { toAddGroupSeminorm := toAddGroupSeminorm✝, map_one' := map_one'✝, map_mul' := map_mul'✝ }
x : R
⊢ ↑toAddGroupSeminorm✝¹ x = ↑toAddGroupSeminorm✝ x
[PROOFSTEP]
exact congr_fun h x
[GOAL]
F : Type u_1
R : Type u_2
S : Type u_3
x✝ y✝ : R
r : ℝ
inst✝³ : NonAssocRing R
inst✝² : DecidableEq R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
src✝ : AddGroupSeminorm R := 1
x y : R
⊢ AddGroupSeminorm.toFun
      { toFun := src✝.toFun, map_zero' := (_ : AddGroupSeminorm.toFun src✝ 0 = 0),
        add_le' :=
          (_ :
            ∀ (r s : R),
              AddGroupSeminorm.toFun src✝ (r + s) ≤ AddGroupSeminorm.toFun src✝ r + AddGroupSeminorm.toFun src✝ s),
        neg' := (_ : ∀ (r : R), AddGroupSeminorm.toFun src✝ (-r) = AddGroupSeminorm.toFun src✝ r) }
      (x * y) =
    AddGroupSeminorm.toFun
        { toFun := src✝.toFun, map_zero' := (_ : AddGroupSeminorm.toFun src✝ 0 = 0),
          add_le' :=
            (_ :
              ∀ (r s : R),
                AddGroupSeminorm.toFun src✝ (r + s) ≤ AddGroupSeminorm.toFun src✝ r + AddGroupSeminorm.toFun src✝ s),
          neg' := (_ : ∀ (r : R), AddGroupSeminorm.toFun src✝ (-r) = AddGroupSeminorm.toFun src✝ r) }
        x *
      AddGroupSeminorm.toFun
        { toFun := src✝.toFun, map_zero' := (_ : AddGroupSeminorm.toFun src✝ 0 = 0),
          add_le' :=
            (_ :
              ∀ (r s : R),
                AddGroupSeminorm.toFun src✝ (r + s) ≤ AddGroupSeminorm.toFun src✝ r + AddGroupSeminorm.toFun src✝ s),
          neg' := (_ : ∀ (r : R), AddGroupSeminorm.toFun src✝ (-r) = AddGroupSeminorm.toFun src✝ r) }
        y
[PROOFSTEP]
obtain rfl | hx := eq_or_ne x 0
[GOAL]
case inl
F : Type u_1
R : Type u_2
S : Type u_3
x y✝ : R
r : ℝ
inst✝³ : NonAssocRing R
inst✝² : DecidableEq R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
src✝ : AddGroupSeminorm R := 1
y : R
⊢ AddGroupSeminorm.toFun
      { toFun := src✝.toFun, map_zero' := (_ : AddGroupSeminorm.toFun src✝ 0 = 0),
        add_le' :=
          (_ :
            ∀ (r s : R),
              AddGroupSeminorm.toFun src✝ (r + s) ≤ AddGroupSeminorm.toFun src✝ r + AddGroupSeminorm.toFun src✝ s),
        neg' := (_ : ∀ (r : R), AddGroupSeminorm.toFun src✝ (-r) = AddGroupSeminorm.toFun src✝ r) }
      (0 * y) =
    AddGroupSeminorm.toFun
        { toFun := src✝.toFun, map_zero' := (_ : AddGroupSeminorm.toFun src✝ 0 = 0),
          add_le' :=
            (_ :
              ∀ (r s : R),
                AddGroupSeminorm.toFun src✝ (r + s) ≤ AddGroupSeminorm.toFun src✝ r + AddGroupSeminorm.toFun src✝ s),
          neg' := (_ : ∀ (r : R), AddGroupSeminorm.toFun src✝ (-r) = AddGroupSeminorm.toFun src✝ r) }
        0 *
      AddGroupSeminorm.toFun
        { toFun := src✝.toFun, map_zero' := (_ : AddGroupSeminorm.toFun src✝ 0 = 0),
          add_le' :=
            (_ :
              ∀ (r s : R),
                AddGroupSeminorm.toFun src✝ (r + s) ≤ AddGroupSeminorm.toFun src✝ r + AddGroupSeminorm.toFun src✝ s),
          neg' := (_ : ∀ (r : R), AddGroupSeminorm.toFun src✝ (-r) = AddGroupSeminorm.toFun src✝ r) }
        y
[PROOFSTEP]
simp
[GOAL]
case inr
F : Type u_1
R : Type u_2
S : Type u_3
x✝ y✝ : R
r : ℝ
inst✝³ : NonAssocRing R
inst✝² : DecidableEq R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
src✝ : AddGroupSeminorm R := 1
x y : R
hx : x ≠ 0
⊢ AddGroupSeminorm.toFun
      { toFun := src✝.toFun, map_zero' := (_ : AddGroupSeminorm.toFun src✝ 0 = 0),
        add_le' :=
          (_ :
            ∀ (r s : R),
              AddGroupSeminorm.toFun src✝ (r + s) ≤ AddGroupSeminorm.toFun src✝ r + AddGroupSeminorm.toFun src✝ s),
        neg' := (_ : ∀ (r : R), AddGroupSeminorm.toFun src✝ (-r) = AddGroupSeminorm.toFun src✝ r) }
      (x * y) =
    AddGroupSeminorm.toFun
        { toFun := src✝.toFun, map_zero' := (_ : AddGroupSeminorm.toFun src✝ 0 = 0),
          add_le' :=
            (_ :
              ∀ (r s : R),
                AddGroupSeminorm.toFun src✝ (r + s) ≤ AddGroupSeminorm.toFun src✝ r + AddGroupSeminorm.toFun src✝ s),
          neg' := (_ : ∀ (r : R), AddGroupSeminorm.toFun src✝ (-r) = AddGroupSeminorm.toFun src✝ r) }
        x *
      AddGroupSeminorm.toFun
        { toFun := src✝.toFun, map_zero' := (_ : AddGroupSeminorm.toFun src✝ 0 = 0),
          add_le' :=
            (_ :
              ∀ (r s : R),
                AddGroupSeminorm.toFun src✝ (r + s) ≤ AddGroupSeminorm.toFun src✝ r + AddGroupSeminorm.toFun src✝ s),
          neg' := (_ : ∀ (r : R), AddGroupSeminorm.toFun src✝ (-r) = AddGroupSeminorm.toFun src✝ r) }
        y
[PROOFSTEP]
obtain rfl | hy := eq_or_ne y 0
[GOAL]
case inr.inl
F : Type u_1
R : Type u_2
S : Type u_3
x✝ y : R
r : ℝ
inst✝³ : NonAssocRing R
inst✝² : DecidableEq R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
src✝ : AddGroupSeminorm R := 1
x : R
hx : x ≠ 0
⊢ AddGroupSeminorm.toFun
      { toFun := src✝.toFun, map_zero' := (_ : AddGroupSeminorm.toFun src✝ 0 = 0),
        add_le' :=
          (_ :
            ∀ (r s : R),
              AddGroupSeminorm.toFun src✝ (r + s) ≤ AddGroupSeminorm.toFun src✝ r + AddGroupSeminorm.toFun src✝ s),
        neg' := (_ : ∀ (r : R), AddGroupSeminorm.toFun src✝ (-r) = AddGroupSeminorm.toFun src✝ r) }
      (x * 0) =
    AddGroupSeminorm.toFun
        { toFun := src✝.toFun, map_zero' := (_ : AddGroupSeminorm.toFun src✝ 0 = 0),
          add_le' :=
            (_ :
              ∀ (r s : R),
                AddGroupSeminorm.toFun src✝ (r + s) ≤ AddGroupSeminorm.toFun src✝ r + AddGroupSeminorm.toFun src✝ s),
          neg' := (_ : ∀ (r : R), AddGroupSeminorm.toFun src✝ (-r) = AddGroupSeminorm.toFun src✝ r) }
        x *
      AddGroupSeminorm.toFun
        { toFun := src✝.toFun, map_zero' := (_ : AddGroupSeminorm.toFun src✝ 0 = 0),
          add_le' :=
            (_ :
              ∀ (r s : R),
                AddGroupSeminorm.toFun src✝ (r + s) ≤ AddGroupSeminorm.toFun src✝ r + AddGroupSeminorm.toFun src✝ s),
          neg' := (_ : ∀ (r : R), AddGroupSeminorm.toFun src✝ (-r) = AddGroupSeminorm.toFun src✝ r) }
        0
[PROOFSTEP]
simp
[GOAL]
case inr.inr
F : Type u_1
R : Type u_2
S : Type u_3
x✝ y✝ : R
r : ℝ
inst✝³ : NonAssocRing R
inst✝² : DecidableEq R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
src✝ : AddGroupSeminorm R := 1
x y : R
hx : x ≠ 0
hy : y ≠ 0
⊢ AddGroupSeminorm.toFun
      { toFun := src✝.toFun, map_zero' := (_ : AddGroupSeminorm.toFun src✝ 0 = 0),
        add_le' :=
          (_ :
            ∀ (r s : R),
              AddGroupSeminorm.toFun src✝ (r + s) ≤ AddGroupSeminorm.toFun src✝ r + AddGroupSeminorm.toFun src✝ s),
        neg' := (_ : ∀ (r : R), AddGroupSeminorm.toFun src✝ (-r) = AddGroupSeminorm.toFun src✝ r) }
      (x * y) =
    AddGroupSeminorm.toFun
        { toFun := src✝.toFun, map_zero' := (_ : AddGroupSeminorm.toFun src✝ 0 = 0),
          add_le' :=
            (_ :
              ∀ (r s : R),
                AddGroupSeminorm.toFun src✝ (r + s) ≤ AddGroupSeminorm.toFun src✝ r + AddGroupSeminorm.toFun src✝ s),
          neg' := (_ : ∀ (r : R), AddGroupSeminorm.toFun src✝ (-r) = AddGroupSeminorm.toFun src✝ r) }
        x *
      AddGroupSeminorm.toFun
        { toFun := src✝.toFun, map_zero' := (_ : AddGroupSeminorm.toFun src✝ 0 = 0),
          add_le' :=
            (_ :
              ∀ (r s : R),
                AddGroupSeminorm.toFun src✝ (r + s) ≤ AddGroupSeminorm.toFun src✝ r + AddGroupSeminorm.toFun src✝ s),
          neg' := (_ : ∀ (r : R), AddGroupSeminorm.toFun src✝ (-r) = AddGroupSeminorm.toFun src✝ r) }
        y
[PROOFSTEP]
simp [hx, hy]
[GOAL]
F : Type u_1
R : Type u_2
S : Type u_3
x y : R
r : ℝ
inst✝ : NonAssocRing R
f g : MulRingNorm R
h : (fun f => f.toFun) f = (fun f => f.toFun) g
⊢ f = g
[PROOFSTEP]
cases f
[GOAL]
case mk
F : Type u_1
R : Type u_2
S : Type u_3
x y : R
r : ℝ
inst✝ : NonAssocRing R
g : MulRingNorm R
toMulRingSeminorm✝ : MulRingSeminorm R
eq_zero_of_map_eq_zero'✝ : ∀ (x : R), AddGroupSeminorm.toFun toMulRingSeminorm✝.toAddGroupSeminorm x = 0 → x = 0
h :
  (fun f => f.toFun) { toMulRingSeminorm := toMulRingSeminorm✝, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'✝ } =
    (fun f => f.toFun) g
⊢ { toMulRingSeminorm := toMulRingSeminorm✝, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'✝ } = g
[PROOFSTEP]
cases g
[GOAL]
case mk.mk
F : Type u_1
R : Type u_2
S : Type u_3
x y : R
r : ℝ
inst✝ : NonAssocRing R
toMulRingSeminorm✝¹ : MulRingSeminorm R
eq_zero_of_map_eq_zero'✝¹ : ∀ (x : R), AddGroupSeminorm.toFun toMulRingSeminorm✝¹.toAddGroupSeminorm x = 0 → x = 0
toMulRingSeminorm✝ : MulRingSeminorm R
eq_zero_of_map_eq_zero'✝ : ∀ (x : R), AddGroupSeminorm.toFun toMulRingSeminorm✝.toAddGroupSeminorm x = 0 → x = 0
h :
  (fun f => f.toFun)
      { toMulRingSeminorm := toMulRingSeminorm✝¹, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'✝¹ } =
    (fun f => f.toFun) { toMulRingSeminorm := toMulRingSeminorm✝, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'✝ }
⊢ { toMulRingSeminorm := toMulRingSeminorm✝¹, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'✝¹ } =
    { toMulRingSeminorm := toMulRingSeminorm✝, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'✝ }
[PROOFSTEP]
congr
[GOAL]
case mk.mk.e_toMulRingSeminorm
F : Type u_1
R : Type u_2
S : Type u_3
x y : R
r : ℝ
inst✝ : NonAssocRing R
toMulRingSeminorm✝¹ : MulRingSeminorm R
eq_zero_of_map_eq_zero'✝¹ : ∀ (x : R), AddGroupSeminorm.toFun toMulRingSeminorm✝¹.toAddGroupSeminorm x = 0 → x = 0
toMulRingSeminorm✝ : MulRingSeminorm R
eq_zero_of_map_eq_zero'✝ : ∀ (x : R), AddGroupSeminorm.toFun toMulRingSeminorm✝.toAddGroupSeminorm x = 0 → x = 0
h :
  (fun f => f.toFun)
      { toMulRingSeminorm := toMulRingSeminorm✝¹, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'✝¹ } =
    (fun f => f.toFun) { toMulRingSeminorm := toMulRingSeminorm✝, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'✝ }
⊢ toMulRingSeminorm✝¹ = toMulRingSeminorm✝
[PROOFSTEP]
ext x
[GOAL]
case mk.mk.e_toMulRingSeminorm.a
F : Type u_1
R : Type u_2
S : Type u_3
x✝ y : R
r : ℝ
inst✝ : NonAssocRing R
toMulRingSeminorm✝¹ : MulRingSeminorm R
eq_zero_of_map_eq_zero'✝¹ : ∀ (x : R), AddGroupSeminorm.toFun toMulRingSeminorm✝¹.toAddGroupSeminorm x = 0 → x = 0
toMulRingSeminorm✝ : MulRingSeminorm R
eq_zero_of_map_eq_zero'✝ : ∀ (x : R), AddGroupSeminorm.toFun toMulRingSeminorm✝.toAddGroupSeminorm x = 0 → x = 0
h :
  (fun f => f.toFun)
      { toMulRingSeminorm := toMulRingSeminorm✝¹, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'✝¹ } =
    (fun f => f.toFun) { toMulRingSeminorm := toMulRingSeminorm✝, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'✝ }
x : R
⊢ ↑toMulRingSeminorm✝¹ x = ↑toMulRingSeminorm✝ x
[PROOFSTEP]
exact congr_fun h x
[GOAL]
F : Type u_1
R : Type u_2
S : Type u_3
x✝ y : R
r : ℝ
K : Type u_4
inst✝ : Field K
f : RingSeminorm K
hnt : f ≠ 0
x : K
hx :
  AddGroupSeminorm.toFun
      { toAddGroupSeminorm := f.toAddGroupSeminorm,
          mul_le' :=
            (_ :
              ∀ (x y : K),
                AddGroupSeminorm.toFun f.toAddGroupSeminorm (x * y) ≤
                  AddGroupSeminorm.toFun f.toAddGroupSeminorm x *
                    AddGroupSeminorm.toFun f.toAddGroupSeminorm y) }.toAddGroupSeminorm
      x =
    0
⊢ x = 0
[PROOFSTEP]
obtain ⟨c, hc⟩ := RingSeminorm.ne_zero_iff.mp hnt
[GOAL]
case intro
F : Type u_1
R : Type u_2
S : Type u_3
x✝ y : R
r : ℝ
K : Type u_4
inst✝ : Field K
f : RingSeminorm K
hnt : f ≠ 0
x : K
hx :
  AddGroupSeminorm.toFun
      { toAddGroupSeminorm := f.toAddGroupSeminorm,
          mul_le' :=
            (_ :
              ∀ (x y : K),
                AddGroupSeminorm.toFun f.toAddGroupSeminorm (x * y) ≤
                  AddGroupSeminorm.toFun f.toAddGroupSeminorm x *
                    AddGroupSeminorm.toFun f.toAddGroupSeminorm y) }.toAddGroupSeminorm
      x =
    0
c : K
hc : ↑f c ≠ 0
⊢ x = 0
[PROOFSTEP]
by_contra hn0
[GOAL]
case intro
F : Type u_1
R : Type u_2
S : Type u_3
x✝ y : R
r : ℝ
K : Type u_4
inst✝ : Field K
f : RingSeminorm K
hnt : f ≠ 0
x : K
hx :
  AddGroupSeminorm.toFun
      { toAddGroupSeminorm := f.toAddGroupSeminorm,
          mul_le' :=
            (_ :
              ∀ (x y : K),
                AddGroupSeminorm.toFun f.toAddGroupSeminorm (x * y) ≤
                  AddGroupSeminorm.toFun f.toAddGroupSeminorm x *
                    AddGroupSeminorm.toFun f.toAddGroupSeminorm y) }.toAddGroupSeminorm
      x =
    0
c : K
hc : ↑f c ≠ 0
hn0 : ¬x = 0
⊢ False
[PROOFSTEP]
have hc0 : f c = 0 := by
  rw [← mul_one c, ← mul_inv_cancel hn0, ← mul_assoc, mul_comm c, mul_assoc]
  exact
    le_antisymm
      (le_trans (map_mul_le_mul f _ _)
        (by rw [← RingSeminorm.toFun_eq_coe, ← AddGroupSeminorm.toFun_eq_coe, hx, zero_mul]))
      (map_nonneg f _)
[GOAL]
F : Type u_1
R : Type u_2
S : Type u_3
x✝ y : R
r : ℝ
K : Type u_4
inst✝ : Field K
f : RingSeminorm K
hnt : f ≠ 0
x : K
hx :
  AddGroupSeminorm.toFun
      { toAddGroupSeminorm := f.toAddGroupSeminorm,
          mul_le' :=
            (_ :
              ∀ (x y : K),
                AddGroupSeminorm.toFun f.toAddGroupSeminorm (x * y) ≤
                  AddGroupSeminorm.toFun f.toAddGroupSeminorm x *
                    AddGroupSeminorm.toFun f.toAddGroupSeminorm y) }.toAddGroupSeminorm
      x =
    0
c : K
hc : ↑f c ≠ 0
hn0 : ¬x = 0
⊢ ↑f c = 0
[PROOFSTEP]
rw [← mul_one c, ← mul_inv_cancel hn0, ← mul_assoc, mul_comm c, mul_assoc]
[GOAL]
F : Type u_1
R : Type u_2
S : Type u_3
x✝ y : R
r : ℝ
K : Type u_4
inst✝ : Field K
f : RingSeminorm K
hnt : f ≠ 0
x : K
hx :
  AddGroupSeminorm.toFun
      { toAddGroupSeminorm := f.toAddGroupSeminorm,
          mul_le' :=
            (_ :
              ∀ (x y : K),
                AddGroupSeminorm.toFun f.toAddGroupSeminorm (x * y) ≤
                  AddGroupSeminorm.toFun f.toAddGroupSeminorm x *
                    AddGroupSeminorm.toFun f.toAddGroupSeminorm y) }.toAddGroupSeminorm
      x =
    0
c : K
hc : ↑f c ≠ 0
hn0 : ¬x = 0
⊢ ↑f (x * (c * x⁻¹)) = 0
[PROOFSTEP]
exact
  le_antisymm
    (le_trans (map_mul_le_mul f _ _)
      (by rw [← RingSeminorm.toFun_eq_coe, ← AddGroupSeminorm.toFun_eq_coe, hx, zero_mul]))
    (map_nonneg f _)
[GOAL]
F : Type u_1
R : Type u_2
S : Type u_3
x✝ y : R
r : ℝ
K : Type u_4
inst✝ : Field K
f : RingSeminorm K
hnt : f ≠ 0
x : K
hx :
  AddGroupSeminorm.toFun
      { toAddGroupSeminorm := f.toAddGroupSeminorm,
          mul_le' :=
            (_ :
              ∀ (x y : K),
                AddGroupSeminorm.toFun f.toAddGroupSeminorm (x * y) ≤
                  AddGroupSeminorm.toFun f.toAddGroupSeminorm x *
                    AddGroupSeminorm.toFun f.toAddGroupSeminorm y) }.toAddGroupSeminorm
      x =
    0
c : K
hc : ↑f c ≠ 0
hn0 : ¬x = 0
⊢ ↑f x * ↑f (c * x⁻¹) ≤ 0
[PROOFSTEP]
rw [← RingSeminorm.toFun_eq_coe, ← AddGroupSeminorm.toFun_eq_coe, hx, zero_mul]
[GOAL]
case intro
F : Type u_1
R : Type u_2
S : Type u_3
x✝ y : R
r : ℝ
K : Type u_4
inst✝ : Field K
f : RingSeminorm K
hnt : f ≠ 0
x : K
hx :
  AddGroupSeminorm.toFun
      { toAddGroupSeminorm := f.toAddGroupSeminorm,
          mul_le' :=
            (_ :
              ∀ (x y : K),
                AddGroupSeminorm.toFun f.toAddGroupSeminorm (x * y) ≤
                  AddGroupSeminorm.toFun f.toAddGroupSeminorm x *
                    AddGroupSeminorm.toFun f.toAddGroupSeminorm y) }.toAddGroupSeminorm
      x =
    0
c : K
hc : ↑f c ≠ 0
hn0 : ¬x = 0
hc0 : ↑f c = 0
⊢ False
[PROOFSTEP]
exact hc hc0
