-- Mathlib/Geometry/Manifold/Instances/Real.lean
lemma boundary_Icc : (𝓡∂ 1).boundary (Icc x y) = {⊥, ⊤}

Proof state:
case h.inr.inl
x y : ℝ
hxy : Fact (x < y)
p : ↑(Icc x y)
hp : ↑p = y
this : p = ⊤
⊢ p ∈ ModelWithCorners.boundary ↑(Icc x y) ↔ p ∈ {⊥, ⊤}

Tactic:
rw [this]

Result:
case h.inr.inl
x y : ℝ
hxy : Fact (x < y)
p : ↑(Icc x y)
hp : ↑p = y
this : p = ⊤
⊢ ⊤ ∈ ModelWithCorners.boundary ↑(Icc x y) ↔ ⊤ ∈ {⊥, ⊤}

Proof state:
case h
x y : ℝ
hxy : Fact (x < y)
p : ↑(Icc x y)
⊢ p ∈ ModelWithCorners.boundary ↑(Icc x y) ↔ p ∈ {⊥, ⊤}

Tactic:
rcases Set.eq_endpoints_or_mem_Ioo_of_mem_Icc p.2 with (hp | hp | hp)

Result:
case h.inl
x y : ℝ
hxy : Fact (x < y)
p : ↑(Icc x y)
hp : ↑p = x
⊢ p ∈ ModelWithCorners.boundary ↑(Icc x y) ↔ p ∈ {⊥, ⊤}

case h.inr.inl
x y : ℝ
hxy : Fact (x < y)
p : ↑(Icc x y)
hp : ↑p = y
⊢ p ∈ ModelWithCorners.boundary ↑(Icc x y) ↔ p ∈ {⊥, ⊤}

case h.inr.inr
x y : ℝ
hxy : Fact (x < y)
p : ↑(Icc x y)
hp : ↑p ∈ Ioo x y
⊢ p ∈ ModelWithCorners.boundary ↑(Icc x y) ↔ p ∈ {⊥, ⊤}

Proof state:
case h.inr.inr.hb
x y : ℝ
hxy : Fact (x < y)
p : ↑(Icc x y)
hp : ↑p ∈ Ioo x y
⊢ p ∉ {⊥, ⊤}

Tactic:
rw [mem_insert_iff, mem_singleton_iff]

Result:
case h.inr.inr.hb
x y : ℝ
hxy : Fact (x < y)
p : ↑(Icc x y)
hp : ↑p ∈ Ioo x y
⊢ ¬(p = ⊥ ∨ p = ⊤)

Proof state:
case h.inr.inr.ha
x y : ℝ
hxy : Fact (x < y)
p : ↑(Icc x y)
hp : ↑p ∈ Ioo x y
⊢ p ∉ ModelWithCorners.boundary ↑(Icc x y)

Tactic:
simpa [← mem_compl_iff, ModelWithCorners.compl_boundary] using
  Icc_isInteriorPoint_interior hp

Result:
no goals

Proof state:
case h.inr.inr.hb
x y : ℝ
hxy : Fact (x < y)
p : ↑(Icc x y)
hp : ↑p ∈ Ioo x y
⊢ p ≠ ⊥ ∧ p ≠ ⊤

Tactic:
constructor <;> by_contra h <;> rw [congrArg Subtype.val h] at hp

Result:
case h.inr.inr.hb.left
x y : ℝ
hxy : Fact (x < y)
p : ↑(Icc x y)
hp : ↑⊥ ∈ Ioo x y
h : p = ⊥
⊢ False

case h.inr.inr.hb.right
x y : ℝ
hxy : Fact (x < y)
p : ↑(Icc x y)
hp : ↑⊤ ∈ Ioo x y
h : p = ⊤
⊢ False

Proof state:
case h.inl
x y : ℝ
hxy : Fact (x < y)
p : ↑(Icc x y)
hp : ↑p = x
this : p = ⊥
⊢ ⊥ ∈ ModelWithCorners.boundary ↑(Icc x y) ↔ ⊥ ∈ {⊥, ⊤}

Tactic:
apply iff_of_true Icc_isBoundaryPoint_bot (mem_insert ⊥ {⊤})

Result:
no goals

Proof state:
case h.inr.inl
x y : ℝ
hxy : Fact (x < y)
p : ↑(Icc x y)
hp : ↑p = y
this : p = ⊤
⊢ ⊤ ∈ ModelWithCorners.boundary ↑(Icc x y) ↔ ⊤ ∈ {⊥, ⊤}

Tactic:
apply iff_of_true Icc_isBoundaryPoint_top (mem_insert_of_mem ⊥ rfl)

Result:
no goals

Proof state:
case h.inr.inr.hb
x y : ℝ
hxy : Fact (x < y)
p : ↑(Icc x y)
hp : ↑p ∈ Ioo x y
⊢ ¬(p = ⊥ ∨ p = ⊤)

Tactic:
push_neg

Result:
case h.inr.inr.hb
x y : ℝ
hxy : Fact (x < y)
p : ↑(Icc x y)
hp : ↑p ∈ Ioo x y
⊢ p ≠ ⊥ ∧ p ≠ ⊤

Proof state:
case h.inl
x y : ℝ
hxy : Fact (x < y)
p : ↑(Icc x y)
hp : ↑p = x
⊢ p ∈ ModelWithCorners.boundary ↑(Icc x y) ↔ p ∈ {⊥, ⊤}

Tactic:
have : p = ⊥ := SetCoe.ext hp

Result:
case h.inl
x y : ℝ
hxy : Fact (x < y)
p : ↑(Icc x y)
hp : ↑p = x
this : p = ⊥
⊢ p ∈ ModelWithCorners.boundary ↑(Icc x y) ↔ p ∈ {⊥, ⊤}

Proof state:
case h.inr.inr.hb.left
x y : ℝ
hxy : Fact (x < y)
p : ↑(Icc x y)
hp : ↑⊥ ∈ Ioo x y
h : p = ⊥
⊢ False

case h.inr.inr.hb.right
x y : ℝ
hxy : Fact (x < y)
p : ↑(Icc x y)
hp : ↑⊤ ∈ Ioo x y
h : p = ⊤
⊢ False

Tactic:
exacts [left_mem_Ioo.mp hp, right_mem_Ioo.mp hp]

Result:
no goals

Proof state:
x y : ℝ
hxy : Fact (x < y)
⊢ ModelWithCorners.boundary ↑(Icc x y) = {⊥, ⊤}

Tactic:
ext p

Result:
case h
x y : ℝ
hxy : Fact (x < y)
p : ↑(Icc x y)
⊢ p ∈ ModelWithCorners.boundary ↑(Icc x y) ↔ p ∈ {⊥, ⊤}

Proof state:
case h.inr.inr
x y : ℝ
hxy : Fact (x < y)
p : ↑(Icc x y)
hp : ↑p ∈ Ioo x y
⊢ p ∈ ModelWithCorners.boundary ↑(Icc x y) ↔ p ∈ {⊥, ⊤}

Tactic:
apply iff_of_false

Result:
case h.inr.inr.ha
x y : ℝ
hxy : Fact (x < y)
p : ↑(Icc x y)
hp : ↑p ∈ Ioo x y
⊢ p ∉ ModelWithCorners.boundary ↑(Icc x y)

case h.inr.inr.hb
x y : ℝ
hxy : Fact (x < y)
p : ↑(Icc x y)
hp : ↑p ∈ Ioo x y
⊢ p ∉ {⊥, ⊤}

Proof state:
case h.inl
x y : ℝ
hxy : Fact (x < y)
p : ↑(Icc x y)
hp : ↑p = x
this : p = ⊥
⊢ p ∈ ModelWithCorners.boundary ↑(Icc x y) ↔ p ∈ {⊥, ⊤}

Tactic:
rw [this]

Result:
case h.inl
x y : ℝ
hxy : Fact (x < y)
p : ↑(Icc x y)
hp : ↑p = x
this : p = ⊥
⊢ ⊥ ∈ ModelWithCorners.boundary ↑(Icc x y) ↔ ⊥ ∈ {⊥, ⊤}

Proof state:
case h.inr.inl
x y : ℝ
hxy : Fact (x < y)
p : ↑(Icc x y)
hp : ↑p = y
⊢ p ∈ ModelWithCorners.boundary ↑(Icc x y) ↔ p ∈ {⊥, ⊤}

Tactic:
have : p = ⊤ := SetCoe.ext hp

Result:
case h.inr.inl
x y : ℝ
hxy : Fact (x < y)
p : ↑(Icc x y)
hp : ↑p = y
this : p = ⊤
⊢ p ∈ ModelWithCorners.boundary ↑(Icc x y) ↔ p ∈ {⊥, ⊤}