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_1 v' : V
w w' : W
u v : U
⊢ (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.inr v)) ↔
    (G ⊕g H ⊕g I).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
⊢ Eq (α := V ⊕ W) ((fun (u : V) ↦ (Sum.inl u : V ⊕ W)) u) ((fun (u : V) ↦ (Sum.inl u : V ⊕ W)) v) → u = 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 v' : V
w w' : W
⊢ ∀ {a b : V},
    (G ⊕g H).Adj (({ toFun := fun (u : V) ↦ Sum.inl u, inj' := ⋯ } : (a : V) → V ⊕ W) a)
        (({ toFun := fun (u : V) ↦ Sum.inl u, inj' := ⋯ } : (a : V) → V ⊕ W) b) ↔
      G.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 : 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
⊢ Eq (α := V ⊕ W) ((fun (u : W) ↦ (Sum.inr u : V ⊕ W)) u) ((fun (u : W) ↦ (Sum.inr u : V ⊕ W)) v) → u = 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 v' : V
w w' : W
⊢ ∀ {a b : W},
    (G ⊕g H).Adj (({ toFun := fun (u : W) ↦ Sum.inr u, inj' := ⋯ } : (a : W) → V ⊕ W) a)
        (({ toFun := fun (u : W) ↦ Sum.inr u, inj' := ⋯ } : (a : W) → V ⊕ W) b) ↔
      H.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 : 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 (Sum.inl val) v →
      (G' ⊕g H').Adj (Sum.map.{u_3, u_4, u_5, u_6} (β := W) (⇑f : (a : V) → V') (⇑g : (a : W) → W') (Sum.inl val))
        (Sum.map (⇑f : (a : V) → V') (⇑g : (a : W) → W') v)
inr :
  ∀ (val : W),
    (G ⊕g H).Adj (Sum.inr val) v →
      (G' ⊕g H').Adj (Sum.map.{u_3, u_4, u_5, u_6} (α := V) (⇑f : (a : V) → V') (⇑g : (a : W) → W') (Sum.inr val))
        (Sum.map (⇑f : (a : V) → V') (⇑g : (a : W) → W') v)
⊢ (G ⊕g H).Adj u v →
    (G' ⊕g H').Adj (Sum.map (⇑f : (a : V) → V') (⇑g : (a : W) → W') u)
      (Sum.map (⇑f : (a : V) → V') (⇑g : (a : W) → W') 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 (Sum.inl val) (Sum.inl val_1) →
      (G' ⊕g H').Adj (Sum.map.{u_3, u_4, u_5, u_6} (β := W) (⇑f : (a : V) → V') (⇑g : (a : W) → W') (Sum.inl val))
        (Sum.map.{u_3, u_4, u_5, u_6} (β := W) (⇑f : (a : V) → V') (⇑g : (a : W) → W') (Sum.inl val_1))
inl₁ :
  ∀ (val_1 : W),
    (G ⊕g H).Adj (Sum.inl val) (Sum.inr val_1) →
      (G' ⊕g H').Adj (Sum.map.{u_3, u_4, u_5, u_6} (β := W) (⇑f : (a : V) → V') (⇑g : (a : W) → W') (Sum.inl val))
        (Sum.map.{u_3, u_4, u_5, u_6} (α := V) (⇑f : (a : V) → V') (⇑g : (a : W) → W') (Sum.inr val_1))
⊢ (G ⊕g H).Adj (Sum.inl val) v →
    (G' ⊕g H').Adj (Sum.map.{u_3, u_4, u_5, u_6} (β := W) (⇑f : (a : V) → V') (⇑g : (a : W) → W') (Sum.inl val))
      (Sum.map (⇑f : (a : V) → V') (⇑g : (a : W) → W') 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 (Sum.inr val) (Sum.inl val_1) →
      (G' ⊕g H').Adj (Sum.map.{u_3, u_4, u_5, u_6} (α := V) (⇑f : (a : V) → V') (⇑g : (a : W) → W') (Sum.inr val))
        (Sum.map.{u_3, u_4, u_5, u_6} (β := W) (⇑f : (a : V) → V') (⇑g : (a : W) → W') (Sum.inl val_1))
inr₁ :
  ∀ (val_1 : W),
    (G ⊕g H).Adj (Sum.inr val) (Sum.inr val_1) →
      (G' ⊕g H').Adj (Sum.map.{u_3, u_4, u_5, u_6} (α := V) (⇑f : (a : V) → V') (⇑g : (a : W) → W') (Sum.inr val))
        (Sum.map.{u_3, u_4, u_5, u_6} (α := V) (⇑f : (a : V) → V') (⇑g : (a : W) → W') (Sum.inr val_1))
⊢ (G ⊕g H).Adj (Sum.inr val) v →
    (G' ⊕g H').Adj (Sum.map.{u_3, u_4, u_5, u_6} (α := V) (⇑f : (a : V) → V') (⇑g : (a : W) → W') (Sum.inr val))
      (Sum.map (⇑f : (a : V) → V') (⇑g : (a : W) → W') 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 (Sum.inl val) (Sum.inl val_1) →
    (G' ⊕g H').Adj (Sum.map.{u_3, u_4, u_5, u_6} (β := W) (⇑f : (a : V) → V') (⇑g : (a : W) → W') (Sum.inl val))
      (Sum.map.{u_3, u_4, u_5, u_6} (β := W) (⇑f : (a : V) → V') (⇑g : (a : W) → W') (Sum.inl val_1))

Tactic:
simp_all [f.map_rel, g.map_rel]

Premises used: RelHom.map_rel
-- 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 (Sum.inl val) (Sum.inr val_1) →
    (G' ⊕g H').Adj (Sum.map.{u_3, u_4, u_5, u_6} (β := W) (⇑f : (a : V) → V') (⇑g : (a : W) → W') (Sum.inl val))
      (Sum.map.{u_3, u_4, u_5, u_6} (α := V) (⇑f : (a : V) → V') (⇑g : (a : W) → W') (Sum.inr val_1))

Tactic:
simp_all [f.map_rel, g.map_rel]

Premises used: RelHom.map_rel
-- 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 (Sum.inr val) (Sum.inl val_1) →
    (G' ⊕g H').Adj (Sum.map.{u_3, u_4, u_5, u_6} (α := V) (⇑f : (a : V) → V') (⇑g : (a : W) → W') (Sum.inr val))
      (Sum.map.{u_3, u_4, u_5, u_6} (β := W) (⇑f : (a : V) → V') (⇑g : (a : W) → W') (Sum.inl val_1))

Tactic:
simp_all [f.map_rel, g.map_rel]

Premises used: RelHom.map_rel
-- 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 (Sum.inr val) (Sum.inr val_1) →
    (G' ⊕g H').Adj (Sum.map.{u_3, u_4, u_5, u_6} (α := V) (⇑f : (a : V) → V') (⇑g : (a : W) → W') (Sum.inr val))
      (Sum.map.{u_3, u_4, u_5, u_6} (α := V) (⇑f : (a : V) → V') (⇑g : (a : W) → W') (Sum.inr val_1))

Tactic:
simp_all [f.map_rel, g.map_rel]

Premises used: RelHom.map_rel
-- 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 : W),
    Eq (α := V' ⊕ W') (((f.sum g).comp (Iso.toHom Iso.sumComm) : (a : W ⊕ V) → V' ⊕ W') (Sum.inl v) : V' ⊕ W')
      ((comp (Iso.toHom Iso.sumComm) (g.sum f) : (a : W ⊕ V) → V' ⊕ W') (Sum.inl v) : V' ⊕ W')
h₁ :
  ∀ (w : V),
    Eq (α := V' ⊕ W') (((f.sum g).comp (Iso.toHom Iso.sumComm) : (a : W ⊕ V) → V' ⊕ W') (Sum.inr w) : V' ⊕ W')
      ((comp (Iso.toHom Iso.sumComm) (g.sum f) : (a : W ⊕ V) → V' ⊕ W') (Sum.inr w) : V' ⊕ W')
⊢ (f.sum g).comp (Iso.toHom Iso.sumComm) = comp (Iso.toHom Iso.sumComm) (g.sum f)

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 : W
⊢ Eq (α := V' ⊕ W') (((f.sum g).comp (Iso.toHom Iso.sumComm) : (a : W ⊕ V) → V' ⊕ W') (Sum.inl v) : V' ⊕ W')
    ((comp (Iso.toHom Iso.sumComm) (g.sum f) : (a : W ⊕ V) → V' ⊕ W') (Sum.inl v) : V' ⊕ W')

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

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.toHom Iso.sumAssoc) : (a : (V ⊕ W) ⊕ U) → V' ⊕ W' ⊕ U') (Sum.inl (Sum.inl v)) :
        V' ⊕ W' ⊕ U')
      ((comp (Iso.toHom 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.toHom Iso.sumAssoc) : (a : (V ⊕ W) ⊕ U) → V' ⊕ W' ⊕ U') (Sum.inl (Sum.inr w)) :
        V' ⊕ W' ⊕ U')
      ((comp (Iso.toHom 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.toHom Iso.sumAssoc) : (a : (V ⊕ W) ⊕ U) → V' ⊕ W' ⊕ U') (Sum.inr u) : V' ⊕ W' ⊕ U')
      ((comp (Iso.toHom 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.toHom Iso.sumAssoc) = comp (Iso.toHom 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.toHom Iso.sumAssoc) : (a : (V ⊕ W) ⊕ U) → V' ⊕ W' ⊕ U') (Sum.inl (Sum.inl v)) :
      V' ⊕ W' ⊕ U')
    ((comp (Iso.toHom 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.toHom Iso.sumAssoc) : (a : (V ⊕ W) ⊕ U) → V' ⊕ W' ⊕ U') (Sum.inl (Sum.inr w)) :
      V' ⊕ W' ⊕ U')
    ((comp (Iso.toHom 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.toHom Iso.sumAssoc) : (a : (V ⊕ W) ⊕ U) → V' ⊕ W' ⊕ U') (Sum.inr u) : V' ⊕ W' ⊕ U')
    ((comp (Iso.toHom 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),
    Eq (α := V' ⊕ W') (Sum.map.{u_3, u_4, u_5, u_6} (β := W) (⇑f : (a : V) → V') (⇑g : (a : W) → W') (Sum.inl val))
        (Sum.map (⇑f : (a : V) → V') (⇑g : (a : W) → W') v) →
      Sum.inl val = v
inr :
  ∀ (val : W),
    Eq (α := V' ⊕ W') (Sum.map.{u_3, u_4, u_5, u_6} (α := V) (⇑f : (a : V) → V') (⇑g : (a : W) → W') (Sum.inr val))
        (Sum.map (⇑f : (a : V) → V') (⇑g : (a : W) → W') v) →
      Sum.inr val = v
⊢ Eq (α := V' ⊕ W') (Sum.map (⇑f : (a : V) → V') (⇑g : (a : W) → W') u)
      (Sum.map (⇑f : (a : V) → V') (⇑g : (a : W) → W') v) →
    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),
    Eq (α := V' ⊕ W') (Sum.map.{u_3, u_4, u_5, u_6} (β := W) (⇑f : (a : V) → V') (⇑g : (a : W) → W') (Sum.inl val))
        (Sum.map.{u_3, u_4, u_5, u_6} (β := W) (⇑f : (a : V) → V') (⇑g : (a : W) → W') (Sum.inl val_1)) →
      Eq (α := V ⊕ W) (Sum.inl val) (Sum.inl val_1)
inl₁ :
  ∀ (val_1 : W),
    Eq (α := V' ⊕ W') (Sum.map.{u_3, u_4, u_5, u_6} (β := W) (⇑f : (a : V) → V') (⇑g : (a : W) → W') (Sum.inl val))
        (Sum.map.{u_3, u_4, u_5, u_6} (α := V) (⇑f : (a : V) → V') (⇑g : (a : W) → W') (Sum.inr val_1)) →
      Sum.inl val = Sum.inr val_1
⊢ Eq (α := V' ⊕ W') (Sum.map.{u_3, u_4, u_5, u_6} (β := W) (⇑f : (a : V) → V') (⇑g : (a : W) → W') (Sum.inl val))
      (Sum.map (⇑f : (a : V) → V') (⇑g : (a : W) → W') v) →
    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),
    Eq (α := V' ⊕ W') (Sum.map.{u_3, u_4, u_5, u_6} (α := V) (⇑f : (a : V) → V') (⇑g : (a : W) → W') (Sum.inr val))
        (Sum.map.{u_3, u_4, u_5, u_6} (β := W) (⇑f : (a : V) → V') (⇑g : (a : W) → W') (Sum.inl val_1)) →
      Sum.inr val = Sum.inl val_1
inr₁ :
  ∀ (val_1 : W),
    Eq (α := V' ⊕ W') (Sum.map.{u_3, u_4, u_5, u_6} (α := V) (⇑f : (a : V) → V') (⇑g : (a : W) → W') (Sum.inr val))
        (Sum.map.{u_3, u_4, u_5, u_6} (α := V) (⇑f : (a : V) → V') (⇑g : (a : W) → W') (Sum.inr val_1)) →
      Eq (α := V ⊕ W) (Sum.inr val) (Sum.inr val_1)
⊢ Eq (α := V' ⊕ W') (Sum.map.{u_3, u_4, u_5, u_6} (α := V) (⇑f : (a : V) → V') (⇑g : (a : W) → W') (Sum.inr val))
      (Sum.map (⇑f : (a : V) → V') (⇑g : (a : W) → W') v) →
    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
⊢ Eq (α := V' ⊕ W') (Sum.map.{u_3, u_4, u_5, u_6} (β := W) (⇑f : (a : V) → V') (⇑g : (a : W) → W') (Sum.inl val))
      (Sum.map.{u_3, u_4, u_5, u_6} (β := W) (⇑f : (a : V) → V') (⇑g : (a : W) → W') (Sum.inl val_1)) →
    Eq (α := V ⊕ W) (Sum.inl val) (Sum.inl val_1)

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 v' : V
w w' : W
f : G ↪g G'
g : H ↪g H'
val : V
val_1 : W
⊢ Eq (α := V' ⊕ W') (Sum.map.{u_3, u_4, u_5, u_6} (β := W) (⇑f : (a : V) → V') (⇑g : (a : W) → W') (Sum.inl val))
      (Sum.map.{u_3, u_4, u_5, u_6} (α := V) (⇑f : (a : V) → V') (⇑g : (a : W) → W') (Sum.inr val_1)) →
    Sum.inl val = Sum.inr val_1

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 v' : V
w w' : W
f : G ↪g G'
g : H ↪g H'
val : W
val_1 : V
⊢ Eq (α := V' ⊕ W') (Sum.map.{u_3, u_4, u_5, u_6} (α := V) (⇑f : (a : V) → V') (⇑g : (a : W) → W') (Sum.inr val))
      (Sum.map.{u_3, u_4, u_5, u_6} (β := W) (⇑f : (a : V) → V') (⇑g : (a : W) → W') (Sum.inl val_1)) →
    Sum.inr val = Sum.inl val_1

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 v' : V
w w' : W
f : G ↪g G'
g : H ↪g H'
val val_1 : W
⊢ Eq (α := V' ⊕ W') (Sum.map.{u_3, u_4, u_5, u_6} (α := V) (⇑f : (a : V) → V') (⇑g : (a : W) → W') (Sum.inr val))
      (Sum.map.{u_3, u_4, u_5, u_6} (α := V) (⇑f : (a : V) → V') (⇑g : (a : W) → W') (Sum.inr val_1)) →
    Eq (α := V ⊕ W) (Sum.inr val) (Sum.inr val_1)

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
        (({ toFun := Sum.map (⇑f : (a : V) → V') (⇑g : (a : W) → W'), inj' := ⋯ } : (a : V ⊕ W) → V' ⊕ W')
          (Sum.inl val))
        (({ toFun := Sum.map (⇑f : (a : V) → V') (⇑g : (a : W) → W'), inj' := ⋯ } : (a : V ⊕ W) → V' ⊕ W') v) ↔
      (G ⊕g H).Adj (Sum.inl val) v
inr :
  ∀ (val : 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') v) ↔
      (G ⊕g H).Adj (Sum.inr val) v
⊢ (G' ⊕g H').Adj (({ toFun := Sum.map (⇑f : (a : V) → V') (⇑g : (a : W) → W'), inj' := ⋯ } : (a : V ⊕ W) → V' ⊕ W') u)
      (({ toFun := Sum.map (⇑f : (a : V) → V') (⇑g : (a : W) → W'), inj' := ⋯ } : (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
        (({ toFun := Sum.map (⇑f : (a : V) → V') (⇑g : (a : W) → W'), inj' := ⋯ } : (a : V ⊕ W) → V' ⊕ W')
          (Sum.inl val))
        (({ toFun := Sum.map (⇑f : (a : V) → V') (⇑g : (a : W) → W'), inj' := ⋯ } : (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
        (({ toFun := Sum.map (⇑f : (a : V) → V') (⇑g : (a : W) → W'), inj' := ⋯ } : (a : V ⊕ W) → V' ⊕ W')
          (Sum.inl 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.inl val) (Sum.inr val_1)
⊢ (G' ⊕g H').Adj
      (({ toFun := Sum.map (⇑f : (a : V) → V') (⇑g : (a : W) → W'), inj' := ⋯ } : (a : V ⊕ W) → V' ⊕ W') (Sum.inl val))
      (({ toFun := Sum.map (⇑f : (a : V) → V') (⇑g : (a : W) → W'), inj' := ⋯ } : (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
        (({ 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.inl val_1)) ↔
      (G ⊕g H).Adj (Sum.inr val) (Sum.inl val_1)
inr₁ :
  ∀ (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)
⊢ (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') 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
      (({ toFun := Sum.map (⇑f : (a : V) → V') (⇑g : (a : W) → W'), inj' := ⋯ } : (a : V ⊕ W) → V' ⊕ W') (Sum.inl val))
      (({ toFun := Sum.map (⇑f : (a : V) → V') (⇑g : (a : W) → W'), inj' := ⋯ } : (a : V ⊕ W) → V' ⊕ W')
        (Sum.inl val_1)) ↔
    (G ⊕g H).Adj (Sum.inl val) (Sum.inl val_1)

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 v' : V
w w' : W
f : G ↪g G'
g : H ↪g H'
val : V
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.inl 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.inl val) (Sum.inr val_1)

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 v' : V
w w' : W
f : G ↪g G'
g : H ↪g H'
val : W
val_1 : V
⊢ (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.inl val_1)) ↔
    (G ⊕g H).Adj (Sum.inr val) (Sum.inl val_1)

Tactic:
simp