awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Enumerative.Stirling
Goal:
n : ℕ
zero : (HAdd.hAdd (α := ℕ) 0 1).stirlingSecond 0 = (HAdd.hAdd (α := ℕ) 0 1).choose 2
succ :
  ∀ (n : ℕ) (ih : (n + 1).stirlingSecond n = (n + 1).choose 2),
    (n + 1 + 1).stirlingSecond (n + 1) = (n + 1 + 1).choose 2
⊢ (n + 1).stirlingSecond n = (n + 1).choose 2

Tactic:
induction n with
  | zero => simp only [zero_add, stirlingSecond_succ_zero, choose_succ_self]
  | succ n ih =>
    rw [stirlingSecond_succ_succ, ih, stirlingSecond_self, mul_one,
      Nat.choose_succ_succ (n + 1), Nat.choose_one_right]

Premises used: Nat.choose_succ_succ, zero_add, Nat.choose_one_right, HAdd.hAdd, Nat.stirlingSecond_succ_zero, Nat.zero, mul_one, Nat.stirlingSecond_self, OfNat.ofNat, Nat.choose_succ_self, Nat.succ, Nat.stirlingSecond_succ_succ
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : Fintype α
inst_3 : Fintype β
G H : SimpleGraph α
⊢ ℕ

Tactic:
exact Nat.findGreatest (fun m ↦ ∃ (G : SimpleGraph α) (_ : DecidableRel G.Adj),
    #(G.cliqueFinset 3) = m ∧ G.LocallyLinear) ((card α).choose 3)

Premises used: Nat.choose, SimpleGraph.LocallyLinear, Exists, Fintype.card, Nat.findGreatest, And, Finset.card, OfNat.ofNat, SimpleGraph.cliqueFinset, Eq
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : Fintype α
inst_3 : Fintype β
G H : SimpleGraph α
⊢ ℕ

Tactic:
classical
  exact Nat.findGreatest (fun m ↦ ∃ (G : SimpleGraph α) (_ : DecidableRel G.Adj),
    #(G.cliqueFinset 3) = m ∧ G.LocallyLinear) ((card α).choose 3)
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
⊢ ruzsaSzemerediNumber α ≤ (Fintype.card α).choose 3

Tactic:
Nat.findGreatest_le _

Premises used: ruzsaSzemerediNumber, Nat.findGreatest_le
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
⊢ Finset.card.{u_1} (α := Finset α) (cliqueFinset ⊥ 3) = 0

Tactic:
simp
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
⊢ ∃ (G : SimpleGraph α) (x : DecidableRel G.Adj), #(G.cliqueFinset 3) = ruzsaSzemerediNumber α ∧ G.LocallyLinear

Tactic:
exact @Nat.findGreatest_spec _
    (fun m ↦ ∃ (G : SimpleGraph α) (_ : DecidableRel G.Adj),
      #(G.cliqueFinset 3) = m ∧ G.LocallyLinear) _ _ (Nat.zero_le _)
    ⟨⊥, inferInstance, by simp, locallyLinear_bot⟩

Premises used: SimpleGraph.locallyLinear_bot, Nat.zero_le, Nat.findGreatest_spec, inferInstance, Bot.bot, And.intro, Exists.intro
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
⊢ ∃ (G : SimpleGraph α) (x : DecidableRel G.Adj), #(G.cliqueFinset 3) = ruzsaSzemerediNumber α ∧ G.LocallyLinear

Tactic:
classical
  exact @Nat.findGreatest_spec _
    (fun m ↦ ∃ (G : SimpleGraph α) (_ : DecidableRel G.Adj),
      #(G.cliqueFinset 3) = m ∧ G.LocallyLinear) _ _ (Nat.zero_le _)
    ⟨⊥, inferInstance, by simp, locallyLinear_bot⟩
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
hG : G.LocallyLinear
⊢ #(G.cliqueFinset 3) = #(G.cliqueFinset 3)

Tactic:
congr
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
hG : G.LocallyLinear
⊢ #(G.cliqueFinset 3) ≤ ruzsaSzemerediNumber α

Tactic:
exact le_findGreatest card_cliqueFinset_le ⟨G, inferInstance, by congr, hG⟩

Premises used: Nat.le_findGreatest, SimpleGraph.card_cliqueFinset_le
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
hG : G.LocallyLinear
⊢ #(G.cliqueFinset 3) ≤ ruzsaSzemerediNumber α

Tactic:
classical
  exact le_findGreatest card_cliqueFinset_le ⟨G, inferInstance, by congr, hG⟩

Premises used: Nat.le_findGreatest, SimpleGraph.card_cliqueFinset_le
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : Fintype α
inst_3 : Fintype β
f : α ↪ β
⊢ ruzsaSzemerediNumber α ≤ ruzsaSzemerediNumber β

Tactic:
findGreatest_mono ?_ (choose_mono _ <| Fintype.card_le_of_embedding f)

Premises used: Nat.choose_mono, Nat.findGreatest_mono, ruzsaSzemerediNumber, Fintype.card_le_of_embedding
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : Fintype α
inst_3 : Fintype β
f : α ↪ β
refine :
  ∀ (n : ℕ),
    (∃ (G : SimpleGraph α) (x : DecidableRel G.Adj), #(G.cliqueFinset 3) = n ∧ G.LocallyLinear) →
      ∃ (G : SimpleGraph β) (x : DecidableRel G.Adj), #(G.cliqueFinset 3) = n ∧ G.LocallyLinear
⊢ ruzsaSzemerediNumber α ≤ ruzsaSzemerediNumber β

Tactic:
refine findGreatest_mono ?_ (choose_mono _ <| Fintype.card_le_of_embedding f)

Premises used: Nat.choose_mono, Nat.findGreatest_mono, Fintype.card_le_of_embedding
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : Fintype α
inst_3 : Fintype β
f : α ↪ β
G : SimpleGraph α
w : DecidableRel G.Adj
hG : G.LocallyLinear
⊢ ∃ (G_1 : SimpleGraph β) (x : DecidableRel G_1.Adj), #(G_1.cliqueFinset 3) = #(G.cliqueFinset 3) ∧ G_1.LocallyLinear

Tactic:
⟨G.map f, inferInstance, ?_, hG.map _⟩

Premises used: inferInstance, SimpleGraph.LocallyLinear.map, And.intro, Exists.intro, DFunLike.coe, SimpleGraph.map
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : Fintype α
inst_3 : Fintype β
f : α ↪ β
G : SimpleGraph α
w : DecidableRel G.Adj
hG : G.LocallyLinear
refine : Finset.card.{u_2} (α := Finset β) (cliqueFinset (SimpleGraph.map (⇑f : (a : α) → β) G) 3) = #(G.cliqueFinset 3)
⊢ ∃ (G_1 : SimpleGraph β) (x : DecidableRel G_1.Adj), #(G_1.cliqueFinset 3) = #(G.cliqueFinset 3) ∧ G_1.LocallyLinear

Tactic:
refine ⟨G.map f, inferInstance, ?_, hG.map _⟩
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : Fintype α
inst_3 : Fintype β
f : α ↪ β
G : SimpleGraph α
w : DecidableRel G.Adj
hG : G.LocallyLinear
rw : Ne (α := ℕ) 3 1
⊢ Finset.card.{u_2} (α := Finset β) (cliqueFinset (SimpleGraph.map (⇑f : (a : α) → β) G) 3) = #(G.cliqueFinset 3)

Tactic:
rw [← card_map ⟨map f, Finset.map_injective _⟩, ← cliqueFinset_map G f]

Premises used: Finset.card_map, Finset.map, Function.Embedding.mk, SimpleGraph.cliqueFinset_map, Finset.map_injective
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : Fintype α
inst_3 : Fintype β
f : α ↪ β
G : SimpleGraph α
w : DecidableRel G.Adj
hG : G.LocallyLinear
⊢ Ne (α := ℕ) 3 1

Tactic:
decide
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : Fintype α
inst_3 : Fintype β
f : α ↪ β
refine :
  ∀ (n : ℕ),
    (∃ (G : SimpleGraph α) (x : DecidableRel G.Adj), #(G.cliqueFinset 3) = n ∧ G.LocallyLinear) →
      ∃ (G : SimpleGraph β) (x : DecidableRel G.Adj), #(G.cliqueFinset 3) = n ∧ G.LocallyLinear
refine₁ :
  ∀ (G : SimpleGraph α) (w : DecidableRel G.Adj) (hG : G.LocallyLinear),
    ∃ (G_1 : SimpleGraph β) (x : DecidableRel G_1.Adj), #(G_1.cliqueFinset 3) = #(G.cliqueFinset 3) ∧ G_1.LocallyLinear
refine₂ :
  ∀ (G : SimpleGraph α) (w : DecidableRel G.Adj) (hG : G.LocallyLinear),
    Finset.card.{u_2} (α := Finset β) (cliqueFinset (SimpleGraph.map (⇑f : (a : α) → β) G) 3) = #(G.cliqueFinset 3)
refine₃ : ∀ (G : SimpleGraph α) (w : DecidableRel G.Adj) (hG : G.LocallyLinear), Ne (α := ℕ) 3 1
⊢ ruzsaSzemerediNumber α ≤ ruzsaSzemerediNumber β

Tactic:
classical
  refine findGreatest_mono ?_ (choose_mono _ <| Fintype.card_le_of_embedding f)
  rintro n ⟨G, _, rfl, hG⟩
  refine ⟨G.map f, inferInstance, ?_, hG.map _⟩
  rw [← card_map ⟨map f, Finset.map_injective _⟩, ← cliqueFinset_map G f]
  decide

Premises used: Finset.card_map, Nat.choose_mono, Finset.map, Function.Embedding.mk, Nat.findGreatest_mono, Finset.map_injective, Fintype.card_le_of_embedding, rfl
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : Fintype α
inst_3 : Fintype β
e : α ≃ β
⊢ ruzsaSzemerediNumber α = ruzsaSzemerediNumber β

Tactic:
(ruzsaSzemerediNumber_mono (e : α ↪ β)).antisymm <| ruzsaSzemerediNumber_mono e.symm

Premises used: LE.le.antisymm, ruzsaSzemerediNumber_mono, Equiv.toEmbedding, Equiv.symm
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
⊢ ruzsaSzemerediNumberNat (Fintype.card α) = ruzsaSzemerediNumber α

Tactic:
ruzsaSzemerediNumber_congr (Fintype.equivFin _).symm

Premises used: ruzsaSzemerediNumber_congr, Fintype.equivFin, ruzsaSzemerediNumberNat, Equiv.symm
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
⊢ Monotone ruzsaSzemerediNumberNat

Tactic:
fun _m _n h =>
  ruzsaSzemerediNumber_mono (Fin.castLEEmb h)

Premises used: Monotone, Fin.castLEEmb, ruzsaSzemerediNumber_mono, ruzsaSzemerediNumberNat
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
n : ℕ
rw rw₁ : n.choose 3 = n.choose 3
⊢ (Fintype.card (Fin n)).choose 3 = n.choose 3

Tactic:
rw [Fintype.card_fin]

Premises used: Fintype.card_fin
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
⊢ ruzsaSzemerediNumberNat 0 = 0

Tactic:
le_zero_iff.1 ruzsaSzemerediNumberNat_le

Premises used: le_zero_iff, ruzsaSzemerediNumberNat_le, Iff.mp
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
⊢ ruzsaSzemerediNumberNat 1 = 0

Tactic:
le_zero_iff.1 ruzsaSzemerediNumberNat_le

Premises used: le_zero_iff, ruzsaSzemerediNumberNat_le, Iff.mp
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
⊢ ruzsaSzemerediNumberNat 2 = 0

Tactic:
le_zero_iff.1 ruzsaSzemerediNumberNat_le

Premises used: le_zero_iff, ruzsaSzemerediNumberNat_le, Iff.mp
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : CommRing α
s_1 : Finset α
x_1 : α × α × α
s : Finset α
x a y b : α
h :
  Eq.{u_1 + 1} (α := α × α × α) ((fun (xa : α × α) ↦ (xa.1, xa.1 + xa.2, xa.1 + 2 * xa.2)) (x, a))
    ((fun (xa : α × α) ↦ (xa.1, xa.1 + xa.2, xa.1 + 2 * xa.2)) (y, b))
⊢ x = y ∧ x + a = y + b ∧ x + 2 * a = y + 2 * b

Tactic:
simp only [Prod.ext_iff] at h

Premises used: Prod.ext_iff
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : CommRing α
s_1 : Finset α
x_1 : α × α × α
s : Finset α
x a y b : α
h : x = y ∧ x + a = y + b ∧ x + 2 * a = y + 2 * b
obtain : ∀ (h : x = x ∧ x + a = x + b ∧ x + 2 * a = x + 2 * b), (x, a) = (x, b)
⊢ (x, a) = (y, b)

Tactic:
obtain rfl := h.1

Premises used: And.left, rfl
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : CommRing α
s_1 : Finset α
x_1 : α × α × α
s : Finset α
x a b : α
h : x = x ∧ x + a = x + b ∧ x + 2 * a = x + 2 * b
obtain : ∀ (h : x = x ∧ x + a = x + a ∧ x + 2 * a = x + 2 * a), (x, a) = (x, a)
⊢ (x, a) = (x, b)

Tactic:
obtain rfl := add_right_injective _ h.2.1

Premises used: add_right_injective, And.right, And.left, rfl
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : CommRing α
s_1 : Finset α
x_1 : α × α × α
s : Finset α
x a : α
h : x = x ∧ x + a = x + a ∧ x + 2 * a = x + 2 * a
⊢ (x, a) = (x, a)

Tactic:
rfl
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
α : Type u_1
inst : Fintype α
inst_1 : CommRing α
s : Finset α
x : α × α × α
⊢ x ∈ triangleIndices s ↔ ∃ (y : α), ∃ a ∈ s, (y, y + a, y + 2 * a) = x

Tactic:
simp [triangleIndices]

Premises used: _private.0.triangleIndices
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
α : Type u_1
inst : Fintype α
inst_1 : CommRing α
s : Finset α
⊢ #(triangleIndices s) = Fintype.card α * #s

Tactic:
simp [triangleIndices]

Premises used: _private.0.triangleIndices
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
α : Type u_1
inst : Fintype α
inst_1 : CommRing α
s : Finset α
hs : ThreeAPFree (↑s : Set α)
simp :
  ∀ ⦃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'
⊢ ∀ ⦃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, forall_exists_index, and_imp]

Premises used: and_imp, Prod.mk_inj, forall_exists_index, _private.0.mem_triangleIndices
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
α : Type u_1
inst : Fintype α
inst_1 : CommRing α
s : Finset α
hs : ThreeAPFree (↑s : Set α)
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

Premises used: Eq.symm
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
α : Type u_1
inst : Fintype α
inst_1 : CommRing α
s : Finset α
hs : ThreeAPFree (↑s : Set α)
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:
have : a + c = b + b := by linear_combination h₁.symm - h₂.symm
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
α : Type u_1
inst : Fintype α
inst_1 : CommRing α
s : Finset α
hs : ThreeAPFree (↑s : Set α)
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
obtain :
  ∀ (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
⊢ d' = d ∨ d + a = d' + b ∨ d + 2 * a = d' + 2 * c

Tactic:
obtain rfl := hs ha hb hc this

Premises used: rfl
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
α : Type u_1
inst : Fintype α
inst_1 : CommRing α
s : Finset α
hs : ThreeAPFree (↑s : Set α)
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
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : CommRing α
s : Finset α
x : α × α × α
inst_2 : Fact (IsUnit.{u_1} (M := α) 2)
simp :
  ∀ ⦃a b c a' : α⦄ (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 → a = a'
⊢ ∀ ⦃a b c a' : α⦄, (a, b, c) ∈ triangleIndices s → (a', b, c) ∈ triangleIndices s → a = a'

Tactic:
simp only [mem_triangleIndices, Prod.mk_inj, forall_exists_index, and_imp]

Premises used: and_imp, Prod.mk_inj, forall_exists_index, _private.0.mem_triangleIndices
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : CommRing α
s : Finset α
x_1 : α × α × α
inst_2 : Fact (IsUnit.{u_1} (M := α) 2)
x a : α
ha : a ∈ s
y b : α
hb : b ∈ s
h₁ : y + b = x + a
h₂ : y + 2 * b = x + 2 * a
⊢ x = y

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

Premises used: Eq.symm
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : CommRing α
s : Finset α
x : α × α × α
inst_2 : Fact (IsUnit.{u_1} (M := α) 2)
simp :
  ∀ ⦃a b c b' : α⦄ (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 → b = b'
⊢ ∀ ⦃a b c b' : α⦄, (a, b, c) ∈ triangleIndices s → (a, b', c) ∈ triangleIndices s → b = b'

Tactic:
simp only [mem_triangleIndices, Prod.mk_inj, forall_exists_index, and_imp]

Premises used: and_imp, Prod.mk_inj, forall_exists_index, _private.0.mem_triangleIndices
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : CommRing α
s : Finset α
x : α × α × α
inst_2 : Fact (IsUnit.{u_1} (M := α) 2)
a : α
ha : a ∈ s
y b : α
hb : b ∈ s
h : y + 2 * b = y + 2 * a
⊢ y + a = y + b

Tactic:
simpa [(Fact.out (p := IsUnit (2 : α))).mul_right_inj, eq_comm] using h

Premises used: eq_comm, IsUnit.mul_right_inj, Fact.out
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : CommRing α
s : Finset α
x : α × α × α
inst_2 : Fact (IsUnit.{u_1} (M := α) 2)
simp :
  ∀ ⦃a 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' → c = c'
⊢ ∀ ⦃a b c c' : α⦄, (a, b, c) ∈ triangleIndices s → (a, b, c') ∈ triangleIndices s → c = c'

Tactic:
simp only [mem_triangleIndices, Prod.mk_inj, forall_exists_index, and_imp]

Premises used: and_imp, Prod.mk_inj, forall_exists_index, _private.0.mem_triangleIndices
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : CommRing α
s : Finset α
x : α × α × α
inst_2 : Fact (IsUnit.{u_1} (M := α) 2)
a : α
ha : a ∈ s
y b : α
hb : b ∈ s
h : y + b = y + a
⊢ y + 2 * a = y + 2 * b

Tactic:
simpa [(Fact.out (p := IsUnit (2 : α))).mul_right_inj, eq_comm] using h

Premises used: eq_comm, IsUnit.mul_right_inj, Fact.out
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
α : Type u_1
inst : Fintype α
inst_1 : CommRing α
s : Finset α
inst_2 : Fact (IsUnit.{u_1} (M := α) 2)
hs : ThreeAPFree (↑s : Set α)
⊢ (graph (triangleIndices s)).LocallyLinear

Tactic:
haveI := noAccidental hs; TripartiteFromTriangles.locallyLinear _

Premises used: SimpleGraph.TripartiteFromTriangles.locallyLinear, _private.0.triangleIndices
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
α : Type u_1
inst : Fintype α
inst_1 : CommRing α
s : Finset α
inst_2 : Fact (IsUnit.{u_1} (M := α) 2)
hs : ThreeAPFree (↑s : Set α)
inst_3 : DecidableEq α
⊢ NoAccidental (triangleIndices s)

Tactic:
haveI := noAccidental hs
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
α : Type u_1
inst : Fintype α
inst_1 : CommRing α
s : Finset α
inst_2 : Fact (IsUnit.{u_1} (M := α) 2)
hs : ThreeAPFree (↑s : Set α)
inst_3 : DecidableEq α
this : NoAccidental (triangleIndices s)
rw : 3 * #((graph (triangleIndices s)).cliqueFinset 3) = 3 * Fintype.card α * #s
rw₁ : 3 * #(triangleIndices s) = 3 * Fintype.card α * #s
rw₂ : 3 * (Fintype.card α * #s) = 3 * Fintype.card α * #s
rw₃ rw₄ : 3 * (Fintype.card α * #s) = 3 * (Fintype.card α * #s)
⊢ #(graph (triangleIndices s)).edgeFinset = 3 * Fintype.card α * #s

Tactic:
rw [(locallyLinear hs).card_edgeFinset, card_triangles, card_triangleIndices, mul_assoc]

Premises used: _private.0.card_triangleIndices, mul_assoc, SimpleGraph.LocallyLinear.card_edgeFinset, SimpleGraph.TripartiteFromTriangles.card_triangles, _private.0.locallyLinear
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : CommRing α
inst_3 : Fact (IsUnit.{u_1} (M := α) 2)
obtain :
  ∀ (s : Finset α) (hscard : #s = (addRothNumber : (a : Finset α) → ℕ) univ) (hs : ThreeAPFree (↑s : Set α)),
    HMul.hMul (β := ℕ) (Fintype.card α) ((addRothNumber : (a : Finset α) → ℕ) univ : ℕ) ≤
      ruzsaSzemerediNumber.{u_1} (α ⊕ α ⊕ α)
⊢ HMul.hMul (β := ℕ) (Fintype.card α) ((addRothNumber : (a : Finset α) → ℕ) univ : ℕ) ≤
    ruzsaSzemerediNumber.{u_1} (α ⊕ α ⊕ α)

Tactic:
obtain ⟨s, -, hscard, hs⟩ := addRothNumber_spec (univ : Finset α)

Premises used: Finset.univ, addRothNumber_spec
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : CommRing α
inst_3 : Fact (IsUnit.{u_1} (M := α) 2)
s : Finset α
hscard : #s = (addRothNumber : (a : Finset α) → ℕ) univ
hs : ThreeAPFree (↑s : Set α)
⊢ NoAccidental (triangleIndices s)

Tactic:
haveI := noAccidental hs
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : CommRing α
inst_3 : Fact (IsUnit.{u_1} (M := α) 2)
s : Finset α
hscard : #s = (addRothNumber : (a : Finset α) → ℕ) univ
hs : ThreeAPFree (↑s : Set α)
this : NoAccidental (triangleIndices s)
rw : #((graph (triangleIndices s)).cliqueFinset 3) ≤ ruzsaSzemerediNumber.{u_1} (α ⊕ α ⊕ α)
⊢ HMul.hMul (β := ℕ) (Fintype.card α) ((addRothNumber : (a : Finset α) → ℕ) univ : ℕ) ≤
    ruzsaSzemerediNumber.{u_1} (α ⊕ α ⊕ α)

Tactic:
rw [← hscard, ← card_triangleIndices, ← card_triangles]

Premises used: _private.0.card_triangleIndices, SimpleGraph.TripartiteFromTriangles.card_triangles
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : CommRing α
inst_3 : Fact (IsUnit.{u_1} (M := α) 2)
s : Finset α
hscard : #s = (addRothNumber : (a : Finset α) → ℕ) univ
hs : ThreeAPFree (↑s : Set α)
this : NoAccidental (triangleIndices s)
⊢ #((graph (triangleIndices s)).cliqueFinset 3) ≤ ruzsaSzemerediNumber.{u_1} (α ⊕ α ⊕ α)

Tactic:
(locallyLinear hs).le_ruzsaSzemerediNumber

Premises used: SimpleGraph.LocallyLinear.le_ruzsaSzemerediNumber, _private.0.locallyLinear
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : CommRing α
inst_3 : Fact (IsUnit.{u_1} (M := α) 2)
s : Finset α
hscard : #s = (addRothNumber : (a : Finset α) → ℕ) univ
hs : ThreeAPFree (↑s : Set α)
this : NoAccidental (triangleIndices s)
⊢ #((graph (triangleIndices s)).cliqueFinset 3) ≤ ruzsaSzemerediNumber.{u_1} (α ⊕ α ⊕ α)

Tactic:
exact (locallyLinear hs).le_ruzsaSzemerediNumber

Premises used: SimpleGraph.LocallyLinear.le_ruzsaSzemerediNumber, _private.0.locallyLinear
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
n : ℕ
α : Type := Fin (2 * n + 1)
⊢ Coprime 2 (2 * n + 1)

Tactic:
simp
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
n : ℕ
α : Type := Fin (2 * n + 1)
⊢ Coprime 2 (2 * n + 1)

Tactic:
have : Nat.Coprime 2 (2 * n + 1) := by simp
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
n : ℕ
α : Type := Fin (2 * n + 1)
this : Coprime 2 (2 * n + 1)
⊢ IsUnit (M := Fin (2 * n + 1)) 2

Tactic:
simpa using (ZMod.unitOfCoprime 2 this).isUnit

Premises used: ZMod.unitOfCoprime, Units.isUnit, OfNat.ofNat
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
n : ℕ
α : Type := Fin (2 * n + 1)
this : Coprime 2 (2 * n + 1)
⊢ Fact (IsUnit (M := Fin (2 * n + 1)) 2)

Tactic:
haveI : Fact (IsUnit (2 : Fin (2 * n + 1))) := ⟨by simpa using (ZMod.unitOfCoprime 2 this).isUnit⟩
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
n : ℕ
α : Type := Fin (2 * n + 1)
this_1 : Coprime 2 (2 * n + 1)
this : Fact (IsUnit (M := Fin (2 * n + 1)) 2)
rw :
  HMul.hMul (β := ℕ) (2 * n + 1) ((rothNumberNat : (a : ℕ) → ℕ) n : ℕ) =
    HMul.hMul (β := ℕ) (Fintype.card α) ((rothNumberNat : (a : ℕ) → ℕ) n : ℕ)
rw₁ rw₂ :
  HMul.hMul (β := ℕ) (2 * n + 1) ((rothNumberNat : (a : ℕ) → ℕ) n : ℕ) =
    HMul.hMul (β := ℕ) (2 * n + 1) ((rothNumberNat : (a : ℕ) → ℕ) n : ℕ)
⊢ HMul.hMul (β := ℕ) (2 * n + 1) ((rothNumberNat : (a : ℕ) → ℕ) n : ℕ) =
    HMul.hMul (β := ℕ) (Fintype.card α) ((addRothNumber : (a : Finset α) → ℕ) (Iio (↑n : α)) : ℕ)

Tactic:
rw [Fin.addRothNumber_eq_rothNumberNat le_rfl, Fintype.card_fin]

Premises used: Fintype.card_fin, le_rfl, Fin.addRothNumber_eq_rothNumberNat
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
n : ℕ
α : Type := Fin (2 * n + 1)
this_1 : Coprime 2 (2 * n + 1)
this : Fact (IsUnit (M := Fin (2 * n + 1)) 2)
bc : LE.le (α := Finset α) (Iio (↑n : α)) univ
⊢ HMul.hMul (β := ℕ) (Fintype.card α) ((addRothNumber : (a : Finset α) → ℕ) (Iio (↑n : α)) : ℕ) ≤
    HMul.hMul (β := ℕ) (Fintype.card α) ((addRothNumber : (a : Finset α) → ℕ) univ : ℕ)

Tactic:
gcongr