internlm/Lean-Github huggingface dataset:
Theorem: two_implies_three
Proof state before:
case intro.mk.mk.intro
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z : V
h : ∃ x y z, SimpleTriangle x y z
S : Set (V × V × V) := {(x, y, z) | SimpleTriangle x y z}
this : S.Nonempty
a b c : V
habc : SimpleTriangle a b c
hmin : ∀ (a' b' c' : V), SimpleTriangle a' b' c' → Delta a b c ≤ Delta a' b' c'
⊢ Line a c = {a, c}
Tactic:
by_contra! h3
Proof state after:
case intro.mk.mk.intro
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z : V
h : ∃ x y z, SimpleTriangle x y z
S : Set (V × V × V) := {(x, y, z) | SimpleTriangle x y z}
this : S.Nonempty
a b c : V
habc : SimpleTriangle a b c
hmin : ∀ (a' b' c' : V), SimpleTriangle a' b' c' → Delta a b c ≤ Delta a' b' c'
h3 : Line a c ≠ {a, c}
⊢ False
Theorem: two_implies_three
Proof state before:
case intro.mk.mk.intro
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z : V
h : ∃ x y z, SimpleTriangle x y z
S : Set (V × V × V) := {(x, y, z) | SimpleTriangle x y z}
this : S.Nonempty
a b c : V
habc : SimpleTriangle a b c
hmin : ∀ (a' b' c' : V), SimpleTriangle a' b' c' → Delta a b c ≤ Delta a' b' c'
h3 : Line a c ≠ {a, c}
⊢ False
Tactic:
obtain ⟨d, hd, hd'⟩ := exists_third habc.2.2.1.1.symm h3
Proof state after:
case intro.mk.mk.intro.intro.intro
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z : V
h : ∃ x y z, SimpleTriangle x y z
S : Set (V × V × V) := {(x, y, z) | SimpleTriangle x y z}
this : S.Nonempty
a b c : V
habc : SimpleTriangle a b c
hmin : ∀ (a' b' c' : V), SimpleTriangle a' b' c' → Delta a b c ≤ Delta a' b' c'
h3 : Line a c ≠ {a, c}
d : V
hd : d ∈ Line a c
hd' : sbtw d a c ∨ sbtw a d c ∨ sbtw a c d
⊢ False
Theorem: two_implies_three
Proof state before:
case intro.mk.mk.intro.intro.intro
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z : V
h : ∃ x y z, SimpleTriangle x y z
S : Set (V × V × V) := {(x, y, z) | SimpleTriangle x y z}
this : S.Nonempty
a b c : V
habc : SimpleTriangle a b c
hmin : ∀ (a' b' c' : V), SimpleTriangle a' b' c' → Delta a b c ≤ Delta a' b' c'
h3 : Line a c ≠ {a, c}
d : V
hd : d ∈ Line a c
hd' : sbtw d a c ∨ sbtw a d c ∨ sbtw a c d
⊢ False
Tactic:
simp only [habc.2.2.1.symm.2 d, false_or] at hd'
Proof state after:
case intro.mk.mk.intro.intro.intro
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z : V
h : ∃ x y z, SimpleTriangle x y z
S : Set (V × V × V) := {(x, y, z) | SimpleTriangle x y z}
this : S.Nonempty
a b c : V
habc : SimpleTriangle a b c
hmin : ∀ (a' b' c' : V), SimpleTriangle a' b' c' → Delta a b c ≤ Delta a' b' c'
h3 : Line a c ≠ {a, c}
d : V
hd : d ∈ Line a c
hd' : sbtw d a c ∨ sbtw a c d
⊢ False
Theorem: two_implies_three
Proof state before:
case intro.mk.mk.intro.intro.intro
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z : V
h : ∃ x y z, SimpleTriangle x y z
S : Set (V × V × V) := {(x, y, z) | SimpleTriangle x y z}
this : S.Nonempty
a b c : V
habc : SimpleTriangle a b c
hmin : ∀ (a' b' c' : V), SimpleTriangle a' b' c' → Delta a b c ≤ Delta a' b' c'
h3 : Line a c ≠ {a, c}
d : V
hd : d ∈ Line a c
hd' : sbtw d a c ∨ sbtw a c d
⊢ False
Tactic:
wlog acd : sbtw a c d generalizing a c
Proof state after:
case intro.mk.mk.intro.intro.intro.inr
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z : V
h : ∃ x y z, SimpleTriangle x y z
S : Set (V × V × V) := {(x, y, z) | SimpleTriangle x y z}
this✝ : S.Nonempty
a b c : V
habc : SimpleTriangle a b c
hmin : ∀ (a' b' c' : V), SimpleTriangle a' b' c' → Delta a b c ≤ Delta a' b' c'
h3 : Line a c ≠ {a, c}
d : V
hd : d ∈ Line a c
hd' : sbtw d a c ∨ sbtw a c d
this :
  ∀ (a c : V),
    SimpleTriangle a b c →
      (∀ (a' b' c' : V), SimpleTriangle a' b' c' → Delta a b c ≤ Delta a' b' c') →
        Line a c ≠ {a, c} → d ∈ Line a c → sbtw d a c ∨ sbtw a c d → sbtw a c d → False
acd : ¬sbtw a c d
⊢ False

V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z : V
h : ∃ x y z, SimpleTriangle x y z
S : Set (V × V × V) := {(x, y, z) | SimpleTriangle x y z}
this : S.Nonempty
b d a c : V
habc : SimpleTriangle a b c
hmin : ∀ (a' b' c' : V), SimpleTriangle a' b' c' → Delta a b c ≤ Delta a' b' c'
h3 : Line a c ≠ {a, c}
hd : d ∈ Line a c
hd' : sbtw d a c ∨ sbtw a c d
acd : sbtw a c d
⊢ False
Theorem: two_implies_three
Proof state before:
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z : V
h : ∃ x y z, SimpleTriangle x y z
S : Set (V × V × V) := {(x, y, z) | SimpleTriangle x y z}
this : S.Nonempty
b d a c : V
habc : SimpleTriangle a b c
hmin : ∀ (a' b' c' : V), SimpleTriangle a' b' c' → Delta a b c ≤ Delta a' b' c'
h3 : Line a c ≠ {a, c}
hd : d ∈ Line a c
hd' : sbtw d a c ∨ sbtw a c d
acd : sbtw a c d
⊢ False
Tactic:
clear hd'
Proof state after:
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z : V
h : ∃ x y z, SimpleTriangle x y z
S : Set (V × V × V) := {(x, y, z) | SimpleTriangle x y z}
this : S.Nonempty
b d a c : V
habc : SimpleTriangle a b c
hmin : ∀ (a' b' c' : V), SimpleTriangle a' b' c' → Delta a b c ≤ Delta a' b' c'
h3 : Line a c ≠ {a, c}
hd : d ∈ Line a c
acd : sbtw a c d
⊢ False
Theorem: two_implies_three
Proof state before:
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z : V
h : ∃ x y z, SimpleTriangle x y z
S : Set (V × V × V) := {(x, y, z) | SimpleTriangle x y z}
this : S.Nonempty
b d a c : V
habc : SimpleTriangle a b c
hmin : ∀ (a' b' c' : V), SimpleTriangle a' b' c' → Delta a b c ≤ Delta a' b' c'
h3 : Line a c ≠ {a, c}
hd : d ∈ Line a c
acd : sbtw a c d
⊢ False
Tactic:
let S : Set V := setOf (sbtw a c)
Proof state after:
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z : V
h : ∃ x y z, SimpleTriangle x y z
S✝ : Set (V × V × V) := {(x, y, z) | SimpleTriangle x y z}
this : S✝.Nonempty
b d a c : V
habc : SimpleTriangle a b c
hmin : ∀ (a' b' c' : V), SimpleTriangle a' b' c' → Delta a b c ≤ Delta a' b' c'
h3 : Line a c ≠ {a, c}
hd : d ∈ Line a c
acd : sbtw a c d
S : Set V := setOf (sbtw a c)
⊢ False
Theorem: two_implies_three
Proof state before:
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z : V
h : ∃ x y z, SimpleTriangle x y z
S✝ : Set (V × V × V) := {(x, y, z) | SimpleTriangle x y z}
this : S✝.Nonempty
b d a c : V
habc : SimpleTriangle a b c
hmin : ∀ (a' b' c' : V), SimpleTriangle a' b' c' → Delta a b c ≤ Delta a' b' c'
h3 : Line a c ≠ {a, c}
hd : d ∈ Line a c
acd : sbtw a c d
S : Set V := setOf (sbtw a c)
⊢ False
Tactic:
obtain ⟨d, hd : sbtw _ _ d, hdmin⟩ := S.toFinite.exists_minimal_wrt (dist c) S ⟨d, acd⟩
Proof state after:
case intro.intro
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z : V
h : ∃ x y z, SimpleTriangle x y z
S✝ : Set (V × V × V) := {(x, y, z) | SimpleTriangle x y z}
this : S✝.Nonempty
b d✝ a c : V
habc : SimpleTriangle a b c
hmin : ∀ (a' b' c' : V), SimpleTriangle a' b' c' → Delta a b c ≤ Delta a' b' c'
h3 : Line a c ≠ {a, c}
hd✝ : d✝ ∈ Line a c
acd : sbtw a c d✝
S : Set V := setOf (sbtw a c)
d : V
hd : sbtw a c d
hdmin : ∀ a' ∈ S, dist c a' ≤ dist c d → dist c d = dist c a'
⊢ False
Theorem: two_implies_three
Proof state before:
case intro.intro
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z : V
h : ∃ x y z, SimpleTriangle x y z
S✝ : Set (V × V × V) := {(x, y, z) | SimpleTriangle x y z}
this : S✝.Nonempty
b d✝ a c : V
habc : SimpleTriangle a b c
hmin : ∀ (a' b' c' : V), SimpleTriangle a' b' c' → Delta a b c ≤ Delta a' b' c'
h3 : Line a c ≠ {a, c}
hd✝ : d✝ ∈ Line a c
acd : sbtw a c d✝
S : Set V := setOf (sbtw a c)
d : V
hd : sbtw a c d
hdmin : ∀ a' ∈ S, dist c a' ≤ dist c d → dist c d = dist c a'
⊢ False
Tactic:
have hbd' : b ≠ d := by
  rintro rfl
  have := habc.2.2.2.2.2.2 (Line a c) (Line_isLine hd.ne12)
  simp [right_extend_mem_Line hd] at this
Proof state after:
case intro.intro
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z : V
h : ∃ x y z, SimpleTriangle x y z
S✝ : Set (V × V × V) := {(x, y, z) | SimpleTriangle x y z}
this : S✝.Nonempty
b d✝ a c : V
habc : SimpleTriangle a b c
hmin : ∀ (a' b' c' : V), SimpleTriangle a' b' c' → Delta a b c ≤ Delta a' b' c'
h3 : Line a c ≠ {a, c}
hd✝ : d✝ ∈ Line a c
acd : sbtw a c d✝
S : Set V := setOf (sbtw a c)
d : V
hd : sbtw a c d
hdmin : ∀ a' ∈ S, dist c a' ≤ dist c d → dist c d = dist c a'
hbd' : b ≠ d
⊢ False
Theorem: two_implies_three
Proof state before:
case intro.intro
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z : V
h : ∃ x y z, SimpleTriangle x y z
S✝ : Set (V × V × V) := {(x, y, z) | SimpleTriangle x y z}
this : S✝.Nonempty
b d✝ a c : V
habc : SimpleTriangle a b c
hmin : ∀ (a' b' c' : V), SimpleTriangle a' b' c' → Delta a b c ≤ Delta a' b' c'
h3 : Line a c ≠ {a, c}
hd✝ : d✝ ∈ Line a c
acd : sbtw a c d✝
S : Set V := setOf (sbtw a c)
d : V
hd : sbtw a c d
hdmin : ∀ a' ∈ S, dist c a' ≤ dist c d → dist c d = dist c a'
hbd' : b ≠ d
⊢ False
Tactic:
replace hdmin : ∀ d', sbtw a c d' → dist c d ≤ dist c d' := by
  intro d' hd'
  by_contra! hd''
  exact hd''.ne' (hdmin d' hd' hd''.le)
Proof state after:
case intro.intro
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z : V
h : ∃ x y z, SimpleTriangle x y z
S✝ : Set (V × V × V) := {(x, y, z) | SimpleTriangle x y z}
this : S✝.Nonempty
b d✝ a c : V
habc : SimpleTriangle a b c
hmin : ∀ (a' b' c' : V), SimpleTriangle a' b' c' → Delta a b c ≤ Delta a' b' c'
h3 : Line a c ≠ {a, c}
hd✝ : d✝ ∈ Line a c
acd : sbtw a c d✝
S : Set V := setOf (sbtw a c)
d : V
hd : sbtw a c d
hbd' : b ≠ d
hdmin : ∀ (d' : V), sbtw a c d' → dist c d ≤ dist c d'
⊢ False
Theorem: two_implies_three
Proof state before:
case intro.intro
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z : V
h : ∃ x y z, SimpleTriangle x y z
S✝ : Set (V × V × V) := {(x, y, z) | SimpleTriangle x y z}
this : S✝.Nonempty
b d✝ a c : V
habc : SimpleTriangle a b c
hmin : ∀ (a' b' c' : V), SimpleTriangle a' b' c' → Delta a b c ≤ Delta a' b' c'
h3 : Line a c ≠ {a, c}
hd✝ : d✝ ∈ Line a c
acd : sbtw a c d✝
S : Set V := setOf (sbtw a c)
d : V
hd : sbtw a c d
hbd' : b ≠ d
hdmin : ∀ (d' : V), sbtw a c d' → dist c d ≤ dist c d'
⊢ False
Tactic:
have hcd : SimpleEdges.Adj c d := by
  use hd.2.2.1
  intro e he
  have : 0 ≤ dist e d := dist_nonneg
  have : dist e d = 0 := by linarith [he.dist, this, hdmin e (hd.right_cancel he)]
  simp only [dist_eq_zero] at this
  exact he.ne23 this
Proof state after:
case intro.intro
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z : V
h : ∃ x y z, SimpleTriangle x y z
S✝ : Set (V × V × V) := {(x, y, z) | SimpleTriangle x y z}
this : S✝.Nonempty
b d✝ a c : V
habc : SimpleTriangle a b c
hmin : ∀ (a' b' c' : V), SimpleTriangle a' b' c' → Delta a b c ≤ Delta a' b' c'
h3 : Line a c ≠ {a, c}
hd✝ : d✝ ∈ Line a c
acd : sbtw a c d✝
S : Set V := setOf (sbtw a c)
d : V
hd : sbtw a c d
hbd' : b ≠ d
hdmin : ∀ (d' : V), sbtw a c d' → dist c d ≤ dist c d'
hcd : SimpleEdges.Adj c d
⊢ False
Theorem: two_implies_three
Proof state before:
case intro.intro
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z : V
h : ∃ x y z, SimpleTriangle x y z
S✝ : Set (V × V × V) := {(x, y, z) | SimpleTriangle x y z}
this : S✝.Nonempty
b d✝ a c : V
habc : SimpleTriangle a b c
hmin : ∀ (a' b' c' : V), SimpleTriangle a' b' c' → Delta a b c ≤ Delta a' b' c'
h3 : Line a c ≠ {a, c}
hd✝ : d✝ ∈ Line a c
acd : sbtw a c d✝
S : Set V := setOf (sbtw a c)
d : V
hd : sbtw a c d
hbd' : b ≠ d
hdmin : ∀ (d' : V), sbtw a c d' → dist c d ≤ dist c d'
hcd : SimpleEdges.Adj c d
⊢ False
Tactic:
have hbd := eqn_7 habc hmin hd hcd
Proof state after:
case intro.intro
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z : V
h : ∃ x y z, SimpleTriangle x y z
S✝ : Set (V × V × V) := {(x, y, z) | SimpleTriangle x y z}
this : S✝.Nonempty
b d✝ a c : V
habc : SimpleTriangle a b c
hmin : ∀ (a' b' c' : V), SimpleTriangle a' b' c' → Delta a b c ≤ Delta a' b' c'
h3 : Line a c ≠ {a, c}
hd✝ : d✝ ∈ Line a c
acd : sbtw a c d✝
S : Set V := setOf (sbtw a c)
d : V
hd : sbtw a c d
hbd' : b ≠ d
hdmin : ∀ (d' : V), sbtw a c d' → dist c d ≤ dist c d'
hcd : SimpleEdges.Adj c d
hbd : ¬SimpleEdges.Adj b d
⊢ False
Theorem: two_implies_three
Proof state before:
case intro.intro
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z : V
h : ∃ x y z, SimpleTriangle x y z
S✝ : Set (V × V × V) := {(x, y, z) | SimpleTriangle x y z}
this : S✝.Nonempty
b d✝ a c : V
habc : SimpleTriangle a b c
hmin : ∀ (a' b' c' : V), SimpleTriangle a' b' c' → Delta a b c ≤ Delta a' b' c'
h3 : Line a c ≠ {a, c}
hd✝ : d✝ ∈ Line a c
acd : sbtw a c d✝
S : Set V := setOf (sbtw a c)
d : V
hd : sbtw a c d
hbd' : b ≠ d
hdmin : ∀ (d' : V), sbtw a c d' → dist c d ≤ dist c d'
hcd : SimpleEdges.Adj c d
hbd : ¬SimpleEdges.Adj b d
⊢ False
Tactic:
let S : Set (List V) := setOf (List.Special a b d)
Proof state after:
case intro.intro
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z : V
h : ∃ x y z, SimpleTriangle x y z
S✝¹ : Set (V × V × V) := {(x, y, z) | SimpleTriangle x y z}
this : S✝¹.Nonempty
b d✝ a c : V
habc : SimpleTriangle a b c
hmin : ∀ (a' b' c' : V), SimpleTriangle a' b' c' → Delta a b c ≤ Delta a' b' c'
h3 : Line a c ≠ {a, c}
hd✝ : d✝ ∈ Line a c
acd : sbtw a c d✝
S✝ : Set V := setOf (sbtw a c)
d : V
hd : sbtw a c d
hbd' : b ≠ d
hdmin : ∀ (d' : V), sbtw a c d' → dist c d ≤ dist c d'
hcd : SimpleEdges.Adj c d
hbd : ¬SimpleEdges.Adj b d
S : Set (List V) := setOf (List.Special a b d)
⊢ False
Theorem: two_implies_three
Proof state before:
case intro.intro
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z : V
h : ∃ x y z, SimpleTriangle x y z
S✝¹ : Set (V × V × V) := {(x, y, z) | SimpleTriangle x y z}
this : S✝¹.Nonempty
b d✝ a c : V
habc : SimpleTriangle a b c
hmin : ∀ (a' b' c' : V), SimpleTriangle a' b' c' → Delta a b c ≤ Delta a' b' c'
h3 : Line a c ≠ {a, c}
hd✝ : d✝ ∈ Line a c
acd : sbtw a c d✝
S✝ : Set V := setOf (sbtw a c)
d : V
hd : sbtw a c d
hbd' : b ≠ d
hdmin : ∀ (d' : V), sbtw a c d' → dist c d ≤ dist c d'
hcd : SimpleEdges.Adj c d
hbd : ¬SimpleEdges.Adj b d
S : Set (List V) := setOf (List.Special a b d)
⊢ False
Tactic:
have : S.Finite := by
  have ⟨n, hn⟩ := uniformly_bounded_of_chain_ne_of_pathLength_le V [a, b, d].pathLength
  exact (List.finite_length_le _ _).subset fun l hl => hn l hl.chain_ne hl.pathLength_le
Proof state after:
case intro.intro
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z : V
h : ∃ x y z, SimpleTriangle x y z
S✝¹ : Set (V × V × V) := {(x, y, z) | SimpleTriangle x y z}
this✝ : S✝¹.Nonempty
b d✝ a c : V
habc : SimpleTriangle a b c
hmin : ∀ (a' b' c' : V), SimpleTriangle a' b' c' → Delta a b c ≤ Delta a' b' c'
h3 : Line a c ≠ {a, c}
hd✝ : d✝ ∈ Line a c
acd : sbtw a c d✝
S✝ : Set V := setOf (sbtw a c)
d : V
hd : sbtw a c d
hbd' : b ≠ d
hdmin : ∀ (d' : V), sbtw a c d' → dist c d ≤ dist c d'
hcd : SimpleEdges.Adj c d
hbd : ¬SimpleEdges.Adj b d
S : Set (List V) := setOf (List.Special a b d)
this : S.Finite
⊢ False
Theorem: two_implies_three
Proof state before:
case intro.intro
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z : V
h : ∃ x y z, SimpleTriangle x y z
S✝¹ : Set (V × V × V) := {(x, y, z) | SimpleTriangle x y z}
this✝ : S✝¹.Nonempty
b d✝ a c : V
habc : SimpleTriangle a b c
hmin : ∀ (a' b' c' : V), SimpleTriangle a' b' c' → Delta a b c ≤ Delta a' b' c'
h3 : Line a c ≠ {a, c}
hd✝ : d✝ ∈ Line a c
acd : sbtw a c d✝
S✝ : Set V := setOf (sbtw a c)
d : V
hd : sbtw a c d
hbd' : b ≠ d
hdmin : ∀ (d' : V), sbtw a c d' → dist c d ≤ dist c d'
hcd : SimpleEdges.Adj c d
hbd : ¬SimpleEdges.Adj b d
S : Set (List V) := setOf (List.Special a b d)
this : S.Finite
⊢ False
Tactic:
have ⟨P, (hP : P.Special a b d), hPmin⟩ :=
  this.exists_minimal_wrt List.pathLength S ⟨[a, b, d], abd_special habc hd hbd' hbd⟩
Proof state after:
case intro.intro
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z : V
h : ∃ x y z, SimpleTriangle x y z
S✝¹ : Set (V × V × V) := {(x, y, z) | SimpleTriangle x y z}
this✝ : S✝¹.Nonempty
b d✝ a c : V
habc : SimpleTriangle a b c
hmin : ∀ (a' b' c' : V), SimpleTriangle a' b' c' → Delta a b c ≤ Delta a' b' c'
h3 : Line a c ≠ {a, c}
hd✝ : d✝ ∈ Line a c
acd : sbtw a c d✝
S✝ : Set V := setOf (sbtw a c)
d : V
hd : sbtw a c d
hbd' : b ≠ d
hdmin : ∀ (d' : V), sbtw a c d' → dist c d ≤ dist c d'
hcd : SimpleEdges.Adj c d
hbd : ¬SimpleEdges.Adj b d
S : Set (List V) := setOf (List.Special a b d)
this : S.Finite
P : List V
hP : List.Special a b d P
hPmin : ∀ a' ∈ S, a'.pathLength ≤ P.pathLength → P.pathLength = a'.pathLength
⊢ False
Theorem: two_implies_three
Proof state before:
case intro.intro
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z : V
h : ∃ x y z, SimpleTriangle x y z
S✝¹ : Set (V × V × V) := {(x, y, z) | SimpleTriangle x y z}
this✝ : S✝¹.Nonempty
b d✝ a c : V
habc : SimpleTriangle a b c
hmin : ∀ (a' b' c' : V), SimpleTriangle a' b' c' → Delta a b c ≤ Delta a' b' c'
h3 : Line a c ≠ {a, c}
hd✝ : d✝ ∈ Line a c
acd : sbtw a c d✝
S✝ : Set V := setOf (sbtw a c)
d : V
hd : sbtw a c d
hbd' : b ≠ d
hdmin : ∀ (d' : V), sbtw a c d' → dist c d ≤ dist c d'
hcd : SimpleEdges.Adj c d
hbd : ¬SimpleEdges.Adj b d
S : Set (List V) := setOf (List.Special a b d)
this : S.Finite
P : List V
hP : List.Special a b d P
hPmin : ∀ a' ∈ S, a'.pathLength ≤ P.pathLength → P.pathLength = a'.pathLength
⊢ False
Tactic:
replace hPmin : ∀ P' : List V, P'.Special a b d → P.pathLength ≤ P'.pathLength := by
  intro P' hP'
  by_contra! h
  exact h.ne' (hPmin P' hP' h.le)
Proof state after:
case intro.intro
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z : V
h : ∃ x y z, SimpleTriangle x y z
S✝¹ : Set (V × V × V) := {(x, y, z) | SimpleTriangle x y z}
this✝ : S✝¹.Nonempty
b d✝ a c : V
habc : SimpleTriangle a b c
hmin : ∀ (a' b' c' : V), SimpleTriangle a' b' c' → Delta a b c ≤ Delta a' b' c'
h3 : Line a c ≠ {a, c}
hd✝ : d✝ ∈ Line a c
acd : sbtw a c d✝
S✝ : Set V := setOf (sbtw a c)
d : V
hd : sbtw a c d
hbd' : b ≠ d
hdmin : ∀ (d' : V), sbtw a c d' → dist c d ≤ dist c d'
hcd : SimpleEdges.Adj c d
hbd : ¬SimpleEdges.Adj b d
S : Set (List V) := setOf (List.Special a b d)
this : S.Finite
P : List V
hP : List.Special a b d P
hPmin : ∀ (P' : List V), List.Special a b d P' → P.pathLength ≤ P'.pathLength
⊢ False
Theorem: two_implies_three
Proof state before:
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z : V
h : ∃ x y z, SimpleTriangle x y z
S : Set (V × V × V) := {(x, y, z) | SimpleTriangle x y z}
this : S.Nonempty
a b c : V
habc : SimpleTriangle a b c
hmin :
  ∀ a' ∈ S,
    ((match a' with
        | (x, y, z) => Delta x y z) ≤
        match (a, b, c) with
        | (x, y, z) => Delta x y z) →
      (match (a, b, c) with
        | (x, y, z) => Delta x y z) =
        match a' with
        | (x, y, z) => Delta x y z
⊢ ∀ (a' b' c' : V), SimpleTriangle a' b' c' → Delta a b c ≤ Delta a' b' c'
Tactic:
intro a' b' c' h
Proof state after:
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z : V
h✝ : ∃ x y z, SimpleTriangle x y z
S : Set (V × V × V) := {(x, y, z) | SimpleTriangle x y z}
this : S.Nonempty
a b c : V
habc : SimpleTriangle a b c
hmin :
  ∀ a' ∈ S,
    ((match a' with
        | (x, y, z) => Delta x y z) ≤
        match (a, b, c) with
        | (x, y, z) => Delta x y z) →
      (match (a, b, c) with
        | (x, y, z) => Delta x y z) =
        match a' with
        | (x, y, z) => Delta x y z
a' b' c' : V
h : SimpleTriangle a' b' c'
⊢ Delta a b c ≤ Delta a' b' c'
Theorem: two_implies_three
Proof state before:
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z : V
h✝ : ∃ x y z, SimpleTriangle x y z
S : Set (V × V × V) := {(x, y, z) | SimpleTriangle x y z}
this : S.Nonempty
a b c : V
habc : SimpleTriangle a b c
hmin :
  ∀ a' ∈ S,
    ((match a' with
        | (x, y, z) => Delta x y z) ≤
        match (a, b, c) with
        | (x, y, z) => Delta x y z) →
      (match (a, b, c) with
        | (x, y, z) => Delta x y z) =
        match a' with
        | (x, y, z) => Delta x y z
a' b' c' : V
h : SimpleTriangle a' b' c'
⊢ Delta a b c ≤ Delta a' b' c'
Tactic:
by_contra! h'
Proof state after:
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z : V
h✝ : ∃ x y z, SimpleTriangle x y z
S : Set (V × V × V) := {(x, y, z) | SimpleTriangle x y z}
this : S.Nonempty
a b c : V
habc : SimpleTriangle a b c
hmin :
  ∀ a' ∈ S,
    ((match a' with
        | (x, y, z) => Delta x y z) ≤
        match (a, b, c) with
        | (x, y, z) => Delta x y z) →
      (match (a, b, c) with
        | (x, y, z) => Delta x y z) =
        match a' with
        | (x, y, z) => Delta x y z
a' b' c' : V
h : SimpleTriangle a' b' c'
h' : Delta a' b' c' < Delta a b c
⊢ False
Theorem: two_implies_three
Proof state before:
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z : V
h✝ : ∃ x y z, SimpleTriangle x y z
S : Set (V × V × V) := {(x, y, z) | SimpleTriangle x y z}
this : S.Nonempty
a b c : V
habc : SimpleTriangle a b c
hmin :
  ∀ a' ∈ S,
    ((match a' with
        | (x, y, z) => Delta x y z) ≤
        match (a, b, c) with
        | (x, y, z) => Delta x y z) →
      (match (a, b, c) with
        | (x, y, z) => Delta x y z) =
        match a' with
        | (x, y, z) => Delta x y z
a' b' c' : V
h : SimpleTriangle a' b' c'
h' : Delta a' b' c' < Delta a b c
⊢ False
Tactic:
exact h'.ne' (hmin (a', b', c') h h'.le)
Proof state after:
no goals
Theorem: two_implies_three
Proof state before:
case intro.mk.mk.intro.intro.intro.inr
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z : V
h : ∃ x y z, SimpleTriangle x y z
S : Set (V × V × V) := {(x, y, z) | SimpleTriangle x y z}
this✝ : S.Nonempty
a b c : V
habc : SimpleTriangle a b c
hmin : ∀ (a' b' c' : V), SimpleTriangle a' b' c' → Delta a b c ≤ Delta a' b' c'
h3 : Line a c ≠ {a, c}
d : V
hd : d ∈ Line a c
hd' : sbtw d a c ∨ sbtw a c d
this :
  ∀ (a c : V),
    SimpleTriangle a b c →
      (∀ (a' b' c' : V), SimpleTriangle a' b' c' → Delta a b c ≤ Delta a' b' c') →
        Line a c ≠ {a, c} → d ∈ Line a c → sbtw d a c ∨ sbtw a c d → sbtw a c d → False
acd : ¬sbtw a c d
⊢ False
Tactic:
rw [Line_comm] at hd h3
Proof state after:
case intro.mk.mk.intro.intro.intro.inr
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z : V
h : ∃ x y z, SimpleTriangle x y z
S : Set (V × V × V) := {(x, y, z) | SimpleTriangle x y z}
this✝ : S.Nonempty
a b c : V
habc : SimpleTriangle a b c
hmin : ∀ (a' b' c' : V), SimpleTriangle a' b' c' → Delta a b c ≤ Delta a' b' c'
h3 : Line c a ≠ {a, c}
d : V
hd : d ∈ Line c a
hd' : sbtw d a c ∨ sbtw a c d
this :
  ∀ (a c : V),
    SimpleTriangle a b c →
      (∀ (a' b' c' : V), SimpleTriangle a' b' c' → Delta a b c ≤ Delta a' b' c') →
        Line a c ≠ {a, c} → d ∈ Line a c → sbtw d a c ∨ sbtw a c d → sbtw a c d → False
acd : ¬sbtw a c d
⊢ False