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
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
⊢ 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:
Subtype.ext_iff.ne.mp <| fᵣ.injective.ne hne

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

Premises used: Function.Injective.ne, Subtype.ext_iff, Iff.ne, Iff.mp, Function.Embedding.injective
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G_1 : SimpleGraph α
s : Set α
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
f : (completeEquipartiteGraph r t).Copy G
pos : (ht : t = 0) → G.CompleteEquipartiteSubgraph r t
neg : (ht : ¬t = 0) → G.CompleteEquipartiteSubgraph r t
⊢ G.CompleteEquipartiteSubgraph r t

Tactic:
by_cases ht : t = 0
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G_1 : SimpleGraph α
s : Set α
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
f : (completeEquipartiteGraph r t).Copy G
ht : t = 0
⊢ ∀ {p : Finset V}, Membership.mem (γ := Finset (Finset V)) ∅ p → #p = t

Tactic:
simp
-- 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
⊢ (↑∅ : Set (Finset V)).Pairwise fun (x1 x2 : Finset V) ↦ G.IsCompleteBetween (↑x1 : Set V) (↑x2 : Set V)

Tactic:
simp
-- 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
⊢ G.CompleteEquipartiteSubgraph r t

Tactic:
exact ⟨∅, .inr ht, by simp, by simp⟩
-- 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
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
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' := ⋯ : 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 : V) (h₂' : x ∈ (↑x_1 : Set V)), G.Adj x_2 x
⊢ G.CompleteEquipartiteSubgraph r 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₂' ↦ ?_⟩
-- 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
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:
simpa using f.injective h

Premises used: SimpleGraph.Copy.injective
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G_1 : SimpleGraph α
s : Set α
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
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₂)
⊢ ∀ (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

Tactic:
simp_rw [Finset.ext_iff] at h

Premises used: Finset.ext_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G_1 : SimpleGraph α
s : Set α
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
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
⊢ NeZero t

Tactic:
have : NeZero t := ⟨ht⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G_1 : SimpleGraph α
s : Set α
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
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
⊢ ∃ (j : Fin t), Eq (α := V) ((f : (a : Fin r × Fin t) → V) (i₁, j) : V) ((f : (a : Fin r × Fin t) → V) (i₂, 0) : V)

Tactic:
simpa using h <| f (i₂, 0)

Premises used: Prod.mk, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G_1 : SimpleGraph α
s : Set α
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
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
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₂
⊢ i₁ = i₂

Tactic:
obtain ⟨_, heq⟩ : ∃ j, f (i₁, j) = f (i₂, 0) := by simpa using h <| f (i₂, 0)

Premises used: Prod.mk, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G_1 : SimpleGraph α
s : Set α
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
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₁, w) = (i₂, 0)

Tactic:
apply f.injective at heq

Premises used: SimpleGraph.Copy.injective
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G_1 : SimpleGraph α
s : Set α
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
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₂ ∧ w = 0

Tactic:
rw [Prod.mk.injEq] at heq

Premises used: Prod.mk.injEq
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G_1 : SimpleGraph α
s : Set α
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
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₁ = i₂ ∧ w = 0
⊢ i₁ = i₂

Tactic:
heq.left

Premises used: And.left
-- 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
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₁ = i₂ ∧ w = 0
⊢ i₁ = i₂

Tactic:
exact heq.left

Premises used: And.left
-- 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
⊢ 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

Tactic:
simp
-- 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
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
⊢ ∃ (a : Fin r),
    map (α := Fin t) { toFun := fun (j : Fin t) ↦ (f : (a : Fin r × Fin t) → V) (a, j), inj' := ⋯ } univ = p

Tactic:
simp_rw [mem_map, mem_univ, Embedding.coeFn_mk, true_and] at h

Premises used: Finset.mem_univ, Function.Embedding.coeFn_mk, Finset.mem_map, true_and
-- 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
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
neg :
  ∀ (w : Fin r)
    (h : map (α := Fin t) { toFun := fun (j : Fin t) ↦ (f : (a : Fin r × Fin t) → V) (w, j), inj' := ⋯ } univ = p),
    #p = t
⊢ #p = t

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
p : Finset V
w : Fin r
h : map (α := Fin t) { toFun := fun (j : Fin t) ↦ (f : (a : Fin r × Fin t) → V) (w, j), inj' := ⋯ } univ = p
⊢ #p = t

Tactic:
simp [← 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 : 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)
⊢ ∃ (y : Fin r),
    map (α := Fin t) { toFun := fun (j : Fin t) ↦ (f : (a : Fin r × Fin t) → V) (y, j), inj' := ⋯ } univ = x

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 : 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
⊢ ∃ (y : Fin r),
    map (α := Fin t) { toFun := fun (j : Fin t) ↦ (f : (a : Fin r × Fin t) → V) (y, j), inj' := ⋯ } univ = x_1

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 : 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
neg :
  ∀ (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
⊢ 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 : 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
neg :
  ∀ (w : Fin r)
    (h₂ : map (α := Fin t) { toFun := fun (j : Fin t) ↦ (f : (a : Fin r × Fin t) → V) (w, j), inj' := ⋯ } univ = x_1),
    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 : 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
neg :
  ∀
    (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 : Fin r)
    (h₂ : map (α := Fin t) { toFun := fun (j : Fin t) ↦ (f : (a : Fin r × Fin t) → V) (w, j), inj' := ⋯ } univ = x_1),
    G.Adj x_2 x_3
⊢ G.Adj x_2 x_3

Tactic:
rw [← h₁] at 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
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
⊢ 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)

Tactic:
rw [← h₂] at 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
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
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)
⊢ map (α := Fin t) { toFun := fun (j : Fin t) ↦ (f : (a : Fin r × Fin t) → V) (w_1, j), inj' := ⋯ } univ = x_1

Tactic:
rw [← h₂] at 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₁' :
  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
⊢ ∃ (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₂'

Premises used: Set.image_univ, Set.mem_range, Finset.coe_univ, Function.Embedding.coeFn_mk, Finset.coe_map