Theorem: List.mem_set (LeanSAT/Upstream/ToStd.lean)

State before:
α : Type u_1
head✝ : α
bs : List α
x✝¹ x✝ : α
h : x✝ ∈ set (head✝ :: bs) 0 x✝¹
⊢ x✝ ∈ head✝ :: bs ∨ x✝ = x✝¹
Tactic:
simp only [set, mem_cons] at h ⊢
State after:
α : Type u_1
head✝ : α
bs : List α
x✝¹ x✝ : α
h : x✝ = x✝¹ ∨ x✝ ∈ bs
⊢ (x✝ = head✝ ∨ x✝ ∈ bs) ∨ x✝ = x✝¹

State before:
α : Type u_1
head✝ : α
bs : List α
x✝¹ x✝ : α
h : x✝ = x✝¹ ∨ x✝ ∈ bs
⊢ (x✝ = head✝ ∨ x✝ ∈ bs) ∨ x✝ = x✝¹
Tactic:
cases h
State after:
case inl
α : Type u_1
head✝ : α
bs : List α
x✝¹ x✝ : α
h✝ : x✝ = x✝¹
⊢ (x✝ = head✝ ∨ x✝ ∈ bs) ∨ x✝ = x✝¹

case inr
α : Type u_1
head✝ : α
bs : List α
x✝¹ x✝ : α
h✝ : x✝ ∈ bs
⊢ (x✝ = head✝ ∨ x✝ ∈ bs) ∨ x✝ = x✝¹

State before:
case inl
α : Type u_1
head✝ : α
bs : List α
x✝¹ x✝ : α
h✝ : x✝ = x✝¹
⊢ (x✝ = head✝ ∨ x✝ ∈ bs) ∨ x✝ = x✝¹
Tactic:
right
State after:
case inl.h
α : Type u_1
head✝ : α
bs : List α
x✝¹ x✝ : α
h✝ : x✝ = x✝¹
⊢ x✝ = x✝¹

State before:
case inl.h
α : Type u_1
head✝ : α
bs : List α
x✝¹ x✝ : α
h✝ : x✝ = x✝¹
⊢ x✝ = x✝¹
Tactic:
assumption
State after:
no goals

State before:
case inr
α : Type u_1
head✝ : α
bs : List α
x✝¹ x✝ : α
h✝ : x✝ ∈ bs
⊢ (x✝ = head✝ ∨ x✝ ∈ bs) ∨ x✝ = x✝¹
Tactic:
left
State after:
case inr.h
α : Type u_1
head✝ : α
bs : List α
x✝¹ x✝ : α
h✝ : x✝ ∈ bs
⊢ x✝ = head✝ ∨ x✝ ∈ bs

State before:
case inr.h
α : Type u_1
head✝ : α
bs : List α
x✝¹ x✝ : α
h✝ : x✝ ∈ bs
⊢ x✝ = head✝ ∨ x✝ ∈ bs
Tactic:
right
State after:
case inr.h.h
α : Type u_1
head✝ : α
bs : List α
x✝¹ x✝ : α
h✝ : x✝ ∈ bs
⊢ x✝ ∈ bs

State before:
case inr.h.h
α : Type u_1
head✝ : α
bs : List α
x✝¹ x✝ : α
h✝ : x✝ ∈ bs
⊢ x✝ ∈ bs
Tactic:
assumption
State after:
no goals

State before:
α : Type u_1
b : α
bs : List α
n : Nat
x✝¹ x✝ : α
h : x✝ ∈ set (b :: bs) (Nat.succ n) x✝¹
⊢ x✝ ∈ b :: bs ∨ x✝ = x✝¹
Tactic:
simp only [set, mem_cons] at h ⊢
State after:
α : Type u_1
b : α
bs : List α
n : Nat
x✝¹ x✝ : α
h : x✝ = b ∨ x✝ ∈ set bs n x✝¹
⊢ (x✝ = b ∨ x✝ ∈ bs) ∨ x✝ = x✝¹

State before:
α : Type u_1
b : α
bs : List α
n : Nat
x✝¹ x✝ : α
h : x✝ = b ∨ x✝ ∈ set bs n x✝¹
⊢ (x✝ = b ∨ x✝ ∈ bs) ∨ x✝ = x✝¹
Tactic:
cases h
State after:
case inl
α : Type u_1
b : α
bs : List α
n : Nat
x✝¹ x✝ : α
h✝ : x✝ = b
⊢ (x✝ = b ∨ x✝ ∈ bs) ∨ x✝ = x✝¹

case inr
α : Type u_1
b : α
bs : List α
n : Nat
x✝¹ x✝ : α
h✝ : x✝ ∈ set bs n x✝¹
⊢ (x✝ = b ∨ x✝ ∈ bs) ∨ x✝ = x✝¹

State before:
case inl
α : Type u_1
b : α
bs : List α
n : Nat
x✝¹ x✝ : α
h✝ : x✝ = b
⊢ (x✝ = b ∨ x✝ ∈ bs) ∨ x✝ = x✝¹

case inr
α : Type u_1
b : α
bs : List α
n : Nat
x✝¹ x✝ : α
h✝ : x✝ ∈ set bs n x✝¹
⊢ (x✝ = b ∨ x✝ ∈ bs) ∨ x✝ = x✝¹
Tactic:
. left; left; assumption
State after:
case inr
α : Type u_1
b : α
bs : List α
n : Nat
x✝¹ x✝ : α
h✝ : x✝ ∈ set bs n x✝¹
⊢ (x✝ = b ∨ x✝ ∈ bs) ∨ x✝ = x✝¹

State before:
case inl
α : Type u_1
b : α
bs : List α
n : Nat
x✝¹ x✝ : α
h✝ : x✝ = b
⊢ (x✝ = b ∨ x✝ ∈ bs) ∨ x✝ = x✝¹
Tactic:
left
State after:
case inl.h
α : Type u_1
b : α
bs : List α
n : Nat
x✝¹ x✝ : α
h✝ : x✝ = b
⊢ x✝ = b ∨ x✝ ∈ bs

State before:
case inl.h
α : Type u_1
b : α
bs : List α
n : Nat
x✝¹ x✝ : α
h✝ : x✝ = b
⊢ x✝ = b ∨ x✝ ∈ bs
Tactic:
left
State after:
case inl.h.h
α : Type u_1
b : α
bs : List α
n : Nat
x✝¹ x✝ : α
h✝ : x✝ = b
⊢ x✝ = b

State before:
case inl.h.h
α : Type u_1
b : α
bs : List α
n : Nat
x✝¹ x✝ : α
h✝ : x✝ = b
⊢ x✝ = b
Tactic:
assumption
State after:
no goals

State before:
case inr
α : Type u_1
b : α
bs : List α
n : Nat
x✝¹ x✝ : α
h✝ : x✝ ∈ set bs n x✝¹
⊢ (x✝ = b ∨ x✝ ∈ bs) ∨ x✝ = x✝¹
Tactic:
rename _ => h
State after:
case inr
α : Type u_1
b : α
bs : List α
n : Nat
x✝¹ x✝ : α
h : x✝ ∈ set bs n x✝¹
⊢ (x✝ = b ∨ x✝ ∈ bs) ∨ x✝ = x✝¹

State before:
case inr
α : Type u_1
b : α
bs : List α
n : Nat
x✝¹ x✝ : α
h : x✝ ∈ set bs n x✝¹
⊢ (x✝ = b ∨ x✝ ∈ bs) ∨ x✝ = x✝¹
Tactic:
cases mem_set h
State after:
case inr.inl
α : Type u_1
b : α
bs : List α
n : Nat
x✝¹ x✝ : α
h : x✝ ∈ set bs n x✝¹
h✝ : x✝ ∈ bs
⊢ (x✝ = b ∨ x✝ ∈ bs) ∨ x✝ = x✝¹

case inr.inr
α : Type u_1
b : α
bs : List α
n : Nat
x✝¹ x✝ : α
h : x✝ ∈ set bs n x✝¹
h✝ : x✝ = x✝¹
⊢ (x✝ = b ∨ x✝ ∈ bs) ∨ x✝ = x✝¹

State before:
case inr.inl
α : Type u_1
b : α
bs : List α
n : Nat
x✝¹ x✝ : α
h : x✝ ∈ set bs n x✝¹
h✝ : x✝ ∈ bs
⊢ (x✝ = b ∨ x✝ ∈ bs) ∨ x✝ = x✝¹
Tactic:
left
State after:
case inr.inl.h
α : Type u_1
b : α
bs : List α
n : Nat
x✝¹ x✝ : α
h : x✝ ∈ set bs n x✝¹
h✝ : x✝ ∈ bs
⊢ x✝ = b ∨ x✝ ∈ bs

State before:
case inr.inl.h
α : Type u_1
b : α
bs : List α
n : Nat
x✝¹ x✝ : α
h : x✝ ∈ set bs n x✝¹
h✝ : x✝ ∈ bs
⊢ x✝ = b ∨ x✝ ∈ bs
Tactic:
right
State after:
case inr.inl.h.h
α : Type u_1
b : α
bs : List α
n : Nat
x✝¹ x✝ : α
h : x✝ ∈ set bs n x✝¹
h✝ : x✝ ∈ bs
⊢ x✝ ∈ bs

State before:
case inr.inl.h.h
α : Type u_1
b : α
bs : List α
n : Nat
x✝¹ x✝ : α
h : x✝ ∈ set bs n x✝¹
h✝ : x✝ ∈ bs
⊢ x✝ ∈ bs
Tactic:
assumption
State after:
no goals

State before:
case inr.inr
α : Type u_1
b : α
bs : List α
n : Nat
x✝¹ x✝ : α
h : x✝ ∈ set bs n x✝¹
h✝ : x✝ = x✝¹
⊢ (x✝ = b ∨ x✝ ∈ bs) ∨ x✝ = x✝¹
Tactic:
right
State after:
case inr.inr.h
α : Type u_1
b : α
bs : List α
n : Nat
x✝¹ x✝ : α
h : x✝ ∈ set bs n x✝¹
h✝ : x✝ = x✝¹
⊢ x✝ = x✝¹

State before:
case inr.inr.h
α : Type u_1
b : α
bs : List α
n : Nat
x✝¹ x✝ : α
h : x✝ ∈ set bs n x✝¹
h✝ : x✝ = x✝¹
⊢ x✝ = x✝¹
Tactic:
assumption
State after:
no goals