Composing surjections, proof using pattern matching

Stream: new members

[Martin C. Martin]

The first exercise in Chapter 8 of Theorem proving in Lean is "Use pattern matching to prove that the composition of surjective functions is surjective:

open function

universes u v w
variables {α : Type u} {β : Type v} {γ : Type w}

lemma surjective_comp {g : β → γ} {f : α → β}
  (hg : surjective g) (hf : surjective f) :
surjective (g ∘ f) := sorry

Here's what I have, which is incomplete, and I feel like I'm barking up the wrong tree:

lemma surjective_comp {g : β → γ} {f : α → β}
  (hg : surjective g) (hf : surjective f) :
surjective (g ∘ f)
| c := exists.elim (hg c)
  (assume b hgb, exists.elim (hf b) (assume a hfa, exists.intro a sorry))

I just used the pattern matching to get c, can it be used for more of the proof? Can the proof be simplified further, hopefully leveraging the pattern matching in a way I'm not seeing, but otherwise using tactics or something?

[Alex J. Best]

Here's a pattern matching solution, no idea what is intended:

lemma surjective_comp {g : β → γ} {f : α → β}
  (hg : surjective g) (hf : surjective f) :
surjective (g ∘ f)
| x := match hg x with
       | ⟨y, hy⟩ := match hf y with
                    | ⟨z, hz⟩ := ⟨z, by rw [← hy, ← hz]⟩
                    end
       end

BTW most of this answer was generated by github copilot! I pretty much wrote half of the first line only, I have no idea if that means this is written somewhere already or if it is just very smart

[Martin C. Martin]

Alex J. Best said:

BTW most of this answer was generated by github copilot! I pretty much wrote half of the first line only, I have no idea if that means this is written somewhere already or if it is just very smart

Perhaps copilot is the new stack overflow. :) Thanks Alex.