awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
m₁ m₂ : M
s : ↥S
rw : mk' f (m₁ + m₂) s = mk' f (s • m₁ + s • m₂) (s * s)
⊢ mk' f (m₁ + m₂) s = mk' f m₁ s + mk' f m₂ s
have rw₁ : mk' f (m₁ + m₂) s = mk' f (s • (m₁ + m₂)) (s * s)
Tactic: rw [mk'_add_mk', ← smul_add, mk'_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
m₁ m₂ : M
s : ↥S
rw : mk' f (m₁ + m₂) s = mk' f (s • m₁ + s • m₂) (s * s)
rw₁ : mk' f (m₁ + m₂) s = mk' f (s • (m₁ + m₂)) (s * s)
⊢ mk' f (m₁ + m₂) s = mk' f m₁ s + mk' f m₂ s
have rw₂ : mk' f (m₁ + m₂) s = mk' f (m₁ + m₂) s
Tactic: rw [mk'_add_mk', ← smul_add, mk'_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
m₁ m₂ : M
s₁ s₂ : ↥S
⊢ mk' f m₁ s₁ = mk' f m₂ s₂ ↔ ∃ (s : ↥S), s • s₁ • m₂ = s • s₂ • m₁
have delta : Eq.{u_3 + 1} (α := M') ((fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk m₁ s₁) : M')
    ((fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk m₂ s₂) : M') ↔
  ∃ (s : ↥S), s • s₁ • m₂ = s • s₂ • m₁
Tactic: delta mk'
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
m₁ m₂ : M
s₁ s₂ : ↥S
⊢ Eq.{u_3 + 1} (α := M') ((fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk m₁ s₁) : M')
      ((fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk m₂ s₂) : M') ↔
    ∃ (s : ↥S), s • s₁ • m₂ = s • s₂ • m₁
have rw : (∃ (u : ↥S), u • s₂ • m₁ = u • s₁ • m₂) ↔ ∃ (s : ↥S), s • s₁ • m₂ = s • s₂ • m₁
Tactic: rw [(fromLocalizedModule.inj S f).eq_iff, LocalizedModule.mk_eq]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_6
M' : Type u_7
inst_1 : AddCommGroup M
inst_2 : SubtractionCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
m : M
s : ↥S
⊢ mk' f (-m) s = -mk' f m s
have delta : Eq.{u_7 + 1} (α := M') ((fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk (-m) s) : M')
  (-(fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk m s) : M')
Tactic: delta mk'
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_6
M' : Type u_7
inst_1 : AddCommGroup M
inst_2 : SubtractionCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
m : M
s : ↥S
⊢ Eq.{u_7 + 1} (α := M') ((fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk (-m) s) : M')
    (-(fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk m s) : M')
have rw : Eq.{u_7 + 1} (α := M') ((fromLocalizedModule S f : (a : LocalizedModule S M) → M') (-LocalizedModule.mk m s) : M')
  (-(fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk m s) : M')
Tactic: rw [LocalizedModule.mk_neg, map_neg]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_6
M' : Type u_7
inst_1 : AddCommGroup M
inst_2 : SubtractionCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
m : M
s : ↥S
rw :
  Eq.{u_7 + 1} (α := M') ((fromLocalizedModule S f : (a : LocalizedModule S M) → M') (-LocalizedModule.mk m s) : M')
    (-(fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk m s) : M')
⊢ Eq.{u_7 + 1} (α := M') ((fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk (-m) s) : M')
    (-(fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk m s) : M')
have rw₁ : Eq.{u_7 + 1} (α := M') (-(fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk m s) : M')
  (-(fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk m s) : M')
Tactic: rw [LocalizedModule.mk_neg, map_neg]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_6
M' : Type u_7
inst_1 : AddCommGroup M
inst_2 : SubtractionCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
m₁ m₂ : M
s : ↥S
⊢ mk' f (m₁ - m₂) s = mk' f m₁ s - mk' f m₂ s
have rw : mk' f (m₁ + -m₂) s = mk' f m₁ s - mk' f m₂ s
Tactic: rw [sub_eq_add_neg, sub_eq_add_neg, mk'_add, mk'_neg]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_6
M' : Type u_7
inst_1 : AddCommGroup M
inst_2 : SubtractionCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
m₁ m₂ : M
s : ↥S
rw : mk' f (m₁ + -m₂) s = mk' f m₁ s - mk' f m₂ s
⊢ mk' f (m₁ - m₂) s = mk' f m₁ s - mk' f m₂ s
have rw₁ : mk' f (m₁ + -m₂) s = mk' f m₁ s + -mk' f m₂ s
Tactic: rw [sub_eq_add_neg, sub_eq_add_neg, mk'_add, mk'_neg]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_6
M' : Type u_7
inst_1 : AddCommGroup M
inst_2 : SubtractionCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
m₁ m₂ : M
s : ↥S
rw : mk' f (m₁ + -m₂) s = mk' f m₁ s - mk' f m₂ s
rw₁ : mk' f (m₁ + -m₂) s = mk' f m₁ s + -mk' f m₂ s
⊢ mk' f (m₁ - m₂) s = mk' f m₁ s - mk' f m₂ s
have rw₂ : mk' f m₁ s + mk' f (-m₂) s = mk' f m₁ s + -mk' f m₂ s
Tactic: rw [sub_eq_add_neg, sub_eq_add_neg, mk'_add, mk'_neg]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_6
M' : Type u_7
inst_1 : AddCommGroup M
inst_2 : SubtractionCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
m₁ m₂ : M
s : ↥S
rw : mk' f (m₁ + -m₂) s = mk' f m₁ s - mk' f m₂ s
rw₁ : mk' f (m₁ + -m₂) s = mk' f m₁ s + -mk' f m₂ s
rw₂ : mk' f m₁ s + mk' f (-m₂) s = mk' f m₁ s + -mk' f m₂ s
⊢ mk' f (m₁ - m₂) s = mk' f m₁ s - mk' f m₂ s
have rw₃ : mk' f m₁ s + -mk' f m₂ s = mk' f m₁ s + -mk' f m₂ s
Tactic: rw [sub_eq_add_neg, sub_eq_add_neg, mk'_add, mk'_neg]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_6
M' : Type u_7
inst_1 : AddCommGroup M
inst_2 : SubtractionCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
m₁ m₂ : M
s₁ s₂ : ↥S
⊢ mk' f m₁ s₁ - mk' f m₂ s₂ = mk' f (s₂ • m₁ - s₁ • m₂) (s₁ * s₂)
have rw : mk' f m₁ s₁ + -mk' f m₂ s₂ = mk' f (s₂ • m₁ - s₁ • m₂) (s₁ * s₂)
Tactic: rw [sub_eq_add_neg, ← mk'_neg, mk'_add_mk', smul_neg, ← sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_6
M' : Type u_7
inst_1 : AddCommGroup M
inst_2 : SubtractionCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
m₁ m₂ : M
s₁ s₂ : ↥S
rw : mk' f m₁ s₁ + -mk' f m₂ s₂ = mk' f (s₂ • m₁ - s₁ • m₂) (s₁ * s₂)
⊢ mk' f m₁ s₁ - mk' f m₂ s₂ = mk' f (s₂ • m₁ - s₁ • m₂) (s₁ * s₂)
have rw₁ : mk' f m₁ s₁ + mk' f (-m₂) s₂ = mk' f (s₂ • m₁ - s₁ • m₂) (s₁ * s₂)
Tactic: rw [sub_eq_add_neg, ← mk'_neg, mk'_add_mk', smul_neg, ← sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_6
M' : Type u_7
inst_1 : AddCommGroup M
inst_2 : SubtractionCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
m₁ m₂ : M
s₁ s₂ : ↥S
rw : mk' f m₁ s₁ + -mk' f m₂ s₂ = mk' f (s₂ • m₁ - s₁ • m₂) (s₁ * s₂)
rw₁ : mk' f m₁ s₁ + mk' f (-m₂) s₂ = mk' f (s₂ • m₁ - s₁ • m₂) (s₁ * s₂)
⊢ mk' f m₁ s₁ - mk' f m₂ s₂ = mk' f (s₂ • m₁ - s₁ • m₂) (s₁ * s₂)
have rw₂ : mk' f (s₂ • m₁ + s₁ • -m₂) (s₁ * s₂) = mk' f (s₂ • m₁ - s₁ • m₂) (s₁ * s₂)
Tactic: rw [sub_eq_add_neg, ← mk'_neg, mk'_add_mk', smul_neg, ← sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_6
M' : Type u_7
inst_1 : AddCommGroup M
inst_2 : SubtractionCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
m₁ m₂ : M
s₁ s₂ : ↥S
rw : mk' f m₁ s₁ + -mk' f m₂ s₂ = mk' f (s₂ • m₁ - s₁ • m₂) (s₁ * s₂)
rw₁ : mk' f m₁ s₁ + mk' f (-m₂) s₂ = mk' f (s₂ • m₁ - s₁ • m₂) (s₁ * s₂)
rw₂ : mk' f (s₂ • m₁ + s₁ • -m₂) (s₁ * s₂) = mk' f (s₂ • m₁ - s₁ • m₂) (s₁ * s₂)
⊢ mk' f m₁ s₁ - mk' f m₂ s₂ = mk' f (s₂ • m₁ - s₁ • m₂) (s₁ * s₂)
have rw₃ : mk' f (s₂ • m₁ + -(s₁ • m₂)) (s₁ * s₂) = mk' f (s₂ • m₁ - s₁ • m₂) (s₁ * s₂)
Tactic: rw [sub_eq_add_neg, ← mk'_neg, mk'_add_mk', smul_neg, ← sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_6
M' : Type u_7
inst_1 : AddCommGroup M
inst_2 : SubtractionCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
m₁ m₂ : M
s₁ s₂ : ↥S
rw : mk' f m₁ s₁ + -mk' f m₂ s₂ = mk' f (s₂ • m₁ - s₁ • m₂) (s₁ * s₂)
rw₁ : mk' f m₁ s₁ + mk' f (-m₂) s₂ = mk' f (s₂ • m₁ - s₁ • m₂) (s₁ * s₂)
rw₂ : mk' f (s₂ • m₁ + s₁ • -m₂) (s₁ * s₂) = mk' f (s₂ • m₁ - s₁ • m₂) (s₁ * s₂)
rw₃ : mk' f (s₂ • m₁ + -(s₁ • m₂)) (s₁ * s₂) = mk' f (s₂ • m₁ - s₁ • m₂) (s₁ * s₂)
⊢ mk' f m₁ s₁ - mk' f m₂ s₂ = mk' f (s₂ • m₁ - s₁ • m₂) (s₁ * s₂)
have rw₄ : mk' f (s₂ • m₁ - s₁ • m₂) (s₁ * s₂) = mk' f (s₂ • m₁ - s₁ • m₂) (s₁ * s₂)
Tactic: rw [sub_eq_add_neg, ← mk'_neg, mk'_add_mk', smul_neg, ← sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_6
M' : Type u_7
inst_1 : NonUnitalNonAssocSemiring M
inst_2 : Semiring M'
inst_3 : Module R M
inst_4 : Algebra R M'
f : M →ₗ[R] M'
hf :
  ∀ (m₁ m₂ : M),
    (f : (a : M) → M') (m₁ * m₂) =
      HMul.hMul (α := M') (β := M') ((f : (a : M) → M') m₁ : M') ((f : (a : M) → M') m₂ : M')
inst_5 : IsLocalizedModule S f
m₁ m₂ : M
s₁ s₂ : ↥S
⊢ mk' f m₁ s₁ * mk' f m₂ s₂ = mk' f (m₁ * m₂) (s₁ * s₂)
have symm : mk' f (m₁ * m₂) (s₁ * s₂) = mk' f m₁ s₁ * mk' f m₂ s₂
Tactic: symm
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_6
M' : Type u_7
inst_1 : NonUnitalNonAssocSemiring M
inst_2 : Semiring M'
inst_3 : Module R M
inst_4 : Algebra R M'
f : M →ₗ[R] M'
hf :
  ∀ (m₁ m₂ : M),
    (f : (a : M) → M') (m₁ * m₂) =
      HMul.hMul (α := M') (β := M') ((f : (a : M) → M') m₁ : M') ((f : (a : M) → M') m₂ : M')
inst_5 : IsLocalizedModule S f
m₁ m₂ : M
s₁ s₂ : ↥S
⊢ mk' f (m₁ * m₂) (s₁ * s₂) = mk' f m₁ s₁ * mk' f m₂ s₂
have apply : (f : (a : M) → M') (m₁ * m₂, s₁ * s₂).1 = (↑(m₁ * m₂, s₁ * s₂).2 : R) • (mk' f m₁ s₁ * mk' f m₂ s₂)
Tactic: apply (Module.End.algebraMap_isUnit_inv_apply_eq_iff _ _ _ _).mpr
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_6
M' : Type u_7
inst_1 : NonUnitalNonAssocSemiring M
inst_2 : Semiring M'
inst_3 : Module R M
inst_4 : Algebra R M'
f : M →ₗ[R] M'
hf :
  ∀ (m₁ m₂ : M),
    (f : (a : M) → M') (m₁ * m₂) =
      HMul.hMul (α := M') (β := M') ((f : (a : M) → M') m₁ : M') ((f : (a : M) → M') m₂ : M')
inst_5 : IsLocalizedModule S f
m₁ m₂ : M
s₁ s₂ : ↥S
⊢ (f : (a : M) → M') (m₁ * m₂, s₁ * s₂).1 = (↑(m₁ * m₂, s₁ * s₂).2 : R) • (mk' f m₁ s₁ * mk' f m₂ s₂)
have simp_rw : (f : (a : M) → M') (m₁ • m₂) = ((↑s₁ : R) • (↑s₂ : R)) • mk' f m₁ s₁ • mk' f m₂ s₂
Tactic: simp_rw [Submonoid.coe_mul, ← smul_eq_mul]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_6
M' : Type u_7
inst_1 : NonUnitalNonAssocSemiring M
inst_2 : Semiring M'
inst_3 : Module R M
inst_4 : Algebra R M'
f : M →ₗ[R] M'
hf :
  ∀ (m₁ m₂ : M),
    (f : (a : M) → M') (m₁ * m₂) =
      HMul.hMul (α := M') (β := M') ((f : (a : M) → M') m₁ : M') ((f : (a : M) → M') m₂ : M')
inst_5 : IsLocalizedModule S f
m₁ m₂ : M
s₁ s₂ : ↥S
⊢ (f : (a : M) → M') (m₁ • m₂) = ((↑s₁ : R) • (↑s₂ : R)) • mk' f m₁ s₁ • mk' f m₂ s₂
have rw : (f : (a : M) → M') (m₁ • m₂) = mk' f ((↑s₁ : R) • m₁) s₁ • mk' f ((↑s₂ : R) • m₂) s₂
Tactic: rw [smul_smul_smul_comm, ← mk'_smul, ← mk'_smul]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_6
M' : Type u_7
inst_1 : NonUnitalNonAssocSemiring M
inst_2 : Semiring M'
inst_3 : Module R M
inst_4 : Algebra R M'
f : M →ₗ[R] M'
hf :
  ∀ (m₁ m₂ : M),
    (f : (a : M) → M') (m₁ * m₂) =
      HMul.hMul (α := M') (β := M') ((f : (a : M) → M') m₁ : M') ((f : (a : M) → M') m₂ : M')
inst_5 : IsLocalizedModule S f
m₁ m₂ : M
s₁ s₂ : ↥S
⊢ (f : (a : M) → M') (m₁ • m₂) = mk' f ((↑s₁ : R) • m₁) s₁ • mk' f ((↑s₂ : R) • m₂) s₂
have simp_rw : (f : (a : M) → M') (m₁ • m₂) = mk' f (s₁ • m₁) s₁ • mk' f (s₂ • m₂) s₂
Tactic: simp_rw [← Submonoid.smul_def, mk'_cancel, smul_eq_mul, hf]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_6
M' : Type u_7
inst_1 : NonUnitalNonAssocSemiring M
inst_2 : Semiring M'
inst_3 : Module R M
inst_4 : Algebra R M'
f : M →ₗ[R] M'
hf :
  ∀ (m₁ m₂ : M),
    (f : (a : M) → M') (m₁ * m₂) =
      HMul.hMul (α := M') (β := M') ((f : (a : M) → M') m₁ : M') ((f : (a : M) → M') m₂ : M')
inst_5 : IsLocalizedModule S f
m₁ m₂ : M
s₁ s₂ : ↥S
simp_rw : (f : (a : M) → M') (m₁ • m₂) = mk' f (s₁ • m₁) s₁ • mk' f (s₂ • m₂) s₂
⊢ (f : (a : M) → M') (m₁ • m₂) = mk' f ((↑s₁ : R) • m₁) s₁ • mk' f ((↑s₂ : R) • m₂) s₂
have simp_rw₁ : (f : (a : M) → M') (m₁ • m₂) = HSMul.hSMul (α := M') (β := M') ((f : (a : M) → M') m₁ : M') ((f : (a : M) → M') m₂ : M')
Tactic: simp_rw [← Submonoid.smul_def, mk'_cancel, smul_eq_mul, hf]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_6
M' : Type u_7
inst_1 : NonUnitalNonAssocSemiring M
inst_2 : Semiring M'
inst_3 : Module R M
inst_4 : Algebra R M'
f : M →ₗ[R] M'
hf :
  ∀ (m₁ m₂ : M),
    (f : (a : M) → M') (m₁ * m₂) =
      HMul.hMul (α := M') (β := M') ((f : (a : M) → M') m₁ : M') ((f : (a : M) → M') m₂ : M')
inst_5 : IsLocalizedModule S f
m₁ m₂ : M
s₁ s₂ : ↥S
simp_rw : (f : (a : M) → M') (m₁ • m₂) = mk' f (s₁ • m₁) s₁ • mk' f (s₂ • m₂) s₂
simp_rw₁ :
  (f : (a : M) → M') (m₁ • m₂) =
    HSMul.hSMul (α := M') (β := M') ((f : (a : M) → M') m₁ : M') ((f : (a : M) → M') m₂ : M')
⊢ (f : (a : M) → M') (m₁ • m₂) = mk' f ((↑s₁ : R) • m₁) s₁ • mk' f ((↑s₂ : R) • m₂) s₂
have simp_rw₂ : (f : (a : M) → M') (m₁ * m₂) = HMul.hMul (α := M') (β := M') ((f : (a : M) → M') m₁ : M') ((f : (a : M) → M') m₂ : M')
Tactic: simp_rw [← Submonoid.smul_def, mk'_cancel, smul_eq_mul, hf]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
m : M
s : ↥S
m' : M'
⊢ mk' f m s = m' ↔ (f : (a : M) → M') m = s • m'
have rw : s • mk' f m s = s • m' ↔ (f : (a : M) → M') m = s • m'
Tactic: rw [← smul_inj f s, Submonoid.smul_def, ← mk'_smul, ← Submonoid.smul_def, mk'_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
m : M
s : ↥S
m' : M'
rw : s • mk' f m s = s • m' ↔ (f : (a : M) → M') m = s • m'
⊢ mk' f m s = m' ↔ (f : (a : M) → M') m = s • m'
have rw₁ : (↑s : R) • mk' f m s = s • m' ↔ (f : (a : M) → M') m = s • m'
Tactic: rw [← smul_inj f s, Submonoid.smul_def, ← mk'_smul, ← Submonoid.smul_def, mk'_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
m : M
s : ↥S
m' : M'
rw : s • mk' f m s = s • m' ↔ (f : (a : M) → M') m = s • m'
rw₁ : (↑s : R) • mk' f m s = s • m' ↔ (f : (a : M) → M') m = s • m'
⊢ mk' f m s = m' ↔ (f : (a : M) → M') m = s • m'
have rw₂ : mk' f ((↑s : R) • m) s = s • m' ↔ (f : (a : M) → M') m = s • m'
Tactic: rw [← smul_inj f s, Submonoid.smul_def, ← mk'_smul, ← Submonoid.smul_def, mk'_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
m : M
s : ↥S
m' : M'
rw : s • mk' f m s = s • m' ↔ (f : (a : M) → M') m = s • m'
rw₁ : (↑s : R) • mk' f m s = s • m' ↔ (f : (a : M) → M') m = s • m'
rw₂ : mk' f ((↑s : R) • m) s = s • m' ↔ (f : (a : M) → M') m = s • m'
⊢ mk' f m s = m' ↔ (f : (a : M) → M') m = s • m'
have rw₃ : mk' f (s • m) s = s • m' ↔ (f : (a : M) → M') m = s • m'
Tactic: rw [← smul_inj f s, Submonoid.smul_def, ← mk'_smul, ← Submonoid.smul_def, mk'_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
m : M
s : ↥S
m' : M'
rw : s • mk' f m s = s • m' ↔ (f : (a : M) → M') m = s • m'
rw₁ : (↑s : R) • mk' f m s = s • m' ↔ (f : (a : M) → M') m = s • m'
rw₂ : mk' f ((↑s : R) • m) s = s • m' ↔ (f : (a : M) → M') m = s • m'
rw₃ : mk' f (s • m) s = s • m' ↔ (f : (a : M) → M') m = s • m'
⊢ mk' f m s = m' ↔ (f : (a : M) → M') m = s • m'
have rw₄ : (f : (a : M) → M') m = s • m' ↔ (f : (a : M) → M') m = s • m'
Tactic: rw [← smul_inj f s, Submonoid.smul_def, ← mk'_smul, ← Submonoid.smul_def, mk'_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
m : M
s : ↥S
⊢ mk' f m s = 0 ↔ Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') m : M') (0 : M')
have rw : (f : (a : M) → M') m = HSMul.hSMul (β := M') s 0 ↔ Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') m : M') (0 : M')
Tactic: rw [mk'_eq_iff, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
m : M
s : ↥S
rw : (f : (a : M) → M') m = HSMul.hSMul (β := M') s 0 ↔ Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') m : M') (0 : M')
⊢ mk' f m s = 0 ↔ Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') m : M') (0 : M')
have rw₁ : Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') m : M') (0 : M') ↔
  Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') m : M') (0 : M')
Tactic: rw [mk'_eq_iff, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
m : M
s : ↥S
⊢ mk' f m s = 0 ↔ ∃ (s' : ↥S), s' • m = 0
have simp_rw : mk' f m s = mk' (S := S) f 0 1 ↔ ∃ (s' : ↥S), s' • m = 0
Tactic: simp_rw [← mk'_zero f (1 : S), mk'_eq_mk'_iff, smul_zero, one_smul, eq_comm]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
m : M
s : ↥S
simp_rw : mk' f m s = mk' (S := S) f 0 1 ↔ ∃ (s' : ↥S), s' • m = 0
⊢ mk' f m s = 0 ↔ ∃ (s' : ↥S), s' • m = 0
have simp_rw₁ : (∃ (s_1 : ↥S), s_1 • HSMul.hSMul (β := M) s 0 = s_1 • HSMul.hSMul.{u_1, u_2, u_2} (α := ↥S) 1 m) ↔
  ∃ (s' : ↥S), s' • m = 0
Tactic: simp_rw [← mk'_zero f (1 : S), mk'_eq_mk'_iff, smul_zero, one_smul, eq_comm]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
m : M
s : ↥S
simp_rw : mk' f m s = mk' (S := S) f 0 1 ↔ ∃ (s' : ↥S), s' • m = 0
simp_rw₁ :
  (∃ (s_1 : ↥S), s_1 • HSMul.hSMul (β := M) s 0 = s_1 • HSMul.hSMul.{u_1, u_2, u_2} (α := ↥S) 1 m) ↔
    ∃ (s' : ↥S), s' • m = 0
⊢ mk' f m s = 0 ↔ ∃ (s' : ↥S), s' • m = 0
have simp_rw₂ : (∃ (s : ↥S), 0 = s • HSMul.hSMul.{u_1, u_2, u_2} (α := ↥S) 1 m) ↔ ∃ (s' : ↥S), s' • m = 0
Tactic: simp_rw [← mk'_zero f (1 : S), mk'_eq_mk'_iff, smul_zero, one_smul, eq_comm]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
m : M
s : ↥S
simp_rw : mk' f m s = mk' (S := S) f 0 1 ↔ ∃ (s' : ↥S), s' • m = 0
simp_rw₁ :
  (∃ (s_1 : ↥S), s_1 • HSMul.hSMul (β := M) s 0 = s_1 • HSMul.hSMul.{u_1, u_2, u_2} (α := ↥S) 1 m) ↔
    ∃ (s' : ↥S), s' • m = 0
simp_rw₂ : (∃ (s : ↥S), 0 = s • HSMul.hSMul.{u_1, u_2, u_2} (α := ↥S) 1 m) ↔ ∃ (s' : ↥S), s' • m = 0
⊢ mk' f m s = 0 ↔ ∃ (s' : ↥S), s' • m = 0
have simp_rw₃ : (∃ (s : ↥S), 0 = s • m) ↔ ∃ (s' : ↥S), s' • m = 0
Tactic: simp_rw [← mk'_zero f (1 : S), mk'_eq_mk'_iff, smul_zero, one_smul, eq_comm]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : ↥S
m : M
⊢ Eq (α := LocalizedModule S M) (LocalizedModule.mk m s) (mk' (LocalizedModule.mkLinearMap S M) m s)
have rw : Eq (α := LocalizedModule S M) (mk' (LocalizedModule.mkLinearMap S M) m s) (LocalizedModule.mk m s)
Tactic: rw [eq_comm, mk'_eq_iff, Submonoid.smul_def, LocalizedModule.smul'_mk, ← Submonoid.smul_def,
    LocalizedModule.mk_cancel, LocalizedModule.mkLinearMap_apply]