Theorem: square_area_not_subset_circle_area (meetings/ex1.lean)

State before:
⊢ ¬Set.Icc (-1) 1 ×ˢ Set.Icc (-1) 1 ⊆ {p | p.1 ^ 2 + p.2 ^ 2 < 1}
Tactic:
intro sub
State after:
sub : Set.Icc (-1) 1 ×ˢ Set.Icc (-1) 1 ⊆ {p | p.1 ^ 2 + p.2 ^ 2 < 1}
⊢ False

State before:
sub : Set.Icc (-1) 1 ×ˢ Set.Icc (-1) 1 ⊆ {p | p.1 ^ 2 + p.2 ^ 2 < 1}
⊢ False
Tactic:
simp at *
State after:
sub : Set.Icc (-1, -1) (1, 1) ⊆ {p | p.1 ^ 2 + p.2 ^ 2 < 1}
⊢ False

State before:
sub : Set.Icc (-1, -1) (1, 1) ⊆ {p | p.1 ^ 2 + p.2 ^ 2 < 1}
⊢ False
Tactic:
have hel : ((-1, -1) : ℝ × ℝ) ∈ Set.Icc (-1, -1) (1, 1) := by
  simp
State after:
sub : Set.Icc (-1, -1) (1, 1) ⊆ {p | p.1 ^ 2 + p.2 ^ 2 < 1}
hel : (-1, -1) ∈ Set.Icc (-1, -1) (1, 1)
⊢ False

State before:
sub : Set.Icc (-1, -1) (1, 1) ⊆ {p | p.1 ^ 2 + p.2 ^ 2 < 1}
hel : (-1, -1) ∈ Set.Icc (-1, -1) (1, 1)
⊢ False
Tactic:
specialize sub hel
State after:
hel : (-1, -1) ∈ Set.Icc (-1, -1) (1, 1)
sub : (-1, -1) ∈ {p | p.1 ^ 2 + p.2 ^ 2 < 1}
⊢ False

State before:
hel : (-1, -1) ∈ Set.Icc (-1, -1) (1, 1)
sub : (-1, -1) ∈ {p | p.1 ^ 2 + p.2 ^ 2 < 1}
⊢ False
Tactic:
simp at sub
State after:
hel : (-1, -1) ∈ Set.Icc (-1, -1) (1, 1)
sub : 1 < 0
⊢ False

State before:
hel : (-1, -1) ∈ Set.Icc (-1, -1) (1, 1)
sub : 1 < 0
⊢ False
Tactic:
linarith
State after:
no goals

State before:
sub : Set.Icc (-1, -1) (1, 1) ⊆ {p | p.1 ^ 2 + p.2 ^ 2 < 1}
⊢ (-1, -1) ∈ Set.Icc (-1, -1) (1, 1)
Tactic:
simp
State after:
no goals