awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.LocalizedModule.IsLocalization
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
A : Type u_2
Aₛ : Type u_3
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : CommSemiring Aₛ
inst_4 : Algebra A Aₛ
inst_5 : Algebra R Aₛ
inst_6 : IsScalarTower R A Aₛ
refine_1 :
  (∀ (x : ↥S),
      IsUnit.{u_3} (M := Module.End R Aₛ)
        ((algebraMap R (Module.End R Aₛ) : (a : R) → Module.End R Aₛ) (↑x : R) : Module.End R Aₛ)) ↔
    ∀ (y : ↥(Algebra.algebraMapSubmonoid A S)), IsUnit.{u_3} (M := Aₛ) ((algebraMap A Aₛ : (a : A) → Aₛ) (↑y : A) : Aₛ)
refine_2 :
  ∀ (x : Aₛ),
    (∃ (x_1 : Prod.{u_2, u_1} A ↥S),
        x_1.2 • x = (AlgHom.toLinearMap (IsScalarTower.toAlgHom R A Aₛ) : (a : A) → Aₛ) x_1.1) ↔
      ∃ (x_1 : A × ↥(Algebra.algebraMapSubmonoid A S)),
        HMul.hMul (β := Aₛ) x ((algebraMap A Aₛ : (a : A) → Aₛ) (↑x_1.2 : A) : Aₛ) =
          (algebraMap A Aₛ : (a : A) → Aₛ) x_1.1
refine_3 :
  ∀ (x x_1 : A),
    (Eq.{u_3 + 1} (α := Aₛ) ((AlgHom.toLinearMap (IsScalarTower.toAlgHom R A Aₛ) : (a : A) → Aₛ) x : Aₛ)
          ((AlgHom.toLinearMap (IsScalarTower.toAlgHom R A Aₛ) : (a : A) → Aₛ) x_1 : Aₛ) →
        ∃ (c : ↥S), c • x = c • x_1) ↔
      Eq.{u_3 + 1} (α := Aₛ) ((algebraMap A Aₛ : (a : A) → Aₛ) x : Aₛ) ((algebraMap A Aₛ : (a : A) → Aₛ) x_1 : Aₛ) →
        ∃ (c : ↥(Algebra.algebraMapSubmonoid A S)), (↑c : A) * x = (↑c : A) * x_1
⊢ ((∀ (x : ↥S),
        IsUnit.{u_3} (M := Module.End R Aₛ)
          ((algebraMap R (Module.End R Aₛ) : (a : R) → Module.End R Aₛ) (↑x : R) : Module.End R Aₛ)) ∧
      (∀ (y : Aₛ),
          ∃ (x : Prod.{u_2, u_1} A ↥S),
            x.2 • y = (AlgHom.toLinearMap (IsScalarTower.toAlgHom R A Aₛ) : (a : A) → Aₛ) x.1) ∧
        ∀ {x₁ x₂ : A},
          Eq.{u_3 + 1} (α := Aₛ) ((AlgHom.toLinearMap (IsScalarTower.toAlgHom R A Aₛ) : (a : A) → Aₛ) x₁ : Aₛ)
              ((AlgHom.toLinearMap (IsScalarTower.toAlgHom R A Aₛ) : (a : A) → Aₛ) x₂ : Aₛ) →
            ∃ (c : ↥S), c • x₁ = c • x₂) ↔
    (∀ (y : ↥(Algebra.algebraMapSubmonoid A S)),
        IsUnit.{u_3} (M := Aₛ) ((algebraMap A Aₛ : (a : A) → Aₛ) (↑y : A) : Aₛ)) ∧
      (∀ (z : Aₛ),
          ∃ (x : A × ↥(Algebra.algebraMapSubmonoid A S)),
            HMul.hMul (β := Aₛ) z ((algebraMap A Aₛ : (a : A) → Aₛ) (↑x.2 : A) : Aₛ) =
              (algebraMap A Aₛ : (a : A) → Aₛ) x.1) ∧
        ∀ {x y : A},
          Eq.{u_3 + 1} (α := Aₛ) ((algebraMap A Aₛ : (a : A) → Aₛ) x : Aₛ) ((algebraMap A Aₛ : (a : A) → Aₛ) y : Aₛ) →
            ∃ (c : ↥(Algebra.algebraMapSubmonoid A S)), (↑c : A) * x = (↑c : A) * y

Tactic:
refine and_congr ?_ (and_congr (forall_congr' fun _ ↦ ?_) (forall₂_congr fun _ _ ↦ ?_))

Premises used: forall₂_congr, forall_congr', and_congr
-- Module: Mathlib.Algebra.Module.LocalizedModule.IsLocalization
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
A : Type u_2
Aₛ : Type u_3
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : CommSemiring Aₛ
inst_4 : Algebra A Aₛ
inst_5 : Algebra R Aₛ
inst_6 : IsScalarTower R A Aₛ
refine_1 :
  (∀ (x : ↥S),
      IsUnit (M := Module.End R Aₛ)
        ((Algebra.lmul R Aₛ : (a : Aₛ) → Module.End R Aₛ) ((algebraMap R Aₛ : (a : R) → Aₛ) (↑x : R) : Aₛ) :
          Module.End R Aₛ)) ↔
    ∀ (y : ↥(Algebra.algebraMapSubmonoid A S)), IsUnit.{u_3} (M := Aₛ) ((algebraMap A Aₛ : (a : A) → Aₛ) (↑y : A) : Aₛ)
refine_1₁ :
  (∀ (x : ↥S), IsUnit.{u_3} (M := Aₛ) ((algebraMap R Aₛ : (a : R) → Aₛ) (↑x : R) : Aₛ)) ↔
    ∀ (y : ↥(Algebra.algebraMapSubmonoid A S)), IsUnit.{u_3} (M := Aₛ) ((algebraMap A Aₛ : (a : A) → Aₛ) (↑y : A) : Aₛ)
refine_1₂ :
  (∀ (a : R) (b : a ∈ S), IsUnit.{u_3} (M := Aₛ) ((algebraMap R Aₛ : (a : R) → Aₛ) a : Aₛ)) ↔
    ∀ (a : A) (b : Membership.mem (γ := Submonoid A) (Algebra.algebraMapSubmonoid A S) a),
      IsUnit.{u_3} (M := Aₛ) ((algebraMap A Aₛ : (a : A) → Aₛ) a : Aₛ)
refine_1₃ :
  (∀ (a : R) (b : a ∈ S), IsUnit.{u_3} (M := Aₛ) ((algebraMap R Aₛ : (a : R) → Aₛ) a : Aₛ)) ↔
    ∀ (a : A) (b : Membership.mem (γ := Submonoid A) (Submonoid.map (F := R →+* A) (algebraMap R A) S) a),
      IsUnit.{u_3} (M := Aₛ) ((algebraMap A Aₛ : (a : A) → Aₛ) a : Aₛ)
refine_1₄ :
  (∀ (a : R) (b : a ∈ (↑S : Set R)), IsUnit.{u_3} (M := Aₛ) ((algebraMap R Aₛ : (a : R) → Aₛ) a : Aₛ)) ↔
    ∀ (a : A) (b : a ∈ (↑(Submonoid.map (F := R →+* A) (algebraMap R A) S) : Set A)),
      IsUnit.{u_3} (M := Aₛ) ((algebraMap A Aₛ : (a : A) → Aₛ) a : Aₛ)
refine_1₅ :
  (∀ (a : R) (b : a ∈ (↑S : Set R)), IsUnit.{u_3} (M := Aₛ) ((algebraMap R Aₛ : (a : R) → Aₛ) a : Aₛ)) ↔
    ∀ (a : A) (b : Membership.mem (γ := Set A) ((⇑(algebraMap R A) : (a : R) → A) '' (↑S : Set R)) a),
      IsUnit.{u_3} (M := Aₛ) ((algebraMap A Aₛ : (a : A) → Aₛ) a : Aₛ)
refine_1₆ :
  (∀ (a : R) (b : a ∈ (↑S : Set R)), IsUnit.{u_3} (M := Aₛ) ((algebraMap R Aₛ : (a : R) → Aₛ) a : Aₛ)) ↔
    ∀ ⦃x : R⦄,
      x ∈ (↑S : Set R) →
        IsUnit.{u_3} (M := Aₛ) ((algebraMap A Aₛ : (a : A) → Aₛ) ((algebraMap R A : (a : R) → A) x : A) : Aₛ)
⊢ (∀ (x : ↥S),
      IsUnit.{u_3} (M := Module.End R Aₛ)
        ((algebraMap R (Module.End R Aₛ) : (a : R) → Module.End R Aₛ) (↑x : R) : Module.End R Aₛ)) ↔
    ∀ (y : ↥(Algebra.algebraMapSubmonoid A S)), IsUnit.{u_3} (M := Aₛ) ((algebraMap A Aₛ : (a : A) → Aₛ) (↑y : A) : Aₛ)

Tactic:
simp_rw [← (Algebra.lmul R Aₛ).commutes, Algebra.lmul_isUnit_iff, Subtype.forall,
      Algebra.algebraMapSubmonoid, ← SetLike.mem_coe, Submonoid.coe_map,
      Set.forall_mem_image, ← IsScalarTower.algebraMap_apply]

Premises used: Algebra.lmul, Submonoid.coe_map, Subtype.forall, SetLike.mem_coe, AlgHom.commutes, Algebra.lmul_isUnit_iff, Algebra.algebraMapSubmonoid, IsScalarTower.algebraMap_apply, Set.forall_mem_image
-- Module: Mathlib.Algebra.Module.LocalizedModule.IsLocalization
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
A : Type u_2
Aₛ : Type u_3
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : CommSemiring Aₛ
inst_4 : Algebra A Aₛ
inst_5 : Algebra R Aₛ
inst_6 : IsScalarTower R A Aₛ
x : Aₛ
refine_2 :
  (∃ (a : A) (a_1 : R) (b : a_1 ∈ S),
      Subtype.mk (p := fun (a : R) ↦ a ∈ S) a_1 b • x =
        (AlgHom.toLinearMap (IsScalarTower.toAlgHom R A Aₛ) : (a : A) → Aₛ) a) ↔
    ∃ (a : A) (a_1 : A) (_ : Membership.mem (γ := Submonoid A) (Submonoid.map (F := R →+* A) (algebraMap R A) S) a_1),
      HMul.hMul (β := Aₛ) x ((algebraMap A Aₛ : (a : A) → Aₛ) a_1 : Aₛ) = (algebraMap A Aₛ : (a : A) → Aₛ) a
⊢ (∃ (x_1 : Prod.{u_2, u_1} A ↥S),
      x_1.2 • x = (AlgHom.toLinearMap (IsScalarTower.toAlgHom R A Aₛ) : (a : A) → Aₛ) x_1.1) ↔
    ∃ (x_1 : A × ↥(Algebra.algebraMapSubmonoid A S)),
      HMul.hMul (β := Aₛ) x ((algebraMap A Aₛ : (a : A) → Aₛ) (↑x_1.2 : A) : Aₛ) =
        (algebraMap A Aₛ : (a : A) → Aₛ) x_1.1

Tactic:
simp_rw [Prod.exists, Subtype.exists, Algebra.algebraMapSubmonoid]

Premises used: Subtype.exists, Algebra.algebraMapSubmonoid, Prod.exists
-- Module: Mathlib.Algebra.Module.LocalizedModule.IsLocalization
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
A : Type u_2
Aₛ : Type u_3
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : CommSemiring Aₛ
inst_4 : Algebra A Aₛ
inst_5 : Algebra R Aₛ
inst_6 : IsScalarTower R A Aₛ
x : Aₛ
⊢ (∃ (a : A) (a_1 : R) (b : a_1 ∈ S),
      Subtype.mk (p := fun (a : R) ↦ a ∈ S) a_1 b • x =
        (AlgHom.toLinearMap (IsScalarTower.toAlgHom R A Aₛ) : (a : A) → Aₛ) a) ↔
    ∃ (a : A) (a_1 : A) (_ : Membership.mem (γ := Submonoid A) (Submonoid.map (F := R →+* A) (algebraMap R A) S) a_1),
      HMul.hMul (β := Aₛ) x ((algebraMap A Aₛ : (a : A) → Aₛ) a_1 : Aₛ) = (algebraMap A Aₛ : (a : A) → Aₛ) a

Tactic:
simp [← IsScalarTower.algebraMap_apply, Submonoid.mk_smul, Algebra.smul_def, mul_comm]

Premises used: Submonoid.mk_smul, mul_comm, Algebra.smul_def, IsScalarTower.algebraMap_apply
-- Module: Mathlib.Algebra.Module.LocalizedModule.IsLocalization
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
A : Type u_2
Aₛ : Type u_3
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : CommSemiring Aₛ
inst_4 : Algebra A Aₛ
inst_5 : Algebra R Aₛ
inst_6 : IsScalarTower R A Aₛ
x x_1 : A
refine_3 :
  (Eq.{u_3 + 1} (α := Aₛ) ((AlgHom.toLinearMap (IsScalarTower.toAlgHom R A Aₛ) : (a : A) → Aₛ) x : Aₛ)
        ((AlgHom.toLinearMap (IsScalarTower.toAlgHom R A Aₛ) : (a : A) → Aₛ) x_1 : Aₛ) →
      ∃ (a : R) (b : a ∈ S),
        Subtype.mk (p := fun (a : R) ↦ a ∈ S) a b • x = Subtype.mk (p := fun (a : R) ↦ a ∈ S) a b • x_1) ↔
    Eq.{u_3 + 1} (α := Aₛ) ((algebraMap A Aₛ : (a : A) → Aₛ) x : Aₛ) ((algebraMap A Aₛ : (a : A) → Aₛ) x_1 : Aₛ) →
      ∃ (a : A) (_ : Membership.mem (γ := Submonoid A) (Submonoid.map (F := R →+* A) (algebraMap R A) S) a),
        a * x = a * x_1
⊢ (Eq.{u_3 + 1} (α := Aₛ) ((AlgHom.toLinearMap (IsScalarTower.toAlgHom R A Aₛ) : (a : A) → Aₛ) x : Aₛ)
        ((AlgHom.toLinearMap (IsScalarTower.toAlgHom R A Aₛ) : (a : A) → Aₛ) x_1 : Aₛ) →
      ∃ (c : ↥S), c • x = c • x_1) ↔
    Eq.{u_3 + 1} (α := Aₛ) ((algebraMap A Aₛ : (a : A) → Aₛ) x : Aₛ) ((algebraMap A Aₛ : (a : A) → Aₛ) x_1 : Aₛ) →
      ∃ (c : ↥(Algebra.algebraMapSubmonoid A S)), (↑c : A) * x = (↑c : A) * x_1

Tactic:
simp_rw [Subtype.exists, Algebra.algebraMapSubmonoid]

Premises used: Subtype.exists, Algebra.algebraMapSubmonoid
-- Module: Mathlib.Algebra.Module.LocalizedModule.IsLocalization
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
A : Type u_2
Aₛ : Type u_3
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : CommSemiring Aₛ
inst_4 : Algebra A Aₛ
inst_5 : Algebra R Aₛ
inst_6 : IsScalarTower R A Aₛ
x x_1 : A
⊢ (Eq.{u_3 + 1} (α := Aₛ) ((AlgHom.toLinearMap (IsScalarTower.toAlgHom R A Aₛ) : (a : A) → Aₛ) x : Aₛ)
        ((AlgHom.toLinearMap (IsScalarTower.toAlgHom R A Aₛ) : (a : A) → Aₛ) x_1 : Aₛ) →
      ∃ (a : R) (b : a ∈ S),
        Subtype.mk (p := fun (a : R) ↦ a ∈ S) a b • x = Subtype.mk (p := fun (a : R) ↦ a ∈ S) a b • x_1) ↔
    Eq.{u_3 + 1} (α := Aₛ) ((algebraMap A Aₛ : (a : A) → Aₛ) x : Aₛ) ((algebraMap A Aₛ : (a : A) → Aₛ) x_1 : Aₛ) →
      ∃ (a : A) (_ : Membership.mem (γ := Submonoid A) (Submonoid.map (F := R →+* A) (algebraMap R A) S) a),
        a * x = a * x_1

Tactic:
simp [Algebra.smul_def]

Premises used: Algebra.smul_def
-- Module: Mathlib.Algebra.Module.LocalizedModule.IsLocalization
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
A : Type u_2
Aₛ : Type u_3
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : CommSemiring Aₛ
inst_4 : Algebra A Aₛ
inst_5 : Algebra R Aₛ
inst_6 : IsScalarTower R A Aₛ
inst_7 : IsLocalization (Algebra.algebraMapSubmonoid A S) Aₛ
⊢ IsLocalizedModule S (AlgHom.toLinearMap (IsScalarTower.toAlgHom R A Aₛ))

Tactic:
isLocalizedModule_iff_isLocalization.mpr ‹_›

Premises used: Iff.mpr, isLocalizedModule_iff_isLocalization
-- Module: Mathlib.Algebra.Module.LocalizedModule.IsLocalization
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
⊢ IsLocalizedModule S (AlgHom.toLinearMap (IsScalarTower.toAlgHom R R A)) ↔
    IsLocalization (Algebra.algebraMapSubmonoid R S) A

Tactic:
isLocalizedModule_iff_isLocalization (S := S) (A := R) (Aₛ := A)

Premises used: isLocalizedModule_iff_isLocalization
-- Module: Mathlib.Algebra.Module.LocalizedModule.IsLocalization
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
h : S = Algebra.algebraMapSubmonoid R S
⊢ IsLocalizedModule S (Algebra.linearMap R A) ↔ IsLocalization S A

Tactic:
convert! isLocalizedModule_iff_isLocalization (S := S) (A := R) (Aₛ := A)

Premises used: isLocalizedModule_iff_isLocalization
-- Module: Mathlib.Algebra.Module.LocalizedModule.IsLocalization
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
⊢ S = Algebra.algebraMapSubmonoid R S

Tactic:
(Submonoid.map_id S).symm

Premises used: Submonoid.map_id, Submonoid.map, Algebra.algebraMapSubmonoid, Eq.symm
-- Module: Mathlib.Algebra.Module.LocalizedModule.IsLocalization
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
⊢ S = Algebra.algebraMapSubmonoid R S

Tactic:
exact (Submonoid.map_id S).symm

Premises used: Submonoid.map_id, Eq.symm
-- Module: Mathlib.Algebra.Module.LocalizedModule.IsLocalization
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
A : Type u_2
Aₛ : Type u_3
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : CommSemiring Aₛ
inst_4 : Algebra A Aₛ
inst_5 : Algebra R Aₛ
inst_6 : IsScalarTower R A Aₛ
inst_7 : IsLocalization S A
⊢ IsLocalizedModule S (Algebra.linearMap R A)

Tactic:
(isLocalizedModule_iff_isLocalization' S _).mpr inferInstance

Premises used: Iff.mpr, inferInstance, isLocalizedModule_iff_isLocalization'
-- Module: Mathlib.Algebra.Module.LocalizedModule.IsLocalization
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
A : Type u_2
Aₛ : Type u_3
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : CommSemiring Aₛ
inst_4 : Algebra A Aₛ
inst_5 : Algebra R Aₛ
inst_6 : IsScalarTower R A Aₛ
inst_7 : IsLocalization (Algebra.algebraMapSubmonoid A S) Aₛ
x : A
s : ↥S
rw :
  HSMul.hSMul.{u_2, u_3, u_3} (α := A) ((algebraMap R A : (a : R) → A) (↑s : R) : A)
      (mk' (M := Algebra.algebraMapSubmonoid A S) Aₛ x
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Algebra.algebraMapSubmonoid A S) x)
          ((algebraMap R A : (a : R) → A) (↑s : R)) ⋯)) =
    (AlgHom.toLinearMap (IsScalarTower.toAlgHom R A Aₛ) : (a : A) → Aₛ) x
⊢ mk' (M := Algebra.algebraMapSubmonoid A S) Aₛ x
      (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Algebra.algebraMapSubmonoid A S) x)
        ((algebraMap R A : (a : R) → A) (↑s : R)) ⋯) =
    IsLocalizedModule.mk' (AlgHom.toLinearMap (IsScalarTower.toAlgHom R A Aₛ)) x s

Tactic:
rw [← IsLocalizedModule.smul_inj (IsScalarTower.toAlgHom R A Aₛ).toLinearMap s,
    IsLocalizedModule.mk'_cancel', Submonoid.smul_def, ← algebraMap_smul A]

Premises used: AlgHom.toLinearMap, IsScalarTower.toAlgHom, algebraMap_smul, IsLocalizedModule.mk'_cancel', Submonoid.smul_def, IsLocalizedModule.smul_inj
-- Module: Mathlib.Algebra.Module.LocalizedModule.IsLocalization
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
A : Type u_2
Aₛ : Type u_3
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : CommSemiring Aₛ
inst_4 : Algebra A Aₛ
inst_5 : Algebra R Aₛ
inst_6 : IsScalarTower R A Aₛ
inst_7 : IsLocalization (Algebra.algebraMapSubmonoid A S) Aₛ
x : A
s : ↥S
⊢ HSMul.hSMul.{u_2, u_3, u_3} (α := A) ((algebraMap R A : (a : R) → A) (↑s : R) : A)
      (mk' (M := Algebra.algebraMapSubmonoid A S) Aₛ x
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Algebra.algebraMapSubmonoid A S) x)
          ((algebraMap R A : (a : R) → A) (↑s : R)) ⋯)) =
    (AlgHom.toLinearMap (IsScalarTower.toAlgHom R A Aₛ) : (a : A) → Aₛ) x

Tactic:
IsLocalization.smul_mk'_self (m := ⟨_, _⟩)

Premises used: IsLocalization.smul_mk'_self
-- Module: Mathlib.Algebra.Module.LocalizedModule.IsLocalization
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
A : Type u_2
Aₛ : Type u_3
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : CommSemiring Aₛ
inst_4 : Algebra A Aₛ
inst_5 : Algebra R Aₛ
inst_6 : IsScalarTower R A Aₛ
inst_7 : IsLocalization (Algebra.algebraMapSubmonoid A S) Aₛ
x : A
s : ↥S
⊢ HSMul.hSMul.{u_2, u_3, u_3} (α := A) ((algebraMap R A : (a : R) → A) (↑s : R) : A)
      (mk' (M := Algebra.algebraMapSubmonoid A S) Aₛ x
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Algebra.algebraMapSubmonoid A S) x)
          ((algebraMap R A : (a : R) → A) (↑s : R)) ⋯)) =
    (AlgHom.toLinearMap (IsScalarTower.toAlgHom R A Aₛ) : (a : A) → Aₛ) x

Tactic:
exact IsLocalization.smul_mk'_self (m := ⟨_, _⟩)

Premises used: IsLocalization.smul_mk'_self
-- Module: Mathlib.Algebra.Module.LocalizedModule.IsLocalization
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : IsLocalization S A
x : R
s : ↥S
rw : s • mk' A x s = (Algebra.linearMap R A : (a : R) → A) x
⊢ mk' A x s = IsLocalizedModule.mk' (Algebra.linearMap R A) x s

Tactic:
rw [← IsLocalizedModule.smul_inj (Algebra.linearMap R A) s, IsLocalizedModule.mk'_cancel']

Premises used: Algebra.linearMap, IsLocalizedModule.mk'_cancel', IsLocalizedModule.smul_inj
-- Module: Mathlib.Algebra.Module.LocalizedModule.IsLocalization
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : IsLocalization S A
x : R
s : ↥S
⊢ s • mk' A x s = (Algebra.linearMap R A : (a : R) → A) x

Tactic:
IsLocalization.smul_mk'_self

Premises used: IsLocalization.smul_mk'_self
-- Module: Mathlib.Algebra.Module.LocalizedModule.IsLocalization
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : IsLocalization S A
x : R
s : ↥S
⊢ s • mk' A x s = (Algebra.linearMap R A : (a : R) → A) x

Tactic:
exact IsLocalization.smul_mk'_self

Premises used: IsLocalization.smul_mk'_self
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Algebra R S
inst_7 : Module S N
inst_8 : IsScalarTower R S N
p : Submonoid R
inst_9 : IsLocalization p S
f : M →ₗ[R] N
inst_10 : IsLocalizedModule p f
M' M'' : Submodule R M
x y : N
h : Membership.mem (γ := Set N) {x : N | ∃ m ∈ M', ∃ (s : ↥p), IsLocalizedModule.mk' f m s = x} x
h_1 : Membership.mem (γ := Set N) {x : N | ∃ m ∈ M', ∃ (s : ↥p), IsLocalizedModule.mk' f m s = x} y
m : M
hm : m ∈ M'
s : ↥p
hx : IsLocalizedModule.mk' f m s = x
n : M
hn : n ∈ M'
t : ↥p
hy : IsLocalizedModule.mk' f n t = y
rw : IsLocalizedModule.mk' f (t • m + s • n) (s * t) = IsLocalizedModule.mk' f m s + y
rw₁ : IsLocalizedModule.mk' f (t • m + s • n) (s * t) = IsLocalizedModule.mk' f m s + IsLocalizedModule.mk' f n t
rw₂ rw₃ : IsLocalizedModule.mk' f (t • m + s • n) (s * t) = IsLocalizedModule.mk' f (t • m + s • n) (s * t)
⊢ IsLocalizedModule.mk' f (t • m + s • n) (s * t) = x + y

Tactic:
rw [← hx, ← hy, IsLocalizedModule.mk'_add_mk']

Premises used: IsLocalizedModule.mk'_add_mk'
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Algebra R S
inst_7 : Module S N
inst_8 : IsScalarTower R S N
p : Submonoid R
inst_9 : IsLocalization p S
f : M →ₗ[R] N
inst_10 : IsLocalizedModule p f
M' M'' : Submodule R M
⊢ IsLocalizedModule.mk' (S := p) f 0 1 = 0

Tactic:
simp
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Algebra R S
inst_7 : Module S N
inst_8 : IsScalarTower R S N
p : Submonoid R
inst_9 : IsLocalization p S
f : M →ₗ[R] N
inst_10 : IsLocalizedModule p f
M' M'' : Submodule R M
r : R
x : N
m : M
hm : m ∈ M'
s : ↥p
hx : IsLocalizedModule.mk' f m s = x
rw : r • IsLocalizedModule.mk' f m s = r • x
rw₁ rw₂ : r • x = r • x
⊢ IsLocalizedModule.mk' f (r • m) s = r • x

Tactic:
rw [IsLocalizedModule.mk'_smul, hx]

Premises used: IsLocalizedModule.mk'_smul
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Algebra R S
inst_7 : Module S N
inst_8 : IsScalarTower R S N
p : Submonoid R
inst_9 : IsLocalization p S
f : M →ₗ[R] N
inst_10 : IsLocalizedModule p f
M' M'' : Submodule R M
r : R
x : N
m : M
hm : m ∈ M'
s : ↥p
hx : IsLocalizedModule.mk' f m s = x
⊢ Membership.mem (γ := Set N) {x : N | ∃ m ∈ M', ∃ (s : ↥p), IsLocalizedModule.mk' f m s = x} (r • x)

Tactic:
exact ⟨r • m, smul_mem M' _ hm, s, by rw [IsLocalizedModule.mk'_smul, hx]⟩
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Algebra R S
inst_7 : Module S N
inst_8 : IsScalarTower R S N
p : Submonoid R
inst_9 : IsLocalization p S
f : M →ₗ[R] N
inst_10 : IsLocalizedModule p f
M' M'' : Submodule R M
r : S
x : N
h : x ∈ (localized₀ p f M').carrier
m : M
hm : m ∈ M'
s : ↥p
hx : IsLocalizedModule.mk' f m s = x
have : ∀ (y : R) (t : ↥p) (hyt : IsLocalization.mk' S y t = r), r • x ∈ (localized₀ p f M').carrier
⊢ r • x ∈ (localized₀ p f M').carrier

Tactic:
have ⟨y, t, hyt⟩ := IsLocalization.exists_mk'_eq p r
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Algebra R S
inst_7 : Module S N
inst_8 : IsScalarTower R S N
p : Submonoid R
inst_9 : IsLocalization p S
f : M →ₗ[R] N
inst_10 : IsLocalizedModule p f
M' M'' : Submodule R M
r : S
x : N
h : x ∈ (localized₀ p f M').carrier
m : M
hm : m ∈ M'
s : ↥p
hx : IsLocalizedModule.mk' f m s = x
y : R
t : ↥p
hyt : IsLocalization.mk' S y t = r
⊢ IsLocalizedModule.mk' f (y • m) (t * s) = r • x

Tactic:
simp [← hyt, ← hx, IsLocalizedModule.mk'_smul_mk']

Premises used: IsLocalizedModule.mk'_smul_mk'
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Algebra R S
inst_7 : Module S N
inst_8 : IsScalarTower R S N
p : Submonoid R
inst_9 : IsLocalization p S
f : M →ₗ[R] N
inst_10 : IsLocalizedModule p f
M' M'' : Submodule R M
r : S
x : N
h : x ∈ (localized₀ p f M').carrier
m : M
hm : m ∈ M'
s : ↥p
hx : IsLocalizedModule.mk' f m s = x
y : R
t : ↥p
hyt : IsLocalization.mk' S y t = r
⊢ r • x ∈ (localized₀ p f M').carrier

Tactic:
exact ⟨y • m, M'.smul_mem y hm, t * s, by simp [← hyt, ← hx, IsLocalizedModule.mk'_smul_mk']⟩
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst_5 : IsLocalizedModule p f
M' : Submodule R M
x : N
⊢ x ∈ localized₀ p f M' ↔ ∃ m ∈ M', ∃ (s : ↥p), IsLocalizedModule.mk' f m s = x

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Algebra R S
inst_7 : Module S N
inst_8 : IsScalarTower R S N
p : Submonoid R
inst_9 : IsLocalization p S
f : M →ₗ[R] N
inst_10 : IsLocalizedModule p f
M' : Submodule R M
x : N
⊢ Membership.mem (γ := Submodule S N) (localized' S p f M') x ↔ ∃ m ∈ M', ∃ (s : ↥p), IsLocalizedModule.mk' f m s = x

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Algebra R S
inst_7 : Module S N
inst_8 : IsScalarTower R S N
p : Submonoid R
inst_9 : IsLocalization p S
f : M →ₗ[R] N
inst_10 : IsLocalizedModule p f
M' : Submodule R M
⊢ restrictScalars R (localized' S p f M') = localized₀ p f M'

Tactic:
rfl

Premises used: Submodule.restrictScalars, setOf, rfl, Submodule.localized₀