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

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s t : Set α
x u v : Set (α × α)
⊢ Monotone fun x => thickening x s
Tactic:
intro u v huv
State after:
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s t : Set α
x u✝ v✝ u v : Set (α × α)
huv : u ≤ v
⊢ (fun x => thickening x s) u ≤ (fun x => thickening x s) v

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s t : Set α
x u✝ v✝ u v : Set (α × α)
huv : u ≤ v
⊢ (fun x => thickening x s) u ≤ (fun x => thickening x s) v
Tactic:
apply iUnion₂_mono
State after:
case h
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s t : Set α
x u✝ v✝ u v : Set (α × α)
huv : u ≤ v
⊢ ∀ i ∈ s, ball i u ⊆ ball i v

State before:
case h
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s t : Set α
x u✝ v✝ u v : Set (α × α)
huv : u ≤ v
⊢ ∀ i ∈ s, ball i u ⊆ ball i v
Tactic:
simp only [ball, le_eq_subset] at huv ⊢
State after:
case h
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s t : Set α
x u✝ v✝ u v : Set (α × α)
huv : u ⊆ v
⊢ ∀ i ∈ s, Prod.mk i ⁻¹' u ⊆ Prod.mk i ⁻¹' v

State before:
case h
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s t : Set α
x u✝ v✝ u v : Set (α × α)
huv : u ⊆ v
⊢ ∀ i ∈ s, Prod.mk i ⁻¹' u ⊆ Prod.mk i ⁻¹' v
Tactic:
exact λ _ _ => preimage_mono huv
State after:
no goals