Bump mathlib

LeanCamCombi.lean

@@ -39,11 +39,12 @@ import LeanCamCombi.Mathlib.Data.Finset.Lattice
 import LeanCamCombi.Mathlib.Data.Finset.Pointwise
 import LeanCamCombi.Mathlib.Data.Finset.PosDiffs
 import LeanCamCombi.Mathlib.Data.Fintype.Basic
+import LeanCamCombi.Mathlib.Data.List.Basic
 import LeanCamCombi.Mathlib.Data.Nat.Factorization.Basic
 import LeanCamCombi.Mathlib.Data.Nat.Factors
+import LeanCamCombi.Mathlib.Data.Set.Finite
 import LeanCamCombi.Mathlib.Data.Set.Image
 import LeanCamCombi.Mathlib.Data.Set.Pointwise.SMul
-import LeanCamCombi.Mathlib.Data.Set.Prod
 import LeanCamCombi.Mathlib.GroupTheory.QuotientGroup
 import LeanCamCombi.Mathlib.GroupTheory.Subgroup.Stabilizer
 import LeanCamCombi.Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
@@ -59,6 +60,7 @@ import LeanCamCombi.Mathlib.Order.Sublattice
 import LeanCamCombi.Mathlib.Order.SupClosed
 import LeanCamCombi.Mathlib.Probability.Independence.Basic
 import LeanCamCombi.Mathlib.Probability.ProbabilityMassFunction.Constructions
+import LeanCamCombi.MetricBetween
 import LeanCamCombi.MinkowskiCaratheodory
 import LeanCamCombi.SimplicialComplex.Basic
 import LeanCamCombi.SimplicialComplex.Finite

LeanCamCombi/Mathlib/Combinatorics/SimpleGraph/Containment.lean

@@ -298,7 +298,6 @@ lemma not_isContained_kill (hG : G ≠ ⊥) : ¬ G ⊑ G.kill H := by
   rw [Sym2.map_map, Set.mem_singleton_iff, ←he₁]
   congr 1 with x
   refine' congr_arg (↑) (Equiv.Set.image_symm_apply _ _ injective_id _ _)
-  simpa using x.2
 
 variable [Fintype H.edgeSet]
 

LeanCamCombi/Mathlib/Data/List/Basic.lean

@@ -0,0 +1,23 @@
+import Mathlib.Data.List.Basic
+
+namespace List
+
+lemma getLast_filter {α : Type*} {p : α → Bool} :
+    ∀ (l : List α) (hlp : l.filter p ≠ []), p (l.getLast (hlp <| ·.symm ▸ rfl)) = true →
+      (l.filter p).getLast hlp = l.getLast (hlp <| ·.symm ▸ rfl)
+  | [a], h, h' => by rw [List.getLast_singleton'] at h'; simp [List.filter_cons, h']
+  | (a :: b :: as), h, h' => by
+      rw [List.getLast_cons_cons] at h' ⊢
+      simp only [List.filter_cons (x := a)] at h ⊢
+      rcases Bool.eq_false_or_eq_true (p a) with ha | ha
+      · simp only [ha, ite_true]
+        have : (b :: as).filter p ≠ []
+        · have : (b :: as).getLast (List.cons_ne_nil _ _) ∈ (b :: as).filter p
+          · rw [List.mem_filter]
+            exact ⟨List.getLast_mem _, h'⟩
+          exact List.ne_nil_of_mem this
+        rw [List.getLast_cons this, getLast_filter (b :: as) this h']
+      simp only [ha, cond_false] at h ⊢
+      exact getLast_filter (b :: as) h h'
+
+end List

LeanCamCombi/Mathlib/Data/Set/Finite.lean

@@ -0,0 +1,20 @@
+import Mathlib.Data.Set.Finite
+
+open Set
+
+namespace List
+variable (α : Type*) [Finite α] (n : ℕ)
+
+lemma finite_length_eq : {l : List α | l.length = n}.Finite := by
+  induction n with
+  | zero => simp [List.length_eq_zero]
+  | succ n ih =>
+    suffices : {l : List α | l.length = n + 1} = Set.univ.image2 (· :: ·) {l | l.length = n}
+    · rw [this]; exact Set.finite_univ.image2 _ ih
+    ext (_ | _) <;> simp [n.succ_ne_zero.symm]
+
+lemma finite_length_lt : {l : List α | l.length < n}.Finite := by
+  convert (Finset.range n).finite_toSet.biUnion fun i _ ↦ finite_length_eq α i; ext; simp
+
+lemma finite_length_le : {l : List α | l.length ≤ n}.Finite := by
+  simpa [Nat.lt_succ_iff] using finite_length_lt α (n + 1)

LeanCamCombi/Mathlib/Order/Sublattice.lean

@@ -1,5 +1,4 @@
 import Mathlib.Order.Sublattice
-import LeanCamCombi.Mathlib.Data.Set.Prod
 import LeanCamCombi.Mathlib.Order.Hom.Lattice
 
 /-!

LeanCamCombi/MetricBetween.lean

@@ -0,0 +1,55 @@
+import Mathlib.Order.Circular
+import Mathlib.Topology.MetricSpace.Basic
+
+/-!
+### TODO
+
+Axiomatic betweenness
+-/
+
+variable {V : Type*} [MetricSpace V] {u v w : V}
+
+def MetricSBtw : SBtw V where
+  sbtw u v w := u ≠ v ∧ u ≠ w ∧ v ≠ w ∧ dist u v + dist v w = dist u w
+
+scoped[MetricBetweenness] attribute [instance] MetricSBtw
+
+open MetricBetweenness
+
+lemma MetricSpace.sbtw_iff :
+  sbtw u v w ↔ u ≠ v ∧ u ≠ w ∧ v ≠ w ∧ dist u v + dist v w = dist u w := Iff.rfl
+
+lemma SBtw.sbtw.ne12 (h : sbtw u v w) : u ≠ v := h.1
+lemma SBtw.sbtw.ne13 (h : sbtw u v w) : u ≠ w := h.2.1
+lemma SBtw.sbtw.ne23 (h : sbtw u v w) : v ≠ w := h.2.2.1
+lemma SBtw.sbtw.dist (h : sbtw u v w) : dist u v + dist v w = dist u w := h.2.2.2
+
+lemma SBtw.sbtw.symm : sbtw u v w → sbtw w v u
+| ⟨huv, huw, hvw, d⟩ => ⟨hvw.symm, huw.symm, huv.symm, by simpa [dist_comm, add_comm] using d⟩
+lemma SBtw.comm : sbtw u v w ↔ sbtw w v u :=
+⟨.symm, .symm⟩
+
+lemma sbtw_iff_of_ne (h12 : u ≠ v) (h13 : u ≠ w) (h23 : v ≠ w) :
+    sbtw u v w ↔ dist u v + dist v w = dist u w :=
+  by simp [MetricSpace.sbtw_iff, h12, h13, h23]
+
+lemma sbtw_mk (h12 : u ≠ v) (h23 : v ≠ w) (h : dist u v + dist v w ≤ dist u w) : sbtw u v w := by
+  refine ⟨h12, ?_, h23, h.antisymm (dist_triangle _ _ _)⟩
+  rintro rfl
+  rw [dist_self] at h
+  replace h : dist v u ≤ 0 := by linarith [dist_comm v u]
+  simp only [dist_le_zero] at h
+  exact h23 h
+
+lemma SBtw.sbtw.right_cancel {u v w x : V} (h : sbtw u v x) (h' : sbtw v w x) : sbtw u v w :=
+  sbtw_mk h.ne12 h'.ne12 (by linarith [h.dist, h'.dist, dist_triangle u w x, dist_triangle u v w])
+
+lemma SBtw.sbtw.asymm_right {u v x : V} (h : sbtw u v x) (h' : sbtw v u x) : False := by
+  have := h'.dist
+  rw [dist_comm] at this
+  have : Dist.dist u v = 0 := by linarith [h.dist]
+  simp [h.ne12] at this
+
+lemma SBtw.sbtw.trans_right' {u v w x : V} (h : sbtw u v x) (h' : sbtw v w x) : sbtw u w x :=
+  have : u ≠ w := by rintro rfl; exact h.asymm_right h'
+  sbtw_mk this h'.ne23 <| by linarith [h.dist, h'.dist, dist_triangle u v w]