internlm/Lean-Github huggingface dataset:
Theorem: Imo2019P2.Imo2019q2Cfg.A₁_ne_B
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.A₁ = cfg.B
hwbtw : Wbtw ℝ cfg.A cfg.P cfg.B
hPQ : affineSpan ℝ {cfg.P, cfg.Q} = affineSpan ℝ {cfg.A, cfg.B}
this : Module.Oriented ℝ V (Fin 2)
haQ : 2 • ∡ cfg.C cfg.B cfg.Q = 2 • ∡ cfg.C cfg.B cfg.A
⊢ False
Tactic:
have ha : (2 : ℤ) • ∡ cfg.C cfg.B cfg.Q = (2 : ℤ) • ∡ cfg.C cfg.Q₁ cfg.Q := by
  rw [oangle_CQ₁Q_eq_oangle_CBA, haQ]
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.A₁ = cfg.B
hwbtw : Wbtw ℝ cfg.A cfg.P cfg.B
hPQ : affineSpan ℝ {cfg.P, cfg.Q} = affineSpan ℝ {cfg.A, cfg.B}
this : Module.Oriented ℝ V (Fin 2)
haQ : 2 • ∡ cfg.C cfg.B cfg.Q = 2 • ∡ cfg.C cfg.B cfg.A
ha : 2 • ∡ cfg.C cfg.B cfg.Q = 2 • ∡ cfg.C cfg.Q₁ cfg.Q
⊢ False
Theorem: Imo2019P2.Imo2019q2Cfg.A₁_ne_B
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.A₁ = cfg.B
hwbtw : Wbtw ℝ cfg.A cfg.P cfg.B
hPQ : affineSpan ℝ {cfg.P, cfg.Q} = affineSpan ℝ {cfg.A, cfg.B}
this : Module.Oriented ℝ V (Fin 2)
haQ : 2 • ∡ cfg.C cfg.B cfg.Q = 2 • ∡ cfg.C cfg.B cfg.A
ha : 2 • ∡ cfg.C cfg.B cfg.Q = 2 • ∡ cfg.C cfg.Q₁ cfg.Q
⊢ False
Tactic:
have hn : ¬Collinear ℝ ({cfg.C, cfg.B, cfg.Q} : Set Pt) := by
  rw [collinear_iff_of_two_zsmul_oangle_eq haQ, Set.pair_comm, Set.insert_comm, Set.pair_comm]
  exact cfg.not_collinear_ABC
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.A₁ = cfg.B
hwbtw : Wbtw ℝ cfg.A cfg.P cfg.B
hPQ : affineSpan ℝ {cfg.P, cfg.Q} = affineSpan ℝ {cfg.A, cfg.B}
this : Module.Oriented ℝ V (Fin 2)
haQ : 2 • ∡ cfg.C cfg.B cfg.Q = 2 • ∡ cfg.C cfg.B cfg.A
ha : 2 • ∡ cfg.C cfg.B cfg.Q = 2 • ∡ cfg.C cfg.Q₁ cfg.Q
hn : ¬Collinear ℝ {cfg.C, cfg.B, cfg.Q}
⊢ False
Theorem: Imo2019P2.Imo2019q2Cfg.A₁_ne_B
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.A₁ = cfg.B
hwbtw : Wbtw ℝ cfg.A cfg.P cfg.B
hPQ : affineSpan ℝ {cfg.P, cfg.Q} = affineSpan ℝ {cfg.A, cfg.B}
this : Module.Oriented ℝ V (Fin 2)
haQ : 2 • ∡ cfg.C cfg.B cfg.Q = 2 • ∡ cfg.C cfg.B cfg.A
ha : 2 • ∡ cfg.C cfg.B cfg.Q = 2 • ∡ cfg.C cfg.Q₁ cfg.Q
hn : ¬Collinear ℝ {cfg.C, cfg.B, cfg.Q}
⊢ False
Tactic:
have hc := cospherical_of_two_zsmul_oangle_eq_of_not_collinear ha hn
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.A₁ = cfg.B
hwbtw : Wbtw ℝ cfg.A cfg.P cfg.B
hPQ : affineSpan ℝ {cfg.P, cfg.Q} = affineSpan ℝ {cfg.A, cfg.B}
this : Module.Oriented ℝ V (Fin 2)
haQ : 2 • ∡ cfg.C cfg.B cfg.Q = 2 • ∡ cfg.C cfg.B cfg.A
ha : 2 • ∡ cfg.C cfg.B cfg.Q = 2 • ∡ cfg.C cfg.Q₁ cfg.Q
hn : ¬Collinear ℝ {cfg.C, cfg.B, cfg.Q}
hc : Cospherical {cfg.C, cfg.B, cfg.Q₁, cfg.Q}
⊢ False
Theorem: Imo2019P2.Imo2019q2Cfg.A₁_ne_B
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.A₁ = cfg.B
hwbtw : Wbtw ℝ cfg.A cfg.P cfg.B
hPQ : affineSpan ℝ {cfg.P, cfg.Q} = affineSpan ℝ {cfg.A, cfg.B}
this : Module.Oriented ℝ V (Fin 2)
haQ : 2 • ∡ cfg.C cfg.B cfg.Q = 2 • ∡ cfg.C cfg.B cfg.A
ha : 2 • ∡ cfg.C cfg.B cfg.Q = 2 • ∡ cfg.C cfg.Q₁ cfg.Q
hn : ¬Collinear ℝ {cfg.C, cfg.B, cfg.Q}
hc : Cospherical {cfg.C, cfg.B, cfg.Q₁, cfg.Q}
⊢ False
Tactic:
have hBQ₁ : cfg.B ≠ cfg.Q₁ := by rw [← h]; exact cfg.sbtw_Q_A₁_Q₁.ne_right
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.A₁ = cfg.B
hwbtw : Wbtw ℝ cfg.A cfg.P cfg.B
hPQ : affineSpan ℝ {cfg.P, cfg.Q} = affineSpan ℝ {cfg.A, cfg.B}
this : Module.Oriented ℝ V (Fin 2)
haQ : 2 • ∡ cfg.C cfg.B cfg.Q = 2 • ∡ cfg.C cfg.B cfg.A
ha : 2 • ∡ cfg.C cfg.B cfg.Q = 2 • ∡ cfg.C cfg.Q₁ cfg.Q
hn : ¬Collinear ℝ {cfg.C, cfg.B, cfg.Q}
hc : Cospherical {cfg.C, cfg.B, cfg.Q₁, cfg.Q}
hBQ₁ : cfg.B ≠ cfg.Q₁
⊢ False
Theorem: Imo2019P2.Imo2019q2Cfg.A₁_ne_B
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.A₁ = cfg.B
hwbtw : Wbtw ℝ cfg.A cfg.P cfg.B
hPQ : affineSpan ℝ {cfg.P, cfg.Q} = affineSpan ℝ {cfg.A, cfg.B}
this : Module.Oriented ℝ V (Fin 2)
haQ : 2 • ∡ cfg.C cfg.B cfg.Q = 2 • ∡ cfg.C cfg.B cfg.A
ha : 2 • ∡ cfg.C cfg.B cfg.Q = 2 • ∡ cfg.C cfg.Q₁ cfg.Q
hn : ¬Collinear ℝ {cfg.C, cfg.B, cfg.Q}
hc : Cospherical {cfg.C, cfg.B, cfg.Q₁, cfg.Q}
hBQ₁ : cfg.B ≠ cfg.Q₁
⊢ False
Tactic:
have hQQ₁ : cfg.Q ≠ cfg.Q₁ := cfg.sbtw_Q_A₁_Q₁.left_ne_right
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.A₁ = cfg.B
hwbtw : Wbtw ℝ cfg.A cfg.P cfg.B
hPQ : affineSpan ℝ {cfg.P, cfg.Q} = affineSpan ℝ {cfg.A, cfg.B}
this : Module.Oriented ℝ V (Fin 2)
haQ : 2 • ∡ cfg.C cfg.B cfg.Q = 2 • ∡ cfg.C cfg.B cfg.A
ha : 2 • ∡ cfg.C cfg.B cfg.Q = 2 • ∡ cfg.C cfg.Q₁ cfg.Q
hn : ¬Collinear ℝ {cfg.C, cfg.B, cfg.Q}
hc : Cospherical {cfg.C, cfg.B, cfg.Q₁, cfg.Q}
hBQ₁ : cfg.B ≠ cfg.Q₁
hQQ₁ : cfg.Q ≠ cfg.Q₁
⊢ False
Theorem: Imo2019P2.Imo2019q2Cfg.A₁_ne_B
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.A₁ = cfg.B
hwbtw : Wbtw ℝ cfg.A cfg.P cfg.B
hPQ : affineSpan ℝ {cfg.P, cfg.Q} = affineSpan ℝ {cfg.A, cfg.B}
this : Module.Oriented ℝ V (Fin 2)
haQ : 2 • ∡ cfg.C cfg.B cfg.Q = 2 • ∡ cfg.C cfg.B cfg.A
ha : 2 • ∡ cfg.C cfg.B cfg.Q = 2 • ∡ cfg.C cfg.Q₁ cfg.Q
hn : ¬Collinear ℝ {cfg.C, cfg.B, cfg.Q}
hc : Cospherical {cfg.C, cfg.B, cfg.Q₁, cfg.Q}
hBQ₁ : cfg.B ≠ cfg.Q₁
hQQ₁ : cfg.Q ≠ cfg.Q₁
⊢ False
Tactic:
have hBQ₁Q : AffineIndependent ℝ ![cfg.B, cfg.Q₁, cfg.Q] :=
  hc.affineIndependent_of_mem_of_ne (Set.mem_insert_of_mem _ (Set.mem_insert _ _))
    (Set.mem_insert_of_mem _ (Set.mem_insert_of_mem _ (Set.mem_insert _ _)))
    (Set.mem_insert_of_mem _
      (Set.mem_insert_of_mem _ (Set.mem_insert_of_mem _ (Set.mem_singleton _))))
    hBQ₁ cfg.Q_ne_B.symm hQQ₁.symm
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.A₁ = cfg.B
hwbtw : Wbtw ℝ cfg.A cfg.P cfg.B
hPQ : affineSpan ℝ {cfg.P, cfg.Q} = affineSpan ℝ {cfg.A, cfg.B}
this : Module.Oriented ℝ V (Fin 2)
haQ : 2 • ∡ cfg.C cfg.B cfg.Q = 2 • ∡ cfg.C cfg.B cfg.A
ha : 2 • ∡ cfg.C cfg.B cfg.Q = 2 • ∡ cfg.C cfg.Q₁ cfg.Q
hn : ¬Collinear ℝ {cfg.C, cfg.B, cfg.Q}
hc : Cospherical {cfg.C, cfg.B, cfg.Q₁, cfg.Q}
hBQ₁ : cfg.B ≠ cfg.Q₁
hQQ₁ : cfg.Q ≠ cfg.Q₁
hBQ₁Q : AffineIndependent ℝ ![cfg.B, cfg.Q₁, cfg.Q]
⊢ False
Theorem: Imo2019P2.Imo2019q2Cfg.A₁_ne_B
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.A₁ = cfg.B
hwbtw : Wbtw ℝ cfg.A cfg.P cfg.B
hPQ : affineSpan ℝ {cfg.P, cfg.Q} = affineSpan ℝ {cfg.A, cfg.B}
this : Module.Oriented ℝ V (Fin 2)
haQ : 2 • ∡ cfg.C cfg.B cfg.Q = 2 • ∡ cfg.C cfg.B cfg.A
ha : 2 • ∡ cfg.C cfg.B cfg.Q = 2 • ∡ cfg.C cfg.Q₁ cfg.Q
hn : ¬Collinear ℝ {cfg.C, cfg.B, cfg.Q}
hc : Cospherical {cfg.C, cfg.B, cfg.Q₁, cfg.Q}
hBQ₁ : cfg.B ≠ cfg.Q₁
hQQ₁ : cfg.Q ≠ cfg.Q₁
hBQ₁Q : AffineIndependent ℝ ![cfg.B, cfg.Q₁, cfg.Q]
⊢ False
Tactic:
rw [affineIndependent_iff_not_collinear_set] at hBQ₁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.A₁ = cfg.B
hwbtw : Wbtw ℝ cfg.A cfg.P cfg.B
hPQ : affineSpan ℝ {cfg.P, cfg.Q} = affineSpan ℝ {cfg.A, cfg.B}
this : Module.Oriented ℝ V (Fin 2)
haQ : 2 • ∡ cfg.C cfg.B cfg.Q = 2 • ∡ cfg.C cfg.B cfg.A
ha : 2 • ∡ cfg.C cfg.B cfg.Q = 2 • ∡ cfg.C cfg.Q₁ cfg.Q
hn : ¬Collinear ℝ {cfg.C, cfg.B, cfg.Q}
hc : Cospherical {cfg.C, cfg.B, cfg.Q₁, cfg.Q}
hBQ₁ : cfg.B ≠ cfg.Q₁
hQQ₁ : cfg.Q ≠ cfg.Q₁
hBQ₁Q : ¬Collinear ℝ {cfg.B, cfg.Q₁, cfg.Q}
⊢ False
Theorem: Imo2019P2.Imo2019q2Cfg.A₁_ne_B
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.A₁ = cfg.B
hwbtw : Wbtw ℝ cfg.A cfg.P cfg.B
hPQ : affineSpan ℝ {cfg.P, cfg.Q} = affineSpan ℝ {cfg.A, cfg.B}
this : Module.Oriented ℝ V (Fin 2)
haQ : 2 • ∡ cfg.C cfg.B cfg.Q = 2 • ∡ cfg.C cfg.B cfg.A
ha : 2 • ∡ cfg.C cfg.B cfg.Q = 2 • ∡ cfg.C cfg.Q₁ cfg.Q
hn : ¬Collinear ℝ {cfg.C, cfg.B, cfg.Q}
hc : Cospherical {cfg.C, cfg.B, cfg.Q₁, cfg.Q}
hBQ₁ : cfg.B ≠ cfg.Q₁
hQQ₁ : cfg.Q ≠ cfg.Q₁
hBQ₁Q : ¬Collinear ℝ {cfg.B, cfg.Q₁, cfg.Q}
⊢ False
Tactic:
refine hBQ₁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.A₁ = cfg.B
hwbtw : Wbtw ℝ cfg.A cfg.P cfg.B
hPQ : affineSpan ℝ {cfg.P, cfg.Q} = affineSpan ℝ {cfg.A, cfg.B}
this : Module.Oriented ℝ V (Fin 2)
haQ : 2 • ∡ cfg.C cfg.B cfg.Q = 2 • ∡ cfg.C cfg.B cfg.A
ha : 2 • ∡ cfg.C cfg.B cfg.Q = 2 • ∡ cfg.C cfg.Q₁ cfg.Q
hn : ¬Collinear ℝ {cfg.C, cfg.B, cfg.Q}
hc : Cospherical {cfg.C, cfg.B, cfg.Q₁, cfg.Q}
hBQ₁ : cfg.B ≠ cfg.Q₁
hQQ₁ : cfg.Q ≠ cfg.Q₁
hBQ₁Q : ¬Collinear ℝ {cfg.B, cfg.Q₁, cfg.Q}
⊢ Collinear ℝ {cfg.B, cfg.Q₁, cfg.Q}
Theorem: Imo2019P2.Imo2019q2Cfg.A₁_ne_B
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.A₁ = cfg.B
hwbtw : Wbtw ℝ cfg.A cfg.P cfg.B
hPQ : affineSpan ℝ {cfg.P, cfg.Q} = affineSpan ℝ {cfg.A, cfg.B}
this : Module.Oriented ℝ V (Fin 2)
haQ : 2 • ∡ cfg.C cfg.B cfg.Q = 2 • ∡ cfg.C cfg.B cfg.A
ha : 2 • ∡ cfg.C cfg.B cfg.Q = 2 • ∡ cfg.C cfg.Q₁ cfg.Q
hn : ¬Collinear ℝ {cfg.C, cfg.B, cfg.Q}
hc : Cospherical {cfg.C, cfg.B, cfg.Q₁, cfg.Q}
hBQ₁ : cfg.B ≠ cfg.Q₁
hQQ₁ : cfg.Q ≠ cfg.Q₁
hBQ₁Q : ¬Collinear ℝ {cfg.B, cfg.Q₁, cfg.Q}
⊢ Collinear ℝ {cfg.B, cfg.Q₁, cfg.Q}
Tactic:
rw [← h, Set.pair_comm, Set.insert_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
h : cfg.A₁ = cfg.B
hwbtw : Wbtw ℝ cfg.A cfg.P cfg.B
hPQ : affineSpan ℝ {cfg.P, cfg.Q} = affineSpan ℝ {cfg.A, cfg.B}
this : Module.Oriented ℝ V (Fin 2)
haQ : 2 • ∡ cfg.C cfg.B cfg.Q = 2 • ∡ cfg.C cfg.B cfg.A
ha : 2 • ∡ cfg.C cfg.B cfg.Q = 2 • ∡ cfg.C cfg.Q₁ cfg.Q
hn : ¬Collinear ℝ {cfg.C, cfg.B, cfg.Q}
hc : Cospherical {cfg.C, cfg.B, cfg.Q₁, cfg.Q}
hBQ₁ : cfg.B ≠ cfg.Q₁
hQQ₁ : cfg.Q ≠ cfg.Q₁
hBQ₁Q : ¬Collinear ℝ {cfg.B, cfg.Q₁, cfg.Q}
⊢ Collinear ℝ {cfg.Q, cfg.A₁, cfg.Q₁}
Theorem: Imo2019P2.Imo2019q2Cfg.A₁_ne_B
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.A₁ = cfg.B
hwbtw : Wbtw ℝ cfg.A cfg.P cfg.B
hPQ : affineSpan ℝ {cfg.P, cfg.Q} = affineSpan ℝ {cfg.A, cfg.B}
this : Module.Oriented ℝ V (Fin 2)
haQ : 2 • ∡ cfg.C cfg.B cfg.Q = 2 • ∡ cfg.C cfg.B cfg.A
ha : 2 • ∡ cfg.C cfg.B cfg.Q = 2 • ∡ cfg.C cfg.Q₁ cfg.Q
hn : ¬Collinear ℝ {cfg.C, cfg.B, cfg.Q}
hc : Cospherical {cfg.C, cfg.B, cfg.Q₁, cfg.Q}
hBQ₁ : cfg.B ≠ cfg.Q₁
hQQ₁ : cfg.Q ≠ cfg.Q₁
hBQ₁Q : ¬Collinear ℝ {cfg.B, cfg.Q₁, cfg.Q}
⊢ Collinear ℝ {cfg.Q, cfg.A₁, cfg.Q₁}
Tactic:
exact cfg.sbtw_Q_A₁_Q₁.wbtw.collinear
Proof state after:
no goals
Theorem: Imo2019P2.Imo2019q2Cfg.A₁_ne_B
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.A₁ = cfg.B
hwbtw : Wbtw ℝ cfg.A cfg.P cfg.B
⊢ affineSpan ℝ {cfg.P, cfg.Q} = affineSpan ℝ {cfg.A, cfg.B}
Tactic:
rw [AffineSubspace.eq_iff_direction_eq_of_mem (left_mem_affineSpan_pair _ _ _)
  hwbtw.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.A₁ = cfg.B
hwbtw : Wbtw ℝ cfg.A cfg.P cfg.B
⊢ (affineSpan ℝ {cfg.P, cfg.Q}).direction = (affineSpan ℝ {cfg.A, cfg.B}).direction
Theorem: Imo2019P2.Imo2019q2Cfg.A₁_ne_B
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.A₁ = cfg.B
hwbtw : Wbtw ℝ cfg.A cfg.P cfg.B
⊢ (affineSpan ℝ {cfg.P, cfg.Q}).direction = (affineSpan ℝ {cfg.A, cfg.B}).direction
Tactic:
exact cfg.PQ_parallel_AB.direction_eq
Proof state after:
no goals
Theorem: Imo2019P2.Imo2019q2Cfg.A₁_ne_B
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.A₁ = cfg.B
hwbtw : Wbtw ℝ cfg.A cfg.P cfg.B
hPQ : affineSpan ℝ {cfg.P, cfg.Q} = affineSpan ℝ {cfg.A, cfg.B}
this : Module.Oriented ℝ V (Fin 2)
⊢ 2 • ∡ cfg.C cfg.B cfg.Q = 2 • ∡ cfg.C cfg.B cfg.A
Tactic:
rw [Collinear.two_zsmul_oangle_eq_right _ cfg.A_ne_B cfg.Q_ne_B]
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.A₁ = cfg.B
hwbtw : Wbtw ℝ cfg.A cfg.P cfg.B
hPQ : affineSpan ℝ {cfg.P, cfg.Q} = affineSpan ℝ {cfg.A, cfg.B}
this : Module.Oriented ℝ V (Fin 2)
⊢ Collinear ℝ {cfg.A, cfg.B, cfg.Q}
Theorem: Imo2019P2.Imo2019q2Cfg.A₁_ne_B
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.A₁ = cfg.B
hwbtw : Wbtw ℝ cfg.A cfg.P cfg.B
hPQ : affineSpan ℝ {cfg.P, cfg.Q} = affineSpan ℝ {cfg.A, cfg.B}
this : Module.Oriented ℝ V (Fin 2)
⊢ Collinear ℝ {cfg.A, cfg.B, cfg.Q}
Tactic:
rw [Set.pair_comm, Set.insert_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
h : cfg.A₁ = cfg.B
hwbtw : Wbtw ℝ cfg.A cfg.P cfg.B
hPQ : affineSpan ℝ {cfg.P, cfg.Q} = affineSpan ℝ {cfg.A, cfg.B}
this : Module.Oriented ℝ V (Fin 2)
⊢ Collinear ℝ {cfg.Q, cfg.A, cfg.B}
Theorem: Imo2019P2.Imo2019q2Cfg.A₁_ne_B
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.A₁ = cfg.B
hwbtw : Wbtw ℝ cfg.A cfg.P cfg.B
hPQ : affineSpan ℝ {cfg.P, cfg.Q} = affineSpan ℝ {cfg.A, cfg.B}
this : Module.Oriented ℝ V (Fin 2)
⊢ Collinear ℝ {cfg.Q, cfg.A, cfg.B}
Tactic:
refine collinear_insert_of_mem_affineSpan_pair ?_
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.A₁ = cfg.B
hwbtw : Wbtw ℝ cfg.A cfg.P cfg.B
hPQ : affineSpan ℝ {cfg.P, cfg.Q} = affineSpan ℝ {cfg.A, cfg.B}
this : Module.Oriented ℝ V (Fin 2)
⊢ cfg.Q ∈ affineSpan ℝ {cfg.A, cfg.B}
Theorem: Imo2019P2.Imo2019q2Cfg.A₁_ne_B
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.A₁ = cfg.B
hwbtw : Wbtw ℝ cfg.A cfg.P cfg.B
hPQ : affineSpan ℝ {cfg.P, cfg.Q} = affineSpan ℝ {cfg.A, cfg.B}
this : Module.Oriented ℝ V (Fin 2)
⊢ cfg.Q ∈ affineSpan ℝ {cfg.A, cfg.B}
Tactic:
rw [← hPQ]
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.A₁ = cfg.B
hwbtw : Wbtw ℝ cfg.A cfg.P cfg.B
hPQ : affineSpan ℝ {cfg.P, cfg.Q} = affineSpan ℝ {cfg.A, cfg.B}
this : Module.Oriented ℝ V (Fin 2)
⊢ cfg.Q ∈ affineSpan ℝ {cfg.P, cfg.Q}
Theorem: Imo2019P2.Imo2019q2Cfg.A₁_ne_B
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.A₁ = cfg.B
hwbtw : Wbtw ℝ cfg.A cfg.P cfg.B
hPQ : affineSpan ℝ {cfg.P, cfg.Q} = affineSpan ℝ {cfg.A, cfg.B}
this : Module.Oriented ℝ V (Fin 2)
⊢ cfg.Q ∈ affineSpan ℝ {cfg.P, cfg.Q}
Tactic:
exact right_mem_affineSpan_pair _ _ _
Proof state after:
no goals
Theorem: Imo2019P2.Imo2019q2Cfg.A₁_ne_B
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.A₁ = cfg.B
hwbtw : Wbtw ℝ cfg.A cfg.P cfg.B
hPQ : affineSpan ℝ {cfg.P, cfg.Q} = affineSpan ℝ {cfg.A, cfg.B}
this : Module.Oriented ℝ V (Fin 2)
haQ : 2 • ∡ cfg.C cfg.B cfg.Q = 2 • ∡ cfg.C cfg.B cfg.A
⊢ 2 • ∡ cfg.C cfg.B cfg.Q = 2 • ∡ cfg.C cfg.Q₁ cfg.Q
Tactic:
rw [oangle_CQ₁Q_eq_oangle_CBA, haQ]
Proof state after:
no goals
Theorem: Imo2019P2.Imo2019q2Cfg.A₁_ne_B
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.A₁ = cfg.B
hwbtw : Wbtw ℝ cfg.A cfg.P cfg.B
hPQ : affineSpan ℝ {cfg.P, cfg.Q} = affineSpan ℝ {cfg.A, cfg.B}
this : Module.Oriented ℝ V (Fin 2)
haQ : 2 • ∡ cfg.C cfg.B cfg.Q = 2 • ∡ cfg.C cfg.B cfg.A
ha : 2 • ∡ cfg.C cfg.B cfg.Q = 2 • ∡ cfg.C cfg.Q₁ cfg.Q
⊢ ¬Collinear ℝ {cfg.C, cfg.B, cfg.Q}
Tactic:
rw [collinear_iff_of_two_zsmul_oangle_eq haQ, 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
h : cfg.A₁ = cfg.B
hwbtw : Wbtw ℝ cfg.A cfg.P cfg.B
hPQ : affineSpan ℝ {cfg.P, cfg.Q} = affineSpan ℝ {cfg.A, cfg.B}
this : Module.Oriented ℝ V (Fin 2)
haQ : 2 • ∡ cfg.C cfg.B cfg.Q = 2 • ∡ cfg.C cfg.B cfg.A
ha : 2 • ∡ cfg.C cfg.B cfg.Q = 2 • ∡ cfg.C cfg.Q₁ cfg.Q
⊢ ¬Collinear ℝ {cfg.A, cfg.B, cfg.C}
Theorem: Imo2019P2.Imo2019q2Cfg.A₁_ne_B
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.A₁ = cfg.B
hwbtw : Wbtw ℝ cfg.A cfg.P cfg.B
hPQ : affineSpan ℝ {cfg.P, cfg.Q} = affineSpan ℝ {cfg.A, cfg.B}
this : Module.Oriented ℝ V (Fin 2)
haQ : 2 • ∡ cfg.C cfg.B cfg.Q = 2 • ∡ cfg.C cfg.B cfg.A
ha : 2 • ∡ cfg.C cfg.B cfg.Q = 2 • ∡ cfg.C cfg.Q₁ cfg.Q
⊢ ¬Collinear ℝ {cfg.A, cfg.B, cfg.C}
Tactic:
exact cfg.not_collinear_ABC
Proof state after:
no goals
Theorem: Imo2019P2.Imo2019q2Cfg.A₁_ne_B
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.A₁ = cfg.B
hwbtw : Wbtw ℝ cfg.A cfg.P cfg.B
hPQ : affineSpan ℝ {cfg.P, cfg.Q} = affineSpan ℝ {cfg.A, cfg.B}
this : Module.Oriented ℝ V (Fin 2)
haQ : 2 • ∡ cfg.C cfg.B cfg.Q = 2 • ∡ cfg.C cfg.B cfg.A
ha : 2 • ∡ cfg.C cfg.B cfg.Q = 2 • ∡ cfg.C cfg.Q₁ cfg.Q
hn : ¬Collinear ℝ {cfg.C, cfg.B, cfg.Q}
hc : Cospherical {cfg.C, cfg.B, cfg.Q₁, cfg.Q}
⊢ cfg.B ≠ cfg.Q₁
Tactic:
rw [← 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.A₁ = cfg.B
hwbtw : Wbtw ℝ cfg.A cfg.P cfg.B
hPQ : affineSpan ℝ {cfg.P, cfg.Q} = affineSpan ℝ {cfg.A, cfg.B}
this : Module.Oriented ℝ V (Fin 2)
haQ : 2 • ∡ cfg.C cfg.B cfg.Q = 2 • ∡ cfg.C cfg.B cfg.A
ha : 2 • ∡ cfg.C cfg.B cfg.Q = 2 • ∡ cfg.C cfg.Q₁ cfg.Q
hn : ¬Collinear ℝ {cfg.C, cfg.B, cfg.Q}
hc : Cospherical {cfg.C, cfg.B, cfg.Q₁, cfg.Q}
⊢ cfg.A₁ ≠ cfg.Q₁
Theorem: Imo2019P2.Imo2019q2Cfg.A₁_ne_B
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.A₁ = cfg.B
hwbtw : Wbtw ℝ cfg.A cfg.P cfg.B
hPQ : affineSpan ℝ {cfg.P, cfg.Q} = affineSpan ℝ {cfg.A, cfg.B}
this : Module.Oriented ℝ V (Fin 2)
haQ : 2 • ∡ cfg.C cfg.B cfg.Q = 2 • ∡ cfg.C cfg.B cfg.A
ha : 2 • ∡ cfg.C cfg.B cfg.Q = 2 • ∡ cfg.C cfg.Q₁ cfg.Q
hn : ¬Collinear ℝ {cfg.C, cfg.B, cfg.Q}
hc : Cospherical {cfg.C, cfg.B, cfg.Q₁, cfg.Q}
⊢ cfg.A₁ ≠ cfg.Q₁
Tactic:
exact cfg.sbtw_Q_A₁_Q₁.ne_right
Proof state after:
no goals
Theorem: Imo2019P2.Imo2019q2Cfg.sbtw_A_A₁_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
⊢ Sbtw ℝ cfg.A cfg.A₁ cfg.A₂
Tactic:
refine Sphere.sbtw_secondInter cfg.A_mem_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
⊢ dist cfg.A₁ (circumsphere cfg.triangleABC).center < (circumsphere cfg.triangleABC).radius
Theorem: Imo2019P2.Imo2019q2Cfg.sbtw_A_A₁_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
⊢ dist cfg.A₁ (circumsphere cfg.triangleABC).center < (circumsphere cfg.triangleABC).radius
Tactic:
convert cfg.sbtw_B_A₁_C.dist_lt_max_dist _
Proof 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)