Theorem: SimpleGraph.ind_singleton (LeanCamCombi/Mathlib/Combinatorics/SimpleGraph/Basic.lean)

State before:
α : Type u_1
β : Type u_2
G✝ H : SimpleGraph α
s✝ : Set (Sym2 α)
s t : Set α
a✝ b : α
G : SimpleGraph α
a : α
⊢ G.ind {a} = ⊥
Tactic:
ext
State after:
case Adj.h.h.a
α : Type u_1
β : Type u_2
G✝ H : SimpleGraph α
s✝ : Set (Sym2 α)
s t : Set α
a✝ b : α
G : SimpleGraph α
a x✝¹ x✝ : α
⊢ (G.ind {a}).Adj x✝¹ x✝ ↔ ⊥.Adj x✝¹ x✝

State before:
case Adj.h.h.a
α : Type u_1
β : Type u_2
G✝ H : SimpleGraph α
s✝ : Set (Sym2 α)
s t : Set α
a✝ b : α
G : SimpleGraph α
a x✝¹ x✝ : α
⊢ (G.ind {a}).Adj x✝¹ x✝ ↔ ⊥.Adj x✝¹ x✝
Tactic:
simp
State after:
case Adj.h.h.a
α : Type u_1
β : Type u_2
G✝ H : SimpleGraph α
s✝ : Set (Sym2 α)
s t : Set α
a✝ b : α
G : SimpleGraph α
a x✝¹ x✝ : α
⊢ G.Adj x✝¹ x✝ → x✝¹ = a → ¬x✝ = a

State before:
case Adj.h.h.a
α : Type u_1
β : Type u_2
G✝ H : SimpleGraph α
s✝ : Set (Sym2 α)
s t : Set α
a✝ b : α
G : SimpleGraph α
a x✝¹ x✝ : α
⊢ G.Adj x✝¹ x✝ → x✝¹ = a → ¬x✝ = a
Tactic:
rintro h rfl
State after:
case Adj.h.h.a
α : Type u_1
β : Type u_2
G✝ H : SimpleGraph α
s✝ : Set (Sym2 α)
s t : Set α
a b : α
G : SimpleGraph α
x✝¹ x✝ : α
h : G.Adj x✝¹ x✝
⊢ ¬x✝ = x✝¹

State before:
case Adj.h.h.a
α : Type u_1
β : Type u_2
G✝ H : SimpleGraph α
s✝ : Set (Sym2 α)
s t : Set α
a b : α
G : SimpleGraph α
x✝¹ x✝ : α
h : G.Adj x✝¹ x✝
⊢ ¬x✝ = x✝¹
Tactic:
exact h.ne'
State after:
no goals