awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
Goal:
V : Type u_1
G : SimpleGraph V
s t : Finset V
inst : Fintype V
inst_1 : DecidableRel G.Adj
h : G.IsBipartiteWith (↑s : Set V) (↑t : Set V)
rw : HMul.hMul (α := ℕ) 2 (∑ v ∈ s, G.degree v) = 2 * #G.edgeFinset
rw₁ : HMul.hMul (α := ℕ) 2 (∑ v ∈ s, G.degree v) = ∑ v ∈ s ∪ t, G.degree v
rw₂ : HMul.hMul (α := ℕ) 2 (∑ v ∈ s, G.degree v) = HAdd.hAdd (α := ℕ) (∑ x ∈ s, G.degree x) (∑ x ∈ t, G.degree x)
rw₃ :
  HAdd.hAdd (α := ℕ) (∑ v ∈ s, G.degree v) (∑ v ∈ s, G.degree v) =
    HAdd.hAdd (α := ℕ) (∑ x ∈ s, G.degree x) (∑ x ∈ t, G.degree x)
⊢ ∑ v ∈ s, G.degree v = #G.edgeFinset
have rw₄ : Eq (α := ℕ) (∑ v ∈ s, G.degree v) (∑ x ∈ t, G.degree x)
Tactic: classical
  rw [← Nat.mul_left_cancel_iff zero_lt_two, ← isBipartiteWith_sum_degrees_eq_twice_card_edges h,
    sum_union (disjoint_coe.mp h.disjoint), two_mul, add_right_inj]
  exact isBipartiteWith_sum_degrees_eq h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
Goal:
V : Type u_1
G : SimpleGraph V
h : G.IsBipartite
⊢ ∃ (s : Set V) (t : Set V), G.IsBipartiteWith s t
have obtain : ∀ (c : V → Fin 2) (hc : ∀ {a b : V}, G.Adj a b → Adj (completeGraph (Fin 2)) (c a) (c b)),
  ∃ (s : Set V) (t : Set V), G.IsBipartiteWith s t
Tactic: obtain ⟨c, hc⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
Goal:
V : Type u_1
G : SimpleGraph V
c : V → Fin 2
hc : ∀ {a b : V}, G.Adj a b → Adj (completeGraph (Fin 2)) (c a) (c b)
⊢ ∃ (s : Set V) (t : Set V), G.IsBipartiteWith s t
have refine : ∀ ⦃v w : V⦄,
  G.Adj v w →
    Membership.mem (γ := Set V) {v : V | c v = 0} v ∧ Membership.mem (γ := Set V) {v : V | c v = 1} w ∨
      Membership.mem (γ := Set V) {v : V | c v = 1} v ∧ Membership.mem (γ := Set V) {v : V | c v = 0} w
Tactic: refine ⟨{v | c v = 0}, {v | c v = 1}, by aesop (add simp [Set.disjoint_left]), ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
c : V → Fin 2
hc : ∀ {a b : V}, G.Adj a b → Adj (completeGraph (Fin 2)) (c a) (c b)
v w : V
hvw : G.Adj v w
⊢ Membership.mem (γ := Set V) {v : V | c v = 0} v ∧ Membership.mem (γ := Set V) {v : V | c v = 1} w ∨
    Membership.mem (γ := Set V) {v : V | c v = 1} v ∧ Membership.mem (γ := Set V) {v : V | c v = 0} w
have hvw₁ : Adj (completeGraph (Fin 2)) (c v) (c w)
Tactic: apply hc at hvw
Cleared hypotheses: hvw
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
c : V → Fin 2
hc : ∀ {a b : V}, G.Adj a b → Adj (completeGraph (Fin 2)) (c a) (c b)
v w : V
hvw : Adj (completeGraph (Fin 2)) (c v) (c w)
⊢ Membership.mem (γ := Set V) {v : V | c v = 0} v ∧ Membership.mem (γ := Set V) {v : V | c v = 1} w ∨
    Membership.mem (γ := Set V) {v : V | c v = 1} v ∧ Membership.mem (γ := Set V) {v : V | c v = 0} w
have hvw₁ : ¬c v = c w
Tactic: simp [Set.mem_setOf_eq] at hvw ⊢
Cleared hypotheses: hvw
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
Goal:
V : Type u_1
G : SimpleGraph V
s t : Set V
h : G.IsBipartiteWith s t
⊢ G.IsBipartite
have refine : ∀ {v w : V} (hw : G.Adj v w), Adj (V := Fin 2) (completeGraph (Fin 2)) (s.indicator 1 v) (s.indicator 1 w)
Tactic: refine ⟨s.indicator 1, fun {v w} hw ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
Goal:
V : Type u_1
G : SimpleGraph V
s t : Set V
h : G.IsBipartiteWith s t
v w : V
hw : G.Adj v w
⊢ Adj (V := Fin 2) (completeGraph (Fin 2)) (s.indicator 1 v) (s.indicator 1 w)
have inl : ∀ (hs : v ∈ s) (ht : w ∈ t), Adj (V := Fin 2) (completeGraph (Fin 2)) (s.indicator 1 v) (s.indicator 1 w)
Tactic: obtain (⟨hs, ht⟩ | ⟨ht, hs⟩) := h.2 hw
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
Goal:
V : Type u_1
G : SimpleGraph V
s t : Set V
h : G.IsBipartiteWith s t
v w : V
hw : G.Adj v w
inl : ∀ (hs : v ∈ s) (ht : w ∈ t), Adj (V := Fin 2) (completeGraph (Fin 2)) (s.indicator 1 v) (s.indicator 1 w)
⊢ Adj (V := Fin 2) (completeGraph (Fin 2)) (s.indicator 1 v) (s.indicator 1 w)
have inr : ∀ (ht : v ∈ t) (hs : w ∈ s), Adj (V := Fin 2) (completeGraph (Fin 2)) (s.indicator 1 v) (s.indicator 1 w)
Tactic: obtain (⟨hs, ht⟩ | ⟨ht, hs⟩) := h.2 hw
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
s t : Set V
h : G.IsBipartiteWith s t
v w : V
hw : G.Adj v w
hs : v ∈ s
ht : w ∈ t
⊢ Adj (V := Fin 2) (completeGraph (Fin 2)) (s.indicator 1 v) (s.indicator 1 w)
have ht₁ : w ∉ s
Tactic: replace ht : _ ∉ s := h.1.subset_compl_left ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
Goal:
V : Type u_1
G : SimpleGraph V
s t : Set V
h : G.IsBipartiteWith s t
v w : V
hw : G.Adj v w
hs : v ∈ s
ht : w ∈ t
⊢ Adj (V := Fin 2) (completeGraph (Fin 2)) (s.indicator 1 v) (s.indicator 1 w)
have inl : ∀ (ht : w ∉ s), Adj (V := Fin 2) (completeGraph (Fin 2)) (s.indicator 1 v) (s.indicator 1 w)
Tactic: { replace ht : _ ∉ s := h.1.subset_compl_left ht; simp [hs, ht] }
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
s t : Set V
h : G.IsBipartiteWith s t
v w : V
hw : G.Adj v w
ht : v ∈ t
hs : w ∈ s
⊢ Adj (V := Fin 2) (completeGraph (Fin 2)) (s.indicator 1 v) (s.indicator 1 w)
have ht₁ : v ∉ s
Tactic: replace ht : _ ∉ s := h.1.subset_compl_left ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
Goal:
V : Type u_1
G : SimpleGraph V
s t : Set V
h : G.IsBipartiteWith s t
v w : V
hw : G.Adj v w
ht : v ∈ t
hs : w ∈ s
⊢ Adj (V := Fin 2) (completeGraph (Fin 2)) (s.indicator 1 v) (s.indicator 1 w)
have inr : ∀ (ht : v ∉ s), Adj (V := Fin 2) (completeGraph (Fin 2)) (s.indicator 1 v) (s.indicator 1 w)
Tactic: { replace ht : _ ∉ s := h.1.subset_compl_left ht; simp [hs, ht] }
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (hypothesis)
Goal:
V : Type u_1
v w : V
G : SimpleGraph V
s t : Set V
α : Type u_2
β : Type u_3
inst : Fintype α
inst_1 : Fintype β
left right : Finset V
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.IsCompleteBetween (↑left : Set V) (↑right : Set V)
⊢ Nonempty (Function.Embedding.{u_2 + 1, u_1 + 1} α ↥left)
have card_left₁ : Fintype.card.{u_1} ↥left = Fintype.card α
Tactic: rw [← card_coe] at card_left
Cleared hypotheses: card_left, card_right, h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (hypothesis)
Goal:
V : Type u_1
v w : V
G : SimpleGraph V
s t : Set V
α : Type u_2
β : Type u_3
inst : Fintype α
inst_1 : Fintype β
left right : Finset V
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.IsCompleteBetween (↑left : Set V) (↑right : Set V)
⊢ (_root_.completeBipartiteGraph α β).Copy G
have this : Nonempty (Function.Embedding.{u_2 + 1, u_1 + 1} α ↥left)
Tactic: have : Nonempty (α ↪ left) := by
    rw [← card_coe] at card_left
    exact Function.Embedding.nonempty_of_card_le card_left.symm.le
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (hypothesis)
Goal:
V : Type u_1
v w : V
G : SimpleGraph V
s t : Set V
α : Type u_2
β : Type u_3
inst : Fintype α
inst_1 : Fintype β
left right : Finset V
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.IsCompleteBetween (↑left : Set V) (↑right : Set V)
this : Nonempty (Function.Embedding.{u_2 + 1, u_1 + 1} α ↥left)
fα : Function.Embedding.{u_2 + 1, u_1 + 1} α ↥left :=
  Classical.arbitrary (Function.Embedding.{u_2 + 1, u_1 + 1} α ↥left)
⊢ Nonempty (Function.Embedding.{u_3 + 1, u_1 + 1} β ↥right)
have card_right₁ : Fintype.card.{u_1} ↥right = Fintype.card β
Tactic: rw [← card_coe] at card_right
Cleared hypotheses: card_right, h, this, fα
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (hypothesis)
Goal:
V : Type u_1
v w : V
G : SimpleGraph V
s t : Set V
α : Type u_2
β : Type u_3
inst : Fintype α
inst_1 : Fintype β
left right : Finset V
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.IsCompleteBetween (↑left : Set V) (↑right : Set V)
this : Nonempty (Function.Embedding.{u_2 + 1, u_1 + 1} α ↥left)
fα : Function.Embedding.{u_2 + 1, u_1 + 1} α ↥left :=
  Classical.arbitrary (Function.Embedding.{u_2 + 1, u_1 + 1} α ↥left)
⊢ (_root_.completeBipartiteGraph α β).Copy G
have this₁ : Nonempty (Function.Embedding.{u_3 + 1, u_1 + 1} β ↥right)
Tactic: have : Nonempty (β ↪ right) := by
    rw [← card_coe] at card_right
    exact Function.Embedding.nonempty_of_card_le card_right.symm.le
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
Goal:
V : Type u_1
v w : V
G : SimpleGraph V
s t : Set V
α : Type u_2
β : Type u_3
inst : Fintype α
inst_1 : Fintype β
left right : Finset V
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.IsCompleteBetween (↑left : Set V) (↑right : Set V)
this_1 : Nonempty (Function.Embedding.{u_2 + 1, u_1 + 1} α ↥left)
fα : Function.Embedding.{u_2 + 1, u_1 + 1} α ↥left :=
  Classical.arbitrary (Function.Embedding.{u_2 + 1, u_1 + 1} α ↥left)
this : Nonempty (Function.Embedding.{u_3 + 1, u_1 + 1} β ↥right)
fβ : Function.Embedding.{u_3 + 1, u_1 + 1} β ↥right :=
  Classical.arbitrary (Function.Embedding.{u_3 + 1, u_1 + 1} β ↥right)
⊢ α ⊕ β ↪ V
have refine : ∀ (s₁ s₂ : α ⊕ β),
  Eq.{u_1 + 1} (α := V)
      (Sum.elim (Function.comp (β := ↥left) (Subtype.val (p := fun (x : V) ↦ x ∈ left)) (⇑fα : (a : α) → ↥left))
        (Function.comp (β := ↥right) (Subtype.val (p := fun (x : V) ↦ x ∈ right)) (⇑fβ : (a : β) → ↥right)) s₁)
      (Sum.elim (Function.comp (β := ↥left) (Subtype.val (p := fun (x : V) ↦ x ∈ left)) (⇑fα : (a : α) → ↥left))
        (Function.comp (β := ↥right) (Subtype.val (p := fun (x : V) ↦ x ∈ right)) (⇑fβ : (a : β) → ↥right)) s₂) →
    s₁ = s₂
Tactic: refine ⟨Sum.elim (Subtype.val ∘ fα) (Subtype.val ∘ fβ), fun s₁ s₂ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
Goal:
V : Type u_1
v w : V
G : SimpleGraph V
s t : Set V
α : Type u_2
β : Type u_3
inst : Fintype α
inst_1 : Fintype β
left right : Finset V
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.IsCompleteBetween (↑left : Set V) (↑right : Set V)
this_1 : Nonempty (Function.Embedding.{u_2 + 1, u_1 + 1} α ↥left)
fα : Function.Embedding.{u_2 + 1, u_1 + 1} α ↥left :=
  Classical.arbitrary (Function.Embedding.{u_2 + 1, u_1 + 1} α ↥left)
this : Nonempty (Function.Embedding.{u_3 + 1, u_1 + 1} β ↥right)
fβ : Function.Embedding.{u_3 + 1, u_1 + 1} β ↥right :=
  Classical.arbitrary (Function.Embedding.{u_3 + 1, u_1 + 1} β ↥right)
f : α ⊕ β ↪ V :=
  {
    toFun :=
      Sum.elim (Function.comp (β := ↥left) (Subtype.val (p := fun (x : V) ↦ x ∈ left)) (⇑fα : (a : α) → ↥left))
        (Function.comp (β := ↥right) (Subtype.val (p := fun (x : V) ↦ x ∈ right)) (⇑fβ : (a : β) → ↥right)),
    inj' := ⋯ }
⊢ (_root_.completeBipartiteGraph α β).Copy G
have refine : ∀ {s₁ s₂ : α ⊕ β} (hadj : (_root_.completeBipartiteGraph α β).Adj s₁ s₂), G.Adj (f.toFun s₁) (f.toFun s₂)
Tactic: refine ⟨⟨f.toFun, fun {s₁ s₂} hadj ↦ ?_⟩, f.injective⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
Goal:
V : Type u_1
v w : V
G : SimpleGraph V
s t : Set V
α : Type u_2
β : Type u_3
inst : Fintype α
inst_1 : Fintype β
left right : Finset V
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.IsCompleteBetween (↑left : Set V) (↑right : Set V)
this_1 : Nonempty (Function.Embedding.{u_2 + 1, u_1 + 1} α ↥left)
fα : Function.Embedding.{u_2 + 1, u_1 + 1} α ↥left :=
  Classical.arbitrary (Function.Embedding.{u_2 + 1, u_1 + 1} α ↥left)
this : Nonempty (Function.Embedding.{u_3 + 1, u_1 + 1} β ↥right)
fβ : Function.Embedding.{u_3 + 1, u_1 + 1} β ↥right :=
  Classical.arbitrary (Function.Embedding.{u_3 + 1, u_1 + 1} β ↥right)
f : α ⊕ β ↪ V :=
  {
    toFun :=
      Sum.elim (Function.comp (β := ↥left) (Subtype.val (p := fun (x : V) ↦ x ∈ left)) (⇑fα : (a : α) → ↥left))
        (Function.comp (β := ↥right) (Subtype.val (p := fun (x : V) ↦ x ∈ right)) (⇑fβ : (a : β) → ↥right)),
    inj' := ⋯ }
s₁ s₂ : α ⊕ β
hadj : (_root_.completeBipartiteGraph α β).Adj s₁ s₂
⊢ G.Adj (f.toFun s₁) (f.toFun s₂)
have inl : ∀ (hs₁ : s₁.isLeft = true) (hs₂ : s₂.isRight = true), G.Adj (f.toFun s₁) (f.toFun s₂)
Tactic: rcases hadj with ⟨hs₁, hs₂⟩ | ⟨hs₁, hs₂⟩
Cleared hypotheses: hadj
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
Goal:
V : Type u_1
v w : V
G : SimpleGraph V
s t : Set V
α : Type u_2
β : Type u_3
inst : Fintype α
inst_1 : Fintype β
left right : Finset V
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.IsCompleteBetween (↑left : Set V) (↑right : Set V)
this_1 : Nonempty (Function.Embedding.{u_2 + 1, u_1 + 1} α ↥left)
fα : Function.Embedding.{u_2 + 1, u_1 + 1} α ↥left :=
  Classical.arbitrary (Function.Embedding.{u_2 + 1, u_1 + 1} α ↥left)
this : Nonempty (Function.Embedding.{u_3 + 1, u_1 + 1} β ↥right)
fβ : Function.Embedding.{u_3 + 1, u_1 + 1} β ↥right :=
  Classical.arbitrary (Function.Embedding.{u_3 + 1, u_1 + 1} β ↥right)
f : α ⊕ β ↪ V :=
  {
    toFun :=
      Sum.elim (Function.comp (β := ↥left) (Subtype.val (p := fun (x : V) ↦ x ∈ left)) (⇑fα : (a : α) → ↥left))
        (Function.comp (β := ↥right) (Subtype.val (p := fun (x : V) ↦ x ∈ right)) (⇑fβ : (a : β) → ↥right)),
    inj' := ⋯ }
s₁ s₂ : α ⊕ β
hadj : (_root_.completeBipartiteGraph α β).Adj s₁ s₂
inl : ∀ (hs₁ : s₁.isLeft = true) (hs₂ : s₂.isRight = true), G.Adj (f.toFun s₁) (f.toFun s₂)
⊢ G.Adj (f.toFun s₁) (f.toFun s₂)
have inr : ∀ (hs₁ : s₁.isRight = true) (hs₂ : s₂.isLeft = true), G.Adj (f.toFun s₁) (f.toFun s₂)
Tactic: rcases hadj with ⟨hs₁, hs₂⟩ | ⟨hs₁, hs₂⟩
Cleared hypotheses: hadj
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
Goal:
V : Type u_1
v w : V
G : SimpleGraph V
s t : Set V
α : Type u_2
β : Type u_3
inst : Fintype α
inst_1 : Fintype β
left right : Finset V
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.IsCompleteBetween (↑left : Set V) (↑right : Set V)
this_1 : Nonempty (Function.Embedding.{u_2 + 1, u_1 + 1} α ↥left)
fα : Function.Embedding.{u_2 + 1, u_1 + 1} α ↥left :=
  Classical.arbitrary (Function.Embedding.{u_2 + 1, u_1 + 1} α ↥left)
this : Nonempty (Function.Embedding.{u_3 + 1, u_1 + 1} β ↥right)
fβ : Function.Embedding.{u_3 + 1, u_1 + 1} β ↥right :=
  Classical.arbitrary (Function.Embedding.{u_3 + 1, u_1 + 1} β ↥right)
f : α ⊕ β ↪ V :=
  {
    toFun :=
      Sum.elim (Function.comp (β := ↥left) (Subtype.val (p := fun (x : V) ↦ x ∈ left)) (⇑fα : (a : α) → ↥left))
        (Function.comp (β := ↥right) (Subtype.val (p := fun (x : V) ↦ x ∈ right)) (⇑fβ : (a : β) → ↥right)),
    inj' := ⋯ }
s₁ s₂ : α ⊕ β
hs₁ : s₁.isLeft = true
hs₂ : s₂.isRight = true
⊢ G.Adj (f.toFun s₁) (f.toFun s₂)
have inl : G.Adj
  (Sum.elim (Function.comp (β := ↥left) (Subtype.val (p := fun (x : V) ↦ x ∈ left)) (⇑fα : (a : α) → ↥left))
    (Function.comp (β := ↥right) (Subtype.val (p := fun (x : V) ↦ x ∈ right)) (⇑fβ : (a : β) → ↥right)) s₁)
  (Sum.elim (Function.comp (β := ↥left) (Subtype.val (p := fun (x : V) ↦ x ∈ left)) (⇑fα : (a : α) → ↥left))
    (Function.comp (β := ↥right) (Subtype.val (p := fun (x : V) ↦ x ∈ right)) (⇑fβ : (a : β) → ↥right)) s₂)
Tactic: dsimp [f]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
Goal:
V : Type u_1
v w : V
G : SimpleGraph V
s t : Set V
α : Type u_2
β : Type u_3
inst : Fintype α
inst_1 : Fintype β
left right : Finset V
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.IsCompleteBetween (↑left : Set V) (↑right : Set V)
this_1 : Nonempty (Function.Embedding.{u_2 + 1, u_1 + 1} α ↥left)
fα : Function.Embedding.{u_2 + 1, u_1 + 1} α ↥left :=
  Classical.arbitrary (Function.Embedding.{u_2 + 1, u_1 + 1} α ↥left)
this : Nonempty (Function.Embedding.{u_3 + 1, u_1 + 1} β ↥right)
fβ : Function.Embedding.{u_3 + 1, u_1 + 1} β ↥right :=
  Classical.arbitrary (Function.Embedding.{u_3 + 1, u_1 + 1} β ↥right)
f : α ⊕ β ↪ V :=
  {
    toFun :=
      Sum.elim (Function.comp (β := ↥left) (Subtype.val (p := fun (x : V) ↦ x ∈ left)) (⇑fα : (a : α) → ↥left))
        (Function.comp (β := ↥right) (Subtype.val (p := fun (x : V) ↦ x ∈ right)) (⇑fβ : (a : β) → ↥right)),
    inj' := ⋯ }
s₁ s₂ : α ⊕ β
hs₁ : s₁.isRight = true
hs₂ : s₂.isLeft = true
⊢ G.Adj (f.toFun s₁) (f.toFun s₂)
have inr : G.Adj
  (Sum.elim (Function.comp (β := ↥left) (Subtype.val (p := fun (x : V) ↦ x ∈ left)) (⇑fα : (a : α) → ↥left))
    (Function.comp (β := ↥right) (Subtype.val (p := fun (x : V) ↦ x ∈ right)) (⇑fβ : (a : β) → ↥right)) s₁)
  (Sum.elim (Function.comp (β := ↥left) (Subtype.val (p := fun (x : V) ↦ x ∈ left)) (⇑fα : (a : α) → ↥left))
    (Function.comp (β := ↥right) (Subtype.val (p := fun (x : V) ↦ x ∈ right)) (⇑fβ : (a : β) → ↥right)) s₂)
Tactic: dsimp [f]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
Goal:
V : Type u_1
v w : V
G : SimpleGraph V
s t : Set V
α : Type u_2
β : Type u_3
inst : Fintype α
inst_1 : Fintype β
left right : Finset V
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.IsCompleteBetween (↑left : Set V) (↑right : Set V)
this_1 : Nonempty (Function.Embedding.{u_2 + 1, u_1 + 1} α ↥left)
fα : Function.Embedding.{u_2 + 1, u_1 + 1} α ↥left :=
  Classical.arbitrary (Function.Embedding.{u_2 + 1, u_1 + 1} α ↥left)
this : Nonempty (Function.Embedding.{u_3 + 1, u_1 + 1} β ↥right)
fβ : Function.Embedding.{u_3 + 1, u_1 + 1} β ↥right :=
  Classical.arbitrary (Function.Embedding.{u_3 + 1, u_1 + 1} β ↥right)
f : α ⊕ β ↪ V :=
  {
    toFun :=
      Sum.elim (Function.comp (β := ↥left) (Subtype.val (p := fun (x : V) ↦ x ∈ left)) (⇑fα : (a : α) → ↥left))
        (Function.comp (β := ↥right) (Subtype.val (p := fun (x : V) ↦ x ∈ right)) (⇑fβ : (a : β) → ↥right)),
    inj' := ⋯ }
s₁ s₂ : α ⊕ β
hs₁ : s₁.isLeft = true
hs₂ : s₂.isRight = true
⊢ G.Adj
    (Sum.elim (Function.comp (β := ↥left) (Subtype.val (p := fun (x : V) ↦ x ∈ left)) (⇑fα : (a : α) → ↥left))
      (Function.comp (β := ↥right) (Subtype.val (p := fun (x : V) ↦ x ∈ right)) (⇑fβ : (a : β) → ↥right)) s₁)
    (Sum.elim (Function.comp (β := ↥left) (Subtype.val (p := fun (x : V) ↦ x ∈ left)) (⇑fα : (a : α) → ↥left))
      (Function.comp (β := ↥right) (Subtype.val (p := fun (x : V) ↦ x ∈ right)) (⇑fβ : (a : β) → ↥right)) s₂)
have inl : G.Adj (Function.comp (β := ↥left) (Subtype.val (p := fun (x : V) ↦ x ∈ left)) (⇑fα : (a : α) → ↥left) (s₁.getLeft hs₁))
  (Function.comp (β := ↥right) (Subtype.val (p := fun (x : V) ↦ x ∈ right)) (⇑fβ : (a : β) → ↥right) (s₂.getRight hs₂))
Tactic: rw [← Sum.inl_getLeft s₁ hs₁, ← Sum.inr_getRight s₂ hs₂,
      Sum.elim_inl, Sum.elim_inr]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
Goal:
V : Type u_1
v w : V
G : SimpleGraph V
s t : Set V
α : Type u_2
β : Type u_3
inst : Fintype α
inst_1 : Fintype β
left right : Finset V
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.IsCompleteBetween (↑left : Set V) (↑right : Set V)
this_1 : Nonempty (Function.Embedding.{u_2 + 1, u_1 + 1} α ↥left)
fα : Function.Embedding.{u_2 + 1, u_1 + 1} α ↥left :=
  Classical.arbitrary (Function.Embedding.{u_2 + 1, u_1 + 1} α ↥left)
this : Nonempty (Function.Embedding.{u_3 + 1, u_1 + 1} β ↥right)
fβ : Function.Embedding.{u_3 + 1, u_1 + 1} β ↥right :=
  Classical.arbitrary (Function.Embedding.{u_3 + 1, u_1 + 1} β ↥right)
f : α ⊕ β ↪ V :=
  {
    toFun :=
      Sum.elim (Function.comp (β := ↥left) (Subtype.val (p := fun (x : V) ↦ x ∈ left)) (⇑fα : (a : α) → ↥left))
        (Function.comp (β := ↥right) (Subtype.val (p := fun (x : V) ↦ x ∈ right)) (⇑fβ : (a : β) → ↥right)),
    inj' := ⋯ }
s₁ s₂ : α ⊕ β
hs₁ : s₁.isRight = true
hs₂ : s₂.isLeft = true
⊢ G.Adj
    (Sum.elim (Function.comp (β := ↥left) (Subtype.val (p := fun (x : V) ↦ x ∈ left)) (⇑fα : (a : α) → ↥left))
      (Function.comp (β := ↥right) (Subtype.val (p := fun (x : V) ↦ x ∈ right)) (⇑fβ : (a : β) → ↥right)) s₁)
    (Sum.elim (Function.comp (β := ↥left) (Subtype.val (p := fun (x : V) ↦ x ∈ left)) (⇑fα : (a : α) → ↥left))
      (Function.comp (β := ↥right) (Subtype.val (p := fun (x : V) ↦ x ∈ right)) (⇑fβ : (a : β) → ↥right)) s₂)
have inr : G.Adj (Function.comp (β := ↥left) (Subtype.val (p := fun (x : V) ↦ x ∈ left)) (⇑fα : (a : α) → ↥left) (s₂.getLeft hs₂))
  (Function.comp (β := ↥right) (Subtype.val (p := fun (x : V) ↦ x ∈ right)) (⇑fβ : (a : β) → ↥right) (s₁.getRight hs₁))
Tactic: rw [← Sum.inr_getRight s₁ hs₁, ← Sum.inl_getLeft s₂ hs₂,
      Sum.elim_inl, Sum.elim_inr, adj_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
Goal:
V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst : Fintype α
inst_1 : Fintype β
⊢ completeBipartiteGraph α β ⊑ G →
    ∃ (left : Finset V) (right : Finset V),
      #left = Fintype.card α ∧ #right = Fintype.card β ∧ G.IsCompleteBetween (↑left : Set V) (↑right : Set V)
have refine : completeBipartiteGraph α β ⊑ G →
  ∀ (f : (completeBipartiteGraph α β).Copy G) (x : V)
    (hl :
      x ∈
        (↑(map { toFun := Function.comp (β := α ⊕ β) (⇑f : (a : α ⊕ β) → V) Sum.inl, inj' := sorry : α ↪ V } univ) : Set V))
    (x_1 : V)
    (hr :
      x_1 ∈
        (↑(map { toFun := Function.comp (β := α ⊕ β) (⇑f : (a : α ⊕ β) → V) Sum.inr, inj' := sorry : β ↪ V } univ) :
          Set V)),
    G.Adj x x_1
Tactic: refine fun ⟨f⟩ ↦ ⟨univ.map ⟨f ∘ Sum.inl, f.injective.comp Sum.inl_injective⟩,
      univ.map ⟨f ∘ Sum.inr, f.injective.comp Sum.inr_injective⟩, by simp, by simp,
      fun _ hl _ hr ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
Goal:
V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst : Fintype α
inst_1 : Fintype β
h : completeBipartiteGraph α β ⊑ G
f : (completeBipartiteGraph α β).Copy G
x : V
hl : x ∈ (↑(map { toFun := Function.comp (β := α ⊕ β) (⇑f : (a : α ⊕ β) → V) Sum.inl, inj' := ⋯ : α ↪ V } univ) : Set V)
x_1 : V
hr :
  x_1 ∈ (↑(map { toFun := Function.comp (β := α ⊕ β) (⇑f : (a : α ⊕ β) → V) Sum.inr, inj' := ⋯ : β ↪ V } univ) : Set V)
⊢ G.Adj x x_1
have rw : ∀
  (hl :
    ∃ (a : α),
      Membership.mem (γ := Finset α) univ a ∧
        ({ toFun := Function.comp (β := α ⊕ β) (⇑f : (a : α ⊕ β) → V) Sum.inl, inj' := sorry : α ↪ V } : (a : α) → V) a = x)
  (x_2 : V)
  (hr :
    ∃ (a : β),
      Membership.mem (γ := Finset β) univ a ∧
        ({ toFun := Function.comp (β := α ⊕ β) (⇑f : (a : α ⊕ β) → V) Sum.inr, inj' := sorry : β ↪ V } : (a : β) → V) a =
          x_2),
  G.Adj x x_2
Tactic: rw [mem_coe, mem_map] at hl hr
Cleared hypotheses: hl, x_1, hr
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
Goal:
V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst : Fintype α
inst_1 : Fintype β
h : completeBipartiteGraph α β ⊑ G
f : (completeBipartiteGraph α β).Copy G
x : V
hl :
  ∃ (a : α),
    Membership.mem (γ := Finset α) univ a ∧
      ({ toFun := Function.comp (β := α ⊕ β) (⇑f : (a : α ⊕ β) → V) Sum.inl, inj' := ⋯ : α ↪ V } : (a : α) → V) a = x
x_1 : V
hr :
  ∃ (a : β),
    Membership.mem (γ := Finset β) univ a ∧
      ({ toFun := Function.comp (β := α ⊕ β) (⇑f : (a : α ⊕ β) → V) Sum.inr, inj' := ⋯ : β ↪ V } : (a : β) → V) a = x_1
⊢ G.Adj x x_1
have replace : ∀ (w : α),
  Membership.mem (γ := Finset α) univ w →
    ∀
      (hl :
        ({ toFun := Function.comp (β := α ⊕ β) (⇑f : (a : α ⊕ β) → V) Sum.inl, inj' := sorry : α ↪ V } : (a : α) → V) w =
          x),
      G.Adj x x_1
Tactic: replace ⟨_, _, hl⟩ := hl
Cleared hypotheses: hl