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

State before:
f g : ℝ → ℝ
x : ℝ
hf : SurjectiveFunction f
⊢ SurjectiveFunction (g ∘ f) ↔ SurjectiveFunction g
Tactic:
constructor
State after:
case mp
f g : ℝ → ℝ
x : ℝ
hf : SurjectiveFunction f
⊢ SurjectiveFunction (g ∘ f) → SurjectiveFunction g

case mpr
f g : ℝ → ℝ
x : ℝ
hf : SurjectiveFunction f
⊢ SurjectiveFunction g → SurjectiveFunction (g ∘ f)

State before:
case mpr
f g : ℝ → ℝ
x : ℝ
hf : SurjectiveFunction f
⊢ SurjectiveFunction g → SurjectiveFunction (g ∘ f)
Tactic:
intro hg z
State after:
case mpr
f g : ℝ → ℝ
x : ℝ
hf : SurjectiveFunction f
hg : SurjectiveFunction g
z : ℝ
⊢ ∃ x, (g ∘ f) x = z

State before:
case mpr
f g : ℝ → ℝ
x : ℝ
hf : SurjectiveFunction f
hg : SurjectiveFunction g
z : ℝ
⊢ ∃ x, (g ∘ f) x = z
Tactic:
obtain ⟨y, hy⟩ := hg z
State after:
case mpr.intro
f g : ℝ → ℝ
x : ℝ
hf : SurjectiveFunction f
hg : SurjectiveFunction g
z y : ℝ
hy : g y = z
⊢ ∃ x, (g ∘ f) x = z

State before:
case mpr.intro
f g : ℝ → ℝ
x : ℝ
hf : SurjectiveFunction f
hg : SurjectiveFunction g
z y : ℝ
hy : g y = z
⊢ ∃ x, (g ∘ f) x = z
Tactic:
obtain ⟨x, hx⟩ := hf y
State after:
case mpr.intro.intro
f g : ℝ → ℝ
x✝ : ℝ
hf : SurjectiveFunction f
hg : SurjectiveFunction g
z y : ℝ
hy : g y = z
x : ℝ
hx : f x = y
⊢ ∃ x, (g ∘ f) x = z

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

State before:
case h
f g : ℝ → ℝ
x✝ : ℝ
hf : SurjectiveFunction f
hg : SurjectiveFunction g
z y : ℝ
hy : g y = z
x : ℝ
hx : f x = y
⊢ (g ∘ f) x = z
Tactic:
rw [← hy, ← hx]
State after:
case h
f g : ℝ → ℝ
x✝ : ℝ
hf : SurjectiveFunction f
hg : SurjectiveFunction g
z y : ℝ
hy : g y = z
x : ℝ
hx : f x = y
⊢ (g ∘ f) x = g (f x)

State before:
case h
f g : ℝ → ℝ
x✝ : ℝ
hf : SurjectiveFunction f
hg : SurjectiveFunction g
z y : ℝ
hy : g y = z
x : ℝ
hx : f x = y
⊢ (g ∘ f) x = g (f x)
Tactic:
rfl
State after:
no goals

State before:
case mp
f g : ℝ → ℝ
x : ℝ
hf : SurjectiveFunction f
⊢ SurjectiveFunction (g ∘ f) → SurjectiveFunction g
Tactic:
exact exercise2_2
State after:
no goals