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
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
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' := ⋯ } univ,
            inj' := ⋯ }
          univ)
        p),
    #p = t
⊢ G.CompleteEquipartiteSubgraph r t
have neg₄ : ∀ (x : Finset V)
  (h₁ :
    x ∈
      (↑(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) :
        Set (Finset V)))
  (x_1 : Finset V)
  (h₂ :
    x_1 ∈
      (↑(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) :
        Set (Finset V)))
  (hne : x ≠ x_1) (x_2 : V) (h₁' : x_2 ∈ (↑x : Set V)) (x : V) (h₂' : x ∈ (↑x_1 : Set V)), G.Adj x_2 x
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 (hypothesis)
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
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₂
have h₁ : ∀ (a : V),
  Membership.mem (γ := Finset V)
      (map (α := Fin t) { toFun := fun (j : Fin t) ↦ (f : (a : Fin r × Fin t) → V) (i₁, j), inj' := sorry } univ) a ↔
    Membership.mem (γ := Finset V)
      (map (α := Fin t) { toFun := fun (j : Fin t) ↦ (f : (a : Fin r × Fin t) → V) (i₂, j), inj' := sorry } univ) a
Tactic: simp_rw [Finset.ext_iff] at h
Cleared hypotheses: h
-- 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
f : (completeEquipartiteGraph r t).Copy G
ht : ¬t = 0
i₁ i₂ : Fin r
h :
  ∀ (a : V),
    Membership.mem (γ := Finset V)
        (map (α := Fin t) { toFun := fun (j : Fin t) ↦ (f : (a : Fin r × Fin t) → V) (i₁, j), inj' := ⋯ } univ) a ↔
      Membership.mem (γ := Finset V)
        (map (α := Fin t) { toFun := fun (j : Fin t) ↦ (f : (a : Fin r × Fin t) → V) (i₂, j), inj' := ⋯ } univ) a
⊢ i₁ = i₂
have this : NeZero t
Tactic: have : NeZero t := ⟨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
f : (completeEquipartiteGraph r t).Copy G
ht : ¬t = 0
i₁ i₂ : Fin r
h :
  ∀ (a : V),
    Membership.mem (γ := Finset V)
        (map (α := Fin t) { toFun := fun (j : Fin t) ↦ (f : (a : Fin r × Fin t) → V) (i₁, j), inj' := ⋯ } univ) a ↔
      Membership.mem (γ := Finset V)
        (map (α := Fin t) { toFun := fun (j : Fin t) ↦ (f : (a : Fin r × Fin t) → V) (i₂, j), inj' := ⋯ } univ) a
this : NeZero t
⊢ i₁ = i₂
have neg : ∀ (w : Fin t)
  (heq : Eq (α := V) ((f : (a : Fin r × Fin t) → V) (i₁, w) : V) ((f : (a : Fin r × Fin t) → V) (i₂, 0) : V)), i₁ = i₂
Tactic: obtain ⟨_, heq⟩ : ∃ j, f (i₁, j) = f (i₂, 0) := by simpa using h <| f (i₂, 0)
-- 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
f : (completeEquipartiteGraph r t).Copy G
ht : ¬t = 0
i₁ i₂ : Fin r
h :
  ∀ (a : V),
    Membership.mem (γ := Finset V)
        (map (α := Fin t) { toFun := fun (j : Fin t) ↦ (f : (a : Fin r × Fin t) → V) (i₁, j), inj' := ⋯ } univ) a ↔
      Membership.mem (γ := Finset V)
        (map (α := Fin t) { toFun := fun (j : Fin t) ↦ (f : (a : Fin r × Fin t) → V) (i₂, j), inj' := ⋯ } univ) a
this : NeZero t
w : Fin t
heq : Eq (α := V) ((f : (a : Fin r × Fin t) → V) (i₁, w) : V) ((f : (a : Fin r × Fin t) → V) (i₂, 0) : V)
⊢ i₁ = i₂
have heq₁ : (i₁, w) = (i₂, 0)
Tactic: apply f.injective at heq
Cleared hypotheses: heq
-- 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
f : (completeEquipartiteGraph r t).Copy G
ht : ¬t = 0
i₁ i₂ : Fin r
h :
  ∀ (a : V),
    Membership.mem (γ := Finset V)
        (map (α := Fin t) { toFun := fun (j : Fin t) ↦ (f : (a : Fin r × Fin t) → V) (i₁, j), inj' := ⋯ } univ) a ↔
      Membership.mem (γ := Finset V)
        (map (α := Fin t) { toFun := fun (j : Fin t) ↦ (f : (a : Fin r × Fin t) → V) (i₂, j), inj' := ⋯ } univ) a
this : NeZero t
w : Fin t
heq : (i₁, w) = (i₂, 0)
⊢ i₁ = i₂
have heq₁ : i₁ = i₂ ∧ w = 0
Tactic: rw [Prod.mk.injEq] at heq
Cleared hypotheses: heq
-- 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
f : (completeEquipartiteGraph r t).Copy G
ht : ¬t = 0
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' := ⋯ } univ,
        inj' := ⋯ }
      univ)
    p
⊢ #p = t
have h₁ : ∃ (a : Fin r), map (α := Fin t) { toFun := fun (j : Fin t) ↦ (f : (a : Fin r × Fin t) → V) (a, j), inj' := sorry } univ = p
Tactic: simp_rw [mem_map, mem_univ, Embedding.coeFn_mk, true_and] at h
Cleared hypotheses: 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
p : Finset V
h :
  ∃ (a : Fin r),
    map (α := Fin t) { toFun := fun (j : Fin t) ↦ (f : (a : Fin r × Fin t) → V) (a, j), inj' := ⋯ } univ = p
⊢ #p = t
have neg : ∀ (w : Fin r)
  (h : map (α := Fin t) { toFun := fun (j : Fin t) ↦ (f : (a : Fin r × Fin t) → V) (w, j), inj' := sorry } univ = p), #p = t
Tactic: replace ⟨_, h⟩ := h
Cleared hypotheses: h
-- 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
f : (completeEquipartiteGraph r t).Copy G
ht : ¬t = 0
x : Finset V
h₁ :
  x ∈
    (↑(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) :
      Set (Finset V))
x_1 : Finset V
h₂ :
  x_1 ∈
    (↑(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) :
      Set (Finset V))
hne : x ≠ x_1
x_2 : V
h₁' : x_2 ∈ (↑x : Set V)
x_3 : V
h₂' : x_3 ∈ (↑x_1 : Set V)
⊢ G.Adj x_2 x_3
have h₃ : ∃ (y : Fin r), map (α := Fin t) { toFun := fun (j : Fin t) ↦ (f : (a : Fin r × Fin t) → V) (y, j), inj' := sorry } univ = x
Tactic: simp_rw [coe_map, Embedding.coeFn_mk, coe_univ, Set.image_univ, Set.mem_range] at h₁ h₂
Cleared hypotheses: h₁, h₂
-- 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
f : (completeEquipartiteGraph r t).Copy G
ht : ¬t = 0
x : Finset V
h₁ :
  x ∈
    (↑(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) :
      Set (Finset V))
x_1 : Finset V
h₂ :
  x_1 ∈
    (↑(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) :
      Set (Finset V))
hne : x ≠ x_1
x_2 : V
h₁' : x_2 ∈ (↑x : Set V)
x_3 : V
h₂' : x_3 ∈ (↑x_1 : Set V)
h₃ :
  ∃ (y : Fin r),
    map (α := Fin t) { toFun := fun (j : Fin t) ↦ (f : (a : Fin r × Fin t) → V) (y, j), inj' := ⋯ } univ = x
⊢ G.Adj x_2 x_3
have h₄ : ∃ (y : Fin r),
  map (α := Fin t) { toFun := fun (j : Fin t) ↦ (f : (a : Fin r × Fin t) → V) (y, j), inj' := sorry } univ = x_1
Tactic: simp_rw [coe_map, Embedding.coeFn_mk, coe_univ, Set.image_univ, Set.mem_range] at h₁ h₂
Cleared hypotheses: 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
x x_1 : Finset V
hne : x ≠ x_1
x_2 : V
h₁' : x_2 ∈ (↑x : Set V)
x_3 : V
h₂' : x_3 ∈ (↑x_1 : Set V)
h₁ :
  ∃ (y : Fin r),
    map (α := Fin t) { toFun := fun (j : Fin t) ↦ (f : (a : Fin r × Fin t) → V) (y, j), inj' := ⋯ } univ = x
h₂ :
  ∃ (y : Fin r),
    map (α := Fin t) { toFun := fun (j : Fin t) ↦ (f : (a : Fin r × Fin t) → V) (y, j), inj' := ⋯ } univ = x_1
⊢ G.Adj x_2 x_3
have neg : ∀ (w : Fin r)
  (h₁ : map (α := Fin t) { toFun := fun (j : Fin t) ↦ (f : (a : Fin r × Fin t) → V) (w, j), inj' := sorry } univ = x),
  G.Adj x_2 x_3
Tactic: replace ⟨_, h₁⟩ := h₁
Cleared hypotheses: 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
x x_1 : Finset V
hne : x ≠ x_1
x_2 : V
h₁' : x_2 ∈ (↑x : Set V)
x_3 : V
h₂' : x_3 ∈ (↑x_1 : Set V)
h₂ :
  ∃ (y : Fin r),
    map (α := Fin t) { toFun := fun (j : Fin t) ↦ (f : (a : Fin r × Fin t) → V) (y, j), inj' := ⋯ } univ = x_1
w : Fin r
h₁ : map (α := Fin t) { toFun := fun (j : Fin t) ↦ (f : (a : Fin r × Fin t) → V) (w, j), inj' := ⋯ } univ = x
⊢ G.Adj x_2 x_3
have neg : ∀ (w : Fin r)
  (h₂ : map (α := Fin t) { toFun := fun (j : Fin t) ↦ (f : (a : Fin r × Fin t) → V) (w, j), inj' := sorry } univ = x_1),
  G.Adj x_2 x_3
Tactic: replace ⟨_, h₂⟩ := h₂
Cleared hypotheses: 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
x x_1 : Finset V
hne : x ≠ x_1
x_2 : V
h₁' : x_2 ∈ (↑x : Set V)
x_3 : V
h₂' : x_3 ∈ (↑x_1 : Set 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
⊢ G.Adj x_2 x_3
have neg : ∀
  (h₁' :
    x_2 ∈
      (↑(map (α := Fin t) { toFun := fun (j : Fin t) ↦ (f : (a : Fin r × Fin t) → V) (w, j), inj' := sorry : 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' := sorry } univ = x)
  (w : Fin r)
  (h₂ : map (α := Fin t) { toFun := fun (j : Fin t) ↦ (f : (a : Fin r × Fin t) → V) (w, j), inj' := sorry } univ = x_1),
  G.Adj x_2 x_3
Tactic: rw [← h₁] at h₁'
Cleared hypotheses: h₁', h₁, w_1, h₂
-- 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
f : (completeEquipartiteGraph r t).Copy G
ht : ¬t = 0
x x_1 : Finset V
hne : x ≠ x_1
x_2 x_3 : V
h₂' : x_3 ∈ (↑x_1 : Set 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₂ : map (α := Fin t) { toFun := fun (j : Fin t) ↦ (f : (a : Fin r × Fin t) → V) (w_1, j), inj' := ⋯ } univ = x_1
⊢ G.Adj x_2 x_3
have h₂'₁ : x_3 ∈
  (↑(map (α := Fin t) { toFun := fun (j : Fin t) ↦ (f : (a : Fin r × Fin t) → V) (w_1, j), inj' := sorry : Fin t ↪ V }
        univ) :
    Set V)
Tactic: rw [← h₂] at h₂'
Cleared hypotheses: h₂', h₂
-- 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
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
⊢ G.Adj x_2 x_3
have h₁'₁ : ∃ (y : Fin t), (f : (a : Fin r × Fin t) → V) (w, y) = x_2
Tactic: simp_rw [coe_map, Embedding.coeFn_mk, coe_univ, Set.image_univ, Set.mem_range] at h₁' h₂'
Cleared hypotheses: h₁', h₂'
-- 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
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
⊢ G.Adj x_2 x_3
have h₂'₁ : ∃ (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₂'
Cleared hypotheses: 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
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
⊢ G.Adj x_2 x_3
have neg : ∀ (w_2 : Fin t) (h₁' : (f : (a : Fin r × Fin t) → V) (w, w_2) = x_2), G.Adj x_2 x_3
Tactic: replace ⟨_, h₁'⟩ := h₁'
Cleared hypotheses: 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
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
⊢ G.Adj x_2 x_3
have neg : ∀ (w : Fin t) (h₂' : (f : (a : Fin r × Fin t) → V) (w_1, w) = x_3), G.Adj x_2 x_3
Tactic: replace ⟨_, h₂'⟩ := h₂'
Cleared hypotheses: 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
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
⊢ G.Adj x_2 x_3
have neg : G.Adj ((f : (a : Fin r × Fin t) → V) (w, w_2)) ((f : (a : Fin r × Fin t) → V) (w_1, w_3))
Tactic: rw [← 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
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
⊢ G.Adj ((f : (a : Fin r × Fin t) → V) (w, w_2)) ((f : (a : Fin r × Fin t) → V) (w_1, w_3))
have neg : (completeEquipartiteGraph r t).Adj (w, w_2) (w_1, w_3)
Tactic: apply f.toHom.map_adj
-- 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
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
⊢ (completeEquipartiteGraph r t).Adj (w, w_2) (w_1, w_3)
have neg : w ≠ w_1
Tactic: simp_rw [completeEquipartiteGraph_adj]
-- 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
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
⊢ w ≠ w_1
have neg : ∀ (heq : w = w_1), x = x_1
Tactic: contrapose hne with heq
Cleared hypotheses: 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
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
⊢ x = x_1
have neg : map (α := Fin t) { toFun := fun (j : Fin t) ↦ (f : (a : Fin r × Fin t) → V) (w, j), inj' := sorry } univ = x_1
Tactic: simp_rw [← h₁, ← h₂, 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
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
⊢ x = x_1
have 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' := sorry } univ)
  (map (α := Fin t) { toFun := fun (j : Fin t) ↦ (f : (a : Fin r × Fin t) → V) (w_1, j), inj' := sorry } univ)
Tactic: simp_rw [← h₁, ← h₂, heq]