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
N : Submodule R M
inst_4 : Module.Finite R M
this_1 : Module.{u_1, u_2} k (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤) :=
  { smul := map_tensorProduct_mk_eq_top._aux_1, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯,
    add_smul := ⋯, zero_smul := ⋯ }
this_2 : IsScalarTower.{u_1, u_1, u_2} R k (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤) := ⋯
f : k ⊗[R] M →ₗ[R] M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤ :=
  AlgebraTensorModule.lift
    ((↑R :
        {S M : Type u_1} →
          {M₂ : Type u_2} →
            [inst : Semiring R] →
              [inst_5 : Semiring S] →
                [inst_6 : AddCommMonoid M] →
                  [inst_7 : AddCommMonoid M₂] →
                    [inst_8 : Module R M] →
                      [inst_9 : Module R M₂] →
                        [inst_10 : Module S M] →
                          [inst_11 : Module S M₂] →
                            [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      (S := k)
      ((LinearEquiv.symm
            (LinearMap.ringLmapEquivSelf k k (M →ₗ[R] M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤)) :
          (a : M →ₗ[R] M ⧸ 𝔪 • ⊤) → k →ₗ[k] M →ₗ[R] M ⧸ 𝔪 • ⊤)
        (HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤).mkQ))
this :
  f ∘ₗ (TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1 =
    (HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤).mkQ
hf :
  Surjective (α := k ⊗[R] M) (β := M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤)
    (⇑f : (a : k ⊗[R] M) → M ⧸ 𝔪 • ⊤)
hN :
  Submodule.map f (Submodule.map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) N) =
    Submodule.map f ⊤
mp : ∀ (hN : Submodule.map (f ∘ₗ (TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) N = Submodule.map f ⊤), N = ⊤
mp₁ : ∀ (hN : Submodule.map (HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤).mkQ N = Submodule.map f ⊤), N = ⊤
mp₂ : ∀ (hN : Submodule.map (HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤).mkQ N = f.range), N = ⊤
mp₃ : ∀ (hN : Submodule.map (HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤).mkQ N = ⊤), N = ⊤
⊢ N = ⊤
have mp₄ : ∀ (hN : N = ⊤), N = ⊤
Tactic: rwa [← Submodule.map_comp, this, Submodule.map_top, LinearMap.range_eq_top.2 hf,
      map_mkQ_eq_top] at hN
Cleared hypotheses: hN
-- 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 : Module.Finite R M
⊢ Eq (α := Submodule R (k ⊗[R] M))
    (Submodule.map (R := R) (M := M) (σ₁₂ := RingHom.id R) ((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) ⊤)
    ⊤
have mpr : Surjective (α := M) (β := k ⊗[R] M) (⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M)
Tactic: rw [Submodule.map_top, LinearMap.range_eq_top]
-- 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 : Module.Finite R M
⊢ Subsingleton (k ⊗[R] M) ↔ Subsingleton M
have rw : Subsingleton (Submodule R (k ⊗[R] M)) ↔ Subsingleton M
Tactic: rw [← Submodule.subsingleton_iff R, ← subsingleton_iff_bot_eq_top,
    ← Submodule.subsingleton_iff R, ← subsingleton_iff_bot_eq_top,
    ← map_tensorProduct_mk_eq_top (M := M), Submodule.map_bot]
-- 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 : Module.Finite R M
rw : Subsingleton (Submodule R (k ⊗[R] M)) ↔ Subsingleton M
⊢ Subsingleton (k ⊗[R] M) ↔ Subsingleton M
have rw₁ : Eq (α := Submodule R (k ⊗[R] M)) ⊥ ⊤ ↔ Subsingleton M
Tactic: rw [← Submodule.subsingleton_iff R, ← subsingleton_iff_bot_eq_top,
    ← Submodule.subsingleton_iff R, ← subsingleton_iff_bot_eq_top,
    ← map_tensorProduct_mk_eq_top (M := M), Submodule.map_bot]
-- 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 : Module.Finite R M
rw : Subsingleton (Submodule R (k ⊗[R] M)) ↔ Subsingleton M
rw₁ : Eq (α := Submodule R (k ⊗[R] M)) ⊥ ⊤ ↔ Subsingleton M
⊢ Subsingleton (k ⊗[R] M) ↔ Subsingleton M
have rw₂ : Eq (α := Submodule R (k ⊗[R] M)) ⊥ ⊤ ↔ Subsingleton.{u_2 + 1} (Submodule R M)
Tactic: rw [← Submodule.subsingleton_iff R, ← subsingleton_iff_bot_eq_top,
    ← Submodule.subsingleton_iff R, ← subsingleton_iff_bot_eq_top,
    ← map_tensorProduct_mk_eq_top (M := M), Submodule.map_bot]
-- 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 : Module.Finite R M
rw : Subsingleton (Submodule R (k ⊗[R] M)) ↔ Subsingleton M
rw₁ : Eq (α := Submodule R (k ⊗[R] M)) ⊥ ⊤ ↔ Subsingleton M
rw₂ : Eq (α := Submodule R (k ⊗[R] M)) ⊥ ⊤ ↔ Subsingleton.{u_2 + 1} (Submodule R M)
⊢ Subsingleton (k ⊗[R] M) ↔ Subsingleton M
have rw₃ : Eq (α := Submodule R (k ⊗[R] M)) ⊥ ⊤ ↔ Eq.{u_2 + 1} (α := Submodule R M) ⊥ ⊤
Tactic: rw [← Submodule.subsingleton_iff R, ← subsingleton_iff_bot_eq_top,
    ← Submodule.subsingleton_iff R, ← subsingleton_iff_bot_eq_top,
    ← map_tensorProduct_mk_eq_top (M := M), Submodule.map_bot]
-- 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 : Module.Finite R M
rw : Subsingleton (Submodule R (k ⊗[R] M)) ↔ Subsingleton M
rw₁ : Eq (α := Submodule R (k ⊗[R] M)) ⊥ ⊤ ↔ Subsingleton M
rw₂ : Eq (α := Submodule R (k ⊗[R] M)) ⊥ ⊤ ↔ Subsingleton.{u_2 + 1} (Submodule R M)
rw₃ : Eq (α := Submodule R (k ⊗[R] M)) ⊥ ⊤ ↔ Eq.{u_2 + 1} (α := Submodule R M) ⊥ ⊤
⊢ Subsingleton (k ⊗[R] M) ↔ Subsingleton M
have rw₄ : Eq (α := Submodule R (k ⊗[R] M)) ⊥ ⊤ ↔
  Eq (α := Submodule R (k ⊗[R] M))
    (Submodule.map (R := R) (M := M) (σ₁₂ := RingHom.id R) ((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) ⊥)
    ⊤
Tactic: rw [← Submodule.subsingleton_iff R, ← subsingleton_iff_bot_eq_top,
    ← Submodule.subsingleton_iff R, ← subsingleton_iff_bot_eq_top,
    ← map_tensorProduct_mk_eq_top (M := M), Submodule.map_bot]
-- 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 : Module.Finite R M
rw : Subsingleton (Submodule R (k ⊗[R] M)) ↔ Subsingleton M
rw₁ : Eq (α := Submodule R (k ⊗[R] M)) ⊥ ⊤ ↔ Subsingleton M
rw₂ : Eq (α := Submodule R (k ⊗[R] M)) ⊥ ⊤ ↔ Subsingleton.{u_2 + 1} (Submodule R M)
rw₃ : Eq (α := Submodule R (k ⊗[R] M)) ⊥ ⊤ ↔ Eq.{u_2 + 1} (α := Submodule R M) ⊥ ⊤
rw₄ :
  Eq (α := Submodule R (k ⊗[R] M)) ⊥ ⊤ ↔
    Eq (α := Submodule R (k ⊗[R] M))
      (Submodule.map (R := R) (M := M) (σ₁₂ := RingHom.id R) ((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1)
        ⊥)
      ⊤
⊢ Subsingleton (k ⊗[R] M) ↔ Subsingleton M
have rw₅ : Eq (α := Submodule R (k ⊗[R] M)) ⊥ ⊤ ↔ Eq (α := Submodule R (k ⊗[R] M)) ⊥ ⊤
Tactic: rw [← Submodule.subsingleton_iff R, ← subsingleton_iff_bot_eq_top,
    ← Submodule.subsingleton_iff R, ← subsingleton_iff_bot_eq_top,
    ← map_tensorProduct_mk_eq_top (M := M), Submodule.map_bot]
-- 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 : Module.Finite R M
ι : Type u_5
f : ι → M
b : Basis ι k (k ⊗[R] M)
hb : ∀ (i : ι), Eq (α := k ⊗[R] M) (1 ⊗ₜ[R] f i) ((b : (a : ι) → k ⊗[R] M) i)
⊢ Eq (α := Submodule R M) (Submodule.span R (Set.range f)) ⊤
have rw : 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) ∘ f)))
  (Submodule.span k (Set.range (ι := ι) (⇑b : (a : ι) → k ⊗[R] M)))
Tactic: rw [← map_tensorProduct_mk_eq_top, Submodule.map_span, ← Submodule.restrictScalars_span R k
    Ideal.Quotient.mk_surjective, Submodule.restrictScalars_eq_top_iff,
    ← b.span_eq, ← Set.range_comp]
-- 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 : Module.Finite R M
p : PrimeSpectrum R
K : Type u_1 := p.asIdeal.ResidueField
e : K ⊗[R] M ≃ₗ[K] K ⊗[Localization.AtPrime p.asIdeal] (Localization.AtPrime p.asIdeal ⊗[R] M) :=
  LinearEquiv.symm (AlgebraTensorModule.cancelBaseChange R (Localization.AtPrime p.asIdeal) K K M)
⊢ Membership.mem (γ := Set (PrimeSpectrum R)) (support R M) p ↔ Nontrivial (p.asIdeal.ResidueField ⊗[R] M)
have rw : Membership.mem (γ := Set (PrimeSpectrum R)) (support R M) p ↔
  Nontrivial (K ⊗[Localization.AtPrime p.asIdeal] (Localization.AtPrime p.asIdeal ⊗[R] M))
Tactic: rw [e.nontrivial_congr, Module.mem_support_iff,
    (LocalizedModule.equivTensorProduct p.asIdeal.primeCompl M).nontrivial_congr,
    ← not_iff_not, not_nontrivial_iff_subsingleton, not_nontrivial_iff_subsingleton,
    IsLocalRing.subsingleton_tensorProduct]
-- 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 : Module.Finite R M
p : PrimeSpectrum R
K : Type u_1 := p.asIdeal.ResidueField
e : K ⊗[R] M ≃ₗ[K] K ⊗[Localization.AtPrime p.asIdeal] (Localization.AtPrime p.asIdeal ⊗[R] M) :=
  LinearEquiv.symm (AlgebraTensorModule.cancelBaseChange R (Localization.AtPrime p.asIdeal) K K M)
rw :
  Membership.mem (γ := Set (PrimeSpectrum R)) (support R M) p ↔
    Nontrivial (K ⊗[Localization.AtPrime p.asIdeal] (Localization.AtPrime p.asIdeal ⊗[R] M))
⊢ Membership.mem (γ := Set (PrimeSpectrum R)) (support R M) p ↔ Nontrivial (p.asIdeal.ResidueField ⊗[R] M)
have rw₁ : Nontrivial (LocalizedModule p.asIdeal.primeCompl M) ↔
  Nontrivial (K ⊗[Localization.AtPrime p.asIdeal] (Localization.AtPrime p.asIdeal ⊗[R] M))
Tactic: rw [e.nontrivial_congr, Module.mem_support_iff,
    (LocalizedModule.equivTensorProduct p.asIdeal.primeCompl M).nontrivial_congr,
    ← not_iff_not, not_nontrivial_iff_subsingleton, not_nontrivial_iff_subsingleton,
    IsLocalRing.subsingleton_tensorProduct]
-- 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 : Module.Finite R M
p : PrimeSpectrum R
K : Type u_1 := p.asIdeal.ResidueField
e : K ⊗[R] M ≃ₗ[K] K ⊗[Localization.AtPrime p.asIdeal] (Localization.AtPrime p.asIdeal ⊗[R] M) :=
  LinearEquiv.symm (AlgebraTensorModule.cancelBaseChange R (Localization.AtPrime p.asIdeal) K K M)
rw :
  Membership.mem (γ := Set (PrimeSpectrum R)) (support R M) p ↔
    Nontrivial (K ⊗[Localization.AtPrime p.asIdeal] (Localization.AtPrime p.asIdeal ⊗[R] M))
rw₁ :
  Nontrivial (LocalizedModule p.asIdeal.primeCompl M) ↔
    Nontrivial (K ⊗[Localization.AtPrime p.asIdeal] (Localization.AtPrime p.asIdeal ⊗[R] M))
⊢ Membership.mem (γ := Set (PrimeSpectrum R)) (support R M) p ↔ Nontrivial (p.asIdeal.ResidueField ⊗[R] M)
have rw₂ : Nontrivial (Localization (M := R) p.asIdeal.primeCompl ⊗[R] M) ↔
  Nontrivial (K ⊗[Localization.AtPrime p.asIdeal] (Localization.AtPrime p.asIdeal ⊗[R] M))
Tactic: rw [e.nontrivial_congr, Module.mem_support_iff,
    (LocalizedModule.equivTensorProduct p.asIdeal.primeCompl M).nontrivial_congr,
    ← not_iff_not, not_nontrivial_iff_subsingleton, not_nontrivial_iff_subsingleton,
    IsLocalRing.subsingleton_tensorProduct]
-- 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 : Module.Finite R M
p : PrimeSpectrum R
K : Type u_1 := p.asIdeal.ResidueField
e : K ⊗[R] M ≃ₗ[K] K ⊗[Localization.AtPrime p.asIdeal] (Localization.AtPrime p.asIdeal ⊗[R] M) :=
  LinearEquiv.symm (AlgebraTensorModule.cancelBaseChange R (Localization.AtPrime p.asIdeal) K K M)
rw :
  Membership.mem (γ := Set (PrimeSpectrum R)) (support R M) p ↔
    Nontrivial (K ⊗[Localization.AtPrime p.asIdeal] (Localization.AtPrime p.asIdeal ⊗[R] M))
rw₁ :
  Nontrivial (LocalizedModule p.asIdeal.primeCompl M) ↔
    Nontrivial (K ⊗[Localization.AtPrime p.asIdeal] (Localization.AtPrime p.asIdeal ⊗[R] M))
rw₂ :
  Nontrivial (Localization (M := R) p.asIdeal.primeCompl ⊗[R] M) ↔
    Nontrivial (K ⊗[Localization.AtPrime p.asIdeal] (Localization.AtPrime p.asIdeal ⊗[R] M))
⊢ Membership.mem (γ := Set (PrimeSpectrum R)) (support R M) p ↔ Nontrivial (p.asIdeal.ResidueField ⊗[R] M)
have rw₃ : ¬Nontrivial (Localization (M := R) p.asIdeal.primeCompl ⊗[R] M) ↔
  ¬Nontrivial (K ⊗[Localization.AtPrime p.asIdeal] (Localization.AtPrime p.asIdeal ⊗[R] M))
Tactic: rw [e.nontrivial_congr, Module.mem_support_iff,
    (LocalizedModule.equivTensorProduct p.asIdeal.primeCompl M).nontrivial_congr,
    ← not_iff_not, not_nontrivial_iff_subsingleton, not_nontrivial_iff_subsingleton,
    IsLocalRing.subsingleton_tensorProduct]
-- 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 : Module.Finite R M
p : PrimeSpectrum R
K : Type u_1 := p.asIdeal.ResidueField
e : K ⊗[R] M ≃ₗ[K] K ⊗[Localization.AtPrime p.asIdeal] (Localization.AtPrime p.asIdeal ⊗[R] M) :=
  LinearEquiv.symm (AlgebraTensorModule.cancelBaseChange R (Localization.AtPrime p.asIdeal) K K M)
rw :
  Membership.mem (γ := Set (PrimeSpectrum R)) (support R M) p ↔
    Nontrivial (K ⊗[Localization.AtPrime p.asIdeal] (Localization.AtPrime p.asIdeal ⊗[R] M))
rw₁ :
  Nontrivial (LocalizedModule p.asIdeal.primeCompl M) ↔
    Nontrivial (K ⊗[Localization.AtPrime p.asIdeal] (Localization.AtPrime p.asIdeal ⊗[R] M))
rw₂ :
  Nontrivial (Localization (M := R) p.asIdeal.primeCompl ⊗[R] M) ↔
    Nontrivial (K ⊗[Localization.AtPrime p.asIdeal] (Localization.AtPrime p.asIdeal ⊗[R] M))
rw₃ :
  ¬Nontrivial (Localization (M := R) p.asIdeal.primeCompl ⊗[R] M) ↔
    ¬Nontrivial (K ⊗[Localization.AtPrime p.asIdeal] (Localization.AtPrime p.asIdeal ⊗[R] M))
⊢ Membership.mem (γ := Set (PrimeSpectrum R)) (support R M) p ↔ Nontrivial (p.asIdeal.ResidueField ⊗[R] M)
have rw₄ : Subsingleton (Localization (M := R) p.asIdeal.primeCompl ⊗[R] M) ↔
  ¬Nontrivial (K ⊗[Localization.AtPrime p.asIdeal] (Localization.AtPrime p.asIdeal ⊗[R] M))
Tactic: rw [e.nontrivial_congr, Module.mem_support_iff,
    (LocalizedModule.equivTensorProduct p.asIdeal.primeCompl M).nontrivial_congr,
    ← not_iff_not, not_nontrivial_iff_subsingleton, not_nontrivial_iff_subsingleton,
    IsLocalRing.subsingleton_tensorProduct]
-- 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 : Module.Finite R M
p : PrimeSpectrum R
K : Type u_1 := p.asIdeal.ResidueField
e : K ⊗[R] M ≃ₗ[K] K ⊗[Localization.AtPrime p.asIdeal] (Localization.AtPrime p.asIdeal ⊗[R] M) :=
  LinearEquiv.symm (AlgebraTensorModule.cancelBaseChange R (Localization.AtPrime p.asIdeal) K K M)
rw :
  Membership.mem (γ := Set (PrimeSpectrum R)) (support R M) p ↔
    Nontrivial (K ⊗[Localization.AtPrime p.asIdeal] (Localization.AtPrime p.asIdeal ⊗[R] M))
rw₁ :
  Nontrivial (LocalizedModule p.asIdeal.primeCompl M) ↔
    Nontrivial (K ⊗[Localization.AtPrime p.asIdeal] (Localization.AtPrime p.asIdeal ⊗[R] M))
rw₂ :
  Nontrivial (Localization (M := R) p.asIdeal.primeCompl ⊗[R] M) ↔
    Nontrivial (K ⊗[Localization.AtPrime p.asIdeal] (Localization.AtPrime p.asIdeal ⊗[R] M))
rw₃ :
  ¬Nontrivial (Localization (M := R) p.asIdeal.primeCompl ⊗[R] M) ↔
    ¬Nontrivial (K ⊗[Localization.AtPrime p.asIdeal] (Localization.AtPrime p.asIdeal ⊗[R] M))
rw₄ :
  Subsingleton (Localization (M := R) p.asIdeal.primeCompl ⊗[R] M) ↔
    ¬Nontrivial (K ⊗[Localization.AtPrime p.asIdeal] (Localization.AtPrime p.asIdeal ⊗[R] M))
⊢ Membership.mem (γ := Set (PrimeSpectrum R)) (support R M) p ↔ Nontrivial (p.asIdeal.ResidueField ⊗[R] M)
have rw₅ : Subsingleton (Localization (M := R) p.asIdeal.primeCompl ⊗[R] M) ↔
  Subsingleton (K ⊗[Localization.AtPrime p.asIdeal] (Localization.AtPrime p.asIdeal ⊗[R] M))
Tactic: rw [e.nontrivial_congr, Module.mem_support_iff,
    (LocalizedModule.equivTensorProduct p.asIdeal.primeCompl M).nontrivial_congr,
    ← not_iff_not, not_nontrivial_iff_subsingleton, not_nontrivial_iff_subsingleton,
    IsLocalRing.subsingleton_tensorProduct]
-- 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 : Module.Finite R M
p : PrimeSpectrum R
K : Type u_1 := p.asIdeal.ResidueField
e : K ⊗[R] M ≃ₗ[K] K ⊗[Localization.AtPrime p.asIdeal] (Localization.AtPrime p.asIdeal ⊗[R] M) :=
  LinearEquiv.symm (AlgebraTensorModule.cancelBaseChange R (Localization.AtPrime p.asIdeal) K K M)
rw :
  Membership.mem (γ := Set (PrimeSpectrum R)) (support R M) p ↔
    Nontrivial (K ⊗[Localization.AtPrime p.asIdeal] (Localization.AtPrime p.asIdeal ⊗[R] M))
rw₁ :
  Nontrivial (LocalizedModule p.asIdeal.primeCompl M) ↔
    Nontrivial (K ⊗[Localization.AtPrime p.asIdeal] (Localization.AtPrime p.asIdeal ⊗[R] M))
rw₂ :
  Nontrivial (Localization (M := R) p.asIdeal.primeCompl ⊗[R] M) ↔
    Nontrivial (K ⊗[Localization.AtPrime p.asIdeal] (Localization.AtPrime p.asIdeal ⊗[R] M))
rw₃ :
  ¬Nontrivial (Localization (M := R) p.asIdeal.primeCompl ⊗[R] M) ↔
    ¬Nontrivial (K ⊗[Localization.AtPrime p.asIdeal] (Localization.AtPrime p.asIdeal ⊗[R] M))
rw₄ :
  Subsingleton (Localization (M := R) p.asIdeal.primeCompl ⊗[R] M) ↔
    ¬Nontrivial (K ⊗[Localization.AtPrime p.asIdeal] (Localization.AtPrime p.asIdeal ⊗[R] M))
rw₅ :
  Subsingleton (Localization (M := R) p.asIdeal.primeCompl ⊗[R] M) ↔
    Subsingleton (K ⊗[Localization.AtPrime p.asIdeal] (Localization.AtPrime p.asIdeal ⊗[R] M))
⊢ Membership.mem (γ := Set (PrimeSpectrum R)) (support R M) p ↔ Nontrivial (p.asIdeal.ResidueField ⊗[R] M)
have rw₆ : Subsingleton (Localization (M := R) p.asIdeal.primeCompl ⊗[R] M) ↔ Subsingleton (Localization.AtPrime p.asIdeal ⊗[R] M)
Tactic: rw [e.nontrivial_congr, Module.mem_support_iff,
    (LocalizedModule.equivTensorProduct p.asIdeal.primeCompl M).nontrivial_congr,
    ← not_iff_not, not_nontrivial_iff_subsingleton, not_nontrivial_iff_subsingleton,
    IsLocalRing.subsingleton_tensorProduct]
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Module (goal)
Goal:
R : Type u_1
inst : CommRing R
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N₁ : Type u_8
N₂ : Type u_9
N₃ : Type u_10
inst_1 : AddCommGroup M₁
inst_2 : Module R M₁
inst_3 : AddCommGroup M₂
inst_4 : Module R M₂
inst_5 : AddCommGroup M₃
inst_6 : Module R M₃
inst_7 : AddCommGroup N₁
inst_8 : Module R N₁
inst_9 : AddCommGroup N₂
inst_10 : Module R N₂
inst_11 : AddCommGroup N₃
inst_12 : Module R N₃
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
g₁ : N₁ →ₗ[R] N₂
g₂ : N₂ →ₗ[R] N₃
hfexact : Exact.{u_5, u_6, u_7} (M := M₁) (N := M₂) (P := M₃) (⇑f₁ : (a : M₁) → M₂) (⇑f₂ : (a : M₂) → M₃)
hfsurj : Surjective.{u_6 + 1, u_7 + 1} (α := M₂) (β := M₃) (⇑f₂ : (a : M₂) → M₃)
hgexact : Exact.{u_8, u_9, u_10} (M := N₁) (N := N₂) (P := N₃) (⇑g₁ : (a : N₁) → N₂) (⇑g₂ : (a : N₂) → N₃)
hgsurj : Surjective.{u_9 + 1, u_10 + 1} (α := N₂) (β := N₃) (⇑g₂ : (a : N₂) → N₃)
hfinj :
  Function.Injective (α := M₁ ⊗[R] N₃) (β := M₂ ⊗[R] N₃) (⇑(LinearMap.rTensor N₃ f₁) : (a : M₁ ⊗[R] N₃) → M₂ ⊗[R] N₃)
hginj :
  Function.Injective (α := M₂ ⊗[R] N₁) (β := M₂ ⊗[R] N₂) (⇑(LinearMap.lTensor M₂ g₁) : (a : M₂ ⊗[R] N₁) → M₂ ⊗[R] N₂)
⊢ Function.Injective (α := M₃ ⊗[R] N₁) (β := M₃ ⊗[R] N₂) (⇑(LinearMap.lTensor M₃ g₁) : (a : M₃ ⊗[R] N₁) → M₃ ⊗[R] N₂)
have rw : ∀ (a : M₃ ⊗[R] N₁),
  Eq (α := M₃ ⊗[R] N₂) ((LinearMap.lTensor M₃ g₁ : (a : M₃ ⊗[R] N₁) → M₃ ⊗[R] N₂) a : M₃ ⊗[R] N₂) (0 : M₃ ⊗[R] N₂) →
    a = 0
Tactic: rw [injective_iff_map_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Module (goal)
Goal:
R : Type u_1
inst : CommRing R
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N₁ : Type u_8
N₂ : Type u_9
N₃ : Type u_10
inst_1 : AddCommGroup M₁
inst_2 : Module R M₁
inst_3 : AddCommGroup M₂
inst_4 : Module R M₂
inst_5 : AddCommGroup M₃
inst_6 : Module R M₃
inst_7 : AddCommGroup N₁
inst_8 : Module R N₁
inst_9 : AddCommGroup N₂
inst_10 : Module R N₂
inst_11 : AddCommGroup N₃
inst_12 : Module R N₃
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
g₁ : N₁ →ₗ[R] N₂
g₂ : N₂ →ₗ[R] N₃
hfexact : Exact.{u_5, u_6, u_7} (M := M₁) (N := M₂) (P := M₃) (⇑f₁ : (a : M₁) → M₂) (⇑f₂ : (a : M₂) → M₃)
hfsurj : Surjective.{u_6 + 1, u_7 + 1} (α := M₂) (β := M₃) (⇑f₂ : (a : M₂) → M₃)
hgexact : Exact.{u_8, u_9, u_10} (M := N₁) (N := N₂) (P := N₃) (⇑g₁ : (a : N₁) → N₂) (⇑g₂ : (a : N₂) → N₃)
hgsurj : Surjective.{u_9 + 1, u_10 + 1} (α := N₂) (β := N₃) (⇑g₂ : (a : N₂) → N₃)
hfinj :
  Function.Injective (α := M₁ ⊗[R] N₃) (β := M₂ ⊗[R] N₃) (⇑(LinearMap.rTensor N₃ f₁) : (a : M₁ ⊗[R] N₃) → M₂ ⊗[R] N₃)
hginj :
  Function.Injective (α := M₂ ⊗[R] N₁) (β := M₂ ⊗[R] N₂) (⇑(LinearMap.lTensor M₂ g₁) : (a : M₂ ⊗[R] N₁) → M₂ ⊗[R] N₂)
x : M₃ ⊗[R] N₁
hx : Eq (α := M₃ ⊗[R] N₂) ((LinearMap.lTensor M₃ g₁ : (a : M₃ ⊗[R] N₁) → M₃ ⊗[R] N₂) x : M₃ ⊗[R] N₂) (0 : M₃ ⊗[R] N₂)
⊢ x = 0
have obtain : ∀ (x : M₂ ⊗[R] N₁)
  (hx :
    Eq (α := M₃ ⊗[R] N₂)
      ((LinearMap.lTensor M₃ g₁ : (a : M₃ ⊗[R] N₁) → M₃ ⊗[R] N₂)
          ((LinearMap.rTensor N₁ f₂ : (a : M₂ ⊗[R] N₁) → M₃ ⊗[R] N₁) x) :
        M₃ ⊗[R] N₂)
      (0 : M₃ ⊗[R] N₂)),
  Eq (α := M₃ ⊗[R] N₁) ((LinearMap.rTensor N₁ f₂ : (a : M₂ ⊗[R] N₁) → M₃ ⊗[R] N₁) x : M₃ ⊗[R] N₁) (0 : M₃ ⊗[R] N₁)
Tactic: obtain ⟨x, rfl⟩ := f₂.rTensor_surjective N₁ hfsurj x
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Module (goal)
Goal:
R : Type u_1
inst : CommRing R
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N₁ : Type u_8
N₂ : Type u_9
N₃ : Type u_10
inst_1 : AddCommGroup M₁
inst_2 : Module R M₁
inst_3 : AddCommGroup M₂
inst_4 : Module R M₂
inst_5 : AddCommGroup M₃
inst_6 : Module R M₃
inst_7 : AddCommGroup N₁
inst_8 : Module R N₁
inst_9 : AddCommGroup N₂
inst_10 : Module R N₂
inst_11 : AddCommGroup N₃
inst_12 : Module R N₃
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
g₁ : N₁ →ₗ[R] N₂
g₂ : N₂ →ₗ[R] N₃
hfexact : Exact.{u_5, u_6, u_7} (M := M₁) (N := M₂) (P := M₃) (⇑f₁ : (a : M₁) → M₂) (⇑f₂ : (a : M₂) → M₃)
hfsurj : Surjective.{u_6 + 1, u_7 + 1} (α := M₂) (β := M₃) (⇑f₂ : (a : M₂) → M₃)
hgexact : Exact.{u_8, u_9, u_10} (M := N₁) (N := N₂) (P := N₃) (⇑g₁ : (a : N₁) → N₂) (⇑g₂ : (a : N₂) → N₃)
hgsurj : Surjective.{u_9 + 1, u_10 + 1} (α := N₂) (β := N₃) (⇑g₂ : (a : N₂) → N₃)
hfinj :
  Function.Injective (α := M₁ ⊗[R] N₃) (β := M₂ ⊗[R] N₃) (⇑(LinearMap.rTensor N₃ f₁) : (a : M₁ ⊗[R] N₃) → M₂ ⊗[R] N₃)
hginj :
  Function.Injective (α := M₂ ⊗[R] N₁) (β := M₂ ⊗[R] N₂) (⇑(LinearMap.lTensor M₂ g₁) : (a : M₂ ⊗[R] N₁) → M₂ ⊗[R] N₂)
x : M₂ ⊗[R] N₁
hx :
  Eq (α := M₃ ⊗[R] N₂)
    ((LinearMap.lTensor M₃ g₁ : (a : M₃ ⊗[R] N₁) → M₃ ⊗[R] N₂)
        ((LinearMap.rTensor N₁ f₂ : (a : M₂ ⊗[R] N₁) → M₃ ⊗[R] N₁) x) :
      M₃ ⊗[R] N₂)
    (0 : M₃ ⊗[R] N₂)
⊢ Eq (α := M₃ ⊗[R] N₂)
    ((LinearMap.rTensor N₂ f₂ : (a : M₂ ⊗[R] N₂) → M₃ ⊗[R] N₂)
        ((LinearMap.lTensor M₂ g₁ : (a : M₂ ⊗[R] N₁) → M₂ ⊗[R] N₂) x) :
      M₃ ⊗[R] N₂)
    (0 : M₃ ⊗[R] N₂)
have rw : Eq (α := M₃ ⊗[R] N₂)
  ((LinearMap.rTensor N₂ f₂ : (a : M₂ ⊗[R] N₂) → M₃ ⊗[R] N₂)
      ((LinearMap.lTensor M₂ g₁ : (a : M₂ ⊗[R] N₁) → M₂ ⊗[R] N₂) x) :
    M₃ ⊗[R] N₂)
  ((LinearMap.lTensor M₃ g₁ : (a : M₃ ⊗[R] N₁) → M₃ ⊗[R] N₂)
      ((LinearMap.rTensor N₁ f₂ : (a : M₂ ⊗[R] N₁) → M₃ ⊗[R] N₁) x) :
    M₃ ⊗[R] N₂)
Tactic: rw [← hx, ← LinearMap.comp_apply, ← LinearMap.comp_apply, LinearMap.rTensor_comp_lTensor,
      LinearMap.lTensor_comp_rTensor]