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 : Flat R M
ι : Type u
f : ι → R
n_1 : ι
s : Finset ι
hn : n_1 ∉ 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)
i_1 : ι
hi_1 : i_1 ∈ insert n_1 s
l : ℕ
a : ↥(insert n_1 s) → Fin l → R
y : Fin l → M
hay :
  ∀ (i : ↥(insert n_1 s)), Eq.{u_2 + 1} (α := M) ((fun (i : ↥(insert n_1 s)) ↦ v (↑i : ι)) i) (∑ j : Fin l, a i j • y j)
hfa : ∀ (j : Fin l), Eq.{u_1 + 1} (α := R) (∑ i : ↥(insert n_1 s), (fun (i : ↥(insert n_1 s)) ↦ f (↑i : ι)) i * a i j) 0
this : v n_1 ∉ HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤
n : ↥(insert n_1 s) := Subtype.mk (p := fun (x : ι) ↦ x ∈ insert n_1 s) n_1 ⋯
n_def : n = Subtype.mk (p := fun (x : ι) ↦ x ∈ insert n_1 s) n_1 ⋯
j : Fin l
hj : IsUnit (a n j)
a' : (i : ι) → R :=
  fun (i : ι) ↦ if hi : i ∈ insert n_1 s then a (Subtype.mk (p := fun (x : ι) ↦ x ∈ insert n_1 s) i hi) j else 0
hfv : ∑ x ∈ s, f x • v x + ((-∑ i ∈ s, f i * a' i) * (↑hj.unit⁻¹ : R)) • v n_1 = 0
a_eq : ∀ (i : ↥(insert n_1 s)), a i j = a' (↑i : ι)
hfn : f (↑n : ι) = (-∑ i ∈ s, f i * a' i) * (↑hj.unit⁻¹ : R)
c : (i : ι) → R := fun (i : ι) ↦ (-if i = (↑n : ι) then 0 else a' i) * (↑hj.unit⁻¹ : R)
i : ι
hi : i ∈ s
rw rw₁ : f i * a' i = f i * a' i
⊢ (f i * if i = (↑n : ι) then 0 else a' i) = f i * a' i

Tactic:
rw [if_neg (ne_of_mem_of_not_mem hi hn)]

Premises used: ne_of_mem_of_not_mem, if_neg
-- 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_1 : ι
s : Finset ι
hn : n_1 ∉ 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)
i : ι
hi : i ∈ insert n_1 s
l : ℕ
a : ↥(insert n_1 s) → Fin l → R
y : Fin l → M
hay :
  ∀ (i : ↥(insert n_1 s)), Eq.{u_2 + 1} (α := M) ((fun (i : ↥(insert n_1 s)) ↦ v (↑i : ι)) i) (∑ j : Fin l, a i j • y j)
hfa : ∀ (j : Fin l), Eq.{u_1 + 1} (α := R) (∑ i : ↥(insert n_1 s), (fun (i : ↥(insert n_1 s)) ↦ f (↑i : ι)) i * a i j) 0
this : v n_1 ∉ HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤
n : ↥(insert n_1 s) := Subtype.mk (p := fun (x : ι) ↦ x ∈ insert n_1 s) n_1 ⋯
n_def : n = Subtype.mk (p := fun (x : ι) ↦ x ∈ insert n_1 s) n_1 ⋯
j : Fin l
hj : IsUnit (a n j)
a' : (i : ι) → R :=
  fun (i : ι) ↦ if hi : i ∈ insert n_1 s then a (Subtype.mk (p := fun (x : ι) ↦ x ∈ insert n_1 s) i hi) j else 0
hfv : ∑ x ∈ s, f x • v x + ((-∑ i ∈ s, f i * a' i) * (↑hj.unit⁻¹ : R)) • v n_1 = 0
a_eq : ∀ (i : ↥(insert n_1 s)), a i j = a' (↑i : ι)
hfn : f (↑n : ι) = (-∑ i ∈ s, f i * a' i) * (↑hj.unit⁻¹ : R)
c : (i : ι) → R := fun (i : ι) ↦ (-if i = (↑n : ι) then 0 else a' i) * (↑hj.unit⁻¹ : R)
⊢ Eq.{u_1 + 1} (α := R) (∑ x ∈ s, f x * if x = (↑n : ι) then 0 else a' x) (∑ i ∈ s, f i * a' i)

Tactic:
exact s.sum_congr rfl fun i hi ↦ by rw [if_neg (ne_of_mem_of_not_mem hi hn)]

Premises used: Finset.sum_congr, rfl
-- 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_1 : ι
s : Finset ι
hn : n_1 ∉ s
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.insert n_1 s), f (↑i : ι) • v (↑i : ι)) 0
i : ι
hi : i ∈ Insert.insert n_1 s
l : ℕ
a : ↥(Insert.insert n_1 s) → Fin l → R
y : Fin l → M
hay :
  ∀ (i : ↥(Insert.insert n_1 s)),
    Eq.{u_2 + 1} (α := M) ((fun (i : ↥(Insert.insert n_1 s)) ↦ v (↑i : ι)) i) (∑ j : Fin l, a i j • y j)
hfa :
  ∀ (j : Fin l),
    Eq.{u_1 + 1} (α := R) (∑ i : ↥(Insert.insert n_1 s), (fun (i : ↥(Insert.insert n_1 s)) ↦ f (↑i : ι)) i * a i j) 0
this : v n_1 ∉ HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤
n : ↥(Insert.insert n_1 s) := Subtype.mk (p := fun (x : ι) ↦ x ∈ Insert.insert n_1 s) n_1 ⋯
n_def : n = Subtype.mk (p := fun (x : ι) ↦ x ∈ Insert.insert n_1 s) n_1 ⋯
j : Fin l
hj : IsUnit (a n j)
a' : (i : ι) → R :=
  fun (i : ι) ↦
    if hi : i ∈ Insert.insert n_1 s then a (Subtype.mk (p := fun (x : ι) ↦ x ∈ Insert.insert n_1 s) i hi) j else 0
a_eq : ∀ (i : ↥(Insert.insert n_1 s)), a i j = a' (↑i : ι)
hfn : f (↑n : ι) = (-∑ i ∈ s, f i * a' i) * (↑hj.unit⁻¹ : R)
c : (i : ι) → R := fun (i : ι) ↦ (-if i = (↑n : ι) then 0 else a' i) * (↑hj.unit⁻¹ : R)
ih : ∀ (i : ι) (hi : i ∈ s), f i = 0
insert : ∀ (hi : i = n_1), f i = 0
insert₁ : ∀ (hi : i ∈ s), f i = 0
⊢ f i = 0

Tactic:
obtain hi | hi := Finset.mem_insert.mp hi

Premises used: Finset.mem_insert, Iff.mp
-- 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_1 : ι
s : Finset ι
hn : n_1 ∉ s
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.insert n_1 s), f (↑i : ι) • v (↑i : ι)) 0
i : ι
hi_1 : i ∈ Insert.insert n_1 s
l : ℕ
a : ↥(Insert.insert n_1 s) → Fin l → R
y : Fin l → M
hay :
  ∀ (i : ↥(Insert.insert n_1 s)),
    Eq.{u_2 + 1} (α := M) ((fun (i : ↥(Insert.insert n_1 s)) ↦ v (↑i : ι)) i) (∑ j : Fin l, a i j • y j)
hfa :
  ∀ (j : Fin l),
    Eq.{u_1 + 1} (α := R) (∑ i : ↥(Insert.insert n_1 s), (fun (i : ↥(Insert.insert n_1 s)) ↦ f (↑i : ι)) i * a i j) 0
this : v n_1 ∉ HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤
n : ↥(Insert.insert n_1 s) := Subtype.mk (p := fun (x : ι) ↦ x ∈ Insert.insert n_1 s) n_1 ⋯
n_def : n = Subtype.mk (p := fun (x : ι) ↦ x ∈ Insert.insert n_1 s) n_1 ⋯
j : Fin l
hj : IsUnit (a n j)
a' : (i : ι) → R :=
  fun (i : ι) ↦
    if hi : i ∈ Insert.insert n_1 s then a (Subtype.mk (p := fun (x : ι) ↦ x ∈ Insert.insert n_1 s) i hi) j else 0
a_eq : ∀ (i : ↥(Insert.insert n_1 s)), a i j = a' (↑i : ι)
hfn : f (↑n : ι) = (-∑ i ∈ s, f i * a' i) * (↑hj.unit⁻¹ : R)
c : (i : ι) → R := fun (i : ι) ↦ (-if i = (↑n : ι) then 0 else a' i) * (↑hj.unit⁻¹ : R)
ih : ∀ (i : ι) (hi : i ∈ s), f i = 0
hi : i = n_1
insert : ∀ x ∈ s, f x * a' x = 0
⊢ f i = 0

Tactic:
rw [hi, hfn, Finset.sum_eq_zero, neg_zero, zero_mul]

Premises used: MulZeroClass.zero_mul, Finset.sum_eq_zero, neg_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 : Flat R M
ι : Type u
f : ι → R
n_1 : ι
s : Finset ι
hn : n_1 ∉ s
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.insert n_1 s), f (↑i : ι) • v (↑i : ι)) 0
i_1 : ι
hi_1 : i_1 ∈ Insert.insert n_1 s
l : ℕ
a : ↥(Insert.insert n_1 s) → Fin l → R
y : Fin l → M
hay :
  ∀ (i : ↥(Insert.insert n_1 s)),
    Eq.{u_2 + 1} (α := M) ((fun (i : ↥(Insert.insert n_1 s)) ↦ v (↑i : ι)) i) (∑ j : Fin l, a i j • y j)
hfa :
  ∀ (j : Fin l),
    Eq.{u_1 + 1} (α := R) (∑ i : ↥(Insert.insert n_1 s), (fun (i : ↥(Insert.insert n_1 s)) ↦ f (↑i : ι)) i * a i j) 0
this : v n_1 ∉ HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤
n : ↥(Insert.insert n_1 s) := Subtype.mk (p := fun (x : ι) ↦ x ∈ Insert.insert n_1 s) n_1 ⋯
n_def : n = Subtype.mk (p := fun (x : ι) ↦ x ∈ Insert.insert n_1 s) n_1 ⋯
j : Fin l
hj : IsUnit (a n j)
a' : (i : ι) → R :=
  fun (i : ι) ↦
    if hi : i ∈ Insert.insert n_1 s then a (Subtype.mk (p := fun (x : ι) ↦ x ∈ Insert.insert n_1 s) i hi) j else 0
a_eq : ∀ (i : ↥(Insert.insert n_1 s)), a i j = a' (↑i : ι)
hfn : f (↑n : ι) = (-∑ i ∈ s, f i * a' i) * (↑hj.unit⁻¹ : R)
c : (i : ι) → R := fun (i : ι) ↦ (-if i = (↑n : ι) then 0 else a' i) * (↑hj.unit⁻¹ : R)
ih : ∀ (i : ι) (hi : i ∈ s), f i = 0
hi_2 : i_1 = n_1
i : ι
hi : i ∈ s
insert : 0 * a' i = 0
insert₁ insert₂ : Eq.{u_1 + 1} (α := R) 0 0
⊢ f i * a' i = 0

Tactic:
rw [ih i hi, zero_mul]

Premises used: MulZeroClass.zero_mul
-- 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_1 : ι
s : Finset ι
hn : n_1 ∉ s
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_1 s), f (↑i : ι) • v (↑i : ι)) 0
i : ι
hi_1 : i ∈ insert n_1 s
l : ℕ
a : ↥(insert n_1 s) → Fin l → R
y : Fin l → M
hay :
  ∀ (i : ↥(insert n_1 s)), Eq.{u_2 + 1} (α := M) ((fun (i : ↥(insert n_1 s)) ↦ v (↑i : ι)) i) (∑ j : Fin l, a i j • y j)
hfa : ∀ (j : Fin l), Eq.{u_1 + 1} (α := R) (∑ i : ↥(insert n_1 s), (fun (i : ↥(insert n_1 s)) ↦ f (↑i : ι)) i * a i j) 0
this : v n_1 ∉ HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤
n : ↥(insert n_1 s) := Subtype.mk (p := fun (x : ι) ↦ x ∈ insert n_1 s) n_1 ⋯
n_def : n = Subtype.mk (p := fun (x : ι) ↦ x ∈ insert n_1 s) n_1 ⋯
j : Fin l
hj : IsUnit (a n j)
a' : (i : ι) → R :=
  fun (i : ι) ↦ if hi : i ∈ insert n_1 s then a (Subtype.mk (p := fun (x : ι) ↦ x ∈ insert n_1 s) i hi) j else 0
a_eq : ∀ (i : ↥(insert n_1 s)), a i j = a' (↑i : ι)
hfn : f (↑n : ι) = (-∑ i ∈ s, f i * a' i) * (↑hj.unit⁻¹ : R)
c : (i : ι) → R := fun (i : ι) ↦ (-if i = (↑n : ι) then 0 else a' i) * (↑hj.unit⁻¹ : R)
ih : ∀ (i : ι) (hi : i ∈ s), f i = 0
hi : i ∈ s
⊢ f i = 0

Tactic:
ih i hi
-- 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_1 : ι
s : Finset ι
hn : n_1 ∉ s
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_1 s), f (↑i : ι) • v (↑i : ι)) 0
i : ι
hi_1 : i ∈ insert n_1 s
l : ℕ
a : ↥(insert n_1 s) → Fin l → R
y : Fin l → M
hay :
  ∀ (i : ↥(insert n_1 s)), Eq.{u_2 + 1} (α := M) ((fun (i : ↥(insert n_1 s)) ↦ v (↑i : ι)) i) (∑ j : Fin l, a i j • y j)
hfa : ∀ (j : Fin l), Eq.{u_1 + 1} (α := R) (∑ i : ↥(insert n_1 s), (fun (i : ↥(insert n_1 s)) ↦ f (↑i : ι)) i * a i j) 0
this : v n_1 ∉ HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤
n : ↥(insert n_1 s) := Subtype.mk (p := fun (x : ι) ↦ x ∈ insert n_1 s) n_1 ⋯
n_def : n = Subtype.mk (p := fun (x : ι) ↦ x ∈ insert n_1 s) n_1 ⋯
j : Fin l
hj : IsUnit (a n j)
a' : (i : ι) → R :=
  fun (i : ι) ↦ if hi : i ∈ insert n_1 s then a (Subtype.mk (p := fun (x : ι) ↦ x ∈ insert n_1 s) i hi) j else 0
a_eq : ∀ (i : ↥(insert n_1 s)), a i j = a' (↑i : ι)
hfn : f (↑n : ι) = (-∑ i ∈ s, f i * a' i) * (↑hj.unit⁻¹ : R)
c : (i : ι) → R := fun (i : ι) ↦ (-if i = (↑n : ι) then 0 else a' i) * (↑hj.unit⁻¹ : R)
ih : ∀ (i : ι) (hi : i ∈ s), f i = 0
hi : i ∈ s
⊢ f i = 0

Tactic:
exact ih i hi
-- 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 : Module.Finite R M
inst_5 : Flat R M
ι : Type u
v : ι → M
h :
  Function.Bijective (α := Finsupp.{u, u_1} ι k) (β := k ⊗[R] M)
    (⇑(linearCombination k ((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v)) :
      (a : ι →₀ k) → k ⊗[R] M)
right : Surjective (α := ι →₀ R) (β := M) (⇑(linearCombination R v) : (a : ι →₀ R) → M)
⊢ Function.Bijective (α := ι →₀ R) (β := M) (⇑(linearCombination R v) : (a : ι →₀ R) → M)

Tactic:
use linearIndependent_of_flat _ h.1

Premises used: Module.IsLocalRing.linearIndependent_of_flat, And.left
-- 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 : Module.Finite R M
inst_5 : Flat R M
ι : Type u
v : ι → M
h :
  Function.Bijective (α := Finsupp.{u, u_1} ι k) (β := k ⊗[R] M)
    (⇑(linearCombination k ((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v)) :
      (a : ι →₀ k) → k ⊗[R] M)
right : Eq (α := Submodule R M) (Submodule.span R (Set.range v)) ⊤
⊢ Surjective (α := ι →₀ R) (β := M) (⇑(linearCombination R v) : (a : ι →₀ R) → M)

Tactic:
rw [← LinearMap.range_eq_top, range_linearCombination]

Premises used: LinearMap.range_eq_top, Finsupp.range_linearCombination
-- 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 : Module.Finite R M
inst_5 : Flat R M
ι : Type u
v : ι → M
h :
  Function.Bijective (α := Finsupp.{u, u_1} ι k) (β := k ⊗[R] M)
    (⇑(linearCombination k ((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v)) :
      (a : ι →₀ k) → k ⊗[R] M)
⊢ Eq (α := Submodule R M) (Submodule.span R (Set.range v)) ⊤

Tactic:
span_eq_top_of_tmul_eq_basis _ (.mk h.1 ?_) fun _ ↦ ?_

Premises used: Module.Basis.mk, And.left, IsLocalRing.span_eq_top_of_tmul_eq_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 : Module.Finite R M
inst_5 : Flat R M
ι : Type u
v : ι → M
h :
  Function.Bijective (α := Finsupp.{u, u_1} ι k) (β := k ⊗[R] M)
    (⇑(linearCombination k ((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v)) :
      (a : ι →₀ k) → k ⊗[R] M)
right :
  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)))
right₁ : ∀ (x : ι), Eq (α := k ⊗[R] M) (1 ⊗ₜ[R] v x) ((Basis.mk ⋯ ⋯ : (a : ι) → k ⊗[R] M) x)
⊢ Eq (α := Submodule R M) (Submodule.span R (Set.range v)) ⊤

Tactic:
refine span_eq_top_of_tmul_eq_basis _ (.mk h.1 ?_) fun _ ↦ ?_

Premises used: Module.Basis.mk, And.left, IsLocalRing.span_eq_top_of_tmul_eq_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 : Module.Finite R M
inst_5 : Flat R M
ι : Type u
v : ι → M
h :
  Function.Bijective (α := Finsupp.{u, u_1} ι k) (β := k ⊗[R] M)
    (⇑(linearCombination k ((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v)) :
      (a : ι →₀ k) → 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:
simpa only [top_le_iff, ← range_linearCombination, LinearMap.range_eq_top] using h.2

Premises used: LinearMap.range_eq_top, Finsupp.range_linearCombination, And.right, top_le_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 : Module.Finite R M
inst_5 : Flat R M
ι : Type u
v : ι → M
h :
  Function.Bijective (α := Finsupp.{u, u_1} ι k) (β := k ⊗[R] M)
    (⇑(linearCombination k ((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v)) :
      (a : ι →₀ k) → k ⊗[R] M)
x : ι
⊢ Eq (α := k ⊗[R] M) (1 ⊗ₜ[R] v x) ((Basis.mk ⋯ ⋯ : (a : ι) → k ⊗[R] M) x)

Tactic:
simp
-- Module: Mathlib.RingTheory.LocalRing.Module
Goal:
R : Type u_1
P : Type u_4
inst : CommRing R
inst_1 : AddCommGroup P
inst_2 : Module R P
inst_3 : IsLocalRing R
inst_4 : Module.Finite R P
inst_5 : Flat R P
w : Basis (Free.ChooseBasisIndex k (k ⊗[R] P)) k (k ⊗[R] P) := Free.chooseBasis k (k ⊗[R] P)
v : Free.ChooseBasisIndex k (k ⊗[R] P) → P
eq :
  Eq (α := Free.ChooseBasisIndex k (k ⊗[R] P) → k ⊗[R] P)
    ((fun (x : Free.ChooseBasisIndex k (k ⊗[R] P) → P) ↦
        ((⇑((TensorProduct.mk R k P : (a : k) → P →ₗ[R] k ⊗[R] P) 1) : (a : P) → k ⊗[R] P) ∘ x :
          Free.ChooseBasisIndex k (k ⊗[R] P) → k ⊗[R] P))
      v)
    (⇑w : (a : Free.ChooseBasisIndex k (k ⊗[R] P)) → k ⊗[R] P)
⊢ LE.le (α := Submodule R P) ⊤ (Submodule.span R (Set.range v))

Tactic:
(span_eq_top_of_tmul_eq_basis _ w <| congr_fun eq).ge

Premises used: Eq.ge, IsLocalRing.span_eq_top_of_tmul_eq_basis, congr_fun
-- Module: Mathlib.RingTheory.LocalRing.Module
Goal:
R : Type u_1
P : Type u_4
inst : CommRing R
inst_1 : AddCommGroup P
inst_2 : Module R P
inst_3 : IsLocalRing R
inst_4 : Module.Finite R P
inst_5 : Flat R P
w : Basis (Free.ChooseBasisIndex k (k ⊗[R] P)) k (k ⊗[R] P) := Free.chooseBasis k (k ⊗[R] P)
v : Free.ChooseBasisIndex k (k ⊗[R] P) → P
eq :
  Eq (α := Free.ChooseBasisIndex k (k ⊗[R] P) → k ⊗[R] P)
    ((fun (x : Free.ChooseBasisIndex k (k ⊗[R] P) → P) ↦
        ((⇑((TensorProduct.mk R k P : (a : k) → P →ₗ[R] k ⊗[R] P) 1) : (a : P) → k ⊗[R] P) ∘ x :
          Free.ChooseBasisIndex k (k ⊗[R] P) → k ⊗[R] P))
      v)
    (⇑w : (a : Free.ChooseBasisIndex k (k ⊗[R] P)) → k ⊗[R] P)
⊢ LE.le (α := Submodule R P) ⊤ (Submodule.span R (Set.range v))

Tactic:
exact (span_eq_top_of_tmul_eq_basis _ w <| congr_fun eq).ge

Premises used: Eq.ge, IsLocalRing.span_eq_top_of_tmul_eq_basis, congr_fun
-- Module: Mathlib.RingTheory.LocalRing.Module
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : AddCommGroup P
inst_6 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
inst_7 : IsLocalRing R
hg : Surjective.{u_3 + 1, u_4 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
h : Exact.{u_2, u_3, u_4} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
inst_8 : Module.Finite R M
inst_9 : Module.Finite R N
inst_10 : Free R N
hf : Function.Injective (α := k ⊗[R] M) (β := k ⊗[R] N) (⇑(LinearMap.lTensor k f) : (a : k ⊗[R] M) → k ⊗[R] N)
rw : (Submodule.map f ⊤).FG
⊢ g.ker.FG

Tactic:
rw [h.linearMap_ker_eq, LinearMap.range_eq_map]

Premises used: Function.Exact.linearMap_ker_eq, LinearMap.range_eq_map
-- Module: Mathlib.RingTheory.LocalRing.Module
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : AddCommGroup P
inst_6 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
inst_7 : IsLocalRing R
hg : Surjective.{u_3 + 1, u_4 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
h : Exact.{u_2, u_3, u_4} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
inst_8 : Module.Finite R M
inst_9 : Module.Finite R N
inst_10 : Free R N
hf : Function.Injective (α := k ⊗[R] M) (β := k ⊗[R] N) (⇑(LinearMap.lTensor k f) : (a : k ⊗[R] M) → k ⊗[R] N)
⊢ (Submodule.map f ⊤).FG

Tactic:
(Module.Finite.fg_top).map f

Premises used: Module.Finite.fg_top, Submodule.FG.map
-- Module: Mathlib.RingTheory.LocalRing.Module
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : AddCommGroup P
inst_6 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
inst_7 : IsLocalRing R
hg : Surjective.{u_3 + 1, u_4 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
h : Exact.{u_2, u_3, u_4} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
inst_8 : Module.Finite R M
inst_9 : Module.Finite R N
inst_10 : Free R N
hf : Function.Injective (α := k ⊗[R] M) (β := k ⊗[R] N) (⇑(LinearMap.lTensor k f) : (a : k ⊗[R] M) → k ⊗[R] N)
⊢ (Submodule.map f ⊤).FG

Tactic:
exact (Module.Finite.fg_top).map f

Premises used: Module.Finite.fg_top, Submodule.FG.map
-- Module: Mathlib.RingTheory.LocalRing.Module
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : AddCommGroup P
inst_6 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
inst_7 : IsLocalRing R
hg : Surjective.{u_3 + 1, u_4 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
h : Exact.{u_2, u_3, u_4} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
inst_8 : Module.Finite R M
inst_9 : Module.Finite R N
inst_10 : Free R N
hf : Function.Injective (α := k ⊗[R] M) (β := k ⊗[R] N) (⇑(LinearMap.lTensor k f) : (a : k ⊗[R] M) → k ⊗[R] N)
⊢ FinitePresentation R P

Tactic:
have := Module.finitePresentation_of_free_of_surjective g hg
    (by rw [h.linearMap_ker_eq, LinearMap.range_eq_map]; exact (Module.Finite.fg_top).map f)
-- Module: Mathlib.RingTheory.LocalRing.Module
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : AddCommGroup P
inst_6 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
inst_7 : IsLocalRing R
hg : Surjective.{u_3 + 1, u_4 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
h : Exact.{u_2, u_3, u_4} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
inst_8 : Module.Finite R M
inst_9 : Module.Finite R N
inst_10 : Free R N
hf : Function.Injective (α := k ⊗[R] M) (β := k ⊗[R] N) (⇑(LinearMap.lTensor k f) : (a : k ⊗[R] M) → k ⊗[R] N)
this : FinitePresentation R P
H :
  Function.Injective (α := ↥𝔪 ⊗[R] P) (β := R ⊗[R] P)
    (⇑(LinearMap.rTensor P (Submodule.subtype 𝔪)) : (a : ↥𝔪 ⊗[R] P) → R ⊗[R] P)
⊢ Free R P

Tactic:
apply free_of_maximalIdeal_rTensor_injective

Premises used: Module.free_of_maximalIdeal_rTensor_injective
-- Module: Mathlib.RingTheory.LocalRing.Module
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : AddCommGroup P
inst_6 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
inst_7 : IsLocalRing R
hg : Surjective.{u_3 + 1, u_4 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
h : Exact.{u_2, u_3, u_4} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
inst_8 : Module.Finite R M
inst_9 : Module.Finite R N
inst_10 : Free R N
hf : Function.Injective (α := k ⊗[R] M) (β := k ⊗[R] N) (⇑(LinearMap.lTensor k f) : (a : k ⊗[R] M) → k ⊗[R] N)
this : FinitePresentation R P
H :
  Function.Injective (α := P ⊗[R] ↥𝔪) (β := P ⊗[R] R)
    (⇑(LinearMap.lTensor P (Submodule.subtype 𝔪)) : (a : P ⊗[R] ↥𝔪) → P ⊗[R] R)
⊢ Function.Injective (α := ↥𝔪 ⊗[R] P) (β := R ⊗[R] P)
    (⇑(LinearMap.rTensor P (Submodule.subtype 𝔪)) : (a : ↥𝔪 ⊗[R] P) → R ⊗[R] P)

Tactic:
rw [← LinearMap.lTensor_inj_iff_rTensor_inj]

Premises used: LinearMap.lTensor_inj_iff_rTensor_inj
-- Module: Mathlib.RingTheory.LocalRing.Module
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : AddCommGroup P
inst_6 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
inst_7 : IsLocalRing R
hg : Surjective.{u_3 + 1, u_4 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
h : Exact.{u_2, u_3, u_4} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
inst_8 : Module.Finite R M
inst_9 : Module.Finite R N
inst_10 : Free R N
hf : Function.Injective (α := k ⊗[R] M) (β := k ⊗[R] N) (⇑(LinearMap.lTensor k f) : (a : k ⊗[R] M) → k ⊗[R] N)
this : FinitePresentation R P
⊢ Function.Injective (α := P ⊗[R] ↥𝔪) (β := P ⊗[R] R)
    (⇑(LinearMap.lTensor P (Submodule.subtype 𝔪)) : (a : P ⊗[R] ↥𝔪) → P ⊗[R] R)

Tactic:
apply lTensor_injective_of_exact_of_exact_of_rTensor_injective
    h hg (LinearMap.exact_subtype_mkQ 𝔪) (Submodule.mkQ_surjective _)
    ((LinearMap.lTensor_inj_iff_rTensor_inj _ _).mp hf)
    (Module.Flat.lTensor_preserves_injective_linearMap _ Subtype.val_injective)