awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 v' : V
w w' : W
f : G ↪g G'
g : H ↪g H'
val val_1 : W
⊢ (G' ⊕g H').Adj
      (({ toFun := Sum.map (⇑f : (a : V) → V') (⇑g : (a : W) → W'), inj' := ⋯ } : (a : V ⊕ W) → V' ⊕ W') (Sum.inr val))
      (({ toFun := Sum.map (⇑f : (a : V) → V') (⇑g : (a : W) → W'), inj' := ⋯ } : (a : V ⊕ W) → V' ⊕ W')
        (Sum.inr val_1)) ↔
    (G ⊕g H).Adj (Sum.inr val) (Sum.inr val_1)

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Sum
Goal:
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'
⊢ (f.sum g).toHom = f.toHom.sum g.toHom

Tactic:
rfl

Premises used: Sum.map, SimpleGraph.Hom.sum, rfl, Sum.elim
-- Module: Mathlib.Combinatorics.SimpleGraph.Sum
Goal:
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'
h :
  ∀ (v : V),
    Eq (α := W' ⊕ V') (((g.sum f).comp (Iso.toEmbedding Iso.sumComm) : (a : V ⊕ W) → W' ⊕ V') (Sum.inl v) : W' ⊕ V')
      ((comp (Iso.toEmbedding Iso.sumComm) (f.sum g) : (a : V ⊕ W) → W' ⊕ V') (Sum.inl v) : W' ⊕ V')
h₁ :
  ∀ (w : W),
    Eq (α := W' ⊕ V') (((g.sum f).comp (Iso.toEmbedding Iso.sumComm) : (a : V ⊕ W) → W' ⊕ V') (Sum.inr w) : W' ⊕ V')
      ((comp (Iso.toEmbedding Iso.sumComm) (f.sum g) : (a : V ⊕ W) → W' ⊕ V') (Sum.inr w) : W' ⊕ V')
⊢ (g.sum f).comp (Iso.toEmbedding Iso.sumComm) = comp (Iso.toEmbedding Iso.sumComm) (f.sum g)

Tactic:
ext (v | w)
-- Module: Mathlib.Combinatorics.SimpleGraph.Sum
Goal:
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
⊢ Eq (α := W' ⊕ V') (((g.sum f).comp (Iso.toEmbedding Iso.sumComm) : (a : V ⊕ W) → W' ⊕ V') (Sum.inl v) : W' ⊕ V')
    ((comp (Iso.toEmbedding Iso.sumComm) (f.sum g) : (a : V ⊕ W) → W' ⊕ V') (Sum.inl v) : W' ⊕ V')

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Sum
Goal:
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
⊢ Eq (α := W' ⊕ V') (((g.sum f).comp (Iso.toEmbedding Iso.sumComm) : (a : V ⊕ W) → W' ⊕ V') (Sum.inr w) : W' ⊕ V')
    ((comp (Iso.toEmbedding Iso.sumComm) (f.sum g) : (a : V ⊕ W) → W' ⊕ V') (Sum.inr w) : W' ⊕ 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
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'
h₁ :
  ∀ (v : V),
    Eq (α := V' ⊕ W' ⊕ U')
      (((f.sum (g.sum h)).comp (Iso.toEmbedding Iso.sumAssoc) : (a : (V ⊕ W) ⊕ U) → V' ⊕ W' ⊕ U')
          (Sum.inl (Sum.inl v)) :
        V' ⊕ W' ⊕ U')
      ((comp (Iso.toEmbedding Iso.sumAssoc) ((f.sum g).sum h) : (a : (V ⊕ W) ⊕ U) → V' ⊕ W' ⊕ U')
          (Sum.inl (Sum.inl v)) :
        V' ⊕ W' ⊕ U')
h₂ :
  ∀ (w : W),
    Eq (α := V' ⊕ W' ⊕ U')
      (((f.sum (g.sum h)).comp (Iso.toEmbedding Iso.sumAssoc) : (a : (V ⊕ W) ⊕ U) → V' ⊕ W' ⊕ U')
          (Sum.inl (Sum.inr w)) :
        V' ⊕ W' ⊕ U')
      ((comp (Iso.toEmbedding Iso.sumAssoc) ((f.sum g).sum h) : (a : (V ⊕ W) ⊕ U) → V' ⊕ W' ⊕ U')
          (Sum.inl (Sum.inr w)) :
        V' ⊕ W' ⊕ U')
h₃ :
  ∀ (u : U),
    Eq (α := V' ⊕ W' ⊕ U')
      (((f.sum (g.sum h)).comp (Iso.toEmbedding Iso.sumAssoc) : (a : (V ⊕ W) ⊕ U) → V' ⊕ W' ⊕ U') (Sum.inr u) :
        V' ⊕ W' ⊕ U')
      ((comp (Iso.toEmbedding Iso.sumAssoc) ((f.sum g).sum h) : (a : (V ⊕ W) ⊕ U) → V' ⊕ W' ⊕ U') (Sum.inr u) :
        V' ⊕ W' ⊕ U')
⊢ (f.sum (g.sum h)).comp (Iso.toEmbedding Iso.sumAssoc) = comp (Iso.toEmbedding Iso.sumAssoc) ((f.sum g).sum h)

Tactic:
ext ((v | w) | 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
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
⊢ Eq (α := V' ⊕ W' ⊕ U')
    (((f.sum (g.sum h)).comp (Iso.toEmbedding Iso.sumAssoc) : (a : (V ⊕ W) ⊕ U) → V' ⊕ W' ⊕ U') (Sum.inl (Sum.inl v)) :
      V' ⊕ W' ⊕ U')
    ((comp (Iso.toEmbedding Iso.sumAssoc) ((f.sum g).sum h) : (a : (V ⊕ W) ⊕ U) → V' ⊕ W' ⊕ U') (Sum.inl (Sum.inl v)) :
      V' ⊕ W' ⊕ U')

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
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
⊢ Eq (α := V' ⊕ W' ⊕ U')
    (((f.sum (g.sum h)).comp (Iso.toEmbedding Iso.sumAssoc) : (a : (V ⊕ W) ⊕ U) → V' ⊕ W' ⊕ U') (Sum.inl (Sum.inr w)) :
      V' ⊕ W' ⊕ U')
    ((comp (Iso.toEmbedding Iso.sumAssoc) ((f.sum g).sum h) : (a : (V ⊕ W) ⊕ U) → V' ⊕ W' ⊕ U') (Sum.inl (Sum.inr w)) :
      V' ⊕ W' ⊕ U')

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
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
⊢ Eq (α := V' ⊕ W' ⊕ U')
    (((f.sum (g.sum h)).comp (Iso.toEmbedding Iso.sumAssoc) : (a : (V ⊕ W) ⊕ U) → V' ⊕ W' ⊕ U') (Sum.inr u) :
      V' ⊕ W' ⊕ U')
    ((comp (Iso.toEmbedding Iso.sumAssoc) ((f.sum g).sum h) : (a : (V ⊕ W) ⊕ U) → V' ⊕ W' ⊕ U') (Sum.inr u) :
      V' ⊕ W' ⊕ U')

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
f : G ≃g G'
g : H ≃g H'
u v : V ⊕ W
inl :
  ∀ (val : V),
    (G' ⊕g H').Adj
        ((f.toEquiv (r := G.Adj) (s := G'.Adj).sumCongr (g.toEquiv (r := H.Adj) (s := H'.Adj)) : (a : V ⊕ W) → V' ⊕ W')
          (Sum.inl val))
        ((f.toEquiv (r := G.Adj) (s := G'.Adj).sumCongr (g.toEquiv (r := H.Adj) (s := H'.Adj)) : (a : V ⊕ W) → V' ⊕ W')
          v) ↔
      (G ⊕g H).Adj (Sum.inl val) v
inr :
  ∀ (val : W),
    (G' ⊕g H').Adj
        ((f.toEquiv (r := G.Adj) (s := G'.Adj).sumCongr (g.toEquiv (r := H.Adj) (s := H'.Adj)) : (a : V ⊕ W) → V' ⊕ W')
          (Sum.inr val))
        ((f.toEquiv (r := G.Adj) (s := G'.Adj).sumCongr (g.toEquiv (r := H.Adj) (s := H'.Adj)) : (a : V ⊕ W) → V' ⊕ W')
          v) ↔
      (G ⊕g H).Adj (Sum.inr val) v
⊢ (G' ⊕g H').Adj
      ((f.toEquiv (r := G.Adj) (s := G'.Adj).sumCongr (g.toEquiv (r := H.Adj) (s := H'.Adj)) : (a : V ⊕ W) → V' ⊕ W') u)
      ((f.toEquiv (r := G.Adj) (s := G'.Adj).sumCongr (g.toEquiv (r := H.Adj) (s := H'.Adj)) : (a : V ⊕ W) → V' ⊕ W')
        v) ↔
    (G ⊕g H).Adj u v

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 : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v_1 v' : V
w w' : W
f : G ≃g G'
g : H ≃g H'
v : V ⊕ W
val : V
inl :
  ∀ (val_1 : V),
    (G' ⊕g H').Adj
        ((f.toEquiv (r := G.Adj) (s := G'.Adj).sumCongr (g.toEquiv (r := H.Adj) (s := H'.Adj)) : (a : V ⊕ W) → V' ⊕ W')
          (Sum.inl val))
        ((f.toEquiv (r := G.Adj) (s := G'.Adj).sumCongr (g.toEquiv (r := H.Adj) (s := H'.Adj)) : (a : V ⊕ W) → V' ⊕ W')
          (Sum.inl val_1)) ↔
      (G ⊕g H).Adj (Sum.inl val) (Sum.inl val_1)
inl₁ :
  ∀ (val_1 : W),
    (G' ⊕g H').Adj
        ((f.toEquiv (r := G.Adj) (s := G'.Adj).sumCongr (g.toEquiv (r := H.Adj) (s := H'.Adj)) : (a : V ⊕ W) → V' ⊕ W')
          (Sum.inl val))
        ((f.toEquiv (r := G.Adj) (s := G'.Adj).sumCongr (g.toEquiv (r := H.Adj) (s := H'.Adj)) : (a : V ⊕ W) → V' ⊕ W')
          (Sum.inr val_1)) ↔
      (G ⊕g H).Adj (Sum.inl val) (Sum.inr val_1)
⊢ (G' ⊕g H').Adj
      ((f.toEquiv (r := G.Adj) (s := G'.Adj).sumCongr (g.toEquiv (r := H.Adj) (s := H'.Adj)) : (a : V ⊕ W) → V' ⊕ W')
        (Sum.inl val))
      ((f.toEquiv (r := G.Adj) (s := G'.Adj).sumCongr (g.toEquiv (r := H.Adj) (s := H'.Adj)) : (a : V ⊕ W) → V' ⊕ W')
        v) ↔
    (G ⊕g H).Adj (Sum.inl val) v

Tactic:
cases v
-- 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
f : G ≃g G'
g : H ≃g H'
v : V ⊕ W
val : W
inr :
  ∀ (val_1 : V),
    (G' ⊕g H').Adj
        ((f.toEquiv (r := G.Adj) (s := G'.Adj).sumCongr (g.toEquiv (r := H.Adj) (s := H'.Adj)) : (a : V ⊕ W) → V' ⊕ W')
          (Sum.inr val))
        ((f.toEquiv (r := G.Adj) (s := G'.Adj).sumCongr (g.toEquiv (r := H.Adj) (s := H'.Adj)) : (a : V ⊕ W) → V' ⊕ W')
          (Sum.inl val_1)) ↔
      (G ⊕g H).Adj (Sum.inr val) (Sum.inl val_1)
inr₁ :
  ∀ (val_1 : W),
    (G' ⊕g H').Adj
        ((f.toEquiv (r := G.Adj) (s := G'.Adj).sumCongr (g.toEquiv (r := H.Adj) (s := H'.Adj)) : (a : V ⊕ W) → V' ⊕ W')
          (Sum.inr val))
        ((f.toEquiv (r := G.Adj) (s := G'.Adj).sumCongr (g.toEquiv (r := H.Adj) (s := H'.Adj)) : (a : V ⊕ W) → V' ⊕ W')
          (Sum.inr val_1)) ↔
      (G ⊕g H).Adj (Sum.inr val) (Sum.inr val_1)
⊢ (G' ⊕g H').Adj
      ((f.toEquiv (r := G.Adj) (s := G'.Adj).sumCongr (g.toEquiv (r := H.Adj) (s := H'.Adj)) : (a : V ⊕ W) → V' ⊕ W')
        (Sum.inr val))
      ((f.toEquiv (r := G.Adj) (s := G'.Adj).sumCongr (g.toEquiv (r := H.Adj) (s := H'.Adj)) : (a : V ⊕ W) → V' ⊕ W')
        v) ↔
    (G ⊕g H).Adj (Sum.inr val) v

Tactic:
cases v
-- 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 v' : V
w w' : W
f : G ≃g G'
g : H ≃g H'
val val_1 : V
⊢ (G' ⊕g H').Adj
      ((f.toEquiv (r := G.Adj) (s := G'.Adj).sumCongr (g.toEquiv (r := H.Adj) (s := H'.Adj)) : (a : V ⊕ W) → V' ⊕ W')
        (Sum.inl val))
      ((f.toEquiv (r := G.Adj) (s := G'.Adj).sumCongr (g.toEquiv (r := H.Adj) (s := H'.Adj)) : (a : V ⊕ W) → V' ⊕ W')
        (Sum.inl val_1)) ↔
    (G ⊕g H).Adj (Sum.inl val) (Sum.inl val_1)

Tactic:
simp [f.map_rel_iff, g.map_rel_iff]

Premises used: RelIso.map_rel_iff
-- 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 v' : V
w w' : W
f : G ≃g G'
g : H ≃g H'
val : V
val_1 : W
⊢ (G' ⊕g H').Adj
      ((f.toEquiv (r := G.Adj) (s := G'.Adj).sumCongr (g.toEquiv (r := H.Adj) (s := H'.Adj)) : (a : V ⊕ W) → V' ⊕ W')
        (Sum.inl val))
      ((f.toEquiv (r := G.Adj) (s := G'.Adj).sumCongr (g.toEquiv (r := H.Adj) (s := H'.Adj)) : (a : V ⊕ W) → V' ⊕ W')
        (Sum.inr val_1)) ↔
    (G ⊕g H).Adj (Sum.inl val) (Sum.inr val_1)

Tactic:
simp [f.map_rel_iff, g.map_rel_iff]

Premises used: RelIso.map_rel_iff
-- 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 v' : V
w w' : W
f : G ≃g G'
g : H ≃g H'
val : W
val_1 : V
⊢ (G' ⊕g H').Adj
      ((f.toEquiv (r := G.Adj) (s := G'.Adj).sumCongr (g.toEquiv (r := H.Adj) (s := H'.Adj)) : (a : V ⊕ W) → V' ⊕ W')
        (Sum.inr val))
      ((f.toEquiv (r := G.Adj) (s := G'.Adj).sumCongr (g.toEquiv (r := H.Adj) (s := H'.Adj)) : (a : V ⊕ W) → V' ⊕ W')
        (Sum.inl val_1)) ↔
    (G ⊕g H).Adj (Sum.inr val) (Sum.inl val_1)

Tactic:
simp [f.map_rel_iff, g.map_rel_iff]

Premises used: RelIso.map_rel_iff
-- 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 v' : V
w w' : W
f : G ≃g G'
g : H ≃g H'
val val_1 : W
⊢ (G' ⊕g H').Adj
      ((f.toEquiv (r := G.Adj) (s := G'.Adj).sumCongr (g.toEquiv (r := H.Adj) (s := H'.Adj)) : (a : V ⊕ W) → V' ⊕ W')
        (Sum.inr val))
      ((f.toEquiv (r := G.Adj) (s := G'.Adj).sumCongr (g.toEquiv (r := H.Adj) (s := H'.Adj)) : (a : V ⊕ W) → V' ⊕ W')
        (Sum.inr val_1)) ↔
    (G ⊕g H).Adj (Sum.inr val) (Sum.inr val_1)

Tactic:
simp [f.map_rel_iff, g.map_rel_iff]

Premises used: RelIso.map_rel_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Sum
Goal:
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'
⊢ (f.sumCongr g).toHom = f.toHom.sum g.toHom

Tactic:
rfl

Premises used: Sum.map, SimpleGraph.Hom.sum, rfl, Sum.elim
-- Module: Mathlib.Combinatorics.SimpleGraph.Sum
Goal:
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'
⊢ (f.sumCongr g).toEmbedding = f.toEmbedding.sum g.toEmbedding

Tactic:
rfl

Premises used: Sum.map, rfl, Sum.elim, SimpleGraph.Embedding.sum
-- Module: Mathlib.Combinatorics.SimpleGraph.Sum
Goal:
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'
h :
  ∀ (v : V),
    Eq (α := W' ⊕ V') ((comp sumComm (f.sumCongr g) : (a : V ⊕ W) → W' ⊕ V') (Sum.inl v) : W' ⊕ V')
      (((g.sumCongr f).comp sumComm : (a : V ⊕ W) → W' ⊕ V') (Sum.inl v) : W' ⊕ V')
h₁ :
  ∀ (w : W),
    Eq (α := W' ⊕ V') ((comp sumComm (f.sumCongr g) : (a : V ⊕ W) → W' ⊕ V') (Sum.inr w) : W' ⊕ V')
      (((g.sumCongr f).comp sumComm : (a : V ⊕ W) → W' ⊕ V') (Sum.inr w) : W' ⊕ V')
⊢ comp sumComm (f.sumCongr g) = (g.sumCongr f).comp sumComm

Tactic:
ext (v | w)
-- Module: Mathlib.Combinatorics.SimpleGraph.Sum
Goal:
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
⊢ Eq (α := W' ⊕ V') ((comp sumComm (f.sumCongr g) : (a : V ⊕ W) → W' ⊕ V') (Sum.inl v) : W' ⊕ V')
    (((g.sumCongr f).comp sumComm : (a : V ⊕ W) → W' ⊕ V') (Sum.inl v) : W' ⊕ V')

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Sum
Goal:
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
⊢ Eq (α := W' ⊕ V') ((comp sumComm (f.sumCongr g) : (a : V ⊕ W) → W' ⊕ V') (Sum.inr w) : W' ⊕ V')
    (((g.sumCongr f).comp sumComm : (a : V ⊕ W) → W' ⊕ V') (Sum.inr w) : W' ⊕ 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
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'
h₁ :
  ∀ (v : V),
    Eq (α := V' ⊕ W' ⊕ U')
      ((comp sumAssoc ((f.sumCongr g).sumCongr h) : (a : (V ⊕ W) ⊕ U) → V' ⊕ W' ⊕ U') (Sum.inl (Sum.inl v)) :
        V' ⊕ W' ⊕ U')
      (((f.sumCongr (g.sumCongr h)).comp sumAssoc : (a : (V ⊕ W) ⊕ U) → V' ⊕ W' ⊕ U') (Sum.inl (Sum.inl v)) :
        V' ⊕ W' ⊕ U')
h₂ :
  ∀ (w : W),
    Eq (α := V' ⊕ W' ⊕ U')
      ((comp sumAssoc ((f.sumCongr g).sumCongr h) : (a : (V ⊕ W) ⊕ U) → V' ⊕ W' ⊕ U') (Sum.inl (Sum.inr w)) :
        V' ⊕ W' ⊕ U')
      (((f.sumCongr (g.sumCongr h)).comp sumAssoc : (a : (V ⊕ W) ⊕ U) → V' ⊕ W' ⊕ U') (Sum.inl (Sum.inr w)) :
        V' ⊕ W' ⊕ U')
h₃ :
  ∀ (u : U),
    Eq (α := V' ⊕ W' ⊕ U')
      ((comp sumAssoc ((f.sumCongr g).sumCongr h) : (a : (V ⊕ W) ⊕ U) → V' ⊕ W' ⊕ U') (Sum.inr u) : V' ⊕ W' ⊕ U')
      (((f.sumCongr (g.sumCongr h)).comp sumAssoc : (a : (V ⊕ W) ⊕ U) → V' ⊕ W' ⊕ U') (Sum.inr u) : V' ⊕ W' ⊕ U')
⊢ comp sumAssoc ((f.sumCongr g).sumCongr h) = (f.sumCongr (g.sumCongr h)).comp sumAssoc

Tactic:
ext ((v | w) | 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
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
⊢ Eq (α := V' ⊕ W' ⊕ U')
    ((comp sumAssoc ((f.sumCongr g).sumCongr h) : (a : (V ⊕ W) ⊕ U) → V' ⊕ W' ⊕ U') (Sum.inl (Sum.inl v)) :
      V' ⊕ W' ⊕ U')
    (((f.sumCongr (g.sumCongr h)).comp sumAssoc : (a : (V ⊕ W) ⊕ U) → V' ⊕ W' ⊕ U') (Sum.inl (Sum.inl v)) :
      V' ⊕ W' ⊕ U')

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
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
⊢ Eq (α := V' ⊕ W' ⊕ U')
    ((comp sumAssoc ((f.sumCongr g).sumCongr h) : (a : (V ⊕ W) ⊕ U) → V' ⊕ W' ⊕ U') (Sum.inl (Sum.inr w)) :
      V' ⊕ W' ⊕ U')
    (((f.sumCongr (g.sumCongr h)).comp sumAssoc : (a : (V ⊕ W) ⊕ U) → V' ⊕ W' ⊕ U') (Sum.inl (Sum.inr w)) :
      V' ⊕ W' ⊕ U')

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
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
⊢ Eq (α := V' ⊕ W' ⊕ U')
    ((comp sumAssoc ((f.sumCongr g).sumCongr h) : (a : (V ⊕ W) ⊕ U) → V' ⊕ W' ⊕ U') (Sum.inr u) : V' ⊕ W' ⊕ U')
    (((f.sumCongr (g.sumCongr h)).comp sumAssoc : (a : (V ⊕ W) ⊕ U) → V' ⊕ W' ⊕ U') (Sum.inr u) : V' ⊕ W' ⊕ U')

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Sum
Goal:
V : Type u_3
W : Type u_5
G : SimpleGraph V
H : SimpleGraph W
v v' : V
w w' : W
hv : G.Reachable v v'
hw : H.Reachable w w'
⊢ ((G ⊕g H) ⊔ edge (Sum.inl v) (Sum.inr w)).Adj ((Embedding.toHom Embedding.sumInl : (a : V) → V ⊕ W) v)
    ((Embedding.toHom Embedding.sumInr : (a : W) → V ⊕ W) w)

Tactic:
simp [edge]

Premises used: SimpleGraph.edge
-- Module: Mathlib.Combinatorics.SimpleGraph.Sum
Goal:
V : Type u_3
W : Type u_5
G : SimpleGraph V
H : SimpleGraph W
v : V
w : W
hG : G.Preconnected
hH : H.Preconnected
v₁ v₂ : V
⊢ ((G ⊕g H) ⊔ edge (Sum.inl v) (Sum.inr w)).Reachable (Sum.inl v₁) (Sum.inl v₂)

Tactic:
((hG v₁ v₂).map Embedding.sumInl.toHom).mono le_sup_left

Premises used: le_sup_left, SimpleGraph.Reachable.map, SimpleGraph.Reachable.mono, SimpleGraph.Embedding.sumInl, SimpleGraph.Embedding.toHom
-- Module: Mathlib.Combinatorics.SimpleGraph.Sum
Goal:
V : Type u_3
W : Type u_5
G : SimpleGraph V
H : SimpleGraph W
v : V
w : W
hG : G.Preconnected
hH : H.Preconnected
v₁ v₂ : V
⊢ ((G ⊕g H) ⊔ edge (Sum.inl v) (Sum.inr w)).Reachable (Sum.inl v₁) (Sum.inl v₂)

Tactic:
exact ((hG v₁ v₂).map Embedding.sumInl.toHom).mono le_sup_left

Premises used: le_sup_left, SimpleGraph.Reachable.map, SimpleGraph.Reachable.mono, SimpleGraph.Embedding.sumInl, SimpleGraph.Embedding.toHom
-- Module: Mathlib.Combinatorics.SimpleGraph.Sum
Goal:
V : Type u_3
W : Type u_5
G : SimpleGraph V
H : SimpleGraph W
v : V
w : W
hG : G.Preconnected
hH : H.Preconnected
v₁ : V
w₂ : W
⊢ ((G ⊕g H) ⊔ edge (Sum.inl v) (Sum.inr w)).Reachable (Sum.inl v₁) (Sum.inr w₂)

Tactic:
(hG ..).sum_sup_edge (hH ..)

Premises used: SimpleGraph.Reachable.sum_sup_edge
-- Module: Mathlib.Combinatorics.SimpleGraph.Sum
Goal:
V : Type u_3
W : Type u_5
G : SimpleGraph V
H : SimpleGraph W
v : V
w : W
hG : G.Preconnected
hH : H.Preconnected
v₁ : V
w₂ : W
⊢ ((G ⊕g H) ⊔ edge (Sum.inl v) (Sum.inr w)).Reachable (Sum.inl v₁) (Sum.inr w₂)

Tactic:
exact (hG ..).sum_sup_edge (hH ..)

Premises used: SimpleGraph.Reachable.sum_sup_edge
-- Module: Mathlib.Combinatorics.SimpleGraph.Sum
Goal:
V : Type u_3
W : Type u_5
G : SimpleGraph V
H : SimpleGraph W
v : V
w : W
hG : G.Preconnected
hH : H.Preconnected
w₁ : W
v₂ : V
⊢ ((G ⊕g H) ⊔ edge (Sum.inl v) (Sum.inr w)).Reachable (Sum.inr w₁) (Sum.inl v₂)

Tactic:
((hG ..).sum_sup_edge (hH ..)).symm

Premises used: SimpleGraph.Reachable.symm, SimpleGraph.Reachable.sum_sup_edge
-- Module: Mathlib.Combinatorics.SimpleGraph.Sum
Goal:
V : Type u_3
W : Type u_5
G : SimpleGraph V
H : SimpleGraph W
v : V
w : W
hG : G.Preconnected
hH : H.Preconnected
w₁ : W
v₂ : V
⊢ ((G ⊕g H) ⊔ edge (Sum.inl v) (Sum.inr w)).Reachable (Sum.inr w₁) (Sum.inl v₂)

Tactic:
exact ((hG ..).sum_sup_edge (hH ..)).symm

Premises used: SimpleGraph.Reachable.symm, SimpleGraph.Reachable.sum_sup_edge
-- Module: Mathlib.Combinatorics.SimpleGraph.Sum
Goal:
V : Type u_3
W : Type u_5
G : SimpleGraph V
H : SimpleGraph W
v : V
w : W
hG : G.Preconnected
hH : H.Preconnected
w₁ w₂ : W
⊢ ((G ⊕g H) ⊔ edge (Sum.inl v) (Sum.inr w)).Reachable (Sum.inr w₁) (Sum.inr w₂)

Tactic:
((hH w₁ w₂).map Embedding.sumInr.toHom).mono le_sup_left

Premises used: le_sup_left, SimpleGraph.Reachable.map, SimpleGraph.Reachable.mono, SimpleGraph.Embedding.sumInr, SimpleGraph.Embedding.toHom
-- Module: Mathlib.Combinatorics.SimpleGraph.Sum
Goal:
V : Type u_3
W : Type u_5
G : SimpleGraph V
H : SimpleGraph W
v : V
w : W
hG : G.Preconnected
hH : H.Preconnected
w₁ w₂ : W
⊢ ((G ⊕g H) ⊔ edge (Sum.inl v) (Sum.inr w)).Reachable (Sum.inr w₁) (Sum.inr w₂)

Tactic:
exact ((hH w₁ w₂).map Embedding.sumInr.toHom).mono le_sup_left

Premises used: le_sup_left, SimpleGraph.Reachable.map, SimpleGraph.Reachable.mono, SimpleGraph.Embedding.sumInr, SimpleGraph.Embedding.toHom
-- Module: Mathlib.Combinatorics.SimpleGraph.Sum
Goal:
V : Type u_3
W : Type u_5
G : SimpleGraph V
H : SimpleGraph W
v : V
w : W
hG : G.Connected
hH : H.Connected
⊢ G.Preconnected

Tactic:
obtain ⟨hG⟩ := hG
-- Module: Mathlib.Combinatorics.SimpleGraph.Sum
Goal:
V : Type u_3
W : Type u_5
G : SimpleGraph V
H : SimpleGraph W
v : V
w : W
hG : G.Connected
hH : H.Connected
hG₁ : G.Preconnected
⊢ Nonempty V

Tactic:
obtain ⟨hG⟩ := hG
-- Module: Mathlib.Combinatorics.SimpleGraph.Sum
Goal:
V : Type u_3
W : Type u_5
G : SimpleGraph V
H : SimpleGraph W
v : V
w : W
hH : H.Connected
hG : G.Preconnected
nonempty : Nonempty V
⊢ ((G ⊕g H) ⊔ edge (Sum.inl v) (Sum.inr w)).Connected

Tactic:
⟨hG.sum_sup_edge hH.preconnected⟩

Premises used: SimpleGraph.Connected.preconnected, SimpleGraph.Connected.mk, SimpleGraph.Preconnected.sum_sup_edge
-- Module: Mathlib.Combinatorics.SimpleGraph.Sum
Goal:
V : Type u_3
W : Type u_5
G : SimpleGraph V
H : SimpleGraph W
v : V
w : W
hH : H.Connected
hG : G.Preconnected
nonempty : Nonempty V
⊢ ((G ⊕g H) ⊔ edge (Sum.inl v) (Sum.inr w)).Connected

Tactic:
exact ⟨hG.sum_sup_edge hH.preconnected⟩
-- 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
cG : G.Coloring γ
cH : H.Coloring γ
u v : V ⊕ W
huv : (G ⊕g H).Adj u v
inl :
  ∀ (val : V) (huv : (G ⊕g H).Adj (Sum.inl val) v),
    (completeGraph γ).Adj (Sum.elim.{u_3, u_5, u_7 + 1} (β := W) (⇑cG : (a : V) → γ) (⇑cH : (a : W) → γ) (Sum.inl val))
      (Sum.elim (⇑cG : (a : V) → γ) (⇑cH : (a : W) → γ) v)
inr :
  ∀ (val : W) (huv : (G ⊕g H).Adj (Sum.inr val) v),
    (completeGraph γ).Adj (Sum.elim.{u_3, u_5, u_7 + 1} (α := V) (⇑cG : (a : V) → γ) (⇑cH : (a : W) → γ) (Sum.inr val))
      (Sum.elim (⇑cG : (a : V) → γ) (⇑cH : (a : W) → γ) v)
⊢ (completeGraph γ).Adj (Sum.elim (⇑cG : (a : V) → γ) (⇑cH : (a : W) → γ) u)
    (Sum.elim (⇑cG : (a : V) → γ) (⇑cH : (a : W) → γ) v)

Tactic:
cases u