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 : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p_1 q_1 : Seminorm 𝕜 E
x_1 : E
p q : Seminorm 𝕜 E
a : 𝕜
x : E
ha : a ≠ 0
⊢ Eq (α := ℝ) (⨅ (u : E), HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) u : ℝ) ((q : (a : E) → ℝ) (a • x - u) : ℝ))
    (⨅ (i : E), HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) (a • i) : ℝ) ((q : (a : E) → ℝ) (a • x - a • i) : ℝ))
have inr : ∀ (u : E),
  HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) (HSMul.hSMul (β := E) a ((fun (x : E) ↦ a⁻¹ • x) u)) : ℝ)
      ((q : (a : E) → ℝ) (a • x - HSMul.hSMul (β := E) a ((fun (x : E) ↦ a⁻¹ • x) u)) : ℝ) =
    HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) u : ℝ) ((q : (a : E) → ℝ) (a • x - u) : ℝ)
Tactic: refine
          Function.Surjective.iInf_congr ((a⁻¹ • ·) : E → E)
            (fun u => ⟨a • u, inv_smul_smul₀ ha u⟩) fun u => ?_
-- 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
p_1 q_1 : Seminorm 𝕜 E
x_1 : E
p q : Seminorm 𝕜 E
a : 𝕜
x : E
ha : a ≠ 0
u : E
⊢ HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) (HSMul.hSMul (β := E) a ((fun (x : E) ↦ a⁻¹ • x) u)) : ℝ)
      ((q : (a : E) → ℝ) (a • x - HSMul.hSMul (β := E) a ((fun (x : E) ↦ a⁻¹ • x) u)) : ℝ) =
    HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) u : ℝ) ((q : (a : E) → ℝ) (a • x - u) : ℝ)
have inr : HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) u : ℝ) ((q : (a : E) → ℝ) (a • x - u) : ℝ) =
  HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) u : ℝ) ((q : (a : E) → ℝ) (a • x - u) : ℝ)
Tactic: rw [smul_inv_smul₀ ha]
-- 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
p_1 q_1 : Seminorm 𝕜 E
x_1 : E
p q : Seminorm 𝕜 E
x : E
⊢ HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) x : ℝ) ((q : (a : E) → ℝ) (x - x) : ℝ) ≤
    (fun (f : Seminorm 𝕜 E) ↦ ((⇑f : (a : E) → ℝ) : (a : E) → ℝ)) p x
have simp : LE.le (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ((p : (a : E) → ℝ) x : ℝ)
Tactic: simp only [sub_self, map_zero, add_zero]
-- 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
p_1 q_1 : Seminorm 𝕜 E
x_1 : E
p q : Seminorm 𝕜 E
x : E
⊢ HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) 0 : ℝ) ((q : (a : E) → ℝ) (x - 0) : ℝ) ≤
    (fun (f : Seminorm 𝕜 E) ↦ ((⇑f : (a : E) → ℝ) : (a : E) → ℝ)) q x
have simp : LE.le (α := ℝ) ((q : (a : E) → ℝ) x : ℝ) ((q : (a : E) → ℝ) x : ℝ)
Tactic: simp only [map_zero, zero_add, sub_zero]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
R : Type u_1
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SMul R ℝ
inst_4 : SMul R ℝ≥0
inst_5 : IsScalarTower R ℝ≥0 ℝ
r : R
p q : Seminorm 𝕜 E
⊢ r • (p ⊓ q) = r • p ⊓ r • q
have h : ∀ (x : E), Eq (α := ℝ) ((r • (p ⊓ q) : (a : E) → ℝ) x : ℝ) ((r • p ⊓ r • q : (a : E) → ℝ) x : ℝ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
R : Type u_1
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SMul R ℝ
inst_4 : SMul R ℝ≥0
inst_5 : IsScalarTower R ℝ≥0 ℝ
r : R
p q : Seminorm 𝕜 E
x : E
⊢ Eq (α := ℝ) ((r • (p ⊓ q) : (a : E) → ℝ) x : ℝ) ((r • p ⊓ r • q : (a : E) → ℝ) x : ℝ)
have h : HSMul.hSMul (β := ℝ) r ((p ⊓ q : (a : E) → ℝ) x : ℝ) = (r • p ⊓ r • q : (a : E) → ℝ) x
Tactic: simp_rw [smul_apply, inf_apply, smul_apply, ← smul_one_smul ℝ≥0 r (_ : ℝ), NNReal.smul_def,
    smul_eq_mul, Real.mul_iInf_of_nonneg (NNReal.coe_nonneg _), mul_add]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
R : Type u_1
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SMul R ℝ
inst_4 : SMul R ℝ≥0
inst_5 : IsScalarTower R ℝ≥0 ℝ
r : R
p q : Seminorm 𝕜 E
x : E
h : HSMul.hSMul (β := ℝ) r ((p ⊓ q : (a : E) → ℝ) x : ℝ) = (r • p ⊓ r • q : (a : E) → ℝ) x
⊢ Eq (α := ℝ) ((r • (p ⊓ q) : (a : E) → ℝ) x : ℝ) ((r • p ⊓ r • q : (a : E) → ℝ) x : ℝ)
have h₁ : HSMul.hSMul (β := ℝ) r
    (⨅ (u : E), HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) u : ℝ) ((q : (a : E) → ℝ) (x - u) : ℝ)) =
  ⨅ (u : E), HAdd.hAdd (α := ℝ) (β := ℝ) ((r • p : (a : E) → ℝ) u : ℝ) ((r • q : (a : E) → ℝ) (x - u) : ℝ)
Tactic: simp_rw [smul_apply, inf_apply, smul_apply, ← smul_one_smul ℝ≥0 r (_ : ℝ), NNReal.smul_def,
    smul_eq_mul, Real.mul_iInf_of_nonneg (NNReal.coe_nonneg _), mul_add]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
R : Type u_1
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SMul R ℝ
inst_4 : SMul R ℝ≥0
inst_5 : IsScalarTower R ℝ≥0 ℝ
r : R
p q : Seminorm 𝕜 E
x : E
h : HSMul.hSMul (β := ℝ) r ((p ⊓ q : (a : E) → ℝ) x : ℝ) = (r • p ⊓ r • q : (a : E) → ℝ) x
h₁ :
  HSMul.hSMul (β := ℝ) r
      (⨅ (u : E), HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) u : ℝ) ((q : (a : E) → ℝ) (x - u) : ℝ)) =
    ⨅ (u : E), HAdd.hAdd (α := ℝ) (β := ℝ) ((r • p : (a : E) → ℝ) u : ℝ) ((r • q : (a : E) → ℝ) (x - u) : ℝ)
⊢ Eq (α := ℝ) ((r • (p ⊓ q) : (a : E) → ℝ) x : ℝ) ((r • p ⊓ r • q : (a : E) → ℝ) x : ℝ)
have h₂ : HSMul.hSMul (β := ℝ) r
    (⨅ (u : E), HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) u : ℝ) ((q : (a : E) → ℝ) (x - u) : ℝ)) =
  ⨅ (u : E), HSMul.hSMul (β := ℝ) r ((p : (a : E) → ℝ) u : ℝ) + HSMul.hSMul (β := ℝ) r ((q : (a : E) → ℝ) (x - u) : ℝ)
Tactic: simp_rw [smul_apply, inf_apply, smul_apply, ← smul_one_smul ℝ≥0 r (_ : ℝ), NNReal.smul_def,
    smul_eq_mul, Real.mul_iInf_of_nonneg (NNReal.coe_nonneg _), mul_add]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
R : Type u_1
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SMul R ℝ
inst_4 : SMul R ℝ≥0
inst_5 : IsScalarTower R ℝ≥0 ℝ
r : R
p q : Seminorm 𝕜 E
x : E
h : HSMul.hSMul (β := ℝ) r ((p ⊓ q : (a : E) → ℝ) x : ℝ) = (r • p ⊓ r • q : (a : E) → ℝ) x
h₁ :
  HSMul.hSMul (β := ℝ) r
      (⨅ (u : E), HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) u : ℝ) ((q : (a : E) → ℝ) (x - u) : ℝ)) =
    ⨅ (u : E), HAdd.hAdd (α := ℝ) (β := ℝ) ((r • p : (a : E) → ℝ) u : ℝ) ((r • q : (a : E) → ℝ) (x - u) : ℝ)
h₂ :
  HSMul.hSMul (β := ℝ) r
      (⨅ (u : E), HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) u : ℝ) ((q : (a : E) → ℝ) (x - u) : ℝ)) =
    ⨅ (u : E), HSMul.hSMul (β := ℝ) r ((p : (a : E) → ℝ) u : ℝ) + HSMul.hSMul (β := ℝ) r ((q : (a : E) → ℝ) (x - u) : ℝ)
⊢ Eq (α := ℝ) ((r • (p ⊓ q) : (a : E) → ℝ) x : ℝ) ((r • p ⊓ r • q : (a : E) → ℝ) x : ℝ)
have h₃ : HSMul.hSMul (β := ℝ) (HSMul.hSMul (β := ℝ≥0) r 1)
    (⨅ (u : E), HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) u : ℝ) ((q : (a : E) → ℝ) (x - u) : ℝ)) =
  ⨅ (u : E),
    HSMul.hSMul (β := ℝ) (HSMul.hSMul (β := ℝ≥0) r 1) ((p : (a : E) → ℝ) u : ℝ) +
      HSMul.hSMul (β := ℝ) (HSMul.hSMul (β := ℝ≥0) r 1) ((q : (a : E) → ℝ) (x - u) : ℝ)
Tactic: simp_rw [smul_apply, inf_apply, smul_apply, ← smul_one_smul ℝ≥0 r (_ : ℝ), NNReal.smul_def,
    smul_eq_mul, Real.mul_iInf_of_nonneg (NNReal.coe_nonneg _), mul_add]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
R : Type u_1
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SMul R ℝ
inst_4 : SMul R ℝ≥0
inst_5 : IsScalarTower R ℝ≥0 ℝ
r : R
p q : Seminorm 𝕜 E
x : E
h : HSMul.hSMul (β := ℝ) r ((p ⊓ q : (a : E) → ℝ) x : ℝ) = (r • p ⊓ r • q : (a : E) → ℝ) x
h₁ :
  HSMul.hSMul (β := ℝ) r
      (⨅ (u : E), HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) u : ℝ) ((q : (a : E) → ℝ) (x - u) : ℝ)) =
    ⨅ (u : E), HAdd.hAdd (α := ℝ) (β := ℝ) ((r • p : (a : E) → ℝ) u : ℝ) ((r • q : (a : E) → ℝ) (x - u) : ℝ)
h₂ :
  HSMul.hSMul (β := ℝ) r
      (⨅ (u : E), HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) u : ℝ) ((q : (a : E) → ℝ) (x - u) : ℝ)) =
    ⨅ (u : E), HSMul.hSMul (β := ℝ) r ((p : (a : E) → ℝ) u : ℝ) + HSMul.hSMul (β := ℝ) r ((q : (a : E) → ℝ) (x - u) : ℝ)
h₃ :
  HSMul.hSMul (β := ℝ) (HSMul.hSMul (β := ℝ≥0) r 1)
      (⨅ (u : E), HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) u : ℝ) ((q : (a : E) → ℝ) (x - u) : ℝ)) =
    ⨅ (u : E),
      HSMul.hSMul (β := ℝ) (HSMul.hSMul (β := ℝ≥0) r 1) ((p : (a : E) → ℝ) u : ℝ) +
        HSMul.hSMul (β := ℝ) (HSMul.hSMul (β := ℝ≥0) r 1) ((q : (a : E) → ℝ) (x - u) : ℝ)
⊢ Eq (α := ℝ) ((r • (p ⊓ q) : (a : E) → ℝ) x : ℝ) ((r • p ⊓ r • q : (a : E) → ℝ) x : ℝ)
have h₄ : HSMul.hSMul (β := ℝ) (↑(HSMul.hSMul (β := ℝ≥0) r 1) : ℝ)
    (⨅ (u : E), HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) u : ℝ) ((q : (a : E) → ℝ) (x - u) : ℝ)) =
  ⨅ (u : E),
    HSMul.hSMul (β := ℝ) (↑(HSMul.hSMul (β := ℝ≥0) r 1) : ℝ) ((p : (a : E) → ℝ) u : ℝ) +
      HSMul.hSMul (β := ℝ) (↑(HSMul.hSMul (β := ℝ≥0) r 1) : ℝ) ((q : (a : E) → ℝ) (x - u) : ℝ)
Tactic: simp_rw [smul_apply, inf_apply, smul_apply, ← smul_one_smul ℝ≥0 r (_ : ℝ), NNReal.smul_def,
    smul_eq_mul, Real.mul_iInf_of_nonneg (NNReal.coe_nonneg _), mul_add]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
R : Type u_1
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SMul R ℝ
inst_4 : SMul R ℝ≥0
inst_5 : IsScalarTower R ℝ≥0 ℝ
r : R
p q : Seminorm 𝕜 E
x : E
h : HSMul.hSMul (β := ℝ) r ((p ⊓ q : (a : E) → ℝ) x : ℝ) = (r • p ⊓ r • q : (a : E) → ℝ) x
h₁ :
  HSMul.hSMul (β := ℝ) r
      (⨅ (u : E), HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) u : ℝ) ((q : (a : E) → ℝ) (x - u) : ℝ)) =
    ⨅ (u : E), HAdd.hAdd (α := ℝ) (β := ℝ) ((r • p : (a : E) → ℝ) u : ℝ) ((r • q : (a : E) → ℝ) (x - u) : ℝ)
h₂ :
  HSMul.hSMul (β := ℝ) r
      (⨅ (u : E), HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) u : ℝ) ((q : (a : E) → ℝ) (x - u) : ℝ)) =
    ⨅ (u : E), HSMul.hSMul (β := ℝ) r ((p : (a : E) → ℝ) u : ℝ) + HSMul.hSMul (β := ℝ) r ((q : (a : E) → ℝ) (x - u) : ℝ)
h₃ :
  HSMul.hSMul (β := ℝ) (HSMul.hSMul (β := ℝ≥0) r 1)
      (⨅ (u : E), HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) u : ℝ) ((q : (a : E) → ℝ) (x - u) : ℝ)) =
    ⨅ (u : E),
      HSMul.hSMul (β := ℝ) (HSMul.hSMul (β := ℝ≥0) r 1) ((p : (a : E) → ℝ) u : ℝ) +
        HSMul.hSMul (β := ℝ) (HSMul.hSMul (β := ℝ≥0) r 1) ((q : (a : E) → ℝ) (x - u) : ℝ)
h₄ :
  HSMul.hSMul (β := ℝ) (↑(HSMul.hSMul (β := ℝ≥0) r 1) : ℝ)
      (⨅ (u : E), HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) u : ℝ) ((q : (a : E) → ℝ) (x - u) : ℝ)) =
    ⨅ (u : E),
      HSMul.hSMul (β := ℝ) (↑(HSMul.hSMul (β := ℝ≥0) r 1) : ℝ) ((p : (a : E) → ℝ) u : ℝ) +
        HSMul.hSMul (β := ℝ) (↑(HSMul.hSMul (β := ℝ≥0) r 1) : ℝ) ((q : (a : E) → ℝ) (x - u) : ℝ)
⊢ Eq (α := ℝ) ((r • (p ⊓ q) : (a : E) → ℝ) x : ℝ) ((r • p ⊓ r • q : (a : E) → ℝ) x : ℝ)
have h₅ : (↑(HSMul.hSMul (β := ℝ≥0) r 1) : ℝ) *
    ⨅ (u : E), HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) u : ℝ) ((q : (a : E) → ℝ) (x - u) : ℝ) =
  ⨅ (u : E),
    HMul.hMul (β := ℝ) (↑(HSMul.hSMul (β := ℝ≥0) r 1) : ℝ) ((p : (a : E) → ℝ) u : ℝ) +
      HMul.hMul (β := ℝ) (↑(HSMul.hSMul (β := ℝ≥0) r 1) : ℝ) ((q : (a : E) → ℝ) (x - u) : ℝ)
Tactic: simp_rw [smul_apply, inf_apply, smul_apply, ← smul_one_smul ℝ≥0 r (_ : ℝ), NNReal.smul_def,
    smul_eq_mul, Real.mul_iInf_of_nonneg (NNReal.coe_nonneg _), mul_add]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
R : Type u_1
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SMul R ℝ
inst_4 : SMul R ℝ≥0
inst_5 : IsScalarTower R ℝ≥0 ℝ
r : R
p q : Seminorm 𝕜 E
x : E
h : HSMul.hSMul (β := ℝ) r ((p ⊓ q : (a : E) → ℝ) x : ℝ) = (r • p ⊓ r • q : (a : E) → ℝ) x
h₁ :
  HSMul.hSMul (β := ℝ) r
      (⨅ (u : E), HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) u : ℝ) ((q : (a : E) → ℝ) (x - u) : ℝ)) =
    ⨅ (u : E), HAdd.hAdd (α := ℝ) (β := ℝ) ((r • p : (a : E) → ℝ) u : ℝ) ((r • q : (a : E) → ℝ) (x - u) : ℝ)
h₂ :
  HSMul.hSMul (β := ℝ) r
      (⨅ (u : E), HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) u : ℝ) ((q : (a : E) → ℝ) (x - u) : ℝ)) =
    ⨅ (u : E), HSMul.hSMul (β := ℝ) r ((p : (a : E) → ℝ) u : ℝ) + HSMul.hSMul (β := ℝ) r ((q : (a : E) → ℝ) (x - u) : ℝ)
h₃ :
  HSMul.hSMul (β := ℝ) (HSMul.hSMul (β := ℝ≥0) r 1)
      (⨅ (u : E), HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) u : ℝ) ((q : (a : E) → ℝ) (x - u) : ℝ)) =
    ⨅ (u : E),
      HSMul.hSMul (β := ℝ) (HSMul.hSMul (β := ℝ≥0) r 1) ((p : (a : E) → ℝ) u : ℝ) +
        HSMul.hSMul (β := ℝ) (HSMul.hSMul (β := ℝ≥0) r 1) ((q : (a : E) → ℝ) (x - u) : ℝ)
h₄ :
  HSMul.hSMul (β := ℝ) (↑(HSMul.hSMul (β := ℝ≥0) r 1) : ℝ)
      (⨅ (u : E), HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) u : ℝ) ((q : (a : E) → ℝ) (x - u) : ℝ)) =
    ⨅ (u : E),
      HSMul.hSMul (β := ℝ) (↑(HSMul.hSMul (β := ℝ≥0) r 1) : ℝ) ((p : (a : E) → ℝ) u : ℝ) +
        HSMul.hSMul (β := ℝ) (↑(HSMul.hSMul (β := ℝ≥0) r 1) : ℝ) ((q : (a : E) → ℝ) (x - u) : ℝ)
h₅ :
  (↑(HSMul.hSMul (β := ℝ≥0) r 1) : ℝ) *
      ⨅ (u : E), HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) u : ℝ) ((q : (a : E) → ℝ) (x - u) : ℝ) =
    ⨅ (u : E),
      HMul.hMul (β := ℝ) (↑(HSMul.hSMul (β := ℝ≥0) r 1) : ℝ) ((p : (a : E) → ℝ) u : ℝ) +
        HMul.hMul (β := ℝ) (↑(HSMul.hSMul (β := ℝ≥0) r 1) : ℝ) ((q : (a : E) → ℝ) (x - u) : ℝ)
⊢ Eq (α := ℝ) ((r • (p ⊓ q) : (a : E) → ℝ) x : ℝ) ((r • p ⊓ r • q : (a : E) → ℝ) x : ℝ)
have h₆ : Eq (α := ℝ)
  (⨅ (i : E),
    (↑(HSMul.hSMul (β := ℝ≥0) r 1) : ℝ) *
      HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) i : ℝ) ((q : (a : E) → ℝ) (x - i) : ℝ))
  (⨅ (u : E),
    HMul.hMul (β := ℝ) (↑(HSMul.hSMul (β := ℝ≥0) r 1) : ℝ) ((p : (a : E) → ℝ) u : ℝ) +
      HMul.hMul (β := ℝ) (↑(HSMul.hSMul (β := ℝ≥0) r 1) : ℝ) ((q : (a : E) → ℝ) (x - u) : ℝ))
Tactic: simp_rw [smul_apply, inf_apply, smul_apply, ← smul_one_smul ℝ≥0 r (_ : ℝ), NNReal.smul_def,
    smul_eq_mul, Real.mul_iInf_of_nonneg (NNReal.coe_nonneg _), mul_add]
-- 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
p q : Seminorm 𝕜 E
x : E
s : Set (Seminorm 𝕜 E)
h : BddAbove (α := E → ℝ) (DFunLike.coe (β := fun (x : E) ↦ ℝ) '' s)
⊢ Eq (α := ℝ) ((⨆ (p : (↑s : Type u_7)), (⇑(↑p : Seminorm 𝕜 E) : (a : E) → ℝ)) 0) 0
have rw : Eq (α := ℝ) (⨆ (i : (↑s : Type u_7)), ((↑i : Seminorm 𝕜 E) : (a : E) → ℝ) 0) (⨆ (x : (↑s : Type u_7)), 0)
Tactic: rw [iSup_apply, ← @Real.iSup_const_zero s]
-- 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
p q : Seminorm 𝕜 E
x : E
s : Set (Seminorm 𝕜 E)
h : BddAbove (α := E → ℝ) (DFunLike.coe (β := fun (x : E) ↦ ℝ) '' s)
⊢ Eq (α := ℝ) (⨆ (i : (↑s : Type u_7)), ((↑i : Seminorm 𝕜 E) : (a : E) → ℝ) 0) (⨆ (x : (↑s : Type u_7)), 0)
have h₁ : ∀ (x : (↑s : Type u_7)), Eq (α := ℝ) (((↑x : Seminorm 𝕜 E) : (a : E) → ℝ) 0 : ℝ) (0 : ℝ)
Tactic: congr!
-- 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
p q : Seminorm 𝕜 E
x_1 : E
s : Set (Seminorm 𝕜 E)
h : BddAbove (α := E → ℝ) (DFunLike.coe (β := fun (x : E) ↦ ℝ) '' s)
x y : E
⊢ (⨆ (p : (↑s : Type u_7)), (⇑(↑p : Seminorm 𝕜 E) : (a : E) → ℝ)) (x + y) ≤
    HAdd.hAdd (α := ℝ) ((⨆ (p : (↑s : Type u_7)), (⇑(↑p : Seminorm 𝕜 E) : (a : E) → ℝ)) x)
      ((⨆ (p : (↑s : Type u_7)), (⇑(↑p : Seminorm 𝕜 E) : (a : E) → ℝ)) y)
have rcases : ∀ (q : E → ℝ) (hq : Membership.mem (γ := Set (E → ℝ)) (upperBounds (DFunLike.coe (β := fun (x : E) ↦ ℝ) '' s)) q),
  (⨆ (p : (↑s : Type u_7)), (⇑(↑p : Seminorm 𝕜 E) : (a : E) → ℝ)) (x + y) ≤
    HAdd.hAdd (α := ℝ) ((⨆ (p : (↑s : Type u_7)), (⇑(↑p : Seminorm 𝕜 E) : (a : E) → ℝ)) x)
      ((⨆ (p : (↑s : Type u_7)), (⇑(↑p : Seminorm 𝕜 E) : (a : E) → ℝ)) y)
Tactic: rcases h with ⟨q, hq⟩
Cleared hypotheses: 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
p q_1 : Seminorm 𝕜 E
x_1 : E
s : Set (Seminorm 𝕜 E)
x y : E
q : E → ℝ
hq : Membership.mem (γ := Set (E → ℝ)) (upperBounds (DFunLike.coe (β := fun (x : E) ↦ ℝ) '' s)) q
⊢ (⨆ (p : (↑s : Type u_7)), (⇑(↑p : Seminorm 𝕜 E) : (a : E) → ℝ)) (x + y) ≤
    HAdd.hAdd (α := ℝ) ((⨆ (p : (↑s : Type u_7)), (⇑(↑p : Seminorm 𝕜 E) : (a : E) → ℝ)) x)
      ((⨆ (p : (↑s : Type u_7)), (⇑(↑p : Seminorm 𝕜 E) : (a : E) → ℝ)) y)
have inl : ∀
  (hq :
    Membership.mem (γ := Set (E → ℝ)) (upperBounds (image (α := Seminorm 𝕜 E) (DFunLike.coe (β := fun (x : E) ↦ ℝ)) ∅))
      q),
  (⨆ (p : (↑∅ : Type u_7)), (⇑(↑p : Seminorm 𝕜 E) : (a : E) → ℝ)) (x + y) ≤
    HAdd.hAdd (α := ℝ) ((⨆ (p : (↑∅ : Type u_7)), (⇑(↑p : Seminorm 𝕜 E) : (a : E) → ℝ)) x)
      ((⨆ (p : (↑∅ : Type u_7)), (⇑(↑p : Seminorm 𝕜 E) : (a : E) → ℝ)) y)
Tactic: obtain rfl | h := s.eq_empty_or_nonempty
Cleared hypotheses: s, hq
-- 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
p q_1 : Seminorm 𝕜 E
x_1 : E
s : Set (Seminorm 𝕜 E)
x y : E
q : E → ℝ
hq : Membership.mem (γ := Set (E → ℝ)) (upperBounds (DFunLike.coe (β := fun (x : E) ↦ ℝ) '' s)) q
inl :
  ∀
    (hq :
      Membership.mem (γ := Set (E → ℝ))
        (upperBounds (image (α := Seminorm 𝕜 E) (DFunLike.coe (β := fun (x : E) ↦ ℝ)) ∅)) q),
    (⨆ (p : (↑∅ : Type u_7)), (⇑(↑p : Seminorm 𝕜 E) : (a : E) → ℝ)) (x + y) ≤
      HAdd.hAdd (α := ℝ) ((⨆ (p : (↑∅ : Type u_7)), (⇑(↑p : Seminorm 𝕜 E) : (a : E) → ℝ)) x)
        ((⨆ (p : (↑∅ : Type u_7)), (⇑(↑p : Seminorm 𝕜 E) : (a : E) → ℝ)) y)
⊢ (⨆ (p : (↑s : Type u_7)), (⇑(↑p : Seminorm 𝕜 E) : (a : E) → ℝ)) (x + y) ≤
    HAdd.hAdd (α := ℝ) ((⨆ (p : (↑s : Type u_7)), (⇑(↑p : Seminorm 𝕜 E) : (a : E) → ℝ)) x)
      ((⨆ (p : (↑s : Type u_7)), (⇑(↑p : Seminorm 𝕜 E) : (a : E) → ℝ)) y)
have inr : ∀ (h : s.Nonempty),
  (⨆ (p : (↑s : Type u_7)), (⇑(↑p : Seminorm 𝕜 E) : (a : E) → ℝ)) (x + y) ≤
    HAdd.hAdd (α := ℝ) ((⨆ (p : (↑s : Type u_7)), (⇑(↑p : Seminorm 𝕜 E) : (a : E) → ℝ)) x)
      ((⨆ (p : (↑s : Type u_7)), (⇑(↑p : Seminorm 𝕜 E) : (a : E) → ℝ)) y)
Tactic: obtain rfl | h := s.eq_empty_or_nonempty
-- 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
p q_1 : Seminorm 𝕜 E
x_1 : E
s : Set (Seminorm 𝕜 E)
x y : E
q : E → ℝ
hq : Membership.mem (γ := Set (E → ℝ)) (upperBounds (DFunLike.coe (β := fun (x : E) ↦ ℝ) '' s)) q
h : s.Nonempty
⊢ (⨆ (p : (↑s : Type u_7)), (⇑(↑p : Seminorm 𝕜 E) : (a : E) → ℝ)) (x + y) ≤
    HAdd.hAdd (α := ℝ) ((⨆ (p : (↑s : Type u_7)), (⇑(↑p : Seminorm 𝕜 E) : (a : E) → ℝ)) x)
      ((⨆ (p : (↑s : Type u_7)), (⇑(↑p : Seminorm 𝕜 E) : (a : E) → ℝ)) y)
have this : Nonempty.{u_7 + 1} (↑s : Type u_7)
Tactic: haveI : Nonempty ↑s := h.coe_sort
-- 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
p q_1 : Seminorm 𝕜 E
x_1 : E
s : Set (Seminorm 𝕜 E)
x y : E
q : E → ℝ
hq : Membership.mem (γ := Set (E → ℝ)) (upperBounds (DFunLike.coe (β := fun (x : E) ↦ ℝ) '' s)) q
h : s.Nonempty
this : Nonempty.{u_7 + 1} (↑s : Type u_7)
⊢ (⨆ (p : (↑s : Type u_7)), (⇑(↑p : Seminorm 𝕜 E) : (a : E) → ℝ)) (x + y) ≤
    HAdd.hAdd (α := ℝ) ((⨆ (p : (↑s : Type u_7)), (⇑(↑p : Seminorm 𝕜 E) : (a : E) → ℝ)) x)
      ((⨆ (p : (↑s : Type u_7)), (⇑(↑p : Seminorm 𝕜 E) : (a : E) → ℝ)) y)
have inr : ⨆ (i : (↑s : Type u_7)), ((↑i : Seminorm 𝕜 E) : (a : E) → ℝ) (x + y) ≤
  HAdd.hAdd (α := ℝ) (⨆ (i : (↑s : Type u_7)), ((↑i : Seminorm 𝕜 E) : (a : E) → ℝ) x)
    (⨆ (i : (↑s : Type u_7)), ((↑i : Seminorm 𝕜 E) : (a : E) → ℝ) y)
Tactic: simp only [iSup_apply]
-- 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
p q_1 : Seminorm 𝕜 E
x_1 : E
s : Set (Seminorm 𝕜 E)
x y : E
q : E → ℝ
hq : Membership.mem (γ := Set (E → ℝ)) (upperBounds (DFunLike.coe (β := fun (x : E) ↦ ℝ) '' s)) q
h : s.Nonempty
this : Nonempty.{u_7 + 1} (↑s : Type u_7)
⊢ ⨆ (i : (↑s : Type u_7)), ((↑i : Seminorm 𝕜 E) : (a : E) → ℝ) (x + y) ≤
    HAdd.hAdd (α := ℝ) (⨆ (i : (↑s : Type u_7)), ((↑i : Seminorm 𝕜 E) : (a : E) → ℝ) x)
      (⨆ (i : (↑s : Type u_7)), ((↑i : Seminorm 𝕜 E) : (a : E) → ℝ) y)
have inr : ∀ (i : (↑s : Type u_7)),
  Membership.mem (γ := Set ℝ)
    (upperBounds (range fun (i : { x : Seminorm 𝕜 E // x ∈ s }) ↦ (↑i : Seminorm 𝕜 E).toFun x)) (q x)
Tactic: refine ciSup_le fun i =>
            ((i : Seminorm 𝕜 E).add_le' x y).trans <| add_le_add
              -- Porting note: `f` is provided to force `Subtype.val` to appear.
              -- A type ascription on `_` would have also worked, but would have been more verbose.
              (le_ciSup (f := fun i => (Subtype.val i : Seminorm 𝕜 E).toFun x) ⟨q x, ?_⟩ i)
              (le_ciSup (f := fun i => (Subtype.val i : Seminorm 𝕜 E).toFun y) ⟨q y, ?_⟩ i)
-- 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
p q_1 : Seminorm 𝕜 E
x_1 : E
s : Set (Seminorm 𝕜 E)
x y : E
q : E → ℝ
hq : Membership.mem (γ := Set (E → ℝ)) (upperBounds (DFunLike.coe (β := fun (x : E) ↦ ℝ) '' s)) q
h : s.Nonempty
this : Nonempty.{u_7 + 1} (↑s : Type u_7)
inr :
  ∀ (i : (↑s : Type u_7)),
    Membership.mem (γ := Set ℝ)
      (upperBounds (range fun (i : { x : Seminorm 𝕜 E // x ∈ s }) ↦ (↑i : Seminorm 𝕜 E).toFun x)) (q x)
⊢ ⨆ (i : (↑s : Type u_7)), ((↑i : Seminorm 𝕜 E) : (a : E) → ℝ) (x + y) ≤
    HAdd.hAdd (α := ℝ) (⨆ (i : (↑s : Type u_7)), ((↑i : Seminorm 𝕜 E) : (a : E) → ℝ) x)
      (⨆ (i : (↑s : Type u_7)), ((↑i : Seminorm 𝕜 E) : (a : E) → ℝ) y)
have inr₁ : ∀ (i : (↑s : Type u_7)),
  Membership.mem (γ := Set ℝ)
    (upperBounds (range fun (i : { x : Seminorm 𝕜 E // x ∈ s }) ↦ (↑i : Seminorm 𝕜 E).toFun y)) (q y)
Tactic: refine ciSup_le fun i =>
            ((i : Seminorm 𝕜 E).add_le' x y).trans <| add_le_add
              -- Porting note: `f` is provided to force `Subtype.val` to appear.
              -- A type ascription on `_` would have also worked, but would have been more verbose.
              (le_ciSup (f := fun i => (Subtype.val i : Seminorm 𝕜 E).toFun x) ⟨q x, ?_⟩ i)
              (le_ciSup (f := fun i => (Subtype.val i : Seminorm 𝕜 E).toFun y) ⟨q y, ?_⟩ i)