Theorem: LocallyLipschitz.ToSubset.compatible_with_nhds_within (Sard/LocallyLipschitz.lean)

State before:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
inst✝ : MetricSpace Z
t U : Set X
x : ↑U
hU : IsOpen U
ht : t ∈ 𝓝[U] ↑x
this : t ∩ U ∈ 𝓝 ↑x
⊢ t.toSubset U ∈ 𝓝 x
Tactic:
apply ToSubset.compatible_with_nhds
State after:
case ht
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
inst✝ : MetricSpace Z
t U : Set X
x : ↑U
hU : IsOpen U
ht : t ∈ 𝓝[U] ↑x
this : t ∩ U ∈ 𝓝 ↑x
⊢ t ∈ 𝓝 ↑x

State before:
case ht
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
inst✝ : MetricSpace Z
t U : Set X
x : ↑U
hU : IsOpen U
ht : t ∈ 𝓝[U] ↑x
this : t ∩ U ∈ 𝓝 ↑x
⊢ t ∈ 𝓝 ↑x
Tactic:
exact Filter.mem_of_superset this (inter_subset_left t U)
State after:
no goals

State before:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
inst✝ : MetricSpace Z
t U : Set X
x : ↑U
hU : IsOpen U
ht : t ∈ 𝓝[U] ↑x
⊢ t ∩ U ∈ 𝓝 ↑x
Tactic:
rcases ht with ⟨b, hb, U', hU', htaU⟩
State after:
case intro.intro.intro.intro
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
inst✝ : MetricSpace Z
t U : Set X
x : ↑U
hU : IsOpen U
b : Set X
hb : b ∈ 𝓝 ↑x
U' : Set X
hU' : U' ∈ Filter.principal U
htaU : t = b ∩ U'
⊢ t ∩ U ∈ 𝓝 ↑x

State before:
case intro.intro.intro.intro
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
inst✝ : MetricSpace Z
t U : Set X
x : ↑U
hU : IsOpen U
b : Set X
hb : b ∈ 𝓝 ↑x
U' : Set X
hU' : U' ∈ Filter.principal U
htaU : t = b ∩ U'
⊢ t ∩ U ∈ 𝓝 ↑x
Tactic:
rw [mem_nhds_iff] at hb
State after:
case intro.intro.intro.intro
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
inst✝ : MetricSpace Z
t U : Set X
x : ↑U
hU : IsOpen U
b : Set X
hb : ∃ t ⊆ b, IsOpen t ∧ ↑x ∈ t
U' : Set X
hU' : U' ∈ Filter.principal U
htaU : t = b ∩ U'
⊢ t ∩ U ∈ 𝓝 ↑x

State before:
case intro.intro.intro.intro
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
inst✝ : MetricSpace Z
t U : Set X
x : ↑U
hU : IsOpen U
b : Set X
hb : ∃ t ⊆ b, IsOpen t ∧ ↑x ∈ t
U' : Set X
hU' : U' ∈ Filter.principal U
htaU : t = b ∩ U'
⊢ t ∩ U ∈ 𝓝 ↑x
Tactic:
rcases hb with ⟨a, ha, haopen, hxa⟩
State after:
case intro.intro.intro.intro.intro.intro.intro
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
inst✝ : MetricSpace Z
t U : Set X
x : ↑U
hU : IsOpen U
b U' : Set X
hU' : U' ∈ Filter.principal U
htaU : t = b ∩ U'
a : Set X
ha : a ⊆ b
haopen : IsOpen a
hxa : ↑x ∈ a
⊢ t ∩ U ∈ 𝓝 ↑x

State before:
case intro.intro.intro.intro.intro.intro.intro
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
inst✝ : MetricSpace Z
t U : Set X
x : ↑U
hU : IsOpen U
b U' : Set X
hU' : U' ∈ Filter.principal U
htaU : t = b ∩ U'
a : Set X
ha : a ⊆ b
haopen : IsOpen a
hxa : ↑x ∈ a
⊢ t ∩ U ∈ 𝓝 ↑x
Tactic:
rw [mem_nhds_iff]
State after:
case intro.intro.intro.intro.intro.intro.intro
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
inst✝ : MetricSpace Z
t U : Set X
x : ↑U
hU : IsOpen U
b U' : Set X
hU' : U' ∈ Filter.principal U
htaU : t = b ∩ U'
a : Set X
ha : a ⊆ b
haopen : IsOpen a
hxa : ↑x ∈ a
⊢ ∃ t_1 ⊆ t ∩ U, IsOpen t_1 ∧ ↑x ∈ t_1

State before:
case intro.intro.intro.intro.intro.intro.intro
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
inst✝ : MetricSpace Z
t U : Set X
x : ↑U
hU : IsOpen U
b U' : Set X
hU' : U' ∈ Filter.principal U
htaU : t = b ∩ U'
a : Set X
ha : a ⊆ b
haopen : IsOpen a
hxa : ↑x ∈ a
⊢ ∃ t_1 ⊆ t ∩ U, IsOpen t_1 ∧ ↑x ∈ t_1
Tactic:
use a ∩ U
State after:
case h
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
inst✝ : MetricSpace Z
t U : Set X
x : ↑U
hU : IsOpen U
b U' : Set X
hU' : U' ∈ Filter.principal U
htaU : t = b ∩ U'
a : Set X
ha : a ⊆ b
haopen : IsOpen a
hxa : ↑x ∈ a
⊢ a ∩ U ⊆ t ∩ U ∧ IsOpen (a ∩ U) ∧ ↑x ∈ a ∩ U

State before:
case h
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
inst✝ : MetricSpace Z
t U : Set X
x : ↑U
hU : IsOpen U
b U' : Set X
hU' : U' ∈ Filter.principal U
htaU : t = b ∩ U'
a : Set X
ha : a ⊆ b
haopen : IsOpen a
hxa : ↑x ∈ a
⊢ a ∩ U ⊆ t ∩ U ∧ IsOpen (a ∩ U) ∧ ↑x ∈ a ∩ U
Tactic:
constructor
State after:
case h.left
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
inst✝ : MetricSpace Z
t U : Set X
x : ↑U
hU : IsOpen U
b U' : Set X
hU' : U' ∈ Filter.principal U
htaU : t = b ∩ U'
a : Set X
ha : a ⊆ b
haopen : IsOpen a
hxa : ↑x ∈ a
⊢ a ∩ U ⊆ t ∩ U

case h.right
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
inst✝ : MetricSpace Z
t U : Set X
x : ↑U
hU : IsOpen U
b U' : Set X
hU' : U' ∈ Filter.principal U
htaU : t = b ∩ U'
a : Set X
ha : a ⊆ b
haopen : IsOpen a
hxa : ↑x ∈ a
⊢ IsOpen (a ∩ U) ∧ ↑x ∈ a ∩ U

State before:
case h.left
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
inst✝ : MetricSpace Z
t U : Set X
x : ↑U
hU : IsOpen U
b U' : Set X
hU' : U' ∈ Filter.principal U
htaU : t = b ∩ U'
a : Set X
ha : a ⊆ b
haopen : IsOpen a
hxa : ↑x ∈ a
⊢ a ∩ U ⊆ t ∩ U
Tactic:
calc a ∩ U
  _ ⊆ b ∩ U := inter_subset_inter_left U ha
  _ = b ∩ (U' ∩ U) := by congr; apply (Set.inter_eq_right.mpr hU').symm
  _ ⊆ (b ∩ U') ∩ U := by rw [inter_assoc]
  _ = t ∩ U := by rw [htaU]
State after:
no goals

State before:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
inst✝ : MetricSpace Z
t U : Set X
x : ↑U
hU : IsOpen U
b U' : Set X
hU' : U' ∈ Filter.principal U
htaU : t = b ∩ U'
a : Set X
ha : a ⊆ b
haopen : IsOpen a
hxa : ↑x ∈ a
⊢ b ∩ U = b ∩ (U' ∩ U)
Tactic:
congr
State after:
case e_a
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
inst✝ : MetricSpace Z
t U : Set X
x : ↑U
hU : IsOpen U
b U' : Set X
hU' : U' ∈ Filter.principal U
htaU : t = b ∩ U'
a : Set X
ha : a ⊆ b
haopen : IsOpen a
hxa : ↑x ∈ a
⊢ U = U' ∩ U

State before:
case e_a
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
inst✝ : MetricSpace Z
t U : Set X
x : ↑U
hU : IsOpen U
b U' : Set X
hU' : U' ∈ Filter.principal U
htaU : t = b ∩ U'
a : Set X
ha : a ⊆ b
haopen : IsOpen a
hxa : ↑x ∈ a
⊢ U = U' ∩ U
Tactic:
apply (Set.inter_eq_right.mpr hU').symm
State after:
no goals

State before:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
inst✝ : MetricSpace Z
t U : Set X
x : ↑U
hU : IsOpen U
b U' : Set X
hU' : U' ∈ Filter.principal U
htaU : t = b ∩ U'
a : Set X
ha : a ⊆ b
haopen : IsOpen a
hxa : ↑x ∈ a
⊢ b ∩ (U' ∩ U) ⊆ b ∩ U' ∩ U
Tactic:
rw [inter_assoc]
State after:
no goals

State before:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
inst✝ : MetricSpace Z
t U : Set X
x : ↑U
hU : IsOpen U
b U' : Set X
hU' : U' ∈ Filter.principal U
htaU : t = b ∩ U'
a : Set X
ha : a ⊆ b
haopen : IsOpen a
hxa : ↑x ∈ a
⊢ b ∩ U' ∩ U = t ∩ U
Tactic:
rw [htaU]
State after:
no goals

State before:
case h.right
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
inst✝ : MetricSpace Z
t U : Set X
x : ↑U
hU : IsOpen U
b U' : Set X
hU' : U' ∈ Filter.principal U
htaU : t = b ∩ U'
a : Set X
ha : a ⊆ b
haopen : IsOpen a
hxa : ↑x ∈ a
⊢ IsOpen (a ∩ U) ∧ ↑x ∈ a ∩ U
Tactic:
exact ⟨IsOpen.inter haopen hU, ⟨hxa, Subtype.mem x⟩⟩
State after:
no goals