Theorem: exercise2_4 (LeanCourse/Assignments/Solutions/Solutions2.lean)

State before:
f g : ℝ → ℝ
x : ℝ
hf : SurjectiveFunction f
⊢ SurjectiveFunction fun x => 2 * f (3 * (x + 4)) + 1
Tactic:
intro y
State after:
f g : ℝ → ℝ
x : ℝ
hf : SurjectiveFunction f
y : ℝ
⊢ ∃ x, (fun x => 2 * f (3 * (x + 4)) + 1) x = y

State before:
f g : ℝ → ℝ
x : ℝ
hf : SurjectiveFunction f
y : ℝ
⊢ ∃ x, (fun x => 2 * f (3 * (x + 4)) + 1) x = y
Tactic:
obtain ⟨x, hx⟩ := hf ((y - 1) / 2)
State after:
case intro
f g : ℝ → ℝ
x✝ : ℝ
hf : SurjectiveFunction f
y x : ℝ
hx : f x = (y - 1) / 2
⊢ ∃ x, (fun x => 2 * f (3 * (x + 4)) + 1) x = y

State before:
case intro
f g : ℝ → ℝ
x✝ : ℝ
hf : SurjectiveFunction f
y x : ℝ
hx : f x = (y - 1) / 2
⊢ ∃ x, (fun x => 2 * f (3 * (x + 4)) + 1) x = y
Tactic:
use x / 3 - 4
State after:
case h
f g : ℝ → ℝ
x✝ : ℝ
hf : SurjectiveFunction f
y x : ℝ
hx : f x = (y - 1) / 2
⊢ (fun x => 2 * f (3 * (x + 4)) + 1) (x / 3 - 4) = y

State before:
case h
f g : ℝ → ℝ
x✝ : ℝ
hf : SurjectiveFunction f
y x : ℝ
hx : f x = (y - 1) / 2
⊢ (fun x => 2 * f (3 * (x + 4)) + 1) (x / 3 - 4) = y
Tactic:
ring
State after:
case h
f g : ℝ → ℝ
x✝ : ℝ
hf : SurjectiveFunction f
y x : ℝ
hx : f x = (y - 1) / 2
⊢ 1 + f x * 2 = y

State before:
case h
f g : ℝ → ℝ
x✝ : ℝ
hf : SurjectiveFunction f
y x : ℝ
hx : f x = (y - 1) / 2
⊢ 1 + f x * 2 = y
Tactic:
rw [hx]
State after:
case h
f g : ℝ → ℝ
x✝ : ℝ
hf : SurjectiveFunction f
y x : ℝ
hx : f x = (y - 1) / 2
⊢ 1 + (y - 1) / 2 * 2 = y

State before:
case h
f g : ℝ → ℝ
x✝ : ℝ
hf : SurjectiveFunction f
y x : ℝ
hx : f x = (y - 1) / 2
⊢ 1 + (y - 1) / 2 * 2 = y
Tactic:
ring
State after:
no goals