awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
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
x : T
a₁ s₁ : A
a₂ s₂ : ↥S
h :
  HSMul.hSMul (β := LocalizedModule S A) x (mk a₁ a₂) * mk s₁ s₂ =
    HSMul.hSMul (β := LocalizedModule S A) x (mk (a₁ * s₁) (a₂ * s₂))
h₁ :
  HMul.hMul (α := LocalizedModule S A) (mk ((IsLocalization.sec S x).1 • a₁) ((IsLocalization.sec S x).2 * a₂))
      (mk s₁ s₂) =
    HSMul.hSMul (β := LocalizedModule S A) x (mk (a₁ * s₁) (a₂ * s₂))
h₂ :
  HMul.hMul (α := LocalizedModule S A) (mk ((IsLocalization.sec S x).1 • a₁) ((IsLocalization.sec S x).2 * a₂))
      (mk s₁ s₂) =
    mk ((IsLocalization.sec S x).1 • (a₁ * s₁)) ((IsLocalization.sec S x).2 * (a₂ * s₂))
h₃ :
  Eq (α := LocalizedModule S A) (mk ((IsLocalization.sec S x).1 • a₁ * s₁) ((IsLocalization.sec S x).2 * a₂ * s₂))
    (mk ((IsLocalization.sec S x).1 • (a₁ * s₁)) ((IsLocalization.sec S x).2 * (a₂ * s₂)))
h₄ :
  Eq (α := LocalizedModule S A) (mk ((IsLocalization.sec S x).1 • a₁ * s₁) ((IsLocalization.sec S x).2 * (a₂ * s₂)))
    (mk ((IsLocalization.sec S x).1 • (a₁ * s₁)) ((IsLocalization.sec S x).2 * (a₂ * s₂)))
h₅ h₆ :
  Eq (α := LocalizedModule S A) (mk ((IsLocalization.sec S x).1 • (a₁ * s₁)) ((IsLocalization.sec S x).2 * (a₂ * s₂)))
    (mk ((IsLocalization.sec S x).1 • (a₁ * s₁)) ((IsLocalization.sec S x).2 * (a₂ * s₂)))
⊢ HSMul.hSMul (β := LocalizedModule S A) x (mk a₁ a₂) * mk s₁ s₂ =
    x • HMul.hMul (α := LocalizedModule S A) (mk a₁ a₂) (mk s₁ s₂)

Tactic:
rw [mk_mul_mk, smul_def, smul_def, mk_mul_mk, mul_assoc, smul_mul_assoc]

Premises used: LocalizedModule.mk_mul_mk, mul_assoc, smul_mul_assoc, LocalizedModule.smul_def
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
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
x : T
a₁ s₁ : A
a₂ s₂ : ↥S
⊢ mk a₁ a₂ * HSMul.hSMul (β := LocalizedModule S A) x (mk s₁ s₂) =
    x • HMul.hMul (α := LocalizedModule S A) (mk a₁ a₂) (mk s₁ s₂)

Tactic:
_
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
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
x : T
p₁ p₂ : LocalizedModule S A
h :
  ∀ (a₁ s₁ : A) (a₂ s₂ : ↥S),
    mk a₁ a₂ * HSMul.hSMul (β := LocalizedModule S A) x (mk s₁ s₂) =
      x • HMul.hMul (α := LocalizedModule S A) (mk a₁ a₂) (mk s₁ s₂)
⊢ p₁ * x • p₂ = x • (p₁ * p₂)

Tactic:
induction p₁, p₂ using induction_on₂ with | _ a₁ s₁ a₂ s₂ => _
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
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
x : T
a₁ s₁ : A
a₂ s₂ : ↥S
h :
  HMul.hMul (α := LocalizedModule S A) (mk a₁ a₂)
      (mk ((IsLocalization.sec S x).1 • s₁) ((IsLocalization.sec S x).2 * s₂)) =
    x • HMul.hMul (α := LocalizedModule S A) (mk a₁ a₂) (mk s₁ s₂)
h₁ :
  mk (a₁ * (IsLocalization.sec S x).1 • s₁) (a₂ * ((IsLocalization.sec S x).2 * s₂)) =
    x • HMul.hMul (α := LocalizedModule S A) (mk a₁ a₂) (mk s₁ s₂)
h₂ :
  mk (a₁ * (IsLocalization.sec S x).1 • s₁) (a₂ * ((IsLocalization.sec S x).2 * s₂)) =
    HSMul.hSMul (β := LocalizedModule S A) x (mk (a₁ * s₁) (a₂ * s₂))
h₃ :
  Eq (α := LocalizedModule S A) (mk (a₁ * (IsLocalization.sec S x).1 • s₁) (a₂ * ((IsLocalization.sec S x).2 * s₂)))
    (mk ((IsLocalization.sec S x).1 • (a₁ * s₁)) ((IsLocalization.sec S x).2 * (a₂ * s₂)))
h₄ :
  Eq (α := LocalizedModule S A) (mk (a₁ * (IsLocalization.sec S x).1 • s₁) ((IsLocalization.sec S x).2 * (a₂ * s₂)))
    (mk ((IsLocalization.sec S x).1 • (a₁ * s₁)) ((IsLocalization.sec S x).2 * (a₂ * s₂)))
h₅ h₆ :
  Eq (α := LocalizedModule S A) (mk ((IsLocalization.sec S x).1 • (a₁ * s₁)) ((IsLocalization.sec S x).2 * (a₂ * s₂)))
    (mk ((IsLocalization.sec S x).1 • (a₁ * s₁)) ((IsLocalization.sec S x).2 * (a₂ * s₂)))
⊢ mk a₁ a₂ * HSMul.hSMul (β := LocalizedModule S A) x (mk s₁ s₂) =
    x • HMul.hMul (α := LocalizedModule S A) (mk a₁ a₂) (mk s₁ s₂)

Tactic:
rw [smul_def, mk_mul_mk, mk_mul_mk, smul_def, mul_left_comm, mul_smul_comm]

Premises used: LocalizedModule.mk_mul_mk, mul_left_comm, LocalizedModule.smul_def, mul_smul_comm
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
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
change :
  HSMul.hSMul (β := LocalizedModule S A) (IsLocalization.mk' T a s) (mk 1 1) = mk ((algebraMap R A : (a : R) → A) a) s
⊢ HSMul.hSMul (β := LocalizedModule S A) (IsLocalization.mk' T a s) 1 = mk ((algebraMap R A : (a : R) → A) a) s

Tactic:
change _ • mk _ _ = _

Premises used: LocalizedModule.mk
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
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)
rw₂ rw₃ : Eq (α := LocalizedModule S A) (mk (HSMul.hSMul (β := A) a 1) s) (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

Tactic:
rw [mk'_smul_mk, Algebra.algebraMap_eq_smul_one, mul_one]

Premises used: Algebra.algebraMap_eq_smul_one, LocalizedModule.mk'_smul_mk, mul_one
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
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
rw₃ :
  HSMul.hSMul (β := LocalizedModule S A) (IsLocalization.mk' T a s) (mk 1 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)

Tactic:
with_unfolding_all
  rw [Algebra.algebraMap_eq_smul_one]
  change _ • mk _ _ = _
  rw [mk'_smul_mk, Algebra.algebraMap_eq_smul_one, mul_one]

Premises used: LocalizedModule.mk, Algebra.algebraMap_eq_smul_one, LocalizedModule.mk'_smul_mk, mul_one
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
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
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)
⊢ 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)

Tactic:
rw [Localization.mk_eq_mk']

Premises used: Localization.mk_eq_mk'
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
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)
        (IsLocalization.mk' (Localization (M := R) S) a s) :
      LocalizedModule S A)
    (mk ((algebraMap R A : (a : R) → A) a) s : LocalizedModule S A)

Tactic:
algebraMap_mk' ..

Premises used: LocalizedModule.algebraMap_mk'
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
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)
        (IsLocalization.mk' (Localization (M := R) S) a s) :
      LocalizedModule S A)
    (mk ((algebraMap R A : (a : R) → A) a) s : LocalizedModule S A)

Tactic:
exact algebraMap_mk' ..

Premises used: LocalizedModule.algebraMap_mk'
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
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
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)
⊢ (r • x) • p = r • x • p

Tactic:
induction p with | _ m s
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
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))
h₅ 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)

Tactic:
rw [← IsLocalization.mk'_sec (M := S) T x, IsLocalization.smul_mk', mk'_smul_mk, mk'_smul_mk,
      smul'_mk, mul_smul]

Premises used: IsLocalization.smul_mk', LocalizedModule.smul'_mk, IsLocalization.mk'_sec, LocalizedModule.mk'_smul_mk, SemigroupAction.mul_smul
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
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
⊢ Eq (α := OreLocalization S A) (mk 1 1) 1

Tactic:
simp [OreLocalization.one_def]

Premises used: OreLocalization.one_def
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
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
⊢ ∀ (x y : A), mk (x * y) 1 = HMul.hMul (α := OreLocalization S A) (mk x 1) (mk y 1)

Tactic:
simp [mk_mul_mk]

Premises used: LocalizedModule.mk_mul_mk
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
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
⊢ Eq (α := OreLocalization S A) (mk 0 1) 0

Tactic:
simp
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
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
⊢ ∀ (x y : A), mk (x + y) 1 = HAdd.hAdd (α := OreLocalization S A) (mk x 1) (mk y 1)

Tactic:
simp
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
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)
      ((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:
_
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
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
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)
⊢ 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)

Tactic:
induction x using induction_on with | _ a s => _
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
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))
h₃ 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))
⊢ 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)

Tactic:
rw [mk_mul_mk, mk_mul_mk, mul_comm, Algebra.commutes]

Premises used: LocalizedModule.mk_mul_mk, mul_comm, Algebra.commutes
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
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)
      ((RingHom.comp numeratorRingHom (algebraMap R A) : (a : R) → LocalizedModule S A) r : LocalizedModule S A)
      (mk a s)

Tactic:
_
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
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
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)
⊢ r • x =
    HMul.hMul (α := LocalizedModule S A)
      ((RingHom.comp numeratorRingHom (algebraMap R A) : (a : R) → LocalizedModule S A) r : LocalizedModule S A) x

Tactic:
induction x using induction_on with | _ a s => _
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
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))
h₃ 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)
⊢ 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)

Tactic:
rw [mk_mul_mk, smul'_mk, Algebra.smul_def, one_mul]

Premises used: LocalizedModule.mk_mul_mk, LocalizedModule.smul'_mk, Algebra.smul_def, one_mul
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
⊢ Eq.{u + 1} (α := Algebra R (OreLocalization S R)) OreLocalization.instAlgebra algebra'

Tactic:
rfl
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
⊢ Eq.{u + 1} (α := Algebra R (OreLocalization S R)) OreLocalization.instAlgebra algebra'

Tactic:
with_reducible_and_instances rfl
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
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
x y : M
⊢ mk (x + y) 1 = HAdd.hAdd (α := LocalizedModule S M) (mk x 1) (mk y 1)

Tactic:
simp
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
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
x : R
x_1 : M
⊢ mk (x • x_1) 1 = HSMul.hSMul (α := R) (β := LocalizedModule S M) ((RingHom.id R : (a : R) → R) x : R) (mk x_1 1)

Tactic:
simp [mk, OreLocalization.smul_oreDiv]

Premises used: LocalizedModule.mk, OreLocalization.smul_oreDiv
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
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
s : ↥S
p : LocalizedModule S M
x x_1 : Prod.{v, u} M ↥S
a : M
b : ↥S
a' : M
b' : ↥S
h : (a, b) ≈ (a', b')
c : ↥S
eq1 : c • (a', b').2 • (a, b).1 = c • (a, b).2 • (a', b').1
rw : c • (a', b').2 • s • (a, b).1 = c • ((a, b).2 * s) • (a', b').1
rw₁ : c • (a', b').2 • s • (a, b).1 = c • (a, b).2 • s • (a', b').1
rw₂ : c • s • (a', b').2 • (a, b).1 = c • (a, b).2 • s • (a', b').1
rw₃ : s • c • (a', b').2 • (a, b).1 = c • (a, b).2 • s • (a', b').1
rw₄ : s • c • (a, b).2 • (a', b').1 = c • (a, b).2 • s • (a', b').1
rw₅ : s • c • (a, b).2 • (a', b').1 = c • s • (a, b).2 • (a', b').1
rw₆ rw₇ : s • c • (a, b).2 • (a', b').1 = s • c • (a, b).2 • (a', b').1
⊢ c • ((a', b').2 * s) • (a, b).1 = c • ((a, b).2 * s) • (a', b').1

Tactic:
rw [mul_smul, mul_smul, smul_comm _ s, smul_comm _ s, eq1, smul_comm _ s,
        smul_comm _ s]

Premises used: SMulCommClass.smul_comm, SemigroupAction.mul_smul
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
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
s : ↥S
x y : LocalizedModule S M
⊢ (x + y).liftOn (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s)) ⋯ =
    HAdd.hAdd (α := LocalizedModule S M) (x.liftOn (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s)) ⋯)
      (y.liftOn (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s)) ⋯)

Tactic:
x.induction_on₂ ?_ y

Premises used: LocalizedModule.induction_on₂
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
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
s : ↥S
x y : LocalizedModule S M
refine :
  ∀ (m m' : M) (s_1 s' : ↥S),
    (HAdd.hAdd (α := LocalizedModule S M) (mk m s_1) (mk m' s')).liftOn (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s))
        ⋯ =
      HAdd.hAdd (α := LocalizedModule S M) (liftOn (mk m s_1) (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s)) ⋯)
        (liftOn (mk m' s') (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s)) ⋯)
⊢ (x + y).liftOn (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s)) ⋯ =
    HAdd.hAdd (α := LocalizedModule S M) (x.liftOn (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s)) ⋯)
      (y.liftOn (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s)) ⋯)

Tactic:
refine x.induction_on₂ ?_ y