bump to nightly-2023-04-27-02

mathlib commit leanprover-community/mathlib@9b2b58d

Mathbin/Algebra/BigOperators/Fin.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov, Anne Baanen
 
 ! This file was ported from Lean 3 source module algebra.big_operators.fin
-! leanprover-community/mathlib commit f16e7a22e11fc09c71f25446ac1db23a24e8a0bd
+! leanprover-community/mathlib commit cdb01be3c499930fd29be05dce960f4d8d201c54
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -25,6 +25,9 @@ The most important results are the induction formulas `fin.prod_univ_cast_succ`
 and `fin.prod_univ_succ`, and the formula `fin.prod_const` for the product of a
 constant function. These results have variants for sums instead of products.
 
+## Main declarations
+
+* `fin_function_fin_equiv`: An explicit equivalence between `fin n → fin m` and `fin (m ^ n)`.
 -/
 
 
@@ -449,6 +452,135 @@ end PartialProd
 
 end Fin
 
+/-- Equivalence between `fin n → fin m` and `fin (m ^ n)`. -/
+@[simps]
+def finFunctionFinEquiv {m n : ℕ} : (Fin n → Fin m) ≃ Fin (m ^ n) :=
+  Equiv.ofRightInverseOfCardLe (le_of_eq <| by simp_rw [Fintype.card_fun, Fintype.card_fin])
+    (fun f =>
+      ⟨∑ i, f i * m ^ (i : ℕ), by
+        induction' n with n ih generalizing f
+        · simp
+        cases m
+        · exact isEmptyElim (f <| Fin.last _)
+        simp_rw [Fin.sum_univ_castSucc, Fin.coe_castSucc, Fin.val_last]
+        refine' (add_lt_add_of_lt_of_le (ih _) <| mul_le_mul_right' (Fin.is_le _) _).trans_eq _
+        rw [← one_add_mul, add_comm, pow_succ]⟩)
+    (fun a b =>
+      ⟨a / m ^ (b : ℕ) % m, by
+        cases n
+        · exact b.elim0
+        cases m
+        · rw [zero_pow n.succ_pos] at a
+          exact a.elim0
+        · exact Nat.mod_lt _ m.succ_pos⟩)
+    fun a => by
+    dsimp
+    induction' n with n ih generalizing a
+    · haveI : Subsingleton (Fin (m ^ 0)) := (Fin.cast <| pow_zero _).toEquiv.Subsingleton
+      exact Subsingleton.elim _ _
+    simp_rw [Fin.forall_iff, Fin.ext_iff, Fin.val_mk] at ih
+    ext
+    simp_rw [Fin.val_mk, Fin.sum_univ_succ, Fin.val_zero, Fin.val_succ, pow_zero, Nat.div_one,
+      mul_one, pow_succ, ← Nat.div_div_eq_div_mul, mul_left_comm _ m, ← mul_sum]
+    rw [ih _ (Nat.div_lt_of_lt_mul a.is_lt), Nat.mod_add_div]
+#align fin_function_fin_equiv finFunctionFinEquiv
+
+theorem finFunctionFinEquiv_apply {m n : ℕ} (f : Fin n → Fin m) :
+    (finFunctionFinEquiv f : ℕ) = ∑ i : Fin n, ↑(f i) * m ^ (i : ℕ) :=
+  rfl
+#align fin_function_fin_equiv_apply finFunctionFinEquiv_apply
+
+theorem finFunctionFinEquiv_single {m n : ℕ} [NeZero m] (i : Fin n) (j : Fin m) :
+    (finFunctionFinEquiv (Pi.single i j) : ℕ) = j * m ^ (i : ℕ) :=
+  by
+  rw [finFunctionFinEquiv_apply, Fintype.sum_eq_single i, Pi.single_eq_same]
+  rintro x hx
+  rw [Pi.single_eq_of_ne hx, Fin.val_zero, MulZeroClass.zero_mul]
+#align fin_function_fin_equiv_single finFunctionFinEquiv_single
+
+/-- Equivalence between `Π i : fin m, fin (n i)` and `fin (∏ i : fin m, n i)`. -/
+def finPiFinEquiv {m : ℕ} {n : Fin m → ℕ} : (∀ i : Fin m, Fin (n i)) ≃ Fin (∏ i : Fin m, n i) :=
+  Equiv.ofRightInverseOfCardLe (le_of_eq <| by simp_rw [Fintype.card_pi, Fintype.card_fin])
+    (fun f =>
+      ⟨∑ i, f i * ∏ j, n (Fin.castLE i.is_lt.le j),
+        by
+        induction' m with m ih generalizing f
+        · simp
+        rw [Fin.prod_univ_castSucc, Fin.sum_univ_castSucc]
+        suffices
+          ∀ (n : Fin m → ℕ) (nn : ℕ) (f : ∀ i : Fin m, Fin (n i)) (fn : Fin nn),
+            ((∑ i : Fin m, ↑(f i) * ∏ j : Fin i, n (Fin.castLE i.prop.le j)) + ↑fn * ∏ j, n j) <
+              (∏ i : Fin m, n i) * nn
+          by
+          replace this := this (Fin.init n) (n (Fin.last _)) (Fin.init f) (f (Fin.last _))
+          rw [← Fin.snoc_init_self f]
+          simp (config := { singlePass := true }) only [← Fin.snoc_init_self n]
+          simp_rw [Fin.snoc_cast_succ, Fin.init_snoc, Fin.snoc_last, Fin.snoc_init_self n]
+          exact this
+        intro n nn f fn
+        cases nn
+        · exact isEmptyElim fn
+        refine' (add_lt_add_of_lt_of_le (ih _) <| mul_le_mul_right' (Fin.is_le _) _).trans_eq _
+        rw [← one_add_mul, mul_comm, add_comm]⟩)
+    (fun a b =>
+      ⟨(a / ∏ j : Fin b, n (Fin.castLE b.is_lt.le j)) % n b,
+        by
+        cases m
+        · exact b.elim0
+        cases' h : n b with nb
+        · rw [prod_eq_zero (Finset.mem_univ _) h] at a
+          exact isEmptyElim a
+        exact Nat.mod_lt _ nb.succ_pos⟩)
+    (by
+      intro a; revert a; dsimp only [Fin.val_mk]
+      refine' Fin.consInduction _ _ n
+      · intro a
+        haveI : Subsingleton (Fin (∏ i : Fin 0, i.elim0ₓ)) :=
+          (Fin.cast <| prod_empty).toEquiv.Subsingleton
+        exact Subsingleton.elim _ _
+      · intro n x xs ih a
+        simp_rw [Fin.forall_iff, Fin.ext_iff, Fin.val_mk] at ih
+        ext
+        simp_rw [Fin.val_mk, Fin.sum_univ_succ, Fin.cons_succ]
+        have := fun i : Fin n =>
+          Fintype.prod_equiv (Fin.cast <| Fin.val_succ i).toEquiv
+            (fun j => (Fin.cons x xs : _ → ℕ) (Fin.castLE (Fin.is_lt _).le j))
+            (fun j => (Fin.cons x xs : _ → ℕ) (Fin.castLE (Nat.succ_le_succ (Fin.is_lt _).le) j))
+            fun j => rfl
+        simp_rw [this]
+        clear this
+        dsimp only [Fin.val_zero]
+        simp_rw [Fintype.prod_empty, Nat.div_one, mul_one, Fin.cons_zero, Fin.prod_univ_succ]
+        change (_ + ∑ y : _, _ / (x * _) % _ * (x * _)) = _
+        simp_rw [← Nat.div_div_eq_div_mul, mul_left_comm (_ % _ : ℕ), ← mul_sum]
+        convert Nat.mod_add_div _ _
+        refine' Eq.trans _ (ih (a / x) (Nat.div_lt_of_lt_mul <| a.is_lt.trans_eq _))
+        swap
+        · convert Fin.prod_univ_succ (Fin.cons x xs : ∀ _, ℕ)
+          simp_rw [Fin.cons_succ]
+        congr with i
+        congr with j
+        · cases j
+          rfl
+        · cases j
+          rfl)
+#align fin_pi_fin_equiv finPiFinEquiv
+
+theorem finPiFinEquiv_apply {m : ℕ} {n : Fin m → ℕ} (f : ∀ i : Fin m, Fin (n i)) :
+    (finPiFinEquiv f : ℕ) = ∑ i, f i * ∏ j, n (Fin.castLE i.is_lt.le j) :=
+  rfl
+#align fin_pi_fin_equiv_apply finPiFinEquiv_apply
+
+theorem finPiFinEquiv_single {m : ℕ} {n : Fin m → ℕ} [∀ i, NeZero (n i)] (i : Fin m)
+    (j : Fin (n i)) :
+    (finPiFinEquiv (Pi.single i j : ∀ i : Fin m, Fin (n i)) : ℕ) =
+      j * ∏ j, n (Fin.castLE i.is_lt.le j) :=
+  by
+  rw [finPiFinEquiv_apply, Fintype.sum_eq_single i, Pi.single_eq_same]
+  rintro x hx
+  rw [Pi.single_eq_of_ne hx, Fin.val_zero, MulZeroClass.zero_mul]
+#align fin_pi_fin_equiv_single finPiFinEquiv_single
+
 namespace List
 
 section CommMonoid

Mathbin/Algebra/Quaternion.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 
 ! This file was ported from Lean 3 source module algebra.quaternion
-! leanprover-community/mathlib commit 039a089d2a4b93c761b234f3e5f5aeb752bac60f
+! leanprover-community/mathlib commit dc7ac07acd84584426773e69e51035bea9a770e7
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -612,10 +612,23 @@ theorem conj_add : (a + b).conj = a.conj + b.conj :=
 theorem conj_mul : (a * b).conj = b.conj * a.conj := by ext <;> simp <;> ring
 #align quaternion_algebra.conj_mul QuaternionAlgebra.conj_mul
 
-theorem conj_conj_mul : (a.conj * b).conj = b.conj * a := by rw [conj_mul, conj_conj]
+instance : StarRing ℍ[R,c₁,c₂] where
+  unit := conj
+  star_involutive := conj_conj
+  star_add := conj_add
+  star_mul := conj_mul
+
+@[simp]
+theorem star_def (a : ℍ[R,c₁,c₂]) : star a = conj a :=
+  rfl
+#align quaternion_algebra.star_def QuaternionAlgebra.star_def
+
+theorem conj_conj_mul : (a.conj * b).conj = b.conj * a :=
+  star_star_mul _ _
 #align quaternion_algebra.conj_conj_mul QuaternionAlgebra.conj_conj_mul
 
-theorem conj_mul_conj : (a * b.conj).conj = b * a.conj := by rw [conj_mul, conj_conj]
+theorem conj_mul_conj : (a * b.conj).conj = b * a.conj :=
+  star_mul_star _ _
 #align quaternion_algebra.conj_mul_conj QuaternionAlgebra.conj_mul_conj
 
 theorem self_add_conj' : a + a.conj = ↑(2 * a.re) := by ext <;> simp [two_mul]
@@ -645,11 +658,7 @@ theorem commute_self_conj : Commute a a.conj :=
 #align quaternion_algebra.commute_self_conj QuaternionAlgebra.commute_self_conj
 
 theorem commute_conj_conj {a b : ℍ[R,c₁,c₂]} (h : Commute a b) : Commute a.conj b.conj :=
-  calc
-    a.conj * b.conj = (b * a).conj := (conj_mul b a).symm
-    _ = (a * b).conj := by rw [h.eq]
-    _ = b.conj * a.conj := conj_mul a b
-
+  h.star_star
 #align quaternion_algebra.commute_conj_conj QuaternionAlgebra.commute_conj_conj
 
 @[simp, norm_cast]
@@ -662,11 +671,13 @@ theorem conj_im : conj a.im = -a.im :=
 #align quaternion_algebra.conj_im QuaternionAlgebra.conj_im
 
 @[simp, norm_cast]
-theorem conj_nat_cast (n : ℕ) : conj (n : ℍ[R,c₁,c₂]) = n := by rw [← coe_nat_cast, conj_coe]
+theorem conj_nat_cast (n : ℕ) : conj (n : ℍ[R,c₁,c₂]) = n :=
+  @star_natCast ℍ[R,c₁,c₂] _ _ n
 #align quaternion_algebra.conj_nat_cast QuaternionAlgebra.conj_nat_cast
 
 @[simp, norm_cast]
-theorem conj_int_cast (z : ℤ) : conj (z : ℍ[R,c₁,c₂]) = z := by rw [← coe_int_cast, conj_coe]
+theorem conj_int_cast (z : ℤ) : conj (z : ℍ[R,c₁,c₂]) = z :=
+  @star_intCast ℍ[R,c₁,c₂] _ _ z
 #align quaternion_algebra.conj_int_cast QuaternionAlgebra.conj_int_cast
 
 @[simp]
@@ -725,17 +736,6 @@ theorem conj_sub : (a - b).conj = a.conj - b.conj :=
   (conj : ℍ[R,c₁,c₂] ≃ₗ[R] _).map_sub a b
 #align quaternion_algebra.conj_sub QuaternionAlgebra.conj_sub
 
-instance : StarRing ℍ[R,c₁,c₂] where
-  unit := conj
-  star_involutive := conj_conj
-  star_add := conj_add
-  star_mul := conj_mul
-
-@[simp]
-theorem star_def (a : ℍ[R,c₁,c₂]) : star a = conj a :=
-  rfl
-#align quaternion_algebra.star_def QuaternionAlgebra.star_def
-
 @[simp]
 theorem conj_pow (n : ℕ) : (a ^ n).conj = a.conj ^ n :=
   star_pow _ _

Mathbin/Algebra/Star/Basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 
 ! This file was ported from Lean 3 source module algebra.star.basic
-! leanprover-community/mathlib commit 30413fc89f202a090a54d78e540963ed3de0056e
+! leanprover-community/mathlib commit dc7ac07acd84584426773e69e51035bea9a770e7
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -113,6 +113,11 @@ theorem star_injective [InvolutiveStar R] : Function.Injective (star : R → R)
 #align star_injective star_injective
 -/
 
+@[simp]
+theorem star_inj [InvolutiveStar R] {x y : R} : star x = star y ↔ x = y :=
+  star_injective.eq_iff
+#align star_inj star_inj
+
 #print Equiv.star /-
 /-- `star` as an equivalence when it is involutive. -/
 protected def Equiv.star [InvolutiveStar R] : Equiv.Perm R :=
@@ -162,6 +167,39 @@ export StarSemigroup (star_mul)
 
 attribute [simp] star_mul
 
+section StarSemigroup
+
+variable [Semigroup R] [StarSemigroup R]
+
+theorem star_star_mul (x y : R) : star (star x * y) = star y * x := by rw [star_mul, star_star]
+#align star_star_mul star_star_mul
+
+theorem star_mul_star (x y : R) : star (x * star y) = y * star x := by rw [star_mul, star_star]
+#align star_mul_star star_mul_star
+
+@[simp]
+theorem semiconjBy_star_star_star {x y z : R} :
+    SemiconjBy (star x) (star z) (star y) ↔ SemiconjBy x y z := by
+  simp_rw [SemiconjBy, ← star_mul, star_inj, eq_comm]
+#align semiconj_by_star_star_star semiconjBy_star_star_star
+
+alias semiconjBy_star_star_star ↔ _ SemiconjBy.star_star_star
+#align semiconj_by.star_star_star SemiconjBy.star_star_star
+
+@[simp]
+theorem commute_star_star {x y : R} : Commute (star x) (star y) ↔ Commute x y :=
+  semiconjBy_star_star_star
+#align commute_star_star commute_star_star
+
+alias commute_star_star ↔ _ Commute.star_star
+#align commute.star_star Commute.star_star
+
+theorem commute_star_comm {x y : R} : Commute (star x) y ↔ Commute x (star y) := by
+  rw [← commute_star_star, star_star]
+#align commute_star_comm commute_star_comm
+
+end StarSemigroup
+
 /- warning: star_mul' -> star_mul' is a dubious translation:
 lean 3 declaration is
   forall {R : Type.{u1}} [_inst_1 : CommSemigroup.{u1} R] [_inst_2 : StarSemigroup.{u1} R (CommSemigroup.toSemigroup.{u1} R _inst_1)] (x : R) (y : R), Eq.{succ u1} R (Star.star.{u1} R (InvolutiveStar.toHasStar.{u1} R (StarSemigroup.toHasInvolutiveStar.{u1} R (CommSemigroup.toSemigroup.{u1} R _inst_1) _inst_2)) (HMul.hMul.{u1, u1, u1} R R R (instHMul.{u1} R (Semigroup.toHasMul.{u1} R (CommSemigroup.toSemigroup.{u1} R _inst_1))) x y)) (HMul.hMul.{u1, u1, u1} R R R (instHMul.{u1} R (Semigroup.toHasMul.{u1} R (CommSemigroup.toSemigroup.{u1} R _inst_1))) (Star.star.{u1} R (InvolutiveStar.toHasStar.{u1} R (StarSemigroup.toHasInvolutiveStar.{u1} R (CommSemigroup.toSemigroup.{u1} R _inst_1) _inst_2)) x) (Star.star.{u1} R (InvolutiveStar.toHasStar.{u1} R (StarSemigroup.toHasInvolutiveStar.{u1} R (CommSemigroup.toSemigroup.{u1} R _inst_1) _inst_2)) y))

Mathbin/AlgebraicGeometry/OpenImmersion.lean

@@ -4,14 +4,15 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Andrew Yang
 
 ! This file was ported from Lean 3 source module algebraic_geometry.open_immersion
-! leanprover-community/mathlib commit d39590fc8728fbf6743249802486f8c91ffe07bc
+! leanprover-community/mathlib commit 178a32653e369dce2da68dc6b2694e385d484ef1
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
 import Mathbin.AlgebraicGeometry.PresheafedSpace.HasColimits
 import Mathbin.CategoryTheory.Limits.Shapes.BinaryProducts
 import Mathbin.CategoryTheory.Limits.Preserves.Shapes.Pullbacks
 import Mathbin.Topology.Sheaves.Functors
+import Mathbin.Topology.Category.Top.Limits.Pullbacks
 import Mathbin.AlgebraicGeometry.Scheme
 import Mathbin.CategoryTheory.Limits.Shapes.StrictInitial
 import Mathbin.CategoryTheory.Limits.Shapes.CommSq

Mathbin/AlgebraicGeometry/PresheafedSpace/HasColimits.lean

@@ -4,12 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 
 ! This file was ported from Lean 3 source module algebraic_geometry.presheafed_space.has_colimits
-! leanprover-community/mathlib commit d39590fc8728fbf6743249802486f8c91ffe07bc
+! leanprover-community/mathlib commit 178a32653e369dce2da68dc6b2694e385d484ef1
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
 import Mathbin.AlgebraicGeometry.PresheafedSpace
-import Mathbin.Topology.Category.Top.Limits
+import Mathbin.Topology.Category.Top.Limits.Basic
 import Mathbin.Topology.Sheaves.Limits
 
 /-!

Mathbin/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean

@@ -372,8 +372,8 @@ private unsafe def mem_tac : tactic Unit :=
 
 include f_deg
 
-/- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:69:18: unsupported non-interactive tactic _private.2197349699.mem_tac -/
-/- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:69:18: unsupported non-interactive tactic _private.2197349699.mem_tac -/
+/- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:69:18: unsupported non-interactive tactic _private.1492521391.mem_tac -/
+/- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:69:18: unsupported non-interactive tactic _private.1492521391.mem_tac -/
 /-- The function from `Spec A⁰_f` to `Proj|D(f)` is defined by `q ↦ {a | aᵢᵐ/fⁱ ∈ q}`, i.e. sending
 `q` a prime ideal in `A⁰_f` to the homogeneous prime relevant ideal containing only and all the
 elements `a : A` such that for every `i`, the degree 0 element formed by dividing the `m`-th power
@@ -403,8 +403,8 @@ def carrier (q : Spec.T A⁰_ f) : Set A :=
         q.1 }
 #align algebraic_geometry.Proj_iso_Spec_Top_component.from_Spec.carrier AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier
 
-/- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:69:18: unsupported non-interactive tactic _private.2197349699.mem_tac -/
-/- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:69:18: unsupported non-interactive tactic _private.2197349699.mem_tac -/
+/- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:69:18: unsupported non-interactive tactic _private.1492521391.mem_tac -/
+/- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:69:18: unsupported non-interactive tactic _private.1492521391.mem_tac -/
 theorem mem_carrier_iff (q : Spec.T A⁰_ f) (a : A) :
     a ∈ carrier f_deg q ↔
       ∀ i,
@@ -442,14 +442,14 @@ theorem mem_carrier_iff' (q : Spec.T A⁰_ f) (a : A) :
         rfl)
 #align algebraic_geometry.Proj_iso_Spec_Top_component.from_Spec.mem_carrier_iff' AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.mem_carrier_iff'
 
-/- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:69:18: unsupported non-interactive tactic _private.2197349699.mem_tac -/
-/- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:69:18: unsupported non-interactive tactic _private.2197349699.mem_tac -/
-/- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:69:18: unsupported non-interactive tactic _private.2197349699.mem_tac -/
-/- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:69:18: unsupported non-interactive tactic _private.2197349699.mem_tac -/
-/- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:69:18: unsupported non-interactive tactic _private.2197349699.mem_tac -/
-/- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:69:18: unsupported non-interactive tactic _private.2197349699.mem_tac -/
-/- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:69:18: unsupported non-interactive tactic _private.2197349699.mem_tac -/
-/- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:69:18: unsupported non-interactive tactic _private.2197349699.mem_tac -/
+/- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:69:18: unsupported non-interactive tactic _private.1492521391.mem_tac -/
+/- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:69:18: unsupported non-interactive tactic _private.1492521391.mem_tac -/
+/- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:69:18: unsupported non-interactive tactic _private.1492521391.mem_tac -/
+/- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:69:18: unsupported non-interactive tactic _private.1492521391.mem_tac -/
+/- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:69:18: unsupported non-interactive tactic _private.1492521391.mem_tac -/
+/- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:69:18: unsupported non-interactive tactic _private.1492521391.mem_tac -/
+/- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:69:18: unsupported non-interactive tactic _private.1492521391.mem_tac -/
+/- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:69:18: unsupported non-interactive tactic _private.1492521391.mem_tac -/
 theorem carrier.add_mem (q : Spec.T A⁰_ f) {a b : A} (ha : a ∈ carrier f_deg q)
     (hb : b ∈ carrier f_deg q) : a + b ∈ carrier f_deg q :=
   by
@@ -541,8 +541,8 @@ theorem carrier.zero_mem : (0 : A) ∈ carrier f_deg q := fun i =>
   convert Localization.mk_zero _ using 1
 #align algebraic_geometry.Proj_iso_Spec_Top_component.from_Spec.carrier.zero_mem AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier.zero_mem
 
-/- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:69:18: unsupported non-interactive tactic _private.2197349699.mem_tac -/
-/- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:69:18: unsupported non-interactive tactic _private.2197349699.mem_tac -/
+/- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:69:18: unsupported non-interactive tactic _private.1492521391.mem_tac -/
+/- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:69:18: unsupported non-interactive tactic _private.1492521391.mem_tac -/
 theorem carrier.smul_mem (c x : A) (hx : x ∈ carrier f_deg q) : c • x ∈ carrier f_deg q :=
   by
   revert c