awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
r t : ℕ
conv_lhs : ∑ v : Fin r × Fin t, (r - 1) * t = 2 * (r.choose 2 * HPow.hPow (β := ℕ) t 2)
⊢ ∑ v : Fin r × Fin t, (completeEquipartiteGraph r t).degree v = 2 * (r.choose 2 * HPow.hPow (β := ℕ) t 2)

Tactic:
conv_lhs =>
    rhs; intro v
    rw [degree_completeEquipartiteGraph v]
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
r t : ℕ
rw : r * t * ((r - 1) * t) = 2 * (r.choose 2 * HPow.hPow (β := ℕ) t 2)
⊢ ∑ v : Fin r × Fin t, (r - 1) * t = 2 * (r.choose 2 * HPow.hPow (β := ℕ) t 2)

Tactic:
rw [sum_const, smul_eq_mul, card_univ, card_prod, Fintype.card_fin, Fintype.card_fin]

Premises used: Finset.card_univ, Fintype.card_fin, Fintype.card_prod, smul_eq_mul, Finset.sum_const
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
r t : ℕ
rw : r * (r - 1) * HPow.hPow (β := ℕ) t 2
| 2 * (r.choose 2 * HPow.hPow (β := ℕ) t 2)

Tactic:
rw [← Nat.mul_assoc, Nat.choose_two_right, Nat.mul_div_cancel' r.even_mul_pred_self.two_dvd]

Premises used: Nat.even_mul_pred_self, Nat.choose_two_right, Nat.mul_assoc, Even.two_dvd, Nat.mul_div_cancel'
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
r t : ℕ
conv_rhs : r * t * ((r - 1) * t) = r * (r - 1) * HPow.hPow (β := ℕ) t 2
⊢ r * t * ((r - 1) * t) = 2 * (r.choose 2 * HPow.hPow (β := ℕ) t 2)

Tactic:
conv_rhs =>
    rw [← Nat.mul_assoc, Nat.choose_two_right, Nat.mul_div_cancel' r.even_mul_pred_self.two_dvd]

Premises used: Nat.even_mul_pred_self, Nat.choose_two_right, Nat.mul_assoc, Even.two_dvd, Nat.mul_div_cancel'
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
r t : ℕ
rw : r * t * (r - 1) * t = r * (r - 1) * HPow.hPow (β := ℕ) t 2
rw₁ : t * r * (r - 1) * t = r * (r - 1) * HPow.hPow (β := ℕ) t 2
rw₂ : t * (r * (r - 1)) * t = r * (r - 1) * HPow.hPow (β := ℕ) t 2
rw₃ : r * (r - 1) * t * t = r * (r - 1) * HPow.hPow (β := ℕ) t 2
rw₄ : r * (r - 1) * (t * t) = r * (r - 1) * HPow.hPow (β := ℕ) t 2
rw₅ rw₆ : r * (r - 1) * HPow.hPow (β := ℕ) t 2 = r * (r - 1) * HPow.hPow (β := ℕ) t 2
⊢ r * t * ((r - 1) * t) = r * (r - 1) * HPow.hPow (β := ℕ) t 2

Tactic:
rw [← mul_assoc, mul_comm r _, mul_assoc t _ _, mul_comm t, mul_assoc _ t, ← pow_two]

Premises used: pow_two, mul_assoc, mul_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G : SimpleGraph α
inst : Fintype α
n : ℕ
C : G.Coloring (Fin n)
t : ℕ
h : ∀ (c : Fin n), Fintype.card.{u} (↑(C.colorClass c) : Type u) ≤ t
c : Fin n
rw : Fintype.card.{u} (↑(C.colorClass c) : Type u) ≤ t
⊢ Nonempty.{max 1 (u + 1)} ((↑(C.colorClass c) : Type u) ↪ Fin t)

Tactic:
rw [Embedding.nonempty_iff_card_le, Fintype.card_fin]

Premises used: Fintype.card_fin, Function.Embedding.nonempty_iff_card_le
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G : SimpleGraph α
inst : Fintype α
n : ℕ
C : G.Coloring (Fin n)
t : ℕ
h : ∀ (c : Fin n), Fintype.card.{u} (↑(C.colorClass c) : Type u) ≤ t
c : Fin n
⊢ Fintype.card.{u} (↑(C.colorClass c) : Type u) ≤ t

Tactic:
h c
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G : SimpleGraph α
inst : Fintype α
n : ℕ
C : G.Coloring (Fin n)
t : ℕ
h : ∀ (c : Fin n), Fintype.card.{u} (↑(C.colorClass c) : Type u) ≤ t
c : Fin n
⊢ Fintype.card.{u} (↑(C.colorClass c) : Type u) ≤ t

Tactic:
exact h c
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G : SimpleGraph α
inst : Fintype α
n : ℕ
C : G.Coloring (Fin n)
t : ℕ
h : ∀ (c : Fin n), Fintype.card.{u} (↑(C.colorClass c) : Type u) ≤ t
⊢ ∀ (c : Fin n), Nonempty.{max 1 (u + 1)} ((↑(C.colorClass c) : Type u) ↪ Fin t)

Tactic:
have (c : Fin n) : Nonempty (C.colorClass c ↪ Fin t) := by
    rw [Embedding.nonempty_iff_card_le, Fintype.card_fin]
    exact h c
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G : SimpleGraph α
inst : Fintype α
n : ℕ
C : G.Coloring (Fin n)
t : ℕ
h : ∀ (c : Fin n), Fintype.card.{u} (↑(C.colorClass c) : Type u) ≤ t
this : ∀ (c : Fin n), Nonempty.{max 1 (u + 1)} ((↑(C.colorClass c) : Type u) ↪ Fin t)
have : ∀ (F : (c : Fin n) → (↑(C.colorClass c) : Type u) ↪ Fin t), G ⊑ completeEquipartiteGraph n t
⊢ G ⊑ completeEquipartiteGraph n t

Tactic:
have F (c : Fin n) := Classical.arbitrary (C.colorClass c ↪ Fin t)
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G : SimpleGraph α
inst : Fintype α
n : ℕ
C : G.Coloring (Fin n)
t : ℕ
h : ∀ (c : Fin n), Fintype.card.{u} (↑(C.colorClass c) : Type u) ≤ t
this : ∀ (c : Fin n), Nonempty.{max 1 (u + 1)} ((↑(C.colorClass c) : Type u) ↪ Fin t)
F : (c : Fin n) → (↑(C.colorClass c) : Type u) ↪ Fin t
c₁ c₂ : Fin n
v₁ : (↑(C.colorClass c₁) : Type u)
v₂ : (↑(C.colorClass c₂) : Type u)
hc : c₁ = c₂
hv :
  Eq (α := Fin t) ((F c₁ : (a : (↑(C.colorClass c₁) : Type u)) → Fin t) v₁ : Fin t)
    ((F c₂ : (a : (↑(C.colorClass c₂) : Type u)) → Fin t) v₂ : Fin t)
⊢ (↑v₁ : α) ∈ C.colorClass c₂

Tactic:
simp [← hc]
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G : SimpleGraph α
inst : Fintype α
n : ℕ
C : G.Coloring (Fin n)
t : ℕ
h : ∀ (c : Fin n), Fintype.card.{u} (↑(C.colorClass c) : Type u) ≤ t
this : ∀ (c : Fin n), Nonempty.{max 1 (u + 1)} ((↑(C.colorClass c) : Type u) ↪ Fin t)
F : (c : Fin n) → (↑(C.colorClass c) : Type u) ↪ Fin t
c₁ c₂ : Fin n
v₁ : (↑(C.colorClass c₁) : Type u)
v₂ : (↑(C.colorClass c₂) : Type u)
hc : c₁ = c₂
hv :
  Eq (α := Fin t) ((F c₁ : (a : (↑(C.colorClass c₁) : Type u)) → Fin t) v₁ : Fin t)
    ((F c₂ : (a : (↑(C.colorClass c₂) : Type u)) → Fin t) v₂ : Fin t)
v₁' : (↑(C.colorClass c₂) : Type u) := Subtype.mk (p := fun (x : α) ↦ x ∈ C.colorClass c₂) (↑v₁ : α) ⋯
h₁ :
  HEq (α := (↑(C.colorClass c₁) : Type u) → Fin t) (⇑(F c₁) : (a : (↑(C.colorClass c₁) : Type u)) → Fin t) (β :=
    (↑(C.colorClass c₂) : Type u) → Fin t) (⇑(F c₂) : (a : (↑(C.colorClass c₂) : Type u)) → Fin t)
h₂ : v₁ ≍ v₁'
⊢ Eq (α := Fin t) ((F c₁ : (a : (↑(C.colorClass c₁) : Type u)) → Fin t) v₁ : Fin t)
    ((F c₂ : (a : (↑(C.colorClass c₂) : Type u)) → Fin t) v₁' : Fin t)

Tactic:
apply congr_heq

Premises used: congr_heq
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G : SimpleGraph α
inst : Fintype α
n : ℕ
C : G.Coloring (Fin n)
t : ℕ
h : ∀ (c : Fin n), Fintype.card.{u} (↑(C.colorClass c) : Type u) ≤ t
this : ∀ (c : Fin n), Nonempty.{max 1 (u + 1)} ((↑(C.colorClass c) : Type u) ↪ Fin t)
F : (c : Fin n) → (↑(C.colorClass c) : Type u) ↪ Fin t
c₁ c₂ : Fin n
v₁ : (↑(C.colorClass c₁) : Type u)
v₂ : (↑(C.colorClass c₂) : Type u)
hc : c₁ = c₂
hv :
  Eq (α := Fin t) ((F c₁ : (a : (↑(C.colorClass c₁) : Type u)) → Fin t) v₁ : Fin t)
    ((F c₂ : (a : (↑(C.colorClass c₂) : Type u)) → Fin t) v₂ : Fin t)
v₁' : (↑(C.colorClass c₂) : Type u) := Subtype.mk (p := fun (x : α) ↦ x ∈ C.colorClass c₂) (↑v₁ : α) ⋯
h₁ h₂ :
  HEq (α := (↑(C.colorClass c₂) : Type u) → Fin t) (⇑(F c₂) : (a : (↑(C.colorClass c₂) : Type u)) → Fin t) (β :=
    (↑(C.colorClass c₂) : Type u) → Fin t) (⇑(F c₂) : (a : (↑(C.colorClass c₂) : Type u)) → Fin t)
⊢ HEq (α := (↑(C.colorClass c₁) : Type u) → Fin t) (⇑(F c₁) : (a : (↑(C.colorClass c₁) : Type u)) → Fin t) (β :=
    (↑(C.colorClass c₂) : Type u) → Fin t) (⇑(F c₂) : (a : (↑(C.colorClass c₂) : Type u)) → Fin t)

Tactic:
rw [hc]
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G : SimpleGraph α
inst : Fintype α
n : ℕ
C : G.Coloring (Fin n)
t : ℕ
h : ∀ (c : Fin n), Fintype.card.{u} (↑(C.colorClass c) : Type u) ≤ t
this : ∀ (c : Fin n), Nonempty.{max 1 (u + 1)} ((↑(C.colorClass c) : Type u) ↪ Fin t)
F : (c : Fin n) → (↑(C.colorClass c) : Type u) ↪ Fin t
c₁ c₂ : Fin n
v₁ : (↑(C.colorClass c₁) : Type u)
v₂ : (↑(C.colorClass c₂) : Type u)
hc : c₁ = c₂
hv :
  Eq (α := Fin t) ((F c₁ : (a : (↑(C.colorClass c₁) : Type u)) → Fin t) v₁ : Fin t)
    ((F c₂ : (a : (↑(C.colorClass c₂) : Type u)) → Fin t) v₂ : Fin t)
v₁' : (↑(C.colorClass c₂) : Type u) := Subtype.mk (p := fun (x : α) ↦ x ∈ C.colorClass c₂) (↑v₁ : α) ⋯
h₂ : ∀ (x : α), x ∈ C.colorClass c₁ ↔ x ∈ C.colorClass c₂
⊢ v₁ ≍ v₁'

Tactic:
rw [Subtype.heq_iff_coe_eq]

Premises used: Subtype.heq_iff_coe_eq
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G : SimpleGraph α
inst : Fintype α
n : ℕ
C : G.Coloring (Fin n)
t : ℕ
h : ∀ (c : Fin n), Fintype.card.{u} (↑(C.colorClass c) : Type u) ≤ t
this : ∀ (c : Fin n), Nonempty.{max 1 (u + 1)} ((↑(C.colorClass c) : Type u) ↪ Fin t)
F : (c : Fin n) → (↑(C.colorClass c) : Type u) ↪ Fin t
c₁ c₂ : Fin n
v₁ : (↑(C.colorClass c₁) : Type u)
v₂ : (↑(C.colorClass c₂) : Type u)
hc : c₁ = c₂
hv :
  Eq (α := Fin t) ((F c₁ : (a : (↑(C.colorClass c₁) : Type u)) → Fin t) v₁ : Fin t)
    ((F c₂ : (a : (↑(C.colorClass c₂) : Type u)) → Fin t) v₂ : Fin t)
v₁' : (↑(C.colorClass c₂) : Type u) := Subtype.mk (p := fun (x : α) ↦ x ∈ C.colorClass c₂) (↑v₁ : α) ⋯
⊢ ∀ (x : α), x ∈ C.colorClass c₁ ↔ x ∈ C.colorClass c₂

Tactic:
simp [hc]
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G : SimpleGraph α
inst : Fintype α
n : ℕ
C : G.Coloring (Fin n)
t : ℕ
h : ∀ (c : Fin n), Fintype.card.{u} (↑(C.colorClass c) : Type u) ≤ t
this : ∀ (c : Fin n), Nonempty.{max 1 (u + 1)} ((↑(C.colorClass c) : Type u) ↪ Fin t)
F : (c : Fin n) → (↑(C.colorClass c) : Type u) ↪ Fin t
c₁ c₂ : Fin n
v₁ : (↑(C.colorClass c₁) : Type u)
v₂ : (↑(C.colorClass c₂) : Type u)
hc : c₁ = c₂
hv :
  Eq (α := Fin t) ((F c₁ : (a : (↑(C.colorClass c₁) : Type u)) → Fin t) v₁ : Fin t)
    ((F c₂ : (a : (↑(C.colorClass c₂) : Type u)) → Fin t) v₂ : Fin t)
v₁' : (↑(C.colorClass c₂) : Type u) := Subtype.mk (p := fun (x : α) ↦ x ∈ C.colorClass c₂) (↑v₁ : α) ⋯
⊢ Eq (α := Fin t) ((F c₁ : (a : (↑(C.colorClass c₁) : Type u)) → Fin t) v₁ : Fin t)
    ((F c₂ : (a : (↑(C.colorClass c₂) : Type u)) → Fin t) v₁' : Fin t)

Tactic:
have hv' : F c₁ v₁ = F c₂ v₁' := by
      apply congr_heq
      · rw [hc]
      · rw [Subtype.heq_iff_coe_eq]
        simp [hc]
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G : SimpleGraph α
inst : Fintype α
n : ℕ
C : G.Coloring (Fin n)
t : ℕ
h : ∀ (c : Fin n), Fintype.card.{u} (↑(C.colorClass c) : Type u) ≤ t
this : ∀ (c : Fin n), Nonempty.{max 1 (u + 1)} ((↑(C.colorClass c) : Type u) ↪ Fin t)
F : (c : Fin n) → (↑(C.colorClass c) : Type u) ↪ Fin t
c₁ c₂ : Fin n
v₁ : (↑(C.colorClass c₁) : Type u)
v₂ : (↑(C.colorClass c₂) : Type u)
hc : c₁ = c₂
hv :
  Eq (α := Fin t) ((F c₁ : (a : (↑(C.colorClass c₁) : Type u)) → Fin t) v₁ : Fin t)
    ((F c₂ : (a : (↑(C.colorClass c₂) : Type u)) → Fin t) v₂ : Fin t)
v₁' : (↑(C.colorClass c₂) : Type u) := Subtype.mk (p := fun (x : α) ↦ x ∈ C.colorClass c₂) (↑v₁ : α) ⋯
hv' :
  Eq (α := Fin t) ((F c₁ : (a : (↑(C.colorClass c₁) : Type u)) → Fin t) v₁ : Fin t)
    ((F c₂ : (a : (↑(C.colorClass c₂) : Type u)) → Fin t) v₁' : Fin t)
⊢ Eq (α := Fin t) ((F c₂ : (a : (↑(C.colorClass c₂) : Type u)) → Fin t) v₁' : Fin t)
    ((F c₂ : (a : (↑(C.colorClass c₂) : Type u)) → Fin t) v₂ : Fin t)

Tactic:
rw [hv'] at hv
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G : SimpleGraph α
inst : Fintype α
n : ℕ
C : G.Coloring (Fin n)
t : ℕ
h : ∀ (c : Fin n), Fintype.card.{u} (↑(C.colorClass c) : Type u) ≤ t
this : ∀ (c : Fin n), Nonempty.{max 1 (u + 1)} ((↑(C.colorClass c) : Type u) ↪ Fin t)
F : (c : Fin n) → (↑(C.colorClass c) : Type u) ↪ Fin t
c₁ c₂ : Fin n
v₁ : (↑(C.colorClass c₁) : Type u)
v₂ : (↑(C.colorClass c₂) : Type u)
hc : c₁ = c₂
hv :
  Eq (α := Fin t) ((F c₁ : (a : (↑(C.colorClass c₁) : Type u)) → Fin t) v₁ : Fin t)
    ((F c₂ : (a : (↑(C.colorClass c₂) : Type u)) → Fin t) v₂ : Fin t)
v₁' : (↑(C.colorClass c₂) : Type u) := Subtype.mk (p := fun (x : α) ↦ x ∈ C.colorClass c₂) (↑v₁ : α) ⋯
hv' :
  Eq (α := Fin t) ((F c₁ : (a : (↑(C.colorClass c₁) : Type u)) → Fin t) v₁ : Fin t)
    ((F c₂ : (a : (↑(C.colorClass c₂) : Type u)) → Fin t) v₁' : Fin t)
hv₁ :
  Eq (α := Fin t) ((F c₂ : (a : (↑(C.colorClass c₂) : Type u)) → Fin t) v₁' : Fin t)
    ((F c₂ : (a : (↑(C.colorClass c₂) : Type u)) → Fin t) v₂ : Fin t)
⊢ Eq (α := Fin t) ((F c₁ : (a : (↑(C.colorClass c₁) : Type u)) → Fin t) v₁ : Fin t)
    ((F c₂ : (a : (↑(C.colorClass c₂) : Type u)) → Fin t) v₁' : Fin t)

Tactic:
rw [hv'] at hv
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G : SimpleGraph α
inst : Fintype α
n : ℕ
C : G.Coloring (Fin n)
t : ℕ
h : ∀ (c : Fin n), Fintype.card.{u} (↑(C.colorClass c) : Type u) ≤ t
this : ∀ (c : Fin n), Nonempty.{max 1 (u + 1)} ((↑(C.colorClass c) : Type u) ↪ Fin t)
F : (c : Fin n) → (↑(C.colorClass c) : Type u) ↪ Fin t
c₁ c₂ : Fin n
v₁ : (↑(C.colorClass c₁) : Type u)
v₂ : (↑(C.colorClass c₂) : Type u)
hc : c₁ = c₂
v₁' : (↑(C.colorClass c₂) : Type u) := Subtype.mk (p := fun (x : α) ↦ x ∈ C.colorClass c₂) (↑v₁ : α) ⋯
hv :
  Eq (α := Fin t) ((F c₂ : (a : (↑(C.colorClass c₂) : Type u)) → Fin t) v₁' : Fin t)
    ((F c₂ : (a : (↑(C.colorClass c₂) : Type u)) → Fin t) v₂ : Fin t)
hv' :
  Eq (α := Fin t) ((F c₁ : (a : (↑(C.colorClass c₁) : Type u)) → Fin t) v₁ : Fin t)
    ((F c₂ : (a : (↑(C.colorClass c₂) : Type u)) → Fin t) v₁' : Fin t)
⊢ (↑v₁ : α) = (↑v₂ : α)

Tactic:
simpa [Subtype.ext_iff] using (F c₂).injective hv

Premises used: Subtype.ext_iff, Function.Embedding.injective
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G : SimpleGraph α
inst : Fintype α
n : ℕ
C : G.Coloring (Fin n)
t : ℕ
h : ∀ (c : Fin n), Fintype.card.{u} (↑(C.colorClass c) : Type u) ≤ t
this : ∀ (c : Fin n), Nonempty.{max 1 (u + 1)} ((↑(C.colorClass c) : Type u) ↪ Fin t)
F : (c : Fin n) → (↑(C.colorClass c) : Type u) ↪ Fin t
⊢ ∀ {c₁ c₂ : Fin n} {v₁ : (↑(C.colorClass c₁) : Type u)} {v₂ : (↑(C.colorClass c₂) : Type u)} (hc : c₁ = c₂)
    (hv :
      Eq (α := Fin t) ((F c₁ : (a : (↑(C.colorClass c₁) : Type u)) → Fin t) v₁ : Fin t)
        ((F c₂ : (a : (↑(C.colorClass c₂) : Type u)) → Fin t) v₂ : Fin t)),
    (↑v₁ : α) = (↑v₂ : α)

Tactic:
have hF {c₁ c₂ v₁ v₂} (hc : c₁ = c₂) (hv : F c₁ v₁ = F c₂ v₂) : v₁.val = v₂.val := by
    let v₁' : C.colorClass c₂ := ⟨v₁, by simp [← hc]⟩
    have hv' : F c₁ v₁ = F c₂ v₁' := by
      apply congr_heq
      · rw [hc]
      · rw [Subtype.heq_iff_coe_eq]
        simp [hc]
    rw [hv'] at hv
    simpa [Subtype.ext_iff] using (F c₂).injective hv
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G : SimpleGraph α
inst : Fintype α
n : ℕ
C : G.Coloring (Fin n)
t : ℕ
h : ∀ (c : Fin n), Fintype.card.{u} (↑(C.colorClass c) : Type u) ≤ t
this : ∀ (c : Fin n), Nonempty.{max 1 (u + 1)} ((↑(C.colorClass c) : Type u) ↪ Fin t)
F : (c : Fin n) → (↑(C.colorClass c) : Type u) ↪ Fin t
hF :
  ∀ {c₁ c₂ : Fin n} {v₁ : (↑(C.colorClass c₁) : Type u)} {v₂ : (↑(C.colorClass c₂) : Type u)} (hc : c₁ = c₂)
    (hv :
      Eq (α := Fin t) ((F c₁ : (a : (↑(C.colorClass c₁) : Type u)) → Fin t) v₁ : Fin t)
        ((F c₂ : (a : (↑(C.colorClass c₂) : Type u)) → Fin t) v₂ : Fin t)),
    (↑v₁ : α) = (↑v₂ : α)
injective' :
  Injective.{u + 1, 1} (α := α) (β := Fin n × Fin t)
    (⇑(RelHom.mk (r := G.Adj) (s := (completeEquipartiteGraph n t).Adj)
          (fun (v : α) ↦
            ((C : (a : α) → Fin n) v,
              ((F ((C : (a : α) → Fin n) v) : (↑(C.colorClass ((C : (a : α) → Fin n) v)) : Type u) ↪ Fin t) :
                  (a : (↑(C.colorClass ((C : (a : α) → Fin n) v)) : Type u)) → Fin t)
                (Subtype.mk (p := fun (x : α) ↦ x ∈ C.colorClass ((C : (a : α) → Fin n) v)) v ⋯)))
          ⋯) :
      (a : α) → Fin n × Fin t)
⊢ G ⊑ completeEquipartiteGraph n t

Tactic:
use ⟨fun v ↦ (C v, F (C v) ⟨v, C.mem_colorClass v⟩), C.valid⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G : SimpleGraph α
inst : Fintype α
n : ℕ
C : G.Coloring (Fin n)
t : ℕ
h_1 : ∀ (c : Fin n), Fintype.card.{u} (↑(C.colorClass c) : Type u) ≤ t
this : ∀ (c : Fin n), Nonempty.{max 1 (u + 1)} ((↑(C.colorClass c) : Type u) ↪ Fin t)
F : (c : Fin n) → (↑(C.colorClass c) : Type u) ↪ Fin t
hF :
  ∀ {c₁ c₂ : Fin n} {v₁ : (↑(C.colorClass c₁) : Type u)} {v₂ : (↑(C.colorClass c₂) : Type u)} (hc : c₁ = c₂)
    (hv :
      Eq (α := Fin t) ((F c₁ : (a : (↑(C.colorClass c₁) : Type u)) → Fin t) v₁ : Fin t)
        ((F c₂ : (a : (↑(C.colorClass c₂) : Type u)) → Fin t) v₂ : Fin t)),
    (↑v₁ : α) = (↑v₂ : α)
v w : α
h :
  Eq (α := Fin n)
      (((RelHom.mk (r := G.Adj) (s := (completeEquipartiteGraph n t).Adj)
                (fun (v : α) ↦
                  ((C : (a : α) → Fin n) v,
                    ((F ((C : (a : α) → Fin n) v) : (↑(C.colorClass ((C : (a : α) → Fin n) v)) : Type u) ↪ Fin t) :
                        (a : (↑(C.colorClass ((C : (a : α) → Fin n) v)) : Type u)) → Fin t)
                      (Subtype.mk (p := fun (x : α) ↦ x ∈ C.colorClass ((C : (a : α) → Fin n) v)) v ⋯)))
                ⋯ :
              G.Adj →r (completeEquipartiteGraph n t).Adj) :
            (a : α) → Fin n × Fin t)
          v).1
      (((RelHom.mk (r := G.Adj) (s := (completeEquipartiteGraph n t).Adj)
                (fun (v : α) ↦
                  ((C : (a : α) → Fin n) v,
                    ((F ((C : (a : α) → Fin n) v) : (↑(C.colorClass ((C : (a : α) → Fin n) v)) : Type u) ↪ Fin t) :
                        (a : (↑(C.colorClass ((C : (a : α) → Fin n) v)) : Type u)) → Fin t)
                      (Subtype.mk (p := fun (x : α) ↦ x ∈ C.colorClass ((C : (a : α) → Fin n) v)) v ⋯)))
                ⋯ :
              G.Adj →r (completeEquipartiteGraph n t).Adj) :
            (a : α) → Fin n × Fin t)
          w).1 ∧
    Eq (α := Fin t)
      (((RelHom.mk (r := G.Adj) (s := (completeEquipartiteGraph n t).Adj)
                (fun (v : α) ↦
                  ((C : (a : α) → Fin n) v,
                    ((F ((C : (a : α) → Fin n) v) : (↑(C.colorClass ((C : (a : α) → Fin n) v)) : Type u) ↪ Fin t) :
                        (a : (↑(C.colorClass ((C : (a : α) → Fin n) v)) : Type u)) → Fin t)
                      (Subtype.mk (p := fun (x : α) ↦ x ∈ C.colorClass ((C : (a : α) → Fin n) v)) v ⋯)))
                ⋯ :
              G.Adj →r (completeEquipartiteGraph n t).Adj) :
            (a : α) → Fin n × Fin t)
          v).2
      (((RelHom.mk (r := G.Adj) (s := (completeEquipartiteGraph n t).Adj)
                (fun (v : α) ↦
                  ((C : (a : α) → Fin n) v,
                    ((F ((C : (a : α) → Fin n) v) : (↑(C.colorClass ((C : (a : α) → Fin n) v)) : Type u) ↪ Fin t) :
                        (a : (↑(C.colorClass ((C : (a : α) → Fin n) v)) : Type u)) → Fin t)
                      (Subtype.mk (p := fun (x : α) ↦ x ∈ C.colorClass ((C : (a : α) → Fin n) v)) v ⋯)))
                ⋯ :
              G.Adj →r (completeEquipartiteGraph n t).Adj) :
            (a : α) → Fin n × Fin t)
          w).2
⊢ v = w

Tactic:
hF h.1 h.2

Premises used: And.right, And.left
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G : SimpleGraph α
inst : Fintype α
n : ℕ
C : G.Coloring (Fin n)
t : ℕ
h_1 : ∀ (c : Fin n), Fintype.card.{u} (↑(C.colorClass c) : Type u) ≤ t
this : ∀ (c : Fin n), Nonempty.{max 1 (u + 1)} ((↑(C.colorClass c) : Type u) ↪ Fin t)
F : (c : Fin n) → (↑(C.colorClass c) : Type u) ↪ Fin t
hF :
  ∀ {c₁ c₂ : Fin n} {v₁ : (↑(C.colorClass c₁) : Type u)} {v₂ : (↑(C.colorClass c₂) : Type u)} (hc : c₁ = c₂)
    (hv :
      Eq (α := Fin t) ((F c₁ : (a : (↑(C.colorClass c₁) : Type u)) → Fin t) v₁ : Fin t)
        ((F c₂ : (a : (↑(C.colorClass c₂) : Type u)) → Fin t) v₂ : Fin t)),
    (↑v₁ : α) = (↑v₂ : α)
v w : α
h :
  Eq (α := Fin n)
      (((RelHom.mk (r := G.Adj) (s := (completeEquipartiteGraph n t).Adj)
                (fun (v : α) ↦
                  ((C : (a : α) → Fin n) v,
                    ((F ((C : (a : α) → Fin n) v) : (↑(C.colorClass ((C : (a : α) → Fin n) v)) : Type u) ↪ Fin t) :
                        (a : (↑(C.colorClass ((C : (a : α) → Fin n) v)) : Type u)) → Fin t)
                      (Subtype.mk (p := fun (x : α) ↦ x ∈ C.colorClass ((C : (a : α) → Fin n) v)) v ⋯)))
                ⋯ :
              G.Adj →r (completeEquipartiteGraph n t).Adj) :
            (a : α) → Fin n × Fin t)
          v).1
      (((RelHom.mk (r := G.Adj) (s := (completeEquipartiteGraph n t).Adj)
                (fun (v : α) ↦
                  ((C : (a : α) → Fin n) v,
                    ((F ((C : (a : α) → Fin n) v) : (↑(C.colorClass ((C : (a : α) → Fin n) v)) : Type u) ↪ Fin t) :
                        (a : (↑(C.colorClass ((C : (a : α) → Fin n) v)) : Type u)) → Fin t)
                      (Subtype.mk (p := fun (x : α) ↦ x ∈ C.colorClass ((C : (a : α) → Fin n) v)) v ⋯)))
                ⋯ :
              G.Adj →r (completeEquipartiteGraph n t).Adj) :
            (a : α) → Fin n × Fin t)
          w).1 ∧
    Eq (α := Fin t)
      (((RelHom.mk (r := G.Adj) (s := (completeEquipartiteGraph n t).Adj)
                (fun (v : α) ↦
                  ((C : (a : α) → Fin n) v,
                    ((F ((C : (a : α) → Fin n) v) : (↑(C.colorClass ((C : (a : α) → Fin n) v)) : Type u) ↪ Fin t) :
                        (a : (↑(C.colorClass ((C : (a : α) → Fin n) v)) : Type u)) → Fin t)
                      (Subtype.mk (p := fun (x : α) ↦ x ∈ C.colorClass ((C : (a : α) → Fin n) v)) v ⋯)))
                ⋯ :
              G.Adj →r (completeEquipartiteGraph n t).Adj) :
            (a : α) → Fin n × Fin t)
          v).2
      (((RelHom.mk (r := G.Adj) (s := (completeEquipartiteGraph n t).Adj)
                (fun (v : α) ↦
                  ((C : (a : α) → Fin n) v,
                    ((F ((C : (a : α) → Fin n) v) : (↑(C.colorClass ((C : (a : α) → Fin n) v)) : Type u) ↪ Fin t) :
                        (a : (↑(C.colorClass ((C : (a : α) → Fin n) v)) : Type u)) → Fin t)
                      (Subtype.mk (p := fun (x : α) ↦ x ∈ C.colorClass ((C : (a : α) → Fin n) v)) v ⋯)))
                ⋯ :
              G.Adj →r (completeEquipartiteGraph n t).Adj) :
            (a : α) → Fin n × Fin t)
          w).2
⊢ v = w

Tactic:
exact hF h.1 h.2

Premises used: And.right, And.left
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
V : Type u_1
G : SimpleGraph V
r t : ℕ
h : r = 0 ∨ t = 0
hr : r = 0
⊢ Finset.card.{u_1} (α := Finset V) ∅ = r ∨ t = 0

Tactic:
simp [hr]
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
V : Type u_1
G : SimpleGraph V
r t : ℕ
h : r = 0 ∨ t = 0
ht : t = 0
⊢ Finset.card.{u_1} (α := Finset V) ∅ = r ∨ t = 0

Tactic:
simp [ht]
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
V : Type u_1
G : SimpleGraph V
r t : ℕ
h : r = 0 ∨ t = 0
⊢ ∀ {p : Finset V}, Membership.mem (γ := Finset (Finset V)) ∅ p → #p = t

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
V : Type u_1
G : SimpleGraph V
r t : ℕ
h : r = 0 ∨ t = 0
⊢ (↑∅ : Set (Finset V)).Pairwise fun (x1 x2 : Finset V) ↦ G.IsCompleteBetween (↑x1 : Set V) (↑x2 : Set V)

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
⊢ (↑K.parts : Set (Finset V)).Pairwise Disjoint

Tactic:
fun _ h₁ _ h₂ hne ↦ Finset.disjoint_left.mpr fun _ h₁' h₂' ↦
    (G.loopless.irrefl _) (K.isCompleteBetween h₁ h₂ hne h₁' h₂')

Premises used: Iff.mpr, SimpleGraph.CompleteEquipartiteSubgraph.isCompleteBetween, Std.Irrefl.irrefl, Set.Pairwise, Finset.disjoint_left
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
rw : K.parts.disjiUnion id ⋯ = K.parts.biUnion id
rw₁ rw₂ : K.parts.biUnion id = K.parts.biUnion id
⊢ K.verts = K.parts.biUnion id

Tactic:
rw [verts, disjiUnion_eq_biUnion]

Premises used: Finset.disjiUnion_eq_biUnion, SimpleGraph.CompleteEquipartiteSubgraph.verts
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
simp_rw : #K.parts = r ∨ t = 0
⊢ #K.verts = r * t

Tactic:
simp_rw [verts, card_disjiUnion, id_eq, sum_congr rfl fun _ ↦ K.card_mem_parts, sum_const,
    smul_eq_mul, mul_eq_mul_right_iff]

Premises used: Finset.card_disjiUnion, mul_eq_mul_right_iff, SimpleGraph.CompleteEquipartiteSubgraph.verts, SimpleGraph.CompleteEquipartiteSubgraph.card_mem_parts, smul_eq_mul, Finset.sum_congr, rfl, id_eq, Finset.sum_const