bump toolchain and Mathlib to v4.19.0

FormalConjectures/Arxiv/1609.08688/sIncreasingrTuples.lean

@@ -125,7 +125,7 @@ theorem maximalLength_zero : maximalLength 0 = 0 := by
   have (x : ℕ) (s : List (Fin 3 → ℕ)) :
       IsIncreasing₂ s ∧ (∀ a, a ∉ s) ∧ s.length = x ↔ s = [] ∧ x = 0 := by
     refine ⟨fun ⟨ha₁, ha₂, rfl⟩ => ?_, fun ⟨h₁, h₂⟩ => by simp [h₁, h₂]⟩
-    simp only [List.length_eq_zero, and_self]
+    simp only [List.length_eq_zero_iff, and_self]
     refine List.eq_nil_of_subset_nil fun ai hai => ?_
     simpa using ha₂ ai hai
   simp [maximalLength, fun x => exists_congr (this x)]
@@ -138,8 +138,8 @@ theorem maximalLength_one : maximalLength 1 = 1 := by
         s = [fun _ => 1] ∧ x = 1 ∨ s = [] ∧ x = 0 := by
     refine ⟨fun ⟨hs₁, hs₂, hx⟩ => ?_, fun h => by aesop⟩
     have := hx ▸ isIncreasing₂_const_length hs₁ hs₂
-    interval_cases x; simp [hx, List.length_eq_zero.1 hx]; simp
-    obtain ⟨a, rfl⟩ := List.length_eq_one.1 hx
+    interval_cases x; simp [hx, List.length_eq_zero_iff.1 hx]; simp
+    obtain ⟨a, rfl⟩ := List.length_eq_one_iff.1 hx
     simp at hs₂
     rw [show a = fun _ => 1 from funext fun i => by simp [hs₂ i]]
   simp [maximalLength, fun x => exists_congr (this x)]

FormalConjectures/ErdosProblems/366.lean

@@ -37,7 +37,7 @@ Note that $8$ is $3$-full and $9$ is 2-full.
 @[category test, AMS 11]
 theorem exists_three_full_then_two_full : (∃ (n : ℕ), (3).Full n ∧ (2).Full (n + 1)) := by
   use 8
-  simp [Nat.Full, Nat.primeFactorsEq]
+  norm_num +contextual [Nat.Full, Nat.primeFactors, Nat.primeFactorsList]
 
 /--
 Are there infinitely many 3-full $n$ such that $n+1$ is 2-full?
@@ -50,7 +50,7 @@ theorem erdos_366.variant.three_two :
 /--
 Are there any consecutive pairs of $3$-full integers?
 -/
-@[category undergraduate, AMS 11]
+@[category research open, AMS 11]
 theorem erdos_366.variant.weaker : (∃ (n : ℕ), (3).Full n ∧ (3).Full (n + 1))  ↔ answer(sorry) := by
   sorry
 

FormalConjectures/ErdosProblems/509.lean

@@ -65,7 +65,7 @@ lemma BoundedDiscCover.bound_nonneg_of_nonempty
     0 < r := by
   apply lt_of_lt_of_le _ bdc.h_bdd
   suffices Nonempty ι by
-    apply tsum_pos bdc.h_summable (fun j => le_of_lt (bdc.h_pos j)) Classical.ofNonempty (bdc.h_pos _)
+    apply Summable.tsum_pos bdc.h_summable (fun j => le_of_lt (bdc.h_pos j)) Classical.ofNonempty (bdc.h_pos _)
   by_contra!
   apply Set.Nonempty.ne_empty hS (Set.eq_empty_of_subset_empty _)
   convert bdc.h_cover

FormalConjectures/ErdosProblems/522.lean

@@ -34,7 +34,7 @@ structure KacPolynomial
     {k : Type*} (n : ℕ) [Field k] [MeasurableSpace k] (S : Set k)
     (Ω : Type*) [MeasureSpace Ω] (μ : Measure k := by volume_tac) where
   toFun : Fin n.succ → Ω → k
-  h_indep : ProbabilityTheory.iIndepFun inferInstance toFun ℙ
+  h_indep : ProbabilityTheory.iIndepFun toFun ℙ
   h_unif : ∀ i, MeasureTheory.pdf.IsUniform (toFun i) S ℙ μ
 
 variable {k : Type*} (n : ℕ) [Field k] [MeasurableSpace k] (S : Set k)

FormalConjectures/ForMathlib/Algebra/Order/Group/Pointwise/Interval.lean

@@ -19,11 +19,8 @@ import Mathlib.Tactic
 
 theorem Nat.image_mul_two_Iio_even {n : ℕ} (h : Even n) :
     (2 * ·) '' Set.Iio (n / 2) = { n | Even n } ∩ Set.Iio n := by
-  norm_num [Set.ext_iff, Nat.even_iff] at *
-  use ⟨by omega, fun _ =>⟨. / 2, by omega⟩⟩
+  aesop (add simp [even_iff_two_dvd, dvd_iff_exists_eq_mul_right])
 
 theorem Nat.image_mul_two_Iio (n : ℕ) :
     (2 * ·) '' Set.Iio ((n + 1) / 2) = { n | Even n } ∩ Set.Iio n := by
-  norm_num [Nat.lt_iff_add_one_le, Set.ext_iff, Nat.le_div_iff_mul_le,
-    Nat.even_iff]
-  use ⟨by omega, fun _ => ⟨. / 2, by omega⟩⟩
+  aesop (add simp [even_iff_two_dvd, dvd_iff_exists_eq_mul_right, mul_comm, lt_div_iff_mul_lt])

FormalConjectures/ForMathlib/Analysis/SpecialFunctions/NthRoot.lean

@@ -107,9 +107,9 @@ theorem nthRoot_mul_of_even_of_nonneg {n : ℕ} {a b : ℝ} (hn : Even n)
   simp only [Real.nthRoot_of_even hn, Real.mul_rpow ha hb]
 
 theorem nthRoot_mul_of_odd {n : ℕ} {a b : ℝ} (hn : Odd n) :
-    Real.nthRoot n (a * b) = Real.nthRoot n a * Real.nthRoot n b := by
-  simp only [Real.nthRoot_of_odd hn, sign_mul, SignType.coe_mul, abs_mul,
-    Real.mul_rpow (Real.nnabs.proof_1 a) (Real.nnabs.proof_1 b)]
+    nthRoot n (a * b) = nthRoot n a * nthRoot n b := by
+  simp [Real.nthRoot_of_odd hn, sign_mul, SignType.coe_mul, abs_mul,
+  Real.mul_rpow (abs_nonneg a) (abs_nonneg b)]
   ring
 
 end Real

FormalConjectures/ForMathlib/Combinatorics/SimpleGraph/Bipartite.lean

@@ -20,6 +20,8 @@ import Mathlib.Algebra.Group.Indicator
 import Mathlib.Combinatorics.Enumerative.DoubleCounting
 import Mathlib.Combinatorics.SimpleGraph.Coloring
 import Mathlib.Combinatorics.SimpleGraph.DegreeSum
+import Mathlib.Combinatorics.SimpleGraph.Bipartite
+import Mathlib.Combinatorics.SimpleGraph.Coloring
 
 /-!
 # Bipartite graphs
@@ -73,187 +75,6 @@ namespace SimpleGraph
 
 variable {V : Type*} {v w : V} {G : SimpleGraph V} {s t : Set V}
 
-section IsBipartiteWith
-
-/-- `G` is bipartite in sets `s` and `t` iff `s` and `t` are disjoint and if vertices `v` and `w`
-are adjacent in `G` then `v ∈ s` and `w ∈ t`, or `v ∈ t` and `w ∈ s`. -/
-structure IsBipartiteWith (G : SimpleGraph V) (s t : Set V) : Prop where
-  disjoint : Disjoint s t
-  mem_of_adj ⦃v w : V⦄ : G.Adj v w → v ∈ s ∧ w ∈ t ∨ v ∈ t ∧ w ∈ s
-
-theorem IsBipartiteWith.symm (h : G.IsBipartiteWith s t) : G.IsBipartiteWith t s where
-  disjoint := h.disjoint.symm
-  mem_of_adj v w hadj := by
-    rw [@and_comm (v ∈ t) (w ∈ s), @and_comm (v ∈ s) (w ∈ t)]
-    exact h.mem_of_adj hadj.symm
-
-theorem isBipartiteWith_comm : G.IsBipartiteWith s t ↔ G.IsBipartiteWith t s :=
-  ⟨IsBipartiteWith.symm, IsBipartiteWith.symm⟩
-
-/-- If `G.IsBipartiteWith s t` and `v ∈ s`, then if `v` is adjacent to `w` in `G` then `w ∈ t`. -/
-theorem IsBipartiteWith.mem_of_mem_adj
-    (h : G.IsBipartiteWith s t) (hv : v ∈ s) (hadj : G.Adj v w) : w ∈ t := by
-  apply h.mem_of_adj at hadj
-  have nhv : v ∉ t := Set.disjoint_left.mp h.disjoint hv
-  simpa [hv, nhv] using hadj
-
-/-- If `G.IsBipartiteWith s t` and `v ∈ s`, then the neighbor set of `v` is the set of vertices in
-`t` adjacent to `v` in `G`. -/
-theorem isBipartiteWith_neighborSet (h : G.IsBipartiteWith s t) (hv : v ∈ s) :
-    G.neighborSet v = { w ∈ t | G.Adj v w } := by
-  ext w
-  rw [mem_neighborSet, Set.mem_setOf_eq, iff_and_self]
-  exact h.mem_of_mem_adj hv
-
-/-- If `G.IsBipartiteWith s t` and `v ∈ s`, then the neighbor set of `v` is a subset of `t`. -/
-theorem isBipartiteWith_neighborSet_subset (h : G.IsBipartiteWith s t) (hv : v ∈ s) :
-    G.neighborSet v ⊆ t := by
-  rw [isBipartiteWith_neighborSet h hv]
-  exact Set.sep_subset t (G.Adj v ·)
-
-/-- If `G.IsBipartiteWith s t` and `v ∈ s`, then the neighbor set of `v` is disjoint to `s`. -/
-theorem isBipartiteWith_neighborSet_disjoint (h : G.IsBipartiteWith s t) (hv : v ∈ s) :
-    Disjoint (G.neighborSet v) s :=
-  Set.disjoint_of_subset_left (isBipartiteWith_neighborSet_subset h hv) h.disjoint.symm
-
-/-- If `G.IsBipartiteWith s t` and `w ∈ t`, then if `v` is adjacent to `w` in `G` then `v ∈ s`. -/
-theorem IsBipartiteWith.mem_of_mem_adj'
-    (h : G.IsBipartiteWith s t) (hw : w ∈ t) (hadj : G.Adj v w) : v ∈ s := by
-  apply h.mem_of_adj at hadj
-  have nhw : w ∉ s := Set.disjoint_right.mp h.disjoint hw
-  simpa [hw, nhw] using hadj
-
-/-- If `G.IsBipartiteWith s t` and `w ∈ t`, then the neighbor set of `w` is the set of vertices in
-`s` adjacent to `w` in `G`. -/
-theorem isBipartiteWith_neighborSet' (h : G.IsBipartiteWith s t) (hw : w ∈ t) :
-    G.neighborSet w = { v ∈ s | G.Adj v w } := by
-  ext v
-  rw [mem_neighborSet, adj_comm, Set.mem_setOf_eq, iff_and_self]
-  exact h.mem_of_mem_adj' hw
-
-/-- If `G.IsBipartiteWith s t` and `w ∈ t`, then the neighbor set of `w` is a subset of `s`. -/
-theorem isBipartiteWith_neighborSet_subset' (h : G.IsBipartiteWith s t) (hw : w ∈ t) :
-    G.neighborSet w ⊆ s := by
-  rw [isBipartiteWith_neighborSet' h hw]
-  exact Set.sep_subset s (G.Adj · w)
-
-/-- If `G.IsBipartiteWith s t`, then the support of `G` is a subset of `s ∪ t`. -/
-theorem isBipartiteWith_support_subset (h : G.IsBipartiteWith s t) : G.support ⊆ s ∪ t := by
-  intro v ⟨w, hadj⟩
-  apply h.mem_of_adj at hadj
-  tauto
-
-/-- If `G.IsBipartiteWith s t` and `w ∈ t`, then the neighbor set of `w` is disjoint to `t`. -/
-theorem isBipartiteWith_neighborSet_disjoint' (h : G.IsBipartiteWith s t) (hw : w ∈ t) :
-    Disjoint (G.neighborSet w) t :=
-  Set.disjoint_of_subset_left (isBipartiteWith_neighborSet_subset' h hw) h.disjoint
-
-variable [Fintype V] {s t : Finset V} [DecidableRel G.Adj]
-
-/-- If `G.IsBipartiteWith s t` and `v ∈ s`, then the neighbor finset of `v` is the set of vertices
-in `s` adjacent to `v` in `G`. -/
-theorem isBipartiteWith_neighborFinset (h : G.IsBipartiteWith s t) (hv : v ∈ s) :
-    G.neighborFinset v = { w ∈ t | G.Adj v w } := by
-  ext w
-  rw [mem_neighborFinset, mem_filter, iff_and_self]
-  exact h.mem_of_mem_adj hv
-
-/-- If `G.IsBipartiteWith s t` and `v ∈ s`, then the neighbor finset of `v` is the set of vertices
-"above" `v` according to the adjacency relation of `G`. -/
-theorem isBipartiteWith_bipartiteAbove (h : G.IsBipartiteWith s t) (hv : v ∈ s) :
-    G.neighborFinset v = bipartiteAbove G.Adj t v := by
-  rw [isBipartiteWith_neighborFinset h hv, bipartiteAbove]
-
-/-- If `G.IsBipartiteWith s t` and `v ∈ s`, then the neighbor finset of `v` is a subset of `s`. -/
-theorem isBipartiteWith_neighborFinset_subset (h : G.IsBipartiteWith s t) (hv : v ∈ s) :
-    G.neighborFinset v ⊆ t := by
-  rw [isBipartiteWith_neighborFinset h hv]
-  exact filter_subset (G.Adj v ·) t
-
-/-- If `G.IsBipartiteWith s t` and `v ∈ s`, then the neighbor finset of `v` is disjoint to `s`. -/
-theorem isBipartiteWith_neighborFinset_disjoint (h : G.IsBipartiteWith s t) (hv : v ∈ s) :
-    Disjoint (G.neighborFinset v) s := by
-  rw [neighborFinset_def, ← disjoint_coe, Set.coe_toFinset]
-  exact isBipartiteWith_neighborSet_disjoint h hv
-
-/-- If `G.IsBipartiteWith s t` and `v ∈ s`, then the degree of `v` in `G` is at most the size of
-`t`. -/
-theorem isBipartiteWith_degree_le (h : G.IsBipartiteWith s t) (hv : v ∈ s) : G.degree v ≤ #t := by
-  rw [← card_neighborFinset_eq_degree]
-  exact card_le_card (isBipartiteWith_neighborFinset_subset h hv)
-
-/-- If `G.IsBipartiteWith s t` and `w ∈ t`, then the neighbor finset of `w` is the set of vertices
-in `s` adjacent to `w` in `G`. -/
-theorem isBipartiteWith_neighborFinset' (h : G.IsBipartiteWith s t) (hw : w ∈ t) :
-    G.neighborFinset w = { v ∈ s | G.Adj v w } := by
-  ext v
-  rw [mem_neighborFinset, adj_comm, mem_filter, iff_and_self]
-  exact h.mem_of_mem_adj' hw
-
-/-- If `G.IsBipartiteWith s t` and `w ∈ t`, then the neighbor finset of `w` is the set of vertices
-"below" `w` according to the adjacency relation of `G`. -/
-theorem isBipartiteWith_bipartiteBelow (h : G.IsBipartiteWith s t) (hw : w ∈ t) :
-    G.neighborFinset w = bipartiteBelow G.Adj s w := by
-  rw [isBipartiteWith_neighborFinset' h hw, bipartiteBelow]
-
-/-- If `G.IsBipartiteWith s t` and `w ∈ t`, then the neighbor finset of `w` is a subset of `s`. -/
-theorem isBipartiteWith_neighborFinset_subset' (h : G.IsBipartiteWith s t) (hw : w ∈ t) :
-    G.neighborFinset w ⊆ s := by
-  rw [isBipartiteWith_neighborFinset' h hw]
-  exact filter_subset (G.Adj · w) s
-
-/-- If `G.IsBipartiteWith s t` and `w ∈ t`, then the neighbor finset of `w` is disjoint to `t`. -/
-theorem isBipartiteWith_neighborFinset_disjoint' (h : G.IsBipartiteWith s t) (hw : w ∈ t) :
-    Disjoint (G.neighborFinset w) t := by
-  rw [neighborFinset_def, ← disjoint_coe, Set.coe_toFinset]
-  exact isBipartiteWith_neighborSet_disjoint' h hw
-
-/-- If `G.IsBipartiteWith s t` and `w ∈ t`, then the degree of `w` in `G` is at most the size of
-`s`. -/
-theorem isBipartiteWith_degree_le' (h : G.IsBipartiteWith s t) (hw : w ∈ t) : G.degree w ≤ #s := by
-  rw [← card_neighborFinset_eq_degree]
-  exact card_le_card (isBipartiteWith_neighborFinset_subset' h hw)
-
-/-- If `G.IsBipartiteWith s t`, then the sum of the degrees of vertices in `s` is equal to the sum
-of the degrees of vertices in `t`.
-
-See `Finset.sum_card_bipartiteAbove_eq_sum_card_bipartiteBelow`. -/
-theorem isBipartiteWith_sum_degrees_eq (h : G.IsBipartiteWith s t) :
-    ∑ v ∈ s, G.degree v = ∑ w ∈ t, G.degree w := by
-  simp_rw [← sum_attach t, ← sum_attach s, ← card_neighborFinset_eq_degree]
-  conv_lhs =>
-    rhs; intro v
-    rw [isBipartiteWith_bipartiteAbove h v.prop]
-  conv_rhs =>
-    rhs; intro w
-    rw [isBipartiteWith_bipartiteBelow h w.prop]
-  simp_rw [sum_attach s fun w ↦ #(bipartiteAbove G.Adj t w),
-    sum_attach t fun v ↦ #(bipartiteBelow G.Adj s v)]
-  exact sum_card_bipartiteAbove_eq_sum_card_bipartiteBelow G.Adj
-
--- This is already proven in Mathlib
-proof_wanted isBipartiteWith_sum_degrees_eq_twice_card_edges
-    [DecidableEq V] (h : G.IsBipartiteWith s t) :
-    ∑ v ∈ s ∪ t, G.degree v = 2 * #G.edgeFinset
-
--- This is already proven in Mathlib
-/-- The degree-sum formula for bipartite graphs, summing over the "left" part.
-
-See `SimpleGraph.sum_degrees_eq_twice_card_edges` for the general version, and
-`SimpleGraph.isBipartiteWith_sum_degrees_eq_card_edges'` for the version from the "right". -/
-proof_wanted isBipartiteWith_sum_degrees_eq_card_edges (h : G.IsBipartiteWith s t) :
-    ∑ v ∈ s, G.degree v = #G.edgeFinset
-
--- This is already proven in Mathlib
-/-- The degree-sum formula for bipartite graphs, summing over the "right" part.
-
-See `SimpleGraph.sum_degrees_eq_twice_card_edges` for the general version, and
-`SimpleGraph.isBipartiteWith_sum_degrees_eq_card_edges` for the version from the "left". -/
-proof_wanted isBipartiteWith_sum_degrees_eq_card_edges' (h : G.IsBipartiteWith s t) :
-    ∑ v ∈ t, G.degree v = #G.edgeFinset
-
-end IsBipartiteWith
-
 section IsBipartite
 
 /-- The predicate for a simple graph to be bipartite. -/

FormalConjectures/ForMathlib/Combinatorics/SimpleGraph/DiamExtra.lean

@@ -42,64 +42,6 @@ assert_not_exists Field
 namespace SimpleGraph
 variable {α : Type*} {G G' : SimpleGraph α}
 
-section eccent
-
-/-- The eccentricity of a vertex is the greatest distance between it and any other vertex. -/
-noncomputable def eccent (G : SimpleGraph α) (u : α) : ℕ∞ :=
-  ⨆ v, G.edist u v
-
-lemma eccent_def : G.eccent = fun u ↦ ⨆ v, G.edist u v := rfl
-
-lemma edist_le_eccent {u v : α} : G.edist u v ≤ G.eccent u :=
-  le_iSup (G.edist u) v
-
-lemma exists_edist_eq_eccent_of_finite [Finite α] (u : α) :
-    ∃ v, G.edist u v = G.eccent u :=
-  have : Nonempty α := Nonempty.intro u
-  exists_eq_ciSup_of_finite
-
-lemma eccent_eq_top_of_not_connected (h : ¬ G.Connected) (u : α) :
-    G.eccent u = ⊤ := by
-  rw [connected_iff_exists_forall_reachable] at h
-  push_neg at h
-  obtain ⟨v, h⟩ := h u
-  rw [eq_top_iff, ← edist_eq_top_of_not_reachable h]
-  exact le_iSup (G.edist u) v
-
-lemma eccent_eq_zero_of_subsingleton [Subsingleton α] (u : α) : G.eccent u = 0 := by
-  simpa [eccent, edist_eq_zero_iff] using subsingleton_iff.mp ‹_› u
-
-lemma eccent_ne_zero [Nontrivial α] (u : α) : G.eccent u ≠ 0 := by
-  obtain ⟨v, huv⟩ := exists_ne ‹_›
-  contrapose! huv
-  simp only [eccent, ENat.iSup_eq_zero, edist_eq_zero_iff] at huv
-  exact (huv v).symm
-
-lemma eccent_eq_zero_iff (u : α) : G.eccent u = 0 ↔ Subsingleton α := by
-  refine ⟨fun h ↦ ?_, fun _ ↦ eccent_eq_zero_of_subsingleton u⟩
-  contrapose! h
-  rw [not_subsingleton_iff_nontrivial] at h
-  exact eccent_ne_zero u
-
-lemma eccent_pos_iff (u : α) : 0 < G.eccent u ↔ Nontrivial α := by
-  rw [pos_iff_ne_zero, ← not_subsingleton_iff_nontrivial, ← eccent_eq_zero_iff]
-
-@[simp]
-lemma eccent_bot [Nontrivial α] (u : α) : (⊥ : SimpleGraph α).eccent u = ⊤ :=
-  eccent_eq_top_of_not_connected bot_not_connected u
-
-@[simp]
-lemma eccent_top [Nontrivial α] (u : α) : (⊤ : SimpleGraph α).eccent u = 1 := by
-  apply le_antisymm ?_ <| Order.one_le_iff_pos.mpr <| pos_iff_ne_zero.mpr <| eccent_ne_zero u
-  rw [eccent, iSup_le_iff]
-  intro v
-  cases eq_or_ne u v <;> simp_all [edist_top_of_ne]
-
-proof_wanted eq_top_iff_forall_eccent_eq_one [Nontrivial α] :
-    G = ⊤ ↔ ∀ u, G.eccent u = 1
-
-end eccent
-
 /--
 The diameter is the greatest distance between any two vertices. If the graph is disconnected,
 this will be `0`.
@@ -114,34 +56,6 @@ lemma nontrivial_of_diam_ne_zero' (h : G.diam ≠ 0) : Nontrivial α := by
   rw [not_nontrivial_iff_subsingleton] at h
   exact diam_eq_zero_of_subsingleton
 
-section radius
-
-/-- The radius of a graph is the minimum eccentricity of its vertices. It's `⊤` for the empty
-graph. -/
-noncomputable def radius (G : SimpleGraph α) : ℕ∞ :=
-  ⨅ u, G.eccent u
-
-/-- The center of a graph is the set of vertices with minimum eccentricity. -/
-noncomputable def center (G : SimpleGraph α) : Set α :=
-  {u | G.eccent u = G.radius}
-
-lemma center_def : G.center = {u | G.eccent u = G.radius} := rfl
-
-lemma radius_le_eccent {u : α} : G.radius ≤ G.eccent u :=
-  iInf_le G.eccent u
-
-proof_wanted radius_le_ediam : G.radius ≤ G.ediam
-
-lemma exists_eccent_eq_radius_of_finite [Nonempty α] [Finite α] :
-    ∃ u, G.eccent u = G.radius :=
-  exists_eq_ciInf_of_finite
-
-lemma center_nonempty_of_finite [Nonempty α] [Finite α] : G.center.Nonempty :=
-  exists_eccent_eq_radius_of_finite
-
-proof_wanted diam_le_two_mul_radius (h : G.center.Nonempty) : G.diam ≤ 2 * G.radius
-
-end radius
 
 section Path
 open Path

FormalConjectures/ForMathlib/Combinatorics/SimpleGraph/GraphConjectures/Invariants.lean

@@ -17,6 +17,7 @@ limitations under the License.
 import FormalConjectures.ForMathlib.Combinatorics.SimpleGraph.GraphConjectures.Definitions
 import FormalConjectures.ForMathlib.Combinatorics.SimpleGraph.GraphConjectures.Domination
 import Mathlib.Combinatorics.SimpleGraph.Metric
+import Mathlib.Data.Multiset.Sort
 import Mathlib.Order.CompletePartialOrder
 
 namespace SimpleGraph

FormalConjectures/ForMathlib/Geometry/2d.lean

@@ -18,7 +18,7 @@ import Mathlib.LinearAlgebra.Orientation
 import Mathlib.Analysis.InnerProductSpace.PiL2
 import Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
 import Mathlib.Geometry.Euclidean.Triangle
-import FormalConjectures.ForMathlib.Logic.Equiv.Fin
+import FormalConjectures.ForMathlib.Logic.Equiv.Fin.Rotate
 
 scoped[EuclideanGeometry] notation "ℝ²" => EuclideanSpace ℝ (Fin 2)