Theorem: Smt.Reconstruct.Prop.resolution_thm (Smt/Reconstruct/Prop/Resolution.lean)

State before:
⊢ ∀ {A B C : Prop}, A ∨ B → ¬A ∨ C → B ∨ C
Tactic:
intros A B C h₁ h₂
State after:
A B C : Prop
h₁ : A ∨ B
h₂ : ¬A ∨ C
⊢ B ∨ C

State before:
A B C : Prop
h₁ : A ∨ B
h₂ : ¬A ∨ C
⊢ B ∨ C
Tactic:
cases h₁ with
| inl ap => cases h₂ with
            | inl nap => exact (False.elim (nap ap))
            | inr cp  => exact (Or.inr cp)
| inr bp => exact (Or.inl bp)
State after:
no goals

State before:
case inl
A B C : Prop
h₂ : ¬A ∨ C
ap : A
⊢ B ∨ C
Tactic:
cases h₂ with
| inl nap => exact (False.elim (nap ap))
| inr cp  => exact (Or.inr cp)
State after:
no goals

State before:
case inl.inl
A B C : Prop
ap : A
nap : ¬A
⊢ B ∨ C
Tactic:
exact (False.elim (nap ap))
State after:
no goals

State before:
case inl.inr
A B C : Prop
ap : A
cp : C
⊢ B ∨ C
Tactic:
exact (Or.inr cp)
State after:
no goals

State before:
case inr
A B C : Prop
h₂ : ¬A ∨ C
bp : B
⊢ B ∨ C
Tactic:
exact (Or.inl bp)
State after:
no goals