Theorem: Imo2019P2.Imo2019q2Cfg.symm_ω (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
⊢ cfg.symm.ω = cfg.ω
Tactic:
rw [symm_ω_eq_trianglePQB₂_circumsphere, ω]
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
⊢ circumsphere cfg.trianglePQB₂ = circumsphere cfg.triangleQPA₂

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
⊢ circumsphere cfg.trianglePQB₂ = circumsphere cfg.triangleQPA₂
Tactic:
refine circumsphere_eq_of_cospherical hd2.out cfg.cospherical_QPB₂A₂ ?_ ?_
State after:
case refine_1
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
⊢ Set.range cfg.trianglePQB₂.points ⊆ {cfg.Q, cfg.P, cfg.B₂, cfg.A₂}

case refine_2
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
⊢ Set.range cfg.triangleQPA₂.points ⊆ {cfg.Q, cfg.P, cfg.B₂, cfg.A₂}

State before:
case refine_1
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
⊢ Set.range cfg.trianglePQB₂.points ⊆ {cfg.Q, cfg.P, cfg.B₂, cfg.A₂}
Tactic:
simp only [trianglePQB₂, Matrix.range_cons, Matrix.range_empty, Set.singleton_union,
  insert_emptyc_eq]
State after:
case refine_1
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
⊢ {cfg.P, cfg.Q, cfg.B₂} ⊆ {cfg.Q, cfg.P, cfg.B₂, cfg.A₂}

State before:
case refine_1
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
⊢ {cfg.P, cfg.Q, cfg.B₂} ⊆ {cfg.Q, cfg.P, cfg.B₂, cfg.A₂}
Tactic:
rw [Set.insert_comm]
State after:
case refine_1
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
⊢ {cfg.Q, cfg.P, cfg.B₂} ⊆ {cfg.Q, cfg.P, cfg.B₂, cfg.A₂}

State before:
case refine_1
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
⊢ {cfg.Q, cfg.P, cfg.B₂} ⊆ {cfg.Q, cfg.P, cfg.B₂, cfg.A₂}
Tactic:
refine Set.insert_subset_insert (Set.insert_subset_insert ?_)
State after:
case refine_1
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
⊢ {cfg.B₂} ⊆ {cfg.B₂, cfg.A₂}

State before:
case refine_1
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
⊢ {cfg.B₂} ⊆ {cfg.B₂, cfg.A₂}
Tactic:
simp
State after:
no goals

State before:
case refine_2
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
⊢ Set.range cfg.triangleQPA₂.points ⊆ {cfg.Q, cfg.P, cfg.B₂, cfg.A₂}
Tactic:
simp only [triangleQPA₂, Matrix.range_cons, Matrix.range_empty, Set.singleton_union,
  insert_emptyc_eq]
State after:
case refine_2
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
⊢ {cfg.Q, cfg.P, cfg.A₂} ⊆ {cfg.Q, cfg.P, cfg.B₂, cfg.A₂}

State before:
case refine_2
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
⊢ {cfg.Q, cfg.P, cfg.A₂} ⊆ {cfg.Q, cfg.P, cfg.B₂, cfg.A₂}
Tactic:
refine Set.insert_subset_insert (Set.insert_subset_insert ?_)
State after:
case refine_2
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
⊢ {cfg.A₂} ⊆ {cfg.B₂, cfg.A₂}

State before:
case refine_2
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
⊢ {cfg.A₂} ⊆ {cfg.B₂, cfg.A₂}
Tactic:
simp
State after:
no goals