awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (goal)
Goal:
α : Type u
G : SimpleGraph α
⊢ G.IsCompleteMultipartite ↔
    ∃ (ι : Type u) (V : ι → Type u) (_ : ∀ (i : ι), Nonempty.{u + 1} (V i)),
      Nonempty.{u + 1} (G ≃g completeMultipartiteGraph V)
have mp : G.IsCompleteMultipartite →
  ∃ (ι : Type u) (V : ι → Type u) (_ : ∀ (i : ι), Nonempty.{u + 1} (V i)),
    Nonempty.{u + 1} (G ≃g completeMultipartiteGraph V)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (goal)
Goal:
α : Type u
G : SimpleGraph α
mp :
  G.IsCompleteMultipartite →
    ∃ (ι : Type u) (V : ι → Type u) (_ : ∀ (i : ι), Nonempty.{u + 1} (V i)),
      Nonempty.{u + 1} (G ≃g completeMultipartiteGraph V)
⊢ G.IsCompleteMultipartite ↔
    ∃ (ι : Type u) (V : ι → Type u) (_ : ∀ (i : ι), Nonempty.{u + 1} (V i)),
      Nonempty.{u + 1} (G ≃g completeMultipartiteGraph V)
have mpr : (∃ (ι : Type u) (V : ι → Type u) (_ : ∀ (i : ι), Nonempty.{u + 1} (V i)),
    Nonempty.{u + 1} (G ≃g completeMultipartiteGraph V)) →
  G.IsCompleteMultipartite
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (goal)
Goal:
α : Type u
G : SimpleGraph α
h :
  ∃ (ι : Type u) (V : ι → Type u) (_ : ∀ (i : ι), Nonempty.{u + 1} (V i)),
    Nonempty.{u + 1} (G ≃g completeMultipartiteGraph V)
⊢ G.IsCompleteMultipartite
have mpr : ∀ (w : Type u) (w_1 : w → Type u),
  (∀ (i : w), Nonempty.{u + 1} (w_1 i)) → ∀ (e : G ≃g completeMultipartiteGraph w_1), G.IsCompleteMultipartite
Tactic: obtain ⟨_, _, _, ⟨e⟩⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (goal)
Goal:
α : Type u
G : SimpleGraph α
w : Type u
w_1 : w → Type u
w_2 : ∀ (i : w), Nonempty.{u + 1} (w_1 i)
e : G ≃g completeMultipartiteGraph w_1
⊢ G.IsCompleteMultipartite
have mpr : ∀ (x x_1 x_2 : α) (h1 : ¬G.Adj x x_1) (h2 : ¬G.Adj x_1 x_2), ¬G.Adj x x_2
Tactic: refine ⟨fun _ _ _ h1 h2 ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (goal)
Goal:
α : Type u
G : SimpleGraph α
w : Type u
w_1 : w → Type u
w_2 : ∀ (i : w), Nonempty.{u + 1} (w_1 i)
e : G ≃g completeMultipartiteGraph w_1
x x_1 x_2 : α
h1 : ¬G.Adj x x_1
h2 : ¬G.Adj x_1 x_2
⊢ ¬G.Adj x x_2
have mpr : ∀ (h1 : ¬(completeMultipartiteGraph w_1).Adj ((e : (a : α) → (i : w) × w_1 i) x) ((e : (a : α) → (i : w) × w_1 i) x_1))
  (h2 :
    ¬(completeMultipartiteGraph w_1).Adj ((e : (a : α) → (i : w) × w_1 i) x_1) ((e : (a : α) → (i : w) × w_1 i) x_2)),
  ¬(completeMultipartiteGraph w_1).Adj ((e : (a : α) → (i : w) × w_1 i) x) ((e : (a : α) → (i : w) × w_1 i) x_2)
Tactic: rw [← e.map_rel_iff] at *
Cleared hypotheses: h1, h2
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (hypothesis)
Goal:
α : Type u
G : SimpleGraph α
v w₁ w₂ : α
h : G.IsPathGraph3Compl v w₁ w₂
⊢ G.IsPathGraph3Compl v w₂ w₁
have h1 : G.Adj w₁ w₂
Tactic: obtain ⟨h1, h2, h3⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (hypothesis)
Goal:
α : Type u
G : SimpleGraph α
v w₁ w₂ : α
h : G.IsPathGraph3Compl v w₁ w₂
h1 : G.Adj w₁ w₂
⊢ G.IsPathGraph3Compl v w₂ w₁
have h2 : ¬G.Adj v w₁
Tactic: obtain ⟨h1, h2, h3⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (hypothesis)
Goal:
α : Type u
G : SimpleGraph α
v w₁ w₂ : α
h : G.IsPathGraph3Compl v w₁ w₂
h1 : G.Adj w₁ w₂
h2 : ¬G.Adj v w₁
⊢ G.IsPathGraph3Compl v w₂ w₁
have h3 : ¬G.Adj v w₂
Tactic: obtain ⟨h1, h2, h3⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (hypothesis)
Goal:
α : Type u
G : SimpleGraph α
h : ¬G.IsCompleteMultipartite
⊢ ∃ (v : α) (w₁ : α) (w₂ : α), G.IsPathGraph3Compl v w₁ w₂
have h₁ : ¬∀ (a b c : α), ¬G.Adj a b → ¬G.Adj b c → ¬G.Adj a c
Tactic: apply mt IsTrans.mk at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (hypothesis)
Goal:
α : Type u
G : SimpleGraph α
h : ¬∀ (a b c : α), ¬G.Adj a b → ¬G.Adj b c → ¬G.Adj a c
⊢ ∃ (v : α) (w₁ : α) (w₂ : α), G.IsPathGraph3Compl v w₁ w₂
have h₁ : ∃ (a : α) (b : α) (c : α), ¬G.Adj a b ∧ ¬G.Adj b c ∧ G.Adj a c
Tactic: push Not at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (goal)
Goal:
α : Type u
G : SimpleGraph α
h : ∃ (a : α) (b : α) (c : α), ¬G.Adj a b ∧ ¬G.Adj b c ∧ G.Adj a c
⊢ ∃ (v : α) (w₁ : α) (w₂ : α), G.IsPathGraph3Compl v w₁ w₂
have obtain : ∀ (w w_1 w_2 : α) (h1 : ¬G.Adj w w_1) (h2 : ¬G.Adj w_1 w_2) (h3 : G.Adj w w_2),
  ∃ (v : α) (w₁ : α) (w₂ : α), G.IsPathGraph3Compl v w₁ w₂
Tactic: obtain ⟨_, _, _, h1, h2, h3⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (hypothesis)
Goal:
α : Type u
G : SimpleGraph α
w w_1 w_2 : α
h1 : ¬G.Adj w w_1
h2 : ¬G.Adj w_1 w_2
h3 : G.Adj w w_2
⊢ ∃ (v : α) (w₁ : α) (w₂ : α), G.IsPathGraph3Compl v w₁ w₂
have h1₁ : ¬G.Adj w_1 w
Tactic: rw [adj_comm] at h1
Cleared hypotheses: h1, h2, h3
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (goal)
Goal:
α : Type u
G : SimpleGraph α
h_1 : ∃ (v : α) (w₁ : α) (w₂ : α), G.IsPathGraph3Compl v w₁ w₂
w w_1 w_2 : α
h1 : G.Adj w_1 w_2
h2 : ¬G.Adj w w_1
h3 : ¬G.Adj w w_2
h : G.IsCompleteMultipartite
⊢ ¬G.Adj w_1 w
have rwa : ∀ (h2 : ¬G.Adj w_1 w) (h3 : ¬G.Adj w w_2) (h : G.IsCompleteMultipartite), ¬G.Adj w_1 w
Tactic: rwa [adj_comm] at h2
Cleared hypotheses: h2, h3, h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (hypothesis)
Goal:
α : Type u
G : SimpleGraph α
s : Set α
v w₁ w₂ : α
h : G.IsPathGraph3Compl v w₁ w₂
a₁ a₂ : Fin 3
h_1 :
  Eq.{u + 1} (α := α)
    ((fun (x : Fin 3) ↦
        (match (motive := Fin 3 → α) x with
          | 0 => w₁
          | 1 => v
          | 2 => w₂ :
          α))
      a₁)
    ((fun (x : Fin 3) ↦
        (match (motive := Fin 3 → α) x with
          | 0 => w₁
          | 1 => v
          | 2 => w₂ :
          α))
      a₂)
⊢ a₁ = a₂
have this : v ≠ w₁
Tactic: have := h.ne_fst
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (hypothesis)
Goal:
α : Type u
G : SimpleGraph α
s : Set α
v w₁ w₂ : α
h : G.IsPathGraph3Compl v w₁ w₂
a₁ a₂ : Fin 3
h_1 :
  Eq.{u + 1} (α := α)
    ((fun (x : Fin 3) ↦
        (match (motive := Fin 3 → α) x with
          | 0 => w₁
          | 1 => v
          | 2 => w₂ :
          α))
      a₁)
    ((fun (x : Fin 3) ↦
        (match (motive := Fin 3 → α) x with
          | 0 => w₁
          | 1 => v
          | 2 => w₂ :
          α))
      a₂)
this : v ≠ w₁
⊢ a₁ = a₂
have this₁ : v ≠ w₂
Tactic: have := h.ne_snd
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (hypothesis)
Goal:
α : Type u
G : SimpleGraph α
s : Set α
v w₁ w₂ : α
h : G.IsPathGraph3Compl v w₁ w₂
a₁ a₂ : Fin 3
h_1 :
  Eq.{u + 1} (α := α)
    ((fun (x : Fin 3) ↦
        (match (motive := Fin 3 → α) x with
          | 0 => w₁
          | 1 => v
          | 2 => w₂ :
          α))
      a₁)
    ((fun (x : Fin 3) ↦
        (match (motive := Fin 3 → α) x with
          | 0 => w₁
          | 1 => v
          | 2 => w₂ :
          α))
      a₂)
this_1 : v ≠ w₁
this : v ≠ w₂
⊢ a₁ = a₂
have this₁ : w₁ ≠ w₂
Tactic: have := h.adj.ne
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (goal)
Goal:
α : Type u
G : SimpleGraph α
s : Set α
v w₁ w₂ : α
h : G.IsPathGraph3Compl v w₁ w₂
a b : Fin 3
⊢ G.Adj
      (({
            toFun := fun (x : Fin 3) ↦
              match (motive := Fin 3 → α) x with
              | 0 => w₁
              | 1 => v
              | 2 => w₂,
            inj' := ⋯ : Fin 3 ↪ α } :
          (a : Fin 3) → α)
        a)
      (({
            toFun := fun (x : Fin 3) ↦
              match (motive := Fin 3 → α) x with
              | 0 => w₁
              | 1 => v
              | 2 => w₂,
            inj' := ⋯ : Fin 3 ↪ α } :
          (a : Fin 3) → α)
        b) ↔
    Adj (pathGraph 3)ᶜ a b
have simp_rw : G.Adj
    (match (motive := Fin 3 → α) a with
    | 0 => w₁
    | 1 => v
    | 2 => w₂)
    (match (motive := Fin 3 → α) b with
    | 0 => w₁
    | 1 => v
    | 2 => w₂) ↔
  ¬a = b ∧ ¬(↑a : ℕ) + 1 = (↑b : ℕ) ∧ ¬(↑b : ℕ) + 1 = (↑a : ℕ)
Tactic: simp_rw [Embedding.coeFn_mk, compl_adj, ne_eq, pathGraph_adj, not_or]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (hypothesis)
Goal:
α : Type u
G : SimpleGraph α
s : Set α
v w₁ w₂ : α
h : G.IsPathGraph3Compl v w₁ w₂
a b : Fin 3
⊢ G.Adj
      (match (motive := Fin 3 → α) a with
      | 0 => w₁
      | 1 => v
      | 2 => w₂)
      (match (motive := Fin 3 → α) b with
      | 0 => w₁
      | 1 => v
      | 2 => w₂) ↔
    ¬a = b ∧ ¬(↑a : ℕ) + 1 = (↑b : ℕ) ∧ ¬(↑b : ℕ) + 1 = (↑a : ℕ)
have this : G.Adj w₁ w₂
Tactic: have := h.adj
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (hypothesis)
Goal:
α : Type u
G : SimpleGraph α
s : Set α
v w₁ w₂ : α
h : G.IsPathGraph3Compl v w₁ w₂
a b : Fin 3
this : G.Adj w₁ w₂
⊢ G.Adj
      (match (motive := Fin 3 → α) a with
      | 0 => w₁
      | 1 => v
      | 2 => w₂)
      (match (motive := Fin 3 → α) b with
      | 0 => w₁
      | 1 => v
      | 2 => w₂) ↔
    ¬a = b ∧ ¬(↑a : ℕ) + 1 = (↑b : ℕ) ∧ ¬(↑b : ℕ) + 1 = (↑a : ℕ)
have this₁ : G.Adj w₂ w₁
Tactic: have := h.adj.symm
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (hypothesis)
Goal:
α : Type u
G : SimpleGraph α
s : Set α
v w₁ w₂ : α
h : G.IsPathGraph3Compl v w₁ w₂
a b : Fin 3
this_1 : G.Adj w₁ w₂
this : G.Adj w₂ w₁
⊢ G.Adj
      (match (motive := Fin 3 → α) a with
      | 0 => w₁
      | 1 => v
      | 2 => w₂)
      (match (motive := Fin 3 → α) b with
      | 0 => w₁
      | 1 => v
      | 2 => w₂) ↔
    ¬a = b ∧ ¬(↑a : ℕ) + 1 = (↑b : ℕ) ∧ ¬(↑b : ℕ) + 1 = (↑a : ℕ)
have h1 : ¬G.Adj v w₁
Tactic: have h1 := h.not_adj_fst
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (hypothesis)
Goal:
α : Type u
G : SimpleGraph α
s : Set α
v w₁ w₂ : α
h : G.IsPathGraph3Compl v w₁ w₂
a b : Fin 3
this_1 : G.Adj w₁ w₂
this : G.Adj w₂ w₁
h1 : ¬G.Adj v w₁
⊢ G.Adj
      (match (motive := Fin 3 → α) a with
      | 0 => w₁
      | 1 => v
      | 2 => w₂)
      (match (motive := Fin 3 → α) b with
      | 0 => w₁
      | 1 => v
      | 2 => w₂) ↔
    ¬a = b ∧ ¬(↑a : ℕ) + 1 = (↑b : ℕ) ∧ ¬(↑b : ℕ) + 1 = (↑a : ℕ)
have h2 : ¬G.Adj v w₂
Tactic: have h2 := h.not_adj_snd
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (hypothesis)
Goal:
α : Type u
G : SimpleGraph α
s : Set α
v w₁ w₂ : α
h : G.IsPathGraph3Compl v w₁ w₂
a b : Fin 3
this_1 : G.Adj w₁ w₂
this : G.Adj w₂ w₁
h1 : ¬G.Adj v w₁
h2 : ¬G.Adj v w₂
⊢ ¬G.Adj w₁ v ∧ ¬G.Adj w₂ v
have h1₁ : ¬G.Adj w₁ v
Tactic: rw [adj_comm] at h1 h2
Cleared hypotheses: h1, h2
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (hypothesis)
Goal:
α : Type u
G : SimpleGraph α
s : Set α
v w₁ w₂ : α
h : G.IsPathGraph3Compl v w₁ w₂
a b : Fin 3
this_1 : G.Adj w₁ w₂
this : G.Adj w₂ w₁
h1 : ¬G.Adj v w₁
h2 : ¬G.Adj v w₂
h1₁ : ¬G.Adj w₁ v
⊢ ¬G.Adj w₁ v ∧ ¬G.Adj w₂ v
have h2₁ : ¬G.Adj w₂ v
Tactic: rw [adj_comm] at h1 h2
Cleared hypotheses: h1, h2
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (hypothesis)
Goal:
α : Type u
G : SimpleGraph α
s : Set α
v w₁ w₂ : α
h : G.IsPathGraph3Compl v w₁ w₂
a b : Fin 3
this_1 : G.Adj w₁ w₂
this : G.Adj w₂ w₁
h1 : ¬G.Adj v w₁
h2 : ¬G.Adj v w₂
⊢ G.Adj
      (match (motive := Fin 3 → α) a with
      | 0 => w₁
      | 1 => v
      | 2 => w₂)
      (match (motive := Fin 3 → α) b with
      | 0 => w₁
      | 1 => v
      | 2 => w₂) ↔
    ¬a = b ∧ ¬(↑a : ℕ) + 1 = (↑b : ℕ) ∧ ¬(↑b : ℕ) + 1 = (↑a : ℕ)
have left : ¬G.Adj w₁ v
Tactic: have ⟨_, _⟩ : ¬ G.Adj w₁ v ∧ ¬ G.Adj w₂ v := by rw [adj_comm] at h1 h2; exact ⟨h1, h2⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (hypothesis)
Goal:
α : Type u
G : SimpleGraph α
s : Set α
v w₁ w₂ : α
h : G.IsPathGraph3Compl v w₁ w₂
a b : Fin 3
this_1 : G.Adj w₁ w₂
this : G.Adj w₂ w₁
h1 : ¬G.Adj v w₁
h2 : ¬G.Adj v w₂
left : ¬G.Adj w₁ v
⊢ G.Adj
      (match (motive := Fin 3 → α) a with
      | 0 => w₁
      | 1 => v
      | 2 => w₂)
      (match (motive := Fin 3 → α) b with
      | 0 => w₁
      | 1 => v
      | 2 => w₂) ↔
    ¬a = b ∧ ¬(↑a : ℕ) + 1 = (↑b : ℕ) ∧ ¬(↑b : ℕ) + 1 = (↑a : ℕ)
have right : ¬G.Adj w₂ v
Tactic: have ⟨_, _⟩ : ¬ G.Adj w₁ v ∧ ¬ G.Adj w₂ v := by rw [adj_comm] at h1 h2; exact ⟨h1, h2⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (hypothesis)
Goal:
α : Type u
G : SimpleGraph α
e : Embedding (V := Fin 3) (pathGraph 3)ᶜ G
h : G.IsCompleteMultipartite
⊢ False
have h0 : ¬G.Adj ((e : (a : Fin 3) → α) 0) ((e : (a : Fin 3) → α) 1)
Tactic: have h0 : ¬ G.Adj (e 0) (e 1) := by simp [pathGraph_adj]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (hypothesis)
Goal:
α : Type u
G : SimpleGraph α
e : Embedding (V := Fin 3) (pathGraph 3)ᶜ G
h : G.IsCompleteMultipartite
h0 : ¬G.Adj ((e : (a : Fin 3) → α) 0) ((e : (a : Fin 3) → α) 1)
⊢ False
have h1 : ¬G.Adj ((e : (a : Fin 3) → α) 1) ((e : (a : Fin 3) → α) 2)
Tactic: have h1 : ¬ G.Adj (e 1) (e 2) := by simp [pathGraph_adj]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (hypothesis)
Goal:
α : Type u
G : SimpleGraph α
e : Embedding (V := Fin 3) (pathGraph 3)ᶜ G
h : G.IsCompleteMultipartite
h0 : ¬G.Adj ((e : (a : Fin 3) → α) 0) ((e : (a : Fin 3) → α) 1)
h1 : ¬G.Adj ((e : (a : Fin 3) → α) 1) ((e : (a : Fin 3) → α) 2)
⊢ False
have h2 : G.Adj ((e : (a : Fin 3) → α) 0) ((e : (a : Fin 3) → α) 2)
Tactic: have h2 : G.Adj (e 0) (e 2) := by simp [pathGraph_adj]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (goal)
Goal:
α : Type u
G : SimpleGraph α
β : Type u_1
H : SimpleGraph β
f : H ↪g G
h : G.IsCompleteMultipartite
⊢ H.IsCompleteMultipartite
have contrapose : ∀ (h : ¬H.IsCompleteMultipartite), ¬G.IsCompleteMultipartite
Tactic: contrapose h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (goal)
Goal:
α : Type u
G : SimpleGraph α
s : Set α
r t : ℕ
⊢ Fin r × Fin t → Fin (r * t)
have refine : ∀ (v : Fin r × Fin t), (↑v.2 : ℕ) * r + (↑v.1 : ℕ) < r * t
Tactic: refine fun v ↦ ⟨v.2 * r + v.1, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (goal)
Goal:
α : Type u
G : SimpleGraph α
s : Set α
r t : ℕ
v : Fin r × Fin t
| r * t
have rw : (t - 1) * r + r
Tactic: rw [← Nat.sub_one_add_one_eq_of_pos v.2.pos, Nat.mul_add_one, mul_comm r (t - 1)]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (goal)
Goal:
α : Type u
G : SimpleGraph α
s : Set α
r t : ℕ
v : Fin r × Fin t
⊢ (↑v.2 : ℕ) * r + (↑v.1 : ℕ) < r * t
have conv_rhs : (↑v.2 : ℕ) * r + (↑v.1 : ℕ) < (t - 1) * r + r
Tactic: conv_rhs =>
      rw [← Nat.sub_one_add_one_eq_of_pos v.2.pos, Nat.mul_add_one, mul_comm r (t - 1)]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (goal)
Goal:
α : Type u
G : SimpleGraph α
s : Set α
r t : ℕ
⊢ Fin (r * t) → Fin r × Fin t
have refine_1 : ∀ (v : Fin (r * t)), (↑v : ℕ) % r < r
Tactic: refine fun v ↦ (⟨v % r, ?_⟩, ⟨v / r, ?_⟩)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (goal)
Goal:
α : Type u
G : SimpleGraph α
s : Set α
r t : ℕ
refine_1 : ∀ (v : Fin (r * t)), (↑v : ℕ) % r < r
⊢ Fin (r * t) → Fin r × Fin t
have refine_2 : ∀ (v : Fin (r * t)), (↑v : ℕ) / r < t
Tactic: refine fun v ↦ (⟨v % r, ?_⟩, ⟨v / r, ?_⟩)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (hypothesis)
Goal:
α : Type u
G : SimpleGraph α
s : Set α
r t : ℕ
v : Fin (r * t)
⊢ (↑v : ℕ) % r < r
have hr : 0 < r
Tactic: have ⟨hr, _⟩ := CanonicallyOrderedAdd.mul_pos.mp v.pos
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (hypothesis)
Goal:
α : Type u
G : SimpleGraph α
s : Set α
r t : ℕ
v : Fin (r * t)
hr : 0 < r
⊢ (↑v : ℕ) % r < r
have right : 0 < t
Tactic: have ⟨hr, _⟩ := CanonicallyOrderedAdd.mul_pos.mp v.pos
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (goal)
Goal:
α : Type u
G : SimpleGraph α
s : Set α
r t : ℕ
v : Fin r × Fin t
⊢ (⟨(↑(⟨(↑v.2 : ℕ) * r + (↑v.1 : ℕ), ⋯⟩ : Fin (r * t)) : ℕ) % r, ⋯⟩,
      ⟨(↑(⟨(↑v.2 : ℕ) * r + (↑v.1 : ℕ), ⋯⟩ : Fin (r * t)) : ℕ) / r, ⋯⟩) =
    v
have refine_1 : (↑((⟨(↑(⟨(↑v.2 : ℕ) * r + (↑v.1 : ℕ), sorry⟩ : Fin (r * t)) : ℕ) % r, sorry⟩ : Fin r),
          (⟨(↑(⟨(↑v.2 : ℕ) * r + (↑v.1 : ℕ), sorry⟩ : Fin (r * t)) : ℕ) / r, sorry⟩ : Fin t)).1 :
    ℕ) =
  (↑v.1 : ℕ)
Tactic: refine Prod.ext (Fin.ext ?_) (Fin.ext ?_)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (goal)
Goal:
α : Type u
G : SimpleGraph α
s : Set α
r t : ℕ
v : Fin r × Fin t
refine_1 :
  (↑((⟨(↑(⟨(↑v.2 : ℕ) * r + (↑v.1 : ℕ), ⋯⟩ : Fin (r * t)) : ℕ) % r, ⋯⟩ : Fin r),
            (⟨(↑(⟨(↑v.2 : ℕ) * r + (↑v.1 : ℕ), ⋯⟩ : Fin (r * t)) : ℕ) / r, ⋯⟩ : Fin t)).1 :
      ℕ) =
    (↑v.1 : ℕ)
⊢ (⟨(↑(⟨(↑v.2 : ℕ) * r + (↑v.1 : ℕ), ⋯⟩ : Fin (r * t)) : ℕ) % r, ⋯⟩,
      ⟨(↑(⟨(↑v.2 : ℕ) * r + (↑v.1 : ℕ), ⋯⟩ : Fin (r * t)) : ℕ) / r, ⋯⟩) =
    v
have refine_2 : (↑((⟨(↑(⟨(↑v.2 : ℕ) * r + (↑v.1 : ℕ), sorry⟩ : Fin (r * t)) : ℕ) % r, sorry⟩ : Fin r),
          (⟨(↑(⟨(↑v.2 : ℕ) * r + (↑v.1 : ℕ), sorry⟩ : Fin (r * t)) : ℕ) / r, sorry⟩ : Fin t)).2 :
    ℕ) =
  (↑v.2 : ℕ)
Tactic: refine Prod.ext (Fin.ext ?_) (Fin.ext ?_)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (goal)
Goal:
α : Type u
G : SimpleGraph α
s : Set α
r t : ℕ
v : Fin r × Fin t
| (↑((⟨(↑(⟨(↑v.2 : ℕ) * r + (↑v.1 : ℕ), ⋯⟩ : Fin (r * t)) : ℕ) % r, ⋯⟩ : Fin r),
            (⟨(↑(⟨(↑v.2 : ℕ) * r + (↑v.1 : ℕ), ⋯⟩ : Fin (r * t)) : ℕ) / r, ⋯⟩ : Fin t)).1 :
      ℕ) =
    (↑v.1 : ℕ)
have enter : (↑(⟨(↑v.2 : ℕ) * r + (↑v.1 : ℕ), sorry⟩ : Fin (r * t)) : ℕ) % r
Tactic: enter [1, 1, 1, 1, 1]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (goal)
Goal:
α : Type u
G : SimpleGraph α
s : Set α
r t : ℕ
v : Fin r × Fin t
| (↑(⟨(↑v.2 : ℕ) * r + (↑v.1 : ℕ), ⋯⟩ : Fin (r * t)) : ℕ) % r
have rw : (↑v.1 : ℕ) % r
Tactic: rw [Nat.mul_add_mod_self_right]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (goal)
Goal:
α : Type u
G : SimpleGraph α
s : Set α
r t : ℕ
v : Fin r × Fin t
| (↑((⟨(↑(⟨(↑v.2 : ℕ) * r + (↑v.1 : ℕ), ⋯⟩ : Fin (r * t)) : ℕ) % r, ⋯⟩ : Fin r),
            (⟨(↑(⟨(↑v.2 : ℕ) * r + (↑v.1 : ℕ), ⋯⟩ : Fin (r * t)) : ℕ) / r, ⋯⟩ : Fin t)).1 :
      ℕ) =
    (↑v.1 : ℕ)
have enter : (↑v.1 : ℕ) % r
Tactic: enter [1, 1, 1, 1, 1]
        rw [Nat.mul_add_mod_self_right]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (goal)
Goal:
α : Type u
G : SimpleGraph α
s : Set α
r t : ℕ
v : Fin r × Fin t
⊢ (↑((⟨(↑(⟨(↑v.2 : ℕ) * r + (↑v.1 : ℕ), ⋯⟩ : Fin (r * t)) : ℕ) % r, ⋯⟩ : Fin r),
            (⟨(↑(⟨(↑v.2 : ℕ) * r + (↑v.1 : ℕ), ⋯⟩ : Fin (r * t)) : ℕ) / r, ⋯⟩ : Fin t)).1 :
      ℕ) =
    (↑v.1 : ℕ)
have refine_1 : (↑((⟨(↑v.1 : ℕ) % r, sorry⟩ : Fin r), (⟨(↑(⟨(↑v.2 : ℕ) * r + (↑v.1 : ℕ), sorry⟩ : Fin (r * t)) : ℕ) / r, sorry⟩ : Fin t)).1 : ℕ) =
  (↑v.1 : ℕ)
Tactic: conv =>
        enter [1, 1, 1, 1, 1]
        rw [Nat.mul_add_mod_self_right]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (goal)
Goal:
α : Type u
G : SimpleGraph α
s : Set α
r t : ℕ
v : Fin r × Fin t
⊢ (↑((⟨(↑(⟨(↑v.2 : ℕ) * r + (↑v.1 : ℕ), ⋯⟩ : Fin (r * t)) : ℕ) % r, ⋯⟩ : Fin r),
            (⟨(↑(⟨(↑v.2 : ℕ) * r + (↑v.1 : ℕ), ⋯⟩ : Fin (r * t)) : ℕ) / r, ⋯⟩ : Fin t)).2 :
      ℕ) =
    (↑v.2 : ℕ)
have refine_2 : (↑((⟨(↑(⟨(↑v.2 : ℕ) * r + (↑v.1 : ℕ), sorry⟩ : Fin (r * t)) : ℕ) % r, sorry⟩ : Fin r),
          (⟨(↑(⟨(↑v.2 : ℕ) * r + (↑v.1 : ℕ), sorry⟩ : Fin (r * t)) : ℕ) / r, sorry⟩ : Fin t)).2 :
    ℕ) ≤
  (↑v.2 : ℕ)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (goal)
Goal:
α : Type u
G : SimpleGraph α
s : Set α
r t : ℕ
v : Fin r × Fin t
refine_2 :
  (↑((⟨(↑(⟨(↑v.2 : ℕ) * r + (↑v.1 : ℕ), ⋯⟩ : Fin (r * t)) : ℕ) % r, ⋯⟩ : Fin r),
            (⟨(↑(⟨(↑v.2 : ℕ) * r + (↑v.1 : ℕ), ⋯⟩ : Fin (r * t)) : ℕ) / r, ⋯⟩ : Fin t)).2 :
      ℕ) ≤
    (↑v.2 : ℕ)
⊢ (↑((⟨(↑(⟨(↑v.2 : ℕ) * r + (↑v.1 : ℕ), ⋯⟩ : Fin (r * t)) : ℕ) % r, ⋯⟩ : Fin r),
            (⟨(↑(⟨(↑v.2 : ℕ) * r + (↑v.1 : ℕ), ⋯⟩ : Fin (r * t)) : ℕ) / r, ⋯⟩ : Fin t)).2 :
      ℕ) =
    (↑v.2 : ℕ)
have refine_2₁ : (↑v.2 : ℕ) ≤
  (↑(⟨(↑(⟨(↑v.2 : ℕ) * r + (↑v.1 : ℕ), sorry⟩ : Fin (r * t)) : ℕ) % r, sorry⟩,
          ⟨(↑(⟨(↑v.2 : ℕ) * r + (↑v.1 : ℕ), sorry⟩ : Fin (r * t)) : ℕ) / r, sorry⟩).2 :
    ℕ)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (goal)
Goal:
α : Type u
G : SimpleGraph α
s : Set α
r t : ℕ
v : Fin r × Fin t
⊢ (↑((⟨(↑(⟨(↑v.2 : ℕ) * r + (↑v.1 : ℕ), ⋯⟩ : Fin (r * t)) : ℕ) % r, ⋯⟩ : Fin r),
            (⟨(↑(⟨(↑v.2 : ℕ) * r + (↑v.1 : ℕ), ⋯⟩ : Fin (r * t)) : ℕ) / r, ⋯⟩ : Fin t)).2 :
      ℕ) ≤
    (↑v.2 : ℕ)
have refine_2 : (↑(⟨(↑v.2 : ℕ) * r + (↑v.1 : ℕ), sorry⟩ : Fin (r * t)) : ℕ) ≤ (↑v.2 : ℕ) * r + (r - 1)
Tactic: rw [Nat.div_le_iff_le_mul_add_pred v.1.pos, mul_comm r ↑v.2]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (goal)
Goal:
α : Type u
G : SimpleGraph α
s : Set α
r t : ℕ
v : Fin r × Fin t
⊢ (↑v.2 : ℕ) ≤
    (↑(⟨(↑(⟨(↑v.2 : ℕ) * r + (↑v.1 : ℕ), ⋯⟩ : Fin (r * t)) : ℕ) % r, ⋯⟩,
            ⟨(↑(⟨(↑v.2 : ℕ) * r + (↑v.1 : ℕ), ⋯⟩ : Fin (r * t)) : ℕ) / r, ⋯⟩).2 :
      ℕ)
have refine_2 : (↑v.2 : ℕ) * r ≤ (↑⟨(↑v.2 : ℕ) * r + (↑v.1 : ℕ), sorry⟩ : ℕ)
Tactic: rw [Nat.le_div_iff_mul_le v.1.pos]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (goal)
Goal:
α : Type u
G : SimpleGraph α
s : Set α
r t : ℕ
v w : Fin r × Fin t
⊢ Adj (V := Fin (r * t)) (SimpleGraph.turanGraph (r * t) r)
      (({ toFun := fun (v : Fin r × Fin t) ↦ ⟨(↑v.2 : ℕ) * r + (↑v.1 : ℕ), ⋯⟩,
            invFun := fun (v : Fin (r * t)) ↦ (⟨(↑v : ℕ) % r, ⋯⟩, ⟨(↑v : ℕ) / r, ⋯⟩), left_inv := ⋯, right_inv := ⋯ } :
          (a : Fin r × Fin t) → Fin (r * t))
        v)
      (({ toFun := fun (v : Fin r × Fin t) ↦ ⟨(↑v.2 : ℕ) * r + (↑v.1 : ℕ), ⋯⟩,
            invFun := fun (v : Fin (r * t)) ↦ (⟨(↑v : ℕ) % r, ⋯⟩, ⟨(↑v : ℕ) / r, ⋯⟩), left_inv := ⋯, right_inv := ⋯ } :
          (a : Fin r × Fin t) → Fin (r * t))
        w) ↔
    (completeEquipartiteGraph r t).Adj v w
have rw : (↑(({ toFun := fun (v : Fin r × Fin t) ↦ (⟨(↑v.2 : ℕ) * r + (↑v.1 : ℕ), sorry⟩ : Fin (r * t)),
                invFun := fun (v : Fin (r * t)) ↦ ((⟨(↑v : ℕ) % r, sorry⟩ : Fin r), (⟨(↑v : ℕ) / r, sorry⟩ : Fin t)),
                left_inv := sorry, right_inv := sorry : Fin r × Fin t ≃ Fin (r * t) } :
              (a : Fin r × Fin t) → Fin (r * t))
            v) :
        ℕ) %
      r ≠
    (↑(({ toFun := fun (v : Fin r × Fin t) ↦ (⟨(↑v.2 : ℕ) * r + (↑v.1 : ℕ), sorry⟩ : Fin (r * t)),
                invFun := fun (v : Fin (r * t)) ↦ ((⟨(↑v : ℕ) % r, sorry⟩ : Fin r), (⟨(↑v : ℕ) / r, sorry⟩ : Fin t)),
                left_inv := sorry, right_inv := sorry : Fin r × Fin t ≃ Fin (r * t) } :
              (a : Fin r × Fin t) → Fin (r * t))
            w) :
        ℕ) %
      r ↔
  (completeEquipartiteGraph r t).Adj v w
Tactic: rw [turanGraph_adj, Equiv.coe_fn_mk, Nat.mul_add_mod_self_right, Nat.mod_eq_of_lt v.1.prop,
      Nat.mul_add_mod_self_right, Nat.mod_eq_of_lt w.1.prop, ← Fin.ext_iff.ne,
      ← completeEquipartiteGraph_adj]