[Merged by Bors] - chore: Remove unnecessary "rw"s #10704

darabos · 2024-02-18T21:38:51Z

Remove unnecessary "rw"s.

This is a non-forked and updated version of #10338. I figure if the proofs still work without these rewrites, then it's best if we remove them, right?

…-rws

Vierkantor

Impressive work! I hope you used some sort of automation for this, you didn't open up every file and go through every rw by hand, right?!

I think we should slightly more careful in removing rw rules here: if the two sides happen to be definitionally equal according to rfl, we don't always have that rw sees this too. The latter is important if the context changes and we need to add an additional rw step. So I went through and suggested to revert every change where the two sides did not end up exactly the same (at least, the same as far as rw is concerned). On the other hand, it seems much easier to implement automation for trimming a rw set if the only criteria are that the proof still goes through. And maybe some types of definitional equalities are more acceptable than others, so I labeled each of the suggestions.

What do you think?

Vierkantor · 2024-02-19T14:24:32Z

Mathlib/Algebra/DirectSum/Decomposition.lean

@@ -135,7 +135,7 @@ theorem decompose_of_mem {x : M} {i : ι} (hx : x ∈ ℳ i) :
 #align direct_sum.decompose_of_mem DirectSum.decompose_of_mem

 theorem decompose_of_mem_same {x : M} {i : ι} (hx : x ∈ ℳ i) : (decompose ℳ x i : M) = x := by
-  rw [decompose_of_mem _ hx, DirectSum.of_eq_same, Subtype.coe_mk]
+  rw [decompose_of_mem _ hx, DirectSum.of_eq_same]


Closing this goal requires reducing the same projection as Subtype.coe_mk does, so let's keep it:

Suggested change

rw [decompose_of_mem _ hx, DirectSum.of_eq_same]

rw [decompose_of_mem _ hx, DirectSum.of_eq_same, Subtype.coe_mk]

Vierkantor · 2024-02-19T14:26:29Z

Mathlib/Algebra/Module/Zlattice.lean

@@ -162,7 +162,7 @@ theorem fract_zspan_add (m : E) {v : E} (h : v ∈ span ℤ (Set.range b)) :
  simp_rw [repr_fract_apply, Int.fract_eq_fract]
  use (b.restrictScalars ℤ).repr ⟨v, h⟩ i
  rw [map_add, Finsupp.coe_add, Pi.add_apply, add_tsub_cancel_right,
-    ← eq_intCast (algebraMap ℤ K) _, Basis.restrictScalars_repr_apply, coe_mk]
+    ← eq_intCast (algebraMap ℤ K) _, Basis.restrictScalars_repr_apply]


This is another projection reduction that I would like to keep:

Suggested change

← eq_intCast (algebraMap ℤ K) _, Basis.restrictScalars_repr_apply]

← eq_intCast (algebraMap ℤ K) _, Basis.restrictScalars_repr_apply, coe_mk]

Vierkantor · 2024-02-19T14:27:03Z

Mathlib/Algebra/MonoidAlgebra/Grading.lean

@@ -183,7 +183,7 @@ instance gradeBy.gradedAlgebra : GradedAlgebra (gradeBy R f) :=
      ext : 2
      simp only [MonoidHom.coe_comp, MonoidHom.coe_coe, AlgHom.coe_comp, Function.comp_apply,
        of_apply, AlgHom.coe_id, id_eq]
-      rw [decomposeAux_single, DirectSum.coeAlgHom_of, Subtype.coe_mk])
+      rw [decomposeAux_single, DirectSum.coeAlgHom_of])


idem:

Suggested change

rw [decomposeAux_single, DirectSum.coeAlgHom_of])

rw [decomposeAux_single, DirectSum.coeAlgHom_of, Subtype.coe_mk])

Vierkantor · 2024-02-19T14:28:39Z

Mathlib/AlgebraicGeometry/StructureSheaf.lean

@@ -386,7 +386,7 @@ theorem const_ext {f₁ f₂ g₁ g₂ : R} {U hu₁ hu₂} (h : f₁ * g₂ = f
    const R f₁ g₁ U hu₁ = const R f₂ g₂ U hu₂ :=
  Subtype.eq <|
    funext fun x =>
-      IsLocalization.mk'_eq_of_eq (by rw [mul_comm, Subtype.coe_mk, ← h, mul_comm, Subtype.coe_mk])
+      IsLocalization.mk'_eq_of_eq (by rw [mul_comm, Subtype.coe_mk, ← h, mul_comm])


idem:

Suggested change

IsLocalization.mk'_eq_of_eq (by rw [mul_comm, Subtype.coe_mk, ← h, mul_comm])

IsLocalization.mk'_eq_of_eq (by rw [mul_comm, Subtype.coe_mk, ← h, mul_comm, Subtype.coe_mk])

Vierkantor · 2024-02-19T14:29:03Z

Mathlib/Analysis/Analytic/Composition.lean

@@ -115,7 +115,7 @@ theorem applyComposition_ones (p : FormalMultilinearSeries 𝕜 E F) (n : ℕ) :
  intro j hjn hj1
  obtain rfl : j = 0 := by linarith
  refine' congr_arg v _
-  rw [Fin.ext_iff, Fin.coe_castLE, Composition.ones_embedding, Fin.val_mk]
+  rw [Fin.ext_iff, Fin.coe_castLE, Composition.ones_embedding]


idem:

Suggested change

rw [Fin.ext_iff, Fin.coe_castLE, Composition.ones_embedding]

rw [Fin.ext_iff, Fin.coe_castLE, Composition.ones_embedding, Fin.val_mk]

Vierkantor · 2024-02-19T15:22:40Z

Mathlib/RingTheory/IsAdjoinRoot.lean

      _ = Pi.single (f := fun _ => R) ((⟨n, hn⟩ : Fin _) : ℕ) (1 : (fun _ => R) n)
        ↑(⟨i, _⟩ : Fin _) := by
        rw [h.basis.repr_self, ← Finsupp.single_eq_pi_single,
          Finsupp.single_apply_left Fin.val_injective]
-      _ = Pi.single (f := fun _ => R) n 1 i := by rw [Fin.val_mk, Fin.val_mk]
+      _ = Pi.single (f := fun _ => R) n 1 i := by rw [Fin.val_mk]


Structure projection:

Suggested change

_ = Pi.single (f := fun _ => R) n 1 i := by rw [Fin.val_mk]

_ = Pi.single (f := fun _ => R) n 1 i := by rw [Fin.val_mk, Fin.val_mk]

or alternatively:

Suggested change

_ = Pi.single (f := fun _ => R) n 1 i := by rw [Fin.val_mk]

_ = Pi.single (f := fun _ => R) n 1 i := rfl

Vierkantor · 2024-02-19T15:26:20Z

Mathlib/RingTheory/UniqueFactorizationDomain.lean

@@ -1696,7 +1696,7 @@ theorem factors_prime_pow [Nontrivial α] {p : Associates α} (hp : Irreducible
  eq_of_prod_eq_prod
    (by
      rw [Associates.factors_prod, FactorSet.prod]
-      dsimp; rw [Multiset.map_replicate, Multiset.prod_replicate, Subtype.coe_mk])
+      dsimp; rw [Multiset.map_replicate, Multiset.prod_replicate])


Structure projection:

Suggested change

dsimp; rw [Multiset.map_replicate, Multiset.prod_replicate])

dsimp; rw [Multiset.map_replicate, Multiset.prod_replicate, Subtype.coe_mk])

Vierkantor · 2024-02-19T15:27:16Z

Mathlib/RingTheory/WittVector/Truncated.lean

@@ -112,7 +112,7 @@ def out (x : TruncatedWittVector p n R) : 𝕎 R :=

 @[simp]
 theorem coeff_out (x : TruncatedWittVector p n R) (i : Fin n) : x.out.coeff i = x.coeff i := by
-  rw [out]; dsimp only; rw [dif_pos i.is_lt, Fin.eta]
+  rw [out]; dsimp only; rw [dif_pos i.is_lt]


Structure eta:

Suggested change

rw [out]; dsimp only; rw [dif_pos i.is_lt]

rw [out]; dsimp only; rw [dif_pos i.is_lt, Fin.eta]

Vierkantor · 2024-02-19T15:27:30Z

Mathlib/RingTheory/WittVector/Truncated.lean

@@ -153,7 +153,7 @@ theorem out_truncateFun (x : 𝕎 R) : (truncateFun n x).out = init n x := by
  ext i
  dsimp [TruncatedWittVector.out, init, select, coeff_mk]
  split_ifs with hi; swap; · rfl
-  rw [coeff_truncateFun, Fin.val_mk]
+  rw [coeff_truncateFun]


Structure projection:

Suggested change

rw [coeff_truncateFun]

rw [coeff_truncateFun, Fin.val_mk]

Vierkantor · 2024-02-19T15:30:43Z

Mathlib/Topology/MetricSpace/GromovHausdorff.lean

@@ -858,7 +858,7 @@ theorem totallyBounded {t : Set GHSpace} {C : ℝ} {u : ℕ → ℝ} {K : ℕ
      rcases mem_iUnion₂.1 this with ⟨y, ys, hy⟩
      let i : ℕ := E q ⟨y, ys⟩
      let hi := ((E q) ⟨y, ys⟩).2
-      have ihi_eq : (⟨i, hi⟩ : Fin (N q)) = (E q) ⟨y, ys⟩ := by rw [Fin.ext_iff, Fin.val_mk]
+      have ihi_eq : (⟨i, hi⟩ : Fin (N q)) = (E q) ⟨y, ys⟩ := by rw [Fin.ext_iff]


Structure projection:

Suggested change

have ihi_eq : (⟨i, hi⟩ : Fin (N q)) = (E q) ⟨y, ys⟩ := by rw [Fin.ext_iff]

have ihi_eq : (⟨i, hi⟩ : Fin (N q)) = (E q) ⟨y, ys⟩ := by rw [Fin.ext_iff, Fin.val_mk]

…actly the same.

darabos · 2024-02-19T17:31:18Z

Impressive work! I hope you used some sort of automation for this, you didn't open up every file and go through every rw by hand, right?!

Haha, no! We're working on a system (machine learning) where the unnecessary rws manifested as errors. I thought this accidental detection may actually be useful for something.

I think we should slightly more careful in removing rw rules here: if the two sides happen to be definitionally equal according to rfl, we don't always have that rw sees this too. The latter is important if the context changes and we need to add an additional rw step. So I went through and suggested to revert every change where the two sides did not end up exactly the same (at least, the same as far as rw is concerned). On the other hand, it seems much easier to implement automation for trimming a rw set if the only criteria are that the proof still goes through. And maybe some types of definitional equalities are more acceptable than others, so I labeled each of the suggestions.

What do you think?

Sorry, I'm too new to Lean to have an opinion on this. I implemented your suggested changes. Thanks for the careful review!

Vierkantor

Thanks! I really appreciate the time you took to deal with these little annoyances.

bors r+

Remove unnecessary "rw"s.

mathlib-bors · 2024-02-20T11:30:20Z

Pull request successfully merged into master.

Build succeeded:

Remove unnecessary "rw"s.

darabos added 2 commits February 18, 2024 22:01

Remove unnecessary "rw"s.

f636b35

Merge remote-tracking branch 'public/master' into darabos-unnecessary…

5350bd2

…-rws

darabos mentioned this pull request Feb 18, 2024

Remove two unnecessary rws #10338

Closed

Vierkantor self-assigned this Feb 19, 2024

Vierkantor added the awaiting-review The author would like community review of the PR label Feb 19, 2024

Vierkantor changed the title ~~Remove unnecessary "rw"s~~ chore: Remove unnecessary "rw"s Feb 19, 2024

Vierkantor reviewed Feb 19, 2024

View reviewed changes

Vierkantor added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Feb 19, 2024

darabos added 2 commits February 19, 2024 18:23

Revert the "rw" simplifications where the two sides did not end up ex…

0ec56ba

…actly the same.

Resolve porting note per @Vierkantor's suggestion.

646dfd9

Vierkantor approved these changes Feb 20, 2024

View reviewed changes

leanprover-community-mathlib4-bot added ready-to-merge This PR has been sent to bors. and removed awaiting-author A reviewer has asked the author a question or requested changes labels Feb 20, 2024

mathlib-bors bot pushed a commit that referenced this pull request Feb 20, 2024

chore: Remove unnecessary "rw"s (#10704)

db5a937

Remove unnecessary "rw"s.

mathlib-bors bot changed the title ~~chore: Remove unnecessary "rw"s~~ [Merged by Bors] - chore: Remove unnecessary "rw"s Feb 20, 2024

mathlib-bors bot closed this Feb 20, 2024

mathlib-bors bot deleted the darabos-unnecessary-rws branch February 20, 2024 11:30

thorimur pushed a commit that referenced this pull request Feb 24, 2024

chore: Remove unnecessary "rw"s (#10704)

ce60eaa

Remove unnecessary "rw"s.

thorimur pushed a commit that referenced this pull request Feb 26, 2024

chore: Remove unnecessary "rw"s (#10704)

04ab60b

Remove unnecessary "rw"s.

riccardobrasca pushed a commit that referenced this pull request Mar 1, 2024

chore: Remove unnecessary "rw"s (#10704)

45f1499

Remove unnecessary "rw"s.

dagurtomas pushed a commit that referenced this pull request Mar 22, 2024

chore: Remove unnecessary "rw"s (#10704)

ad24340

Remove unnecessary "rw"s.

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - chore: Remove unnecessary "rw"s #10704

[Merged by Bors] - chore: Remove unnecessary "rw"s #10704

darabos commented Feb 18, 2024

Vierkantor left a comment

Vierkantor Feb 19, 2024

Vierkantor Feb 19, 2024

Vierkantor Feb 19, 2024

Vierkantor Feb 19, 2024

Vierkantor Feb 19, 2024

Vierkantor Feb 19, 2024

Vierkantor Feb 19, 2024

Vierkantor Feb 19, 2024

Vierkantor Feb 19, 2024

Vierkantor Feb 19, 2024

darabos commented Feb 19, 2024

Vierkantor left a comment

mathlib-bors bot commented Feb 20, 2024

	rw [decompose_of_mem _ hx, DirectSum.of_eq_same]
	rw [decompose_of_mem _ hx, DirectSum.of_eq_same, Subtype.coe_mk]

	← eq_intCast (algebraMap ℤ K) _, Basis.restrictScalars_repr_apply]
	← eq_intCast (algebraMap ℤ K) _, Basis.restrictScalars_repr_apply, coe_mk]

	rw [decomposeAux_single, DirectSum.coeAlgHom_of])
	rw [decomposeAux_single, DirectSum.coeAlgHom_of, Subtype.coe_mk])

	IsLocalization.mk'_eq_of_eq (by rw [mul_comm, Subtype.coe_mk, ← h, mul_comm])
	IsLocalization.mk'_eq_of_eq (by rw [mul_comm, Subtype.coe_mk, ← h, mul_comm, Subtype.coe_mk])

	rw [Fin.ext_iff, Fin.coe_castLE, Composition.ones_embedding]
	rw [Fin.ext_iff, Fin.coe_castLE, Composition.ones_embedding, Fin.val_mk]

	_ = Pi.single (f := fun _ => R) n 1 i := by rw [Fin.val_mk]
	_ = Pi.single (f := fun _ => R) n 1 i := by rw [Fin.val_mk, Fin.val_mk]

	dsimp; rw [Multiset.map_replicate, Multiset.prod_replicate])
	dsimp; rw [Multiset.map_replicate, Multiset.prod_replicate, Subtype.coe_mk])

	rw [out]; dsimp only; rw [dif_pos i.is_lt]
	rw [out]; dsimp only; rw [dif_pos i.is_lt, Fin.eta]

	have ihi_eq : (⟨i, hi⟩ : Fin (N q)) = (E q) ⟨y, ys⟩ := by rw [Fin.ext_iff]
	have ihi_eq : (⟨i, hi⟩ : Fin (N q)) = (E q) ⟨y, ys⟩ := by rw [Fin.ext_iff, Fin.val_mk]

[Merged by Bors] - chore: Remove unnecessary "rw"s #10704

[Merged by Bors] - chore: Remove unnecessary "rw"s #10704

Conversation

darabos commented Feb 18, 2024

Vierkantor left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

darabos commented Feb 19, 2024

Vierkantor left a comment

Choose a reason for hiding this comment

mathlib-bors bot commented Feb 20, 2024