awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
rw₂ : r ≤ #K.parts
⊢ Nonempty.{max 1 (u_1 + 1)} (Fin r ↪ ↥K.parts)
have rw₃ : r ≤ r
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 (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
⊢ (completeEquipartiteGraph r t).Copy G
have this : 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]
-- 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
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))
have rw : Fintype.card (Fin t) ≤ Fintype.card.{u_1} ↥(↑p : Finset V)
Tactic: rw [Embedding.nonempty_iff_card_le, Fintype.card_fin, card_coe, K.card_mem_parts p.prop]
-- 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
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)
⊢ Nonempty.{max 1 (u_1 + 1)} (Fin t ↪ ↥(↑p : Finset V))
have rw₁ : t ≤ Fintype.card.{u_1} ↥(↑p : Finset V)
Tactic: rw [Embedding.nonempty_iff_card_le, Fintype.card_fin, card_coe, K.card_mem_parts p.prop]
-- 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
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)
⊢ Nonempty.{max 1 (u_1 + 1)} (Fin t ↪ ↥(↑p : Finset V))
have rw₂ : t ≤ #(↑p : Finset V)
Tactic: rw [Embedding.nonempty_iff_card_le, Fintype.card_fin, card_coe, K.card_mem_parts p.prop]
-- 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
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)
⊢ Nonempty.{max 1 (u_1 + 1)} (Fin t ↪ ↥(↑p : Finset V))
have rw₃ : t ≤ t
Tactic: rw [Embedding.nonempty_iff_card_le, Fintype.card_fin, card_coe, K.card_mem_parts p.prop]
-- 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
this : Nonempty.{max 1 (u_1 + 1)} (Fin r ↪ ↥K.parts)
fᵣ : Fin r ↪ ↥K.parts := Classical.arbitrary (Fin r ↪ ↥K.parts)
⊢ (completeEquipartiteGraph r t).Copy G
have this₁ : ∀ (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]
-- 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
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))
⊢ Fin r × Fin t ↪ V
have 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)
Tactic: use fun (i, j) ↦ fₜ (fᵣ i) j
-- 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
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
⊢ ∀ ⦃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₂
have 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₂)
Tactic: (i₂, j₂)
-- 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
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₂))
⊢ (i₁, j₁) = (i₂, j₂)
have inj' : i₁ = i₂ ∧ j₁ = j₂
Tactic: rw [Prod.mk.injEq]
-- 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
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₂))
⊢ i₁ = i₂ ∧ j₁ = j₂
have 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)
Tactic: contrapose! heq with hne
Cleared hypotheses: heq
-- 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
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₂
⊢ 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)
have 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)
Tactic: rcases eq_or_ne i₁ i₂ with heq | hne
-- 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
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)
⊢ 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)
have 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)
Tactic: rcases eq_or_ne i₁ i₂ with heq | hne
-- 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
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.{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)
have 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))
Tactic: rw [heq, ← Subtype.ext_iff.ne]
-- 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
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)
have 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)
Tactic: refine (K.isCompleteBetween (fᵣ _).prop (fᵣ _).prop ?_ (fₜ _ _).prop (fₜ _ _).prop).ne
-- 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
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' := ⋯ }
⊢ (completeEquipartiteGraph r t).Copy G
have 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)
Tactic: refine ⟨⟨f, fun hne ↦ ?_⟩, f.injective⟩
-- 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
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)
have 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)
Tactic: refine K.isCompleteBetween (fᵣ _).prop (fᵣ _).prop ?_ (fₜ _ _).prop (fₜ _ _).prop
-- 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
f : (completeEquipartiteGraph r t).Copy G
⊢ G.CompleteEquipartiteSubgraph r t
have pos : (ht : t = 0) → G.CompleteEquipartiteSubgraph r t
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
f : (completeEquipartiteGraph r t).Copy G
pos : (ht : t = 0) → G.CompleteEquipartiteSubgraph r t
⊢ G.CompleteEquipartiteSubgraph r t
have neg : (ht : ¬t = 0) → G.CompleteEquipartiteSubgraph r t
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
f : (completeEquipartiteGraph r t).Copy G
ht : ¬t = 0
⊢ G.CompleteEquipartiteSubgraph r t
have neg : ∀ (i : Fin r) (x x_1 : Fin t)
  (h :
    Eq.{u_1 + 1} (α := V) ((fun (j : Fin t) ↦ ((f : (a : Fin r × Fin t) → V) (i, j) : V)) x)
      ((fun (j : Fin t) ↦ ((f : (a : Fin r × Fin t) → V) (i, j) : V)) x_1)),
  x = x_1
Tactic: refine ⟨univ.map ⟨fun i ↦ univ.map ⟨fun j ↦ f (i, j), fun _ _ h ↦ ?_⟩, fun i₁ i₂ h ↦ ?_⟩,
      ?_, fun h ↦ ?_, fun _ h₁ _ h₂ hne _ h₁' _ h₂' ↦ ?_⟩
-- 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
f : (completeEquipartiteGraph r t).Copy G
ht : ¬t = 0
neg :
  ∀ (i : Fin r) (x x_1 : Fin t)
    (h :
      Eq.{u_1 + 1} (α := V) ((fun (j : Fin t) ↦ ((f : (a : Fin r × Fin t) → V) (i, j) : V)) x)
        ((fun (j : Fin t) ↦ ((f : (a : Fin r × Fin t) → V) (i, j) : V)) x_1)),
    x = x_1
⊢ G.CompleteEquipartiteSubgraph r t
have neg₁ : ∀ (i₁ i₂ : Fin r)
  (h :
    Eq.{u_1 + 1} (α := Finset V)
      ((fun (i : Fin r) ↦
          (map (α := Fin t) { toFun := fun (j : Fin t) ↦ (f : (a : Fin r × Fin t) → V) (i, j), inj' := sorry } univ :
            Finset V))
        i₁)
      ((fun (i : Fin r) ↦
          (map (α := Fin t) { toFun := fun (j : Fin t) ↦ (f : (a : Fin r × Fin t) → V) (i, j), inj' := sorry } univ :
            Finset V))
        i₂)),
  i₁ = i₂
Tactic: refine ⟨univ.map ⟨fun i ↦ univ.map ⟨fun j ↦ f (i, j), fun _ _ h ↦ ?_⟩, fun i₁ i₂ h ↦ ?_⟩,
      ?_, fun h ↦ ?_, fun _ h₁ _ h₂ hne _ h₁' _ h₂' ↦ ?_⟩
-- 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
f : (completeEquipartiteGraph r t).Copy G
ht : ¬t = 0
neg :
  ∀ (i : Fin r) (x x_1 : Fin t)
    (h :
      Eq.{u_1 + 1} (α := V) ((fun (j : Fin t) ↦ ((f : (a : Fin r × Fin t) → V) (i, j) : V)) x)
        ((fun (j : Fin t) ↦ ((f : (a : Fin r × Fin t) → V) (i, j) : V)) x_1)),
    x = x_1
neg₁ :
  ∀ (i₁ i₂ : Fin r)
    (h :
      Eq.{u_1 + 1} (α := Finset V)
        ((fun (i : Fin r) ↦
            (map (α := Fin t) { toFun := fun (j : Fin t) ↦ (f : (a : Fin r × Fin t) → V) (i, j), inj' := ⋯ } univ :
              Finset V))
          i₁)
        ((fun (i : Fin r) ↦
            (map (α := Fin t) { toFun := fun (j : Fin t) ↦ (f : (a : Fin r × Fin t) → V) (i, j), inj' := ⋯ } univ :
              Finset V))
          i₂)),
    i₁ = i₂
⊢ G.CompleteEquipartiteSubgraph r t
have neg₂ : Finset.card.{u_1} (α := Finset V)
      (map (α := Fin r)
        {
          toFun := fun (i : Fin r) ↦
            map (α := Fin t) { toFun := fun (j : Fin t) ↦ (f : (a : Fin r × Fin t) → V) (i, j), inj' := sorry : Fin t ↪ V }
              univ,
          inj' := sorry : Fin r ↪ Finset V }
        univ) =
    r ∨
  t = 0
Tactic: refine ⟨univ.map ⟨fun i ↦ univ.map ⟨fun j ↦ f (i, j), fun _ _ h ↦ ?_⟩, fun i₁ i₂ h ↦ ?_⟩,
      ?_, fun h ↦ ?_, fun _ h₁ _ h₂ hne _ h₁' _ h₂' ↦ ?_⟩
-- 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
f : (completeEquipartiteGraph r t).Copy G
ht : ¬t = 0
neg :
  ∀ (i : Fin r) (x x_1 : Fin t)
    (h :
      Eq.{u_1 + 1} (α := V) ((fun (j : Fin t) ↦ ((f : (a : Fin r × Fin t) → V) (i, j) : V)) x)
        ((fun (j : Fin t) ↦ ((f : (a : Fin r × Fin t) → V) (i, j) : V)) x_1)),
    x = x_1
neg₁ :
  ∀ (i₁ i₂ : Fin r)
    (h :
      Eq.{u_1 + 1} (α := Finset V)
        ((fun (i : Fin r) ↦
            (map (α := Fin t) { toFun := fun (j : Fin t) ↦ (f : (a : Fin r × Fin t) → V) (i, j), inj' := ⋯ } univ :
              Finset V))
          i₁)
        ((fun (i : Fin r) ↦
            (map (α := Fin t) { toFun := fun (j : Fin t) ↦ (f : (a : Fin r × Fin t) → V) (i, j), inj' := ⋯ } univ :
              Finset V))
          i₂)),
    i₁ = i₂
neg₂ :
  Finset.card.{u_1} (α := Finset V)
        (map (α := Fin r)
          {
            toFun := fun (i : Fin r) ↦
              map (α := Fin t)
                { toFun := fun (j : Fin t) ↦ (f : (a : Fin r × Fin t) → V) (i, j), inj' := ⋯ : Fin t ↪ V } univ,
            inj' := ⋯ : Fin r ↪ Finset V }
          univ) =
      r ∨
    t = 0
⊢ G.CompleteEquipartiteSubgraph r t
have neg₃ : ∀ {p : Finset V}
  (h :
    Membership.mem (γ := Finset (Finset V))
      (map (α := Fin r)
        {
          toFun := fun (i : Fin r) ↦
            map (α := Fin t) { toFun := fun (j : Fin t) ↦ (f : (a : Fin r × Fin t) → V) (i, j), inj' := sorry } univ,
          inj' := sorry }
        univ)
      p),
  #p = t
Tactic: refine ⟨univ.map ⟨fun i ↦ univ.map ⟨fun j ↦ f (i, j), fun _ _ h ↦ ?_⟩, fun i₁ i₂ h ↦ ?_⟩,
      ?_, fun h ↦ ?_, fun _ h₁ _ h₂ hne _ h₁' _ h₂' ↦ ?_⟩