Theorem: SimpleGraph.pair_subset (Turan4/CliqueFreeSets.lean)

State before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v w : α
A : Finset α
hv : v ∈ A
hw : w ∈ A
⊢ {v, w} ⊆ A
Tactic:
intro x
State after:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v w : α
A : Finset α
hv : v ∈ A
hw : w ∈ A
x : α
⊢ x ∈ {v, w} → x ∈ A

State before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v w : α
A : Finset α
hv : v ∈ A
hw : w ∈ A
x : α
⊢ x ∈ {v, w} → x ∈ A
Tactic:
rw [mem_insert,mem_singleton]
State after:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v w : α
A : Finset α
hv : v ∈ A
hw : w ∈ A
x : α
⊢ x = v ∨ x = w → x ∈ A

State before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v w : α
A : Finset α
hv : v ∈ A
hw : w ∈ A
x : α
⊢ x = v ∨ x = w → x ∈ A
Tactic:
intro h
State after:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v w : α
A : Finset α
hv : v ∈ A
hw : w ∈ A
x : α
h : x = v ∨ x = w
⊢ x ∈ A

State before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v w : α
A : Finset α
hv : v ∈ A
hw : w ∈ A
x : α
h : x = v ∨ x = w
⊢ x ∈ A
Tactic:
cases h with
| inl h => exact h ▸ hv
| inr h => exact h ▸ hw
State after:
no goals

State before:
case inl
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v w : α
A : Finset α
hv : v ∈ A
hw : w ∈ A
x : α
h : x = v
⊢ x ∈ A
Tactic:
exact h ▸ hv
State after:
no goals

State before:
case inr
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v w : α
A : Finset α
hv : v ∈ A
hw : w ∈ A
x : α
h : x = w
⊢ x ∈ A
Tactic:
exact h ▸ hw
State after:
no goals