-- Mathlib/Combinatorics/Extremal/RuzsaSzemeredi.lean
lemma rothNumberNat_le_ruzsaSzemerediNumberNat (n : ℕ) :
    (2 * n + 1) * rothNumberNat n ≤ ruzsaSzemerediNumberNat (6 * n + 3)

Proof state:
n : ℕ
α : Type := Fin (2 * n + 1)
this✝ : Coprime 2 (2 * n + 1)
this : Fact (IsUnit 2)
⊢ ruzsaSzemerediNumber (α ⊕ α ⊕ α) = ruzsaSzemerediNumberNat (6 * n + 3)

Tactic:
simp_rw [← ruzsaSzemerediNumberNat_card, Fintype.card_sum, α, Fintype.card_fin]

Result:
n : ℕ
α : Type := Fin (2 * n + 1)
this✝ : Coprime 2 (2 * n + 1)
this : Fact (IsUnit 2)
⊢ ruzsaSzemerediNumberNat (2 * n + 1 + (2 * n + 1 + (2 * n + 1))) = ruzsaSzemerediNumberNat (6 * n + 3)

Proof state:
n : ℕ
α : Type := Fin (2 * n + 1)
this : Coprime 2 (2 * n + 1)
⊢ (2 * n + 1) * rothNumberNat n ≤ ruzsaSzemerediNumberNat (6 * n + 3)

Tactic:
haveI : Fact (IsUnit (2 : Fin (2 * n + 1))) := ⟨by simpa using (ZMod.unitOfCoprime 2 this).isUnit⟩

Result:
n : ℕ
α : Type := Fin (2 * n + 1)
this✝ : Coprime 2 (2 * n + 1)
this : Fact (IsUnit 2)
⊢ (2 * n + 1) * rothNumberNat n ≤ ruzsaSzemerediNumberNat (6 * n + 3)

Proof state:
n : ℕ
α : Type := Fin (2 * n + 1)
this : Coprime 2 (2 * n + 1)
⊢ IsUnit 2

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

Result:
no goals

Proof state:
n : ℕ
α : Type := Fin (2 * n + 1)
this✝ : Coprime 2 (2 * n + 1)
this : Fact (IsUnit 2)
⊢ Fintype.card α * addRothNumber (Iio ↑n) ≤ Fintype.card α * addRothNumber univ

Tactic:
gcongr

Result:
case bc.hab
n : ℕ
α : Type := Fin (2 * n + 1)
this✝ : Coprime 2 (2 * n + 1)
this : Fact (IsUnit 2)
⊢ Iio ↑n ≤ univ

Proof state:
n : ℕ
α : Type := Fin (2 * n + 1)
⊢ Coprime 2 (2 * n + 1)

Tactic:
simp

Result:
no goals

Proof state:
n : ℕ
⊢ (2 * n + 1) * rothNumberNat n ≤ ruzsaSzemerediNumberNat (6 * n + 3)

Tactic:
let α := Fin (2 * n + 1)

Result:
n : ℕ
α : Type := Fin (2 * n + 1)
⊢ (2 * n + 1) * rothNumberNat n ≤ ruzsaSzemerediNumberNat (6 * n + 3)

Proof state:
case bc.hab
n : ℕ
α : Type := Fin (2 * n + 1)
this✝ : Coprime 2 (2 * n + 1)
this : Fact (IsUnit 2)
⊢ Iio ↑n ≤ univ

Tactic:
exact subset_univ _

Result:
no goals

Proof state:
n : ℕ
α : Type := Fin (2 * n + 1)
this✝ : Coprime 2 (2 * n + 1)
this : Fact (IsUnit 2)
⊢ ruzsaSzemerediNumberNat (2 * n + 1 + (2 * n + 1 + (2 * n + 1))) = ruzsaSzemerediNumberNat (6 * n + 3)

Tactic:
ring_nf

Result:
no goals

Proof state:
n : ℕ
α : Type := Fin (2 * n + 1)
this✝ : Coprime 2 (2 * n + 1)
this : Fact (IsUnit 2)
⊢ (2 * n + 1) * rothNumberNat n = Fintype.card α * addRothNumber (Iio ↑n)

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

Result:
no goals

Proof state:
n : ℕ
α : Type := Fin (2 * n + 1)
⊢ (2 * n + 1) * rothNumberNat n ≤ ruzsaSzemerediNumberNat (6 * n + 3)

Tactic:
have : Nat.Coprime 2 (2 * n + 1) := by simp

Result:
n : ℕ
α : Type := Fin (2 * n + 1)
this : Coprime 2 (2 * n + 1)
⊢ (2 * n + 1) * rothNumberNat n ≤ ruzsaSzemerediNumberNat (6 * n + 3)

Proof state:
n : ℕ
α : Type := Fin (2 * n + 1)
this✝ : Coprime 2 (2 * n + 1)
this : Fact (IsUnit 2)
⊢ (2 * n + 1) * rothNumberNat n ≤ ruzsaSzemerediNumberNat (6 * n + 3)

Tactic:
calc
  (2 * n + 1) * rothNumberNat n
  _ = Fintype.card α * addRothNumber (Iio (n : α)) := by
    rw [Fin.addRothNumber_eq_rothNumberNat le_rfl, Fintype.card_fin]
  _ ≤ Fintype.card α * addRothNumber (univ : Finset α) := by
    gcongr; exact subset_univ _
  _ ≤ ruzsaSzemerediNumber (Sum α (Sum α α)) := addRothNumber_le_ruzsaSzemerediNumber _
  _ = ruzsaSzemerediNumberNat (6 * n + 3) := by
    simp_rw [← ruzsaSzemerediNumberNat_card, Fintype.card_sum, α, Fintype.card_fin]
    ring_nf

Result:
no goals