internlm/Lean-Github huggingface dataset:
Theorem: Imo2019P2.Imo2019q2Cfg.sbtw_A_A₁_A₂
Proof state before:
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)
Tactic:
change _ = max (dist (cfg.triangleABC.points 1) _) (dist (cfg.triangleABC.points 2) _)
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.triangleABC.points 1) (circumsphere cfg.triangleABC).center)
      (dist (cfg.triangleABC.points 2) (circumsphere cfg.triangleABC).center)
Theorem: Imo2019P2.Imo2019q2Cfg.sbtw_A_A₁_A₂
Proof state before:
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.triangleABC.points 1) (circumsphere cfg.triangleABC).center)
      (dist (cfg.triangleABC.points 2) (circumsphere cfg.triangleABC).center)
Tactic:
simp_rw [circumsphere_center, circumsphere_radius, dist_circumcenter_eq_circumradius, max_self]
Proof state after:
no goals
Theorem: Imo2019P2.Imo2019q2Cfg.sbtw_B_B₁_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
⊢ Sbtw ℝ cfg.B cfg.B₁ cfg.B₂
Tactic:
rw [← cfg.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
⊢ Sbtw ℝ cfg.B cfg.B₁ cfg.symm.A₂
Theorem: Imo2019P2.Imo2019q2Cfg.sbtw_B_B₁_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
⊢ Sbtw ℝ cfg.B cfg.B₁ cfg.symm.A₂
Tactic:
exact cfg.symm.sbtw_A_A₁_A₂
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 h₁ := cfg.sbtw_A_A₁_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
h₁ : Sbtw ℝ cfg.A cfg.A₁ 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
h₁ : Sbtw ℝ cfg.A cfg.A₁ cfg.A₂
⊢ 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.A₂ = cfg.B
h₁ : Sbtw ℝ cfg.A 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
h₁ : Sbtw ℝ cfg.A cfg.A₁ cfg.B
⊢ False
Tactic:
refine 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
h₁ : Sbtw ℝ cfg.A cfg.A₁ cfg.B
⊢ 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
h₁ : Sbtw ℝ cfg.A cfg.A₁ cfg.B
⊢ Collinear ℝ {cfg.A, cfg.B, cfg.C}
Tactic:
have hc : Collinear ℝ ({cfg.A, cfg.C, cfg.B, cfg.A₁} : Set Pt) :=
  collinear_insert_insert_of_mem_affineSpan_pair h₁.left_mem_affineSpan
    cfg.sbtw_B_A₁_C.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.A₂ = cfg.B
h₁ : Sbtw ℝ cfg.A cfg.A₁ cfg.B
hc : Collinear ℝ {cfg.A, cfg.C, cfg.B, cfg.A₁}
⊢ 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
h₁ : Sbtw ℝ cfg.A cfg.A₁ cfg.B
hc : Collinear ℝ {cfg.A, cfg.C, cfg.B, cfg.A₁}
⊢ Collinear ℝ {cfg.A, cfg.B, cfg.C}
Tactic:
refine hc.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
h : cfg.A₂ = cfg.B
h₁ : Sbtw ℝ cfg.A cfg.A₁ cfg.B
hc : Collinear ℝ {cfg.A, cfg.C, cfg.B, cfg.A₁}
⊢ {cfg.A, cfg.B, cfg.C} ⊆ {cfg.A, cfg.C, cfg.B, cfg.A₁}
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
h₁ : Sbtw ℝ cfg.A cfg.A₁ cfg.B
hc : Collinear ℝ {cfg.A, cfg.C, cfg.B, cfg.A₁}
⊢ {cfg.A, cfg.B, cfg.C} ⊆ {cfg.A, cfg.C, cfg.B, cfg.A₁}
Tactic:
rw [Set.pair_comm _ cfg.A₁, Set.insert_comm _ cfg.A₁, Set.insert_comm _ cfg.A₁, 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
h₁ : Sbtw ℝ cfg.A cfg.A₁ cfg.B
hc : Collinear ℝ {cfg.A, cfg.C, cfg.B, cfg.A₁}
⊢ {cfg.A, cfg.C, cfg.B} ⊆ {cfg.A₁, cfg.A, cfg.C, 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
h₁ : Sbtw ℝ cfg.A cfg.A₁ cfg.B
hc : Collinear ℝ {cfg.A, cfg.C, cfg.B, cfg.A₁}
⊢ {cfg.A, cfg.C, cfg.B} ⊆ {cfg.A₁, cfg.A, cfg.C, cfg.B}
Tactic:
exact Set.subset_insert _ _
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 h₁ := cfg.sbtw_A_A₁_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.C
h₁ : Sbtw ℝ cfg.A cfg.A₁ cfg.A₂
⊢ 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
h₁ : Sbtw ℝ cfg.A cfg.A₁ cfg.A₂
⊢ 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.A₂ = cfg.C
h₁ : Sbtw ℝ cfg.A 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
h₁ : Sbtw ℝ cfg.A cfg.A₁ cfg.C
⊢ False
Tactic:
refine 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.C
h₁ : Sbtw ℝ cfg.A cfg.A₁ cfg.C
⊢ Collinear ℝ {cfg.A, cfg.B, cfg.C}
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
h₁ : Sbtw ℝ cfg.A cfg.A₁ cfg.C
⊢ Collinear ℝ {cfg.A, cfg.B, cfg.C}
Tactic:
have hc : Collinear ℝ ({cfg.A, cfg.B, cfg.C, cfg.A₁} : Set Pt) :=
  collinear_insert_insert_of_mem_affineSpan_pair h₁.left_mem_affineSpan
    cfg.sbtw_B_A₁_C.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.A₂ = cfg.C
h₁ : Sbtw ℝ cfg.A cfg.A₁ cfg.C
hc : Collinear ℝ {cfg.A, cfg.B, cfg.C, cfg.A₁}
⊢ Collinear ℝ {cfg.A, cfg.B, cfg.C}
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
h₁ : Sbtw ℝ cfg.A cfg.A₁ cfg.C
hc : Collinear ℝ {cfg.A, cfg.B, cfg.C, cfg.A₁}
⊢ Collinear ℝ {cfg.A, cfg.B, cfg.C}
Tactic:
refine hc.subset (Set.insert_subset_insert (Set.insert_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
h : cfg.A₂ = cfg.C
h₁ : Sbtw ℝ cfg.A cfg.A₁ cfg.C
hc : Collinear ℝ {cfg.A, cfg.B, cfg.C, cfg.A₁}
⊢ {cfg.C} ⊆ {cfg.C, cfg.A₁}
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
h₁ : Sbtw ℝ cfg.A cfg.A₁ cfg.C
hc : Collinear ℝ {cfg.A, cfg.B, cfg.C, cfg.A₁}
⊢ {cfg.C} ⊆ {cfg.C, cfg.A₁}
Tactic:
rw [Set.singleton_subset_iff]
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
h₁ : Sbtw ℝ cfg.A cfg.A₁ cfg.C
hc : Collinear ℝ {cfg.A, cfg.B, cfg.C, cfg.A₁}
⊢ cfg.C ∈ {cfg.C, cfg.A₁}
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
h₁ : Sbtw ℝ cfg.A cfg.A₁ cfg.C
hc : Collinear ℝ {cfg.A, cfg.B, cfg.C, cfg.A₁}
⊢ cfg.C ∈ {cfg.C, cfg.A₁}
Tactic:
exact Set.mem_insert _ _
Proof state after:
no goals
Theorem: Imo2019P2.Imo2019q2Cfg.B₂_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.B₂ ≠ 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
⊢ cfg.symm.A₂ ≠ cfg.B
Theorem: Imo2019P2.Imo2019q2Cfg.B₂_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.symm.A₂ ≠ cfg.B
Tactic:
exact cfg.symm.A₂_ne_A
Proof state after:
no goals
Theorem: Imo2019P2.Imo2019q2Cfg.B₂_ne_Q
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.B₂ ≠ cfg.Q
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
⊢ cfg.symm.A₂ ≠ cfg.Q
Theorem: Imo2019P2.Imo2019q2Cfg.B₂_ne_Q
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.A₂ ≠ cfg.Q
Tactic:
exact cfg.symm.A₂_ne_P
Proof state after:
no goals
Theorem: Imo2019P2.Imo2019q2Cfg.B₂_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.B₂ ≠ 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.B₂ = cfg.A₂
⊢ False
Theorem: Imo2019P2.Imo2019q2Cfg.B₂_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.B₂ = cfg.A₂
⊢ False
Tactic:
have hA : Sbtw ℝ (cfg.triangleABC.points 1) cfg.A₁ (cfg.triangleABC.points 2) := cfg.sbtw_B_A₁_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
h : cfg.B₂ = cfg.A₂
hA : Sbtw ℝ (cfg.triangleABC.points 1) cfg.A₁ (cfg.triangleABC.points 2)
⊢ False
Theorem: Imo2019P2.Imo2019q2Cfg.B₂_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.B₂ = cfg.A₂
hA : Sbtw ℝ (cfg.triangleABC.points 1) cfg.A₁ (cfg.triangleABC.points 2)
⊢ False
Tactic:
have hB : Sbtw ℝ (cfg.triangleABC.points 0) cfg.B₁ (cfg.triangleABC.points 2) := cfg.sbtw_A_B₁_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
h : cfg.B₂ = cfg.A₂
hA : Sbtw ℝ (cfg.triangleABC.points 1) cfg.A₁ (cfg.triangleABC.points 2)
hB : Sbtw ℝ (cfg.triangleABC.points 0) cfg.B₁ (cfg.triangleABC.points 2)
⊢ False
Theorem: Imo2019P2.Imo2019q2Cfg.B₂_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.B₂ = cfg.A₂
hA : Sbtw ℝ (cfg.triangleABC.points 1) cfg.A₁ (cfg.triangleABC.points 2)
hB : Sbtw ℝ (cfg.triangleABC.points 0) cfg.B₁ (cfg.triangleABC.points 2)
⊢ False
Tactic:
have hA' : cfg.A₂ ∈ line[ℝ, cfg.triangleABC.points 0, cfg.A₁] :=
  Sphere.secondInter_vsub_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.B₂ = cfg.A₂
hA : Sbtw ℝ (cfg.triangleABC.points 1) cfg.A₁ (cfg.triangleABC.points 2)
hB : Sbtw ℝ (cfg.triangleABC.points 0) cfg.B₁ (cfg.triangleABC.points 2)
hA' : cfg.A₂ ∈ affineSpan ℝ {cfg.triangleABC.points 0, cfg.A₁}
⊢ False
Theorem: Imo2019P2.Imo2019q2Cfg.B₂_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.B₂ = cfg.A₂
hA : Sbtw ℝ (cfg.triangleABC.points 1) cfg.A₁ (cfg.triangleABC.points 2)
hB : Sbtw ℝ (cfg.triangleABC.points 0) cfg.B₁ (cfg.triangleABC.points 2)
hA' : cfg.A₂ ∈ affineSpan ℝ {cfg.triangleABC.points 0, cfg.A₁}
⊢ False
Tactic:
have hB' : cfg.A₂ ∈ line[ℝ, cfg.triangleABC.points 1, cfg.B₁] := by
  rw [← h]; exact Sphere.secondInter_vsub_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.B₂ = cfg.A₂
hA : Sbtw ℝ (cfg.triangleABC.points 1) cfg.A₁ (cfg.triangleABC.points 2)
hB : Sbtw ℝ (cfg.triangleABC.points 0) cfg.B₁ (cfg.triangleABC.points 2)
hA' : cfg.A₂ ∈ affineSpan ℝ {cfg.triangleABC.points 0, cfg.A₁}
hB' : cfg.A₂ ∈ affineSpan ℝ {cfg.triangleABC.points 1, cfg.B₁}
⊢ False
Theorem: Imo2019P2.Imo2019q2Cfg.B₂_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.B₂ = cfg.A₂
hA : Sbtw ℝ (cfg.triangleABC.points 1) cfg.A₁ (cfg.triangleABC.points 2)
hB : Sbtw ℝ (cfg.triangleABC.points 0) cfg.B₁ (cfg.triangleABC.points 2)
hA' : cfg.A₂ ∈ affineSpan ℝ {cfg.triangleABC.points 0, cfg.A₁}
hB' : cfg.A₂ ∈ affineSpan ℝ {cfg.triangleABC.points 1, cfg.B₁}
⊢ False
Tactic:
exact (sbtw_of_sbtw_of_sbtw_of_mem_affineSpan_pair (by decide) hA hB hA' hB').symm.not_rotate
  cfg.sbtw_A_A₁_A₂.wbtw
Proof state after:
no goals
Theorem: Imo2019P2.Imo2019q2Cfg.B₂_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.B₂ = cfg.A₂
hA : Sbtw ℝ (cfg.triangleABC.points 1) cfg.A₁ (cfg.triangleABC.points 2)
hB : Sbtw ℝ (cfg.triangleABC.points 0) cfg.B₁ (cfg.triangleABC.points 2)
hA' : cfg.A₂ ∈ affineSpan ℝ {cfg.triangleABC.points 0, cfg.A₁}
⊢ cfg.A₂ ∈ affineSpan ℝ {cfg.triangleABC.points 1, cfg.B₁}
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.B₂ = cfg.A₂
hA : Sbtw ℝ (cfg.triangleABC.points 1) cfg.A₁ (cfg.triangleABC.points 2)
hB : Sbtw ℝ (cfg.triangleABC.points 0) cfg.B₁ (cfg.triangleABC.points 2)
hA' : cfg.A₂ ∈ affineSpan ℝ {cfg.triangleABC.points 0, cfg.A₁}
⊢ cfg.B₂ ∈ affineSpan ℝ {cfg.triangleABC.points 1, cfg.B₁}
Theorem: Imo2019P2.Imo2019q2Cfg.B₂_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.B₂ = cfg.A₂
hA : Sbtw ℝ (cfg.triangleABC.points 1) cfg.A₁ (cfg.triangleABC.points 2)
hB : Sbtw ℝ (cfg.triangleABC.points 0) cfg.B₁ (cfg.triangleABC.points 2)
hA' : cfg.A₂ ∈ affineSpan ℝ {cfg.triangleABC.points 0, cfg.A₁}
⊢ cfg.B₂ ∈ affineSpan ℝ {cfg.triangleABC.points 1, cfg.B₁}
Tactic:
exact Sphere.secondInter_vsub_mem_affineSpan _ _ _
Proof state after:
no goals
Theorem: Imo2019P2.Imo2019q2Cfg.B₂_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.B₂ = cfg.A₂
hA : Sbtw ℝ (cfg.triangleABC.points 1) cfg.A₁ (cfg.triangleABC.points 2)
hB : Sbtw ℝ (cfg.triangleABC.points 0) cfg.B₁ (cfg.triangleABC.points 2)
hA' : cfg.A₂ ∈ affineSpan ℝ {cfg.triangleABC.points 0, cfg.A₁}
hB' : cfg.A₂ ∈ affineSpan ℝ {cfg.triangleABC.points 1, cfg.B₁}
⊢ 0 ≠ 1
Tactic:
decide
Proof state after:
no goals
Theorem: Imo2019P2.Imo2019q2Cfg.two_zsmul_oangle_QPA₂_eq_two_zsmul_oangle_BAA₂
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.Q cfg.P cfg.A₂ = 2 • ∡ cfg.B cfg.A cfg.A₂
Tactic:
refine two_zsmul_oangle_of_parallel cfg.QP_parallel_BA ?_
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
inst✝ : Module.Oriented ℝ V (Fin 2)
⊢ affineSpan ℝ {cfg.A₂, cfg.P} ∥ affineSpan ℝ {cfg.A₂, cfg.A}
Theorem: Imo2019P2.Imo2019q2Cfg.two_zsmul_oangle_QPA₂_eq_two_zsmul_oangle_BAA₂
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)
⊢ affineSpan ℝ {cfg.A₂, cfg.P} ∥ affineSpan ℝ {cfg.A₂, cfg.A}
Tactic:
convert AffineSubspace.Parallel.refl (k := ℝ) (P := Pt) _ using 1
Proof state after:
case h.e'_9
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)
⊢ affineSpan ℝ {cfg.A₂, cfg.A} = affineSpan ℝ {cfg.A₂, cfg.P}
Theorem: Imo2019P2.Imo2019q2Cfg.two_zsmul_oangle_QPA₂_eq_two_zsmul_oangle_BAA₂
Proof state before:
case h.e'_9
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)
⊢ affineSpan ℝ {cfg.A₂, cfg.A} = affineSpan ℝ {cfg.A₂, cfg.P}
Tactic:
rw [cfg.collinear_PAA₁A₂.affineSpan_eq_of_ne (Set.mem_insert_of_mem _
  (Set.mem_insert_of_mem _ (Set.mem_insert_of_mem _ (Set.mem_singleton _))))
  (Set.mem_insert_of_mem _ (Set.mem_insert _ _)) cfg.A₂_ne_A,
    cfg.collinear_PAA₁A₂.affineSpan_eq_of_ne (Set.mem_insert_of_mem _
  (Set.mem_insert_of_mem _ (Set.mem_insert_of_mem _ (Set.mem_singleton _))))
  (Set.mem_insert _ _) cfg.A₂_ne_P]
Proof state after:
no goals