mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.SimpleGraph.Sum

Goal state before:
pp: case inl
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
G : SimpleGraph V
H : SimpleGraph W
G' : SimpleGraph V'
H' : SimpleGraph W'
f : G ↪g G'
g : H ↪g H'
v : V
⊢ ((g.sum f).comp Iso.sumComm.toEmbedding) (Sum.inl v) = (Iso.sumComm.toEmbedding.comp (f.sum g)) (Sum.inl v)

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Sum

Goal state before:
pp: case inr
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
G : SimpleGraph V
H : SimpleGraph W
G' : SimpleGraph V'
H' : SimpleGraph W'
f : G ↪g G'
g : H ↪g H'
w : W
⊢ ((g.sum f).comp Iso.sumComm.toEmbedding) (Sum.inr w) = (Iso.sumComm.toEmbedding.comp (f.sum g)) (Sum.inr w)

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Sum

Goal state before:
pp: case inl.inl
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
f : G ↪g G'
g : H ↪g H'
h : I ↪g I'
v : V
⊢ ((f.sum (g.sum h)).comp Iso.sumAssoc.toEmbedding) (Sum.inl (Sum.inl v)) =
    (Iso.sumAssoc.toEmbedding.comp ((f.sum g).sum h)) (Sum.inl (Sum.inl v))

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Sum

Goal state before:
pp: case inl.inr
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
f : G ↪g G'
g : H ↪g H'
h : I ↪g I'
w : W
⊢ ((f.sum (g.sum h)).comp Iso.sumAssoc.toEmbedding) (Sum.inl (Sum.inr w)) =
    (Iso.sumAssoc.toEmbedding.comp ((f.sum g).sum h)) (Sum.inl (Sum.inr w))

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Sum

Goal state before:
pp: case inr
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
f : G ↪g G'
g : H ↪g H'
h : I ↪g I'
u : U
⊢ ((f.sum (g.sum h)).comp Iso.sumAssoc.toEmbedding) (Sum.inr u) =
    (Iso.sumAssoc.toEmbedding.comp ((f.sum g).sum h)) (Sum.inr u)

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: case pos
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u u
hpc : p.IsCycle
i : ℕ
hi : p.getVert i = v ∧ i ≤ p.length
he : i = 0 ∨ i = p.length
⊢ (p.toSubgraph.neighborSet v).ncard = 2

Tactic:
have huv : u = v := by aesop
    rw [← huv, hpc.neighborSet_toSubgraph_endpoint]
    exact Set.ncard_pair hpc.snd_ne_penultimate

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: case inl.inl.inl
V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst✝³ : Finite α
inst✝² : Finite β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
this✝ : Fintype α
this : Fintype β
x✝ :
  ∃ left right, #left = Fintype.card α ∧ #right = Fintype.card β ∧ G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
left right : Finset (V ⊕ V)
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
l : V
hl : Sum.inl l ∈ left
hmem_left :
  ∀ {l' : V ⊕ V},
    l' ∈ left → ((Sum.inl l).isLeft = true → l'.isLeft = true) ∧ ((Sum.inl l).isRight = true → l'.isRight = true)
r : V
hr : Sum.inl r ∈ right
r' : V
hr' : Sum.inl r' ∈ right
⊢ ((Sum.inl r).isLeft = true → (Sum.inl r').isLeft = true) ∧ ((Sum.inl r).isRight = true → (Sum.inl r').isRight = true)

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: case inl.inl.inr
V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst✝³ : Finite α
inst✝² : Finite β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
this✝ : Fintype α
this : Fintype β
x✝ :
  ∃ left right, #left = Fintype.card α ∧ #right = Fintype.card β ∧ G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
left right : Finset (V ⊕ V)
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
l : V
hl : Sum.inl l ∈ left
hmem_left :
  ∀ {l' : V ⊕ V},
    l' ∈ left → ((Sum.inl l).isLeft = true → l'.isLeft = true) ∧ ((Sum.inl l).isRight = true → l'.isRight = true)
r : V
hr : Sum.inl r ∈ right
r' : V
hr' : Sum.inr r' ∈ right
⊢ ((Sum.inl r).isLeft = true → (Sum.inr r').isLeft = true) ∧ ((Sum.inl r).isRight = true → (Sum.inr r').isRight = true)

Tactic:
simp

Goal state after:
case inl.inl.inr
V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst✝³ : Finite α
inst✝² : Finite β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
this✝ : Fintype α
this : Fintype β
x✝ :
  ∃ left right, #left = Fintype.card α ∧ #right = Fintype.card β ∧ G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
left right : Finset (V ⊕ V)
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
l : V
hl : Sum.inl l ∈ left
hmem_left :
  ∀ {l' : V ⊕ V},
    l' ∈ left → ((Sum.inl l).isLeft = true → l'.isLeft = true) ∧ ((Sum.inl l).isRight = true → l'.isRight = true)
r : V
hr : Sum.inl r ∈ right
r' : V
hr' : Sum.inr r' ∈ right
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Sum

Goal state before:
pp: 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✝ v' : V
w w' : W
f : G ≃g G'
g : H ≃g H'
u v : V ⊕ W
⊢ (G' ⊕g H').Adj ((f.sumCongr g.toEquiv) u) ((f.sumCongr g.toEquiv) v) ↔ (G ⊕g H).Adj u v

Tactic:
by cases u <;> cases v <;> simp [f.map_rel_iff, g.map_rel_iff]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Sum

Goal state before:
pp: case inl
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
G : SimpleGraph V
H : SimpleGraph W
G' : SimpleGraph V'
H' : SimpleGraph W'
f : G ≃g G'
g : H ≃g H'
v : V
⊢ (sumComm.comp (f.sumCongr g)) (Sum.inl v) = ((g.sumCongr f).comp sumComm) (Sum.inl v)

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Sum

Goal state before:
pp: case inr
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
G : SimpleGraph V
H : SimpleGraph W
G' : SimpleGraph V'
H' : SimpleGraph W'
f : G ≃g G'
g : H ≃g H'
w : W
⊢ (sumComm.comp (f.sumCongr g)) (Sum.inr w) = ((g.sumCongr f).comp sumComm) (Sum.inr w)

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Sum

Goal state before:
pp: case inl.inl
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
f : G ≃g G'
g : H ≃g H'
h : I ≃g I'
v : V
⊢ (sumAssoc.comp ((f.sumCongr g).sumCongr h)) (Sum.inl (Sum.inl v)) =
    ((f.sumCongr (g.sumCongr h)).comp sumAssoc) (Sum.inl (Sum.inl v))

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Sum

Goal state before:
pp: case inl.inr
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
f : G ≃g G'
g : H ≃g H'
h : I ≃g I'
w : W
⊢ (sumAssoc.comp ((f.sumCongr g).sumCongr h)) (Sum.inl (Sum.inr w)) =
    ((f.sumCongr (g.sumCongr h)).comp sumAssoc) (Sum.inl (Sum.inr w))

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Sum

Goal state before:
pp: case inr
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
f : G ≃g G'
g : H ≃g H'
h : I ≃g I'
u : U
⊢ (sumAssoc.comp ((f.sumCongr g).sumCongr h)) (Sum.inr u) = ((f.sumCongr (g.sumCongr h)).comp sumAssoc) (Sum.inr u)

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: case inl.inr.inl
V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst✝³ : Finite α
inst✝² : Finite β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
this✝ : Fintype α
this : Fintype β
x✝ :
  ∃ left right, #left = Fintype.card α ∧ #right = Fintype.card β ∧ G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
left right : Finset (V ⊕ V)
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
l : V
hl : Sum.inl l ∈ left
hmem_left :
  ∀ {l' : V ⊕ V},
    l' ∈ left → ((Sum.inl l).isLeft = true → l'.isLeft = true) ∧ ((Sum.inl l).isRight = true → l'.isRight = true)
r : V
hr : Sum.inr r ∈ right
r' : V
hr' : Sum.inl r' ∈ right
⊢ ((Sum.inr r).isLeft = true → (Sum.inl r').isLeft = true) ∧ ((Sum.inr r).isRight = true → (Sum.inl r').isRight = true)

Tactic:
simp

Goal state after:
case inl.inr.inl
V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst✝³ : Finite α
inst✝² : Finite β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
this✝ : Fintype α
this : Fintype β
x✝ :
  ∃ left right, #left = Fintype.card α ∧ #right = Fintype.card β ∧ G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
left right : Finset (V ⊕ V)
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
l : V
hl : Sum.inl l ∈ left
hmem_left :
  ∀ {l' : V ⊕ V},
    l' ∈ left → ((Sum.inl l).isLeft = true → l'.isLeft = true) ∧ ((Sum.inl l).isRight = true → l'.isRight = true)
r : V
hr : Sum.inr r ∈ right
r' : V
hr' : Sum.inl r' ∈ right
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Sum

Goal state before:
pp: 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 v' : V
w w' : W
e : Sym2 V
he : e ∈ G.edgeSet
⊢ ∀ (a b : V) (h : G.Adj a b), ⟨s(Sum.inl a, Sum.inl b), h⟩ = ⟨s(Sum.inl b, Sum.inl a), ⋯⟩

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Sum

Goal state before:
pp: 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 v' : V
w w' : W
e : Sym2 W
he : e ∈ H.edgeSet
⊢ ∀ (a b : W) (h : H.Adj a b), ⟨s(Sum.inr a, Sum.inr b), h⟩ = ⟨s(Sum.inr b, Sum.inr a), ⋯⟩

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: case inl.inr.inr
V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst✝³ : Finite α
inst✝² : Finite β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
this✝ : Fintype α
this : Fintype β
x✝ :
  ∃ left right, #left = Fintype.card α ∧ #right = Fintype.card β ∧ G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
left right : Finset (V ⊕ V)
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
l : V
hl : Sum.inl l ∈ left
hmem_left :
  ∀ {l' : V ⊕ V},
    l' ∈ left → ((Sum.inl l).isLeft = true → l'.isLeft = true) ∧ ((Sum.inl l).isRight = true → l'.isRight = true)
r : V
hr : Sum.inr r ∈ right
r' : V
hr' : Sum.inr r' ∈ right
⊢ ((Sum.inr r).isLeft = true → (Sum.inr r').isLeft = true) ∧ ((Sum.inr r).isRight = true → (Sum.inr r').isRight = true)

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: case inr.inl.inl
V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst✝³ : Finite α
inst✝² : Finite β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
this✝ : Fintype α
this : Fintype β
x✝ :
  ∃ left right, #left = Fintype.card α ∧ #right = Fintype.card β ∧ G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
left right : Finset (V ⊕ V)
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
l : V
hl : Sum.inr l ∈ left
hmem_left :
  ∀ {l' : V ⊕ V},
    l' ∈ left → ((Sum.inr l).isLeft = true → l'.isLeft = true) ∧ ((Sum.inr l).isRight = true → l'.isRight = true)
r : V
hr : Sum.inl r ∈ right
r' : V
hr' : Sum.inl r' ∈ right
⊢ ((Sum.inl r).isLeft = true → (Sum.inl r').isLeft = true) ∧ ((Sum.inl r).isRight = true → (Sum.inl r').isRight = true)

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: case inr.inl.inr
V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst✝³ : Finite α
inst✝² : Finite β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
this✝ : Fintype α
this : Fintype β
x✝ :
  ∃ left right, #left = Fintype.card α ∧ #right = Fintype.card β ∧ G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
left right : Finset (V ⊕ V)
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
l : V
hl : Sum.inr l ∈ left
hmem_left :
  ∀ {l' : V ⊕ V},
    l' ∈ left → ((Sum.inr l).isLeft = true → l'.isLeft = true) ∧ ((Sum.inr l).isRight = true → l'.isRight = true)
r : V
hr : Sum.inl r ∈ right
r' : V
hr' : Sum.inr r' ∈ right
⊢ ((Sum.inl r).isLeft = true → (Sum.inr r').isLeft = true) ∧ ((Sum.inl r).isRight = true → (Sum.inr r').isRight = true)

Tactic:
simp

Goal state after:
case inr.inl.inr
V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst✝³ : Finite α
inst✝² : Finite β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
this✝ : Fintype α
this : Fintype β
x✝ :
  ∃ left right, #left = Fintype.card α ∧ #right = Fintype.card β ∧ G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
left right : Finset (V ⊕ V)
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
l : V
hl : Sum.inr l ∈ left
hmem_left :
  ∀ {l' : V ⊕ V},
    l' ∈ left → ((Sum.inr l).isLeft = true → l'.isLeft = true) ∧ ((Sum.inr l).isRight = true → l'.isRight = true)
r : V
hr : Sum.inl r ∈ right
r' : V
hr' : Sum.inr r' ∈ right
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: case inr.inr.inl
V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst✝³ : Finite α
inst✝² : Finite β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
this✝ : Fintype α
this : Fintype β
x✝ :
  ∃ left right, #left = Fintype.card α ∧ #right = Fintype.card β ∧ G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
left right : Finset (V ⊕ V)
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
l : V
hl : Sum.inr l ∈ left
hmem_left :
  ∀ {l' : V ⊕ V},
    l' ∈ left → ((Sum.inr l).isLeft = true → l'.isLeft = true) ∧ ((Sum.inr l).isRight = true → l'.isRight = true)
r : V
hr : Sum.inr r ∈ right
r' : V
hr' : Sum.inl r' ∈ right
⊢ ((Sum.inr r).isLeft = true → (Sum.inl r').isLeft = true) ∧ ((Sum.inr r).isRight = true → (Sum.inl r').isRight = true)

Tactic:
simp

Goal state after:
case inr.inr.inl
V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst✝³ : Finite α
inst✝² : Finite β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
this✝ : Fintype α
this : Fintype β
x✝ :
  ∃ left right, #left = Fintype.card α ∧ #right = Fintype.card β ∧ G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
left right : Finset (V ⊕ V)
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
l : V
hl : Sum.inr l ∈ left
hmem_left :
  ∀ {l' : V ⊕ V},
    l' ∈ left → ((Sum.inr l).isLeft = true → l'.isLeft = true) ∧ ((Sum.inr l).isRight = true → l'.isRight = true)
r : V
hr : Sum.inr r ∈ right
r' : V
hr' : Sum.inl r' ∈ right
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: case inr.inr.inr
V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst✝³ : Finite α
inst✝² : Finite β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
this✝ : Fintype α
this : Fintype β
x✝ :
  ∃ left right, #left = Fintype.card α ∧ #right = Fintype.card β ∧ G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
left right : Finset (V ⊕ V)
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
l : V
hl : Sum.inr l ∈ left
hmem_left :
  ∀ {l' : V ⊕ V},
    l' ∈ left → ((Sum.inr l).isLeft = true → l'.isLeft = true) ∧ ((Sum.inr l).isRight = true → l'.isRight = true)
r : V
hr : Sum.inr r ∈ right
r' : V
hr' : Sum.inr r' ∈ right
⊢ ((Sum.inr r).isLeft = true → (Sum.inr r').isLeft = true) ∧ ((Sum.inr r).isRight = true → (Sum.inr r').isRight = true)

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Sum

Goal state before:
pp: V : Type u_3
W : Type u_5
G : SimpleGraph V
H : SimpleGraph W
v : V
w : W
⊢ ¬(G ⊕g H).Adj (Sum.inl v) (Sum.inr w)

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x y : α × β
top_case : (G □ H).edist x y = ⊤ ↔ G.edist x.1 y.1 = ⊤ ∨ H.edist x.2 y.2 = ⊤
h : ¬(G □ H).edist x y = ⊤
rGH : G.edist x.1 y.1 ≠ ⊤ ∧ H.edist x.2 y.2 ≠ ⊤
wG : G.Walk x.1 y.1
hwG : ↑wG.length = G.edist x.1 y.1
wH : H.Walk x.2 y.2
hwH : ↑wH.length = H.edist x.2 y.2
w_app : (G □ H).Walk (x.1, x.2) (y.1, y.2) := (Walk.boxProdLeft H x.2 wG).append (Walk.boxProdRight G y.1 wH)
⊢ ((Walk.map (G.boxProdLeft H x.2).toHom wG).append (Walk.map (G.boxProdRight H y.1).toHom wH)).length =
    wG.length + wH.length

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Sum

Goal state before:
pp: V : Type u_3
W : Type u_5
G : SimpleGraph V
H : SimpleGraph W
v : V
w : W
p : (G ⊕g H).Walk (Sum.inl v) (Sum.inr w)
⊢ ∀ (x : V ⊕ W), x ∉ Set.range Sum.inl ↔ x ∈ Set.range Sum.inr

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Sum

Goal state before:
pp: V : Type u_3
W : Type u_5
G : SimpleGraph V
H : SimpleGraph W
v : V
w : W
p : (G ⊕g H).Walk (Sum.inl v) (Sum.inr w)
hs : ∀ (x : V ⊕ W), x ∉ Set.range Sum.inl ↔ x ∈ Set.range Sum.inr
⊢ Sum.inl v ∈ Set.range Sum.inl

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Sum

Goal state before:
pp: V : Type u_3
W : Type u_5
G : SimpleGraph V
H : SimpleGraph W
v : V
w : W
p : (G ⊕g H).Walk (Sum.inl v) (Sum.inr w)
hs : ∀ (x : V ⊕ W), x ∉ Set.range Sum.inl ↔ x ∈ Set.range Sum.inr
⊢ Sum.inr w ∉ Set.range Sum.inl

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
u v u✝ w w✝ : V
h : G.Adj u✝ w
p : G.Walk w w✝
ih : p.toSubgraph.Connected
⊢ w ∈ (G.subgraphOfAdj h ⊓ p.toSubgraph).verts

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
H : G.Subgraph
s t : Set V
sconn : (H.induce s).Preconnected
tconn : (H.induce t).Preconnected
sintert : (s ⊓ t).Nonempty
⊢ (H.induce s ⊔ H.induce t).verts = (H.induce (s ∪ t)).verts

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Sum

Goal state before:
pp: case top
V : Type u_3
W : Type u_5
G : SimpleGraph V
H : SimpleGraph W
hG : G.chromaticNumber ≤ ⊤
hH : H.chromaticNumber ≤ ⊤
⊢ (G ⊕g H).chromaticNumber ≤ ⊤

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Sum

Goal state before:
pp: case inl
V : Type u_3
W : Type u_5
G : SimpleGraph V
H : SimpleGraph W
v v' : V
⊢ Sum.inl v' ∈ (G ⊕g H).neighborSet (Sum.inl v) ↔ Sum.inl v' ∈ Sum.inl '' G.neighborSet v

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Sum

Goal state before:
pp: case inr
V : Type u_3
W : Type u_5
G : SimpleGraph V
H : SimpleGraph W
v : V
w' : W
⊢ Sum.inr w' ∈ (G ⊕g H).neighborSet (Sum.inl v) ↔ Sum.inr w' ∈ Sum.inl '' G.neighborSet v

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Sum

Goal state before:
pp: case inl
V : Type u_3
W : Type u_5
G : SimpleGraph V
H : SimpleGraph W
w : W
v' : V
⊢ Sum.inl v' ∈ (G ⊕g H).neighborSet (Sum.inr w) ↔ Sum.inl v' ∈ Sum.inr '' H.neighborSet w

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Sum

Goal state before:
pp: case inr
V : Type u_3
W : Type u_5
G : SimpleGraph V
H : SimpleGraph W
w w' : W
⊢ Sum.inr w' ∈ (G ⊕g H).neighborSet (Sum.inr w) ↔ Sum.inr w' ∈ Sum.inr '' H.neighborSet w

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Hasse

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Preorder α
a b : α
⊢ ∀ {a b : αᵒᵈ}, (hasse α).Adj (ofDual a) (ofDual b) ↔ (hasse αᵒᵈ).Adj a b

Tactic:
by simp [or_comm]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Hasse

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b c : α
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
hc : (hasse α).IsClique ↑{a, b, c}
hcard : {a, b, c}.card = 3
⊢ a ∈ ↑{a, b, c}

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Hasse

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b c : α
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
hc : (hasse α).IsClique ↑{a, b, c}
hcard : {a, b, c}.card = 3
⊢ b ∈ ↑{a, b, c}

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Hasse

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b c : α
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
hc : (hasse α).IsClique ↑{a, b, c}
hcard : {a, b, c}.card = 3
this : (hasse α).Adj a b
⊢ b ∈ ↑{a, b, c}

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Hasse

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b c : α
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
hc : (hasse α).IsClique ↑{a, b, c}
hcard : {a, b, c}.card = 3
this : (hasse α).Adj a b
⊢ c ∈ ↑{a, b, c}

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Hasse

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b c : α
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
hc : (hasse α).IsClique ↑{a, b, c}
hcard : {a, b, c}.card = 3
this✝ : (hasse α).Adj a b
this : (hasse α).Adj b c
⊢ a ∈ ↑{a, b, c}

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Hasse

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b c : α
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
hc : (hasse α).IsClique ↑{a, b, c}
hcard : {a, b, c}.card = 3
this✝ : (hasse α).Adj a b
this : (hasse α).Adj b c
⊢ c ∈ ↑{a, b, c}

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.CycleGraph

Goal state before:
pp: n : ℕ
⊢ pathGraph 0 ≤ cycleGraph 0

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.CycleGraph

Goal state before:
pp: n : ℕ
⊢ pathGraph 1 ≤ cycleGraph 1

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: case refine_2.hu
V : Type u
G : SimpleGraph V
Gpc : G.Preconnected
t : Finset V
u : V
ut : u ∈ t
⊢ u ∈ ↑(t.biUnion fun v ↦ (Nonempty.some ⋯).support.toFinset)

Tactic:
simp only [Finset.coe_biUnion, Finset.mem_coe, List.coe_toFinset, Set.mem_iUnion,
                 Set.mem_ofPred_eq, Walk.start_mem_support, exists_prop, and_true]
      exact ⟨u, ut⟩

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst✝³ : Finite α
inst✝² : Finite β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
this✝ : Fintype α
this : Fintype β
x✝ :
  ∃ left right, #left = Fintype.card α ∧ #right = Fintype.card β ∧ G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
left right : Finset (V ⊕ V)
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
l : V
hl : Sum.inl l ∈ left
hmem_left :
  ∀ {l' : V ⊕ V},
    l' ∈ left → ((Sum.inl l).isLeft = true → l'.isLeft = true) ∧ ((Sum.inl l).isRight = true → l'.isRight = true)
r : V
hr : Sum.inr r ∈ right
hmem_right :
  ∀ {r' : V ⊕ V},
    r' ∈ right → ((Sum.inr r).isLeft = true → r'.isLeft = true) ∧ ((Sum.inr r).isRight = true → r'.isRight = true)
i : V
hi : i ∈ left.toLeft
j : V
hj : j ∈ left.toLeft
⊢ Sum.inl i = Sum.inl j → i = j

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.CycleGraph

Goal state before:
pp: case zero
n : ℕ
hm : 0 ≤ n + 3
⊢ (cycle n).getVert 0 = ⟨(n + 3 - 0) % (n + 3), ⋯⟩

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.CycleGraph

Goal state before:
pp: n : ℕ
⊢ 3 ≤ (cycle n).length

Tactic:
simp

Goal state after: