Theorem: Section10sheet1Solutions.Real.isOpen_inter (FormalisingMathematics2024/Solutions/Section10TopologicalSpaces/Sheet1.lean)

State before:
X : Type
s t : Set ℝ
hs : IsOpen s
ht : IsOpen t
⊢ IsOpen (s ∩ t)
Tactic:
intro x hx
State after:
X : Type
s t : Set ℝ
hs : IsOpen s
ht : IsOpen t
x : ℝ
hx : x ∈ s ∩ t
⊢ ∃ δ > 0, ∀ (y : ℝ), x - δ < y ∧ y < x + δ → y ∈ s ∩ t

State before:
X : Type
s t : Set ℝ
hs : IsOpen s
ht : IsOpen t
x : ℝ
hx : x ∈ s ∩ t
⊢ ∃ δ > 0, ∀ (y : ℝ), x - δ < y ∧ y < x + δ → y ∈ s ∩ t
Tactic:
obtain ⟨δs, δspos, hs⟩ := hs x (by aesop)
State after:
case intro.intro
X : Type
s t : Set ℝ
hs✝ : IsOpen s
ht : IsOpen t
x : ℝ
hx : x ∈ s ∩ t
δs : ℝ
δspos : δs > 0
hs : ∀ (y : ℝ), x - δs < y ∧ y < x + δs → y ∈ s
⊢ ∃ δ > 0, ∀ (y : ℝ), x - δ < y ∧ y < x + δ → y ∈ s ∩ t

State before:
case intro.intro
X : Type
s t : Set ℝ
hs✝ : IsOpen s
ht : IsOpen t
x : ℝ
hx : x ∈ s ∩ t
δs : ℝ
δspos : δs > 0
hs : ∀ (y : ℝ), x - δs < y ∧ y < x + δs → y ∈ s
⊢ ∃ δ > 0, ∀ (y : ℝ), x - δ < y ∧ y < x + δ → y ∈ s ∩ t
Tactic:
obtain ⟨δt, δtpos, ht⟩ := ht x (by aesop)
State after:
case intro.intro.intro.intro
X : Type
s t : Set ℝ
hs✝ : IsOpen s
ht✝ : IsOpen t
x : ℝ
hx : x ∈ s ∩ t
δs : ℝ
δspos : δs > 0
hs : ∀ (y : ℝ), x - δs < y ∧ y < x + δs → y ∈ s
δt : ℝ
δtpos : δt > 0
ht : ∀ (y : ℝ), x - δt < y ∧ y < x + δt → y ∈ t
⊢ ∃ δ > 0, ∀ (y : ℝ), x - δ < y ∧ y < x + δ → y ∈ s ∩ t

State before:
case intro.intro.intro.intro
X : Type
s t : Set ℝ
hs✝ : IsOpen s
ht✝ : IsOpen t
x : ℝ
hx : x ∈ s ∩ t
δs : ℝ
δspos : δs > 0
hs : ∀ (y : ℝ), x - δs < y ∧ y < x + δs → y ∈ s
δt : ℝ
δtpos : δt > 0
ht : ∀ (y : ℝ), x - δt < y ∧ y < x + δt → y ∈ t
⊢ ∃ δ > 0, ∀ (y : ℝ), x - δ < y ∧ y < x + δ → y ∈ s ∩ t
Tactic:
use min δs δt, by positivity
State after:
case right
X : Type
s t : Set ℝ
hs✝ : IsOpen s
ht✝ : IsOpen t
x : ℝ
hx : x ∈ s ∩ t
δs : ℝ
δspos : δs > 0
hs : ∀ (y : ℝ), x - δs < y ∧ y < x + δs → y ∈ s
δt : ℝ
δtpos : δt > 0
ht : ∀ (y : ℝ), x - δt < y ∧ y < x + δt → y ∈ t
⊢ ∀ (y : ℝ), x - min δs δt < y ∧ y < x + min δs δt → y ∈ s ∩ t

State before:
case right
X : Type
s t : Set ℝ
hs✝ : IsOpen s
ht✝ : IsOpen t
x : ℝ
hx : x ∈ s ∩ t
δs : ℝ
δspos : δs > 0
hs : ∀ (y : ℝ), x - δs < y ∧ y < x + δs → y ∈ s
δt : ℝ
δtpos : δt > 0
ht : ∀ (y : ℝ), x - δt < y ∧ y < x + δt → y ∈ t
⊢ ∀ (y : ℝ), x - min δs δt < y ∧ y < x + min δs δt → y ∈ s ∩ t
Tactic:
rintro y ⟨h1, h2⟩
State after:
case right.intro
X : Type
s t : Set ℝ
hs✝ : IsOpen s
ht✝ : IsOpen t
x : ℝ
hx : x ∈ s ∩ t
δs : ℝ
δspos : δs > 0
hs : ∀ (y : ℝ), x - δs < y ∧ y < x + δs → y ∈ s
δt : ℝ
δtpos : δt > 0
ht : ∀ (y : ℝ), x - δt < y ∧ y < x + δt → y ∈ t
y : ℝ
h1 : x - min δs δt < y
h2 : y < x + min δs δt
⊢ y ∈ s ∩ t

State before:
case right.intro
X : Type
s t : Set ℝ
hs✝ : IsOpen s
ht✝ : IsOpen t
x : ℝ
hx : x ∈ s ∩ t
δs : ℝ
δspos : δs > 0
hs : ∀ (y : ℝ), x - δs < y ∧ y < x + δs → y ∈ s
δt : ℝ
δtpos : δt > 0
ht : ∀ (y : ℝ), x - δt < y ∧ y < x + δt → y ∈ t
y : ℝ
h1 : x - min δs δt < y
h2 : y < x + min δs δt
⊢ y ∈ s ∩ t
Tactic:
constructor
State after:
case right.intro.left
X : Type
s t : Set ℝ
hs✝ : IsOpen s
ht✝ : IsOpen t
x : ℝ
hx : x ∈ s ∩ t
δs : ℝ
δspos : δs > 0
hs : ∀ (y : ℝ), x - δs < y ∧ y < x + δs → y ∈ s
δt : ℝ
δtpos : δt > 0
ht : ∀ (y : ℝ), x - δt < y ∧ y < x + δt → y ∈ t
y : ℝ
h1 : x - min δs δt < y
h2 : y < x + min δs δt
⊢ y ∈ s

case right.intro.right
X : Type
s t : Set ℝ
hs✝ : IsOpen s
ht✝ : IsOpen t
x : ℝ
hx : x ∈ s ∩ t
δs : ℝ
δspos : δs > 0
hs : ∀ (y : ℝ), x - δs < y ∧ y < x + δs → y ∈ s
δt : ℝ
δtpos : δt > 0
ht : ∀ (y : ℝ), x - δt < y ∧ y < x + δt → y ∈ t
y : ℝ
h1 : x - min δs δt < y
h2 : y < x + min δs δt
⊢ y ∈ t

State before:
X : Type
s t : Set ℝ
hs : IsOpen s
ht : IsOpen t
x : ℝ
hx : x ∈ s ∩ t
⊢ x ∈ s
Tactic:
aesop
State after:
no goals

State before:
X : Type
s t : Set ℝ
hs✝ : IsOpen s
ht : IsOpen t
x : ℝ
hx : x ∈ s ∩ t
δs : ℝ
δspos : δs > 0
hs : ∀ (y : ℝ), x - δs < y ∧ y < x + δs → y ∈ s
⊢ x ∈ t
Tactic:
aesop
State after:
no goals

State before:
X : Type
s t : Set ℝ
hs✝ : IsOpen s
ht✝ : IsOpen t
x : ℝ
hx : x ∈ s ∩ t
δs : ℝ
δspos : δs > 0
hs : ∀ (y : ℝ), x - δs < y ∧ y < x + δs → y ∈ s
δt : ℝ
δtpos : δt > 0
ht : ∀ (y : ℝ), x - δt < y ∧ y < x + δt → y ∈ t
⊢ min δs δt > 0
Tactic:
positivity
State after:
no goals

State before:
case right.intro.left
X : Type
s t : Set ℝ
hs✝ : IsOpen s
ht✝ : IsOpen t
x : ℝ
hx : x ∈ s ∩ t
δs : ℝ
δspos : δs > 0
hs : ∀ (y : ℝ), x - δs < y ∧ y < x + δs → y ∈ s
δt : ℝ
δtpos : δt > 0
ht : ∀ (y : ℝ), x - δt < y ∧ y < x + δt → y ∈ t
y : ℝ
h1 : x - min δs δt < y
h2 : y < x + min δs δt
⊢ y ∈ s
Tactic:
apply hs
State after:
case right.intro.left.a
X : Type
s t : Set ℝ
hs✝ : IsOpen s
ht✝ : IsOpen t
x : ℝ
hx : x ∈ s ∩ t
δs : ℝ
δspos : δs > 0
hs : ∀ (y : ℝ), x - δs < y ∧ y < x + δs → y ∈ s
δt : ℝ
δtpos : δt > 0
ht : ∀ (y : ℝ), x - δt < y ∧ y < x + δt → y ∈ t
y : ℝ
h1 : x - min δs δt < y
h2 : y < x + min δs δt
⊢ x - δs < y ∧ y < x + δs

State before:
case right.intro.left.a
X : Type
s t : Set ℝ
hs✝ : IsOpen s
ht✝ : IsOpen t
x : ℝ
hx : x ∈ s ∩ t
δs : ℝ
δspos : δs > 0
hs : ∀ (y : ℝ), x - δs < y ∧ y < x + δs → y ∈ s
δt : ℝ
δtpos : δt > 0
ht : ∀ (y : ℝ), x - δt < y ∧ y < x + δt → y ∈ t
y : ℝ
h1 : x - min δs δt < y
h2 : y < x + min δs δt
⊢ x - δs < y ∧ y < x + δs
Tactic:
have foo : min δs δt ≤ δs := min_le_left δs δt
State after:
case right.intro.left.a
X : Type
s t : Set ℝ
hs✝ : IsOpen s
ht✝ : IsOpen t
x : ℝ
hx : x ∈ s ∩ t
δs : ℝ
δspos : δs > 0
hs : ∀ (y : ℝ), x - δs < y ∧ y < x + δs → y ∈ s
δt : ℝ
δtpos : δt > 0
ht : ∀ (y : ℝ), x - δt < y ∧ y < x + δt → y ∈ t
y : ℝ
h1 : x - min δs δt < y
h2 : y < x + min δs δt
foo : min δs δt ≤ δs
⊢ x - δs < y ∧ y < x + δs

State before:
case right.intro.left.a
X : Type
s t : Set ℝ
hs✝ : IsOpen s
ht✝ : IsOpen t
x : ℝ
hx : x ∈ s ∩ t
δs : ℝ
δspos : δs > 0
hs : ∀ (y : ℝ), x - δs < y ∧ y < x + δs → y ∈ s
δt : ℝ
δtpos : δt > 0
ht : ∀ (y : ℝ), x - δt < y ∧ y < x + δt → y ∈ t
y : ℝ
h1 : x - min δs δt < y
h2 : y < x + min δs δt
foo : min δs δt ≤ δs
⊢ x - δs < y ∧ y < x + δs
Tactic:
constructor <;> linarith
State after:
no goals

State before:
case right.intro.right
X : Type
s t : Set ℝ
hs✝ : IsOpen s
ht✝ : IsOpen t
x : ℝ
hx : x ∈ s ∩ t
δs : ℝ
δspos : δs > 0
hs : ∀ (y : ℝ), x - δs < y ∧ y < x + δs → y ∈ s
δt : ℝ
δtpos : δt > 0
ht : ∀ (y : ℝ), x - δt < y ∧ y < x + δt → y ∈ t
y : ℝ
h1 : x - min δs δt < y
h2 : y < x + min δs δt
⊢ y ∈ t
Tactic:
apply ht
State after:
case right.intro.right.a
X : Type
s t : Set ℝ
hs✝ : IsOpen s
ht✝ : IsOpen t
x : ℝ
hx : x ∈ s ∩ t
δs : ℝ
δspos : δs > 0
hs : ∀ (y : ℝ), x - δs < y ∧ y < x + δs → y ∈ s
δt : ℝ
δtpos : δt > 0
ht : ∀ (y : ℝ), x - δt < y ∧ y < x + δt → y ∈ t
y : ℝ
h1 : x - min δs δt < y
h2 : y < x + min δs δt
⊢ x - δt < y ∧ y < x + δt

State before:
case right.intro.right.a
X : Type
s t : Set ℝ
hs✝ : IsOpen s
ht✝ : IsOpen t
x : ℝ
hx : x ∈ s ∩ t
δs : ℝ
δspos : δs > 0
hs : ∀ (y : ℝ), x - δs < y ∧ y < x + δs → y ∈ s
δt : ℝ
δtpos : δt > 0
ht : ∀ (y : ℝ), x - δt < y ∧ y < x + δt → y ∈ t
y : ℝ
h1 : x - min δs δt < y
h2 : y < x + min δs δt
⊢ x - δt < y ∧ y < x + δt
Tactic:
have foo : min δs δt ≤ δt := min_le_right δs δt
State after:
case right.intro.right.a
X : Type
s t : Set ℝ
hs✝ : IsOpen s
ht✝ : IsOpen t
x : ℝ
hx : x ∈ s ∩ t
δs : ℝ
δspos : δs > 0
hs : ∀ (y : ℝ), x - δs < y ∧ y < x + δs → y ∈ s
δt : ℝ
δtpos : δt > 0
ht : ∀ (y : ℝ), x - δt < y ∧ y < x + δt → y ∈ t
y : ℝ
h1 : x - min δs δt < y
h2 : y < x + min δs δt
foo : min δs δt ≤ δt
⊢ x - δt < y ∧ y < x + δt

State before:
case right.intro.right.a
X : Type
s t : Set ℝ
hs✝ : IsOpen s
ht✝ : IsOpen t
x : ℝ
hx : x ∈ s ∩ t
δs : ℝ
δspos : δs > 0
hs : ∀ (y : ℝ), x - δs < y ∧ y < x + δs → y ∈ s
δt : ℝ
δtpos : δt > 0
ht : ∀ (y : ℝ), x - δt < y ∧ y < x + δt → y ∈ t
y : ℝ
h1 : x - min δs δt < y
h2 : y < x + min δs δt
foo : min δs δt ≤ δt
⊢ x - δt < y ∧ y < x + δt
Tactic:
constructor <;> linarith
State after:
no goals