awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
T : Type u_1
inst_1 : CommSemiring T
inst_2 : Algebra R T
inst_3 : IsLocalization S T
A : Type u_2
inst_4 : Semiring A
inst_5 : Algebra R A
a : R
s : ↥S
rw : Eq (α := LocalizedModule S A) (mk (HSMul.hSMul (β := A) a 1) (s * 1)) (mk ((algebraMap R A : (a : R) → A) a) s)
⊢ HSMul.hSMul (β := LocalizedModule S A) (IsLocalization.mk' T a s) (mk 1 1) = mk ((algebraMap R A : (a : R) → A) a) s
have rw₁ : Eq (α := LocalizedModule S A) (mk (HSMul.hSMul (β := A) a 1) (s * 1)) (mk (HSMul.hSMul (β := A) a 1) s)
Tactic: rw [mk'_smul_mk, Algebra.algebraMap_eq_smul_one, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
T : Type u_1
inst_1 : CommSemiring T
inst_2 : Algebra R T
inst_3 : IsLocalization S T
A : Type u_2
inst_4 : Semiring A
inst_5 : Algebra R A
a : R
s : ↥S
rw : Eq (α := LocalizedModule S A) (mk (HSMul.hSMul (β := A) a 1) (s * 1)) (mk ((algebraMap R A : (a : R) → A) a) s)
rw₁ : Eq (α := LocalizedModule S A) (mk (HSMul.hSMul (β := A) a 1) (s * 1)) (mk (HSMul.hSMul (β := A) a 1) s)
⊢ HSMul.hSMul (β := LocalizedModule S A) (IsLocalization.mk' T a s) (mk 1 1) = mk ((algebraMap R A : (a : R) → A) a) s
have rw₂ : Eq (α := LocalizedModule S A) (mk (HSMul.hSMul (β := A) a 1) s) (mk (HSMul.hSMul (β := A) a 1) s)
Tactic: rw [mk'_smul_mk, Algebra.algebraMap_eq_smul_one, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
T : Type u_1
inst_1 : CommSemiring T
inst_2 : Algebra R T
inst_3 : IsLocalization S T
A : Type u_2
inst_4 : Semiring A
inst_5 : Algebra R A
a : R
s : ↥S
⊢ Eq (α := LocalizedModule S A)
    ((algebraMap T (LocalizedModule S A) : (a : T) → LocalizedModule S A) (IsLocalization.mk' T a s) :
      LocalizedModule S A)
    (mk ((algebraMap R A : (a : R) → A) a) s : LocalizedModule S A)
have rw : HSMul.hSMul (β := LocalizedModule S A) (IsLocalization.mk' T a s) 1 = mk ((algebraMap R A : (a : R) → A) a) s
Tactic: with_unfolding_all
  rw [Algebra.algebraMap_eq_smul_one]
  change _ • mk _ _ = _
  rw [mk'_smul_mk, Algebra.algebraMap_eq_smul_one, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
T : Type u_1
inst_1 : CommSemiring T
inst_2 : Algebra R T
inst_3 : IsLocalization S T
A : Type u_2
inst_4 : Semiring A
inst_5 : Algebra R A
a : R
s : ↥S
rw rw₁ rw₂ :
  HSMul.hSMul (β := LocalizedModule S A) (IsLocalization.mk' T a s) 1 = mk ((algebraMap R A : (a : R) → A) a) s
⊢ Eq (α := LocalizedModule S A)
    ((algebraMap T (LocalizedModule S A) : (a : T) → LocalizedModule S A) (IsLocalization.mk' T a s) :
      LocalizedModule S A)
    (mk ((algebraMap R A : (a : R) → A) a) s : LocalizedModule S A)
have rw₃ : HSMul.hSMul (β := LocalizedModule S A) (IsLocalization.mk' T a s) (mk 1 1) = mk ((algebraMap R A : (a : R) → A) a) s
Tactic: with_unfolding_all
  rw [Algebra.algebraMap_eq_smul_one]
  change _ • mk _ _ = _
  rw [mk'_smul_mk, Algebra.algebraMap_eq_smul_one, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
A : Type u_2
inst_1 : Semiring A
inst_2 : Algebra R A
a : R
s : ↥S
⊢ Eq (α := LocalizedModule S A)
    ((algebraMap (Localization (M := R) S) (LocalizedModule S A) : (a : Localization S) → LocalizedModule S A)
        (Localization.mk a s) :
      LocalizedModule S A)
    (mk ((algebraMap R A : (a : R) → A) a) s : LocalizedModule S A)
have rw : Eq (α := LocalizedModule S A)
  ((algebraMap (Localization (M := R) S) (LocalizedModule S A) : (a : Localization S) → LocalizedModule S A)
      (IsLocalization.mk' (Localization (M := R) S) a s) :
    LocalizedModule S A)
  (mk ((algebraMap R A : (a : R) → A) a) s : LocalizedModule S A)
Tactic: rw [Localization.mk_eq_mk']
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
T : Type u_1
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : IsLocalization S T
r : R
x : T
p : LocalizedModule S M
⊢ (r • x) • p = r • x • p
have h : ∀ (m : M) (s : ↥S),
  HSMul.hSMul (β := LocalizedModule S M) (r • x) (mk m s) = r • HSMul.hSMul (β := LocalizedModule S M) x (mk m s)
Tactic: induction p with | _ m s
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
T : Type u_1
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : IsLocalization S T
r : R
x : T
m : M
s : ↥S
⊢ HSMul.hSMul (β := LocalizedModule S M) (r • x) (mk m s) = r • HSMul.hSMul (β := LocalizedModule S M) x (mk m s)
have h : HSMul.hSMul (β := LocalizedModule S M) (r • IsLocalization.mk' T (IsLocalization.sec S x).1 (IsLocalization.sec S x).2)
    (mk m s) =
  r •
    HSMul.hSMul (β := LocalizedModule S M) (IsLocalization.mk' T (IsLocalization.sec S x).1 (IsLocalization.sec S x).2)
      (mk m s)
Tactic: rw [← IsLocalization.mk'_sec (M := S) T x, IsLocalization.smul_mk', mk'_smul_mk, mk'_smul_mk,
      smul'_mk, mul_smul]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
T : Type u_1
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : IsLocalization S T
r : R
x : T
m : M
s : ↥S
h :
  HSMul.hSMul (β := LocalizedModule S M)
      (r • IsLocalization.mk' T (IsLocalization.sec S x).1 (IsLocalization.sec S x).2) (mk m s) =
    r •
      HSMul.hSMul (β := LocalizedModule S M)
        (IsLocalization.mk' T (IsLocalization.sec S x).1 (IsLocalization.sec S x).2) (mk m s)
⊢ HSMul.hSMul (β := LocalizedModule S M) (r • x) (mk m s) = r • HSMul.hSMul (β := LocalizedModule S M) x (mk m s)
have h₁ : HSMul.hSMul (β := LocalizedModule S M)
    (IsLocalization.mk' T (r * (IsLocalization.sec S x).1) (IsLocalization.sec S x).2) (mk m s) =
  r •
    HSMul.hSMul (β := LocalizedModule S M) (IsLocalization.mk' T (IsLocalization.sec S x).1 (IsLocalization.sec S x).2)
      (mk m s)
Tactic: rw [← IsLocalization.mk'_sec (M := S) T x, IsLocalization.smul_mk', mk'_smul_mk, mk'_smul_mk,
      smul'_mk, mul_smul]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
T : Type u_1
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : IsLocalization S T
r : R
x : T
m : M
s : ↥S
h :
  HSMul.hSMul (β := LocalizedModule S M)
      (r • IsLocalization.mk' T (IsLocalization.sec S x).1 (IsLocalization.sec S x).2) (mk m s) =
    r •
      HSMul.hSMul (β := LocalizedModule S M)
        (IsLocalization.mk' T (IsLocalization.sec S x).1 (IsLocalization.sec S x).2) (mk m s)
h₁ :
  HSMul.hSMul (β := LocalizedModule S M)
      (IsLocalization.mk' T (r * (IsLocalization.sec S x).1) (IsLocalization.sec S x).2) (mk m s) =
    r •
      HSMul.hSMul (β := LocalizedModule S M)
        (IsLocalization.mk' T (IsLocalization.sec S x).1 (IsLocalization.sec S x).2) (mk m s)
⊢ HSMul.hSMul (β := LocalizedModule S M) (r • x) (mk m s) = r • HSMul.hSMul (β := LocalizedModule S M) x (mk m s)
have h₂ : mk ((r * (IsLocalization.sec S x).1) • m) ((IsLocalization.sec S x).2 * s) =
  r •
    HSMul.hSMul (β := LocalizedModule S M) (IsLocalization.mk' T (IsLocalization.sec S x).1 (IsLocalization.sec S x).2)
      (mk m s)
Tactic: rw [← IsLocalization.mk'_sec (M := S) T x, IsLocalization.smul_mk', mk'_smul_mk, mk'_smul_mk,
      smul'_mk, mul_smul]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
T : Type u_1
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : IsLocalization S T
r : R
x : T
m : M
s : ↥S
h :
  HSMul.hSMul (β := LocalizedModule S M)
      (r • IsLocalization.mk' T (IsLocalization.sec S x).1 (IsLocalization.sec S x).2) (mk m s) =
    r •
      HSMul.hSMul (β := LocalizedModule S M)
        (IsLocalization.mk' T (IsLocalization.sec S x).1 (IsLocalization.sec S x).2) (mk m s)
h₁ :
  HSMul.hSMul (β := LocalizedModule S M)
      (IsLocalization.mk' T (r * (IsLocalization.sec S x).1) (IsLocalization.sec S x).2) (mk m s) =
    r •
      HSMul.hSMul (β := LocalizedModule S M)
        (IsLocalization.mk' T (IsLocalization.sec S x).1 (IsLocalization.sec S x).2) (mk m s)
h₂ :
  mk ((r * (IsLocalization.sec S x).1) • m) ((IsLocalization.sec S x).2 * s) =
    r •
      HSMul.hSMul (β := LocalizedModule S M)
        (IsLocalization.mk' T (IsLocalization.sec S x).1 (IsLocalization.sec S x).2) (mk m s)
⊢ HSMul.hSMul (β := LocalizedModule S M) (r • x) (mk m s) = r • HSMul.hSMul (β := LocalizedModule S M) x (mk m s)
have h₃ : mk ((r * (IsLocalization.sec S x).1) • m) ((IsLocalization.sec S x).2 * s) =
  HSMul.hSMul (β := LocalizedModule S M) r (mk ((IsLocalization.sec S x).1 • m) ((IsLocalization.sec S x).2 * s))
Tactic: rw [← IsLocalization.mk'_sec (M := S) T x, IsLocalization.smul_mk', mk'_smul_mk, mk'_smul_mk,
      smul'_mk, mul_smul]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
T : Type u_1
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : IsLocalization S T
r : R
x : T
m : M
s : ↥S
h :
  HSMul.hSMul (β := LocalizedModule S M)
      (r • IsLocalization.mk' T (IsLocalization.sec S x).1 (IsLocalization.sec S x).2) (mk m s) =
    r •
      HSMul.hSMul (β := LocalizedModule S M)
        (IsLocalization.mk' T (IsLocalization.sec S x).1 (IsLocalization.sec S x).2) (mk m s)
h₁ :
  HSMul.hSMul (β := LocalizedModule S M)
      (IsLocalization.mk' T (r * (IsLocalization.sec S x).1) (IsLocalization.sec S x).2) (mk m s) =
    r •
      HSMul.hSMul (β := LocalizedModule S M)
        (IsLocalization.mk' T (IsLocalization.sec S x).1 (IsLocalization.sec S x).2) (mk m s)
h₂ :
  mk ((r * (IsLocalization.sec S x).1) • m) ((IsLocalization.sec S x).2 * s) =
    r •
      HSMul.hSMul (β := LocalizedModule S M)
        (IsLocalization.mk' T (IsLocalization.sec S x).1 (IsLocalization.sec S x).2) (mk m s)
h₃ :
  mk ((r * (IsLocalization.sec S x).1) • m) ((IsLocalization.sec S x).2 * s) =
    HSMul.hSMul (β := LocalizedModule S M) r (mk ((IsLocalization.sec S x).1 • m) ((IsLocalization.sec S x).2 * s))
⊢ HSMul.hSMul (β := LocalizedModule S M) (r • x) (mk m s) = r • HSMul.hSMul (β := LocalizedModule S M) x (mk m s)
have h₄ : Eq (α := LocalizedModule S M) (mk ((r * (IsLocalization.sec S x).1) • m) ((IsLocalization.sec S x).2 * s))
  (mk (r • (IsLocalization.sec S x).1 • m) ((IsLocalization.sec S x).2 * s))
Tactic: rw [← IsLocalization.mk'_sec (M := S) T x, IsLocalization.smul_mk', mk'_smul_mk, mk'_smul_mk,
      smul'_mk, mul_smul]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
T : Type u_1
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : IsLocalization S T
r : R
x : T
m : M
s : ↥S
h :
  HSMul.hSMul (β := LocalizedModule S M)
      (r • IsLocalization.mk' T (IsLocalization.sec S x).1 (IsLocalization.sec S x).2) (mk m s) =
    r •
      HSMul.hSMul (β := LocalizedModule S M)
        (IsLocalization.mk' T (IsLocalization.sec S x).1 (IsLocalization.sec S x).2) (mk m s)
h₁ :
  HSMul.hSMul (β := LocalizedModule S M)
      (IsLocalization.mk' T (r * (IsLocalization.sec S x).1) (IsLocalization.sec S x).2) (mk m s) =
    r •
      HSMul.hSMul (β := LocalizedModule S M)
        (IsLocalization.mk' T (IsLocalization.sec S x).1 (IsLocalization.sec S x).2) (mk m s)
h₂ :
  mk ((r * (IsLocalization.sec S x).1) • m) ((IsLocalization.sec S x).2 * s) =
    r •
      HSMul.hSMul (β := LocalizedModule S M)
        (IsLocalization.mk' T (IsLocalization.sec S x).1 (IsLocalization.sec S x).2) (mk m s)
h₃ :
  mk ((r * (IsLocalization.sec S x).1) • m) ((IsLocalization.sec S x).2 * s) =
    HSMul.hSMul (β := LocalizedModule S M) r (mk ((IsLocalization.sec S x).1 • m) ((IsLocalization.sec S x).2 * s))
h₄ :
  Eq (α := LocalizedModule S M) (mk ((r * (IsLocalization.sec S x).1) • m) ((IsLocalization.sec S x).2 * s))
    (mk (r • (IsLocalization.sec S x).1 • m) ((IsLocalization.sec S x).2 * s))
⊢ HSMul.hSMul (β := LocalizedModule S M) (r • x) (mk m s) = r • HSMul.hSMul (β := LocalizedModule S M) x (mk m s)
have h₅ : Eq (α := LocalizedModule S M) (mk (r • (IsLocalization.sec S x).1 • m) ((IsLocalization.sec S x).2 * s))
  (mk (r • (IsLocalization.sec S x).1 • m) ((IsLocalization.sec S x).2 * s))
Tactic: rw [← IsLocalization.mk'_sec (M := S) T x, IsLocalization.smul_mk', mk'_smul_mk, mk'_smul_mk,
      smul'_mk, mul_smul]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
T : Type u_1
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : IsLocalization S T
A : Type u_2
inst_6 : Semiring A
inst_7 : Algebra R A
r : R
x : LocalizedModule S A
⊢ HMul.hMul (α := LocalizedModule S A)
      ((RingHom.comp numeratorRingHom (algebraMap R A) : (a : R) → LocalizedModule S A) r : LocalizedModule S A) x =
    HMul.hMul (β := LocalizedModule S A) x
      ((RingHom.comp numeratorRingHom (algebraMap R A) : (a : R) → LocalizedModule S A) r : LocalizedModule S A)
have h : ∀ (a : A) (s : ↥S),
  HMul.hMul (α := LocalizedModule S A) (β := LocalizedModule S A)
      ((RingHom.comp numeratorRingHom (algebraMap R A) : (a : R) → LocalizedModule S A) r : LocalizedModule S A)
      (mk a s) =
    HMul.hMul (α := LocalizedModule S A) (β := LocalizedModule S A) (mk a s)
      ((RingHom.comp numeratorRingHom (algebraMap R A) : (a : R) → LocalizedModule S A) r : LocalizedModule S A)
Tactic: induction x using induction_on with | _ a s => _
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
T : Type u_1
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : IsLocalization S T
A : Type u_2
inst_6 : Semiring A
inst_7 : Algebra R A
r : R
a : A
s : ↥S
⊢ HMul.hMul (α := LocalizedModule S A) (β := LocalizedModule S A)
      (mk ((algebraMap R A : (a : R) → A) r) 1 : LocalizedModule S A) (mk a s) =
    HMul.hMul (α := LocalizedModule S A) (β := LocalizedModule S A) (mk a s)
      (mk ((algebraMap R A : (a : R) → A) r) 1 : LocalizedModule S A)
have h : mk (HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) a) (1 * s) =
  HMul.hMul (α := LocalizedModule S A) (β := LocalizedModule S A) (mk a s)
    (mk ((algebraMap R A : (a : R) → A) r) 1 : LocalizedModule S A)
Tactic: rw [mk_mul_mk, mk_mul_mk, mul_comm, Algebra.commutes]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
T : Type u_1
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : IsLocalization S T
A : Type u_2
inst_6 : Semiring A
inst_7 : Algebra R A
r : R
a : A
s : ↥S
h :
  mk (HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) a) (1 * s) =
    HMul.hMul (α := LocalizedModule S A) (β := LocalizedModule S A) (mk a s)
      (mk ((algebraMap R A : (a : R) → A) r) 1 : LocalizedModule S A)
⊢ HMul.hMul (α := LocalizedModule S A) (β := LocalizedModule S A)
      (mk ((algebraMap R A : (a : R) → A) r) 1 : LocalizedModule S A) (mk a s) =
    HMul.hMul (α := LocalizedModule S A) (β := LocalizedModule S A) (mk a s)
      (mk ((algebraMap R A : (a : R) → A) r) 1 : LocalizedModule S A)
have h₁ : Eq (α := LocalizedModule S A) (mk (HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) a) (1 * s))
  (mk (HMul.hMul (β := A) a ((algebraMap R A : (a : R) → A) r : A)) (s * 1))
Tactic: rw [mk_mul_mk, mk_mul_mk, mul_comm, Algebra.commutes]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
T : Type u_1
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : IsLocalization S T
A : Type u_2
inst_6 : Semiring A
inst_7 : Algebra R A
r : R
a : A
s : ↥S
h :
  mk (HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) a) (1 * s) =
    HMul.hMul (α := LocalizedModule S A) (β := LocalizedModule S A) (mk a s)
      (mk ((algebraMap R A : (a : R) → A) r) 1 : LocalizedModule S A)
h₁ :
  Eq (α := LocalizedModule S A) (mk (HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) a) (1 * s))
    (mk (HMul.hMul (β := A) a ((algebraMap R A : (a : R) → A) r : A)) (s * 1))
⊢ HMul.hMul (α := LocalizedModule S A) (β := LocalizedModule S A)
      (mk ((algebraMap R A : (a : R) → A) r) 1 : LocalizedModule S A) (mk a s) =
    HMul.hMul (α := LocalizedModule S A) (β := LocalizedModule S A) (mk a s)
      (mk ((algebraMap R A : (a : R) → A) r) 1 : LocalizedModule S A)
have h₂ : Eq (α := LocalizedModule S A) (mk (HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) a) (s * 1))
  (mk (HMul.hMul (β := A) a ((algebraMap R A : (a : R) → A) r : A)) (s * 1))
Tactic: rw [mk_mul_mk, mk_mul_mk, mul_comm, Algebra.commutes]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
T : Type u_1
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : IsLocalization S T
A : Type u_2
inst_6 : Semiring A
inst_7 : Algebra R A
r : R
a : A
s : ↥S
h :
  mk (HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) a) (1 * s) =
    HMul.hMul (α := LocalizedModule S A) (β := LocalizedModule S A) (mk a s)
      (mk ((algebraMap R A : (a : R) → A) r) 1 : LocalizedModule S A)
h₁ :
  Eq (α := LocalizedModule S A) (mk (HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) a) (1 * s))
    (mk (HMul.hMul (β := A) a ((algebraMap R A : (a : R) → A) r : A)) (s * 1))
h₂ :
  Eq (α := LocalizedModule S A) (mk (HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) a) (s * 1))
    (mk (HMul.hMul (β := A) a ((algebraMap R A : (a : R) → A) r : A)) (s * 1))
⊢ HMul.hMul (α := LocalizedModule S A) (β := LocalizedModule S A)
      (mk ((algebraMap R A : (a : R) → A) r) 1 : LocalizedModule S A) (mk a s) =
    HMul.hMul (α := LocalizedModule S A) (β := LocalizedModule S A) (mk a s)
      (mk ((algebraMap R A : (a : R) → A) r) 1 : LocalizedModule S A)
have h₃ : Eq (α := LocalizedModule S A) (mk (HMul.hMul (β := A) a ((algebraMap R A : (a : R) → A) r : A)) (s * 1))
  (mk (HMul.hMul (β := A) a ((algebraMap R A : (a : R) → A) r : A)) (s * 1))
Tactic: rw [mk_mul_mk, mk_mul_mk, mul_comm, Algebra.commutes]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
T : Type u_1
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : IsLocalization S T
A : Type u_2
inst_6 : Semiring A
inst_7 : Algebra R A
r : R
x : LocalizedModule S A
⊢ r • x =
    HMul.hMul (α := LocalizedModule S A)
      ((RingHom.comp numeratorRingHom (algebraMap R A) : (a : R) → LocalizedModule S A) r : LocalizedModule S A) x
have h : ∀ (a : A) (s : ↥S),
  HSMul.hSMul (β := LocalizedModule S A) r (mk a s) =
    HMul.hMul (α := LocalizedModule S A) (β := LocalizedModule S A)
      ((RingHom.comp numeratorRingHom (algebraMap R A) : (a : R) → LocalizedModule S A) r : LocalizedModule S A)
      (mk a s)
Tactic: induction x using induction_on with | _ a s => _
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
T : Type u_1
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : IsLocalization S T
A : Type u_2
inst_6 : Semiring A
inst_7 : Algebra R A
r : R
a : A
s : ↥S
⊢ HSMul.hSMul (β := LocalizedModule S A) r (mk a s) =
    HMul.hMul (α := LocalizedModule S A) (β := LocalizedModule S A)
      (mk ((algebraMap R A : (a : R) → A) r) 1 : LocalizedModule S A) (mk a s)
have h : HSMul.hSMul (β := LocalizedModule S A) r (mk a s) =
  mk (HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) a) (1 * s)
Tactic: rw [mk_mul_mk, smul'_mk, Algebra.smul_def, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
T : Type u_1
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : IsLocalization S T
A : Type u_2
inst_6 : Semiring A
inst_7 : Algebra R A
r : R
a : A
s : ↥S
h :
  HSMul.hSMul (β := LocalizedModule S A) r (mk a s) =
    mk (HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) a) (1 * s)
⊢ HSMul.hSMul (β := LocalizedModule S A) r (mk a s) =
    HMul.hMul (α := LocalizedModule S A) (β := LocalizedModule S A)
      (mk ((algebraMap R A : (a : R) → A) r) 1 : LocalizedModule S A) (mk a s)
have h₁ : Eq (α := LocalizedModule S A) (mk (r • a) s) (mk (HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) a) (1 * s))
Tactic: rw [mk_mul_mk, smul'_mk, Algebra.smul_def, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
T : Type u_1
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : IsLocalization S T
A : Type u_2
inst_6 : Semiring A
inst_7 : Algebra R A
r : R
a : A
s : ↥S
h :
  HSMul.hSMul (β := LocalizedModule S A) r (mk a s) =
    mk (HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) a) (1 * s)
h₁ :
  Eq (α := LocalizedModule S A) (mk (r • a) s)
    (mk (HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) a) (1 * s))
⊢ HSMul.hSMul (β := LocalizedModule S A) r (mk a s) =
    HMul.hMul (α := LocalizedModule S A) (β := LocalizedModule S A)
      (mk ((algebraMap R A : (a : R) → A) r) 1 : LocalizedModule S A) (mk a s)
have h₂ : Eq (α := LocalizedModule S A) (mk (HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) a) s)
  (mk (HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) a) (1 * s))
Tactic: rw [mk_mul_mk, smul'_mk, Algebra.smul_def, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
T : Type u_1
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : IsLocalization S T
A : Type u_2
inst_6 : Semiring A
inst_7 : Algebra R A
r : R
a : A
s : ↥S
h :
  HSMul.hSMul (β := LocalizedModule S A) r (mk a s) =
    mk (HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) a) (1 * s)
h₁ :
  Eq (α := LocalizedModule S A) (mk (r • a) s)
    (mk (HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) a) (1 * s))
h₂ :
  Eq (α := LocalizedModule S A) (mk (HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) a) s)
    (mk (HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) a) (1 * s))
⊢ HSMul.hSMul (β := LocalizedModule S A) r (mk a s) =
    HMul.hMul (α := LocalizedModule S A) (β := LocalizedModule S A)
      (mk ((algebraMap R A : (a : R) → A) r) 1 : LocalizedModule S A) (mk a s)
have h₃ : Eq (α := LocalizedModule S A) (mk (HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) a) s)
  (mk (HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) a) s)
Tactic: rw [mk_mul_mk, smul'_mk, Algebra.smul_def, one_mul]