-- Mathlib/Combinatorics/Extremal/RuzsaSzemeredi.lean
private lemma noAccidental (hs : ThreeAPFree (s : Set α)) :
    NoAccidental (triangleIndices s : Finset (α × α × α)) where
  eq_or_eq_or_eq

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : CommRing α
s : Finset α
hs : ThreeAPFree ↑s
d a : α
ha : a ∈ s
d' c : α
hc : c ∈ s
h₂ : d' + c = d + a
hb : a ∈ s
h₁ : d' + 2 * a = d + 2 * a
this : a + c = a + a
⊢ d' = d ∨ d + a = d' + a ∨ d + 2 * a = d' + 2 * c

Tactic:
simp_all

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : CommRing α
s : Finset α
hs : ThreeAPFree ↑s
⊢ ∀ ⦃a a' b b' c c' : α⦄,
    (a', b, c) ∈ triangleIndices s →
      (a, b', c) ∈ triangleIndices s → (a, b, c') ∈ triangleIndices s → a = a' ∨ b = b' ∨ c = c'

Tactic:
simp only [mem_triangleIndices, Prod.mk.inj_iff, exists_prop, forall_exists_index, and_imp]

Result:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : CommRing α
s : Finset α
hs : ThreeAPFree ↑s
⊢ ∀ ⦃a a' b b' c c' : α⦄ (x x_1 : α),
    x_1 ∈ s →
      x = a' →
        x + x_1 = b →
          x + 2 * x_1 = c →
            ∀ (x x_2 : α),
              x_2 ∈ s →
                x = a →
                  x + x_2 = b' →
                    x + 2 * x_2 = c →
                      ∀ (x x_3 : α), x_3 ∈ s → x = a → x + x_3 = b → x + 2 * x_3 = c' → a = a' ∨ b = b' ∨ c = c'

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : CommRing α
s : Finset α
hs : ThreeAPFree ↑s
d a : α
ha : a ∈ s
b : α
hb : b ∈ s
d' c : α
hc : c ∈ s
h₁ : d' + 2 * b = d + 2 * a
h₂ : d' + c = d + a
⊢ d' = d ∨ d + a = d' + b ∨ d + 2 * a = d' + 2 * c

Tactic:
have : a + c = b + b := by linear_combination h₁.symm - h₂.symm

Result:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : CommRing α
s : Finset α
hs : ThreeAPFree ↑s
d a : α
ha : a ∈ s
b : α
hb : b ∈ s
d' c : α
hc : c ∈ s
h₁ : d' + 2 * b = d + 2 * a
h₂ : d' + c = d + a
this : a + c = b + b
⊢ d' = d ∨ d + a = d' + b ∨ d + 2 * a = d' + 2 * c

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : CommRing α
s : Finset α
hs : ThreeAPFree ↑s
d a : α
ha : a ∈ s
b : α
hb : b ∈ s
d' c : α
hc : c ∈ s
h₁ : d' + 2 * b = d + 2 * a
h₂ : d' + c = d + a
⊢ a + c = b + b

Tactic:
linear_combination h₁.symm - h₂.symm

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : CommRing α
s : Finset α
hs : ThreeAPFree ↑s
d a : α
ha : a ∈ s
b : α
hb : b ∈ s
d' c : α
hc : c ∈ s
h₁ : d' + 2 * b = d + 2 * a
h₂ : d' + c = d + a
this : a + c = b + b
⊢ d' = d ∨ d + a = d' + b ∨ d + 2 * a = d' + 2 * c

Tactic:
obtain rfl := hs ha hb hc this

Result:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : CommRing α
s : Finset α
hs : ThreeAPFree ↑s
d a : α
ha : a ∈ s
d' c : α
hc : c ∈ s
h₂ : d' + c = d + a
hb : a ∈ s
h₁ : d' + 2 * a = d + 2 * a
this : a + c = a + a
⊢ d' = d ∨ d + a = d' + a ∨ d + 2 * a = d' + 2 * c

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : CommRing α
s : Finset α
hs : ThreeAPFree ↑s
⊢ ∀ ⦃a a' b b' c c' : α⦄ (x x_1 : α),
    x_1 ∈ s →
      x = a' →
        x + x_1 = b →
          x + 2 * x_1 = c →
            ∀ (x x_2 : α),
              x_2 ∈ s →
                x = a →
                  x + x_2 = b' →
                    x + 2 * x_2 = c →
                      ∀ (x x_3 : α), x_3 ∈ s → x = a → x + x_3 = b → x + 2 * x_3 = c' → a = a' ∨ b = b' ∨ c = c'

Tactic:
rintro _ _ _ _ _ _ d a ha rfl rfl rfl b' b hb rfl rfl h₁ d' c hc rfl h₂ rfl

Result:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : CommRing α
s : Finset α
hs : ThreeAPFree ↑s
d a : α
ha : a ∈ s
b : α
hb : b ∈ s
d' c : α
hc : c ∈ s
h₁ : d' + 2 * b = d + 2 * a
h₂ : d' + c = d + a
⊢ d' = d ∨ d + a = d' + b ∨ d + 2 * a = d' + 2 * c