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'
v : V ⊕ W
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)
have 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))
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 (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))
⊢ (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)
have 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))
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'
⊢ (f.sum g).comp (Iso.toHom Iso.sumComm) = comp (Iso.toHom Iso.sumComm) (g.sum f)
have 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: 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 : 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')
⊢ (f.sum g).comp (Iso.toHom Iso.sumComm) = comp (Iso.toHom Iso.sumComm) (g.sum f)
have 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: 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'
⊢ (f.sum (g.sum h)).comp (Iso.toHom Iso.sumAssoc) = comp (Iso.toHom Iso.sumAssoc) ((f.sum g).sum h)
have 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')
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')
      (((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')
⊢ (f.sum (g.sum h)).comp (Iso.toHom Iso.sumAssoc) = comp (Iso.toHom Iso.sumAssoc) ((f.sum g).sum h)
have 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')
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')
      (((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')
⊢ (f.sum (g.sum h)).comp (Iso.toHom Iso.sumAssoc) = comp (Iso.toHom Iso.sumAssoc) ((f.sum g).sum h)
have 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')
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
γ : 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
⊢ 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
have 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
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),
    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
⊢ 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
have 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
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
⊢ 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
have 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)
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),
    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)
⊢ 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
have 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
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
⊢ 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
have 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
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),
    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
⊢ 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
have 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)
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'
u v : V ⊕ W
⊢ (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
have inl : ∀ (val : V),
  (G' ⊕g H').Adj
      (({ toFun := Sum.map (⇑f : (a : V) → V') (⇑g : (a : W) → W'), inj' := sorry } : (a : V ⊕ W) → V' ⊕ W') (Sum.inl val))
      (({ toFun := Sum.map (⇑f : (a : V) → V') (⇑g : (a : W) → W'), inj' := sorry } : (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
        (({ 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
⊢ (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
have inr : ∀ (val : W),
  (G' ⊕g H').Adj
      (({ toFun := Sum.map (⇑f : (a : V) → V') (⇑g : (a : W) → W'), inj' := sorry } : (a : V ⊕ W) → V' ⊕ W') (Sum.inr val))
      (({ toFun := Sum.map (⇑f : (a : V) → V') (⇑g : (a : W) → W'), inj' := sorry } : (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
      (({ 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
have inl : ∀ (val_1 : V),
  (G' ⊕g H').Adj
      (({ toFun := Sum.map (⇑f : (a : V) → V') (⇑g : (a : W) → W'), inj' := sorry } : (a : V ⊕ W) → V' ⊕ W') (Sum.inl val))
      (({ toFun := Sum.map (⇑f : (a : V) → V') (⇑g : (a : W) → W'), inj' := sorry } : (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
        (({ 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)
⊢ (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
have inl₁ : ∀ (val_1 : W),
  (G' ⊕g H').Adj
      (({ toFun := Sum.map (⇑f : (a : V) → V') (⇑g : (a : W) → W'), inj' := sorry } : (a : V ⊕ W) → V' ⊕ W') (Sum.inl val))
      (({ toFun := Sum.map (⇑f : (a : V) → V') (⇑g : (a : W) → W'), inj' := sorry } : (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
      (({ 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
have inr : ∀ (val_1 : V),
  (G' ⊕g H').Adj
      (({ toFun := Sum.map (⇑f : (a : V) → V') (⇑g : (a : W) → W'), inj' := sorry } : (a : V ⊕ W) → V' ⊕ W') (Sum.inr val))
      (({ toFun := Sum.map (⇑f : (a : V) → V') (⇑g : (a : W) → W'), inj' := sorry } : (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
        (({ 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)
⊢ (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
have inr₁ : ∀ (val_1 : W),
  (G' ⊕g H').Adj
      (({ toFun := Sum.map (⇑f : (a : V) → V') (⇑g : (a : W) → W'), inj' := sorry } : (a : V ⊕ W) → V' ⊕ W') (Sum.inr val))
      (({ toFun := Sum.map (⇑f : (a : V) → V') (⇑g : (a : W) → W'), inj' := sorry } : (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'
⊢ (g.sum f).comp (Iso.toEmbedding Iso.sumComm) = comp (Iso.toEmbedding Iso.sumComm) (f.sum g)
have 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: 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') (((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')
⊢ (g.sum f).comp (Iso.toEmbedding Iso.sumComm) = comp (Iso.toEmbedding Iso.sumComm) (f.sum g)
have 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: 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'
⊢ (f.sum (g.sum h)).comp (Iso.toEmbedding Iso.sumAssoc) = comp (Iso.toEmbedding Iso.sumAssoc) ((f.sum g).sum h)
have 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')
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')
      (((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')
⊢ (f.sum (g.sum h)).comp (Iso.toEmbedding Iso.sumAssoc) = comp (Iso.toEmbedding Iso.sumAssoc) ((f.sum g).sum h)
have 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')
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')
      (((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')
⊢ (f.sum (g.sum h)).comp (Iso.toEmbedding Iso.sumAssoc) = comp (Iso.toEmbedding Iso.sumAssoc) ((f.sum g).sum h)
have 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')
Tactic: ext ((v | w) | u)