awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
R : Type u_1
R' : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
𝕝 : Type u_6
E : Type u_7
E₂ : Type u_8
E₃ : Type u_9
F : Type u_10
ι : Type u_11
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
f : E → ℝ
add_le : ∀ (x y : E), f (x + y) ≤ f x + f y
smul : ∀ (a : 𝕜) (x : E), f (a • x) = ‖a‖ * f x
x : E
rw : f (HSMul.hSMul.{u_3, u_7, u_7} (α := 𝕜) (-1) x) = f x
rw₁ : norm.{u_3} (E := 𝕜) (-1) * f x = f x
⊢ f (-x) = f x
have rw₂ : norm.{u_3} (E := 𝕜) 1 * f x = f x
Tactic: rw [← neg_one_smul 𝕜, smul, norm_neg, ← smul, one_smul]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
R : Type u_1
R' : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
𝕝 : Type u_6
E : Type u_7
E₂ : Type u_8
E₃ : Type u_9
F : Type u_10
ι : Type u_11
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
f : E → ℝ
add_le : ∀ (x y : E), f (x + y) ≤ f x + f y
smul : ∀ (a : 𝕜) (x : E), f (a • x) = ‖a‖ * f x
x : E
rw : f (HSMul.hSMul.{u_3, u_7, u_7} (α := 𝕜) (-1) x) = f x
rw₁ : norm.{u_3} (E := 𝕜) (-1) * f x = f x
rw₂ : norm.{u_3} (E := 𝕜) 1 * f x = f x
⊢ f (-x) = f x
have rw₃ : f (HSMul.hSMul.{u_3, u_7, u_7} (α := 𝕜) 1 x) = f x
Tactic: rw [← neg_one_smul 𝕜, smul, norm_neg, ← smul, one_smul]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
R : Type u_1
R' : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
𝕝 : Type u_6
E : Type u_7
E₂ : Type u_8
E₃ : Type u_9
F : Type u_10
ι : Type u_11
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
f : E → ℝ
add_le : ∀ (x y : E), f (x + y) ≤ f x + f y
smul : ∀ (a : 𝕜) (x : E), f (a • x) = ‖a‖ * f x
x : E
rw : f (HSMul.hSMul.{u_3, u_7, u_7} (α := 𝕜) (-1) x) = f x
rw₁ : norm.{u_3} (E := 𝕜) (-1) * f x = f x
rw₂ : norm.{u_3} (E := 𝕜) 1 * f x = f x
rw₃ : f (HSMul.hSMul.{u_3, u_7, u_7} (α := 𝕜) 1 x) = f x
⊢ f (-x) = f x
have rw₄ : f x = f x
Tactic: rw [← neg_one_smul 𝕜, smul, norm_neg, ← smul, one_smul]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
R : Type u_1
R' : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
𝕝 : Type u_6
E : Type u_7
E₂ : Type u_8
E₃ : Type u_9
F : Type u_10
ι : Type u_11
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
f : E → ℝ
map_zero : f 0 = 0
add_le : ∀ (x y : E), f (x + y) ≤ f x + f y
smul_le : ∀ (r : 𝕜) (x : E), f (r • x) ≤ ‖r‖ * f x
r : 𝕜
x : E
⊢ f (r • x) = ‖r‖ * f x
have refine : ‖r‖ * f x ≤ f (r • x)
Tactic: refine le_antisymm (smul_le r x) ?_
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
R : Type u_1
R' : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
𝕝 : Type u_6
E : Type u_7
E₂ : Type u_8
E₃ : Type u_9
F : Type u_10
ι : Type u_11
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
f : E → ℝ
map_zero : f 0 = 0
add_le : ∀ (x y : E), f (x + y) ≤ f x + f y
smul_le : ∀ (r : 𝕜) (x : E), f (r • x) ≤ ‖r‖ * f x
r : 𝕜
x : E
⊢ ‖r‖ * f x ≤ f (r • x)
have pos : ∀ (h : r = 0), ‖r‖ * f x ≤ f (r • x)
Tactic: by_cases h : r = 0
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
R : Type u_1
R' : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
𝕝 : Type u_6
E : Type u_7
E₂ : Type u_8
E₃ : Type u_9
F : Type u_10
ι : Type u_11
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
f : E → ℝ
map_zero : f 0 = 0
add_le : ∀ (x y : E), f (x + y) ≤ f x + f y
smul_le : ∀ (r : 𝕜) (x : E), f (r • x) ≤ ‖r‖ * f x
r : 𝕜
x : E
pos : ∀ (h : r = 0), ‖r‖ * f x ≤ f (r • x)
⊢ ‖r‖ * f x ≤ f (r • x)
have neg : ∀ (h : ¬r = 0), ‖r‖ * f x ≤ f (r • x)
Tactic: by_cases h : r = 0
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
R : Type u_1
R' : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
𝕝 : Type u_6
E : Type u_7
E₂ : Type u_8
E₃ : Type u_9
F : Type u_10
ι : Type u_11
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
f : E → ℝ
map_zero : f 0 = 0
add_le : ∀ (x y : E), f (x + y) ≤ f x + f y
smul_le : ∀ (r : 𝕜) (x : E), f (r • x) ≤ ‖r‖ * f x
r : 𝕜
x : E
h : ¬r = 0
⊢ ‖r‖ * f x ≤ f (r • x)
have neg : ‖r‖⁻¹ * (‖r‖ * f x) ≤ ‖r‖⁻¹ * f (r • x)
Tactic: rw [← mul_le_mul_iff_right₀ (inv_pos.mpr (norm_pos_iff.mpr h))]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
R : Type u_1
R' : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
𝕝 : Type u_6
E : Type u_7
E₂ : Type u_8
E₃ : Type u_9
F : Type u_10
ι : Type u_11
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
f : E → ℝ
map_zero : f 0 = 0
add_le : ∀ (x y : E), f (x + y) ≤ f x + f y
smul_le : ∀ (r : 𝕜) (x : E), f (r • x) ≤ ‖r‖ * f x
r : 𝕜
x : E
h : ¬r = 0
⊢ ‖r‖⁻¹ * (‖r‖ * f x) ≤ ‖r‖⁻¹ * f (r • x)
have neg : f x ≤ ‖r‖⁻¹ * f (r • x)
Tactic: rw [inv_mul_cancel_left₀ (norm_ne_zero_iff.mpr h)]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (hypothesis)
Goal:
R : Type u_1
R' : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
𝕝 : Type u_6
E : Type u_7
E₂ : Type u_8
E₃ : Type u_9
F : Type u_10
ι : Type u_11
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
f : E → ℝ
map_zero : f 0 = 0
add_le : ∀ (x y : E), f (x + y) ≤ f x + f y
smul_le : ∀ (r : 𝕜) (x : E), f (r • x) ≤ ‖r‖ * f x
r : 𝕜
x : E
h : ¬r = 0
⊢ f x ≤ ‖r‖⁻¹ * f (r • x)
have smul_le₁ : f (r⁻¹ • r • x) ≤ ‖r⁻¹‖ * f (r • x)
Tactic: specialize smul_le r⁻¹ (r • x)
Cleared hypotheses: smul_le
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (hypothesis)
Goal:
R : Type u_1
R' : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
𝕝 : Type u_6
E : Type u_7
E₂ : Type u_8
E₃ : Type u_9
F : Type u_10
ι : Type u_11
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
f : E → ℝ
map_zero : f 0 = 0
add_le : ∀ (x y : E), f (x + y) ≤ f x + f y
r : 𝕜
x : E
h : ¬r = 0
smul_le : f (r⁻¹ • r • x) ≤ ‖r⁻¹‖ * f (r • x)
⊢ f x ≤ ‖r‖⁻¹ * f (r • x)
have smul_le₁ : f (r⁻¹ • r • x) ≤ ‖r‖⁻¹ * f (r • x)
Tactic: rw [norm_inv] at smul_le
Cleared hypotheses: smul_le
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
R : Type u_1
R' : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
𝕝 : Type u_6
E : Type u_7
E₂ : Type u_8
E₃ : Type u_9
F : Type u_10
ι : Type u_11
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
f : E → ℝ
map_zero : f 0 = 0
add_le : ∀ (x y : E), f (x + y) ≤ f x + f y
r : 𝕜
x : E
h : ¬r = 0
smul_le : f (r⁻¹ • r • x) ≤ ‖r‖⁻¹ * f (r • x)
⊢ f x ≤ ‖r‖⁻¹ * f (r • x)
have h₁ : x = r⁻¹ • r • x
Tactic: convert! smul_le
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
R : Type u_1
R' : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
𝕝 : Type u_6
E : Type u_7
E₂ : Type u_8
E₃ : Type u_9
F : Type u_10
ι : Type u_11
inst : SeminormedRing 𝕜
inst_1 : AddGroup E
inst_2 : SMul 𝕜 E
f g : Seminorm 𝕜 E
h :
  Eq.{max (u_7 + 1) 1} (α := (a : E) → ℝ) ((fun (f : Seminorm 𝕜 E) ↦ f.toFun) f) ((fun (f : Seminorm 𝕜 E) ↦ f.toFun) g)
⊢ f = g
have rcases : ∀ (toFun : E → ℝ) (map_zero' : toFun 0 = 0) (add_le' : ∀ (r s : E), toFun (r + s) ≤ toFun r + toFun s)
  (neg' : ∀ (r : E), toFun (-r) = toFun r)
  (smul' :
    ∀ (a : 𝕜) (x : E),
      { toFun := toFun, map_zero' := map_zero', add_le' := add_le', neg' := neg' : AddGroupSeminorm E }.toFun (a • x) =
        ‖a‖ * { toFun := toFun, map_zero' := map_zero', add_le' := add_le', neg' := neg' : AddGroupSeminorm E }.toFun x)
  (h :
    Eq.{max (u_7 + 1) 1} (α := (a : E) → ℝ)
      ((fun (f : Seminorm 𝕜 E) ↦ f.toFun)
        { toFun := toFun, map_zero' := map_zero', add_le' := add_le', neg' := neg', smul' := smul' })
      ((fun (f : Seminorm 𝕜 E) ↦ f.toFun) g)),
  { toFun := toFun, map_zero' := map_zero', add_le' := add_le', neg' := neg', smul' := smul' : Seminorm 𝕜 E } = g
Tactic: rcases f with ⟨⟨_⟩⟩
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
R : Type u_1
R' : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
𝕝 : Type u_6
E : Type u_7
E₂ : Type u_8
E₃ : Type u_9
F : Type u_10
ι : Type u_11
inst : SeminormedRing 𝕜
inst_1 : AddGroup E
inst_2 : SMul 𝕜 E
g : Seminorm 𝕜 E
toFun : E → ℝ
map_zero' : toFun 0 = 0
add_le' : ∀ (r s : E), toFun (r + s) ≤ toFun r + toFun s
neg' : ∀ (r : E), toFun (-r) = toFun r
smul' :
  ∀ (a : 𝕜) (x : E),
    { toFun := toFun, map_zero' := map_zero', add_le' := add_le', neg' := neg' : AddGroupSeminorm E }.toFun (a • x) =
      ‖a‖ * { toFun := toFun, map_zero' := map_zero', add_le' := add_le', neg' := neg' : AddGroupSeminorm E }.toFun x
h :
  Eq.{max (u_7 + 1) 1} (α := (a : E) → ℝ)
    ((fun (f : Seminorm 𝕜 E) ↦ f.toFun)
      { toFun := toFun, map_zero' := map_zero', add_le' := add_le', neg' := neg', smul' := smul' })
    ((fun (f : Seminorm 𝕜 E) ↦ f.toFun) g)
⊢ { toFun := toFun, map_zero' := map_zero', add_le' := add_le', neg' := neg', smul' := smul' : Seminorm 𝕜 E } = g
have rcases : ∀ (toFun_1 : E → ℝ) (map_zero'_1 : toFun_1 0 = 0) (add_le'_1 : ∀ (r s : E), toFun_1 (r + s) ≤ toFun_1 r + toFun_1 s)
  (neg'_1 : ∀ (r : E), toFun_1 (-r) = toFun_1 r)
  (smul'_1 :
    ∀ (a : 𝕜) (x : E),
      { toFun := toFun_1, map_zero' := map_zero'_1, add_le' := add_le'_1, neg' := neg'_1 : AddGroupSeminorm E }.toFun
          (a • x) =
        ‖a‖ *
          { toFun := toFun_1, map_zero' := map_zero'_1, add_le' := add_le'_1, neg' := neg'_1 :
                AddGroupSeminorm E }.toFun
            x)
  (h :
    Eq.{max (u_7 + 1) 1} (α := (a : E) → ℝ)
      ((fun (f : Seminorm 𝕜 E) ↦ f.toFun)
        { toFun := toFun, map_zero' := map_zero', add_le' := add_le', neg' := neg', smul' := smul' })
      ((fun (f : Seminorm 𝕜 E) ↦ f.toFun)
        { toFun := toFun_1, map_zero' := map_zero'_1, add_le' := add_le'_1, neg' := neg'_1, smul' := smul'_1 })),
  { toFun := toFun, map_zero' := map_zero', add_le' := add_le', neg' := neg', smul' := smul' : Seminorm 𝕜 E } =
    { toFun := toFun_1, map_zero' := map_zero'_1, add_le' := add_le'_1, neg' := neg'_1, smul' := smul'_1 }
Tactic: rcases g with ⟨⟨_⟩⟩
Cleared hypotheses: g, h
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
R : Type u_1
R' : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
𝕝 : Type u_6
E : Type u_7
E₂ : Type u_8
E₃ : Type u_9
F : Type u_10
ι : Type u_11
inst : SeminormedRing 𝕜
inst_1 : AddGroup E
inst_2 : SMul 𝕜 E
p_1 : Seminorm 𝕜 E
x : E
r_1 : ℝ
inst_3 : SMul R ℝ
inst_4 : SMul R ℝ≥0
inst_5 : IsScalarTower R ℝ≥0 ℝ
r : R
p : Seminorm 𝕜 E
x_1 : 𝕜
x_2 : E
⊢ HSMul.hSMul (β := ℝ) r ((p : (a : E) → ℝ) (x_1 • x_2) : ℝ) =
    ‖x_1‖ * HSMul.hSMul (β := ℝ) r ((p : (a : E) → ℝ) x_2 : ℝ)
have simp : HMul.hMul (β := ℝ) (↑(HSMul.hSMul (β := ℝ≥0) r 1) : ℝ) ((p : (a : E) → ℝ) (x_1 • x_2) : ℝ) =
  ‖x_1‖ * HMul.hMul (β := ℝ) (↑(HSMul.hSMul (β := ℝ≥0) r 1) : ℝ) ((p : (a : E) → ℝ) x_2 : ℝ)
Tactic: simp only [← smul_one_smul ℝ≥0 r (_ : ℝ), NNReal.smul_def, smul_eq_mul]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
R : Type u_1
R' : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
𝕝 : Type u_6
E : Type u_7
E₂ : Type u_8
E₃ : Type u_9
F : Type u_10
ι : Type u_11
inst : SeminormedRing 𝕜
inst_1 : AddGroup E
inst_2 : SMul 𝕜 E
p_1 : Seminorm 𝕜 E
x : E
r_1 : ℝ
inst_3 : SMul R ℝ
inst_4 : SMul R ℝ≥0
inst_5 : IsScalarTower R ℝ≥0 ℝ
r : R
p : Seminorm 𝕜 E
x_1 : 𝕜
x_2 : E
⊢ HMul.hMul (β := ℝ) (↑(HSMul.hSMul (β := ℝ≥0) r 1) : ℝ) ((p : (a : E) → ℝ) (x_1 • x_2) : ℝ) =
    ‖x_1‖ * HMul.hMul (β := ℝ) (↑(HSMul.hSMul (β := ℝ≥0) r 1) : ℝ) ((p : (a : E) → ℝ) x_2 : ℝ)
have rw : (↑(HSMul.hSMul (β := ℝ≥0) r 1) : ℝ) * HMul.hMul (β := ℝ) ‖x_1‖ ((p : (a : E) → ℝ) x_2 : ℝ) =
  ‖x_1‖ * HMul.hMul (β := ℝ) (↑(HSMul.hSMul (β := ℝ≥0) r 1) : ℝ) ((p : (a : E) → ℝ) x_2 : ℝ)
Tactic: rw [map_smul_eq_mul, mul_left_comm]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
R : Type u_1
R' : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
𝕝 : Type u_6
E : Type u_7
E₂ : Type u_8
E₃ : Type u_9
F : Type u_10
ι : Type u_11
inst : SeminormedRing 𝕜
inst_1 : AddGroup E
inst_2 : SMul 𝕜 E
p_1 : Seminorm 𝕜 E
x : E
r_1 : ℝ
inst_3 : SMul R ℝ
inst_4 : SMul R ℝ≥0
inst_5 : IsScalarTower R ℝ≥0 ℝ
r : R
p : Seminorm 𝕜 E
x_1 : 𝕜
x_2 : E
rw :
  (↑(HSMul.hSMul (β := ℝ≥0) r 1) : ℝ) * HMul.hMul (β := ℝ) ‖x_1‖ ((p : (a : E) → ℝ) x_2 : ℝ) =
    ‖x_1‖ * HMul.hMul (β := ℝ) (↑(HSMul.hSMul (β := ℝ≥0) r 1) : ℝ) ((p : (a : E) → ℝ) x_2 : ℝ)
⊢ HMul.hMul (β := ℝ) (↑(HSMul.hSMul (β := ℝ≥0) r 1) : ℝ) ((p : (a : E) → ℝ) (x_1 • x_2) : ℝ) =
    ‖x_1‖ * HMul.hMul (β := ℝ) (↑(HSMul.hSMul (β := ℝ≥0) r 1) : ℝ) ((p : (a : E) → ℝ) x_2 : ℝ)
have rw₁ : ‖x_1‖ * HMul.hMul (β := ℝ) (↑(HSMul.hSMul (β := ℝ≥0) r 1) : ℝ) ((p : (a : E) → ℝ) x_2 : ℝ) =
  ‖x_1‖ * HMul.hMul (β := ℝ) (↑(HSMul.hSMul (β := ℝ≥0) r 1) : ℝ) ((p : (a : E) → ℝ) x_2 : ℝ)
Tactic: rw [map_smul_eq_mul, mul_left_comm]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : ι → Seminorm 𝕜 E
x : E
⊢ 0 = (↑0 : ℝ)
have empty : Eq (α := ℕ) 0 0
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : ι → Seminorm 𝕜 E
x : E
a : ι
s : Finset ι
ha : a ∉ s
ih : (s.sup p : (a : E) → ℝ) x = (↑(s.sup fun (i : ι) ↦ NNReal.mk ((p i : (a : E) → ℝ) x) ⋯) : ℝ)
⊢ ((Finset.cons a s ha).sup p : (a : E) → ℝ) x =
    (↑((Finset.cons a s ha).sup fun (i : ι) ↦ NNReal.mk ((p i : (a : E) → ℝ) x) ⋯) : ℝ)
have cons : (p a ⊔ s.sup p : (a : E) → ℝ) x = (↑((Finset.cons a s ha).sup fun (i : ι) ↦ NNReal.mk ((p i : (a : E) → ℝ) x) sorry) : ℝ)
Tactic: rw [Finset.sup_cons, Finset.sup_cons, coe_sup, Pi.sup_apply, NNReal.coe_max, NNReal.coe_mk, ih]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : ι → Seminorm 𝕜 E
x : E
a : ι
s : Finset ι
ha : a ∉ s
ih : (s.sup p : (a : E) → ℝ) x = (↑(s.sup fun (i : ι) ↦ NNReal.mk ((p i : (a : E) → ℝ) x) ⋯) : ℝ)
cons :
  (p a ⊔ s.sup p : (a : E) → ℝ) x = (↑((Finset.cons a s ha).sup fun (i : ι) ↦ NNReal.mk ((p i : (a : E) → ℝ) x) ⋯) : ℝ)
⊢ ((Finset.cons a s ha).sup p : (a : E) → ℝ) x =
    (↑((Finset.cons a s ha).sup fun (i : ι) ↦ NNReal.mk ((p i : (a : E) → ℝ) x) ⋯) : ℝ)
have cons₁ : (p a ⊔ s.sup p : (a : E) → ℝ) x =
  (↑(max (NNReal.mk ((p a : (a : E) → ℝ) x) sorry) (s.sup fun (i : ι) ↦ NNReal.mk ((p i : (a : E) → ℝ) x) sorry)) : ℝ)
Tactic: rw [Finset.sup_cons, Finset.sup_cons, coe_sup, Pi.sup_apply, NNReal.coe_max, NNReal.coe_mk, ih]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : ι → Seminorm 𝕜 E
x : E
a : ι
s : Finset ι
ha : a ∉ s
ih : (s.sup p : (a : E) → ℝ) x = (↑(s.sup fun (i : ι) ↦ NNReal.mk ((p i : (a : E) → ℝ) x) ⋯) : ℝ)
cons :
  (p a ⊔ s.sup p : (a : E) → ℝ) x = (↑((Finset.cons a s ha).sup fun (i : ι) ↦ NNReal.mk ((p i : (a : E) → ℝ) x) ⋯) : ℝ)
cons₁ :
  (p a ⊔ s.sup p : (a : E) → ℝ) x =
    (↑(max (NNReal.mk ((p a : (a : E) → ℝ) x) ⋯) (s.sup fun (i : ι) ↦ NNReal.mk ((p i : (a : E) → ℝ) x) ⋯)) : ℝ)
⊢ ((Finset.cons a s ha).sup p : (a : E) → ℝ) x =
    (↑((Finset.cons a s ha).sup fun (i : ι) ↦ NNReal.mk ((p i : (a : E) → ℝ) x) ⋯) : ℝ)
have cons₂ : ((⇑(p a) : (a : E) → ℝ) ⊔ (⇑(s.sup p) : (a : E) → ℝ)) x =
  (↑(max (NNReal.mk ((p a : (a : E) → ℝ) x) sorry) (s.sup fun (i : ι) ↦ NNReal.mk ((p i : (a : E) → ℝ) x) sorry)) : ℝ)
Tactic: rw [Finset.sup_cons, Finset.sup_cons, coe_sup, Pi.sup_apply, NNReal.coe_max, NNReal.coe_mk, ih]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : ι → Seminorm 𝕜 E
x : E
a : ι
s : Finset ι
ha : a ∉ s
ih : (s.sup p : (a : E) → ℝ) x = (↑(s.sup fun (i : ι) ↦ NNReal.mk ((p i : (a : E) → ℝ) x) ⋯) : ℝ)
cons :
  (p a ⊔ s.sup p : (a : E) → ℝ) x = (↑((Finset.cons a s ha).sup fun (i : ι) ↦ NNReal.mk ((p i : (a : E) → ℝ) x) ⋯) : ℝ)
cons₁ :
  (p a ⊔ s.sup p : (a : E) → ℝ) x =
    (↑(max (NNReal.mk ((p a : (a : E) → ℝ) x) ⋯) (s.sup fun (i : ι) ↦ NNReal.mk ((p i : (a : E) → ℝ) x) ⋯)) : ℝ)
cons₂ :
  ((⇑(p a) : (a : E) → ℝ) ⊔ (⇑(s.sup p) : (a : E) → ℝ)) x =
    (↑(max (NNReal.mk ((p a : (a : E) → ℝ) x) ⋯) (s.sup fun (i : ι) ↦ NNReal.mk ((p i : (a : E) → ℝ) x) ⋯)) : ℝ)
⊢ ((Finset.cons a s ha).sup p : (a : E) → ℝ) x =
    (↑((Finset.cons a s ha).sup fun (i : ι) ↦ NNReal.mk ((p i : (a : E) → ℝ) x) ⋯) : ℝ)
have cons₃ : max ((p a : (a : E) → ℝ) x) ((s.sup p : (a : E) → ℝ) x) =
  (↑(max (NNReal.mk ((p a : (a : E) → ℝ) x) sorry) (s.sup fun (i : ι) ↦ NNReal.mk ((p i : (a : E) → ℝ) x) sorry)) : ℝ)
Tactic: rw [Finset.sup_cons, Finset.sup_cons, coe_sup, Pi.sup_apply, NNReal.coe_max, NNReal.coe_mk, ih]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : ι → Seminorm 𝕜 E
x : E
a : ι
s : Finset ι
ha : a ∉ s
ih : (s.sup p : (a : E) → ℝ) x = (↑(s.sup fun (i : ι) ↦ NNReal.mk ((p i : (a : E) → ℝ) x) ⋯) : ℝ)
cons :
  (p a ⊔ s.sup p : (a : E) → ℝ) x = (↑((Finset.cons a s ha).sup fun (i : ι) ↦ NNReal.mk ((p i : (a : E) → ℝ) x) ⋯) : ℝ)
cons₁ :
  (p a ⊔ s.sup p : (a : E) → ℝ) x =
    (↑(max (NNReal.mk ((p a : (a : E) → ℝ) x) ⋯) (s.sup fun (i : ι) ↦ NNReal.mk ((p i : (a : E) → ℝ) x) ⋯)) : ℝ)
cons₂ :
  ((⇑(p a) : (a : E) → ℝ) ⊔ (⇑(s.sup p) : (a : E) → ℝ)) x =
    (↑(max (NNReal.mk ((p a : (a : E) → ℝ) x) ⋯) (s.sup fun (i : ι) ↦ NNReal.mk ((p i : (a : E) → ℝ) x) ⋯)) : ℝ)
cons₃ :
  max ((p a : (a : E) → ℝ) x) ((s.sup p : (a : E) → ℝ) x) =
    (↑(max (NNReal.mk ((p a : (a : E) → ℝ) x) ⋯) (s.sup fun (i : ι) ↦ NNReal.mk ((p i : (a : E) → ℝ) x) ⋯)) : ℝ)
⊢ ((Finset.cons a s ha).sup p : (a : E) → ℝ) x =
    (↑((Finset.cons a s ha).sup fun (i : ι) ↦ NNReal.mk ((p i : (a : E) → ℝ) x) ⋯) : ℝ)
have cons₄ : max ((p a : (a : E) → ℝ) x) ((s.sup p : (a : E) → ℝ) x) =
  max (↑(NNReal.mk ((p a : (a : E) → ℝ) x) sorry) : ℝ) (↑(s.sup fun (i : ι) ↦ NNReal.mk ((p i : (a : E) → ℝ) x) sorry) : ℝ)
Tactic: rw [Finset.sup_cons, Finset.sup_cons, coe_sup, Pi.sup_apply, NNReal.coe_max, NNReal.coe_mk, ih]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : ι → Seminorm 𝕜 E
x : E
a : ι
s : Finset ι
ha : a ∉ s
ih : (s.sup p : (a : E) → ℝ) x = (↑(s.sup fun (i : ι) ↦ NNReal.mk ((p i : (a : E) → ℝ) x) ⋯) : ℝ)
cons :
  (p a ⊔ s.sup p : (a : E) → ℝ) x = (↑((Finset.cons a s ha).sup fun (i : ι) ↦ NNReal.mk ((p i : (a : E) → ℝ) x) ⋯) : ℝ)
cons₁ :
  (p a ⊔ s.sup p : (a : E) → ℝ) x =
    (↑(max (NNReal.mk ((p a : (a : E) → ℝ) x) ⋯) (s.sup fun (i : ι) ↦ NNReal.mk ((p i : (a : E) → ℝ) x) ⋯)) : ℝ)
cons₂ :
  ((⇑(p a) : (a : E) → ℝ) ⊔ (⇑(s.sup p) : (a : E) → ℝ)) x =
    (↑(max (NNReal.mk ((p a : (a : E) → ℝ) x) ⋯) (s.sup fun (i : ι) ↦ NNReal.mk ((p i : (a : E) → ℝ) x) ⋯)) : ℝ)
cons₃ :
  max ((p a : (a : E) → ℝ) x) ((s.sup p : (a : E) → ℝ) x) =
    (↑(max (NNReal.mk ((p a : (a : E) → ℝ) x) ⋯) (s.sup fun (i : ι) ↦ NNReal.mk ((p i : (a : E) → ℝ) x) ⋯)) : ℝ)
cons₄ :
  max ((p a : (a : E) → ℝ) x) ((s.sup p : (a : E) → ℝ) x) =
    max (↑(NNReal.mk ((p a : (a : E) → ℝ) x) ⋯) : ℝ) (↑(s.sup fun (i : ι) ↦ NNReal.mk ((p i : (a : E) → ℝ) x) ⋯) : ℝ)
⊢ ((Finset.cons a s ha).sup p : (a : E) → ℝ) x =
    (↑((Finset.cons a s ha).sup fun (i : ι) ↦ NNReal.mk ((p i : (a : E) → ℝ) x) ⋯) : ℝ)
have cons₅ : Eq (α := ℝ) (max ((p a : (a : E) → ℝ) x) ((s.sup p : (a : E) → ℝ) x) : ℝ)
  (max ((p a : (a : E) → ℝ) x) (↑(s.sup fun (i : ι) ↦ NNReal.mk ((p i : (a : E) → ℝ) x) sorry) : ℝ) : ℝ)
Tactic: rw [Finset.sup_cons, Finset.sup_cons, coe_sup, Pi.sup_apply, NNReal.coe_max, NNReal.coe_mk, ih]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : ι → Seminorm 𝕜 E
x : E
a : ι
s : Finset ι
ha : a ∉ s
ih : (s.sup p : (a : E) → ℝ) x = (↑(s.sup fun (i : ι) ↦ NNReal.mk ((p i : (a : E) → ℝ) x) ⋯) : ℝ)
cons :
  (p a ⊔ s.sup p : (a : E) → ℝ) x = (↑((Finset.cons a s ha).sup fun (i : ι) ↦ NNReal.mk ((p i : (a : E) → ℝ) x) ⋯) : ℝ)
cons₁ :
  (p a ⊔ s.sup p : (a : E) → ℝ) x =
    (↑(max (NNReal.mk ((p a : (a : E) → ℝ) x) ⋯) (s.sup fun (i : ι) ↦ NNReal.mk ((p i : (a : E) → ℝ) x) ⋯)) : ℝ)
cons₂ :
  ((⇑(p a) : (a : E) → ℝ) ⊔ (⇑(s.sup p) : (a : E) → ℝ)) x =
    (↑(max (NNReal.mk ((p a : (a : E) → ℝ) x) ⋯) (s.sup fun (i : ι) ↦ NNReal.mk ((p i : (a : E) → ℝ) x) ⋯)) : ℝ)
cons₃ :
  max ((p a : (a : E) → ℝ) x) ((s.sup p : (a : E) → ℝ) x) =
    (↑(max (NNReal.mk ((p a : (a : E) → ℝ) x) ⋯) (s.sup fun (i : ι) ↦ NNReal.mk ((p i : (a : E) → ℝ) x) ⋯)) : ℝ)
cons₄ :
  max ((p a : (a : E) → ℝ) x) ((s.sup p : (a : E) → ℝ) x) =
    max (↑(NNReal.mk ((p a : (a : E) → ℝ) x) ⋯) : ℝ) (↑(s.sup fun (i : ι) ↦ NNReal.mk ((p i : (a : E) → ℝ) x) ⋯) : ℝ)
cons₅ :
  Eq (α := ℝ) (max ((p a : (a : E) → ℝ) x) ((s.sup p : (a : E) → ℝ) x) : ℝ)
    (max ((p a : (a : E) → ℝ) x) (↑(s.sup fun (i : ι) ↦ NNReal.mk ((p i : (a : E) → ℝ) x) ⋯) : ℝ) : ℝ)
⊢ ((Finset.cons a s ha).sup p : (a : E) → ℝ) x =
    (↑((Finset.cons a s ha).sup fun (i : ι) ↦ NNReal.mk ((p i : (a : E) → ℝ) x) ⋯) : ℝ)
have cons₆ : Eq (α := ℝ) (max ((p a : (a : E) → ℝ) x) (↑(s.sup fun (i : ι) ↦ NNReal.mk ((p i : (a : E) → ℝ) x) sorry) : ℝ) : ℝ)
  (max ((p a : (a : E) → ℝ) x) (↑(s.sup fun (i : ι) ↦ NNReal.mk ((p i : (a : E) → ℝ) x) sorry) : ℝ) : ℝ)
Tactic: rw [Finset.sup_cons, Finset.sup_cons, coe_sup, Pi.sup_apply, NNReal.coe_max, NNReal.coe_mk, ih]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
x : E
⊢ (s.sup p : (a : E) → ℝ) x = (↑(s.sup fun (i : ι) ↦ NNReal.mk ((p i : (a : E) → ℝ) x) ⋯) : ℝ)
have empty : (Finset.sup ∅ p : (a : E) → ℝ) x = (↑(Finset.sup ∅ fun (i : ι) ↦ NNReal.mk ((p i : (a : E) → ℝ) x) sorry) : ℝ)
Tactic: induction s using Finset.cons_induction_on with
  | empty =>
    rw [Finset.sup_empty, Finset.sup_empty, coe_bot, _root_.bot_eq_zero, Pi.zero_apply]
    norm_cast
  | cons a s ha ih =>
    rw [Finset.sup_cons, Finset.sup_cons, coe_sup, Pi.sup_apply, NNReal.coe_max, NNReal.coe_mk, ih]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
x : E
empty : (Finset.sup ∅ p : (a : E) → ℝ) x = (↑(Finset.sup ∅ fun (i : ι) ↦ NNReal.mk ((p i : (a : E) → ℝ) x) ⋯) : ℝ)
⊢ (s.sup p : (a : E) → ℝ) x = (↑(s.sup fun (i : ι) ↦ NNReal.mk ((p i : (a : E) → ℝ) x) ⋯) : ℝ)
have cons : ∀ (a : ι) (s : Finset ι) (ha : a ∉ s)
  (ih : (s.sup p : (a : E) → ℝ) x = (↑(s.sup fun (i : ι) ↦ NNReal.mk ((p i : (a : E) → ℝ) x) sorry) : ℝ)),
  ((Finset.cons a s ha).sup p : (a : E) → ℝ) x =
    (↑((Finset.cons a s ha).sup fun (i : ι) ↦ NNReal.mk ((p i : (a : E) → ℝ) x) sorry) : ℝ)
Tactic: induction s using Finset.cons_induction_on with
  | empty =>
    rw [Finset.sup_empty, Finset.sup_empty, coe_bot, _root_.bot_eq_zero, Pi.zero_apply]
    norm_cast
  | cons a s ha ih =>
    rw [Finset.sup_cons, Finset.sup_cons, coe_sup, Pi.sup_apply, NNReal.coe_max, NNReal.coe_mk, ih]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
hs : s.Nonempty
x : E
⊢ ∃ i ∈ s, Eq (α := ℝ) ((s.sup p : (a : E) → ℝ) x : ℝ) ((p i : (a : E) → ℝ) x : ℝ)
have rcases : ∀ (i : ι) (hi : i ∈ s)
  (hix :
    Eq (α := { r : ℝ // 0 ≤ r })
      (s.sup fun (i : ι) ↦ Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) ((p i : (a : E) → ℝ) x) sorry : { r : ℝ // 0 ≤ r })
      (Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) ((p i : (a : E) → ℝ) x) sorry : { r : ℝ // 0 ≤ r })),
  ∃ i ∈ s, Eq (α := ℝ) ((s.sup p : (a : E) → ℝ) x : ℝ) ((p i : (a : E) → ℝ) x : ℝ)
Tactic: rcases Finset.exists_mem_eq_sup s hs (fun i ↦ (⟨p i x, apply_nonneg _ _⟩ : ℝ≥0)) with ⟨i, hi, hix⟩