awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Module (goal)
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 ι)
sec : (y : Mₛ) → Prod.{u_3, u_1} M ↥S
hsec : ∀ (y : Mₛ), (sec y).2 • y = (f : (a : M) → Mₛ) (sec y).1
⊢ LinearIndependent.{u_5, u_1, u_3} R (M := M) fun (i : ι) ↦ (sec (v i)).1
have 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
Tactic: rw [linearIndependent_iff'ₛ] at hf ⊢
Cleared hypotheses: hf, h, inj, sec, hsec
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Module (goal)
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
have 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))
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
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Module (goal)
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)
⊢ 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))
have 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)
Tactic: simp_rw [mul_smul, ← Submonoid.smul_def, hsec, ← map_smul, ← map_sum, eq]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Module (goal)
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)
⊢ 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))
have 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)
Tactic: simp_rw [mul_smul, ← Submonoid.smul_def, hsec, ← map_smul, ← map_sum, eq]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Module (goal)
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)
⊢ 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))
have 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ₛ))
Tactic: simp_rw [mul_smul, ← Submonoid.smul_def, hsec, ← map_smul, ← map_sum, eq]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Module (goal)
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ₛ))
⊢ 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))
have 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))
Tactic: simp_rw [mul_smul, ← Submonoid.smul_def, hsec, ← map_smul, ← map_sum, eq]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Module (goal)
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))
⊢ 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))
have 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ₛ)
Tactic: simp_rw [mul_smul, ← Submonoid.smul_def, hsec, ← map_smul, ← map_sum, eq]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Module (goal)
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
⊢ 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))))
have 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))))
Tactic: rw [Set.range_comp, span_eq_top_of_isLocalizedModule Rₛ S _ b.span_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Module (goal)
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))))
⊢ 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))))
have rw₁ : LE.le.{u_4} (α := Submodule Rₛ Mₛ) ⊤ ⊤
Tactic: rw [Set.range_comp, span_eq_top_of_isLocalizedModule Rₛ S _ b.span_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Module (goal)
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 : ι
⊢ Eq.{u_4 + 1} (α := Mₛ) ((ofIsLocalizedModule Rₛ S f b : (a : ι) → Mₛ) i : Mₛ)
    ((f : (a : M) → Mₛ) ((b : (a : ι) → M) i : M) : Mₛ)
have rw : Eq.{u_4 + 1} (α := Mₛ) ((Basis.mk sorry sorry : (a : ι) → Mₛ) i : Mₛ) ((f : (a : M) → Mₛ) ((b : (a : ι) → M) i : M) : Mₛ)
Tactic: rw [ofIsLocalizedModule, coe_mk, Function.comp_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Module (goal)
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ₛ)
⊢ Eq.{u_4 + 1} (α := Mₛ) ((ofIsLocalizedModule Rₛ S f b : (a : ι) → Mₛ) i : Mₛ)
    ((f : (a : M) → Mₛ) ((b : (a : ι) → M) i : M) : Mₛ)
have 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ₛ)
Tactic: rw [ofIsLocalizedModule, coe_mk, Function.comp_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Module (goal)
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ₛ)
⊢ Eq.{u_4 + 1} (α := Mₛ) ((ofIsLocalizedModule Rₛ S f b : (a : ι) → Mₛ) i : Mₛ)
    ((f : (a : M) → Mₛ) ((b : (a : ι) → M) i : M) : Mₛ)
have 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ₛ)
Tactic: rw [ofIsLocalizedModule, coe_mk, Function.comp_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Module (goal)
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 : ι
⊢ 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ₛ)
have 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))
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
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Module (goal)
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 : ι
⊢ 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))
have refine : ∀ (i : ι),
  Eq (α := ι →₀ 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 :
          (a : M) → ι →₀ Rₛ)
        ((b : (a : ι) → M) i) :
      ι →₀ Rₛ)
    ((Finsupp.mapRange.linearMap (Algebra.linearMap R Rₛ) ∘ₗ (↑b.repr : M →ₗ[R] ι →₀ R) : (a : M) → ι →₀ Rₛ)
        ((b : (a : ι) → M) i) :
      ι →₀ Rₛ)
Tactic: refine ext b fun i ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Module (goal)
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_1 i : ι
⊢ Eq (α := ι →₀ 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 :
          (a : M) → ι →₀ Rₛ)
        ((b : (a : ι) → M) i) :
      ι →₀ Rₛ)
    ((Finsupp.mapRange.linearMap (Algebra.linearMap R Rₛ) ∘ₗ (↑b.repr : M →ₗ[R] ι →₀ R) : (a : M) → ι →₀ Rₛ)
        ((b : (a : ι) → M) i) :
      ι →₀ Rₛ)
have rw : Eq (α := ι →₀ Rₛ)
  (Function.comp (α := M) (β := Mₛ)
      (⇑((↑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ₛ)) :
        (a : Mₛ) → ι →₀ Rₛ)
      ((⇑f : (a : M) → Mₛ) : (a : M) → Mₛ) ((b : (a : ι) → M) i : M) :
    ι →₀ Rₛ)
  ((Finsupp.mapRange.linearMap (Algebra.linearMap R Rₛ) ∘ₗ (↑b.repr : M →ₗ[R] ι →₀ R) : (a : M) → ι →₀ Rₛ)
      ((b : (a : ι) → M) i) :
    ι →₀ Rₛ)
Tactic: rw [LinearMap.coe_comp, Function.comp_apply, LinearMap.coe_restrictScalars,
    LinearEquiv.coe_coe, ← b.ofIsLocalizedModule_apply Rₛ S f, repr_self, LinearMap.coe_comp,
    Function.comp_apply, LinearEquiv.coe_coe, repr_self, Finsupp.mapRange.linearMap_apply,
    Finsupp.mapRange_single, Algebra.linearMap_apply, map_one]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Module (goal)
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
⊢ Eq.{u_4 + 1} (α := Submodule R Mₛ)
    (span R (Set.range.{u_4, u_5 + 1} (ι := ι) (⇑(ofIsLocalizedModule Rₛ S f b) : (a : ι) → Mₛ)))
    (span R (Set.image.{u_3, u_4} (α := M) (⇑f : (a : M) → Mₛ) (Set.range.{u_3, u_5 + 1} (ι := ι) (⇑b : (a : ι) → M))))
have e_s : Eq.{u_4 + 1} (α := Set Mₛ) (Set.range.{u_4, u_5 + 1} (ι := ι) (⇑(ofIsLocalizedModule Rₛ S f b) : (a : ι) → Mₛ))
  (Set.image.{u_3, u_4} (α := M) (⇑f : (a : M) → Mₛ) (Set.range.{u_3, u_5 + 1} (ι := ι) (⇑b : (a : ι) → M)))
Tactic: congr
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Module (goal)
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
⊢ Eq.{u_4 + 1} (α := Set Mₛ) (Set.range.{u_4, u_5 + 1} (ι := ι) (⇑(ofIsLocalizedModule Rₛ S f b) : (a : ι) → Mₛ))
    (Set.image.{u_3, u_4} (α := M) (⇑f : (a : M) → Mₛ) (Set.range.{u_3, u_5 + 1} (ι := ι) (⇑b : (a : ι) → M)))
have e_s : ∀ (x : Mₛ),
  Membership.mem (γ := Set Mₛ) (Set.range.{u_4, u_5 + 1} (ι := ι) (⇑(ofIsLocalizedModule Rₛ S f b) : (a : ι) → Mₛ)) x ↔
    Membership.mem (γ := Set Mₛ)
      (Set.image.{u_3, u_4} (α := M) (⇑f : (a : M) → Mₛ) (Set.range.{u_3, u_5 + 1} (ι := ι) (⇑b : (a : ι) → M))) x
Tactic: ext