Theorem: Smt.Reconstruct.Prop.flipped_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 nap => cases h₂ with
             | inl ap => 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
nap : ¬A
⊢ B ∨ C
Tactic:
cases h₂ with
| inl ap => exact False.elim (nap ap)
| inr cp => exact (Or.inr cp)
State after:
no goals

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

State before:
case inl.inr
A B C : Prop
nap : ¬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