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
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)
s : Finset ι
f : ι → R
hfv : Eq.{u_2 + 1} (α := M) (∑ i ∈ s, f i • v i) 0
i : ι
hi : i ∈ s
insert :
  ∀ (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.insert n s, f i • v i) 0) (i : ι) (hi : i ∈ Insert.insert n s), f i = 0
⊢ f i = 0

Tactic:
induction s using Finset.induction generalizing v i with
  | empty => exact (Finset.notMem_empty _ hi).elim
  | insert n s hn ih => ?_

Premises used: False.elim, Insert.insert, 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.insert n s, f i • v i) 0
i : ι
hi : i ∈ Insert.insert n s
insert :
  ∀ (hfv : Eq.{u_2 + 1} (α := M) (∑ i : ↥(Insert.insert n s), f (↑i : ι) • v (↑i : ι)) 0) (i : ι)
    (hi : i ∈ Insert.insert n s), f i = 0
⊢ f i = 0

Tactic:
rw [← Finset.sum_coe_sort] at hfv

Premises used: Finset.sum_coe_sort
-- 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.insert n s), f (↑i : ι) • v (↑i : ι)) 0
i : ι
hi : i ∈ Insert.insert n s
insert :
  ∀ (l : ℕ) (a : ↥(Insert.insert n s) → Fin l → R) (y : Fin l → M)
    (hay :
      ∀ (i : ↥(Insert.insert n s)),
        Eq.{u_2 + 1} (α := M) ((fun (i : ↥(Insert.insert n 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 s), (fun (i : ↥(Insert.insert n s)) ↦ f (↑i : ι)) i * a i j) 0),
    f i = 0
⊢ f i = 0

Tactic:
have ⟨l, a, y, hay, hfa⟩ := Flat.isTrivialRelation_of_sum_smul_eq_zero hfv
-- 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
l : ℕ
a : ↥(insert n s) → Fin l → R
y : Fin l → M
hay : ∀ (i : ↥(insert n s)), Eq.{u_2 + 1} (α := M) ((fun (i : ↥(insert n s)) ↦ v (↑i : ι)) i) (∑ j : Fin l, a i j • y j)
hfa : ∀ (j : Fin l), Eq.{u_1 + 1} (α := R) (∑ i : ↥(insert n s), (fun (i : ↥(insert n s)) ↦ f (↑i : ι)) i * a i j) 0
⊢ v n ∉ HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤

Tactic:
simpa only [← LinearMap.ker_tensorProductMk] using h.ne_zero n

Premises used: LinearIndependent.ne_zero, LinearMap.ker_tensorProductMk
-- 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
l : ℕ
a : ↥(insert n s) → Fin l → R
y : Fin l → M
hay : ∀ (i : ↥(insert n s)), Eq.{u_2 + 1} (α := M) ((fun (i : ↥(insert n s)) ↦ v (↑i : ι)) i) (∑ j : Fin l, a i j • y j)
hfa : ∀ (j : Fin l), Eq.{u_1 + 1} (α := R) (∑ i : ↥(insert n s), (fun (i : ↥(insert n s)) ↦ f (↑i : ι)) i * a i j) 0
⊢ v n ∉ HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤

Tactic:
have : v n ∉ 𝔪 • (⊤ : Submodule R M) := by
    simpa only [← LinearMap.ker_tensorProductMk] using h.ne_zero n
-- 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
l : ℕ
a : ↥(insert n s) → Fin l → R
y : Fin l → M
hay : ∀ (i : ↥(insert n s)), Eq.{u_2 + 1} (α := M) ((fun (i : ↥(insert n s)) ↦ v (↑i : ι)) i) (∑ j : Fin l, a i j • y j)
hfa : ∀ (j : Fin l), Eq.{u_1 + 1} (α := R) (∑ i : ↥(insert n s), (fun (i : ↥(insert n s)) ↦ f (↑i : ι)) i * a i j) 0
this : v n ∉ HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤
⊢ let n_1 : ↥(insert n s) := Subtype.mk (p := fun (x : ι) ↦ x ∈ insert n s) n ⋯;
  n_1 = Subtype.mk (p := fun (x : ι) ↦ x ∈ insert n s) n ⋯

Tactic:
set n : ↥(insert n s) := ⟨n, Finset.mem_insert_self ..⟩ with n_def

Premises used: Insert.insert
-- 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)
hfv : Eq.{u_2 + 1} (α := M) (∑ i : ↥(insert n_1 s), f (↑i : ι) • v (↑i : ι)) 0
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 ⋯
contrapose! : ∀ (this : ∀ (j : Fin l), ¬IsUnit (a n j)), v n_1 ∈ HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤
⊢ ∃ (j : Fin l), IsUnit (a n j)

Tactic:
contrapose! this
-- 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)
hfv : Eq.{u_2 + 1} (α := M) (∑ i : ↥(insert n_1 s), f (↑i : ι) • v (↑i : ι)) 0
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
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 ⋯
this : ∀ (j : Fin l), ¬IsUnit (a n j)
rw : ∑ j : Fin l, a n j • y j ∈ HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤
⊢ v n_1 ∈ HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤

Tactic:
rw [show v n = _ from hay n]
-- 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)
hfv : Eq.{u_2 + 1} (α := M) (∑ i : ↥(insert n_1 s), f (↑i : ι) • v (↑i : ι)) 0
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
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 ⋯
this : ∀ (j : Fin l), ¬IsUnit (a n j)
⊢ ∑ j : Fin l, a n j • y j ∈ HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤

Tactic:
sum_mem fun _ _ ↦ Submodule.smul_mem_smul (this _) ⟨⟩

Premises used: Submodule.smul_mem_smul, sum_mem, True.intro
-- 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)
hfv : Eq.{u_2 + 1} (α := M) (∑ i : ↥(insert n_1 s), f (↑i : ι) • v (↑i : ι)) 0
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
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 ⋯
this : ∀ (j : Fin l), ¬IsUnit (a n j)
⊢ ∑ j : Fin l, a n j • y j ∈ HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤

Tactic:
exact sum_mem fun _ _ ↦ Submodule.smul_mem_smul (this _) ⟨⟩
-- 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)
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 ⋯
insert : ∀ (j : Fin l) (hj : IsUnit (a n j)), f i = 0
⊢ f i = 0

Tactic:
obtain ⟨j, hj⟩ : ∃ j, IsUnit (a n j) := by
    contrapose! this
    rw [show v n = _ from hay n]
    exact sum_mem fun _ _ ↦ Submodule.smul_mem_smul (this _) ⟨⟩
-- 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)
hfv : Eq.{u_2 + 1} (α := M) (∑ i : ↥(insert n_1 s), f (↑i : ι) • v (↑i : ι)) 0
i_1 : ι
hi : 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
i : ↥(insert n_1 s)
simp_rw :
  a i j = 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 i j = a' (↑i : ι)

Tactic:
simp_rw [a', dif_pos i.2]

Premises used: dif_pos, Subtype.property
-- 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)
hfv : Eq.{u_2 + 1} (α := M) (∑ i : ↥(insert n_1 s), f (↑i : ι) • v (↑i : ι)) 0
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
⊢ ∀ (i : ↥(insert n_1 s)), a i j = a' (↑i : ι)

Tactic:
have a_eq i : a i j = a' i.1 := by simp_rw [a', dif_pos i.2]
-- 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)
hfv : Eq.{u_2 + 1} (α := M) (∑ i : ↥(insert n_1 s), f (↑i : ι) • v (↑i : ι)) 0
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
a_eq : ∀ (i : ↥(insert n_1 s)), a i j = a' (↑i : ι)
rw : f (↑n : ι) * a n j + ∑ i ∈ s, f i * a' i = 0
⊢ f (↑n : ι) = (-∑ i ∈ s, f i * a' i) * (↑hj.unit⁻¹ : R)

Tactic:
rw [← hj.mul_left_inj, mul_assoc, hj.val_inv_mul, mul_one, eq_neg_iff_add_eq_zero]

Premises used: mul_assoc, IsUnit.mul_left_inj, mul_one, eq_neg_iff_add_eq_zero, IsUnit.val_inv_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
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_1 s), f (↑i : ι) • v (↑i : ι)) 0
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
a_eq : ∀ (i : ↥(insert n_1 s)), a i j = a' (↑i : ι)
⊢ Eq.{u_1 + 1} (α := R) (∑ i : ↥(insert n_1 s), (fun (i : ↥(insert n_1 s)) ↦ f (↑i : ι)) i * a i j) 0

Tactic:
hfa j
-- 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)
hfv : Eq.{u_2 + 1} (α := M) (∑ i : ↥(insert n_1 s), f (↑i : ι) • v (↑i : ι)) 0
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
a_eq : ∀ (i : ↥(insert n_1 s)), a i j = a' (↑i : ι)
h₁ :
  f (↑n : ι) * a n j + ∑ i ∈ s, f i * a' i = ∑ i : ↥(insert n_1 s), (fun (i : ↥(insert n_1 s)) ↦ f (↑i : ι)) i * a i j
⊢ f (↑n : ι) * a n j + ∑ i ∈ s, f i * a' i = 0

Tactic:
convert! hfa j