Theorem: Imo2019P2.Imo2019q2Cfg.not_collinear_QPA₂ (Compfiles/Imo2019P2.lean)

State before:
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
⊢ ¬Collinear ℝ {cfg.Q, cfg.P, cfg.A₂}
Tactic:
haveI := someOrientation V
State after:
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
this : Module.Oriented ℝ V (Fin 2)
⊢ ¬Collinear ℝ {cfg.Q, cfg.P, cfg.A₂}

State before:
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
this : Module.Oriented ℝ V (Fin 2)
⊢ ¬Collinear ℝ {cfg.Q, cfg.P, cfg.A₂}
Tactic:
rw [collinear_iff_of_two_zsmul_oangle_eq cfg.two_zsmul_oangle_QPA₂_eq_two_zsmul_oangle_BAA₂, ←
  affineIndependent_iff_not_collinear_set]
State after:
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
this : Module.Oriented ℝ V (Fin 2)
⊢ AffineIndependent ℝ ![cfg.B, cfg.A, cfg.A₂]

State before:
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
this : Module.Oriented ℝ V (Fin 2)
⊢ AffineIndependent ℝ ![cfg.B, cfg.A, cfg.A₂]
Tactic:
have h : Cospherical ({cfg.B, cfg.A, cfg.A₂} : Set Pt) := by
  refine cfg.triangleABC.circumsphere.cospherical.subset ?_
  simp only [Set.insert_subset_iff, cfg.A_mem_circumsphere, cfg.B_mem_circumsphere,
    cfg.A₂_mem_circumsphere, Sphere.mem_coe, Set.singleton_subset_iff, and_true]
State after:
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
this : Module.Oriented ℝ V (Fin 2)
h : Cospherical {cfg.B, cfg.A, cfg.A₂}
⊢ AffineIndependent ℝ ![cfg.B, cfg.A, cfg.A₂]

State before:
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
this : Module.Oriented ℝ V (Fin 2)
h : Cospherical {cfg.B, cfg.A, cfg.A₂}
⊢ AffineIndependent ℝ ![cfg.B, cfg.A, cfg.A₂]
Tactic:
exact h.affineIndependent_of_ne cfg.A_ne_B.symm cfg.A₂_ne_B.symm cfg.A₂_ne_A.symm
State after:
no goals

State before:
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
this : Module.Oriented ℝ V (Fin 2)
⊢ Cospherical {cfg.B, cfg.A, cfg.A₂}
Tactic:
refine cfg.triangleABC.circumsphere.cospherical.subset ?_
State after:
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
this : Module.Oriented ℝ V (Fin 2)
⊢ {cfg.B, cfg.A, cfg.A₂} ⊆ Metric.sphere (circumsphere cfg.triangleABC).center (circumsphere cfg.triangleABC).radius

State before:
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
this : Module.Oriented ℝ V (Fin 2)
⊢ {cfg.B, cfg.A, cfg.A₂} ⊆ Metric.sphere (circumsphere cfg.triangleABC).center (circumsphere cfg.triangleABC).radius
Tactic:
simp only [Set.insert_subset_iff, cfg.A_mem_circumsphere, cfg.B_mem_circumsphere,
  cfg.A₂_mem_circumsphere, Sphere.mem_coe, Set.singleton_subset_iff, and_true]
State after:
no goals