Theorem: anda (Katydid/Std/Ltac.lean)

State before:
a : Prop
⊢ a → a ∧ a
Tactic:
intro a
State after:
a✝ : Prop
a : a✝
⊢ a✝ ∧ a✝

State before:
a✝ : Prop
a : a✝
⊢ a✝ ∧ a✝
Tactic:
apply And.intro
State after:
case left
a✝ : Prop
a : a✝
⊢ a✝

case right
a✝ : Prop
a : a✝
⊢ a✝

State before:
a✝ : Prop
a : a✝
⊢ a✝
Tactic:
case left => assumption
State after:
no goals

State before:
a✝ : Prop
a : a✝
⊢ a✝
Tactic:
case right => assumption
State after:
no goals

State before:
a✝ : Prop
a : a✝
⊢ a✝
Tactic:
assumption
State after:
no goals