Theorem: preimage_fn (meetings/ex4.lean)

State before:
⊢ fn ⁻¹' Set.Icc 12 19 = Set.Icc 3 4 ∪ Set.Icc (-4) (-3)
Tactic:
ext x
State after:
case h
x : ℝ
⊢ x ∈ fn ⁻¹' Set.Icc 12 19 ↔ x ∈ Set.Icc 3 4 ∪ Set.Icc (-4) (-3)

State before:
case h
x : ℝ
⊢ x ∈ fn ⁻¹' Set.Icc 12 19 ↔ x ∈ Set.Icc 3 4 ∪ Set.Icc (-4) (-3)
Tactic:
simp only [ge_iff_le, not_le, gt_iff_lt, Set.mem_preimage, Set.mem_Icc, neg_le_neg_iff,
  neg_lt_neg_iff, Set.mem_union, fn]
State after:
case h
x : ℝ
⊢ 12 ≤ x ^ 2 + 3 ∧ x ^ 2 + 3 ≤ 19 ↔ 3 ≤ x ∧ x ≤ 4 ∨ -4 ≤ x ∧ x ≤ -3

State before:
case h
x : ℝ
⊢ 12 ≤ x ^ 2 + 3 ∧ x ^ 2 + 3 ≤ 19 ↔ 3 ≤ x ∧ x ≤ 4 ∨ -4 ≤ x ∧ x ≤ -3
Tactic:
constructor
State after:
case h.mp
x : ℝ
⊢ 12 ≤ x ^ 2 + 3 ∧ x ^ 2 + 3 ≤ 19 → 3 ≤ x ∧ x ≤ 4 ∨ -4 ≤ x ∧ x ≤ -3

case h.mpr
x : ℝ
⊢ 3 ≤ x ∧ x ≤ 4 ∨ -4 ≤ x ∧ x ≤ -3 → 12 ≤ x ^ 2 + 3 ∧ x ^ 2 + 3 ≤ 19

State before:
case h.mp
x : ℝ
⊢ 12 ≤ x ^ 2 + 3 ∧ x ^ 2 + 3 ≤ 19 → 3 ≤ x ∧ x ≤ 4 ∨ -4 ≤ x ∧ x ≤ -3
Tactic:
intro hlege
State after:
case h.mp
x : ℝ
hlege : 12 ≤ x ^ 2 + 3 ∧ x ^ 2 + 3 ≤ 19
⊢ 3 ≤ x ∧ x ≤ 4 ∨ -4 ≤ x ∧ x ≤ -3

State before:
case h.mp
x : ℝ
hlege : 12 ≤ x ^ 2 + 3 ∧ x ^ 2 + 3 ≤ 19
⊢ 3 ≤ x ∧ x ≤ 4 ∨ -4 ≤ x ∧ x ≤ -3
Tactic:
rcases hlege with ⟨h12le, h19ge⟩
State after:
case h.mp.intro
x : ℝ
h12le : 12 ≤ x ^ 2 + 3
h19ge : x ^ 2 + 3 ≤ 19
⊢ 3 ≤ x ∧ x ≤ 4 ∨ -4 ≤ x ∧ x ≤ -3

State before:
case h.mp.intro
x : ℝ
h12le : 12 ≤ x ^ 2 + 3
h19ge : x ^ 2 + 3 ≤ 19
⊢ 3 ≤ x ∧ x ≤ 4 ∨ -4 ≤ x ∧ x ≤ -3
Tactic:
have heq12 : (12 : ℝ) = (3^2) + 3 := by ring
State after:
case h.mp.intro
x : ℝ
h12le : 12 ≤ x ^ 2 + 3
h19ge : x ^ 2 + 3 ≤ 19
heq12 : 12 = 3 ^ 2 + 3
⊢ 3 ≤ x ∧ x ≤ 4 ∨ -4 ≤ x ∧ x ≤ -3

State before:
case h.mp.intro
x : ℝ
h12le : 12 ≤ x ^ 2 + 3
h19ge : x ^ 2 + 3 ≤ 19
heq12 : 12 = 3 ^ 2 + 3
⊢ 3 ≤ x ∧ x ≤ 4 ∨ -4 ≤ x ∧ x ≤ -3
Tactic:
rw [heq12, add_le_add_iff_right, sq_le_sq, abs_of_pos (by simp), le_abs, le_neg] at h12le
State after:
case h.mp.intro
x : ℝ
h12le : 3 ≤ x ∨ x ≤ -3
h19ge : x ^ 2 + 3 ≤ 19
heq12 : 12 = 3 ^ 2 + 3
⊢ 3 ≤ x ∧ x ≤ 4 ∨ -4 ≤ x ∧ x ≤ -3

State before:
case h.mp.intro
x : ℝ
h12le : 3 ≤ x ∨ x ≤ -3
h19ge : x ^ 2 + 3 ≤ 19
heq12 : 12 = 3 ^ 2 + 3
⊢ 3 ≤ x ∧ x ≤ 4 ∨ -4 ≤ x ∧ x ≤ -3
Tactic:
have heq19 : (19 : ℝ) = (4^2) + 3 := by ring
State after:
case h.mp.intro
x : ℝ
h12le : 3 ≤ x ∨ x ≤ -3
h19ge : x ^ 2 + 3 ≤ 19
heq12 : 12 = 3 ^ 2 + 3
heq19 : 19 = 4 ^ 2 + 3
⊢ 3 ≤ x ∧ x ≤ 4 ∨ -4 ≤ x ∧ x ≤ -3

State before:
case h.mp.intro
x : ℝ
h12le : 3 ≤ x ∨ x ≤ -3
h19ge : x ^ 2 + 3 ≤ 19
heq12 : 12 = 3 ^ 2 + 3
heq19 : 19 = 4 ^ 2 + 3
⊢ 3 ≤ x ∧ x ≤ 4 ∨ -4 ≤ x ∧ x ≤ -3
Tactic:
have lt04 : (0 : ℝ) < 4 := by simp
State after:
case h.mp.intro
x : ℝ
h12le : 3 ≤ x ∨ x ≤ -3
h19ge : x ^ 2 + 3 ≤ 19
heq12 : 12 = 3 ^ 2 + 3
heq19 : 19 = 4 ^ 2 + 3
lt04 : 0 < 4
⊢ 3 ≤ x ∧ x ≤ 4 ∨ -4 ≤ x ∧ x ≤ -3

State before:
case h.mp.intro
x : ℝ
h12le : 3 ≤ x ∨ x ≤ -3
h19ge : x ^ 2 + 3 ≤ 19
heq12 : 12 = 3 ^ 2 + 3
heq19 : 19 = 4 ^ 2 + 3
lt04 : 0 < 4
⊢ 3 ≤ x ∧ x ≤ 4 ∨ -4 ≤ x ∧ x ≤ -3
Tactic:
rw [heq19, add_le_add_iff_right, sq_le_sq, abs_of_pos lt04, abs_le] at h19ge
State after:
case h.mp.intro
x : ℝ
h12le : 3 ≤ x ∨ x ≤ -3
h19ge : -4 ≤ x ∧ x ≤ 4
heq12 : 12 = 3 ^ 2 + 3
heq19 : 19 = 4 ^ 2 + 3
lt04 : 0 < 4
⊢ 3 ≤ x ∧ x ≤ 4 ∨ -4 ≤ x ∧ x ≤ -3

State before:
case h.mp.intro
x : ℝ
h12le : 3 ≤ x ∨ x ≤ -3
h19ge : -4 ≤ x ∧ x ≤ 4
heq12 : 12 = 3 ^ 2 + 3
heq19 : 19 = 4 ^ 2 + 3
lt04 : 0 < 4
⊢ 3 ≤ x ∧ x ≤ 4 ∨ -4 ≤ x ∧ x ≤ -3
Tactic:
rcases h12le with (h3le | hm3ge)
State after:
case h.mp.intro.inl
x : ℝ
h19ge : -4 ≤ x ∧ x ≤ 4
heq12 : 12 = 3 ^ 2 + 3
heq19 : 19 = 4 ^ 2 + 3
lt04 : 0 < 4
h3le : 3 ≤ x
⊢ 3 ≤ x ∧ x ≤ 4 ∨ -4 ≤ x ∧ x ≤ -3

case h.mp.intro.inr
x : ℝ
h19ge : -4 ≤ x ∧ x ≤ 4
heq12 : 12 = 3 ^ 2 + 3
heq19 : 19 = 4 ^ 2 + 3
lt04 : 0 < 4
hm3ge : x ≤ -3
⊢ 3 ≤ x ∧ x ≤ 4 ∨ -4 ≤ x ∧ x ≤ -3

State before:
x : ℝ
h12le : 12 ≤ x ^ 2 + 3
h19ge : x ^ 2 + 3 ≤ 19
⊢ 12 = 3 ^ 2 + 3
Tactic:
ring
State after:
no goals

State before:
x : ℝ
h12le : |3| ≤ |x|
h19ge : x ^ 2 + 3 ≤ 19
heq12 : 12 = 3 ^ 2 + 3
⊢ 0 < 3
Tactic:
simp
State after:
no goals

State before:
x : ℝ
h12le : 3 ≤ x ∨ x ≤ -3
h19ge : x ^ 2 + 3 ≤ 19
heq12 : 12 = 3 ^ 2 + 3
⊢ 19 = 4 ^ 2 + 3
Tactic:
ring
State after:
no goals

State before:
x : ℝ
h12le : 3 ≤ x ∨ x ≤ -3
h19ge : x ^ 2 + 3 ≤ 19
heq12 : 12 = 3 ^ 2 + 3
heq19 : 19 = 4 ^ 2 + 3
⊢ 0 < 4
Tactic:
simp
State after:
no goals

State before:
case h.mp.intro.inl
x : ℝ
h19ge : -4 ≤ x ∧ x ≤ 4
heq12 : 12 = 3 ^ 2 + 3
heq19 : 19 = 4 ^ 2 + 3
lt04 : 0 < 4
h3le : 3 ≤ x
⊢ 3 ≤ x ∧ x ≤ 4 ∨ -4 ≤ x ∧ x ≤ -3
Tactic:
left
State after:
case h.mp.intro.inl.h
x : ℝ
h19ge : -4 ≤ x ∧ x ≤ 4
heq12 : 12 = 3 ^ 2 + 3
heq19 : 19 = 4 ^ 2 + 3
lt04 : 0 < 4
h3le : 3 ≤ x
⊢ 3 ≤ x ∧ x ≤ 4

State before:
case h.mp.intro.inl.h
x : ℝ
h19ge : -4 ≤ x ∧ x ≤ 4
heq12 : 12 = 3 ^ 2 + 3
heq19 : 19 = 4 ^ 2 + 3
lt04 : 0 < 4
h3le : 3 ≤ x
⊢ 3 ≤ x ∧ x ≤ 4
Tactic:
exact ⟨h3le, h19ge.2⟩
State after:
no goals

State before:
case h.mp.intro.inr
x : ℝ
h19ge : -4 ≤ x ∧ x ≤ 4
heq12 : 12 = 3 ^ 2 + 3
heq19 : 19 = 4 ^ 2 + 3
lt04 : 0 < 4
hm3ge : x ≤ -3
⊢ 3 ≤ x ∧ x ≤ 4 ∨ -4 ≤ x ∧ x ≤ -3
Tactic:
right
State after:
case h.mp.intro.inr.h
x : ℝ
h19ge : -4 ≤ x ∧ x ≤ 4
heq12 : 12 = 3 ^ 2 + 3
heq19 : 19 = 4 ^ 2 + 3
lt04 : 0 < 4
hm3ge : x ≤ -3
⊢ -4 ≤ x ∧ x ≤ -3

State before:
case h.mp.intro.inr.h
x : ℝ
h19ge : -4 ≤ x ∧ x ≤ 4
heq12 : 12 = 3 ^ 2 + 3
heq19 : 19 = 4 ^ 2 + 3
lt04 : 0 < 4
hm3ge : x ≤ -3
⊢ -4 ≤ x ∧ x ≤ -3
Tactic:
exact ⟨h19ge.1, hm3ge⟩
State after:
no goals

State before:
case h.mpr
x : ℝ
⊢ 3 ≤ x ∧ x ≤ 4 ∨ -4 ≤ x ∧ x ≤ -3 → 12 ≤ x ^ 2 + 3 ∧ x ^ 2 + 3 ≤ 19
Tactic:
intro hlege
State after:
case h.mpr
x : ℝ
hlege : 3 ≤ x ∧ x ≤ 4 ∨ -4 ≤ x ∧ x ≤ -3
⊢ 12 ≤ x ^ 2 + 3 ∧ x ^ 2 + 3 ≤ 19

State before:
case h.mpr
x : ℝ
hlege : 3 ≤ x ∧ x ≤ 4 ∨ -4 ≤ x ∧ x ≤ -3
⊢ 12 ≤ x ^ 2 + 3 ∧ x ^ 2 + 3 ≤ 19
Tactic:
rcases hlege with (⟨h3le, h4ge⟩ | ⟨hm4le, hm3ge⟩)
State after:
case h.mpr.inl.intro
x : ℝ
h3le : 3 ≤ x
h4ge : x ≤ 4
⊢ 12 ≤ x ^ 2 + 3 ∧ x ^ 2 + 3 ≤ 19

case h.mpr.inr.intro
x : ℝ
hm4le : -4 ≤ x
hm3ge : x ≤ -3
⊢ 12 ≤ x ^ 2 + 3 ∧ x ^ 2 + 3 ≤ 19

State before:
case h.mpr.inl.intro
x : ℝ
h3le : 3 ≤ x
h4ge : x ≤ 4
⊢ 12 ≤ x ^ 2 + 3 ∧ x ^ 2 + 3 ≤ 19
Tactic:
constructor
State after:
case h.mpr.inl.intro.left
x : ℝ
h3le : 3 ≤ x
h4ge : x ≤ 4
⊢ 12 ≤ x ^ 2 + 3

case h.mpr.inl.intro.right
x : ℝ
h3le : 3 ≤ x
h4ge : x ≤ 4
⊢ x ^ 2 + 3 ≤ 19

State before:
case h.mpr.inl.intro.left
x : ℝ
h3le : 3 ≤ x
h4ge : x ≤ 4
⊢ 12 ≤ x ^ 2 + 3
Tactic:
nlinarith
State after:
no goals

State before:
case h.mpr.inl.intro.right
x : ℝ
h3le : 3 ≤ x
h4ge : x ≤ 4
⊢ x ^ 2 + 3 ≤ 19
Tactic:
nlinarith
State after:
no goals

State before:
case h.mpr.inr.intro
x : ℝ
hm4le : -4 ≤ x
hm3ge : x ≤ -3
⊢ 12 ≤ x ^ 2 + 3 ∧ x ^ 2 + 3 ≤ 19
Tactic:
constructor
State after:
case h.mpr.inr.intro.left
x : ℝ
hm4le : -4 ≤ x
hm3ge : x ≤ -3
⊢ 12 ≤ x ^ 2 + 3

case h.mpr.inr.intro.right
x : ℝ
hm4le : -4 ≤ x
hm3ge : x ≤ -3
⊢ x ^ 2 + 3 ≤ 19

State before:
case h.mpr.inr.intro.left
x : ℝ
hm4le : -4 ≤ x
hm3ge : x ≤ -3
⊢ 12 ≤ x ^ 2 + 3
Tactic:
nlinarith
State after:
no goals

State before:
case h.mpr.inr.intro.right
x : ℝ
hm4le : -4 ≤ x
hm3ge : x ≤ -3
⊢ x ^ 2 + 3 ≤ 19
Tactic:
nlinarith
State after:
no goals