Theorem: Imo2019P2.Imo2019q2Cfg.A₂_ne_C (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.C
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.C
⊢ 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.C
⊢ 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.C
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.C
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.C
h₁ : Sbtw ℝ cfg.A cfg.A₁ cfg.C
⊢ 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.C
h₁ : Sbtw ℝ cfg.A cfg.A₁ cfg.C
⊢ 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.C
h₁ : Sbtw ℝ cfg.A cfg.A₁ cfg.C
⊢ 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.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
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}

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

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

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