awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
f : (completeEquipartiteGraph r t).Copy G
ht : ¬t = 0
x x_1 : Finset V
hne : x ≠ x_1
x_2 x_3 : V
w : Fin r
h₁' :
  x_2 ∈
    (↑(map (α := Fin t) { toFun := fun (j : Fin t) ↦ (f : (a : Fin r × Fin t) → V) (w, j), inj' := ⋯ : Fin t ↪ V }
          univ) :
      Set V)
h₁ : map (α := Fin t) { toFun := fun (j : Fin t) ↦ (f : (a : Fin r × Fin t) → V) (w, j), inj' := ⋯ } univ = x
w_1 : Fin r
h₂' :
  x_3 ∈
    (↑(map (α := Fin t) { toFun := fun (j : Fin t) ↦ (f : (a : Fin r × Fin t) → V) (w_1, j), inj' := ⋯ : Fin t ↪ V }
          univ) :
      Set V)
h₂ : map (α := Fin t) { toFun := fun (j : Fin t) ↦ (f : (a : Fin r × Fin t) → V) (w_1, j), inj' := ⋯ } univ = x_1
h₁'₁ : ∃ (y : Fin t), (f : (a : Fin r × Fin t) → V) (w, y) = x_2
⊢ ∃ (y : Fin t), (f : (a : Fin r × Fin t) → V) (w_1, y) = x_3

Tactic:
simp_rw [coe_map, Embedding.coeFn_mk, coe_univ, Set.image_univ, Set.mem_range] at h₁' h₂'

Premises used: Set.image_univ, Set.mem_range, Finset.coe_univ, Function.Embedding.coeFn_mk, Finset.coe_map
-- 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
f : (completeEquipartiteGraph r t).Copy G
ht : ¬t = 0
x x_1 : Finset V
hne : x ≠ x_1
x_2 x_3 : V
w : Fin r
h₁ : map (α := Fin t) { toFun := fun (j : Fin t) ↦ (f : (a : Fin r × Fin t) → V) (w, j), inj' := ⋯ } univ = x
w_1 : Fin r
h₂ : map (α := Fin t) { toFun := fun (j : Fin t) ↦ (f : (a : Fin r × Fin t) → V) (w_1, j), inj' := ⋯ } univ = x_1
h₁' : ∃ (y : Fin t), (f : (a : Fin r × Fin t) → V) (w, y) = x_2
h₂' : ∃ (y : Fin t), (f : (a : Fin r × Fin t) → V) (w_1, y) = x_3
neg : ∀ (w_2 : Fin t) (h₁' : (f : (a : Fin r × Fin t) → V) (w, w_2) = x_2), G.Adj x_2 x_3
⊢ G.Adj x_2 x_3

Tactic:
replace ⟨_, h₁'⟩ := h₁'
-- 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
f : (completeEquipartiteGraph r t).Copy G
ht : ¬t = 0
x x_1 : Finset V
hne : x ≠ x_1
x_2 x_3 : V
w : Fin r
h₁ : map (α := Fin t) { toFun := fun (j : Fin t) ↦ (f : (a : Fin r × Fin t) → V) (w, j), inj' := ⋯ } univ = x
w_1 : Fin r
h₂ : map (α := Fin t) { toFun := fun (j : Fin t) ↦ (f : (a : Fin r × Fin t) → V) (w_1, j), inj' := ⋯ } univ = x_1
h₂' : ∃ (y : Fin t), (f : (a : Fin r × Fin t) → V) (w_1, y) = x_3
w_2 : Fin t
h₁' : (f : (a : Fin r × Fin t) → V) (w, w_2) = x_2
neg : ∀ (w : Fin t) (h₂' : (f : (a : Fin r × Fin t) → V) (w_1, w) = x_3), G.Adj x_2 x_3
⊢ G.Adj x_2 x_3

Tactic:
replace ⟨_, h₂'⟩ := h₂'
-- 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
f : (completeEquipartiteGraph r t).Copy G
ht : ¬t = 0
x x_1 : Finset V
hne : x ≠ x_1
x_2 x_3 : V
w : Fin r
h₁ : map (α := Fin t) { toFun := fun (j : Fin t) ↦ (f : (a : Fin r × Fin t) → V) (w, j), inj' := ⋯ } univ = x
w_1 : Fin r
h₂ : map (α := Fin t) { toFun := fun (j : Fin t) ↦ (f : (a : Fin r × Fin t) → V) (w_1, j), inj' := ⋯ } univ = x_1
w_2 : Fin t
h₁' : (f : (a : Fin r × Fin t) → V) (w, w_2) = x_2
w_3 : Fin t
h₂' : (f : (a : Fin r × Fin t) → V) (w_1, w_3) = x_3
neg : G.Adj ((f : (a : Fin r × Fin t) → V) (w, w_2)) ((f : (a : Fin r × Fin t) → V) (w_1, w_3))
⊢ G.Adj x_2 x_3

Tactic:
rw [← h₁', ← h₂']
-- 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
f : (completeEquipartiteGraph r t).Copy G
ht : ¬t = 0
x x_1 : Finset V
hne : x ≠ x_1
x_2 x_3 : V
w : Fin r
h₁ : map (α := Fin t) { toFun := fun (j : Fin t) ↦ (f : (a : Fin r × Fin t) → V) (w, j), inj' := ⋯ } univ = x
w_1 : Fin r
h₂ : map (α := Fin t) { toFun := fun (j : Fin t) ↦ (f : (a : Fin r × Fin t) → V) (w_1, j), inj' := ⋯ } univ = x_1
w_2 : Fin t
h₁' : (f : (a : Fin r × Fin t) → V) (w, w_2) = x_2
w_3 : Fin t
h₂' : (f : (a : Fin r × Fin t) → V) (w_1, w_3) = x_3
neg : (completeEquipartiteGraph r t).Adj (w, w_2) (w_1, w_3)
⊢ G.Adj ((f : (a : Fin r × Fin t) → V) (w, w_2)) ((f : (a : Fin r × Fin t) → V) (w_1, w_3))

Tactic:
apply f.toHom.map_adj

Premises used: SimpleGraph.Hom.map_adj, SimpleGraph.Copy.toHom
-- 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
f : (completeEquipartiteGraph r t).Copy G
ht : ¬t = 0
x x_1 : Finset V
hne : x ≠ x_1
x_2 x_3 : V
w : Fin r
h₁ : map (α := Fin t) { toFun := fun (j : Fin t) ↦ (f : (a : Fin r × Fin t) → V) (w, j), inj' := ⋯ } univ = x
w_1 : Fin r
h₂ : map (α := Fin t) { toFun := fun (j : Fin t) ↦ (f : (a : Fin r × Fin t) → V) (w_1, j), inj' := ⋯ } univ = x_1
w_2 : Fin t
h₁' : (f : (a : Fin r × Fin t) → V) (w, w_2) = x_2
w_3 : Fin t
h₂' : (f : (a : Fin r × Fin t) → V) (w_1, w_3) = x_3
neg : w ≠ w_1
⊢ (completeEquipartiteGraph r t).Adj (w, w_2) (w_1, w_3)

Tactic:
simp_rw [completeEquipartiteGraph_adj]

Premises used: SimpleGraph.completeEquipartiteGraph_adj
-- 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
f : (completeEquipartiteGraph r t).Copy G
ht : ¬t = 0
x x_1 : Finset V
hne : x ≠ x_1
x_2 x_3 : V
w : Fin r
h₁ : map (α := Fin t) { toFun := fun (j : Fin t) ↦ (f : (a : Fin r × Fin t) → V) (w, j), inj' := ⋯ } univ = x
w_1 : Fin r
h₂ : map (α := Fin t) { toFun := fun (j : Fin t) ↦ (f : (a : Fin r × Fin t) → V) (w_1, j), inj' := ⋯ } univ = x_1
w_2 : Fin t
h₁' : (f : (a : Fin r × Fin t) → V) (w, w_2) = x_2
w_3 : Fin t
h₂' : (f : (a : Fin r × Fin t) → V) (w_1, w_3) = x_3
neg : ∀ (heq : w = w_1), x = x_1
⊢ w ≠ w_1

Tactic:
contrapose hne with heq
-- 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
f : (completeEquipartiteGraph r t).Copy G
ht : ¬t = 0
x x_1 : Finset V
x_2 x_3 : V
w : Fin r
h₁ : map (α := Fin t) { toFun := fun (j : Fin t) ↦ (f : (a : Fin r × Fin t) → V) (w, j), inj' := ⋯ } univ = x
w_1 : Fin r
h₂ : map (α := Fin t) { toFun := fun (j : Fin t) ↦ (f : (a : Fin r × Fin t) → V) (w_1, j), inj' := ⋯ } univ = x_1
w_2 : Fin t
h₁' : (f : (a : Fin r × Fin t) → V) (w, w_2) = x_2
w_3 : Fin t
h₂' : (f : (a : Fin r × Fin t) → V) (w_1, w_3) = x_3
heq : w = w_1
neg : map (α := Fin t) { toFun := fun (j : Fin t) ↦ (f : (a : Fin r × Fin t) → V) (w, j), inj' := ⋯ } univ = x_1
neg₁ :
  Eq.{u_1 + 1} (α := Finset V)
    (map (α := Fin t) { toFun := fun (j : Fin t) ↦ (f : (a : Fin r × Fin t) → V) (w, j), inj' := ⋯ } univ)
    (map (α := Fin t) { toFun := fun (j : Fin t) ↦ (f : (a : Fin r × Fin t) → V) (w_1, j), inj' := ⋯ } univ)
⊢ x = x_1

Tactic:
simp_rw [← h₁, ← h₂, heq]
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
V : Type u_1
G : SimpleGraph V
r t : ℕ
⊢ completeEquipartiteGraph r t ⊑ G ↔ Nonempty.{u_1 + 1} (G.CompleteEquipartiteSubgraph r t)

Tactic:
⟨fun ⟨f⟩ ↦ ⟨CompleteEquipartiteSubgraph.ofCopy f⟩, fun ⟨K⟩ ↦ ⟨K.toCopy⟩⟩

Premises used: SimpleGraph.IsContained, SimpleGraph.CompleteEquipartiteSubgraph.toCopy, SimpleGraph.CompleteEquipartiteSubgraph.ofCopy, _private.0.SimpleGraph.completeEquipartiteGraph_isContained_iff.match_2, _private.0.SimpleGraph.completeEquipartiteGraph_isContained_iff.match_1, Nonempty.intro, Iff.intro, Nonempty, SimpleGraph.CompleteEquipartiteSubgraph, SimpleGraph.completeEquipartiteGraph
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
V : Type u_1
G : SimpleGraph V
r t : ℕ
pos :
  ∀ (ht : t = 0),
    IsContained (α := Fin (r + 1) × Fin t) (completeEquipartiteGraph (r + 1) t) G ↔
      ∃ (K : G.CompleteEquipartiteSubgraph r t) (s : Finset V),
        #s = t ∧ ∀ p ∈ K.parts, G.IsCompleteBetween (↑p : Set V) (↑s : Set V)
neg :
  ∀ (ht : ¬t = 0),
    IsContained (α := Fin (r + 1) × Fin t) (completeEquipartiteGraph (r + 1) t) G ↔
      ∃ (K : G.CompleteEquipartiteSubgraph r t) (s : Finset V),
        #s = t ∧ ∀ p ∈ K.parts, G.IsCompleteBetween (↑p : Set V) (↑s : Set V)
⊢ IsContained (α := Fin (r + 1) × Fin t) (completeEquipartiteGraph (r + 1) t) G ↔
    ∃ (K : G.CompleteEquipartiteSubgraph r t) (s : Finset V),
      #s = t ∧ ∀ p ∈ K.parts, G.IsCompleteBetween (↑p : Set V) (↑s : Set V)

Tactic:
by_cases ht : t = 0
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
V : Type u_1
G : SimpleGraph V
r t : ℕ
ht : t = 0
r' : ℕ
⊢ IsEmpty (Fin r' × Fin t)

Tactic:
simp [ht, Fin.isEmpty]

Premises used: Fin.isEmpty
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
V : Type u_1
G : SimpleGraph V
r t : ℕ
ht : t = 0
⊢ ∀ (r' : ℕ), IsEmpty (Fin r' × Fin t)

Tactic:
have (r' : ℕ) : IsEmpty (Fin r' × Fin t) := by simp [ht, Fin.isEmpty]
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
V : Type u_1
G : SimpleGraph V
r t : ℕ
ht : t = 0
this : ∀ (r' : ℕ), IsEmpty (Fin r' × Fin t)
⊢ ∀ (r' : ℕ), completeEquipartiteGraph r' t = ⊥

Tactic:
have h_bot (r' : ℕ) : completeEquipartiteGraph r' t = ⊥ :=
      completeEquipartiteGraph_eq_bot_iff.mpr <| .inr ht
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
V : Type u_1
G : SimpleGraph V
r t : ℕ
ht : t = 0
this : ∀ (r' : ℕ), IsEmpty (Fin r' × Fin t)
h_bot : ∀ (r' : ℕ), completeEquipartiteGraph r' t = ⊥
pos : IsContained (α := Fin (r + 1) × Fin t) ⊥ G ↔ Nonempty.{u_1 + 1} (G.CompleteEquipartiteSubgraph r t)
⊢ IsContained (α := Fin (r + 1) × Fin t) (completeEquipartiteGraph (r + 1) t) G ↔
    ∃ (K : G.CompleteEquipartiteSubgraph r t) (s : Finset V),
      #s = t ∧ ∀ p ∈ K.parts, G.IsCompleteBetween (↑p : Set V) (↑s : Set V)

Tactic:
simp_rw [h_bot (r + 1), ht, Finset.card_eq_zero, exists_eq_left, IsCompleteBetween, mem_coe,
      notMem_empty, IsEmpty.forall_iff, implies_true, exists_true_iff_nonempty]

Premises used: exists_true_iff_nonempty, exists_eq_left, Finset.notMem_empty, SimpleGraph.IsCompleteBetween, HAdd.hAdd, Finset.card_eq_zero, implies_true, OfNat.ofNat, Finset.mem_coe, IsEmpty.forall_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
V : Type u_1
G : SimpleGraph V
r t : ℕ
ht : t = 0
this : ∀ (r' : ℕ), IsEmpty (Fin r' × Fin t)
h_bot : ∀ (r' : ℕ), completeEquipartiteGraph r' t = ⊥
⊢ IsContained (α := Fin (r + 1) × Fin t) ⊥ G ↔ Nonempty.{u_1 + 1} (G.CompleteEquipartiteSubgraph r t)

Tactic:
⟨fun _ ↦ CompleteEquipartiteSubgraph.nonempty_of_eq_zero_or_eq_zero (.inr ht),
      fun _ ↦ ⟨Copy.bot .ofIsEmpty⟩⟩

Premises used: Function.Embedding.ofIsEmpty, SimpleGraph.CompleteEquipartiteSubgraph.nonempty_of_eq_zero_or_eq_zero, Nonempty.intro, Iff.intro, SimpleGraph.Copy.bot, Or.inr
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
V : Type u_1
G : SimpleGraph V
r t : ℕ
ht : t = 0
this : ∀ (r' : ℕ), IsEmpty (Fin r' × Fin t)
h_bot : ∀ (r' : ℕ), completeEquipartiteGraph r' t = ⊥
⊢ IsContained (α := Fin (r + 1) × Fin t) ⊥ G ↔ Nonempty.{u_1 + 1} (G.CompleteEquipartiteSubgraph r t)

Tactic:
exact ⟨fun _ ↦ CompleteEquipartiteSubgraph.nonempty_of_eq_zero_or_eq_zero (.inr ht),
      fun _ ↦ ⟨Copy.bot .ofIsEmpty⟩⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
V : Type u_1
G : SimpleGraph V
r t : ℕ
ht : ¬t = 0
neg :
  Nonempty.{u_1 + 1} (G.CompleteEquipartiteSubgraph (r + 1) t) ↔
    ∃ (K : G.CompleteEquipartiteSubgraph r t) (s : Finset V),
      #s = t ∧ ∀ p ∈ K.parts, G.IsCompleteBetween (↑p : Set V) (↑s : Set V)
⊢ IsContained (α := Fin (r + 1) × Fin t) (completeEquipartiteGraph (r + 1) t) G ↔
    ∃ (K : G.CompleteEquipartiteSubgraph r t) (s : Finset V),
      #s = t ∧ ∀ p ∈ K.parts, G.IsCompleteBetween (↑p : Set V) (↑s : Set V)

Tactic:
rw [completeEquipartiteGraph_isContained_iff]

Premises used: SimpleGraph.completeEquipartiteGraph_isContained_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
V : Type u_1
G : SimpleGraph V
r t : ℕ
ht : ¬t = 0
⊢ Nonempty.{u_1 + 1} (G.CompleteEquipartiteSubgraph (r + 1) t) ↔
    ∃ (K : G.CompleteEquipartiteSubgraph r t) (s : Finset V),
      #s = t ∧ ∀ p ∈ K.parts, G.IsCompleteBetween (↑p : Set V) (↑s : Set V)

Tactic:
⟨fun ⟨K'⟩ ↦ ?_, fun ⟨K, s, hs, hadj⟩ ↦ ?_⟩

Premises used: _private.0.SimpleGraph.completeEquipartiteGraph_succ_isContained_iff.match_7, Exists, And, HAdd.hAdd, Iff.intro, Finset.card, Nonempty, _private.0.SimpleGraph.completeEquipartiteGraph_succ_isContained_iff.match_6, SimpleGraph.CompleteEquipartiteSubgraph, OfNat.ofNat, Eq
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
V : Type u_1
G : SimpleGraph V
r t : ℕ
ht : ¬t = 0
neg :
  Nonempty.{u_1 + 1} (G.CompleteEquipartiteSubgraph (r + 1) t) →
    ∀ (K' : G.CompleteEquipartiteSubgraph (r + 1) t),
      ∃ (K : G.CompleteEquipartiteSubgraph r t) (s : Finset V),
        #s = t ∧ ∀ p ∈ K.parts, G.IsCompleteBetween (↑p : Set V) (↑s : Set V)
neg₁ :
  (∃ (K : G.CompleteEquipartiteSubgraph r t) (s : Finset V),
      #s = t ∧ ∀ p ∈ K.parts, G.IsCompleteBetween (↑p : Set V) (↑s : Set V)) →
    ∀ (K : G.CompleteEquipartiteSubgraph r t) (s : Finset V) (hs : #s = t)
      (hadj : ∀ p ∈ K.parts, G.IsCompleteBetween (↑p : Set V) (↑s : Set V)),
      Nonempty.{u_1 + 1} (G.CompleteEquipartiteSubgraph (r + 1) t)
⊢ Nonempty.{u_1 + 1} (G.CompleteEquipartiteSubgraph (r + 1) t) ↔
    ∃ (K : G.CompleteEquipartiteSubgraph r t) (s : Finset V),
      #s = t ∧ ∀ p ∈ K.parts, G.IsCompleteBetween (↑p : Set V) (↑s : Set V)

Tactic:
refine ⟨fun ⟨K'⟩ ↦ ?_, fun ⟨K, s, hs, hadj⟩ ↦ ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
V : Type u_1
G : SimpleGraph V
r t : ℕ
ht : ¬t = 0
h : Nonempty.{u_1 + 1} (G.CompleteEquipartiteSubgraph (r + 1) t)
K' : G.CompleteEquipartiteSubgraph (r + 1) t
neg :
  ∀ (parts : Finset (Finset V)) (hparts_sub : parts ⊆ K'.parts) (hparts_card : #parts = (#K'.parts).pred),
    ∃ (K : G.CompleteEquipartiteSubgraph r t) (s : Finset V),
      #s = t ∧ ∀ p ∈ K.parts, G.IsCompleteBetween (↑p : Set V) (↑s : Set V)
⊢ ∃ (K : G.CompleteEquipartiteSubgraph r t) (s : Finset V),
    #s = t ∧ ∀ p ∈ K.parts, G.IsCompleteBetween (↑p : Set V) (↑s : Set V)

Tactic:
obtain ⟨parts, hparts_sub, hparts_card⟩ := K'.parts.exists_subset_card_eq (Nat.pred_le _)

Premises used: Finset.exists_subset_card_eq, Nat.pred_le
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
V : Type u_1
G : SimpleGraph V
r t : ℕ
ht : ¬t = 0
h : Nonempty.{u_1 + 1} (G.CompleteEquipartiteSubgraph (r + 1) t)
K' : G.CompleteEquipartiteSubgraph (r + 1) t
parts : Finset (Finset V)
hparts_sub : parts ⊆ K'.parts
hparts_card : #parts = (#K'.parts).pred
refine : #parts = r ∨ t = 0
⊢ G.CompleteEquipartiteSubgraph r t

Tactic:
refine ⟨parts, ?_, fun h ↦ K'.card_mem_parts (hparts_sub h),
          fun _ h₁ _ h₂ hne ↦ K'.isCompleteBetween (hparts_sub h₁) (hparts_sub h₂) hne⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
V : Type u_1
G : SimpleGraph V
r t : ℕ
ht : ¬t = 0
h : Nonempty.{u_1 + 1} (G.CompleteEquipartiteSubgraph (r + 1) t)
K' : G.CompleteEquipartiteSubgraph (r + 1) t
parts : Finset (Finset V)
hparts_sub : parts ⊆ K'.parts
hparts_card : #parts = (#K'.parts).pred
rw : (r + 1).pred = r ∨ t = 0
⊢ #parts = r ∨ t = 0

Tactic:
rw [hparts_card, K'.card_parts.resolve_right ht]

Premises used: SimpleGraph.CompleteEquipartiteSubgraph.card_parts, Or.resolve_right
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
V : Type u_1
G : SimpleGraph V
r t : ℕ
ht : ¬t = 0
h : Nonempty.{u_1 + 1} (G.CompleteEquipartiteSubgraph (r + 1) t)
K' : G.CompleteEquipartiteSubgraph (r + 1) t
parts : Finset (Finset V)
hparts_sub : parts ⊆ K'.parts
hparts_card : #parts = (#K'.parts).pred
⊢ (r + 1).pred = r ∨ t = 0

Tactic:
.inl (Nat.pred_succ r)

Premises used: Nat.pred_succ, Or.inl
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
V : Type u_1
G : SimpleGraph V
r t : ℕ
ht : ¬t = 0
h : Nonempty.{u_1 + 1} (G.CompleteEquipartiteSubgraph (r + 1) t)
K' : G.CompleteEquipartiteSubgraph (r + 1) t
parts : Finset (Finset V)
hparts_sub : parts ⊆ K'.parts
hparts_card : #parts = (#K'.parts).pred
⊢ (r + 1).pred = r ∨ t = 0

Tactic:
exact .inl (Nat.pred_succ r)
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
V : Type u_1
G : SimpleGraph V
r t : ℕ
ht : ¬t = 0
h : Nonempty.{u_1 + 1} (G.CompleteEquipartiteSubgraph (r + 1) t)
K' : G.CompleteEquipartiteSubgraph (r + 1) t
parts : Finset (Finset V)
hparts_sub : parts ⊆ K'.parts
hparts_card : #parts = (#K'.parts).pred
K : G.CompleteEquipartiteSubgraph r t :=
  { parts := parts, card_parts := ⋯, card_mem_parts := ⋯, isCompleteBetween := ⋯ }
⊢ ∃ s ∉ K.parts, insert s K.parts = K'.parts

Tactic:
exists_eq_insert_iff.mpr ⟨hparts_sub, ?_⟩

Premises used: Iff.mpr, And.intro, Finset.exists_eq_insert_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
V : Type u_1
G : SimpleGraph V
r t : ℕ
ht : ¬t = 0
h : Nonempty.{u_1 + 1} (G.CompleteEquipartiteSubgraph (r + 1) t)
K' : G.CompleteEquipartiteSubgraph (r + 1) t
parts : Finset (Finset V)
hparts_sub : parts ⊆ K'.parts
hparts_card : #parts = (#K'.parts).pred
K : G.CompleteEquipartiteSubgraph r t :=
  { parts := parts, card_parts := ⋯, card_mem_parts := ⋯, isCompleteBetween := ⋯ }
refine : #K.parts + 1 = #K'.parts
⊢ ∃ s ∉ K.parts, insert s K.parts = K'.parts

Tactic:
refine exists_eq_insert_iff.mpr ⟨hparts_sub, ?_⟩

Premises used: Iff.mpr, And.intro, Finset.exists_eq_insert_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
V : Type u_1
G : SimpleGraph V
r t : ℕ
ht : ¬t = 0
h : Nonempty.{u_1 + 1} (G.CompleteEquipartiteSubgraph (r + 1) t)
K' : G.CompleteEquipartiteSubgraph (r + 1) t
parts : Finset (Finset V)
hparts_sub : parts ⊆ K'.parts
hparts_card : #parts = (#K'.parts).pred
K : G.CompleteEquipartiteSubgraph r t :=
  { parts := parts, card_parts := ⋯, card_mem_parts := ⋯, isCompleteBetween := ⋯ }
rw : r + 1 = #K'.parts
rw₁ rw₂ : r + 1 = r + 1
⊢ #K.parts + 1 = #K'.parts

Tactic:
rw [K.card_parts.resolve_right ht, K'.card_parts.resolve_right ht]

Premises used: SimpleGraph.CompleteEquipartiteSubgraph.card_parts, Or.resolve_right
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
V : Type u_1
G : SimpleGraph V
r t : ℕ
ht : ¬t = 0
h : Nonempty.{u_1 + 1} (G.CompleteEquipartiteSubgraph (r + 1) t)
K' : G.CompleteEquipartiteSubgraph (r + 1) t
parts : Finset (Finset V)
hparts_sub : parts ⊆ K'.parts
hparts_card : #parts = (#K'.parts).pred
K : G.CompleteEquipartiteSubgraph r t :=
  { parts := parts, card_parts := ⋯, card_mem_parts := ⋯, isCompleteBetween := ⋯ }
neg :
  ∀ (s : Finset V) (nhs_mem : s ∉ K.parts) (hs : insert s K.parts = K'.parts),
    ∃ (K : G.CompleteEquipartiteSubgraph r t) (s : Finset V),
      #s = t ∧ ∀ p ∈ K.parts, G.IsCompleteBetween (↑p : Set V) (↑s : Set V)
⊢ ∃ (K : G.CompleteEquipartiteSubgraph r t) (s : Finset V),
    #s = t ∧ ∀ p ∈ K.parts, G.IsCompleteBetween (↑p : Set V) (↑s : Set V)

Tactic:
obtain ⟨s, nhs_mem, hs⟩ : ∃ s ∉ K.parts, insert s K.parts = K'.parts := by
        refine exists_eq_insert_iff.mpr ⟨hparts_sub, ?_⟩
        rw [K.card_parts.resolve_right ht, K'.card_parts.resolve_right ht]

Premises used: SimpleGraph.CompleteEquipartiteSubgraph.parts
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
V : Type u_1
G : SimpleGraph V
r t : ℕ
ht : ¬t = 0
h : Nonempty.{u_1 + 1} (G.CompleteEquipartiteSubgraph (r + 1) t)
K' : G.CompleteEquipartiteSubgraph (r + 1) t
parts : Finset (Finset V)
hparts_sub : parts ⊆ K'.parts
hparts_card : #parts = (#K'.parts).pred
K : G.CompleteEquipartiteSubgraph r t :=
  { parts := parts, card_parts := ⋯, card_mem_parts := ⋯, isCompleteBetween := ⋯ }
s : Finset V
nhs_mem : s ∉ K.parts
hs : insert s K.parts = K'.parts
⊢ s ∈ K'.parts

Tactic:
simp [← hs]
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
V : Type u_1
G : SimpleGraph V
r t : ℕ
ht : ¬t = 0
h : Nonempty.{u_1 + 1} (G.CompleteEquipartiteSubgraph (r + 1) t)
K' : G.CompleteEquipartiteSubgraph (r + 1) t
parts : Finset (Finset V)
hparts_sub : parts ⊆ K'.parts
hparts_card : #parts = (#K'.parts).pred
K : G.CompleteEquipartiteSubgraph r t :=
  { parts := parts, card_parts := ⋯, card_mem_parts := ⋯, isCompleteBetween := ⋯ }
s : Finset V
nhs_mem : s ∉ K.parts
hs : insert s K.parts = K'.parts
⊢ s ∈ K'.parts

Tactic:
have hs_mem : s ∈ K'.parts := by simp [← hs]
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
V : Type u_1
G : SimpleGraph V
r t : ℕ
ht : ¬t = 0
h : Nonempty.{u_1 + 1} (G.CompleteEquipartiteSubgraph (r + 1) t)
K' : G.CompleteEquipartiteSubgraph (r + 1) t
parts : Finset (Finset V)
hparts_sub : parts ⊆ K'.parts
hparts_card : #parts = (#K'.parts).pred
K : G.CompleteEquipartiteSubgraph r t :=
  { parts := parts, card_parts := ⋯, card_mem_parts := ⋯, isCompleteBetween := ⋯ }
s : Finset V
nhs_mem : s ∉ K.parts
hs : insert s K.parts = K'.parts
hs_mem : s ∈ K'.parts
⊢ ∃ (K : G.CompleteEquipartiteSubgraph r t) (s : Finset V),
    #s = t ∧ ∀ p ∈ K.parts, G.IsCompleteBetween (↑p : Set V) (↑s : Set V)

Tactic:
⟨K, s, K'.card_mem_parts hs_mem,
        fun _ h ↦ K'.isCompleteBetween (hparts_sub h) hs_mem (ne_of_mem_of_not_mem h nhs_mem)⟩

Premises used: SimpleGraph.CompleteEquipartiteSubgraph.isCompleteBetween, ne_of_mem_of_not_mem, And.intro, Exists.intro, SimpleGraph.CompleteEquipartiteSubgraph.card_mem_parts
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
V : Type u_1
G : SimpleGraph V
r t : ℕ
ht : ¬t = 0
h : Nonempty.{u_1 + 1} (G.CompleteEquipartiteSubgraph (r + 1) t)
K' : G.CompleteEquipartiteSubgraph (r + 1) t
parts : Finset (Finset V)
hparts_sub : parts ⊆ K'.parts
hparts_card : #parts = (#K'.parts).pred
K : G.CompleteEquipartiteSubgraph r t :=
  { parts := parts, card_parts := ⋯, card_mem_parts := ⋯, isCompleteBetween := ⋯ }
s : Finset V
nhs_mem : s ∉ K.parts
hs : insert s K.parts = K'.parts
hs_mem : s ∈ K'.parts
⊢ ∃ (K : G.CompleteEquipartiteSubgraph r t) (s : Finset V),
    #s = t ∧ ∀ p ∈ K.parts, G.IsCompleteBetween (↑p : Set V) (↑s : Set V)

Tactic:
exact ⟨K, s, K'.card_mem_parts hs_mem,
        fun _ h ↦ K'.isCompleteBetween (hparts_sub h) hs_mem (ne_of_mem_of_not_mem h nhs_mem)⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
V : Type u_1
G : SimpleGraph V
r t : ℕ
ht : ¬t = 0
h :
  ∃ (K : G.CompleteEquipartiteSubgraph r t) (s : Finset V),
    #s = t ∧ ∀ p ∈ K.parts, G.IsCompleteBetween (↑p : Set V) (↑s : Set V)
K : G.CompleteEquipartiteSubgraph r t
s : Finset V
hs : #s = t
hadj : ∀ p ∈ K.parts, G.IsCompleteBetween (↑p : Set V) (↑s : Set V)
⊢ Nonempty.{u_1 + 1} (G.CompleteEquipartiteSubgraph (r + 1) t)

Tactic:
⟨K.parts.cons s ?_, ?_, ?_, ?_⟩

Premises used: Finset.cons, Nonempty.intro, SimpleGraph.CompleteEquipartiteSubgraph.mk, SimpleGraph.CompleteEquipartiteSubgraph.parts
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
V : Type u_1
G : SimpleGraph V
r t : ℕ
ht : ¬t = 0
h :
  ∃ (K : G.CompleteEquipartiteSubgraph r t) (s : Finset V),
    #s = t ∧ ∀ p ∈ K.parts, G.IsCompleteBetween (↑p : Set V) (↑s : Set V)
K : G.CompleteEquipartiteSubgraph r t
s : Finset V
hs : #s = t
hadj : ∀ p ∈ K.parts, G.IsCompleteBetween (↑p : Set V) (↑s : Set V)
neg : s ∉ K.parts
neg₁ : #(cons s K.parts ⋯) = r + 1 ∨ t = 0
neg₂ : ∀ {p : Finset V}, p ∈ cons s K.parts ⋯ → #p = t
neg₃ :
  (↑(cons s K.parts ⋯) : Set (Finset V)).Pairwise fun (x1 x2 : Finset V) ↦
    G.IsCompleteBetween (↑x1 : Set V) (↑x2 : Set V)
⊢ Nonempty.{u_1 + 1} (G.CompleteEquipartiteSubgraph (r + 1) t)

Tactic:
refine ⟨K.parts.cons s ?_, ?_, ?_, ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
V : Type u_1
G : SimpleGraph V
r t : ℕ
ht : ¬t = 0
h :
  ∃ (K : G.CompleteEquipartiteSubgraph r t) (s : Finset V),
    #s = t ∧ ∀ p ∈ K.parts, G.IsCompleteBetween (↑p : Set V) (↑s : Set V)
K : G.CompleteEquipartiteSubgraph r t
s : Finset V
hs : #s = t
hadj : ∀ p ∈ K.parts, G.IsCompleteBetween (↑p : Set V) (↑s : Set V)
neg : ∀ (hs_mem : s ∈ K.parts), False
⊢ s ∉ K.parts

Tactic:
by_contra! hs_mem