Theorem: circle_area_subset_square_area (meetings/ex1.lean)

State before:
⊢ {p | p.1 ^ 2 + p.2 ^ 2 < 1} ⊆ Set.Icc (-1) 1 ×ˢ Set.Icc (-1) 1
Tactic:
intros p hmem
State after:
p : ℝ × ℝ
hmem : p ∈ {p | p.1 ^ 2 + p.2 ^ 2 < 1}
⊢ p ∈ Set.Icc (-1) 1 ×ˢ Set.Icc (-1) 1

State before:
p : ℝ × ℝ
hmem : p ∈ {p | p.1 ^ 2 + p.2 ^ 2 < 1}
⊢ p ∈ Set.Icc (-1) 1 ×ˢ Set.Icc (-1) 1
Tactic:
simp at *
State after:
p : ℝ × ℝ
hmem : p.1 ^ 2 + p.2 ^ 2 < 1
⊢ (-1, -1) ≤ p ∧ p ≤ (1, 1)

State before:
p : ℝ × ℝ
hmem : p.1 ^ 2 + p.2 ^ 2 < 1
h : p.1 ^ 2 ≤ 1 ∧ p.2 ^ 2 ≤ 1
⊢ (-1, -1) ≤ p ∧ p ≤ (1, 1)
Tactic:
simp only [sq_le_one_iff_abs_le_one, abs_le] at h
State after:
p : ℝ × ℝ
hmem : p.1 ^ 2 + p.2 ^ 2 < 1
h : (-1 ≤ p.1 ∧ p.1 ≤ 1) ∧ -1 ≤ p.2 ∧ p.2 ≤ 1
⊢ (-1, -1) ≤ p ∧ p ≤ (1, 1)

State before:
p : ℝ × ℝ
hmem : p.1 ^ 2 + p.2 ^ 2 < 1
h : (-1 ≤ p.1 ∧ p.1 ≤ 1) ∧ -1 ≤ p.2 ∧ p.2 ≤ 1
⊢ (-1, -1) ≤ p ∧ p ≤ (1, 1)
Tactic:
exact ⟨⟨h.1.1, h.2.1⟩, ⟨h.1.2, h.2.2⟩⟩
State after:
no goals

State before:
p : ℝ × ℝ
hmem : p.1 ^ 2 + p.2 ^ 2 < 1
⊢ p.1 ^ 2 ≤ 1 ∧ p.2 ^ 2 ≤ 1
Tactic:
have p1nonneg := sq_nonneg (p.1)
State after:
p : ℝ × ℝ
hmem : p.1 ^ 2 + p.2 ^ 2 < 1
p1nonneg : 0 ≤ p.1 ^ 2
⊢ p.1 ^ 2 ≤ 1 ∧ p.2 ^ 2 ≤ 1

State before:
p : ℝ × ℝ
hmem : p.1 ^ 2 + p.2 ^ 2 < 1
p1nonneg : 0 ≤ p.1 ^ 2
⊢ p.1 ^ 2 ≤ 1 ∧ p.2 ^ 2 ≤ 1
Tactic:
have p2nonneg := sq_nonneg (p.2)
State after:
p : ℝ × ℝ
hmem : p.1 ^ 2 + p.2 ^ 2 < 1
p1nonneg : 0 ≤ p.1 ^ 2
p2nonneg : 0 ≤ p.2 ^ 2
⊢ p.1 ^ 2 ≤ 1 ∧ p.2 ^ 2 ≤ 1

State before:
p : ℝ × ℝ
hmem : p.1 ^ 2 + p.2 ^ 2 < 1
p1nonneg : 0 ≤ p.1 ^ 2
p2nonneg : 0 ≤ p.2 ^ 2
⊢ p.1 ^ 2 ≤ 1 ∧ p.2 ^ 2 ≤ 1
Tactic:
constructor
State after:
case left
p : ℝ × ℝ
hmem : p.1 ^ 2 + p.2 ^ 2 < 1
p1nonneg : 0 ≤ p.1 ^ 2
p2nonneg : 0 ≤ p.2 ^ 2
⊢ p.1 ^ 2 ≤ 1

case right
p : ℝ × ℝ
hmem : p.1 ^ 2 + p.2 ^ 2 < 1
p1nonneg : 0 ≤ p.1 ^ 2
p2nonneg : 0 ≤ p.2 ^ 2
⊢ p.2 ^ 2 ≤ 1

State before:
case left
p : ℝ × ℝ
hmem : p.1 ^ 2 + p.2 ^ 2 < 1
p1nonneg : 0 ≤ p.1 ^ 2
p2nonneg : 0 ≤ p.2 ^ 2
⊢ p.1 ^ 2 ≤ 1
Tactic:
linarith
State after:
no goals

State before:
case right
p : ℝ × ℝ
hmem : p.1 ^ 2 + p.2 ^ 2 < 1
p1nonneg : 0 ≤ p.1 ^ 2
p2nonneg : 0 ≤ p.2 ^ 2
⊢ p.2 ^ 2 ≤ 1
Tactic:
linarith
State after:
no goals