Theorem: Smt.Reconstruct.Builtin.scopes (Smt/Reconstruct/Builtin/Lemmas.lean)

State before:
⊢ ∀ {ps : List Prop} {q : Prop}, impliesN ps q → andN ps → q
Tactic:
intros ps q h
State after:
ps : List Prop
q : Prop
h : impliesN ps q
⊢ andN ps → q

State before:
ps : List Prop
q : Prop
h : impliesN ps q
⊢ andN ps → q
Tactic:
match ps with
| []   => intro; exact h
| [p]  => unfold andN
          unfold impliesN at h
          exact h
| p₁::p₂::ps => unfold andN
                unfold impliesN at h
                intro ⟨hp₁, hps⟩
                revert hps
                exact scopes (h hp₁)
State after:
no goals

State before:
ps : List Prop
q : Prop
h : impliesN [] q
⊢ andN [] → q
Tactic:
intro
State after:
ps : List Prop
q : Prop
h : impliesN [] q
a✝ : andN []
⊢ q

State before:
ps : List Prop
q : Prop
h : impliesN [] q
a✝ : andN []
⊢ q
Tactic:
exact h
State after:
no goals

State before:
ps : List Prop
q p : Prop
h : impliesN [p] q
⊢ andN [p] → q
Tactic:
unfold andN
State after:
ps : List Prop
q p : Prop
h : impliesN [p] q
⊢ p → q

State before:
ps : List Prop
q p : Prop
h : impliesN [p] q
⊢ p → q
Tactic:
unfold impliesN at h
State after:
ps : List Prop
q p : Prop
h : p → impliesN [] q
⊢ p → q

State before:
ps : List Prop
q p : Prop
h : p → impliesN [] q
⊢ p → q
Tactic:
exact h
State after:
no goals

State before:
ps✝ : List Prop
q p₁ p₂ : Prop
ps : List Prop
h : impliesN (p₁ :: p₂ :: ps) q
⊢ andN (p₁ :: p₂ :: ps) → q
Tactic:
unfold andN
State after:
ps✝ : List Prop
q p₁ p₂ : Prop
ps : List Prop
h : impliesN (p₁ :: p₂ :: ps) q
⊢ p₁ ∧ andN (p₂ :: ps) → q

State before:
ps✝ : List Prop
q p₁ p₂ : Prop
ps : List Prop
h : impliesN (p₁ :: p₂ :: ps) q
⊢ p₁ ∧ andN (p₂ :: ps) → q
Tactic:
unfold impliesN at h
State after:
ps✝ : List Prop
q p₁ p₂ : Prop
ps : List Prop
h : p₁ → impliesN (p₂ :: ps) q
⊢ p₁ ∧ andN (p₂ :: ps) → q

State before:
ps✝ : List Prop
q p₁ p₂ : Prop
ps : List Prop
h : p₁ → impliesN (p₂ :: ps) q
⊢ p₁ ∧ andN (p₂ :: ps) → q
Tactic:
intro ⟨hp₁, hps⟩
State after:
ps✝ : List Prop
q p₁ p₂ : Prop
ps : List Prop
h : p₁ → impliesN (p₂ :: ps) q
hp₁ : p₁
hps : andN (p₂ :: ps)
⊢ q

State before:
ps✝ : List Prop
q p₁ p₂ : Prop
ps : List Prop
h : p₁ → impliesN (p₂ :: ps) q
hp₁ : p₁
hps : andN (p₂ :: ps)
⊢ q
Tactic:
revert hps
State after:
ps✝ : List Prop
q p₁ p₂ : Prop
ps : List Prop
h : p₁ → impliesN (p₂ :: ps) q
hp₁ : p₁
⊢ andN (p₂ :: ps) → q

State before:
ps✝ : List Prop
q p₁ p₂ : Prop
ps : List Prop
h : p₁ → impliesN (p₂ :: ps) q
hp₁ : p₁
⊢ andN (p₂ :: ps) → q
Tactic:
exact scopes (h hp₁)
State after:
no goals