awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst : CommGroup E
inst_1 : CommGroup F
p_1 q_1 : GroupSeminorm E
x_1 : E
p q : GroupSeminorm E
x : E
rw :
  HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) x : ℝ) ((q : (a : E) → ℝ) 1 : ℝ) ≤
    (fun (f : GroupSeminorm E) ↦ ((⇑f : (a : E) → ℝ) : (a : E) → ℝ)) p x
rw₁ :
  HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) x : ℝ) (0 : ℝ) ≤
    (fun (f : GroupSeminorm E) ↦ ((⇑f : (a : E) → ℝ) : (a : E) → ℝ)) p x
rw₂ rw₃ : LE.le (α := (fun (a : E) ↦ ℝ) x) ((p : (a : E) → ℝ) x : ℝ) ((p : (a : E) → ℝ) x : ℝ)
⊢ HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) x : ℝ) ((q : (a : E) → ℝ) (x / x) : ℝ) ≤
    (fun (f : GroupSeminorm E) ↦ ((⇑f : (a : E) → ℝ) : (a : E) → ℝ)) p x

Tactic:
rw [div_self', map_one_eq_zero q, add_zero]

Premises used: GroupSeminormClass.map_one_eq_zero, div_self', add_zero
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst : CommGroup E
inst_1 : CommGroup F
p_1 q_1 : GroupSeminorm E
x_1 : E
p q : GroupSeminorm E
x : E
⊢ HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) 1 : ℝ) ((q : (a : E) → ℝ) (x / 1) : ℝ) ≤
    (fun (f : GroupSeminorm E) ↦ ((⇑f : (a : E) → ℝ) : (a : E) → ℝ)) q x

Tactic:
simpa only [div_one x, map_one_eq_zero p, zero_add (q x)] using le_rfl

Premises used: le_rfl, GroupSeminormClass.map_one_eq_zero, zero_add, div_one, DFunLike.coe
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst : AddGroup E
inst_1 : SMul R ℝ
inst_2 : SMul R ℝ≥0
inst_3 : IsScalarTower R ℝ≥0 ℝ
inst_4 : DecidableEq E
x y : E
pos :
  ∀ (hx : x = 0), (if x + y = 0 then 0 else 1) ≤ HAdd.hAdd (α := ℝ) (if x = 0 then 0 else 1) (if y = 0 then 0 else 1)
neg :
  ∀ (hx : ¬x = 0), (if x + y = 0 then 0 else 1) ≤ HAdd.hAdd (α := ℝ) (if x = 0 then 0 else 1) (if y = 0 then 0 else 1)
⊢ (if x + y = 0 then 0 else 1) ≤ HAdd.hAdd (α := ℝ) (if x = 0 then 0 else 1) (if y = 0 then 0 else 1)

Tactic:
by_cases hx : x = 0
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst : AddGroup E
inst_1 : SMul R ℝ
inst_2 : SMul R ℝ≥0
inst_3 : IsScalarTower R ℝ≥0 ℝ
inst_4 : DecidableEq E
x y : E
hx : x = 0
pos : (if x + y = 0 then 0 else 1) ≤ HAdd.hAdd (α := ℝ) 0 (if y = 0 then 0 else 1)
pos₁ : (if 0 + y = 0 then 0 else 1) ≤ HAdd.hAdd (α := ℝ) 0 (if y = 0 then 0 else 1)
pos₂ : (if y = 0 then 0 else 1) ≤ HAdd.hAdd (α := ℝ) 0 (if y = 0 then 0 else 1)
pos₃ pos₄ : LE.le (α := ℝ) (if y = 0 then 0 else 1) (if y = 0 then 0 else 1)
⊢ (if x + y = 0 then 0 else 1) ≤ HAdd.hAdd (α := ℝ) (if x = 0 then 0 else 1) (if y = 0 then 0 else 1)

Tactic:
rw [if_pos hx, hx, zero_add, zero_add]

Premises used: if_pos, zero_add
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst : AddGroup E
inst_1 : SMul R ℝ
inst_2 : SMul R ℝ≥0
inst_3 : IsScalarTower R ℝ≥0 ℝ
inst_4 : DecidableEq E
x y : E
hx : ¬x = 0
neg : (if x + y = 0 then 0 else 1) ≤ HAdd.hAdd (α := ℝ) 1 (if y = 0 then 0 else 1)
⊢ (if x + y = 0 then 0 else 1) ≤ HAdd.hAdd (α := ℝ) (if x = 0 then 0 else 1) (if y = 0 then 0 else 1)

Tactic:
rw [if_neg hx]

Premises used: if_neg
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst : AddGroup E
inst_1 : SMul R ℝ
inst_2 : SMul R ℝ≥0
inst_3 : IsScalarTower R ℝ≥0 ℝ
inst_4 : DecidableEq E
x y : E
hx : ¬x = 0
⊢ (if x + y = 0 then 0 else 1) ≤ HAdd.hAdd (α := ℝ) 1 (if y = 0 then 0 else 1)

Tactic:
le_add_of_le_of_nonneg ?_ ?_

Premises used: le_add_of_le_of_nonneg
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst : AddGroup E
inst_1 : SMul R ℝ
inst_2 : SMul R ℝ≥0
inst_3 : IsScalarTower R ℝ≥0 ℝ
inst_4 : DecidableEq E
x y : E
hx : ¬x = 0
neg : LE.le (α := ℝ) (if x + y = 0 then 0 else 1) 1
neg₁ : LE.le (α := ℝ) 0 (if y = 0 then 0 else 1)
⊢ (if x + y = 0 then 0 else 1) ≤ HAdd.hAdd (α := ℝ) 1 (if y = 0 then 0 else 1)

Tactic:
refine le_add_of_le_of_nonneg ?_ ?_

Premises used: le_add_of_le_of_nonneg
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst : AddGroup E
inst_1 : SMul R ℝ
inst_2 : SMul R ℝ≥0
inst_3 : IsScalarTower R ℝ≥0 ℝ
inst_4 : DecidableEq E
x y : E
hx : ¬x = 0
pos : x + y = 0 → LE.le (α := ℝ) 0 1
neg : ¬x + y = 0 → LE.le (α := ℝ) 1 1
⊢ LE.le (α := ℝ) (if x + y = 0 then 0 else 1) 1

Tactic:
split_ifs
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst : AddGroup E
inst_1 : SMul R ℝ
inst_2 : SMul R ℝ≥0
inst_3 : IsScalarTower R ℝ≥0 ℝ
inst_4 : DecidableEq E
x y : E
hx : ¬x = 0
pos : y = 0 → LE.le (α := ℝ) 0 0
neg : ¬y = 0 → LE.le (α := ℝ) 0 1
⊢ LE.le (α := ℝ) 0 (if y = 0 then 0 else 1)

Tactic:
split_ifs
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst : AddGroup E
inst_1 : SMul R ℝ
inst_2 : SMul R ℝ≥0
inst_3 : IsScalarTower R ℝ≥0 ℝ
inst_4 : DecidableEq E
x y : E
hx : ¬x = 0
h : x + y = 0
⊢ LE.le (α := ℝ) 0 1

Tactic:
norm_num
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst : AddGroup E
inst_1 : SMul R ℝ
inst_2 : SMul R ℝ≥0
inst_3 : IsScalarTower R ℝ≥0 ℝ
inst_4 : DecidableEq E
x y : E
hx : ¬x = 0
h : ¬x + y = 0
⊢ LE.le (α := ℝ) 1 1

Tactic:
norm_num
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst : AddGroup E
inst_1 : SMul R ℝ
inst_2 : SMul R ℝ≥0
inst_3 : IsScalarTower R ℝ≥0 ℝ
inst_4 : DecidableEq E
x y : E
hx : ¬x = 0
h : y = 0
⊢ LE.le (α := ℝ) 0 0

Tactic:
norm_num
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst : AddGroup E
inst_1 : SMul R ℝ
inst_2 : SMul R ℝ≥0
inst_3 : IsScalarTower R ℝ≥0 ℝ
inst_4 : DecidableEq E
x y : E
hx : ¬x = 0
h : ¬y = 0
⊢ LE.le (α := ℝ) 0 1

Tactic:
norm_num
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst : AddGroup E
inst_1 : SMul R ℝ
inst_2 : SMul R ℝ≥0
inst_3 : IsScalarTower R ℝ≥0 ℝ
inst_4 : DecidableEq E
x : E
⊢ Eq (α := ℝ) (if -x = 0 then 0 else 1) (if x = 0 then 0 else 1)

Tactic:
simp_rw [neg_eq_zero]

Premises used: neg_eq_zero
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
E : Type u_3
inst : AddGroup E
inst_1 : DecidableEq E
x : E
⊢ Eq (α := ℝ) ((1 : (a : E) → ℝ) x : ℝ) (if x = 0 then 0 else 1 : ℝ)

Tactic:
rfl

Premises used: rfl, ite
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst : AddGroup E
inst_1 : SMul R ℝ
inst_2 : SMul R ℝ≥0
inst_3 : IsScalarTower R ℝ≥0 ℝ
r : R
p : AddGroupSeminorm E
⊢ HSMul.hSMul (β := ℝ) r ((p : (a : E) → ℝ) 0 : ℝ) = 0

Tactic:
simp only [← smul_one_smul ℝ≥0 r (_ : ℝ), NNReal.smul_def, smul_eq_mul, map_zero, mul_zero]

Premises used: map_zero, NNReal, MulZeroClass.mul_zero, NNReal.smul_def, smul_one_smul, smul_eq_mul
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst : AddGroup E
inst_1 : SMul R ℝ
inst_2 : SMul R ℝ≥0
inst_3 : IsScalarTower R ℝ≥0 ℝ
r : R
p : AddGroupSeminorm E
x x_1 : E
simp :
  HMul.hMul (β := ℝ) (↑(HSMul.hSMul (β := ℝ≥0) r 1) : ℝ) ((p : (a : E) → ℝ) (x + x_1) : ℝ) ≤
    (↑(HSMul.hSMul (β := ℝ≥0) r 1) : ℝ) *
      HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) x : ℝ) ((p : (a : E) → ℝ) x_1 : ℝ)
⊢ HSMul.hSMul (β := ℝ) r ((p : (a : E) → ℝ) (x + x_1) : ℝ) ≤
    HSMul.hSMul (β := ℝ) r ((p : (a : E) → ℝ) x : ℝ) + HSMul.hSMul (β := ℝ) r ((p : (a : E) → ℝ) x_1 : ℝ)

Tactic:
simp only [← smul_one_smul ℝ≥0 r (_ : ℝ), NNReal.smul_def, smul_eq_mul, ← mul_add]

Premises used: NNReal, NNReal.smul_def, smul_one_smul, mul_add, smul_eq_mul
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst : AddGroup E
inst_1 : SMul R ℝ
inst_2 : SMul R ℝ≥0
inst_3 : IsScalarTower R ℝ≥0 ℝ
r : R
p : AddGroupSeminorm E
x x_1 : E
hbc : (p : (a : E) → ℝ) (x + x_1) ≤ HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) x : ℝ) ((p : (a : E) → ℝ) x_1 : ℝ)
⊢ HMul.hMul (β := ℝ) (↑(HSMul.hSMul (β := ℝ≥0) r 1) : ℝ) ((p : (a : E) → ℝ) (x + x_1) : ℝ) ≤
    (↑(HSMul.hSMul (β := ℝ≥0) r 1) : ℝ) *
      HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) x : ℝ) ((p : (a : E) → ℝ) x_1 : ℝ)

Tactic:
gcongr
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst : AddGroup E
inst_1 : SMul R ℝ
inst_2 : SMul R ℝ≥0
inst_3 : IsScalarTower R ℝ≥0 ℝ
r : R
p : AddGroupSeminorm E
x x_1 : E
⊢ (p : (a : E) → ℝ) (x + x_1) ≤ HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) x : ℝ) ((p : (a : E) → ℝ) x_1 : ℝ)

Tactic:
apply map_add_le_add

Premises used: SubadditiveHomClass.map_add_le_add
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst : AddGroup E
inst_1 : SMul R ℝ
inst_2 : SMul R ℝ≥0
inst_3 : IsScalarTower R ℝ≥0 ℝ
r : R
p : AddGroupSeminorm E
x : E
⊢ HSMul.hSMul (β := ℝ) r ((p : (a : E) → ℝ) (-x) : ℝ) = HSMul.hSMul (β := ℝ) r ((p : (a : E) → ℝ) x : ℝ)

Tactic:
simp_rw [map_neg_eq_map]

Premises used: AddGroupSeminormClass.map_neg_eq_map
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
R : Type u_1
E : Type u_3
inst : AddGroup E
inst_1 : SMul R ℝ
inst_2 : SMul R ℝ≥0
inst_3 : IsScalarTower R ℝ≥0 ℝ
r : R
p : AddGroupSeminorm E
⊢ (⇑(r • p) : (a : E) → ℝ) = HSMul.hSMul (β := (a : E) → ℝ) r (⇑p : (a : E) → ℝ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
R : Type u_1
E : Type u_3
inst : AddGroup E
inst_1 : SMul R ℝ
inst_2 : SMul R ℝ≥0
inst_3 : IsScalarTower R ℝ≥0 ℝ
r : R
p : AddGroupSeminorm E
x : E
⊢ (r • p : (a : E) → ℝ) x = HSMul.hSMul (β := ℝ) r ((p : (a : E) → ℝ) x : ℝ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst : AddGroup E
inst_1 : SMul R ℝ
inst_2 : SMul R ℝ≥0
inst_3 : IsScalarTower R ℝ≥0 ℝ
inst_4 : SMul R' ℝ
inst_5 : SMul R' ℝ≥0
inst_6 : IsScalarTower R' ℝ≥0 ℝ
inst_7 : SMul R R'
inst_8 : IsScalarTower R R' ℝ
⊢ IsScalarTower.{u_1, u_2, u_3} R R' (AddGroupSeminorm E)

Tactic:
⟨fun r a p => ext fun x => smul_assoc r a (p x)⟩

Premises used: smul_assoc, AddGroupSeminorm.ext, IsScalarTower.mk, DFunLike.coe
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
R : Type u_1
E : Type u_3
inst : AddGroup E
inst_1 : SMul R ℝ
inst_2 : SMul R ℝ≥0
inst_3 : IsScalarTower R ℝ≥0 ℝ
r : R
p q : AddGroupSeminorm E
x y : ℝ
⊢ r • max x y = max (r • x) (r • y)

Tactic:
simpa only [← smul_eq_mul, ← NNReal.smul_def, smul_one_smul ℝ≥0 r (_ : ℝ)] using
      mul_max_of_nonneg x y (r • (1 : ℝ≥0) : ℝ≥0).coe_nonneg

Premises used: NNReal, mul_max_of_nonneg, NNReal.smul_def, smul_one_smul, NNReal.coe_nonneg, HSMul.hSMul, smul_eq_mul, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst : AddGroup E
p q f g : NonarchAddGroupSeminorm E
h :
  Eq.{max (u_3 + 1) 1} (α := (a : E) → ℝ) ((fun (f : NonarchAddGroupSeminorm E) ↦ f.toFun) f)
    ((fun (f : NonarchAddGroupSeminorm E) ↦ f.toFun) g)
obtain :
  ∀ (toFun : E → ℝ) (map_zero' : toFun 0 = 0)
    (add_le_max' :
      ∀ (r s : E),
        { toFun := toFun, map_zero' := map_zero' : ZeroHom E ℝ }.toFun (r + s) ≤
          max ({ toFun := toFun, map_zero' := map_zero' : ZeroHom E ℝ }.toFun r)
            ({ toFun := toFun, map_zero' := map_zero' : ZeroHom E ℝ }.toFun s))
    (neg' :
      ∀ (r : E),
        { toFun := toFun, map_zero' := map_zero' : ZeroHom E ℝ }.toFun (-r) =
          { toFun := toFun, map_zero' := map_zero' : ZeroHom E ℝ }.toFun r)
    (h :
      Eq.{max (u_3 + 1) 1} (α := (a : E) → ℝ)
        ((fun (f : NonarchAddGroupSeminorm E) ↦ f.toFun)
          { toFun := toFun, map_zero' := map_zero', add_le_max' := add_le_max', neg' := neg' })
        ((fun (f : NonarchAddGroupSeminorm E) ↦ f.toFun) g)),
    { toFun := toFun, map_zero' := map_zero', add_le_max' := add_le_max', neg' := neg' : NonarchAddGroupSeminorm E } = g
⊢ f = g

Tactic:
obtain ⟨⟨_, _⟩, _, _⟩ := f
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst : AddGroup E
p q g : NonarchAddGroupSeminorm E
toFun : E → ℝ
map_zero' : toFun 0 = 0
add_le_max' :
  ∀ (r s : E),
    { toFun := toFun, map_zero' := map_zero' : ZeroHom E ℝ }.toFun (r + s) ≤
      max ({ toFun := toFun, map_zero' := map_zero' : ZeroHom E ℝ }.toFun r)
        ({ toFun := toFun, map_zero' := map_zero' : ZeroHom E ℝ }.toFun s)
neg' :
  ∀ (r : E),
    { toFun := toFun, map_zero' := map_zero' : ZeroHom E ℝ }.toFun (-r) =
      { toFun := toFun, map_zero' := map_zero' : ZeroHom E ℝ }.toFun r
h :
  Eq.{max (u_3 + 1) 1} (α := (a : E) → ℝ)
    ((fun (f : NonarchAddGroupSeminorm E) ↦ f.toFun)
      { toFun := toFun, map_zero' := map_zero', add_le_max' := add_le_max', neg' := neg' })
    ((fun (f : NonarchAddGroupSeminorm E) ↦ f.toFun) g)
mk :
  ∀ (toZeroHom : ZeroHom E ℝ)
    (add_le_max'_1 : ∀ (r s : E), toZeroHom.toFun (r + s) ≤ max (toZeroHom.toFun r) (toZeroHom.toFun s))
    (neg'_1 : ∀ (r : E), toZeroHom.toFun (-r) = toZeroHom.toFun r)
    (h :
      Eq.{max (u_3 + 1) 1} (α := (a : E) → ℝ)
        ((fun (f : NonarchAddGroupSeminorm E) ↦ f.toFun)
          { toFun := toFun, map_zero' := map_zero', add_le_max' := add_le_max', neg' := neg' })
        ((fun (f : NonarchAddGroupSeminorm E) ↦ f.toFun)
          { toZeroHom := toZeroHom, add_le_max' := add_le_max'_1, neg' := neg'_1 })),
    { toFun := toFun, map_zero' := map_zero', add_le_max' := add_le_max', neg' := neg' : NonarchAddGroupSeminorm E } =
      { toZeroHom := toZeroHom, add_le_max' := add_le_max'_1, neg' := neg'_1 }
⊢ { toFun := toFun, map_zero' := map_zero', add_le_max' := add_le_max', neg' := neg' : NonarchAddGroupSeminorm E } = g

Tactic:
cases g
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst : AddGroup E
p q : NonarchAddGroupSeminorm E
toFun : E → ℝ
map_zero' : toFun 0 = 0
add_le_max' :
  ∀ (r s : E),
    { toFun := toFun, map_zero' := map_zero' : ZeroHom E ℝ }.toFun (r + s) ≤
      max ({ toFun := toFun, map_zero' := map_zero' : ZeroHom E ℝ }.toFun r)
        ({ toFun := toFun, map_zero' := map_zero' : ZeroHom E ℝ }.toFun s)
neg' :
  ∀ (r : E),
    { toFun := toFun, map_zero' := map_zero' : ZeroHom E ℝ }.toFun (-r) =
      { toFun := toFun, map_zero' := map_zero' : ZeroHom E ℝ }.toFun r
toZeroHom : ZeroHom E ℝ
add_le_max'_1 : ∀ (r s : E), toZeroHom.toFun (r + s) ≤ max (toZeroHom.toFun r) (toZeroHom.toFun s)
neg'_1 : ∀ (r : E), toZeroHom.toFun (-r) = toZeroHom.toFun r
h :
  Eq.{max (u_3 + 1) 1} (α := (a : E) → ℝ)
    ((fun (f : NonarchAddGroupSeminorm E) ↦ f.toFun)
      { toFun := toFun, map_zero' := map_zero', add_le_max' := add_le_max', neg' := neg' })
    ((fun (f : NonarchAddGroupSeminorm E) ↦ f.toFun)
      { toZeroHom := toZeroHom, add_le_max' := add_le_max'_1, neg' := neg'_1 })
⊢ { toFun := toFun, map_zero' := map_zero', add_le_max' := add_le_max', neg' := neg' : NonarchAddGroupSeminorm E } =
    { toZeroHom := toZeroHom, add_le_max' := add_le_max'_1, neg' := neg'_1 }

Tactic:
congr
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
E : Type u_3
inst : AddGroup E
p : NonarchAddGroupSeminorm E
⊢ Eq (α := (a : E) → ℝ) (⇑p.toZeroHom : (a : E) → ℝ) (⇑p : (a : E) → ℝ)

Tactic:
rfl
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
E : Type u_3
inst : AddGroup E
p q : NonarchAddGroupSeminorm E
⊢ (∀ (x : E), Eq (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ((q : (a : E) → ℝ) x : ℝ)) → p = q

Tactic:
DFunLike.ext p q

Premises used: DFunLike.ext
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
E : Type u_3
inst : AddGroup E
p q : NonarchAddGroupSeminorm E
⊢ p ≤ q ↔ LE.le (α := (a : E) → ℝ) (⇑p : (a : E) → ℝ) (⇑q : (a : E) → ℝ)

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
E : Type u_3
inst : AddGroup E
p q : NonarchAddGroupSeminorm E
⊢ p < q ↔ LT.lt (α := (a : E) → ℝ) (⇑p : (a : E) → ℝ) (⇑q : (a : E) → ℝ)

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
E : Type u_3
inst : AddGroup E
p q : NonarchAddGroupSeminorm E
⊢ LE.le (α := (a : E) → ℝ) (⇑p : (a : E) → ℝ) (⇑q : (a : E) → ℝ) ↔ p ≤ q

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
E : Type u_3
inst : AddGroup E
p q : NonarchAddGroupSeminorm E
⊢ LT.lt (α := (a : E) → ℝ) (⇑p : (a : E) → ℝ) (⇑q : (a : E) → ℝ) ↔ p < q

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst : AddGroup E
p q : NonarchAddGroupSeminorm E
r s : E
rw : LE.le (α := ℝ) 0 0
⊢ LE.le (α := ℝ) 0 (max 0 0)

Tactic:
rw [max_eq_right]

Premises used: max_eq_right
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst : AddGroup E
p q : NonarchAddGroupSeminorm E
r s : E
⊢ LE.le (α := ℝ) 0 0

Tactic:
rfl
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
E : Type u_3
inst : AddGroup E
⊢ Eq.{u_3 + 1} (α := (a : E) → ℝ) (⇑0 : (a : E) → ℝ) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
E : Type u_3
inst : AddGroup E
x : E
⊢ Eq (α := ℝ) ((0 : (a : E) → ℝ) x : ℝ) (0 : ℝ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst : AddGroup E
p q : NonarchAddGroupSeminorm E
s : Set (NonarchAddGroupSeminorm E)
h : BddAbove s
⊢ Eq (α := ℝ) (⨆ (p : (↑s : Type u_3)), ((↑p : NonarchAddGroupSeminorm E) : (a : E) → ℝ) 0) 0

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst : AddGroup E
p q : NonarchAddGroupSeminorm E
s : Set (NonarchAddGroupSeminorm E)
h : BddAbove s
x y : E
inl :
  ∀ (h : BddAbove.{u_3} (α := NonarchAddGroupSeminorm E) ∅),
    LE.le (α := ℝ) (⨆ (p : (↑∅ : Type u_3)), ((↑p : NonarchAddGroupSeminorm E) : (a : E) → ℝ) (x + y))
      (max (⨆ (p : (↑∅ : Type u_3)), ((↑p : NonarchAddGroupSeminorm E) : (a : E) → ℝ) x)
        (⨆ (p : (↑∅ : Type u_3)), ((↑p : NonarchAddGroupSeminorm E) : (a : E) → ℝ) y))
inr :
  ∀ (hs : s.Nonempty),
    LE.le (α := ℝ) (⨆ (p : (↑s : Type u_3)), ((↑p : NonarchAddGroupSeminorm E) : (a : E) → ℝ) (x + y))
      (max (⨆ (p : (↑s : Type u_3)), ((↑p : NonarchAddGroupSeminorm E) : (a : E) → ℝ) x)
        (⨆ (p : (↑s : Type u_3)), ((↑p : NonarchAddGroupSeminorm E) : (a : E) → ℝ) y))
⊢ LE.le (α := ℝ) (⨆ (p : (↑s : Type u_3)), ((↑p : NonarchAddGroupSeminorm E) : (a : E) → ℝ) (x + y))
    (max (⨆ (p : (↑s : Type u_3)), ((↑p : NonarchAddGroupSeminorm E) : (a : E) → ℝ) x)
      (⨆ (p : (↑s : Type u_3)), ((↑p : NonarchAddGroupSeminorm E) : (a : E) → ℝ) y))

Tactic:
obtain (rfl | hs) := eq_empty_or_nonempty s

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst : AddGroup E
p q : NonarchAddGroupSeminorm E
x y : E
h : BddAbove.{u_3} (α := NonarchAddGroupSeminorm E) ∅
⊢ LE.le (α := ℝ) (⨆ (p : (↑∅ : Type u_3)), ((↑p : NonarchAddGroupSeminorm E) : (a : E) → ℝ) (x + y))
    (max (⨆ (p : (↑∅ : Type u_3)), ((↑p : NonarchAddGroupSeminorm E) : (a : E) → ℝ) x)
      (⨆ (p : (↑∅ : Type u_3)), ((↑p : NonarchAddGroupSeminorm E) : (a : E) → ℝ) y))

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst : AddGroup E
p q : NonarchAddGroupSeminorm E
s : Set (NonarchAddGroupSeminorm E)
h : BddAbove s
x y : E
hs : s.Nonempty
⊢ Nonempty.{u_3 + 1} (↑s : Type u_3)

Tactic:
have : Nonempty s := hs.to_subtype
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst : AddGroup E
p q : NonarchAddGroupSeminorm E
s : Set (NonarchAddGroupSeminorm E)
h : BddAbove s
x y : E
hs : s.Nonempty
this : Nonempty.{u_3 + 1} (↑s : Type u_3)
⊢ LE.le (α := ℝ) (⨆ (p : (↑s : Type u_3)), ((↑p : NonarchAddGroupSeminorm E) : (a : E) → ℝ) (x + y))
    (max (⨆ (p : (↑s : Type u_3)), ((↑p : NonarchAddGroupSeminorm E) : (a : E) → ℝ) x)
      (⨆ (p : (↑s : Type u_3)), ((↑p : NonarchAddGroupSeminorm E) : (a : E) → ℝ) y))

Tactic:
ciSup_le fun p ↦ (map_add_le_max p.1 x y).trans ?_

Premises used: LE.le.trans, Subtype.val, ciSup_le, NonarchimedeanHomClass.map_add_le_max
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst : AddGroup E
p q : NonarchAddGroupSeminorm E
s : Set (NonarchAddGroupSeminorm E)
h : BddAbove s
x y : E
hs : s.Nonempty
this : Nonempty.{u_3 + 1} (↑s : Type u_3)
inr :
  ∀ (p : (↑s : Type u_3)),
    LE.le (α := ℝ)
      (max (((↑p : NonarchAddGroupSeminorm E) : (a : E) → ℝ) x) (((↑p : NonarchAddGroupSeminorm E) : (a : E) → ℝ) y) :
        ℝ)
      (max (⨆ (p : (↑s : Type u_3)), ((↑p : NonarchAddGroupSeminorm E) : (a : E) → ℝ) x)
          (⨆ (p : (↑s : Type u_3)), ((↑p : NonarchAddGroupSeminorm E) : (a : E) → ℝ) y) :
        ℝ)
⊢ LE.le (α := ℝ) (⨆ (p : (↑s : Type u_3)), ((↑p : NonarchAddGroupSeminorm E) : (a : E) → ℝ) (x + y))
    (max (⨆ (p : (↑s : Type u_3)), ((↑p : NonarchAddGroupSeminorm E) : (a : E) → ℝ) x)
      (⨆ (p : (↑s : Type u_3)), ((↑p : NonarchAddGroupSeminorm E) : (a : E) → ℝ) y))

Tactic:
refine ciSup_le fun p ↦ (map_add_le_max p.1 x y).trans ?_

Premises used: ciSup_le
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst : AddGroup E
p_1 q : NonarchAddGroupSeminorm E
s : Set (NonarchAddGroupSeminorm E)
h : BddAbove s
x y : E
hs : s.Nonempty
this : Nonempty.{u_3 + 1} (↑s : Type u_3)
p : (↑s : Type u_3)
inr :
  LE.le (α := ℝ) (((↑p : NonarchAddGroupSeminorm E) : (a : E) → ℝ) x : ℝ)
    (⨆ (p : (↑s : Type u_3)), ((↑p : NonarchAddGroupSeminorm E) : (a : E) → ℝ) x : ℝ)
inr₁ :
  LE.le (α := ℝ) (((↑p : NonarchAddGroupSeminorm E) : (a : E) → ℝ) y : ℝ)
    (⨆ (p : (↑s : Type u_3)), ((↑p : NonarchAddGroupSeminorm E) : (a : E) → ℝ) y : ℝ)
⊢ LE.le (α := ℝ)
    (max (((↑p : NonarchAddGroupSeminorm E) : (a : E) → ℝ) x) (((↑p : NonarchAddGroupSeminorm E) : (a : E) → ℝ) y) : ℝ)
    (max (⨆ (p : (↑s : Type u_3)), ((↑p : NonarchAddGroupSeminorm E) : (a : E) → ℝ) x)
        (⨆ (p : (↑s : Type u_3)), ((↑p : NonarchAddGroupSeminorm E) : (a : E) → ℝ) y) :
      ℝ)

Tactic:
gcongr
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst : AddGroup E
p_1 q : NonarchAddGroupSeminorm E
s : Set (NonarchAddGroupSeminorm E)
h : BddAbove s
x y : E
hs : s.Nonempty
this : Nonempty.{u_3 + 1} (↑s : Type u_3)
p : (↑s : Type u_3)
apply :
  BddAbove (α := ℝ)
    (range.{0, max 1 (u_3 + 1)} (ι := { x : NonarchAddGroupSeminorm E // x ∈ s })
      ((fun (x_1 : NonarchAddGroupSeminorm E) ↦ (x_1 : (a : E) → ℝ) x) ∘
        Subtype.val (p := fun (x : NonarchAddGroupSeminorm E) ↦ x ∈ s)))
⊢ LE.le (α := ℝ) (((↑p : NonarchAddGroupSeminorm E) : (a : E) → ℝ) x : ℝ)
    (⨆ (p : (↑s : Type u_3)), ((↑p : NonarchAddGroupSeminorm E) : (a : E) → ℝ) x : ℝ)

Tactic:
apply le_ciSup (f := (DFunLike.coe · _) ∘ Subtype.val) ?_ p

Premises used: le_ciSup
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst : AddGroup E
p_1 q : NonarchAddGroupSeminorm E
s : Set (NonarchAddGroupSeminorm E)
h : BddAbove s
x y : E
hs : s.Nonempty
this : Nonempty.{u_3 + 1} (↑s : Type u_3)
p : (↑s : Type u_3)
x_1 x_2 : NonarchAddGroupSeminorm E
h' : x_1 ≤ x_2
⊢ LE.le (α := ℝ) ((x_1 : (a : E) → ℝ) x : ℝ) ((x_2 : (a : E) → ℝ) x : ℝ)

Tactic:
h' _