English
The GP-free property of a set is characterized by GP-free of s and two extra conditions when inserting an element a: ThreeGPFree(insert a s) holds exactly when ThreeGPFree s holds together with the two compatibility conditions between a and elements of s.
Русский
Свойство GP-free для множества охарактеризовано вставкой элемента a: ThreeGPFree(вставить a в s) эквивалентно ThreeGPFree(s) и двум дополнительным условиям совместимости между a и элементами s.
LaTeX
$$$ThreeGPFree(insert\ a\ s) \iff ThreeGPFree(s) \land (\forall b\in s\forall c\in s, a*c=b^2 \Rightarrow a=b) \land (\forall b\in s\forall c\in s, b*c=a^2 \Rightarrow b=a)$$$
Lean4
@[to_additive]
theorem threeGPFree_insert :
ThreeGPFree (insert a s) ↔
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 :=
by
refine
⟨fun hs ↦
⟨hs.mono (subset_insert _ _), fun b hb c hc ↦ hs (Or.inl rfl) (Or.inr hb) (Or.inr hc), fun b hb c hc ↦
hs (Or.inr hb) (Or.inl rfl) (Or.inr hc)⟩,
?_⟩
rintro ⟨hs, ha, ha'⟩ b hb c hc d hd h
rw [mem_insert_iff] at hb hc hd
obtain rfl | hb := hb <;> obtain rfl | hc := hc
· rfl
all_goals obtain rfl | hd := hd
· exact (ha' hc hc h.symm).symm
· exact ha hc hd h
· exact mul_right_cancel h
· exact ha' hb hd h
· obtain rfl := ha hc hb ((mul_comm _ _).trans h)
exact ha' hb hc h
· exact hs hb hc hd h
