awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
⊢ #K.parts = r ∨ t = 0

Tactic:
K.card_parts

Premises used: SimpleGraph.CompleteEquipartiteSubgraph.card_parts
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
⊢ #K.parts = r ∨ t = 0

Tactic:
exact K.card_parts

Premises used: SimpleGraph.CompleteEquipartiteSubgraph.card_parts
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
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
neg : (ht : ¬t = 0) → (completeEquipartiteGraph r t).Copy G
⊢ (completeEquipartiteGraph r t).Copy G

Tactic:
by_cases ht : t = 0
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
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
pos : Copy (α := Fin r × Fin t) ⊥ G
⊢ (completeEquipartiteGraph r t).Copy G

Tactic:
rw [completeEquipartiteGraph_eq_bot_iff.mpr <| .inr ht]

Premises used: Iff.mpr, SimpleGraph.completeEquipartiteGraph_eq_bot_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
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
⊢ IsEmpty (Fin r × Fin t)

Tactic:
simp [ht, Fin.isEmpty]

Premises used: Fin.isEmpty
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
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
⊢ IsEmpty (Fin r × Fin t)

Tactic:
have : IsEmpty (Fin r × Fin t) := by simp [ht, Fin.isEmpty]
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
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
this : IsEmpty (Fin r × Fin t)
⊢ Copy (α := Fin r × Fin t) ⊥ G

Tactic:
exact Copy.bot .ofIsEmpty

Premises used: Function.Embedding.ofIsEmpty, SimpleGraph.Copy.bot
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
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
rw₂ : r ≤ #K.parts
rw₃ rw₄ : r ≤ r
⊢ Nonempty.{max 1 (u_1 + 1)} (Fin r ↪ ↥K.parts)

Tactic:
rw [Embedding.nonempty_iff_card_le,
        Fintype.card_fin, card_coe, K.card_parts.resolve_right ht]

Premises used: Fintype.card_fin, Function.Embedding.nonempty_iff_card_le, SimpleGraph.CompleteEquipartiteSubgraph.card_parts, Or.resolve_right, Fintype.card_coe
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
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)

Tactic:
have : Nonempty (Fin r ↪ K.parts) := by
      rw [Embedding.nonempty_iff_card_le,
        Fintype.card_fin, card_coe, K.card_parts.resolve_right ht]
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
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
this : Nonempty.{max 1 (u_1 + 1)} (Fin r ↪ ↥K.parts)
fᵣ : Fin r ↪ ↥K.parts := Classical.arbitrary (Fin r ↪ ↥K.parts)
p : ↥K.parts
rw : Fintype.card (Fin t) ≤ Fintype.card.{u_1} ↥(↑p : Finset V)
rw₁ : t ≤ Fintype.card.{u_1} ↥(↑p : Finset V)
rw₂ : t ≤ #(↑p : Finset V)
rw₃ rw₄ : t ≤ t
⊢ Nonempty.{max 1 (u_1 + 1)} (Fin t ↪ ↥(↑p : Finset V))

Tactic:
rw [Embedding.nonempty_iff_card_le, Fintype.card_fin, card_coe, K.card_mem_parts p.prop]

Premises used: Fintype.card_fin, Function.Embedding.nonempty_iff_card_le, Subtype.prop, SimpleGraph.CompleteEquipartiteSubgraph.card_mem_parts, Fintype.card_coe
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
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
this : Nonempty.{max 1 (u_1 + 1)} (Fin r ↪ ↥K.parts)
fᵣ : Fin r ↪ ↥K.parts := Classical.arbitrary (Fin r ↪ ↥K.parts)
⊢ ∀ (p : ↥K.parts), Nonempty.{max 1 (u_1 + 1)} (Fin t ↪ ↥(↑p : Finset V))

Tactic:
have (p : K.parts) : Nonempty (Fin t ↪ p) := by
      rw [Embedding.nonempty_iff_card_le, Fintype.card_fin, card_coe, K.card_mem_parts p.prop]
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
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
this_1 : Nonempty.{max 1 (u_1 + 1)} (Fin r ↪ ↥K.parts)
fᵣ : Fin r ↪ ↥K.parts := Classical.arbitrary (Fin r ↪ ↥K.parts)
this : ∀ (p : ↥K.parts), Nonempty.{max 1 (u_1 + 1)} (Fin t ↪ ↥(↑p : Finset V))
fₜ : (p : ↥K.parts) → Fin t ↪ ↥(↑p : Finset V) := fun (p : ↥K.parts) ↦ Classical.arbitrary (Fin t ↪ ↥(↑p : Finset V))
inj' :
  Injective.{1, u_1 + 1} (β := V) fun (x : Fin r × Fin t) ↦
    match (motive := Fin r × Fin t → V) x with
    | (i, j) =>
      (↑((fₜ ((fᵣ : (a : Fin r) → ↥K.parts) i) : (a : Fin t) → ↥(↑((fᵣ : (a : Fin r) → ↥K.parts) i) : Finset V)) j) : V)
⊢ Fin r × Fin t ↪ V

Tactic:
use fun (i, j) ↦ fₜ (fᵣ i) j
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
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
this_1 : Nonempty.{max 1 (u_1 + 1)} (Fin r ↪ ↥K.parts)
fᵣ : Fin r ↪ ↥K.parts := Classical.arbitrary (Fin r ↪ ↥K.parts)
this : ∀ (p : ↥K.parts), Nonempty.{max 1 (u_1 + 1)} (Fin t ↪ ↥(↑p : Finset V))
fₜ : (p : ↥K.parts) → Fin t ↪ ↥(↑p : Finset V) := fun (p : ↥K.parts) ↦ Classical.arbitrary (Fin t ↪ ↥(↑p : Finset V))
i₁ : Fin r
j₁ : Fin t
inj' :
  ∀ (i₂ : Fin r) (j₂ : Fin t),
    Eq.{u_1 + 1} (α := V)
        ((fun (x : Fin r × Fin t) ↦
            (match (motive := Fin r × Fin t → V) x with
              | (i, j) =>
                (↑((fₜ ((fᵣ : (a : Fin r) → ↥K.parts) i) :
                        (a : Fin t) → ↥(↑((fᵣ : (a : Fin r) → ↥K.parts) i) : Finset V))
                      j) :
                  V) :
              V))
          (i₁, j₁))
        ((fun (x : Fin r × Fin t) ↦
            (match (motive := Fin r × Fin t → V) x with
              | (i, j) =>
                (↑((fₜ ((fᵣ : (a : Fin r) → ↥K.parts) i) :
                        (a : Fin t) → ↥(↑((fᵣ : (a : Fin r) → ↥K.parts) i) : Finset V))
                      j) :
                  V) :
              V))
          (i₂, j₂)) →
      (i₁, j₁) = (i₂, j₂)
⊢ ∀ ⦃a₂ : Fin r × Fin t⦄,
    Eq.{u_1 + 1} (α := V)
        ((fun (x : Fin r × Fin t) ↦
            (match (motive := Fin r × Fin t → V) x with
              | (i, j) =>
                (↑((fₜ ((fᵣ : (a : Fin r) → ↥K.parts) i) :
                        (a : Fin t) → ↥(↑((fᵣ : (a : Fin r) → ↥K.parts) i) : Finset V))
                      j) :
                  V) :
              V))
          (i₁, j₁))
        ((fun (x : Fin r × Fin t) ↦
            (match (motive := Fin r × Fin t → V) x with
              | (i, j) =>
                (↑((fₜ ((fᵣ : (a : Fin r) → ↥K.parts) i) :
                        (a : Fin t) → ↥(↑((fᵣ : (a : Fin r) → ↥K.parts) i) : Finset V))
                      j) :
                  V) :
              V))
          a₂) →
      (i₁, j₁) = a₂

Tactic:
(i₂, j₂)
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
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
this_1 : Nonempty.{max 1 (u_1 + 1)} (Fin r ↪ ↥K.parts)
fᵣ : Fin r ↪ ↥K.parts := Classical.arbitrary (Fin r ↪ ↥K.parts)
this : ∀ (p : ↥K.parts), Nonempty.{max 1 (u_1 + 1)} (Fin t ↪ ↥(↑p : Finset V))
fₜ : (p : ↥K.parts) → Fin t ↪ ↥(↑p : Finset V) := fun (p : ↥K.parts) ↦ Classical.arbitrary (Fin t ↪ ↥(↑p : Finset V))
i₁ : Fin r
j₁ : Fin t
i₂ : Fin r
j₂ : Fin t
heq :
  Eq.{u_1 + 1} (α := V)
    ((fun (x : Fin r × Fin t) ↦
        (match (motive := Fin r × Fin t → V) x with
          | (i, j) =>
            (↑((fₜ ((fᵣ : (a : Fin r) → ↥K.parts) i) : (a : Fin t) → ↥(↑((fᵣ : (a : Fin r) → ↥K.parts) i) : Finset V))
                  j) :
              V) :
          V))
      (i₁, j₁))
    ((fun (x : Fin r × Fin t) ↦
        (match (motive := Fin r × Fin t → V) x with
          | (i, j) =>
            (↑((fₜ ((fᵣ : (a : Fin r) → ↥K.parts) i) : (a : Fin t) → ↥(↑((fᵣ : (a : Fin r) → ↥K.parts) i) : Finset V))
                  j) :
              V) :
          V))
      (i₂, j₂))
inj' : i₁ = i₂ ∧ j₁ = j₂
⊢ (i₁, j₁) = (i₂, j₂)

Tactic:
rw [Prod.mk.injEq]

Premises used: Prod.mk.injEq
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
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
this_1 : Nonempty.{max 1 (u_1 + 1)} (Fin r ↪ ↥K.parts)
fᵣ : Fin r ↪ ↥K.parts := Classical.arbitrary (Fin r ↪ ↥K.parts)
this : ∀ (p : ↥K.parts), Nonempty.{max 1 (u_1 + 1)} (Fin t ↪ ↥(↑p : Finset V))
fₜ : (p : ↥K.parts) → Fin t ↪ ↥(↑p : Finset V) := fun (p : ↥K.parts) ↦ Classical.arbitrary (Fin t ↪ ↥(↑p : Finset V))
i₁ : Fin r
j₁ : Fin t
i₂ : Fin r
j₂ : Fin t
heq :
  Eq.{u_1 + 1} (α := V)
    ((fun (x : Fin r × Fin t) ↦
        (match (motive := Fin r × Fin t → V) x with
          | (i, j) =>
            (↑((fₜ ((fᵣ : (a : Fin r) → ↥K.parts) i) : (a : Fin t) → ↥(↑((fᵣ : (a : Fin r) → ↥K.parts) i) : Finset V))
                  j) :
              V) :
          V))
      (i₁, j₁))
    ((fun (x : Fin r × Fin t) ↦
        (match (motive := Fin r × Fin t → V) x with
          | (i, j) =>
            (↑((fₜ ((fᵣ : (a : Fin r) → ↥K.parts) i) : (a : Fin t) → ↥(↑((fᵣ : (a : Fin r) → ↥K.parts) i) : Finset V))
                  j) :
              V) :
          V))
      (i₂, j₂))
inj' :
  ∀ (hne : ∀ (_ : i₁ = i₂), j₁ ≠ j₂),
    Ne.{u_1 + 1} (α := V)
      (↑((fₜ ((fᵣ : (a : Fin r) → ↥K.parts) i₁) : (a : Fin t) → ↥(↑((fᵣ : (a : Fin r) → ↥K.parts) i₁) : Finset V)) j₁) :
        V)
      (↑((fₜ ((fᵣ : (a : Fin r) → ↥K.parts) i₂) : (a : Fin t) → ↥(↑((fᵣ : (a : Fin r) → ↥K.parts) i₂) : Finset V)) j₂) :
        V)
⊢ i₁ = i₂ ∧ j₁ = j₂

Tactic:
contrapose! heq with hne
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
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
this_1 : Nonempty.{max 1 (u_1 + 1)} (Fin r ↪ ↥K.parts)
fᵣ : Fin r ↪ ↥K.parts := Classical.arbitrary (Fin r ↪ ↥K.parts)
this : ∀ (p : ↥K.parts), Nonempty.{max 1 (u_1 + 1)} (Fin t ↪ ↥(↑p : Finset V))
fₜ : (p : ↥K.parts) → Fin t ↪ ↥(↑p : Finset V) := fun (p : ↥K.parts) ↦ Classical.arbitrary (Fin t ↪ ↥(↑p : Finset V))
i₁ : Fin r
j₁ : Fin t
i₂ : Fin r
j₂ : Fin t
hne : ∀ (_ : i₁ = i₂), j₁ ≠ j₂
inj' :
  ∀ (heq : i₁ = i₂),
    Ne.{u_1 + 1} (α := V)
      (↑((fₜ ((fᵣ : (a : Fin r) → ↥K.parts) i₁) : (a : Fin t) → ↥(↑((fᵣ : (a : Fin r) → ↥K.parts) i₁) : Finset V)) j₁) :
        V)
      (↑((fₜ ((fᵣ : (a : Fin r) → ↥K.parts) i₂) : (a : Fin t) → ↥(↑((fᵣ : (a : Fin r) → ↥K.parts) i₂) : Finset V)) j₂) :
        V)
inj'₁ :
  ∀ (hne : i₁ ≠ i₂),
    Ne.{u_1 + 1} (α := V)
      (↑((fₜ ((fᵣ : (a : Fin r) → ↥K.parts) i₁) : (a : Fin t) → ↥(↑((fᵣ : (a : Fin r) → ↥K.parts) i₁) : Finset V)) j₁) :
        V)
      (↑((fₜ ((fᵣ : (a : Fin r) → ↥K.parts) i₂) : (a : Fin t) → ↥(↑((fᵣ : (a : Fin r) → ↥K.parts) i₂) : Finset V)) j₂) :
        V)
⊢ Ne.{u_1 + 1} (α := V)
    (↑((fₜ ((fᵣ : (a : Fin r) → ↥K.parts) i₁) : (a : Fin t) → ↥(↑((fᵣ : (a : Fin r) → ↥K.parts) i₁) : Finset V)) j₁) :
      V)
    (↑((fₜ ((fᵣ : (a : Fin r) → ↥K.parts) i₂) : (a : Fin t) → ↥(↑((fᵣ : (a : Fin r) → ↥K.parts) i₂) : Finset V)) j₂) :
      V)

Tactic:
rcases eq_or_ne i₁ i₂ with heq | hne

Premises used: eq_or_ne
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
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
this_1 : Nonempty.{max 1 (u_1 + 1)} (Fin r ↪ ↥K.parts)
fᵣ : Fin r ↪ ↥K.parts := Classical.arbitrary (Fin r ↪ ↥K.parts)
this : ∀ (p : ↥K.parts), Nonempty.{max 1 (u_1 + 1)} (Fin t ↪ ↥(↑p : Finset V))
fₜ : (p : ↥K.parts) → Fin t ↪ ↥(↑p : Finset V) := fun (p : ↥K.parts) ↦ Classical.arbitrary (Fin t ↪ ↥(↑p : Finset V))
i₁ : Fin r
j₁ : Fin t
i₂ : Fin r
j₂ : Fin t
hne : ∀ (_ : i₁ = i₂), j₁ ≠ j₂
heq : i₁ = i₂
inj' :
  Ne.{max 1 (u_1 + 1)} (α := ↥(↑((fᵣ : (a : Fin r) → ↥K.parts) i₂) : Finset V))
    ((fₜ ((fᵣ : (a : Fin r) → ↥K.parts) i₂) : (a : Fin t) → ↥(↑((fᵣ : (a : Fin r) → ↥K.parts) i₂) : Finset V)) j₁ :
      ↥(↑((fᵣ : (a : Fin r) → ↥K.parts) i₂) : Finset V))
    ((fₜ ((fᵣ : (a : Fin r) → ↥K.parts) i₂) : (a : Fin t) → ↥(↑((fᵣ : (a : Fin r) → ↥K.parts) i₂) : Finset V)) j₂ :
      ↥(↑((fᵣ : (a : Fin r) → ↥K.parts) i₂) : Finset V))
⊢ Ne.{u_1 + 1} (α := V)
    (↑((fₜ ((fᵣ : (a : Fin r) → ↥K.parts) i₁) : (a : Fin t) → ↥(↑((fᵣ : (a : Fin r) → ↥K.parts) i₁) : Finset V)) j₁) :
      V)
    (↑((fₜ ((fᵣ : (a : Fin r) → ↥K.parts) i₂) : (a : Fin t) → ↥(↑((fᵣ : (a : Fin r) → ↥K.parts) i₂) : Finset V)) j₂) :
      V)

Tactic:
rw [heq, ← Subtype.ext_iff.ne]

Premises used: Subtype.ext_iff, Iff.ne
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
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
this_1 : Nonempty.{max 1 (u_1 + 1)} (Fin r ↪ ↥K.parts)
fᵣ : Fin r ↪ ↥K.parts := Classical.arbitrary (Fin r ↪ ↥K.parts)
this : ∀ (p : ↥K.parts), Nonempty.{max 1 (u_1 + 1)} (Fin t ↪ ↥(↑p : Finset V))
fₜ : (p : ↥K.parts) → Fin t ↪ ↥(↑p : Finset V) := fun (p : ↥K.parts) ↦ Classical.arbitrary (Fin t ↪ ↥(↑p : Finset V))
i₁ : Fin r
j₁ : Fin t
i₂ : Fin r
j₂ : Fin t
hne : ∀ (_ : i₁ = i₂), j₁ ≠ j₂
heq : i₁ = i₂
⊢ Ne.{max 1 (u_1 + 1)} (α := ↥(↑((fᵣ : (a : Fin r) → ↥K.parts) i₂) : Finset V))
    ((fₜ ((fᵣ : (a : Fin r) → ↥K.parts) i₂) : (a : Fin t) → ↥(↑((fᵣ : (a : Fin r) → ↥K.parts) i₂) : Finset V)) j₁ :
      ↥(↑((fᵣ : (a : Fin r) → ↥K.parts) i₂) : Finset V))
    ((fₜ ((fᵣ : (a : Fin r) → ↥K.parts) i₂) : (a : Fin t) → ↥(↑((fᵣ : (a : Fin r) → ↥K.parts) i₂) : Finset V)) j₂ :
      ↥(↑((fᵣ : (a : Fin r) → ↥K.parts) i₂) : Finset V))

Tactic:
(fₜ _).injective.ne (hne heq)

Premises used: Function.Injective.ne, Function.Embedding.injective
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
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
this_1 : Nonempty.{max 1 (u_1 + 1)} (Fin r ↪ ↥K.parts)
fᵣ : Fin r ↪ ↥K.parts := Classical.arbitrary (Fin r ↪ ↥K.parts)
this : ∀ (p : ↥K.parts), Nonempty.{max 1 (u_1 + 1)} (Fin t ↪ ↥(↑p : Finset V))
fₜ : (p : ↥K.parts) → Fin t ↪ ↥(↑p : Finset V) := fun (p : ↥K.parts) ↦ Classical.arbitrary (Fin t ↪ ↥(↑p : Finset V))
i₁ : Fin r
j₁ : Fin t
i₂ : Fin r
j₂ : Fin t
hne : ∀ (_ : i₁ = i₂), j₁ ≠ j₂
heq : i₁ = i₂
⊢ Ne.{max 1 (u_1 + 1)} (α := ↥(↑((fᵣ : (a : Fin r) → ↥K.parts) i₂) : Finset V))
    ((fₜ ((fᵣ : (a : Fin r) → ↥K.parts) i₂) : (a : Fin t) → ↥(↑((fᵣ : (a : Fin r) → ↥K.parts) i₂) : Finset V)) j₁ :
      ↥(↑((fᵣ : (a : Fin r) → ↥K.parts) i₂) : Finset V))
    ((fₜ ((fᵣ : (a : Fin r) → ↥K.parts) i₂) : (a : Fin t) → ↥(↑((fᵣ : (a : Fin r) → ↥K.parts) i₂) : Finset V)) j₂ :
      ↥(↑((fᵣ : (a : Fin r) → ↥K.parts) i₂) : Finset V))

Tactic:
exact (fₜ _).injective.ne (hne heq)

Premises used: Function.Injective.ne, Function.Embedding.injective
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
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
this_1 : Nonempty.{max 1 (u_1 + 1)} (Fin r ↪ ↥K.parts)
fᵣ : Fin r ↪ ↥K.parts := Classical.arbitrary (Fin r ↪ ↥K.parts)
this : ∀ (p : ↥K.parts), Nonempty.{max 1 (u_1 + 1)} (Fin t ↪ ↥(↑p : Finset V))
fₜ : (p : ↥K.parts) → Fin t ↪ ↥(↑p : Finset V) := fun (p : ↥K.parts) ↦ Classical.arbitrary (Fin t ↪ ↥(↑p : Finset V))
i₁ : Fin r
j₁ : Fin t
i₂ : Fin r
j₂ : Fin t
hne_1 : ∀ (_ : i₁ = i₂), j₁ ≠ j₂
hne : i₁ ≠ i₂
⊢ Ne.{u_1 + 1} (α := V)
    (↑((fₜ ((fᵣ : (a : Fin r) → ↥K.parts) i₁) : (a : Fin t) → ↥(↑((fᵣ : (a : Fin r) → ↥K.parts) i₁) : Finset V)) j₁) :
      V)
    (↑((fₜ ((fᵣ : (a : Fin r) → ↥K.parts) i₂) : (a : Fin t) → ↥(↑((fᵣ : (a : Fin r) → ↥K.parts) i₂) : Finset V)) j₂) :
      V)

Tactic:
(K.isCompleteBetween (fᵣ _).prop (fᵣ _).prop ?_ (fₜ _ _).prop (fₜ _ _).prop).ne

Premises used: SimpleGraph.CompleteEquipartiteSubgraph.isCompleteBetween, SimpleGraph.Adj.ne, Subtype.prop, DFunLike.coe
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
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
this_1 : Nonempty.{max 1 (u_1 + 1)} (Fin r ↪ ↥K.parts)
fᵣ : Fin r ↪ ↥K.parts := Classical.arbitrary (Fin r ↪ ↥K.parts)
this : ∀ (p : ↥K.parts), Nonempty.{max 1 (u_1 + 1)} (Fin t ↪ ↥(↑p : Finset V))
fₜ : (p : ↥K.parts) → Fin t ↪ ↥(↑p : Finset V) := fun (p : ↥K.parts) ↦ Classical.arbitrary (Fin t ↪ ↥(↑p : Finset V))
i₁ : Fin r
j₁ : Fin t
i₂ : Fin r
j₂ : Fin t
hne_1 : ∀ (_ : i₁ = i₂), j₁ ≠ j₂
hne : i₁ ≠ i₂
inj' :
  Ne.{u_1 + 1} (α := Finset V) (↑((fᵣ : (a : Fin r) → ↥K.parts) i₁) : Finset V)
    (↑((fᵣ : (a : Fin r) → ↥K.parts) i₂) : Finset V)
⊢ Ne.{u_1 + 1} (α := V)
    (↑((fₜ ((fᵣ : (a : Fin r) → ↥K.parts) i₁) : (a : Fin t) → ↥(↑((fᵣ : (a : Fin r) → ↥K.parts) i₁) : Finset V)) j₁) :
      V)
    (↑((fₜ ((fᵣ : (a : Fin r) → ↥K.parts) i₂) : (a : Fin t) → ↥(↑((fᵣ : (a : Fin r) → ↥K.parts) i₂) : Finset V)) j₂) :
      V)

Tactic:
refine (K.isCompleteBetween (fᵣ _).prop (fᵣ _).prop ?_ (fₜ _ _).prop (fₜ _ _).prop).ne

Premises used: SimpleGraph.CompleteEquipartiteSubgraph.isCompleteBetween, SimpleGraph.Adj.ne, Subtype.prop, DFunLike.coe
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
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
this_1 : Nonempty.{max 1 (u_1 + 1)} (Fin r ↪ ↥K.parts)
fᵣ : Fin r ↪ ↥K.parts := Classical.arbitrary (Fin r ↪ ↥K.parts)
this : ∀ (p : ↥K.parts), Nonempty.{max 1 (u_1 + 1)} (Fin t ↪ ↥(↑p : Finset V))
fₜ : (p : ↥K.parts) → Fin t ↪ ↥(↑p : Finset V) := fun (p : ↥K.parts) ↦ Classical.arbitrary (Fin t ↪ ↥(↑p : Finset V))
i₁ : Fin r
j₁ : Fin t
i₂ : Fin r
j₂ : Fin t
hne_1 : ∀ (_ : i₁ = i₂), j₁ ≠ j₂
hne : i₁ ≠ i₂
⊢ Ne.{u_1 + 1} (α := Finset V) (↑((fᵣ : (a : Fin r) → ↥K.parts) i₁) : Finset V)
    (↑((fᵣ : (a : Fin r) → ↥K.parts) i₂) : Finset V)

Tactic:
Subtype.ext_iff.ne.mp <| fᵣ.injective.ne hne

Premises used: Function.Injective.ne, Subtype.ext_iff, Iff.ne, Iff.mp, Function.Embedding.injective
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
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
this_1 : Nonempty.{max 1 (u_1 + 1)} (Fin r ↪ ↥K.parts)
fᵣ : Fin r ↪ ↥K.parts := Classical.arbitrary (Fin r ↪ ↥K.parts)
this : ∀ (p : ↥K.parts), Nonempty.{max 1 (u_1 + 1)} (Fin t ↪ ↥(↑p : Finset V))
fₜ : (p : ↥K.parts) → Fin t ↪ ↥(↑p : Finset V) := fun (p : ↥K.parts) ↦ Classical.arbitrary (Fin t ↪ ↥(↑p : Finset V))
i₁ : Fin r
j₁ : Fin t
i₂ : Fin r
j₂ : Fin t
hne_1 : ∀ (_ : i₁ = i₂), j₁ ≠ j₂
hne : i₁ ≠ i₂
⊢ Ne.{u_1 + 1} (α := Finset V) (↑((fᵣ : (a : Fin r) → ↥K.parts) i₁) : Finset V)
    (↑((fᵣ : (a : Fin r) → ↥K.parts) i₂) : Finset V)

Tactic:
exact Subtype.ext_iff.ne.mp <| fᵣ.injective.ne hne

Premises used: Function.Injective.ne, Subtype.ext_iff, Iff.ne, Iff.mp, Function.Embedding.injective
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
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
this_1 : Nonempty.{max 1 (u_1 + 1)} (Fin r ↪ ↥K.parts)
fᵣ : Fin r ↪ ↥K.parts := Classical.arbitrary (Fin r ↪ ↥K.parts)
this : ∀ (p : ↥K.parts), Nonempty.{max 1 (u_1 + 1)} (Fin t ↪ ↥(↑p : Finset V))
fₜ : (p : ↥K.parts) → Fin t ↪ ↥(↑p : Finset V) := fun (p : ↥K.parts) ↦ Classical.arbitrary (Fin t ↪ ↥(↑p : Finset V))
f : Fin r × Fin t ↪ V :=
  {
    toFun := fun (x : Fin r × Fin t) ↦
      match (motive := Fin r × Fin t → V) x with
      | (i, j) =>
        (↑((fₜ ((fᵣ : (a : Fin r) → ↥K.parts) i) : (a : Fin t) → ↥(↑((fᵣ : (a : Fin r) → ↥K.parts) i) : Finset V)) j) :
          V),
    inj' := ⋯ }
neg :
  ∀ {a b : Fin r × Fin t} (hne : (completeEquipartiteGraph r t).Adj a b),
    G.Adj ((f : (a : Fin r × Fin t) → V) a) ((f : (a : Fin r × Fin t) → V) b)
⊢ (completeEquipartiteGraph r t).Copy G

Tactic:
refine ⟨⟨f, fun hne ↦ ?_⟩, f.injective⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
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
this_1 : Nonempty.{max 1 (u_1 + 1)} (Fin r ↪ ↥K.parts)
fᵣ : Fin r ↪ ↥K.parts := Classical.arbitrary (Fin r ↪ ↥K.parts)
this : ∀ (p : ↥K.parts), Nonempty.{max 1 (u_1 + 1)} (Fin t ↪ ↥(↑p : Finset V))
fₜ : (p : ↥K.parts) → Fin t ↪ ↥(↑p : Finset V) := fun (p : ↥K.parts) ↦ Classical.arbitrary (Fin t ↪ ↥(↑p : Finset V))
f : Fin r × Fin t ↪ V :=
  {
    toFun := fun (x : Fin r × Fin t) ↦
      match (motive := Fin r × Fin t → V) x with
      | (i, j) =>
        (↑((fₜ ((fᵣ : (a : Fin r) → ↥K.parts) i) : (a : Fin t) → ↥(↑((fᵣ : (a : Fin r) → ↥K.parts) i) : Finset V)) j) :
          V),
    inj' := ⋯ }
a b : Fin r × Fin t
hne : (completeEquipartiteGraph r t).Adj a b
⊢ G.Adj ((f : (a : Fin r × Fin t) → V) a) ((f : (a : Fin r × Fin t) → V) b)

Tactic:
K.isCompleteBetween (fᵣ _).prop (fᵣ _).prop ?_ (fₜ _ _).prop (fₜ _ _).prop

Premises used: SimpleGraph.CompleteEquipartiteSubgraph.isCompleteBetween, Subtype.prop, DFunLike.coe
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
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
this_1 : Nonempty.{max 1 (u_1 + 1)} (Fin r ↪ ↥K.parts)
fᵣ : Fin r ↪ ↥K.parts := Classical.arbitrary (Fin r ↪ ↥K.parts)
this : ∀ (p : ↥K.parts), Nonempty.{max 1 (u_1 + 1)} (Fin t ↪ ↥(↑p : Finset V))
fₜ : (p : ↥K.parts) → Fin t ↪ ↥(↑p : Finset V) := fun (p : ↥K.parts) ↦ Classical.arbitrary (Fin t ↪ ↥(↑p : Finset V))
f : Fin r × Fin t ↪ V :=
  {
    toFun := fun (x : Fin r × Fin t) ↦
      match (motive := Fin r × Fin t → V) x with
      | (i, j) =>
        (↑((fₜ ((fᵣ : (a : Fin r) → ↥K.parts) i) : (a : Fin t) → ↥(↑((fᵣ : (a : Fin r) → ↥K.parts) i) : Finset V)) j) :
          V),
    inj' := ⋯ }
a b : Fin r × Fin t
hne : (completeEquipartiteGraph r t).Adj a b
neg :
  Ne.{u_1 + 1} (α := Finset V) (↑((fᵣ : (a : Fin r) → ↥K.parts) a.1) : Finset V)
    (↑((fᵣ : (a : Fin r) → ↥K.parts) b.1) : Finset V)
⊢ G.Adj ((f : (a : Fin r × Fin t) → V) a) ((f : (a : Fin r × Fin t) → V) b)

Tactic:
refine K.isCompleteBetween (fᵣ _).prop (fᵣ _).prop ?_ (fₜ _ _).prop (fₜ _ _).prop

Premises used: SimpleGraph.CompleteEquipartiteSubgraph.isCompleteBetween, Subtype.prop, DFunLike.coe