case intro.intro
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.2242
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s✝ t : Set E
x : E
s : Set E
a : 𝕜
ha : ‖a‖ ≤ 1
y : E
hy : y ∈ balancedCore 𝕜 s
⊢ (fun x => a • x) y ∈ balancedCore 𝕜 s
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.2242
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s✝ t : Set E
x : E
s : Set E
a : 𝕜
ha : ‖a‖ ≤ 1
⊢ a • balancedCore 𝕜 s ⊆ balancedCore 𝕜 s
rintro x ⟨y, hy, rfl⟩
case intro.intro
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.2242
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s✝ t : Set E
x : E
s : Set E
a : 𝕜
ha : ‖a‖ ≤ 1
y : E
hy : ∃ t, Balanced 𝕜 t ∧ t ⊆ s ∧ y ∈ t
⊢ (fun x => a • x) y ∈ balancedCore 𝕜 s
case intro.intro
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.2242
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s✝ t : Set E
x : E
s : Set E
a : 𝕜
ha : ‖a‖ ≤ 1
y : E
hy : y ∈ balancedCore 𝕜 s
⊢ (fun x => a • x) y ∈ balancedCore 𝕜 s
rw [mem_balancedCore_iff] at hy
case intro.intro.intro.intro.intro
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.2242
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s✝ t✝ : Set E
x : E
s : Set E
a : 𝕜
ha : ‖a‖ ≤ 1
y : E
t : Set E
ht1 : Balanced 𝕜 t
ht2 : t ⊆ s
hy : y ∈ t
⊢ (fun x => a • x) y ∈ balancedCore 𝕜 s
case intro.intro
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.2242
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s✝ t : Set E
x : E
s : Set E
a : 𝕜
ha : ‖a‖ ≤ 1
y : E
hy : ∃ t, Balanced 𝕜 t ∧ t ⊆ s ∧ y ∈ t
⊢ (fun x => a • x) y ∈ balancedCore 𝕜 s
rcases hy with ⟨t, ht1, ht2, hy⟩
no goals
case intro.intro.intro.intro.intro
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.2242
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s✝ t✝ : Set E
x : E
s : Set E
a : 𝕜
ha : ‖a‖ ≤ 1
y : E
t : Set E
ht1 : Balanced 𝕜 t
ht2 : t ⊆ s
hy : y ∈ t
⊢ (fun x => a • x) y ∈ balancedCore 𝕜 s
exact ⟨t, ⟨ht1, ht2⟩, ht1 a ha (smul_mem_smul_set hy)⟩