Theorem: image_fn (meetings/ex4.lean)

State before:
⊢ fn '' Set.Icc 3 5 = Set.Icc 12 28
Tactic:
ext x
State after:
case h
x : ℝ
⊢ x ∈ fn '' Set.Icc 3 5 ↔ x ∈ Set.Icc 12 28

State before:
case h
x : ℝ
⊢ x ∈ fn '' Set.Icc 3 5 ↔ x ∈ Set.Icc 12 28
Tactic:
simp only [ge_iff_le, not_le, gt_iff_lt, Set.mem_image, Set.mem_Icc, fn]
State after:
case h
x : ℝ
⊢ (∃ x_1, (3 ≤ x_1 ∧ x_1 ≤ 5) ∧ x_1 ^ 2 + 3 = x) ↔ 12 ≤ x ∧ x ≤ 28

State before:
case h
x : ℝ
⊢ (∃ x_1, (3 ≤ x_1 ∧ x_1 ≤ 5) ∧ x_1 ^ 2 + 3 = x) ↔ 12 ≤ x ∧ x ≤ 28
Tactic:
constructor
State after:
case h.mp
x : ℝ
⊢ (∃ x_1, (3 ≤ x_1 ∧ x_1 ≤ 5) ∧ x_1 ^ 2 + 3 = x) → 12 ≤ x ∧ x ≤ 28

case h.mpr
x : ℝ
⊢ 12 ≤ x ∧ x ≤ 28 → ∃ x_1, (3 ≤ x_1 ∧ x_1 ≤ 5) ∧ x_1 ^ 2 + 3 = x

State before:
case h.mp
x : ℝ
⊢ (∃ x_1, (3 ≤ x_1 ∧ x_1 ≤ 5) ∧ x_1 ^ 2 + 3 = x) → 12 ≤ x ∧ x ≤ 28
Tactic:
intro hex
State after:
case h.mp
x : ℝ
hex : ∃ x_1, (3 ≤ x_1 ∧ x_1 ≤ 5) ∧ x_1 ^ 2 + 3 = x
⊢ 12 ≤ x ∧ x ≤ 28

State before:
case h.mp
x : ℝ
hex : ∃ x_1, (3 ≤ x_1 ∧ x_1 ≤ 5) ∧ x_1 ^ 2 + 3 = x
⊢ 12 ≤ x ∧ x ≤ 28
Tactic:
rcases hex with ⟨y, ⟨⟨h3le, h5ge⟩ , hfy⟩⟩
State after:
case h.mp.intro.intro.intro
x y : ℝ
hfy : y ^ 2 + 3 = x
h3le : 3 ≤ y
h5ge : y ≤ 5
⊢ 12 ≤ x ∧ x ≤ 28

State before:
case h.mp.intro.intro.intro
x y : ℝ
hfy : y ^ 2 + 3 = x
h3le : 3 ≤ y
h5ge : y ≤ 5
⊢ 12 ≤ x ∧ x ≤ 28
Tactic:
constructor
State after:
case h.mp.intro.intro.intro.left
x y : ℝ
hfy : y ^ 2 + 3 = x
h3le : 3 ≤ y
h5ge : y ≤ 5
⊢ 12 ≤ x

case h.mp.intro.intro.intro.right
x y : ℝ
hfy : y ^ 2 + 3 = x
h3le : 3 ≤ y
h5ge : y ≤ 5
⊢ x ≤ 28

State before:
case h.mp.intro.intro.intro.left
x y : ℝ
hfy : y ^ 2 + 3 = x
h3le : 3 ≤ y
h5ge : y ≤ 5
⊢ 12 ≤ x
Tactic:
nlinarith
State after:
no goals

State before:
case h.mp.intro.intro.intro.right
x y : ℝ
hfy : y ^ 2 + 3 = x
h3le : 3 ≤ y
h5ge : y ≤ 5
⊢ x ≤ 28
Tactic:
nlinarith
State after:
no goals

State before:
case h.mpr
x : ℝ
⊢ 12 ≤ x ∧ x ≤ 28 → ∃ x_1, (3 ≤ x_1 ∧ x_1 ≤ 5) ∧ x_1 ^ 2 + 3 = x
Tactic:
intro hlege
State after:
case h.mpr
x : ℝ
hlege : 12 ≤ x ∧ x ≤ 28
⊢ ∃ x_1, (3 ≤ x_1 ∧ x_1 ≤ 5) ∧ x_1 ^ 2 + 3 = x

State before:
case h.mpr
x : ℝ
hlege : 12 ≤ x ∧ x ≤ 28
⊢ ∃ x_1, (3 ≤ x_1 ∧ x_1 ≤ 5) ∧ x_1 ^ 2 + 3 = x
Tactic:
rcases hlege with ⟨h12ge, h28le⟩
State after:
case h.mpr.intro
x : ℝ
h12ge : 12 ≤ x
h28le : x ≤ 28
⊢ ∃ x_1, (3 ≤ x_1 ∧ x_1 ≤ 5) ∧ x_1 ^ 2 + 3 = x

State before:
case h.mpr.intro
x : ℝ
h12ge : 12 ≤ x
h28le : x ≤ 28
⊢ ∃ x_1, (3 ≤ x_1 ∧ x_1 ≤ 5) ∧ x_1 ^ 2 + 3 = x
Tactic:
use (Real.sqrt (x - 3))
State after:
case h
x : ℝ
h12ge : 12 ≤ x
h28le : x ≤ 28
⊢ (3 ≤ Real.sqrt (x - 3) ∧ Real.sqrt (x - 3) ≤ 5) ∧ Real.sqrt (x - 3) ^ 2 + 3 = x

State before:
case h
x : ℝ
h12ge : 12 ≤ x
h28le : x ≤ 28
⊢ (3 ≤ Real.sqrt (x - 3) ∧ Real.sqrt (x - 3) ≤ 5) ∧ Real.sqrt (x - 3) ^ 2 + 3 = x
Tactic:
constructor
State after:
case h.left
x : ℝ
h12ge : 12 ≤ x
h28le : x ≤ 28
⊢ 3 ≤ Real.sqrt (x - 3) ∧ Real.sqrt (x - 3) ≤ 5

case h.right
x : ℝ
h12ge : 12 ≤ x
h28le : x ≤ 28
⊢ Real.sqrt (x - 3) ^ 2 + 3 = x

State before:
case h.left
x : ℝ
h12ge : 12 ≤ x
h28le : x ≤ 28
⊢ 3 ≤ Real.sqrt (x - 3) ∧ Real.sqrt (x - 3) ≤ 5
Tactic:
constructor
State after:
case h.left.left
x : ℝ
h12ge : 12 ≤ x
h28le : x ≤ 28
⊢ 3 ≤ Real.sqrt (x - 3)

case h.left.right
x : ℝ
h12ge : 12 ≤ x
h28le : x ≤ 28
⊢ Real.sqrt (x - 3) ≤ 5

State before:
case h.left.left
x : ℝ
h12ge : 12 ≤ x
h28le : x ≤ 28
⊢ 3 ≤ Real.sqrt (x - 3)
Tactic:
refine Real.le_sqrt_of_sq_le ?h.left.left.h
State after:
case h.left.left.h
x : ℝ
h12ge : 12 ≤ x
h28le : x ≤ 28
⊢ 3 ^ 2 ≤ x - 3

State before:
case h.left.left.h
x : ℝ
h12ge : 12 ≤ x
h28le : x ≤ 28
⊢ 3 ^ 2 ≤ x - 3
Tactic:
linarith
State after:
no goals

State before:
case h.left.right
x : ℝ
h12ge : 12 ≤ x
h28le : x ≤ 28
⊢ Real.sqrt (x - 3) ≤ 5
Tactic:
refine Real.sqrt_le_iff.mpr ?h.left.right.a
State after:
case h.left.right.a
x : ℝ
h12ge : 12 ≤ x
h28le : x ≤ 28
⊢ 0 ≤ 5 ∧ x - 3 ≤ 5 ^ 2

State before:
case h.left.right.a
x : ℝ
h12ge : 12 ≤ x
h28le : x ≤ 28
⊢ 0 ≤ 5 ∧ x - 3 ≤ 5 ^ 2
Tactic:
constructor
State after:
case h.left.right.a.left
x : ℝ
h12ge : 12 ≤ x
h28le : x ≤ 28
⊢ 0 ≤ 5

case h.left.right.a.right
x : ℝ
h12ge : 12 ≤ x
h28le : x ≤ 28
⊢ x - 3 ≤ 5 ^ 2

State before:
case h.left.right.a.left
x : ℝ
h12ge : 12 ≤ x
h28le : x ≤ 28
⊢ 0 ≤ 5
Tactic:
nlinarith
State after:
no goals

State before:
case h.left.right.a.right
x : ℝ
h12ge : 12 ≤ x
h28le : x ≤ 28
⊢ x - 3 ≤ 5 ^ 2
Tactic:
nlinarith
State after:
no goals

State before:
case h.right
x : ℝ
h12ge : 12 ≤ x
h28le : x ≤ 28
⊢ Real.sqrt (x - 3) ^ 2 + 3 = x
Tactic:
rw [Real.sq_sqrt]
State after:
case h.right
x : ℝ
h12ge : 12 ≤ x
h28le : x ≤ 28
⊢ x - 3 + 3 = x

case h.right
x : ℝ
h12ge : 12 ≤ x
h28le : x ≤ 28
⊢ 0 ≤ x - 3

State before:
case h.right
x : ℝ
h12ge : 12 ≤ x
h28le : x ≤ 28
⊢ x - 3 + 3 = x
Tactic:
nlinarith
State after:
no goals

State before:
case h.right
x : ℝ
h12ge : 12 ≤ x
h28le : x ≤ 28
⊢ 0 ≤ x - 3
Tactic:
nlinarith
State after:
no goals