-- Mathlib/Topology/MetricSpace/Gluing.lean
theorem Sum.mem_uniformity (s : Set ((X ⊕ Y) × (X ⊕ Y))) :
    s ∈ 𝓤 (X ⊕ Y) ↔ ∃ ε > 0, ∀ a b, Sum.dist a b < ε → (a, b) ∈ s

Proof state:
case mpr.intro.intro
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
s : Set ((X ⊕ Y) × (X ⊕ Y))
ε : ℝ
ε0 : ε > 0
H : ∀ (a b : X ⊕ Y), Sum.dist a b < ε → (a, b) ∈ s
⊢ s ∈ 𝓤 (X ⊕ Y)

Tactic:
constructor <;> rw [Filter.mem_map, mem_uniformity_dist] <;> exact ⟨ε, ε0, fun _ _ h => H _ _ h⟩

Result:
no goals

Proof state:
case mp.intro.intro.intro.intro.intro.inr.inr
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
s : Set ((X ⊕ Y) × (X ⊕ Y))
hsX : s ∈ Filter.map (fun p => (Sum.inl p.1, Sum.inl p.2)) (𝓤 X)
hsY : s ∈ Filter.map (fun p => (Sum.inr p.1, Sum.inr p.2)) (𝓤 Y)
εX : ℝ
εX0 : εX > 0
hX : ∀ ⦃a b : X⦄, dist a b < εX → (a, b) ∈ (fun p => (Sum.inl p.1, Sum.inl p.2)) ⁻¹' s
εY : ℝ
εY0 : εY > 0
hY : ∀ ⦃a b : Y⦄, dist a b < εY → (a, b) ∈ (fun p => (Sum.inr p.1, Sum.inr p.2)) ⁻¹' s
a b : Y
h : Sum.dist (Sum.inr a) (Sum.inr b) < εX ⊓ εY ⊓ 1
⊢ (Sum.inr a, Sum.inr b) ∈ s

Tactic:
exact hY (lt_of_lt_of_le h (le_trans (min_le_left _ _) (min_le_right _ _)))

Result:
no goals

Proof state:
case mp.intro.intro.intro.intro.intro.inl.inl
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
s : Set ((X ⊕ Y) × (X ⊕ Y))
hsX : s ∈ Filter.map (fun p => (Sum.inl p.1, Sum.inl p.2)) (𝓤 X)
hsY : s ∈ Filter.map (fun p => (Sum.inr p.1, Sum.inr p.2)) (𝓤 Y)
εX : ℝ
εX0 : εX > 0
hX : ∀ ⦃a b : X⦄, dist a b < εX → (a, b) ∈ (fun p => (Sum.inl p.1, Sum.inl p.2)) ⁻¹' s
εY : ℝ
εY0 : εY > 0
hY : ∀ ⦃a b : Y⦄, dist a b < εY → (a, b) ∈ (fun p => (Sum.inr p.1, Sum.inr p.2)) ⁻¹' s
a b : X
h : Sum.dist (Sum.inl a) (Sum.inl b) < εX ⊓ εY ⊓ 1
⊢ (Sum.inl a, Sum.inl b) ∈ s

Tactic:
exact hX (lt_of_lt_of_le h (le_trans (min_le_left _ _) (min_le_left _ _)))

Result:
no goals

Proof state:
case mp.intro.intro.intro.intro.intro.inr.inl
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
s : Set ((X ⊕ Y) × (X ⊕ Y))
hsX : s ∈ Filter.map (fun p => (Sum.inl p.1, Sum.inl p.2)) (𝓤 X)
hsY : s ∈ Filter.map (fun p => (Sum.inr p.1, Sum.inr p.2)) (𝓤 Y)
εX : ℝ
εX0 : εX > 0
hX : ∀ ⦃a b : X⦄, dist a b < εX → (a, b) ∈ (fun p => (Sum.inl p.1, Sum.inl p.2)) ⁻¹' s
εY : ℝ
εY0 : εY > 0
hY : ∀ ⦃a b : Y⦄, dist a b < εY → (a, b) ∈ (fun p => (Sum.inr p.1, Sum.inr p.2)) ⁻¹' s
a : Y
b : X
h : Sum.dist (Sum.inr a) (Sum.inl b) < εX ⊓ εY ⊓ 1
⊢ (Sum.inr a, Sum.inl b) ∈ s

Tactic:
cases not_le_of_lt (lt_of_lt_of_le h (min_le_right _ _)) Sum.one_le_dist_inr_inl

Result:
no goals

Proof state:
case mp
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
s : Set ((X ⊕ Y) × (X ⊕ Y))
⊢ s ∈ 𝓤 (X ⊕ Y) → ∃ ε > 0, ∀ (a b : X ⊕ Y), Sum.dist a b < ε → (a, b) ∈ s

Tactic:
rintro ⟨hsX, hsY⟩

Result:
case mp.intro
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
s : Set ((X ⊕ Y) × (X ⊕ Y))
hsX : s ∈ Filter.map (fun p => (Sum.inl p.1, Sum.inl p.2)) (𝓤 X)
hsY : s ∈ Filter.map (fun p => (Sum.inr p.1, Sum.inr p.2)) (𝓤 Y)
⊢ ∃ ε > 0, ∀ (a b : X ⊕ Y), Sum.dist a b < ε → (a, b) ∈ s

Proof state:
case mp.intro.intro.intro.intro.intro
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
s : Set ((X ⊕ Y) × (X ⊕ Y))
hsX : s ∈ Filter.map (fun p => (Sum.inl p.1, Sum.inl p.2)) (𝓤 X)
hsY : s ∈ Filter.map (fun p => (Sum.inr p.1, Sum.inr p.2)) (𝓤 Y)
εX : ℝ
εX0 : εX > 0
hX : ∀ ⦃a b : X⦄, dist a b < εX → (a, b) ∈ (fun p => (Sum.inl p.1, Sum.inl p.2)) ⁻¹' s
εY : ℝ
εY0 : εY > 0
hY : ∀ ⦃a b : Y⦄, dist a b < εY → (a, b) ∈ (fun p => (Sum.inr p.1, Sum.inr p.2)) ⁻¹' s
⊢ ∀ (a b : X ⊕ Y), Sum.dist a b < εX ⊓ εY ⊓ 1 → (a, b) ∈ s

Tactic:
rintro (a | a) (b | b) h

Result:
case mp.intro.intro.intro.intro.intro.inl.inl
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
s : Set ((X ⊕ Y) × (X ⊕ Y))
hsX : s ∈ Filter.map (fun p => (Sum.inl p.1, Sum.inl p.2)) (𝓤 X)
hsY : s ∈ Filter.map (fun p => (Sum.inr p.1, Sum.inr p.2)) (𝓤 Y)
εX : ℝ
εX0 : εX > 0
hX : ∀ ⦃a b : X⦄, dist a b < εX → (a, b) ∈ (fun p => (Sum.inl p.1, Sum.inl p.2)) ⁻¹' s
εY : ℝ
εY0 : εY > 0
hY : ∀ ⦃a b : Y⦄, dist a b < εY → (a, b) ∈ (fun p => (Sum.inr p.1, Sum.inr p.2)) ⁻¹' s
a b : X
h : Sum.dist (Sum.inl a) (Sum.inl b) < εX ⊓ εY ⊓ 1
⊢ (Sum.inl a, Sum.inl b) ∈ s

case mp.intro.intro.intro.intro.intro.inl.inr
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
s : Set ((X ⊕ Y) × (X ⊕ Y))
hsX : s ∈ Filter.map (fun p => (Sum.inl p.1, Sum.inl p.2)) (𝓤 X)
hsY : s ∈ Filter.map (fun p => (Sum.inr p.1, Sum.inr p.2)) (𝓤 Y)
εX : ℝ
εX0 : εX > 0
hX : ∀ ⦃a b : X⦄, dist a b < εX → (a, b) ∈ (fun p => (Sum.inl p.1, Sum.inl p.2)) ⁻¹' s
εY : ℝ
εY0 : εY > 0
hY : ∀ ⦃a b : Y⦄, dist a b < εY → (a, b) ∈ (fun p => (Sum.inr p.1, Sum.inr p.2)) ⁻¹' s
a : X
b : Y
h : Sum.dist (Sum.inl a) (Sum.inr b) < εX ⊓ εY ⊓ 1
⊢ (Sum.inl a, Sum.inr b) ∈ s

case mp.intro.intro.intro.intro.intro.inr.inl
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
s : Set ((X ⊕ Y) × (X ⊕ Y))
hsX : s ∈ Filter.map (fun p => (Sum.inl p.1, Sum.inl p.2)) (𝓤 X)
hsY : s ∈ Filter.map (fun p => (Sum.inr p.1, Sum.inr p.2)) (𝓤 Y)
εX : ℝ
εX0 : εX > 0
hX : ∀ ⦃a b : X⦄, dist a b < εX → (a, b) ∈ (fun p => (Sum.inl p.1, Sum.inl p.2)) ⁻¹' s
εY : ℝ
εY0 : εY > 0
hY : ∀ ⦃a b : Y⦄, dist a b < εY → (a, b) ∈ (fun p => (Sum.inr p.1, Sum.inr p.2)) ⁻¹' s
a : Y
b : X
h : Sum.dist (Sum.inr a) (Sum.inl b) < εX ⊓ εY ⊓ 1
⊢ (Sum.inr a, Sum.inl b) ∈ s

case mp.intro.intro.intro.intro.intro.inr.inr
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
s : Set ((X ⊕ Y) × (X ⊕ Y))
hsX : s ∈ Filter.map (fun p => (Sum.inl p.1, Sum.inl p.2)) (𝓤 X)
hsY : s ∈ Filter.map (fun p => (Sum.inr p.1, Sum.inr p.2)) (𝓤 Y)
εX : ℝ
εX0 : εX > 0
hX : ∀ ⦃a b : X⦄, dist a b < εX → (a, b) ∈ (fun p => (Sum.inl p.1, Sum.inl p.2)) ⁻¹' s
εY : ℝ
εY0 : εY > 0
hY : ∀ ⦃a b : Y⦄, dist a b < εY → (a, b) ∈ (fun p => (Sum.inr p.1, Sum.inr p.2)) ⁻¹' s
a b : Y
h : Sum.dist (Sum.inr a) (Sum.inr b) < εX ⊓ εY ⊓ 1
⊢ (Sum.inr a, Sum.inr b) ∈ s

Proof state:
case mp.intro.intro.intro
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
s : Set ((X ⊕ Y) × (X ⊕ Y))
hsX : s ∈ Filter.map (fun p => (Sum.inl p.1, Sum.inl p.2)) (𝓤 X)
hsY : s ∈ Filter.map (fun p => (Sum.inr p.1, Sum.inr p.2)) (𝓤 Y)
εX : ℝ
εX0 : εX > 0
hX : ∀ ⦃a b : X⦄, dist a b < εX → (a, b) ∈ (fun p => (Sum.inl p.1, Sum.inl p.2)) ⁻¹' s
⊢ ∃ ε > 0, ∀ (a b : X ⊕ Y), Sum.dist a b < ε → (a, b) ∈ s

Tactic:
rcases mem_uniformity_dist.1 hsY with ⟨εY, εY0, hY⟩

Result:
case mp.intro.intro.intro.intro.intro
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
s : Set ((X ⊕ Y) × (X ⊕ Y))
hsX : s ∈ Filter.map (fun p => (Sum.inl p.1, Sum.inl p.2)) (𝓤 X)
hsY : s ∈ Filter.map (fun p => (Sum.inr p.1, Sum.inr p.2)) (𝓤 Y)
εX : ℝ
εX0 : εX > 0
hX : ∀ ⦃a b : X⦄, dist a b < εX → (a, b) ∈ (fun p => (Sum.inl p.1, Sum.inl p.2)) ⁻¹' s
εY : ℝ
εY0 : εY > 0
hY : ∀ ⦃a b : Y⦄, dist a b < εY → (a, b) ∈ (fun p => (Sum.inr p.1, Sum.inr p.2)) ⁻¹' s
⊢ ∃ ε > 0, ∀ (a b : X ⊕ Y), Sum.dist a b < ε → (a, b) ∈ s

Proof state:
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
s : Set ((X ⊕ Y) × (X ⊕ Y))
⊢ s ∈ 𝓤 (X ⊕ Y) ↔ ∃ ε > 0, ∀ (a b : X ⊕ Y), Sum.dist a b < ε → (a, b) ∈ s

Tactic:
constructor

Result:
case mp
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
s : Set ((X ⊕ Y) × (X ⊕ Y))
⊢ s ∈ 𝓤 (X ⊕ Y) → ∃ ε > 0, ∀ (a b : X ⊕ Y), Sum.dist a b < ε → (a, b) ∈ s

case mpr
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
s : Set ((X ⊕ Y) × (X ⊕ Y))
⊢ (∃ ε > 0, ∀ (a b : X ⊕ Y), Sum.dist a b < ε → (a, b) ∈ s) → s ∈ 𝓤 (X ⊕ Y)