A first proof

Stream: new members

[Calvin Lee]

Hello!
I have a bit of (programming) experience in Lean4 and theorem proving experience in Agda/Coq but I'm new to Lean3.
I'm currently trying to show that if $M$ is an $R$-module, then $M/IM$ is an $R/I$-module.

Here is my first attempt at a lean3 proof to show that the scalar multiplication is well defined, I'm hoping some of you could give me some pointers on things I could do better going forward, since working with setoids here was a bit rough (and appears to be just as bad when defining the module laws).

variables (R M : Type _) [comm_ring R] [add_comm_group M] [module R M] (I : ideal R)
instance quotient_over_ideal_smul_residue : has_smul (R ⧸ I) (M ⧸ (I • ⊤ : submodule R M)) :=
⟨ λ r m, quotient.lift_on₂' r m (λ (r : R) (m : M), submodule.quotient.mk $ r • m)
  begin
    intros r₁ m₁ r₂ m₂ h₁ h₂,
    unfold,
    rw submodule.quotient.eq,
    have : (r₁ = r₂ + (r₁ - r₂)) := by ring,
    rw this, clear this,
    have : (r₂ + (r₁ - r₂))•m₁ = r₂•m₁ + (r₁ - r₂)•m₁,
    { rw add_smul },
    rw this, clear this,
    rw add_sub_right_comm,
    apply submodule.add_mem (I • (⊤ : submodule R M)),
    {
      have : m₁ = m₂ + (m₁ - m₂) := eq_add_of_sub_eq' rfl,
      rw [this, smul_add, add_sub_right_comm, add_comm_group.sub_eq_add_neg, add_neg_self, zero_add ],
      clear this,
      apply (submodule.smul_mem' _ _ _),
      rw submodule.quotient_rel_r_def at h₂,
      assumption
    },
    {
      apply submodule.smul_mem_smul,
      {
        rw ← quotient.eq' at h₁,
        rw ← ideal.quotient.eq,
        assumption,
      },
      {
        exact submodule.mem_top,
      },
    },
  end⟩

[Adam Topaz]

This is a great start! The data all seems good to me so far! I golfed your proof just a bit... I hope this illustrates some useful Lean3/mathlib tricks.

import ring_theory.ideal.quotient
import algebra.category.Module.abelian

variables (R M : Type _) [comm_ring R] [add_comm_group M] [module R M] (I : ideal R)

instance quotient_over_ideal_smul_residue : has_smul (R ⧸ I) (M ⧸ (I • ⊤ : submodule R M)) :=
⟨ λ r m, quotient.lift_on₂' r m (λ r' m', submodule.quotient.mk (r' • m'))
  begin
    intros r₁ m₁ r₂ m₂ h₁ h₂,
    rw ← quotient.eq' at h₁ h₂, dsimp at h₁ h₂,
    erw quotient_add_group.mk'_eq_mk' at h₁ h₂,
    obtain ⟨m,hm,rfl⟩ := h₁,
    obtain ⟨n,hn,rfl⟩ := h₂,
    dsimp, simp only [smul_add, add_smul, add_assoc],
    symmetry, convert add_zero _,
    simp_rw [← submodule.quotient.mk_smul, ← submodule.quotient.mk_add],
    rw submodule.quotient.mk_eq_zero,
    refine submodule.add_mem _ _ (submodule.add_mem _ _ _),
    { refine submodule.smul_mem _ _ hn },
    all_goals { refine submodule.smul_mem_smul hm trivial, },
  end ⟩

[Calvin Lee]

Thank you!
I have a few questions (and thanks for obtain I really needed that but couldn't find it)
Doesn't this use nonterminal simps in several places? I've heard that could be an issue

[Anne Baanen]

simp only is OK, since it explicitly lists what is going to happen. dsimp is usually also fine because the result of simplifying is guaranteed to be definitionally equal, although I prefer dsimp only.

[Andrew Yang]

You can also see how it is done in mathlib here: docs#module.has_quotient.quotient.module.

[Junyan Xu]

It's annoying that squeeze_dsimp usually doesn't return a valid result ...

[Kevin Buzzard]

Yes, you mean it suggests dsimp only but dsimp only doesn't work? I've seen this many times. Does the output of show_term {dsimp} make any sense?

[Junyan Xu]

Yes, you mean it suggests dsimp only but dsimp only doesn't work?

Yes exactly. I never tried show_term; I thought it must be used with a block of tactics that solve the goal!

[Kevin Buzzard]

show_term {dsimp} should work fine in a tactic proof. It might give you an awful mess though, I never tried. This only occurred to me recently, and I've not had squeeze_dsimp fail on me since I had the idea.

[Calvin Lee]

Andrew Yang said:

You can also see how it is done in mathlib here: docs#module.has_quotient.quotient.module.

OMG i tried looking for this for so long and couldn't find it

[Junyan Xu]

show_term {dsimp} just returns refine id _ ... at least in this case. If I use set_option pp.implicit true it returns something like

refine @id
  ((λ (y : Y × ({j // j ≠ i} → Y)) (j : N),
        @dite Y (j = i) (_inst_3 j i) (λ (h : j = i), y.fst)
          (λ (h : ¬j = i), y.snd (@subtype.mk N (λ (j : N), j ≠ i) j h)))
       ((λ (f : N → Y), (f i, λ (j : {j // j ≠ i}), f ↑j)) y)
       j =
     y j)
  _

but using change would certainly be shorter than copying this.

[Kevin Buzzard]

In the case you linked to, dsimp only changes the goal to dite not ite but for me changing dsimp to dsimp only doesn't break the proof (and similarly for line 79) (I pushed the changes)

[Junyan Xu]

Thanks! It doesn't work for the remaining two dsimp in the file though.