Theorem: inter_rectangles (meetings/ex1.lean)

State before:
⊢ ⋂ α ∈ Set.Icc 0 1, rectangle α = Set.singleton (1, 0)
Tactic:
simp only [ge_iff_le, zero_le_one, not_true, gt_iff_lt, Set.mem_Icc]
State after:
⊢ ⋂ α, ⋂ (_ : 0 ≤ α ∧ α ≤ 1), rectangle α = Set.singleton (1, 0)

State before:
⊢ ⋂ α, ⋂ (_ : 0 ≤ α ∧ α ≤ 1), rectangle α = Set.singleton (1, 0)
Tactic:
simp_rw [rectangle, Set.ext_iff]
State after:
⊢ ∀ (x : ℝ × ℝ), x ∈ ⋂ α, ⋂ (_ : 0 ≤ α ∧ α ≤ 1), Set.Icc α 1 ×ˢ Set.Icc 0 α ↔ x ∈ Set.singleton (1, 0)

State before:
⊢ ∀ (x : ℝ × ℝ), x ∈ ⋂ α, ⋂ (_ : 0 ≤ α ∧ α ≤ 1), Set.Icc α 1 ×ˢ Set.Icc 0 α ↔ x ∈ Set.singleton (1, 0)
Tactic:
intro x
State after:
x : ℝ × ℝ
⊢ x ∈ ⋂ α, ⋂ (_ : 0 ≤ α ∧ α ≤ 1), Set.Icc α 1 ×ˢ Set.Icc 0 α ↔ x ∈ Set.singleton (1, 0)

State before:
x : ℝ × ℝ
⊢ x ∈ ⋂ α, ⋂ (_ : 0 ≤ α ∧ α ≤ 1), Set.Icc α 1 ×ˢ Set.Icc 0 α ↔ x ∈ Set.singleton (1, 0)
Tactic:
simp only [ge_iff_le, not_le, gt_iff_lt, Set.Icc_prod_Icc, Prod.mk_le_mk, not_and, Prod.mk_lt_mk, Set.mem_iInter, Set.mem_Icc, and_imp]
State after:
x : ℝ × ℝ
⊢ (∀ (i : ℝ), 0 ≤ i → i ≤ 1 → (i, 0) ≤ x ∧ x ≤ (1, i)) ↔ x ∈ Set.singleton (1, 0)

State before:
x : ℝ × ℝ
⊢ (∀ (i : ℝ), 0 ≤ i → i ≤ 1 → (i, 0) ≤ x ∧ x ≤ (1, i)) ↔ x ∈ Set.singleton (1, 0)
Tactic:
constructor
State after:
case mp
x : ℝ × ℝ
⊢ (∀ (i : ℝ), 0 ≤ i → i ≤ 1 → (i, 0) ≤ x ∧ x ≤ (1, i)) → x ∈ Set.singleton (1, 0)

case mpr
x : ℝ × ℝ
⊢ x ∈ Set.singleton (1, 0) → ∀ (i : ℝ), 0 ≤ i → i ≤ 1 → (i, 0) ≤ x ∧ x ≤ (1, i)

State before:
case mp
x : ℝ × ℝ
⊢ (∀ (i : ℝ), 0 ≤ i → i ≤ 1 → (i, 0) ≤ x ∧ x ≤ (1, i)) → x ∈ Set.singleton (1, 0)
Tactic:
intro imp
State after:
case mp
x : ℝ × ℝ
imp : ∀ (i : ℝ), 0 ≤ i → i ≤ 1 → (i, 0) ≤ x ∧ x ≤ (1, i)
⊢ x ∈ Set.singleton (1, 0)

State before:
case mp
x : ℝ × ℝ
imp : ∀ (i : ℝ), 0 ≤ i → i ≤ 1 → (i, 0) ≤ x ∧ x ≤ (1, i)
⊢ x ∈ Set.singleton (1, 0)
Tactic:
have h1 := imp 0
State after:
case mp
x : ℝ × ℝ
imp : ∀ (i : ℝ), 0 ≤ i → i ≤ 1 → (i, 0) ≤ x ∧ x ≤ (1, i)
h1 : 0 ≤ 0 → 0 ≤ 1 → (0, 0) ≤ x ∧ x ≤ (1, 0)
⊢ x ∈ Set.singleton (1, 0)

State before:
case mp
x : ℝ × ℝ
imp : ∀ (i : ℝ), 0 ≤ i → i ≤ 1 → (i, 0) ≤ x ∧ x ≤ (1, i)
h1 : 0 ≤ 0 → 0 ≤ 1 → (0, 0) ≤ x ∧ x ≤ (1, 0)
⊢ x ∈ Set.singleton (1, 0)
Tactic:
have h2 := imp 1
State after:
case mp
x : ℝ × ℝ
imp : ∀ (i : ℝ), 0 ≤ i → i ≤ 1 → (i, 0) ≤ x ∧ x ≤ (1, i)
h1 : 0 ≤ 0 → 0 ≤ 1 → (0, 0) ≤ x ∧ x ≤ (1, 0)
h2 : 0 ≤ 1 → 1 ≤ 1 → (1, 0) ≤ x ∧ x ≤ (1, 1)
⊢ x ∈ Set.singleton (1, 0)

State before:
case mp
x : ℝ × ℝ
imp : ∀ (i : ℝ), 0 ≤ i → i ≤ 1 → (i, 0) ≤ x ∧ x ≤ (1, i)
h1 : 0 ≤ 0 → 0 ≤ 1 → (0, 0) ≤ x ∧ x ≤ (1, 0)
h2 : 0 ≤ 1 → 1 ≤ 1 → (1, 0) ≤ x ∧ x ≤ (1, 1)
⊢ x ∈ Set.singleton (1, 0)
Tactic:
simp [Prod.le_def] at *
State after:
case mp
x : ℝ × ℝ
imp : ∀ (i : ℝ), 0 ≤ i → i ≤ 1 → (i ≤ x.1 ∧ 0 ≤ x.2) ∧ x.1 ≤ 1 ∧ x.2 ≤ i
h1 : (0 ≤ x.1 ∧ 0 ≤ x.2) ∧ x.1 ≤ 1 ∧ x.2 ≤ 0
h2 : (1 ≤ x.1 ∧ 0 ≤ x.2) ∧ x.1 ≤ 1 ∧ x.2 ≤ 1
⊢ x ∈ Set.singleton (1, 0)

State before:
case mp
x : ℝ × ℝ
imp : ∀ (i : ℝ), 0 ≤ i → i ≤ 1 → (i ≤ x.1 ∧ 0 ≤ x.2) ∧ x.1 ≤ 1 ∧ x.2 ≤ i
h1 : (0 ≤ x.1 ∧ 0 ≤ x.2) ∧ x.1 ≤ 1 ∧ x.2 ≤ 0
h2 : (1 ≤ x.1 ∧ 0 ≤ x.2) ∧ x.1 ≤ 1 ∧ x.2 ≤ 1
⊢ x ∈ Set.singleton (1, 0)
Tactic:
have hx1 : x.1 = 1 := by
  linarith
State after:
case mp
x : ℝ × ℝ
imp : ∀ (i : ℝ), 0 ≤ i → i ≤ 1 → (i ≤ x.1 ∧ 0 ≤ x.2) ∧ x.1 ≤ 1 ∧ x.2 ≤ i
h1 : (0 ≤ x.1 ∧ 0 ≤ x.2) ∧ x.1 ≤ 1 ∧ x.2 ≤ 0
h2 : (1 ≤ x.1 ∧ 0 ≤ x.2) ∧ x.1 ≤ 1 ∧ x.2 ≤ 1
hx1 : x.1 = 1
⊢ x ∈ Set.singleton (1, 0)

State before:
case mp
x : ℝ × ℝ
imp : ∀ (i : ℝ), 0 ≤ i → i ≤ 1 → (i ≤ x.1 ∧ 0 ≤ x.2) ∧ x.1 ≤ 1 ∧ x.2 ≤ i
h1 : (0 ≤ x.1 ∧ 0 ≤ x.2) ∧ x.1 ≤ 1 ∧ x.2 ≤ 0
h2 : (1 ≤ x.1 ∧ 0 ≤ x.2) ∧ x.1 ≤ 1 ∧ x.2 ≤ 1
hx1 : x.1 = 1
⊢ x ∈ Set.singleton (1, 0)
Tactic:
have hx2 : x.2 = 0 := by
  linarith
State after:
case mp
x : ℝ × ℝ
imp : ∀ (i : ℝ), 0 ≤ i → i ≤ 1 → (i ≤ x.1 ∧ 0 ≤ x.2) ∧ x.1 ≤ 1 ∧ x.2 ≤ i
h1 : (0 ≤ x.1 ∧ 0 ≤ x.2) ∧ x.1 ≤ 1 ∧ x.2 ≤ 0
h2 : (1 ≤ x.1 ∧ 0 ≤ x.2) ∧ x.1 ≤ 1 ∧ x.2 ≤ 1
hx1 : x.1 = 1
hx2 : x.2 = 0
⊢ x ∈ Set.singleton (1, 0)

State before:
case mp
x : ℝ × ℝ
imp : ∀ (i : ℝ), 0 ≤ i → i ≤ 1 → (i ≤ x.1 ∧ 0 ≤ x.2) ∧ x.1 ≤ 1 ∧ x.2 ≤ i
h1 : (0 ≤ x.1 ∧ 0 ≤ x.2) ∧ x.1 ≤ 1 ∧ x.2 ≤ 0
h2 : (1 ≤ x.1 ∧ 0 ≤ x.2) ∧ x.1 ≤ 1 ∧ x.2 ≤ 1
hx1 : x.1 = 1
hx2 : x.2 = 0
⊢ x ∈ Set.singleton (1, 0)
Tactic:
exact Set.mem_singleton_of_eq (Prod.ext hx1 hx2)
State after:
no goals

State before:
x : ℝ × ℝ
imp : ∀ (i : ℝ), 0 ≤ i → i ≤ 1 → (i ≤ x.1 ∧ 0 ≤ x.2) ∧ x.1 ≤ 1 ∧ x.2 ≤ i
h1 : (0 ≤ x.1 ∧ 0 ≤ x.2) ∧ x.1 ≤ 1 ∧ x.2 ≤ 0
h2 : (1 ≤ x.1 ∧ 0 ≤ x.2) ∧ x.1 ≤ 1 ∧ x.2 ≤ 1
⊢ x.1 = 1
Tactic:
linarith
State after:
no goals

State before:
x : ℝ × ℝ
imp : ∀ (i : ℝ), 0 ≤ i → i ≤ 1 → (i ≤ x.1 ∧ 0 ≤ x.2) ∧ x.1 ≤ 1 ∧ x.2 ≤ i
h1 : (0 ≤ x.1 ∧ 0 ≤ x.2) ∧ x.1 ≤ 1 ∧ x.2 ≤ 0
h2 : (1 ≤ x.1 ∧ 0 ≤ x.2) ∧ x.1 ≤ 1 ∧ x.2 ≤ 1
hx1 : x.1 = 1
⊢ x.2 = 0
Tactic:
linarith
State after:
no goals

State before:
case mpr
x : ℝ × ℝ
⊢ x ∈ Set.singleton (1, 0) → ∀ (i : ℝ), 0 ≤ i → i ≤ 1 → (i, 0) ≤ x ∧ x ≤ (1, i)
Tactic:
intros mem i hle0i hlei1
State after:
case mpr
x : ℝ × ℝ
mem : x ∈ Set.singleton (1, 0)
i : ℝ
hle0i : 0 ≤ i
hlei1 : i ≤ 1
⊢ (i, 0) ≤ x ∧ x ≤ (1, i)

State before:
case mpr
x : ℝ × ℝ
mem : x ∈ Set.singleton (1, 0)
i : ℝ
hle0i : 0 ≤ i
hlei1 : i ≤ 1
⊢ (i, 0) ≤ x ∧ x ≤ (1, i)
Tactic:
have mem' := Set.eq_of_mem_singleton mem
State after:
case mpr
x : ℝ × ℝ
mem : x ∈ Set.singleton (1, 0)
i : ℝ
hle0i : 0 ≤ i
hlei1 : i ≤ 1
mem' : x = (1, 0)
⊢ (i, 0) ≤ x ∧ x ≤ (1, i)

State before:
case mpr
x : ℝ × ℝ
mem : x ∈ Set.singleton (1, 0)
i : ℝ
hle0i : 0 ≤ i
hlei1 : i ≤ 1
mem' : x = (1, 0)
⊢ (i, 0) ≤ x ∧ x ≤ (1, i)
Tactic:
constructor
State after:
case mpr.left
x : ℝ × ℝ
mem : x ∈ Set.singleton (1, 0)
i : ℝ
hle0i : 0 ≤ i
hlei1 : i ≤ 1
mem' : x = (1, 0)
⊢ (i, 0) ≤ x

case mpr.right
x : ℝ × ℝ
mem : x ∈ Set.singleton (1, 0)
i : ℝ
hle0i : 0 ≤ i
hlei1 : i ≤ 1
mem' : x = (1, 0)
⊢ x ≤ (1, i)

State before:
case mpr.left
x : ℝ × ℝ
mem : x ∈ Set.singleton (1, 0)
i : ℝ
hle0i : 0 ≤ i
hlei1 : i ≤ 1
mem' : x = (1, 0)
⊢ (i, 0) ≤ x
Tactic:
rw [mem']
State after:
case mpr.left
x : ℝ × ℝ
mem : x ∈ Set.singleton (1, 0)
i : ℝ
hle0i : 0 ≤ i
hlei1 : i ≤ 1
mem' : x = (1, 0)
⊢ (i, 0) ≤ (1, 0)

State before:
case mpr.left
x : ℝ × ℝ
mem : x ∈ Set.singleton (1, 0)
i : ℝ
hle0i : 0 ≤ i
hlei1 : i ≤ 1
mem' : x = (1, 0)
⊢ (i, 0) ≤ (1, 0)
Tactic:
simp [Prod.le_def]
State after:
case mpr.left
x : ℝ × ℝ
mem : x ∈ Set.singleton (1, 0)
i : ℝ
hle0i : 0 ≤ i
hlei1 : i ≤ 1
mem' : x = (1, 0)
⊢ i ≤ 1

State before:
case mpr.left
x : ℝ × ℝ
mem : x ∈ Set.singleton (1, 0)
i : ℝ
hle0i : 0 ≤ i
hlei1 : i ≤ 1
mem' : x = (1, 0)
⊢ i ≤ 1
Tactic:
exact hlei1
State after:
no goals

State before:
case mpr.right
x : ℝ × ℝ
mem : x ∈ Set.singleton (1, 0)
i : ℝ
hle0i : 0 ≤ i
hlei1 : i ≤ 1
mem' : x = (1, 0)
⊢ x ≤ (1, i)
Tactic:
rw [mem']
State after:
case mpr.right
x : ℝ × ℝ
mem : x ∈ Set.singleton (1, 0)
i : ℝ
hle0i : 0 ≤ i
hlei1 : i ≤ 1
mem' : x = (1, 0)
⊢ (1, 0) ≤ (1, i)

State before:
case mpr.right
x : ℝ × ℝ
mem : x ∈ Set.singleton (1, 0)
i : ℝ
hle0i : 0 ≤ i
hlei1 : i ≤ 1
mem' : x = (1, 0)
⊢ (1, 0) ≤ (1, i)
Tactic:
simp
State after:
case mpr.right
x : ℝ × ℝ
mem : x ∈ Set.singleton (1, 0)
i : ℝ
hle0i : 0 ≤ i
hlei1 : i ≤ 1
mem' : x = (1, 0)
⊢ 0 ≤ i

State before:
case mpr.right
x : ℝ × ℝ
mem : x ∈ Set.singleton (1, 0)
i : ℝ
hle0i : 0 ≤ i
hlei1 : i ≤ 1
mem' : x = (1, 0)
⊢ 0 ≤ i
Tactic:
exact hle0i
State after:
no goals