case h₀
R : Type ?u.865125
R' : Type ?u.865128
𝕜 : Type u_1
𝕜₂ : Type ?u.865134
𝕜₃ : Type ?u.865137
𝕝 : Type ?u.865140
E : Type u_2
E₂ : Type ?u.865146
E₃ : Type ?u.865149
F : Type ?u.865152
G : Type ?u.865155
ι : Type u_3
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
p✝ : Seminorm 𝕜 E
x y : E
r✝ : ℝ
p : ι → Seminorm 𝕜 E
s : Finset ι
e : E
r : ℝ
a : ι
⊢ ball (Finset.sup' {a} (_ : Finset.Nonempty {a}) p) e r =
    Finset.inf' {a} (_ : Finset.Nonempty {a}) fun i => ball (p i) e r

case h₁
R : Type ?u.865125
R' : Type ?u.865128
𝕜 : Type u_1
𝕜₂ : Type ?u.865134
𝕜₃ : Type ?u.865137
𝕝 : Type ?u.865140
E : Type u_2
E₂ : Type ?u.865146
E₃ : Type ?u.865149
F : Type ?u.865152
G : Type ?u.865155
ι : Type u_3
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
p✝ : Seminorm 𝕜 E
x y : E
r✝ : ℝ
p : ι → Seminorm 𝕜 E
s✝ : Finset ι
e : E
r : ℝ
a : ι
s : Finset ι
ha : ¬a ∈ s
hs : Finset.Nonempty s
ih : ball (Finset.sup' s hs p) e r = Finset.inf' s hs fun i => ball (p i) e r
⊢ ball (Finset.sup' (Finset.cons a s ha) (_ : Finset.Nonempty (Finset.cons a s ha)) p) e r =
    Finset.inf' (Finset.cons a s ha) (_ : Finset.Nonempty (Finset.cons a s ha)) fun i => ball (p i) e r
R : Type ?u.865125
R' : Type ?u.865128
𝕜 : Type u_1
𝕜₂ : Type ?u.865134
𝕜₃ : Type ?u.865137
𝕝 : Type ?u.865140
E : Type u_2
E₂ : Type ?u.865146
E₃ : Type ?u.865149
F : Type ?u.865152
G : Type ?u.865155
ι : Type u_3
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
p✝ : Seminorm 𝕜 E
x y : E
r✝ : ℝ
p : ι → Seminorm 𝕜 E
s : Finset ι
H : Finset.Nonempty s
e : E
r : ℝ
⊢ ball (Finset.sup' s H p) e r = Finset.inf' s H fun i => ball (p i) e r
induction' H using Finset.Nonempty.cons_induction with a a s ha hs ih
no goals
case h₀
R : Type ?u.865125
R' : Type ?u.865128
𝕜 : Type u_1
𝕜₂ : Type ?u.865134
𝕜₃ : Type ?u.865137
𝕝 : Type ?u.865140
E : Type u_2
E₂ : Type ?u.865146
E₃ : Type ?u.865149
F : Type ?u.865152
G : Type ?u.865155
ι : Type u_3
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
p✝ : Seminorm 𝕜 E
x y : E
r✝ : ℝ
p : ι → Seminorm 𝕜 E
s : Finset ι
e : E
r : ℝ
a : ι
⊢ ball (Finset.sup' {a} (_ : Finset.Nonempty {a}) p) e r =
    Finset.inf' {a} (_ : Finset.Nonempty {a}) fun i => ball (p i) e r
classical simp
no goals
case h₀
R : Type ?u.865125
R' : Type ?u.865128
𝕜 : Type u_1
𝕜₂ : Type ?u.865134
𝕜₃ : Type ?u.865137
𝕝 : Type ?u.865140
E : Type u_2
E₂ : Type ?u.865146
E₃ : Type ?u.865149
F : Type ?u.865152
G : Type ?u.865155
ι : Type u_3
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
p✝ : Seminorm 𝕜 E
x y : E
r✝ : ℝ
p : ι → Seminorm 𝕜 E
s : Finset ι
e : E
r : ℝ
a : ι
⊢ ball (Finset.sup' {a} (_ : Finset.Nonempty {a}) p) e r =
    Finset.inf' {a} (_ : Finset.Nonempty {a}) fun i => ball (p i) e r
simp
case h₁
R : Type ?u.865125
R' : Type ?u.865128
𝕜 : Type u_1
𝕜₂ : Type ?u.865134
𝕜₃ : Type ?u.865137
𝕝 : Type ?u.865140
E : Type u_2
E₂ : Type ?u.865146
E₃ : Type ?u.865149
F : Type ?u.865152
G : Type ?u.865155
ι : Type u_3
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
p✝ : Seminorm 𝕜 E
x y : E
r✝ : ℝ
p : ι → Seminorm 𝕜 E
s✝ : Finset ι
e : E
r : ℝ
a : ι
s : Finset ι
ha : ¬a ∈ s
hs : Finset.Nonempty s
ih : ball (Finset.sup' s hs p) e r = Finset.inf' s hs fun i => ball (p i) e r
⊢ ball (p a) e r ∩ ball (Finset.sup' s hs p) e r = ball (p a) e r ⊓ Finset.inf' s hs fun i => ball (p i) e r
case h₁
R : Type ?u.865125
R' : Type ?u.865128
𝕜 : Type u_1
𝕜₂ : Type ?u.865134
𝕜₃ : Type ?u.865137
𝕝 : Type ?u.865140
E : Type u_2
E₂ : Type ?u.865146
E₃ : Type ?u.865149
F : Type ?u.865152
G : Type ?u.865155
ι : Type u_3
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
p✝ : Seminorm 𝕜 E
x y : E
r✝ : ℝ
p : ι → Seminorm 𝕜 E
s✝ : Finset ι
e : E
r : ℝ
a : ι
s : Finset ι
ha : ¬a ∈ s
hs : Finset.Nonempty s
ih : ball (Finset.sup' s hs p) e r = Finset.inf' s hs fun i => ball (p i) e r
⊢ ball (Finset.sup' (Finset.cons a s ha) (_ : Finset.Nonempty (Finset.cons a s ha)) p) e r =
    Finset.inf' (Finset.cons a s ha) (_ : Finset.Nonempty (Finset.cons a s ha)) fun i => ball (p i) e r
rw [Finset.sup'_cons hs, Finset.inf'_cons hs, ball_sup]
no goals
case h₁
R : Type ?u.865125
R' : Type ?u.865128
𝕜 : Type u_1
𝕜₂ : Type ?u.865134
𝕜₃ : Type ?u.865137
𝕝 : Type ?u.865140
E : Type u_2
E₂ : Type ?u.865146
E₃ : Type ?u.865149
F : Type ?u.865152
G : Type ?u.865155
ι : Type u_3
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
p✝ : Seminorm 𝕜 E
x y : E
r✝ : ℝ
p : ι → Seminorm 𝕜 E
s✝ : Finset ι
e : E
r : ℝ
a : ι
s : Finset ι
ha : ¬a ∈ s
hs : Finset.Nonempty s
ih : ball (Finset.sup' s hs p) e r = Finset.inf' s hs fun i => ball (p i) e r
⊢ ball (p a) e r ∩ ball (Finset.sup' s hs p) e r = ball (p a) e r ⊓ Finset.inf' s hs fun i => ball (p i) e r
simp only [inf_eq_inter, ih]