awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Seminorm (goal)
Goal:
E : Type u_3
F : Type u_4
inst : AddGroup E
inst_1 : FunLike F E ℝ
inst_2 : NonarchAddGroupSeminormClass F E
f : F
x y : E
⊢ LE.le (α := ℝ) ((f : (a : E) → ℝ) (x - y) : ℝ) (max ((f : (a : E) → ℝ) x) ((f : (a : E) → ℝ) y) : ℝ)
have rw : LE.le (α := ℝ) ((f : (a : E) → ℝ) (x + -y) : ℝ) (max ((f : (a : E) → ℝ) x) ((f : (a : E) → ℝ) (-y)) : ℝ)
Tactic: rw [sub_eq_add_neg, ← NonarchAddGroupSeminormClass.map_neg_eq_map' f y]
-- 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 : FunLike F E ℝ
inst_1 : AddGroup E
inst_2 : NonarchAddGroupSeminormClass F E
f : F
x x_1 a : E
⊢ LE.le (α := ℝ) (0 : ℝ) ((f : (a : E) → ℝ) a : ℝ)
have rw : LE.le (α := ℝ) ((f : (a : E) → ℝ) (a - a) : ℝ) ((f : (a : E) → ℝ) a : ℝ)
Tactic: rw [← NonarchAddGroupSeminormClass.map_zero f, ← sub_self a]
-- 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 : FunLike F E ℝ
inst_1 : AddGroup E
inst_2 : NonarchAddGroupSeminormClass F E
f : F
x x_1 a : E
⊢ LE.le (α := ℝ) (max ((f : (a : E) → ℝ) a) ((f : (a : E) → ℝ) a) : ℝ) ((f : (a : E) → ℝ) a : ℝ)
have rw : LE.le (α := ℝ) ((f : (a : E) → ℝ) a : ℝ) ((f : (a : E) → ℝ) a : ℝ)
Tactic: rw [max_self (f a)]
-- 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 : Group F
inst_2 : Group G
p q f g : GroupSeminorm E
h :
  Eq.{max (u_3 + 1) 1} (α := (a : E) → ℝ) ((fun (f : GroupSeminorm E) ↦ f.toFun) f)
    ((fun (f : GroupSeminorm E) ↦ f.toFun) g)
⊢ f = g
have mk : ∀ (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)
  (h :
    Eq.{max (u_3 + 1) 1} (α := (a : E) → ℝ)
      ((fun (f : GroupSeminorm E) ↦ f.toFun) { toFun := toFun, map_one' := map_one', mul_le' := mul_le', inv' := inv' })
      ((fun (f : GroupSeminorm E) ↦ f.toFun) g)),
  { toFun := toFun, map_one' := map_one', mul_le' := mul_le', inv' := inv' : GroupSeminorm E } = g
Tactic: cases 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
inst_1 : Group F
inst_2 : Group G
p q g : GroupSeminorm 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
h :
  Eq.{max (u_3 + 1) 1} (α := (a : E) → ℝ)
    ((fun (f : GroupSeminorm E) ↦ f.toFun) { toFun := toFun, map_one' := map_one', mul_le' := mul_le', inv' := inv' })
    ((fun (f : GroupSeminorm E) ↦ f.toFun) g)
⊢ { toFun := toFun, map_one' := map_one', mul_le' := mul_le', inv' := inv' : GroupSeminorm E } = g
have mk : ∀ (toFun_1 : E → ℝ) (map_one'_1 : toFun_1 1 = 0) (mul_le'_1 : ∀ (x y : E), toFun_1 (x * y) ≤ toFun_1 x + toFun_1 y)
  (inv'_1 : ∀ (x : E), toFun_1 x⁻¹ = toFun_1 x)
  (h :
    Eq.{max (u_3 + 1) 1} (α := (a : E) → ℝ)
      ((fun (f : GroupSeminorm E) ↦ f.toFun) { toFun := toFun, map_one' := map_one', mul_le' := mul_le', inv' := inv' })
      ((fun (f : GroupSeminorm E) ↦ f.toFun)
        { toFun := toFun_1, map_one' := map_one'_1, mul_le' := mul_le'_1, inv' := inv'_1 })),
  { toFun := toFun, map_one' := map_one', mul_le' := mul_le', inv' := inv' : GroupSeminorm E } =
    { toFun := toFun_1, map_one' := map_one'_1, mul_le' := mul_le'_1, inv' := inv'_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 : Group E
inst_1 : Group F
inst_2 : Group G
p_1 q_1 : GroupSeminorm E
f : F →* E
p q : GroupSeminorm E
⊢ HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) 1 : ℝ) ((q : (a : E) → ℝ) 1 : ℝ) = 0
have simp_rw : HAdd.hAdd (α := ℝ) (β := ℝ) (0 : ℝ) ((q : (a : E) → ℝ) 1 : ℝ) = 0
Tactic: simp_rw [map_one_eq_zero p, map_one_eq_zero q, 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 : Group F
inst_2 : Group G
p_1 q_1 : GroupSeminorm E
f : F →* E
p q : GroupSeminorm E
simp_rw : HAdd.hAdd (α := ℝ) (β := ℝ) (0 : ℝ) ((q : (a : E) → ℝ) 1 : ℝ) = 0
⊢ HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) 1 : ℝ) ((q : (a : E) → ℝ) 1 : ℝ) = 0
have simp_rw₁ : HAdd.hAdd (α := ℝ) 0 0 = 0
Tactic: simp_rw [map_one_eq_zero p, map_one_eq_zero q, 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 : Group F
inst_2 : Group G
p_1 q_1 : GroupSeminorm E
f : F →* E
p q : GroupSeminorm E
x : E
⊢ HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) x⁻¹ : ℝ) ((q : (a : E) → ℝ) x⁻¹ : ℝ) =
    HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) x : ℝ) ((q : (a : E) → ℝ) x : ℝ)
have simp_rw : HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) x : ℝ) ((q : (a : E) → ℝ) x⁻¹ : ℝ) =
  HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) x : ℝ) ((q : (a : E) → ℝ) x : ℝ)
Tactic: simp_rw [map_inv_eq_map p, 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 : Group E
inst_1 : Group F
inst_2 : Group G
p q : GroupSeminorm E
f : F →* E
s : Set (GroupSeminorm E)
h : BddAbove s
x y : E
⊢ ⨆ (p : (↑s : Type u_3)), ((↑p : GroupSeminorm E) : (a : E) → ℝ) (x * y) ≤
    HAdd.hAdd (α := ℝ) (⨆ (p : (↑s : Type u_3)), ((↑p : GroupSeminorm E) : (a : E) → ℝ) x)
      (⨆ (p : (↑s : Type u_3)), ((↑p : GroupSeminorm E) : (a : E) → ℝ) y)
have inl : ∀ (h : BddAbove.{u_3} (α := GroupSeminorm E) ∅),
  ⨆ (p : (↑∅ : Type u_3)), ((↑p : GroupSeminorm E) : (a : E) → ℝ) (x * y) ≤
    HAdd.hAdd (α := ℝ) (⨆ (p : (↑∅ : Type u_3)), ((↑p : GroupSeminorm E) : (a : E) → ℝ) x)
      (⨆ (p : (↑∅ : Type u_3)), ((↑p : GroupSeminorm 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 : Group E
inst_1 : Group F
inst_2 : Group G
p q : GroupSeminorm E
f : F →* E
s : Set (GroupSeminorm E)
h : BddAbove s
x y : E
inl :
  ∀ (h : BddAbove.{u_3} (α := GroupSeminorm E) ∅),
    ⨆ (p : (↑∅ : Type u_3)), ((↑p : GroupSeminorm E) : (a : E) → ℝ) (x * y) ≤
      HAdd.hAdd (α := ℝ) (⨆ (p : (↑∅ : Type u_3)), ((↑p : GroupSeminorm E) : (a : E) → ℝ) x)
        (⨆ (p : (↑∅ : Type u_3)), ((↑p : GroupSeminorm E) : (a : E) → ℝ) y)
⊢ ⨆ (p : (↑s : Type u_3)), ((↑p : GroupSeminorm E) : (a : E) → ℝ) (x * y) ≤
    HAdd.hAdd (α := ℝ) (⨆ (p : (↑s : Type u_3)), ((↑p : GroupSeminorm E) : (a : E) → ℝ) x)
      (⨆ (p : (↑s : Type u_3)), ((↑p : GroupSeminorm E) : (a : E) → ℝ) y)
have inr : ∀ (hs : s.Nonempty),
  ⨆ (p : (↑s : Type u_3)), ((↑p : GroupSeminorm E) : (a : E) → ℝ) (x * y) ≤
    HAdd.hAdd (α := ℝ) (⨆ (p : (↑s : Type u_3)), ((↑p : GroupSeminorm E) : (a : E) → ℝ) x)
      (⨆ (p : (↑s : Type u_3)), ((↑p : GroupSeminorm 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 : Group E
inst_1 : Group F
inst_2 : Group G
p q : GroupSeminorm E
f : F →* E
s : Set (GroupSeminorm E)
h : BddAbove s
x y : E
hs : s.Nonempty
⊢ ⨆ (p : (↑s : Type u_3)), ((↑p : GroupSeminorm E) : (a : E) → ℝ) (x * y) ≤
    HAdd.hAdd (α := ℝ) (⨆ (p : (↑s : Type u_3)), ((↑p : GroupSeminorm E) : (a : E) → ℝ) x)
      (⨆ (p : (↑s : Type u_3)), ((↑p : GroupSeminorm 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 : Group E
inst_1 : Group F
inst_2 : Group G
p q : GroupSeminorm E
f : F →* E
s : Set (GroupSeminorm E)
h : BddAbove s
x y : E
hs : s.Nonempty
this : Nonempty.{u_3 + 1} (↑s : Type u_3)
⊢ ⨆ (p : (↑s : Type u_3)), ((↑p : GroupSeminorm E) : (a : E) → ℝ) (x * y) ≤
    HAdd.hAdd (α := ℝ) (⨆ (p : (↑s : Type u_3)), ((↑p : GroupSeminorm E) : (a : E) → ℝ) x)
      (⨆ (p : (↑s : Type u_3)), ((↑p : GroupSeminorm E) : (a : E) → ℝ) y)
have inr : ∀ (p : (↑s : Type u_3)),
  HAdd.hAdd (α := ℝ) (β := ℝ) (((↑p : GroupSeminorm E) : (a : E) → ℝ) x : ℝ)
      (((↑p : GroupSeminorm E) : (a : E) → ℝ) y : ℝ) ≤
    HAdd.hAdd (α := ℝ) (⨆ (p : (↑s : Type u_3)), ((↑p : GroupSeminorm E) : (a : E) → ℝ) x)
      (⨆ (p : (↑s : Type u_3)), ((↑p : GroupSeminorm E) : (a : E) → ℝ) y)
Tactic: refine ciSup_le fun p ↦ (map_mul_le_add 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 : Group E
inst_1 : Group F
inst_2 : Group G
p_1 q : GroupSeminorm E
f : F →* E
s : Set (GroupSeminorm E)
h : BddAbove s
x y : E
hs : s.Nonempty
this : Nonempty.{u_3 + 1} (↑s : Type u_3)
p : (↑s : Type u_3)
⊢ HAdd.hAdd (α := ℝ) (β := ℝ) (((↑p : GroupSeminorm E) : (a : E) → ℝ) x : ℝ)
      (((↑p : GroupSeminorm E) : (a : E) → ℝ) y : ℝ) ≤
    HAdd.hAdd (α := ℝ) (⨆ (p : (↑s : Type u_3)), ((↑p : GroupSeminorm E) : (a : E) → ℝ) x)
      (⨆ (p : (↑s : Type u_3)), ((↑p : GroupSeminorm E) : (a : E) → ℝ) y)
have inr : LE.le (α := ℝ) (((↑p : GroupSeminorm E) : (a : E) → ℝ) x : ℝ)
  (⨆ (p : (↑s : Type u_3)), ((↑p : GroupSeminorm 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 : Group E
inst_1 : Group F
inst_2 : Group G
p_1 q : GroupSeminorm E
f : F →* E
s : Set (GroupSeminorm 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 : GroupSeminorm E) : (a : E) → ℝ) x : ℝ)
    (⨆ (p : (↑s : Type u_3)), ((↑p : GroupSeminorm E) : (a : E) → ℝ) x : ℝ)
⊢ HAdd.hAdd (α := ℝ) (β := ℝ) (((↑p : GroupSeminorm E) : (a : E) → ℝ) x : ℝ)
      (((↑p : GroupSeminorm E) : (a : E) → ℝ) y : ℝ) ≤
    HAdd.hAdd (α := ℝ) (⨆ (p : (↑s : Type u_3)), ((↑p : GroupSeminorm E) : (a : E) → ℝ) x)
      (⨆ (p : (↑s : Type u_3)), ((↑p : GroupSeminorm E) : (a : E) → ℝ) y)
have inr₁ : LE.le (α := ℝ) (((↑p : GroupSeminorm E) : (a : E) → ℝ) y : ℝ)
  (⨆ (p : (↑s : Type u_3)), ((↑p : GroupSeminorm 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 : Group E
inst_1 : Group F
inst_2 : Group G
p_1 q : GroupSeminorm E
f : F →* E
s : Set (GroupSeminorm 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 : GroupSeminorm E) : (a : E) → ℝ) x : ℝ)
    (⨆ (p : (↑s : Type u_3)), ((↑p : GroupSeminorm E) : (a : E) → ℝ) x : ℝ)
have apply : BddAbove (α := ℝ)
  (range.{0, max 1 (u_3 + 1)} (ι := { x : GroupSeminorm E // x ∈ s })
    ((fun (x_1 : GroupSeminorm E) ↦ (x_1 : (a : E) → ℝ) x) ∘ Subtype.val (p := fun (x : GroupSeminorm 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:
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 : Group F
inst_2 : Group G
p_1 q : GroupSeminorm E
f : F →* E
s : Set (GroupSeminorm 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 : GroupSeminorm E) : (a : E) → ℝ) y : ℝ)
    (⨆ (p : (↑s : Type u_3)), ((↑p : GroupSeminorm E) : (a : E) → ℝ) y : ℝ)
have apply : BddAbove (α := ℝ)
  (range.{0, max 1 (u_3 + 1)} (ι := { x : GroupSeminorm E // x ∈ s })
    ((fun (x : GroupSeminorm E) ↦ (x : (a : E) → ℝ) y) ∘ Subtype.val (p := fun (x : GroupSeminorm 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 : Group E
s : Set (GroupSeminorm E)
hs : BddAbove s
x : E
⊢ Eq (α := ℝ) ((sSup s : (a : E) → ℝ) x : ℝ) (⨆ (p : (↑s : Type u_3)), ((↑p : GroupSeminorm E) : (a : E) → ℝ) x : ℝ)
have simp : Eq (α := ℝ)
  (({ toFun := fun (x : E) ↦ ⨆ (p : (↑s : Type u_3)), ((↑p : GroupSeminorm E) : (a : E) → ℝ) x, map_one' := sorry,
          mul_le' := sorry, inv' := sorry } :
        (a : E) → ℝ)
      x :
    ℝ)
  (⨆ (p : (↑s : Type u_3)), ((↑p : GroupSeminorm 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 : Group E
s : Set (GroupSeminorm E)
hs : BddAbove s
x : E
⊢ Eq (α := ℝ) ((sSup s : (a : E) → ℝ) x : ℝ) (sSup ((fun (x_1 : GroupSeminorm E) ↦ (x_1 : (a : E) → ℝ) x) '' s) : ℝ)
have rw : Eq (α := ℝ) (sSup (range fun (p : (↑s : Type u_3)) ↦ ((↑p : GroupSeminorm E) : (a : E) → ℝ) x))
  (sSup ((fun (x_1 : GroupSeminorm 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 : Group E
s : Set (GroupSeminorm E)
hs : BddAbove s
x : E
⊢ Eq (α := ℝ) (sSup (range fun (p : (↑s : Type u_3)) ↦ ((↑p : GroupSeminorm E) : (a : E) → ℝ) x))
    (sSup ((fun (x_1 : GroupSeminorm E) ↦ (x_1 : (a : E) → ℝ) x) '' s))
have e_a : Eq (α := Set ℝ) (range fun (p : (↑s : Type u_3)) ↦ ((↑p : GroupSeminorm E) : (a : E) → ℝ) x)
  ((fun (x_1 : GroupSeminorm 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 : Group E
s : Set (GroupSeminorm E)
hs : BddAbove s
x : E
⊢ Eq (α := Set ℝ) (range fun (p : (↑s : Type u_3)) ↦ ((↑p : GroupSeminorm E) : (a : E) → ℝ) x)
    ((fun (x_1 : GroupSeminorm E) ↦ (x_1 : (a : E) → ℝ) x) '' s)
have e_a : ∀ (x_1 : ℝ),
  Membership.mem (γ := Set ℝ) (range fun (p : (↑s : Type u_3)) ↦ ((↑p : GroupSeminorm E) : (a : E) → ℝ) x) x_1 ↔
    Membership.mem (γ := Set ℝ) ((fun (x_2 : GroupSeminorm 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 : Group E
ι : Type u_6
f : ι → GroupSeminorm 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 : GroupSeminorm 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 : Group E
inst_1 : Group F
inst_2 : Group G
p_1 q_1 : GroupSeminorm E
f : F →* E
p q : GroupSeminorm E
⊢ Eq (α := ℝ) (((⇑p : (a : E) → ℝ) ⊔ (⇑q : (a : E) → ℝ)) 1) 0
have rw : Eq (α := ℝ) (max ((p : (a : E) → ℝ) 1) ((q : (a : E) → ℝ) 1) : ℝ) (0 : ℝ)
Tactic: rw [Pi.sup_apply, ← map_one_eq_zero p, sup_eq_left, map_one_eq_zero p, map_one_eq_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 : Group E
inst_1 : Group F
inst_2 : Group G
p_1 q_1 : GroupSeminorm E
f : F →* E
p q : GroupSeminorm E
rw : Eq (α := ℝ) (max ((p : (a : E) → ℝ) 1) ((q : (a : E) → ℝ) 1) : ℝ) (0 : ℝ)
⊢ Eq (α := ℝ) (((⇑p : (a : E) → ℝ) ⊔ (⇑q : (a : E) → ℝ)) 1) 0
have rw₁ : Eq (α := ℝ) (max ((p : (a : E) → ℝ) 1) ((q : (a : E) → ℝ) 1) : ℝ) ((p : (a : E) → ℝ) 1 : ℝ)
Tactic: rw [Pi.sup_apply, ← map_one_eq_zero p, sup_eq_left, map_one_eq_zero p, map_one_eq_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 : Group E
inst_1 : Group F
inst_2 : Group G
p_1 q_1 : GroupSeminorm E
f : F →* E
p q : GroupSeminorm E
rw : Eq (α := ℝ) (max ((p : (a : E) → ℝ) 1) ((q : (a : E) → ℝ) 1) : ℝ) (0 : ℝ)
rw₁ : Eq (α := ℝ) (max ((p : (a : E) → ℝ) 1) ((q : (a : E) → ℝ) 1) : ℝ) ((p : (a : E) → ℝ) 1 : ℝ)
⊢ Eq (α := ℝ) (((⇑p : (a : E) → ℝ) ⊔ (⇑q : (a : E) → ℝ)) 1) 0
have rw₂ : LE.le (α := ℝ) ((q : (a : E) → ℝ) 1 : ℝ) ((p : (a : E) → ℝ) 1 : ℝ)
Tactic: rw [Pi.sup_apply, ← map_one_eq_zero p, sup_eq_left, map_one_eq_zero p, map_one_eq_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 : Group E
inst_1 : Group F
inst_2 : Group G
p_1 q_1 : GroupSeminorm E
f : F →* E
p q : GroupSeminorm E
rw : Eq (α := ℝ) (max ((p : (a : E) → ℝ) 1) ((q : (a : E) → ℝ) 1) : ℝ) (0 : ℝ)
rw₁ : Eq (α := ℝ) (max ((p : (a : E) → ℝ) 1) ((q : (a : E) → ℝ) 1) : ℝ) ((p : (a : E) → ℝ) 1 : ℝ)
rw₂ : LE.le (α := ℝ) ((q : (a : E) → ℝ) 1 : ℝ) ((p : (a : E) → ℝ) 1 : ℝ)
⊢ Eq (α := ℝ) (((⇑p : (a : E) → ℝ) ⊔ (⇑q : (a : E) → ℝ)) 1) 0
have rw₃ : LE.le (α := ℝ) ((q : (a : E) → ℝ) 1 : ℝ) (0 : ℝ)
Tactic: rw [Pi.sup_apply, ← map_one_eq_zero p, sup_eq_left, map_one_eq_zero p, map_one_eq_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 : Group E
inst_1 : Group F
inst_2 : Group G
p_1 q_1 : GroupSeminorm E
f : F →* E
p q : GroupSeminorm E
rw : Eq (α := ℝ) (max ((p : (a : E) → ℝ) 1) ((q : (a : E) → ℝ) 1) : ℝ) (0 : ℝ)
rw₁ : Eq (α := ℝ) (max ((p : (a : E) → ℝ) 1) ((q : (a : E) → ℝ) 1) : ℝ) ((p : (a : E) → ℝ) 1 : ℝ)
rw₂ : LE.le (α := ℝ) ((q : (a : E) → ℝ) 1 : ℝ) ((p : (a : E) → ℝ) 1 : ℝ)
rw₃ : LE.le (α := ℝ) ((q : (a : E) → ℝ) 1 : ℝ) (0 : ℝ)
⊢ Eq (α := ℝ) (((⇑p : (a : E) → ℝ) ⊔ (⇑q : (a : E) → ℝ)) 1) 0
have rw₄ : LE.le (α := ℝ) 0 0
Tactic: rw [Pi.sup_apply, ← map_one_eq_zero p, sup_eq_left, map_one_eq_zero p, map_one_eq_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 : Group E
inst_1 : Group F
inst_2 : Group G
p_1 q_1 : GroupSeminorm E
f : F →* E
p q : GroupSeminorm E
x : E
⊢ Eq (α := ℝ) (((⇑p : (a : E) → ℝ) ⊔ (⇑q : (a : E) → ℝ)) x⁻¹) (((⇑p : (a : E) → ℝ) ⊔ (⇑q : (a : E) → ℝ)) x)
have rw : Eq (α := ℝ) (max ((p : (a : E) → ℝ) x⁻¹) ((q : (a : E) → ℝ) x⁻¹) : ℝ) (((⇑p : (a : E) → ℝ) ⊔ (⇑q : (a : E) → ℝ)) x : ℝ)
Tactic: rw [Pi.sup_apply, Pi.sup_apply, map_inv_eq_map p, 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 : Group E
inst_1 : Group F
inst_2 : Group G
p_1 q_1 : GroupSeminorm E
f : F →* E
p q : GroupSeminorm E
x : E
rw :
  Eq (α := ℝ) (max ((p : (a : E) → ℝ) x⁻¹) ((q : (a : E) → ℝ) x⁻¹) : ℝ)
    (((⇑p : (a : E) → ℝ) ⊔ (⇑q : (a : E) → ℝ)) x : ℝ)
⊢ Eq (α := ℝ) (((⇑p : (a : E) → ℝ) ⊔ (⇑q : (a : E) → ℝ)) x⁻¹) (((⇑p : (a : E) → ℝ) ⊔ (⇑q : (a : E) → ℝ)) x)
have rw₁ : Eq (α := ℝ) (max ((p : (a : E) → ℝ) x⁻¹) ((q : (a : E) → ℝ) x⁻¹) : ℝ)
  (max ((p : (a : E) → ℝ) x) ((q : (a : E) → ℝ) x) : ℝ)
Tactic: rw [Pi.sup_apply, Pi.sup_apply, map_inv_eq_map p, 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 : Group E
inst_1 : Group F
inst_2 : Group G
p_1 q_1 : GroupSeminorm E
f : F →* E
p q : GroupSeminorm E
x : E
rw :
  Eq (α := ℝ) (max ((p : (a : E) → ℝ) x⁻¹) ((q : (a : E) → ℝ) x⁻¹) : ℝ)
    (((⇑p : (a : E) → ℝ) ⊔ (⇑q : (a : E) → ℝ)) x : ℝ)
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 rw₂ : Eq (α := ℝ) (max ((p : (a : E) → ℝ) x) ((q : (a : E) → ℝ) x⁻¹) : ℝ)
  (max ((p : (a : E) → ℝ) x) ((q : (a : E) → ℝ) x) : ℝ)
Tactic: rw [Pi.sup_apply, Pi.sup_apply, map_inv_eq_map p, 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 : Group E
inst_1 : Group F
inst_2 : Group G
p_1 q_1 : GroupSeminorm E
f : F →* E
p q : GroupSeminorm E
x : E
rw :
  Eq (α := ℝ) (max ((p : (a : E) → ℝ) x⁻¹) ((q : (a : E) → ℝ) x⁻¹) : ℝ)
    (((⇑p : (a : E) → ℝ) ⊔ (⇑q : (a : E) → ℝ)) x : ℝ)
rw₁ :
  Eq (α := ℝ) (max ((p : (a : E) → ℝ) x⁻¹) ((q : (a : E) → ℝ) x⁻¹) : ℝ)
    (max ((p : (a : E) → ℝ) x) ((q : (a : E) → ℝ) x) : ℝ)
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 rw₃ : Eq (α := ℝ) (max ((p : (a : E) → ℝ) x) ((q : (a : E) → ℝ) x) : ℝ) (max ((p : (a : E) → ℝ) x) ((q : (a : E) → ℝ) x) : ℝ)
Tactic: rw [Pi.sup_apply, Pi.sup_apply, map_inv_eq_map p, 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 : Group E
inst_1 : Group F
inst_2 : Group G
p_1 q : GroupSeminorm E
f_1 : F →* E
p : GroupSeminorm E
f : F →* E
⊢ Eq (α := ℝ) ((p : (a : E) → ℝ) ((f : (a : F) → E) 1 : E) : ℝ) (0 : ℝ)
have simp_rw : Eq (α := ℝ) ((p : (a : E) → ℝ) 1 : ℝ) (0 : ℝ)
Tactic: simp_rw [f.map_one, map_one_eq_zero p]
-- 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 : Group F
inst_2 : Group G
p_1 q : GroupSeminorm E
f_1 : F →* E
p : GroupSeminorm E
f : F →* E
x : F
⊢ Eq (α := ℝ) ((p : (a : E) → ℝ) ((f : (a : F) → E) x⁻¹ : E) : ℝ) ((p : (a : E) → ℝ) ((f : (a : F) → E) x : E) : ℝ)
have simp_rw : Eq (α := ℝ) ((p : (a : E) → ℝ) (((f : (a : F) → E) x)⁻¹ : E) : ℝ) ((p : (a : E) → ℝ) ((f : (a : F) → E) x : E) : ℝ)
Tactic: simp_rw [map_inv, map_inv_eq_map p]
-- 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 : E
p q : GroupSeminorm E
r : ℝ
hr : 0 < r
⊢ HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) 1 : ℝ) ((q : (a : E) → ℝ) (1 / 1) : ℝ) < r
have rwa : HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) 1 : ℝ) ((q : (a : E) → ℝ) 1 : ℝ) < r
Tactic: rwa [div_one, map_one_eq_zero p, 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 : E
p q : GroupSeminorm E
r : ℝ
hr : 0 < r
rwa : HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) 1 : ℝ) ((q : (a : E) → ℝ) 1 : ℝ) < r
⊢ HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) 1 : ℝ) ((q : (a : E) → ℝ) (1 / 1) : ℝ) < r
have rwa₁ : HAdd.hAdd (α := ℝ) (β := ℝ) (0 : ℝ) ((q : (a : E) → ℝ) 1 : ℝ) < r
Tactic: rwa [div_one, map_one_eq_zero p, 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 : E
p q : GroupSeminorm E
r : ℝ
hr : 0 < r
rwa : HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) 1 : ℝ) ((q : (a : E) → ℝ) 1 : ℝ) < r
rwa₁ : HAdd.hAdd (α := ℝ) (β := ℝ) (0 : ℝ) ((q : (a : E) → ℝ) 1 : ℝ) < r
⊢ HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) 1 : ℝ) ((q : (a : E) → ℝ) (1 / 1) : ℝ) < r
have rwa₂ : HAdd.hAdd (α := ℝ) 0 0 < r
Tactic: rwa [div_one, map_one_eq_zero p, map_one_eq_zero q, add_zero]