Theorem: Imo2019P2.Imo2019q2Cfg.B₂_ne_A₂ (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.B₂ ≠ cfg.A₂
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.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.B₂ = cfg.A₂
⊢ False
Tactic:
have hA : Sbtw ℝ (cfg.triangleABC.points 1) cfg.A₁ (cfg.triangleABC.points 2) := cfg.sbtw_B_A₁_C
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

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

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

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

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

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