case mk
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.56107
inst✝ : UniformSpace α
V W M : Set (β × β)
hW' : SymmetricRel W
x y : β
⊢ (x, y) ∈ V ○ M ○ W ↔ Set.Nonempty (ball (x, y).fst V ×ˢ ball (x, y).snd W ∩ M)
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.56107
inst✝ : UniformSpace α
V W M : Set (β × β)
hW' : SymmetricRel W
p : β × β
⊢ p ∈ V ○ M ○ W ↔ Set.Nonempty (ball p.fst V ×ˢ ball p.snd W ∩ M)
cases' p with x y
case mk.mp
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.56107
inst✝ : UniformSpace α
V W M : Set (β × β)
hW' : SymmetricRel W
x y : β
⊢ (x, y) ∈ V ○ M ○ W → Set.Nonempty (ball (x, y).fst V ×ˢ ball (x, y).snd W ∩ M)

case mk.mpr
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.56107
inst✝ : UniformSpace α
V W M : Set (β × β)
hW' : SymmetricRel W
x y : β
⊢ Set.Nonempty (ball (x, y).fst V ×ˢ ball (x, y).snd W ∩ M) → (x, y) ∈ V ○ M ○ W
case mk
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.56107
inst✝ : UniformSpace α
V W M : Set (β × β)
hW' : SymmetricRel W
x y : β
⊢ (x, y) ∈ V ○ M ○ W ↔ Set.Nonempty (ball (x, y).fst V ×ˢ ball (x, y).snd W ∩ M)
constructor
case mk.mp.intro.intro.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.56107
inst✝ : UniformSpace α
V W M : Set (β × β)
hW' : SymmetricRel W
x y z : β
hzy : (z, (x, y).snd) ∈ W
w : β
hpw : (((x, y).fst, z).fst, w) ∈ V
hwz : (w, ((x, y).fst, z).snd) ∈ M
⊢ Set.Nonempty (ball (x, y).fst V ×ˢ ball (x, y).snd W ∩ M)
case mk.mp
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.56107
inst✝ : UniformSpace α
V W M : Set (β × β)
hW' : SymmetricRel W
x y : β
⊢ (x, y) ∈ V ○ M ○ W → Set.Nonempty (ball (x, y).fst V ×ˢ ball (x, y).snd W ∩ M)
rintro ⟨z, ⟨w, hpw, hwz⟩, hzy⟩
no goals
case mk.mp.intro.intro.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.56107
inst✝ : UniformSpace α
V W M : Set (β × β)
hW' : SymmetricRel W
x y z : β
hzy : (z, (x, y).snd) ∈ W
w : β
hpw : (((x, y).fst, z).fst, w) ∈ V
hwz : (w, ((x, y).fst, z).snd) ∈ M
⊢ Set.Nonempty (ball (x, y).fst V ×ˢ ball (x, y).snd W ∩ M)
exact ⟨(w, z), ⟨hpw, by rwa [mem_ball_symmetry hW']⟩, hwz⟩
no goals
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.56107
inst✝ : UniformSpace α
V W M : Set (β × β)
hW' : SymmetricRel W
x y z : β
hzy : (z, (x, y).snd) ∈ W
w : β
hpw : (((x, y).fst, z).fst, w) ∈ V
hwz : (w, ((x, y).fst, z).snd) ∈ M
⊢ (w, z).snd ∈ ball (x, y).snd W
rwa [mem_ball_symmetry hW']
case mk.mpr.intro.mk.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.56107
inst✝ : UniformSpace α
V W M : Set (β × β)
hW' : SymmetricRel W
x y w z : β
hwz : (w, z) ∈ M
w_in : (w, z).fst ∈ ball (x, y).fst V
z_in : (w, z).snd ∈ ball (x, y).snd W
⊢ (x, y) ∈ V ○ M ○ W
case mk.mpr
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.56107
inst✝ : UniformSpace α
V W M : Set (β × β)
hW' : SymmetricRel W
x y : β
⊢ Set.Nonempty (ball (x, y).fst V ×ˢ ball (x, y).snd W ∩ M) → (x, y) ∈ V ○ M ○ W
rintro ⟨⟨w, z⟩, ⟨w_in, z_in⟩, hwz⟩
case mk.mpr.intro.mk.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.56107
inst✝ : UniformSpace α
V W M : Set (β × β)
hW' : SymmetricRel W
x y w z : β
hwz : (w, z) ∈ M
w_in : (w, z).fst ∈ ball (x, y).fst V
z_in : (x, y).snd ∈ ball (w, z).snd W
⊢ (x, y) ∈ V ○ M ○ W
case mk.mpr.intro.mk.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.56107
inst✝ : UniformSpace α
V W M : Set (β × β)
hW' : SymmetricRel W
x y w z : β
hwz : (w, z) ∈ M
w_in : (w, z).fst ∈ ball (x, y).fst V
z_in : (w, z).snd ∈ ball (x, y).snd W
⊢ (x, y) ∈ V ○ M ○ W
rw [mem_ball_symmetry hW'] at z_in
no goals
case mk.mpr.intro.mk.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.56107
inst✝ : UniformSpace α
V W M : Set (β × β)
hW' : SymmetricRel W
x y w z : β
hwz : (w, z) ∈ M
w_in : (w, z).fst ∈ ball (x, y).fst V
z_in : (x, y).snd ∈ ball (w, z).snd W
⊢ (x, y) ∈ V ○ M ○ W
exact ⟨z, ⟨w, w_in, hwz⟩, z_in⟩