Theorem: SimpleGraph.ind_inter (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 α
s t : Set α
⊢ G.ind (s ∩ t) = G.ind s ⊓ G.ind t
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 α
s t : Set α
x✝¹ x✝ : α
⊢ (G.ind (s ∩ t)).Adj x✝¹ x✝ ↔ (G.ind s ⊓ G.ind t).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 α
s t : Set α
x✝¹ x✝ : α
⊢ (G.ind (s ∩ t)).Adj x✝¹ x✝ ↔ (G.ind s ⊓ G.ind t).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 α
s t : Set α
x✝¹ x✝ : α
⊢ G.Adj x✝¹ x✝ ∧ (x✝¹ ∈ s ∧ x✝¹ ∈ t) ∧ x✝ ∈ s ∧ x✝ ∈ t ↔
    (G.Adj x✝¹ x✝ ∧ x✝¹ ∈ s ∧ x✝ ∈ s) ∧ G.Adj x✝¹ x✝ ∧ x✝¹ ∈ t ∧ x✝ ∈ t

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 α
s t : Set α
x✝¹ x✝ : α
⊢ G.Adj x✝¹ x✝ ∧ (x✝¹ ∈ s ∧ x✝¹ ∈ t) ∧ x✝ ∈ s ∧ x✝ ∈ t ↔
    (G.Adj x✝¹ x✝ ∧ x✝¹ ∈ s ∧ x✝ ∈ s) ∧ G.Adj x✝¹ x✝ ∧ x✝¹ ∈ t ∧ x✝ ∈ t
Tactic:
tauto
State after:
no goals