awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
rw₂ : Finset.card (α := Fin r) {v.1}ᶜ * Finset.card (α := Fin t) univ = (r - 1) * t
⊢ (completeEquipartiteGraph r t).degree v = (r - 1) * t
have rw₃ : (Fintype.card (Fin r) - 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]
-- 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
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
⊢ (completeEquipartiteGraph r t).degree v = (r - 1) * t
have rw₄ : (Fintype.card (Fin r) - 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]
-- 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
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
⊢ (completeEquipartiteGraph r t).degree v = (r - 1) * t
have rw₅ : (r - 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]
-- 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
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
⊢ (completeEquipartiteGraph r t).degree v = (r - 1) * t
have rw₆ : (r - 1) * Fintype.card (Fin t) = (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
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
⊢ (completeEquipartiteGraph r t).degree v = (r - 1) * t
have rw₇ : (r - 1) * t = (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 : ℕ
⊢ #(completeEquipartiteGraph r t).edgeFinset = r.choose 2 * HPow.hPow (β := ℕ) t 2
have rw : ∑ v : Fin r × Fin t, (completeEquipartiteGraph r t).degree v = 2 * (r.choose 2 * HPow.hPow (β := ℕ) t 2)
Tactic: rw [← mul_right_inj' two_ne_zero, ← sum_degrees_eq_twice_card_edges]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (goal)
Goal:
r t : ℕ
| ∑ v : Fin r × Fin t, (completeEquipartiteGraph r t).degree v
have rhs : fun (v : Fin r × Fin t) ↦ (completeEquipartiteGraph r t).degree v
Tactic: rhs
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (goal)
Goal:
r t : ℕ
v : Fin r × Fin t
| (completeEquipartiteGraph r t).degree v
have h : (r - 1) * t
Tactic: rw [degree_completeEquipartiteGraph v]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (goal)
Goal:
r t : ℕ
| ∑ v : Fin r × Fin t, (completeEquipartiteGraph r t).degree v
have h : ∀ (v : Fin r × Fin t), (r - 1) * t
Tactic: rhs; intro v
    rw [degree_completeEquipartiteGraph v]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (goal)
Goal:
r t : ℕ
⊢ ∑ v : Fin r × Fin t, (completeEquipartiteGraph r t).degree v = 2 * (r.choose 2 * HPow.hPow (β := ℕ) t 2)
have conv_lhs : ∑ v : Fin r × Fin t, (r - 1) * t = 2 * (r.choose 2 * HPow.hPow (β := ℕ) t 2)
Tactic: conv_lhs =>
    rhs; intro v
    rw [degree_completeEquipartiteGraph v]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (goal)
Goal:
r t : ℕ
⊢ ∑ v : Fin r × Fin t, (r - 1) * t = 2 * (r.choose 2 * HPow.hPow (β := ℕ) t 2)
have rw : r * 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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (goal)
Goal:
r t : ℕ
| 2 * (r.choose 2 * HPow.hPow (β := ℕ) t 2)
have rw : r * (r - 1) * HPow.hPow (β := ℕ) t 2
Tactic: rw [← Nat.mul_assoc, Nat.choose_two_right, Nat.mul_div_cancel' r.even_mul_pred_self.two_dvd]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (goal)
Goal:
r t : ℕ
⊢ r * t * ((r - 1) * t) = 2 * (r.choose 2 * HPow.hPow (β := ℕ) t 2)
have conv_rhs : r * t * ((r - 1) * t) = r * (r - 1) * 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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (goal)
Goal:
r t : ℕ
⊢ r * t * ((r - 1) * t) = r * (r - 1) * HPow.hPow (β := ℕ) t 2
have rw : 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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (goal)
Goal:
r t : ℕ
rw : r * t * (r - 1) * t = r * (r - 1) * HPow.hPow (β := ℕ) t 2
⊢ r * t * ((r - 1) * t) = r * (r - 1) * HPow.hPow (β := ℕ) t 2
have rw₁ : t * r * (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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (goal)
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
⊢ r * t * ((r - 1) * t) = r * (r - 1) * HPow.hPow (β := ℕ) t 2
have rw₂ : t * (r * (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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (goal)
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
⊢ r * t * ((r - 1) * t) = r * (r - 1) * HPow.hPow (β := ℕ) t 2
have rw₃ : r * (r - 1) * t * 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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (goal)
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
⊢ r * t * ((r - 1) * t) = r * (r - 1) * HPow.hPow (β := ℕ) t 2
have rw₄ : r * (r - 1) * (t * 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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (goal)
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
⊢ r * t * ((r - 1) * t) = r * (r - 1) * HPow.hPow (β := ℕ) t 2
have rw₅ : r * (r - 1) * HPow.hPow (β := ℕ) t 2 = 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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (goal)
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)
have rw : Fintype.card.{u} (↑(C.colorClass c) : Type u) ≤ t
Tactic: rw [Embedding.nonempty_iff_card_le, Fintype.card_fin]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (hypothesis)
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
⊢ G ⊑ completeEquipartiteGraph n t
have this : ∀ (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
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (goal)
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)
⊢ G ⊑ completeEquipartiteGraph n t
have have : ∀ (F : (c : Fin n) → (↑(C.colorClass c) : Type u) ↪ Fin t), G ⊑ completeEquipartiteGraph n t
Tactic: have F (c : Fin n) := Classical.arbitrary (C.colorClass c ↪ Fin t)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (goal)
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)
have 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)
Tactic: apply congr_heq
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (goal)
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)
⊢ 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)
have h₂ : v₁ ≍ v₁'
Tactic: apply congr_heq
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (goal)
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₁ : α) ⋯
⊢ 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)
have 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)
Tactic: rw [hc]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (goal)
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₁ : α) ⋯
⊢ v₁ ≍ v₁'
have h₂ : ∀ (x : α), x ∈ C.colorClass c₁ ↔ x ∈ C.colorClass c₂
Tactic: rw [Subtype.heq_iff_coe_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (hypothesis)
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₁ : α) ⋯
⊢ (↑v₁ : α) = (↑v₂ : α)
have 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)
Tactic: have hv' : F c₁ v₁ = F c₂ v₁' := by
      apply congr_heq
      · rw [hc]
      · rw [Subtype.heq_iff_coe_eq]
        simp [hc]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (hypothesis)
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)
⊢ (↑v₁ : α) = (↑v₂ : α)
have 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)
Tactic: rw [hv'] at hv
Cleared hypotheses: hv, hv'
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (hypothesis)
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
⊢ G ⊑ completeEquipartiteGraph n t
have 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₂ : α)
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
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (goal)
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₂ : α)
⊢ G ⊑ completeEquipartiteGraph n t
have 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 sorry)))
        sorry) :
    (a : α) → Fin n × Fin t)
Tactic: use ⟨fun v ↦ (C v, F (C v) ⟨v, C.mem_colorClass v⟩), C.valid⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (goal)
Goal:
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
⊢ K.verts = K.parts.biUnion id
have rw : K.parts.disjiUnion id sorry = K.parts.biUnion id
Tactic: rw [verts, disjiUnion_eq_biUnion]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (goal)
Goal:
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
rw : K.parts.disjiUnion id ⋯ = K.parts.biUnion id
⊢ K.verts = K.parts.biUnion id
have rw₁ : K.parts.biUnion id = K.parts.biUnion id
Tactic: rw [verts, disjiUnion_eq_biUnion]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (goal)
Goal:
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
⊢ #K.verts = r * t
have simp_rw : #K.parts = r ∨ t = 0
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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (goal)
Goal:
α : Type u
G_1 : SimpleGraph α
s : Set α
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
⊢ (completeEquipartiteGraph r t).Copy G
have pos : (ht : t = 0) → (completeEquipartiteGraph r t).Copy G
Tactic: by_cases ht : t = 0
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (goal)
Goal:
α : Type u
G_1 : SimpleGraph α
s : Set α
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
pos : (ht : t = 0) → (completeEquipartiteGraph r t).Copy G
⊢ (completeEquipartiteGraph r t).Copy G
have neg : (ht : ¬t = 0) → (completeEquipartiteGraph r t).Copy G
Tactic: by_cases ht : t = 0
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (goal)
Goal:
α : Type u
G_1 : SimpleGraph α
s : Set α
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
ht : t = 0
⊢ (completeEquipartiteGraph r t).Copy G
have pos : Copy (α := Fin r × Fin t) ⊥ G
Tactic: rw [completeEquipartiteGraph_eq_bot_iff.mpr <| .inr ht]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (hypothesis)
Goal:
α : Type u
G_1 : SimpleGraph α
s : Set α
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
ht : t = 0
⊢ Copy (α := Fin r × Fin t) ⊥ G
have this : IsEmpty (Fin r × Fin t)
Tactic: have : IsEmpty (Fin r × Fin t) := by simp [ht, Fin.isEmpty]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (goal)
Goal:
α : Type u
G_1 : SimpleGraph α
s : Set α
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
ht : ¬t = 0
⊢ Nonempty.{max 1 (u_1 + 1)} (Fin r ↪ ↥K.parts)
have rw : Fintype.card (Fin r) ≤ Fintype.card.{u_1} ↥K.parts
Tactic: rw [Embedding.nonempty_iff_card_le,
        Fintype.card_fin, card_coe, K.card_parts.resolve_right ht]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (goal)
Goal:
α : Type u
G_1 : SimpleGraph α
s : Set α
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
ht : ¬t = 0
rw : Fintype.card (Fin r) ≤ Fintype.card.{u_1} ↥K.parts
⊢ Nonempty.{max 1 (u_1 + 1)} (Fin r ↪ ↥K.parts)
have rw₁ : r ≤ Fintype.card.{u_1} ↥K.parts
Tactic: rw [Embedding.nonempty_iff_card_le,
        Fintype.card_fin, card_coe, K.card_parts.resolve_right ht]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (goal)
Goal:
α : Type u
G_1 : SimpleGraph α
s : Set α
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
ht : ¬t = 0
rw : Fintype.card (Fin r) ≤ Fintype.card.{u_1} ↥K.parts
rw₁ : r ≤ Fintype.card.{u_1} ↥K.parts
⊢ Nonempty.{max 1 (u_1 + 1)} (Fin r ↪ ↥K.parts)
have rw₂ : r ≤ #K.parts
Tactic: rw [Embedding.nonempty_iff_card_le,
        Fintype.card_fin, card_coe, K.card_parts.resolve_right ht]