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 : 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:
exact h' _
-- 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)
⊢ 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)))

Tactic:
simpa [Set.range_comp] using Monotone.map_bddAbove (fun _ _ h' ↦ by exact h' _) h

Premises used: Set.range_comp, Monotone.map_bddAbove
-- 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 : NonarchAddGroupSeminorm E) ↦ (x : (a : E) → ℝ) y) ∘
        Subtype.val (p := fun (x : NonarchAddGroupSeminorm E) ↦ x ∈ s)))
⊢ LE.le (α := ℝ) (((↑p : NonarchAddGroupSeminorm E) : (a : E) → ℝ) y : ℝ)
    (⨆ (p : (↑s : Type u_3)), ((↑p : NonarchAddGroupSeminorm E) : (a : E) → ℝ) y : ℝ)

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) → ℝ) y : ℝ) ((x_2 : (a : E) → ℝ) y : ℝ)

Tactic:
h' _
-- 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) → ℝ) y : ℝ) ((x_2 : (a : E) → ℝ) y : ℝ)

Tactic:
exact h' _
-- 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)
⊢ BddAbove (α := ℝ)
    (range.{0, max 1 (u_3 + 1)} (ι := { x : NonarchAddGroupSeminorm E // x ∈ s })
      ((fun (x : NonarchAddGroupSeminorm E) ↦ (x : (a : E) → ℝ) y) ∘
        Subtype.val (p := fun (x : NonarchAddGroupSeminorm E) ↦ x ∈ s)))

Tactic:
simpa [Set.range_comp] using Monotone.map_bddAbove (fun _ _ h' ↦ by exact h' _) h

Premises used: Set.range_comp, Monotone.map_bddAbove
-- 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
⊢ ∀ (r : E),
    Eq (α := ℝ) (⨆ (p : (↑s : Type u_3)), ((↑p : NonarchAddGroupSeminorm E) : (a : E) → ℝ) (-r))
      (⨆ (p : (↑s : Type u_3)), ((↑p : NonarchAddGroupSeminorm E) : (a : E) → ℝ) r)

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
E : Type u_3
inst : AddGroup E
s : Set (NonarchAddGroupSeminorm E)
hs : ¬BddAbove s
⊢ sSup s = 0

Tactic:
simp [SupSet.sSup, hs]

Premises used: SupSet.sSup
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
E : Type u_3
inst : AddGroup E
s : Set (NonarchAddGroupSeminorm E)
hs : BddAbove s
x : E
simp :
  Eq (α := ℝ)
    (({ toFun := fun (x : E) ↦ ⨆ (p : (↑s : Type u_3)), ((↑p : NonarchAddGroupSeminorm E) : (a : E) → ℝ) x,
            map_zero' := ⋯, add_le_max' := ⋯, neg' := ⋯ } :
          (a : E) → ℝ)
        x :
      ℝ)
    (⨆ (p : (↑s : Type u_3)), ((↑p : NonarchAddGroupSeminorm E) : (a : E) → ℝ) x : ℝ)
⊢ Eq (α := ℝ) ((sSup s : (a : E) → ℝ) x : ℝ)
    (⨆ (p : (↑s : Type u_3)), ((↑p : NonarchAddGroupSeminorm E) : (a : E) → ℝ) x : ℝ)

Tactic:
simp [SupSet.sSup, hs]

Premises used: SupSet.sSup
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
E : Type u_3
inst : AddGroup E
s : Set (NonarchAddGroupSeminorm E)
hs : BddAbove s
x : E
⊢ Eq (α := ℝ)
    (({ toFun := fun (x : E) ↦ ⨆ (p : (↑s : Type u_3)), ((↑p : NonarchAddGroupSeminorm E) : (a : E) → ℝ) x,
            map_zero' := ⋯, add_le_max' := ⋯, neg' := ⋯ } :
          (a : E) → ℝ)
        x :
      ℝ)
    (⨆ (p : (↑s : Type u_3)), ((↑p : NonarchAddGroupSeminorm E) : (a : E) → ℝ) x : ℝ)

Tactic:
rfl
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
E : Type u_3
inst : AddGroup E
s : Set (NonarchAddGroupSeminorm E)
hs : BddAbove s
x : E
rw :
  Eq (α := ℝ) (sSup (range fun (p : (↑s : Type u_3)) ↦ ((↑p : NonarchAddGroupSeminorm E) : (a : E) → ℝ) x))
    (sSup ((fun (x_1 : NonarchAddGroupSeminorm E) ↦ (x_1 : (a : E) → ℝ) x) '' s))
⊢ Eq (α := ℝ) ((sSup s : (a : E) → ℝ) x : ℝ)
    (sSup ((fun (x_1 : NonarchAddGroupSeminorm E) ↦ (x_1 : (a : E) → ℝ) x) '' s) : ℝ)

Tactic:
rw [coe_sSup_apply hs, ← sSup_range]

Premises used: sSup_range, NonarchAddGroupSeminorm.coe_sSup_apply
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
E : Type u_3
inst : AddGroup E
s : Set (NonarchAddGroupSeminorm E)
hs : BddAbove s
x : E
e_a :
  Eq (α := Set ℝ) (range fun (p : (↑s : Type u_3)) ↦ ((↑p : NonarchAddGroupSeminorm E) : (a : E) → ℝ) x)
    ((fun (x_1 : NonarchAddGroupSeminorm E) ↦ (x_1 : (a : E) → ℝ) x) '' s)
⊢ Eq (α := ℝ) (sSup (range fun (p : (↑s : Type u_3)) ↦ ((↑p : NonarchAddGroupSeminorm E) : (a : E) → ℝ) x))
    (sSup ((fun (x_1 : NonarchAddGroupSeminorm E) ↦ (x_1 : (a : E) → ℝ) x) '' s))

Tactic:
congr
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
E : Type u_3
inst : AddGroup E
s : Set (NonarchAddGroupSeminorm E)
hs : BddAbove s
x : E
e_a :
  ∀ (x_1 : ℝ),
    Membership.mem (γ := Set ℝ) (range fun (p : (↑s : Type u_3)) ↦ ((↑p : NonarchAddGroupSeminorm E) : (a : E) → ℝ) x)
        x_1 ↔
      Membership.mem (γ := Set ℝ) ((fun (x_2 : NonarchAddGroupSeminorm E) ↦ (x_2 : (a : E) → ℝ) x) '' s) x_1
⊢ Eq (α := Set ℝ) (range fun (p : (↑s : Type u_3)) ↦ ((↑p : NonarchAddGroupSeminorm E) : (a : E) → ℝ) x)
    ((fun (x_1 : NonarchAddGroupSeminorm E) ↦ (x_1 : (a : E) → ℝ) x) '' s)

Tactic:
ext
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
E : Type u_3
inst : AddGroup E
s : Set (NonarchAddGroupSeminorm E)
hs : BddAbove s
x : E
x_1 : ℝ
⊢ Membership.mem (γ := Set ℝ) (range fun (p : (↑s : Type u_3)) ↦ ((↑p : NonarchAddGroupSeminorm E) : (a : E) → ℝ) x)
      x_1 ↔
    Membership.mem (γ := Set ℝ) ((fun (x_2 : NonarchAddGroupSeminorm E) ↦ (x_2 : (a : E) → ℝ) x) '' s) x_1

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
E : Type u_3
inst : AddGroup E
ι : Type u_6
f : ι → NonarchAddGroupSeminorm E
h : BddAbove (range f)
x : E
rw :
  Eq (α := ℝ) (⨆ (p : (↑(range f) : Type u_3)), ((↑p : NonarchAddGroupSeminorm E) : (a : E) → ℝ) x)
    (⨆ (i : ι), (f i : (a : E) → ℝ) x)
⊢ Eq (α := ℝ) ((⨆ (i : ι), f i : (a : E) → ℝ) x : ℝ) (⨆ (i : ι), (f i : (a : E) → ℝ) x : ℝ)

Tactic:
rw [← sSup_range, coe_sSup_apply h]

Premises used: sSup_range, NonarchAddGroupSeminorm.coe_sSup_apply
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
E : Type u_3
inst : AddGroup E
ι : Type u_6
f : ι → NonarchAddGroupSeminorm E
h : BddAbove (range f)
x : E
⊢ ∀ (x_1 : ι),
    Eq (α := ℝ) (((↑(rangeFactorization f x_1) : NonarchAddGroupSeminorm E) : (a : E) → ℝ) x : ℝ)
      ((f x_1 : (a : E) → ℝ) x : ℝ)

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
E : Type u_3
inst : AddGroup E
ι : Type u_6
f : ι → NonarchAddGroupSeminorm E
h : BddAbove (range f)
x : E
⊢ Eq (α := ℝ) (⨆ (p : (↑(range f) : Type u_3)), ((↑p : NonarchAddGroupSeminorm E) : (a : E) → ℝ) x)
    (⨆ (i : ι), (f i : (a : E) → ℝ) x)

Tactic:
exact (Set.rangeFactorization_surjective.iSup_congr _ (by simp)) |>.symm

Premises used: Function.Surjective.iSup_congr, Set.rangeFactorization_surjective, Eq.symm
-- 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_1 p q : NonarchAddGroupSeminorm E
rw : Eq (α := ℝ) (max ((p : (a : E) → ℝ) 0) ((q : (a : E) → ℝ) 0) : ℝ) (0 : ℝ)
rw₁ : Eq (α := ℝ) (max ((p : (a : E) → ℝ) 0) ((q : (a : E) → ℝ) 0) : ℝ) ((p : (a : E) → ℝ) 0 : ℝ)
rw₂ : LE.le (α := ℝ) ((q : (a : E) → ℝ) 0 : ℝ) ((p : (a : E) → ℝ) 0 : ℝ)
rw₃ : LE.le (α := ℝ) ((q : (a : E) → ℝ) 0 : ℝ) (0 : ℝ)
rw₄ rw₅ : LE.le (α := ℝ) 0 0
⊢ Eq (α := ℝ) (((⇑p : (a : E) → ℝ) ⊔ (⇑q : (a : E) → ℝ)) 0) 0

Tactic:
rw [Pi.sup_apply, ← map_zero p, sup_eq_left, map_zero p, map_zero q]

Premises used: map_zero, sup_eq_left, Pi.sup_apply
-- 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_1 p q : NonarchAddGroupSeminorm E
x : E
simp_rw :
  Eq (α := ℝ) (max ((p : (a : E) → ℝ) (-x)) ((q : (a : E) → ℝ) (-x)) : ℝ)
    (max ((p : (a : E) → ℝ) x) ((q : (a : E) → ℝ) x) : ℝ)
simp_rw₁ :
  Eq (α := ℝ) (max ((p : (a : E) → ℝ) x) ((q : (a : E) → ℝ) (-x)) : ℝ)
    (max ((p : (a : E) → ℝ) x) ((q : (a : E) → ℝ) x) : ℝ)
⊢ Eq (α := ℝ) (((⇑p : (a : E) → ℝ) ⊔ (⇑q : (a : E) → ℝ)) (-x)) (((⇑p : (a : E) → ℝ) ⊔ (⇑q : (a : E) → ℝ)) x)

Tactic:
simp_rw [Pi.sup_apply, map_neg_eq_map p, map_neg_eq_map q]

Premises used: AddGroupSeminormClass.map_neg_eq_map, Pi.sup_apply
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
E : Type u_3
inst : AddGroup E
p q : NonarchAddGroupSeminorm E
⊢ Eq (α := (a : E) → ℝ) (⇑(p ⊔ q) : (a : E) → ℝ) ((⇑p : (a : E) → ℝ) ⊔ (⇑q : (a : E) → ℝ))

Tactic:
rfl

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

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
E : Type u_3
inst : AddCommGroup E
p q : NonarchAddGroupSeminorm E
x_1 x : E
⊢ 0 ≤ HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) x : ℝ) ((q : (a : E) → ℝ) (x_1 - x) : ℝ)

Tactic:
positivity
-- 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 : Group 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 = 1), (if x * y = 1 then 0 else 1) ≤ HAdd.hAdd (α := ℝ) (if x = 1 then 0 else 1) (if y = 1 then 0 else 1)
neg :
  ∀ (hx : ¬x = 1), (if x * y = 1 then 0 else 1) ≤ HAdd.hAdd (α := ℝ) (if x = 1 then 0 else 1) (if y = 1 then 0 else 1)
⊢ (if x * y = 1 then 0 else 1) ≤ HAdd.hAdd (α := ℝ) (if x = 1 then 0 else 1) (if y = 1 then 0 else 1)

Tactic:
by_cases hx : x = 1
-- 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 : Group E
inst_1 : SMul R ℝ
inst_2 : SMul R ℝ≥0
inst_3 : IsScalarTower R ℝ≥0 ℝ
inst_4 : DecidableEq E
x y : E
hx : x = 1
pos : (if x * y = 1 then 0 else 1) ≤ HAdd.hAdd (α := ℝ) 0 (if y = 1 then 0 else 1)
pos₁ : (if 1 * y = 1 then 0 else 1) ≤ HAdd.hAdd (α := ℝ) 0 (if y = 1 then 0 else 1)
pos₂ : (if y = 1 then 0 else 1) ≤ HAdd.hAdd (α := ℝ) 0 (if y = 1 then 0 else 1)
pos₃ pos₄ : LE.le (α := ℝ) (if y = 1 then 0 else 1) (if y = 1 then 0 else 1)
⊢ (if x * y = 1 then 0 else 1) ≤ HAdd.hAdd (α := ℝ) (if x = 1 then 0 else 1) (if y = 1 then 0 else 1)

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

Premises used: if_pos, zero_add, one_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 : Group E
inst_1 : SMul R ℝ
inst_2 : SMul R ℝ≥0
inst_3 : IsScalarTower R ℝ≥0 ℝ
inst_4 : DecidableEq E
x y : E
hx : ¬x = 1
neg : (if x * y = 1 then 0 else 1) ≤ HAdd.hAdd (α := ℝ) 1 (if y = 1 then 0 else 1)
⊢ (if x * y = 1 then 0 else 1) ≤ HAdd.hAdd (α := ℝ) (if x = 1 then 0 else 1) (if y = 1 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 : Group E
inst_1 : SMul R ℝ
inst_2 : SMul R ℝ≥0
inst_3 : IsScalarTower R ℝ≥0 ℝ
inst_4 : DecidableEq E
x y : E
hx : ¬x = 1
⊢ (if x * y = 1 then 0 else 1) ≤ HAdd.hAdd (α := ℝ) 1 (if y = 1 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 : Group E
inst_1 : SMul R ℝ
inst_2 : SMul R ℝ≥0
inst_3 : IsScalarTower R ℝ≥0 ℝ
inst_4 : DecidableEq E
x y : E
hx : ¬x = 1
neg : LE.le (α := ℝ) (if x * y = 1 then 0 else 1) 1
neg₁ : LE.le (α := ℝ) 0 (if y = 1 then 0 else 1)
⊢ (if x * y = 1 then 0 else 1) ≤ HAdd.hAdd (α := ℝ) 1 (if y = 1 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 : Group E
inst_1 : SMul R ℝ
inst_2 : SMul R ℝ≥0
inst_3 : IsScalarTower R ℝ≥0 ℝ
inst_4 : DecidableEq E
x y : E
hx : ¬x = 1
pos : x * y = 1 → LE.le (α := ℝ) 0 1
neg : ¬x * y = 1 → LE.le (α := ℝ) 1 1
⊢ LE.le (α := ℝ) (if x * y = 1 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 : Group E
inst_1 : SMul R ℝ
inst_2 : SMul R ℝ≥0
inst_3 : IsScalarTower R ℝ≥0 ℝ
inst_4 : DecidableEq E
x y : E
hx : ¬x = 1
pos : y = 1 → LE.le (α := ℝ) 0 0
neg : ¬y = 1 → LE.le (α := ℝ) 0 1
⊢ LE.le (α := ℝ) 0 (if y = 1 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 : Group E
inst_1 : SMul R ℝ
inst_2 : SMul R ℝ≥0
inst_3 : IsScalarTower R ℝ≥0 ℝ
inst_4 : DecidableEq E
x y : E
hx : ¬x = 1
h : x * y = 1
⊢ 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 : Group E
inst_1 : SMul R ℝ
inst_2 : SMul R ℝ≥0
inst_3 : IsScalarTower R ℝ≥0 ℝ
inst_4 : DecidableEq E
x y : E
hx : ¬x = 1
h : ¬x * y = 1
⊢ 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 : Group E
inst_1 : SMul R ℝ
inst_2 : SMul R ℝ≥0
inst_3 : IsScalarTower R ℝ≥0 ℝ
inst_4 : DecidableEq E
x y : E
hx : ¬x = 1
h : y = 1
⊢ 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 : Group E
inst_1 : SMul R ℝ
inst_2 : SMul R ℝ≥0
inst_3 : IsScalarTower R ℝ≥0 ℝ
inst_4 : DecidableEq E
x y : E
hx : ¬x = 1
h : ¬y = 1
⊢ 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 : Group E
inst_1 : SMul R ℝ
inst_2 : SMul R ℝ≥0
inst_3 : IsScalarTower R ℝ≥0 ℝ
inst_4 : DecidableEq E
x : E
⊢ Eq (α := ℝ) (if x⁻¹ = 1 then 0 else 1) (if x = 1 then 0 else 1)

Tactic:
simp_rw [inv_eq_one]

Premises used: inv_eq_one
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
E : Type u_3
inst : Group E
inst_1 : DecidableEq E
x : E
⊢ Eq (α := ℝ) ((1 : (a : E) → ℝ) x : ℝ) (if x = 1 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 : Group E
inst_1 : SMul R ℝ
inst_2 : SMul R ℝ≥0
inst_3 : IsScalarTower R ℝ≥0 ℝ
r : R
p : GroupSeminorm E
⊢ HSMul.hSMul (β := ℝ) r ((p : (a : E) → ℝ) 1 : ℝ) = 0

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

Premises used: GroupSeminormClass.map_one_eq_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 : Group E
inst_1 : SMul R ℝ
inst_2 : SMul R ℝ≥0
inst_3 : IsScalarTower R ℝ≥0 ℝ
r : R
p : GroupSeminorm 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 : Group E
inst_1 : SMul R ℝ
inst_2 : SMul R ℝ≥0
inst_3 : IsScalarTower R ℝ≥0 ℝ
r : R
p : GroupSeminorm 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 : Group E
inst_1 : SMul R ℝ
inst_2 : SMul R ℝ≥0
inst_3 : IsScalarTower R ℝ≥0 ℝ
r : R
p : GroupSeminorm 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_mul_le_add

Premises used: MulLEAddHomClass.map_mul_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 : Group E
inst_1 : SMul R ℝ
inst_2 : SMul R ℝ≥0
inst_3 : IsScalarTower R ℝ≥0 ℝ
r : R
p : GroupSeminorm E
x : E
⊢ HSMul.hSMul (β := ℝ) r ((p : (a : E) → ℝ) x⁻¹ : ℝ) = HSMul.hSMul (β := ℝ) r ((p : (a : E) → ℝ) x : ℝ)

Tactic:
simp_rw [map_inv_eq_map p]

Premises used: GroupSeminormClass.map_inv_eq_map
-- 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 : Group 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' (GroupSeminorm E)

Tactic:
⟨fun r a p => ext fun x => smul_assoc r a <| p x⟩

Premises used: smul_assoc, GroupSeminorm.ext, IsScalarTower.mk, DFunLike.coe
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
R : Type u_1
E : Type u_3
inst : Group E
inst_1 : SMul R ℝ
inst_2 : SMul R ℝ≥0
inst_3 : IsScalarTower R ℝ≥0 ℝ
r : R
p : GroupSeminorm 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 : Group E
inst_1 : SMul R ℝ
inst_2 : SMul R ℝ≥0
inst_3 : IsScalarTower R ℝ≥0 ℝ
r : R
p : GroupSeminorm 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
E : Type u_3
inst : Group E
inst_1 : SMul R ℝ
inst_2 : SMul R ℝ≥0
inst_3 : IsScalarTower R ℝ≥0 ℝ
r : R
p q : GroupSeminorm 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
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), LE.le (α := ℝ) (if x + y = 0 then 0 else 1) (max (if x = 0 then 0 else 1) (if y = 0 then 0 else 1))
neg :
  ∀ (hx : ¬x = 0), LE.le (α := ℝ) (if x + y = 0 then 0 else 1) (max (if x = 0 then 0 else 1) (if y = 0 then 0 else 1))
⊢ LE.le (α := ℝ) (if x + y = 0 then 0 else 1) (max (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 : LE.le (α := ℝ) (if y = 0 then 0 else 1) (max 0 (if y = 0 then 0 else 1))
⊢ LE.le (α := ℝ) (if x + y = 0 then 0 else 1) (max (if x = 0 then 0 else 1) (if y = 0 then 0 else 1))

Tactic:
simp_rw [if_pos hx, hx, 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
⊢ LE.le (α := ℝ) (if y = 0 then 0 else 1) (max 0 (if y = 0 then 0 else 1))

Tactic:
le_max_of_le_right (le_refl _)

Premises used: le_refl, le_max_of_le_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
inst_1 : SMul R ℝ
inst_2 : SMul R ℝ≥0
inst_3 : IsScalarTower R ℝ≥0 ℝ
inst_4 : DecidableEq E
x y : E
hx : x = 0
⊢ LE.le (α := ℝ) (if y = 0 then 0 else 1) (max 0 (if y = 0 then 0 else 1))

Tactic:
exact le_max_of_le_right (le_refl _)

Premises used: le_refl, le_max_of_le_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
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) (max 1 (if y = 0 then 0 else 1))
⊢ LE.le (α := ℝ) (if x + y = 0 then 0 else 1) (max (if x = 0 then 0 else 1) (if y = 0 then 0 else 1))

Tactic:
simp_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
pos : x + y = 0 → y = 0 → LE.le (α := ℝ) 0 (max 1 0)
neg : x + y = 0 → ¬y = 0 → LE.le (α := ℝ) 0 (max 1 1)
pos₁ : ¬x + y = 0 → y = 0 → LE.le (α := ℝ) 1 (max 1 0)
neg₁ : ¬x + y = 0 → ¬y = 0 → LE.le (α := ℝ) 1 (max 1 1)
⊢ LE.le (α := ℝ) (if x + y = 0 then 0 else 1) (max 1 (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
h_1 : y = 0
⊢ LE.le (α := ℝ) 0 (max 1 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
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
h_1 : ¬y = 0
⊢ LE.le (α := ℝ) 0 (max 1 1)

Tactic:
simp