Theorem: BunchImpl.Subbunch.trans (BunchImpl/Subbunch.lean)

State before:
P✝ : Sort u_1
b1 b2 b3 : Bunch P✝
⊢ Subbunch b1 b2 → Subbunch b2 b3 → Subbunch b1 b3
Tactic:
intro h1 h2
State after:
P✝ : Sort u_1
b1 b2 b3 : Bunch P✝
h1 : Subbunch b1 b2
h2 : Subbunch b2 b3
⊢ Subbunch b1 b3

State before:
P✝ : Sort u_1
b1 b2 b3 : Bunch P✝
h1 : Subbunch b1 b2
h2 : Subbunch b2 b3
⊢ Subbunch b1 b3
Tactic:
induction h1 <;> cases h2 <;> simp_all
State after:
no goals