internlm/Lean-Github huggingface dataset:
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 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
Tactic:
rw [Set.pair_comm] at 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 ≠ {c, a}
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
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 c a ≠ {c, a}
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
Tactic:
have h' := hd'.resolve_right acd
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 ≠ {c, a}
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
h' : sbtw d a c
⊢ False
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 c a ≠ {c, a}
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
h' : sbtw d a c
⊢ False
Tactic:
refine this c a habc.swap ?_ h3 hd (Or.inr h'.symm) h'.symm
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 ≠ {c, a}
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
h' : sbtw d a c
⊢ ∀ (a' b' c' : V), SimpleTriangle a' b' c' → Delta c b a ≤ Delta a' b' c'
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 c a ≠ {c, a}
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
h' : sbtw d a c
⊢ ∀ (a' b' c' : V), SimpleTriangle a' b' c' → Delta c b a ≤ Delta a' b' c'
Tactic:
intro a' b' c' h'
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 ≠ {c, a}
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
h'✝ : sbtw d a c
a' b' c' : V
h' : SimpleTriangle a' b' c'
⊢ Delta c b a ≤ Delta a' b' c'
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 c a ≠ {c, a}
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
h'✝ : sbtw d a c
a' b' c' : V
h' : SimpleTriangle a' b' c'
⊢ Delta c b a ≤ Delta a' b' c'
Tactic:
rw [Delta_comm]
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 ≠ {c, a}
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
h'✝ : sbtw d a c
a' b' c' : V
h' : SimpleTriangle a' b' c'
⊢ Delta a b c ≤ Delta a' b' c'
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 c a ≠ {c, a}
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
h'✝ : sbtw d a c
a' b' c' : V
h' : SimpleTriangle a' b' c'
⊢ Delta a b c ≤ Delta a' b' c'
Tactic:
exact hmin _ _ _ h'
Proof state after:
no goals
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)
d : V
hd : sbtw a c d
hdmin : ∀ a' ∈ S, dist c a' ≤ dist c d → dist c d = dist c a'
⊢ b ≠ d
Tactic:
rintro rfl
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)
hd : sbtw a c b
hdmin : ∀ a' ∈ S, dist c a' ≤ dist c b → dist c b = dist c a'
⊢ 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)
hd : sbtw a c b
hdmin : ∀ a' ∈ S, dist c a' ≤ dist c b → dist c b = dist c a'
⊢ False
Tactic:
have := habc.2.2.2.2.2.2 (Line a c) (Line_isLine hd.ne12)
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)
hd : sbtw a c b
hdmin : ∀ a' ∈ S, dist c a' ≤ dist c b → dist c b = dist c a'
this : ¬{a, b, c} ⊆ Line 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)
hd : sbtw a c b
hdmin : ∀ a' ∈ S, dist c a' ≤ dist c b → dist c b = dist c a'
this : ¬{a, b, c} ⊆ Line a c
⊢ False
Tactic:
simp [right_extend_mem_Line hd] at this
Proof state after:
no goals
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)
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
⊢ ∀ (d' : V), sbtw a c d' → dist c d ≤ dist c d'
Tactic:
intro d' 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✝
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
d' : V
hd' : sbtw a c d'
⊢ dist c d ≤ dist c d'
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)
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
d' : V
hd' : sbtw a c d'
⊢ dist c d ≤ dist c d'
Tactic:
by_contra! 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✝
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
d' : V
hd' : sbtw a c d'
hd'' : dist c d' < dist 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✝
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
d' : V
hd' : sbtw a c d'
hd'' : dist c d' < dist c d
⊢ False
Tactic:
exact hd''.ne' (hdmin d' hd' hd''.le)
Proof state after:
no goals
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)
d : V
hd : sbtw a c d
hbd' : b ≠ d
hdmin : ∀ (d' : V), sbtw a c d' → dist c d ≤ dist c d'
⊢ SimpleEdges.Adj c d
Tactic:
use hd.2.2.1
Proof state after:
case right
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'
⊢ ∀ (x : V), ¬sbtw c x d
Theorem: two_implies_three
Proof state before:
case right
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'
⊢ ∀ (x : V), ¬sbtw c x d
Tactic:
intro e he
Proof state after:
case right
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'
e : V
he : sbtw c e d
⊢ False
Theorem: two_implies_three
Proof state before:
case right
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'
e : V
he : sbtw c e d
⊢ False
Tactic:
have : 0 ≤ dist e d := dist_nonneg
Proof state after:
case right
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'
e : V
he : sbtw c e d
this : 0 ≤ dist e d
⊢ False
Theorem: two_implies_three
Proof state before:
case right
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'
e : V
he : sbtw c e d
this : 0 ≤ dist e d
⊢ False
Tactic:
have : dist e d = 0 := by linarith [he.dist, this, hdmin e (hd.right_cancel he)]
Proof state after:
case right
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'
e : V
he : sbtw c e d
this✝ : 0 ≤ dist e d
this : dist e d = 0
⊢ False
Theorem: two_implies_three
Proof state before:
case right
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'
e : V
he : sbtw c e d
this✝ : 0 ≤ dist e d
this : dist e d = 0
⊢ False
Tactic:
simp only [dist_eq_zero] at this
Proof state after:
case right
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'
e : V
he : sbtw c e d
this✝ : 0 ≤ dist e d
this : e = d
⊢ False
Theorem: two_implies_three
Proof state before:
case right
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'
e : V
he : sbtw c e d
this✝ : 0 ≤ dist e d
this : e = d
⊢ False
Tactic:
exact he.ne23 this
Proof state after:
no goals
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)
d : V
hd : sbtw a c d
hbd' : b ≠ d
hdmin : ∀ (d' : V), sbtw a c d' → dist c d ≤ dist c d'
e : V
he : sbtw c e d
this : 0 ≤ dist e d
⊢ dist e d = 0
Tactic:
linarith [he.dist, this, hdmin e (hd.right_cancel he)]
Proof state after:
no goals
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)
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)
⊢ S.Finite
Tactic:
have ⟨n, hn⟩ := uniformly_bounded_of_chain_ne_of_pathLength_le V [a, b, d].pathLength
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)
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)
n : ℕ
hn : ∀ (l : List V), List.Chain' (fun x x_1 => x ≠ x_1) l → l.pathLength ≤ [a, b, d].pathLength → l.length ≤ n
⊢ S.Finite