awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
v : Set M
hv : Eq (α := Submodule R M) (span R v) ⊤
x : Mₛ
h : Membership.mem (γ := Submodule Rₛ Mₛ) ⊤ x
⊢ Membership.mem (γ := Submodule Rₛ Mₛ) (span Rₛ ((⇑f : (a : M) → Mₛ) '' v)) x
have 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
Tactic: obtain ⟨⟨m, s⟩, h⟩ := IsLocalizedModule.surj S f x
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Module (hypothesis)
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
⊢ Membership.mem (γ := Submodule Rₛ Mₛ) (span Rₛ ((⇑f : (a : M) → Mₛ) '' v)) x
have h₁ : HSMul.hSMul (α := Rₛˣ) (β := Mₛ) (IsUnit.unit (a := (algebraMap R Rₛ : (a : R) → Rₛ) (↑s : R)) sorry)⁻¹
    ((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
Cleared hypotheses: h
-- 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
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
have refine : Membership.mem (α := Mₛ) (↑(span R ((⇑f : (a : M) → Mₛ) '' v)) : Set Mₛ) ((f : (a : M) → Mₛ) (m, s).1 : Mₛ)
Tactic: refine h ▸ smul_mem _ _ (span_subset_span R Rₛ _ ?_)
-- 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
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ₛ) (↑(span R ((⇑f : (a : M) → Mₛ) '' v)) : Set Mₛ) ((f : (a : M) → Mₛ) (m, s).1 : Mₛ)
have 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ₛ)
Tactic: rw [← LinearMap.coe_restrictScalars R, ← LinearMap.map_span, hv]
-- 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
v : ι → M
hv : LinearIndependent R v
⊢ LinearIndependent.{u_5, u_2, u_4} Rₛ (M := Mₛ) ((⇑f : (a : M) → Mₛ) ∘ v)
have 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
Tactic: rw [linearIndependent_iff'ₛ] at hv ⊢
Cleared hypotheses: hv
-- 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
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
⊢ g₁ i = g₂ i
have 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
Tactic: choose! a fg hfg using IsLocalization.exist_integer_multiples S (t.disjSum t) (Sum.elim g₁ g₂)
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Module (hypothesis)
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
⊢ g₁ i = g₂ i
have 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 : ι)
Tactic: simp_rw [Sum.forall, Finset.inl_mem_disjSum, Sum.elim_inl, Finset.inr_mem_disjSum, Sum.elim_inr,
    Subtype.forall'] at hfg
Cleared hypotheses: hfg
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Module (hypothesis)
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 : ι)
⊢ g₁ i = g₂ i
have 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))
Tactic: apply_fun ((a : R) • ·) at eq
Cleared hypotheses: eq
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Module (hypothesis)
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))
⊢ g₁ i = g₂ i
have 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ₛ)
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
Cleared hypotheses: 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
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ₛ)
⊢ g₁ i = g₂ i
have 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
Tactic: have ⟨s, eq⟩ := IsLocalizedModule.exists_of_eq (S := S) eq
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Module (hypothesis)
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)
⊢ g₁ i = g₂ i
have 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)
Tactic: simp_rw [Finset.smul_sum, Submonoid.smul_def, smul_smul] at eq
Cleared hypotheses: eq
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Module (hypothesis)
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)
⊢ g₁ i = g₂ i
have 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ₛ)
Tactic: have := congr(algebraMap R Rₛ $(hv t _ _ eq i hi))
-- 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
hv : LinearIndependent R v
h : ∀ (s : ↥S), IsRegular (↑s : R)
⊢ Set.InjOn.{u_3, u_4} (β := Mₛ) (⇑f : (a : M) → Mₛ) (↑(span R (Set.range v)) : Set M)
have rw : Set.InjOn.{u_3, u_4} (β := Mₛ) (⇑f : (a : M) → Mₛ) (↑(LinearMap.range (Finsupp.linearCombination R v)) : Set M)
Tactic: rw [← Finsupp.range_linearCombination]
-- 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
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ₛ)
⊢ Eq.{u_3 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) w : M)
    ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) w_1 : M)
have h₁ : w = w_1
Tactic: congr
-- 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
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ₛ)
⊢ w = w_1
have h₁ : ∀ (i : ι), Eq.{u_1 + 1} (α := R) ((w : (a : ι) → R) i : R) ((w_1 : (a : ι) → R) i : R)
Tactic: ext i
-- 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
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 : ι
⊢ Eq.{u_1 + 1} (α := R) ((w : (a : ι) → R) i : R) ((w_1 : (a : ι) → R) i : R)
have 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)
Tactic: have ⟨s, eq⟩ := IsLocalizedModule.exists_of_eq (S := S) eq
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Module (hypothesis)
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_1 + 1} (α := R) ((w : (a : ι) → R) i : R) ((w_1 : (a : ι) → R) i : R)
have 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)
Tactic: simp_rw [Submonoid.smul_def, ← map_smul] at eq
Cleared hypotheses: eq
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Module (hypothesis)
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
⊢ LinearIndependent Rₛ b
have this : IsLocalizedModule.{u_1, u_3, u_3} (M := M) S LinearMap.id
Tactic: have := isLocalizedModule_id S M Rₛ
-- 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
⊢ ∃ (w : ι → M), LinearIndependent R w
have inl : IsEmpty ι → ∃ (w : ι → M), LinearIndependent R w
Tactic: cases isEmpty_or_nonempty ι
-- 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
inl : IsEmpty ι → ∃ (w : ι → M), LinearIndependent R w
⊢ ∃ (w : ι → M), LinearIndependent R w
have inr : Nonempty ι → ∃ (w : ι → M), LinearIndependent R w
Tactic: cases isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Module (hypothesis)
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 ι
⊢ ∃ (w : ι → M), LinearIndependent R w
have inj : 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 ι)
-- 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 ι)
⊢ ∃ (w : ι → M), LinearIndependent R w
have 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
Tactic: choose sec hsec using surj S f
-- 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
⊢ ∃ (w : ι → M), LinearIndependent R w
have h : LinearIndependent.{u_5, u_1, u_3} R (M := M) fun (i : ι) ↦ (sec (v i)).1
Tactic: use fun i ↦ (sec (v i)).1