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 : CommGroup E
inst_1 : CommGroup F
p_1 q_1 : GroupSeminorm E
x_1 : E
p q : GroupSeminorm E
x y u v : E
⊢ ⨅ (y_1 : E), HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) y_1 : ℝ) ((q : (a : E) → ℝ) (x * y / y_1) : ℝ) ≤
    HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) u : ℝ) ((q : (a : E) → ℝ) (x / u) : ℝ) +
      HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) v : ℝ) ((q : (a : E) → ℝ) (y / v) : ℝ)
have refine : HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) (u * v) : ℝ) ((q : (a : E) → ℝ) (x * y / (u * v)) : ℝ) ≤
  HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) u : ℝ) ((q : (a : E) → ℝ) (x / u) : ℝ) +
    HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) v : ℝ) ((q : (a : E) → ℝ) (y / v) : ℝ)
Tactic: refine ciInf_le_of_le mul_bddBelow_range_add (u * v) ?_
-- 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 : CommGroup E
inst_1 : CommGroup F
p_1 q_1 : GroupSeminorm E
x_1 : E
p q : GroupSeminorm E
x y u v : E
⊢ HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) (u * v) : ℝ) ((q : (a : E) → ℝ) (x * y / (u * v)) : ℝ) ≤
    HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) u : ℝ) ((q : (a : E) → ℝ) (x / u) : ℝ) +
      HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) v : ℝ) ((q : (a : E) → ℝ) (y / v) : ℝ)
have rw : HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) (u * v) : ℝ) ((q : (a : E) → ℝ) (x / u * (y / v)) : ℝ) ≤
  HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) u : ℝ) ((p : (a : E) → ℝ) v : ℝ) +
    HAdd.hAdd (α := ℝ) (β := ℝ) ((q : (a : E) → ℝ) (x / u) : ℝ) ((q : (a : E) → ℝ) (y / v) : ℝ)
Tactic: rw [mul_div_mul_comm, add_add_add_comm]
-- 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 : CommGroup E
inst_1 : CommGroup F
p_1 q_1 : GroupSeminorm E
x_1 : E
p q : GroupSeminorm E
x : E
⊢ Eq (α := ℝ)
    (⨅ (x_2 : E), HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) x_2⁻¹ : ℝ) ((q : (a : E) → ℝ) (x⁻¹ / x_2⁻¹) : ℝ))
    (⨅ (y : E), HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) y : ℝ) ((q : (a : E) → ℝ) (x / y) : ℝ))
have simp_rw : Eq (α := ℝ) (⨅ (x_2 : E), HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) x_2 : ℝ) ((q : (a : E) → ℝ) (x⁻¹ / x_2⁻¹) : ℝ))
  (⨅ (y : E), HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) y : ℝ) ((q : (a : E) → ℝ) (x / y) : ℝ))
Tactic: simp_rw [map_inv_eq_map p, ← inv_div', map_inv_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 : CommGroup E
inst_1 : CommGroup F
p_1 q_1 : GroupSeminorm E
x_1 : E
p q : GroupSeminorm E
x : E
simp_rw :
  Eq (α := ℝ)
    (⨅ (x_2 : E), HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) x_2 : ℝ) ((q : (a : E) → ℝ) (x⁻¹ / x_2⁻¹) : ℝ))
    (⨅ (y : E), HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) y : ℝ) ((q : (a : E) → ℝ) (x / y) : ℝ))
⊢ Eq (α := ℝ)
    (⨅ (x_2 : E), HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) x_2⁻¹ : ℝ) ((q : (a : E) → ℝ) (x⁻¹ / x_2⁻¹) : ℝ))
    (⨅ (y : E), HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) y : ℝ) ((q : (a : E) → ℝ) (x / y) : ℝ))
have simp_rw₁ : Eq (α := ℝ) (⨅ (x_2 : E), HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) x_2 : ℝ) ((q : (a : E) → ℝ) (x / x_2)⁻¹ : ℝ))
  (⨅ (y : E), HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) y : ℝ) ((q : (a : E) → ℝ) (x / y) : ℝ))
Tactic: simp_rw [map_inv_eq_map p, ← inv_div', map_inv_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 : 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) → ℝ) x : ℝ) ((q : (a : E) → ℝ) (x / x) : ℝ) ≤
    (fun (f : GroupSeminorm E) ↦ ((⇑f : (a : E) → ℝ) : (a : E) → ℝ)) p x
have rw : HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) x : ℝ) ((q : (a : E) → ℝ) 1 : ℝ) ≤
  (fun (f : GroupSeminorm E) ↦ ((⇑f : (a : E) → ℝ) : (a : E) → ℝ)) p x
Tactic: rw [div_self', map_one_eq_zero q, add_zero]
-- 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 : 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
⊢ HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) x : ℝ) ((q : (a : E) → ℝ) (x / x) : ℝ) ≤
    (fun (f : GroupSeminorm E) ↦ ((⇑f : (a : E) → ℝ) : (a : E) → ℝ)) p x
have rw₁ : HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) x : ℝ) (0 : ℝ) ≤
  (fun (f : GroupSeminorm E) ↦ ((⇑f : (a : E) → ℝ) : (a : E) → ℝ)) p x
Tactic: rw [div_self', map_one_eq_zero q, add_zero]
-- 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 : 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
⊢ HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) x : ℝ) ((q : (a : E) → ℝ) (x / x) : ℝ) ≤
    (fun (f : GroupSeminorm E) ↦ ((⇑f : (a : E) → ℝ) : (a : E) → ℝ)) p x
have rw₂ : LE.le (α := (fun (a : E) ↦ ℝ) x) ((p : (a : E) → ℝ) x : ℝ) ((p : (a : E) → ℝ) x : ℝ)
Tactic: rw [div_self', map_one_eq_zero q, add_zero]
-- 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
⊢ (if x + y = 0 then 0 else 1) ≤ HAdd.hAdd (α := ℝ) (if x = 0 then 0 else 1) (if y = 0 then 0 else 1)
have 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)
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), (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)
have 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)
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
⊢ (if x + y = 0 then 0 else 1) ≤ HAdd.hAdd (α := ℝ) (if x = 0 then 0 else 1) (if y = 0 then 0 else 1)
have pos : (if x + y = 0 then 0 else 1) ≤ HAdd.hAdd (α := ℝ) 0 (if y = 0 then 0 else 1)
Tactic: rw [if_pos hx, hx, zero_add, 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
pos : (if x + y = 0 then 0 else 1) ≤ HAdd.hAdd (α := ℝ) 0 (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)
have pos₁ : (if 0 + y = 0 then 0 else 1) ≤ HAdd.hAdd (α := ℝ) 0 (if y = 0 then 0 else 1)
Tactic: rw [if_pos hx, hx, zero_add, 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
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)
⊢ (if x + y = 0 then 0 else 1) ≤ HAdd.hAdd (α := ℝ) (if x = 0 then 0 else 1) (if y = 0 then 0 else 1)
have pos₂ : (if y = 0 then 0 else 1) ≤ HAdd.hAdd (α := ℝ) 0 (if y = 0 then 0 else 1)
Tactic: rw [if_pos hx, hx, zero_add, 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
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)
⊢ (if x + y = 0 then 0 else 1) ≤ HAdd.hAdd (α := ℝ) (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) (if y = 0 then 0 else 1)
Tactic: rw [if_pos hx, hx, zero_add, 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
⊢ (if x + y = 0 then 0 else 1) ≤ HAdd.hAdd (α := ℝ) (if x = 0 then 0 else 1) (if y = 0 then 0 else 1)
have neg : (if x + y = 0 then 0 else 1) ≤ HAdd.hAdd (α := ℝ) 1 (if y = 0 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 : 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)
have neg : LE.le (α := ℝ) (if x + y = 0 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 : 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
⊢ (if x + y = 0 then 0 else 1) ≤ HAdd.hAdd (α := ℝ) 1 (if y = 0 then 0 else 1)
have neg₁ : LE.le (α := ℝ) 0 (if y = 0 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 : 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) 1
have pos : x + y = 0 → 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 : 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
⊢ LE.le (α := ℝ) (if x + y = 0 then 0 else 1) 1
have neg : ¬x + y = 0 → 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 : 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 (α := ℝ) 0 (if y = 0 then 0 else 1)
have pos : y = 0 → 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 : 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
⊢ LE.le (α := ℝ) 0 (if y = 0 then 0 else 1)
have neg : ¬y = 0 → 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 : 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
⊢ 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 : 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
⊢ 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
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)
⊢ f = g
have 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
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 : 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)
⊢ { toFun := toFun, map_zero' := map_zero', add_le_max' := add_le_max', neg' := neg' : NonarchAddGroupSeminorm E } = g
have 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 }
Tactic: cases g
Cleared hypotheses: g, 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 q : NonarchAddGroupSeminorm E
r s : E
⊢ LE.le (α := ℝ) 0 (max 0 0)
have rw : LE.le (α := ℝ) 0 0
Tactic: rw [max_eq_right]
-- 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 q : NonarchAddGroupSeminorm E
s : Set (NonarchAddGroupSeminorm E)
h : BddAbove s
x y : E
⊢ 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))
have 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))
Tactic: obtain (rfl | hs) := eq_empty_or_nonempty s
Cleared hypotheses: s, 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 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))
⊢ 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))
have 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))
Tactic: obtain (rfl | hs) := eq_empty_or_nonempty s
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Seminorm (hypothesis)
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
⊢ 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))
have this : Nonempty.{u_3 + 1} (↑s : Type u_3)
Tactic: have : Nonempty s := hs.to_subtype
-- 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 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))
have 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) :
      ℝ)
Tactic: refine ciSup_le fun p ↦ (map_add_le_max p.1 x y).trans ?_
-- 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 (α := ℝ)
    (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) :
      ℝ)
have inr : LE.le (α := ℝ) (((↑p : NonarchAddGroupSeminorm E) : (a : E) → ℝ) x : ℝ)
  (⨆ (p : (↑s : Type u_3)), ((↑p : NonarchAddGroupSeminorm E) : (a : E) → ℝ) x : ℝ)
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
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 : ℝ)
⊢ 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) :
      ℝ)
have inr₁ : LE.le (α := ℝ) (((↑p : NonarchAddGroupSeminorm E) : (a : E) → ℝ) y : ℝ)
  (⨆ (p : (↑s : Type u_3)), ((↑p : NonarchAddGroupSeminorm E) : (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 : 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) → ℝ) x : ℝ)
    (⨆ (p : (↑s : Type u_3)), ((↑p : NonarchAddGroupSeminorm E) : (a : E) → ℝ) x : ℝ)
have 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)))
Tactic: apply le_ciSup (f := (DFunLike.coe · _) ∘ Subtype.val) ?_ p