import Mathlib

namespace SimpleGraph

variable {V W₁ W₂ : Type*} (G : SimpleGraph V) {s t : Set V}

theorem eq_sym2_out (v : Sym2 V) : v = s(v.out.1, v.out.2) := by
  ext
  simp

theorem edgeSet_eq : G.edgeSet = { x | ∃ v w : V, x = s(v, w) ∧ G.Adj v w } := by
  refine Set.ext fun x ↦ ⟨fun h ↦ ?_, by grind [mem_edgeSet]⟩
  exact ⟨x.out.1, x.out.2, by simp [G.mem_edgeSet.mp <| eq_sym2_out x ▸ h]⟩

theorem completeBipartiteGraph_edgeSet : (completeBipartiteGraph W₁ W₂).edgeSet = Set.range (fun x : W₁ × W₂ ↦ s(.inl x.1, .inr x.2)) := by
  refine Set.ext fun x ↦ ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · simp only [edgeSet_eq, completeBipartiteGraph_adj, Sum.exists, Sum.isRight_inl,
      Bool.false_eq_true, and_false, Sum.isLeft_inl, and_true, false_or, exists_and_right,
      Sum.isRight_inr, Sum.isLeft_inr, or_false, Set.mem_setOf_eq] at h
    cases h with | inl h' | inr h' <;> obtain ⟨u,v,huv⟩ := h' <;> simp_all
  · obtain ⟨u, v, huv⟩ := h
    simp

theorem completeBipartiteGraph_edgeSet_encard : (completeBipartiteGraph W₁ W₂).edgeSet.encard = ENat.card W₁ * ENat.card W₂ := by
  let g (x : W₁ × W₂) : Sym2 (W₁ ⊕ W₂) := s(.inl x.1, .inr x.2)
  have : Function.Injective g := fun _ _ _ ↦ by grind
  have := this.encard_image Set.univ
  simpa [completeBipartiteGraph_edgeSet, this]

theorem IsBipartiteWith.induce_encard_edgeSet_le {s t : Set V} (hG : G.IsBipartiteWith s t) :
    (G.induce (s ∪ t)).edgeSet.encard ≤ s.encard * t.encard := by
  have : (G.induce (s ∪ t)).edgeSet.encard ≤ (completeBipartiteGraph s t).edgeSet.encard := by
    refine Function.Embedding.encard_le ?_
    classical
    set f : ↑(s ∪ t) → (↑s ⊕ ↑t) :=
      fun h => if h₀ : ↑h ∈ s then Sum.inl ⟨↑h, h₀⟩ else Sum.inr ⟨↑h, by grind⟩
    set f₀ : ↑(induce (s ∪ t) G).edgeSet → ↑(completeBipartiteGraph ↑s ↑t).edgeSet := by
      rintro ⟨e, he⟩
      use e.map f
      simp [f]
      cases e with | h x y =>
      simp only [mem_edgeSet, comap_adj, Function.Embedding.subtype_apply] at he
      simp only [Sym2.map_pair_eq, mem_edgeSet, completeBipartiteGraph_adj]
      by_cases h : ↑x ∈ s
      · have h₀ := hG.mem_of_adj he
        have h₁ := hG.disjoint
        grind
      · simp only [h, ↓reduceDIte, Sum.isLeft_inr, Bool.false_eq_true, false_and, Sum.isRight_inr,
        true_and, false_or]
        have h₀ := hG.mem_of_adj he
        grind
    use f₀
    intros x y hxy
    simp only [Subtype.mk.injEq, f₀, f] at hxy
    cases x with | mk x hx =>
    cases y with | mk y hy =>
    cases x with | h x₁ x₂ =>
    cases y with | h y₁ y₂ =>
    simp_all
    grind
  grw [this, completeBipartiteGraph_edgeSet_encard]
  simp

theorem IsBipartiteWith.induce_edgeSet_eq_edgeSet {s t : Set V} (hG : G.IsBipartiteWith s t) :
    G.edgeSet.encard = (G.induce (s ∪ t)).edgeSet.encard := by
  have h : G.edgeSet = (fun e => e.map (fun x => x.val)) '' (G.induce (s ∪ t)).edgeSet := by
    ext e
    cases e with | h x y =>
    simp only [mem_edgeSet, induce, Function.Embedding.coe_subtype, Set.mem_image]
    constructor
    · intro hxy
      have h₀ := hG.mem_of_adj hxy
      use s(⟨x, by grind⟩, ⟨y, by grind⟩)
      simp [hxy]
    · intros he
      obtain ⟨e, h₀, h₁⟩ := he
      cases e with | h x₁ y₁ =>
      simp only [mem_edgeSet, comap_adj] at h₀
      simp only [Sym2.map_pair_eq, Sym2.eq, Sym2.rel_iff', Prod.mk.injEq, Prod.swap_prod_mk] at h₁
      obtain h₁ | h₁ := h₁
      · grind
      · symm
        grind
  rw [h]
  apply Function.Injective.encard_image
  intros e₁ e₂ he
  simp only at he
  cases e₁ with | h x₁ y₁ =>
  cases e₂ with | h x₂ y₂ =>
  simp_all
  grind

theorem IsBipartiteWith.encard_edgeSet_le {s t : Set V} (hG : G.IsBipartiteWith s t) :
    G.edgeSet.encard ≤ s.encard * t.encard := by
  rw [induce_edgeSet_eq_edgeSet G hG]
  exact induce_encard_edgeSet_le G hG