awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.LocalRing.Module
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsLocalRing R
inst_4 : FinitePresentation R M
ι : Type u_5
v : ι → M
hli :
  LinearIndependent k (M := k ⊗[R] M)
    ((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v)
hsp :
  Eq (α := Submodule k (k ⊗[R] M))
    (Submodule.span k
      (Set.range ((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v)))
    ⊤
H :
  Function.Injective (α := ↥𝔪 ⊗[R] M) (β := R ⊗[R] M)
    (⇑(LinearMap.rTensor M (Submodule.subtype 𝔪)) : (a : ↥𝔪 ⊗[R] M) → R ⊗[R] M)
bk : Basis ι k (k ⊗[R] M) := Basis.mk hli ⋯
this_1 : Finite ι
this_2 : Fintype ι := Fintype.ofFinite ι
i : (ι →₀ R) →ₗ[R] M := Finsupp.linearCombination R v
hi : Surjective (α := ι →₀ R) (β := M) (⇑i : (a : ι →₀ R) → M)
this_3 : Module.Finite R ↥i.ker
this :
  Surjective (α := k ⊗[R] (ι →₀ R)) (β := k ⊗[R] M) (⇑(LinearMap.baseChange k i) : (a : k ⊗[R] (ι →₀ R)) → k ⊗[R] M)
hi' :
  Function.Bijective (α := k ⊗[R] (ι →₀ R)) (β := k ⊗[R] M)
    (⇑(LinearMap.baseChange k i) : (a : k ⊗[R] (ι →₀ R)) → k ⊗[R] M)
x : k ⊗[R] ↥i.ker
refine_2 :
  Eq (α := k ⊗[R] M) ((LinearMap.lTensor k 0 : (a : (R ⧸ 𝔪) ⊗[R] ↥i.ker) → k ⊗[R] M) x : k ⊗[R] M)
    ((LinearMap.lTensor k i : (a : k ⊗[R] (ι →₀ R)) → k ⊗[R] M)
        ((LinearMap.lTensor (HasQuotient.Quotient R (B := Submodule R R) (𝔪 : Ideal R)) i.ker.subtype :
            (a : (R ⧸ 𝔪) ⊗[R] ↥i.ker) → (R ⧸ 𝔪) ⊗[R] (ι →₀ R))
          0) :
      k ⊗[R] M)
⊢ Eq (α := k ⊗[R] M) ((LinearMap.lTensor k (i ∘ₗ i.ker.subtype) : (a : (R ⧸ 𝔪) ⊗[R] ↥i.ker) → k ⊗[R] M) x : k ⊗[R] M)
    ((LinearMap.lTensor k i : (a : k ⊗[R] (ι →₀ R)) → k ⊗[R] M)
        ((LinearMap.lTensor (HasQuotient.Quotient R (B := Submodule R R) (𝔪 : Ideal R)) i.ker.subtype :
            (a : (R ⧸ 𝔪) ⊗[R] ↥i.ker) → (R ⧸ 𝔪) ⊗[R] (ι →₀ R))
          0) :
      k ⊗[R] M)

Tactic:
rw [(LinearMap.exact_subtype_ker_map i).linearMap_comp_eq_zero]

Premises used: Function.Exact.linearMap_comp_eq_zero, LinearMap.exact_subtype_ker_map
-- Module: Mathlib.RingTheory.LocalRing.Module
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsLocalRing R
inst_4 : FinitePresentation R M
ι : Type u_5
v : ι → M
hli :
  LinearIndependent k (M := k ⊗[R] M)
    ((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v)
hsp :
  Eq (α := Submodule k (k ⊗[R] M))
    (Submodule.span k
      (Set.range ((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v)))
    ⊤
H :
  Function.Injective (α := ↥𝔪 ⊗[R] M) (β := R ⊗[R] M)
    (⇑(LinearMap.rTensor M (Submodule.subtype 𝔪)) : (a : ↥𝔪 ⊗[R] M) → R ⊗[R] M)
bk : Basis ι k (k ⊗[R] M) := Basis.mk hli ⋯
this_1 : Finite ι
this_2 : Fintype ι := Fintype.ofFinite ι
i : (ι →₀ R) →ₗ[R] M := Finsupp.linearCombination R v
hi : Surjective (α := ι →₀ R) (β := M) (⇑i : (a : ι →₀ R) → M)
this_3 : Module.Finite R ↥i.ker
this :
  Surjective (α := k ⊗[R] (ι →₀ R)) (β := k ⊗[R] M) (⇑(LinearMap.baseChange k i) : (a : k ⊗[R] (ι →₀ R)) → k ⊗[R] M)
hi' :
  Function.Bijective (α := k ⊗[R] (ι →₀ R)) (β := k ⊗[R] M)
    (⇑(LinearMap.baseChange k i) : (a : k ⊗[R] (ι →₀ R)) → k ⊗[R] M)
x : k ⊗[R] ↥i.ker
⊢ Eq (α := k ⊗[R] M) ((LinearMap.lTensor k 0 : (a : (R ⧸ 𝔪) ⊗[R] ↥i.ker) → k ⊗[R] M) x : k ⊗[R] M)
    ((LinearMap.lTensor k i : (a : k ⊗[R] (ι →₀ R)) → k ⊗[R] M)
        ((LinearMap.lTensor (HasQuotient.Quotient R (B := Submodule R R) (𝔪 : Ideal R)) i.ker.subtype :
            (a : (R ⧸ 𝔪) ⊗[R] ↥i.ker) → (R ⧸ 𝔪) ⊗[R] (ι →₀ R))
          0) :
      k ⊗[R] M)

Tactic:
simp only [LinearMap.lTensor_zero, LinearMap.zero_apply, map_zero]

Premises used: LinearMap.zero_apply, map_zero, LinearMap.lTensor_zero
-- Module: Mathlib.RingTheory.LocalRing.Module
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsLocalRing R
inst_4 : FinitePresentation R M
ι : Type u_5
v : ι → M
hli :
  LinearIndependent k (M := k ⊗[R] M)
    ((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v)
hsp :
  Eq (α := Submodule k (k ⊗[R] M))
    (Submodule.span k
      (Set.range ((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v)))
    ⊤
H :
  Function.Injective (α := ↥𝔪 ⊗[R] M) (β := R ⊗[R] M)
    (⇑(LinearMap.rTensor M (Submodule.subtype 𝔪)) : (a : ↥𝔪 ⊗[R] M) → R ⊗[R] M)
bk : Basis ι k (k ⊗[R] M) := Basis.mk hli ⋯
this_1 : Finite ι
this_2 : Fintype ι := Fintype.ofFinite ι
i : (ι →₀ R) →ₗ[R] M := Finsupp.linearCombination R v
hi : Surjective (α := ι →₀ R) (β := M) (⇑i : (a : ι →₀ R) → M)
this : Module.Finite R ↥i.ker
iequiv : (ι →₀ R) ≃ₗ[R] M := LinearEquiv.ofBijective i ⋯
h : ∀ (i : ι), ({ repr := iequiv.symm : Basis ι R M } : (a : ι) → M) i = v i
⊢ ∃ (b : Basis ι R M), ∀ (i : ι), (b : (a : ι) → M) i = v i

Tactic:
use Basis.ofRepr iequiv.symm

Premises used: Module.Basis.ofRepr, LinearEquiv.symm
-- Module: Mathlib.RingTheory.LocalRing.Module
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsLocalRing R
inst_4 : FinitePresentation R M
ι : Type u_5
v : ι → M
hli :
  LinearIndependent k (M := k ⊗[R] M)
    ((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v)
hsp :
  Eq (α := Submodule k (k ⊗[R] M))
    (Submodule.span k
      (Set.range ((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v)))
    ⊤
H :
  Function.Injective (α := ↥𝔪 ⊗[R] M) (β := R ⊗[R] M)
    (⇑(LinearMap.rTensor M (Submodule.subtype 𝔪)) : (a : ↥𝔪 ⊗[R] M) → R ⊗[R] M)
bk : Basis ι k (k ⊗[R] M) := Basis.mk hli ⋯
this_1 : Finite ι
this_2 : Fintype ι := Fintype.ofFinite ι
i : (ι →₀ R) →ₗ[R] M := Finsupp.linearCombination R v
hi : Surjective (α := ι →₀ R) (β := M) (⇑i : (a : ι →₀ R) → M)
this : Module.Finite R ↥i.ker
iequiv : (ι →₀ R) ≃ₗ[R] M := LinearEquiv.ofBijective i ⋯
j : ι
⊢ ({ repr := iequiv.symm : Basis ι R M } : (a : ι) → M) j = v j

Tactic:
simp [iequiv, i]
-- Module: Mathlib.RingTheory.LocalRing.Module
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsLocalRing R
inst_4 : FinitePresentation R M
H :
  Function.Injective (α := ↥𝔪 ⊗[R] M) (β := R ⊗[R] M)
    (⇑(LinearMap.rTensor M (Submodule.subtype 𝔪)) : (a : ↥𝔪 ⊗[R] M) → R ⊗[R] M)
ι : Type u
v : ι → M
hv : Eq (α := Submodule R M) (Submodule.span R (Set.range v)) ⊤
⊢ Eq (α := Submodule R (k ⊗[R] M))
    (Submodule.map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1)
      (Submodule.span R (Set.range v)))
    ⊤

Tactic:
have := (map_tensorProduct_mk_eq_top (N := Submodule.span R (Set.range v))).mpr hv
-- Module: Mathlib.RingTheory.LocalRing.Module
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsLocalRing R
inst_4 : FinitePresentation R M
H :
  Function.Injective (α := ↥𝔪 ⊗[R] M) (β := R ⊗[R] M)
    (⇑(LinearMap.rTensor M (Submodule.subtype 𝔪)) : (a : ↥𝔪 ⊗[R] M) → R ⊗[R] M)
ι : Type u
v : ι → M
hv : Eq (α := Submodule R M) (Submodule.span R (Set.range v)) ⊤
this :
  Eq (α := Submodule R (k ⊗[R] M))
    (Submodule.map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1)
      (Submodule.span R (Set.range v)))
    ⊤
⊢ Set.univ ⊆
    (↑(Submodule.span R
          (Set.range ((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v))) :
      Set (k ⊗[R] M))

Tactic:
rw [← Submodule.span_image, ← Set.range_comp, eq_top_iff, ← SetLike.coe_subset_coe,
    Submodule.top_coe] at this

Premises used: Set.range_comp, eq_top_iff, SetLike.coe_subset_coe, Submodule.top_coe, Submodule.span_image
-- Module: Mathlib.RingTheory.LocalRing.Module
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsLocalRing R
inst_4 : FinitePresentation R M
H :
  Function.Injective (α := ↥𝔪 ⊗[R] M) (β := R ⊗[R] M)
    (⇑(LinearMap.rTensor M (Submodule.subtype 𝔪)) : (a : ↥𝔪 ⊗[R] M) → R ⊗[R] M)
ι : Type u
v : ι → M
hv : Eq (α := Submodule R M) (Submodule.span R (Set.range v)) ⊤
this :
  Set.univ ⊆
    (↑(Submodule.span R
          (Set.range ((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v))) :
      Set (k ⊗[R] M))
rw :
  LE.le (α := Submodule k (k ⊗[R] M)) ⊤
    (Submodule.span k
      (Set.range ((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v)))
⊢ Eq (α := Submodule k (k ⊗[R] M))
    (Submodule.span k
      (Set.range ((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v)))
    ⊤

Tactic:
rw [eq_top_iff]

Premises used: eq_top_iff
-- Module: Mathlib.RingTheory.LocalRing.Module
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsLocalRing R
inst_4 : FinitePresentation R M
H :
  Function.Injective (α := ↥𝔪 ⊗[R] M) (β := R ⊗[R] M)
    (⇑(LinearMap.rTensor M (Submodule.subtype 𝔪)) : (a : ↥𝔪 ⊗[R] M) → R ⊗[R] M)
ι : Type u
v : ι → M
hv : Eq (α := Submodule R M) (Submodule.span R (Set.range v)) ⊤
this :
  Set.univ ⊆
    (↑(Submodule.span R
          (Set.range ((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v))) :
      Set (k ⊗[R] M))
⊢ LE.le (α := Submodule k (k ⊗[R] M)) ⊤
    (Submodule.span k
      (Set.range ((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v)))

Tactic:
Set.Subset.trans this (Submodule.span_subset_span _ _ _)

Premises used: Submodule.span_subset_span, Set.Subset.trans, Set.Subset
-- Module: Mathlib.RingTheory.LocalRing.Module
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsLocalRing R
inst_4 : FinitePresentation R M
H :
  Function.Injective (α := ↥𝔪 ⊗[R] M) (β := R ⊗[R] M)
    (⇑(LinearMap.rTensor M (Submodule.subtype 𝔪)) : (a : ↥𝔪 ⊗[R] M) → R ⊗[R] M)
ι : Type u
v : ι → M
hv : Eq (α := Submodule R M) (Submodule.span R (Set.range v)) ⊤
this :
  Set.univ ⊆
    (↑(Submodule.span R
          (Set.range ((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v))) :
      Set (k ⊗[R] M))
⊢ LE.le (α := Submodule k (k ⊗[R] M)) ⊤
    (Submodule.span k
      (Set.range ((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v)))

Tactic:
exact Set.Subset.trans this (Submodule.span_subset_span _ _ _)

Premises used: Submodule.span_subset_span, Set.Subset.trans
-- Module: Mathlib.RingTheory.LocalRing.Module
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsLocalRing R
inst_4 : FinitePresentation R M
H :
  Function.Injective (α := ↥𝔪 ⊗[R] M) (β := R ⊗[R] M)
    (⇑(LinearMap.rTensor M (Submodule.subtype 𝔪)) : (a : ↥𝔪 ⊗[R] M) → R ⊗[R] M)
ι : Type u
v : ι → M
hv : Eq (α := Submodule R M) (Submodule.span R (Set.range v)) ⊤
this :
  Set.univ ⊆
    (↑(Submodule.span R
          (Set.range ((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v))) :
      Set (k ⊗[R] M))
⊢ Eq (α := Submodule k (k ⊗[R] M))
    (Submodule.span k
      (Set.range ((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v)))
    ⊤

Tactic:
have : Submodule.span k (Set.range (TensorProduct.mk R k M 1 ∘ v)) = ⊤ := by
    rw [eq_top_iff]
    exact Set.Subset.trans this (Submodule.span_subset_span _ _ _)
-- Module: Mathlib.RingTheory.LocalRing.Module
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsLocalRing R
inst_4 : FinitePresentation R M
H :
  Function.Injective (α := ↥𝔪 ⊗[R] M) (β := R ⊗[R] M)
    (⇑(LinearMap.rTensor M (Submodule.subtype 𝔪)) : (a : ↥𝔪 ⊗[R] M) → R ⊗[R] M)
ι : Type u
v : ι → M
hv : Eq (α := Submodule R M) (Submodule.span R (Set.range v)) ⊤
this_1 :
  Set.univ ⊆
    (↑(Submodule.span R
          (Set.range ((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v))) :
      Set (k ⊗[R] M))
this :
  Eq (α := Submodule k (k ⊗[R] M))
    (Submodule.span k
      (Set.range ((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v)))
    ⊤
obtain :
  ∀ (κ : Type u) (a : κ → ι) (ha : Function.Injective a)
    (hsp :
      Eq (α := Submodule k (k ⊗[R] M))
        (Submodule.span k
          (Set.range (((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v) ∘ a)))
        (Submodule.span k
          (Set.range ((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v))))
    (hli :
      LinearIndependent k (M := k ⊗[R] M)
        (((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v) ∘ a)),
    ∃ (κ : Type u) (a : κ → ι) (b : Basis κ R M), ∀ (i : κ), (b : (a : κ) → M) i = v (a i)
⊢ ∃ (κ : Type u) (a : κ → ι) (b : Basis κ R M), ∀ (i : κ), (b : (a : κ) → M) i = v (a i)

Tactic:
obtain ⟨κ, a, ha, hsp, hli⟩ := exists_linearIndependent' k (TensorProduct.mk R k M 1 ∘ v)
-- Module: Mathlib.RingTheory.LocalRing.Module
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsLocalRing R
inst_4 : FinitePresentation R M
H :
  Function.Injective (α := ↥𝔪 ⊗[R] M) (β := R ⊗[R] M)
    (⇑(LinearMap.rTensor M (Submodule.subtype 𝔪)) : (a : ↥𝔪 ⊗[R] M) → R ⊗[R] M)
ι : Type u
v : ι → M
hv : Eq (α := Submodule R M) (Submodule.span R (Set.range v)) ⊤
this_1 :
  Set.univ ⊆
    (↑(Submodule.span R
          (Set.range ((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v))) :
      Set (k ⊗[R] M))
this :
  Eq (α := Submodule k (k ⊗[R] M))
    (Submodule.span k
      (Set.range ((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v)))
    ⊤
κ : Type u
a : κ → ι
ha : Function.Injective a
hsp :
  Eq (α := Submodule k (k ⊗[R] M))
    (Submodule.span k
      (Set.range (((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v) ∘ a)))
    (Submodule.span k
      (Set.range ((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v)))
hli :
  LinearIndependent k (M := k ⊗[R] M)
    (((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v) ∘ a)
⊢ Eq (α := Submodule k (k ⊗[R] M))
    (Submodule.span k
      (Set.range (((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v) ∘ a)))
    ⊤

Tactic:
rw [this] at hsp
-- Module: Mathlib.RingTheory.LocalRing.Module
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsLocalRing R
inst_4 : FinitePresentation R M
H :
  Function.Injective (α := ↥𝔪 ⊗[R] M) (β := R ⊗[R] M)
    (⇑(LinearMap.rTensor M (Submodule.subtype 𝔪)) : (a : ↥𝔪 ⊗[R] M) → R ⊗[R] M)
ι : Type u
v : ι → M
hv : Eq (α := Submodule R M) (Submodule.span R (Set.range v)) ⊤
this_1 :
  Set.univ ⊆
    (↑(Submodule.span R
          (Set.range ((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v))) :
      Set (k ⊗[R] M))
this :
  Eq (α := Submodule k (k ⊗[R] M))
    (Submodule.span k
      (Set.range ((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v)))
    ⊤
κ : Type u
a : κ → ι
ha : Function.Injective a
hsp :
  Eq (α := Submodule k (k ⊗[R] M))
    (Submodule.span k
      (Set.range (((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v) ∘ a)))
    (Submodule.span k
      (Set.range ((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v)))
hli :
  LinearIndependent k (M := k ⊗[R] M)
    (((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v) ∘ a)
hsp₁ :
  Eq (α := Submodule k (k ⊗[R] M))
    (Submodule.span k
      (Set.range (((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v) ∘ a)))
    ⊤
⊢ LinearIndependent k (M := k ⊗[R] M)
    (((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v) ∘ a)

Tactic:
rw [this] at hsp
-- Module: Mathlib.RingTheory.LocalRing.Module
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsLocalRing R
inst_4 : FinitePresentation R M
H :
  Function.Injective (α := ↥𝔪 ⊗[R] M) (β := R ⊗[R] M)
    (⇑(LinearMap.rTensor M (Submodule.subtype 𝔪)) : (a : ↥𝔪 ⊗[R] M) → R ⊗[R] M)
ι : Type u
v : ι → M
hv : Eq (α := Submodule R M) (Submodule.span R (Set.range v)) ⊤
this_1 :
  Set.univ ⊆
    (↑(Submodule.span R
          (Set.range ((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v))) :
      Set (k ⊗[R] M))
this :
  Eq (α := Submodule k (k ⊗[R] M))
    (Submodule.span k
      (Set.range ((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v)))
    ⊤
κ : Type u
a : κ → ι
ha : Function.Injective a
hsp :
  Eq (α := Submodule k (k ⊗[R] M))
    (Submodule.span k
      (Set.range (((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v) ∘ a)))
    ⊤
hli :
  LinearIndependent k (M := k ⊗[R] M)
    (((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v) ∘ a)
obtain :
  ∀ (b : Basis κ R M) (hb : ∀ (i : κ), (b : (a : κ) → M) i = (v ∘ a) i),
    ∃ (κ : Type u) (a : κ → ι) (b : Basis κ R M), ∀ (i : κ), (b : (a : κ) → M) i = v (a i)
⊢ ∃ (κ : Type u) (a : κ → ι) (b : Basis κ R M), ∀ (i : κ), (b : (a : κ) → M) i = v (a i)

Tactic:
obtain ⟨b, hb⟩ := exists_basis_of_basis_baseChange (v ∘ a) hli hsp H

Premises used: Function.comp, Module.exists_basis_of_basis_baseChange
-- Module: Mathlib.RingTheory.LocalRing.Module
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsLocalRing R
inst_4 : FinitePresentation R M
H :
  Function.Injective (α := ↥𝔪 ⊗[R] M) (β := R ⊗[R] M)
    (⇑(LinearMap.rTensor M (Submodule.subtype 𝔪)) : (a : ↥𝔪 ⊗[R] M) → R ⊗[R] M)
ι : Type u
v : ι → M
hv : Eq (α := Submodule R M) (Submodule.span R (Set.range v)) ⊤
this_1 :
  Set.univ ⊆
    (↑(Submodule.span R
          (Set.range ((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v))) :
      Set (k ⊗[R] M))
this :
  Eq (α := Submodule k (k ⊗[R] M))
    (Submodule.span k
      (Set.range ((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v)))
    ⊤
κ : Type u
a : κ → ι
ha : Function.Injective a
hsp :
  Eq (α := Submodule k (k ⊗[R] M))
    (Submodule.span k
      (Set.range (((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v) ∘ a)))
    ⊤
hli :
  LinearIndependent k (M := k ⊗[R] M)
    (((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v) ∘ a)
b : Basis κ R M
hb : ∀ (i : κ), (b : (a : κ) → M) i = (v ∘ a) i
w : Type u
w₁ : κ → ι
w₂ : Basis κ R M
h : ∀ (i : κ), (b : (a : κ) → M) i = v (a i)
⊢ ∃ (κ : Type u) (a : κ → ι) (b : Basis κ R M), ∀ (i : κ), (b : (a : κ) → M) i = v (a i)

Tactic:
use κ, a, b, hb
-- Module: Mathlib.RingTheory.LocalRing.Module
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsLocalRing R
inst_4 : FinitePresentation R M
inst_5 : Flat R M
ι : Type u
v : ι → M
hv : Eq (α := Submodule R M) (Submodule.span R (Set.range v)) ⊤
⊢ ∃ (κ : Type u) (a : κ → ι) (b : Basis κ R M), ∀ (i : κ), (b : (a : κ) → M) i = v (a i)

Tactic:
exists_basis_of_span_of_maximalIdeal_rTensor_injective
    (Module.Flat.rTensor_preserves_injective_linearMap (𝔪).subtype Subtype.val_injective) v hv

Premises used: Subtype.val_injective, IsLocalRing.maximalIdeal, Module.exists_basis_of_span_of_maximalIdeal_rTensor_injective, Submodule.subtype, Module.Flat.rTensor_preserves_injective_linearMap
-- Module: Mathlib.RingTheory.LocalRing.Module
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsLocalRing R
inst_4 : FinitePresentation R M
H :
  Function.Injective (α := ↥𝔪 ⊗[R] M) (β := R ⊗[R] M)
    (⇑(LinearMap.rTensor M (Submodule.subtype 𝔪)) : (a : ↥𝔪 ⊗[R] M) → R ⊗[R] M)
⊢ Eq.{u_2 + 1} (α := Submodule R M) (Submodule.span R (Set.range id)) ⊤

Tactic:
simp
-- Module: Mathlib.RingTheory.LocalRing.Module
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsLocalRing R
inst_4 : FinitePresentation R M
H :
  Function.Injective (α := ↥𝔪 ⊗[R] M) (β := R ⊗[R] M)
    (⇑(LinearMap.rTensor M (Submodule.subtype 𝔪)) : (a : ↥𝔪 ⊗[R] M) → R ⊗[R] M)
obtain : ∀ (w : Type u_2) (w_1 : w → M) (b : Basis w R M), (∀ (i : w), (b : (a : w) → M) i = id (w_1 i)) → Free R M
⊢ Free R M

Tactic:
obtain ⟨_, _, b, _⟩ := exists_basis_of_span_of_maximalIdeal_rTensor_injective H id (by simp)

Premises used: id, Module.exists_basis_of_span_of_maximalIdeal_rTensor_injective
-- Module: Mathlib.RingTheory.LocalRing.Module
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsLocalRing R
inst_4 : FinitePresentation R M
H :
  Function.Injective (α := ↥𝔪 ⊗[R] M) (β := R ⊗[R] M)
    (⇑(LinearMap.rTensor M (Submodule.subtype 𝔪)) : (a : ↥𝔪 ⊗[R] M) → R ⊗[R] M)
w : Type u_2
w_1 : w → M
b : Basis w R M
h : ∀ (i : w), (b : (a : w) → M) i = id (w_1 i)
⊢ Free R M

Tactic:
Free.of_basis b

Premises used: Module.Free.of_basis
-- Module: Mathlib.RingTheory.LocalRing.Module
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsLocalRing R
inst_4 : FinitePresentation R M
H :
  Function.Injective (α := ↥𝔪 ⊗[R] M) (β := R ⊗[R] M)
    (⇑(LinearMap.rTensor M (Submodule.subtype 𝔪)) : (a : ↥𝔪 ⊗[R] M) → R ⊗[R] M)
w : Type u_2
w_1 : w → M
b : Basis w R M
h : ∀ (i : w), (b : (a : w) → M) i = id (w_1 i)
⊢ Free R M

Tactic:
exact Free.of_basis b

Premises used: Module.Free.of_basis
-- Module: Mathlib.RingTheory.LocalRing.Module
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsLocalRing R
inst_4 : Flat R M
ι : Type u
v : ι → M
h :
  LinearIndependent k (M := k ⊗[R] M)
    ((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v)
rw : ∀ (s : Finset ι) (g : ι → R), Eq.{u_2 + 1} (α := M) (∑ i ∈ s, g i • v i) 0 → ∀ i ∈ s, g i = 0
⊢ LinearIndependent R v

Tactic:
rw [linearIndependent_iff']

Premises used: linearIndependent_iff'
-- Module: Mathlib.RingTheory.LocalRing.Module
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsLocalRing R
inst_4 : Flat R M
ι : Type u
f : ι → R
v : ι → M
h :
  LinearIndependent k (M := k ⊗[R] M)
    ((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v)
hfv : Eq.{u_2 + 1} (α := M) (∑ i ∈ ∅, f i • v i) 0
i : ι
hi : Membership.mem (γ := Finset ι) ∅ i
⊢ f i = 0

Tactic:
(Finset.notMem_empty _ hi).elim

Premises used: False.elim, Finset.notMem_empty
-- Module: Mathlib.RingTheory.LocalRing.Module
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsLocalRing R
inst_4 : Flat R M
ι : Type u
f : ι → R
v : ι → M
h :
  LinearIndependent k (M := k ⊗[R] M)
    ((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v)
hfv : Eq.{u_2 + 1} (α := M) (∑ i ∈ ∅, f i • v i) 0
i : ι
hi : Membership.mem (γ := Finset ι) ∅ i
⊢ f i = 0

Tactic:
exact (Finset.notMem_empty _ hi).elim

Premises used: False.elim, Finset.notMem_empty
-- Module: Mathlib.RingTheory.LocalRing.Module
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsLocalRing R
inst_4 : Flat R M
ι : Type u
f : ι → R
n : ι
s : Finset ι
hn : n ∉ s
ih :
  ∀ (v : ι → M)
    (h :
      LinearIndependent k (M := k ⊗[R] M)
        ((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v))
    (hfv : Eq.{u_2 + 1} (α := M) (∑ i ∈ s, f i • v i) 0) (i : ι) (hi : i ∈ s), f i = 0
v : ι → M
h :
  LinearIndependent k (M := k ⊗[R] M)
    ((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v)
hfv : Eq.{u_2 + 1} (α := M) (∑ i ∈ insert n s, f i • v i) 0
i : ι
hi : i ∈ insert n s
⊢ f i = 0

Tactic:
?_