-- Mathlib/RingTheory/Regular/RegularSequence.lean
private lemma IsWeaklyRegular.swap {a b : R} (h1 : IsWeaklyRegular M [a, b])
    (h2 : torsionBy R M b = a • torsionBy R M b → torsionBy R M b = ⊥) :
    IsWeaklyRegular M [b, a]

Proof state:
case intro
R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a b : R
h2 : torsionBy R M b = a • torsionBy R M b → IsSMulRegular M b
ha : IsSMulRegular M a
hb : IsSMulRegular (QuotSMulTop a M) b
⊢ IsSMulRegular M b ∧ IsSMulRegular (QuotSMulTop b M) a

Tactic:
specialize h2 (le_antisymm ?_ (smul_le_self_of_tower a (torsionBy R M b)))

Result:
case intro
R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a b : R
h2 : torsionBy R M b = a • torsionBy R M b → IsSMulRegular M b
ha : IsSMulRegular M a
hb : IsSMulRegular (QuotSMulTop a M) b
⊢ torsionBy R M b ≤ a • torsionBy R M b

case intro
R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a b : R
ha : IsSMulRegular M a
hb : IsSMulRegular (QuotSMulTop a M) b
h2 : IsSMulRegular M b
⊢ IsSMulRegular M b ∧ IsSMulRegular (QuotSMulTop b M) a

Proof state:
case intro
R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a b : R
h2 : torsionBy R M b = a • torsionBy R M b → IsSMulRegular M b
ha : IsSMulRegular M a
hb : IsSMulRegular (QuotSMulTop a M) b
⊢ torsionBy R M b = a • ⊤ ⊓ torsionBy R M b

Tactic:
rw [← (isSMulRegular_on_quot_iff_lsmul_comap_eq _ _).mp hb]

Result:
case intro
R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a b : R
h2 : torsionBy R M b = a • torsionBy R M b → IsSMulRegular M b
ha : IsSMulRegular M a
hb : IsSMulRegular (QuotSMulTop a M) b
⊢ torsionBy R M b = comap ((lsmul R M) b) (a • ⊤) ⊓ torsionBy R M b

Proof state:
case intro
R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a b : R
h2 : torsionBy R M b = a • torsionBy R M b → IsSMulRegular M b
ha : IsSMulRegular M a
hb : IsSMulRegular (QuotSMulTop a M) b
⊢ torsionBy R M b ≤ a • torsionBy R M b

Tactic:
refine le_of_eq_of_le ?_ <| smul_top_inf_eq_smul_of_isSMulRegular_on_quot <|
  ha.of_injective _ <| ker_eq_bot.mp <| ker_liftQ_eq_bot' _ (lsmul R M b) rfl

Result:
case intro
R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a b : R
h2 : torsionBy R M b = a • torsionBy R M b → IsSMulRegular M b
ha : IsSMulRegular M a
hb : IsSMulRegular (QuotSMulTop a M) b
⊢ torsionBy R M b = a • ⊤ ⊓ torsionBy R M b

Proof state:
R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a b : R
h1 : IsSMulRegular M a ∧ IsSMulRegular (QuotSMulTop a M) b
h2 : torsionBy R M b = a • torsionBy R M b → torsionBy R M b = ⊥
⊢ IsSMulRegular M b ∧ IsSMulRegular (QuotSMulTop b M) a

Tactic:
obtain ⟨ha, hb⟩ := h1

Result:
case intro
R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a b : R
h2 : torsionBy R M b = a • torsionBy R M b → torsionBy R M b = ⊥
ha : IsSMulRegular M a
hb : IsSMulRegular (QuotSMulTop a M) b
⊢ IsSMulRegular M b ∧ IsSMulRegular (QuotSMulTop b M) a

Proof state:
case intro
R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a b : R
h2 : torsionBy R M b = a • torsionBy R M b → IsSMulRegular M b
ha : IsSMulRegular M a
hb : IsSMulRegular (QuotSMulTop a M) b
⊢ torsionBy R M b = comap ((lsmul R M) b) (a • ⊤) ⊓ torsionBy R M b

Tactic:
exact (inf_eq_right.mpr (ker_le_comap _)).symm

Result:
no goals

Proof state:
case intro
R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a b : R
h2 : torsionBy R M b = a • torsionBy R M b → torsionBy R M b = ⊥
ha : IsSMulRegular M a
hb : IsSMulRegular (QuotSMulTop a M) b
⊢ IsSMulRegular M b ∧ IsSMulRegular (QuotSMulTop b M) a

Tactic:
rw [← isSMulRegular_iff_torsionBy_eq_bot] at h2

Result:
case intro
R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a b : R
h2 : torsionBy R M b = a • torsionBy R M b → IsSMulRegular M b
ha : IsSMulRegular M a
hb : IsSMulRegular (QuotSMulTop a M) b
⊢ IsSMulRegular M b ∧ IsSMulRegular (QuotSMulTop b M) a

Proof state:
case intro
R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a b : R
ha : IsSMulRegular M a
hb : IsSMulRegular (QuotSMulTop a M) b
h2 : IsSMulRegular M b
⊢ IsSMulRegular M b ∧ IsSMulRegular (QuotSMulTop b M) a

Tactic:
rwa [ha.isSMulRegular_on_quot_iff_smul_top_inf_eq_smul, inf_comm, smul_comm,
  ← h2.isSMulRegular_on_quot_iff_smul_top_inf_eq_smul, and_iff_left hb]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a b : R
h1 : IsWeaklyRegular M [a, b]
h2 : torsionBy R M b = a • torsionBy R M b → torsionBy R M b = ⊥
⊢ IsWeaklyRegular M [b, a]

Tactic:
rw [isWeaklyRegular_cons_iff, isWeaklyRegular_singleton_iff] at h1 ⊢

Result:
R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a b : R
h1 : IsSMulRegular M a ∧ IsSMulRegular (QuotSMulTop a M) b
h2 : torsionBy R M b = a • torsionBy R M b → torsionBy R M b = ⊥
⊢ IsSMulRegular M b ∧ IsSMulRegular (QuotSMulTop b M) a