internlm/Lean-Github huggingface dataset:
Theorem: eqn_7
Proof 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⟩
Proof 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
Theorem: eqn_7
Proof 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]
Proof 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
Theorem: eqn_7
Proof 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) ?_
Proof 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
Theorem: eqn_7
Proof 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]
Proof state after:
no goals
Theorem: eqn_7
Proof 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 ↦ ?_⟩
Proof 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
Theorem: eqn_7
Proof 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
Proof 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
Theorem: eqn_7
Proof 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])
Proof state after:
no goals
Theorem: eqn_7
Proof 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]
Proof state after:
no goals
Theorem: eqn_7
Proof 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 ?_
Proof 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
Theorem: eqn_7
Proof 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
Proof 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
Theorem: eqn_7
Proof 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
Proof 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
Theorem: eqn_7
Proof 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]
Proof state after:
no goals
Theorem: eqn_8
Proof 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
hacd : sbtw a c d
⊢ dist a b + dist b d < dist a d + Delta a b c
Tactic:
by_contra!
Proof 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
hacd : sbtw a c d
this : dist a d + Delta a b c ≤ dist a b + dist b d
⊢ False
Theorem: eqn_8
Proof 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
hacd : sbtw a c d
this : dist a d + Delta a b c ≤ dist a b + dist b d
⊢ False
Tactic:
have hbcd : sbtw b c d := by
  refine sbtw_mk habc.2.1.ne hacd.ne23 ?_
  rw [Delta] at this
  linarith [hacd.dist]
Proof 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
hacd : sbtw a c d
this : dist a d + Delta a b c ≤ dist a b + dist b d
hbcd : sbtw b c d
⊢ False
Theorem: eqn_8
Proof 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
hacd : sbtw a c d
this : dist a d + Delta a b c ≤ dist a b + dist b d
hbcd : sbtw b c d
⊢ False
Tactic:
refine habc.2.2.2.2.2.2 (Line c d) (Line_isLine hbcd.ne23) ?_
Proof 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
hacd : sbtw a c d
this : dist a d + Delta a b c ≤ dist a b + dist b d
hbcd : sbtw b c d
⊢ {a, b, c} ⊆ Line c d
Theorem: eqn_8
Proof 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
hacd : sbtw a c d
this : dist a d + Delta a b c ≤ dist a b + dist b d
hbcd : sbtw b c d
⊢ {a, b, c} ⊆ Line c d
Tactic:
simp [left_extend_mem_Line, hacd, hbcd]
Proof state after:
no goals
Theorem: eqn_8
Proof 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
hacd : sbtw a c d
this : dist a d + Delta a b c ≤ dist a b + dist b d
⊢ sbtw b c d
Tactic:
refine sbtw_mk habc.2.1.ne hacd.ne23 ?_
Proof 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
hacd : sbtw a c d
this : dist a d + Delta a b c ≤ dist a b + dist b d
⊢ dist b c + dist c d ≤ dist b d
Theorem: eqn_8
Proof 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
hacd : sbtw a c d
this : dist a d + Delta a b c ≤ dist a b + dist b d
⊢ dist b c + dist c d ≤ dist b d
Tactic:
rw [Delta] at this
Proof 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
hacd : sbtw a c d
this : dist a d + (dist a b + dist b c - dist a c) ≤ dist a b + dist b d
⊢ dist b c + dist c d ≤ dist b d
Theorem: eqn_8
Proof 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
hacd : sbtw a c d
this : dist a d + (dist a b + dist b c - dist a c) ≤ dist a b + dist b d
⊢ dist b c + dist c d ≤ dist b d
Tactic:
linarith [hacd.dist]
Proof state after:
no goals
Theorem: List.pathLength_nonneg
Proof state before:
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z head✝ : V
⊢ 0 ≤ [head✝].pathLength
Tactic:
simp [pathLength]
Proof state after:
no goals
Theorem: exists_min_dist
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✝ : Finite V
⊢ ∃ r, 0 < r ∧ ∀ (x y : V), x ≠ y → r ≤ dist x y
Tactic:
cases subsingleton_or_nontrivial V
Proof state after:
case inl
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✝ : Finite V
h✝ : Subsingleton V
⊢ ∃ r, 0 < r ∧ ∀ (x y : V), x ≠ y → r ≤ dist x y

case inr
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✝ : Finite V
h✝ : Nontrivial V
⊢ ∃ r, 0 < r ∧ ∀ (x y : V), x ≠ y → r ≤ dist x y
Theorem: exists_min_dist
Proof state before:
case inr
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✝ : Finite V
h✝ : Nontrivial V
⊢ ∃ r, 0 < r ∧ ∀ (x y : V), x ≠ y → r ≤ dist x y
Tactic:
let S : Set (V × V) := (Set.diagonal V)ᶜ
Proof state after:
case inr
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✝ : Finite V
h✝ : Nontrivial V
S : Set (V × V) := (Set.diagonal V)ᶜ
⊢ ∃ r, 0 < r ∧ ∀ (x y : V), x ≠ y → r ≤ dist x y
Theorem: exists_min_dist
Proof state before:
case inr
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✝ : Finite V
h✝ : Nontrivial V
S : Set (V × V) := (Set.diagonal V)ᶜ
⊢ ∃ r, 0 < r ∧ ∀ (x y : V), x ≠ y → r ≤ dist x y
Tactic:
have : S.Nonempty := have ⟨x, y, hxy⟩ := exists_pair_ne V; ⟨(x, y), by simp [S, hxy]⟩
Proof state after:
case inr
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✝ : Finite V
h✝ : Nontrivial V
S : Set (V × V) := (Set.diagonal V)ᶜ
this : S.Nonempty
⊢ ∃ r, 0 < r ∧ ∀ (x y : V), x ≠ y → r ≤ dist x y
Theorem: exists_min_dist
Proof state before:
case inr
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✝ : Finite V
h✝ : Nontrivial V
S : Set (V × V) := (Set.diagonal V)ᶜ
this : S.Nonempty
⊢ ∃ r, 0 < r ∧ ∀ (x y : V), x ≠ y → r ≤ dist x y
Tactic:
obtain ⟨⟨x, y⟩, (hxy : x ≠ y), h⟩ := S.toFinite.exists_minimal_wrt (Function.uncurry dist) _ this
Proof state after:
case inr.intro.mk.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✝ : Finite V
h✝ : Nontrivial V
S : Set (V × V) := (Set.diagonal V)ᶜ
this : S.Nonempty
x y : V
hxy : x ≠ y
h :
  ∀ a' ∈ S,
    Function.uncurry dist a' ≤ Function.uncurry dist (x, y) → Function.uncurry dist (x, y) = Function.uncurry dist a'
⊢ ∃ r, 0 < r ∧ ∀ (x y : V), x ≠ y → r ≤ dist x y
Theorem: exists_min_dist
Proof state before:
case inr.intro.mk.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✝ : Finite V
h✝ : Nontrivial V
S : Set (V × V) := (Set.diagonal V)ᶜ
this : S.Nonempty
x y : V
hxy : x ≠ y
h :
  ∀ a' ∈ S,
    Function.uncurry dist a' ≤ Function.uncurry dist (x, y) → Function.uncurry dist (x, y) = Function.uncurry dist a'
⊢ ∃ r, 0 < r ∧ ∀ (x y : V), x ≠ y → r ≤ dist x y
Tactic:
simp only [Set.mem_compl_iff, Set.mem_diagonal_iff, Function.uncurry_apply_pair, Prod.forall] at h
Proof state after:
case inr.intro.mk.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✝ : Finite V
h✝ : Nontrivial V
S : Set (V × V) := (Set.diagonal V)ᶜ
this : S.Nonempty
x y : V
hxy : x ≠ y
h : ∀ (a b : V), (a, b) ∈ S → dist a b ≤ dist x y → dist x y = dist a b
⊢ ∃ r, 0 < r ∧ ∀ (x y : V), x ≠ y → r ≤ dist x y
Theorem: exists_min_dist
Proof state before:
case inr.intro.mk.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✝ : Finite V
h✝ : Nontrivial V
S : Set (V × V) := (Set.diagonal V)ᶜ
this : S.Nonempty
x y : V
hxy : x ≠ y
h : ∀ (a b : V), (a, b) ∈ S → dist a b ≤ dist x y → dist x y = dist a b
⊢ ∃ r, 0 < r ∧ ∀ (x y : V), x ≠ y → r ≤ dist x y
Tactic:
exact ⟨dist x y, by simp [hxy], fun a b hab => le_of_not_lt (fun h' => h'.ne' (h _ _ hab h'.le))⟩
Proof state after:
no goals
Theorem: exists_min_dist
Proof state before:
case inl
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✝ : Finite V
h✝ : Subsingleton V
⊢ ∃ r, 0 < r ∧ ∀ (x y : V), x ≠ y → r ≤ dist x y
Tactic:
exact ⟨1, zero_lt_one, fun x y ↦ by simp [Subsingleton.elim x y]⟩
Proof state after:
no goals
Theorem: exists_min_dist
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✝ : Finite V
h✝ : Subsingleton V
x y : V
⊢ x ≠ y → 1 ≤ dist x y
Tactic:
simp [Subsingleton.elim x y]
Proof state after:
no goals
Theorem: exists_min_dist
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✝ : Finite V
h✝ : Nontrivial V
S : Set (V × V) := (Set.diagonal V)ᶜ
x y : V
hxy : x ≠ y
⊢ (x, y) ∈ S
Tactic:
simp [S, hxy]
Proof state after:
no goals
Theorem: exists_min_dist
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✝ : Finite V
h✝ : Nontrivial V
S : Set (V × V) := (Set.diagonal V)ᶜ
this : S.Nonempty
x y : V
hxy : x ≠ y
h : ∀ (a b : V), (a, b) ∈ S → dist a b ≤ dist x y → dist x y = dist a b
⊢ 0 < dist x y
Tactic:
simp [hxy]
Proof state after:
no goals
Theorem: length_mul_le_pathLength_add
Proof state before:
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z : V
r : ℝ
hr : 0 ≤ r
h : ∀ (x y : V), x ≠ y → r ≤ dist x y
x✝ : List.Chain' (fun x x_1 => x ≠ x_1) []
⊢ ↑[].length * r ≤ [].pathLength + r
Tactic:
simp [List.pathLength, hr]
Proof state after:
no goals
Theorem: length_mul_le_pathLength_add
Proof state before:
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z : V
r : ℝ
hr : 0 ≤ r
h : ∀ (x y : V), x ≠ y → r ≤ dist x y
head✝ : V
x✝ : List.Chain' (fun x x_1 => x ≠ x_1) [head✝]
⊢ ↑[head✝].length * r ≤ [head✝].pathLength + r
Tactic:
simp [List.pathLength]
Proof state after:
no goals
Theorem: length_mul_le_pathLength_add
Proof state before:
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x✝ y✝ z : V
r : ℝ
hr : 0 ≤ r
h : ∀ (x y : V), x ≠ y → r ≤ dist x y
x y : V
xs : List V
h' : List.Chain' (fun x x_1 => x ≠ x_1) (x :: y :: xs)
⊢ ↑(x :: y :: xs).length * r ≤ (x :: y :: xs).pathLength + r
Tactic:
simp only [List.chain'_cons] at 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
r : ℝ
hr : 0 ≤ r
h : ∀ (x y : V), x ≠ y → r ≤ dist x y
x y : V
xs : List V
h' : x ≠ y ∧ List.Chain' (fun x x_1 => x ≠ x_1) (y :: xs)
⊢ ↑(x :: y :: xs).length * r ≤ (x :: y :: xs).pathLength + r
Theorem: length_mul_le_pathLength_add
Proof state before:
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x✝ y✝ z : V
r : ℝ
hr : 0 ≤ r
h : ∀ (x y : V), x ≠ y → r ≤ dist x y
x y : V
xs : List V
h' : x ≠ y ∧ List.Chain' (fun x x_1 => x ≠ x_1) (y :: xs)
⊢ ↑(x :: y :: xs).length * r ≤ (x :: y :: xs).pathLength + r
Tactic:
rw [List.pathLength, List.length, Nat.cast_add_one, add_one_mul (α := ℝ), add_assoc,
  add_comm]
Proof state after:
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x✝ y✝ z : V
r : ℝ
hr : 0 ≤ r
h : ∀ (x y : V), x ≠ y → r ≤ dist x y
x y : V
xs : List V
h' : x ≠ y ∧ List.Chain' (fun x x_1 => x ≠ x_1) (y :: xs)
⊢ r + ↑(y :: xs).length * r ≤ dist x y + ((y :: xs).pathLength + r)
Theorem: length_mul_le_pathLength_add
Proof state before:
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x✝ y✝ z : V
r : ℝ
hr : 0 ≤ r
h : ∀ (x y : V), x ≠ y → r ≤ dist x y
x y : V
xs : List V
h' : x ≠ y ∧ List.Chain' (fun x x_1 => x ≠ x_1) (y :: xs)
⊢ r + ↑(y :: xs).length * r ≤ dist x y + ((y :: xs).pathLength + r)
Tactic:
exact add_le_add (h _ _ h'.1) (length_mul_le_pathLength_add hr h h'.2)
Proof state after:
no goals
Theorem: uniformly_bounded_of_chain_ne_of_pathLength_le
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✝ : Finite V
R : ℝ
⊢ ∃ n, ∀ (l : List V), List.Chain' (fun x x_1 => x ≠ x_1) l → l.pathLength ≤ R → l.length ≤ n
Tactic:
have ⟨r, hr, hr'⟩ := exists_min_dist V
Proof state after:
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✝ : Finite V
R r : ℝ
hr : 0 < r
hr' : ∀ (x y : V), x ≠ y → r ≤ dist x y
⊢ ∃ n, ∀ (l : List V), List.Chain' (fun x x_1 => x ≠ x_1) l → l.pathLength ≤ R → l.length ≤ n
Theorem: uniformly_bounded_of_chain_ne_of_pathLength_le
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✝ : Finite V
R r : ℝ
hr : 0 < r
hr' : ∀ (x y : V), x ≠ y → r ≤ dist x y
⊢ ∃ n, ∀ (l : List V), List.Chain' (fun x x_1 => x ≠ x_1) l → l.pathLength ≤ R → l.length ≤ n
Tactic:
refine ⟨⌊R / r + 1⌋₊, ?_⟩
Proof state after:
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✝ : Finite V
R r : ℝ
hr : 0 < r
hr' : ∀ (x y : V), x ≠ y → r ≤ dist x y
⊢ ∀ (l : List V), List.Chain' (fun x x_1 => x ≠ x_1) l → l.pathLength ≤ R → l.length ≤ ⌊R / r + 1⌋₊
Theorem: uniformly_bounded_of_chain_ne_of_pathLength_le
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✝ : Finite V
R r : ℝ
hr : 0 < r
hr' : ∀ (x y : V), x ≠ y → r ≤ dist x y
⊢ ∀ (l : List V), List.Chain' (fun x x_1 => x ≠ x_1) l → l.pathLength ≤ R → l.length ≤ ⌊R / r + 1⌋₊
Tactic:
intro l hl hl'
Proof state after:
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✝ : Finite V
R r : ℝ
hr : 0 < r
hr' : ∀ (x y : V), x ≠ y → r ≤ dist x y
l : List V
hl : List.Chain' (fun x x_1 => x ≠ x_1) l
hl' : l.pathLength ≤ R
⊢ l.length ≤ ⌊R / r + 1⌋₊
Theorem: uniformly_bounded_of_chain_ne_of_pathLength_le
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✝ : Finite V
R r : ℝ
hr : 0 < r
hr' : ∀ (x y : V), x ≠ y → r ≤ dist x y
l : List V
hl : List.Chain' (fun x x_1 => x ≠ x_1) l
hl' : l.pathLength ≤ R
⊢ l.length ≤ ⌊R / r + 1⌋₊
Tactic:
have hR : 0 ≤ R := l.pathLength_nonneg.trans hl'
Proof state after:
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✝ : Finite V
R r : ℝ
hr : 0 < r
hr' : ∀ (x y : V), x ≠ y → r ≤ dist x y
l : List V
hl : List.Chain' (fun x x_1 => x ≠ x_1) l
hl' : l.pathLength ≤ R
hR : 0 ≤ R
⊢ l.length ≤ ⌊R / r + 1⌋₊