awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Seminorm (goal)
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)
⊢ LE.le (α := ℝ) (((↑p : NonarchAddGroupSeminorm E) : (a : E) → ℝ) y : ℝ)
    (⨆ (p : (↑s : Type u_3)), ((↑p : NonarchAddGroupSeminorm E) : (a : E) → ℝ) y : ℝ)
have 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)))
Tactic: apply le_ciSup (f := (DFunLike.coe · _) ∘ Subtype.val) ?_ p
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Seminorm (goal)
Goal:
E : Type u_3
inst : AddGroup E
s : Set (NonarchAddGroupSeminorm E)
hs : BddAbove s
x : E
⊢ Eq (α := ℝ) ((sSup s : (a : E) → ℝ) x : ℝ)
    (⨆ (p : (↑s : Type u_3)), ((↑p : NonarchAddGroupSeminorm E) : (a : E) → ℝ) x : ℝ)
have simp : Eq (α := ℝ)
  (({ toFun := fun (x : E) ↦ ⨆ (p : (↑s : Type u_3)), ((↑p : NonarchAddGroupSeminorm E) : (a : E) → ℝ) x,
          map_zero' := sorry, add_le_max' := sorry, neg' := sorry } :
        (a : E) → ℝ)
      x :
    ℝ)
  (⨆ (p : (↑s : Type u_3)), ((↑p : NonarchAddGroupSeminorm E) : (a : E) → ℝ) x : ℝ)
Tactic: simp [SupSet.sSup, hs]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Seminorm (goal)
Goal:
E : Type u_3
inst : AddGroup E
s : Set (NonarchAddGroupSeminorm E)
hs : BddAbove s
x : E
⊢ Eq (α := ℝ) ((sSup s : (a : E) → ℝ) x : ℝ)
    (sSup ((fun (x_1 : NonarchAddGroupSeminorm E) ↦ (x_1 : (a : E) → ℝ) x) '' s) : ℝ)
have 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))
Tactic: rw [coe_sSup_apply hs, ← sSup_range]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Seminorm (goal)
Goal:
E : Type u_3
inst : AddGroup E
s : Set (NonarchAddGroupSeminorm E)
hs : BddAbove s
x : E
⊢ 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))
have 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)
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Seminorm (goal)
Goal:
E : Type u_3
inst : AddGroup E
s : Set (NonarchAddGroupSeminorm E)
hs : BddAbove s
x : E
⊢ 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)
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Seminorm (goal)
Goal:
E : Type u_3
inst : AddGroup E
ι : Type u_6
f : ι → NonarchAddGroupSeminorm E
h : BddAbove (range f)
x : E
⊢ Eq (α := ℝ) ((⨆ (i : ι), f i : (a : E) → ℝ) x : ℝ) (⨆ (i : ι), (f i : (a : E) → ℝ) x : ℝ)
have rw : Eq (α := ℝ) (⨆ (p : (↑(range f) : Type u_3)), ((↑p : NonarchAddGroupSeminorm E) : (a : E) → ℝ) x)
  (⨆ (i : ι), (f i : (a : E) → ℝ) x)
Tactic: rw [← sSup_range, coe_sSup_apply h]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Seminorm (goal)
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
⊢ Eq (α := ℝ) (((⇑p : (a : E) → ℝ) ⊔ (⇑q : (a : E) → ℝ)) 0) 0
have rw : Eq (α := ℝ) (max ((p : (a : E) → ℝ) 0) ((q : (a : E) → ℝ) 0) : ℝ) (0 : ℝ)
Tactic: rw [Pi.sup_apply, ← map_zero p, sup_eq_left, map_zero p, map_zero q]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Seminorm (goal)
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 : ℝ)
⊢ Eq (α := ℝ) (((⇑p : (a : E) → ℝ) ⊔ (⇑q : (a : E) → ℝ)) 0) 0
have rw₁ : Eq (α := ℝ) (max ((p : (a : E) → ℝ) 0) ((q : (a : E) → ℝ) 0) : ℝ) ((p : (a : E) → ℝ) 0 : ℝ)
Tactic: rw [Pi.sup_apply, ← map_zero p, sup_eq_left, map_zero p, map_zero q]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Seminorm (goal)
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 : ℝ)
⊢ Eq (α := ℝ) (((⇑p : (a : E) → ℝ) ⊔ (⇑q : (a : E) → ℝ)) 0) 0
have rw₂ : LE.le (α := ℝ) ((q : (a : E) → ℝ) 0 : ℝ) ((p : (a : E) → ℝ) 0 : ℝ)
Tactic: rw [Pi.sup_apply, ← map_zero p, sup_eq_left, map_zero p, map_zero q]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Seminorm (goal)
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 : ℝ)
⊢ Eq (α := ℝ) (((⇑p : (a : E) → ℝ) ⊔ (⇑q : (a : E) → ℝ)) 0) 0
have rw₃ : LE.le (α := ℝ) ((q : (a : E) → ℝ) 0 : ℝ) (0 : ℝ)
Tactic: rw [Pi.sup_apply, ← map_zero p, sup_eq_left, map_zero p, map_zero q]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Seminorm (goal)
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 : ℝ)
⊢ Eq (α := ℝ) (((⇑p : (a : E) → ℝ) ⊔ (⇑q : (a : E) → ℝ)) 0) 0
have rw₄ : LE.le (α := ℝ) 0 0
Tactic: rw [Pi.sup_apply, ← map_zero p, sup_eq_left, map_zero p, map_zero q]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Seminorm (goal)
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
⊢ Eq (α := ℝ) (((⇑p : (a : E) → ℝ) ⊔ (⇑q : (a : E) → ℝ)) (-x)) (((⇑p : (a : E) → ℝ) ⊔ (⇑q : (a : E) → ℝ)) x)
have simp_rw : Eq (α := ℝ) (max ((p : (a : E) → ℝ) (-x)) ((q : (a : E) → ℝ) (-x)) : ℝ)
  (max ((p : (a : E) → ℝ) x) ((q : (a : E) → ℝ) x) : ℝ)
Tactic: simp_rw [Pi.sup_apply, map_neg_eq_map p, map_neg_eq_map q]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Seminorm (goal)
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) : ℝ)
⊢ Eq (α := ℝ) (((⇑p : (a : E) → ℝ) ⊔ (⇑q : (a : E) → ℝ)) (-x)) (((⇑p : (a : E) → ℝ) ⊔ (⇑q : (a : E) → ℝ)) x)
have simp_rw₁ : Eq (α := ℝ) (max ((p : (a : E) → ℝ) x) ((q : (a : E) → ℝ) (-x)) : ℝ)
  (max ((p : (a : E) → ℝ) x) ((q : (a : E) → ℝ) x) : ℝ)
Tactic: simp_rw [Pi.sup_apply, map_neg_eq_map p, map_neg_eq_map q]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Seminorm (goal)
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
⊢ (if x * y = 1 then 0 else 1) ≤ HAdd.hAdd (α := ℝ) (if x = 1 then 0 else 1) (if y = 1 then 0 else 1)
have 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)
Tactic: by_cases hx : x = 1
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Seminorm (goal)
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)
⊢ (if x * y = 1 then 0 else 1) ≤ HAdd.hAdd (α := ℝ) (if x = 1 then 0 else 1) (if y = 1 then 0 else 1)
have 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)
Tactic: by_cases hx : x = 1
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Seminorm (goal)
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 (α := ℝ) (if x = 1 then 0 else 1) (if y = 1 then 0 else 1)
have pos : (if x * y = 1 then 0 else 1) ≤ HAdd.hAdd (α := ℝ) 0 (if y = 1 then 0 else 1)
Tactic: rw [if_pos hx, hx, one_mul, zero_add]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Seminorm (goal)
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)
⊢ (if x * y = 1 then 0 else 1) ≤ HAdd.hAdd (α := ℝ) (if x = 1 then 0 else 1) (if y = 1 then 0 else 1)
have pos₁ : (if 1 * y = 1 then 0 else 1) ≤ HAdd.hAdd (α := ℝ) 0 (if y = 1 then 0 else 1)
Tactic: rw [if_pos hx, hx, one_mul, zero_add]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Seminorm (goal)
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)
⊢ (if x * y = 1 then 0 else 1) ≤ HAdd.hAdd (α := ℝ) (if x = 1 then 0 else 1) (if y = 1 then 0 else 1)
have pos₂ : (if y = 1 then 0 else 1) ≤ HAdd.hAdd (α := ℝ) 0 (if y = 1 then 0 else 1)
Tactic: rw [if_pos hx, hx, one_mul, zero_add]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Seminorm (goal)
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)
⊢ (if x * y = 1 then 0 else 1) ≤ HAdd.hAdd (α := ℝ) (if x = 1 then 0 else 1) (if y = 1 then 0 else 1)
have pos₃ : LE.le (α := ℝ) (if y = 1 then 0 else 1) (if y = 1 then 0 else 1)
Tactic: rw [if_pos hx, hx, one_mul, zero_add]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Seminorm (goal)
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 (α := ℝ) (if x = 1 then 0 else 1) (if y = 1 then 0 else 1)
have neg : (if x * y = 1 then 0 else 1) ≤ HAdd.hAdd (α := ℝ) 1 (if y = 1 then 0 else 1)
Tactic: rw [if_neg hx]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Seminorm (goal)
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)
have neg : LE.le (α := ℝ) (if x * y = 1 then 0 else 1) 1
Tactic: refine le_add_of_le_of_nonneg ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Seminorm (goal)
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
⊢ (if x * y = 1 then 0 else 1) ≤ HAdd.hAdd (α := ℝ) 1 (if y = 1 then 0 else 1)
have neg₁ : LE.le (α := ℝ) 0 (if y = 1 then 0 else 1)
Tactic: refine le_add_of_le_of_nonneg ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Seminorm (goal)
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
⊢ LE.le (α := ℝ) (if x * y = 1 then 0 else 1) 1
have pos : x * y = 1 → LE.le (α := ℝ) 0 1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Seminorm (goal)
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
⊢ LE.le (α := ℝ) (if x * y = 1 then 0 else 1) 1
have neg : ¬x * y = 1 → LE.le (α := ℝ) 1 1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Seminorm (goal)
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
⊢ LE.le (α := ℝ) 0 (if y = 1 then 0 else 1)
have pos : y = 1 → LE.le (α := ℝ) 0 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Seminorm (goal)
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
⊢ LE.le (α := ℝ) 0 (if y = 1 then 0 else 1)
have neg : ¬y = 1 → LE.le (α := ℝ) 0 1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Seminorm (goal)
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
⊢ HSMul.hSMul (β := ℝ) r ((p : (a : E) → ℝ) (x * x_1) : ℝ) ≤
    HSMul.hSMul (β := ℝ) r ((p : (a : E) → ℝ) x : ℝ) + HSMul.hSMul (β := ℝ) r ((p : (a : E) → ℝ) x_1 : ℝ)
have 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 : ℝ)
Tactic: simp only [← smul_one_smul ℝ≥0 r (_ : ℝ), NNReal.smul_def, smul_eq_mul, ← mul_add]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Seminorm (goal)
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
⊢ 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 : ℝ)
have hbc : (p : (a : E) → ℝ) (x * x_1) ≤ HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) x : ℝ) ((p : (a : E) → ℝ) x_1 : ℝ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Seminorm (goal)
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
⊢ 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))
have 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))
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Seminorm (goal)
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))
⊢ 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))
have 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))
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Seminorm (goal)
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 x + y = 0 then 0 else 1) (max (if x = 0 then 0 else 1) (if y = 0 then 0 else 1))
have pos : LE.le (α := ℝ) (if y = 0 then 0 else 1) (max 0 (if y = 0 then 0 else 1))
Tactic: simp_rw [if_pos hx, hx, zero_add]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Seminorm (goal)
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 x + y = 0 then 0 else 1) (max (if x = 0 then 0 else 1) (if y = 0 then 0 else 1))
have neg : LE.le (α := ℝ) (if x + y = 0 then 0 else 1) (max 1 (if y = 0 then 0 else 1))
Tactic: simp_rw [if_neg hx]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Seminorm (goal)
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 x + y = 0 then 0 else 1) (max 1 (if y = 0 then 0 else 1))
have pos : x + y = 0 → y = 0 → LE.le (α := ℝ) 0 (max 1 0)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Seminorm (goal)
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)
⊢ LE.le (α := ℝ) (if x + y = 0 then 0 else 1) (max 1 (if y = 0 then 0 else 1))
have neg : x + y = 0 → ¬y = 0 → LE.le (α := ℝ) 0 (max 1 1)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Seminorm (goal)
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)
⊢ LE.le (α := ℝ) (if x + y = 0 then 0 else 1) (max 1 (if y = 0 then 0 else 1))
have pos₁ : ¬x + y = 0 → y = 0 → LE.le (α := ℝ) 1 (max 1 0)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Seminorm (goal)
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)
⊢ LE.le (α := ℝ) (if x + y = 0 then 0 else 1) (max 1 (if y = 0 then 0 else 1))
have neg₁ : ¬x + y = 0 → ¬y = 0 → LE.le (α := ℝ) 1 (max 1 1)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Seminorm (goal)
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 : NonarchAddGroupSeminorm E
x y : E
⊢ HSMul.hSMul (β := ℝ) r ((p : (a : E) → ℝ) (x + y) : ℝ) ≤
    max (HSMul.hSMul (β := ℝ) r ((p : (a : E) → ℝ) x : ℝ)) (HSMul.hSMul (β := ℝ) r ((p : (a : E) → ℝ) y : ℝ))
have simp : HMul.hMul (β := ℝ) (↑(HSMul.hSMul (β := ℝ≥0) r 1) : ℝ) ((p : (a : E) → ℝ) (x + y) : ℝ) ≤
  HMul.hMul (β := ℝ) (↑(HSMul.hSMul (β := ℝ≥0) r 1) : ℝ) (max ((p : (a : E) → ℝ) x) ((p : (a : E) → ℝ) y) : ℝ)
Tactic: simp only [← smul_one_smul ℝ≥0 r (_ : ℝ), NNReal.smul_def, smul_eq_mul, ←
          mul_max_of_nonneg _ _ NNReal.zero_le_coe]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Seminorm (goal)
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 : NonarchAddGroupSeminorm E
x y : E
⊢ HMul.hMul (β := ℝ) (↑(HSMul.hSMul (β := ℝ≥0) r 1) : ℝ) ((p : (a : E) → ℝ) (x + y) : ℝ) ≤
    HMul.hMul (β := ℝ) (↑(HSMul.hSMul (β := ℝ≥0) r 1) : ℝ) (max ((p : (a : E) → ℝ) x) ((p : (a : E) → ℝ) y) : ℝ)
have hbc : LE.le (α := ℝ) ((p : (a : E) → ℝ) (x + y) : ℝ) (max ((p : (a : E) → ℝ) x) ((p : (a : E) → ℝ) y) : ℝ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Seminorm (goal)
Goal:
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst : Group E
p q f g : GroupNorm E
h : Eq.{max (u_3 + 1) 1} (α := (a : E) → ℝ) ((fun (f : GroupNorm E) ↦ f.toFun) f) ((fun (f : GroupNorm E) ↦ f.toFun) g)
⊢ f = g
have obtain : ∀ (toFun : E → ℝ) (map_one' : toFun 1 = 0) (mul_le' : ∀ (x y : E), toFun (x * y) ≤ toFun x + toFun y)
  (inv' : ∀ (x : E), toFun x⁻¹ = toFun x)
  (eq_one_of_map_eq_zero' :
    ∀ (x : E),
      { toFun := toFun, map_one' := map_one', mul_le' := mul_le', inv' := inv' : GroupSeminorm E }.toFun x = 0 → x = 1)
  (h :
    Eq.{max (u_3 + 1) 1} (α := (a : E) → ℝ)
      ((fun (f : GroupNorm E) ↦ f.toFun)
        { toFun := toFun, map_one' := map_one', mul_le' := mul_le', inv' := inv',
          eq_one_of_map_eq_zero' := eq_one_of_map_eq_zero' })
      ((fun (f : GroupNorm E) ↦ f.toFun) g)),
  { toFun := toFun, map_one' := map_one', mul_le' := mul_le', inv' := inv',
      eq_one_of_map_eq_zero' := eq_one_of_map_eq_zero' : GroupNorm E } =
    g
Tactic: obtain ⟨⟨_, _, _, _⟩, _⟩ := f
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Seminorm (goal)
Goal:
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst : Group E
p q g : GroupNorm E
toFun : E → ℝ
map_one' : toFun 1 = 0
mul_le' : ∀ (x y : E), toFun (x * y) ≤ toFun x + toFun y
inv' : ∀ (x : E), toFun x⁻¹ = toFun x
eq_one_of_map_eq_zero' :
  ∀ (x : E),
    { toFun := toFun, map_one' := map_one', mul_le' := mul_le', inv' := inv' : GroupSeminorm E }.toFun x = 0 → x = 1
h :
  Eq.{max (u_3 + 1) 1} (α := (a : E) → ℝ)
    ((fun (f : GroupNorm E) ↦ f.toFun)
      { toFun := toFun, map_one' := map_one', mul_le' := mul_le', inv' := inv',
        eq_one_of_map_eq_zero' := eq_one_of_map_eq_zero' })
    ((fun (f : GroupNorm E) ↦ f.toFun) g)
⊢ { toFun := toFun, map_one' := map_one', mul_le' := mul_le', inv' := inv',
      eq_one_of_map_eq_zero' := eq_one_of_map_eq_zero' : GroupNorm E } =
    g
have mk : ∀ (toGroupSeminorm : GroupSeminorm E) (eq_one_of_map_eq_zero'_1 : ∀ (x : E), toGroupSeminorm.toFun x = 0 → x = 1)
  (h :
    Eq.{max (u_3 + 1) 1} (α := (a : E) → ℝ)
      ((fun (f : GroupNorm E) ↦ f.toFun)
        { toFun := toFun, map_one' := map_one', mul_le' := mul_le', inv' := inv',
          eq_one_of_map_eq_zero' := eq_one_of_map_eq_zero' })
      ((fun (f : GroupNorm E) ↦ f.toFun)
        { toGroupSeminorm := toGroupSeminorm, eq_one_of_map_eq_zero' := eq_one_of_map_eq_zero'_1 })),
  { toFun := toFun, map_one' := map_one', mul_le' := mul_le', inv' := inv',
      eq_one_of_map_eq_zero' := eq_one_of_map_eq_zero' : GroupNorm E } =
    { toGroupSeminorm := toGroupSeminorm, eq_one_of_map_eq_zero' := eq_one_of_map_eq_zero'_1 }
Tactic: cases g
Cleared hypotheses: g, h