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 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)
⊢ Membership.mem (γ := Set ℝ)
    (upperBounds (range fun (i : { x : Seminorm 𝕜 E // x ∈ s }) ↦ (↑i : Seminorm 𝕜 E).toFun x)) (q x)
have inr : ∀ (i : { x : Seminorm 𝕜 E // x ∈ s }), (↑i : Seminorm 𝕜 E).toFun x ≤ q x
Tactic: rw [mem_upperBounds, forall_mem_range]
-- 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)
⊢ Membership.mem (γ := Set ℝ)
    (upperBounds (range fun (i : { x : Seminorm 𝕜 E // x ∈ s }) ↦ (↑i : Seminorm 𝕜 E).toFun y)) (q y)
have inr : ∀ (i : { x : Seminorm 𝕜 E // x ∈ s }), (↑i : Seminorm 𝕜 E).toFun y ≤ q y
Tactic: rw [mem_upperBounds, forall_mem_range]
-- 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 : E
⊢ Eq (α := ℝ) ((⨆ (p : (↑s : Type u_7)), (⇑(↑p : Seminorm 𝕜 E) : (a : E) → ℝ)) (-x))
    ((⨆ (p : (↑s : Type u_7)), (⇑(↑p : Seminorm 𝕜 E) : (a : E) → ℝ)) x)
have simp : Eq (α := ℝ) (⨆ (i : (↑s : Type u_7)), ((↑i : Seminorm 𝕜 E) : (a : E) → ℝ) (-x))
  (⨆ (i : (↑s : Type u_7)), ((↑i : Seminorm 𝕜 E) : (a : E) → ℝ) x)
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 : Seminorm 𝕜 E
x_1 : E
s : Set (Seminorm 𝕜 E)
h : BddAbove (α := E → ℝ) (DFunLike.coe (β := fun (x : E) ↦ ℝ) '' s)
x : E
⊢ Eq (α := ℝ) (⨆ (i : (↑s : Type u_7)), ((↑i : Seminorm 𝕜 E) : (a : E) → ℝ) (-x))
    (⨆ (i : (↑s : Type u_7)), ((↑i : Seminorm 𝕜 E) : (a : E) → ℝ) x)
have h₁ : ∀ (x_2 : (↑s : Type u_7)),
  Eq (α := ℝ) (((↑x_2 : Seminorm 𝕜 E) : (a : E) → ℝ) (-x) : ℝ) (((↑x_2 : Seminorm 𝕜 E) : (a : E) → ℝ) x : ℝ)
Tactic: congr! 2
-- 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)
a : 𝕜
x : E
⊢ (⨆ (p : (↑s : Type u_7)), (⇑(↑p : Seminorm 𝕜 E) : (a : E) → ℝ)) (a • x) =
    ‖a‖ * (⨆ (p : (↑s : Type u_7)), (⇑(↑p : Seminorm 𝕜 E) : (a : E) → ℝ)) x
have simp : ⨆ (i : (↑s : Type u_7)), ((↑i : Seminorm 𝕜 E) : (a : E) → ℝ) (a • x) =
  ‖a‖ * ⨆ (i : (↑s : Type u_7)), ((↑i : Seminorm 𝕜 E) : (a : E) → ℝ) x
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 : Seminorm 𝕜 E
x_1 : E
s : Set (Seminorm 𝕜 E)
h : BddAbove (α := E → ℝ) (DFunLike.coe (β := fun (x : E) ↦ ℝ) '' s)
a : 𝕜
x : E
⊢ ⨆ (i : (↑s : Type u_7)), ((↑i : Seminorm 𝕜 E) : (a : E) → ℝ) (a • x) =
    ‖a‖ * ⨆ (i : (↑s : Type u_7)), ((↑i : Seminorm 𝕜 E) : (a : E) → ℝ) x
have rw : Eq (α := ℝ) (⨆ (i : (↑s : Type u_7)), ((↑i : Seminorm 𝕜 E) : (a : E) → ℝ) (a • x))
  (⨆ (i : (↑s : Type u_7)), HSMul.hSMul (β := ℝ) ‖a‖ (((↑i : Seminorm 𝕜 E) : (a : E) → ℝ) x : ℝ))
Tactic: rw [← smul_eq_mul,
            Real.smul_iSup_of_nonneg (norm_nonneg a) fun i : s => (i : Seminorm 𝕜 E) 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
p q : Seminorm 𝕜 E
x_1 : E
s : Set (Seminorm 𝕜 E)
h : BddAbove (α := E → ℝ) (DFunLike.coe (β := fun (x : E) ↦ ℝ) '' s)
a : 𝕜
x : E
⊢ Eq (α := ℝ) (⨆ (i : (↑s : Type u_7)), ((↑i : Seminorm 𝕜 E) : (a : E) → ℝ) (a • x))
    (⨆ (i : (↑s : Type u_7)), HSMul.hSMul (β := ℝ) ‖a‖ (((↑i : Seminorm 𝕜 E) : (a : E) → ℝ) x : ℝ))
have h₁ : ∀ (x_2 : (↑s : Type u_7)),
  ((↑x_2 : Seminorm 𝕜 E) : (a : E) → ℝ) (a • x) = HSMul.hSMul (β := ℝ) ‖a‖ (((↑x_2 : Seminorm 𝕜 E) : (a : E) → ℝ) x : ℝ)
Tactic: congr!
-- 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
s : Set (Seminorm 𝕜 E)
H : BddAbove (α := E → ℝ) (DFunLike.coe (β := fun (x : E) ↦ ℝ) '' s)
p : Seminorm 𝕜 E
hp : p ∈ s
x : E
⊢ LE.le (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ((sSup s : (a : E) → ℝ) x : ℝ)
have rw : LE.le (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) (⨆ (i : (↑s : Type u_7)), ((↑i : Seminorm 𝕜 E) : (a : E) → ℝ) x : ℝ)
Tactic: rw [Seminorm.coe_sSup_eq' H, iSup_apply]
-- 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
s : Set (Seminorm 𝕜 E)
H : BddAbove (α := E → ℝ) (DFunLike.coe (β := fun (x : E) ↦ ℝ) '' s)
p : Seminorm 𝕜 E
hp : p ∈ s
x : E
⊢ LE.le (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) (⨆ (i : (↑s : Type u_7)), ((↑i : Seminorm 𝕜 E) : (a : E) → ℝ) x : ℝ)
have rcases : ∀ (q : E → ℝ) (hq : Membership.mem (γ := Set (E → ℝ)) (upperBounds (DFunLike.coe (β := fun (x : E) ↦ ℝ) '' s)) q),
  LE.le (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) (⨆ (i : (↑s : Type u_7)), ((↑i : Seminorm 𝕜 E) : (a : E) → ℝ) x : ℝ)
Tactic: rcases H with ⟨q, hq⟩
Cleared hypotheses: H
-- 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
ι : Sort u_12
p : ι → Seminorm 𝕜 E
⊢ BddAbove (range p) ↔ ∀ (x : E), BddAbove (α := ℝ) (range fun (i : ι) ↦ (p i : (a : E) → ℝ) x)
have rw : (∀ (a : E), BddAbove (α := ℝ) (range fun (i : ι) ↦ (DFunLike.coe (β := fun (x : E) ↦ ℝ) ∘ p) i a)) ↔
  ∀ (x : E), BddAbove (α := ℝ) (range fun (i : ι) ↦ (p i : (a : E) → ℝ) x)
Tactic: rw [Seminorm.bddAbove_iff, ← range_comp, bddAbove_range_pi]
-- 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
ι : Sort u_12
p : ι → Seminorm 𝕜 E
hp : BddAbove (range p)
⊢ Eq.{u_7 + 1} (α := (a : E) → ℝ) (⇑(⨆ (i : ι), p i) : (a : E) → ℝ) (⨆ (i : ι), (⇑(p i) : (a : E) → ℝ))
have rw : Eq.{u_7 + 1} (α := (a : E) → ℝ) (⨆ (p_1 : (↑(range p) : Type u_7)), (⇑(↑p_1 : Seminorm 𝕜 E) : (a : E) → ℝ))
  (⨆ (i : ι), (⇑(p i) : (a : E) → ℝ))
Tactic: rw [← sSup_range, Seminorm.coe_sSup_eq hp]
-- 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
s : Set (Seminorm 𝕜 E)
hp : BddAbove s
x : E
⊢ Eq (α := ℝ) ((sSup s : (a : E) → ℝ) x : ℝ) (⨆ (p : (↑s : Type u_7)), ((↑p : Seminorm 𝕜 E) : (a : E) → ℝ) x : ℝ)
have rw : Eq (α := ℝ) ((⨆ (p : (↑s : Type u_7)), (⇑(↑p : Seminorm 𝕜 E) : (a : E) → ℝ)) x)
  (⨆ (p : (↑s : Type u_7)), ((↑p : Seminorm 𝕜 E) : (a : E) → ℝ) x)
Tactic: rw [Seminorm.coe_sSup_eq hp, iSup_apply]
-- 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
s : Set (Seminorm 𝕜 E)
hp : BddAbove s
x : E
rw :
  Eq (α := ℝ) ((⨆ (p : (↑s : Type u_7)), (⇑(↑p : Seminorm 𝕜 E) : (a : E) → ℝ)) x)
    (⨆ (p : (↑s : Type u_7)), ((↑p : Seminorm 𝕜 E) : (a : E) → ℝ) x)
⊢ Eq (α := ℝ) ((sSup s : (a : E) → ℝ) x : ℝ) (⨆ (p : (↑s : Type u_7)), ((↑p : Seminorm 𝕜 E) : (a : E) → ℝ) x : ℝ)
have rw₁ : Eq (α := ℝ) (⨆ (i : (↑s : Type u_7)), ((↑i : Seminorm 𝕜 E) : (a : E) → ℝ) x)
  (⨆ (p : (↑s : Type u_7)), ((↑p : Seminorm 𝕜 E) : (a : E) → ℝ) x)
Tactic: rw [Seminorm.coe_sSup_eq hp, iSup_apply]
-- 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
ι : Sort u_12
p : ι → Seminorm 𝕜 E
hp : BddAbove (range p)
x : E
⊢ Eq (α := ℝ) ((⨆ (i : ι), p i : (a : E) → ℝ) x : ℝ) (⨆ (i : ι), (p i : (a : E) → ℝ) x : ℝ)
have rw : Eq (α := ℝ) ((⨆ (i : ι), (⇑(p i) : (a : E) → ℝ)) x) (⨆ (i : ι), (p i : (a : E) → ℝ) x)
Tactic: rw [Seminorm.coe_iSup_eq hp, iSup_apply]
-- 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
ι : Sort u_12
p : ι → Seminorm 𝕜 E
hp : BddAbove (range p)
x : E
rw : Eq (α := ℝ) ((⨆ (i : ι), (⇑(p i) : (a : E) → ℝ)) x) (⨆ (i : ι), (p i : (a : E) → ℝ) x)
⊢ Eq (α := ℝ) ((⨆ (i : ι), p i : (a : E) → ℝ) x : ℝ) (⨆ (i : ι), (p i : (a : E) → ℝ) x : ℝ)
have rw₁ : Eq (α := ℝ) (⨆ (i : ι), (p i : (a : E) → ℝ) x) (⨆ (i : ι), (p i : (a : E) → ℝ) x)
Tactic: rw [Seminorm.coe_iSup_eq hp, iSup_apply]
-- 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
⊢ Eq.{u_7 + 1} (α := Seminorm 𝕜 E) (sSup ∅) ⊥
have h : ∀ (x : E), Eq (α := ℝ) ((sSup ∅ : (a : E) → ℝ) x : ℝ) ((⊥ : (a : E) → ℝ) x : ℝ)
Tactic: ext
-- 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
x : E
⊢ Eq (α := ℝ) ((sSup ∅ : (a : E) → ℝ) x : ℝ) ((⊥ : (a : E) → ℝ) x : ℝ)
have h : Eq (α := ℝ) (0 : ℝ) ((⊥ : (a : E) → ℝ) x : ℝ)
Tactic: rw [Seminorm.sSup_apply bddAbove_empty, Real.iSup_of_isEmpty]
-- 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
s : Set (Seminorm 𝕜 E)
hs₁ : BddAbove s
hs₂ : s.Nonempty
⊢ IsLUB s (sSup s)
have refine_1 : ∀ (p : Seminorm 𝕜 E) (hp : p ∈ s) (x : E),
  LE.le (α := (fun (a : E) ↦ ℝ) x) ((fun (f : Seminorm 𝕜 E) ↦ ((⇑f : (a : E) → ℝ) : (a : E) → ℝ)) p x)
    ((fun (f : Seminorm 𝕜 E) ↦ ((⇑f : (a : E) → ℝ) : (a : E) → ℝ)) (sSup s) x)
Tactic: refine ⟨fun p hp x => ?_, fun p hp x => ?_⟩
-- 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
s : Set (Seminorm 𝕜 E)
hs₁ : BddAbove s
hs₂ : s.Nonempty
refine_1 :
  ∀ (p : Seminorm 𝕜 E) (hp : p ∈ s) (x : E),
    LE.le (α := (fun (a : E) ↦ ℝ) x) ((fun (f : Seminorm 𝕜 E) ↦ ((⇑f : (a : E) → ℝ) : (a : E) → ℝ)) p x)
      ((fun (f : Seminorm 𝕜 E) ↦ ((⇑f : (a : E) → ℝ) : (a : E) → ℝ)) (sSup s) x)
⊢ IsLUB s (sSup s)
have refine_2 : ∀ (p : Seminorm 𝕜 E) (hp : p ∈ upperBounds s) (x : E),
  LE.le (α := (fun (a : E) ↦ ℝ) x) ((fun (f : Seminorm 𝕜 E) ↦ ((⇑f : (a : E) → ℝ) : (a : E) → ℝ)) (sSup s) x)
    ((fun (f : Seminorm 𝕜 E) ↦ ((⇑f : (a : E) → ℝ) : (a : E) → ℝ)) p x)
Tactic: refine ⟨fun p hp x => ?_, fun p hp x => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (hypothesis)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set (Seminorm 𝕜 E)
hs₁ : BddAbove s
hs₂ : s.Nonempty
p : Seminorm 𝕜 E
hp : p ∈ s
x : E
⊢ LE.le (α := (fun (a : E) ↦ ℝ) x) ((fun (f : Seminorm 𝕜 E) ↦ ((⇑f : (a : E) → ℝ) : (a : E) → ℝ)) p x)
    ((fun (f : Seminorm 𝕜 E) ↦ ((⇑f : (a : E) → ℝ) : (a : E) → ℝ)) (sSup s) x)
have this : Nonempty.{u_7 + 1} (↑s : Type u_7)
Tactic: haveI : Nonempty ↑s := hs₂.coe_sort
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (hypothesis)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set (Seminorm 𝕜 E)
hs₁ : BddAbove s
hs₂ : s.Nonempty
p : Seminorm 𝕜 E
hp : p ∈ upperBounds s
x : E
⊢ LE.le (α := (fun (a : E) ↦ ℝ) x) ((fun (f : Seminorm 𝕜 E) ↦ ((⇑f : (a : E) → ℝ) : (a : E) → ℝ)) (sSup s) x)
    ((fun (f : Seminorm 𝕜 E) ↦ ((⇑f : (a : E) → ℝ) : (a : E) → ℝ)) p x)
have this : Nonempty.{u_7 + 1} (↑s : Type u_7)
Tactic: haveI : Nonempty ↑s := hs₂.coe_sort
-- 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
s : Set (Seminorm 𝕜 E)
hs₁ : BddAbove s
hs₂ : s.Nonempty
p : Seminorm 𝕜 E
hp : p ∈ s
x : E
this : Nonempty.{u_7 + 1} (↑s : Type u_7)
⊢ LE.le (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ((sSup s : (a : E) → ℝ) x : ℝ)
have refine_1 : LE.le (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) (⨆ (i : (↑s : Type u_7)), ((↑i : Seminorm 𝕜 E) : (a : E) → ℝ) x : ℝ)
Tactic: rw [Seminorm.coe_sSup_eq hs₁, iSup_apply]
-- 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
s : Set (Seminorm 𝕜 E)
hs₁ : BddAbove s
hs₂ : s.Nonempty
p : Seminorm 𝕜 E
hp : p ∈ upperBounds s
x : E
this : Nonempty.{u_7 + 1} (↑s : Type u_7)
⊢ LE.le (α := ℝ) ((sSup s : (a : E) → ℝ) x : ℝ) ((p : (a : E) → ℝ) x : ℝ)
have refine_2 : LE.le (α := ℝ) (⨆ (i : (↑s : Type u_7)), ((↑i : Seminorm 𝕜 E) : (a : E) → ℝ) x : ℝ) ((p : (a : E) → ℝ) x : ℝ)
Tactic: rw [Seminorm.coe_sSup_eq hs₁, iSup_apply]
-- 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
s : Set (Seminorm 𝕜 E)
hs₁ : BddAbove s
hs₂ : s.Nonempty
p : Seminorm 𝕜 E
hp : p ∈ s
x : E
this : Nonempty.{u_7 + 1} (↑s : Type u_7)
⊢ LE.le (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) (⨆ (i : (↑s : Type u_7)), ((↑i : Seminorm 𝕜 E) : (a : E) → ℝ) x : ℝ)
have refine_1 : ∀ (q : Seminorm 𝕜 E) (hq : q ∈ upperBounds s),
  LE.le (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) (⨆ (i : (↑s : Type u_7)), ((↑i : Seminorm 𝕜 E) : (a : E) → ℝ) x : ℝ)
Tactic: rcases hs₁ with ⟨q, hq⟩
Cleared hypotheses: hs₁
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : SMul 𝕜 E
p : Seminorm 𝕜 E
y : E
r : ℝ
⊢ y ∈ p.ball 0 r ↔ (p : (a : E) → ℝ) y < r
have rw : (p : (a : E) → ℝ) (y - 0) < r ↔ (p : (a : E) → ℝ) y < r
Tactic: rw [mem_ball, sub_zero]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : SMul 𝕜 E
p : Seminorm 𝕜 E
y : E
r : ℝ
rw : (p : (a : E) → ℝ) (y - 0) < r ↔ (p : (a : E) → ℝ) y < r
⊢ y ∈ p.ball 0 r ↔ (p : (a : E) → ℝ) y < r
have rw₁ : (p : (a : E) → ℝ) y < r ↔ (p : (a : E) → ℝ) y < r
Tactic: rw [mem_ball, sub_zero]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : SMul 𝕜 E
p : Seminorm 𝕜 E
y : E
r : ℝ
⊢ y ∈ p.closedBall 0 r ↔ (p : (a : E) → ℝ) y ≤ r
have rw : (p : (a : E) → ℝ) (y - 0) ≤ r ↔ (p : (a : E) → ℝ) y ≤ r
Tactic: rw [mem_closedBall, sub_zero]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : SMul 𝕜 E
p : Seminorm 𝕜 E
y : E
r : ℝ
rw : (p : (a : E) → ℝ) (y - 0) ≤ r ↔ (p : (a : E) → ℝ) y ≤ r
⊢ y ∈ p.closedBall 0 r ↔ (p : (a : E) → ℝ) y ≤ r
have rw₁ : (p : (a : E) → ℝ) y ≤ r ↔ (p : (a : E) → ℝ) y ≤ r
Tactic: rw [mem_closedBall, sub_zero]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : SMul 𝕜 E
p : Seminorm 𝕜 E
x : E
r : ℝ
⊢ p.closedBall x r = ⋂ (ρ : ℝ), ⋂ (_ : ρ > r), p.ball x ρ
have h : ∀ (y : E), y ∈ p.closedBall x r ↔ Membership.mem (γ := Set E) (⋂ (ρ : ℝ), ⋂ (_ : ρ > r), p.ball x ρ) y
Tactic: ext y
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : SMul 𝕜 E
p : Seminorm 𝕜 E
x : E
r : ℝ
y : E
⊢ y ∈ p.closedBall x r ↔ Membership.mem (γ := Set E) (⋂ (ρ : ℝ), ⋂ (_ : ρ > r), p.ball x ρ) y
have h : (p : (a : E) → ℝ) (y - x) ≤ r ↔ Membership.mem (γ := Set E) (⋂ (ρ : ℝ), ⋂ (_ : ρ > r), p.ball x ρ) y
Tactic: simp_rw [mem_closedBall, mem_iInter₂, mem_ball, ← forall_gt_iff_le]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : SMul 𝕜 E
p : Seminorm 𝕜 E
x : E
r : ℝ
y : E
h : (p : (a : E) → ℝ) (y - x) ≤ r ↔ Membership.mem (γ := Set E) (⋂ (ρ : ℝ), ⋂ (_ : ρ > r), p.ball x ρ) y
⊢ y ∈ p.closedBall x r ↔ Membership.mem (γ := Set E) (⋂ (ρ : ℝ), ⋂ (_ : ρ > r), p.ball x ρ) y
have h₁ : (p : (a : E) → ℝ) (y - x) ≤ r ↔ ∀ (i : ℝ) (j : i > r), y ∈ p.ball x i
Tactic: simp_rw [mem_closedBall, mem_iInter₂, mem_ball, ← forall_gt_iff_le]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : SMul 𝕜 E
p : Seminorm 𝕜 E
x : E
r : ℝ
y : E
h : (p : (a : E) → ℝ) (y - x) ≤ r ↔ Membership.mem (γ := Set E) (⋂ (ρ : ℝ), ⋂ (_ : ρ > r), p.ball x ρ) y
h₁ : (p : (a : E) → ℝ) (y - x) ≤ r ↔ ∀ (i : ℝ) (j : i > r), y ∈ p.ball x i
⊢ y ∈ p.closedBall x r ↔ Membership.mem (γ := Set E) (⋂ (ρ : ℝ), ⋂ (_ : ρ > r), p.ball x ρ) y
have h₂ : (p : (a : E) → ℝ) (y - x) ≤ r ↔ ∀ (i : ℝ) (j : i > r), (p : (a : E) → ℝ) (y - x) < i
Tactic: simp_rw [mem_closedBall, mem_iInter₂, mem_ball, ← forall_gt_iff_le]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : SMul 𝕜 E
r : ℝ
x : E
hr : 0 < r
⊢ ball.{u_3, u_7} (𝕜 := 𝕜) 0 x r = univ
have rw : ∀ (x_1 : E), Membership.mem (γ := Set E) {y : E | (0 : (a : E) → ℝ) (y - x) < r} x_1
Tactic: rw [Set.eq_univ_iff_forall, ball]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : SMul 𝕜 E
p : Seminorm 𝕜 E
c : ℝ≥0
hc : 0 < c
r : ℝ
x : E
⊢ (c • p).ball x r = p.ball x (r / (↑c : ℝ))
have h : ∀ (x_1 : E), x_1 ∈ (c • p).ball x r ↔ x_1 ∈ p.ball x (r / (↑c : ℝ))
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : SMul 𝕜 E
p : Seminorm 𝕜 E
c : ℝ≥0
hc : 0 < c
r : ℝ
x x_1 : E
⊢ x_1 ∈ (c • p).ball x r ↔ x_1 ∈ p.ball x (r / (↑c : ℝ))
have h : (c • p : (a : E) → ℝ) (x_1 - x) < r ↔ x_1 ∈ p.ball x (r / (↑c : ℝ))
Tactic: rw [mem_ball, mem_ball, smul_apply, NNReal.smul_def, smul_eq_mul, mul_comm,
    lt_div_iff₀ (NNReal.coe_pos.mpr hc)]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : SMul 𝕜 E
p : Seminorm 𝕜 E
c : ℝ≥0
hc : 0 < c
r : ℝ
x x_1 : E
h : (c • p : (a : E) → ℝ) (x_1 - x) < r ↔ x_1 ∈ p.ball x (r / (↑c : ℝ))
⊢ x_1 ∈ (c • p).ball x r ↔ x_1 ∈ p.ball x (r / (↑c : ℝ))
have h₁ : (c • p : (a : E) → ℝ) (x_1 - x) < r ↔ (p : (a : E) → ℝ) (x_1 - x) < r / (↑c : ℝ)
Tactic: rw [mem_ball, mem_ball, smul_apply, NNReal.smul_def, smul_eq_mul, mul_comm,
    lt_div_iff₀ (NNReal.coe_pos.mpr hc)]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : SMul 𝕜 E
p : Seminorm 𝕜 E
c : ℝ≥0
hc : 0 < c
r : ℝ
x x_1 : E
h : (c • p : (a : E) → ℝ) (x_1 - x) < r ↔ x_1 ∈ p.ball x (r / (↑c : ℝ))
h₁ : (c • p : (a : E) → ℝ) (x_1 - x) < r ↔ (p : (a : E) → ℝ) (x_1 - x) < r / (↑c : ℝ)
⊢ x_1 ∈ (c • p).ball x r ↔ x_1 ∈ p.ball x (r / (↑c : ℝ))
have h₂ : HSMul.hSMul (β := ℝ) c ((p : (a : E) → ℝ) (x_1 - x) : ℝ) < r ↔ (p : (a : E) → ℝ) (x_1 - x) < r / (↑c : ℝ)
Tactic: rw [mem_ball, mem_ball, smul_apply, NNReal.smul_def, smul_eq_mul, mul_comm,
    lt_div_iff₀ (NNReal.coe_pos.mpr hc)]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : SMul 𝕜 E
p : Seminorm 𝕜 E
c : ℝ≥0
hc : 0 < c
r : ℝ
x x_1 : E
h : (c • p : (a : E) → ℝ) (x_1 - x) < r ↔ x_1 ∈ p.ball x (r / (↑c : ℝ))
h₁ : (c • p : (a : E) → ℝ) (x_1 - x) < r ↔ (p : (a : E) → ℝ) (x_1 - x) < r / (↑c : ℝ)
h₂ : HSMul.hSMul (β := ℝ) c ((p : (a : E) → ℝ) (x_1 - x) : ℝ) < r ↔ (p : (a : E) → ℝ) (x_1 - x) < r / (↑c : ℝ)
⊢ x_1 ∈ (c • p).ball x r ↔ x_1 ∈ p.ball x (r / (↑c : ℝ))
have h₃ : HSMul.hSMul (β := ℝ) (↑c : ℝ) ((p : (a : E) → ℝ) (x_1 - x) : ℝ) < r ↔ (p : (a : E) → ℝ) (x_1 - x) < r / (↑c : ℝ)
Tactic: rw [mem_ball, mem_ball, smul_apply, NNReal.smul_def, smul_eq_mul, mul_comm,
    lt_div_iff₀ (NNReal.coe_pos.mpr hc)]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : SMul 𝕜 E
p : Seminorm 𝕜 E
c : ℝ≥0
hc : 0 < c
r : ℝ
x x_1 : E
h : (c • p : (a : E) → ℝ) (x_1 - x) < r ↔ x_1 ∈ p.ball x (r / (↑c : ℝ))
h₁ : (c • p : (a : E) → ℝ) (x_1 - x) < r ↔ (p : (a : E) → ℝ) (x_1 - x) < r / (↑c : ℝ)
h₂ : HSMul.hSMul (β := ℝ) c ((p : (a : E) → ℝ) (x_1 - x) : ℝ) < r ↔ (p : (a : E) → ℝ) (x_1 - x) < r / (↑c : ℝ)
h₃ : HSMul.hSMul (β := ℝ) (↑c : ℝ) ((p : (a : E) → ℝ) (x_1 - x) : ℝ) < r ↔ (p : (a : E) → ℝ) (x_1 - x) < r / (↑c : ℝ)
⊢ x_1 ∈ (c • p).ball x r ↔ x_1 ∈ p.ball x (r / (↑c : ℝ))
have h₄ : HMul.hMul (β := ℝ) (↑c : ℝ) ((p : (a : E) → ℝ) (x_1 - x) : ℝ) < r ↔ (p : (a : E) → ℝ) (x_1 - x) < r / (↑c : ℝ)
Tactic: rw [mem_ball, mem_ball, smul_apply, NNReal.smul_def, smul_eq_mul, mul_comm,
    lt_div_iff₀ (NNReal.coe_pos.mpr hc)]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : SMul 𝕜 E
p : Seminorm 𝕜 E
c : ℝ≥0
hc : 0 < c
r : ℝ
x x_1 : E
h : (c • p : (a : E) → ℝ) (x_1 - x) < r ↔ x_1 ∈ p.ball x (r / (↑c : ℝ))
h₁ : (c • p : (a : E) → ℝ) (x_1 - x) < r ↔ (p : (a : E) → ℝ) (x_1 - x) < r / (↑c : ℝ)
h₂ : HSMul.hSMul (β := ℝ) c ((p : (a : E) → ℝ) (x_1 - x) : ℝ) < r ↔ (p : (a : E) → ℝ) (x_1 - x) < r / (↑c : ℝ)
h₃ : HSMul.hSMul (β := ℝ) (↑c : ℝ) ((p : (a : E) → ℝ) (x_1 - x) : ℝ) < r ↔ (p : (a : E) → ℝ) (x_1 - x) < r / (↑c : ℝ)
h₄ : HMul.hMul (β := ℝ) (↑c : ℝ) ((p : (a : E) → ℝ) (x_1 - x) : ℝ) < r ↔ (p : (a : E) → ℝ) (x_1 - x) < r / (↑c : ℝ)
⊢ x_1 ∈ (c • p).ball x r ↔ x_1 ∈ p.ball x (r / (↑c : ℝ))
have h₅ : HMul.hMul (α := ℝ) ((p : (a : E) → ℝ) (x_1 - x) : ℝ) (↑c : ℝ) < r ↔ (p : (a : E) → ℝ) (x_1 - x) < r / (↑c : ℝ)
Tactic: rw [mem_ball, mem_ball, smul_apply, NNReal.smul_def, smul_eq_mul, mul_comm,
    lt_div_iff₀ (NNReal.coe_pos.mpr hc)]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : SMul 𝕜 E
p : Seminorm 𝕜 E
c : ℝ≥0
hc : 0 < c
r : ℝ
x x_1 : E
h : (c • p : (a : E) → ℝ) (x_1 - x) < r ↔ x_1 ∈ p.ball x (r / (↑c : ℝ))
h₁ : (c • p : (a : E) → ℝ) (x_1 - x) < r ↔ (p : (a : E) → ℝ) (x_1 - x) < r / (↑c : ℝ)
h₂ : HSMul.hSMul (β := ℝ) c ((p : (a : E) → ℝ) (x_1 - x) : ℝ) < r ↔ (p : (a : E) → ℝ) (x_1 - x) < r / (↑c : ℝ)
h₃ : HSMul.hSMul (β := ℝ) (↑c : ℝ) ((p : (a : E) → ℝ) (x_1 - x) : ℝ) < r ↔ (p : (a : E) → ℝ) (x_1 - x) < r / (↑c : ℝ)
h₄ : HMul.hMul (β := ℝ) (↑c : ℝ) ((p : (a : E) → ℝ) (x_1 - x) : ℝ) < r ↔ (p : (a : E) → ℝ) (x_1 - x) < r / (↑c : ℝ)
h₅ : HMul.hMul (α := ℝ) ((p : (a : E) → ℝ) (x_1 - x) : ℝ) (↑c : ℝ) < r ↔ (p : (a : E) → ℝ) (x_1 - x) < r / (↑c : ℝ)
⊢ x_1 ∈ (c • p).ball x r ↔ x_1 ∈ p.ball x (r / (↑c : ℝ))
have h₆ : HMul.hMul (α := ℝ) ((p : (a : E) → ℝ) (x_1 - x) : ℝ) (↑c : ℝ) < r ↔
  HMul.hMul (α := ℝ) ((p : (a : E) → ℝ) (x_1 - x) : ℝ) (↑c : ℝ) < r
Tactic: rw [mem_ball, mem_ball, smul_apply, NNReal.smul_def, smul_eq_mul, mul_comm,
    lt_div_iff₀ (NNReal.coe_pos.mpr hc)]