@[category research solved, AMS 5]
theorem theorem1 (G : SimpleGraph α) [DecidableRel G.Adj] (h₁ : G.CliqueFree 3) (h₂ : f G = 2) :
    G.IsBipartite ∧ G.minDegree = 1 ∧ HasCompactdegreeSequence G := by
  -- AlphaProof found a disproof
  negate_goal
  by_contra! p
  specialize@p<|ULift (Fin 2)
  delta SimpleGraph.IsBipartite SimpleGraph.minDegree SimpleGraph.degree SimpleGraph.f SimpleGraph.CliqueFree at*
  norm_cast at*
  delta SimpleGraph.largestInducedForestSize at*
  simp_rw [SimpleGraph.isAcyclic_iff_forall_adj_isBridge]at*
  use(p ⊥ (by decide) (IsGreatest.csSup_eq ⟨⟨⊤, nofun, rfl⟩, fun and⟨A, B, C⟩=>C▸ A.card_le_univ⟩)).elim (by norm_num+decide[← Fintype.card_coe])

/-- **Lemma 3.** For every `n` there exists a bipartite graph with
`8 n` vertices, minimum degree `n + 1`, and `f = 3`. -/
@[category API, AMS 5]
lemma lemma3 (n : ℕ) (hn : 0 < n) :
    ∃ (G : SimpleGraph (Fin (8 * n))) (_ : DecidableRel G.Adj),
      G.IsBipartite ∧ G.minDegree = n + 1 ∧ f G = 3 := by
  -- AlphaProof found a disproof
  negate_goal
  delta SimpleGraph.IsBipartite Ne SimpleGraph.degree SimpleGraph.minDegree SimpleGraph.f
  delta SimpleGraph.largestInducedForestSize
  use 64,by decide,mod_cast fun and y ⟨a, _⟩ A B=>?_
  have:=Fintype.card_congr ((.sigmaFiberEquiv a))▸ Fintype.card_sigma
  replace B y: Fintype.card {s | a s=y}≤3:=( Fintype.card_subtype _).trans_le (B▸le_csSup ((Set.toFinite _).image _).exists_le ⟨ _,?_, rfl⟩)
  · norm_num[SimpleGraph.isAcyclic_iff_forall_adj_isBridge]at‹∀_, _›⊢
    use fun and R M K V=>absurd (‹∀ (x _),_› and M) (by norm_num[*])
  · use (by decide ∘(Fintype.card_fin _▸this).trans_le) ( Finset.sum_le_sum fun and k=>B _)