Theorem: UniformSpace.thickening_inter_eq_empty_comm (RMT4/uniform.lean)

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s t : Set α
x u v : Set (α × α)
hu : SymmetricRel u
⊢ thickening u s ∩ t = ∅ ↔ s ∩ thickening u t = ∅
Tactic:
simp [thickening_inter_eq_empty, inter_comm s]
State after:
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s t : Set α
x u v : Set (α × α)
hu : SymmetricRel u
⊢ (∀ a ∈ s, ∀ b ∈ t, (a, b) ∉ u) ↔ ∀ a ∈ t, ∀ b ∈ s, (a, b) ∉ u

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s t : Set α
x u v : Set (α × α)
hu : SymmetricRel u
⊢ (∀ a ∈ s, ∀ b ∈ t, (a, b) ∉ u) ↔ ∀ a ∈ t, ∀ b ∈ s, (a, b) ∉ u
Tactic:
apply Iff.intro
State after:
case mp
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s t : Set α
x u v : Set (α × α)
hu : SymmetricRel u
⊢ (∀ a ∈ s, ∀ b ∈ t, (a, b) ∉ u) → ∀ a ∈ t, ∀ b ∈ s, (a, b) ∉ u

case mpr
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s t : Set α
x u v : Set (α × α)
hu : SymmetricRel u
⊢ (∀ a ∈ t, ∀ b ∈ s, (a, b) ∉ u) → ∀ a ∈ s, ∀ b ∈ t, (a, b) ∉ u

State before:
case mp
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s t : Set α
x u v : Set (α × α)
hu : SymmetricRel u
⊢ (∀ a ∈ s, ∀ b ∈ t, (a, b) ∉ u) → ∀ a ∈ t, ∀ b ∈ s, (a, b) ∉ u

case mpr
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s t : Set α
x u v : Set (α × α)
hu : SymmetricRel u
⊢ (∀ a ∈ t, ∀ b ∈ s, (a, b) ∉ u) → ∀ a ∈ s, ∀ b ∈ t, (a, b) ∉ u
Tactic:
repeat exact λ h a ha b hb hab => h b hb a ha (hu.mk_mem_comm.mp hab)
State after:
no goals

State before:
case mpr
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s t : Set α
x u v : Set (α × α)
hu : SymmetricRel u
⊢ (∀ a ∈ t, ∀ b ∈ s, (a, b) ∉ u) → ∀ a ∈ s, ∀ b ∈ t, (a, b) ∉ u
Tactic:
exact λ h a ha b hb hab => h b hb a ha (hu.mk_mem_comm.mp hab)
State after:
no goals