Theorem: LoVe.abcd_bd_again (LoVe/Labs/Lab10Solution.lean)

State before:
a b c d : Prop
⊢ a ∧ (b ∧ c) ∧ d → b ∧ d
Tactic:
intro h
State after:
a b c d : Prop
h : a ∧ (b ∧ c) ∧ d
⊢ b ∧ d

State before:
a b c d : Prop
h : a ∧ (b ∧ c) ∧ d
⊢ b ∧ d
Tactic:
cases_and
State after:
case intro.intro.intro
a b c d : Prop
left : a
right : d
left_1 : b
right_1 : c
⊢ b ∧ d

State before:
case intro.intro.intro
a b c d : Prop
left : a
right : d
left_1 : b
right_1 : c
⊢ b ∧ d
Tactic:
sorry
State after:
no goals