-- Mathlib/Topology/MetricSpace/Pseudo/Pi.lean
/-- A sphere in a product space is a union of spheres on each component restricted to the closed
ball. -/
lemma sphere_pi (x : ∀ b, π b) {r : ℝ} (h : 0 < r ∨ Nonempty β) :
    sphere x r = (⋃ i : β, Function.eval i ⁻¹' sphere (x i) r) ∩ closedBall x r

Proof state:
case inr.inl
β : Type u_2
π : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (π b)
x✝ : (b : β) → π b
h : 0 < 0 ∨ Nonempty β
this : Nonempty β := Or.resolve_left h (lt_irrefl 0)
inhabited_h : Inhabited β
x : (x : β) → π x
hx : dist x x✝ ≤ 0
⊢ x ∈ Function.eval default ⁻¹' sphere (x✝ default) 0

Tactic:
rw [dist_pi_le_iff le_rfl] at hx

Result:
case inr.inl
β : Type u_2
π : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (π b)
x✝ : (b : β) → π b
h : 0 < 0 ∨ Nonempty β
this : Nonempty β := Or.resolve_left h (lt_irrefl 0)
inhabited_h : Inhabited β
x : (x : β) → π x
hx : ∀ (b : β), dist (x b) (x✝ b) ≤ 0
⊢ x ∈ Function.eval default ⁻¹' sphere (x✝ default) 0

Proof state:
case inl
β : Type u_2
π : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (π b)
x : (b : β) → π b
r : ℝ
h : 0 < r ∨ Nonempty β
hr : r < 0
⊢ sphere x r = (⋃ i, Function.eval i ⁻¹' sphere (x i) r) ∩ closedBall x r

Tactic:
simp [hr]

Result:
no goals

Proof state:
β : Type u_2
π : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (π b)
x : (b : β) → π b
r : ℝ
h : 0 < r ∨ Nonempty β
⊢ sphere x r = (⋃ i, Function.eval i ⁻¹' sphere (x i) r) ∩ closedBall x r

Tactic:
obtain hr | rfl | hr := lt_trichotomy r 0

Result:
case inl
β : Type u_2
π : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (π b)
x : (b : β) → π b
r : ℝ
h : 0 < r ∨ Nonempty β
hr : r < 0
⊢ sphere x r = (⋃ i, Function.eval i ⁻¹' sphere (x i) r) ∩ closedBall x r

case inr.inl
β : Type u_2
π : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (π b)
x : (b : β) → π b
h : 0 < 0 ∨ Nonempty β
⊢ sphere x 0 = (⋃ i, Function.eval i ⁻¹' sphere (x i) 0) ∩ closedBall x 0

case inr.inr
β : Type u_2
π : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (π b)
x : (b : β) → π b
r : ℝ
h : 0 < r ∨ Nonempty β
hr : 0 < r
⊢ sphere x r = (⋃ i, Function.eval i ⁻¹' sphere (x i) r) ∩ closedBall x r

Proof state:
case inr.inl
β : Type u_2
π : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (π b)
x : (b : β) → π b
h : 0 < 0 ∨ Nonempty β
⊢ sphere x 0 = (⋃ i, Function.eval i ⁻¹' sphere (x i) 0) ∩ closedBall x 0

Tactic:
rw [closedBall_eq_sphere_of_nonpos le_rfl, eq_comm, Set.inter_eq_right]

Result:
case inr.inl
β : Type u_2
π : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (π b)
x : (b : β) → π b
h : 0 < 0 ∨ Nonempty β
⊢ sphere x 0 ⊆ ⋃ i, Function.eval i ⁻¹' sphere (x i) 0

Proof state:
case inr.inl
β : Type u_2
π : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (π b)
x : (b : β) → π b
h : 0 < 0 ∨ Nonempty β
this : Nonempty β := Or.resolve_left h (lt_irrefl 0)
⊢ sphere x 0 ⊆ ⋃ i, Function.eval i ⁻¹' sphere (x i) 0

Tactic:
inhabit β

Result:
case inr.inl
β : Type u_2
π : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (π b)
x : (b : β) → π b
h : 0 < 0 ∨ Nonempty β
this : Nonempty β := Or.resolve_left h (lt_irrefl 0)
inhabited_h : Inhabited β
⊢ sphere x 0 ⊆ ⋃ i, Function.eval i ⁻¹' sphere (x i) 0

Proof state:
case inr.inl
β : Type u_2
π : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (π b)
x : (b : β) → π b
h : 0 < 0 ∨ Nonempty β
this : Nonempty β := Or.resolve_left h (lt_irrefl 0)
inhabited_h : Inhabited β
⊢ sphere x 0 ⊆ Function.eval default ⁻¹' sphere (x default) 0

Tactic:
intro x hx

Result:
case inr.inl
β : Type u_2
π : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (π b)
x✝ : (b : β) → π b
h : 0 < 0 ∨ Nonempty β
this : Nonempty β := Or.resolve_left h (lt_irrefl 0)
inhabited_h : Inhabited β
x : (x : β) → π x
hx : x ∈ sphere x✝ 0
⊢ x ∈ Function.eval default ⁻¹' sphere (x✝ default) 0

Proof state:
case inr.inl
β : Type u_2
π : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (π b)
x : (b : β) → π b
h : 0 < 0 ∨ Nonempty β
this : Nonempty β := Or.resolve_left h (lt_irrefl 0)
inhabited_h : Inhabited β
⊢ sphere x 0 ⊆ ⋃ i, Function.eval i ⁻¹' sphere (x i) 0

Tactic:
refine subset_iUnion_of_subset default ?_

Result:
case inr.inl
β : Type u_2
π : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (π b)
x : (b : β) → π b
h : 0 < 0 ∨ Nonempty β
this : Nonempty β := Or.resolve_left h (lt_irrefl 0)
inhabited_h : Inhabited β
⊢ sphere x 0 ⊆ Function.eval default ⁻¹' sphere (x default) 0

Proof state:
case inr.inl
β : Type u_2
π : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (π b)
x : (b : β) → π b
h : 0 < 0 ∨ Nonempty β
⊢ sphere x 0 ⊆ ⋃ i, Function.eval i ⁻¹' sphere (x i) 0

Tactic:
letI := h.resolve_left (lt_irrefl _)

Result:
case inr.inl
β : Type u_2
π : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (π b)
x : (b : β) → π b
h : 0 < 0 ∨ Nonempty β
this : Nonempty β := Or.resolve_left h (lt_irrefl 0)
⊢ sphere x 0 ⊆ ⋃ i, Function.eval i ⁻¹' sphere (x i) 0

Proof state:
case inr.inl
β : Type u_2
π : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (π b)
x✝ : (b : β) → π b
h : 0 < 0 ∨ Nonempty β
this : Nonempty β := Or.resolve_left h (lt_irrefl 0)
inhabited_h : Inhabited β
x : (x : β) → π x
hx : x ∈ sphere x✝ 0
⊢ x ∈ Function.eval default ⁻¹' sphere (x✝ default) 0

Tactic:
replace hx := hx.le

Result:
case inr.inl
β : Type u_2
π : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (π b)
x✝ : (b : β) → π b
h : 0 < 0 ∨ Nonempty β
this : Nonempty β := Or.resolve_left h (lt_irrefl 0)
inhabited_h : Inhabited β
x : (x : β) → π x
hx : dist x x✝ ≤ 0
⊢ x ∈ Function.eval default ⁻¹' sphere (x✝ default) 0

Proof state:
case inr.inl
β : Type u_2
π : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (π b)
x✝ : (b : β) → π b
h : 0 < 0 ∨ Nonempty β
this : Nonempty β := Or.resolve_left h (lt_irrefl 0)
inhabited_h : Inhabited β
x : (x : β) → π x
hx : ∀ (b : β), dist (x b) (x✝ b) ≤ 0
⊢ x ∈ Function.eval default ⁻¹' sphere (x✝ default) 0

Tactic:
exact le_antisymm (hx default) dist_nonneg

Result:
no goals

Proof state:
case inr.inr.h
β : Type u_2
π : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (π b)
x : (b : β) → π b
r : ℝ
h : 0 < r ∨ Nonempty β
hr : 0 < r
x✝ : (b : β) → π b
⊢ x✝ ∈ sphere x r ↔ x✝ ∈ (⋃ i, Function.eval i ⁻¹' sphere (x i) r) ∩ closedBall x r

Tactic:
simp [dist_pi_eq_iff hr, dist_pi_le_iff hr.le]

Result:
no goals

Proof state:
case inr.inr
β : Type u_2
π : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (π b)
x : (b : β) → π b
r : ℝ
h : 0 < r ∨ Nonempty β
hr : 0 < r
⊢ sphere x r = (⋃ i, Function.eval i ⁻¹' sphere (x i) r) ∩ closedBall x r

Tactic:
ext

Result:
case inr.inr.h
β : Type u_2
π : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (π b)
x : (b : β) → π b
r : ℝ
h : 0 < r ∨ Nonempty β
hr : 0 < r
x✝ : (b : β) → π b
⊢ x✝ ∈ sphere x r ↔ x✝ ∈ (⋃ i, Function.eval i ⁻¹' sphere (x i) r) ∩ closedBall x r