Theorem: Imo2019P2.Imo2019q2Cfg.sbtw_A_A₁_A₂ (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
⊢ Sbtw ℝ cfg.A cfg.A₁ cfg.A₂
Tactic:
refine Sphere.sbtw_secondInter cfg.A_mem_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
⊢ dist cfg.A₁ (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
⊢ dist cfg.A₁ (circumsphere cfg.triangleABC).center < (circumsphere cfg.triangleABC).radius
Tactic:
convert cfg.sbtw_B_A₁_C.dist_lt_max_dist _
State after:
case h.e'_4
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.triangleABC).radius =
    max (dist cfg.B (circumsphere cfg.triangleABC).center) (dist cfg.C (circumsphere cfg.triangleABC).center)

State before:
case h.e'_4
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.triangleABC).radius =
    max (dist cfg.B (circumsphere cfg.triangleABC).center) (dist cfg.C (circumsphere cfg.triangleABC).center)
Tactic:
change _ = max (dist (cfg.triangleABC.points 1) _) (dist (cfg.triangleABC.points 2) _)
State after:
case h.e'_4
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.triangleABC).radius =
    max (dist (cfg.triangleABC.points 1) (circumsphere cfg.triangleABC).center)
      (dist (cfg.triangleABC.points 2) (circumsphere cfg.triangleABC).center)

State before:
case h.e'_4
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.triangleABC).radius =
    max (dist (cfg.triangleABC.points 1) (circumsphere cfg.triangleABC).center)
      (dist (cfg.triangleABC.points 2) (circumsphere cfg.triangleABC).center)
Tactic:
simp_rw [circumsphere_center, circumsphere_radius, dist_circumcenter_eq_circumradius, max_self]
State after:
no goals