internlm/Lean-Github huggingface dataset:
Theorem: Imo2019P2.Imo2019q2Cfg.symm_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
⊢ (circumsphere cfg.triangleABC).secondInter cfg.symm.A (cfg.symm.A₁ -ᵥ cfg.symm.A) =
    (circumsphere cfg.triangleABC).secondInter cfg.B (cfg.B₁ -ᵥ cfg.B)
Tactic:
rfl
Proof state after:
no goals
Theorem: Imo2019P2.Imo2019q2Cfg.QP_parallel_BA
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
⊢ affineSpan ℝ {cfg.Q, cfg.P} ∥ affineSpan ℝ {cfg.B, cfg.A}
Tactic:
rw [Set.pair_comm cfg.Q, Set.pair_comm cfg.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
⊢ affineSpan ℝ {cfg.P, cfg.Q} ∥ affineSpan ℝ {cfg.A, cfg.B}
Theorem: Imo2019P2.Imo2019q2Cfg.QP_parallel_BA
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
⊢ affineSpan ℝ {cfg.P, cfg.Q} ∥ affineSpan ℝ {cfg.A, cfg.B}
Tactic:
exact cfg.PQ_parallel_AB
Proof state after:
no goals
Theorem: Imo2019P2.Imo2019q2Cfg.A_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.A ≠ 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.A = cfg.A₁
⊢ False
Theorem: Imo2019P2.Imo2019q2Cfg.A_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.A = cfg.A₁
⊢ False
Tactic:
have h' := 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.A₁
h' : ¬Collinear ℝ {cfg.A, cfg.B, cfg.C}
⊢ False
Theorem: Imo2019P2.Imo2019q2Cfg.A_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.A = cfg.A₁
h' : ¬Collinear ℝ {cfg.A, cfg.B, cfg.C}
⊢ False
Tactic:
rw [h, Set.insert_comm] 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.A = cfg.A₁
h' : ¬Collinear ℝ {cfg.B, cfg.A₁, cfg.C}
⊢ False
Theorem: Imo2019P2.Imo2019q2Cfg.A_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.A = cfg.A₁
h' : ¬Collinear ℝ {cfg.B, cfg.A₁, cfg.C}
⊢ False
Tactic:
exact h' cfg.wbtw_B_A₁_C.collinear
Proof state after:
no goals
Theorem: Imo2019P2.Imo2019q2Cfg.collinear_PAA₁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.P, cfg.A, cfg.A₁, cfg.A₂}
Tactic:
rw [A₂,
  (cfg.triangleABC.circumsphere.secondInter_collinear cfg.A cfg.A₁).collinear_insert_iff_of_ne
    (Set.mem_insert _ _) (Set.mem_insert_of_mem _ (Set.mem_insert _ _)) cfg.A_ne_A₁,
  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
⊢ Collinear ℝ {cfg.A, cfg.P, cfg.A₁}
Theorem: Imo2019P2.Imo2019q2Cfg.collinear_PAA₁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.A, cfg.P, cfg.A₁}
Tactic:
exact cfg.wbtw_A_P_A₁.collinear
Proof state after:
no goals
Theorem: Imo2019P2.Imo2019q2Cfg.A₁_ne_C
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.A₁ ≠ cfg.C
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.A₁ = cfg.C
⊢ False
Theorem: Imo2019P2.Imo2019q2Cfg.A₁_ne_C
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.C
⊢ False
Tactic:
have hsbtw := 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.A₁ = cfg.C
hsbtw : Sbtw ℝ cfg.Q cfg.A₁ cfg.Q₁
⊢ False
Theorem: Imo2019P2.Imo2019q2Cfg.A₁_ne_C
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.C
hsbtw : Sbtw ℝ cfg.Q cfg.A₁ cfg.Q₁
⊢ False
Tactic:
rw [h] at hsbtw
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.C
hsbtw : Sbtw ℝ cfg.Q cfg.C cfg.Q₁
⊢ False
Theorem: Imo2019P2.Imo2019q2Cfg.A₁_ne_C
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.C
hsbtw : Sbtw ℝ cfg.Q cfg.C cfg.Q₁
⊢ False
Tactic:
have ha := hsbtw.angle₂₃₁_eq_zero
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.C
hsbtw : Sbtw ℝ cfg.Q cfg.C cfg.Q₁
ha : ∠ cfg.C cfg.Q₁ cfg.Q = 0
⊢ False
Theorem: Imo2019P2.Imo2019q2Cfg.A₁_ne_C
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.C
hsbtw : Sbtw ℝ cfg.Q cfg.C cfg.Q₁
ha : ∠ cfg.C cfg.Q₁ cfg.Q = 0
⊢ False
Tactic:
rw [angle_CQ₁Q_eq_angle_CBA, angle_comm] at 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.A₁ = cfg.C
hsbtw : Sbtw ℝ cfg.Q cfg.C cfg.Q₁
ha : ∠ cfg.A cfg.B cfg.C = 0
⊢ False
Theorem: Imo2019P2.Imo2019q2Cfg.A₁_ne_C
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.C
hsbtw : Sbtw ℝ cfg.Q cfg.C cfg.Q₁
ha : ∠ cfg.A cfg.B cfg.C = 0
⊢ False
Tactic:
exact (angle_ne_zero_of_not_collinear cfg.not_collinear_ABC) ha
Proof state after:
no goals
Theorem: Imo2019P2.Imo2019q2Cfg.Q_not_mem_CB
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 ∉ affineSpan ℝ {cfg.C, cfg.B}
Tactic:
intro hQ
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
hQ : cfg.Q ∈ affineSpan ℝ {cfg.C, cfg.B}
⊢ False
Theorem: Imo2019P2.Imo2019q2Cfg.Q_not_mem_CB
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
hQ : cfg.Q ∈ affineSpan ℝ {cfg.C, cfg.B}
⊢ False
Tactic:
have hQA₁ : line[ℝ, cfg.Q, cfg.A₁] ≤ line[ℝ, cfg.C, cfg.B] :=
  affineSpan_pair_le_of_mem_of_mem hQ cfg.wbtw_B_A₁_C.symm.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
hQ : cfg.Q ∈ affineSpan ℝ {cfg.C, cfg.B}
hQA₁ : affineSpan ℝ {cfg.Q, cfg.A₁} ≤ affineSpan ℝ {cfg.C, cfg.B}
⊢ False
Theorem: Imo2019P2.Imo2019q2Cfg.Q_not_mem_CB
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
hQ : cfg.Q ∈ affineSpan ℝ {cfg.C, cfg.B}
hQA₁ : affineSpan ℝ {cfg.Q, cfg.A₁} ≤ affineSpan ℝ {cfg.C, cfg.B}
⊢ False
Tactic:
have hQ₁ : cfg.Q₁ ∈ line[ℝ, cfg.C, cfg.B] := by
  rw [AffineSubspace.le_def'] at hQA₁
  exact hQA₁ _ cfg.sbtw_Q_A₁_Q₁.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
hQ : cfg.Q ∈ affineSpan ℝ {cfg.C, cfg.B}
hQA₁ : affineSpan ℝ {cfg.Q, cfg.A₁} ≤ affineSpan ℝ {cfg.C, cfg.B}
hQ₁ : cfg.Q₁ ∈ affineSpan ℝ {cfg.C, cfg.B}
⊢ False
Theorem: Imo2019P2.Imo2019q2Cfg.Q_not_mem_CB
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
hQ : cfg.Q ∈ affineSpan ℝ {cfg.C, cfg.B}
hQA₁ : affineSpan ℝ {cfg.Q, cfg.A₁} ≤ affineSpan ℝ {cfg.C, cfg.B}
hQ₁ : cfg.Q₁ ∈ affineSpan ℝ {cfg.C, cfg.B}
⊢ False
Tactic:
have hc : Collinear ℝ ({cfg.C, cfg.Q₁, cfg.Q} : Set Pt) :=
  haveI hc' : Collinear ℝ ({cfg.B, cfg.C, cfg.Q₁, cfg.Q} : Set Pt) := by
    rw [Set.insert_comm cfg.B, Set.insert_comm cfg.B, Set.pair_comm, Set.insert_comm cfg.C,
      Set.insert_comm cfg.C]
    exact collinear_insert_insert_of_mem_affineSpan_pair hQ₁ hQ
  hc'.subset (Set.subset_insert _ _)
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
hQ : cfg.Q ∈ affineSpan ℝ {cfg.C, cfg.B}
hQA₁ : affineSpan ℝ {cfg.Q, cfg.A₁} ≤ affineSpan ℝ {cfg.C, cfg.B}
hQ₁ : cfg.Q₁ ∈ affineSpan ℝ {cfg.C, cfg.B}
hc : Collinear ℝ {cfg.C, cfg.Q₁, cfg.Q}
⊢ False
Theorem: Imo2019P2.Imo2019q2Cfg.Q_not_mem_CB
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
hQ : cfg.Q ∈ affineSpan ℝ {cfg.C, cfg.B}
hQA₁ : affineSpan ℝ {cfg.Q, cfg.A₁} ≤ affineSpan ℝ {cfg.C, cfg.B}
hQ₁ : cfg.Q₁ ∈ affineSpan ℝ {cfg.C, cfg.B}
hc : Collinear ℝ {cfg.C, cfg.Q₁, cfg.Q}
⊢ False
Tactic:
rw [collinear_iff_eq_or_eq_or_angle_eq_zero_or_angle_eq_pi, cfg.angle_CQ₁Q_eq_angle_CBA,
  or_iff_right cfg.C_ne_Q₁, or_iff_right cfg.sbtw_Q_A₁_Q₁.left_ne_right, angle_comm] at hc
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
hQ : cfg.Q ∈ affineSpan ℝ {cfg.C, cfg.B}
hQA₁ : affineSpan ℝ {cfg.Q, cfg.A₁} ≤ affineSpan ℝ {cfg.C, cfg.B}
hQ₁ : cfg.Q₁ ∈ affineSpan ℝ {cfg.C, cfg.B}
hc : ∠ cfg.A cfg.B cfg.C = 0 ∨ ∠ cfg.A cfg.B cfg.C = π
⊢ False
Theorem: Imo2019P2.Imo2019q2Cfg.Q_not_mem_CB
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
hQ : cfg.Q ∈ affineSpan ℝ {cfg.C, cfg.B}
hQA₁ : affineSpan ℝ {cfg.Q, cfg.A₁} ≤ affineSpan ℝ {cfg.C, cfg.B}
hQ₁ : cfg.Q₁ ∈ affineSpan ℝ {cfg.C, cfg.B}
hc : ∠ cfg.A cfg.B cfg.C = 0 ∨ ∠ cfg.A cfg.B cfg.C = π
⊢ False
Tactic:
exact cfg.not_collinear_ABC (hc.elim collinear_of_angle_eq_zero collinear_of_angle_eq_pi)
Proof state after:
no goals
Theorem: Imo2019P2.Imo2019q2Cfg.Q_not_mem_CB
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
hQ : cfg.Q ∈ affineSpan ℝ {cfg.C, cfg.B}
hQA₁ : affineSpan ℝ {cfg.Q, cfg.A₁} ≤ affineSpan ℝ {cfg.C, cfg.B}
⊢ cfg.Q₁ ∈ affineSpan ℝ {cfg.C, cfg.B}
Tactic:
rw [AffineSubspace.le_def'] at hQA₁
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
hQ : cfg.Q ∈ affineSpan ℝ {cfg.C, cfg.B}
hQA₁ : ∀ p ∈ affineSpan ℝ {cfg.Q, cfg.A₁}, p ∈ affineSpan ℝ {cfg.C, cfg.B}
⊢ cfg.Q₁ ∈ affineSpan ℝ {cfg.C, cfg.B}
Theorem: Imo2019P2.Imo2019q2Cfg.Q_not_mem_CB
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
hQ : cfg.Q ∈ affineSpan ℝ {cfg.C, cfg.B}
hQA₁ : ∀ p ∈ affineSpan ℝ {cfg.Q, cfg.A₁}, p ∈ affineSpan ℝ {cfg.C, cfg.B}
⊢ cfg.Q₁ ∈ affineSpan ℝ {cfg.C, cfg.B}
Tactic:
exact hQA₁ _ cfg.sbtw_Q_A₁_Q₁.right_mem_affineSpan
Proof state after:
no goals
Theorem: Imo2019P2.Imo2019q2Cfg.Q_not_mem_CB
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
hQ : cfg.Q ∈ affineSpan ℝ {cfg.C, cfg.B}
hQA₁ : affineSpan ℝ {cfg.Q, cfg.A₁} ≤ affineSpan ℝ {cfg.C, cfg.B}
hQ₁ : cfg.Q₁ ∈ affineSpan ℝ {cfg.C, cfg.B}
⊢ Collinear ℝ {cfg.B, cfg.C, cfg.Q₁, cfg.Q}
Tactic:
rw [Set.insert_comm cfg.B, Set.insert_comm cfg.B, Set.pair_comm, Set.insert_comm cfg.C,
  Set.insert_comm cfg.C]
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
hQ : cfg.Q ∈ affineSpan ℝ {cfg.C, cfg.B}
hQA₁ : affineSpan ℝ {cfg.Q, cfg.A₁} ≤ affineSpan ℝ {cfg.C, cfg.B}
hQ₁ : cfg.Q₁ ∈ affineSpan ℝ {cfg.C, cfg.B}
⊢ Collinear ℝ {cfg.Q₁, cfg.Q, cfg.C, cfg.B}
Theorem: Imo2019P2.Imo2019q2Cfg.Q_not_mem_CB
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
hQ : cfg.Q ∈ affineSpan ℝ {cfg.C, cfg.B}
hQA₁ : affineSpan ℝ {cfg.Q, cfg.A₁} ≤ affineSpan ℝ {cfg.C, cfg.B}
hQ₁ : cfg.Q₁ ∈ affineSpan ℝ {cfg.C, cfg.B}
⊢ Collinear ℝ {cfg.Q₁, cfg.Q, cfg.C, cfg.B}
Tactic:
exact collinear_insert_insert_of_mem_affineSpan_pair hQ₁ hQ
Proof state after:
no goals
Theorem: Imo2019P2.Imo2019q2Cfg.Q_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
⊢ cfg.Q ≠ cfg.B
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.B
⊢ False
Theorem: Imo2019P2.Imo2019q2Cfg.Q_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.Q = cfg.B
⊢ False
Tactic:
have h' := cfg.Q_not_mem_CB
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.B
h' : cfg.Q ∉ affineSpan ℝ {cfg.C, cfg.B}
⊢ False
Theorem: Imo2019P2.Imo2019q2Cfg.Q_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.Q = cfg.B
h' : cfg.Q ∉ affineSpan ℝ {cfg.C, cfg.B}
⊢ 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.B
h' : cfg.B ∉ affineSpan ℝ {cfg.C, cfg.B}
⊢ False
Theorem: Imo2019P2.Imo2019q2Cfg.Q_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.Q = cfg.B
h' : cfg.B ∉ affineSpan ℝ {cfg.C, cfg.B}
⊢ False
Tactic:
exact h' (right_mem_affineSpan_pair _ _ _)
Proof state after:
no goals
Theorem: Imo2019P2.Imo2019q2Cfg.oangle_CQ₁Q_sign_eq_oangle_CBA_sign
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)
⊢ (∡ cfg.C cfg.Q₁ cfg.Q).sign = (∡ cfg.C cfg.B cfg.A).sign
Tactic:
rw [← cfg.sbtw_Q_A₁_Q₁.symm.oangle_eq_right,
  cfg.sOppSide_CB_Q_Q₁.oangle_sign_eq_neg (left_mem_affineSpan_pair ℝ cfg.C cfg.B)
    cfg.wbtw_B_A₁_C.symm.mem_affineSpan,
  ← Real.Angle.sign_neg, ← oangle_rev,
  cfg.wbtw_B_A₁_C.oangle_sign_eq_of_ne_right cfg.Q cfg.A₁_ne_C, oangle_rotate_sign,
  cfg.wbtw_B_Q_B₁.oangle_eq_right cfg.Q_ne_B,
  cfg.wbtw_A_B₁_C.symm.oangle_sign_eq_of_ne_left cfg.B cfg.B₁_ne_C.symm]
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
⊢ cfg.A₁ ≠ cfg.B
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.A₁ = cfg.B
⊢ 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
⊢ False
Tactic:
have hwbtw := cfg.wbtw_A_P_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.A₁ = cfg.B
hwbtw : Wbtw ℝ cfg.A cfg.P cfg.A₁
⊢ 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.A₁
⊢ False
Tactic:
rw [h] at hwbtw
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
⊢ 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
⊢ 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
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}
⊢ 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}
⊢ False
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
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
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)
⊢ 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 _ _ _
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
⊢ False