Fix broken commit, bump mathlib

Signed-off-by: zeramorphic <[email protected]>
leanprover-community · Dec 21, 2023 · 99703ba · 99703ba
1 parent cf756dd
commit 99703ba
Show file tree

Hide file tree

Showing 4 changed files with 26 additions and 3 deletions.
diff --git a/ConNF/Counting/Spec.lean b/ConNF/Counting/Spec.lean
@@ -1,3 +1,4 @@
+import ConNF.Mathlib.Support
 import ConNF.FOA.Basic.Flexible
 import ConNF.Counting.CodingFunction
 
@@ -321,7 +322,7 @@ theorem specFor_smul_inflexibleCoe {S : Support β} {A : ExtendedIndex β} {N :
           (Allowable.comp (h.path.B.cons h.path.hδ) ρ) ?_ ?_
       · simp only [smul_support, this]
       · rw [Enumeration.smul_carrier]
-        exact (support_supports h.t).smul (Allowable.comp (h.path.B.cons h.path.hδ) ρ)
+        exact (support_supports h.t).smul' (Allowable.comp (h.path.B.cons h.path.hδ) ρ)
       · exact support_supports h.t
   · rw [← ih h.path.δ (coe_lt_coe.mp h.δ_lt_β)
       (S.comp (h.path.B.cons h.path.hδ) + h.t.support) (Allowable.comp (h.path.B.cons h.path.hδ) ρ)]

diff --git a/ConNF/Mathlib.lean b/ConNF/Mathlib.lean
@@ -8,5 +8,6 @@ import ConNF.Mathlib.Ordinal
 import ConNF.Mathlib.Equiv
 import ConNF.Mathlib.Group
 import ConNF.Mathlib.GroupAction
+import ConNF.Mathlib.Support
 import ConNF.Mathlib.Transfer
 import ConNF.Mathlib.Logic.Equiv.PartialPerm
diff --git a/ConNF/Mathlib/Support.lean b/ConNF/Mathlib/Support.lean
@@ -0,0 +1,21 @@
+import Mathlib.GroupTheory.GroupAction.Support
+
+open Pointwise
+
+variable {G H α β : Type*}
+
+namespace MulAction
+
+variable [Group G] [MulAction G α] [MulAction G β] {s t : Set α} {b : β}
+
+@[to_additive]
+theorem Supports.smul' (g : G) (h : Supports G s b) : Supports G (g • s) (g • b) := by
+  rintro g' hg'
+  have := h (g⁻¹ * g' * g) ?_
+  · rw [mul_smul, mul_smul, inv_smul_eq_iff] at this
+    exact this
+  · rintro a ha
+    rw [mul_smul, mul_smul, inv_smul_eq_iff]
+    exact Set.ball_image_iff.1 hg' a ha
+
+end MulAction
diff --git a/lake-manifest.json b/lake-manifest.json
@@ -4,7 +4,7 @@
  [{"url": "https://github.com/leanprover/std4",
    "type": "git",
    "subDir": null,
-   "rev": "9dd24a3493cceefa2bede383f21e4ef548990b68",
+   "rev": "5bf9172331fb4de21647a919c64d3569839b63c6",
    "name": "std",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -49,7 +49,7 @@
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
-   "rev": "9e1e18da15a810d7f193da8afc09b6fcc89bd5dd",
+   "rev": "e7c657f3b4b6f175895c3c1143a5275d24ba418c",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,