awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
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)
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₂
⊢ α ⊕ β ↪ V

Tactic:
refine ⟨Sum.elim (Subtype.val ∘ fα) (Subtype.val ∘ fβ), fun s₁ s₂ ↦ ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
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)
s₁ s₂ : α ⊕ β
p₁ p₂ : α
⊢ Eq.{u_1 + 1} (α := V)
      (Sum.elim.{u_2, u_3, u_1 + 1} (β := β)
        (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))
        (Sum.inl p₁))
      (Sum.elim.{u_2, u_3, u_1 + 1} (β := β)
        (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))
        (Sum.inl p₂)) →
    Eq (α := α ⊕ β) (Sum.inl p₁) (Sum.inl p₂)

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
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)
s₁ s₂ : α ⊕ β
p₁ : β
p₂ : α
⊢ Eq.{u_1 + 1} (α := V)
      (Sum.elim.{u_2, u_3, u_1 + 1} (α := α)
        (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))
        (Sum.inr p₁))
      (Sum.elim.{u_2, u_3, u_1 + 1} (β := β)
        (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))
        (Sum.inl p₂)) →
    Sum.inr p₁ = Sum.inl p₂

Tactic:
simpa using (h (fα p₂).prop (fβ p₁).prop).ne'

Premises used: SimpleGraph.Adj.ne', Subtype.prop, DFunLike.coe
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
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)
s₁ s₂ : α ⊕ β
p₁ : α
p₂ : β
⊢ Eq.{u_1 + 1} (α := V)
      (Sum.elim.{u_2, u_3, u_1 + 1} (β := β)
        (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))
        (Sum.inl p₁))
      (Sum.elim.{u_2, u_3, u_1 + 1} (α := α)
        (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))
        (Sum.inr p₂)) →
    Sum.inl p₁ = Sum.inr p₂

Tactic:
simpa using (h (fα p₁).prop (fβ p₂).prop).symm.ne'

Premises used: SimpleGraph.Adj.symm, SimpleGraph.Adj.ne', Subtype.prop, DFunLike.coe
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
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)
s₁ s₂ : α ⊕ β
p₁ p₂ : β
⊢ Eq.{u_1 + 1} (α := V)
      (Sum.elim.{u_2, u_3, u_1 + 1} (α := α)
        (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))
        (Sum.inr p₁))
      (Sum.elim.{u_2, u_3, u_1 + 1} (α := α)
        (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))
        (Sum.inr p₂)) →
    Eq (α := α ⊕ β) (Sum.inr p₁) (Sum.inr p₂)

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
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)
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:
match s₁, s₂ with
    | .inl p₁, .inl p₂ => simp
    | .inr p₁, .inl p₂ =>
      simpa using (h (fα p₂).prop (fβ p₁).prop).ne'
    | .inl p₁, .inr p₂ =>
      simpa using (h (fα p₁).prop (fβ p₂).prop).symm.ne'
    | .inr p₁, .inr p₂ => simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
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' := ⋯ }
refine : ∀ {s₁ s₂ : α ⊕ β} (hadj : (_root_.completeBipartiteGraph α β).Adj s₁ s₂), G.Adj (f.toFun s₁) (f.toFun s₂)
⊢ (_root_.completeBipartiteGraph α β).Copy G

Tactic:
refine ⟨⟨f.toFun, fun {s₁ s₂} hadj ↦ ?_⟩, f.injective⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
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₂)
inr : ∀ (hs₁ : s₁.isRight = true) (hs₂ : s₂.isLeft = true), G.Adj (f.toFun s₁) (f.toFun s₂)
⊢ G.Adj (f.toFun s₁) (f.toFun s₂)

Tactic:
rcases hadj with ⟨hs₁, hs₂⟩ | ⟨hs₁, hs₂⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
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
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₂)
⊢ G.Adj (f.toFun s₁) (f.toFun s₂)

Tactic:
dsimp [f]
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
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
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₂)
⊢ G.Adj (f.toFun s₁) (f.toFun s₂)

Tactic:
dsimp [f]
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
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
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₂))
⊢ 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:
rw [← Sum.inl_getLeft s₁ hs₁, ← Sum.inr_getRight s₂ hs₂,
      Sum.elim_inl, Sum.elim_inr]

Premises used: Sum.inl_getLeft, Sum.inr_getRight, Sum.elim_inr, Sum.elim_inl
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
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
⊢ Function.comp (β := ↥left) (Subtype.val (p := fun (x : V) ↦ x ∈ left)) (⇑fα : (a : α) → ↥left) (s₁.getLeft hs₁) ∈
    (↑left : Set V)

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
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
⊢ Function.comp (β := ↥right) (Subtype.val (p := fun (x : V) ↦ x ∈ right)) (⇑fβ : (a : β) → ↥right) (s₂.getRight hs₂) ∈
    (↑right : Set V)

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
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
    (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:
exact h (by simp) (by simp)
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
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
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₁))
⊢ 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:
rw [← Sum.inr_getRight s₁ hs₁, ← Sum.inl_getLeft s₂ hs₂,
      Sum.elim_inl, Sum.elim_inr, adj_comm]

Premises used: Sum.inl_getLeft, Sum.inr_getRight, Sum.elim_inr, Sum.elim_inl, SimpleGraph.adj_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
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
⊢ Function.comp (β := ↥left) (Subtype.val (p := fun (x : V) ↦ x ∈ left)) (⇑fα : (a : α) → ↥left) (s₂.getLeft hs₂) ∈
    (↑left : Set V)

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
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
⊢ Function.comp (β := ↥right) (Subtype.val (p := fun (x : V) ↦ x ∈ right)) (⇑fβ : (a : β) → ↥right) (s₁.getRight hs₁) ∈
    (↑right : Set V)

Tactic:
simp