awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Seminorm
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 : { x : Seminorm 𝕜 E // x ∈ s }), (↑i : Seminorm 𝕜 E).toFun y ≤ q y

Tactic:
fun j => hq (mem_image_of_mem _ j.2) _

Premises used: Set.mem_image_of_mem, DFunLike.coe, Subtype.property
-- Module: Mathlib.Analysis.Seminorm
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 : { x : Seminorm 𝕜 E // x ∈ s }), (↑i : Seminorm 𝕜 E).toFun y ≤ q y

Tactic:
exact fun j => hq (mem_image_of_mem _ j.2) _

Premises used: Set.mem_image_of_mem, DFunLike.coe
-- Module: Mathlib.Analysis.Seminorm
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
simp :
  Eq (α := ℝ) (⨆ (i : (↑s : Type u_7)), ((↑i : Seminorm 𝕜 E) : (a : E) → ℝ) (-x))
    (⨆ (i : (↑s : Type u_7)), ((↑i : Seminorm 𝕜 E) : (a : E) → ℝ) x)
⊢ Eq (α := ℝ) ((⨆ (p : (↑s : Type u_7)), (⇑(↑p : Seminorm 𝕜 E) : (a : E) → ℝ)) (-x))
    ((⨆ (p : (↑s : Type u_7)), (⇑(↑p : Seminorm 𝕜 E) : (a : E) → ℝ)) x)

Tactic:
simp only [iSup_apply]

Premises used: iSup_apply
-- Module: Mathlib.Analysis.Seminorm
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
h₁ :
  ∀ (x_2 : (↑s : Type u_7)),
    Eq (α := ℝ) (((↑x_2 : Seminorm 𝕜 E) : (a : E) → ℝ) (-x) : ℝ) (((↑x_2 : Seminorm 𝕜 E) : (a : E) → ℝ) x : ℝ)
⊢ Eq (α := ℝ) (⨆ (i : (↑s : Type u_7)), ((↑i : Seminorm 𝕜 E) : (a : E) → ℝ) (-x))
    (⨆ (i : (↑s : Type u_7)), ((↑i : Seminorm 𝕜 E) : (a : E) → ℝ) x)

Tactic:
congr! 2
-- Module: Mathlib.Analysis.Seminorm
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
i : (↑s : Type u_7)
⊢ Eq (α := ℝ) (((↑i : Seminorm 𝕜 E) : (a : E) → ℝ) (-x) : ℝ) (((↑i : Seminorm 𝕜 E) : (a : E) → ℝ) x : ℝ)

Tactic:
i.1.neg' _

Premises used: AddGroupSeminorm.neg', Seminorm.toAddGroupSeminorm, Subtype.val
-- Module: Mathlib.Analysis.Seminorm
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
i : (↑s : Type u_7)
⊢ Eq (α := ℝ) (((↑i : Seminorm 𝕜 E) : (a : E) → ℝ) (-x) : ℝ) (((↑i : Seminorm 𝕜 E) : (a : E) → ℝ) x : ℝ)

Tactic:
exact i.1.neg' _

Premises used: AddGroupSeminorm.neg', Seminorm.toAddGroupSeminorm, Subtype.val
-- Module: Mathlib.Analysis.Seminorm
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
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
⊢ (⨆ (p : (↑s : Type u_7)), (⇑(↑p : Seminorm 𝕜 E) : (a : E) → ℝ)) (a • x) =
    ‖a‖ * (⨆ (p : (↑s : Type u_7)), (⇑(↑p : Seminorm 𝕜 E) : (a : E) → ℝ)) x

Tactic:
simp only [iSup_apply]

Premises used: iSup_apply
-- Module: Mathlib.Analysis.Seminorm
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
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 : ℝ))
⊢ ⨆ (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:
rw [← smul_eq_mul,
            Real.smul_iSup_of_nonneg (norm_nonneg a) fun i : s => (i : Seminorm 𝕜 E) x]

Premises used: Real.smul_iSup_of_nonneg, smul_eq_mul, Subtype.val, DFunLike.coe, norm_nonneg
-- Module: Mathlib.Analysis.Seminorm
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
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 : ℝ)
⊢ 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:
congr!
-- Module: Mathlib.Analysis.Seminorm
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) = HSMul.hSMul (β := ℝ) ‖a‖ (((↑i : Seminorm 𝕜 E) : (a : E) → ℝ) x : ℝ)

Tactic:
i.1.smul' a x

Premises used: Seminorm.smul', Subtype.val
-- Module: Mathlib.Analysis.Seminorm
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) = HSMul.hSMul (β := ℝ) ‖a‖ (((↑i : Seminorm 𝕜 E) : (a : E) → ℝ) x : ℝ)

Tactic:
exact i.1.smul' a x

Premises used: Seminorm.smul', Subtype.val
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set (Seminorm 𝕜 E)
hs : BddAbove (α := E → ℝ) (DFunLike.coe (β := fun (x : E) ↦ ℝ) '' s)
⊢ Eq (α := (a : E) → ℝ) (⇑(sSup s) : (a : E) → ℝ) (⨆ (p : (↑s : Type u_7)), (⇑(↑p : Seminorm 𝕜 E) : (a : E) → ℝ))

Tactic:
congr_arg _ (dif_pos hs)

Premises used: iSup, dif_pos, congr_arg
-- Module: Mathlib.Analysis.Seminorm
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
rw : LE.le (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) (⨆ (i : (↑s : Type u_7)), ((↑i : Seminorm 𝕜 E) : (a : E) → ℝ) x : ℝ)
⊢ LE.le (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ((sSup s : (a : E) → ℝ) x : ℝ)

Tactic:
rw [Seminorm.coe_sSup_eq' H, iSup_apply]

Premises used: Seminorm.coe_sSup_eq', iSup_apply
-- Module: Mathlib.Analysis.Seminorm
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
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 : ℝ)
⊢ LE.le (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) (⨆ (i : (↑s : Type u_7)), ((↑i : Seminorm 𝕜 E) : (a : E) → ℝ) x : ℝ)

Tactic:
rcases H with ⟨q, hq⟩
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set (Seminorm 𝕜 E)
p : Seminorm 𝕜 E
hp : p ∈ s
x : E
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:
le_ciSup ⟨q x, forall_mem_range.mpr fun i : s => hq (mem_image_of_mem _ i.2) x⟩ ⟨p, hp⟩

Premises used: Iff.mpr, Set.forall_mem_range, Subtype.mk, le_ciSup, Set.mem_image_of_mem, Exists.intro, DFunLike.coe, Subtype.property
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set (Seminorm 𝕜 E)
p : Seminorm 𝕜 E
hp : p ∈ s
x : E
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:
exact
        le_ciSup ⟨q x, forall_mem_range.mpr fun i : s => hq (mem_image_of_mem _ i.2) x⟩ ⟨p, hp⟩

Premises used: Iff.mpr, Set.forall_mem_range, Subtype.mk, le_ciSup, Set.mem_image_of_mem, Exists.intro, DFunLike.coe, Subtype.property
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
ι : Sort u_12
p : ι → Seminorm 𝕜 E
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)
⊢ BddAbove (range p) ↔ ∀ (x : E), BddAbove (α := ℝ) (range fun (i : ι) ↦ (p i : (a : E) → ℝ) x)

Tactic:
rw [Seminorm.bddAbove_iff, ← range_comp, bddAbove_range_pi]

Premises used: Set.range_comp, Seminorm.bddAbove_iff, bddAbove_range_pi
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
ι : Sort u_12
p : ι → Seminorm 𝕜 E
⊢ (∀ (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:
rfl
-- Module: Mathlib.Analysis.Seminorm
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
⊢ Eq (α := (a : E) → ℝ) (⇑(sSup s) : (a : E) → ℝ) (⨆ (p : (↑s : Type u_7)), (⇑(↑p : Seminorm 𝕜 E) : (a : E) → ℝ))

Tactic:
Seminorm.coe_sSup_eq' (Seminorm.bddAbove_iff.mp hs)

Premises used: Seminorm.bddAbove_iff, Seminorm.coe_sSup_eq', Iff.mp
-- Module: Mathlib.Analysis.Seminorm
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)
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) → ℝ))
⊢ Eq.{u_7 + 1} (α := (a : E) → ℝ) (⇑(⨆ (i : ι), p i) : (a : E) → ℝ) (⨆ (i : ι), (⇑(p i) : (a : E) → ℝ))

Tactic:
rw [← sSup_range, Seminorm.coe_sSup_eq hp]

Premises used: Seminorm.coe_sSup_eq, sSup_range
-- Module: Mathlib.Analysis.Seminorm
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) → ℝ) (⨆ (p_1 : (↑(range p) : Type u_7)), (⇑(↑p_1 : Seminorm 𝕜 E) : (a : E) → ℝ))
    (⨆ (i : ι), (⇑(p i) : (a : E) → ℝ))

Tactic:
iSup_range' (fun p : Seminorm 𝕜 E => (p : E → ℝ)) p

Premises used: iSup_range', DFunLike.coe
-- Module: Mathlib.Analysis.Seminorm
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) → ℝ) (⨆ (p_1 : (↑(range p) : Type u_7)), (⇑(↑p_1 : Seminorm 𝕜 E) : (a : E) → ℝ))
    (⨆ (i : ι), (⇑(p i) : (a : E) → ℝ))

Tactic:
exact iSup_range' (fun p : Seminorm 𝕜 E => (p : E → ℝ)) p

Premises used: iSup_range', DFunLike.coe
-- Module: Mathlib.Analysis.Seminorm
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)
rw₁ rw₂ :
  Eq (α := ℝ) (⨆ (i : (↑s : Type u_7)), ((↑i : 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 : ℝ)

Tactic:
rw [Seminorm.coe_sSup_eq hp, iSup_apply]

Premises used: Seminorm.coe_sSup_eq, iSup_apply
-- Module: Mathlib.Analysis.Seminorm
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)
rw₁ 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 : ℝ)

Tactic:
rw [Seminorm.coe_iSup_eq hp, iSup_apply]

Premises used: Seminorm.coe_iSup_eq, iSup_apply
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
h : ∀ (x : E), Eq (α := ℝ) ((sSup ∅ : (a : E) → ℝ) x : ℝ) ((⊥ : (a : E) → ℝ) x : ℝ)
⊢ Eq.{u_7 + 1} (α := Seminorm 𝕜 E) (sSup ∅) ⊥

Tactic:
ext
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
x : E
h : Eq (α := ℝ) (0 : ℝ) ((⊥ : (a : E) → ℝ) x : ℝ)
⊢ Eq (α := ℝ) ((sSup ∅ : (a : E) → ℝ) x : ℝ) ((⊥ : (a : E) → ℝ) x : ℝ)

Tactic:
rw [Seminorm.sSup_apply bddAbove_empty, Real.iSup_of_isEmpty]

Premises used: Real.iSup_of_isEmpty, bddAbove_empty, Seminorm.sSup_apply
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
x : E
⊢ Eq (α := ℝ) (0 : ℝ) ((⊥ : (a : E) → ℝ) x : ℝ)

Tactic:
rfl
-- Module: Mathlib.Analysis.Seminorm
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)

Tactic:
⟨fun p hp x => ?_, fun p hp x => ?_⟩

Premises used: IsLeast, And.intro, IsLUB
-- Module: Mathlib.Analysis.Seminorm
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)
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)
⊢ IsLUB s (sSup s)

Tactic:
refine ⟨fun p hp x => ?_, fun p hp x => ?_⟩
-- Module: Mathlib.Analysis.Seminorm
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
⊢ Nonempty.{u_7 + 1} (↑s : Type u_7)

Tactic:
haveI : Nonempty ↑s := hs₂.coe_sort
-- Module: Mathlib.Analysis.Seminorm
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
⊢ Nonempty.{u_7 + 1} (↑s : Type u_7)

Tactic:
haveI : Nonempty ↑s := hs₂.coe_sort
-- Module: Mathlib.Analysis.Seminorm
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)
refine_1 : LE.le (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) (⨆ (i : (↑s : Type u_7)), ((↑i : Seminorm 𝕜 E) : (a : E) → ℝ) x : ℝ)
⊢ LE.le (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ((sSup s : (a : E) → ℝ) x : ℝ)

Tactic:
rw [Seminorm.coe_sSup_eq hs₁, iSup_apply]

Premises used: Seminorm.coe_sSup_eq, iSup_apply
-- Module: Mathlib.Analysis.Seminorm
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)
refine_2 : LE.le (α := ℝ) (⨆ (i : (↑s : Type u_7)), ((↑i : Seminorm 𝕜 E) : (a : E) → ℝ) x : ℝ) ((p : (a : E) → ℝ) x : ℝ)
⊢ LE.le (α := ℝ) ((sSup s : (a : E) → ℝ) x : ℝ) ((p : (a : E) → ℝ) x : ℝ)

Tactic:
rw [Seminorm.coe_sSup_eq hs₁, iSup_apply]

Premises used: Seminorm.coe_sSup_eq, iSup_apply
-- Module: Mathlib.Analysis.Seminorm
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)
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 : ℝ)
⊢ LE.le (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) (⨆ (i : (↑s : Type u_7)), ((↑i : Seminorm 𝕜 E) : (a : E) → ℝ) x : ℝ)

Tactic:
rcases hs₁ with ⟨q, hq⟩
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set (Seminorm 𝕜 E)
hs₂ : s.Nonempty
p : Seminorm 𝕜 E
hp : p ∈ s
x : E
this : Nonempty.{u_7 + 1} (↑s : Type u_7)
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:
le_ciSup ⟨q x, forall_mem_range.mpr fun i : s => hq i.2 x⟩ ⟨p, hp⟩

Premises used: Iff.mpr, Set.forall_mem_range, Subtype.mk, le_ciSup, Exists.intro, DFunLike.coe, Subtype.property
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set (Seminorm 𝕜 E)
hs₂ : s.Nonempty
p : Seminorm 𝕜 E
hp : p ∈ s
x : E
this : Nonempty.{u_7 + 1} (↑s : Type u_7)
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:
exact le_ciSup ⟨q x, forall_mem_range.mpr fun i : s => hq i.2 x⟩ ⟨p, hp⟩

Premises used: Iff.mpr, Set.forall_mem_range, Subtype.mk, le_ciSup, Exists.intro, DFunLike.coe, Subtype.property
-- Module: Mathlib.Analysis.Seminorm
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 (α := ℝ) (⨆ (i : (↑s : Type u_7)), ((↑i : Seminorm 𝕜 E) : (a : E) → ℝ) x : ℝ) ((p : (a : E) → ℝ) x : ℝ)

Tactic:
ciSup_le fun q => hp q.2 x

Premises used: ciSup_le, Subtype.property
-- Module: Mathlib.Analysis.Seminorm
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 (α := ℝ) (⨆ (i : (↑s : Type u_7)), ((↑i : Seminorm 𝕜 E) : (a : E) → ℝ) x : ℝ) ((p : (a : E) → ℝ) x : ℝ)

Tactic:
exact ciSup_le fun q => hp q.2 x

Premises used: ciSup_le
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : SMul 𝕜 E
p : Seminorm 𝕜 E
x y : E
r : ℝ
⊢ y ∈ p.ball x r ↔ (p : (a : E) → ℝ) (y - x) < r

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, Seminorm.ball
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : SMul 𝕜 E
p : Seminorm 𝕜 E
x y : E
r : ℝ
⊢ y ∈ p.closedBall x r ↔ (p : (a : E) → ℝ) (y - x) ≤ r

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, Seminorm.closedBall
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : SMul 𝕜 E
p : Seminorm 𝕜 E
x : E
r : ℝ
hr : 0 < r
⊢ x ∈ p.ball x r

Tactic:
simp [hr]
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : SMul 𝕜 E
p : Seminorm 𝕜 E
x : E
r : ℝ
hr : 0 ≤ r
⊢ x ∈ p.closedBall x r

Tactic:
simp [hr]
-- Module: Mathlib.Analysis.Seminorm
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
rw₁ rw₂ : (p : (a : E) → ℝ) y < r ↔ (p : (a : E) → ℝ) y < r
⊢ y ∈ p.ball 0 r ↔ (p : (a : E) → ℝ) y < r

Tactic:
rw [mem_ball, sub_zero]

Premises used: sub_zero, Seminorm.mem_ball
-- Module: Mathlib.Analysis.Seminorm
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
rw₁ rw₂ : (p : (a : E) → ℝ) y ≤ r ↔ (p : (a : E) → ℝ) y ≤ r
⊢ y ∈ p.closedBall 0 r ↔ (p : (a : E) → ℝ) y ≤ r

Tactic:
rw [mem_closedBall, sub_zero]

Premises used: sub_zero, Seminorm.mem_closedBall
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : SMul 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
⊢ p.ball 0 r = {y : E | (p : (a : E) → ℝ) y < r}

Tactic:
Set.ext fun _ => p.mem_ball_zero

Premises used: Seminorm.mem_ball_zero, Set.ext
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : SMul 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
⊢ p.closedBall 0 r = {y : E | (p : (a : E) → ℝ) y ≤ r}

Tactic:
Set.ext fun _ => p.mem_closedBall_zero

Premises used: Set.ext, Seminorm.mem_closedBall_zero
-- Module: Mathlib.Analysis.Seminorm
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.ball x r ⊆ p.closedBall x r

Tactic:
fun _ h =>
  (mem_closedBall _).mpr ((mem_ball _).mp h).le

Premises used: Iff.mpr, LT.lt.le, Set.Subset, Seminorm.mem_ball, Iff.mp, Seminorm.mem_closedBall
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : SMul 𝕜 E
p : Seminorm 𝕜 E
x : E
r : ℝ
h : ∀ (y : E), y ∈ p.closedBall x r ↔ Membership.mem (γ := Set E) (⋂ (ρ : ℝ), ⋂ (_ : ρ > r), p.ball x ρ) y
⊢ p.closedBall x r = ⋂ (ρ : ℝ), ⋂ (_ : ρ > r), p.ball x ρ

Tactic:
ext y