Theorem: local_homeo_preserves_empty_interior (Sard/ObsoleteHelpers.lean)

State before:
α β : Type
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : PartialHomeomorph α β
s : Set α
hs : s ⊆ f.source
h₂s : interior s = ∅
⊢ interior (↑f '' s) = ∅
Tactic:
have h₁ : s = s ∩ f.source := by
  rw [← @inter_eq_left α s f.source] at hs
  symm
  exact hs
State after:
α β : Type
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : PartialHomeomorph α β
s : Set α
hs : s ⊆ f.source
h₂s : interior s = ∅
h₁ : s = s ∩ f.source
⊢ interior (↑f '' s) = ∅

State before:
α β : Type
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : PartialHomeomorph α β
s : Set α
hs : s ⊆ f.source
h₂s : interior s = ∅
h₁ : s = s ∩ f.source
⊢ interior (↑f '' s) = ∅
Tactic:
have h₂ : interior s = interior (s ∩ f.source) := by
  sorry
State after:
α β : Type
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : PartialHomeomorph α β
s : Set α
hs : s ⊆ f.source
h₂s : interior s = ∅
h₁ : s = s ∩ f.source
h₂ : interior s = interior (s ∩ f.source)
⊢ interior (↑f '' s) = ∅

State before:
α β : Type
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : PartialHomeomorph α β
s : Set α
hs : s ⊆ f.source
h₂s : interior s = ∅
h₁ : s = s ∩ f.source
h₂ : interior s = interior (s ∩ f.source)
⊢ interior (↑f '' s) = ∅
Tactic:
rw [h₁] at h₂s
State after:
α β : Type
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : PartialHomeomorph α β
s : Set α
hs : s ⊆ f.source
h₂s : interior (s ∩ f.source) = ∅
h₁ : s = s ∩ f.source
h₂ : interior s = interior (s ∩ f.source)
⊢ interior (↑f '' s) = ∅

State before:
α β : Type
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : PartialHomeomorph α β
s : Set α
hs : s ⊆ f.source
h₂s : interior (s ∩ f.source) = ∅
h₁ : s = s ∩ f.source
h₂ : interior s = interior (s ∩ f.source)
⊢ interior (↑f '' s) = ∅
Tactic:
have h₃ : f '' (interior s ∩ f.source) = ∅ := by sorry
State after:
α β : Type
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : PartialHomeomorph α β
s : Set α
hs : s ⊆ f.source
h₂s : interior (s ∩ f.source) = ∅
h₁ : s = s ∩ f.source
h₂ : interior s = interior (s ∩ f.source)
h₃ : ↑f '' (interior s ∩ f.source) = ∅
⊢ interior (↑f '' s) = ∅

State before:
α β : Type
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : PartialHomeomorph α β
s : Set α
hs : s ⊆ f.source
h₂s : interior (s ∩ f.source) = ∅
h₁ : s = s ∩ f.source
h₂ : interior s = interior (s ∩ f.source)
h₃ : ↑f '' (interior s ∩ f.source) = ∅
⊢ interior (↑f '' s) = ∅
Tactic:
sorry
State after:
no goals

State before:
α β : Type
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : PartialHomeomorph α β
s : Set α
hs : s ⊆ f.source
h₂s : interior s = ∅
⊢ s = s ∩ f.source
Tactic:
rw [← @inter_eq_left α s f.source] at hs
State after:
α β : Type
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : PartialHomeomorph α β
s : Set α
hs : s ∩ f.source = s
h₂s : interior s = ∅
⊢ s = s ∩ f.source

State before:
α β : Type
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : PartialHomeomorph α β
s : Set α
hs : s ∩ f.source = s
h₂s : interior s = ∅
⊢ s = s ∩ f.source
Tactic:
symm
State after:
α β : Type
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : PartialHomeomorph α β
s : Set α
hs : s ∩ f.source = s
h₂s : interior s = ∅
⊢ s ∩ f.source = s

State before:
α β : Type
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : PartialHomeomorph α β
s : Set α
hs : s ∩ f.source = s
h₂s : interior s = ∅
⊢ s ∩ f.source = s
Tactic:
exact hs
State after:
no goals

State before:
α β : Type
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : PartialHomeomorph α β
s : Set α
hs : s ⊆ f.source
h₂s : interior s = ∅
h₁ : s = s ∩ f.source
⊢ interior s = interior (s ∩ f.source)
Tactic:
sorry
State after:
no goals

State before:
α β : Type
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : PartialHomeomorph α β
s : Set α
hs : s ⊆ f.source
h₂s : interior (s ∩ f.source) = ∅
h₁ : s = s ∩ f.source
h₂ : interior s = interior (s ∩ f.source)
⊢ ↑f '' (interior s ∩ f.source) = ∅
Tactic:
sorry
State after:
no goals