awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
rw :
  (↑(({ toFun := fun (v : Fin r × Fin t) ↦ (⟨(↑v.2 : ℕ) * r + (↑v.1 : ℕ), ⋯⟩ : Fin (r * t)),
                  invFun := fun (v : Fin (r * t)) ↦ ((⟨(↑v : ℕ) % r, ⋯⟩ : Fin r), (⟨(↑v : ℕ) / r, ⋯⟩ : Fin t)),
                  left_inv := ⋯, right_inv := ⋯ : 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 : ℕ), ⋯⟩ : Fin (r * t)),
                  invFun := fun (v : Fin (r * t)) ↦ ((⟨(↑v : ℕ) % r, ⋯⟩ : Fin r), (⟨(↑v : ℕ) / r, ⋯⟩ : Fin t)),
                  left_inv := ⋯, right_inv := ⋯ : Fin r × Fin t ≃ Fin (r * t) } :
                (a : Fin r × Fin t) → Fin (r * t))
              w) :
          ℕ) %
        r ↔
    (completeEquipartiteGraph r t).Adj v w
⊢ 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₁ : (↑(⟨(↑v.2 : ℕ) * r + (↑v.1 : ℕ), sorry⟩ : Fin (r * t)) : ℕ) % r ≠
    (↑(⟨(↑w.2 : ℕ) * r + (↑w.1 : ℕ), sorry⟩ : Fin (r * t)) : ℕ) % 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]
-- 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
rw :
  (↑(({ toFun := fun (v : Fin r × Fin t) ↦ (⟨(↑v.2 : ℕ) * r + (↑v.1 : ℕ), ⋯⟩ : Fin (r * t)),
                  invFun := fun (v : Fin (r * t)) ↦ ((⟨(↑v : ℕ) % r, ⋯⟩ : Fin r), (⟨(↑v : ℕ) / r, ⋯⟩ : Fin t)),
                  left_inv := ⋯, right_inv := ⋯ : 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 : ℕ), ⋯⟩ : Fin (r * t)),
                  invFun := fun (v : Fin (r * t)) ↦ ((⟨(↑v : ℕ) % r, ⋯⟩ : Fin r), (⟨(↑v : ℕ) / r, ⋯⟩ : Fin t)),
                  left_inv := ⋯, right_inv := ⋯ : Fin r × Fin t ≃ Fin (r * t) } :
                (a : Fin r × Fin t) → Fin (r * t))
              w) :
          ℕ) %
        r ↔
    (completeEquipartiteGraph r t).Adj v w
rw₁ :
  (↑(⟨(↑v.2 : ℕ) * r + (↑v.1 : ℕ), ⋯⟩ : Fin (r * t)) : ℕ) % r ≠
      (↑(⟨(↑w.2 : ℕ) * r + (↑w.1 : ℕ), ⋯⟩ : Fin (r * t)) : ℕ) % r ↔
    (completeEquipartiteGraph r t).Adj v w
⊢ 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₂ : (↑v.1 : ℕ) % r ≠ (↑(⟨(↑w.2 : ℕ) * r + (↑w.1 : ℕ), sorry⟩ : Fin (r * t)) : ℕ) % 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]
-- 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
rw :
  (↑(({ toFun := fun (v : Fin r × Fin t) ↦ (⟨(↑v.2 : ℕ) * r + (↑v.1 : ℕ), ⋯⟩ : Fin (r * t)),
                  invFun := fun (v : Fin (r * t)) ↦ ((⟨(↑v : ℕ) % r, ⋯⟩ : Fin r), (⟨(↑v : ℕ) / r, ⋯⟩ : Fin t)),
                  left_inv := ⋯, right_inv := ⋯ : 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 : ℕ), ⋯⟩ : Fin (r * t)),
                  invFun := fun (v : Fin (r * t)) ↦ ((⟨(↑v : ℕ) % r, ⋯⟩ : Fin r), (⟨(↑v : ℕ) / r, ⋯⟩ : Fin t)),
                  left_inv := ⋯, right_inv := ⋯ : Fin r × Fin t ≃ Fin (r * t) } :
                (a : Fin r × Fin t) → Fin (r * t))
              w) :
          ℕ) %
        r ↔
    (completeEquipartiteGraph r t).Adj v w
rw₁ :
  (↑(⟨(↑v.2 : ℕ) * r + (↑v.1 : ℕ), ⋯⟩ : Fin (r * t)) : ℕ) % r ≠
      (↑(⟨(↑w.2 : ℕ) * r + (↑w.1 : ℕ), ⋯⟩ : Fin (r * t)) : ℕ) % r ↔
    (completeEquipartiteGraph r t).Adj v w
rw₂ :
  (↑v.1 : ℕ) % r ≠ (↑(⟨(↑w.2 : ℕ) * r + (↑w.1 : ℕ), ⋯⟩ : Fin (r * t)) : ℕ) % r ↔ (completeEquipartiteGraph r t).Adj v w
⊢ 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₃ : (↑v.1 : ℕ) ≠ (↑(⟨(↑w.2 : ℕ) * r + (↑w.1 : ℕ), sorry⟩ : Fin (r * t)) : ℕ) % 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]
-- 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
rw :
  (↑(({ toFun := fun (v : Fin r × Fin t) ↦ (⟨(↑v.2 : ℕ) * r + (↑v.1 : ℕ), ⋯⟩ : Fin (r * t)),
                  invFun := fun (v : Fin (r * t)) ↦ ((⟨(↑v : ℕ) % r, ⋯⟩ : Fin r), (⟨(↑v : ℕ) / r, ⋯⟩ : Fin t)),
                  left_inv := ⋯, right_inv := ⋯ : 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 : ℕ), ⋯⟩ : Fin (r * t)),
                  invFun := fun (v : Fin (r * t)) ↦ ((⟨(↑v : ℕ) % r, ⋯⟩ : Fin r), (⟨(↑v : ℕ) / r, ⋯⟩ : Fin t)),
                  left_inv := ⋯, right_inv := ⋯ : Fin r × Fin t ≃ Fin (r * t) } :
                (a : Fin r × Fin t) → Fin (r * t))
              w) :
          ℕ) %
        r ↔
    (completeEquipartiteGraph r t).Adj v w
rw₁ :
  (↑(⟨(↑v.2 : ℕ) * r + (↑v.1 : ℕ), ⋯⟩ : Fin (r * t)) : ℕ) % r ≠
      (↑(⟨(↑w.2 : ℕ) * r + (↑w.1 : ℕ), ⋯⟩ : Fin (r * t)) : ℕ) % r ↔
    (completeEquipartiteGraph r t).Adj v w
rw₂ :
  (↑v.1 : ℕ) % r ≠ (↑(⟨(↑w.2 : ℕ) * r + (↑w.1 : ℕ), ⋯⟩ : Fin (r * t)) : ℕ) % r ↔ (completeEquipartiteGraph r t).Adj v w
rw₃ : (↑v.1 : ℕ) ≠ (↑(⟨(↑w.2 : ℕ) * r + (↑w.1 : ℕ), ⋯⟩ : Fin (r * t)) : ℕ) % r ↔ (completeEquipartiteGraph r t).Adj v w
⊢ 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₄ : (↑v.1 : ℕ) ≠ (↑w.1 : ℕ) % 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]
-- 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
rw :
  (↑(({ toFun := fun (v : Fin r × Fin t) ↦ (⟨(↑v.2 : ℕ) * r + (↑v.1 : ℕ), ⋯⟩ : Fin (r * t)),
                  invFun := fun (v : Fin (r * t)) ↦ ((⟨(↑v : ℕ) % r, ⋯⟩ : Fin r), (⟨(↑v : ℕ) / r, ⋯⟩ : Fin t)),
                  left_inv := ⋯, right_inv := ⋯ : 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 : ℕ), ⋯⟩ : Fin (r * t)),
                  invFun := fun (v : Fin (r * t)) ↦ ((⟨(↑v : ℕ) % r, ⋯⟩ : Fin r), (⟨(↑v : ℕ) / r, ⋯⟩ : Fin t)),
                  left_inv := ⋯, right_inv := ⋯ : Fin r × Fin t ≃ Fin (r * t) } :
                (a : Fin r × Fin t) → Fin (r * t))
              w) :
          ℕ) %
        r ↔
    (completeEquipartiteGraph r t).Adj v w
rw₁ :
  (↑(⟨(↑v.2 : ℕ) * r + (↑v.1 : ℕ), ⋯⟩ : Fin (r * t)) : ℕ) % r ≠
      (↑(⟨(↑w.2 : ℕ) * r + (↑w.1 : ℕ), ⋯⟩ : Fin (r * t)) : ℕ) % r ↔
    (completeEquipartiteGraph r t).Adj v w
rw₂ :
  (↑v.1 : ℕ) % r ≠ (↑(⟨(↑w.2 : ℕ) * r + (↑w.1 : ℕ), ⋯⟩ : Fin (r * t)) : ℕ) % r ↔ (completeEquipartiteGraph r t).Adj v w
rw₃ : (↑v.1 : ℕ) ≠ (↑(⟨(↑w.2 : ℕ) * r + (↑w.1 : ℕ), ⋯⟩ : Fin (r * t)) : ℕ) % r ↔ (completeEquipartiteGraph r t).Adj v w
rw₄ : (↑v.1 : ℕ) ≠ (↑w.1 : ℕ) % r ↔ (completeEquipartiteGraph r t).Adj v w
⊢ 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₅ : (↑v.1 : ℕ) ≠ (↑w.1 : ℕ) ↔ (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]
-- 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
rw :
  (↑(({ toFun := fun (v : Fin r × Fin t) ↦ (⟨(↑v.2 : ℕ) * r + (↑v.1 : ℕ), ⋯⟩ : Fin (r * t)),
                  invFun := fun (v : Fin (r * t)) ↦ ((⟨(↑v : ℕ) % r, ⋯⟩ : Fin r), (⟨(↑v : ℕ) / r, ⋯⟩ : Fin t)),
                  left_inv := ⋯, right_inv := ⋯ : 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 : ℕ), ⋯⟩ : Fin (r * t)),
                  invFun := fun (v : Fin (r * t)) ↦ ((⟨(↑v : ℕ) % r, ⋯⟩ : Fin r), (⟨(↑v : ℕ) / r, ⋯⟩ : Fin t)),
                  left_inv := ⋯, right_inv := ⋯ : Fin r × Fin t ≃ Fin (r * t) } :
                (a : Fin r × Fin t) → Fin (r * t))
              w) :
          ℕ) %
        r ↔
    (completeEquipartiteGraph r t).Adj v w
rw₁ :
  (↑(⟨(↑v.2 : ℕ) * r + (↑v.1 : ℕ), ⋯⟩ : Fin (r * t)) : ℕ) % r ≠
      (↑(⟨(↑w.2 : ℕ) * r + (↑w.1 : ℕ), ⋯⟩ : Fin (r * t)) : ℕ) % r ↔
    (completeEquipartiteGraph r t).Adj v w
rw₂ :
  (↑v.1 : ℕ) % r ≠ (↑(⟨(↑w.2 : ℕ) * r + (↑w.1 : ℕ), ⋯⟩ : Fin (r * t)) : ℕ) % r ↔ (completeEquipartiteGraph r t).Adj v w
rw₃ : (↑v.1 : ℕ) ≠ (↑(⟨(↑w.2 : ℕ) * r + (↑w.1 : ℕ), ⋯⟩ : Fin (r * t)) : ℕ) % r ↔ (completeEquipartiteGraph r t).Adj v w
rw₄ : (↑v.1 : ℕ) ≠ (↑w.1 : ℕ) % r ↔ (completeEquipartiteGraph r t).Adj v w
rw₅ : (↑v.1 : ℕ) ≠ (↑w.1 : ℕ) ↔ (completeEquipartiteGraph r t).Adj v w
⊢ 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₆ : v.1 ≠ w.1 ↔ (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]
-- 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
rw :
  (↑(({ toFun := fun (v : Fin r × Fin t) ↦ (⟨(↑v.2 : ℕ) * r + (↑v.1 : ℕ), ⋯⟩ : Fin (r * t)),
                  invFun := fun (v : Fin (r * t)) ↦ ((⟨(↑v : ℕ) % r, ⋯⟩ : Fin r), (⟨(↑v : ℕ) / r, ⋯⟩ : Fin t)),
                  left_inv := ⋯, right_inv := ⋯ : 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 : ℕ), ⋯⟩ : Fin (r * t)),
                  invFun := fun (v : Fin (r * t)) ↦ ((⟨(↑v : ℕ) % r, ⋯⟩ : Fin r), (⟨(↑v : ℕ) / r, ⋯⟩ : Fin t)),
                  left_inv := ⋯, right_inv := ⋯ : Fin r × Fin t ≃ Fin (r * t) } :
                (a : Fin r × Fin t) → Fin (r * t))
              w) :
          ℕ) %
        r ↔
    (completeEquipartiteGraph r t).Adj v w
rw₁ :
  (↑(⟨(↑v.2 : ℕ) * r + (↑v.1 : ℕ), ⋯⟩ : Fin (r * t)) : ℕ) % r ≠
      (↑(⟨(↑w.2 : ℕ) * r + (↑w.1 : ℕ), ⋯⟩ : Fin (r * t)) : ℕ) % r ↔
    (completeEquipartiteGraph r t).Adj v w
rw₂ :
  (↑v.1 : ℕ) % r ≠ (↑(⟨(↑w.2 : ℕ) * r + (↑w.1 : ℕ), ⋯⟩ : Fin (r * t)) : ℕ) % r ↔ (completeEquipartiteGraph r t).Adj v w
rw₃ : (↑v.1 : ℕ) ≠ (↑(⟨(↑w.2 : ℕ) * r + (↑w.1 : ℕ), ⋯⟩ : Fin (r * t)) : ℕ) % r ↔ (completeEquipartiteGraph r t).Adj v w
rw₄ : (↑v.1 : ℕ) ≠ (↑w.1 : ℕ) % r ↔ (completeEquipartiteGraph r t).Adj v w
rw₅ : (↑v.1 : ℕ) ≠ (↑w.1 : ℕ) ↔ (completeEquipartiteGraph r t).Adj v w
rw₆ : v.1 ≠ w.1 ↔ (completeEquipartiteGraph r t).Adj v w
⊢ 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₇ : (completeEquipartiteGraph r t).Adj v w ↔ (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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (goal)
Goal:
r t : ℕ
⊢ completeEquipartiteGraph r t = ⊥ ↔ r ≤ 1 ∨ t = 0
have contrapose! : completeEquipartiteGraph r t ≠ ⊥ ↔ 1 < r ∧ t ≠ 0
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (goal)
Goal:
r t : ℕ
⊢ completeEquipartiteGraph r t ≠ ⊥ ↔ 1 < r ∧ t ≠ 0
have rw : (completeEquipartiteGraph r t).edgeSet.Nonempty ↔ Nontrivial (Fin r) ∧ Nonempty (Fin t)
Tactic: rw [← edgeSet_nonempty, ← Nat.succ_le_iff, ← Fin.nontrivial_iff_two_le, ← Nat.pos_iff_ne_zero,
    Fin.pos_iff_nonempty]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (goal)
Goal:
r t : ℕ
⊢ (completeEquipartiteGraph r t).edgeSet.Nonempty ↔ Nontrivial (Fin r) ∧ Nonempty (Fin t)
have refine_1 : (completeEquipartiteGraph r t).edgeSet.Nonempty →
  ∀ (e : Sym2 (Fin r × Fin t)) (he : e ∈ (completeEquipartiteGraph r t).edgeSet), Nontrivial (Fin r) ∧ Nonempty (Fin t)
Tactic: refine ⟨fun ⟨e, he⟩ ↦ ?_, fun ⟨⟨i₁, i₂, hv⟩, ⟨x⟩⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (goal)
Goal:
r t : ℕ
refine_1 :
  (completeEquipartiteGraph r t).edgeSet.Nonempty →
    ∀ (e : Sym2 (Fin r × Fin t)) (he : e ∈ (completeEquipartiteGraph r t).edgeSet),
      Nontrivial (Fin r) ∧ Nonempty (Fin t)
⊢ (completeEquipartiteGraph r t).edgeSet.Nonempty ↔ Nontrivial (Fin r) ∧ Nonempty (Fin t)
have refine_2 : Nontrivial (Fin r) ∧ Nonempty (Fin t) →
  ∀ (i₁ i₂ : Fin r) (hv : i₁ ≠ i₂) (x : Fin t), (completeEquipartiteGraph r t).edgeSet.Nonempty
Tactic: refine ⟨fun ⟨e, he⟩ ↦ ?_, fun ⟨⟨i₁, i₂, hv⟩, ⟨x⟩⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (goal)
Goal:
r t : ℕ
h : (completeEquipartiteGraph r t).edgeSet.Nonempty
e : Sym2 (Fin r × Fin t)
he : e ∈ (completeEquipartiteGraph r t).edgeSet
⊢ Nontrivial (Fin r) ∧ Nonempty (Fin t)
have refine_1 : ∀ (v₁ v₂ : Fin r × Fin t) (he : s(v₁, v₂) ∈ (completeEquipartiteGraph r t).edgeSet),
  Nontrivial (Fin r) ∧ Nonempty (Fin t)
Tactic: induction e with | _ v₁ v₂
Cleared hypotheses: e, he
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (hypothesis)
Goal:
r t : ℕ
h : (completeEquipartiteGraph r t).edgeSet.Nonempty
v₁ v₂ : Fin r × Fin t
he : s(v₁, v₂) ∈ (completeEquipartiteGraph r t).edgeSet
⊢ Nontrivial (Fin r) ∧ Nonempty (Fin t)
have he₁ : v₁.1 ≠ v₂.1
Tactic: rw [mem_edgeSet, completeEquipartiteGraph_adj] at he
Cleared hypotheses: he
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (goal)
Goal:
r t : ℕ
h : Nontrivial (Fin r) ∧ Nonempty (Fin t)
i₁ i₂ : Fin r
hv : i₁ ≠ i₂
x : Fin t
⊢ (completeEquipartiteGraph r t).edgeSet.Nonempty
have h : s((i₁, x), (i₂, x)) ∈ (completeEquipartiteGraph r t).edgeSet
Tactic: use s((i₁, x), (i₂, x))
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (goal)
Goal:
r t : ℕ
h : Nontrivial (Fin r) ∧ Nonempty (Fin t)
i₁ i₂ : Fin r
hv : i₁ ≠ i₂
x : Fin t
⊢ s((i₁, x), (i₂, x)) ∈ (completeEquipartiteGraph r t).edgeSet
have h : (i₁, x).1 ≠ (i₂, x).1
Tactic: rw [mem_edgeSet, completeEquipartiteGraph_adj]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (goal)
Goal:
r t : ℕ
⊢ (completeEquipartiteGraph r t).IsCompleteMultipartite
have inl : ∀ (ht_eq0 : t = 0), (completeEquipartiteGraph r t).IsCompleteMultipartite
Tactic: rcases t.eq_zero_or_pos with ht_eq0 | ht_pos
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (goal)
Goal:
r t : ℕ
inl : ∀ (ht_eq0 : t = 0), (completeEquipartiteGraph r t).IsCompleteMultipartite
⊢ (completeEquipartiteGraph r t).IsCompleteMultipartite
have inr : ∀ (ht_pos : t > 0), (completeEquipartiteGraph r t).IsCompleteMultipartite
Tactic: rcases t.eq_zero_or_pos with ht_eq0 | ht_pos
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (goal)
Goal:
r t : ℕ
ht_eq0 : t = 0
⊢ (completeEquipartiteGraph r t).IsCompleteMultipartite
have inl : IsCompleteMultipartite (α := Fin r × Fin t) ⊥
Tactic: rw [completeEquipartiteGraph_eq_bot_iff.mpr (Or.inr ht_eq0)]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (goal)
Goal:
r t : ℕ
ht_pos : t > 0
⊢ (completeEquipartiteGraph r t).IsCompleteMultipartite
have inr : ∃ (ι : Type) (V : ι → Type) (_ : ∀ (i : ι), Nonempty (V i)),
  Nonempty (completeEquipartiteGraph r t ≃g SimpleGraph.completeMultipartiteGraph V)
Tactic: rw [isCompleteMultipartite_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (goal)
Goal:
r t : ℕ
ht_pos : t > 0
⊢ ∃ (ι : Type) (V : ι → Type) (_ : ∀ (i : ι), Nonempty (V i)),
    Nonempty (completeEquipartiteGraph r t ≃g SimpleGraph.completeMultipartiteGraph V)
have h : ∃ (_ : ∀ (i : Fin r), Nonempty (const (Fin r) (Fin t) i)),
  Nonempty
    ((completeEquipartiteGraph r t).Iso (W := (i : Fin r) × const (Fin r) (Fin t) i)
      (SimpleGraph.completeMultipartiteGraph (const (Fin r) (Fin t))))
Tactic: use (Fin r), const (Fin r) (Fin t)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (goal)
Goal:
r t : ℕ
ht_pos : t > 0
⊢ ∃ (_ : ∀ (i : Fin r), Nonempty (const (Fin r) (Fin t) i)),
    Nonempty
      ((completeEquipartiteGraph r t).Iso (W := (i : Fin r) × const (Fin r) (Fin t) i)
        (SimpleGraph.completeMultipartiteGraph (const (Fin r) (Fin t))))
have h : (∀ (i : Fin r), Nonempty (Fin t)) ∧
  Nonempty
    ((completeEquipartiteGraph r t).Iso (W := (_ : Fin r) × Fin t)
      (SimpleGraph.completeMultipartiteGraph (const (Fin r) (Fin t))))
Tactic: simp_rw [const_apply, exists_prop]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (goal)
Goal:
r t : ℕ
v : Fin r × Fin t
⊢ (completeEquipartiteGraph r t).neighborSet v = SProd.sprod (α := Set (Fin r)) (β := Set (Fin t)) {v.1}ᶜ Set.univ
have h : ∀ (x : Fin r × Fin t),
  x ∈ (completeEquipartiteGraph r t).neighborSet v ↔
    x ∈ SProd.sprod (α := Set (Fin r)) (β := Set (Fin t)) {v.1}ᶜ Set.univ
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (goal)
Goal:
r t : ℕ
v : Fin r × Fin t
⊢ (completeEquipartiteGraph r t).neighborFinset v = SProd.sprod (α := Finset (Fin r)) (β := Finset (Fin t)) {v.1}ᶜ univ
have h : ∀ (a : Fin r × Fin t),
  a ∈ (completeEquipartiteGraph r t).neighborFinset v ↔
    a ∈ SProd.sprod (α := Finset (Fin r)) (β := Finset (Fin t)) {v.1}ᶜ univ
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (goal)
Goal:
r t : ℕ
v : Fin r × Fin t
⊢ (completeEquipartiteGraph r t).degree v = (r - 1) * t
have rw : #((completeEquipartiteGraph r t).neighborFinset v) = (r - 1) * t
Tactic: rw [← card_neighborFinset_eq_degree, neighborFinset_completeEquipartiteGraph v,
    card_product, card_compl, card_singleton, Fintype.card_fin, card_univ, Fintype.card_fin]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (goal)
Goal:
r t : ℕ
v : Fin r × Fin t
rw : #((completeEquipartiteGraph r t).neighborFinset v) = (r - 1) * t
⊢ (completeEquipartiteGraph r t).degree v = (r - 1) * t
have rw₁ : #(SProd.sprod (α := Finset (Fin r)) (β := Finset (Fin t)) {v.1}ᶜ univ) = (r - 1) * t
Tactic: rw [← card_neighborFinset_eq_degree, neighborFinset_completeEquipartiteGraph v,
    card_product, card_compl, card_singleton, Fintype.card_fin, card_univ, Fintype.card_fin]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (goal)
Goal:
r t : ℕ
v : Fin r × Fin t
rw : #((completeEquipartiteGraph r t).neighborFinset v) = (r - 1) * t
rw₁ : #(SProd.sprod (α := Finset (Fin r)) (β := Finset (Fin t)) {v.1}ᶜ univ) = (r - 1) * t
⊢ (completeEquipartiteGraph r t).degree v = (r - 1) * t
have rw₂ : Finset.card (α := Fin r) {v.1}ᶜ * Finset.card (α := Fin t) univ = (r - 1) * t
Tactic: rw [← card_neighborFinset_eq_degree, neighborFinset_completeEquipartiteGraph v,
    card_product, card_compl, card_singleton, Fintype.card_fin, card_univ, Fintype.card_fin]