awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Sum (goal)
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
⊢ (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
have 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
Tactic: cases u
Cleared hypotheses: u
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Sum (goal)
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
⊢ (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
have 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
Tactic: cases u
Cleared hypotheses: u
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Sum (goal)
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
⊢ (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
have 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)
Tactic: cases v
Cleared hypotheses: v
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Sum (goal)
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)
⊢ (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
have 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)
Tactic: cases v
Cleared hypotheses: v
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Sum (goal)
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
⊢ (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
have 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)
Tactic: cases v
Cleared hypotheses: v
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Sum (goal)
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)
⊢ (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
have 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)
Tactic: cases v
Cleared hypotheses: v
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Sum (goal)
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'
⊢ comp sumComm (f.sumCongr g) = (g.sumCongr f).comp sumComm
have 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: ext (v | w)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Sum (goal)
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')
⊢ comp sumComm (f.sumCongr g) = (g.sumCongr f).comp sumComm
have 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: ext (v | w)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Sum (goal)
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'
⊢ comp sumAssoc ((f.sumCongr g).sumCongr h) = (f.sumCongr (g.sumCongr h)).comp sumAssoc
have 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')
Tactic: ext ((v | w) | u)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Sum (goal)
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')
⊢ comp sumAssoc ((f.sumCongr g).sumCongr h) = (f.sumCongr (g.sumCongr h)).comp sumAssoc
have 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')
Tactic: ext ((v | w) | u)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Sum (goal)
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')
⊢ comp sumAssoc ((f.sumCongr g).sumCongr h) = (f.sumCongr (g.sumCongr h)).comp sumAssoc
have 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')
Tactic: ext ((v | w) | u)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Sum (hypothesis)
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 ⊕g H) ⊔ edge (Sum.inl v) (Sum.inr w)).Connected
have hG₁ : G.Preconnected
Tactic: obtain ⟨hG⟩ := hG
Cleared hypotheses: hG
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Sum (hypothesis)
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
⊢ ((G ⊕g H) ⊔ edge (Sum.inl v) (Sum.inr w)).Connected
have nonempty : Nonempty V
Tactic: obtain ⟨hG⟩ := hG
Cleared hypotheses: hG
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Sum (goal)
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
⊢ (completeGraph γ).Adj (Sum.elim (⇑cG : (a : V) → γ) (⇑cH : (a : W) → γ) u)
    (Sum.elim (⇑cG : (a : V) → γ) (⇑cH : (a : W) → γ) v)
have 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)
Tactic: cases u
Cleared hypotheses: u, huv
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Sum (goal)
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)
⊢ (completeGraph γ).Adj (Sum.elim (⇑cG : (a : V) → γ) (⇑cH : (a : W) → γ) u)
    (Sum.elim (⇑cG : (a : V) → γ) (⇑cH : (a : W) → γ) v)
have 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)
Tactic: cases u
Cleared hypotheses: u, huv
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Sum (goal)
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 γ
v : V ⊕ W
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)
have inl : ∀ (val_1 : V) (huv : (G ⊕g H).Adj (Sum.inl val) (Sum.inl val_1)),
  (completeGraph γ).Adj (Sum.elim.{u_3, u_5, u_7 + 1} (β := W) (⇑cG : (a : V) → γ) (⇑cH : (a : W) → γ) (Sum.inl val))
    (Sum.elim.{u_3, u_5, u_7 + 1} (β := W) (⇑cG : (a : V) → γ) (⇑cH : (a : W) → γ) (Sum.inl val_1))
Tactic: cases v
Cleared hypotheses: v, huv
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Sum (goal)
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 γ
v : V ⊕ W
val : V
huv : (G ⊕g H).Adj (Sum.inl val) v
inl :
  ∀ (val_1 : V) (huv : (G ⊕g H).Adj (Sum.inl val) (Sum.inl val_1)),
    (completeGraph γ).Adj (Sum.elim.{u_3, u_5, u_7 + 1} (β := W) (⇑cG : (a : V) → γ) (⇑cH : (a : W) → γ) (Sum.inl val))
      (Sum.elim.{u_3, u_5, u_7 + 1} (β := W) (⇑cG : (a : V) → γ) (⇑cH : (a : W) → γ) (Sum.inl val_1))
⊢ (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)
have inl₁ : ∀ (val_1 : W) (huv : (G ⊕g H).Adj (Sum.inl val) (Sum.inr val_1)),
  (completeGraph γ).Adj (Sum.elim.{u_3, u_5, u_7 + 1} (β := W) (⇑cG : (a : V) → γ) (⇑cH : (a : W) → γ) (Sum.inl val))
    (Sum.elim.{u_3, u_5, u_7 + 1} (α := V) (⇑cG : (a : V) → γ) (⇑cH : (a : W) → γ) (Sum.inr val_1))
Tactic: cases v
Cleared hypotheses: v, huv
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Sum (goal)
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 γ
v : V ⊕ W
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)
have inr : ∀ (val_1 : V) (huv : (G ⊕g H).Adj (Sum.inr val) (Sum.inl val_1)),
  (completeGraph γ).Adj (Sum.elim.{u_3, u_5, u_7 + 1} (α := V) (⇑cG : (a : V) → γ) (⇑cH : (a : W) → γ) (Sum.inr val))
    (Sum.elim.{u_3, u_5, u_7 + 1} (β := W) (⇑cG : (a : V) → γ) (⇑cH : (a : W) → γ) (Sum.inl val_1))
Tactic: cases v
Cleared hypotheses: v, huv
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Sum (goal)
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 γ
v : V ⊕ W
val : W
huv : (G ⊕g H).Adj (Sum.inr val) v
inr :
  ∀ (val_1 : V) (huv : (G ⊕g H).Adj (Sum.inr val) (Sum.inl val_1)),
    (completeGraph γ).Adj (Sum.elim.{u_3, u_5, u_7 + 1} (α := V) (⇑cG : (a : V) → γ) (⇑cH : (a : W) → γ) (Sum.inr val))
      (Sum.elim.{u_3, u_5, u_7 + 1} (β := W) (⇑cG : (a : V) → γ) (⇑cH : (a : W) → γ) (Sum.inl val_1))
⊢ (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)
have inr₁ : ∀ (val_1 : W) (huv : (G ⊕g H).Adj (Sum.inr val) (Sum.inr val_1)),
  (completeGraph γ).Adj (Sum.elim.{u_3, u_5, u_7 + 1} (α := V) (⇑cG : (a : V) → γ) (⇑cH : (a : W) → γ) (Sum.inr val))
    (Sum.elim.{u_3, u_5, u_7 + 1} (α := V) (⇑cG : (a : V) → γ) (⇑cH : (a : W) → γ) (Sum.inr val_1))
Tactic: cases v
Cleared hypotheses: v, huv
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Sum (goal)
Goal:
V : Type u_3
W : Type u_5
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
c : (G ⊕g H).Coloring γ
⊢ c.sumLeft.sum c.sumRight = c
have h : ∀ (u : V),
  Eq.{u_7 + 1} (α := γ) ((c.sumLeft.sum c.sumRight : (a : V ⊕ W) → γ) (Sum.inl u) : γ)
    ((c : (a : V ⊕ W) → γ) (Sum.inl u) : γ)
Tactic: ext (u | u)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Sum (goal)
Goal:
V : Type u_3
W : Type u_5
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
c : (G ⊕g H).Coloring γ
h :
  ∀ (u : V),
    Eq.{u_7 + 1} (α := γ) ((c.sumLeft.sum c.sumRight : (a : V ⊕ W) → γ) (Sum.inl u) : γ)
      ((c : (a : V ⊕ W) → γ) (Sum.inl u) : γ)
⊢ c.sumLeft.sum c.sumRight = c
have h₁ : ∀ (u : W),
  Eq.{u_7 + 1} (α := γ) ((c.sumLeft.sum c.sumRight : (a : V ⊕ W) → γ) (Sum.inr u) : γ)
    ((c : (a : V ⊕ W) → γ) (Sum.inr u) : γ)
Tactic: ext (u | u)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Sum (goal)
Goal:
V : Type u_3
W : Type u_5
G : SimpleGraph V
H : SimpleGraph W
n : ℕ
h : G.Colorable n ∧ H.Colorable n
cG : G.Colorable n
cH : H.Colorable n
⊢ (G ⊕g H).Colorable n
have rw : (G ⊕g H).Colorable (max n n)
Tactic: rw [← n.max_self]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Sum (goal)
Goal:
V : Type u_3
W : Type u_5
G : SimpleGraph V
H : SimpleGraph W
⊢ (G ⊕g H).chromaticNumber = max G.chromaticNumber H.chromaticNumber
have refine : ∀ {d : ℕ∞} (hG : G.chromaticNumber ≤ d) (hH : H.chromaticNumber ≤ d), (G ⊕g H).chromaticNumber ≤ d
Tactic: refine eq_max chromaticNumber_le_sum_left chromaticNumber_le_sum_right fun {d} hG hH => ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Sum (goal)
Goal:
V : Type u_3
W : Type u_5
G : SimpleGraph V
H : SimpleGraph W
d : ℕ∞
hG : G.chromaticNumber ≤ d
hH : H.chromaticNumber ≤ d
⊢ (G ⊕g H).chromaticNumber ≤ d
have top : ∀ (hG : G.chromaticNumber ≤ ⊤) (hH : H.chromaticNumber ≤ ⊤), (G ⊕g H).chromaticNumber ≤ ⊤
Tactic: cases d with
  | top => simp
  | coe n =>
    let cG : G.Coloring (Fin n) := (chromaticNumber_le_iff_colorable.mp hG).some
    let cH : H.Coloring (Fin n) := (chromaticNumber_le_iff_colorable.mp hH).some
    exact chromaticNumber_le_iff_colorable.mpr (Nonempty.intro (cG.sum cH))
Cleared hypotheses: d, hG, hH
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Sum (goal)
Goal:
V : Type u_3
W : Type u_5
G : SimpleGraph V
H : SimpleGraph W
d : ℕ∞
hG : G.chromaticNumber ≤ d
hH : H.chromaticNumber ≤ d
top : ∀ (hG : G.chromaticNumber ≤ ⊤) (hH : H.chromaticNumber ≤ ⊤), (G ⊕g H).chromaticNumber ≤ ⊤
⊢ (G ⊕g H).chromaticNumber ≤ d
have coe : ∀ (n : ℕ) (hG : G.chromaticNumber ≤ (↑n : ℕ∞)) (hH : H.chromaticNumber ≤ (↑n : ℕ∞)),
  (G ⊕g H).chromaticNumber ≤ (↑n : ℕ∞)
Tactic: cases d with
  | top => simp
  | coe n =>
    let cG : G.Coloring (Fin n) := (chromaticNumber_le_iff_colorable.mp hG).some
    let cH : H.Coloring (Fin n) := (chromaticNumber_le_iff_colorable.mp hH).some
    exact chromaticNumber_le_iff_colorable.mpr (Nonempty.intro (cG.sum cH))
Cleared hypotheses: d, hG, hH
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Sum (goal)
Goal:
V : Type u_3
W : Type u_5
G : SimpleGraph V
H : SimpleGraph W
v : V
⊢ (G ⊕g H).neighborSet (Sum.inl v) = Sum.inl '' G.neighborSet v
have h : ∀ (v' : V),
  Sum.inl v' ∈ (G ⊕g H).neighborSet (Sum.inl v) ↔
    Membership.mem (γ := Set (V ⊕ W)) (Sum.inl '' G.neighborSet v) (Sum.inl v')
Tactic: ext (v' | w')
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Sum (goal)
Goal:
V : Type u_3
W : Type u_5
G : SimpleGraph V
H : SimpleGraph W
v : V
h :
  ∀ (v' : V),
    Sum.inl v' ∈ (G ⊕g H).neighborSet (Sum.inl v) ↔
      Membership.mem (γ := Set (V ⊕ W)) (Sum.inl '' G.neighborSet v) (Sum.inl v')
⊢ (G ⊕g H).neighborSet (Sum.inl v) = Sum.inl '' G.neighborSet v
have h₁ : ∀ (w' : W),
  Sum.inr w' ∈ (G ⊕g H).neighborSet (Sum.inl v) ↔
    Membership.mem (γ := Set (V ⊕ W)) (Sum.inl '' G.neighborSet v) (Sum.inr w')
Tactic: ext (v' | w')
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Sum (goal)
Goal:
V : Type u_3
W : Type u_5
G : SimpleGraph V
H : SimpleGraph W
w : W
⊢ (G ⊕g H).neighborSet (Sum.inr w) = Sum.inr '' H.neighborSet w
have h : ∀ (v' : V),
  Sum.inl v' ∈ (G ⊕g H).neighborSet (Sum.inr w) ↔
    Membership.mem (γ := Set (V ⊕ W)) (Sum.inr '' H.neighborSet w) (Sum.inl v')
Tactic: ext (v' | w')
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Sum (goal)
Goal:
V : Type u_3
W : Type u_5
G : SimpleGraph V
H : SimpleGraph W
w : W
h :
  ∀ (v' : V),
    Sum.inl v' ∈ (G ⊕g H).neighborSet (Sum.inr w) ↔
      Membership.mem (γ := Set (V ⊕ W)) (Sum.inr '' H.neighborSet w) (Sum.inl v')
⊢ (G ⊕g H).neighborSet (Sum.inr w) = Sum.inr '' H.neighborSet w
have h₁ : ∀ (w' : W),
  Sum.inr w' ∈ (G ⊕g H).neighborSet (Sum.inr w) ↔
    Membership.mem (γ := Set (V ⊕ W)) (Sum.inr '' H.neighborSet w) (Sum.inr w')
Tactic: ext (v' | w')
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Sum (goal)
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
inst : DecidableEq V
inst_1 : DecidableEq W
inst_2 : G.LocallyFinite
inst_3 : H.LocallyFinite
v : V
⊢ Fintype (↑((G ⊕g H).neighborSet (Sum.inl v)) : Type (max u_5 u_3))
have inl : Fintype (↑(Sum.inl '' G.neighborSet v) : Type (max u_5 u_3))
Tactic: simp only [neighborSet_sum_inl, neighborSet_sum_inr]