awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
⊢ Adj (G := G) (induce ⊤ {v, w}) v w

Tactic:
simp [hvw, hvw.symm]

Premises used: SimpleGraph.Adj.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
⊢ Adj (G := G) (induce ⊤ {v, w}) w v

Tactic:
simp [hvw, hvw.symm]

Premises used: SimpleGraph.Adj.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
x x_1 : V
h : Adj (G := G) (induce ⊤ {v, w}) x x_1
⊢ (x = v ∨ x = w) ∧ (x_1 = v ∨ x_1 = w) ∧ G.Adj x x_1

Tactic:
simp only [induce_adj, Set.mem_insert_iff, Set.mem_singleton_iff, top_adj] at h

Premises used: SimpleGraph.Subgraph.induce_adj, Set.mem_singleton_iff, SimpleGraph.Subgraph.top_adj, Set.mem_insert_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
x x_1 : V
h : (x = v ∨ x = w) ∧ (x_1 = v ∨ x_1 = w) ∧ G.Adj x x_1
Adj : ∀ (hvw : G.Adj x_1 w) (ha : G.Adj x_1 x_1), (G.subgraphOfAdj hvw).Adj x_1 x_1
Adj₁ : ∀ (ha hvw : G.Adj x x_1), (G.subgraphOfAdj hvw).Adj x x_1
Adj₂ : ∀ (ha : G.Adj x x_1) (hvw : G.Adj x_1 x), (G.subgraphOfAdj hvw).Adj x x_1
Adj₃ : ∀ (hvw : G.Adj v x_1) (ha : G.Adj x_1 x_1), (G.subgraphOfAdj hvw).Adj x_1 x_1
⊢ (G.subgraphOfAdj hvw).Adj x x_1

Tactic:
obtain ⟨rfl | rfl, rfl | rfl, ha⟩ := h

Premises used: rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
w x : V
hvw : G.Adj x w
ha : G.Adj x x
⊢ (G.subgraphOfAdj hvw).Adj x x

Tactic:
(ha.ne rfl).elim

Premises used: SimpleGraph.Adj.ne, False.elim, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
w x : V
hvw : G.Adj x w
ha : G.Adj x x
⊢ (G.subgraphOfAdj hvw).Adj x x

Tactic:
exact (ha.ne rfl).elim

Premises used: SimpleGraph.Adj.ne, False.elim, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
w x : V
hvw : G.Adj x w
ha : G.Adj x x
⊢ (G.subgraphOfAdj hvw).Adj x x

Tactic:
first | exact (ha.ne rfl).elim | simp

Premises used: SimpleGraph.Adj.ne, False.elim, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
x x_1 : V
ha hvw : G.Adj x x_1
⊢ (G.subgraphOfAdj hvw).Adj x x_1

Tactic:
(ha.ne rfl).elim

Premises used: SimpleGraph.Adj.ne, False.elim
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
x x_1 : V
ha hvw : G.Adj x x_1
⊢ (G.subgraphOfAdj hvw).Adj x x_1

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
x x_1 : V
ha hvw : G.Adj x x_1
⊢ (G.subgraphOfAdj hvw).Adj x x_1

Tactic:
first | exact (ha.ne rfl).elim | simp

Premises used: SimpleGraph.Adj.ne, False.elim
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
x x_1 : V
ha : G.Adj x x_1
hvw : G.Adj x_1 x
⊢ (G.subgraphOfAdj hvw).Adj x x_1

Tactic:
(ha.ne rfl).elim

Premises used: SimpleGraph.Adj.ne, False.elim
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
x x_1 : V
ha : G.Adj x x_1
hvw : G.Adj x_1 x
⊢ (G.subgraphOfAdj hvw).Adj x x_1

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
x x_1 : V
ha : G.Adj x x_1
hvw : G.Adj x_1 x
⊢ (G.subgraphOfAdj hvw).Adj x x_1

Tactic:
first | exact (ha.ne rfl).elim | simp

Premises used: SimpleGraph.Adj.ne, False.elim
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
v x : V
hvw : G.Adj v x
ha : G.Adj x x
⊢ (G.subgraphOfAdj hvw).Adj x x

Tactic:
(ha.ne rfl).elim

Premises used: SimpleGraph.Adj.ne, False.elim, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
v x : V
hvw : G.Adj v x
ha : G.Adj x x
⊢ (G.subgraphOfAdj hvw).Adj x x

Tactic:
exact (ha.ne rfl).elim

Premises used: SimpleGraph.Adj.ne, False.elim, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
v x : V
hvw : G.Adj v x
ha : G.Adj x x
⊢ (G.subgraphOfAdj hvw).Adj x x

Tactic:
first | exact (ha.ne rfl).elim | simp

Premises used: SimpleGraph.Adj.ne, False.elim, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' G'' : G.Subgraph
s_1 s' s : Set V
h : s ⊆ G'.verts
x : (↑(G'.induce s).verts : Type u)
v : V
hv : v ∈ s
⊢ Membership.mem (γ := Set (↑G'.verts : Type u)) {v : (↑G'.verts : Type u) | (↑v : V) ∈ s}
    (Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) v ⋯)

Tactic:
aesop
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' G'' : G.Subgraph
s_1 s' s : Set V
h : s ⊆ G'.verts
⊢ ∀ {a b : (↑(G'.induce s).verts : Type u)},
    SimpleGraph.Adj (V := (↑{v : (↑G'.verts : Type u) | (↑v : V) ∈ s} : Type u))
        (SimpleGraph.induce {v : (↑G'.verts : Type u) | (↑v : V) ∈ s} G'.coe)
        (({
              toFun := fun (x : (↑(G'.induce s).verts : Type u)) ↦
                match (motive :=
                  (↑(G'.induce s).verts : Type u) → (↑{v : (↑G'.verts : Type u) | (↑v : V) ∈ s} : Type u)) x with
                | ⟨v, hv⟩ =>
                  Subtype.mk (p := fun (x : (↑G'.verts : Type u)) ↦
                    Membership.mem (γ := Set (↑G'.verts : Type u)) {v : (↑G'.verts : Type u) | (↑v : V) ∈ s} x)
                    (Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) v ⋯) hv,
              invFun := fun (x : (↑{v : (↑G'.verts : Type u) | (↑v : V) ∈ s} : Type u)) ↦
                match (motive :=
                  (↑{v : (↑G'.verts : Type u) | (↑v : V) ∈ s} : Type u) → (↑(G'.induce s).verts : Type u)) x with
                | ⟨v, hv⟩ => Subtype.mk (p := fun (x : V) ↦ x ∈ (G'.induce s).verts) (↑v : V) hv,
              left_inv := ⋯, right_inv := ⋯ :
              (↑(G'.induce s).verts : Type u) ≃ (↑{v : (↑G'.verts : Type u) | (↑v : V) ∈ s} : Type u) } :
            (a : (↑(G'.induce s).verts : Type u)) → (↑{v : (↑G'.verts : Type u) | (↑v : V) ∈ s} : Type u))
          a)
        (({
              toFun := fun (x : (↑(G'.induce s).verts : Type u)) ↦
                match (motive :=
                  (↑(G'.induce s).verts : Type u) → (↑{v : (↑G'.verts : Type u) | (↑v : V) ∈ s} : Type u)) x with
                | ⟨v, hv⟩ =>
                  Subtype.mk (p := fun (x : (↑G'.verts : Type u)) ↦
                    Membership.mem (γ := Set (↑G'.verts : Type u)) {v : (↑G'.verts : Type u) | (↑v : V) ∈ s} x)
                    (Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) v ⋯) hv,
              invFun := fun (x : (↑{v : (↑G'.verts : Type u) | (↑v : V) ∈ s} : Type u)) ↦
                match (motive :=
                  (↑{v : (↑G'.verts : Type u) | (↑v : V) ∈ s} : Type u) → (↑(G'.induce s).verts : Type u)) x with
                | ⟨v, hv⟩ => Subtype.mk (p := fun (x : V) ↦ x ∈ (G'.induce s).verts) (↑v : V) hv,
              left_inv := ⋯, right_inv := ⋯ :
              (↑(G'.induce s).verts : Type u) ≃ (↑{v : (↑G'.verts : Type u) | (↑v : V) ∈ s} : Type u) } :
            (a : (↑(G'.induce s).verts : Type u)) → (↑{v : (↑G'.verts : Type u) | (↑v : V) ∈ s} : Type u))
          b) ↔
      (G'.induce s).coe.Adj a b

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set V
⊢ (G'.deleteVerts s).verts = G'.verts \ s

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set V
u v : V
⊢ (G'.deleteVerts s).Adj u v ↔ u ∈ G'.verts ∧ u ∉ s ∧ v ∈ G'.verts ∧ v ∉ s ∧ G'.Adj u v

Tactic:
simp [and_assoc]

Premises used: and_assoc
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s s' : Set V
verts : ∀ (x : V), x ∈ ((G'.deleteVerts s).deleteVerts s').verts ↔ x ∈ (G'.deleteVerts (s ∪ s')).verts
Adj : ∀ (x x_1 : V), ((G'.deleteVerts s).deleteVerts s').Adj x x_1 ↔ (G'.deleteVerts (s ∪ s')).Adj x x_1
⊢ (G'.deleteVerts s).deleteVerts s' = G'.deleteVerts (s ∪ s')

Tactic:
ext
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s s' : Set V
x : V
⊢ x ∈ ((G'.deleteVerts s).deleteVerts s').verts ↔ x ∈ (G'.deleteVerts (s ∪ s')).verts

Tactic:
simp +contextual [not_or, and_assoc]

Premises used: not_or, and_assoc
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s s' : Set V
x x_1 : V
⊢ ((G'.deleteVerts s).deleteVerts s').Adj x x_1 ↔ (G'.deleteVerts (s ∪ s')).Adj x x_1

Tactic:
simp +contextual [not_or, and_assoc]

Premises used: not_or, and_assoc
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
⊢ G'.deleteVerts ∅ = G'

Tactic:
simp [deleteVerts]

Premises used: SimpleGraph.Subgraph.deleteVerts
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set V
left : (G'.deleteVerts s).verts ⊆ G'.verts
right : ∀ ⦃v w : V⦄, (G'.deleteVerts s).Adj v w → G'.Adj v w
⊢ G'.deleteVerts s ≤ G'

Tactic:
constructor
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set V
⊢ (G'.deleteVerts s).verts ⊆ G'.verts

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set V
⊢ ∀ ⦃v w : V⦄, (G'.deleteVerts s).Adj v w → G'.Adj v w

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
s : Set V
G' G'' : G.Subgraph
h : G' ≤ G''
⊢ G'.deleteVerts s ≤ G''.deleteVerts s

Tactic:
induce_mono h (Set.diff_subset_diff_left h.1)

Premises used: Set.diff_subset_diff_left, And.left, SimpleGraph.Subgraph.induce_mono
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G G' : SimpleGraph V
u : Set V
h : G ≤ G'
v w : (↑(verts (G := G) (deleteVerts ⊤ u)) : Type u)
hvw : SimpleGraph.Adj (Subgraph.coe (deleteVerts ⊤ u)) v w
⊢ SimpleGraph.Adj (Subgraph.coe (deleteVerts ⊤ u)) v w

Tactic:
aesop
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s s' : Set V
h : s ⊆ s'
⊢ G'.deleteVerts s' ≤ G'.deleteVerts s

Tactic:
induce_mono (le_refl _) (Set.diff_subset_diff_right h)

Premises used: le_refl, Set.diff_subset_diff_right, SimpleGraph.Subgraph.induce_mono
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set V
verts : ∀ (x : V), x ∈ (G'.deleteVerts (G'.verts ∩ s)).verts ↔ x ∈ (G'.deleteVerts s).verts
Adj : ∀ (x x_1 : V), (G'.deleteVerts (G'.verts ∩ s)).Adj x x_1 ↔ (G'.deleteVerts s).Adj x x_1
⊢ G'.deleteVerts (G'.verts ∩ s) = G'.deleteVerts s

Tactic:
ext
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set V
x : V
⊢ x ∈ (G'.deleteVerts (G'.verts ∩ s)).verts ↔ x ∈ (G'.deleteVerts s).verts

Tactic:
simp +contextual
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set V
x x_1 : V
⊢ (G'.deleteVerts (G'.verts ∩ s)).Adj x x_1 ↔ (G'.deleteVerts s).Adj x x_1

Tactic:
simp +contextual
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set V
verts : ∀ (x : V), x ∈ (G'.deleteVerts (s ∩ G'.verts)).verts ↔ x ∈ (G'.deleteVerts s).verts
Adj : ∀ (x x_1 : V), (G'.deleteVerts (s ∩ G'.verts)).Adj x x_1 ↔ (G'.deleteVerts s).Adj x x_1
⊢ G'.deleteVerts (s ∩ G'.verts) = G'.deleteVerts s

Tactic:
ext
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set V
x : V
⊢ x ∈ (G'.deleteVerts (s ∩ G'.verts)).verts ↔ x ∈ (G'.deleteVerts s).verts

Tactic:
simp +contextual
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set V
x x_1 : V
⊢ (G'.deleteVerts (s ∩ G'.verts)).Adj x x_1 ↔ (G'.deleteVerts s).Adj x x_1

Tactic:
simp +contextual
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : G.Subgraph
s u : Set V
r : DecidableRel G.Adj
x y : (↑(verts (G := G) (deleteVerts ⊤ u)) : Type u)
h : G.Adj (↑x : V) (↑y : V)
⊢ Membership.mem (γ := Set V) (verts (G := G) ⊤) (↑x : V)

Tactic:
trivial
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : G.Subgraph
s u : Set V
r : DecidableRel G.Adj
x y : (↑(verts (G := G) (deleteVerts ⊤ u)) : Type u)
h : G.Adj (↑x : V) (↑y : V)
⊢ Membership.mem (γ := Set V) (verts (G := G) ⊤) (↑y : V)

Tactic:
trivial
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : G.Subgraph
s_1 s : Set V
x : (↑(G'.deleteVerts s).verts : Type u)
v : V
hv : v ∈ (G'.deleteVerts s).verts
⊢ Membership.mem (γ := Set (↑G'.verts : Type u)) {v : (↑G'.verts : Type u) | (↑v : V) ∉ s}
    (Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) v ⋯)

Tactic:
aesop
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : G.Subgraph
s_1 s : Set V
x : (↑{v : (↑G'.verts : Type u) | (↑v : V) ∉ s} : Type u)
v : (↑G'.verts : Type u)
hv : Membership.mem (γ := Set (↑G'.verts : Type u)) {v : (↑G'.verts : Type u) | (↑v : V) ∉ s} v
⊢ (↑v : V) ∈ (G'.deleteVerts s).verts

Tactic:
simp_all
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : G.Subgraph
s_1 s : Set V
⊢ ∀ {a b : (↑(G'.deleteVerts s).verts : Type u)},
    SimpleGraph.Adj (V := (↑{v : (↑G'.verts : Type u) | (↑v : V) ∉ s} : Type u))
        (SimpleGraph.induce {v : (↑G'.verts : Type u) | (↑v : V) ∉ s} G'.coe)
        (({
              toFun := fun (x : (↑(G'.deleteVerts s).verts : Type u)) ↦
                match (motive :=
                  (↑(G'.deleteVerts s).verts : Type u) → (↑{v : (↑G'.verts : Type u) | (↑v : V) ∉ s} : Type u)) x with
                | ⟨v, hv⟩ =>
                  Subtype.mk (p := fun (x : (↑G'.verts : Type u)) ↦
                    Membership.mem (γ := Set (↑G'.verts : Type u)) {v : (↑G'.verts : Type u) | (↑v : V) ∉ s} x)
                    (Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) v ⋯) ⋯,
              invFun := fun (x : (↑{v : (↑G'.verts : Type u) | (↑v : V) ∉ s} : Type u)) ↦
                match (motive :=
                  (↑{v : (↑G'.verts : Type u) | (↑v : V) ∉ s} : Type u) → (↑(G'.deleteVerts s).verts : Type u)) x with
                | ⟨v, hv⟩ => Subtype.mk (p := fun (x : V) ↦ x ∈ (G'.deleteVerts s).verts) (↑v : V) ⋯,
              left_inv := ⋯, right_inv := ⋯ } :
            (a : (↑(G'.deleteVerts s).verts : Type u)) → (↑{v : (↑G'.verts : Type u) | (↑v : V) ∉ s} : Type u))
          a)
        (({
              toFun := fun (x : (↑(G'.deleteVerts s).verts : Type u)) ↦
                match (motive :=
                  (↑(G'.deleteVerts s).verts : Type u) → (↑{v : (↑G'.verts : Type u) | (↑v : V) ∉ s} : Type u)) x with
                | ⟨v, hv⟩ =>
                  Subtype.mk (p := fun (x : (↑G'.verts : Type u)) ↦
                    Membership.mem (γ := Set (↑G'.verts : Type u)) {v : (↑G'.verts : Type u) | (↑v : V) ∉ s} x)
                    (Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) v ⋯) ⋯,
              invFun := fun (x : (↑{v : (↑G'.verts : Type u) | (↑v : V) ∉ s} : Type u)) ↦
                match (motive :=
                  (↑{v : (↑G'.verts : Type u) | (↑v : V) ∉ s} : Type u) → (↑(G'.deleteVerts s).verts : Type u)) x with
                | ⟨v, hv⟩ => Subtype.mk (p := fun (x : V) ↦ x ∈ (G'.deleteVerts s).verts) (↑v : V) ⋯,
              left_inv := ⋯, right_inv := ⋯ } :
            (a : (↑(G'.deleteVerts s).verts : Type u)) → (↑{v : (↑G'.verts : Type u) | (↑v : V) ∉ s} : Type u))
          b) ↔
      (G'.deleteVerts s).coe.Adj a b

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Sum
Goal:
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
γ : Type u_7
G_1 : SimpleGraph V
H_1 : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v v' : V
w w' : W
G : SimpleGraph V
H : SimpleGraph W
u : V ⊕ W
inl :
  ∀ (val : V),
    ¬match (motive := V ⊕ W → V ⊕ W → Prop) Sum.inl val, Sum.inl val with
      | Sum.inl u, Sum.inl v => G.Adj u v
      | Sum.inr u, Sum.inr v => H.Adj u v
      | x, x_1 => false = true
inr :
  ∀ (val : W),
    ¬match (motive := V ⊕ W → V ⊕ W → Prop) Sum.inr val, Sum.inr val with
      | Sum.inl u, Sum.inl v => G.Adj u v
      | Sum.inr u, Sum.inr v => H.Adj u v
      | x, x_1 => false = true
⊢ ¬match (motive := V ⊕ W → V ⊕ W → Prop) u, u with
    | Sum.inl u, Sum.inl v => G.Adj u v
    | Sum.inr u, Sum.inr v => H.Adj u v
    | x, x_1 => false = true

Tactic:
cases u
-- Module: Mathlib.Combinatorics.SimpleGraph.Sum
Goal:
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
γ : Type u_7
G_1 : SimpleGraph V
H_1 : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v v' : V
w w' : W
G : SimpleGraph V
H : SimpleGraph W
val : V
⊢ ¬match (motive := V ⊕ W → V ⊕ W → Prop) Sum.inl val, Sum.inl val with
    | Sum.inl u, Sum.inl v => G.Adj u v
    | Sum.inr u, Sum.inr v => H.Adj u v
    | x, x_1 => false = true

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Sum
Goal:
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
γ : Type u_7
G_1 : SimpleGraph V
H_1 : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v v' : V
w w' : W
G : SimpleGraph V
H : SimpleGraph W
val : W
⊢ ¬match (motive := V ⊕ W → V ⊕ W → Prop) Sum.inr val, Sum.inr val with
    | Sum.inl u, Sum.inl v => G.Adj u v
    | Sum.inr u, Sum.inr v => H.Adj u v
    | x, x_1 => false = true

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Sum
Goal:
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v_1 v' : V
w w' : W
u v : V
⊢ (H ⊕g G).Adj ((Equiv.sumComm V W : (a : V ⊕ W) → W ⊕ V) (Sum.inl u))
      ((Equiv.sumComm V W : (a : V ⊕ W) → W ⊕ V) (Sum.inl v)) ↔
    (G ⊕g H).Adj (Sum.inl u) (Sum.inl v)

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Sum
Goal:
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v_1 v' : V
w w' : W
u : V
v : W
⊢ (H ⊕g G).Adj ((Equiv.sumComm V W : (a : V ⊕ W) → W ⊕ V) (Sum.inl u))
      ((Equiv.sumComm V W : (a : V ⊕ W) → W ⊕ V) (Sum.inr v)) ↔
    (G ⊕g H).Adj (Sum.inl u) (Sum.inr v)

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Sum
Goal:
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v_1 v' : V
w w' u : W
v : V
⊢ (H ⊕g G).Adj ((Equiv.sumComm V W : (a : V ⊕ W) → W ⊕ V) (Sum.inr u))
      ((Equiv.sumComm V W : (a : V ⊕ W) → W ⊕ V) (Sum.inl v)) ↔
    (G ⊕g H).Adj (Sum.inr u) (Sum.inl v)

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Sum
Goal:
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v_1 v' : V
w w' u v : W
⊢ (H ⊕g G).Adj ((Equiv.sumComm V W : (a : V ⊕ W) → W ⊕ V) (Sum.inr u))
      ((Equiv.sumComm V W : (a : V ⊕ W) → W ⊕ V) (Sum.inr v)) ↔
    (G ⊕g H).Adj (Sum.inr u) (Sum.inr v)

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Sum
Goal:
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v_1 v' : V
w w' : W
u v : V
⊢ (G ⊕g (H ⊕g I)).Adj ((Equiv.sumAssoc V W U : (a : (V ⊕ W) ⊕ U) → V ⊕ W ⊕ U) (Sum.inl (Sum.inl u)))
      ((Equiv.sumAssoc V W U : (a : (V ⊕ W) ⊕ U) → V ⊕ W ⊕ U) (Sum.inl (Sum.inl v))) ↔
    (G ⊕g H ⊕g I).Adj (Sum.inl (Sum.inl u)) (Sum.inl (Sum.inl v))

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Sum
Goal:
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v_1 v' : V
w w' : W
u : V
v : W
⊢ (G ⊕g (H ⊕g I)).Adj ((Equiv.sumAssoc V W U : (a : (V ⊕ W) ⊕ U) → V ⊕ W ⊕ U) (Sum.inl (Sum.inl u)))
      ((Equiv.sumAssoc V W U : (a : (V ⊕ W) ⊕ U) → V ⊕ W ⊕ U) (Sum.inl (Sum.inr v))) ↔
    (G ⊕g H ⊕g I).Adj (Sum.inl (Sum.inl u)) (Sum.inl (Sum.inr v))

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Sum
Goal:
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v_1 v' : V
w w' : W
u : V
v : U
⊢ (G ⊕g (H ⊕g I)).Adj ((Equiv.sumAssoc V W U : (a : (V ⊕ W) ⊕ U) → V ⊕ W ⊕ U) (Sum.inl (Sum.inl u)))
      ((Equiv.sumAssoc V W U : (a : (V ⊕ W) ⊕ U) → V ⊕ W ⊕ U) (Sum.inr v)) ↔
    (G ⊕g H ⊕g I).Adj (Sum.inl (Sum.inl u)) (Sum.inr v)

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Sum
Goal:
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v_1 v' : V
w w' u : W
v : V
⊢ (G ⊕g (H ⊕g I)).Adj ((Equiv.sumAssoc V W U : (a : (V ⊕ W) ⊕ U) → V ⊕ W ⊕ U) (Sum.inl (Sum.inr u)))
      ((Equiv.sumAssoc V W U : (a : (V ⊕ W) ⊕ U) → V ⊕ W ⊕ U) (Sum.inl (Sum.inl v))) ↔
    (G ⊕g H ⊕g I).Adj (Sum.inl (Sum.inr u)) (Sum.inl (Sum.inl v))

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Sum
Goal:
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v_1 v' : V
w w' u v : W
⊢ (G ⊕g (H ⊕g I)).Adj ((Equiv.sumAssoc V W U : (a : (V ⊕ W) ⊕ U) → V ⊕ W ⊕ U) (Sum.inl (Sum.inr u)))
      ((Equiv.sumAssoc V W U : (a : (V ⊕ W) ⊕ U) → V ⊕ W ⊕ U) (Sum.inl (Sum.inr v))) ↔
    (G ⊕g H ⊕g I).Adj (Sum.inl (Sum.inr u)) (Sum.inl (Sum.inr v))

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Sum
Goal:
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v_1 v' : V
w w' u : W
v : U
⊢ (G ⊕g (H ⊕g I)).Adj ((Equiv.sumAssoc V W U : (a : (V ⊕ W) ⊕ U) → V ⊕ W ⊕ U) (Sum.inl (Sum.inr u)))
      ((Equiv.sumAssoc V W U : (a : (V ⊕ W) ⊕ U) → V ⊕ W ⊕ U) (Sum.inr v)) ↔
    (G ⊕g H ⊕g I).Adj (Sum.inl (Sum.inr u)) (Sum.inr v)

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Sum
Goal:
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v_1 v' : V
w w' : W
u : U
v : V
⊢ (G ⊕g (H ⊕g I)).Adj ((Equiv.sumAssoc V W U : (a : (V ⊕ W) ⊕ U) → V ⊕ W ⊕ U) (Sum.inr u))
      ((Equiv.sumAssoc V W U : (a : (V ⊕ W) ⊕ U) → V ⊕ W ⊕ U) (Sum.inl (Sum.inl v))) ↔
    (G ⊕g H ⊕g I).Adj (Sum.inr u) (Sum.inl (Sum.inl v))

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Sum
Goal:
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v_1 v' : V
w w' : W
u : U
v : W
⊢ (G ⊕g (H ⊕g I)).Adj ((Equiv.sumAssoc V W U : (a : (V ⊕ W) ⊕ U) → V ⊕ W ⊕ U) (Sum.inr u))
      ((Equiv.sumAssoc V W U : (a : (V ⊕ W) ⊕ U) → V ⊕ W ⊕ U) (Sum.inl (Sum.inr v))) ↔
    (G ⊕g H ⊕g I).Adj (Sum.inr u) (Sum.inl (Sum.inr v))

Tactic:
simp