almost nothing

DividedPowers/DPAlgebra/PolynomialMap.lean

@@ -117,17 +117,14 @@ example {N : Type*} [AddCommGroup N] [Module R N] (n : ℕ) :
 noncomputable
 def grade_basis (n : ℕ) {ι : Type*} (b : Basis ι R M) :
     Basis { h : ι →₀ ℕ // (h.sum fun i n ↦ n) = n } R (grade R M n) := by
-  let v : (ι →₀ ℕ) → DividedPowerAlgebra R M :=
-    fun h ↦ h.prod (fun i n ↦ dp R n (b i))
+  let v (h : ι →₀ ℕ) : DividedPowerAlgebra R M := h.prod (fun i n ↦ dp R n (b i))
   have hv : ∀ h, v h ∈ grade R M (h.sum fun i n ↦ n) := sorry
-  have v' : { h : ι →₀ ℕ // (h.sum fun i n ↦ n) = n} → grade R M n :=
-    fun ⟨h, hh⟩ ↦ ⟨v h, by rw [← hh]; apply hv⟩
+  set v' : { h : ι →₀ ℕ // (h.sum fun i n ↦ n) = n} → grade R M n :=
+    fun ⟨h, hh⟩ ↦ ⟨v h, by rw [← hh]; apply hv⟩ with hv'
   apply Basis.mk (v := v')
-  · /- Linear independence is the difficult part, it relies on the PolynomialMap
-       interpretation -/
+  · /- Linear independence is the difficult part, it relies on the PolynomialMap interpretation -/
     sorry
-  · /- It should be easy to prove that these elements generate
-      * the `dp R n (b i)` generate -/
+  · /- It should be easy to prove that the `dp R n (b i)` generate -/
     sorry
 
 theorem grade_free [Module.Free R M] (n : ℕ): Module.Free R (grade R M n) :=

DividedPowers/ForMathlib/GradedBaseChange.lean

@@ -51,7 +51,7 @@ constructor
   · rintro _ ⟨x, hx, rfl⟩
     simp only [mk_apply, LinearMap.mem_range]
     use 1 ⊗ₜ[R] (⟨x, hx⟩ : p)
-    simp only [LinearMap.baseChange_tmul, Submodule.coeSubtype]
+    simp only [LinearMap.baseChange_tmul, Submodule.coe_subtype]
   · exact zero_mem _
   · intro x y hx hy
     exact add_mem hx hy
@@ -61,7 +61,7 @@ constructor
   induction x using TensorProduct.induction_on with
   | zero => simp
   | tmul a x =>
-    simp only [LinearMap.baseChange_tmul, coeSubtype]
+    simp only [LinearMap.baseChange_tmul, coe_subtype]
     exact tmul_mem_baseChange_of_mem a (coe_mem x)
   | add x y hx hy =>
     simp only [map_add]
@@ -129,7 +129,7 @@ theorem Decompose.baseChange.decompose_of_mem {m : S ⊗[R] M} {i : ι}
     rw [LinearMap.map_add, px, py, eq_comm]
     simp only [← DirectSum.lof_eq_of S]
     convert LinearMap.map_add _ _ _
-    simp only [AddSubmonoid.mk_add_mk, Submodule.map_coe]
+    simp only [AddMemClass.mk_add_mk, Submodule.map_coe]
   · intro s x hx px
     rw [LinearMap.map_smul, px, eq_comm]
     simp only [← DirectSum.lof_eq_of S]

DividedPowers/IdealAdd2.lean

@@ -56,7 +56,7 @@ noncomputable def _root_.Submodule.quotientCoprodAddEquiv :
   rintro ⟨x, hx⟩ _
   obtain ⟨y, hy, z, hz, rfl⟩ := mem_sup.mp hx
   use ⟨⟨y, hy⟩, ⟨z, hz⟩⟩
-  simp [← Subtype.coe_inj]
+  simp only [coprod_apply, ← Subtype.coe_inj, coe_add, coe_inclusion]
 
 noncomputable def onSup (h : ∀ x (hM : x ∈ M) (hN : x ∈ N), f ⟨x, hM⟩ = g ⟨x, hN⟩) :
     M + N →ₗ[A] Y := by