Theorem: Imo2019P2.Imo2019q2Cfg.A₁_ne_B (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.A₁ ≠ cfg.B
Tactic:
intro h
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
⊢ False

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
⊢ False
Tactic:
have hwbtw := cfg.wbtw_A_P_A₁
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.A₁
⊢ False

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.A₁
⊢ False
Tactic:
rw [h] at hwbtw
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
⊢ False

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
⊢ False
Tactic:
have hPQ : line[ℝ, cfg.P, cfg.Q] = line[ℝ, cfg.A, cfg.B] := by
  rw [AffineSubspace.eq_iff_direction_eq_of_mem (left_mem_affineSpan_pair _ _ _)
    hwbtw.mem_affineSpan]
  exact cfg.PQ_parallel_AB.direction_eq
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}
⊢ False

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}
⊢ False
Tactic:
haveI := someOrientation V
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)
⊢ False

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)
⊢ False
Tactic:
have haQ : (2 : ℤ) • ∡ cfg.C cfg.B cfg.Q = (2 : ℤ) • ∡ cfg.C cfg.B cfg.A := by
  rw [Collinear.two_zsmul_oangle_eq_right _ cfg.A_ne_B cfg.Q_ne_B]
  rw [Set.pair_comm, Set.insert_comm]
  refine collinear_insert_of_mem_affineSpan_pair ?_
  rw [← hPQ]
  exact right_mem_affineSpan_pair _ _ _
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
⊢ False

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]
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

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
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

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
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

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
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

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
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

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
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

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
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

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 ?_
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}

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]
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₁}

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
State after:
no goals

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]
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

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
State after:
no goals

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]
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}

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]
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}

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 ?_
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}

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]
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}

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 _ _ _
State after:
no goals

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]
State after:
no goals

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]
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}

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
State after:
no goals

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]
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₁

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
State after:
no goals