mathlib-initiative/mathlib-tactics huggingface dataset:
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
r : V
hr : Sum.inl r ∈ right
l' : V
hl' : Sum.inr l' ∈ left
⊢ ((Sum.inl l).isLeft = true → (Sum.inr l').isLeft = true) ∧ ((Sum.inl l).isRight = true → (Sum.inr l').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
r : V
hr : Sum.inl r ∈ right
l' : V
hl' : Sum.inr l' ∈ left
⊢ False
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
r : V
hr : Sum.inr r ∈ right
l' : V
hl' : Sum.inl l' ∈ left
⊢ ((Sum.inl l).isLeft = true → (Sum.inl l').isLeft = true) ∧ ((Sum.inl l).isRight = true → (Sum.inl l').isRight = true)

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
r : V
hr : Sum.inr r ∈ right
l' : V
hl' : Sum.inr l' ∈ left
⊢ ((Sum.inl l).isLeft = true → (Sum.inr l').isLeft = true) ∧ ((Sum.inl l).isRight = true → (Sum.inr l').isRight = true)

Tactic:
simp

Goal state after:
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
r : V
hr : Sum.inr r ∈ right
l' : V
hl' : Sum.inr l' ∈ left
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Metric

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
⊢ G.dist u v ≠ 0 ↔ u ≠ v ∧ G.Reachable u v

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
r : V
hr : Sum.inl r ∈ right
l' : V
hl' : Sum.inl l' ∈ left
⊢ ((Sum.inr l).isLeft = true → (Sum.inl l').isLeft = true) ∧ ((Sum.inr l).isRight = true → (Sum.inl l').isRight = true)

Tactic:
simp

Goal state after:
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
r : V
hr : Sum.inl r ∈ right
l' : V
hl' : Sum.inl l' ∈ left
⊢ False
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
r : V
hr : Sum.inl r ∈ right
l' : V
hl' : Sum.inr l' ∈ left
⊢ ((Sum.inr l).isLeft = true → (Sum.inr l').isLeft = true) ∧ ((Sum.inr l).isRight = true → (Sum.inr l').isRight = true)

Tactic:
simp

Goal state after:
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
r : V
hr : Sum.inr r ∈ right
l' : V
hl' : Sum.inl l' ∈ left
⊢ ((Sum.inr l).isLeft = true → (Sum.inl l').isLeft = true) ∧ ((Sum.inr l).isRight = true → (Sum.inl l').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
r : V
hr : Sum.inr r ∈ right
l' : V
hl' : Sum.inl l' ∈ left
⊢ 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
r : V
hr : Sum.inr r ∈ right
l' : V
hl' : Sum.inr l' ∈ left
⊢ ((Sum.inr l).isLeft = true → (Sum.inr l').isLeft = true) ∧ ((Sum.inr l).isRight = true → (Sum.inr l').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' : V
⊢ (G ⊕g H).Adj (Sum.inl v) (Sum.inl v') ↔ G.Adj v v'

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
w w' : W
⊢ (G ⊕g H).Adj (Sum.inr w) (Sum.inr w') ↔ H.Adj w 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
γ : 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
u v : V
⊢ (H ⊕g G).Adj ((Equiv.sumComm V W) (Sum.inl u)) ((Equiv.sumComm V W) (Sum.inl v)) ↔
    (G ⊕g H).Adj (Sum.inl u) (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
γ : 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
u : V
v : W
⊢ (H ⊕g G).Adj ((Equiv.sumComm V W) (Sum.inl u)) ((Equiv.sumComm V W) (Sum.inr v)) ↔
    (G ⊕g H).Adj (Sum.inl u) (Sum.inr v)

Tactic:
simp

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

Goal state before:
pp: case inr.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
γ : 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' u : W
v : V
⊢ (H ⊕g G).Adj ((Equiv.sumComm V W) (Sum.inr u)) ((Equiv.sumComm V W) (Sum.inl v)) ↔
    (G ⊕g H).Adj (Sum.inr u) (Sum.inl v)

Tactic:
simp

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

Goal state before:
pp: case inr.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
γ : 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' u v : W
⊢ (H ⊕g G).Adj ((Equiv.sumComm V W) (Sum.inr u)) ((Equiv.sumComm V W) (Sum.inr v)) ↔
    (G ⊕g H).Adj (Sum.inr u) (Sum.inr v)

Tactic:
simp

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

Goal state before:
pp: case inl.inl.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
γ : 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
u v : V
⊢ (G ⊕g (H ⊕g I)).Adj ((Equiv.sumAssoc V W U) (Sum.inl (Sum.inl u))) ((Equiv.sumAssoc 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

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

Goal state before:
pp: case inl.inl.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
γ : 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
u : V
v : W
⊢ (G ⊕g (H ⊕g I)).Adj ((Equiv.sumAssoc V W U) (Sum.inl (Sum.inl u))) ((Equiv.sumAssoc 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

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

Goal state before:
pp: case inl.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
γ : 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
u : V
v : U
⊢ (G ⊕g (H ⊕g I)).Adj ((Equiv.sumAssoc V W U) (Sum.inl (Sum.inl u))) ((Equiv.sumAssoc V W U) (Sum.inr v)) ↔
    (G ⊕g H ⊕g I).Adj (Sum.inl (Sum.inl u)) (Sum.inr v)

Tactic:
simp

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

Goal state before:
pp: case inl.inr.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
γ : 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' u : W
v : V
⊢ (G ⊕g (H ⊕g I)).Adj ((Equiv.sumAssoc V W U) (Sum.inl (Sum.inr u))) ((Equiv.sumAssoc 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

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

Goal state before:
pp: case inl.inr.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
γ : 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' u v : W
⊢ (G ⊕g (H ⊕g I)).Adj ((Equiv.sumAssoc V W U) (Sum.inl (Sum.inr u))) ((Equiv.sumAssoc 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

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

Goal state before:
pp: case inl.inr.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
γ : 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' u : W
v : U
⊢ (G ⊕g (H ⊕g I)).Adj ((Equiv.sumAssoc V W U) (Sum.inl (Sum.inr u))) ((Equiv.sumAssoc V W U) (Sum.inr v)) ↔
    (G ⊕g H ⊕g I).Adj (Sum.inl (Sum.inr u)) (Sum.inr v)

Tactic:
simp

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

Goal state before:
pp: case inr.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
γ : 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
u : U
v : V
⊢ (G ⊕g (H ⊕g I)).Adj ((Equiv.sumAssoc V W U) (Sum.inr u)) ((Equiv.sumAssoc V W U) (Sum.inl (Sum.inl v))) ↔
    (G ⊕g H ⊕g I).Adj (Sum.inr u) (Sum.inl (Sum.inl v))

Tactic:
simp

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

Goal state before:
pp: case inr.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
γ : 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
u : U
v : W
⊢ (G ⊕g (H ⊕g I)).Adj ((Equiv.sumAssoc V W U) (Sum.inr u)) ((Equiv.sumAssoc V W U) (Sum.inl (Sum.inr v))) ↔
    (G ⊕g H ⊕g I).Adj (Sum.inr u) (Sum.inl (Sum.inr v))

Tactic:
simp

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

Goal state before:
pp: case inr.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
γ : 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
u v : U
⊢ (G ⊕g (H ⊕g I)).Adj ((Equiv.sumAssoc V W U) (Sum.inr u)) ((Equiv.sumAssoc V W U) (Sum.inr v)) ↔
    (G ⊕g H ⊕g I).Adj (Sum.inr u) (Sum.inr v)

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
u v : V
⊢ (fun u ↦ Sum.inl u) u = (fun u ↦ Sum.inl u) v → u = v

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
⊢ ∀ {a b : V},
    (G ⊕g H).Adj ({ toFun := fun u ↦ Sum.inl u, inj' := ⋯ } a) ({ toFun := fun u ↦ Sum.inl u, inj' := ⋯ } b) ↔ G.Adj a b

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' u v : W
⊢ (fun u ↦ Sum.inr u) u = (fun u ↦ Sum.inr u) v → u = v

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
⊢ ∀ {a b : W},
    (G ⊕g H).Adj ({ toFun := fun u ↦ Sum.inr u, inj' := ⋯ } a) ({ toFun := fun u ↦ Sum.inr u, inj' := ⋯ } b) ↔ H.Adj a b

Tactic:
simp

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 : W
⊢ ((f.sum g).comp Iso.sumComm.toHom) (Sum.inl v) = (Iso.sumComm.toHom.comp (g.sum f)) (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 : V
⊢ ((f.sum g).comp Iso.sumComm.toHom) (Sum.inr w) = (Iso.sumComm.toHom.comp (g.sum f)) (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.toHom) (Sum.inl (Sum.inl v)) =
    (Iso.sumAssoc.toHom.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.toHom) (Sum.inl (Sum.inr w)) =
    (Iso.sumAssoc.toHom.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.toHom) (Sum.inr u) = (Iso.sumAssoc.toHom.comp ((f.sum g).sum h)) (Sum.inr u)

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
V : Type u_4
V₁ : Type u_5
V₂ : Type u_6
W : Type u_7
W₁ : Type u_8
W₂ : Type u_9
G✝ : SimpleGraph α
H : SimpleGraph β
G : SimpleGraph V
H₁ : SimpleGraph W₁
H₂ : SimpleGraph W₂
⊢ ∀ {a b : V × (W₁ ⊕ W₂)},
    (G □ H₁ ⊕g G □ H₂).Adj ((Equiv.prodSumDistrib V W₁ W₂) a) ((Equiv.prodSumDistrib V W₁ W₂) b) ↔
      (G □ (H₁ ⊕g H₂)).Adj a b

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
V : Type u_4
V₁ : Type u_5
V₂ : Type u_6
W : Type u_7
W₁ : Type u_8
W₂ : Type u_9
G : SimpleGraph α
H✝ : SimpleGraph β
G₁ : SimpleGraph V₁
G₂ : SimpleGraph V₂
H : SimpleGraph W
⊢ ∀ {a b : (V₁ ⊕ V₂) × W},
    (G₁ □ H ⊕g G₂ □ H).Adj ((Equiv.sumProdDistrib V₁ V₂ W) a) ((Equiv.sumProdDistrib V₁ V₂ W) b) ↔
      ((G₁ ⊕g G₂) □ H).Adj a b

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
γ : 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'
val✝¹ val✝ : V
⊢ Sum.map (⇑f) (⇑g) (Sum.inl val✝¹) = Sum.map (⇑f) (⇑g) (Sum.inl val✝) → Sum.inl val✝¹ = Sum.inl val✝

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
γ : 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'
val✝¹ : V
val✝ : W
⊢ Sum.map (⇑f) (⇑g) (Sum.inl val✝¹) = Sum.map (⇑f) (⇑g) (Sum.inr val✝) → Sum.inl val✝¹ = Sum.inr val✝

Tactic:
simp

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

Goal state before:
pp: case inr.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
γ : 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'
val✝¹ : W
val✝ : V
⊢ Sum.map (⇑f) (⇑g) (Sum.inr val✝¹) = Sum.map (⇑f) (⇑g) (Sum.inl val✝) → Sum.inr val✝¹ = Sum.inl val✝

Tactic:
simp

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

Goal state before:
pp: case inr.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
γ : 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'
val✝¹ val✝ : W
⊢ Sum.map (⇑f) (⇑g) (Sum.inr val✝¹) = Sum.map (⇑f) (⇑g) (Sum.inr val✝) → Sum.inr val✝¹ = Sum.inr val✝

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
γ : 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'
val✝¹ val✝ : V
⊢ (G' ⊕g H').Adj ({ toFun := Sum.map ⇑f ⇑g, inj' := ⋯ } (Sum.inl val✝¹))
      ({ toFun := Sum.map ⇑f ⇑g, inj' := ⋯ } (Sum.inl val✝)) ↔
    (G ⊕g H).Adj (Sum.inl val✝¹) (Sum.inl val✝)

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
γ : 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'
val✝¹ : V
val✝ : W
⊢ (G' ⊕g H').Adj ({ toFun := Sum.map ⇑f ⇑g, inj' := ⋯ } (Sum.inl val✝¹))
      ({ toFun := Sum.map ⇑f ⇑g, inj' := ⋯ } (Sum.inr val✝)) ↔
    (G ⊕g H).Adj (Sum.inl val✝¹) (Sum.inr val✝)

Tactic:
simp

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

Goal state before:
pp: case inr.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
γ : 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'
val✝¹ : W
val✝ : V
⊢ (G' ⊕g H').Adj ({ toFun := Sum.map ⇑f ⇑g, inj' := ⋯ } (Sum.inr val✝¹))
      ({ toFun := Sum.map ⇑f ⇑g, inj' := ⋯ } (Sum.inl val✝)) ↔
    (G ⊕g H).Adj (Sum.inr val✝¹) (Sum.inl val✝)

Tactic:
simp

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

Goal state before:
pp: case inr.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
γ : 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'
val✝¹ val✝ : W
⊢ (G' ⊕g H').Adj ({ toFun := Sum.map ⇑f ⇑g, inj' := ⋯ } (Sum.inr val✝¹))
      ({ toFun := Sum.map ⇑f ⇑g, inj' := ⋯ } (Sum.inr val✝)) ↔
    (G ⊕g H).Adj (Sum.inr val✝¹) (Sum.inr val✝)

Tactic:
simp

Goal state after: