awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Module (goal)
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 : ι)
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)
⊢ (⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘
      (v + fun (x : ι) ↦ c x • v (↑n : ι)) =
    HAdd.hAdd (α := ι → k ⊗[R] M)
      ((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v) fun (x : ι) ↦
      HSMul.hSMul (α := HasQuotient.Quotient R (B := Ideal R) (𝔪 : Ideal R)) (β := k ⊗[R] M)
        (((⇑(Ideal.Quotient.mk 𝔪) : (a : R) → R ⧸ 𝔪) ∘ c) x)
        (((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v) (↑n : ι))
have h₁ : ∀ (x : ι),
  ((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘
        (v + fun (x : ι) ↦ c x • v (↑n : ι)))
      x =
    HAdd.hAdd (α := ι → k ⊗[R] M) (β := ι → k ⊗[R] M)
      ((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v)
      (fun (x : ι) ↦
        HSMul.hSMul (α := HasQuotient.Quotient R (B := Ideal R) (𝔪 : Ideal R)) (β := k ⊗[R] M)
          (((⇑(Ideal.Quotient.mk 𝔪) : (a : R) → R ⧸ 𝔪) ∘ c) x)
          (((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v) (↑n : ι)))
      x
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Module (goal)
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 : ι)
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)
x : ι
⊢ ((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘
        (v + fun (x : ι) ↦ c x • v (↑n : ι)))
      x =
    HAdd.hAdd (α := ι → k ⊗[R] M) (β := ι → k ⊗[R] M)
      ((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v)
      (fun (x : ι) ↦
        HSMul.hSMul (α := HasQuotient.Quotient R (B := Ideal R) (𝔪 : Ideal R)) (β := k ⊗[R] M)
          (((⇑(Ideal.Quotient.mk 𝔪) : (a : R) → R ⧸ 𝔪) ∘ c) x)
          (((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v) (↑n : ι)))
      x
have h₁ : HSMul.hSMul (β := k ⊗[R] M) (c x) (1 ⊗ₜ[R] v (↑n : ι)) =
  HSMul.hSMul (α := HasQuotient.Quotient R (B := Ideal R) (𝔪 : Ideal R)) (β := k ⊗[R] M)
    ((Ideal.Quotient.mk 𝔪 : (a : R) → R ⧸ 𝔪) (c x) : HasQuotient.Quotient R (B := Ideal R) (𝔪 : Ideal R))
    (1 ⊗ₜ[R] v (↑n : ι))
Tactic: simp [tmul_add]
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Module (goal)
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 : ι)
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 (α := HasQuotient.Quotient R (B := Ideal R) (𝔪 : Ideal R))
    (((⇑(Ideal.Quotient.mk 𝔪) : (a : R) → R ⧸ 𝔪) ∘ c) (↑n : ι)) 0
have insert : Eq (α := HasQuotient.Quotient R (B := Ideal R) (𝔪 : Ideal R))
  ((Ideal.Quotient.mk 𝔪 : (a : R) → R ⧸ 𝔪) (c (↑n : ι)) : HasQuotient.Quotient R (B := Ideal R) (𝔪 : Ideal R))
  (0 : HasQuotient.Quotient R (B := Ideal R) (𝔪 : Ideal R))
Tactic: simp_rw [Function.comp_def, c, if_pos, neg_zero, zero_mul, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Module (goal)
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 ⋯
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)
insert :
  Eq (α := HasQuotient.Quotient R (B := Ideal R) (𝔪 : Ideal R))
    ((Ideal.Quotient.mk 𝔪 : (a : R) → R ⧸ 𝔪) (c (↑n : ι)) : HasQuotient.Quotient R (B := Ideal R) (𝔪 : Ideal R))
    (0 : HasQuotient.Quotient R (B := Ideal R) (𝔪 : Ideal R))
⊢ Eq (α := HasQuotient.Quotient R (B := Ideal R) (𝔪 : Ideal R))
    (((⇑(Ideal.Quotient.mk 𝔪) : (a : R) → R ⧸ 𝔪) ∘ c) (↑n : ι)) 0
have insert₁ : Eq (α := HasQuotient.Quotient R (B := Ideal R) (𝔪 : Ideal R))
  ((Ideal.Quotient.mk 𝔪 : (a : R) → R ⧸ 𝔪) ((-if True then 0 else a' (↑n : ι)) * (↑hj.unit⁻¹ : R)) :
    HasQuotient.Quotient R (B := Ideal R) (𝔪 : Ideal R))
  (0 : HasQuotient.Quotient R (B := Ideal R) (𝔪 : Ideal R))
Tactic: simp_rw [Function.comp_def, c, if_pos, neg_zero, zero_mul, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Module (goal)
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 ⋯
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)
insert :
  Eq (α := HasQuotient.Quotient R (B := Ideal R) (𝔪 : Ideal R))
    ((Ideal.Quotient.mk 𝔪 : (a : R) → R ⧸ 𝔪) (c (↑n : ι)) : HasQuotient.Quotient R (B := Ideal R) (𝔪 : Ideal R))
    (0 : HasQuotient.Quotient R (B := Ideal R) (𝔪 : Ideal R))
insert₁ :
  Eq (α := HasQuotient.Quotient R (B := Ideal R) (𝔪 : Ideal R))
    ((Ideal.Quotient.mk 𝔪 : (a : R) → R ⧸ 𝔪) ((-if True then 0 else a' (↑n : ι)) * (↑hj.unit⁻¹ : R)) :
      HasQuotient.Quotient R (B := Ideal R) (𝔪 : Ideal R))
    (0 : HasQuotient.Quotient R (B := Ideal R) (𝔪 : Ideal R))
⊢ Eq (α := HasQuotient.Quotient R (B := Ideal R) (𝔪 : Ideal R))
    (((⇑(Ideal.Quotient.mk 𝔪) : (a : R) → R ⧸ 𝔪) ∘ c) (↑n : ι)) 0
have insert₂ : Eq (α := HasQuotient.Quotient R (B := Ideal R) (𝔪 : Ideal R))
  ((Ideal.Quotient.mk 𝔪 : (a : R) → R ⧸ 𝔪) (-0 * (↑hj.unit⁻¹ : R)) :
    HasQuotient.Quotient R (B := Ideal R) (𝔪 : Ideal R))
  (0 : HasQuotient.Quotient R (B := Ideal R) (𝔪 : Ideal R))
Tactic: simp_rw [Function.comp_def, c, if_pos, neg_zero, zero_mul, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Module (goal)
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 ⋯
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)
insert :
  Eq (α := HasQuotient.Quotient R (B := Ideal R) (𝔪 : Ideal R))
    ((Ideal.Quotient.mk 𝔪 : (a : R) → R ⧸ 𝔪) (c (↑n : ι)) : HasQuotient.Quotient R (B := Ideal R) (𝔪 : Ideal R))
    (0 : HasQuotient.Quotient R (B := Ideal R) (𝔪 : Ideal R))
insert₁ :
  Eq (α := HasQuotient.Quotient R (B := Ideal R) (𝔪 : Ideal R))
    ((Ideal.Quotient.mk 𝔪 : (a : R) → R ⧸ 𝔪) ((-if True then 0 else a' (↑n : ι)) * (↑hj.unit⁻¹ : R)) :
      HasQuotient.Quotient R (B := Ideal R) (𝔪 : Ideal R))
    (0 : HasQuotient.Quotient R (B := Ideal R) (𝔪 : Ideal R))
insert₂ :
  Eq (α := HasQuotient.Quotient R (B := Ideal R) (𝔪 : Ideal R))
    ((Ideal.Quotient.mk 𝔪 : (a : R) → R ⧸ 𝔪) (-0 * (↑hj.unit⁻¹ : R)) :
      HasQuotient.Quotient R (B := Ideal R) (𝔪 : Ideal R))
    (0 : HasQuotient.Quotient R (B := Ideal R) (𝔪 : Ideal R))
⊢ Eq (α := HasQuotient.Quotient R (B := Ideal R) (𝔪 : Ideal R))
    (((⇑(Ideal.Quotient.mk 𝔪) : (a : R) → R ⧸ 𝔪) ∘ c) (↑n : ι)) 0
have insert₃ : Eq (α := HasQuotient.Quotient R (B := Ideal R) (𝔪 : Ideal R))
  ((Ideal.Quotient.mk 𝔪 : (a : R) → R ⧸ 𝔪) (0 * (↑hj.unit⁻¹ : R)) : HasQuotient.Quotient R (B := Ideal R) (𝔪 : Ideal R))
  (0 : HasQuotient.Quotient R (B := Ideal R) (𝔪 : Ideal R))
Tactic: simp_rw [Function.comp_def, c, if_pos, neg_zero, zero_mul, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Module (goal)
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 ⋯
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)
insert :
  Eq (α := HasQuotient.Quotient R (B := Ideal R) (𝔪 : Ideal R))
    ((Ideal.Quotient.mk 𝔪 : (a : R) → R ⧸ 𝔪) (c (↑n : ι)) : HasQuotient.Quotient R (B := Ideal R) (𝔪 : Ideal R))
    (0 : HasQuotient.Quotient R (B := Ideal R) (𝔪 : Ideal R))
insert₁ :
  Eq (α := HasQuotient.Quotient R (B := Ideal R) (𝔪 : Ideal R))
    ((Ideal.Quotient.mk 𝔪 : (a : R) → R ⧸ 𝔪) ((-if True then 0 else a' (↑n : ι)) * (↑hj.unit⁻¹ : R)) :
      HasQuotient.Quotient R (B := Ideal R) (𝔪 : Ideal R))
    (0 : HasQuotient.Quotient R (B := Ideal R) (𝔪 : Ideal R))
insert₂ :
  Eq (α := HasQuotient.Quotient R (B := Ideal R) (𝔪 : Ideal R))
    ((Ideal.Quotient.mk 𝔪 : (a : R) → R ⧸ 𝔪) (-0 * (↑hj.unit⁻¹ : R)) :
      HasQuotient.Quotient R (B := Ideal R) (𝔪 : Ideal R))
    (0 : HasQuotient.Quotient R (B := Ideal R) (𝔪 : Ideal R))
insert₃ :
  Eq (α := HasQuotient.Quotient R (B := Ideal R) (𝔪 : Ideal R))
    ((Ideal.Quotient.mk 𝔪 : (a : R) → R ⧸ 𝔪) (0 * (↑hj.unit⁻¹ : R)) :
      HasQuotient.Quotient R (B := Ideal R) (𝔪 : Ideal R))
    (0 : HasQuotient.Quotient R (B := Ideal R) (𝔪 : Ideal R))
⊢ Eq (α := HasQuotient.Quotient R (B := Ideal R) (𝔪 : Ideal R))
    (((⇑(Ideal.Quotient.mk 𝔪) : (a : R) → R ⧸ 𝔪) ∘ c) (↑n : ι)) 0
have insert₄ : Eq.{u_1 + 1} (α := HasQuotient.Quotient R (B := Ideal R) (𝔪 : Ideal R)) ((Ideal.Quotient.mk 𝔪 : (a : R) → R ⧸ 𝔪) 0) 0
Tactic: simp_rw [Function.comp_def, c, if_pos, neg_zero, zero_mul, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Module (goal)
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 : ι)
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_2 + 1} (α := M) (∑ i ∈ s, f i • HAdd.hAdd (β := ι → M) v (fun (x : ι) ↦ c x • v (↑n : ι)) i) 0
have insert : ∀ (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) 𝔪 ⊤),
  let n : ↥(insert n_1 s) := Subtype.mk (p := fun (x : ι) ↦ x ∈ insert n_1 s) n_1 sorry;
  ∀ (n_def : n = Subtype.mk (p := fun (x : ι) ↦ x ∈ insert n_1 s) n_1 sorry) (j : Fin l) (hj : IsUnit (a n j)),
    let 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)),
      let c : (i : ι) → R := fun (i : ι) ↦ (-if i = (↑n : ι) then 0 else a' i) * (↑hj.unit⁻¹ : R);
      Eq.{u_2 + 1} (α := M) (∑ i ∈ s, f i • HAdd.hAdd (β := ι → M) v (fun (x : ι) ↦ c x • v (↑n : ι)) i) 0
Tactic: rw [Finset.sum_coe_sort _ (fun i ↦ f i • v i), s.sum_insert hn, add_comm, hfn] at hfv
Cleared hypotheses: hfv, i, hi, l, a, y, hay, hfa, this, n, n_def, j, hj, a', a_eq, hfn, c
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Module (goal)
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_2 + 1} (α := M) (∑ i ∈ s, f i • HAdd.hAdd (β := ι → M) v (fun (x : ι) ↦ c x • v (↑n : ι)) i) 0
have insert : ∑ x ∈ s, f x • v x + ((-∑ x ∈ s, f x * if x = (↑n : ι) then 0 else a' x) * (↑hj.unit⁻¹ : R)) • v (↑n : ι) =
  ∑ x ∈ s, f x • v x + ((-∑ i ∈ s, f i * a' i) * (↑hj.unit⁻¹ : R)) • v n_1
Tactic: simp_rw [Pi.add_apply, smul_add, s.sum_add_distrib, c, smul_smul, ← s.sum_smul, ← mul_assoc,
      ← s.sum_mul, mul_neg, s.sum_neg_distrib, ← hfv]