awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
y : E
r : ℝ
a : 𝕜
ha : a ≠ 0
x : E
⊢ Membership.mem (γ := Set E) ((fun (x : E) ↦ a • x) ⁻¹' p.closedBall y r) x ↔ x ∈ p.closedBall (a⁻¹ • y) (r / ‖a‖)
have rw : a • x ∈ p.closedBall y r ↔ x ∈ p.closedBall (a⁻¹ • y) (r / ‖a‖)
Tactic: rw [mem_preimage, mem_closedBall, mem_closedBall, le_div_iff₀ (norm_pos_iff.mpr ha), mul_comm, ←
      map_smul_eq_mul p, smul_sub, smul_inv_smul₀ ha]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
y : E
r : ℝ
a : 𝕜
ha : a ≠ 0
x : E
rw : a • x ∈ p.closedBall y r ↔ x ∈ p.closedBall (a⁻¹ • y) (r / ‖a‖)
⊢ Membership.mem (γ := Set E) ((fun (x : E) ↦ a • x) ⁻¹' p.closedBall y r) x ↔ x ∈ p.closedBall (a⁻¹ • y) (r / ‖a‖)
have rw₁ : (p : (a : E) → ℝ) (a • x - y) ≤ r ↔ x ∈ p.closedBall (a⁻¹ • y) (r / ‖a‖)
Tactic: rw [mem_preimage, mem_closedBall, mem_closedBall, le_div_iff₀ (norm_pos_iff.mpr ha), mul_comm, ←
      map_smul_eq_mul p, smul_sub, smul_inv_smul₀ ha]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
y : E
r : ℝ
a : 𝕜
ha : a ≠ 0
x : E
rw : a • x ∈ p.closedBall y r ↔ x ∈ p.closedBall (a⁻¹ • y) (r / ‖a‖)
rw₁ : (p : (a : E) → ℝ) (a • x - y) ≤ r ↔ x ∈ p.closedBall (a⁻¹ • y) (r / ‖a‖)
⊢ Membership.mem (γ := Set E) ((fun (x : E) ↦ a • x) ⁻¹' p.closedBall y r) x ↔ x ∈ p.closedBall (a⁻¹ • y) (r / ‖a‖)
have rw₂ : (p : (a : E) → ℝ) (a • x - y) ≤ r ↔ (p : (a : E) → ℝ) (x - a⁻¹ • y) ≤ r / ‖a‖
Tactic: rw [mem_preimage, mem_closedBall, mem_closedBall, le_div_iff₀ (norm_pos_iff.mpr ha), mul_comm, ←
      map_smul_eq_mul p, smul_sub, smul_inv_smul₀ ha]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
y : E
r : ℝ
a : 𝕜
ha : a ≠ 0
x : E
rw : a • x ∈ p.closedBall y r ↔ x ∈ p.closedBall (a⁻¹ • y) (r / ‖a‖)
rw₁ : (p : (a : E) → ℝ) (a • x - y) ≤ r ↔ x ∈ p.closedBall (a⁻¹ • y) (r / ‖a‖)
rw₂ : (p : (a : E) → ℝ) (a • x - y) ≤ r ↔ (p : (a : E) → ℝ) (x - a⁻¹ • y) ≤ r / ‖a‖
⊢ Membership.mem (γ := Set E) ((fun (x : E) ↦ a • x) ⁻¹' p.closedBall y r) x ↔ x ∈ p.closedBall (a⁻¹ • y) (r / ‖a‖)
have rw₃ : (p : (a : E) → ℝ) (a • x - y) ≤ r ↔ HMul.hMul (α := ℝ) ((p : (a : E) → ℝ) (x - a⁻¹ • y) : ℝ) ‖a‖ ≤ r
Tactic: rw [mem_preimage, mem_closedBall, mem_closedBall, le_div_iff₀ (norm_pos_iff.mpr ha), mul_comm, ←
      map_smul_eq_mul p, smul_sub, smul_inv_smul₀ ha]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
y : E
r : ℝ
a : 𝕜
ha : a ≠ 0
x : E
rw : a • x ∈ p.closedBall y r ↔ x ∈ p.closedBall (a⁻¹ • y) (r / ‖a‖)
rw₁ : (p : (a : E) → ℝ) (a • x - y) ≤ r ↔ x ∈ p.closedBall (a⁻¹ • y) (r / ‖a‖)
rw₂ : (p : (a : E) → ℝ) (a • x - y) ≤ r ↔ (p : (a : E) → ℝ) (x - a⁻¹ • y) ≤ r / ‖a‖
rw₃ : (p : (a : E) → ℝ) (a • x - y) ≤ r ↔ HMul.hMul (α := ℝ) ((p : (a : E) → ℝ) (x - a⁻¹ • y) : ℝ) ‖a‖ ≤ r
⊢ Membership.mem (γ := Set E) ((fun (x : E) ↦ a • x) ⁻¹' p.closedBall y r) x ↔ x ∈ p.closedBall (a⁻¹ • y) (r / ‖a‖)
have rw₄ : (p : (a : E) → ℝ) (a • x - y) ≤ r ↔ HMul.hMul (β := ℝ) ‖a‖ ((p : (a : E) → ℝ) (x - a⁻¹ • y) : ℝ) ≤ r
Tactic: rw [mem_preimage, mem_closedBall, mem_closedBall, le_div_iff₀ (norm_pos_iff.mpr ha), mul_comm, ←
      map_smul_eq_mul p, smul_sub, smul_inv_smul₀ ha]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
y : E
r : ℝ
a : 𝕜
ha : a ≠ 0
x : E
rw : a • x ∈ p.closedBall y r ↔ x ∈ p.closedBall (a⁻¹ • y) (r / ‖a‖)
rw₁ : (p : (a : E) → ℝ) (a • x - y) ≤ r ↔ x ∈ p.closedBall (a⁻¹ • y) (r / ‖a‖)
rw₂ : (p : (a : E) → ℝ) (a • x - y) ≤ r ↔ (p : (a : E) → ℝ) (x - a⁻¹ • y) ≤ r / ‖a‖
rw₃ : (p : (a : E) → ℝ) (a • x - y) ≤ r ↔ HMul.hMul (α := ℝ) ((p : (a : E) → ℝ) (x - a⁻¹ • y) : ℝ) ‖a‖ ≤ r
rw₄ : (p : (a : E) → ℝ) (a • x - y) ≤ r ↔ HMul.hMul (β := ℝ) ‖a‖ ((p : (a : E) → ℝ) (x - a⁻¹ • y) : ℝ) ≤ r
⊢ Membership.mem (γ := Set E) ((fun (x : E) ↦ a • x) ⁻¹' p.closedBall y r) x ↔ x ∈ p.closedBall (a⁻¹ • y) (r / ‖a‖)
have rw₅ : (p : (a : E) → ℝ) (a • x - y) ≤ r ↔ (p : (a : E) → ℝ) (a • (x - a⁻¹ • y)) ≤ r
Tactic: rw [mem_preimage, mem_closedBall, mem_closedBall, le_div_iff₀ (norm_pos_iff.mpr ha), mul_comm, ←
      map_smul_eq_mul p, smul_sub, smul_inv_smul₀ ha]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
y : E
r : ℝ
a : 𝕜
ha : a ≠ 0
x : E
rw : a • x ∈ p.closedBall y r ↔ x ∈ p.closedBall (a⁻¹ • y) (r / ‖a‖)
rw₁ : (p : (a : E) → ℝ) (a • x - y) ≤ r ↔ x ∈ p.closedBall (a⁻¹ • y) (r / ‖a‖)
rw₂ : (p : (a : E) → ℝ) (a • x - y) ≤ r ↔ (p : (a : E) → ℝ) (x - a⁻¹ • y) ≤ r / ‖a‖
rw₃ : (p : (a : E) → ℝ) (a • x - y) ≤ r ↔ HMul.hMul (α := ℝ) ((p : (a : E) → ℝ) (x - a⁻¹ • y) : ℝ) ‖a‖ ≤ r
rw₄ : (p : (a : E) → ℝ) (a • x - y) ≤ r ↔ HMul.hMul (β := ℝ) ‖a‖ ((p : (a : E) → ℝ) (x - a⁻¹ • y) : ℝ) ≤ r
rw₅ : (p : (a : E) → ℝ) (a • x - y) ≤ r ↔ (p : (a : E) → ℝ) (a • (x - a⁻¹ • y)) ≤ r
⊢ Membership.mem (γ := Set E) ((fun (x : E) ↦ a • x) ⁻¹' p.closedBall y r) x ↔ x ∈ p.closedBall (a⁻¹ • y) (r / ‖a‖)
have rw₆ : (p : (a : E) → ℝ) (a • x - y) ≤ r ↔ (p : (a : E) → ℝ) (a • x - a • a⁻¹ • y) ≤ r
Tactic: rw [mem_preimage, mem_closedBall, mem_closedBall, le_div_iff₀ (norm_pos_iff.mpr ha), mul_comm, ←
      map_smul_eq_mul p, smul_sub, smul_inv_smul₀ ha]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
y : E
r : ℝ
a : 𝕜
ha : a ≠ 0
x : E
rw : a • x ∈ p.closedBall y r ↔ x ∈ p.closedBall (a⁻¹ • y) (r / ‖a‖)
rw₁ : (p : (a : E) → ℝ) (a • x - y) ≤ r ↔ x ∈ p.closedBall (a⁻¹ • y) (r / ‖a‖)
rw₂ : (p : (a : E) → ℝ) (a • x - y) ≤ r ↔ (p : (a : E) → ℝ) (x - a⁻¹ • y) ≤ r / ‖a‖
rw₃ : (p : (a : E) → ℝ) (a • x - y) ≤ r ↔ HMul.hMul (α := ℝ) ((p : (a : E) → ℝ) (x - a⁻¹ • y) : ℝ) ‖a‖ ≤ r
rw₄ : (p : (a : E) → ℝ) (a • x - y) ≤ r ↔ HMul.hMul (β := ℝ) ‖a‖ ((p : (a : E) → ℝ) (x - a⁻¹ • y) : ℝ) ≤ r
rw₅ : (p : (a : E) → ℝ) (a • x - y) ≤ r ↔ (p : (a : E) → ℝ) (a • (x - a⁻¹ • y)) ≤ r
rw₆ : (p : (a : E) → ℝ) (a • x - y) ≤ r ↔ (p : (a : E) → ℝ) (a • x - a • a⁻¹ • y) ≤ r
⊢ Membership.mem (γ := Set E) ((fun (x : E) ↦ a • x) ⁻¹' p.closedBall y r) x ↔ x ∈ p.closedBall (a⁻¹ • y) (r / ‖a‖)
have rw₇ : (p : (a : E) → ℝ) (a • x - y) ≤ r ↔ (p : (a : E) → ℝ) (a • x - y) ≤ r
Tactic: rw [mem_preimage, mem_closedBall, mem_closedBall, le_div_iff₀ (norm_pos_iff.mpr ha), mul_comm, ←
      map_smul_eq_mul p, smul_sub, smul_inv_smul₀ ha]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : NormedSpace ℝ 𝕜
inst_3 : Module 𝕜 E
inst_4 : SMul ℝ E
inst_5 : IsScalarTower ℝ 𝕜 E
p : Seminorm 𝕜 E
⊢ ConvexOn ℝ (E := E) (β := ℝ) univ (⇑p : (a : E) → ℝ)
have refine : ∀ (x : E),
  Membership.mem (γ := Set E) univ x →
    ∀ (y : E),
      Membership.mem (γ := Set E) univ y →
        ∀ (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b),
          a + b = 1 →
            (p : (a : E) → ℝ) (a • x + b • y) ≤
              HSMul.hSMul (β := ℝ) a ((p : (a : E) → ℝ) x : ℝ) + HSMul.hSMul (β := ℝ) b ((p : (a : E) → ℝ) y : ℝ)
Tactic: refine ⟨convex_univ, fun x _ y _ a b ha hb _ => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : NormedSpace ℝ 𝕜
inst_3 : Module 𝕜 E
inst_4 : SMul ℝ E
inst_5 : IsScalarTower ℝ 𝕜 E
p : Seminorm 𝕜 E
x : E
h : Membership.mem (γ := Set E) univ x
y : E
h_1 : Membership.mem (γ := Set E) univ y
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
h_2 : a + b = 1
⊢ HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) (a • x) : ℝ) ((p : (a : E) → ℝ) (b • y) : ℝ) =
    HMul.hMul (β := ℝ) ‖HSMul.hSMul (β := 𝕜) a 1‖ ((p : (a : E) → ℝ) x : ℝ) +
      HMul.hMul (β := ℝ) ‖HSMul.hSMul (β := 𝕜) b 1‖ ((p : (a : E) → ℝ) y : ℝ)
have rw : HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) (a • x) : ℝ) ((p : (a : E) → ℝ) (b • y) : ℝ) =
  HAdd.hAdd (α := ℝ) ((p : (a : E) → ℝ) (HSMul.hSMul (β := 𝕜) a 1 • x) : ℝ)
    (HMul.hMul (β := ℝ) ‖HSMul.hSMul (β := 𝕜) b 1‖ ((p : (a : E) → ℝ) y : ℝ))
Tactic: rw [← map_smul_eq_mul p, ← map_smul_eq_mul p, smul_one_smul, smul_one_smul]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : NormedSpace ℝ 𝕜
inst_3 : Module 𝕜 E
inst_4 : SMul ℝ E
inst_5 : IsScalarTower ℝ 𝕜 E
p : Seminorm 𝕜 E
x : E
h : Membership.mem (γ := Set E) univ x
y : E
h_1 : Membership.mem (γ := Set E) univ y
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
h_2 : a + b = 1
rw :
  HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) (a • x) : ℝ) ((p : (a : E) → ℝ) (b • y) : ℝ) =
    HAdd.hAdd (α := ℝ) ((p : (a : E) → ℝ) (HSMul.hSMul (β := 𝕜) a 1 • x) : ℝ)
      (HMul.hMul (β := ℝ) ‖HSMul.hSMul (β := 𝕜) b 1‖ ((p : (a : E) → ℝ) y : ℝ))
⊢ HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) (a • x) : ℝ) ((p : (a : E) → ℝ) (b • y) : ℝ) =
    HMul.hMul (β := ℝ) ‖HSMul.hSMul (β := 𝕜) a 1‖ ((p : (a : E) → ℝ) x : ℝ) +
      HMul.hMul (β := ℝ) ‖HSMul.hSMul (β := 𝕜) b 1‖ ((p : (a : E) → ℝ) y : ℝ)
have rw₁ : HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) (a • x) : ℝ) ((p : (a : E) → ℝ) (b • y) : ℝ) =
  HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) (HSMul.hSMul (β := 𝕜) a 1 • x) : ℝ)
    ((p : (a : E) → ℝ) (HSMul.hSMul (β := 𝕜) b 1 • y) : ℝ)
Tactic: rw [← map_smul_eq_mul p, ← map_smul_eq_mul p, smul_one_smul, smul_one_smul]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : NormedSpace ℝ 𝕜
inst_3 : Module 𝕜 E
inst_4 : SMul ℝ E
inst_5 : IsScalarTower ℝ 𝕜 E
p : Seminorm 𝕜 E
x : E
h : Membership.mem (γ := Set E) univ x
y : E
h_1 : Membership.mem (γ := Set E) univ y
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
h_2 : a + b = 1
rw :
  HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) (a • x) : ℝ) ((p : (a : E) → ℝ) (b • y) : ℝ) =
    HAdd.hAdd (α := ℝ) ((p : (a : E) → ℝ) (HSMul.hSMul (β := 𝕜) a 1 • x) : ℝ)
      (HMul.hMul (β := ℝ) ‖HSMul.hSMul (β := 𝕜) b 1‖ ((p : (a : E) → ℝ) y : ℝ))
rw₁ :
  HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) (a • x) : ℝ) ((p : (a : E) → ℝ) (b • y) : ℝ) =
    HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) (HSMul.hSMul (β := 𝕜) a 1 • x) : ℝ)
      ((p : (a : E) → ℝ) (HSMul.hSMul (β := 𝕜) b 1 • y) : ℝ)
⊢ HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) (a • x) : ℝ) ((p : (a : E) → ℝ) (b • y) : ℝ) =
    HMul.hMul (β := ℝ) ‖HSMul.hSMul (β := 𝕜) a 1‖ ((p : (a : E) → ℝ) x : ℝ) +
      HMul.hMul (β := ℝ) ‖HSMul.hSMul (β := 𝕜) b 1‖ ((p : (a : E) → ℝ) y : ℝ)
have rw₂ : HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) (a • x) : ℝ) ((p : (a : E) → ℝ) (b • y) : ℝ) =
  HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) (a • x) : ℝ) ((p : (a : E) → ℝ) (HSMul.hSMul (β := 𝕜) b 1 • y) : ℝ)
Tactic: rw [← map_smul_eq_mul p, ← map_smul_eq_mul p, smul_one_smul, smul_one_smul]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : NormedSpace ℝ 𝕜
inst_3 : Module 𝕜 E
inst_4 : SMul ℝ E
inst_5 : IsScalarTower ℝ 𝕜 E
p : Seminorm 𝕜 E
x : E
h : Membership.mem (γ := Set E) univ x
y : E
h_1 : Membership.mem (γ := Set E) univ y
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
h_2 : a + b = 1
rw :
  HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) (a • x) : ℝ) ((p : (a : E) → ℝ) (b • y) : ℝ) =
    HAdd.hAdd (α := ℝ) ((p : (a : E) → ℝ) (HSMul.hSMul (β := 𝕜) a 1 • x) : ℝ)
      (HMul.hMul (β := ℝ) ‖HSMul.hSMul (β := 𝕜) b 1‖ ((p : (a : E) → ℝ) y : ℝ))
rw₁ :
  HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) (a • x) : ℝ) ((p : (a : E) → ℝ) (b • y) : ℝ) =
    HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) (HSMul.hSMul (β := 𝕜) a 1 • x) : ℝ)
      ((p : (a : E) → ℝ) (HSMul.hSMul (β := 𝕜) b 1 • y) : ℝ)
rw₂ :
  HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) (a • x) : ℝ) ((p : (a : E) → ℝ) (b • y) : ℝ) =
    HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) (a • x) : ℝ) ((p : (a : E) → ℝ) (HSMul.hSMul (β := 𝕜) b 1 • y) : ℝ)
⊢ HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) (a • x) : ℝ) ((p : (a : E) → ℝ) (b • y) : ℝ) =
    HMul.hMul (β := ℝ) ‖HSMul.hSMul (β := 𝕜) a 1‖ ((p : (a : E) → ℝ) x : ℝ) +
      HMul.hMul (β := ℝ) ‖HSMul.hSMul (β := 𝕜) b 1‖ ((p : (a : E) → ℝ) y : ℝ)
have rw₃ : HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) (a • x) : ℝ) ((p : (a : E) → ℝ) (b • y) : ℝ) =
  HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) (a • x) : ℝ) ((p : (a : E) → ℝ) (b • y) : ℝ)
Tactic: rw [← map_smul_eq_mul p, ← map_smul_eq_mul p, smul_one_smul, smul_one_smul]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : NormedSpace ℝ 𝕜
inst_3 : Module 𝕜 E
inst_4 : SMul ℝ E
inst_5 : IsScalarTower ℝ 𝕜 E
p : Seminorm 𝕜 E
x : E
h : Membership.mem (γ := Set E) univ x
y : E
h_1 : Membership.mem (γ := Set E) univ y
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
h_2 : a + b = 1
⊢ HMul.hMul (β := ℝ) ‖HSMul.hSMul (β := 𝕜) a 1‖ ((p : (a : E) → ℝ) x : ℝ) +
      HMul.hMul (β := ℝ) ‖HSMul.hSMul (β := 𝕜) b 1‖ ((p : (a : E) → ℝ) y : ℝ) =
    HMul.hMul (β := ℝ) a ((p : (a : E) → ℝ) x : ℝ) + HMul.hMul (β := ℝ) b ((p : (a : E) → ℝ) y : ℝ)
have rw : HMul.hMul (β := ℝ) (‖a‖ * norm.{u_3} (E := 𝕜) 1) ((p : (a : E) → ℝ) x : ℝ) +
    HMul.hMul (β := ℝ) ‖HSMul.hSMul (β := 𝕜) b 1‖ ((p : (a : E) → ℝ) y : ℝ) =
  HMul.hMul (β := ℝ) a ((p : (a : E) → ℝ) x : ℝ) + HMul.hMul (β := ℝ) b ((p : (a : E) → ℝ) y : ℝ)
Tactic: rw [norm_smul, norm_smul, norm_one, mul_one, mul_one, Real.norm_of_nonneg ha,
        Real.norm_of_nonneg hb]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : NormedSpace ℝ 𝕜
inst_3 : Module 𝕜 E
inst_4 : SMul ℝ E
inst_5 : IsScalarTower ℝ 𝕜 E
p : Seminorm 𝕜 E
x : E
h : Membership.mem (γ := Set E) univ x
y : E
h_1 : Membership.mem (γ := Set E) univ y
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
h_2 : a + b = 1
rw :
  HMul.hMul (β := ℝ) (‖a‖ * norm.{u_3} (E := 𝕜) 1) ((p : (a : E) → ℝ) x : ℝ) +
      HMul.hMul (β := ℝ) ‖HSMul.hSMul (β := 𝕜) b 1‖ ((p : (a : E) → ℝ) y : ℝ) =
    HMul.hMul (β := ℝ) a ((p : (a : E) → ℝ) x : ℝ) + HMul.hMul (β := ℝ) b ((p : (a : E) → ℝ) y : ℝ)
⊢ HMul.hMul (β := ℝ) ‖HSMul.hSMul (β := 𝕜) a 1‖ ((p : (a : E) → ℝ) x : ℝ) +
      HMul.hMul (β := ℝ) ‖HSMul.hSMul (β := 𝕜) b 1‖ ((p : (a : E) → ℝ) y : ℝ) =
    HMul.hMul (β := ℝ) a ((p : (a : E) → ℝ) x : ℝ) + HMul.hMul (β := ℝ) b ((p : (a : E) → ℝ) y : ℝ)
have rw₁ : HMul.hMul (β := ℝ) (‖a‖ * norm.{u_3} (E := 𝕜) 1) ((p : (a : E) → ℝ) x : ℝ) +
    HMul.hMul (β := ℝ) (‖b‖ * norm.{u_3} (E := 𝕜) 1) ((p : (a : E) → ℝ) y : ℝ) =
  HMul.hMul (β := ℝ) a ((p : (a : E) → ℝ) x : ℝ) + HMul.hMul (β := ℝ) b ((p : (a : E) → ℝ) y : ℝ)
Tactic: rw [norm_smul, norm_smul, norm_one, mul_one, mul_one, Real.norm_of_nonneg ha,
        Real.norm_of_nonneg hb]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : NormedSpace ℝ 𝕜
inst_3 : Module 𝕜 E
inst_4 : SMul ℝ E
inst_5 : IsScalarTower ℝ 𝕜 E
p : Seminorm 𝕜 E
x : E
h : Membership.mem (γ := Set E) univ x
y : E
h_1 : Membership.mem (γ := Set E) univ y
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
h_2 : a + b = 1
rw :
  HMul.hMul (β := ℝ) (‖a‖ * norm.{u_3} (E := 𝕜) 1) ((p : (a : E) → ℝ) x : ℝ) +
      HMul.hMul (β := ℝ) ‖HSMul.hSMul (β := 𝕜) b 1‖ ((p : (a : E) → ℝ) y : ℝ) =
    HMul.hMul (β := ℝ) a ((p : (a : E) → ℝ) x : ℝ) + HMul.hMul (β := ℝ) b ((p : (a : E) → ℝ) y : ℝ)
rw₁ :
  HMul.hMul (β := ℝ) (‖a‖ * norm.{u_3} (E := 𝕜) 1) ((p : (a : E) → ℝ) x : ℝ) +
      HMul.hMul (β := ℝ) (‖b‖ * norm.{u_3} (E := 𝕜) 1) ((p : (a : E) → ℝ) y : ℝ) =
    HMul.hMul (β := ℝ) a ((p : (a : E) → ℝ) x : ℝ) + HMul.hMul (β := ℝ) b ((p : (a : E) → ℝ) y : ℝ)
⊢ HMul.hMul (β := ℝ) ‖HSMul.hSMul (β := 𝕜) a 1‖ ((p : (a : E) → ℝ) x : ℝ) +
      HMul.hMul (β := ℝ) ‖HSMul.hSMul (β := 𝕜) b 1‖ ((p : (a : E) → ℝ) y : ℝ) =
    HMul.hMul (β := ℝ) a ((p : (a : E) → ℝ) x : ℝ) + HMul.hMul (β := ℝ) b ((p : (a : E) → ℝ) y : ℝ)
have rw₂ : HMul.hMul (β := ℝ) (‖a‖ * 1) ((p : (a : E) → ℝ) x : ℝ) + HMul.hMul (β := ℝ) (‖b‖ * 1) ((p : (a : E) → ℝ) y : ℝ) =
  HMul.hMul (β := ℝ) a ((p : (a : E) → ℝ) x : ℝ) + HMul.hMul (β := ℝ) b ((p : (a : E) → ℝ) y : ℝ)
Tactic: rw [norm_smul, norm_smul, norm_one, mul_one, mul_one, Real.norm_of_nonneg ha,
        Real.norm_of_nonneg hb]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : NormedSpace ℝ 𝕜
inst_3 : Module 𝕜 E
inst_4 : SMul ℝ E
inst_5 : IsScalarTower ℝ 𝕜 E
p : Seminorm 𝕜 E
x : E
h : Membership.mem (γ := Set E) univ x
y : E
h_1 : Membership.mem (γ := Set E) univ y
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
h_2 : a + b = 1
rw :
  HMul.hMul (β := ℝ) (‖a‖ * norm.{u_3} (E := 𝕜) 1) ((p : (a : E) → ℝ) x : ℝ) +
      HMul.hMul (β := ℝ) ‖HSMul.hSMul (β := 𝕜) b 1‖ ((p : (a : E) → ℝ) y : ℝ) =
    HMul.hMul (β := ℝ) a ((p : (a : E) → ℝ) x : ℝ) + HMul.hMul (β := ℝ) b ((p : (a : E) → ℝ) y : ℝ)
rw₁ :
  HMul.hMul (β := ℝ) (‖a‖ * norm.{u_3} (E := 𝕜) 1) ((p : (a : E) → ℝ) x : ℝ) +
      HMul.hMul (β := ℝ) (‖b‖ * norm.{u_3} (E := 𝕜) 1) ((p : (a : E) → ℝ) y : ℝ) =
    HMul.hMul (β := ℝ) a ((p : (a : E) → ℝ) x : ℝ) + HMul.hMul (β := ℝ) b ((p : (a : E) → ℝ) y : ℝ)
rw₂ :
  HMul.hMul (β := ℝ) (‖a‖ * 1) ((p : (a : E) → ℝ) x : ℝ) + HMul.hMul (β := ℝ) (‖b‖ * 1) ((p : (a : E) → ℝ) y : ℝ) =
    HMul.hMul (β := ℝ) a ((p : (a : E) → ℝ) x : ℝ) + HMul.hMul (β := ℝ) b ((p : (a : E) → ℝ) y : ℝ)
⊢ HMul.hMul (β := ℝ) ‖HSMul.hSMul (β := 𝕜) a 1‖ ((p : (a : E) → ℝ) x : ℝ) +
      HMul.hMul (β := ℝ) ‖HSMul.hSMul (β := 𝕜) b 1‖ ((p : (a : E) → ℝ) y : ℝ) =
    HMul.hMul (β := ℝ) a ((p : (a : E) → ℝ) x : ℝ) + HMul.hMul (β := ℝ) b ((p : (a : E) → ℝ) y : ℝ)
have rw₃ : HMul.hMul (β := ℝ) ‖a‖ ((p : (a : E) → ℝ) x : ℝ) + HMul.hMul (β := ℝ) (‖b‖ * 1) ((p : (a : E) → ℝ) y : ℝ) =
  HMul.hMul (β := ℝ) a ((p : (a : E) → ℝ) x : ℝ) + HMul.hMul (β := ℝ) b ((p : (a : E) → ℝ) y : ℝ)
Tactic: rw [norm_smul, norm_smul, norm_one, mul_one, mul_one, Real.norm_of_nonneg ha,
        Real.norm_of_nonneg hb]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : NormedSpace ℝ 𝕜
inst_3 : Module 𝕜 E
inst_4 : SMul ℝ E
inst_5 : IsScalarTower ℝ 𝕜 E
p : Seminorm 𝕜 E
x : E
h : Membership.mem (γ := Set E) univ x
y : E
h_1 : Membership.mem (γ := Set E) univ y
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
h_2 : a + b = 1
rw :
  HMul.hMul (β := ℝ) (‖a‖ * norm.{u_3} (E := 𝕜) 1) ((p : (a : E) → ℝ) x : ℝ) +
      HMul.hMul (β := ℝ) ‖HSMul.hSMul (β := 𝕜) b 1‖ ((p : (a : E) → ℝ) y : ℝ) =
    HMul.hMul (β := ℝ) a ((p : (a : E) → ℝ) x : ℝ) + HMul.hMul (β := ℝ) b ((p : (a : E) → ℝ) y : ℝ)
rw₁ :
  HMul.hMul (β := ℝ) (‖a‖ * norm.{u_3} (E := 𝕜) 1) ((p : (a : E) → ℝ) x : ℝ) +
      HMul.hMul (β := ℝ) (‖b‖ * norm.{u_3} (E := 𝕜) 1) ((p : (a : E) → ℝ) y : ℝ) =
    HMul.hMul (β := ℝ) a ((p : (a : E) → ℝ) x : ℝ) + HMul.hMul (β := ℝ) b ((p : (a : E) → ℝ) y : ℝ)
rw₂ :
  HMul.hMul (β := ℝ) (‖a‖ * 1) ((p : (a : E) → ℝ) x : ℝ) + HMul.hMul (β := ℝ) (‖b‖ * 1) ((p : (a : E) → ℝ) y : ℝ) =
    HMul.hMul (β := ℝ) a ((p : (a : E) → ℝ) x : ℝ) + HMul.hMul (β := ℝ) b ((p : (a : E) → ℝ) y : ℝ)
rw₃ :
  HMul.hMul (β := ℝ) ‖a‖ ((p : (a : E) → ℝ) x : ℝ) + HMul.hMul (β := ℝ) (‖b‖ * 1) ((p : (a : E) → ℝ) y : ℝ) =
    HMul.hMul (β := ℝ) a ((p : (a : E) → ℝ) x : ℝ) + HMul.hMul (β := ℝ) b ((p : (a : E) → ℝ) y : ℝ)
⊢ HMul.hMul (β := ℝ) ‖HSMul.hSMul (β := 𝕜) a 1‖ ((p : (a : E) → ℝ) x : ℝ) +
      HMul.hMul (β := ℝ) ‖HSMul.hSMul (β := 𝕜) b 1‖ ((p : (a : E) → ℝ) y : ℝ) =
    HMul.hMul (β := ℝ) a ((p : (a : E) → ℝ) x : ℝ) + HMul.hMul (β := ℝ) b ((p : (a : E) → ℝ) y : ℝ)
have rw₄ : HMul.hMul (β := ℝ) ‖a‖ ((p : (a : E) → ℝ) x : ℝ) + HMul.hMul (β := ℝ) ‖b‖ ((p : (a : E) → ℝ) y : ℝ) =
  HMul.hMul (β := ℝ) a ((p : (a : E) → ℝ) x : ℝ) + HMul.hMul (β := ℝ) b ((p : (a : E) → ℝ) y : ℝ)
Tactic: rw [norm_smul, norm_smul, norm_one, mul_one, mul_one, Real.norm_of_nonneg ha,
        Real.norm_of_nonneg hb]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : NormedSpace ℝ 𝕜
inst_3 : Module 𝕜 E
inst_4 : SMul ℝ E
inst_5 : IsScalarTower ℝ 𝕜 E
p : Seminorm 𝕜 E
x : E
h : Membership.mem (γ := Set E) univ x
y : E
h_1 : Membership.mem (γ := Set E) univ y
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
h_2 : a + b = 1
rw :
  HMul.hMul (β := ℝ) (‖a‖ * norm.{u_3} (E := 𝕜) 1) ((p : (a : E) → ℝ) x : ℝ) +
      HMul.hMul (β := ℝ) ‖HSMul.hSMul (β := 𝕜) b 1‖ ((p : (a : E) → ℝ) y : ℝ) =
    HMul.hMul (β := ℝ) a ((p : (a : E) → ℝ) x : ℝ) + HMul.hMul (β := ℝ) b ((p : (a : E) → ℝ) y : ℝ)
rw₁ :
  HMul.hMul (β := ℝ) (‖a‖ * norm.{u_3} (E := 𝕜) 1) ((p : (a : E) → ℝ) x : ℝ) +
      HMul.hMul (β := ℝ) (‖b‖ * norm.{u_3} (E := 𝕜) 1) ((p : (a : E) → ℝ) y : ℝ) =
    HMul.hMul (β := ℝ) a ((p : (a : E) → ℝ) x : ℝ) + HMul.hMul (β := ℝ) b ((p : (a : E) → ℝ) y : ℝ)
rw₂ :
  HMul.hMul (β := ℝ) (‖a‖ * 1) ((p : (a : E) → ℝ) x : ℝ) + HMul.hMul (β := ℝ) (‖b‖ * 1) ((p : (a : E) → ℝ) y : ℝ) =
    HMul.hMul (β := ℝ) a ((p : (a : E) → ℝ) x : ℝ) + HMul.hMul (β := ℝ) b ((p : (a : E) → ℝ) y : ℝ)
rw₃ :
  HMul.hMul (β := ℝ) ‖a‖ ((p : (a : E) → ℝ) x : ℝ) + HMul.hMul (β := ℝ) (‖b‖ * 1) ((p : (a : E) → ℝ) y : ℝ) =
    HMul.hMul (β := ℝ) a ((p : (a : E) → ℝ) x : ℝ) + HMul.hMul (β := ℝ) b ((p : (a : E) → ℝ) y : ℝ)
rw₄ :
  HMul.hMul (β := ℝ) ‖a‖ ((p : (a : E) → ℝ) x : ℝ) + HMul.hMul (β := ℝ) ‖b‖ ((p : (a : E) → ℝ) y : ℝ) =
    HMul.hMul (β := ℝ) a ((p : (a : E) → ℝ) x : ℝ) + HMul.hMul (β := ℝ) b ((p : (a : E) → ℝ) y : ℝ)
⊢ HMul.hMul (β := ℝ) ‖HSMul.hSMul (β := 𝕜) a 1‖ ((p : (a : E) → ℝ) x : ℝ) +
      HMul.hMul (β := ℝ) ‖HSMul.hSMul (β := 𝕜) b 1‖ ((p : (a : E) → ℝ) y : ℝ) =
    HMul.hMul (β := ℝ) a ((p : (a : E) → ℝ) x : ℝ) + HMul.hMul (β := ℝ) b ((p : (a : E) → ℝ) y : ℝ)
have rw₅ : HMul.hMul (β := ℝ) a ((p : (a : E) → ℝ) x : ℝ) + HMul.hMul (β := ℝ) ‖b‖ ((p : (a : E) → ℝ) y : ℝ) =
  HMul.hMul (β := ℝ) a ((p : (a : E) → ℝ) x : ℝ) + HMul.hMul (β := ℝ) b ((p : (a : E) → ℝ) y : ℝ)
Tactic: rw [norm_smul, norm_smul, norm_one, mul_one, mul_one, Real.norm_of_nonneg ha,
        Real.norm_of_nonneg hb]