rw [Set.insert_comm cfg.B, Set.insert_comm cfg.B, Set.pair_comm, Set.insert_comm cfg.C,
  Set.insert_comm cfg.C]
V : Type u_1
Pt : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace Pt
inst✝ : NormedAddTorsor V Pt
hd2 : Fact (finrank ℝ V = 2)
cfg : Imo2019q2Cfg V Pt
hQ : cfg.Q ∈ affineSpan ℝ {cfg.C, cfg.B}
hQA₁ : affineSpan ℝ {cfg.Q, cfg.A₁} ≤ affineSpan ℝ {cfg.C, cfg.B}
hQ₁ : cfg.Q₁ ∈ affineSpan ℝ {cfg.C, cfg.B}
⊢ Collinear ℝ {cfg.B, cfg.C, cfg.Q₁, cfg.Q}
V : Type u_1
Pt : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace Pt
inst✝ : NormedAddTorsor V Pt
hd2 : Fact (finrank ℝ V = 2)
cfg : Imo2019q2Cfg V Pt
hQ : cfg.Q ∈ affineSpan ℝ {cfg.C, cfg.B}
hQA₁ : affineSpan ℝ {cfg.Q, cfg.A₁} ≤ affineSpan ℝ {cfg.C, cfg.B}
hQ₁ : cfg.Q₁ ∈ affineSpan ℝ {cfg.C, cfg.B}
⊢ Collinear ℝ {cfg.Q₁, cfg.Q, cfg.C, cfg.B}