Disjunction of two known implications

Stream: new members

[Achyut Raj]

Given the two hypotheses, h: P -> Q and j: R -> S, which tactic can be used to close the goal: (P v R) -> (Q v S)?

[Kevin Buzzard]

tauto!

[Kevin Buzzard]

Probably also library_search

[Ruben Van de Velde]

Not a tactic, but you could use the lemma docs#or.imp

[Kevin Buzzard]

The tactic hint will list tactics which close the current goal, by the way

[Ruben Van de Velde]

I guesssuggest might find it as well, if we're listing all the tactics :)

[Achyut Raj]

thanks for the suggestions :)
I'd like to add a lil context tho. I have just been playing the natural number game, I am specifically on the Lvl 9 of Inequality world (https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/?world=10&level=9) where I faced this problem. So I'm kinda limited as to what all I could use. For instance, I cannot use tauto because this level doesn't import it.

So I am curious if there's a way to prove the disjunction of two implications using just the basic tactics

[Bulhwi Cha]

-- this code is written in Lean 3
example {p q r s : Prop} (h : p → q) (j : r → s) : p ∨ r → q ∨ s :=
begin
  intro hpr,
  cases hpr with hp hr,
  { exact or.inl (h hp) },
  { exact or.inr (j hr) },
end

Solution written in Lean 4

-- this code is written in Lean 4
example {p q r s : Prop} (h : p → q) (j : r → s) : p ∨ r → q ∨ s := by
  intro hpr
  cases hpr with
  | inl hp => exact Or.inl (h hp)
  | inr hr => exact Or.inr (j hr)