awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
w w_1 : ι →₀ R
eq :
  Eq.{u_4 + 1} (α := Mₛ) ((f : (a : M) → Mₛ) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) w : M) : Mₛ)
    ((f : (a : M) → Mₛ) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) w_1 : M) : Mₛ)
h₁ : w = w_1
⊢ Eq.{u_3 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) w : M)
    ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) w_1 : M)

Tactic:
congr
-- 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)
w w_1 : ι →₀ R
eq :
  Eq.{u_4 + 1} (α := Mₛ) ((f : (a : M) → Mₛ) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) w : M) : Mₛ)
    ((f : (a : M) → Mₛ) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) w_1 : M) : Mₛ)
h₁ : ∀ (i : ι), Eq.{u_1 + 1} (α := R) ((w : (a : ι) → R) i : R) ((w_1 : (a : ι) → R) i : R)
⊢ w = w_1

Tactic:
ext i
-- 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)
w w_1 : ι →₀ R
eq :
  Eq.{u_4 + 1} (α := Mₛ) ((f : (a : M) → Mₛ) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) w : M) : Mₛ)
    ((f : (a : M) → Mₛ) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) w_1 : M) : Mₛ)
i : ι
h₁ :
  ∀ (s : ↥S)
    (eq :
      HSMul.hSMul (β := M) s ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) w : M) =
        HSMul.hSMul (β := M) s ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) w_1 : M)),
    Eq.{u_1 + 1} (α := R) ((w : (a : ι) → R) i : R) ((w_1 : (a : ι) → R) i : R)
⊢ Eq.{u_1 + 1} (α := R) ((w : (a : ι) → R) i : R) ((w_1 : (a : ι) → R) i : R)

Tactic:
have ⟨s, eq⟩ := IsLocalizedModule.exists_of_eq (S := S) eq
-- 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)
w w_1 : ι →₀ R
eq_1 :
  Eq.{u_4 + 1} (α := Mₛ) ((f : (a : M) → Mₛ) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) w : M) : Mₛ)
    ((f : (a : M) → Mₛ) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) w_1 : M) : Mₛ)
i : ι
s : ↥S
eq :
  HSMul.hSMul (β := M) s ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) w : M) =
    HSMul.hSMul (β := M) s ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) w_1 : M)
⊢ Eq.{u_3 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) ((↑s : R) • w) : M)
    ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) ((↑s : R) • w_1) : M)

Tactic:
simp_rw [Submonoid.smul_def, ← map_smul] at eq

Premises used: Submonoid.smul_def, map_smul
-- 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)
w w_1 : ι →₀ R
eq_1 :
  Eq.{u_4 + 1} (α := Mₛ) ((f : (a : M) → Mₛ) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) w : M) : Mₛ)
    ((f : (a : M) → Mₛ) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) w_1 : M) : Mₛ)
i : ι
s : ↥S
eq :
  Eq.{u_3 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) ((↑s : R) • w) : M)
    ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) ((↑s : R) • w_1) : M)
⊢ Eq.{u_1 + 1} (α := R) ((w : (a : ι) → R) i : R) ((w_1 : (a : ι) → R) i : R)

Tactic:
(h s).1 (DFunLike.congr_fun (hv eq) i)

Premises used: DFunLike.congr_fun, IsRegular.left
-- 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)
w w_1 : ι →₀ R
eq_1 :
  Eq.{u_4 + 1} (α := Mₛ) ((f : (a : M) → Mₛ) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) w : M) : Mₛ)
    ((f : (a : M) → Mₛ) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) w_1 : M) : Mₛ)
i : ι
s : ↥S
eq :
  Eq.{u_3 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) ((↑s : R) • w) : M)
    ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) ((↑s : R) • w_1) : M)
⊢ Eq.{u_1 + 1} (α := R) ((w : (a : ι) → R) i : R) ((w_1 : (a : ι) → R) i : R)

Tactic:
exact (h s).1 (DFunLike.congr_fun (hv eq) i)

Premises used: DFunLike.congr_fun, IsRegular.left
-- 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
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : Module Rₛ M
inst_7 : IsScalarTower R Rₛ M
ι : Type u_5
b : ι → M
hli : LinearIndependent R b
⊢ IsLocalizedModule.{u_1, u_3, u_3} (M := M) S LinearMap.id

Tactic:
have := isLocalizedModule_id S M 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
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : Module Rₛ M
inst_7 : IsScalarTower R Rₛ M
ι : Type u_5
b : ι → M
hli : LinearIndependent R b
this : IsLocalizedModule.{u_1, u_3, u_3} (M := M) S LinearMap.id
⊢ LinearIndependent Rₛ b

Tactic:
hli.of_isLocalizedModule Rₛ S .id

Premises used: LinearMap.id, LinearIndependent.of_isLocalizedModule
-- 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
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : Module Rₛ M
inst_7 : IsScalarTower R Rₛ M
ι : Type u_5
b : ι → M
hli : LinearIndependent R b
this : IsLocalizedModule.{u_1, u_3, u_3} (M := M) S LinearMap.id
⊢ LinearIndependent Rₛ b

Tactic:
exact hli.of_isLocalizedModule Rₛ S .id

Premises used: LinearMap.id, LinearIndependent.of_isLocalizedModule
-- 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ₛ
hf : LinearIndependent R v
inl : IsEmpty ι → ∃ (w : ι → M), LinearIndependent R w
inr : Nonempty ι → ∃ (w : ι → M), LinearIndependent R w
⊢ ∃ (w : ι → M), LinearIndependent R w

Tactic:
cases isEmpty_or_nonempty ι

Premises used: isEmpty_or_nonempty
-- 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ₛ
hf : LinearIndependent R v
h : IsEmpty ι
⊢ ∃ (w : ι → M), LinearIndependent R w

Tactic:
⟨isEmptyElim, linearIndependent_empty_type⟩

Premises used: isEmptyElim, linearIndependent_empty_type, Exists.intro
-- 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ₛ
hf : LinearIndependent R v
h : IsEmpty ι
⊢ ∃ (w : ι → M), LinearIndependent R w

Tactic:
exact ⟨isEmptyElim, linearIndependent_empty_type⟩
-- 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ₛ
hf : LinearIndependent R v
h : Nonempty ι
⊢ Function.Injective.{u_1 + 1, u_4 + 1} (β := Mₛ) fun (r : R) ↦ r • v (Classical.arbitrary ι)

Tactic:
have inj := hf.smul_left_injective (Classical.arbitrary ι)
-- 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ₛ
hf : LinearIndependent R v
h : Nonempty ι
inj : Function.Injective.{u_1 + 1, u_4 + 1} (β := Mₛ) fun (r : R) ↦ r • v (Classical.arbitrary ι)
inr :
  ∀ (sec : (y : Mₛ) → Prod.{u_3, u_1} M ↥S) (hsec : ∀ (y : Mₛ), (sec y).2 • y = (f : (a : M) → Mₛ) (sec y).1),
    ∃ (w : ι → M), LinearIndependent R w
⊢ ∃ (w : ι → M), LinearIndependent R w

Tactic:
choose sec hsec using surj S f

Premises used: IsLocalizedModule.surj
-- 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ₛ
hf : LinearIndependent R v
h_1 : Nonempty ι
inj : Function.Injective.{u_1 + 1, u_4 + 1} (β := Mₛ) fun (r : R) ↦ r • v (Classical.arbitrary ι)
sec : (y : Mₛ) → Prod.{u_3, u_1} M ↥S
hsec : ∀ (y : Mₛ), (sec y).2 • y = (f : (a : M) → Mₛ) (sec y).1
h : LinearIndependent.{u_5, u_1, u_3} R (M := M) fun (i : ι) ↦ (sec (v i)).1
⊢ ∃ (w : ι → M), LinearIndependent R w

Tactic:
use fun i ↦ (sec (v i)).1

Premises used: Prod.fst
-- 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ₛ
hf : LinearIndependent R v
h_1 : Nonempty ι
inj : Function.Injective.{u_1 + 1, u_4 + 1} (β := Mₛ) fun (r : R) ↦ r • v (Classical.arbitrary ι)
sec : (y : Mₛ) → Prod.{u_3, u_1} M ↥S
hsec : ∀ (y : Mₛ), (sec y).2 • y = (f : (a : M) → Mₛ) (sec y).1
h :
  ∀
    (hf :
      ∀ (s : Finset ι) (f g : ι → R),
        Eq.{u_4 + 1} (α := Mₛ) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i) → ∀ i ∈ s, f i = g i)
    (h : Nonempty ι) (inj : Function.Injective.{u_1 + 1, u_4 + 1} (β := Mₛ) fun (r : R) ↦ r • v (Classical.arbitrary ι))
    (sec : (y : Mₛ) → Prod.{u_3, u_1} M ↥S) (hsec : ∀ (y : Mₛ), (sec y).2 • y = (f : (a : M) → Mₛ) (sec y).1)
    (s : Finset ι) (f g : ι → R),
    Eq.{u_3 + 1} (α := M) (∑ i ∈ s, f i • (sec (v i)).1) (∑ i ∈ s, g i • (sec (v i)).1) → ∀ i ∈ s, f i = g i
⊢ LinearIndependent.{u_5, u_1, u_3} R (M := M) fun (i : ι) ↦ (sec (v i)).1

Tactic:
rw [linearIndependent_iff'ₛ] at hf ⊢

Premises used: linearIndependent_iff'ₛ
-- 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ₛ
hf :
  ∀ (s : Finset ι) (f g : ι → R), Eq.{u_4 + 1} (α := Mₛ) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i) → ∀ i ∈ s, f i = g i
h : Nonempty ι
inj : Function.Injective.{u_1 + 1, u_4 + 1} (β := Mₛ) fun (r : R) ↦ r • v (Classical.arbitrary ι)
sec : (y : Mₛ) → Prod.{u_3, u_1} M ↥S
hsec : ∀ (y : Mₛ), (sec y).2 • y = (f : (a : M) → Mₛ) (sec y).1
t : Finset ι
g g' : ι → R
eq : Eq.{u_3 + 1} (α := M) (∑ i ∈ t, g i • (sec (v i)).1) (∑ i ∈ t, g' i • (sec (v i)).1)
i : ι
hit : i ∈ t
⊢ g i = g' i

Tactic:
(isRegular_of_smul_left_injective f inj (sec (v i)).2).2 <|
    hf t (fun i ↦ _ * (sec (v i)).2) (fun i ↦ _ * (sec (v i)).2) ?_ i hit

Premises used: HMul.hMul, IsRegular.right, IsLocalizedModule.isRegular_of_smul_left_injective, Subtype.val, Prod.snd
-- 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ₛ
hf :
  ∀ (s : Finset ι) (f g : ι → R), Eq.{u_4 + 1} (α := Mₛ) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i) → ∀ i ∈ s, f i = g i
h_1 : Nonempty ι
inj : Function.Injective.{u_1 + 1, u_4 + 1} (β := Mₛ) fun (r : R) ↦ r • v (Classical.arbitrary ι)
sec : (y : Mₛ) → Prod.{u_3, u_1} M ↥S
hsec : ∀ (y : Mₛ), (sec y).2 • y = (f : (a : M) → Mₛ) (sec y).1
t : Finset ι
g g' : ι → R
eq : Eq.{u_3 + 1} (α := M) (∑ i ∈ t, g i • (sec (v i)).1) (∑ i ∈ t, g' i • (sec (v i)).1)
i : ι
hit : i ∈ t
h :
  Eq.{u_4 + 1} (α := Mₛ)
    (∑ i ∈ t, HSMul.hSMul.{u_1, u_4, u_4} (α := R) ((fun (i : ι) ↦ g i * (↑(sec (v i)).2 : R)) i) (v i))
    (∑ i ∈ t, HSMul.hSMul.{u_1, u_4, u_4} (α := R) ((fun (i : ι) ↦ g' i * (↑(sec (v i)).2 : R)) i) (v i))
⊢ g i = g' i

Tactic:
refine (isRegular_of_smul_left_injective f inj (sec (v i)).2).2 <|
    hf t (fun i ↦ _ * (sec (v i)).2) (fun i ↦ _ * (sec (v i)).2) ?_ i hit

Premises used: HMul.hMul, IsRegular.right, IsLocalizedModule.isRegular_of_smul_left_injective, Subtype.val, Prod.snd
-- 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ₛ
hf :
  ∀ (s : Finset ι) (f g : ι → R), Eq.{u_4 + 1} (α := Mₛ) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i) → ∀ i ∈ s, f i = g i
h_1 : Nonempty ι
inj : Function.Injective.{u_1 + 1, u_4 + 1} (β := Mₛ) fun (r : R) ↦ r • v (Classical.arbitrary ι)
sec : (y : Mₛ) → Prod.{u_3, u_1} M ↥S
hsec : ∀ (y : Mₛ), (sec y).2 • y = (f : (a : M) → Mₛ) (sec y).1
t : Finset ι
g g' : ι → R
eq : Eq.{u_3 + 1} (α := M) (∑ i ∈ t, g i • (sec (v i)).1) (∑ i ∈ t, g' i • (sec (v i)).1)
i : ι
hit : i ∈ t
h h₁ :
  Eq.{u_4 + 1} (α := Mₛ) (∑ x ∈ t, (g x * (↑(sec (v x)).2 : R)) • v x) (∑ x ∈ t, (g' x * (↑(sec (v x)).2 : R)) • v x)
h₂ : Eq.{u_4 + 1} (α := Mₛ) (∑ x ∈ t, g x • (↑(sec (v x)).2 : R) • v x) (∑ x ∈ t, g' x • (↑(sec (v x)).2 : R) • v x)
h₃ : Eq.{u_4 + 1} (α := Mₛ) (∑ x ∈ t, g x • (sec (v x)).2 • v x) (∑ x ∈ t, g' x • (sec (v x)).2 • v x)
h₄ :
  Eq.{u_4 + 1} (α := Mₛ) (∑ x ∈ t, HSMul.hSMul (β := Mₛ) (g x) ((f : (a : M) → Mₛ) (sec (v x)).1 : Mₛ))
    (∑ x ∈ t, HSMul.hSMul (β := Mₛ) (g' x) ((f : (a : M) → Mₛ) (sec (v x)).1 : Mₛ))
h₅ :
  Eq.{u_4 + 1} (α := Mₛ) (∑ x ∈ t, (f : (a : M) → Mₛ) (g x • (sec (v x)).1))
    (∑ x ∈ t, (f : (a : M) → Mₛ) (g' x • (sec (v x)).1))
h₆ :
  Eq.{u_4 + 1} (α := Mₛ) ((f : (a : M) → Mₛ) (∑ x ∈ t, g x • (sec (v x)).1) : Mₛ)
    ((f : (a : M) → Mₛ) (∑ x ∈ t, g' x • (sec (v x)).1) : Mₛ)
⊢ Eq.{u_4 + 1} (α := Mₛ)
    (∑ i ∈ t, HSMul.hSMul.{u_1, u_4, u_4} (α := R) ((fun (i : ι) ↦ g i * (↑(sec (v i)).2 : R)) i) (v i))
    (∑ i ∈ t, HSMul.hSMul.{u_1, u_4, u_4} (α := R) ((fun (i : ι) ↦ g' i * (↑(sec (v i)).2 : R)) i) (v i))

Tactic:
simp_rw [mul_smul, ← Submonoid.smul_def, hsec, ← map_smul, ← map_sum, eq]

Premises used: map_sum, Submonoid.smul_def, SemigroupAction.mul_smul, 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
b : Basis ι R M
rw :
  LE.le.{u_4} (α := Submodule Rₛ Mₛ) ⊤
    (span Rₛ (Set.image.{u_3, u_4} (α := M) (⇑f : (a : M) → Mₛ) (Set.range.{u_3, u_5 + 1} (ι := ι) (⇑b : (a : ι) → M))))
rw₁ rw₂ : LE.le.{u_4} (α := Submodule Rₛ Mₛ) ⊤ ⊤
⊢ LE.le.{u_4} (α := Submodule Rₛ Mₛ) ⊤
    (span Rₛ
      (Set.range.{u_4, u_5 + 1} (ι := ι)
        (Function.comp.{u_5 + 1, u_3 + 1, u_4 + 1} (β := M) (⇑f : (a : M) → Mₛ) (⇑b : (a : ι) → M))))

Tactic:
rw [Set.range_comp, span_eq_top_of_isLocalizedModule Rₛ S _ b.span_eq]

Premises used: Set.range_comp, span_eq_top_of_isLocalizedModule, Module.Basis.span_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
b : Basis ι R M
i : ι
rw : Eq.{u_4 + 1} (α := Mₛ) ((Basis.mk ⋯ ⋯ : (a : ι) → Mₛ) i : Mₛ) ((f : (a : M) → Mₛ) ((b : (a : ι) → M) i : M) : Mₛ)
rw₁ :
  Eq.{u_4 + 1} (α := Mₛ)
    (Function.comp.{u_5 + 1, u_3 + 1, u_4 + 1} (β := M) (⇑f : (a : M) → Mₛ) (⇑b : (a : ι) → M) i : Mₛ)
    ((f : (a : M) → Mₛ) ((b : (a : ι) → M) i : M) : Mₛ)
rw₂ rw₃ :
  Eq.{u_4 + 1} (α := Mₛ) ((f : (a : M) → Mₛ) ((b : (a : ι) → M) i : M) : Mₛ)
    ((f : (a : M) → Mₛ) ((b : (a : ι) → M) i : M) : Mₛ)
⊢ Eq.{u_4 + 1} (α := Mₛ) ((ofIsLocalizedModule Rₛ S f b : (a : ι) → Mₛ) i : Mₛ)
    ((f : (a : M) → Mₛ) ((b : (a : ι) → M) i : M) : Mₛ)

Tactic:
rw [ofIsLocalizedModule, coe_mk, Function.comp_apply]

Premises used: Module.Basis.coe_mk, Function.comp_apply, Module.Basis.ofIsLocalizedModule
-- 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
b : Basis ι R M
m : M
i : ι
this :
  Eq (α := M →ₗ[R] ι →₀ Rₛ)
    ((↑R :
          {S : Type u_2} →
            {M : Type u_4} →
              {M₂ : Type (max u_2 u_5)} →
                [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₂)
        (↑(repr (ofIsLocalizedModule Rₛ S f b)) : Mₛ →ₗ[Rₛ] ι →₀ Rₛ) ∘ₗ
      f)
    (Finsupp.mapRange.linearMap (Algebra.linearMap R Rₛ) ∘ₗ (↑b.repr : M →ₗ[R] ι →₀ R))
⊢ Eq.{u_2 + 1} (α := Rₛ)
    ((((repr (ofIsLocalizedModule Rₛ S f b) : (a : Mₛ) → ι →₀ Rₛ) ((f : (a : M) → Mₛ) m) : ι →₀ Rₛ) : (a : ι) → Rₛ) i :
      Rₛ)
    ((algebraMap R Rₛ : (a : R) → Rₛ) ((((b.repr : (a : M) → ι →₀ R) m : ι →₀ R) : (a : ι) → R) i : R) : Rₛ)

Tactic:
DFunLike.congr_fun (LinearMap.congr_fun this m) i

Premises used: DFunLike.congr_fun, LinearMap.congr_fun
-- 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
b : Basis ι R M
m : M
i : ι
this :
  Eq (α := M →ₗ[R] ι →₀ Rₛ)
    ((↑R :
          {S : Type u_2} →
            {M : Type u_4} →
              {M₂ : Type (max u_2 u_5)} →
                [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₂)
        (↑(repr (ofIsLocalizedModule Rₛ S f b)) : Mₛ →ₗ[Rₛ] ι →₀ Rₛ) ∘ₗ
      f)
    (Finsupp.mapRange.linearMap (Algebra.linearMap R Rₛ) ∘ₗ (↑b.repr : M →ₗ[R] ι →₀ R))
⊢ Eq.{u_2 + 1} (α := Rₛ)
    ((((repr (ofIsLocalizedModule Rₛ S f b) : (a : Mₛ) → ι →₀ Rₛ) ((f : (a : M) → Mₛ) m) : ι →₀ Rₛ) : (a : ι) → Rₛ) i :
      Rₛ)
    ((algebraMap R Rₛ : (a : R) → Rₛ) ((((b.repr : (a : M) → ι →₀ R) m : ι →₀ R) : (a : ι) → R) i : R) : Rₛ)

Tactic:
exact DFunLike.congr_fun (LinearMap.congr_fun this m) i

Premises used: DFunLike.congr_fun, LinearMap.congr_fun
-- 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
b : Basis ι R M
m : M
i : ι
suffices :
  Eq (α := M →ₗ[R] ι →₀ Rₛ)
    ((↑R :
          {S : Type u_2} →
            {M : Type u_4} →
              {M₂ : Type (max u_2 u_5)} →
                [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₂)
        (↑(repr (ofIsLocalizedModule Rₛ S f b)) : Mₛ →ₗ[Rₛ] ι →₀ Rₛ) ∘ₗ
      f)
    (Finsupp.mapRange.linearMap (Algebra.linearMap R Rₛ) ∘ₗ (↑b.repr : M →ₗ[R] ι →₀ R))
⊢ Eq.{u_2 + 1} (α := Rₛ)
    ((((repr (ofIsLocalizedModule Rₛ S f b) : (a : Mₛ) → ι →₀ Rₛ) ((f : (a : M) → Mₛ) m) : ι →₀ Rₛ) : (a : ι) → Rₛ) i :
      Rₛ)
    ((algebraMap R Rₛ : (a : R) → Rₛ) ((((b.repr : (a : M) → ι →₀ R) m : ι →₀ R) : (a : ι) → R) i : R) : Rₛ)

Tactic:
suffices ((b.ofIsLocalizedModule Rₛ S f).repr.toLinearMap.restrictScalars R) ∘ₗ f =
      Finsupp.mapRange.linearMap (Algebra.linearMap R Rₛ) ∘ₗ b.repr.toLinearMap by
    exact DFunLike.congr_fun (LinearMap.congr_fun this m) i