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

State before:
f g : ℝ → ℝ
x : ℝ
h : SurjectiveFunction (g ∘ f)
⊢ SurjectiveFunction g
Tactic:
intro y
State after:
f g : ℝ → ℝ
x : ℝ
h : SurjectiveFunction (g ∘ f)
y : ℝ
⊢ ∃ x, g x = y

State before:
f g : ℝ → ℝ
x : ℝ
h : SurjectiveFunction (g ∘ f)
y : ℝ
⊢ ∃ x, g x = y
Tactic:
obtain ⟨x, hx⟩ := h y
State after:
case intro
f g : ℝ → ℝ
x✝ : ℝ
h : SurjectiveFunction (g ∘ f)
y x : ℝ
hx : (g ∘ f) x = y
⊢ ∃ x, g x = y

State before:
case intro
f g : ℝ → ℝ
x✝ : ℝ
h : SurjectiveFunction (g ∘ f)
y x : ℝ
hx : (g ∘ f) x = y
⊢ ∃ x, g x = y
Tactic:
use f x
State after:
case h
f g : ℝ → ℝ
x✝ : ℝ
h : SurjectiveFunction (g ∘ f)
y x : ℝ
hx : (g ∘ f) x = y
⊢ g (f x) = y

State before:
case h
f g : ℝ → ℝ
x✝ : ℝ
h : SurjectiveFunction (g ∘ f)
y x : ℝ
hx : (g ∘ f) x = y
⊢ g (f x) = y
Tactic:
exact hx
State after:
no goals