Theorem: IsPathConnected.of_frontier (Ray/Misc/Connected.lean)

State before:
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
⊢ IsPathConnected (f ⁻¹' s)
Tactic:
have pc' := pc
State after:
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
pc' : IsPathConnected (f ⁻¹' frontier s)
⊢ IsPathConnected (f ⁻¹' s)

State before:
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
pc' : IsPathConnected (f ⁻¹' frontier s)
⊢ IsPathConnected (f ⁻¹' s)
Tactic:
rcases pc' with ⟨b, fb, j⟩
State after:
case intro.intro
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : b ∈ f ⁻¹' frontier s
j : ∀ {y : X}, y ∈ f ⁻¹' frontier s → JoinedIn (f ⁻¹' frontier s) b y
⊢ IsPathConnected (f ⁻¹' s)

State before:
case intro.intro
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : b ∈ f ⁻¹' frontier s
j : ∀ {y : X}, y ∈ f ⁻¹' frontier s → JoinedIn (f ⁻¹' frontier s) b y
⊢ IsPathConnected (f ⁻¹' s)
Tactic:
use b
State after:
case h
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : b ∈ f ⁻¹' frontier s
j : ∀ {y : X}, y ∈ f ⁻¹' frontier s → JoinedIn (f ⁻¹' frontier s) b y
⊢ b ∈ f ⁻¹' s ∧ ∀ {y : X}, y ∈ f ⁻¹' s → JoinedIn (f ⁻¹' s) b y

State before:
case h
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : b ∈ f ⁻¹' frontier s
j : ∀ {y : X}, y ∈ f ⁻¹' frontier s → JoinedIn (f ⁻¹' frontier s) b y
⊢ b ∈ f ⁻¹' s ∧ ∀ {y : X}, y ∈ f ⁻¹' s → JoinedIn (f ⁻¹' s) b y
Tactic:
simp only [mem_preimage, mem_singleton_iff] at fb j ⊢
State after:
case h
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
⊢ f b ∈ s ∧ ∀ {y : X}, f y ∈ s → JoinedIn (f ⁻¹' s) b y

State before:
case h
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
⊢ f b ∈ s ∧ ∀ {y : X}, f y ∈ s → JoinedIn (f ⁻¹' s) b y
Tactic:
have bs : f b ∈ s := sc.frontier_subset fb
State after:
case h
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
⊢ f b ∈ s ∧ ∀ {y : X}, f y ∈ s → JoinedIn (f ⁻¹' s) b y

State before:
case h
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
⊢ f b ∈ s ∧ ∀ {y : X}, f y ∈ s → JoinedIn (f ⁻¹' s) b y
Tactic:
use bs
State after:
case right
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
⊢ ∀ {y : X}, f y ∈ s → JoinedIn (f ⁻¹' s) b y

State before:
case right
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
⊢ ∀ {y : X}, f y ∈ s → JoinedIn (f ⁻¹' s) b y
Tactic:
intro x fx
State after:
case right
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
⊢ JoinedIn (f ⁻¹' s) b x

State before:
case right
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
⊢ JoinedIn (f ⁻¹' s) b x
Tactic:
have p := PathConnectedSpace.somePath x b
State after:
case right
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
⊢ JoinedIn (f ⁻¹' s) b x

State before:
case right
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
⊢ JoinedIn (f ⁻¹' s) b x
Tactic:
generalize hu : Icc (0 : ℝ) 1 ∩ ⋂ (a) (_ : f (p.extend a) ∉ s), Iic a = u
State after:
case right
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
⊢ JoinedIn (f ⁻¹' s) b x

State before:
case right
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
⊢ JoinedIn (f ⁻¹' s) b x
Tactic:
have bdd : BddAbove u := by rw [← hu, bddAbove_def]; use 1; intro t ⟨m, _⟩; exact m.2
State after:
case right
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
⊢ JoinedIn (f ⁻¹' s) b x

State before:
case right
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
⊢ JoinedIn (f ⁻¹' s) b x
Tactic:
have un : u.Nonempty := by
  rw [← hu]; use 0, left_mem_Icc.mpr zero_le_one; simp only [mem_iInter₂, mem_Iic]; intro a m
  contrapose m; simp only [not_not, p.extend_of_le_zero (not_le.mp m).le, fx]
State after:
case right
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
⊢ JoinedIn (f ⁻¹' s) b x

State before:
case right
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
⊢ JoinedIn (f ⁻¹' s) b x
Tactic:
have uc : IsClosed u := by
  rw [← hu]; apply isClosed_Icc.inter; apply isClosed_iInter; intro a; apply isClosed_iInter
  intro _; exact isClosed_Iic
State after:
case right
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
⊢ JoinedIn (f ⁻¹' s) b x

State before:
case right
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
⊢ JoinedIn (f ⁻¹' s) b x
Tactic:
generalize ht : sSup u = t
State after:
case right
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
⊢ JoinedIn (f ⁻¹' s) b x

State before:
case right
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
⊢ JoinedIn (f ⁻¹' s) b x
Tactic:
have tu : t ∈ u := by rw [← uc.closure_eq, ← ht]; exact csSup_mem_closure un bdd
State after:
case right
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
⊢ JoinedIn (f ⁻¹' s) b x

State before:
case right
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
⊢ JoinedIn (f ⁻¹' s) b x
Tactic:
have m : t ∈ Icc (0 : ℝ) 1 := by rw [← hu] at tu; exact tu.1
State after:
case right
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
⊢ JoinedIn (f ⁻¹' s) b x

State before:
case right
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
⊢ JoinedIn (f ⁻¹' s) b x
Tactic:
have lo : ∀ a, a ≤ t → f (p.extend a) ∈ s := by
  intro a h; contrapose h; simp only [not_le]
  replace h : ∀ᶠ b in 𝓝 a, f (p.extend b) ∉ s :=
    (fc.comp p.continuous_extend).continuousAt.eventually_mem (sc.isOpen_compl.mem_nhds h)
  simp only [← hu, mem_inter_iff, mem_iInter₂, mem_Iic] at tu ⊢
  rcases ((frequently_lt_nhds a).and_eventually h).exists with ⟨c, ca, cs⟩
  exact lt_of_le_of_lt (tu.2 c cs) ca
State after:
case right
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
⊢ JoinedIn (f ⁻¹' s) b x

State before:
case right
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
⊢ JoinedIn (f ⁻¹' s) b x
Tactic:
by_cases t1 : t = 1
State after:
case pos
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t = 1
⊢ JoinedIn (f ⁻¹' s) b x

case neg
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : ¬t = 1
⊢ JoinedIn (f ⁻¹' s) b x

State before:
case neg
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : ¬t = 1
⊢ JoinedIn (f ⁻¹' s) b x
Tactic:
replace t1 : t < 1 := Ne.lt_of_le t1 m.2
State after:
case neg
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
⊢ JoinedIn (f ⁻¹' s) b x

State before:
case neg
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
ft : f (p ⟨t, m⟩) ∈ frontier s
⊢ JoinedIn (f ⁻¹' s) b x
Tactic:
refine ((pc.joinedIn _ ft b fb).mono (preimage_mono sc.frontier_subset)).symm.trans
  (JoinedIn.symm ?_)
State after:
case neg
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
ft : f (p ⟨t, m⟩) ∈ frontier s
⊢ JoinedIn (f ⁻¹' s) x (p ⟨t, m⟩)

State before:
case neg
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
ft : f (p ⟨t, m⟩) ∈ frontier s
⊢ JoinedIn (f ⁻¹' s) x (p ⟨t, m⟩)
Tactic:
generalize hq : (fun a : unitInterval ↦ p.extend (min a t)) = q
State after:
case neg
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
ft : f (p ⟨t, m⟩) ∈ frontier s
q : ↑unitInterval → X
hq : (fun a => p.extend (min (↑a) t)) = q
⊢ JoinedIn (f ⁻¹' s) x (p ⟨t, m⟩)

State before:
case neg
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
ft : f (p ⟨t, m⟩) ∈ frontier s
q : ↑unitInterval → X
hq : (fun a => p.extend (min (↑a) t)) = q
⊢ JoinedIn (f ⁻¹' s) x (p ⟨t, m⟩)
Tactic:
have qc : Continuous q := by
  rw [← hq]; exact p.continuous_extend.comp (continuous_subtype_val.min continuous_const)
State after:
case neg
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
ft : f (p ⟨t, m⟩) ∈ frontier s
q : ↑unitInterval → X
hq : (fun a => p.extend (min (↑a) t)) = q
qc : Continuous q
⊢ JoinedIn (f ⁻¹' s) x (p ⟨t, m⟩)

State before:
case neg
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
ft : f (p ⟨t, m⟩) ∈ frontier s
q : ↑unitInterval → X
hq : (fun a => p.extend (min (↑a) t)) = q
qc : Continuous q
⊢ JoinedIn (f ⁻¹' s) x (p ⟨t, m⟩)
Tactic:
refine ⟨⟨⟨q,qc⟩,?_,?_⟩,?_⟩
State after:
case neg.refine_1
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
ft : f (p ⟨t, m⟩) ∈ frontier s
q : ↑unitInterval → X
hq : (fun a => p.extend (min (↑a) t)) = q
qc : Continuous q
⊢ { toFun := q, continuous_toFun := qc }.toFun 0 = x

case neg.refine_2
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
ft : f (p ⟨t, m⟩) ∈ frontier s
q : ↑unitInterval → X
hq : (fun a => p.extend (min (↑a) t)) = q
qc : Continuous q
⊢ { toFun := q, continuous_toFun := qc }.toFun 1 = p ⟨t, m⟩

case neg.refine_3
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
ft : f (p ⟨t, m⟩) ∈ frontier s
q : ↑unitInterval → X
hq : (fun a => p.extend (min (↑a) t)) = q
qc : Continuous q
⊢ ∀ (t_1 : ↑unitInterval),
    { toFun := q, continuous_toFun := qc, source' := ?neg.refine_1✝, target' := ?neg.refine_2✝ } t_1 ∈ f ⁻¹' s

State before:
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
⊢ BddAbove u
Tactic:
rw [← hu, bddAbove_def]
State after:
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
⊢ ∃ x_1, ∀ y ∈ Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a, y ≤ x_1

State before:
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
⊢ ∃ x_1, ∀ y ∈ Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a, y ≤ x_1
Tactic:
use 1
State after:
case h
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
⊢ ∀ y ∈ Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a, y ≤ 1

State before:
case h
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
⊢ ∀ y ∈ Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a, y ≤ 1
Tactic:
intro t ⟨m, _⟩
State after:
case h
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
t : ℝ
m : t ∈ Icc 0 1
right✝ : t ∈ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a
⊢ t ≤ 1

State before:
case h
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
t : ℝ
m : t ∈ Icc 0 1
right✝ : t ∈ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a
⊢ t ≤ 1
Tactic:
exact m.2
State after:
no goals

State before:
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
⊢ u.Nonempty
Tactic:
rw [← hu]
State after:
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
⊢ (Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a).Nonempty

State before:
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
⊢ (Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a).Nonempty
Tactic:
use 0, left_mem_Icc.mpr zero_le_one
State after:
case right
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
⊢ 0 ∈ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a

State before:
case right
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
⊢ 0 ∈ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a
Tactic:
simp only [mem_iInter₂, mem_Iic]
State after:
case right
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
⊢ ∀ (i : ℝ), f (p.extend i) ∉ s → 0 ≤ i

State before:
case right
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
⊢ ∀ (i : ℝ), f (p.extend i) ∉ s → 0 ≤ i
Tactic:
intro a m
State after:
case right
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
a : ℝ
m : f (p.extend a) ∉ s
⊢ 0 ≤ a

State before:
case right
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
a : ℝ
m : f (p.extend a) ∉ s
⊢ 0 ≤ a
Tactic:
contrapose m
State after:
case right
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
a : ℝ
m : ¬0 ≤ a
⊢ ¬f (p.extend a) ∉ s

State before:
case right
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
a : ℝ
m : ¬0 ≤ a
⊢ ¬f (p.extend a) ∉ s
Tactic:
simp only [not_not, p.extend_of_le_zero (not_le.mp m).le, fx]
State after:
no goals

State before:
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
⊢ IsClosed u
Tactic:
rw [← hu]
State after:
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
⊢ IsClosed (Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a)

State before:
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
⊢ IsClosed (Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a)
Tactic:
apply isClosed_Icc.inter
State after:
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
⊢ IsClosed (⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a)

State before:
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
⊢ IsClosed (⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a)
Tactic:
apply isClosed_iInter
State after:
case h
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
⊢ ∀ (i : ℝ), IsClosed (⋂ (_ : f (p.extend i) ∉ s), Iic i)

State before:
case h
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
⊢ ∀ (i : ℝ), IsClosed (⋂ (_ : f (p.extend i) ∉ s), Iic i)
Tactic:
intro a
State after:
case h
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
a : ℝ
⊢ IsClosed (⋂ (_ : f (p.extend a) ∉ s), Iic a)

State before:
case h
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
a : ℝ
⊢ IsClosed (⋂ (_ : f (p.extend a) ∉ s), Iic a)
Tactic:
apply isClosed_iInter
State after:
case h.h
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
a : ℝ
⊢ f (p.extend a) ∉ s → IsClosed (Iic a)

State before:
case h.h
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
a : ℝ
⊢ f (p.extend a) ∉ s → IsClosed (Iic a)
Tactic:
intro _
State after:
case h.h
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
a : ℝ
i✝ : f (p.extend a) ∉ s
⊢ IsClosed (Iic a)

State before:
case h.h
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
a : ℝ
i✝ : f (p.extend a) ∉ s
⊢ IsClosed (Iic a)
Tactic:
exact isClosed_Iic
State after:
no goals

State before:
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
⊢ t ∈ u
Tactic:
rw [← uc.closure_eq, ← ht]
State after:
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
⊢ sSup u ∈ closure u

State before:
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
⊢ sSup u ∈ closure u
Tactic:
exact csSup_mem_closure un bdd
State after:
no goals

State before:
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
⊢ t ∈ Icc 0 1
Tactic:
rw [← hu] at tu
State after:
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a
⊢ t ∈ Icc 0 1

State before:
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a
⊢ t ∈ Icc 0 1
Tactic:
exact tu.1
State after:
no goals

State before:
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
⊢ ∀ a ≤ t, f (p.extend a) ∈ s
Tactic:
intro a h
State after:
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
a : ℝ
h : a ≤ t
⊢ f (p.extend a) ∈ s

State before:
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
a : ℝ
h : a ≤ t
⊢ f (p.extend a) ∈ s
Tactic:
contrapose h
State after:
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
a : ℝ
h : f (p.extend a) ∉ s
⊢ ¬a ≤ t

State before:
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
a : ℝ
h : f (p.extend a) ∉ s
⊢ ¬a ≤ t
Tactic:
simp only [not_le]
State after:
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
a : ℝ
h : f (p.extend a) ∉ s
⊢ t < a

State before:
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
a : ℝ
h : f (p.extend a) ∉ s
⊢ t < a
Tactic:
replace h : ∀ᶠ b in 𝓝 a, f (p.extend b) ∉ s :=
  (fc.comp p.continuous_extend).continuousAt.eventually_mem (sc.isOpen_compl.mem_nhds h)
State after:
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
a : ℝ
h : ∀ᶠ (b_1 : ℝ) in 𝓝 a, f (p.extend b_1) ∉ s
⊢ t < a

State before:
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
a : ℝ
h : ∀ᶠ (b_1 : ℝ) in 𝓝 a, f (p.extend b_1) ∉ s
⊢ t < a
Tactic:
simp only [← hu, mem_inter_iff, mem_iInter₂, mem_Iic] at tu ⊢
State after:
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
m : t ∈ Icc 0 1
a : ℝ
h : ∀ᶠ (b_1 : ℝ) in 𝓝 a, f (p.extend b_1) ∉ s
tu : t ∈ Icc 0 1 ∧ ∀ (i : ℝ), f (p.extend i) ∉ s → t ≤ i
⊢ t < a

State before:
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
m : t ∈ Icc 0 1
a : ℝ
h : ∀ᶠ (b_1 : ℝ) in 𝓝 a, f (p.extend b_1) ∉ s
tu : t ∈ Icc 0 1 ∧ ∀ (i : ℝ), f (p.extend i) ∉ s → t ≤ i
⊢ t < a
Tactic:
rcases ((frequently_lt_nhds a).and_eventually h).exists with ⟨c, ca, cs⟩
State after:
case intro.intro
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
m : t ∈ Icc 0 1
a : ℝ
h : ∀ᶠ (b_1 : ℝ) in 𝓝 a, f (p.extend b_1) ∉ s
tu : t ∈ Icc 0 1 ∧ ∀ (i : ℝ), f (p.extend i) ∉ s → t ≤ i
c : ℝ
ca : c < a
cs : f (p.extend c) ∉ s
⊢ t < a

State before:
case intro.intro
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
m : t ∈ Icc 0 1
a : ℝ
h : ∀ᶠ (b_1 : ℝ) in 𝓝 a, f (p.extend b_1) ∉ s
tu : t ∈ Icc 0 1 ∧ ∀ (i : ℝ), f (p.extend i) ∉ s → t ≤ i
c : ℝ
ca : c < a
cs : f (p.extend c) ∉ s
⊢ t < a
Tactic:
exact lt_of_le_of_lt (tu.2 c cs) ca
State after:
no goals

State before:
case pos
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t = 1
⊢ JoinedIn (f ⁻¹' s) b x
Tactic:
use p.symm
State after:
case h
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t = 1
⊢ ∀ (t : ↑unitInterval), p.symm t ∈ f ⁻¹' s

State before:
case h
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t = 1
⊢ ∀ (t : ↑unitInterval), p.symm t ∈ f ⁻¹' s
Tactic:
intro a
State after:
case h
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t = 1
a : ↑unitInterval
⊢ p.symm a ∈ f ⁻¹' s

State before:
case h
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t = 1
a : ↑unitInterval
⊢ p.symm a ∈ f ⁻¹' s
Tactic:
simp only [p.symm_apply, Function.comp, mem_preimage]
State after:
case h
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t = 1
a : ↑unitInterval
⊢ f (p (unitInterval.symm a)) ∈ s

State before:
case h
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t = 1
a : ↑unitInterval
⊢ f (p (unitInterval.symm a)) ∈ s
Tactic:
rw [← Path.extend_extends']
State after:
case h
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t = 1
a : ↑unitInterval
⊢ f (p.extend ↑(unitInterval.symm a)) ∈ s

State before:
case h
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t = 1
a : ↑unitInterval
⊢ f (p.extend ↑(unitInterval.symm a)) ∈ s
Tactic:
apply lo
State after:
case h.a
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t = 1
a : ↑unitInterval
⊢ ↑(unitInterval.symm a) ≤ t

State before:
case h.a
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t = 1
a : ↑unitInterval
⊢ ↑(unitInterval.symm a) ≤ t
Tactic:
rw [t1]
State after:
case h.a
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t = 1
a : ↑unitInterval
⊢ ↑(unitInterval.symm a) ≤ 1

State before:
case h.a
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t = 1
a : ↑unitInterval
⊢ ↑(unitInterval.symm a) ≤ 1
Tactic:
unit_interval
State after:
no goals

State before:
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
⊢ f (p ⟨t, m⟩) ∈ frontier s
Tactic:
simp only [frontier, mem_diff, sc.closure_eq]
State after:
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
⊢ f (p ⟨t, m⟩) ∈ s ∧ f (p ⟨t, m⟩) ∉ interior s

State before:
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
⊢ f (p ⟨t, m⟩) ∈ s ∧ f (p ⟨t, m⟩) ∉ interior s
Tactic:
constructor
State after:
case left
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
⊢ f (p ⟨t, m⟩) ∈ s

case right
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
⊢ f (p ⟨t, m⟩) ∉ interior s

State before:
case left
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
⊢ f (p ⟨t, m⟩) ∈ s
Tactic:
convert lo t (le_refl _)
State after:
case h.e'_4.h.e'_1
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
⊢ p ⟨t, m⟩ = p.extend t

State before:
case h.e'_4.h.e'_1
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
⊢ p ⟨t, m⟩ = p.extend t
Tactic:
simp only [ge_iff_le, zero_le_one, not_true, gt_iff_lt, mem_Icc, Path.extend_extends _ m]
State after:
no goals

State before:
case right
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
⊢ f (p ⟨t, m⟩) ∉ interior s
Tactic:
have e : p ⟨t, m⟩ = p.extend t := by
  simp only [Path.extend, IccExtend_apply, min_eq_right m.2, max_eq_right m.1]
State after:
case right
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
e : p ⟨t, m⟩ = p.extend t
⊢ f (p ⟨t, m⟩) ∉ interior s

State before:
case right
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
e : p ⟨t, m⟩ = p.extend t
⊢ f (p ⟨t, m⟩) ∉ interior s
Tactic:
rw [e]
State after:
case right
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
e : p ⟨t, m⟩ = p.extend t
⊢ f (p.extend t) ∉ interior s

State before:
case right
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
e : p ⟨t, m⟩ = p.extend t
⊢ f (p.extend t) ∉ interior s
Tactic:
clear e
State after:
case right
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
⊢ f (p.extend t) ∉ interior s

State before:
case right
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
⊢ f (p.extend t) ∉ interior s
Tactic:
simp only [← @mem_preimage _ _ (f.comp p.extend), ← ht]
State after:
case right
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
⊢ f (p.extend (sSup u)) ∉ interior s

State before:
case right
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
⊢ f (p.extend (sSup u)) ∉ interior s
Tactic:
by_contra h
State after:
case right
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
h : f (p.extend (sSup u)) ∈ interior s
⊢ False

State before:
case right
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
h : f (p.extend (sSup u)) ∈ interior s
⊢ False
Tactic:
rw [ht] at h
State after:
case right
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
h : f (p.extend t) ∈ interior s
⊢ False

State before:
case right
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
h : f (p.extend t) ∈ interior s
⊢ False
Tactic:
have o : IsOpen (f ∘ p.extend ⁻¹' interior s) :=
  isOpen_interior.preimage (fc.comp p.continuous_extend)
State after:
case right
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
h : f (p.extend t) ∈ interior s
o : IsOpen (f ∘ p.extend ⁻¹' interior s)
⊢ False

State before:
case right
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
h : f (p.extend t) ∈ interior s
o : IsOpen (f ∘ p.extend ⁻¹' interior s)
⊢ False
Tactic:
rcases (nhds_basis_Ioo t).mem_iff.mp (o.mem_nhds h) with ⟨⟨x, y⟩, ⟨xt, ty⟩, h⟩
State after:
case right.intro.mk.intro.intro
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x✝ : X
fx : f x✝ ∈ s
p : Path x✝ b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
h✝ : f (p.extend t) ∈ interior s
o : IsOpen (f ∘ p.extend ⁻¹' interior s)
x y : ℝ
h : Ioo (x, y).1 (x, y).2 ⊆ f ∘ p.extend ⁻¹' interior s
xt : (x, y).1 < t
ty : t < (x, y).2
⊢ False

State before:
case right.intro.mk.intro.intro
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x✝ : X
fx : f x✝ ∈ s
p : Path x✝ b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
h✝ : f (p.extend t) ∈ interior s
o : IsOpen (f ∘ p.extend ⁻¹' interior s)
x y : ℝ
h : Ioo (x, y).1 (x, y).2 ⊆ f ∘ p.extend ⁻¹' interior s
xt : (x, y).1 < t
ty : t < (x, y).2
⊢ False
Tactic:
simp only [subset_def, mem_Ioo, and_imp, mem_preimage, Function.comp] at xt ty h
State after:
case right.intro.mk.intro.intro
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x✝ : X
fx : f x✝ ∈ s
p : Path x✝ b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
h✝ : f (p.extend t) ∈ interior s
o : IsOpen (f ∘ p.extend ⁻¹' interior s)
x y : ℝ
xt : x < t
ty : t < y
h : ∀ (x_1 : ℝ), x < x_1 → x_1 < y → f (p.extend x_1) ∈ interior s
⊢ False

State before:
case right.intro.mk.intro.intro
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x✝ : X
fx : f x✝ ∈ s
p : Path x✝ b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
h✝ : f (p.extend t) ∈ interior s
o : IsOpen (f ∘ p.extend ⁻¹' interior s)
x y : ℝ
xt : x < t
ty : t < y
h : ∀ (x_1 : ℝ), x < x_1 → x_1 < y → f (p.extend x_1) ∈ interior s
⊢ False
Tactic:
rcases exists_between (lt_min ty t1) with ⟨z, tz, zy1⟩
State after:
case right.intro.mk.intro.intro.intro.intro
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x✝ : X
fx : f x✝ ∈ s
p : Path x✝ b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
h✝ : f (p.extend t) ∈ interior s
o : IsOpen (f ∘ p.extend ⁻¹' interior s)
x y : ℝ
xt : x < t
ty : t < y
h : ∀ (x_1 : ℝ), x < x_1 → x_1 < y → f (p.extend x_1) ∈ interior s
z : ℝ
tz : t < z
zy1 : z < min y 1
⊢ False

State before:
case right.intro.mk.intro.intro.intro.intro
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x✝ : X
fx : f x✝ ∈ s
p : Path x✝ b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
h✝ : f (p.extend t) ∈ interior s
o : IsOpen (f ∘ p.extend ⁻¹' interior s)
x y : ℝ
xt : x < t
ty : t < y
h : ∀ (x_1 : ℝ), x < x_1 → x_1 < y → f (p.extend x_1) ∈ interior s
z : ℝ
tz : t < z
zy1 : z < min y 1
⊢ False
Tactic:
rcases lt_min_iff.mp zy1 with ⟨zy, z1⟩
State after:
case right.intro.mk.intro.intro.intro.intro.intro
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x✝ : X
fx : f x✝ ∈ s
p : Path x✝ b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
h✝ : f (p.extend t) ∈ interior s
o : IsOpen (f ∘ p.extend ⁻¹' interior s)
x y : ℝ
xt : x < t
ty : t < y
h : ∀ (x_1 : ℝ), x < x_1 → x_1 < y → f (p.extend x_1) ∈ interior s
z : ℝ
tz : t < z
zy1 : z < min y 1
zy : z < y
z1 : z < 1
⊢ False

State before:
case right.intro.mk.intro.intro.intro.intro.intro
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x✝ : X
fx : f x✝ ∈ s
p : Path x✝ b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
h✝ : f (p.extend t) ∈ interior s
o : IsOpen (f ∘ p.extend ⁻¹' interior s)
x y : ℝ
xt : x < t
ty : t < y
h : ∀ (x_1 : ℝ), x < x_1 → x_1 < y → f (p.extend x_1) ∈ interior s
z : ℝ
tz : t < z
zy1 : z < min y 1
zy : z < y
z1 : z < 1
⊢ False
Tactic:
suffices h : z ∈ u by linarith [le_csSup bdd h]
State after:
case right.intro.mk.intro.intro.intro.intro.intro
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x✝ : X
fx : f x✝ ∈ s
p : Path x✝ b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
h✝ : f (p.extend t) ∈ interior s
o : IsOpen (f ∘ p.extend ⁻¹' interior s)
x y : ℝ
xt : x < t
ty : t < y
h : ∀ (x_1 : ℝ), x < x_1 → x_1 < y → f (p.extend x_1) ∈ interior s
z : ℝ
tz : t < z
zy1 : z < min y 1
zy : z < y
z1 : z < 1
⊢ z ∈ u

State before:
case right.intro.mk.intro.intro.intro.intro.intro
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x✝ : X
fx : f x✝ ∈ s
p : Path x✝ b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
h✝ : f (p.extend t) ∈ interior s
o : IsOpen (f ∘ p.extend ⁻¹' interior s)
x y : ℝ
xt : x < t
ty : t < y
h : ∀ (x_1 : ℝ), x < x_1 → x_1 < y → f (p.extend x_1) ∈ interior s
z : ℝ
tz : t < z
zy1 : z < min y 1
zy : z < y
z1 : z < 1
⊢ z ∈ u
Tactic:
rw [← hu]
State after:
case right.intro.mk.intro.intro.intro.intro.intro
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x✝ : X
fx : f x✝ ∈ s
p : Path x✝ b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
h✝ : f (p.extend t) ∈ interior s
o : IsOpen (f ∘ p.extend ⁻¹' interior s)
x y : ℝ
xt : x < t
ty : t < y
h : ∀ (x_1 : ℝ), x < x_1 → x_1 < y → f (p.extend x_1) ∈ interior s
z : ℝ
tz : t < z
zy1 : z < min y 1
zy : z < y
z1 : z < 1
⊢ z ∈ Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a

State before:
case right.intro.mk.intro.intro.intro.intro.intro
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x✝ : X
fx : f x✝ ∈ s
p : Path x✝ b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
h✝ : f (p.extend t) ∈ interior s
o : IsOpen (f ∘ p.extend ⁻¹' interior s)
x y : ℝ
xt : x < t
ty : t < y
h : ∀ (x_1 : ℝ), x < x_1 → x_1 < y → f (p.extend x_1) ∈ interior s
z : ℝ
tz : t < z
zy1 : z < min y 1
zy : z < y
z1 : z < 1
⊢ z ∈ Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a
Tactic:
refine ⟨⟨_root_.trans m.1 tz.le, z1.le⟩, ?_⟩
State after:
case right.intro.mk.intro.intro.intro.intro.intro
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x✝ : X
fx : f x✝ ∈ s
p : Path x✝ b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
h✝ : f (p.extend t) ∈ interior s
o : IsOpen (f ∘ p.extend ⁻¹' interior s)
x y : ℝ
xt : x < t
ty : t < y
h : ∀ (x_1 : ℝ), x < x_1 → x_1 < y → f (p.extend x_1) ∈ interior s
z : ℝ
tz : t < z
zy1 : z < min y 1
zy : z < y
z1 : z < 1
⊢ z ∈ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a

State before:
case right.intro.mk.intro.intro.intro.intro.intro
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x✝ : X
fx : f x✝ ∈ s
p : Path x✝ b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
h✝ : f (p.extend t) ∈ interior s
o : IsOpen (f ∘ p.extend ⁻¹' interior s)
x y : ℝ
xt : x < t
ty : t < y
h : ∀ (x_1 : ℝ), x < x_1 → x_1 < y → f (p.extend x_1) ∈ interior s
z : ℝ
tz : t < z
zy1 : z < min y 1
zy : z < y
z1 : z < 1
⊢ z ∈ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a
Tactic:
simp only [mem_iInter₂, mem_Iic]
State after:
case right.intro.mk.intro.intro.intro.intro.intro
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x✝ : X
fx : f x✝ ∈ s
p : Path x✝ b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
h✝ : f (p.extend t) ∈ interior s
o : IsOpen (f ∘ p.extend ⁻¹' interior s)
x y : ℝ
xt : x < t
ty : t < y
h : ∀ (x_1 : ℝ), x < x_1 → x_1 < y → f (p.extend x_1) ∈ interior s
z : ℝ
tz : t < z
zy1 : z < min y 1
zy : z < y
z1 : z < 1
⊢ ∀ (i : ℝ), f (p.extend i) ∉ s → z ≤ i

State before:
case right.intro.mk.intro.intro.intro.intro.intro
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x✝ : X
fx : f x✝ ∈ s
p : Path x✝ b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
h✝ : f (p.extend t) ∈ interior s
o : IsOpen (f ∘ p.extend ⁻¹' interior s)
x y : ℝ
xt : x < t
ty : t < y
h : ∀ (x_1 : ℝ), x < x_1 → x_1 < y → f (p.extend x_1) ∈ interior s
z : ℝ
tz : t < z
zy1 : z < min y 1
zy : z < y
z1 : z < 1
⊢ ∀ (i : ℝ), f (p.extend i) ∉ s → z ≤ i
Tactic:
intro w ws
State after:
case right.intro.mk.intro.intro.intro.intro.intro
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x✝ : X
fx : f x✝ ∈ s
p : Path x✝ b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
h✝ : f (p.extend t) ∈ interior s
o : IsOpen (f ∘ p.extend ⁻¹' interior s)
x y : ℝ
xt : x < t
ty : t < y
h : ∀ (x_1 : ℝ), x < x_1 → x_1 < y → f (p.extend x_1) ∈ interior s
z : ℝ
tz : t < z
zy1 : z < min y 1
zy : z < y
z1 : z < 1
w : ℝ
ws : f (p.extend w) ∉ s
⊢ z ≤ w

State before:
case right.intro.mk.intro.intro.intro.intro.intro
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x✝ : X
fx : f x✝ ∈ s
p : Path x✝ b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
h✝ : f (p.extend t) ∈ interior s
o : IsOpen (f ∘ p.extend ⁻¹' interior s)
x y : ℝ
xt : x < t
ty : t < y
h : ∀ (x_1 : ℝ), x < x_1 → x_1 < y → f (p.extend x_1) ∈ interior s
z : ℝ
tz : t < z
zy1 : z < min y 1
zy : z < y
z1 : z < 1
w : ℝ
ws : f (p.extend w) ∉ s
⊢ z ≤ w
Tactic:
contrapose ws
State after:
case right.intro.mk.intro.intro.intro.intro.intro
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x✝ : X
fx : f x✝ ∈ s
p : Path x✝ b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
h✝ : f (p.extend t) ∈ interior s
o : IsOpen (f ∘ p.extend ⁻¹' interior s)
x y : ℝ
xt : x < t
ty : t < y
h : ∀ (x_1 : ℝ), x < x_1 → x_1 < y → f (p.extend x_1) ∈ interior s
z : ℝ
tz : t < z
zy1 : z < min y 1
zy : z < y
z1 : z < 1
w : ℝ
ws : ¬z ≤ w
⊢ ¬f (p.extend w) ∉ s

State before:
case right.intro.mk.intro.intro.intro.intro.intro
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x✝ : X
fx : f x✝ ∈ s
p : Path x✝ b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
h✝ : f (p.extend t) ∈ interior s
o : IsOpen (f ∘ p.extend ⁻¹' interior s)
x y : ℝ
xt : x < t
ty : t < y
h : ∀ (x_1 : ℝ), x < x_1 → x_1 < y → f (p.extend x_1) ∈ interior s
z : ℝ
tz : t < z
zy1 : z < min y 1
zy : z < y
z1 : z < 1
w : ℝ
ws : ¬z ≤ w
⊢ ¬f (p.extend w) ∉ s
Tactic:
simp only [not_not, not_le] at ws ⊢
State after:
case right.intro.mk.intro.intro.intro.intro.intro
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x✝ : X
fx : f x✝ ∈ s
p : Path x✝ b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
h✝ : f (p.extend t) ∈ interior s
o : IsOpen (f ∘ p.extend ⁻¹' interior s)
x y : ℝ
xt : x < t
ty : t < y
h : ∀ (x_1 : ℝ), x < x_1 → x_1 < y → f (p.extend x_1) ∈ interior s
z : ℝ
tz : t < z
zy1 : z < min y 1
zy : z < y
z1 : z < 1
w : ℝ
ws : w < z
⊢ f (p.extend w) ∈ s

State before:
case right.intro.mk.intro.intro.intro.intro.intro
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x✝ : X
fx : f x✝ ∈ s
p : Path x✝ b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
h✝ : f (p.extend t) ∈ interior s
o : IsOpen (f ∘ p.extend ⁻¹' interior s)
x y : ℝ
xt : x < t
ty : t < y
h : ∀ (x_1 : ℝ), x < x_1 → x_1 < y → f (p.extend x_1) ∈ interior s
z : ℝ
tz : t < z
zy1 : z < min y 1
zy : z < y
z1 : z < 1
w : ℝ
ws : w < z
⊢ f (p.extend w) ∈ s
Tactic:
by_cases xw : x < w
State after:
case pos
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x✝ : X
fx : f x✝ ∈ s
p : Path x✝ b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
h✝ : f (p.extend t) ∈ interior s
o : IsOpen (f ∘ p.extend ⁻¹' interior s)
x y : ℝ
xt : x < t
ty : t < y
h : ∀ (x_1 : ℝ), x < x_1 → x_1 < y → f (p.extend x_1) ∈ interior s
z : ℝ
tz : t < z
zy1 : z < min y 1
zy : z < y
z1 : z < 1
w : ℝ
ws : w < z
xw : x < w
⊢ f (p.extend w) ∈ s

case neg
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x✝ : X
fx : f x✝ ∈ s
p : Path x✝ b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
h✝ : f (p.extend t) ∈ interior s
o : IsOpen (f ∘ p.extend ⁻¹' interior s)
x y : ℝ
xt : x < t
ty : t < y
h : ∀ (x_1 : ℝ), x < x_1 → x_1 < y → f (p.extend x_1) ∈ interior s
z : ℝ
tz : t < z
zy1 : z < min y 1
zy : z < y
z1 : z < 1
w : ℝ
ws : w < z
xw : ¬x < w
⊢ f (p.extend w) ∈ s

State before:
case pos
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x✝ : X
fx : f x✝ ∈ s
p : Path x✝ b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
h✝ : f (p.extend t) ∈ interior s
o : IsOpen (f ∘ p.extend ⁻¹' interior s)
x y : ℝ
xt : x < t
ty : t < y
h : ∀ (x_1 : ℝ), x < x_1 → x_1 < y → f (p.extend x_1) ∈ interior s
z : ℝ
tz : t < z
zy1 : z < min y 1
zy : z < y
z1 : z < 1
w : ℝ
ws : w < z
xw : x < w
⊢ f (p.extend w) ∈ s

case neg
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x✝ : X
fx : f x✝ ∈ s
p : Path x✝ b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
h✝ : f (p.extend t) ∈ interior s
o : IsOpen (f ∘ p.extend ⁻¹' interior s)
x y : ℝ
xt : x < t
ty : t < y
h : ∀ (x_1 : ℝ), x < x_1 → x_1 < y → f (p.extend x_1) ∈ interior s
z : ℝ
tz : t < z
zy1 : z < min y 1
zy : z < y
z1 : z < 1
w : ℝ
ws : w < z
xw : ¬x < w
⊢ f (p.extend w) ∈ s
Tactic:
refine interior_subset (h _ xw (_root_.trans ws zy))
State after:
case neg
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x✝ : X
fx : f x✝ ∈ s
p : Path x✝ b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
h✝ : f (p.extend t) ∈ interior s
o : IsOpen (f ∘ p.extend ⁻¹' interior s)
x y : ℝ
xt : x < t
ty : t < y
h : ∀ (x_1 : ℝ), x < x_1 → x_1 < y → f (p.extend x_1) ∈ interior s
z : ℝ
tz : t < z
zy1 : z < min y 1
zy : z < y
z1 : z < 1
w : ℝ
ws : w < z
xw : ¬x < w
⊢ f (p.extend w) ∈ s

State before:
case neg
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x✝ : X
fx : f x✝ ∈ s
p : Path x✝ b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
h✝ : f (p.extend t) ∈ interior s
o : IsOpen (f ∘ p.extend ⁻¹' interior s)
x y : ℝ
xt : x < t
ty : t < y
h : ∀ (x_1 : ℝ), x < x_1 → x_1 < y → f (p.extend x_1) ∈ interior s
z : ℝ
tz : t < z
zy1 : z < min y 1
zy : z < y
z1 : z < 1
w : ℝ
ws : w < z
xw : ¬x < w
⊢ f (p.extend w) ∈ s
Tactic:
simp only [not_lt] at xw
State after:
case neg
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x✝ : X
fx : f x✝ ∈ s
p : Path x✝ b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
h✝ : f (p.extend t) ∈ interior s
o : IsOpen (f ∘ p.extend ⁻¹' interior s)
x y : ℝ
xt : x < t
ty : t < y
h : ∀ (x_1 : ℝ), x < x_1 → x_1 < y → f (p.extend x_1) ∈ interior s
z : ℝ
tz : t < z
zy1 : z < min y 1
zy : z < y
z1 : z < 1
w : ℝ
ws : w < z
xw : w ≤ x
⊢ f (p.extend w) ∈ s

State before:
case neg
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x✝ : X
fx : f x✝ ∈ s
p : Path x✝ b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
h✝ : f (p.extend t) ∈ interior s
o : IsOpen (f ∘ p.extend ⁻¹' interior s)
x y : ℝ
xt : x < t
ty : t < y
h : ∀ (x_1 : ℝ), x < x_1 → x_1 < y → f (p.extend x_1) ∈ interior s
z : ℝ
tz : t < z
zy1 : z < min y 1
zy : z < y
z1 : z < 1
w : ℝ
ws : w < z
xw : w ≤ x
⊢ f (p.extend w) ∈ s
Tactic:
exact lo _ (_root_.trans xw xt.le)
State after:
no goals

State before:
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
⊢ p ⟨t, m⟩ = p.extend t
Tactic:
simp only [Path.extend, IccExtend_apply, min_eq_right m.2, max_eq_right m.1]
State after:
no goals

State before:
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x✝ : X
fx : f x✝ ∈ s
p : Path x✝ b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
h✝¹ : f (p.extend t) ∈ interior s
o : IsOpen (f ∘ p.extend ⁻¹' interior s)
x y : ℝ
xt : x < t
ty : t < y
h✝ : ∀ (x_1 : ℝ), x < x_1 → x_1 < y → f (p.extend x_1) ∈ interior s
z : ℝ
tz : t < z
zy1 : z < min y 1
zy : z < y
z1 : z < 1
h : z ∈ u
⊢ False
Tactic:
linarith [le_csSup bdd h]
State after:
no goals

State before:
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
ft : f (p ⟨t, m⟩) ∈ frontier s
q : ↑unitInterval → X
hq : (fun a => p.extend (min (↑a) t)) = q
⊢ Continuous q
Tactic:
rw [← hq]
State after:
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
ft : f (p ⟨t, m⟩) ∈ frontier s
q : ↑unitInterval → X
hq : (fun a => p.extend (min (↑a) t)) = q
⊢ Continuous fun a => p.extend (min (↑a) t)

State before:
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
ft : f (p ⟨t, m⟩) ∈ frontier s
q : ↑unitInterval → X
hq : (fun a => p.extend (min (↑a) t)) = q
⊢ Continuous fun a => p.extend (min (↑a) t)
Tactic:
exact p.continuous_extend.comp (continuous_subtype_val.min continuous_const)
State after:
no goals

State before:
case neg.refine_1
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
ft : f (p ⟨t, m⟩) ∈ frontier s
q : ↑unitInterval → X
hq : (fun a => p.extend (min (↑a) t)) = q
qc : Continuous q
⊢ { toFun := q, continuous_toFun := qc }.toFun 0 = x
Tactic:
simp only [← hq]
State after:
case neg.refine_1
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
ft : f (p ⟨t, m⟩) ∈ frontier s
q : ↑unitInterval → X
hq : (fun a => p.extend (min (↑a) t)) = q
qc : Continuous q
⊢ p.extend (min (↑0) t) = x

State before:
case neg.refine_1
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
ft : f (p ⟨t, m⟩) ∈ frontier s
q : ↑unitInterval → X
hq : (fun a => p.extend (min (↑a) t)) = q
qc : Continuous q
⊢ p.extend (min (↑0) t) = x
Tactic:
simp only [Icc.coe_zero, min_eq_left m.1, p.extend_zero]
State after:
no goals

State before:
case neg.refine_2
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
ft : f (p ⟨t, m⟩) ∈ frontier s
q : ↑unitInterval → X
hq : (fun a => p.extend (min (↑a) t)) = q
qc : Continuous q
⊢ { toFun := q, continuous_toFun := qc }.toFun 1 = p ⟨t, m⟩
Tactic:
simp only [← hq]
State after:
case neg.refine_2
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
ft : f (p ⟨t, m⟩) ∈ frontier s
q : ↑unitInterval → X
hq : (fun a => p.extend (min (↑a) t)) = q
qc : Continuous q
⊢ p.extend (min (↑1) t) = p ⟨t, m⟩

State before:
case neg.refine_2
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
ft : f (p ⟨t, m⟩) ∈ frontier s
q : ↑unitInterval → X
hq : (fun a => p.extend (min (↑a) t)) = q
qc : Continuous q
⊢ p.extend (min (↑1) t) = p ⟨t, m⟩
Tactic:
simp only [Icc.coe_one, min_eq_right m.2, Path.extend, IccExtend_apply, max_eq_right m.1]
State after:
no goals

State before:
case neg.refine_3
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
ft : f (p ⟨t, m⟩) ∈ frontier s
q : ↑unitInterval → X
hq : (fun a => p.extend (min (↑a) t)) = q
qc : Continuous q
⊢ ∀ (t_1 : ↑unitInterval), { toFun := q, continuous_toFun := qc, source' := ⋯, target' := ⋯ } t_1 ∈ f ⁻¹' s
Tactic:
intro ⟨a, n⟩
State after:
case neg.refine_3
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
ft : f (p ⟨t, m⟩) ∈ frontier s
q : ↑unitInterval → X
hq : (fun a => p.extend (min (↑a) t)) = q
qc : Continuous q
a : ℝ
n : a ∈ unitInterval
⊢ { toFun := q, continuous_toFun := qc, source' := ⋯, target' := ⋯ } ⟨a, n⟩ ∈ f ⁻¹' s

State before:
case neg.refine_3
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
ft : f (p ⟨t, m⟩) ∈ frontier s
q : ↑unitInterval → X
hq : (fun a => p.extend (min (↑a) t)) = q
qc : Continuous q
a : ℝ
n : a ∈ unitInterval
⊢ { toFun := q, continuous_toFun := qc, source' := ⋯, target' := ⋯ } ⟨a, n⟩ ∈ f ⁻¹' s
Tactic:
simp only [mem_preimage, Path.coe_mk_mk, ← hq, Subtype.coe_mk]
State after:
case neg.refine_3
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
ft : f (p ⟨t, m⟩) ∈ frontier s
q : ↑unitInterval → X
hq : (fun a => p.extend (min (↑a) t)) = q
qc : Continuous q
a : ℝ
n : a ∈ unitInterval
⊢ f (p.extend (min a t)) ∈ s

State before:
case neg.refine_3
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
ft : f (p ⟨t, m⟩) ∈ frontier s
q : ↑unitInterval → X
hq : (fun a => p.extend (min (↑a) t)) = q
qc : Continuous q
a : ℝ
n : a ∈ unitInterval
⊢ f (p.extend (min a t)) ∈ s
Tactic:
exact lo _ (min_le_right _ _)
State after:
no goals