[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s t u v A B : Set E
hu : Absorbs 𝕜 s u
hv : Absorbs 𝕜 s v
⊢ Absorbs 𝕜 s (u ∪ v)
[PROOFSTEP]
obtain ⟨a, ha, hu⟩ := hu
[GOAL]
case intro.intro
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s t u v A B : Set E
hv : Absorbs 𝕜 s v
a : ℝ
ha : 0 < a
hu : ∀ (a_1 : 𝕜), a ≤ ‖a_1‖ → u ⊆ a_1 • s
⊢ Absorbs 𝕜 s (u ∪ v)
[PROOFSTEP]
obtain ⟨b, _hb, hv⟩ := hv
[GOAL]
case intro.intro.intro.intro
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s t u v A B : Set E
a : ℝ
ha : 0 < a
hu : ∀ (a_1 : 𝕜), a ≤ ‖a_1‖ → u ⊆ a_1 • s
b : ℝ
_hb : 0 < b
hv : ∀ (a : 𝕜), b ≤ ‖a‖ → v ⊆ a • s
⊢ Absorbs 𝕜 s (u ∪ v)
[PROOFSTEP]
exact
  ⟨max a b, lt_max_of_lt_left ha, fun c hc =>
    union_subset (hu _ <| le_of_max_le_left hc) (hv _ <| le_of_max_le_right hc)⟩
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι✝ : Sort u_4
κ : ι✝ → Sort u_5
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s t✝ u v A B : Set E
ι : Type u_6
t : Finset ι
f : ι → Set E
⊢ Absorbs 𝕜 s (⋃ (i : ι) (_ : i ∈ t), f i) ↔ ∀ (i : ι), i ∈ t → Absorbs 𝕜 s (f i)
[PROOFSTEP]
classical
induction' t using Finset.induction_on with i t _ht hi
· simp only [Finset.not_mem_empty, Set.iUnion_false, Set.iUnion_empty, absorbs_empty, IsEmpty.forall_iff, imp_true_iff]
rw [Finset.set_biUnion_insert, absorbs_union, hi]
constructor <;> intro h
· refine' fun _ hi' => (Finset.mem_insert.mp hi').elim _ (h.2 _)
  exact fun hi'' => by
    rw [hi'']
    exact h.1
exact ⟨h i (Finset.mem_insert_self i t), fun i' hi' => h i' (Finset.mem_insert_of_mem hi')⟩
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι✝ : Sort u_4
κ : ι✝ → Sort u_5
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s t✝ u v A B : Set E
ι : Type u_6
t : Finset ι
f : ι → Set E
⊢ Absorbs 𝕜 s (⋃ (i : ι) (_ : i ∈ t), f i) ↔ ∀ (i : ι), i ∈ t → Absorbs 𝕜 s (f i)
[PROOFSTEP]
induction' t using Finset.induction_on with i t _ht hi
[GOAL]
case empty
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι✝ : Sort u_4
κ : ι✝ → Sort u_5
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s t u v A B : Set E
ι : Type u_6
f : ι → Set E
⊢ Absorbs 𝕜 s (⋃ (i : ι) (_ : i ∈ ∅), f i) ↔ ∀ (i : ι), i ∈ ∅ → Absorbs 𝕜 s (f i)
[PROOFSTEP]
simp only [Finset.not_mem_empty, Set.iUnion_false, Set.iUnion_empty, absorbs_empty, IsEmpty.forall_iff, imp_true_iff]
[GOAL]
case insert
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι✝ : Sort u_4
κ : ι✝ → Sort u_5
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s t✝ u v A B : Set E
ι : Type u_6
f : ι → Set E
i : ι
t : Finset ι
_ht : ¬i ∈ t
hi : Absorbs 𝕜 s (⋃ (i : ι) (_ : i ∈ t), f i) ↔ ∀ (i : ι), i ∈ t → Absorbs 𝕜 s (f i)
⊢ Absorbs 𝕜 s (⋃ (i_1 : ι) (_ : i_1 ∈ insert i t), f i_1) ↔ ∀ (i_1 : ι), i_1 ∈ insert i t → Absorbs 𝕜 s (f i_1)
[PROOFSTEP]
rw [Finset.set_biUnion_insert, absorbs_union, hi]
[GOAL]
case insert
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι✝ : Sort u_4
κ : ι✝ → Sort u_5
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s t✝ u v A B : Set E
ι : Type u_6
f : ι → Set E
i : ι
t : Finset ι
_ht : ¬i ∈ t
hi : Absorbs 𝕜 s (⋃ (i : ι) (_ : i ∈ t), f i) ↔ ∀ (i : ι), i ∈ t → Absorbs 𝕜 s (f i)
⊢ (Absorbs 𝕜 s (f i) ∧ ∀ (i : ι), i ∈ t → Absorbs 𝕜 s (f i)) ↔ ∀ (i_1 : ι), i_1 ∈ insert i t → Absorbs 𝕜 s (f i_1)
[PROOFSTEP]
constructor
[GOAL]
case insert.mp
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι✝ : Sort u_4
κ : ι✝ → Sort u_5
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s t✝ u v A B : Set E
ι : Type u_6
f : ι → Set E
i : ι
t : Finset ι
_ht : ¬i ∈ t
hi : Absorbs 𝕜 s (⋃ (i : ι) (_ : i ∈ t), f i) ↔ ∀ (i : ι), i ∈ t → Absorbs 𝕜 s (f i)
⊢ (Absorbs 𝕜 s (f i) ∧ ∀ (i : ι), i ∈ t → Absorbs 𝕜 s (f i)) → ∀ (i_1 : ι), i_1 ∈ insert i t → Absorbs 𝕜 s (f i_1)
[PROOFSTEP]
intro h
[GOAL]
case insert.mpr
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι✝ : Sort u_4
κ : ι✝ → Sort u_5
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s t✝ u v A B : Set E
ι : Type u_6
f : ι → Set E
i : ι
t : Finset ι
_ht : ¬i ∈ t
hi : Absorbs 𝕜 s (⋃ (i : ι) (_ : i ∈ t), f i) ↔ ∀ (i : ι), i ∈ t → Absorbs 𝕜 s (f i)
⊢ (∀ (i_1 : ι), i_1 ∈ insert i t → Absorbs 𝕜 s (f i_1)) → Absorbs 𝕜 s (f i) ∧ ∀ (i : ι), i ∈ t → Absorbs 𝕜 s (f i)
[PROOFSTEP]
intro h
[GOAL]
case insert.mp
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι✝ : Sort u_4
κ : ι✝ → Sort u_5
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s t✝ u v A B : Set E
ι : Type u_6
f : ι → Set E
i : ι
t : Finset ι
_ht : ¬i ∈ t
hi : Absorbs 𝕜 s (⋃ (i : ι) (_ : i ∈ t), f i) ↔ ∀ (i : ι), i ∈ t → Absorbs 𝕜 s (f i)
h : Absorbs 𝕜 s (f i) ∧ ∀ (i : ι), i ∈ t → Absorbs 𝕜 s (f i)
⊢ ∀ (i_1 : ι), i_1 ∈ insert i t → Absorbs 𝕜 s (f i_1)
[PROOFSTEP]
refine' fun _ hi' => (Finset.mem_insert.mp hi').elim _ (h.2 _)
[GOAL]
case insert.mp
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι✝ : Sort u_4
κ : ι✝ → Sort u_5
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s t✝ u v A B : Set E
ι : Type u_6
f : ι → Set E
i : ι
t : Finset ι
_ht : ¬i ∈ t
hi : Absorbs 𝕜 s (⋃ (i : ι) (_ : i ∈ t), f i) ↔ ∀ (i : ι), i ∈ t → Absorbs 𝕜 s (f i)
h : Absorbs 𝕜 s (f i) ∧ ∀ (i : ι), i ∈ t → Absorbs 𝕜 s (f i)
x✝ : ι
hi' : x✝ ∈ insert i t
⊢ x✝ = i → Absorbs 𝕜 s (f x✝)
[PROOFSTEP]
exact fun hi'' => by
  rw [hi'']
  exact h.1
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι✝ : Sort u_4
κ : ι✝ → Sort u_5
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s t✝ u v A B : Set E
ι : Type u_6
f : ι → Set E
i : ι
t : Finset ι
_ht : ¬i ∈ t
hi : Absorbs 𝕜 s (⋃ (i : ι) (_ : i ∈ t), f i) ↔ ∀ (i : ι), i ∈ t → Absorbs 𝕜 s (f i)
h : Absorbs 𝕜 s (f i) ∧ ∀ (i : ι), i ∈ t → Absorbs 𝕜 s (f i)
x✝ : ι
hi' : x✝ ∈ insert i t
hi'' : x✝ = i
⊢ Absorbs 𝕜 s (f x✝)
[PROOFSTEP]
rw [hi'']
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι✝ : Sort u_4
κ : ι✝ → Sort u_5
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s t✝ u v A B : Set E
ι : Type u_6
f : ι → Set E
i : ι
t : Finset ι
_ht : ¬i ∈ t
hi : Absorbs 𝕜 s (⋃ (i : ι) (_ : i ∈ t), f i) ↔ ∀ (i : ι), i ∈ t → Absorbs 𝕜 s (f i)
h : Absorbs 𝕜 s (f i) ∧ ∀ (i : ι), i ∈ t → Absorbs 𝕜 s (f i)
x✝ : ι
hi' : x✝ ∈ insert i t
hi'' : x✝ = i
⊢ Absorbs 𝕜 s (f i)
[PROOFSTEP]
exact h.1
[GOAL]
case insert.mpr
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι✝ : Sort u_4
κ : ι✝ → Sort u_5
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s t✝ u v A B : Set E
ι : Type u_6
f : ι → Set E
i : ι
t : Finset ι
_ht : ¬i ∈ t
hi : Absorbs 𝕜 s (⋃ (i : ι) (_ : i ∈ t), f i) ↔ ∀ (i : ι), i ∈ t → Absorbs 𝕜 s (f i)
h : ∀ (i_1 : ι), i_1 ∈ insert i t → Absorbs 𝕜 s (f i_1)
⊢ Absorbs 𝕜 s (f i) ∧ ∀ (i : ι), i ∈ t → Absorbs 𝕜 s (f i)
[PROOFSTEP]
exact ⟨h i (Finset.mem_insert_self i t), fun i' hi' => h i' (Finset.mem_insert_of_mem hi')⟩
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι✝ : Sort u_4
κ : ι✝ → Sort u_5
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s✝ t✝ u v A B : Set E
ι : Type u_6
s : Set E
t : Set ι
f : ι → Set E
hi : Set.Finite t
⊢ Absorbs 𝕜 s (⋃ (i : ι) (_ : i ∈ t), f i) ↔ ∀ (i : ι), i ∈ t → Absorbs 𝕜 s (f i)
[PROOFSTEP]
lift t to Finset ι using hi
[GOAL]
case intro
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι✝ : Sort u_4
κ : ι✝ → Sort u_5
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s✝ t✝ u v A B : Set E
ι : Type u_6
s : Set E
f : ι → Set E
t : Finset ι
⊢ Absorbs 𝕜 s (⋃ (i : ι) (_ : i ∈ ↑t), f i) ↔ ∀ (i : ι), i ∈ ↑t → Absorbs 𝕜 s (f i)
[PROOFSTEP]
simp only [Finset.mem_coe]
[GOAL]
case intro
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι✝ : Sort u_4
κ : ι✝ → Sort u_5
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s✝ t✝ u v A B : Set E
ι : Type u_6
s : Set E
f : ι → Set E
t : Finset ι
⊢ Absorbs 𝕜 s (⋃ (i : ι) (_ : i ∈ t), f i) ↔ ∀ (i : ι), i ∈ t → Absorbs 𝕜 s (f i)
[PROOFSTEP]
exact absorbs_iUnion_finset
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s t u v A B : Set E
hA : Absorbent 𝕜 A
hAB : A ⊆ B
⊢ Absorbent 𝕜 B
[PROOFSTEP]
refine' forall_imp (fun x => _) hA
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s t u v A B : Set E
hA : Absorbent 𝕜 A
hAB : A ⊆ B
x : E
⊢ (∃ r, 0 < r ∧ ∀ (a : 𝕜), r ≤ ‖a‖ → x ∈ a • A) → ∃ r, 0 < r ∧ ∀ (a : 𝕜), r ≤ ‖a‖ → x ∈ a • B
[PROOFSTEP]
exact Exists.imp fun r => And.imp_right <| forall₂_imp fun a _ha hx => Set.smul_set_mono hAB hx
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s t u v A B : Set E
⊢ Absorbent 𝕜 A ↔ ∀ (x : E), Absorbs 𝕜 A {x}
[PROOFSTEP]
simp_rw [Absorbs, Absorbent, singleton_subset_iff]
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s✝ t u v✝ A B s : Set E
hs : Absorbent 𝕜 s
v : Set E
hv : Set.Finite v
⊢ Absorbs 𝕜 s v
[PROOFSTEP]
rw [← Set.biUnion_of_singleton v]
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s✝ t u v✝ A B s : Set E
hs : Absorbent 𝕜 s
v : Set E
hv : Set.Finite v
⊢ Absorbs 𝕜 s (⋃ (x : E) (_ : x ∈ v), {x})
[PROOFSTEP]
exact hv.absorbs_iUnion.mpr fun _ _ => hs.absorbs
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s t u v A B : Set E
x✝¹ : 𝕜
x✝ : ‖x✝¹‖ ≤ 1
⊢ x✝¹ • ∅ ⊆ ∅
[PROOFSTEP]
rw [smul_set_empty]
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s s₁ s₂ t t₁ t₂ : Set E
h₁ : Absorbs 𝕜 s₁ t₁
h₂ : Absorbs 𝕜 s₂ t₂
⊢ Absorbs 𝕜 (s₁ - s₂) (t₁ - t₂)
[PROOFSTEP]
simp_rw [sub_eq_add_neg]
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s s₁ s₂ t t₁ t₂ : Set E
h₁ : Absorbs 𝕜 s₁ t₁
h₂ : Absorbs 𝕜 s₂ t₂
⊢ Absorbs 𝕜 (s₁ + -s₂) (t₁ + -t₂)
[PROOFSTEP]
exact h₁.add h₂.neg
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s s₁ s₂ t t₁ t₂ : Set E
hs : Balanced 𝕜 s
ht : Balanced 𝕜 t
⊢ Balanced 𝕜 (s - t)
[PROOFSTEP]
simp_rw [sub_eq_add_neg]
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s s₁ s₂ t t₁ t₂ : Set E
hs : Balanced 𝕜 s
ht : Balanced 𝕜 t
⊢ Balanced 𝕜 (s + -t)
[PROOFSTEP]
exact hs.add ht.neg
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a✝ b✝ : 𝕜
hs : Balanced 𝕝 s
a : 𝕝
b : 𝕜
h : ‖a‖ ≤ ‖b‖
⊢ a • s ⊆ b • s
[PROOFSTEP]
obtain rfl | hb := eq_or_ne b 0
[GOAL]
case inl
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a✝ b : 𝕜
hs : Balanced 𝕝 s
a : 𝕝
h : ‖a‖ ≤ ‖0‖
⊢ a • s ⊆ 0 • s
[PROOFSTEP]
rw [norm_zero] at h
[GOAL]
case inl
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a✝ b : 𝕜
hs : Balanced 𝕝 s
a : 𝕝
h : ‖a‖ ≤ 0
⊢ a • s ⊆ 0 • s
[PROOFSTEP]
rw [norm_eq_zero.1 (h.antisymm <| norm_nonneg _)]
[GOAL]
case inl
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a✝ b : 𝕜
hs : Balanced 𝕝 s
a : 𝕝
h : ‖a‖ ≤ 0
⊢ 0 • s ⊆ 0 • s
[PROOFSTEP]
obtain rfl | h := s.eq_empty_or_nonempty
[GOAL]
case inl.inl
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
t u v A B : Set E
x : E
a✝ b : 𝕜
a : 𝕝
h : ‖a‖ ≤ 0
hs : Balanced 𝕝 ∅
⊢ 0 • ∅ ⊆ 0 • ∅
[PROOFSTEP]
simp_rw [smul_set_empty]
[GOAL]
case inl.inl
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
t u v A B : Set E
x : E
a✝ b : 𝕜
a : 𝕝
h : ‖a‖ ≤ 0
hs : Balanced 𝕝 ∅
⊢ ∅ ⊆ ∅
[PROOFSTEP]
rfl
[GOAL]
case inl.inr
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a✝ b : 𝕜
hs : Balanced 𝕝 s
a : 𝕝
h✝ : ‖a‖ ≤ 0
h : Set.Nonempty s
⊢ 0 • s ⊆ 0 • s
[PROOFSTEP]
simp_rw [zero_smul_set h]
[GOAL]
case inl.inr
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a✝ b : 𝕜
hs : Balanced 𝕝 s
a : 𝕝
h✝ : ‖a‖ ≤ 0
h : Set.Nonempty s
⊢ 0 ⊆ 0
[PROOFSTEP]
rfl
[GOAL]
case inr
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a✝ b✝ : 𝕜
hs : Balanced 𝕝 s
a : 𝕝
b : 𝕜
h : ‖a‖ ≤ ‖b‖
hb : b ≠ 0
⊢ a • s ⊆ b • s
[PROOFSTEP]
rintro _ ⟨x, hx, rfl⟩
[GOAL]
case inr.intro.intro
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x✝ : E
a✝ b✝ : 𝕜
hs : Balanced 𝕝 s
a : 𝕝
b : 𝕜
h : ‖a‖ ≤ ‖b‖
hb : b ≠ 0
x : E
hx : x ∈ s
⊢ (fun x => a • x) x ∈ b • s
[PROOFSTEP]
refine' ⟨b⁻¹ • a • x, _, smul_inv_smul₀ hb _⟩
[GOAL]
case inr.intro.intro
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x✝ : E
a✝ b✝ : 𝕜
hs : Balanced 𝕝 s
a : 𝕝
b : 𝕜
h : ‖a‖ ≤ ‖b‖
hb : b ≠ 0
x : E
hx : x ∈ s
⊢ b⁻¹ • a • x ∈ s
[PROOFSTEP]
rw [← smul_assoc]
[GOAL]
case inr.intro.intro
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x✝ : E
a✝ b✝ : 𝕜
hs : Balanced 𝕝 s
a : 𝕝
b : 𝕜
h : ‖a‖ ≤ ‖b‖
hb : b ≠ 0
x : E
hx : x ∈ s
⊢ (b⁻¹ • a) • x ∈ s
[PROOFSTEP]
refine' hs _ _ (smul_mem_smul_set hx)
[GOAL]
case inr.intro.intro
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x✝ : E
a✝ b✝ : 𝕜
hs : Balanced 𝕝 s
a : 𝕝
b : 𝕜
h : ‖a‖ ≤ ‖b‖
hb : b ≠ 0
x : E
hx : x ∈ s
⊢ ‖b⁻¹ • a‖ ≤ 1
[PROOFSTEP]
rw [norm_smul, norm_inv, ← div_eq_inv_mul]
[GOAL]
case inr.intro.intro
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x✝ : E
a✝ b✝ : 𝕜
hs : Balanced 𝕝 s
a : 𝕝
b : 𝕜
h : ‖a‖ ≤ ‖b‖
hb : b ≠ 0
x : E
hx : x ∈ s
⊢ ‖a‖ / ‖b‖ ≤ 1
[PROOFSTEP]
exact div_le_one_of_le h (norm_nonneg _)
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a b : 𝕜
hA : Balanced 𝕜 A
⊢ Absorbs 𝕜 A A
[PROOFSTEP]
refine' ⟨1, zero_lt_one, fun a ha x hx => _⟩
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x✝ : E
a✝ b : 𝕜
hA : Balanced 𝕜 A
a : 𝕜
ha : 1 ≤ ‖a‖
x : E
hx : x ∈ A
⊢ x ∈ a • A
[PROOFSTEP]
rw [mem_smul_set_iff_inv_smul_mem₀ (norm_pos_iff.1 <| zero_lt_one.trans_le ha)]
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x✝ : E
a✝ b : 𝕜
hA : Balanced 𝕜 A
a : 𝕜
ha : 1 ≤ ‖a‖
x : E
hx : x ∈ A
⊢ a⁻¹ • x ∈ A
[PROOFSTEP]
refine' hA a⁻¹ _ (smul_mem_smul_set hx)
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x✝ : E
a✝ b : 𝕜
hA : Balanced 𝕜 A
a : 𝕜
ha : 1 ≤ ‖a‖
x : E
hx : x ∈ A
⊢ ‖a⁻¹‖ ≤ 1
[PROOFSTEP]
rw [norm_inv]
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x✝ : E
a✝ b : 𝕜
hA : Balanced 𝕜 A
a : 𝕜
ha : 1 ≤ ‖a‖
x : E
hx : x ∈ A
⊢ ‖a‖⁻¹ ≤ 1
[PROOFSTEP]
exact inv_le_one ha
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a b : 𝕜
hA : Balanced 𝕜 A
ha : 1 ≤ ‖a‖
⊢ A ⊆ a • A
[PROOFSTEP]
refine' (subset_set_smul_iff₀ _).2 (hA a⁻¹ _)
[GOAL]
case refine'_1
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a b : 𝕜
hA : Balanced 𝕜 A
ha : 1 ≤ ‖a‖
⊢ a ≠ 0
[PROOFSTEP]
rintro rfl
[GOAL]
case refine'_1
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
b : 𝕜
hA : Balanced 𝕜 A
ha : 1 ≤ ‖0‖
⊢ False
[PROOFSTEP]
rw [norm_zero] at ha
[GOAL]
case refine'_1
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
b : 𝕜
hA : Balanced 𝕜 A
ha : 1 ≤ 0
⊢ False
[PROOFSTEP]
exact zero_lt_one.not_le ha
[GOAL]
case refine'_2
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a b : 𝕜
hA : Balanced 𝕜 A
ha : 1 ≤ ‖a‖
⊢ ‖a⁻¹‖ ≤ 1
[PROOFSTEP]
rw [norm_inv]
[GOAL]
case refine'_2
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a b : 𝕜
hA : Balanced 𝕜 A
ha : 1 ≤ ‖a‖
⊢ ‖a‖⁻¹ ≤ 1
[PROOFSTEP]
exact inv_le_one ha
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a b : 𝕜
hs : Balanced 𝕜 s
h : ‖a‖ = ‖b‖
⊢ a • x ∈ s ↔ b • x ∈ s
[PROOFSTEP]
obtain rfl | hb := eq_or_ne b 0
[GOAL]
case inl
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a : 𝕜
hs : Balanced 𝕜 s
h : ‖a‖ = ‖0‖
⊢ a • x ∈ s ↔ 0 • x ∈ s
[PROOFSTEP]
rw [norm_zero, norm_eq_zero] at h
[GOAL]
case inl
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a : 𝕜
hs : Balanced 𝕜 s
h : a = 0
⊢ a • x ∈ s ↔ 0 • x ∈ s
[PROOFSTEP]
rw [h]
[GOAL]
case inr
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a b : 𝕜
hs : Balanced 𝕜 s
h : ‖a‖ = ‖b‖
hb : b ≠ 0
⊢ a • x ∈ s ↔ b • x ∈ s
[PROOFSTEP]
have ha : a ≠ 0 := norm_ne_zero_iff.1 (ne_of_eq_of_ne h <| norm_ne_zero_iff.2 hb)
[GOAL]
case inr
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a b : 𝕜
hs : Balanced 𝕜 s
h : ‖a‖ = ‖b‖
hb : b ≠ 0
ha : a ≠ 0
⊢ a • x ∈ s ↔ b • x ∈ s
[PROOFSTEP]
constructor <;> intro h' <;> [rw [← inv_mul_cancel_right₀ ha b]; rw [← inv_mul_cancel_right₀ hb a]]
[GOAL]
case inr
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a b : 𝕜
hs : Balanced 𝕜 s
h : ‖a‖ = ‖b‖
hb : b ≠ 0
ha : a ≠ 0
⊢ a • x ∈ s ↔ b • x ∈ s
[PROOFSTEP]
constructor
[GOAL]
case inr.mp
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a b : 𝕜
hs : Balanced 𝕜 s
h : ‖a‖ = ‖b‖
hb : b ≠ 0
ha : a ≠ 0
⊢ a • x ∈ s → b • x ∈ s
[PROOFSTEP]
intro h'
[GOAL]
case inr.mpr
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a b : 𝕜
hs : Balanced 𝕜 s
h : ‖a‖ = ‖b‖
hb : b ≠ 0
ha : a ≠ 0
⊢ b • x ∈ s → a • x ∈ s
[PROOFSTEP]
intro h'
[GOAL]
case inr.mp
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a b : 𝕜
hs : Balanced 𝕜 s
h : ‖a‖ = ‖b‖
hb : b ≠ 0
ha : a ≠ 0
h' : a • x ∈ s
⊢ b • x ∈ s
[PROOFSTEP]
rw [← inv_mul_cancel_right₀ ha b]
[GOAL]
case inr.mpr
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a b : 𝕜
hs : Balanced 𝕜 s
h : ‖a‖ = ‖b‖
hb : b ≠ 0
ha : a ≠ 0
h' : b • x ∈ s
⊢ a • x ∈ s
[PROOFSTEP]
rw [← inv_mul_cancel_right₀ hb a]
[GOAL]
case inr.mp
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a b : 𝕜
hs : Balanced 𝕜 s
h : ‖a‖ = ‖b‖
hb : b ≠ 0
ha : a ≠ 0
h' : a • x ∈ s
⊢ (b * a⁻¹ * a) • x ∈ s
[PROOFSTEP]
rw [← smul_eq_mul, smul_assoc]
[GOAL]
case inr.mp
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a b : 𝕜
hs : Balanced 𝕜 s
h : ‖a‖ = ‖b‖
hb : b ≠ 0
ha : a ≠ 0
h' : a • x ∈ s
⊢ (b * a⁻¹) • a • x ∈ s
[PROOFSTEP]
refine' hs.smul_mem _ h'
[GOAL]
case inr.mp
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a b : 𝕜
hs : Balanced 𝕜 s
h : ‖a‖ = ‖b‖
hb : b ≠ 0
ha : a ≠ 0
h' : a • x ∈ s
⊢ ‖b * a⁻¹‖ ≤ 1
[PROOFSTEP]
simp [← h, ha]
[GOAL]
case inr.mpr
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a b : 𝕜
hs : Balanced 𝕜 s
h : ‖a‖ = ‖b‖
hb : b ≠ 0
ha : a ≠ 0
h' : b • x ∈ s
⊢ (a * b⁻¹ * b) • x ∈ s
[PROOFSTEP]
rw [← smul_eq_mul, smul_assoc]
[GOAL]
case inr.mpr
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a b : 𝕜
hs : Balanced 𝕜 s
h : ‖a‖ = ‖b‖
hb : b ≠ 0
ha : a ≠ 0
h' : b • x ∈ s
⊢ (a * b⁻¹) • b • x ∈ s
[PROOFSTEP]
refine' hs.smul_mem _ h'
[GOAL]
case inr.mpr
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a b : 𝕜
hs : Balanced 𝕜 s
h : ‖a‖ = ‖b‖
hb : b ≠ 0
ha : a ≠ 0
h' : b • x ∈ s
⊢ ‖a * b⁻¹‖ ≤ 1
[PROOFSTEP]
simp [← h, ha]
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a b : 𝕜
hs : Balanced 𝕜 s
⊢ -x ∈ s ↔ x ∈ s
[PROOFSTEP]
convert hs.mem_smul_iff (x := x) (norm_neg 1) using 0
[GOAL]
case a
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a b : 𝕜
hs : Balanced 𝕜 s
⊢ (-x ∈ s ↔ x ∈ s) ↔ (-1 • x ∈ s ↔ 1 • x ∈ s)
[PROOFSTEP]
simp only [neg_smul, one_smul 𝕜 x]
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a b : 𝕜
hs : Absorbs 𝕜 s u
ht : Absorbs 𝕜 t u
⊢ Absorbs 𝕜 (s ∩ t) u
[PROOFSTEP]
obtain ⟨a, ha, hs⟩ := hs
[GOAL]
case intro.intro
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a✝ b : 𝕜
ht : Absorbs 𝕜 t u
a : ℝ
ha : 0 < a
hs : ∀ (a_1 : 𝕜), a ≤ ‖a_1‖ → u ⊆ a_1 • s
⊢ Absorbs 𝕜 (s ∩ t) u
[PROOFSTEP]
obtain ⟨b, _hb, ht⟩ := ht
[GOAL]
case intro.intro.intro.intro
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a✝ b✝ : 𝕜
a : ℝ
ha : 0 < a
hs : ∀ (a_1 : 𝕜), a ≤ ‖a_1‖ → u ⊆ a_1 • s
b : ℝ
_hb : 0 < b
ht : ∀ (a : 𝕜), b ≤ ‖a‖ → u ⊆ a • t
⊢ Absorbs 𝕜 (s ∩ t) u
[PROOFSTEP]
have h : 0 < max a b := lt_max_of_lt_left ha
[GOAL]
case intro.intro.intro.intro
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a✝ b✝ : 𝕜
a : ℝ
ha : 0 < a
hs : ∀ (a_1 : 𝕜), a ≤ ‖a_1‖ → u ⊆ a_1 • s
b : ℝ
_hb : 0 < b
ht : ∀ (a : 𝕜), b ≤ ‖a‖ → u ⊆ a • t
h : 0 < max a b
⊢ Absorbs 𝕜 (s ∩ t) u
[PROOFSTEP]
refine' ⟨max a b, lt_max_of_lt_left ha, fun c hc => _⟩
[GOAL]
case intro.intro.intro.intro
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a✝ b✝ : 𝕜
a : ℝ
ha : 0 < a
hs : ∀ (a_1 : 𝕜), a ≤ ‖a_1‖ → u ⊆ a_1 • s
b : ℝ
_hb : 0 < b
ht : ∀ (a : 𝕜), b ≤ ‖a‖ → u ⊆ a • t
h : 0 < max a b
c : 𝕜
hc : max a b ≤ ‖c‖
⊢ u ⊆ c • (s ∩ t)
[PROOFSTEP]
rw [smul_set_inter₀ (norm_pos_iff.1 <| h.trans_le hc)]
[GOAL]
case intro.intro.intro.intro
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a✝ b✝ : 𝕜
a : ℝ
ha : 0 < a
hs : ∀ (a_1 : 𝕜), a ≤ ‖a_1‖ → u ⊆ a_1 • s
b : ℝ
_hb : 0 < b
ht : ∀ (a : 𝕜), b ≤ ‖a‖ → u ⊆ a • t
h : 0 < max a b
c : 𝕜
hc : max a b ≤ ‖c‖
⊢ u ⊆ c • s ∩ c • t
[PROOFSTEP]
exact subset_inter (hs _ <| le_of_max_le_left hc) (ht _ <| le_of_max_le_right hc)
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a b : 𝕜
⊢ Absorbent 𝕜 univ
[PROOFSTEP]
refine' fun x => ⟨1, zero_lt_one, fun a ha => _⟩
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x✝ : E
a✝ b : 𝕜
x : E
a : 𝕜
ha : 1 ≤ ‖a‖
⊢ x ∈ a • univ
[PROOFSTEP]
rw [smul_set_univ₀ (norm_pos_iff.1 <| zero_lt_one.trans_le ha)]
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x✝ : E
a✝ b : 𝕜
x : E
a : 𝕜
ha : 1 ≤ ‖a‖
⊢ x ∈ univ
[PROOFSTEP]
exact trivial
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedRing 𝕝
inst✝⁶ : NormedSpace 𝕜 𝕝
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SMulWithZero 𝕝 E
inst✝² : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a b : 𝕜
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
hA : A ∈ 𝓝 0
⊢ Absorbent 𝕜 A
[PROOFSTEP]
intro x
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedRing 𝕝
inst✝⁶ : NormedSpace 𝕜 𝕝
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SMulWithZero 𝕝 E
inst✝² : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x✝ : E
a b : 𝕜
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
hA : A ∈ 𝓝 0
x : E
⊢ ∃ r, 0 < r ∧ ∀ (a : 𝕜), r ≤ ‖a‖ → x ∈ a • A
[PROOFSTEP]
obtain ⟨w, hw₁, hw₂, hw₃⟩ := mem_nhds_iff.mp hA
[GOAL]
case intro.intro.intro
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedRing 𝕝
inst✝⁶ : NormedSpace 𝕜 𝕝
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SMulWithZero 𝕝 E
inst✝² : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x✝ : E
a b : 𝕜
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
hA : A ∈ 𝓝 0
x : E
w : Set E
hw₁ : w ⊆ A
hw₂ : IsOpen w
hw₃ : 0 ∈ w
⊢ ∃ r, 0 < r ∧ ∀ (a : 𝕜), r ≤ ‖a‖ → x ∈ a • A
[PROOFSTEP]
have hc : Continuous fun t : 𝕜 => t • x := continuous_id.smul continuous_const
[GOAL]
case intro.intro.intro
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedRing 𝕝
inst✝⁶ : NormedSpace 𝕜 𝕝
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SMulWithZero 𝕝 E
inst✝² : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x✝ : E
a b : 𝕜
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
hA : A ∈ 𝓝 0
x : E
w : Set E
hw₁ : w ⊆ A
hw₂ : IsOpen w
hw₃ : 0 ∈ w
hc : Continuous fun t => t • x
⊢ ∃ r, 0 < r ∧ ∀ (a : 𝕜), r ≤ ‖a‖ → x ∈ a • A
[PROOFSTEP]
obtain ⟨r, hr₁, hr₂⟩ := Metric.isOpen_iff.mp (hw₂.preimage hc) 0 (by rwa [mem_preimage, zero_smul])
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedRing 𝕝
inst✝⁶ : NormedSpace 𝕜 𝕝
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SMulWithZero 𝕝 E
inst✝² : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x✝ : E
a b : 𝕜
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
hA : A ∈ 𝓝 0
x : E
w : Set E
hw₁ : w ⊆ A
hw₂ : IsOpen w
hw₃ : 0 ∈ w
hc : Continuous fun t => t • x
⊢ 0 ∈ (fun t => t • x) ⁻¹' w
[PROOFSTEP]
rwa [mem_preimage, zero_smul]
[GOAL]
case intro.intro.intro.intro.intro
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedRing 𝕝
inst✝⁶ : NormedSpace 𝕜 𝕝
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SMulWithZero 𝕝 E
inst✝² : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x✝ : E
a b : 𝕜
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
hA : A ∈ 𝓝 0
x : E
w : Set E
hw₁ : w ⊆ A
hw₂ : IsOpen w
hw₃ : 0 ∈ w
hc : Continuous fun t => t • x
r : ℝ
hr₁ : r > 0
hr₂ : Metric.ball 0 r ⊆ (fun t => t • x) ⁻¹' w
⊢ ∃ r, 0 < r ∧ ∀ (a : 𝕜), r ≤ ‖a‖ → x ∈ a • A
[PROOFSTEP]
have hr₃ := inv_pos.mpr (half_pos hr₁)
[GOAL]
case intro.intro.intro.intro.intro
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedRing 𝕝
inst✝⁶ : NormedSpace 𝕜 𝕝
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SMulWithZero 𝕝 E
inst✝² : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x✝ : E
a b : 𝕜
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
hA : A ∈ 𝓝 0
x : E
w : Set E
hw₁ : w ⊆ A
hw₂ : IsOpen w
hw₃ : 0 ∈ w
hc : Continuous fun t => t • x
r : ℝ
hr₁ : r > 0
hr₂ : Metric.ball 0 r ⊆ (fun t => t • x) ⁻¹' w
hr₃ : 0 < (r / 2)⁻¹
⊢ ∃ r, 0 < r ∧ ∀ (a : 𝕜), r ≤ ‖a‖ → x ∈ a • A
[PROOFSTEP]
refine' ⟨(r / 2)⁻¹, hr₃, fun a ha₁ => _⟩
[GOAL]
case intro.intro.intro.intro.intro
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedRing 𝕝
inst✝⁶ : NormedSpace 𝕜 𝕝
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SMulWithZero 𝕝 E
inst✝² : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x✝ : E
a✝ b : 𝕜
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
hA : A ∈ 𝓝 0
x : E
w : Set E
hw₁ : w ⊆ A
hw₂ : IsOpen w
hw₃ : 0 ∈ w
hc : Continuous fun t => t • x
r : ℝ
hr₁ : r > 0
hr₂ : Metric.ball 0 r ⊆ (fun t => t • x) ⁻¹' w
hr₃ : 0 < (r / 2)⁻¹
a : 𝕜
ha₁ : (r / 2)⁻¹ ≤ ‖a‖
⊢ x ∈ a • A
[PROOFSTEP]
have ha₂ : 0 < ‖a‖ := hr₃.trans_le ha₁
[GOAL]
case intro.intro.intro.intro.intro
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedRing 𝕝
inst✝⁶ : NormedSpace 𝕜 𝕝
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SMulWithZero 𝕝 E
inst✝² : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x✝ : E
a✝ b : 𝕜
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
hA : A ∈ 𝓝 0
x : E
w : Set E
hw₁ : w ⊆ A
hw₂ : IsOpen w
hw₃ : 0 ∈ w
hc : Continuous fun t => t • x
r : ℝ
hr₁ : r > 0
hr₂ : Metric.ball 0 r ⊆ (fun t => t • x) ⁻¹' w
hr₃ : 0 < (r / 2)⁻¹
a : 𝕜
ha₁ : (r / 2)⁻¹ ≤ ‖a‖
ha₂ : 0 < ‖a‖
⊢ x ∈ a • A
[PROOFSTEP]
refine' (mem_smul_set_iff_inv_smul_mem₀ (norm_pos_iff.mp ha₂) _ _).2 (hw₁ <| hr₂ _)
[GOAL]
case intro.intro.intro.intro.intro
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedRing 𝕝
inst✝⁶ : NormedSpace 𝕜 𝕝
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SMulWithZero 𝕝 E
inst✝² : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x✝ : E
a✝ b : 𝕜
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
hA : A ∈ 𝓝 0
x : E
w : Set E
hw₁ : w ⊆ A
hw₂ : IsOpen w
hw₃ : 0 ∈ w
hc : Continuous fun t => t • x
r : ℝ
hr₁ : r > 0
hr₂ : Metric.ball 0 r ⊆ (fun t => t • x) ⁻¹' w
hr₃ : 0 < (r / 2)⁻¹
a : 𝕜
ha₁ : (r / 2)⁻¹ ≤ ‖a‖
ha₂ : 0 < ‖a‖
⊢ a⁻¹ ∈ Metric.ball 0 r
[PROOFSTEP]
rw [Metric.mem_ball, dist_zero_right, norm_inv]
[GOAL]
case intro.intro.intro.intro.intro
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedRing 𝕝
inst✝⁶ : NormedSpace 𝕜 𝕝
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SMulWithZero 𝕝 E
inst✝² : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x✝ : E
a✝ b : 𝕜
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
hA : A ∈ 𝓝 0
x : E
w : Set E
hw₁ : w ⊆ A
hw₂ : IsOpen w
hw₃ : 0 ∈ w
hc : Continuous fun t => t • x
r : ℝ
hr₁ : r > 0
hr₂ : Metric.ball 0 r ⊆ (fun t => t • x) ⁻¹' w
hr₃ : 0 < (r / 2)⁻¹
a : 𝕜
ha₁ : (r / 2)⁻¹ ≤ ‖a‖
ha₂ : 0 < ‖a‖
⊢ ‖a‖⁻¹ < r
[PROOFSTEP]
calc
  ‖a‖⁻¹ ≤ r / 2 := (inv_le (half_pos hr₁) ha₂).mp ha₁
  _ < r := half_lt_self hr₁
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedRing 𝕝
inst✝⁶ : NormedSpace 𝕜 𝕝
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SMulWithZero 𝕝 E
inst✝² : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a b : 𝕜
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
hA : Balanced 𝕜 A
⊢ Balanced 𝕜 (0 ∪ interior A)
[PROOFSTEP]
intro a ha
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedRing 𝕝
inst✝⁶ : NormedSpace 𝕜 𝕝
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SMulWithZero 𝕝 E
inst✝² : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a✝ b : 𝕜
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
hA : Balanced 𝕜 A
a : 𝕜
ha : ‖a‖ ≤ 1
⊢ a • (0 ∪ interior A) ⊆ 0 ∪ interior A
[PROOFSTEP]
obtain rfl | h := eq_or_ne a 0
[GOAL]
case inl
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedRing 𝕝
inst✝⁶ : NormedSpace 𝕜 𝕝
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SMulWithZero 𝕝 E
inst✝² : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a b : 𝕜
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
hA : Balanced 𝕜 A
ha : ‖0‖ ≤ 1
⊢ 0 • (0 ∪ interior A) ⊆ 0 ∪ interior A
[PROOFSTEP]
rw [zero_smul_set]
[GOAL]
case inl
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedRing 𝕝
inst✝⁶ : NormedSpace 𝕜 𝕝
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SMulWithZero 𝕝 E
inst✝² : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a b : 𝕜
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
hA : Balanced 𝕜 A
ha : ‖0‖ ≤ 1
⊢ 0 ⊆ 0 ∪ interior A
case inl
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedRing 𝕝
inst✝⁶ : NormedSpace 𝕜 𝕝
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SMulWithZero 𝕝 E
inst✝² : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a b : 𝕜
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
hA : Balanced 𝕜 A
ha : ‖0‖ ≤ 1
⊢ Set.Nonempty (0 ∪ interior A)
[PROOFSTEP]
exacts [subset_union_left _ _, ⟨0, Or.inl rfl⟩]
[GOAL]
case inr
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedRing 𝕝
inst✝⁶ : NormedSpace 𝕜 𝕝
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SMulWithZero 𝕝 E
inst✝² : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a✝ b : 𝕜
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
hA : Balanced 𝕜 A
a : 𝕜
ha : ‖a‖ ≤ 1
h : a ≠ 0
⊢ a • (0 ∪ interior A) ⊆ 0 ∪ interior A
[PROOFSTEP]
rw [← image_smul, image_union]
[GOAL]
case inr
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedRing 𝕝
inst✝⁶ : NormedSpace 𝕜 𝕝
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SMulWithZero 𝕝 E
inst✝² : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a✝ b : 𝕜
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
hA : Balanced 𝕜 A
a : 𝕜
ha : ‖a‖ ≤ 1
h : a ≠ 0
⊢ (fun x => a • x) '' 0 ∪ (fun x => a • x) '' interior A ⊆ 0 ∪ interior A
[PROOFSTEP]
apply union_subset_union
[GOAL]
case inr.h₁
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedRing 𝕝
inst✝⁶ : NormedSpace 𝕜 𝕝
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SMulWithZero 𝕝 E
inst✝² : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a✝ b : 𝕜
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
hA : Balanced 𝕜 A
a : 𝕜
ha : ‖a‖ ≤ 1
h : a ≠ 0
⊢ (fun x => a • x) '' 0 ⊆ 0
[PROOFSTEP]
rw [image_zero, smul_zero]
[GOAL]
case inr.h₁
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedRing 𝕝
inst✝⁶ : NormedSpace 𝕜 𝕝
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SMulWithZero 𝕝 E
inst✝² : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a✝ b : 𝕜
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
hA : Balanced 𝕜 A
a : 𝕜
ha : ‖a‖ ≤ 1
h : a ≠ 0
⊢ {0} ⊆ 0
[PROOFSTEP]
rfl
[GOAL]
case inr.h₂
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedRing 𝕝
inst✝⁶ : NormedSpace 𝕜 𝕝
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SMulWithZero 𝕝 E
inst✝² : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a✝ b : 𝕜
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
hA : Balanced 𝕜 A
a : 𝕜
ha : ‖a‖ ≤ 1
h : a ≠ 0
⊢ (fun x => a • x) '' interior A ⊆ interior A
[PROOFSTEP]
calc
  a • interior A ⊆ interior (a • A) := (isOpenMap_smul₀ h).image_interior_subset A
  _ ⊆ interior A := interior_mono (hA _ ha)
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedRing 𝕝
inst✝⁶ : NormedSpace 𝕜 𝕝
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SMulWithZero 𝕝 E
inst✝² : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a b : 𝕜
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
hA : Balanced 𝕜 A
h : 0 ∈ _root_.interior A
⊢ Balanced 𝕜 (_root_.interior A)
[PROOFSTEP]
rw [← union_eq_self_of_subset_left (singleton_subset_iff.2 h)]
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedRing 𝕝
inst✝⁶ : NormedSpace 𝕜 𝕝
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SMulWithZero 𝕝 E
inst✝² : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a b : 𝕜
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
hA : Balanced 𝕜 A
h : 0 ∈ _root_.interior A
⊢ Balanced 𝕜 ({0} ∪ _root_.interior A)
[PROOFSTEP]
exact balanced_zero_union_interior hA
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
⊢ Absorbs 𝕜 s 0 ↔ 0 ∈ s
[PROOFSTEP]
refine' ⟨_, fun h => ⟨1, zero_lt_one, fun a _ => zero_subset.2 <| zero_mem_smul_set h⟩⟩
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
⊢ Absorbs 𝕜 s 0 → 0 ∈ s
[PROOFSTEP]
rintro ⟨r, hr, h⟩
[GOAL]
case intro.intro
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
r : ℝ
hr : 0 < r
h : ∀ (a : 𝕜), r ≤ ‖a‖ → 0 ⊆ a • s
⊢ 0 ∈ s
[PROOFSTEP]
obtain ⟨a, ha⟩ := NormedSpace.exists_lt_norm 𝕜 𝕜 r
[GOAL]
case intro.intro.intro
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
r : ℝ
hr : 0 < r
h : ∀ (a : 𝕜), r ≤ ‖a‖ → 0 ⊆ a • s
a : 𝕜
ha : r < ‖a‖
⊢ 0 ∈ s
[PROOFSTEP]
have := h _ ha.le
[GOAL]
case intro.intro.intro
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
r : ℝ
hr : 0 < r
h : ∀ (a : 𝕜), r ≤ ‖a‖ → 0 ⊆ a • s
a : 𝕜
ha : r < ‖a‖
this : 0 ⊆ a • s
⊢ 0 ∈ s
[PROOFSTEP]
rwa [zero_subset, zero_mem_smul_set_iff] at this
[GOAL]
case intro.intro.intro
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
r : ℝ
hr : 0 < r
h : ∀ (a : 𝕜), r ≤ ‖a‖ → 0 ⊆ a • s
a : 𝕜
ha : r < ‖a‖
this : 0 ∈ a • s
⊢ a ≠ 0
[PROOFSTEP]
exact norm_ne_zero_iff.1 (hr.trans ha).ne'
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
s : Set E
inst✝¹ : Module ℝ E
inst✝ : SMulCommClass ℝ 𝕜 E
hs : Balanced 𝕜 s
⊢ Balanced 𝕜 (↑(convexHull ℝ) s)
[PROOFSTEP]
suffices Convex ℝ {x | ∀ a : 𝕜, ‖a‖ ≤ 1 → a • x ∈ convexHull ℝ s}
  by
  rw [balanced_iff_smul_mem] at hs ⊢
  refine' fun a ha x hx => convexHull_min _ this hx a ha
  exact fun y hy a ha => subset_convexHull ℝ s (hs ha hy)
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
s : Set E
inst✝¹ : Module ℝ E
inst✝ : SMulCommClass ℝ 𝕜 E
hs : Balanced 𝕜 s
this : Convex ℝ {x | ∀ (a : 𝕜), ‖a‖ ≤ 1 → a • x ∈ ↑(convexHull ℝ) s}
⊢ Balanced 𝕜 (↑(convexHull ℝ) s)
[PROOFSTEP]
rw [balanced_iff_smul_mem] at hs ⊢
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
s : Set E
inst✝¹ : Module ℝ E
inst✝ : SMulCommClass ℝ 𝕜 E
hs : ∀ ⦃a : 𝕜⦄, ‖a‖ ≤ 1 → ∀ ⦃x : E⦄, x ∈ s → a • x ∈ s
this : Convex ℝ {x | ∀ (a : 𝕜), ‖a‖ ≤ 1 → a • x ∈ ↑(convexHull ℝ) s}
⊢ ∀ ⦃a : 𝕜⦄, ‖a‖ ≤ 1 → ∀ ⦃x : E⦄, x ∈ ↑(convexHull ℝ) s → a • x ∈ ↑(convexHull ℝ) s
[PROOFSTEP]
refine' fun a ha x hx => convexHull_min _ this hx a ha
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
s : Set E
inst✝¹ : Module ℝ E
inst✝ : SMulCommClass ℝ 𝕜 E
hs : ∀ ⦃a : 𝕜⦄, ‖a‖ ≤ 1 → ∀ ⦃x : E⦄, x ∈ s → a • x ∈ s
this : Convex ℝ {x | ∀ (a : 𝕜), ‖a‖ ≤ 1 → a • x ∈ ↑(convexHull ℝ) s}
a : 𝕜
ha : ‖a‖ ≤ 1
x : E
hx : x ∈ ↑(convexHull ℝ) s
⊢ s ⊆ {x | ∀ (a : 𝕜), ‖a‖ ≤ 1 → a • x ∈ ↑(convexHull ℝ) s}
[PROOFSTEP]
exact fun y hy a ha => subset_convexHull ℝ s (hs ha hy)
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
s : Set E
inst✝¹ : Module ℝ E
inst✝ : SMulCommClass ℝ 𝕜 E
hs : Balanced 𝕜 s
⊢ Convex ℝ {x | ∀ (a : 𝕜), ‖a‖ ≤ 1 → a • x ∈ ↑(convexHull ℝ) s}
[PROOFSTEP]
intro x hx y hy u v hu hv huv a ha
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
s : Set E
inst✝¹ : Module ℝ E
inst✝ : SMulCommClass ℝ 𝕜 E
hs : Balanced 𝕜 s
x : E
hx : x ∈ {x | ∀ (a : 𝕜), ‖a‖ ≤ 1 → a • x ∈ ↑(convexHull ℝ) s}
y : E
hy : y ∈ {x | ∀ (a : 𝕜), ‖a‖ ≤ 1 → a • x ∈ ↑(convexHull ℝ) s}
u v : ℝ
hu : 0 ≤ u
hv : 0 ≤ v
huv : u + v = 1
a : 𝕜
ha : ‖a‖ ≤ 1
⊢ a • (u • x + v • y) ∈ ↑(convexHull ℝ) s
[PROOFSTEP]
simp only [smul_add, ← smul_comm]
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
s : Set E
inst✝¹ : Module ℝ E
inst✝ : SMulCommClass ℝ 𝕜 E
hs : Balanced 𝕜 s
x : E
hx : x ∈ {x | ∀ (a : 𝕜), ‖a‖ ≤ 1 → a • x ∈ ↑(convexHull ℝ) s}
y : E
hy : y ∈ {x | ∀ (a : 𝕜), ‖a‖ ≤ 1 → a • x ∈ ↑(convexHull ℝ) s}
u v : ℝ
hu : 0 ≤ u
hv : 0 ≤ v
huv : u + v = 1
a : 𝕜
ha : ‖a‖ ≤ 1
⊢ u • a • x + v • a • y ∈ ↑(convexHull ℝ) s
[PROOFSTEP]
exact convex_convexHull ℝ s (hx a ha) (hy a ha) hu hv huv
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
hs : Convex ℝ s
⊢ Balanced ℝ s ↔ ∀ ⦃x : E⦄, x ∈ s → -x ∈ s
[PROOFSTEP]
refine' ⟨fun h x => h.neg_mem_iff.2, fun h a ha => smul_set_subset_iff.2 fun x hx => _⟩
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
hs : Convex ℝ s
h : ∀ ⦃x : E⦄, x ∈ s → -x ∈ s
a : ℝ
ha : ‖a‖ ≤ 1
x : E
hx : x ∈ s
⊢ a • x ∈ s
[PROOFSTEP]
rw [Real.norm_eq_abs, abs_le] at ha
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
hs : Convex ℝ s
h : ∀ ⦃x : E⦄, x ∈ s → -x ∈ s
a : ℝ
ha : -1 ≤ a ∧ a ≤ 1
x : E
hx : x ∈ s
⊢ a • x ∈ s
[PROOFSTEP]
rw [show a = -((1 - a) / 2) + (a - -1) / 2 by ring, add_smul, neg_smul, ← smul_neg]
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
hs : Convex ℝ s
h : ∀ ⦃x : E⦄, x ∈ s → -x ∈ s
a : ℝ
ha : -1 ≤ a ∧ a ≤ 1
x : E
hx : x ∈ s
⊢ a = -((1 - a) / 2) + (a - -1) / 2
[PROOFSTEP]
ring
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
hs : Convex ℝ s
h : ∀ ⦃x : E⦄, x ∈ s → -x ∈ s
a : ℝ
ha : -1 ≤ a ∧ a ≤ 1
x : E
hx : x ∈ s
⊢ ((1 - a) / 2) • -x + ((a - -1) / 2) • x ∈ s
[PROOFSTEP]
exact
  hs (h hx) hx (div_nonneg (sub_nonneg_of_le ha.2) zero_le_two) (div_nonneg (sub_nonneg_of_le ha.1) zero_le_two)
    (by ring)
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
hs : Convex ℝ s
h : ∀ ⦃x : E⦄, x ∈ s → -x ∈ s
a : ℝ
ha : -1 ≤ a ∧ a ≤ 1
x : E
hx : x ∈ s
⊢ (1 - a) / 2 + (a - -1) / 2 = 1
[PROOFSTEP]
ring


[GOAL]
a : ℝ
⊢ interior {z | z.re ≤ a} = {z | z.re < a}
[PROOFSTEP]
simpa only [interior_Iic] using interior_preimage_re (Iic a)
[GOAL]
a : ℝ
⊢ interior {z | z.im ≤ a} = {z | z.im < a}
[PROOFSTEP]
simpa only [interior_Iic] using interior_preimage_im (Iic a)
[GOAL]
a : ℝ
⊢ interior {z | a ≤ z.re} = {z | a < z.re}
[PROOFSTEP]
simpa only [interior_Ici] using interior_preimage_re (Ici a)
[GOAL]
a : ℝ
⊢ interior {z | a ≤ z.im} = {z | a < z.im}
[PROOFSTEP]
simpa only [interior_Ici] using interior_preimage_im (Ici a)
[GOAL]
a : ℝ
⊢ closure {z | z.re < a} = {z | z.re ≤ a}
[PROOFSTEP]
simpa only [closure_Iio] using closure_preimage_re (Iio a)
[GOAL]
a : ℝ
⊢ closure {z | z.im < a} = {z | z.im ≤ a}
[PROOFSTEP]
simpa only [closure_Iio] using closure_preimage_im (Iio a)
[GOAL]
a : ℝ
⊢ closure {z | a < z.re} = {z | a ≤ z.re}
[PROOFSTEP]
simpa only [closure_Ioi] using closure_preimage_re (Ioi a)
[GOAL]
a : ℝ
⊢ closure {z | a < z.im} = {z | a ≤ z.im}
[PROOFSTEP]
simpa only [closure_Ioi] using closure_preimage_im (Ioi a)
[GOAL]
a : ℝ
⊢ frontier {z | z.re ≤ a} = {z | z.re = a}
[PROOFSTEP]
simpa only [frontier_Iic] using frontier_preimage_re (Iic a)
[GOAL]
a : ℝ
⊢ frontier {z | z.im ≤ a} = {z | z.im = a}
[PROOFSTEP]
simpa only [frontier_Iic] using frontier_preimage_im (Iic a)
[GOAL]
a : ℝ
⊢ frontier {z | a ≤ z.re} = {z | z.re = a}
[PROOFSTEP]
simpa only [frontier_Ici] using frontier_preimage_re (Ici a)
[GOAL]
a : ℝ
⊢ frontier {z | a ≤ z.im} = {z | z.im = a}
[PROOFSTEP]
simpa only [frontier_Ici] using frontier_preimage_im (Ici a)
[GOAL]
a : ℝ
⊢ frontier {z | z.re < a} = {z | z.re = a}
[PROOFSTEP]
simpa only [frontier_Iio] using frontier_preimage_re (Iio a)
[GOAL]
a : ℝ
⊢ frontier {z | z.im < a} = {z | z.im = a}
[PROOFSTEP]
simpa only [frontier_Iio] using frontier_preimage_im (Iio a)
[GOAL]
a : ℝ
⊢ frontier {z | a < z.re} = {z | z.re = a}
[PROOFSTEP]
simpa only [frontier_Ioi] using frontier_preimage_re (Ioi a)
[GOAL]
a : ℝ
⊢ frontier {z | a < z.im} = {z | z.im = a}
[PROOFSTEP]
simpa only [frontier_Ioi] using frontier_preimage_im (Ioi a)
[GOAL]
s t : Set ℝ
⊢ closure (s ×ℂ t) = closure s ×ℂ closure t
[PROOFSTEP]
simpa only [← preimage_eq_preimage equivRealProdClm.symm.toHomeomorph.surjective,
  equivRealProdClm.symm.toHomeomorph.preimage_closure] using @closure_prod_eq _ _ _ _ s t
[GOAL]
s t : Set ℝ
⊢ interior (s ×ℂ t) = interior s ×ℂ interior t
[PROOFSTEP]
rw [Set.reProdIm, Set.reProdIm, interior_inter, interior_preimage_re, interior_preimage_im]
[GOAL]
s t : Set ℝ
⊢ frontier (s ×ℂ t) = closure s ×ℂ frontier t ∪ frontier s ×ℂ closure t
[PROOFSTEP]
simpa only [← preimage_eq_preimage equivRealProdClm.symm.toHomeomorph.surjective,
  equivRealProdClm.symm.toHomeomorph.preimage_frontier] using frontier_prod_eq s t
[GOAL]
a b : ℝ
⊢ frontier {z | a ≤ z.re ∧ b ≤ z.im} = {z | a ≤ z.re ∧ z.im = b ∨ z.re = a ∧ b ≤ z.im}
[PROOFSTEP]
simpa only [closure_Ici, frontier_Ici] using frontier_reProdIm (Ici a) (Ici b)
[GOAL]
a b : ℝ
⊢ frontier {z | a ≤ z.re ∧ z.im ≤ b} = {z | a ≤ z.re ∧ z.im = b ∨ z.re = a ∧ z.im ≤ b}
[PROOFSTEP]
simpa only [closure_Ici, closure_Iic, frontier_Ici, frontier_Iic] using frontier_reProdIm (Ici a) (Iic b)


[GOAL]
⊢ 1 = ‖↑reClm 1‖
[PROOFSTEP]
simp
[GOAL]
⊢ ‖1‖ ≤ 1
[PROOFSTEP]
simp
[GOAL]
⊢ 1 = ‖↑imClm I‖
[PROOFSTEP]
simp
[GOAL]
⊢ ‖I‖ ≤ 1
[PROOFSTEP]
simp


[GOAL]
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R₄ : Type u_4
E : Type u_5
E₂ : Type u_6
E₃ : Type u_7
E₄ : Type u_8
F : Type u_9
𝓕 : Type u_10
inst✝³³ : Semiring R
inst✝³² : Semiring R₂
inst✝³¹ : Semiring R₃
inst✝³⁰ : Semiring R₄
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
σ₁₃ : R →+* R₃
σ₃₁ : R₃ →+* R
σ₁₄ : R →+* R₄
σ₄₁ : R₄ →+* R
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
σ₂₄ : R₂ →+* R₄
σ₄₂ : R₄ →+* R₂
σ₃₄ : R₃ →+* R₄
σ₄₃ : R₄ →+* R₃
inst✝²⁹ : RingHomInvPair σ₁₂ σ₂₁
inst✝²⁸ : RingHomInvPair σ₂₁ σ₁₂
inst✝²⁷ : RingHomInvPair σ₁₃ σ₃₁
inst✝²⁶ : RingHomInvPair σ₃₁ σ₁₃
inst✝²⁵ : RingHomInvPair σ₂₃ σ₃₂
inst✝²⁴ : RingHomInvPair σ₃₂ σ₂₃
inst✝²³ : RingHomInvPair σ₁₄ σ₄₁
inst✝²² : RingHomInvPair σ₄₁ σ₁₄
inst✝²¹ : RingHomInvPair σ₂₄ σ₄₂
inst✝²⁰ : RingHomInvPair σ₄₂ σ₂₄
inst✝¹⁹ : RingHomInvPair σ₃₄ σ₄₃
inst✝¹⁸ : RingHomInvPair σ₄₃ σ₃₄
inst✝¹⁷ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹⁶ : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄
inst✝¹⁵ : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄
inst✝¹⁴ : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
inst✝¹³ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
inst✝¹² : RingHomCompTriple σ₄₂ σ₂₁ σ₄₁
inst✝¹¹ : RingHomCompTriple σ₄₃ σ₃₂ σ₄₂
inst✝¹⁰ : RingHomCompTriple σ₄₃ σ₃₁ σ₄₁
inst✝⁹ : SeminormedAddCommGroup E
inst✝⁸ : SeminormedAddCommGroup E₂
inst✝⁷ : SeminormedAddCommGroup E₃
inst✝⁶ : SeminormedAddCommGroup E₄
inst✝⁵ : Module R E
inst✝⁴ : Module R₂ E₂
inst✝³ : Module R₃ E₃
inst✝² : Module R₄ E₄
inst✝¹ : NormedAddCommGroup F
inst✝ : Module R F
f : E →ₛₗᵢ[σ₁₂] E₂
f₁ : F →ₛₗᵢ[σ₁₂] E₂
⊢ Injective fun f => ↑f
[PROOFSTEP]
rintro ⟨_⟩ ⟨_⟩
[GOAL]
case mk.mk
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R₄ : Type u_4
E : Type u_5
E₂ : Type u_6
E₃ : Type u_7
E₄ : Type u_8
F : Type u_9
𝓕 : Type u_10
inst✝³³ : Semiring R
inst✝³² : Semiring R₂
inst✝³¹ : Semiring R₃
inst✝³⁰ : Semiring R₄
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
σ₁₃ : R →+* R₃
σ₃₁ : R₃ →+* R
σ₁₄ : R →+* R₄
σ₄₁ : R₄ →+* R
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
σ₂₄ : R₂ →+* R₄
σ₄₂ : R₄ →+* R₂
σ₃₄ : R₃ →+* R₄
σ₄₃ : R₄ →+* R₃
inst✝²⁹ : RingHomInvPair σ₁₂ σ₂₁
inst✝²⁸ : RingHomInvPair σ₂₁ σ₁₂
inst✝²⁷ : RingHomInvPair σ₁₃ σ₃₁
inst✝²⁶ : RingHomInvPair σ₃₁ σ₁₃
inst✝²⁵ : RingHomInvPair σ₂₃ σ₃₂
inst✝²⁴ : RingHomInvPair σ₃₂ σ₂₃
inst✝²³ : RingHomInvPair σ₁₄ σ₄₁
inst✝²² : RingHomInvPair σ₄₁ σ₁₄
inst✝²¹ : RingHomInvPair σ₂₄ σ₄₂
inst✝²⁰ : RingHomInvPair σ₄₂ σ₂₄
inst✝¹⁹ : RingHomInvPair σ₃₄ σ₄₃
inst✝¹⁸ : RingHomInvPair σ₄₃ σ₃₄
inst✝¹⁷ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹⁶ : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄
inst✝¹⁵ : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄
inst✝¹⁴ : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
inst✝¹³ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
inst✝¹² : RingHomCompTriple σ₄₂ σ₂₁ σ₄₁
inst✝¹¹ : RingHomCompTriple σ₄₃ σ₃₂ σ₄₂
inst✝¹⁰ : RingHomCompTriple σ₄₃ σ₃₁ σ₄₁
inst✝⁹ : SeminormedAddCommGroup E
inst✝⁸ : SeminormedAddCommGroup E₂
inst✝⁷ : SeminormedAddCommGroup E₃
inst✝⁶ : SeminormedAddCommGroup E₄
inst✝⁵ : Module R E
inst✝⁴ : Module R₂ E₂
inst✝³ : Module R₃ E₃
inst✝² : Module R₄ E₄
inst✝¹ : NormedAddCommGroup F
inst✝ : Module R F
f : E →ₛₗᵢ[σ₁₂] E₂
f₁ : F →ₛₗᵢ[σ₁₂] E₂
toLinearMap✝¹ : E →ₛₗ[σ₁₂] E₂
norm_map'✝¹ : ∀ (x : E), ‖↑toLinearMap✝¹ x‖ = ‖x‖
toLinearMap✝ : E →ₛₗ[σ₁₂] E₂
norm_map'✝ : ∀ (x : E), ‖↑toLinearMap✝ x‖ = ‖x‖
⊢ (fun f => ↑f) { toLinearMap := toLinearMap✝¹, norm_map' := norm_map'✝¹ } =
      (fun f => ↑f) { toLinearMap := toLinearMap✝, norm_map' := norm_map'✝ } →
    { toLinearMap := toLinearMap✝¹, norm_map' := norm_map'✝¹ } =
      { toLinearMap := toLinearMap✝, norm_map' := norm_map'✝ }
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R₄ : Type u_4
E : Type u_5
E₂ : Type u_6
E₃ : Type u_7
E₄ : Type u_8
F : Type u_9
𝓕 : Type u_10
inst✝³³ : Semiring R
inst✝³² : Semiring R₂
inst✝³¹ : Semiring R₃
inst✝³⁰ : Semiring R₄
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
σ₁₃ : R →+* R₃
σ₃₁ : R₃ →+* R
σ₁₄ : R →+* R₄
σ₄₁ : R₄ →+* R
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
σ₂₄ : R₂ →+* R₄
σ₄₂ : R₄ →+* R₂
σ₃₄ : R₃ →+* R₄
σ₄₃ : R₄ →+* R₃
inst✝²⁹ : RingHomInvPair σ₁₂ σ₂₁
inst✝²⁸ : RingHomInvPair σ₂₁ σ₁₂
inst✝²⁷ : RingHomInvPair σ₁₃ σ₃₁
inst✝²⁶ : RingHomInvPair σ₃₁ σ₁₃
inst✝²⁵ : RingHomInvPair σ₂₃ σ₃₂
inst✝²⁴ : RingHomInvPair σ₃₂ σ₂₃
inst✝²³ : RingHomInvPair σ₁₄ σ₄₁
inst✝²² : RingHomInvPair σ₄₁ σ₁₄
inst✝²¹ : RingHomInvPair σ₂₄ σ₄₂
inst✝²⁰ : RingHomInvPair σ₄₂ σ₂₄
inst✝¹⁹ : RingHomInvPair σ₃₄ σ₄₃
inst✝¹⁸ : RingHomInvPair σ₄₃ σ₃₄
inst✝¹⁷ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹⁶ : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄
inst✝¹⁵ : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄
inst✝¹⁴ : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
inst✝¹³ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
inst✝¹² : RingHomCompTriple σ₄₂ σ₂₁ σ₄₁
inst✝¹¹ : RingHomCompTriple σ₄₃ σ₃₂ σ₄₂
inst✝¹⁰ : RingHomCompTriple σ₄₃ σ₃₁ σ₄₁
inst✝⁹ : SeminormedAddCommGroup E
inst✝⁸ : SeminormedAddCommGroup E₂
inst✝⁷ : SeminormedAddCommGroup E₃
inst✝⁶ : SeminormedAddCommGroup E₄
inst✝⁵ : Module R E
inst✝⁴ : Module R₂ E₂
inst✝³ : Module R₃ E₃
inst✝² : Module R₄ E₄
inst✝¹ : NormedAddCommGroup F
inst✝ : Module R F
f : E →ₛₗ[σ₁₂] E₂
hf : Isometry ↑f
⊢ ∀ (x : E),
    ‖↑{ toAddHom := f.toAddHom,
              map_smul' :=
                (_ : ∀ (r : R) (x : E), AddHom.toFun f.toAddHom (r • x) = ↑σ₁₂ r • AddHom.toFun f.toAddHom x) }
          x‖ =
      ‖x‖
[PROOFSTEP]
simp_rw [← dist_zero_right]
[GOAL]
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R₄ : Type u_4
E : Type u_5
E₂ : Type u_6
E₃ : Type u_7
E₄ : Type u_8
F : Type u_9
𝓕 : Type u_10
inst✝³³ : Semiring R
inst✝³² : Semiring R₂
inst✝³¹ : Semiring R₃
inst✝³⁰ : Semiring R₄
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
σ₁₃ : R →+* R₃
σ₃₁ : R₃ →+* R
σ₁₄ : R →+* R₄
σ₄₁ : R₄ →+* R
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
σ₂₄ : R₂ →+* R₄
σ₄₂ : R₄ →+* R₂
σ₃₄ : R₃ →+* R₄
σ₄₃ : R₄ →+* R₃
inst✝²⁹ : RingHomInvPair σ₁₂ σ₂₁
inst✝²⁸ : RingHomInvPair σ₂₁ σ₁₂
inst✝²⁷ : RingHomInvPair σ₁₃ σ₃₁
inst✝²⁶ : RingHomInvPair σ₃₁ σ₁₃
inst✝²⁵ : RingHomInvPair σ₂₃ σ₃₂
inst✝²⁴ : RingHomInvPair σ₃₂ σ₂₃
inst✝²³ : RingHomInvPair σ₁₄ σ₄₁
inst✝²² : RingHomInvPair σ₄₁ σ₁₄
inst✝²¹ : RingHomInvPair σ₂₄ σ₄₂
inst✝²⁰ : RingHomInvPair σ₄₂ σ₂₄
inst✝¹⁹ : RingHomInvPair σ₃₄ σ₄₃
inst✝¹⁸ : RingHomInvPair σ₄₃ σ₃₄
inst✝¹⁷ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹⁶ : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄
inst✝¹⁵ : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄
inst✝¹⁴ : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
inst✝¹³ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
inst✝¹² : RingHomCompTriple σ₄₂ σ₂₁ σ₄₁
inst✝¹¹ : RingHomCompTriple σ₄₃ σ₃₂ σ₄₂
inst✝¹⁰ : RingHomCompTriple σ₄₃ σ₃₁ σ₄₁
inst✝⁹ : SeminormedAddCommGroup E
inst✝⁸ : SeminormedAddCommGroup E₂
inst✝⁷ : SeminormedAddCommGroup E₃
inst✝⁶ : SeminormedAddCommGroup E₄
inst✝⁵ : Module R E
inst✝⁴ : Module R₂ E₂
inst✝³ : Module R₃ E₃
inst✝² : Module R₄ E₄
inst✝¹ : NormedAddCommGroup F
inst✝ : Module R F
f : E →ₛₗ[σ₁₂] E₂
hf : Isometry ↑f
⊢ ∀ (x : E),
    dist
        (↑{ toAddHom := f.toAddHom,
              map_smul' :=
                (_ : ∀ (r : R) (x : E), AddHom.toFun f.toAddHom (r • x) = ↑σ₁₂ r • AddHom.toFun f.toAddHom x) }
          x)
        0 =
      dist x 0
[PROOFSTEP]
simpa using (hf.dist_eq · 0)
[GOAL]
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R₄ : Type u_4
E : Type u_5
E₂ : Type u_6
E₃ : Type u_7
E₄ : Type u_8
F : Type u_9
𝓕 : Type u_10
inst✝³³ : Semiring R
inst✝³² : Semiring R₂
inst✝³¹ : Semiring R₃
inst✝³⁰ : Semiring R₄
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
σ₁₃ : R →+* R₃
σ₃₁ : R₃ →+* R
σ₁₄ : R →+* R₄
σ₄₁ : R₄ →+* R
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
σ₂₄ : R₂ →+* R₄
σ₄₂ : R₄ →+* R₂
σ₃₄ : R₃ →+* R₄
σ₄₃ : R₄ →+* R₃
inst✝²⁹ : RingHomInvPair σ₁₂ σ₂₁
inst✝²⁸ : RingHomInvPair σ₂₁ σ₁₂
inst✝²⁷ : RingHomInvPair σ₁₃ σ₃₁
inst✝²⁶ : RingHomInvPair σ₃₁ σ₁₃
inst✝²⁵ : RingHomInvPair σ₂₃ σ₃₂
inst✝²⁴ : RingHomInvPair σ₃₂ σ₂₃
inst✝²³ : RingHomInvPair σ₁₄ σ₄₁
inst✝²² : RingHomInvPair σ₄₁ σ₁₄
inst✝²¹ : RingHomInvPair σ₂₄ σ₄₂
inst✝²⁰ : RingHomInvPair σ₄₂ σ₂₄
inst✝¹⁹ : RingHomInvPair σ₃₄ σ₄₃
inst✝¹⁸ : RingHomInvPair σ₄₃ σ₃₄
inst✝¹⁷ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹⁶ : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄
inst✝¹⁵ : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄
inst✝¹⁴ : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
inst✝¹³ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
inst✝¹² : RingHomCompTriple σ₄₂ σ₂₁ σ₄₁
inst✝¹¹ : RingHomCompTriple σ₄₃ σ₃₂ σ₄₂
inst✝¹⁰ : RingHomCompTriple σ₄₃ σ₃₁ σ₄₁
inst✝⁹ : SeminormedAddCommGroup E
inst✝⁸ : SeminormedAddCommGroup E₂
inst✝⁷ : SeminormedAddCommGroup E₃
inst✝⁶ : SeminormedAddCommGroup E₄
inst✝⁵ : Module R E
inst✝⁴ : Module R₂ E₂
inst✝³ : Module R₃ E₃
inst✝² : Module R₄ E₄
inst✝¹ : NormedAddCommGroup F
inst✝ : Module R F
e f g : E ≃ₛₗᵢ[σ₁₂] E₂
h₁ : (fun e => e.toFun) f = (fun e => e.toFun) g
h₂ : (fun e => e.invFun) f = (fun e => e.invFun) g
⊢ f = g
[PROOFSTEP]
cases' f with f' _
[GOAL]
case mk
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R₄ : Type u_4
E : Type u_5
E₂ : Type u_6
E₃ : Type u_7
E₄ : Type u_8
F : Type u_9
𝓕 : Type u_10
inst✝³³ : Semiring R
inst✝³² : Semiring R₂
inst✝³¹ : Semiring R₃
inst✝³⁰ : Semiring R₄
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
σ₁₃ : R →+* R₃
σ₃₁ : R₃ →+* R
σ₁₄ : R →+* R₄
σ₄₁ : R₄ →+* R
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
σ₂₄ : R₂ →+* R₄
σ₄₂ : R₄ →+* R₂
σ₃₄ : R₃ →+* R₄
σ₄₃ : R₄ →+* R₃
inst✝²⁹ : RingHomInvPair σ₁₂ σ₂₁
inst✝²⁸ : RingHomInvPair σ₂₁ σ₁₂
inst✝²⁷ : RingHomInvPair σ₁₃ σ₃₁
inst✝²⁶ : RingHomInvPair σ₃₁ σ₁₃
inst✝²⁵ : RingHomInvPair σ₂₃ σ₃₂
inst✝²⁴ : RingHomInvPair σ₃₂ σ₂₃
inst✝²³ : RingHomInvPair σ₁₄ σ₄₁
inst✝²² : RingHomInvPair σ₄₁ σ₁₄
inst✝²¹ : RingHomInvPair σ₂₄ σ₄₂
inst✝²⁰ : RingHomInvPair σ₄₂ σ₂₄
inst✝¹⁹ : RingHomInvPair σ₃₄ σ₄₃
inst✝¹⁸ : RingHomInvPair σ₄₃ σ₃₄
inst✝¹⁷ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹⁶ : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄
inst✝¹⁵ : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄
inst✝¹⁴ : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
inst✝¹³ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
inst✝¹² : RingHomCompTriple σ₄₂ σ₂₁ σ₄₁
inst✝¹¹ : RingHomCompTriple σ₄₃ σ₃₂ σ₄₂
inst✝¹⁰ : RingHomCompTriple σ₄₃ σ₃₁ σ₄₁
inst✝⁹ : SeminormedAddCommGroup E
inst✝⁸ : SeminormedAddCommGroup E₂
inst✝⁷ : SeminormedAddCommGroup E₃
inst✝⁶ : SeminormedAddCommGroup E₄
inst✝⁵ : Module R E
inst✝⁴ : Module R₂ E₂
inst✝³ : Module R₃ E₃
inst✝² : Module R₄ E₄
inst✝¹ : NormedAddCommGroup F
inst✝ : Module R F
e g : E ≃ₛₗᵢ[σ₁₂] E₂
f' : E ≃ₛₗ[σ₁₂] E₂
norm_map'✝ : ∀ (x : E), ‖↑f' x‖ = ‖x‖
h₁ : (fun e => e.toFun) { toLinearEquiv := f', norm_map' := norm_map'✝ } = (fun e => e.toFun) g
h₂ : (fun e => e.invFun) { toLinearEquiv := f', norm_map' := norm_map'✝ } = (fun e => e.invFun) g
⊢ { toLinearEquiv := f', norm_map' := norm_map'✝ } = g
[PROOFSTEP]
cases' g with g' _
[GOAL]
case mk.mk
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R₄ : Type u_4
E : Type u_5
E₂ : Type u_6
E₃ : Type u_7
E₄ : Type u_8
F : Type u_9
𝓕 : Type u_10
inst✝³³ : Semiring R
inst✝³² : Semiring R₂
inst✝³¹ : Semiring R₃
inst✝³⁰ : Semiring R₄
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
σ₁₃ : R →+* R₃
σ₃₁ : R₃ →+* R
σ₁₄ : R →+* R₄
σ₄₁ : R₄ →+* R
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
σ₂₄ : R₂ →+* R₄
σ₄₂ : R₄ →+* R₂
σ₃₄ : R₃ →+* R₄
σ₄₃ : R₄ →+* R₃
inst✝²⁹ : RingHomInvPair σ₁₂ σ₂₁
inst✝²⁸ : RingHomInvPair σ₂₁ σ₁₂
inst✝²⁷ : RingHomInvPair σ₁₃ σ₃₁
inst✝²⁶ : RingHomInvPair σ₃₁ σ₁₃
inst✝²⁵ : RingHomInvPair σ₂₃ σ₃₂
inst✝²⁴ : RingHomInvPair σ₃₂ σ₂₃
inst✝²³ : RingHomInvPair σ₁₄ σ₄₁
inst✝²² : RingHomInvPair σ₄₁ σ₁₄
inst✝²¹ : RingHomInvPair σ₂₄ σ₄₂
inst✝²⁰ : RingHomInvPair σ₄₂ σ₂₄
inst✝¹⁹ : RingHomInvPair σ₃₄ σ₄₃
inst✝¹⁸ : RingHomInvPair σ₄₃ σ₃₄
inst✝¹⁷ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹⁶ : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄
inst✝¹⁵ : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄
inst✝¹⁴ : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
inst✝¹³ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
inst✝¹² : RingHomCompTriple σ₄₂ σ₂₁ σ₄₁
inst✝¹¹ : RingHomCompTriple σ₄₃ σ₃₂ σ₄₂
inst✝¹⁰ : RingHomCompTriple σ₄₃ σ₃₁ σ₄₁
inst✝⁹ : SeminormedAddCommGroup E
inst✝⁸ : SeminormedAddCommGroup E₂
inst✝⁷ : SeminormedAddCommGroup E₃
inst✝⁶ : SeminormedAddCommGroup E₄
inst✝⁵ : Module R E
inst✝⁴ : Module R₂ E₂
inst✝³ : Module R₃ E₃
inst✝² : Module R₄ E₄
inst✝¹ : NormedAddCommGroup F
inst✝ : Module R F
e : E ≃ₛₗᵢ[σ₁₂] E₂
f' : E ≃ₛₗ[σ₁₂] E₂
norm_map'✝¹ : ∀ (x : E), ‖↑f' x‖ = ‖x‖
g' : E ≃ₛₗ[σ₁₂] E₂
norm_map'✝ : ∀ (x : E), ‖↑g' x‖ = ‖x‖
h₁ :
  (fun e => e.toFun) { toLinearEquiv := f', norm_map' := norm_map'✝¹ } =
    (fun e => e.toFun) { toLinearEquiv := g', norm_map' := norm_map'✝ }
h₂ :
  (fun e => e.invFun) { toLinearEquiv := f', norm_map' := norm_map'✝¹ } =
    (fun e => e.invFun) { toLinearEquiv := g', norm_map' := norm_map'✝ }
⊢ { toLinearEquiv := f', norm_map' := norm_map'✝¹ } = { toLinearEquiv := g', norm_map' := norm_map'✝ }
[PROOFSTEP]
cases f'
[GOAL]
case mk.mk.mk
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R₄ : Type u_4
E : Type u_5
E₂ : Type u_6
E₃ : Type u_7
E₄ : Type u_8
F : Type u_9
𝓕 : Type u_10
inst✝³³ : Semiring R
inst✝³² : Semiring R₂
inst✝³¹ : Semiring R₃
inst✝³⁰ : Semiring R₄
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
σ₁₃ : R →+* R₃
σ₃₁ : R₃ →+* R
σ₁₄ : R →+* R₄
σ₄₁ : R₄ →+* R
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
σ₂₄ : R₂ →+* R₄
σ₄₂ : R₄ →+* R₂
σ₃₄ : R₃ →+* R₄
σ₄₃ : R₄ →+* R₃
inst✝²⁹ : RingHomInvPair σ₁₂ σ₂₁
inst✝²⁸ : RingHomInvPair σ₂₁ σ₁₂
inst✝²⁷ : RingHomInvPair σ₁₃ σ₃₁
inst✝²⁶ : RingHomInvPair σ₃₁ σ₁₃
inst✝²⁵ : RingHomInvPair σ₂₃ σ₃₂
inst✝²⁴ : RingHomInvPair σ₃₂ σ₂₃
inst✝²³ : RingHomInvPair σ₁₄ σ₄₁
inst✝²² : RingHomInvPair σ₄₁ σ₁₄
inst✝²¹ : RingHomInvPair σ₂₄ σ₄₂
inst✝²⁰ : RingHomInvPair σ₄₂ σ₂₄
inst✝¹⁹ : RingHomInvPair σ₃₄ σ₄₃
inst✝¹⁸ : RingHomInvPair σ₄₃ σ₃₄
inst✝¹⁷ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹⁶ : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄
inst✝¹⁵ : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄
inst✝¹⁴ : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
inst✝¹³ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
inst✝¹² : RingHomCompTriple σ₄₂ σ₂₁ σ₄₁
inst✝¹¹ : RingHomCompTriple σ₄₃ σ₃₂ σ₄₂
inst✝¹⁰ : RingHomCompTriple σ₄₃ σ₃₁ σ₄₁
inst✝⁹ : SeminormedAddCommGroup E
inst✝⁸ : SeminormedAddCommGroup E₂
inst✝⁷ : SeminormedAddCommGroup E₃
inst✝⁶ : SeminormedAddCommGroup E₄
inst✝⁵ : Module R E
inst✝⁴ : Module R₂ E₂
inst✝³ : Module R₃ E₃
inst✝² : Module R₄ E₄
inst✝¹ : NormedAddCommGroup F
inst✝ : Module R F
e : E ≃ₛₗᵢ[σ₁₂] E₂
g' : E ≃ₛₗ[σ₁₂] E₂
norm_map'✝¹ : ∀ (x : E), ‖↑g' x‖ = ‖x‖
toLinearMap✝ : E →ₛₗ[σ₁₂] E₂
invFun✝ : E₂ → E
left_inv✝ : LeftInverse invFun✝ toLinearMap✝.toFun
right_inv✝ : Function.RightInverse invFun✝ toLinearMap✝.toFun
norm_map'✝ :
  ∀ (x : E),
    ‖↑{ toLinearMap := toLinearMap✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } x‖ = ‖x‖
h₁ :
  (fun e => e.toFun)
      {
        toLinearEquiv :=
          { toLinearMap := toLinearMap✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ },
        norm_map' := norm_map'✝ } =
    (fun e => e.toFun) { toLinearEquiv := g', norm_map' := norm_map'✝¹ }
h₂ :
  (fun e => e.invFun)
      {
        toLinearEquiv :=
          { toLinearMap := toLinearMap✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ },
        norm_map' := norm_map'✝ } =
    (fun e => e.invFun) { toLinearEquiv := g', norm_map' := norm_map'✝¹ }
⊢ { toLinearEquiv := { toLinearMap := toLinearMap✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ },
      norm_map' := norm_map'✝ } =
    { toLinearEquiv := g', norm_map' := norm_map'✝¹ }
[PROOFSTEP]
cases g'
[GOAL]
case mk.mk.mk.mk
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R₄ : Type u_4
E : Type u_5
E₂ : Type u_6
E₃ : Type u_7
E₄ : Type u_8
F : Type u_9
𝓕 : Type u_10
inst✝³³ : Semiring R
inst✝³² : Semiring R₂
inst✝³¹ : Semiring R₃
inst✝³⁰ : Semiring R₄
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
σ₁₃ : R →+* R₃
σ₃₁ : R₃ →+* R
σ₁₄ : R →+* R₄
σ₄₁ : R₄ →+* R
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
σ₂₄ : R₂ →+* R₄
σ₄₂ : R₄ →+* R₂
σ₃₄ : R₃ →+* R₄
σ₄₃ : R₄ →+* R₃
inst✝²⁹ : RingHomInvPair σ₁₂ σ₂₁
inst✝²⁸ : RingHomInvPair σ₂₁ σ₁₂
inst✝²⁷ : RingHomInvPair σ₁₃ σ₃₁
inst✝²⁶ : RingHomInvPair σ₃₁ σ₁₃
inst✝²⁵ : RingHomInvPair σ₂₃ σ₃₂
inst✝²⁴ : RingHomInvPair σ₃₂ σ₂₃
inst✝²³ : RingHomInvPair σ₁₄ σ₄₁
inst✝²² : RingHomInvPair σ₄₁ σ₁₄
inst✝²¹ : RingHomInvPair σ₂₄ σ₄₂
inst✝²⁰ : RingHomInvPair σ₄₂ σ₂₄
inst✝¹⁹ : RingHomInvPair σ₃₄ σ₄₃
inst✝¹⁸ : RingHomInvPair σ₄₃ σ₃₄
inst✝¹⁷ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹⁶ : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄
inst✝¹⁵ : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄
inst✝¹⁴ : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
inst✝¹³ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
inst✝¹² : RingHomCompTriple σ₄₂ σ₂₁ σ₄₁
inst✝¹¹ : RingHomCompTriple σ₄₃ σ₃₂ σ₄₂
inst✝¹⁰ : RingHomCompTriple σ₄₃ σ₃₁ σ₄₁
inst✝⁹ : SeminormedAddCommGroup E
inst✝⁸ : SeminormedAddCommGroup E₂
inst✝⁷ : SeminormedAddCommGroup E₃
inst✝⁶ : SeminormedAddCommGroup E₄
inst✝⁵ : Module R E
inst✝⁴ : Module R₂ E₂
inst✝³ : Module R₃ E₃
inst✝² : Module R₄ E₄
inst✝¹ : NormedAddCommGroup F
inst✝ : Module R F
e : E ≃ₛₗᵢ[σ₁₂] E₂
toLinearMap✝¹ : E →ₛₗ[σ₁₂] E₂
invFun✝¹ : E₂ → E
left_inv✝¹ : LeftInverse invFun✝¹ toLinearMap✝¹.toFun
right_inv✝¹ : Function.RightInverse invFun✝¹ toLinearMap✝¹.toFun
norm_map'✝¹ :
  ∀ (x : E),
    ‖↑{ toLinearMap := toLinearMap✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ } x‖ = ‖x‖
toLinearMap✝ : E →ₛₗ[σ₁₂] E₂
invFun✝ : E₂ → E
left_inv✝ : LeftInverse invFun✝ toLinearMap✝.toFun
right_inv✝ : Function.RightInverse invFun✝ toLinearMap✝.toFun
norm_map'✝ :
  ∀ (x : E),
    ‖↑{ toLinearMap := toLinearMap✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } x‖ = ‖x‖
h₁ :
  (fun e => e.toFun)
      {
        toLinearEquiv :=
          { toLinearMap := toLinearMap✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ },
        norm_map' := norm_map'✝¹ } =
    (fun e => e.toFun)
      {
        toLinearEquiv :=
          { toLinearMap := toLinearMap✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ },
        norm_map' := norm_map'✝ }
h₂ :
  (fun e => e.invFun)
      {
        toLinearEquiv :=
          { toLinearMap := toLinearMap✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ },
        norm_map' := norm_map'✝¹ } =
    (fun e => e.invFun)
      {
        toLinearEquiv :=
          { toLinearMap := toLinearMap✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ },
        norm_map' := norm_map'✝ }
⊢ {
      toLinearEquiv :=
        { toLinearMap := toLinearMap✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ },
      norm_map' := norm_map'✝¹ } =
    {
      toLinearEquiv :=
        { toLinearMap := toLinearMap✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ },
      norm_map' := norm_map'✝ }
[PROOFSTEP]
simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, FunLike.coe_fn_eq] at h₁
[GOAL]
case mk.mk.mk.mk
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R₄ : Type u_4
E : Type u_5
E₂ : Type u_6
E₃ : Type u_7
E₄ : Type u_8
F : Type u_9
𝓕 : Type u_10
inst✝³³ : Semiring R
inst✝³² : Semiring R₂
inst✝³¹ : Semiring R₃
inst✝³⁰ : Semiring R₄
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
σ₁₃ : R →+* R₃
σ₃₁ : R₃ →+* R
σ₁₄ : R →+* R₄
σ₄₁ : R₄ →+* R
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
σ₂₄ : R₂ →+* R₄
σ₄₂ : R₄ →+* R₂
σ₃₄ : R₃ →+* R₄
σ₄₃ : R₄ →+* R₃
inst✝²⁹ : RingHomInvPair σ₁₂ σ₂₁
inst✝²⁸ : RingHomInvPair σ₂₁ σ₁₂
inst✝²⁷ : RingHomInvPair σ₁₃ σ₃₁
inst✝²⁶ : RingHomInvPair σ₃₁ σ₁₃
inst✝²⁵ : RingHomInvPair σ₂₃ σ₃₂
inst✝²⁴ : RingHomInvPair σ₃₂ σ₂₃
inst✝²³ : RingHomInvPair σ₁₄ σ₄₁
inst✝²² : RingHomInvPair σ₄₁ σ₁₄
inst✝²¹ : RingHomInvPair σ₂₄ σ₄₂
inst✝²⁰ : RingHomInvPair σ₄₂ σ₂₄
inst✝¹⁹ : RingHomInvPair σ₃₄ σ₄₃
inst✝¹⁸ : RingHomInvPair σ₄₃ σ₃₄
inst✝¹⁷ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹⁶ : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄
inst✝¹⁵ : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄
inst✝¹⁴ : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
inst✝¹³ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
inst✝¹² : RingHomCompTriple σ₄₂ σ₂₁ σ₄₁
inst✝¹¹ : RingHomCompTriple σ₄₃ σ₃₂ σ₄₂
inst✝¹⁰ : RingHomCompTriple σ₄₃ σ₃₁ σ₄₁
inst✝⁹ : SeminormedAddCommGroup E
inst✝⁸ : SeminormedAddCommGroup E₂
inst✝⁷ : SeminormedAddCommGroup E₃
inst✝⁶ : SeminormedAddCommGroup E₄
inst✝⁵ : Module R E
inst✝⁴ : Module R₂ E₂
inst✝³ : Module R₃ E₃
inst✝² : Module R₄ E₄
inst✝¹ : NormedAddCommGroup F
inst✝ : Module R F
e : E ≃ₛₗᵢ[σ₁₂] E₂
toLinearMap✝¹ : E →ₛₗ[σ₁₂] E₂
invFun✝¹ : E₂ → E
left_inv✝¹ : LeftInverse invFun✝¹ toLinearMap✝¹.toFun
right_inv✝¹ : Function.RightInverse invFun✝¹ toLinearMap✝¹.toFun
norm_map'✝¹ :
  ∀ (x : E),
    ‖↑{ toLinearMap := toLinearMap✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ } x‖ = ‖x‖
toLinearMap✝ : E →ₛₗ[σ₁₂] E₂
invFun✝ : E₂ → E
left_inv✝ : LeftInverse invFun✝ toLinearMap✝.toFun
right_inv✝ : Function.RightInverse invFun✝ toLinearMap✝.toFun
norm_map'✝ :
  ∀ (x : E),
    ‖↑{ toLinearMap := toLinearMap✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } x‖ = ‖x‖
h₂ :
  (fun e => e.invFun)
      {
        toLinearEquiv :=
          { toLinearMap := toLinearMap✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ },
        norm_map' := norm_map'✝¹ } =
    (fun e => e.invFun)
      {
        toLinearEquiv :=
          { toLinearMap := toLinearMap✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ },
        norm_map' := norm_map'✝ }
h₁ : toLinearMap✝¹ = toLinearMap✝
⊢ {
      toLinearEquiv :=
        { toLinearMap := toLinearMap✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ },
      norm_map' := norm_map'✝¹ } =
    {
      toLinearEquiv :=
        { toLinearMap := toLinearMap✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ },
      norm_map' := norm_map'✝ }
[PROOFSTEP]
congr
[GOAL]
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R₄ : Type u_4
E : Type u_5
E₂ : Type u_6
E₃ : Type u_7
E₄ : Type u_8
F : Type u_9
𝓕 : Type u_10
inst✝³³ : Semiring R
inst✝³² : Semiring R₂
inst✝³¹ : Semiring R₃
inst✝³⁰ : Semiring R₄
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
σ₁₃ : R →+* R₃
σ₃₁ : R₃ →+* R
σ₁₄ : R →+* R₄
σ₄₁ : R₄ →+* R
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
σ₂₄ : R₂ →+* R₄
σ₄₂ : R₄ →+* R₂
σ₃₄ : R₃ →+* R₄
σ₄₃ : R₄ →+* R₃
inst✝²⁹ : RingHomInvPair σ₁₂ σ₂₁
inst✝²⁸ : RingHomInvPair σ₂₁ σ₁₂
inst✝²⁷ : RingHomInvPair σ₁₃ σ₃₁
inst✝²⁶ : RingHomInvPair σ₃₁ σ₁₃
inst✝²⁵ : RingHomInvPair σ₂₃ σ₃₂
inst✝²⁴ : RingHomInvPair σ₃₂ σ₂₃
inst✝²³ : RingHomInvPair σ₁₄ σ₄₁
inst✝²² : RingHomInvPair σ₄₁ σ₁₄
inst✝²¹ : RingHomInvPair σ₂₄ σ₄₂
inst✝²⁰ : RingHomInvPair σ₄₂ σ₂₄
inst✝¹⁹ : RingHomInvPair σ₃₄ σ₄₃
inst✝¹⁸ : RingHomInvPair σ₄₃ σ₃₄
inst✝¹⁷ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹⁶ : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄
inst✝¹⁵ : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄
inst✝¹⁴ : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
inst✝¹³ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
inst✝¹² : RingHomCompTriple σ₄₂ σ₂₁ σ₄₁
inst✝¹¹ : RingHomCompTriple σ₄₃ σ₃₂ σ₄₂
inst✝¹⁰ : RingHomCompTriple σ₄₃ σ₃₁ σ₄₁
inst✝⁹ : SeminormedAddCommGroup E
inst✝⁸ : SeminormedAddCommGroup E₂
inst✝⁷ : SeminormedAddCommGroup E₃
inst✝⁶ : SeminormedAddCommGroup E₄
inst✝⁵ : Module R E
inst✝⁴ : Module R₂ E₂
inst✝³ : Module R₃ E₃
inst✝² : Module R₄ E₄
inst✝¹ : NormedAddCommGroup F
inst✝ : Module R F
e✝ : E ≃ₛₗᵢ[σ₁₂] E₂
e : E ≃ₛₗ[σ₁₂] E₂
h₁ : ∀ (x : E), ‖↑e x‖ ≤ ‖x‖
h₂ : ∀ (y : E₂), ‖↑(LinearEquiv.symm e) y‖ ≤ ‖y‖
x : E
⊢ ‖x‖ ≤ ‖↑e x‖
[PROOFSTEP]
simpa only [e.symm_apply_apply] using h₂ (e x)
[GOAL]
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R₄ : Type u_4
E : Type u_5
E₂ : Type u_6
E₃ : Type u_7
E₄ : Type u_8
F : Type u_9
𝓕 : Type u_10
inst✝³³ : Semiring R
inst✝³² : Semiring R₂
inst✝³¹ : Semiring R₃
inst✝³⁰ : Semiring R₄
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
σ₁₃ : R →+* R₃
σ₃₁ : R₃ →+* R
σ₁₄ : R →+* R₄
σ₄₁ : R₄ →+* R
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
σ₂₄ : R₂ →+* R₄
σ₄₂ : R₄ →+* R₂
σ₃₄ : R₃ →+* R₄
σ₄₃ : R₄ →+* R₃
inst✝²⁹ : RingHomInvPair σ₁₂ σ₂₁
inst✝²⁸ : RingHomInvPair σ₂₁ σ₁₂
inst✝²⁷ : RingHomInvPair σ₁₃ σ₃₁
inst✝²⁶ : RingHomInvPair σ₃₁ σ₁₃
inst✝²⁵ : RingHomInvPair σ₂₃ σ₃₂
inst✝²⁴ : RingHomInvPair σ₃₂ σ₂₃
inst✝²³ : RingHomInvPair σ₁₄ σ₄₁
inst✝²² : RingHomInvPair σ₄₁ σ₁₄
inst✝²¹ : RingHomInvPair σ₂₄ σ₄₂
inst✝²⁰ : RingHomInvPair σ₄₂ σ₂₄
inst✝¹⁹ : RingHomInvPair σ₃₄ σ₄₃
inst✝¹⁸ : RingHomInvPair σ₄₃ σ₃₄
inst✝¹⁷ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹⁶ : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄
inst✝¹⁵ : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄
inst✝¹⁴ : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
inst✝¹³ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
inst✝¹² : RingHomCompTriple σ₄₂ σ₂₁ σ₄₁
inst✝¹¹ : RingHomCompTriple σ₄₃ σ₃₂ σ₄₂
inst✝¹⁰ : RingHomCompTriple σ₄₃ σ₃₁ σ₄₁
inst✝⁹ : SeminormedAddCommGroup E
inst✝⁸ : SeminormedAddCommGroup E₂
inst✝⁷ : SeminormedAddCommGroup E₃
inst✝⁶ : SeminormedAddCommGroup E₄
inst✝⁵ : Module R E
inst✝⁴ : Module R₂ E₂
inst✝³ : Module R₃ E₃
inst✝² : Module R₄ E₄
inst✝¹ : NormedAddCommGroup F
inst✝ : Module R F
e✝ e : E ≃ₛₗᵢ[σ₁₂] E₂
⊢ range ↑e = univ
[PROOFSTEP]
rw [← coe_toIsometryEquiv]
[GOAL]
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R₄ : Type u_4
E : Type u_5
E₂ : Type u_6
E₃ : Type u_7
E₄ : Type u_8
F : Type u_9
𝓕 : Type u_10
inst✝³³ : Semiring R
inst✝³² : Semiring R₂
inst✝³¹ : Semiring R₃
inst✝³⁰ : Semiring R₄
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
σ₁₃ : R →+* R₃
σ₃₁ : R₃ →+* R
σ₁₄ : R →+* R₄
σ₄₁ : R₄ →+* R
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
σ₂₄ : R₂ →+* R₄
σ₄₂ : R₄ →+* R₂
σ₃₄ : R₃ →+* R₄
σ₄₃ : R₄ →+* R₃
inst✝²⁹ : RingHomInvPair σ₁₂ σ₂₁
inst✝²⁸ : RingHomInvPair σ₂₁ σ₁₂
inst✝²⁷ : RingHomInvPair σ₁₃ σ₃₁
inst✝²⁶ : RingHomInvPair σ₃₁ σ₁₃
inst✝²⁵ : RingHomInvPair σ₂₃ σ₃₂
inst✝²⁴ : RingHomInvPair σ₃₂ σ₂₃
inst✝²³ : RingHomInvPair σ₁₄ σ₄₁
inst✝²² : RingHomInvPair σ₄₁ σ₁₄
inst✝²¹ : RingHomInvPair σ₂₄ σ₄₂
inst✝²⁰ : RingHomInvPair σ₄₂ σ₂₄
inst✝¹⁹ : RingHomInvPair σ₃₄ σ₄₃
inst✝¹⁸ : RingHomInvPair σ₄₃ σ₃₄
inst✝¹⁷ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹⁶ : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄
inst✝¹⁵ : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄
inst✝¹⁴ : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
inst✝¹³ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
inst✝¹² : RingHomCompTriple σ₄₂ σ₂₁ σ₄₁
inst✝¹¹ : RingHomCompTriple σ₄₃ σ₃₂ σ₄₂
inst✝¹⁰ : RingHomCompTriple σ₄₃ σ₃₁ σ₄₁
inst✝⁹ : SeminormedAddCommGroup E
inst✝⁸ : SeminormedAddCommGroup E₂
inst✝⁷ : SeminormedAddCommGroup E₃
inst✝⁶ : SeminormedAddCommGroup E₄
inst✝⁵ : Module R E
inst✝⁴ : Module R₂ E₂
inst✝³ : Module R₃ E₃
inst✝² : Module R₄ E₄
inst✝¹ : NormedAddCommGroup F
inst✝ : Module R F
e✝ e : E ≃ₛₗᵢ[σ₁₂] E₂
⊢ range ↑(toIsometryEquiv e) = univ
[PROOFSTEP]
exact IsometryEquiv.range_eq_univ _
[GOAL]
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R₄ : Type u_4
E : Type u_5
E₂ : Type u_6
E₃ : Type u_7
E₄ : Type u_8
F : Type u_9
𝓕 : Type u_10
inst✝³⁴ : Semiring R
inst✝³³ : Semiring R₂
inst✝³² : Semiring R₃
inst✝³¹ : Semiring R₄
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
σ₁₃ : R →+* R₃
σ₃₁ : R₃ →+* R
σ₁₄ : R →+* R₄
σ₄₁ : R₄ →+* R
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
σ₂₄ : R₂ →+* R₄
σ₄₂ : R₄ →+* R₂
σ₃₄ : R₃ →+* R₄
σ₄₃ : R₄ →+* R₃
inst✝³⁰ : RingHomInvPair σ₁₂ σ₂₁
inst✝²⁹ : RingHomInvPair σ₂₁ σ₁₂
inst✝²⁸ : RingHomInvPair σ₁₃ σ₃₁
inst✝²⁷ : RingHomInvPair σ₃₁ σ₁₃
inst✝²⁶ : RingHomInvPair σ₂₃ σ₃₂
inst✝²⁵ : RingHomInvPair σ₃₂ σ₂₃
inst✝²⁴ : RingHomInvPair σ₁₄ σ₄₁
inst✝²³ : RingHomInvPair σ₄₁ σ₁₄
inst✝²² : RingHomInvPair σ₂₄ σ₄₂
inst✝²¹ : RingHomInvPair σ₄₂ σ₂₄
inst✝²⁰ : RingHomInvPair σ₃₄ σ₄₃
inst✝¹⁹ : RingHomInvPair σ₄₃ σ₃₄
inst✝¹⁸ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹⁷ : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄
inst✝¹⁶ : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄
inst✝¹⁵ : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
inst✝¹⁴ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
inst✝¹³ : RingHomCompTriple σ₄₂ σ₂₁ σ₄₁
inst✝¹² : RingHomCompTriple σ₄₃ σ₃₂ σ₄₂
inst✝¹¹ : RingHomCompTriple σ₄₃ σ₃₁ σ₄₁
inst✝¹⁰ : SeminormedAddCommGroup E
inst✝⁹ : SeminormedAddCommGroup E₂
inst✝⁸ : SeminormedAddCommGroup E₃
inst✝⁷ : SeminormedAddCommGroup E₄
inst✝⁶ : Module R E
inst✝⁵ : Module R₂ E₂
inst✝⁴ : Module R₃ E₃
inst✝³ : Module R₄ E₄
inst✝² : NormedAddCommGroup F
inst✝¹ : Module R F
e : E ≃ₛₗᵢ[σ₁₂] E₂
α : Type u_11
inst✝ : TopologicalSpace α
f : F →ₛₗᵢ[σ₁₂] E₂
hfr : Surjective ↑f
⊢ ↑(ofSurjective f hfr) = ↑f
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R₄ : Type u_4
E : Type u_5
E₂ : Type u_6
E₃ : Type u_7
E₄ : Type u_8
F : Type u_9
𝓕 : Type u_10
inst✝³⁴ : Semiring R
inst✝³³ : Semiring R₂
inst✝³² : Semiring R₃
inst✝³¹ : Semiring R₄
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
σ₁₃ : R →+* R₃
σ₃₁ : R₃ →+* R
σ₁₄ : R →+* R₄
σ₄₁ : R₄ →+* R
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
σ₂₄ : R₂ →+* R₄
σ₄₂ : R₄ →+* R₂
σ₃₄ : R₃ →+* R₄
σ₄₃ : R₄ →+* R₃
inst✝³⁰ : RingHomInvPair σ₁₂ σ₂₁
inst✝²⁹ : RingHomInvPair σ₂₁ σ₁₂
inst✝²⁸ : RingHomInvPair σ₁₃ σ₃₁
inst✝²⁷ : RingHomInvPair σ₃₁ σ₁₃
inst✝²⁶ : RingHomInvPair σ₂₃ σ₃₂
inst✝²⁵ : RingHomInvPair σ₃₂ σ₂₃
inst✝²⁴ : RingHomInvPair σ₁₄ σ₄₁
inst✝²³ : RingHomInvPair σ₄₁ σ₁₄
inst✝²² : RingHomInvPair σ₂₄ σ₄₂
inst✝²¹ : RingHomInvPair σ₄₂ σ₂₄
inst✝²⁰ : RingHomInvPair σ₃₄ σ₄₃
inst✝¹⁹ : RingHomInvPair σ₄₃ σ₃₄
inst✝¹⁸ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹⁷ : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄
inst✝¹⁶ : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄
inst✝¹⁵ : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
inst✝¹⁴ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
inst✝¹³ : RingHomCompTriple σ₄₂ σ₂₁ σ₄₁
inst✝¹² : RingHomCompTriple σ₄₃ σ₃₂ σ₄₂
inst✝¹¹ : RingHomCompTriple σ₄₃ σ₃₁ σ₄₁
inst✝¹⁰ : SeminormedAddCommGroup E
inst✝⁹ : SeminormedAddCommGroup E₂
inst✝⁸ : SeminormedAddCommGroup E₃
inst✝⁷ : SeminormedAddCommGroup E₄
inst✝⁶ : Module R E
inst✝⁵ : Module R₂ E₂
inst✝⁴ : Module R₃ E₃
inst✝³ : Module R₄ E₄
inst✝² : NormedAddCommGroup F
inst✝¹ : Module R F
e : E ≃ₛₗᵢ[σ₁₂] E₂
α : Type u_11
inst✝ : TopologicalSpace α
f : F →ₛₗᵢ[σ₁₂] E₂
hfr : Surjective ↑f
x✝ : F
⊢ ↑(ofSurjective f hfr) x✝ = ↑f x✝
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R₄ : Type u_4
E : Type u_5
E₂ : Type u_6
E₃ : Type u_7
E₄ : Type u_8
F : Type u_9
𝓕 : Type u_10
inst✝³⁶ : Semiring R
inst✝³⁵ : Semiring R₂
inst✝³⁴ : Semiring R₃
inst✝³³ : Semiring R₄
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
σ₁₃ : R →+* R₃
σ₃₁ : R₃ →+* R
σ₁₄ : R →+* R₄
σ₄₁ : R₄ →+* R
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
σ₂₄ : R₂ →+* R₄
σ₄₂ : R₄ →+* R₂
σ₃₄ : R₃ →+* R₄
σ₄₃ : R₄ →+* R₃
inst✝³² : RingHomInvPair σ₁₂ σ₂₁
inst✝³¹ : RingHomInvPair σ₂₁ σ₁₂
inst✝³⁰ : RingHomInvPair σ₁₃ σ₃₁
inst✝²⁹ : RingHomInvPair σ₃₁ σ₁₃
inst✝²⁸ : RingHomInvPair σ₂₃ σ₃₂
inst✝²⁷ : RingHomInvPair σ₃₂ σ₂₃
inst✝²⁶ : RingHomInvPair σ₁₄ σ₄₁
inst✝²⁵ : RingHomInvPair σ₄₁ σ₁₄
inst✝²⁴ : RingHomInvPair σ₂₄ σ₄₂
inst✝²³ : RingHomInvPair σ₄₂ σ₂₄
inst✝²² : RingHomInvPair σ₃₄ σ₄₃
inst✝²¹ : RingHomInvPair σ₄₃ σ₃₄
inst✝²⁰ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹⁹ : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄
inst✝¹⁸ : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄
inst✝¹⁷ : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
inst✝¹⁶ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
inst✝¹⁵ : RingHomCompTriple σ₄₂ σ₂₁ σ₄₁
inst✝¹⁴ : RingHomCompTriple σ₄₃ σ₃₂ σ₄₂
inst✝¹³ : RingHomCompTriple σ₄₃ σ₃₁ σ₄₁
inst✝¹² : SeminormedAddCommGroup E
inst✝¹¹ : SeminormedAddCommGroup E₂
inst✝¹⁰ : SeminormedAddCommGroup E₃
inst✝⁹ : SeminormedAddCommGroup E₄
inst✝⁸ : Module R E
inst✝⁷ : Module R₂ E₂
inst✝⁶ : Module R₃ E₃
inst✝⁵ : Module R₄ E₄
inst✝⁴ : NormedAddCommGroup F
inst✝³ : Module R F
e : E ≃ₛₗᵢ[σ₁₂] E₂
α : Type u_11
inst✝² : TopologicalSpace α
inst✝¹ : Module R E₂
inst✝ : Module R E₃
src✝ : (E × E₂) × E₃ ≃ E × E₂ × E₃ := Equiv.prodAssoc E E₂ E₃
⊢ ∀ (x y : (E × E₂) × E₃),
    ↑(Equiv.prodAssoc E E₂ E₃) (x + y) = ↑(Equiv.prodAssoc E E₂ E₃) x + ↑(Equiv.prodAssoc E E₂ E₃) y
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R₄ : Type u_4
E : Type u_5
E₂ : Type u_6
E₃ : Type u_7
E₄ : Type u_8
F : Type u_9
𝓕 : Type u_10
inst✝³⁶ : Semiring R
inst✝³⁵ : Semiring R₂
inst✝³⁴ : Semiring R₃
inst✝³³ : Semiring R₄
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
σ₁₃ : R →+* R₃
σ₃₁ : R₃ →+* R
σ₁₄ : R →+* R₄
σ₄₁ : R₄ →+* R
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
σ₂₄ : R₂ →+* R₄
σ₄₂ : R₄ →+* R₂
σ₃₄ : R₃ →+* R₄
σ₄₃ : R₄ →+* R₃
inst✝³² : RingHomInvPair σ₁₂ σ₂₁
inst✝³¹ : RingHomInvPair σ₂₁ σ₁₂
inst✝³⁰ : RingHomInvPair σ₁₃ σ₃₁
inst✝²⁹ : RingHomInvPair σ₃₁ σ₁₃
inst✝²⁸ : RingHomInvPair σ₂₃ σ₃₂
inst✝²⁷ : RingHomInvPair σ₃₂ σ₂₃
inst✝²⁶ : RingHomInvPair σ₁₄ σ₄₁
inst✝²⁵ : RingHomInvPair σ₄₁ σ₁₄
inst✝²⁴ : RingHomInvPair σ₂₄ σ₄₂
inst✝²³ : RingHomInvPair σ₄₂ σ₂₄
inst✝²² : RingHomInvPair σ₃₄ σ₄₃
inst✝²¹ : RingHomInvPair σ₄₃ σ₃₄
inst✝²⁰ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹⁹ : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄
inst✝¹⁸ : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄
inst✝¹⁷ : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
inst✝¹⁶ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
inst✝¹⁵ : RingHomCompTriple σ₄₂ σ₂₁ σ₄₁
inst✝¹⁴ : RingHomCompTriple σ₄₃ σ₃₂ σ₄₂
inst✝¹³ : RingHomCompTriple σ₄₃ σ₃₁ σ₄₁
inst✝¹² : SeminormedAddCommGroup E
inst✝¹¹ : SeminormedAddCommGroup E₂
inst✝¹⁰ : SeminormedAddCommGroup E₃
inst✝⁹ : SeminormedAddCommGroup E₄
inst✝⁸ : Module R E
inst✝⁷ : Module R₂ E₂
inst✝⁶ : Module R₃ E₃
inst✝⁵ : Module R₄ E₄
inst✝⁴ : NormedAddCommGroup F
inst✝³ : Module R F
e : E ≃ₛₗᵢ[σ₁₂] E₂
α : Type u_11
inst✝² : TopologicalSpace α
inst✝¹ : Module R E₂
inst✝ : Module R E₃
src✝ : (E × E₂) × E₃ ≃ E × E₂ × E₃ := Equiv.prodAssoc E E₂ E₃
⊢ ∀ (r : R) (x : (E × E₂) × E₃),
    AddHom.toFun
        { toFun := ↑(Equiv.prodAssoc E E₂ E₃),
          map_add' :=
            (_ :
              ∀ (a a_1 : (E × E₂) × E₃),
                (a.fst.fst + a_1.fst.fst, a.fst.snd + a_1.fst.snd, a.snd + a_1.snd) =
                  (a.fst.fst + a_1.fst.fst, a.fst.snd + a_1.fst.snd, a.snd + a_1.snd)) }
        (r • x) =
      ↑(RingHom.id R) r •
        AddHom.toFun
          { toFun := ↑(Equiv.prodAssoc E E₂ E₃),
            map_add' :=
              (_ :
                ∀ (a a_1 : (E × E₂) × E₃),
                  (a.fst.fst + a_1.fst.fst, a.fst.snd + a_1.fst.snd, a.snd + a_1.snd) =
                    (a.fst.fst + a_1.fst.fst, a.fst.snd + a_1.fst.snd, a.snd + a_1.snd)) }
          x
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R₄ : Type u_4
E : Type u_5
E₂ : Type u_6
E₃ : Type u_7
E₄ : Type u_8
F : Type u_9
𝓕 : Type u_10
inst✝³⁶ : Semiring R
inst✝³⁵ : Semiring R₂
inst✝³⁴ : Semiring R₃
inst✝³³ : Semiring R₄
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
σ₁₃ : R →+* R₃
σ₃₁ : R₃ →+* R
σ₁₄ : R →+* R₄
σ₄₁ : R₄ →+* R
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
σ₂₄ : R₂ →+* R₄
σ₄₂ : R₄ →+* R₂
σ₃₄ : R₃ →+* R₄
σ₄₃ : R₄ →+* R₃
inst✝³² : RingHomInvPair σ₁₂ σ₂₁
inst✝³¹ : RingHomInvPair σ₂₁ σ₁₂
inst✝³⁰ : RingHomInvPair σ₁₃ σ₃₁
inst✝²⁹ : RingHomInvPair σ₃₁ σ₁₃
inst✝²⁸ : RingHomInvPair σ₂₃ σ₃₂
inst✝²⁷ : RingHomInvPair σ₃₂ σ₂₃
inst✝²⁶ : RingHomInvPair σ₁₄ σ₄₁
inst✝²⁵ : RingHomInvPair σ₄₁ σ₁₄
inst✝²⁴ : RingHomInvPair σ₂₄ σ₄₂
inst✝²³ : RingHomInvPair σ₄₂ σ₂₄
inst✝²² : RingHomInvPair σ₃₄ σ₄₃
inst✝²¹ : RingHomInvPair σ₄₃ σ₃₄
inst✝²⁰ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹⁹ : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄
inst✝¹⁸ : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄
inst✝¹⁷ : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
inst✝¹⁶ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
inst✝¹⁵ : RingHomCompTriple σ₄₂ σ₂₁ σ₄₁
inst✝¹⁴ : RingHomCompTriple σ₄₃ σ₃₂ σ₄₂
inst✝¹³ : RingHomCompTriple σ₄₃ σ₃₁ σ₄₁
inst✝¹² : SeminormedAddCommGroup E
inst✝¹¹ : SeminormedAddCommGroup E₂
inst✝¹⁰ : SeminormedAddCommGroup E₃
inst✝⁹ : SeminormedAddCommGroup E₄
inst✝⁸ : Module R E
inst✝⁷ : Module R₂ E₂
inst✝⁶ : Module R₃ E₃
inst✝⁵ : Module R₄ E₄
inst✝⁴ : NormedAddCommGroup F
inst✝³ : Module R F
e : E ≃ₛₗᵢ[σ₁₂] E₂
α : Type u_11
inst✝² : TopologicalSpace α
inst✝¹ : Module R E₂
inst✝ : Module R E₃
src✝ : (E × E₂) × E₃ ≃ E × E₂ × E₃ := Equiv.prodAssoc E E₂ E₃
⊢ ∀ (x : (E × E₂) × E₃),
    ‖↑{
              toLinearMap :=
                {
                  toAddHom :=
                    { toFun := ↑(Equiv.prodAssoc E E₂ E₃),
                      map_add' :=
                        (_ :
                          ∀ (a a_1 : (E × E₂) × E₃),
                            (a.fst.fst + a_1.fst.fst, a.fst.snd + a_1.fst.snd, a.snd + a_1.snd) =
                              (a.fst.fst + a_1.fst.fst, a.fst.snd + a_1.fst.snd, a.snd + a_1.snd)) },
                  map_smul' :=
                    (_ :
                      ∀ (a : R) (a_1 : (E × E₂) × E₃),
                        (a • a_1.fst.fst, a • a_1.fst.snd, a • a_1.snd) =
                          (a • a_1.fst.fst, a • a_1.fst.snd, a • a_1.snd)) },
              invFun := ↑(Equiv.prodAssoc E E₂ E₃).symm, left_inv := (_ : LeftInverse src✝.invFun src✝.toFun),
              right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
          x‖ =
      ‖x‖
[PROOFSTEP]
rintro ⟨⟨e, f⟩, g⟩
[GOAL]
case mk.mk
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R₄ : Type u_4
E : Type u_5
E₂ : Type u_6
E₃ : Type u_7
E₄ : Type u_8
F : Type u_9
𝓕 : Type u_10
inst✝³⁶ : Semiring R
inst✝³⁵ : Semiring R₂
inst✝³⁴ : Semiring R₃
inst✝³³ : Semiring R₄
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
σ₁₃ : R →+* R₃
σ₃₁ : R₃ →+* R
σ₁₄ : R →+* R₄
σ₄₁ : R₄ →+* R
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
σ₂₄ : R₂ →+* R₄
σ₄₂ : R₄ →+* R₂
σ₃₄ : R₃ →+* R₄
σ₄₃ : R₄ →+* R₃
inst✝³² : RingHomInvPair σ₁₂ σ₂₁
inst✝³¹ : RingHomInvPair σ₂₁ σ₁₂
inst✝³⁰ : RingHomInvPair σ₁₃ σ₃₁
inst✝²⁹ : RingHomInvPair σ₃₁ σ₁₃
inst✝²⁸ : RingHomInvPair σ₂₃ σ₃₂
inst✝²⁷ : RingHomInvPair σ₃₂ σ₂₃
inst✝²⁶ : RingHomInvPair σ₁₄ σ₄₁
inst✝²⁵ : RingHomInvPair σ₄₁ σ₁₄
inst✝²⁴ : RingHomInvPair σ₂₄ σ₄₂
inst✝²³ : RingHomInvPair σ₄₂ σ₂₄
inst✝²² : RingHomInvPair σ₃₄ σ₄₃
inst✝²¹ : RingHomInvPair σ₄₃ σ₃₄
inst✝²⁰ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹⁹ : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄
inst✝¹⁸ : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄
inst✝¹⁷ : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
inst✝¹⁶ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
inst✝¹⁵ : RingHomCompTriple σ₄₂ σ₂₁ σ₄₁
inst✝¹⁴ : RingHomCompTriple σ₄₃ σ₃₂ σ₄₂
inst✝¹³ : RingHomCompTriple σ₄₃ σ₃₁ σ₄₁
inst✝¹² : SeminormedAddCommGroup E
inst✝¹¹ : SeminormedAddCommGroup E₂
inst✝¹⁰ : SeminormedAddCommGroup E₃
inst✝⁹ : SeminormedAddCommGroup E₄
inst✝⁸ : Module R E
inst✝⁷ : Module R₂ E₂
inst✝⁶ : Module R₃ E₃
inst✝⁵ : Module R₄ E₄
inst✝⁴ : NormedAddCommGroup F
inst✝³ : Module R F
e✝ : E ≃ₛₗᵢ[σ₁₂] E₂
α : Type u_11
inst✝² : TopologicalSpace α
inst✝¹ : Module R E₂
inst✝ : Module R E₃
src✝ : (E × E₂) × E₃ ≃ E × E₂ × E₃ := Equiv.prodAssoc E E₂ E₃
g : E₃
e : E
f : E₂
⊢ ‖↑{
            toLinearMap :=
              {
                toAddHom :=
                  { toFun := ↑(Equiv.prodAssoc E E₂ E₃),
                    map_add' :=
                      (_ :
                        ∀ (a a_1 : (E × E₂) × E₃),
                          (a.fst.fst + a_1.fst.fst, a.fst.snd + a_1.fst.snd, a.snd + a_1.snd) =
                            (a.fst.fst + a_1.fst.fst, a.fst.snd + a_1.fst.snd, a.snd + a_1.snd)) },
                map_smul' :=
                  (_ :
                    ∀ (a : R) (a_1 : (E × E₂) × E₃),
                      (a • a_1.fst.fst, a • a_1.fst.snd, a • a_1.snd) =
                        (a • a_1.fst.fst, a • a_1.fst.snd, a • a_1.snd)) },
            invFun := ↑(Equiv.prodAssoc E E₂ E₃).symm, left_inv := (_ : LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        ((e, f), g)‖ =
    ‖((e, f), g)‖
[PROOFSTEP]
simp only [LinearEquiv.coe_mk, Equiv.prodAssoc_apply, Prod.norm_def, max_assoc]
[GOAL]
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R₄ : Type u_4
E : Type u_5
E₂ : Type u_6
E₃ : Type u_7
E₄ : Type u_8
F : Type u_9
𝓕 : Type u_10
inst✝³⁶ : Semiring R
inst✝³⁵ : Semiring R₂
inst✝³⁴ : Semiring R₃
inst✝³³ : Semiring R₄
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
σ₁₃ : R →+* R₃
σ₃₁ : R₃ →+* R
σ₁₄ : R →+* R₄
σ₄₁ : R₄ →+* R
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
σ₂₄ : R₂ →+* R₄
σ₄₂ : R₄ →+* R₂
σ₃₄ : R₃ →+* R₄
σ₄₃ : R₄ →+* R₃
inst✝³² : RingHomInvPair σ₁₂ σ₂₁
inst✝³¹ : RingHomInvPair σ₂₁ σ₁₂
inst✝³⁰ : RingHomInvPair σ₁₃ σ₃₁
inst✝²⁹ : RingHomInvPair σ₃₁ σ₁₃
inst✝²⁸ : RingHomInvPair σ₂₃ σ₃₂
inst✝²⁷ : RingHomInvPair σ₃₂ σ₂₃
inst✝²⁶ : RingHomInvPair σ₁₄ σ₄₁
inst✝²⁵ : RingHomInvPair σ₄₁ σ₁₄
inst✝²⁴ : RingHomInvPair σ₂₄ σ₄₂
inst✝²³ : RingHomInvPair σ₄₂ σ₂₄
inst✝²² : RingHomInvPair σ₃₄ σ₄₃
inst✝²¹ : RingHomInvPair σ₄₃ σ₃₄
inst✝²⁰ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹⁹ : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄
inst✝¹⁸ : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄
inst✝¹⁷ : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
inst✝¹⁶ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
inst✝¹⁵ : RingHomCompTriple σ₄₂ σ₂₁ σ₄₁
inst✝¹⁴ : RingHomCompTriple σ₄₃ σ₃₂ σ₄₂
inst✝¹³ : RingHomCompTriple σ₄₃ σ₃₁ σ₄₁
inst✝¹² : SeminormedAddCommGroup E
inst✝¹¹ : SeminormedAddCommGroup E₂
inst✝¹⁰ : SeminormedAddCommGroup E₃
inst✝⁹ : SeminormedAddCommGroup E₄
inst✝⁸ : Module R E
inst✝⁷ : Module R₂ E₂
inst✝⁶ : Module R₃ E₃
inst✝⁵ : Module R₄ E₄
inst✝⁴ : NormedAddCommGroup F
inst✝³ : Module R F
e : E ≃ₛₗᵢ[σ₁₂] E₂
α : Type u_11
inst✝² : TopologicalSpace α
R' : Type u_12
inst✝¹ : Ring R'
inst✝ : Module R' E
p q : Submodule R' E
⊢ ofEq p p (_ : p = p) = refl R' { x // x ∈ p }
[PROOFSTEP]
funext
[GOAL]
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R₄ : Type u_4
E : Type u_5
E₂ : Type u_6
E₃ : Type u_7
E₄ : Type u_8
F : Type u_9
𝓕 : Type u_10
inst✝³⁶ : Semiring R
inst✝³⁵ : Semiring R₂
inst✝³⁴ : Semiring R₃
inst✝³³ : Semiring R₄
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
σ₁₃ : R →+* R₃
σ₃₁ : R₃ →+* R
σ₁₄ : R →+* R₄
σ₄₁ : R₄ →+* R
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
σ₂₄ : R₂ →+* R₄
σ₄₂ : R₄ →+* R₂
σ₃₄ : R₃ →+* R₄
σ₄₃ : R₄ →+* R₃
inst✝³² : RingHomInvPair σ₁₂ σ₂₁
inst✝³¹ : RingHomInvPair σ₂₁ σ₁₂
inst✝³⁰ : RingHomInvPair σ₁₃ σ₃₁
inst✝²⁹ : RingHomInvPair σ₃₁ σ₁₃
inst✝²⁸ : RingHomInvPair σ₂₃ σ₃₂
inst✝²⁷ : RingHomInvPair σ₃₂ σ₂₃
inst✝²⁶ : RingHomInvPair σ₁₄ σ₄₁
inst✝²⁵ : RingHomInvPair σ₄₁ σ₁₄
inst✝²⁴ : RingHomInvPair σ₂₄ σ₄₂
inst✝²³ : RingHomInvPair σ₄₂ σ₂₄
inst✝²² : RingHomInvPair σ₃₄ σ₄₃
inst✝²¹ : RingHomInvPair σ₄₃ σ₃₄
inst✝²⁰ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹⁹ : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄
inst✝¹⁸ : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄
inst✝¹⁷ : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
inst✝¹⁶ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
inst✝¹⁵ : RingHomCompTriple σ₄₂ σ₂₁ σ₄₁
inst✝¹⁴ : RingHomCompTriple σ₄₃ σ₃₂ σ₄₂
inst✝¹³ : RingHomCompTriple σ₄₃ σ₃₁ σ₄₁
inst✝¹² : SeminormedAddCommGroup E
inst✝¹¹ : SeminormedAddCommGroup E₂
inst✝¹⁰ : SeminormedAddCommGroup E₃
inst✝⁹ : SeminormedAddCommGroup E₄
inst✝⁸ : Module R E
inst✝⁷ : Module R₂ E₂
inst✝⁶ : Module R₃ E₃
inst✝⁵ : Module R₄ E₄
inst✝⁴ : NormedAddCommGroup F
inst✝³ : Module R F
e : E ≃ₛₗᵢ[σ₁₂] E₂
α : Type u_11
inst✝² : TopologicalSpace α
R' : Type u_12
inst✝¹ : Ring R'
inst✝ : Module R' E
p q : Submodule R' E
⊢ ofEq p p (_ : p = p) = refl R' { x // x ∈ p }
[PROOFSTEP]
rfl