awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (goal)
Goal:
V : Type u_1
G : SimpleGraph V
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)
have 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)
Tactic: by_cases ht : t = 0
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (goal)
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)
⊢ 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)
have 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)
Tactic: by_cases ht : t = 0
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
r t : ℕ
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)
have this : ∀ (r' : ℕ), IsEmpty (Fin r' × Fin t)
Tactic: have (r' : ℕ) : IsEmpty (Fin r' × Fin t) := by simp [ht, Fin.isEmpty]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
r t : ℕ
ht : t = 0
this : ∀ (r' : ℕ), IsEmpty (Fin r' × Fin 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)
have h_bot : ∀ (r' : ℕ), completeEquipartiteGraph r' t = ⊥
Tactic: have h_bot (r' : ℕ) : completeEquipartiteGraph r' t = ⊥ :=
      completeEquipartiteGraph_eq_bot_iff.mpr <| .inr ht
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (goal)
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) (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)
have pos : IsContained (α := Fin (r + 1) × Fin t) ⊥ G ↔ Nonempty.{u_1 + 1} (G.CompleteEquipartiteSubgraph r t)
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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (goal)
Goal:
V : Type u_1
G : SimpleGraph V
r t : ℕ
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)
have 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)
Tactic: rw [completeEquipartiteGraph_isContained_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (goal)
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)
have 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)
Tactic: refine ⟨fun ⟨K'⟩ ↦ ?_, fun ⟨K, s, hs, hadj⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (goal)
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)
⊢ 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)
have 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)
Tactic: refine ⟨fun ⟨K'⟩ ↦ ?_, fun ⟨K, s, hs, hadj⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (goal)
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
⊢ ∃ (K : G.CompleteEquipartiteSubgraph r t) (s : Finset V),
    #s = t ∧ ∀ p ∈ K.parts, G.IsCompleteBetween (↑p : Set V) (↑s : Set V)
have 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)
Tactic: obtain ⟨parts, hparts_sub, hparts_card⟩ := K'.parts.exists_subset_card_eq (Nat.pred_le _)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (goal)
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
⊢ G.CompleteEquipartiteSubgraph r t
have refine : #parts = r ∨ t = 0
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⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (goal)
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
⊢ #parts = r ∨ t = 0
have rw : (r + 1).pred = r ∨ t = 0
Tactic: rw [hparts_card, K'.card_parts.resolve_right ht]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (goal)
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
have refine : #K.parts + 1 = #K'.parts
Tactic: refine exists_eq_insert_iff.mpr ⟨hparts_sub, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (goal)
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 := ⋯ }
⊢ #K.parts + 1 = #K'.parts
have rw : r + 1 = #K'.parts
Tactic: rw [K.card_parts.resolve_right ht, K'.card_parts.resolve_right ht]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (goal)
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
⊢ #K.parts + 1 = #K'.parts
have rw₁ : r + 1 = r + 1
Tactic: rw [K.card_parts.resolve_right ht, K'.card_parts.resolve_right ht]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (goal)
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 := ⋯ }
⊢ ∃ (K : G.CompleteEquipartiteSubgraph r t) (s : Finset V),
    #s = t ∧ ∀ p ∈ K.parts, G.IsCompleteBetween (↑p : Set V) (↑s : Set V)
have 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)
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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (hypothesis)
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
⊢ ∃ (K : G.CompleteEquipartiteSubgraph r t) (s : Finset V),
    #s = t ∧ ∀ p ∈ K.parts, G.IsCompleteBetween (↑p : Set V) (↑s : Set V)
have hs_mem : s ∈ K'.parts
Tactic: have hs_mem : s ∈ K'.parts := by simp [← hs]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (goal)
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)
have neg : s ∉ K.parts
Tactic: refine ⟨K.parts.cons s ?_, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (goal)
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
⊢ Nonempty.{u_1 + 1} (G.CompleteEquipartiteSubgraph (r + 1) t)
have neg₁ : #(cons s K.parts sorry) = r + 1 ∨ t = 0
Tactic: refine ⟨K.parts.cons s ?_, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (goal)
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
⊢ Nonempty.{u_1 + 1} (G.CompleteEquipartiteSubgraph (r + 1) t)
have neg₂ : ∀ {p : Finset V}, p ∈ cons s K.parts sorry → #p = t
Tactic: refine ⟨K.parts.cons s ?_, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (goal)
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
⊢ Nonempty.{u_1 + 1} (G.CompleteEquipartiteSubgraph (r + 1) t)
have neg₃ : (↑(cons s K.parts sorry) : Set (Finset V)).Pairwise fun (x1 x2 : Finset V) ↦ G.IsCompleteBetween (↑x1 : Set V) (↑x2 : Set V)
Tactic: refine ⟨K.parts.cons s ?_, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (goal)
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)
hs_mem : s ∈ K.parts
⊢ s.Nonempty
have rw : 0 < t
Tactic: rw [← Finset.card_pos, hs]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (goal)
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)
hs_mem : s ∈ K.parts
⊢ False
have neg : ∀ (v : V) (hv : v ∈ s), False
Tactic: obtain ⟨v, hv⟩ : s.Nonempty := by
          rw [← Finset.card_pos, hs]
          exact Nat.pos_of_ne_zero ht
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (goal)
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)
hs_mem : s ∈ K.parts
v : V
hv : v ∈ s
⊢ False
have neg : ¬G.Adj v v
Tactic: absurd hadj s hs_mem hv hv
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (goal)
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)
⊢ #(cons s K.parts ⋯) = r + 1 ∨ t = 0
have neg : r + 1 = r + 1 ∨ t = 0
Tactic: rw [Finset.card_cons, K.card_parts.resolve_right ht]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (goal)
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)
⊢ ∀ {p : Finset V}, p ∈ cons s K.parts ⋯ → #p = t
have neg : #s = t ∧ ∀ a ∈ K.parts, #a = t
Tactic: simp_rw [mem_cons, forall_eq_or_imp]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (goal)
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)
⊢ (↑(cons s K.parts ⋯) : Set (Finset V)).Pairwise fun (x1 x2 : Finset V) ↦
    G.IsCompleteBetween (↑x1 : Set V) (↑x2 : Set V)
have neg : (insert s (↑K.parts : Set (Finset V))).Pairwise fun (x1 x2 : Finset V) ↦ G.IsCompleteBetween (↑x1 : Set V) (↑x2 : Set V)
Tactic: rw [coe_cons]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (goal)
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)
⊢ (insert s (↑K.parts : Set (Finset V))).Pairwise fun (x1 x2 : Finset V) ↦
    G.IsCompleteBetween (↑x1 : Set V) (↑x2 : Set V)
have neg : Symmetric fun (x1 x2 : Finset V) ↦ G.IsCompleteBetween (↑x1 : Set V) (↑x2 : Set V)
Tactic: refine K.isCompleteBetween.insert_of_symmetric ?_ (fun p hp _ ↦ (hadj p hp).symm)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (goal)
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)
⊢ Symmetric fun (x1 x2 : Finset V) ↦ G.IsCompleteBetween (↑x1 : Set V) (↑x2 : Set V)
have neg : ∀ ⦃x y : Finset V⦄, G.IsCompleteBetween (↑x : Set V) (↑y : Set V) → G.IsCompleteBetween (↑y : Set V) (↑x : Set V)
Tactic: simp_rw [Symmetric, isCompleteBetween_comm, imp_self, implies_true]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (goal)
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 : ∀ ⦃x y : Finset V⦄, G.IsCompleteBetween (↑x : Set V) (↑y : Set V) → G.IsCompleteBetween (↑y : Set V) (↑x : Set V)
⊢ Symmetric fun (x1 x2 : Finset V) ↦ G.IsCompleteBetween (↑x1 : Set V) (↑x2 : Set V)
have neg₁ : ∀ ⦃x y : Finset V⦄, G.IsCompleteBetween (↑x : Set V) (↑y : Set V) → G.IsCompleteBetween (↑x : Set V) (↑y : Set V)
Tactic: simp_rw [Symmetric, isCompleteBetween_comm, imp_self, implies_true]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite (goal)
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 : ∀ ⦃x y : Finset V⦄, G.IsCompleteBetween (↑x : Set V) (↑y : Set V) → G.IsCompleteBetween (↑y : Set V) (↑x : Set V)
neg₁ : ∀ ⦃x y : Finset V⦄, G.IsCompleteBetween (↑x : Set V) (↑y : Set V) → G.IsCompleteBetween (↑x : Set V) (↑y : Set V)
⊢ Symmetric fun (x1 x2 : Finset V) ↦ G.IsCompleteBetween (↑x1 : Set V) (↑x2 : Set V)
have neg₂ : ∀ ⦃x y : Finset V⦄, True
Tactic: simp_rw [Symmetric, isCompleteBetween_comm, imp_self, implies_true]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
⊢ G.Reachable u v ↔ Relation.ReflTransGen G.Adj u v
have mp : G.Reachable u v → Relation.ReflTransGen G.Adj u v
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
mp : G.Reachable u v → Relation.ReflTransGen G.Adj u v
⊢ G.Reachable u v ↔ Relation.ReflTransGen G.Adj u v
have mpr : Relation.ReflTransGen G.Adj u v → G.Reachable u v
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
h : G.Walk u v
⊢ Relation.ReflTransGen G.Adj u v
have mp : ∀ {u : V}, Relation.ReflTransGen G.Adj u u
Tactic: induction h with
    | nil => rfl
    | cons h' _ ih => exact (Relation.ReflTransGen.single h').trans ih
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
h : G.Walk u v
mp : ∀ {u : V}, Relation.ReflTransGen G.Adj u u
⊢ Relation.ReflTransGen G.Adj u v
have mp₁ : ∀ {u v w : V} (h' : G.Adj u v) (p : G.Walk v w) (ih : Relation.ReflTransGen G.Adj v w), Relation.ReflTransGen G.Adj u w
Tactic: induction h with
    | nil => rfl
    | cons h' _ ih => exact (Relation.ReflTransGen.single h').trans ih
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
h : Relation.ReflTransGen G.Adj u v
⊢ G.Reachable u v
have mpr : G.Reachable u u
Tactic: induction h with
    | refl => rfl
    | tail _ ha hr => exact Reachable.trans hr ⟨Walk.cons ha Walk.nil⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
h : Relation.ReflTransGen G.Adj u v
mpr : G.Reachable u u
⊢ G.Reachable u v
have mpr₁ : ∀ {b c : V}, Relation.ReflTransGen G.Adj u b → ∀ (ha : G.Adj b c) (hr : G.Reachable u b), G.Reachable u c
Tactic: induction h with
    | refl => rfl
    | tail _ ha hr => exact Reachable.trans hr ⟨Walk.cons ha Walk.nil⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
G : SimpleGraph V
⊢ G.Reachable = Relation.ReflTransGen G.Adj
have h : ∀ (x x_1 : V), G.Reachable x x_1 ↔ Relation.ReflTransGen G.Adj x x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
s : Set (Sym2 V)
⊢ (fromEdgeSet s).Reachable = Relation.ReflTransGen (Sym2.ToRel s)
have rw : Relation.TransGen (Relation.ReflGen (fromEdgeSet s).Adj) = Relation.TransGen (Relation.ReflGen (Sym2.ToRel s))
Tactic: rw [reachable_eq_reflTransGen, ← Relation.transGen_reflGen, ← Relation.transGen_reflGen]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
s : Set (Sym2 V)
⊢ Relation.TransGen (Relation.ReflGen (fromEdgeSet s).Adj) = Relation.TransGen (Relation.ReflGen (Sym2.ToRel s))
have e_r : Relation.ReflGen (fromEdgeSet s).Adj = Relation.ReflGen (Sym2.ToRel s)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
s : Set (Sym2 V)
⊢ Relation.ReflGen (fromEdgeSet s).Adj = Relation.ReflGen (Sym2.ToRel s)
have e_r : ∀ (x x_1 : V), Relation.ReflGen (fromEdgeSet s).Adj x x_1 ↔ Relation.ReflGen (Sym2.ToRel s) x x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
s : Set (Sym2 V)
x x_1 : V
⊢ x_1 = x ∨ s(x, x_1) ∈ s ∧ ¬x = x_1 ↔ x_1 = x ∨ s(x, x_1) ∈ s
have mp : x_1 = x ∨ s(x, x_1) ∈ s ∧ ¬x = x_1 → x_1 = x ∨ s(x, x_1) ∈ s
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
s : Set (Sym2 V)
x x_1 : V
mp : x_1 = x ∨ s(x, x_1) ∈ s ∧ ¬x = x_1 → x_1 = x ∨ s(x, x_1) ∈ s
⊢ x_1 = x ∨ s(x, x_1) ∈ s ∧ ¬x = x_1 ↔ x_1 = x ∨ s(x, x_1) ∈ s
have mpr : x_1 = x ∨ s(x, x_1) ∈ s → x_1 = x ∨ s(x, x_1) ∈ s ∧ ¬x = x_1
Tactic: tauto