have hBQ₁Q : AffineIndependent ℝ ![cfg.B, cfg.Q₁, cfg.Q] :=
  hc.affineIndependent_of_mem_of_ne (Set.mem_insert_of_mem _ (Set.mem_insert _ _))
    (Set.mem_insert_of_mem _ (Set.mem_insert_of_mem _ (Set.mem_insert _ _)))
    (Set.mem_insert_of_mem _
      (Set.mem_insert_of_mem _ (Set.mem_insert_of_mem _ (Set.mem_singleton _))))
    hBQ₁ cfg.Q_ne_B.symm hQQ₁.symm
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
h : cfg.A₁ = cfg.B
hwbtw : Wbtw ℝ cfg.A cfg.P cfg.B
hPQ : affineSpan ℝ {cfg.P, cfg.Q} = affineSpan ℝ {cfg.A, cfg.B}
this : Module.Oriented ℝ V (Fin 2)
haQ : 2 • ∡ cfg.C cfg.B cfg.Q = 2 • ∡ cfg.C cfg.B cfg.A
ha : 2 • ∡ cfg.C cfg.B cfg.Q = 2 • ∡ cfg.C cfg.Q₁ cfg.Q
hn : ¬Collinear ℝ {cfg.C, cfg.B, cfg.Q}
hc : Cospherical {cfg.C, cfg.B, cfg.Q₁, cfg.Q}
hBQ₁ : cfg.B ≠ cfg.Q₁
hQQ₁ : cfg.Q ≠ cfg.Q₁
⊢ False
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
h : cfg.A₁ = cfg.B
hwbtw : Wbtw ℝ cfg.A cfg.P cfg.B
hPQ : affineSpan ℝ {cfg.P, cfg.Q} = affineSpan ℝ {cfg.A, cfg.B}
this : Module.Oriented ℝ V (Fin 2)
haQ : 2 • ∡ cfg.C cfg.B cfg.Q = 2 • ∡ cfg.C cfg.B cfg.A
ha : 2 • ∡ cfg.C cfg.B cfg.Q = 2 • ∡ cfg.C cfg.Q₁ cfg.Q
hn : ¬Collinear ℝ {cfg.C, cfg.B, cfg.Q}
hc : Cospherical {cfg.C, cfg.B, cfg.Q₁, cfg.Q}
hBQ₁ : cfg.B ≠ cfg.Q₁
hQQ₁ : cfg.Q ≠ cfg.Q₁
hBQ₁Q : AffineIndependent ℝ ![cfg.B, cfg.Q₁, cfg.Q]
⊢ False