awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
α : Type u_2
inst : CommMonoid α
inst_1 : IsCancelMul α
s : Set α
hs : ThreeGPFree s
b c d : α
h : b * d = c * c
ha : ∀ ⦃b_1 : α⦄, b_1 ∈ s → ∀ ⦃c : α⦄, c ∈ s → b * c = b_1 * b_1 → b = b_1
ha' : ∀ ⦃b_1 : α⦄, b_1 ∈ s → ∀ ⦃c : α⦄, c ∈ s → b_1 * c = b * b → b_1 = b
hc : c ∈ s
hd : d ∈ s
⊢ b = c

Tactic:
ha hc hd h
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
α : Type u_2
inst : CommMonoid α
inst_1 : IsCancelMul α
s : Set α
hs : ThreeGPFree s
b c d : α
h : b * d = c * c
ha : ∀ ⦃b_1 : α⦄, b_1 ∈ s → ∀ ⦃c : α⦄, c ∈ s → b * c = b_1 * b_1 → b = b_1
ha' : ∀ ⦃b_1 : α⦄, b_1 ∈ s → ∀ ⦃c : α⦄, c ∈ s → b_1 * c = b * b → b_1 = b
hc : c ∈ s
hd : d ∈ s
⊢ b = c

Tactic:
exact ha hc hd h
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
α : Type u_2
inst : CommMonoid α
inst_1 : IsCancelMul α
s : Set α
hs : ThreeGPFree s
b d : α
hb : b ∈ s
h : b * d = d * d
ha : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → d * c = b * b → d = b
ha' : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → b * c = d * d → b = d
⊢ b = d

Tactic:
mul_right_cancel h

Premises used: mul_right_cancel
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
α : Type u_2
inst : CommMonoid α
inst_1 : IsCancelMul α
s : Set α
hs : ThreeGPFree s
b d : α
hb : b ∈ s
h : b * d = d * d
ha : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → d * c = b * b → d = b
ha' : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → b * c = d * d → b = d
⊢ b = d

Tactic:
exact mul_right_cancel h

Premises used: mul_right_cancel
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
α : Type u_2
inst : CommMonoid α
inst_1 : IsCancelMul α
s : Set α
hs : ThreeGPFree s
b c d : α
h : b * d = c * c
hb : b ∈ s
ha : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c_1 : α⦄, c_1 ∈ s → c * c_1 = b * b → c = b
ha' : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c_1 : α⦄, c_1 ∈ s → b * c_1 = c * c → b = c
hd : d ∈ s
⊢ b = c

Tactic:
ha' hb hd h
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
α : Type u_2
inst : CommMonoid α
inst_1 : IsCancelMul α
s : Set α
hs : ThreeGPFree s
b c d : α
h : b * d = c * c
hb : b ∈ s
ha : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c_1 : α⦄, c_1 ∈ s → c * c_1 = b * b → c = b
ha' : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c_1 : α⦄, c_1 ∈ s → b * c_1 = c * c → b = c
hd : d ∈ s
⊢ b = c

Tactic:
exact ha' hb hd h
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
α : Type u_2
inst : CommMonoid α
inst_1 : IsCancelMul α
s : Set α
hs : ThreeGPFree s
b c d : α
h : b * d = c * c
hb : b ∈ s
hc : c ∈ s
ha : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → d * c = b * b → d = b
ha' : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → b * c = d * d → b = d
inr : ∀ (h : b * d = d * d) (hc : d ∈ s), b = d
⊢ b = c

Tactic:
obtain rfl := ha hc hb ((mul_comm _ _).trans h)

Premises used: mul_comm, rfl, Eq.trans
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
α : Type u_2
inst : CommMonoid α
inst_1 : IsCancelMul α
s : Set α
hs : ThreeGPFree s
b d : α
hb : b ∈ s
ha : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → d * c = b * b → d = b
ha' : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → b * c = d * d → b = d
h : b * d = d * d
hc : d ∈ s
⊢ b = d

Tactic:
ha' hb hc h
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
α : Type u_2
inst : CommMonoid α
inst_1 : IsCancelMul α
s : Set α
hs : ThreeGPFree s
b d : α
hb : b ∈ s
ha : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → d * c = b * b → d = b
ha' : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → b * c = d * d → b = d
h : b * d = d * d
hc : d ∈ s
⊢ b = d

Tactic:
exact ha' hb hc h
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
α : Type u_2
inst : CommMonoid α
inst_1 : IsCancelMul α
s : Set α
a : α
hs : ThreeGPFree s
ha : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → a * c = b * b → a = b
ha' : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → b * c = a * a → b = a
b c d : α
h : b * d = c * c
hb : b ∈ s
hc : c ∈ s
hd : d ∈ s
⊢ b = c

Tactic:
hs hb hc hd h
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
α : Type u_2
inst : CommMonoid α
inst_1 : IsCancelMul α
s : Set α
a : α
hs : ThreeGPFree s
ha : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → a * c = b * b → a = b
ha' : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → b * c = a * a → b = a
b c d : α
h : b * d = c * c
hb : b ∈ s
hc : c ∈ s
hd : d ∈ s
⊢ b = c

Tactic:
exact hs hb hc hd h
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
α : Type u_2
inst : CommMonoid α
inst_1 : IsCancelMul α
s : Set α
a : α
hs : ThreeGPFree s
b : α
hb : b ∈ s
c : α
hc : c ∈ s
d : α
hd : d ∈ s
h :
  HMul.hMul (α := α) ((fun (x : α) ↦ a • x) b) ((fun (x : α) ↦ a • x) d) =
    HMul.hMul (α := α) ((fun (x : α) ↦ a • x) c) ((fun (x : α) ↦ a • x) c)
⊢ b * d = c * c

Tactic:
simpa [mul_mul_mul_comm _ _ a] using h

Premises used: mul_mul_mul_comm
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
α : Type u_2
inst : CommMonoid α
inst_1 : IsCancelMul α
s : Set α
a : α
hs : ThreeGPFree s
b : α
hb : b ∈ s
c : α
hc : c ∈ s
d : α
hd : d ∈ s
h :
  HMul.hMul (α := α) ((fun (x : α) ↦ a • x) b) ((fun (x : α) ↦ a • x) d) =
    HMul.hMul (α := α) ((fun (x : α) ↦ a • x) c) ((fun (x : α) ↦ a • x) c)
⊢ Eq.{u_2 + 1} (α := α) ((fun (x : α) ↦ a • x) b) ((fun (x : α) ↦ a • x) c)

Tactic:
exact congr_arg (a • ·) <| hs hb hc hd <| by simpa [mul_mul_mul_comm _ _ a] using h

Premises used: congr_arg, HSMul.hSMul
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
α : Type u_2
inst : CommMonoid α
inst_1 : IsCancelMul α
s : Set α
a : α
hs : ThreeGPFree (a • s)
b : α
hb : b ∈ s
c : α
hc : c ∈ s
d : α
hd : d ∈ s
h : b * d = c * c
rw : a • b * a • d = a * a * (c * c)
rw₁ : a * b * a • d = a * a * (c * c)
rw₂ : a * b * (a * d) = a * a * (c * c)
rw₃ : a * a * (b * d) = a * a * (c * c)
rw₄ rw₅ : a * a * (c * c) = a * a * (c * c)
⊢ a • b * a • d = a * c * (a * c)

Tactic:
rw [mul_mul_mul_comm, smul_eq_mul, smul_eq_mul, mul_mul_mul_comm, h]

Premises used: mul_mul_mul_comm, smul_eq_mul
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
α : Type u_2
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelMonoid α
s : Set α
a : α
hs : ∀ i ∈ s, i < a
⊢ ThreeGPFree (insert a s) ↔ ThreeGPFree s ∧ ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → a * c = b * b → a = b

Tactic:
threeGPFree_insert.trans ?_

Premises used: Iff.trans, threeGPFree_insert
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
α : Type u_2
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelMonoid α
s : Set α
a : α
hs : ∀ i ∈ s, i < a
refine :
  (ThreeGPFree s ∧
      (∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → a * c = b * b → a = b) ∧
        ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → b * c = a * a → b = a) ↔
    ThreeGPFree s ∧ ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → a * c = b * b → a = b
⊢ ThreeGPFree (insert a s) ↔ ThreeGPFree s ∧ ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → a * c = b * b → a = b

Tactic:
refine threeGPFree_insert.trans ?_

Premises used: Iff.trans, threeGPFree_insert
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
α : Type u_2
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelMonoid α
s : Set α
a : α
hs : ∀ i ∈ s, i < a
rw :
  ((ThreeGPFree s ∧ ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → a * c = b * b → a = b) ∧
      ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → b * c = a * a → b = a) ↔
    ThreeGPFree s ∧ ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → a * c = b * b → a = b
⊢ (ThreeGPFree s ∧
      (∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → a * c = b * b → a = b) ∧
        ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → b * c = a * a → b = a) ↔
    ThreeGPFree s ∧ ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → a * c = b * b → a = b

Tactic:
rw [← and_assoc]

Premises used: and_assoc
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
α : Type u_2
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelMonoid α
s : Set α
a : α
hs : ∀ i ∈ s, i < a
⊢ ((ThreeGPFree s ∧ ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → a * c = b * b → a = b) ∧
      ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → b * c = a * a → b = a) ↔
    ThreeGPFree s ∧ ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → a * c = b * b → a = b

Tactic:
and_iff_left fun b hb c hc h => ((mul_lt_mul_of_lt_of_lt (hs _ hb) (hs _ hc)).ne h).elim

Premises used: False.elim, and_iff_left, mul_lt_mul_of_lt_of_lt, LT.lt.ne
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
α : Type u_2
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelMonoid α
s : Set α
a : α
hs : ∀ i ∈ s, i < a
⊢ ((ThreeGPFree s ∧ ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → a * c = b * b → a = b) ∧
      ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → b * c = a * a → b = a) ↔
    ThreeGPFree s ∧ ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → a * c = b * b → a = b

Tactic:
exact and_iff_left fun b hb c hc h => ((mul_lt_mul_of_lt_of_lt (hs _ hb) (hs _ hc)).ne h).elim

Premises used: False.elim, and_iff_left, mul_lt_mul_of_lt_of_lt, LT.lt.ne
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
α : Type u_2
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
inst_2 : NoZeroDivisors α
s : Set α
a : α
hs : ThreeGPFree s
ha : a ≠ 0
b : α
hb : b ∈ s
c : α
hc : c ∈ s
d : α
hd : d ∈ s
h :
  HMul.hMul (α := α) ((fun (x : α) ↦ a • x) b) ((fun (x : α) ↦ a • x) d) =
    HMul.hMul (α := α) ((fun (x : α) ↦ a • x) c) ((fun (x : α) ↦ a • x) c)
⊢ b * d = c * c

Tactic:
simpa [mul_mul_mul_comm _ _ a, ha] using h

Premises used: mul_mul_mul_comm
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
α : Type u_2
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
inst_2 : NoZeroDivisors α
s : Set α
a : α
hs : ThreeGPFree s
ha : a ≠ 0
b : α
hb : b ∈ s
c : α
hc : c ∈ s
d : α
hd : d ∈ s
h :
  HMul.hMul (α := α) ((fun (x : α) ↦ a • x) b) ((fun (x : α) ↦ a • x) d) =
    HMul.hMul (α := α) ((fun (x : α) ↦ a • x) c) ((fun (x : α) ↦ a • x) c)
⊢ Eq.{u_2 + 1} (α := α) ((fun (x : α) ↦ a • x) b) ((fun (x : α) ↦ a • x) c)

Tactic:
exact congr_arg (a • ·) <| hs hb hc hd <| by simpa [mul_mul_mul_comm _ _ a, ha] using h

Premises used: congr_arg, HSMul.hSMul
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
α : Type u_2
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
inst_2 : NoZeroDivisors α
s : Set α
a : α
ha : a ≠ 0
hs : ThreeGPFree (a • s)
b : α
hb : b ∈ s
c : α
hc : c ∈ s
d : α
hd : d ∈ s
h : b * d = c * c
rw : a * b * a • d = a * c * (a * c)
rw₁ : a * b * (a * d) = a * c * (a * c)
rw₂ : a * a * (b * d) = a * c * (a * c)
rw₃ : a * a * (c * c) = a * c * (a * c)
rw₄ rw₅ : a * c * (a * c) = a * c * (a * c)
⊢ a • b * a • d = a * c * (a * c)

Tactic:
rw [smul_eq_mul, smul_eq_mul, mul_mul_mul_comm, h, mul_mul_mul_comm]

Premises used: mul_mul_mul_comm, smul_eq_mul
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
s : Set ℕ
⊢ ThreeAPFree s ↔ ∀ ⦃a : ℕ⦄, a ∈ s → ∀ ⦃b : ℕ⦄, b ∈ s → ∀ ⦃c : ℕ⦄, c ∈ s → a + c = b + b → a = c

Tactic:
forall₄_congr fun a _ha b hb => forall₃_congr fun c hc habc => ⟨?_, ?_⟩

Premises used: ThreeAPFree, forall₃_congr, Iff.intro, forall₄_congr
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
s : Set ℕ
refine_1 : ∀ (a : ℕ) (_ha : a ∈ s) (b : ℕ) (hb : b ∈ s) (c : ℕ) (hc : c ∈ s) (habc : a + c = b + b), a = b → a = c
refine_2 : ∀ (a : ℕ) (_ha : a ∈ s) (b : ℕ) (hb : b ∈ s) (c : ℕ) (hc : c ∈ s) (habc : a + c = b + b), a = c → a = b
⊢ ThreeAPFree s ↔ ∀ ⦃a : ℕ⦄, a ∈ s → ∀ ⦃b : ℕ⦄, b ∈ s → ∀ ⦃c : ℕ⦄, c ∈ s → a + c = b + b → a = c

Tactic:
refine forall₄_congr fun a _ha b hb => forall₃_congr fun c hc habc => ⟨?_, ?_⟩

Premises used: forall₃_congr, Iff.intro, forall₄_congr
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
s : Set ℕ
a : ℕ
_ha : a ∈ s
c : ℕ
hc : c ∈ s
hb : a ∈ s
habc : a + c = a + a
⊢ a = c

Tactic:
(add_left_cancel habc).symm

Premises used: add_left_cancel, Eq.symm
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
s : Set ℕ
a : ℕ
_ha : a ∈ s
c : ℕ
hc : c ∈ s
hb : a ∈ s
habc : a + c = a + a
⊢ a = c

Tactic:
exact (add_left_cancel habc).symm

Premises used: add_left_cancel, Eq.symm
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
s : Set ℕ
a : ℕ
_ha : a ∈ s
b : ℕ
hb : b ∈ s
hc : a ∈ s
habc : a + a = b + b
⊢ 2 * a = 2 * b

Tactic:
simp_rw [← two_mul] at habc

Premises used: two_mul
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
s : Set ℕ
a : ℕ
_ha : a ∈ s
b : ℕ
hb : b ∈ s
hc : a ∈ s
habc : 2 * a = 2 * b
⊢ a = b

Tactic:
mul_left_cancel₀ two_ne_zero habc

Premises used: mul_left_cancel₀, two_ne_zero
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
s : Set ℕ
a : ℕ
_ha : a ∈ s
b : ℕ
hb : b ∈ s
hc : a ∈ s
habc : 2 * a = 2 * b
⊢ a = b

Tactic:
exact mul_left_cancel₀ two_ne_zero habc

Premises used: mul_left_cancel₀, two_ne_zero
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : Monoid α
inst_2 : DecidableEq β
inst_3 : Monoid β
s t_1 t u : Finset α
htu : t ≤ u
⊢ LE.le (α := ℕ)
    ((fun (s : Finset α) ↦ Nat.findGreatest (fun (m : ℕ) ↦ ∃ t ⊆ s, #t = m ∧ ThreeGPFree (↑t : Set α)) #s) t)
    ((fun (s : Finset α) ↦ Nat.findGreatest (fun (m : ℕ) ↦ ∃ t ⊆ s, #t = m ∧ ThreeGPFree (↑t : Set α)) #s) u)

Tactic:
Nat.findGreatest_mono (fun m => ?_) (card_le_card htu)

Premises used: Finset.card_le_card, Nat.findGreatest_mono
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : Monoid α
inst_2 : DecidableEq β
inst_3 : Monoid β
s t_1 t u : Finset α
htu : t ≤ u
refine : ∀ (m : ℕ), (∃ t_2 ⊆ t, #t_2 = m ∧ ThreeGPFree (↑t_2 : Set α)) → ∃ t ⊆ u, #t = m ∧ ThreeGPFree (↑t : Set α)
⊢ LE.le (α := ℕ)
    ((fun (s : Finset α) ↦ Nat.findGreatest (fun (m : ℕ) ↦ ∃ t ⊆ s, #t = m ∧ ThreeGPFree (↑t : Set α)) #s) t)
    ((fun (s : Finset α) ↦ Nat.findGreatest (fun (m : ℕ) ↦ ∃ t ⊆ s, #t = m ∧ ThreeGPFree (↑t : Set α)) #s) u)

Tactic:
refine Nat.findGreatest_mono (fun m => ?_) (card_le_card htu)

Premises used: Finset.card_le_card, Nat.findGreatest_mono
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : Monoid α
inst_2 : DecidableEq β
inst_3 : Monoid β
s t_1 t u : Finset α
htu : t ≤ u
m : ℕ
v : Finset α
hvt : v ⊆ t
hv : #v = m ∧ ThreeGPFree (↑v : Set α)
⊢ ∃ t ⊆ u, #t = m ∧ ThreeGPFree (↑t : Set α)

Tactic:
⟨v, hvt.trans htu, hv⟩

Premises used: HasSubset.Subset.trans, And.intro, Exists.intro
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : Monoid α
inst_2 : DecidableEq β
inst_3 : Monoid β
s t_1 t u : Finset α
htu : t ≤ u
m : ℕ
v : Finset α
hvt : v ⊆ t
hv : #v = m ∧ ThreeGPFree (↑v : Set α)
⊢ ∃ t ⊆ u, #t = m ∧ ThreeGPFree (↑t : Set α)

Tactic:
exact ⟨v, hvt.trans htu, hv⟩
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Monoid α
s : Finset α
⊢ (mulRothNumber : (a : Finset α) → ℕ) s ≤ #s

Tactic:
Nat.findGreatest_le #s

Premises used: Finset.card, Nat.findGreatest_le
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Monoid α
s : Finset α
norm_cast : ThreeGPFree.{u_2} (α := α) ∅
⊢ ThreeGPFree (↑∅ : Set α)

Tactic:
norm_cast
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Monoid α
s : Finset α
⊢ ThreeGPFree.{u_2} (α := α) ∅

Tactic:
threeGPFree_empty

Premises used: threeGPFree_empty
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Monoid α
s : Finset α
⊢ ThreeGPFree.{u_2} (α := α) ∅

Tactic:
exact threeGPFree_empty

Premises used: threeGPFree_empty
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Monoid α
s t : Finset α
hs : ThreeGPFree (↑s : Set α)
h : s ⊆ t
⊢ #s ≤ (mulRothNumber : (a : Finset α) → ℕ) t

Tactic:
Nat.le_findGreatest (card_le_card h) ⟨s, h, rfl, hs⟩

Premises used: Finset.card_le_card, Nat.le_findGreatest, And.intro, Exists.intro, rfl
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Monoid α
s : Finset α
hs : ThreeGPFree (↑s : Set α)
⊢ (mulRothNumber : (a : Finset α) → ℕ) s = #s

Tactic:
(mulRothNumber_le _).antisymm <| hs.le_mulRothNumber <| Subset.refl _

Premises used: Finset.Subset.refl, LE.le.antisymm, ThreeGPFree.le_mulRothNumber, mulRothNumber_le
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Monoid α
⊢ Eq (α := ℕ) ((mulRothNumber : (a : Finset α) → ℕ) ∅ : ℕ) (0 : ℕ)

Tactic:
Nat.eq_zero_of_le_zero <| (mulRothNumber_le _).trans card_empty.le

Premises used: Eq.le, Finset.card_empty, mulRothNumber_le, LE.le.trans, Nat.eq_zero_of_le_zero
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Monoid α
a : α
⊢ Eq (α := ℕ) ((mulRothNumber : (a : Finset α) → ℕ) {a} : ℕ) (1 : ℕ)

Tactic:
ThreeGPFree.mulRothNumber_eq ?_

Premises used: ThreeGPFree.mulRothNumber_eq, Finset.card, Multiset.card
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Monoid α
a : α
refine : ThreeGPFree (↑{a} : Set α)
⊢ Eq (α := ℕ) ((mulRothNumber : (a : Finset α) → ℕ) {a} : ℕ) (1 : ℕ)

Tactic:
refine ThreeGPFree.mulRothNumber_eq ?_

Premises used: ThreeGPFree.mulRothNumber_eq
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Monoid α
a : α
rw : ThreeGPFree (α := α) {a}
⊢ ThreeGPFree (↑{a} : Set α)

Tactic:
rw [coe_singleton]

Premises used: Finset.coe_singleton
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Monoid α
a : α
⊢ ThreeGPFree (α := α) {a}

Tactic:
threeGPFree_singleton a

Premises used: threeGPFree_singleton
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Monoid α
a : α
⊢ ThreeGPFree (α := α) {a}

Tactic:
exact threeGPFree_singleton a

Premises used: threeGPFree_singleton
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Monoid α
s t u : Finset α
hus : u ⊆ s ∪ t
hcard : #u = (mulRothNumber : (a : Finset α) → ℕ) (s ∪ t)
hu : ThreeGPFree (↑u : Set α)
rw : #u = #(u ∩ (s ∪ t))
rw₁ rw₂ : #u = #u
⊢ #u = #(u ∩ s ∪ u ∩ t)

Tactic:
rw [← inter_union_distrib_left, inter_eq_left.2 hus]

Premises used: Iff.mpr, Finset.inter_union_distrib_left, Finset.inter_eq_left
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : Monoid α
inst_2 : DecidableEq β
inst_3 : Monoid β
s : Finset α
t : Finset β
obtain :
  ∀ (u : Finset α) (hus : u ⊆ s) (hucard : #u = (mulRothNumber : (a : Finset α) → ℕ) s) (hu : ThreeGPFree (↑u : Set α)),
    HMul.hMul (α := ℕ) (β := ℕ) ((mulRothNumber : (a : Finset α) → ℕ) s : ℕ)
        ((mulRothNumber : (a : Finset β) → ℕ) t : ℕ) ≤
      (mulRothNumber : (a : Finset (α × β)) → ℕ) (s ×ˢ t)
⊢ HMul.hMul (α := ℕ) (β := ℕ) ((mulRothNumber : (a : Finset α) → ℕ) s : ℕ)
      ((mulRothNumber : (a : Finset β) → ℕ) t : ℕ) ≤
    (mulRothNumber : (a : Finset (α × β)) → ℕ) (s ×ˢ t)

Tactic:
obtain ⟨u, hus, hucard, hu⟩ := mulRothNumber_spec s

Premises used: mulRothNumber_spec
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : Monoid α
inst_2 : DecidableEq β
inst_3 : Monoid β
s : Finset α
t : Finset β
u : Finset α
hus : u ⊆ s
hucard : #u = (mulRothNumber : (a : Finset α) → ℕ) s
hu : ThreeGPFree (↑u : Set α)
obtain :
  ∀ (v : Finset β) (hvt : v ⊆ t) (hvcard : #v = (mulRothNumber : (a : Finset β) → ℕ) t) (hv : ThreeGPFree (↑v : Set β)),
    HMul.hMul (α := ℕ) (β := ℕ) ((mulRothNumber : (a : Finset α) → ℕ) s : ℕ)
        ((mulRothNumber : (a : Finset β) → ℕ) t : ℕ) ≤
      (mulRothNumber : (a : Finset (α × β)) → ℕ) (s ×ˢ t)
⊢ HMul.hMul (α := ℕ) (β := ℕ) ((mulRothNumber : (a : Finset α) → ℕ) s : ℕ)
      ((mulRothNumber : (a : Finset β) → ℕ) t : ℕ) ≤
    (mulRothNumber : (a : Finset (α × β)) → ℕ) (s ×ˢ t)

Tactic:
obtain ⟨v, hvt, hvcard, hv⟩ := mulRothNumber_spec t

Premises used: mulRothNumber_spec
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : Monoid α
inst_2 : DecidableEq β
inst_3 : Monoid β
s : Finset α
t : Finset β
u : Finset α
hus : u ⊆ s
hucard : #u = (mulRothNumber : (a : Finset α) → ℕ) s
hu : ThreeGPFree (↑u : Set α)
v : Finset β
hvt : v ⊆ t
hvcard : #v = (mulRothNumber : (a : Finset β) → ℕ) t
hv : ThreeGPFree (↑v : Set β)
rw : #(u ×ˢ v) ≤ (mulRothNumber : (a : Finset (α × β)) → ℕ) (s ×ˢ t)
⊢ HMul.hMul (α := ℕ) (β := ℕ) ((mulRothNumber : (a : Finset α) → ℕ) s : ℕ)
      ((mulRothNumber : (a : Finset β) → ℕ) t : ℕ) ≤
    (mulRothNumber : (a : Finset (α × β)) → ℕ) (s ×ˢ t)

Tactic:
rw [← hucard, ← hvcard, ← card_product]

Premises used: Finset.card_product
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : Monoid α
inst_2 : DecidableEq β
inst_3 : Monoid β
s : Finset α
t : Finset β
u : Finset α
hus : u ⊆ s
hucard : #u = (mulRothNumber : (a : Finset α) → ℕ) s
hu : ThreeGPFree (↑u : Set α)
v : Finset β
hvt : v ⊆ t
hvcard : #v = (mulRothNumber : (a : Finset β) → ℕ) t
hv : ThreeGPFree (↑v : Set β)
⊢ #(u ×ˢ v) ≤ (mulRothNumber : (a : Finset (α × β)) → ℕ) (s ×ˢ t)

Tactic:
ThreeGPFree.le_mulRothNumber ?_ (product_subset_product hus hvt)

Premises used: Finset.product_subset_product, ThreeGPFree.le_mulRothNumber
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : Monoid α
inst_2 : DecidableEq β
inst_3 : Monoid β
s : Finset α
t : Finset β
u : Finset α
hus : u ⊆ s
hucard : #u = (mulRothNumber : (a : Finset α) → ℕ) s
hu : ThreeGPFree (↑u : Set α)
v : Finset β
hvt : v ⊆ t
hvcard : #v = (mulRothNumber : (a : Finset β) → ℕ) t
hv : ThreeGPFree (↑v : Set β)
refine : ThreeGPFree (↑(u ×ˢ v) : Set (α × β))
⊢ #(u ×ˢ v) ≤ (mulRothNumber : (a : Finset (α × β)) → ℕ) (s ×ˢ t)

Tactic:
refine ThreeGPFree.le_mulRothNumber ?_ (product_subset_product hus hvt)

Premises used: Finset.product_subset_product, ThreeGPFree.le_mulRothNumber
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : Monoid α
inst_2 : DecidableEq β
inst_3 : Monoid β
s : Finset α
t : Finset β
u : Finset α
hus : u ⊆ s
hucard : #u = (mulRothNumber : (a : Finset α) → ℕ) s
hu : ThreeGPFree (↑u : Set α)
v : Finset β
hvt : v ⊆ t
hvcard : #v = (mulRothNumber : (a : Finset β) → ℕ) t
hv : ThreeGPFree (↑v : Set β)
rw : ThreeGPFree ((↑u : Set α) ×ˢ (↑v : Set β))
⊢ ThreeGPFree (↑(u ×ˢ v) : Set (α × β))

Tactic:
rw [coe_product]

Premises used: Finset.coe_product
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : Monoid α
inst_2 : DecidableEq β
inst_3 : Monoid β
s : Finset α
t : Finset β
u : Finset α
hus : u ⊆ s
hucard : #u = (mulRothNumber : (a : Finset α) → ℕ) s
hu : ThreeGPFree (↑u : Set α)
v : Finset β
hvt : v ⊆ t
hvcard : #v = (mulRothNumber : (a : Finset β) → ℕ) t
hv : ThreeGPFree (↑v : Set β)
⊢ ThreeGPFree ((↑u : Set α) ×ˢ (↑v : Set β))

Tactic:
hu.prod hv

Premises used: ThreeGPFree.prod
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : Monoid α
inst_2 : DecidableEq β
inst_3 : Monoid β
s : Finset α
t : Finset β
u : Finset α
hus : u ⊆ s
hucard : #u = (mulRothNumber : (a : Finset α) → ℕ) s
hu : ThreeGPFree (↑u : Set α)
v : Finset β
hvt : v ⊆ t
hvcard : #v = (mulRothNumber : (a : Finset β) → ℕ) t
hv : ThreeGPFree (↑v : Set β)
⊢ ThreeGPFree ((↑u : Set α) ×ˢ (↑v : Set β))

Tactic:
exact hu.prod hv

Premises used: ThreeGPFree.prod
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Monoid α
s : Finset α
n : ℕ
h : ∀ t ∈ powersetCard n s, ¬ThreeGPFree (↑t : Set α)
obtain :
  ∀ (t : Finset α) (hts : t ⊆ s) (hcard : #t = (mulRothNumber : (a : Finset α) → ℕ) s) (ht : ThreeGPFree (↑t : Set α)),
    (mulRothNumber : (a : Finset α) → ℕ) s < n
⊢ (mulRothNumber : (a : Finset α) → ℕ) s < n

Tactic:
obtain ⟨t, hts, hcard, ht⟩ := mulRothNumber_spec s

Premises used: mulRothNumber_spec