awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G : SimpleGraph α
s : Set α
r t : ℕ
v : Fin r × Fin t
conv_rhs : (↑v.2 : ℕ) * r + (↑v.1 : ℕ) < (t - 1) * r + r
⊢ (↑v.2 : ℕ) * r + (↑v.1 : ℕ) < r * t

Tactic:
conv_rhs =>
      rw [← Nat.sub_one_add_one_eq_of_pos v.2.pos, Nat.mul_add_one, mul_comm r (t - 1)]

Premises used: HSub.hSub, Fin.pos, Nat.sub_one_add_one_eq_of_pos, mul_comm, Nat.mul_add_one, OfNat.ofNat, Prod.snd
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G : SimpleGraph α
s : Set α
r t : ℕ
v : Fin r × Fin t
⊢ (↑v.2 : ℕ) * r + (↑v.1 : ℕ) < (t - 1) * r + r

Tactic:
add_lt_add_of_le_of_lt (Nat.mul_le_mul_right r (Nat.le_pred_of_lt v.2.prop)) v.1.prop

Premises used: add_lt_add_of_le_of_lt, Nat.mul_le_mul_right, Fin.prop, Prod.fst, Nat.le_pred_of_lt, Prod.snd
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G : SimpleGraph α
s : Set α
r t : ℕ
v : Fin r × Fin t
⊢ (↑v.2 : ℕ) * r + (↑v.1 : ℕ) < (t - 1) * r + r

Tactic:
exact add_lt_add_of_le_of_lt (Nat.mul_le_mul_right r (Nat.le_pred_of_lt v.2.prop)) v.1.prop

Premises used: add_lt_add_of_le_of_lt, Nat.mul_le_mul_right, Fin.prop, Prod.fst, Nat.le_pred_of_lt, Prod.snd
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G : SimpleGraph α
s : Set α
r t : ℕ
refine_1 : ∀ (v : Fin (r * t)), (↑v : ℕ) % r < r
refine_2 : ∀ (v : Fin (r * t)), (↑v : ℕ) / r < t
⊢ Fin (r * t) → Fin r × Fin t

Tactic:
refine fun v ↦ (⟨v % r, ?_⟩, ⟨v / r, ?_⟩)

Premises used: Prod.mk
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G : SimpleGraph α
s : Set α
r t : ℕ
v : Fin (r * t)
⊢ 0 < r

Tactic:
have ⟨hr, _⟩ := CanonicallyOrderedAdd.mul_pos.mp v.pos
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G : SimpleGraph α
s : Set α
r t : ℕ
v : Fin (r * t)
hr : 0 < r
⊢ 0 < t

Tactic:
have ⟨hr, _⟩ := CanonicallyOrderedAdd.mul_pos.mp v.pos
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G : SimpleGraph α
s : Set α
r t : ℕ
v : Fin (r * t)
hr : 0 < r
right : 0 < t
⊢ (↑v : ℕ) % r < r

Tactic:
Nat.mod_lt v hr

Premises used: Fin.val, Nat.mod_lt
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G : SimpleGraph α
s : Set α
r t : ℕ
v : Fin (r * t)
hr : 0 < r
right : 0 < t
⊢ (↑v : ℕ) % r < r

Tactic:
exact Nat.mod_lt v hr

Premises used: Fin.val, Nat.mod_lt
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G : SimpleGraph α
s : Set α
r t : ℕ
v : Fin (r * t)
⊢ (↑v : ℕ) / r < t

Tactic:
Nat.div_lt_of_lt_mul v.prop

Premises used: Fin.prop, Nat.div_lt_of_lt_mul
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G : SimpleGraph α
s : Set α
r t : ℕ
v : Fin (r * t)
⊢ (↑v : ℕ) / r < t

Tactic:
exact Nat.div_lt_of_lt_mul v.prop

Premises used: Fin.prop, Nat.div_lt_of_lt_mul
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
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

Tactic:
Prod.ext (Fin.ext ?_) (Fin.ext ?_)

Premises used: Fin.ext, Prod.ext
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
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 : ℕ)
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, ⋯⟩,
      ⟨(↑(⟨(↑v.2 : ℕ) * r + (↑v.1 : ℕ), ⋯⟩ : Fin (r * t)) : ℕ) / r, ⋯⟩) =
    v

Tactic:
refine Prod.ext (Fin.ext ?_) (Fin.ext ?_)

Premises used: Fin.ext, Prod.ext
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G : SimpleGraph α
s : Set α
r t : ℕ
v : Fin r × Fin t
enter : (↑(⟨(↑v.2 : ℕ) * r + (↑v.1 : ℕ), ⋯⟩ : Fin (r * t)) : ℕ) % r
| (↑((⟨(↑(⟨(↑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 : ℕ)

Tactic:
enter [1, 1, 1, 1, 1]
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G : SimpleGraph α
s : Set α
r t : ℕ
v : Fin r × Fin t
rw : (↑v.1 : ℕ) % r
| (↑(⟨(↑v.2 : ℕ) * r + (↑v.1 : ℕ), ⋯⟩ : Fin (r * t)) : ℕ) % r

Tactic:
rw [Nat.mul_add_mod_self_right]

Premises used: Nat.mul_add_mod_self_right
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G : SimpleGraph α
s : Set α
r t : ℕ
v : Fin r × Fin t
enter : (↑v.1 : ℕ) % r
| (↑((⟨(↑(⟨(↑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 : ℕ)

Tactic:
enter [1, 1, 1, 1, 1]
        rw [Nat.mul_add_mod_self_right]

Premises used: Nat.mul_add_mod_self_right
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G : SimpleGraph α
s : Set α
r t : ℕ
v : Fin r × Fin t
refine_1 :
  (↑((⟨(↑v.1 : ℕ) % 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, ⋯⟩ : Fin r),
            (⟨(↑(⟨(↑v.2 : ℕ) * r + (↑v.1 : ℕ), ⋯⟩ : Fin (r * t)) : ℕ) / r, ⋯⟩ : Fin t)).1 :
      ℕ) =
    (↑v.1 : ℕ)

Tactic:
conv =>
        enter [1, 1, 1, 1, 1]
        rw [Nat.mul_add_mod_self_right]

Premises used: Nat.mul_add_mod_self_right
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G : SimpleGraph α
s : Set α
r t : ℕ
v : Fin r × Fin t
⊢ (↑((⟨(↑v.1 : ℕ) % r, ⋯⟩ : Fin r), (⟨(↑(⟨(↑v.2 : ℕ) * r + (↑v.1 : ℕ), ⋯⟩ : Fin (r * t)) : ℕ) / r, ⋯⟩ : Fin t)).1 : ℕ) =
    (↑v.1 : ℕ)

Tactic:
Nat.mod_eq_of_lt v.1.prop

Premises used: Fin.prop, Nat.mod_eq_of_lt, Prod.fst
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G : SimpleGraph α
s : Set α
r t : ℕ
v : Fin r × Fin t
⊢ (↑((⟨(↑v.1 : ℕ) % r, ⋯⟩ : Fin r), (⟨(↑(⟨(↑v.2 : ℕ) * r + (↑v.1 : ℕ), ⋯⟩ : Fin (r * t)) : ℕ) / r, ⋯⟩ : Fin t)).1 : ℕ) =
    (↑v.1 : ℕ)

Tactic:
exact Nat.mod_eq_of_lt v.1.prop

Premises used: Fin.prop, Nat.mod_eq_of_lt, Prod.fst
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
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 : ℕ)
refine_2₁ :
  (↑v.2 : ℕ) ≤
    (↑(⟨(↑(⟨(↑v.2 : ℕ) * r + (↑v.1 : ℕ), ⋯⟩ : Fin (r * t)) : ℕ) % r, ⋯⟩,
            ⟨(↑(⟨(↑v.2 : ℕ) * r + (↑v.1 : ℕ), ⋯⟩ : Fin (r * t)) : ℕ) / r, ⋯⟩).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 : ℕ)

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G : SimpleGraph α
s : Set α
r t : ℕ
v : Fin r × Fin t
refine_2 : (↑(⟨(↑v.2 : ℕ) * r + (↑v.1 : ℕ), ⋯⟩ : Fin (r * t)) : ℕ) ≤ (↑v.2 : ℕ) * r + (r - 1)
⊢ (↑((⟨(↑(⟨(↑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 : ℕ)

Tactic:
rw [Nat.div_le_iff_le_mul_add_pred v.1.pos, mul_comm r ↑v.2]

Premises used: Fin.pos, Fin.val, Prod.fst, Nat.div_le_iff_le_mul_add_pred, mul_comm, Prod.snd
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G : SimpleGraph α
s : Set α
r t : ℕ
v : Fin r × Fin t
⊢ (↑(⟨(↑v.2 : ℕ) * r + (↑v.1 : ℕ), ⋯⟩ : Fin (r * t)) : ℕ) ≤ (↑v.2 : ℕ) * r + (r - 1)

Tactic:
Nat.add_le_add_left (Nat.le_pred_of_lt v.1.prop) (↑v.2 * r)

Premises used: HMul.hMul, Fin.prop, Prod.fst, Nat.le_pred_of_lt, Nat.pred, Nat.add_le_add_left
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G : SimpleGraph α
s : Set α
r t : ℕ
v : Fin r × Fin t
⊢ (↑(⟨(↑v.2 : ℕ) * r + (↑v.1 : ℕ), ⋯⟩ : Fin (r * t)) : ℕ) ≤ (↑v.2 : ℕ) * r + (r - 1)

Tactic:
exact Nat.add_le_add_left (Nat.le_pred_of_lt v.1.prop) (↑v.2 * r)

Premises used: HMul.hMul, Fin.prop, Prod.fst, Nat.le_pred_of_lt, Nat.add_le_add_left
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G : SimpleGraph α
s : Set α
r t : ℕ
v : Fin r × Fin t
refine_2 : (↑v.2 : ℕ) * r ≤ (↑⟨(↑v.2 : ℕ) * r + (↑v.1 : ℕ), ⋯⟩ : ℕ)
⊢ (↑v.2 : ℕ) ≤
    (↑(⟨(↑(⟨(↑v.2 : ℕ) * r + (↑v.1 : ℕ), ⋯⟩ : Fin (r * t)) : ℕ) % r, ⋯⟩,
            ⟨(↑(⟨(↑v.2 : ℕ) * r + (↑v.1 : ℕ), ⋯⟩ : Fin (r * t)) : ℕ) / r, ⋯⟩).2 :
      ℕ)

Tactic:
rw [Nat.le_div_iff_mul_le v.1.pos]

Premises used: Fin.pos, Prod.fst, Nat.le_div_iff_mul_le
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G : SimpleGraph α
s : Set α
r t : ℕ
v : Fin r × Fin t
⊢ (↑v.2 : ℕ) * r ≤ (↑⟨(↑v.2 : ℕ) * r + (↑v.1 : ℕ), ⋯⟩ : ℕ)

Tactic:
Nat.le_add_right (↑v.2 * r) ↑v.1

Premises used: HMul.hMul, Nat.le_add_right, Fin.val, Prod.fst
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G : SimpleGraph α
s : Set α
r t : ℕ
v : Fin r × Fin t
⊢ (↑v.2 : ℕ) * r ≤ (↑⟨(↑v.2 : ℕ) * r + (↑v.1 : ℕ), ⋯⟩ : ℕ)

Tactic:
exact Nat.le_add_right (↑v.2 * r) ↑v.1

Premises used: HMul.hMul, Nat.le_add_right, Fin.val, Prod.fst
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
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
rw₇ rw₈ : (completeEquipartiteGraph r t).Adj v w ↔ (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

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]

Premises used: Fin.ext_iff, Fin.prop, SimpleGraph.completeEquipartiteGraph_adj, Nat.mod_eq_of_lt, Prod.fst, SimpleGraph.turanGraph_adj, Iff.ne, Equiv.coe_fn_mk, Nat.mul_add_mod_self_right
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
r t : ℕ
contrapose! : completeEquipartiteGraph r t ≠ ⊥ ↔ 1 < r ∧ t ≠ 0
⊢ completeEquipartiteGraph r t = ⊥ ↔ r ≤ 1 ∨ t = 0

Tactic:
contrapose!
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
r t : ℕ
rw : (completeEquipartiteGraph r t).edgeSet.Nonempty ↔ Nontrivial (Fin r) ∧ Nonempty (Fin t)
⊢ completeEquipartiteGraph r t ≠ ⊥ ↔ 1 < r ∧ t ≠ 0

Tactic:
rw [← edgeSet_nonempty, ← Nat.succ_le_iff, ← Fin.nontrivial_iff_two_le, ← Nat.pos_iff_ne_zero,
    Fin.pos_iff_nonempty]

Premises used: Nat.pos_iff_ne_zero, SimpleGraph.edgeSet_nonempty, Fin.pos_iff_nonempty, Nat.succ_le_iff, Fin.nontrivial_iff_two_le
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
r t : ℕ
⊢ (completeEquipartiteGraph r t).edgeSet.Nonempty ↔ Nontrivial (Fin r) ∧ Nonempty (Fin t)

Tactic:
⟨fun ⟨e, he⟩ ↦ ?_, fun ⟨⟨i₁, i₂, hv⟩, ⟨x⟩⟩ ↦ ?_⟩

Premises used: Nontrivial, _private.0.SimpleGraph.completeEquipartiteGraph_eq_bot_iff.match_2, SimpleGraph.edgeSet, And, Set.Nonempty, Iff.intro, _private.0.SimpleGraph.completeEquipartiteGraph_eq_bot_iff.match_1, Nonempty, SimpleGraph.completeEquipartiteGraph, Fin
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
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)
refine_2 :
  Nontrivial (Fin r) ∧ Nonempty (Fin t) →
    ∀ (i₁ i₂ : Fin r) (hv : i₁ ≠ i₂) (x : Fin t), (completeEquipartiteGraph r t).edgeSet.Nonempty
⊢ (completeEquipartiteGraph r t).edgeSet.Nonempty ↔ Nontrivial (Fin r) ∧ Nonempty (Fin t)

Tactic:
refine ⟨fun ⟨e, he⟩ ↦ ?_, fun ⟨⟨i₁, i₂, hv⟩, ⟨x⟩⟩ ↦ ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
r t : ℕ
h : (completeEquipartiteGraph r t).edgeSet.Nonempty
e : Sym2 (Fin r × Fin t)
he : e ∈ (completeEquipartiteGraph r t).edgeSet
refine_1 :
  ∀ (v₁ v₂ : Fin r × Fin t) (he : s(v₁, v₂) ∈ (completeEquipartiteGraph r t).edgeSet),
    Nontrivial (Fin r) ∧ Nonempty (Fin t)
⊢ Nontrivial (Fin r) ∧ Nonempty (Fin t)

Tactic:
induction e with | _ v₁ v₂
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
r t : ℕ
h : (completeEquipartiteGraph r t).edgeSet.Nonempty
v₁ v₂ : Fin r × Fin t
he : s(v₁, v₂) ∈ (completeEquipartiteGraph r t).edgeSet
⊢ v₁.1 ≠ v₂.1

Tactic:
rw [mem_edgeSet, completeEquipartiteGraph_adj] at he

Premises used: SimpleGraph.completeEquipartiteGraph_adj, SimpleGraph.mem_edgeSet
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
r t : ℕ
h : (completeEquipartiteGraph r t).edgeSet.Nonempty
v₁ v₂ : Fin r × Fin t
he : v₁.1 ≠ v₂.1
⊢ Nontrivial (Fin r) ∧ Nonempty (Fin t)

Tactic:
⟨⟨v₁.1, v₂.1, he⟩, ⟨v₁.2⟩⟩

Premises used: Nontrivial.mk, Nonempty.intro, Prod.fst, And.intro, Exists.intro, Prod.snd
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
r t : ℕ
h : (completeEquipartiteGraph r t).edgeSet.Nonempty
v₁ v₂ : Fin r × Fin t
he : v₁.1 ≠ v₂.1
⊢ Nontrivial (Fin r) ∧ Nonempty (Fin t)

Tactic:
exact ⟨⟨v₁.1, v₂.1, he⟩, ⟨v₁.2⟩⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
r t : ℕ
h_1 : Nontrivial (Fin r) ∧ Nonempty (Fin t)
i₁ i₂ : Fin r
hv : i₁ ≠ i₂
x : Fin t
h : s((i₁, x), (i₂, x)) ∈ (completeEquipartiteGraph r t).edgeSet
⊢ (completeEquipartiteGraph r t).edgeSet.Nonempty

Tactic:
use s((i₁, x), (i₂, x))

Premises used: Prod.mk
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
r t : ℕ
h_1 : Nontrivial (Fin r) ∧ Nonempty (Fin t)
i₁ i₂ : Fin r
hv : i₁ ≠ i₂
x : Fin t
h : (i₁, x).1 ≠ (i₂, x).1
⊢ s((i₁, x), (i₂, x)) ∈ (completeEquipartiteGraph r t).edgeSet

Tactic:
rw [mem_edgeSet, completeEquipartiteGraph_adj]

Premises used: SimpleGraph.completeEquipartiteGraph_adj, SimpleGraph.mem_edgeSet
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
r t : ℕ
h : Nontrivial (Fin r) ∧ Nonempty (Fin t)
i₁ i₂ : Fin r
hv : i₁ ≠ i₂
x : Fin t
⊢ (i₁, x).1 ≠ (i₂, x).1

Tactic:
hv
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
r t : ℕ
h : Nontrivial (Fin r) ∧ Nonempty (Fin t)
i₁ i₂ : Fin r
hv : i₁ ≠ i₂
x : Fin t
⊢ (i₁, x).1 ≠ (i₂, x).1

Tactic:
exact hv
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
r t : ℕ
inl : ∀ (ht_eq0 : t = 0), (completeEquipartiteGraph r t).IsCompleteMultipartite
inr : ∀ (ht_pos : t > 0), (completeEquipartiteGraph r t).IsCompleteMultipartite
⊢ (completeEquipartiteGraph r t).IsCompleteMultipartite

Tactic:
rcases t.eq_zero_or_pos with ht_eq0 | ht_pos

Premises used: Nat.eq_zero_or_pos
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
r t : ℕ
ht_eq0 : t = 0
inl : IsCompleteMultipartite (α := Fin r × Fin t) ⊥
⊢ (completeEquipartiteGraph r t).IsCompleteMultipartite

Tactic:
rw [completeEquipartiteGraph_eq_bot_iff.mpr (Or.inr ht_eq0)]

Premises used: Iff.mpr, SimpleGraph.completeEquipartiteGraph_eq_bot_iff, Or.inr
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
r t : ℕ
ht_eq0 : t = 0
⊢ IsCompleteMultipartite (α := Fin r × Fin t) ⊥

Tactic:
bot_isCompleteMultipartite

Premises used: SimpleGraph.bot_isCompleteMultipartite
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
r t : ℕ
ht_eq0 : t = 0
⊢ IsCompleteMultipartite (α := Fin r × Fin t) ⊥

Tactic:
exact bot_isCompleteMultipartite

Premises used: SimpleGraph.bot_isCompleteMultipartite
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
r t : ℕ
ht_pos : t > 0
inr :
  ∃ (ι : Type) (V : ι → Type) (_ : ∀ (i : ι), Nonempty (V i)),
    Nonempty (completeEquipartiteGraph r t ≃g SimpleGraph.completeMultipartiteGraph V)
⊢ (completeEquipartiteGraph r t).IsCompleteMultipartite

Tactic:
rw [isCompleteMultipartite_iff]

Premises used: SimpleGraph.isCompleteMultipartite_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
r t : ℕ
ht_pos : t > 0
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))))
⊢ ∃ (ι : Type) (V : ι → Type) (_ : ∀ (i : ι), Nonempty (V i)),
    Nonempty (completeEquipartiteGraph r t ≃g SimpleGraph.completeMultipartiteGraph V)

Tactic:
use (Fin r), const (Fin r) (Fin t)

Premises used: Function.const, Fin
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
r t : ℕ
ht_pos : t > 0
h :
  (∀ (i : Fin r), Nonempty (Fin t)) ∧
    Nonempty
      ((completeEquipartiteGraph r t).Iso (W := (_ : Fin r) × Fin t)
        (SimpleGraph.completeMultipartiteGraph (const (Fin r) (Fin t))))
⊢ ∃ (_ : ∀ (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:
simp_rw [const_apply, exists_prop]

Premises used: Function.const_apply, exists_prop
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
r t : ℕ
ht_pos : t > 0
⊢ (∀ (i : Fin r), Nonempty (Fin t)) ∧
    Nonempty
      ((completeEquipartiteGraph r t).Iso (W := (_ : Fin r) × Fin t)
        (SimpleGraph.completeMultipartiteGraph (const (Fin r) (Fin t))))

Tactic:
⟨const (Fin r) (Fin.pos_iff_nonempty.mp ht_pos),
      ⟨completeEquipartiteGraph.completeMultipartiteGraph⟩⟩

Premises used: Nonempty.intro, And.intro, Iff.mp, Function.const, Fin.pos_iff_nonempty, Fin, SimpleGraph.completeEquipartiteGraph.completeMultipartiteGraph
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
r t : ℕ
ht_pos : t > 0
⊢ (∀ (i : Fin r), Nonempty (Fin t)) ∧
    Nonempty
      ((completeEquipartiteGraph r t).Iso (W := (_ : Fin r) × Fin t)
        (SimpleGraph.completeMultipartiteGraph (const (Fin r) (Fin t))))

Tactic:
exact ⟨const (Fin r) (Fin.pos_iff_nonempty.mp ht_pos),
      ⟨completeEquipartiteGraph.completeMultipartiteGraph⟩⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
r t : ℕ
v : Fin r × Fin t
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
⊢ (completeEquipartiteGraph r t).neighborSet v = SProd.sprod (α := Set (Fin r)) (β := Set (Fin t)) {v.1}ᶜ Set.univ

Tactic:
ext
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
r t : ℕ
v 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:
simp [ne_comm]

Premises used: ne_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
r t : ℕ
v : Fin r × Fin t
h :
  ∀ (a : Fin r × Fin t),
    a ∈ (completeEquipartiteGraph r t).neighborFinset v ↔
      a ∈ SProd.sprod (α := Finset (Fin r)) (β := Finset (Fin t)) {v.1}ᶜ univ
⊢ (completeEquipartiteGraph r t).neighborFinset v = SProd.sprod (α := Finset (Fin r)) (β := Finset (Fin t)) {v.1}ᶜ univ

Tactic:
ext
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
r t : ℕ
v a : Fin r × Fin t
⊢ a ∈ (completeEquipartiteGraph r t).neighborFinset v ↔
    a ∈ SProd.sprod (α := Finset (Fin r)) (β := Finset (Fin t)) {v.1}ᶜ univ

Tactic:
simp [ne_comm]

Premises used: ne_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
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
rw₂ : Finset.card (α := Fin r) {v.1}ᶜ * Finset.card (α := Fin t) univ = (r - 1) * t
rw₃ : (Fintype.card (Fin r) - Finset.card (α := Fin r) {v.1}) * Finset.card (α := Fin t) univ = (r - 1) * t
rw₄ : (Fintype.card (Fin r) - 1) * Finset.card (α := Fin t) univ = (r - 1) * t
rw₅ : (r - 1) * Finset.card (α := Fin t) univ = (r - 1) * t
rw₆ : (r - 1) * Fintype.card (Fin t) = (r - 1) * t
rw₇ rw₈ : (r - 1) * t = (r - 1) * t
⊢ (completeEquipartiteGraph r t).degree 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]

Premises used: Finset.card_univ, Fintype.card_fin, Finset.card_product, Finset.card_compl, SimpleGraph.neighborFinset_completeEquipartiteGraph, SimpleGraph.card_neighborFinset_eq_degree, Finset.card_singleton
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
r t : ℕ
rw : ∑ v : Fin r × Fin t, (completeEquipartiteGraph r t).degree v = 2 * (r.choose 2 * HPow.hPow (β := ℕ) t 2)
⊢ #(completeEquipartiteGraph r t).edgeFinset = r.choose 2 * HPow.hPow (β := ℕ) t 2

Tactic:
rw [← mul_right_inj' two_ne_zero, ← sum_degrees_eq_twice_card_edges]

Premises used: SimpleGraph.sum_degrees_eq_twice_card_edges, two_ne_zero, mul_right_inj'
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
r t : ℕ
rhs : fun (v : Fin r × Fin t) ↦ (completeEquipartiteGraph r t).degree v
| ∑ v : Fin r × Fin t, (completeEquipartiteGraph r t).degree v

Tactic:
rhs
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
r t : ℕ
v : Fin r × Fin t
h : (r - 1) * t
| (completeEquipartiteGraph r t).degree v

Tactic:
rw [degree_completeEquipartiteGraph v]

Premises used: SimpleGraph.degree_completeEquipartiteGraph
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
r t : ℕ
h : ∀ (v : Fin r × Fin t), (r - 1) * t
| ∑ v : Fin r × Fin t, (completeEquipartiteGraph r t).degree v

Tactic:
rhs; intro v
    rw [degree_completeEquipartiteGraph v]