awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.FreeLocus (goal)
Goal:
R : Type uR
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Flat R M
inst_4 : Module.Finite R M
S : Type u_1
inst_5 : CommRing S
inst_6 : Algebra R S
p : PrimeSpectrum S
q : PrimeSpectrum R := comap (algebraMap R S) p
this : Algebra.{uR, u_1} (Localization.AtPrime q.asIdeal) (Localization.AtPrime p.asIdeal) :=
  AtPrime.algebraOfLiesOver q.asIdeal p.asIdeal
e : LocalizedModule p.asIdeal.primeCompl (S ⊗[R] M) ≃ₗ[Localization.AtPrime p.asIdeal]
  Localization.AtPrime p.asIdeal ⊗[Localization.AtPrime q.asIdeal] LocalizedModule q.asIdeal.primeCompl M :=
  ((equivTensorProduct p.asIdeal.primeCompl (S ⊗[R] M) ≪≫ₗ
            AlgebraTensorModule.cancelBaseChange R S (Localization.AtPrime p.asIdeal)
              (Localization (M := S) p.asIdeal.primeCompl) M :
          LocalizedModule p.asIdeal.primeCompl (S ⊗[R] M) ≃ₗ[Localization.AtPrime p.asIdeal]
            TensorProduct.{uR, u_1, uM} R (Localization (M := S) p.asIdeal.primeCompl) M) ≪≫ₗ
        (LinearEquiv.symm
            (AlgebraTensorModule.cancelBaseChange R (Localization.AtPrime q.asIdeal) (Localization.AtPrime p.asIdeal)
              (Localization (M := S) p.asIdeal.primeCompl) M) :
          TensorProduct.{uR, u_1, uM} R (Localization (M := S) p.asIdeal.primeCompl)
              M ≃ₗ[Localization.AtPrime p.asIdeal]
            Localization (M := S) p.asIdeal.primeCompl ⊗[Localization.AtPrime q.asIdeal]
              (Localization.AtPrime q.asIdeal ⊗[R] M)) :
      LocalizedModule p.asIdeal.primeCompl (S ⊗[R] M) ≃ₗ[Localization.AtPrime p.asIdeal]
        Localization (M := S) p.asIdeal.primeCompl ⊗[Localization.AtPrime q.asIdeal]
          (Localization.AtPrime q.asIdeal ⊗[R] M)) ≪≫ₗ
    (AlgebraTensorModule.congr
        (LinearEquiv.refl (Localization.AtPrime p.asIdeal) (Localization (M := S) p.asIdeal.primeCompl))
        (LinearEquiv.symm (equivTensorProduct q.asIdeal.primeCompl M)) :
      Localization (M := S) p.asIdeal.primeCompl ⊗[Localization.AtPrime q.asIdeal]
          (Localization.AtPrime q.asIdeal ⊗[R] M) ≃ₗ[Localization.AtPrime p.asIdeal]
        Localization.AtPrime p.asIdeal ⊗[Localization.AtPrime q.asIdeal] LocalizedModule q.asIdeal.primeCompl M)
⊢ rankAtStalk (S ⊗[R] M) p = rankAtStalk M (comap (algebraMap R S) p)
have rw : finrank (Localization.AtPrime p.asIdeal)
    (Localization.AtPrime p.asIdeal ⊗[Localization.AtPrime q.asIdeal] LocalizedModule q.asIdeal.primeCompl M) =
  rankAtStalk M (comap (algebraMap R S) p)
Tactic: rw [rankAtStalk, e.finrank_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.FreeLocus (goal)
Goal:
R : Type uR
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Flat R M
inst_4 : Module.Finite R M
N : Type u_1
inst_5 : AddCommGroup N
inst_6 : Module R N
inst_7 : Module.Finite R N
inst_8 : Flat R N
⊢ rankAtStalk (M ⊗[R] N) = HMul.hMul (α := (p : PrimeSpectrum R) → ℕ) (rankAtStalk M) (rankAtStalk N)
have h : ∀ (p : PrimeSpectrum R),
  rankAtStalk (M ⊗[R] N) p =
    HMul.hMul (α := (p : PrimeSpectrum R) → ℕ) (β := (p : PrimeSpectrum R) → ℕ) (rankAtStalk M) (rankAtStalk N) p
Tactic: ext p
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.FreeLocus (goal)
Goal:
R : Type uR
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Flat R M
inst_4 : Module.Finite R M
N : Type u_1
inst_5 : AddCommGroup N
inst_6 : Module R N
inst_7 : Module.Finite R N
inst_8 : Flat R N
p : PrimeSpectrum R
e : Localization.AtPrime p.asIdeal ⊗[R] (M ⊗[R] N) ≃ₗ[Localization.AtPrime p.asIdeal]
  Localization.AtPrime p.asIdeal ⊗[R] M ⊗[Localization.AtPrime p.asIdeal] (Localization.AtPrime p.asIdeal ⊗[R] N) :=
  (LinearEquiv.symm
        (AlgebraTensorModule.assoc R R (Localization.AtPrime p.asIdeal) (Localization.AtPrime p.asIdeal) M N) :
      Localization.AtPrime p.asIdeal ⊗[R] (M ⊗[R] N) ≃ₗ[Localization.AtPrime p.asIdeal]
        Localization.AtPrime p.asIdeal ⊗[R] M ⊗[R] N) ≪≫ₗ
    (LinearEquiv.symm
        (AlgebraTensorModule.cancelBaseChange R (Localization.AtPrime p.asIdeal) (Localization.AtPrime p.asIdeal)
          (Localization.AtPrime p.asIdeal ⊗[R] M) N) :
      Localization.AtPrime p.asIdeal ⊗[R] M ⊗[R] N ≃ₗ[Localization.AtPrime p.asIdeal]
        Localization.AtPrime p.asIdeal ⊗[R] M ⊗[Localization.AtPrime p.asIdeal] (Localization.AtPrime p.asIdeal ⊗[R] N))
⊢ rankAtStalk (M ⊗[R] N) p =
    HMul.hMul (α := (p : PrimeSpectrum R) → ℕ) (β := (p : PrimeSpectrum R) → ℕ) (rankAtStalk M) (rankAtStalk N) p
have h : finrank (Localization.AtPrime p.asIdeal) (Localization.AtPrime p.asIdeal ⊗[R] (M ⊗[R] N)) =
  HMul.hMul (α := (p : PrimeSpectrum R) → ℕ) (β := (p : PrimeSpectrum R) → ℕ) (rankAtStalk M) (rankAtStalk N) p
Tactic: rw [rankAtStalk_eq_finrank_tensorProduct, e.finrank_eq, finrank_tensorProduct,
    ← rankAtStalk_eq_finrank_tensorProduct, ← rankAtStalk_eq_finrank_tensorProduct, Pi.mul_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.FreeLocus (goal)
Goal:
R : Type uR
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Flat R M
inst_4 : Module.Finite R M
N : Type u_1
inst_5 : AddCommGroup N
inst_6 : Module R N
inst_7 : Module.Finite R N
inst_8 : Flat R N
p : PrimeSpectrum R
e : Localization.AtPrime p.asIdeal ⊗[R] (M ⊗[R] N) ≃ₗ[Localization.AtPrime p.asIdeal]
  Localization.AtPrime p.asIdeal ⊗[R] M ⊗[Localization.AtPrime p.asIdeal] (Localization.AtPrime p.asIdeal ⊗[R] N) :=
  (LinearEquiv.symm
        (AlgebraTensorModule.assoc R R (Localization.AtPrime p.asIdeal) (Localization.AtPrime p.asIdeal) M N) :
      Localization.AtPrime p.asIdeal ⊗[R] (M ⊗[R] N) ≃ₗ[Localization.AtPrime p.asIdeal]
        Localization.AtPrime p.asIdeal ⊗[R] M ⊗[R] N) ≪≫ₗ
    (LinearEquiv.symm
        (AlgebraTensorModule.cancelBaseChange R (Localization.AtPrime p.asIdeal) (Localization.AtPrime p.asIdeal)
          (Localization.AtPrime p.asIdeal ⊗[R] M) N) :
      Localization.AtPrime p.asIdeal ⊗[R] M ⊗[R] N ≃ₗ[Localization.AtPrime p.asIdeal]
        Localization.AtPrime p.asIdeal ⊗[R] M ⊗[Localization.AtPrime p.asIdeal] (Localization.AtPrime p.asIdeal ⊗[R] N))
h :
  finrank (Localization.AtPrime p.asIdeal) (Localization.AtPrime p.asIdeal ⊗[R] (M ⊗[R] N)) =
    HMul.hMul (α := (p : PrimeSpectrum R) → ℕ) (β := (p : PrimeSpectrum R) → ℕ) (rankAtStalk M) (rankAtStalk N) p
⊢ rankAtStalk (M ⊗[R] N) p =
    HMul.hMul (α := (p : PrimeSpectrum R) → ℕ) (β := (p : PrimeSpectrum R) → ℕ) (rankAtStalk M) (rankAtStalk N) p
have h₁ : finrank (Localization.AtPrime p.asIdeal)
    (Localization.AtPrime p.asIdeal ⊗[R] M ⊗[Localization.AtPrime p.asIdeal] (Localization.AtPrime p.asIdeal ⊗[R] N)) =
  HMul.hMul (α := (p : PrimeSpectrum R) → ℕ) (β := (p : PrimeSpectrum R) → ℕ) (rankAtStalk M) (rankAtStalk N) p
Tactic: rw [rankAtStalk_eq_finrank_tensorProduct, e.finrank_eq, finrank_tensorProduct,
    ← rankAtStalk_eq_finrank_tensorProduct, ← rankAtStalk_eq_finrank_tensorProduct, Pi.mul_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.FreeLocus (goal)
Goal:
R : Type uR
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Flat R M
inst_4 : Module.Finite R M
N : Type u_1
inst_5 : AddCommGroup N
inst_6 : Module R N
inst_7 : Module.Finite R N
inst_8 : Flat R N
p : PrimeSpectrum R
e : Localization.AtPrime p.asIdeal ⊗[R] (M ⊗[R] N) ≃ₗ[Localization.AtPrime p.asIdeal]
  Localization.AtPrime p.asIdeal ⊗[R] M ⊗[Localization.AtPrime p.asIdeal] (Localization.AtPrime p.asIdeal ⊗[R] N) :=
  (LinearEquiv.symm
        (AlgebraTensorModule.assoc R R (Localization.AtPrime p.asIdeal) (Localization.AtPrime p.asIdeal) M N) :
      Localization.AtPrime p.asIdeal ⊗[R] (M ⊗[R] N) ≃ₗ[Localization.AtPrime p.asIdeal]
        Localization.AtPrime p.asIdeal ⊗[R] M ⊗[R] N) ≪≫ₗ
    (LinearEquiv.symm
        (AlgebraTensorModule.cancelBaseChange R (Localization.AtPrime p.asIdeal) (Localization.AtPrime p.asIdeal)
          (Localization.AtPrime p.asIdeal ⊗[R] M) N) :
      Localization.AtPrime p.asIdeal ⊗[R] M ⊗[R] N ≃ₗ[Localization.AtPrime p.asIdeal]
        Localization.AtPrime p.asIdeal ⊗[R] M ⊗[Localization.AtPrime p.asIdeal] (Localization.AtPrime p.asIdeal ⊗[R] N))
h :
  finrank (Localization.AtPrime p.asIdeal) (Localization.AtPrime p.asIdeal ⊗[R] (M ⊗[R] N)) =
    HMul.hMul (α := (p : PrimeSpectrum R) → ℕ) (β := (p : PrimeSpectrum R) → ℕ) (rankAtStalk M) (rankAtStalk N) p
h₁ :
  finrank (Localization.AtPrime p.asIdeal)
      (Localization.AtPrime p.asIdeal ⊗[R] M ⊗[Localization.AtPrime p.asIdeal]
        (Localization.AtPrime p.asIdeal ⊗[R] N)) =
    HMul.hMul (α := (p : PrimeSpectrum R) → ℕ) (β := (p : PrimeSpectrum R) → ℕ) (rankAtStalk M) (rankAtStalk N) p
⊢ rankAtStalk (M ⊗[R] N) p =
    HMul.hMul (α := (p : PrimeSpectrum R) → ℕ) (β := (p : PrimeSpectrum R) → ℕ) (rankAtStalk M) (rankAtStalk N) p
have h₂ : finrank (Localization.AtPrime p.asIdeal) (Localization.AtPrime p.asIdeal ⊗[R] M) *
    finrank (Localization.AtPrime p.asIdeal) (Localization.AtPrime p.asIdeal ⊗[R] N) =
  HMul.hMul (α := (p : PrimeSpectrum R) → ℕ) (β := (p : PrimeSpectrum R) → ℕ) (rankAtStalk M) (rankAtStalk N) p
Tactic: rw [rankAtStalk_eq_finrank_tensorProduct, e.finrank_eq, finrank_tensorProduct,
    ← rankAtStalk_eq_finrank_tensorProduct, ← rankAtStalk_eq_finrank_tensorProduct, Pi.mul_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.FreeLocus (goal)
Goal:
R : Type uR
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Flat R M
inst_4 : Module.Finite R M
N : Type u_1
inst_5 : AddCommGroup N
inst_6 : Module R N
inst_7 : Module.Finite R N
inst_8 : Flat R N
p : PrimeSpectrum R
e : Localization.AtPrime p.asIdeal ⊗[R] (M ⊗[R] N) ≃ₗ[Localization.AtPrime p.asIdeal]
  Localization.AtPrime p.asIdeal ⊗[R] M ⊗[Localization.AtPrime p.asIdeal] (Localization.AtPrime p.asIdeal ⊗[R] N) :=
  (LinearEquiv.symm
        (AlgebraTensorModule.assoc R R (Localization.AtPrime p.asIdeal) (Localization.AtPrime p.asIdeal) M N) :
      Localization.AtPrime p.asIdeal ⊗[R] (M ⊗[R] N) ≃ₗ[Localization.AtPrime p.asIdeal]
        Localization.AtPrime p.asIdeal ⊗[R] M ⊗[R] N) ≪≫ₗ
    (LinearEquiv.symm
        (AlgebraTensorModule.cancelBaseChange R (Localization.AtPrime p.asIdeal) (Localization.AtPrime p.asIdeal)
          (Localization.AtPrime p.asIdeal ⊗[R] M) N) :
      Localization.AtPrime p.asIdeal ⊗[R] M ⊗[R] N ≃ₗ[Localization.AtPrime p.asIdeal]
        Localization.AtPrime p.asIdeal ⊗[R] M ⊗[Localization.AtPrime p.asIdeal] (Localization.AtPrime p.asIdeal ⊗[R] N))
h :
  finrank (Localization.AtPrime p.asIdeal) (Localization.AtPrime p.asIdeal ⊗[R] (M ⊗[R] N)) =
    HMul.hMul (α := (p : PrimeSpectrum R) → ℕ) (β := (p : PrimeSpectrum R) → ℕ) (rankAtStalk M) (rankAtStalk N) p
h₁ :
  finrank (Localization.AtPrime p.asIdeal)
      (Localization.AtPrime p.asIdeal ⊗[R] M ⊗[Localization.AtPrime p.asIdeal]
        (Localization.AtPrime p.asIdeal ⊗[R] N)) =
    HMul.hMul (α := (p : PrimeSpectrum R) → ℕ) (β := (p : PrimeSpectrum R) → ℕ) (rankAtStalk M) (rankAtStalk N) p
h₂ :
  finrank (Localization.AtPrime p.asIdeal) (Localization.AtPrime p.asIdeal ⊗[R] M) *
      finrank (Localization.AtPrime p.asIdeal) (Localization.AtPrime p.asIdeal ⊗[R] N) =
    HMul.hMul (α := (p : PrimeSpectrum R) → ℕ) (β := (p : PrimeSpectrum R) → ℕ) (rankAtStalk M) (rankAtStalk N) p
⊢ rankAtStalk (M ⊗[R] N) p =
    HMul.hMul (α := (p : PrimeSpectrum R) → ℕ) (β := (p : PrimeSpectrum R) → ℕ) (rankAtStalk M) (rankAtStalk N) p
have h₃ : rankAtStalk M p * finrank (Localization.AtPrime p.asIdeal) (Localization.AtPrime p.asIdeal ⊗[R] N) =
  HMul.hMul (α := (p : PrimeSpectrum R) → ℕ) (β := (p : PrimeSpectrum R) → ℕ) (rankAtStalk M) (rankAtStalk N) p
Tactic: rw [rankAtStalk_eq_finrank_tensorProduct, e.finrank_eq, finrank_tensorProduct,
    ← rankAtStalk_eq_finrank_tensorProduct, ← rankAtStalk_eq_finrank_tensorProduct, Pi.mul_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.FreeLocus (goal)
Goal:
R : Type uR
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Flat R M
inst_4 : Module.Finite R M
N : Type u_1
inst_5 : AddCommGroup N
inst_6 : Module R N
inst_7 : Module.Finite R N
inst_8 : Flat R N
p : PrimeSpectrum R
e : Localization.AtPrime p.asIdeal ⊗[R] (M ⊗[R] N) ≃ₗ[Localization.AtPrime p.asIdeal]
  Localization.AtPrime p.asIdeal ⊗[R] M ⊗[Localization.AtPrime p.asIdeal] (Localization.AtPrime p.asIdeal ⊗[R] N) :=
  (LinearEquiv.symm
        (AlgebraTensorModule.assoc R R (Localization.AtPrime p.asIdeal) (Localization.AtPrime p.asIdeal) M N) :
      Localization.AtPrime p.asIdeal ⊗[R] (M ⊗[R] N) ≃ₗ[Localization.AtPrime p.asIdeal]
        Localization.AtPrime p.asIdeal ⊗[R] M ⊗[R] N) ≪≫ₗ
    (LinearEquiv.symm
        (AlgebraTensorModule.cancelBaseChange R (Localization.AtPrime p.asIdeal) (Localization.AtPrime p.asIdeal)
          (Localization.AtPrime p.asIdeal ⊗[R] M) N) :
      Localization.AtPrime p.asIdeal ⊗[R] M ⊗[R] N ≃ₗ[Localization.AtPrime p.asIdeal]
        Localization.AtPrime p.asIdeal ⊗[R] M ⊗[Localization.AtPrime p.asIdeal] (Localization.AtPrime p.asIdeal ⊗[R] N))
h :
  finrank (Localization.AtPrime p.asIdeal) (Localization.AtPrime p.asIdeal ⊗[R] (M ⊗[R] N)) =
    HMul.hMul (α := (p : PrimeSpectrum R) → ℕ) (β := (p : PrimeSpectrum R) → ℕ) (rankAtStalk M) (rankAtStalk N) p
h₁ :
  finrank (Localization.AtPrime p.asIdeal)
      (Localization.AtPrime p.asIdeal ⊗[R] M ⊗[Localization.AtPrime p.asIdeal]
        (Localization.AtPrime p.asIdeal ⊗[R] N)) =
    HMul.hMul (α := (p : PrimeSpectrum R) → ℕ) (β := (p : PrimeSpectrum R) → ℕ) (rankAtStalk M) (rankAtStalk N) p
h₂ :
  finrank (Localization.AtPrime p.asIdeal) (Localization.AtPrime p.asIdeal ⊗[R] M) *
      finrank (Localization.AtPrime p.asIdeal) (Localization.AtPrime p.asIdeal ⊗[R] N) =
    HMul.hMul (α := (p : PrimeSpectrum R) → ℕ) (β := (p : PrimeSpectrum R) → ℕ) (rankAtStalk M) (rankAtStalk N) p
h₃ :
  rankAtStalk M p * finrank (Localization.AtPrime p.asIdeal) (Localization.AtPrime p.asIdeal ⊗[R] N) =
    HMul.hMul (α := (p : PrimeSpectrum R) → ℕ) (β := (p : PrimeSpectrum R) → ℕ) (rankAtStalk M) (rankAtStalk N) p
⊢ rankAtStalk (M ⊗[R] N) p =
    HMul.hMul (α := (p : PrimeSpectrum R) → ℕ) (β := (p : PrimeSpectrum R) → ℕ) (rankAtStalk M) (rankAtStalk N) p
have h₄ : rankAtStalk M p * rankAtStalk N p =
  HMul.hMul (α := (p : PrimeSpectrum R) → ℕ) (β := (p : PrimeSpectrum R) → ℕ) (rankAtStalk M) (rankAtStalk N) p
Tactic: rw [rankAtStalk_eq_finrank_tensorProduct, e.finrank_eq, finrank_tensorProduct,
    ← rankAtStalk_eq_finrank_tensorProduct, ← rankAtStalk_eq_finrank_tensorProduct, Pi.mul_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.FreeLocus (goal)
Goal:
R : Type uR
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Flat R M
inst_4 : Module.Finite R M
N : Type u_1
inst_5 : AddCommGroup N
inst_6 : Module R N
inst_7 : Module.Finite R N
inst_8 : Flat R N
p : PrimeSpectrum R
e : Localization.AtPrime p.asIdeal ⊗[R] (M ⊗[R] N) ≃ₗ[Localization.AtPrime p.asIdeal]
  Localization.AtPrime p.asIdeal ⊗[R] M ⊗[Localization.AtPrime p.asIdeal] (Localization.AtPrime p.asIdeal ⊗[R] N) :=
  (LinearEquiv.symm
        (AlgebraTensorModule.assoc R R (Localization.AtPrime p.asIdeal) (Localization.AtPrime p.asIdeal) M N) :
      Localization.AtPrime p.asIdeal ⊗[R] (M ⊗[R] N) ≃ₗ[Localization.AtPrime p.asIdeal]
        Localization.AtPrime p.asIdeal ⊗[R] M ⊗[R] N) ≪≫ₗ
    (LinearEquiv.symm
        (AlgebraTensorModule.cancelBaseChange R (Localization.AtPrime p.asIdeal) (Localization.AtPrime p.asIdeal)
          (Localization.AtPrime p.asIdeal ⊗[R] M) N) :
      Localization.AtPrime p.asIdeal ⊗[R] M ⊗[R] N ≃ₗ[Localization.AtPrime p.asIdeal]
        Localization.AtPrime p.asIdeal ⊗[R] M ⊗[Localization.AtPrime p.asIdeal] (Localization.AtPrime p.asIdeal ⊗[R] N))
h :
  finrank (Localization.AtPrime p.asIdeal) (Localization.AtPrime p.asIdeal ⊗[R] (M ⊗[R] N)) =
    HMul.hMul (α := (p : PrimeSpectrum R) → ℕ) (β := (p : PrimeSpectrum R) → ℕ) (rankAtStalk M) (rankAtStalk N) p
h₁ :
  finrank (Localization.AtPrime p.asIdeal)
      (Localization.AtPrime p.asIdeal ⊗[R] M ⊗[Localization.AtPrime p.asIdeal]
        (Localization.AtPrime p.asIdeal ⊗[R] N)) =
    HMul.hMul (α := (p : PrimeSpectrum R) → ℕ) (β := (p : PrimeSpectrum R) → ℕ) (rankAtStalk M) (rankAtStalk N) p
h₂ :
  finrank (Localization.AtPrime p.asIdeal) (Localization.AtPrime p.asIdeal ⊗[R] M) *
      finrank (Localization.AtPrime p.asIdeal) (Localization.AtPrime p.asIdeal ⊗[R] N) =
    HMul.hMul (α := (p : PrimeSpectrum R) → ℕ) (β := (p : PrimeSpectrum R) → ℕ) (rankAtStalk M) (rankAtStalk N) p
h₃ :
  rankAtStalk M p * finrank (Localization.AtPrime p.asIdeal) (Localization.AtPrime p.asIdeal ⊗[R] N) =
    HMul.hMul (α := (p : PrimeSpectrum R) → ℕ) (β := (p : PrimeSpectrum R) → ℕ) (rankAtStalk M) (rankAtStalk N) p
h₄ :
  rankAtStalk M p * rankAtStalk N p =
    HMul.hMul (α := (p : PrimeSpectrum R) → ℕ) (β := (p : PrimeSpectrum R) → ℕ) (rankAtStalk M) (rankAtStalk N) p
⊢ rankAtStalk (M ⊗[R] N) p =
    HMul.hMul (α := (p : PrimeSpectrum R) → ℕ) (β := (p : PrimeSpectrum R) → ℕ) (rankAtStalk M) (rankAtStalk N) p
have h₅ : rankAtStalk M p * rankAtStalk N p = rankAtStalk M p * rankAtStalk N p
Tactic: rw [rankAtStalk_eq_finrank_tensorProduct, e.finrank_eq, finrank_tensorProduct,
    ← rankAtStalk_eq_finrank_tensorProduct, ← rankAtStalk_eq_finrank_tensorProduct, Pi.mul_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.FreeLocus (goal)
Goal:
R : Type uR
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Flat R M
inst_4 : Module.Finite R M
p : PrimeSpectrum R
k : Type uR := p.asIdeal.ResidueField
e : k ⊗[Localization.AtPrime p.asIdeal] (Localization.AtPrime p.asIdeal ⊗[R] M) ≃ₗ[k] k ⊗[R] M :=
  AlgebraTensorModule.cancelBaseChange R (Localization.AtPrime p.asIdeal) k k M
⊢ rankAtStalk M p = finrank p.asIdeal.ResidueField (p.asIdeal.Fiber M)
have rw : rankAtStalk M p = finrank k (k ⊗[Localization.AtPrime p.asIdeal] (Localization.AtPrime p.asIdeal ⊗[R] M))
Tactic: rw [← e.finrank_eq, finrank_baseChange, rankAtStalk_eq_finrank_tensorProduct]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.FreeLocus (goal)
Goal:
R : Type uR
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Flat R M
inst_4 : Module.Finite R M
p : PrimeSpectrum R
k : Type uR := p.asIdeal.ResidueField
e : k ⊗[Localization.AtPrime p.asIdeal] (Localization.AtPrime p.asIdeal ⊗[R] M) ≃ₗ[k] k ⊗[R] M :=
  AlgebraTensorModule.cancelBaseChange R (Localization.AtPrime p.asIdeal) k k M
rw : rankAtStalk M p = finrank k (k ⊗[Localization.AtPrime p.asIdeal] (Localization.AtPrime p.asIdeal ⊗[R] M))
⊢ rankAtStalk M p = finrank p.asIdeal.ResidueField (p.asIdeal.Fiber M)
have rw₁ : rankAtStalk M p = finrank (Localization.AtPrime p.asIdeal) (Localization.AtPrime p.asIdeal ⊗[R] M)
Tactic: rw [← e.finrank_eq, finrank_baseChange, rankAtStalk_eq_finrank_tensorProduct]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.FreeLocus (goal)
Goal:
R : Type uR
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Flat R M
inst_4 : Module.Finite R M
p : PrimeSpectrum R
k : Type uR := p.asIdeal.ResidueField
e : k ⊗[Localization.AtPrime p.asIdeal] (Localization.AtPrime p.asIdeal ⊗[R] M) ≃ₗ[k] k ⊗[R] M :=
  AlgebraTensorModule.cancelBaseChange R (Localization.AtPrime p.asIdeal) k k M
rw : rankAtStalk M p = finrank k (k ⊗[Localization.AtPrime p.asIdeal] (Localization.AtPrime p.asIdeal ⊗[R] M))
rw₁ : rankAtStalk M p = finrank (Localization.AtPrime p.asIdeal) (Localization.AtPrime p.asIdeal ⊗[R] M)
⊢ rankAtStalk M p = finrank p.asIdeal.ResidueField (p.asIdeal.Fiber M)
have rw₂ : finrank (Localization.AtPrime p.asIdeal) (Localization.AtPrime p.asIdeal ⊗[R] M) =
  finrank (Localization.AtPrime p.asIdeal) (Localization.AtPrime p.asIdeal ⊗[R] M)
Tactic: rw [← e.finrank_eq, finrank_baseChange, rankAtStalk_eq_finrank_tensorProduct]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.IsOpenComapC (goal)
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
⊢ IsOpen (imageOfDf f)
have rw : IsOpen.{u_1} (X := PrimeSpectrum R) (⋃ (i : ℕ), {x : PrimeSpectrum R | f.coeff i ∉ x.asIdeal})
Tactic: rw [imageOfDf, setOf_exists fun i (x : PrimeSpectrum R) => coeff f i ∉ x.asIdeal]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.IsOpenComapC (goal)
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
⊢ imageOfDf f = PrimeSpectrum.comap C '' (zeroLocus {f})ᶜ
have h : ∀ (x : PrimeSpectrum R),
  x ∈ imageOfDf f ↔ Membership.mem (γ := Set (PrimeSpectrum R)) (PrimeSpectrum.comap C '' (zeroLocus {f})ᶜ) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.IsOpenComapC (goal)
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
x : PrimeSpectrum R
⊢ x ∈ imageOfDf f ↔ Membership.mem (γ := Set (PrimeSpectrum R)) (PrimeSpectrum.comap C '' (zeroLocus {f})ᶜ) x
have h : ∀ (hx : x ∈ imageOfDf f),
  Membership.mem (γ := Set (PrimeSpectrum R[X])) (zeroLocus {f})ᶜ
    { asIdeal := Ideal.map (F := R →+* R[X]) C x.asIdeal, isPrime := sorry }
Tactic: refine ⟨fun hx => ⟨⟨map C x.asIdeal, isPrime_map_C_of_isPrime⟩, ⟨?_, ?_⟩⟩, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.IsOpenComapC (goal)
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
x : PrimeSpectrum R
h :
  ∀ (hx : x ∈ imageOfDf f),
    Membership.mem (γ := Set (PrimeSpectrum R[X])) (zeroLocus {f})ᶜ
      { asIdeal := Ideal.map (F := R →+* R[X]) C x.asIdeal, isPrime := ⋯ }
⊢ x ∈ imageOfDf f ↔ Membership.mem (γ := Set (PrimeSpectrum R)) (PrimeSpectrum.comap C '' (zeroLocus {f})ᶜ) x
have h₁ : ∀ (hx : x ∈ imageOfDf f), PrimeSpectrum.comap C { asIdeal := Ideal.map (F := R →+* R[X]) C x.asIdeal, isPrime := sorry } = x
Tactic: refine ⟨fun hx => ⟨⟨map C x.asIdeal, isPrime_map_C_of_isPrime⟩, ⟨?_, ?_⟩⟩, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.IsOpenComapC (goal)
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
x : PrimeSpectrum R
h :
  ∀ (hx : x ∈ imageOfDf f),
    Membership.mem (γ := Set (PrimeSpectrum R[X])) (zeroLocus {f})ᶜ
      { asIdeal := Ideal.map (F := R →+* R[X]) C x.asIdeal, isPrime := ⋯ }
h₁ :
  ∀ (hx : x ∈ imageOfDf f),
    PrimeSpectrum.comap C { asIdeal := Ideal.map (F := R →+* R[X]) C x.asIdeal, isPrime := ⋯ } = x
⊢ x ∈ imageOfDf f ↔ Membership.mem (γ := Set (PrimeSpectrum R)) (PrimeSpectrum.comap C '' (zeroLocus {f})ᶜ) x
have h₂ : Membership.mem (γ := Set (PrimeSpectrum R)) (PrimeSpectrum.comap C '' (zeroLocus {f})ᶜ) x → x ∈ imageOfDf f
Tactic: refine ⟨fun hx => ⟨⟨map C x.asIdeal, isPrime_map_C_of_isPrime⟩, ⟨?_, ?_⟩⟩, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.IsOpenComapC (goal)
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
x : PrimeSpectrum R
hx : x ∈ imageOfDf f
⊢ Membership.mem (γ := Set (PrimeSpectrum R[X])) (zeroLocus {f})ᶜ
    { asIdeal := Ideal.map (F := R →+* R[X]) C x.asIdeal, isPrime := ⋯ }
have h : f ∉ (↑(asIdeal { asIdeal := Ideal.map (F := R →+* R[X]) C x.asIdeal, isPrime := sorry : PrimeSpectrum R[X] }) : Set R[X])
Tactic: rw [mem_compl_iff, mem_zeroLocus, singleton_subset_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.IsOpenComapC (goal)
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
x : PrimeSpectrum R
hx : x ∈ imageOfDf f
⊢ f ∉ (↑(asIdeal { asIdeal := Ideal.map (F := R →+* R[X]) C x.asIdeal, isPrime := ⋯ : PrimeSpectrum R[X] }) : Set R[X])
have h : ∀ (i : ℕ) (hi : f.coeff i ∉ x.asIdeal),
  f ∉ (↑(asIdeal { asIdeal := Ideal.map (F := R →+* R[X]) C x.asIdeal, isPrime := sorry : PrimeSpectrum R[X] }) : Set R[X])
Tactic: obtain ⟨i, hi⟩ := hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.IsOpenComapC (goal)
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
x : PrimeSpectrum R
hx : x ∈ imageOfDf f
⊢ PrimeSpectrum.comap C { asIdeal := Ideal.map (F := R →+* R[X]) C x.asIdeal, isPrime := ⋯ } = x
have h : ∀ (x_1 : R),
  Membership.mem (γ := Ideal R)
      (asIdeal (PrimeSpectrum.comap C { asIdeal := Ideal.map (F := R →+* R[X]) C x.asIdeal, isPrime := sorry })) x_1 ↔
    x_1 ∈ x.asIdeal
Tactic: ext x