awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Module (hypothesis)
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)) ⊤
⊢ ∃ (κ : Type u) (a : κ → ι) (b : Basis κ R M), ∀ (i : κ), (b : (a : κ) → M) i = v (a i)
have 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)))
  ⊤
Tactic: have := (map_tensorProduct_mk_eq_top (N := Submodule.span R (Set.range v))).mpr hv
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Module (hypothesis)
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)))
    ⊤
⊢ ∃ (κ : Type u) (a : κ → ι) (b : Basis κ R M), ∀ (i : κ), (b : (a : κ) → M) i = v (a i)
have 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))
Tactic: rw [← Submodule.span_image, ← Set.range_comp, eq_top_iff, ← SetLike.coe_subset_coe,
    Submodule.top_coe] at this
Cleared hypotheses: this
-- 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 : 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)))
    ⊤
have 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)))
Tactic: rw [eq_top_iff]
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Module (hypothesis)
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))
⊢ ∃ (κ : Type u) (a : κ → ι) (b : Basis κ R M), ∀ (i : κ), (b : (a : κ) → M) i = v (a i)
have 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)))
  ⊤
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 _ _ _)
-- 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 : 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 : κ → ι) (b : Basis κ R M), ∀ (i : κ), (b : (a : κ) → M) i = v (a i)
have 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)
Tactic: obtain ⟨κ, a, ha, hsp, hli⟩ := exists_linearIndependent' k (TensorProduct.mk R k M 1 ∘ v)
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Module (hypothesis)
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)
⊢ ∃ (κ : Type u) (a : κ → ι) (b : Basis κ R M), ∀ (i : κ), (b : (a : κ) → M) i = v (a i)
have 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)))
  ⊤
Tactic: rw [this] at hsp
Cleared hypotheses: hsp, hli
-- 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 : 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)
⊢ ∃ (κ : Type u) (a : κ → ι) (b : Basis κ R M), ∀ (i : κ), (b : (a : κ) → M) i = v (a i)
have 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)
Tactic: obtain ⟨b, hb⟩ := exists_basis_of_basis_baseChange (v ∘ a) hli hsp H
-- 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 : 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
⊢ ∃ (κ : Type u) (a : κ → ι) (b : Basis κ R M), ∀ (i : κ), (b : (a : κ) → M) i = v (a i)
have h : ∀ (i : κ), (b : (a : κ) → M) i = v (a i)
Tactic: use κ, a, b, hb
-- 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 : FinitePresentation R M
H :
  Function.Injective (α := ↥𝔪 ⊗[R] M) (β := R ⊗[R] M)
    (⇑(LinearMap.rTensor M (Submodule.subtype 𝔪)) : (a : ↥𝔪 ⊗[R] M) → R ⊗[R] M)
⊢ Free R M
have 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
Tactic: obtain ⟨_, _, b, _⟩ := exists_basis_of_span_of_maximalIdeal_rTensor_injective H id (by simp)
-- 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
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)
⊢ LinearIndependent R v
have rw : ∀ (s : Finset ι) (g : ι → R), Eq.{u_2 + 1} (α := M) (∑ i ∈ s, g i • v i) 0 → ∀ i ∈ s, g i = 0
Tactic: rw [linearIndependent_iff']
-- 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
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
⊢ f i = 0
have 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 n s, f i • v i) 0) (i : ι) (hi : i ∈ insert n s), 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 => ?_
Cleared hypotheses: v, h, s, hfv, i, hi
-- 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 : ι
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
have insert : ∀ (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: rw [← Finset.sum_coe_sort] at hfv
Cleared hypotheses: hfv, i, hi
-- 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 : ι
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
have insert : ∀ (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),
  f i = 0
Tactic: have ⟨l, a, y, hay, hfa⟩ := Flat.isTrivialRelation_of_sum_smul_eq_zero hfv
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Module (hypothesis)
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
⊢ f i = 0
have this : 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
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Module (hypothesis)
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) 𝔪 ⊤
⊢ f i = 0
have n_def : let n_1 : ↥(insert n s) := Subtype.mk (p := fun (x : ι) ↦ x ∈ insert n s) n sorry;
n_1 = Subtype.mk (p := fun (x : ι) ↦ x ∈ insert n s) n sorry
Tactic: set n : ↥(insert n s) := ⟨n, Finset.mem_insert_self ..⟩ with n_def
-- 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), IsUnit (a n j)
have contrapose! : ∀ (this : ∀ (j : Fin l), ¬IsUnit (a n j)), v n_1 ∈ HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤
Tactic: contrapose! this
Cleared hypotheses: this
-- 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
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)
⊢ v n_1 ∈ HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤
have rw : ∑ j : Fin l, a n j • y j ∈ HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤
Tactic: rw [show v n = _ from hay n]
-- 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 ⋯
⊢ f i = 0
have insert : ∀ (j : Fin l) (hj : IsUnit (a n j)), 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 _) ⟨⟩
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Module (hypothesis)
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
⊢ f i = 0
have a_eq : ∀ (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]