internlm/Lean-Github huggingface dataset:
Theorem: Imo2019P2.Imo2019q2Cfg.not_collinear_QPA₂
Proof 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
Proof 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₂}
Theorem: Imo2019P2.Imo2019q2Cfg.not_collinear_QPA₂
Proof 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]
Proof 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₂]
Theorem: Imo2019P2.Imo2019q2Cfg.not_collinear_QPA₂
Proof 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]
Proof 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₂]
Theorem: Imo2019P2.Imo2019q2Cfg.not_collinear_QPA₂
Proof 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
Proof state after:
no goals
Theorem: Imo2019P2.Imo2019q2Cfg.not_collinear_QPA₂
Proof 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 ?_
Proof 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
Theorem: Imo2019P2.Imo2019q2Cfg.not_collinear_QPA₂
Proof 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]
Proof state after:
no goals
Theorem: Imo2019P2.Imo2019q2Cfg.Q₁_ne_A₂
Proof 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.Q₁ ≠ cfg.A₂
Tactic:
intro h
Proof 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
h : cfg.Q₁ = cfg.A₂
⊢ False
Theorem: Imo2019P2.Imo2019q2Cfg.Q₁_ne_A₂
Proof 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
h : cfg.Q₁ = cfg.A₂
⊢ False
Tactic:
have h₁ := cfg.sbtw_Q_A₁_Q₁
Proof 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
h : cfg.Q₁ = cfg.A₂
h₁ : Sbtw ℝ cfg.Q cfg.A₁ cfg.Q₁
⊢ False
Theorem: Imo2019P2.Imo2019q2Cfg.Q₁_ne_A₂
Proof 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
h : cfg.Q₁ = cfg.A₂
h₁ : Sbtw ℝ cfg.Q cfg.A₁ cfg.Q₁
⊢ False
Tactic:
rw [h] at h₁
Proof 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
h : cfg.Q₁ = cfg.A₂
h₁ : Sbtw ℝ cfg.Q cfg.A₁ cfg.A₂
⊢ False
Theorem: Imo2019P2.Imo2019q2Cfg.Q₁_ne_A₂
Proof 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
h : cfg.Q₁ = cfg.A₂
h₁ : Sbtw ℝ cfg.Q cfg.A₁ cfg.A₂
⊢ False
Tactic:
refine cfg.not_collinear_QPA₂ ?_
Proof 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
h : cfg.Q₁ = cfg.A₂
h₁ : Sbtw ℝ cfg.Q cfg.A₁ cfg.A₂
⊢ Collinear ℝ {cfg.Q, cfg.P, cfg.A₂}
Theorem: Imo2019P2.Imo2019q2Cfg.Q₁_ne_A₂
Proof 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
h : cfg.Q₁ = cfg.A₂
h₁ : Sbtw ℝ cfg.Q cfg.A₁ cfg.A₂
⊢ Collinear ℝ {cfg.Q, cfg.P, cfg.A₂}
Tactic:
have hA₂ := cfg.sbtw_A_A₁_A₂.right_mem_affineSpan
Proof 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
h : cfg.Q₁ = cfg.A₂
h₁ : Sbtw ℝ cfg.Q cfg.A₁ cfg.A₂
hA₂ : cfg.A₂ ∈ affineSpan ℝ {cfg.A, cfg.A₁}
⊢ Collinear ℝ {cfg.Q, cfg.P, cfg.A₂}
Theorem: Imo2019P2.Imo2019q2Cfg.Q₁_ne_A₂
Proof 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
h : cfg.Q₁ = cfg.A₂
h₁ : Sbtw ℝ cfg.Q cfg.A₁ cfg.A₂
hA₂ : cfg.A₂ ∈ affineSpan ℝ {cfg.A, cfg.A₁}
⊢ Collinear ℝ {cfg.Q, cfg.P, cfg.A₂}
Tactic:
have hA₂A₁ : line[ℝ, cfg.A₂, cfg.A₁] ≤ line[ℝ, cfg.A, cfg.A₁] :=
  affineSpan_pair_le_of_left_mem hA₂
Proof 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
h : cfg.Q₁ = cfg.A₂
h₁ : Sbtw ℝ cfg.Q cfg.A₁ cfg.A₂
hA₂ : cfg.A₂ ∈ affineSpan ℝ {cfg.A, cfg.A₁}
hA₂A₁ : affineSpan ℝ {cfg.A₂, cfg.A₁} ≤ affineSpan ℝ {cfg.A, cfg.A₁}
⊢ Collinear ℝ {cfg.Q, cfg.P, cfg.A₂}
Theorem: Imo2019P2.Imo2019q2Cfg.Q₁_ne_A₂
Proof 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
h : cfg.Q₁ = cfg.A₂
h₁ : Sbtw ℝ cfg.Q cfg.A₁ cfg.A₂
hA₂ : cfg.A₂ ∈ affineSpan ℝ {cfg.A, cfg.A₁}
hA₂A₁ : affineSpan ℝ {cfg.A₂, cfg.A₁} ≤ affineSpan ℝ {cfg.A, cfg.A₁}
⊢ Collinear ℝ {cfg.Q, cfg.P, cfg.A₂}
Tactic:
have hQ : cfg.Q ∈ line[ℝ, cfg.A, cfg.A₁] := by
  rw [AffineSubspace.le_def'] at hA₂A₁
  exact hA₂A₁ _ h₁.left_mem_affineSpan
Proof 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
h : cfg.Q₁ = cfg.A₂
h₁ : Sbtw ℝ cfg.Q cfg.A₁ cfg.A₂
hA₂ : cfg.A₂ ∈ affineSpan ℝ {cfg.A, cfg.A₁}
hA₂A₁ : affineSpan ℝ {cfg.A₂, cfg.A₁} ≤ affineSpan ℝ {cfg.A, cfg.A₁}
hQ : cfg.Q ∈ affineSpan ℝ {cfg.A, cfg.A₁}
⊢ Collinear ℝ {cfg.Q, cfg.P, cfg.A₂}
Theorem: Imo2019P2.Imo2019q2Cfg.Q₁_ne_A₂
Proof 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
h : cfg.Q₁ = cfg.A₂
h₁ : Sbtw ℝ cfg.Q cfg.A₁ cfg.A₂
hA₂ : cfg.A₂ ∈ affineSpan ℝ {cfg.A, cfg.A₁}
hA₂A₁ : affineSpan ℝ {cfg.A₂, cfg.A₁} ≤ affineSpan ℝ {cfg.A, cfg.A₁}
hQ : cfg.Q ∈ affineSpan ℝ {cfg.A, cfg.A₁}
⊢ Collinear ℝ {cfg.Q, cfg.P, cfg.A₂}
Tactic:
exact collinear_triple_of_mem_affineSpan_pair hQ cfg.wbtw_A_P_A₁.mem_affineSpan hA₂
Proof state after:
no goals
Theorem: Imo2019P2.Imo2019q2Cfg.Q₁_ne_A₂
Proof 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
h : cfg.Q₁ = cfg.A₂
h₁ : Sbtw ℝ cfg.Q cfg.A₁ cfg.A₂
hA₂ : cfg.A₂ ∈ affineSpan ℝ {cfg.A, cfg.A₁}
hA₂A₁ : affineSpan ℝ {cfg.A₂, cfg.A₁} ≤ affineSpan ℝ {cfg.A, cfg.A₁}
⊢ cfg.Q ∈ affineSpan ℝ {cfg.A, cfg.A₁}
Tactic:
rw [AffineSubspace.le_def'] at hA₂A₁
Proof 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
h : cfg.Q₁ = cfg.A₂
h₁ : Sbtw ℝ cfg.Q cfg.A₁ cfg.A₂
hA₂ : cfg.A₂ ∈ affineSpan ℝ {cfg.A, cfg.A₁}
hA₂A₁ : ∀ p ∈ affineSpan ℝ {cfg.A₂, cfg.A₁}, p ∈ affineSpan ℝ {cfg.A, cfg.A₁}
⊢ cfg.Q ∈ affineSpan ℝ {cfg.A, cfg.A₁}
Theorem: Imo2019P2.Imo2019q2Cfg.Q₁_ne_A₂
Proof 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
h : cfg.Q₁ = cfg.A₂
h₁ : Sbtw ℝ cfg.Q cfg.A₁ cfg.A₂
hA₂ : cfg.A₂ ∈ affineSpan ℝ {cfg.A, cfg.A₁}
hA₂A₁ : ∀ p ∈ affineSpan ℝ {cfg.A₂, cfg.A₁}, p ∈ affineSpan ℝ {cfg.A, cfg.A₁}
⊢ cfg.Q ∈ affineSpan ℝ {cfg.A, cfg.A₁}
Tactic:
exact hA₂A₁ _ h₁.left_mem_affineSpan
Proof state after:
no goals
Theorem: Imo2019P2.Imo2019q2Cfg.affineIndependent_PQB₂
Proof 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
⊢ AffineIndependent ℝ ![cfg.P, cfg.Q, cfg.B₂]
Tactic:
rw [← symm_A₂]
Proof 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
⊢ AffineIndependent ℝ ![cfg.P, cfg.Q, cfg.symm.A₂]
Theorem: Imo2019P2.Imo2019q2Cfg.affineIndependent_PQB₂
Proof 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
⊢ AffineIndependent ℝ ![cfg.P, cfg.Q, cfg.symm.A₂]
Tactic:
exact cfg.symm.affineIndependent_QPA₂
Proof state after:
no goals
Theorem: Imo2019P2.Imo2019q2Cfg.symm_triangleQPA₂
Proof 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.triangleQPA₂ = cfg.trianglePQB₂
Tactic:
simp_rw [trianglePQB₂, ← symm_A₂]
Proof 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.symm.triangleQPA₂ = { points := ![cfg.P, cfg.Q, cfg.symm.A₂], independent := ⋯ }
Theorem: Imo2019P2.Imo2019q2Cfg.symm_triangleQPA₂
Proof 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.triangleQPA₂ = { points := ![cfg.P, cfg.Q, cfg.symm.A₂], independent := ⋯ }
Tactic:
ext i
Proof state after:
case h
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
i : Fin (2 + 1)
⊢ cfg.symm.triangleQPA₂.points i = { points := ![cfg.P, cfg.Q, cfg.symm.A₂], independent := ⋯ }.points i
Theorem: Imo2019P2.Imo2019q2Cfg.symm_triangleQPA₂
Proof state before:
case h
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
i : Fin (2 + 1)
⊢ cfg.symm.triangleQPA₂.points i = { points := ![cfg.P, cfg.Q, cfg.symm.A₂], independent := ⋯ }.points i
Tactic:
fin_cases i <;> rfl
Proof state after:
no goals
Theorem: Imo2019P2.Imo2019q2Cfg.two_zsmul_oangle_QPA₂_eq_two_zsmul_oangle_QB₂A₂
Proof 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
inst✝ : Module.Oriented ℝ V (Fin 2)
⊢ 2 • ∡ cfg.B cfg.B₂ cfg.A₂ = 2 • ∡ cfg.Q cfg.B₂ cfg.A₂
Tactic:
rw [cfg.wbtw_B_Q_B₂.symm.oangle_eq_left cfg.B₂_ne_Q.symm]
Proof state after:
no goals
Theorem: Imo2019P2.Imo2019q2Cfg.symm_ω_eq_trianglePQB₂_circumsphere
Proof 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.ω = circumsphere cfg.trianglePQB₂
Tactic:
rw [ω, symm_triangleQPA₂]
Proof state after:
no goals
Theorem: Imo2019P2.Imo2019q2Cfg.symm_ω
Proof 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, ω]
Proof 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₂
Theorem: Imo2019P2.Imo2019q2Cfg.symm_ω
Proof 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₂ ?_ ?_
Proof 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₂}
Theorem: Imo2019P2.Imo2019q2Cfg.symm_ω
Proof 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]
Proof 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₂}
Theorem: Imo2019P2.Imo2019q2Cfg.symm_ω
Proof 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]
Proof 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₂}
Theorem: Imo2019P2.Imo2019q2Cfg.symm_ω
Proof 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 ?_)
Proof 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₂}
Theorem: Imo2019P2.Imo2019q2Cfg.symm_ω
Proof 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
Proof state after:
no goals
Theorem: Imo2019P2.Imo2019q2Cfg.symm_ω
Proof 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]
Proof 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₂}
Theorem: Imo2019P2.Imo2019q2Cfg.symm_ω
Proof 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 ?_)
Proof 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₂}
Theorem: Imo2019P2.Imo2019q2Cfg.symm_ω
Proof 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
Proof state after:
no goals
Theorem: Imo2019P2.Imo2019q2Cfg.two_zsmul_oangle_CA₂A₁_eq_two_zsmul_oangle_CBA
Proof 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
inst✝ : Module.Oriented ℝ V (Fin 2)
⊢ 2 • ∡ cfg.C cfg.A₂ cfg.A₁ = 2 • ∡ cfg.C cfg.A₂ cfg.A
Tactic:
rw [cfg.sbtw_A_A₁_A₂.symm.oangle_eq_right]
Proof state after:
no goals
Theorem: Imo2019P2.Imo2019q2Cfg.two_zsmul_oangle_CA₂A₁_eq_two_zsmul_oangle_CQ₁A₁
Proof 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
inst✝ : Module.Oriented ℝ V (Fin 2)
⊢ 2 • ∡ cfg.C cfg.B cfg.A = 2 • ∡ cfg.C cfg.Q₁ cfg.Q
Tactic:
rw [oangle_CQ₁Q_eq_oangle_CBA]
Proof state after:
no goals
Theorem: Imo2019P2.Imo2019q2Cfg.two_zsmul_oangle_CA₂A₁_eq_two_zsmul_oangle_CQ₁A₁
Proof 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
inst✝ : Module.Oriented ℝ V (Fin 2)
⊢ 2 • ∡ cfg.C cfg.Q₁ cfg.Q = 2 • ∡ cfg.C cfg.Q₁ cfg.A₁
Tactic:
rw [cfg.sbtw_Q_A₁_Q₁.symm.oangle_eq_right]
Proof state after:
no goals
Theorem: Imo2019P2.Imo2019q2Cfg.not_collinear_CA₂A₁
Proof 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.C, cfg.A₂, cfg.A₁}
Tactic:
haveI := someOrientation V
Proof 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.C, cfg.A₂, cfg.A₁}
Theorem: Imo2019P2.Imo2019q2Cfg.not_collinear_CA₂A₁
Proof 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.C, cfg.A₂, cfg.A₁}
Tactic:
rw [collinear_iff_of_two_zsmul_oangle_eq cfg.two_zsmul_oangle_CA₂A₁_eq_two_zsmul_oangle_CBA,
  Set.pair_comm, Set.insert_comm, Set.pair_comm]
Proof 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.A, cfg.B, cfg.C}
Theorem: Imo2019P2.Imo2019q2Cfg.not_collinear_CA₂A₁
Proof 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.A, cfg.B, cfg.C}
Tactic:
exact cfg.not_collinear_ABC
Proof state after:
no goals