awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Localization.LocalizationLocalization
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
inst_1 : IsDomain R
S : Type u_2
T : Type u_3
inst_2 : CommRing S
inst_3 : CommRing T
inst_4 : Algebra R S
inst_5 : Algebra R T
inst_6 : Algebra S T
inst_7 : IsScalarTower R S T
inst_8 : IsLocalization M S
inst_9 : IsFractionRing R T
this_1 : Nontrivial T
this : Nontrivial S
x : R
hx : x ∈ M
hx' : x = 0
⊢ ∃ (m : ↥M), (↑m : R) * 1 = 0

Tactic:
exact ⟨⟨x, hx⟩, by simp [hx']⟩
-- Module: Mathlib.RingTheory.Localization.LocalizationLocalization
Goal:
R_1 : Type u_1
inst : CommRing R_1
M : Submonoid R_1
R : Type u_2
inst_1 : CommRing R
inst_2 : IsDomain R
p : Ideal R
inst_3 : p.IsPrime
⊢ IsFractionRing.{u_2, u_2} (Localization.AtPrime p) (FractionRing R)

Tactic:
IsFractionRing.isFractionRing_of_isDomain_of_isLocalization p.primeCompl
    (Localization.AtPrime p) (FractionRing R)

Premises used: Localization.AtPrime, FractionRing, IsFractionRing.isFractionRing_of_isDomain_of_isLocalization, Ideal.primeCompl
-- Module: Mathlib.RingTheory.Localization.Module
Goal:
R : Type u_1
Rₛ : Type u_2
inst : CommSemiring R
S : Submonoid R
inst_1 : CommSemiring Rₛ
inst_2 : Algebra R Rₛ
inst_3 : IsLocalization S Rₛ
M : Type u_3
Mₛ : Type u_4
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : AddCommMonoid Mₛ
inst_7 : Module R Mₛ
inst_8 : Module Rₛ Mₛ
inst_9 : IsScalarTower R Rₛ Mₛ
f : M →ₗ[R] Mₛ
inst_10 : IsLocalizedModule S f
v : Set M
hv : Eq (α := Submodule R M) (span R v) ⊤
x : Mₛ
h : Membership.mem (γ := Submodule Rₛ Mₛ) ⊤ x
obtain :
  ∀ (m : M) (s : ↥S) (h : (m, s).2 • x = (f : (a : M) → Mₛ) (m, s).1),
    Membership.mem (γ := Submodule Rₛ Mₛ) (span Rₛ ((⇑f : (a : M) → Mₛ) '' v)) x
⊢ Membership.mem (γ := Submodule Rₛ Mₛ) (span Rₛ ((⇑f : (a : M) → Mₛ) '' v)) x

Tactic:
obtain ⟨⟨m, s⟩, h⟩ := IsLocalizedModule.surj S f x

Premises used: IsLocalizedModule.surj
-- Module: Mathlib.RingTheory.Localization.Module
Goal:
R : Type u_1
Rₛ : Type u_2
inst : CommSemiring R
S : Submonoid R
inst_1 : CommSemiring Rₛ
inst_2 : Algebra R Rₛ
inst_3 : IsLocalization S Rₛ
M : Type u_3
Mₛ : Type u_4
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : AddCommMonoid Mₛ
inst_7 : Module R Mₛ
inst_8 : Module Rₛ Mₛ
inst_9 : IsScalarTower R Rₛ Mₛ
f : M →ₗ[R] Mₛ
inst_10 : IsLocalizedModule S f
v : Set M
hv : Eq (α := Submodule R M) (span R v) ⊤
x : Mₛ
h_1 : Membership.mem (γ := Submodule Rₛ Mₛ) ⊤ x
m : M
s : ↥S
h : (m, s).2 • x = (f : (a : M) → Mₛ) (m, s).1
⊢ HSMul.hSMul (α := Rₛˣ) (β := Mₛ) (IsUnit.unit (a := (algebraMap R Rₛ : (a : R) → Rₛ) (↑s : R)) ⋯)⁻¹
      ((f : (a : M) → Mₛ) (m, s).1 : Mₛ) =
    x

Tactic:
rw [Submonoid.smul_def, ← algebraMap_smul Rₛ, ← Units.smul_isUnit (IsLocalization.map_units Rₛ s),
    eq_comm, ← inv_smul_eq_iff] at h

Premises used: inv_smul_eq_iff, Units.smul_isUnit, algebraMap_smul, eq_comm, Submonoid.smul_def, IsLocalization.map_units
-- Module: Mathlib.RingTheory.Localization.Module
Goal:
R : Type u_1
Rₛ : Type u_2
inst : CommSemiring R
S : Submonoid R
inst_1 : CommSemiring Rₛ
inst_2 : Algebra R Rₛ
inst_3 : IsLocalization S Rₛ
M : Type u_3
Mₛ : Type u_4
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : AddCommMonoid Mₛ
inst_7 : Module R Mₛ
inst_8 : Module Rₛ Mₛ
inst_9 : IsScalarTower R Rₛ Mₛ
f : M →ₗ[R] Mₛ
inst_10 : IsLocalizedModule S f
v : Set M
hv : Eq (α := Submodule R M) (span R v) ⊤
x : Mₛ
h_1 : Membership.mem (γ := Submodule Rₛ Mₛ) ⊤ x
m : M
s : ↥S
h :
  HSMul.hSMul (α := Rₛˣ) (β := Mₛ) (IsUnit.unit (a := (algebraMap R Rₛ : (a : R) → Rₛ) (↑s : R)) ⋯)⁻¹
      ((f : (a : M) → Mₛ) (m, s).1 : Mₛ) =
    x
⊢ Membership.mem (γ := Submodule Rₛ Mₛ) (span Rₛ ((⇑f : (a : M) → Mₛ) '' v)) x

Tactic:
h ▸ smul_mem _ _ (span_subset_span R Rₛ _ ?_)

Premises used: Submodule.span_subset_span, Eq.rec, Submodule.smul_mem
-- Module: Mathlib.RingTheory.Localization.Module
Goal:
R : Type u_1
Rₛ : Type u_2
inst : CommSemiring R
S : Submonoid R
inst_1 : CommSemiring Rₛ
inst_2 : Algebra R Rₛ
inst_3 : IsLocalization S Rₛ
M : Type u_3
Mₛ : Type u_4
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : AddCommMonoid Mₛ
inst_7 : Module R Mₛ
inst_8 : Module Rₛ Mₛ
inst_9 : IsScalarTower R Rₛ Mₛ
f : M →ₗ[R] Mₛ
inst_10 : IsLocalizedModule S f
v : Set M
hv : Eq (α := Submodule R M) (span R v) ⊤
x : Mₛ
h_1 : Membership.mem (γ := Submodule Rₛ Mₛ) ⊤ x
m : M
s : ↥S
h :
  HSMul.hSMul (α := Rₛˣ) (β := Mₛ) (IsUnit.unit (a := (algebraMap R Rₛ : (a : R) → Rₛ) (↑s : R)) ⋯)⁻¹
      ((f : (a : M) → Mₛ) (m, s).1 : Mₛ) =
    x
refine : Membership.mem (α := Mₛ) (↑(span R ((⇑f : (a : M) → Mₛ) '' v)) : Set Mₛ) ((f : (a : M) → Mₛ) (m, s).1 : Mₛ)
⊢ Membership.mem (γ := Submodule Rₛ Mₛ) (span Rₛ ((⇑f : (a : M) → Mₛ) '' v)) x

Tactic:
refine h ▸ smul_mem _ _ (span_subset_span R Rₛ _ ?_)
-- Module: Mathlib.RingTheory.Localization.Module
Goal:
R : Type u_1
Rₛ : Type u_2
inst : CommSemiring R
S : Submonoid R
inst_1 : CommSemiring Rₛ
inst_2 : Algebra R Rₛ
inst_3 : IsLocalization S Rₛ
M : Type u_3
Mₛ : Type u_4
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : AddCommMonoid Mₛ
inst_7 : Module R Mₛ
inst_8 : Module Rₛ Mₛ
inst_9 : IsScalarTower R Rₛ Mₛ
f : M →ₗ[R] Mₛ
inst_10 : IsLocalizedModule S f
v : Set M
hv : Eq (α := Submodule R M) (span R v) ⊤
x : Mₛ
h_1 : Membership.mem (γ := Submodule Rₛ Mₛ) ⊤ x
m : M
s : ↥S
h :
  HSMul.hSMul (α := Rₛˣ) (β := Mₛ) (IsUnit.unit (a := (algebraMap R Rₛ : (a : R) → Rₛ) (↑s : R)) ⋯)⁻¹
      ((f : (a : M) → Mₛ) (m, s).1 : Mₛ) =
    x
rw :
  Membership.mem (α := Mₛ)
    (↑(map
          ((↑R :
              {S : Type u_1} →
                {M : Type u_3} →
                  {M₂ : Type u_4} →
                    [inst : Semiring R] →
                      [inst_11 : Semiring S] →
                        [inst_12 : AddCommMonoid M] →
                          [inst_13 : AddCommMonoid M₂] →
                            [inst_14 : Module R M] →
                              [inst_15 : Module R M₂] →
                                [inst_16 : Module S M] →
                                  [inst_17 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
            f)
          ⊤) :
      Set Mₛ)
    (((↑R :
              {S : Type u_1} →
                {M : Type u_3} →
                  {M₂ : Type u_4} →
                    [inst : Semiring R] →
                      [inst_11 : Semiring S] →
                        [inst_12 : AddCommMonoid M] →
                          [inst_13 : AddCommMonoid M₂] →
                            [inst_14 : Module R M] →
                              [inst_15 : Module R M₂] →
                                [inst_16 : Module S M] →
                                  [inst_17 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
            f :
          (a : M) → Mₛ)
        (m, s).1 :
      Mₛ)
⊢ Membership.mem (α := Mₛ) (↑(span R ((⇑f : (a : M) → Mₛ) '' v)) : Set Mₛ) ((f : (a : M) → Mₛ) (m, s).1 : Mₛ)

Tactic:
rw [← LinearMap.coe_restrictScalars R, ← LinearMap.map_span, hv]

Premises used: LinearMap.coe_restrictScalars, LinearMap.map_span
-- Module: Mathlib.RingTheory.Localization.Module
Goal:
R : Type u_1
Rₛ : Type u_2
inst : CommSemiring R
S : Submonoid R
inst_1 : CommSemiring Rₛ
inst_2 : Algebra R Rₛ
inst_3 : IsLocalization S Rₛ
M : Type u_3
Mₛ : Type u_4
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : AddCommMonoid Mₛ
inst_7 : Module R Mₛ
inst_8 : Module Rₛ Mₛ
inst_9 : IsScalarTower R Rₛ Mₛ
f : M →ₗ[R] Mₛ
inst_10 : IsLocalizedModule S f
v : Set M
hv : Eq (α := Submodule R M) (span R v) ⊤
x : Mₛ
h_1 : Membership.mem (γ := Submodule Rₛ Mₛ) ⊤ x
m : M
s : ↥S
h :
  HSMul.hSMul (α := Rₛˣ) (β := Mₛ) (IsUnit.unit (a := (algebraMap R Rₛ : (a : R) → Rₛ) (↑s : R)) ⋯)⁻¹
      ((f : (a : M) → Mₛ) (m, s).1 : Mₛ) =
    x
⊢ Membership.mem (α := Mₛ)
    (↑(map
          ((↑R :
              {S : Type u_1} →
                {M : Type u_3} →
                  {M₂ : Type u_4} →
                    [inst : Semiring R] →
                      [inst_11 : Semiring S] →
                        [inst_12 : AddCommMonoid M] →
                          [inst_13 : AddCommMonoid M₂] →
                            [inst_14 : Module R M] →
                              [inst_15 : Module R M₂] →
                                [inst_16 : Module S M] →
                                  [inst_17 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
            f)
          ⊤) :
      Set Mₛ)
    (((↑R :
              {S : Type u_1} →
                {M : Type u_3} →
                  {M₂ : Type u_4} →
                    [inst : Semiring R] →
                      [inst_11 : Semiring S] →
                        [inst_12 : AddCommMonoid M] →
                          [inst_13 : AddCommMonoid M₂] →
                            [inst_14 : Module R M] →
                              [inst_15 : Module R M₂] →
                                [inst_16 : Module S M] →
                                  [inst_17 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
            f :
          (a : M) → Mₛ)
        (m, s).1 :
      Mₛ)

Tactic:
mem_map_of_mem mem_top

Premises used: Set.Mem, Submodule.mem_map_of_mem, Submodule.mem_top
-- Module: Mathlib.RingTheory.Localization.Module
Goal:
R : Type u_1
Rₛ : Type u_2
inst : CommSemiring R
S : Submonoid R
inst_1 : CommSemiring Rₛ
inst_2 : Algebra R Rₛ
inst_3 : IsLocalization S Rₛ
M : Type u_3
Mₛ : Type u_4
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : AddCommMonoid Mₛ
inst_7 : Module R Mₛ
inst_8 : Module Rₛ Mₛ
inst_9 : IsScalarTower R Rₛ Mₛ
f : M →ₗ[R] Mₛ
inst_10 : IsLocalizedModule S f
v : Set M
hv : Eq (α := Submodule R M) (span R v) ⊤
x : Mₛ
h_1 : Membership.mem (γ := Submodule Rₛ Mₛ) ⊤ x
m : M
s : ↥S
h :
  HSMul.hSMul (α := Rₛˣ) (β := Mₛ) (IsUnit.unit (a := (algebraMap R Rₛ : (a : R) → Rₛ) (↑s : R)) ⋯)⁻¹
      ((f : (a : M) → Mₛ) (m, s).1 : Mₛ) =
    x
⊢ Membership.mem (α := Mₛ)
    (↑(map
          ((↑R :
              {S : Type u_1} →
                {M : Type u_3} →
                  {M₂ : Type u_4} →
                    [inst : Semiring R] →
                      [inst_11 : Semiring S] →
                        [inst_12 : AddCommMonoid M] →
                          [inst_13 : AddCommMonoid M₂] →
                            [inst_14 : Module R M] →
                              [inst_15 : Module R M₂] →
                                [inst_16 : Module S M] →
                                  [inst_17 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
            f)
          ⊤) :
      Set Mₛ)
    (((↑R :
              {S : Type u_1} →
                {M : Type u_3} →
                  {M₂ : Type u_4} →
                    [inst : Semiring R] →
                      [inst_11 : Semiring S] →
                        [inst_12 : AddCommMonoid M] →
                          [inst_13 : AddCommMonoid M₂] →
                            [inst_14 : Module R M] →
                              [inst_15 : Module R M₂] →
                                [inst_16 : Module S M] →
                                  [inst_17 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
            f :
          (a : M) → Mₛ)
        (m, s).1 :
      Mₛ)

Tactic:
exact mem_map_of_mem mem_top

Premises used: Submodule.mem_map_of_mem, Submodule.mem_top
-- Module: Mathlib.RingTheory.Localization.Module
Goal:
R : Type u_1
Rₛ : Type u_2
inst : CommSemiring R
S : Submonoid R
inst_1 : CommSemiring Rₛ
inst_2 : Algebra R Rₛ
inst_3 : IsLocalization S Rₛ
M : Type u_3
Mₛ : Type u_4
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : AddCommMonoid Mₛ
inst_7 : Module R Mₛ
inst_8 : Module Rₛ Mₛ
inst_9 : IsScalarTower R Rₛ Mₛ
f : M →ₗ[R] Mₛ
inst_10 : IsLocalizedModule S f
ι : Type u_5
v : ι → M
hv : LinearIndependent R v
rw :
  ∀
    (hv :
      ∀ (s : Finset ι) (f g : ι → R),
        Eq.{u_3 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i) → ∀ i ∈ s, f i = g i)
    (s : Finset ι) (f_1 g : ι → Rₛ),
    Eq.{u_4 + 1} (α := Mₛ) (∑ i ∈ s, HSMul.hSMul (β := Mₛ) (f_1 i) (((⇑f : (a : M) → Mₛ) ∘ v) i))
        (∑ i ∈ s, HSMul.hSMul (β := Mₛ) (g i) (((⇑f : (a : M) → Mₛ) ∘ v) i)) →
      ∀ i ∈ s, f_1 i = g i
⊢ LinearIndependent.{u_5, u_2, u_4} Rₛ (M := Mₛ) ((⇑f : (a : M) → Mₛ) ∘ v)

Tactic:
rw [linearIndependent_iff'ₛ] at hv ⊢

Premises used: linearIndependent_iff'ₛ
-- Module: Mathlib.RingTheory.Localization.Module
Goal:
R : Type u_1
Rₛ : Type u_2
inst : CommSemiring R
S : Submonoid R
inst_1 : CommSemiring Rₛ
inst_2 : Algebra R Rₛ
inst_3 : IsLocalization S Rₛ
M : Type u_3
Mₛ : Type u_4
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : AddCommMonoid Mₛ
inst_7 : Module R Mₛ
inst_8 : Module Rₛ Mₛ
inst_9 : IsScalarTower R Rₛ Mₛ
f : M →ₗ[R] Mₛ
inst_10 : IsLocalizedModule S f
ι : Type u_5
v : ι → M
hv :
  ∀ (s : Finset ι) (f g : ι → R), Eq.{u_3 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i) → ∀ i ∈ s, f i = g i
t : Finset ι
g₁ g₂ : ι → Rₛ
eq :
  Eq.{u_4 + 1} (α := Mₛ) (∑ i ∈ t, HSMul.hSMul (β := Mₛ) (g₁ i) (((⇑f : (a : M) → Mₛ) ∘ v) i))
    (∑ i ∈ t, HSMul.hSMul (β := Mₛ) (g₂ i) (((⇑f : (a : M) → Mₛ) ∘ v) i))
i : ι
hi : i ∈ t
choose! :
  ∀ (a : ↥S) (fg : (i : ι ⊕ ι) → R)
    (hfg : ∀ i ∈ t.disjSum t, (algebraMap R Rₛ : (a : R) → Rₛ) (fg i) = (↑a : R) • Sum.elim g₁ g₂ i), g₁ i = g₂ i
⊢ g₁ i = g₂ i

Tactic:
choose! a fg hfg using IsLocalization.exist_integer_multiples S (t.disjSum t) (Sum.elim g₁ g₂)

Premises used: Finset.disjSum, IsLocalization.exist_integer_multiples, Sum.elim
-- Module: Mathlib.RingTheory.Localization.Module
Goal:
R : Type u_1
Rₛ : Type u_2
inst : CommSemiring R
S : Submonoid R
inst_1 : CommSemiring Rₛ
inst_2 : Algebra R Rₛ
inst_3 : IsLocalization S Rₛ
M : Type u_3
Mₛ : Type u_4
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : AddCommMonoid Mₛ
inst_7 : Module R Mₛ
inst_8 : Module Rₛ Mₛ
inst_9 : IsScalarTower R Rₛ Mₛ
f : M →ₗ[R] Mₛ
inst_10 : IsLocalizedModule S f
ι : Type u_5
v : ι → M
hv :
  ∀ (s : Finset ι) (f g : ι → R), Eq.{u_3 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i) → ∀ i ∈ s, f i = g i
t : Finset ι
g₁ g₂ : ι → Rₛ
eq :
  Eq.{u_4 + 1} (α := Mₛ) (∑ i ∈ t, HSMul.hSMul (β := Mₛ) (g₁ i) (((⇑f : (a : M) → Mₛ) ∘ v) i))
    (∑ i ∈ t, HSMul.hSMul (β := Mₛ) (g₂ i) (((⇑f : (a : M) → Mₛ) ∘ v) i))
i : ι
hi : i ∈ t
a : ↥S
fg : (i : ι ⊕ ι) → R
hfg : ∀ i ∈ t.disjSum t, (algebraMap R Rₛ : (a : R) → Rₛ) (fg i) = (↑a : R) • Sum.elim g₁ g₂ i
⊢ (∀ (x : ↥t), (algebraMap R Rₛ : (a : R) → Rₛ) (fg (Sum.inl (↑x : ι))) = (↑a : R) • g₁ (↑x : ι)) ∧
    ∀ (x : ↥t), (algebraMap R Rₛ : (a : R) → Rₛ) (fg (Sum.inr (↑x : ι))) = (↑a : R) • g₂ (↑x : ι)

Tactic:
simp_rw [Sum.forall, Finset.inl_mem_disjSum, Sum.elim_inl, Finset.inr_mem_disjSum, Sum.elim_inr,
    Subtype.forall'] at hfg

Premises used: Finset.inr_mem_disjSum, Sum.elim_inr, Finset.inl_mem_disjSum, Sum.elim_inl, Sum.forall, Subtype.forall'
-- Module: Mathlib.RingTheory.Localization.Module
Goal:
R : Type u_1
Rₛ : Type u_2
inst : CommSemiring R
S : Submonoid R
inst_1 : CommSemiring Rₛ
inst_2 : Algebra R Rₛ
inst_3 : IsLocalization S Rₛ
M : Type u_3
Mₛ : Type u_4
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : AddCommMonoid Mₛ
inst_7 : Module R Mₛ
inst_8 : Module Rₛ Mₛ
inst_9 : IsScalarTower R Rₛ Mₛ
f : M →ₗ[R] Mₛ
inst_10 : IsLocalizedModule S f
ι : Type u_5
v : ι → M
hv :
  ∀ (s : Finset ι) (f g : ι → R), Eq.{u_3 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i) → ∀ i ∈ s, f i = g i
t : Finset ι
g₁ g₂ : ι → Rₛ
eq :
  Eq.{u_4 + 1} (α := Mₛ) (∑ i ∈ t, HSMul.hSMul (β := Mₛ) (g₁ i) (((⇑f : (a : M) → Mₛ) ∘ v) i))
    (∑ i ∈ t, HSMul.hSMul (β := Mₛ) (g₂ i) (((⇑f : (a : M) → Mₛ) ∘ v) i))
i : ι
hi : i ∈ t
a : ↥S
fg : (i : ι ⊕ ι) → R
hfg :
  (∀ (x : ↥t), (algebraMap R Rₛ : (a : R) → Rₛ) (fg (Sum.inl (↑x : ι))) = (↑a : R) • g₁ (↑x : ι)) ∧
    ∀ (x : ↥t), (algebraMap R Rₛ : (a : R) → Rₛ) (fg (Sum.inr (↑x : ι))) = (↑a : R) • g₂ (↑x : ι)
⊢ HSMul.hSMul (β := Mₛ) (↑a : R) (∑ i ∈ t, HSMul.hSMul (β := Mₛ) (g₁ i) (((⇑f : (a : M) → Mₛ) ∘ v) i)) =
    HSMul.hSMul (β := Mₛ) (↑a : R) (∑ i ∈ t, HSMul.hSMul (β := Mₛ) (g₂ i) (((⇑f : (a : M) → Mₛ) ∘ v) i))

Tactic:
apply_fun ((a : R) • ·) at eq

Premises used: HSMul.hSMul, Subtype.val
-- Module: Mathlib.RingTheory.Localization.Module
Goal:
R : Type u_1
Rₛ : Type u_2
inst : CommSemiring R
S : Submonoid R
inst_1 : CommSemiring Rₛ
inst_2 : Algebra R Rₛ
inst_3 : IsLocalization S Rₛ
M : Type u_3
Mₛ : Type u_4
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : AddCommMonoid Mₛ
inst_7 : Module R Mₛ
inst_8 : Module Rₛ Mₛ
inst_9 : IsScalarTower R Rₛ Mₛ
f : M →ₗ[R] Mₛ
inst_10 : IsLocalizedModule S f
ι : Type u_5
v : ι → M
hv :
  ∀ (s : Finset ι) (f g : ι → R), Eq.{u_3 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i) → ∀ i ∈ s, f i = g i
t : Finset ι
g₁ g₂ : ι → Rₛ
i : ι
hi : i ∈ t
a : ↥S
fg : (i : ι ⊕ ι) → R
hfg :
  (∀ (x : ↥t), (algebraMap R Rₛ : (a : R) → Rₛ) (fg (Sum.inl (↑x : ι))) = (↑a : R) • g₁ (↑x : ι)) ∧
    ∀ (x : ↥t), (algebraMap R Rₛ : (a : R) → Rₛ) (fg (Sum.inr (↑x : ι))) = (↑a : R) • g₂ (↑x : ι)
eq :
  HSMul.hSMul (β := Mₛ) (↑a : R) (∑ i ∈ t, HSMul.hSMul (β := Mₛ) (g₁ i) (((⇑f : (a : M) → Mₛ) ∘ v) i)) =
    HSMul.hSMul (β := Mₛ) (↑a : R) (∑ i ∈ t, HSMul.hSMul (β := Mₛ) (g₂ i) (((⇑f : (a : M) → Mₛ) ∘ v) i))
⊢ Eq.{u_4 + 1} (α := Mₛ) ((f : (a : M) → Mₛ) (∑ i ∈ t, fg (Sum.inl i) • v i) : Mₛ)
    ((f : (a : M) → Mₛ) (∑ i ∈ t, fg (Sum.inr i) • v i) : Mₛ)

Tactic:
simp_rw [← t.sum_coe_sort, Finset.smul_sum, ← smul_assoc, ← hfg,
    algebraMap_smul, Function.comp_def, ← map_smul, ← map_sum,
    t.sum_coe_sort (f := fun x ↦ fg (Sum.inl x) • v x),
    t.sum_coe_sort (f := fun x ↦ fg (Sum.inr x) • v x)] at eq

Premises used: smul_assoc, algebraMap_smul, Sum.inl, map_sum, Function.comp_def, Sum.inr, Finset.smul_sum, HSMul.hSMul, Finset.sum_coe_sort, map_smul
-- Module: Mathlib.RingTheory.Localization.Module
Goal:
R : Type u_1
Rₛ : Type u_2
inst : CommSemiring R
S : Submonoid R
inst_1 : CommSemiring Rₛ
inst_2 : Algebra R Rₛ
inst_3 : IsLocalization S Rₛ
M : Type u_3
Mₛ : Type u_4
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : AddCommMonoid Mₛ
inst_7 : Module R Mₛ
inst_8 : Module Rₛ Mₛ
inst_9 : IsScalarTower R Rₛ Mₛ
f : M →ₗ[R] Mₛ
inst_10 : IsLocalizedModule S f
ι : Type u_5
v : ι → M
hv :
  ∀ (s : Finset ι) (f g : ι → R), Eq.{u_3 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i) → ∀ i ∈ s, f i = g i
t : Finset ι
g₁ g₂ : ι → Rₛ
i : ι
hi : i ∈ t
a : ↥S
fg : (i : ι ⊕ ι) → R
hfg :
  (∀ (x : ↥t), (algebraMap R Rₛ : (a : R) → Rₛ) (fg (Sum.inl (↑x : ι))) = (↑a : R) • g₁ (↑x : ι)) ∧
    ∀ (x : ↥t), (algebraMap R Rₛ : (a : R) → Rₛ) (fg (Sum.inr (↑x : ι))) = (↑a : R) • g₂ (↑x : ι)
eq :
  Eq.{u_4 + 1} (α := Mₛ) ((f : (a : M) → Mₛ) (∑ i ∈ t, fg (Sum.inl i) • v i) : Mₛ)
    ((f : (a : M) → Mₛ) (∑ i ∈ t, fg (Sum.inr i) • v i) : Mₛ)
have :
  ∀ (s : ↥S)
    (eq :
      HSMul.hSMul (β := M) s (∑ i ∈ t, fg (Sum.inl i) • v i) = HSMul.hSMul (β := M) s (∑ i ∈ t, fg (Sum.inr i) • v i)),
    g₁ i = g₂ i
⊢ g₁ i = g₂ i

Tactic:
have ⟨s, eq⟩ := IsLocalizedModule.exists_of_eq (S := S) eq
-- Module: Mathlib.RingTheory.Localization.Module
Goal:
R : Type u_1
Rₛ : Type u_2
inst : CommSemiring R
S : Submonoid R
inst_1 : CommSemiring Rₛ
inst_2 : Algebra R Rₛ
inst_3 : IsLocalization S Rₛ
M : Type u_3
Mₛ : Type u_4
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : AddCommMonoid Mₛ
inst_7 : Module R Mₛ
inst_8 : Module Rₛ Mₛ
inst_9 : IsScalarTower R Rₛ Mₛ
f : M →ₗ[R] Mₛ
inst_10 : IsLocalizedModule S f
ι : Type u_5
v : ι → M
hv :
  ∀ (s : Finset ι) (f g : ι → R), Eq.{u_3 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i) → ∀ i ∈ s, f i = g i
t : Finset ι
g₁ g₂ : ι → Rₛ
i : ι
hi : i ∈ t
a : ↥S
fg : (i : ι ⊕ ι) → R
hfg :
  (∀ (x : ↥t), (algebraMap R Rₛ : (a : R) → Rₛ) (fg (Sum.inl (↑x : ι))) = (↑a : R) • g₁ (↑x : ι)) ∧
    ∀ (x : ↥t), (algebraMap R Rₛ : (a : R) → Rₛ) (fg (Sum.inr (↑x : ι))) = (↑a : R) • g₂ (↑x : ι)
eq_1 :
  Eq.{u_4 + 1} (α := Mₛ) ((f : (a : M) → Mₛ) (∑ i ∈ t, fg (Sum.inl i) • v i) : Mₛ)
    ((f : (a : M) → Mₛ) (∑ i ∈ t, fg (Sum.inr i) • v i) : Mₛ)
s : ↥S
eq : HSMul.hSMul (β := M) s (∑ i ∈ t, fg (Sum.inl i) • v i) = HSMul.hSMul (β := M) s (∑ i ∈ t, fg (Sum.inr i) • v i)
⊢ Eq.{u_3 + 1} (α := M) (∑ x ∈ t, ((↑s : R) * fg (Sum.inl x)) • v x) (∑ x ∈ t, ((↑s : R) * fg (Sum.inr x)) • v x)

Tactic:
simp_rw [Finset.smul_sum, Submonoid.smul_def, smul_smul] at eq

Premises used: smul_smul, Submonoid.smul_def, Finset.smul_sum
-- Module: Mathlib.RingTheory.Localization.Module
Goal:
R : Type u_1
Rₛ : Type u_2
inst : CommSemiring R
S : Submonoid R
inst_1 : CommSemiring Rₛ
inst_2 : Algebra R Rₛ
inst_3 : IsLocalization S Rₛ
M : Type u_3
Mₛ : Type u_4
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : AddCommMonoid Mₛ
inst_7 : Module R Mₛ
inst_8 : Module Rₛ Mₛ
inst_9 : IsScalarTower R Rₛ Mₛ
f : M →ₗ[R] Mₛ
inst_10 : IsLocalizedModule S f
ι : Type u_5
v : ι → M
hv :
  ∀ (s : Finset ι) (f g : ι → R), Eq.{u_3 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i) → ∀ i ∈ s, f i = g i
t : Finset ι
g₁ g₂ : ι → Rₛ
i : ι
hi : i ∈ t
a : ↥S
fg : (i : ι ⊕ ι) → R
hfg :
  (∀ (x : ↥t), (algebraMap R Rₛ : (a : R) → Rₛ) (fg (Sum.inl (↑x : ι))) = (↑a : R) • g₁ (↑x : ι)) ∧
    ∀ (x : ↥t), (algebraMap R Rₛ : (a : R) → Rₛ) (fg (Sum.inr (↑x : ι))) = (↑a : R) • g₂ (↑x : ι)
eq_1 :
  Eq.{u_4 + 1} (α := Mₛ) ((f : (a : M) → Mₛ) (∑ i ∈ t, fg (Sum.inl i) • v i) : Mₛ)
    ((f : (a : M) → Mₛ) (∑ i ∈ t, fg (Sum.inr i) • v i) : Mₛ)
s : ↥S
eq : Eq.{u_3 + 1} (α := M) (∑ x ∈ t, ((↑s : R) * fg (Sum.inl x)) • v x) (∑ x ∈ t, ((↑s : R) * fg (Sum.inr x)) • v x)
⊢ Eq.{u_2 + 1} (α := Rₛ) ((algebraMap R Rₛ : (a : R) → Rₛ) ((↑s : R) * fg (Sum.inl i)) : Rₛ)
    ((algebraMap R Rₛ : (a : R) → Rₛ) ((↑s : R) * fg (Sum.inr i)) : Rₛ)

Tactic:
have := congr(algebraMap R Rₛ $(hv t _ _ eq i hi))
-- Module: Mathlib.RingTheory.Localization.Module
Goal:
R : Type u_1
Rₛ : Type u_2
inst : CommSemiring R
S : Submonoid R
inst_1 : CommSemiring Rₛ
inst_2 : Algebra R Rₛ
inst_3 : IsLocalization S Rₛ
M : Type u_3
Mₛ : Type u_4
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : AddCommMonoid Mₛ
inst_7 : Module R Mₛ
inst_8 : Module Rₛ Mₛ
inst_9 : IsScalarTower R Rₛ Mₛ
f : M →ₗ[R] Mₛ
inst_10 : IsLocalizedModule S f
ι : Type u_5
v : ι → M
hv :
  ∀ (s : Finset ι) (f g : ι → R), Eq.{u_3 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i) → ∀ i ∈ s, f i = g i
t : Finset ι
g₁ g₂ : ι → Rₛ
i : ι
hi : i ∈ t
a : ↥S
fg : (i : ι ⊕ ι) → R
hfg :
  (∀ (x : ↥t), (algebraMap R Rₛ : (a : R) → Rₛ) (fg (Sum.inl (↑x : ι))) = (↑a : R) • g₁ (↑x : ι)) ∧
    ∀ (x : ↥t), (algebraMap R Rₛ : (a : R) → Rₛ) (fg (Sum.inr (↑x : ι))) = (↑a : R) • g₂ (↑x : ι)
eq_1 :
  Eq.{u_4 + 1} (α := Mₛ) ((f : (a : M) → Mₛ) (∑ i ∈ t, fg (Sum.inl i) • v i) : Mₛ)
    ((f : (a : M) → Mₛ) (∑ i ∈ t, fg (Sum.inr i) • v i) : Mₛ)
s : ↥S
eq : Eq.{u_3 + 1} (α := M) (∑ x ∈ t, ((↑s : R) * fg (Sum.inl x)) • v x) (∑ x ∈ t, ((↑s : R) * fg (Sum.inr x)) • v x)
this :
  Eq.{u_2 + 1} (α := Rₛ) ((algebraMap R Rₛ : (a : R) → Rₛ) ((↑s : R) * fg (Sum.inl i)) : Rₛ)
    ((algebraMap R Rₛ : (a : R) → Rₛ) ((↑s : R) * fg (Sum.inr i)) : Rₛ)
⊢ g₁ i = g₂ i

Tactic:
simpa only [map_mul, (IsLocalization.map_units Rₛ s).mul_right_inj, hfg.1 ⟨i, hi⟩, hfg.2 ⟨i, hi⟩,
    Algebra.smul_def, (IsLocalization.map_units Rₛ a).mul_right_inj] using this

Premises used: IsUnit.mul_right_inj, Subtype.mk, map_mul, And.right, And.left, IsLocalization.map_units, Algebra.smul_def
-- Module: Mathlib.RingTheory.Localization.Module
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_3
Mₛ : Type u_4
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid Mₛ
inst_4 : Module R Mₛ
f : M →ₗ[R] Mₛ
inst_5 : IsLocalizedModule S f
ι : Type u_5
v : ι → M
hv : LinearIndependent R v
h : ∀ (s : ↥S), IsRegular (↑s : R)
rw : Set.InjOn.{u_3, u_4} (β := Mₛ) (⇑f : (a : M) → Mₛ) (↑(LinearMap.range (Finsupp.linearCombination R v)) : Set M)
⊢ Set.InjOn.{u_3, u_4} (β := Mₛ) (⇑f : (a : M) → Mₛ) (↑(span R (Set.range v)) : Set M)

Tactic:
rw [← Finsupp.range_linearCombination]

Premises used: Finsupp.range_linearCombination