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
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))
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))
⊢ (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 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
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))
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))
⊢ (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 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
cG : G.Coloring γ
cH : H.Coloring γ
val 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:
simp_all [cG.valid, cH.valid]

Premises used: SimpleGraph.Coloring.valid
-- 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
cG : G.Coloring γ
cH : H.Coloring γ
val : V
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:
simp_all [cG.valid, cH.valid]

Premises used: SimpleGraph.Coloring.valid
-- 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
cG : G.Coloring γ
cH : H.Coloring γ
val : W
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:
simp_all [cG.valid, cH.valid]

Premises used: SimpleGraph.Coloring.valid
-- 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
cG : G.Coloring γ
cH : H.Coloring γ
val 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:
simp_all [cG.valid, cH.valid]

Premises used: SimpleGraph.Coloring.valid
-- Module: Mathlib.Combinatorics.SimpleGraph.Sum
Goal:
V : Type u_3
W : Type u_5
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
cG : G.Coloring γ
cH : H.Coloring γ
⊢ (cG.sum cH).sumLeft = cG

Tactic:
rfl

Premises used: SimpleGraph.Coloring.sumLeft, RelHom.comp, rfl, Sum.elim
-- Module: Mathlib.Combinatorics.SimpleGraph.Sum
Goal:
V : Type u_3
W : Type u_5
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
cG : G.Coloring γ
cH : H.Coloring γ
⊢ (cG.sum cH).sumRight = cH

Tactic:
rfl

Premises used: SimpleGraph.Coloring.sumRight, RelHom.comp, rfl, Sum.elim
-- Module: Mathlib.Combinatorics.SimpleGraph.Sum
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) : γ)
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) : γ)
⊢ c.sumLeft.sum c.sumRight = c

Tactic:
ext (u | u)
-- Module: Mathlib.Combinatorics.SimpleGraph.Sum
Goal:
V : Type u_3
W : Type u_5
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
c : (G ⊕g H).Coloring γ
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:
rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Sum
Goal:
V : Type u_3
W : Type u_5
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
c : (G ⊕g H).Coloring γ
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:
rfl
-- 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
c : (G ⊕g H).Coloring γ
⊢ (fun (p : G.Coloring γ × H.Coloring γ) ↦ p.1.sum p.2) ((fun (c : (G ⊕g H).Coloring γ) ↦ (c.sumLeft, c.sumRight)) c) =
    c

Tactic:
simp [sum_sumLeft_sumRight c]

Premises used: SimpleGraph.Coloring.sum_sumLeft_sumRight
-- Module: Mathlib.Combinatorics.SimpleGraph.Sum
Goal:
V : Type u_3
W : Type u_5
G : SimpleGraph V
H : SimpleGraph W
n m : ℕ
hG : G.Colorable n
hH : H.Colorable m
⊢ (G ⊕g H).Colorable (max n m)

Tactic:
Nonempty.intro (hG.some.sumFin hH.some)

Premises used: Nonempty.some, Nonempty.intro, SimpleGraph.Colorable, SimpleGraph.Coloring.sumFin
-- Module: Mathlib.Combinatorics.SimpleGraph.Sum
Goal:
V : Type u_3
W : Type u_5
G : SimpleGraph V
H : SimpleGraph W
n : ℕ
h : (G ⊕g H).Colorable n
⊢ G.Colorable n

Tactic:
Nonempty.intro (h.some.sumLeft)

Premises used: Nonempty.some, Nonempty.intro, SimpleGraph.Coloring.sumLeft, SimpleGraph.Colorable
-- Module: Mathlib.Combinatorics.SimpleGraph.Sum
Goal:
V : Type u_3
W : Type u_5
G : SimpleGraph V
H : SimpleGraph W
n : ℕ
h : (G ⊕g H).Colorable n
⊢ H.Colorable n

Tactic:
Nonempty.intro (h.some.sumRight)

Premises used: Nonempty.some, Nonempty.intro, SimpleGraph.Coloring.sumRight, SimpleGraph.Colorable
-- Module: Mathlib.Combinatorics.SimpleGraph.Sum
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
rw : (G ⊕g H).Colorable (max n n)
⊢ (G ⊕g H).Colorable n

Tactic:
rw [← n.max_self]

Premises used: Nat.max_self
-- Module: Mathlib.Combinatorics.SimpleGraph.Sum
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 (max n n)

Tactic:
cG.sum_max cH

Premises used: SimpleGraph.Colorable.sum_max
-- Module: Mathlib.Combinatorics.SimpleGraph.Sum
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 (max n n)

Tactic:
exact cG.sum_max cH

Premises used: SimpleGraph.Colorable.sum_max
-- Module: Mathlib.Combinatorics.SimpleGraph.Sum
Goal:
V : Type u_3
W : Type u_5
G : SimpleGraph V
H : SimpleGraph W
⊢ G.chromaticNumber ≤ (G ⊕g H).chromaticNumber

Tactic:
chromaticNumber_le_of_forall_imp (fun _ h ↦ h.of_sum_left)

Premises used: SimpleGraph.chromaticNumber_le_of_forall_imp, SimpleGraph.Colorable.of_sum_left
-- Module: Mathlib.Combinatorics.SimpleGraph.Sum
Goal:
V : Type u_3
W : Type u_5
G : SimpleGraph V
H : SimpleGraph W
⊢ H.chromaticNumber ≤ (G ⊕g H).chromaticNumber

Tactic:
chromaticNumber_le_of_forall_imp (fun _ h ↦ h.of_sum_right)

Premises used: SimpleGraph.Colorable.of_sum_right, SimpleGraph.chromaticNumber_le_of_forall_imp
-- Module: Mathlib.Combinatorics.SimpleGraph.Sum
Goal:
V : Type u_3
W : Type u_5
G : SimpleGraph V
H : SimpleGraph W
⊢ (G ⊕g H).chromaticNumber = max G.chromaticNumber H.chromaticNumber

Tactic:
eq_max chromaticNumber_le_sum_left chromaticNumber_le_sum_right fun {d} hG hH => ?_

Premises used: eq_max, SimpleGraph.chromaticNumber_le_sum_right, SimpleGraph.chromaticNumber_le_sum_left
-- Module: Mathlib.Combinatorics.SimpleGraph.Sum
Goal:
V : Type u_3
W : Type u_5
G : SimpleGraph V
H : SimpleGraph W
refine : ∀ {d : ℕ∞} (hG : G.chromaticNumber ≤ d) (hH : H.chromaticNumber ≤ d), (G ⊕g H).chromaticNumber ≤ d
⊢ (G ⊕g H).chromaticNumber = max G.chromaticNumber H.chromaticNumber

Tactic:
refine eq_max chromaticNumber_le_sum_left chromaticNumber_le_sum_right fun {d} hG hH => ?_

Premises used: eq_max, SimpleGraph.chromaticNumber_le_sum_right, SimpleGraph.chromaticNumber_le_sum_left
-- Module: Mathlib.Combinatorics.SimpleGraph.Sum
Goal:
V : Type u_3
W : Type u_5
G : SimpleGraph V
H : SimpleGraph W
hG : G.chromaticNumber ≤ ⊤
hH : H.chromaticNumber ≤ ⊤
⊢ (G ⊕g H).chromaticNumber ≤ ⊤

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Sum
Goal:
V : Type u_3
W : Type u_5
G : SimpleGraph V
H : SimpleGraph W
n : ℕ
hG : G.chromaticNumber ≤ (↑n : ℕ∞)
hH : H.chromaticNumber ≤ (↑n : ℕ∞)
cG : G.Coloring (Fin n) := Nonempty.some ⋯
cH : H.Coloring (Fin n) := Nonempty.some ⋯
⊢ (G ⊕g H).chromaticNumber ≤ (↑n : ℕ∞)

Tactic:
chromaticNumber_le_iff_colorable.mpr (Nonempty.intro (cG.sum cH))

Premises used: Iff.mpr, SimpleGraph.chromaticNumber_le_iff_colorable, Nonempty.intro, SimpleGraph.Coloring.sum
-- Module: Mathlib.Combinatorics.SimpleGraph.Sum
Goal:
V : Type u_3
W : Type u_5
G : SimpleGraph V
H : SimpleGraph W
n : ℕ
hG : G.chromaticNumber ≤ (↑n : ℕ∞)
hH : H.chromaticNumber ≤ (↑n : ℕ∞)
cG : G.Coloring (Fin n) := Nonempty.some ⋯
cH : H.Coloring (Fin n) := Nonempty.some ⋯
⊢ (G ⊕g H).chromaticNumber ≤ (↑n : ℕ∞)

Tactic:
exact chromaticNumber_le_iff_colorable.mpr (Nonempty.intro (cG.sum cH))

Premises used: Iff.mpr, SimpleGraph.chromaticNumber_le_iff_colorable, Nonempty.intro, SimpleGraph.Coloring.sum
-- Module: Mathlib.Combinatorics.SimpleGraph.Sum
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 ≤ ⊤
coe :
  ∀ (n : ℕ) (hG : G.chromaticNumber ≤ (↑n : ℕ∞)) (hH : H.chromaticNumber ≤ (↑n : ℕ∞)),
    (G ⊕g H).chromaticNumber ≤ (↑n : ℕ∞)
⊢ (G ⊕g H).chromaticNumber ≤ d

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))
-- Module: Mathlib.Combinatorics.SimpleGraph.Sum
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')
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')
⊢ (G ⊕g H).neighborSet (Sum.inl v) = Sum.inl '' G.neighborSet v

Tactic:
ext (v' | w')
-- Module: Mathlib.Combinatorics.SimpleGraph.Sum
Goal:
V : Type u_3
W : Type u_5
G : SimpleGraph V
H : SimpleGraph W
v 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:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Sum
Goal:
V : Type u_3
W : Type u_5
G : SimpleGraph V
H : SimpleGraph W
v : V
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:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Sum
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')
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')
⊢ (G ⊕g H).neighborSet (Sum.inr w) = Sum.inr '' H.neighborSet w

Tactic:
ext (v' | w')
-- Module: Mathlib.Combinatorics.SimpleGraph.Sum
Goal:
V : Type u_3
W : Type u_5
G : SimpleGraph V
H : SimpleGraph W
w : W
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:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Sum
Goal:
V : Type u_3
W : Type u_5
G : SimpleGraph V
H : SimpleGraph W
w 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:
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
inst : DecidableEq V
inst_1 : DecidableEq W
inst_2 : G.LocallyFinite
inst_3 : H.LocallyFinite
v : V
inl : Fintype (↑(Sum.inl '' G.neighborSet v) : Type (max u_5 u_3))
⊢ Fintype (↑((G ⊕g H).neighborSet (Sum.inl v)) : Type (max u_5 u_3))

Tactic:
simp only [neighborSet_sum_inl, neighborSet_sum_inr]

Premises used: SimpleGraph.neighborSet_sum_inl, SimpleGraph.neighborSet_sum_inr
-- 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_1 w' : W
inst : DecidableEq V
inst_1 : DecidableEq W
inst_2 : G.LocallyFinite
inst_3 : H.LocallyFinite
w : W
inr : Fintype (↑(Sum.inr '' H.neighborSet w) : Type (max u_5 u_3))
⊢ Fintype (↑((G ⊕g H).neighborSet (Sum.inr w)) : Type (max u_5 u_3))

Tactic:
simp only [neighborSet_sum_inl, neighborSet_sum_inr]

Premises used: SimpleGraph.neighborSet_sum_inl, SimpleGraph.neighborSet_sum_inr
-- 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
inst : DecidableEq V
inst_1 : DecidableEq W
inst_2 : G.LocallyFinite
inst_3 : H.LocallyFinite
v : V
⊢ Fintype (↑(Sum.inl '' G.neighborSet v) : Type (max u_5 u_3))

Tactic:
infer_instance
-- 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_1 w' : W
inst : DecidableEq V
inst_1 : DecidableEq W
inst_2 : G.LocallyFinite
inst_3 : H.LocallyFinite
w : W
⊢ Fintype (↑(Sum.inr '' H.neighborSet w) : Type (max u_5 u_3))

Tactic:
infer_instance
-- Module: Mathlib.Combinatorics.SimpleGraph.Trails
Goal:
V : Type u_1
G : SimpleGraph V
inst : DecidableEq V
u v x u_1 : V
ht : IsTrail.{u_1} (V := V) (G := G) (u := u_1) Walk.nil
⊢ Even (List.countP (fun (e : Sym2 V) ↦ decide (x ∈ e)) (edges (G := G) (u := u_1) Walk.nil)) ↔
    u_1 ≠ u_1 → x ≠ u_1 ∧ x ≠ u_1

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Trails
Goal:
V : Type u_1
G : SimpleGraph V
inst : DecidableEq V
u v x u_1 v_1 w : V
huv : G.Adj u_1 v_1
p : G.Walk v_1 w
ih : ∀ (ht : p.IsTrail), Even (List.countP (fun (e : Sym2 V) ↦ decide (x ∈ e)) p.edges) ↔ v_1 ≠ w → x ≠ v_1 ∧ x ≠ w
ht : (cons huv p).IsTrail
⊢ p.IsTrail ∧ s(u_1, v_1) ∉ p.edges

Tactic:
rw [isTrail_cons] at ht

Premises used: SimpleGraph.Walk.isTrail_cons
-- Module: Mathlib.Combinatorics.SimpleGraph.Trails
Goal:
V : Type u_1
G : SimpleGraph V
inst : DecidableEq V
u v x u_1 v_1 w : V
huv : G.Adj u_1 v_1
p : G.Walk v_1 w
ih : ∀ (ht : p.IsTrail), Even (List.countP (fun (e : Sym2 V) ↦ decide (x ∈ e)) p.edges) ↔ v_1 ≠ w → x ≠ v_1 ∧ x ≠ w
ht : p.IsTrail ∧ s(u_1, v_1) ∉ p.edges
⊢ Even (List.countP (fun (e : Sym2 V) ↦ decide (x ∈ e)) p.edges) ↔ v_1 ≠ w → x ≠ v_1 ∧ x ≠ w

Tactic:
specialize ih ht.1

Premises used: And.left
-- Module: Mathlib.Combinatorics.SimpleGraph.Trails
Goal:
V : Type u_1
G : SimpleGraph V
inst : DecidableEq V
u v x u_1 v_1 w : V
huv : G.Adj u_1 v_1
p : G.Walk v_1 w
ht : p.IsTrail ∧ s(u_1, v_1) ∉ p.edges
ih : Even (List.countP (fun (e : Sym2 V) ↦ decide (x ∈ e)) p.edges) ↔ v_1 ≠ w → x ≠ v_1 ∧ x ≠ w
cons :
  Even (List.countP (fun (e : Sym2 V) ↦ decide (x ∈ e)) p.edges + if decide (x = u_1 ∨ x = v_1) = true then 1 else 0) ↔
    ¬u_1 = w → ¬x = u_1 ∧ ¬x = w
⊢ Even (List.countP (fun (e : Sym2 V) ↦ decide (x ∈ e)) (Walk.cons huv p).edges) ↔ u_1 ≠ w → x ≠ u_1 ∧ x ≠ w

Tactic:
simp only [List.countP_cons, Ne, edges_cons, Sym2.mem_iff]

Premises used: Ne, SimpleGraph.Walk.edges_cons, Sym2.mem_iff, List.countP_cons
-- Module: Mathlib.Combinatorics.SimpleGraph.Trails
Goal:
V : Type u_1
G : SimpleGraph V
inst : DecidableEq V
u v x u_1 v_1 w : V
huv : G.Adj u_1 v_1
p : G.Walk v_1 w
ht : p.IsTrail ∧ s(u_1, v_1) ∉ p.edges
ih : Even (List.countP (fun (e : Sym2 V) ↦ decide (x ∈ e)) p.edges) ↔ v_1 ≠ w → x ≠ v_1 ∧ x ≠ w
pos :
  ∀ (h : decide (x = u_1 ∨ x = v_1) = true),
    Even (List.countP (fun (e : Sym2 V) ↦ decide (x ∈ e)) p.edges + 1) ↔ ¬u_1 = w → ¬x = u_1 ∧ ¬x = w
neg :
  ∀ (h : ¬decide (x = u_1 ∨ x = v_1) = true),
    Even (List.countP (fun (e : Sym2 V) ↦ decide (x ∈ e)) p.edges + 0) ↔ ¬u_1 = w → ¬x = u_1 ∧ ¬x = w
⊢ Even (List.countP (fun (e : Sym2 V) ↦ decide (x ∈ e)) p.edges + if decide (x = u_1 ∨ x = v_1) = true then 1 else 0) ↔
    ¬u_1 = w → ¬x = u_1 ∧ ¬x = w

Tactic:
split_ifs with h
-- Module: Mathlib.Combinatorics.SimpleGraph.Trails
Goal:
V : Type u_1
G : SimpleGraph V
inst : DecidableEq V
u v x u_1 v_1 w : V
huv : G.Adj u_1 v_1
p : G.Walk v_1 w
ht : p.IsTrail ∧ s(u_1, v_1) ∉ p.edges
ih : Even (List.countP (fun (e : Sym2 V) ↦ decide (x ∈ e)) p.edges) ↔ v_1 ≠ w → x ≠ v_1 ∧ x ≠ w
h : decide (x = u_1 ∨ x = v_1) = true
⊢ x = u_1 ∨ x = v_1

Tactic:
rw [decide_eq_true_eq] at h

Premises used: decide_eq_true_eq
-- Module: Mathlib.Combinatorics.SimpleGraph.Trails
Goal:
V : Type u_1
G : SimpleGraph V
inst : DecidableEq V
u v x u_1 v_1 w : V
huv : G.Adj u_1 v_1
p : G.Walk v_1 w
ht : p.IsTrail ∧ s(u_1, v_1) ∉ p.edges
ih : Even (List.countP (fun (e : Sym2 V) ↦ decide (x ∈ e)) p.edges) ↔ v_1 ≠ w → x ≠ v_1 ∧ x ≠ w
h : x = u_1 ∨ x = v_1
pos :
  ∀ (huv : G.Adj x v_1) (ht : p.IsTrail ∧ s(x, v_1) ∉ p.edges),
    Even (List.countP (fun (e : Sym2 V) ↦ decide (x ∈ e)) p.edges + 1) ↔ ¬x = w → ¬x = x ∧ ¬x = w
pos₁ :
  ∀ (huv : G.Adj u_1 x) (p : G.Walk x w) (ht : p.IsTrail ∧ s(u_1, x) ∉ p.edges)
    (ih : Even (List.countP (fun (e : Sym2 V) ↦ decide (x ∈ e)) p.edges) ↔ x ≠ w → x ≠ x ∧ x ≠ w),
    Even (List.countP (fun (e : Sym2 V) ↦ decide (x ∈ e)) p.edges + 1) ↔ ¬u_1 = w → ¬x = u_1 ∧ ¬x = w
⊢ Even (List.countP (fun (e : Sym2 V) ↦ decide (x ∈ e)) p.edges + 1) ↔ ¬u_1 = w → ¬x = u_1 ∧ ¬x = w

Tactic:
obtain (rfl | rfl) := h

Premises used: rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Trails
Goal:
V : Type u_1
G : SimpleGraph V
inst : DecidableEq V
u v x v_1 w : V
p : G.Walk v_1 w
ih : Even (List.countP (fun (e : Sym2 V) ↦ decide (x ∈ e)) p.edges) ↔ v_1 ≠ w → x ≠ v_1 ∧ x ≠ w
huv : G.Adj x v_1
ht : p.IsTrail ∧ s(x, v_1) ∉ p.edges
pos : ¬(v_1 ≠ w → x ≠ v_1 ∧ x ≠ w) ↔ ¬x = w → ¬x = x ∧ ¬x = w
⊢ Even (List.countP (fun (e : Sym2 V) ↦ decide (x ∈ e)) p.edges + 1) ↔ ¬x = w → ¬x = x ∧ ¬x = w

Tactic:
rw [Nat.even_add_one, ih]

Premises used: Nat.even_add_one
-- Module: Mathlib.Combinatorics.SimpleGraph.Trails
Goal:
V : Type u_1
G : SimpleGraph V
inst : DecidableEq V
u v x v_1 w : V
p : G.Walk v_1 w
ih : Even (List.countP (fun (e : Sym2 V) ↦ decide (x ∈ e)) p.edges) ↔ v_1 ≠ w → x ≠ v_1 ∧ x ≠ w
huv : G.Adj x v_1
ht : p.IsTrail ∧ s(x, v_1) ∉ p.edges
pos : x = w → ¬v_1 = w
⊢ ¬(v_1 ≠ w → x ≠ v_1 ∧ x ≠ w) ↔ ¬x = w → ¬x = x ∧ ¬x = w

Tactic:
simp only [huv.ne, imp_false, Ne, not_false_iff, true_and, not_forall,
          Classical.not_not, exists_prop, not_true, false_and,
          and_iff_right_iff_imp]

Premises used: SimpleGraph.Adj.ne, Classical.not_not, imp_false, false_and, Ne, exists_prop, and_iff_right_iff_imp, not_true, not_false_iff, Classical.not_forall, true_and
-- Module: Mathlib.Combinatorics.SimpleGraph.Trails
Goal:
V : Type u_1
G : SimpleGraph V
inst : DecidableEq V
u v v_1 : V
huv : G.Adj v_1 v_1
p : G.Walk v_1 v_1
ih : Even (List.countP (fun (e : Sym2 V) ↦ decide (v_1 ∈ e)) p.edges) ↔ v_1 ≠ v_1 → v_1 ≠ v_1 ∧ v_1 ≠ v_1
ht : p.IsTrail ∧ s(v_1, v_1) ∉ p.edges
⊢ False

Tactic:
G.loopless.irrefl _ huv

Premises used: Std.Irrefl.irrefl
-- Module: Mathlib.Combinatorics.SimpleGraph.Trails
Goal:
V : Type u_1
G : SimpleGraph V
inst : DecidableEq V
u v v_1 : V
huv : G.Adj v_1 v_1
p : G.Walk v_1 v_1
ih : Even (List.countP (fun (e : Sym2 V) ↦ decide (v_1 ∈ e)) p.edges) ↔ v_1 ≠ v_1 → v_1 ≠ v_1 ∧ v_1 ≠ v_1
ht : p.IsTrail ∧ s(v_1, v_1) ∉ p.edges
⊢ False

Tactic:
exact G.loopless.irrefl _ huv

Premises used: Std.Irrefl.irrefl
-- Module: Mathlib.Combinatorics.SimpleGraph.Trails
Goal:
V : Type u_1
G : SimpleGraph V
inst : DecidableEq V
u v x u_1 w : V
huv : G.Adj u_1 x
p : G.Walk x w
ht : p.IsTrail ∧ s(u_1, x) ∉ p.edges
ih : Even (List.countP (fun (e : Sym2 V) ↦ decide (x ∈ e)) p.edges) ↔ x ≠ w → x ≠ x ∧ x ≠ w
⊢ u_1 ≠ x

Tactic:
have := huv.ne
-- Module: Mathlib.Combinatorics.SimpleGraph.Trails
Goal:
V : Type u_1
G : SimpleGraph V
inst : DecidableEq V
u v x u_1 w : V
huv : G.Adj u_1 x
p : G.Walk x w
ht : p.IsTrail ∧ s(u_1, x) ∉ p.edges
ih : Even (List.countP (fun (e : Sym2 V) ↦ decide (x ∈ e)) p.edges) ↔ x ≠ w → x ≠ x ∧ x ≠ w
this : u_1 ≠ x
⊢ Even (List.countP (fun (e : Sym2 V) ↦ decide (x ∈ e)) p.edges + 1) ↔ ¬u_1 = w → ¬x = u_1 ∧ ¬x = w

Tactic:
grind
-- Module: Mathlib.Combinatorics.SimpleGraph.Trails
Goal:
V : Type u_1
G : SimpleGraph V
inst : DecidableEq V
u v x u_1 v_1 w : V
huv : G.Adj u_1 v_1
p : G.Walk v_1 w
ht : p.IsTrail ∧ s(u_1, v_1) ∉ p.edges
ih : Even (List.countP (fun (e : Sym2 V) ↦ decide (x ∈ e)) p.edges) ↔ v_1 ≠ w → x ≠ v_1 ∧ x ≠ w
h : ¬decide (x = u_1 ∨ x = v_1) = true
⊢ Even (List.countP (fun (e : Sym2 V) ↦ decide (x ∈ e)) p.edges + 0) ↔ ¬u_1 = w → ¬x = u_1 ∧ ¬x = w

Tactic:
grind