internlm/Lean-Github huggingface dataset:
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)
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
Tactic:
exact (List.finite_length_le _ _).subset fun l hl => hn l hl.chain_ne hl.pathLength_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'
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
⊢ ∀ (P' : List V), List.Special a b d P' → P.pathLength ≤ P'.pathLength
Tactic:
intro P' hP'
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)
this : S.Finite
P : List V
hP : List.Special a b d P
hPmin : ∀ a' ∈ S, a'.pathLength ≤ P.pathLength → P.pathLength = a'.pathLength
P' : List V
hP' : List.Special a b d P'
⊢ P.pathLength ≤ P'.pathLength
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)
this : S.Finite
P : List V
hP : List.Special a b d P
hPmin : ∀ a' ∈ S, a'.pathLength ≤ P.pathLength → P.pathLength = a'.pathLength
P' : List V
hP' : List.Special a b d P'
⊢ P.pathLength ≤ P'.pathLength
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
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
P' : List V
hP' : List.Special a b d P'
h : 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
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
P' : List V
hP' : List.Special a b d P'
h : P'.pathLength < P.pathLength
⊢ False
Tactic:
exact h.ne' (hPmin P' hP' h.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'
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
a₁ a₂ a₃ : V
l : List V
hP : List.Special a b d (a₁ :: a₂ :: a₃ :: l)
hPmin : ∀ (P' : List V), List.Special a b d P' → (a₁ :: a₂ :: a₃ :: l).pathLength ≤ P'.pathLength
⊢ False
Tactic:
simp only [List.Special] at hP
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)
this : S.Finite
P : List V
a₁ a₂ a₃ : V
l : List V
hP :
  a₁ = a ∧
    NotCollinear a₁ a₂ a₃ ∧
      (¬SimpleEdges.Adj a₁ a₂ ∨ ¬SimpleEdges.Adj a₂ a₃) ∧
        (a₁ :: a₂ :: a₃ :: l).getLast ⋯ = d ∧
          List.Chain' (fun x x_1 => x ≠ x_1) (a₁ :: a₂ :: a₃ :: l) ∧
            (a₁ :: a₂ :: a₃ :: l).pathLength ≤ [a, b, d].pathLength
hPmin : ∀ (P' : List V), List.Special a b d P' → (a₁ :: a₂ :: a₃ :: l).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
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
a₁ a₂ a₃ : V
l : List V
hP :
  a₁ = a ∧
    NotCollinear a₁ a₂ a₃ ∧
      (¬SimpleEdges.Adj a₁ a₂ ∨ ¬SimpleEdges.Adj a₂ a₃) ∧
        (a₁ :: a₂ :: a₃ :: l).getLast ⋯ = d ∧
          List.Chain' (fun x x_1 => x ≠ x_1) (a₁ :: a₂ :: a₃ :: l) ∧
            (a₁ :: a₂ :: a₃ :: l).pathLength ≤ [a, b, d].pathLength
hPmin : ∀ (P' : List V), List.Special a b d P' → (a₁ :: a₂ :: a₃ :: l).pathLength ≤ P'.pathLength
⊢ False
Tactic:
rcases hP with ⟨ha₁, hα, hβ, hPd, hPc, _⟩
Proof state after:
case intro.intro.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
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
a₁ a₂ a₃ : V
l : List V
hPmin : ∀ (P' : List V), List.Special a b d P' → (a₁ :: a₂ :: a₃ :: l).pathLength ≤ P'.pathLength
ha₁ : a₁ = a
hα : NotCollinear a₁ a₂ a₃
hβ : ¬SimpleEdges.Adj a₁ a₂ ∨ ¬SimpleEdges.Adj a₂ a₃
hPd : (a₁ :: a₂ :: a₃ :: l).getLast ⋯ = d
hPc : List.Chain' (fun x x_1 => x ≠ x_1) (a₁ :: a₂ :: a₃ :: l)
right✝ : (a₁ :: a₂ :: a₃ :: l).pathLength ≤ [a, b, d].pathLength
⊢ False
Theorem: two_implies_three
Proof state before:
case intro.intro.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
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
a₁ a₂ a₃ : V
l : List V
hPmin : ∀ (P' : List V), List.Special a b d P' → (a₁ :: a₂ :: a₃ :: l).pathLength ≤ P'.pathLength
ha₁ : a₁ = a
hα : NotCollinear a₁ a₂ a₃
hβ : ¬SimpleEdges.Adj a₁ a₂ ∨ ¬SimpleEdges.Adj a₂ a₃
hPd : (a₁ :: a₂ :: a₃ :: l).getLast ⋯ = d
hPc : List.Chain' (fun x x_1 => x ≠ x_1) (a₁ :: a₂ :: a₃ :: l)
right✝ : (a₁ :: a₂ :: a₃ :: l).pathLength ≤ [a, b, d].pathLength
⊢ False
Tactic:
have : (¬ SimpleEdges.Adj a₁ a₂ ∧ ¬ SimpleEdges.Adj a₂ a₃) ∨
      (SimpleEdges.Adj a₁ a₂ ∧ ¬ SimpleEdges.Adj a₂ a₃) ∨
      (¬ SimpleEdges.Adj a₁ a₂ ∧ SimpleEdges.Adj a₂ a₃) := by tauto
Proof state after:
case intro.intro.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
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
a₁ a₂ a₃ : V
l : List V
hPmin : ∀ (P' : List V), List.Special a b d P' → (a₁ :: a₂ :: a₃ :: l).pathLength ≤ P'.pathLength
ha₁ : a₁ = a
hα : NotCollinear a₁ a₂ a₃
hβ : ¬SimpleEdges.Adj a₁ a₂ ∨ ¬SimpleEdges.Adj a₂ a₃
hPd : (a₁ :: a₂ :: a₃ :: l).getLast ⋯ = d
hPc : List.Chain' (fun x x_1 => x ≠ x_1) (a₁ :: a₂ :: a₃ :: l)
right✝ : (a₁ :: a₂ :: a₃ :: l).pathLength ≤ [a, b, d].pathLength
this :
  ¬SimpleEdges.Adj a₁ a₂ ∧ ¬SimpleEdges.Adj a₂ a₃ ∨
    SimpleEdges.Adj a₁ a₂ ∧ ¬SimpleEdges.Adj a₂ a₃ ∨ ¬SimpleEdges.Adj a₁ a₂ ∧ SimpleEdges.Adj a₂ 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)
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
a₁ a₂ a₃ : V
l : List V
hPmin : ∀ (P' : List V), List.Special a b d P' → (a₁ :: a₂ :: a₃ :: l).pathLength ≤ P'.pathLength
ha₁ : a₁ = a
hα : NotCollinear a₁ a₂ a₃
hβ : ¬SimpleEdges.Adj a₁ a₂ ∨ ¬SimpleEdges.Adj a₂ a₃
hPd : (a₁ :: a₂ :: a₃ :: l).getLast ⋯ = d
hPc : List.Chain' (fun x x_1 => x ≠ x_1) (a₁ :: a₂ :: a₃ :: l)
right✝ : (a₁ :: a₂ :: a₃ :: l).pathLength ≤ [a, b, d].pathLength
⊢ ¬SimpleEdges.Adj a₁ a₂ ∧ ¬SimpleEdges.Adj a₂ a₃ ∨
    SimpleEdges.Adj a₁ a₂ ∧ ¬SimpleEdges.Adj a₂ a₃ ∨ ¬SimpleEdges.Adj a₁ a₂ ∧ SimpleEdges.Adj a₂ a₃
Tactic:
tauto
Proof state after:
no goals
Theorem: two_implies_three
Proof state before:
case intro.intro.intro.intro.intro.inl.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
a₁ a₂ a₃ : V
l : List V
hPmin : ∀ (P' : List V), List.Special a b d P' → (a₁ :: a₂ :: a₃ :: l).pathLength ≤ P'.pathLength
ha₁ : a₁ = a
hα : NotCollinear a₁ a₂ a₃
hβ : ¬SimpleEdges.Adj a₁ a₂ ∨ ¬SimpleEdges.Adj a₂ a₃
hPd : (a₁ :: a₂ :: a₃ :: l).getLast ⋯ = d
hPc : List.Chain' (fun x x_1 => x ≠ x_1) (a₁ :: a₂ :: a₃ :: l)
right✝ : (a₁ :: a₂ :: a₃ :: l).pathLength ≤ [a, b, d].pathLength
c₁1 : ¬SimpleEdges.Adj a₁ a₂
c₁2 : ¬SimpleEdges.Adj a₂ a₃
⊢ False
Tactic:
exact case1 habc hmin hd hbd' hbd hPmin ha₁ hα hPd hPc c₁1 c₁2
Proof state after:
no goals
Theorem: two_implies_three
Proof state before:
case intro.intro.intro.intro.intro.inr.inl.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
a₁ a₂ a₃ : V
l : List V
hPmin : ∀ (P' : List V), List.Special a b d P' → (a₁ :: a₂ :: a₃ :: l).pathLength ≤ P'.pathLength
ha₁ : a₁ = a
hα : NotCollinear a₁ a₂ a₃
hβ : ¬SimpleEdges.Adj a₁ a₂ ∨ ¬SimpleEdges.Adj a₂ a₃
hPd : (a₁ :: a₂ :: a₃ :: l).getLast ⋯ = d
hPc : List.Chain' (fun x x_1 => x ≠ x_1) (a₁ :: a₂ :: a₃ :: l)
right✝ : (a₁ :: a₂ :: a₃ :: l).pathLength ≤ [a, b, d].pathLength
c₂1 : SimpleEdges.Adj a₁ a₂
c₂2 : ¬SimpleEdges.Adj a₂ a₃
⊢ False
Tactic:
exact case2 habc hmin hd hbd' hbd hPmin ha₁ hα hPd hPc c₂1 c₂2
Proof state after:
no goals
Theorem: two_implies_three
Proof state before:
case intro.intro.intro.intro.intro.inr.inr.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
a₁ a₂ a₃ : V
l : List V
hPmin : ∀ (P' : List V), List.Special a b d P' → (a₁ :: a₂ :: a₃ :: l).pathLength ≤ P'.pathLength
ha₁ : a₁ = a
hα : NotCollinear a₁ a₂ a₃
hβ : ¬SimpleEdges.Adj a₁ a₂ ∨ ¬SimpleEdges.Adj a₂ a₃
hPd : (a₁ :: a₂ :: a₃ :: l).getLast ⋯ = d
hPc : List.Chain' (fun x x_1 => x ≠ x_1) (a₁ :: a₂ :: a₃ :: l)
right✝ : (a₁ :: a₂ :: a₃ :: l).pathLength ≤ [a, b, d].pathLength
c₃1 : ¬SimpleEdges.Adj a₁ a₂
c₃2 : SimpleEdges.Adj a₂ a₃
⊢ False
Tactic:
exact case3 habc hmin hd hbd' hbd hPmin ha₁ hα hPd hPc c₃1 c₃2
Proof state after:
no goals
Theorem: sylvester_chvatal
Proof state before:
V✝ : Type u_1
inst✝⁵ : MetricSpace V✝
u v w : V✝
inst✝⁴ : Finite V✝
inst✝³ : Nontrivial V✝
x y z : V✝
V : Type u_2
inst✝² : MetricSpace V
inst✝¹ : Nontrivial V
inst✝ : Finite V
⊢ ∃ a b, a ≠ b ∧ (Line a b = {a, b} ∨ Line a b = Set.univ)
Tactic:
by_cases h : ∀ x y z : V, ¬ NotCollinear x y z
Proof state after:
case pos
V✝ : Type u_1
inst✝⁵ : MetricSpace V✝
u v w : V✝
inst✝⁴ : Finite V✝
inst✝³ : Nontrivial V✝
x y z : V✝
V : Type u_2
inst✝² : MetricSpace V
inst✝¹ : Nontrivial V
inst✝ : Finite V
h : ∀ (x y z : V), ¬NotCollinear x y z
⊢ ∃ a b, a ≠ b ∧ (Line a b = {a, b} ∨ Line a b = Set.univ)

case neg
V✝ : Type u_1
inst✝⁵ : MetricSpace V✝
u v w : V✝
inst✝⁴ : Finite V✝
inst✝³ : Nontrivial V✝
x y z : V✝
V : Type u_2
inst✝² : MetricSpace V
inst✝¹ : Nontrivial V
inst✝ : Finite V
h : ¬∀ (x y z : V), ¬NotCollinear x y z
⊢ ∃ a b, a ≠ b ∧ (Line a b = {a, b} ∨ Line a b = Set.univ)
Theorem: sylvester_chvatal
Proof state before:
case neg
V✝ : Type u_1
inst✝⁵ : MetricSpace V✝
u v w : V✝
inst✝⁴ : Finite V✝
inst✝³ : Nontrivial V✝
x y z : V✝
V : Type u_2
inst✝² : MetricSpace V
inst✝¹ : Nontrivial V
inst✝ : Finite V
h : ¬∀ (x y z : V), ¬NotCollinear x y z
⊢ ∃ a b, a ≠ b ∧ (Line a b = {a, b} ∨ Line a b = Set.univ)
Tactic:
push_neg at h
Proof state after:
case neg
V✝ : Type u_1
inst✝⁵ : MetricSpace V✝
u v w : V✝
inst✝⁴ : Finite V✝
inst✝³ : Nontrivial V✝
x y z : V✝
V : Type u_2
inst✝² : MetricSpace V
inst✝¹ : Nontrivial V
inst✝ : Finite V
h : ∃ x y z, NotCollinear x y z
⊢ ∃ a b, a ≠ b ∧ (Line a b = {a, b} ∨ Line a b = Set.univ)
Theorem: sylvester_chvatal
Proof state before:
case neg
V✝ : Type u_1
inst✝⁵ : MetricSpace V✝
u v w : V✝
inst✝⁴ : Finite V✝
inst✝³ : Nontrivial V✝
x y z : V✝
V : Type u_2
inst✝² : MetricSpace V
inst✝¹ : Nontrivial V
inst✝ : Finite V
h : ∃ x y z, NotCollinear x y z
⊢ ∃ a b, a ≠ b ∧ (Line a b = {a, b} ∨ Line a b = Set.univ)
Tactic:
replace h := one_implies_two h
Proof state after:
case neg
V✝ : Type u_1
inst✝⁵ : MetricSpace V✝
u v w : V✝
inst✝⁴ : Finite V✝
inst✝³ : Nontrivial V✝
x y z : V✝
V : Type u_2
inst✝² : MetricSpace V
inst✝¹ : Nontrivial V
inst✝ : Finite V
h : ∃ x y z, SimpleTriangle x y z
⊢ ∃ a b, a ≠ b ∧ (Line a b = {a, b} ∨ Line a b = Set.univ)
Theorem: sylvester_chvatal
Proof state before:
case neg
V✝ : Type u_1
inst✝⁵ : MetricSpace V✝
u v w : V✝
inst✝⁴ : Finite V✝
inst✝³ : Nontrivial V✝
x y z : V✝
V : Type u_2
inst✝² : MetricSpace V
inst✝¹ : Nontrivial V
inst✝ : Finite V
h : ∃ x y z, SimpleTriangle x y z
⊢ ∃ a b, a ≠ b ∧ (Line a b = {a, b} ∨ Line a b = Set.univ)
Tactic:
obtain ⟨a, b, h, hl⟩ := two_implies_three h
Proof state after:
case neg.intro.intro.intro
V✝ : Type u_1
inst✝⁵ : MetricSpace V✝
u v w : V✝
inst✝⁴ : Finite V✝
inst✝³ : Nontrivial V✝
x y z : V✝
V : Type u_2
inst✝² : MetricSpace V
inst✝¹ : Nontrivial V
inst✝ : Finite V
h✝ : ∃ x y z, SimpleTriangle x y z
a b : V
h : a ≠ b
hl : Line a b = {a, b}
⊢ ∃ a b, a ≠ b ∧ (Line a b = {a, b} ∨ Line a b = Set.univ)
Theorem: sylvester_chvatal
Proof state before:
case neg.intro.intro.intro
V✝ : Type u_1
inst✝⁵ : MetricSpace V✝
u v w : V✝
inst✝⁴ : Finite V✝
inst✝³ : Nontrivial V✝
x y z : V✝
V : Type u_2
inst✝² : MetricSpace V
inst✝¹ : Nontrivial V
inst✝ : Finite V
h✝ : ∃ x y z, SimpleTriangle x y z
a b : V
h : a ≠ b
hl : Line a b = {a, b}
⊢ ∃ a b, a ≠ b ∧ (Line a b = {a, b} ∨ Line a b = Set.univ)
Tactic:
exact ⟨a, b, h, Or.inl hl⟩
Proof state after:
no goals
Theorem: sylvester_chvatal
Proof state before:
case pos
V✝ : Type u_1
inst✝⁵ : MetricSpace V✝
u v w : V✝
inst✝⁴ : Finite V✝
inst✝³ : Nontrivial V✝
x y z : V✝
V : Type u_2
inst✝² : MetricSpace V
inst✝¹ : Nontrivial V
inst✝ : Finite V
h : ∀ (x y z : V), ¬NotCollinear x y z
⊢ ∃ a b, a ≠ b ∧ (Line a b = {a, b} ∨ Line a b = Set.univ)
Tactic:
obtain ⟨L, hL, a, b, hab, rfl⟩ := thm_two' h
Proof state after:
case pos.intro.intro.intro.intro.intro
V✝ : Type u_1
inst✝⁵ : MetricSpace V✝
u v w : V✝
inst✝⁴ : Finite V✝
inst✝³ : Nontrivial V✝
x y z : V✝
V : Type u_2
inst✝² : MetricSpace V
inst✝¹ : Nontrivial V
inst✝ : Finite V
h : ∀ (x y z : V), ¬NotCollinear x y z
a b : V
hab : a ≠ b
hL : Line a b = Set.univ
⊢ ∃ a b, a ≠ b ∧ (Line a b = {a, b} ∨ Line a b = Set.univ)
Theorem: sylvester_chvatal
Proof state before:
case pos.intro.intro.intro.intro.intro
V✝ : Type u_1
inst✝⁵ : MetricSpace V✝
u v w : V✝
inst✝⁴ : Finite V✝
inst✝³ : Nontrivial V✝
x y z : V✝
V : Type u_2
inst✝² : MetricSpace V
inst✝¹ : Nontrivial V
inst✝ : Finite V
h : ∀ (x y z : V), ¬NotCollinear x y z
a b : V
hab : a ≠ b
hL : Line a b = Set.univ
⊢ ∃ a b, a ≠ b ∧ (Line a b = {a, b} ∨ Line a b = Set.univ)
Tactic:
exact ⟨a, b, hab, Or.inr hL⟩
Proof state after:
no goals
Theorem: ErdosRenyi.meas
Proof state before:
α : Type u_1
Ω : Type u_2
inst✝⁵ : MeasurableSpace Ω
G : Ω → SimpleGraph α
H : SimpleGraph α
inst✝⁴ : (ω : Ω) → DecidableRel (G ω).Adj
p : ℝ≥0
μ : Measure Ω
inst✝³ : IsProbabilityMeasure μ
hG : ErdosRenyi G p μ
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel H.Adj
⊢ μ {ω | G ω = H} = ↑p ^ H.edgeFinset.card * (1 - ↑p) ^ (Fintype.card (Sym2 α) - H.edgeFinset.card)
Tactic:
simpa using hG.meas H.edgeFinset
Proof state after:
no goals
Theorem: convexHull_extremePoints
Proof state before:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
x : E
s B : Set E
hscomp : IsCompact s
hsconv : Convex ℝ s
⊢ (convexHull ℝ) (extremePoints ℝ s) = s
Tactic:
sorry
Proof state after:
no goals
Theorem: closed_convexHull_extremePoints_of_compact_of_convex
Proof state before:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
x : E
s B : Set E
hscomp : IsCompact s
hsconv : Convex ℝ s
⊢ closure ((convexHull ℝ) (extremePoints ℝ s)) = (convexHull ℝ) (extremePoints ℝ s)
Tactic:
rw [closure_convexHull_extremePoints hscomp hsconv, convexHull_extremePoints hscomp hsconv]
Proof state after:
no goals
Theorem: Real.closedBall_eq_segment
Proof state before:
ε r : ℝ
hε : 0 ≤ ε
⊢ closedBall r ε = segment ℝ (r - ε) (r + ε)
Tactic:
rw [closedBall_eq_Icc, segment_eq_Icc ((sub_le_self _ hε).trans $ le_add_of_nonneg_right hε)]
Proof state after:
no goals
Theorem: IsOpen.exists_mem_intrinsicInterior_convexHull_finset
Proof state before:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
x : E
hs : IsOpen (Subtype.val ⁻¹' s)
hx : x ∈ s
⊢ ∃ t, x ∈ intrinsicInterior ℝ ((convexHull ℝ) ↑t) ∧ (convexHull ℝ) ↑t ⊆ s
Tactic:
classical
lift x to affineSpan ℝ s using subset_affineSpan _ _ hx
set x : affineSpan ℝ s := x with hx
clear_value x
subst hx
obtain ⟨ε, hε, hεx⟩ := (Metric.nhds_basis_closedBall.1 _).1 (isOpen_iff_mem_nhds.1 hs _ hx)
set f : Finset (Fin $ finrank ℝ $ vectorSpan ℝ s) → vectorSpan ℝ s :=
  fun u ↦ (ε / ∑ i, ‖finBasis ℝ (vectorSpan ℝ s) i‖) • ∑ i, if i ∈ u then
    finBasis ℝ (vectorSpan ℝ s) i else -finBasis ℝ (vectorSpan ℝ s) i
    with hf
sorry
Proof state after:
no goals