Theorem: eqn_7 (LeanCamCombi/SylvesterChvatal.lean)

State before:
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z a b c d : V
habc : SimpleTriangle a b c
habc_min : ∀ (a' b' c' : V), SimpleTriangle a' b' c' → Delta a b c ≤ Delta a' b' c'
hacd : sbtw a c d
hcd : SimpleEdges.Adj c d
⊢ ¬SimpleEdges.Adj b d
Tactic:
intro h
State after:
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z a b c d : V
habc : SimpleTriangle a b c
habc_min : ∀ (a' b' c' : V), SimpleTriangle a' b' c' → Delta a b c ≤ Delta a' b' c'
hacd : sbtw a c d
hcd : SimpleEdges.Adj c d
h : SimpleEdges.Adj b d
⊢ False

State before:
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z a b c d : V
habc : SimpleTriangle a b c
habc_min : ∀ (a' b' c' : V), SimpleTriangle a' b' c' → Delta a b c ≤ Delta a' b' c'
hacd : sbtw a c d
hcd : SimpleEdges.Adj c d
h : SimpleEdges.Adj b d
⊢ False
Tactic:
have hbcd : NotCollinear b c d := by
  refine ⟨habc.2.1.ne, h.ne, hcd.ne, fun l hl h ↦ ?_⟩
  simp only [Set.mem_singleton_iff, Set.mem_insert_iff, Set.subset_def, forall_eq_or_imp,
    forall_eq] at h
  refine habc.2.2.2.2.2.2 l hl (by simp [*, hl.close_left h.2.1 h.2.2 hacd])
State after:
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z a b c d : V
habc : SimpleTriangle a b c
habc_min : ∀ (a' b' c' : V), SimpleTriangle a' b' c' → Delta a b c ≤ Delta a' b' c'
hacd : sbtw a c d
hcd : SimpleEdges.Adj c d
h : SimpleEdges.Adj b d
hbcd : NotCollinear b c d
⊢ False

State before:
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z a b c d : V
habc : SimpleTriangle a b c
habc_min : ∀ (a' b' c' : V), SimpleTriangle a' b' c' → Delta a b c ≤ Delta a' b' c'
hacd : sbtw a c d
hcd : SimpleEdges.Adj c d
h : SimpleEdges.Adj b d
hbcd : NotCollinear b c d
⊢ False
Tactic:
replace hbcd : SimpleTriangle b c d := ⟨habc.2.1, hcd, h.symm, hbcd⟩
State after:
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z a b c d : V
habc : SimpleTriangle a b c
habc_min : ∀ (a' b' c' : V), SimpleTriangle a' b' c' → Delta a b c ≤ Delta a' b' c'
hacd : sbtw a c d
hcd : SimpleEdges.Adj c d
h : SimpleEdges.Adj b d
hbcd : SimpleTriangle b c d
⊢ False

State before:
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z a b c d : V
habc : SimpleTriangle a b c
habc_min : ∀ (a' b' c' : V), SimpleTriangle a' b' c' → Delta a b c ≤ Delta a' b' c'
hacd : sbtw a c d
hcd : SimpleEdges.Adj c d
h : SimpleEdges.Adj b d
hbcd : SimpleTriangle b c d
⊢ False
Tactic:
have habd : sbtw a b d := by
  refine sbtw_mk habc.1.ne h.ne ?_
  have := habc_min _ _ _ hbcd
  rw [Delta, Delta] at this
  linarith [hacd.dist]
State after:
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z a b c d : V
habc : SimpleTriangle a b c
habc_min : ∀ (a' b' c' : V), SimpleTriangle a' b' c' → Delta a b c ≤ Delta a' b' c'
hacd : sbtw a c d
hcd : SimpleEdges.Adj c d
h : SimpleEdges.Adj b d
hbcd : SimpleTriangle b c d
habd : sbtw a b d
⊢ False

State before:
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z a b c d : V
habc : SimpleTriangle a b c
habc_min : ∀ (a' b' c' : V), SimpleTriangle a' b' c' → Delta a b c ≤ Delta a' b' c'
hacd : sbtw a c d
hcd : SimpleEdges.Adj c d
h : SimpleEdges.Adj b d
hbcd : SimpleTriangle b c d
habd : sbtw a b d
⊢ False
Tactic:
refine habc.2.2.2.2.2.2 (Line a d) (Line_isLine habd.ne13) ?_
State after:
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z a b c d : V
habc : SimpleTriangle a b c
habc_min : ∀ (a' b' c' : V), SimpleTriangle a' b' c' → Delta a b c ≤ Delta a' b' c'
hacd : sbtw a c d
hcd : SimpleEdges.Adj c d
h : SimpleEdges.Adj b d
hbcd : SimpleTriangle b c d
habd : sbtw a b d
⊢ {a, b, c} ⊆ Line a d

State before:
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z a b c d : V
habc : SimpleTriangle a b c
habc_min : ∀ (a' b' c' : V), SimpleTriangle a' b' c' → Delta a b c ≤ Delta a' b' c'
hacd : sbtw a c d
hcd : SimpleEdges.Adj c d
h : SimpleEdges.Adj b d
hbcd : SimpleTriangle b c d
habd : sbtw a b d
⊢ {a, b, c} ⊆ Line a d
Tactic:
simp [middle_extend_mem_Line, hacd, habd]
State after:
no goals

State before:
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z a b c d : V
habc : SimpleTriangle a b c
habc_min : ∀ (a' b' c' : V), SimpleTriangle a' b' c' → Delta a b c ≤ Delta a' b' c'
hacd : sbtw a c d
hcd : SimpleEdges.Adj c d
h : SimpleEdges.Adj b d
⊢ NotCollinear b c d
Tactic:
refine ⟨habc.2.1.ne, h.ne, hcd.ne, fun l hl h ↦ ?_⟩
State after:
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z a b c d : V
habc : SimpleTriangle a b c
habc_min : ∀ (a' b' c' : V), SimpleTriangle a' b' c' → Delta a b c ≤ Delta a' b' c'
hacd : sbtw a c d
hcd : SimpleEdges.Adj c d
h✝ : SimpleEdges.Adj b d
l : Set V
hl : l.IsLine
h : {b, c, d} ⊆ l
⊢ False

State before:
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z a b c d : V
habc : SimpleTriangle a b c
habc_min : ∀ (a' b' c' : V), SimpleTriangle a' b' c' → Delta a b c ≤ Delta a' b' c'
hacd : sbtw a c d
hcd : SimpleEdges.Adj c d
h✝ : SimpleEdges.Adj b d
l : Set V
hl : l.IsLine
h : {b, c, d} ⊆ l
⊢ False
Tactic:
simp only [Set.mem_singleton_iff, Set.mem_insert_iff, Set.subset_def, forall_eq_or_imp,
  forall_eq] at h
State after:
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z a b c d : V
habc : SimpleTriangle a b c
habc_min : ∀ (a' b' c' : V), SimpleTriangle a' b' c' → Delta a b c ≤ Delta a' b' c'
hacd : sbtw a c d
hcd : SimpleEdges.Adj c d
h✝ : SimpleEdges.Adj b d
l : Set V
hl : l.IsLine
h : b ∈ l ∧ c ∈ l ∧ d ∈ l
⊢ False

State before:
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z a b c d : V
habc : SimpleTriangle a b c
habc_min : ∀ (a' b' c' : V), SimpleTriangle a' b' c' → Delta a b c ≤ Delta a' b' c'
hacd : sbtw a c d
hcd : SimpleEdges.Adj c d
h✝ : SimpleEdges.Adj b d
l : Set V
hl : l.IsLine
h : b ∈ l ∧ c ∈ l ∧ d ∈ l
⊢ False
Tactic:
refine habc.2.2.2.2.2.2 l hl (by simp [*, hl.close_left h.2.1 h.2.2 hacd])
State after:
no goals

State before:
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z a b c d : V
habc : SimpleTriangle a b c
habc_min : ∀ (a' b' c' : V), SimpleTriangle a' b' c' → Delta a b c ≤ Delta a' b' c'
hacd : sbtw a c d
hcd : SimpleEdges.Adj c d
h✝ : SimpleEdges.Adj b d
l : Set V
hl : l.IsLine
h : b ∈ l ∧ c ∈ l ∧ d ∈ l
⊢ {a, b, c} ⊆ l
Tactic:
simp [*, hl.close_left h.2.1 h.2.2 hacd]
State after:
no goals

State before:
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z a b c d : V
habc : SimpleTriangle a b c
habc_min : ∀ (a' b' c' : V), SimpleTriangle a' b' c' → Delta a b c ≤ Delta a' b' c'
hacd : sbtw a c d
hcd : SimpleEdges.Adj c d
h : SimpleEdges.Adj b d
hbcd : SimpleTriangle b c d
⊢ sbtw a b d
Tactic:
refine sbtw_mk habc.1.ne h.ne ?_
State after:
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z a b c d : V
habc : SimpleTriangle a b c
habc_min : ∀ (a' b' c' : V), SimpleTriangle a' b' c' → Delta a b c ≤ Delta a' b' c'
hacd : sbtw a c d
hcd : SimpleEdges.Adj c d
h : SimpleEdges.Adj b d
hbcd : SimpleTriangle b c d
⊢ dist a b + dist b d ≤ dist a d

State before:
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z a b c d : V
habc : SimpleTriangle a b c
habc_min : ∀ (a' b' c' : V), SimpleTriangle a' b' c' → Delta a b c ≤ Delta a' b' c'
hacd : sbtw a c d
hcd : SimpleEdges.Adj c d
h : SimpleEdges.Adj b d
hbcd : SimpleTriangle b c d
⊢ dist a b + dist b d ≤ dist a d
Tactic:
have := habc_min _ _ _ hbcd
State after:
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z a b c d : V
habc : SimpleTriangle a b c
habc_min : ∀ (a' b' c' : V), SimpleTriangle a' b' c' → Delta a b c ≤ Delta a' b' c'
hacd : sbtw a c d
hcd : SimpleEdges.Adj c d
h : SimpleEdges.Adj b d
hbcd : SimpleTriangle b c d
this : Delta a b c ≤ Delta b c d
⊢ dist a b + dist b d ≤ dist a d

State before:
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z a b c d : V
habc : SimpleTriangle a b c
habc_min : ∀ (a' b' c' : V), SimpleTriangle a' b' c' → Delta a b c ≤ Delta a' b' c'
hacd : sbtw a c d
hcd : SimpleEdges.Adj c d
h : SimpleEdges.Adj b d
hbcd : SimpleTriangle b c d
this : Delta a b c ≤ Delta b c d
⊢ dist a b + dist b d ≤ dist a d
Tactic:
rw [Delta, Delta] at this
State after:
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z a b c d : V
habc : SimpleTriangle a b c
habc_min : ∀ (a' b' c' : V), SimpleTriangle a' b' c' → Delta a b c ≤ Delta a' b' c'
hacd : sbtw a c d
hcd : SimpleEdges.Adj c d
h : SimpleEdges.Adj b d
hbcd : SimpleTriangle b c d
this : dist a b + dist b c - dist a c ≤ dist b c + dist c d - dist b d
⊢ dist a b + dist b d ≤ dist a d

State before:
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z a b c d : V
habc : SimpleTriangle a b c
habc_min : ∀ (a' b' c' : V), SimpleTriangle a' b' c' → Delta a b c ≤ Delta a' b' c'
hacd : sbtw a c d
hcd : SimpleEdges.Adj c d
h : SimpleEdges.Adj b d
hbcd : SimpleTriangle b c d
this : dist a b + dist b c - dist a c ≤ dist b c + dist c d - dist b d
⊢ dist a b + dist b d ≤ dist a d
Tactic:
linarith [hacd.dist]
State after:
no goals