awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions (hypothesis)
Goal:
α : Type u_1
G : SimpleGraph α
h : ∀ (u : α) (w : G.Walk u u), ¬Odd w.length
c : G.ConnectedComponent
w : α
hv : w ∈ c.supp
a b : ↥c
hab : c.toSimpleGraph.Adj a b
he :
  Eq (α := Fin 2) (Fin.ofNat 2 (length (u := Subtype.mk (p := fun (x : α) ↦ x ∈ c) w hv) (Nonempty.some ⋯)))
    (Fin.ofNat 2 (length (u := Subtype.mk (p := fun (x : α) ↦ x ∈ c) w hv) (Nonempty.some ⋯)))
⊢ Odd
    (length (u := Subtype.mk (p := fun (x : α) ↦ x ∈ c) w hv) (Nonempty.some ⋯) +
        length (u := Subtype.mk (p := fun (x : α) ↦ x ∈ c) w hv) (Nonempty.some ⋯) +
      1)
have this : length (u := Subtype.mk (p := fun (x : α) ↦ x ∈ c) w hv) (Nonempty.some sorry) % 2 =
  length (u := Subtype.mk (p := fun (x : α) ↦ x ∈ c) w hv) (Nonempty.some sorry) % 2
Tactic: have : ((Nonempty.some (c.connected_toSimpleGraph ⟨_, hv⟩ a)).length) % 2 =
        (Nonempty.some (c.connected_toSimpleGraph ⟨_, hv⟩ b)).length % 2 := by
      simp_rw [← Fin.val_natCast, ← Fin.ofNat_eq_cast, he]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling (goal)
Goal:
V : Type u_1
K : Type u_3
inst : DecidableEq V
inst_1 : Fintype V
inst_2 : Fintype K
⊢ Fintype.card K ^ Fintype.card.{u_1} (↑(edgeSet ⊤) : Type u_1) = Fintype.card K ^ (Fintype.card V).choose 2
have rw : Fintype.card K ^ Finset.card.{u_1} (α := Sym2 V) (edgeFinset ⊤) = Fintype.card K ^ (Fintype.card V).choose 2
Tactic: rw [← edgeFinset_card, card_edgeFinset_top_eq_card_choose_two]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling (goal)
Goal:
V : Type u_1
K : Type u_3
inst : DecidableEq V
inst_1 : Fintype V
inst_2 : Fintype K
rw : Fintype.card K ^ Finset.card.{u_1} (α := Sym2 V) (edgeFinset ⊤) = Fintype.card K ^ (Fintype.card V).choose 2
⊢ Fintype.card K ^ Fintype.card.{u_1} (↑(edgeSet ⊤) : Type u_1) = Fintype.card K ^ (Fintype.card V).choose 2
have rw₁ : Fintype.card K ^ (Fintype.card V).choose 2 = Fintype.card K ^ (Fintype.card V).choose 2
Tactic: rw [← edgeFinset_card, card_edgeFinset_top_eq_card_choose_two]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling (goal)
Goal:
V : Type u_1
G : SimpleGraph V
K : Type u_3
C C' : G.EdgeLabeling K
h : ∀ (x y : V) (h : G.Adj x y), C.get x y h = C'.get x y h
⊢ C = C'
have h₁ : ∀ (e : Sym2 V) (he : e ∈ G.edgeSet),
  C (Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ G.edgeSet) e he) =
    C' (Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ G.edgeSet) e he)
Tactic: funext ⟨e, he⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling (goal)
Goal:
V : Type u_1
G : SimpleGraph V
K : Type u_3
C C' : G.EdgeLabeling K
h : ∀ (x y : V) (h : G.Adj x y), C.get x y h = C'.get x y h
e : Sym2 V
he : e ∈ G.edgeSet
⊢ C (Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ G.edgeSet) e he) =
    C' (Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ G.edgeSet) e he)
have h₁ : ∀ (x y : V) (he : s(x, y) ∈ G.edgeSet),
  C (Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ G.edgeSet) s(x, y) he) =
    C' (Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ G.edgeSet) s(x, y) he)
Tactic: induction e using Sym2.inductionOn
Cleared hypotheses: e, he
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling (goal)
Goal:
V : Type u_1
V' : Type u_2
G : SimpleGraph V
G' : SimpleGraph V'
K : Type u_3
K' : Type u_4
C : G.EdgeLabeling K
f : (x y : V) → G.Adj x y → K
f_symm : ∀ (x y : V) (H : G.Adj x y), f y x ⋯ = f x y H
e : Sym2 V
he : e ∈ G.edgeSet
⊢ K
have revert : (he : e ∈ G.edgeSet) → K
Tactic: revert he
Cleared hypotheses: he
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling (goal)
Goal:
V : Type u_1
V' : Type u_2
G : SimpleGraph V
G' : SimpleGraph V'
K : Type u_3
K' : Type u_4
C : G.EdgeLabeling K
f : (x y : V) → G.Adj x y → K
f_symm : ∀ (x y : V) (H : G.Adj x y), f y x ⋯ = f x y H
e : Sym2 V
⊢ (he : e ∈ G.edgeSet) → K
have refine : ∀ (a b : V), f a b ≍ f b a
Tactic: refine Sym2.hrec f (fun a b ↦ ?_) e
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling (goal)
Goal:
V : Type u_1
V' : Type u_2
G : SimpleGraph V
G' : SimpleGraph V'
K : Type u_3
K' : Type u_4
C : G.EdgeLabeling K
f : (x y : V) → G.Adj x y → K
f_symm : ∀ (x y : V) (H : G.Adj x y), f y x ⋯ = f x y H
e : Sym2 V
a b : V
⊢ f a b ≍ f b a
have apply : ∀ (a_1 : G.Adj a b) (a' : G.Adj b a), a_1 ≍ a' → f a b a_1 ≍ f b a a'
Tactic: apply Function.hfunext (by simp [adj_comm])
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling (goal)
Goal:
V : Type u_1
G : SimpleGraph V
K : Type u_3
C : G.EdgeLabeling K
k : K
x y : V
⊢ Adj (fromEdgeSet {e : Sym2 V | ∃ (h : e ∈ G.edgeSet), C (Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ G.edgeSet) e h) = k})
      x y ↔
    ∃ (H : G.Adj x y), C (Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ G.edgeSet) s(x, y) H) = k
have simp : (∃ (h : G.Adj x y), C (Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ G.edgeSet) s(x, y) sorry) = k) ∧ ¬x = y ↔
  ∃ (H : G.Adj x y), C (Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ G.edgeSet) s(x, y) H) = k
Tactic: simp only [mem_edgeSet, fromEdgeSet_adj, Set.mem_setOf_eq, Ne.eq_def]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling (goal)
Goal:
V : Type u_1
G : SimpleGraph V
K : Type u_3
C : G.EdgeLabeling K
i j : K
h : i ≠ j
⊢ Disjoint (C.labelGraph i) (C.labelGraph j)
have rw : ∀ (x y : V), (C.labelGraph i).Adj x y → ¬(C.labelGraph j).Adj x y
Tactic: rw [disjoint_left]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling (goal)
Goal:
V : Type u_1
G : SimpleGraph V
K : Type u_3
C : G.EdgeLabeling K
⊢ ⨆ (k : K), C.labelGraph k = G
have Adj : ∀ (x y : V), Adj (⨆ (k : K), C.labelGraph k) x y ↔ G.Adj x y
Tactic: ext x y
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling (goal)
Goal:
V : Type u_1
G : SimpleGraph V
K : Type u_3
C : G.EdgeLabeling K
x y : V
⊢ Adj (⨆ (k : K), C.labelGraph k) x y ↔ G.Adj x y
have Adj : (∃ (i : K) (H : G.Adj x y), C (Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ G.edgeSet) s(x, y) H) = i) ↔ G.Adj x y
Tactic: simp only [iSup_adj, EdgeLabeling.labelGraph_adj]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : DecidableRel G.Adj
⊢ EdgeLabeling.labelGraph G.toTopEdgeLabeling 1 = G
have Adj : ∀ (x y : V), (EdgeLabeling.labelGraph G.toTopEdgeLabeling 1).Adj x y ↔ G.Adj x y
Tactic: ext x y
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : DecidableRel G.Adj
⊢ EdgeLabeling.labelGraph G.toTopEdgeLabeling 0 = Gᶜ
have Adj : ∀ (x y : V), (EdgeLabeling.labelGraph G.toTopEdgeLabeling 0).Adj x y ↔ Gᶜ.Adj x y
Tactic: ext x y
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling (goal)
Goal:
V : Type u_1
inst : DecidableEq V
C : TopEdgeLabeling V (Fin 2)
⊢ (EdgeLabeling.labelGraph C 1).toTopEdgeLabeling = C
have refine : ∀ (x y : V) (h : Adj ⊤ x y),
  EdgeLabeling.get (EdgeLabeling.labelGraph C 1).toTopEdgeLabeling x y h = EdgeLabeling.get C x y h
Tactic: refine EdgeLabeling.ext_get ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (goal)
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
ι : Type u_1
α : Type u_2
β : Type u_3
C : G.Coloring α
inst : Nonempty (G.Coloring α)
inst_1 : Nontrivial α
inst_2 : Nonempty V
⊢ Nontrivial (G.Coloring α)
have have : ∀ (C : G.Coloring α), Nontrivial (G.Coloring α)
Tactic: have ⟨C⟩ := ‹Nonempty <| G.Coloring α›
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (goal)
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
ι : Type u_1
α : Type u_2
β : Type u_3
C_1 : G.Coloring α
inst : Nonempty (G.Coloring α)
inst_1 : Nontrivial α
inst_2 : Nonempty V
C : G.Coloring α
⊢ Nontrivial (G.Coloring α)
have have : ∀ (v : V), Nontrivial (G.Coloring α)
Tactic: have ⟨v⟩ := ‹Nonempty V›
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (goal)
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
ι : Type u_1
α : Type u_2
β : Type u_3
C_1 : G.Coloring α
inst : Nonempty (G.Coloring α)
inst_1 : Nontrivial α
inst_2 : Nonempty V
C : G.Coloring α
v : V
⊢ Nontrivial (G.Coloring α)
have have : ∀ (c : α) (hc : c ≠ (C : (a : V) → α) v), Nontrivial (G.Coloring α)
Tactic: have ⟨c, hc⟩ := nontrivial_iff_exists_ne (C v) |>.mp inferInstance
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (goal)
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
ι : Type u_1
α : Type u_2
β : Type u_3
C_1 : G.Coloring α
inst : Nonempty (G.Coloring α)
inst_1 : Nontrivial α
inst_2 : Nonempty V
C : G.Coloring α
v : V
c : α
hc : c ≠ (C : (a : V) → α) v
⊢ Nontrivial (G.Coloring α)
have refine : ∀ (h : Hom.comp (Iso.toHom (Iso.completeGraph (Equiv.swap ((C : (a : V) → α) v) c))) C = C), c = (C : (a : V) → α) v
Tactic: refine ⟨(Iso.completeGraph <| Equiv.swap (C v) c).toHom.comp C, C, fun h ↦ hc ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
ι : Type u_1
α : Type u_2
β : Type u_3
C_1 : G.Coloring α
inst : Nonempty (G.Coloring α)
inst_1 : Nontrivial α
inst_2 : Nonempty V
C : G.Coloring α
v : V
c : α
hc : c ≠ (C : (a : V) → α) v
h : Hom.comp (Iso.toHom (Iso.completeGraph (Equiv.swap ((C : (a : V) → α) v) c))) C = C
⊢ c = (C : (a : V) → α) v
have this : RelHom.toFun (r := G.Adj) (s := (completeGraph α).Adj)
    (Hom.comp (Iso.toHom (Iso.completeGraph (Equiv.swap ((C : (a : V) → α) v) c))) C) v =
  C.toFun (r := G.Adj) (s := (completeGraph α).Adj) v
Tactic: have := congrFun (congrArg RelHom.toFun h) v
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (goal)
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
ι : Type u_1
α : Type u_2
β : Type u_3
C : G.Coloring α
inst : Nonempty (G.Coloring α)
inst_1 : Nontrivial α
inst_2 : Nonempty V
⊢ Nontrivial (G.Coloring α)
have have : ∀ (C : G.Coloring α), Nontrivial (G.Coloring α)
Tactic: classical
  have ⟨C⟩ := ‹Nonempty <| G.Coloring α›
  have ⟨v⟩ := ‹Nonempty V›
  have ⟨c, hc⟩ := nontrivial_iff_exists_ne (C v) |>.mp inferInstance
  refine ⟨(Iso.completeGraph <| Equiv.swap (C v) c).toHom.comp C, C, fun h ↦ hc ?_⟩
  have := congrFun (congrArg RelHom.toFun h) v
  dsimp [Iso.completeGraph] at this
  grind
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (goal)
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
ι : Type u_1
α : Type u_2
β : Type u_3
C : G.Coloring α
inst : Nonempty (G.Coloring α)
inst_1 : Nontrivial α
inst_2 : Nonempty V
have have₁ have₂ : ∀ (C : G.Coloring α), Nontrivial (G.Coloring α)
⊢ Nontrivial (G.Coloring α)
have have₃ : ∀ (C : G.Coloring α) (v : V), Nontrivial (G.Coloring α)
Tactic: classical
  have ⟨C⟩ := ‹Nonempty <| G.Coloring α›
  have ⟨v⟩ := ‹Nonempty V›
  have ⟨c, hc⟩ := nontrivial_iff_exists_ne (C v) |>.mp inferInstance
  refine ⟨(Iso.completeGraph <| Equiv.swap (C v) c).toHom.comp C, C, fun h ↦ hc ?_⟩
  have := congrFun (congrArg RelHom.toFun h) v
  dsimp [Iso.completeGraph] at this
  grind
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (goal)
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
ι : Type u_1
α : Type u_2
β : Type u_3
C : G.Coloring α
inst : Nonempty (G.Coloring α)
inst_1 : Nontrivial α
inst_2 : Nonempty V
have have₁ have₂ : ∀ (C : G.Coloring α), Nontrivial (G.Coloring α)
have₃ : ∀ (C : G.Coloring α) (v : V), Nontrivial (G.Coloring α)
⊢ Nontrivial (G.Coloring α)
have have₄ : ∀ (C : G.Coloring α) (v : V) (c : α) (hc : c ≠ (C : (a : V) → α) v), Nontrivial (G.Coloring α)
Tactic: classical
  have ⟨C⟩ := ‹Nonempty <| G.Coloring α›
  have ⟨v⟩ := ‹Nonempty V›
  have ⟨c, hc⟩ := nontrivial_iff_exists_ne (C v) |>.mp inferInstance
  refine ⟨(Iso.completeGraph <| Equiv.swap (C v) c).toHom.comp C, C, fun h ↦ hc ?_⟩
  have := congrFun (congrArg RelHom.toFun h) v
  dsimp [Iso.completeGraph] at this
  grind
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (goal)
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
ι : Type u_1
α : Type u_2
β : Type u_3
C : G.Coloring α
inst : Nonempty (G.Coloring α)
inst_1 : Nontrivial α
inst_2 : Nonempty V
have have₁ have₂ : ∀ (C : G.Coloring α), Nontrivial (G.Coloring α)
have₃ : ∀ (C : G.Coloring α) (v : V), Nontrivial (G.Coloring α)
have₄ : ∀ (C : G.Coloring α) (v : V) (c : α) (hc : c ≠ (C : (a : V) → α) v), Nontrivial (G.Coloring α)
⊢ Nontrivial (G.Coloring α)
have have₅ : ∀ (C : G.Coloring α) (v : V) (c : α) (hc : c ≠ (C : (a : V) → α) v)
  (h : Hom.comp (Iso.toHom (Iso.completeGraph (Equiv.swap ((C : (a : V) → α) v) c))) C = C), c = (C : (a : V) → α) v
Tactic: classical
  have ⟨C⟩ := ‹Nonempty <| G.Coloring α›
  have ⟨v⟩ := ‹Nonempty V›
  have ⟨c, hc⟩ := nontrivial_iff_exists_ne (C v) |>.mp inferInstance
  refine ⟨(Iso.completeGraph <| Equiv.swap (C v) c).toHom.comp C, C, fun h ↦ hc ?_⟩
  have := congrFun (congrArg RelHom.toFun h) v
  dsimp [Iso.completeGraph] at this
  grind
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (goal)
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
ι : Type u_1
α : Type u_2
β : Type u_3
C : G.Coloring α
inst : Nonempty (G.Coloring α)
inst_1 : Nontrivial α
inst_2 : Nonempty V
have have₁ have₂ : ∀ (C : G.Coloring α), Nontrivial (G.Coloring α)
have₃ : ∀ (C : G.Coloring α) (v : V), Nontrivial (G.Coloring α)
have₄ : ∀ (C : G.Coloring α) (v : V) (c : α) (hc : c ≠ (C : (a : V) → α) v), Nontrivial (G.Coloring α)
have₅ :
  ∀ (C : G.Coloring α) (v : V) (c : α) (hc : c ≠ (C : (a : V) → α) v)
    (h : Hom.comp (Iso.toHom (Iso.completeGraph (Equiv.swap ((C : (a : V) → α) v) c))) C = C), c = (C : (a : V) → α) v
⊢ Nontrivial (G.Coloring α)
have have₆ : ∀ (C : G.Coloring α) (v : V) (c : α) (hc : c ≠ (C : (a : V) → α) v)
  (h : Hom.comp (Iso.toHom (Iso.completeGraph (Equiv.swap ((C : (a : V) → α) v) c))) C = C)
  (this :
    RelHom.toFun (r := G.Adj) (s := (completeGraph α).Adj)
        (Hom.comp (Iso.toHom (Iso.completeGraph (Equiv.swap ((C : (a : V) → α) v) c))) C) v =
      C.toFun (r := G.Adj) (s := (completeGraph α).Adj) v),
  c = (C : (a : V) → α) v
Tactic: classical
  have ⟨C⟩ := ‹Nonempty <| G.Coloring α›
  have ⟨v⟩ := ‹Nonempty V›
  have ⟨c, hc⟩ := nontrivial_iff_exists_ne (C v) |>.mp inferInstance
  refine ⟨(Iso.completeGraph <| Equiv.swap (C v) c).toHom.comp C, C, fun h ↦ hc ?_⟩
  have := congrFun (congrArg RelHom.toFun h) v
  dsimp [Iso.completeGraph] at this
  grind
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (goal)
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
ι : Type u_1
α : Type u_2
β : Type u_3
C : G.Coloring α
inst : Nonempty (G.Coloring α)
inst_1 : Nontrivial α
inst_2 : Nonempty V
have have₁ have₂ : ∀ (C : G.Coloring α), Nontrivial (G.Coloring α)
have₃ : ∀ (C : G.Coloring α) (v : V), Nontrivial (G.Coloring α)
have₄ : ∀ (C : G.Coloring α) (v : V) (c : α) (hc : c ≠ (C : (a : V) → α) v), Nontrivial (G.Coloring α)
have₅ :
  ∀ (C : G.Coloring α) (v : V) (c : α) (hc : c ≠ (C : (a : V) → α) v)
    (h : Hom.comp (Iso.toHom (Iso.completeGraph (Equiv.swap ((C : (a : V) → α) v) c))) C = C), c = (C : (a : V) → α) v
have₆ :
  ∀ (C : G.Coloring α) (v : V) (c : α) (hc : c ≠ (C : (a : V) → α) v)
    (h : Hom.comp (Iso.toHom (Iso.completeGraph (Equiv.swap ((C : (a : V) → α) v) c))) C = C)
    (this :
      RelHom.toFun (r := G.Adj) (s := (completeGraph α).Adj)
          (Hom.comp (Iso.toHom (Iso.completeGraph (Equiv.swap ((C : (a : V) → α) v) c))) C) v =
        C.toFun (r := G.Adj) (s := (completeGraph α).Adj) v),
    c = (C : (a : V) → α) v
⊢ Nontrivial (G.Coloring α)
have have₇ : ∀ (C : G.Coloring α) (v : V) (c : α) (hc : c ≠ (C : (a : V) → α) v)
  (h : Hom.comp (Iso.toHom (Iso.completeGraph (Equiv.swap ((C : (a : V) → α) v) c))) C = C)
  (this :
    Eq.{u_2 + 1} (α := α)
      (((Equiv.swap ((C : (a : V) → α) v) c : Equiv.Perm α) : (a : α) → α) ((C : (a : V) → α) v : α) : α)
      ((C : (a : V) → α) v : α)),
  c = (C : (a : V) → α) v
Tactic: classical
  have ⟨C⟩ := ‹Nonempty <| G.Coloring α›
  have ⟨v⟩ := ‹Nonempty V›
  have ⟨c, hc⟩ := nontrivial_iff_exists_ne (C v) |>.mp inferInstance
  refine ⟨(Iso.completeGraph <| Equiv.swap (C v) c).toHom.comp C, C, fun h ↦ hc ?_⟩
  have := congrFun (congrArg RelHom.toFun h) v
  dsimp [Iso.completeGraph] at this
  grind
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (goal)
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
ι : Type u_1
α : Type u_2
β : Type u_3
C : G.Coloring α
inst : Nonempty (G.Coloring α)
inst_1 : Infinite α
inst_2 : Nonempty V
⊢ Infinite (G.Coloring α)
have have : ∀ (C : G.Coloring α), Infinite (G.Coloring α)
Tactic: have ⟨C⟩ := ‹Nonempty <| G.Coloring α›
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (goal)
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
ι : Type u_1
α : Type u_2
β : Type u_3
C_1 : G.Coloring α
inst : Nonempty (G.Coloring α)
inst_1 : Infinite α
inst_2 : Nonempty V
C : G.Coloring α
⊢ Infinite (G.Coloring α)
have have : ∀ (v : V), Infinite (G.Coloring α)
Tactic: have ⟨v⟩ := ‹Nonempty V›
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (goal)
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
ι : Type u_1
α : Type u_2
β : Type u_3
C_1 : G.Coloring α
inst : Nonempty (G.Coloring α)
inst_1 : Infinite α
inst_2 : Nonempty V
C : G.Coloring α
v : V
f : (c : α) → G →g completeGraph α :=
  fun (c : α) ↦ Hom.comp (Iso.toHom (Iso.completeGraph (Equiv.swap ((C : (a : V) → α) v) c))) C
⊢ Infinite (G.Coloring α)
have refine : ∀ (a b : α) (h : f a = f b), a = b
Tactic: refine Infinite.of_injective f fun a b h ↦ ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
ι : Type u_1
α : Type u_2
β : Type u_3
C_1 : G.Coloring α
inst : Nonempty (G.Coloring α)
inst_1 : Infinite α
inst_2 : Nonempty V
C : G.Coloring α
v : V
f : (c : α) → G →g completeGraph α :=
  fun (c : α) ↦ Hom.comp (Iso.toHom (Iso.completeGraph (Equiv.swap ((C : (a : V) → α) v) c))) C
a b : α
h : f a = f b
⊢ a = b
have this : (f a).toFun (r := G.Adj) (s := (completeGraph α).Adj) v = (f b).toFun (r := G.Adj) (s := (completeGraph α).Adj) v
Tactic: have := congrFun (congrArg RelHom.toFun h) v
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (goal)
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
ι : Type u_1
α : Type u_2
β : Type u_3
C : G.Coloring α
inst : Nonempty (G.Coloring α)
inst_1 : Infinite α
inst_2 : Nonempty V
⊢ Infinite (G.Coloring α)
have have : ∀ (C : G.Coloring α), Infinite (G.Coloring α)
Tactic: classical
  have ⟨C⟩ := ‹Nonempty <| G.Coloring α›
  have ⟨v⟩ := ‹Nonempty V›
  let f c := (Iso.completeGraph <| Equiv.swap (C v) c).toHom.comp C
  refine Infinite.of_injective f fun a b h ↦ ?_
  have := congrFun (congrArg RelHom.toFun h) v
  dsimp [f, Iso.completeGraph] at this
  grind
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (goal)
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
ι : Type u_1
α : Type u_2
β : Type u_3
C : G.Coloring α
inst : Nonempty (G.Coloring α)
inst_1 : Infinite α
inst_2 : Nonempty V
have have₁ have₂ : ∀ (C : G.Coloring α), Infinite (G.Coloring α)
⊢ Infinite (G.Coloring α)
have have₃ : ∀ (C : G.Coloring α) (v : V), Infinite (G.Coloring α)
Tactic: classical
  have ⟨C⟩ := ‹Nonempty <| G.Coloring α›
  have ⟨v⟩ := ‹Nonempty V›
  let f c := (Iso.completeGraph <| Equiv.swap (C v) c).toHom.comp C
  refine Infinite.of_injective f fun a b h ↦ ?_
  have := congrFun (congrArg RelHom.toFun h) v
  dsimp [f, Iso.completeGraph] at this
  grind
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (goal)
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
ι : Type u_1
α : Type u_2
β : Type u_3
C : G.Coloring α
inst : Nonempty (G.Coloring α)
inst_1 : Infinite α
inst_2 : Nonempty V
have have₁ have₂ : ∀ (C : G.Coloring α), Infinite (G.Coloring α)
have₃ have₄ : ∀ (C : G.Coloring α) (v : V), Infinite (G.Coloring α)
⊢ Infinite (G.Coloring α)
have have₅ : ∀ (C : G.Coloring α) (v : V),
  let f : (c : α) → G →g completeGraph α := fun (c : α) ↦
    Hom.comp (Iso.toHom (Iso.completeGraph (Equiv.swap ((C : (a : V) → α) v) c))) C;
  ∀ (a b : α) (h : f a = f b), a = b
Tactic: classical
  have ⟨C⟩ := ‹Nonempty <| G.Coloring α›
  have ⟨v⟩ := ‹Nonempty V›
  let f c := (Iso.completeGraph <| Equiv.swap (C v) c).toHom.comp C
  refine Infinite.of_injective f fun a b h ↦ ?_
  have := congrFun (congrArg RelHom.toFun h) v
  dsimp [f, Iso.completeGraph] at this
  grind
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (goal)
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
ι : Type u_1
α : Type u_2
β : Type u_3
C : G.Coloring α
inst : Nonempty (G.Coloring α)
inst_1 : Infinite α
inst_2 : Nonempty V
have have₁ have₂ : ∀ (C : G.Coloring α), Infinite (G.Coloring α)
have₃ have₄ : ∀ (C : G.Coloring α) (v : V), Infinite (G.Coloring α)
have₅ :
  ∀ (C : G.Coloring α) (v : V),
    let f : (c : α) → G →g completeGraph α := fun (c : α) ↦
      Hom.comp (Iso.toHom (Iso.completeGraph (Equiv.swap ((C : (a : V) → α) v) c))) C;
    ∀ (a b : α) (h : f a = f b), a = b
⊢ Infinite (G.Coloring α)
have have₆ : ∀ (C : G.Coloring α) (v : V),
  let f : (c : α) → G →g completeGraph α := fun (c : α) ↦
    Hom.comp (Iso.toHom (Iso.completeGraph (Equiv.swap ((C : (a : V) → α) v) c))) C;
  ∀ (a b : α) (h : f a = f b)
    (this :
      (f a).toFun (r := G.Adj) (s := (completeGraph α).Adj) v =
        (f b).toFun (r := G.Adj) (s := (completeGraph α).Adj) v),
    a = b
Tactic: classical
  have ⟨C⟩ := ‹Nonempty <| G.Coloring α›
  have ⟨v⟩ := ‹Nonempty V›
  let f c := (Iso.completeGraph <| Equiv.swap (C v) c).toHom.comp C
  refine Infinite.of_injective f fun a b h ↦ ?_
  have := congrFun (congrArg RelHom.toFun h) v
  dsimp [f, Iso.completeGraph] at this
  grind
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (goal)
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
ι : Type u_1
α : Type u_2
β : Type u_3
C : G.Coloring α
inst : Nonempty (G.Coloring α)
inst_1 : Infinite α
inst_2 : Nonempty V
have have₁ have₂ : ∀ (C : G.Coloring α), Infinite (G.Coloring α)
have₃ have₄ : ∀ (C : G.Coloring α) (v : V), Infinite (G.Coloring α)
have₅ :
  ∀ (C : G.Coloring α) (v : V),
    let f : (c : α) → G →g completeGraph α := fun (c : α) ↦
      Hom.comp (Iso.toHom (Iso.completeGraph (Equiv.swap ((C : (a : V) → α) v) c))) C;
    ∀ (a b : α) (h : f a = f b), a = b
have₆ :
  ∀ (C : G.Coloring α) (v : V),
    let f : (c : α) → G →g completeGraph α := fun (c : α) ↦
      Hom.comp (Iso.toHom (Iso.completeGraph (Equiv.swap ((C : (a : V) → α) v) c))) C;
    ∀ (a b : α) (h : f a = f b)
      (this :
        (f a).toFun (r := G.Adj) (s := (completeGraph α).Adj) v =
          (f b).toFun (r := G.Adj) (s := (completeGraph α).Adj) v),
      a = b
⊢ Infinite (G.Coloring α)
have have₇ : ∀ (C : G.Coloring α) (v : V),
  let f : (c : α) → G →g completeGraph α := fun (c : α) ↦
    Hom.comp (Iso.toHom (Iso.completeGraph (Equiv.swap ((C : (a : V) → α) v) c))) C;
  ∀ (a b : α) (h : f a = f b)
    (this :
      Eq.{u_2 + 1} (α := α)
        (((Equiv.swap ((C : (a : V) → α) v) a : Equiv.Perm α) : (a : α) → α) ((C : (a : V) → α) v : α) : α)
        (((Equiv.swap ((C : (a : V) → α) v) b : Equiv.Perm α) : (a : α) → α) ((C : (a : V) → α) v : α) : α)),
    a = b
Tactic: classical
  have ⟨C⟩ := ‹Nonempty <| G.Coloring α›
  have ⟨v⟩ := ‹Nonempty V›
  let f c := (Iso.completeGraph <| Equiv.swap (C v) c).toHom.comp C
  refine Infinite.of_injective f fun a b h ↦ ?_
  have := congrFun (congrArg RelHom.toFun h) v
  dsimp [f, Iso.completeGraph] at this
  grind
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring (goal)
Goal:
V : Type u
G : SimpleGraph V
⊢ G.Colorable 1 ↔ G = ⊥
have refine : G.Colorable 1 → ∀ (C : G.Coloring (Fin 1)) (u v : V) (h : G.Adj u v), False
Tactic: refine ⟨fun ⟨C⟩ ↦ eq_bot_iff_forall_not_adj.mpr fun u v h ↦ ?_, fun h ↦ h ▸ ⟨0, by simp⟩⟩