awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ι
hi : i ∈ s
hix :
  Eq (α := { r : ℝ // 0 ≤ r })
    (s.sup fun (i : ι) ↦ Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) ((p i : (a : E) → ℝ) x) ⋯ : { r : ℝ // 0 ≤ r })
    (Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) ((p i : (a : E) → ℝ) x) ⋯ : { r : ℝ // 0 ≤ r })
⊢ ∃ i ∈ s, Eq (α := ℝ) ((s.sup p : (a : E) → ℝ) x : ℝ) ((p i : (a : E) → ℝ) x : ℝ)
have rw : ∃ i ∈ s, (↑(s.sup fun (i : ι) ↦ NNReal.mk ((p i : (a : E) → ℝ) x) sorry) : ℝ) = (p i : (a : E) → ℝ) x
Tactic: rw [finset_sup_apply]
-- 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
⊢ Eq (α := ℝ) ((s.sup p : (a : E) → ℝ) x : ℝ) (0 : ℝ) ∨
    ∃ i ∈ s, Eq (α := ℝ) ((s.sup p : (a : E) → ℝ) x : ℝ) ((p i : (a : E) → ℝ) x : ℝ)
have inl : Eq (α := ℝ) ((Finset.sup ∅ p : (a : E) → ℝ) x : ℝ) (0 : ℝ) ∨
  ∃ (i : ι),
    Membership.mem (γ := Finset ι) ∅ i ∧ Eq (α := ℝ) ((Finset.sup ∅ p : (a : E) → ℝ) x : ℝ) ((p i : (a : E) → ℝ) x : ℝ)
Tactic: rcases Finset.eq_empty_or_nonempty s with (rfl | hs)
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
inl :
  Eq (α := ℝ) ((Finset.sup ∅ p : (a : E) → ℝ) x : ℝ) (0 : ℝ) ∨
    ∃ (i : ι),
      Membership.mem (γ := Finset ι) ∅ i ∧
        Eq (α := ℝ) ((Finset.sup ∅ p : (a : E) → ℝ) x : ℝ) ((p i : (a : E) → ℝ) x : ℝ)
⊢ Eq (α := ℝ) ((s.sup p : (a : E) → ℝ) x : ℝ) (0 : ℝ) ∨
    ∃ i ∈ s, Eq (α := ℝ) ((s.sup p : (a : E) → ℝ) x : ℝ) ((p i : (a : E) → ℝ) x : ℝ)
have inr : ∀ (hs : s.Nonempty),
  Eq (α := ℝ) ((s.sup p : (a : E) → ℝ) x : ℝ) (0 : ℝ) ∨
    ∃ i ∈ s, Eq (α := ℝ) ((s.sup p : (a : E) → ℝ) x : ℝ) ((p i : (a : E) → ℝ) x : ℝ)
Tactic: rcases Finset.eq_empty_or_nonempty s with (rfl | hs)
-- 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
⊢ Eq (α := ℝ) ((Finset.sup ∅ p : (a : E) → ℝ) x : ℝ) (0 : ℝ) ∨
    ∃ (i : ι),
      Membership.mem (γ := Finset ι) ∅ i ∧
        Eq (α := ℝ) ((Finset.sup ∅ p : (a : E) → ℝ) x : ℝ) ((p i : (a : E) → ℝ) x : ℝ)
have inl : Eq (α := ℝ) ((Finset.sup ∅ p : (a : E) → ℝ) x : ℝ) (0 : ℝ)
Tactic: left
-- 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
hs : s.Nonempty
⊢ Eq (α := ℝ) ((s.sup p : (a : E) → ℝ) x : ℝ) (0 : ℝ) ∨
    ∃ i ∈ s, Eq (α := ℝ) ((s.sup p : (a : E) → ℝ) x : ℝ) ((p i : (a : E) → ℝ) x : ℝ)
have inr : ∃ i ∈ s, Eq (α := ℝ) ((s.sup p : (a : E) → ℝ) x : ℝ) ((p i : (a : E) → ℝ) x : ℝ)
Tactic: right
-- 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 ι
C : ℝ≥0
⊢ s.sup (C • p) = C • s.sup p
have h : ∀ (x : E), Eq (α := ℝ) ((s.sup (C • p) : (a : E) → ℝ) x : ℝ) ((C • s.sup p : (a : E) → ℝ) x : ℝ)
Tactic: ext x
-- 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 ι
C : ℝ≥0
x : E
⊢ Eq (α := ℝ) ((s.sup (C • p) : (a : E) → ℝ) x : ℝ) ((C • s.sup p : (a : E) → ℝ) x : ℝ)
have h : (↑(s.sup fun (i : ι) ↦ NNReal.mk (((C • p) i : (a : E) → ℝ) x) sorry) : ℝ) =
  C • (↑(s.sup fun (i : ι) ↦ NNReal.mk ((p i : (a : E) → ℝ) x) sorry) : ℝ)
Tactic: rw [smul_apply, finset_sup_apply, finset_sup_apply]
-- 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 ι
C : ℝ≥0
x : E
⊢ (↑(s.sup fun (i : ι) ↦ NNReal.mk (((C • p) i : (a : E) → ℝ) x) ⋯) : ℝ) =
    C • (↑(s.sup fun (i : ι) ↦ NNReal.mk ((p i : (a : E) → ℝ) x) ⋯) : ℝ)
have h : C • (↑(s.sup fun (i : ι) ↦ NNReal.mk ((p i : (a : E) → ℝ) x) sorry) : ℝ) =
  (↑(s.sup fun (i : ι) ↦ NNReal.mk (((C • p) i : (a : E) → ℝ) x) sorry) : ℝ)
Tactic: symm
-- 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 ι
⊢ s.sup p ≤ ∑ i ∈ s, p i
have refine : ∀ b ∈ s, p b ≤ ∑ i ∈ s, p i
Tactic: refine Finset.sup_le_iff.mpr ?_
-- 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 ι
i : ι
hi : i ∈ s
⊢ p i ≤ ∑ i ∈ s, p i
have rw : LE.le.{u_7} (α := Seminorm 𝕜 E) 0 (∑ x ∈ s \ {i}, p x)
Tactic: rw [Finset.sum_eq_sum_diff_singleton_add hi, le_add_iff_nonneg_left]
-- 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 ι
⊢ s.sup p ≤ ∑ i ∈ s, p i
have refine : ∀ b ∈ s, p b ≤ ∑ i ∈ s, p i
Tactic: classical
  refine Finset.sup_le_iff.mpr ?_
  intro i hi
  rw [Finset.sum_eq_sum_diff_singleton_add hi, le_add_iff_nonneg_left]
  exact bot_le
-- 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 ι
refine refine₁ : ∀ (i : ι) (hi : i ∈ s), p i ≤ ∑ i ∈ s, p i
⊢ s.sup p ≤ ∑ i ∈ s, p i
have refine₂ : ∀ (i : ι) (hi : i ∈ s), LE.le.{u_7} (α := Seminorm 𝕜 E) 0 (∑ x ∈ s \ {i}, p x)
Tactic: classical
  refine Finset.sup_le_iff.mpr ?_
  intro i hi
  rw [Finset.sum_eq_sum_diff_singleton_add hi, le_add_iff_nonneg_left]
  exact bot_le
-- 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
a : ℝ
ha : 0 ≤ a
h : ∀ i ∈ s, (p i : (a : E) → ℝ) x ≤ a
⊢ (s.sup p : (a : E) → ℝ) x ≤ a
have lift : ∀ (a : ℝ≥0) (h : ∀ i ∈ s, (p i : (a : E) → ℝ) x ≤ (↑a : ℝ)), (s.sup p : (a : E) → ℝ) x ≤ (↑a : ℝ)
Tactic: lift a to ℝ≥0 using ha
Cleared hypotheses: a, ha, h
-- 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
a : ℝ≥0
h : ∀ i ∈ s, (p i : (a : E) → ℝ) x ≤ (↑a : ℝ)
⊢ (s.sup p : (a : E) → ℝ) x ≤ (↑a : ℝ)
have rw : (s.sup fun (i : ι) ↦ NNReal.mk ((p i : (a : E) → ℝ) x) sorry) ≤ a
Tactic: rw [finset_sup_apply, NNReal.coe_le_coe]
-- 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
a : ℝ
ha : 0 < a
h : ∀ i ∈ s, (p i : (a : E) → ℝ) x < a
⊢ (s.sup p : (a : E) → ℝ) x < a
have lift : ∀ (a : ℝ≥0) (ha : 0 < (↑a : ℝ)) (h : ∀ i ∈ s, (p i : (a : E) → ℝ) x < (↑a : ℝ)), (s.sup p : (a : E) → ℝ) x < (↑a : ℝ)
Tactic: lift a to ℝ≥0 using ha.le
Cleared hypotheses: a, ha, h
-- 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
a : ℝ≥0
ha : 0 < (↑a : ℝ)
h : ∀ i ∈ s, (p i : (a : E) → ℝ) x < (↑a : ℝ)
⊢ (s.sup p : (a : E) → ℝ) x < (↑a : ℝ)
have rw : ∀ b ∈ s, NNReal.mk ((p b : (a : E) → ℝ) x) sorry < a
Tactic: rw [finset_sup_apply, NNReal.coe_lt_coe, Finset.sup_lt_iff]
-- 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
a : ℝ≥0
ha : 0 < (↑a : ℝ)
h : ∀ i ∈ s, (p i : (a : E) → ℝ) x < (↑a : ℝ)
rw : ∀ b ∈ s, NNReal.mk ((p b : (a : E) → ℝ) x) ⋯ < a
⊢ (s.sup p : (a : E) → ℝ) x < (↑a : ℝ)
have rw₁ : ⊥ < a
Tactic: rw [finset_sup_apply, NNReal.coe_lt_coe, Finset.sup_lt_iff]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
𝕜₂ : Type u_4
E : Type u_7
E₂ : Type u_8
inst : SeminormedRing 𝕜
inst_1 : SeminormedCommRing 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst_2 : RingHomIsometric σ₁₂
inst_3 : AddCommGroup E
inst_4 : AddCommGroup E₂
inst_5 : Module 𝕜 E
inst_6 : Module 𝕜₂ E₂
p : Seminorm 𝕜₂ E₂
f : E →ₛₗ[σ₁₂] E₂
c : 𝕜₂
x : E
⊢ Eq (α := ℝ) ((p.comp (c • f) : (a : E) → ℝ) x : ℝ) ((‖c‖₊ • p.comp f : (a : E) → ℝ) x : ℝ)
have rw : Eq (α := ℝ) ((p : (a : E₂) → ℝ) ((c • f : (a : E) → E₂) x : E₂) : ℝ) ((‖c‖₊ • p.comp f : (a : E) → ℝ) x : ℝ)
Tactic: rw [comp_apply, smul_apply, LinearMap.smul_apply, map_smul_eq_mul, NNReal.smul_def, coe_nnnorm,
      smul_eq_mul, comp_apply]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
𝕜₂ : Type u_4
E : Type u_7
E₂ : Type u_8
inst : SeminormedRing 𝕜
inst_1 : SeminormedCommRing 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst_2 : RingHomIsometric σ₁₂
inst_3 : AddCommGroup E
inst_4 : AddCommGroup E₂
inst_5 : Module 𝕜 E
inst_6 : Module 𝕜₂ E₂
p : Seminorm 𝕜₂ E₂
f : E →ₛₗ[σ₁₂] E₂
c : 𝕜₂
x : E
rw : Eq (α := ℝ) ((p : (a : E₂) → ℝ) ((c • f : (a : E) → E₂) x : E₂) : ℝ) ((‖c‖₊ • p.comp f : (a : E) → ℝ) x : ℝ)
⊢ Eq (α := ℝ) ((p.comp (c • f) : (a : E) → ℝ) x : ℝ) ((‖c‖₊ • p.comp f : (a : E) → ℝ) x : ℝ)
have rw₁ : (p : (a : E₂) → ℝ) ((c • f : (a : E) → E₂) x : E₂) = HSMul.hSMul (β := ℝ) ‖c‖₊ ((p.comp f : (a : E) → ℝ) x : ℝ)
Tactic: rw [comp_apply, smul_apply, LinearMap.smul_apply, map_smul_eq_mul, NNReal.smul_def, coe_nnnorm,
      smul_eq_mul, comp_apply]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
𝕜₂ : Type u_4
E : Type u_7
E₂ : Type u_8
inst : SeminormedRing 𝕜
inst_1 : SeminormedCommRing 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst_2 : RingHomIsometric σ₁₂
inst_3 : AddCommGroup E
inst_4 : AddCommGroup E₂
inst_5 : Module 𝕜 E
inst_6 : Module 𝕜₂ E₂
p : Seminorm 𝕜₂ E₂
f : E →ₛₗ[σ₁₂] E₂
c : 𝕜₂
x : E
rw : Eq (α := ℝ) ((p : (a : E₂) → ℝ) ((c • f : (a : E) → E₂) x : E₂) : ℝ) ((‖c‖₊ • p.comp f : (a : E) → ℝ) x : ℝ)
rw₁ : (p : (a : E₂) → ℝ) ((c • f : (a : E) → E₂) x : E₂) = HSMul.hSMul (β := ℝ) ‖c‖₊ ((p.comp f : (a : E) → ℝ) x : ℝ)
⊢ Eq (α := ℝ) ((p.comp (c • f) : (a : E) → ℝ) x : ℝ) ((‖c‖₊ • p.comp f : (a : E) → ℝ) x : ℝ)
have rw₂ : (p : (a : E₂) → ℝ) (HSMul.hSMul (β := E₂) c ((f : (a : E) → E₂) x : E₂)) =
  HSMul.hSMul (β := ℝ) ‖c‖₊ ((p.comp f : (a : E) → ℝ) x : ℝ)
Tactic: rw [comp_apply, smul_apply, LinearMap.smul_apply, map_smul_eq_mul, NNReal.smul_def, coe_nnnorm,
      smul_eq_mul, comp_apply]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
𝕜₂ : Type u_4
E : Type u_7
E₂ : Type u_8
inst : SeminormedRing 𝕜
inst_1 : SeminormedCommRing 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst_2 : RingHomIsometric σ₁₂
inst_3 : AddCommGroup E
inst_4 : AddCommGroup E₂
inst_5 : Module 𝕜 E
inst_6 : Module 𝕜₂ E₂
p : Seminorm 𝕜₂ E₂
f : E →ₛₗ[σ₁₂] E₂
c : 𝕜₂
x : E
rw : Eq (α := ℝ) ((p : (a : E₂) → ℝ) ((c • f : (a : E) → E₂) x : E₂) : ℝ) ((‖c‖₊ • p.comp f : (a : E) → ℝ) x : ℝ)
rw₁ : (p : (a : E₂) → ℝ) ((c • f : (a : E) → E₂) x : E₂) = HSMul.hSMul (β := ℝ) ‖c‖₊ ((p.comp f : (a : E) → ℝ) x : ℝ)
rw₂ :
  (p : (a : E₂) → ℝ) (HSMul.hSMul (β := E₂) c ((f : (a : E) → E₂) x : E₂)) =
    HSMul.hSMul (β := ℝ) ‖c‖₊ ((p.comp f : (a : E) → ℝ) x : ℝ)
⊢ Eq (α := ℝ) ((p.comp (c • f) : (a : E) → ℝ) x : ℝ) ((‖c‖₊ • p.comp f : (a : E) → ℝ) x : ℝ)
have rw₃ : HMul.hMul (β := ℝ) ‖c‖ ((p : (a : E₂) → ℝ) ((f : (a : E) → E₂) x : E₂) : ℝ) =
  HSMul.hSMul (β := ℝ) ‖c‖₊ ((p.comp f : (a : E) → ℝ) x : ℝ)
Tactic: rw [comp_apply, smul_apply, LinearMap.smul_apply, map_smul_eq_mul, NNReal.smul_def, coe_nnnorm,
      smul_eq_mul, comp_apply]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
𝕜₂ : Type u_4
E : Type u_7
E₂ : Type u_8
inst : SeminormedRing 𝕜
inst_1 : SeminormedCommRing 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst_2 : RingHomIsometric σ₁₂
inst_3 : AddCommGroup E
inst_4 : AddCommGroup E₂
inst_5 : Module 𝕜 E
inst_6 : Module 𝕜₂ E₂
p : Seminorm 𝕜₂ E₂
f : E →ₛₗ[σ₁₂] E₂
c : 𝕜₂
x : E
rw : Eq (α := ℝ) ((p : (a : E₂) → ℝ) ((c • f : (a : E) → E₂) x : E₂) : ℝ) ((‖c‖₊ • p.comp f : (a : E) → ℝ) x : ℝ)
rw₁ : (p : (a : E₂) → ℝ) ((c • f : (a : E) → E₂) x : E₂) = HSMul.hSMul (β := ℝ) ‖c‖₊ ((p.comp f : (a : E) → ℝ) x : ℝ)
rw₂ :
  (p : (a : E₂) → ℝ) (HSMul.hSMul (β := E₂) c ((f : (a : E) → E₂) x : E₂)) =
    HSMul.hSMul (β := ℝ) ‖c‖₊ ((p.comp f : (a : E) → ℝ) x : ℝ)
rw₃ :
  HMul.hMul (β := ℝ) ‖c‖ ((p : (a : E₂) → ℝ) ((f : (a : E) → E₂) x : E₂) : ℝ) =
    HSMul.hSMul (β := ℝ) ‖c‖₊ ((p.comp f : (a : E) → ℝ) x : ℝ)
⊢ Eq (α := ℝ) ((p.comp (c • f) : (a : E) → ℝ) x : ℝ) ((‖c‖₊ • p.comp f : (a : E) → ℝ) x : ℝ)
have rw₄ : HMul.hMul (β := ℝ) ‖c‖ ((p : (a : E₂) → ℝ) ((f : (a : E) → E₂) x : E₂) : ℝ) =
  HSMul.hSMul (β := ℝ) (↑‖c‖₊ : ℝ) ((p.comp f : (a : E) → ℝ) x : ℝ)
Tactic: rw [comp_apply, smul_apply, LinearMap.smul_apply, map_smul_eq_mul, NNReal.smul_def, coe_nnnorm,
      smul_eq_mul, comp_apply]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
𝕜₂ : Type u_4
E : Type u_7
E₂ : Type u_8
inst : SeminormedRing 𝕜
inst_1 : SeminormedCommRing 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst_2 : RingHomIsometric σ₁₂
inst_3 : AddCommGroup E
inst_4 : AddCommGroup E₂
inst_5 : Module 𝕜 E
inst_6 : Module 𝕜₂ E₂
p : Seminorm 𝕜₂ E₂
f : E →ₛₗ[σ₁₂] E₂
c : 𝕜₂
x : E
rw : Eq (α := ℝ) ((p : (a : E₂) → ℝ) ((c • f : (a : E) → E₂) x : E₂) : ℝ) ((‖c‖₊ • p.comp f : (a : E) → ℝ) x : ℝ)
rw₁ : (p : (a : E₂) → ℝ) ((c • f : (a : E) → E₂) x : E₂) = HSMul.hSMul (β := ℝ) ‖c‖₊ ((p.comp f : (a : E) → ℝ) x : ℝ)
rw₂ :
  (p : (a : E₂) → ℝ) (HSMul.hSMul (β := E₂) c ((f : (a : E) → E₂) x : E₂)) =
    HSMul.hSMul (β := ℝ) ‖c‖₊ ((p.comp f : (a : E) → ℝ) x : ℝ)
rw₃ :
  HMul.hMul (β := ℝ) ‖c‖ ((p : (a : E₂) → ℝ) ((f : (a : E) → E₂) x : E₂) : ℝ) =
    HSMul.hSMul (β := ℝ) ‖c‖₊ ((p.comp f : (a : E) → ℝ) x : ℝ)
rw₄ :
  HMul.hMul (β := ℝ) ‖c‖ ((p : (a : E₂) → ℝ) ((f : (a : E) → E₂) x : E₂) : ℝ) =
    HSMul.hSMul (β := ℝ) (↑‖c‖₊ : ℝ) ((p.comp f : (a : E) → ℝ) x : ℝ)
⊢ Eq (α := ℝ) ((p.comp (c • f) : (a : E) → ℝ) x : ℝ) ((‖c‖₊ • p.comp f : (a : E) → ℝ) x : ℝ)
have rw₅ : HMul.hMul (β := ℝ) ‖c‖ ((p : (a : E₂) → ℝ) ((f : (a : E) → E₂) x : E₂) : ℝ) =
  HSMul.hSMul (β := ℝ) ‖c‖ ((p.comp f : (a : E) → ℝ) x : ℝ)
Tactic: rw [comp_apply, smul_apply, LinearMap.smul_apply, map_smul_eq_mul, NNReal.smul_def, coe_nnnorm,
      smul_eq_mul, comp_apply]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
𝕜₂ : Type u_4
E : Type u_7
E₂ : Type u_8
inst : SeminormedRing 𝕜
inst_1 : SeminormedCommRing 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst_2 : RingHomIsometric σ₁₂
inst_3 : AddCommGroup E
inst_4 : AddCommGroup E₂
inst_5 : Module 𝕜 E
inst_6 : Module 𝕜₂ E₂
p : Seminorm 𝕜₂ E₂
f : E →ₛₗ[σ₁₂] E₂
c : 𝕜₂
x : E
rw : Eq (α := ℝ) ((p : (a : E₂) → ℝ) ((c • f : (a : E) → E₂) x : E₂) : ℝ) ((‖c‖₊ • p.comp f : (a : E) → ℝ) x : ℝ)
rw₁ : (p : (a : E₂) → ℝ) ((c • f : (a : E) → E₂) x : E₂) = HSMul.hSMul (β := ℝ) ‖c‖₊ ((p.comp f : (a : E) → ℝ) x : ℝ)
rw₂ :
  (p : (a : E₂) → ℝ) (HSMul.hSMul (β := E₂) c ((f : (a : E) → E₂) x : E₂)) =
    HSMul.hSMul (β := ℝ) ‖c‖₊ ((p.comp f : (a : E) → ℝ) x : ℝ)
rw₃ :
  HMul.hMul (β := ℝ) ‖c‖ ((p : (a : E₂) → ℝ) ((f : (a : E) → E₂) x : E₂) : ℝ) =
    HSMul.hSMul (β := ℝ) ‖c‖₊ ((p.comp f : (a : E) → ℝ) x : ℝ)
rw₄ :
  HMul.hMul (β := ℝ) ‖c‖ ((p : (a : E₂) → ℝ) ((f : (a : E) → E₂) x : E₂) : ℝ) =
    HSMul.hSMul (β := ℝ) (↑‖c‖₊ : ℝ) ((p.comp f : (a : E) → ℝ) x : ℝ)
rw₅ :
  HMul.hMul (β := ℝ) ‖c‖ ((p : (a : E₂) → ℝ) ((f : (a : E) → E₂) x : E₂) : ℝ) =
    HSMul.hSMul (β := ℝ) ‖c‖ ((p.comp f : (a : E) → ℝ) x : ℝ)
⊢ Eq (α := ℝ) ((p.comp (c • f) : (a : E) → ℝ) x : ℝ) ((‖c‖₊ • p.comp f : (a : E) → ℝ) x : ℝ)
have rw₆ : HMul.hMul (β := ℝ) ‖c‖ ((p : (a : E₂) → ℝ) ((f : (a : E) → E₂) x : E₂) : ℝ) =
  HMul.hMul (β := ℝ) ‖c‖ ((p.comp f : (a : E) → ℝ) x : ℝ)
Tactic: rw [comp_apply, smul_apply, LinearMap.smul_apply, map_smul_eq_mul, NNReal.smul_def, coe_nnnorm,
      smul_eq_mul, comp_apply]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
𝕜₂ : Type u_4
E : Type u_7
E₂ : Type u_8
inst : SeminormedRing 𝕜
inst_1 : SeminormedCommRing 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst_2 : RingHomIsometric σ₁₂
inst_3 : AddCommGroup E
inst_4 : AddCommGroup E₂
inst_5 : Module 𝕜 E
inst_6 : Module 𝕜₂ E₂
p : Seminorm 𝕜₂ E₂
f : E →ₛₗ[σ₁₂] E₂
c : 𝕜₂
x : E
rw : Eq (α := ℝ) ((p : (a : E₂) → ℝ) ((c • f : (a : E) → E₂) x : E₂) : ℝ) ((‖c‖₊ • p.comp f : (a : E) → ℝ) x : ℝ)
rw₁ : (p : (a : E₂) → ℝ) ((c • f : (a : E) → E₂) x : E₂) = HSMul.hSMul (β := ℝ) ‖c‖₊ ((p.comp f : (a : E) → ℝ) x : ℝ)
rw₂ :
  (p : (a : E₂) → ℝ) (HSMul.hSMul (β := E₂) c ((f : (a : E) → E₂) x : E₂)) =
    HSMul.hSMul (β := ℝ) ‖c‖₊ ((p.comp f : (a : E) → ℝ) x : ℝ)
rw₃ :
  HMul.hMul (β := ℝ) ‖c‖ ((p : (a : E₂) → ℝ) ((f : (a : E) → E₂) x : E₂) : ℝ) =
    HSMul.hSMul (β := ℝ) ‖c‖₊ ((p.comp f : (a : E) → ℝ) x : ℝ)
rw₄ :
  HMul.hMul (β := ℝ) ‖c‖ ((p : (a : E₂) → ℝ) ((f : (a : E) → E₂) x : E₂) : ℝ) =
    HSMul.hSMul (β := ℝ) (↑‖c‖₊ : ℝ) ((p.comp f : (a : E) → ℝ) x : ℝ)
rw₅ :
  HMul.hMul (β := ℝ) ‖c‖ ((p : (a : E₂) → ℝ) ((f : (a : E) → E₂) x : E₂) : ℝ) =
    HSMul.hSMul (β := ℝ) ‖c‖ ((p.comp f : (a : E) → ℝ) x : ℝ)
rw₆ :
  HMul.hMul (β := ℝ) ‖c‖ ((p : (a : E₂) → ℝ) ((f : (a : E) → E₂) x : E₂) : ℝ) =
    HMul.hMul (β := ℝ) ‖c‖ ((p.comp f : (a : E) → ℝ) x : ℝ)
⊢ Eq (α := ℝ) ((p.comp (c • f) : (a : E) → ℝ) x : ℝ) ((‖c‖₊ • p.comp f : (a : E) → ℝ) x : ℝ)
have rw₇ : HMul.hMul (β := ℝ) ‖c‖ ((p : (a : E₂) → ℝ) ((f : (a : E) → E₂) x : E₂) : ℝ) =
  HMul.hMul (β := ℝ) ‖c‖ ((p : (a : E₂) → ℝ) ((f : (a : E) → E₂) x : E₂) : ℝ)
Tactic: rw [comp_apply, smul_apply, LinearMap.smul_apply, map_smul_eq_mul, NNReal.smul_def, coe_nnnorm,
      smul_eq_mul, comp_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_1 q_1 : Seminorm 𝕜 E
x_1 : E
p q : Seminorm 𝕜 E
a : 𝕜
x : E
⊢ ⨅ (u : E), HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) u : ℝ) ((q : (a : E) → ℝ) (a • x - u) : ℝ) =
    ‖a‖ * ⨅ (u : E), HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) u : ℝ) ((q : (a : E) → ℝ) (x - u) : ℝ)
have inl : ⨅ (u : E),
    HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) u : ℝ)
      ((q : (a : E) → ℝ) (HSMul.hSMul.{u_3, u_7, u_7} (α := 𝕜) 0 x - u) : ℝ) =
  norm.{u_3} (E := 𝕜) 0 *
    ⨅ (u : E), HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) u : ℝ) ((q : (a : E) → ℝ) (x - u) : ℝ)
Tactic: obtain rfl | ha := eq_or_ne a 0
Cleared hypotheses: a
-- 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
inl :
  ⨅ (u : E),
      HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) u : ℝ)
        ((q : (a : E) → ℝ) (HSMul.hSMul.{u_3, u_7, u_7} (α := 𝕜) 0 x - u) : ℝ) =
    norm.{u_3} (E := 𝕜) 0 *
      ⨅ (u : E), HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) u : ℝ) ((q : (a : E) → ℝ) (x - u) : ℝ)
⊢ ⨅ (u : E), HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) u : ℝ) ((q : (a : E) → ℝ) (a • x - u) : ℝ) =
    ‖a‖ * ⨅ (u : E), HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) u : ℝ) ((q : (a : E) → ℝ) (x - u) : ℝ)
have inr : ∀ (ha : a ≠ 0),
  ⨅ (u : E), HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) u : ℝ) ((q : (a : E) → ℝ) (a • x - u) : ℝ) =
    ‖a‖ * ⨅ (u : E), HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) u : ℝ) ((q : (a : E) → ℝ) (x - u) : ℝ)
Tactic: obtain rfl | ha := eq_or_ne a 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
p_1 q_1 : Seminorm 𝕜 E
x_1 : E
p q : Seminorm 𝕜 E
x : E
⊢ ⨅ (u : E),
      HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) u : ℝ)
        ((q : (a : E) → ℝ) (HSMul.hSMul.{u_3, u_7, u_7} (α := 𝕜) 0 x - u) : ℝ) =
    norm.{u_3} (E := 𝕜) 0 *
      ⨅ (u : E), HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) u : ℝ) ((q : (a : E) → ℝ) (x - u) : ℝ)
have inl : Eq (α := ℝ) (⨅ (u : E), HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) u : ℝ) ((q : (a : E) → ℝ) (0 - u) : ℝ)) 0
Tactic: rw [norm_zero, zero_mul, zero_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
p_1 q_1 : Seminorm 𝕜 E
x_1 : E
p q : Seminorm 𝕜 E
x_2 : E
x : ℝ
hx : 0 < x
⊢ HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) 0 : ℝ) ((q : (a : E) → ℝ) (HSub.hSub (α := E) 0 0) : ℝ) < x
have rwa : HAdd.hAdd (α := ℝ) (β := ℝ) (0 : ℝ) ((q : (a : E) → ℝ) (HSub.hSub (α := E) 0 0) : ℝ) < x
Tactic: rwa [map_zero, sub_zero, 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_2 : E
x : ℝ
hx : 0 < x
rwa : HAdd.hAdd (α := ℝ) (β := ℝ) (0 : ℝ) ((q : (a : E) → ℝ) (HSub.hSub (α := E) 0 0) : ℝ) < x
⊢ HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) 0 : ℝ) ((q : (a : E) → ℝ) (HSub.hSub (α := E) 0 0) : ℝ) < x
have rwa₁ : HAdd.hAdd (α := ℝ) (β := ℝ) (0 : ℝ) ((q : (a : E) → ℝ) 0 : ℝ) < x
Tactic: rwa [map_zero, sub_zero, 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_2 : E
x : ℝ
hx : 0 < x
rwa : HAdd.hAdd (α := ℝ) (β := ℝ) (0 : ℝ) ((q : (a : E) → ℝ) (HSub.hSub (α := E) 0 0) : ℝ) < x
rwa₁ : HAdd.hAdd (α := ℝ) (β := ℝ) (0 : ℝ) ((q : (a : E) → ℝ) 0 : ℝ) < x
⊢ HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) 0 : ℝ) ((q : (a : E) → ℝ) (HSub.hSub (α := E) 0 0) : ℝ) < x
have rwa₂ : HAdd.hAdd (α := ℝ) 0 0 < x
Tactic: rwa [map_zero, sub_zero, 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
a : 𝕜
x : E
ha : a ≠ 0
⊢ ⨅ (u : E), HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) u : ℝ) ((q : (a : E) → ℝ) (a • x - u) : ℝ) =
    ‖a‖ * ⨅ (u : E), HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) u : ℝ) ((q : (a : E) → ℝ) (x - u) : ℝ)
have inr : 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) : ℝ))
Tactic: simp_rw [Real.mul_iInf_of_nonneg (norm_nonneg a), mul_add, ← map_smul_eq_mul p, ←
          map_smul_eq_mul q, smul_sub]