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 h₁ := cfg.sbtw_A_A₁_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
h₁ : Sbtw ℝ cfg.A cfg.A₁ 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
h₁ : Sbtw ℝ cfg.A cfg.A₁ cfg.A₂
⊢ False
Tactic:
rw [h] at 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
h₁ : Sbtw ℝ cfg.A 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
h₁ : Sbtw ℝ cfg.A cfg.A₁ cfg.B
⊢ False
Tactic:
refine 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
h₁ : Sbtw ℝ cfg.A cfg.A₁ cfg.B
⊢ 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
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
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}

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

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

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