Theorem: Imo2019P2.Imo2019q2Cfg.result (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
⊢ Concyclic {cfg.P, cfg.Q, cfg.P₁, cfg.Q₁}
Tactic:
refine ⟨?_, coplanar_of_fact_finrank_eq_two _⟩
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
⊢ Cospherical {cfg.P, cfg.Q, cfg.P₁, cfg.Q₁}

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
⊢ Cospherical {cfg.P, cfg.Q, cfg.P₁, cfg.Q₁}
Tactic:
rw [cospherical_iff_exists_sphere]
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
⊢ ∃ s, {cfg.P, cfg.Q, cfg.P₁, cfg.Q₁} ⊆ Metric.sphere s.center s.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
⊢ ∃ s, {cfg.P, cfg.Q, cfg.P₁, cfg.Q₁} ⊆ Metric.sphere s.center s.radius
Tactic:
refine ⟨cfg.ω, ?_⟩
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
⊢ {cfg.P, cfg.Q, cfg.P₁, cfg.Q₁} ⊆ Metric.sphere cfg.ω.center cfg.ω.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
⊢ {cfg.P, cfg.Q, cfg.P₁, cfg.Q₁} ⊆ Metric.sphere cfg.ω.center cfg.ω.radius
Tactic:
simp only [Set.insert_subset_iff, Set.singleton_subset_iff]
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
⊢ cfg.P ∈ Metric.sphere cfg.ω.center cfg.ω.radius ∧
    cfg.Q ∈ Metric.sphere cfg.ω.center cfg.ω.radius ∧
      cfg.P₁ ∈ Metric.sphere cfg.ω.center cfg.ω.radius ∧ cfg.Q₁ ∈ Metric.sphere cfg.ω.center cfg.ω.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
⊢ cfg.P ∈ Metric.sphere cfg.ω.center cfg.ω.radius ∧
    cfg.Q ∈ Metric.sphere cfg.ω.center cfg.ω.radius ∧
      cfg.P₁ ∈ Metric.sphere cfg.ω.center cfg.ω.radius ∧ cfg.Q₁ ∈ Metric.sphere cfg.ω.center cfg.ω.radius
Tactic:
exact ⟨cfg.P_mem_ω, cfg.Q_mem_ω, cfg.P₁_mem_ω, cfg.Q₁_mem_ω⟩
State after:
no goals