import Mathlib.Combinatorics.SimpleGraph.Acyclic

universe u

namespace SimpleGraph

open Finset

/-- In a nontrivial tree, twice the order is at most the number of leaves plus the degree sum. --/
lemma IsTree.two_card_vert_le_card_leaves_plus_sum_degrees_of_nontrivial
  {V : Type u} {G : SimpleGraph V}
  [Fintype V] [Nontrivial V] [DecidableRel G.Adj]
  (h_tree : G.IsTree) : 2 * Fintype.card V ≤ #{ v | G.degree v = 1 } + ∑ v, G.degree v := by
    let is_leaf := fun x => G.degree x = 1
    let L := filter is_leaf univ
    let R := filter (fun x => ¬ is_leaf x) univ

    have h_disj : Disjoint L R := by apply disjoint_filter_filter_neg
    have h_disjUnion : univ = disjUnion L R h_disj := by grind
    have h_L_deg : ∀ v ∈ L, G.degree v = 1 := by grind

    have h_R_deg_lb : ∀ v ∈ R, G.degree v ≥ 2 := by
      intro v h_vinR
      have : 1 = G.minDegree := by simp only [h_tree, IsTree.minDegree_eq_one_of_nontrivial]
      have : 1 ≤ G.degree v := by simp only [this, minDegree_le_degree, le_of_eq_of_le]
      grind

    have h_n_l_r : Fintype.card V = #L + #R := by grind

    calc 2*Fintype.card V
      _ = 2*#L + 2*#R := by simp only [Nat.mul_add, h_n_l_r]
      _ ≤ 2*#L + ∑ v ∈ R, 2 := by
          gcongr; simp only [sum_const, smul_eq_mul, Nat.mul_comm, le_refl]
      _ ≤ 2*#L + ∑ v ∈ R, G.degree v := by gcongr with v hv; exact h_R_deg_lb v hv
      _ ≤ #L + ∑ v ∈ L, 1 + ∑ v ∈ R, G.degree v := by
          gcongr; simp only [Nat.two_mul, sum_const, smul_eq_mul, mul_one, le_refl]
      _ ≤ #L + ∑ v ∈ L, G.degree v + ∑ v ∈ R, G.degree v := by
          gcongr 2; gcongr with v hv
          exact ge_of_eq (h_L_deg v hv)
      _ ≤ #L + (∑ v ∈ L, G.degree v + ∑ v ∈ R, G.degree v) := by linarith
      _ ≤ #L + ∑ v, G.degree v := by
          gcongr; rw [h_disjUnion, sum_disjUnion]

/-- A nontrivial tree has two distinct vertices of degree one. --/
lemma IsTree.exists_two_verts_degree_one_of_nontrivial
  {V : Type u} (G : SimpleGraph V)
  [Fintype V] [Nontrivial V] [DecidableRel G.Adj]
  (h_tree : G.IsTree) : ∃ u v, G.degree u = 1 ∧ G.degree v = 1 ∧ u ≠ v := by
    let n := Fintype.card V
    let m := #G.edgeFinset
    let L : Finset V := { v | G.degree v = 1 }

    have hlem : 2*n ≤ #L + ∑ v, G.degree v := two_card_vert_le_card_leaves_plus_sum_degrees_of_nontrivial h_tree
    have : 1 < #L := by
      suffices 2*n + 2 ≤ #L + 2*n by grind
      calc 2*n + 2
        _ ≤ #L + ∑ v, G.degree v + 2 := by apply Nat.add_le_add_right hlem
        _ ≤ #L + 2*m + 2 := by rw [sum_degrees_eq_twice_card_edges]
        _ ≤ #L + 2*n := by
          have : m + 1 = n := IsTree.card_edgeFinset h_tree
          grind
    rw [one_lt_card_iff] at this
    rcases this with ⟨u, v, huL, hvL, hne⟩
    grind

end SimpleGraph