[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


[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedCommRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
s : Set E
x✝¹ : E
x✝ : x✝¹ ∈ s
⊢ ‖↑(↑B x✝¹) 0‖ ≤ 1
[PROOFSTEP]
simp only [map_zero, norm_zero, zero_le_one]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedCommRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
s : Set E
⊢ polar B s = ⋂ (x : E) (_ : x ∈ s), {y | ‖↑(↑B x) y‖ ≤ 1}
[PROOFSTEP]
ext
[GOAL]
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedCommRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
s : Set E
x✝ : F
⊢ x✝ ∈ polar B s ↔ x✝ ∈ ⋂ (x : E) (_ : x ∈ s), {y | ‖↑(↑B x) y‖ ≤ 1}
[PROOFSTEP]
simp only [polar_mem_iff, Set.mem_iInter, Set.mem_setOf_eq]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedCommRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
⊢ polar B {0} = Set.univ
[PROOFSTEP]
refine' Set.eq_univ_iff_forall.mpr fun y x hx => _
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedCommRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
y : F
x : E
hx : x ∈ {0}
⊢ ‖↑(↑B x) y‖ ≤ 1
[PROOFSTEP]
rw [Set.mem_singleton_iff.mp hx, map_zero, LinearMap.zero_apply, norm_zero]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedCommRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
y : F
x : E
hx : x ∈ {0}
⊢ 0 ≤ 1
[PROOFSTEP]
exact zero_le_one
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedCommRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
s : Set E
x : E
hx : x ∈ s
y : F
hy : y ∈ polar B s
⊢ ‖↑(↑(flip B) y) x‖ ≤ 1
[PROOFSTEP]
rw [B.flip_apply]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedCommRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
s : Set E
x : E
hx : x ∈ s
y : F
hy : y ∈ polar B s
⊢ ‖↑(↑B x) y‖ ≤ 1
[PROOFSTEP]
exact hy x hx
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedCommRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
s : Set E
⊢ IsClosed (polar B s)
[PROOFSTEP]
rw [polar_eq_iInter]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedCommRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
s : Set E
⊢ IsClosed (⋂ (x : E) (_ : x ∈ s), {y | ‖↑(↑B x) y‖ ≤ 1})
[PROOFSTEP]
refine' isClosed_iInter fun x => isClosed_iInter fun _ => _
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedCommRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
s : Set E
x : E
x✝ : x ∈ s
⊢ IsClosed {y | ‖↑(↑B x) y‖ ≤ 1}
[PROOFSTEP]
exact isClosed_le (WeakBilin.eval_continuous B.flip x).norm continuous_const
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
h : SeparatingRight B
⊢ polar B Set.univ = {0}
[PROOFSTEP]
rw [Set.eq_singleton_iff_unique_mem]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
h : SeparatingRight B
⊢ 0 ∈ polar B Set.univ ∧ ∀ (x : F), x ∈ polar B Set.univ → x = 0
[PROOFSTEP]
refine' ⟨by simp only [zero_mem_polar], fun y hy => h _ fun x => _⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
h : SeparatingRight B
⊢ 0 ∈ polar B Set.univ
[PROOFSTEP]
simp only [zero_mem_polar]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
h : SeparatingRight B
y : F
hy : y ∈ polar B Set.univ
x : E
⊢ ↑(↑B x) y = 0
[PROOFSTEP]
refine' norm_le_zero_iff.mp (le_of_forall_le_of_dense fun ε hε => _)
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
h : SeparatingRight B
y : F
hy : y ∈ polar B Set.univ
x : E
ε : ℝ
hε : 0 < ε
⊢ ‖↑(↑B x) y‖ ≤ ε
[PROOFSTEP]
rcases NormedField.exists_norm_lt 𝕜 hε with ⟨c, hc, hcε⟩
[GOAL]
case intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
h : SeparatingRight B
y : F
hy : y ∈ polar B Set.univ
x : E
ε : ℝ
hε : 0 < ε
c : 𝕜
hc : 0 < ‖c‖
hcε : ‖c‖ < ε
⊢ ‖↑(↑B x) y‖ ≤ ε
[PROOFSTEP]
calc
  ‖B x y‖ = ‖c‖ * ‖B (c⁻¹ • x) y‖ := by
    rw [B.map_smul, LinearMap.smul_apply, Algebra.id.smul_eq_mul, norm_mul, norm_inv, mul_inv_cancel_left₀ hc.ne']
  _ ≤ ε * 1 := by gcongr; exact hy _ trivial
  _ = ε := mul_one _
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
h : SeparatingRight B
y : F
hy : y ∈ polar B Set.univ
x : E
ε : ℝ
hε : 0 < ε
c : 𝕜
hc : 0 < ‖c‖
hcε : ‖c‖ < ε
⊢ ‖↑(↑B x) y‖ = ‖c‖ * ‖↑(↑B (c⁻¹ • x)) y‖
[PROOFSTEP]
rw [B.map_smul, LinearMap.smul_apply, Algebra.id.smul_eq_mul, norm_mul, norm_inv, mul_inv_cancel_left₀ hc.ne']
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
h : SeparatingRight B
y : F
hy : y ∈ polar B Set.univ
x : E
ε : ℝ
hε : 0 < ε
c : 𝕜
hc : 0 < ‖c‖
hcε : ‖c‖ < ε
⊢ ‖c‖ * ‖↑(↑B (c⁻¹ • x)) y‖ ≤ ε * 1
[PROOFSTEP]
gcongr
[GOAL]
case h₂
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
h : SeparatingRight B
y : F
hy : y ∈ polar B Set.univ
x : E
ε : ℝ
hε : 0 < ε
c : 𝕜
hc : 0 < ‖c‖
hcε : ‖c‖ < ε
⊢ ‖↑(↑B (c⁻¹ • x)) y‖ ≤ 1
[PROOFSTEP]
exact hy _ trivial


[GOAL]
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : BarrelledSpace 𝕜 E
p : ι → Seminorm 𝕜 E
hp : ∀ (i : ι), Continuous ↑(p i)
bdd : BddAbove (range p)
⊢ Continuous (⨆ (i : ι), ↑(p i))
[PROOFSTEP]
rw [← Seminorm.coe_iSup_eq bdd]
[GOAL]
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : BarrelledSpace 𝕜 E
p : ι → Seminorm 𝕜 E
hp : ∀ (i : ι), Continuous ↑(p i)
bdd : BddAbove (range p)
⊢ Continuous ↑(⨆ (i : ι), p i)
[PROOFSTEP]
refine Seminorm.continuous_of_lowerSemicontinuous _ ?_
[GOAL]
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : BarrelledSpace 𝕜 E
p : ι → Seminorm 𝕜 E
hp : ∀ (i : ι), Continuous ↑(p i)
bdd : BddAbove (range p)
⊢ LowerSemicontinuous ↑(⨆ (i : ι), p i)
[PROOFSTEP]
rw [Seminorm.coe_iSup_eq bdd]
[GOAL]
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : BarrelledSpace 𝕜 E
p : ι → Seminorm 𝕜 E
hp : ∀ (i : ι), Continuous ↑(p i)
bdd : BddAbove (range p)
⊢ LowerSemicontinuous (⨆ (i : ι), ↑(p i))
[PROOFSTEP]
rw [Seminorm.bddAbove_range_iff] at bdd
[GOAL]
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : BarrelledSpace 𝕜 E
p : ι → Seminorm 𝕜 E
hp : ∀ (i : ι), Continuous ↑(p i)
bdd : ∀ (x : E), BddAbove (range fun i => ↑(p i) x)
⊢ LowerSemicontinuous (⨆ (i : ι), ↑(p i))
[PROOFSTEP]
convert lowerSemicontinuous_ciSup (f := fun i x ↦ p i x) bdd (fun i ↦ (hp i).lowerSemicontinuous)
[GOAL]
case h.e'_5.h
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : BarrelledSpace 𝕜 E
p : ι → Seminorm 𝕜 E
hp : ∀ (i : ι), Continuous ↑(p i)
bdd : ∀ (x : E), BddAbove (range fun i => ↑(p i) x)
x✝ : E
⊢ iSup (fun i => ↑(p i)) x✝ = ⨆ (i : ι), ↑(p i) x✝
[PROOFSTEP]
exact iSup_apply
[GOAL]
α : Type u_1
ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst✝¹¹ : Nonempty κ
inst✝¹⁰ : NontriviallyNormedField 𝕜₁
inst✝⁹ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst✝⁸ : RingHomIsometric σ₁₂
inst✝⁷ : AddCommGroup E
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : Module 𝕜₂ F
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousConstSMul 𝕜₁ E
inst✝ : BaireSpace E
⊢ ∀ (p : Seminorm 𝕜₁ E), LowerSemicontinuous ↑p → Continuous ↑p
[PROOFSTEP]
intro p hp
[GOAL]
α : Type u_1
ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst✝¹¹ : Nonempty κ
inst✝¹⁰ : NontriviallyNormedField 𝕜₁
inst✝⁹ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst✝⁸ : RingHomIsometric σ₁₂
inst✝⁷ : AddCommGroup E
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : Module 𝕜₂ F
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousConstSMul 𝕜₁ E
inst✝ : BaireSpace E
p : Seminorm 𝕜₁ E
hp : LowerSemicontinuous ↑p
⊢ Continuous ↑p
[PROOFSTEP]
have h₁ : ∀ n : ℕ, IsClosed (p.closedBall (0 : E) n) := fun n ↦ by
  simpa [p.closedBall_zero_eq] using hp.isClosed_preimage n
[GOAL]
α : Type u_1
ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst✝¹¹ : Nonempty κ
inst✝¹⁰ : NontriviallyNormedField 𝕜₁
inst✝⁹ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst✝⁸ : RingHomIsometric σ₁₂
inst✝⁷ : AddCommGroup E
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : Module 𝕜₂ F
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousConstSMul 𝕜₁ E
inst✝ : BaireSpace E
p : Seminorm 𝕜₁ E
hp : LowerSemicontinuous ↑p
n : ℕ
⊢ IsClosed (Seminorm.closedBall p 0 ↑n)
[PROOFSTEP]
simpa [p.closedBall_zero_eq] using hp.isClosed_preimage n
[GOAL]
α : Type u_1
ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst✝¹¹ : Nonempty κ
inst✝¹⁰ : NontriviallyNormedField 𝕜₁
inst✝⁹ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst✝⁸ : RingHomIsometric σ₁₂
inst✝⁷ : AddCommGroup E
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : Module 𝕜₂ F
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousConstSMul 𝕜₁ E
inst✝ : BaireSpace E
p : Seminorm 𝕜₁ E
hp : LowerSemicontinuous ↑p
h₁ : ∀ (n : ℕ), IsClosed (Seminorm.closedBall p 0 ↑n)
⊢ Continuous ↑p
[PROOFSTEP]
have h₂ : (⋃ n : ℕ, p.closedBall (0 : E) n) = univ :=
  eq_univ_of_forall fun x ↦
    mem_iUnion.mpr
      (exists_nat_ge <| p (x - 0))
        -- Hence, one of them has nonempty interior. Let `n : ℕ` be its radius, and fix `x` an
            -- interior point.
[GOAL]
α : Type u_1
ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst✝¹¹ : Nonempty κ
inst✝¹⁰ : NontriviallyNormedField 𝕜₁
inst✝⁹ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst✝⁸ : RingHomIsometric σ₁₂
inst✝⁷ : AddCommGroup E
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : Module 𝕜₂ F
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousConstSMul 𝕜₁ E
inst✝ : BaireSpace E
p : Seminorm 𝕜₁ E
hp : LowerSemicontinuous ↑p
h₁ : ∀ (n : ℕ), IsClosed (Seminorm.closedBall p 0 ↑n)
h₂ : ⋃ (n : ℕ), Seminorm.closedBall p 0 ↑n = univ
⊢ Continuous ↑p
[PROOFSTEP]
rcases nonempty_interior_of_iUnion_of_closed h₁ h₂ with
  ⟨n, ⟨x, hxn⟩⟩
    -- To show that `p` is continuous, we will show that the `p`-closed-ball of
        -- radius `2*n` is a neighborhood of zero.
[GOAL]
case intro.intro
α : Type u_1
ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst✝¹¹ : Nonempty κ
inst✝¹⁰ : NontriviallyNormedField 𝕜₁
inst✝⁹ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst✝⁸ : RingHomIsometric σ₁₂
inst✝⁷ : AddCommGroup E
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : Module 𝕜₂ F
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousConstSMul 𝕜₁ E
inst✝ : BaireSpace E
p : Seminorm 𝕜₁ E
hp : LowerSemicontinuous ↑p
h₁ : ∀ (n : ℕ), IsClosed (Seminorm.closedBall p 0 ↑n)
h₂ : ⋃ (n : ℕ), Seminorm.closedBall p 0 ↑n = univ
n : ℕ
x : E
hxn : x ∈ interior (Seminorm.closedBall p 0 ↑n)
⊢ Continuous ↑p
[PROOFSTEP]
refine Seminorm.continuous' (r := n + n) ?_
[GOAL]
case intro.intro
α : Type u_1
ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst✝¹¹ : Nonempty κ
inst✝¹⁰ : NontriviallyNormedField 𝕜₁
inst✝⁹ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst✝⁸ : RingHomIsometric σ₁₂
inst✝⁷ : AddCommGroup E
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : Module 𝕜₂ F
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousConstSMul 𝕜₁ E
inst✝ : BaireSpace E
p : Seminorm 𝕜₁ E
hp : LowerSemicontinuous ↑p
h₁ : ∀ (n : ℕ), IsClosed (Seminorm.closedBall p 0 ↑n)
h₂ : ⋃ (n : ℕ), Seminorm.closedBall p 0 ↑n = univ
n : ℕ
x : E
hxn : x ∈ interior (Seminorm.closedBall p 0 ↑n)
⊢ Seminorm.closedBall p 0 (↑n + ↑n) ∈ 𝓝 0
[PROOFSTEP]
rw [p.closedBall_zero_eq] at hxn ⊢
[GOAL]
case intro.intro
α : Type u_1
ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst✝¹¹ : Nonempty κ
inst✝¹⁰ : NontriviallyNormedField 𝕜₁
inst✝⁹ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst✝⁸ : RingHomIsometric σ₁₂
inst✝⁷ : AddCommGroup E
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : Module 𝕜₂ F
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousConstSMul 𝕜₁ E
inst✝ : BaireSpace E
p : Seminorm 𝕜₁ E
hp : LowerSemicontinuous ↑p
h₁ : ∀ (n : ℕ), IsClosed (Seminorm.closedBall p 0 ↑n)
h₂ : ⋃ (n : ℕ), Seminorm.closedBall p 0 ↑n = univ
n : ℕ
x : E
hxn : x ∈ interior {y | ↑p y ≤ ↑n}
⊢ {y | ↑p y ≤ ↑n + ↑n} ∈ 𝓝 0
[PROOFSTEP]
have hxn' : p x ≤ n := by convert interior_subset hxn
[GOAL]
α : Type u_1
ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst✝¹¹ : Nonempty κ
inst✝¹⁰ : NontriviallyNormedField 𝕜₁
inst✝⁹ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst✝⁸ : RingHomIsometric σ₁₂
inst✝⁷ : AddCommGroup E
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : Module 𝕜₂ F
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousConstSMul 𝕜₁ E
inst✝ : BaireSpace E
p : Seminorm 𝕜₁ E
hp : LowerSemicontinuous ↑p
h₁ : ∀ (n : ℕ), IsClosed (Seminorm.closedBall p 0 ↑n)
h₂ : ⋃ (n : ℕ), Seminorm.closedBall p 0 ↑n = univ
n : ℕ
x : E
hxn : x ∈ interior {y | ↑p y ≤ ↑n}
⊢ ↑p x ≤ ↑n
[PROOFSTEP]
convert interior_subset hxn
[GOAL]
case intro.intro
α : Type u_1
ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst✝¹¹ : Nonempty κ
inst✝¹⁰ : NontriviallyNormedField 𝕜₁
inst✝⁹ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst✝⁸ : RingHomIsometric σ₁₂
inst✝⁷ : AddCommGroup E
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : Module 𝕜₂ F
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousConstSMul 𝕜₁ E
inst✝ : BaireSpace E
p : Seminorm 𝕜₁ E
hp : LowerSemicontinuous ↑p
h₁ : ∀ (n : ℕ), IsClosed (Seminorm.closedBall p 0 ↑n)
h₂ : ⋃ (n : ℕ), Seminorm.closedBall p 0 ↑n = univ
n : ℕ
x : E
hxn : x ∈ interior {y | ↑p y ≤ ↑n}
hxn' : ↑p x ≤ ↑n
⊢ {y | ↑p y ≤ ↑n + ↑n} ∈ 𝓝 0
[PROOFSTEP]
rw [mem_interior_iff_mem_nhds, ← map_add_left_nhds_zero] at hxn
[GOAL]
case intro.intro
α : Type u_1
ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst✝¹¹ : Nonempty κ
inst✝¹⁰ : NontriviallyNormedField 𝕜₁
inst✝⁹ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst✝⁸ : RingHomIsometric σ₁₂
inst✝⁷ : AddCommGroup E
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : Module 𝕜₂ F
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousConstSMul 𝕜₁ E
inst✝ : BaireSpace E
p : Seminorm 𝕜₁ E
hp : LowerSemicontinuous ↑p
h₁ : ∀ (n : ℕ), IsClosed (Seminorm.closedBall p 0 ↑n)
h₂ : ⋃ (n : ℕ), Seminorm.closedBall p 0 ↑n = univ
n : ℕ
x : E
hxn✝ : {y | ↑p y ≤ ↑n} ∈ 𝓝 x
hxn : {y | ↑p y ≤ ↑n} ∈ map ((fun x x_1 => x + x_1) x) (𝓝 0)
hxn' : ↑p x ≤ ↑n
⊢ {y | ↑p y ≤ ↑n + ↑n} ∈ 𝓝 0
[PROOFSTEP]
filter_upwards [hxn] with y hy
[GOAL]
case h
α : Type u_1
ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst✝¹¹ : Nonempty κ
inst✝¹⁰ : NontriviallyNormedField 𝕜₁
inst✝⁹ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst✝⁸ : RingHomIsometric σ₁₂
inst✝⁷ : AddCommGroup E
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : Module 𝕜₂ F
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousConstSMul 𝕜₁ E
inst✝ : BaireSpace E
p : Seminorm 𝕜₁ E
hp : LowerSemicontinuous ↑p
h₁ : ∀ (n : ℕ), IsClosed (Seminorm.closedBall p 0 ↑n)
h₂ : ⋃ (n : ℕ), Seminorm.closedBall p 0 ↑n = univ
n : ℕ
x : E
hxn✝ : {y | ↑p y ≤ ↑n} ∈ 𝓝 x
hxn : {y | ↑p y ≤ ↑n} ∈ map ((fun x x_1 => x + x_1) x) (𝓝 0)
hxn' : ↑p x ≤ ↑n
y : E
hy : y ∈ (fun x_1 => x + x_1) ⁻¹' {y | ↑p y ≤ ↑n}
⊢ ↑p y ≤ ↑n + ↑n
[PROOFSTEP]
calc
  p y = p (x + y - x) := by rw [add_sub_cancel']
  _ ≤ p (x + y) + p x := (map_sub_le_add _ _ _)
  _ ≤ n + n := add_le_add hy hxn'
[GOAL]
α : Type u_1
ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst✝¹¹ : Nonempty κ
inst✝¹⁰ : NontriviallyNormedField 𝕜₁
inst✝⁹ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst✝⁸ : RingHomIsometric σ₁₂
inst✝⁷ : AddCommGroup E
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : Module 𝕜₂ F
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousConstSMul 𝕜₁ E
inst✝ : BaireSpace E
p : Seminorm 𝕜₁ E
hp : LowerSemicontinuous ↑p
h₁ : ∀ (n : ℕ), IsClosed (Seminorm.closedBall p 0 ↑n)
h₂ : ⋃ (n : ℕ), Seminorm.closedBall p 0 ↑n = univ
n : ℕ
x : E
hxn✝ : {y | ↑p y ≤ ↑n} ∈ 𝓝 x
hxn : {y | ↑p y ≤ ↑n} ∈ map ((fun x x_1 => x + x_1) x) (𝓝 0)
hxn' : ↑p x ≤ ↑n
y : E
hy : y ∈ (fun x_1 => x + x_1) ⁻¹' {y | ↑p y ≤ ↑n}
⊢ ↑p y = ↑p (x + y - x)
[PROOFSTEP]
rw [add_sub_cancel']
[GOAL]
α : Type u_1
ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst✝¹⁴ : Nonempty κ
inst✝¹³ : NontriviallyNormedField 𝕜₁
inst✝¹² : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst✝¹¹ : RingHomIsometric σ₁₂
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜₁ E
inst✝⁷ : Module 𝕜₂ F
inst✝⁶ : UniformSpace E
inst✝⁵ : UniformSpace F
inst✝⁴ : UniformAddGroup E
inst✝³ : UniformAddGroup F
inst✝² : ContinuousSMul 𝕜₁ E
inst✝¹ : ContinuousSMul 𝕜₂ F
inst✝ : BarrelledSpace 𝕜₁ E
𝓕 : ι → E →SL[σ₁₂] F
q : SeminormFamily 𝕜₂ F κ
hq : WithSeminorms q
H : ∀ (k : κ) (x : E), BddAbove (range fun i => ↑(q k) (↑(𝓕 i) x))
⊢ UniformEquicontinuous (FunLike.coe ∘ 𝓕)
[PROOFSTEP]
refine (hq.uniformEquicontinuous_iff_bddAbove_and_continuous_iSup ((toLinearMap) ∘ 𝓕)).mpr ?_
[GOAL]
α : Type u_1
ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst✝¹⁴ : Nonempty κ
inst✝¹³ : NontriviallyNormedField 𝕜₁
inst✝¹² : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst✝¹¹ : RingHomIsometric σ₁₂
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜₁ E
inst✝⁷ : Module 𝕜₂ F
inst✝⁶ : UniformSpace E
inst✝⁵ : UniformSpace F
inst✝⁴ : UniformAddGroup E
inst✝³ : UniformAddGroup F
inst✝² : ContinuousSMul 𝕜₁ E
inst✝¹ : ContinuousSMul 𝕜₂ F
inst✝ : BarrelledSpace 𝕜₁ E
𝓕 : ι → E →SL[σ₁₂] F
q : SeminormFamily 𝕜₂ F κ
hq : WithSeminorms q
H : ∀ (k : κ) (x : E), BddAbove (range fun i => ↑(q k) (↑(𝓕 i) x))
⊢ ∀ (i : κ),
    BddAbove (range fun k => Seminorm.comp (q i) ((toLinearMap ∘ 𝓕) k)) ∧
      Continuous (⨆ (k : ι), ↑(Seminorm.comp (q i) ((toLinearMap ∘ 𝓕) k)))
[PROOFSTEP]
intro k
[GOAL]
α : Type u_1
ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst✝¹⁴ : Nonempty κ
inst✝¹³ : NontriviallyNormedField 𝕜₁
inst✝¹² : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst✝¹¹ : RingHomIsometric σ₁₂
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜₁ E
inst✝⁷ : Module 𝕜₂ F
inst✝⁶ : UniformSpace E
inst✝⁵ : UniformSpace F
inst✝⁴ : UniformAddGroup E
inst✝³ : UniformAddGroup F
inst✝² : ContinuousSMul 𝕜₁ E
inst✝¹ : ContinuousSMul 𝕜₂ F
inst✝ : BarrelledSpace 𝕜₁ E
𝓕 : ι → E →SL[σ₁₂] F
q : SeminormFamily 𝕜₂ F κ
hq : WithSeminorms q
H : ∀ (k : κ) (x : E), BddAbove (range fun i => ↑(q k) (↑(𝓕 i) x))
k : κ
⊢ BddAbove (range fun k_1 => Seminorm.comp (q k) ((toLinearMap ∘ 𝓕) k_1)) ∧
    Continuous (⨆ (k_1 : ι), ↑(Seminorm.comp (q k) ((toLinearMap ∘ 𝓕) k_1)))
[PROOFSTEP]
have : BddAbove (range fun i ↦ (q k).comp (𝓕 i).toLinearMap) :=
  by
  rw [Seminorm.bddAbove_range_iff]
  exact H k
[GOAL]
α : Type u_1
ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst✝¹⁴ : Nonempty κ
inst✝¹³ : NontriviallyNormedField 𝕜₁
inst✝¹² : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst✝¹¹ : RingHomIsometric σ₁₂
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜₁ E
inst✝⁷ : Module 𝕜₂ F
inst✝⁶ : UniformSpace E
inst✝⁵ : UniformSpace F
inst✝⁴ : UniformAddGroup E
inst✝³ : UniformAddGroup F
inst✝² : ContinuousSMul 𝕜₁ E
inst✝¹ : ContinuousSMul 𝕜₂ F
inst✝ : BarrelledSpace 𝕜₁ E
𝓕 : ι → E →SL[σ₁₂] F
q : SeminormFamily 𝕜₂ F κ
hq : WithSeminorms q
H : ∀ (k : κ) (x : E), BddAbove (range fun i => ↑(q k) (↑(𝓕 i) x))
k : κ
⊢ BddAbove (range fun i => Seminorm.comp (q k) ↑(𝓕 i))
[PROOFSTEP]
rw [Seminorm.bddAbove_range_iff]
[GOAL]
α : Type u_1
ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst✝¹⁴ : Nonempty κ
inst✝¹³ : NontriviallyNormedField 𝕜₁
inst✝¹² : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst✝¹¹ : RingHomIsometric σ₁₂
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜₁ E
inst✝⁷ : Module 𝕜₂ F
inst✝⁶ : UniformSpace E
inst✝⁵ : UniformSpace F
inst✝⁴ : UniformAddGroup E
inst✝³ : UniformAddGroup F
inst✝² : ContinuousSMul 𝕜₁ E
inst✝¹ : ContinuousSMul 𝕜₂ F
inst✝ : BarrelledSpace 𝕜₁ E
𝓕 : ι → E →SL[σ₁₂] F
q : SeminormFamily 𝕜₂ F κ
hq : WithSeminorms q
H : ∀ (k : κ) (x : E), BddAbove (range fun i => ↑(q k) (↑(𝓕 i) x))
k : κ
⊢ ∀ (x : E), BddAbove (range fun i => ↑(Seminorm.comp (q k) ↑(𝓕 i)) x)
[PROOFSTEP]
exact H k
[GOAL]
α : Type u_1
ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst✝¹⁴ : Nonempty κ
inst✝¹³ : NontriviallyNormedField 𝕜₁
inst✝¹² : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst✝¹¹ : RingHomIsometric σ₁₂
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜₁ E
inst✝⁷ : Module 𝕜₂ F
inst✝⁶ : UniformSpace E
inst✝⁵ : UniformSpace F
inst✝⁴ : UniformAddGroup E
inst✝³ : UniformAddGroup F
inst✝² : ContinuousSMul 𝕜₁ E
inst✝¹ : ContinuousSMul 𝕜₂ F
inst✝ : BarrelledSpace 𝕜₁ E
𝓕 : ι → E →SL[σ₁₂] F
q : SeminormFamily 𝕜₂ F κ
hq : WithSeminorms q
H : ∀ (k : κ) (x : E), BddAbove (range fun i => ↑(q k) (↑(𝓕 i) x))
k : κ
this : BddAbove (range fun i => Seminorm.comp (q k) ↑(𝓕 i))
⊢ BddAbove (range fun k_1 => Seminorm.comp (q k) ((toLinearMap ∘ 𝓕) k_1)) ∧
    Continuous (⨆ (k_1 : ι), ↑(Seminorm.comp (q k) ((toLinearMap ∘ 𝓕) k_1)))
[PROOFSTEP]
exact ⟨this, Seminorm.continuous_iSup _ (fun i ↦ (hq.continuous_seminorm k).comp (𝓕 i).continuous) this⟩
[GOAL]
α : Type u_1
ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst✝¹⁷ : Nonempty κ
inst✝¹⁶ : NontriviallyNormedField 𝕜₁
inst✝¹⁵ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst✝¹⁴ : RingHomIsometric σ₁₂
inst✝¹³ : AddCommGroup E
inst✝¹² : AddCommGroup F
inst✝¹¹ : Module 𝕜₁ E
inst✝¹⁰ : Module 𝕜₂ F
inst✝⁹ : UniformSpace E
inst✝⁸ : UniformSpace F
inst✝⁷ : UniformAddGroup E
inst✝⁶ : UniformAddGroup F
inst✝⁵ : ContinuousSMul 𝕜₁ E
inst✝⁴ : ContinuousSMul 𝕜₂ F
inst✝³ : BarrelledSpace 𝕜₁ E
𝓕 : ι → E →SL[σ₁₂] F
q : SeminormFamily 𝕜₂ F κ
hq : WithSeminorms q
inst✝² : T2Space F
l : Filter α
inst✝¹ : IsCountablyGenerated l
inst✝ : NeBot l
g : α → E →SL[σ₁₂] F
f : E → F
h : Tendsto (fun n x => ↑(g n) x) l (𝓝 f)
⊢ Continuous (linearMapOfTendsto f (fun a => ↑(g a)) h).toAddHom.toFun
[PROOFSTEP]
rcases l.exists_seq_tendsto with
  ⟨u, hu⟩
    -- We claim that the limit is continuous because it's a limit of an equicontinuous family.
        -- By the Banach-Steinhaus theorem, this equicontinuity will follow from pointwise boundedness.
[GOAL]
case intro
α : Type u_1
ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst✝¹⁷ : Nonempty κ
inst✝¹⁶ : NontriviallyNormedField 𝕜₁
inst✝¹⁵ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst✝¹⁴ : RingHomIsometric σ₁₂
inst✝¹³ : AddCommGroup E
inst✝¹² : AddCommGroup F
inst✝¹¹ : Module 𝕜₁ E
inst✝¹⁰ : Module 𝕜₂ F
inst✝⁹ : UniformSpace E
inst✝⁸ : UniformSpace F
inst✝⁷ : UniformAddGroup E
inst✝⁶ : UniformAddGroup F
inst✝⁵ : ContinuousSMul 𝕜₁ E
inst✝⁴ : ContinuousSMul 𝕜₂ F
inst✝³ : BarrelledSpace 𝕜₁ E
𝓕 : ι → E →SL[σ₁₂] F
q : SeminormFamily 𝕜₂ F κ
hq : WithSeminorms q
inst✝² : T2Space F
l : Filter α
inst✝¹ : IsCountablyGenerated l
inst✝ : NeBot l
g : α → E →SL[σ₁₂] F
f : E → F
h : Tendsto (fun n x => ↑(g n) x) l (𝓝 f)
u : ℕ → α
hu : Tendsto u atTop l
⊢ Continuous (linearMapOfTendsto f (fun a => ↑(g a)) h).toAddHom.toFun
[PROOFSTEP]
refine (h.comp hu).continuous_of_equicontinuous_at (hq.banach_steinhaus ?_).equicontinuous
[GOAL]
case intro
α : Type u_1
ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst✝¹⁷ : Nonempty κ
inst✝¹⁶ : NontriviallyNormedField 𝕜₁
inst✝¹⁵ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst✝¹⁴ : RingHomIsometric σ₁₂
inst✝¹³ : AddCommGroup E
inst✝¹² : AddCommGroup F
inst✝¹¹ : Module 𝕜₁ E
inst✝¹⁰ : Module 𝕜₂ F
inst✝⁹ : UniformSpace E
inst✝⁸ : UniformSpace F
inst✝⁷ : UniformAddGroup E
inst✝⁶ : UniformAddGroup F
inst✝⁵ : ContinuousSMul 𝕜₁ E
inst✝⁴ : ContinuousSMul 𝕜₂ F
inst✝³ : BarrelledSpace 𝕜₁ E
𝓕 : ι → E →SL[σ₁₂] F
q : SeminormFamily 𝕜₂ F κ
hq : WithSeminorms q
inst✝² : T2Space F
l : Filter α
inst✝¹ : IsCountablyGenerated l
inst✝ : NeBot l
g : α → E →SL[σ₁₂] F
f : E → F
h : Tendsto (fun n x => ↑(g n) x) l (𝓝 f)
u : ℕ → α
hu : Tendsto u atTop l
⊢ ∀ (k : κ) (x : E), BddAbove (range fun i => ↑(q k) (↑(g (u i)) x))
[PROOFSTEP]
intro k x
[GOAL]
case intro
α : Type u_1
ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst✝¹⁷ : Nonempty κ
inst✝¹⁶ : NontriviallyNormedField 𝕜₁
inst✝¹⁵ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst✝¹⁴ : RingHomIsometric σ₁₂
inst✝¹³ : AddCommGroup E
inst✝¹² : AddCommGroup F
inst✝¹¹ : Module 𝕜₁ E
inst✝¹⁰ : Module 𝕜₂ F
inst✝⁹ : UniformSpace E
inst✝⁸ : UniformSpace F
inst✝⁷ : UniformAddGroup E
inst✝⁶ : UniformAddGroup F
inst✝⁵ : ContinuousSMul 𝕜₁ E
inst✝⁴ : ContinuousSMul 𝕜₂ F
inst✝³ : BarrelledSpace 𝕜₁ E
𝓕 : ι → E →SL[σ₁₂] F
q : SeminormFamily 𝕜₂ F κ
hq : WithSeminorms q
inst✝² : T2Space F
l : Filter α
inst✝¹ : IsCountablyGenerated l
inst✝ : NeBot l
g : α → E →SL[σ₁₂] F
f : E → F
h : Tendsto (fun n x => ↑(g n) x) l (𝓝 f)
u : ℕ → α
hu : Tendsto u atTop l
k : κ
x : E
⊢ BddAbove (range fun i => ↑(q k) (↑(g (u i)) x))
[PROOFSTEP]
rw [tendsto_pi_nhds] at h
[GOAL]
case intro
α : Type u_1
ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst✝¹⁷ : Nonempty κ
inst✝¹⁶ : NontriviallyNormedField 𝕜₁
inst✝¹⁵ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst✝¹⁴ : RingHomIsometric σ₁₂
inst✝¹³ : AddCommGroup E
inst✝¹² : AddCommGroup F
inst✝¹¹ : Module 𝕜₁ E
inst✝¹⁰ : Module 𝕜₂ F
inst✝⁹ : UniformSpace E
inst✝⁸ : UniformSpace F
inst✝⁷ : UniformAddGroup E
inst✝⁶ : UniformAddGroup F
inst✝⁵ : ContinuousSMul 𝕜₁ E
inst✝⁴ : ContinuousSMul 𝕜₂ F
inst✝³ : BarrelledSpace 𝕜₁ E
𝓕 : ι → E →SL[σ₁₂] F
q : SeminormFamily 𝕜₂ F κ
hq : WithSeminorms q
inst✝² : T2Space F
l : Filter α
inst✝¹ : IsCountablyGenerated l
inst✝ : NeBot l
g : α → E →SL[σ₁₂] F
f : E → F
h : ∀ (x : E), Tendsto (fun i => ↑(g i) x) l (𝓝 (f x))
u : ℕ → α
hu : Tendsto u atTop l
k : κ
x : E
⊢ BddAbove (range fun i => ↑(q k) (↑(g (u i)) x))
[PROOFSTEP]
exact (((hq.continuous_seminorm k).tendsto _).comp <| (h x).comp hu).bddAbove_range


[GOAL]
X Y : SemiNormedGroupCat₁
f : X ⟶ Y
⊢ f ≫
      mkHom (AddSubgroup.normedMk (NormedAddGroupHom.range ↑f))
        (_ : ∀ (m : ↑Y), ‖↑(AddSubgroup.normedMk (NormedAddGroupHom.range ↑f)) m‖ ≤ ‖m‖) =
    0 ≫
      mkHom (AddSubgroup.normedMk (NormedAddGroupHom.range ↑f))
        (_ : ∀ (m : ↑Y), ‖↑(AddSubgroup.normedMk (NormedAddGroupHom.range ↑f)) m‖ ≤ ‖m‖)
[PROOFSTEP]
ext x
[GOAL]
case w.h
X Y : SemiNormedGroupCat₁
f : X ⟶ Y
x : ↑X
⊢ ↑(f ≫
          mkHom (AddSubgroup.normedMk (NormedAddGroupHom.range ↑f))
            (_ : ∀ (m : ↑Y), ‖↑(AddSubgroup.normedMk (NormedAddGroupHom.range ↑f)) m‖ ≤ ‖m‖))
      x =
    ↑(0 ≫
          mkHom (AddSubgroup.normedMk (NormedAddGroupHom.range ↑f))
            (_ : ∀ (m : ↑Y), ‖↑(AddSubgroup.normedMk (NormedAddGroupHom.range ↑f)) m‖ ≤ ‖m‖))
      x
[PROOFSTEP]
rw [Limits.zero_comp, comp_apply, SemiNormedGroupCat₁.mkHom_apply, SemiNormedGroupCat₁.zero_apply, ←
  NormedAddGroupHom.mem_ker, f.1.range.ker_normedMk, f.1.mem_range]
[GOAL]
case w.h
X Y : SemiNormedGroupCat₁
f : X ⟶ Y
x : ↑X
⊢ ∃ w, ↑↑f w = ↑f x
[PROOFSTEP]
use x
[GOAL]
case h
X Y : SemiNormedGroupCat₁
f : X ⟶ Y
x : ↑X
⊢ ↑↑f x = ↑f x
[PROOFSTEP]
rfl
[GOAL]
X Y : SemiNormedGroupCat₁
f : X ⟶ Y
s : CokernelCofork f
⊢ (cokernelCocone f).pt ⟶ s.pt
[PROOFSTEP]
fconstructor
  -- The lift itself:
[GOAL]
case val
X Y : SemiNormedGroupCat₁
f : X ⟶ Y
s : CokernelCofork f
⊢ NormedAddGroupHom ↑(cokernelCocone f).pt ↑s.pt
[PROOFSTEP]
apply NormedAddGroupHom.lift _ s.π.1
[GOAL]
case val
X Y : SemiNormedGroupCat₁
f : X ⟶ Y
s : CokernelCofork f
⊢ ∀ (s_1 : ↑((parallelPair f 0).obj WalkingParallelPair.one)), s_1 ∈ NormedAddGroupHom.range ↑f → ↑↑(Cofork.π s) s_1 = 0
[PROOFSTEP]
rintro _ ⟨b, rfl⟩
[GOAL]
case val.intro
X Y : SemiNormedGroupCat₁
f : X ⟶ Y
s : CokernelCofork f
b : ↑X
⊢ ↑↑(Cofork.π s) (↑(NormedAddGroupHom.toAddMonoidHom ↑f) b) = 0
[PROOFSTEP]
change (f ≫ s.π) b = 0
[GOAL]
case val.intro
X Y : SemiNormedGroupCat₁
f : X ⟶ Y
s : CokernelCofork f
b : ↑X
⊢ ↑(f ≫ Cofork.π s) b = 0
[PROOFSTEP]
simp
  -- The lift has norm at most one:
[GOAL]
case property
X Y : SemiNormedGroupCat₁
f : X ⟶ Y
s : CokernelCofork f
⊢ NormedAddGroupHom.NormNoninc
    (NormedAddGroupHom.lift (NormedAddGroupHom.range ↑f) ↑(Cofork.π s)
      (_ :
        ∀ (s_1 : ↑((parallelPair f 0).obj WalkingParallelPair.one)),
          s_1 ∈ NormedAddGroupHom.range ↑f → ↑↑(Cofork.π s) s_1 = 0))
[PROOFSTEP]
exact NormedAddGroupHom.lift_normNoninc _ _ _ s.π.2
[GOAL]
X✝ Y✝ : SemiNormedGroupCat₁
f : X✝ ⟶ Y✝
s : CokernelCofork f
⊢ Cofork.π (cokernelCocone f) ≫ cokernelLift f s = Cofork.π s
[PROOFSTEP]
ext
[GOAL]
case w.h
X✝ Y✝ : SemiNormedGroupCat₁
f : X✝ ⟶ Y✝
s : CokernelCofork f
x✝ : ↑((parallelPair f 0).obj WalkingParallelPair.one)
⊢ ↑(Cofork.π (cokernelCocone f) ≫ cokernelLift f s) x✝ = ↑(Cofork.π s) x✝
[PROOFSTEP]
apply NormedAddGroupHom.lift_mk f.1.range
[GOAL]
case w.h.hf
X✝ Y✝ : SemiNormedGroupCat₁
f : X✝ ⟶ Y✝
s : CokernelCofork f
x✝ : ↑((parallelPair f 0).obj WalkingParallelPair.one)
⊢ ∀ (s_1 : ↑Y✝), s_1 ∈ NormedAddGroupHom.range ↑f → ↑↑(Cofork.π s) s_1 = 0
[PROOFSTEP]
rintro _ ⟨b, rfl⟩
[GOAL]
case w.h.hf.intro
X✝ Y✝ : SemiNormedGroupCat₁
f : X✝ ⟶ Y✝
s : CokernelCofork f
x✝ : ↑((parallelPair f 0).obj WalkingParallelPair.one)
b : ↑X✝
⊢ ↑↑(Cofork.π s) (↑(NormedAddGroupHom.toAddMonoidHom ↑f) b) = 0
[PROOFSTEP]
change (f ≫ s.π) b = 0
[GOAL]
case w.h.hf.intro
X✝ Y✝ : SemiNormedGroupCat₁
f : X✝ ⟶ Y✝
s : CokernelCofork f
x✝ : ↑((parallelPair f 0).obj WalkingParallelPair.one)
b : ↑X✝
⊢ ↑(f ≫ Cofork.π s) b = 0
[PROOFSTEP]
simp
[GOAL]
⊢ HasCokernels SemiNormedGroupCat₁
[PROOFSTEP]
infer_instance
[GOAL]
V W : SemiNormedGroupCat
f g : V ⟶ W
⊢ NormedAddGroupHom.incl (NormedAddGroupHom.ker (f - g)) ≫ f =
    NormedAddGroupHom.incl (NormedAddGroupHom.ker (f - g)) ≫ g
[PROOFSTEP]
change NormedAddGroupHom V W at f g
[GOAL]
V W : SemiNormedGroupCat
f g : NormedAddGroupHom ↑V ↑W
⊢ NormedAddGroupHom.incl (NormedAddGroupHom.ker (f - g)) ≫ f =
    NormedAddGroupHom.incl (NormedAddGroupHom.ker (f - g)) ≫ g
[PROOFSTEP]
ext v
[GOAL]
case h
V W : SemiNormedGroupCat
f g : NormedAddGroupHom ↑V ↑W
v : ↑(of { x // x ∈ NormedAddGroupHom.ker (f - g) })
⊢ ↑(NormedAddGroupHom.incl (NormedAddGroupHom.ker (f - g)) ≫ f) v =
    ↑(NormedAddGroupHom.incl (NormedAddGroupHom.ker (f - g)) ≫ g) v
[PROOFSTEP]
have : v.1 ∈ (f - g).ker := v.2
[GOAL]
case h
V W : SemiNormedGroupCat
f g : NormedAddGroupHom ↑V ↑W
v : ↑(of { x // x ∈ NormedAddGroupHom.ker (f - g) })
this : ↑v ∈ NormedAddGroupHom.ker (f - g)
⊢ ↑(NormedAddGroupHom.incl (NormedAddGroupHom.ker (f - g)) ≫ f) v =
    ↑(NormedAddGroupHom.incl (NormedAddGroupHom.ker (f - g)) ≫ g) v
[PROOFSTEP]
simpa only [NormedAddGroupHom.incl_apply, Pi.zero_apply, coe_comp, NormedAddGroupHom.coe_zero,
  NormedAddGroupHom.mem_ker, NormedAddGroupHom.coe_sub, Pi.sub_apply, sub_eq_zero] using this
[GOAL]
V W : SemiNormedGroupCat
f g : V ⟶ W
c : Fork f g
⊢ ↑(↑NormedAddGroupHom.compHom (f - g)) (Fork.ι c) = 0
[PROOFSTEP]
rw [AddMonoidHom.map_sub, AddMonoidHom.sub_apply, sub_eq_zero]
[GOAL]
V W : SemiNormedGroupCat
f g : V ⟶ W
c : Fork f g
⊢ ↑(↑NormedAddGroupHom.compHom f) (Fork.ι c) = ↑(↑NormedAddGroupHom.compHom g) (Fork.ι c)
[PROOFSTEP]
exact c.condition
[GOAL]
V W : SemiNormedGroupCat
f g✝ : V ⟶ W
c : Fork f g✝
g : c.pt ⟶ (fork f g✝).pt
h : g ≫ Fork.ι (fork f g✝) = Fork.ι c
⊢ g =
    (fun c =>
        NormedAddGroupHom.ker.lift (Fork.ι c) (f - g✝) (_ : ↑(↑NormedAddGroupHom.compHom (f - g✝)) (Fork.ι c) = 0))
      c
[PROOFSTEP]
ext x
[GOAL]
case h
V W : SemiNormedGroupCat
f g✝ : V ⟶ W
c : Fork f g✝
g : c.pt ⟶ (fork f g✝).pt
h : g ≫ Fork.ι (fork f g✝) = Fork.ι c
x : ↑c.pt
⊢ ↑g x =
    ↑((fun c =>
            NormedAddGroupHom.ker.lift (Fork.ι c) (f - g✝) (_ : ↑(↑NormedAddGroupHom.compHom (f - g✝)) (Fork.ι c) = 0))
          c)
      x
[PROOFSTEP]
dsimp
[GOAL]
case h
V W : SemiNormedGroupCat
f g✝ : V ⟶ W
c : Fork f g✝
g : c.pt ⟶ (fork f g✝).pt
h : g ≫ Fork.ι (fork f g✝) = Fork.ι c
x : ↑c.pt
⊢ ↑g x =
    ↑(NormedAddGroupHom.ker.lift (Fork.ι c) (f - g✝)
          (_ : ↑(↑NormedAddGroupHom.compHom f) (Fork.ι c) - ↑(↑NormedAddGroupHom.compHom g✝) (Fork.ι c) = 0))
      x
[PROOFSTEP]
simp_rw [← h]
[GOAL]
case h
V W : SemiNormedGroupCat
f g✝ : V ⟶ W
c : Fork f g✝
g : c.pt ⟶ (fork f g✝).pt
h : g ≫ Fork.ι (fork f g✝) = Fork.ι c
x : ↑c.pt
⊢ ↑g x =
    ↑(NormedAddGroupHom.ker.lift (g ≫ Fork.ι (fork f g✝)) (f - g✝)
          (_ : NormedAddGroupHom.comp (f - g✝) (g ≫ Fork.ι (fork f g✝)) = 0))
      x
[PROOFSTEP]
rfl
[GOAL]
X Y : SemiNormedGroupCat
f : X ⟶ Y
⊢ f ≫ AddSubgroup.normedMk (NormedAddGroupHom.range f) = 0 ≫ AddSubgroup.normedMk (NormedAddGroupHom.range f)
[PROOFSTEP]
ext
[GOAL]
case h
X Y : SemiNormedGroupCat
f : X ⟶ Y
x✝ : ↑X
⊢ ↑(f ≫ AddSubgroup.normedMk (NormedAddGroupHom.range f)) x✝ =
    ↑(0 ≫ AddSubgroup.normedMk (NormedAddGroupHom.range f)) x✝
[PROOFSTEP]
simp only [comp_apply, Limits.zero_comp]
  -- porting note: `simp` not firing on the below
[GOAL]
case h
X Y : SemiNormedGroupCat
f : X ⟶ Y
x✝ : ↑X
⊢ ↑(f ≫ AddSubgroup.normedMk (NormedAddGroupHom.range f)) x✝ = ↑0 x✝
[PROOFSTEP]
rw [comp_apply, NormedAddGroupHom.zero_apply]
  -- porting note: Lean 3 didn't need this instance
[GOAL]
case h
X Y : SemiNormedGroupCat
f : X ⟶ Y
x✝ : ↑X
⊢ ↑(AddSubgroup.normedMk (NormedAddGroupHom.range f)) (↑f x✝) = 0
[PROOFSTEP]
letI : SeminormedAddCommGroup ((forget SemiNormedGroupCat).obj Y) :=
  (inferInstance : SeminormedAddCommGroup Y)
    -- porting note: again simp doesn't seem to be firing in the below line
[GOAL]
case h
X Y : SemiNormedGroupCat
f : X ⟶ Y
x✝ : ↑X
this : SeminormedAddCommGroup ((forget SemiNormedGroupCat).obj Y) := inferInstance
⊢ ↑(AddSubgroup.normedMk (NormedAddGroupHom.range f)) (↑f x✝) = 0
[PROOFSTEP]
rw [← NormedAddGroupHom.mem_ker, f.range.ker_normedMk, f.mem_range]
[GOAL]
case h
X Y : SemiNormedGroupCat
f : X ⟶ Y
x✝ : ↑X
this : SeminormedAddCommGroup ((forget SemiNormedGroupCat).obj Y) := inferInstance
⊢ ∃ w, ↑f w = ↑f x✝
[PROOFSTEP]
simp only [exists_apply_eq_apply]
[GOAL]
X Y : SemiNormedGroupCat
f : X ⟶ Y
s : CokernelCofork f
⊢ ∀ (s_1 : ↑Y), s_1 ∈ NormedAddGroupHom.range f → ↑(Cofork.π s) s_1 = 0
[PROOFSTEP]
rintro _ ⟨b, rfl⟩
[GOAL]
case intro
X Y : SemiNormedGroupCat
f : X ⟶ Y
s : CokernelCofork f
b : ↑X
⊢ ↑(Cofork.π s) (↑(NormedAddGroupHom.toAddMonoidHom f) b) = 0
[PROOFSTEP]
change (f ≫ s.π) b = 0
[GOAL]
case intro
X Y : SemiNormedGroupCat
f : X ⟶ Y
s : CokernelCofork f
b : ↑X
⊢ ↑(f ≫ Cofork.π s) b = 0
[PROOFSTEP]
simp
[GOAL]
X Y : SemiNormedGroupCat
f : X ⟶ Y
s : CokernelCofork f
⊢ Cofork.π (cokernelCocone f) ≫ cokernelLift f s = Cofork.π s
[PROOFSTEP]
ext
[GOAL]
case h
X Y : SemiNormedGroupCat
f : X ⟶ Y
s : CokernelCofork f
x✝ : ↑((parallelPair f 0).obj WalkingParallelPair.one)
⊢ ↑(Cofork.π (cokernelCocone f) ≫ cokernelLift f s) x✝ = ↑(Cofork.π s) x✝
[PROOFSTEP]
apply NormedAddGroupHom.lift_mk f.range
[GOAL]
case h.hf
X Y : SemiNormedGroupCat
f : X ⟶ Y
s : CokernelCofork f
x✝ : ↑((parallelPair f 0).obj WalkingParallelPair.one)
⊢ ∀ (s_1 : ↑Y), s_1 ∈ NormedAddGroupHom.range f → ↑(Cofork.π s) s_1 = 0
[PROOFSTEP]
rintro _ ⟨b, rfl⟩
[GOAL]
case h.hf.intro
X Y : SemiNormedGroupCat
f : X ⟶ Y
s : CokernelCofork f
x✝ : ↑((parallelPair f 0).obj WalkingParallelPair.one)
b : ↑X
⊢ ↑(Cofork.π s) (↑(NormedAddGroupHom.toAddMonoidHom f) b) = 0
[PROOFSTEP]
change (f ≫ s.π) b = 0
[GOAL]
case h.hf.intro
X Y : SemiNormedGroupCat
f : X ⟶ Y
s : CokernelCofork f
x✝ : ↑((parallelPair f 0).obj WalkingParallelPair.one)
b : ↑X
⊢ ↑(f ≫ Cofork.π s) b = 0
[PROOFSTEP]
simp
[GOAL]
⊢ HasCokernels SemiNormedGroupCat
[PROOFSTEP]
infer_instance
[GOAL]
X Y Z : SemiNormedGroupCat
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
⊢ f ≫ g = 0 ≫ g
[PROOFSTEP]
simp [w]
[GOAL]
X Y : SemiNormedGroupCat
f : X ⟶ Y
⊢ f ≫ explicitCokernelπ f = 0
[PROOFSTEP]
convert (cokernelCocone f).w WalkingParallelPairHom.left
[GOAL]
case h.e'_3.h
X Y : SemiNormedGroupCat
f : X ⟶ Y
e_1✝ :
  (X ⟶ explicitCokernel f) =
    ((parallelPair f 0).obj WalkingParallelPair.zero ⟶
      ((Functor.const WalkingParallelPair).obj (cokernelCocone f).pt).obj WalkingParallelPair.one)
⊢ 0 = NatTrans.app (cokernelCocone f).ι WalkingParallelPair.zero
[PROOFSTEP]
simp
[GOAL]
X Y : SemiNormedGroupCat
f : X ⟶ Y
x : ↑X
⊢ ↑(f ≫ explicitCokernelπ f) x = 0
[PROOFSTEP]
rw [comp_explicitCokernelπ]
[GOAL]
X Y : SemiNormedGroupCat
f : X ⟶ Y
x : ↑X
⊢ ↑0 x = 0
[PROOFSTEP]
rfl
[GOAL]
X Y Z : SemiNormedGroupCat
f : X ⟶ Y
g : Y ⟶ Z
cond : f ≫ g = 0
x : ↑Y
⊢ ↑(explicitCokernelπ f ≫ explicitCokernelDesc cond) x = ↑g x
[PROOFSTEP]
rw [explicitCokernelπ_desc]
[GOAL]
X Y Z : SemiNormedGroupCat
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
e : explicitCokernel f ⟶ Z
he : explicitCokernelπ f ≫ e = g
⊢ e = explicitCokernelDesc w
[PROOFSTEP]
apply (isColimitCokernelCocone f).uniq (Cofork.ofπ g (by simp [w]))
[GOAL]
X Y Z : SemiNormedGroupCat
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
e : explicitCokernel f ⟶ Z
he : explicitCokernelπ f ≫ e = g
⊢ f ≫ g = 0 ≫ g
[PROOFSTEP]
simp [w]
[GOAL]
case x
X Y Z : SemiNormedGroupCat
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
e : explicitCokernel f ⟶ Z
he : explicitCokernelπ f ≫ e = g
⊢ ∀ (j : WalkingParallelPair),
    NatTrans.app (cokernelCocone f).ι j ≫ e = NatTrans.app (Cofork.ofπ g (_ : f ≫ g = 0 ≫ g)).ι j
[PROOFSTEP]
rintro (_ | _)
[GOAL]
case x.zero
X Y Z : SemiNormedGroupCat
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
e : explicitCokernel f ⟶ Z
he : explicitCokernelπ f ≫ e = g
⊢ NatTrans.app (cokernelCocone f).ι WalkingParallelPair.zero ≫ e =
    NatTrans.app (Cofork.ofπ g (_ : f ≫ g = 0 ≫ g)).ι WalkingParallelPair.zero
[PROOFSTEP]
convert w.symm
[GOAL]
case h.e'_2.h
X Y Z : SemiNormedGroupCat
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
e : explicitCokernel f ⟶ Z
he : explicitCokernelπ f ≫ e = g
e_1✝ : ((parallelPair f 0).obj WalkingParallelPair.zero ⟶ (Cofork.ofπ g (_ : f ≫ g = 0 ≫ g)).pt) = (X ⟶ Z)
⊢ NatTrans.app (cokernelCocone f).ι WalkingParallelPair.zero ≫ e = 0
[PROOFSTEP]
simp
[GOAL]
case x.one
X Y Z : SemiNormedGroupCat
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
e : explicitCokernel f ⟶ Z
he : explicitCokernelπ f ≫ e = g
⊢ NatTrans.app (cokernelCocone f).ι WalkingParallelPair.one ≫ e =
    NatTrans.app (Cofork.ofπ g (_ : f ≫ g = 0 ≫ g)).ι WalkingParallelPair.one
[PROOFSTEP]
exact he
[GOAL]
X Y Z W : SemiNormedGroupCat
f : X ⟶ Y
g : Y ⟶ Z
h : Z ⟶ W
cond' : f ≫ g = 0
⊢ f ≫ g ≫ h = 0
[PROOFSTEP]
rw [← CategoryTheory.Category.assoc, cond', Limits.zero_comp]
[GOAL]
X Y Z W : SemiNormedGroupCat
f : X ⟶ Y
g : Y ⟶ Z
h : Z ⟶ W
cond' : f ≫ g = 0
⊢ explicitCokernelDesc cond' ≫ h = explicitCokernelDesc (_ : f ≫ g ≫ h = 0)
[PROOFSTEP]
refine' explicitCokernelDesc_unique _ _ _
[GOAL]
X Y Z W : SemiNormedGroupCat
f : X ⟶ Y
g : Y ⟶ Z
h : Z ⟶ W
cond' : f ≫ g = 0
⊢ explicitCokernelπ f ≫ explicitCokernelDesc cond' ≫ h = g ≫ h
[PROOFSTEP]
rw [← CategoryTheory.Category.assoc, explicitCokernelπ_desc]
[GOAL]
X Y Z : SemiNormedGroupCat
f : X ⟶ Y
e₁ e₂ : explicitCokernel f ⟶ Z
h : explicitCokernelπ f ≫ e₁ = explicitCokernelπ f ≫ e₂
⊢ e₁ = e₂
[PROOFSTEP]
let g : Y ⟶ Z := explicitCokernelπ f ≫ e₂
[GOAL]
X Y Z : SemiNormedGroupCat
f : X ⟶ Y
e₁ e₂ : explicitCokernel f ⟶ Z
h : explicitCokernelπ f ≫ e₁ = explicitCokernelπ f ≫ e₂
g : Y ⟶ Z := explicitCokernelπ f ≫ e₂
⊢ e₁ = e₂
[PROOFSTEP]
have w : f ≫ g = 0 := by simp
[GOAL]
X Y Z : SemiNormedGroupCat
f : X ⟶ Y
e₁ e₂ : explicitCokernel f ⟶ Z
h : explicitCokernelπ f ≫ e₁ = explicitCokernelπ f ≫ e₂
g : Y ⟶ Z := explicitCokernelπ f ≫ e₂
⊢ f ≫ g = 0
[PROOFSTEP]
simp
[GOAL]
X Y Z : SemiNormedGroupCat
f : X ⟶ Y
e₁ e₂ : explicitCokernel f ⟶ Z
h : explicitCokernelπ f ≫ e₁ = explicitCokernelπ f ≫ e₂
g : Y ⟶ Z := explicitCokernelπ f ≫ e₂
w : f ≫ g = 0
⊢ e₁ = e₂
[PROOFSTEP]
have : e₂ = explicitCokernelDesc w := by apply explicitCokernelDesc_unique; rfl
[GOAL]
X Y Z : SemiNormedGroupCat
f : X ⟶ Y
e₁ e₂ : explicitCokernel f ⟶ Z
h : explicitCokernelπ f ≫ e₁ = explicitCokernelπ f ≫ e₂
g : Y ⟶ Z := explicitCokernelπ f ≫ e₂
w : f ≫ g = 0
⊢ e₂ = explicitCokernelDesc w
[PROOFSTEP]
apply explicitCokernelDesc_unique
[GOAL]
case he
X Y Z : SemiNormedGroupCat
f : X ⟶ Y
e₁ e₂ : explicitCokernel f ⟶ Z
h : explicitCokernelπ f ≫ e₁ = explicitCokernelπ f ≫ e₂
g : Y ⟶ Z := explicitCokernelπ f ≫ e₂
w : f ≫ g = 0
⊢ explicitCokernelπ f ≫ e₂ = g
[PROOFSTEP]
rfl
[GOAL]
X Y Z : SemiNormedGroupCat
f : X ⟶ Y
e₁ e₂ : explicitCokernel f ⟶ Z
h : explicitCokernelπ f ≫ e₁ = explicitCokernelπ f ≫ e₂
g : Y ⟶ Z := explicitCokernelπ f ≫ e₂
w : f ≫ g = 0
this : e₂ = explicitCokernelDesc w
⊢ e₁ = e₂
[PROOFSTEP]
rw [this]
[GOAL]
X Y Z : SemiNormedGroupCat
f : X ⟶ Y
e₁ e₂ : explicitCokernel f ⟶ Z
h : explicitCokernelπ f ≫ e₁ = explicitCokernelπ f ≫ e₂
g : Y ⟶ Z := explicitCokernelπ f ≫ e₂
w : f ≫ g = 0
this : e₂ = explicitCokernelDesc w
⊢ e₁ = explicitCokernelDesc w
[PROOFSTEP]
apply explicitCokernelDesc_unique
[GOAL]
case he
X Y Z : SemiNormedGroupCat
f : X ⟶ Y
e₁ e₂ : explicitCokernel f ⟶ Z
h : explicitCokernelπ f ≫ e₁ = explicitCokernelπ f ≫ e₂
g : Y ⟶ Z := explicitCokernelπ f ≫ e₂
w : f ≫ g = 0
this : e₂ = explicitCokernelDesc w
⊢ explicitCokernelπ f ≫ e₁ = g
[PROOFSTEP]
exact h
[GOAL]
X Y : SemiNormedGroupCat
f : X ⟶ Y
⊢ Epi (explicitCokernelπ f)
[PROOFSTEP]
constructor
[GOAL]
case left_cancellation
X Y : SemiNormedGroupCat
f : X ⟶ Y
⊢ ∀ {Z : SemiNormedGroupCat} (g h : explicitCokernel f ⟶ Z), explicitCokernelπ f ≫ g = explicitCokernelπ f ≫ h → g = h
[PROOFSTEP]
intro Z g h H
[GOAL]
case left_cancellation
X Y : SemiNormedGroupCat
f : X ⟶ Y
Z : SemiNormedGroupCat
g h : explicitCokernel f ⟶ Z
H : explicitCokernelπ f ≫ g = explicitCokernelπ f ≫ h
⊢ g = h
[PROOFSTEP]
ext x
[GOAL]
case left_cancellation.h.h
X Y : SemiNormedGroupCat
f : X ⟶ Y
Z : SemiNormedGroupCat
g h : explicitCokernel f ⟶ Z
H : explicitCokernelπ f ≫ g = explicitCokernelπ f ≫ h
x : ↑Y
⊢ ↑(explicitCokernelπ f ≫ g) x = ↑(explicitCokernelπ f ≫ h) x
[PROOFSTEP]
rw [H]
[GOAL]
X Y Z : SemiNormedGroupCat
f : X ⟶ Y
g : Y ⟶ Z
cond : f ≫ g = 0
hg : NormedAddGroupHom.NormNoninc g
⊢ NormedAddGroupHom.NormNoninc (explicitCokernelDesc cond)
[PROOFSTEP]
refine' NormedAddGroupHom.NormNoninc.normNoninc_iff_norm_le_one.2 _
[GOAL]
X Y Z : SemiNormedGroupCat
f : X ⟶ Y
g : Y ⟶ Z
cond : f ≫ g = 0
hg : NormedAddGroupHom.NormNoninc g
⊢ ‖explicitCokernelDesc cond‖ ≤ 1
[PROOFSTEP]
rw [← NNReal.coe_one]
[GOAL]
X Y Z : SemiNormedGroupCat
f : X ⟶ Y
g : Y ⟶ Z
cond : f ≫ g = 0
hg : NormedAddGroupHom.NormNoninc g
⊢ ‖explicitCokernelDesc cond‖ ≤ ↑1
[PROOFSTEP]
exact explicitCokernelDesc_norm_le_of_norm_le cond 1 (NormedAddGroupHom.NormNoninc.normNoninc_iff_norm_le_one.1 hg)
[GOAL]
X Y Z W : SemiNormedGroupCat
f : X ⟶ Y
g : Y ⟶ Z
h : Z ⟶ W
cond : f ≫ g = 0
cond2 : g ≫ h = 0
⊢ explicitCokernelDesc cond ≫ h = 0
[PROOFSTEP]
rw [← cancel_epi (explicitCokernelπ f), ← Category.assoc, explicitCokernelπ_desc]
[GOAL]
X Y Z W : SemiNormedGroupCat
f : X ⟶ Y
g : Y ⟶ Z
h : Z ⟶ W
cond : f ≫ g = 0
cond2 : g ≫ h = 0
⊢ g ≫ h = explicitCokernelπ f ≫ 0
[PROOFSTEP]
simp [cond2]
[GOAL]
X Y : SemiNormedGroupCat
f : X ⟶ Y
⊢ explicitCokernelπ f ≫ (explicitCokernelIso f).hom = cokernel.π f
[PROOFSTEP]
simp [explicitCokernelπ, explicitCokernelIso, IsColimit.coconePointUniqueUpToIso]
[GOAL]
X Y : SemiNormedGroupCat
f : X ⟶ Y
⊢ cokernel.π f ≫ (explicitCokernelIso f).inv = explicitCokernelπ f
[PROOFSTEP]
simp [explicitCokernelπ, explicitCokernelIso]
[GOAL]
X Y Z : SemiNormedGroupCat
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
⊢ (explicitCokernelIso f).hom ≫ cokernel.desc f g w = explicitCokernelDesc w
[PROOFSTEP]
ext1
[GOAL]
case h
X Y Z : SemiNormedGroupCat
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
⊢ explicitCokernelπ f ≫ (explicitCokernelIso f).hom ≫ cokernel.desc f g w = explicitCokernelπ f ≫ explicitCokernelDesc w
[PROOFSTEP]
simp [explicitCokernelDesc, explicitCokernelπ, explicitCokernelIso, IsColimit.coconePointUniqueUpToIso]
[GOAL]
A B C D : SemiNormedGroupCat
fab : A ⟶ B
fbd : B ⟶ D
fac : A ⟶ C
fcd : C ⟶ D
h : fab ≫ fbd = fac ≫ fcd
⊢ fab ≫ fbd ≫ explicitCokernelπ fcd = 0
[PROOFSTEP]
simp [reassoc_of% h]
[GOAL]
A B C D B' D' : SemiNormedGroupCat
fab : A ⟶ B
fbd : B ⟶ D
fac : A ⟶ C
fcd : C ⟶ D
h : fab ≫ fbd = fac ≫ fcd
fbb' : B ⟶ B'
fdd' : D ⟶ D'
condb : fab ≫ fbb' = 0
condd : fcd ≫ fdd' = 0
g : B' ⟶ D'
h' : fbb' ≫ g = fbd ≫ fdd'
⊢ explicitCokernelDesc condb ≫ g = explicitCokernel.map h ≫ explicitCokernelDesc condd
[PROOFSTEP]
delta explicitCokernel.map
[GOAL]
A B C D B' D' : SemiNormedGroupCat
fab : A ⟶ B
fbd : B ⟶ D
fac : A ⟶ C
fcd : C ⟶ D
h : fab ≫ fbd = fac ≫ fcd
fbb' : B ⟶ B'
fdd' : D ⟶ D'
condb : fab ≫ fbb' = 0
condd : fcd ≫ fdd' = 0
g : B' ⟶ D'
h' : fbb' ≫ g = fbd ≫ fdd'
⊢ explicitCokernelDesc condb ≫ g =
    explicitCokernelDesc (_ : fab ≫ fbd ≫ explicitCokernelπ fcd = 0) ≫ explicitCokernelDesc condd
[PROOFSTEP]
simp [← cancel_epi (explicitCokernelπ fab), ← Category.assoc, explicitCokernelπ_desc, h']